(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) (assert (not (= (- (+ (* x x) (* y y)) (* 2.0 x y)) (* (- x y) (+ (- y) x))) )) (check-sat)