path: root/test/regress/regress1/rels/rel_pressure_0.cvc

% EXPECT: unsat
OPTION "logic" "ALL";
IntPair: TYPE = [INT, INT];
x : SET OF IntPair;
y : SET OF IntPair;
z : SET OF IntPair;
r : SET OF IntPair;

a11 : IntPair;
ASSERT a11 = (1, 1);
ASSERT a11 IS_IN x;
a12 : IntPair;
ASSERT a12 = (1, 2);
ASSERT a12 IS_IN x;
a13 : IntPair;
ASSERT a13 = (1, 3);
ASSERT a13 IS_IN x;
a14 : IntPair;
ASSERT a14 = (1, 4);
ASSERT a14 IS_IN x;
a15 : IntPair;
ASSERT a15 = (1, 5);
ASSERT a15 IS_IN x;
a16 : IntPair;
ASSERT a16 = (1, 6);
ASSERT a16 IS_IN x;
a17 : IntPair;
ASSERT a17 = (1, 7);
ASSERT a17 IS_IN x;
a18 : IntPair;
ASSERT a18 = (1, 8);
ASSERT a18 IS_IN x;
a19 : IntPair;
ASSERT a19 = (1, 9);
ASSERT a19 IS_IN x;
a110 : IntPair;
ASSERT a110 = (1, 10);
ASSERT a110 IS_IN x;
a21 : IntPair;
ASSERT a21 = (2, 1);
ASSERT a21 IS_IN x;
a22 : IntPair;
ASSERT a22 = (2, 2);
ASSERT a22 IS_IN x;
a23 : IntPair;
ASSERT a23 = (2, 3);
ASSERT a23 IS_IN x;
a24 : IntPair;
ASSERT a24 = (2, 4);
ASSERT a24 IS_IN x;
a25 : IntPair;
ASSERT a25 = (2, 5);
ASSERT a25 IS_IN x;
a26 : IntPair;
ASSERT a26 = (2, 6);
ASSERT a26 IS_IN x;
a27 : IntPair;
ASSERT a27 = (2, 7);
ASSERT a27 IS_IN x;
a28 : IntPair;
ASSERT a28 = (2, 8);
ASSERT a28 IS_IN x;
a29 : IntPair;
ASSERT a29 = (2, 9);
ASSERT a29 IS_IN x;
a210 : IntPair;
ASSERT a210 = (2, 10);
ASSERT a210 IS_IN x;
a31 : IntPair;
ASSERT a31 = (3, 1);
ASSERT a31 IS_IN x;
a32 : IntPair;
ASSERT a32 = (3, 2);
ASSERT a32 IS_IN x;
a33 : IntPair;
ASSERT a33 = (3, 3);
ASSERT a33 IS_IN x;
a34 : IntPair;
ASSERT a34 = (3, 4);
ASSERT a34 IS_IN x;
a35 : IntPair;
ASSERT a35 = (3, 5);
ASSERT a35 IS_IN x;
a36 : IntPair;
ASSERT a36 = (3, 6);
ASSERT a36 IS_IN x;
a37 : IntPair;
ASSERT a37 = (3, 7);
ASSERT a37 IS_IN x;
a38 : IntPair;
ASSERT a38 = (3, 8);
ASSERT a38 IS_IN x;
a39 : IntPair;
ASSERT a39 = (3, 9);
ASSERT a39 IS_IN x;
a310 : IntPair;
ASSERT a310 = (3, 10);
ASSERT a310 IS_IN x;
a41 : IntPair;
ASSERT a41 = (4, 1);
ASSERT a41 IS_IN x;
a42 : IntPair;
ASSERT a42 = (4, 2);
ASSERT a42 IS_IN x;
a43 : IntPair;
ASSERT a43 = (4, 3);
ASSERT a43 IS_IN x;
a44 : IntPair;
ASSERT a44 = (4, 4);
ASSERT a44 IS_IN x;
a45 : IntPair;
ASSERT a45 = (4, 5);
ASSERT a45 IS_IN x;
a46 : IntPair;
ASSERT a46 = (4, 6);
ASSERT a46 IS_IN x;
a47 : IntPair;
ASSERT a47 = (4, 7);
ASSERT a47 IS_IN x;
a48 : IntPair;
ASSERT a48 = (4, 8);
ASSERT a48 IS_IN x;
a49 : IntPair;
ASSERT a49 = (4, 9);
ASSERT a49 IS_IN x;
a410 : IntPair;
ASSERT a410 = (4, 10);
ASSERT a410 IS_IN x;
a51 : IntPair;
ASSERT a51 = (5, 1);
ASSERT a51 IS_IN x;
a52 : IntPair;
ASSERT a52 = (5, 2);
ASSERT a52 IS_IN x;
a53 : IntPair;
ASSERT a53 = (5, 3);
ASSERT a53 IS_IN x;
a54 : IntPair;
ASSERT a54 = (5, 4);
ASSERT a54 IS_IN x;
a55 : IntPair;
ASSERT a55 = (5, 5);
ASSERT a55 IS_IN x;
a56 : IntPair;
ASSERT a56 = (5, 6);
ASSERT a56 IS_IN x;
a57 : IntPair;
ASSERT a57 = (5, 7);
ASSERT a57 IS_IN x;
a58 : IntPair;
ASSERT a58 = (5, 8);
ASSERT a58 IS_IN x;
a59 : IntPair;
ASSERT a59 = (5, 9);
ASSERT a59 IS_IN x;
a510 : IntPair;
ASSERT a510 = (5, 10);
ASSERT a510 IS_IN x;
a61 : IntPair;
ASSERT a61 = (6, 1);
ASSERT a61 IS_IN x;
a62 : IntPair;
ASSERT a62 = (6, 2);
ASSERT a62 IS_IN x;
a63 : IntPair;
ASSERT a63 = (6, 3);
ASSERT a63 IS_IN x;
a64 : IntPair;
ASSERT a64 = (6, 4);
ASSERT a64 IS_IN x;
a65 : IntPair;
ASSERT a65 = (6, 5);
ASSERT a65 IS_IN x;
a66 : IntPair;
ASSERT a66 = (6, 6);
ASSERT a66 IS_IN x;
a67 : IntPair;
ASSERT a67 = (6, 7);
ASSERT a67 IS_IN x;
a68 : IntPair;
ASSERT a68 = (6, 8);
ASSERT a68 IS_IN x;
a69 : IntPair;
ASSERT a69 = (6, 9);
ASSERT a69 IS_IN x;
a610 : IntPair;
ASSERT a610 = (6, 10);
ASSERT a610 IS_IN x;
a71 : IntPair;
ASSERT a71 = (7, 1);
ASSERT a71 IS_IN x;
a72 : IntPair;
ASSERT a72 = (7, 2);
ASSERT a72 IS_IN x;
a73 : IntPair;
ASSERT a73 = (7, 3);
ASSERT a73 IS_IN x;
a74 : IntPair;
ASSERT a74 = (7, 4);
ASSERT a74 IS_IN x;
a75 : IntPair;
ASSERT a75 = (7, 5);
ASSERT a75 IS_IN x;
a76 : IntPair;
ASSERT a76 = (7, 6);
ASSERT a76 IS_IN x;
a77 : IntPair;
ASSERT a77 = (7, 7);
ASSERT a77 IS_IN x;
a78 : IntPair;
ASSERT a78 = (7, 8);
ASSERT a78 IS_IN x;
a79 : IntPair;
ASSERT a79 = (7, 9);
ASSERT a79 IS_IN x;
a710 : IntPair;
ASSERT a710 = (7, 10);
ASSERT a710 IS_IN x;
a81 : IntPair;
ASSERT a81 = (8, 1);
ASSERT a81 IS_IN x;
a82 : IntPair;
ASSERT a82 = (8, 2);
ASSERT a82 IS_IN x;
a83 : IntPair;
ASSERT a83 = (8, 3);
ASSERT a83 IS_IN x;
a84 : IntPair;
ASSERT a84 = (8, 4);
ASSERT a84 IS_IN x;
a85 : IntPair;
ASSERT a85 = (8, 5);
ASSERT a85 IS_IN x;
a86 : IntPair;
ASSERT a86 = (8, 6);
ASSERT a86 IS_IN x;
a87 : IntPair;
ASSERT a87 = (8, 7);
ASSERT a87 IS_IN x;
a88 : IntPair;
ASSERT a88 = (8, 8);
ASSERT a88 IS_IN x;
a89 : IntPair;
ASSERT a89 = (8, 9);
ASSERT a89 IS_IN x;
a810 : IntPair;
ASSERT a810 = (8, 10);
ASSERT a810 IS_IN x;
a91 : IntPair;
ASSERT a91 = (9, 1);
ASSERT a91 IS_IN x;
a92 : IntPair;
ASSERT a92 = (9, 2);
ASSERT a92 IS_IN x;
a93 : IntPair;
ASSERT a93 = (9, 3);
ASSERT a93 IS_IN x;
a94 : IntPair;
ASSERT a94 = (9, 4);
ASSERT a94 IS_IN x;
a95 : IntPair;
ASSERT a95 = (9, 5);
ASSERT a95 IS_IN x;
a96 : IntPair;
ASSERT a96 = (9, 6);
ASSERT a96 IS_IN x;
a97 : IntPair;
ASSERT a97 = (9, 7);
ASSERT a97 IS_IN x;
a98 : IntPair;
ASSERT a98 = (9, 8);
ASSERT a98 IS_IN x;
a99 : IntPair;
ASSERT a99 = (9, 9);
ASSERT a99 IS_IN x;
a910 : IntPair;
ASSERT a910 = (9, 10);
ASSERT a910 IS_IN x;
a101 : IntPair;
ASSERT a101 = (10, 1);
ASSERT a101 IS_IN x;
a102 : IntPair;
ASSERT a102 = (10, 2);
ASSERT a102 IS_IN x;
a103 : IntPair;
ASSERT a103 = (10, 3);
ASSERT a103 IS_IN x;
a104 : IntPair;
ASSERT a104 = (10, 4);
ASSERT a104 IS_IN x;
a105 : IntPair;
ASSERT a105 = (10, 5);
ASSERT a105 IS_IN x;
a106 : IntPair;
ASSERT a106 = (10, 6);
ASSERT a106 IS_IN x;
a107 : IntPair;
ASSERT a107 = (10, 7);
ASSERT a107 IS_IN x;
a108 : IntPair;
ASSERT a108 = (10, 8);
ASSERT a108 IS_IN x;
a109 : IntPair;
ASSERT a109 = (10, 9);
ASSERT a109 IS_IN x;
a1010 : IntPair;
ASSERT a1010 = (10, 10);
ASSERT a1010 IS_IN x;
b11 : IntPair;
ASSERT b11 = (1, 1);
ASSERT b11 IS_IN y;
b12 : IntPair;
ASSERT b12 = (1, 2);
ASSERT b12 IS_IN y;
b13 : IntPair;
ASSERT b13 = (1, 3);
ASSERT b13 IS_IN y;
b14 : IntPair;
ASSERT b14 = (1, 4);
ASSERT b14 IS_IN y;
b15 : IntPair;
ASSERT b15 = (1, 5);
ASSERT b15 IS_IN y;
b16 : IntPair;
ASSERT b16 = (1, 6);
ASSERT b16 IS_IN y;
b17 : IntPair;
ASSERT b17 = (1, 7);
ASSERT b17 IS_IN y;
b18 : IntPair;
ASSERT b18 = (1, 8);
ASSERT b18 IS_IN y;
b19 : IntPair;
ASSERT b19 = (1, 9);
ASSERT b19 IS_IN y;
b110 : IntPair;
ASSERT b110 = (1, 10);
ASSERT b110 IS_IN y;
b21 : IntPair;
ASSERT b21 = (2, 1);
ASSERT b21 IS_IN y;
b22 : IntPair;
ASSERT b22 = (2, 2);
ASSERT b22 IS_IN y;
b23 : IntPair;
ASSERT b23 = (2, 3);
ASSERT b23 IS_IN y;
b24 : IntPair;
ASSERT b24 = (2, 4);
ASSERT b24 IS_IN y;
b25 : IntPair;
ASSERT b25 = (2, 5);
ASSERT b25 IS_IN y;
b26 : IntPair;
ASSERT b26 = (2, 6);
ASSERT b26 IS_IN y;
b27 : IntPair;
ASSERT b27 = (2, 7);
ASSERT b27 IS_IN y;
b28 : IntPair;
ASSERT b28 = (2, 8);
ASSERT b28 IS_IN y;
b29 : IntPair;
ASSERT b29 = (2, 9);
ASSERT b29 IS_IN y;
b210 : IntPair;
ASSERT b210 = (2, 10);
ASSERT b210 IS_IN y;
b31 : IntPair;
ASSERT b31 = (3, 1);
ASSERT b31 IS_IN y;
b32 : IntPair;
ASSERT b32 = (3, 2);
ASSERT b32 IS_IN y;
b33 : IntPair;
ASSERT b33 = (3, 3);
ASSERT b33 IS_IN y;
b34 : IntPair;
ASSERT b34 = (3, 4);
ASSERT b34 IS_IN y;
b35 : IntPair;
ASSERT b35 = (3, 5);
ASSERT b35 IS_IN y;
b36 : IntPair;
ASSERT b36 = (3, 6);
ASSERT b36 IS_IN y;
b37 : IntPair;
ASSERT b37 = (3, 7);
ASSERT b37 IS_IN y;
b38 : IntPair;
ASSERT b38 = (3, 8);
ASSERT b38 IS_IN y;
b39 : IntPair;
ASSERT b39 = (3, 9);
ASSERT b39 IS_IN y;
b310 : IntPair;
ASSERT b310 = (3, 10);
ASSERT b310 IS_IN y;
b41 : IntPair;
ASSERT b41 = (4, 1);
ASSERT b41 IS_IN y;
b42 : IntPair;
ASSERT b42 = (4, 2);
ASSERT b42 IS_IN y;
b43 : IntPair;
ASSERT b43 = (4, 3);
ASSERT b43 IS_IN y;
b44 : IntPair;
ASSERT b44 = (4, 4);
ASSERT b44 IS_IN y;
b45 : IntPair;
ASSERT b45 = (4, 5);
ASSERT b45 IS_IN y;
b46 : IntPair;
ASSERT b46 = (4, 6);
ASSERT b46 IS_IN y;
b47 : IntPair;
ASSERT b47 = (4, 7);
ASSERT b47 IS_IN y;
b48 : IntPair;
ASSERT b48 = (4, 8);
ASSERT b48 IS_IN y;
b49 : IntPair;
ASSERT b49 = (4, 9);
ASSERT b49 IS_IN y;
b410 : IntPair;
ASSERT b410 = (4, 10);
ASSERT b410 IS_IN y;
b51 : IntPair;
ASSERT b51 = (5, 1);
ASSERT b51 IS_IN y;
b52 : IntPair;
ASSERT b52 = (5, 2);
ASSERT b52 IS_IN y;
b53 : IntPair;
ASSERT b53 = (5, 3);
ASSERT b53 IS_IN y;
b54 : IntPair;
ASSERT b54 = (5, 4);
ASSERT b54 IS_IN y;
b55 : IntPair;
ASSERT b55 = (5, 5);
ASSERT b55 IS_IN y;
b56 : IntPair;
ASSERT b56 = (5, 6);
ASSERT b56 IS_IN y;
b57 : IntPair;
ASSERT b57 = (5, 7);
ASSERT b57 IS_IN y;
b58 : IntPair;
ASSERT b58 = (5, 8);
ASSERT b58 IS_IN y;
b59 : IntPair;
ASSERT b59 = (5, 9);
ASSERT b59 IS_IN y;
b510 : IntPair;
ASSERT b510 = (5, 10);
ASSERT b510 IS_IN y;
b61 : IntPair;
ASSERT b61 = (6, 1);
ASSERT b61 IS_IN y;
b62 : IntPair;
ASSERT b62 = (6, 2);
ASSERT b62 IS_IN y;
b63 : IntPair;
ASSERT b63 = (6, 3);
ASSERT b63 IS_IN y;
b64 : IntPair;
ASSERT b64 = (6, 4);
ASSERT b64 IS_IN y;
b65 : IntPair;
ASSERT b65 = (6, 5);
ASSERT b65 IS_IN y;
b66 : IntPair;
ASSERT b66 = (6, 6);
ASSERT b66 IS_IN y;
b67 : IntPair;
ASSERT b67 = (6, 7);
ASSERT b67 IS_IN y;
b68 : IntPair;
ASSERT b68 = (6, 8);
ASSERT b68 IS_IN y;
b69 : IntPair;
ASSERT b69 = (6, 9);
ASSERT b69 IS_IN y;
b610 : IntPair;
ASSERT b610 = (6, 10);
ASSERT b610 IS_IN y;
b71 : IntPair;
ASSERT b71 = (7, 1);
ASSERT b71 IS_IN y;
b72 : IntPair;
ASSERT b72 = (7, 2);
ASSERT b72 IS_IN y;
b73 : IntPair;
ASSERT b73 = (7, 3);
ASSERT b73 IS_IN y;
b74 : IntPair;
ASSERT b74 = (7, 4);
ASSERT b74 IS_IN y;
b75 : IntPair;
ASSERT b75 = (7, 5);
ASSERT b75 IS_IN y;
b76 : IntPair;
ASSERT b76 = (7, 6);
ASSERT b76 IS_IN y;
b77 : IntPair;
ASSERT b77 = (7, 7);
ASSERT b77 IS_IN y;
b78 : IntPair;
ASSERT b78 = (7, 8);
ASSERT b78 IS_IN y;
b79 : IntPair;
ASSERT b79 = (7, 9);
ASSERT b79 IS_IN y;
b710 : IntPair;
ASSERT b710 = (7, 10);
ASSERT b710 IS_IN y;
b81 : IntPair;
ASSERT b81 = (8, 1);
ASSERT b81 IS_IN y;
b82 : IntPair;
ASSERT b82 = (8, 2);
ASSERT b82 IS_IN y;
b83 : IntPair;
ASSERT b83 = (8, 3);
ASSERT b83 IS_IN y;
b84 : IntPair;
ASSERT b84 = (8, 4);
ASSERT b84 IS_IN y;
b85 : IntPair;
ASSERT b85 = (8, 5);
ASSERT b85 IS_IN y;
b86 : IntPair;
ASSERT b86 = (8, 6);
ASSERT b86 IS_IN y;
b87 : IntPair;
ASSERT b87 = (8, 7);
ASSERT b87 IS_IN y;
b88 : IntPair;
ASSERT b88 = (8, 8);
ASSERT b88 IS_IN y;
b89 : IntPair;
ASSERT b89 = (8, 9);
ASSERT b89 IS_IN y;
b810 : IntPair;
ASSERT b810 = (8, 10);
ASSERT b810 IS_IN y;
b91 : IntPair;
ASSERT b91 = (9, 1);
ASSERT b91 IS_IN y;
b92 : IntPair;
ASSERT b92 = (9, 2);
ASSERT b92 IS_IN y;
b93 : IntPair;
ASSERT b93 = (9, 3);
ASSERT b93 IS_IN y;
b94 : IntPair;
ASSERT b94 = (9, 4);
ASSERT b94 IS_IN y;
b95 : IntPair;
ASSERT b95 = (9, 5);
ASSERT b95 IS_IN y;
b96 : IntPair;
ASSERT b96 = (9, 6);
ASSERT b96 IS_IN y;
b97 : IntPair;
ASSERT b97 = (9, 7);
ASSERT b97 IS_IN y;
b98 : IntPair;
ASSERT b98 = (9, 8);
ASSERT b98 IS_IN y;
b99 : IntPair;
ASSERT b99 = (9, 9);
ASSERT b99 IS_IN y;
b910 : IntPair;
ASSERT b910 = (9, 10);
ASSERT b910 IS_IN y;
b101 : IntPair;
ASSERT b101 = (10, 1);
ASSERT b101 IS_IN y;
b102 : IntPair;
ASSERT b102 = (10, 2);
ASSERT b102 IS_IN y;
b103 : IntPair;
ASSERT b103 = (10, 3);
ASSERT b103 IS_IN y;
b104 : IntPair;
ASSERT b104 = (10, 4);
ASSERT b104 IS_IN y;
b105 : IntPair;
ASSERT b105 = (10, 5);
ASSERT b105 IS_IN y;
b106 : IntPair;
ASSERT b106 = (10, 6);
ASSERT b106 IS_IN y;
b107 : IntPair;
ASSERT b107 = (10, 7);
ASSERT b107 IS_IN y;
b108 : IntPair;
ASSERT b108 = (10, 8);
ASSERT b108 IS_IN y;
b109 : IntPair;
ASSERT b109 = (10, 9);
ASSERT b109 IS_IN y;
b1010 : IntPair;
ASSERT b1010 = (10, 10);
ASSERT b1010 IS_IN y;

ASSERT (1, 9) IS_IN z;

a : IntPair;
ASSERT a = (9,1);
ASSERT r = ((TRANSPOSE(x) JOIN y) JOIN z);
ASSERT NOT (a IS_IN TRANSPOSE(r));

CHECKSAT;