sig
  type term = Libzipperposition.TypedSTerm.t
  type ty = Reasoner.term
  type property = Reasoner.term
  type fact = Reasoner.term
  val property_ty : Libzipperposition.TypedSTerm.t
  val property_id : Libzipperposition.ID.t
  exception Error of string
  module Clause :
    sig
      type t = { head : Reasoner.term; body : Reasoner.term list; }
      val rule : Reasoner.term -> Reasoner.term list -> Reasoner.Clause.t
      val fact : Reasoner.term -> Reasoner.Clause.t
      val is_fact : Reasoner.Clause.t -> bool
      val pp : t CCFormat.printer
      val to_string : t -> string
      val equal : t -> t -> bool
      val hash_fun : t -> CCHash.state -> CCHash.state
      val hash : t -> int
      val compare : t -> t -> int
      module Seq :
        sig
          val terms : Reasoner.Clause.t -> Reasoner.term Sequence.t
          val vars :
            Reasoner.Clause.t ->
            Reasoner.ty Libzipperposition.Var.t Sequence.t
        end
    end
  type clause = Reasoner.Clause.t
  module Proof :
    sig
      type t =
          Axiom
        | Resolved of Reasoner.fact Reasoner.Proof.with_proof *
            Reasoner.clause Reasoner.Proof.with_proof
      and 'a with_proof = { conclusion : 'a; proof : Reasoner.Proof.t; }
      val facts : Reasoner.Proof.t -> Reasoner.fact Sequence.t
      val rules : Reasoner.Proof.t -> Reasoner.clause Sequence.t
    end
  type proof = Reasoner.Proof.t
  type consequence = Reasoner.fact * Reasoner.proof
  type t
  val empty : Reasoner.t
  val add :
    Reasoner.t ->
    Reasoner.clause -> Reasoner.t * Reasoner.consequence Sequence.t
  val add_fact :
    Reasoner.t ->
    Reasoner.fact -> Reasoner.t * Reasoner.consequence Sequence.t
  module Seq :
    sig
      val of_seq :
        Reasoner.t ->
        Reasoner.clause Sequence.t ->
        Reasoner.t * Reasoner.consequence Sequence.t
      val to_seq : Reasoner.t -> Reasoner.clause Sequence.t
      val facts : Reasoner.t -> Reasoner.fact Sequence.t
    end
end