Name | mps-v2-13-7/MIPLIB/miplib/normalized-mps-v2-13-7-p0282.opb |
MD5SUM | a733e9fa1e4e3ac90baf85249f7c3e9a |
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.5803 |
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 wulflinc20 THE 2005-09-20 03:18:33 (client local time) PB2005-SCRIPT v4.0 MARKUPS: idlaunch=3259 boxname=wulflinc20 idbench=915 idsolver=3 numberseed=0 MD5SUM SOLVER: MD5SUM BENCH: a733e9fa1e4e3ac90baf85249f7c3e9a /oldhome/oroussel/tmp/wulflinc20/normalized-mps-v2-13-7-p0282.opb REAL COMMAND: minisat+_script /oldhome/oroussel/tmp/wulflinc20/normalized-mps-v2-13-7-p0282.opb IDLAUNCH: 3259 /proc/cpuinfo: processor : 0 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 3 cpu MHz : 451.215 cache size : 512 KB fdiv_bug : no hlt_bug : no f00f_bug : no coma_bug : no fpu : yes fpu_exception : yes cpuid level : 2 wp : yes flags : fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse bogomips : 888.83 processor : 1 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 3 cpu MHz : 451.215 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 : 901.12 /proc/meminfo: MemTotal: 1034660 kB MemFree: 922128 kB Buffers: 5164 kB Cached: 78336 kB SwapCached: 820 kB Active: 18908 kB Inactive: 67208 kB HighTotal: 131008 kB HighFree: 48496 kB LowTotal: 903652 kB LowFree: 873632 kB SwapTotal: 2097892 kB SwapFree: 2096508 kB Dirty: 28 kB Writeback: 0 kB Mapped: 5640 kB Slab: 20600 kB Committed_AS: 64168 kB PageTables: 328 kB VmallocTotal: 114680 kB VmallocUsed: 1368 kB VmallocChunk: 113252 kB JOB ENDED THE 2005-09-20 03:38:44 (client local time) WITH STATUS 10 IN 1209.27 SECONDS stats: 3259 7 1209.27 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 % | c | 119463 | 286211 671329 | 153647 48850 2652967 54.3 | 1.612 % | c | 120223 | 286211 671329 | 169012 49610 2714939 54.7 | 1.612 % | c | 121362 | 286211 671329 | 185913 50749 2870613 56.6 | 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/28417/stat): 28417 (minisat+_script) R 28416 28417 2660 0 -1 0 19 0 0 0 0 0 0 0 23 0 1 0 1855238664 712704 3 4294967295 134512640 135087896 3221224512 3221224512 1073744960 0 0 5 0 0 0 0 17 0 0 0 Raw data (/proc/28417/statm): 174 3 169 147 0 27 0 [pid=28417] 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=28418 New process pid=28419 New process pid=28420 One traced child (pid=28419) exited with status: 0 execve syscall for /bin/sed executable 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=28420) exited with status: 0 One traced child (pid=28418) exited with status: 0 New process pid=28421 execve syscall for /oldhome/oroussel/solvers/minisat+_64-bit_static executable open syscall for file /dev/null open syscall for file /oldhome/oroussel/tmp/wulflinc20/normalized-mps-v2-13-7-p0282.opb [startup+10.0033 s] Raw data (loadavg): 0.93 0.95 0.90 2/57 28421 Raw data (/proc/28417/stat): 28417 (minisat+_script) S 28416 28417 2660 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855238664 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/28417/statm): 531 226 485 147 0 384 0 [pid=28417] vsize: 2124 Raw data (/proc/28421/stat): 28421 (minisat+_64-bit) R 28417 28417 2660 0 -1 0 8650 0 0 0 927 33 0 0 25 0 1 0 1855238669 38129664 8294 4294967295 134512640 135094434 3221224432 3221221892 134677077 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/28421/statm): 9309 8294 145 145 0 9164 0 [pid=28421] vsize: 37236 Current children cumulated CPU time (s) 9.6 Current children cumulated vsize (Kb) 39360 [startup+20.005 s] Raw data (loadavg): 0.94 0.96 0.91 2/57 28421 Raw data (/proc/28417/stat): 28417 (minisat+_script) S 28416 28417 2660 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855238664 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/28417/statm): 531 226 485 147 0 384 0 [pid=28417] vsize: 2124 Raw data (/proc/28421/stat): 28421 (minisat+_64-bit) R 28417 28417 2660 0 -1 0 8720 0 0 0 1926 33 0 0 25 0 1 0 1855238669 38387712 8364 4294967295 134512640 135094434 3221224432 3221223056 134557717 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/28421/statm): 9372 8364 145 145 0 9227 0 [pid=28421] vsize: 37488 Current children cumulated CPU time (s) 19.59 Current children cumulated vsize (Kb) 39612 [startup+30.0058 s] Raw data (loadavg): 0.95 0.96 0.91 2/57 28421 Raw data (/proc/28417/stat): 28417 (minisat+_script) S 28416 28417 2660 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855238664 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/28417/statm): 531 226 485 147 0 384 0 [pid=28417] vsize: 2124 Raw data (/proc/28421/stat): 28421 (minisat+_64-bit) R 28417 28417 2660 0 -1 0 8795 0 0 0 2926 34 0 0 25 0 1 0 1855238669 38682624 8439 4294967295 134512640 135094434 3221224432 3221223056 134557565 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/28421/statm): 9444 8439 145 145 0 9299 0 [pid=28421] vsize: 37776 Current children cumulated CPU time (s) 29.6 Current children cumulated vsize (Kb) 39900 [startup+40.0065 s] Raw data (loadavg): 0.95 0.96 0.91 2/57 28421 Raw data (/proc/28417/stat): 28417 (minisat+_script) S 28416 28417 2660 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855238664 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/28417/statm): 531 226 485 147 0 384 0 [pid=28417] vsize: 2124 Raw data (/proc/28421/stat): 28421 (minisat+_64-bit) R 28417 28417 2660 0 -1 0 8849 0 0 0 3924 34 0 0 25 0 1 0 1855238669 38899712 8493 4294967295 134512640 135094434 3221224432 3221223056 134557650 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/28421/statm): 9497 8493 145 145 0 9352 0 [pid=28421] vsize: 37988 Current children cumulated CPU time (s) 39.58 Current children cumulated vsize (Kb) 40112 [startup+50.0082 s] Raw data (loadavg): 0.96 0.96 0.91 2/57 28421 Raw data (/proc/28417/stat): 28417 (minisat+_script) S 28416 28417 2660 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855238664 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/28417/statm): 531 226 485 147 0 384 0 [pid=28417] vsize: 2124 Raw data (/proc/28421/stat): 28421 (minisat+_64-bit) R 28417 28417 2660 0 -1 0 8930 0 0 0 4923 35 0 0 25 0 1 0 1855238669 39251968 8574 4294967295 134512640 135094434 3221224432 3221223088 134558405 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/28421/statm): 9583 8574 145 145 0 9438 0 [pid=28421] vsize: 38332 Current children cumulated CPU time (s) 49.58 Current children cumulated vsize (Kb) 40456 [startup+60.0089 s] Raw data (loadavg): 0.97 0.96 0.91 2/57 28421 Raw data (/proc/28417/stat): 28417 (minisat+_script) S 28416 28417 2660 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855238664 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/28417/statm): 531 226 485 147 0 384 0 [pid=28417] vsize: 2124 Raw data (/proc/28421/stat): 28421 (minisat+_64-bit) R 28417 28417 2660 0 -1 0 8974 0 0 0 5922 36 0 0 25 0 1 0 1855238669 39424000 8618 4294967295 134512640 135094434 3221224432 3221223092 134553530 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/28421/statm): 9625 8618 145 145 0 9480 0 [pid=28421] vsize: 38500 Current children cumulated CPU time (s) 59.58 Current children cumulated vsize (Kb) 40624 [startup+70.0106 s] Raw data (loadavg): 0.97 0.96 0.91 2/57 28421 Raw data (/proc/28417/stat): 28417 (minisat+_script) S 28416 28417 2660 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855238664 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/28417/statm): 531 226 485 147 0 384 0 [pid=28417] vsize: 2124 Raw data (/proc/28421/stat): 28421 (minisat+_64-bit) R 28417 28417 2660 0 -1 0 9059 0 0 0 6921 36 0 0 25 0 1 0 1855238669 39768064 8703 4294967295 134512640 135094434 3221224432 3221223092 134553494 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/28421/statm): 9709 8703 145 145 0 9564 0 [pid=28421] vsize: 38836 Current children cumulated CPU time (s) 69.57 Current children cumulated vsize (Kb) 40960 [startup+80.0114 s] Raw data (loadavg): 0.98 0.96 0.91 2/57 28421 Raw data (/proc/28417/stat): 28417 (minisat+_script) S 28416 28417 2660 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855238664 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/28417/statm): 531 226 485 147 0 384 0 [pid=28417] vsize: 2124 Raw data (/proc/28421/stat): 28421 (minisat+_64-bit) R 28417 28417 2660 0 -1 0 9191 0 0 0 7918 38 0 0 25 0 1 0 1855238669 40296448 8835 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/28421/statm): 9838 8835 145 145 0 9693 0 [pid=28421] vsize: 39352 Current children cumulated CPU time (s) 79.56 Current children cumulated vsize (Kb) 41476 [startup+90.0121 s] Raw data (loadavg): 0.98 0.96 0.91 2/57 28421 Raw data (/proc/28417/stat): 28417 (minisat+_script) S 28416 28417 2660 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855238664 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/28417/statm): 531 226 485 147 0 384 0 [pid=28417] vsize: 2124 Raw data (/proc/28421/stat): 28421 (minisat+_64-bit) R 28417 28417 2660 0 -1 0 9252 0 0 0 8918 38 0 0 25 0 1 0 1855238669 40546304 8896 4294967295 134512640 135094434 3221224432 3221223088 134558208 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/28421/statm): 9899 8896 145 145 0 9754 0 [pid=28421] vsize: 39596 Current children cumulated CPU time (s) 89.56 Current children cumulated vsize (Kb) 41720 [startup+100.013 s] Raw data (loadavg): 0.98 0.96 0.91 2/57 28421 Raw data (/proc/28417/stat): 28417 (minisat+_script) S 28416 28417 2660 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855238664 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/28417/statm): 531 226 485 147 0 384 0 [pid=28417] vsize: 2124 Raw data (/proc/28421/stat): 28421 (minisat+_64-bit) R 28417 28417 2660 0 -1 0 9315 0 0 0 9916 40 0 0 25 0 1 0 1855238669 40792064 8959 4294967295 134512640 135094434 3221224432 3221223068 134557560 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/28421/statm): 9959 8959 145 145 0 9814 0 [pid=28421] vsize: 39836 Current children cumulated CPU time (s) 99.56 Current children cumulated vsize (Kb) 41960 [startup+110.014 s] Raw data (loadavg): 0.98 0.96 0.91 2/57 28421 Raw data (/proc/28417/stat): 28417 (minisat+_script) S 28416 28417 2660 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855238664 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/28417/statm): 531 226 485 147 0 384 0 [pid=28417] vsize: 2124 Raw data (/proc/28421/stat): 28421 (minisat+_64-bit) R 28417 28417 2660 0 -1 0 9367 0 0 0 10915 41 0 0 25 0 1 0 1855238669 41054208 9011 4294967295 134512640 135094434 3221224432 3221223088 134557835 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/28421/statm): 10023 9011 145 145 0 9878 0 [pid=28421] vsize: 40092 Current children cumulated CPU time (s) 109.56 Current children cumulated vsize (Kb) 42216 [startup+120.014 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 28421 Raw data (/proc/28417/stat): 28417 (minisat+_script) S 28416 28417 2660 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855238664 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/28417/statm): 531 226 485 147 0 384 0 [pid=28417] vsize: 2124 Raw data (/proc/28421/stat): 28421 (minisat+_64-bit) R 28417 28417 2660 0 -1 0 9447 0 0 0 11913 42 0 0 25 0 1 0 1855238669 41369600 9091 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/28421/statm): 10100 9091 145 145 0 9955 0 [pid=28421] vsize: 40400 Current children cumulated CPU time (s) 119.55 Current children cumulated vsize (Kb) 42524 [startup+130.015 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 28421 Raw data (/proc/28417/stat): 28417 (minisat+_script) S 28416 28417 2660 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855238664 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/28417/statm): 531 226 485 147 0 384 0 [pid=28417] vsize: 2124 Raw data (/proc/28421/stat): 28421 (minisat+_64-bit) R 28417 28417 2660 0 -1 0 9531 0 0 0 12912 43 0 0 25 0 1 0 1855238669 41709568 9175 4294967295 134512640 135094434 3221224432 3221223056 134557596 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/28421/statm): 10183 9175 145 145 0 10038 0 [pid=28421] vsize: 40732 Current children cumulated CPU time (s) 129.55 Current children cumulated vsize (Kb) 42856 [startup+140.016 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 28421 Raw data (/proc/28417/stat): 28417 (minisat+_script) S 28416 28417 2660 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855238664 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/28417/statm): 531 226 485 147 0 384 0 [pid=28417] vsize: 2124 Raw data (/proc/28421/stat): 28421 (minisat+_64-bit) R 28417 28417 2660 0 -1 0 9614 0 0 0 13910 43 0 0 25 0 1 0 1855238669 42049536 9258 4294967295 134512640 135094434 3221224432 3221221280 134677307 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/28421/statm): 10266 9258 145 145 0 10121 0 [pid=28421] vsize: 41064 Current children cumulated CPU time (s) 139.53 Current children cumulated vsize (Kb) 43188 [startup+150.016 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 28421 Raw data (/proc/28417/stat): 28417 (minisat+_script) S 28416 28417 2660 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855238664 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/28417/statm): 531 226 485 147 0 384 0 [pid=28417] vsize: 2124 Raw data (/proc/28421/stat): 28421 (minisat+_64-bit) R 28417 28417 2660 0 -1 0 9648 0 0 0 14909 44 0 0 25 0 1 0 1855238669 42160128 9292 4294967295 134512640 135094434 3221224432 3221223064 134557561 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/28421/statm): 10293 9292 145 145 0 10148 0 [pid=28421] vsize: 41172 Current children cumulated CPU time (s) 149.53 Current children cumulated vsize (Kb) 43296 [startup+160.017 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 28421 Raw data (/proc/28417/stat): 28417 (minisat+_script) S 28416 28417 2660 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855238664 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/28417/statm): 531 226 485 147 0 384 0 [pid=28417] vsize: 2124 Raw data (/proc/28421/stat): 28421 (minisat+_64-bit) R 28417 28417 2660 0 -1 0 9744 0 0 0 15907 45 0 0 25 0 1 0 1855238669 42532864 9388 4294967295 134512640 135094434 3221224432 3221223104 134556468 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/28421/statm): 10384 9388 145 145 0 10239 0 [pid=28421] vsize: 41536 Current children cumulated CPU time (s) 159.52 Current children cumulated vsize (Kb) 43660 [startup+170.018 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 28421 Raw data (/proc/28417/stat): 28417 (minisat+_script) S 28416 28417 2660 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855238664 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/28417/statm): 531 226 485 147 0 384 0 [pid=28417] vsize: 2124 Raw data (/proc/28421/stat): 28421 (minisat+_64-bit) R 28417 28417 2660 0 -1 0 9873 0 0 0 16905 45 0 0 25 0 1 0 1855238669 43057152 9517 4294967295 134512640 135094434 3221224432 3221223088 134558411 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/28421/statm): 10512 9517 145 145 0 10367 0 [pid=28421] vsize: 42048 Current children cumulated CPU time (s) 169.5 Current children cumulated vsize (Kb) 44172 [startup+180.019 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 28421 Raw data (/proc/28417/stat): 28417 (minisat+_script) S 28416 28417 2660 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855238664 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/28417/statm): 531 226 485 147 0 384 0 [pid=28417] vsize: 2124 Raw data (/proc/28421/stat): 28421 (minisat+_64-bit) R 28417 28417 2660 0 -1 0 9951 0 0 0 17903 46 0 0 25 0 1 0 1855238669 43372544 9595 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/28421/statm): 10589 9595 145 145 0 10444 0 [pid=28421] vsize: 42356 Current children cumulated CPU time (s) 179.49 Current children cumulated vsize (Kb) 44480 [startup+190.019 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 28421 Raw data (/proc/28417/stat): 28417 (minisat+_script) S 28416 28417 2660 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855238664 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/28417/statm): 531 226 485 147 0 384 0 [pid=28417] vsize: 2124 Raw data (/proc/28421/stat): 28421 (minisat+_64-bit) R 28417 28417 2660 0 -1 0 10080 0 0 0 18902 47 0 0 25 0 1 0 1855238669 43888640 9724 4294967295 134512640 135094434 3221224432 3221222256 134677049 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/28421/statm): 10715 9724 145 145 0 10570 0 [pid=28421] vsize: 42860 Current children cumulated CPU time (s) 189.49 Current children cumulated vsize (Kb) 44984 [startup+200.02 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 28421 Raw data (/proc/28417/stat): 28417 (minisat+_script) S 28416 28417 2660 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855238664 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/28417/statm): 531 226 485 147 0 384 0 [pid=28417] vsize: 2124 Raw data (/proc/28421/stat): 28421 (minisat+_64-bit) R 28417 28417 2660 0 -1 0 10149 0 0 0 19902 47 0 0 25 0 1 0 1855238669 44298240 9793 4294967295 134512640 135094434 3221224432 3221223056 134557696 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/28421/statm): 10815 9793 145 145 0 10670 0 [pid=28421] vsize: 43260 Current children cumulated CPU time (s) 199.49 Current children cumulated vsize (Kb) 45384 [startup+210.021 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 28421 Raw data (/proc/28417/stat): 28417 (minisat+_script) S 28416 28417 2660 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855238664 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/28417/statm): 531 226 485 147 0 384 0 [pid=28417] vsize: 2124 Raw data (/proc/28421/stat): 28421 (minisat+_64-bit) R 28417 28417 2660 0 -1 0 10213 0 0 0 20901 48 0 0 25 0 1 0 1855238669 44556288 9857 4294967295 134512640 135094434 3221224432 3221223056 134562104 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/28421/statm): 10878 9857 145 145 0 10733 0 [pid=28421] vsize: 43512 Current children cumulated CPU time (s) 209.49 Current children cumulated vsize (Kb) 45636 [startup+220.022 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 28421 Raw data (/proc/28417/stat): 28417 (minisat+_script) S 28416 28417 2660 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855238664 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/28417/statm): 531 226 485 147 0 384 0 [pid=28417] vsize: 2124 Raw data (/proc/28421/stat): 28421 (minisat+_64-bit) R 28417 28417 2660 0 -1 0 10290 0 0 0 21900 49 0 0 25 0 1 0 1855238669 44879872 9934 4294967295 134512640 135094434 3221224432 3221223024 134557016 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/28421/statm): 10957 9934 145 145 0 10812 0 [pid=28421] vsize: 43828 Current children cumulated CPU time (s) 219.49 Current children cumulated vsize (Kb) 45952 [startup+230.022 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 28421 Raw data (/proc/28417/stat): 28417 (minisat+_script) S 28416 28417 2660 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855238664 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/28417/statm): 531 226 485 147 0 384 0 [pid=28417] vsize: 2124 Raw data (/proc/28421/stat): 28421 (minisat+_64-bit) R 28417 28417 2660 0 -1 0 10365 0 0 0 22900 49 0 0 25 0 1 0 1855238669 45277184 10009 4294967295 134512640 135094434 3221224432 3221223088 134557948 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/28421/statm): 11054 10009 145 145 0 10909 0 [pid=28421] vsize: 44216 Current children cumulated CPU time (s) 229.49 Current children cumulated vsize (Kb) 46340 [startup+240.023 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 28421 Raw data (/proc/28417/stat): 28417 (minisat+_script) S 28416 28417 2660 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855238664 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/28417/statm): 531 226 485 147 0 384 0 [pid=28417] vsize: 2124 Raw data (/proc/28421/stat): 28421 (minisat+_64-bit) R 28417 28417 2660 0 -1 0 10406 0 0 0 23899 49 0 0 25 0 1 0 1855238669 45441024 10050 4294967295 134512640 135094434 3221224432 3221223120 134554746 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/28421/statm): 11094 10050 145 145 0 10949 0 [pid=28421] vsize: 44376 Current children cumulated CPU time (s) 239.48 Current children cumulated vsize (Kb) 46500 [startup+250.024 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 28421 Raw data (/proc/28417/stat): 28417 (minisat+_script) S 28416 28417 2660 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855238664 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/28417/statm): 531 226 485 147 0 384 0 [pid=28417] vsize: 2124 Raw data (/proc/28421/stat): 28421 (minisat+_64-bit) R 28417 28417 2660 0 -1 0 10470 0 0 0 24898 50 0 0 19 0 1 0 1855238669 45699072 10114 4294967295 134512640 135094434 3221224432 3221223056 134557596 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/28421/statm): 11157 10114 145 145 0 11012 0 [pid=28421] vsize: 44628 Current children cumulated CPU time (s) 249.48 Current children cumulated vsize (Kb) 46752 [startup+260.023 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 28421 Raw data (/proc/28417/stat): 28417 (minisat+_script) S 28416 28417 2660 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855238664 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/28417/statm): 531 226 485 147 0 384 0 [pid=28417] vsize: 2124 Raw data (/proc/28421/stat): 28421 (minisat+_64-bit) R 28417 28417 2660 0 -1 0 10566 0 0 0 25896 51 0 0 25 0 1 0 1855238669 46092288 10210 4294967295 134512640 135094434 3221224432 3221223056 134557717 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/28421/statm): 11253 10210 145 145 0 11108 0 [pid=28421] vsize: 45012 Current children cumulated CPU time (s) 259.47 Current children cumulated vsize (Kb) 47136 [startup+270.025 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 28421 Raw data (/proc/28417/stat): 28417 (minisat+_script) S 28416 28417 2660 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855238664 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/28417/statm): 531 226 485 147 0 384 0 [pid=28417] vsize: 2124 Raw data (/proc/28421/stat): 28421 (minisat+_64-bit) R 28417 28417 2660 0 -1 0 10688 0 0 0 26895 52 0 0 25 0 1 0 1855238669 46579712 10332 4294967295 134512640 135094434 3221224432 3221223056 134557577 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/28421/statm): 11372 10332 145 145 0 11227 0 [pid=28421] vsize: 45488 Current children cumulated CPU time (s) 269.47 Current children cumulated vsize (Kb) 47612 [startup+280.026 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 28421 Raw data (/proc/28417/stat): 28417 (minisat+_script) S 28416 28417 2660 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855238664 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/28417/statm): 531 226 485 147 0 384 0 [pid=28417] vsize: 2124 Raw data (/proc/28421/stat): 28421 (minisat+_64-bit) R 28417 28417 2660 0 -1 0 10760 0 0 0 27894 52 0 0 25 0 1 0 1855238669 46870528 10404 4294967295 134512640 135094434 3221224432 3221223056 134557596 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/28421/statm): 11443 10404 145 145 0 11298 0 [pid=28421] vsize: 45772 Current children cumulated CPU time (s) 279.46 Current children cumulated vsize (Kb) 47896 [startup+290.027 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 28421 Raw data (/proc/28417/stat): 28417 (minisat+_script) S 28416 28417 2660 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855238664 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/28417/statm): 531 226 485 147 0 384 0 [pid=28417] vsize: 2124 Raw data (/proc/28421/stat): 28421 (minisat+_64-bit) R 28417 28417 2660 0 -1 0 10851 0 0 0 28893 53 0 0 25 0 1 0 1855238669 47243264 10495 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/28421/statm): 11534 10495 145 145 0 11389 0 [pid=28421] vsize: 46136 Current children cumulated CPU time (s) 289.46 Current children cumulated vsize (Kb) 48260 [startup+300.027 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 28421 Raw data (/proc/28417/stat): 28417 (minisat+_script) S 28416 28417 2660 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855238664 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/28417/statm): 531 226 485 147 0 384 0 [pid=28417] vsize: 2124 Raw data (/proc/28421/stat): 28421 (minisat+_64-bit) R 28417 28417 2660 0 -1 0 10940 0 0 0 29892 53 0 0 25 0 1 0 1855238669 47607808 10584 4294967295 134512640 135094434 3221224432 3221223088 134558249 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/28421/statm): 11623 10584 145 145 0 11478 0 [pid=28421] vsize: 46492 Current children cumulated CPU time (s) 299.45 Current children cumulated vsize (Kb) 48616 [startup+310.028 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 28421 Raw data (/proc/28417/stat): 28417 (minisat+_script) S 28416 28417 2660 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855238664 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/28417/statm): 531 226 485 147 0 384 0 [pid=28417] vsize: 2124 Raw data (/proc/28421/stat): 28421 (minisat+_64-bit) R 28417 28417 2660 0 -1 0 11020 0 0 0 30892 53 0 0 25 0 1 0 1855238669 47927296 10664 4294967295 134512640 135094434 3221224432 3221223056 134557648 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/28421/statm): 11701 10664 145 145 0 11556 0 [pid=28421] vsize: 46804 Current children cumulated CPU time (s) 309.45 Current children cumulated vsize (Kb) 48928 [startup+320.03 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 28421 Raw data (/proc/28417/stat): 28417 (minisat+_script) S 28416 28417 2660 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855238664 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/28417/statm): 531 226 485 147 0 384 0 [pid=28417] vsize: 2124 Raw data (/proc/28421/stat): 28421 (minisat+_64-bit) R 28417 28417 2660 0 -1 0 11130 0 0 0 31890 54 0 0 25 0 1 0 1855238669 48373760 10774 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/28421/statm): 11810 10774 145 145 0 11665 0 [pid=28421] vsize: 47240 Current children cumulated CPU time (s) 319.44 Current children cumulated vsize (Kb) 49364 [startup+330.032 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 28421 Raw data (/proc/28417/stat): 28417 (minisat+_script) S 28416 28417 2660 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855238664 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/28417/statm): 531 226 485 147 0 384 0 [pid=28417] vsize: 2124 Raw data (/proc/28421/stat): 28421 (minisat+_64-bit) R 28417 28417 2660 0 -1 0 11215 0 0 0 32889 55 0 0 25 0 1 0 1855238669 48717824 10859 4294967295 134512640 135094434 3221224432 3221223088 134558249 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/28421/statm): 11894 10859 145 145 0 11749 0 [pid=28421] vsize: 47576 Current children cumulated CPU time (s) 329.44 Current children cumulated vsize (Kb) 49700 [startup+340.032 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 28421 Raw data (/proc/28417/stat): 28417 (minisat+_script) S 28416 28417 2660 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855238664 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/28417/statm): 531 226 485 147 0 384 0 [pid=28417] vsize: 2124 Raw data (/proc/28421/stat): 28421 (minisat+_64-bit) R 28417 28417 2660 0 -1 0 11312 0 0 0 33887 56 0 0 25 0 1 0 1855238669 49111040 10956 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/28421/statm): 11990 10956 145 145 0 11845 0 [pid=28421] vsize: 47960 Current children cumulated CPU time (s) 339.43 Current children cumulated vsize (Kb) 50084 [startup+350.034 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 28421 Raw data (/proc/28417/stat): 28417 (minisat+_script) S 28416 28417 2660 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855238664 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/28417/statm): 531 226 485 147 0 384 0 [pid=28417] vsize: 2124 Raw data (/proc/28421/stat): 28421 (minisat+_64-bit) R 28417 28417 2660 0 -1 0 11365 0 0 0 34886 57 0 0 25 0 1 0 1855238669 49328128 11009 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/28421/statm): 12043 11009 145 145 0 11898 0 [pid=28421] vsize: 48172 Current children cumulated CPU time (s) 349.43 Current children cumulated vsize (Kb) 50296 [startup+360.035 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 28421 Raw data (/proc/28417/stat): 28417 (minisat+_script) S 28416 28417 2660 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855238664 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/28417/statm): 531 226 485 147 0 384 0 [pid=28417] vsize: 2124 Raw data (/proc/28421/stat): 28421 (minisat+_64-bit) R 28417 28417 2660 0 -1 0 11425 0 0 0 35885 57 0 0 25 0 1 0 1855238669 49569792 11069 4294967295 134512640 135094434 3221224432 3221223240 134553433 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/28421/statm): 12102 11069 145 145 0 11957 0 [pid=28421] vsize: 48408 Current children cumulated CPU time (s) 359.42 Current children cumulated vsize (Kb) 50532 [startup+370.035 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 28421 Raw data (/proc/28417/stat): 28417 (minisat+_script) S 28416 28417 2660 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855238664 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/28417/statm): 531 226 485 147 0 384 0 [pid=28417] vsize: 2124 Raw data (/proc/28421/stat): 28421 (minisat+_64-bit) R 28417 28417 2660 0 -1 0 11460 0 0 0 36884 58 0 0 25 0 1 0 1855238669 49704960 11104 4294967295 134512640 135094434 3221224432 3221223104 134556323 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/28421/statm): 12135 11104 145 145 0 11990 0 [pid=28421] vsize: 48540 Current children cumulated CPU time (s) 369.42 Current children cumulated vsize (Kb) 50664 [startup+380.036 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 28421 Raw data (/proc/28417/stat): 28417 (minisat+_script) S 28416 28417 2660 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855238664 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/28417/statm): 531 226 485 147 0 384 0 [pid=28417] vsize: 2124 Raw data (/proc/28421/stat): 28421 (minisat+_64-bit) R 28417 28417 2660 0 -1 0 11571 0 0 0 37881 60 0 0 25 0 1 0 1855238669 50155520 11215 4294967295 134512640 135094434 3221224432 3221223024 134557334 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/28421/statm): 12245 11215 145 145 0 12100 0 [pid=28421] vsize: 48980 Current children cumulated CPU time (s) 379.41 Current children cumulated vsize (Kb) 51104 [startup+390.037 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 28421 Raw data (/proc/28417/stat): 28417 (minisat+_script) S 28416 28417 2660 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855238664 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/28417/statm): 531 226 485 147 0 384 0 [pid=28417] vsize: 2124 Raw data (/proc/28421/stat): 28421 (minisat+_64-bit) R 28417 28417 2660 0 -1 0 11648 0 0 0 38879 61 0 0 25 0 1 0 1855238669 50466816 11292 4294967295 134512640 135094434 3221224432 3221223088 134557945 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/28421/statm): 12321 11292 145 145 0 12176 0 [pid=28421] vsize: 49284 Current children cumulated CPU time (s) 389.4 Current children cumulated vsize (Kb) 51408 [startup+400.038 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 28421 Raw data (/proc/28417/stat): 28417 (minisat+_script) S 28416 28417 2660 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855238664 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/28417/statm): 531 226 485 147 0 384 0 [pid=28417] vsize: 2124 Raw data (/proc/28421/stat): 28421 (minisat+_64-bit) R 28417 28417 2660 0 -1 0 11764 0 0 0 39877 62 0 0 25 0 1 0 1855238669 50937856 11408 4294967295 134512640 135094434 3221224432 3221223220 134553515 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/28421/statm): 12436 11408 145 145 0 12291 0 [pid=28421] vsize: 49744 Current children cumulated CPU time (s) 399.39 Current children cumulated vsize (Kb) 51868 [startup+410.038 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 28421 Raw data (/proc/28417/stat): 28417 (minisat+_script) S 28416 28417 2660 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855238664 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/28417/statm): 531 226 485 147 0 384 0 [pid=28417] vsize: 2124 Raw data (/proc/28421/stat): 28421 (minisat+_64-bit) R 28417 28417 2660 0 -1 0 11788 0 0 0 40876 63 0 0 25 0 1 0 1855238669 51032064 11432 4294967295 134512640 135094434 3221224432 3221223064 134557561 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/28421/statm): 12459 11432 145 145 0 12314 0 [pid=28421] vsize: 49836 Current children cumulated CPU time (s) 409.39 Current children cumulated vsize (Kb) 51960 [startup+420.04 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 28421 Raw data (/proc/28417/stat): 28417 (minisat+_script) S 28416 28417 2660 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855238664 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/28417/statm): 531 226 485 147 0 384 0 [pid=28417] vsize: 2124 Raw data (/proc/28421/stat): 28421 (minisat+_64-bit) R 28417 28417 2660 0 -1 0 11877 0 0 0 41875 63 0 0 25 0 1 0 1855238669 51392512 11521 4294967295 134512640 135094434 3221224432 3221223120 134554746 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/28421/statm): 12547 11521 145 145 0 12402 0 [pid=28421] vsize: 50188 Current children cumulated CPU time (s) 419.38 Current children cumulated vsize (Kb) 52312 [startup+430.041 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 28421 Raw data (/proc/28417/stat): 28417 (minisat+_script) S 28416 28417 2660 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855238664 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/28417/statm): 531 226 485 147 0 384 0 [pid=28417] vsize: 2124 Raw data (/proc/28421/stat): 28421 (minisat+_64-bit) R 28417 28417 2660 0 -1 0 11958 0 0 0 42874 64 0 0 25 0 1 0 1855238669 51720192 11602 4294967295 134512640 135094434 3221224432 3221223024 134557401 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/28421/statm): 12627 11602 145 145 0 12482 0 [pid=28421] vsize: 50508 Current children cumulated CPU time (s) 429.38 Current children cumulated vsize (Kb) 52632 [startup+440.041 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 28421 Raw data (/proc/28417/stat): 28417 (minisat+_script) S 28416 28417 2660 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855238664 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/28417/statm): 531 226 485 147 0 384 0 [pid=28417] vsize: 2124 Raw data (/proc/28421/stat): 28421 (minisat+_64-bit) R 28417 28417 2660 0 -1 0 12021 0 0 0 43873 65 0 0 25 0 1 0 1855238669 51974144 11665 4294967295 134512640 135094434 3221224432 3221223024 134556864 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/28421/statm): 12689 11665 145 145 0 12544 0 [pid=28421] vsize: 50756 Current children cumulated CPU time (s) 439.38 Current children cumulated vsize (Kb) 52880 [startup+450.041 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 28421 Raw data (/proc/28417/stat): 28417 (minisat+_script) S 28416 28417 2660 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855238664 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/28417/statm): 531 226 485 147 0 384 0 [pid=28417] vsize: 2124 Raw data (/proc/28421/stat): 28421 (minisat+_64-bit) R 28417 28417 2660 0 -1 0 12058 0 0 0 44872 65 0 0 25 0 1 0 1855238669 52125696 11702 4294967295 134512640 135094434 3221224432 3221223056 134557675 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/28421/statm): 12726 11702 145 145 0 12581 0 [pid=28421] vsize: 50904 Current children cumulated CPU time (s) 449.37 Current children cumulated vsize (Kb) 53028 [startup+460.042 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 28421 Raw data (/proc/28417/stat): 28417 (minisat+_script) S 28416 28417 2660 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855238664 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/28417/statm): 531 226 485 147 0 384 0 [pid=28417] vsize: 2124 Raw data (/proc/28421/stat): 28421 (minisat+_64-bit) R 28417 28417 2660 0 -1 0 12111 0 0 0 45871 65 0 0 25 0 1 0 1855238669 52338688 11755 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/28421/statm): 12778 11755 145 145 0 12633 0 [pid=28421] vsize: 51112 Current children cumulated CPU time (s) 459.36 Current children cumulated vsize (Kb) 53236 [startup+470.043 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 28421 Raw data (/proc/28417/stat): 28417 (minisat+_script) S 28416 28417 2660 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855238664 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/28417/statm): 531 226 485 147 0 384 0 [pid=28417] vsize: 2124 Raw data (/proc/28421/stat): 28421 (minisat+_64-bit) R 28417 28417 2660 0 -1 0 12194 0 0 0 46870 66 0 0 25 0 1 0 1855238669 52674560 11838 4294967295 134512640 135094434 3221224432 3221223024 134556862 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/28421/statm): 12860 11838 145 145 0 12715 0 [pid=28421] vsize: 51440 Current children cumulated CPU time (s) 469.36 Current children cumulated vsize (Kb) 53564 [startup+480.043 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 28421 Raw data (/proc/28417/stat): 28417 (minisat+_script) S 28416 28417 2660 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855238664 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/28417/statm): 531 226 485 147 0 384 0 [pid=28417] vsize: 2124 Raw data (/proc/28421/stat): 28421 (minisat+_64-bit) R 28417 28417 2660 0 -1 0 12275 0 0 0 47870 66 0 0 25 0 1 0 1855238669 53002240 11919 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/28421/statm): 12940 11919 145 145 0 12795 0 [pid=28421] vsize: 51760 Current children cumulated CPU time (s) 479.36 Current children cumulated vsize (Kb) 53884 [startup+490.044 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 28421 Raw data (/proc/28417/stat): 28417 (minisat+_script) S 28416 28417 2660 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855238664 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/28417/statm): 531 226 485 147 0 384 0 [pid=28417] vsize: 2124 Raw data (/proc/28421/stat): 28421 (minisat+_64-bit) R 28417 28417 2660 0 -1 0 12351 0 0 0 48869 67 0 0 25 0 1 0 1855238669 53313536 11995 4294967295 134512640 135094434 3221224432 3221223024 134556868 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/28421/statm): 13016 11995 145 145 0 12871 0 [pid=28421] vsize: 52064 Current children cumulated CPU time (s) 489.36 Current children cumulated vsize (Kb) 54188 [startup+500.045 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 28421 Raw data (/proc/28417/stat): 28417 (minisat+_script) S 28416 28417 2660 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855238664 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/28417/statm): 531 226 485 147 0 384 0 [pid=28417] vsize: 2124 Raw data (/proc/28421/stat): 28421 (minisat+_64-bit) R 28417 28417 2660 0 -1 0 12442 0 0 0 49867 68 0 0 25 0 1 0 1855238669 53686272 12086 4294967295 134512640 135094434 3221224432 3221223064 134557561 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/28421/statm): 13107 12086 145 145 0 12962 0 [pid=28421] vsize: 52428 Current children cumulated CPU time (s) 499.35 Current children cumulated vsize (Kb) 54552 [startup+510.046 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 28421 Raw data (/proc/28417/stat): 28417 (minisat+_script) S 28416 28417 2660 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855238664 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/28417/statm): 531 226 485 147 0 384 0 [pid=28417] vsize: 2124 Raw data (/proc/28421/stat): 28421 (minisat+_64-bit) R 28417 28417 2660 0 -1 0 12516 0 0 0 50867 68 0 0 25 0 1 0 1855238669 53977088 12160 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/28421/statm): 13178 12160 145 145 0 13033 0 [pid=28421] vsize: 52712 Current children cumulated CPU time (s) 509.35 Current children cumulated vsize (Kb) 54836 [startup+520.046 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 28421 Raw data (/proc/28417/stat): 28417 (minisat+_script) S 28416 28417 2660 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855238664 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/28417/statm): 531 226 485 147 0 384 0 [pid=28417] vsize: 2124 Raw data (/proc/28421/stat): 28421 (minisat+_64-bit) R 28417 28417 2660 0 -1 0 12586 0 0 0 51865 69 0 0 25 0 1 0 1855238669 54521856 12230 4294967295 134512640 135094434 3221224432 3221223120 134554746 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/28421/statm): 13311 12230 145 145 0 13166 0 [pid=28421] vsize: 53244 Current children cumulated CPU time (s) 519.34 Current children cumulated vsize (Kb) 55368 [startup+530.047 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 28421 Raw data (/proc/28417/stat): 28417 (minisat+_script) S 28416 28417 2660 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855238664 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/28417/statm): 531 226 485 147 0 384 0 [pid=28417] vsize: 2124 Raw data (/proc/28421/stat): 28421 (minisat+_64-bit) R 28417 28417 2660 0 -1 0 12640 0 0 0 52864 69 0 0 25 0 1 0 1855238669 54738944 12284 4294967295 134512640 135094434 3221224432 3221223088 134558210 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/28421/statm): 13364 12284 145 145 0 13219 0 [pid=28421] vsize: 53456 Current children cumulated CPU time (s) 529.33 Current children cumulated vsize (Kb) 55580 [startup+540.048 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 28421 Raw data (/proc/28417/stat): 28417 (minisat+_script) S 28416 28417 2660 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855238664 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/28417/statm): 531 226 485 147 0 384 0 [pid=28417] vsize: 2124 Raw data (/proc/28421/stat): 28421 (minisat+_64-bit) R 28417 28417 2660 0 -1 0 12683 0 0 0 53863 70 0 0 25 0 1 0 1855238669 54915072 12327 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/28421/statm): 13407 12327 145 145 0 13262 0 [pid=28421] vsize: 53628 Current children cumulated CPU time (s) 539.33 Current children cumulated vsize (Kb) 55752 [startup+550.048 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 28421 Raw data (/proc/28417/stat): 28417 (minisat+_script) S 28416 28417 2660 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855238664 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/28417/statm): 531 226 485 147 0 384 0 [pid=28417] vsize: 2124 Raw data (/proc/28421/stat): 28421 (minisat+_64-bit) R 28417 28417 2660 0 -1 0 12729 0 0 0 54863 70 0 0 25 0 1 0 1855238669 55099392 12373 4294967295 134512640 135094434 3221224432 3221223088 134558249 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/28421/statm): 13452 12373 145 145 0 13307 0 [pid=28421] vsize: 53808 Current children cumulated CPU time (s) 549.33 Current children cumulated vsize (Kb) 55932 [startup+560.049 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 28421 Raw data (/proc/28417/stat): 28417 (minisat+_script) S 28416 28417 2660 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855238664 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/28417/statm): 531 226 485 147 0 384 0 [pid=28417] vsize: 2124 Raw data (/proc/28421/stat): 28421 (minisat+_64-bit) R 28417 28417 2660 0 -1 0 12792 0 0 0 55863 70 0 0 25 0 1 0 1855238669 55353344 12436 4294967295 134512640 135094434 3221224432 3221223136 134559017 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/28421/statm): 13514 12436 145 145 0 13369 0 [pid=28421] vsize: 54056 Current children cumulated CPU time (s) 559.33 Current children cumulated vsize (Kb) 56180 [startup+570.051 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 28421 Raw data (/proc/28417/stat): 28417 (minisat+_script) S 28416 28417 2660 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855238664 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/28417/statm): 531 226 485 147 0 384 0 [pid=28417] vsize: 2124 Raw data (/proc/28421/stat): 28421 (minisat+_64-bit) R 28417 28417 2660 0 -1 0 12833 0 0 0 56863 71 0 0 25 0 1 0 1855238669 55521280 12477 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/28421/statm): 13555 12477 145 145 0 13410 0 [pid=28421] vsize: 54220 Current children cumulated CPU time (s) 569.34 Current children cumulated vsize (Kb) 56344 [startup+580.052 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 28421 Raw data (/proc/28417/stat): 28417 (minisat+_script) S 28416 28417 2660 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855238664 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/28417/statm): 531 226 485 147 0 384 0 [pid=28417] vsize: 2124 Raw data (/proc/28421/stat): 28421 (minisat+_64-bit) R 28417 28417 2660 0 -1 0 12913 0 0 0 57862 71 0 0 25 0 1 0 1855238669 55844864 12557 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/28421/statm): 13634 12557 145 145 0 13489 0 [pid=28421] vsize: 54536 Current children cumulated CPU time (s) 579.33 Current children cumulated vsize (Kb) 56660 [startup+590.052 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 28421 Raw data (/proc/28417/stat): 28417 (minisat+_script) S 28416 28417 2660 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855238664 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/28417/statm): 531 226 485 147 0 384 0 [pid=28417] vsize: 2124 Raw data (/proc/28421/stat): 28421 (minisat+_64-bit) R 28417 28417 2660 0 -1 0 13012 0 0 0 58860 72 0 0 25 0 1 0 1855238669 56233984 12656 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/28421/statm): 13729 12656 145 145 0 13584 0 [pid=28421] vsize: 54916 Current children cumulated CPU time (s) 589.32 Current children cumulated vsize (Kb) 57040 [startup+600.054 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 28421 Raw data (/proc/28417/stat): 28417 (minisat+_script) S 28416 28417 2660 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855238664 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/28417/statm): 531 226 485 147 0 384 0 [pid=28417] vsize: 2124 Raw data (/proc/28421/stat): 28421 (minisat+_64-bit) R 28417 28417 2660 0 -1 0 13076 0 0 0 59860 72 0 0 25 0 1 0 1855238669 56492032 12720 4294967295 134512640 135094434 3221224432 3221223024 134557180 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/28421/statm): 13792 12720 145 145 0 13647 0 [pid=28421] vsize: 55168 Current children cumulated CPU time (s) 599.32 Current children cumulated vsize (Kb) 57292 [startup+610.054 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 28421 Raw data (/proc/28417/stat): 28417 (minisat+_script) S 28416 28417 2660 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855238664 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/28417/statm): 531 226 485 147 0 384 0 [pid=28417] vsize: 2124 Raw data (/proc/28421/stat): 28421 (minisat+_64-bit) R 28417 28417 2660 0 -1 0 13161 0 0 0 60858 73 0 0 25 0 1 0 1855238669 56836096 12805 4294967295 134512640 135094434 3221224432 3221223088 134558402 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/28421/statm): 13876 12805 145 145 0 13731 0 [pid=28421] vsize: 55504 Current children cumulated CPU time (s) 609.31 Current children cumulated vsize (Kb) 57628 [startup+620.055 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 28421 Raw data (/proc/28417/stat): 28417 (minisat+_script) S 28416 28417 2660 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855238664 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/28417/statm): 531 226 485 147 0 384 0 [pid=28417] vsize: 2124 Raw data (/proc/28421/stat): 28421 (minisat+_64-bit) R 28417 28417 2660 0 -1 0 13221 0 0 0 61858 74 0 0 25 0 1 0 1855238669 57081856 12865 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/28421/statm): 13936 12865 145 145 0 13791 0 [pid=28421] vsize: 55744 Current children cumulated CPU time (s) 619.32 Current children cumulated vsize (Kb) 57868 [startup+630.056 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 28421 Raw data (/proc/28417/stat): 28417 (minisat+_script) S 28416 28417 2660 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855238664 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/28417/statm): 531 226 485 147 0 384 0 [pid=28417] vsize: 2124 Raw data (/proc/28421/stat): 28421 (minisat+_64-bit) R 28417 28417 2660 0 -1 0 13299 0 0 0 62857 74 0 0 25 0 1 0 1855238669 57401344 12943 4294967295 134512640 135094434 3221224432 3221223044 134563055 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/28421/statm): 14014 12943 145 145 0 13869 0 [pid=28421] vsize: 56056 Current children cumulated CPU time (s) 629.31 Current children cumulated vsize (Kb) 58180 [startup+640.056 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 28421 Raw data (/proc/28417/stat): 28417 (minisat+_script) S 28416 28417 2660 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855238664 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/28417/statm): 531 226 485 147 0 384 0 [pid=28417] vsize: 2124 Raw data (/proc/28421/stat): 28421 (minisat+_64-bit) R 28417 28417 2660 0 -1 0 13384 0 0 0 63856 74 0 0 25 0 1 0 1855238669 57741312 13028 4294967295 134512640 135094434 3221224432 3221223024 134557398 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/28421/statm): 14097 13028 145 145 0 13952 0 [pid=28421] vsize: 56388 Current children cumulated CPU time (s) 639.3 Current children cumulated vsize (Kb) 58512 [startup+650.057 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 28421 Raw data (/proc/28417/stat): 28417 (minisat+_script) S 28416 28417 2660 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855238664 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/28417/statm): 531 226 485 147 0 384 0 [pid=28417] vsize: 2124 Raw data (/proc/28421/stat): 28421 (minisat+_64-bit) R 28417 28417 2660 0 -1 0 13437 0 0 0 64856 75 0 0 25 0 1 0 1855238669 57954304 13081 4294967295 134512640 135094434 3221224432 3221223088 134558159 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/28421/statm): 14149 13081 145 145 0 14004 0 [pid=28421] vsize: 56596 Current children cumulated CPU time (s) 649.31 Current children cumulated vsize (Kb) 58720 [startup+660.058 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 28421 Raw data (/proc/28417/stat): 28417 (minisat+_script) S 28416 28417 2660 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855238664 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/28417/statm): 531 226 485 147 0 384 0 [pid=28417] vsize: 2124 Raw data (/proc/28421/stat): 28421 (minisat+_64-bit) R 28417 28417 2660 0 -1 0 13487 0 0 0 65855 75 0 0 25 0 1 0 1855238669 58155008 13131 4294967295 134512640 135094434 3221224432 3221223104 134555953 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/28421/statm): 14198 13131 145 145 0 14053 0 [pid=28421] vsize: 56792 Current children cumulated CPU time (s) 659.3 Current children cumulated vsize (Kb) 58916 [startup+670.058 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 28421 Raw data (/proc/28417/stat): 28417 (minisat+_script) S 28416 28417 2660 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855238664 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/28417/statm): 531 226 485 147 0 384 0 [pid=28417] vsize: 2124 Raw data (/proc/28421/stat): 28421 (minisat+_64-bit) R 28417 28417 2660 0 -1 0 13550 0 0 0 66854 76 0 0 25 0 1 0 1855238669 58413056 13194 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/28421/statm): 14261 13194 145 145 0 14116 0 [pid=28421] vsize: 57044 Current children cumulated CPU time (s) 669.3 Current children cumulated vsize (Kb) 59168 [startup+680.059 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 28421 Raw data (/proc/28417/stat): 28417 (minisat+_script) S 28416 28417 2660 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855238664 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/28417/statm): 531 226 485 147 0 384 0 [pid=28417] vsize: 2124 Raw data (/proc/28421/stat): 28421 (minisat+_64-bit) R 28417 28417 2660 0 -1 0 13578 0 0 0 67854 76 0 0 25 0 1 0 1855238669 58523648 13222 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/28421/statm): 14288 13222 145 145 0 14143 0 [pid=28421] vsize: 57152 Current children cumulated CPU time (s) 679.3 Current children cumulated vsize (Kb) 59276 [startup+690.06 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 28421 Raw data (/proc/28417/stat): 28417 (minisat+_script) S 28416 28417 2660 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855238664 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/28417/statm): 531 226 485 147 0 384 0 [pid=28417] vsize: 2124 Raw data (/proc/28421/stat): 28421 (minisat+_64-bit) T 28417 28417 2660 0 -1 0 13617 0 0 0 68853 77 0 0 25 0 1 0 1855238669 58683392 13261 4294967295 134512640 135094434 3221224432 3221222796 134870330 0 0 5 16386 3222434794 0 0 17 1 0 0 Raw data (/proc/28421/statm): 14327 13261 145 145 0 14182 0 [pid=28421] vsize: 57308 Current children cumulated CPU time (s) 689.3 Current children cumulated vsize (Kb) 59432 [startup+700.06 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 28421 Raw data (/proc/28417/stat): 28417 (minisat+_script) S 28416 28417 2660 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855238664 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/28417/statm): 531 226 485 147 0 384 0 [pid=28417] vsize: 2124 Raw data (/proc/28421/stat): 28421 (minisat+_64-bit) R 28417 28417 2660 0 -1 0 13691 0 0 0 69851 78 0 0 25 0 1 0 1855238669 58982400 13335 4294967295 134512640 135094434 3221224432 3221223088 134558213 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/28421/statm): 14400 13335 145 145 0 14255 0 [pid=28421] vsize: 57600 Current children cumulated CPU time (s) 699.29 Current children cumulated vsize (Kb) 59724 [startup+710.061 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 28421 Raw data (/proc/28417/stat): 28417 (minisat+_script) S 28416 28417 2660 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855238664 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/28417/statm): 531 226 485 147 0 384 0 [pid=28417] vsize: 2124 Raw data (/proc/28421/stat): 28421 (minisat+_64-bit) R 28417 28417 2660 0 -1 0 13775 0 0 0 70849 80 0 0 25 0 1 0 1855238669 59322368 13419 4294967295 134512640 135094434 3221224432 3221223088 134558178 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/28421/statm): 14483 13419 145 145 0 14338 0 [pid=28421] vsize: 57932 Current children cumulated CPU time (s) 709.29 Current children cumulated vsize (Kb) 60056 [startup+720.062 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 28421 Raw data (/proc/28417/stat): 28417 (minisat+_script) S 28416 28417 2660 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855238664 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/28417/statm): 531 226 485 147 0 384 0 [pid=28417] vsize: 2124 Raw data (/proc/28421/stat): 28421 (minisat+_64-bit) R 28417 28417 2660 0 -1 0 13838 0 0 0 71848 80 0 0 25 0 1 0 1855238669 59580416 13482 4294967295 134512640 135094434 3221224432 3221223024 134557404 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/28421/statm): 14546 13482 145 145 0 14401 0 [pid=28421] vsize: 58184 Current children cumulated CPU time (s) 719.28 Current children cumulated vsize (Kb) 60308 [startup+730.063 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 28421 Raw data (/proc/28417/stat): 28417 (minisat+_script) S 28416 28417 2660 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855238664 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/28417/statm): 531 226 485 147 0 384 0 [pid=28417] vsize: 2124 Raw data (/proc/28421/stat): 28421 (minisat+_64-bit) R 28417 28417 2660 0 -1 0 13913 0 0 0 72847 81 0 0 25 0 1 0 1855238669 59883520 13557 4294967295 134512640 135094434 3221224432 3221223024 134556802 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/28421/statm): 14620 13557 145 145 0 14475 0 [pid=28421] vsize: 58480 Current children cumulated CPU time (s) 729.28 Current children cumulated vsize (Kb) 60604 [startup+740.063 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 28421 Raw data (/proc/28417/stat): 28417 (minisat+_script) S 28416 28417 2660 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855238664 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/28417/statm): 531 226 485 147 0 384 0 [pid=28417] vsize: 2124 Raw data (/proc/28421/stat): 28421 (minisat+_64-bit) R 28417 28417 2660 0 -1 0 13997 0 0 0 73846 82 0 0 25 0 1 0 1855238669 60227584 13641 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/28421/statm): 14704 13641 145 145 0 14559 0 [pid=28421] vsize: 58816 Current children cumulated CPU time (s) 739.28 Current children cumulated vsize (Kb) 60940 [startup+750.065 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 28421 Raw data (/proc/28417/stat): 28417 (minisat+_script) S 28416 28417 2660 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855238664 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/28417/statm): 531 226 485 147 0 384 0 [pid=28417] vsize: 2124 Raw data (/proc/28421/stat): 28421 (minisat+_64-bit) R 28417 28417 2660 0 -1 0 14082 0 0 0 74844 83 0 0 25 0 1 0 1855238669 60567552 13726 4294967295 134512640 135094434 3221224432 3221223056 134562057 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/28421/statm): 14787 13726 145 145 0 14642 0 [pid=28421] vsize: 59148 Current children cumulated CPU time (s) 749.27 Current children cumulated vsize (Kb) 61272 [startup+760.066 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 28421 Raw data (/proc/28417/stat): 28417 (minisat+_script) S 28416 28417 2660 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855238664 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/28417/statm): 531 226 485 147 0 384 0 [pid=28417] vsize: 2124 Raw data (/proc/28421/stat): 28421 (minisat+_64-bit) R 28417 28417 2660 0 -1 0 14165 0 0 0 75843 84 0 0 25 0 1 0 1855238669 60903424 13809 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/28421/statm): 14869 13809 145 145 0 14724 0 [pid=28421] vsize: 59476 Current children cumulated CPU time (s) 759.27 Current children cumulated vsize (Kb) 61600 [startup+770.067 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 28421 Raw data (/proc/28417/stat): 28417 (minisat+_script) S 28416 28417 2660 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855238664 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/28417/statm): 531 226 485 147 0 384 0 [pid=28417] vsize: 2124 Raw data (/proc/28421/stat): 28421 (minisat+_64-bit) R 28417 28417 2660 0 -1 0 14249 0 0 0 76842 84 0 0 25 0 1 0 1855238669 61247488 13893 4294967295 134512640 135094434 3221224432 3221223088 134558249 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/28421/statm): 14953 13893 145 145 0 14808 0 [pid=28421] vsize: 59812 Current children cumulated CPU time (s) 769.26 Current children cumulated vsize (Kb) 61936 [startup+780.068 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 28421 Raw data (/proc/28417/stat): 28417 (minisat+_script) S 28416 28417 2660 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855238664 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/28417/statm): 531 226 485 147 0 384 0 [pid=28417] vsize: 2124 Raw data (/proc/28421/stat): 28421 (minisat+_64-bit) R 28417 28417 2660 0 -1 0 14310 0 0 0 77841 85 0 0 25 0 1 0 1855238669 61501440 13954 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/28421/statm): 15015 13954 145 145 0 14870 0 [pid=28421] vsize: 60060 Current children cumulated CPU time (s) 779.26 Current children cumulated vsize (Kb) 62184 [startup+790.068 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 28421 Raw data (/proc/28417/stat): 28417 (minisat+_script) S 28416 28417 2660 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855238664 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/28417/statm): 531 226 485 147 0 384 0 [pid=28417] vsize: 2124 Raw data (/proc/28421/stat): 28421 (minisat+_64-bit) R 28417 28417 2660 0 -1 0 14554 0 0 0 78838 86 0 0 25 0 1 0 1855238669 62492672 14198 4294967295 134512640 135094434 3221224432 3221223120 134554746 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/28421/statm): 15257 14198 145 145 0 15112 0 [pid=28421] vsize: 61028 Current children cumulated CPU time (s) 789.24 Current children cumulated vsize (Kb) 63152 [startup+800.069 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 28421 Raw data (/proc/28417/stat): 28417 (minisat+_script) S 28416 28417 2660 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855238664 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/28417/statm): 531 226 485 147 0 384 0 [pid=28417] vsize: 2124 Raw data (/proc/28421/stat): 28421 (minisat+_64-bit) R 28417 28417 2660 0 -1 0 14614 0 0 0 79837 86 0 0 25 0 1 0 1855238669 62734336 14258 4294967295 134512640 135094434 3221224432 3221223088 134558213 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/28421/statm): 15316 14258 145 145 0 15171 0 [pid=28421] vsize: 61264 Current children cumulated CPU time (s) 799.23 Current children cumulated vsize (Kb) 63388 [startup+810.069 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 28421 Raw data (/proc/28417/stat): 28417 (minisat+_script) S 28416 28417 2660 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855238664 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/28417/statm): 531 226 485 147 0 384 0 [pid=28417] vsize: 2124 Raw data (/proc/28421/stat): 28421 (minisat+_64-bit) R 28417 28417 2660 0 -1 0 14700 0 0 0 80835 87 0 0 25 0 1 0 1855238669 63086592 14344 4294967295 134512640 135094434 3221224432 3221223104 134555568 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/28421/statm): 15402 14344 145 145 0 15257 0 [pid=28421] vsize: 61608 Current children cumulated CPU time (s) 809.22 Current children cumulated vsize (Kb) 63732 [startup+820.07 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 28421 Raw data (/proc/28417/stat): 28417 (minisat+_script) S 28416 28417 2660 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855238664 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/28417/statm): 531 226 485 147 0 384 0 [pid=28417] vsize: 2124 Raw data (/proc/28421/stat): 28421 (minisat+_64-bit) R 28417 28417 2660 0 -1 0 14834 0 0 0 81834 88 0 0 25 0 1 0 1855238669 63655936 14478 4294967295 134512640 135094434 3221224432 3221223024 134556826 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/28421/statm): 15541 14478 145 145 0 15396 0 [pid=28421] vsize: 62164 Current children cumulated CPU time (s) 819.22 Current children cumulated vsize (Kb) 64288 [startup+830.071 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 28421 Raw data (/proc/28417/stat): 28417 (minisat+_script) S 28416 28417 2660 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855238664 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/28417/statm): 531 226 485 147 0 384 0 [pid=28417] vsize: 2124 Raw data (/proc/28421/stat): 28421 (minisat+_64-bit) R 28417 28417 2660 0 -1 0 14980 0 0 0 82832 89 0 0 25 0 1 0 1855238669 64241664 14624 4294967295 134512640 135094434 3221224432 3221223024 134557423 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/28421/statm): 15684 14624 145 145 0 15539 0 [pid=28421] vsize: 62736 Current children cumulated CPU time (s) 829.21 Current children cumulated vsize (Kb) 64860 [startup+840.072 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 28421 Raw data (/proc/28417/stat): 28417 (minisat+_script) S 28416 28417 2660 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855238664 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/28417/statm): 531 226 485 147 0 384 0 [pid=28417] vsize: 2124 Raw data (/proc/28421/stat): 28421 (minisat+_64-bit) R 28417 28417 2660 0 -1 0 15081 0 0 0 83830 90 0 0 25 0 1 0 1855238669 64651264 14725 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/28421/statm): 15784 14725 145 145 0 15639 0 [pid=28421] vsize: 63136 Current children cumulated CPU time (s) 839.2 Current children cumulated vsize (Kb) 65260 [startup+850.072 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 28421 Raw data (/proc/28417/stat): 28417 (minisat+_script) S 28416 28417 2660 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855238664 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/28417/statm): 531 226 485 147 0 384 0 [pid=28417] vsize: 2124 Raw data (/proc/28421/stat): 28421 (minisat+_64-bit) R 28417 28417 2660 0 -1 0 15142 0 0 0 84830 90 0 0 25 0 1 0 1855238669 64897024 14786 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/28421/statm): 15844 14786 145 145 0 15699 0 [pid=28421] vsize: 63376 Current children cumulated CPU time (s) 849.2 Current children cumulated vsize (Kb) 65500 [startup+860.073 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 28421 Raw data (/proc/28417/stat): 28417 (minisat+_script) S 28416 28417 2660 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855238664 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/28417/statm): 531 226 485 147 0 384 0 [pid=28417] vsize: 2124 Raw data (/proc/28421/stat): 28421 (minisat+_64-bit) R 28417 28417 2660 0 -1 0 15228 0 0 0 85828 91 0 0 25 0 1 0 1855238669 65261568 14872 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/28421/statm): 15933 14872 145 145 0 15788 0 [pid=28421] vsize: 63732 Current children cumulated CPU time (s) 859.19 Current children cumulated vsize (Kb) 65856 [startup+870.075 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 28421 Raw data (/proc/28417/stat): 28417 (minisat+_script) S 28416 28417 2660 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855238664 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/28417/statm): 531 226 485 147 0 384 0 [pid=28417] vsize: 2124 Raw data (/proc/28421/stat): 28421 (minisat+_64-bit) R 28417 28417 2660 0 -1 0 15290 0 0 0 86827 91 0 0 25 0 1 0 1855238669 65511424 14934 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/28421/statm): 15994 14934 145 145 0 15849 0 [pid=28421] vsize: 63976 Current children cumulated CPU time (s) 869.18 Current children cumulated vsize (Kb) 66100 [startup+880.075 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 28421 Raw data (/proc/28417/stat): 28417 (minisat+_script) S 28416 28417 2660 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855238664 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/28417/statm): 531 226 485 147 0 384 0 [pid=28417] vsize: 2124 Raw data (/proc/28421/stat): 28421 (minisat+_64-bit) R 28417 28417 2660 0 -1 0 15336 0 0 0 87827 92 0 0 25 0 1 0 1855238669 65695744 14980 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/28421/statm): 16039 14980 145 145 0 15894 0 [pid=28421] vsize: 64156 Current children cumulated CPU time (s) 879.19 Current children cumulated vsize (Kb) 66280 [startup+890.076 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 28421 Raw data (/proc/28417/stat): 28417 (minisat+_script) S 28416 28417 2660 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855238664 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/28417/statm): 531 226 485 147 0 384 0 [pid=28417] vsize: 2124 Raw data (/proc/28421/stat): 28421 (minisat+_64-bit) R 28417 28417 2660 0 -1 0 15396 0 0 0 88826 92 0 0 25 0 1 0 1855238669 65949696 15040 4294967295 134512640 135094434 3221224432 3221223088 134558159 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/28421/statm): 16101 15040 145 145 0 15956 0 [pid=28421] vsize: 64404 Current children cumulated CPU time (s) 889.18 Current children cumulated vsize (Kb) 66528 [startup+900.077 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 28421 Raw data (/proc/28417/stat): 28417 (minisat+_script) S 28416 28417 2660 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855238664 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/28417/statm): 531 226 485 147 0 384 0 [pid=28417] vsize: 2124 Raw data (/proc/28421/stat): 28421 (minisat+_64-bit) R 28417 28417 2660 0 -1 0 15453 0 0 0 89825 93 0 0 25 0 1 0 1855238669 66183168 15097 4294967295 134512640 135094434 3221224432 3221223056 134557574 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/28421/statm): 16158 15097 145 145 0 16013 0 [pid=28421] vsize: 64632 Current children cumulated CPU time (s) 899.18 Current children cumulated vsize (Kb) 66756 [startup+910.078 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 28421 Raw data (/proc/28417/stat): 28417 (minisat+_script) S 28416 28417 2660 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855238664 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/28417/statm): 531 226 485 147 0 384 0 [pid=28417] vsize: 2124 Raw data (/proc/28421/stat): 28421 (minisat+_64-bit) R 28417 28417 2660 0 -1 0 15525 0 0 0 90824 93 0 0 25 0 1 0 1855238669 66473984 15169 4294967295 134512640 135094434 3221224432 3221223088 134558187 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/28421/statm): 16229 15169 145 145 0 16084 0 [pid=28421] vsize: 64916 Current children cumulated CPU time (s) 909.17 Current children cumulated vsize (Kb) 67040 [startup+920.078 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 28421 Raw data (/proc/28417/stat): 28417 (minisat+_script) S 28416 28417 2660 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855238664 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/28417/statm): 531 226 485 147 0 384 0 [pid=28417] vsize: 2124 Raw data (/proc/28421/stat): 28421 (minisat+_64-bit) R 28417 28417 2660 0 -1 0 15599 0 0 0 91823 94 0 0 25 0 1 0 1855238669 66772992 15243 4294967295 134512640 135094434 3221224432 3221223088 134558426 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/28421/statm): 16302 15243 145 145 0 16157 0 [pid=28421] vsize: 65208 Current children cumulated CPU time (s) 919.17 Current children cumulated vsize (Kb) 67332 [startup+930.079 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 28421 Raw data (/proc/28417/stat): 28417 (minisat+_script) S 28416 28417 2660 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855238664 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/28417/statm): 531 226 485 147 0 384 0 [pid=28417] vsize: 2124 Raw data (/proc/28421/stat): 28421 (minisat+_64-bit) R 28417 28417 2660 0 -1 0 15687 0 0 0 92822 95 0 0 25 0 1 0 1855238669 67129344 15331 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/28421/statm): 16389 15331 145 145 0 16244 0 [pid=28421] vsize: 65556 Current children cumulated CPU time (s) 929.17 Current children cumulated vsize (Kb) 67680 [startup+940.08 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 28421 Raw data (/proc/28417/stat): 28417 (minisat+_script) S 28416 28417 2660 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855238664 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/28417/statm): 531 226 485 147 0 384 0 [pid=28417] vsize: 2124 Raw data (/proc/28421/stat): 28421 (minisat+_64-bit) R 28417 28417 2660 0 -1 0 15731 0 0 0 93821 95 0 0 25 0 1 0 1855238669 67309568 15375 4294967295 134512640 135094434 3221224432 3221223120 134554731 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/28421/statm): 16433 15375 145 145 0 16288 0 [pid=28421] vsize: 65732 Current children cumulated CPU time (s) 939.16 Current children cumulated vsize (Kb) 67856 [startup+950.082 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 28421 Raw data (/proc/28417/stat): 28417 (minisat+_script) S 28416 28417 2660 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855238664 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/28417/statm): 531 226 485 147 0 384 0 [pid=28417] vsize: 2124 Raw data (/proc/28421/stat): 28421 (minisat+_64-bit) R 28417 28417 2660 0 -1 0 15731 0 0 0 94821 95 0 0 25 0 1 0 1855238669 67309568 15375 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/28421/statm): 16433 15375 145 145 0 16288 0 [pid=28421] vsize: 65732 Current children cumulated CPU time (s) 949.16 Current children cumulated vsize (Kb) 67856 [startup+960.082 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 28421 Raw data (/proc/28417/stat): 28417 (minisat+_script) S 28416 28417 2660 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855238664 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/28417/statm): 531 226 485 147 0 384 0 [pid=28417] vsize: 2124 Raw data (/proc/28421/stat): 28421 (minisat+_64-bit) R 28417 28417 2660 0 -1 0 15731 0 0 0 95822 95 0 0 25 0 1 0 1855238669 67309568 15375 4294967295 134512640 135094434 3221224432 3221221456 134676539 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/28421/statm): 16433 15375 145 145 0 16288 0 [pid=28421] vsize: 65732 Current children cumulated CPU time (s) 959.17 Current children cumulated vsize (Kb) 67856 [startup+970.083 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 28421 Raw data (/proc/28417/stat): 28417 (minisat+_script) S 28416 28417 2660 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855238664 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/28417/statm): 531 226 485 147 0 384 0 [pid=28417] vsize: 2124 Raw data (/proc/28421/stat): 28421 (minisat+_64-bit) R 28417 28417 2660 0 -1 0 15732 0 0 0 96822 95 0 0 25 0 1 0 1855238669 67309568 15376 4294967295 134512640 135094434 3221224432 3221223088 134558029 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/28421/statm): 16433 15376 145 145 0 16288 0 [pid=28421] vsize: 65732 Current children cumulated CPU time (s) 969.17 Current children cumulated vsize (Kb) 67856 [startup+980.084 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 28421 Raw data (/proc/28417/stat): 28417 (minisat+_script) S 28416 28417 2660 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855238664 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/28417/statm): 531 226 485 147 0 384 0 [pid=28417] vsize: 2124 Raw data (/proc/28421/stat): 28421 (minisat+_64-bit) R 28417 28417 2660 0 -1 0 15732 0 0 0 97822 96 0 0 25 0 1 0 1855238669 67309568 15376 4294967295 134512640 135094434 3221224432 3221223120 134554746 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/28421/statm): 16433 15376 145 145 0 16288 0 [pid=28421] vsize: 65732 Current children cumulated CPU time (s) 979.18 Current children cumulated vsize (Kb) 67856 [startup+990.085 s] Raw data (loadavg): 0.99 0.97 0.91 3/57 28421 Raw data (/proc/28417/stat): 28417 (minisat+_script) S 28416 28417 2660 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855238664 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/28417/statm): 531 226 485 147 0 384 0 [pid=28417] vsize: 2124 Raw data (/proc/28421/stat): 28421 (minisat+_64-bit) R 28417 28417 2660 0 -1 0 15732 0 0 0 98822 96 0 0 25 0 1 0 1855238669 67309568 15376 4294967295 134512640 135094434 3221224432 3221223120 134554705 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/28421/statm): 16433 15376 145 145 0 16288 0 [pid=28421] vsize: 65732 Current children cumulated CPU time (s) 989.18 Current children cumulated vsize (Kb) 67856 [startup+1000.09 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 28421 Raw data (/proc/28417/stat): 28417 (minisat+_script) S 28416 28417 2660 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855238664 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/28417/statm): 531 226 485 147 0 384 0 [pid=28417] vsize: 2124 Raw data (/proc/28421/stat): 28421 (minisat+_64-bit) R 28417 28417 2660 0 -1 0 15732 0 0 0 99822 96 0 0 25 0 1 0 1855238669 67309568 15376 4294967295 134512640 135094434 3221224432 3221223024 134556862 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/28421/statm): 16433 15376 145 145 0 16288 0 [pid=28421] vsize: 65732 Current children cumulated CPU time (s) 999.18 Current children cumulated vsize (Kb) 67856 [startup+1010.09 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 28421 Raw data (/proc/28417/stat): 28417 (minisat+_script) S 28416 28417 2660 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855238664 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/28417/statm): 531 226 485 147 0 384 0 [pid=28417] vsize: 2124 Raw data (/proc/28421/stat): 28421 (minisat+_64-bit) R 28417 28417 2660 0 -1 0 15732 0 0 0 100822 96 0 0 25 0 1 0 1855238669 67309568 15376 4294967295 134512640 135094434 3221224432 3221223084 134558255 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/28421/statm): 16433 15376 145 145 0 16288 0 [pid=28421] vsize: 65732 Current children cumulated CPU time (s) 1009.18 Current children cumulated vsize (Kb) 67856 [startup+1020.09 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 28421 Raw data (/proc/28417/stat): 28417 (minisat+_script) S 28416 28417 2660 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855238664 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/28417/statm): 531 226 485 147 0 384 0 [pid=28417] vsize: 2124 Raw data (/proc/28421/stat): 28421 (minisat+_64-bit) R 28417 28417 2660 0 -1 0 15732 0 0 0 101823 96 0 0 25 0 1 0 1855238669 67309568 15376 4294967295 134512640 135094434 3221224432 3221223072 134558264 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/28421/statm): 16433 15376 145 145 0 16288 0 [pid=28421] vsize: 65732 Current children cumulated CPU time (s) 1019.19 Current children cumulated vsize (Kb) 67856 [startup+1030.09 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 28421 Raw data (/proc/28417/stat): 28417 (minisat+_script) S 28416 28417 2660 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855238664 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/28417/statm): 531 226 485 147 0 384 0 [pid=28417] vsize: 2124 Raw data (/proc/28421/stat): 28421 (minisat+_64-bit) R 28417 28417 2660 0 -1 0 15732 0 0 0 102823 96 0 0 25 0 1 0 1855238669 67309568 15376 4294967295 134512640 135094434 3221224432 3221223088 134558213 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/28421/statm): 16433 15376 145 145 0 16288 0 [pid=28421] vsize: 65732 Current children cumulated CPU time (s) 1029.19 Current children cumulated vsize (Kb) 67856 [startup+1040.09 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 28421 Raw data (/proc/28417/stat): 28417 (minisat+_script) S 28416 28417 2660 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855238664 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/28417/statm): 531 226 485 147 0 384 0 [pid=28417] vsize: 2124 Raw data (/proc/28421/stat): 28421 (minisat+_64-bit) R 28417 28417 2660 0 -1 0 15732 0 0 0 103823 96 0 0 25 0 1 0 1855238669 67309568 15376 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/28421/statm): 16433 15376 145 145 0 16288 0 [pid=28421] vsize: 65732 Current children cumulated CPU time (s) 1039.19 Current children cumulated vsize (Kb) 67856 [startup+1050.09 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 28421 Raw data (/proc/28417/stat): 28417 (minisat+_script) S 28416 28417 2660 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855238664 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/28417/statm): 531 226 485 147 0 384 0 [pid=28417] vsize: 2124 Raw data (/proc/28421/stat): 28421 (minisat+_64-bit) R 28417 28417 2660 0 -1 0 15732 0 0 0 104823 96 0 0 25 0 1 0 1855238669 67309568 15376 4294967295 134512640 135094434 3221224432 3221223024 134557180 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/28421/statm): 16433 15376 145 145 0 16288 0 [pid=28421] vsize: 65732 Current children cumulated CPU time (s) 1049.19 Current children cumulated vsize (Kb) 67856 [startup+1060.09 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 28421 Raw data (/proc/28417/stat): 28417 (minisat+_script) S 28416 28417 2660 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855238664 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/28417/statm): 531 226 485 147 0 384 0 [pid=28417] vsize: 2124 Raw data (/proc/28421/stat): 28421 (minisat+_64-bit) R 28417 28417 2660 0 -1 0 15732 0 0 0 105823 96 0 0 25 0 1 0 1855238669 67309568 15376 4294967295 134512640 135094434 3221224432 3221223088 134557866 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/28421/statm): 16433 15376 145 145 0 16288 0 [pid=28421] vsize: 65732 Current children cumulated CPU time (s) 1059.19 Current children cumulated vsize (Kb) 67856 [startup+1070.09 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 28421 Raw data (/proc/28417/stat): 28417 (minisat+_script) S 28416 28417 2660 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855238664 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/28417/statm): 531 226 485 147 0 384 0 [pid=28417] vsize: 2124 Raw data (/proc/28421/stat): 28421 (minisat+_64-bit) R 28417 28417 2660 0 -1 0 15732 0 0 0 106823 96 0 0 25 0 1 0 1855238669 67309568 15376 4294967295 134512640 135094434 3221224432 3221223120 134554731 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/28421/statm): 16433 15376 145 145 0 16288 0 [pid=28421] vsize: 65732 Current children cumulated CPU time (s) 1069.19 Current children cumulated vsize (Kb) 67856 [startup+1080.09 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 28421 Raw data (/proc/28417/stat): 28417 (minisat+_script) S 28416 28417 2660 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855238664 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/28417/statm): 531 226 485 147 0 384 0 [pid=28417] vsize: 2124 Raw data (/proc/28421/stat): 28421 (minisat+_64-bit) R 28417 28417 2660 0 -1 0 15732 0 0 0 107824 96 0 0 25 0 1 0 1855238669 67309568 15376 4294967295 134512640 135094434 3221224432 3221223024 134557180 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/28421/statm): 16433 15376 145 145 0 16288 0 [pid=28421] vsize: 65732 Current children cumulated CPU time (s) 1079.2 Current children cumulated vsize (Kb) 67856 [startup+1090.09 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 28421 Raw data (/proc/28417/stat): 28417 (minisat+_script) S 28416 28417 2660 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855238664 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/28417/statm): 531 226 485 147 0 384 0 [pid=28417] vsize: 2124 Raw data (/proc/28421/stat): 28421 (minisat+_64-bit) R 28417 28417 2660 0 -1 0 15734 0 0 0 108824 96 0 0 25 0 1 0 1855238669 67309568 15378 4294967295 134512640 135094434 3221224432 3221221984 134677307 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/28421/statm): 16433 15378 145 145 0 16288 0 [pid=28421] vsize: 65732 Current children cumulated CPU time (s) 1089.2 Current children cumulated vsize (Kb) 67856 [startup+1100.1 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 28421 Raw data (/proc/28417/stat): 28417 (minisat+_script) S 28416 28417 2660 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855238664 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/28417/statm): 531 226 485 147 0 384 0 [pid=28417] vsize: 2124 Raw data (/proc/28421/stat): 28421 (minisat+_64-bit) R 28417 28417 2660 0 -1 0 15734 0 0 0 109824 96 0 0 25 0 1 0 1855238669 67309568 15378 4294967295 134512640 135094434 3221224432 3221222160 134677307 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/28421/statm): 16433 15378 145 145 0 16288 0 [pid=28421] vsize: 65732 Current children cumulated CPU time (s) 1099.2 Current children cumulated vsize (Kb) 67856 [startup+1110.1 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 28421 Raw data (/proc/28417/stat): 28417 (minisat+_script) S 28416 28417 2660 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855238664 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/28417/statm): 531 226 485 147 0 384 0 [pid=28417] vsize: 2124 Raw data (/proc/28421/stat): 28421 (minisat+_64-bit) R 28417 28417 2660 0 -1 0 15734 0 0 0 110824 97 0 0 25 0 1 0 1855238669 67309568 15378 4294967295 134512640 135094434 3221224432 3221223120 134554746 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/28421/statm): 16433 15378 145 145 0 16288 0 [pid=28421] vsize: 65732 Current children cumulated CPU time (s) 1109.21 Current children cumulated vsize (Kb) 67856 [startup+1120.1 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 28421 Raw data (/proc/28417/stat): 28417 (minisat+_script) S 28416 28417 2660 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855238664 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/28417/statm): 531 226 485 147 0 384 0 [pid=28417] vsize: 2124 Raw data (/proc/28421/stat): 28421 (minisat+_64-bit) R 28417 28417 2660 0 -1 0 15734 0 0 0 111824 97 0 0 25 0 1 0 1855238669 67309568 15378 4294967295 134512640 135094434 3221224432 3221221876 134677085 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/28421/statm): 16433 15378 145 145 0 16288 0 [pid=28421] vsize: 65732 Current children cumulated CPU time (s) 1119.21 Current children cumulated vsize (Kb) 67856 [startup+1130.1 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 28421 Raw data (/proc/28417/stat): 28417 (minisat+_script) S 28416 28417 2660 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855238664 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/28417/statm): 531 226 485 147 0 384 0 [pid=28417] vsize: 2124 Raw data (/proc/28421/stat): 28421 (minisat+_64-bit) R 28417 28417 2660 0 -1 0 15734 0 0 0 112824 97 0 0 25 0 1 0 1855238669 67309568 15378 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/28421/statm): 16433 15378 145 145 0 16288 0 [pid=28421] vsize: 65732 Current children cumulated CPU time (s) 1129.21 Current children cumulated vsize (Kb) 67856 [startup+1140.1 s] Raw data (loadavg): 0.99 0.97 0.91 3/57 28421 Raw data (/proc/28417/stat): 28417 (minisat+_script) S 28416 28417 2660 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855238664 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/28417/statm): 531 226 485 147 0 384 0 [pid=28417] vsize: 2124 Raw data (/proc/28421/stat): 28421 (minisat+_64-bit) R 28417 28417 2660 0 -1 0 15734 0 0 0 113824 97 0 0 25 0 1 0 1855238669 67309568 15378 4294967295 134512640 135094434 3221224432 3221223088 134558162 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/28421/statm): 16433 15378 145 145 0 16288 0 [pid=28421] vsize: 65732 Current children cumulated CPU time (s) 1139.21 Current children cumulated vsize (Kb) 67856 [startup+1150.1 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 28421 Raw data (/proc/28417/stat): 28417 (minisat+_script) S 28416 28417 2660 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855238664 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/28417/statm): 531 226 485 147 0 384 0 [pid=28417] vsize: 2124 Raw data (/proc/28421/stat): 28421 (minisat+_64-bit) R 28417 28417 2660 0 -1 0 15734 0 0 0 114825 97 0 0 25 0 1 0 1855238669 67309568 15378 4294967295 134512640 135094434 3221224432 3221223088 134557846 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/28421/statm): 16433 15378 145 145 0 16288 0 [pid=28421] vsize: 65732 Current children cumulated CPU time (s) 1149.22 Current children cumulated vsize (Kb) 67856 [startup+1160.1 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 28421 Raw data (/proc/28417/stat): 28417 (minisat+_script) S 28416 28417 2660 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855238664 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/28417/statm): 531 226 485 147 0 384 0 [pid=28417] vsize: 2124 Raw data (/proc/28421/stat): 28421 (minisat+_64-bit) R 28417 28417 2660 0 -1 0 15735 0 0 0 115825 97 0 0 25 0 1 0 1855238669 67309568 15379 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/28421/statm): 16433 15379 145 145 0 16288 0 [pid=28421] vsize: 65732 Current children cumulated CPU time (s) 1159.22 Current children cumulated vsize (Kb) 67856 [startup+1170.1 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 28421 Raw data (/proc/28417/stat): 28417 (minisat+_script) S 28416 28417 2660 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855238664 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/28417/statm): 531 226 485 147 0 384 0 [pid=28417] vsize: 2124 Raw data (/proc/28421/stat): 28421 (minisat+_64-bit) R 28417 28417 2660 0 -1 0 15735 0 0 0 116825 97 0 0 25 0 1 0 1855238669 67309568 15379 4294967295 134512640 135094434 3221224432 3221223024 134557366 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/28421/statm): 16433 15379 145 145 0 16288 0 [pid=28421] vsize: 65732 Current children cumulated CPU time (s) 1169.22 Current children cumulated vsize (Kb) 67856 [startup+1180.1 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 28421 Raw data (/proc/28417/stat): 28417 (minisat+_script) S 28416 28417 2660 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855238664 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/28417/statm): 531 226 485 147 0 384 0 [pid=28417] vsize: 2124 Raw data (/proc/28421/stat): 28421 (minisat+_64-bit) R 28417 28417 2660 0 -1 0 15735 0 0 0 117825 97 0 0 25 0 1 0 1855238669 67309568 15379 4294967295 134512640 135094434 3221224432 3221223056 134562125 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/28421/statm): 16433 15379 145 145 0 16288 0 [pid=28421] vsize: 65732 Current children cumulated CPU time (s) 1179.22 Current children cumulated vsize (Kb) 67856 [startup+1190.1 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 28421 Raw data (/proc/28417/stat): 28417 (minisat+_script) S 28416 28417 2660 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855238664 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/28417/statm): 531 226 485 147 0 384 0 [pid=28417] vsize: 2124 Raw data (/proc/28421/stat): 28421 (minisat+_64-bit) R 28417 28417 2660 0 -1 0 15735 0 0 0 118825 97 0 0 25 0 1 0 1855238669 67309568 15379 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/28421/statm): 16433 15379 145 145 0 16288 0 [pid=28421] vsize: 65732 Current children cumulated CPU time (s) 1189.22 Current children cumulated vsize (Kb) 67856 [startup+1200.1 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 28421 Raw data (/proc/28417/stat): 28417 (minisat+_script) S 28416 28417 2660 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855238664 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/28417/statm): 531 226 485 147 0 384 0 [pid=28417] vsize: 2124 Raw data (/proc/28421/stat): 28421 (minisat+_64-bit) R 28417 28417 2660 0 -1 0 15735 0 0 0 119825 97 0 0 25 0 1 0 1855238669 67309568 15379 4294967295 134512640 135094434 3221224432 3221223024 134556993 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/28421/statm): 16433 15379 145 145 0 16288 0 [pid=28421] vsize: 65732 Current children cumulated CPU time (s) 1199.22 Current children cumulated vsize (Kb) 67856 [startup+1210.11 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 28421 Raw data (/proc/28417/stat): 28417 (minisat+_script) S 28416 28417 2660 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855238664 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/28417/statm): 531 226 485 147 0 384 0 [pid=28417] vsize: 2124 Raw data (/proc/28421/stat): 28421 (minisat+_64-bit) R 28417 28417 2660 0 -1 0 15735 0 0 0 120826 97 0 0 25 0 1 0 1855238669 67309568 15379 4294967295 134512640 135094434 3221224432 3221223088 134558178 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/28421/statm): 16433 15379 145 145 0 16288 0 [pid=28421] vsize: 65732 Current children cumulated CPU time (s) 1209.23 Current children cumulated vsize (Kb) 67856 Maximum CPU time exceeded: sending SIGTERM then SIGKILL [startup+1210.11 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 28421 Raw data (/proc/28417/stat): 28417 (minisat+_script) S 28416 28417 2660 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855238664 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/28417/statm): 531 226 485 147 0 384 0 [pid=28417] vsize: 2124 Raw data (/proc/28421/stat): 28421 (minisat+_64-bit) R 28417 28417 2660 0 -1 0 15735 0 0 0 120826 97 0 0 25 0 1 0 1855238669 67309568 15379 4294967295 134512640 135094434 3221224432 3221223088 134558249 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/28421/statm): 16433 15379 145 145 0 16288 0 [pid=28421] vsize: 65732 Current children cumulated CPU time (s) 1209.23 Current children cumulated vsize (Kb) 67856 Sending SIGTERM to -28417 Sleeping 2 seconds One traced child (pid=28417) ended because it received signal 15 (SIGTERM) One traced child (pid=28421) exited with status: 10 All traced children have exited ! Game is over. Child status: 10 Real time (s): 1210.14 CPU time (s): 1209.27 CPU user time (s): 1208.26 CPU system time (s): 1.00585 CPU usage (%): 99.928 Max. virtual memory (cumulated for all children) (Kb): 67856
ERROR: no interpretation found !