sig
  type 'a printer = Format.formatter -> 'a -> unit
  type 'a lit = Eq of 'a * 'a * bool | Prop of 'a * bool | Bool of bool
  val fmap_lit : ('a -> 'b) -> 'a Encoding.lit -> 'b Encoding.lit
  type 'a clause = 'a Encoding.lit list
  val fmap_clause : ('a -> 'b) -> 'a Encoding.clause -> 'b Encoding.clause
  type foterm = Libzipperposition.FOTerm.t
  type hoterm = Libzipperposition.TypedSTerm.t
  type foclause = Encoding.foterm Encoding.clause
  type hoclause = Encoding.hoterm Encoding.clause
  val foclause_of_clause :
    Libzipperposition.FOTerm.t Libzipperposition.SLiteral.t list ->
    Encoding.foclause
  val clause_of_foclause :
    Encoding.foclause ->
    Libzipperposition.FOTerm.t Libzipperposition.SLiteral.t list
  val pp_clause : 'a Encoding.printer -> 'a Encoding.clause Encoding.printer
  class type ['a, 'b] t =
    object method decode : 'b -> 'a option method encode : 'a -> 'b end
  val id : ('a, 'a) Encoding.t
  val compose :
    ('a, 'b) Encoding.t -> ('b, 'c) Encoding.t -> ('a, 'c) Encoding.t
  val ( >>> ) :
    ('a, 'b) Encoding.t -> ('b, 'c) Encoding.t -> ('a, 'c) Encoding.t
  val currying :
    (Encoding.foterm Encoding.clause, Encoding.hoterm Encoding.clause)
    Encoding.t
  module EncodedClause :
    sig
      type t = private Reasoner.term
      val pp : t CCFormat.printer
      val to_string : t -> string
      val equal : t -> t -> bool
      val hash_fun : t -> CCHash.state -> CCHash.state
      val hash : t -> int
      val compare : t -> t -> int
      val __magic : Encoding.hoterm -> Encoding.EncodedClause.t
    end
  val clause_prop : (Encoding.hoclause, Encoding.EncodedClause.t) Encoding.t
end