The following is an example program input:
The three elements represent the following objects:
In general, the representation of the input constraint can contain the following symbols:
All binary symbols are infix, and all other prefix. One can use parenthesis for the term structure and brackets for the logical structure. Quantifiers have three arguments:
Note that quantifiers bind stronger than connectives. Hence the input
will result in the error message that the variable x cannot be found. Using brackets, arriving at
solves the problem.
Although the software also allows equality predicates = it currently is not able to deduce positive information for them. Work on constraints with equalities is in progress.
Trigonometric functions expect their input in radians.