sig
  type ty = Unitype
  type var = FO_tptp.ty Var.t
  type term =
      App of ID.t * FO_tptp.term list
    | Var of FO_tptp.var
    | True
    | False
    | Undefined_atom of FO_tptp.term list
  type form =
      And of FO_tptp.form list
    | Or of FO_tptp.form list
    | Not of FO_tptp.form
    | Imply of FO_tptp.form * FO_tptp.form
    | Equiv of FO_tptp.form * FO_tptp.form
    | Atom of FO_tptp.term
    | Eq of FO_tptp.term * FO_tptp.term
    | Neq of FO_tptp.term * FO_tptp.term
    | Forall of FO_tptp.var * FO_tptp.form
    | Exists of FO_tptp.var * FO_tptp.form
  type role = R_axiom | R_conjecture
  type statement = {
    st_name : string;
    st_role : FO_tptp.role;
    st_form : FO_tptp.form;
  }
  type problem = {
    pb_statements : FO_tptp.statement CCVector.ro_vector;
    pb_meta : ProblemMetadata.t;
  }
  val const : ID.t -> FO_tptp.term
  val app : ID.t -> FO_tptp.term list -> FO_tptp.term
  val var : FO_tptp.var -> FO_tptp.term
  val undefined_atom : FO_tptp.term list -> FO_tptp.term
  val true_ : FO_tptp.term
  val false_ : FO_tptp.term
  val term_equal : FO_tptp.term -> FO_tptp.term -> bool
  val term_hash : FO_tptp.term -> int
  val and_ : FO_tptp.form list -> FO_tptp.form
  val or_ : FO_tptp.form list -> FO_tptp.form
  val imply : FO_tptp.form -> FO_tptp.form -> FO_tptp.form
  val equiv : FO_tptp.form -> FO_tptp.form -> FO_tptp.form
  val atom : FO_tptp.term -> FO_tptp.form
  val not_ : FO_tptp.form -> FO_tptp.form
  val eq : FO_tptp.term -> FO_tptp.term -> FO_tptp.form
  val neq : FO_tptp.term -> FO_tptp.term -> FO_tptp.form
  val forall : FO_tptp.var -> FO_tptp.form -> FO_tptp.form
  val forall_l : FO_tptp.var list -> FO_tptp.form -> FO_tptp.form
  val exists : FO_tptp.var -> FO_tptp.form -> FO_tptp.form
  val exists_l : FO_tptp.var list -> FO_tptp.form -> FO_tptp.form
  val axiom : ?name:string -> FO_tptp.form -> FO_tptp.statement
  val conjecture : ?name:string -> FO_tptp.form -> FO_tptp.statement
  val erase : ID.Erase.state
  val print_role_tptp : FO_tptp.role CCFormat.printer
  val print_term_tptp : FO_tptp.term CCFormat.printer
  val print_form_tptp : FO_tptp.form CCFormat.printer
  val print_statement_tptp : FO_tptp.statement CCFormat.printer
  val print_problem_tptp : FO_tptp.problem CCFormat.printer
end