sig
  type t =
      True
    | False
    | Comp of Types.Term.t * Types.op_comp * Types.Term.t
    | Ite of Types.SAtom.t * Types.Atom.t * Types.Atom.t
  val compare : Types.Atom.t -> Types.Atom.t -> int
  val trivial_is_implied : Types.Atom.t -> Types.Atom.t -> int
  val neg : Types.Atom.t -> Types.Atom.t
  val hash : Types.Atom.t -> int
  val equal : Types.Atom.t -> Types.Atom.t -> bool
  val subst : Variable.subst -> Types.Atom.t -> Types.Atom.t
  val has_var : Variable.t -> Types.Atom.t -> bool
  val has_vars : Variable.t list -> Types.Atom.t -> bool
  val variables : Types.Atom.t -> Variable.Set.t
  val variables_proc : Types.Atom.t -> Variable.Set.t
  val print : Format.formatter -> Types.Atom.t -> unit
end