sig
  type term = Libzipperposition.FOTerm.t
  type t = Literal.t array
  val equal_com : Literals.t -> Literals.t -> bool
  val compare : Literals.t -> Literals.t -> int
  val equal : Literals.t -> Literals.t -> bool
  val hash_fun : t -> CCHash.state -> CCHash.state
  val hash : t -> int
  val variant :
    ?subst:Libzipperposition.Substs.t ->
    Literals.t Libzipperposition.Scoped.t ->
    Literals.t Libzipperposition.Scoped.t ->
    Libzipperposition.Substs.t Sequence.t
  val are_variant : Literals.t -> Literals.t -> bool
  val weight : Literals.t -> int
  val depth : Literals.t -> int
  val vars :
    Literals.t -> Libzipperposition.Type.t Libzipperposition.HVar.t list
  val is_ground : Literals.t -> bool
  val to_form : Literals.t -> Literals.term Libzipperposition.SLiteral.t list
  val apply_subst :
    renaming:Libzipperposition.Substs.Renaming.t ->
    Libzipperposition.Substs.t ->
    Literals.t Libzipperposition.Scoped.t -> Literals.t
  val map : (Literals.term -> Literals.term) -> Literals.t -> Literals.t
  val pos : Literals.t -> CCBV.t
  val neg : Literals.t -> CCBV.t
  val maxlits : ord:Libzipperposition.Ordering.t -> Literals.t -> CCBV.t
  val maxlits_l :
    ord:Libzipperposition.Ordering.t -> Literals.t -> (Literal.t * int) list
  val is_max : ord:Libzipperposition.Ordering.t -> Literals.t -> int -> bool
  val is_trivial : Literals.t -> bool
  val is_absurd : Literals.t -> bool
  module Seq :
    sig
      val vars :
        Literals.t ->
        Libzipperposition.Type.t Libzipperposition.HVar.t Sequence.t
      val terms : Literals.t -> Literals.term Sequence.t
      val to_form :
        Literals.t -> Literals.term Libzipperposition.SLiteral.t Sequence.t
    end
  module Pos :
    sig
      val at : Literals.t -> Libzipperposition.Position.t -> Literals.term
      val lit_at :
        Literals.t ->
        Libzipperposition.Position.t ->
        Literal.t * Libzipperposition.Position.t
      val replace :
        Literals.t ->
        at:Libzipperposition.Position.t -> by:Literals.term -> unit
      val idx : Libzipperposition.Position.t -> int
      val tail : Libzipperposition.Position.t -> Libzipperposition.Position.t
      val cut :
        Libzipperposition.Position.t -> int * Libzipperposition.Position.t
    end
  module Conv :
    sig
      val of_forms :
        ?hooks:Literal.Conv.hook_from list ->
        Literals.term Libzipperposition.SLiteral.t list -> Literals.t
      val to_forms :
        ?hooks:Literal.Conv.hook_to list ->
        Literals.t -> Literals.term Libzipperposition.SLiteral.t list
    end
  module View :
    sig
      val get_eqn :
        Literals.t ->
        Libzipperposition.Position.t ->
        (Literals.term * Literals.term * bool) option
      val get_arith :
        Literals.t -> Libzipperposition.Position.t -> ArithLit.Focus.t option
      val get_eqn_exn :
        Literals.t ->
        Libzipperposition.Position.t -> Literals.term * Literals.term * bool
      val get_arith_exn :
        Literals.t -> Libzipperposition.Position.t -> ArithLit.Focus.t
    end
  val fold_lits :
    eligible:(int -> Literal.t -> bool) ->
    Literals.t -> (Literal.t * int) Sequence.t
  val fold_eqn :
    ?both:bool ->
    ?sign:bool ->
    ord:Libzipperposition.Ordering.t ->
    eligible:(int -> Literal.t -> bool) ->
    Literals.t ->
    (Literals.term * Literals.term * bool * Libzipperposition.Position.t)
    Sequence.t
  val fold_arith :
    eligible:(int -> Literal.t -> bool) ->
    Literals.t -> (ArithLit.t * Libzipperposition.Position.t) Sequence.t
  val fold_arith_terms :
    eligible:(int -> Literal.t -> bool) ->
    which:[< `All | `Max ] ->
    ord:Libzipperposition.Ordering.t ->
    Literals.t ->
    (Literals.term * ArithLit.Focus.t * Libzipperposition.Position.t)
    Sequence.t
  val fold_terms :
    ?vars:bool ->
    ?ty_args:bool ->
    which:[< `All | `Max ] ->
    ord:Libzipperposition.Ordering.t ->
    subterms:bool ->
    eligible:(int -> Literal.t -> bool) ->
    Literals.t -> (Literals.term * Libzipperposition.Position.t) Sequence.t
  val symbols :
    ?init:Libzipperposition.ID.Set.t ->
    Literals.t -> Libzipperposition.ID.Set.t
  val pp : Literals.t CCFormat.printer
  val pp_tstp : Literals.t CCFormat.printer
  val to_string : Literals.t -> string
  val is_RR_horn_clause : Literals.t -> bool
  val is_horn : Literals.t -> bool
  val is_pos_eq : Literals.t -> (Literals.term * Literals.term) option
end