functor (X : ALIEN) ->
  sig
    type t = X.r abstract
    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