Assumptions can be given both as an argument and as an option value:
Specifying
Assumptions as an option value prevents
Refine from using
$Assumptions:
Checking whether a condition follows from assumptions may take a long time:
If a condition does not follow from assumptions, checking this may still take a long time:
The time spent on a single condition check is restricted by the value of
TimeConstraint:
With a time constraint of 1 second
Refine cannot prove that
x6+y6+z6-x y z≥0: