sig
  type 'a or_error = [ `Error of string | `Ok of 'a ]
  type t
  type clause = Reasoner.clause
  val empty : Prover.t
  val reasoner : Prover.t -> Reasoner.t
  val signature : Prover.t -> Reasoner.ty Libzipperposition.ID.Map.t
  val add :
    Prover.t -> Reasoner.clause -> Prover.t * Reasoner.consequence Sequence.t
  val add_fact :
    Prover.t -> Reasoner.fact -> Prover.t * Reasoner.consequence Sequence.t
  val add_fo_clause :
    Prover.t ->
    Encoding.foclause -> Prover.t * Reasoner.consequence Sequence.t
  module Seq :
    sig
      val to_seq : Prover.t -> Reasoner.clause Sequence.t
      val of_seq :
        Prover.t ->
        Reasoner.clause Sequence.t ->
        Prover.t * Reasoner.consequence Sequence.t
    end
  val of_ho_ast :
    Prover.t ->
    Libzipperposition_parsers.Ast_ho.t Sequence.t ->
    (Prover.t * Reasoner.consequence Sequence.t) Prover.or_error
  val parse_file :
    Prover.t ->
    string -> (Prover.t * Reasoner.consequence Sequence.t) Prover.or_error
end