sig
  type term = Libzipperposition.FOTerm.t
  type op = Equal | Different | Less | Lesseq
  type 'm divides = { num : Z.t; power : int; monome : 'm; sign : bool; }
  type t = private
      Binary of ArithLit.op * Z.t Monome.t * Z.t Monome.t
    | Divides of Z.t Monome.t ArithLit.divides
  type lit = ArithLit.t
  val equal_com : ArithLit.t -> ArithLit.t -> bool
  val compare : ArithLit.t -> ArithLit.t -> int
  val equal : ArithLit.t -> ArithLit.t -> bool
  val hash_fun : t -> CCHash.state -> CCHash.state
  val hash : t -> int
  val make : ArithLit.op -> Z.t Monome.t -> Z.t Monome.t -> ArithLit.t
  val mk_eq : Z.t Monome.t -> Z.t Monome.t -> ArithLit.t
  val mk_neq : Z.t Monome.t -> Z.t Monome.t -> ArithLit.t
  val mk_less : Z.t Monome.t -> Z.t Monome.t -> ArithLit.t
  val mk_lesseq : Z.t Monome.t -> Z.t Monome.t -> ArithLit.t
  val mk_divides :
    ?sign:bool -> Z.t -> power:int -> Z.t Monome.t -> ArithLit.t
  val mk_not_divides : Z.t -> power:int -> Z.t Monome.t -> ArithLit.t
  val negate : ArithLit.t -> ArithLit.t
  val sign : ArithLit.t -> bool
  val polarity : ArithLit.t -> bool
  val is_pos : ArithLit.t -> bool
  val is_neg : ArithLit.t -> bool
  val is_eq : ArithLit.t -> bool
  val is_neq : ArithLit.t -> bool
  val is_eqn : ArithLit.t -> bool
  val is_ineq : ArithLit.t -> bool
  val is_less : ArithLit.t -> bool
  val is_lesseq : ArithLit.t -> bool
  val is_divides : ArithLit.t -> bool
  val pp : ArithLit.t CCFormat.printer
  val pp_tstp : ArithLit.t CCFormat.printer
  val to_string : ArithLit.t -> string
  val fold : ('a -> ArithLit.term -> 'a) -> 'a -> ArithLit.t -> 'a
  val map : (ArithLit.term -> ArithLit.term) -> ArithLit.t -> ArithLit.t
  type 'a unif =
      subst:Libzipperposition.Substs.t ->
      'a Libzipperposition.Scoped.t ->
      'a Libzipperposition.Scoped.t -> Libzipperposition.Substs.t Sequence.t
  val generic_unif : Z.t Monome.t ArithLit.unif -> ArithLit.t ArithLit.unif
  val apply_subst :
    renaming:Libzipperposition.Substs.Renaming.t ->
    Libzipperposition.Substs.t ->
    ArithLit.t Libzipperposition.Scoped.t -> ArithLit.t
  val apply_subst_no_renaming :
    Libzipperposition.Substs.t ->
    ArithLit.t Libzipperposition.Scoped.t -> ArithLit.t
  val apply_subst_no_simp :
    renaming:Libzipperposition.Substs.Renaming.t ->
    Libzipperposition.Substs.t ->
    ArithLit.t Libzipperposition.Scoped.t -> ArithLit.t
  val matching :
    ?subst:Libzipperposition.Substs.t ->
    ArithLit.t Libzipperposition.Scoped.t ->
    ArithLit.t Libzipperposition.Scoped.t ->
    Libzipperposition.Substs.t Sequence.t
  val variant :
    ?subst:Libzipperposition.Substs.t ->
    ArithLit.t Libzipperposition.Scoped.t ->
    ArithLit.t Libzipperposition.Scoped.t ->
    Libzipperposition.Substs.t Sequence.t
  val unify :
    ?subst:Libzipperposition.Substs.t ->
    ArithLit.t Libzipperposition.Scoped.t ->
    ArithLit.t Libzipperposition.Scoped.t ->
    Libzipperposition.Substs.t Sequence.t
  val subsumes :
    ?subst:Libzipperposition.Substs.t ->
    ArithLit.t Libzipperposition.Scoped.t ->
    ArithLit.t Libzipperposition.Scoped.t ->
    Libzipperposition.Substs.t Sequence.t
  val are_variant : ArithLit.t -> ArithLit.t -> bool
  val is_trivial : ArithLit.t -> bool
  val is_absurd : ArithLit.t -> bool
  val fold_terms :
    ?pos:Libzipperposition.Position.t ->
    ?vars:bool ->
    ?ty_args:bool ->
    which:[< `All | `Max ] ->
    ord:Libzipperposition.Ordering.t ->
    subterms:bool ->
    ArithLit.t -> (ArithLit.term * Libzipperposition.Position.t) Sequence.t
  val max_terms :
    ord:Libzipperposition.Ordering.t -> ArithLit.t -> ArithLit.term list
  val to_form :
    ArithLit.t -> Libzipperposition.FOTerm.t Libzipperposition.SLiteral.t
  module Seq :
    sig
      val terms : ArithLit.t -> ArithLit.term Sequence.t
      val vars : ArithLit.t -> Libzipperposition.FOTerm.var Sequence.t
      val to_multiset : ArithLit.t -> (ArithLit.term * Z.t) Sequence.t
    end
  module Focus :
    sig
      type t =
          Left of ArithLit.op * Z.t Monome.Focus.t * Z.t Monome.t
        | Right of ArithLit.op * Z.t Monome.t * Z.t Monome.Focus.t
        | Div of Z.t Monome.Focus.t ArithLit.divides
      val mk_left :
        ArithLit.op -> Z.t Monome.Focus.t -> Z.t Monome.t -> ArithLit.Focus.t
      val mk_right :
        ArithLit.op -> Z.t Monome.t -> Z.t Monome.Focus.t -> ArithLit.Focus.t
      val mk_div :
        ?sign:bool ->
        Z.t -> power:int -> Z.t Monome.Focus.t -> ArithLit.Focus.t
      val get :
        ArithLit.lit ->
        Libzipperposition.Position.t -> ArithLit.Focus.t option
      val get_exn :
        ArithLit.lit -> Libzipperposition.Position.t -> ArithLit.Focus.t
      val focus_term :
        ArithLit.lit -> ArithLit.term -> ArithLit.Focus.t option
      val focus_term_exn : ArithLit.lit -> ArithLit.term -> ArithLit.Focus.t
      val replace : ArithLit.Focus.t -> Z.t Monome.t -> ArithLit.lit
      val term : ArithLit.Focus.t -> ArithLit.term
      val focused_monome : ArithLit.Focus.t -> Z.t Monome.Focus.t
      val opposite_monome : ArithLit.Focus.t -> Z.t Monome.t option
      val opposite_monome_exn : ArithLit.Focus.t -> Z.t Monome.t
      val is_max :
        ord:Libzipperposition.Ordering.t -> ArithLit.Focus.t -> bool
      val is_strictly_max :
        ord:Libzipperposition.Ordering.t -> ArithLit.Focus.t -> bool
      val map_lit :
        f_m:(Z.t Monome.t -> Z.t Monome.t) ->
        f_mf:(Z.t Monome.Focus.t -> Z.t Monome.Focus.t) ->
        ArithLit.Focus.t -> ArithLit.Focus.t
      val product : ArithLit.Focus.t -> Z.t -> ArithLit.Focus.t
      val scale :
        ArithLit.Focus.t ->
        ArithLit.Focus.t -> ArithLit.Focus.t * ArithLit.Focus.t
      val scale_power : ArithLit.Focus.t -> int -> ArithLit.Focus.t
      val apply_subst :
        renaming:Libzipperposition.Substs.Renaming.t ->
        Libzipperposition.Substs.t ->
        ArithLit.Focus.t Libzipperposition.Scoped.t -> ArithLit.Focus.t
      val apply_subst_no_renaming :
        Libzipperposition.Substs.t ->
        ArithLit.Focus.t Libzipperposition.Scoped.t -> ArithLit.Focus.t
      val unify :
        ?subst:Libzipperposition.Substs.t ->
        ArithLit.Focus.t Libzipperposition.Scoped.t ->
        ArithLit.Focus.t Libzipperposition.Scoped.t ->
        (ArithLit.Focus.t * ArithLit.Focus.t * Libzipperposition.Substs.t)
        Sequence.t
      val fold_terms :
        ?pos:Libzipperposition.Position.t ->
        ArithLit.lit ->
        (ArithLit.Focus.t * Libzipperposition.Position.t) Sequence.t
      val op : ArithLit.Focus.t -> [ `Binary of ArithLit.op | `Divides ]
      val unfocus : ArithLit.Focus.t -> ArithLit.lit
      val pp : ArithLit.Focus.t CCFormat.printer
      val to_string : ArithLit.Focus.t -> string
    end
  module Util :
    sig
      type divisor = { prime : Z.t; power : int; }
      val is_prime : Z.t -> bool
      val prime_decomposition : Z.t -> ArithLit.Util.divisor list
      val primes_leq : Z.t -> Z.t Sequence.t
    end
end