functor
  (X : Sig.X) (P : sig
                     type r = X.r
                     type t
                     val compare : t -> t -> int
                     val hash : t -> int
                     val create : (Num.num * r) list -> Num.num -> Ty.t -> t
                     val add : t -> t -> t
                     val sub : t -> t -> t
                     val mult : t -> t -> t
                     val mult_const : Num.num -> t -> t
                     val div : t -> t -> t * bool
                     val modulo : t -> t -> t
                     val is_empty : t -> bool
                     val find : r -> t -> Num.num
                     val choose : t -> Num.num * r
                     val subst : r -> t -> t -> t
                     val remove : r -> t -> t
                     val to_list : t -> (Num.num * r) list * Num.num
                     val print : Format.formatter -> t -> unit
                     val type_info : t -> Ty.t
                     val is_monomial : t -> (Num.num * r * Num.num) option
                     val ppmc_denominators : t -> Num.num
                     val pgcd_numerators : t -> Num.num
                     val normal_form : t -> t * Num.num * Num.num
                     val normal_form_pos : t -> t * Num.num * Num.num
                   end) (C : sig
                               type t = P.t
                               type r = X.r
                               val extract : r -> t option
                               val embed : t -> r
                             end) ->
  sig
    type t = P.t
    type r = X.r
    val name : string
    val is_mine_symb : Symbols.t -> bool
    val unsolvable : t -> bool
    val make : Term.t -> r * Literal.LT.t list
    val term_extract : r -> Term.t option
    val type_info : t -> Ty.t
    val embed : r -> t
    val leaves : t -> r list
    val subst : r -> r -> t -> r
    val compare : t -> t -> int
    val hash : t -> int
    val solve : r -> r -> (r * r) list
    val print : Format.formatter -> t -> unit
    val fully_interpreted : Symbols.t -> bool
    module Rel :
      sig
        type 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