sig
  type t = Clause.disjunction * Jst.t
  and disjunction
  val unsat : Jst.t -> Clause.t
  val is_unsat : Clause.t -> bool
  val of_list : Atom.t list * Jst.t -> Clause.t
  val singleton : Fact.t -> Clause.t
  val pp : Clause.t Pretty.printer
  val eq : Clause.t -> Clause.t -> bool
  val d_singleton : Clause.t -> Fact.t
end