Name | normalized-opb/mps-v2-20-10/MIPLIB/miplib/normalized-mps-v2-20-10-p2756.opb |
MD5SUM | cc9b9a1bf5f3e0998bc97d2eed5cbbd9 |
Bench Category | optimization, small integers (OPTSMALLINT) |
Has Objective Function | YES |
Satisfiable | YES |
(Un)Satisfiability was proved | YES |
Best value of the objective function | 4605 |
Optimality of the best value was proved | NO |
Number of terms in the objective function | 2166 |
Biggest coefficient in the objective function | 11000 |
Number of bits for the biggest coefficient in the objective function | 14 |
Sum of the numbers in the objective function | 321831 |
Number of bits of the sum of numbers in the objective function | 19 |
Biggest number in a constraint | 11000 |
Number of bits of the biggest number in a constraint | 14 |
Biggest sum of numbers in a constraint | 321831 |
Number of bits of the biggest sum of numbers | 19 |
Best result obtained on this benchmark | SAT |
Best CPU time to get the best result obtained on this benchmark | 1.07384 |
Number of variables | 2756 |
Total number of constraints | 3511 |
Number of constraints which are clauses | 132 |
Number of constraints which are cardinality constraints (but not clauses) | 2976 |
Number of constraints which are nor clauses,nor cardinality constraints | 403 |
Minimum length of a constraint | 1 |
Maximum length of a constraint | 546 |
#### BEGIN LAUNCHER DATA #### LAUNCH ON wulflinc11 THE 2005-04-22 01:58:57 (client local time) PB2005-SCRIPT v4.0 MARKUPS: idlaunch=12180 boxname=wulflinc11 idbench=937 idsolver=12 numberseed=0 MD5SUM SOLVER: MD5SUM BENCH: cc9b9a1bf5f3e0998bc97d2eed5cbbd9 /oldhome/oroussel/tmp/wulflinc11/normalized-mps-v2-20-10-p2756.opb REAL COMMAND: minisat+ -cb -gs /oldhome/oroussel/tmp/wulflinc11/normalized-mps-v2-20-10-p2756.opb /oldhome/oroussel/tmp/wulflinc11/normalized-mps-v2-20-10-p2756.opb IDLAUNCH: 12180 /proc/cpuinfo: processor : 0 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 2 cpu MHz : 451.028 cache size : 512 KB fdiv_bug : no hlt_bug : no f00f_bug : no coma_bug : no fpu : yes fpu_exception : yes cpuid level : 2 wp : yes flags : fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse bogomips : 888.83 processor : 1 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 2 cpu MHz : 451.028 cache size : 512 KB fdiv_bug : no hlt_bug : no f00f_bug : no coma_bug : no fpu : yes fpu_exception : yes cpuid level : 2 wp : yes flags : fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse bogomips : 899.07 /proc/meminfo: MemTotal: 1034660 kB MemFree: 309428 kB Buffers: 34960 kB Cached: 668160 kB SwapCached: 0 kB Active: 250644 kB Inactive: 455184 kB HighTotal: 131008 kB HighFree: 29148 kB LowTotal: 903652 kB LowFree: 280280 kB SwapTotal: 2097136 kB SwapFree: 2097048 kB Dirty: 28 kB Writeback: 0 kB Mapped: 6820 kB Slab: 13612 kB Committed_AS: 63600 kB PageTables: 316 kB VmallocTotal: 114680 kB VmallocUsed: 1364 kB VmallocChunk: 113256 kB JOB ENDED THE 2005-04-22 02:19:00 (client local time) WITH STATUS 10 IN 1200.33 SECONDS stats: 12180 7 1200.33 10 #### END LAUNCHER DATA #### #### BEGIN SOLVER DATA #### c Parsing PB file... c Converting 738 PB-constraints to clauses... c -- Unit propagations: (none) c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): ssssssssss..ssssss.sss.ssss.................................................................................................................................... c ---[ 759]---> BDD-cost: 31 c ---[ 758]---> BDD-cost: 19 c ---[ 757]---> BDD-cost: 15 c ---[ 756]---> BDD-cost: 135 c ---[ 755]---> BDD-cost: 81 c ---[ 754]---> BDD-cost: 36 c ---[ 753]---> BDD-cost: 18 c ---[ 752]---> BDD-cost: 9 c ---[ 751]---> BDD-cost: 160 c ---[ 750]---> BDD-cost: 50 c ---[ 749]---> BDD-cost: 31 c ---[ 748]---> BDD-cost: 14 c ---[ 746]---> BDD-cost: 232 c ---[ 745]---> BDD-cost: 64 c ---[ 744]---> BDD-cost: 37 c ---[ 743]---> BDD-cost: 17 c ---[ 742]---> BDD-cost: 29 c ---[ 741]---> BDD-cost: 202 c ---[ 740]---> BDD-cost: 34 c ---[ 739]---> BDD-cost: 11 c ---[ 738]---> BDD-cost: 77 c ---[ 737]---> BDD-cost: 59 c ---[ 736]---> BDD-cost: 117 c ---[ 735]---> BDD-cost: 105 c ---[ 734]---> BDD-cost: 66 c ---[ 733]---> BDD-cost: 51 c ---[ 732]---> BDD-cost: 96 c ---[ 731]---> BDD-cost: 143 c ---[ 730]---> BDD-cost: 148 c ---[ 729]---> BDD-cost: 69 c ---[ 728]---> BDD-cost: 35 c ---[ 727]---> BDD-cost: 91 c ---[ 726]---> BDD-cost: 15 c ---[ 725]---> BDD-cost: 8 c ---[ 724]---> BDD-cost: 46 c ---[ 723]---> BDD-cost: 108 c ---[ 722]---> BDD-cost: 160 c ---[ 721]---> BDD-cost: 510 c ---[ 720]---> BDD-cost: 367 c ---[ 719]---> BDD-cost: 102 c ---[ 718]---> BDD-cost: 188 c ---[ 717]---> BDD-cost: 163 c ---[ 716]---> BDD-cost: 165 c ---[ 715]---> BDD-cost: 90 c ---[ 714]---> BDD-cost: 158 c ---[ 713]---> BDD-cost: 23 c ---[ 712]---> BDD-cost: 8 c ---[ 711]---> BDD-cost: 47 c ---[ 710]---> BDD-cost: 25 c ---[ 709]---> BDD-cost: 143 c ---[ 708]---> BDD-cost: 163 c ---[ 707]---> BDD-cost: 485 c ---[ 706]---> BDD-cost: 342 c ---[ 705]---> BDD-cost: 109 c ---[ 704]---> BDD-cost: 190 c ---[ 703]---> BDD-cost: 145 c ---[ 702]---> BDD-cost: 132 c ---[ 701]---> BDD-cost: 76 c ---[ 700]---> BDD-cost: 111 c ---[ 698]---> BDD-cost: 52 c ---[ 696]---> BDD-cost: 53 c ---[ 695]---> BDD-cost: 53 c ---[ 694]---> BDD-cost: 132 c ---[ 693]---> BDD-cost: 56 c ---[ 692]---> BDD-cost: 56 c ---[ 691]---> BDD-cost: 75 c ---[ 690]---> BDD-cost: 55 c ---[ 689]---> BDD-cost: 50 c ---[ 688]---> BDD-cost: 61 c ---[ 687]---> BDD-cost: 83 c ---[ 686]---> BDD-cost: 133 c ---[ 685]---> BDD-cost: 52 c ---[ 684]---> BDD-cost: 93 c ---[ 683]---> BDD-cost: 125 c ---[ 682]---> BDD-cost: 50 c ---[ 681]---> BDD-cost: 96 c ---[ 680]---> BDD-cost: 344 c ---[ 679]---> BDD-cost: 378 c ---[ 678]---> BDD-cost: 879 c ---[ 677]---> BDD-cost: 252 c ---[ 676]---> BDD-cost: 356 c ---[ 675]---> BDD-cost: 253 c ---[ 674]---> BDD-cost: 63 c ---[ 673]---> BDD-cost: 177 c ---[ 672]---> BDD-cost: 596 c ---[ 671]---> BDD-cost: 833 c ---[ 670]---> BDD-cost: 1052 c ---[ 669]---> BDD-cost: 113 c ---[ 668]---> BDD-cost: 702 c ---[ 667]---> BDD-cost: 190 c ---[ 666]---> BDD-cost: 157 c ---[ 665]---> BDD-cost: 236 c ---[ 663]---> BDD-cost: 378 c ---[ 662]---> BDD-cost: 109 c ---[ 661]---> BDD-cost: 231 c ---[ 660]---> BDD-cost: 449 c ---[ 658]---> BDD-cost: 318 c ---[ 657]---> BDD-cost: 379 c ---[ 656]---> BDD-cost: 216 c ---[ 655]---> BDD-cost: 415 c ---[ 653]---> BDD-cost: 105 c ---[ 652]---> BDD-cost: 475 c ---[ 651]---> BDD-cost: 100 c ---[ 650]---> BDD-cost: 317 c ---[ 649]---> BDD-cost: 131 c ---[ 648]---> BDD-cost: 193 c ---[ 647]---> BDD-cost: 186 c ---[ 646]---> BDD-cost: 67 c ---[ 645]---> BDD-cost: 111 c ---[ 644]---> BDD-cost: 243 c ---[ 643]---> BDD-cost: 236 c ---[ 642]---> BDD-cost: 413 c ---[ 641]---> BDD-cost: 193 c ---[ 640]---> BDD-cost: 64 c ---[ 639]---> BDD-cost: 126 c ---[ 638]---> BDD-cost: 103 c ---[ 637]---> BDD-cost: 110 c ---[ 636]---> BDD-cost: 410 c ---[ 635]---> BDD-cost: 183 c ---[ 634]---> BDD-cost: 70 c ---[ 633]---> BDD-cost: 114 c ---[ 632]---> BDD-cost: 186 c ---[ 631]---> BDD-cost: 191 c ---[ 630]---> BDD-cost: 424 c ---[ 629]---> BDD-cost: 193 c ---[ 628]---> BDD-cost: 44 c ---[ 627]---> BDD-cost: 144 c ---[ 626]---> BDD-cost: 90 c ---[ 625]---> BDD-cost: 63 c ---[ 624]---> BDD-cost: 336 c ---[ 623]---> BDD-cost: 440 c ---[ 622]---> BDD-cost: 202 c ---[ 621]---> BDD-cost: 5 c ---[ 620]---> BDD-cost: 22 c ---[ 619]---> BDD-cost: 105 c ---[ 618]---> BDD-cost: 87 c ---[ 617]---> BDD-cost: 104 c ---[ 616]---> BDD-cost: 70 c ---[ 615]---> BDD-cost: 143 c ---[ 614]---> BDD-cost: 188 c ---[ 613]---> BDD-cost: 147 c ---[ 612]---> BDD-cost: 151 c ---[ 611]---> BDD-cost: 144 c ---[ 610]---> BDD-cost: 31 c ---[ 609]---> BDD-cost: 103 c ---[ 608]---> BDD-cost: 89 c ---[ 607]---> BDD-cost: 101 c ---[ 606]---> BDD-cost: 62 c ---[ 605]---> BDD-cost: 142 c ---[ 604]---> BDD-cost: 189 c ---[ 603]---> BDD-cost: 147 c ---[ 602]---> BDD-cost: 157 c ---[ 601]---> BDD-cost: 146 c ---[ 600]---> BDD-cost: 32 c ---[ 599]---> BDD-cost: 112 c ---[ 598]---> BDD-cost: 90 c ---[ 597]---> BDD-cost: 102 c ---[ 596]---> BDD-cost: 70 c ---[ 595]---> BDD-cost: 136 c ---[ 594]---> BDD-cost: 201 c ---[ 593]---> BDD-cost: 159 c ---[ 592]---> BDD-cost: 154 c ---[ 591]---> BDD-cost: 148 c ---[ 590]---> BDD-cost: 18 c ---[ 589]---> BDD-cost: 540 c ---[ 588]---> BDD-cost: 370 c ---[ 587]---> BDD-cost: 266 c ---[ 586]---> BDD-cost: 134 c ---[ 585]---> BDD-cost: 76 c ---[ 584]---> BDD-cost: 835 c ---[ 583]---> BDD-cost: 34 c ---[ 582]---> BDD-cost: 27 c ---[ 580]---> BDD-cost: 11 c ---[ 578]---> BDD-cost: 16 c ---[ 577]---> BDD-cost: 66 c ---[ 575]---> BDD-cost: 10 c ---[ 573]---> BDD-cost: 40 c ---[ 572]---> BDD-cost: 79 c ---[ 569]---> BDD-cost: 9 c ---[ 568]---> BDD-cost: 14 c ---[ 567]---> BDD-cost: 10 c ---[ 566]---> BDD-cost: 54 c ---[ 565]---> BDD-cost: 66 c ---[ 564]---> BDD-cost: 14 c ---[ 563]---> BDD-cost: 16 c ---[ 562]---> BDD-cost: 10 c ---[ 561]---> BDD-cost: 51 c ---[ 560]---> BDD-cost: 54 c ---[ 559]---> BDD-cost: 7 c ---[ 557]---> BDD-cost: 9 c ---[ 556]---> BDD-cost: 8 c ---[ 555]---> BDD-cost: 23 c ---[ 554]---> BDD-cost: 85 c ---[ 553]---> BDD-cost: 57 c ---[ 552]---> BDD-cost: 7 c ---[ 551]---> BDD-cost: 9 c ---[ 550]---> BDD-cost: 37 c ---[ 549]---> BDD-cost: 36 c ---[ 548]---> BDD-cost: 84 c ---[ 547]---> BDD-cost: 55 c ---[ 546]---> BDD-cost: 13 c ---[ 545]---> BDD-cost: 13 c ---[ 544]---> BDD-cost: 21 c ---[ 543]---> BDD-cost: 47 c ---[ 541]---> BDD-cost: 17 c ---[ 540]---> BDD-cost: 37 c ---[ 539]---> BDD-cost: 272 c ---[ 538]---> BDD-cost: 223 c ---[ 537]---> BDD-cost: 22 c ---[ 536]---> BDD-cost: 64 c ---[ 535]---> BDD-cost: 70 c ---[ 532]---> BDD-cost: 77 c ---[ 531]---> BDD-cost: 11 c ---[ 530]---> BDD-cost: 20 c ---[ 529]---> BDD-cost: 42 c ---[ 528]---> BDD-cost: 3 c ---[ 527]---> BDD-cost: 23 c ---[ 526]---> BDD-cost: 32 c ---[ 525]---> BDD-cost: 272 c ---[ 524]---> BDD-cost: 218 c ---[ 523]---> BDD-cost: 21 c ---[ 522]---> BDD-cost: 40 c ---[ 521]---> BDD-cost: 31 c ---[ 518]---> BDD-cost: 82 c ---[ 517]---> BDD-cost: 15 c ---[ 516]---> BDD-cost: 12 c ---[ 515]---> BDD-cost: 14 c ---[ 514]---> BDD-cost: 16 c ---[ 513]---> BDD-cost: 13 c ---[ 512]---> BDD-cost: 43 c ---[ 511]---> BDD-cost: 35 c ---[ 510]---> BDD-cost: 10 c ---[ 509]---> BDD-cost: 12 c ---[ 508]---> BDD-cost: 18 c ---[ 507]---> BDD-cost: 13 c ---[ 506]---> BDD-cost: 15 c ---[ 505]---> BDD-cost: 13 c ---[ 504]---> BDD-cost: 43 c ---[ 503]---> BDD-cost: 39 c ---[ 502]---> BDD-cost: 27 c ---[ 501]---> BDD-cost: 13 c ---[ 500]---> BDD-cost: 15 c ---[ 499]---> BDD-cost: 6 c ---[ 498]---> BDD-cost: 56 c ---[ 497]---> BDD-cost: 39 c ---[ 496]---> BDD-cost: 180 c ---[ 495]---> BDD-cost: 124 c ---[ 494]---> BDD-cost: 46 c ---[ 493]---> BDD-cost: 36 c ---[ 492]---> BDD-cost: 26 c ---[ 491]---> BDD-cost: 22 c ---[ 490]---> BDD-cost: 144 c ---[ 489]---> BDD-cost: 139 c ---[ 488]---> BDD-cost: 268 c ---[ 486]---> BDD-cost: 137 c ---[ 485]---> BDD-cost: 20 c ---[ 484]---> BDD-cost: 41 c ---[ 483]---> BDD-cost: 94 c ---[ 482]---> BDD-cost: 17 c ---[ 481]---> BDD-cost: 215 c ---[ 480]---> BDD-cost: 13 c ---[ 479]---> BDD-cost: 39 c ---[ 478]---> BDD-cost: 261 c ---[ 477]---> BDD-cost: 17 c ---[ 476]---> BDD-cost: 40 c ---[ 475]---> BDD-cost: 87 c ---[ 473]---> BDD-cost: 229 c ---[ 472]---> BDD-cost: 18 c ---[ 471]---> BDD-cost: 22 c ---[ 470]---> BDD-cost: 258 c ---[ 469]---> BDD-cost: 4 c ---[ 468]---> BDD-cost: 51 c ---[ 467]---> BDD-cost: 58 c ---[ 465]---> BDD-cost: 63 c ---[ 464]---> BDD-cost: 35 c ---[ 463]---> BDD-cost: 30 c ---[ 462]---> BDD-cost: 168 c ---[ 461]---> BDD-cost: 148 c ---[ 460]---> BDD-cost: 114 c ---[ 459]---> BDD-cost: 77 c ---[ 458]---> BDD-cost: 45 c ---[ 457]---> BDD-cost: 37 c ---[ 454]---> BDD-cost: 196 c ---[ 453]---> BDD-cost: 68 c ---[ 452]---> BDD-cost: 37 c ---[ 451]---> BDD-cost: 30 c ---[ 450]---> BDD-cost: 162 c ---[ 449]---> BDD-cost: 136 c ---[ 448]---> BDD-cost: 163 c ---[ 447]---> BDD-cost: 94 c ---[ 446]---> BDD-cost: 48 c ---[ 445]---> BDD-cost: 58 c ---[ 444]---> BDD-cost: 13 c ---[ 442]---> BDD-cost: 228 c ---[ 441]---> BDD-cost: 119 c ---[ 440]---> BDD-cost: 78 c ---[ 438]---> BDD-cost: 5 c ---[ 437]---> BDD-cost: 11 c ---[ 436]---> BDD-cost: 15 c ---[ 435]---> BDD-cost: 15 c ---[ 434]---> BDD-cost: 19 c ---[ 433]---> BDD-cost: 10 c ---[ 432]---> BDD-cost: 118 c ---[ 431]---> BDD-cost: 55 c ---[ 430]---> BDD-cost: 47 c ---[ 429]---> BDD-cost: 54 c ---[ 428]---> BDD-cost: 33 c ---[ 427]---> BDD-cost: 74 c ---[ 426]---> BDD-cost: 13 c ---[ 425]---> BDD-cost: 13 c ---[ 424]---> BDD-cost: 23 c ---[ 423]---> BDD-cost: 4 c ---[ 422]---> BDD-cost: 127 c ---[ 421]---> BDD-cost: 49 c ---[ 420]---> BDD-cost: 45 c ---[ 419]---> BDD-cost: 61 c ---[ 418]---> BDD-cost: 32 c ---[ 417]---> BDD-cost: 75 c ---[ 416]---> BDD-cost: 18 c ---[ 415]---> BDD-cost: 18 c ---[ 414]---> BDD-cost: 23 c ---[ 413]---> BDD-cost: 4 c ---[ 412]---> BDD-cost: 111 c ---[ 411]---> BDD-cost: 62 c ---[ 410]---> BDD-cost: 53 c ---[ 409]---> BDD-cost: 60 c ---[ 408]---> BDD-cost: 29 c ---[ 407]---> BDD-cost: 85 c ---[ 406]---> BDD-cost: 254 c ---[ 405]---> BDD-cost: 219 c ---[ 404]---> BDD-cost: 25 c ---[ 402]---> BDD-cost: 10 c ---[ 401]---> BDD-cost: 189 c ---[ 400]---> BDD-cost: 17 c ---[ 399]---> BDD-cost: 14 c ---[ 397]---> BDD-cost:195145 c ---[ 396]---> BDD-cost: 2456 c ---[ 395]---> BDD-cost: 7851 c ---[ 394]---> BDD-cost:11061 c ---[ 393]---> BDD-cost:17352 c ---[ 392]---> BDD-cost: 9650 c ---[ 391]---> BDD-cost: 99 c ---[ 390]---> BDD-cost: 52 c ---[ 389]---> BDD-cost: 5 c ---[ 386]---> BDD-cost: 5 c ---[ 384]---> BDD-cost: 5 c ---[ 383]---> BDD-cost: 5 c ---[ 381]---> BDD-cost: 5 c ---[ 379]---> BDD-cost: 5 c ---[ 376]---> BDD-cost: 5 c ---[ 374]---> BDD-cost: 5 c ---[ 373]---> BDD-cost: 5 c ---[ 371]---> BDD-cost: 5 c ---[ 369]---> BDD-cost: 3 c ---[ 368]---> BDD-cost: 3 c ---[ 367]---> BDD-cost: 3 c ---[ 366]---> BDD-cost: 5 c ---[ 363]---> BDD-cost: 5 c ---[ 361]---> BDD-cost: 5 c ---[ 360]---> BDD-cost: 5 c ---[ 358]---> BDD-cost: 5 c ---[ 356]---> BDD-cost: 5 c ---[ 353]---> BDD-cost: 5 c ---[ 351]---> BDD-cost: 5 c ---[ 350]---> BDD-cost: 5 c ---[ 348]---> BDD-cost: 5 c ---[ 346]---> BDD-cost: 3 c ---[ 345]---> BDD-cost: 3 c ---[ 344]---> BDD-cost: 3 c ---[ 343]---> BDD-cost: 5 c ---[ 341]---> BDD-cost: 5 c ---[ 339]---> BDD-cost: 3 c ---[ 337]---> BDD-cost: 3 c ---[ 334]---> BDD-cost: 3 c ---[ 333]---> BDD-cost: 5 c ---[ 331]---> BDD-cost: 5 c ---[ 328]---> BDD-cost: 3 c ---[ 325]---> BDD-cost: 3 c ---[ 324]---> BDD-cost: 3 c ---[ 323]---> BDD-cost: 5 c ---[ 322]---> BDD-cost: 5 c ---[ 321]---> BDD-cost: 3 c ---[ 320]---> BDD-cost: 5 c ---[ 317]---> BDD-cost: 5 c ---[ 316]---> BDD-cost: 3 c ---[ 314]---> BDD-cost: 5 c ---[ 312]---> BDD-cost: 3 c ---[ 311]---> BDD-cost: 5 c ---[ 308]---> BDD-cost: 5 c ---[ 307]---> BDD-cost: 3 c ---[ 305]---> BDD-cost: 5 c ---[ 303]---> BDD-cost: 3 c ---[ 302]---> BDD-cost: 3 c ---[ 301]---> BDD-cost: 5 c ---[ 300]---> BDD-cost: 5 c ---[ 299]---> BDD-cost: 3 c ---[ 298]---> BDD-cost: 5 c ---[ 295]---> BDD-cost: 5 c ---[ 294]---> BDD-cost: 3 c ---[ 292]---> BDD-cost: 5 c ---[ 290]---> BDD-cost: 3 c ---[ 289]---> BDD-cost: 5 c ---[ 286]---> BDD-cost: 5 c ---[ 285]---> BDD-cost: 3 c ---[ 283]---> BDD-cost: 5 c ---[ 281]---> BDD-cost: 3 c ---[ 280]---> BDD-cost: 5 c ---[ 277]---> BDD-cost: 5 c ---[ 274]---> BDD-cost: 5 c ---[ 272]---> BDD-cost: 3 c ---[ 269]---> BDD-cost: 3 c ---[ 268]---> BDD-cost: 5 c ---[ 265]---> BDD-cost: 5 c ---[ 262]---> BDD-cost: 5 c ---[ 260]---> BDD-cost: 3 c ---[ 257]---> BDD-cost: 3 c ---[ 256]---> BDD-cost: 5 c ---[ 255]---> BDD-cost: 5 c ---[ 252]---> BDD-cost: 5 c ---[ 251]---> BDD-cost: 5 c ---[ 249]---> BDD-cost: 5 c ---[ 248]---> BDD-cost: 5 c ---[ 246]---> BDD-cost: 5 c ---[ 245]---> BDD-cost: 5 c ---[ 244]---> BDD-cost: 5 c ---[ 242]---> BDD-cost: 5 c ---[ 241]---> BDD-cost: 5 c ---[ 240]---> BDD-cost: 3 c ---[ 238]---> BDD-cost: 5 c ---[ 236]---> BDD-cost: 5 c ---[ 235]---> BDD-cost: 5 c ---[ 234]---> BDD-cost: 3 c ---[ 233]---> BDD-cost: 5 c ---[ 232]---> BDD-cost: 5 c ---[ 229]---> BDD-cost: 5 c ---[ 228]---> BDD-cost: 5 c ---[ 226]---> BDD-cost: 5 c ---[ 225]---> BDD-cost: 5 c ---[ 223]---> BDD-cost: 5 c ---[ 222]---> BDD-cost: 5 c ---[ 221]---> BDD-cost: 5 c ---[ 219]---> BDD-cost: 5 c ---[ 218]---> BDD-cost: 5 c ---[ 217]---> BDD-cost: 3 c ---[ 215]---> BDD-cost: 5 c ---[ 213]---> BDD-cost: 5 c ---[ 212]---> BDD-cost: 5 c ---[ 211]---> BDD-cost: 3 c ---[ 210]---> BDD-cost: 5 c ---[ 209]---> BDD-cost: 5 c ---[ 208]---> BDD-cost: 3 c ---[ 207]---> BDD-cost: 5 c ---[ 206]---> BDD-cost: 5 c ---[ 205]---> BDD-cost: 5 c ---[ 204]---> BDD-cost: 5 c ---[ 203]---> BDD-cost: 5 c ---[ 202]---> BDD-cost: 5 c ---[ 201]---> BDD-cost: 3 c ---[ 200]---> BDD-cost: 5 c ---[ 199]---> BDD-cost: 5 c ---[ 197]---> BDD-cost: 5 c ---[ 196]---> BDD-cost: 5 c ---[ 194]---> BDD-cost: 5 c ---[ 193]---> BDD-cost: 5 c ---[ 192]---> BDD-cost: 5 c ---[ 191]---> BDD-cost: 5 c ---[ 189]---> BDD-cost: 5 c ---[ 188]---> BDD-cost: 5 c ---[ 186]---> BDD-cost: 5 c ---[ 185]---> BDD-cost: 5 c ---[ 183]---> BDD-cost: 5 c ---[ 182]---> BDD-cost: 5 c ---[ 181]---> BDD-cost: 5 c ---[ 180]---> BDD-cost: 5 c ---[ 178]---> BDD-cost: 5 c ---[ 177]---> BDD-cost: 5 c ---[ 175]---> BDD-cost: 5 c ---[ 174]---> BDD-cost: 5 c ---[ 172]---> BDD-cost: 5 c ---[ 171]---> BDD-cost: 5 c ---[ 170]---> BDD-cost: 5 c ---[ 168]---> BDD-cost: 5 c ---[ 167]---> BDD-cost: 5 c ---[ 165]---> BDD-cost: 5 c ---[ 164]---> BDD-cost: 5 c ---[ 162]---> BDD-cost: 5 c ---[ 161]---> BDD-cost: 5 c ---[ 160]---> BDD-cost: 5 c ---[ 158]---> BDD-cost: 5 c ---[ 155]---> BDD-cost: 5 c ---[ 153]---> BDD-cost: 5 c ---[ 152]---> BDD-cost: 3 c ---[ 150]---> BDD-cost: 5 c ---[ 148]---> BDD-cost: 5 c ---[ 147]---> BDD-cost: 3 c ---[ 146]---> BDD-cost: 5 c ---[ 143]---> BDD-cost: 5 c ---[ 141]---> BDD-cost: 5 c ---[ 140]---> BDD-cost: 3 c ---[ 138]---> BDD-cost: 5 c ---[ 136]---> BDD-cost: 5 c ---[ 135]---> BDD-cost: 3 c ---[ 134]---> BDD-cost: 5 c ---[ 131]---> BDD-cost: 5 c ---[ 129]---> BDD-cost: 5 c ---[ 128]---> BDD-cost: 3 c ---[ 126]---> BDD-cost: 5 c ---[ 124]---> BDD-cost: 5 c ---[ 123]---> BDD-cost: 3 c ---[ 122]---> BDD-cost: 5 c ---[ 119]---> BDD-cost: 5 c ---[ 117]---> BDD-cost: 5 c ---[ 116]---> BDD-cost: 3 c ---[ 114]---> BDD-cost: 5 c ---[ 112]---> BDD-cost: 5 c ---[ 111]---> BDD-cost: 3 c ---[ 110]---> BDD-cost: 5 c ---[ 109]---> BDD-cost: 5 c ---[ 107]---> BDD-cost: 5 c ---[ 105]---> BDD-cost: 3 c ---[ 104]---> BDD-cost: 3 c ---[ 103]---> BDD-cost: 5 c ---[ 101]---> BDD-cost: 5 c ---[ 100]---> BDD-cost: 5 c ---[ 98]---> BDD-cost: 5 c ---[ 97]---> BDD-cost: 5 c ---[ 95]---> BDD-cost: 5 c ---[ 93]---> BDD-cost: 5 c ---[ 92]---> BDD-cost: 5 c ---[ 90]---> BDD-cost: 5 c ---[ 89]---> BDD-cost: 5 c ---[ 87]---> BDD-cost: 5 c ---[ 85]---> BDD-cost: 5 c ---[ 84]---> BDD-cost: 5 c ---[ 82]---> BDD-cost: 5 c ---[ 81]---> BDD-cost: 5 c ---[ 79]---> BDD-cost: 5 c ---[ 77]---> BDD-cost: 5 c ---[ 76]---> BDD-cost: 5 c ---[ 74]---> BDD-cost: 5 c ---[ 73]---> BDD-cost: 5 c ---[ 71]---> BDD-cost: 5 c ---[ 69]---> BDD-cost: 5 c ---[ 68]---> BDD-cost: 5 c ---[ 66]---> BDD-cost: 5 c ---[ 65]---> BDD-cost: 5 c ---[ 63]---> BDD-cost: 5 c ---[ 61]---> BDD-cost: 5 c ---[ 60]---> BDD-cost: 5 c ---[ 58]---> BDD-cost: 5 c ---[ 57]---> BDD-cost: 5 c ---[ 55]---> BDD-cost: 5 c ---[ 54]---> BDD-cost: 5 c ---[ 52]---> BDD-cost: 5 c ---[ 51]---> BDD-cost: 5 c ---[ 50]---> BDD-cost: 5 c ---[ 49]---> BDD-cost: 5 c ---[ 47]---> BDD-cost: 5 c ---[ 46]---> BDD-cost: 5 c ---[ 44]---> BDD-cost: 5 c ---[ 43]---> BDD-cost: 5 c ---[ 42]---> BDD-cost: 5 c ---[ 41]---> BDD-cost: 5 c ---[ 37]---> BDD-cost: 189 c ---[ 36]---> BDD-cost: 14 c ---[ 35]---> BDD-cost: 14 c ---[ 34]---> BDD-cost: 14 c ---[ 33]---> BDD-cost: 14 c ---[ 32]---> BDD-cost: 33 c ---[ 31]---> BDD-cost: 32 c ---[ 30]---> BDD-cost: 40 c ---[ 29]---> BDD-cost: 46 c ---[ 28]---> BDD-cost: 122 c ---[ 27]---> BDD-cost: 122 c ---[ 26]---> BDD-cost: 122 c ---[ 25]---> BDD-cost: 122 c ---[ 24]---> BDD-cost: 8 c ---[ 23]---> BDD-cost: 60 c ---[ 22]---> BDD-cost: 9 c ---[ 21]---> BDD-cost: 24 c ---[ 20]---> BDD-cost: 45 c ---[ 19]---> BDD-cost: 25 c ---[ 18]---> BDD-cost: 62 c ---[ 17]---> BDD-cost: 73 c ---[ 16]---> BDD-cost: 67 c ---[ 15]---> BDD-cost: 9 c ---[ 14]---> BDD-cost: 1 c ---[ 13]---> BDD-cost: 7 c ---[ 12]---> BDD-cost: 3 c ---[ 11]---> BDD-cost: 9 c ---[ 10]---> BDD-cost: 8 c ---[ 9]---> BDD-cost: 11 c ---[ 8]---> BDD-cost: 19 c ---[ 7]---> BDD-cost: 19 c ---[ 6]---> BDD-cost: 12 c ---[ 5]---> BDD-cost: 25 c ---[ 4]---> BDD-cost: 28 c ---[ 3]---> BDD-cost: 3 c ---[ 2]---> BDD-cost: 2 c ---[ 1]---> BDD-cost: 34 c ---[ 0]---> BDD-cost: 15 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 0 | 864317 2569663 | 288105 0 0 nan | 0.000 % | c | 100 | 859596 2556412 | 316915 40 1623 40.6 | 0.736 % | c | 250 | 857602 2550477 | 348607 123 4691 38.1 | 0.957 % | c | 477 | 855075 2543005 | 383467 315 14768 46.9 | 1.053 % | c | 814 | 852976 2536708 | 421814 567 20667 36.4 | 1.283 % | c | 1320 | 849364 2525872 | 463995 911 25918 28.5 | 1.712 % | c | 2079 | 840384 2498932 | 510395 1188 40183 33.8 | 2.778 % | c | 3218 | 839933 2497579 | 561435 2292 88810 38.7 | 2.834 % | c | 4927 | 833780 2479320 | 617578 3730 134487 36.1 | 3.574 % | c | 7489 | 815758 2425265 | 679336 4836 161846 33.5 | 5.709 % | c | 11334 | 800203 2378626 | 747270 6837 205841 30.1 | 7.545 % | c | 17101 | 778867 2315261 | 821997 9132 406480 44.5 | 9.626 % | c ============================================================================== c [1mFound solution: 153858[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost:688838 Base: 2 2 3 3 3 5 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 20358 | 2731613 6873566 | 910537 10680 740267 69.3 | 9.626 % | c | 20459 | 2731053 6872259 | 1001590 10770 741712 68.9 | 2.980 % | c | 20609 | 2731053 6872259 | 1101749 10920 742908 68.0 | 2.980 % | c | 20834 | 2731053 6872259 | 1211924 11145 744237 66.8 | 2.980 % | c | 21171 | 2731053 6872259 | 1333117 11482 746783 65.0 | 2.980 % | c | 21677 | 2731053 6872259 | 1466428 11988 751011 62.6 | 2.980 % | c | 22436 | 2731053 6872259 | 1613071 12747 758908 59.5 | 2.980 % | c | 23575 | 2731017 6872178 | 1774379 13885 767150 55.3 | 2.981 % | c | 25284 | 2731017 6872178 | 1951816 15594 786238 50.4 | 2.981 % | c | 27846 | 2731017 6872178 | 2146998 18156 809425 44.6 | 2.981 % | c | 31691 | 2730781 6871645 | 2361698 21998 857265 39.0 | 2.987 % | c | 37457 | 2729023 6867410 | 2597868 27675 907979 32.8 | 3.039 % | c | 46107 | 2729023 6867410 | 2857655 36325 1574611 43.3 | 3.039 % | c | 59081 | 2727413 6863624 | 3143420 49215 1685670 34.3 | 3.088 % | c | 78542 | 2725037 6857196 | 3457762 68610 2085537 30.4 | 3.169 % | c | 107734 | 2724164 6855195 | 3803539 97793 3559212 36.4 | 3.197 % | c c *** TERMINATED *** s SATISFIABLE v C1001_bit0 C1002_bit0 -C1003_bit0 C1004_bit0 -C1005_bit0 -C1006_bit0 C1009_bit0 -C1010_bit0 C1011_bit0 C1014_bit0 -C1017_bit0 C1019_bit0 -C1020_bit0 -C1021_bit0 -C1022_bit0 -C1023_bit0 C1024_bit0 C1027_bit0 -C1029_bit0 -C1030_bit0 C1031_bit0 -C1032_bit0 -C1033_bit0 C1034_bit0 C1035_bit0 -C1036_bit0 -C1037_bit0 -C1038_bit0 -C1039_bit0 C1042_bit0 -C1044_bit0 -C1045_bit0 -C1046_bit0 -C1047_bit0 -C1048_bit0 C1049_bit0 -C1050_bit0 C1051_bit0 C1054_bit0 -C1056_bit0 C1057_bit0 C1058_bit0 -C1059_bit0 -C1060_bit0 -C1061_bit0 -C1062_bit0 C1065_bit0 C1066_bit0 -C1067_bit0 C1068_bit0 C1070_bit0 C1073_bit0 C1074_bit0 -C1075_bit0 -C1076_bit0 -C1077_bit0 -C1078_bit0 -C1079_bit0 -C1080_bit0 -C1083_bit0 -C1085_bit0 -C1086_bit0 C1087_bit0 -C1088_bit0 -C1089_bit0 C1090_bit0 C1091_bit0 -C1092_bit0 C1093_bit0 -C1094_bit0 -C1095_bit0 C1098_bit0 C1100_bit0 -C1101_bit0 -C1102_bit0 -C1103_bit0 -C1104_bit0 -C1105_bit0 C1106_bit0 -C1107_bit0 -C1110_bit0 -C1112_bit0 -C1113_bit0 -C1114_bit0 -C1115_bit0 -C1116_bit0 -C1117_bit0 C1119_bit0 -C1120_bit0 C1121_bit0 -C1122_bit0 -C1123_bit0 -C1124_bit0 -C1126_bit0 -C1127_bit0 C1128_bit0 -C1129_bit0 -C1131_bit0 -C1132_bit0 -C1133_bit0 -C1134_bit0 -C1135_bit0 -C1136_bit0 -C1137_bit0 -C1139_bit0 C1140_bit0 C1141_bit0 -C1142_bit0 -C1143_bit0 -C1144_bit0 -C1145_bit0 C1148_bit0 -C1149_bit0 -C1150_bit0 C1153_bit0 C1156_bit0 -C1158_bit0 -C1159_bit0 -C1160_bit0 -C1161_bit0 -C1162_bit0 -C1163_bit0 C1166_bit0 -C1168_bit0 -C1169_bit0 -C1170_bit0 -C1171_bit0 -C1172_bit0 C1173_bit0 C1174_bit0 -C1175_bit0 C1176_bit0 -C1177_bit0 -C1178_bit0 C1181_bit0 -C1183_bit0 -C1184_bit0 -C1185_bit0 -C1186_bit0 -C1187_bit0 C1188_bit0 C1189_bit0 -C1190_bit0 C1193_bit0 -C1195_bit0 C1196_bit0 -C1197_bit0 -C1198_bit0 C1199_bit0 -C1200_bit0 -C1201_bit0 C1204_bit0 -C1205_bit0 -C1206_bit0 -C1207_bit0 C1209_bit0 C1212_bit0 C1213_bit0 C1214_bit0 C1215_bit0 C1216_bit0 -C1217_bit0 -C1218_bit0 -C1219_bit0 C1222_bit0 C1224_bit0 -C1225_bit0 C1226_bit0 -C1227_bit0 -C1228_bit0 C1229_bit0 -C1230_bit0 -C1231_bit0 C1232_bit0 -C1233_bit0 -C1234_bit0 C1237_bit0 C1239_bit0 -C1240_bit0 C1241_bit0 -C1242_bit0 -C1243_bit0 C1244_bit0 -C1245_bit0 -C1246_bit0 -C1249_bit0 -C1251_bit0 -C1252_bit0 -C1253_bit0 -C1254_bit0 -C1255_bit0 -C1256_bit0 -C1258_bit0 -C1259_bit0 -C1260_bit0 -C1261_bit0 C1262_bit0 C1263_bit0 C1265_bit0 -C1266_bit0 -C1267_bit0 -C1268_bit0 -C1270_bit0 -C1271_bit0 -C1272_bit0 -C1273_bit0 -C1274_bit0 -C1275_bit0 -C1276_bit0 -C1278_bit0 -C1279_bit0 C1280_bit0 C1281_bit0 -C1283_bit0 -C1284_bit0 -C1285_bit0 C1286_bit0 C1289_bit0 -C1290_bit0 -C1291_bit0 -C1292_bit0 -C1293_bit0 -C1294_bit0 -C1295_bit0 C1296_bit0 -C1297_bit0 -C1298_bit0 -C1299_bit0 C1300_bit0 C1303_bit0 -C1304_bit0 -C1305_bit0 -C1306_bit0 C1307_bit0 C1308_bit0 C1309_bit0 -C1310_bit0 -C1313_bit0 -C1314_bit0 C1315_bit0 C1316_bit0 C1317_bit0 C1318_bit0 C1319_bit0 -C1320_bit0 C1321_bit0 -C1322_bit0 -C1323_bit0 C1326_bit0 C1327_bit0 -C1328_bit0 C1329_bit0 C1330_bit0 C1331_bit0 C1332_bit0 C1333_bit0 C1335_bit0 -C1338_bit0 C1339_bit0 C1340_bit0 C1341_bit0 C1343_bit0 -C1344_bit0 -C1345_bit0 -C1347_bit0 C1348_bit0 -C1349_bit0 C1351_bit0 -C1352_bit0 -C1353_bit0 -C1354_bit0 -C1356_bit0 C1357_bit0 C1358_bit0 -C1359_bit0 -C1360_bit0 -C1361_bit0 -C1362_bit0 C1363_bit0 -C1366_bit0 -C1367_bit0 -C1368_bit0 C1369_bit0 C1370_bit0 -C1371_bit0 C1372_bit0 -C1373_bit0 -C1374_bit0 -C1375_bit0 -C1376_bit0 -C1377_bit0 C1380_bit0 -C1381_bit0 C1382_bit0 C1383_bit0 -C1384_bit0 -C1385_bit0 C1386_bit0 C1387_bit0 C1390_bit0 -C1391_bit0 C1392_bit0 C1393_bit0 -C1394_bit0 C1395_bit0 C1396_bit0 -C1397_bit0 C1398_bit0 -C1399_bit0 -C1400_bit0 C1403_bit0 C1404_bit0 C1405_bit0 C1406_bit0 C1407_bit0 C1408_bit0 -C1409_bit0 C1410_bit0 C1411_bit0 C1412_bit0 C1415_bit0 C1416_bit0 C1417_bit0 C1418_bit0 C1419_bit0 C1420_bit0 -C1421_bit0 C1422_bit0 C1423_bit0 -C1424_bit0 -C1425_bit0 C1426_bit0 -C1428_bit0 -C1429_bit0 -C1430_bit0 C1431_bit0 -C1432_bit0 -C1433_bit0 C1434_bit0 -C1435_bit0 -C1436_bit0 C1437_bit0 C1438_bit0 -C1439_bit0 -C1440_bit0 -C1441_bit0 -C1442_bit0 -C1443_bit0 -C1444_bit0 -C1445_bit0 -C1446_bit0 -C1447_bit0 -C1448_bit0 -C1449_bit0 C1450_bit0 -C1451_bit0 -C1452_bit0 -C1453_bit0 C1454_bit0 C1456_bit0 C1457_bit0 C1458_bit0 C1459_bit0 C1460_bit0 -C1461_bit0 C1463_bit0 -C1464_bit0 -C1465_bit0 C1466_bit0 -C1467_bit0 -C1468_bit0 C1469_bit0 -C1470_bit0 C1471_bit0 -C1472_bit0 -C1473_bit0 C1474_bit0 -C1475_bit0 -C1476_bit0 -C1479_bit0 -C1480_bit0 -C1481_bit0 -C1482_bit0 -C1483_bit0 C1484_bit0 -C1485_bit0 -C1486_bit0 -C1489_bit0 C1490_bit0 C1491_bit0 -C1492_bit0 -C1493_bit0 C1494_bit0 -C1495_bit0 -C1496_bit0 -C1497_bit0 C1498_bit0 C1499_bit0 C1500_bit0 -C1501_bit0 C1502_bit0 -C1503_bit0 C1506_bit0 C1507_bit0 C1508_bit0 C1509_bit0 C1510_bit0 -C1511_bit0 -C1512_bit0 C1513_bit0 -C1514_bit0 C1515_bit0 C1516_bit0 C1517_bit0 C1519_bit0 C1522_bit0 C1523_bit0 -C1524_bit0 C1525_bit0 C1526_bit0 -C1527_bit0 C1528_bit0 -C1529_bit0 C1530_bit0 C1531_bit0 -C1532_bit0 -C1533_bit0 C1535_bit0 -C1536_bit0 -C1537_bit0 C1538_bit0 C1539_bit0 C1540_bit0 C1541_bit0 C1542_bit0 -C1543_bit0 -C1544_bit0 -C1545_bit0 -C1546_bit0 C1549_bit0 -C1550_bit0 C1551_bit0 C1552_bit0 -C1553_bit0 C1554_bit0 -C1555_bit0 -C1556_bit0 C1559_bit0 -C1560_bit0 C1561_bit0 C1562_bit0 C1563_bit0 -C1564_bit0 C1565_bit0 -C1566_bit0 -C1567_bit0 C1568_bit0 C1569_bit0 C1570_bit0 -C1571_bit0 -C1572_bit0 -C1573_bit0 C1576_bit0 -C1577_bit0 C1578_bit0 C1579_bit0 C1580_bit0 C1581_bit0 -C1582_bit0 -C1583_bit0 -C1584_bit0 C1585_bit0 C1586_bit0 -C1587_bit0 C1588_bit0 C1589_bit0 C1592_bit0 -C1593_bit0 C1594_bit0 C1595_bit0 C1596_bit0 -C1597_bit0 C1598_bit0 C1599_bit0 C1600_bit0 C1601_bit0 -C1602_bit0 -C1603_bit0 C1605_bit0 -C1606_bit0 C1607_bit0 C1608_bit0 C1609_bit0 -C1610_bit0 C1611_bit0 -C1612_bit0 -C1613_bit0 C1614_bit0 C1615_bit0 -C1616_bit0 -C1617_bit0 -C1618_bit0 -C1619_bit0 -C1620_bit0 -C1621_bit0 -C1622_bit0 -C1623_bit0 -C1624_bit0 -C1625_bit0 -C1626_bit0 C1627_bit0 -C1628_bit0 -C1629_bit0 -C1630_bit0 C1631_bit0 C1633_bit0 C1634_bit0 C1635_bit0 C1636_bit0 C1637_bit0 C1638_bit0 -C1639_bit0 -C1640_bit0 -C1641_bit0 C1642_bit0 -C1643_bit0 -C1644_bit0 -C1645_bit0 C1646_bit0 C1647_bit0 C1648_bit0 -C1650_bit0 C1651_bit0 -C1652_bit0 -C1653_bit0 C1656_bit0 -C1657_bit0 C1658_bit0 C1659_bit0 C1660_bit0 C1661_bit0 -C1662_bit0 C1663_bit0 C1666_bit0 -C1667_bit0 C1668_bit0 C1669_bit0 -C1670_bit0 -C1671_bit0 -C1672_bit0 -C1673_bit0 -C1674_bit0 C1675_bit0 C1676_bit0 C1677_bit0 C1678_bit0 -C1679_bit0 -C1680_bit0 C1683_bit0 C1684_bit0 C1685_bit0 C1686_bit0 C1687_bit0 -C1688_bit0 C1689_bit0 -C1690_bit0 -C1691_bit0 C1692_bit0 C1693_bit0 C1694_bit0 C1696_bit0 C1699_bit0 C1700_bit0 C1701_bit0 C1702_bit0 C1703_bit0 C1704_bit0 C1705_bit0 -C1706_bit0 -C1707_bit0 -C1708_bit0 C1709_bit0 -C1710_bit0 C1712_bit0 -C1713_bit0 C1714_bit0 C1715_bit0 C1716_bit0 -C1717_bit0 C1718_bit0 -C1719_bit0 C1720_bit0 -C1721_bit0 -C1722_bit0 -C1723_bit0 C1726_bit0 -C1727_bit0 C1728_bit0 C1729_bit0 C1730_bit0 -C1731_bit0 C1732_bit0 -C1733_bit0 C1736_bit0 -C1737_bit0 C1738_bit0 C1739_bit0 C1740_bit0 -C1741_bit0 -C1742_bit0 C1743_bit0 -C1744_bit0 C1745_bit0 C1746_bit0 -C1747_bit0 -C1748_bit0 -C1749_bit0 -C1750_bit0 -C1753_bit0 -C1754_bit0 C1755_bit0 C1756_bit0 C1757_bit0 -C1758_bit0 -C1759_bit0 -C1760_bit0 -C1761_bit0 C1762_bit0 C1763_bit0 -C1764_bit0 C1765_bit0 -C1766_bit0 C1769_bit0 C1770_bit0 C1771_bit0 C1772_bit0 C1773_bit0 -C1774_bit0 C1775_bit0 C1776_bit0 C1777_bit0 -C1778_bit0 -C1779_bit0 C1780_bit0 -C1782_bit0 C1783_bit0 C1784_bit0 C1785_bit0 C1786_bit0 C1787_bit0 C1788_bit0 C1789_bit0 C1790_bit0 -C1791_bit0 -C1792_bit0 -C1793_bit0 C1796_bit0 -C1797_bit0 -C1798_bit0 -C1799_bit0 C1800_bit0 C1812_bit0 -C1813_bit0 C1814_bit0 -C1815_bit0 -C1816_bit0 -C1817_bit0 C1818_bit0 -C1821_bit0 -C1822_bit0 -C1823_bit0 -C1824_bit0 C1825_bit0 C1829_bit0 -C1833_bit0 C1837_bit0 -C1838_bit0 -C1839_bit0 -C1840_bit0 -C1841_bit0 -C1842_bit0 -C1843_bit0 C1846_bit0 -C1847_bit0 -C1848_bit0 -C1849_bit0 C1850_bit0 C1851_bit0 -C1854_bit0 -C1856_bit0 -C1860_bit0 -C1864_bit0 -C1865_bit0 -C1867_bit0 -C1870_bit0 -C1871_bit0 -C1872_bit0 -C1873_bit0 -C1875_bit0 C1876_bit0 -C1877_bit0 -C1878_bit0 -C1879_bit0 C1880_bit0 -C1882_bit0 -C1883_bit0 -C1884_bit0 -C1885_bit0 C1886_bit0 C1887_bit0 -C1888_bit0 C1889_bit0 -C1890_bit0 C1891_bit0 -C1892_bit0 -C1893_bit0 -C1896_bit0 -C1897_bit0 -C1898_bit0 -C1899_bit0 -C1900_bit0 -C1904_bit0 -C1908_bit0 C1912_bit0 -C1913_bit0 C1914_bit0 -C1915_bit0 -C1916_bit0 -C1917_bit0 C1918_bit0 C1921_bit0 -C1922_bit0 -C1923_bit0 -C1924_bit0 C1925_bit0 -C1926_bit0 -C1929_bit0 -C1933_bit0 C1937_bit0 -C1938_bit0 -C1939_bit0 -C1940_bit0 -C1941_bit0 -C1942_bit0 -C1943_bit0 C1946_bit0 -C1947_bit0 C1948_bit0 C1949_bit0 -C1950_bit0 -C1951_bit0 C1952_bit0 -C1954_bit0 C1955_bit0 -C1956_bit0 C1959_bit0 -C1960_bit0 -C1961_bit0 C1962_bit0 C1964_bit0 C1965_bit0 C1967_bit0 C1970_bit0 C1971_bit0 C1972_bit0 C1973_bit0 C1974_bit0 -C1975_bit0 -C1976_bit0 C1977_bit0 -C1978_bit0 C1979_bit0 -C1980_bit0 C1982_bit0 C1983_bit0 -C1984_bit0 -C1985_bit0 -C1986_bit0 -C1987_bit0 -C1988_bit0 -C1989_bit0 -C1990_bit0 -C1991_bit0 C1992_bit0 C1993_bit0 -C1994_bit0 -C1995_bit0 -C1996_bit0 -C1997_bit0 -C2000_bit0 -C2001_bit0 -C2002_bit0 -C2003_bit0 -C2004_bit0 -C2005_bit0 C2008_bit0 -C2011_bit0 -C2012_bit0 C2013_bit0 C2014_bit0 -C2016_bit0 -C2017_bit0 -C2018_bit0 -C2019_bit0 C2020_bit0 -C2021_bit0 -C2022_bit0 -C2023_bit0 -C2024_bit0 -C2025_bit0 -C2026_bit0 -C2029_bit0 -C2030_bit0 -C2031_bit0 -C2032_bit0 -C2033_bit0 -C2034_bit0 -C2035_bit0 -C2036_bit0 -C2037_bit0 C2038_bit0 -C2039_bit0 -C2040_bit0 C2041_bit0 C2042_bit0 -C2043_bit0 C2045_bit0 -C2048_bit0 -C2049_bit0 -C2050_bit0 -C2051_bit0 -C2052_bit0 -C2053_bit0 -C2054_bit0 -C2055_bit0 -C2056_bit0 -C2057_bit0 -C2058_bit0 -C2059_bit0 C2060_bit0 C2061_bit0 -C2062_bit0 -C2063_bit0 -C2064_bit0 -C2065_bit0 C2066_bit0 -C2067_bit0 -C2070_bit0 -C2071_bit0 -C2072_bit0 -C2073_bit0 -C2074_bit0 -C2075_bit0 -C2076_bit0 -C2077_bit0 -C2078_bit0 -C2079_bit0 -C2080_bit0 C2081_bit0 C2082_bit0 C2083_bit0 -C2084_bit0 -C2085_bit0 -C2086_bit0 C2087_bit0 -C2088_bit0 C2091_bit0 -C2092_bit0 C2093_bit0 C2094_bit0 C2095_bit0 -C2096_bit0 C2097_bit0 -C2098_bit0 -C2099_bit0 C2100_bit0 -C2101_bit0 -C2102_bit0 -C2103_bit0 C2106_bit0 C2107_bit0 C2108_bit0 C2109_bit0 C2110_bit0 -C2111_bit0 -C2112_bit0 -C2113_bit0 -C2114_bit0 C2115_bit0 C2116_bit0 -C2117_bit0 -C2118_bit0 C2119_bit0 -C2120_bit0 C2121_bit0 -C2122_bit0 -C2123_bit0 -C2124_bit0 -C2126_bit0 -C2127_bit0 C2128_bit0 -C2129_bit0 C2130_bit0 -C2131_bit0 -C2132_bit0 C2133_bit0 -C2134_bit0 C2135_bit0 C2136_bit0 -C2137_bit0 -C2138_bit0 -C2139_bit0 C2140_bit0 -C2141_bit0 C2144_bit0 -C2145_bit0 C2146_bit0 -C2147_bit0 -C2148_bit0 C2149_bit0 C2152_bit0 C2155_bit0 -C2156_bit0 C2157_bit0 C2158_bit0 -C2160_bit0 -C2161_bit0 -C2162_bit0 C2163_bit0 C2164_bit0 -C2165_bit0 -C2166_bit0 -C2167_bit0 -C2168_bit0 -C2169_bit0 C2170_bit0 C2173_bit0 -C2174_bit0 C2175_bit0 -C2176_bit0 -C2177_bit0 -C2178_bit0 -C2179_bit0 C2180_bit0 C2181_bit0 -C2182_bit0 -C2183_bit0 -C2184_bit0 -C2185_bit0 C2186_bit0 -C2187_bit0 C2189_bit0 C2192_bit0 -C2193_bit0 C2194_bit0 C2195_bit0 C2196_bit0 -C2197_bit0 -C2198_bit0 -C2199_bit0 C2200_bit0 C2201_bit0 -C2202_bit0 -C2203_bit0 -C2204_bit0 C2205_bit0 -C2206_bit0 C2207_bit0 -C2208_bit0 -C2209_bit0 -C2210_bit0 C2211_bit0 C2214_bit0 -C2215_bit0 C2216_bit0 C2217_bit0 C2218_bit0 -C2219_bit0 -C2220_bit0 -C2221_bit0 C2222_bit0 -C2223_bit0 -C2224_bit0 C2225_bit0 -C2226_bit0 C2227_bit0 C2228_bit0 C2229_bit0 C2230_bit0 -C2231_bit0 -C2232_bit0 C2235_bit0 -C2236_bit0 C2237_bit0 C2238_bit0 C2239_bit0 -C2240_bit0 C2241_bit0 -C2242_bit0 -C2243_bit0 C2244_bit0 C2245_bit0 C2246_bit0 C2247_bit0 C2250_bit0 C2251_bit0 C2252_bit0 C2253_bit0 C2254_bit0 -C2255_bit0 -C2256_bit0 -C2257_bit0 -C2258_bit0 C2259_bit0 C2260_bit0 -C2261_bit0 -C2262_bit0 C2263_bit0 -C2264_bit0 C2265_bit0 -C2266_bit0 -C2267_bit0 -C2268_bit0 C2270_bit0 -C2271_bit0 C2272_bit0 C2273_bit0 C2274_bit0 C2275_bit0 -C2276_bit0 -C2277_bit0 -C2278_bit0 -C2279_bit0 -C2280_bit0 -C2281_bit0 C2282_bit0 -C2283_bit0 C2284_bit0 -C2285_bit0 -C2286_bit0 -C2287_bit0 C2288_bit0 -C2289_bit0 C2290_bit0 -C2291_bit0 C2292_bit0 -C2293_bit0 -C2294_bit0 -C2295_bit0 -C2296_bit0 -C2297_bit0 -C2298_bit0 -C2299_bit0 C2300_bit0 C2301_bit0 C2302_bit0 -C2303_bit0 C2304_bit0 C2305_bit0 C2306_bit0 C2307_bit0 -C2308_bit0 -C2309_bit0 -C2310_bit0 -C2311_bit0 -C2312_bit0 -C2313_bit0 -C2314_bit0 C2315_bit0 -C2316_bit0 C2317_bit0 C2318_bit0 C2319_bit0 C2320_bit0 -C2321_bit0 -C2322_bit0 -C2323_bit0 -C2324_bit0 C2325_bit0 C2326_bit0 -C2327_bit0 -C2328_bit0 -C2329_bit0 C2330_bit0 -C2331_bit0 -C2332_bit0 -C2333_bit0 C2334_bit0 -C2335_bit0 -C2336_bit0 -C2337_bit0 -C2338_bit0 C2339_bit0 -C2340_bit0 -C2341_bit0 -C2342_bit0 -C2343_bit0 -C2344_bit0 -C2345_bit0 -C2346_bit0 -C2348_bit0 C2349_bit0 -C2351_bit0 -C2352_bit0 -C2353_bit0 -C2354_bit0 -C2355_bit0 -C2356_bit0 -C2357_bit0 -C2358_bit0 -C2359_bit0 -C2360_bit0 -C2361_bit0 -C2362_bit0 C2363_bit0 -C2364_bit0 -C2365_bit0 C2366_bit0 -C2367_bit0 C2369_bit0 -C2370_bit0 -C2371_bit0 -C2372_bit0 C2373_bit0 -C2374_bit0 -C2375_bit0 -C2376_bit0 -C2377_bit0 -C2378_bit0 -C2379_bit0 -C2380_bit0 C2381_bit0 -C2382_bit0 -C2384_bit0 C2386_bit0 -C2387_bit0 -C2391_bit0 -C2392_bit0 -C2393_bit0 -C2394_bit0 -C2395_bit0 C2396_bit0 -C2397_bit0 -C2398_bit0 -C2399_bit0 C2401_bit0 -C2402_bit0 C2404_bit0 -C2405_bit0 C2406_bit0 C2407_bit0 C2408_bit0 -C2409_bit0 -C2410_bit0 -C2411_bit0 -C2412_bit0 C2413_bit0 C2414_bit0 -C2415_bit0 -C2416_bit0 -C2417_bit0 -C2418_bit0 C2419_bit0 -C2420_bit0 C2422_bit0 -C2423_bit0 -C2424_bit0 -C2425_bit0 -C2426_bit0 -C2427_bit0 -C2428_bit0 -C2429_bit0 -C2430_bit0 -C2431_bit0 -C2432_bit0 C2433_bit0 C2434_bit0 -C2435_bit0 C2436_bit0 -C2437_bit0 -C2438_bit0 C2440_bit0 -C2441_bit0 C2442_bit0 C2443_bit0 -C2444_bit0 C2445_bit0 -C2446_bit0 -C2447_bit0 -C2448_bit0 -C2449_bit0 C2450_bit0 -C2451_bit0 -C2452_bit0 C2453_bit0 C2455_bit0 C2457_bit0 -C2458_bit0 C2459_bit0 C2460_bit0 C2461_bit0 -C2462_bit0 -C2463_bit0 -C2464_bit0 -C2465_bit0 -C2466_bit0 -C2467_bit0 C2468_bit0 -C2469_bit0 C2470_bit0 C2471_bit0 -C2472_bit0 C2473_bit0 C2475_bit0 -C2476_bit0 -C2477_bit0 -C2478_bit0 -C2479_bit0 -C2480_bit0 C2481_bit0 -C2482_bit0 -C2483_bit0 -C2484_bit0 -C2485_bit0 C2486_bit0 -C2487_bit0 C2488_bit0 -C2489_bit0 -C2490_bit0 C2491_bit0 C2493_bit0 C2494_bit0 C2495_bit0 C2496_bit0 C2497_bit0 -C2498_bit0 -C2499_bit0 C2500_bit0 -C2501_bit0 -C2502_bit0 C2503_bit0 -C2504_bit0 -C2505_bit0 -C2506_bit0 C2507_bit0 C2508_bit0 -C2509_bit0 -C2511_bit0 -C2512_bit0 -C2513_bit0 -C2514_bit0 -C2515_bit0 -C2516_bit0 -C2517_bit0 -C2518_bit0 -C2519_bit0 -C2520_bit0 C2521_bit0 C2522_bit0 C2524_bit0 -C2525_bit0 -C2526_bit0 C2527_bit0 -C2528_bit0 C2529_bit0 -C2530_bit0 -C2531_bit0 C2532_bit0 -C2533_bit0 -C2534_bit0 -C2535_bit0 -C2536_bit0 C2537_bit0 C2538_bit0 C2539_bit0 -C2540_bit0 C2542_bit0 C2543_bit0 C2544_bit0 C2545_bit0 C2546_bit0 -C2547_bit0 C2548_bit0 -C2549_bit0 -C2550_bit0 -C2551_bit0 -C2552_bit0 -C2553_bit0 -C2554_bit0 -C2555_bit0 -C2556_bit0 -C2557_bit0 -C2558_bit0 -C2560_bit0 -C2561_bit0 C2562_bit0 -C2563_bit0 -C2564_bit0 -C2565_bit0 -C2566_bit0 -C2567_bit0 -C2568_bit0 C2569_bit0 C2570_bit0 -C2571_bit0 -C2572_bit0 C2573_bit0 C2574_bit0 -C2575_bit0 -C2576_bit0 -C2578_bit0 -C2579_bit0 -C2580_bit0 C2581_bit0 -C2582_bit0 -C2583_bit0 C2584_bit0 -C2585_bit0 -C2586_bit0 C2587_bit0 C2588_bit0 C2589_bit0 -C2591_bit0 C2592_bit0 -C2593_bit0 C2594_bit0 -C2595_bit0 -C2596_bit0 -C2597_bit0 -C2598_bit0 -C2599_bit0 -C2600_bit0 -C2601_bit0 -C2602_bit0 -C2603_bit0 C2604_bit0 -C2605_bit0 -C2606_bit0 -C2607_bit0 C2609_bit0 -C2610_bit0 C2611_bit0 -C2612_bit0 -C2613_bit0 C2614_bit0 -C2615_bit0 -C2616_bit0 -C2617_bit0 -C2618_bit0 C2619_bit0 -C2620_bit0 C2623_bit0 -C2624_bit0 C2625_bit0 C2626_bit0 C2627_bit0 -C2628_bit0 -C2631_bit0 C2634_bit0 C2635_bit0 C2636_bit0 -C2637_bit0 C2639_bit0 -C2640_bit0 C2641_bit0 -C2642_bit0 -C2643_bit0 -C2644_bit0 -C2647_bit0 -C2648_bit0 -C2649_bit0 C2650_bit0 -C2651_bit0 C2652_bit0 -C2653_bit0 -C2654_bit0 -C2655_bit0 C2656_bit0 C2658_bit0 -C2659_bit0 -C2660_bit0 C2663_bit0 C2664_bit0 C2665_bit0 C2666_bit0 C2667_bit0 C2668_bit0 -C2669_bit0 -C2670_bit0 -C2671_bit0 C2672_bit0 C2673_bit0 C2675_bit0 C2678_bit0 C2679_bit0 C2680_bit0 -C2683_bit0 -C2684_bit0 -C2685_bit0 -C2686_bit0 C2687_bit0 C2688_bit0 C2690_bit0 -C2692_bit0 C2694_bit0 -C2695_bit0 -C2696_bit0 C2699_bit0 C2700_bit0 C2701_bit0 -C2702_bit0 C2703_bit0 -C2704_bit0 -C2705_bit0 C2708_bit0 -C2709_bit0 C2710_bit0 C2711_bit0 -C2712_bit0 C2713_bit0 -C2714_bit0 C2716_bit0 C2719_bit0 -C2720_bit0 -C2721_bit0 C2722_bit0 -C2723_bit0 -C2724_bit0 -C2725_bit0 -C2726_bit0 -C2727_bit0 -C2728_bit0 C2729_bit0 -C2732_bit0 C2733_bit0 C2734_bit0 -C2735_bit0 -C2736_bit0 -C2737_bit0 C2738_bit0 -C2739_bit0 -C2740_bit0 C2741_bit0 -C2742_bit0 -C2743_bit0 C2744_bit0 -C2745_bit0 -C2748_bit0 C2749_bit0 -C2750_bit0 -C2751_bit0 -C2752_bit0 -C2753_bit0 C2754_bit0 -C2755_bit0 -C2756_bit0 -C2757_bit0 -C2758_bit0 C2760_bit0 C2763_bit0 -C2764_bit0 -C2765_bit0 -C2766_bit0 -C2768_bit0 -C2769_bit0 -C2770_bit0 C2771_bit0 C2772_bit0 C2773_bit0 C2775_bit0 -C2776_bit0 -C2777_bit0 -C2779_bit0 -C2780_bit0 C2781_bit0 C2782_bit0 C2783_bit0 C2784_bit0 C2785_bit0 -C2786_bit0 -C2787_bit0 -C2788_bit0 C2789_bit0 -C2790_bit0 C2793_bit0 -C2794_bit0 C2795_bit0 C2796_bit0 C2797_bit0 -C2798_bit0 C2799_bit0 -C2801_bit0 C2804_bit0 C2805_bit0 C2806_bit0 C2807_bit0 C2808_bit0 -C2809_bit0 C2810_bit0 -C2811_bit0 C2812_bit0 -C2813_bit0 -C2814_bit0 -C2817_bit0 -C2818_bit0 C2819_bit0 -C2820_bit0 -C2821_bit0 -C2822_bit0 -C2823_bit0 -C2824_bit0 -C2825_bit0 -C2826_bit0 C2827_bit0 -C2828_bit0 -C2829_bit0 -C2830_bit0 -C2833_bit0 -C2834_bit0 -C2835_bit0 -C2836_bit0 -C2837_bit0 -C2838_bit0 -C2839_bit0 -C2840_bit0 C2841_bit0 C2842_bit0 C2843_bit0 C2845_bit0 -C2848_bit0 C2849_bit0 C2850_bit0 C2851_bit0 C2852_bit0 -C2853_bit0 -C2854_bit0 -C2855_bit0 -C2856_bit0 -C2857_bit0 C2858_bit0 -C2859_bit0 C2860_bit0 -C2861_bit0 -C2862_bit0 -C2864_bit0 C2865_bit0 C2866_bit0 -C2867_bit0 -C2868_bit0 -C2869_bit0 C2870_bit0 C2871_bit0 C2872_bit0 -C2873_bit0 -C2874_bit0 -C2875_bit0 C2878_bit0 -C2879_bit0 C2880_bit0 C2881_bit0 C2882_bit0 C2883_bit0 -C2884_bit0 C2885_bit0 C2886_bit0 C2889_bit0 C2890_bit0 C2891_bit0 -C2892_bit0 C2893_bit0 C2894_bit0 -C2895_bit0 -C2896_bit0 -C2897_bit0 C2898_bit0 -C2899_bit0 C2902_bit0 -C2903_bit0 C2904_bit0 C2905_bit0 C2906_bit0 C2907_bit0 -C2908_bit0 -C2909_bit0 -C2910_bit0 C2911_bit0 -C2912_bit0 -C2913_bit0 -C2914_bit0 -C2915_bit0 C2918_bit0 -C2919_bit0 -C2920_bit0 -C2921_bit0 -C2922_bit0 -C2923_bit0 -C2924_bit0 -C2925_bit0 -C2926_bit0 C2927_bit0 -C2928_bit0 -C2929_bit0 C2930_bit0 C2933_bit0 -C2934_bit0 -C2935_bit0 C2936_bit0 -C2937_bit0 -C2938_bit0 C2939_bit0 -C2940_bit0 -C2941_bit0 C2942_bit0 C2943_bit0 -C2944_bit0 -C2945_bit0 C2946_bit0 -C2947_bit0 C2949_bit0 C2950_bit0 C2951_bit0 C2952_bit0 C2953_bit0 -C2954_bit0 -C2955_bit0 -C2956_bit0 -C2957_bit0 C2958_bit0 C2959_bit0 C2960_bit0 -C2961_bit0 -C2962_bit0 -C2963_bit0 -C2966_bit0 C2967_bit0 C2968_bit0 C2969_bit0 C2970_bit0 -C2971_bit0 -C2972_bit0 C2973_bit0 -C2974_bit0 C2975_bit0 -C2976_bit0 C2977_bit0 C2980_bit0 -C2981_bit0 C2982_bit0 C2983_bit0 -C2984_bit0 C2985_bit0 -C2986_bit0 -C2987_bit0 -C2988_bit0 -C2989_bit0 -C2990_bit0 -C2991_bit0 -C2992_bit0 -C2993_bit0 -C2994_bit0 -C2995_bit0 -C2996_bit0 -C2997_bit0 -C2998_bit0 -C2999_bit0 C3000_bit0 C3001_bit0 C3003_bit0 -C3004_bit0 C3005_bit0 -C3006_bit0 -C3007_bit0 -C3008_bit0 -C3009_bit0 -C3010_bit0 C3011_bit0 -C3012_bit0 -C3013_bit0 -C3014_bit0 -C3015_bit0 -C3016_bit0 -C3017_bit0 -C3018_bit0 C3019_bit0 -C3020_bit0 -C3021_bit0 C3022_bit0 C3023_bit0 C3024_bit0 -C3025_bit0 C3027_bit0 -C3028_bit0 -C3029_bit0 C3030_bit0 -C3031_bit0 -C3032_bit0 -C3033_bit0 -C3034_bit0 C3035_bit0 -C3038_bit0 C3040_bit0 C3041_bit0 -C3042_bit0 -C3043_bit0 -C3045_bit0 -C3046_bit0 C3047_bit0 -C3048_bit0 -C3049_bit0 C3050_bit0 -C3051_bit0 C3053_bit0 -C3054_bit0 -C3055_bit0 C3056_bit0 C3057_bit0 -C3058_bit0 C3059_bit0 -C3060_bit0 -C3061_bit0 -C3062_bit0 C3064_bit0 C3066_bit0 -C3067_bit0 -C3068_bit0 -C3071_bit0 C3072_bit0 -C3073_bit0 -C3074_bit0 C3075_bit0 -C3076_bit0 C3077_bit0 -C3078_bit0 C3080_bit0 C3081_bit0 C3082_bit0 C3083_bit0 C3084_bit0 -C3085_bit0 -C3086_bit0 -C3087_bit0 C3088_bit0 C3089_bit0 -C3090_bit0 -C3091_bit0 -C3092_bit0 C3094_bit0 -C3095_bit0 -C3096_bit0 C3097_bit0 C3098_bit0 -C3099_bit0 -C3100_bit0 -C3101_bit0 -C3102_bit0 C3105_bit0 C3107_bit0 -C3108_bit0 -C3109_bit0 C3110_bit0 -C3112_bit0 -C3113_bit0 C3114_bit0 -C3115_bit0 C3116_bit0 -C3117_bit0 -C3118_bit0 C3120_bit0 C3121_bit0 -C3122_bit0 C3123_bit0 C3124_bit0 -C3125_bit0 C3126_bit0 -C3127_bit0 -C3128_bit0 C3129_bit0 C3131_bit0 C3133_bit0 -C3134_bit0 -C3135_bit0 -C3138_bit0 -C3139_bit0 -C3140_bit0 -C3141_bit0 -C3142_bit0 C3143_bit0 C3144_bit0 -C3145_bit0 -C3147_bit0 -C3148_bit0 -C3149_bit0 -C3150_bit0 -C3151_bit0 C3152_bit0 -C3153_bit0 -C3154_bit0 -C3155_bit0 C3156_bit0 C3157_bit0 C3158_bit0 -C3159_bit0 C3161_bit0 -C3162_bit0 -C3163_bit0 C3164_bit0 -C3165_bit0 -C3166_bit0 -C3167_bit0 C3168_bit0 -C3169_bit0 C3170_bit0 C3172_bit0 C3174_bit0 -C3175_bit0 -C3176_bit0 -C3177_bit0 C3178_bit0 -C3179_bit0 -C3180_bit0 -C3181_bit0 -C3182_bit0 C3183_bit0 -C3184_bit0 -C3185_bit0 C3187_bit0 C3188_bit0 -C3189_bit0 C3190_bit0 -C3191_bit0 -C3192_bit0 -C3193_bit0 -C3194_bit0 -C3195_bit0 -C3196_bit0 C3198_bit0 C3200_bit0 -C3201_bit0 C3202_bit0 -C3203_bit0 C3204_bit0 -C3205_bit0 -C3206_bit0 C3207_bit0 -C3208_bit0 C3209_bit0 C3210_bit0 C3211_bit0 -C3212_bit0 C3214_bit0 C3215_bit0 C3216_bit0 C3217_bit0 C3218_bit0 C3219_bit0 -C3220_bit0 -C3221_bit0 -C3222_bit0 C3223_bit0 C3224_bit0 -C3225_bit0 -C3226_bit0 C3228_bit0 -C3229_bit0 C3230_bit0 C3231_bit0 C3232_bit0 -C3233_bit0 -C3234_bit0 C3235_bit0 -C3236_bit0 -C3237_bit0 C3239_bit0 -C3241_bit0 -C3242_bit0 C3243_bit0 C3244_bit0 C3245_bit0 -C3246_bit0 -C3247_bit0 C3248_bit0 -C3249_bit0 C3250_bit0 -C3251_bit0 -C3252_bit0 C3254_bit0 C3255_bit0 C3256_bit0 C3257_bit0 C3258_bit0 -C3259_bit0 -C3260_bit0 -C3261_bit0 C3262_bit0 -C3263_bit0 C3265_bit0 C3267_bit0 -C3268_bit0 C3269_bit0 C3270_bit0 C3271_bit0 -C3272_bit0 -C3273_bit0 -C3274_bit0 -C3275_bit0 -C3276_bit0 C3277_bit0 C3278_bit0 -C3279_bit0 -C3281_bit0 -C3282_bit0 -C3283_bit0 -C3284_bit0 -C3285_bit0 -C3286_bit0 -C3287_bit0 C3288_bit0 -C3289_bit0 -C3290_bit0 C3291_bit0 C3292_bit0 -C3293_bit0 C3295_bit0 -C3296_bit0 -C3297_bit0 C3298_bit0 C3299_bit0 -C3300_bit0 -C3301_bit0 -C3302_bit0 C3303_bit0 C3306_bit0 C3308_bit0 C3309_bit0 -C3310_bit0 -C3311_bit0 -C3313_bit0 -C3314_bit0 -C3315_bit0 C3316_bit0 C3317_bit0 -C3318_bit0 -C3319_bit0 C3321_bit0 -C3322_bit0 -C3323_bit0 -C3324_bit0 C3325_bit0 -C3326_bit0 C3327_bit0 -C3328_bit0 -C3329_bit0 -C3330_bit0 C3332_bit0 C3334_bit0 -C3335_bit0 -C3336_bit0 -C3337_bit0 -C3339_bit0 C3340_bit0 -C3341_bit0 -C3342_bit0 C3343_bit0 -C3345_bit0 C3346_bit0 C3348_bit0 C3349_bit0 C3350_bit0 C3351_bit0 C3352_bit0 C3353_bit0 -C3354_bit0 -C3355_bit0 -C3356_bit0 C3357_bit0 C3358_bit0 -C3359_bit0 -C3360_bit0 -C3362_bit0 C3363_bit0 -C3364_bit0 -C3365_bit0 C3366_bit0 -C3367_bit0 -C3368_bit0 -C3369_bit0 -C3370_bit0 C3373_bit0 C3375_bit0 -C3376_bit0 -C3377_bit0 C3378_bit0 C3380_bit0 -C3381_bit0 -C3382_bit0 -C3383_bit0 -C3384_bit0 -C3385_bit0 C3386_bit0 C3388_bit0 C3389_bit0 C3390_bit0 C3391_bit0 -C3392_bit0 C3393_bit0 -C3394_bit0 -C3395_bit0 -C3396_bit0 -C3397_bit0 C3399_bit0 C3401_bit0 -C3402_bit0 C3403_bit0 C3404_bit0 -C3406_bit0 -C3407_bit0 -C3408_bit0 -C3409_bit0 -C3410_bit0 -C3411_bit0 C3412_bit0 -C3413_bit0 -C3415_bit0 -C3416_bit0 -C3417_bit0 -C3418_bit0 -C3419_bit0 -C3420_bit0 -C3421_bit0 -C3422_bit0 C3423_bit0 C3424_bit0 -C3425_bit0 -C3426_bit0 -C3427_bit0 C3428_bit0 -C3429_bit0 -C3430_bit0 C3432_bit0 C3433_bit0 C3434_bit0 C3435_bit0 C3436_bit0 -C3437_bit0 -C3438_bit0 -C3439_bit0 -C3440_bit0 -C3441_bit0 -C3442_bit0 -C3443_bit0 -C3444_bit0 C3445_bit0 -C3446_bit0 -C3448_bit0 -C3449_bit0 C3450_bit0 -C3451_bit0 -C3452_bit0 -C3453_bit0 -C3454_bit0 C3455_bit0 -C3456_bit0 C3457_bit0 -C3458_bit0 -C3459_bit0 -C3460_bit0 C3461_bit0 C3462_bit0 -C3463_bit0 -C3464_bit0 -C3466_bit0 -C3467_bit0 -C3468_bit0 -C3469_bit0 -C3470_bit0 -C3471_bit0 -C3472_bit0 C3473_bit0 -C3474_bit0 -C3475_bit0 C3476_bit0 -C3477_bit0 -C3478_bit0 -C3479_bit0 -C3480_bit0 -C3481_bit0 C3483_bit0 -C3484_bit0 -C3485_bit0 -C3486_bit0 C3487_bit0 -C3488_bit0 -C3489_bit0 -C3490_bit0 -C3491_bit0 -C3492_bit0 -C3493_bit0 -C3494_bit0 -C3495_bit0 C3496_bit0 -C3497_bit0 -C3499_bit0 -C3500_bit0 -C3501_bit0 -C3502_bit0 -C3503_bit0 C3504_bit0 -C3505_bit0 -C3506_bit0 -C3507_bit0 -C3508_bit0 -C3509_bit0 C3510_bit0 -C3511_bit0 -C3512_bit0 C3513_bit0 C3514_bit0 -C3515_bit0 C3517_bit0 -C3518_bit0 -C3519_bit0 C3520_bit0 C3521_bit0 C3522_bit0 -C3523_bit0 -C3524_bit0 C3526_bit0 C3527_bit0 -C3528_bit0 C3529_bit0 C3530_bit0 -C3531_bit0 -C3532_bit0 -C3534_bit0 C3535_bit0 C3536_bit0 C3537_bit0 C3538_bit0 -C3539_bit0 -C3540_bit0 C3541_bit0 -C3542_bit0 -C3544_bit0 -C3545_bit0 -C3546_bit0 -C3547_bit0 -C3548_bit0 C3549_bit0 C3550_bit0 C3551_bit0 C3552_bit0 -C3553_bit0 C3554_bit0 C3555_bit0 C3556_bit0 C3557_bit0 C3558_bit0 C3559_bit0 C3560_bit0 C3561_bit0 -C3562_bit0 C3563_bit0 C3564_bit0 -C3565_bit0 -C3566_bit0 -C3567_bit0 C1007_bit0 -C1008_bit0 -C1012_bit0 -C1013_bit0 C1015_bit0 -C1016_bit0 C1018_bit0 -C1025_bit0 -C1026_bit0 -C1028_bit0 -C1040_bit0 C1041_bit0 -C1043_bit0 -C1052_bit0 -C1053_bit0 -C1055_bit0 -C1063_bit0 -C1064_bit0 C1069_bit0 -C1071_bit0 -C1072_bit0 -C1081_bit0 C1082_bit0 -C1084_bit0 C1096_bit0 -C1097_bit0 -C1099_bit0 -C1108_bit0 -C1109_bit0 -C1111_bit0 -C1118_bit0 -C1125_bit0 -C1130_bit0 -C1138_bit0 C1146_bit0 -C1147_bit0 -C1151_bit0 -C1152_bit0 C1154_bit0 -C1155_bit0 C1157_bit0 -C1164_bit0 C1165_bit0 -C1167_bit0 C1179_bit0 -C1180_bit0 C1182_bit0 -C1191_bit0 -C1192_bit0 C1194_bit0 -C1202_bit0 -C1203_bit0 C1208_bit0 C1210_bit0 -C1211_bit0 -C1220_bit0 -C1221_bit0 -C1223_bit0 C1235_bit0 -C1236_bit0 -C1238_bit0 -C1247_bit0 -C1248_bit0 C1250_bit0 -C1257_bit0 -C1264_bit0 C1269_bit0 -C1277_bit0 -C1282_bit0 -C1287_bit0 -C1288_bit0 -C1301_bit0 -C1302_bit0 -C1311_bit0 -C1312_bit0 -C1324_bit0 C1325_bit0 C1334_bit0 -C1336_bit0 C1337_bit0 -C1342_bit0 C1346_bit0 -C1350_bit0 C1355_bit0 -C1364_bit0 -C1365_bit0 C1378_bit0 -C1379_bit0 -C1388_bit0 -C1389_bit0 -C1401_bit0 C1402_bit0 -C1413_bit0 C1414_bit0 -C1427_bit0 -C1455_bit0 -C1462_bit0 C1477_bit0 -C1478_bit0 -C1487_bit0 C1488_bit0 -C1504_bit0 C1505_bit0 C1518_bit0 -C1520_bit0 C1521_bit0 C1534_bit0 -C1547_bit0 C1548_bit0 C1557_bit0 -C1558_bit0 -C1574_bit0 -C1575_bit0 -C1590_bit0 -C1591_bit0 C1604_bit0 C1632_bit0 C1649_bit0 -C1654_bit0 -C1655_bit0 -C1664_bit0 C1665_bit0 -C1681_bit0 C1682_bit0 C1695_bit0 C1697_bit0 -C1698_bit0 -C1711_bit0 -C1724_bit0 -C1725_bit0 C1734_bit0 -C1735_bit0 -C1751_bit0 C1752_bit0 -C1767_bit0 -C1768_bit0 C1781_bit0 -C1794_bit0 C1795_bit0 -C1801_bit0 C1802_bit0 C1803_bit0 -C1804_bit0 -C1805_bit0 -C1806_bit0 C1807_bit0 -C1808_bit0 C1809_bit0 -C1810_bit0 C1811_bit0 -C1819_bit0 C1820_bit0 -C1826_bit0 -C1827_bit0 -C1828_bit0 C1830_bit0 -C1831_bit0 C1832_bit0 C1834_bit0 -C1835_bit0 C1836_bit0 -C1844_bit0 -C1845_bit0 C1852_bit0 C1853_bit0 C1855_bit0 -C1857_bit0 -C1858_bit0 C1859_bit0 C1861_bit0 C1862_bit0 -C1863_bit0 -C1866_bit0 -C1868_bit0 C1869_bit0 -C1874_bit0 -C1881_bit0 -C1894_bit0 -C1895_bit0 -C1901_bit0 -C1902_bit0 C1903_bit0 -C1905_bit0 C1906_bit0 C1907_bit0 -C1909_bit0 C1910_bit0 -C1911_bit0 -C1919_bit0 -C1920_bit0 -C1927_bit0 C1928_bit0 -C1930_bit0 C1931_bit0 -C1932_bit0 -C1934_bit0 -C1935_bit0 C1936_bit0 -C1944_bit0 -C1945_bit0 -C1953_bit0 C1957_bit0 -C1958_bit0 C1963_bit0 -C1966_bit0 -C1968_bit0 -C1969_bit0 C1981_bit0 -C1998_bit0 C1999_bit0 C2006_bit0 -C2007_bit0 -C2009_bit0 -C2010_bit0 C2015_bit0 -C2027_bit0 C2028_bit0 C2044_bit0 -C2046_bit0 C2047_bit0 -C2068_bit0 C2069_bit0 -C2089_bit0 -C2090_bit0 -C2104_bit0 C2105_bit0 -C2125_bit0 -C2142_bit0 -C2143_bit0 -C2150_bit0 -C2151_bit0 -C2153_bit0 -C2154_bit0 C2159_bit0 -C2171_bit0 -C2172_bit0 C2188_bit0 C2190_bit0 -C2191_bit0 -C2212_bit0 -C2213_bit0 C2233_bit0 -C2234_bit0 C2248_bit0 -C2249_bit0 C2269_bit0 C2347_bit0 C2350_bit0 -C2368_bit0 C2383_bit0 -C2385_bit0 C2388_bit0 C2389_bit0 C2390_bit0 C2400_bit0 -C2403_bit0 -C2421_bit0 -C2439_bit0 C2454_bit0 -C2456_bit0 -C2474_bit0 C2492_bit0 C2510_bit0 C2523_bit0 C2541_bit0 -C2559_bit0 C2577_bit0 C2590_bit0 -C2608_bit0 C2621_bit0 -C2622_bit0 C2629_bit0 -C2630_bit0 C2632_bit0 -C2633_bit0 C2638_bit0 C2645_bit0 -C2646_bit0 C2657_bit0 -C2661_bit0 C2662_bit0 -C2674_bit0 C2676_bit0 -C2677_bit0 C2681_bit0 -C2682_bit0 C2689_bit0 -C2691_bit0 C2693_bit0 C2697_bit0 C2698_bit0 C2706_bit0 -C2707_bit0 -C2715_bit0 -C2717_bit0 -C2718_bit0 C2730_bit0 -C2731_bit0 -C2746_bit0 -C2747_bit0 C2759_bit0 -C2761_bit0 -C2762_bit0#### END SOLVER DATA #### #### BEGIN WATCHER DATA #### Enforcing CPU limit (will send SIGTERM then SIGKILL): 1200 seconds Enforcing CPUTime (will send SIGXCPU) limit: 1230 seconds Enforcing VSIZE limit: 943718400 bytes Raw data (loadavg): 0.85 0.94 0.90 2/54 16077 Raw data (stat): 16077 (runsolver) R 16076 32461 32460 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 491720905 1052672 99 4294967295 134512640 135381576 3221224432 3221219676 135158418 0 2147483391 7 90112 0 0 0 17 1 0 0 Raw data (statm): 257 99 215 215 0 42 0 vsize: 1028 [startup+10.0002 s] Raw data (loadavg): 0.87 0.94 0.90 2/54 16077 Raw data (stat): 16077 (minisat+) R 16076 32461 32460 0 -1 0 14631 0 0 0 960 38 0 0 25 0 1 0 491720905 58085376 12618 4294967295 134512640 134672761 3221224544 3221126096 134564831 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 14181 12618 603 41 0 14140 0 vsize: 56724 [startup+20.0013 s] Raw data (loadavg): 0.89 0.94 0.90 2/54 16077 Raw data (stat): 16077 (minisat+) R 16076 32461 32460 0 -1 0 26045 0 0 0 1937 61 0 0 25 0 1 0 491720905 121151488 24032 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 29578 24032 603 41 0 29537 0 vsize: 118312 [startup+30.0017 s] Raw data (loadavg): 0.91 0.94 0.90 2/54 16077 Raw data (stat): 16077 (minisat+) R 16076 32461 32460 0 -1 0 26212 0 0 0 2936 62 0 0 25 0 1 0 491720905 121798656 24199 4294967295 134512640 134672761 3221224544 3221223716 134556627 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 29736 24199 603 41 0 29695 0 vsize: 118944 [startup+40.0025 s] Raw data (loadavg): 0.92 0.94 0.90 2/54 16077 Raw data (stat): 16077 (minisat+) R 16076 32461 32460 0 -1 0 26221 0 0 0 3936 63 0 0 25 0 1 0 491720905 121798656 24208 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 29736 24208 603 41 0 29695 0 vsize: 118944 [startup+50.0037 s] Raw data (loadavg): 0.93 0.94 0.90 2/54 16077 Raw data (stat): 16077 (minisat+) R 16076 32461 32460 0 -1 0 26231 0 0 0 4936 63 0 0 25 0 1 0 491720905 121798656 24218 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 29736 24218 603 41 0 29695 0 vsize: 118944 [startup+60.003 s] Raw data (loadavg): 0.94 0.95 0.91 2/54 16077 Raw data (stat): 16077 (minisat+) R 16076 32461 32460 0 -1 0 26261 0 0 0 5936 63 0 0 25 0 1 0 491720905 121933824 24248 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 29769 24248 603 41 0 29728 0 vsize: 119076 [startup+70.004 s] Raw data (loadavg): 1.03 0.96 0.91 3/57 16125 Raw data (stat): 16077 (minisat+) R 16076 32461 32460 0 -1 0 26313 0 0 0 6935 64 0 0 25 0 1 0 491720905 122204160 24300 4294967295 134512640 134672761 3221224544 3221223760 134561993 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 29835 24300 603 41 0 29794 0 vsize: 119340 [startup+80.0045 s] Raw data (loadavg): 1.03 0.96 0.91 2/54 16130 Raw data (stat): 16077 (minisat+) R 16076 32461 32460 0 -1 0 26348 0 0 0 7935 64 0 0 25 0 1 0 491720905 122204160 24335 4294967295 134512640 134672761 3221224544 3221223716 134556669 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 29835 24335 603 41 0 29794 0 vsize: 119340 [startup+90.0043 s] Raw data (loadavg): 1.02 0.97 0.91 2/54 16130 Raw data (stat): 16077 (minisat+) R 16076 32461 32460 0 -1 0 26518 0 0 0 8935 64 0 0 25 0 1 0 491720905 122875904 24505 4294967295 134512640 134672761 3221224544 3221223752 134561960 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 29999 24505 603 41 0 29958 0 vsize: 119996 [startup+100.004 s] Raw data (loadavg): 1.02 0.97 0.91 2/54 16130 Raw data (stat): 16077 (minisat+) R 16076 32461 32460 0 -1 0 26520 0 0 0 9935 64 0 0 25 0 1 0 491720905 122875904 24507 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 29999 24507 603 41 0 29958 0 vsize: 119996 [startup+110.004 s] Raw data (loadavg): 1.01 0.97 0.91 2/54 16130 Raw data (stat): 16077 (minisat+) R 16076 32461 32460 0 -1 0 26527 0 0 0 10934 65 0 0 25 0 1 0 491720905 122875904 24514 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 29999 24514 603 41 0 29958 0 vsize: 119996 [startup+120.005 s] Raw data (loadavg): 1.01 0.97 0.91 2/54 16130 Raw data (stat): 16077 (minisat+) R 16076 32461 32460 0 -1 0 26533 0 0 0 11933 65 0 0 25 0 1 0 491720905 122875904 24520 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 29999 24520 603 41 0 29958 0 vsize: 119996 [startup+130.004 s] Raw data (loadavg): 1.01 0.97 0.91 2/54 16130 Raw data (stat): 16077 (minisat+) R 16076 32461 32460 0 -1 0 26533 0 0 0 12934 65 0 0 25 0 1 0 491720905 122875904 24520 4294967295 134512640 134672761 3221224544 3221223740 134556584 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 29999 24520 603 41 0 29958 0 vsize: 119996 [startup+140.004 s] Raw data (loadavg): 1.01 0.97 0.91 2/54 16132 Raw data (stat): 16077 (minisat+) R 16076 32461 32460 0 -1 0 26533 0 0 0 13934 65 0 0 25 0 1 0 491720905 122875904 24520 4294967295 134512640 134672761 3221224544 3221223744 134561972 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 29999 24520 603 41 0 29958 0 vsize: 119996 [startup+150.005 s] Raw data (loadavg): 1.01 0.97 0.91 2/54 16132 Raw data (stat): 16077 (minisat+) R 16076 32461 32460 0 -1 0 26563 0 0 0 14934 65 0 0 25 0 1 0 491720905 123129856 24550 4294967295 134512640 134672761 3221224544 3221223744 134561972 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 30061 24550 603 41 0 30020 0 vsize: 120244 [startup+160.005 s] Raw data (loadavg): 1.00 0.97 0.91 2/54 16132 Raw data (stat): 16077 (minisat+) R 16076 32461 32460 0 -1 0 26565 0 0 0 15934 65 0 0 25 0 1 0 491720905 123129856 24552 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 30061 24552 603 41 0 30020 0 vsize: 120244 [startup+170.005 s] Raw data (loadavg): 1.00 0.97 0.91 2/54 16132 Raw data (stat): 16077 (minisat+) R 16076 32461 32460 0 -1 0 26565 0 0 0 16934 65 0 0 25 0 1 0 491720905 123129856 24552 4294967295 134512640 134672761 3221224544 3221223748 134561964 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 30061 24552 603 41 0 30020 0 vsize: 120244 [startup+180.005 s] Raw data (loadavg): 1.00 0.97 0.91 2/54 16132 Raw data (stat): 16077 (minisat+) R 16076 32461 32460 0 -1 0 26594 0 0 0 17934 65 0 0 25 0 1 0 491720905 123129856 24581 4294967295 134512640 134672761 3221224544 3221223716 134556627 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 30061 24581 603 41 0 30020 0 vsize: 120244 [startup+190.005 s] Raw data (loadavg): 1.00 0.97 0.91 2/54 16132 Raw data (stat): 16077 (minisat+) R 16076 32461 32460 0 -1 0 26610 0 0 0 18935 65 0 0 25 0 1 0 491720905 123260928 24597 4294967295 134512640 134672761 3221224544 3221223716 134556602 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 30093 24597 603 41 0 30052 0 vsize: 120372 [startup+200.005 s] Raw data (loadavg): 1.00 0.97 0.91 2/54 16132 Raw data (stat): 16077 (minisat+) R 16076 32461 32460 0 -1 0 26612 0 0 0 19935 65 0 0 25 0 1 0 491720905 123260928 24599 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 30093 24599 603 41 0 30052 0 vsize: 120372 [startup+210.005 s] Raw data (loadavg): 1.00 0.97 0.91 2/54 16132 Raw data (stat): 16077 (minisat+) R 16076 32461 32460 0 -1 0 26614 0 0 0 20935 65 0 0 25 0 1 0 491720905 123260928 24601 4294967295 134512640 134672761 3221224544 3221223760 134561987 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 30093 24601 603 41 0 30052 0 vsize: 120372 [startup+220.006 s] Raw data (loadavg): 1.00 0.97 0.91 2/54 16132 Raw data (stat): 16077 (minisat+) R 16076 32461 32460 0 -1 0 26614 0 0 0 21935 65 0 0 25 0 1 0 491720905 123260928 24601 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 30093 24601 603 41 0 30052 0 vsize: 120372 [startup+230.005 s] Raw data (loadavg): 1.00 0.97 0.91 2/54 16132 Raw data (stat): 16077 (minisat+) R 16076 32461 32460 0 -1 0 26614 0 0 0 22935 65 0 0 25 0 1 0 491720905 123260928 24601 4294967295 134512640 134672761 3221224544 3221223748 134561964 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 30093 24601 603 41 0 30052 0 vsize: 120372 [startup+240.006 s] Raw data (loadavg): 1.00 0.97 0.91 2/54 16132 Raw data (stat): 16077 (minisat+) R 16076 32461 32460 0 -1 0 26618 0 0 0 23935 65 0 0 25 0 1 0 491720905 123260928 24605 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 30093 24605 603 41 0 30052 0 vsize: 120372 [startup+250.006 s] Raw data (loadavg): 1.00 0.97 0.91 2/54 16132 Raw data (stat): 16077 (minisat+) R 16076 32461 32460 0 -1 0 26622 0 0 0 24936 65 0 0 25 0 1 0 491720905 123260928 24609 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 30093 24609 603 41 0 30052 0 vsize: 120372 [startup+260.006 s] Raw data (loadavg): 1.00 0.97 0.91 2/54 16132 Raw data (stat): 16077 (minisat+) R 16076 32461 32460 0 -1 0 26624 0 0 0 25936 65 0 0 25 0 1 0 491720905 123260928 24611 4294967295 134512640 134672761 3221224544 3221223716 134556688 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 30093 24611 603 41 0 30052 0 vsize: 120372 [startup+270.006 s] Raw data (loadavg): 1.00 0.97 0.91 2/54 16132 Raw data (stat): 16077 (minisat+) R 16076 32461 32460 0 -1 0 26629 0 0 0 26936 65 0 0 25 0 1 0 491720905 123260928 24616 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 30093 24616 603 41 0 30052 0 vsize: 120372 [startup+280.005 s] Raw data (loadavg): 1.00 0.97 0.91 2/54 16132 Raw data (stat): 16077 (minisat+) R 16076 32461 32460 0 -1 0 26633 0 0 0 27936 65 0 0 25 0 1 0 491720905 123396096 24620 4294967295 134512640 134672761 3221224544 3221223744 134557911 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 30126 24620 603 41 0 30085 0 vsize: 120504 [startup+290.006 s] Raw data (loadavg): 1.00 0.97 0.91 2/54 16132 Raw data (stat): 16077 (minisat+) R 16076 32461 32460 0 -1 0 26633 0 0 0 28936 65 0 0 25 0 1 0 491720905 123396096 24620 4294967295 134512640 134672761 3221224544 3221223748 134561964 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 30126 24620 603 41 0 30085 0 vsize: 120504 [startup+300.007 s] Raw data (loadavg): 1.00 0.97 0.91 2/54 16132 Raw data (stat): 16077 (minisat+) R 16076 32461 32460 0 -1 0 26745 0 0 0 29936 66 0 0 25 0 1 0 491720905 123658240 24732 4294967295 134512640 134672761 3221224544 3221223760 134557531 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 30190 24732 603 41 0 30149 0 vsize: 120760 [startup+310.006 s] Raw data (loadavg): 1.00 0.97 0.91 2/54 16132 Raw data (stat): 16077 (minisat+) R 16076 32461 32460 0 -1 0 26837 0 0 0 30936 66 0 0 25 0 1 0 491720905 123920384 24824 4294967295 134512640 134672761 3221224544 3221223716 134556688 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 30254 24824 603 41 0 30213 0 vsize: 121016 [startup+320.005 s] Raw data (loadavg): 1.00 0.97 0.91 2/54 16132 Raw data (stat): 16077 (minisat+) R 16076 32461 32460 0 -1 0 26859 0 0 0 31936 66 0 0 25 0 1 0 491720905 123920384 24846 4294967295 134512640 134672761 3221224544 3221223716 134556643 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 30254 24846 603 41 0 30213 0 vsize: 121016 [startup+330.006 s] Raw data (loadavg): 1.00 0.97 0.91 2/54 16132 Raw data (stat): 16077 (minisat+) R 16076 32461 32460 0 -1 0 26901 0 0 0 32936 66 0 0 25 0 1 0 491720905 124055552 24888 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 30287 24888 603 41 0 30246 0 vsize: 121148 [startup+340.006 s] Raw data (loadavg): 1.00 0.97 0.91 2/54 16132 Raw data (stat): 16077 (minisat+) R 16076 32461 32460 0 -1 0 26998 0 0 0 33936 66 0 0 25 0 1 0 491720905 124325888 24985 4294967295 134512640 134672761 3221224544 3221223744 134557842 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 30353 24985 603 41 0 30312 0 vsize: 121412 [startup+350.006 s] Raw data (loadavg): 1.00 0.97 0.91 2/54 16132 Raw data (stat): 16077 (minisat+) R 16076 32461 32460 0 -1 0 27178 0 0 0 34936 66 0 0 25 0 1 0 491720905 125149184 25165 4294967295 134512640 134672761 3221224544 3221223716 134556653 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 30554 25165 603 41 0 30513 0 vsize: 122216 [startup+360.006 s] Raw data (loadavg): 1.00 0.97 0.91 2/54 16132 Raw data (stat): 16077 (minisat+) R 16076 32461 32460 0 -1 0 27275 0 0 0 35936 67 0 0 25 0 1 0 491720905 125550592 25262 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 30652 25262 603 41 0 30611 0 vsize: 122608 [startup+370.006 s] Raw data (loadavg): 1.00 0.97 0.91 2/54 16132 Raw data (stat): 16077 (minisat+) R 16076 32461 32460 0 -1 0 27527 0 0 0 36935 68 0 0 25 0 1 0 491720905 126631936 25514 4294967295 134512640 134672761 3221224544 3221223668 134566043 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 30916 25514 603 41 0 30875 0 vsize: 123664 [startup+380.006 s] Raw data (loadavg): 1.00 0.97 0.91 2/54 16132 Raw data (stat): 16077 (minisat+) R 16076 32461 32460 0 -1 0 27546 0 0 0 37935 68 0 0 25 0 1 0 491720905 126631936 25533 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 30916 25533 603 41 0 30875 0 vsize: 123664 [startup+390.006 s] Raw data (loadavg): 1.00 0.97 0.91 2/54 16132 Raw data (stat): 16077 (minisat+) R 16076 32461 32460 0 -1 0 27583 0 0 0 38935 68 0 0 25 0 1 0 491720905 126767104 25570 4294967295 134512640 134672761 3221224544 3221223712 134561164 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 30949 25570 603 41 0 30908 0 vsize: 123796 [startup+400.007 s] Raw data (loadavg): 1.00 0.97 0.91 2/54 16134 Raw data (stat): 16077 (minisat+) R 16076 32461 32460 0 -1 0 45175 0 0 0 39895 108 0 0 25 0 1 0 491720905 182243328 41186 4294967295 134512640 134672761 3221224544 3221152736 1075350517 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 44493 41187 603 41 0 44452 0 vsize: 177972 [startup+410.007 s] Raw data (loadavg): 1.00 0.97 0.91 2/54 16134 Raw data (stat): 16077 (minisat+) R 16076 32461 32460 0 -1 0 81598 0 0 0 40812 191 0 0 25 0 1 0 491720905 338219008 77608 4294967295 134512640 134672761 3221224544 3221223888 134561993 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 82573 77608 603 41 0 82532 0 vsize: 330292 [startup+420.007 s] Raw data (loadavg): 1.00 0.97 0.91 2/54 16134 Raw data (stat): 16077 (minisat+) R 16076 32461 32460 0 -1 0 81648 0 0 0 41812 192 0 0 25 0 1 0 491720905 338354176 77658 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 82606 77658 603 41 0 82565 0 vsize: 330424 [startup+430.007 s] Raw data (loadavg): 1.00 0.97 0.91 2/54 16134 Raw data (stat): 16077 (minisat+) R 16076 32461 32460 0 -1 0 81748 0 0 0 42811 192 0 0 25 0 1 0 491720905 338485248 77758 4294967295 134512640 134672761 3221224544 3221223680 134560677 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 82638 77758 603 41 0 82597 0 vsize: 330552 [startup+440.007 s] Raw data (loadavg): 1.00 0.97 0.91 2/54 16134 Raw data (stat): 16077 (minisat+) R 16076 32461 32460 0 -1 0 81782 0 0 0 43811 192 0 0 25 0 1 0 491720905 338620416 77792 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 82671 77792 603 41 0 82630 0 vsize: 330684 [startup+450.007 s] Raw data (loadavg): 1.00 0.97 0.91 2/54 16134 Raw data (stat): 16077 (minisat+) R 16076 32461 32460 0 -1 0 81826 0 0 0 44811 192 0 0 25 0 1 0 491720905 338755584 77836 4294967295 134512640 134672761 3221224544 3221223744 134557809 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 82704 77836 603 41 0 82663 0 vsize: 330816 [startup+460.006 s] Raw data (loadavg): 1.00 0.97 0.91 2/54 16134 Raw data (stat): 16077 (minisat+) R 16076 32461 32460 0 -1 0 81895 0 0 0 45811 193 0 0 25 0 1 0 491720905 339099648 77905 4294967295 134512640 134672761 3221224544 3221223680 134560709 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 82788 77905 603 41 0 82747 0 vsize: 331152 [startup+470.007 s] Raw data (loadavg): 1.00 0.97 0.91 2/54 16134 Raw data (stat): 16077 (minisat+) R 16076 32461 32460 0 -1 0 81923 0 0 0 46812 193 0 0 25 0 1 0 491720905 339234816 77933 4294967295 134512640 134672761 3221224544 3221223680 134560718 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 82821 77933 603 41 0 82780 0 vsize: 331284 [startup+480.008 s] Raw data (loadavg): 1.00 0.97 0.91 2/54 16134 Raw data (stat): 16077 (minisat+) R 16076 32461 32460 0 -1 0 81954 0 0 0 47812 193 0 0 25 0 1 0 491720905 339369984 77964 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 82854 77964 603 41 0 82813 0 vsize: 331416 [startup+490.008 s] Raw data (loadavg): 1.00 0.97 0.91 2/54 16134 Raw data (stat): 16077 (minisat+) R 16076 32461 32460 0 -1 0 81966 0 0 0 48812 193 0 0 25 0 1 0 491720905 339369984 77976 4294967295 134512640 134672761 3221224544 3221223752 134561960 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 82854 77976 603 41 0 82813 0 vsize: 331416 [startup+500.009 s] Raw data (loadavg): 1.00 0.97 0.91 2/54 16134 Raw data (stat): 16077 (minisat+) R 16076 32461 32460 0 -1 0 81974 0 0 0 49812 193 0 0 25 0 1 0 491720905 339369984 77984 4294967295 134512640 134672761 3221224544 3221223716 134556660 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 82854 77984 603 41 0 82813 0 vsize: 331416 [startup+510.009 s] Raw data (loadavg): 1.00 0.97 0.91 2/54 16134 Raw data (stat): 16077 (minisat+) R 16076 32461 32460 0 -1 0 81987 0 0 0 50812 193 0 0 25 0 1 0 491720905 339505152 77997 4294967295 134512640 134672761 3221224544 3221223680 134560598 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 82887 77997 603 41 0 82846 0 vsize: 331548 [startup+520.009 s] Raw data (loadavg): 1.00 0.97 0.91 2/54 16134 Raw data (stat): 16077 (minisat+) R 16076 32461 32460 0 -1 0 82027 0 0 0 51812 193 0 0 25 0 1 0 491720905 339640320 78037 4294967295 134512640 134672761 3221224544 3221223728 134558662 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 82920 78037 603 41 0 82879 0 vsize: 331680 [startup+530.009 s] Raw data (loadavg): 1.00 0.97 0.91 2/54 16134 Raw data (stat): 16077 (minisat+) R 16076 32461 32460 0 -1 0 82261 0 0 0 52811 194 0 0 25 0 1 0 491720905 339775488 78271 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 82953 78271 603 41 0 82912 0 vsize: 331812 [startup+540.01 s] Raw data (loadavg): 1.00 0.97 0.91 2/54 16134 Raw data (stat): 16077 (minisat+) R 16076 32461 32460 0 -1 0 82403 0 0 0 53811 194 0 0 25 0 1 0 491720905 340316160 78413 4294967295 134512640 134672761 3221224544 3221223680 134560588 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 83085 78413 603 41 0 83044 0 vsize: 332340 [startup+550.011 s] Raw data (loadavg): 1.00 0.97 0.91 2/54 16134 Raw data (stat): 16077 (minisat+) R 16076 32461 32460 0 -1 0 82642 0 0 0 54811 195 0 0 25 0 1 0 491720905 341254144 78652 4294967295 134512640 134672761 3221224544 3221223680 134560588 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 83314 78652 603 41 0 83273 0 vsize: 333256 [startup+560.01 s] Raw data (loadavg): 1.00 0.97 0.91 2/54 16134 Raw data (stat): 16077 (minisat+) R 16076 32461 32460 0 -1 0 82883 0 0 0 55810 196 0 0 25 0 1 0 491720905 342192128 78893 4294967295 134512640 134672761 3221224544 3221223744 134557836 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 83543 78893 603 41 0 83502 0 vsize: 334172 [startup+570.011 s] Raw data (loadavg): 1.00 0.97 0.91 2/54 16134 Raw data (stat): 16077 (minisat+) R 16076 32461 32460 0 -1 0 82917 0 0 0 56810 196 0 0 25 0 1 0 491720905 342454272 78927 4294967295 134512640 134672761 3221224544 3221223668 134566118 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 83607 78927 603 41 0 83566 0 vsize: 334428 [startup+580.011 s] Raw data (loadavg): 1.00 0.97 0.91 2/54 16134 Raw data (stat): 16077 (minisat+) R 16076 32461 32460 0 -1 0 82949 0 0 0 57810 196 0 0 25 0 1 0 491720905 342589440 78959 4294967295 134512640 134672761 3221224544 3221223680 134560640 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 83640 78959 603 41 0 83599 0 vsize: 334560 [startup+590.012 s] Raw data (loadavg): 1.00 0.97 0.91 2/54 16134 Raw data (stat): 16077 (minisat+) R 16076 32461 32460 0 -1 0 82979 0 0 0 58810 196 0 0 25 0 1 0 491720905 342724608 78989 4294967295 134512640 134672761 3221224544 3221223712 134561118 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 83673 78989 603 41 0 83632 0 vsize: 334692 [startup+600.012 s] Raw data (loadavg): 1.00 0.97 0.91 2/54 16134 Raw data (stat): 16077 (minisat+) R 16076 32461 32460 0 -1 0 83000 0 0 0 59810 196 0 0 25 0 1 0 491720905 342859776 79010 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 83706 79010 603 41 0 83665 0 vsize: 334824 [startup+610.012 s] Raw data (loadavg): 1.00 0.97 0.91 2/54 16134 Raw data (stat): 16077 (minisat+) R 16076 32461 32460 0 -1 0 83032 0 0 0 60810 196 0 0 25 0 1 0 491720905 342994944 79042 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 83739 79042 603 41 0 83698 0 vsize: 334956 [startup+620.012 s] Raw data (loadavg): 1.00 0.97 0.91 2/54 16134 Raw data (stat): 16077 (minisat+) R 16076 32461 32460 0 -1 0 83049 0 0 0 61810 196 0 0 25 0 1 0 491720905 342994944 79059 4294967295 134512640 134672761 3221224544 3221223716 134556649 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 83739 79059 603 41 0 83698 0 vsize: 334956 [startup+630.012 s] Raw data (loadavg): 1.00 0.97 0.91 2/54 16134 Raw data (stat): 16077 (minisat+) R 16076 32461 32460 0 -1 0 83061 0 0 0 62810 196 0 0 25 0 1 0 491720905 342994944 79071 4294967295 134512640 134672761 3221224544 3221223712 134561375 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 83739 79071 603 41 0 83698 0 vsize: 334956 [startup+640.013 s] Raw data (loadavg): 1.00 0.97 0.91 2/54 16134 Raw data (stat): 16077 (minisat+) R 16076 32461 32460 0 -1 0 83170 0 0 0 63810 197 0 0 25 0 1 0 491720905 343265280 79180 4294967295 134512640 134672761 3221224544 3221223744 134557809 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 83805 79180 603 41 0 83764 0 vsize: 335220 [startup+650.012 s] Raw data (loadavg): 1.00 0.97 0.91 2/54 16134 Raw data (stat): 16077 (minisat+) R 16076 32461 32460 0 -1 0 83195 0 0 0 64810 197 0 0 25 0 1 0 491720905 343265280 79205 4294967295 134512640 134672761 3221224544 3221223712 134560825 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 83805 79205 603 41 0 83764 0 vsize: 335220 [startup+660.013 s] Raw data (loadavg): 1.00 0.97 0.91 2/54 16134 Raw data (stat): 16077 (minisat+) R 16076 32461 32460 0 -1 0 83236 0 0 0 65810 197 0 0 25 0 1 0 491720905 343527424 79246 4294967295 134512640 134672761 3221224544 3221223744 134557842 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 83869 79246 603 41 0 83828 0 vsize: 335476 [startup+670.013 s] Raw data (loadavg): 1.00 0.97 0.91 2/54 16134 Raw data (stat): 16077 (minisat+) R 16076 32461 32460 0 -1 0 83285 0 0 0 66810 197 0 0 25 0 1 0 491720905 343662592 79295 4294967295 134512640 134672761 3221224544 3221223712 134561229 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 83902 79295 603 41 0 83861 0 vsize: 335608 [startup+680.013 s] Raw data (loadavg): 1.00 0.97 0.91 2/54 16134 Raw data (stat): 16077 (minisat+) R 16076 32461 32460 0 -1 0 83454 0 0 0 67810 198 0 0 25 0 1 0 491720905 344334336 79464 4294967295 134512640 134672761 3221224544 3221223704 134561238 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 84066 79464 603 41 0 84025 0 vsize: 336264 [startup+690.014 s] Raw data (loadavg): 1.00 0.97 0.91 2/54 16134 Raw data (stat): 16077 (minisat+) R 16076 32461 32460 0 -1 0 83500 0 0 0 68810 198 0 0 25 0 1 0 491720905 344469504 79510 4294967295 134512640 134672761 3221224544 3221223712 134560956 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 84099 79510 603 41 0 84058 0 vsize: 336396 [startup+700.013 s] Raw data (loadavg): 1.00 0.97 0.91 2/54 16134 Raw data (stat): 16077 (minisat+) R 16076 32461 32460 0 -1 0 83528 0 0 0 69810 198 0 0 25 0 1 0 491720905 344604672 79538 4294967295 134512640 134672761 3221224544 3221223716 134556649 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 84132 79538 603 41 0 84091 0 vsize: 336528 [startup+710.013 s] Raw data (loadavg): 1.00 0.97 0.91 2/54 16134 Raw data (stat): 16077 (minisat+) R 16076 32461 32460 0 -1 0 83539 0 0 0 70810 198 0 0 25 0 1 0 491720905 344739840 79549 4294967295 134512640 134672761 3221224544 3221223712 134561382 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 84165 79549 603 41 0 84124 0 vsize: 336660 [startup+720.014 s] Raw data (loadavg): 1.00 0.97 0.91 2/54 16134 Raw data (stat): 16077 (minisat+) R 16076 32461 32460 0 -1 0 83570 0 0 0 71810 198 0 0 25 0 1 0 491720905 344739840 79580 4294967295 134512640 134672761 3221224544 3221223680 134560557 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 84165 79580 603 41 0 84124 0 vsize: 336660 [startup+730.014 s] Raw data (loadavg): 1.00 0.97 0.91 2/54 16134 Raw data (stat): 16077 (minisat+) R 16076 32461 32460 0 -1 0 83660 0 0 0 72810 198 0 0 25 0 1 0 491720905 345141248 79670 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 84263 79670 603 41 0 84222 0 vsize: 337052 [startup+740.015 s] Raw data (loadavg): 1.00 0.97 0.91 2/54 16134 Raw data (stat): 16077 (minisat+) R 16076 32461 32460 0 -1 0 83691 0 0 0 73810 198 0 0 25 0 1 0 491720905 345534464 79701 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 84359 79701 603 41 0 84318 0 vsize: 337436 [startup+750.015 s] Raw data (loadavg): 1.00 0.97 0.91 2/54 16134 Raw data (stat): 16077 (minisat+) R 16076 32461 32460 0 -1 0 83701 0 0 0 74811 198 0 0 25 0 1 0 491720905 345534464 79711 4294967295 134512640 134672761 3221224544 3221223680 134560588 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 84359 79711 603 41 0 84318 0 vsize: 337436 [startup+760.015 s] Raw data (loadavg): 1.00 0.97 0.91 2/54 16134 Raw data (stat): 16077 (minisat+) R 16076 32461 32460 0 -1 0 83753 0 0 0 75811 198 0 0 25 0 1 0 491720905 345804800 79763 4294967295 134512640 134672761 3221224544 3221223712 134561272 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 84425 79763 603 41 0 84384 0 vsize: 337700 [startup+770.015 s] Raw data (loadavg): 1.00 0.97 0.91 2/54 16134 Raw data (stat): 16077 (minisat+) R 16076 32461 32460 0 -1 0 83775 0 0 0 76811 198 0 0 25 0 1 0 491720905 345804800 79785 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 84425 79785 603 41 0 84384 0 vsize: 337700 [startup+780.015 s] Raw data (loadavg): 1.00 0.97 0.91 2/54 16134 Raw data (stat): 16077 (minisat+) R 16076 32461 32460 0 -1 0 83827 0 0 0 77811 199 0 0 25 0 1 0 491720905 346075136 79837 4294967295 134512640 134672761 3221224544 3221223728 134559498 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 84491 79837 603 41 0 84450 0 vsize: 337964 [startup+790.016 s] Raw data (loadavg): 1.00 0.97 0.91 2/54 16134 Raw data (stat): 16077 (minisat+) R 16076 32461 32460 0 -1 0 83862 0 0 0 78811 199 0 0 25 0 1 0 491720905 346206208 79872 4294967295 134512640 134672761 3221224544 3221223680 134560688 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 84523 79872 603 41 0 84482 0 vsize: 338092 [startup+800.015 s] Raw data (loadavg): 1.00 0.97 0.91 2/54 16134 Raw data (stat): 16077 (minisat+) R 16076 32461 32460 0 -1 0 83906 0 0 0 79811 199 0 0 25 0 1 0 491720905 346337280 79916 4294967295 134512640 134672761 3221224544 3221223712 134561229 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 84555 79916 603 41 0 84514 0 vsize: 338220 [startup+810.015 s] Raw data (loadavg): 1.00 0.97 0.91 2/54 16134 Raw data (stat): 16077 (minisat+) R 16076 32461 32460 0 -1 0 83946 0 0 0 80811 199 0 0 25 0 1 0 491720905 346603520 79956 4294967295 134512640 134672761 3221224544 3221223680 134560588 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 84620 79956 603 41 0 84579 0 vsize: 338480 [startup+820.016 s] Raw data (loadavg): 1.00 0.97 0.91 2/54 16134 Raw data (stat): 16077 (minisat+) R 16076 32461 32460 0 -1 0 83988 0 0 0 81811 199 0 0 25 0 1 0 491720905 346738688 79998 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 84653 79998 603 41 0 84612 0 vsize: 338612 [startup+830.016 s] Raw data (loadavg): 1.00 0.97 0.91 2/54 16134 Raw data (stat): 16077 (minisat+) R 16076 32461 32460 0 -1 0 84034 0 0 0 82811 199 0 0 25 0 1 0 491720905 346869760 80044 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 84685 80044 603 41 0 84644 0 vsize: 338740 [startup+840.016 s] Raw data (loadavg): 1.00 0.97 0.91 2/54 16134 Raw data (stat): 16077 (minisat+) R 16076 32461 32460 0 -1 0 84084 0 0 0 83811 199 0 0 25 0 1 0 491720905 347136000 80094 4294967295 134512640 134672761 3221224544 3221223712 134560839 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 84750 80094 603 41 0 84709 0 vsize: 339000 [startup+850.016 s] Raw data (loadavg): 1.00 0.97 0.91 2/54 16134 Raw data (stat): 16077 (minisat+) R 16076 32461 32460 0 -1 0 84140 0 0 0 84811 200 0 0 25 0 1 0 491720905 347398144 80150 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 84814 80150 603 41 0 84773 0 vsize: 339256 [startup+860.016 s] Raw data (loadavg): 1.00 0.97 0.91 2/54 16134 Raw data (stat): 16077 (minisat+) R 16076 32461 32460 0 -1 0 84193 0 0 0 85811 200 0 0 25 0 1 0 491720905 347533312 80203 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 84847 80203 603 41 0 84806 0 vsize: 339388 [startup+870.016 s] Raw data (loadavg): 1.00 0.97 0.91 2/54 16134 Raw data (stat): 16077 (minisat+) R 16076 32461 32460 0 -1 0 84253 0 0 0 86811 200 0 0 25 0 1 0 491720905 347799552 80263 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 84912 80263 603 41 0 84871 0 vsize: 339648 [startup+880.016 s] Raw data (loadavg): 1.00 0.97 0.91 2/54 16134 Raw data (stat): 16077 (minisat+) R 16076 32461 32460 0 -1 0 84316 0 0 0 87811 200 0 0 25 0 1 0 491720905 348065792 80326 4294967295 134512640 134672761 3221224544 3221223544 1075350517 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 84977 80326 603 41 0 84936 0 vsize: 339908 [startup+890.016 s] Raw data (loadavg): 1.00 0.97 0.91 2/54 16134 Raw data (stat): 16077 (minisat+) R 16076 32461 32460 0 -1 0 84387 0 0 0 88811 200 0 0 25 0 1 0 491720905 348336128 80397 4294967295 134512640 134672761 3221224544 3221223680 134560688 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 85043 80397 603 41 0 85002 0 vsize: 340172 [startup+900.016 s] Raw data (loadavg): 1.00 0.97 0.91 2/54 16134 Raw data (stat): 16077 (minisat+) R 16076 32461 32460 0 -1 0 84447 0 0 0 89811 201 0 0 25 0 1 0 491720905 348606464 80457 4294967295 134512640 134672761 3221224544 3221223648 134559890 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 85109 80457 603 41 0 85068 0 vsize: 340436 [startup+910.016 s] Raw data (loadavg): 1.00 0.97 0.91 2/54 16134 Raw data (stat): 16077 (minisat+) R 16076 32461 32460 0 -1 0 84511 0 0 0 90811 201 0 0 25 0 1 0 491720905 348876800 80521 4294967295 134512640 134672761 3221224544 3221223680 134560652 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 85175 80521 603 41 0 85134 0 vsize: 340700 [startup+920.017 s] Raw data (loadavg): 1.00 0.97 0.91 2/54 16134 Raw data (stat): 16077 (minisat+) R 16076 32461 32460 0 -1 0 84564 0 0 0 91810 201 0 0 25 0 1 0 491720905 349011968 80574 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 85208 80574 603 41 0 85167 0 vsize: 340832 [startup+930.017 s] Raw data (loadavg): 1.00 0.97 0.91 2/54 16134 Raw data (stat): 16077 (minisat+) R 16076 32461 32460 0 -1 0 84616 0 0 0 92810 201 0 0 25 0 1 0 491720905 349282304 80626 4294967295 134512640 134672761 3221224544 3221223744 134557842 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 85274 80626 603 41 0 85233 0 vsize: 341096 [startup+940.017 s] Raw data (loadavg): 1.00 0.97 0.91 2/54 16134 Raw data (stat): 16077 (minisat+) R 16076 32461 32460 0 -1 0 84664 0 0 0 93810 202 0 0 25 0 1 0 491720905 349417472 80674 4294967295 134512640 134672761 3221224544 3221223712 134561229 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 85307 80674 603 41 0 85266 0 vsize: 341228 [startup+950.017 s] Raw data (loadavg): 1.00 0.97 0.91 2/54 16134 Raw data (stat): 16077 (minisat+) R 16076 32461 32460 0 -1 0 84700 0 0 0 94810 202 0 0 25 0 1 0 491720905 349556736 80710 4294967295 134512640 134672761 3221224544 3221223712 134561229 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 85341 80710 603 41 0 85300 0 vsize: 341364 [startup+960.017 s] Raw data (loadavg): 1.00 0.97 0.91 2/54 16134 Raw data (stat): 16077 (minisat+) R 16076 32461 32460 0 -1 0 84747 0 0 0 95810 202 0 0 25 0 1 0 491720905 349822976 80757 4294967295 134512640 134672761 3221224544 3221223680 134560588 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 85406 80757 603 41 0 85365 0 vsize: 341624 [startup+970.018 s] Raw data (loadavg): 1.00 0.97 0.91 2/54 16134 Raw data (stat): 16077 (minisat+) R 16076 32461 32460 0 -1 0 84794 0 0 0 96810 202 0 0 25 0 1 0 491720905 349954048 80804 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 85438 80804 603 41 0 85397 0 vsize: 341752 [startup+980.018 s] Raw data (loadavg): 1.00 0.97 0.91 2/54 16134 Raw data (stat): 16077 (minisat+) R 16076 32461 32460 0 -1 0 84852 0 0 0 97810 203 0 0 25 0 1 0 491720905 350220288 80862 4294967295 134512640 134672761 3221224544 3221223680 134560642 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 85503 80862 603 41 0 85462 0 vsize: 342012 [startup+990.018 s] Raw data (loadavg): 1.00 0.97 0.91 2/54 16134 Raw data (stat): 16077 (minisat+) R 16076 32461 32460 0 -1 0 84893 0 0 0 98810 203 0 0 25 0 1 0 491720905 350351360 80903 4294967295 134512640 134672761 3221224544 3221223728 134558662 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 85535 80903 603 41 0 85494 0 vsize: 342140 [startup+1000.02 s] Raw data (loadavg): 1.00 0.97 0.91 2/54 16134 Raw data (stat): 16077 (minisat+) R 16076 32461 32460 0 -1 0 84946 0 0 0 99810 203 0 0 25 0 1 0 491720905 350617600 80956 4294967295 134512640 134672761 3221224544 3221223712 134561266 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 85600 80956 603 41 0 85559 0 vsize: 342400 [startup+1010.02 s] Raw data (loadavg): 1.00 0.97 0.91 2/54 16134 Raw data (stat): 16077 (minisat+) R 16076 32461 32460 0 -1 0 85001 0 0 0 100810 203 0 0 25 0 1 0 491720905 350879744 81011 4294967295 134512640 134672761 3221224544 3221223744 134557895 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 85664 81011 603 41 0 85623 0 vsize: 342656 [startup+1020.02 s] Raw data (loadavg): 1.00 0.97 0.91 2/54 16134 Raw data (stat): 16077 (minisat+) R 16076 32461 32460 0 -1 0 85049 0 0 0 101810 203 0 0 25 0 1 0 491720905 351014912 81059 4294967295 134512640 134672761 3221224544 3221223648 134560005 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 85697 81059 603 41 0 85656 0 vsize: 342788 [startup+1030.02 s] Raw data (loadavg): 1.00 0.97 0.91 2/54 16134 Raw data (stat): 16077 (minisat+) R 16076 32461 32460 0 -1 0 85092 0 0 0 102810 203 0 0 25 0 1 0 491720905 351145984 81102 4294967295 134512640 134672761 3221224544 3221223680 134560588 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 85729 81102 603 41 0 85688 0 vsize: 342916 [startup+1040.02 s] Raw data (loadavg): 1.00 0.97 0.91 2/54 16134 Raw data (stat): 16077 (minisat+) R 16076 32461 32460 0 -1 0 85116 0 0 0 103810 203 0 0 25 0 1 0 491720905 351281152 81126 4294967295 134512640 134672761 3221224544 3221223744 134557911 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 85762 81126 603 41 0 85721 0 vsize: 343048 [startup+1050.02 s] Raw data (loadavg): 1.00 0.97 0.91 2/54 16134 Raw data (stat): 16077 (minisat+) R 16076 32461 32460 0 -1 0 85212 0 0 0 104810 204 0 0 25 0 1 0 491720905 351686656 81222 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 85861 81222 603 41 0 85820 0 vsize: 343444 [startup+1060.02 s] Raw data (loadavg): 1.00 0.97 0.91 2/54 16134 Raw data (stat): 16077 (minisat+) R 16076 32461 32460 0 -1 0 85264 0 0 0 105810 204 0 0 25 0 1 0 491720905 351817728 81274 4294967295 134512640 134672761 3221224544 3221223740 134556678 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 85893 81274 603 41 0 85852 0 vsize: 343572 [startup+1070.02 s] Raw data (loadavg): 1.00 0.97 0.91 2/54 16134 Raw data (stat): 16077 (minisat+) R 16076 32461 32460 0 -1 0 85278 0 0 0 106810 204 0 0 25 0 1 0 491720905 351952896 81288 4294967295 134512640 134672761 3221224544 3221223712 134560871 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 85926 81288 603 41 0 85885 0 vsize: 343704 [startup+1080.02 s] Raw data (loadavg): 1.00 0.97 0.91 2/54 16134 Raw data (stat): 16077 (minisat+) R 16076 32461 32460 0 -1 0 85370 0 0 0 107810 204 0 0 25 0 1 0 491720905 352354304 81380 4294967295 134512640 134672761 3221224544 3221223744 134557809 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 86024 81380 603 41 0 85983 0 vsize: 344096 [startup+1090.02 s] Raw data (loadavg): 1.00 0.97 0.91 2/54 16134 Raw data (stat): 16077 (minisat+) R 16076 32461 32460 0 -1 0 85421 0 0 0 108810 204 0 0 25 0 1 0 491720905 352485376 81431 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 86056 81431 603 41 0 86015 0 vsize: 344224 [startup+1100.02 s] Raw data (loadavg): 1.00 0.97 0.91 2/54 16134 Raw data (stat): 16077 (minisat+) R 16076 32461 32460 0 -1 0 85458 0 0 0 109810 204 0 0 25 0 1 0 491720905 352616448 81468 4294967295 134512640 134672761 3221224544 3221223680 134560703 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 86088 81468 603 41 0 86047 0 vsize: 344352 [startup+1110.02 s] Raw data (loadavg): 1.00 0.97 0.91 2/54 16134 Raw data (stat): 16077 (minisat+) R 16076 32461 32460 0 -1 0 85518 0 0 0 110809 205 0 0 25 0 1 0 491720905 352886784 81528 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 86154 81528 603 41 0 86113 0 vsize: 344616 [startup+1120.02 s] Raw data (loadavg): 1.00 0.97 0.91 2/54 16134 Raw data (stat): 16077 (minisat+) R 16076 32461 32460 0 -1 0 85583 0 0 0 111808 205 0 0 25 0 1 0 491720905 353153024 81593 4294967295 134512640 134672761 3221224544 3221223680 134560590 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 86219 81593 603 41 0 86178 0 vsize: 344876 [startup+1130.02 s] Raw data (loadavg): 1.00 0.97 0.91 2/54 16134 Raw data (stat): 16077 (minisat+) R 16076 32461 32460 0 -1 0 85594 0 0 0 112808 206 0 0 25 0 1 0 491720905 353153024 81604 4294967295 134512640 134672761 3221224544 3221223680 134560634 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 86219 81604 603 41 0 86178 0 vsize: 344876 [startup+1140.02 s] Raw data (loadavg): 1.00 0.97 0.91 2/54 16134 Raw data (stat): 16077 (minisat+) R 16076 32461 32460 0 -1 0 85599 0 0 0 113808 206 0 0 25 0 1 0 491720905 353153024 81609 4294967295 134512640 134672761 3221224544 3221223748 134561964 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 86219 81609 603 41 0 86178 0 vsize: 344876 [startup+1150.02 s] Raw data (loadavg): 1.00 0.97 0.91 2/54 16134 Raw data (stat): 16077 (minisat+) R 16076 32461 32460 0 -1 0 85620 0 0 0 114808 206 0 0 25 0 1 0 491720905 353288192 81630 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 86252 81630 603 41 0 86211 0 vsize: 345008 [startup+1160.02 s] Raw data (loadavg): 1.00 0.97 0.91 2/54 16134 Raw data (stat): 16077 (minisat+) R 16076 32461 32460 0 -1 0 85652 0 0 0 115808 206 0 0 25 0 1 0 491720905 353423360 81662 4294967295 134512640 134672761 3221224544 3221223716 134556688 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 86285 81662 603 41 0 86244 0 vsize: 345140 [startup+1170.02 s] Raw data (loadavg): 1.00 0.97 0.91 2/54 16134 Raw data (stat): 16077 (minisat+) R 16076 32461 32460 0 -1 0 85719 0 0 0 116808 206 0 0 25 0 1 0 491720905 353693696 81729 4294967295 134512640 134672761 3221224544 3221223544 1075350517 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 86351 81729 603 41 0 86310 0 vsize: 345404 [startup+1180.02 s] Raw data (loadavg): 1.00 0.97 0.91 2/54 16134 Raw data (stat): 16077 (minisat+) R 16076 32461 32460 0 -1 0 85737 0 0 0 117808 206 0 0 25 0 1 0 491720905 353693696 81747 4294967295 134512640 134672761 3221224544 3221223708 134561235 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 86351 81747 603 41 0 86310 0 vsize: 345404 [startup+1190.02 s] Raw data (loadavg): 1.00 0.97 0.91 2/54 16134 Raw data (stat): 16077 (minisat+) R 16076 32461 32460 0 -1 0 85814 0 0 0 118808 207 0 0 25 0 1 0 491720905 354099200 81824 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 86450 81824 603 41 0 86409 0 vsize: 345800 [startup+1200.02 s] Raw data (loadavg): 1.00 0.97 0.91 2/54 16134 Raw data (stat): 16077 (minisat+) R 16076 32461 32460 0 -1 0 86108 0 0 0 119807 207 0 0 25 0 1 0 491720905 355180544 82118 4294967295 134512640 134672761 3221224544 3221223648 134560289 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 86714 82118 603 41 0 86673 0 vsize: 346856 Maximum CPU time exceeded: sending SIGTERM and SIGKILL [startup+1200.19 s] Raw data (loadavg): 1.00 0.97 0.91 1/54 16134 Raw data (stat): 16077 (minisat+) Z 16076 32461 32460 0 -1 12 86111 0 0 0 119808 224 0 0 25 0 1 0 491720905 0 0 4294967295 0 0 0 0 0 0 16384 5 16386 3222412051 0 0 17 1 0 0 Raw data (statm): 0 0 0 0 0 0 0 vsize: 0 Maximum CPU time exceeded: sending SIGTERM and SIGKILL Child status: 10 Real time (s): 1200.19 CPU time (s): 1200.33 CPU user time (s): 1198.08 CPU system time (s): 2.24166 CPU usage (%): 100.011 Max. virtual memory (Kb): 346856 #### END WATCHER DATA #### #### BEGIN VERIFIER DATA #### ERROR: no interpretation found ! #### END VERIFIER DATA ####