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