## Chapter 4

Produced Output

The output is a set of boxes on which the input is guaranteed to be true, a set of
boxes, on which the input is guaranteed to be false, and a set of boxes for which
we do not know anything. Note that if the input contains function symbols
that are not defined everywhere (e.g., asin is only defined on the interval
[-1, 1]), then also the truth value of the corresponding constraint might
be undefined, and no corresponding box of true or false values will be
computed.

In some cases, the software also prints witnesses corresponding to these boxes.
For example, in the case when an existentially quantified constraint has
been proven to hold, in certain cases it also prints a witness for this
quantifier, that is, a point for which the constraint under the quantifier
holds.

There is a separate graphical user interface, which prints true boxes in green
and false boxes red boxes in red. Note that the graphical output is not faithfully
rounded. For example, a green and a red box might touch on the screen, although
the computed boxes do not.