% EXPECT: sat
% EXIT: 10
x, y: REAL;
f: REAL -> REAL;

CHECKSAT NOT (f(x) = f(y));