WebSPASS-SAT

WebSPASS-SAT Input Form

There is a documentation for SPASS-SAT and SPASS-CNF available. You can also try the File Upload Form.

c STATUS UNSATISFIABLE
c out_mj <-> 1
c product13_eq <-> 2
c product12_eq <-> 3
c product11_eq <-> 4
c product10_eq <-> 5
c product9_eq <-> 6
c product8_eq <-> 7
c product7_eq <-> 8
c product6_eq <-> 9
c product5_eq <-> 10
c product4_eq <-> 11
c product3_eq <-> 12
c product2_eq <-> 13
c notone_b_and_2_0 <-> 14
c notone_b_and_2_0_ <-> 14
c notone_a_and_2_0 <-> 15
c notone_a_and_2_0_ <-> 15
c product13_ <-> 16
c and_2_41_ <-> 17
c product12_ <-> 18
c and_1_41_ <-> 19
c xxor_1_41_ <-> 20
c finaladder_4_carryout_ <-> 21
c and_2_40_ <-> 22
c product11_ <-> 23
c and_1_40_ <-> 24
c xxor_1_40_ <-> 25
c finaladder_3_carryout_ <-> 26
c and_2_39_ <-> 27
c product10_ <-> 28
c and_1_39_ <-> 29
c xxor_1_39_ <-> 30
c finaladder_2_carryout_ <-> 31
c and_2_38_ <-> 32
c product9_ <-> 33
c and_1_38_ <-> 34
c xxor_1_38_ <-> 35
c finaladder_1_carryout_ <-> 36
c and_2_37_ <-> 37
c product8_ <-> 38
c and_1_37_ <-> 39
c xxor_1_37_ <-> 40
c finaladder_0_carryout_ <-> 41
c and_1_36_ <-> 41
c product7_ <-> 42
c xxor_1_36_ <-> 42
c adder_5_6_carryout_ <-> 43
c and_2_35_ <-> 44
c adder_5_6_out_ <-> 45
c and_1_35_ <-> 46
c xxor_1_35_ <-> 47
c adder_4_6_carryout_ <-> 48
c and_2_34_ <-> 49
c adder_4_6_out_ <-> 50
c and_1_34_ <-> 51
c xxor_1_34_ <-> 52
c adder_3_6_carryout_ <-> 53
c and_2_33_ <-> 54
c adder_3_6_out_ <-> 55
c and_1_33_ <-> 56
c xxor_1_33_ <-> 57
c adder_2_6_carryout_ <-> 58
c and_2_32_ <-> 59
c adder_2_6_out_ <-> 60
c and_1_32_ <-> 61
c xxor_1_32_ <-> 62
c adder_1_6_carryout_ <-> 63
c and_2_31_ <-> 64
c adder_1_6_out_ <-> 65
c and_1_31_ <-> 66
c xxor_1_31_ <-> 67
c adder_0_6_carryout_ <-> 68
c and_2_30_ <-> 69
c product6_ <-> 70
c and_1_30_ <-> 71
c xxor_1_30_ <-> 72
c adder_5_5_carryout_ <-> 73
c and_2_29_ <-> 74
c adder_5_5_out_ <-> 75
c adder_4_5_carryout_ <-> 76
c and_2_28_ <-> 77
c adder_4_5_out_ <-> 78
c and_1_28_ <-> 79
c xxor_1_28_ <-> 80
c adder_3_5_carryout_ <-> 81
c and_2_27_ <-> 82
c adder_3_5_out_ <-> 83
c and_1_27_ <-> 84
c xxor_1_27_ <-> 85
c adder_2_5_carryout_ <-> 86
c and_2_26_ <-> 87
c adder_2_5_out_ <-> 88
c and_1_26_ <-> 89
c xxor_1_26_ <-> 90
c adder_1_5_carryout_ <-> 91
c and_2_25_ <-> 92
c adder_1_5_out_ <-> 93
c and_1_25_ <-> 94
c xxor_1_25_ <-> 95
c adder_0_5_carryout_ <-> 96
c and_2_24_ <-> 97
c product5_ <-> 98
c and_1_24_ <-> 99
c xxor_1_24_ <-> 100
c adder_5_4_carryout_ <-> 101
c and_2_23_ <-> 102
c adder_5_4_out_ <-> 103
c and_1_23_ <-> 104
c xxor_1_23_ <-> 105
c adder_4_4_carryout_ <-> 106
c and_2_22_ <-> 107
c adder_4_4_out_ <-> 108
c and_1_22_ <-> 109
c xxor_1_22_ <-> 110
c adder_3_4_carryout_ <-> 111
c and_2_21_ <-> 112
c adder_3_4_out_ <-> 113
c and_1_21_ <-> 114
c xxor_1_21_ <-> 115
c adder_2_4_carryout_ <-> 116
c and_2_20_ <-> 117
c adder_2_4_out_ <-> 118
c and_1_20_ <-> 119
c xxor_1_20_ <-> 120
c adder_1_4_carryout_ <-> 121
c and_2_19_ <-> 122
c adder_1_4_out_ <-> 123
c and_1_19_ <-> 124
c xxor_1_19_ <-> 125
c adder_0_4_carryout_ <-> 126
c and_2_18_ <-> 127
c product4_ <-> 128
c and_1_18_ <-> 129
c xxor_1_18_ <-> 130
c adder_5_3_carryout_ <-> 131
c and_2_17_ <-> 132
c adder_5_3_out_ <-> 133
c adder_4_3_carryout_ <-> 134
c and_2_16_ <-> 135
c adder_4_3_out_ <-> 136
c and_1_16_ <-> 137
c xxor_1_16_ <-> 138
c adder_3_3_carryout_ <-> 139
c and_2_15_ <-> 140
c adder_3_3_out_ <-> 141
c and_1_15_ <-> 142
c xxor_1_15_ <-> 143
c adder_2_3_carryout_ <-> 144
c and_2_14_ <-> 145
c adder_2_3_out_ <-> 146
c and_1_14_ <-> 147
c xxor_1_14_ <-> 148
c adder_1_3_carryout_ <-> 149
c and_2_13_ <-> 150
c adder_1_3_out_ <-> 151
c and_1_13_ <-> 152
c xxor_1_13_ <-> 153
c adder_0_3_carryout_ <-> 154
c and_2_12_ <-> 155
c product3_ <-> 156
c and_1_12_ <-> 157
c xxor_1_12_ <-> 158
c adder_5_2_carryout_ <-> 159
c and_2_11_ <-> 160
c adder_5_2_out_ <-> 161
c and_1_11_ <-> 162
c xxor_1_11_ <-> 163
c adder_4_2_carryout_ <-> 164
c and_2_10_ <-> 165
c adder_4_2_out_ <-> 166
c and_1_10_ <-> 167
c xxor_1_10_ <-> 168
c adder_3_2_carryout_ <-> 169
c and_2_9_ <-> 170
c adder_3_2_out_ <-> 171
c and_1_9_ <-> 172
c xxor_1_9_ <-> 173
c adder_2_2_carryout_ <-> 174
c and_2_8_ <-> 175
c adder_2_2_out_ <-> 176
c and_1_8_ <-> 177
c xxor_1_8_ <-> 178
c adder_1_2_carryout_ <-> 179
c and_2_7_ <-> 180
c adder_1_2_out_ <-> 181
c and_1_7_ <-> 182
c xxor_1_7_ <-> 183
c adder_0_2_carryout_ <-> 184
c and_2_6_ <-> 185
c product2_ <-> 186
c and_1_6_ <-> 187
c xxor_1_6_ <-> 188
c adder_2_0_carry12 <-> 189
c adder_2_0_propagate_generate4_7_to_12 <-> 190
c adder_2_0_carry13 <-> 191
c adder_2_0_propagatecarry12to13 <-> 191
c adder_2_0_propagategenerate10_10_to_8_11 <-> 192
c adder_2_0_propagategenerate9_9_to_8_11 <-> 193
c adder_2_0_propagategenerate8_8_to_8_11 <-> 194
c adder_2_0_propagate_generate8_8_to_10 <-> 195
c adder_2_0_carry11 <-> 198
c adder_2_0_propagate_generate9_9_to_11 <-> 199
c adder_2_0_propagate_generate8_8_to_11 <-> 200
c adder_2_0_carry10 <-> 201
c adder_2_0_carry9 <-> 202
c adder_2_0_propagatecarry8to11 <-> 203
c adder_2_0_propagatecarry8to10 <-> 204
c adder_2_0_propagatecarry8to9 <-> 205
c adder_2_0_carry8 <-> 206
c adder_2_0_generate4_7 <-> 206
c adder_2_0_propagategenerate6_6_to_4_7 <-> 207
c adder_2_0_propagategenerate5_5_to_4_7 <-> 208
c adder_2_0_propagategenerate4_4_to_4_7 <-> 209
c adder_2_0_propagate_generate4_4_to_6 <-> 210
c adder_2_0_carry7 <-> 211
c adder_2_0_propagate_generate5_5_to_7 <-> 212
c adder_2_0_propagate_generate4_4_to_7 <-> 213
c adder_2_0_carry6 <-> 214
c product13 <-> 215
c adder_2_0_sum13 <-> 215
c product12 <-> 216
c adder_2_0_sum12 <-> 216
c product11 <-> 217
c adder_2_0_sum11 <-> 217
c adder_2_0_generate11_11 <-> 218
c adder_2_0_propagate11_11 <-> 219
c product10 <-> 220
c adder_2_0_sum10 <-> 220
c adder_2_0_generate10_10 <-> 221
c adder_2_0_propagate10_10 <-> 222
c product9 <-> 223
c adder_2_0_sum9 <-> 223
c adder_2_0_generate9_9 <-> 224
c adder_2_0_propagate9_9 <-> 225
c product8 <-> 226
c adder_2_0_sum8 <-> 226
c adder_2_0_generate8_8 <-> 227
c adder_2_0_propagate8_8 <-> 228
c product7 <-> 229
c adder_2_0_sum7 <-> 229
c adder_2_0_generate7_7 <-> 230
c adder_2_0_propagate7_7 <-> 231
c product6 <-> 232
c adder_2_0_sum6 <-> 232
c adder_2_0_generate6_6 <-> 233
c adder_2_0_propagate6_6 <-> 234
c product5 <-> 235
c adder_2_0_sum5 <-> 235
c adder_2_0_generate5_5 <-> 236
c adder_2_0_propagate5_5 <-> 237
c adder_2_0_carry5 <-> 238
c adder_2_0_generate4_4 <-> 238
c product4 <-> 239
c adder_2_0_sum4 <-> 239
c adder_2_0_propagate4_4 <-> 239
c adder_1_1_carry8 <-> 240
c adder_1_1_propagate_generate0_3_to_8 <-> 241
c adder_2_0_propagate13_13 <-> 242
c adder_1_1_sum9 <-> 242
c adder_1_1_carry9 <-> 242
c adder_1_1_propagatecarry8to9 <-> 243
c adder_1_1_propagategenerate6_6_to_4_7 <-> 244
c adder_1_1_propagategenerate5_5_to_4_7 <-> 245
c adder_1_1_propagategenerate4_4_to_4_7 <-> 246
c adder_1_1_propagate_generate4_4_to_6 <-> 247
c adder_1_1_carry7 <-> 250
c adder_1_1_propagate_generate5_5_to_7 <-> 251
c adder_1_1_propagate_generate4_4_to_7 <-> 252
c adder_1_1_carry6 <-> 253
c adder_1_1_carry5 <-> 254
c adder_1_1_propagatecarry4to7 <-> 255
c adder_1_1_propagatecarry4to6 <-> 256
c adder_1_1_propagatecarry4to5 <-> 257
c adder_1_1_carry4 <-> 258
c adder_1_1_generate0_3 <-> 258
c adder_1_1_propagategenerate2_2_to_0_3 <-> 259
c adder_2_0_propagate12_12 <-> 260
c adder_1_1_sum8 <-> 260
c adder_1_1_generate8_8 <-> 261
c adder_1_1_propagate8_8 <-> 262
c adder_1_1_sum7 <-> 263
c adder_1_1_generate7_7 <-> 264
c adder_1_1_propagate7_7 <-> 265
c adder_1_1_sum6 <-> 266
c adder_1_1_generate6_6 <-> 267
c adder_1_1_propagate6_6 <-> 268
c adder_1_1_sum5 <-> 269
c adder_1_1_generate5_5 <-> 270
c adder_1_1_propagate5_5 <-> 271
c adder_1_1_sum4 <-> 272
c adder_1_1_generate4_4 <-> 273
c adder_1_1_propagate4_4 <-> 274
c adder_1_1_sum3 <-> 275
c adder_1_1_generate3_3 <-> 276
c adder_1_1_propagate3_3 <-> 277
c adder_1_1_carry3 <-> 278
c adder_1_1_generate2_2 <-> 278
c adder_1_1_sum2 <-> 279
c adder_1_1_propagate2_2 <-> 279
c adder_1_0_carry8 <-> 280
c adder_1_0_propagate_generate0_3_to_8 <-> 281
c adder_1_0_carryout <-> 282
c adder_1_0_sum11 <-> 282
c adder_1_0_carry11 <-> 282
c adder_1_0_propagate_generate8_8_to_11 <-> 283
c adder_1_0_carry10 <-> 284
c adder_1_0_propagate_generate8_8_to_10 <-> 285
c adder_1_0_carry9 <-> 286
c adder_1_0_propagatecarry8to11 <-> 287
c adder_1_0_propagatecarry8to10 <-> 288
c adder_1_0_propagatecarry8to9 <-> 289
c adder_1_0_propagategenerate6_6_to_4_7 <-> 290
c adder_1_0_propagategenerate5_5_to_4_7 <-> 291
c adder_1_0_propagategenerate4_4_to_4_7 <-> 292
c adder_1_0_propagate_generate4_4_to_6 <-> 293
c adder_1_0_carry7 <-> 296
c adder_1_0_propagate_generate5_5_to_7 <-> 297
c adder_1_0_propagate_generate4_4_to_7 <-> 298
c adder_1_0_carry6 <-> 299
c adder_1_0_carry5 <-> 300
c adder_1_0_propagatecarry4to7 <-> 301
c adder_1_0_propagatecarry4to6 <-> 302
c adder_1_0_propagatecarry4to5 <-> 303
c adder_1_0_carry4 <-> 304
c adder_1_0_generate0_3 <-> 304
c adder_1_0_propagategenerate2_2_to_0_3 <-> 305
c adder_1_0_sum10 <-> 306
c adder_1_0_sum9 <-> 307
c adder_1_0_sum8 <-> 308
c adder_1_0_generate8_8 <-> 309
c adder_1_0_propagate8_8 <-> 310
c adder_1_0_sum7 <-> 311
c adder_1_0_generate7_7 <-> 312
c adder_1_0_propagate7_7 <-> 313
c adder_1_0_sum6 <-> 314
c adder_1_0_generate6_6 <-> 315
c adder_1_0_propagate6_6 <-> 316
c adder_1_0_sum5 <-> 317
c adder_1_0_generate5_5 <-> 318
c adder_1_0_propagate5_5 <-> 319
c adder_1_0_sum4 <-> 320
c adder_1_0_generate4_4 <-> 321
c adder_1_0_propagate4_4 <-> 322
c product3 <-> 323
c adder_2_0_sum3 <-> 323
c adder_2_0_propagate3_3 <-> 323
c adder_1_0_sum3 <-> 323
c adder_1_0_generate3_3 <-> 324
c adder_1_0_propagate3_3 <-> 325
c adder_1_0_carry3 <-> 326
c adder_1_0_generate2_2 <-> 326
c product2 <-> 327
c adder_2_0_sum2 <-> 327
c adder_2_0_propagate2_2 <-> 327
c adder_1_0_sum2 <-> 327
c adder_1_0_propagate2_2 <-> 327
c adder_0_2_carryout <-> 328
c adder_0_2_carry8 <-> 328
c adder_0_2_propagate_generate0_3_to_8 <-> 329
c adder_0_2_propagategenerate6_6_to_4_7 <-> 330
c adder_0_2_propagategenerate5_5_to_4_7 <-> 331
c adder_0_2_propagategenerate4_4_to_4_7 <-> 332
c adder_0_2_propagate_generate4_4_to_6 <-> 333
c adder_0_2_carry7 <-> 336
c adder_0_2_propagate_generate5_5_to_7 <-> 337
c adder_0_2_propagate_generate4_4_to_7 <-> 338
c adder_0_2_carry6 <-> 339
c adder_0_2_carry5 <-> 340
c adder_0_2_propagatecarry4to7 <-> 341
c adder_0_2_propagatecarry4to6 <-> 342
c adder_0_2_propagatecarry4to5 <-> 343
c adder_0_2_carry4 <-> 344
c adder_0_2_generate0_3 <-> 344
c adder_0_2_propagategenerate2_2_to_0_3 <-> 345
c adder_0_2_propagategenerate1_1_to_0_3 <-> 346
c adder_0_2_carry3 <-> 347
c adder_0_2_propagate_generate1_1_to_3 <-> 348
c adder_0_2_sum7 <-> 349
c adder_0_2_sum6 <-> 350
c and_1_29_ <-> 351
c adder_0_2_generate6_6 <-> 351
c xxor_1_29_ <-> 352
c adder_0_2_propagate6_6 <-> 352
c adder_0_2_sum5 <-> 353
c adder_0_2_generate5_5 <-> 354
c adder_0_2_propagate5_5 <-> 355
c adder_0_2_sum4 <-> 356
c adder_0_2_generate4_4 <-> 357
c adder_0_2_propagate4_4 <-> 358
c adder_0_2_sum3 <-> 359
c adder_0_2_generate3_3 <-> 360
c adder_0_2_propagate3_3 <-> 361
c adder_0_2_sum2 <-> 362
c adder_0_2_generate2_2 <-> 363
c adder_0_2_propagate2_2 <-> 364
c adder_0_2_carry2 <-> 365
c adder_0_2_generate1_1 <-> 365
c adder_1_1_sum1 <-> 366
c adder_1_1_propagate1_1 <-> 366
c adder_0_2_sum1 <-> 366
c adder_0_2_propagate1_1 <-> 366
c adder_1_0_propagate10_10 <-> 367
c adder_0_1_carryout <-> 367
c adder_0_1_carry8 <-> 367
c adder_0_1_propagate_generate0_3_to_8 <-> 368
c adder_0_1_propagategenerate6_6_to_4_7 <-> 369
c adder_0_1_propagategenerate5_5_to_4_7 <-> 370
c adder_0_1_propagategenerate4_4_to_4_7 <-> 371
c adder_0_1_propagate_generate4_4_to_6 <-> 372
c adder_0_1_carry7 <-> 375
c adder_0_1_propagate_generate5_5_to_7 <-> 376
c adder_0_1_propagate_generate4_4_to_7 <-> 377
c adder_0_1_carry6 <-> 378
c adder_0_1_carry5 <-> 379
c adder_0_1_propagatecarry4to7 <-> 380
c adder_0_1_propagatecarry4to6 <-> 381
c adder_0_1_propagatecarry4to5 <-> 382
c adder_0_1_carry4 <-> 383
c adder_0_1_generate0_3 <-> 383
c adder_0_1_propagategenerate2_2_to_0_3 <-> 384
c adder_0_1_propagategenerate1_1_to_0_3 <-> 385
c adder_0_1_carry3 <-> 386
c adder_0_1_propagate_generate1_1_to_3 <-> 387
c adder_1_0_propagate9_9 <-> 388
c adder_0_1_sum7 <-> 388
c adder_0_1_sum6 <-> 389
c and_1_17_ <-> 390
c adder_0_1_generate6_6 <-> 390
c xxor_1_17_ <-> 391
c adder_0_1_propagate6_6 <-> 391
c adder_0_1_sum5 <-> 392
c adder_0_1_generate5_5 <-> 393
c adder_0_1_propagate5_5 <-> 394
c adder_0_1_sum4 <-> 395
c adder_0_1_generate4_4 <-> 396
c adder_0_1_propagate4_4 <-> 397
c adder_0_1_sum3 <-> 398
c adder_0_1_generate3_3 <-> 399
c adder_0_1_propagate3_3 <-> 400
c adder_0_1_sum2 <-> 401
c adder_0_1_generate2_2 <-> 402
c adder_0_1_propagate2_2 <-> 403
c adder_0_1_carry2 <-> 404
c adder_0_1_generate1_1 <-> 404
c adder_0_1_sum1 <-> 405
c adder_0_1_propagate1_1 <-> 405
c adder_0_0_carryout <-> 406
c adder_0_0_carry8 <-> 406
c adder_0_0_propagate_generate0_3_to_8 <-> 407
c adder_0_0_propagategenerate6_6_to_4_7 <-> 408
c adder_0_0_propagategenerate5_5_to_4_7 <-> 409
c adder_0_0_propagategenerate4_4_to_4_7 <-> 410
c adder_0_0_propagate_generate4_4_to_6 <-> 411
c adder_0_0_carry7 <-> 414
c adder_0_0_propagate_generate5_5_to_7 <-> 415
c adder_0_0_propagate_generate4_4_to_7 <-> 416
c adder_0_0_carry6 <-> 417
c adder_0_0_carry5 <-> 418
c adder_0_0_propagatecarry4to7 <-> 419
c adder_0_0_propagatecarry4to6 <-> 420
c adder_0_0_propagatecarry4to5 <-> 421
c adder_0_0_carry4 <-> 422
c adder_0_0_generate0_3 <-> 422
c adder_0_0_propagategenerate2_2_to_0_3 <-> 423
c adder_0_0_propagategenerate1_1_to_0_3 <-> 424
c adder_0_0_carry3 <-> 425
c adder_0_0_propagate_generate1_1_to_3 <-> 426
c adder_0_0_sum7 <-> 427
c adder_0_0_sum6 <-> 428
c and_1_5_ <-> 429
c adder_5_1_carryout_ <-> 429
c adder_0_0_generate6_6 <-> 429
c xxor_1_5_ <-> 430
c adder_5_1_out_ <-> 430
c adder_0_0_propagate6_6 <-> 430
c adder_0_0_sum5 <-> 431
c and_1_4_ <-> 432
c adder_4_1_carryout_ <-> 432
c adder_0_0_generate5_5 <-> 432
c xxor_1_4_ <-> 433
c adder_4_1_out_ <-> 433
c adder_0_0_propagate5_5 <-> 433
c adder_0_0_sum4 <-> 434
c and_1_3_ <-> 435
c adder_3_1_carryout_ <-> 435
c adder_0_0_generate4_4 <-> 435
c xxor_1_3_ <-> 436
c adder_3_1_out_ <-> 436
c adder_0_0_propagate4_4 <-> 436
c adder_0_0_sum3 <-> 437
c and_1_2_ <-> 438
c adder_2_1_carryout_ <-> 438
c adder_0_0_generate3_3 <-> 438
c xxor_1_2_ <-> 439
c adder_2_1_out_ <-> 439
c adder_0_0_propagate3_3 <-> 439
c adder_0_0_sum2 <-> 440
c and_1_1_ <-> 441
c adder_1_1_carryout_ <-> 441
c adder_0_0_generate2_2 <-> 441
c xxor_1_1_ <-> 442
c adder_1_1_out_ <-> 442
c adder_0_0_propagate2_2 <-> 442
c and_1_0_ <-> 443
c adder_0_1_carryout_ <-> 443
c adder_0_0_carry2 <-> 443
c adder_0_0_generate1_1 <-> 443
c a6_and_b6_ <-> 444
c adder_0_3_sum6 <-> 444
c a6_and_b6 <-> 444
c a6_and_b5_ <-> 445
c adder_0_2_propagate7_7 <-> 445
c a6_and_b5 <-> 445
c a6_and_b4_ <-> 446
c a6_and_b4 <-> 446
c a6_and_b3_ <-> 447
c adder_0_1_propagate7_7 <-> 447
c a6_and_b3 <-> 447
c a6_and_b2_ <-> 448
c a6_and_b2 <-> 448
c a6_and_b1_ <-> 449
c adder_0_0_propagate7_7 <-> 449
c a6_and_b1 <-> 449
c a6_and_b0_ <-> 450
c a6_and_b0 <-> 450
c a6 <-> 451
c a5_and_b6_ <-> 452
c adder_0_3_sum5 <-> 452
c a5_and_b6 <-> 452
c a5_and_b5_ <-> 453
c a5_and_b5 <-> 453
c a5_and_b4_ <-> 454
c a5_and_b4 <-> 454
c a5_and_b3_ <-> 455
c a5_and_b3 <-> 455
c a5_and_b2_ <-> 456
c a5_and_b2 <-> 456
c a5_and_b1_ <-> 457
c a5_and_b1 <-> 457
c a5_and_b0_ <-> 458
c a5_and_b0 <-> 458
c a5 <-> 459
c a4_and_b6_ <-> 460
c adder_0_3_sum4 <-> 460
c a4_and_b6 <-> 460
c a4_and_b5_ <-> 461
c a4_and_b5 <-> 461
c a4_and_b4_ <-> 462
c a4_and_b4 <-> 462
c a4_and_b3_ <-> 463
c a4_and_b3 <-> 463
c a4_and_b2_ <-> 464
c a4_and_b2 <-> 464
c a4_and_b1_ <-> 465
c a4_and_b1 <-> 465
c a4_and_b0_ <-> 466
c a4_and_b0 <-> 466
c a4 <-> 467
c a3_and_b6_ <-> 468
c adder_0_3_sum3 <-> 468
c a3_and_b6 <-> 468
c a3_and_b5_ <-> 469
c a3_and_b5 <-> 469
c a3_and_b4_ <-> 470
c a3_and_b4 <-> 470
c a3_and_b3_ <-> 471
c a3_and_b3 <-> 471
c a3_and_b2_ <-> 472
c a3_and_b2 <-> 472
c a3_and_b1_ <-> 473
c a3_and_b1 <-> 473
c a3_and_b0_ <-> 474
c a3_and_b0 <-> 474
c a3 <-> 475
c a2_and_b6_ <-> 476
c adder_0_3_sum2 <-> 476
c a2_and_b6 <-> 476
c a2_and_b5_ <-> 477
c a2_and_b5 <-> 477
c a2_and_b4_ <-> 478
c a2_and_b4 <-> 478
c a2_and_b3_ <-> 479
c a2_and_b3 <-> 479
c a2_and_b2_ <-> 480
c a2_and_b2 <-> 480
c a2_and_b1_ <-> 481
c a2_and_b1 <-> 481
c a2_and_b0_ <-> 482
c a2_and_b0 <-> 482
c a2 <-> 483
c a1_and_b6_ <-> 484
c adder_0_3_sum1 <-> 484
c a1_and_b6 <-> 484
c a1_and_b5_ <-> 485
c a1_and_b5 <-> 485
c a1_and_b4_ <-> 486
c a1_and_b4 <-> 486
c a1_and_b3_ <-> 487
c a1_and_b3 <-> 487
c a1_and_b2_ <-> 488
c a1_and_b2 <-> 488
c a1_and_b1_ <-> 489
c a1_and_b1 <-> 489
c a1_and_b0_ <-> 490
c a1_and_b0 <-> 490
c a1 <-> 491
c a0_and_b6_ <-> 492
c adder_0_3_sum0 <-> 492
c a0_and_b6 <-> 492
c b6 <-> 493
c a0_and_b5_ <-> 494
c a0_and_b5 <-> 494
c b5 <-> 495
c a0_and_b4_ <-> 496
c adder_1_1_sum0 <-> 496
c adder_1_1_propagate0_0 <-> 496
c adder_0_2_sum0 <-> 496
c adder_0_2_propagate0_0 <-> 496
c a0_and_b4 <-> 496
c b4 <-> 497
c a0_and_b3_ <-> 498
c a0_and_b3 <-> 498
c b3 <-> 499
c a0_and_b2_ <-> 500
c adder_0_1_sum0 <-> 500
c adder_0_1_propagate0_0 <-> 500
c a0_and_b2 <-> 500
c b2 <-> 501
c a0_and_b1_ <-> 502
c a0_and_b1 <-> 502
c b1 <-> 503
c b0 <-> 504
c a0 <-> 505
p cnf 505 1696
-1 2 0
-1 3 0
-1 4 0
-1 5 0
-1 6 0
-1 7 0
-1 8 0
-1 9 0
-1 10 0
-1 11 0
-1 12 0
-1 13 0
1 -13 -12 -11 -10 -9 -8 -7 -6 -5 -4 -3 -2 0
-1 0
2 215 16 0
2 -215 -16 0
-2 215 -16 0
-2 -215 16 0
3 216 18 0
3 -216 -18 0
-3 216 -18 0
-3 -216 18 0
4 217 23 0
4 -217 -23 0
-4 217 -23 0
-4 -217 23 0
5 220 28 0
5 -220 -28 0
-5 220 -28 0
-5 -220 28 0
6 223 33 0
6 -223 -33 0
-6 223 -33 0
-6 -223 33 0
7 226 38 0
7 -226 -38 0
-7 226 -38 0
-7 -226 38 0
8 229 42 0
8 -229 -42 0
-8 229 -42 0
-8 -229 42 0
9 232 70 0
9 -232 -70 0
-9 232 -70 0
-9 -232 70 0
10 235 98 0
10 -235 -98 0
-10 235 -98 0
-10 -235 98 0
11 239 128 0
11 -239 -128 0
-11 239 -128 0
-11 -239 128 0
12 323 156 0
12 -323 -156 0
-12 323 -156 0
-12 -323 156 0
13 327 186 0
13 -327 -186 0
-13 327 -186 0
-13 -327 186 0
-14 -493 0
-14 -495 0
-14 -497 0
-14 -499 0
-14 -501 0
-14 -503 0
-14 504 0
14 -504 503 501 499 497 495 493 0
-14 0
-15 -451 0
-15 -459 0
-15 -467 0
-15 -475 0
-15 -483 0
-15 -491 0
-15 505 0
15 -505 491 483 475 467 459 451 0
-15 0
16 -17 0
16 -19 0
-16 19 17 0
-17 20 0
-17 21 0
17 -21 -20 0
18 21 -20 0
18 -21 20 0
-18 21 20 0
-18 -21 -20 0
-19 43 0
-19 444 0
19 -444 -43 0
20 444 -43 0
20 -444 43 0
-20 444 43 0
-20 -444 -43 0
21 -22 0
21 -24 0
-21 24 22 0
-22 25 0
-22 26 0
22 -26 -25 0
23 26 -25 0
23 -26 25 0
-23 26 25 0
-23 -26 -25 0
-24 45 0
-24 48 0
24 -48 -45 0
25 48 -45 0
25 -48 45 0
-25 48 45 0
-25 -48 -45 0
26 -27 0
26 -29 0
-26 29 27 0
-27 30 0
-27 31 0
27 -31 -30 0
28 31 -30 0
28 -31 30 0
-28 31 30 0
-28 -31 -30 0
-29 50 0
-29 53 0
29 -53 -50 0
30 53 -50 0
30 -53 50 0
-30 53 50 0
-30 -53 -50 0
31 -32 0
31 -34 0
-31 34 32 0
-32 35 0
-32 36 0
32 -36 -35 0
33 36 -35 0
33 -36 35 0
-33 36 35 0
-33 -36 -35 0
-34 55 0
-34 58 0
34 -58 -55 0
35 58 -55 0
35 -58 55 0
-35 58 55 0
-35 -58 -55 0
36 -37 0
36 -39 0
-36 39 37 0
-37 40 0
-37 41 0
37 -41 -40 0
38 41 -40 0
38 -41 40 0
-38 41 40 0
-38 -41 -40 0
-39 60 0
-39 63 0
39 -63 -60 0
40 63 -60 0
40 -63 60 0
-40 63 60 0
-40 -63 -60 0
-41 65 0
-41 68 0
41 -68 -65 0
42 68 -65 0
42 -68 65 0
-42 68 65 0
-42 -68 -65 0
43 -44 0
43 -46 0
-43 46 44 0
-44 47 0
-44 73 0
44 -73 -47 0
45 73 -47 0
45 -73 47 0
-45 73 47 0
-45 -73 -47 0
-46 445 0
-46 452 0
46 -452 -445 0
47 452 -445 0
47 -452 445 0
-47 452 445 0
-47 -452 -445 0
48 -49 0
48 -51 0
-48 51 49 0
-49 52 0
-49 76 0
49 -76 -52 0
50 76 -52 0
50 -76 52 0
-50 76 52 0
-50 -76 -52 0
-51 75 0
-51 460 0
51 -460 -75 0
52 460 -75 0
52 -460 75 0
-52 460 75 0
-52 -460 -75 0
53 -54 0
53 -56 0
-53 56 54 0
-54 57 0
-54 81 0
54 -81 -57 0
55 81 -57 0
55 -81 57 0
-55 81 57 0
-55 -81 -57 0
-56 78 0
-56 468 0
56 -468 -78 0
57 468 -78 0
57 -468 78 0
-57 468 78 0
-57 -468 -78 0
58 -59 0
58 -61 0
-58 61 59 0
-59 62 0
-59 86 0
59 -86 -62 0
60 86 -62 0
60 -86 62 0
-60 86 62 0
-60 -86 -62 0
-61 83 0
-61 476 0
61 -476 -83 0
62 476 -83 0
62 -476 83 0
-62 476 83 0
-62 -476 -83 0
63 -64 0
63 -66 0
-63 66 64 0
-64 67 0
-64 91 0
64 -91 -67 0
65 91 -67 0
65 -91 67 0
-65 91 67 0
-65 -91 -67 0
-66 88 0
-66 484 0
66 -484 -88 0
67 484 -88 0
67 -484 88 0
-67 484 88 0
-67 -484 -88 0
68 -69 0
68 -71 0
-68 71 69 0
-69 72 0
-69 96 0
69 -96 -72 0
70 96 -72 0
70 -96 72 0
-70 96 72 0
-70 -96 -72 0
-71 93 0
-71 492 0
71 -492 -93 0
72 492 -93 0
72 -492 93 0
-72 492 93 0
-72 -492 -93 0
73 -74 0
73 -351 0
-73 351 74 0
-74 101 0
-74 352 0
74 -352 -101 0
75 352 -101 0
75 -352 101 0
-75 352 101 0
-75 -352 -101 0
76 -77 0
76 -79 0
-76 79 77 0
-77 80 0
-77 106 0
77 -106 -80 0
78 106 -80 0
78 -106 80 0
-78 106 80 0
-78 -106 -80 0
-79 103 0
-79 461 0
79 -461 -103 0
80 461 -103 0
80 -461 103 0
-80 461 103 0
-80 -461 -103 0
81 -82 0
81 -84 0
-81 84 82 0
-82 85 0
-82 111 0
82 -111 -85 0
83 111 -85 0
83 -111 85 0
-83 111 85 0
-83 -111 -85 0
-84 108 0
-84 469 0
84 -469 -108 0
85 469 -108 0
85 -469 108 0
-85 469 108 0
-85 -469 -108 0
86 -87 0
86 -89 0
-86 89 87 0
-87 90 0
-87 116 0
87 -116 -90 0
88 116 -90 0
88 -116 90 0
-88 116 90 0
-88 -116 -90 0
-89 113 0
-89 477 0
89 -477 -113 0
90 477 -113 0
90 -477 113 0
-90 477 113 0
-90 -477 -113 0
91 -92 0
91 -94 0
-91 94 92 0
-92 95 0
-92 121 0
92 -121 -95 0
93 121 -95 0
93 -121 95 0
-93 121 95 0
-93 -121 -95 0
-94 118 0
-94 485 0
94 -485 -118 0
95 485 -118 0
95 -485 118 0
-95 485 118 0
-95 -485 -118 0
96 -97 0
96 -99 0
-96 99 97 0
-97 100 0
-97 126 0
97 -126 -100 0
98 126 -100 0
98 -126 100 0
-98 126 100 0
-98 -126 -100 0
-99 123 0
-99 494 0
99 -494 -123 0
100 494 -123 0
100 -494 123 0
-100 494 123 0
-100 -494 -123 0
101 -102 0
101 -104 0
-101 104 102 0
-102 105 0
-102 131 0
102 -131 -105 0
103 131 -105 0
103 -131 105 0
-103 131 105 0
-103 -131 -105 0
-104 447 0
-104 454 0
104 -454 -447 0
105 454 -447 0
105 -454 447 0
-105 454 447 0
-105 -454 -447 0
106 -107 0
106 -109 0
-106 109 107 0
-107 110 0
-107 134 0
107 -134 -110 0
108 134 -110 0
108 -134 110 0
-108 134 110 0
-108 -134 -110 0
-109 133 0
-109 462 0
109 -462 -133 0
110 462 -133 0
110 -462 133 0
-110 462 133 0
-110 -462 -133 0
111 -112 0
111 -114 0
-111 114 112 0
-112 115 0
-112 139 0
112 -139 -115 0
113 139 -115 0
113 -139 115 0
-113 139 115 0
-113 -139 -115 0
-114 136 0
-114 470 0
114 -470 -136 0
115 470 -136 0
115 -470 136 0
-115 470 136 0
-115 -470 -136 0
116 -117 0
116 -119 0
-116 119 117 0
-117 120 0
-117 144 0
117 -144 -120 0
118 144 -120 0
118 -144 120 0
-118 144 120 0
-118 -144 -120 0
-119 141 0
-119 478 0
119 -478 -141 0
120 478 -141 0
120 -478 141 0
-120 478 141 0
-120 -478 -141 0
121 -122 0
121 -124 0
-121 124 122 0
-122 125 0
-122 149 0
122 -149 -125 0
123 149 -125 0
123 -149 125 0
-123 149 125 0
-123 -149 -125 0
-124 146 0
-124 486 0
124 -486 -146 0
125 486 -146 0
125 -486 146 0
-125 486 146 0
-125 -486 -146 0
126 -127 0
126 -129 0
-126 129 127 0
-127 130 0
-127 154 0
127 -154 -130 0
128 154 -130 0
128 -154 130 0
-128 154 130 0
-128 -154 -130 0
-129 151 0
-129 496 0
129 -496 -151 0
130 496 -151 0
130 -496 151 0
-130 496 151 0
-130 -496 -151 0
131 -132 0
131 -390 0
-131 390 132 0
-132 159 0
-132 391 0
132 -391 -159 0
133 391 -159 0
133 -391 159 0
-133 391 159 0
-133 -391 -159 0
134 -135 0
134 -137 0
-134 137 135 0
-135 138 0
-135 164 0
135 -164 -138 0
136 164 -138 0
136 -164 138 0
-136 164 138 0
-136 -164 -138 0
-137 161 0
-137 463 0
137 -463 -161 0
138 463 -161 0
138 -463 161 0
-138 463 161 0
-138 -463 -161 0
139 -140 0
139 -142 0
-139 142 140 0
-140 169 0
-140 143 0
140 -143 -169 0
141 143 -169 0
141 -143 169 0
-141 143 169 0
-141 -143 -169 0
-142 166 0
-142 471 0
142 -471 -166 0
143 471 -166 0
143 -471 166 0
-143 471 166 0
-143 -471 -166 0
144 -145 0
144 -147 0
-144 147 145 0
-145 174 0
-145 148 0
145 -148 -174 0
146 148 -174 0
146 -148 174 0
-146 148 174 0
-146 -148 -174 0
-147 171 0
-147 479 0
147 -479 -171 0
148 479 -171 0
148 -479 171 0
-148 479 171 0
-148 -479 -171 0
149 -150 0
149 -152 0
-149 152 150 0
-150 179 0
-150 153 0
150 -153 -179 0
151 153 -179 0
151 -153 179 0
-151 153 179 0
-151 -153 -179 0
-152 176 0
-152 487 0
152 -487 -176 0
153 487 -176 0
153 -487 176 0
-153 487 176 0
-153 -487 -176 0
154 -155 0
154 -157 0
-154 157 155 0
-155 184 0
-155 158 0
155 -158 -184 0
156 158 -184 0
156 -158 184 0
-156 158 184 0
-156 -158 -184 0
-157 181 0
-157 498 0
157 -498 -181 0
158 498 -181 0
158 -498 181 0
-158 498 181 0
-158 -498 -181 0
159 -162 0
159 -160 0
-159 160 162 0
-160 163 0
-160 429 0
160 -429 -163 0
161 429 -163 0
161 -429 163 0
-161 429 163 0
-161 -429 -163 0
-162 449 0
-162 456 0
162 -456 -449 0
163 456 -449 0
163 -456 449 0
-163 456 449 0
-163 -456 -449 0
164 -165 0
164 -167 0
-164 167 165 0
-165 168 0
-165 432 0
165 -432 -168 0
166 432 -168 0
166 -432 168 0
-166 432 168 0
-166 -432 -168 0
-167 430 0
-167 464 0
167 -464 -430 0
168 464 -430 0
168 -464 430 0
-168 464 430 0
-168 -464 -430 0
169 -170 0
169 -172 0
-169 172 170 0
-170 173 0
-170 435 0
170 -435 -173 0
171 435 -173 0
171 -435 173 0
-171 435 173 0
-171 -435 -173 0
-172 433 0
-172 472 0
172 -472 -433 0
173 472 -433 0
173 -472 433 0
-173 472 433 0
-173 -472 -433 0
174 -175 0
174 -177 0
-174 177 175 0
-175 178 0
-175 438 0
175 -438 -178 0
176 438 -178 0
176 -438 178 0
-176 438 178 0
-176 -438 -178 0
-177 436 0
-177 480 0
177 -480 -436 0
178 480 -436 0
178 -480 436 0
-178 480 436 0
-178 -480 -436 0
179 -180 0
179 -182 0
-179 182 180 0
-180 183 0
-180 441 0
180 -441 -183 0
181 441 -183 0
181 -441 183 0
-181 441 183 0
-181 -441 -183 0
-182 439 0
-182 488 0
182 -488 -439 0
183 488 -439 0
183 -488 439 0
-183 488 439 0
-183 -488 -439 0
184 -185 0
184 -187 0
-184 187 185 0
-185 188 0
-185 443 0
185 -443 -188 0
186 443 -188 0
186 -443 188 0
-186 443 188 0
-186 -443 -188 0
-187 442 0
-187 500 0
187 -500 -442 0
188 500 -442 0
188 -500 442 0
-188 500 442 0
-188 -500 -442 0
189 -190 0
189 -192 0
189 -193 0
189 -194 0
189 -218 0
-189 218 194 193 192 190 0
-190 203 0
-190 219 0
190 -219 -203 0
-191 189 0
-191 260 0
191 -260 -189 0
-192 219 0
-192 221 0
192 -221 -219 0
-193 199 0
-193 219 0
193 -219 -199 0
-194 200 0
-194 219 0
194 -219 -200 0
-195 225 0
-195 227 0
195 -227 -225 0
-196 197 0
-196 222 0
196 -222 -197 0
-197 225 0
-197 228 0
197 -228 -225 0
198 -199 0
198 -200 0
198 -203 0
198 -221 0
-198 221 203 200 199 0
-199 222 0
-199 224 0
199 -224 -222 0
-200 195 0
-200 222 0
200 -222 -195 0
201 -195 0
201 -204 0
201 -224 0
-201 224 204 195 0
202 -205 0
202 -227 0
-202 227 205 0
-203 196 0
-203 206 0
203 -206 -196 0
-204 197 0
-204 206 0
204 -206 -197 0
-205 206 0
-205 228 0
205 -228 -206 0
206 -207 0
206 -208 0
206 -209 0
206 -230 0
-206 230 209 208 207 0
-207 231 0
-207 233 0
207 -233 -231 0
-208 212 0
-208 231 0
208 -231 -212 0
-209 213 0
-209 231 0
209 -231 -213 0
-210 237 0
-210 238 0
210 -238 -237 0
211 -212 0
211 -213 0
211 -233 0
-211 233 213 212 0
-212 234 0
-212 236 0
212 -236 -234 0
-213 210 0
-213 234 0
213 -234 -210 0
214 -210 0
214 -236 0
-214 236 210 0
215 242 -191 0
215 -242 191 0
-215 242 191 0
-215 -242 -191 0
216 260 -189 0
216 -260 189 0
-216 260 189 0
-216 -260 -189 0
217 219 -198 0
217 -219 198 0
-217 219 198 0
-217 -219 -198 0
-218 263 0
-218 282 0
218 -282 -263 0
219 282 -263 0
219 -282 263 0
-219 282 263 0
-219 -282 -263 0
220 222 -201 0
220 -222 201 0
-220 222 201 0
-220 -222 -201 0
-221 266 0
-221 306 0
221 -306 -266 0
222 306 -266 0
222 -306 266 0
-222 306 266 0
-222 -306 -266 0
223 225 -202 0
223 -225 202 0
-223 225 202 0
-223 -225 -202 0
-224 269 0
-224 307 0
224 -307 -269 0
225 307 -269 0
225 -307 269 0
-225 307 269 0
-225 -307 -269 0
226 228 -206 0
226 -228 206 0
-226 228 206 0
-226 -228 -206 0
-227 272 0
-227 308 0
227 -308 -272 0
228 308 -272 0
228 -308 272 0
-228 308 272 0
-228 -308 -272 0
229 231 -211 0
229 -231 211 0
-229 231 211 0
-229 -231 -211 0
-230 275 0
-230 311 0
230 -311 -275 0
231 311 -275 0
231 -311 275 0
-231 311 275 0
-231 -311 -275 0
232 234 -214 0
232 -234 214 0
-232 234 214 0
-232 -234 -214 0
-233 279 0
-233 314 0
233 -314 -279 0
234 314 -279 0
234 -314 279 0
-234 314 279 0
-234 -314 -279 0
235 238 -237 0
235 -238 237 0
-235 238 237 0
-235 -238 -237 0
-236 317 0
-236 366 0
236 -366 -317 0
237 366 -317 0
237 -366 317 0
-237 366 317 0
-237 -366 -317 0
-238 320 0
-238 496 0
238 -496 -320 0
239 496 -320 0
239 -496 320 0
-239 496 320 0
-239 -496 -320 0
240 -241 0
240 -244 0
240 -245 0
240 -246 0
240 -264 0
-240 264 246 245 244 241 0
-241 255 0
-241 265 0
241 -265 -255 0
242 -243 0
242 -261 0
-242 261 243 0
-243 240 0
-243 262 0
243 -262 -240 0
-244 265 0
-244 267 0
244 -267 -265 0
-245 251 0
-245 265 0
245 -265 -251 0
-246 252 0
-246 265 0
246 -265 -252 0
-247 271 0
-247 273 0
247 -273 -271 0
-248 249 0
-248 268 0
248 -268 -249 0
-249 271 0
-249 274 0
249 -274 -271 0
250 -251 0
250 -252 0
250 -255 0
250 -267 0
-250 267 255 252 251 0
-251 268 0
-251 270 0
251 -270 -268 0
-252 247 0
-252 268 0
252 -268 -247 0
253 -247 0
253 -256 0
253 -270 0
-253 270 256 247 0
254 -257 0
254 -273 0
-254 273 257 0
-255 248 0
-255 258 0
255 -258 -248 0
-256 249 0
-256 258 0
256 -258 -249 0
-257 258 0
-257 274 0
257 -274 -258 0
258 -259 0
258 -276 0
-258 276 259 0
-259 277 0
-259 278 0
259 -278 -277 0
260 262 -240 0
260 -262 240 0
-260 262 240 0
-260 -262 -240 0
-261 328 0
-261 444 0
261 -444 -328 0
262 444 -328 0
262 -444 328 0
-262 444 328 0
-262 -444 -328 0
263 265 -250 0
263 -265 250 0
-263 265 250 0
-263 -265 -250 0
-264 349 0
-264 452 0
264 -452 -349 0
265 452 -349 0
265 -452 349 0
-265 452 349 0
-265 -452 -349 0
266 268 -253 0
266 -268 253 0
-266 268 253 0
-266 -268 -253 0
-267 350 0
-267 460 0
267 -460 -350 0
268 460 -350 0
268 -460 350 0
-268 460 350 0
-268 -460 -350 0
269 271 -254 0
269 -271 254 0
-269 271 254 0
-269 -271 -254 0
-270 353 0
-270 468 0
270 -468 -353 0
271 468 -353 0
271 -468 353 0
-271 468 353 0
-271 -468 -353 0
272 274 -258 0
272 -274 258 0
-272 274 258 0
-272 -274 -258 0
-273 356 0
-273 476 0
273 -476 -356 0
274 476 -356 0
274 -476 356 0
-274 476 356 0
-274 -476 -356 0
275 278 -277 0
275 -278 277 0
-275 278 277 0
-275 -278 -277 0
-276 359 0
-276 484 0
276 -484 -359 0
277 484 -359 0
277 -484 359 0
-277 484 359 0
-277 -484 -359 0
-278 362 0
-278 492 0
278 -492 -362 0
279 492 -362 0
279 -492 362 0
-279 492 362 0
-279 -492 -362 0
280 -290 0
280 -291 0
280 -292 0
280 -312 0
280 -281 0
-280 281 312 292 291 290 0
-281 301 0
-281 313 0
281 -313 -301 0
282 -283 0
282 -287 0
-282 287 283 0
-283 285 0
-283 367 0
283 -367 -285 0
284 -285 0
284 -288 0
-284 288 285 0
-285 309 0
-285 388 0
285 -388 -309 0
286 -289 0
286 -309 0
-286 309 289 0
-287 288 0
-287 367 0
287 -367 -288 0
-288 289 0
-288 388 0
288 -388 -289 0
-289 310 0
-289 280 0
289 -280 -310 0
-290 313 0
-290 315 0
290 -315 -313 0
-291 297 0
-291 313 0
291 -313 -297 0
-292 298 0
-292 313 0
292 -313 -298 0
-293 319 0
-293 321 0
293 -321 -319 0
-294 295 0
-294 316 0
294 -316 -295 0
-295 319 0
-295 322 0
295 -322 -319 0
296 -297 0
296 -298 0
296 -301 0
296 -315 0
-296 315 301 298 297 0
-297 316 0
-297 318 0
297 -318 -316 0
-298 293 0
-298 316 0
298 -316 -293 0
299 -293 0
299 -302 0
299 -318 0
-299 318 302 293 0
300 -303 0
300 -321 0
-300 321 303 0
-301 294 0
-301 304 0
301 -304 -294 0
-302 295 0
-302 304 0
302 -304 -295 0
-303 304 0
-303 322 0
303 -322 -304 0
304 -305 0
304 -324 0
-304 324 305 0
-305 325 0
-305 326 0
305 -326 -325 0
306 367 -284 0
306 -367 284 0
-306 367 284 0
-306 -367 -284 0
307 388 -286 0
307 -388 286 0
-307 388 286 0
-307 -388 -286 0
308 280 -310 0
308 -280 310 0
-308 280 310 0
-308 -280 -310 0
-309 389 0
-309 406 0
309 -406 -389 0
310 406 -389 0
310 -406 389 0
-310 406 389 0
-310 -406 -389 0
311 313 -296 0
311 -313 296 0
-311 313 296 0
-311 -313 -296 0
-312 392 0
-312 427 0
312 -427 -392 0
313 427 -392 0
313 -427 392 0
-313 427 392 0
-313 -427 -392 0
314 316 -299 0
314 -316 299 0
-314 316 299 0
-314 -316 -299 0
-315 395 0
-315 428 0
315 -428 -395 0
316 428 -395 0
316 -428 395 0
-316 428 395 0
-316 -428 -395 0
317 319 -300 0
317 -319 300 0
-317 319 300 0
-317 -319 -300 0
-318 398 0
-318 431 0
318 -431 -398 0
319 431 -398 0
319 -431 398 0
-319 431 398 0
-319 -431 -398 0
320 322 -304 0
320 -322 304 0
-320 322 304 0
-320 -322 -304 0
-321 401 0
-321 434 0
321 -434 -401 0
322 434 -401 0
322 -434 401 0
-322 434 401 0
-322 -434 -401 0
323 326 -325 0
323 -326 325 0
-323 326 325 0
-323 -326 -325 0
-324 405 0
-324 437 0
324 -437 -405 0
325 437 -405 0
325 -437 405 0
-325 437 405 0
-325 -437 -405 0
-326 440 0
-326 500 0
326 -500 -440 0
327 500 -440 0
327 -500 440 0
-327 500 440 0
-327 -500 -440 0
328 -329 0
328 -330 0
328 -331 0
328 -332 0
-328 332 331 330 329 0
-329 341 0
-329 445 0
329 -445 -341 0
-330 351 0
-330 445 0
330 -445 -351 0
-331 337 0
-331 445 0
331 -445 -337 0
-332 338 0
-332 445 0
332 -445 -338 0
-333 355 0
-333 357 0
333 -357 -355 0
-334 335 0
-334 352 0
334 -352 -335 0
-335 355 0
-335 358 0
335 -358 -355 0
336 -337 0
336 -338 0
336 -341 0
336 -351 0
-336 351 341 338 337 0
-337 352 0
-337 354 0
337 -354 -352 0
-338 333 0
-338 352 0
338 -352 -333 0
339 -333 0
339 -342 0
339 -354 0
-339 354 342 333 0
340 -343 0
340 -357 0
-340 357 343 0
-341 334 0
-341 344 0
341 -344 -334 0
-342 335 0
-342 344 0
342 -344 -335 0
-343 344 0
-343 358 0
343 -358 -344 0
344 -345 0
344 -346 0
344 -360 0
-344 360 346 345 0
-345 361 0
-345 363 0
345 -363 -361 0
-346 348 0
-346 361 0
346 -361 -348 0
347 -348 0
347 -363 0
-347 363 348 0
-348 364 0
-348 365 0
348 -365 -364 0
349 445 -336 0
349 -445 336 0
-349 445 336 0
-349 -445 -336 0
350 352 -339 0
350 -352 339 0
-350 352 339 0
-350 -352 -339 0
-351 446 0
-351 453 0
351 -453 -446 0
352 453 -446 0
352 -453 446 0
-352 453 446 0
-352 -453 -446 0
353 355 -340 0
353 -355 340 0
-353 355 340 0
-353 -355 -340 0
-354 454 0
-354 461 0
354 -461 -454 0
355 461 -454 0
355 -461 454 0
-355 461 454 0
-355 -461 -454 0
356 358 -344 0
356 -358 344 0
-356 358 344 0
-356 -358 -344 0
-357 462 0
-357 469 0
357 -469 -462 0
358 469 -462 0
358 -469 462 0
-358 469 462 0
-358 -469 -462 0
359 361 -347 0
359 -361 347 0
-359 361 347 0
-359 -361 -347 0
-360 470 0
-360 477 0
360 -477 -470 0
361 477 -470 0
361 -477 470 0
-361 477 470 0
-361 -477 -470 0
362 365 -364 0
362 -365 364 0
-362 365 364 0
-362 -365 -364 0
-363 478 0
-363 485 0
363 -485 -478 0
364 485 -478 0
364 -485 478 0
-364 485 478 0
-364 -485 -478 0
-365 486 0
-365 494 0
365 -494 -486 0
366 494 -486 0
366 -494 486 0
-366 494 486 0
-366 -494 -486 0
367 -368 0
367 -370 0
367 -371 0
367 -369 0
-367 369 371 370 368 0
-368 380 0
-368 447 0
368 -447 -380 0
-369 390 0
-369 447 0
369 -447 -390 0
-370 376 0
-370 447 0
370 -447 -376 0
-371 377 0
-371 447 0
371 -447 -377 0
-372 394 0
-372 396 0
372 -396 -394 0
-373 374 0
-373 391 0
373 -391 -374 0
-374 394 0
-374 397 0
374 -397 -394 0
375 -376 0
375 -377 0
375 -380 0
375 -390 0
-375 390 380 377 376 0
-376 391 0
-376 393 0
376 -393 -391 0
-377 372 0
-377 391 0
377 -391 -372 0
378 -372 0
378 -381 0
378 -393 0
-378 393 381 372 0
379 -382 0
379 -396 0
-379 396 382 0
-380 373 0
-380 383 0
380 -383 -373 0
-381 374 0
-381 383 0
381 -383 -374 0
-382 383 0
-382 397 0
382 -397 -383 0
383 -384 0
383 -385 0
383 -399 0
-383 399 385 384 0
-384 400 0
-384 402 0
384 -402 -400 0
-385 387 0
-385 400 0
385 -400 -387 0
386 -387 0
386 -402 0
-386 402 387 0
-387 403 0
-387 404 0
387 -404 -403 0
388 447 -375 0
388 -447 375 0
-388 447 375 0
-388 -447 -375 0
389 391 -378 0
389 -391 378 0
-389 391 378 0
-389 -391 -378 0
-390 448 0
-390 455 0
390 -455 -448 0
391 455 -448 0
391 -455 448 0
-391 455 448 0
-391 -455 -448 0
392 394 -379 0
392 -394 379 0
-392 394 379 0
-392 -394 -379 0
-393 456 0
-393 463 0
393 -463 -456 0
394 463 -456 0
394 -463 456 0
-394 463 456 0
-394 -463 -456 0
395 397 -383 0
395 -397 383 0
-395 397 383 0
-395 -397 -383 0
-396 464 0
-396 471 0
396 -471 -464 0
397 471 -464 0
397 -471 464 0
-397 471 464 0
-397 -471 -464 0
398 400 -386 0
398 -400 386 0
-398 400 386 0
-398 -400 -386 0
-399 472 0
-399 479 0
399 -479 -472 0
400 479 -472 0
400 -479 472 0
-400 479 472 0
-400 -479 -472 0
401 404 -403 0
401 -404 403 0
-401 404 403 0
-401 -404 -403 0
-402 480 0
-402 487 0
402 -487 -480 0
403 487 -480 0
403 -487 480 0
-403 487 480 0
-403 -487 -480 0
-404 488 0
-404 498 0
404 -498 -488 0
405 498 -488 0
405 -498 488 0
-405 498 488 0
-405 -498 -488 0
406 -407 0
406 -408 0
406 -409 0
406 -410 0
-406 410 409 408 407 0
-407 419 0
-407 449 0
407 -449 -419 0
-408 429 0
-408 449 0
408 -449 -429 0
-409 415 0
-409 449 0
409 -449 -415 0
-410 416 0
-410 449 0
410 -449 -416 0
-411 433 0
-411 435 0
411 -435 -433 0
-412 413 0
-412 430 0
412 -430 -413 0
-413 433 0
-413 436 0
413 -436 -433 0
414 -415 0
414 -416 0
414 -419 0
414 -429 0
-414 429 419 416 415 0
-415 430 0
-415 432 0
415 -432 -430 0
-416 411 0
-416 430 0
416 -430 -411 0
417 -411 0
417 -420 0
417 -432 0
-417 432 420 411 0
418 -421 0
418 -435 0
-418 435 421 0
-419 412 0
-419 422 0
419 -422 -412 0
-420 413 0
-420 422 0
420 -422 -413 0
-421 422 0
-421 436 0
421 -436 -422 0
422 -423 0
422 -424 0
422 -438 0
-422 438 424 423 0
-423 439 0
-423 441 0
423 -441 -439 0
-424 426 0
-424 439 0
424 -439 -426 0
425 -426 0
425 -441 0
-425 441 426 0
-426 442 0
-426 443 0
426 -443 -442 0
427 449 -414 0
427 -449 414 0
-427 449 414 0
-427 -449 -414 0
428 430 -417 0
428 -430 417 0
-428 430 417 0
-428 -430 -417 0
-429 450 0
-429 457 0
429 -457 -450 0
430 457 -450 0
430 -457 450 0
-430 457 450 0
-430 -457 -450 0
431 433 -418 0
431 -433 418 0
-431 433 418 0
-431 -433 -418 0
-432 458 0
-432 465 0
432 -465 -458 0
433 465 -458 0
433 -465 458 0
-433 465 458 0
-433 -465 -458 0
434 436 -422 0
434 -436 422 0
-434 436 422 0
-434 -436 -422 0
-435 466 0
-435 473 0
435 -473 -466 0
436 473 -466 0
436 -473 466 0
-436 473 466 0
-436 -473 -466 0
437 439 -425 0
437 -439 425 0
-437 439 425 0
-437 -439 -425 0
-438 474 0
-438 481 0
438 -481 -474 0
439 481 -474 0
439 -481 474 0
-439 481 474 0
-439 -481 -474 0
440 443 -442 0
440 -443 442 0
-440 443 442 0
-440 -443 -442 0
-441 482 0
-441 489 0
441 -489 -482 0
442 489 -482 0
442 -489 482 0
-442 489 482 0
-442 -489 -482 0
-443 490 0
-443 502 0
443 -502 -490 0
-444 451 0
-444 493 0
444 -493 -451 0
-445 451 0
-445 495 0
445 -495 -451 0
-446 451 0
-446 497 0
446 -497 -451 0
-447 451 0
-447 499 0
447 -499 -451 0
-448 451 0
-448 501 0
448 -501 -451 0
-449 451 0
-449 503 0
449 -503 -451 0
-450 451 0
-450 504 0
450 -504 -451 0
-452 459 0
-452 493 0
452 -493 -459 0
-453 459 0
-453 495 0
453 -495 -459 0
-454 459 0
-454 497 0
454 -497 -459 0
-455 459 0
-455 499 0
455 -499 -459 0
-456 459 0
-456 501 0
456 -501 -459 0
-457 459 0
-457 503 0
457 -503 -459 0
-458 459 0
-458 504 0
458 -504 -459 0
-460 467 0
-460 493 0
460 -493 -467 0
-461 467 0
-461 495 0
461 -495 -467 0
-462 467 0
-462 497 0
462 -497 -467 0
-463 467 0
-463 499 0
463 -499 -467 0
-464 467 0
-464 501 0
464 -501 -467 0
-465 467 0
-465 503 0
465 -503 -467 0
-466 467 0
-466 504 0
466 -504 -467 0
-468 475 0
-468 493 0
468 -493 -475 0
-469 475 0
-469 495 0
469 -495 -475 0
-470 475 0
-470 497 0
470 -497 -475 0
-471 475 0
-471 499 0
471 -499 -475 0
-472 475 0
-472 501 0
472 -501 -475 0
-473 475 0
-473 503 0
473 -503 -475 0
-474 475 0
-474 504 0
474 -504 -475 0
-476 483 0
-476 493 0
476 -493 -483 0
-477 483 0
-477 495 0
477 -495 -483 0
-478 483 0
-478 497 0
478 -497 -483 0
-479 483 0
-479 499 0
479 -499 -483 0
-480 483 0
-480 501 0
480 -501 -483 0
-481 483 0
-481 503 0
481 -503 -483 0
-482 483 0
-482 504 0
482 -504 -483 0
-484 491 0
-484 493 0
484 -493 -491 0
-485 491 0
-485 495 0
485 -495 -491 0
-486 491 0
-486 497 0
486 -497 -491 0
-487 491 0
-487 499 0
487 -499 -491 0
-488 491 0
-488 501 0
488 -501 -491 0
-489 491 0
-489 503 0
489 -503 -491 0
-490 491 0
-490 504 0
490 -504 -491 0
-492 493 0
-492 505 0
492 -505 -493 0
-494 495 0
-494 505 0
494 -505 -495 0
-496 497 0
-496 505 0
496 -505 -497 0
-498 499 0
-498 505 0
498 -505 -499 0
-500 501 0
-500 505 0
500 -505 -501 0
-502 503 0
-502 505 0
502 -505 -503 0

To submit this form, please press this button:

To reset this form to its initial setting, please press this button:

Imprint / Impressum | Data Protection / Datenschutzhinweis