sig
  type token =
      XOR
    | WILDCARD
    | VLINE
    | UPPER_WORD of string
    | UNDERSCORE
    | TYPE_TY
    | TRUE
    | TFF
    | STAR
    | SINGLE_QUOTED of string
    | RIGHT_PAREN
    | RIGHT_BRACKET
    | REAL of string
    | RATIONAL of string
    | NOT_EQUAL
    | NOTVLINE
    | NOTAND
    | NOT
    | LOWER_WORD of string
    | LEFT_PAREN
    | LEFT_IMPLY
    | LEFT_BRACKET
    | INTEGER of string
    | INCLUDE
    | IMPLY
    | GENTZEN_ARROW
    | FORALL_TY
    | FORALL
    | FOF
    | FALSE
    | EXISTS
    | EQUIV
    | EQUAL
    | EOI
    | DOT
    | DOLLAR_WORD of string
    | DOLLAR_DOLLAR_WORD of string
    | DISTINCT_OBJECT of string
    | COMMA
    | COLUMN
    | CNF
    | ARROW
    | AND
  exception Error
  val parse_term :
    (Lexing.lexbuf -> Parse_tptp.token) ->
    Lexing.lexbuf -> Libzipperposition.STerm.t
  val parse_formula :
    (Lexing.lexbuf -> Parse_tptp.token) ->
    Lexing.lexbuf -> Libzipperposition.STerm.t
  val parse_declarations :
    (Lexing.lexbuf -> Parse_tptp.token) ->
    Lexing.lexbuf -> Libzipperposition.STerm.t Ast_tptp.declaration list
  val parse_declaration :
    (Lexing.lexbuf -> Parse_tptp.token) ->
    Lexing.lexbuf -> Libzipperposition.STerm.t Ast_tptp.declaration
  val parse_answer_tuple :
    (Lexing.lexbuf -> Parse_tptp.token) ->
    Lexing.lexbuf -> Libzipperposition.STerm.t list list
end