Name | mps-v2-13-7/MIPLIB/miplib3/normalized-mps-v2-13-7-p0282.opb |
MD5SUM | 1a8deb577df7e72871b7e1004c098336 |
Bench Category | optimization, medium integers (OPTMEDINT) |
Has Objective Function | YES |
Satisfiable | YES |
(Un)Satisfiability was proved | YES |
Best value of the objective function | 258411 |
Optimality of the best value was proved | YES |
Number of terms in the objective function | 282 |
Biggest coefficient in the objective function | 160646 |
Number of bits for the biggest coefficient in the objective function | 18 |
Sum of the numbers in the objective function | 1302615 |
Number of bits of the sum of numbers in the objective function | 21 |
Biggest number in a constraint | 160646 |
Number of bits of the biggest number in a constraint | 18 |
Biggest sum of numbers in a constraint | 1302615 |
Number of bits of the biggest sum of numbers | 21 |
Best result obtained on this benchmark | OPTIMUM FOUND |
Best CPU time to get the best result obtained on this benchmark | 50.1794 |
Number of variables | 282 |
Total number of constraints | 523 |
Number of constraints which are clauses | 177 |
Number of constraints which are cardinality constraints (but not clauses) | 282 |
Number of constraints which are nor clauses,nor cardinality constraints | 64 |
Minimum length of a constraint | 1 |
Maximum length of a constraint | 57 |
LAUNCH ON wulflinc23 THE 2005-09-20 04:32:37 (client local time) PB2005-SCRIPT v4.0 MARKUPS: idlaunch=3381 boxname=wulflinc23 idbench=1037 idsolver=3 numberseed=0 MD5SUM SOLVER: MD5SUM BENCH: 1a8deb577df7e72871b7e1004c098336 /oldhome/oroussel/tmp/wulflinc23/normalized-mps-v2-13-7-p0282.opb REAL COMMAND: minisat+_script /oldhome/oroussel/tmp/wulflinc23/normalized-mps-v2-13-7-p0282.opb IDLAUNCH: 3381 /proc/cpuinfo: processor : 0 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 3 cpu MHz : 451.037 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 : 890.88 processor : 1 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 3 cpu MHz : 451.037 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: 907284 kB Buffers: 18952 kB Cached: 80984 kB SwapCached: 840 kB Active: 27972 kB Inactive: 74568 kB HighTotal: 131008 kB HighFree: 48944 kB LowTotal: 903652 kB LowFree: 858340 kB SwapTotal: 2097136 kB SwapFree: 2095788 kB Dirty: 28 kB Writeback: 0 kB Mapped: 5668 kB Slab: 19188 kB Committed_AS: 64168 kB PageTables: 328 kB VmallocTotal: 114680 kB VmallocUsed: 1364 kB VmallocChunk: 113256 kB JOB ENDED THE 2005-09-20 04:52:47 (client local time) WITH STATUS 10 IN 1209.25 SECONDS stats: 3381 7 1209.25 10
c Parsing PB file... c Converting 221 PB-constraints to clauses... c -- Unit propagations: (none) c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): sss................................................................................................................................................................................. c ---[ 223]---> Sorter-cost: 850 Base: 5 2 3 3 c ---[ 222]---> Sorter-cost: 712 Base: 5 2 3 3 c ---[ 221]---> Sorter-cost: 1135 Base: 2 5 5 c ---[ 220]---> Sorter-cost: 908 Base: 2 5 5 c ---[ 219]---> Sorter-cost: 1099 Base: 2 5 3 2 c ---[ 218]---> Sorter-cost: 882 Base: 2 5 3 3 c ---[ 217]---> Sorter-cost: 908 Base: 2 5 5 c ---[ 216]---> Sorter-cost: 909 Base: 2 5 5 c ---[ 215]---> Sorter-cost: 1016 Base: 2 5 3 c ---[ 214]---> Sorter-cost: 898 Base: 2 5 3 3 c ---[ 213]---> Sorter-cost: 1146 Base: 2 5 3 3 c ---[ 211]---> Sorter-cost: 996 Base: 2 5 3 3 c ---[ 209]---> Sorter-cost: 943 Base: 2 5 3 3 c ---[ 208]---> Sorter-cost: 760 Base: 2 5 3 3 c ---[ 207]---> Sorter-cost: 769 Base: 5 2 3 3 c ---[ 206]---> Sorter-cost: 713 Base: 5 2 3 3 c ---[ 205]---> Sorter-cost: 1005 Base: 2 5 5 c ---[ 204]---> Sorter-cost: 908 Base: 2 5 5 c ---[ 203]---> Sorter-cost: 1072 Base: 2 5 3 c ---[ 202]---> Sorter-cost: 885 Base: 2 5 3 2 c ---[ 201]---> Sorter-cost: 712 Base: 5 2 3 3 c ---[ 199]---> Sorter-cost: 908 Base: 2 5 5 c ---[ 198]---> Sorter-cost: 909 Base: 2 5 5 c ---[ 197]---> Sorter-cost: 938 Base: 2 5 3 2 c ---[ 196]---> Sorter-cost: 852 Base: 2 5 3 3 c ---[ 195]---> Sorter-cost: 1059 Base: 2 5 3 3 c ---[ 194]---> Sorter-cost: 949 Base: 2 5 3 3 c ---[ 193]---> Sorter-cost: 844 Base: 2 5 3 3 c ---[ 192]---> Sorter-cost: 841 Base: 2 5 3 3 c ---[ 191]---> Sorter-cost: 1081 Base: 2 5 3 3 c ---[ 190]---> Sorter-cost: 996 Base: 2 5 3 2 c ---[ 189]---> Sorter-cost: 995 Base: 2 5 3 3 c ---[ 188]---> Sorter-cost: 985 Base: 2 5 3 2 c ---[ 187]---> BDD-cost: 56 c ---[ 186]---> BDD-cost: 10 c ---[ 185]---> BDD-cost: 56 c ---[ 184]---> BDD-cost: 56 c ---[ 183]---> BDD-cost: 16 c ---[ 182]---> BDD-cost: 26 c ---[ 181]---> BDD-cost: 8 c ---[ 180]---> BDD-cost: 4 c ---[ 2]---> Sorter-cost: 678 Base: 2 5 3 c ---[ 1]---> Sorter-cost: 694 Base: 2 5 3 c ---[ 0]---> BDD-cost: 12 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 0 | 70255 164891 | 23418 0 0 nan | 0.000 % | c ============================================================================== c [1mFound solution: 881867[0m c ---[ 0]---> Sorter-cost:77310 Base: 3 3 3 3 2 3 3 3 3 3 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 94 | 288858 675684 | 96286 88 654 7.4 | 0.000 % | c | 195 | 288627 675172 | 105914 184 1358 7.4 | 0.198 % | c | 347 | 288591 675094 | 116506 333 2602 7.8 | 0.208 % | c | 573 | 288578 675066 | 128156 558 4285 7.7 | 0.212 % | c ============================================================================== c [1mFound solution: 798158[0m c ---[ 0]---> Sorter-cost: 12 Base: 3 3 3 3 2 3 3 3 3 3 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 595 | 289292 677295 | 96430 580 4464 7.7 | 0.212 % | c | 695 | 289229 677156 | 106073 677 5230 7.7 | 0.228 % | c | 845 | 289229 677156 | 116680 827 11071 13.4 | 0.228 % | c | 1070 | 289229 677156 | 128348 1052 12272 11.7 | 0.228 % | c | 1407 | 289229 677156 | 141183 1389 16783 12.1 | 0.228 % | c | 1913 | 289229 677156 | 155301 1895 22562 11.9 | 0.228 % | c | 2673 | 289075 676811 | 170831 2651 36393 13.7 | 0.268 % | c ============================================================================== c [1mFound solution: 491204[0m c ---[ 0]---> Sorter-cost: 12 Base: 3 3 3 3 2 3 3 3 3 3 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 3485 | 289830 678675 | 96610 3463 53869 15.6 | 0.268 % | c | 3588 | 289830 678675 | 106271 3566 56114 15.7 | 0.268 % | c | 3738 | 289830 678675 | 116898 3716 57041 15.4 | 0.268 % | c | 3964 | 289830 678675 | 128587 3942 58762 14.9 | 0.268 % | c | 4302 | 289497 677924 | 141446 4259 65556 15.4 | 0.359 % | c | 4808 | 289486 677901 | 155591 4764 76531 16.1 | 0.362 % | c | 5570 | 289486 677901 | 171150 5526 92145 16.7 | 0.362 % | c | 6709 | 289269 677414 | 188265 6660 147337 22.1 | 0.421 % | c | 8420 | 289226 677317 | 207092 8370 195883 23.4 | 0.433 % | c | 10982 | 288502 675683 | 227801 10882 251129 23.1 | 0.639 % | c | 14827 | 288119 674823 | 250581 14713 432249 29.4 | 0.746 % | c ============================================================================== c [1mFound solution: 436562[0m c ---[ 0]---> Sorter-cost: 11 Base: 3 3 3 3 2 3 3 3 3 3 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 16547 | 288672 676183 | 96224 16433 539492 32.8 | 0.746 % | c | 16647 | 288672 676183 | 105846 16533 540183 32.7 | 0.744 % | c | 16798 | 288672 676183 | 116431 16684 541629 32.5 | 0.744 % | c | 17024 | 288672 676183 | 128074 16910 550880 32.6 | 0.744 % | c | 17362 | 288672 676183 | 140881 17248 558318 32.4 | 0.744 % | c | 17868 | 288672 676183 | 154969 17754 566864 31.9 | 0.744 % | c | 18629 | 288542 675891 | 170466 18512 573030 31.0 | 0.778 % | c | 19768 | 288542 675891 | 187513 19651 616919 31.4 | 0.778 % | c | 21478 | 288517 675836 | 206264 21359 721335 33.8 | 0.785 % | c ============================================================================== c [1mFound solution: 435105[0m c ---[ 0]---> Sorter-cost: 12 Base: 3 3 3 3 2 3 3 3 3 3 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 22186 | 288522 676084 | 96174 22015 748548 34.0 | 0.785 % | c | 22286 | 288522 676084 | 105791 22115 750097 33.9 | 0.886 % | c | 22437 | 288522 676084 | 116370 22266 750817 33.7 | 0.886 % | c | 22662 | 288522 676084 | 128007 22491 752052 33.4 | 0.886 % | c | 22999 | 288522 676084 | 140808 22828 754156 33.0 | 0.886 % | c | 23505 | 288522 676084 | 154889 23334 777295 33.3 | 0.886 % | c | 24266 | 288458 675940 | 170378 24094 804215 33.4 | 0.902 % | c | 25405 | 288430 675876 | 187415 25231 822738 32.6 | 0.910 % | c | 27116 | 288321 675631 | 206157 26937 846652 31.4 | 0.940 % | c | 29681 | 288251 675472 | 226773 29492 1007488 34.2 | 0.960 % | c ============================================================================== c [1mFound solution: 376947[0m c ---[ 0]---> Sorter-cost: 10 Base: 3 3 3 3 2 3 3 3 3 3 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 31856 | 288251 675561 | 96083 31666 1138561 36.0 | 0.960 % | c | 31957 | 288251 675561 | 105691 31767 1139909 35.9 | 0.971 % | c | 32108 | 288251 675561 | 116260 31918 1140918 35.7 | 0.971 % | c | 32333 | 288145 675322 | 127886 32142 1144235 35.6 | 1.000 % | c | 32670 | 287939 674860 | 140675 32454 1155638 35.6 | 1.055 % | c | 33176 | 287939 674860 | 154742 32960 1220439 37.0 | 1.056 % | c | 33936 | 287939 674860 | 170216 33720 1267260 37.6 | 1.055 % | c | 35075 | 287807 674558 | 187238 34853 1287014 36.9 | 1.095 % | c ============================================================================== c [1mFound solution: 376622[0m c ---[ 0]---> Sorter-cost: 10 Base: 3 3 3 3 2 3 3 3 3 3 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 35698 | 287822 674602 | 95940 35476 1359098 38.3 | 1.095 % | c | 35798 | 287822 674602 | 105534 35576 1365673 38.4 | 1.096 % | c | 35949 | 287822 674602 | 116087 35727 1372000 38.4 | 1.096 % | c | 36174 | 287822 674602 | 127696 35952 1376958 38.3 | 1.096 % | c | 36512 | 287822 674602 | 140465 36290 1395290 38.4 | 1.096 % | c ============================================================================== c [1mFound solution: 354913[0m c ---[ 0]---> Sorter-cost: 11 Base: 3 3 3 3 2 3 3 3 3 3 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 36822 | 287792 674547 | 95930 36599 1404305 38.4 | 1.096 % | c | 36922 | 287792 674547 | 105523 36699 1405521 38.3 | 1.108 % | c | 37073 | 287792 674547 | 116075 36850 1406497 38.2 | 1.108 % | c | 37300 | 287792 674547 | 127682 37077 1420087 38.3 | 1.108 % | c | 37637 | 287792 674547 | 140451 37414 1438814 38.5 | 1.108 % | c | 38143 | 287792 674547 | 154496 37920 1448278 38.2 | 1.108 % | c | 38902 | 287682 674299 | 169945 38677 1480337 38.3 | 1.138 % | c | 40042 | 287644 674215 | 186940 39816 1638384 41.1 | 1.148 % | c | 41750 | 287644 674215 | 205634 41524 1686397 40.6 | 1.148 % | c | 44312 | 287644 674215 | 226197 44086 1953984 44.3 | 1.148 % | c | 48157 | 287510 673913 | 248817 47929 2297892 47.9 | 1.183 % | c ============================================================================== c [1mFound solution: 354908[0m c ---[ 0]---> Sorter-cost: 9 Base: 3 3 3 3 2 3 3 3 3 3 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 48837 | 287329 673517 | 95776 48605 2325753 47.9 | 1.183 % | c | 48937 | 287329 673517 | 105353 48705 2331070 47.9 | 1.232 % | c | 49087 | 287329 673517 | 115888 48855 2338335 47.9 | 1.232 % | c | 49312 | 287325 673508 | 127477 49079 2340723 47.7 | 1.233 % | c | 49649 | 287289 673426 | 140225 49415 2349449 47.5 | 1.244 % | c | 50156 | 287289 673426 | 154248 49922 2366434 47.4 | 1.244 % | c | 50915 | 287289 673426 | 169673 50681 2372878 46.8 | 1.244 % | c | 52055 | 287289 673426 | 186640 51821 2416696 46.6 | 1.244 % | c | 53763 | 287265 673372 | 205304 53528 2515819 47.0 | 1.252 % | c ============================================================================== c [1mFound solution: 354907[0m c ---[ 0]---> Sorter-cost: 10 Base: 3 3 3 3 2 3 3 3 3 3 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 54985 | 287199 673349 | 95733 54748 2617771 47.8 | 1.252 % | c | 55087 | 287199 673349 | 105306 54850 2618381 47.7 | 1.274 % | c | 55238 | 287102 673132 | 115836 54999 2628353 47.8 | 1.302 % | c | 55463 | 287102 673132 | 127420 55224 2648900 48.0 | 1.302 % | c | 55800 | 287102 673132 | 140162 55561 2658612 47.9 | 1.302 % | c | 56308 | 286962 672814 | 154178 56048 2666934 47.6 | 1.342 % | c | 57068 | 286958 672805 | 169596 56807 2740203 48.2 | 1.343 % | c | 58207 | 286941 672768 | 186556 57945 2841513 49.0 | 1.348 % | c | 59916 | 286941 672768 | 205212 59654 2921875 49.0 | 1.348 % | c | 62478 | 286920 672722 | 225733 62215 3171421 51.0 | 1.354 % | c ============================================================================== c [1mFound solution: 354893[0m c ---[ 0]---> Sorter-cost: 12 Base: 3 3 3 3 2 3 3 3 3 3 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 64209 | 286932 672754 | 95644 63946 3295032 51.5 | 1.354 % | c | 64310 | 286932 672754 | 105208 64047 3295611 51.5 | 1.355 % | c | 64461 | 286932 672754 | 115729 64198 3303094 51.5 | 1.355 % | c | 64686 | 286932 672754 | 127302 64423 3312052 51.4 | 1.355 % | c | 65024 | 286932 672754 | 140032 64761 3314663 51.2 | 1.355 % | c | 65533 | 286932 672754 | 154035 65270 3354188 51.4 | 1.355 % | c | 66292 | 286932 672754 | 169439 66029 3386946 51.3 | 1.355 % | c | 67432 | 286932 672754 | 186383 67169 3429370 51.1 | 1.355 % | c | 69140 | 286932 672754 | 205021 68877 3498751 50.8 | 1.355 % | c ============================================================================== c [1mFound solution: 351999[0m c ---[ 0]---> Sorter-cost: 5 Base: 3 3 3 3 2 3 3 3 3 3 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 69370 | 286939 672772 | 95646 69107 3514837 50.9 | 1.355 % | c | 69470 | 286939 672772 | 105210 69207 3517481 50.8 | 1.356 % | c ============================================================================== c [1mFound solution: 325754[0m c ---[ 0]---> Sorter-cost: 7 Base: 3 3 3 3 2 3 3 3 3 3 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 69603 | 286918 672729 | 95639 69339 3525718 50.8 | 1.356 % | c | 69703 | 286892 672670 | 105202 69438 3526373 50.8 | 1.370 % | c | 69853 | 286892 672670 | 115723 69588 3547742 51.0 | 1.370 % | c | 70079 | 286892 672670 | 127295 69814 3569348 51.1 | 1.370 % | c | 70416 | 286892 672670 | 140025 70151 3584009 51.1 | 1.370 % | c | 70924 | 286892 672670 | 154027 70659 3654183 51.7 | 1.370 % | c | 71683 | 286892 672670 | 169430 71418 3667043 51.3 | 1.370 % | c | 72822 | 286847 672568 | 186373 72554 3696020 50.9 | 1.382 % | c | 74530 | 286730 672304 | 205010 74256 3740046 50.4 | 1.415 % | c | 77092 | 286632 672083 | 225511 76816 4009626 52.2 | 1.440 % | c ============================================================================== c [1mFound solution: 325267[0m c ---[ 0]---> Sorter-cost: 9 Base: 3 3 3 3 2 3 3 3 3 3 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 79868 | 286603 672024 | 95534 79590 4117132 51.7 | 1.440 % | c | 79968 | 286505 671805 | 105087 79688 4120996 51.7 | 1.482 % | c | 80118 | 286505 671805 | 115596 79838 4127671 51.7 | 1.482 % | c | 80345 | 286505 671805 | 127155 80065 4142188 51.7 | 1.482 % | c ============================================================================== c [1mFound solution: 324891[0m c ---[ 0]---> Sorter-cost: 12 Base: 3 3 3 3 2 3 3 3 3 3 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 80640 | 286523 671924 | 95507 80360 4169092 51.9 | 1.482 % | c | 80740 | 286523 671924 | 105057 80460 4169528 51.8 | 1.483 % | c | 80890 | 286523 671924 | 115563 80610 4174709 51.8 | 1.483 % | c | 81115 | 286523 671924 | 127119 80835 4178907 51.7 | 1.483 % | c | 81452 | 286523 671924 | 139831 81172 4190033 51.6 | 1.483 % | c | 81958 | 286523 671924 | 153814 81678 4215423 51.6 | 1.483 % | c | 82717 | 286523 671924 | 169196 82437 4248696 51.5 | 1.483 % | c | 83856 | 286523 671924 | 186116 83576 4378185 52.4 | 1.483 % | c | 85565 | 286472 671808 | 204727 85284 4571724 53.6 | 1.496 % | c | 88129 | 286472 671808 | 225200 87848 4870692 55.4 | 1.496 % | c | 91973 | 286472 671808 | 247720 91692 5330851 58.1 | 1.496 % | c ============================================================================== c [1mFound solution: 324675[0m c ---[ 0]---> Sorter-cost: 12 Base: 3 3 3 3 2 3 3 3 3 3 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 94793 | 286465 671793 | 95488 94511 5591844 59.2 | 1.496 % | c | 94894 | 286465 671793 | 105036 94612 5592545 59.1 | 1.504 % | c | 95044 | 286465 671793 | 115540 94762 5594717 59.0 | 1.504 % | c | 95269 | 286465 671793 | 127094 94987 5596716 58.9 | 1.504 % | c | 95606 | 286465 671793 | 139803 95324 5616092 58.9 | 1.504 % | c | 96113 | 286465 671793 | 153784 95831 5651619 59.0 | 1.504 % | c | 96872 | 286465 671793 | 169162 96590 5684967 58.9 | 1.504 % | c ============================================================================== c [1mFound solution: 322839[0m c ---[ 0]---> Sorter-cost: 5 Base: 3 3 3 3 2 3 3 3 3 3 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 97234 | 286471 671807 | 95490 96952 5711630 58.9 | 1.504 % | c | 97334 | 286471 671807 | 105039 97052 5717178 58.9 | 1.505 % | c | 97484 | 286471 671807 | 115542 97202 5734519 59.0 | 1.505 % | c | 97709 | 286471 671807 | 127097 97427 5742109 58.9 | 1.505 % | c | 98046 | 286471 671807 | 139806 97764 5793815 59.3 | 1.505 % | c | 98554 | 286471 671807 | 153787 98272 5827995 59.3 | 1.505 % | c | 99315 | 286471 671807 | 169166 99033 5883452 59.4 | 1.505 % | c | 100454 | 286471 671807 | 186082 100172 5970295 59.6 | 1.505 % | c | 102162 | 286471 671807 | 204691 101880 6133092 60.2 | 1.505 % | c ============================================================================== c [1mFound solution: 322838[0m c ---[ 0]---> Sorter-cost: 4 Base: 3 3 3 3 2 3 3 3 3 3 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 102452 | 286404 671657 | 95468 102169 6157887 60.3 | 1.505 % | c | 102552 | 286404 671657 | 105014 31986 1235638 38.6 | 1.526 % | c | 102705 | 286404 671657 | 115516 32139 1236710 38.5 | 1.526 % | c | 102930 | 286404 671657 | 127067 32364 1251376 38.7 | 1.526 % | c | 103267 | 286404 671657 | 139774 32701 1270087 38.8 | 1.526 % | c ============================================================================== c [1mFound solution: 322837[0m c ---[ 0]---> Sorter-cost: 5 Base: 3 3 3 3 2 3 3 3 3 3 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 103418 | 286367 671574 | 95455 32851 1280341 39.0 | 1.526 % | c | 103519 | 286367 671574 | 105000 32952 1293027 39.2 | 1.540 % | c | 103669 | 286367 671574 | 115500 33102 1300251 39.3 | 1.540 % | c | 103895 | 286367 671574 | 127050 33328 1319175 39.6 | 1.540 % | c | 104232 | 286367 671574 | 139755 33665 1337270 39.7 | 1.540 % | c ============================================================================== c [1mFound solution: 322815[0m c ---[ 0]---> Sorter-cost: 11 Base: 3 3 3 3 2 3 3 3 3 3 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 104482 | 286377 671676 | 95459 33915 1366281 40.3 | 1.540 % | c | 104582 | 286377 671676 | 105004 34015 1372203 40.3 | 1.541 % | c | 104734 | 286377 671676 | 115505 34167 1378933 40.4 | 1.541 % | c | 104959 | 286377 671676 | 127055 34392 1386271 40.3 | 1.541 % | c | 105297 | 286377 671676 | 139761 34730 1407505 40.5 | 1.541 % | c | 105805 | 286377 671676 | 153737 35238 1445714 41.0 | 1.541 % | c ============================================================================== c [1mFound solution: 322803[0m c ---[ 0]---> Sorter-cost: 12 Base: 3 3 3 3 2 3 3 3 3 3 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 106109 | 286389 671708 | 95463 35542 1464879 41.2 | 1.541 % | c | 106209 | 286389 671708 | 105009 35642 1465756 41.1 | 1.542 % | c | 106359 | 286389 671708 | 115510 35792 1466498 41.0 | 1.542 % | c | 106585 | 286389 671708 | 127061 36018 1486837 41.3 | 1.542 % | c | 106923 | 286389 671708 | 139767 36356 1523724 41.9 | 1.542 % | c | 107429 | 286389 671708 | 153744 36862 1551729 42.1 | 1.542 % | c | 108189 | 286389 671708 | 169118 37622 1594362 42.4 | 1.542 % | c | 109329 | 286389 671708 | 186030 38762 1800693 46.5 | 1.542 % | c | 111038 | 286389 671708 | 204633 40471 1924175 47.5 | 1.542 % | c ============================================================================== c [1mFound solution: 322758[0m c ---[ 0]---> Sorter-cost: 8 Base: 3 3 3 3 2 3 3 3 3 3 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 111639 | 286398 671731 | 95466 41072 1983502 48.3 | 1.542 % | c | 111741 | 286398 671731 | 105012 41174 1991568 48.4 | 1.543 % | c | 111892 | 286398 671731 | 115513 41325 1999481 48.4 | 1.543 % | c | 112120 | 286398 671731 | 127065 41553 2036891 49.0 | 1.543 % | c | 112460 | 286392 671717 | 139771 41892 2039196 48.7 | 1.545 % | c | 112967 | 286249 671395 | 153748 42358 2072777 48.9 | 1.583 % | c ============================================================================== c [1mFound solution: 322756[0m c ---[ 0]---> Sorter-cost: 8 Base: 3 3 3 3 2 3 3 3 3 3 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 113407 | 286258 671420 | 95419 42798 2163613 50.6 | 1.583 % | c | 113507 | 286258 671420 | 104960 42898 2164127 50.4 | 1.583 % | c | 113658 | 286258 671420 | 115456 43049 2168960 50.4 | 1.583 % | c | 113884 | 286258 671420 | 127002 43275 2185067 50.5 | 1.583 % | c ============================================================================== c [1mFound solution: 322749[0m c ---[ 0]---> Sorter-cost: 9 Base: 3 3 3 3 2 3 3 3 3 3 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 114012 | 286267 671443 | 95422 43403 2215288 51.0 | 1.583 % | c | 114113 | 286267 671443 | 104964 43504 2217181 51.0 | 1.584 % | c | 114264 | 286237 671377 | 115460 43654 2230119 51.1 | 1.592 % | c | 114490 | 286237 671377 | 127006 43880 2242532 51.1 | 1.592 % | c | 114829 | 286237 671377 | 139707 44219 2259868 51.1 | 1.592 % | c | 115337 | 286233 671369 | 153678 44726 2305115 51.5 | 1.594 % | c ============================================================================== c [1mFound solution: 321363[0m c ---[ 0]---> Sorter-cost: 11 Base: 3 3 3 3 2 3 3 3 3 3 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 115687 | 286244 671397 | 95414 45076 2358047 52.3 | 1.594 % | c | 115787 | 286244 671397 | 104955 45176 2358575 52.2 | 1.595 % | c | 115938 | 286244 671397 | 115450 45327 2365104 52.2 | 1.595 % | c ============================================================================== c [1mFound solution: 321360[0m c ---[ 0]---> Sorter-cost: 13 Base: 3 3 3 3 2 3 3 3 3 3 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 116085 | 286258 671432 | 95419 45474 2385540 52.5 | 1.595 % | c | 116185 | 286258 671432 | 104960 45574 2387910 52.4 | 1.596 % | c | 116337 | 286258 671432 | 115456 45726 2399983 52.5 | 1.596 % | c | 116563 | 286258 671432 | 127002 45952 2434724 53.0 | 1.596 % | c | 116900 | 286237 671386 | 139702 46288 2472885 53.4 | 1.602 % | c | 117406 | 286237 671386 | 153673 46794 2485584 53.1 | 1.602 % | c ============================================================================== c [1mFound solution: 319923[0m c ---[ 0]---> Sorter-cost: 5 Base: 3 3 3 3 2 3 3 3 3 3 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 118136 | 286211 671329 | 95403 47523 2581249 54.3 | 1.602 % | c | 118237 | 286211 671329 | 104943 47624 2582560 54.2 | 1.612 % | c | 118389 | 286211 671329 | 115437 47776 2590145 54.2 | 1.612 % | c | 118614 | 286211 671329 | 126981 48001 2612706 54.4 | 1.612 % | c | 118956 | 286211 671329 | 139679 48343 2625316 54.3 | 1.612 % |
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/27473/stat): 27473 (minisat+_script) R 27472 27473 5299 0 -1 0 19 0 0 0 0 0 0 0 22 0 1 0 1855693918 712704 3 4294967295 134512640 135087896 3221224512 3221224512 1073744960 0 0 5 0 0 0 0 17 0 0 0 Raw data (/proc/27473/statm): 174 3 169 147 0 27 0 [pid=27473] 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=27474 New process pid=27475 New process pid=27476 execve syscall for /bin/sed executable One traced child (pid=27475) 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=27476) exited with status: 0 One traced child (pid=27474) exited with status: 0 New process pid=27477 execve syscall for /oldhome/oroussel/solvers/minisat+_64-bit_static executable open syscall for file /dev/null open syscall for file /oldhome/oroussel/tmp/wulflinc23/normalized-mps-v2-13-7-p0282.opb [startup+10.0035 s] Raw data (loadavg): 0.93 0.96 0.96 2/57 27477 Raw data (/proc/27473/stat): 27473 (minisat+_script) S 27472 27473 5299 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855693918 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27473/statm): 531 226 485 147 0 384 0 [pid=27473] vsize: 2124 Raw data (/proc/27477/stat): 27477 (minisat+_64-bit) R 27473 27473 5299 0 -1 0 8650 0 0 0 925 37 0 0 25 0 1 0 1855693923 38129664 8294 4294967295 134512640 135094434 3221224432 3221221616 134600246 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27477/statm): 9309 8294 145 145 0 9164 0 [pid=27477] vsize: 37236 Current children cumulated CPU time (s) 9.63 Current children cumulated vsize (Kb) 39360 [startup+20.0042 s] Raw data (loadavg): 0.94 0.96 0.96 2/57 27477 Raw data (/proc/27473/stat): 27473 (minisat+_script) S 27472 27473 5299 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855693918 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27473/statm): 531 226 485 147 0 384 0 [pid=27473] vsize: 2124 Raw data (/proc/27477/stat): 27477 (minisat+_64-bit) R 27473 27473 5299 0 -1 0 8718 0 0 0 1924 38 0 0 25 0 1 0 1855693923 38379520 8362 4294967295 134512640 135094434 3221224432 3221223120 134554700 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27477/statm): 9370 8362 145 145 0 9225 0 [pid=27477] vsize: 37480 Current children cumulated CPU time (s) 19.63 Current children cumulated vsize (Kb) 39604 [startup+30.0058 s] Raw data (loadavg): 0.95 0.96 0.96 2/57 27477 Raw data (/proc/27473/stat): 27473 (minisat+_script) S 27472 27473 5299 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855693918 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27473/statm): 531 226 485 147 0 384 0 [pid=27473] vsize: 2124 Raw data (/proc/27477/stat): 27477 (minisat+_64-bit) R 27473 27473 5299 0 -1 0 8791 0 0 0 2922 39 0 0 25 0 1 0 1855693923 38666240 8435 4294967295 134512640 135094434 3221224432 3221223088 134557893 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27477/statm): 9440 8435 145 145 0 9295 0 [pid=27477] vsize: 37760 Current children cumulated CPU time (s) 29.62 Current children cumulated vsize (Kb) 39884 [startup+40.0065 s] Raw data (loadavg): 0.96 0.96 0.96 2/57 27477 Raw data (/proc/27473/stat): 27473 (minisat+_script) S 27472 27473 5299 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855693918 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27473/statm): 531 226 485 147 0 384 0 [pid=27473] vsize: 2124 Raw data (/proc/27477/stat): 27477 (minisat+_64-bit) R 27473 27473 5299 0 -1 0 8843 0 0 0 3921 40 0 0 25 0 1 0 1855693923 38875136 8487 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27477/statm): 9491 8487 145 145 0 9346 0 [pid=27477] vsize: 37964 Current children cumulated CPU time (s) 39.62 Current children cumulated vsize (Kb) 40088 [startup+50.0081 s] Raw data (loadavg): 0.96 0.96 0.96 2/57 27477 Raw data (/proc/27473/stat): 27473 (minisat+_script) S 27472 27473 5299 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855693918 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27473/statm): 531 226 485 147 0 384 0 [pid=27473] vsize: 2124 Raw data (/proc/27477/stat): 27477 (minisat+_64-bit) R 27473 27473 5299 0 -1 0 8930 0 0 0 4919 41 0 0 25 0 1 0 1855693923 39251968 8574 4294967295 134512640 135094434 3221224432 3221223120 134554746 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27477/statm): 9583 8574 145 145 0 9438 0 [pid=27477] vsize: 38332 Current children cumulated CPU time (s) 49.61 Current children cumulated vsize (Kb) 40456 [startup+60.0087 s] Raw data (loadavg): 0.97 0.96 0.96 2/57 27477 Raw data (/proc/27473/stat): 27473 (minisat+_script) S 27472 27473 5299 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855693918 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27473/statm): 531 226 485 147 0 384 0 [pid=27473] vsize: 2124 Raw data (/proc/27477/stat): 27477 (minisat+_64-bit) R 27473 27473 5299 0 -1 0 8965 0 0 0 5918 41 0 0 25 0 1 0 1855693923 39391232 8609 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27477/statm): 9617 8609 145 145 0 9472 0 [pid=27477] vsize: 38468 Current children cumulated CPU time (s) 59.6 Current children cumulated vsize (Kb) 40592 [startup+70.0094 s] Raw data (loadavg): 0.97 0.96 0.96 2/57 27477 Raw data (/proc/27473/stat): 27473 (minisat+_script) S 27472 27473 5299 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855693918 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27473/statm): 531 226 485 147 0 384 0 [pid=27473] vsize: 2124 Raw data (/proc/27477/stat): 27477 (minisat+_64-bit) R 27473 27473 5299 0 -1 0 9050 0 0 0 6916 42 0 0 25 0 1 0 1855693923 39731200 8694 4294967295 134512640 135094434 3221224432 3221223120 134554746 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27477/statm): 9700 8694 145 145 0 9555 0 [pid=27477] vsize: 38800 Current children cumulated CPU time (s) 69.59 Current children cumulated vsize (Kb) 40924 [startup+80.01 s] Raw data (loadavg): 0.98 0.96 0.96 2/57 27477 Raw data (/proc/27473/stat): 27473 (minisat+_script) S 27472 27473 5299 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855693918 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27473/statm): 531 226 485 147 0 384 0 [pid=27473] vsize: 2124 Raw data (/proc/27477/stat): 27477 (minisat+_64-bit) T 27473 27473 5299 0 -1 0 9172 0 0 0 7914 43 0 0 25 0 1 0 1855693923 40222720 8816 4294967295 134512640 135094434 3221224432 3221222796 134870330 0 0 5 16386 3222434794 0 0 17 1 0 0 Raw data (/proc/27477/statm): 9820 8816 145 145 0 9675 0 [pid=27477] vsize: 39280 Current children cumulated CPU time (s) 79.58 Current children cumulated vsize (Kb) 41404 [startup+90.0106 s] Raw data (loadavg): 0.98 0.96 0.96 2/57 27477 Raw data (/proc/27473/stat): 27473 (minisat+_script) S 27472 27473 5299 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855693918 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27473/statm): 531 226 485 147 0 384 0 [pid=27473] vsize: 2124 Raw data (/proc/27477/stat): 27477 (minisat+_64-bit) R 27473 27473 5299 0 -1 0 9228 0 0 0 8912 44 0 0 25 0 1 0 1855693923 40448000 8872 4294967295 134512640 135094434 3221224432 3221223088 134558249 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27477/statm): 9875 8872 145 145 0 9730 0 [pid=27477] vsize: 39500 Current children cumulated CPU time (s) 89.57 Current children cumulated vsize (Kb) 41624 [startup+100.011 s] Raw data (loadavg): 0.98 0.96 0.96 2/57 27477 Raw data (/proc/27473/stat): 27473 (minisat+_script) S 27472 27473 5299 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855693918 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27473/statm): 531 226 485 147 0 384 0 [pid=27473] vsize: 2124 Raw data (/proc/27477/stat): 27477 (minisat+_64-bit) R 27473 27473 5299 0 -1 0 9302 0 0 0 9911 44 0 0 25 0 1 0 1855693923 40738816 8946 4294967295 134512640 135094434 3221224432 3221223076 134558261 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27477/statm): 9946 8946 145 145 0 9801 0 [pid=27477] vsize: 39784 Current children cumulated CPU time (s) 99.56 Current children cumulated vsize (Kb) 41908 [startup+110.012 s] Raw data (loadavg): 0.98 0.97 0.96 2/57 27477 Raw data (/proc/27473/stat): 27473 (minisat+_script) S 27472 27473 5299 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855693918 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27473/statm): 531 226 485 147 0 384 0 [pid=27473] vsize: 2124 Raw data (/proc/27477/stat): 27477 (minisat+_64-bit) R 27473 27473 5299 0 -1 0 9360 0 0 0 10911 45 0 0 25 0 1 0 1855693923 41025536 9004 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27477/statm): 10016 9004 145 145 0 9871 0 [pid=27477] vsize: 40064 Current children cumulated CPU time (s) 109.57 Current children cumulated vsize (Kb) 42188 [startup+120.013 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 27477 Raw data (/proc/27473/stat): 27473 (minisat+_script) S 27472 27473 5299 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855693918 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27473/statm): 531 226 485 147 0 384 0 [pid=27473] vsize: 2124 Raw data (/proc/27477/stat): 27477 (minisat+_64-bit) R 27473 27473 5299 0 -1 0 9427 0 0 0 11909 45 0 0 25 0 1 0 1855693923 41291776 9071 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27477/statm): 10081 9071 145 145 0 9936 0 [pid=27477] vsize: 40324 Current children cumulated CPU time (s) 119.55 Current children cumulated vsize (Kb) 42448 [startup+130.013 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 27477 Raw data (/proc/27473/stat): 27473 (minisat+_script) S 27472 27473 5299 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855693918 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27473/statm): 531 226 485 147 0 384 0 [pid=27473] vsize: 2124 Raw data (/proc/27477/stat): 27477 (minisat+_64-bit) R 27473 27473 5299 0 -1 0 9508 0 0 0 12909 46 0 0 25 0 1 0 1855693923 41619456 9152 4294967295 134512640 135094434 3221224432 3221223092 134553482 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27477/statm): 10161 9152 145 145 0 10016 0 [pid=27477] vsize: 40644 Current children cumulated CPU time (s) 129.56 Current children cumulated vsize (Kb) 42768 [startup+140.014 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 27477 Raw data (/proc/27473/stat): 27473 (minisat+_script) S 27472 27473 5299 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855693918 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27473/statm): 531 226 485 147 0 384 0 [pid=27473] vsize: 2124 Raw data (/proc/27477/stat): 27477 (minisat+_64-bit) R 27473 27473 5299 0 -1 0 9566 0 0 0 13908 47 0 0 25 0 1 0 1855693923 41852928 9210 4294967295 134512640 135094434 3221224432 3221223088 134557852 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27477/statm): 10218 9210 145 145 0 10073 0 [pid=27477] vsize: 40872 Current children cumulated CPU time (s) 139.56 Current children cumulated vsize (Kb) 42996 [startup+150.015 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 27477 Raw data (/proc/27473/stat): 27473 (minisat+_script) S 27472 27473 5299 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855693918 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27473/statm): 531 226 485 147 0 384 0 [pid=27473] vsize: 2124 Raw data (/proc/27477/stat): 27477 (minisat+_64-bit) R 27473 27473 5299 0 -1 0 9623 0 0 0 14907 47 0 0 25 0 1 0 1855693923 42057728 9267 4294967295 134512640 135094434 3221224432 3221223024 134557175 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27477/statm): 10268 9267 145 145 0 10123 0 [pid=27477] vsize: 41072 Current children cumulated CPU time (s) 149.55 Current children cumulated vsize (Kb) 43196 [startup+160.016 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 27477 Raw data (/proc/27473/stat): 27473 (minisat+_script) S 27472 27473 5299 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855693918 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27473/statm): 531 226 485 147 0 384 0 [pid=27473] vsize: 2124 Raw data (/proc/27477/stat): 27477 (minisat+_64-bit) T 27473 27473 5299 0 -1 0 9709 0 0 0 15905 48 0 0 25 0 1 0 1855693923 42397696 9353 4294967295 134512640 135094434 3221224432 3221222812 134870330 0 0 5 16386 3222434794 0 0 17 1 0 0 Raw data (/proc/27477/statm): 10351 9353 145 145 0 10206 0 [pid=27477] vsize: 41404 Current children cumulated CPU time (s) 159.54 Current children cumulated vsize (Kb) 43528 [startup+170.017 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 27477 Raw data (/proc/27473/stat): 27473 (minisat+_script) S 27472 27473 5299 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855693918 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27473/statm): 531 226 485 147 0 384 0 [pid=27473] vsize: 2124 Raw data (/proc/27477/stat): 27477 (minisat+_64-bit) R 27473 27473 5299 0 -1 0 9809 0 0 0 16903 49 0 0 25 0 1 0 1855693923 42799104 9453 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27477/statm): 10449 9453 145 145 0 10304 0 [pid=27477] vsize: 41796 Current children cumulated CPU time (s) 169.53 Current children cumulated vsize (Kb) 43920 [startup+180.018 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 27477 Raw data (/proc/27473/stat): 27473 (minisat+_script) S 27472 27473 5299 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855693918 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27473/statm): 531 226 485 147 0 384 0 [pid=27473] vsize: 2124 Raw data (/proc/27477/stat): 27477 (minisat+_64-bit) R 27473 27473 5299 0 -1 0 9924 0 0 0 17900 50 0 0 25 0 1 0 1855693923 43266048 9568 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27477/statm): 10563 9568 145 145 0 10418 0 [pid=27477] vsize: 42252 Current children cumulated CPU time (s) 179.51 Current children cumulated vsize (Kb) 44376 [startup+190.019 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 27477 Raw data (/proc/27473/stat): 27473 (minisat+_script) S 27472 27473 5299 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855693918 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27473/statm): 531 226 485 147 0 384 0 [pid=27473] vsize: 2124 Raw data (/proc/27477/stat): 27477 (minisat+_64-bit) R 27473 27473 5299 0 -1 0 9987 0 0 0 18899 51 0 0 25 0 1 0 1855693923 43520000 9631 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27477/statm): 10625 9631 145 145 0 10480 0 [pid=27477] vsize: 42500 Current children cumulated CPU time (s) 189.51 Current children cumulated vsize (Kb) 44624 [startup+200.02 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 27477 Raw data (/proc/27473/stat): 27473 (minisat+_script) S 27472 27473 5299 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855693918 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27473/statm): 531 226 485 147 0 384 0 [pid=27473] vsize: 2124 Raw data (/proc/27477/stat): 27477 (minisat+_64-bit) R 27473 27473 5299 0 -1 0 10080 0 0 0 19898 52 0 0 25 0 1 0 1855693923 43888640 9724 4294967295 134512640 135094434 3221224432 3221223088 134557813 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27477/statm): 10715 9724 145 145 0 10570 0 [pid=27477] vsize: 42860 Current children cumulated CPU time (s) 199.51 Current children cumulated vsize (Kb) 44984 [startup+210.02 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 27477 Raw data (/proc/27473/stat): 27473 (minisat+_script) S 27472 27473 5299 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855693918 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27473/statm): 531 226 485 147 0 384 0 [pid=27473] vsize: 2124 Raw data (/proc/27477/stat): 27477 (minisat+_64-bit) R 27473 27473 5299 0 -1 0 10193 0 0 0 20896 52 0 0 25 0 1 0 1855693923 44478464 9837 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27477/statm): 10859 9837 145 145 0 10714 0 [pid=27477] vsize: 43436 Current children cumulated CPU time (s) 209.49 Current children cumulated vsize (Kb) 45560 [startup+220.02 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 27477 Raw data (/proc/27473/stat): 27473 (minisat+_script) S 27472 27473 5299 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855693918 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27473/statm): 531 226 485 147 0 384 0 [pid=27473] vsize: 2124 Raw data (/proc/27477/stat): 27477 (minisat+_64-bit) R 27473 27473 5299 0 -1 0 10221 0 0 0 21896 53 0 0 25 0 1 0 1855693923 44584960 9865 4294967295 134512640 135094434 3221224432 3221223056 134557565 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27477/statm): 10885 9865 145 145 0 10740 0 [pid=27477] vsize: 43540 Current children cumulated CPU time (s) 219.5 Current children cumulated vsize (Kb) 45664 [startup+230.021 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 27477 Raw data (/proc/27473/stat): 27473 (minisat+_script) S 27472 27473 5299 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855693918 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27473/statm): 531 226 485 147 0 384 0 [pid=27473] vsize: 2124 Raw data (/proc/27477/stat): 27477 (minisat+_64-bit) R 27473 27473 5299 0 -1 0 10355 0 0 0 22895 54 0 0 25 0 1 0 1855693923 45240320 9999 4294967295 134512640 135094434 3221224432 3221223252 134558984 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27477/statm): 11045 9999 145 145 0 10900 0 [pid=27477] vsize: 44180 Current children cumulated CPU time (s) 229.5 Current children cumulated vsize (Kb) 46304 [startup+240.021 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 27477 Raw data (/proc/27473/stat): 27473 (minisat+_script) S 27472 27473 5299 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855693918 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27473/statm): 531 226 485 147 0 384 0 [pid=27473] vsize: 2124 Raw data (/proc/27477/stat): 27477 (minisat+_64-bit) R 27473 27473 5299 0 -1 0 10404 0 0 0 23894 54 0 0 25 0 1 0 1855693923 45436928 10048 4294967295 134512640 135094434 3221224432 3221221984 134600314 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27477/statm): 11093 10048 145 145 0 10948 0 [pid=27477] vsize: 44372 Current children cumulated CPU time (s) 239.49 Current children cumulated vsize (Kb) 46496 [startup+250.022 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 27477 Raw data (/proc/27473/stat): 27473 (minisat+_script) S 27472 27473 5299 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855693918 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27473/statm): 531 226 485 147 0 384 0 [pid=27473] vsize: 2124 Raw data (/proc/27477/stat): 27477 (minisat+_64-bit) R 27473 27473 5299 0 -1 0 10426 0 0 0 24893 54 0 0 25 0 1 0 1855693923 45522944 10070 4294967295 134512640 135094434 3221224432 3221223088 134557879 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27477/statm): 11114 10070 145 145 0 10969 0 [pid=27477] vsize: 44456 Current children cumulated CPU time (s) 249.48 Current children cumulated vsize (Kb) 46580 [startup+260.023 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 27477 Raw data (/proc/27473/stat): 27473 (minisat+_script) S 27472 27473 5299 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855693918 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27473/statm): 531 226 485 147 0 384 0 [pid=27473] vsize: 2124 Raw data (/proc/27477/stat): 27477 (minisat+_64-bit) R 27473 27473 5299 0 -1 0 10478 0 0 0 25893 55 0 0 25 0 1 0 1855693923 45731840 10122 4294967295 134512640 135094434 3221224432 3221223120 134554746 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27477/statm): 11165 10122 145 145 0 11020 0 [pid=27477] vsize: 44660 Current children cumulated CPU time (s) 259.49 Current children cumulated vsize (Kb) 46784 [startup+270.023 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 27477 Raw data (/proc/27473/stat): 27473 (minisat+_script) S 27472 27473 5299 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855693918 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27473/statm): 531 226 485 147 0 384 0 [pid=27473] vsize: 2124 Raw data (/proc/27477/stat): 27477 (minisat+_64-bit) R 27473 27473 5299 0 -1 0 10602 0 0 0 26891 55 0 0 25 0 1 0 1855693923 46235648 10246 4294967295 134512640 135094434 3221224432 3221223088 134558395 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27477/statm): 11288 10246 145 145 0 11143 0 [pid=27477] vsize: 45152 Current children cumulated CPU time (s) 269.47 Current children cumulated vsize (Kb) 47276 [startup+280.024 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 27477 Raw data (/proc/27473/stat): 27473 (minisat+_script) S 27472 27473 5299 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855693918 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27473/statm): 531 226 485 147 0 384 0 [pid=27473] vsize: 2124 Raw data (/proc/27477/stat): 27477 (minisat+_64-bit) R 27473 27473 5299 0 -1 0 10707 0 0 0 27889 56 0 0 25 0 1 0 1855693923 46657536 10351 4294967295 134512640 135094434 3221224432 3221223056 134557737 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27477/statm): 11391 10351 145 145 0 11246 0 [pid=27477] vsize: 45564 Current children cumulated CPU time (s) 279.46 Current children cumulated vsize (Kb) 47688 [startup+290.024 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 27477 Raw data (/proc/27473/stat): 27473 (minisat+_script) S 27472 27473 5299 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855693918 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27473/statm): 531 226 485 147 0 384 0 [pid=27473] vsize: 2124 Raw data (/proc/27477/stat): 27477 (minisat+_64-bit) R 27473 27473 5299 0 -1 0 10779 0 0 0 28889 57 0 0 25 0 1 0 1855693923 46948352 10423 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27477/statm): 11462 10423 145 145 0 11317 0 [pid=27477] vsize: 45848 Current children cumulated CPU time (s) 289.47 Current children cumulated vsize (Kb) 47972 [startup+300.026 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 27477 Raw data (/proc/27473/stat): 27473 (minisat+_script) S 27472 27473 5299 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855693918 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27473/statm): 531 226 485 147 0 384 0 [pid=27473] vsize: 2124 Raw data (/proc/27477/stat): 27477 (minisat+_64-bit) R 27473 27473 5299 0 -1 0 10862 0 0 0 29888 57 0 0 25 0 1 0 1855693923 47284224 10506 4294967295 134512640 135094434 3221224432 3221223088 134558210 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27477/statm): 11544 10506 145 145 0 11399 0 [pid=27477] vsize: 46176 Current children cumulated CPU time (s) 299.46 Current children cumulated vsize (Kb) 48300 [startup+310.027 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 27477 Raw data (/proc/27473/stat): 27473 (minisat+_script) S 27472 27473 5299 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855693918 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27473/statm): 531 226 485 147 0 384 0 [pid=27473] vsize: 2124 Raw data (/proc/27477/stat): 27477 (minisat+_64-bit) R 27473 27473 5299 0 -1 0 10942 0 0 0 30887 58 0 0 25 0 1 0 1855693923 47611904 10586 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27477/statm): 11624 10586 145 145 0 11479 0 [pid=27477] vsize: 46496 Current children cumulated CPU time (s) 309.46 Current children cumulated vsize (Kb) 48620 [startup+320.026 s] Raw data (loadavg): 0.99 0.97 0.96 1/57 27477 Raw data (/proc/27473/stat): 27473 (minisat+_script) S 27472 27473 5299 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855693918 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27473/statm): 531 226 485 147 0 384 0 [pid=27473] vsize: 2124 Raw data (/proc/27477/stat): 27477 (minisat+_64-bit) T 27473 27473 5299 0 -1 0 11033 0 0 0 31885 59 0 0 25 0 1 0 1855693923 47980544 10677 4294967295 134512640 135094434 3221224432 3221222812 134870330 0 0 5 16386 3222434794 0 0 17 1 0 0 Raw data (/proc/27477/statm): 11714 10677 145 145 0 11569 0 [pid=27477] vsize: 46856 Current children cumulated CPU time (s) 319.45 Current children cumulated vsize (Kb) 48980 [startup+330.028 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 27477 Raw data (/proc/27473/stat): 27473 (minisat+_script) S 27472 27473 5299 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855693918 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27473/statm): 531 226 485 147 0 384 0 [pid=27473] vsize: 2124 Raw data (/proc/27477/stat): 27477 (minisat+_64-bit) R 27473 27473 5299 0 -1 0 11139 0 0 0 32884 59 0 0 25 0 1 0 1855693923 48410624 10783 4294967295 134512640 135094434 3221224432 3221223088 134558004 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27477/statm): 11819 10783 145 145 0 11674 0 [pid=27477] vsize: 47276 Current children cumulated CPU time (s) 329.44 Current children cumulated vsize (Kb) 49400 [startup+340.029 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 27477 Raw data (/proc/27473/stat): 27473 (minisat+_script) S 27472 27473 5299 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855693918 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27473/statm): 531 226 485 147 0 384 0 [pid=27473] vsize: 2124 Raw data (/proc/27477/stat): 27477 (minisat+_64-bit) R 27473 27473 5299 0 -1 0 11219 0 0 0 33882 60 0 0 25 0 1 0 1855693923 48734208 10863 4294967295 134512640 135094434 3221224432 3221223072 134562165 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27477/statm): 11898 10863 145 145 0 11753 0 [pid=27477] vsize: 47592 Current children cumulated CPU time (s) 339.43 Current children cumulated vsize (Kb) 49716 [startup+350.029 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 27477 Raw data (/proc/27473/stat): 27473 (minisat+_script) S 27472 27473 5299 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855693918 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27473/statm): 531 226 485 147 0 384 0 [pid=27473] vsize: 2124 Raw data (/proc/27477/stat): 27477 (minisat+_64-bit) R 27473 27473 5299 0 -1 0 11310 0 0 0 34880 62 0 0 25 0 1 0 1855693923 49102848 10954 4294967295 134512640 135094434 3221224432 3221223024 134556851 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27477/statm): 11988 10954 145 145 0 11843 0 [pid=27477] vsize: 47952 Current children cumulated CPU time (s) 349.43 Current children cumulated vsize (Kb) 50076 [startup+360.03 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 27477 Raw data (/proc/27473/stat): 27473 (minisat+_script) S 27472 27473 5299 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855693918 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27473/statm): 531 226 485 147 0 384 0 [pid=27473] vsize: 2124 Raw data (/proc/27477/stat): 27477 (minisat+_64-bit) R 27473 27473 5299 0 -1 0 11363 0 0 0 35878 63 0 0 25 0 1 0 1855693923 49319936 11007 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27477/statm): 12041 11007 145 145 0 11896 0 [pid=27477] vsize: 48164 Current children cumulated CPU time (s) 359.42 Current children cumulated vsize (Kb) 50288 [startup+370.031 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 27477 Raw data (/proc/27473/stat): 27473 (minisat+_script) S 27472 27473 5299 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855693918 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27473/statm): 531 226 485 147 0 384 0 [pid=27473] vsize: 2124 Raw data (/proc/27477/stat): 27477 (minisat+_64-bit) R 27473 27473 5299 0 -1 0 11425 0 0 0 36877 64 0 0 25 0 1 0 1855693923 49569792 11069 4294967295 134512640 135094434 3221224432 3221221984 134677366 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27477/statm): 12102 11069 145 145 0 11957 0 [pid=27477] vsize: 48408 Current children cumulated CPU time (s) 369.42 Current children cumulated vsize (Kb) 50532 [startup+380.031 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 27477 Raw data (/proc/27473/stat): 27473 (minisat+_script) S 27472 27473 5299 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855693918 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27473/statm): 531 226 485 147 0 384 0 [pid=27473] vsize: 2124 Raw data (/proc/27477/stat): 27477 (minisat+_64-bit) R 27473 27473 5299 0 -1 0 11445 0 0 0 37877 64 0 0 25 0 1 0 1855693923 49647616 11089 4294967295 134512640 135094434 3221224432 3221223120 134554746 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27477/statm): 12121 11089 145 145 0 11976 0 [pid=27477] vsize: 48484 Current children cumulated CPU time (s) 379.42 Current children cumulated vsize (Kb) 50608 [startup+390.032 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 27477 Raw data (/proc/27473/stat): 27473 (minisat+_script) S 27472 27473 5299 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855693918 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27473/statm): 531 226 485 147 0 384 0 [pid=27473] vsize: 2124 Raw data (/proc/27477/stat): 27477 (minisat+_64-bit) R 27473 27473 5299 0 -1 0 11556 0 0 0 38874 66 0 0 25 0 1 0 1855693923 50094080 11200 4294967295 134512640 135094434 3221224432 3221223088 134558289 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27477/statm): 12230 11200 145 145 0 12085 0 [pid=27477] vsize: 48920 Current children cumulated CPU time (s) 389.41 Current children cumulated vsize (Kb) 51044 [startup+400.033 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 27477 Raw data (/proc/27473/stat): 27473 (minisat+_script) S 27472 27473 5299 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855693918 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27473/statm): 531 226 485 147 0 384 0 [pid=27473] vsize: 2124 Raw data (/proc/27477/stat): 27477 (minisat+_64-bit) R 27473 27473 5299 0 -1 0 11637 0 0 0 39873 67 0 0 25 0 1 0 1855693923 50421760 11281 4294967295 134512640 135094434 3221224432 3221223120 134554746 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27477/statm): 12310 11281 145 145 0 12165 0 [pid=27477] vsize: 49240 Current children cumulated CPU time (s) 399.41 Current children cumulated vsize (Kb) 51364 [startup+410.033 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 27477 Raw data (/proc/27473/stat): 27473 (minisat+_script) S 27472 27473 5299 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855693918 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27473/statm): 531 226 485 147 0 384 0 [pid=27473] vsize: 2124 Raw data (/proc/27477/stat): 27477 (minisat+_64-bit) R 27473 27473 5299 0 -1 0 11735 0 0 0 40871 68 0 0 25 0 1 0 1855693923 50819072 11379 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27477/statm): 12407 11379 145 145 0 12262 0 [pid=27477] vsize: 49628 Current children cumulated CPU time (s) 409.4 Current children cumulated vsize (Kb) 51752 [startup+420.034 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 27477 Raw data (/proc/27473/stat): 27473 (minisat+_script) S 27472 27473 5299 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855693918 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27473/statm): 531 226 485 147 0 384 0 [pid=27473] vsize: 2124 Raw data (/proc/27477/stat): 27477 (minisat+_64-bit) R 27473 27473 5299 0 -1 0 11773 0 0 0 41871 68 0 0 25 0 1 0 1855693923 50974720 11417 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27477/statm): 12445 11417 145 145 0 12300 0 [pid=27477] vsize: 49780 Current children cumulated CPU time (s) 419.4 Current children cumulated vsize (Kb) 51904 [startup+430.034 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 27477 Raw data (/proc/27473/stat): 27473 (minisat+_script) S 27472 27473 5299 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855693918 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27473/statm): 531 226 485 147 0 384 0 [pid=27473] vsize: 2124 Raw data (/proc/27477/stat): 27477 (minisat+_64-bit) R 27473 27473 5299 0 -1 0 11846 0 0 0 42870 69 0 0 25 0 1 0 1855693923 51265536 11490 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27477/statm): 12516 11490 145 145 0 12371 0 [pid=27477] vsize: 50064 Current children cumulated CPU time (s) 429.4 Current children cumulated vsize (Kb) 52188 [startup+440.035 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 27477 Raw data (/proc/27473/stat): 27473 (minisat+_script) S 27472 27473 5299 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855693918 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27473/statm): 531 226 485 147 0 384 0 [pid=27473] vsize: 2124 Raw data (/proc/27477/stat): 27477 (minisat+_64-bit) R 27473 27473 5299 0 -1 0 11925 0 0 0 43869 70 0 0 25 0 1 0 1855693923 51585024 11569 4294967295 134512640 135094434 3221224432 3221223056 134557565 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27477/statm): 12594 11569 145 145 0 12449 0 [pid=27477] vsize: 50376 Current children cumulated CPU time (s) 439.4 Current children cumulated vsize (Kb) 52500 [startup+450.037 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 27477 Raw data (/proc/27473/stat): 27473 (minisat+_script) S 27472 27473 5299 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855693918 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27473/statm): 531 226 485 147 0 384 0 [pid=27473] vsize: 2124 Raw data (/proc/27477/stat): 27477 (minisat+_64-bit) R 27473 27473 5299 0 -1 0 12002 0 0 0 44867 71 0 0 25 0 1 0 1855693923 51900416 11646 4294967295 134512640 135094434 3221224432 3221223060 134557564 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27477/statm): 12671 11646 145 145 0 12526 0 [pid=27477] vsize: 50684 Current children cumulated CPU time (s) 449.39 Current children cumulated vsize (Kb) 52808 [startup+460.037 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 27477 Raw data (/proc/27473/stat): 27473 (minisat+_script) S 27472 27473 5299 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855693918 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27473/statm): 531 226 485 147 0 384 0 [pid=27473] vsize: 2124 Raw data (/proc/27477/stat): 27477 (minisat+_64-bit) R 27473 27473 5299 0 -1 0 12043 0 0 0 45867 72 0 0 25 0 1 0 1855693923 52064256 11687 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27477/statm): 12711 11687 145 145 0 12566 0 [pid=27477] vsize: 50844 Current children cumulated CPU time (s) 459.4 Current children cumulated vsize (Kb) 52968 [startup+470.037 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 27477 Raw data (/proc/27473/stat): 27473 (minisat+_script) S 27472 27473 5299 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855693918 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27473/statm): 531 226 485 147 0 384 0 [pid=27473] vsize: 2124 Raw data (/proc/27477/stat): 27477 (minisat+_64-bit) R 27473 27473 5299 0 -1 0 12086 0 0 0 46866 72 0 0 25 0 1 0 1855693923 52236288 11730 4294967295 134512640 135094434 3221224432 3221223088 134558395 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27477/statm): 12753 11730 145 145 0 12608 0 [pid=27477] vsize: 51012 Current children cumulated CPU time (s) 469.39 Current children cumulated vsize (Kb) 53136 [startup+480.039 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 27477 Raw data (/proc/27473/stat): 27473 (minisat+_script) S 27472 27473 5299 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855693918 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27473/statm): 531 226 485 147 0 384 0 [pid=27473] vsize: 2124 Raw data (/proc/27477/stat): 27477 (minisat+_64-bit) R 27473 27473 5299 0 -1 0 12154 0 0 0 47865 73 0 0 25 0 1 0 1855693923 52510720 11798 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27477/statm): 12820 11798 145 145 0 12675 0 [pid=27477] vsize: 51280 Current children cumulated CPU time (s) 479.39 Current children cumulated vsize (Kb) 53404 [startup+490.039 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 27477 Raw data (/proc/27473/stat): 27473 (minisat+_script) S 27472 27473 5299 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855693918 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27473/statm): 531 226 485 147 0 384 0 [pid=27473] vsize: 2124 Raw data (/proc/27477/stat): 27477 (minisat+_64-bit) R 27473 27473 5299 0 -1 0 12233 0 0 0 48864 74 0 0 25 0 1 0 1855693923 52834304 11877 4294967295 134512640 135094434 3221224432 3221223104 134555931 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27477/statm): 12899 11877 145 145 0 12754 0 [pid=27477] vsize: 51596 Current children cumulated CPU time (s) 489.39 Current children cumulated vsize (Kb) 53720 [startup+500.04 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 27477 Raw data (/proc/27473/stat): 27473 (minisat+_script) S 27472 27473 5299 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855693918 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27473/statm): 531 226 485 147 0 384 0 [pid=27473] vsize: 2124 Raw data (/proc/27477/stat): 27477 (minisat+_64-bit) R 27473 27473 5299 0 -1 0 12309 0 0 0 49863 75 0 0 25 0 1 0 1855693923 53141504 11953 4294967295 134512640 135094434 3221224432 3221223184 134559282 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27477/statm): 12974 11953 145 145 0 12829 0 [pid=27477] vsize: 51896 Current children cumulated CPU time (s) 499.39 Current children cumulated vsize (Kb) 54020 [startup+510.041 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 27477 Raw data (/proc/27473/stat): 27473 (minisat+_script) S 27472 27473 5299 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855693918 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27473/statm): 531 226 485 147 0 384 0 [pid=27473] vsize: 2124 Raw data (/proc/27477/stat): 27477 (minisat+_64-bit) R 27473 27473 5299 0 -1 0 12379 0 0 0 50861 75 0 0 25 0 1 0 1855693923 53428224 12023 4294967295 134512640 135094434 3221224432 3221223056 134557724 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27477/statm): 13044 12023 145 145 0 12899 0 [pid=27477] vsize: 52176 Current children cumulated CPU time (s) 509.37 Current children cumulated vsize (Kb) 54300 [startup+520.04 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 27477 Raw data (/proc/27473/stat): 27473 (minisat+_script) S 27472 27473 5299 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855693918 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27473/statm): 531 226 485 147 0 384 0 [pid=27473] vsize: 2124 Raw data (/proc/27477/stat): 27477 (minisat+_64-bit) R 27473 27473 5299 0 -1 0 12484 0 0 0 51859 76 0 0 25 0 1 0 1855693923 53850112 12128 4294967295 134512640 135094434 3221224432 3221223044 134563046 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27477/statm): 13147 12128 145 145 0 13002 0 [pid=27477] vsize: 52588 Current children cumulated CPU time (s) 519.36 Current children cumulated vsize (Kb) 54712 [startup+530.041 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 27477 Raw data (/proc/27473/stat): 27473 (minisat+_script) S 27472 27473 5299 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855693918 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27473/statm): 531 226 485 147 0 384 0 [pid=27473] vsize: 2124 Raw data (/proc/27477/stat): 27477 (minisat+_64-bit) R 27473 27473 5299 0 -1 0 12553 0 0 0 52858 77 0 0 25 0 1 0 1855693923 54128640 12197 4294967295 134512640 135094434 3221224432 3221223024 134557037 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27477/statm): 13215 12197 145 145 0 13070 0 [pid=27477] vsize: 52860 Current children cumulated CPU time (s) 529.36 Current children cumulated vsize (Kb) 54984 [startup+540.042 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 27477 Raw data (/proc/27473/stat): 27473 (minisat+_script) S 27472 27473 5299 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855693918 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27473/statm): 531 226 485 147 0 384 0 [pid=27473] vsize: 2124 Raw data (/proc/27477/stat): 27477 (minisat+_64-bit) R 27473 27473 5299 0 -1 0 12601 0 0 0 53857 77 0 0 25 0 1 0 1855693923 54583296 12245 4294967295 134512640 135094434 3221224432 3221223088 134558289 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27477/statm): 13326 12245 145 145 0 13181 0 [pid=27477] vsize: 53304 Current children cumulated CPU time (s) 539.35 Current children cumulated vsize (Kb) 55428 [startup+550.043 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 27477 Raw data (/proc/27473/stat): 27473 (minisat+_script) S 27472 27473 5299 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855693918 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27473/statm): 531 226 485 147 0 384 0 [pid=27473] vsize: 2124 Raw data (/proc/27477/stat): 27477 (minisat+_64-bit) R 27473 27473 5299 0 -1 0 12655 0 0 0 54856 78 0 0 25 0 1 0 1855693923 54804480 12299 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27477/statm): 13380 12299 145 145 0 13235 0 [pid=27477] vsize: 53520 Current children cumulated CPU time (s) 549.35 Current children cumulated vsize (Kb) 55644 [startup+560.044 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 27477 Raw data (/proc/27473/stat): 27473 (minisat+_script) S 27472 27473 5299 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855693918 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27473/statm): 531 226 485 147 0 384 0 [pid=27473] vsize: 2124 Raw data (/proc/27477/stat): 27477 (minisat+_64-bit) R 27473 27473 5299 0 -1 0 12697 0 0 0 55856 78 0 0 25 0 1 0 1855693923 54972416 12341 4294967295 134512640 135094434 3221224432 3221223120 134554746 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27477/statm): 13421 12341 145 145 0 13276 0 [pid=27477] vsize: 53684 Current children cumulated CPU time (s) 559.35 Current children cumulated vsize (Kb) 55808 [startup+570.044 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 27477 Raw data (/proc/27473/stat): 27473 (minisat+_script) S 27472 27473 5299 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855693918 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27473/statm): 531 226 485 147 0 384 0 [pid=27473] vsize: 2124 Raw data (/proc/27477/stat): 27477 (minisat+_64-bit) R 27473 27473 5299 0 -1 0 12738 0 0 0 56855 79 0 0 25 0 1 0 1855693923 55136256 12382 4294967295 134512640 135094434 3221224432 3221223088 134558159 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27477/statm): 13461 12382 145 145 0 13316 0 [pid=27477] vsize: 53844 Current children cumulated CPU time (s) 569.35 Current children cumulated vsize (Kb) 55968 [startup+580.045 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 27477 Raw data (/proc/27473/stat): 27473 (minisat+_script) S 27472 27473 5299 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855693918 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27473/statm): 531 226 485 147 0 384 0 [pid=27473] vsize: 2124 Raw data (/proc/27477/stat): 27477 (minisat+_64-bit) R 27473 27473 5299 0 -1 0 12809 0 0 0 57854 79 0 0 25 0 1 0 1855693923 55422976 12453 4294967295 134512640 135094434 3221224432 3221221632 134676539 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27477/statm): 13531 12453 145 145 0 13386 0 [pid=27477] vsize: 54124 Current children cumulated CPU time (s) 579.34 Current children cumulated vsize (Kb) 56248 [startup+590.046 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 27477 Raw data (/proc/27473/stat): 27473 (minisat+_script) S 27472 27473 5299 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855693918 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27473/statm): 531 226 485 147 0 384 0 [pid=27473] vsize: 2124 Raw data (/proc/27477/stat): 27477 (minisat+_64-bit) R 27473 27473 5299 0 -1 0 12840 0 0 0 58853 80 0 0 25 0 1 0 1855693923 55549952 12484 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27477/statm): 13562 12484 145 145 0 13417 0 [pid=27477] vsize: 54248 Current children cumulated CPU time (s) 589.34 Current children cumulated vsize (Kb) 56372 [startup+600.046 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 27477 Raw data (/proc/27473/stat): 27473 (minisat+_script) S 27472 27473 5299 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855693918 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27473/statm): 531 226 485 147 0 384 0 [pid=27473] vsize: 2124 Raw data (/proc/27477/stat): 27477 (minisat+_64-bit) R 27473 27473 5299 0 -1 0 12925 0 0 0 59852 81 0 0 25 0 1 0 1855693923 55889920 12569 4294967295 134512640 135094434 3221224432 3221223120 134554750 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27477/statm): 13645 12569 145 145 0 13500 0 [pid=27477] vsize: 54580 Current children cumulated CPU time (s) 599.34 Current children cumulated vsize (Kb) 56704 [startup+610.047 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 27477 Raw data (/proc/27473/stat): 27473 (minisat+_script) S 27472 27473 5299 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855693918 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27473/statm): 531 226 485 147 0 384 0 [pid=27473] vsize: 2124 Raw data (/proc/27477/stat): 27477 (minisat+_64-bit) R 27473 27473 5299 0 -1 0 13020 0 0 0 60850 81 0 0 25 0 1 0 1855693923 56266752 12664 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27477/statm): 13737 12664 145 145 0 13592 0 [pid=27477] vsize: 54948 Current children cumulated CPU time (s) 609.32 Current children cumulated vsize (Kb) 57072 [startup+620.048 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 27477 Raw data (/proc/27473/stat): 27473 (minisat+_script) S 27472 27473 5299 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855693918 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27473/statm): 531 226 485 147 0 384 0 [pid=27473] vsize: 2124 Raw data (/proc/27477/stat): 27477 (minisat+_64-bit) R 27473 27473 5299 0 -1 0 13091 0 0 0 61849 82 0 0 25 0 1 0 1855693923 56553472 12735 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27477/statm): 13807 12735 145 145 0 13662 0 [pid=27477] vsize: 55228 Current children cumulated CPU time (s) 619.32 Current children cumulated vsize (Kb) 57352 [startup+630.048 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 27477 Raw data (/proc/27473/stat): 27473 (minisat+_script) S 27472 27473 5299 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855693918 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27473/statm): 531 226 485 147 0 384 0 [pid=27473] vsize: 2124 Raw data (/proc/27477/stat): 27477 (minisat+_64-bit) R 27473 27473 5299 0 -1 0 13163 0 0 0 62848 82 0 0 25 0 1 0 1855693923 56844288 12807 4294967295 134512640 135094434 3221224432 3221223056 134562104 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27477/statm): 13878 12807 145 145 0 13733 0 [pid=27477] vsize: 55512 Current children cumulated CPU time (s) 629.31 Current children cumulated vsize (Kb) 57636 [startup+640.049 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 27477 Raw data (/proc/27473/stat): 27473 (minisat+_script) S 27472 27473 5299 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855693918 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27473/statm): 531 226 485 147 0 384 0 [pid=27473] vsize: 2124 Raw data (/proc/27477/stat): 27477 (minisat+_64-bit) R 27473 27473 5299 0 -1 0 13223 0 0 0 63847 82 0 0 25 0 1 0 1855693923 57090048 12867 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27477/statm): 13938 12867 145 145 0 13793 0 [pid=27477] vsize: 55752 Current children cumulated CPU time (s) 639.3 Current children cumulated vsize (Kb) 57876 [startup+650.051 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 27477 Raw data (/proc/27473/stat): 27473 (minisat+_script) S 27472 27473 5299 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855693918 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27473/statm): 531 226 485 147 0 384 0 [pid=27473] vsize: 2124 Raw data (/proc/27477/stat): 27477 (minisat+_64-bit) R 27473 27473 5299 0 -1 0 13300 0 0 0 64846 83 0 0 25 0 1 0 1855693923 57405440 12944 4294967295 134512640 135094434 3221224432 3221223056 134557596 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27477/statm): 14015 12944 145 145 0 13870 0 [pid=27477] vsize: 56060 Current children cumulated CPU time (s) 649.3 Current children cumulated vsize (Kb) 58184 [startup+660.051 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 27477 Raw data (/proc/27473/stat): 27473 (minisat+_script) S 27472 27473 5299 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855693918 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27473/statm): 531 226 485 147 0 384 0 [pid=27473] vsize: 2124 Raw data (/proc/27477/stat): 27477 (minisat+_64-bit) R 27473 27473 5299 0 -1 0 13381 0 0 0 65845 83 0 0 25 0 1 0 1855693923 57729024 13025 4294967295 134512640 135094434 3221224432 3221223088 134558249 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27477/statm): 14094 13025 145 145 0 13949 0 [pid=27477] vsize: 56376 Current children cumulated CPU time (s) 659.29 Current children cumulated vsize (Kb) 58500 [startup+670.052 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 27477 Raw data (/proc/27473/stat): 27473 (minisat+_script) S 27472 27473 5299 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855693918 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27473/statm): 531 226 485 147 0 384 0 [pid=27473] vsize: 2124 Raw data (/proc/27477/stat): 27477 (minisat+_64-bit) R 27473 27473 5299 0 -1 0 13433 0 0 0 66845 84 0 0 25 0 1 0 1855693923 57937920 13077 4294967295 134512640 135094434 3221224432 3221223076 134558261 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27477/statm): 14145 13077 145 145 0 14000 0 [pid=27477] vsize: 56580 Current children cumulated CPU time (s) 669.3 Current children cumulated vsize (Kb) 58704 [startup+680.053 s] Raw data (loadavg): 1.07 0.99 0.96 2/57 27477 Raw data (/proc/27473/stat): 27473 (minisat+_script) S 27472 27473 5299 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855693918 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27473/statm): 531 226 485 147 0 384 0 [pid=27473] vsize: 2124 Raw data (/proc/27477/stat): 27477 (minisat+_64-bit) R 27473 27473 5299 0 -1 0 13486 0 0 0 67845 84 0 0 25 0 1 0 1855693923 58155008 13130 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27477/statm): 14198 13130 145 145 0 14053 0 [pid=27477] vsize: 56792 Current children cumulated CPU time (s) 679.3 Current children cumulated vsize (Kb) 58916 [startup+690.053 s] Raw data (loadavg): 1.14 1.00 0.97 2/57 27477 Raw data (/proc/27473/stat): 27473 (minisat+_script) S 27472 27473 5299 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855693918 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27473/statm): 531 226 485 147 0 384 0 [pid=27473] vsize: 2124 Raw data (/proc/27477/stat): 27477 (minisat+_64-bit) R 27473 27473 5299 0 -1 0 13550 0 0 0 68844 85 0 0 25 0 1 0 1855693923 58413056 13194 4294967295 134512640 135094434 3221224432 3221221860 134676608 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27477/statm): 14261 13194 145 145 0 14116 0 [pid=27477] vsize: 57044 Current children cumulated CPU time (s) 689.3 Current children cumulated vsize (Kb) 59168 [startup+700.054 s] Raw data (loadavg): 1.11 1.00 0.97 2/57 27477 Raw data (/proc/27473/stat): 27473 (minisat+_script) S 27472 27473 5299 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855693918 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27473/statm): 531 226 485 147 0 384 0 [pid=27473] vsize: 2124 Raw data (/proc/27477/stat): 27477 (minisat+_64-bit) R 27473 27473 5299 0 -1 0 13566 0 0 0 69844 85 0 0 25 0 1 0 1855693923 58474496 13210 4294967295 134512640 135094434 3221224432 3221223024 134556817 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27477/statm): 14276 13210 145 145 0 14131 0 [pid=27477] vsize: 57104 Current children cumulated CPU time (s) 699.3 Current children cumulated vsize (Kb) 59228 [startup+710.054 s] Raw data (loadavg): 1.10 1.00 0.97 2/57 27477 Raw data (/proc/27473/stat): 27473 (minisat+_script) S 27472 27473 5299 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855693918 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27473/statm): 531 226 485 147 0 384 0 [pid=27473] vsize: 2124 Raw data (/proc/27477/stat): 27477 (minisat+_64-bit) R 27473 27473 5299 0 -1 0 13607 0 0 0 70843 85 0 0 25 0 1 0 1855693923 58642432 13251 4294967295 134512640 135094434 3221224432 3221223088 134557866 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27477/statm): 14317 13251 145 145 0 14172 0 [pid=27477] vsize: 57268 Current children cumulated CPU time (s) 709.29 Current children cumulated vsize (Kb) 59392 [startup+720.055 s] Raw data (loadavg): 1.08 1.00 0.97 2/57 27477 Raw data (/proc/27473/stat): 27473 (minisat+_script) S 27472 27473 5299 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855693918 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27473/statm): 531 226 485 147 0 384 0 [pid=27473] vsize: 2124 Raw data (/proc/27477/stat): 27477 (minisat+_64-bit) R 27473 27473 5299 0 -1 0 13674 0 0 0 71843 86 0 0 25 0 1 0 1855693923 58916864 13318 4294967295 134512640 135094434 3221224432 3221223024 134556964 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27477/statm): 14384 13318 145 145 0 14239 0 [pid=27477] vsize: 57536 Current children cumulated CPU time (s) 719.3 Current children cumulated vsize (Kb) 59660 [startup+730.056 s] Raw data (loadavg): 1.07 1.00 0.97 2/57 27477 Raw data (/proc/27473/stat): 27473 (minisat+_script) S 27472 27473 5299 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855693918 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27473/statm): 531 226 485 147 0 384 0 [pid=27473] vsize: 2124 Raw data (/proc/27477/stat): 27477 (minisat+_64-bit) R 27473 27473 5299 0 -1 0 13757 0 0 0 72842 86 0 0 25 0 1 0 1855693923 59252736 13401 4294967295 134512640 135094434 3221224432 3221223056 134557717 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27477/statm): 14466 13401 145 145 0 14321 0 [pid=27477] vsize: 57864 Current children cumulated CPU time (s) 729.29 Current children cumulated vsize (Kb) 59988 [startup+740.056 s] Raw data (loadavg): 1.06 1.00 0.97 2/57 27477 Raw data (/proc/27473/stat): 27473 (minisat+_script) S 27472 27473 5299 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855693918 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27473/statm): 531 226 485 147 0 384 0 [pid=27473] vsize: 2124 Raw data (/proc/27477/stat): 27477 (minisat+_64-bit) R 27473 27473 5299 0 -1 0 13821 0 0 0 73841 86 0 0 25 0 1 0 1855693923 59510784 13465 4294967295 134512640 135094434 3221224432 3221223088 134558007 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27477/statm): 14529 13465 145 145 0 14384 0 [pid=27477] vsize: 58116 Current children cumulated CPU time (s) 739.28 Current children cumulated vsize (Kb) 60240 [startup+750.057 s] Raw data (loadavg): 1.05 1.00 0.97 2/57 27477 Raw data (/proc/27473/stat): 27473 (minisat+_script) S 27472 27473 5299 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855693918 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27473/statm): 531 226 485 147 0 384 0 [pid=27473] vsize: 2124 Raw data (/proc/27477/stat): 27477 (minisat+_64-bit) R 27473 27473 5299 0 -1 0 13891 0 0 0 74841 86 0 0 25 0 1 0 1855693923 59797504 13535 4294967295 134512640 135094434 3221224432 3221223024 134557180 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27477/statm): 14599 13535 145 145 0 14454 0 [pid=27477] vsize: 58396 Current children cumulated CPU time (s) 749.28 Current children cumulated vsize (Kb) 60520 [startup+760.058 s] Raw data (loadavg): 1.04 1.00 0.97 2/57 27477 Raw data (/proc/27473/stat): 27473 (minisat+_script) S 27472 27473 5299 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855693918 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27473/statm): 531 226 485 147 0 384 0 [pid=27473] vsize: 2124 Raw data (/proc/27477/stat): 27477 (minisat+_64-bit) R 27473 27473 5299 0 -1 0 13971 0 0 0 75839 88 0 0 25 0 1 0 1855693923 60121088 13615 4294967295 134512640 135094434 3221224432 3221223024 134556802 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27477/statm): 14678 13615 145 145 0 14533 0 [pid=27477] vsize: 58712 Current children cumulated CPU time (s) 759.28 Current children cumulated vsize (Kb) 60836 [startup+770.058 s] Raw data (loadavg): 1.03 1.00 0.97 2/57 27477 Raw data (/proc/27473/stat): 27473 (minisat+_script) S 27472 27473 5299 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855693918 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27473/statm): 531 226 485 147 0 384 0 [pid=27473] vsize: 2124 Raw data (/proc/27477/stat): 27477 (minisat+_64-bit) R 27473 27473 5299 0 -1 0 14052 0 0 0 76837 89 0 0 25 0 1 0 1855693923 60444672 13696 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27477/statm): 14757 13696 145 145 0 14612 0 [pid=27477] vsize: 59028 Current children cumulated CPU time (s) 769.27 Current children cumulated vsize (Kb) 61152 [startup+780.059 s] Raw data (loadavg): 1.03 1.00 0.97 2/57 27477 Raw data (/proc/27473/stat): 27473 (minisat+_script) S 27472 27473 5299 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855693918 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27473/statm): 531 226 485 147 0 384 0 [pid=27473] vsize: 2124 Raw data (/proc/27477/stat): 27477 (minisat+_64-bit) R 27473 27473 5299 0 -1 0 14132 0 0 0 77836 89 0 0 25 0 1 0 1855693923 60772352 13776 4294967295 134512640 135094434 3221224432 3221223056 134557598 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27477/statm): 14837 13776 145 145 0 14692 0 [pid=27477] vsize: 59348 Current children cumulated CPU time (s) 779.26 Current children cumulated vsize (Kb) 61472 [startup+790.06 s] Raw data (loadavg): 1.02 1.00 0.97 2/57 27477 Raw data (/proc/27473/stat): 27473 (minisat+_script) S 27472 27473 5299 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855693918 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27473/statm): 531 226 485 147 0 384 0 [pid=27473] vsize: 2124 Raw data (/proc/27477/stat): 27477 (minisat+_64-bit) R 27473 27473 5299 0 -1 0 14224 0 0 0 78835 90 0 0 25 0 1 0 1855693923 61145088 13868 4294967295 134512640 135094434 3221224432 3221223088 134558159 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27477/statm): 14928 13868 145 145 0 14783 0 [pid=27477] vsize: 59712 Current children cumulated CPU time (s) 789.26 Current children cumulated vsize (Kb) 61836 [startup+800.061 s] Raw data (loadavg): 1.02 1.00 0.97 2/57 27477 Raw data (/proc/27473/stat): 27473 (minisat+_script) S 27472 27473 5299 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855693918 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27473/statm): 531 226 485 147 0 384 0 [pid=27473] vsize: 2124 Raw data (/proc/27477/stat): 27477 (minisat+_64-bit) R 27473 27473 5299 0 -1 0 14286 0 0 0 79834 90 0 0 25 0 1 0 1855693923 61399040 13930 4294967295 134512640 135094434 3221224432 3221223056 134562057 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27477/statm): 14990 13930 145 145 0 14845 0 [pid=27477] vsize: 59960 Current children cumulated CPU time (s) 799.25 Current children cumulated vsize (Kb) 62084 [startup+810.062 s] Raw data (loadavg): 1.02 1.00 0.97 2/57 27477 Raw data (/proc/27473/stat): 27473 (minisat+_script) S 27472 27473 5299 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855693918 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27473/statm): 531 226 485 147 0 384 0 [pid=27473] vsize: 2124 Raw data (/proc/27477/stat): 27477 (minisat+_64-bit) R 27473 27473 5299 0 -1 0 14457 0 0 0 80832 91 0 0 25 0 1 0 1855693923 62095360 14101 4294967295 134512640 135094434 3221224432 3221223044 134563049 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27477/statm): 15160 14101 145 145 0 15015 0 [pid=27477] vsize: 60640 Current children cumulated CPU time (s) 809.24 Current children cumulated vsize (Kb) 62764 [startup+820.062 s] Raw data (loadavg): 1.01 1.00 0.97 2/57 27477 Raw data (/proc/27473/stat): 27473 (minisat+_script) S 27472 27473 5299 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855693918 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27473/statm): 531 226 485 147 0 384 0 [pid=27473] vsize: 2124 Raw data (/proc/27477/stat): 27477 (minisat+_64-bit) R 27473 27473 5299 0 -1 0 14584 0 0 0 81829 92 0 0 25 0 1 0 1855693923 62611456 14228 4294967295 134512640 135094434 3221224432 3221223104 134555574 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27477/statm): 15286 14228 145 145 0 15141 0 [pid=27477] vsize: 61144 Current children cumulated CPU time (s) 819.22 Current children cumulated vsize (Kb) 63268 [startup+830.063 s] Raw data (loadavg): 1.01 1.00 0.97 2/57 27477 Raw data (/proc/27473/stat): 27473 (minisat+_script) S 27472 27473 5299 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855693918 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27473/statm): 531 226 485 147 0 384 0 [pid=27473] vsize: 2124 Raw data (/proc/27477/stat): 27477 (minisat+_64-bit) R 27473 27473 5299 0 -1 0 14655 0 0 0 82829 93 0 0 25 0 1 0 1855693923 62902272 14299 4294967295 134512640 135094434 3221224432 3221223024 134557423 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27477/statm): 15357 14299 145 145 0 15212 0 [pid=27477] vsize: 61428 Current children cumulated CPU time (s) 829.23 Current children cumulated vsize (Kb) 63552 [startup+840.064 s] Raw data (loadavg): 1.01 1.00 0.97 2/57 27477 Raw data (/proc/27473/stat): 27473 (minisat+_script) S 27472 27473 5299 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855693918 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27473/statm): 531 226 485 147 0 384 0 [pid=27473] vsize: 2124 Raw data (/proc/27477/stat): 27477 (minisat+_64-bit) R 27473 27473 5299 0 -1 0 14787 0 0 0 83827 94 0 0 25 0 1 0 1855693923 63447040 14431 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27477/statm): 15490 14431 145 145 0 15345 0 [pid=27477] vsize: 61960 Current children cumulated CPU time (s) 839.22 Current children cumulated vsize (Kb) 64084 [startup+850.065 s] Raw data (loadavg): 1.01 1.00 0.97 2/57 27477 Raw data (/proc/27473/stat): 27473 (minisat+_script) S 27472 27473 5299 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855693918 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27473/statm): 531 226 485 147 0 384 0 [pid=27473] vsize: 2124 Raw data (/proc/27477/stat): 27477 (minisat+_64-bit) R 27473 27473 5299 0 -1 0 14883 0 0 0 84826 94 0 0 25 0 1 0 1855693923 63848448 14527 4294967295 134512640 135094434 3221224432 3221223056 134557596 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27477/statm): 15588 14527 145 145 0 15443 0 [pid=27477] vsize: 62352 Current children cumulated CPU time (s) 849.21 Current children cumulated vsize (Kb) 64476 [startup+860.066 s] Raw data (loadavg): 1.00 1.00 0.97 2/57 27477 Raw data (/proc/27473/stat): 27473 (minisat+_script) S 27472 27473 5299 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855693918 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27473/statm): 531 226 485 147 0 384 0 [pid=27473] vsize: 2124 Raw data (/proc/27477/stat): 27477 (minisat+_64-bit) R 27473 27473 5299 0 -1 0 15081 0 0 0 85823 95 0 0 25 0 1 0 1855693923 64651264 14725 4294967295 134512640 135094434 3221224432 3221221104 134677307 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27477/statm): 15784 14725 145 145 0 15639 0 [pid=27477] vsize: 63136 Current children cumulated CPU time (s) 859.19 Current children cumulated vsize (Kb) 65260 [startup+870.066 s] Raw data (loadavg): 1.00 1.00 0.97 2/57 27477 Raw data (/proc/27473/stat): 27473 (minisat+_script) S 27472 27473 5299 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855693918 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27473/statm): 531 226 485 147 0 384 0 [pid=27473] vsize: 2124 Raw data (/proc/27477/stat): 27477 (minisat+_64-bit) R 27473 27473 5299 0 -1 0 15098 0 0 0 86823 95 0 0 25 0 1 0 1855693923 64716800 14742 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27477/statm): 15800 14742 145 145 0 15655 0 [pid=27477] vsize: 63200 Current children cumulated CPU time (s) 869.19 Current children cumulated vsize (Kb) 65324 [startup+880.066 s] Raw data (loadavg): 1.00 1.00 0.97 2/57 27477 Raw data (/proc/27473/stat): 27473 (minisat+_script) S 27472 27473 5299 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855693918 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27473/statm): 531 226 485 147 0 384 0 [pid=27473] vsize: 2124 Raw data (/proc/27477/stat): 27477 (minisat+_64-bit) R 27473 27473 5299 0 -1 0 15175 0 0 0 87822 96 0 0 25 0 1 0 1855693923 65048576 14819 4294967295 134512640 135094434 3221224432 3221223120 134554746 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27477/statm): 15881 14819 145 145 0 15736 0 [pid=27477] vsize: 63524 Current children cumulated CPU time (s) 879.19 Current children cumulated vsize (Kb) 65648 [startup+890.067 s] Raw data (loadavg): 1.00 1.00 0.97 2/57 27477 Raw data (/proc/27473/stat): 27473 (minisat+_script) S 27472 27473 5299 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855693918 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27473/statm): 531 226 485 147 0 384 0 [pid=27473] vsize: 2124 Raw data (/proc/27477/stat): 27477 (minisat+_64-bit) R 27473 27473 5299 0 -1 0 15237 0 0 0 88821 96 0 0 25 0 1 0 1855693923 65294336 14881 4294967295 134512640 135094434 3221224432 3221223084 134675707 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27477/statm): 15941 14881 145 145 0 15796 0 [pid=27477] vsize: 63764 Current children cumulated CPU time (s) 889.18 Current children cumulated vsize (Kb) 65888 [startup+900.069 s] Raw data (loadavg): 1.00 1.00 0.97 2/57 27477 Raw data (/proc/27473/stat): 27473 (minisat+_script) S 27472 27473 5299 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855693918 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27473/statm): 531 226 485 147 0 384 0 [pid=27473] vsize: 2124 Raw data (/proc/27477/stat): 27477 (minisat+_64-bit) R 27473 27473 5299 0 -1 0 15305 0 0 0 89821 97 0 0 25 0 1 0 1855693923 65572864 14949 4294967295 134512640 135094434 3221224432 3221223024 134557175 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27477/statm): 16009 14949 145 145 0 15864 0 [pid=27477] vsize: 64036 Current children cumulated CPU time (s) 899.19 Current children cumulated vsize (Kb) 66160 [startup+910.069 s] Raw data (loadavg): 1.00 1.00 0.97 2/57 27477 Raw data (/proc/27473/stat): 27473 (minisat+_script) S 27472 27473 5299 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855693918 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27473/statm): 531 226 485 147 0 384 0 [pid=27473] vsize: 2124 Raw data (/proc/27477/stat): 27477 (minisat+_64-bit) R 27473 27473 5299 0 -1 0 15345 0 0 0 90820 97 0 0 25 0 1 0 1855693923 65732608 14989 4294967295 134512640 135094434 3221224432 3221223088 134557893 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27477/statm): 16048 14989 145 145 0 15903 0 [pid=27477] vsize: 64192 Current children cumulated CPU time (s) 909.18 Current children cumulated vsize (Kb) 66316 [startup+920.07 s] Raw data (loadavg): 1.00 1.00 0.97 2/57 27477 Raw data (/proc/27473/stat): 27473 (minisat+_script) S 27472 27473 5299 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855693918 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27473/statm): 531 226 485 147 0 384 0 [pid=27473] vsize: 2124 Raw data (/proc/27477/stat): 27477 (minisat+_64-bit) R 27473 27473 5299 0 -1 0 15411 0 0 0 91819 98 0 0 25 0 1 0 1855693923 66007040 15055 4294967295 134512640 135094434 3221224432 3221223088 134558249 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27477/statm): 16115 15055 145 145 0 15970 0 [pid=27477] vsize: 64460 Current children cumulated CPU time (s) 919.18 Current children cumulated vsize (Kb) 66584 [startup+930.071 s] Raw data (loadavg): 1.00 1.00 0.97 2/57 27477 Raw data (/proc/27473/stat): 27473 (minisat+_script) S 27472 27473 5299 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855693918 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27473/statm): 531 226 485 147 0 384 0 [pid=27473] vsize: 2124 Raw data (/proc/27477/stat): 27477 (minisat+_64-bit) R 27473 27473 5299 0 -1 0 15461 0 0 0 92819 99 0 0 25 0 1 0 1855693923 66215936 15105 4294967295 134512640 135094434 3221224432 3221223088 134558249 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27477/statm): 16166 15105 145 145 0 16021 0 [pid=27477] vsize: 64664 Current children cumulated CPU time (s) 929.19 Current children cumulated vsize (Kb) 66788 [startup+940.071 s] Raw data (loadavg): 1.00 1.00 0.97 2/57 27477 Raw data (/proc/27473/stat): 27473 (minisat+_script) S 27472 27473 5299 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855693918 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27473/statm): 531 226 485 147 0 384 0 [pid=27473] vsize: 2124 Raw data (/proc/27477/stat): 27477 (minisat+_64-bit) R 27473 27473 5299 0 -1 0 15543 0 0 0 93817 99 0 0 25 0 1 0 1855693923 66547712 15187 4294967295 134512640 135094434 3221224432 3221223104 134556327 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27477/statm): 16247 15187 145 145 0 16102 0 [pid=27477] vsize: 64988 Current children cumulated CPU time (s) 939.17 Current children cumulated vsize (Kb) 67112 [startup+950.073 s] Raw data (loadavg): 1.00 1.00 0.97 2/57 27477 Raw data (/proc/27473/stat): 27473 (minisat+_script) S 27472 27473 5299 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855693918 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27473/statm): 531 226 485 147 0 384 0 [pid=27473] vsize: 2124 Raw data (/proc/27477/stat): 27477 (minisat+_64-bit) R 27473 27473 5299 0 -1 0 15618 0 0 0 94814 101 0 0 25 0 1 0 1855693923 66846720 15262 4294967295 134512640 135094434 3221224432 3221223120 134554793 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27477/statm): 16320 15262 145 145 0 16175 0 [pid=27477] vsize: 65280 Current children cumulated CPU time (s) 949.16 Current children cumulated vsize (Kb) 67404 [startup+960.073 s] Raw data (loadavg): 1.00 1.00 0.97 2/57 27477 Raw data (/proc/27473/stat): 27473 (minisat+_script) S 27472 27473 5299 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855693918 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27473/statm): 531 226 485 147 0 384 0 [pid=27473] vsize: 2124 Raw data (/proc/27477/stat): 27477 (minisat+_64-bit) R 27473 27473 5299 0 -1 0 15699 0 0 0 95813 103 0 0 25 0 1 0 1855693923 67178496 15343 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27477/statm): 16401 15343 145 145 0 16256 0 [pid=27477] vsize: 65604 Current children cumulated CPU time (s) 959.17 Current children cumulated vsize (Kb) 67728 [startup+970.074 s] Raw data (loadavg): 1.00 1.00 0.97 2/57 27477 Raw data (/proc/27473/stat): 27473 (minisat+_script) S 27472 27473 5299 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855693918 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27473/statm): 531 226 485 147 0 384 0 [pid=27473] vsize: 2124 Raw data (/proc/27477/stat): 27477 (minisat+_64-bit) R 27473 27473 5299 0 -1 0 15731 0 0 0 96812 103 0 0 25 0 1 0 1855693923 67309568 15375 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27477/statm): 16433 15375 145 145 0 16288 0 [pid=27477] vsize: 65732 Current children cumulated CPU time (s) 969.16 Current children cumulated vsize (Kb) 67856 [startup+980.075 s] Raw data (loadavg): 1.08 1.02 0.97 3/57 27477 Raw data (/proc/27473/stat): 27473 (minisat+_script) S 27472 27473 5299 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855693918 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27473/statm): 531 226 485 147 0 384 0 [pid=27473] vsize: 2124 Raw data (/proc/27477/stat): 27477 (minisat+_64-bit) R 27473 27473 5299 0 -1 0 15731 0 0 0 97812 103 0 0 25 0 1 0 1855693923 67309568 15375 4294967295 134512640 135094434 3221224432 3221223076 134558261 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27477/statm): 16433 15375 145 145 0 16288 0 [pid=27477] vsize: 65732 Current children cumulated CPU time (s) 979.16 Current children cumulated vsize (Kb) 67856 [startup+990.075 s] Raw data (loadavg): 1.14 1.03 0.98 2/57 27477 Raw data (/proc/27473/stat): 27473 (minisat+_script) S 27472 27473 5299 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855693918 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27473/statm): 531 226 485 147 0 384 0 [pid=27473] vsize: 2124 Raw data (/proc/27477/stat): 27477 (minisat+_64-bit) R 27473 27473 5299 0 -1 0 15731 0 0 0 98812 104 0 0 25 0 1 0 1855693923 67309568 15375 4294967295 134512640 135094434 3221224432 3221221904 134677007 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27477/statm): 16433 15375 145 145 0 16288 0 [pid=27477] vsize: 65732 Current children cumulated CPU time (s) 989.17 Current children cumulated vsize (Kb) 67856 [startup+1000.08 s] Raw data (loadavg): 1.12 1.03 0.98 2/57 27477 Raw data (/proc/27473/stat): 27473 (minisat+_script) S 27472 27473 5299 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855693918 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27473/statm): 531 226 485 147 0 384 0 [pid=27473] vsize: 2124 Raw data (/proc/27477/stat): 27477 (minisat+_64-bit) R 27473 27473 5299 0 -1 0 15732 0 0 0 99812 104 0 0 25 0 1 0 1855693923 67309568 15376 4294967295 134512640 135094434 3221224432 3221223120 134554746 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27477/statm): 16433 15376 145 145 0 16288 0 [pid=27477] vsize: 65732 Current children cumulated CPU time (s) 999.17 Current children cumulated vsize (Kb) 67856 [startup+1010.08 s] Raw data (loadavg): 1.10 1.03 0.98 2/57 27477 Raw data (/proc/27473/stat): 27473 (minisat+_script) S 27472 27473 5299 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855693918 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27473/statm): 531 226 485 147 0 384 0 [pid=27473] vsize: 2124 Raw data (/proc/27477/stat): 27477 (minisat+_64-bit) R 27473 27473 5299 0 -1 0 15732 0 0 0 100812 104 0 0 25 0 1 0 1855693923 67309568 15376 4294967295 134512640 135094434 3221224432 3221223024 134557328 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27477/statm): 16433 15376 145 145 0 16288 0 [pid=27477] vsize: 65732 Current children cumulated CPU time (s) 1009.17 Current children cumulated vsize (Kb) 67856 [startup+1020.08 s] Raw data (loadavg): 1.08 1.03 0.98 2/57 27477 Raw data (/proc/27473/stat): 27473 (minisat+_script) S 27472 27473 5299 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855693918 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27473/statm): 531 226 485 147 0 384 0 [pid=27473] vsize: 2124 Raw data (/proc/27477/stat): 27477 (minisat+_64-bit) R 27473 27473 5299 0 -1 0 15732 0 0 0 101812 104 0 0 25 0 1 0 1855693923 67309568 15376 4294967295 134512640 135094434 3221224432 3221223120 134554746 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27477/statm): 16433 15376 145 145 0 16288 0 [pid=27477] vsize: 65732 Current children cumulated CPU time (s) 1019.17 Current children cumulated vsize (Kb) 67856 [startup+1030.08 s] Raw data (loadavg): 1.07 1.03 0.98 2/57 27477 Raw data (/proc/27473/stat): 27473 (minisat+_script) S 27472 27473 5299 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855693918 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27473/statm): 531 226 485 147 0 384 0 [pid=27473] vsize: 2124 Raw data (/proc/27477/stat): 27477 (minisat+_64-bit) R 27473 27473 5299 0 -1 0 15732 0 0 0 102812 105 0 0 25 0 1 0 1855693923 67309568 15376 4294967295 134512640 135094434 3221224432 3221223088 134557882 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27477/statm): 16433 15376 145 145 0 16288 0 [pid=27477] vsize: 65732 Current children cumulated CPU time (s) 1029.18 Current children cumulated vsize (Kb) 67856 [startup+1040.08 s] Raw data (loadavg): 1.06 1.03 0.98 2/57 27477 Raw data (/proc/27473/stat): 27473 (minisat+_script) S 27472 27473 5299 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855693918 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27473/statm): 531 226 485 147 0 384 0 [pid=27473] vsize: 2124 Raw data (/proc/27477/stat): 27477 (minisat+_64-bit) R 27473 27473 5299 0 -1 0 15732 0 0 0 103812 105 0 0 25 0 1 0 1855693923 67309568 15376 4294967295 134512640 135094434 3221224432 3221223104 134556317 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27477/statm): 16433 15376 145 145 0 16288 0 [pid=27477] vsize: 65732 Current children cumulated CPU time (s) 1039.18 Current children cumulated vsize (Kb) 67856 [startup+1050.08 s] Raw data (loadavg): 1.05 1.02 0.98 2/57 27477 Raw data (/proc/27473/stat): 27473 (minisat+_script) S 27472 27473 5299 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855693918 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27473/statm): 531 226 485 147 0 384 0 [pid=27473] vsize: 2124 Raw data (/proc/27477/stat): 27477 (minisat+_64-bit) R 27473 27473 5299 0 -1 0 15732 0 0 0 104812 105 0 0 25 0 1 0 1855693923 67309568 15376 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27477/statm): 16433 15376 145 145 0 16288 0 [pid=27477] vsize: 65732 Current children cumulated CPU time (s) 1049.18 Current children cumulated vsize (Kb) 67856 [startup+1060.08 s] Raw data (loadavg): 1.04 1.02 0.98 2/57 27477 Raw data (/proc/27473/stat): 27473 (minisat+_script) S 27472 27473 5299 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855693918 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27473/statm): 531 226 485 147 0 384 0 [pid=27473] vsize: 2124 Raw data (/proc/27477/stat): 27477 (minisat+_64-bit) R 27473 27473 5299 0 -1 0 15732 0 0 0 105812 105 0 0 25 0 1 0 1855693923 67309568 15376 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27477/statm): 16433 15376 145 145 0 16288 0 [pid=27477] vsize: 65732 Current children cumulated CPU time (s) 1059.18 Current children cumulated vsize (Kb) 67856 [startup+1070.08 s] Raw data (loadavg): 1.04 1.02 0.98 2/57 27477 Raw data (/proc/27473/stat): 27473 (minisat+_script) S 27472 27473 5299 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855693918 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27473/statm): 531 226 485 147 0 384 0 [pid=27473] vsize: 2124 Raw data (/proc/27477/stat): 27477 (minisat+_64-bit) R 27473 27473 5299 0 -1 0 15732 0 0 0 106812 105 0 0 25 0 1 0 1855693923 67309568 15376 4294967295 134512640 135094434 3221224432 3221223024 134557037 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27477/statm): 16433 15376 145 145 0 16288 0 [pid=27477] vsize: 65732 Current children cumulated CPU time (s) 1069.18 Current children cumulated vsize (Kb) 67856 [startup+1080.08 s] Raw data (loadavg): 1.03 1.02 0.98 2/57 27477 Raw data (/proc/27473/stat): 27473 (minisat+_script) S 27472 27473 5299 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855693918 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27473/statm): 531 226 485 147 0 384 0 [pid=27473] vsize: 2124 Raw data (/proc/27477/stat): 27477 (minisat+_64-bit) R 27473 27473 5299 0 -1 0 15732 0 0 0 107813 105 0 0 25 0 1 0 1855693923 67309568 15376 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27477/statm): 16433 15376 145 145 0 16288 0 [pid=27477] vsize: 65732 Current children cumulated CPU time (s) 1079.19 Current children cumulated vsize (Kb) 67856 [startup+1090.08 s] Raw data (loadavg): 1.02 1.02 0.98 2/57 27477 Raw data (/proc/27473/stat): 27473 (minisat+_script) S 27472 27473 5299 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855693918 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27473/statm): 531 226 485 147 0 384 0 [pid=27473] vsize: 2124 Raw data (/proc/27477/stat): 27477 (minisat+_64-bit) R 27473 27473 5299 0 -1 0 15732 0 0 0 108812 106 0 0 25 0 1 0 1855693923 67309568 15376 4294967295 134512640 135094434 3221224432 3221223056 134557737 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27477/statm): 16433 15376 145 145 0 16288 0 [pid=27477] vsize: 65732 Current children cumulated CPU time (s) 1089.19 Current children cumulated vsize (Kb) 67856 [startup+1100.08 s] Raw data (loadavg): 1.02 1.02 0.98 2/57 27477 Raw data (/proc/27473/stat): 27473 (minisat+_script) S 27472 27473 5299 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855693918 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27473/statm): 531 226 485 147 0 384 0 [pid=27473] vsize: 2124 Raw data (/proc/27477/stat): 27477 (minisat+_64-bit) R 27473 27473 5299 0 -1 0 15732 0 0 0 109813 106 0 0 25 0 1 0 1855693923 67309568 15376 4294967295 134512640 135094434 3221224432 3221221688 134676461 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27477/statm): 16433 15376 145 145 0 16288 0 [pid=27477] vsize: 65732 Current children cumulated CPU time (s) 1099.2 Current children cumulated vsize (Kb) 67856 [startup+1110.08 s] Raw data (loadavg): 1.02 1.02 0.98 2/57 27477 Raw data (/proc/27473/stat): 27473 (minisat+_script) S 27472 27473 5299 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855693918 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27473/statm): 531 226 485 147 0 384 0 [pid=27473] vsize: 2124 Raw data (/proc/27477/stat): 27477 (minisat+_64-bit) R 27473 27473 5299 0 -1 0 15732 0 0 0 110813 106 0 0 25 0 1 0 1855693923 67309568 15376 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27477/statm): 16433 15376 145 145 0 16288 0 [pid=27477] vsize: 65732 Current children cumulated CPU time (s) 1109.2 Current children cumulated vsize (Kb) 67856 [startup+1120.08 s] Raw data (loadavg): 1.01 1.02 0.98 2/57 27477 Raw data (/proc/27473/stat): 27473 (minisat+_script) S 27472 27473 5299 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855693918 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27473/statm): 531 226 485 147 0 384 0 [pid=27473] vsize: 2124 Raw data (/proc/27477/stat): 27477 (minisat+_64-bit) R 27473 27473 5299 0 -1 0 15734 0 0 0 111813 106 0 0 25 0 1 0 1855693923 67309568 15378 4294967295 134512640 135094434 3221224432 3221223024 134556851 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27477/statm): 16433 15378 145 145 0 16288 0 [pid=27477] vsize: 65732 Current children cumulated CPU time (s) 1119.2 Current children cumulated vsize (Kb) 67856 [startup+1130.08 s] Raw data (loadavg): 1.01 1.02 0.98 2/57 27477 Raw data (/proc/27473/stat): 27473 (minisat+_script) S 27472 27473 5299 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855693918 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27473/statm): 531 226 485 147 0 384 0 [pid=27473] vsize: 2124 Raw data (/proc/27477/stat): 27477 (minisat+_64-bit) R 27473 27473 5299 0 -1 0 15734 0 0 0 112812 106 0 0 25 0 1 0 1855693923 67309568 15378 4294967295 134512640 135094434 3221224432 3221223104 134556073 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27477/statm): 16433 15378 145 145 0 16288 0 [pid=27477] vsize: 65732 Current children cumulated CPU time (s) 1129.19 Current children cumulated vsize (Kb) 67856 [startup+1140.08 s] Raw data (loadavg): 1.01 1.02 0.98 2/57 27477 Raw data (/proc/27473/stat): 27473 (minisat+_script) S 27472 27473 5299 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855693918 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27473/statm): 531 226 485 147 0 384 0 [pid=27473] vsize: 2124 Raw data (/proc/27477/stat): 27477 (minisat+_64-bit) R 27473 27473 5299 0 -1 0 15734 0 0 0 113813 106 0 0 25 0 1 0 1855693923 67309568 15378 4294967295 134512640 135094434 3221224432 3221223088 134558249 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27477/statm): 16433 15378 145 145 0 16288 0 [pid=27477] vsize: 65732 Current children cumulated CPU time (s) 1139.2 Current children cumulated vsize (Kb) 67856 [startup+1150.08 s] Raw data (loadavg): 1.01 1.01 0.98 2/57 27477 Raw data (/proc/27473/stat): 27473 (minisat+_script) S 27472 27473 5299 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855693918 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27473/statm): 531 226 485 147 0 384 0 [pid=27473] vsize: 2124 Raw data (/proc/27477/stat): 27477 (minisat+_64-bit) R 27473 27473 5299 0 -1 0 15734 0 0 0 114813 106 0 0 25 0 1 0 1855693923 67309568 15378 4294967295 134512640 135094434 3221224432 3221223088 134557914 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27477/statm): 16433 15378 145 145 0 16288 0 [pid=27477] vsize: 65732 Current children cumulated CPU time (s) 1149.2 Current children cumulated vsize (Kb) 67856 [startup+1160.08 s] Raw data (loadavg): 1.01 1.01 0.98 2/57 27477 Raw data (/proc/27473/stat): 27473 (minisat+_script) S 27472 27473 5299 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855693918 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27473/statm): 531 226 485 147 0 384 0 [pid=27473] vsize: 2124 Raw data (/proc/27477/stat): 27477 (minisat+_64-bit) R 27473 27473 5299 0 -1 0 15734 0 0 0 115813 106 0 0 25 0 1 0 1855693923 67309568 15378 4294967295 134512640 135094434 3221224432 3221221708 134677081 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27477/statm): 16433 15378 145 145 0 16288 0 [pid=27477] vsize: 65732 Current children cumulated CPU time (s) 1159.2 Current children cumulated vsize (Kb) 67856 [startup+1170.08 s] Raw data (loadavg): 1.00 1.01 0.98 2/57 27477 Raw data (/proc/27473/stat): 27473 (minisat+_script) S 27472 27473 5299 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855693918 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27473/statm): 531 226 485 147 0 384 0 [pid=27473] vsize: 2124 Raw data (/proc/27477/stat): 27477 (minisat+_64-bit) R 27473 27473 5299 0 -1 0 15734 0 0 0 116813 107 0 0 25 0 1 0 1855693923 67309568 15378 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27477/statm): 16433 15378 145 145 0 16288 0 [pid=27477] vsize: 65732 Current children cumulated CPU time (s) 1169.21 Current children cumulated vsize (Kb) 67856 [startup+1180.08 s] Raw data (loadavg): 1.00 1.01 0.98 2/57 27477 Raw data (/proc/27473/stat): 27473 (minisat+_script) S 27472 27473 5299 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855693918 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27473/statm): 531 226 485 147 0 384 0 [pid=27473] vsize: 2124 Raw data (/proc/27477/stat): 27477 (minisat+_64-bit) R 27473 27473 5299 0 -1 0 15734 0 0 0 117813 107 0 0 25 0 1 0 1855693923 67309568 15378 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27477/statm): 16433 15378 145 145 0 16288 0 [pid=27477] vsize: 65732 Current children cumulated CPU time (s) 1179.21 Current children cumulated vsize (Kb) 67856 [startup+1190.08 s] Raw data (loadavg): 1.00 1.01 0.98 2/57 27477 Raw data (/proc/27473/stat): 27473 (minisat+_script) S 27472 27473 5299 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855693918 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27473/statm): 531 226 485 147 0 384 0 [pid=27473] vsize: 2124 Raw data (/proc/27477/stat): 27477 (minisat+_64-bit) R 27473 27473 5299 0 -1 0 15734 0 0 0 118813 107 0 0 25 0 1 0 1855693923 67309568 15378 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27477/statm): 16433 15378 145 145 0 16288 0 [pid=27477] vsize: 65732 Current children cumulated CPU time (s) 1189.21 Current children cumulated vsize (Kb) 67856 [startup+1200.08 s] Raw data (loadavg): 1.00 1.01 0.98 2/57 27477 Raw data (/proc/27473/stat): 27473 (minisat+_script) S 27472 27473 5299 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855693918 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27473/statm): 531 226 485 147 0 384 0 [pid=27473] vsize: 2124 Raw data (/proc/27477/stat): 27477 (minisat+_64-bit) R 27473 27473 5299 0 -1 0 15735 0 0 0 119813 107 0 0 25 0 1 0 1855693923 67309568 15379 4294967295 134512640 135094434 3221224432 3221223088 134557900 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27477/statm): 16433 15379 145 145 0 16288 0 [pid=27477] vsize: 65732 Current children cumulated CPU time (s) 1199.21 Current children cumulated vsize (Kb) 67856 [startup+1210.09 s] Raw data (loadavg): 1.00 1.01 0.98 2/57 27477 Raw data (/proc/27473/stat): 27473 (minisat+_script) S 27472 27473 5299 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855693918 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27473/statm): 531 226 485 147 0 384 0 [pid=27473] vsize: 2124 Raw data (/proc/27477/stat): 27477 (minisat+_64-bit) R 27473 27473 5299 0 -1 0 15735 0 0 0 120814 107 0 0 25 0 1 0 1855693923 67309568 15379 4294967295 134512640 135094434 3221224432 3221223088 134558159 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27477/statm): 16433 15379 145 145 0 16288 0 [pid=27477] vsize: 65732 Current children cumulated CPU time (s) 1209.22 Current children cumulated vsize (Kb) 67856 Maximum CPU time exceeded: sending SIGTERM then SIGKILL [startup+1210.09 s] Raw data (loadavg): 1.00 1.01 0.98 2/57 27477 Raw data (/proc/27473/stat): 27473 (minisat+_script) S 27472 27473 5299 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855693918 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27473/statm): 531 226 485 147 0 384 0 [pid=27473] vsize: 2124 Raw data (/proc/27477/stat): 27477 (minisat+_64-bit) R 27473 27473 5299 0 -1 0 15735 0 0 0 120814 107 0 0 25 0 1 0 1855693923 67309568 15379 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27477/statm): 16433 15379 145 145 0 16288 0 [pid=27477] vsize: 65732 Current children cumulated CPU time (s) 1209.22 Current children cumulated vsize (Kb) 67856 Sending SIGTERM to -27473 Sleeping 2 seconds One traced child (pid=27473) ended because it received signal 15 (SIGTERM) One traced child (pid=27477) exited with status: 10 All traced children have exited ! Game is over. Child status: 10 Real time (s): 1210.12 CPU time (s): 1209.25 CPU user time (s): 1208.14 CPU system time (s): 1.10583 CPU usage (%): 99.928 Max. virtual memory (cumulated for all children) (Kb): 67856
ERROR: no interpretation found !