% EXPECT: unsat
OPTION "sets-ext";
OPTION "logic" "ALL_SUPPORTED";
Atom: TYPE;

a : SET OF [Atom];
b : SET OF [Atom, Atom];

x : Atom;
y : Atom;

ASSERT NOT(x = y);

ASSERT TUPLE(y) IS_IN a;
ASSERT (x, y) IS_IN b;

ASSERT UNIVERSE::SET OF [Atom, Atom] = (UNIVERSE::SET OF [Atom] PRODUCT UNIVERSE::SET OF [Atom]);

u : SET OF [Atom, Atom];
ASSERT u = UNIVERSE::SET OF [Atom, Atom];

ASSERT NOT (x, y) IS_IN u;

CHECKSAT;