sig
  type token =
      XOR
    | WILDCARD
    | VLINE
    | UPPER_WORD of string
    | UNDERSCORE
    | TY_TYPE
    | TY_PROP
    | TRUE
    | THF
    | TFF
    | STAR
    | SINGLE_QUOTED of string
    | ROLE_TYPE
    | ROLE_DEFINITION
    | ROLE_CONJECTURE
    | ROLE_AXIOM
    | 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
    | LAMBDA
    | ITE_T
    | ITE_F
    | INTEGER of string
    | INCLUDE
    | IMPLY
    | HO_FORALL
    | HO_EXISTS
    | 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
    | AT
    | ARROW
    | AND
  exception Error
  val parse_ty :
    (Lexing.lexbuf -> TPTP_parser.token) ->
    Lexing.lexbuf -> Nunchaku_core.UntypedAST.ty
  val parse_term :
    (Lexing.lexbuf -> TPTP_parser.token) ->
    Lexing.lexbuf -> Nunchaku_core.UntypedAST.term
  val parse_statement_list :
    (Lexing.lexbuf -> TPTP_parser.token) ->
    Lexing.lexbuf -> Nunchaku_core.UntypedAST.statement list
  val parse_statement :
    (Lexing.lexbuf -> TPTP_parser.token) ->
    Lexing.lexbuf -> Nunchaku_core.UntypedAST.statement
  val parse_ho_form :
    (Lexing.lexbuf -> TPTP_parser.token) ->
    Lexing.lexbuf -> Nunchaku_core.UntypedAST.term
  val parse_fo_form :
    (Lexing.lexbuf -> TPTP_parser.token) ->
    Lexing.lexbuf -> Nunchaku_core.UntypedAST.term
  val parse_answer_tuples :
    (Lexing.lexbuf -> TPTP_parser.token) ->
    Lexing.lexbuf -> Nunchaku_core.UntypedAST.term list list
end