402 lines
4.3 KiB
Plaintext
402 lines
4.3 KiB
Plaintext
|
p cnf 149 400
|
||
|
-17 1 0
|
||
|
-17 -2 0
|
||
|
-1 2 17 0
|
||
|
-18 -1 0
|
||
|
-18 2 0
|
||
|
1 -2 18 0
|
||
|
-19 -17 0
|
||
|
-19 -18 0
|
||
|
17 18 19 0
|
||
|
-20 3 0
|
||
|
-20 4 0
|
||
|
-3 -4 20 0
|
||
|
-21 5 0
|
||
|
-21 6 0
|
||
|
-5 -6 21 0
|
||
|
-22 -3 0
|
||
|
-22 -4 0
|
||
|
3 4 22 0
|
||
|
-23 21 0
|
||
|
-23 -22 0
|
||
|
-21 22 23 0
|
||
|
-24 -20 0
|
||
|
-24 -23 0
|
||
|
20 23 24 0
|
||
|
-25 -19 0
|
||
|
-25 -24 0
|
||
|
19 24 25 0
|
||
|
-26 19 0
|
||
|
-26 24 0
|
||
|
-19 -24 26 0
|
||
|
-27 -25 0
|
||
|
-27 -26 0
|
||
|
25 26 27 0
|
||
|
-28 3 0
|
||
|
-28 -4 0
|
||
|
-3 4 28 0
|
||
|
-29 -3 0
|
||
|
-29 4 0
|
||
|
3 -4 29 0
|
||
|
-30 -28 0
|
||
|
-30 -29 0
|
||
|
28 29 30 0
|
||
|
-31 21 0
|
||
|
-31 -30 0
|
||
|
-21 30 31 0
|
||
|
-32 -20 0
|
||
|
-32 -31 0
|
||
|
20 31 32 0
|
||
|
-33 -19 0
|
||
|
-33 -32 0
|
||
|
19 32 33 0
|
||
|
-34 19 0
|
||
|
-34 32 0
|
||
|
-19 -32 34 0
|
||
|
-35 -33 0
|
||
|
-35 -34 0
|
||
|
33 34 35 0
|
||
|
-36 27 0
|
||
|
-36 -35 0
|
||
|
-27 35 36 0
|
||
|
-37 -27 0
|
||
|
-37 35 0
|
||
|
27 -35 37 0
|
||
|
-38 -36 0
|
||
|
-38 -37 0
|
||
|
36 37 38 0
|
||
|
-39 7 0
|
||
|
-39 -8 0
|
||
|
-7 8 39 0
|
||
|
-40 -7 0
|
||
|
-40 8 0
|
||
|
7 -8 40 0
|
||
|
-41 -39 0
|
||
|
-41 -40 0
|
||
|
39 40 41 0
|
||
|
-42 1 0
|
||
|
-42 2 0
|
||
|
-1 -2 42 0
|
||
|
-43 -1 0
|
||
|
-43 -2 0
|
||
|
1 2 43 0
|
||
|
-44 -43 0
|
||
|
-44 -24 0
|
||
|
43 24 44 0
|
||
|
-45 -42 0
|
||
|
-45 -44 0
|
||
|
42 44 45 0
|
||
|
-46 -41 0
|
||
|
-46 -45 0
|
||
|
41 45 46 0
|
||
|
-47 41 0
|
||
|
-47 45 0
|
||
|
-41 -45 47 0
|
||
|
-48 -46 0
|
||
|
-48 -47 0
|
||
|
46 47 48 0
|
||
|
-49 -42 0
|
||
|
-49 -33 0
|
||
|
42 33 49 0
|
||
|
-50 -41 0
|
||
|
-50 -49 0
|
||
|
41 49 50 0
|
||
|
-51 41 0
|
||
|
-51 49 0
|
||
|
-41 -49 51 0
|
||
|
-52 -50 0
|
||
|
-52 -51 0
|
||
|
50 51 52 0
|
||
|
-53 48 0
|
||
|
-53 -52 0
|
||
|
-48 52 53 0
|
||
|
-54 -48 0
|
||
|
-54 52 0
|
||
|
48 -52 54 0
|
||
|
-55 -53 0
|
||
|
-55 -54 0
|
||
|
53 54 55 0
|
||
|
-56 38 0
|
||
|
-56 55 0
|
||
|
-38 -55 56 0
|
||
|
-57 9 0
|
||
|
-57 -10 0
|
||
|
-9 10 57 0
|
||
|
-58 -9 0
|
||
|
-58 10 0
|
||
|
9 -10 58 0
|
||
|
-59 -57 0
|
||
|
-59 -58 0
|
||
|
57 58 59 0
|
||
|
-60 7 0
|
||
|
-60 8 0
|
||
|
-7 -8 60 0
|
||
|
-61 -7 0
|
||
|
-61 -8 0
|
||
|
7 8 61 0
|
||
|
-62 42 0
|
||
|
-62 -61 0
|
||
|
-42 61 62 0
|
||
|
-63 -60 0
|
||
|
-63 -62 0
|
||
|
60 62 63 0
|
||
|
-64 -43 0
|
||
|
-64 -61 0
|
||
|
43 61 64 0
|
||
|
-65 -24 0
|
||
|
-65 64 0
|
||
|
24 -64 65 0
|
||
|
-66 63 0
|
||
|
-66 -65 0
|
||
|
-63 65 66 0
|
||
|
-67 -59 0
|
||
|
-67 -66 0
|
||
|
59 66 67 0
|
||
|
-68 59 0
|
||
|
-68 66 0
|
||
|
-59 -66 68 0
|
||
|
-69 -67 0
|
||
|
-69 -68 0
|
||
|
67 68 69 0
|
||
|
-70 -60 0
|
||
|
-70 -50 0
|
||
|
60 50 70 0
|
||
|
-71 -59 0
|
||
|
-71 -70 0
|
||
|
59 70 71 0
|
||
|
-72 59 0
|
||
|
-72 70 0
|
||
|
-59 -70 72 0
|
||
|
-73 -71 0
|
||
|
-73 -72 0
|
||
|
71 72 73 0
|
||
|
-74 69 0
|
||
|
-74 -73 0
|
||
|
-69 73 74 0
|
||
|
-75 -69 0
|
||
|
-75 73 0
|
||
|
69 -73 75 0
|
||
|
-76 -74 0
|
||
|
-76 -75 0
|
||
|
74 75 76 0
|
||
|
-77 56 0
|
||
|
-77 76 0
|
||
|
-56 -76 77 0
|
||
|
-78 11 0
|
||
|
-78 -12 0
|
||
|
-11 12 78 0
|
||
|
-79 -11 0
|
||
|
-79 12 0
|
||
|
11 -12 79 0
|
||
|
-80 -78 0
|
||
|
-80 -79 0
|
||
|
78 79 80 0
|
||
|
-81 9 0
|
||
|
-81 10 0
|
||
|
-9 -10 81 0
|
||
|
-82 -9 0
|
||
|
-82 -10 0
|
||
|
9 10 82 0
|
||
|
-83 -82 0
|
||
|
-83 -66 0
|
||
|
82 66 83 0
|
||
|
-84 -81 0
|
||
|
-84 -83 0
|
||
|
81 83 84 0
|
||
|
-85 -80 0
|
||
|
-85 -84 0
|
||
|
80 84 85 0
|
||
|
-86 80 0
|
||
|
-86 84 0
|
||
|
-80 -84 86 0
|
||
|
-87 -85 0
|
||
|
-87 -86 0
|
||
|
85 86 87 0
|
||
|
-88 -81 0
|
||
|
-88 -71 0
|
||
|
81 71 88 0
|
||
|
-89 -80 0
|
||
|
-89 -88 0
|
||
|
80 88 89 0
|
||
|
-90 80 0
|
||
|
-90 88 0
|
||
|
-80 -88 90 0
|
||
|
-91 -89 0
|
||
|
-91 -90 0
|
||
|
89 90 91 0
|
||
|
-92 87 0
|
||
|
-92 -91 0
|
||
|
-87 91 92 0
|
||
|
-93 -87 0
|
||
|
-93 91 0
|
||
|
87 -91 93 0
|
||
|
-94 -92 0
|
||
|
-94 -93 0
|
||
|
92 93 94 0
|
||
|
-95 77 0
|
||
|
-95 94 0
|
||
|
-77 -94 95 0
|
||
|
-96 13 0
|
||
|
-96 -14 0
|
||
|
-13 14 96 0
|
||
|
-97 -13 0
|
||
|
-97 14 0
|
||
|
13 -14 97 0
|
||
|
-98 -96 0
|
||
|
-98 -97 0
|
||
|
96 97 98 0
|
||
|
-99 11 0
|
||
|
-99 12 0
|
||
|
-11 -12 99 0
|
||
|
-100 -11 0
|
||
|
-100 -12 0
|
||
|
11 12 100 0
|
||
|
-101 81 0
|
||
|
-101 -100 0
|
||
|
-81 100 101 0
|
||
|
-102 -99 0
|
||
|
-102 -101 0
|
||
|
99 101 102 0
|
||
|
-103 -82 0
|
||
|
-103 -100 0
|
||
|
82 100 103 0
|
||
|
-104 -66 0
|
||
|
-104 103 0
|
||
|
66 -103 104 0
|
||
|
-105 102 0
|
||
|
-105 -104 0
|
||
|
-102 104 105 0
|
||
|
-106 -98 0
|
||
|
-106 -105 0
|
||
|
98 105 106 0
|
||
|
-107 98 0
|
||
|
-107 105 0
|
||
|
-98 -105 107 0
|
||
|
-108 -106 0
|
||
|
-108 -107 0
|
||
|
106 107 108 0
|
||
|
-109 -99 0
|
||
|
-109 -89 0
|
||
|
99 89 109 0
|
||
|
-110 -98 0
|
||
|
-110 -109 0
|
||
|
98 109 110 0
|
||
|
-111 98 0
|
||
|
-111 109 0
|
||
|
-98 -109 111 0
|
||
|
-112 -110 0
|
||
|
-112 -111 0
|
||
|
110 111 112 0
|
||
|
-113 108 0
|
||
|
-113 -112 0
|
||
|
-108 112 113 0
|
||
|
-114 -108 0
|
||
|
-114 112 0
|
||
|
108 -112 114 0
|
||
|
-115 -113 0
|
||
|
-115 -114 0
|
||
|
113 114 115 0
|
||
|
-116 95 0
|
||
|
-116 115 0
|
||
|
-95 -115 116 0
|
||
|
-117 15 0
|
||
|
-117 -16 0
|
||
|
-15 16 117 0
|
||
|
-118 -15 0
|
||
|
-118 16 0
|
||
|
15 -16 118 0
|
||
|
-119 -117 0
|
||
|
-119 -118 0
|
||
|
117 118 119 0
|
||
|
-120 13 0
|
||
|
-120 14 0
|
||
|
-13 -14 120 0
|
||
|
-121 -13 0
|
||
|
-121 -14 0
|
||
|
13 14 121 0
|
||
|
-122 -121 0
|
||
|
-122 -105 0
|
||
|
121 105 122 0
|
||
|
-123 -120 0
|
||
|
-123 -122 0
|
||
|
120 122 123 0
|
||
|
-124 -119 0
|
||
|
-124 -123 0
|
||
|
119 123 124 0
|
||
|
-125 119 0
|
||
|
-125 123 0
|
||
|
-119 -123 125 0
|
||
|
-126 -124 0
|
||
|
-126 -125 0
|
||
|
124 125 126 0
|
||
|
-127 -120 0
|
||
|
-127 -110 0
|
||
|
120 110 127 0
|
||
|
-128 -119 0
|
||
|
-128 -127 0
|
||
|
119 127 128 0
|
||
|
-129 119 0
|
||
|
-129 127 0
|
||
|
-119 -127 129 0
|
||
|
-130 -128 0
|
||
|
-130 -129 0
|
||
|
128 129 130 0
|
||
|
-131 126 0
|
||
|
-131 -130 0
|
||
|
-126 130 131 0
|
||
|
-132 -126 0
|
||
|
-132 130 0
|
||
|
126 -130 132 0
|
||
|
-133 -131 0
|
||
|
-133 -132 0
|
||
|
131 132 133 0
|
||
|
-134 116 0
|
||
|
-134 133 0
|
||
|
-116 -133 134 0
|
||
|
-135 15 0
|
||
|
-135 16 0
|
||
|
-15 -16 135 0
|
||
|
-136 -15 0
|
||
|
-136 -16 0
|
||
|
15 16 136 0
|
||
|
-137 120 0
|
||
|
-137 -136 0
|
||
|
-120 136 137 0
|
||
|
-138 -135 0
|
||
|
-138 -137 0
|
||
|
135 137 138 0
|
||
|
-139 -121 0
|
||
|
-139 -136 0
|
||
|
121 136 139 0
|
||
|
-140 -102 0
|
||
|
-140 139 0
|
||
|
102 -139 140 0
|
||
|
-141 138 0
|
||
|
-141 -140 0
|
||
|
-138 140 141 0
|
||
|
-142 103 0
|
||
|
-142 139 0
|
||
|
-103 -139 142 0
|
||
|
-143 -66 0
|
||
|
-143 142 0
|
||
|
66 -142 143 0
|
||
|
-144 141 0
|
||
|
-144 -143 0
|
||
|
-141 143 144 0
|
||
|
-145 -135 0
|
||
|
-145 -128 0
|
||
|
135 128 145 0
|
||
|
-146 -144 0
|
||
|
-146 145 0
|
||
|
144 -145 146 0
|
||
|
-147 144 0
|
||
|
-147 -145 0
|
||
|
-144 145 147 0
|
||
|
-148 -146 0
|
||
|
-148 -147 0
|
||
|
146 147 148 0
|
||
|
-149 134 0
|
||
|
-149 148 0
|
||
|
-134 -148 149 0
|
||
|
-149 0
|