180 lines
1.7 KiB
Plaintext
180 lines
1.7 KiB
Plaintext
|
p cnf 65 178
|
||
|
-7 -2 0
|
||
|
-7 -3 0
|
||
|
2 3 7 0
|
||
|
-8 1 0
|
||
|
-8 7 0
|
||
|
-1 -7 8 0
|
||
|
-9 -5 0
|
||
|
-9 -6 0
|
||
|
5 6 9 0
|
||
|
-10 4 0
|
||
|
-10 9 0
|
||
|
-4 -9 10 0
|
||
|
-11 -8 0
|
||
|
-11 -10 0
|
||
|
8 10 11 0
|
||
|
-12 1 0
|
||
|
-12 4 0
|
||
|
-1 -4 12 0
|
||
|
-13 1 0
|
||
|
-13 6 0
|
||
|
-1 -6 13 0
|
||
|
-14 3 0
|
||
|
-14 4 0
|
||
|
-3 -4 14 0
|
||
|
-15 13 0
|
||
|
-15 14 0
|
||
|
-13 -14 15 0
|
||
|
-16 -13 0
|
||
|
-16 -14 0
|
||
|
13 14 16 0
|
||
|
-17 -15 0
|
||
|
-17 -16 0
|
||
|
15 16 17 0
|
||
|
-18 2 0
|
||
|
-18 4 0
|
||
|
-2 -4 18 0
|
||
|
-19 1 0
|
||
|
-19 5 0
|
||
|
-1 -5 19 0
|
||
|
-20 3 0
|
||
|
-20 6 0
|
||
|
-3 -6 20 0
|
||
|
-21 20 0
|
||
|
-21 -15 0
|
||
|
-20 15 21 0
|
||
|
-22 -20 0
|
||
|
-22 15 0
|
||
|
20 -15 22 0
|
||
|
-23 -21 0
|
||
|
-23 -22 0
|
||
|
21 22 23 0
|
||
|
-24 19 0
|
||
|
-24 -23 0
|
||
|
-19 23 24 0
|
||
|
-25 -19 0
|
||
|
-25 23 0
|
||
|
19 -23 25 0
|
||
|
-26 -24 0
|
||
|
-26 -25 0
|
||
|
24 25 26 0
|
||
|
-27 18 0
|
||
|
-27 26 0
|
||
|
-18 -26 27 0
|
||
|
-28 -18 0
|
||
|
-28 -26 0
|
||
|
18 26 28 0
|
||
|
-29 -27 0
|
||
|
-29 -28 0
|
||
|
27 28 29 0
|
||
|
-30 3 0
|
||
|
-30 5 0
|
||
|
-3 -5 30 0
|
||
|
-31 -19 0
|
||
|
-31 -20 0
|
||
|
19 20 31 0
|
||
|
-32 15 0
|
||
|
-32 -31 0
|
||
|
-15 31 32 0
|
||
|
-33 19 0
|
||
|
-33 20 0
|
||
|
-19 -20 33 0
|
||
|
-34 -32 0
|
||
|
-34 -33 0
|
||
|
32 33 34 0
|
||
|
-35 30 0
|
||
|
-35 -34 0
|
||
|
-30 34 35 0
|
||
|
-36 -30 0
|
||
|
-36 34 0
|
||
|
30 -34 36 0
|
||
|
-37 -35 0
|
||
|
-37 -36 0
|
||
|
35 36 37 0
|
||
|
-38 2 0
|
||
|
-38 6 0
|
||
|
-2 -6 38 0
|
||
|
-39 38 0
|
||
|
-39 -27 0
|
||
|
-38 27 39 0
|
||
|
-40 -38 0
|
||
|
-40 27 0
|
||
|
38 -27 40 0
|
||
|
-41 -39 0
|
||
|
-41 -40 0
|
||
|
39 40 41 0
|
||
|
-42 37 0
|
||
|
-42 -41 0
|
||
|
-37 41 42 0
|
||
|
-43 -37 0
|
||
|
-43 41 0
|
||
|
37 -41 43 0
|
||
|
-44 -42 0
|
||
|
-44 -43 0
|
||
|
42 43 44 0
|
||
|
-45 -38 0
|
||
|
-45 -37 0
|
||
|
38 37 45 0
|
||
|
-46 27 0
|
||
|
-46 -45 0
|
||
|
-27 45 46 0
|
||
|
-47 38 0
|
||
|
-47 37 0
|
||
|
-38 -37 47 0
|
||
|
-48 -46 0
|
||
|
-48 -47 0
|
||
|
46 47 48 0
|
||
|
-49 2 0
|
||
|
-49 5 0
|
||
|
-2 -5 49 0
|
||
|
-50 -49 0
|
||
|
-50 -35 0
|
||
|
49 35 50 0
|
||
|
-51 -48 0
|
||
|
-51 -50 0
|
||
|
48 50 51 0
|
||
|
-52 49 0
|
||
|
-52 35 0
|
||
|
-49 -35 52 0
|
||
|
-53 -51 0
|
||
|
-53 -52 0
|
||
|
51 52 53 0
|
||
|
-54 49 0
|
||
|
-54 48 0
|
||
|
-49 -48 54 0
|
||
|
-55 -49 0
|
||
|
-55 -48 0
|
||
|
49 48 55 0
|
||
|
-56 -54 0
|
||
|
-56 -55 0
|
||
|
54 55 56 0
|
||
|
-57 35 0
|
||
|
-57 -56 0
|
||
|
-35 56 57 0
|
||
|
-58 -35 0
|
||
|
-58 56 0
|
||
|
35 -56 58 0
|
||
|
-59 -57 0
|
||
|
-59 -58 0
|
||
|
57 58 59 0
|
||
|
-60 53 0
|
||
|
-60 -59 0
|
||
|
-53 59 60 0
|
||
|
-61 44 0
|
||
|
-61 60 0
|
||
|
-44 -60 61 0
|
||
|
-62 -29 0
|
||
|
-62 61 0
|
||
|
29 -61 62 0
|
||
|
-63 -17 0
|
||
|
-63 62 0
|
||
|
17 -62 63 0
|
||
|
-64 12 0
|
||
|
-64 63 0
|
||
|
-12 -63 64 0
|
||
|
-65 11 0
|
||
|
-65 64 0
|
||
|
-11 -64 65 0
|
||
|
65 0
|