% EXPECT: unsat
OPTION "logic" "ALL_SUPPORTED";
IntPair: TYPE = [INT, INT];
x : SET OF IntPair;
y : SET OF IntPair;
a: INT;
b:INT;
c:INT;
d:INT;
ASSERT (1, a) IS_IN x;
ASSERT (1, c) IS_IN x;
ASSERT (1, d) IS_IN x;
ASSERT (b, 1) IS_IN x;
ASSERT (b = d);
ASSERT (2,b) IS_IN ((x JOIN x) JOIN x);
ASSERT NOT (2, 1) IS_IN TCLOSURE(x);


CHECKSAT;