sig
  type spec = AC_intf.spec
  module type S = AC_intf.S
  module Make :
    functor (Env : Env.S) ->
      sig
        module Env :
          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 = Env.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 Env.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 = Env.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 =
                      Env.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 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 = Env.ProofState.CQueue.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 = Env.ProofState.TermIndex.t
                    type elt = C.WithPos.t
                    module Leaf :
                      sig
                        type t = Env.ProofState.TermIndex.Leaf.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 = Env.ProofState.UnitIndex.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 = Env.ProofState.SubsumptionIndex.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 :
                  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 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 =
              'a Env.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
        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
        val on_add : AC_intf.spec Logtk.Signal.t
        val add :
          proof:Logtk.Proof.parent -> Logtk.ID.t -> Logtk.Type.t -> unit
        val is_ac : Logtk.ID.t -> bool
        val find_proof : Logtk.ID.t -> Logtk.Proof.parent
        val symbols : unit -> Logtk.ID.Set.t
        val symbols_of_terms : Logtk.Term.t Sequence.t -> Logtk.ID.Set.t
        val exists_ac : unit -> bool
        val scan_statement : Logtk.Statement.clause_t -> unit
        val is_trivial_lit : Logtk.Literal.t -> bool
        val is_trivial : C.t -> bool
        val simplify : Env.simplify_rule
        val setup : unit -> unit
      end
  val key_ac : (module AC.S) Logtk.Flex_state.key
  val extension : Extensions.t
end