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