The formulas in the benchmarks presented here are quantified formulas,
with equality, uninterpreted predicates and functions, order
predicates, and linear real arithmetic, or linear integer arithmetic.
The input langage is
Simplify-like:
Boolean functions are written
(<connector> <pred1>... <predN>),
where <connector> can be AND, OR, IMPLIES (N=2), IFF (N=2) or
NOT (N=1).
Universally quantified formulas are written
(FORALL (<var1> ... <varN>) <body>), and
existentially quantified formulas
(EXISTS (<var1> ... <varN>) <body>).
An atom is either a proposition, which is simply written as the
proposition identifier, an uninterpreted predicate <id> applied
to the right number N of terms (<id> <term1>
... <termN>), or a relation between two terms written
(<relation> <term1> <term2>) where <relation> is
either EQ, <, <=, >, >=.
Finally, a term is either an uninterpreted constant or variable, which
is simply written as the identifier, or a number, or an uninterpreted
function <id> applied to the right number N of terms (<id>
<term1> ... <termN>), or a arithmetic function
(<function> <term1> ... <termN>) where
<function> is either +, *, or -.