Counter-example search result

Formula not valid, found a counter-example

Counter-example values

{{cex.symbol}}
{{cex.value}}

Speculated values for quantified variables

{{cex.symbol}}
{{cex.value}}

No counter-example found. Try proving it to see if it is valid. Some arithmetic simplifications may help reduce the complexity.

If the formula cannot be proved (⊢ false) and no counter-example can be found, then sanity check it, e.g., whether you could have divided by zero.

No counter-example found before search timeout expired.

No counter-example found, but the sequent contains box modalities [a]p or diamond modalities <a>p, which make counter-example search less effective.

Please use more proof steps on formula

{{origFormula}}

to handle modalities, until only arithmetic formulas remain and then try again.

The current backend tool does not support counter-example search.

Please go to Help → Tool Configuration and configure Mathematica as backend tool.