sig
  type r
  type th
  val extract : Sig.COMBINATOR.r -> Sig.COMBINATOR.th
  val make : Term.t -> Sig.COMBINATOR.r * Literal.LT.t list
  val type_info : Sig.COMBINATOR.r -> Ty.t
  val compare : Sig.COMBINATOR.r -> Sig.COMBINATOR.r -> int
  val leaves : Sig.COMBINATOR.r -> Sig.COMBINATOR.r list
  val subst :
    Sig.COMBINATOR.r ->
    Sig.COMBINATOR.r -> Sig.COMBINATOR.r -> Sig.COMBINATOR.r
  val solve :
    Sig.COMBINATOR.r ->
    Sig.COMBINATOR.r -> (Sig.COMBINATOR.r * Sig.COMBINATOR.r) list
  val empty_embedding : Term.t -> Sig.COMBINATOR.r
  val normal_form : Literal.LT.t -> Literal.LT.t
  val print : Format.formatter -> Sig.COMBINATOR.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