| Name | mps-v2-13-7/MIPLIB/miplib3/normalized-mps-v2-13-7-p2756.opb |
| MD5SUM | 49fba7b1c2f3e65c53f8418d126e3ec3 |
| Bench Category | optimization, small integers (OPTSMALLINT) |
| Has Objective Function | YES |
| Satisfiable | YES |
| (Un)Satisfiability was proved | YES |
| Best value of the objective function | 3709 |
| 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 | 1247.64 |
| 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 |
LAUNCH ON wulflinc2 THE 2005-09-20 04:34:20 (client local time) PB2005-SCRIPT v4.0 MARKUPS: idlaunch=3383 boxname=wulflinc2 idbench=1039 idsolver=3 numberseed=0 MD5SUM SOLVER: MD5SUM BENCH: 49fba7b1c2f3e65c53f8418d126e3ec3 /oldhome/oroussel/tmp/wulflinc2/normalized-mps-v2-13-7-p2756.opb REAL COMMAND: minisat+_script /oldhome/oroussel/tmp/wulflinc2/normalized-mps-v2-13-7-p2756.opb IDLAUNCH: 3383 /proc/cpuinfo: processor : 0 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 2 cpu MHz : 451.191 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.191 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: 912044 kB Buffers: 13764 kB Cached: 84240 kB SwapCached: 1004 kB Active: 16916 kB Inactive: 83688 kB HighTotal: 131008 kB HighFree: 45276 kB LowTotal: 903652 kB LowFree: 866768 kB SwapTotal: 2097136 kB SwapFree: 2095552 kB Dirty: 28 kB Writeback: 0 kB Mapped: 5600 kB Slab: 16456 kB Committed_AS: 72492 kB PageTables: 332 kB VmallocTotal: 114680 kB VmallocUsed: 1388 kB VmallocChunk: 113256 kB JOB ENDED THE 2005-09-20 04:54:31 (client local time) WITH STATUS 10 IN 1208.81 SECONDS stats: 3383 7 1208.81 10
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]---> Sorter-cost: 1050 Base: 7 3 3 2 c ---[ 745]---> BDD-cost: 64 c ---[ 744]---> BDD-cost: 37 c ---[ 743]---> BDD-cost: 17 c ---[ 742]---> BDD-cost: 29 c ---[ 741]---> Sorter-cost: 807 Base: 5 2 2 2 3 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]---> Sorter-cost: 586 Base: 2 2 2 2 2 5 c ---[ 721]---> Sorter-cost: 1046 Base: 3 3 3 2 17 c ---[ 720]---> Sorter-cost: 774 Base: 3 3 2 3 17 c ---[ 719]---> BDD-cost: 102 c ---[ 718]---> Sorter-cost: 757 Base: 2 2 2 2 2 5 c ---[ 717]---> Sorter-cost: 670 Base: 2 2 2 2 2 5 c ---[ 716]---> BDD-cost: 165 c ---[ 715]---> BDD-cost: 90 c ---[ 714]---> Sorter-cost: 555 Base: 2 2 2 2 2 2 2 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]---> Sorter-cost: 634 Base: 2 2 2 2 2 5 c ---[ 707]---> Sorter-cost: 993 Base: 3 3 3 2 17 c ---[ 706]---> Sorter-cost: 759 Base: 3 3 3 2 17 c ---[ 705]---> BDD-cost: 109 c ---[ 704]---> Sorter-cost: 820 Base: 3 3 3 2 3 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]---> Sorter-cost: 1225 Base: 3 3 3 2 2 c ---[ 679]---> Sorter-cost: 1627 Base: 3 3 3 2 2 c ---[ 678]---> Sorter-cost: 1475 Base: 3 3 3 2 2 c ---[ 677]---> Sorter-cost: 886 Base: 3 3 3 2 3 c ---[ 676]---> Sorter-cost: 1364 Base: 3 3 3 2 2 c ---[ 675]---> Sorter-cost: 1206 Base: 3 3 3 2 2 c ---[ 674]---> BDD-cost: 63 c ---[ 673]---> BDD-cost: 177 c ---[ 672]---> Sorter-cost: 1281 Base: 3 3 5 2 c ---[ 671]---> Sorter-cost: 1586 Base: 3 3 3 2 2 c ---[ 670]---> Sorter-cost: 1514 Base: 3 3 3 2 2 c ---[ 669]---> BDD-cost: 113 c ---[ 668]---> Sorter-cost: 1402 Base: 3 3 3 2 2 c ---[ 667]---> BDD-cost: 190 c ---[ 666]---> BDD-cost: 157 c ---[ 665]---> Sorter-cost: 929 Base: 3 3 5 2 c ---[ 663]---> Sorter-cost: 1077 Base: 3 3 5 2 11 c ---[ 662]---> BDD-cost: 109 c ---[ 661]---> BDD-cost: 231 c ---[ 660]---> Sorter-cost: 1074 Base: 3 3 3 2 17 c ---[ 658]---> Sorter-cost: 1216 Base: 3 3 5 2 c ---[ 657]---> Sorter-cost: 995 Base: 3 3 3 2 2 c ---[ 656]---> BDD-cost: 216 c ---[ 655]---> Sorter-cost: 1087 Base: 3 3 5 2 11 c ---[ 653]---> BDD-cost: 105 c ---[ 652]---> Sorter-cost: 1073 Base: 3 3 3 2 17 c ---[ 651]---> BDD-cost: 100 c ---[ 650]---> Sorter-cost: 1092 Base: 3 3 3 2 2 c ---[ 649]---> BDD-cost: 131 c ---[ 648]---> BDD-cost: 193 c ---[ 647]---> Sorter-cost: 802 Base: 2 2 5 2 3 c ---[ 646]---> BDD-cost: 67 c ---[ 645]---> BDD-cost: 111 c ---[ 644]---> Sorter-cost: 931 Base: 5 2 3 3 11 c ---[ 643]---> Sorter-cost: 797 Base: 3 3 3 2 17 c ---[ 642]---> Sorter-cost: 1035 Base: 5 3 3 2 c ---[ 641]---> Sorter-cost: 779 Base: 2 2 5 2 3 c ---[ 640]---> BDD-cost: 64 c ---[ 639]---> BDD-cost: 126 c ---[ 638]---> BDD-cost: 103 c ---[ 637]---> BDD-cost: 110 c ---[ 636]---> Sorter-cost: 1070 Base: 5 3 3 3 c ---[ 635]---> Sorter-cost: 736 Base: 5 2 3 2 2 c ---[ 634]---> BDD-cost: 70 c ---[ 633]---> BDD-cost: 114 c ---[ 632]---> BDD-cost: 186 c ---[ 631]---> BDD-cost: 191 c ---[ 630]---> Sorter-cost: 1065 Base: 3 3 5 3 c ---[ 629]---> Sorter-cost: 730 Base: 5 2 3 2 2 c ---[ 628]---> BDD-cost: 44 c ---[ 627]---> BDD-cost: 144 c ---[ 626]---> BDD-cost: 90 c ---[ 625]---> BDD-cost: 63 c ---[ 624]---> Sorter-cost: 1075 Base: 5 2 3 3 5 c ---[ 623]---> Sorter-cost: 1156 Base: 5 2 3 3 c ---[ 622]---> Sorter-cost: 779 Base: 3 3 3 2 2 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]---> Sorter-cost: 711 Base: 3 3 3 2 3 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]---> Sorter-cost: 762 Base: 5 2 3 3 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]---> Sorter-cost: 804 Base: 5 2 3 3 c ---[ 593]---> BDD-cost: 159 c ---[ 592]---> BDD-cost: 154 c ---[ 591]---> BDD-cost: 148 c ---[ 590]---> BDD-cost: 18 c ---[ 589]---> Sorter-cost: 1077 Base: 5 2 3 3 c ---[ 588]---> Sorter-cost: 977 Base: 3 3 2 3 17 c ---[ 587]---> Sorter-cost: 1107 Base: 5 3 3 2 c ---[ 586]---> BDD-cost: 134 c ---[ 585]---> BDD-cost: 76 c ---[ 584]---> Sorter-cost: 1081 Base: 5 3 3 2 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: 142 c ---[ 565]---> BDD-cost: 66 c ---[ 564]---> BDD-cost: 14 c ---[ 563]---> BDD-cost: 16 c ---[ 562]---> BDD-cost: 10 c ---[ 561]---> BDD-cost: 138 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: 111 c ---[ 539]---> Sorter-cost: 808 Base: 3 3 3 2 3 c ---[ 538]---> Sorter-cost: 763 Base: 3 3 2 3 2 c ---[ 537]---> BDD-cost: 22 c ---[ 536]---> BDD-cost: 142 c ---[ 535]---> Sorter-cost: 698 Base: 5 2 3 2 2 c ---[ 532]---> BDD-cost: 143 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: 102 c ---[ 525]---> Sorter-cost: 880 Base: 3 3 2 3 3 c ---[ 524]---> Sorter-cost: 640 Base: 3 3 3 2 2 c ---[ 523]---> BDD-cost: 21 c ---[ 522]---> BDD-cost: 110 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: 179 c ---[ 497]---> BDD-cost: 148 c ---[ 496]---> Sorter-cost: 1206 Base: 3 3 3 2 13 c ---[ 495]---> Sorter-cost: 772 Base: 3 3 3 2 2 c ---[ 494]---> BDD-cost: 134 c ---[ 493]---> BDD-cost: 87 c ---[ 492]---> BDD-cost: 26 c ---[ 491]---> BDD-cost: 22 c ---[ 490]---> Sorter-cost: 842 Base: 3 3 5 2 7 c ---[ 489]---> Sorter-cost: 1348 Base: 3 3 3 2 3 c ---[ 488]---> Sorter-cost: 1331 Base: 3 3 5 2 5 c ---[ 486]---> Sorter-cost: 1144 Base: 3 3 5 2 5 c ---[ 485]---> BDD-cost: 20 c ---[ 484]---> BDD-cost: 41 c ---[ 483]---> Sorter-cost: 543 Base: 3 3 5 2 c ---[ 482]---> BDD-cost: 17 c ---[ 481]---> Sorter-cost: 1034 Base: 3 3 3 2 2 c ---[ 480]---> BDD-cost: 13 c ---[ 479]---> BDD-cost: 39 c ---[ 478]---> Sorter-cost: 815 Base: 3 3 3 2 2 c ---[ 477]---> BDD-cost: 17 c ---[ 476]---> BDD-cost: 162 c ---[ 475]---> Sorter-cost: 842 Base: 3 3 5 2 11 c ---[ 473]---> Sorter-cost: 1010 Base: 3 3 3 2 2 c ---[ 472]---> BDD-cost: 18 c ---[ 471]---> BDD-cost: 22 c ---[ 470]---> Sorter-cost: 814 Base: 3 3 3 2 2 c ---[ 469]---> BDD-cost: 4 c ---[ 468]---> BDD-cost: 178 c ---[ 467]---> BDD-cost: 58 c ---[ 465]---> BDD-cost: 140 c ---[ 464]---> BDD-cost: 35 c ---[ 463]---> BDD-cost: 30 c ---[ 462]---> Sorter-cost: 775 Base: 5 2 3 3 c ---[ 461]---> Sorter-cost: 688 Base: 3 3 2 3 2 c ---[ 460]---> Sorter-cost: 744 Base: 5 3 3 3 c ---[ 459]---> BDD-cost: 153 c ---[ 458]---> BDD-cost: 45 c ---[ 457]---> BDD-cost: 37 c ---[ 454]---> Sorter-cost: 599 Base: 5 3 3 3 c ---[ 453]---> BDD-cost: 146 c ---[ 452]---> BDD-cost: 37 c ---[ 451]---> BDD-cost: 30 c ---[ 450]---> BDD-cost: 162 c ---[ 449]---> BDD-cost: 136 c ---[ 448]---> Sorter-cost: 883 Base: 5 3 3 3 c ---[ 447]---> Sorter-cost: 689 Base: 5 2 3 5 c ---[ 446]---> BDD-cost: 48 c ---[ 445]---> BDD-cost: 58 c ---[ 444]---> BDD-cost: 13 c ---[ 442]---> Sorter-cost: 1042 Base: 3 3 5 2 c ---[ 441]---> Sorter-cost: 704 Base: 5 2 3 3 11 c ---[ 440]---> BDD-cost: 173 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: 127 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: 136 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: 147 c ---[ 410]---> BDD-cost: 53 c ---[ 409]---> BDD-cost: 60 c ---[ 408]---> BDD-cost: 29 c ---[ 407]---> BDD-cost: 85 c ---[ 406]---> Sorter-cost: 795 Base: 5 2 3 3 c ---[ 405]---> Sorter-cost: 905 Base: 3 3 5 2 c ---[ 404]---> BDD-cost: 98 c ---[ 402]---> BDD-cost: 10 c ---[ 401]---> Sorter-cost: 715 Base: 5 3 3 2 11 c ---[ 400]---> BDD-cost: 17 c ---[ 399]---> BDD-cost: 14 c ---[ 397]---> Adder-cost: 1996 maxlim: 571 bits: 11/10 c ---[ 396]---> Adder-cost: 166 maxlim: 399 bits: 10/9 c ---[ 395]---> Adder-cost: 307 maxlim: 274 bits: 10/9 c ---[ 394]---> Adder-cost: 426 maxlim: 1316 bits: 11/11 c ---[ 393]---> Adder-cost: 540 maxlim: 1397 bits: 11/11 c ---[ 392]---> Adder-cost: 533 maxlim: 98 bits: 8/7 c ---[ 391]---> BDD-cost: 99 c ---[ 390]---> Adder-cost: 90 maxlim: 119 bits: 8/7 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: 3 c ---[ 358]---> BDD-cost: 5 c ---[ 356]---> BDD-cost: 5 c ---[ 353]---> BDD-cost: 5 c ---[ 351]---> BDD-cost: 5 c ---[ 350]---> BDD-cost: 3 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: 3 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: 3 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: 3 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: 3 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: 3 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: 3 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 | 237390 612897 | 79130 0 0 nan | 0.000 % | c | 100 | 237379 612875 | 87043 99 367 3.7 | 0.799 % | c | 250 | 237236 612535 | 95747 240 1225 5.1 | 0.844 % | c | 475 | 237096 612187 | 105322 460 2621 5.7 | 0.878 % | c | 812 | 237096 612187 | 115854 797 6724 8.4 | 0.878 % | c | 1318 | 237096 612187 | 127439 1303 12818 9.8 | 0.878 % | c | 2077 | 237081 612148 | 140183 2059 22538 10.9 | 0.880 % | c | 3216 | 236799 611484 | 154201 3184 35574 11.2 | 0.969 % | c | 4924 | 235594 608759 | 169622 4844 49962 10.3 | 1.372 % | c | 7487 | 234596 606489 | 186584 7357 92033 12.5 | 1.704 % | c | 11333 | 232744 602220 | 205242 11082 135288 12.2 | 2.319 % | c | 17102 | 231637 599741 | 225767 16752 244322 14.6 | 2.726 % | c | 25752 | 229307 594192 | 248343 25205 360963 14.3 | 3.518 % | c | 38727 | 227507 589976 | 273178 38022 638158 16.8 | 4.130 % | c | 58191 | 225375 585093 | 300496 57315 1073890 18.7 | 4.883 % | c ============================================================================== c [1mFound solution: 161145[0m c ---[ 0]---> Adder-cost: 11288 maxlim: 160686 bits: 19/18 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 69323 | 302657 863266 | 100885 62136 1145646 18.4 | 4.883 % | c | 69423 | 302496 862850 | 110973 62228 1146107 18.4 | 4.854 % | c | 69573 | 302466 862783 | 122070 62377 1148000 18.4 | 4.864 % | c | 69799 | 302395 862622 | 134277 62601 1153932 18.4 | 4.890 % | c | 70137 | 302313 862420 | 147705 62935 1157391 18.4 | 4.914 % | c | 70644 | 302276 862309 | 162476 63438 1163568 18.3 | 4.919 % | c | 71403 | 302233 862197 | 178723 64191 1181164 18.4 | 4.929 % | c | 72543 | 302148 862002 | 196596 65325 1204525 18.4 | 4.957 % | c | 74251 | 301787 861100 | 216255 66998 1226397 18.3 | 5.059 % | c | 76813 | 301467 860338 | 237881 69486 1266100 18.2 | 5.154 % | c | 80657 | 301078 859437 | 261669 73291 1323258 18.1 | 5.286 % | c | 86423 | 300245 857539 | 287836 78963 1407398 17.8 | 5.557 % | c | 95072 | 299431 855679 | 316620 87539 1530720 17.5 | 5.819 % | c | 108046 | 298522 853599 | 348282 100410 1721488 17.1 | 6.125 % | c | 127507 | 297913 852185 | 383110 119787 2002881 16.7 | 6.339 % | c | 156700 | 297077 850238 | 421421 148852 2553199 17.2 | 6.617 % | c | 200492 | 295501 846577 | 463563 192435 3291021 17.1 | 7.134 % | c | 266176 | 294050 843224 | 509920 257894 4303204 16.7 | 7.615 % | c ============================================================================== c [1mFound solution: 130062[0m c ---[ 0]---> Adder-cost: 0 maxlim: 191769 bits: 19/18 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 330156 | 292937 840118 | 97645 321670 5555461 17.3 | 7.615 % | c | 330256 | 292925 840090 | 107409 41345 378288 9.1 | 7.899 % | c | 330406 | 292871 839968 | 118150 41485 379643 9.2 | 7.916 % | c | 330633 | 292828 839868 | 129965 41706 381848 9.2 | 7.933 % | c | 330970 | 292828 839868 | 142962 42043 385758 9.2 | 7.933 % | c | 331477 | 292813 839831 | 157258 42549 391863 9.2 | 7.937 % | c | 332238 | 292813 839831 | 172984 43310 418112 9.7 | 7.937 % | c | 333380 | 292813 839831 | 190282 44452 436488 9.8 | 7.937 % | c | 335088 | 292673 839511 | 209310 46150 457177 9.9 | 7.987 % | c | 337650 | 292670 839502 | 230241 48711 505973 10.4 | 7.988 % | c | 341494 | 292498 839096 | 253265 52534 554707 10.6 | 8.043 % | 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 -C
Enforcing CPU limit (will send SIGTERM then SIGKILL): 1200 seconds Enforcing CPUTime (will send SIGXCPU) limit: 1230 seconds Enforcing Stack size limit: 67108864 bytes Enforcing memory limit (will send SIGTERM then SIGKILL): 921600 Kb Enforcing VSIZE limit: 994918400 bytes Current StackSize limit: 67108864 bytes Raw data (/proc/8513/stat): 8513 (minisat+_script) R 8512 8513 6872 0 -1 0 19 0 0 0 0 0 0 0 22 0 1 0 1797478189 712704 3 4294967295 134512640 135087896 3221224512 3221224512 1073744960 0 0 5 0 0 0 0 17 1 0 0 Raw data (/proc/8513/statm): 174 3 169 147 0 27 0 [pid=8513] vsize: 696 open syscall for file /etc/ld.so.preload open syscall for file tls/i686/mmx/libtermcap.so.2 open syscall for file tls/i686/libtermcap.so.2 open syscall for file tls/mmx/libtermcap.so.2 open syscall for file tls/libtermcap.so.2 open syscall for file i686/mmx/libtermcap.so.2 open syscall for file i686/libtermcap.so.2 open syscall for file mmx/libtermcap.so.2 open syscall for file libtermcap.so.2 open syscall for file /oldhome/oroussel/lib/tls/i686/mmx/libtermcap.so.2 open syscall for file /oldhome/oroussel/lib/tls/i686/libtermcap.so.2 open syscall for file /oldhome/oroussel/lib/tls/mmx/libtermcap.so.2 open syscall for file /oldhome/oroussel/lib/tls/libtermcap.so.2 open syscall for file /oldhome/oroussel/lib/i686/mmx/libtermcap.so.2 open syscall for file /oldhome/oroussel/lib/i686/libtermcap.so.2 open syscall for file /oldhome/oroussel/lib/mmx/libtermcap.so.2 open syscall for file /oldhome/oroussel/lib/libtermcap.so.2 open syscall for file /etc/ld.so.cache open syscall for file /lib/libtermcap.so.2 open syscall for file tls/i686/mmx/libdl.so.2 open syscall for file tls/i686/libdl.so.2 open syscall for file tls/mmx/libdl.so.2 open syscall for file tls/libdl.so.2 open syscall for file i686/mmx/libdl.so.2 open syscall for file i686/libdl.so.2 open syscall for file mmx/libdl.so.2 open syscall for file libdl.so.2 open syscall for file /oldhome/oroussel/lib/libdl.so.2 open syscall for file /lib/libdl.so.2 open syscall for file tls/i686/mmx/libc.so.6 open syscall for file tls/i686/libc.so.6 open syscall for file tls/mmx/libc.so.6 open syscall for file tls/libc.so.6 open syscall for file i686/mmx/libc.so.6 open syscall for file i686/libc.so.6 open syscall for file mmx/libc.so.6 open syscall for file libc.so.6 open syscall for file /oldhome/oroussel/lib/libc.so.6 open syscall for file /lib/tls/libc.so.6 open syscall for file /dev/tty open syscall for file /etc/mtab open syscall for file /proc/meminfo open syscall for file /oldhome/oroussel/solvers/minisat+_script New process pid=8514 New process pid=8515 New process pid=8516 execve syscall for /bin/sed executable One traced child (pid=8515) exited with status: 0 open syscall for file /etc/ld.so.preload open syscall for file tls/i686/mmx/libc.so.6 open syscall for file tls/i686/libc.so.6 open syscall for file tls/mmx/libc.so.6 open syscall for file tls/libc.so.6 open syscall for file i686/mmx/libc.so.6 open syscall for file i686/libc.so.6 open syscall for file mmx/libc.so.6 open syscall for file libc.so.6 open syscall for file /oldhome/oroussel/lib/tls/i686/mmx/libc.so.6 open syscall for file /oldhome/oroussel/lib/tls/i686/libc.so.6 open syscall for file /oldhome/oroussel/lib/tls/mmx/libc.so.6 open syscall for file /oldhome/oroussel/lib/tls/libc.so.6 open syscall for file /oldhome/oroussel/lib/i686/mmx/libc.so.6 open syscall for file /oldhome/oroussel/lib/i686/libc.so.6 open syscall for file /oldhome/oroussel/lib/mmx/libc.so.6 open syscall for file /oldhome/oroussel/lib/libc.so.6 open syscall for file /etc/ld.so.cache open syscall for file /lib/tls/libc.so.6 One traced child (pid=8516) exited with status: 0 One traced child (pid=8514) exited with status: 0 New process pid=8517 execve syscall for /oldhome/oroussel/solvers/minisat+_64-bit_static executable open syscall for file /dev/null open syscall for file /oldhome/oroussel/tmp/wulflinc2/normalized-mps-v2-13-7-p2756.opb [startup+10.0033 s] Raw data (loadavg): 0.93 0.95 0.91 2/57 8517 Raw data (/proc/8513/stat): 8513 (minisat+_script) S 8512 8513 6872 0 -1 0 289 239 0 0 0 0 0 1 18 0 1 0 1797478189 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/8513/statm): 531 226 485 147 0 384 0 [pid=8513] vsize: 2124 Raw data (/proc/8517/stat): 8517 (minisat+_64-bit) R 8513 8513 6872 0 -1 0 7451 0 0 0 937 28 0 0 25 0 1 0 1797478194 33300480 7101 4294967295 134512640 135094434 3221224448 3221223108 134553497 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/8517/statm): 8130 7101 145 145 0 7985 0 [pid=8517] vsize: 32520 Current children cumulated CPU time (s) 9.66 Current children cumulated vsize (Kb) 34644 [startup+20.004 s] Raw data (loadavg): 0.94 0.96 0.91 2/57 8517 Raw data (/proc/8513/stat): 8513 (minisat+_script) S 8512 8513 6872 0 -1 0 289 239 0 0 0 0 0 1 18 0 1 0 1797478189 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/8513/statm): 531 226 485 147 0 384 0 [pid=8513] vsize: 2124 Raw data (/proc/8517/stat): 8517 (minisat+_64-bit) R 8513 8513 6872 0 -1 0 7583 0 0 0 1935 29 0 0 25 0 1 0 1797478194 33767424 7233 4294967295 134512640 135094434 3221224448 3221223108 134553446 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/8517/statm): 8244 7233 145 145 0 8099 0 [pid=8517] vsize: 32976 Current children cumulated CPU time (s) 19.65 Current children cumulated vsize (Kb) 35100 [startup+30.0047 s] Raw data (loadavg): 0.95 0.96 0.91 2/57 8517 Raw data (/proc/8513/stat): 8513 (minisat+_script) S 8512 8513 6872 0 -1 0 289 239 0 0 0 0 0 1 18 0 1 0 1797478189 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/8513/statm): 531 226 485 147 0 384 0 [pid=8513] vsize: 2124 Raw data (/proc/8517/stat): 8517 (minisat+_64-bit) R 8513 8513 6872 0 -1 0 7671 0 0 0 2933 30 0 0 25 0 1 0 1797478194 34107392 7321 4294967295 134512640 135094434 3221224448 3221223072 134562104 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/8517/statm): 8327 7321 145 145 0 8182 0 [pid=8517] vsize: 33308 Current children cumulated CPU time (s) 29.64 Current children cumulated vsize (Kb) 35432 [startup+40.0054 s] Raw data (loadavg): 0.95 0.96 0.91 2/57 8517 Raw data (/proc/8513/stat): 8513 (minisat+_script) S 8512 8513 6872 0 -1 0 289 239 0 0 0 0 0 1 18 0 1 0 1797478189 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/8513/statm): 531 226 485 147 0 384 0 [pid=8513] vsize: 2124 Raw data (/proc/8517/stat): 8517 (minisat+_64-bit) R 8513 8513 6872 0 -1 0 7841 0 0 0 3930 32 0 0 25 0 1 0 1797478194 34762752 7491 4294967295 134512640 135094434 3221224448 3221223108 134553446 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/8517/statm): 8487 7491 145 145 0 8342 0 [pid=8517] vsize: 33948 Current children cumulated CPU time (s) 39.63 Current children cumulated vsize (Kb) 36072 [startup+50.0061 s] Raw data (loadavg): 0.96 0.96 0.91 2/57 8517 Raw data (/proc/8513/stat): 8513 (minisat+_script) S 8512 8513 6872 0 -1 0 289 239 0 0 0 0 0 1 18 0 1 0 1797478189 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/8513/statm): 531 226 485 147 0 384 0 [pid=8513] vsize: 2124 Raw data (/proc/8517/stat): 8517 (minisat+_64-bit) R 8513 8513 6872 0 -1 0 7963 0 0 0 4928 33 0 0 25 0 1 0 1797478194 35311616 7613 4294967295 134512640 135094434 3221224448 3221223108 134553530 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/8517/statm): 8621 7613 145 145 0 8476 0 [pid=8517] vsize: 34484 Current children cumulated CPU time (s) 49.62 Current children cumulated vsize (Kb) 36608 [startup+60.0058 s] Raw data (loadavg): 0.97 0.96 0.91 2/57 8517 Raw data (/proc/8513/stat): 8513 (minisat+_script) S 8512 8513 6872 0 -1 0 289 239 0 0 0 0 0 1 18 0 1 0 1797478189 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/8513/statm): 531 226 485 147 0 384 0 [pid=8513] vsize: 2124 Raw data (/proc/8517/stat): 8517 (minisat+_64-bit) T 8513 8513 6872 0 -1 0 8015 0 0 0 5927 33 0 0 25 0 1 0 1797478194 35512320 7665 4294967295 134512640 135094434 3221224448 3221222812 134870330 0 0 5 16386 3222434794 0 0 17 0 0 0 Raw data (/proc/8517/statm): 8670 7665 145 145 0 8525 0 [pid=8517] vsize: 34680 Current children cumulated CPU time (s) 59.61 Current children cumulated vsize (Kb) 36804 [startup+70.0075 s] Raw data (loadavg): 0.97 0.96 0.91 2/57 8517 Raw data (/proc/8513/stat): 8513 (minisat+_script) S 8512 8513 6872 0 -1 0 289 239 0 0 0 0 0 1 18 0 1 0 1797478189 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/8513/statm): 531 226 485 147 0 384 0 [pid=8513] vsize: 2124 Raw data (/proc/8517/stat): 8517 (minisat+_64-bit) R 8513 8513 6872 0 -1 0 8067 0 0 0 6926 34 0 0 25 0 1 0 1797478194 35717120 7717 4294967295 134512640 135094434 3221224448 3221223084 134562980 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/8517/statm): 8720 7717 145 145 0 8575 0 [pid=8517] vsize: 34880 Current children cumulated CPU time (s) 69.61 Current children cumulated vsize (Kb) 37004 [startup+80.0082 s] Raw data (loadavg): 0.98 0.96 0.91 2/57 8517 Raw data (/proc/8513/stat): 8513 (minisat+_script) S 8512 8513 6872 0 -1 0 289 239 0 0 0 0 0 1 18 0 1 0 1797478189 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/8513/statm): 531 226 485 147 0 384 0 [pid=8513] vsize: 2124 Raw data (/proc/8517/stat): 8517 (minisat+_64-bit) R 8513 8513 6872 0 -1 0 8157 0 0 0 7925 34 0 0 25 0 1 0 1797478194 36069376 7807 4294967295 134512640 135094434 3221224448 3221223108 134553446 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/8517/statm): 8806 7807 145 145 0 8661 0 [pid=8517] vsize: 35224 Current children cumulated CPU time (s) 79.6 Current children cumulated vsize (Kb) 37348 [startup+90.0089 s] Raw data (loadavg): 0.98 0.96 0.91 2/57 8517 Raw data (/proc/8513/stat): 8513 (minisat+_script) S 8512 8513 6872 0 -1 0 289 239 0 0 0 0 0 1 18 0 1 0 1797478189 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/8513/statm): 531 226 485 147 0 384 0 [pid=8513] vsize: 2124 Raw data (/proc/8517/stat): 8517 (minisat+_64-bit) R 8513 8513 6872 0 -1 0 8422 0 0 0 8922 36 0 0 25 0 1 0 1797478194 37257216 8072 4294967295 134512640 135094434 3221224448 3221223104 134557900 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/8517/statm): 9096 8072 145 145 0 8951 0 [pid=8517] vsize: 36384 Current children cumulated CPU time (s) 89.59 Current children cumulated vsize (Kb) 38508 [startup+100.01 s] Raw data (loadavg): 0.98 0.96 0.91 2/57 8517 Raw data (/proc/8513/stat): 8513 (minisat+_script) S 8512 8513 6872 0 -1 0 289 239 0 0 0 0 0 1 18 0 1 0 1797478189 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/8513/statm): 531 226 485 147 0 384 0 [pid=8513] vsize: 2124 Raw data (/proc/8517/stat): 8517 (minisat+_64-bit) R 8513 8513 6872 0 -1 0 8505 0 0 0 9920 36 0 0 25 0 1 0 1797478194 37584896 8155 4294967295 134512640 135094434 3221224448 3221223104 134557900 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/8517/statm): 9176 8155 145 145 0 9031 0 [pid=8517] vsize: 36704 Current children cumulated CPU time (s) 99.57 Current children cumulated vsize (Kb) 38828 [startup+110.01 s] Raw data (loadavg): 0.98 0.96 0.91 2/57 8517 Raw data (/proc/8513/stat): 8513 (minisat+_script) S 8512 8513 6872 0 -1 0 289 239 0 0 0 0 0 1 18 0 1 0 1797478189 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/8513/statm): 531 226 485 147 0 384 0 [pid=8513] vsize: 2124 Raw data (/proc/8517/stat): 8517 (minisat+_64-bit) R 8513 8513 6872 0 -1 0 8791 0 0 0 10916 37 0 0 25 0 1 0 1797478194 38748160 8441 4294967295 134512640 135094434 3221224448 3221223104 134557945 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/8517/statm): 9460 8441 145 145 0 9315 0 [pid=8517] vsize: 37840 Current children cumulated CPU time (s) 109.54 Current children cumulated vsize (Kb) 39964 [startup+120.011 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 8517 Raw data (/proc/8513/stat): 8513 (minisat+_script) S 8512 8513 6872 0 -1 0 289 239 0 0 0 0 0 1 18 0 1 0 1797478189 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/8513/statm): 531 226 485 147 0 384 0 [pid=8513] vsize: 2124 Raw data (/proc/8517/stat): 8517 (minisat+_64-bit) R 8513 8513 6872 0 -1 0 8874 0 0 0 11915 38 0 0 25 0 1 0 1797478194 39079936 8524 4294967295 134512640 135094434 3221224448 3221223108 134553446 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/8517/statm): 9541 8524 145 145 0 9396 0 [pid=8517] vsize: 38164 Current children cumulated CPU time (s) 119.54 Current children cumulated vsize (Kb) 40288 [startup+130.012 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 8517 Raw data (/proc/8513/stat): 8513 (minisat+_script) S 8512 8513 6872 0 -1 0 289 239 0 0 0 0 0 1 18 0 1 0 1797478189 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/8513/statm): 531 226 485 147 0 384 0 [pid=8513] vsize: 2124 Raw data (/proc/8517/stat): 8517 (minisat+_64-bit) R 8513 8513 6872 0 -1 0 8988 0 0 0 12913 39 0 0 25 0 1 0 1797478194 39538688 8638 4294967295 134512640 135094434 3221224448 3221223088 134562104 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/8517/statm): 9653 8638 145 145 0 9508 0 [pid=8517] vsize: 38612 Current children cumulated CPU time (s) 129.53 Current children cumulated vsize (Kb) 40736 [startup+140.012 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 8517 Raw data (/proc/8513/stat): 8513 (minisat+_script) S 8512 8513 6872 0 -1 0 289 239 0 0 0 0 0 1 18 0 1 0 1797478189 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/8513/statm): 531 226 485 147 0 384 0 [pid=8513] vsize: 2124 Raw data (/proc/8517/stat): 8517 (minisat+_64-bit) R 8513 8513 6872 0 -1 0 9118 0 0 0 13911 40 0 0 25 0 1 0 1797478194 40050688 8768 4294967295 134512640 135094434 3221224448 3221223088 134562057 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/8517/statm): 9778 8768 145 145 0 9633 0 [pid=8517] vsize: 39112 Current children cumulated CPU time (s) 139.52 Current children cumulated vsize (Kb) 41236 [startup+150.013 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 8517 Raw data (/proc/8513/stat): 8513 (minisat+_script) S 8512 8513 6872 0 -1 0 289 239 0 0 0 0 0 1 18 0 1 0 1797478189 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/8513/statm): 531 226 485 147 0 384 0 [pid=8513] vsize: 2124 Raw data (/proc/8517/stat): 8517 (minisat+_64-bit) R 8513 8513 6872 0 -1 0 9217 0 0 0 14909 41 0 0 25 0 1 0 1797478194 40468480 8867 4294967295 134512640 135094434 3221224448 3221223104 134557792 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/8517/statm): 9880 8867 145 145 0 9735 0 [pid=8517] vsize: 39520 Current children cumulated CPU time (s) 149.51 Current children cumulated vsize (Kb) 41644 [startup+160.014 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 8517 Raw data (/proc/8513/stat): 8513 (minisat+_script) S 8512 8513 6872 0 -1 0 289 239 0 0 0 0 0 1 18 0 1 0 1797478189 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/8513/statm): 531 226 485 147 0 384 0 [pid=8513] vsize: 2124 Raw data (/proc/8517/stat): 8517 (minisat+_64-bit) R 8513 8513 6872 0 -1 0 9220 0 0 0 15909 41 0 0 25 0 1 0 1797478194 40476672 8870 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/8517/statm): 9882 8870 145 145 0 9737 0 [pid=8517] vsize: 39528 Current children cumulated CPU time (s) 159.51 Current children cumulated vsize (Kb) 41652 [startup+170.014 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 8517 Raw data (/proc/8513/stat): 8513 (minisat+_script) S 8512 8513 6872 0 -1 0 289 239 0 0 0 0 0 1 18 0 1 0 1797478189 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/8513/statm): 531 226 485 147 0 384 0 [pid=8513] vsize: 2124 Raw data (/proc/8517/stat): 8517 (minisat+_64-bit) R 8513 8513 6872 0 -1 0 9238 0 0 0 16909 42 0 0 25 0 1 0 1797478194 40542208 8888 4294967295 134512640 135094434 3221224448 3221223060 134563080 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/8517/statm): 9898 8888 145 145 0 9753 0 [pid=8517] vsize: 39592 Current children cumulated CPU time (s) 169.52 Current children cumulated vsize (Kb) 41716 [startup+180.014 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 8517 Raw data (/proc/8513/stat): 8513 (minisat+_script) S 8512 8513 6872 0 -1 0 289 239 0 0 0 0 0 1 18 0 1 0 1797478189 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/8513/statm): 531 226 485 147 0 384 0 [pid=8513] vsize: 2124 Raw data (/proc/8517/stat): 8517 (minisat+_64-bit) R 8513 8513 6872 0 -1 0 16263 0 0 0 17864 67 0 0 25 0 1 0 1797478194 70459392 14861 4294967295 134512640 135094434 3221224448 3221223108 134553482 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/8517/statm): 17202 14861 145 145 0 17057 0 [pid=8517] vsize: 68808 Current children cumulated CPU time (s) 179.32 Current children cumulated vsize (Kb) 70932 [startup+190.016 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 8517 Raw data (/proc/8513/stat): 8513 (minisat+_script) S 8512 8513 6872 0 -1 0 289 239 0 0 0 0 0 1 18 0 1 0 1797478189 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/8513/statm): 531 226 485 147 0 384 0 [pid=8513] vsize: 2124 Raw data (/proc/8517/stat): 8517 (minisat+_64-bit) R 8513 8513 6872 0 -1 0 16359 0 0 0 18863 68 0 0 25 0 1 0 1797478194 71102464 14957 4294967295 134512640 135094434 3221224448 3221223108 134553446 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/8517/statm): 17359 14957 145 145 0 17214 0 [pid=8517] vsize: 69436 Current children cumulated CPU time (s) 189.32 Current children cumulated vsize (Kb) 71560 [startup+200.017 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 8517 Raw data (/proc/8513/stat): 8513 (minisat+_script) S 8512 8513 6872 0 -1 0 289 239 0 0 0 0 0 1 18 0 1 0 1797478189 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/8513/statm): 531 226 485 147 0 384 0 [pid=8513] vsize: 2124 Raw data (/proc/8517/stat): 8517 (minisat+_64-bit) R 8513 8513 6872 0 -1 0 16406 0 0 0 19862 68 0 0 25 0 1 0 1797478194 71286784 15004 4294967295 134512640 135094434 3221224448 3221223060 134563069 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/8517/statm): 17404 15004 145 145 0 17259 0 [pid=8517] vsize: 69616 Current children cumulated CPU time (s) 199.31 Current children cumulated vsize (Kb) 71740 [startup+210.016 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 8517 Raw data (/proc/8513/stat): 8513 (minisat+_script) S 8512 8513 6872 0 -1 0 289 239 0 0 0 0 0 1 18 0 1 0 1797478189 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/8513/statm): 531 226 485 147 0 384 0 [pid=8513] vsize: 2124 Raw data (/proc/8517/stat): 8517 (minisat+_64-bit) R 8513 8513 6872 0 -1 0 16513 0 0 0 20861 69 0 0 25 0 1 0 1797478194 71704576 15111 4294967295 134512640 135094434 3221224448 3221223108 134553446 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/8517/statm): 17506 15111 145 145 0 17361 0 [pid=8517] vsize: 70024 Current children cumulated CPU time (s) 209.31 Current children cumulated vsize (Kb) 72148 [startup+220.017 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 8517 Raw data (/proc/8513/stat): 8513 (minisat+_script) S 8512 8513 6872 0 -1 0 289 239 0 0 0 0 0 1 18 0 1 0 1797478189 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/8513/statm): 531 226 485 147 0 384 0 [pid=8513] vsize: 2124 Raw data (/proc/8517/stat): 8517 (minisat+_64-bit) R 8513 8513 6872 0 -1 0 16568 0 0 0 21860 69 0 0 25 0 1 0 1797478194 71913472 15166 4294967295 134512640 135094434 3221224448 3221223072 134557714 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/8517/statm): 17557 15166 145 145 0 17412 0 [pid=8517] vsize: 70228 Current children cumulated CPU time (s) 219.3 Current children cumulated vsize (Kb) 72352 [startup+230.018 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 8517 Raw data (/proc/8513/stat): 8513 (minisat+_script) S 8512 8513 6872 0 -1 0 289 239 0 0 0 0 0 1 18 0 1 0 1797478189 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/8513/statm): 531 226 485 147 0 384 0 [pid=8513] vsize: 2124 Raw data (/proc/8517/stat): 8517 (minisat+_64-bit) R 8513 8513 6872 0 -1 0 16606 0 0 0 22859 69 0 0 25 0 1 0 1797478194 72065024 15204 4294967295 134512640 135094434 3221224448 3221223088 134562068 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/8517/statm): 17594 15204 145 145 0 17449 0 [pid=8517] vsize: 70376 Current children cumulated CPU time (s) 229.29 Current children cumulated vsize (Kb) 72500 [startup+240.018 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 8517 Raw data (/proc/8513/stat): 8513 (minisat+_script) S 8512 8513 6872 0 -1 0 289 239 0 0 0 0 0 1 18 0 1 0 1797478189 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/8513/statm): 531 226 485 147 0 384 0 [pid=8513] vsize: 2124 Raw data (/proc/8517/stat): 8517 (minisat+_64-bit) R 8513 8513 6872 0 -1 0 16671 0 0 0 23859 70 0 0 25 0 1 0 1797478194 72323072 15269 4294967295 134512640 135094434 3221224448 3221223108 134553530 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/8517/statm): 17657 15269 145 145 0 17512 0 [pid=8517] vsize: 70628 Current children cumulated CPU time (s) 239.3 Current children cumulated vsize (Kb) 72752 [startup+250.019 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 8517 Raw data (/proc/8513/stat): 8513 (minisat+_script) S 8512 8513 6872 0 -1 0 289 239 0 0 0 0 0 1 18 0 1 0 1797478189 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/8513/statm): 531 226 485 147 0 384 0 [pid=8513] vsize: 2124 Raw data (/proc/8517/stat): 8517 (minisat+_64-bit) R 8513 8513 6872 0 -1 0 16710 0 0 0 24858 70 0 0 25 0 1 0 1797478194 72474624 15308 4294967295 134512640 135094434 3221224448 3221223136 134554746 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/8517/statm): 17694 15308 145 145 0 17549 0 [pid=8517] vsize: 70776 Current children cumulated CPU time (s) 249.29 Current children cumulated vsize (Kb) 72900 [startup+260.019 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 8517 Raw data (/proc/8513/stat): 8513 (minisat+_script) S 8512 8513 6872 0 -1 0 289 239 0 0 0 0 0 1 18 0 1 0 1797478189 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/8513/statm): 531 226 485 147 0 384 0 [pid=8513] vsize: 2124 Raw data (/proc/8517/stat): 8517 (minisat+_64-bit) R 8513 8513 6872 0 -1 0 16774 0 0 0 25856 71 0 0 25 0 1 0 1797478194 72728576 15372 4294967295 134512640 135094434 3221224448 3221223108 134553497 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/8517/statm): 17756 15372 145 145 0 17611 0 [pid=8517] vsize: 71024 Current children cumulated CPU time (s) 259.28 Current children cumulated vsize (Kb) 73148 [startup+270.019 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 8517 Raw data (/proc/8513/stat): 8513 (minisat+_script) S 8512 8513 6872 0 -1 0 289 239 0 0 0 0 0 1 18 0 1 0 1797478189 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/8513/statm): 531 226 485 147 0 384 0 [pid=8513] vsize: 2124 Raw data (/proc/8517/stat): 8517 (minisat+_64-bit) R 8513 8513 6872 0 -1 0 16817 0 0 0 26856 71 0 0 25 0 1 0 1797478194 72900608 15415 4294967295 134512640 135094434 3221224448 3221223104 134557964 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/8517/statm): 17798 15415 145 145 0 17653 0 [pid=8517] vsize: 71192 Current children cumulated CPU time (s) 269.28 Current children cumulated vsize (Kb) 73316 [startup+280.02 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 8517 Raw data (/proc/8513/stat): 8513 (minisat+_script) S 8512 8513 6872 0 -1 0 289 239 0 0 0 0 0 1 18 0 1 0 1797478189 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/8513/statm): 531 226 485 147 0 384 0 [pid=8513] vsize: 2124 Raw data (/proc/8517/stat): 8517 (minisat+_64-bit) R 8513 8513 6872 0 -1 0 16883 0 0 0 27855 72 0 0 25 0 1 0 1797478194 73158656 15481 4294967295 134512640 135094434 3221224448 3221223108 134553446 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/8517/statm): 17861 15481 145 145 0 17716 0 [pid=8517] vsize: 71444 Current children cumulated CPU time (s) 279.28 Current children cumulated vsize (Kb) 73568 [startup+290.021 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 8517 Raw data (/proc/8513/stat): 8513 (minisat+_script) S 8512 8513 6872 0 -1 0 289 239 0 0 0 0 0 1 18 0 1 0 1797478189 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/8513/statm): 531 226 485 147 0 384 0 [pid=8513] vsize: 2124 Raw data (/proc/8517/stat): 8517 (minisat+_64-bit) R 8513 8513 6872 0 -1 0 16934 0 0 0 28854 72 0 0 25 0 1 0 1797478194 73359360 15532 4294967295 134512640 135094434 3221224448 3221223060 134563049 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/8517/statm): 17910 15532 145 145 0 17765 0 [pid=8517] vsize: 71640 Current children cumulated CPU time (s) 289.27 Current children cumulated vsize (Kb) 73764 [startup+300.022 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 8517 Raw data (/proc/8513/stat): 8513 (minisat+_script) S 8512 8513 6872 0 -1 0 289 239 0 0 0 0 0 1 18 0 1 0 1797478189 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/8513/statm): 531 226 485 147 0 384 0 [pid=8513] vsize: 2124 Raw data (/proc/8517/stat): 8517 (minisat+_64-bit) R 8513 8513 6872 0 -1 0 17005 0 0 0 29854 73 0 0 25 0 1 0 1797478194 73641984 15603 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/8517/statm): 17979 15603 145 145 0 17834 0 [pid=8517] vsize: 71916 Current children cumulated CPU time (s) 299.28 Current children cumulated vsize (Kb) 74040 [startup+310.022 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 8517 Raw data (/proc/8513/stat): 8513 (minisat+_script) S 8512 8513 6872 0 -1 0 289 239 0 0 0 0 0 1 18 0 1 0 1797478189 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/8513/statm): 531 226 485 147 0 384 0 [pid=8513] vsize: 2124 Raw data (/proc/8517/stat): 8517 (minisat+_64-bit) R 8513 8513 6872 0 -1 0 17059 0 0 0 30853 73 0 0 25 0 1 0 1797478194 73850880 15657 4294967295 134512640 135094434 3221224448 3221223108 134553536 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/8517/statm): 18030 15657 145 145 0 17885 0 [pid=8517] vsize: 72120 Current children cumulated CPU time (s) 309.27 Current children cumulated vsize (Kb) 74244 [startup+320.023 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 8517 Raw data (/proc/8513/stat): 8513 (minisat+_script) S 8512 8513 6872 0 -1 0 289 239 0 0 0 0 0 1 18 0 1 0 1797478189 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/8513/statm): 531 226 485 147 0 384 0 [pid=8513] vsize: 2124 Raw data (/proc/8517/stat): 8517 (minisat+_64-bit) R 8513 8513 6872 0 -1 0 17099 0 0 0 31852 73 0 0 25 0 1 0 1797478194 74010624 15697 4294967295 134512640 135094434 3221224448 3221223060 134563046 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/8517/statm): 18069 15697 145 145 0 17924 0 [pid=8517] vsize: 72276 Current children cumulated CPU time (s) 319.26 Current children cumulated vsize (Kb) 74400 [startup+330.023 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 8517 Raw data (/proc/8513/stat): 8513 (minisat+_script) S 8512 8513 6872 0 -1 0 289 239 0 0 0 0 0 1 18 0 1 0 1797478189 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/8513/statm): 531 226 485 147 0 384 0 [pid=8513] vsize: 2124 Raw data (/proc/8517/stat): 8517 (minisat+_64-bit) R 8513 8513 6872 0 -1 0 17163 0 0 0 32851 74 0 0 25 0 1 0 1797478194 74264576 15761 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/8517/statm): 18131 15761 145 145 0 17986 0 [pid=8517] vsize: 72524 Current children cumulated CPU time (s) 329.26 Current children cumulated vsize (Kb) 74648 [startup+340.023 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 8517 Raw data (/proc/8513/stat): 8513 (minisat+_script) S 8512 8513 6872 0 -1 0 289 239 0 0 0 0 0 1 18 0 1 0 1797478189 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/8513/statm): 531 226 485 147 0 384 0 [pid=8513] vsize: 2124 Raw data (/proc/8517/stat): 8517 (minisat+_64-bit) R 8513 8513 6872 0 -1 0 17219 0 0 0 33851 74 0 0 25 0 1 0 1797478194 74481664 15817 4294967295 134512640 135094434 3221224448 3221223072 134557717 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/8517/statm): 18184 15817 145 145 0 18039 0 [pid=8517] vsize: 72736 Current children cumulated CPU time (s) 339.26 Current children cumulated vsize (Kb) 74860 [startup+350.024 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 8517 Raw data (/proc/8513/stat): 8513 (minisat+_script) S 8512 8513 6872 0 -1 0 289 239 0 0 0 0 0 1 18 0 1 0 1797478189 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/8513/statm): 531 226 485 147 0 384 0 [pid=8513] vsize: 2124 Raw data (/proc/8517/stat): 8517 (minisat+_64-bit) R 8513 8513 6872 0 -1 0 17279 0 0 0 34850 75 0 0 25 0 1 0 1797478194 74719232 15877 4294967295 134512640 135094434 3221224448 3221223104 134557948 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/8517/statm): 18242 15877 145 145 0 18097 0 [pid=8517] vsize: 72968 Current children cumulated CPU time (s) 349.26 Current children cumulated vsize (Kb) 75092 [startup+360.024 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 8517 Raw data (/proc/8513/stat): 8513 (minisat+_script) S 8512 8513 6872 0 -1 0 289 239 0 0 0 0 0 1 18 0 1 0 1797478189 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/8513/statm): 531 226 485 147 0 384 0 [pid=8513] vsize: 2124 Raw data (/proc/8517/stat): 8517 (minisat+_64-bit) R 8513 8513 6872 0 -1 0 17321 0 0 0 35849 75 0 0 25 0 1 0 1797478194 74883072 15919 4294967295 134512640 135094434 3221224448 3221223136 134554746 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/8517/statm): 18282 15919 145 145 0 18137 0 [pid=8517] vsize: 73128 Current children cumulated CPU time (s) 359.25 Current children cumulated vsize (Kb) 75252 [startup+370.024 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 8517 Raw data (/proc/8513/stat): 8513 (minisat+_script) S 8512 8513 6872 0 -1 0 289 239 0 0 0 0 0 1 18 0 1 0 1797478189 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/8513/statm): 531 226 485 147 0 384 0 [pid=8513] vsize: 2124 Raw data (/proc/8517/stat): 8517 (minisat+_64-bit) R 8513 8513 6872 0 -1 0 17382 0 0 0 36848 76 0 0 25 0 1 0 1797478194 75120640 15980 4294967295 134512640 135094434 3221224448 3221223104 134557903 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/8517/statm): 18340 15980 145 145 0 18195 0 [pid=8517] vsize: 73360 Current children cumulated CPU time (s) 369.25 Current children cumulated vsize (Kb) 75484 [startup+380.024 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 8517 Raw data (/proc/8513/stat): 8513 (minisat+_script) S 8512 8513 6872 0 -1 0 289 239 0 0 0 0 0 1 18 0 1 0 1797478189 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/8513/statm): 531 226 485 147 0 384 0 [pid=8513] vsize: 2124 Raw data (/proc/8517/stat): 8517 (minisat+_64-bit) R 8513 8513 6872 0 -1 0 17477 0 0 0 37846 77 0 0 25 0 1 0 1797478194 75497472 16075 4294967295 134512640 135094434 3221224448 3221223108 134553482 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/8517/statm): 18432 16075 145 145 0 18287 0 [pid=8517] vsize: 73728 Current children cumulated CPU time (s) 379.24 Current children cumulated vsize (Kb) 75852 [startup+390.025 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 8517 Raw data (/proc/8513/stat): 8513 (minisat+_script) S 8512 8513 6872 0 -1 0 289 239 0 0 0 0 0 1 18 0 1 0 1797478189 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/8513/statm): 531 226 485 147 0 384 0 [pid=8513] vsize: 2124 Raw data (/proc/8517/stat): 8517 (minisat+_64-bit) R 8513 8513 6872 0 -1 0 17542 0 0 0 38844 77 0 0 25 0 1 0 1797478194 75751424 16140 4294967295 134512640 135094434 3221224448 3221223136 134554746 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/8517/statm): 18494 16140 145 145 0 18349 0 [pid=8517] vsize: 73976 Current children cumulated CPU time (s) 389.22 Current children cumulated vsize (Kb) 76100 [startup+400.026 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 8517 Raw data (/proc/8513/stat): 8513 (minisat+_script) S 8512 8513 6872 0 -1 0 289 239 0 0 0 0 0 1 18 0 1 0 1797478189 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/8513/statm): 531 226 485 147 0 384 0 [pid=8513] vsize: 2124 Raw data (/proc/8517/stat): 8517 (minisat+_64-bit) R 8513 8513 6872 0 -1 0 17593 0 0 0 39843 78 0 0 25 0 1 0 1797478194 75948032 16191 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/8517/statm): 18542 16191 145 145 0 18397 0 [pid=8517] vsize: 74168 Current children cumulated CPU time (s) 399.22 Current children cumulated vsize (Kb) 76292 [startup+410.026 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 8517 Raw data (/proc/8513/stat): 8513 (minisat+_script) S 8512 8513 6872 0 -1 0 289 239 0 0 0 0 0 1 18 0 1 0 1797478189 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/8513/statm): 531 226 485 147 0 384 0 [pid=8513] vsize: 2124 Raw data (/proc/8517/stat): 8517 (minisat+_64-bit) R 8513 8513 6872 0 -1 0 17652 0 0 0 40842 79 0 0 25 0 1 0 1797478194 76181504 16250 4294967295 134512640 135094434 3221224448 3221223120 134553523 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/8517/statm): 18599 16250 145 145 0 18454 0 [pid=8517] vsize: 74396 Current children cumulated CPU time (s) 409.22 Current children cumulated vsize (Kb) 76520 [startup+420.027 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 8517 Raw data (/proc/8513/stat): 8513 (minisat+_script) S 8512 8513 6872 0 -1 0 289 239 0 0 0 0 0 1 18 0 1 0 1797478189 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/8513/statm): 531 226 485 147 0 384 0 [pid=8513] vsize: 2124 Raw data (/proc/8517/stat): 8517 (minisat+_64-bit) R 8513 8513 6872 0 -1 0 17687 0 0 0 41840 79 0 0 25 0 1 0 1797478194 76316672 16285 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/8517/statm): 18632 16285 145 145 0 18487 0 [pid=8517] vsize: 74528 Current children cumulated CPU time (s) 419.2 Current children cumulated vsize (Kb) 76652 [startup+430.028 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 8517 Raw data (/proc/8513/stat): 8513 (minisat+_script) S 8512 8513 6872 0 -1 0 289 239 0 0 0 0 0 1 18 0 1 0 1797478189 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/8513/statm): 531 226 485 147 0 384 0 [pid=8513] vsize: 2124 Raw data (/proc/8517/stat): 8517 (minisat+_64-bit) R 8513 8513 6872 0 -1 0 17758 0 0 0 42839 80 0 0 25 0 1 0 1797478194 76595200 16356 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/8517/statm): 18700 16356 145 145 0 18555 0 [pid=8517] vsize: 74800 Current children cumulated CPU time (s) 429.2 Current children cumulated vsize (Kb) 76924 [startup+440.028 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 8517 Raw data (/proc/8513/stat): 8513 (minisat+_script) S 8512 8513 6872 0 -1 0 289 239 0 0 0 0 0 1 18 0 1 0 1797478189 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/8513/statm): 531 226 485 147 0 384 0 [pid=8513] vsize: 2124 Raw data (/proc/8517/stat): 8517 (minisat+_64-bit) R 8513 8513 6872 0 -1 0 17995 0 0 0 43835 81 0 0 25 0 1 0 1797478194 77561856 16593 4294967295 134512640 135094434 3221224448 3221223120 134554891 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/8517/statm): 18936 16593 145 145 0 18791 0 [pid=8517] vsize: 75744 Current children cumulated CPU time (s) 439.17 Current children cumulated vsize (Kb) 77868 [startup+450.029 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 8517 Raw data (/proc/8513/stat): 8513 (minisat+_script) S 8512 8513 6872 0 -1 0 289 239 0 0 0 0 0 1 18 0 1 0 1797478189 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/8513/statm): 531 226 485 147 0 384 0 [pid=8513] vsize: 2124 Raw data (/proc/8517/stat): 8517 (minisat+_64-bit) R 8513 8513 6872 0 -1 0 18047 0 0 0 44834 82 0 0 25 0 1 0 1797478194 78290944 16645 4294967295 134512640 135094434 3221224448 3221223072 134557642 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/8517/statm): 19114 16645 145 145 0 18969 0 [pid=8517] vsize: 76456 Current children cumulated CPU time (s) 449.17 Current children cumulated vsize (Kb) 78580 [startup+460.03 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 8517 Raw data (/proc/8513/stat): 8513 (minisat+_script) S 8512 8513 6872 0 -1 0 289 239 0 0 0 0 0 1 18 0 1 0 1797478189 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/8513/statm): 531 226 485 147 0 384 0 [pid=8513] vsize: 2124 Raw data (/proc/8517/stat): 8517 (minisat+_64-bit) R 8513 8513 6872 0 -1 0 18087 0 0 0 45833 83 0 0 25 0 1 0 1797478194 78450688 16685 4294967295 134512640 135094434 3221224448 3221223060 134563046 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/8517/statm): 19153 16685 145 145 0 19008 0 [pid=8517] vsize: 76612 Current children cumulated CPU time (s) 459.17 Current children cumulated vsize (Kb) 78736 [startup+470.03 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 8517 Raw data (/proc/8513/stat): 8513 (minisat+_script) S 8512 8513 6872 0 -1 0 289 239 0 0 0 0 0 1 18 0 1 0 1797478189 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/8513/statm): 531 226 485 147 0 384 0 [pid=8513] vsize: 2124 Raw data (/proc/8517/stat): 8517 (minisat+_64-bit) R 8513 8513 6872 0 -1 0 18185 0 0 0 46831 84 0 0 25 0 1 0 1797478194 78839808 16783 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/8517/statm): 19248 16783 145 145 0 19103 0 [pid=8517] vsize: 76992 Current children cumulated CPU time (s) 469.16 Current children cumulated vsize (Kb) 79116 [startup+480.031 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 8517 Raw data (/proc/8513/stat): 8513 (minisat+_script) S 8512 8513 6872 0 -1 0 289 239 0 0 0 0 0 1 18 0 1 0 1797478189 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/8513/statm): 531 226 485 147 0 384 0 [pid=8513] vsize: 2124 Raw data (/proc/8517/stat): 8517 (minisat+_64-bit) R 8513 8513 6872 0 -1 0 18255 0 0 0 47830 84 0 0 25 0 1 0 1797478194 79114240 16853 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/8517/statm): 19315 16853 145 145 0 19170 0 [pid=8517] vsize: 77260 Current children cumulated CPU time (s) 479.15 Current children cumulated vsize (Kb) 79384 [startup+490.033 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 8517 Raw data (/proc/8513/stat): 8513 (minisat+_script) S 8512 8513 6872 0 -1 0 289 239 0 0 0 0 0 1 18 0 1 0 1797478189 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/8513/statm): 531 226 485 147 0 384 0 [pid=8513] vsize: 2124 Raw data (/proc/8517/stat): 8517 (minisat+_64-bit) R 8513 8513 6872 0 -1 0 18316 0 0 0 48829 85 0 0 25 0 1 0 1797478194 79355904 16914 4294967295 134512640 135094434 3221224448 3221223140 134558984 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/8517/statm): 19374 16914 145 145 0 19229 0 [pid=8517] vsize: 77496 Current children cumulated CPU time (s) 489.15 Current children cumulated vsize (Kb) 79620 [startup+500.034 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 8517 Raw data (/proc/8513/stat): 8513 (minisat+_script) S 8512 8513 6872 0 -1 0 289 239 0 0 0 0 0 1 18 0 1 0 1797478189 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/8513/statm): 531 226 485 147 0 384 0 [pid=8513] vsize: 2124 Raw data (/proc/8517/stat): 8517 (minisat+_64-bit) R 8513 8513 6872 0 -1 0 18378 0 0 0 49829 85 0 0 25 0 1 0 1797478194 79597568 16976 4294967295 134512640 135094434 3221224448 3221223136 134554746 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/8517/statm): 19433 16976 145 145 0 19288 0 [pid=8517] vsize: 77732 Current children cumulated CPU time (s) 499.15 Current children cumulated vsize (Kb) 79856 [startup+510.034 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 8517 Raw data (/proc/8513/stat): 8513 (minisat+_script) S 8512 8513 6872 0 -1 0 289 239 0 0 0 0 0 1 18 0 1 0 1797478189 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/8513/statm): 531 226 485 147 0 384 0 [pid=8513] vsize: 2124 Raw data (/proc/8517/stat): 8517 (minisat+_64-bit) R 8513 8513 6872 0 -1 0 18456 0 0 0 50827 86 0 0 25 0 1 0 1797478194 79904768 17054 4294967295 134512640 135094434 3221224448 3221223060 134563083 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/8517/statm): 19508 17054 145 145 0 19363 0 [pid=8517] vsize: 78032 Current children cumulated CPU time (s) 509.14 Current children cumulated vsize (Kb) 80156 [startup+520.035 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 8517 Raw data (/proc/8513/stat): 8513 (minisat+_script) S 8512 8513 6872 0 -1 0 289 239 0 0 0 0 0 1 18 0 1 0 1797478189 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/8513/statm): 531 226 485 147 0 384 0 [pid=8513] vsize: 2124 Raw data (/proc/8517/stat): 8517 (minisat+_64-bit) R 8513 8513 6872 0 -1 0 18512 0 0 0 51826 87 0 0 25 0 1 0 1797478194 80125952 17110 4294967295 134512640 135094434 3221224448 3221223104 134557875 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/8517/statm): 19562 17110 145 145 0 19417 0 [pid=8517] vsize: 78248 Current children cumulated CPU time (s) 519.14 Current children cumulated vsize (Kb) 80372 [startup+530.036 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 8517 Raw data (/proc/8513/stat): 8513 (minisat+_script) S 8512 8513 6872 0 -1 0 289 239 0 0 0 0 0 1 18 0 1 0 1797478189 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/8513/statm): 531 226 485 147 0 384 0 [pid=8513] vsize: 2124 Raw data (/proc/8517/stat): 8517 (minisat+_64-bit) R 8513 8513 6872 0 -1 0 18565 0 0 0 52825 87 0 0 25 0 1 0 1797478194 80334848 17163 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/8517/statm): 19613 17163 145 145 0 19468 0 [pid=8517] vsize: 78452 Current children cumulated CPU time (s) 529.13 Current children cumulated vsize (Kb) 80576 [startup+540.036 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 8517 Raw data (/proc/8513/stat): 8513 (minisat+_script) S 8512 8513 6872 0 -1 0 289 239 0 0 0 0 0 1 18 0 1 0 1797478189 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/8513/statm): 531 226 485 147 0 384 0 [pid=8513] vsize: 2124 Raw data (/proc/8517/stat): 8517 (minisat+_64-bit) R 8513 8513 6872 0 -1 0 18627 0 0 0 53824 88 0 0 25 0 1 0 1797478194 80576512 17225 4294967295 134512640 135094434 3221224448 3221223104 134558235 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/8517/statm): 19672 17225 145 145 0 19527 0 [pid=8517] vsize: 78688 Current children cumulated CPU time (s) 539.13 Current children cumulated vsize (Kb) 80812 [startup+550.037 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 8517 Raw data (/proc/8513/stat): 8513 (minisat+_script) S 8512 8513 6872 0 -1 0 289 239 0 0 0 0 0 1 18 0 1 0 1797478189 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/8513/statm): 531 226 485 147 0 384 0 [pid=8513] vsize: 2124 Raw data (/proc/8517/stat): 8517 (minisat+_64-bit) R 8513 8513 6872 0 -1 0 18697 0 0 0 54823 89 0 0 25 0 1 0 1797478194 80855040 17295 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/8517/statm): 19740 17295 145 145 0 19595 0 [pid=8517] vsize: 78960 Current children cumulated CPU time (s) 549.13 Current children cumulated vsize (Kb) 81084 [startup+560.038 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 8517 Raw data (/proc/8513/stat): 8513 (minisat+_script) S 8512 8513 6872 0 -1 0 289 239 0 0 0 0 0 1 18 0 1 0 1797478189 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/8513/statm): 531 226 485 147 0 384 0 [pid=8513] vsize: 2124 Raw data (/proc/8517/stat): 8517 (minisat+_64-bit) R 8513 8513 6872 0 -1 0 18740 0 0 0 55822 89 0 0 25 0 1 0 1797478194 81018880 17338 4294967295 134512640 135094434 3221224448 3221223076 134557564 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/8517/statm): 19780 17338 145 145 0 19635 0 [pid=8517] vsize: 79120 Current children cumulated CPU time (s) 559.12 Current children cumulated vsize (Kb) 81244 [startup+570.038 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 8517 Raw data (/proc/8513/stat): 8513 (minisat+_script) S 8512 8513 6872 0 -1 0 289 239 0 0 0 0 0 1 18 0 1 0 1797478189 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/8513/statm): 531 226 485 147 0 384 0 [pid=8513] vsize: 2124 Raw data (/proc/8517/stat): 8517 (minisat+_64-bit) R 8513 8513 6872 0 -1 0 18789 0 0 0 56821 90 0 0 25 0 1 0 1797478194 81207296 17387 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/8517/statm): 19826 17387 145 145 0 19681 0 [pid=8517] vsize: 79304 Current children cumulated CPU time (s) 569.12 Current children cumulated vsize (Kb) 81428 [startup+580.039 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 8517 Raw data (/proc/8513/stat): 8513 (minisat+_script) S 8512 8513 6872 0 -1 0 289 239 0 0 0 0 0 1 18 0 1 0 1797478189 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/8513/statm): 531 226 485 147 0 384 0 [pid=8513] vsize: 2124 Raw data (/proc/8517/stat): 8517 (minisat+_64-bit) R 8513 8513 6872 0 -1 0 18872 0 0 0 57819 91 0 0 25 0 1 0 1797478194 81534976 17470 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/8517/statm): 19906 17470 145 145 0 19761 0 [pid=8517] vsize: 79624 Current children cumulated CPU time (s) 579.11 Current children cumulated vsize (Kb) 81748 [startup+590.04 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 8517 Raw data (/proc/8513/stat): 8513 (minisat+_script) S 8512 8513 6872 0 -1 0 289 239 0 0 0 0 0 1 18 0 1 0 1797478189 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/8513/statm): 531 226 485 147 0 384 0 [pid=8513] vsize: 2124 Raw data (/proc/8517/stat): 8517 (minisat+_64-bit) R 8513 8513 6872 0 -1 0 19029 0 0 0 58816 93 0 0 25 0 1 0 1797478194 82161664 17627 4294967295 134512640 135094434 3221224448 3221223108 134553446 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/8517/statm): 20059 17627 145 145 0 19914 0 [pid=8517] vsize: 80236 Current children cumulated CPU time (s) 589.1 Current children cumulated vsize (Kb) 82360 [startup+600.043 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 8517 Raw data (/proc/8513/stat): 8513 (minisat+_script) S 8512 8513 6872 0 -1 0 289 239 0 0 0 0 0 1 18 0 1 0 1797478189 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/8513/statm): 531 226 485 147 0 384 0 [pid=8513] vsize: 2124 Raw data (/proc/8517/stat): 8517 (minisat+_64-bit) R 8513 8513 6872 0 -1 0 19081 0 0 0 59816 93 0 0 25 0 1 0 1797478194 82362368 17679 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/8517/statm): 20108 17679 145 145 0 19963 0 [pid=8517] vsize: 80432 Current children cumulated CPU time (s) 599.1 Current children cumulated vsize (Kb) 82556 [startup+610.043 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 8517 Raw data (/proc/8513/stat): 8513 (minisat+_script) S 8512 8513 6872 0 -1 0 289 239 0 0 0 0 0 1 18 0 1 0 1797478189 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/8513/statm): 531 226 485 147 0 384 0 [pid=8513] vsize: 2124 Raw data (/proc/8517/stat): 8517 (minisat+_64-bit) R 8513 8513 6872 0 -1 0 19127 0 0 0 60815 93 0 0 25 0 1 0 1797478194 82542592 17725 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/8517/statm): 20152 17725 145 145 0 20007 0 [pid=8517] vsize: 80608 Current children cumulated CPU time (s) 609.09 Current children cumulated vsize (Kb) 82732 [startup+620.044 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 8517 Raw data (/proc/8513/stat): 8513 (minisat+_script) S 8512 8513 6872 0 -1 0 289 239 0 0 0 0 0 1 18 0 1 0 1797478189 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/8513/statm): 531 226 485 147 0 384 0 [pid=8513] vsize: 2124 Raw data (/proc/8517/stat): 8517 (minisat+_64-bit) R 8513 8513 6872 0 -1 0 19201 0 0 0 61814 94 0 0 25 0 1 0 1797478194 82841600 17799 4294967295 134512640 135094434 3221224448 3221223104 134558178 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/8517/statm): 20225 17799 145 145 0 20080 0 [pid=8517] vsize: 80900 Current children cumulated CPU time (s) 619.09 Current children cumulated vsize (Kb) 83024 [startup+630.045 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 8517 Raw data (/proc/8513/stat): 8513 (minisat+_script) S 8512 8513 6872 0 -1 0 289 239 0 0 0 0 0 1 18 0 1 0 1797478189 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/8513/statm): 531 226 485 147 0 384 0 [pid=8513] vsize: 2124 Raw data (/proc/8517/stat): 8517 (minisat+_64-bit) R 8513 8513 6872 0 -1 0 19262 0 0 0 62813 94 0 0 25 0 1 0 1797478194 83083264 17860 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/8517/statm): 20284 17860 145 145 0 20139 0 [pid=8517] vsize: 81136 Current children cumulated CPU time (s) 629.08 Current children cumulated vsize (Kb) 83260 [startup+640.045 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 8517 Raw data (/proc/8513/stat): 8513 (minisat+_script) S 8512 8513 6872 0 -1 0 289 239 0 0 0 0 0 1 18 0 1 0 1797478189 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/8513/statm): 531 226 485 147 0 384 0 [pid=8513] vsize: 2124 Raw data (/proc/8517/stat): 8517 (minisat+_64-bit) R 8513 8513 6872 0 -1 0 19304 0 0 0 63812 95 0 0 25 0 1 0 1797478194 83247104 17902 4294967295 134512640 135094434 3221224448 3221223108 134553475 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/8517/statm): 20324 17902 145 145 0 20179 0 [pid=8517] vsize: 81296 Current children cumulated CPU time (s) 639.08 Current children cumulated vsize (Kb) 83420 [startup+650.046 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 8517 Raw data (/proc/8513/stat): 8513 (minisat+_script) S 8512 8513 6872 0 -1 0 289 239 0 0 0 0 0 1 18 0 1 0 1797478189 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/8513/statm): 531 226 485 147 0 384 0 [pid=8513] vsize: 2124 Raw data (/proc/8517/stat): 8517 (minisat+_64-bit) R 8513 8513 6872 0 -1 0 19360 0 0 0 64811 95 0 0 25 0 1 0 1797478194 83468288 17958 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/8517/statm): 20378 17958 145 145 0 20233 0 [pid=8517] vsize: 81512 Current children cumulated CPU time (s) 649.07 Current children cumulated vsize (Kb) 83636 [startup+660.047 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 8517 Raw data (/proc/8513/stat): 8513 (minisat+_script) S 8512 8513 6872 0 -1 0 289 239 0 0 0 0 0 1 18 0 1 0 1797478189 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/8513/statm): 531 226 485 147 0 384 0 [pid=8513] vsize: 2124 Raw data (/proc/8517/stat): 8517 (minisat+_64-bit) R 8513 8513 6872 0 -1 0 19410 0 0 0 65810 96 0 0 25 0 1 0 1797478194 83664896 18008 4294967295 134512640 135094434 3221224448 3221223060 134563049 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/8517/statm): 20426 18008 145 145 0 20281 0 [pid=8517] vsize: 81704 Current children cumulated CPU time (s) 659.07 Current children cumulated vsize (Kb) 83828 [startup+670.047 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 8517 Raw data (/proc/8513/stat): 8513 (minisat+_script) S 8512 8513 6872 0 -1 0 289 239 0 0 0 0 0 1 18 0 1 0 1797478189 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/8513/statm): 531 226 485 147 0 384 0 [pid=8513] vsize: 2124 Raw data (/proc/8517/stat): 8517 (minisat+_64-bit) R 8513 8513 6872 0 -1 0 19458 0 0 0 66809 97 0 0 25 0 1 0 1797478194 83853312 18056 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/8517/statm): 20472 18056 145 145 0 20327 0 [pid=8517] vsize: 81888 Current children cumulated CPU time (s) 669.07 Current children cumulated vsize (Kb) 84012 [startup+680.048 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 8517 Raw data (/proc/8513/stat): 8513 (minisat+_script) S 8512 8513 6872 0 -1 0 289 239 0 0 0 0 0 1 18 0 1 0 1797478189 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/8513/statm): 531 226 485 147 0 384 0 [pid=8513] vsize: 2124 Raw data (/proc/8517/stat): 8517 (minisat+_64-bit) R 8513 8513 6872 0 -1 0 19539 0 0 0 67808 97 0 0 25 0 1 0 1797478194 84168704 18137 4294967295 134512640 135094434 3221224448 3221223072 134557711 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/8517/statm): 20549 18137 145 145 0 20404 0 [pid=8517] vsize: 82196 Current children cumulated CPU time (s) 679.06 Current children cumulated vsize (Kb) 84320 [startup+690.049 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 8517 Raw data (/proc/8513/stat): 8513 (minisat+_script) S 8512 8513 6872 0 -1 0 289 239 0 0 0 0 0 1 18 0 1 0 1797478189 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/8513/statm): 531 226 485 147 0 384 0 [pid=8513] vsize: 2124 Raw data (/proc/8517/stat): 8517 (minisat+_64-bit) R 8513 8513 6872 0 -1 0 19629 0 0 0 68806 98 0 0 25 0 1 0 1797478194 84525056 18227 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/8517/statm): 20636 18227 145 145 0 20491 0 [pid=8517] vsize: 82544 Current children cumulated CPU time (s) 689.05 Current children cumulated vsize (Kb) 84668 [startup+700.05 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 8517 Raw data (/proc/8513/stat): 8513 (minisat+_script) S 8512 8513 6872 0 -1 0 289 239 0 0 0 0 0 1 18 0 1 0 1797478189 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/8513/statm): 531 226 485 147 0 384 0 [pid=8513] vsize: 2124 Raw data (/proc/8517/stat): 8517 (minisat+_64-bit) R 8513 8513 6872 0 -1 0 19698 0 0 0 69805 98 0 0 25 0 1 0 1797478194 84795392 18296 4294967295 134512640 135094434 3221224448 3221223076 134557564 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/8517/statm): 20702 18296 145 145 0 20557 0 [pid=8517] vsize: 82808 Current children cumulated CPU time (s) 699.04 Current children cumulated vsize (Kb) 84932 [startup+710.05 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 8517 Raw data (/proc/8513/stat): 8513 (minisat+_script) S 8512 8513 6872 0 -1 0 289 239 0 0 0 0 0 1 18 0 1 0 1797478189 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/8513/statm): 531 226 485 147 0 384 0 [pid=8513] vsize: 2124 Raw data (/proc/8517/stat): 8517 (minisat+_64-bit) R 8513 8513 6872 0 -1 0 19746 0 0 0 70804 99 0 0 25 0 1 0 1797478194 84983808 18344 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/8517/statm): 20748 18344 145 145 0 20603 0 [pid=8517] vsize: 82992 Current children cumulated CPU time (s) 709.04 Current children cumulated vsize (Kb) 85116 [startup+720.051 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 8517 Raw data (/proc/8513/stat): 8513 (minisat+_script) S 8512 8513 6872 0 -1 0 289 239 0 0 0 0 0 1 18 0 1 0 1797478189 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/8513/statm): 531 226 485 147 0 384 0 [pid=8513] vsize: 2124 Raw data (/proc/8517/stat): 8517 (minisat+_64-bit) R 8513 8513 6872 0 -1 0 19819 0 0 0 71803 99 0 0 25 0 1 0 1797478194 85278720 18417 4294967295 134512640 135094434 3221224448 3221223060 134563064 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/8517/statm): 20820 18417 145 145 0 20675 0 [pid=8517] vsize: 83280 Current children cumulated CPU time (s) 719.03 Current children cumulated vsize (Kb) 85404 [startup+730.052 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 8517 Raw data (/proc/8513/stat): 8513 (minisat+_script) S 8512 8513 6872 0 -1 0 289 239 0 0 0 0 0 1 18 0 1 0 1797478189 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/8513/statm): 531 226 485 147 0 384 0 [pid=8513] vsize: 2124 Raw data (/proc/8517/stat): 8517 (minisat+_64-bit) R 8513 8513 6872 0 -1 0 19879 0 0 0 72802 100 0 0 25 0 1 0 1797478194 85516288 18477 4294967295 134512640 135094434 3221224448 3221223136 134554709 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/8517/statm): 20878 18477 145 145 0 20733 0 [pid=8517] vsize: 83512 Current children cumulated CPU time (s) 729.03 Current children cumulated vsize (Kb) 85636 [startup+740.052 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 8517 Raw data (/proc/8513/stat): 8513 (minisat+_script) S 8512 8513 6872 0 -1 0 289 239 0 0 0 0 0 1 18 0 1 0 1797478189 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/8513/statm): 531 226 485 147 0 384 0 [pid=8513] vsize: 2124 Raw data (/proc/8517/stat): 8517 (minisat+_64-bit) R 8513 8513 6872 0 -1 0 19930 0 0 0 73801 100 0 0 25 0 1 0 1797478194 85712896 18528 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/8517/statm): 20926 18528 145 145 0 20781 0 [pid=8517] vsize: 83704 Current children cumulated CPU time (s) 739.02 Current children cumulated vsize (Kb) 85828 [startup+750.053 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 8517 Raw data (/proc/8513/stat): 8513 (minisat+_script) S 8512 8513 6872 0 -1 0 289 239 0 0 0 0 0 1 18 0 1 0 1797478189 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/8513/statm): 531 226 485 147 0 384 0 [pid=8513] vsize: 2124 Raw data (/proc/8517/stat): 8517 (minisat+_64-bit) R 8513 8513 6872 0 -1 0 19993 0 0 0 74801 100 0 0 25 0 1 0 1797478194 85962752 18591 4294967295 134512640 135094434 3221224448 3221223104 134557774 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/8517/statm): 20987 18591 145 145 0 20842 0 [pid=8517] vsize: 83948 Current children cumulated CPU time (s) 749.02 Current children cumulated vsize (Kb) 86072 [startup+760.054 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 8517 Raw data (/proc/8513/stat): 8513 (minisat+_script) S 8512 8513 6872 0 -1 0 289 239 0 0 0 0 0 1 18 0 1 0 1797478189 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/8513/statm): 531 226 485 147 0 384 0 [pid=8513] vsize: 2124 Raw data (/proc/8517/stat): 8517 (minisat+_64-bit) R 8513 8513 6872 0 -1 0 20057 0 0 0 75800 101 0 0 25 0 1 0 1797478194 86212608 18655 4294967295 134512640 135094434 3221224448 3221223060 134563087 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/8517/statm): 21048 18655 145 145 0 20903 0 [pid=8517] vsize: 84192 Current children cumulated CPU time (s) 759.02 Current children cumulated vsize (Kb) 86316 [startup+770.054 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 8517 Raw data (/proc/8513/stat): 8513 (minisat+_script) S 8512 8513 6872 0 -1 0 289 239 0 0 0 0 0 1 18 0 1 0 1797478189 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/8513/statm): 531 226 485 147 0 384 0 [pid=8513] vsize: 2124 Raw data (/proc/8517/stat): 8517 (minisat+_64-bit) R 8513 8513 6872 0 -1 0 20105 0 0 0 76799 101 0 0 25 0 1 0 1797478194 86401024 18703 4294967295 134512640 135094434 3221224448 3221223060 134563148 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/8517/statm): 21094 18703 145 145 0 20949 0 [pid=8517] vsize: 84376 Current children cumulated CPU time (s) 769.01 Current children cumulated vsize (Kb) 86500 [startup+780.055 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 8517 Raw data (/proc/8513/stat): 8513 (minisat+_script) S 8512 8513 6872 0 -1 0 289 239 0 0 0 0 0 1 18 0 1 0 1797478189 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/8513/statm): 531 226 485 147 0 384 0 [pid=8513] vsize: 2124 Raw data (/proc/8517/stat): 8517 (minisat+_64-bit) R 8513 8513 6872 0 -1 0 20200 0 0 0 77798 102 0 0 25 0 1 0 1797478194 86777856 18798 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/8517/statm): 21186 18798 145 145 0 21041 0 [pid=8517] vsize: 84744 Current children cumulated CPU time (s) 779.01 Current children cumulated vsize (Kb) 86868 [startup+790.056 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 8517 Raw data (/proc/8513/stat): 8513 (minisat+_script) S 8512 8513 6872 0 -1 0 289 239 0 0 0 0 0 1 18 0 1 0 1797478189 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/8513/statm): 531 226 485 147 0 384 0 [pid=8513] vsize: 2124 Raw data (/proc/8517/stat): 8517 (minisat+_64-bit) R 8513 8513 6872 0 -1 0 20261 0 0 0 78798 102 0 0 25 0 1 0 1797478194 87015424 18859 4294967295 134512640 135094434 3221224448 3221223136 134554723 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/8517/statm): 21244 18859 145 145 0 21099 0 [pid=8517] vsize: 84976 Current children cumulated CPU time (s) 789.01 Current children cumulated vsize (Kb) 87100 [startup+800.057 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 8517 Raw data (/proc/8513/stat): 8513 (minisat+_script) S 8512 8513 6872 0 -1 0 289 239 0 0 0 0 0 1 18 0 1 0 1797478189 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/8513/statm): 531 226 485 147 0 384 0 [pid=8513] vsize: 2124 Raw data (/proc/8517/stat): 8517 (minisat+_64-bit) R 8513 8513 6872 0 -1 0 20333 0 0 0 79797 103 0 0 25 0 1 0 1797478194 87298048 18931 4294967295 134512640 135094434 3221224448 3221223104 134557948 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/8517/statm): 21313 18931 145 145 0 21168 0 [pid=8517] vsize: 85252 Current children cumulated CPU time (s) 799.01 Current children cumulated vsize (Kb) 87376 [startup+810.057 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 8517 Raw data (/proc/8513/stat): 8513 (minisat+_script) S 8512 8513 6872 0 -1 0 289 239 0 0 0 0 0 1 18 0 1 0 1797478189 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/8513/statm): 531 226 485 147 0 384 0 [pid=8513] vsize: 2124 Raw data (/proc/8517/stat): 8517 (minisat+_64-bit) R 8513 8513 6872 0 -1 0 20423 0 0 0 80795 103 0 0 25 0 1 0 1797478194 87654400 19021 4294967295 134512640 135094434 3221224448 3221223104 134557884 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/8517/statm): 21400 19021 145 145 0 21255 0 [pid=8517] vsize: 85600 Current children cumulated CPU time (s) 808.99 Current children cumulated vsize (Kb) 87724 [startup+820.058 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 8517 Raw data (/proc/8513/stat): 8513 (minisat+_script) S 8512 8513 6872 0 -1 0 289 239 0 0 0 0 0 1 18 0 1 0 1797478189 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/8513/statm): 531 226 485 147 0 384 0 [pid=8513] vsize: 2124 Raw data (/proc/8517/stat): 8517 (minisat+_64-bit) R 8513 8513 6872 0 -1 0 20487 0 0 0 81794 104 0 0 25 0 1 0 1797478194 87920640 19085 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/8517/statm): 21465 19085 145 145 0 21320 0 [pid=8517] vsize: 85860 Current children cumulated CPU time (s) 818.99 Current children cumulated vsize (Kb) 87984 [startup+830.059 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 8517 Raw data (/proc/8513/stat): 8513 (minisat+_script) S 8512 8513 6872 0 -1 0 289 239 0 0 0 0 0 1 18 0 1 0 1797478189 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/8513/statm): 531 226 485 147 0 384 0 [pid=8513] vsize: 2124 Raw data (/proc/8517/stat): 8517 (minisat+_64-bit) R 8513 8513 6872 0 -1 0 20555 0 0 0 82792 105 0 0 25 0 1 0 1797478194 88199168 19153 4294967295 134512640 135094434 3221224448 3221223104 134558213 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/8517/statm): 21533 19153 145 145 0 21388 0 [pid=8517] vsize: 86132 Current children cumulated CPU time (s) 828.98 Current children cumulated vsize (Kb) 88256 [startup+840.059 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 8517 Raw data (/proc/8513/stat): 8513 (minisat+_script) S 8512 8513 6872 0 -1 0 289 239 0 0 0 0 0 1 18 0 1 0 1797478189 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/8513/statm): 531 226 485 147 0 384 0 [pid=8513] vsize: 2124 Raw data (/proc/8517/stat): 8517 (minisat+_64-bit) R 8513 8513 6872 0 -1 0 20621 0 0 0 83791 106 0 0 25 0 1 0 1797478194 88465408 19219 4294967295 134512640 135094434 3221224448 3221223104 134558159 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/8517/statm): 21598 19219 145 145 0 21453 0 [pid=8517] vsize: 86392 Current children cumulated CPU time (s) 838.98 Current children cumulated vsize (Kb) 88516 [startup+850.06 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 8517 Raw data (/proc/8513/stat): 8513 (minisat+_script) S 8512 8513 6872 0 -1 0 289 239 0 0 0 0 0 1 18 0 1 0 1797478189 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/8513/statm): 531 226 485 147 0 384 0 [pid=8513] vsize: 2124 Raw data (/proc/8517/stat): 8517 (minisat+_64-bit) R 8513 8513 6872 0 -1 0 20725 0 0 0 84790 106 0 0 25 0 1 0 1797478194 88887296 19323 4294967295 134512640 135094434 3221224448 3221223104 134557846 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/8517/statm): 21701 19323 145 145 0 21556 0 [pid=8517] vsize: 86804 Current children cumulated CPU time (s) 848.97 Current children cumulated vsize (Kb) 88928 [startup+860.06 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 8517 Raw data (/proc/8513/stat): 8513 (minisat+_script) S 8512 8513 6872 0 -1 0 289 239 0 0 0 0 0 1 18 0 1 0 1797478189 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/8513/statm): 531 226 485 147 0 384 0 [pid=8513] vsize: 2124 Raw data (/proc/8517/stat): 8517 (minisat+_64-bit) R 8513 8513 6872 0 -1 0 20819 0 0 0 85789 106 0 0 25 0 1 0 1797478194 89264128 19417 4294967295 134512640 135094434 3221224448 3221223088 134562092 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/8517/statm): 21793 19417 145 145 0 21648 0 [pid=8517] vsize: 87172 Current children cumulated CPU time (s) 858.96 Current children cumulated vsize (Kb) 89296 [startup+870.061 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 8517 Raw data (/proc/8513/stat): 8513 (minisat+_script) S 8512 8513 6872 0 -1 0 289 239 0 0 0 0 0 1 18 0 1 0 1797478189 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/8513/statm): 531 226 485 147 0 384 0 [pid=8513] vsize: 2124 Raw data (/proc/8517/stat): 8517 (minisat+_64-bit) R 8513 8513 6872 0 -1 0 20906 0 0 0 86787 107 0 0 25 0 1 0 1797478194 89604096 19504 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/8517/statm): 21876 19504 145 145 0 21731 0 [pid=8517] vsize: 87504 Current children cumulated CPU time (s) 868.95 Current children cumulated vsize (Kb) 89628 [startup+880.061 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 8517 Raw data (/proc/8513/stat): 8513 (minisat+_script) S 8512 8513 6872 0 -1 0 289 239 0 0 0 0 0 1 18 0 1 0 1797478189 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/8513/statm): 531 226 485 147 0 384 0 [pid=8513] vsize: 2124 Raw data (/proc/8517/stat): 8517 (minisat+_64-bit) R 8513 8513 6872 0 -1 0 20989 0 0 0 87786 108 0 0 25 0 1 0 1797478194 89931776 19587 4294967295 134512640 135094434 3221224448 3221223072 134557696 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/8517/statm): 21956 19587 145 145 0 21811 0 [pid=8517] vsize: 87824 Current children cumulated CPU time (s) 878.95 Current children cumulated vsize (Kb) 89948 [startup+890.062 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 8517 Raw data (/proc/8513/stat): 8513 (minisat+_script) S 8512 8513 6872 0 -1 0 289 239 0 0 0 0 0 1 18 0 1 0 1797478189 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/8513/statm): 531 226 485 147 0 384 0 [pid=8513] vsize: 2124 Raw data (/proc/8517/stat): 8517 (minisat+_64-bit) R 8513 8513 6872 0 -1 0 21078 0 0 0 88785 108 0 0 25 0 1 0 1797478194 90275840 19676 4294967295 134512640 135094434 3221224448 3221223136 134554731 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/8517/statm): 22040 19676 145 145 0 21895 0 [pid=8517] vsize: 88160 Current children cumulated CPU time (s) 888.94 Current children cumulated vsize (Kb) 90284 [startup+900.063 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 8517 Raw data (/proc/8513/stat): 8513 (minisat+_script) S 8512 8513 6872 0 -1 0 289 239 0 0 0 0 0 1 18 0 1 0 1797478189 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/8513/statm): 531 226 485 147 0 384 0 [pid=8513] vsize: 2124 Raw data (/proc/8517/stat): 8517 (minisat+_64-bit) R 8513 8513 6872 0 -1 0 21152 0 0 0 89784 109 0 0 25 0 1 0 1797478194 90570752 19750 4294967295 134512640 135094434 3221224448 3221223104 134558402 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/8517/statm): 22112 19750 145 145 0 21967 0 [pid=8517] vsize: 88448 Current children cumulated CPU time (s) 898.94 Current children cumulated vsize (Kb) 90572 [startup+910.063 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 8517 Raw data (/proc/8513/stat): 8513 (minisat+_script) S 8512 8513 6872 0 -1 0 289 239 0 0 0 0 0 1 18 0 1 0 1797478189 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/8513/statm): 531 226 485 147 0 384 0 [pid=8513] vsize: 2124 Raw data (/proc/8517/stat): 8517 (minisat+_64-bit) R 8513 8513 6872 0 -1 0 21198 0 0 0 90783 109 0 0 25 0 1 0 1797478194 90750976 19796 4294967295 134512640 135094434 3221224448 3221223108 134553450 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/8517/statm): 22156 19796 145 145 0 22011 0 [pid=8517] vsize: 88624 Current children cumulated CPU time (s) 908.93 Current children cumulated vsize (Kb) 90748 [startup+920.064 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 8517 Raw data (/proc/8513/stat): 8513 (minisat+_script) S 8512 8513 6872 0 -1 0 289 239 0 0 0 0 0 1 18 0 1 0 1797478189 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/8513/statm): 531 226 485 147 0 384 0 [pid=8513] vsize: 2124 Raw data (/proc/8517/stat): 8517 (minisat+_64-bit) R 8513 8513 6872 0 -1 0 21278 0 0 0 91782 110 0 0 25 0 1 0 1797478194 91066368 19876 4294967295 134512640 135094434 3221224448 3221223104 134558402 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/8517/statm): 22233 19876 145 145 0 22088 0 [pid=8517] vsize: 88932 Current children cumulated CPU time (s) 918.93 Current children cumulated vsize (Kb) 91056 [startup+930.065 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 8517 Raw data (/proc/8513/stat): 8513 (minisat+_script) S 8512 8513 6872 0 -1 0 289 239 0 0 0 0 0 1 18 0 1 0 1797478189 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/8513/statm): 531 226 485 147 0 384 0 [pid=8513] vsize: 2124 Raw data (/proc/8517/stat): 8517 (minisat+_64-bit) R 8513 8513 6872 0 -1 0 21369 0 0 0 92780 111 0 0 25 0 1 0 1797478194 91430912 19967 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/8517/statm): 22322 19967 145 145 0 22177 0 [pid=8517] vsize: 89288 Current children cumulated CPU time (s) 928.92 Current children cumulated vsize (Kb) 91412 [startup+940.066 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 8517 Raw data (/proc/8513/stat): 8513 (minisat+_script) S 8512 8513 6872 0 -1 0 289 239 0 0 0 0 0 1 18 0 1 0 1797478189 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/8513/statm): 531 226 485 147 0 384 0 [pid=8513] vsize: 2124 Raw data (/proc/8517/stat): 8517 (minisat+_64-bit) R 8513 8513 6872 0 -1 0 21450 0 0 0 93778 112 0 0 25 0 1 0 1797478194 91750400 20048 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/8517/statm): 22400 20048 145 145 0 22255 0 [pid=8517] vsize: 89600 Current children cumulated CPU time (s) 938.91 Current children cumulated vsize (Kb) 91724 [startup+950.067 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 8517 Raw data (/proc/8513/stat): 8513 (minisat+_script) S 8512 8513 6872 0 -1 0 289 239 0 0 0 0 0 1 18 0 1 0 1797478189 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/8513/statm): 531 226 485 147 0 384 0 [pid=8513] vsize: 2124 Raw data (/proc/8517/stat): 8517 (minisat+_64-bit) R 8513 8513 6872 0 -1 0 21497 0 0 0 94778 112 0 0 25 0 1 0 1797478194 92975104 20095 4294967295 134512640 135094434 3221224448 3221223108 134553501 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/8517/statm): 22699 20095 145 145 0 22554 0 [pid=8517] vsize: 90796 Current children cumulated CPU time (s) 948.91 Current children cumulated vsize (Kb) 92920 [startup+960.068 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 8517 Raw data (/proc/8513/stat): 8513 (minisat+_script) S 8512 8513 6872 0 -1 0 289 239 0 0 0 0 0 1 18 0 1 0 1797478189 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/8513/statm): 531 226 485 147 0 384 0 [pid=8513] vsize: 2124 Raw data (/proc/8517/stat): 8517 (minisat+_64-bit) R 8513 8513 6872 0 -1 0 21575 0 0 0 95777 112 0 0 25 0 1 0 1797478194 93282304 20173 4294967295 134512640 135094434 3221224448 3221223088 134562146 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/8517/statm): 22774 20173 145 145 0 22629 0 [pid=8517] vsize: 91096 Current children cumulated CPU time (s) 958.9 Current children cumulated vsize (Kb) 93220 [startup+970.068 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 8517 Raw data (/proc/8513/stat): 8513 (minisat+_script) S 8512 8513 6872 0 -1 0 289 239 0 0 0 0 0 1 18 0 1 0 1797478189 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/8513/statm): 531 226 485 147 0 384 0 [pid=8513] vsize: 2124 Raw data (/proc/8517/stat): 8517 (minisat+_64-bit) R 8513 8513 6872 0 -1 0 21689 0 0 0 96776 113 0 0 25 0 1 0 1797478194 93736960 20287 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/8517/statm): 22885 20287 145 145 0 22740 0 [pid=8517] vsize: 91540 Current children cumulated CPU time (s) 968.9 Current children cumulated vsize (Kb) 93664 [startup+980.069 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 8517 Raw data (/proc/8513/stat): 8513 (minisat+_script) S 8512 8513 6872 0 -1 0 289 239 0 0 0 0 0 1 18 0 1 0 1797478189 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/8513/statm): 531 226 485 147 0 384 0 [pid=8513] vsize: 2124 Raw data (/proc/8517/stat): 8517 (minisat+_64-bit) R 8513 8513 6872 0 -1 0 21788 0 0 0 97775 113 0 0 25 0 1 0 1797478194 94126080 20386 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/8517/statm): 22980 20386 145 145 0 22835 0 [pid=8517] vsize: 91920 Current children cumulated CPU time (s) 978.89 Current children cumulated vsize (Kb) 94044 [startup+990.07 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 8517 Raw data (/proc/8513/stat): 8513 (minisat+_script) S 8512 8513 6872 0 -1 0 289 239 0 0 0 0 0 1 18 0 1 0 1797478189 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/8513/statm): 531 226 485 147 0 384 0 [pid=8513] vsize: 2124 Raw data (/proc/8517/stat): 8517 (minisat+_64-bit) R 8513 8513 6872 0 -1 0 21837 0 0 0 98774 114 0 0 25 0 1 0 1797478194 94318592 20435 4294967295 134512640 135094434 3221224448 3221223108 134553515 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/8517/statm): 23027 20435 145 145 0 22882 0 [pid=8517] vsize: 92108 Current children cumulated CPU time (s) 988.89 Current children cumulated vsize (Kb) 94232 [startup+1000.07 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 8517 Raw data (/proc/8513/stat): 8513 (minisat+_script) S 8512 8513 6872 0 -1 0 289 239 0 0 0 0 0 1 18 0 1 0 1797478189 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/8513/statm): 531 226 485 147 0 384 0 [pid=8513] vsize: 2124 Raw data (/proc/8517/stat): 8517 (minisat+_64-bit) R 8513 8513 6872 0 -1 0 21875 0 0 0 99774 114 0 0 25 0 1 0 1797478194 94466048 20473 4294967295 134512640 135094434 3221224448 3221223108 134553497 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/8517/statm): 23063 20473 145 145 0 22918 0 [pid=8517] vsize: 92252 Current children cumulated CPU time (s) 998.89 Current children cumulated vsize (Kb) 94376 [startup+1010.07 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 8517 Raw data (/proc/8513/stat): 8513 (minisat+_script) S 8512 8513 6872 0 -1 0 289 239 0 0 0 0 0 1 18 0 1 0 1797478189 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/8513/statm): 531 226 485 147 0 384 0 [pid=8513] vsize: 2124 Raw data (/proc/8517/stat): 8517 (minisat+_64-bit) R 8513 8513 6872 0 -1 0 21908 0 0 0 100773 115 0 0 25 0 1 0 1797478194 94593024 20506 4294967295 134512640 135094434 3221224448 3221223140 134558984 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/8517/statm): 23094 20506 145 145 0 22949 0 [pid=8517] vsize: 92376 Current children cumulated CPU time (s) 1008.89 Current children cumulated vsize (Kb) 94500 [startup+1020.07 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 8517 Raw data (/proc/8513/stat): 8513 (minisat+_script) S 8512 8513 6872 0 -1 0 289 239 0 0 0 0 0 1 18 0 1 0 1797478189 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/8513/statm): 531 226 485 147 0 384 0 [pid=8513] vsize: 2124 Raw data (/proc/8517/stat): 8517 (minisat+_64-bit) R 8513 8513 6872 0 -1 0 21943 0 0 0 101773 115 0 0 25 0 1 0 1797478194 94732288 20541 4294967295 134512640 135094434 3221224448 3221223108 134553446 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/8517/statm): 23128 20541 145 145 0 22983 0 [pid=8517] vsize: 92512 Current children cumulated CPU time (s) 1018.89 Current children cumulated vsize (Kb) 94636 [startup+1030.07 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 8517 Raw data (/proc/8513/stat): 8513 (minisat+_script) S 8512 8513 6872 0 -1 0 289 239 0 0 0 0 0 1 18 0 1 0 1797478189 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/8513/statm): 531 226 485 147 0 384 0 [pid=8513] vsize: 2124 Raw data (/proc/8517/stat): 8517 (minisat+_64-bit) R 8513 8513 6872 0 -1 0 22018 0 0 0 102771 115 0 0 25 0 1 0 1797478194 95031296 20616 4294967295 134512640 135094434 3221224448 3221223104 134557866 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/8517/statm): 23201 20616 145 145 0 23056 0 [pid=8517] vsize: 92804 Current children cumulated CPU time (s) 1028.87 Current children cumulated vsize (Kb) 94928 [startup+1040.07 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 8517 Raw data (/proc/8513/stat): 8513 (minisat+_script) S 8512 8513 6872 0 -1 0 289 239 0 0 0 0 0 1 18 0 1 0 1797478189 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/8513/statm): 531 226 485 147 0 384 0 [pid=8513] vsize: 2124 Raw data (/proc/8517/stat): 8517 (minisat+_64-bit) R 8513 8513 6872 0 -1 0 22079 0 0 0 103771 116 0 0 25 0 1 0 1797478194 95268864 20677 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/8517/statm): 23259 20677 145 145 0 23114 0 [pid=8517] vsize: 93036 Current children cumulated CPU time (s) 1038.88 Current children cumulated vsize (Kb) 95160 [startup+1050.07 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 8517 Raw data (/proc/8513/stat): 8513 (minisat+_script) S 8512 8513 6872 0 -1 0 289 239 0 0 0 0 0 1 18 0 1 0 1797478189 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/8513/statm): 531 226 485 147 0 384 0 [pid=8513] vsize: 2124 Raw data (/proc/8517/stat): 8517 (minisat+_64-bit) R 8513 8513 6872 0 -1 0 22142 0 0 0 104770 116 0 0 25 0 1 0 1797478194 95514624 20740 4294967295 134512640 135094434 3221224448 3221223172 134554336 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/8517/statm): 23319 20740 145 145 0 23174 0 [pid=8517] vsize: 93276 Current children cumulated CPU time (s) 1048.87 Current children cumulated vsize (Kb) 95400 [startup+1060.07 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 8517 Raw data (/proc/8513/stat): 8513 (minisat+_script) S 8512 8513 6872 0 -1 0 289 239 0 0 0 0 0 1 18 0 1 0 1797478189 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/8513/statm): 531 226 485 147 0 384 0 [pid=8513] vsize: 2124 Raw data (/proc/8517/stat): 8517 (minisat+_64-bit) R 8513 8513 6872 0 -1 0 22205 0 0 0 105768 117 0 0 25 0 1 0 1797478194 95764480 20803 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/8517/statm): 23380 20803 145 145 0 23235 0 [pid=8517] vsize: 93520 Current children cumulated CPU time (s) 1058.86 Current children cumulated vsize (Kb) 95644 [startup+1070.08 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 8517 Raw data (/proc/8513/stat): 8513 (minisat+_script) S 8512 8513 6872 0 -1 0 289 239 0 0 0 0 0 1 18 0 1 0 1797478189 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/8513/statm): 531 226 485 147 0 384 0 [pid=8513] vsize: 2124 Raw data (/proc/8517/stat): 8517 (minisat+_64-bit) R 8513 8513 6872 0 -1 0 22317 0 0 0 106766 118 0 0 25 0 1 0 1797478194 96206848 20915 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/8517/statm): 23488 20915 145 145 0 23343 0 [pid=8517] vsize: 93952 Current children cumulated CPU time (s) 1068.85 Current children cumulated vsize (Kb) 96076 [startup+1080.08 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 8517 Raw data (/proc/8513/stat): 8513 (minisat+_script) S 8512 8513 6872 0 -1 0 289 239 0 0 0 0 0 1 18 0 1 0 1797478189 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/8513/statm): 531 226 485 147 0 384 0 [pid=8513] vsize: 2124 Raw data (/proc/8517/stat): 8517 (minisat+_64-bit) R 8513 8513 6872 0 -1 0 22392 0 0 0 107765 118 0 0 25 0 1 0 1797478194 96505856 20990 4294967295 134512640 135094434 3221224448 3221223104 134558426 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/8517/statm): 23561 20990 145 145 0 23416 0 [pid=8517] vsize: 94244 Current children cumulated CPU time (s) 1078.84 Current children cumulated vsize (Kb) 96368 [startup+1090.08 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 8517 Raw data (/proc/8513/stat): 8513 (minisat+_script) S 8512 8513 6872 0 -1 0 289 239 0 0 0 0 0 1 18 0 1 0 1797478189 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/8513/statm): 531 226 485 147 0 384 0 [pid=8513] vsize: 2124 Raw data (/proc/8517/stat): 8517 (minisat+_64-bit) R 8513 8513 6872 0 -1 0 22595 0 0 0 108761 120 0 0 25 0 1 0 1797478194 97316864 21193 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/8517/statm): 23759 21193 145 145 0 23614 0 [pid=8517] vsize: 95036 Current children cumulated CPU time (s) 1088.82 Current children cumulated vsize (Kb) 97160 [startup+1100.08 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 8517 Raw data (/proc/8513/stat): 8513 (minisat+_script) S 8512 8513 6872 0 -1 0 289 239 0 0 0 0 0 1 18 0 1 0 1797478189 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/8513/statm): 531 226 485 147 0 384 0 [pid=8513] vsize: 2124 Raw data (/proc/8517/stat): 8517 (minisat+_64-bit) R 8513 8513 6872 0 -1 0 22666 0 0 0 109760 121 0 0 25 0 1 0 1797478194 97599488 21264 4294967295 134512640 135094434 3221224448 3221223104 134558159 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/8517/statm): 23828 21264 145 145 0 23683 0 [pid=8517] vsize: 95312 Current children cumulated CPU time (s) 1098.82 Current children cumulated vsize (Kb) 97436 [startup+1110.08 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 8517 Raw data (/proc/8513/stat): 8513 (minisat+_script) S 8512 8513 6872 0 -1 0 289 239 0 0 0 0 0 1 18 0 1 0 1797478189 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/8513/statm): 531 226 485 147 0 384 0 [pid=8513] vsize: 2124 Raw data (/proc/8517/stat): 8517 (minisat+_64-bit) R 8513 8513 6872 0 -1 0 22802 0 0 0 110758 121 0 0 25 0 1 0 1797478194 98140160 21400 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/8517/statm): 23960 21400 145 145 0 23815 0 [pid=8517] vsize: 95840 Current children cumulated CPU time (s) 1108.8 Current children cumulated vsize (Kb) 97964 [startup+1120.08 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 8517 Raw data (/proc/8513/stat): 8513 (minisat+_script) S 8512 8513 6872 0 -1 0 289 239 0 0 0 0 0 1 18 0 1 0 1797478189 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/8513/statm): 531 226 485 147 0 384 0 [pid=8513] vsize: 2124 Raw data (/proc/8517/stat): 8517 (minisat+_64-bit) R 8513 8513 6872 0 -1 0 22894 0 0 0 111757 122 0 0 25 0 1 0 1797478194 98500608 21492 4294967295 134512640 135094434 3221224448 3221223104 134558213 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/8517/statm): 24048 21492 145 145 0 23903 0 [pid=8517] vsize: 96192 Current children cumulated CPU time (s) 1118.8 Current children cumulated vsize (Kb) 98316 [startup+1130.08 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 8517 Raw data (/proc/8513/stat): 8513 (minisat+_script) S 8512 8513 6872 0 -1 0 289 239 0 0 0 0 0 1 18 0 1 0 1797478189 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/8513/statm): 531 226 485 147 0 384 0 [pid=8513] vsize: 2124 Raw data (/proc/8517/stat): 8517 (minisat+_64-bit) R 8513 8513 6872 0 -1 0 23014 0 0 0 112755 123 0 0 25 0 1 0 1797478194 98975744 21612 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/8517/statm): 24164 21612 145 145 0 24019 0 [pid=8517] vsize: 96656 Current children cumulated CPU time (s) 1128.79 Current children cumulated vsize (Kb) 98780 [startup+1140.08 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 8517 Raw data (/proc/8513/stat): 8513 (minisat+_script) S 8512 8513 6872 0 -1 0 289 239 0 0 0 0 0 1 18 0 1 0 1797478189 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/8513/statm): 531 226 485 147 0 384 0 [pid=8513] vsize: 2124 Raw data (/proc/8517/stat): 8517 (minisat+_64-bit) R 8513 8513 6872 0 -1 0 23112 0 0 0 113754 124 0 0 25 0 1 0 1797478194 99368960 21710 4294967295 134512640 135094434 3221224448 3221223108 134553482 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/8517/statm): 24260 21710 145 145 0 24115 0 [pid=8517] vsize: 97040 Current children cumulated CPU time (s) 1138.79 Current children cumulated vsize (Kb) 99164 [startup+1150.08 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 8517 Raw data (/proc/8513/stat): 8513 (minisat+_script) S 8512 8513 6872 0 -1 0 289 239 0 0 0 0 0 1 18 0 1 0 1797478189 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/8513/statm): 531 226 485 147 0 384 0 [pid=8513] vsize: 2124 Raw data (/proc/8517/stat): 8517 (minisat+_64-bit) R 8513 8513 6872 0 -1 0 23172 0 0 0 114752 124 0 0 25 0 1 0 1797478194 99606528 21770 4294967295 134512640 135094434 3221224448 3221223104 134557948 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/8517/statm): 24318 21770 145 145 0 24173 0 [pid=8517] vsize: 97272 Current children cumulated CPU time (s) 1148.77 Current children cumulated vsize (Kb) 99396 [startup+1160.08 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 8517 Raw data (/proc/8513/stat): 8513 (minisat+_script) S 8512 8513 6872 0 -1 0 289 239 0 0 0 0 0 1 18 0 1 0 1797478189 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/8513/statm): 531 226 485 147 0 384 0 [pid=8513] vsize: 2124 Raw data (/proc/8517/stat): 8517 (minisat+_64-bit) R 8513 8513 6872 0 -1 0 23229 0 0 0 115751 125 0 0 25 0 1 0 1797478194 99831808 21827 4294967295 134512640 135094434 3221224448 3221223104 134558159 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/8517/statm): 24373 21827 145 145 0 24228 0 [pid=8517] vsize: 97492 Current children cumulated CPU time (s) 1158.77 Current children cumulated vsize (Kb) 99616 [startup+1170.08 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 8517 Raw data (/proc/8513/stat): 8513 (minisat+_script) S 8512 8513 6872 0 -1 0 289 239 0 0 0 0 0 1 18 0 1 0 1797478189 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/8513/statm): 531 226 485 147 0 384 0 [pid=8513] vsize: 2124 Raw data (/proc/8517/stat): 8517 (minisat+_64-bit) R 8513 8513 6872 0 -1 0 23289 0 0 0 116750 125 0 0 25 0 1 0 1797478194 100065280 21887 4294967295 134512640 135094434 3221224448 3221223072 134557596 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/8517/statm): 24430 21887 145 145 0 24285 0 [pid=8517] vsize: 97720 Current children cumulated CPU time (s) 1168.76 Current children cumulated vsize (Kb) 99844 [startup+1180.08 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 8517 Raw data (/proc/8513/stat): 8513 (minisat+_script) S 8512 8513 6872 0 -1 0 289 239 0 0 0 0 0 1 18 0 1 0 1797478189 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/8513/statm): 531 226 485 147 0 384 0 [pid=8513] vsize: 2124 Raw data (/proc/8517/stat): 8517 (minisat+_64-bit) R 8513 8513 6872 0 -1 0 23615 0 0 0 117747 127 0 0 25 0 1 0 1797478194 101056512 22085 4294967295 134512640 135094434 3221224448 3221223088 134562057 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/8517/statm): 24672 22085 145 145 0 24527 0 [pid=8517] vsize: 98688 Current children cumulated CPU time (s) 1178.75 Current children cumulated vsize (Kb) 100812 [startup+1190.08 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 8517 Raw data (/proc/8513/stat): 8513 (minisat+_script) S 8512 8513 6872 0 -1 0 289 239 0 0 0 0 0 1 18 0 1 0 1797478189 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/8513/statm): 531 226 485 147 0 384 0 [pid=8513] vsize: 2124 Raw data (/proc/8517/stat): 8517 (minisat+_64-bit) R 8513 8513 6872 0 -1 0 23615 0 0 0 118748 127 0 0 25 0 1 0 1797478194 101056512 22085 4294967295 134512640 135094434 3221224448 3221223104 134557937 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/8517/statm): 24672 22085 145 145 0 24527 0 [pid=8517] vsize: 98688 Current children cumulated CPU time (s) 1188.76 Current children cumulated vsize (Kb) 100812 [startup+1200.08 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 8517 Raw data (/proc/8513/stat): 8513 (minisat+_script) S 8512 8513 6872 0 -1 0 289 239 0 0 0 0 0 1 18 0 1 0 1797478189 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/8513/statm): 531 226 485 147 0 384 0 [pid=8513] vsize: 2124 Raw data (/proc/8517/stat): 8517 (minisat+_64-bit) R 8513 8513 6872 0 -1 0 23615 0 0 0 119748 127 0 0 25 0 1 0 1797478194 101056512 22085 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/8517/statm): 24672 22085 145 145 0 24527 0 [pid=8517] vsize: 98688 Current children cumulated CPU time (s) 1198.76 Current children cumulated vsize (Kb) 100812 [startup+1210.09 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 8517 Raw data (/proc/8513/stat): 8513 (minisat+_script) S 8512 8513 6872 0 -1 0 289 239 0 0 0 0 0 1 18 0 1 0 1797478189 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/8513/statm): 531 226 485 147 0 384 0 [pid=8513] vsize: 2124 Raw data (/proc/8517/stat): 8517 (minisat+_64-bit) R 8513 8513 6872 0 -1 0 23615 0 0 0 120748 127 0 0 25 0 1 0 1797478194 101056512 22085 4294967295 134512640 135094434 3221224448 3221222976 134780558 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/8517/statm): 24672 22085 145 145 0 24527 0 [pid=8517] vsize: 98688 Current children cumulated CPU time (s) 1208.76 Current children cumulated vsize (Kb) 100812 Maximum CPU time exceeded: sending SIGTERM then SIGKILL [startup+1210.09 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 8517 Raw data (/proc/8513/stat): 8513 (minisat+_script) S 8512 8513 6872 0 -1 0 289 239 0 0 0 0 0 1 18 0 1 0 1797478189 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/8513/statm): 531 226 485 147 0 384 0 [pid=8513] vsize: 2124 Raw data (/proc/8517/stat): 8517 (minisat+_64-bit) R 8513 8513 6872 0 -1 0 23615 0 0 0 120748 127 0 0 25 0 1 0 1797478194 101056512 22085 4294967295 134512640 135094434 3221224448 3221223032 134552439 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/8517/statm): 24672 22085 145 145 0 24527 0 [pid=8517] vsize: 98688 Current children cumulated CPU time (s) 1208.76 Current children cumulated vsize (Kb) 100812 Sending SIGTERM to -8513 Sleeping 2 seconds One traced child (pid=8513) ended because it received signal 15 (SIGTERM) One traced child (pid=8517) exited with status: 10 All traced children have exited ! Game is over. Child status: 10 Real time (s): 1210.15 CPU time (s): 1208.81 CPU user time (s): 1207.49 CPU system time (s): 1.3168 CPU usage (%): 99.8896 Max. virtual memory (cumulated for all children) (Kb): 100812
ERROR: no interpretation found !