sig
  type scope = LogtkSubsts.scope
  type term = LogtkFOTerm.t
  type subst = LogtkSubsts.t
  module type LEAF =
    sig
      type t
      type elt
      val empty : LogtkIndex.LEAF.t
      val add :
        LogtkIndex.LEAF.t ->
        LogtkIndex.term -> LogtkIndex.LEAF.elt -> LogtkIndex.LEAF.t
      val remove :
        LogtkIndex.LEAF.t ->
        LogtkIndex.term -> LogtkIndex.LEAF.elt -> LogtkIndex.LEAF.t
      val is_empty : LogtkIndex.LEAF.t -> bool
      val iter :
        LogtkIndex.LEAF.t ->
        (LogtkIndex.term -> LogtkIndex.LEAF.elt -> unit) -> unit
      val fold :
        LogtkIndex.LEAF.t ->
        '-> ('-> LogtkIndex.term -> LogtkIndex.LEAF.elt -> 'a) -> 'a
      val size : LogtkIndex.LEAF.t -> int
      val fold_unify :
        ?subst:LogtkIndex.subst ->
        LogtkIndex.LEAF.t ->
        LogtkIndex.scope ->
        LogtkIndex.term ->
        LogtkIndex.scope ->
        '->
        ('->
         LogtkIndex.term -> LogtkIndex.LEAF.elt -> LogtkIndex.subst -> 'a) ->
        'a
      val fold_match :
        ?allow_open:bool ->
        ?subst:LogtkIndex.subst ->
        LogtkIndex.LEAF.t ->
        LogtkIndex.scope ->
        LogtkIndex.term ->
        LogtkIndex.scope ->
        '->
        ('->
         LogtkIndex.term -> LogtkIndex.LEAF.elt -> LogtkIndex.subst -> 'a) ->
        'a
      val fold_matched :
        ?allow_open:bool ->
        ?subst:LogtkIndex.subst ->
        LogtkIndex.LEAF.t ->
        LogtkIndex.scope ->
        LogtkIndex.term ->
        LogtkIndex.scope ->
        '->
        ('->
         LogtkIndex.term -> LogtkIndex.LEAF.elt -> LogtkIndex.subst -> 'a) ->
        'a
    end
  module MakeLeaf :
    functor (X : Set.OrderedType->
      sig
        type t
        type elt = X.t
        val empty : t
        val add : t -> term -> elt -> t
        val remove : t -> term -> elt -> t
        val is_empty : t -> bool
        val iter : t -> (term -> elt -> unit) -> unit
        val fold : t -> '-> ('-> term -> elt -> 'a) -> 'a
        val size : t -> int
        val fold_unify :
          ?subst:subst ->
          t ->
          scope ->
          term -> scope -> '-> ('-> term -> elt -> subst -> 'a) -> 'a
        val fold_match :
          ?allow_open:bool ->
          ?subst:subst ->
          t ->
          scope ->
          term -> scope -> '-> ('-> term -> elt -> subst -> 'a) -> 'a
        val fold_matched :
          ?allow_open:bool ->
          ?subst:subst ->
          t ->
          scope ->
          term -> scope -> '-> ('-> term -> elt -> subst -> 'a) -> 'a
      end
  module type TERM_IDX =
    sig
      type t
      type elt
      module Leaf :
        sig
          type t
          type elt = elt
          val empty : t
          val add : t -> term -> elt -> t
          val remove : t -> term -> elt -> t
          val is_empty : t -> bool
          val iter : t -> (term -> elt -> unit) -> unit
          val fold : t -> '-> ('-> term -> elt -> 'a) -> 'a
          val size : t -> int
          val fold_unify :
            ?subst:subst ->
            t ->
            scope ->
            term -> scope -> '-> ('-> term -> elt -> subst -> 'a) -> 'a
          val fold_match :
            ?allow_open:bool ->
            ?subst:subst ->
            t ->
            scope ->
            term -> scope -> '-> ('-> term -> elt -> subst -> 'a) -> 'a
          val fold_matched :
            ?allow_open:bool ->
            ?subst:subst ->
            t ->
            scope ->
            term -> scope -> '-> ('-> term -> elt -> subst -> 'a) -> 'a
        end
      val name : string
      val empty : unit -> LogtkIndex.TERM_IDX.t
      val is_empty : LogtkIndex.TERM_IDX.t -> bool
      val size : LogtkIndex.TERM_IDX.t -> int
      val add :
        LogtkIndex.TERM_IDX.t ->
        LogtkIndex.term -> LogtkIndex.TERM_IDX.elt -> LogtkIndex.TERM_IDX.t
      val remove :
        LogtkIndex.TERM_IDX.t ->
        LogtkIndex.term -> LogtkIndex.TERM_IDX.elt -> LogtkIndex.TERM_IDX.t
      val iter :
        LogtkIndex.TERM_IDX.t ->
        (LogtkIndex.term -> LogtkIndex.TERM_IDX.elt -> unit) -> unit
      val fold :
        LogtkIndex.TERM_IDX.t ->
        ('-> LogtkIndex.term -> LogtkIndex.TERM_IDX.elt -> 'a) -> '-> 'a
      val retrieve_unifiables :
        ?subst:LogtkIndex.subst ->
        LogtkIndex.TERM_IDX.t ->
        LogtkIndex.scope ->
        LogtkIndex.term ->
        LogtkIndex.scope ->
        '->
        ('->
         LogtkIndex.term -> LogtkIndex.TERM_IDX.elt -> LogtkIndex.subst -> 'a) ->
        'a
      val retrieve_generalizations :
        ?allow_open:bool ->
        ?subst:LogtkIndex.subst ->
        LogtkIndex.TERM_IDX.t ->
        LogtkIndex.scope ->
        LogtkIndex.term ->
        LogtkIndex.scope ->
        '->
        ('->
         LogtkIndex.term -> LogtkIndex.TERM_IDX.elt -> LogtkIndex.subst -> 'a) ->
        'a
      val retrieve_specializations :
        ?allow_open:bool ->
        ?subst:LogtkIndex.subst ->
        LogtkIndex.TERM_IDX.t ->
        LogtkIndex.scope ->
        LogtkIndex.term ->
        LogtkIndex.scope ->
        '->
        ('->
         LogtkIndex.term -> LogtkIndex.TERM_IDX.elt -> LogtkIndex.subst -> 'a) ->
        'a
      val to_dot :
        (Buffer.t -> LogtkIndex.TERM_IDX.elt -> unit) ->
        Buffer.t -> LogtkIndex.TERM_IDX.t -> unit
    end
  type lits = (bool * LogtkIndex.term Sequence.t) Sequence.t
  module type CLAUSE =
    sig
      type t
      val cmp : LogtkIndex.CLAUSE.t -> LogtkIndex.CLAUSE.t -> int
      val to_lits : LogtkIndex.CLAUSE.t -> LogtkIndex.lits
    end
  module type SUBSUMPTION_IDX =
    sig
      type t
      module C : CLAUSE
      val name : string
      val empty : unit -> LogtkIndex.SUBSUMPTION_IDX.t
      val add :
        LogtkIndex.SUBSUMPTION_IDX.t -> C.t -> LogtkIndex.SUBSUMPTION_IDX.t
      val add_seq :
        LogtkIndex.SUBSUMPTION_IDX.t ->
        C.t Sequence.t -> LogtkIndex.SUBSUMPTION_IDX.t
      val remove :
        LogtkIndex.SUBSUMPTION_IDX.t -> C.t -> LogtkIndex.SUBSUMPTION_IDX.t
      val remove_seq :
        LogtkIndex.SUBSUMPTION_IDX.t ->
        C.t Sequence.t -> LogtkIndex.SUBSUMPTION_IDX.t
      val retrieve_subsuming :
        LogtkIndex.SUBSUMPTION_IDX.t ->
        LogtkIndex.lits -> '-> ('-> C.t -> 'a) -> 'a
      val retrieve_subsuming_c :
        LogtkIndex.SUBSUMPTION_IDX.t -> C.t -> '-> ('-> C.t -> 'a) -> 'a
      val retrieve_subsumed :
        LogtkIndex.SUBSUMPTION_IDX.t ->
        LogtkIndex.lits -> '-> ('-> C.t -> 'a) -> 'a
      val retrieve_subsumed_c :
        LogtkIndex.SUBSUMPTION_IDX.t -> C.t -> '-> ('-> C.t -> 'a) -> 'a
      val iter : LogtkIndex.SUBSUMPTION_IDX.t -> (C.t -> unit) -> unit
      val fold :
        ('-> C.t -> 'a) -> '-> LogtkIndex.SUBSUMPTION_IDX.t -> 'a
    end
  module type EQUATION =
    sig
      type t
      type rhs
      val compare : LogtkIndex.EQUATION.t -> LogtkIndex.EQUATION.t -> int
      val extract :
        LogtkIndex.EQUATION.t ->
        LogtkIndex.term * LogtkIndex.EQUATION.rhs * bool
      val priority : LogtkIndex.EQUATION.t -> int
    end
  module BasicEquation :
    sig
      type t = LogtkFOTerm.t * LogtkFOTerm.t
      type rhs = LogtkFOTerm.t
      val compare : t -> t -> int
      val extract : t -> term * rhs * bool
      val priority : t -> int
    end
  module type UNIT_IDX =
    sig
      type t
      module E : EQUATION
      type rhs = E.rhs
      val empty : unit -> LogtkIndex.UNIT_IDX.t
      val is_empty : LogtkIndex.UNIT_IDX.t -> bool
      val add : LogtkIndex.UNIT_IDX.t -> E.t -> LogtkIndex.UNIT_IDX.t
      val add_seq :
        LogtkIndex.UNIT_IDX.t -> E.t Sequence.t -> LogtkIndex.UNIT_IDX.t
      val remove : LogtkIndex.UNIT_IDX.t -> E.t -> LogtkIndex.UNIT_IDX.t
      val remove_seq :
        LogtkIndex.UNIT_IDX.t -> E.t Sequence.t -> LogtkIndex.UNIT_IDX.t
      val size : LogtkIndex.UNIT_IDX.t -> int
      val iter :
        LogtkIndex.UNIT_IDX.t -> (LogtkIndex.term -> E.t -> unit) -> unit
      val retrieve :
        ?allow_open:bool ->
        ?subst:LogtkIndex.subst ->
        sign:bool ->
        LogtkIndex.UNIT_IDX.t ->
        LogtkIndex.scope ->
        LogtkIndex.term ->
        LogtkIndex.scope ->
        '->
        ('->
         LogtkIndex.term ->
         LogtkIndex.UNIT_IDX.rhs -> E.t -> LogtkIndex.subst -> 'a) ->
        'a
      val to_dot : Buffer.t -> LogtkIndex.UNIT_IDX.t -> unit
    end
end