2023-03-21 08:36:53 +00:00
|
|
|
p cnf 196 514
|
|
|
|
-37 -1 0
|
|
|
|
37 1 0
|
|
|
|
-38 -2 0
|
|
|
|
38 2 0
|
|
|
|
-39 -4 0
|
|
|
|
39 4 0
|
|
|
|
-40 -6 0
|
|
|
|
40 6 0
|
|
|
|
-41 -8 0
|
|
|
|
41 8 0
|
|
|
|
-42 -10 0
|
|
|
|
42 10 0
|
|
|
|
-43 -12 0
|
|
|
|
43 12 0
|
|
|
|
-44 -14 0
|
|
|
|
44 14 0
|
|
|
|
-45 -16 0
|
|
|
|
45 16 0
|
|
|
|
-46 -18 0
|
|
|
|
46 18 0
|
|
|
|
-47 -20 0
|
|
|
|
47 20 0
|
|
|
|
-48 -22 0
|
|
|
|
48 22 0
|
|
|
|
-49 -24 0
|
|
|
|
49 24 0
|
|
|
|
-50 -26 0
|
|
|
|
50 26 0
|
|
|
|
-51 -28 0
|
|
|
|
51 28 0
|
|
|
|
-52 -30 0
|
|
|
|
52 30 0
|
|
|
|
-53 -32 0
|
|
|
|
53 32 0
|
|
|
|
-54 -34 0
|
|
|
|
54 34 0
|
|
|
|
55 37 0
|
|
|
|
55 2 0
|
|
|
|
-37 -2 -55 0
|
|
|
|
3 38 56 0
|
|
|
|
-56 -3 0
|
|
|
|
-56 -38 0
|
|
|
|
5 38 57 0
|
|
|
|
-57 -5 0
|
|
|
|
-57 -38 0
|
|
|
|
58 39 0
|
|
|
|
58 6 0
|
|
|
|
-39 -6 -58 0
|
|
|
|
61 41 0
|
|
|
|
61 10 0
|
|
|
|
-41 -10 -61 0
|
|
|
|
64 43 0
|
|
|
|
64 14 0
|
|
|
|
-43 -14 -64 0
|
|
|
|
67 45 0
|
|
|
|
67 18 0
|
|
|
|
-45 -18 -67 0
|
|
|
|
70 47 0
|
|
|
|
70 22 0
|
|
|
|
-47 -22 -70 0
|
|
|
|
73 49 0
|
|
|
|
73 26 0
|
|
|
|
-49 -26 -73 0
|
|
|
|
76 51 0
|
|
|
|
76 30 0
|
|
|
|
-51 -30 -76 0
|
|
|
|
79 53 0
|
|
|
|
79 34 0
|
|
|
|
-53 -34 -79 0
|
|
|
|
7 40 59 0
|
|
|
|
-59 -7 0
|
|
|
|
-59 -40 0
|
|
|
|
9 40 60 0
|
|
|
|
-60 -9 0
|
|
|
|
-60 -40 0
|
|
|
|
11 42 62 0
|
|
|
|
-62 -11 0
|
|
|
|
-62 -42 0
|
|
|
|
13 42 63 0
|
|
|
|
-63 -13 0
|
|
|
|
-63 -42 0
|
|
|
|
15 44 65 0
|
|
|
|
-65 -15 0
|
|
|
|
-65 -44 0
|
|
|
|
17 44 66 0
|
|
|
|
-66 -17 0
|
|
|
|
-66 -44 0
|
|
|
|
19 46 68 0
|
|
|
|
-68 -19 0
|
|
|
|
-68 -46 0
|
|
|
|
21 46 69 0
|
|
|
|
-69 -21 0
|
|
|
|
-69 -46 0
|
|
|
|
23 48 71 0
|
|
|
|
-71 -23 0
|
|
|
|
-71 -48 0
|
|
|
|
25 48 72 0
|
|
|
|
-72 -25 0
|
|
|
|
-72 -48 0
|
|
|
|
27 50 74 0
|
|
|
|
-74 -27 0
|
|
|
|
-74 -50 0
|
|
|
|
29 50 75 0
|
|
|
|
-75 -29 0
|
|
|
|
-75 -50 0
|
|
|
|
31 52 77 0
|
|
|
|
-77 -31 0
|
|
|
|
-77 -52 0
|
|
|
|
33 52 78 0
|
|
|
|
-78 -33 0
|
|
|
|
-78 -52 0
|
|
|
|
35 54 80 0
|
|
|
|
-80 -35 0
|
|
|
|
-80 -54 0
|
|
|
|
36 54 81 0
|
|
|
|
-81 -36 0
|
|
|
|
-81 -54 0
|
|
|
|
-82 55 0
|
|
|
|
-82 58 0
|
|
|
|
-82 61 0
|
|
|
|
-82 64 0
|
|
|
|
-82 67 0
|
|
|
|
-82 70 0
|
|
|
|
-82 73 0
|
|
|
|
-82 76 0
|
|
|
|
-82 79 0
|
|
|
|
-55 -58 -61 -64 -67 -70 -73 -76 -79 82 0
|
|
|
|
-83 -82 0
|
|
|
|
83 82 0
|
|
|
|
-84 -82 0
|
|
|
|
84 82 0
|
|
|
|
-85 -82 0
|
|
|
|
85 82 0
|
|
|
|
-86 -83 -55 0
|
|
|
|
-86 83 55 0
|
|
|
|
86 -83 55 0
|
|
|
|
86 83 -55 0
|
|
|
|
-87 -83 -58 0
|
|
|
|
-87 83 58 0
|
|
|
|
87 -83 58 0
|
|
|
|
87 83 -58 0
|
|
|
|
-88 -83 -61 0
|
|
|
|
-88 83 61 0
|
|
|
|
88 -83 61 0
|
|
|
|
88 83 -61 0
|
|
|
|
-89 -83 -64 0
|
|
|
|
-89 83 64 0
|
|
|
|
89 -83 64 0
|
|
|
|
89 83 -64 0
|
|
|
|
-90 -83 -67 0
|
|
|
|
-90 83 67 0
|
|
|
|
90 -83 67 0
|
|
|
|
90 83 -67 0
|
|
|
|
-91 -83 -70 0
|
|
|
|
-91 83 70 0
|
|
|
|
91 -83 70 0
|
|
|
|
91 83 -70 0
|
|
|
|
95 1 0
|
|
|
|
95 84 0
|
|
|
|
-1 -84 -95 0
|
|
|
|
-92 -83 -73 0
|
|
|
|
-92 83 73 0
|
|
|
|
92 -83 73 0
|
|
|
|
92 83 -73 0
|
|
|
|
96 84 0
|
|
|
|
96 4 0
|
|
|
|
-84 -4 -96 0
|
|
|
|
-93 -83 -76 0
|
|
|
|
-93 83 76 0
|
|
|
|
93 -83 76 0
|
|
|
|
93 83 -76 0
|
|
|
|
97 84 0
|
|
|
|
97 8 0
|
|
|
|
-84 -8 -97 0
|
|
|
|
-94 -83 -79 0
|
|
|
|
-94 83 79 0
|
|
|
|
94 -83 79 0
|
|
|
|
94 83 -79 0
|
|
|
|
98 84 0
|
|
|
|
98 12 0
|
|
|
|
-84 -12 -98 0
|
|
|
|
99 84 0
|
|
|
|
99 16 0
|
|
|
|
-84 -16 -99 0
|
|
|
|
100 84 0
|
|
|
|
100 20 0
|
|
|
|
-84 -20 -100 0
|
|
|
|
101 84 0
|
|
|
|
101 24 0
|
|
|
|
-84 -24 -101 0
|
|
|
|
102 84 0
|
|
|
|
102 28 0
|
|
|
|
-84 -28 -102 0
|
|
|
|
103 84 0
|
|
|
|
103 32 0
|
|
|
|
-84 -32 -103 0
|
|
|
|
104 86 0
|
|
|
|
104 56 0
|
|
|
|
-86 -56 -104 0
|
|
|
|
105 86 0
|
|
|
|
105 57 0
|
|
|
|
-86 -57 -105 0
|
|
|
|
106 87 0
|
|
|
|
106 59 0
|
|
|
|
-87 -59 -106 0
|
|
|
|
108 88 0
|
|
|
|
108 62 0
|
|
|
|
-88 -62 -108 0
|
|
|
|
110 89 0
|
|
|
|
110 65 0
|
|
|
|
-89 -65 -110 0
|
|
|
|
112 90 0
|
|
|
|
112 68 0
|
|
|
|
-90 -68 -112 0
|
|
|
|
114 91 0
|
|
|
|
114 71 0
|
|
|
|
-91 -71 -114 0
|
|
|
|
116 92 0
|
|
|
|
116 74 0
|
|
|
|
-92 -74 -116 0
|
|
|
|
118 93 0
|
|
|
|
118 77 0
|
|
|
|
-93 -77 -118 0
|
|
|
|
120 94 0
|
|
|
|
120 80 0
|
|
|
|
-94 -80 -120 0
|
|
|
|
107 87 0
|
|
|
|
107 60 0
|
|
|
|
-87 -60 -107 0
|
|
|
|
109 88 0
|
|
|
|
109 63 0
|
|
|
|
-88 -63 -109 0
|
|
|
|
111 89 0
|
|
|
|
111 66 0
|
|
|
|
-89 -66 -111 0
|
|
|
|
113 90 0
|
|
|
|
113 69 0
|
|
|
|
-90 -69 -113 0
|
|
|
|
115 91 0
|
|
|
|
115 72 0
|
|
|
|
-91 -72 -115 0
|
|
|
|
117 92 0
|
|
|
|
117 75 0
|
|
|
|
-92 -75 -117 0
|
|
|
|
119 93 0
|
|
|
|
119 78 0
|
|
|
|
-93 -78 -119 0
|
|
|
|
121 94 0
|
|
|
|
121 81 0
|
|
|
|
-94 -81 -121 0
|
|
|
|
-130 104 0
|
|
|
|
-130 106 0
|
|
|
|
-130 108 0
|
|
|
|
-130 110 0
|
|
|
|
-130 112 0
|
|
|
|
-130 114 0
|
|
|
|
-130 116 0
|
|
|
|
-130 118 0
|
|
|
|
-130 120 0
|
|
|
|
-104 -106 -108 -110 -112 -114 -116 -118 -120 130 0
|
|
|
|
-122 -105 0
|
|
|
|
122 105 0
|
|
|
|
-123 -107 0
|
|
|
|
123 107 0
|
|
|
|
-124 -109 0
|
|
|
|
124 109 0
|
|
|
|
-125 -111 0
|
|
|
|
125 111 0
|
|
|
|
-126 -113 0
|
|
|
|
126 113 0
|
|
|
|
-127 -115 0
|
|
|
|
127 115 0
|
|
|
|
-128 -117 0
|
|
|
|
128 117 0
|
|
|
|
-129 -119 0
|
|
|
|
129 119 0
|
|
|
|
-131 -121 0
|
|
|
|
131 121 0
|
|
|
|
-132 -130 0
|
|
|
|
132 130 0
|
|
|
|
-133 -130 0
|
|
|
|
133 130 0
|
|
|
|
-134 -130 0
|
|
|
|
134 130 0
|
|
|
|
-135 -132 -104 0
|
|
|
|
-135 132 104 0
|
|
|
|
135 -132 104 0
|
|
|
|
135 132 -104 0
|
|
|
|
-136 -132 -106 0
|
|
|
|
-136 132 106 0
|
|
|
|
136 -132 106 0
|
|
|
|
136 132 -106 0
|
|
|
|
-137 -132 -108 0
|
|
|
|
-137 132 108 0
|
|
|
|
137 -132 108 0
|
|
|
|
137 132 -108 0
|
|
|
|
-138 -132 -110 0
|
|
|
|
-138 132 110 0
|
|
|
|
138 -132 110 0
|
|
|
|
138 132 -110 0
|
|
|
|
144 3 0
|
|
|
|
144 133 0
|
|
|
|
-3 -133 -144 0
|
|
|
|
-139 -132 -112 0
|
|
|
|
-139 132 112 0
|
|
|
|
139 -132 112 0
|
|
|
|
139 132 -112 0
|
|
|
|
145 133 0
|
|
|
|
145 7 0
|
|
|
|
-133 -7 -145 0
|
|
|
|
-140 -132 -114 0
|
|
|
|
-140 132 114 0
|
|
|
|
140 -132 114 0
|
|
|
|
140 132 -114 0
|
|
|
|
146 133 0
|
|
|
|
146 11 0
|
|
|
|
-133 -11 -146 0
|
|
|
|
-141 -132 -116 0
|
|
|
|
-141 132 116 0
|
|
|
|
141 -132 116 0
|
|
|
|
141 132 -116 0
|
|
|
|
147 133 0
|
|
|
|
147 15 0
|
|
|
|
-133 -15 -147 0
|
|
|
|
-142 -132 -118 0
|
|
|
|
-142 132 118 0
|
|
|
|
142 -132 118 0
|
|
|
|
142 132 -118 0
|
|
|
|
148 133 0
|
|
|
|
148 19 0
|
|
|
|
-133 -19 -148 0
|
|
|
|
-143 -132 -120 0
|
|
|
|
-143 132 120 0
|
|
|
|
143 -132 120 0
|
|
|
|
143 132 -120 0
|
|
|
|
149 133 0
|
|
|
|
149 23 0
|
|
|
|
-133 -23 -149 0
|
|
|
|
150 133 0
|
|
|
|
150 27 0
|
|
|
|
-133 -27 -150 0
|
|
|
|
151 133 0
|
|
|
|
151 31 0
|
|
|
|
-133 -31 -151 0
|
|
|
|
152 133 0
|
|
|
|
152 35 0
|
|
|
|
-133 -35 -152 0
|
|
|
|
153 135 0
|
|
|
|
153 122 0
|
|
|
|
-135 -122 -153 0
|
|
|
|
154 136 0
|
|
|
|
154 123 0
|
|
|
|
-136 -123 -154 0
|
|
|
|
155 137 0
|
|
|
|
155 124 0
|
|
|
|
-137 -124 -155 0
|
|
|
|
156 138 0
|
|
|
|
156 125 0
|
|
|
|
-138 -125 -156 0
|
|
|
|
157 139 0
|
|
|
|
157 126 0
|
|
|
|
-139 -126 -157 0
|
|
|
|
158 140 0
|
|
|
|
158 127 0
|
|
|
|
-140 -127 -158 0
|
|
|
|
159 141 0
|
|
|
|
159 128 0
|
|
|
|
-141 -128 -159 0
|
|
|
|
160 142 0
|
|
|
|
160 129 0
|
|
|
|
-142 -129 -160 0
|
|
|
|
161 143 0
|
|
|
|
161 131 0
|
|
|
|
-143 -131 -161 0
|
|
|
|
-162 153 0
|
|
|
|
-162 154 0
|
|
|
|
-162 155 0
|
|
|
|
-162 156 0
|
|
|
|
-162 157 0
|
|
|
|
-162 158 0
|
|
|
|
-162 159 0
|
|
|
|
-162 160 0
|
|
|
|
-162 161 0
|
|
|
|
-153 -154 -155 -156 -157 -158 -159 -160 -161 162 0
|
|
|
|
-163 -162 0
|
|
|
|
163 162 0
|
|
|
|
-164 -162 0
|
|
|
|
164 162 0
|
|
|
|
165 5 0
|
|
|
|
165 163 0
|
|
|
|
-5 -163 -165 0
|
|
|
|
166 163 0
|
|
|
|
166 9 0
|
|
|
|
-163 -9 -166 0
|
|
|
|
167 163 0
|
|
|
|
167 13 0
|
|
|
|
-163 -13 -167 0
|
|
|
|
168 163 0
|
|
|
|
168 17 0
|
|
|
|
-163 -17 -168 0
|
|
|
|
169 163 0
|
|
|
|
169 21 0
|
|
|
|
-163 -21 -169 0
|
|
|
|
170 163 0
|
|
|
|
170 25 0
|
|
|
|
-163 -25 -170 0
|
|
|
|
171 163 0
|
|
|
|
171 29 0
|
|
|
|
-163 -29 -171 0
|
|
|
|
172 163 0
|
|
|
|
172 33 0
|
|
|
|
-163 -33 -172 0
|
|
|
|
173 163 0
|
|
|
|
173 36 0
|
|
|
|
-163 -36 -173 0
|
|
|
|
174 2 0
|
|
|
|
174 95 0
|
|
|
|
174 144 0
|
|
|
|
174 165 0
|
|
|
|
-2 -95 -144 -165 -174 0
|
|
|
|
175 96 0
|
|
|
|
175 145 0
|
|
|
|
175 166 0
|
|
|
|
175 6 0
|
|
|
|
-96 -145 -166 -6 -175 0
|
|
|
|
176 97 0
|
|
|
|
176 146 0
|
|
|
|
176 167 0
|
|
|
|
176 10 0
|
|
|
|
-97 -146 -167 -10 -176 0
|
|
|
|
177 98 0
|
|
|
|
177 147 0
|
|
|
|
177 168 0
|
|
|
|
177 14 0
|
|
|
|
-98 -147 -168 -14 -177 0
|
|
|
|
178 99 0
|
|
|
|
178 148 0
|
|
|
|
178 169 0
|
|
|
|
178 18 0
|
|
|
|
-99 -148 -169 -18 -178 0
|
|
|
|
179 100 0
|
|
|
|
179 149 0
|
|
|
|
179 170 0
|
|
|
|
179 22 0
|
|
|
|
-100 -149 -170 -22 -179 0
|
|
|
|
180 101 0
|
|
|
|
180 150 0
|
|
|
|
180 171 0
|
|
|
|
180 26 0
|
|
|
|
-101 -150 -171 -26 -180 0
|
|
|
|
181 102 0
|
|
|
|
181 151 0
|
|
|
|
181 172 0
|
|
|
|
181 30 0
|
|
|
|
-102 -151 -172 -30 -181 0
|
|
|
|
182 103 0
|
|
|
|
182 152 0
|
|
|
|
182 173 0
|
|
|
|
182 34 0
|
|
|
|
-103 -152 -173 -34 -182 0
|
|
|
|
-183 -174 0
|
|
|
|
183 174 0
|
|
|
|
-188 175 0
|
|
|
|
-188 176 0
|
|
|
|
-188 177 0
|
|
|
|
-188 178 0
|
|
|
|
-188 179 0
|
|
|
|
-188 180 0
|
|
|
|
-188 181 0
|
|
|
|
-188 182 0
|
|
|
|
-175 -176 -177 -178 -179 -180 -181 -182 188 0
|
|
|
|
-184 -177 0
|
|
|
|
184 177 0
|
|
|
|
-185 -179 0
|
|
|
|
185 179 0
|
|
|
|
-186 -180 0
|
|
|
|
186 180 0
|
|
|
|
-187 -181 0
|
|
|
|
187 181 0
|
|
|
|
183 188 193 0
|
|
|
|
-193 -183 0
|
|
|
|
-193 -188 0
|
|
|
|
189 176 0
|
|
|
|
189 184 0
|
|
|
|
-176 -184 -189 0
|
|
|
|
190 176 0
|
|
|
|
190 177 0
|
|
|
|
190 185 0
|
|
|
|
190 178 0
|
|
|
|
-176 -177 -185 -178 -190 0
|
|
|
|
191 178 0
|
|
|
|
191 177 0
|
|
|
|
191 186 0
|
|
|
|
-178 -177 -186 -191 0
|
|
|
|
192 176 0
|
|
|
|
192 177 0
|
|
|
|
192 180 0
|
|
|
|
192 187 0
|
|
|
|
-176 -177 -180 -187 -192 0
|
|
|
|
194 175 0
|
|
|
|
194 176 0
|
|
|
|
194 189 0
|
|
|
|
194 178 0
|
|
|
|
-175 -176 -189 -178 -194 0
|
|
|
|
195 175 0
|
|
|
|
195 176 0
|
|
|
|
195 190 0
|
|
|
|
195 191 0
|
|
|
|
-175 -176 -190 -191 -195 0
|
|
|
|
196 175 0
|
|
|
|
196 189 0
|
|
|
|
196 190 0
|
|
|
|
196 192 0
|
|
|
|
-175 -189 -190 -192 -196 0
|