functor (C : Clause.S) ->
  sig
    module Ctx :
      sig
        val ord : unit -> Libzipperposition.Ordering.t
        val selection_fun : unit -> Selection.t
        val set_selection_fun : Selection.t -> unit
        val set_ord : Libzipperposition.Ordering.t -> unit
        val signature : unit -> Libzipperposition.Signature.t
        val renaming : Libzipperposition.Substs.Renaming.t
        val compare :
          Libzipperposition.FOTerm.t ->
          Libzipperposition.FOTerm.t -> Libzipperposition.Comparison.t
        val select : Selection.t
        val renaming_clear : unit -> Libzipperposition.Substs.Renaming.t
        val lost_completeness : unit -> unit
        val is_completeness_preserved : unit -> bool
        val add_signature : Libzipperposition.Signature.t -> unit
        val find_signature :
          Libzipperposition.ID.t -> Libzipperposition.Type.t option
        val find_signature_exn :
          Libzipperposition.ID.t -> Libzipperposition.Type.t
        val declare :
          Libzipperposition.ID.t -> Libzipperposition.Type.t -> unit
        val on_new_symbol :
          (Libzipperposition.ID.t * Libzipperposition.Type.t) Signal.t
        val on_signature_update : Libzipperposition.Signature.t Signal.t
        module Lit :
          sig
            val from_hooks : unit -> Literal.Conv.hook_from list
            val add_from_hook : Literal.Conv.hook_from -> unit
            val to_hooks : unit -> Literal.Conv.hook_to list
            val add_to_hook : Literal.Conv.hook_to -> unit
            val of_form :
              Libzipperposition.FOTerm.t Libzipperposition.SLiteral.t ->
              Literal.t
            val to_form :
              Literal.t ->
              Libzipperposition.FOTerm.t Libzipperposition.SLiteral.t
          end
      end
    module C :
      sig
        module Ctx :
          sig
            val ord : unit -> Libzipperposition.Ordering.t
            val selection_fun : unit -> Selection.t
            val set_selection_fun : Selection.t -> unit
            val set_ord : Libzipperposition.Ordering.t -> unit
            val signature : unit -> Libzipperposition.Signature.t
            val renaming : Libzipperposition.Substs.Renaming.t
            val compare :
              Libzipperposition.FOTerm.t ->
              Libzipperposition.FOTerm.t -> Libzipperposition.Comparison.t
            val select : Selection.t
            val renaming_clear : unit -> Libzipperposition.Substs.Renaming.t
            val lost_completeness : unit -> unit
            val is_completeness_preserved : unit -> bool
            val add_signature : Libzipperposition.Signature.t -> unit
            val find_signature :
              Libzipperposition.ID.t -> Libzipperposition.Type.t option
            val find_signature_exn :
              Libzipperposition.ID.t -> Libzipperposition.Type.t
            val declare :
              Libzipperposition.ID.t -> Libzipperposition.Type.t -> unit
            val on_new_symbol :
              (Libzipperposition.ID.t * Libzipperposition.Type.t) Signal.t
            val on_signature_update : Libzipperposition.Signature.t Signal.t
            module Lit :
              sig
                val from_hooks : unit -> Literal.Conv.hook_from list
                val add_from_hook : Literal.Conv.hook_from -> unit
                val to_hooks : unit -> Literal.Conv.hook_to list
                val add_to_hook : Literal.Conv.hook_to -> unit
                val of_form :
                  Libzipperposition.FOTerm.t Libzipperposition.SLiteral.t ->
                  Literal.t
                val to_form :
                  Literal.t ->
                  Libzipperposition.FOTerm.t Libzipperposition.SLiteral.t
              end
          end
        type t = C.t
        type clause = t
        type flag = SClause.flag
        val set_flag : flag -> t -> bool -> unit
        val get_flag : flag -> t -> bool
        val mark_redundant : t -> unit
        val is_redundant : t -> bool
        val mark_backward_simplified : t -> unit
        val is_backward_simplified : t -> bool
        val equal : t -> t -> bool
        val hash_fun : t -> CCHash.state -> CCHash.state
        val hash : t -> int
        val compare : t -> t -> int
        val id : t -> int
        val lits : t -> Literal.t array
        val is_ground : t -> bool
        val weight : t -> int
        module CHashtbl :
          sig
            type key = t
            type 'a t = 'a C.CHashtbl.t
            val create : int -> 'a t
            val clear : 'a t -> unit
            val reset : 'a t -> unit
            val copy : 'a t -> 'a t
            val add : 'a t -> key -> 'a -> unit
            val remove : 'a t -> key -> unit
            val find : 'a t -> key -> 'a
            val find_all : 'a t -> key -> 'a list
            val replace : 'a t -> key -> 'a -> unit
            val mem : 'a t -> key -> bool
            val iter : (key -> 'a -> unit) -> 'a t -> unit
            val fold : (key -> 'a -> 'b -> 'b) -> 'a t -> 'b -> 'b
            val length : 'a t -> int
            val stats : 'a t -> Hashtbl.statistics
            val get : 'a t -> key -> 'a option
            val get_or : 'a t -> key -> or_:'a -> 'a
            val add_list : 'a list t -> key -> 'a -> unit
            val incr : ?by:int -> int t -> key -> unit
            val decr : ?by:int -> int t -> key -> unit
            val keys : 'a t -> key CCHashtbl.sequence
            val values : 'a t -> 'a CCHashtbl.sequence
            val keys_list : 'a t -> key list
            val values_list : 'a t -> 'a list
            val map_list : (key -> 'a -> 'b) -> 'a t -> 'b list
            val to_seq : 'a t -> (key * 'a) CCHashtbl.sequence
            val of_seq : (key * 'a) CCHashtbl.sequence -> 'a t
            val add_seq : 'a t -> (key * 'a) CCHashtbl.sequence -> unit
            val add_seq_count : int t -> key CCHashtbl.sequence -> unit
            val of_seq_count : key CCHashtbl.sequence -> int t
            val to_list : 'a t -> (key * 'a) list
            val of_list : (key * 'a) list -> 'a t
            val update :
              'a t -> f:(key -> 'a option -> 'a option) -> k:key -> unit
            val print :
              key CCHashtbl.printer ->
              'a CCHashtbl.printer -> 'a t CCHashtbl.printer
          end
        val is_goal : t -> bool
        val distance_to_goal : t -> int option
        val pp_trail : Trail.t CCFormat.printer
        val has_trail : t -> bool
        val trail : t -> Trail.t
        val trail_l : t list -> Trail.t
        val update_trail : (Trail.t -> Trail.t) -> t -> t
        val trail_subsumes : t -> t -> bool
        val is_active : t -> v:Trail.valuation -> bool
        val create :
          trail:Trail.t -> Literal.t list -> Clause_intf.proof_step -> t
        val create_a :
          trail:Trail.t -> Literal.t array -> Clause_intf.proof_step -> t
        val of_sclause : SClause.t -> Clause_intf.proof_step -> t
        val of_forms :
          trail:Trail.t ->
          Libzipperposition.FOTerm.t Libzipperposition.SLiteral.t list ->
          Clause_intf.proof_step -> t
        val of_forms_axiom :
          file:string ->
          name:string ->
          Libzipperposition.FOTerm.t Libzipperposition.SLiteral.t list -> t
        val of_statement : Libzipperposition.Statement.clause_t -> t list
        val proof_step : t -> Clause_intf.proof_step
        val proof : t -> Clause_intf.proof
        val update_proof :
          t -> (Clause_intf.proof_step -> Clause_intf.proof_step) -> t
        val is_empty : t -> bool
        val length : t -> int
        val apply_subst :
          renaming:Libzipperposition.Substs.Renaming.t ->
          Libzipperposition.Substs.t -> t Libzipperposition.Scoped.t -> t
        val maxlits :
          t Libzipperposition.Scoped.t ->
          Libzipperposition.Substs.t -> CCBV.t
        val is_maxlit :
          t Libzipperposition.Scoped.t ->
          Libzipperposition.Substs.t -> idx:int -> bool
        val eligible_res :
          t Libzipperposition.Scoped.t ->
          Libzipperposition.Substs.t -> CCBV.t
        val eligible_param :
          t Libzipperposition.Scoped.t ->
          Libzipperposition.Substs.t -> CCBV.t
        val is_eligible_param :
          t Libzipperposition.Scoped.t ->
          Libzipperposition.Substs.t -> idx:int -> bool
        val has_selected_lits : t -> bool
        val is_selected : t -> int -> bool
        val selected_lits : t -> (Literal.t * int) list
        val is_unit_clause : t -> bool
        val is_oriented_rule : t -> bool
        val symbols :
          ?init:Libzipperposition.ID.Set.t ->
          t Sequence.t -> Libzipperposition.ID.Set.t
        val to_sclause : t -> SClause.t
        val to_forms :
          t -> Libzipperposition.FOTerm.t Libzipperposition.SLiteral.t list
        module Seq :
          sig
            val lits : t -> Literal.t Sequence.t
            val terms : t -> Libzipperposition.FOTerm.t Sequence.t
            val vars :
              t ->
              Libzipperposition.Type.t Libzipperposition.HVar.t Sequence.t
          end
        module Eligible :
          sig
            type t = int -> Literal.t -> bool
            val res : clause -> t
            val param : clause -> t
            val eq : t
            val arith : t
            val filter : (Literal.t -> bool) -> t
            val max : clause -> t
            val pos : t
            val neg : t
            val always : t
            val combine : t list -> t
            val ( ** ) : t -> t -> t
            val ( ++ ) : t -> t -> t
            val ( ~~ ) : t -> t
          end
        module ClauseSet :
          sig
            type elt = t
            type t = C.ClauseSet.t
            val empty : t
            val is_empty : t -> bool
            val mem : elt -> t -> bool
            val add : elt -> t -> t
            val singleton : elt -> t
            val remove : elt -> t -> t
            val union : t -> t -> t
            val inter : t -> t -> t
            val diff : t -> t -> t
            val compare : t -> t -> int
            val equal : t -> t -> bool
            val subset : t -> t -> bool
            val iter : (elt -> unit) -> t -> unit
            val fold : (elt -> 'a -> 'a) -> t -> 'a -> 'a
            val for_all : (elt -> bool) -> t -> bool
            val exists : (elt -> bool) -> t -> bool
            val filter : (elt -> bool) -> t -> t
            val partition : (elt -> bool) -> t -> t * t
            val cardinal : t -> int
            val elements : t -> elt list
            val min_elt : t -> elt
            val max_elt : t -> elt
            val choose : t -> elt
            val split : elt -> t -> t * bool * t
            val find : elt -> t -> elt
            val of_seq : elt CCSet.sequence -> t
            val add_seq : t -> elt CCSet.sequence -> t
            val to_seq : t -> elt CCSet.sequence
            val of_list : elt list -> t
            val add_list : t -> elt list -> t
            val to_list : t -> elt list
            val pp :
              ?start:string ->
              ?stop:string ->
              ?sep:string -> elt CCSet.printer -> t CCSet.printer
            val print :
              ?start:string ->
              ?stop:string ->
              ?sep:string -> elt CCSet.formatter -> t CCSet.formatter
          end
        module Pos :
          sig
            val at :
              t -> Libzipperposition.Position.t -> Libzipperposition.FOTerm.t
          end
        module WithPos :
          sig
            type t =
              C.WithPos.t = {
              clause : clause;
              pos : Libzipperposition.Position.t;
              term : Libzipperposition.FOTerm.t;
            }
            val compare : t -> t -> int
            val pp : t CCFormat.printer
          end
        val pp : t CCFormat.printer
        val pp_tstp : t CCFormat.printer
        val pp_tstp_full : t CCFormat.printer
        val to_string : t -> string
        val pp_set : ClauseSet.t CCFormat.printer
        val pp_set_tstp : ClauseSet.t CCFormat.printer
      end
    module CQueue :
      sig
        module C :
          sig
            module Ctx :
              sig
                val ord : unit -> Libzipperposition.Ordering.t
                val selection_fun : unit -> Selection.t
                val set_selection_fun : Selection.t -> unit
                val set_ord : Libzipperposition.Ordering.t -> unit
                val signature : unit -> Libzipperposition.Signature.t
                val renaming : Libzipperposition.Substs.Renaming.t
                val compare :
                  Libzipperposition.FOTerm.t ->
                  Libzipperposition.FOTerm.t ->
                  Libzipperposition.Comparison.t
                val select : Selection.t
                val renaming_clear :
                  unit -> Libzipperposition.Substs.Renaming.t
                val lost_completeness : unit -> unit
                val is_completeness_preserved : unit -> bool
                val add_signature : Libzipperposition.Signature.t -> unit
                val find_signature :
                  Libzipperposition.ID.t -> Libzipperposition.Type.t option
                val find_signature_exn :
                  Libzipperposition.ID.t -> Libzipperposition.Type.t
                val declare :
                  Libzipperposition.ID.t -> Libzipperposition.Type.t -> unit
                val on_new_symbol :
                  (Libzipperposition.ID.t * Libzipperposition.Type.t)
                  Signal.t
                val on_signature_update :
                  Libzipperposition.Signature.t Signal.t
                module Lit :
                  sig
                    val from_hooks : unit -> Literal.Conv.hook_from list
                    val add_from_hook : Literal.Conv.hook_from -> unit
                    val to_hooks : unit -> Literal.Conv.hook_to list
                    val add_to_hook : Literal.Conv.hook_to -> unit
                    val of_form :
                      Libzipperposition.FOTerm.t Libzipperposition.SLiteral.t ->
                      Literal.t
                    val to_form :
                      Literal.t ->
                      Libzipperposition.FOTerm.t Libzipperposition.SLiteral.t
                  end
              end
            type t = C.t
            type clause = t
            type flag = SClause.flag
            val set_flag : flag -> t -> bool -> unit
            val get_flag : flag -> t -> bool
            val mark_redundant : t -> unit
            val is_redundant : t -> bool
            val mark_backward_simplified : t -> unit
            val is_backward_simplified : t -> bool
            val equal : t -> t -> bool
            val hash_fun : t -> CCHash.state -> CCHash.state
            val hash : t -> int
            val compare : t -> t -> int
            val id : t -> int
            val lits : t -> Literal.t array
            val is_ground : t -> bool
            val weight : t -> int
            module CHashtbl :
              sig
                type key = t
                type 'a t = 'a C.CHashtbl.t
                val create : int -> 'a t
                val clear : 'a t -> unit
                val reset : 'a t -> unit
                val copy : 'a t -> 'a t
                val add : 'a t -> key -> 'a -> unit
                val remove : 'a t -> key -> unit
                val find : 'a t -> key -> 'a
                val find_all : 'a t -> key -> 'a list
                val replace : 'a t -> key -> 'a -> unit
                val mem : 'a t -> key -> bool
                val iter : (key -> 'a -> unit) -> 'a t -> unit
                val fold : (key -> 'a -> 'b -> 'b) -> 'a t -> 'b -> 'b
                val length : 'a t -> int
                val stats : 'a t -> Hashtbl.statistics
                val get : 'a t -> key -> 'a option
                val get_or : 'a t -> key -> or_:'a -> 'a
                val add_list : 'a list t -> key -> 'a -> unit
                val incr : ?by:int -> int t -> key -> unit
                val decr : ?by:int -> int t -> key -> unit
                val keys : 'a t -> key CCHashtbl.sequence
                val values : 'a t -> 'a CCHashtbl.sequence
                val keys_list : 'a t -> key list
                val values_list : 'a t -> 'a list
                val map_list : (key -> 'a -> 'b) -> 'a t -> 'b list
                val to_seq : 'a t -> (key * 'a) CCHashtbl.sequence
                val of_seq : (key * 'a) CCHashtbl.sequence -> 'a t
                val add_seq : 'a t -> (key * 'a) CCHashtbl.sequence -> unit
                val add_seq_count : int t -> key CCHashtbl.sequence -> unit
                val of_seq_count : key CCHashtbl.sequence -> int t
                val to_list : 'a t -> (key * 'a) list
                val of_list : (key * 'a) list -> 'a t
                val update :
                  'a t -> f:(key -> 'a option -> 'a option) -> k:key -> unit
                val print :
                  key CCHashtbl.printer ->
                  'a CCHashtbl.printer -> 'a t CCHashtbl.printer
              end
            val is_goal : t -> bool
            val distance_to_goal : t -> int option
            val pp_trail : Trail.t CCFormat.printer
            val has_trail : t -> bool
            val trail : t -> Trail.t
            val trail_l : t list -> Trail.t
            val update_trail : (Trail.t -> Trail.t) -> t -> t
            val trail_subsumes : t -> t -> bool
            val is_active : t -> v:Trail.valuation -> bool
            val create :
              trail:Trail.t -> Literal.t list -> Clause_intf.proof_step -> t
            val create_a :
              trail:Trail.t -> Literal.t array -> Clause_intf.proof_step -> t
            val of_sclause : SClause.t -> Clause_intf.proof_step -> t
            val of_forms :
              trail:Trail.t ->
              Libzipperposition.FOTerm.t Libzipperposition.SLiteral.t list ->
              Clause_intf.proof_step -> t
            val of_forms_axiom :
              file:string ->
              name:string ->
              Libzipperposition.FOTerm.t Libzipperposition.SLiteral.t list ->
              t
            val of_statement : Libzipperposition.Statement.clause_t -> t list
            val proof_step : t -> Clause_intf.proof_step
            val proof : t -> Clause_intf.proof
            val update_proof :
              t -> (Clause_intf.proof_step -> Clause_intf.proof_step) -> t
            val is_empty : t -> bool
            val length : t -> int
            val apply_subst :
              renaming:Libzipperposition.Substs.Renaming.t ->
              Libzipperposition.Substs.t -> t Libzipperposition.Scoped.t -> t
            val maxlits :
              t Libzipperposition.Scoped.t ->
              Libzipperposition.Substs.t -> CCBV.t
            val is_maxlit :
              t Libzipperposition.Scoped.t ->
              Libzipperposition.Substs.t -> idx:int -> bool
            val eligible_res :
              t Libzipperposition.Scoped.t ->
              Libzipperposition.Substs.t -> CCBV.t
            val eligible_param :
              t Libzipperposition.Scoped.t ->
              Libzipperposition.Substs.t -> CCBV.t
            val is_eligible_param :
              t Libzipperposition.Scoped.t ->
              Libzipperposition.Substs.t -> idx:int -> bool
            val has_selected_lits : t -> bool
            val is_selected : t -> int -> bool
            val selected_lits : t -> (Literal.t * int) list
            val is_unit_clause : t -> bool
            val is_oriented_rule : t -> bool
            val symbols :
              ?init:Libzipperposition.ID.Set.t ->
              t Sequence.t -> Libzipperposition.ID.Set.t
            val to_sclause : t -> SClause.t
            val to_forms :
              t ->
              Libzipperposition.FOTerm.t Libzipperposition.SLiteral.t list
            module Seq :
              sig
                val lits : t -> Literal.t Sequence.t
                val terms : t -> Libzipperposition.FOTerm.t Sequence.t
                val vars :
                  t ->
                  Libzipperposition.Type.t Libzipperposition.HVar.t
                  Sequence.t
              end
            module Eligible :
              sig
                type t = int -> Literal.t -> bool
                val res : clause -> t
                val param : clause -> t
                val eq : t
                val arith : t
                val filter : (Literal.t -> bool) -> t
                val max : clause -> t
                val pos : t
                val neg : t
                val always : t
                val combine : t list -> t
                val ( ** ) : t -> t -> t
                val ( ++ ) : t -> t -> t
                val ( ~~ ) : t -> t
              end
            module ClauseSet :
              sig
                type elt = t
                type t = C.ClauseSet.t
                val empty : t
                val is_empty : t -> bool
                val mem : elt -> t -> bool
                val add : elt -> t -> t
                val singleton : elt -> t
                val remove : elt -> t -> t
                val union : t -> t -> t
                val inter : t -> t -> t
                val diff : t -> t -> t
                val compare : t -> t -> int
                val equal : t -> t -> bool
                val subset : t -> t -> bool
                val iter : (elt -> unit) -> t -> unit
                val fold : (elt -> 'a -> 'a) -> t -> 'a -> 'a
                val for_all : (elt -> bool) -> t -> bool
                val exists : (elt -> bool) -> t -> bool
                val filter : (elt -> bool) -> t -> t
                val partition : (elt -> bool) -> t -> t * t
                val cardinal : t -> int
                val elements : t -> elt list
                val min_elt : t -> elt
                val max_elt : t -> elt
                val choose : t -> elt
                val split : elt -> t -> t * bool * t
                val find : elt -> t -> elt
                val of_seq : elt CCSet.sequence -> t
                val add_seq : t -> elt CCSet.sequence -> t
                val to_seq : t -> elt CCSet.sequence
                val of_list : elt list -> t
                val add_list : t -> elt list -> t
                val to_list : t -> elt list
                val pp :
                  ?start:string ->
                  ?stop:string ->
                  ?sep:string -> elt CCSet.printer -> t CCSet.printer
                val print :
                  ?start:string ->
                  ?stop:string ->
                  ?sep:string -> elt CCSet.formatter -> t CCSet.formatter
              end
            module Pos :
              sig
                val at :
                  t ->
                  Libzipperposition.Position.t -> Libzipperposition.FOTerm.t
              end
            module WithPos :
              sig
                type t =
                  C.WithPos.t = {
                  clause : clause;
                  pos : Libzipperposition.Position.t;
                  term : Libzipperposition.FOTerm.t;
                }
                val compare : t -> t -> int
                val pp : t CCFormat.printer
              end
            val pp : t CCFormat.printer
            val pp_tstp : t CCFormat.printer
            val pp_tstp_full : t CCFormat.printer
            val to_string : t -> string
            val pp_set : ClauseSet.t CCFormat.printer
            val pp_set_tstp : ClauseSet.t CCFormat.printer
          end
        module WeightFun :
          sig
            type t = C.t -> int
            val default : t
            val age : t
            val favor_all_neg : t
            val favor_non_all_neg : t
            val favor_ground : t
            val favor_horn : t
            val favor_goal : t
            val combine : (t * int) list -> t
          end
        type t
        val add : t -> C.t -> t
        val adds : t -> C.t Sequence.t -> t
        val is_empty : t -> bool
        val take_first : t -> t * C.t
        val name : t -> string
        val make : weight:(C.t -> int) -> string -> t
        val bfs : t
        val explore : t
        val ground : t
        val goal_oriented : t
        val default : t
        val of_profile : ClauseQueue_intf.profile -> t
        val pp : t CCFormat.printer
        val to_string : t -> string
      end
    module TermIndex :
      sig
        type t
        type elt = C.WithPos.t
        module Leaf :
          sig
            type t
            type elt = elt
            val empty : t
            val add : t -> Libzipperposition.Index_intf.term -> elt -> t
            val remove : t -> Libzipperposition.Index_intf.term -> elt -> t
            val is_empty : t -> bool
            val iter :
              t -> (Libzipperposition.Index_intf.term -> elt -> unit) -> unit
            val fold :
              t ->
              'a ->
              ('a -> Libzipperposition.Index_intf.term -> elt -> 'a) -> 'a
            val size : t -> int
            val fold_unify :
              ?subst:Libzipperposition.Index_intf.subst ->
              t Libzipperposition.Scoped.t ->
              Libzipperposition.Index_intf.term Libzipperposition.Scoped.t ->
              (Libzipperposition.Index_intf.term * elt *
               Libzipperposition.Index_intf.subst)
              Sequence.t
            val fold_match :
              ?subst:Libzipperposition.Index_intf.subst ->
              t Libzipperposition.Scoped.t ->
              Libzipperposition.Index_intf.term Libzipperposition.Scoped.t ->
              (Libzipperposition.Index_intf.term * elt *
               Libzipperposition.Index_intf.subst)
              Sequence.t
            val fold_matched :
              ?subst:Libzipperposition.Index_intf.subst ->
              t Libzipperposition.Scoped.t ->
              Libzipperposition.Index_intf.term Libzipperposition.Scoped.t ->
              (Libzipperposition.Index_intf.term * elt *
               Libzipperposition.Index_intf.subst)
              Sequence.t
          end
        val name : string
        val empty : unit -> t
        val is_empty : t -> bool
        val size : t -> int
        val add : t -> Libzipperposition.Index_intf.term -> elt -> t
        val add_seq :
          t -> (Libzipperposition.Index_intf.term * elt) Sequence.t -> t
        val add_list :
          t -> (Libzipperposition.Index_intf.term * elt) list -> t
        val remove : t -> Libzipperposition.Index_intf.term -> elt -> t
        val iter :
          t -> (Libzipperposition.Index_intf.term -> elt -> unit) -> unit
        val fold :
          t ->
          ('a -> Libzipperposition.Index_intf.term -> elt -> 'a) -> 'a -> 'a
        val retrieve_unifiables :
          ?subst:Libzipperposition.Index_intf.subst ->
          t Libzipperposition.Scoped.t ->
          Libzipperposition.Index_intf.term Libzipperposition.Scoped.t ->
          (Libzipperposition.Index_intf.term * elt *
           Libzipperposition.Index_intf.subst)
          Sequence.t
        val retrieve_generalizations :
          ?subst:Libzipperposition.Index_intf.subst ->
          t Libzipperposition.Scoped.t ->
          Libzipperposition.Index_intf.term Libzipperposition.Scoped.t ->
          (Libzipperposition.Index_intf.term * elt *
           Libzipperposition.Index_intf.subst)
          Sequence.t
        val retrieve_specializations :
          ?subst:Libzipperposition.Index_intf.subst ->
          t Libzipperposition.Scoped.t ->
          Libzipperposition.Index_intf.term Libzipperposition.Scoped.t ->
          (Libzipperposition.Index_intf.term * elt *
           Libzipperposition.Index_intf.subst)
          Sequence.t
        val to_dot : elt CCFormat.printer -> t CCFormat.printer
      end
    module UnitIndex :
      sig
        type t
        module E :
          sig
            type t =
                Libzipperposition.FOTerm.t * Libzipperposition.FOTerm.t *
                bool * C.t
            type rhs = Libzipperposition.FOTerm.t
            val compare : t -> t -> int
            val extract : t -> Libzipperposition.Index_intf.term * rhs * bool
            val priority : t -> int
          end
        type rhs = E.rhs
        val empty : unit -> t
        val is_empty : t -> bool
        val add : t -> E.t -> t
        val add_seq : t -> E.t Sequence.t -> t
        val add_list : t -> E.t list -> t
        val remove : t -> E.t -> t
        val remove_seq : t -> E.t Sequence.t -> t
        val size : t -> int
        val iter :
          t -> (Libzipperposition.Index_intf.term -> E.t -> unit) -> unit
        val retrieve :
          ?subst:Libzipperposition.Index_intf.subst ->
          sign:bool ->
          t Libzipperposition.Scoped.t ->
          Libzipperposition.Index_intf.term Libzipperposition.Scoped.t ->
          (Libzipperposition.Index_intf.term * rhs * E.t *
           Libzipperposition.Index_intf.subst)
          Sequence.t
        val to_dot : t CCFormat.printer
      end
    module SubsumptionIndex :
      sig
        type t
        module C :
          sig
            type t = C.t
            val compare : t -> t -> int
            val to_lits : t -> Libzipperposition.Index_intf.lits
          end
        val name : string
        val empty : unit -> t
        val add : t -> C.t -> t
        val add_seq : t -> C.t Sequence.t -> t
        val add_list : t -> C.t list -> t
        val remove : t -> C.t -> t
        val remove_seq : t -> C.t Sequence.t -> t
        val retrieve_subsuming :
          t -> Libzipperposition.Index_intf.lits -> C.t Sequence.t
        val retrieve_subsuming_c : t -> C.t -> C.t Sequence.t
        val retrieve_subsumed :
          t -> Libzipperposition.Index_intf.lits -> C.t Sequence.t
        val retrieve_subsumed_c : t -> C.t -> C.t Sequence.t
        val iter : t -> C.t Sequence.t
        val fold : ('a -> C.t -> 'a) -> 'a -> t -> 'a
      end
    module type CLAUSE_SET =
      sig
        val on_add_clause : C.t Signal.t
        val on_remove_clause : C.t Signal.t
        val add : C.t Sequence.t -> unit
        val remove : C.t Sequence.t -> unit
      end
    module ActiveSet :
      sig
        val on_add_clause : C.t Signal.t
        val on_remove_clause : C.t Signal.t
        val add : C.t Sequence.t -> unit
        val remove : C.t Sequence.t -> unit
        val clauses : unit -> C.ClauseSet.t
        val num_clauses : unit -> int
      end
    module SimplSet : CLAUSE_SET
    module PassiveSet :
      sig
        val on_add_clause : C.t Signal.t
        val on_remove_clause : C.t Signal.t
        val add : C.t Sequence.t -> unit
        val remove : C.t Sequence.t -> unit
        val clauses : unit -> C.ClauseSet.t
        val queue : unit -> CQueue.t
        val next : unit -> C.t option
        val num_clauses : unit -> int
      end
    type stats = int * int * int
    val stats : unit -> stats
    val pp : unit CCFormat.printer
    val debug : unit CCFormat.printer
  end