1 2 3 4 5 6 7 8 9
% EXPECT: unsat x, y: REAL; f: REAL -> REAL; ASSERT (x <= y); ASSERT (y <= x); ASSERT NOT (f(x) = f(y)); CHECKSAT;