functor (X : Sig.X) ->
  sig
    type t
    module R :
      sig
        type r = X.r
        val make : Term.t -> r * Literal.LT.t list
        val type_info : r -> Ty.t
        val compare : r -> r -> int
        val equal : r -> r -> bool
        val hash : r -> int
        val leaves : r -> r list
        val subst : r -> r -> r -> r
        val solve : r -> r -> (r * r) list
        val term_embed : Term.t -> r
        val term_extract : r -> Term.t option
        val unsolvable : r -> bool
        val fully_interpreted : Symbols.t -> bool
        val print : Format.formatter -> r -> unit
        module Rel :
          sig
            type t = X.Rel.t
            type r = r
            val empty : unit -> t
            val assume : t -> r Sig.input list -> t * r Sig.result
            val query : t -> r Sig.input -> Sig.answer
            val case_split :
              t -> (r Literal.view * Explanation.t * Num.num) list
            val add : t -> r -> t
          end
      end
    val empty : t
    val add : t -> Term.t -> t * Literal.LT.t list
    val mem : t -> Term.t -> bool
    val find : t -> Term.t -> R.r * Explanation.t
    val find_r : t -> R.r -> R.r * Explanation.t
    val union :
      t ->
      R.r ->
      R.r ->
      Explanation.t ->
      t * (R.r * (R.r * R.r * Explanation.t) list * R.r) list
    val distinct : t -> R.r list -> Explanation.t -> t
    val are_equal : t -> Term.t -> Term.t -> Sig.answer
    val are_distinct : t -> Term.t -> Term.t -> Sig.answer
    val already_distinct : t -> R.r list -> bool
    val class_of : t -> Term.t -> Term.t list
  end