sig
  type term = Libzipperposition.FOTerm.t
  type 'a t
  type 'a monome = 'a Monome.t
  val eq : 'n Monome.t -> 'n Monome.t -> bool
  val compare : 'n Monome.t -> 'n Monome.t -> int
  val hash : 'a Monome.t -> int
  val hash_fun : 'a Monome.t CCHash.hash_fun
  val ty : 'a Monome.t -> Libzipperposition.Type.t
  val const : 'a Monome.t -> 'a
  val coeffs : 'a Monome.t -> ('a * Monome.term) list
  val find : 'a Monome.t -> Monome.term -> 'a option
  val find_exn : 'a Monome.t -> Monome.term -> 'a
  val mem : 'a Monome.t -> Monome.term -> bool
  val add : 'a Monome.t -> 'a -> Monome.term -> 'a Monome.t
  val add_const : 'a Monome.t -> 'a -> 'a Monome.t
  val remove : 'a Monome.t -> Monome.term -> 'a Monome.t
  val remove_const : 'a Monome.t -> 'a Monome.t
  val add_list : 'a Monome.t -> ('a * Monome.term) list -> 'a Monome.t
  val map : (Monome.term -> Monome.term) -> 'a Monome.t -> 'a Monome.t
  val map_num : ('a -> 'a) -> 'a Monome.t -> 'a Monome.t
  module Seq :
    sig
      val terms : 'a Monome.t -> Monome.term Sequence.t
      val vars : 'a Monome.t -> Libzipperposition.FOTerm.var Sequence.t
      val coeffs : 'a Monome.t -> ('a * Monome.term) Sequence.t
      val coeffs_swap : 'a Monome.t -> (Monome.term * 'a) Sequence.t
    end
  val is_const : 'a Monome.t -> bool
  val is_zero : 'a Monome.t -> bool
  val sign : 'a Monome.t -> int
  val size : 'a Monome.t -> int
  val terms : 'a Monome.t -> Monome.term list
  val var_occurs : var:Libzipperposition.FOTerm.var -> 'a Monome.t -> bool
  val sum : 'a Monome.t -> 'a Monome.t -> 'a Monome.t
  val difference : 'a Monome.t -> 'a Monome.t -> 'a Monome.t
  val uminus : 'a Monome.t -> 'a Monome.t
  val product : 'a Monome.t -> 'a -> 'a Monome.t
  val succ : 'a Monome.t -> 'a Monome.t
  val pred : 'a Monome.t -> 'a Monome.t
  val sum_list : 'a Monome.t list -> 'a Monome.t
  val comparison :
    'a Monome.t -> 'a Monome.t -> Libzipperposition.Comparison.t
  val dominates : strict:bool -> 'a Monome.t -> 'a Monome.t -> bool
  val split : 'a Monome.t -> 'a Monome.t * 'a Monome.t
  val apply_subst :
    renaming:Libzipperposition.Substs.Renaming.t ->
    Libzipperposition.Substs.t ->
    'a Monome.t Libzipperposition.Scoped.t -> 'a Monome.t
  val apply_subst_no_renaming :
    Libzipperposition.Substs.t ->
    'a Monome.t Libzipperposition.Scoped.t -> 'a Monome.t
  val variant :
    ?subst:Libzipperposition.Substs.t ->
    'a Monome.t Libzipperposition.Scoped.t ->
    'a Monome.t Libzipperposition.Scoped.t ->
    Libzipperposition.Substs.t Sequence.t
  val matching :
    ?subst:Libzipperposition.Substs.t ->
    'a Monome.t Libzipperposition.Scoped.t ->
    'a Monome.t Libzipperposition.Scoped.t ->
    Libzipperposition.Substs.t Sequence.t
  val unify :
    ?subst:Libzipperposition.Substs.t ->
    'a Monome.t Libzipperposition.Scoped.t ->
    'a Monome.t Libzipperposition.Scoped.t ->
    Libzipperposition.Substs.t Sequence.t
  val is_ground : 'a Monome.t -> bool
  val fold :
    ('a -> int -> 'b -> Monome.term -> 'a) -> 'a -> 'b Monome.t -> 'a
  val fold_max :
    ord:Libzipperposition.Ordering.t ->
    ('a -> int -> 'b -> Monome.term -> 'a) -> 'a -> 'b Monome.t -> 'a
  val nth : 'a Monome.t -> int -> 'a * Monome.term
  val set : 'a Monome.t -> int -> 'a * Monome.term -> 'a Monome.t
  val set_term : 'a Monome.t -> int -> Monome.term -> 'a Monome.t
  module Focus :
    sig
      type 'a t = {
        term : Monome.term;
        coeff : 'a;
        rest : 'a Monome.monome;
      }
      val get : 'a Monome.monome -> int -> 'a Monome.Focus.t
      val focus_term :
        'a Monome.monome -> Monome.term -> 'a Monome.Focus.t option
      val focus_term_exn :
        'a Monome.monome -> Monome.term -> 'a Monome.Focus.t
      val to_monome : 'a Monome.Focus.t -> 'a Monome.monome
      val coeff : 'a Monome.Focus.t -> 'a
      val term : 'a Monome.Focus.t -> Monome.term
      val rest : 'a Monome.Focus.t -> 'a Monome.monome
      val sum : 'a Monome.Focus.t -> 'a Monome.monome -> 'a Monome.Focus.t
      val difference :
        'a Monome.Focus.t -> 'a Monome.monome -> 'a Monome.Focus.t
      val uminus : 'a Monome.Focus.t -> 'a Monome.Focus.t
      val product : 'a Monome.Focus.t -> 'a -> 'a Monome.Focus.t
      val map :
        ?term:(Monome.term -> Monome.term) ->
        ?coeff:('a -> 'a) ->
        ?rest:('a Monome.monome -> 'a Monome.monome) ->
        'a Monome.Focus.t -> 'a Monome.Focus.t
      val scale :
        Z.t Monome.Focus.t ->
        Z.t Monome.Focus.t -> Z.t Monome.Focus.t * Z.t Monome.Focus.t
      val is_max :
        ord:Libzipperposition.Ordering.t -> 'a Monome.Focus.t -> bool
      val fold_m :
        pos:Libzipperposition.Position.t ->
        'a Monome.monome ->
        'b ->
        ('b -> 'a Monome.Focus.t -> Libzipperposition.Position.t -> 'b) -> 'b
      val apply_subst :
        renaming:Libzipperposition.Substs.Renaming.t ->
        Libzipperposition.Substs.t ->
        'a Monome.Focus.t Libzipperposition.Scoped.t -> 'a Monome.Focus.t
      val apply_subst_no_renaming :
        Libzipperposition.Substs.t ->
        'a Monome.Focus.t Libzipperposition.Scoped.t -> 'a Monome.Focus.t
      val unify_ff :
        ?subst:Libzipperposition.Substs.t ->
        'a Monome.Focus.t Libzipperposition.Scoped.t ->
        'a Monome.Focus.t Libzipperposition.Scoped.t ->
        ('a Monome.Focus.t * 'a Monome.Focus.t * Libzipperposition.Substs.t)
        Sequence.t
      val unify_mm :
        ?subst:Libzipperposition.Substs.t ->
        'a Monome.monome Libzipperposition.Scoped.t ->
        'a Monome.monome Libzipperposition.Scoped.t ->
        ('a Monome.Focus.t * 'a Monome.Focus.t * Libzipperposition.Substs.t)
        Sequence.t
      val unify_self :
        ?subst:Libzipperposition.Substs.t ->
        'a Monome.Focus.t Libzipperposition.Scoped.t ->
        ('a Monome.Focus.t * Libzipperposition.Substs.t) Sequence.t
      val unify_self_monome :
        ?subst:Libzipperposition.Substs.t ->
        'a Monome.monome Libzipperposition.Scoped.t ->
        ('a Monome.Focus.t * Libzipperposition.Substs.t) Sequence.t
      val pp : 'a Monome.Focus.t CCFormat.printer
    end
  val pp : 'a Monome.t CCFormat.printer
  val to_string : 'a Monome.t -> string
  val pp_tstp : 'a Monome.t CCFormat.printer
  exception NotLinear
  module Int :
    sig
      type t = Z.t Monome.monome
      val const : Z.t -> Monome.Int.t
      val singleton : Z.t -> Monome.term -> Monome.Int.t
      val of_list : Z.t -> (Z.t * Monome.term) list -> Monome.Int.t
      val of_term : Monome.term -> Monome.Int.t option
      val of_term_exn : Monome.term -> Monome.Int.t
      val to_term : Monome.Int.t -> Monome.term
      val normalize : Monome.Int.t -> Monome.Int.t
      val has_instances : Monome.Int.t -> bool
      val quotient : Monome.Int.t -> Z.t -> Monome.Int.t option
      val divisible : Monome.Int.t -> Z.t -> bool
      val factorize : Monome.Int.t -> (Monome.Int.t * Z.t) option
      val normalize_wrt_zero : Monome.Int.t -> Monome.Int.t
      val reduce_same_factor :
        Monome.Int.t ->
        Monome.Int.t -> Monome.term -> Monome.Int.t * Monome.Int.t
      val compare :
        (Monome.term -> Monome.term -> Libzipperposition.Comparison.t) ->
        Monome.Int.t -> Monome.Int.t -> Libzipperposition.Comparison.t
      val to_multiset : Monome.Int.t -> Multisets.MT.t
      module Modulo :
        sig
          val modulo : n:Z.t -> Z.t -> Z.t
          val sum : n:Z.t -> Z.t -> Z.t -> Z.t
          val uminus : n:Z.t -> Z.t -> Z.t
        end
      module Solve :
        sig
          type solution = (Monome.term * Monome.Int.t) list
          val split_solution :
            Monome.Int.Solve.solution ->
            Libzipperposition.Substs.t * Monome.Int.Solve.solution
          val diophant2 : Z.t -> Z.t -> Z.t -> Z.t * Z.t * Z.t
          val diophant_l : Z.t list -> Z.t -> Z.t list * Z.t
          val coeffs_n :
            Z.t list -> Z.t -> Monome.term list -> Monome.Int.t list
          val eq_zero :
            ?fresh_var:(Libzipperposition.Type.t -> Monome.term) ->
            Monome.Int.t -> Monome.Int.Solve.solution list
          val lower_zero :
            ?fresh_var:(Libzipperposition.Type.t -> Monome.term) ->
            strict:bool -> Monome.Int.t -> Monome.Int.Solve.solution list
          val lt_zero :
            ?fresh_var:(Libzipperposition.Type.t -> Monome.term) ->
            Monome.Int.t -> Monome.Int.Solve.solution list
          val leq_zero :
            ?fresh_var:(Libzipperposition.Type.t -> Monome.term) ->
            Monome.Int.t -> Monome.Int.Solve.solution list
          val neq_zero :
            ?fresh_var:(Libzipperposition.Type.t -> Monome.term) ->
            Monome.Int.t -> Monome.Int.Solve.solution list
        end
    end
end