sig
  module type S = ProofState_intf.S
  module Make :
    functor (C : Clause.S) ->
      sig
        module Ctx :
          sig
            val ord : unit -> Logtk.Ordering.t
            val selection_fun : unit -> Selection.t
            val set_selection_fun : Selection.t -> unit
            val set_ord : Logtk.Ordering.t -> unit
            val signature : unit -> Logtk.Signature.t
            val renaming : Logtk.Subst.Renaming.t
            val compare : Logtk.Term.t -> Logtk.Term.t -> Logtk.Comparison.t
            val select : Selection.t
            val lost_completeness : unit -> unit
            val is_completeness_preserved : unit -> bool
            val add_signature : Logtk.Signature.t -> unit
            val find_signature : Logtk.ID.t -> Logtk.Type.t option
            val find_signature_exn : Logtk.ID.t -> Logtk.Type.t
            val declare : Logtk.ID.t -> Logtk.Type.t -> unit
            val on_new_symbol : (Logtk.ID.t * Logtk.Type.t) Logtk.Signal.t
            val on_signature_update : Logtk.Signature.t Logtk.Signal.t
            module Lit :
              sig
                val from_hooks : unit -> Logtk.Literal.Conv.hook_from list
                val add_from_hook : Logtk.Literal.Conv.hook_from -> unit
                val to_hooks : unit -> Logtk.Literal.Conv.hook_to list
                val add_to_hook : Logtk.Literal.Conv.hook_to -> unit
                val of_form :
                  Logtk.Term.t Logtk.SLiteral.t -> Logtk.Literal.t
                val to_form :
                  Logtk.Literal.t -> Logtk.Term.t Logtk.SLiteral.t
              end
          end
        module C :
          sig
            module Ctx :
              sig
                val ord : unit -> Logtk.Ordering.t
                val selection_fun : unit -> Selection.t
                val set_selection_fun : Selection.t -> unit
                val set_ord : Logtk.Ordering.t -> unit
                val signature : unit -> Logtk.Signature.t
                val renaming : Logtk.Subst.Renaming.t
                val compare :
                  Logtk.Term.t -> Logtk.Term.t -> Logtk.Comparison.t
                val select : Selection.t
                val lost_completeness : unit -> unit
                val is_completeness_preserved : unit -> bool
                val add_signature : Logtk.Signature.t -> unit
                val find_signature : Logtk.ID.t -> Logtk.Type.t option
                val find_signature_exn : Logtk.ID.t -> Logtk.Type.t
                val declare : Logtk.ID.t -> Logtk.Type.t -> unit
                val on_new_symbol :
                  (Logtk.ID.t * Logtk.Type.t) Logtk.Signal.t
                val on_signature_update : Logtk.Signature.t Logtk.Signal.t
                module Lit :
                  sig
                    val from_hooks :
                      unit -> Logtk.Literal.Conv.hook_from list
                    val add_from_hook : Logtk.Literal.Conv.hook_from -> unit
                    val to_hooks : unit -> Logtk.Literal.Conv.hook_to list
                    val add_to_hook : Logtk.Literal.Conv.hook_to -> unit
                    val of_form :
                      Logtk.Term.t Logtk.SLiteral.t -> Logtk.Literal.t
                    val to_form :
                      Logtk.Literal.t -> Logtk.Term.t Logtk.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 : t -> int
            val compare : t -> t -> int
            val id : t -> int
            val lits : t -> Logtk.Literal.t array
            val is_ground : t -> bool
            val weight : t -> int
            module Tbl :
              sig
                type key = t
                type 'a t = 'a C.Tbl.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 filter_map_inplace :
                  (key -> 'a -> 'a option) -> '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 -> default:'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 get_or_add : 'a t -> f:(key -> 'a) -> k:key -> 'a
                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 comes_from_goal : t -> bool
            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 :
              penalty:int ->
              trail:Trail.t ->
              Logtk.Literal.t list -> Clause_intf.proof_step -> t
            val create_a :
              penalty:int ->
              trail:Trail.t ->
              Logtk.Literal.t array -> Clause_intf.proof_step -> t
            val of_sclause :
              ?penalty:int -> SClause.t -> Clause_intf.proof_step -> t
            val of_forms :
              ?penalty:int ->
              trail:Trail.t ->
              Logtk.Term.t Logtk.SLiteral.t list ->
              Clause_intf.proof_step -> t
            val of_forms_axiom :
              ?penalty:int ->
              file:string ->
              name:string -> Logtk.Term.t Logtk.SLiteral.t list -> t
            val of_statement : Logtk.Statement.clause_t -> t list
            val proof_step : t -> Clause_intf.proof_step
            val proof : t -> Clause_intf.proof
            val proof_parent : t -> Logtk.Proof.Parent.t
            val proof_parent_subst :
              Logtk.Subst.Renaming.t ->
              t Logtk.Scoped.t -> Logtk.Subst.t -> Logtk.Proof.Parent.t
            val update_proof :
              t -> (Clause_intf.proof_step -> Clause_intf.proof_step) -> t
            val is_empty : t -> bool
            val length : t -> int
            val maxlits : t Logtk.Scoped.t -> Logtk.Subst.t -> CCBV.t
            val is_maxlit :
              t Logtk.Scoped.t -> Logtk.Subst.t -> idx:int -> bool
            val eligible_res : t Logtk.Scoped.t -> Logtk.Subst.t -> CCBV.t
            val eligible_res_no_subst : t -> CCBV.t
            val eligible_param : t Logtk.Scoped.t -> Logtk.Subst.t -> CCBV.t
            val is_eligible_param :
              t Logtk.Scoped.t -> Logtk.Subst.t -> idx:int -> bool
            val has_selected_lits : t -> bool
            val is_selected : t -> int -> bool
            val selected_lits : t -> (Logtk.Literal.t * int) list
            val penalty : t -> int
            val is_unit_clause : t -> bool
            val is_oriented_rule : t -> bool
            val symbols :
              ?init:Logtk.ID.Set.t -> t Sequence.t -> Logtk.ID.Set.t
            val to_sclause : t -> SClause.t
            val to_forms : t -> Logtk.Term.t Logtk.SLiteral.t list
            val to_s_form : t -> Logtk.TypedSTerm.Form.t
            module Seq :
              sig
                val lits : t -> Logtk.Literal.t Sequence.t
                val terms : t -> Logtk.Term.t Sequence.t
                val vars : t -> Logtk.Type.t Logtk.HVar.t Sequence.t
              end
            module Eligible :
              sig
                type t = int -> Logtk.Literal.t -> bool
                val res : clause -> t
                val param : clause -> t
                val eq : t
                val arith : t
                val filter : (Logtk.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 map : (elt -> elt) -> t -> t
                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
              end
            module Pos :
              sig val at : t -> Logtk.Position.t -> Logtk.Term.t end
            module WithPos :
              sig
                type t =
                  C.WithPos.t = {
                  clause : clause;
                  pos : Logtk.Position.t;
                  term : Logtk.Term.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 -> Logtk.Ordering.t
                    val selection_fun : unit -> Selection.t
                    val set_selection_fun : Selection.t -> unit
                    val set_ord : Logtk.Ordering.t -> unit
                    val signature : unit -> Logtk.Signature.t
                    val renaming : Logtk.Subst.Renaming.t
                    val compare :
                      Logtk.Term.t -> Logtk.Term.t -> Logtk.Comparison.t
                    val select : Selection.t
                    val lost_completeness : unit -> unit
                    val is_completeness_preserved : unit -> bool
                    val add_signature : Logtk.Signature.t -> unit
                    val find_signature : Logtk.ID.t -> Logtk.Type.t option
                    val find_signature_exn : Logtk.ID.t -> Logtk.Type.t
                    val declare : Logtk.ID.t -> Logtk.Type.t -> unit
                    val on_new_symbol :
                      (Logtk.ID.t * Logtk.Type.t) Logtk.Signal.t
                    val on_signature_update :
                      Logtk.Signature.t Logtk.Signal.t
                    module Lit :
                      sig
                        val from_hooks :
                          unit -> Logtk.Literal.Conv.hook_from list
                        val add_from_hook :
                          Logtk.Literal.Conv.hook_from -> unit
                        val to_hooks :
                          unit -> Logtk.Literal.Conv.hook_to list
                        val add_to_hook : Logtk.Literal.Conv.hook_to -> unit
                        val of_form :
                          Logtk.Term.t Logtk.SLiteral.t -> Logtk.Literal.t
                        val to_form :
                          Logtk.Literal.t -> Logtk.Term.t Logtk.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 : t -> int
                val compare : t -> t -> int
                val id : t -> int
                val lits : t -> Logtk.Literal.t array
                val is_ground : t -> bool
                val weight : t -> int
                module Tbl :
                  sig
                    type key = t
                    type 'a t = 'a C.Tbl.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 filter_map_inplace :
                      (key -> 'a -> 'a option) -> '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 -> default:'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 get_or_add : 'a t -> f:(key -> 'a) -> k:key -> 'a
                    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 comes_from_goal : t -> bool
                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 :
                  penalty:int ->
                  trail:Trail.t ->
                  Logtk.Literal.t list -> Clause_intf.proof_step -> t
                val create_a :
                  penalty:int ->
                  trail:Trail.t ->
                  Logtk.Literal.t array -> Clause_intf.proof_step -> t
                val of_sclause :
                  ?penalty:int -> SClause.t -> Clause_intf.proof_step -> t
                val of_forms :
                  ?penalty:int ->
                  trail:Trail.t ->
                  Logtk.Term.t Logtk.SLiteral.t list ->
                  Clause_intf.proof_step -> t
                val of_forms_axiom :
                  ?penalty:int ->
                  file:string ->
                  name:string -> Logtk.Term.t Logtk.SLiteral.t list -> t
                val of_statement : Logtk.Statement.clause_t -> t list
                val proof_step : t -> Clause_intf.proof_step
                val proof : t -> Clause_intf.proof
                val proof_parent : t -> Logtk.Proof.Parent.t
                val proof_parent_subst :
                  Logtk.Subst.Renaming.t ->
                  t Logtk.Scoped.t -> Logtk.Subst.t -> Logtk.Proof.Parent.t
                val update_proof :
                  t ->
                  (Clause_intf.proof_step -> Clause_intf.proof_step) -> t
                val is_empty : t -> bool
                val length : t -> int
                val maxlits : t Logtk.Scoped.t -> Logtk.Subst.t -> CCBV.t
                val is_maxlit :
                  t Logtk.Scoped.t -> Logtk.Subst.t -> idx:int -> bool
                val eligible_res :
                  t Logtk.Scoped.t -> Logtk.Subst.t -> CCBV.t
                val eligible_res_no_subst : t -> CCBV.t
                val eligible_param :
                  t Logtk.Scoped.t -> Logtk.Subst.t -> CCBV.t
                val is_eligible_param :
                  t Logtk.Scoped.t -> Logtk.Subst.t -> idx:int -> bool
                val has_selected_lits : t -> bool
                val is_selected : t -> int -> bool
                val selected_lits : t -> (Logtk.Literal.t * int) list
                val penalty : t -> int
                val is_unit_clause : t -> bool
                val is_oriented_rule : t -> bool
                val symbols :
                  ?init:Logtk.ID.Set.t -> t Sequence.t -> Logtk.ID.Set.t
                val to_sclause : t -> SClause.t
                val to_forms : t -> Logtk.Term.t Logtk.SLiteral.t list
                val to_s_form : t -> Logtk.TypedSTerm.Form.t
                module Seq :
                  sig
                    val lits : t -> Logtk.Literal.t Sequence.t
                    val terms : t -> Logtk.Term.t Sequence.t
                    val vars : t -> Logtk.Type.t Logtk.HVar.t Sequence.t
                  end
                module Eligible :
                  sig
                    type t = int -> Logtk.Literal.t -> bool
                    val res : clause -> t
                    val param : clause -> t
                    val eq : t
                    val arith : t
                    val filter : (Logtk.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 map : (elt -> elt) -> t -> t
                    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
                  end
                module Pos :
                  sig val at : t -> Logtk.Position.t -> Logtk.Term.t end
                module WithPos :
                  sig
                    type t =
                      C.WithPos.t = {
                      clause : clause;
                      pos : Logtk.Position.t;
                      term : Logtk.Term.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 penalty : 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 -> unit
            val add_seq : t -> C.t Sequence.t -> unit
            val length : t -> int
            val is_empty : t -> bool
            val take_first : t -> C.t
            val name : t -> string
            val make : ratio:int -> weight:(C.t -> int) -> string -> t
            val bfs : unit -> t
            val almost_bfs : unit -> t
            val explore : unit -> t
            val ground : unit -> t
            val goal_oriented : unit -> t
            val default : unit -> 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 -> Logtk.Index_intf.term -> elt -> t
                val remove : t -> Logtk.Index_intf.term -> elt -> t
                val is_empty : t -> bool
                val iter :
                  t -> (Logtk.Index_intf.term -> elt -> unit) -> unit
                val fold :
                  t -> 'a -> ('a -> Logtk.Index_intf.term -> elt -> 'a) -> 'a
                val size : t -> int
                val fold_unify :
                  ?subst:Logtk.Unif_subst.t ->
                  t Logtk.Scoped.t ->
                  Logtk.Index_intf.term Logtk.Scoped.t ->
                  (Logtk.Index_intf.term * elt * Logtk.Unif_subst.t)
                  Sequence.t
                val fold_match :
                  ?subst:Logtk.Index_intf.subst ->
                  t Logtk.Scoped.t ->
                  Logtk.Index_intf.term Logtk.Scoped.t ->
                  (Logtk.Index_intf.term * elt * Logtk.Index_intf.subst)
                  Sequence.t
                val fold_matched :
                  ?subst:Logtk.Index_intf.subst ->
                  t Logtk.Scoped.t ->
                  Logtk.Index_intf.term Logtk.Scoped.t ->
                  (Logtk.Index_intf.term * elt * Logtk.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 -> Logtk.Index_intf.term -> elt -> t
            val add_seq : t -> (Logtk.Index_intf.term * elt) Sequence.t -> t
            val add_list : t -> (Logtk.Index_intf.term * elt) list -> t
            val remove : t -> Logtk.Index_intf.term -> elt -> t
            val remove_seq :
              t -> (Logtk.Index_intf.term * elt) Sequence.t -> t
            val remove_list : t -> (Logtk.Index_intf.term * elt) list -> t
            val iter : t -> (Logtk.Index_intf.term -> elt -> unit) -> unit
            val fold :
              t -> ('a -> Logtk.Index_intf.term -> elt -> 'a) -> 'a -> 'a
            val retrieve_unifiables :
              ?subst:Logtk.Unif_subst.t ->
              t Logtk.Scoped.t ->
              Logtk.Index_intf.term Logtk.Scoped.t ->
              (Logtk.Index_intf.term * elt * Logtk.Unif_subst.t) Sequence.t
            val retrieve_generalizations :
              ?subst:Logtk.Index_intf.subst ->
              t Logtk.Scoped.t ->
              Logtk.Index_intf.term Logtk.Scoped.t ->
              (Logtk.Index_intf.term * elt * Logtk.Index_intf.subst)
              Sequence.t
            val retrieve_specializations :
              ?subst:Logtk.Index_intf.subst ->
              t Logtk.Scoped.t ->
              Logtk.Index_intf.term Logtk.Scoped.t ->
              (Logtk.Index_intf.term * elt * Logtk.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 = Logtk.Term.t * Logtk.Term.t * bool * C.t
                type rhs = Logtk.Term.t
                val compare : t -> t -> int
                val extract : t -> Logtk.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 -> (Logtk.Index_intf.term -> E.t -> unit) -> unit
            val retrieve :
              ?subst:Logtk.Index_intf.subst ->
              sign:bool ->
              t Logtk.Scoped.t ->
              Logtk.Index_intf.term Logtk.Scoped.t ->
              (Logtk.Index_intf.term * rhs * E.t * Logtk.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 -> Logtk.Index_intf.lits
                val labels : t -> Logtk.Index_intf.labels
              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 ->
              Logtk.Index_intf.lits ->
              Logtk.Index_intf.labels -> C.t Sequence.t
            val retrieve_subsuming_c : t -> C.t -> C.t Sequence.t
            val retrieve_subsumed :
              t ->
              Logtk.Index_intf.lits ->
              Logtk.Index_intf.labels -> C.t Sequence.t
            val retrieve_subsumed_c : t -> C.t -> C.t Sequence.t
            val retrieve_alpha_equiv :
              t ->
              Logtk.Index_intf.lits ->
              Logtk.Index_intf.labels -> C.t Sequence.t
            val retrieve_alpha_equiv_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 Logtk.Signal.t
            val on_remove_clause : C.t Logtk.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 Logtk.Signal.t
            val on_remove_clause : C.t Logtk.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 Logtk.Signal.t
            val on_remove_clause : C.t Logtk.Signal.t
            val add : C.t Sequence.t -> unit
            val remove : C.t Sequence.t -> unit
            val clauses : unit -> C.ClauseSet.t
            val queue : 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
end