/*example of simplied assumption & predicate 21 query */
#include <civlc.cvh>

$input double x0, x1;

void main() {
  $assume((x0 > 0) && (x1 > 0));
  
  $assert((x1 * x1 *(-1) > 0 || x1 * x1 > 0) &&
	  (x1 * x1 *(-1) > 0 || x0 * x0 + x1 * x1 >= 0) &&
	  (x1 * x1 > 0 || x0 * x0 * (-1) + x1 * x1 * (-1) >=0) &&
	  (x0 * x0 * (-1) + x1 * x1 * (-1) >=0 || x0 * x0 + x1 * x1 >=0));
}