sig
  module type S =
    sig
      type t
      module R : Sig.X
      val empty : Uf.S.t
      val add : Uf.S.t -> Term.t -> Uf.S.t * Literal.LT.t list
      val mem : Uf.S.t -> Term.t -> bool
      val find : Uf.S.t -> Term.t -> R.r * Explanation.t
      val find_r : Uf.S.t -> R.r -> R.r * Explanation.t
      val union :
        Uf.S.t ->
        R.r ->
        R.r ->
        Explanation.t ->
        Uf.S.t * (R.r * (R.r * R.r * Explanation.t) list * R.r) list
      val distinct : Uf.S.t -> R.r list -> Explanation.t -> Uf.S.t
      val are_equal : Uf.S.t -> Term.t -> Term.t -> Sig.answer
      val are_distinct : Uf.S.t -> Term.t -> Term.t -> Sig.answer
      val already_distinct : Uf.S.t -> R.r list -> bool
      val class_of : Uf.S.t -> Term.t -> Term.t list
    end
  module Make :
    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
end