(logic UFNIA
:written_by {Cesare Tinelli}
:date {26/06/09}
:theory Ints
:language
"Closed formulas built over an arbitrary expansion of the Ints signature
with free sort, function, and/or predicate symbol, containing one or
more non-linear atoms, that is, atoms with terms of the form
(* x y) where neither x nor y is a numeral.
"
:extensions
"In addition to 0 and 1, numerals n > 1 are allowed also as arguments of
predicate or function symbols. In that case, they abbreviate the term
(+ 1 ... 1) with n occurrences of 1.
"
)