sig
  type id = ID.t
  type 'a var = 'a Var.t
  type 'a printer = Format.formatter -> 'a -> unit
  type 'a or_error = ('a, string) CCResult.t
  type metadata = ProblemMetadata.t
  type ('a, 'b) res = ('a, 'b) Problem.Res.t
  module TyBuiltin :
    sig
      type t = [ `Prop | `Unitype ]
      val equal : FO.TyBuiltin.t -> FO.TyBuiltin.t -> bool
      val compare : FO.TyBuiltin.t -> FO.TyBuiltin.t -> int
      val print : FO.TyBuiltin.t FO.printer
    end
  module Builtin :
    sig
      type t = [ `Int of int ]
      val equal : FO.Builtin.t -> FO.Builtin.t -> bool
      val compare : FO.Builtin.t -> FO.Builtin.t -> int
      val print : FO.Builtin.t FO.printer
    end
  type ('t, 'ty) view =
      Builtin of FO.Builtin.t
    | Var of 'ty FO.var
    | App of FO.id * 't list
    | DataTest of FO.id * 't
    | DataSelect of FO.id * int * 't
    | Undefined of FO.id * 't
    | Undefined_atom of FO.id * 'ty FO.toplevel_ty * 't list
    | Unparsable of 'ty
    | Fun of 'ty FO.var * 't
    | Mu of 'ty FO.var * 't
    | Let of 'ty FO.var * 't * 't
    | Ite of 't * 't * 't
    | True
    | False
    | Eq of 't * 't
    | And of 't list
    | Or of 't list
    | Not of 't
    | Imply of 't * 't
    | Equiv of 't * 't
    | Forall of 'ty FO.var * 't
    | Exists of 'ty FO.var * 't
  and 'ty toplevel_ty = 'ty list * 'ty
  type 'ty ty_view = TyBuiltin of FO.TyBuiltin.t | TyApp of FO.id * 'ty list
  type 'ty constructor = { cstor_name : FO.id; cstor_args : 'ty list; }
  type 'ty tydef = {
    ty_name : FO.id;
    ty_cstors : 'ty FO.constructor ID.Map.t;
  }
  type 'ty mutual_types = {
    tys_vars : FO.id list;
    tys_defs : 'ty FO.tydef list;
  }
  type attr = Attr_pseudo_prop | Attr_pseudo_true
  type ('t, 'ty) statement =
      TyDecl of FO.id * int * FO.attr list
    | Decl of FO.id * 'ty FO.toplevel_ty * FO.attr list
    | Axiom of 't
    | CardBound of FO.id * [ `Max | `Min ] * int
    | MutualTypes of [ `Codata | `Data ] * 'ty FO.mutual_types
    | Goal of 't
  module Ty :
    sig
      type t
      type toplevel_ty = FO.Ty.t list * FO.Ty.t
      val view : FO.Ty.t -> FO.Ty.t FO.ty_view
      val const : FO.id -> FO.Ty.t
      val app : FO.id -> FO.Ty.t list -> FO.Ty.t
      val builtin : FO.TyBuiltin.t -> FO.Ty.t
      val arrow : FO.Ty.t list -> FO.Ty.t -> FO.Ty.toplevel_ty
      val is_prop : FO.Ty.t -> bool
      val equal : FO.Ty.t -> FO.Ty.t -> bool
      val compare : FO.Ty.t -> FO.Ty.t -> int
      val hash : FO.Ty.t -> int
      val to_seq : FO.Ty.t -> FO.Ty.t Sequence.t
    end
  module T :
    sig
      type t
      val view : FO.T.t -> (FO.T.t, FO.Ty.t) FO.view
      val compare : FO.T.t -> FO.T.t -> int
      val equal : FO.T.t -> FO.T.t -> bool
      val hash : FO.T.t -> int
      val builtin : FO.Builtin.t -> FO.T.t
      val const : FO.id -> FO.T.t
      val app : FO.id -> FO.T.t list -> FO.T.t
      val data_test : FO.id -> FO.T.t -> FO.T.t
      val data_select : FO.id -> int -> FO.T.t -> FO.T.t
      val undefined : FO.id -> FO.T.t -> FO.T.t
      val undefined_atom :
        FO.id -> FO.Ty.toplevel_ty -> FO.T.t list -> FO.T.t
      val unparsable : FO.Ty.t -> FO.T.t
      val var : FO.Ty.t FO.var -> FO.T.t
      val let_ : FO.Ty.t FO.var -> FO.T.t -> FO.T.t -> FO.T.t
      val fun_ : FO.Ty.t FO.var -> FO.T.t -> FO.T.t
      val mu : FO.Ty.t FO.var -> FO.T.t -> FO.T.t
      val ite : FO.T.t -> FO.T.t -> FO.T.t -> FO.T.t
      val true_ : FO.T.t
      val false_ : FO.T.t
      val eq : FO.T.t -> FO.T.t -> FO.T.t
      val and_ : FO.T.t list -> FO.T.t
      val or_ : FO.T.t list -> FO.T.t
      val not_ : FO.T.t -> FO.T.t
      val imply : FO.T.t -> FO.T.t -> FO.T.t
      val equiv : FO.T.t -> FO.T.t -> FO.T.t
      val forall : FO.Ty.t FO.var -> FO.T.t -> FO.T.t
      val exists : FO.Ty.t FO.var -> FO.T.t -> FO.T.t
      val to_seq : FO.T.t -> FO.T.t Sequence.t
    end
  module Problem :
    sig
      type ('t, 'ty) t = {
        statements : ('t, 'ty) FO.statement CCVector.ro_vector;
        meta : FO.metadata;
      }
      val make :
        meta:FO.metadata ->
        ('t, 'ty) FO.statement CCVector.ro_vector -> ('t, 'ty) FO.Problem.t
      val of_list :
        meta:FO.metadata ->
        ('t, 'ty) FO.statement list -> ('t, 'ty) FO.Problem.t
      val statements :
        ('t, 'ty) FO.Problem.t -> ('t, 'ty) FO.statement CCVector.ro_vector
      val meta : ('a, 'b) FO.Problem.t -> FO.metadata
      val map :
        meta:FO.metadata ->
        (('t, 'ty) FO.statement -> ('t2, 'ty2) FO.statement) ->
        ('t, 'ty) FO.Problem.t -> ('t2, 'ty2) FO.Problem.t
      val flat_map :
        meta:FO.metadata ->
        (('t, 'ty) FO.statement -> ('t2, 'ty2) FO.statement list) ->
        ('t, 'ty) FO.Problem.t -> ('t2, 'ty2) FO.Problem.t
      val fold_flat_map :
        meta:FO.metadata ->
        ('acc ->
         ('t, 'ty) FO.statement -> 'acc * ('t2, 'ty2) FO.statement list) ->
        'acc -> ('t, 'ty) FO.Problem.t -> 'acc * ('t2, 'ty2) FO.Problem.t
      val to_seq :
        ('t, 'ty) FO.Problem.t -> ('t, 'ty) FO.statement Sequence.t
    end
  module Util :
    sig
      val dt_of_term :
        vars:FO.Ty.t Var.t list -> FO.T.t -> (FO.T.t, FO.Ty.t) Model.DT.t
      val problem_kinds :
        ('a, FO.Ty.t) FO.Problem.t -> Model.symbol_kind ID.Map.t
    end
  val tys_of_toplevel_ty : 'ty FO.toplevel_ty -> 'ty Sequence.t
  val terms_of_statement : ('t, 'a) FO.statement -> 't Sequence.t
  val tys_of_statement : ('a, 'ty) FO.statement -> 'ty Sequence.t
  val print_ty : FO.Ty.t FO.printer
  val print_toplevel_ty : FO.Ty.toplevel_ty FO.printer
  val print_term : FO.T.t FO.printer
  val print_term' : 'a -> FO.T.t FO.printer
  val print_statement : (FO.T.t, FO.Ty.t) FO.statement FO.printer
  val print_model : (FO.T.t * FO.T.t) list FO.printer
  val print_problem : (FO.T.t, FO.Ty.t) FO.Problem.t FO.printer
  module To_tptp :
    sig
      exception Error of string
      val conv_form : FO.T.t -> FO_tptp.form
      val conv_statement :
        (FO.T.t, FO.Ty.t) FO.statement -> FO_tptp.statement option
      val conv_problem : (FO.T.t, FO.Ty.t) FO.Problem.t -> FO_tptp.problem
    end
  module Of_tptp :
    sig
      val conv_ty : FO_tptp.ty -> FO.Ty.t
      val conv_term : FO_tptp.term -> FO.T.t
      val conv_form : FO_tptp.form -> FO.T.t
    end
  val pipe_tptp :
    ((FO.T.t, FO.Ty.t) FO.Problem.t, FO_tptp.problem,
     (FO_tptp.term, FO_tptp.ty) FO.res, (FO.T.t, FO.Ty.t) FO.res)
    Transform.t
end