sig
  type atom
  type t
  val f_true : Tseitin_intf.S.t
  val f_false : Tseitin_intf.S.t
  val make_atom : Tseitin_intf.S.atom -> Tseitin_intf.S.t
  val make_not : Tseitin_intf.S.t -> Tseitin_intf.S.t
  val make_and : Tseitin_intf.S.t list -> Tseitin_intf.S.t
  val make_or : Tseitin_intf.S.t list -> Tseitin_intf.S.t
  val make_xor : Tseitin_intf.S.t -> Tseitin_intf.S.t -> Tseitin_intf.S.t
  val make_imply : Tseitin_intf.S.t -> Tseitin_intf.S.t -> Tseitin_intf.S.t
  val make_equiv : Tseitin_intf.S.t -> Tseitin_intf.S.t -> Tseitin_intf.S.t
  val make_cnf : Tseitin_intf.S.t -> Tseitin_intf.S.atom list list
  val print : Format.formatter -> Tseitin_intf.S.t -> unit
end