sig
  module type S = Env_intf.S
  type 'a packed = (module Env.S with type C.t = 'a)
  module Make :
    functor
      (X : sig
             module Ctx : Ctx.S
             val params : Params.t
             val flex_state : Logtk.Flex_state.t
           end) ->
      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
            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
                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
                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 = {
                  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 ProofState :
          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
        type inf_rule = C.t -> C.t list
        type generate_rule = full:bool -> unit -> C.t list
        type binary_inf_rule = inf_rule
        type unary_inf_rule = inf_rule
        type simplify_rule = C.t -> C.t SimplM.t
        type active_simplify_rule = simplify_rule
        type rw_simplify_rule = simplify_rule
        type backward_simplify_rule = C.t -> C.ClauseSet.t
        type redundant_rule = C.t -> bool
        type backward_redundant_rule = C.ClauseSet.t -> C.t -> C.ClauseSet.t
        type is_trivial_trail_rule = Trail.t -> bool
        type is_trivial_rule = C.t -> bool
        type term_rewrite_rule =
            Logtk.Term.t -> (Logtk.Term.t * Logtk.Proof.parent list) option
        type lit_rewrite_rule =
            Logtk.Literal.t ->
            (Logtk.Literal.t * Logtk.Proof.parent list * Logtk.Proof.tag list)
            option
        type multi_simpl_rule = C.t -> C.t list option
        type 'a conversion_result = CR_skip | CR_add of 'a | CR_return of 'a
        type clause_conversion_rule =
            Logtk.Statement.clause_t -> C.t list conversion_result
        val add_passive : C.t Sequence.t -> unit
        val add_active : C.t Sequence.t -> unit
        val add_simpl : C.t Sequence.t -> unit
        val remove_passive : C.t Sequence.t -> unit
        val remove_active : C.t Sequence.t -> unit
        val remove_simpl : C.t Sequence.t -> unit
        val get_passive : unit -> C.t Sequence.t
        val get_active : unit -> C.t Sequence.t
        val add_binary_inf : string -> binary_inf_rule -> unit
        val add_unary_inf : string -> unary_inf_rule -> unit
        val add_rw_simplify : rw_simplify_rule -> unit
        val add_active_simplify : active_simplify_rule -> unit
        val add_backward_simplify : backward_simplify_rule -> unit
        val add_redundant : redundant_rule -> unit
        val add_backward_redundant : backward_redundant_rule -> unit
        val add_basic_simplify : simplify_rule -> unit
        val add_unary_simplify : simplify_rule -> unit
        val add_multi_simpl_rule : multi_simpl_rule -> unit
        val add_is_trivial_trail : is_trivial_trail_rule -> unit
        val add_is_trivial : is_trivial_rule -> unit
        val add_rewrite_rule : string -> term_rewrite_rule -> unit
        val add_lit_rule : string -> lit_rewrite_rule -> unit
        val add_generate : string -> generate_rule -> unit
        val cr_skip : 'a conversion_result
        val cr_return : 'a -> 'a conversion_result
        val cr_add : 'a -> 'a conversion_result
        val add_clause_conversion : clause_conversion_rule -> unit
        val add_step_init : (unit -> unit) -> unit
        val multi_simplify : C.t -> C.t list option
        val params : Params.t
        val get_empty_clauses : unit -> C.ClauseSet.t
        val get_some_empty_clause : unit -> C.t option
        val has_empty_clause : unit -> bool
        val on_start : unit Logtk.Signal.t
        val on_input_statement : Logtk.Statement.clause_t Logtk.Signal.t
        val convert_input_statements :
          Logtk.Statement.clause_t CCVector.ro_vector -> C.t Clause.sets
        val on_empty_clause : C.t Logtk.Signal.t
        val ord : unit -> Logtk.Ordering.t
        val precedence : unit -> Logtk.Precedence.t
        val signature : unit -> Logtk.Signature.t
        val pp : unit CCFormat.printer
        val pp_full : unit CCFormat.printer
        type stats = int * int * int
        val stats : unit -> stats
        val next_passive : unit -> C.t option
        val do_binary_inferences : C.t -> C.t Sequence.t
        val do_unary_inferences : C.t -> C.t Sequence.t
        val do_generate : full:bool -> unit -> C.t Sequence.t
        val is_trivial_trail : Trail.t -> bool
        val is_trivial : C.t -> bool
        val is_active : C.t -> bool
        val is_passive : C.t -> bool
        val basic_simplify : simplify_rule
        val unary_simplify : simplify_rule
        val backward_simplify : C.t -> C.ClauseSet.t * C.t Sequence.t
        val simplify_active_with : (C.t -> C.t list option) -> unit
        val forward_simplify : simplify_rule
        val generate : C.t -> C.t Sequence.t
        val is_redundant : C.t -> bool
        val subsumed_by : C.t -> C.ClauseSet.t
        val all_simplify : C.t -> C.t list SimplM.t
        val step_init : unit -> unit
        val flex_state : unit -> Logtk.Flex_state.t
        val update_flex_state :
          (Logtk.Flex_state.t -> Logtk.Flex_state.t) -> unit
        val flex_add : 'a Logtk.Flex_state.key -> 'a -> unit
        val flex_get : 'a Logtk.Flex_state.key -> 'a
      end
end