Quantifier elimination QE
decides truth of real arithmetic formulas.
QE may potentially take a long time. Reducing the number of variables that occur in formulas helps.
Use Edit → abbrv
to simplify formulas together with hideL
and hideR
to hide irrelevant
assumptions and alternatives prior to QE.
See also
Learning resources