cloud-sat/kissat-inc/test/cnf/sqrt6889.cnf

p cnf 302 839
-8 1 0
-8 2 0
8 -1 -2 0
-9 1 0
-9 3 0
9 -1 -3 0
-10 3 0
-10 8 0
10 -3 -8 0
-11 -3 0
-11 -8 0
11 3 8 0
-12 -10 0
-12 -11 0
12 10 11 0
-13 9 0
-13 12 0
13 -9 -12 0
-14 -9 0
-14 -12 0
14 9 12 0
-15 -13 0
-15 -14 0
15 13 14 0
-16 8 0
-16 15 0
16 -8 -15 0
-17 -8 0
-17 -15 0
18 16 17 0
-19 1 0
-19 4 0
19 -1 -4 0
-20 2 0
-20 3 0
20 -2 -3 0
-21 -10 0
-21 -13 0
21 10 13 0
-22 19 0
-22 20 0
22 -19 -20 0
-23 -19 0
-23 -20 0
23 19 20 0
-24 -22 0
-24 -23 0
24 22 23 0
-25 -21 0
-25 24 0
25 21 -24 0
-26 21 0
-26 -24 0
26 -21 24 0
-27 -25 0
-27 -26 0
27 25 26 0
-28 20 0
-28 27 0
28 -20 -27 0
-29 -20 0
-29 -27 0
29 20 27 0
-30 -28 0
-30 -29 0
30 28 29 0
-31 16 0
-31 30 0
31 -16 -30 0
-32 -16 0
-32 -30 0
32 16 30 0
-33 -31 0
-33 -32 0
33 31 32 0
-34 19 0
-34 33 0
34 -19 -33 0
35 19 33 0
-36 -34 0
-36 -35 0
-37 1 0
-37 5 0
37 -1 -5 0
-38 3 0
-38 4 0
38 -3 -4 0
-39 -28 0
-39 -31 0
39 28 31 0
-40 -22 0
-40 -25 0
40 22 25 0
-41 37 0
-41 38 0
41 -37 -38 0
-42 -37 0
-42 -38 0
42 37 38 0
-43 -41 0
-43 -42 0
43 41 42 0
-44 -40 0
-44 43 0
44 40 -43 0
-45 40 0
-45 -43 0
45 -40 43 0
-46 -44 0
-46 -45 0
46 44 45 0
-47 2 0
-47 46 0
47 -2 -46 0
-48 -2 0
-48 -46 0
48 2 46 0
-49 -47 0
-49 -48 0
49 47 48 0
-50 -39 0
-50 49 0
50 39 -49 0
-51 39 0
-51 -49 0
51 -39 49 0
-52 -50 0
-52 -51 0
52 50 51 0
-53 38 0
-53 52 0
53 -38 -52 0
-54 -38 0
-54 -52 0
54 38 52 0
-55 -53 0
-55 -54 0
55 53 54 0
-56 34 0
-56 55 0
56 -34 -55 0
-57 -34 0
-57 -55 0
57 34 55 0
-58 -56 0
-58 -57 0
58 56 57 0
-59 37 0
-59 58 0
59 -37 -58 0
-60 -37 0
-60 -58 0
61 59 60 0
-62 1 0
-62 6 0
62 -1 -6 0
-63 3 0
-63 5 0
63 -3 -5 0
-64 -53 0
-64 -56 0
64 53 56 0
-65 2 0
-65 4 0
65 -2 -4 0
-66 -47 0
-66 -50 0
66 47 50 0
-67 -41 0
-67 -44 0
67 41 44 0
-68 62 0
-68 63 0
68 -62 -63 0
-69 -62 0
-69 -63 0
69 62 63 0
-70 -68 0
-70 -69 0
70 68 69 0
-71 -67 0
-71 70 0
71 67 -70 0
-72 67 0
-72 -70 0
72 -67 70 0
-73 -71 0
-73 -72 0
73 71 72 0
-74 65 0
-74 73 0
74 -65 -73 0
-75 -65 0
-75 -73 0
75 65 73 0
-76 -74 0
-76 -75 0
76 74 75 0
-77 -66 0
-77 76 0
77 66 -76 0
-78 66 0
-78 -76 0
78 -66 76 0
-79 -77 0
-79 -78 0
79 77 78 0
-80 65 0
-80 79 0
80 -65 -79 0
-81 -65 0
-81 -79 0
81 65 79 0
-82 -80 0
-82 -81 0
82 80 81 0
-83 -64 0
-83 82 0
83 64 -82 0
-84 64 0
-84 -82 0
84 -64 82 0
-85 -83 0
-85 -84 0
85 83 84 0
-86 63 0
-86 85 0
86 -63 -85 0
-87 -63 0
-87 -85 0
87 63 85 0
-88 -86 0
-88 -87 0
88 86 87 0
-89 59 0
-89 88 0
89 -59 -88 0
-90 -59 0
-90 -88 0
90 59 88 0
-91 -89 0
-91 -90 0
91 89 90 0
-92 62 0
-92 91 0
92 -62 -91 0
93 62 91 0
-94 -92 0
-94 -93 0
-95 1 0
-95 7 0
95 -1 -7 0
-96 3 0
-96 6 0
96 -3 -6 0
-97 -86 0
-97 -89 0
97 86 89 0
-98 2 0
-98 5 0
98 -2 -5 0
-99 -80 0
-99 -83 0
99 80 83 0
-100 -74 0
-100 -77 0
100 74 77 0
-101 -68 0
-101 -71 0
101 68 71 0
-102 95 0
-102 96 0
102 -95 -96 0
-103 -95 0
-103 -96 0
103 95 96 0
-104 -102 0
-104 -103 0
104 102 103 0
-105 -101 0
-105 104 0
105 101 -104 0
-106 101 0
-106 -104 0
106 -101 104 0
-107 -105 0
-107 -106 0
107 105 106 0
-108 98 0
-108 107 0
108 -98 -107 0
-109 -98 0
-109 -107 0
109 98 107 0
-110 -108 0
-110 -109 0
110 108 109 0
-111 -100 0
-111 110 0
111 100 -110 0
-112 100 0
-112 -110 0
112 -100 110 0
-113 -111 0
-113 -112 0
113 111 112 0
-114 4 0
-114 113 0
114 -4 -113 0
-115 -4 0
-115 -113 0
115 4 113 0
-116 -114 0
-116 -115 0
116 114 115 0
-117 -99 0
-117 116 0
117 99 -116 0
-118 99 0
-118 -116 0
118 -99 116 0
-119 -117 0
-119 -118 0
119 117 118 0
-120 98 0
-120 119 0
120 -98 -119 0
-121 -98 0
-121 -119 0
121 98 119 0
-122 -120 0
-122 -121 0
122 120 121 0
-123 -97 0
-123 122 0
123 97 -122 0
-124 97 0
-124 -122 0
124 -97 122 0
-125 -123 0
-125 -124 0
125 123 124 0
-126 96 0
-126 125 0
126 -96 -125 0
-127 -96 0
-127 -125 0
127 96 125 0
-128 -126 0
-128 -127 0
128 126 127 0
-129 92 0
-129 128 0
129 -92 -128 0
-130 -92 0
-130 -128 0
130 92 128 0
-131 -129 0
-131 -130 0
131 129 130 0
-132 95 0
-132 131 0
132 -95 -131 0
133 95 131 0
-134 -132 0
-134 -133 0
-135 3 0
-135 7 0
135 -3 -7 0
-136 -126 0
-136 -129 0
136 126 129 0
-137 2 0
-137 6 0
137 -2 -6 0
-138 -120 0
-138 -123 0
138 120 123 0
-139 4 0
-139 5 0
139 -4 -5 0
-140 -114 0
-140 -117 0
140 114 117 0
-141 -108 0
-141 -111 0
141 108 111 0
-142 -102 0
-142 -105 0
142 102 105 0
-143 135 0
-143 -142 0
143 -135 142 0
-144 -135 0
-144 142 0
144 135 -142 0
-145 -143 0
-145 -144 0
145 143 144 0
-146 137 0
-146 145 0
146 -137 -145 0
-147 -137 0
-147 -145 0
147 137 145 0
-148 -146 0
-148 -147 0
148 146 147 0
-149 -141 0
-149 148 0
149 141 -148 0
-150 141 0
-150 -148 0
150 -141 148 0
-151 -149 0
-151 -150 0
151 149 150 0
-152 139 0
-152 151 0
152 -139 -151 0
-153 -139 0
-153 -151 0
153 139 151 0
-154 -152 0
-154 -153 0
154 152 153 0
-155 -140 0
-155 154 0
155 140 -154 0
-156 140 0
-156 -154 0
156 -140 154 0
-157 -155 0
-157 -156 0
157 155 156 0
-158 139 0
-158 157 0
158 -139 -157 0
-159 -139 0
-159 -157 0
159 139 157 0
-160 -158 0
-160 -159 0
160 158 159 0
-161 -138 0
-161 160 0
161 138 -160 0
-162 138 0
-162 -160 0
162 -138 160 0
-163 -161 0
-163 -162 0
163 161 162 0
-164 137 0
-164 163 0
164 -137 -163 0
-165 -137 0
-165 -163 0
165 137 163 0
-166 -164 0
-166 -165 0
166 164 165 0
-167 -136 0
-167 166 0
167 136 -166 0
-168 136 0
-168 -166 0
168 -136 166 0
-169 -167 0
-169 -168 0
169 167 168 0
-170 135 0
-170 169 0
170 -135 -169 0
-171 -135 0
-171 -169 0
171 135 169 0
-172 -170 0
-172 -171 0
172 170 171 0
-173 132 0
-173 172 0
173 -132 -172 0
174 132 172 0
-175 -173 0
-175 -174 0
-176 -170 0
-176 -173 0
176 170 173 0
-177 2 0
-177 7 0
177 -2 -7 0
-178 -164 0
-178 -167 0
178 164 167 0
-179 4 0
-179 6 0
179 -4 -6 0
-180 -158 0
-180 -161 0
180 158 161 0
-181 -152 0
-181 -155 0
181 152 155 0
-182 -146 0
-182 -149 0
182 146 149 0
-183 143 0
-183 177 0
183 -143 -177 0
-184 -143 0
-184 -177 0
184 143 177 0
-185 -183 0
-185 -184 0
185 183 184 0
-186 -182 0
-186 185 0
186 182 -185 0
-187 182 0
-187 -185 0
187 -182 185 0
-188 -186 0
-188 -187 0
188 186 187 0
-189 179 0
-189 188 0
189 -179 -188 0
-190 -179 0
-190 -188 0
190 179 188 0
-191 -189 0
-191 -190 0
191 189 190 0
-192 -181 0
-192 191 0
192 181 -191 0
-193 181 0
-193 -191 0
193 -181 191 0
-194 -192 0
-194 -193 0
194 192 193 0
-195 5 0
-195 194 0
195 -5 -194 0
-196 -5 0
-196 -194 0
196 5 194 0
-197 -195 0
-197 -196 0
197 195 196 0
-198 -180 0
-198 197 0
198 180 -197 0
-199 180 0
-199 -197 0
199 -180 197 0
-200 -198 0
-200 -199 0
200 198 199 0
-201 179 0
-201 200 0
201 -179 -200 0
-202 -179 0
-202 -200 0
202 179 200 0
-203 -201 0
-203 -202 0
203 201 202 0
-204 -178 0
-204 203 0
204 178 -203 0
-205 178 0
-205 -203 0
205 -178 203 0
-206 -204 0
-206 -205 0
206 204 205 0
-207 177 0
-207 206 0
207 -177 -206 0
-208 -177 0
-208 -206 0
208 177 206 0
-209 -207 0
-209 -208 0
209 207 208 0
-210 -176 0
-210 209 0
210 176 -209 0
-211 176 0
-211 -209 0
212 210 211 0
-213 -207 0
-213 -210 0
213 207 210 0
-214 4 0
-214 7 0
214 -4 -7 0
-215 -201 0
-215 -204 0
215 201 204 0
-216 5 0
-216 6 0
216 -5 -6 0
-217 -195 0
-217 -198 0
217 195 198 0
-218 -189 0
-218 -192 0
218 189 192 0
-219 -183 0
-219 -186 0
219 183 186 0
-220 214 0
-220 -219 0
220 -214 219 0
-221 -214 0
-221 219 0
221 214 -219 0
-222 -220 0
-222 -221 0
222 220 221 0
-223 -218 0
-223 222 0
223 218 -222 0
-224 218 0
-224 -222 0
224 -218 222 0
-225 -223 0
-225 -224 0
225 223 224 0
-226 216 0
-226 225 0
226 -216 -225 0
-227 -216 0
-227 -225 0
227 216 225 0
-228 -226 0
-228 -227 0
228 226 227 0
-229 -217 0
-229 228 0
229 217 -228 0
-230 217 0
-230 -228 0
230 -217 228 0
-231 -229 0
-231 -230 0
231 229 230 0
-232 216 0
-232 231 0
232 -216 -231 0
-233 -216 0
-233 -231 0
233 216 231 0
-234 -232 0
-234 -233 0
234 232 233 0
-235 -215 0
-235 234 0
235 215 -234 0
-236 215 0
-236 -234 0
236 -215 234 0
-237 -235 0
-237 -236 0
237 235 236 0
-238 214 0
-238 237 0
238 -214 -237 0
-239 -214 0
-239 -237 0
239 214 237 0
-240 -238 0
-240 -239 0
240 238 239 0
-241 -213 0
-241 240 0
241 213 -240 0
242 -213 240 0
-243 -241 0
-243 -242 0
-244 -238 0
-244 -241 0
244 238 241 0
-245 5 0
-245 7 0
245 -5 -7 0
-246 -232 0
-246 -235 0
246 232 235 0
-247 -226 0
-247 -229 0
247 226 229 0
-248 -220 0
-248 -223 0
248 220 223 0
-249 245 0
-249 -248 0
249 -245 248 0
-250 -245 0
-250 248 0
250 245 -248 0
-251 -249 0
-251 -250 0
251 249 250 0
-252 -247 0
-252 251 0
252 247 -251 0
-253 247 0
-253 -251 0
253 -247 251 0
-254 -252 0
-254 -253 0
254 252 253 0
-255 6 0
-255 254 0
255 -6 -254 0
-256 -6 0
-256 -254 0
256 6 254 0
-257 -255 0
-257 -256 0
257 255 256 0
-258 -246 0
-258 257 0
258 246 -257 0
-259 246 0
-259 -257 0
259 -246 257 0
-260 -258 0
-260 -259 0
260 258 259 0
-261 245 0
-261 260 0
261 -245 -260 0
-262 -245 0
-262 -260 0
262 245 260 0
-263 -261 0
-263 -262 0
263 261 262 0
-264 -244 0
-264 263 0
264 244 -263 0
-265 244 0
-265 -263 0
266 264 265 0
-267 -261 0
-267 -264 0
267 261 264 0
-268 6 0
-268 7 0
268 -6 -7 0
-269 -255 0
-269 -258 0
269 255 258 0
-270 -249 0
-270 -252 0
270 249 252 0
-271 268 0
-271 -270 0
271 -268 270 0
-272 -268 0
-272 270 0
272 268 -270 0
-273 -271 0
-273 -272 0
273 271 272 0
-274 -269 0
-274 273 0
274 269 -273 0
-275 269 0
-275 -273 0
275 -269 273 0
-276 -274 0
-276 -275 0
276 274 275 0
-277 268 0
-277 276 0
277 -268 -276 0
-278 -268 0
-278 -276 0
278 268 276 0
-279 -277 0
-279 -278 0
279 277 278 0
-280 -267 0
-280 279 0
280 267 -279 0
281 -267 279 0
-282 -280 0
-282 -281 0
-283 -277 0
-283 -280 0
283 277 280 0
-284 -271 0
-284 -274 0
284 271 274 0
-285 7 0
-285 -284 0
285 -7 284 0
-286 -7 0
-286 284 0
286 7 -284 0
-287 -285 0
-287 -286 0
287 285 286 0
288 -283 287 0
289 283 -287 0
-290 -285 0
-290 -289 0
-291 -288 0
-291 290 0
-292 282 0
-292 291 0
-293 -266 0
-293 292 0
-294 243 0
-294 293 0
-295 -212 0
-295 294 0
-296 175 0
-296 295 0
-297 134 0
-297 296 0
-298 94 0
-298 297 0
-299 -61 0
-299 298 0
-300 36 0
-300 299 0
-301 -18 0
-301 300 0
-302 1 0
-302 301 0
302 0