Name | mps-v2-20-10/MIPLIB/miplib/normalized-mps-v2-20-10-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.7373 |
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 wulflinc31 THE 2005-09-19 03:19:47 (client local time) PB2005-SCRIPT v4.0 MARKUPS: idlaunch=2875 boxname=wulflinc31 idbench=531 idsolver=3 numberseed=0 MD5SUM SOLVER: MD5SUM BENCH: a733e9fa1e4e3ac90baf85249f7c3e9a /oldhome/oroussel/tmp/wulflinc31/normalized-mps-v2-20-10-p0282.opb REAL COMMAND: minisat+_script /oldhome/oroussel/tmp/wulflinc31/normalized-mps-v2-20-10-p0282.opb IDLAUNCH: 2875 /proc/cpuinfo: processor : 0 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 3 cpu MHz : 451.153 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.153 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: 675080 kB Buffers: 36940 kB Cached: 292116 kB SwapCached: 1016 kB Active: 107784 kB Inactive: 224036 kB HighTotal: 131008 kB HighFree: 252 kB LowTotal: 903652 kB LowFree: 674828 kB SwapTotal: 2097892 kB SwapFree: 2096404 kB Dirty: 28 kB Writeback: 0 kB Mapped: 5772 kB Slab: 22068 kB Committed_AS: 64340 kB PageTables: 340 kB VmallocTotal: 114680 kB VmallocUsed: 1368 kB VmallocChunk: 113252 kB JOB ENDED THE 2005-09-19 03:39:57 (client local time) WITH STATUS 10 IN 1209.28 SECONDS stats: 2875 7 1209.28 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 % |
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/22672/stat): 22672 (minisat+_script) R 22671 22672 9102 0 -1 0 19 0 0 0 0 0 0 0 23 0 1 0 1846564936 712704 3 4294967295 134512640 135087896 3221224496 3221224496 1073744960 0 0 5 0 0 0 0 17 0 0 0 Raw data (/proc/22672/statm): 174 3 169 147 0 27 0 [pid=22672] 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=22673 New process pid=22674 New process pid=22675 execve syscall for /bin/sed executable One traced child (pid=22674) exited with status: 0 open syscall for file /etc/ld.so.preload open syscall for file tls/i686/mmx/libc.so.6 open syscall for file tls/i686/libc.so.6 open syscall for file tls/mmx/libc.so.6 open syscall for file tls/libc.so.6 open syscall for file i686/mmx/libc.so.6 open syscall for file i686/libc.so.6 open syscall for file mmx/libc.so.6 open syscall for file libc.so.6 open syscall for file /oldhome/oroussel/lib/tls/i686/mmx/libc.so.6 open syscall for file /oldhome/oroussel/lib/tls/i686/libc.so.6 open syscall for file /oldhome/oroussel/lib/tls/mmx/libc.so.6 open syscall for file /oldhome/oroussel/lib/tls/libc.so.6 open syscall for file /oldhome/oroussel/lib/i686/mmx/libc.so.6 open syscall for file /oldhome/oroussel/lib/i686/libc.so.6 open syscall for file /oldhome/oroussel/lib/mmx/libc.so.6 open syscall for file /oldhome/oroussel/lib/libc.so.6 open syscall for file /etc/ld.so.cache open syscall for file /lib/tls/libc.so.6 One traced child (pid=22675) exited with status: 0 One traced child (pid=22673) exited with status: 0 New process pid=22676 execve syscall for /oldhome/oroussel/solvers/minisat+_64-bit_static executable open syscall for file /dev/null open syscall for file /oldhome/oroussel/tmp/wulflinc31/normalized-mps-v2-20-10-p0282.opb [startup+10.0032 s] Raw data (loadavg): 0.91 0.98 0.99 2/58 22676 Raw data (/proc/22672/stat): 22672 (minisat+_script) S 22671 22672 9102 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846564936 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/22672/statm): 531 226 485 147 0 384 0 [pid=22672] vsize: 2124 Raw data (/proc/22676/stat): 22676 (minisat+_64-bit) R 22672 22672 9102 0 -1 0 8650 0 0 0 931 32 0 0 25 0 1 0 1846564941 38129664 8294 4294967295 134512640 135094434 3221224432 3221222160 134600228 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/22676/statm): 9309 8294 145 145 0 9164 0 [pid=22676] vsize: 37236 Current children cumulated CPU time (s) 9.64 Current children cumulated vsize (Kb) 39360 [startup+20.0052 s] Raw data (loadavg): 0.93 0.98 0.99 2/58 22676 Raw data (/proc/22672/stat): 22672 (minisat+_script) S 22671 22672 9102 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846564936 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/22672/statm): 531 226 485 147 0 384 0 [pid=22672] vsize: 2124 Raw data (/proc/22676/stat): 22676 (minisat+_64-bit) R 22672 22672 9102 0 -1 0 8721 0 0 0 1930 33 0 0 25 0 1 0 1846564941 38391808 8365 4294967295 134512640 135094434 3221224432 3221223044 134563121 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/22676/statm): 9373 8365 145 145 0 9228 0 [pid=22676] vsize: 37492 Current children cumulated CPU time (s) 19.64 Current children cumulated vsize (Kb) 39616 [startup+30.0061 s] Raw data (loadavg): 0.94 0.98 0.99 2/58 22676 Raw data (/proc/22672/stat): 22672 (minisat+_script) S 22671 22672 9102 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846564936 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/22672/statm): 531 226 485 147 0 384 0 [pid=22672] vsize: 2124 Raw data (/proc/22676/stat): 22676 (minisat+_64-bit) R 22672 22672 9102 0 -1 0 8795 0 0 0 2928 35 0 0 25 0 1 0 1846564941 38682624 8439 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/22676/statm): 9444 8439 145 145 0 9299 0 [pid=22676] vsize: 37776 Current children cumulated CPU time (s) 29.64 Current children cumulated vsize (Kb) 39900 [startup+40.0071 s] Raw data (loadavg): 0.95 0.98 0.99 2/58 22678 Raw data (/proc/22672/stat): 22672 (minisat+_script) S 22671 22672 9102 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846564936 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/22672/statm): 531 226 485 147 0 384 0 [pid=22672] vsize: 2124 Raw data (/proc/22676/stat): 22676 (minisat+_64-bit) R 22672 22672 9102 0 -1 0 8850 0 0 0 3927 36 0 0 25 0 1 0 1846564941 38903808 8494 4294967295 134512640 135094434 3221224432 3221223120 134554746 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/22676/statm): 9498 8494 145 145 0 9353 0 [pid=22676] vsize: 37992 Current children cumulated CPU time (s) 39.64 Current children cumulated vsize (Kb) 40116 [startup+50.009 s] Raw data (loadavg): 0.95 0.98 0.99 2/58 22678 Raw data (/proc/22672/stat): 22672 (minisat+_script) S 22671 22672 9102 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846564936 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/22672/statm): 531 226 485 147 0 384 0 [pid=22672] vsize: 2124 Raw data (/proc/22676/stat): 22676 (minisat+_64-bit) R 22672 22672 9102 0 -1 0 8932 0 0 0 4925 37 0 0 25 0 1 0 1846564941 39260160 8576 4294967295 134512640 135094434 3221224432 3221223120 134554746 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/22676/statm): 9585 8576 145 145 0 9440 0 [pid=22676] vsize: 38340 Current children cumulated CPU time (s) 49.63 Current children cumulated vsize (Kb) 40464 [startup+60.0099 s] Raw data (loadavg): 0.96 0.98 0.99 2/58 22678 Raw data (/proc/22672/stat): 22672 (minisat+_script) S 22671 22672 9102 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846564936 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/22672/statm): 531 226 485 147 0 384 0 [pid=22672] vsize: 2124 Raw data (/proc/22676/stat): 22676 (minisat+_64-bit) R 22672 22672 9102 0 -1 0 8975 0 0 0 5924 37 0 0 25 0 1 0 1846564941 39428096 8619 4294967295 134512640 135094434 3221224432 3221223104 134556317 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/22676/statm): 9626 8619 145 145 0 9481 0 [pid=22676] vsize: 38504 Current children cumulated CPU time (s) 59.62 Current children cumulated vsize (Kb) 40628 [startup+70.0119 s] Raw data (loadavg): 0.97 0.98 0.99 2/58 22678 Raw data (/proc/22672/stat): 22672 (minisat+_script) S 22671 22672 9102 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846564936 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/22672/statm): 531 226 485 147 0 384 0 [pid=22672] vsize: 2124 Raw data (/proc/22676/stat): 22676 (minisat+_64-bit) R 22672 22672 9102 0 -1 0 9060 0 0 0 6922 39 0 0 25 0 1 0 1846564941 39772160 8704 4294967295 134512640 135094434 3221224432 3221223056 134557574 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/22676/statm): 9710 8704 145 145 0 9565 0 [pid=22676] vsize: 38840 Current children cumulated CPU time (s) 69.62 Current children cumulated vsize (Kb) 40964 [startup+80.0128 s] Raw data (loadavg): 0.97 0.98 0.99 2/58 22678 Raw data (/proc/22672/stat): 22672 (minisat+_script) S 22671 22672 9102 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846564936 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/22672/statm): 531 226 485 147 0 384 0 [pid=22672] vsize: 2124 Raw data (/proc/22676/stat): 22676 (minisat+_64-bit) R 22672 22672 9102 0 -1 0 9193 0 0 0 7920 40 0 0 25 0 1 0 1846564941 40304640 8837 4294967295 134512640 135094434 3221224432 3221223120 134554746 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/22676/statm): 9840 8837 145 145 0 9695 0 [pid=22676] vsize: 39360 Current children cumulated CPU time (s) 79.61 Current children cumulated vsize (Kb) 41484 [startup+90.0148 s] Raw data (loadavg): 0.98 0.98 0.99 2/58 22678 Raw data (/proc/22672/stat): 22672 (minisat+_script) S 22671 22672 9102 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846564936 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/22672/statm): 531 226 485 147 0 384 0 [pid=22672] vsize: 2124 Raw data (/proc/22676/stat): 22676 (minisat+_64-bit) R 22672 22672 9102 0 -1 0 9257 0 0 0 8918 41 0 0 25 0 1 0 1846564941 40566784 8901 4294967295 134512640 135094434 3221224432 3221223088 134557875 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/22676/statm): 9904 8901 145 145 0 9759 0 [pid=22676] vsize: 39616 Current children cumulated CPU time (s) 89.6 Current children cumulated vsize (Kb) 41740 [startup+100.016 s] Raw data (loadavg): 0.98 0.98 0.99 2/58 22680 Raw data (/proc/22672/stat): 22672 (minisat+_script) S 22671 22672 9102 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846564936 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/22672/statm): 531 226 485 147 0 384 0 [pid=22672] vsize: 2124 Raw data (/proc/22676/stat): 22676 (minisat+_64-bit) R 22672 22672 9102 0 -1 0 9319 0 0 0 9917 42 0 0 25 0 1 0 1846564941 40808448 8963 4294967295 134512640 135094434 3221224432 3221222992 134550329 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/22676/statm): 9963 8963 145 145 0 9818 0 [pid=22676] vsize: 39852 Current children cumulated CPU time (s) 99.6 Current children cumulated vsize (Kb) 41976 [startup+110.017 s] Raw data (loadavg): 0.98 0.98 0.99 2/58 22680 Raw data (/proc/22672/stat): 22672 (minisat+_script) S 22671 22672 9102 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846564936 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/22672/statm): 531 226 485 147 0 384 0 [pid=22672] vsize: 2124 Raw data (/proc/22676/stat): 22676 (minisat+_64-bit) R 22672 22672 9102 0 -1 0 9371 0 0 0 10916 42 0 0 25 0 1 0 1846564941 41070592 9015 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/22676/statm): 10027 9015 145 145 0 9882 0 [pid=22676] vsize: 40108 Current children cumulated CPU time (s) 109.59 Current children cumulated vsize (Kb) 42232 [startup+120.019 s] Raw data (loadavg): 0.98 0.98 0.99 2/58 22680 Raw data (/proc/22672/stat): 22672 (minisat+_script) S 22671 22672 9102 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846564936 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/22672/statm): 531 226 485 147 0 384 0 [pid=22672] vsize: 2124 Raw data (/proc/22676/stat): 22676 (minisat+_64-bit) R 22672 22672 9102 0 -1 0 9451 0 0 0 11914 44 0 0 25 0 1 0 1846564941 41385984 9095 4294967295 134512640 135094434 3221224432 3221223120 134554723 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/22676/statm): 10104 9095 145 145 0 9959 0 [pid=22676] vsize: 40416 Current children cumulated CPU time (s) 119.59 Current children cumulated vsize (Kb) 42540 [startup+130.019 s] Raw data (loadavg): 0.99 0.98 0.99 2/58 22680 Raw data (/proc/22672/stat): 22672 (minisat+_script) S 22671 22672 9102 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846564936 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/22672/statm): 531 226 485 147 0 384 0 [pid=22672] vsize: 2124 Raw data (/proc/22676/stat): 22676 (minisat+_64-bit) R 22672 22672 9102 0 -1 0 9537 0 0 0 12912 45 0 0 25 0 1 0 1846564941 41734144 9181 4294967295 134512640 135094434 3221224432 3221223104 134555811 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/22676/statm): 10189 9181 145 145 0 10044 0 [pid=22676] vsize: 40756 Current children cumulated CPU time (s) 129.58 Current children cumulated vsize (Kb) 42880 [startup+140.02 s] Raw data (loadavg): 0.99 0.98 0.99 2/58 22680 Raw data (/proc/22672/stat): 22672 (minisat+_script) S 22671 22672 9102 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846564936 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/22672/statm): 531 226 485 147 0 384 0 [pid=22672] vsize: 2124 Raw data (/proc/22676/stat): 22676 (minisat+_64-bit) R 22672 22672 9102 0 -1 0 9614 0 0 0 13911 45 0 0 25 0 1 0 1846564941 42049536 9258 4294967295 134512640 135094434 3221224432 3221222212 134676464 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/22676/statm): 10266 9258 145 145 0 10121 0 [pid=22676] vsize: 41064 Current children cumulated CPU time (s) 139.57 Current children cumulated vsize (Kb) 43188 [startup+150.021 s] Raw data (loadavg): 0.99 0.98 0.99 2/58 22680 Raw data (/proc/22672/stat): 22672 (minisat+_script) S 22671 22672 9102 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846564936 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/22672/statm): 531 226 485 147 0 384 0 [pid=22672] vsize: 2124 Raw data (/proc/22676/stat): 22676 (minisat+_64-bit) R 22672 22672 9102 0 -1 0 9651 0 0 0 14911 45 0 0 25 0 1 0 1846564941 42172416 9295 4294967295 134512640 135094434 3221224432 3221223088 134557884 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/22676/statm): 10296 9295 145 145 0 10151 0 [pid=22676] vsize: 41184 Current children cumulated CPU time (s) 149.57 Current children cumulated vsize (Kb) 43308 [startup+160.021 s] Raw data (loadavg): 0.99 0.98 0.99 2/58 22682 Raw data (/proc/22672/stat): 22672 (minisat+_script) S 22671 22672 9102 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846564936 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/22672/statm): 531 226 485 147 0 384 0 [pid=22672] vsize: 2124 Raw data (/proc/22676/stat): 22676 (minisat+_64-bit) R 22672 22672 9102 0 -1 0 9751 0 0 0 15909 47 0 0 25 0 1 0 1846564941 42561536 9395 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/22676/statm): 10391 9395 145 145 0 10246 0 [pid=22676] vsize: 41564 Current children cumulated CPU time (s) 159.57 Current children cumulated vsize (Kb) 43688 [startup+170.023 s] Raw data (loadavg): 0.99 0.98 0.99 2/58 22682 Raw data (/proc/22672/stat): 22672 (minisat+_script) S 22671 22672 9102 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846564936 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/22672/statm): 531 226 485 147 0 384 0 [pid=22672] vsize: 2124 Raw data (/proc/22676/stat): 22676 (minisat+_64-bit) R 22672 22672 9102 0 -1 0 9880 0 0 0 16907 48 0 0 25 0 1 0 1846564941 43085824 9524 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/22676/statm): 10519 9524 145 145 0 10374 0 [pid=22676] vsize: 42076 Current children cumulated CPU time (s) 169.56 Current children cumulated vsize (Kb) 44200 [startup+180.024 s] Raw data (loadavg): 0.99 0.98 0.99 2/58 22682 Raw data (/proc/22672/stat): 22672 (minisat+_script) S 22671 22672 9102 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846564936 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/22672/statm): 531 226 485 147 0 384 0 [pid=22672] vsize: 2124 Raw data (/proc/22676/stat): 22676 (minisat+_64-bit) R 22672 22672 9102 0 -1 0 9954 0 0 0 17906 48 0 0 25 0 1 0 1846564941 43384832 9598 4294967295 134512640 135094434 3221224432 3221223120 134554746 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/22676/statm): 10592 9598 145 145 0 10447 0 [pid=22676] vsize: 42368 Current children cumulated CPU time (s) 179.55 Current children cumulated vsize (Kb) 44492 [startup+190.026 s] Raw data (loadavg): 0.99 0.98 0.99 2/58 22682 Raw data (/proc/22672/stat): 22672 (minisat+_script) S 22671 22672 9102 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846564936 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/22672/statm): 531 226 485 147 0 384 0 [pid=22672] vsize: 2124 Raw data (/proc/22676/stat): 22676 (minisat+_64-bit) R 22672 22672 9102 0 -1 0 10080 0 0 0 18904 49 0 0 25 0 1 0 1846564941 43888640 9724 4294967295 134512640 135094434 3221224432 3221221312 134519159 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/22676/statm): 10715 9724 145 145 0 10570 0 [pid=22676] vsize: 42860 Current children cumulated CPU time (s) 189.54 Current children cumulated vsize (Kb) 44984 [startup+200.027 s] Raw data (loadavg): 0.99 0.98 0.99 2/58 22682 Raw data (/proc/22672/stat): 22672 (minisat+_script) S 22671 22672 9102 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846564936 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/22672/statm): 531 226 485 147 0 384 0 [pid=22672] vsize: 2124 Raw data (/proc/22676/stat): 22676 (minisat+_64-bit) R 22672 22672 9102 0 -1 0 10149 0 0 0 19903 50 0 0 25 0 1 0 1846564941 44298240 9793 4294967295 134512640 135094434 3221224432 3221223088 134558235 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/22676/statm): 10815 9793 145 145 0 10670 0 [pid=22676] vsize: 43260 Current children cumulated CPU time (s) 199.54 Current children cumulated vsize (Kb) 45384 [startup+210.028 s] Raw data (loadavg): 0.99 0.98 0.99 2/58 22682 Raw data (/proc/22672/stat): 22672 (minisat+_script) S 22671 22672 9102 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846564936 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/22672/statm): 531 226 485 147 0 384 0 [pid=22672] vsize: 2124 Raw data (/proc/22676/stat): 22676 (minisat+_64-bit) R 22672 22672 9102 0 -1 0 10213 0 0 0 20902 50 0 0 25 0 1 0 1846564941 44556288 9857 4294967295 134512640 135094434 3221224432 3221223088 134558208 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/22676/statm): 10878 9857 145 145 0 10733 0 [pid=22676] vsize: 43512 Current children cumulated CPU time (s) 209.53 Current children cumulated vsize (Kb) 45636 [startup+220.029 s] Raw data (loadavg): 0.99 0.98 0.99 2/58 22684 Raw data (/proc/22672/stat): 22672 (minisat+_script) S 22671 22672 9102 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846564936 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/22672/statm): 531 226 485 147 0 384 0 [pid=22672] vsize: 2124 Raw data (/proc/22676/stat): 22676 (minisat+_64-bit) R 22672 22672 9102 0 -1 0 10290 0 0 0 21901 51 0 0 25 0 1 0 1846564941 44879872 9934 4294967295 134512640 135094434 3221224432 3221223104 134555945 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/22676/statm): 10957 9934 145 145 0 10812 0 [pid=22676] vsize: 43828 Current children cumulated CPU time (s) 219.53 Current children cumulated vsize (Kb) 45952 [startup+230.03 s] Raw data (loadavg): 0.99 0.98 0.99 2/58 22684 Raw data (/proc/22672/stat): 22672 (minisat+_script) S 22671 22672 9102 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846564936 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/22672/statm): 531 226 485 147 0 384 0 [pid=22672] vsize: 2124 Raw data (/proc/22676/stat): 22676 (minisat+_64-bit) R 22672 22672 9102 0 -1 0 10365 0 0 0 22901 51 0 0 25 0 1 0 1846564941 45277184 10009 4294967295 134512640 135094434 3221224432 3221223068 134557560 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/22676/statm): 11054 10009 145 145 0 10909 0 [pid=22676] vsize: 44216 Current children cumulated CPU time (s) 229.53 Current children cumulated vsize (Kb) 46340 [startup+240.031 s] Raw data (loadavg): 0.99 0.98 0.99 2/58 22684 Raw data (/proc/22672/stat): 22672 (minisat+_script) S 22671 22672 9102 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846564936 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/22672/statm): 531 226 485 147 0 384 0 [pid=22672] vsize: 2124 Raw data (/proc/22676/stat): 22676 (minisat+_64-bit) T 22672 22672 9102 0 -1 0 10406 0 0 0 23900 51 0 0 25 0 1 0 1846564941 45441024 10050 4294967295 134512640 135094434 3221224432 3221222812 134870330 0 0 5 16386 3222434794 0 0 17 1 0 0 Raw data (/proc/22676/statm): 11094 10050 145 145 0 10949 0 [pid=22676] vsize: 44376 Current children cumulated CPU time (s) 239.52 Current children cumulated vsize (Kb) 46500 [startup+250.032 s] Raw data (loadavg): 0.99 0.98 0.99 2/58 22684 Raw data (/proc/22672/stat): 22672 (minisat+_script) S 22671 22672 9102 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846564936 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/22672/statm): 531 226 485 147 0 384 0 [pid=22672] vsize: 2124 Raw data (/proc/22676/stat): 22676 (minisat+_64-bit) R 22672 22672 9102 0 -1 0 10470 0 0 0 24899 52 0 0 25 0 1 0 1846564941 45699072 10114 4294967295 134512640 135094434 3221224432 3221223120 134554723 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/22676/statm): 11157 10114 145 145 0 11012 0 [pid=22676] vsize: 44628 Current children cumulated CPU time (s) 249.52 Current children cumulated vsize (Kb) 46752 [startup+260.032 s] Raw data (loadavg): 0.99 0.98 0.99 2/58 22684 Raw data (/proc/22672/stat): 22672 (minisat+_script) S 22671 22672 9102 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846564936 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/22672/statm): 531 226 485 147 0 384 0 [pid=22672] vsize: 2124 Raw data (/proc/22676/stat): 22676 (minisat+_64-bit) R 22672 22672 9102 0 -1 0 10566 0 0 0 25897 53 0 0 25 0 1 0 1846564941 46092288 10210 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/22676/statm): 11253 10210 145 145 0 11108 0 [pid=22676] vsize: 45012 Current children cumulated CPU time (s) 259.51 Current children cumulated vsize (Kb) 47136 [startup+270.033 s] Raw data (loadavg): 0.99 0.98 0.99 2/58 22684 Raw data (/proc/22672/stat): 22672 (minisat+_script) S 22671 22672 9102 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846564936 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/22672/statm): 531 226 485 147 0 384 0 [pid=22672] vsize: 2124 Raw data (/proc/22676/stat): 22676 (minisat+_64-bit) R 22672 22672 9102 0 -1 0 10685 0 0 0 26895 53 0 0 25 0 1 0 1846564941 46567424 10329 4294967295 134512640 135094434 3221224432 3221223088 134558249 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/22676/statm): 11369 10329 145 145 0 11224 0 [pid=22676] vsize: 45476 Current children cumulated CPU time (s) 269.49 Current children cumulated vsize (Kb) 47600 [startup+280.034 s] Raw data (loadavg): 0.99 0.98 0.99 2/58 22686 Raw data (/proc/22672/stat): 22672 (minisat+_script) S 22671 22672 9102 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846564936 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/22672/statm): 531 226 485 147 0 384 0 [pid=22672] vsize: 2124 Raw data (/proc/22676/stat): 22676 (minisat+_64-bit) R 22672 22672 9102 0 -1 0 10760 0 0 0 27893 54 0 0 25 0 1 0 1846564941 46870528 10404 4294967295 134512640 135094434 3221224432 3221223120 134554731 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/22676/statm): 11443 10404 145 145 0 11298 0 [pid=22676] vsize: 45772 Current children cumulated CPU time (s) 279.48 Current children cumulated vsize (Kb) 47896 [startup+290.035 s] Raw data (loadavg): 0.99 0.98 0.99 2/58 22686 Raw data (/proc/22672/stat): 22672 (minisat+_script) S 22671 22672 9102 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846564936 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/22672/statm): 531 226 485 147 0 384 0 [pid=22672] vsize: 2124 Raw data (/proc/22676/stat): 22676 (minisat+_64-bit) R 22672 22672 9102 0 -1 0 10851 0 0 0 28893 55 0 0 25 0 1 0 1846564941 47243264 10495 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/22676/statm): 11534 10495 145 145 0 11389 0 [pid=22676] vsize: 46136 Current children cumulated CPU time (s) 289.49 Current children cumulated vsize (Kb) 48260 [startup+300.036 s] Raw data (loadavg): 0.99 0.98 0.99 2/58 22686 Raw data (/proc/22672/stat): 22672 (minisat+_script) S 22671 22672 9102 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846564936 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/22672/statm): 531 226 485 147 0 384 0 [pid=22672] vsize: 2124 Raw data (/proc/22676/stat): 22676 (minisat+_64-bit) R 22672 22672 9102 0 -1 0 10934 0 0 0 29892 55 0 0 25 0 1 0 1846564941 47579136 10578 4294967295 134512640 135094434 3221224432 3221223088 134558004 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/22676/statm): 11616 10578 145 145 0 11471 0 [pid=22676] vsize: 46464 Current children cumulated CPU time (s) 299.48 Current children cumulated vsize (Kb) 48588 [startup+310.037 s] Raw data (loadavg): 0.99 0.98 0.99 2/58 22686 Raw data (/proc/22672/stat): 22672 (minisat+_script) S 22671 22672 9102 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846564936 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/22672/statm): 531 226 485 147 0 384 0 [pid=22672] vsize: 2124 Raw data (/proc/22676/stat): 22676 (minisat+_64-bit) R 22672 22672 9102 0 -1 0 11015 0 0 0 30891 56 0 0 25 0 1 0 1846564941 47906816 10659 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/22676/statm): 11696 10659 145 145 0 11551 0 [pid=22676] vsize: 46784 Current children cumulated CPU time (s) 309.48 Current children cumulated vsize (Kb) 48908 [startup+320.038 s] Raw data (loadavg): 0.99 0.98 0.99 2/58 22686 Raw data (/proc/22672/stat): 22672 (minisat+_script) S 22671 22672 9102 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846564936 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/22672/statm): 531 226 485 147 0 384 0 [pid=22672] vsize: 2124 Raw data (/proc/22676/stat): 22676 (minisat+_64-bit) R 22672 22672 9102 0 -1 0 11129 0 0 0 31888 57 0 0 25 0 1 0 1846564941 48369664 10773 4294967295 134512640 135094434 3221224432 3221223056 134557612 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/22676/statm): 11809 10773 145 145 0 11664 0 [pid=22676] vsize: 47236 Current children cumulated CPU time (s) 319.46 Current children cumulated vsize (Kb) 49360 [startup+330.039 s] Raw data (loadavg): 0.99 0.98 0.99 2/58 22686 Raw data (/proc/22672/stat): 22672 (minisat+_script) S 22671 22672 9102 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846564936 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/22672/statm): 531 226 485 147 0 384 0 [pid=22672] vsize: 2124 Raw data (/proc/22676/stat): 22676 (minisat+_64-bit) R 22672 22672 9102 0 -1 0 11205 0 0 0 32888 57 0 0 25 0 1 0 1846564941 48676864 10849 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/22676/statm): 11884 10849 145 145 0 11739 0 [pid=22676] vsize: 47536 Current children cumulated CPU time (s) 329.46 Current children cumulated vsize (Kb) 49660 [startup+340.041 s] Raw data (loadavg): 0.99 0.98 0.99 2/58 22688 Raw data (/proc/22672/stat): 22672 (minisat+_script) S 22671 22672 9102 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846564936 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/22672/statm): 531 226 485 147 0 384 0 [pid=22672] vsize: 2124 Raw data (/proc/22676/stat): 22676 (minisat+_64-bit) R 22672 22672 9102 0 -1 0 11297 0 0 0 33886 58 0 0 25 0 1 0 1846564941 49053696 10941 4294967295 134512640 135094434 3221224432 3221223088 134558249 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/22676/statm): 11976 10941 145 145 0 11831 0 [pid=22676] vsize: 47904 Current children cumulated CPU time (s) 339.45 Current children cumulated vsize (Kb) 50028 [startup+350.042 s] Raw data (loadavg): 0.99 0.98 0.99 2/58 22688 Raw data (/proc/22672/stat): 22672 (minisat+_script) S 22671 22672 9102 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846564936 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/22672/statm): 531 226 485 147 0 384 0 [pid=22672] vsize: 2124 Raw data (/proc/22676/stat): 22676 (minisat+_64-bit) R 22672 22672 9102 0 -1 0 11360 0 0 0 34885 59 0 0 25 0 1 0 1846564941 49307648 11004 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/22676/statm): 12038 11004 145 145 0 11893 0 [pid=22676] vsize: 48152 Current children cumulated CPU time (s) 349.45 Current children cumulated vsize (Kb) 50276 [startup+360.043 s] Raw data (loadavg): 0.99 0.98 0.99 2/58 22688 Raw data (/proc/22672/stat): 22672 (minisat+_script) S 22671 22672 9102 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846564936 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/22672/statm): 531 226 485 147 0 384 0 [pid=22672] vsize: 2124 Raw data (/proc/22676/stat): 22676 (minisat+_64-bit) R 22672 22672 9102 0 -1 0 11425 0 0 0 35885 59 0 0 25 0 1 0 1846564941 49569792 11069 4294967295 134512640 135094434 3221224432 3221221808 134600283 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/22676/statm): 12102 11069 145 145 0 11957 0 [pid=22676] vsize: 48408 Current children cumulated CPU time (s) 359.45 Current children cumulated vsize (Kb) 50532 [startup+370.044 s] Raw data (loadavg): 0.99 0.98 0.99 2/58 22688 Raw data (/proc/22672/stat): 22672 (minisat+_script) S 22671 22672 9102 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846564936 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/22672/statm): 531 226 485 147 0 384 0 [pid=22672] vsize: 2124 Raw data (/proc/22676/stat): 22676 (minisat+_64-bit) R 22672 22672 9102 0 -1 0 11445 0 0 0 36884 59 0 0 25 0 1 0 1846564941 49647616 11089 4294967295 134512640 135094434 3221224432 3221223056 134557596 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/22676/statm): 12121 11089 145 145 0 11976 0 [pid=22676] vsize: 48484 Current children cumulated CPU time (s) 369.44 Current children cumulated vsize (Kb) 50608 [startup+380.045 s] Raw data (loadavg): 0.99 0.98 0.99 2/58 22688 Raw data (/proc/22672/stat): 22672 (minisat+_script) S 22671 22672 9102 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846564936 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/22672/statm): 531 226 485 147 0 384 0 [pid=22672] vsize: 2124 Raw data (/proc/22676/stat): 22676 (minisat+_64-bit) R 22672 22672 9102 0 -1 0 11557 0 0 0 37883 60 0 0 25 0 1 0 1846564941 50098176 11201 4294967295 134512640 135094434 3221224432 3221223056 134557669 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/22676/statm): 12231 11201 145 145 0 12086 0 [pid=22676] vsize: 48924 Current children cumulated CPU time (s) 379.44 Current children cumulated vsize (Kb) 51048 [startup+390.046 s] Raw data (loadavg): 0.99 0.98 0.99 2/58 22688 Raw data (/proc/22672/stat): 22672 (minisat+_script) S 22671 22672 9102 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846564936 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/22672/statm): 531 226 485 147 0 384 0 [pid=22672] vsize: 2124 Raw data (/proc/22676/stat): 22676 (minisat+_64-bit) R 22672 22672 9102 0 -1 0 11639 0 0 0 38882 60 0 0 25 0 1 0 1846564941 50429952 11283 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/22676/statm): 12312 11283 145 145 0 12167 0 [pid=22676] vsize: 49248 Current children cumulated CPU time (s) 389.43 Current children cumulated vsize (Kb) 51372 [startup+400.047 s] Raw data (loadavg): 0.99 0.98 0.99 2/58 22690 Raw data (/proc/22672/stat): 22672 (minisat+_script) S 22671 22672 9102 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846564936 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/22672/statm): 531 226 485 147 0 384 0 [pid=22672] vsize: 2124 Raw data (/proc/22676/stat): 22676 (minisat+_64-bit) R 22672 22672 9102 0 -1 0 11764 0 0 0 39880 61 0 0 25 0 1 0 1846564941 50937856 11408 4294967295 134512640 135094434 3221224432 3221221552 134676999 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/22676/statm): 12436 11408 145 145 0 12291 0 [pid=22676] vsize: 49744 Current children cumulated CPU time (s) 399.42 Current children cumulated vsize (Kb) 51868 [startup+410.048 s] Raw data (loadavg): 0.99 0.98 0.99 2/58 22690 Raw data (/proc/22672/stat): 22672 (minisat+_script) S 22671 22672 9102 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846564936 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/22672/statm): 531 226 485 147 0 384 0 [pid=22672] vsize: 2124 Raw data (/proc/22676/stat): 22676 (minisat+_64-bit) R 22672 22672 9102 0 -1 0 11778 0 0 0 40880 61 0 0 25 0 1 0 1846564941 50991104 11422 4294967295 134512640 135094434 3221224432 3221223120 134554685 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/22676/statm): 12449 11422 145 145 0 12304 0 [pid=22676] vsize: 49796 Current children cumulated CPU time (s) 409.42 Current children cumulated vsize (Kb) 51920 [startup+420.049 s] Raw data (loadavg): 0.99 0.98 0.99 2/58 22690 Raw data (/proc/22672/stat): 22672 (minisat+_script) S 22671 22672 9102 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846564936 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/22672/statm): 531 226 485 147 0 384 0 [pid=22672] vsize: 2124 Raw data (/proc/22676/stat): 22676 (minisat+_64-bit) R 22672 22672 9102 0 -1 0 11855 0 0 0 41878 62 0 0 25 0 1 0 1846564941 51302400 11499 4294967295 134512640 135094434 3221224432 3221223088 134558213 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/22676/statm): 12525 11499 145 145 0 12380 0 [pid=22676] vsize: 50100 Current children cumulated CPU time (s) 419.41 Current children cumulated vsize (Kb) 52224 [startup+430.05 s] Raw data (loadavg): 0.99 0.98 0.99 2/58 22690 Raw data (/proc/22672/stat): 22672 (minisat+_script) S 22671 22672 9102 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846564936 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/22672/statm): 531 226 485 147 0 384 0 [pid=22672] vsize: 2124 Raw data (/proc/22676/stat): 22676 (minisat+_64-bit) R 22672 22672 9102 0 -1 0 11940 0 0 0 42877 63 0 0 25 0 1 0 1846564941 51646464 11584 4294967295 134512640 135094434 3221224432 3221223088 134558276 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/22676/statm): 12609 11584 145 145 0 12464 0 [pid=22676] vsize: 50436 Current children cumulated CPU time (s) 429.41 Current children cumulated vsize (Kb) 52560 [startup+440.051 s] Raw data (loadavg): 0.99 0.98 0.99 2/58 22690 Raw data (/proc/22672/stat): 22672 (minisat+_script) S 22671 22672 9102 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846564936 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/22672/statm): 531 226 485 147 0 384 0 [pid=22672] vsize: 2124 Raw data (/proc/22676/stat): 22676 (minisat+_64-bit) R 22672 22672 9102 0 -1 0 12009 0 0 0 43876 64 0 0 25 0 1 0 1846564941 51929088 11653 4294967295 134512640 135094434 3221224432 3221223120 134554746 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/22676/statm): 12678 11653 145 145 0 12533 0 [pid=22676] vsize: 50712 Current children cumulated CPU time (s) 439.41 Current children cumulated vsize (Kb) 52836 [startup+450.052 s] Raw data (loadavg): 0.99 0.98 0.99 2/58 22690 Raw data (/proc/22672/stat): 22672 (minisat+_script) S 22671 22672 9102 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846564936 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/22672/statm): 531 226 485 147 0 384 0 [pid=22672] vsize: 2124 Raw data (/proc/22676/stat): 22676 (minisat+_64-bit) R 22672 22672 9102 0 -1 0 12051 0 0 0 44875 65 0 0 25 0 1 0 1846564941 52097024 11695 4294967295 134512640 135094434 3221224432 3221223088 134557996 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/22676/statm): 12719 11695 145 145 0 12574 0 [pid=22676] vsize: 50876 Current children cumulated CPU time (s) 449.41 Current children cumulated vsize (Kb) 53000 [startup+460.053 s] Raw data (loadavg): 0.99 0.98 0.99 2/58 22692 Raw data (/proc/22672/stat): 22672 (minisat+_script) S 22671 22672 9102 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846564936 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/22672/statm): 531 226 485 147 0 384 0 [pid=22672] vsize: 2124 Raw data (/proc/22676/stat): 22676 (minisat+_64-bit) R 22672 22672 9102 0 -1 0 12096 0 0 0 45873 66 0 0 25 0 1 0 1846564941 52277248 11740 4294967295 134512640 135094434 3221224432 3221223116 134553432 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/22676/statm): 12763 11740 145 145 0 12618 0 [pid=22676] vsize: 51052 Current children cumulated CPU time (s) 459.4 Current children cumulated vsize (Kb) 53176 [startup+470.055 s] Raw data (loadavg): 0.99 0.98 0.99 2/58 22692 Raw data (/proc/22672/stat): 22672 (minisat+_script) S 22671 22672 9102 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846564936 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/22672/statm): 531 226 485 147 0 384 0 [pid=22672] vsize: 2124 Raw data (/proc/22676/stat): 22676 (minisat+_64-bit) R 22672 22672 9102 0 -1 0 12171 0 0 0 46872 67 0 0 25 0 1 0 1846564941 52580352 11815 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/22676/statm): 12837 11815 145 145 0 12692 0 [pid=22676] vsize: 51348 Current children cumulated CPU time (s) 469.4 Current children cumulated vsize (Kb) 53472 [startup+480.056 s] Raw data (loadavg): 0.99 0.98 0.99 2/58 22692 Raw data (/proc/22672/stat): 22672 (minisat+_script) S 22671 22672 9102 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846564936 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/22672/statm): 531 226 485 147 0 384 0 [pid=22672] vsize: 2124 Raw data (/proc/22676/stat): 22676 (minisat+_64-bit) R 22672 22672 9102 0 -1 0 12252 0 0 0 47871 68 0 0 25 0 1 0 1846564941 52912128 11896 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/22676/statm): 12918 11896 145 145 0 12773 0 [pid=22676] vsize: 51672 Current children cumulated CPU time (s) 479.4 Current children cumulated vsize (Kb) 53796 [startup+490.058 s] Raw data (loadavg): 0.99 0.98 0.99 2/58 22692 Raw data (/proc/22672/stat): 22672 (minisat+_script) S 22671 22672 9102 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846564936 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/22672/statm): 531 226 485 147 0 384 0 [pid=22672] vsize: 2124 Raw data (/proc/22676/stat): 22676 (minisat+_64-bit) R 22672 22672 9102 0 -1 0 12331 0 0 0 48870 69 0 0 25 0 1 0 1846564941 53231616 11975 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/22676/statm): 12996 11975 145 145 0 12851 0 [pid=22676] vsize: 51984 Current children cumulated CPU time (s) 489.4 Current children cumulated vsize (Kb) 54108 [startup+500.059 s] Raw data (loadavg): 0.99 0.98 0.99 2/58 22692 Raw data (/proc/22672/stat): 22672 (minisat+_script) S 22671 22672 9102 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846564936 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/22672/statm): 531 226 485 147 0 384 0 [pid=22672] vsize: 2124 Raw data (/proc/22676/stat): 22676 (minisat+_64-bit) R 22672 22672 9102 0 -1 0 12405 0 0 0 49869 70 0 0 25 0 1 0 1846564941 53530624 12049 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/22676/statm): 13069 12049 145 145 0 12924 0 [pid=22676] vsize: 52276 Current children cumulated CPU time (s) 499.4 Current children cumulated vsize (Kb) 54400 [startup+510.06 s] Raw data (loadavg): 0.99 0.98 0.99 2/58 22692 Raw data (/proc/22672/stat): 22672 (minisat+_script) S 22671 22672 9102 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846564936 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/22672/statm): 531 226 485 147 0 384 0 [pid=22672] vsize: 2124 Raw data (/proc/22676/stat): 22676 (minisat+_64-bit) R 22672 22672 9102 0 -1 0 12515 0 0 0 50867 71 0 0 25 0 1 0 1846564941 53977088 12159 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/22676/statm): 13178 12159 145 145 0 13033 0 [pid=22676] vsize: 52712 Current children cumulated CPU time (s) 509.39 Current children cumulated vsize (Kb) 54836 [startup+520.061 s] Raw data (loadavg): 0.99 0.98 0.99 2/58 22694 Raw data (/proc/22672/stat): 22672 (minisat+_script) S 22671 22672 9102 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846564936 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/22672/statm): 531 226 485 147 0 384 0 [pid=22672] vsize: 2124 Raw data (/proc/22676/stat): 22676 (minisat+_64-bit) R 22672 22672 9102 0 -1 0 12572 0 0 0 51866 71 0 0 25 0 1 0 1846564941 54206464 12216 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/22676/statm): 13234 12216 145 145 0 13089 0 [pid=22676] vsize: 52936 Current children cumulated CPU time (s) 519.38 Current children cumulated vsize (Kb) 55060 [startup+530.063 s] Raw data (loadavg): 0.99 0.98 0.99 2/58 22694 Raw data (/proc/22672/stat): 22672 (minisat+_script) S 22671 22672 9102 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846564936 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/22672/statm): 531 226 485 147 0 384 0 [pid=22672] vsize: 2124 Raw data (/proc/22676/stat): 22676 (minisat+_64-bit) R 22672 22672 9102 0 -1 0 12621 0 0 0 52866 71 0 0 25 0 1 0 1846564941 54665216 12265 4294967295 134512640 135094434 3221224432 3221223088 134557988 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/22676/statm): 13346 12265 145 145 0 13201 0 [pid=22676] vsize: 53384 Current children cumulated CPU time (s) 529.38 Current children cumulated vsize (Kb) 55508 [startup+540.065 s] Raw data (loadavg): 0.99 0.98 0.99 2/58 22694 Raw data (/proc/22672/stat): 22672 (minisat+_script) S 22671 22672 9102 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846564936 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/22672/statm): 531 226 485 147 0 384 0 [pid=22672] vsize: 2124 Raw data (/proc/22676/stat): 22676 (minisat+_64-bit) R 22672 22672 9102 0 -1 0 12672 0 0 0 53865 72 0 0 25 0 1 0 1846564941 54870016 12316 4294967295 134512640 135094434 3221224432 3221223056 134557596 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/22676/statm): 13396 12316 145 145 0 13251 0 [pid=22676] vsize: 53584 Current children cumulated CPU time (s) 539.38 Current children cumulated vsize (Kb) 55708 [startup+550.066 s] Raw data (loadavg): 0.99 0.98 0.99 2/58 22694 Raw data (/proc/22672/stat): 22672 (minisat+_script) S 22671 22672 9102 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846564936 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/22672/statm): 531 226 485 147 0 384 0 [pid=22672] vsize: 2124 Raw data (/proc/22676/stat): 22676 (minisat+_64-bit) R 22672 22672 9102 0 -1 0 12717 0 0 0 54865 72 0 0 25 0 1 0 1846564941 55054336 12361 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/22676/statm): 13441 12361 145 145 0 13296 0 [pid=22676] vsize: 53764 Current children cumulated CPU time (s) 549.38 Current children cumulated vsize (Kb) 55888 [startup+560.067 s] Raw data (loadavg): 0.99 0.98 0.99 2/58 22694 Raw data (/proc/22672/stat): 22672 (minisat+_script) S 22671 22672 9102 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846564936 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/22672/statm): 531 226 485 147 0 384 0 [pid=22672] vsize: 2124 Raw data (/proc/22676/stat): 22676 (minisat+_64-bit) R 22672 22672 9102 0 -1 0 12791 0 0 0 55864 72 0 0 25 0 1 0 1846564941 55353344 12435 4294967295 134512640 135094434 3221224432 3221222220 134676460 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/22676/statm): 13514 12435 145 145 0 13369 0 [pid=22676] vsize: 54056 Current children cumulated CPU time (s) 559.37 Current children cumulated vsize (Kb) 56180 [startup+570.068 s] Raw data (loadavg): 0.99 0.98 0.99 2/58 22694 Raw data (/proc/22672/stat): 22672 (minisat+_script) S 22671 22672 9102 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846564936 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/22672/statm): 531 226 485 147 0 384 0 [pid=22672] vsize: 2124 Raw data (/proc/22676/stat): 22676 (minisat+_64-bit) R 22672 22672 9102 0 -1 0 12809 0 0 0 56864 73 0 0 25 0 1 0 1846564941 55422976 12453 4294967295 134512640 135094434 3221224432 3221223056 134557724 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/22676/statm): 13531 12453 145 145 0 13386 0 [pid=22676] vsize: 54124 Current children cumulated CPU time (s) 569.38 Current children cumulated vsize (Kb) 56248 [startup+580.069 s] Raw data (loadavg): 0.99 0.98 0.99 2/58 22696 Raw data (/proc/22672/stat): 22672 (minisat+_script) S 22671 22672 9102 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846564936 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/22672/statm): 531 226 485 147 0 384 0 [pid=22672] vsize: 2124 Raw data (/proc/22676/stat): 22676 (minisat+_64-bit) R 22672 22672 9102 0 -1 0 12874 0 0 0 57863 73 0 0 25 0 1 0 1846564941 55685120 12518 4294967295 134512640 135094434 3221224432 3221223120 134554746 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/22676/statm): 13595 12518 145 145 0 13450 0 [pid=22676] vsize: 54380 Current children cumulated CPU time (s) 579.37 Current children cumulated vsize (Kb) 56504 [startup+590.071 s] Raw data (loadavg): 0.99 0.98 0.99 2/58 22696 Raw data (/proc/22672/stat): 22672 (minisat+_script) S 22671 22672 9102 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846564936 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/22672/statm): 531 226 485 147 0 384 0 [pid=22672] vsize: 2124 Raw data (/proc/22676/stat): 22676 (minisat+_64-bit) R 22672 22672 9102 0 -1 0 12995 0 0 0 58861 74 0 0 25 0 1 0 1846564941 56168448 12639 4294967295 134512640 135094434 3221224432 3221223088 134558159 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/22676/statm): 13713 12639 145 145 0 13568 0 [pid=22676] vsize: 54852 Current children cumulated CPU time (s) 589.36 Current children cumulated vsize (Kb) 56976 [startup+600.071 s] Raw data (loadavg): 0.99 0.98 0.99 2/58 22696 Raw data (/proc/22672/stat): 22672 (minisat+_script) S 22671 22672 9102 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846564936 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/22672/statm): 531 226 485 147 0 384 0 [pid=22672] vsize: 2124 Raw data (/proc/22676/stat): 22676 (minisat+_64-bit) R 22672 22672 9102 0 -1 0 13041 0 0 0 59860 75 0 0 25 0 1 0 1846564941 56356864 12685 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/22676/statm): 13759 12685 145 145 0 13614 0 [pid=22676] vsize: 55036 Current children cumulated CPU time (s) 599.36 Current children cumulated vsize (Kb) 57160 [startup+610.071 s] Raw data (loadavg): 0.99 0.98 0.99 2/58 22696 Raw data (/proc/22672/stat): 22672 (minisat+_script) S 22671 22672 9102 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846564936 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/22672/statm): 531 226 485 147 0 384 0 [pid=22672] vsize: 2124 Raw data (/proc/22676/stat): 22676 (minisat+_64-bit) R 22672 22672 9102 0 -1 0 13139 0 0 0 60858 75 0 0 25 0 1 0 1846564941 56745984 12783 4294967295 134512640 135094434 3221224432 3221223088 134558187 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/22676/statm): 13854 12783 145 145 0 13709 0 [pid=22676] vsize: 55416 Current children cumulated CPU time (s) 609.34 Current children cumulated vsize (Kb) 57540 [startup+620.072 s] Raw data (loadavg): 0.99 0.98 0.99 2/58 22696 Raw data (/proc/22672/stat): 22672 (minisat+_script) S 22671 22672 9102 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846564936 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/22672/statm): 531 226 485 147 0 384 0 [pid=22672] vsize: 2124 Raw data (/proc/22676/stat): 22676 (minisat+_64-bit) R 22672 22672 9102 0 -1 0 13196 0 0 0 61858 75 0 0 25 0 1 0 1846564941 56983552 12840 4294967295 134512640 135094434 3221224432 3221223056 134562104 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/22676/statm): 13912 12840 145 145 0 13767 0 [pid=22676] vsize: 55648 Current children cumulated CPU time (s) 619.34 Current children cumulated vsize (Kb) 57772 [startup+630.073 s] Raw data (loadavg): 0.99 0.98 0.99 2/58 22696 Raw data (/proc/22672/stat): 22672 (minisat+_script) S 22671 22672 9102 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846564936 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/22672/statm): 531 226 485 147 0 384 0 [pid=22672] vsize: 2124 Raw data (/proc/22676/stat): 22676 (minisat+_64-bit) R 22672 22672 9102 0 -1 0 13269 0 0 0 62857 76 0 0 25 0 1 0 1846564941 57278464 12913 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/22676/statm): 13984 12913 145 145 0 13839 0 [pid=22676] vsize: 55936 Current children cumulated CPU time (s) 629.34 Current children cumulated vsize (Kb) 58060 [startup+640.074 s] Raw data (loadavg): 0.99 0.98 0.99 2/58 22698 Raw data (/proc/22672/stat): 22672 (minisat+_script) S 22671 22672 9102 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846564936 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/22672/statm): 531 226 485 147 0 384 0 [pid=22672] vsize: 2124 Raw data (/proc/22676/stat): 22676 (minisat+_64-bit) R 22672 22672 9102 0 -1 0 13356 0 0 0 63855 77 0 0 25 0 1 0 1846564941 57626624 13000 4294967295 134512640 135094434 3221224432 3221223056 134557596 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/22676/statm): 14069 13000 145 145 0 13924 0 [pid=22676] vsize: 56276 Current children cumulated CPU time (s) 639.33 Current children cumulated vsize (Kb) 58400 [startup+650.075 s] Raw data (loadavg): 0.99 0.98 0.99 2/58 22698 Raw data (/proc/22672/stat): 22672 (minisat+_script) S 22671 22672 9102 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846564936 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/22672/statm): 531 226 485 147 0 384 0 [pid=22672] vsize: 2124 Raw data (/proc/22676/stat): 22676 (minisat+_64-bit) R 22672 22672 9102 0 -1 0 13415 0 0 0 64855 77 0 0 25 0 1 0 1846564941 57864192 13059 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/22676/statm): 14127 13059 145 145 0 13982 0 [pid=22676] vsize: 56508 Current children cumulated CPU time (s) 649.33 Current children cumulated vsize (Kb) 58632 [startup+660.076 s] Raw data (loadavg): 0.99 0.98 0.99 2/58 22698 Raw data (/proc/22672/stat): 22672 (minisat+_script) S 22671 22672 9102 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846564936 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/22672/statm): 531 226 485 147 0 384 0 [pid=22672] vsize: 2124 Raw data (/proc/22676/stat): 22676 (minisat+_64-bit) R 22672 22672 9102 0 -1 0 13486 0 0 0 65854 78 0 0 25 0 1 0 1846564941 58155008 13130 4294967295 134512640 135094434 3221224432 3221223092 134553536 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/22676/statm): 14198 13130 145 145 0 14053 0 [pid=22676] vsize: 56792 Current children cumulated CPU time (s) 659.33 Current children cumulated vsize (Kb) 58916 [startup+670.077 s] Raw data (loadavg): 0.99 0.98 0.99 1/58 22698 Raw data (/proc/22672/stat): 22672 (minisat+_script) S 22671 22672 9102 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846564936 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/22672/statm): 531 226 485 147 0 384 0 [pid=22672] vsize: 2124 Raw data (/proc/22676/stat): 22676 (minisat+_64-bit) T 22672 22672 9102 0 -1 0 13509 0 0 0 66854 78 0 0 25 0 1 0 1846564941 58245120 13153 4294967295 134512640 135094434 3221224432 3221222812 134870330 0 0 5 16386 3222434794 0 0 17 1 0 0 Raw data (/proc/22676/statm): 14220 13153 145 145 0 14075 0 [pid=22676] vsize: 56880 Current children cumulated CPU time (s) 669.33 Current children cumulated vsize (Kb) 59004 [startup+680.078 s] Raw data (loadavg): 0.99 0.98 0.99 2/58 22698 Raw data (/proc/22672/stat): 22672 (minisat+_script) S 22671 22672 9102 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846564936 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/22672/statm): 531 226 485 147 0 384 0 [pid=22672] vsize: 2124 Raw data (/proc/22676/stat): 22676 (minisat+_64-bit) R 22672 22672 9102 0 -1 0 13551 0 0 0 67853 79 0 0 25 0 1 0 1846564941 58413056 13195 4294967295 134512640 135094434 3221224432 3221223120 134554731 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/22676/statm): 14261 13195 145 145 0 14116 0 [pid=22676] vsize: 57044 Current children cumulated CPU time (s) 679.33 Current children cumulated vsize (Kb) 59168 [startup+690.079 s] Raw data (loadavg): 0.99 0.98 0.99 2/58 22698 Raw data (/proc/22672/stat): 22672 (minisat+_script) S 22671 22672 9102 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846564936 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/22672/statm): 531 226 485 147 0 384 0 [pid=22672] vsize: 2124 Raw data (/proc/22676/stat): 22676 (minisat+_64-bit) R 22672 22672 9102 0 -1 0 13597 0 0 0 68853 79 0 0 25 0 1 0 1846564941 58597376 13241 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/22676/statm): 14306 13241 145 145 0 14161 0 [pid=22676] vsize: 57224 Current children cumulated CPU time (s) 689.33 Current children cumulated vsize (Kb) 59348 [startup+700.08 s] Raw data (loadavg): 0.99 0.98 0.99 2/58 22700 Raw data (/proc/22672/stat): 22672 (minisat+_script) S 22671 22672 9102 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846564936 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/22672/statm): 531 226 485 147 0 384 0 [pid=22672] vsize: 2124 Raw data (/proc/22676/stat): 22676 (minisat+_64-bit) R 22672 22672 9102 0 -1 0 13648 0 0 0 69851 80 0 0 25 0 1 0 1846564941 58810368 13292 4294967295 134512640 135094434 3221224432 3221223056 134562085 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/22676/statm): 14358 13292 145 145 0 14213 0 [pid=22676] vsize: 57432 Current children cumulated CPU time (s) 699.32 Current children cumulated vsize (Kb) 59556 [startup+710.081 s] Raw data (loadavg): 0.99 0.98 0.99 2/58 22700 Raw data (/proc/22672/stat): 22672 (minisat+_script) S 22671 22672 9102 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846564936 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/22672/statm): 531 226 485 147 0 384 0 [pid=22672] vsize: 2124 Raw data (/proc/22676/stat): 22676 (minisat+_64-bit) R 22672 22672 9102 0 -1 0 13742 0 0 0 70850 80 0 0 25 0 1 0 1846564941 59191296 13386 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/22676/statm): 14451 13386 145 145 0 14306 0 [pid=22676] vsize: 57804 Current children cumulated CPU time (s) 709.31 Current children cumulated vsize (Kb) 59928 [startup+720.082 s] Raw data (loadavg): 0.99 0.98 0.99 2/58 22700 Raw data (/proc/22672/stat): 22672 (minisat+_script) S 22671 22672 9102 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846564936 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/22672/statm): 531 226 485 147 0 384 0 [pid=22672] vsize: 2124 Raw data (/proc/22676/stat): 22676 (minisat+_64-bit) R 22672 22672 9102 0 -1 0 13808 0 0 0 71849 81 0 0 25 0 1 0 1846564941 59457536 13452 4294967295 134512640 135094434 3221224432 3221223104 134556394 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/22676/statm): 14516 13452 145 145 0 14371 0 [pid=22676] vsize: 58064 Current children cumulated CPU time (s) 719.31 Current children cumulated vsize (Kb) 60188 [startup+730.083 s] Raw data (loadavg): 0.99 0.98 0.99 2/58 22700 Raw data (/proc/22672/stat): 22672 (minisat+_script) S 22671 22672 9102 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846564936 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/22672/statm): 531 226 485 147 0 384 0 [pid=22672] vsize: 2124 Raw data (/proc/22676/stat): 22676 (minisat+_64-bit) R 22672 22672 9102 0 -1 0 13871 0 0 0 72848 81 0 0 25 0 1 0 1846564941 59715584 13515 4294967295 134512640 135094434 3221224432 3221223024 134557040 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/22676/statm): 14579 13515 145 145 0 14434 0 [pid=22676] vsize: 58316 Current children cumulated CPU time (s) 729.3 Current children cumulated vsize (Kb) 60440 [startup+740.085 s] Raw data (loadavg): 0.99 0.98 0.99 2/58 22700 Raw data (/proc/22672/stat): 22672 (minisat+_script) S 22671 22672 9102 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846564936 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/22672/statm): 531 226 485 147 0 384 0 [pid=22672] vsize: 2124 Raw data (/proc/22676/stat): 22676 (minisat+_64-bit) R 22672 22672 9102 0 -1 0 13948 0 0 0 73846 82 0 0 25 0 1 0 1846564941 60026880 13592 4294967295 134512640 135094434 3221224432 3221223024 134556809 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/22676/statm): 14655 13592 145 145 0 14510 0 [pid=22676] vsize: 58620 Current children cumulated CPU time (s) 739.29 Current children cumulated vsize (Kb) 60744 [startup+750.086 s] Raw data (loadavg): 0.99 0.98 0.99 2/58 22700 Raw data (/proc/22672/stat): 22672 (minisat+_script) S 22671 22672 9102 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846564936 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/22672/statm): 531 226 485 147 0 384 0 [pid=22672] vsize: 2124 Raw data (/proc/22676/stat): 22676 (minisat+_64-bit) R 22672 22672 9102 0 -1 0 14030 0 0 0 74845 83 0 0 25 0 1 0 1846564941 60362752 13674 4294967295 134512640 135094434 3221224432 3221223056 134557636 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/22676/statm): 14737 13674 145 145 0 14592 0 [pid=22676] vsize: 58948 Current children cumulated CPU time (s) 749.29 Current children cumulated vsize (Kb) 61072 [startup+760.085 s] Raw data (loadavg): 0.99 0.98 0.99 2/58 22702 Raw data (/proc/22672/stat): 22672 (minisat+_script) S 22671 22672 9102 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846564936 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/22672/statm): 531 226 485 147 0 384 0 [pid=22672] vsize: 2124 Raw data (/proc/22676/stat): 22676 (minisat+_64-bit) R 22672 22672 9102 0 -1 0 14114 0 0 0 75844 83 0 0 25 0 1 0 1846564941 60698624 13758 4294967295 134512640 135094434 3221224432 3221223056 134557696 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/22676/statm): 14819 13758 145 145 0 14674 0 [pid=22676] vsize: 59276 Current children cumulated CPU time (s) 759.28 Current children cumulated vsize (Kb) 61400 [startup+770.087 s] Raw data (loadavg): 0.99 0.98 0.99 2/58 22702 Raw data (/proc/22672/stat): 22672 (minisat+_script) S 22671 22672 9102 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846564936 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/22672/statm): 531 226 485 147 0 384 0 [pid=22672] vsize: 2124 Raw data (/proc/22676/stat): 22676 (minisat+_64-bit) R 22672 22672 9102 0 -1 0 14212 0 0 0 76843 84 0 0 25 0 1 0 1846564941 61095936 13856 4294967295 134512640 135094434 3221224432 3221223088 134558159 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/22676/statm): 14916 13856 145 145 0 14771 0 [pid=22676] vsize: 59664 Current children cumulated CPU time (s) 769.28 Current children cumulated vsize (Kb) 61788 [startup+780.088 s] Raw data (loadavg): 0.99 0.98 0.99 2/58 22702 Raw data (/proc/22672/stat): 22672 (minisat+_script) S 22671 22672 9102 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846564936 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/22672/statm): 531 226 485 147 0 384 0 [pid=22672] vsize: 2124 Raw data (/proc/22676/stat): 22676 (minisat+_64-bit) R 22672 22672 9102 0 -1 0 14283 0 0 0 77842 84 0 0 25 0 1 0 1846564941 61386752 13927 4294967295 134512640 135094434 3221224432 3221223088 134558213 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/22676/statm): 14987 13927 145 145 0 14842 0 [pid=22676] vsize: 59948 Current children cumulated CPU time (s) 779.27 Current children cumulated vsize (Kb) 62072 [startup+790.089 s] Raw data (loadavg): 0.99 0.98 0.99 2/58 22702 Raw data (/proc/22672/stat): 22672 (minisat+_script) S 22671 22672 9102 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846564936 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/22672/statm): 531 226 485 147 0 384 0 [pid=22672] vsize: 2124 Raw data (/proc/22676/stat): 22676 (minisat+_64-bit) R 22672 22672 9102 0 -1 0 14426 0 0 0 78840 86 0 0 25 0 1 0 1846564941 61968384 14070 4294967295 134512640 135094434 3221224432 3221223088 134558159 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/22676/statm): 15129 14070 145 145 0 14984 0 [pid=22676] vsize: 60516 Current children cumulated CPU time (s) 789.27 Current children cumulated vsize (Kb) 62640 [startup+800.09 s] Raw data (loadavg): 0.99 0.98 0.99 2/58 22702 Raw data (/proc/22672/stat): 22672 (minisat+_script) S 22671 22672 9102 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846564936 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/22672/statm): 531 226 485 147 0 384 0 [pid=22672] vsize: 2124 Raw data (/proc/22676/stat): 22676 (minisat+_64-bit) R 22672 22672 9102 0 -1 0 14578 0 0 0 79838 87 0 0 25 0 1 0 1846564941 62586880 14222 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/22676/statm): 15280 14222 145 145 0 15135 0 [pid=22676] vsize: 61120 Current children cumulated CPU time (s) 799.26 Current children cumulated vsize (Kb) 63244 [startup+810.091 s] Raw data (loadavg): 0.99 0.98 0.99 2/58 22702 Raw data (/proc/22672/stat): 22672 (minisat+_script) S 22671 22672 9102 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846564936 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/22672/statm): 531 226 485 147 0 384 0 [pid=22672] vsize: 2124 Raw data (/proc/22676/stat): 22676 (minisat+_64-bit) R 22672 22672 9102 0 -1 0 14650 0 0 0 80837 87 0 0 25 0 1 0 1846564941 62881792 14294 4294967295 134512640 135094434 3221224432 3221223104 134556317 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/22676/statm): 15352 14294 145 145 0 15207 0 [pid=22676] vsize: 61408 Current children cumulated CPU time (s) 809.25 Current children cumulated vsize (Kb) 63532 [startup+820.092 s] Raw data (loadavg): 0.99 0.98 0.99 2/58 22704 Raw data (/proc/22672/stat): 22672 (minisat+_script) S 22671 22672 9102 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846564936 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/22672/statm): 531 226 485 147 0 384 0 [pid=22672] vsize: 2124 Raw data (/proc/22676/stat): 22676 (minisat+_64-bit) R 22672 22672 9102 0 -1 0 14782 0 0 0 81835 88 0 0 25 0 1 0 1846564941 63426560 14426 4294967295 134512640 135094434 3221224432 3221223104 134556454 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/22676/statm): 15485 14426 145 145 0 15340 0 [pid=22676] vsize: 61940 Current children cumulated CPU time (s) 819.24 Current children cumulated vsize (Kb) 64064 [startup+830.093 s] Raw data (loadavg): 0.99 0.98 0.99 2/58 22704 Raw data (/proc/22672/stat): 22672 (minisat+_script) S 22671 22672 9102 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846564936 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/22672/statm): 531 226 485 147 0 384 0 [pid=22672] vsize: 2124 Raw data (/proc/22676/stat): 22676 (minisat+_64-bit) R 22672 22672 9102 0 -1 0 14881 0 0 0 82834 88 0 0 25 0 1 0 1846564941 63840256 14525 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/22676/statm): 15586 14525 145 145 0 15441 0 [pid=22676] vsize: 62344 Current children cumulated CPU time (s) 829.23 Current children cumulated vsize (Kb) 64468 [startup+840.095 s] Raw data (loadavg): 0.99 0.98 0.99 2/58 22704 Raw data (/proc/22672/stat): 22672 (minisat+_script) S 22671 22672 9102 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846564936 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/22672/statm): 531 226 485 147 0 384 0 [pid=22672] vsize: 2124 Raw data (/proc/22676/stat): 22676 (minisat+_64-bit) R 22672 22672 9102 0 -1 0 15081 0 0 0 83831 90 0 0 25 0 1 0 1846564941 64651264 14725 4294967295 134512640 135094434 3221224432 3221221808 134600225 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/22676/statm): 15784 14725 145 145 0 15639 0 [pid=22676] vsize: 63136 Current children cumulated CPU time (s) 839.22 Current children cumulated vsize (Kb) 65260 [startup+850.096 s] Raw data (loadavg): 0.99 0.98 0.99 2/58 22704 Raw data (/proc/22672/stat): 22672 (minisat+_script) S 22671 22672 9102 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846564936 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/22672/statm): 531 226 485 147 0 384 0 [pid=22672] vsize: 2124 Raw data (/proc/22676/stat): 22676 (minisat+_64-bit) R 22672 22672 9102 0 -1 0 15098 0 0 0 84831 90 0 0 25 0 1 0 1846564941 64716800 14742 4294967295 134512640 135094434 3221224432 3221223024 134556853 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/22676/statm): 15800 14742 145 145 0 15655 0 [pid=22676] vsize: 63200 Current children cumulated CPU time (s) 849.22 Current children cumulated vsize (Kb) 65324 [startup+860.096 s] Raw data (loadavg): 0.99 0.98 0.99 2/58 22704 Raw data (/proc/22672/stat): 22672 (minisat+_script) S 22671 22672 9102 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846564936 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/22672/statm): 531 226 485 147 0 384 0 [pid=22672] vsize: 2124 Raw data (/proc/22676/stat): 22676 (minisat+_64-bit) R 22672 22672 9102 0 -1 0 15175 0 0 0 85830 91 0 0 25 0 1 0 1846564941 65048576 14819 4294967295 134512640 135094434 3221224432 3221223088 134558249 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/22676/statm): 15881 14819 145 145 0 15736 0 [pid=22676] vsize: 63524 Current children cumulated CPU time (s) 859.22 Current children cumulated vsize (Kb) 65648 [startup+870.097 s] Raw data (loadavg): 0.99 0.98 0.99 2/58 22704 Raw data (/proc/22672/stat): 22672 (minisat+_script) S 22671 22672 9102 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846564936 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/22672/statm): 531 226 485 147 0 384 0 [pid=22672] vsize: 2124 Raw data (/proc/22676/stat): 22676 (minisat+_64-bit) R 22672 22672 9102 0 -1 0 15237 0 0 0 86828 91 0 0 25 0 1 0 1846564941 65294336 14881 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/22676/statm): 15941 14881 145 145 0 15796 0 [pid=22676] vsize: 63764 Current children cumulated CPU time (s) 869.2 Current children cumulated vsize (Kb) 65888 [startup+880.098 s] Raw data (loadavg): 0.99 0.98 0.99 2/58 22706 Raw data (/proc/22672/stat): 22672 (minisat+_script) S 22671 22672 9102 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846564936 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/22672/statm): 531 226 485 147 0 384 0 [pid=22672] vsize: 2124 Raw data (/proc/22676/stat): 22676 (minisat+_64-bit) R 22672 22672 9102 0 -1 0 15306 0 0 0 87828 92 0 0 25 0 1 0 1846564941 65576960 14950 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/22676/statm): 16010 14950 145 145 0 15865 0 [pid=22676] vsize: 64040 Current children cumulated CPU time (s) 879.21 Current children cumulated vsize (Kb) 66164 [startup+890.1 s] Raw data (loadavg): 0.99 0.98 0.99 2/58 22706 Raw data (/proc/22672/stat): 22672 (minisat+_script) S 22671 22672 9102 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846564936 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/22672/statm): 531 226 485 147 0 384 0 [pid=22672] vsize: 2124 Raw data (/proc/22676/stat): 22676 (minisat+_64-bit) R 22672 22672 9102 0 -1 0 15347 0 0 0 88828 92 0 0 25 0 1 0 1846564941 65740800 14991 4294967295 134512640 135094434 3221224432 3221223088 134558395 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/22676/statm): 16050 14991 145 145 0 15905 0 [pid=22676] vsize: 64200 Current children cumulated CPU time (s) 889.21 Current children cumulated vsize (Kb) 66324 [startup+900.101 s] Raw data (loadavg): 0.99 0.98 0.99 2/58 22706 Raw data (/proc/22672/stat): 22672 (minisat+_script) S 22671 22672 9102 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846564936 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/22672/statm): 531 226 485 147 0 384 0 [pid=22672] vsize: 2124 Raw data (/proc/22676/stat): 22676 (minisat+_64-bit) R 22672 22672 9102 0 -1 0 15414 0 0 0 89827 92 0 0 25 0 1 0 1846564941 66019328 15058 4294967295 134512640 135094434 3221224432 3221223024 134557131 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/22676/statm): 16118 15058 145 145 0 15973 0 [pid=22676] vsize: 64472 Current children cumulated CPU time (s) 899.2 Current children cumulated vsize (Kb) 66596 [startup+910.101 s] Raw data (loadavg): 0.99 0.98 0.99 2/58 22706 Raw data (/proc/22672/stat): 22672 (minisat+_script) S 22671 22672 9102 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846564936 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/22672/statm): 531 226 485 147 0 384 0 [pid=22672] vsize: 2124 Raw data (/proc/22676/stat): 22676 (minisat+_64-bit) R 22672 22672 9102 0 -1 0 15465 0 0 0 90827 92 0 0 25 0 1 0 1846564941 66232320 15109 4294967295 134512640 135094434 3221224432 3221223024 134556851 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/22676/statm): 16170 15109 145 145 0 16025 0 [pid=22676] vsize: 64680 Current children cumulated CPU time (s) 909.2 Current children cumulated vsize (Kb) 66804 [startup+920.102 s] Raw data (loadavg): 0.99 0.98 0.99 2/58 22706 Raw data (/proc/22672/stat): 22672 (minisat+_script) S 22671 22672 9102 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846564936 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/22672/statm): 531 226 485 147 0 384 0 [pid=22672] vsize: 2124 Raw data (/proc/22676/stat): 22676 (minisat+_64-bit) R 22672 22672 9102 0 -1 0 15552 0 0 0 91826 93 0 0 25 0 1 0 1846564941 66584576 15196 4294967295 134512640 135094434 3221224432 3221223056 134557604 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/22676/statm): 16256 15196 145 145 0 16111 0 [pid=22676] vsize: 65024 Current children cumulated CPU time (s) 919.2 Current children cumulated vsize (Kb) 67148 [startup+930.103 s] Raw data (loadavg): 0.99 0.98 0.99 2/58 22706 Raw data (/proc/22672/stat): 22672 (minisat+_script) S 22671 22672 9102 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846564936 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/22672/statm): 531 226 485 147 0 384 0 [pid=22672] vsize: 2124 Raw data (/proc/22676/stat): 22676 (minisat+_64-bit) R 22672 22672 9102 0 -1 0 15639 0 0 0 92824 93 0 0 25 0 1 0 1846564941 66940928 15283 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/22676/statm): 16343 15283 145 145 0 16198 0 [pid=22676] vsize: 65372 Current children cumulated CPU time (s) 929.18 Current children cumulated vsize (Kb) 67496 [startup+940.104 s] Raw data (loadavg): 0.99 0.98 0.99 2/58 22708 Raw data (/proc/22672/stat): 22672 (minisat+_script) S 22671 22672 9102 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846564936 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/22672/statm): 531 226 485 147 0 384 0 [pid=22672] vsize: 2124 Raw data (/proc/22676/stat): 22676 (minisat+_64-bit) R 22672 22672 9102 0 -1 0 15731 0 0 0 93823 95 0 0 25 0 1 0 1846564941 67309568 15375 4294967295 134512640 135094434 3221224432 3221221248 134600704 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/22676/statm): 16433 15375 145 145 0 16288 0 [pid=22676] vsize: 65732 Current children cumulated CPU time (s) 939.19 Current children cumulated vsize (Kb) 67856 [startup+950.105 s] Raw data (loadavg): 0.99 0.98 0.99 2/58 22708 Raw data (/proc/22672/stat): 22672 (minisat+_script) S 22671 22672 9102 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846564936 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/22672/statm): 531 226 485 147 0 384 0 [pid=22672] vsize: 2124 Raw data (/proc/22676/stat): 22676 (minisat+_64-bit) R 22672 22672 9102 0 -1 0 15731 0 0 0 94823 95 0 0 25 0 1 0 1846564941 67309568 15375 4294967295 134512640 135094434 3221224432 3221223104 134556317 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/22676/statm): 16433 15375 145 145 0 16288 0 [pid=22676] vsize: 65732 Current children cumulated CPU time (s) 949.19 Current children cumulated vsize (Kb) 67856 [startup+960.106 s] Raw data (loadavg): 0.99 0.98 0.99 2/58 22708 Raw data (/proc/22672/stat): 22672 (minisat+_script) S 22671 22672 9102 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846564936 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/22672/statm): 531 226 485 147 0 384 0 [pid=22672] vsize: 2124 Raw data (/proc/22676/stat): 22676 (minisat+_64-bit) R 22672 22672 9102 0 -1 0 15731 0 0 0 95823 95 0 0 25 0 1 0 1846564941 67309568 15375 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/22676/statm): 16433 15375 145 145 0 16288 0 [pid=22676] vsize: 65732 Current children cumulated CPU time (s) 959.19 Current children cumulated vsize (Kb) 67856 [startup+970.107 s] Raw data (loadavg): 0.99 0.98 0.99 2/58 22708 Raw data (/proc/22672/stat): 22672 (minisat+_script) S 22671 22672 9102 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846564936 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/22672/statm): 531 226 485 147 0 384 0 [pid=22672] vsize: 2124 Raw data (/proc/22676/stat): 22676 (minisat+_64-bit) R 22672 22672 9102 0 -1 0 15732 0 0 0 96823 95 0 0 25 0 1 0 1846564941 67309568 15376 4294967295 134512640 135094434 3221224432 3221222912 134781309 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/22676/statm): 16433 15376 145 145 0 16288 0 [pid=22676] vsize: 65732 Current children cumulated CPU time (s) 969.19 Current children cumulated vsize (Kb) 67856 [startup+980.108 s] Raw data (loadavg): 0.99 0.98 0.99 2/58 22708 Raw data (/proc/22672/stat): 22672 (minisat+_script) S 22671 22672 9102 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846564936 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/22672/statm): 531 226 485 147 0 384 0 [pid=22672] vsize: 2124 Raw data (/proc/22676/stat): 22676 (minisat+_64-bit) R 22672 22672 9102 0 -1 0 15732 0 0 0 97823 95 0 0 25 0 1 0 1846564941 67309568 15376 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/22676/statm): 16433 15376 145 145 0 16288 0 [pid=22676] vsize: 65732 Current children cumulated CPU time (s) 979.19 Current children cumulated vsize (Kb) 67856 [startup+990.109 s] Raw data (loadavg): 0.99 0.98 0.99 2/58 22708 Raw data (/proc/22672/stat): 22672 (minisat+_script) S 22671 22672 9102 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846564936 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/22672/statm): 531 226 485 147 0 384 0 [pid=22672] vsize: 2124 Raw data (/proc/22676/stat): 22676 (minisat+_64-bit) R 22672 22672 9102 0 -1 0 15732 0 0 0 98823 95 0 0 25 0 1 0 1846564941 67309568 15376 4294967295 134512640 135094434 3221224432 3221221904 134677069 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/22676/statm): 16433 15376 145 145 0 16288 0 [pid=22676] vsize: 65732 Current children cumulated CPU time (s) 989.19 Current children cumulated vsize (Kb) 67856 [startup+1000.11 s] Raw data (loadavg): 0.99 0.98 0.99 2/58 22710 Raw data (/proc/22672/stat): 22672 (minisat+_script) S 22671 22672 9102 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846564936 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/22672/statm): 531 226 485 147 0 384 0 [pid=22672] vsize: 2124 Raw data (/proc/22676/stat): 22676 (minisat+_64-bit) R 22672 22672 9102 0 -1 0 15732 0 0 0 99824 95 0 0 25 0 1 0 1846564941 67309568 15376 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/22676/statm): 16433 15376 145 145 0 16288 0 [pid=22676] vsize: 65732 Current children cumulated CPU time (s) 999.2 Current children cumulated vsize (Kb) 67856 [startup+1010.11 s] Raw data (loadavg): 0.99 0.98 0.99 2/58 22710 Raw data (/proc/22672/stat): 22672 (minisat+_script) S 22671 22672 9102 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846564936 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/22672/statm): 531 226 485 147 0 384 0 [pid=22672] vsize: 2124 Raw data (/proc/22676/stat): 22676 (minisat+_64-bit) R 22672 22672 9102 0 -1 0 15732 0 0 0 100824 95 0 0 25 0 1 0 1846564941 67309568 15376 4294967295 134512640 135094434 3221224432 3221223056 134557585 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/22676/statm): 16433 15376 145 145 0 16288 0 [pid=22676] vsize: 65732 Current children cumulated CPU time (s) 1009.2 Current children cumulated vsize (Kb) 67856 [startup+1020.11 s] Raw data (loadavg): 0.99 0.98 0.99 2/58 22710 Raw data (/proc/22672/stat): 22672 (minisat+_script) S 22671 22672 9102 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846564936 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/22672/statm): 531 226 485 147 0 384 0 [pid=22672] vsize: 2124 Raw data (/proc/22676/stat): 22676 (minisat+_64-bit) R 22672 22672 9102 0 -1 0 15732 0 0 0 101824 95 0 0 25 0 1 0 1846564941 67309568 15376 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/22676/statm): 16433 15376 145 145 0 16288 0 [pid=22676] vsize: 65732 Current children cumulated CPU time (s) 1019.2 Current children cumulated vsize (Kb) 67856 [startup+1030.11 s] Raw data (loadavg): 0.99 0.98 0.99 2/58 22710 Raw data (/proc/22672/stat): 22672 (minisat+_script) S 22671 22672 9102 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846564936 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/22672/statm): 531 226 485 147 0 384 0 [pid=22672] vsize: 2124 Raw data (/proc/22676/stat): 22676 (minisat+_64-bit) R 22672 22672 9102 0 -1 0 15732 0 0 0 102824 95 0 0 25 0 1 0 1846564941 67309568 15376 4294967295 134512640 135094434 3221224432 3221223056 134557565 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/22676/statm): 16433 15376 145 145 0 16288 0 [pid=22676] vsize: 65732 Current children cumulated CPU time (s) 1029.2 Current children cumulated vsize (Kb) 67856 [startup+1040.11 s] Raw data (loadavg): 0.99 0.98 0.99 2/58 22710 Raw data (/proc/22672/stat): 22672 (minisat+_script) S 22671 22672 9102 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846564936 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/22672/statm): 531 226 485 147 0 384 0 [pid=22672] vsize: 2124 Raw data (/proc/22676/stat): 22676 (minisat+_64-bit) R 22672 22672 9102 0 -1 0 15732 0 0 0 103824 95 0 0 25 0 1 0 1846564941 67309568 15376 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/22676/statm): 16433 15376 145 145 0 16288 0 [pid=22676] vsize: 65732 Current children cumulated CPU time (s) 1039.2 Current children cumulated vsize (Kb) 67856 [startup+1050.12 s] Raw data (loadavg): 0.99 0.98 0.99 2/58 22710 Raw data (/proc/22672/stat): 22672 (minisat+_script) S 22671 22672 9102 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846564936 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/22672/statm): 531 226 485 147 0 384 0 [pid=22672] vsize: 2124 Raw data (/proc/22676/stat): 22676 (minisat+_64-bit) R 22672 22672 9102 0 -1 0 15732 0 0 0 104824 96 0 0 25 0 1 0 1846564941 67309568 15376 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/22676/statm): 16433 15376 145 145 0 16288 0 [pid=22676] vsize: 65732 Current children cumulated CPU time (s) 1049.21 Current children cumulated vsize (Kb) 67856 [startup+1060.12 s] Raw data (loadavg): 0.99 0.98 0.99 2/58 22712 Raw data (/proc/22672/stat): 22672 (minisat+_script) S 22671 22672 9102 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846564936 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/22672/statm): 531 226 485 147 0 384 0 [pid=22672] vsize: 2124 Raw data (/proc/22676/stat): 22676 (minisat+_64-bit) R 22672 22672 9102 0 -1 0 15732 0 0 0 105823 97 0 0 25 0 1 0 1846564941 67309568 15376 4294967295 134512640 135094434 3221224432 3221223024 134556949 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/22676/statm): 16433 15376 145 145 0 16288 0 [pid=22676] vsize: 65732 Current children cumulated CPU time (s) 1059.21 Current children cumulated vsize (Kb) 67856 [startup+1070.12 s] Raw data (loadavg): 0.99 0.98 0.99 2/58 22712 Raw data (/proc/22672/stat): 22672 (minisat+_script) S 22671 22672 9102 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846564936 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/22672/statm): 531 226 485 147 0 384 0 [pid=22672] vsize: 2124 Raw data (/proc/22676/stat): 22676 (minisat+_64-bit) R 22672 22672 9102 0 -1 0 15732 0 0 0 106823 97 0 0 25 0 1 0 1846564941 67309568 15376 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/22676/statm): 16433 15376 145 145 0 16288 0 [pid=22676] vsize: 65732 Current children cumulated CPU time (s) 1069.21 Current children cumulated vsize (Kb) 67856 [startup+1080.12 s] Raw data (loadavg): 0.99 0.98 0.99 2/58 22712 Raw data (/proc/22672/stat): 22672 (minisat+_script) S 22671 22672 9102 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846564936 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/22672/statm): 531 226 485 147 0 384 0 [pid=22672] vsize: 2124 Raw data (/proc/22676/stat): 22676 (minisat+_64-bit) R 22672 22672 9102 0 -1 0 15732 0 0 0 107823 98 0 0 25 0 1 0 1846564941 67309568 15376 4294967295 134512640 135094434 3221224432 3221223024 134557180 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/22676/statm): 16433 15376 145 145 0 16288 0 [pid=22676] vsize: 65732 Current children cumulated CPU time (s) 1079.22 Current children cumulated vsize (Kb) 67856 [startup+1090.12 s] Raw data (loadavg): 0.99 0.98 0.99 2/58 22712 Raw data (/proc/22672/stat): 22672 (minisat+_script) S 22671 22672 9102 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846564936 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/22672/statm): 531 226 485 147 0 384 0 [pid=22672] vsize: 2124 Raw data (/proc/22676/stat): 22676 (minisat+_64-bit) R 22672 22672 9102 0 -1 0 15732 0 0 0 108823 98 0 0 25 0 1 0 1846564941 67309568 15376 4294967295 134512640 135094434 3221224432 3221223024 134557512 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/22676/statm): 16433 15376 145 145 0 16288 0 [pid=22676] vsize: 65732 Current children cumulated CPU time (s) 1089.22 Current children cumulated vsize (Kb) 67856 [startup+1100.12 s] Raw data (loadavg): 0.99 0.98 0.99 2/58 22712 Raw data (/proc/22672/stat): 22672 (minisat+_script) S 22671 22672 9102 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846564936 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/22672/statm): 531 226 485 147 0 384 0 [pid=22672] vsize: 2124 Raw data (/proc/22676/stat): 22676 (minisat+_64-bit) R 22672 22672 9102 0 -1 0 15734 0 0 0 109823 98 0 0 25 0 1 0 1846564941 67309568 15378 4294967295 134512640 135094434 3221224432 3221223220 134553482 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/22676/statm): 16433 15378 145 145 0 16288 0 [pid=22676] vsize: 65732 Current children cumulated CPU time (s) 1099.22 Current children cumulated vsize (Kb) 67856 [startup+1110.12 s] Raw data (loadavg): 0.99 0.98 0.99 2/58 22712 Raw data (/proc/22672/stat): 22672 (minisat+_script) S 22671 22672 9102 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846564936 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/22672/statm): 531 226 485 147 0 384 0 [pid=22672] vsize: 2124 Raw data (/proc/22676/stat): 22676 (minisat+_64-bit) R 22672 22672 9102 0 -1 0 15734 0 0 0 110823 98 0 0 25 0 1 0 1846564941 67309568 15378 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/22676/statm): 16433 15378 145 145 0 16288 0 [pid=22676] vsize: 65732 Current children cumulated CPU time (s) 1109.22 Current children cumulated vsize (Kb) 67856 [startup+1120.12 s] Raw data (loadavg): 0.99 0.98 0.99 2/58 22714 Raw data (/proc/22672/stat): 22672 (minisat+_script) S 22671 22672 9102 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846564936 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/22672/statm): 531 226 485 147 0 384 0 [pid=22672] vsize: 2124 Raw data (/proc/22676/stat): 22676 (minisat+_64-bit) R 22672 22672 9102 0 -1 0 15734 0 0 0 111823 98 0 0 25 0 1 0 1846564941 67309568 15378 4294967295 134512640 135094434 3221224432 3221223088 134558213 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/22676/statm): 16433 15378 145 145 0 16288 0 [pid=22676] vsize: 65732 Current children cumulated CPU time (s) 1119.22 Current children cumulated vsize (Kb) 67856 [startup+1130.12 s] Raw data (loadavg): 0.99 0.98 0.99 2/58 22714 Raw data (/proc/22672/stat): 22672 (minisat+_script) S 22671 22672 9102 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846564936 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/22672/statm): 531 226 485 147 0 384 0 [pid=22672] vsize: 2124 Raw data (/proc/22676/stat): 22676 (minisat+_64-bit) R 22672 22672 9102 0 -1 0 15734 0 0 0 112823 98 0 0 25 0 1 0 1846564941 67309568 15378 4294967295 134512640 135094434 3221224432 3221223088 134557893 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/22676/statm): 16433 15378 145 145 0 16288 0 [pid=22676] vsize: 65732 Current children cumulated CPU time (s) 1129.22 Current children cumulated vsize (Kb) 67856 [startup+1140.12 s] Raw data (loadavg): 0.99 0.98 0.99 2/58 22714 Raw data (/proc/22672/stat): 22672 (minisat+_script) S 22671 22672 9102 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846564936 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/22672/statm): 531 226 485 147 0 384 0 [pid=22672] vsize: 2124 Raw data (/proc/22676/stat): 22676 (minisat+_64-bit) R 22672 22672 9102 0 -1 0 15734 0 0 0 113823 99 0 0 25 0 1 0 1846564941 67309568 15378 4294967295 134512640 135094434 3221224432 3221223088 134558208 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/22676/statm): 16433 15378 145 145 0 16288 0 [pid=22676] vsize: 65732 Current children cumulated CPU time (s) 1139.23 Current children cumulated vsize (Kb) 67856 [startup+1150.13 s] Raw data (loadavg): 0.99 0.98 0.99 2/58 22714 Raw data (/proc/22672/stat): 22672 (minisat+_script) S 22671 22672 9102 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846564936 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/22672/statm): 531 226 485 147 0 384 0 [pid=22672] vsize: 2124 Raw data (/proc/22676/stat): 22676 (minisat+_64-bit) R 22672 22672 9102 0 -1 0 15734 0 0 0 114823 99 0 0 25 0 1 0 1846564941 67309568 15378 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/22676/statm): 16433 15378 145 145 0 16288 0 [pid=22676] vsize: 65732 Current children cumulated CPU time (s) 1149.23 Current children cumulated vsize (Kb) 67856 [startup+1160.13 s] Raw data (loadavg): 0.99 0.98 0.99 2/58 22714 Raw data (/proc/22672/stat): 22672 (minisat+_script) S 22671 22672 9102 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846564936 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/22672/statm): 531 226 485 147 0 384 0 [pid=22672] vsize: 2124 Raw data (/proc/22676/stat): 22676 (minisat+_64-bit) R 22672 22672 9102 0 -1 0 15734 0 0 0 115823 99 0 0 25 0 1 0 1846564941 67309568 15378 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/22676/statm): 16433 15378 145 145 0 16288 0 [pid=22676] vsize: 65732 Current children cumulated CPU time (s) 1159.23 Current children cumulated vsize (Kb) 67856 [startup+1170.13 s] Raw data (loadavg): 0.99 0.98 0.99 2/58 22714 Raw data (/proc/22672/stat): 22672 (minisat+_script) S 22671 22672 9102 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846564936 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/22672/statm): 531 226 485 147 0 384 0 [pid=22672] vsize: 2124 Raw data (/proc/22676/stat): 22676 (minisat+_64-bit) R 22672 22672 9102 0 -1 0 15735 0 0 0 116823 99 0 0 25 0 1 0 1846564941 67309568 15379 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/22676/statm): 16433 15379 145 145 0 16288 0 [pid=22676] vsize: 65732 Current children cumulated CPU time (s) 1169.23 Current children cumulated vsize (Kb) 67856 [startup+1180.13 s] Raw data (loadavg): 0.99 0.98 0.99 2/58 22716 Raw data (/proc/22672/stat): 22672 (minisat+_script) S 22671 22672 9102 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846564936 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/22672/statm): 531 226 485 147 0 384 0 [pid=22672] vsize: 2124 Raw data (/proc/22676/stat): 22676 (minisat+_64-bit) R 22672 22672 9102 0 -1 0 15735 0 0 0 117824 99 0 0 25 0 1 0 1846564941 67309568 15379 4294967295 134512640 135094434 3221224432 3221223120 134554748 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/22676/statm): 16433 15379 145 145 0 16288 0 [pid=22676] vsize: 65732 Current children cumulated CPU time (s) 1179.24 Current children cumulated vsize (Kb) 67856 [startup+1190.13 s] Raw data (loadavg): 0.99 0.98 0.99 2/58 22716 Raw data (/proc/22672/stat): 22672 (minisat+_script) S 22671 22672 9102 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846564936 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/22672/statm): 531 226 485 147 0 384 0 [pid=22672] vsize: 2124 Raw data (/proc/22676/stat): 22676 (minisat+_64-bit) R 22672 22672 9102 0 -1 0 15735 0 0 0 118824 99 0 0 25 0 1 0 1846564941 67309568 15379 4294967295 134512640 135094434 3221224432 3221223088 134558249 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/22676/statm): 16433 15379 145 145 0 16288 0 [pid=22676] vsize: 65732 Current children cumulated CPU time (s) 1189.24 Current children cumulated vsize (Kb) 67856 [startup+1200.13 s] Raw data (loadavg): 0.99 0.98 0.99 2/58 22716 Raw data (/proc/22672/stat): 22672 (minisat+_script) S 22671 22672 9102 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846564936 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/22672/statm): 531 226 485 147 0 384 0 [pid=22672] vsize: 2124 Raw data (/proc/22676/stat): 22676 (minisat+_64-bit) R 22672 22672 9102 0 -1 0 15735 0 0 0 119824 99 0 0 25 0 1 0 1846564941 67309568 15379 4294967295 134512640 135094434 3221224432 3221223056 134557696 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/22676/statm): 16433 15379 145 145 0 16288 0 [pid=22676] vsize: 65732 Current children cumulated CPU time (s) 1199.24 Current children cumulated vsize (Kb) 67856 [startup+1210.13 s] Raw data (loadavg): 0.99 0.98 0.99 2/58 22716 Raw data (/proc/22672/stat): 22672 (minisat+_script) S 22671 22672 9102 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846564936 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/22672/statm): 531 226 485 147 0 384 0 [pid=22672] vsize: 2124 Raw data (/proc/22676/stat): 22676 (minisat+_64-bit) R 22672 22672 9102 0 -1 0 15735 0 0 0 120824 99 0 0 25 0 1 0 1846564941 67309568 15379 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/22676/statm): 16433 15379 145 145 0 16288 0 [pid=22676] vsize: 65732 Current children cumulated CPU time (s) 1209.24 Current children cumulated vsize (Kb) 67856 Maximum CPU time exceeded: sending SIGTERM then SIGKILL [startup+1210.13 s] Raw data (loadavg): 0.99 0.98 0.99 2/58 22716 Raw data (/proc/22672/stat): 22672 (minisat+_script) S 22671 22672 9102 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846564936 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/22672/statm): 531 226 485 147 0 384 0 [pid=22672] vsize: 2124 Raw data (/proc/22676/stat): 22676 (minisat+_64-bit) R 22672 22672 9102 0 -1 0 15735 0 0 0 120824 99 0 0 25 0 1 0 1846564941 67309568 15379 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/22676/statm): 16433 15379 145 145 0 16288 0 [pid=22676] vsize: 65732 Current children cumulated CPU time (s) 1209.24 Current children cumulated vsize (Kb) 67856 Sending SIGTERM to -22672 Sleeping 2 seconds One traced child (pid=22672) ended because it received signal 15 (SIGTERM) One traced child (pid=22676) exited with status: 10 All traced children have exited ! Game is over. Child status: 10 Real time (s): 1210.17 CPU time (s): 1209.28 CPU user time (s): 1208.25 CPU system time (s): 1.02984 CPU usage (%): 99.9266 Max. virtual memory (cumulated for all children) (Kb): 67856
ERROR: no interpretation found !