Name | submitted/een/normalized-p0201.opb |
MD5SUM | ff4eb45c2603a47e5b79b2649e926ba4 |
Bench Category | optimization, small integers (OPTSMALLINT) |
Has Objective Function | YES |
Satisfiable | YES |
(Un)Satisfiability was proved | YES |
Best value of the objective function | 1523 |
Optimality of the best value was proved | YES |
Number of terms in the objective function | 201 |
Biggest coefficient in the objective function | 1920 |
Number of bits for the biggest coefficient in the objective function | 11 |
Sum of the numbers in the objective function | 19980 |
Number of bits of the sum of numbers in the objective function | 15 |
Biggest number in a constraint | 1920 |
Number of bits of the biggest number in a constraint | 11 |
Biggest sum of numbers in a constraint | 19980 |
Number of bits of the biggest sum of numbers | 15 |
Best result obtained on this benchmark | OPTIMUM FOUND |
Best CPU time to get the best result obtained on this benchmark | 221.9 |
Number of variables | 195 |
Total number of constraints | 133 |
Number of constraints which are clauses | 20 |
Number of constraints which are cardinality constraints (but not clauses) | 26 |
Number of constraints which are nor clauses,nor cardinality constraints | 87 |
Minimum length of a constraint | 3 |
Maximum length of a constraint | 65 |
LAUNCH ON wulflinc5 THE 2005-09-18 18:25:09 (client local time) PB2005-SCRIPT v4.0 MARKUPS: idlaunch=2625 boxname=wulflinc5 idbench=281 idsolver=3 numberseed=0 MD5SUM SOLVER: MD5SUM BENCH: ff4eb45c2603a47e5b79b2649e926ba4 /oldhome/oroussel/tmp/wulflinc5/normalized-p0201.opb REAL COMMAND: minisat+_script /oldhome/oroussel/tmp/wulflinc5/normalized-p0201.opb IDLAUNCH: 2625 /proc/cpuinfo: processor : 0 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 2 cpu MHz : 451.007 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.007 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: 917876 kB Buffers: 33892 kB Cached: 59440 kB SwapCached: 780 kB Active: 59456 kB Inactive: 36588 kB HighTotal: 131008 kB HighFree: 67928 kB LowTotal: 903652 kB LowFree: 849948 kB SwapTotal: 2097136 kB SwapFree: 2095888 kB Dirty: 28 kB Writeback: 0 kB Mapped: 5804 kB Slab: 15216 kB Committed_AS: 64264 kB PageTables: 332 kB VmallocTotal: 114680 kB VmallocUsed: 1364 kB VmallocChunk: 113256 kB JOB ENDED THE 2005-09-18 18:45:19 (client local time) WITH STATUS 10 IN 1209.72 SECONDS stats: 2625 7 1209.72 10
c Parsing PB file... c Converting 133 PB-constraints to clauses... c -- Unit propagations: (none) c -- Detecting intervals from adjacent constraints: ################### c -- Clauses(.)/Splits(s): .sssss c ---[ 137]---> BDD-cost: 3 c ---[ 136]---> BDD-cost: 3 c ---[ 135]---> BDD-cost: 3 c ---[ 134]---> BDD-cost: 3 c ---[ 133]---> BDD-cost: 3 c ---[ 132]---> BDD-cost: 3 c ---[ 131]---> BDD-cost: 3 c ---[ 130]---> BDD-cost: 3 c ---[ 129]---> BDD-cost: 3 c ---[ 128]---> BDD-cost: 11 c ---[ 127]---> BDD-cost: 11 c ---[ 126]---> BDD-cost: 11 c ---[ 125]---> BDD-cost: 11 c ---[ 124]---> BDD-cost: 11 c ---[ 123]---> BDD-cost: 11 c ---[ 122]---> BDD-cost: 11 c ---[ 121]---> BDD-cost: 11 c ---[ 120]---> BDD-cost: 11 c ---[ 119]---> BDD-cost: 11 c ---[ 118]---> BDD-cost: 11 c ---[ 117]---> BDD-cost: 11 c ---[ 116]---> BDD-cost: 11 c ---[ 115]---> BDD-cost: 11 c ---[ 114]---> BDD-cost: 11 c ---[ 113]---> BDD-cost: 11 c ---[ 112]---> BDD-cost: 11 c ---[ 111]---> BDD-cost: 11 c ---[ 110]---> BDD-cost: 11 c ---[ 109]---> BDD-cost: 11 c ---[ 108]---> BDD-cost: 11 c ---[ 107]---> BDD-cost: 11 c ---[ 106]---> BDD-cost: 11 c ---[ 105]---> BDD-cost: 11 c ---[ 104]---> BDD-cost: 11 c ---[ 103]---> BDD-cost: 11 c ---[ 102]---> BDD-cost: 11 c ---[ 101]---> BDD-cost: 11 c ---[ 100]---> BDD-cost: 11 c ---[ 99]---> BDD-cost: 11 c ---[ 98]---> BDD-cost: 11 c ---[ 97]---> BDD-cost: 11 c ---[ 96]---> BDD-cost: 11 c ---[ 95]---> BDD-cost: 11 c ---[ 94]---> BDD-cost: 11 c ---[ 93]---> BDD-cost: 11 c ---[ 92]---> BDD-cost: 11 c ---[ 91]---> BDD-cost: 11 c ---[ 90]---> BDD-cost: 11 c ---[ 89]---> BDD-cost: 11 c ---[ 88]---> BDD-cost: 11 c ---[ 87]---> BDD-cost: 11 c ---[ 86]---> BDD-cost: 11 c ---[ 85]---> BDD-cost: 11 c ---[ 84]---> BDD-cost: 11 c ---[ 83]---> BDD-cost: 11 c ---[ 82]---> BDD-cost: 11 c ---[ 81]---> BDD-cost: 11 c ---[ 80]---> BDD-cost: 11 c ---[ 79]---> BDD-cost: 11 c ---[ 78]---> BDD-cost: 11 c ---[ 77]---> BDD-cost: 11 c ---[ 76]---> BDD-cost: 11 c ---[ 75]---> BDD-cost: 11 c ---[ 74]---> BDD-cost: 11 c ---[ 72]---> BDD-cost: 13 c ---[ 70]---> BDD-cost: 15 c ---[ 68]---> BDD-cost: 15 c ---[ 66]---> BDD-cost: 13 c ---[ 64]---> BDD-cost: 13 c ---[ 62]---> BDD-cost: 13 c ---[ 60]---> BDD-cost: 13 c ---[ 58]---> BDD-cost: 13 c ---[ 56]---> BDD-cost: 13 c ---[ 54]---> BDD-cost: 13 c ---[ 52]---> BDD-cost: 13 c ---[ 50]---> BDD-cost: 13 c ---[ 48]---> BDD-cost: 13 c ---[ 46]---> BDD-cost: 13 c ---[ 44]---> BDD-cost: 13 c ---[ 42]---> BDD-cost: 13 c ---[ 40]---> BDD-cost: 13 c ---[ 38]---> BDD-cost: 13 c ---[ 36]---> BDD-cost: 13 c ---[ 31]---> BDD-cost: 39 c ---[ 28]---> BDD-cost: 54 c ---[ 27]---> BDD-cost: 42 c ---[ 26]---> BDD-cost: 42 c ---[ 25]---> BDD-cost: 73 c ---[ 24]---> BDD-cost: 73 c ---[ 23]---> BDD-cost: 98 c ---[ 22]---> BDD-cost: 160 c ---[ 21]---> BDD-cost: 85 c ---[ 20]---> BDD-cost: 85 c ---[ 19]---> BDD-cost: 201 c ---[ 18]---> BDD-cost: 107 c ---[ 17]---> BDD-cost: 107 c ---[ 16]---> BDD-cost: 241 c ---[ 15]---> BDD-cost: 128 c ---[ 14]---> BDD-cost: 128 c ---[ 13]---> BDD-cost: 150 c ---[ 12]---> BDD-cost: 150 c ---[ 11]---> BDD-cost: 281 c ---[ 10]---> BDD-cost: 321 c ---[ 9]---> BDD-cost: 172 c ---[ 8]---> BDD-cost: 172 c ---[ 7]---> BDD-cost: 194 c ---[ 6]---> BDD-cost: 194 c ---[ 5]---> BDD-cost: 361 c ---[ 4]---> BDD-cost: 1 c ---[ 3]---> BDD-cost: 1 c ---[ 2]---> BDD-cost: 1 c ---[ 1]---> BDD-cost: 1 c ---[ 0]---> BDD-cost: 1 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 0 | 11741 34627 | 3913 0 0 nan | 0.000 % | c ============================================================================== c [1mFound solution: 2321[0m c ---[ 0]---> Sorter-cost:21987 Base: 5 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 22 | 60840 149261 | 20280 21 108 5.1 | 0.000 % | c | 122 | 60771 149095 | 22308 116 9072 78.2 | 0.586 % | c | 272 | 60333 148103 | 24538 263 10198 38.8 | 1.087 % | c ============================================================================== c [1mFound solution: 2304[0m c ---[ 0]---> Sorter-cost: 6 Base: 5 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 464 | 59190 145572 | 19730 360 10756 29.9 | 1.087 % | c | 564 | 56937 140394 | 21703 431 11589 26.9 | 6.067 % | c | 715 | 56667 139775 | 23873 579 15674 27.1 | 6.418 % | c | 940 | 56053 138362 | 26260 791 17405 22.0 | 7.522 % | c ============================================================================== c [1mFound solution: 2221[0m c ---[ 0]---> Sorter-cost: 1 Base: 5 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 973 | 55214 136433 | 18404 810 17568 21.7 | 7.522 % | c | 1073 | 55078 136119 | 20244 909 31790 35.0 | 8.517 % | c | 1223 | 53987 133608 | 22268 1036 32305 31.2 | 9.937 % | c | 1452 | 53445 132352 | 24495 1232 40064 32.5 | 10.686 % | c ============================================================================== c [1mFound solution: 2166[0m c ---[ 0]---> Sorter-cost: 5 Base: 5 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 1536 | 52668 130555 | 17556 1307 41474 31.7 | 10.686 % | c | 1637 | 52668 130555 | 19311 1408 46677 33.2 | 11.681 % | c | 1787 | 52668 130555 | 21242 1558 51594 33.1 | 11.682 % | c ============================================================================== c [1mFound solution: 2136[0m c ---[ 0]---> Sorter-cost: 5 Base: 5 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 1825 | 52689 130614 | 17563 1596 52210 32.7 | 11.682 % | c | 1925 | 52689 130614 | 19319 1696 54746 32.3 | 11.679 % | c | 2080 | 52689 130614 | 21251 1851 60799 32.8 | 11.679 % | c ============================================================================== c [1mFound solution: 1963[0m c ---[ 0]---> Sorter-cost: 6 Base: 5 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 2126 | 52479 130144 | 17493 1888 62844 33.3 | 11.679 % | c | 2226 | 52479 130144 | 19242 1988 64360 32.4 | 12.091 % | c | 2377 | 52479 130144 | 21166 2139 70843 33.1 | 12.091 % | c ============================================================================== c [1mFound solution: 1959[0m c ---[ 0]---> Sorter-cost: 6 Base: 5 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 2471 | 52489 130172 | 17496 2233 72955 32.7 | 12.091 % | c | 2571 | 52322 129787 | 19245 2328 74840 32.1 | 12.323 % | c | 2721 | 51285 127390 | 21170 2429 80367 33.1 | 13.717 % | c | 2947 | 50170 124809 | 23287 2621 85422 32.6 | 15.200 % | c | 3287 | 48847 121747 | 25615 2911 101992 35.0 | 16.952 % | c | 3793 | 48358 120612 | 28177 3403 113615 33.4 | 17.588 % | c ============================================================================== c [1mFound solution: 1948[0m c ---[ 0]---> Sorter-cost: 6 Base: 5 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 4119 | 48366 120631 | 16122 3729 137025 36.7 | 17.588 % | c | 4219 | 48366 120631 | 17734 3829 138803 36.3 | 17.588 % | c | 4369 | 48048 119892 | 19507 3958 145830 36.8 | 18.022 % | c | 4594 | 46695 116764 | 21458 4091 147117 36.0 | 19.828 % | c | 4932 | 46689 116746 | 23604 4428 161011 36.4 | 19.837 % | c | 5439 | 46689 116746 | 25964 4935 174660 35.4 | 19.837 % | c ============================================================================== c [1mFound solution: 1939[0m c ---[ 0]---> Sorter-cost: 4 Base: 5 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 5595 | 46694 116758 | 15564 5091 183472 36.0 | 19.837 % | c | 5695 | 46694 116758 | 17120 5191 187041 36.0 | 19.838 % | c | 5846 | 46694 116758 | 18832 5342 193524 36.2 | 19.838 % | c | 6071 | 46694 116758 | 20715 5567 199369 35.8 | 19.838 % | c ============================================================================== c [1mFound solution: 1935[0m c ---[ 0]---> Sorter-cost: 6 Base: 5 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 6244 | 46756 116908 | 15585 5740 205127 35.7 | 19.838 % | c | 6346 | 46610 116564 | 17143 5837 209713 35.9 | 20.053 % | c | 6496 | 46529 116378 | 18857 5981 213413 35.7 | 20.158 % | c | 6721 | 46529 116378 | 20743 6206 228623 36.8 | 20.158 % | c ============================================================================== c [1mFound solution: 1931[0m c ---[ 0]---> Sorter-cost: 4 Base: 5 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 6870 | 44969 112759 | 14989 6212 230635 37.1 | 20.158 % | c | 6971 | 44969 112759 | 16487 6313 236280 37.4 | 22.294 % | c | 7121 | 44539 111755 | 18136 6433 238185 37.0 | 22.870 % | c | 7348 | 44147 110835 | 19950 6616 255984 38.7 | 23.437 % | c | 7687 | 44141 110817 | 21945 6953 266703 38.4 | 23.445 % | c | 8195 | 44132 110790 | 24139 7455 285481 38.3 | 23.458 % | c ============================================================================== c [1mFound solution: 1924[0m c ---[ 0]---> Sorter-cost: 4 Base: 5 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 8652 | 43344 108952 | 14448 7850 318221 40.5 | 23.458 % | c | 8753 | 43191 108593 | 15892 7939 320098 40.3 | 24.773 % | c | 8903 | 43162 108520 | 17482 8088 328118 40.6 | 24.824 % | c | 9130 | 43162 108520 | 19230 8315 335246 40.3 | 24.824 % | c ============================================================================== c [1mFound solution: 1914[0m c ---[ 0]---> Sorter-cost: 3291 Base: 5 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 9281 | 45828 114675 | 15276 8466 342248 40.4 | 24.824 % | c | 9382 | 45828 114675 | 16803 8567 345184 40.3 | 23.183 % | c | 9532 | 45828 114675 | 18483 8717 356244 40.9 | 23.183 % | c | 9757 | 45828 114675 | 20332 8942 380246 42.5 | 23.183 % | c | 10096 | 45411 113705 | 22365 9242 389539 42.1 | 23.724 % | c | 10604 | 45101 112977 | 24602 9691 417766 43.1 | 24.120 % | c | 11364 | 45101 112977 | 27062 10451 459434 44.0 | 24.120 % | c ============================================================================== c [1mFound solution: 1909[0m c ---[ 0]---> Sorter-cost: 5 Base: 5 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 11707 | 44947 112614 | 14982 10785 486650 45.1 | 24.120 % | c | 11807 | 44926 112551 | 16480 10883 491738 45.2 | 24.394 % | c | 11958 | 44926 112551 | 18128 11034 493878 44.8 | 24.394 % | c | 12184 | 44926 112551 | 19941 11260 511699 45.4 | 24.394 % | c ============================================================================== c [1mFound solution: 1759[0m c ---[ 0]---> Sorter-cost: 3 Base: 5 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 12229 | 44945 112599 | 14981 11305 512517 45.3 | 24.394 % | c | 12332 | 44851 112382 | 16479 11400 515625 45.2 | 24.509 % | c | 12483 | 44851 112382 | 18127 11551 525382 45.5 | 24.509 % | c | 12708 | 44851 112382 | 19939 11776 530560 45.1 | 24.509 % | c | 13046 | 44847 112373 | 21933 12112 554374 45.8 | 24.513 % | c | 13553 | 44847 112373 | 24127 12619 586073 46.4 | 24.513 % | c | 14312 | 44395 111348 | 26539 13291 609205 45.8 | 25.144 % | c | 15452 | 44357 111261 | 29193 14408 672095 46.6 | 25.195 % | c | 17160 | 44357 111261 | 32113 16116 732967 45.5 | 25.195 % | c | 19724 | 44099 110658 | 35324 18624 917611 49.3 | 25.536 % | c | 23568 | 43596 109488 | 38856 22420 1217299 54.3 | 26.195 % | c ============================================================================== c [1mFound solution: 1748[0m c ---[ 0]---> Sorter-cost: 3 Base: 5 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 27185 | 43512 109291 | 14504 26028 1445048 55.5 | 26.195 % | c | 27285 | 43512 109291 | 15954 13114 718324 54.8 | 26.347 % | c | 27435 | 43512 109291 | 17549 13264 723440 54.5 | 26.347 % | c | 27662 | 43512 109291 | 19304 13491 742053 55.0 | 26.347 % | c | 28001 | 43457 109164 | 21235 13826 756100 54.7 | 26.418 % | c | 28507 | 43457 109164 | 23358 14332 788988 55.1 | 26.418 % | c | 29266 | 43457 109164 | 25694 15091 851678 56.4 | 26.418 % | c | 30405 | 43457 109164 | 28264 16230 917258 56.5 | 26.418 % | c | 32116 | 43445 109128 | 31090 17939 1028851 57.4 | 26.433 % | c | 34678 | 43445 109128 | 34199 20501 1145720 55.9 | 26.433 % | c | 38524 | 43445 109128 | 37619 24347 1331202 54.7 | 26.433 % | c ============================================================================== c [1mFound solution: 1744[0m c ---[ 0]---> Sorter-cost: 2 Base: 5 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 40084 | 43451 109141 | 14483 25907 1413810 54.6 | 26.433 % | c | 40184 | 43451 109141 | 15931 13054 485055 37.2 | 26.434 % | c | 40334 | 43451 109141 | 17524 13204 494401 37.4 | 26.434 % | c | 40560 | 43451 109141 | 19276 13430 510472 38.0 | 26.434 % | c | 40897 | 43451 109141 | 21204 13767 528771 38.4 | 26.434 % | c | 41405 | 43451 109141 | 23325 14275 562681 39.4 | 26.434 % | c | 42165 | 43451 109141 | 25657 15035 600347 39.9 | 26.434 % | c | 43307 | 43451 109141 | 28223 16177 663217 41.0 | 26.434 % | c | 45017 | 42985 108057 | 31045 17876 742191 41.5 | 27.022 % | c ============================================================================== c [1mFound solution: 1736[0m c ---[ 0]---> Sorter-cost: 2 Base: 5 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 45161 | 42991 108073 | 14330 18020 750130 41.6 | 27.022 % | c | 45261 | 42991 108073 | 15763 18120 757033 41.8 | 27.022 % | c | 45412 | 42991 108073 | 17339 18271 763489 41.8 | 27.022 % | c | 45638 | 42991 108073 | 19073 18497 771489 41.7 | 27.022 % | c | 45975 | 42991 108073 | 20980 18834 791375 42.0 | 27.022 % | c | 46481 | 42987 108064 | 23078 19337 809336 41.9 | 27.026 % | c | 47240 | 42987 108064 | 25386 20096 863745 43.0 | 27.026 % | c | 48382 | 42987 108064 | 27925 21238 943746 44.4 | 27.026 % | c ============================================================================== c [1mFound solution: 1729[0m c ---[ 0]---> Sorter-cost: 4 Base: 5 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 49754 | 42993 108079 | 14331 22610 1015698 44.9 | 27.026 % | c | 49859 | 42993 108079 | 15764 11410 419418 36.8 | 27.025 % | c | 50010 | 42993 108079 | 17340 11561 424641 36.7 | 27.025 % | c | 50235 | 42993 108079 | 19074 11786 438359 37.2 | 27.025 % | c | 50573 | 42993 108079 | 20982 12124 460647 38.0 | 27.025 % | c | 51079 | 42993 108079 | 23080 12630 483267 38.3 | 27.025 % | c | 51838 | 42993 108079 | 25388 13389 517484 38.6 | 27.025 % | c | 52980 | 42993 108079 | 27927 14531 578959 39.8 | 27.025 % | c | 54689 | 42993 108079 | 30719 16240 670254 41.3 | 27.025 % | c | 57253 | 42993 108079 | 33791 18804 805986 42.9 | 27.025 % | c | 61097 | 42993 108079 | 37170 22648 1043110 46.1 | 27.025 % | c | 66863 | 42984 108057 | 40888 28410 1338415 47.1 | 27.037 % | c | 75512 | 42921 107897 | 44976 37050 2118376 57.2 | 27.123 % | c ============================================================================== c [1mFound solution: 1721[0m c ---[ 0]---> Sorter-cost: 3 Base: 5 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 86999 | 42811 107624 | 14270 48513 2865417 59.1 | 27.123 % | c | 87099 | 42811 107624 | 15697 18350 839087 45.7 | 27.265 % | c | 87249 | 42811 107624 | 17266 18500 845161 45.7 | 27.265 % | c ============================================================================== c [1mFound solution: 1716[0m c ---[ 0]---> Sorter-cost: 4 Base: 5 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 87420 | 42818 107641 | 14272 18671 852903 45.7 | 27.265 % | c | 87522 | 42818 107641 | 15699 18773 858915 45.8 | 27.263 % | c | 87673 | 42818 107641 | 17269 18924 867102 45.8 | 27.263 % | c ============================================================================== c [1mFound solution: 1709[0m c ---[ 0]---> Sorter-cost: 3 Base: 5 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 87754 | 42824 107655 | 14274 19005 873644 46.0 | 27.263 % | c | 87854 | 42824 107655 | 15701 19105 878102 46.0 | 27.263 % | c | 88006 | 42824 107655 | 17271 19257 883087 45.9 | 27.263 % | c | 88231 | 42824 107655 | 18998 19482 899073 46.1 | 27.263 % | c | 88568 | 42824 107655 | 20898 19819 907472 45.8 | 27.263 % | c | 89074 | 42824 107655 | 22988 20325 927868 45.7 | 27.263 % | c | 89835 | 42824 107655 | 25287 21086 959351 45.5 | 27.263 % | c | 90975 | 42824 107655 | 27815 22226 1009265 45.4 | 27.263 % | c | 92683 | 42812 107619 | 30597 23931 1116385 46.7 | 27.279 % | c | 95247 | 42743 107460 | 33657 26491 1332738 50.3 | 27.365 % | c ============================================================================== c [1mFound solution: 1704[0m c ---[ 0]---> Sorter-cost: 3 Base: 5 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 97966 | 42741 107458 | 14247 29207 1573586 53.9 | 27.365 % | c | 98067 | 42501 106900 | 15671 14695 680378 46.3 | 27.689 % | c | 98221 | 42501 106900 | 17238 14849 692647 46.6 | 27.689 % | c | 98446 | 42501 106900 | 18962 15074 711042 47.2 | 27.689 % | c | 98783 | 42501 106900 | 20859 15411 737707 47.9 | 27.689 % | c | 99289 | 42501 106900 | 22944 15917 771236 48.5 | 27.689 % | c | 100049 | 42395 106656 | 25239 16670 793350 47.6 | 27.823 % | c ============================================================================== c [1mFound solution: 1694[0m c ---[ 0]---> Sorter-cost: 4 Base: 5 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 100789 | 42400 106668 | 14133 17410 820456 47.1 | 27.823 % | c | 100891 | 42316 106471 | 15546 17506 822128 47.0 | 27.941 % | c | 101041 | 42316 106471 | 17100 17656 830622 47.0 | 27.941 % | c | 101266 | 42316 106471 | 18811 17881 833523 46.6 | 27.941 % | c | 101603 | 42296 106424 | 20692 18216 854152 46.9 | 27.968 % | c | 102109 | 42296 106424 | 22761 18722 881251 47.1 | 27.968 % | c | 102869 | 42296 106424 | 25037 19482 923636 47.4 | 27.968 % | c | 104008 | 42296 106424 | 27541 20621 1002974 48.6 | 27.968 % | c | 105717 | 42201 106203 | 30295 22325 1112136 49.8 | 28.094 % | c ============================================================================== c [1mFound solution: 1691[0m c ---[ 0]---> Sorter-cost: 2 Base: 5 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 106698 | 42206 106214 | 14068 23306 1194126 51.2 | 28.094 % | c | 106800 | 42206 106214 | 15474 11755 439579 37.4 | 28.094 % | c | 106951 | 41960 105641 | 17022 11888 442183 37.2 | 28.419 % | c | 107176 | 41960 105641 | 18724 12113 454948 37.6 | 28.419 % | c | 107513 | 41960 105641 | 20596 12450 472512 38.0 | 28.419 % | c ============================================================================== c [1mFound solution: 1684[0m c ---[ 0]---> Sorter-cost: 2 Base: 5 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 107802 | 41965 105652 | 13988 12739 489211 38.4 | 28.419 % | c | 107902 | 41965 105652 | 15386 12839 496709 38.7 | 28.419 % | c | 108054 | 41959 105640 | 16925 12989 500059 38.5 | 28.427 % | c | 108283 | 41794 105269 | 18618 12922 495216 38.3 | 28.635 % | c | 108621 | 41735 105135 | 20479 13241 500692 37.8 | 28.705 % | c | 109127 | 41732 105126 | 22527 13746 535569 39.0 | 28.709 % | c | 109886 | 41732 105126 | 24780 14505 561412 38.7 | 28.709 % | c | 111025 | 41726 105108 | 27258 15643 673525 43.1 | 28.717 % | c | 112734 | 41102 103658 | 29984 17271 759767 44.0 | 29.546 % | c ============================================================================== c [1mFound solution: 1667[0m c ---[ 0]---> Sorter-cost: 6 Base: 5 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 112862 | 41147 103764 | 13715 17399 768153 44.1 | 29.546 % | c | 112962 | 41147 103764 | 15086 17499 771190 44.1 | 29.533 % | c | 113112 | 41147 103764 | 16595 17649 775472 43.9 | 29.533 % | c | 113338 | 41147 103764 | 18254 17875 782287 43.8 | 29.533 % | c | 113676 | 41125 103714 | 20080 18207 795126 43.7 | 29.564 % | c | 114182 | 41125 103714 | 22088 18713 822570 44.0 | 29.564 % | c | 114943 | 41125 103714 | 24296 19474 860623 44.2 | 29.564 % | c | 116083 | 41125 103714 | 26726 20614 921723 44.7 | 29.564 % | c ============================================================================== c [1mFound solution: 1663[0m c ---[ 0]---> Sorter-cost: 4 Base: 5 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 117182 | 41130 103725 | 13710 21713 983432 45.3 | 29.564 % | c | 117283 | 41130 103725 | 15081 10958 348621 31.8 | 29.566 % | c | 117434 | 41130 103725 | 16589 11109 350539 31.6 | 29.566 % | c | 117659 | 41130 103725 | 18248 11334 357808 31.6 | 29.566 % | c | 117996 | 40870 103125 | 20072 11654 367895 31.6 | 29.882 % | c | 118502 | 40870 103125 | 22080 12160 387551 31.9 | 29.882 % | c | 119261 | 40870 103125 | 24288 12919 408418 31.6 | 29.882 % | c ============================================================================== c [1mFound solution: 1661[0m c ---[ 0]---> Sorter-cost: 1 Base: 5 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 119511 | 40884 103161 | 13628 13169 421521 32.0 | 29.882 % | c | 119614 | 40741 102828 | 14990 13263 423078 31.9 | 30.071 % | c | 119764 | 40741 102828 | 16489 13413 428871 32.0 | 30.071 % | c | 119990 | 40741 102828 | 18138 13639 440457 32.3 | 30.071 % | c | 120329 | 40741 102828 | 19952 13978 459794 32.9 | 30.071 % | c | 120835 | 40741 102828 | 21948 14484 478929 33.1 | 30.071 % | c | 121595 | 40741 102828 | 24142 15244 512143 33.6 | 30.071 % | c | 122736 | 40741 102828 | 26557 16385 573126 35.0 | 30.071 % | c | 124444 | 40741 102828 | 29212 18093 664548 36.7 | 30.071 % | c | 127008 | 40741 102828 | 32134 20657 777134 37.6 | 30.071 % | c ============================================================================== c [1mFound solution: 1656[0m c ---[ 0]---> Sorter-cost: 2 Base: 5 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 130089 | 40745 102841 | 13581 23738 899116 37.9 | 30.071 % | c | 130192 | 40745 102841 | 14939 11972 322953 27.0 | 30.071 % | c | 130342 | 40745 102841 | 16433 12122 329170 27.2 | 30.071 % | c | 130567 | 40745 102841 | 18076 12347 333628 27.0 | 30.072 % | c | 130904 | 40745 102841 | 19883 12684 346118 27.3 | 30.072 % | c | 131412 | 40745 102841 | 21872 13192 369164 28.0 | 30.072 % | c | 132173 | 40745 102841 | 24059 13953 409035 29.3 | 30.071 % | c | 133313 | 40725 102794 | 26465 15088 439980 29.2 | 30.099 % | c | 135021 | 40715 102768 | 29112 16793 516035 30.7 | 30.114 % | c ============================================================================== c [1mFound solution: 1652[0m c ---[ 0]---> Sorter-cost: 6 Base: 5 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 135571 | 40722 102793 | 13574 17343 537198 31.0 | 30.114 % | c | 135673 | 40722 102793 | 14931 17445 543058 31.1 | 30.112 % | c | 135824 | 40722 102793 | 16424 17596 547935 31.1 | 30.112 % | c | 136051 | 40722 102793 | 18066 17823 558959 31.4 | 30.112 % | c | 136388 | 40722 102793 | 19873 18160 570744 31.4 | 30.112 % | c | 136900 | 40722 102793 | 21861 18672 606492 32.5 | 30.113 % | c | 137659 | 40722 102793 | 24047 19431 650239 33.5 | 30.112 % | c | 138801 | 40722 102793 | 26451 20573 705072 34.3 | 30.112 % | c | 140509 | 40722 102793 | 29097 22281 792761 35.6 | 30.112 % | c ============================================================================== c [1mFound solution: 1651[0m c ---[ 0]---> Sorter-cost: 3 Base: 5 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 142457 | 40716 102777 | 13572 24224 905816 37.4 | 30.112 % | c | 142557 | 40716 102777 | 14929 12212 387737 31.8 | 30.128 % | c | 142707 | 40716 102777 | 16422 12362 392691 31.8 | 30.128 % | c | 142933 | 40716 102777 | 18064 12588 399321 31.7 | 30.128 % | c | 143270 | 40716 102777 | 19870 12925 415415 32.1 | 30.128 % | c | 143776 | 40716 102777 | 21857 13431 436400 32.5 | 30.128 % | c | 144537 | 40716 102777 | 24043 14192 469687 33.1 | 30.128 % | c | 145676 | 40716 102777 | 26447 15331 521292 34.0 | 30.128 % | c ============================================================================== c [1mFound solution: 1644[0m c ---[ 0]---> Sorter-cost: 3 Base: 5 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 146892 | 40720 102787 | 13573 16547 575446 34.8 | 30.128 % | c | 146995 | 40720 102787 | 14930 16650 581097 34.9 | 30.129 % | c | 147146 | 40720 102787 | 16423 16801 582869 34.7 | 30.129 % | c | 147371 | 40720 102787 | 18065 17026 591875 34.8 | 30.129 % | c | 147712 | 40720 102787 | 19872 17367 600578 34.6 | 30.129 % | c | 148219 | 40720 102787 | 21859 17874 617502 34.5 | 30.129 % | c | 148978 | 40720 102787 | 24045 18633 648881 34.8 | 30.129 % | c | 150117 | 40720 102787 | 26449 19772 710266 35.9 | 30.129 % | c | 151825 | 40720 102787 | 29094 21480 785614 36.6 | 30.129 % | c | 154387 | 40720 102787 | 32004 24042 880535 36.6 | 30.129 % | c ============================================================================== c [1mFound solution: 1642[0m c ---[ 0]---> Sorter-cost: 5 Base: 5 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 154777 | 40726 102802 | 13575 24432 906188 37.1 | 30.129 % | c | 154877 | 40726 102802 | 14932 12316 335227 27.2 | 30.128 % | c | 155027 | 40726 102802 | 16425 12466 342339 27.5 | 30.128 % | c | 155252 | 40726 102802 | 18068 12691 355758 28.0 | 30.128 % | c | 155590 | 40726 102802 | 19875 13029 368814 28.3 | 30.128 % | c | 156099 | 40726 102802 | 21862 13538 389774 28.8 | 30.128 % | c | 156858 | 40726 102802 | 24048 14297 425274 29.7 | 30.128 % | c | 157997 | 40726 102802 | 26453 15436 460574 29.8 | 30.128 % | c | 159706 | 40726 102802 | 29099 17145 510125 29.8 | 30.128 % | c | 162272 | 40726 102802 | 32009 19711 608934 30.9 | 30.128 % | c | 166116 | 40726 102802 | 35210 23555 759486 32.2 | 30.128 % | c | 171882 | 40726 102802 | 38731 29321 1114603 38.0 | 30.128 % | c | 180531 | 40726 102802 | 42604 37970 1447309 38.1 | 30.128 % | c | 193506 | 40711 102757 | 46864 50940 2113661 41.5 | 30.148 % | c ============================================================================== c [1mFound solution: 1639[0m c ---[ 0]---> Sorter-cost: 2 Base: 5 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 195154 | 40714 102764 | 13571 52588 2224442 42.3 | 30.148 % | c | 195255 | 40714 102764 | 14928 19845 732694 36.9 | 30.149 % | c | 195408 | 40714 102764 | 16420 19998 741441 37.1 | 30.149 % | c ============================================================================== c [1mFound solution: 1631[0m c ---[ 0]---> Sorter-cost: 4 Base: 5 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 195571 | 40720 102778 | 13573 20161 748582 37.1 | 30.149 % | c | 195671 | 40720 102778 | 14930 20261 750087 37.0 | 30.148 % | c | 195821 | 40714 102764 | 16423 20408 752993 36.9 | 30.156 % | c | 196047 | 40714 102764 | 18065 20634 763296 37.0 | 30.156 % | c | 196384 | 40714 102764 | 19872 20971 786775 37.5 | 30.156 % | c | 196892 | 40714 102764 | 21859 21479 819658 38.2 | 30.156 % | c | 197652 | 40708 102746 | 24045 22238 864204 38.9 | 30.164 % | c | 198792 | 40708 102746 | 26449 23378 920169 39.4 | 30.164 % | c | 200501 | 40708 102746 | 29094 25087 1032119 41.1 | 30.164 % | c | 203063 | 40708 102746 | 32004 27649 1212199 43.8 | 30.164 % | c | 206908 | 40708 102746 | 35204 31494 1422349 45.2 | 30.164 % | c | 212675 | 40708 102746 | 38725 37261 1761049 47.3 | 30.164 % | c | 221324 | 40708 102746 | 42597 45910 2183773 47.6 | 30.164 % | c | 234298 | 40652 102615 | 46857 25366 975711 38.5 | 30.234 % | c ============================================================================== c [1mFound solution: 1623[0m c ---[ 0]---> Sorter-cost: 3 Base: 5 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 248606 | 40658 102629 | 13552 39674 2053944 51.8 | 30.234 % | c | 248706 | 40516 102298 | 14907 16548 1008096 60.9 | 30.421 % | c | 248858 | 40516 102298 | 16397 16700 1013335 60.7 | 30.421 % | c | 249083 | 40513 102289 | 18037 16923 1023539 60.5 | 30.424 % | c | 249421 | 40513 102289 | 19841 17261 1032090 59.8 | 30.424 % | c | 249928 | 40513 102289 | 21825 17768 1050100 59.1 | 30.424 % | c | 250689 | 40513 102289 | 24008 18529 1075792 58.1 | 30.424 % | c | 251829 | 40513 102289 | 26409 19669 1120189 57.0 | 30.424 % | c | 253537 | 40352 101910 | 29049 21357 1252590 58.7 | 30.647 % | c | 256100 | 40352 101910 | 31954 23920 1396669 58.4 | 30.647 % | c | 259945 | 40352 101910 | 35150 27765 1641354 59.1 | 30.647 % | c | 265711 | 40352 101910 | 38665 33531 1958634 58.4 | 30.647 % | c | 274360 | 40352 101910 | 42531 42180 2471283 58.6 | 30.647 % | c | 287334 | 40342 101886 | 46785 21232 859949 40.5 | 30.662 % |
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/12218/stat): 12218 (minisat+_script) R 12217 12218 824 0 -1 0 19 0 0 0 0 0 0 0 23 0 1 0 1785174303 712704 3 4294967295 134512640 135087896 3221224512 3221224512 1073744960 0 0 5 0 0 0 0 17 1 0 0 Raw data (/proc/12218/statm): 174 3 169 147 0 27 0 [pid=12218] 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=12219 New process pid=12220 New process pid=12221 execve syscall for /bin/sed executable One traced child (pid=12220) 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=12221) exited with status: 0 One traced child (pid=12219) exited with status: 0 New process pid=12222 execve syscall for /oldhome/oroussel/solvers/minisat+_64-bit_static executable open syscall for file /dev/null open syscall for file /oldhome/oroussel/tmp/wulflinc5/normalized-p0201.opb [startup+10.0039 s] Raw data (loadavg): 0.93 0.97 0.91 2/57 12222 Raw data (/proc/12218/stat): 12218 (minisat+_script) S 12217 12218 824 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785174303 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/12218/statm): 531 226 485 147 0 384 0 [pid=12218] vsize: 2124 Raw data (/proc/12222/stat): 12222 (minisat+_64-bit) R 12218 12218 824 0 -1 0 2240 0 0 0 979 8 0 0 25 0 1 0 1785174308 9809920 2174 4294967295 134512640 135094434 3221224448 3221223136 134554746 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/12222/statm): 2395 2174 145 145 0 2250 0 [pid=12222] vsize: 9580 Current children cumulated CPU time (s) 9.87 Current children cumulated vsize (Kb) 11704 [startup+20.0057 s] Raw data (loadavg): 0.94 0.97 0.91 2/57 12222 Raw data (/proc/12218/stat): 12218 (minisat+_script) S 12217 12218 824 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785174303 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/12218/statm): 531 226 485 147 0 384 0 [pid=12218] vsize: 2124 Raw data (/proc/12222/stat): 12222 (minisat+_64-bit) R 12218 12218 824 0 -1 0 2380 0 0 0 1976 9 0 0 25 0 1 0 1785174308 10383360 2314 4294967295 134512640 135094434 3221224448 3221223108 134553499 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/12222/statm): 2535 2314 145 145 0 2390 0 [pid=12222] vsize: 10140 Current children cumulated CPU time (s) 19.85 Current children cumulated vsize (Kb) 12264 [startup+30.0064 s] Raw data (loadavg): 0.95 0.97 0.91 2/57 12222 Raw data (/proc/12218/stat): 12218 (minisat+_script) S 12217 12218 824 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785174303 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/12218/statm): 531 226 485 147 0 384 0 [pid=12218] vsize: 2124 Raw data (/proc/12222/stat): 12222 (minisat+_64-bit) R 12218 12218 824 0 -1 0 2637 0 0 0 2972 10 0 0 25 0 1 0 1785174308 11296768 2571 4294967295 134512640 135094434 3221224448 3221223108 134553489 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/12222/statm): 2758 2571 145 145 0 2613 0 [pid=12222] vsize: 11032 Current children cumulated CPU time (s) 29.82 Current children cumulated vsize (Kb) 13156 [startup+40.0071 s] Raw data (loadavg): 0.96 0.97 0.91 2/57 12222 Raw data (/proc/12218/stat): 12218 (minisat+_script) S 12217 12218 824 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785174303 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/12218/statm): 531 226 485 147 0 384 0 [pid=12218] vsize: 2124 Raw data (/proc/12222/stat): 12222 (minisat+_64-bit) R 12218 12218 824 0 -1 0 2851 0 0 0 3969 12 0 0 25 0 1 0 1785174308 12136448 2785 4294967295 134512640 135094434 3221224448 3221223040 134557514 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/12222/statm): 2963 2785 145 145 0 2818 0 [pid=12222] vsize: 11852 Current children cumulated CPU time (s) 39.81 Current children cumulated vsize (Kb) 13976 [startup+50.0079 s] Raw data (loadavg): 0.96 0.97 0.91 2/57 12222 Raw data (/proc/12218/stat): 12218 (minisat+_script) S 12217 12218 824 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785174303 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/12218/statm): 531 226 485 147 0 384 0 [pid=12218] vsize: 2124 Raw data (/proc/12222/stat): 12222 (minisat+_64-bit) R 12218 12218 824 0 -1 0 3041 0 0 0 4965 13 0 0 25 0 1 0 1785174308 12914688 2975 4294967295 134512640 135094434 3221224448 3221223104 134557893 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/12222/statm): 3153 2975 145 145 0 3008 0 [pid=12222] vsize: 12612 Current children cumulated CPU time (s) 49.78 Current children cumulated vsize (Kb) 14736 [startup+60.0076 s] Raw data (loadavg): 0.97 0.97 0.91 2/57 12222 Raw data (/proc/12218/stat): 12218 (minisat+_script) S 12217 12218 824 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785174303 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/12218/statm): 531 226 485 147 0 384 0 [pid=12218] vsize: 2124 Raw data (/proc/12222/stat): 12222 (minisat+_64-bit) R 12218 12218 824 0 -1 0 3254 0 0 0 5962 14 0 0 25 0 1 0 1785174308 13840384 3188 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/12222/statm): 3379 3188 145 145 0 3234 0 [pid=12222] vsize: 13516 Current children cumulated CPU time (s) 59.76 Current children cumulated vsize (Kb) 15640 [startup+70.0083 s] Raw data (loadavg): 0.97 0.97 0.91 2/57 12222 Raw data (/proc/12218/stat): 12218 (minisat+_script) S 12217 12218 824 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785174303 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/12218/statm): 531 226 485 147 0 384 0 [pid=12218] vsize: 2124 Raw data (/proc/12222/stat): 12222 (minisat+_64-bit) R 12218 12218 824 0 -1 0 3514 0 0 0 6955 17 0 0 25 0 1 0 1785174308 14893056 3448 4294967295 134512640 135094434 3221224448 3221223104 134558007 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/12222/statm): 3636 3448 145 145 0 3491 0 [pid=12222] vsize: 14544 Current children cumulated CPU time (s) 69.72 Current children cumulated vsize (Kb) 16668 [startup+80.0091 s] Raw data (loadavg): 0.98 0.97 0.91 2/57 12222 Raw data (/proc/12218/stat): 12218 (minisat+_script) S 12217 12218 824 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785174303 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/12218/statm): 531 226 485 147 0 384 0 [pid=12218] vsize: 2124 Raw data (/proc/12222/stat): 12222 (minisat+_64-bit) R 12218 12218 824 0 -1 0 3731 0 0 0 7950 19 0 0 25 0 1 0 1785174308 15773696 3665 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/12222/statm): 3851 3665 145 145 0 3706 0 [pid=12222] vsize: 15404 Current children cumulated CPU time (s) 79.69 Current children cumulated vsize (Kb) 17528 [startup+90.0098 s] Raw data (loadavg): 0.98 0.97 0.91 2/57 12222 Raw data (/proc/12218/stat): 12218 (minisat+_script) S 12217 12218 824 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785174303 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/12218/statm): 531 226 485 147 0 384 0 [pid=12218] vsize: 2124 Raw data (/proc/12222/stat): 12222 (minisat+_64-bit) R 12218 12218 824 0 -1 0 3896 0 0 0 8948 20 0 0 25 0 1 0 1785174308 16441344 3830 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/12222/statm): 4014 3830 145 145 0 3869 0 [pid=12222] vsize: 16056 Current children cumulated CPU time (s) 89.68 Current children cumulated vsize (Kb) 18180 [startup+100.011 s] Raw data (loadavg): 0.98 0.97 0.91 2/57 12222 Raw data (/proc/12218/stat): 12218 (minisat+_script) S 12217 12218 824 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785174303 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/12218/statm): 531 226 485 147 0 384 0 [pid=12218] vsize: 2124 Raw data (/proc/12222/stat): 12222 (minisat+_64-bit) R 12218 12218 824 0 -1 0 3896 0 0 0 9948 20 0 0 25 0 1 0 1785174308 16441344 3830 4294967295 134512640 135094434 3221224448 3221223072 134557681 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/12222/statm): 4014 3830 145 145 0 3869 0 [pid=12222] vsize: 16056 Current children cumulated CPU time (s) 99.68 Current children cumulated vsize (Kb) 18180 [startup+110.011 s] Raw data (loadavg): 0.98 0.97 0.91 2/57 12222 Raw data (/proc/12218/stat): 12218 (minisat+_script) S 12217 12218 824 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785174303 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/12218/statm): 531 226 485 147 0 384 0 [pid=12218] vsize: 2124 Raw data (/proc/12222/stat): 12222 (minisat+_64-bit) R 12218 12218 824 0 -1 0 3896 0 0 0 10949 20 0 0 25 0 1 0 1785174308 16441344 3830 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/12222/statm): 4014 3830 145 145 0 3869 0 [pid=12222] vsize: 16056 Current children cumulated CPU time (s) 109.69 Current children cumulated vsize (Kb) 18180 [startup+120.012 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 12222 Raw data (/proc/12218/stat): 12218 (minisat+_script) S 12217 12218 824 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785174303 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/12218/statm): 531 226 485 147 0 384 0 [pid=12218] vsize: 2124 Raw data (/proc/12222/stat): 12222 (minisat+_64-bit) R 12218 12218 824 0 -1 0 3896 0 0 0 11949 20 0 0 25 0 1 0 1785174308 16441344 3830 4294967295 134512640 135094434 3221224448 3221223100 134558255 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/12222/statm): 4014 3830 145 145 0 3869 0 [pid=12222] vsize: 16056 Current children cumulated CPU time (s) 119.69 Current children cumulated vsize (Kb) 18180 [startup+130.012 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 12222 Raw data (/proc/12218/stat): 12218 (minisat+_script) S 12217 12218 824 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785174303 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/12218/statm): 531 226 485 147 0 384 0 [pid=12218] vsize: 2124 Raw data (/proc/12222/stat): 12222 (minisat+_64-bit) R 12218 12218 824 0 -1 0 3896 0 0 0 12949 20 0 0 25 0 1 0 1785174308 16441344 3830 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/12222/statm): 4014 3830 145 145 0 3869 0 [pid=12222] vsize: 16056 Current children cumulated CPU time (s) 129.69 Current children cumulated vsize (Kb) 18180 [startup+140.014 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 12222 Raw data (/proc/12218/stat): 12218 (minisat+_script) S 12217 12218 824 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785174303 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/12218/statm): 531 226 485 147 0 384 0 [pid=12218] vsize: 2124 Raw data (/proc/12222/stat): 12222 (minisat+_64-bit) R 12218 12218 824 0 -1 0 3938 0 0 0 13949 20 0 0 25 0 1 0 1785174308 16613376 3872 4294967295 134512640 135094434 3221224448 3221223084 134557560 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/12222/statm): 4056 3872 145 145 0 3911 0 [pid=12222] vsize: 16224 Current children cumulated CPU time (s) 139.69 Current children cumulated vsize (Kb) 18348 [startup+150.014 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 12222 Raw data (/proc/12218/stat): 12218 (minisat+_script) S 12217 12218 824 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785174303 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/12218/statm): 531 226 485 147 0 384 0 [pid=12218] vsize: 2124 Raw data (/proc/12222/stat): 12222 (minisat+_64-bit) R 12218 12218 824 0 -1 0 3938 0 0 0 14949 20 0 0 25 0 1 0 1785174308 16613376 3872 4294967295 134512640 135094434 3221224448 3221223040 134557230 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/12222/statm): 4056 3872 145 145 0 3911 0 [pid=12222] vsize: 16224 Current children cumulated CPU time (s) 149.69 Current children cumulated vsize (Kb) 18348 [startup+160.014 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 12222 Raw data (/proc/12218/stat): 12218 (minisat+_script) S 12217 12218 824 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785174303 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/12218/statm): 531 226 485 147 0 384 0 [pid=12218] vsize: 2124 Raw data (/proc/12222/stat): 12222 (minisat+_64-bit) R 12218 12218 824 0 -1 0 3938 0 0 0 15949 20 0 0 25 0 1 0 1785174308 16613376 3872 4294967295 134512640 135094434 3221224448 3221223104 134558284 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/12222/statm): 4056 3872 145 145 0 3911 0 [pid=12222] vsize: 16224 Current children cumulated CPU time (s) 159.69 Current children cumulated vsize (Kb) 18348 [startup+170.016 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 12222 Raw data (/proc/12218/stat): 12218 (minisat+_script) S 12217 12218 824 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785174303 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/12218/statm): 531 226 485 147 0 384 0 [pid=12218] vsize: 2124 Raw data (/proc/12222/stat): 12222 (minisat+_64-bit) R 12218 12218 824 0 -1 0 3938 0 0 0 16949 20 0 0 25 0 1 0 1785174308 16613376 3872 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/12222/statm): 4056 3872 145 145 0 3911 0 [pid=12222] vsize: 16224 Current children cumulated CPU time (s) 169.69 Current children cumulated vsize (Kb) 18348 [startup+180.016 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 12222 Raw data (/proc/12218/stat): 12218 (minisat+_script) S 12217 12218 824 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785174303 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/12218/statm): 531 226 485 147 0 384 0 [pid=12218] vsize: 2124 Raw data (/proc/12222/stat): 12222 (minisat+_64-bit) R 12218 12218 824 0 -1 0 3948 0 0 0 17949 20 0 0 25 0 1 0 1785174308 16654336 3882 4294967295 134512640 135094434 3221224448 3221223040 134557230 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/12222/statm): 4066 3882 145 145 0 3921 0 [pid=12222] vsize: 16264 Current children cumulated CPU time (s) 179.69 Current children cumulated vsize (Kb) 18388 [startup+190.017 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 12222 Raw data (/proc/12218/stat): 12218 (minisat+_script) S 12217 12218 824 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785174303 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/12218/statm): 531 226 485 147 0 384 0 [pid=12218] vsize: 2124 Raw data (/proc/12222/stat): 12222 (minisat+_64-bit) R 12218 12218 824 0 -1 0 3948 0 0 0 18950 20 0 0 25 0 1 0 1785174308 16654336 3882 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/12222/statm): 4066 3882 145 145 0 3921 0 [pid=12222] vsize: 16264 Current children cumulated CPU time (s) 189.7 Current children cumulated vsize (Kb) 18388 [startup+200.018 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 12222 Raw data (/proc/12218/stat): 12218 (minisat+_script) S 12217 12218 824 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785174303 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/12218/statm): 531 226 485 147 0 384 0 [pid=12218] vsize: 2124 Raw data (/proc/12222/stat): 12222 (minisat+_64-bit) R 12218 12218 824 0 -1 0 3948 0 0 0 19950 20 0 0 25 0 1 0 1785174308 16654336 3882 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/12222/statm): 4066 3882 145 145 0 3921 0 [pid=12222] vsize: 16264 Current children cumulated CPU time (s) 199.7 Current children cumulated vsize (Kb) 18388 [startup+210.019 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 12222 Raw data (/proc/12218/stat): 12218 (minisat+_script) S 12217 12218 824 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785174303 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/12218/statm): 531 226 485 147 0 384 0 [pid=12218] vsize: 2124 Raw data (/proc/12222/stat): 12222 (minisat+_64-bit) R 12218 12218 824 0 -1 0 3948 0 0 0 20950 20 0 0 25 0 1 0 1785174308 16654336 3882 4294967295 134512640 135094434 3221224448 3221223076 134557564 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/12222/statm): 4066 3882 145 145 0 3921 0 [pid=12222] vsize: 16264 Current children cumulated CPU time (s) 209.7 Current children cumulated vsize (Kb) 18388 [startup+220.019 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 12222 Raw data (/proc/12218/stat): 12218 (minisat+_script) S 12217 12218 824 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785174303 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/12218/statm): 531 226 485 147 0 384 0 [pid=12218] vsize: 2124 Raw data (/proc/12222/stat): 12222 (minisat+_64-bit) R 12218 12218 824 0 -1 0 3948 0 0 0 21950 20 0 0 25 0 1 0 1785174308 16654336 3882 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/12222/statm): 4066 3882 145 145 0 3921 0 [pid=12222] vsize: 16264 Current children cumulated CPU time (s) 219.7 Current children cumulated vsize (Kb) 18388 [startup+230.02 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 12222 Raw data (/proc/12218/stat): 12218 (minisat+_script) S 12217 12218 824 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785174303 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/12218/statm): 531 226 485 147 0 384 0 [pid=12218] vsize: 2124 Raw data (/proc/12222/stat): 12222 (minisat+_64-bit) R 12218 12218 824 0 -1 0 3948 0 0 0 22951 20 0 0 25 0 1 0 1785174308 16654336 3882 4294967295 134512640 135094434 3221224448 3221223072 134557648 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/12222/statm): 4066 3882 145 145 0 3921 0 [pid=12222] vsize: 16264 Current children cumulated CPU time (s) 229.71 Current children cumulated vsize (Kb) 18388 [startup+240.022 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 12222 Raw data (/proc/12218/stat): 12218 (minisat+_script) S 12217 12218 824 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785174303 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/12218/statm): 531 226 485 147 0 384 0 [pid=12218] vsize: 2124 Raw data (/proc/12222/stat): 12222 (minisat+_64-bit) R 12218 12218 824 0 -1 0 3950 0 0 0 23951 20 0 0 25 0 1 0 1785174308 16654336 3884 4294967295 134512640 135094434 3221224448 3221223104 134558187 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/12222/statm): 4066 3884 145 145 0 3921 0 [pid=12222] vsize: 16264 Current children cumulated CPU time (s) 239.71 Current children cumulated vsize (Kb) 18388 [startup+250.023 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 12222 Raw data (/proc/12218/stat): 12218 (minisat+_script) S 12217 12218 824 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785174303 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/12218/statm): 531 226 485 147 0 384 0 [pid=12218] vsize: 2124 Raw data (/proc/12222/stat): 12222 (minisat+_64-bit) R 12218 12218 824 0 -1 0 4064 0 0 0 24949 21 0 0 25 0 1 0 1785174308 17113088 3998 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/12222/statm): 4178 3998 145 145 0 4033 0 [pid=12222] vsize: 16712 Current children cumulated CPU time (s) 249.7 Current children cumulated vsize (Kb) 18836 [startup+260.023 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 12222 Raw data (/proc/12218/stat): 12218 (minisat+_script) S 12217 12218 824 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785174303 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/12218/statm): 531 226 485 147 0 384 0 [pid=12218] vsize: 2124 Raw data (/proc/12222/stat): 12222 (minisat+_64-bit) R 12218 12218 824 0 -1 0 4297 0 0 0 25944 23 0 0 25 0 1 0 1785174308 18059264 4231 4294967295 134512640 135094434 3221224448 3221223040 134557044 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/12222/statm): 4409 4231 145 145 0 4264 0 [pid=12222] vsize: 17636 Current children cumulated CPU time (s) 259.67 Current children cumulated vsize (Kb) 19760 [startup+270.024 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 12222 Raw data (/proc/12218/stat): 12218 (minisat+_script) S 12217 12218 824 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785174303 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/12218/statm): 531 226 485 147 0 384 0 [pid=12218] vsize: 2124 Raw data (/proc/12222/stat): 12222 (minisat+_64-bit) R 12218 12218 824 0 -1 0 4530 0 0 0 26941 24 0 0 25 0 1 0 1785174308 19140608 4464 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/12222/statm): 4673 4464 145 145 0 4528 0 [pid=12222] vsize: 18692 Current children cumulated CPU time (s) 269.65 Current children cumulated vsize (Kb) 20816 [startup+280.025 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 12222 Raw data (/proc/12218/stat): 12218 (minisat+_script) S 12217 12218 824 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785174303 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/12218/statm): 531 226 485 147 0 384 0 [pid=12218] vsize: 2124 Raw data (/proc/12222/stat): 12222 (minisat+_64-bit) T 12218 12218 824 0 -1 0 4740 0 0 0 27938 26 0 0 25 0 1 0 1785174308 19992576 4674 4294967295 134512640 135094434 3221224448 3221222812 134870330 0 0 5 16386 3222434794 0 0 17 0 0 0 Raw data (/proc/12222/statm): 4881 4674 145 145 0 4736 0 [pid=12222] vsize: 19524 Current children cumulated CPU time (s) 279.64 Current children cumulated vsize (Kb) 21648 [startup+290.027 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 12222 Raw data (/proc/12218/stat): 12218 (minisat+_script) S 12217 12218 824 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785174303 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/12218/statm): 531 226 485 147 0 384 0 [pid=12218] vsize: 2124 Raw data (/proc/12222/stat): 12222 (minisat+_64-bit) R 12218 12218 824 0 -1 0 4921 0 0 0 28935 28 0 0 25 0 1 0 1785174308 20750336 4855 4294967295 134512640 135094434 3221224448 3221223104 134558159 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/12222/statm): 5066 4855 145 145 0 4921 0 [pid=12222] vsize: 20264 Current children cumulated CPU time (s) 289.63 Current children cumulated vsize (Kb) 22388 [startup+300.027 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 12222 Raw data (/proc/12218/stat): 12218 (minisat+_script) S 12217 12218 824 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785174303 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/12218/statm): 531 226 485 147 0 384 0 [pid=12218] vsize: 2124 Raw data (/proc/12222/stat): 12222 (minisat+_64-bit) R 12218 12218 824 0 -1 0 5095 0 0 0 29932 29 0 0 25 0 1 0 1785174308 21454848 5029 4294967295 134512640 135094434 3221224448 3221223040 134557180 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/12222/statm): 5238 5029 145 145 0 5093 0 [pid=12222] vsize: 20952 Current children cumulated CPU time (s) 299.61 Current children cumulated vsize (Kb) 23076 [startup+310.028 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 12222 Raw data (/proc/12218/stat): 12218 (minisat+_script) S 12217 12218 824 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785174303 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/12218/statm): 531 226 485 147 0 384 0 [pid=12218] vsize: 2124 Raw data (/proc/12222/stat): 12222 (minisat+_64-bit) R 12218 12218 824 0 -1 0 5230 0 0 0 30930 30 0 0 25 0 1 0 1785174308 21995520 5164 4294967295 134512640 135094434 3221224448 3221223072 134562068 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/12222/statm): 5370 5164 145 145 0 5225 0 [pid=12222] vsize: 21480 Current children cumulated CPU time (s) 309.6 Current children cumulated vsize (Kb) 23604 [startup+320.029 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 12222 Raw data (/proc/12218/stat): 12218 (minisat+_script) S 12217 12218 824 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785174303 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/12218/statm): 531 226 485 147 0 384 0 [pid=12218] vsize: 2124 Raw data (/proc/12222/stat): 12222 (minisat+_64-bit) R 12218 12218 824 0 -1 0 5347 0 0 0 31928 31 0 0 25 0 1 0 1785174308 22478848 5281 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/12222/statm): 5488 5281 145 145 0 5343 0 [pid=12222] vsize: 21952 Current children cumulated CPU time (s) 319.59 Current children cumulated vsize (Kb) 24076 [startup+330.03 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 12222 Raw data (/proc/12218/stat): 12218 (minisat+_script) S 12217 12218 824 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785174303 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/12218/statm): 531 226 485 147 0 384 0 [pid=12218] vsize: 2124 Raw data (/proc/12222/stat): 12222 (minisat+_64-bit) R 12218 12218 824 0 -1 0 5485 0 0 0 32926 32 0 0 25 0 1 0 1785174308 23040000 5419 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/12222/statm): 5625 5419 145 145 0 5480 0 [pid=12222] vsize: 22500 Current children cumulated CPU time (s) 329.58 Current children cumulated vsize (Kb) 24624 [startup+340.03 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 12222 Raw data (/proc/12218/stat): 12218 (minisat+_script) S 12217 12218 824 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785174303 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/12218/statm): 531 226 485 147 0 384 0 [pid=12218] vsize: 2124 Raw data (/proc/12222/stat): 12222 (minisat+_64-bit) R 12218 12218 824 0 -1 0 5649 0 0 0 33923 33 0 0 25 0 1 0 1785174308 23703552 5583 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/12222/statm): 5787 5583 145 145 0 5642 0 [pid=12222] vsize: 23148 Current children cumulated CPU time (s) 339.56 Current children cumulated vsize (Kb) 25272 [startup+350.031 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 12222 Raw data (/proc/12218/stat): 12218 (minisat+_script) S 12217 12218 824 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785174303 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/12218/statm): 531 226 485 147 0 384 0 [pid=12218] vsize: 2124 Raw data (/proc/12222/stat): 12222 (minisat+_64-bit) R 12218 12218 824 0 -1 0 5649 0 0 0 34923 33 0 0 25 0 1 0 1785174308 23703552 5583 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/12222/statm): 5787 5583 145 145 0 5642 0 [pid=12222] vsize: 23148 Current children cumulated CPU time (s) 349.56 Current children cumulated vsize (Kb) 25272 [startup+360.032 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 12222 Raw data (/proc/12218/stat): 12218 (minisat+_script) S 12217 12218 824 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785174303 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/12218/statm): 531 226 485 147 0 384 0 [pid=12218] vsize: 2124 Raw data (/proc/12222/stat): 12222 (minisat+_64-bit) R 12218 12218 824 0 -1 0 5649 0 0 0 35923 33 0 0 25 0 1 0 1785174308 23703552 5583 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/12222/statm): 5787 5583 145 145 0 5642 0 [pid=12222] vsize: 23148 Current children cumulated CPU time (s) 359.56 Current children cumulated vsize (Kb) 25272 [startup+370.033 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 12222 Raw data (/proc/12218/stat): 12218 (minisat+_script) S 12217 12218 824 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785174303 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/12218/statm): 531 226 485 147 0 384 0 [pid=12218] vsize: 2124 Raw data (/proc/12222/stat): 12222 (minisat+_64-bit) R 12218 12218 824 0 -1 0 5649 0 0 0 36922 33 0 0 25 0 1 0 1785174308 23703552 5583 4294967295 134512640 135094434 3221224448 3221223040 134557416 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/12222/statm): 5787 5583 145 145 0 5642 0 [pid=12222] vsize: 23148 Current children cumulated CPU time (s) 369.55 Current children cumulated vsize (Kb) 25272 [startup+380.033 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 12222 Raw data (/proc/12218/stat): 12218 (minisat+_script) S 12217 12218 824 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785174303 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/12218/statm): 531 226 485 147 0 384 0 [pid=12218] vsize: 2124 Raw data (/proc/12222/stat): 12222 (minisat+_64-bit) R 12218 12218 824 0 -1 0 5649 0 0 0 37923 33 0 0 25 0 1 0 1785174308 23703552 5583 4294967295 134512640 135094434 3221224448 3221223072 134557737 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/12222/statm): 5787 5583 145 145 0 5642 0 [pid=12222] vsize: 23148 Current children cumulated CPU time (s) 379.56 Current children cumulated vsize (Kb) 25272 [startup+390.034 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 12222 Raw data (/proc/12218/stat): 12218 (minisat+_script) S 12217 12218 824 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785174303 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/12218/statm): 531 226 485 147 0 384 0 [pid=12218] vsize: 2124 Raw data (/proc/12222/stat): 12222 (minisat+_64-bit) R 12218 12218 824 0 -1 0 5649 0 0 0 38923 33 0 0 25 0 1 0 1785174308 23703552 5583 4294967295 134512640 135094434 3221224448 3221223072 134557737 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/12222/statm): 5787 5583 145 145 0 5642 0 [pid=12222] vsize: 23148 Current children cumulated CPU time (s) 389.56 Current children cumulated vsize (Kb) 25272 [startup+400.035 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 12222 Raw data (/proc/12218/stat): 12218 (minisat+_script) S 12217 12218 824 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785174303 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/12218/statm): 531 226 485 147 0 384 0 [pid=12218] vsize: 2124 Raw data (/proc/12222/stat): 12222 (minisat+_64-bit) R 12218 12218 824 0 -1 0 5649 0 0 0 39923 34 0 0 25 0 1 0 1785174308 23703552 5583 4294967295 134512640 135094434 3221224448 3221223136 134554746 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/12222/statm): 5787 5583 145 145 0 5642 0 [pid=12222] vsize: 23148 Current children cumulated CPU time (s) 399.57 Current children cumulated vsize (Kb) 25272 [startup+410.035 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 12222 Raw data (/proc/12218/stat): 12218 (minisat+_script) S 12217 12218 824 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785174303 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/12218/statm): 531 226 485 147 0 384 0 [pid=12218] vsize: 2124 Raw data (/proc/12222/stat): 12222 (minisat+_64-bit) R 12218 12218 824 0 -1 0 5649 0 0 0 40923 34 0 0 25 0 1 0 1785174308 23703552 5583 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/12222/statm): 5787 5583 145 145 0 5642 0 [pid=12222] vsize: 23148 Current children cumulated CPU time (s) 409.57 Current children cumulated vsize (Kb) 25272 [startup+420.037 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 12222 Raw data (/proc/12218/stat): 12218 (minisat+_script) S 12217 12218 824 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785174303 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/12218/statm): 531 226 485 147 0 384 0 [pid=12218] vsize: 2124 Raw data (/proc/12222/stat): 12222 (minisat+_64-bit) R 12218 12218 824 0 -1 0 5649 0 0 0 41923 34 0 0 25 0 1 0 1785174308 23703552 5583 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/12222/statm): 5787 5583 145 145 0 5642 0 [pid=12222] vsize: 23148 Current children cumulated CPU time (s) 419.57 Current children cumulated vsize (Kb) 25272 [startup+430.038 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 12222 Raw data (/proc/12218/stat): 12218 (minisat+_script) S 12217 12218 824 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785174303 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/12218/statm): 531 226 485 147 0 384 0 [pid=12218] vsize: 2124 Raw data (/proc/12222/stat): 12222 (minisat+_64-bit) R 12218 12218 824 0 -1 0 5649 0 0 0 42923 34 0 0 25 0 1 0 1785174308 23703552 5583 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/12222/statm): 5787 5583 145 145 0 5642 0 [pid=12222] vsize: 23148 Current children cumulated CPU time (s) 429.57 Current children cumulated vsize (Kb) 25272 [startup+440.039 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 12222 Raw data (/proc/12218/stat): 12218 (minisat+_script) S 12217 12218 824 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785174303 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/12218/statm): 531 226 485 147 0 384 0 [pid=12218] vsize: 2124 Raw data (/proc/12222/stat): 12222 (minisat+_64-bit) R 12218 12218 824 0 -1 0 5649 0 0 0 43924 34 0 0 25 0 1 0 1785174308 23703552 5583 4294967295 134512640 135094434 3221224448 3221223136 134554731 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/12222/statm): 5787 5583 145 145 0 5642 0 [pid=12222] vsize: 23148 Current children cumulated CPU time (s) 439.58 Current children cumulated vsize (Kb) 25272 [startup+450.039 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 12222 Raw data (/proc/12218/stat): 12218 (minisat+_script) S 12217 12218 824 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785174303 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/12218/statm): 531 226 485 147 0 384 0 [pid=12218] vsize: 2124 Raw data (/proc/12222/stat): 12222 (minisat+_64-bit) R 12218 12218 824 0 -1 0 5649 0 0 0 44924 34 0 0 25 0 1 0 1785174308 23703552 5583 4294967295 134512640 135094434 3221224448 3221223104 134557884 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/12222/statm): 5787 5583 145 145 0 5642 0 [pid=12222] vsize: 23148 Current children cumulated CPU time (s) 449.58 Current children cumulated vsize (Kb) 25272 [startup+460.04 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 12222 Raw data (/proc/12218/stat): 12218 (minisat+_script) S 12217 12218 824 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785174303 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/12218/statm): 531 226 485 147 0 384 0 [pid=12218] vsize: 2124 Raw data (/proc/12222/stat): 12222 (minisat+_64-bit) R 12218 12218 824 0 -1 0 5651 0 0 0 45924 34 0 0 25 0 1 0 1785174308 23703552 5585 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/12222/statm): 5787 5585 145 145 0 5642 0 [pid=12222] vsize: 23148 Current children cumulated CPU time (s) 459.58 Current children cumulated vsize (Kb) 25272 [startup+470.041 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 12222 Raw data (/proc/12218/stat): 12218 (minisat+_script) S 12217 12218 824 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785174303 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/12218/statm): 531 226 485 147 0 384 0 [pid=12218] vsize: 2124 Raw data (/proc/12222/stat): 12222 (minisat+_64-bit) R 12218 12218 824 0 -1 0 5651 0 0 0 46924 34 0 0 25 0 1 0 1785174308 23703552 5585 4294967295 134512640 135094434 3221224448 3221223104 134558227 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/12222/statm): 5787 5585 145 145 0 5642 0 [pid=12222] vsize: 23148 Current children cumulated CPU time (s) 469.58 Current children cumulated vsize (Kb) 25272 [startup+480.042 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 12222 Raw data (/proc/12218/stat): 12218 (minisat+_script) S 12217 12218 824 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785174303 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/12218/statm): 531 226 485 147 0 384 0 [pid=12218] vsize: 2124 Raw data (/proc/12222/stat): 12222 (minisat+_64-bit) R 12218 12218 824 0 -1 0 5651 0 0 0 47924 34 0 0 25 0 1 0 1785174308 23703552 5585 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/12222/statm): 5787 5585 145 145 0 5642 0 [pid=12222] vsize: 23148 Current children cumulated CPU time (s) 479.58 Current children cumulated vsize (Kb) 25272 [startup+490.043 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 12222 Raw data (/proc/12218/stat): 12218 (minisat+_script) S 12217 12218 824 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785174303 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/12218/statm): 531 226 485 147 0 384 0 [pid=12218] vsize: 2124 Raw data (/proc/12222/stat): 12222 (minisat+_64-bit) R 12218 12218 824 0 -1 0 5651 0 0 0 48924 34 0 0 25 0 1 0 1785174308 23703552 5585 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/12222/statm): 5787 5585 145 145 0 5642 0 [pid=12222] vsize: 23148 Current children cumulated CPU time (s) 489.58 Current children cumulated vsize (Kb) 25272 [startup+500.044 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 12222 Raw data (/proc/12218/stat): 12218 (minisat+_script) S 12217 12218 824 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785174303 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/12218/statm): 531 226 485 147 0 384 0 [pid=12218] vsize: 2124 Raw data (/proc/12222/stat): 12222 (minisat+_64-bit) R 12218 12218 824 0 -1 0 5652 0 0 0 49924 34 0 0 25 0 1 0 1785174308 23703552 5586 4294967295 134512640 135094434 3221224448 3221223072 134557650 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/12222/statm): 5787 5586 145 145 0 5642 0 [pid=12222] vsize: 23148 Current children cumulated CPU time (s) 499.58 Current children cumulated vsize (Kb) 25272 [startup+510.044 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 12222 Raw data (/proc/12218/stat): 12218 (minisat+_script) S 12217 12218 824 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785174303 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/12218/statm): 531 226 485 147 0 384 0 [pid=12218] vsize: 2124 Raw data (/proc/12222/stat): 12222 (minisat+_64-bit) R 12218 12218 824 0 -1 0 5652 0 0 0 50924 34 0 0 25 0 1 0 1785174308 23703552 5586 4294967295 134512640 135094434 3221224448 3221223104 134561460 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/12222/statm): 5787 5586 145 145 0 5642 0 [pid=12222] vsize: 23148 Current children cumulated CPU time (s) 509.58 Current children cumulated vsize (Kb) 25272 [startup+520.046 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 12222 Raw data (/proc/12218/stat): 12218 (minisat+_script) S 12217 12218 824 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785174303 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/12218/statm): 531 226 485 147 0 384 0 [pid=12218] vsize: 2124 Raw data (/proc/12222/stat): 12222 (minisat+_64-bit) R 12218 12218 824 0 -1 0 5652 0 0 0 51924 35 0 0 25 0 1 0 1785174308 23703552 5586 4294967295 134512640 135094434 3221224448 3221223120 134556410 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/12222/statm): 5787 5586 145 145 0 5642 0 [pid=12222] vsize: 23148 Current children cumulated CPU time (s) 519.59 Current children cumulated vsize (Kb) 25272 [startup+530.046 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 12222 Raw data (/proc/12218/stat): 12218 (minisat+_script) S 12217 12218 824 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785174303 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/12218/statm): 531 226 485 147 0 384 0 [pid=12218] vsize: 2124 Raw data (/proc/12222/stat): 12222 (minisat+_64-bit) R 12218 12218 824 0 -1 0 5652 0 0 0 52924 35 0 0 25 0 1 0 1785174308 23703552 5586 4294967295 134512640 135094434 3221224448 3221223072 134557737 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/12222/statm): 5787 5586 145 145 0 5642 0 [pid=12222] vsize: 23148 Current children cumulated CPU time (s) 529.59 Current children cumulated vsize (Kb) 25272 [startup+540.047 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 12222 Raw data (/proc/12218/stat): 12218 (minisat+_script) S 12217 12218 824 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785174303 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/12218/statm): 531 226 485 147 0 384 0 [pid=12218] vsize: 2124 Raw data (/proc/12222/stat): 12222 (minisat+_64-bit) R 12218 12218 824 0 -1 0 5652 0 0 0 53925 35 0 0 25 0 1 0 1785174308 23703552 5586 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/12222/statm): 5787 5586 145 145 0 5642 0 [pid=12222] vsize: 23148 Current children cumulated CPU time (s) 539.6 Current children cumulated vsize (Kb) 25272 [startup+550.048 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 12222 Raw data (/proc/12218/stat): 12218 (minisat+_script) S 12217 12218 824 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785174303 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/12218/statm): 531 226 485 147 0 384 0 [pid=12218] vsize: 2124 Raw data (/proc/12222/stat): 12222 (minisat+_64-bit) R 12218 12218 824 0 -1 0 5652 0 0 0 54925 35 0 0 25 0 1 0 1785174308 23703552 5586 4294967295 134512640 135094434 3221224448 3221223104 134558249 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/12222/statm): 5787 5586 145 145 0 5642 0 [pid=12222] vsize: 23148 Current children cumulated CPU time (s) 549.6 Current children cumulated vsize (Kb) 25272 [startup+560.049 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 12222 Raw data (/proc/12218/stat): 12218 (minisat+_script) S 12217 12218 824 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785174303 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/12218/statm): 531 226 485 147 0 384 0 [pid=12218] vsize: 2124 Raw data (/proc/12222/stat): 12222 (minisat+_64-bit) R 12218 12218 824 0 -1 0 5652 0 0 0 55925 35 0 0 25 0 1 0 1785174308 23703552 5586 4294967295 134512640 135094434 3221224448 3221223120 134556410 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/12222/statm): 5787 5586 145 145 0 5642 0 [pid=12222] vsize: 23148 Current children cumulated CPU time (s) 559.6 Current children cumulated vsize (Kb) 25272 [startup+570.049 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 12222 Raw data (/proc/12218/stat): 12218 (minisat+_script) S 12217 12218 824 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785174303 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/12218/statm): 531 226 485 147 0 384 0 [pid=12218] vsize: 2124 Raw data (/proc/12222/stat): 12222 (minisat+_64-bit) R 12218 12218 824 0 -1 0 5652 0 0 0 56925 35 0 0 25 0 1 0 1785174308 23703552 5586 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/12222/statm): 5787 5586 145 145 0 5642 0 [pid=12222] vsize: 23148 Current children cumulated CPU time (s) 569.6 Current children cumulated vsize (Kb) 25272 [startup+580.05 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 12222 Raw data (/proc/12218/stat): 12218 (minisat+_script) S 12217 12218 824 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785174303 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/12218/statm): 531 226 485 147 0 384 0 [pid=12218] vsize: 2124 Raw data (/proc/12222/stat): 12222 (minisat+_64-bit) R 12218 12218 824 0 -1 0 5652 0 0 0 57925 35 0 0 25 0 1 0 1785174308 23703552 5586 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/12222/statm): 5787 5586 145 145 0 5642 0 [pid=12222] vsize: 23148 Current children cumulated CPU time (s) 579.6 Current children cumulated vsize (Kb) 25272 [startup+590.052 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 12222 Raw data (/proc/12218/stat): 12218 (minisat+_script) S 12217 12218 824 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785174303 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/12218/statm): 531 226 485 147 0 384 0 [pid=12218] vsize: 2124 Raw data (/proc/12222/stat): 12222 (minisat+_64-bit) R 12218 12218 824 0 -1 0 5652 0 0 0 58925 35 0 0 25 0 1 0 1785174308 23703552 5586 4294967295 134512640 135094434 3221224448 3221223040 134557334 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/12222/statm): 5787 5586 145 145 0 5642 0 [pid=12222] vsize: 23148 Current children cumulated CPU time (s) 589.6 Current children cumulated vsize (Kb) 25272 [startup+600.053 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 12222 Raw data (/proc/12218/stat): 12218 (minisat+_script) S 12217 12218 824 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785174303 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/12218/statm): 531 226 485 147 0 384 0 [pid=12218] vsize: 2124 Raw data (/proc/12222/stat): 12222 (minisat+_64-bit) R 12218 12218 824 0 -1 0 5652 0 0 0 59926 35 0 0 25 0 1 0 1785174308 23703552 5586 4294967295 134512640 135094434 3221224448 3221223120 134556487 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/12222/statm): 5787 5586 145 145 0 5642 0 [pid=12222] vsize: 23148 Current children cumulated CPU time (s) 599.61 Current children cumulated vsize (Kb) 25272 [startup+610.053 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 12222 Raw data (/proc/12218/stat): 12218 (minisat+_script) S 12217 12218 824 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785174303 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/12218/statm): 531 226 485 147 0 384 0 [pid=12218] vsize: 2124 Raw data (/proc/12222/stat): 12222 (minisat+_64-bit) R 12218 12218 824 0 -1 0 5652 0 0 0 60926 35 0 0 25 0 1 0 1785174308 23703552 5586 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/12222/statm): 5787 5586 145 145 0 5642 0 [pid=12222] vsize: 23148 Current children cumulated CPU time (s) 609.61 Current children cumulated vsize (Kb) 25272 [startup+620.054 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 12222 Raw data (/proc/12218/stat): 12218 (minisat+_script) S 12217 12218 824 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785174303 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/12218/statm): 531 226 485 147 0 384 0 [pid=12218] vsize: 2124 Raw data (/proc/12222/stat): 12222 (minisat+_64-bit) R 12218 12218 824 0 -1 0 5652 0 0 0 61926 35 0 0 25 0 1 0 1785174308 23703552 5586 4294967295 134512640 135094434 3221224448 3221223120 134556266 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/12222/statm): 5787 5586 145 145 0 5642 0 [pid=12222] vsize: 23148 Current children cumulated CPU time (s) 619.61 Current children cumulated vsize (Kb) 25272 [startup+630.055 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 12222 Raw data (/proc/12218/stat): 12218 (minisat+_script) S 12217 12218 824 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785174303 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/12218/statm): 531 226 485 147 0 384 0 [pid=12218] vsize: 2124 Raw data (/proc/12222/stat): 12222 (minisat+_64-bit) R 12218 12218 824 0 -1 0 5652 0 0 0 62926 35 0 0 25 0 1 0 1785174308 23703552 5586 4294967295 134512640 135094434 3221224448 3221223120 134556410 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/12222/statm): 5787 5586 145 145 0 5642 0 [pid=12222] vsize: 23148 Current children cumulated CPU time (s) 629.61 Current children cumulated vsize (Kb) 25272 [startup+640.056 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 12222 Raw data (/proc/12218/stat): 12218 (minisat+_script) S 12217 12218 824 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785174303 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/12218/statm): 531 226 485 147 0 384 0 [pid=12218] vsize: 2124 Raw data (/proc/12222/stat): 12222 (minisat+_64-bit) R 12218 12218 824 0 -1 0 5652 0 0 0 63927 35 0 0 25 0 1 0 1785174308 23703552 5586 4294967295 134512640 135094434 3221224448 3221223104 134558284 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/12222/statm): 5787 5586 145 145 0 5642 0 [pid=12222] vsize: 23148 Current children cumulated CPU time (s) 639.62 Current children cumulated vsize (Kb) 25272 [startup+650.056 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 12222 Raw data (/proc/12218/stat): 12218 (minisat+_script) S 12217 12218 824 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785174303 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/12218/statm): 531 226 485 147 0 384 0 [pid=12218] vsize: 2124 Raw data (/proc/12222/stat): 12222 (minisat+_64-bit) R 12218 12218 824 0 -1 0 5652 0 0 0 64927 35 0 0 25 0 1 0 1785174308 23703552 5586 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/12222/statm): 5787 5586 145 145 0 5642 0 [pid=12222] vsize: 23148 Current children cumulated CPU time (s) 649.62 Current children cumulated vsize (Kb) 25272 [startup+660.057 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 12222 Raw data (/proc/12218/stat): 12218 (minisat+_script) S 12217 12218 824 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785174303 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/12218/statm): 531 226 485 147 0 384 0 [pid=12218] vsize: 2124 Raw data (/proc/12222/stat): 12222 (minisat+_64-bit) R 12218 12218 824 0 -1 0 5652 0 0 0 65927 35 0 0 25 0 1 0 1785174308 23703552 5586 4294967295 134512640 135094434 3221224448 3221223104 134558213 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/12222/statm): 5787 5586 145 145 0 5642 0 [pid=12222] vsize: 23148 Current children cumulated CPU time (s) 659.62 Current children cumulated vsize (Kb) 25272 [startup+670.059 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 12222 Raw data (/proc/12218/stat): 12218 (minisat+_script) S 12217 12218 824 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785174303 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/12218/statm): 531 226 485 147 0 384 0 [pid=12218] vsize: 2124 Raw data (/proc/12222/stat): 12222 (minisat+_64-bit) R 12218 12218 824 0 -1 0 5652 0 0 0 66927 35 0 0 25 0 1 0 1785174308 23703552 5586 4294967295 134512640 135094434 3221224448 3221223136 134554744 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/12222/statm): 5787 5586 145 145 0 5642 0 [pid=12222] vsize: 23148 Current children cumulated CPU time (s) 669.62 Current children cumulated vsize (Kb) 25272 [startup+680.059 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 12222 Raw data (/proc/12218/stat): 12218 (minisat+_script) S 12217 12218 824 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785174303 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/12218/statm): 531 226 485 147 0 384 0 [pid=12218] vsize: 2124 Raw data (/proc/12222/stat): 12222 (minisat+_64-bit) R 12218 12218 824 0 -1 0 5652 0 0 0 67927 35 0 0 25 0 1 0 1785174308 23703552 5586 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/12222/statm): 5787 5586 145 145 0 5642 0 [pid=12222] vsize: 23148 Current children cumulated CPU time (s) 679.62 Current children cumulated vsize (Kb) 25272 [startup+690.06 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 12222 Raw data (/proc/12218/stat): 12218 (minisat+_script) S 12217 12218 824 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785174303 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/12218/statm): 531 226 485 147 0 384 0 [pid=12218] vsize: 2124 Raw data (/proc/12222/stat): 12222 (minisat+_64-bit) R 12218 12218 824 0 -1 0 5653 0 0 0 68928 35 0 0 25 0 1 0 1785174308 23703552 5587 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/12222/statm): 5787 5587 145 145 0 5642 0 [pid=12222] vsize: 23148 Current children cumulated CPU time (s) 689.63 Current children cumulated vsize (Kb) 25272 [startup+700.062 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 12222 Raw data (/proc/12218/stat): 12218 (minisat+_script) S 12217 12218 824 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785174303 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/12218/statm): 531 226 485 147 0 384 0 [pid=12218] vsize: 2124 Raw data (/proc/12222/stat): 12222 (minisat+_64-bit) R 12218 12218 824 0 -1 0 5653 0 0 0 69928 35 0 0 25 0 1 0 1785174308 23703552 5587 4294967295 134512640 135094434 3221224448 3221223072 134557685 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/12222/statm): 5787 5587 145 145 0 5642 0 [pid=12222] vsize: 23148 Current children cumulated CPU time (s) 699.63 Current children cumulated vsize (Kb) 25272 [startup+710.063 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 12222 Raw data (/proc/12218/stat): 12218 (minisat+_script) S 12217 12218 824 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785174303 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/12218/statm): 531 226 485 147 0 384 0 [pid=12218] vsize: 2124 Raw data (/proc/12222/stat): 12222 (minisat+_64-bit) R 12218 12218 824 0 -1 0 5653 0 0 0 70928 35 0 0 25 0 1 0 1785174308 23703552 5587 4294967295 134512640 135094434 3221224448 3221223080 134557561 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/12222/statm): 5787 5587 145 145 0 5642 0 [pid=12222] vsize: 23148 Current children cumulated CPU time (s) 709.63 Current children cumulated vsize (Kb) 25272 [startup+720.063 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 12222 Raw data (/proc/12218/stat): 12218 (minisat+_script) S 12217 12218 824 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785174303 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/12218/statm): 531 226 485 147 0 384 0 [pid=12218] vsize: 2124 Raw data (/proc/12222/stat): 12222 (minisat+_64-bit) R 12218 12218 824 0 -1 0 5654 0 0 0 71929 35 0 0 25 0 1 0 1785174308 23703552 5588 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/12222/statm): 5787 5588 145 145 0 5642 0 [pid=12222] vsize: 23148 Current children cumulated CPU time (s) 719.64 Current children cumulated vsize (Kb) 25272 [startup+730.064 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 12222 Raw data (/proc/12218/stat): 12218 (minisat+_script) S 12217 12218 824 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785174303 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/12218/statm): 531 226 485 147 0 384 0 [pid=12218] vsize: 2124 Raw data (/proc/12222/stat): 12222 (minisat+_64-bit) R 12218 12218 824 0 -1 0 5657 0 0 0 72929 35 0 0 25 0 1 0 1785174308 23703552 5591 4294967295 134512640 135094434 3221224448 3221223040 134556812 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/12222/statm): 5787 5591 145 145 0 5642 0 [pid=12222] vsize: 23148 Current children cumulated CPU time (s) 729.64 Current children cumulated vsize (Kb) 25272 [startup+740.066 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 12222 Raw data (/proc/12218/stat): 12218 (minisat+_script) S 12217 12218 824 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785174303 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/12218/statm): 531 226 485 147 0 384 0 [pid=12218] vsize: 2124 Raw data (/proc/12222/stat): 12222 (minisat+_64-bit) R 12218 12218 824 0 -1 0 5657 0 0 0 73929 35 0 0 25 0 1 0 1785174308 23703552 5591 4294967295 134512640 135094434 3221224448 3221223104 134558249 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/12222/statm): 5787 5591 145 145 0 5642 0 [pid=12222] vsize: 23148 Current children cumulated CPU time (s) 739.64 Current children cumulated vsize (Kb) 25272 [startup+750.067 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 12222 Raw data (/proc/12218/stat): 12218 (minisat+_script) S 12217 12218 824 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785174303 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/12218/statm): 531 226 485 147 0 384 0 [pid=12218] vsize: 2124 Raw data (/proc/12222/stat): 12222 (minisat+_64-bit) R 12218 12218 824 0 -1 0 5658 0 0 0 74929 35 0 0 25 0 1 0 1785174308 23703552 5592 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/12222/statm): 5787 5592 145 145 0 5642 0 [pid=12222] vsize: 23148 Current children cumulated CPU time (s) 749.64 Current children cumulated vsize (Kb) 25272 [startup+760.067 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 12222 Raw data (/proc/12218/stat): 12218 (minisat+_script) S 12217 12218 824 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785174303 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/12218/statm): 531 226 485 147 0 384 0 [pid=12218] vsize: 2124 Raw data (/proc/12222/stat): 12222 (minisat+_64-bit) R 12218 12218 824 0 -1 0 5660 0 0 0 75930 35 0 0 25 0 1 0 1785174308 23703552 5594 4294967295 134512640 135094434 3221224448 3221223040 134557236 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/12222/statm): 5787 5594 145 145 0 5642 0 [pid=12222] vsize: 23148 Current children cumulated CPU time (s) 759.65 Current children cumulated vsize (Kb) 25272 [startup+770.069 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 12222 Raw data (/proc/12218/stat): 12218 (minisat+_script) S 12217 12218 824 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785174303 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/12218/statm): 531 226 485 147 0 384 0 [pid=12218] vsize: 2124 Raw data (/proc/12222/stat): 12222 (minisat+_64-bit) R 12218 12218 824 0 -1 0 5662 0 0 0 76930 35 0 0 25 0 1 0 1785174308 23703552 5596 4294967295 134512640 135094434 3221224448 3221223104 134558187 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/12222/statm): 5787 5596 145 145 0 5642 0 [pid=12222] vsize: 23148 Current children cumulated CPU time (s) 769.65 Current children cumulated vsize (Kb) 25272 [startup+780.07 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 12222 Raw data (/proc/12218/stat): 12218 (minisat+_script) S 12217 12218 824 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785174303 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/12218/statm): 531 226 485 147 0 384 0 [pid=12218] vsize: 2124 Raw data (/proc/12222/stat): 12222 (minisat+_64-bit) R 12218 12218 824 0 -1 0 5662 0 0 0 77930 35 0 0 25 0 1 0 1785174308 23703552 5596 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/12222/statm): 5787 5596 145 145 0 5642 0 [pid=12222] vsize: 23148 Current children cumulated CPU time (s) 779.65 Current children cumulated vsize (Kb) 25272 [startup+790.072 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 12222 Raw data (/proc/12218/stat): 12218 (minisat+_script) S 12217 12218 824 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785174303 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/12218/statm): 531 226 485 147 0 384 0 [pid=12218] vsize: 2124 Raw data (/proc/12222/stat): 12222 (minisat+_64-bit) R 12218 12218 824 0 -1 0 5662 0 0 0 78930 35 0 0 25 0 1 0 1785174308 23703552 5596 4294967295 134512640 135094434 3221224448 3221223040 134556904 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/12222/statm): 5787 5596 145 145 0 5642 0 [pid=12222] vsize: 23148 Current children cumulated CPU time (s) 789.65 Current children cumulated vsize (Kb) 25272 [startup+800.072 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 12222 Raw data (/proc/12218/stat): 12218 (minisat+_script) S 12217 12218 824 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785174303 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/12218/statm): 531 226 485 147 0 384 0 [pid=12218] vsize: 2124 Raw data (/proc/12222/stat): 12222 (minisat+_64-bit) R 12218 12218 824 0 -1 0 5662 0 0 0 79930 35 0 0 25 0 1 0 1785174308 23703552 5596 4294967295 134512640 135094434 3221224448 3221223040 134556961 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/12222/statm): 5787 5596 145 145 0 5642 0 [pid=12222] vsize: 23148 Current children cumulated CPU time (s) 799.65 Current children cumulated vsize (Kb) 25272 [startup+810.072 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 12222 Raw data (/proc/12218/stat): 12218 (minisat+_script) S 12217 12218 824 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785174303 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/12218/statm): 531 226 485 147 0 384 0 [pid=12218] vsize: 2124 Raw data (/proc/12222/stat): 12222 (minisat+_64-bit) R 12218 12218 824 0 -1 0 5662 0 0 0 80931 35 0 0 25 0 1 0 1785174308 23703552 5596 4294967295 134512640 135094434 3221224448 3221223104 134558126 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/12222/statm): 5787 5596 145 145 0 5642 0 [pid=12222] vsize: 23148 Current children cumulated CPU time (s) 809.66 Current children cumulated vsize (Kb) 25272 [startup+820.073 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 12222 Raw data (/proc/12218/stat): 12218 (minisat+_script) S 12217 12218 824 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785174303 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/12218/statm): 531 226 485 147 0 384 0 [pid=12218] vsize: 2124 Raw data (/proc/12222/stat): 12222 (minisat+_64-bit) R 12218 12218 824 0 -1 0 5662 0 0 0 81931 35 0 0 25 0 1 0 1785174308 23703552 5596 4294967295 134512640 135094434 3221224448 3221223104 134558178 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/12222/statm): 5787 5596 145 145 0 5642 0 [pid=12222] vsize: 23148 Current children cumulated CPU time (s) 819.66 Current children cumulated vsize (Kb) 25272 [startup+830.074 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 12222 Raw data (/proc/12218/stat): 12218 (minisat+_script) S 12217 12218 824 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785174303 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/12218/statm): 531 226 485 147 0 384 0 [pid=12218] vsize: 2124 Raw data (/proc/12222/stat): 12222 (minisat+_64-bit) R 12218 12218 824 0 -1 0 5662 0 0 0 82931 35 0 0 25 0 1 0 1785174308 23703552 5596 4294967295 134512640 135094434 3221224448 3221223040 134557273 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/12222/statm): 5787 5596 145 145 0 5642 0 [pid=12222] vsize: 23148 Current children cumulated CPU time (s) 829.66 Current children cumulated vsize (Kb) 25272 [startup+840.074 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 12222 Raw data (/proc/12218/stat): 12218 (minisat+_script) S 12217 12218 824 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785174303 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/12218/statm): 531 226 485 147 0 384 0 [pid=12218] vsize: 2124 Raw data (/proc/12222/stat): 12222 (minisat+_64-bit) R 12218 12218 824 0 -1 0 5662 0 0 0 83931 35 0 0 25 0 1 0 1785174308 23703552 5596 4294967295 134512640 135094434 3221224448 3221223072 134557714 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/12222/statm): 5787 5596 145 145 0 5642 0 [pid=12222] vsize: 23148 Current children cumulated CPU time (s) 839.66 Current children cumulated vsize (Kb) 25272 [startup+850.075 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 12222 Raw data (/proc/12218/stat): 12218 (minisat+_script) S 12217 12218 824 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785174303 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/12218/statm): 531 226 485 147 0 384 0 [pid=12218] vsize: 2124 Raw data (/proc/12222/stat): 12222 (minisat+_64-bit) R 12218 12218 824 0 -1 0 5662 0 0 0 84932 35 0 0 25 0 1 0 1785174308 23703552 5596 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/12222/statm): 5787 5596 145 145 0 5642 0 [pid=12222] vsize: 23148 Current children cumulated CPU time (s) 849.67 Current children cumulated vsize (Kb) 25272 [startup+860.076 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 12222 Raw data (/proc/12218/stat): 12218 (minisat+_script) S 12217 12218 824 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785174303 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/12218/statm): 531 226 485 147 0 384 0 [pid=12218] vsize: 2124 Raw data (/proc/12222/stat): 12222 (minisat+_64-bit) R 12218 12218 824 0 -1 0 5662 0 0 0 85932 35 0 0 25 0 1 0 1785174308 23703552 5596 4294967295 134512640 135094434 3221224448 3221223104 134558249 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/12222/statm): 5787 5596 145 145 0 5642 0 [pid=12222] vsize: 23148 Current children cumulated CPU time (s) 859.67 Current children cumulated vsize (Kb) 25272 [startup+870.077 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 12222 Raw data (/proc/12218/stat): 12218 (minisat+_script) S 12217 12218 824 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785174303 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/12218/statm): 531 226 485 147 0 384 0 [pid=12218] vsize: 2124 Raw data (/proc/12222/stat): 12222 (minisat+_64-bit) R 12218 12218 824 0 -1 0 5662 0 0 0 86932 35 0 0 25 0 1 0 1785174308 23703552 5596 4294967295 134512640 135094434 3221224448 3221223104 134558254 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/12222/statm): 5787 5596 145 145 0 5642 0 [pid=12222] vsize: 23148 Current children cumulated CPU time (s) 869.67 Current children cumulated vsize (Kb) 25272 [startup+880.077 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 12222 Raw data (/proc/12218/stat): 12218 (minisat+_script) S 12217 12218 824 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785174303 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/12218/statm): 531 226 485 147 0 384 0 [pid=12218] vsize: 2124 Raw data (/proc/12222/stat): 12222 (minisat+_64-bit) R 12218 12218 824 0 -1 0 5662 0 0 0 87932 36 0 0 25 0 1 0 1785174308 23703552 5596 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/12222/statm): 5787 5596 145 145 0 5642 0 [pid=12222] vsize: 23148 Current children cumulated CPU time (s) 879.68 Current children cumulated vsize (Kb) 25272 [startup+890.078 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 12222 Raw data (/proc/12218/stat): 12218 (minisat+_script) S 12217 12218 824 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785174303 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/12218/statm): 531 226 485 147 0 384 0 [pid=12218] vsize: 2124 Raw data (/proc/12222/stat): 12222 (minisat+_64-bit) R 12218 12218 824 0 -1 0 5662 0 0 0 88932 36 0 0 25 0 1 0 1785174308 23703552 5596 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/12222/statm): 5787 5596 145 145 0 5642 0 [pid=12222] vsize: 23148 Current children cumulated CPU time (s) 889.68 Current children cumulated vsize (Kb) 25272 [startup+900.079 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 12222 Raw data (/proc/12218/stat): 12218 (minisat+_script) S 12217 12218 824 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785174303 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/12218/statm): 531 226 485 147 0 384 0 [pid=12218] vsize: 2124 Raw data (/proc/12222/stat): 12222 (minisat+_64-bit) R 12218 12218 824 0 -1 0 5662 0 0 0 89933 36 0 0 25 0 1 0 1785174308 23703552 5596 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/12222/statm): 5787 5596 145 145 0 5642 0 [pid=12222] vsize: 23148 Current children cumulated CPU time (s) 899.69 Current children cumulated vsize (Kb) 25272 [startup+910.079 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 12222 Raw data (/proc/12218/stat): 12218 (minisat+_script) S 12217 12218 824 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785174303 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/12218/statm): 531 226 485 147 0 384 0 [pid=12218] vsize: 2124 Raw data (/proc/12222/stat): 12222 (minisat+_64-bit) R 12218 12218 824 0 -1 0 5662 0 0 0 90933 36 0 0 25 0 1 0 1785174308 23703552 5596 4294967295 134512640 135094434 3221224448 3221223072 134557565 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/12222/statm): 5787 5596 145 145 0 5642 0 [pid=12222] vsize: 23148 Current children cumulated CPU time (s) 909.69 Current children cumulated vsize (Kb) 25272 [startup+920.08 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 12222 Raw data (/proc/12218/stat): 12218 (minisat+_script) S 12217 12218 824 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785174303 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/12218/statm): 531 226 485 147 0 384 0 [pid=12218] vsize: 2124 Raw data (/proc/12222/stat): 12222 (minisat+_64-bit) R 12218 12218 824 0 -1 0 5662 0 0 0 91933 36 0 0 25 0 1 0 1785174308 23703552 5596 4294967295 134512640 135094434 3221224448 3221223104 134558249 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/12222/statm): 5787 5596 145 145 0 5642 0 [pid=12222] vsize: 23148 Current children cumulated CPU time (s) 919.69 Current children cumulated vsize (Kb) 25272 [startup+930.081 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 12222 Raw data (/proc/12218/stat): 12218 (minisat+_script) S 12217 12218 824 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785174303 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/12218/statm): 531 226 485 147 0 384 0 [pid=12218] vsize: 2124 Raw data (/proc/12222/stat): 12222 (minisat+_64-bit) R 12218 12218 824 0 -1 0 5662 0 0 0 92933 36 0 0 25 0 1 0 1785174308 23703552 5596 4294967295 134512640 135094434 3221224448 3221223136 134554731 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/12222/statm): 5787 5596 145 145 0 5642 0 [pid=12222] vsize: 23148 Current children cumulated CPU time (s) 929.69 Current children cumulated vsize (Kb) 25272 [startup+940.083 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 12222 Raw data (/proc/12218/stat): 12218 (minisat+_script) S 12217 12218 824 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785174303 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/12218/statm): 531 226 485 147 0 384 0 [pid=12218] vsize: 2124 Raw data (/proc/12222/stat): 12222 (minisat+_64-bit) R 12218 12218 824 0 -1 0 5662 0 0 0 93934 36 0 0 25 0 1 0 1785174308 23703552 5596 4294967295 134512640 135094434 3221224448 3221223072 134557645 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/12222/statm): 5787 5596 145 145 0 5642 0 [pid=12222] vsize: 23148 Current children cumulated CPU time (s) 939.7 Current children cumulated vsize (Kb) 25272 [startup+950.083 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 12222 Raw data (/proc/12218/stat): 12218 (minisat+_script) S 12217 12218 824 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785174303 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/12218/statm): 531 226 485 147 0 384 0 [pid=12218] vsize: 2124 Raw data (/proc/12222/stat): 12222 (minisat+_64-bit) R 12218 12218 824 0 -1 0 5662 0 0 0 94934 36 0 0 25 0 1 0 1785174308 23703552 5596 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/12222/statm): 5787 5596 145 145 0 5642 0 [pid=12222] vsize: 23148 Current children cumulated CPU time (s) 949.7 Current children cumulated vsize (Kb) 25272 [startup+960.083 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 12222 Raw data (/proc/12218/stat): 12218 (minisat+_script) S 12217 12218 824 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785174303 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/12218/statm): 531 226 485 147 0 384 0 [pid=12218] vsize: 2124 Raw data (/proc/12222/stat): 12222 (minisat+_64-bit) R 12218 12218 824 0 -1 0 5662 0 0 0 95934 36 0 0 25 0 1 0 1785174308 23703552 5596 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/12222/statm): 5787 5596 145 145 0 5642 0 [pid=12222] vsize: 23148 Current children cumulated CPU time (s) 959.7 Current children cumulated vsize (Kb) 25272 [startup+970.085 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 12222 Raw data (/proc/12218/stat): 12218 (minisat+_script) S 12217 12218 824 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785174303 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/12218/statm): 531 226 485 147 0 384 0 [pid=12218] vsize: 2124 Raw data (/proc/12222/stat): 12222 (minisat+_64-bit) R 12218 12218 824 0 -1 0 5662 0 0 0 96934 36 0 0 25 0 1 0 1785174308 23703552 5596 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/12222/statm): 5787 5596 145 145 0 5642 0 [pid=12222] vsize: 23148 Current children cumulated CPU time (s) 969.7 Current children cumulated vsize (Kb) 25272 [startup+980.086 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 12222 Raw data (/proc/12218/stat): 12218 (minisat+_script) S 12217 12218 824 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785174303 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/12218/statm): 531 226 485 147 0 384 0 [pid=12218] vsize: 2124 Raw data (/proc/12222/stat): 12222 (minisat+_64-bit) R 12218 12218 824 0 -1 0 5662 0 0 0 97935 36 0 0 25 0 1 0 1785174308 23703552 5596 4294967295 134512640 135094434 3221224448 3221223040 134557310 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/12222/statm): 5787 5596 145 145 0 5642 0 [pid=12222] vsize: 23148 Current children cumulated CPU time (s) 979.71 Current children cumulated vsize (Kb) 25272 [startup+990.086 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 12222 Raw data (/proc/12218/stat): 12218 (minisat+_script) S 12217 12218 824 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785174303 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/12218/statm): 531 226 485 147 0 384 0 [pid=12218] vsize: 2124 Raw data (/proc/12222/stat): 12222 (minisat+_64-bit) R 12218 12218 824 0 -1 0 5662 0 0 0 98935 36 0 0 25 0 1 0 1785174308 23703552 5596 4294967295 134512640 135094434 3221224448 3221223104 134558213 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/12222/statm): 5787 5596 145 145 0 5642 0 [pid=12222] vsize: 23148 Current children cumulated CPU time (s) 989.71 Current children cumulated vsize (Kb) 25272 [startup+1000.09 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 12222 Raw data (/proc/12218/stat): 12218 (minisat+_script) S 12217 12218 824 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785174303 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/12218/statm): 531 226 485 147 0 384 0 [pid=12218] vsize: 2124 Raw data (/proc/12222/stat): 12222 (minisat+_64-bit) R 12218 12218 824 0 -1 0 5662 0 0 0 99935 36 0 0 25 0 1 0 1785174308 23703552 5596 4294967295 134512640 135094434 3221224448 3221223072 134557685 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/12222/statm): 5787 5596 145 145 0 5642 0 [pid=12222] vsize: 23148 Current children cumulated CPU time (s) 999.71 Current children cumulated vsize (Kb) 25272 [startup+1010.09 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 12222 Raw data (/proc/12218/stat): 12218 (minisat+_script) S 12217 12218 824 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785174303 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/12218/statm): 531 226 485 147 0 384 0 [pid=12218] vsize: 2124 Raw data (/proc/12222/stat): 12222 (minisat+_64-bit) R 12218 12218 824 0 -1 0 5662 0 0 0 100935 36 0 0 25 0 1 0 1785174308 23703552 5596 4294967295 134512640 135094434 3221224448 3221223072 134557596 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/12222/statm): 5787 5596 145 145 0 5642 0 [pid=12222] vsize: 23148 Current children cumulated CPU time (s) 1009.71 Current children cumulated vsize (Kb) 25272 [startup+1020.09 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 12222 Raw data (/proc/12218/stat): 12218 (minisat+_script) S 12217 12218 824 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785174303 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/12218/statm): 531 226 485 147 0 384 0 [pid=12218] vsize: 2124 Raw data (/proc/12222/stat): 12222 (minisat+_64-bit) R 12218 12218 824 0 -1 0 5662 0 0 0 101936 36 0 0 25 0 1 0 1785174308 23703552 5596 4294967295 134512640 135094434 3221224448 3221223040 134557287 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/12222/statm): 5787 5596 145 145 0 5642 0 [pid=12222] vsize: 23148 Current children cumulated CPU time (s) 1019.72 Current children cumulated vsize (Kb) 25272 [startup+1030.09 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 12222 Raw data (/proc/12218/stat): 12218 (minisat+_script) S 12217 12218 824 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785174303 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/12218/statm): 531 226 485 147 0 384 0 [pid=12218] vsize: 2124 Raw data (/proc/12222/stat): 12222 (minisat+_64-bit) R 12218 12218 824 0 -1 0 5662 0 0 0 102936 36 0 0 25 0 1 0 1785174308 23703552 5596 4294967295 134512640 135094434 3221224448 3221223108 134553536 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/12222/statm): 5787 5596 145 145 0 5642 0 [pid=12222] vsize: 23148 Current children cumulated CPU time (s) 1029.72 Current children cumulated vsize (Kb) 25272 [startup+1040.09 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 12222 Raw data (/proc/12218/stat): 12218 (minisat+_script) S 12217 12218 824 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785174303 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/12218/statm): 531 226 485 147 0 384 0 [pid=12218] vsize: 2124 Raw data (/proc/12222/stat): 12222 (minisat+_64-bit) R 12218 12218 824 0 -1 0 5662 0 0 0 103936 36 0 0 25 0 1 0 1785174308 23703552 5596 4294967295 134512640 135094434 3221224448 3221223040 134557208 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/12222/statm): 5787 5596 145 145 0 5642 0 [pid=12222] vsize: 23148 Current children cumulated CPU time (s) 1039.72 Current children cumulated vsize (Kb) 25272 [startup+1050.09 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 12222 Raw data (/proc/12218/stat): 12218 (minisat+_script) S 12217 12218 824 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785174303 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/12218/statm): 531 226 485 147 0 384 0 [pid=12218] vsize: 2124 Raw data (/proc/12222/stat): 12222 (minisat+_64-bit) R 12218 12218 824 0 -1 0 5662 0 0 0 104936 36 0 0 25 0 1 0 1785174308 23703552 5596 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/12222/statm): 5787 5596 145 145 0 5642 0 [pid=12222] vsize: 23148 Current children cumulated CPU time (s) 1049.72 Current children cumulated vsize (Kb) 25272 [startup+1060.09 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 12222 Raw data (/proc/12218/stat): 12218 (minisat+_script) S 12217 12218 824 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785174303 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/12218/statm): 531 226 485 147 0 384 0 [pid=12218] vsize: 2124 Raw data (/proc/12222/stat): 12222 (minisat+_64-bit) R 12218 12218 824 0 -1 0 5662 0 0 0 105936 36 0 0 25 0 1 0 1785174308 23703552 5596 4294967295 134512640 135094434 3221224448 3221223040 134556902 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/12222/statm): 5787 5596 145 145 0 5642 0 [pid=12222] vsize: 23148 Current children cumulated CPU time (s) 1059.72 Current children cumulated vsize (Kb) 25272 [startup+1070.09 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 12222 Raw data (/proc/12218/stat): 12218 (minisat+_script) S 12217 12218 824 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785174303 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/12218/statm): 531 226 485 147 0 384 0 [pid=12218] vsize: 2124 Raw data (/proc/12222/stat): 12222 (minisat+_64-bit) R 12218 12218 824 0 -1 0 5662 0 0 0 106937 36 0 0 25 0 1 0 1785174308 23703552 5596 4294967295 134512640 135094434 3221224448 3221223120 134556309 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/12222/statm): 5787 5596 145 145 0 5642 0 [pid=12222] vsize: 23148 Current children cumulated CPU time (s) 1069.73 Current children cumulated vsize (Kb) 25272 [startup+1080.09 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 12222 Raw data (/proc/12218/stat): 12218 (minisat+_script) S 12217 12218 824 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785174303 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/12218/statm): 531 226 485 147 0 384 0 [pid=12218] vsize: 2124 Raw data (/proc/12222/stat): 12222 (minisat+_64-bit) R 12218 12218 824 0 -1 0 5662 0 0 0 107937 36 0 0 25 0 1 0 1785174308 23703552 5596 4294967295 134512640 135094434 3221224448 3221223040 134557236 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/12222/statm): 5787 5596 145 145 0 5642 0 [pid=12222] vsize: 23148 Current children cumulated CPU time (s) 1079.73 Current children cumulated vsize (Kb) 25272 [startup+1090.09 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 12222 Raw data (/proc/12218/stat): 12218 (minisat+_script) S 12217 12218 824 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785174303 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/12218/statm): 531 226 485 147 0 384 0 [pid=12218] vsize: 2124 Raw data (/proc/12222/stat): 12222 (minisat+_64-bit) R 12218 12218 824 0 -1 0 5662 0 0 0 108937 36 0 0 25 0 1 0 1785174308 23703552 5596 4294967295 134512640 135094434 3221224448 3221223040 134557230 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/12222/statm): 5787 5596 145 145 0 5642 0 [pid=12222] vsize: 23148 Current children cumulated CPU time (s) 1089.73 Current children cumulated vsize (Kb) 25272 [startup+1100.09 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 12222 Raw data (/proc/12218/stat): 12218 (minisat+_script) S 12217 12218 824 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785174303 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/12218/statm): 531 226 485 147 0 384 0 [pid=12218] vsize: 2124 Raw data (/proc/12222/stat): 12222 (minisat+_64-bit) R 12218 12218 824 0 -1 0 5662 0 0 0 109937 36 0 0 25 0 1 0 1785174308 23703552 5596 4294967295 134512640 135094434 3221224448 3221223104 134558405 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/12222/statm): 5787 5596 145 145 0 5642 0 [pid=12222] vsize: 23148 Current children cumulated CPU time (s) 1099.73 Current children cumulated vsize (Kb) 25272 [startup+1110.1 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 12222 Raw data (/proc/12218/stat): 12218 (minisat+_script) S 12217 12218 824 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785174303 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/12218/statm): 531 226 485 147 0 384 0 [pid=12218] vsize: 2124 Raw data (/proc/12222/stat): 12222 (minisat+_64-bit) R 12218 12218 824 0 -1 0 5662 0 0 0 110937 36 0 0 25 0 1 0 1785174308 23703552 5596 4294967295 134512640 135094434 3221224448 3221223136 134554746 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/12222/statm): 5787 5596 145 145 0 5642 0 [pid=12222] vsize: 23148 Current children cumulated CPU time (s) 1109.73 Current children cumulated vsize (Kb) 25272 [startup+1120.1 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 12222 Raw data (/proc/12218/stat): 12218 (minisat+_script) S 12217 12218 824 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785174303 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/12218/statm): 531 226 485 147 0 384 0 [pid=12218] vsize: 2124 Raw data (/proc/12222/stat): 12222 (minisat+_64-bit) R 12218 12218 824 0 -1 0 5662 0 0 0 111938 36 0 0 25 0 1 0 1785174308 23703552 5596 4294967295 134512640 135094434 3221224448 3221223104 134557920 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/12222/statm): 5787 5596 145 145 0 5642 0 [pid=12222] vsize: 23148 Current children cumulated CPU time (s) 1119.74 Current children cumulated vsize (Kb) 25272 [startup+1130.1 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 12222 Raw data (/proc/12218/stat): 12218 (minisat+_script) S 12217 12218 824 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785174303 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/12218/statm): 531 226 485 147 0 384 0 [pid=12218] vsize: 2124 Raw data (/proc/12222/stat): 12222 (minisat+_64-bit) R 12218 12218 824 0 -1 0 5662 0 0 0 112938 36 0 0 25 0 1 0 1785174308 23703552 5596 4294967295 134512640 135094434 3221224448 3221223104 134558249 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/12222/statm): 5787 5596 145 145 0 5642 0 [pid=12222] vsize: 23148 Current children cumulated CPU time (s) 1129.74 Current children cumulated vsize (Kb) 25272 [startup+1140.1 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 12222 Raw data (/proc/12218/stat): 12218 (minisat+_script) S 12217 12218 824 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785174303 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/12218/statm): 531 226 485 147 0 384 0 [pid=12218] vsize: 2124 Raw data (/proc/12222/stat): 12222 (minisat+_64-bit) R 12218 12218 824 0 -1 0 5732 0 0 0 113936 37 0 0 25 0 1 0 1785174308 23990272 5666 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/12222/statm): 5857 5666 145 145 0 5712 0 [pid=12222] vsize: 23428 Current children cumulated CPU time (s) 1139.73 Current children cumulated vsize (Kb) 25552 [startup+1150.1 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 12222 Raw data (/proc/12218/stat): 12218 (minisat+_script) S 12217 12218 824 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785174303 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/12218/statm): 531 226 485 147 0 384 0 [pid=12218] vsize: 2124 Raw data (/proc/12222/stat): 12222 (minisat+_64-bit) R 12218 12218 824 0 -1 0 5859 0 0 0 114934 38 0 0 25 0 1 0 1785174308 24510464 5793 4294967295 134512640 135094434 3221224448 3221223120 134555599 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/12222/statm): 5984 5793 145 145 0 5839 0 [pid=12222] vsize: 23936 Current children cumulated CPU time (s) 1149.72 Current children cumulated vsize (Kb) 26060 [startup+1160.1 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 12222 Raw data (/proc/12218/stat): 12218 (minisat+_script) S 12217 12218 824 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785174303 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/12218/statm): 531 226 485 147 0 384 0 [pid=12218] vsize: 2124 Raw data (/proc/12222/stat): 12222 (minisat+_64-bit) R 12218 12218 824 0 -1 0 5989 0 0 0 115933 38 0 0 25 0 1 0 1785174308 25042944 5923 4294967295 134512640 135094434 3221224448 3221223104 134557813 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/12222/statm): 6114 5923 145 145 0 5969 0 [pid=12222] vsize: 24456 Current children cumulated CPU time (s) 1159.71 Current children cumulated vsize (Kb) 26580 [startup+1170.1 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 12222 Raw data (/proc/12218/stat): 12218 (minisat+_script) S 12217 12218 824 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785174303 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/12218/statm): 531 226 485 147 0 384 0 [pid=12218] vsize: 2124 Raw data (/proc/12222/stat): 12222 (minisat+_64-bit) R 12218 12218 824 0 -1 0 6086 0 0 0 116932 38 0 0 25 0 1 0 1785174308 25440256 6020 4294967295 134512640 135094434 3221224448 3221223104 134558249 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/12222/statm): 6211 6020 145 145 0 6066 0 [pid=12222] vsize: 24844 Current children cumulated CPU time (s) 1169.7 Current children cumulated vsize (Kb) 26968 [startup+1180.1 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 12222 Raw data (/proc/12218/stat): 12218 (minisat+_script) S 12217 12218 824 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785174303 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/12218/statm): 531 226 485 147 0 384 0 [pid=12218] vsize: 2124 Raw data (/proc/12222/stat): 12222 (minisat+_64-bit) R 12218 12218 824 0 -1 0 6175 0 0 0 117930 39 0 0 25 0 1 0 1785174308 25817088 6109 4294967295 134512640 135094434 3221224448 3221223104 134558395 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/12222/statm): 6303 6109 145 145 0 6158 0 [pid=12222] vsize: 25212 Current children cumulated CPU time (s) 1179.69 Current children cumulated vsize (Kb) 27336 [startup+1190.1 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 12222 Raw data (/proc/12218/stat): 12218 (minisat+_script) S 12217 12218 824 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785174303 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/12218/statm): 531 226 485 147 0 384 0 [pid=12218] vsize: 2124 Raw data (/proc/12222/stat): 12222 (minisat+_64-bit) R 12218 12218 824 0 -1 0 6190 0 0 0 118930 39 0 0 25 0 1 0 1785174308 25878528 6124 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/12222/statm): 6318 6124 145 145 0 6173 0 [pid=12222] vsize: 25272 Current children cumulated CPU time (s) 1189.69 Current children cumulated vsize (Kb) 27396 [startup+1200.1 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 12222 Raw data (/proc/12218/stat): 12218 (minisat+_script) S 12217 12218 824 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785174303 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/12218/statm): 531 226 485 147 0 384 0 [pid=12218] vsize: 2124 Raw data (/proc/12222/stat): 12222 (minisat+_64-bit) R 12218 12218 824 0 -1 0 6196 0 0 0 119930 39 0 0 25 0 1 0 1785174308 25907200 6130 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/12222/statm): 6325 6130 145 145 0 6180 0 [pid=12222] vsize: 25300 Current children cumulated CPU time (s) 1199.69 Current children cumulated vsize (Kb) 27424 [startup+1210.11 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 12222 Raw data (/proc/12218/stat): 12218 (minisat+_script) S 12217 12218 824 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785174303 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/12218/statm): 531 226 485 147 0 384 0 [pid=12218] vsize: 2124 Raw data (/proc/12222/stat): 12222 (minisat+_64-bit) R 12218 12218 824 0 -1 0 6204 0 0 0 120930 39 0 0 25 0 1 0 1785174308 25939968 6138 4294967295 134512640 135094434 3221224448 3221223104 134557879 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/12222/statm): 6333 6138 145 145 0 6188 0 [pid=12222] vsize: 25332 Current children cumulated CPU time (s) 1209.69 Current children cumulated vsize (Kb) 27456 Maximum CPU time exceeded: sending SIGTERM then SIGKILL [startup+1210.11 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 12222 Raw data (/proc/12218/stat): 12218 (minisat+_script) S 12217 12218 824 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785174303 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/12218/statm): 531 226 485 147 0 384 0 [pid=12218] vsize: 2124 Raw data (/proc/12222/stat): 12222 (minisat+_64-bit) R 12218 12218 824 0 -1 0 6204 0 0 0 120930 39 0 0 25 0 1 0 1785174308 25939968 6138 4294967295 134512640 135094434 3221224448 3221223104 134558213 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/12222/statm): 6333 6138 145 145 0 6188 0 [pid=12222] vsize: 25332 Current children cumulated CPU time (s) 1209.69 Current children cumulated vsize (Kb) 27456 Sending SIGTERM to -12218 Sleeping 2 seconds One traced child (pid=12218) ended because it received signal 15 (SIGTERM) One traced child (pid=12222) exited with status: 10 All traced children have exited ! Game is over. Child status: 10 Real time (s): 1210.12 CPU time (s): 1209.72 CPU user time (s): 1209.31 CPU system time (s): 0.412937 CPU usage (%): 99.967 Max. virtual memory (cumulated for all children) (Kb): 27456
ERROR: no interpretation found !