puresat-0.1: dimacs/parity/par8-1.cnf
c FILE: par8-1.cnf
c
c SOURCE: James Crawford (jc@research.att.com)
c
c DESCRIPTION: Instance arises from the problem of learning the parity
c function.
c
c parxx-y denotes a parity problem on xx bits. y is simply the
c intance number.
c
c parxx-y-c denotes an instance identical to parxx-y except that
c the instances have been simplified (to create an equivalent
c problem).
c
c NOTE: Satisfiable (checked for 8 and 16 size instances. All
c instances are satisfiable by construction)
c
c NOTE: Number of clauses corrected August 3, 1993
c
c Converted from tableau format Tue Aug 3 09:55:22 EDT 1993
p cnf 350 1149
-1
0
145 -1 2
0
-145 1 2
0
145 1 -2
0
-145 -1 -2
0
146 -2 3
0
-146 2 3
0
146 2 -3
0
-146 -2 -3
0
147 -3 4
0
-147 3 4
0
147 3 -4
0
-147 -3 -4
0
5 -4
0
-5 4
0
6 -5
0
-6 5
0
150 -6 7
0
-150 6 7
0
150 6 -7
0
-150 -6 -7
0
8 -7
0
-8 7
0
152 -8 9
0
-152 8 9
0
152 8 -9
0
-152 -8 -9
0
10
0
145 -10 11
0
-145 10 11
0
145 10 -11
0
-145 -10 -11
0
146 -11 12
0
-146 11 12
0
146 11 -12
0
-146 -11 -12
0
147 -12 13
0
-147 12 13
0
147 12 -13
0
-147 -12 -13
0
148 -13 14
0
-148 13 14
0
148 13 -14
0
-148 -13 -14
0
15 -14
0
-15 14
0
16 -15
0
-16 15
0
17 -16
0
-17 16
0
18 -17
0
-18 17
0
19
0
20 -19
0
-20 19
0
21 -20
0
-21 20
0
22 -21
0
-22 21
0
23 -22
0
-23 22
0
24 -23
0
-24 23
0
25 -24
0
-25 24
0
151 -25 26
0
-151 25 26
0
151 25 -26
0
-151 -25 -26
0
27 -26
0
-27 26
0
-28
0
29 -28
0
-29 28
0
146 -29 30
0
-146 29 30
0
146 29 -30
0
-146 -29 -30
0
31 -30
0
-31 30
0
148 -31 32
0
-148 31 32
0
148 31 -32
0
-148 -31 -32
0
149 -32 33
0
-149 32 33
0
149 32 -33
0
-149 -32 -33
0
34 -33
0
-34 33
0
151 -34 35
0
-151 34 35
0
151 34 -35
0
-151 -34 -35
0
152 -35 36
0
-152 35 36
0
152 35 -36
0
-152 -35 -36
0
37
0
38 -37
0
-38 37
0
146 -38 39
0
-146 38 39
0
146 38 -39
0
-146 -38 -39
0
40 -39
0
-40 39
0
41 -40
0
-41 40
0
149 -41 42
0
-149 41 42
0
149 41 -42
0
-149 -41 -42
0
150 -42 43
0
-150 42 43
0
150 42 -43
0
-150 -42 -43
0
151 -43 44
0
-151 43 44
0
151 43 -44
0
-151 -43 -44
0
45 -44
0
-45 44
0
46
0
47 -46
0
-47 46
0
48 -47
0
-48 47
0
147 -48 49
0
-147 48 49
0
147 48 -49
0
-147 -48 -49
0
50 -49
0
-50 49
0
51 -50
0
-51 50
0
150 -51 52
0
-150 51 52
0
150 51 -52
0
-150 -51 -52
0
53 -52
0
-53 52
0
54 -53
0
-54 53
0
55
0
56 -55
0
-56 55
0
57 -56
0
-57 56
0
147 -57 58
0
-147 57 58
0
147 57 -58
0
-147 -57 -58
0
59 -58
0
-59 58
0
149 -59 60
0
-149 59 60
0
149 59 -60
0
-149 -59 -60
0
150 -60 61
0
-150 60 61
0
150 60 -61
0
-150 -60 -61
0
151 -61 62
0
-151 61 62
0
151 61 -62
0
-151 -61 -62
0
63 -62
0
-63 62
0
64
0
65 -64
0
-65 64
0
66 -65
0
-66 65
0
147 -66 67
0
-147 66 67
0
147 66 -67
0
-147 -66 -67
0
148 -67 68
0
-148 67 68
0
148 67 -68
0
-148 -67 -68
0
149 -68 69
0
-149 68 69
0
149 68 -69
0
-149 -68 -69
0
70 -69
0
-70 69
0
71 -70
0
-71 70
0
152 -71 72
0
-152 71 72
0
152 71 -72
0
-152 -71 -72
0
-73
0
74 -73
0
-74 73
0
75 -74
0
-75 74
0
76 -75
0
-76 75
0
77 -76
0
-77 76
0
149 -77 78
0
-149 77 78
0
149 77 -78
0
-149 -77 -78
0
79 -78
0
-79 78
0
80 -79
0
-80 79
0
152 -80 81
0
-152 80 81
0
152 80 -81
0
-152 -80 -81
0
-82
0
83 -82
0
-83 82
0
84 -83
0
-84 83
0
85 -84
0
-85 84
0
148 -85 86
0
-148 85 86
0
148 85 -86
0
-148 -85 -86
0
149 -86 87
0
-149 86 87
0
149 86 -87
0
-149 -86 -87
0
88 -87
0
-88 87
0
151 -88 89
0
-151 88 89
0
151 88 -89
0
-151 -88 -89
0
90 -89
0
-90 89
0
-91
0
92 -91
0
-92 91
0
146 -92 93
0
-146 92 93
0
146 92 -93
0
-146 -92 -93
0
94 -93
0
-94 93
0
95 -94
0
-95 94
0
96 -95
0
-96 95
0
150 -96 97
0
-150 96 97
0
150 96 -97
0
-150 -96 -97
0
98 -97
0
-98 97
0
152 -98 99
0
-152 98 99
0
152 98 -99
0
-152 -98 -99
0
-100
0
101 -100
0
-101 100
0
146 -101 102
0
-146 101 102
0
146 101 -102
0
-146 -101 -102
0
103 -102
0
-103 102
0
148 -103 104
0
-148 103 104
0
148 103 -104
0
-148 -103 -104
0
105 -104
0
-105 104
0
150 -105 106
0
-150 105 106
0
150 105 -106
0
-150 -105 -106
0
107 -106
0
-107 106
0
152 -107 108
0
-152 107 108
0
152 107 -108
0
-152 -107 -108
0
-109
0
145 -109 110
0
-145 109 110
0
145 109 -110
0
-145 -109 -110
0
146 -110 111
0
-146 110 111
0
146 110 -111
0
-146 -110 -111
0
112 -111
0
-112 111
0
148 -112 113
0
-148 112 113
0
148 112 -113
0
-148 -112 -113
0
114 -113
0
-114 113
0
115 -114
0
-115 114
0
116 -115
0
-116 115
0
117 -116
0
-117 116
0
-118
0
119 -118
0
-119 118
0
146 -119 120
0
-146 119 120
0
146 119 -120
0
-146 -119 -120
0
121 -120
0
-121 120
0
148 -121 122
0
-148 121 122
0
148 121 -122
0
-148 -121 -122
0
123 -122
0
-123 122
0
150 -123 124
0
-150 123 124
0
150 123 -124
0
-150 -123 -124
0
151 -124 125
0
-151 124 125
0
151 124 -125
0
-151 -124 -125
0
126 -125
0
-126 125
0
127
0
145 -127 128
0
-145 127 128
0
145 127 -128
0
-145 -127 -128
0
146 -128 129
0
-146 128 129
0
146 128 -129
0
-146 -128 -129
0
147 -129 130
0
-147 129 130
0
147 129 -130
0
-147 -129 -130
0
131 -130
0
-131 130
0
149 -131 132
0
-149 131 132
0
149 131 -132
0
-149 -131 -132
0
133 -132
0
-133 132
0
134 -133
0
-134 133
0
152 -134 135
0
-152 134 135
0
152 134 -135
0
-152 -134 -135
0
136
0
137 -136
0
-137 136
0
146 -137 138
0
-146 137 138
0
146 137 -138
0
-146 -137 -138
0
139 -138
0
-139 138
0
148 -139 140
0
-148 139 140
0
148 139 -140
0
-148 -139 -140
0
149 -140 141
0
-149 140 141
0
149 140 -141
0
-149 -140 -141
0
150 -141 142
0
-150 141 142
0
150 141 -142
0
-150 -141 -142
0
143 -142
0
-143 142
0
144 -143
0
-144 143
0
-153
0
-154
0
-155
0
-156
0
-157
0
-158
0
9 -255
0
-9 255
0
255 -153 159
0
-255 153 159
0
255 153 -159
0
-255 -153 -159
0
256 -154 160
0
-256 154 160
0
256 154 -160
0
-256 -154 -160
0
255 -256
0
153 -256
0
-255 -153 256
0
-153 159 256
0
257 -155 161
0
-257 155 161
0
257 155 -161
0
-257 -155 -161
0
256 -257
0
154 -257
0
-256 -154 257
0
-154 160 257
0
258 -156 162
0
-258 156 162
0
258 156 -162
0
-258 -156 -162
0
257 -258
0
155 -258
0
-257 -155 258
0
-155 161 258
0
259 -157 163
0
-259 157 163
0
259 157 -163
0
-259 -157 -163
0
258 -259
0
156 -259
0
-258 -156 259
0
-156 162 259
0
260 -158 164
0
-260 158 164
0
260 158 -164
0
-260 -158 -164
0
259 -260
0
157 -260
0
-259 -157 260
0
-157 163 260
0
18 -261
0
-18 261
0
261 -159 165
0
-261 159 165
0
261 159 -165
0
-261 -159 -165
0
262 -160 166
0
-262 160 166
0
262 160 -166
0
-262 -160 -166
0
261 -262
0
159 -262
0
-261 -159 262
0
-159 165 262
0
263 -161 167
0
-263 161 167
0
263 161 -167
0
-263 -161 -167
0
262 -263
0
160 -263
0
-262 -160 263
0
-160 166 263
0
264 -162 168
0
-264 162 168
0
264 162 -168
0
-264 -162 -168
0
263 -264
0
161 -264
0
-263 -161 264
0
-161 167 264
0
265 -163 169
0
-265 163 169
0
265 163 -169
0
-265 -163 -169
0
264 -265
0
162 -265
0
-264 -162 265
0
-162 168 265
0
266 -164 170
0
-266 164 170
0
266 164 -170
0
-266 -164 -170
0
265 -266
0
163 -266
0
-265 -163 266
0
-163 169 266
0
27 -267
0
-27 267
0
267 -165 171
0
-267 165 171
0
267 165 -171
0
-267 -165 -171
0
268 -166 172
0
-268 166 172
0
268 166 -172
0
-268 -166 -172
0
267 -268
0
165 -268
0
-267 -165 268
0
-165 171 268
0
269 -167 173
0
-269 167 173
0
269 167 -173
0
-269 -167 -173
0
268 -269
0
166 -269
0
-268 -166 269
0
-166 172 269
0
270 -168 174
0
-270 168 174
0
270 168 -174
0
-270 -168 -174
0
269 -270
0
167 -270
0
-269 -167 270
0
-167 173 270
0
271 -169 175
0
-271 169 175
0
271 169 -175
0
-271 -169 -175
0
270 -271
0
168 -271
0
-270 -168 271
0
-168 174 271
0
272 -170 176
0
-272 170 176
0
272 170 -176
0
-272 -170 -176
0
271 -272
0
169 -272
0
-271 -169 272
0
-169 175 272
0
36 -273
0
-36 273
0
273 -171 177
0
-273 171 177
0
273 171 -177
0
-273 -171 -177
0
274 -172 178
0
-274 172 178
0
274 172 -178
0
-274 -172 -178
0
273 -274
0
171 -274
0
-273 -171 274
0
-171 177 274
0
275 -173 179
0
-275 173 179
0
275 173 -179
0
-275 -173 -179
0
274 -275
0
172 -275
0
-274 -172 275
0
-172 178 275
0
276 -174 180
0
-276 174 180
0
276 174 -180
0
-276 -174 -180
0
275 -276
0
173 -276
0
-275 -173 276
0
-173 179 276
0
277 -175 181
0
-277 175 181
0
277 175 -181
0
-277 -175 -181
0
276 -277
0
174 -277
0
-276 -174 277
0
-174 180 277
0
278 -176 182
0
-278 176 182
0
278 176 -182
0
-278 -176 -182
0
277 -278
0
175 -278
0
-277 -175 278
0
-175 181 278
0
45 -279
0
-45 279
0
279 -177 183
0
-279 177 183
0
279 177 -183
0
-279 -177 -183
0
280 -178 184
0
-280 178 184
0
280 178 -184
0
-280 -178 -184
0
279 -280
0
177 -280
0
-279 -177 280
0
-177 183 280
0
281 -179 185
0
-281 179 185
0
281 179 -185
0
-281 -179 -185
0
280 -281
0
178 -281
0
-280 -178 281
0
-178 184 281
0
282 -180 186
0
-282 180 186
0
282 180 -186
0
-282 -180 -186
0
281 -282
0
179 -282
0
-281 -179 282
0
-179 185 282
0
283 -181 187
0
-283 181 187
0
283 181 -187
0
-283 -181 -187
0
282 -283
0
180 -283
0
-282 -180 283
0
-180 186 283
0
284 -182 188
0
-284 182 188
0
284 182 -188
0
-284 -182 -188
0
283 -284
0
181 -284
0
-283 -181 284
0
-181 187 284
0
54 -285
0
-54 285
0
285 -183 189
0
-285 183 189
0
285 183 -189
0
-285 -183 -189
0
286 -184 190
0
-286 184 190
0
286 184 -190
0
-286 -184 -190
0
285 -286
0
183 -286
0
-285 -183 286
0
-183 189 286
0
287 -185 191
0
-287 185 191
0
287 185 -191
0
-287 -185 -191
0
286 -287
0
184 -287
0
-286 -184 287
0
-184 190 287
0
288 -186 192
0
-288 186 192
0
288 186 -192
0
-288 -186 -192
0
287 -288
0
185 -288
0
-287 -185 288
0
-185 191 288
0
289 -187 193
0
-289 187 193
0
289 187 -193
0
-289 -187 -193
0
288 -289
0
186 -289
0
-288 -186 289
0
-186 192 289
0
290 -188 194
0
-290 188 194
0
290 188 -194
0
-290 -188 -194
0
289 -290
0
187 -290
0
-289 -187 290
0
-187 193 290
0
63 -291
0
-63 291
0
291 -189 195
0
-291 189 195
0
291 189 -195
0
-291 -189 -195
0
292 -190 196
0
-292 190 196
0
292 190 -196
0
-292 -190 -196
0
291 -292
0
189 -292
0
-291 -189 292
0
-189 195 292
0
293 -191 197
0
-293 191 197
0
293 191 -197
0
-293 -191 -197
0
292 -293
0
190 -293
0
-292 -190 293
0
-190 196 293
0
294 -192 198
0
-294 192 198
0
294 192 -198
0
-294 -192 -198
0
293 -294
0
191 -294
0
-293 -191 294
0
-191 197 294
0
295 -193 199
0
-295 193 199
0
295 193 -199
0
-295 -193 -199
0
294 -295
0
192 -295
0
-294 -192 295
0
-192 198 295
0
296 -194 200
0
-296 194 200
0
296 194 -200
0
-296 -194 -200
0
295 -296
0
193 -296
0
-295 -193 296
0
-193 199 296
0
72 -297
0
-72 297
0
297 -195 201
0
-297 195 201
0
297 195 -201
0
-297 -195 -201
0
298 -196 202
0
-298 196 202
0
298 196 -202
0
-298 -196 -202
0
297 -298
0
195 -298
0
-297 -195 298
0
-195 201 298
0
299 -197 203
0
-299 197 203
0
299 197 -203
0
-299 -197 -203
0
298 -299
0
196 -299
0
-298 -196 299
0
-196 202 299
0
300 -198 204
0
-300 198 204
0
300 198 -204
0
-300 -198 -204
0
299 -300
0
197 -300
0
-299 -197 300
0
-197 203 300
0
301 -199 205
0
-301 199 205
0
301 199 -205
0
-301 -199 -205
0
300 -301
0
198 -301
0
-300 -198 301
0
-198 204 301
0
302 -200 206
0
-302 200 206
0
302 200 -206
0
-302 -200 -206
0
301 -302
0
199 -302
0
-301 -199 302
0
-199 205 302
0
81 -303
0
-81 303
0
303 -201 207
0
-303 201 207
0
303 201 -207
0
-303 -201 -207
0
304 -202 208
0
-304 202 208
0
304 202 -208
0
-304 -202 -208
0
303 -304
0
201 -304
0
-303 -201 304
0
-201 207 304
0
305 -203 209
0
-305 203 209
0
305 203 -209
0
-305 -203 -209
0
304 -305
0
202 -305
0
-304 -202 305
0
-202 208 305
0
306 -204 210
0
-306 204 210
0
306 204 -210
0
-306 -204 -210
0
305 -306
0
203 -306
0
-305 -203 306
0
-203 209 306
0
307 -205 211
0
-307 205 211
0
307 205 -211
0
-307 -205 -211
0
306 -307
0
204 -307
0
-306 -204 307
0
-204 210 307
0
308 -206 212
0
-308 206 212
0
308 206 -212
0
-308 -206 -212
0
307 -308
0
205 -308
0
-307 -205 308
0
-205 211 308
0
90 -309
0
-90 309
0
309 -207 213
0
-309 207 213
0
309 207 -213
0
-309 -207 -213
0
310 -208 214
0
-310 208 214
0
310 208 -214
0
-310 -208 -214
0
309 -310
0
207 -310
0
-309 -207 310
0
-207 213 310
0
311 -209 215
0
-311 209 215
0
311 209 -215
0
-311 -209 -215
0
310 -311
0
208 -311
0
-310 -208 311
0
-208 214 311
0
312 -210 216
0
-312 210 216
0
312 210 -216
0
-312 -210 -216
0
311 -312
0
209 -312
0
-311 -209 312
0
-209 215 312
0
313 -211 217
0
-313 211 217
0
313 211 -217
0
-313 -211 -217
0
312 -313
0
210 -313
0
-312 -210 313
0
-210 216 313
0
314 -212 218
0
-314 212 218
0
314 212 -218
0
-314 -212 -218
0
313 -314
0
211 -314
0
-313 -211 314
0
-211 217 314
0
99 -315
0
-99 315
0
315 -213 219
0
-315 213 219
0
315 213 -219
0
-315 -213 -219
0
316 -214 220
0
-316 214 220
0
316 214 -220
0
-316 -214 -220
0
315 -316
0
213 -316
0
-315 -213 316
0
-213 219 316
0
317 -215 221
0
-317 215 221
0
317 215 -221
0
-317 -215 -221
0
316 -317
0
214 -317
0
-316 -214 317
0
-214 220 317
0
318 -216 222
0
-318 216 222
0
318 216 -222
0
-318 -216 -222
0
317 -318
0
215 -318
0
-317 -215 318
0
-215 221 318
0
319 -217 223
0
-319 217 223
0
319 217 -223
0
-319 -217 -223
0
318 -319
0
216 -319
0
-318 -216 319
0
-216 222 319
0
320 -218 224
0
-320 218 224
0
320 218 -224
0
-320 -218 -224
0
319 -320
0
217 -320
0
-319 -217 320
0
-217 223 320
0
108 -321
0
-108 321
0
321 -219 225
0
-321 219 225
0
321 219 -225
0
-321 -219 -225
0
322 -220 226
0
-322 220 226
0
322 220 -226
0
-322 -220 -226
0
321 -322
0
219 -322
0
-321 -219 322
0
-219 225 322
0
323 -221 227
0
-323 221 227
0
323 221 -227
0
-323 -221 -227
0
322 -323
0
220 -323
0
-322 -220 323
0
-220 226 323
0
324 -222 228
0
-324 222 228
0
324 222 -228
0
-324 -222 -228
0
323 -324
0
221 -324
0
-323 -221 324
0
-221 227 324
0
325 -223 229
0
-325 223 229
0
325 223 -229
0
-325 -223 -229
0
324 -325
0
222 -325
0
-324 -222 325
0
-222 228 325
0
326 -224 230
0
-326 224 230
0
326 224 -230
0
-326 -224 -230
0
325 -326
0
223 -326
0
-325 -223 326
0
-223 229 326
0
117 -327
0
-117 327
0
327 -225 231
0
-327 225 231
0
327 225 -231
0
-327 -225 -231
0
328 -226 232
0
-328 226 232
0
328 226 -232
0
-328 -226 -232
0
327 -328
0
225 -328
0
-327 -225 328
0
-225 231 328
0
329 -227 233
0
-329 227 233
0
329 227 -233
0
-329 -227 -233
0
328 -329
0
226 -329
0
-328 -226 329
0
-226 232 329
0
330 -228 234
0
-330 228 234
0
330 228 -234
0
-330 -228 -234
0
329 -330
0
227 -330
0
-329 -227 330
0
-227 233 330
0
331 -229 235
0
-331 229 235
0
331 229 -235
0
-331 -229 -235
0
330 -331
0
228 -331
0
-330 -228 331
0
-228 234 331
0
332 -230 236
0
-332 230 236
0
332 230 -236
0
-332 -230 -236
0
331 -332
0
229 -332
0
-331 -229 332
0
-229 235 332
0
126 -333
0
-126 333
0
333 -231 237
0
-333 231 237
0
333 231 -237
0
-333 -231 -237
0
334 -232 238
0
-334 232 238
0
334 232 -238
0
-334 -232 -238
0
333 -334
0
231 -334
0
-333 -231 334
0
-231 237 334
0
335 -233 239
0
-335 233 239
0
335 233 -239
0
-335 -233 -239
0
334 -335
0
232 -335
0
-334 -232 335
0
-232 238 335
0
336 -234 240
0
-336 234 240
0
336 234 -240
0
-336 -234 -240
0
335 -336
0
233 -336
0
-335 -233 336
0
-233 239 336
0
337 -235 241
0
-337 235 241
0
337 235 -241
0
-337 -235 -241
0
336 -337
0
234 -337
0
-336 -234 337
0
-234 240 337
0
338 -236 242
0
-338 236 242
0
338 236 -242
0
-338 -236 -242
0
337 -338
0
235 -338
0
-337 -235 338
0
-235 241 338
0
135 -339
0
-135 339
0
339 -237 243
0
-339 237 243
0
339 237 -243
0
-339 -237 -243
0
340 -238 244
0
-340 238 244
0
340 238 -244
0
-340 -238 -244
0
339 -340
0
237 -340
0
-339 -237 340
0
-237 243 340
0
341 -239 245
0
-341 239 245
0
341 239 -245
0
-341 -239 -245
0
340 -341
0
238 -341
0
-340 -238 341
0
-238 244 341
0
342 -240 246
0
-342 240 246
0
342 240 -246
0
-342 -240 -246
0
341 -342
0
239 -342
0
-341 -239 342
0
-239 245 342
0
343 -241 247
0
-343 241 247
0
343 241 -247
0
-343 -241 -247
0
342 -343
0
240 -343
0
-342 -240 343
0
-240 246 343
0
344 -242 248
0
-344 242 248
0
344 242 -248
0
-344 -242 -248
0
343 -344
0
241 -344
0
-343 -241 344
0
-241 247 344
0
144 -345
0
-144 345
0
345 -243 249
0
-345 243 249
0
345 243 -249
0
-345 -243 -249
0
346 -244 250
0
-346 244 250
0
346 244 -250
0
-346 -244 -250
0
345 -346
0
243 -346
0
-345 -243 346
0
-243 249 346
0
347 -245 251
0
-347 245 251
0
347 245 -251
0
-347 -245 -251
0
346 -347
0
244 -347
0
-346 -244 347
0
-244 250 347
0
348 -246 252
0
-348 246 252
0
348 246 -252
0
-348 -246 -252
0
347 -348
0
245 -348
0
-347 -245 348
0
-245 251 348
0
349 -247 253
0
-349 247 253
0
349 247 -253
0
-349 -247 -253
0
348 -349
0
246 -349
0
-348 -246 349
0
-246 252 349
0
350 -248 254
0
-350 248 254
0
350 248 -254
0
-350 -248 -254
0
349 -350
0
247 -350
0
-349 -247 350
0
-247 253 350
0
-254
0
-253
0
-252
0
-251
0
-250
0
-260
0
-266
0
-272
0
-278
0
-284
0
-290
0
-296
0
-302
0
-308
0
-314
0
-320
0
-326
0
-332
0
-338
0
-344
0
-350
0