sig
  type term = Term.term
  type literal = Term.literal
  type clause = Term.clause
  type binding = Subst.binding
  type subst = Subst.subst
  exception UNIFICATION_FAIL
  val is_term_generalization :
    ?p_preserving:bool -> Unification.term -> Unification.term -> bool
  val is_term_instance :
    ?p_preserving:bool -> Unification.term -> Unification.term -> bool
  val is_literal_instance :
    ?p_preserving:bool -> Unification.literal -> Unification.literal -> bool
  val match_terms :
    recompute:bool ->
    ?p_preserving:bool ->
    Unification.term -> int -> Unification.term -> int -> Unification.subst
  val match_literals :
    recompute:bool ->
    ?p_preserving:bool ->
    Unification.literal ->
    int -> Unification.literal -> int -> Unification.subst
  val are_terms_unifiable :
    ?p_preserving:bool -> Unification.term -> Unification.term -> bool
  val unify_terms :
    recompute:bool ->
    ?p_preserving:bool ->
    Unification.term -> int -> Unification.term -> int -> Unification.subst
  val unify_terms_ :
    recompute:bool ->
    ?p_preserving:bool ->
    Unification.subst ->
    Unification.term -> int -> Unification.term -> int -> Unification.subst
  val unify_literals :
    recompute:bool ->
    ?p_preserving:bool ->
    Unification.literal ->
    int -> Unification.literal -> int -> Unification.subst
  val unify_literals_ :
    recompute:bool ->
    ?p_preserving:bool ->
    Unification.subst ->
    Unification.literal ->
    int -> Unification.literal -> int -> Unification.subst
  val unify_constraints :
    recompute:bool ->
    ((Unification.literal * int) * (Unification.literal * int)) list ->
    Unification.subst
  val unify_constraints' :
    recompute:bool ->
    ((Unification.literal * int) * (Unification.literal * int)) list ->
    Subst.hash_subst
  val match_substs :
    recompute:bool ->
    ?p_preserving:bool ->
    int -> Unification.subst -> Unification.subst -> Unification.subst
  val unify_substs :
    recompute:bool ->
    ?p_preserving:bool ->
    Unification.subst -> Unification.subst -> Unification.subst
  val unify_substs_shallow : Unification.subst -> Unification.subst -> unit
  val merge_substs :
    Unification.subst -> Unification.subst -> Unification.subst
  val subsumes : Unification.clause -> Unification.clause -> bool
  val condense : Unification.clause -> Unification.clause
end