sig
  type term = Libzipperposition.FOTerm.t
  type t = private
      True
    | False
    | Equation of Literal.term * Literal.term * bool
    | Prop of Literal.term * bool
    | Arith of ArithLit.t
  val equal_com : Literal.t -> Literal.t -> bool
  val compare : Literal.t -> Literal.t -> int
  val equal : Literal.t -> Literal.t -> bool
  val hash_fun : t -> CCHash.state -> CCHash.state
  val hash : Literal.t -> int
  val weight : Literal.t -> int
  val heuristic_weight : (Literal.term -> int) -> Literal.t -> int
  val depth : Literal.t -> int
  val sign : Literal.t -> bool
  val is_pos : Literal.t -> bool
  val is_neg : Literal.t -> bool
  val is_eqn : Literal.t -> bool
  val is_prop : Literal.t -> bool
  val is_eq : Literal.t -> bool
  val is_neq : Literal.t -> bool
  val is_arith : Literal.t -> bool
  val is_arith_eqn : Literal.t -> bool
  val is_arith_eq : Literal.t -> bool
  val is_arith_neq : Literal.t -> bool
  val is_arith_ineq : Literal.t -> bool
  val is_arith_less : Literal.t -> bool
  val is_arith_lesseq : Literal.t -> bool
  val is_arith_divides : Literal.t -> bool
  val mk_eq : Literal.term -> Literal.term -> Literal.t
  val mk_neq : Literal.term -> Literal.term -> Literal.t
  val mk_lit : Literal.term -> Literal.term -> bool -> Literal.t
  val mk_prop : Literal.term -> bool -> Literal.t
  val mk_true : Literal.term -> Literal.t
  val mk_false : Literal.term -> Literal.t
  val mk_tauto : Literal.t
  val mk_absurd : Literal.t
  val mk_arith : ArithLit.t -> Literal.t
  val mk_arith_op : ArithLit.op -> Z.t Monome.t -> Z.t Monome.t -> Literal.t
  val mk_arith_eq : Z.t Monome.t -> Z.t Monome.t -> Literal.t
  val mk_arith_neq : Z.t Monome.t -> Z.t Monome.t -> Literal.t
  val mk_arith_less : Z.t Monome.t -> Z.t Monome.t -> Literal.t
  val mk_arith_lesseq : Z.t Monome.t -> Z.t Monome.t -> Literal.t
  val mk_divides :
    ?sign:bool -> Z.t -> power:int -> Z.t Monome.t -> Literal.t
  val mk_not_divides : Z.t -> power:int -> Z.t Monome.t -> Literal.t
  val matching :
    ?subst:Libzipperposition.Substs.t ->
    pattern:Literal.t Libzipperposition.Scoped.t ->
    Literal.t Libzipperposition.Scoped.t ->
    Libzipperposition.Substs.t Sequence.t
  val subsumes :
    ?subst:Libzipperposition.Substs.t ->
    Literal.t Libzipperposition.Scoped.t ->
    Literal.t Libzipperposition.Scoped.t ->
    Libzipperposition.Substs.t Sequence.t
  val variant :
    ?subst:Libzipperposition.Substs.t ->
    Literal.t Libzipperposition.Scoped.t ->
    Literal.t Libzipperposition.Scoped.t ->
    Libzipperposition.Substs.t Sequence.t
  val unify :
    ?subst:Libzipperposition.Substs.t ->
    Literal.t Libzipperposition.Scoped.t ->
    Literal.t Libzipperposition.Scoped.t ->
    Libzipperposition.Substs.t Sequence.t
  val are_variant : Literal.t -> Literal.t -> bool
  val apply_subst :
    renaming:Libzipperposition.Substs.Renaming.t ->
    Libzipperposition.Substs.t ->
    Literal.t Libzipperposition.Scoped.t -> Literal.t
  val apply_subst_no_renaming :
    Libzipperposition.Substs.t ->
    Literal.t Libzipperposition.Scoped.t -> Literal.t
  val apply_subst_no_simp :
    renaming:Libzipperposition.Substs.Renaming.t ->
    Libzipperposition.Substs.t ->
    Literal.t Libzipperposition.Scoped.t -> Literal.t
  val apply_subst_list :
    renaming:Libzipperposition.Substs.Renaming.t ->
    Libzipperposition.Substs.t ->
    Literal.t list Libzipperposition.Scoped.t -> Literal.t list
  val negate : Literal.t -> Literal.t
  val map : (Literal.term -> Literal.term) -> Literal.t -> Literal.t
  val fold : ('a -> Literal.term -> 'a) -> 'a -> Literal.t -> 'a
  val vars :
    Literal.t -> Libzipperposition.Type.t Libzipperposition.HVar.t list
  val var_occurs :
    Libzipperposition.Type.t Libzipperposition.HVar.t -> Literal.t -> bool
  val is_ground : Literal.t -> bool
  val symbols : Literal.t -> Libzipperposition.ID.Set.t
  val root_terms : Literal.t -> Literal.term list
  val is_trivial : Literal.t -> bool
  val is_absurd : Literal.t -> bool
  val fold_terms :
    ?position:Libzipperposition.Position.t ->
    ?vars:bool ->
    ?ty_args:bool ->
    which:[< `All | `Max ] ->
    ord:Libzipperposition.Ordering.t ->
    subterms:bool ->
    Literal.t -> (Literal.term * Libzipperposition.Position.t) Sequence.t
  module Comp :
    sig
      val max_terms :
        ord:Libzipperposition.Ordering.t -> Literal.t -> Literal.term list
      val compare :
        ord:Libzipperposition.Ordering.t ->
        Literal.t -> Literal.t -> Libzipperposition.Comparison.t
    end
  module Seq :
    sig
      val terms : Literal.t -> Literal.term Sequence.t
      val vars :
        Literal.t ->
        Libzipperposition.Type.t Libzipperposition.HVar.t Sequence.t
      val symbols : Literal.t -> Libzipperposition.ID.t Sequence.t
    end
  module Pos :
    sig
      type split = {
        lit_pos : Libzipperposition.Position.t;
        term_pos : Libzipperposition.Position.t;
        term : Literal.term;
      }
      val split :
        Literal.t -> Libzipperposition.Position.t -> Literal.Pos.split
      val at : Literal.t -> Libzipperposition.Position.t -> Literal.term
      val replace :
        Literal.t ->
        at:Libzipperposition.Position.t -> by:Literal.term -> Literal.t
      val cut :
        Literal.t ->
        Libzipperposition.Position.t ->
        Libzipperposition.Position.t * Libzipperposition.Position.t
      val root_term :
        Literal.t -> Libzipperposition.Position.t -> Literal.term
      val term_pos :
        Literal.t ->
        Libzipperposition.Position.t -> Libzipperposition.Position.t
      val is_max_term :
        ord:Libzipperposition.Ordering.t ->
        Literal.t -> Libzipperposition.Position.t -> bool
    end
  module View :
    sig
      val as_eqn : Literal.t -> (Literal.term * Literal.term * bool) option
      val get_eqn :
        Literal.t ->
        Libzipperposition.Position.t ->
        (Literal.term * Literal.term * bool) option
      val get_arith : Literal.t -> ArithLit.t option
      val focus_arith :
        Literal.t -> Libzipperposition.Position.t -> ArithLit.Focus.t option
      val unfocus_arith : ArithLit.Focus.t -> Literal.t
    end
  module Conv :
    sig
      type hook_from =
          Literal.term Libzipperposition.SLiteral.t -> Literal.t option
      type hook_to =
          Literal.t -> Literal.term Libzipperposition.SLiteral.t option
      val arith_hook_from : Literal.Conv.hook_from
      val of_form :
        ?hooks:Literal.Conv.hook_from list ->
        Literal.term Libzipperposition.SLiteral.t -> Literal.t
      val to_form :
        ?hooks:Literal.Conv.hook_to list ->
        Literal.t -> Literal.term Libzipperposition.SLiteral.t
    end
  type print_hook = CCFormat.t -> Literal.t -> bool
  val add_default_hook : Literal.print_hook -> unit
  val pp_debug : ?hooks:Literal.print_hook list -> Literal.t CCFormat.printer
  val pp : Literal.t CCFormat.printer
  val pp_tstp : Literal.t CCFormat.printer
  val to_string : Literal.t -> string
end