% EXPECT: sat
% EXIT: 10
x1, y1, z1: REAL;
x2, y2, z2: REAL;
f: REAL -> REAL;
g: (REAL, REAL) -> REAL;

ASSERT (z1 = f(x1));
ASSERT (z2 = f(y1));
ASSERT NOT (g(z1, z2) = g(z2, y2));

CHECKSAT;