sig
  type t = Atom.t * Jst.t
  val pp : Fact.t Pretty.printer
  val print_justification : bool Pervasives.ref
  val eq : Fact.t -> Fact.t -> bool
  val map : Jst.Eqtrans.t -> Fact.t -> Fact.t
  val replace : Term.t * Term.t * Jst.t -> Fact.t -> Fact.t
  module Equal :
    sig
      type t = Term.t * Term.t * Jst.t
      val lhs_of : Fact.Equal.t -> Term.t
      val rhs_of : Fact.Equal.t -> Term.t
      val pp : Fact.Equal.t Pretty.printer
      val make : Term.t -> Term.t -> Jst.t -> Fact.Equal.t
      val both_sides : (Term.t -> bool) -> Fact.Equal.t -> bool
      val is_var : Fact.Equal.t -> bool
      val is_pure : Th.t -> Fact.Equal.t -> bool
      val status : Fact.Equal.t -> Term.status
      val map2 :
        Jst.Eqtrans.t * Jst.Eqtrans.t -> Fact.Equal.t -> Fact.Equal.t
      val map : Jst.Eqtrans.t -> Fact.Equal.t -> Fact.Equal.t
      val map_lhs : Jst.Eqtrans.t -> Fact.Equal.t -> Fact.Equal.t
      val map_rhs : Jst.Eqtrans.t -> Fact.Equal.t -> Fact.Equal.t
    end
  module Diseq :
    sig
      type t = Term.t * Term.t * Jst.t
      val make : Term.t -> Term.t -> Jst.t -> Fact.Diseq.t
      val lhs_of : Fact.Diseq.t -> Term.t
      val rhs_of : Fact.Diseq.t -> Term.t
      val pp : Fact.Diseq.t Pretty.printer
      val map : Jst.Eqtrans.t -> Fact.Diseq.t -> Fact.Diseq.t
      val both_sides : (Term.t -> bool) -> Fact.Diseq.t -> bool
      val is_var : Fact.Diseq.t -> bool
      val is_pure : Th.t -> Fact.Diseq.t -> bool
      val status : Fact.Diseq.t -> Term.status
      module Set :
        sig
          type elt = t
          and t
          val empty : t
          val is_empty : t -> bool
          val mem : elt -> t -> bool
          val add : elt -> t -> t
          val singleton : elt -> t
          val remove : elt -> t -> t
          val union : t -> t -> t
          val inter : t -> t -> t
          val diff : t -> t -> t
          val compare : t -> t -> int
          val equal : t -> t -> bool
          val subset : t -> t -> bool
          val iter : (elt -> unit) -> t -> unit
          val fold : (elt -> 'a -> 'a) -> t -> 'a -> 'a
          val for_all : (elt -> bool) -> t -> bool
          val exists : (elt -> bool) -> t -> bool
          val filter : (elt -> bool) -> t -> t
          val partition : (elt -> bool) -> t -> t * t
          val cardinal : t -> int
          val elements : t -> elt list
          val min_elt : t -> elt
          val max_elt : t -> elt
          val choose : t -> elt
        end
    end
  module Nonneg :
    sig
      type t = Term.t * Jst.t
      val make : Term.t -> Jst.t -> Fact.Nonneg.t
      val term_of : Fact.Nonneg.t -> Term.t
      val pp : Fact.Nonneg.t Pretty.printer
      val map : Jst.Eqtrans.t -> Fact.Nonneg.t -> Fact.Nonneg.t
      val is_var : Fact.Nonneg.t -> bool
      val is_pure : Th.t -> Fact.Nonneg.t -> bool
      val status : Fact.Nonneg.t -> Term.status
    end
  module Pos :
    sig
      type t = Term.t * Jst.t
      val make : Term.t -> Jst.t -> Fact.Pos.t
      val term_of : Fact.Pos.t -> Term.t
      val pp : Fact.Pos.t Pretty.printer
      val map : Jst.Eqtrans.t -> Fact.Pos.t -> Fact.Pos.t
      val is_var : Fact.Pos.t -> bool
      val is_pure : Th.t -> Fact.Pos.t -> bool
      val status : Fact.Pos.t -> Term.status
    end
  val of_equal : Fact.Equal.t -> Fact.t
  val of_diseq : Fact.Diseq.t -> Fact.t
end