c forge.problem sat
p cnf 27 137
-5 21 22 0
-25 13 0
-9 27 -20 0
-9 -23 -27 0
8 -7 0
-2 19 -17 0
4 -8 0
23 15 0
6 27 0
-19 9 13 0
-18 12 0
-7 16 0
17 -5 0
-12 18 0
27 17 0
-20 19 0
-27 -7 9 0
6 -19 -12 0
18 -24 0
27 9 -22 0
21 9 3 8 0
9 -4 8 0
-26 3 0
25 23 27 0
-9 -19 20 -27 0
-22 15 10 0
9 -21 27 0
2 18 0
21 -10 22 0
-22 23 5 0
25 27 14 0
27 12 0
-19 17 0
9 11 27 0
-16 7 0
27 -2 0
-27 -25 0
-23 27 9 0
1 11 0
-27 9 -20 0
8 9 21 1 0
-20 13 0
-19 -22 0
3 4 0
10 24 0
2 4 0
27 19 25 0
9 20 27 0
19 -11 9 0
22 1 19 27 0
-26 19 0
-8 -9 27 0
-14 -9 -27 0
25 9 27 0
1 9 27 0
-18 24 -19 0
-22 -1 -11 0
2 -27 0
-19 -25 0
3 21 8 27 0
18 27 0
-27 -22 -9 0
-3 19 27 0
2 -8 1 0
15 10 -21 0
-1 8 -4 -3 0
-8 7 0
8 1 21 27 0
6 -22 0
2 3 -8 0
27 13 0
27 19 -11 0
6 -24 19 0
-21 23 5 0
4 -27 -9 0
9 -27 -8 0
-19 3 0
27 19 9 0
27 24 0
-1 -26 -11 0
10 15 -5 0
-23 -15 0
-24 -5 19 0
-25 -26 0
26 -22 0
24 -19 -12 0
-4 -1 -2 -3 0
-2 5 -17 -6 0
-12 -2 0
-19 26 0
-27 -10 0
-15 6 0
19 12 -17 0
-20 -25 0
-25 10 0
-23 -25 0
12 2 0
23 -27 9 0
-25 16 0
27 10 0
-24 13 -10 0
9 14 0
-14 -25 -9 0
19 23 9 0
-10 23 5 0
6 -21 0
-7 27 -9 0
8 -9 -27 0
11 -27 -9 0
-8 -21 0
-6 -17 5 12 0
-3 -27 -4 -1 0
-27 -13 0
25 -16 0
22 -6 15 21 0
3 -27 -9 0
17 -12 0
3 9 27 0
19 9 -3 0
-5 27 0
-23 -5 0
26 1 0
-19 -16 0
9 27 4 0
-21 -3 -1 0
-10 -15 0
-27 -9 -21 0
6 17 0
-12 -19 -5 0
19 9 1 22 0
24 -13 0
-6 -17 5 19 -27 0
-6 24 -18 5 0
27 19 16 0
-19 11 0
27 9 8 0
1 4 0