sig
  module E : Env.S
  module C = E.C
  type lemma = C.t
  type axiom = Libzipperposition.ID.t * MetaProverState_intf.term list
  type theory = Libzipperposition.ID.t * MetaProverState_intf.term list
  type rewrite =
      (Libzipperposition.FOTerm.t * Libzipperposition.FOTerm.t) list
  type pre_rewrite =
      (MetaProverState_intf.term * MetaProverState_intf.term) list
  module Result :
    sig
      type t
      val lemmas :
        MetaProverState_intf.S.Result.t -> MetaProverState_intf.S.lemma list
      val theories :
        MetaProverState_intf.S.Result.t -> MetaProverState_intf.S.theory list
      val axioms :
        MetaProverState_intf.S.Result.t -> MetaProverState_intf.S.axiom list
      val rewrite :
        MetaProverState_intf.S.Result.t ->
        MetaProverState_intf.S.rewrite list
      val pre_rewrite :
        MetaProverState_intf.S.Result.t ->
        MetaProverState_intf.S.pre_rewrite list
      val print : Format.formatter -> MetaProverState_intf.S.Result.t -> unit
    end
  val results : unit -> MetaProverState_intf.S.Result.t
  val pop_new_results : unit -> MetaProverState_intf.S.Result.t
  val theories : MetaProverState_intf.S.theory Sequence.t
  val reasoner : Libzipperposition_meta.Reasoner.t
  val prover : Libzipperposition_meta.Prover.t
  val on_theory : MetaProverState_intf.S.theory Signal.t
  val on_lemma : MetaProverState_intf.S.lemma Signal.t
  val on_axiom : MetaProverState_intf.S.axiom Signal.t
  val on_rewrite : MetaProverState_intf.S.rewrite Signal.t
  val on_pre_rewrite : MetaProverState_intf.S.pre_rewrite Signal.t
  val parse_theory_file :
    string -> MetaProverState_intf.S.Result.t MetaProverState_intf.or_error
  val parse_theory_files :
    string list ->
    MetaProverState_intf.S.Result.t MetaProverState_intf.or_error
  val scan_clause : C.t -> MetaProverState_intf.S.Result.t
  val setup : unit -> unit
end