sig
  type t
  type proof
  val equal : t -> t -> bool
  val hash : t -> int
  val print : Format.formatter -> t -> unit
  val dummy : t
  val neg : t -> t
  val norm : t -> t * Formula_intf.negated
  val make : int -> t
  val fresh : unit -> t
  val compare : t -> t -> int
  val sign : t -> bool
  val apply_sign : bool -> t -> t
  val set_sign : bool -> t -> t
end