(set-info :smt-lib-version 2.6) (set-logic QF_NRA) (set-info :category |Crafted from GATeL POs|) (set-info :status unsat) (declare-fun x () Real) (declare-fun y () Real) (define-fun s2 () Real (+ (+ (+ (- (* (* 1.9 x) x) (* y y)) (* (* 2.0 x) y)) (* (* 1.1 x) x)) (* (* 4.0 y) y))) (define-fun s2r () Real (+ (* (+ x y) (+ x y)) (* 2.0 x x) (* 2.0 y y))) (assert (not (= s2 s2r) )) (check-sat)