c 1 = x@1
c 2 = x@0
c 3 = y@1
c 4 = y@0
p cnf 20 49
-5 -1 0
-5 2 0
1 -2 5 0
-6 -3 0
-6 4 0
3 -4 6 0
-7 -5 0
-7 -6 0
5 6 7 0
-8 2 0
-8 4 0
-2 -4 8 0
-9 2 0
-9 3 0
-2 -3 9 0
-10 1 0
-10 4 0
-1 -4 10 0
-11 9 0
-11 10 0
-9 -10 11 0
-12 -9 0
-12 -10 0
9 10 12 0
-13 -11 0
-13 -12 0
11 12 13 0
-14 1 0
-14 3 0
-1 -3 14 0
-15 14 0
-15 11 0
-14 -11 15 0
-16 -14 0
-16 -11 0
14 11 16 0
-17 -15 0
-17 -16 0
15 16 17 0
-18 -13 0
-18 17 0
13 -17 18 0
-19 -8 0
-19 18 0
8 -18 19 0
-20 7 0
-20 19 0
-7 -19 20 0
20 0