sig
  val sigma : Sym.t -> Term.t list -> Term.t
  val solve : Th.t -> Term.Equal.t -> Term.Subst.t
  module E :
    sig
      type t
      val u_of : Combine.E.t -> U.S.t
      val la_of : Combine.E.t -> La.S.t
      val nl_of : Combine.E.t -> Solution.Set.t
      val p_of : Combine.E.t -> Solution.Set.t
      val cop_of : Combine.E.t -> Solution.Set.t
      val cl_of : Combine.E.t -> Solution.Set.t
      val arr_of : Combine.E.t -> Solution.Set.t
      val set_of : Combine.E.t -> Solution.Set.t
      val empty : Combine.E.t
      val copy : Combine.E.t -> Combine.E.t
      val is_empty : Combine.E.t -> bool
      val eq : Combine.E.t -> Combine.E.t -> bool
      val pp : Combine.E.t Pretty.printer
      val pp_i : Th.t -> Combine.E.t Pretty.printer
      val find : Combine.E.t * Partition.t -> Th.t -> Jst.Eqtrans.t
      val inv : Combine.E.t * Partition.t -> Jst.Eqtrans.t
      val dep : Th.t -> Combine.E.t -> Term.t -> Term.Var.Set.t
      val diff : Combine.E.t -> Combine.E.t -> Combine.E.t
    end
  type t = Combine.E.t Infsys.Config.t
  val process :
    Fact.t -> Combine.E.t * Partition.t -> Combine.E.t * Partition.t
  val is_sat :
    Combine.E.t * Partition.t -> (Combine.E.t * Partition.t) option
  val dom : Combine.E.t * Partition.t -> Term.t -> Dom.t * Jst.t
  val can : Combine.E.t * Partition.t -> Jst.Eqtrans.t
  val simplify : Combine.E.t * Partition.t -> Atom.t -> Atom.t * Jst.t
  val cheap : bool Pervasives.ref
  val gc : Combine.t -> unit
  val maximize : Combine.E.t * Partition.t -> Jst.Eqtrans.t
  val minimize : Combine.E.t * Partition.t -> Jst.Eqtrans.t
  val model : Combine.E.t * Partition.t -> Term.t list -> Term.t Term.Map.t
end