sig
  type form = TypedSTerm.t
  type term = TypedSTerm.t
  exception NotALit of SLiteral.form
  type 't t =
      True
    | False
    | Atom of 't * bool
    | Eq of 't * 't
    | Neq of 't * 't
  type 'a lit = 'a SLiteral.t
  val of_form : SLiteral.form -> SLiteral.term SLiteral.t
  val to_form : SLiteral.term SLiteral.t -> SLiteral.form
  val map : f:('a -> 'b) -> 'a SLiteral.t -> 'b SLiteral.t
  val fold : ('a -> 't -> 'a) -> 'a -> 't SLiteral.t -> 'a
  val iter : f:('a -> unit) -> 'a SLiteral.t -> unit
  val to_seq : 'a SLiteral.t -> 'a Sequence.t
  val equal : ('a -> 'a -> bool) -> 'a SLiteral.t -> 'a SLiteral.t -> bool
  val true_ : 'a SLiteral.t
  val false_ : 'a SLiteral.t
  val eq : 'a -> 'a -> 'a SLiteral.t
  val neq : 'a -> 'a -> 'a SLiteral.t
  val atom : 'a -> bool -> 'a SLiteral.t
  val is_true : 'a SLiteral.t -> bool
  val is_false : 'a SLiteral.t -> bool
  val sign : 'a SLiteral.t -> bool
  val is_pos : 'a SLiteral.t -> bool
  val is_neg : 'a SLiteral.t -> bool
  val negate : 'a SLiteral.t -> 'a SLiteral.t
  val pp : 'a CCFormat.printer -> 'a t CCFormat.printer
  val to_string : 'a CCFormat.printer -> 'a t -> string
  module TPTP :
    sig
      val pp : 'a CCFormat.printer -> 'a t CCFormat.printer
      val to_string : 'a CCFormat.printer -> 'a t -> string
    end
  module ZF :
    sig
      val pp : 'a CCFormat.printer -> 'a t CCFormat.printer
      val to_string : 'a CCFormat.printer -> 'a t -> string
    end
end