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.