(logic QF_UFNRA

 :written_by {Cesare Tinelli}
 :date {26/06/09}
] 
 :theory Reals

 :language
 "Closed quantifier-free formulas built over an arbitrary expansion of 
  the Reals signature with free sort, function, and/or predicate symbols 
  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.

  Formulas in ite terms must satisfy the same restriction, with the 
  exception that they need not be closed.
 "
 :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.
 "
 :extensions
 "Also allowed are rational coefficients: expressions of the form:
  (/ m n) where n is a numeral other than 0 and m is either a numeral
  or an expression of the form (~ i) for some numeral i, 

  An atom with rational coefficients is syntactic sugar for any equivalent
  atom with integer coefficients obtained by applying standard arithmetic
  transformations.
 ")