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