| Name | mps-v2-13-7/MIPLIB/miplib2003/normalized-mps-v2-13-7-pk1.opb |
| MD5SUM | 9c5126d785c8d5465220e290c5fc25a6 |
| Bench Category | optimization, medium integers (OPTMEDINT) |
| Has Objective Function | YES |
| Satisfiable | YES |
| (Un)Satisfiability was proved | YES |
| Best value of the objective function | 6656 |
| Optimality of the best value was proved | NO |
| Number of terms in the objective function | 20 |
| Biggest coefficient in the objective function | 524288 |
| Number of bits for the biggest coefficient in the objective function | 20 |
| Sum of the numbers in the objective function | 1048575 |
| Number of bits of the sum of numbers in the objective function | 20 |
| Biggest number in a constraint | 524288 |
| Number of bits of the biggest number in a constraint | 20 |
| Biggest sum of numbers in a constraint | 2421502 |
| Number of bits of the biggest sum of numbers | 22 |
| Best result obtained on this benchmark | SAT |
| Best CPU time to get the best result obtained on this benchmark | 1189.01 |
| Number of variables | 675 |
| Total number of constraints | 100 |
| Number of constraints which are clauses | 0 |
| Number of constraints which are cardinality constraints (but not clauses) | 55 |
| Number of constraints which are nor clauses,nor cardinality constraints | 45 |
| Minimum length of a constraint | 1 |
| Maximum length of a constraint | 95 |
LAUNCH ON wulflinc28 THE 2005-09-20 03:51:49 (client local time) PB2005-SCRIPT v4.0 MARKUPS: idlaunch=3318 boxname=wulflinc28 idbench=974 idsolver=3 numberseed=0 MD5SUM SOLVER: MD5SUM BENCH: 9c5126d785c8d5465220e290c5fc25a6 /oldhome/oroussel/tmp/wulflinc28/normalized-mps-v2-13-7-pk1.opb REAL COMMAND: minisat+_script /oldhome/oroussel/tmp/wulflinc28/normalized-mps-v2-13-7-pk1.opb IDLAUNCH: 3318 /proc/cpuinfo: processor : 0 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 3 cpu MHz : 451.077 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.077 cache size : 512 KB fdiv_bug : no hlt_bug : no f00f_bug : no coma_bug : no fpu : yes fpu_exception : yes cpuid level : 2 wp : yes flags : fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse bogomips : 899.07 /proc/meminfo: MemTotal: 1034660 kB MemFree: 889896 kB Buffers: 25304 kB Cached: 90520 kB SwapCached: 660 kB Active: 30708 kB Inactive: 87640 kB HighTotal: 131008 kB HighFree: 36988 kB LowTotal: 903652 kB LowFree: 852908 kB SwapTotal: 2097640 kB SwapFree: 2096408 kB Dirty: 28 kB Writeback: 0 kB Mapped: 5820 kB Slab: 20684 kB Committed_AS: 64164 kB PageTables: 328 kB VmallocTotal: 114680 kB VmallocUsed: 1368 kB VmallocChunk: 113252 kB JOB ENDED THE 2005-09-20 04:11:53 (client local time) WITH STATUS 10 IN 1202.51 SECONDS stats: 3318 7 1202.51 10
c Parsing PB file... c Converting 60 PB-constraints to clauses... c -- Unit propagations: (none) c -- Detecting intervals from adjacent constraints: ############### c -- Clauses(.)/Splits(s): (none) c ---[ 58]---> Adder-cost: 358 maxlim: 1151871 bits: 22/21 c ---[ 56]---> Adder-cost: 382 maxlim: 1183231 bits: 22/21 c ---[ 54]---> Adder-cost: 338 maxlim: 1135231 bits: 22/21 c ---[ 52]---> Adder-cost: 362 maxlim: 1185791 bits: 22/21 c ---[ 50]---> Adder-cost: 360 maxlim: 1161855 bits: 22/21 c ---[ 48]---> Adder-cost: 354 maxlim: 1184383 bits: 22/21 c ---[ 46]---> Adder-cost: 362 maxlim: 1156479 bits: 22/21 c ---[ 45]---> BDD-cost: 58 c ---[ 44]---> BDD-cost: 58 c ---[ 43]---> BDD-cost: 58 c ---[ 42]---> BDD-cost: 58 c ---[ 40]---> Adder-cost: 352 maxlim: 1176959 bits: 22/21 c ---[ 39]---> BDD-cost: 58 c ---[ 38]---> BDD-cost: 58 c ---[ 37]---> BDD-cost: 58 c ---[ 36]---> BDD-cost: 58 c ---[ 35]---> BDD-cost: 58 c ---[ 34]---> BDD-cost: 58 c ---[ 33]---> BDD-cost: 58 c ---[ 32]---> BDD-cost: 58 c ---[ 31]---> BDD-cost: 58 c ---[ 30]---> BDD-cost: 58 c ---[ 28]---> Adder-cost: 368 maxlim: 1155967 bits: 22/21 c ---[ 27]---> BDD-cost: 58 c ---[ 26]---> BDD-cost: 58 c ---[ 25]---> BDD-cost: 58 c ---[ 24]---> BDD-cost: 58 c ---[ 23]---> BDD-cost: 58 c ---[ 22]---> BDD-cost: 58 c ---[ 21]---> BDD-cost: 58 c ---[ 20]---> BDD-cost: 58 c ---[ 19]---> BDD-cost: 58 c ---[ 18]---> BDD-cost: 58 c ---[ 16]---> Adder-cost: 362 maxlim: 1178367 bits: 22/21 c ---[ 15]---> BDD-cost: 58 c ---[ 14]---> BDD-cost: 58 c ---[ 13]---> BDD-cost: 58 c ---[ 12]---> BDD-cost: 58 c ---[ 11]---> BDD-cost: 58 c ---[ 10]---> BDD-cost: 58 c ---[ 8]---> Adder-cost: 374 maxlim: 1184767 bits: 22/21 c ---[ 6]---> Adder-cost: 348 maxlim: 1169791 bits: 22/21 c ---[ 4]---> Adder-cost: 352 maxlim: 1145087 bits: 22/21 c ---[ 2]---> Adder-cost: 368 maxlim: 1171455 bits: 22/21 c ---[ 0]---> Adder-cost: 384 maxlim: 1175295 bits: 22/21 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 0 | 39453 136875 | 13151 0 0 nan | 0.000 % | c | 100 | 39447 136857 | 14466 99 387 3.9 | 8.290 % | c | 250 | 39439 136831 | 15912 248 1467 5.9 | 8.303 % | c | 475 | 39425 136787 | 17503 471 2953 6.3 | 8.327 % | c | 812 | 39401 136709 | 19254 805 6605 8.2 | 8.364 % | c | 1318 | 39303 136389 | 21179 1293 11310 8.7 | 8.523 % | c | 2077 | 39272 136288 | 23297 2048 17663 8.6 | 8.572 % | c | 3217 | 39045 135547 | 25627 3144 35150 11.2 | 8.953 % | c | 4925 | 39022 135472 | 28190 4849 68728 14.2 | 8.989 % | c | 7487 | 38936 135194 | 31009 7394 126289 17.1 | 9.137 % | c ============================================================================== c [1mFound solution: 1032188[0m c ---[ 0]---> BDD-cost: 17 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 11175 | 38567 133997 | 12855 10992 196903 17.9 | 9.137 % | c | 11275 | 38551 133943 | 14140 11087 198273 17.9 | 9.808 % | c ============================================================================== c [1mFound solution: 1031548[0m c ---[ 0]---> BDD-cost: 13 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 11361 | 38561 133977 | 12853 11173 199002 17.8 | 9.808 % | c | 11461 | 38561 133977 | 14138 11273 201356 17.9 | 9.811 % | c | 11612 | 38561 133977 | 15552 11424 205134 18.0 | 9.811 % | c | 11837 | 38553 133951 | 17107 11648 211611 18.2 | 9.824 % | c ============================================================================== c [1mFound solution: 999316[0m c ---[ 0]---> BDD-cost: 17 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 11949 | 38564 133985 | 12854 11760 212665 18.1 | 9.824 % | c | 12050 | 38564 133985 | 14139 11861 213681 18.0 | 9.829 % | c | 12201 | 38514 133821 | 15553 12001 215264 17.9 | 9.914 % | c ============================================================================== c [1mFound solution: 900724[0m c ---[ 0]---> BDD-cost: 15 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 12334 | 38517 133828 | 12839 12133 217327 17.9 | 9.914 % | c | 12435 | 38517 133828 | 14122 12234 218286 17.8 | 9.930 % | c | 12586 | 38517 133828 | 15535 12385 220130 17.8 | 9.930 % | c | 12812 | 38509 133802 | 17088 12610 222918 17.7 | 9.943 % | c ============================================================================== c [1mFound solution: 900020[0m c ---[ 0]---> BDD-cost: 14 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 13064 | 38510 133803 | 12836 12860 227360 17.7 | 9.943 % | c | 13165 | 38466 133657 | 14119 12949 228997 17.7 | 10.042 % | c ============================================================================== c [1mFound solution: 769020[0m c ---[ 0]---> BDD-cost: 10 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 13229 | 38476 133687 | 12825 13013 230078 17.7 | 10.042 % | c | 13334 | 38476 133687 | 14107 13118 232125 17.7 | 10.045 % | c | 13484 | 38476 133687 | 15518 13268 234387 17.7 | 10.045 % | c | 13709 | 38476 133687 | 17070 13493 236832 17.6 | 10.045 % | c ============================================================================== c [1mFound solution: 703676[0m c ---[ 0]---> BDD-cost: 14 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 13796 | 38493 133732 | 12831 13580 238203 17.5 | 10.045 % | c | 13896 | 38493 133732 | 14114 13680 240714 17.6 | 10.044 % | c ============================================================================== c [1mFound solution: 638428[0m c ---[ 0]---> BDD-cost: 15 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 14024 | 38507 133772 | 12835 13808 242939 17.6 | 10.044 % | c | 14124 | 38507 133772 | 14118 7004 104595 14.9 | 10.045 % | c | 14274 | 38507 133772 | 15530 7154 107672 15.1 | 10.045 % | c | 14501 | 38507 133772 | 17083 7381 111538 15.1 | 10.045 % | c | 14838 | 38507 133772 | 18791 7718 116976 15.2 | 10.045 % | c ============================================================================== c [1mFound solution: 636344[0m c ---[ 0]---> BDD-cost: 16 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 15054 | 38524 133816 | 12841 7934 120685 15.2 | 10.045 % | c | 15155 | 38524 133816 | 14125 8035 123448 15.4 | 10.044 % | c | 15306 | 38524 133816 | 15537 8186 127081 15.5 | 10.044 % | c | 15531 | 38524 133816 | 17091 8411 129719 15.4 | 10.044 % | c ============================================================================== c [1mFound solution: 602108[0m c ---[ 0]---> BDD-cost: 8 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 15864 | 38528 133819 | 12842 8743 134226 15.4 | 10.044 % | c | 15964 | 38528 133819 | 14126 8843 135467 15.3 | 10.060 % | c ============================================================================== c [1mFound solution: 597428[0m c ---[ 0]---> BDD-cost: 11 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 16015 | 38541 133852 | 12847 8894 136196 15.3 | 10.060 % | c | 16115 | 38541 133852 | 14131 8994 136847 15.2 | 10.063 % | c | 16265 | 38541 133852 | 15544 9144 139325 15.2 | 10.063 % | c | 16491 | 38541 133852 | 17099 9370 142064 15.2 | 10.063 % | c | 16828 | 38541 133852 | 18809 9707 148938 15.3 | 10.063 % | c ============================================================================== c [1mFound solution: 597424[0m c ---[ 0]---> BDD-cost: 15 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 17192 | 38507 133728 | 12835 10058 158021 15.7 | 10.063 % | c ============================================================================== c [1mFound solution: 571244[0m c ---[ 0]---> BDD-cost: 16 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 17251 | 38525 133774 | 12841 10117 158593 15.7 | 10.063 % | c | 17351 | 38525 133774 | 14125 10216 162923 15.9 | 10.160 % | c ============================================================================== c [1mFound solution: 470844[0m c ---[ 0]---> BDD-cost: 12 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 17378 | 38185 132707 | 12728 10242 163117 15.9 | 10.160 % | c ============================================================================== c [1mFound solution: 438116[0m c ---[ 0]---> BDD-cost: 15 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 17426 | 38200 132747 | 12733 10290 163932 15.9 | 10.160 % | c ============================================================================== c [1mFound solution: 437588[0m c ---[ 0]---> BDD-cost: 13 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 17447 | 38218 132791 | 12739 10311 164180 15.9 | 10.160 % | c ============================================================================== c [1mFound solution: 408412[0m c ---[ 0]---> BDD-cost: 12 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 17505 | 38230 132823 | 12743 10369 165755 16.0 | 10.160 % | c | 17605 | 38230 132823 | 14017 10469 166737 15.9 | 11.624 % | c | 17755 | 38222 132797 | 15419 10618 167941 15.8 | 11.636 % | c ============================================================================== c [1mFound solution: 342700[0m c ---[ 0]---> BDD-cost: 13 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 17794 | 38239 132839 | 12746 10657 168345 15.8 | 11.636 % | c | 17894 | 38239 132839 | 14020 10757 169464 15.8 | 11.633 % | c | 18045 | 38239 132839 | 15422 10908 172308 15.8 | 11.633 % | c ============================================================================== c [1mFound solution: 339528[0m c ---[ 0]---> BDD-cost: 15 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 18081 | 38257 132882 | 12752 10944 172755 15.8 | 11.633 % | c ============================================================================== c [1mFound solution: 338528[0m c ---[ 0]---> BDD-cost: 13 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 18149 | 38275 132924 | 12758 11012 174024 15.8 | 11.633 % | c | 18249 | 38275 132924 | 14033 11112 175147 15.8 | 11.628 % | c ============================================================================== c [1mFound solution: 269032[0m c ---[ 0]---> BDD-cost: 14 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 18274 | 38291 132963 | 12763 11137 175440 15.8 | 11.628 % | c ============================================================================== c [1mFound solution: 267460[0m c ---[ 0]---> BDD-cost: 14 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 18294 | 38308 133002 | 12769 11157 175904 15.8 | 11.628 % | c | 18394 | 38308 133002 | 14045 11257 177555 15.8 | 11.629 % | c ============================================================================== c [1mFound solution: 265440[0m c ---[ 0]---> BDD-cost: 12 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 18450 | 38321 133032 | 12773 11313 179038 15.8 | 11.629 % | c | 18551 | 38321 133032 | 14050 11414 179872 15.8 | 11.634 % | c ============================================================================== c [1mFound solution: 263756[0m c ---[ 0]---> BDD-cost: 14 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 18564 | 38337 133068 | 12779 11427 179959 15.7 | 11.634 % | c ============================================================================== c [1mFound solution: 158920[0m c ---[ 0]---> BDD-cost: 11 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 18629 | 38000 132024 | 12666 11492 181243 15.8 | 11.634 % | c | 18729 | 38000 132024 | 13932 11592 182173 15.7 | 13.088 % | c ============================================================================== c [1mFound solution: 142412[0m c ---[ 0]---> BDD-cost: 9 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 18810 | 38011 132050 | 12670 11673 183844 15.7 | 13.088 % | c | 18912 | 38011 132050 | 13937 11775 184544 15.7 | 13.090 % | c | 19062 | 38011 132050 | 15330 11925 187341 15.7 | 13.090 % | c ============================================================================== c [1mFound solution: 140972[0m c ---[ 0]---> BDD-cost: 8 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 19147 | 38021 132073 | 12673 12010 189602 15.8 | 13.090 % | c | 19248 | 38021 132073 | 13940 12111 191119 15.8 | 13.094 % | c | 19398 | 38021 132073 | 15334 12261 192404 15.7 | 13.094 % | c ============================================================================== c [1mFound solution: 140012[0m c ---[ 0]---> BDD-cost: 11 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 19411 | 38035 132105 | 12678 12274 192575 15.7 | 13.094 % | c | 19512 | 38035 132105 | 13945 12375 194923 15.8 | 13.095 % | c ============================================================================== c [1mFound solution: 139980[0m c ---[ 0]---> BDD-cost: 11 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 19532 | 38049 132137 | 12683 12395 195223 15.8 | 13.095 % | c ============================================================================== c [1mFound solution: 139940[0m c ---[ 0]---> BDD-cost: 12 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 19541 | 38066 132176 | 12688 12404 195352 15.7 | 13.095 % | c ============================================================================== c [1mFound solution: 139820[0m c ---[ 0]---> BDD-cost: 11 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 19581 | 38080 132207 | 12693 12444 196195 15.8 | 13.095 % | c ============================================================================== c [1mFound solution: 139816[0m c ---[ 0]---> BDD-cost: 12 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 19593 | 38096 132243 | 12698 12456 196315 15.8 | 13.095 % | c ============================================================================== c [1mFound solution: 139812[0m c ---[ 0]---> BDD-cost: 11 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 19661 | 38110 132274 | 12703 12524 198150 15.8 | 13.095 % | c | 19762 | 38110 132274 | 13973 12625 200106 15.8 | 13.100 % | c | 19913 | 38110 132274 | 15370 12776 202386 15.8 | 13.100 % | c ============================================================================== c [1mFound solution: 134348[0m c ---[ 0]---> BDD-cost: 9 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 19951 | 38120 132297 | 12706 12814 203025 15.8 | 13.100 % | c ============================================================================== c [1mFound solution: 132268[0m c ---[ 0]---> BDD-cost: 9 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 19982 | 38131 132321 | 12710 12845 203417 15.8 | 13.100 % | c ============================================================================== c [1mFound solution: 131148[0m c ---[ 0]---> BDD-cost: 8 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 20019 | 38140 132340 | 12713 12882 203941 15.8 | 13.100 % | c ============================================================================== c [1mFound solution: 131108[0m c ---[ 0]---> BDD-cost: 9 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 20059 | 38150 132361 | 12716 12922 204966 15.9 | 13.100 % | c ============================================================================== c [1mFound solution: 131104[0m c ---[ 0]---> BDD-cost: 12 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 20088 | 38163 132388 | 12721 12951 205451 15.9 | 13.100 % | c ============================================================================== c [1mFound solution: 131076[0m c ---[ 0]---> BDD-cost: 12 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 20118 | 38176 132415 | 12725 12981 205799 15.9 | 13.100 % | c | 20220 | 38176 132415 | 13997 13083 210002 16.1 | 13.147 % | c ============================================================================== c [1mFound solution: 131072[0m c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 20309 | 37814 131312 | 12604 13171 211513 16.1 | 13.147 % | c | 20409 | 37814 131312 | 13864 13271 213184 16.1 | 14.582 % | c ============================================================================== c [1mFound solution: 98532[0m c ---[ 0]---> BDD-cost: 10 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 20486 | 37824 131335 | 12608 13348 214437 16.1 | 14.582 % | c | 20586 | 37824 131335 | 13868 13448 215561 16.0 | 14.589 % | c ============================================================================== c [1mFound solution: 98380[0m c ---[ 0]---> BDD-cost: 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 20627 | 37831 131351 | 12610 13489 215928 16.0 | 14.589 % | c | 20727 | 37831 131351 | 13871 13589 218006 16.0 | 14.597 % | c ============================================================================== c [1mFound solution: 98372[0m c ---[ 0]---> BDD-cost: 10 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 20747 | 37842 131376 | 12614 13609 218241 16.0 | 14.597 % | c ============================================================================== c [1mFound solution: 98368[0m c ---[ 0]---> BDD-cost: 10 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 20780 | 37852 131398 | 12617 13642 218780 16.0 | 14.597 % | c | 20880 | 37852 131398 | 13878 13742 219699 16.0 | 14.612 % | c ============================================================================== c [1mFound solution: 65772[0m c ---[ 0]---> BDD-cost: 8 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 21024 | 37861 131417 | 12620 13886 221900 16.0 | 14.612 % | c | 21127 | 37861 131417 | 13882 7046 93558 13.3 | 14.621 % | c | 21277 | 37847 131373 | 15270 7194 94459 13.1 | 14.645 % | c ============================================================================== c [1mFound solution: 36008[0m c ---[ 0]---> BDD-cost: 9 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 21471 | 37490 130280 | 12496 7385 98544 13.3 | 14.645 % | c | 21572 | 37490 130280 | 13745 7486 100549 13.4 | 16.079 % | c | 21723 | 37490 130280 | 15120 7637 104959 13.7 | 16.079 % | c ============================================================================== c [1mFound solution: 36000[0m c ---[ 0]---> BDD-cost: 9 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 21897 | 37502 130308 | 12500 7811 107277 13.7 | 16.079 % | c | 21998 | 37502 130308 | 13750 7912 109182 13.8 | 16.079 % | c | 22149 | 37502 130308 | 15125 8063 112160 13.9 | 16.079 % | c | 22376 | 37502 130308 | 16637 8290 115326 13.9 | 16.079 % | c | 22715 | 37502 130308 | 18301 8629 121340 14.1 | 16.079 % | c ============================================================================== c [1mFound solution: 23588[0m c ---[ 0]---> BDD-cost: 5 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 23197 | 37143 129228 | 12381 9109 130456 14.3 | 16.079 % | c | 23297 | 37143 129228 | 13619 9209 131580 14.3 | 17.514 % | c ============================================================================== c [1mFound solution: 22572[0m c ---[ 0]---> BDD-cost: 6 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 23394 | 37150 129245 | 12383 9306 133607 14.4 | 17.514 % | c | 23495 | 37150 129245 | 13621 9407 135033 14.4 | 17.518 % | c | 23646 | 37150 129245 | 14983 9558 137670 14.4 | 17.518 % | c | 23871 | 37150 129245 | 16481 9783 141845 14.5 | 17.518 % | c ============================================================================== c [1mFound solution: 22568[0m c ---[ 0]---> BDD-cost: 6 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 24053 | 37157 129262 | 12385 9965 145314 14.6 | 17.518 % | c | 24154 | 37157 129262 | 13623 10066 146158 14.5 | 17.521 % | c | 24304 | 37149 129236 | 14985 10215 147556 14.4 | 17.533 % | c | 24530 | 37149 129236 | 16484 10441 150377 14.4 | 17.533 % | c | 24867 | 37149 129236 | 18132 10778 157768 14.6 | 17.533 % | c | 25373 | 37149 129236 | 19946 11284 173225 15.4 | 17.533 % | c ============================================================================== c [1mFound solution: 22564[0m c ---[ 0]---> BDD-cost: 4 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 25675 | 37155 129251 | 12385 11586 180952 15.6 | 17.533 % | c | 25775 | 37155 129251 | 13623 11686 182432 15.6 | 17.537 % | c | 25925 | 37155 129251 | 14985 11836 187672 15.9 | 17.537 % | c | 26152 | 37155 129251 | 16484 12063 191383 15.9 | 17.537 % | c | 26491 | 37155 129251 | 18132 12402 198077 16.0 | 17.537 % | c ============================================================================== c [1mFound solution: 21668[0m c ---[ 0]---> BDD-cost: 6 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 26746 | 37164 129272 | 12388 12657 201035 15.9 | 17.537 % | c | 26846 | 37164 129272 | 13626 12757 203685 16.0 | 17.536 % | c | 26996 | 37164 129272 | 14989 12907 208447 16.1 | 17.536 % | c | 27221 | 37164 129272 | 16488 13132 214257 16.3 | 17.536 % | c | 27558 | 37164 129272 | 18137 13469 217763 16.2 | 17.536 % | c ============================================================================== c [1mFound solution: 16544[0m c ---[ 0]---> BDD-cost: 5 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 27707 | 37170 129285 | 12390 13618 219822 16.1 | 17.536 % | c | 27808 | 37170 129285 | 13629 13719 221409 16.1 | 17.544 % | c | 27958 | 37170 129285 | 14991 13869 226366 16.3 | 17.544 % | c | 28184 | 37170 129285 | 16491 14095 228647 16.2 | 17.544 % | c | 28521 | 37170 129285 | 18140 14432 239750 16.6 | 17.544 % | c | 29027 | 37170 129285 | 19954 14938 253849 17.0 | 17.544 % | c ============================================================================== c [1mFound solution: 16524[0m c ---[ 0]---> BDD-cost: 9 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 29673 | 37181 129309 | 12393 15584 272030 17.5 | 17.544 % | c | 29774 | 37181 129309 | 13632 7893 137617 17.4 | 17.547 % | c | 29924 | 37181 129309 | 14995 8043 139888 17.4 | 17.547 % | c | 30149 | 37181 129309 | 16495 8268 145904 17.6 | 17.547 % | c | 30488 | 37181 129309 | 18144 8607 153568 17.8 | 17.547 % | c | 30994 | 37181 129309 | 19959 9113 166116 18.2 | 17.547 % | c | 31754 | 37181 129309 | 21954 9873 193403 19.6 | 17.547 % | c | 32893 | 37181 129309 | 24150 11012 216824 19.7 | 17.547 % | c | 34602 | 37181 129309 | 26565 12721 262463 20.6 | 17.547 % | c ============================================================================== c [1mFound solution: 16520[0m c ---[ 0]---> BDD-cost: 9 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 35592 | 37192 129333 | 12397 13711 293702 21.4 | 17.547 % | c | 35692 | 37192 129333 | 13636 13811 294721 21.3 | 17.551 % | c | 35842 | 37192 129333 | 15000 13961 297442 21.3 | 17.551 % | c | 36069 | 37192 129333 | 16500 14188 300629 21.2 | 17.551 % | c | 36407 | 37192 129333 | 18150 14526 309396 21.3 | 17.551 % | c | 36914 | 37192 129333 | 19965 15033 324455 21.6 | 17.551 % | c ============================================================================== c [1mFound solution: 15496[0m c ---[ 0]---> BDD-cost: 4 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 37582 | 36812 128207 | 12270 15624 334459 21.4 | 17.551 % | c | 37683 | 36812 128207 | 13497 7913 167346 21.1 | 18.984 % | c | 37833 | 36812 128207 | 14846 8063 168686 20.9 | 18.984 % | c | 38060 | 36812 128207 | 16331 8290 171955 20.7 | 18.984 % | c | 38397 | 36812 128207 | 17964 8627 186378 21.6 | 18.984 % | c | 38905 | 36812 128207 | 19760 9135 199250 21.8 | 18.984 % | c | 39665 | 36812 128207 | 21737 9895 223851 22.6 | 18.984 % | c | 40806 | 36812 128207 | 23910 11036 267122 24.2 | 18.984 % | c | 42514 | 36812 128207 | 26301 12744 328129 25.7 | 18.984 % | c | 45076 | 36812 128207 | 28932 15306 412358 26.9 | 18.984 % | c ============================================================================== c [1mFound solution: 15492[0m c ---[ 0]---> BDD-cost: 7 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 46273 | 36819 128226 | 12273 16503 446142 27.0 | 18.984 % | c | 46375 | 36819 128226 | 13500 8354 218481 26.2 | 18.987 % | c | 46525 | 36819 128226 | 14850 8504 219448 25.8 | 18.987 % | c | 46750 | 36819 128226 | 16335 8729 223297 25.6 | 18.987 % | c | 47087 | 36819 128226 | 17968 9066 231276 25.5 | 18.987 % | c | 47593 | 36819 128226 | 19765 9572 242126 25.3 | 18.987 % | c | 48352 | 36819 128226 | 21742 10331 266491 25.8 | 18.987 % | c | 49491 | 36819 128226 | 23916 11470 301953 26.3 | 18.987 % | c | 51199 | 36819 128226 | 26308 13178 372554 28.3 | 18.987 % | c | 53761 | 36819 128226 | 28939 15740 465301 29.6 | 18.987 % | c ============================================================================== c [1mFound solution: 14516[0m c ---[ 0]---> BDD-cost: 6 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 56057 | 36825 128242 | 12275 18036 539152 29.9 | 18.987 % | c | 56157 | 36825 128242 | 13502 9118 270230 29.6 | 18.992 % | c | 56309 | 36825 128242 | 14852 9270 273833 29.5 | 18.992 % | c | 56534 | 36825 128242 | 16338 9495 275433 29.0 | 18.992 % | c | 56871 | 36825 128242 | 17971 9832 280944 28.6 | 18.992 % | c | 57377 | 36825 128242 | 19769 10338 292852 28.3 | 18.992 % | c | 58136 | 36825 128242 | 21745 11097 321161 28.9 | 18.992 % | c | 59276 | 36825 128242 | 23920 12237 362408 29.6 | 18.992 % | c | 60985 | 36825 128242 | 26312 13946 413995 29.7 | 18.992 % | c | 63548 | 36825 128242 | 28943 16509 509356 30.9 | 18.992 % | c | 67394 | 36825 128242 | 31838 20355 665859 32.7 | 18.992 % | c | 73160 | 36825 128242 | 35022 26121 926100 35.5 | 18.992 % | c ============================================================================== c [1mFound solution: 14452[0m c ---[ 0]---> BDD-cost: 5 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 74281 | 36829 128253 | 12276 27242 956014 35.1 | 18.992 % | c | 74381 | 36829 128253 | 13503 12868 470218 36.5 | 18.999 % | c | 74531 | 36829 128253 | 14853 13018 471153 36.2 | 18.999 % | c | 74756 | 36829 128253 | 16339 13243 474383 35.8 | 18.999 % | c | 75095 | 36829 128253 | 17973 13582 482641 35.5 | 18.999 % | c | 75602 | 36829 128253 | 19770 14089 494660 35.1 | 18.999 % | c | 76361 | 36829 128253 | 21747 14848 510233 34.4 | 18.999 % | c | 77501 | 36829 128253 | 23922 15988 537418 33.6 | 18.999 % | c | 79209 | 36829 128253 | 26314 17696 580456 32.8 | 18.999 % | c | 81772 | 36829 128253 | 28946 20259 667461 32.9 | 18.999 % | c | 85618 | 36829 128253 | 31840 24105 781852 32.4 | 18.999 % | c | 91385 | 36829 128253 | 35024 29872 993586 33.3 | 18.999 % | c ============================================================================== c [1mFound solution: 14428[0m c ---[ 0]---> BDD-cost: 6 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 95801 | 36834 128266 | 12278 34288 1184646 34.5 | 18.999 % | c | 95903 | 36834 128266 | 13505 7065 213373 30.2 | 19.007 % | c | 96055 | 36834 128266 | 14856 7217 216410 30.0 | 19.007 % | c | 96280 | 36834 128266 | 16342 7442 218148 29.3 | 19.007 % | c | 96618 | 36834 128266 | 17976 7780 224906 28.9 | 19.007 % | c | 97124 | 36834 128266 | 19773 8286 238918 28.8 | 19.007 % | c | 97885 | 36834 128266 | 21751 9047 260057 28.7 | 19.007 % | c ============================================================================== c [1mFound solution: 13724[0m c ---[ 0]---> BDD-cost: 8 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 98124 | 36843 128289 | 12281 9286 264979 28.5 | 19.007 % | c | 98224 | 36843 128289 | 13509 9386 265508 28.3 | 19.005 % | c | 98374 | 36843 128289 | 14860 9536 267139 28.0 | 19.005 % | c | 98601 | 36843 128289 | 16346 9763 270535 27.7 | 19.005 % | c | 98939 | 36843 128289 | 17980 10101 275717 27.3 | 19.005 % | c | 99447 | 36843 128289 | 19778 10609 293159 27.6 | 19.005 % | c | 100207 | 36843 128289 | 21756 11369 304277 26.8 | 19.005 % | c | 101348 | 36843 128289 | 23932 12510 334789 26.8 | 19.005 % | c ============================================================================== c [1mFound solution: 13644[0m c ---[ 0]---> BDD-cost: 6 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 101688 | 36852 128311 | 12284 12850 342245 26.6 | 19.005 % | c | 101789 | 36852 128311 | 13512 12951 342884 26.5 | 19.003 % | c | 101940 | 36852 128311 | 14863 13102 343846 26.2 | 19.003 % | c | 102166 | 36845 128288 | 16350 13327 347272 26.1 | 19.015 % | c | 102503 | 36845 128288 | 17985 13664 353135 25.8 | 19.015 % | c | 103010 | 36845 128288 | 19783 14171 365913 25.8 | 19.015 % | c | 103769 | 36845 128288 | 21761 14930 388571 26.0 | 19.015 % | c | 104909 | 36845 128288 | 23938 16070 421710 26.2 | 19.015 % | c | 106617 | 36845 128288 | 26331 17778 484189 27.2 | 19.015 % | c | 109179 | 36845 128288 | 28965 20340 575241 28.3 | 19.015 % | c ============================================================================== c [1mFound solution: 12572[0m c ---[ 0]---> BDD-cost: 7 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 111904 | 36853 128307 | 12284 23065 672026 29.1 | 19.015 % | c | 112006 | 36853 128307 | 13512 11635 320975 27.6 | 19.018 % | c | 112156 | 36853 128307 | 14863 11785 324077 27.5 | 19.018 % | c | 112381 | 36853 128307 | 16350 12010 328289 27.3 | 19.018 % | c | 112719 | 36853 128307 | 17985 12348 336145 27.2 | 19.018 % | c | 113226 | 36853 128307 | 19783 12855 345644 26.9 | 19.018 % | c | 113986 | 36853 128307 | 21761 13615 371037 27.3 | 19.018 % | c | 115127 | 36853 128307 | 23938 14756 404373 27.4 | 19.018 % | c | 116835 | 36853 128307 | 26331 16464 461239 28.0 | 19.018 % | c | 119398 | 36853 128307 | 28965 19027 545495 28.7 | 19.018 % | c | 123242 | 36853 128307 | 31861 22871 639038 27.9 | 19.018 % | c | 129010 | 36853 128307 | 35047 28639 882207 30.8 | 19.018 % | c | 137660 | 36853 128307 | 38552 13830 485312 35.1 | 19.018 % | c | 150634 | 36853 128307 | 42407 26804 1127282 42.1 | 19.018 % | c | 170096 | 36853 128307 | 46648 15068 588063 39.0 | 19.018 % | c ============================================================================== c [1mFound solution: 12564[0m c ---[ 0]---> BDD-cost: 7 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 171077 | 36861 128326 | 12287 16049 612333 38.2 | 19.018 % | c | 171178 | 36861 128326 | 13515 8126 296422 36.5 | 19.021 % | c | 171328 | 36861 128326 | 14867 8276 297256 35.9 | 19.021 % | c | 171553 | 36861 128326 | 16353 8501 302353 35.6 | 19.021 % | c | 171890 | 36861 128326 | 17989 8838 306531 34.7 | 19.021 % | c | 172397 | 36861 128326 | 19788 9345 318405 34.1 | 19.021 % | c | 173157 | 36861 128326 | 21767 10105 329823 32.6 | 19.021 % | c | 174296 | 36861 128326 | 23943 11244 367773 32.7 | 19.021 % | c | 176005 | 36861 128326 | 26338 12953 419145 32.4 | 19.021 % | c ============================================================================== c [1mFound solution: 12380[0m c ---[ 0]---> BDD-cost: 3 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 176994 | 36864 128334 | 12288 13942 439645 31.5 | 19.021 % | c | 177094 | 36864 128334 | 13516 7071 152283 21.5 | 19.028 % | c | 177244 | 36864 128334 | 14868 7221 153279 21.2 | 19.028 % | c | 177469 | 36864 128334 | 16355 7446 155909 20.9 | 19.028 % | c | 177808 | 36864 128334 | 17990 7785 163986 21.1 | 19.028 % | c | 178314 | 36864 128334 | 19789 8291 180208 21.7 | 19.028 % | c | 179074 | 36864 128334 | 21768 9051 199445 22.0 | 19.028 % | c | 180213 | 36864 128334 | 23945 10190 243214 23.9 | 19.028 % | c | 181922 | 36864 128334 | 26340 11899 290182 24.4 | 19.028 % | c | 184484 | 36864 128334 | 28974 14461 377967 26.1 | 19.028 % | c | 188329 | 36864 128334 | 31871 18306 538763 29.4 | 19.028 % | c | 194096 | 36864 128334 | 35059 24073 731057 30.4 | 19.028 % | c | 202745 | 36864 128334 | 38565 32722 1000173 30.6 | 19.028 % | c | 215719 | 36864 128334 | 42421 18645 716290 38.4 | 19.028 % | c | 235182 | 36864 128334 | 46663 38108 1426096 37.4 | 19.028 % | c | 264375 | 36864 128334 | 51330 32704 1699302 52.0 | 19.028 % | c ============================================================================== c [1mFound solution: 12376[0m c ---[ 0]---> BDD-cost: 9 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 287208 | 36875 128360 | 12291 16661 884812 53.1 | 19.028 % | c | 287310 | 36875 128360 | 13520 8433 371193 44.0 | 19.029 % | c | 287460 | 36875 128360 | 14872 8583 373817 43.6 | 19.029 % | c | 287685 | 36875 128360 | 16359 8808 377028 42.8 | 19.029 % | c | 288022 | 36875 128360 | 17995 9145 379856 41.5 | 19.029 % | c | 288529 | 36875 128360 | 19794 9652 386997 40.1 | 19.029 % | c | 289288 | 36875 128360 | 21774 10411 417070 40.1 | 19.029 % | c | 290427 | 36875 128360 | 23951 11550 453289 39.2 | 19.029 % | c | 292136 | 36875 128360 | 26346 13259 501736 37.8 | 19.029 % | c | 294699 | 36875 128360 | 28981 15822 607437 38.4 | 19.029 % | c | 298543 | 36875 128360 | 31879 19666 754415 38.4 | 19.029 % | c | 304309 | 36875 128360 | 35067 25432 976585 38.4 | 19.029 % | c | 312958 | 36875 128360 | 38574 34081 1371811 40.3 | 19.029 % | c ============================================================================== c [1mFound solution: 12352[0m c ---[ 0]---> BDD-cost: 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 319353 | 36882 128376 | 12294 40476 1598657 39.5 | 19.029 % | c | 319453 | 36882 128376 | 13523 7082 205798 29.1 | 19.036 % | c | 319604 | 36882 128376 | 14875 7233 206704 28.6 | 19.036 % | c | 319829 | 36882 128376 | 16363 7458 209007 28.0 | 19.036 % | c | 320166 | 36882 128376 | 17999 7795 215612 27.7 | 19.036 % | c | 320674 | 36882 128376 | 19799 8303 223348 26.9 | 19.036 % | c | 321433 | 36882 128376 | 21779 9062 250219 27.6 | 19.036 % | c | 322572 | 36882 128376 | 23957 10201 282129 27.7 | 19.036 % | c | 324282 | 36882 128376 | 26353 11911 358349 30.1 | 19.036 % | c | 326844 | 36882 128376 | 28988 14473 441330 30.5 | 19.036 % | c | 330689 | 36882 128376 | 31887 18318 589478 32.2 | 19.036 % | c | 336455 | 36882 128376 | 35076 24084 823104 34.2 | 19.036 % | c | 345104 | 36882 128376 | 38583 32733 1226373 37.5 | 19.036 % | c | 358078 | 36882 128376 | 42442 19067 786517 41.3 | 19.036 % | c | 377539 | 36882 128376 | 46686 38528 1589767 41.3 | 19.036 % | c ============================================================================== c [1mFound solution: 12308[0m c ---[ 0]---> BDD-cost: 6 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 404877 | 36888 128390 | 12296 31387 1372032 43.7 | 19.036 % | c | 404977 | 36888 128390 | 13525 13898 517090 37.2 | 19.043 % | c | 405128 | 36888 128390 | 14878 14049 518096 36.9 | 19.043 % | c | 405354 | 36888 128390 | 16365 14275 522256 36.6 | 19.043 % | c | 405691 | 36888 128390 | 18002 14612 528261 36.2 | 19.043 % | c | 406200 | 36888 128390 | 19802 15121 540334 35.7 | 19.043 % | c | 406959 | 36888 128390 | 21783 15880 563197 35.5 | 19.043 % | c | 408100 | 36888 128390 | 23961 17021 592453 34.8 | 19.043 % | c | 409808 | 36888 128390 | 26357 18729 659724 35.2 | 19.043 % | c | 412372 | 36888 128390 | 28993 21293 746976 35.1 | 19.043 % | c | 416216 | 36888 128390 | 31892 25137 891860 35.5 | 19.043 % | c | 421982 | 36888 128390 | 35081 30903 1112849 36.0 | 19.043 % | c | 430632 | 36888 128390 | 38590 15691 553318 35.3 | 19.043 % | c ============================================================================== c [1mFound solution: 12304[0m c ---[ 0]---> BDD-cost: 9 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 435245 | 36897 128410 | 12299 20304 714432 35.2 | 19.043 % | c | 435345 | 36897 128410 | 13528 10252 334706 32.6 | 19.050 % | c | 435497 | 36897 128410 | 14881 10404 335682 32.3 | 19.050 % | c | 435722 | 36897 128410 | 16369 10629 340217 32.0 | 19.050 % | c | 436060 | 36897 128410 | 18006 10967 344797 31.4 | 19.050 % | c | 436566 | 36897 128410 | 19807 11473 352241 30.7 | 19.050 % | c | 437325 | 36897 128410 | 21788 12232 372264 30.4 | 19.050 % | c | 438466 | 36897 128410 | 23967 13373 405058 30.3 | 19.050 % | c | 440174 | 36897 128410 | 26363 15081 464949 30.8 | 19.050 % | c | 442738 | 36897 128410 | 29000 17645 587210 33.3 | 19.050 % | c | 446583 | 36897 128410 | 31900 21490 740992 34.5 | 19.050 % | c | 452351 | 36897 128410 | 35090 27258 975686 35.8 | 19.050 % | c ============================================================================== c [1mFound solution: 12300[0m c ---[ 0]---> BDD-cost: 7 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 459893 | 36904 128426 | 12301 34800 1269525 36.5 | 19.050 % | c | 459994 | 36904 128426 | 13531 12782 465076 36.4 | 19.058 % | c | 460144 | 36904 128426 | 14884 12932 466107 36.0 | 19.058 % | c | 460370 | 36904 128426 | 16372 13158 470093 35.7 | 19.058 % | c | 460707 | 36904 128426 | 18009 13495 478617 35.5 | 19.058 % | c | 461215 | 36904 128426 | 19810 14003 491629 35.1 | 19.058 % | c | 461974 | 36904 128426 | 21791 14762 524771 35.5 | 19.058 % | c | 463113 | 36904 128426 | 23971 15901 560101 35.2 | 19.058 % | c | 464822 | 36904 128426 | 26368 17610 611527 34.7 | 19.058 % | c | 467385 | 36904 128426 | 29005 20173 701515 34.8 | 19.058 % | c | 471229 | 36904 128426 | 31905 24017 834838 34.8 | 19.058 % | c | 476996 | 36904 128426 | 35096 29784 1055919 35.5 | 19.058 % | c | 485645 | 36904 128426 | 38605 13465 445759 33.1 | 19.058 % | c | 498619 | 36904 128426 | 42466 26439 986258 37.3 | 19.058 % | c ============================================================================== c [1mFound solution: 12296[0m c ---[ 0]---> BDD-cost: 7 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 500304 | 36911 128442 | 12303 28124 1044146 37.1 | 19.058 % | c | 500405 | 36911 128442 | 13533 12951 474327 36.6 | 19.065 % | c | 500556 | 36911 128442 | 14886 13102 475139 36.3 | 19.065 % | c | 500782 | 36911 128442 | 16375 13328 479053 35.9 | 19.065 % | c | 501119 | 36911 128442 | 18012 13665 492568 36.0 | 19.065 % | c | 501625 | 36911 128442 | 19814 14171 498742 35.2 | 19.065 % | c | 502385 | 36911 128442 | 21795 14931 522892 35.0 | 19.065 % | c | 503524 | 36911 128442 | 23975 16070 560981 34.9 | 19.065 % | c | 505232 | 36911 128442 | 26372 17778 621666 35.0 | 19.065 % | c | 507795 | 36911 128442 | 29009 20341 724349 35.6 | 19.065 % | c | 511639 | 36911 128442 | 31910 24185 892062 36.9 | 19.065 % | c | 517405 | 36911 128442 | 35101 29951 1120245 37.4 | 19.065 % | c | 526054 | 36911 128442 | 38612 14957 555573 37.1 | 19.065 % | c ============================================================================== c [1mFound solution: 12292[0m c ---[ 0]---> BDD-cost: 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 538824 | 36918 128458 | 12306 27727 1041990 37.6 | 19.065 % | c | 538925 | 36918 128458 | 13536 13300 445778 33.5 | 19.072 % | c | 539075 | 36918 128458 | 14890 13450 447494 33.3 | 19.072 % | c | 539300 | 36918 128458 | 16379 13675 451225 33.0 | 19.072 % | c | 539638 | 36918 128458 | 18017 14013 454258 32.4 | 19.072 % | c | 540144 | 36918 128458 | 19818 14519 466428 32.1 | 19.072 % | c | 540903 | 36918 128458 | 21800 15278 485291 31.8 | 19.072 % | c | 542042 | 36918 128458 | 23980 16417 509433 31.0 | 19.072 % | c | 543752 | 36918 128458 | 26379 18127 568529 31.4 | 19.072 % | c | 546316 | 36918 128458 | 29016 20691 665788 32.2 | 19.072 % | c | 550164 | 36918 128458 | 31918 24539 807746 32.9 | 19.072 % | c ============================================================================== c [1mFound solution: 12288[0m c ---[ 0]---> BDD-cost: 1 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 553313 | 36919 128461 | 12306 27688 901704 32.6 | 19.072 % | c | 553413 | 36919 128461 | 13536 13355 399236 29.9 | 19.082 % | c | 553564 | 36919 128461 | 14890 13506 402397 29.8 | 19.082 % | c | 553790 | 36919 128461 | 16379 13732 408434 29.7 | 19.082 % | c | 554127 | 36919 128461 | 18017 14069 413835 29.4 | 19.082 % | c | 554634 | 36919 128461 | 19818 14576 428619 29.4 | 19.082 % | c | 555394 | 36919 128461 | 21800 15336 453713 29.6 | 19.082 % | c | 556533 | 36919 128461 | 23980 16475 501139 30.4 | 19.082 % | c ============================================================================== c [1mFound solution: 11308[0m c ---[ 0]---> BDD-cost: 4 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 557161 | 36925 128476 | 12308 17103 519226 30.4 | 19.082 % | c | 557261 | 36925 128476 | 13538 8652 216099 25.0 | 19.084 % | c | 557412 | 36925 128476 | 14892 8803 217982 24.8 | 19.084 % | c | 557637 | 36925 128476 | 16381 9028 220294 24.4 | 19.084 % | c | 557975 | 36925 128476 | 18020 9366 227457 24.3 | 19.084 % | c | 558481 | 36925 128476 | 19822 9872 233513 23.7 | 19.084 % | c | 559242 | 36925 128476 | 21804 10633 258958 24.4 | 19.084 % | c | 560381 | 36925 128476 | 23984 11772 289947 24.6 | 19.084 % | c | 562090 | 36925 128476 | 26383 13481 368252 27.3 | 19.084 % | c | 564652 | 36925 128476 | 29021 16043 452259 28.2 | 19.084 % | c | 568496 | 36925 128476 | 31923 19887 583420 29.3 | 19.084 % | c ============================================================================== c [1mFound solution: 10840[0m c ---[ 0]---> BDD-cost: 5 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 571855 | 36935 128499 | 12311 23246 708088 30.5 | 19.084 % | c | 571956 | 36935 128499 | 13542 11724 342079 29.2 | 19.083 % | c | 572107 | 36935 128499 | 14896 11875 343548 28.9 | 19.083 % | c | 572332 | 36935 128499 | 16385 12100 346793 28.7 | 19.083 % | c | 572669 | 36935 128499 | 18024 12437 352077 28.3 | 19.083 % | c | 573176 | 36935 128499 | 19826 12944 363266 28.1 | 19.083 % | c | 573936 | 36935 128499 | 21809 13704 382290 27.9 | 19.083 % | c | 575075 | 36935 128499 | 23990 14843 428729 28.9 | 19.083 % | c | 576784 | 36935 128499 | 26389 16552 488127 29.5 | 19.083 % | c | 579347 | 36935 128499 | 29028 19115 583719 30.5 | 19.083 % | c | 583191 | 36935 128499 | 31931 22959 720947 31.4 | 19.083 % | c | 588957 | 36935 128499 | 35124 28725 949541 33.1 | 19.083 % | c | 597606 | 36935 128499 | 38637 13848 527370 38.1 | 19.083 % | c | 610581 | 36935 128499 | 42500 26823 1067082 39.8 | 19.083 % | c ============================================================================== c [1mFound solution: 10524[0m c ---[ 0]---> BDD-cost: 3 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 617925 | 36942 128515 | 12314 34167 1322141 38.7 | 19.083 % | c | 618026 | 36942 128515 | 13545 13741 477183 34.7 | 19.085 % | c | 618176 | 36942 128515 | 14899 13891 478333 34.4 | 19.085 % | c | 618401 | 36942 128515 | 16389 14116 481586 34.1 | 19.085 % | c | 618739 | 36942 128515 | 18028 14454 484344 33.5 | 19.085 % | c | 619245 | 36942 128515 | 19831 14960 497601 33.3 | 19.085 % | c | 620005 | 36942 128515 | 21815 15720 515760 32.8 | 19.085 % | c | 621145 | 36942 128515 | 23996 16860 554466 32.9 | 19.085 % | c | 622853 | 36942 128515 | 26396 18568 602863 32.5 | 19.085 % | c | 625417 | 36942 128515 | 29035 21132 711495 33.7 | 19.085 % | c | 629261 | 36942 128515 | 31939 24976 882134 35.3 | 19.085 % | c ============================================================================== c [1mFound solution: 10520[0m c ---[ 0]---> BDD-cost: 8 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 633363 | 36953 128540 | 12317 29078 1040042 35.8 | 19.085 % | c | 633463 | 36953 128540 | 13548 12992 465138 35.8 | 19.084 % | c | 633614 | 36953 128540 | 14903 13143 466619 35.5 | 19.084 % | c | 633839 | 36953 128540 | 16393 13368 471791 35.3 | 19.084 % | c | 634177 | 36953 128540 | 18033 13706 476213 34.7 | 19.084 % | c | 634683 | 36953 128540 | 19836 14212 487566 34.3 | 19.084 % | c | 635442 | 36953 128540 | 21820 14971 508943 34.0 | 19.084 % | c | 636581 | 36953 128540 | 24002 16110 552250 34.3 | 19.084 % | c | 638289 | 36953 128540 | 26402 17818 607599 34.1 | 19.084 % | c | 640851 | 36953 128540 | 29042 20380 686359 33.7 | 19.084 % | c | 644695 | 36953 128540 | 31947 24224 830966 34.3 | 19.084 % | c | 650461 | 36953 128540 | 35141 29990 1086221 36.2 | 19.084 % | c | 659111 | 36953 128540 | 38656 14286 613779 43.0 | 19.084 % | c | 672085 | 36953 128540 | 42521 27260 1168557 42.9 | 19.084 % | c | 691548 | 36953 128540 | 46773 16332 665480 40.7 | 19.084 % | c | 720740 | 36953 128540 | 51451 45524 1969401 43.3 | 19.084 % | c | 764529 | 36953 128540 | 56596 49182 2478158 50.4 | 19.084 % | c c *** TERMINATED *** s SATISFIABLE v -x1_bit_7 -x1_bit_6 -x1_bit_5 x1_bit_4 x1_bit_3 -x1_bit_2 -x1_bit_1 -x1_bit0 x1_bit1 -x1_bit2 -x1_bit3 x1_bit4 -x1_bit5 x1_bit6 -x1_bit7 -x1_bit8 -x1_bit9 -x1_bit10 -x1_bit11 -x1_bit12 -x2_bit0 -x3_bit0 x4_bit0 x5_bit0 x6_bit0 -x7_bit0 x8_bit0 -x9_bit0 -x10_bit0 -x11_bit0 x12_bit0 -x13_bit0 -x14_bit0 -x15_bit0 -x16_bit0 x17_bit0 x18_bit0 -x19_bit0 x20_bit0 -x21_bit0 -x22_bit0 -x23_bit0 x24_bit0 x25_bit0 -x26_bit0 x27_bit0 -x28_bit0 -x29_bit0 -x30_bit0 x31_bit0 -x32_bit0 -x33_bit0 -x34_bit0 x35_bit0 x36_bit0 -x37_bit0 x38_bit0 -x39_bit0 -x40_bit0 -x41_bit0 x42_bit0 x43_bit0 x44_bit0 x45_bit0 -x46_bit0 x47_bit0 x48_bit0 -x49_bit0 x50_bit0 -x51_bit0 -x52_bit0 -x53_bit0 -x54_bit0 x55_bit0 x56_bit0 -x57_bit_7 -x57_bit_6 -x57_bit_5 -x57_bit_4 -x57_bit_3 -x57_bit_2 -x57_bit_1 -x57_bit0 -x57_bit1 x57_bit2 -x57_bit3 x57_bit4 -x57_bit5 -x57_bit6 -x57_bit7 -x57_bit8 -x57_bit9 -x57_bit10 -x57_bit11 -x57_bit12 -x58_bit_7 -x58_bit_6 -x58_bit_5 -x58_bit_4 -x58_bit_3 -x58_bit_2 -x58_bit_1 x58_bit0 x58_bit1 -x58_bit2 -x58_bit3 x58_bit4 x58_bit5 -x58_bit6 -x58_bit7 -x58_bit8 -x58_bit9 -x58_bit10 -x58_bit11 -x58_bit12 -x75_bit_7 -x75_bit_6 -x75_bit_5 -x75_bit_4 -x75_bit_3 -x75_bit_2 -x75_bit_1 -x75_bit0 -x75_bit1 -x75_bit2 x75_bit3 -x75_bit4 -x75_bit5 -x75_bit6 -x75_bit7 -x75_bit8 -x75_bit9 -x75_bit10 -x75_bit11 -x75_bit12 -x76_bit_7 -x76_bit_6 -x76_bit_5 -x76_bit_4 -x76_bit_3 -x76_bit_2 -x76_bit_1 x76_bit0 -x76_bit1 -x76_bit2 -x76_bit3 x76_bit4 -x76_bit5 x76_bit6 -x76_bit7 -x76_bit8 -x76_bit9 -x76_bit10 -x76_bit11 -x76_bit12 -x77_bit_7 -x77_bit_6 -x77_bit_5 -x77_bit_4 -x77_bit_3 -x77_bit_2 -x77_bit_1 -x77_bit0 -x77_bit1 -x77_bit2 -x77_bit3 x77_bit4 x77_bit5 -x77_bit6 -x77_bit7 -x77_bit8 -x77_bit9 -x77_bit10 -x77_bit11 -x77_bit12 -x78_bit_7 -x78_bit_6 -x78_bit_5 -x78_bit_4 -x78_bit_3 -x78_bit_2 -x78_bit_1 x78_bit0 -x78_bit1 x78_bit2 x78_bit3 -x78_bit4 -x78_bit5 -x78_bit6 -x78_bit7 -x78_bit8 -x78_bit9 -x78_bit10 -x78_bit11 -x78_bit12 -x79_bit_7 -x79_bit_6 -x79_bit_5 -x79_bit_4 -x79_bit_3 -x79_bit_2 -x79_bit_1 -x79_bit0 x79_bit1 -x79_bit2 x79_bit3 x79_bit4 -x79_bit5 -x79_bit6 -x79_bit7 -x79_bit8 -x79_bit9 -x79_bit10 -x79_bit11 -x79_bit12 -x80_bit_7 -x80_bit_6 -x80_bit_5 -x80_bit_4 -x80_bit_3 -x80_bit_2 -x80_bit_1 x80_bit0 -x80_bit1 x80_bit2 -x80_bit3 -x80_bit4 -x80_bit5 x80_bit6 -x80_bit7 -x80_bit8 -x80_bit9 -x80_bit10 -x80_bit11 -x80_bit12 -x81_bit_7 -x81_bit_6 -x81_bit_5 -x81_bit_4 -x81_bit_3 -x81_bit_2 -x81_bit_1 x81_bit0 -x81_bit1 -x81_bit2 -x81_bit3 x81_bit4 -x81_bit5 -x81_bit6 -x81_bit7 -x81_bit8 -x81_bit9 -x81_bit10 -x81_bit11 -x81_bit12 -x82_bit_7 -x82_bit_6 -x82_bit_5 -x82_bit_4 -x82_bit_3 -x82_bit_2 -x82_bit_1 -x82_bit0 -x82_bit1 -x82_bit2 x82_bit3 -x82_bit4 -x82_bit5 x82_bit6 -x82_bit7 -x82_bit8 -x82_bit9 -x82_bit10 -x82_bit11 -x82_bit12 -x83_bit_7 -x83_bit_6 -x83_bit_5 -x83_bit_4 -x83_bit_3 -x83_bit_2 -x83_bit_1 -x83_bit0 x83_bit1 x83_bit2 -x83_bit3 -x83_bit4 -x83_bit5 x83_bit6 -x83_bit7 -x83_bit8 -x83_bit9 -x83_bit10 -x83_bit11 -x83_bit12 -x84_bit_7 -x84_bit_6 -x84_bit_5 -x84_bit_4 -x84_bit_3 -x84_bit_2 -x84_bit_1 x84_bit0 -x84_bit1 -x84_bit2 x84_bit3 x84_bit4 x84_bit5 -x84_bit6 -x84_bit7 -x84_bit8 -x84_bit9 -x84_bit10 -x84_bit11 -x84_bit12 -x85_bit_7 -x85_bit_6 -x85_bit_5 -x85_bit_4 -x85_bit_3 -x85_bit_2 -x85_bit_1 -x85_bit0 x85_bit1 -x85_bit2 -x85_bit3 -x85_bit4 x85_bit5 -x85_bit6 -x85_bit7 -x85_bit8 -x85_bit9 -x85_bit10 -x85_bit11 -x85_bit12 -x86_bit_7 -x86_bit_6 -x86_bit_5 -x86_bit_4 -x86_bit_3 -x86_bit_2 -x86_bit_1 -x86_bit0 -x86_bit1 -x86_bit2 -x86_bit3 x86_bit4 x86_bit5 -x86_bit6 -x86_bit7 -x86_bit8 -x86_bit9 -x86_bit10 -x86_bit11 -x86_bit12 -x59_bit_7 -x59_bit_6 -x59_bit_5 -x59_bit_4 -x59_bit_3 -x59_bit_2 -x59_bit_1 -x59_bit0 x59_bit1 -x59_bit2 -x59_bit3 -x59_bit4 -x59_bit5 -x59_bit6 -x59_bit7 -x59_bit8 -x59_bit9 -x59_bit10 -x59_bit11 -x59_bit12 -x60_bit_7 -x60_bit_6 -x60_bit_5 -x60_bit_4 -x60_bit_3 -x60_bit_2 -x60_bit_1 -x60_bit0 -x60_bit1 -x60_bit2 -x60_bit3 -x60_bit4 -x60_bit5 -x60_bit6 -x60_bit7 -x60_bit8 -x60_bit9 -x60_bit10 -x60_bit11 -x60_bit12 -x61_bit_7 -x61_bit_6 -x61_bit
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/21054/stat): 21054 (minisat+_script) R 21053 21054 20115 0 -1 0 19 0 0 0 0 0 0 0 23 0 1 0 1855448975 712704 3 4294967295 134512640 135087896 3221224512 3221224512 1073744960 0 0 5 0 0 0 0 17 0 0 0 Raw data (/proc/21054/statm): 174 3 169 147 0 27 0 [pid=21054] 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=21055 New process pid=21056 New process pid=21057 execve syscall for /bin/sed executable One traced child (pid=21056) 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=21057) exited with status: 0 One traced child (pid=21055) exited with status: 0 New process pid=21058 execve syscall for /oldhome/oroussel/solvers/minisat+_64-bit_static executable open syscall for file /dev/null open syscall for file /oldhome/oroussel/tmp/wulflinc28/normalized-mps-v2-13-7-pk1.opb [startup+10.0042 s] Raw data (loadavg): 0.87 0.95 0.90 2/57 21058 Raw data (/proc/21054/stat): 21054 (minisat+_script) S 21053 21054 20115 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855448975 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/21054/statm): 531 226 485 147 0 384 0 [pid=21054] vsize: 2124 Raw data (/proc/21058/stat): 21058 (minisat+_64-bit) R 21054 21054 20115 0 -1 0 1329 0 0 0 982 6 0 0 25 0 1 0 1855448980 5672960 1280 4294967295 134512640 135094434 3221224448 3221223108 134553482 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/21058/statm): 1385 1280 145 145 0 1240 0 [pid=21058] vsize: 5540 Current children cumulated CPU time (s) 9.88 Current children cumulated vsize (Kb) 7664 [startup+20.0049 s] Raw data (loadavg): 0.89 0.96 0.91 2/57 21058 Raw data (/proc/21054/stat): 21054 (minisat+_script) S 21053 21054 20115 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855448975 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/21054/statm): 531 226 485 147 0 384 0 [pid=21054] vsize: 2124 Raw data (/proc/21058/stat): 21058 (minisat+_64-bit) R 21054 21054 20115 0 -1 0 1475 0 0 0 1979 7 0 0 25 0 1 0 1855448980 6643712 1426 4294967295 134512640 135094434 3221224448 3221223236 134553446 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/21058/statm): 1622 1426 145 145 0 1477 0 [pid=21058] vsize: 6488 Current children cumulated CPU time (s) 19.86 Current children cumulated vsize (Kb) 8612 [startup+30.0065 s] Raw data (loadavg): 0.91 0.96 0.91 2/57 21058 Raw data (/proc/21054/stat): 21054 (minisat+_script) S 21053 21054 20115 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855448975 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/21054/statm): 531 226 485 147 0 384 0 [pid=21054] vsize: 2124 Raw data (/proc/21058/stat): 21058 (minisat+_64-bit) R 21054 21054 20115 0 -1 0 1585 0 0 0 2976 8 0 0 25 0 1 0 1855448980 7086080 1536 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/21058/statm): 1730 1536 145 145 0 1585 0 [pid=21058] vsize: 6920 Current children cumulated CPU time (s) 29.84 Current children cumulated vsize (Kb) 9044 [startup+40.0072 s] Raw data (loadavg): 0.92 0.96 0.91 2/57 21058 Raw data (/proc/21054/stat): 21054 (minisat+_script) S 21053 21054 20115 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855448975 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/21054/statm): 531 226 485 147 0 384 0 [pid=21054] vsize: 2124 Raw data (/proc/21058/stat): 21058 (minisat+_64-bit) R 21054 21054 20115 0 -1 0 1783 0 0 0 3971 11 0 0 25 0 1 0 1855448980 7897088 1734 4294967295 134512640 135094434 3221224448 3221223104 134558225 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/21058/statm): 1928 1734 145 145 0 1783 0 [pid=21058] vsize: 7712 Current children cumulated CPU time (s) 39.82 Current children cumulated vsize (Kb) 9836 [startup+50.0079 s] Raw data (loadavg): 0.93 0.96 0.91 2/57 21058 Raw data (/proc/21054/stat): 21054 (minisat+_script) S 21053 21054 20115 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855448975 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/21054/statm): 531 226 485 147 0 384 0 [pid=21054] vsize: 2124 Raw data (/proc/21058/stat): 21058 (minisat+_64-bit) R 21054 21054 20115 0 -1 0 1967 0 0 0 4968 12 0 0 25 0 1 0 1855448980 8704000 1918 4294967295 134512640 135094434 3221224448 3221223040 134557398 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/21058/statm): 2125 1918 145 145 0 1980 0 [pid=21058] vsize: 8500 Current children cumulated CPU time (s) 49.8 Current children cumulated vsize (Kb) 10624 [startup+60.0096 s] Raw data (loadavg): 0.94 0.96 0.91 2/57 21058 Raw data (/proc/21054/stat): 21054 (minisat+_script) S 21053 21054 20115 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855448975 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/21054/statm): 531 226 485 147 0 384 0 [pid=21054] vsize: 2124 Raw data (/proc/21058/stat): 21058 (minisat+_64-bit) R 21054 21054 20115 0 -1 0 2110 0 0 0 5966 13 0 0 25 0 1 0 1855448980 9281536 2061 4294967295 134512640 135094434 3221224448 3221223104 134557813 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/21058/statm): 2266 2061 145 145 0 2121 0 [pid=21058] vsize: 9064 Current children cumulated CPU time (s) 59.79 Current children cumulated vsize (Kb) 11188 [startup+70.0102 s] Raw data (loadavg): 0.95 0.96 0.91 2/57 21058 Raw data (/proc/21054/stat): 21054 (minisat+_script) S 21053 21054 20115 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855448975 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/21054/statm): 531 226 485 147 0 384 0 [pid=21054] vsize: 2124 Raw data (/proc/21058/stat): 21058 (minisat+_64-bit) T 21054 21054 20115 0 -1 0 2391 0 0 0 6960 17 0 0 25 0 1 0 1855448980 10412032 2342 4294967295 134512640 135094434 3221224448 3221222796 134870330 0 0 5 16386 3222434794 0 0 17 1 0 0 Raw data (/proc/21058/statm): 2542 2342 145 145 0 2397 0 [pid=21058] vsize: 10168 Current children cumulated CPU time (s) 69.77 Current children cumulated vsize (Kb) 12292 [startup+80.0119 s] Raw data (loadavg): 0.96 0.96 0.91 2/57 21058 Raw data (/proc/21054/stat): 21054 (minisat+_script) S 21053 21054 20115 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855448975 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/21054/statm): 531 226 485 147 0 384 0 [pid=21054] vsize: 2124 Raw data (/proc/21058/stat): 21058 (minisat+_64-bit) R 21054 21054 20115 0 -1 0 2469 0 0 0 7958 17 0 0 25 0 1 0 1855448980 10723328 2420 4294967295 134512640 135094434 3221224448 3221223104 134557988 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/21058/statm): 2618 2420 145 145 0 2473 0 [pid=21058] vsize: 10472 Current children cumulated CPU time (s) 79.75 Current children cumulated vsize (Kb) 12596 [startup+90.0126 s] Raw data (loadavg): 0.96 0.96 0.91 2/57 21058 Raw data (/proc/21054/stat): 21054 (minisat+_script) S 21053 21054 20115 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855448975 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/21054/statm): 531 226 485 147 0 384 0 [pid=21054] vsize: 2124 Raw data (/proc/21058/stat): 21058 (minisat+_64-bit) R 21054 21054 20115 0 -1 0 2656 0 0 0 8955 19 0 0 25 0 1 0 1855448980 11472896 2607 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/21058/statm): 2801 2607 145 145 0 2656 0 [pid=21058] vsize: 11204 Current children cumulated CPU time (s) 89.74 Current children cumulated vsize (Kb) 13328 [startup+100.013 s] Raw data (loadavg): 0.97 0.96 0.91 2/57 21058 Raw data (/proc/21054/stat): 21054 (minisat+_script) S 21053 21054 20115 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855448975 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/21054/statm): 531 226 485 147 0 384 0 [pid=21054] vsize: 2124 Raw data (/proc/21058/stat): 21058 (minisat+_64-bit) R 21054 21054 20115 0 -1 0 2793 0 0 0 9953 19 0 0 25 0 1 0 1855448980 12156928 2744 4294967295 134512640 135094434 3221224448 3221223104 134550408 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/21058/statm): 2968 2744 145 145 0 2823 0 [pid=21058] vsize: 11872 Current children cumulated CPU time (s) 99.72 Current children cumulated vsize (Kb) 13996 [startup+110.015 s] Raw data (loadavg): 0.97 0.96 0.91 2/57 21058 Raw data (/proc/21054/stat): 21054 (minisat+_script) S 21053 21054 20115 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855448975 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/21054/statm): 531 226 485 147 0 384 0 [pid=21054] vsize: 2124 Raw data (/proc/21058/stat): 21058 (minisat+_64-bit) R 21054 21054 20115 0 -1 0 2793 0 0 0 10953 19 0 0 25 0 1 0 1855448980 12156928 2744 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/21058/statm): 2968 2744 145 145 0 2823 0 [pid=21058] vsize: 11872 Current children cumulated CPU time (s) 109.72 Current children cumulated vsize (Kb) 13996 [startup+120.016 s] Raw data (loadavg): 0.98 0.97 0.91 2/57 21058 Raw data (/proc/21054/stat): 21054 (minisat+_script) S 21053 21054 20115 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855448975 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/21054/statm): 531 226 485 147 0 384 0 [pid=21054] vsize: 2124 Raw data (/proc/21058/stat): 21058 (minisat+_64-bit) R 21054 21054 20115 0 -1 0 2793 0 0 0 11953 20 0 0 25 0 1 0 1855448980 12156928 2744 4294967295 134512640 135094434 3221224448 3221223104 134557950 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/21058/statm): 2968 2744 145 145 0 2823 0 [pid=21058] vsize: 11872 Current children cumulated CPU time (s) 119.73 Current children cumulated vsize (Kb) 13996 [startup+130.017 s] Raw data (loadavg): 0.98 0.97 0.91 2/57 21058 Raw data (/proc/21054/stat): 21054 (minisat+_script) S 21053 21054 20115 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855448975 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/21054/statm): 531 226 485 147 0 384 0 [pid=21054] vsize: 2124 Raw data (/proc/21058/stat): 21058 (minisat+_64-bit) R 21054 21054 20115 0 -1 0 2793 0 0 0 12953 20 0 0 25 0 1 0 1855448980 12156928 2744 4294967295 134512640 135094434 3221224448 3221223104 134558227 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/21058/statm): 2968 2744 145 145 0 2823 0 [pid=21058] vsize: 11872 Current children cumulated CPU time (s) 129.73 Current children cumulated vsize (Kb) 13996 [startup+140.018 s] Raw data (loadavg): 0.98 0.97 0.91 2/57 21058 Raw data (/proc/21054/stat): 21054 (minisat+_script) S 21053 21054 20115 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855448975 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/21054/statm): 531 226 485 147 0 384 0 [pid=21054] vsize: 2124 Raw data (/proc/21058/stat): 21058 (minisat+_64-bit) R 21054 21054 20115 0 -1 0 2966 0 0 0 13950 21 0 0 25 0 1 0 1855448980 12853248 2917 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/21058/statm): 3138 2917 145 145 0 2993 0 [pid=21058] vsize: 12552 Current children cumulated CPU time (s) 139.71 Current children cumulated vsize (Kb) 14676 [startup+150.019 s] Raw data (loadavg): 0.98 0.97 0.91 2/57 21058 Raw data (/proc/21054/stat): 21054 (minisat+_script) S 21053 21054 20115 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855448975 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/21054/statm): 531 226 485 147 0 384 0 [pid=21054] vsize: 2124 Raw data (/proc/21058/stat): 21058 (minisat+_64-bit) R 21054 21054 20115 0 -1 0 2968 0 0 0 14950 21 0 0 25 0 1 0 1855448980 12861440 2919 4294967295 134512640 135094434 3221224448 3221223040 134557273 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/21058/statm): 3140 2919 145 145 0 2995 0 [pid=21058] vsize: 12560 Current children cumulated CPU time (s) 149.71 Current children cumulated vsize (Kb) 14684 [startup+160.019 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 21060 Raw data (/proc/21054/stat): 21054 (minisat+_script) S 21053 21054 20115 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855448975 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/21054/statm): 531 226 485 147 0 384 0 [pid=21054] vsize: 2124 Raw data (/proc/21058/stat): 21058 (minisat+_64-bit) R 21054 21054 20115 0 -1 0 3166 0 0 0 15946 23 0 0 25 0 1 0 1855448980 13672448 3117 4294967295 134512640 135094434 3221224448 3221223104 134558246 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/21058/statm): 3338 3117 145 145 0 3193 0 [pid=21058] vsize: 13352 Current children cumulated CPU time (s) 159.69 Current children cumulated vsize (Kb) 15476 [startup+170.02 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 21060 Raw data (/proc/21054/stat): 21054 (minisat+_script) S 21053 21054 20115 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855448975 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/21054/statm): 531 226 485 147 0 384 0 [pid=21054] vsize: 2124 Raw data (/proc/21058/stat): 21058 (minisat+_64-bit) T 21054 21054 20115 0 -1 0 3529 0 0 0 16939 26 0 0 25 0 1 0 1855448980 15151104 3480 4294967295 134512640 135094434 3221224448 3221222812 134870330 0 0 5 16386 3222434794 0 0 17 1 0 0 Raw data (/proc/21058/statm): 3699 3480 145 145 0 3554 0 [pid=21058] vsize: 14796 Current children cumulated CPU time (s) 169.65 Current children cumulated vsize (Kb) 16920 [startup+180.021 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 21060 Raw data (/proc/21054/stat): 21054 (minisat+_script) S 21053 21054 20115 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855448975 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/21054/statm): 531 226 485 147 0 384 0 [pid=21054] vsize: 2124 Raw data (/proc/21058/stat): 21058 (minisat+_64-bit) R 21054 21054 20115 0 -1 0 3814 0 0 0 17934 28 0 0 25 0 1 0 1855448980 16297984 3765 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/21058/statm): 3979 3765 145 145 0 3834 0 [pid=21058] vsize: 15916 Current children cumulated CPU time (s) 179.62 Current children cumulated vsize (Kb) 18040 [startup+190.022 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 21060 Raw data (/proc/21054/stat): 21054 (minisat+_script) S 21053 21054 20115 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855448975 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/21054/statm): 531 226 485 147 0 384 0 [pid=21054] vsize: 2124 Raw data (/proc/21058/stat): 21058 (minisat+_64-bit) R 21054 21054 20115 0 -1 0 3814 0 0 0 18933 28 0 0 25 0 1 0 1855448980 16297984 3765 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/21058/statm): 3979 3765 145 145 0 3834 0 [pid=21058] vsize: 15916 Current children cumulated CPU time (s) 189.61 Current children cumulated vsize (Kb) 18040 [startup+200.023 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 21060 Raw data (/proc/21054/stat): 21054 (minisat+_script) S 21053 21054 20115 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855448975 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/21054/statm): 531 226 485 147 0 384 0 [pid=21054] vsize: 2124 Raw data (/proc/21058/stat): 21058 (minisat+_64-bit) R 21054 21054 20115 0 -1 0 3814 0 0 0 19934 28 0 0 25 0 1 0 1855448980 16297984 3765 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/21058/statm): 3979 3765 145 145 0 3834 0 [pid=21058] vsize: 15916 Current children cumulated CPU time (s) 199.62 Current children cumulated vsize (Kb) 18040 [startup+210.024 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 21060 Raw data (/proc/21054/stat): 21054 (minisat+_script) S 21053 21054 20115 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855448975 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/21054/statm): 531 226 485 147 0 384 0 [pid=21054] vsize: 2124 Raw data (/proc/21058/stat): 21058 (minisat+_64-bit) R 21054 21054 20115 0 -1 0 3814 0 0 0 20934 28 0 0 25 0 1 0 1855448980 16297984 3765 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/21058/statm): 3979 3765 145 145 0 3834 0 [pid=21058] vsize: 15916 Current children cumulated CPU time (s) 209.62 Current children cumulated vsize (Kb) 18040 [startup+220.024 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 21060 Raw data (/proc/21054/stat): 21054 (minisat+_script) S 21053 21054 20115 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855448975 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/21054/statm): 531 226 485 147 0 384 0 [pid=21054] vsize: 2124 Raw data (/proc/21058/stat): 21058 (minisat+_64-bit) R 21054 21054 20115 0 -1 0 3814 0 0 0 21934 28 0 0 25 0 1 0 1855448980 16297984 3765 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/21058/statm): 3979 3765 145 145 0 3834 0 [pid=21058] vsize: 15916 Current children cumulated CPU time (s) 219.62 Current children cumulated vsize (Kb) 18040 [startup+230.025 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 21060 Raw data (/proc/21054/stat): 21054 (minisat+_script) S 21053 21054 20115 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855448975 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/21054/statm): 531 226 485 147 0 384 0 [pid=21054] vsize: 2124 Raw data (/proc/21058/stat): 21058 (minisat+_64-bit) R 21054 21054 20115 0 -1 0 3814 0 0 0 22934 28 0 0 25 0 1 0 1855448980 16297984 3765 4294967295 134512640 135094434 3221224448 3221223120 134556485 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/21058/statm): 3979 3765 145 145 0 3834 0 [pid=21058] vsize: 15916 Current children cumulated CPU time (s) 229.62 Current children cumulated vsize (Kb) 18040 [startup+240.026 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 21060 Raw data (/proc/21054/stat): 21054 (minisat+_script) S 21053 21054 20115 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855448975 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/21054/statm): 531 226 485 147 0 384 0 [pid=21054] vsize: 2124 Raw data (/proc/21058/stat): 21058 (minisat+_64-bit) R 21054 21054 20115 0 -1 0 3814 0 0 0 23935 28 0 0 25 0 1 0 1855448980 16297984 3765 4294967295 134512640 135094434 3221224448 3221223120 134556499 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/21058/statm): 3979 3765 145 145 0 3834 0 [pid=21058] vsize: 15916 Current children cumulated CPU time (s) 239.63 Current children cumulated vsize (Kb) 18040 [startup+250.026 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 21060 Raw data (/proc/21054/stat): 21054 (minisat+_script) S 21053 21054 20115 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855448975 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/21054/statm): 531 226 485 147 0 384 0 [pid=21054] vsize: 2124 Raw data (/proc/21058/stat): 21058 (minisat+_64-bit) R 21054 21054 20115 0 -1 0 3814 0 0 0 24935 28 0 0 25 0 1 0 1855448980 16297984 3765 4294967295 134512640 135094434 3221224448 3221223104 134558004 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/21058/statm): 3979 3765 145 145 0 3834 0 [pid=21058] vsize: 15916 Current children cumulated CPU time (s) 249.63 Current children cumulated vsize (Kb) 18040 [startup+260.027 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 21060 Raw data (/proc/21054/stat): 21054 (minisat+_script) S 21053 21054 20115 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855448975 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/21054/statm): 531 226 485 147 0 384 0 [pid=21054] vsize: 2124 Raw data (/proc/21058/stat): 21058 (minisat+_64-bit) R 21054 21054 20115 0 -1 0 3814 0 0 0 25935 28 0 0 25 0 1 0 1855448980 16297984 3765 4294967295 134512640 135094434 3221224448 3221223104 134557917 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/21058/statm): 3979 3765 145 145 0 3834 0 [pid=21058] vsize: 15916 Current children cumulated CPU time (s) 259.63 Current children cumulated vsize (Kb) 18040 [startup+270.028 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 21060 Raw data (/proc/21054/stat): 21054 (minisat+_script) S 21053 21054 20115 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855448975 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/21054/statm): 531 226 485 147 0 384 0 [pid=21054] vsize: 2124 Raw data (/proc/21058/stat): 21058 (minisat+_64-bit) R 21054 21054 20115 0 -1 0 3814 0 0 0 26935 29 0 0 25 0 1 0 1855448980 16297984 3765 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/21058/statm): 3979 3765 145 145 0 3834 0 [pid=21058] vsize: 15916 Current children cumulated CPU time (s) 269.64 Current children cumulated vsize (Kb) 18040 [startup+280.029 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 21060 Raw data (/proc/21054/stat): 21054 (minisat+_script) S 21053 21054 20115 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855448975 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/21054/statm): 531 226 485 147 0 384 0 [pid=21054] vsize: 2124 Raw data (/proc/21058/stat): 21058 (minisat+_64-bit) R 21054 21054 20115 0 -1 0 4109 0 0 0 27929 31 0 0 25 0 1 0 1855448980 17489920 4060 4294967295 134512640 135094434 3221224448 3221223104 134558019 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/21058/statm): 4270 4060 145 145 0 4125 0 [pid=21058] vsize: 17080 Current children cumulated CPU time (s) 279.6 Current children cumulated vsize (Kb) 19204 [startup+290.03 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 21060 Raw data (/proc/21054/stat): 21054 (minisat+_script) S 21053 21054 20115 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855448975 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/21054/statm): 531 226 485 147 0 384 0 [pid=21054] vsize: 2124 Raw data (/proc/21058/stat): 21058 (minisat+_64-bit) R 21054 21054 20115 0 -1 0 4144 0 0 0 28929 31 0 0 25 0 1 0 1855448980 17633280 4095 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/21058/statm): 4305 4095 145 145 0 4160 0 [pid=21058] vsize: 17220 Current children cumulated CPU time (s) 289.6 Current children cumulated vsize (Kb) 19344 [startup+300.031 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 21060 Raw data (/proc/21054/stat): 21054 (minisat+_script) S 21053 21054 20115 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855448975 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/21054/statm): 531 226 485 147 0 384 0 [pid=21054] vsize: 2124 Raw data (/proc/21058/stat): 21058 (minisat+_64-bit) R 21054 21054 20115 0 -1 0 4156 0 0 0 29929 31 0 0 25 0 1 0 1855448980 17682432 4107 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/21058/statm): 4317 4107 145 145 0 4172 0 [pid=21058] vsize: 17268 Current children cumulated CPU time (s) 299.6 Current children cumulated vsize (Kb) 19392 [startup+310.033 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 21060 Raw data (/proc/21054/stat): 21054 (minisat+_script) S 21053 21054 20115 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855448975 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/21054/statm): 531 226 485 147 0 384 0 [pid=21054] vsize: 2124 Raw data (/proc/21058/stat): 21058 (minisat+_64-bit) R 21054 21054 20115 0 -1 0 4171 0 0 0 30929 32 0 0 25 0 1 0 1855448980 17747968 4122 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/21058/statm): 4333 4122 145 145 0 4188 0 [pid=21058] vsize: 17332 Current children cumulated CPU time (s) 309.61 Current children cumulated vsize (Kb) 19456 [startup+320.033 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 21060 Raw data (/proc/21054/stat): 21054 (minisat+_script) S 21053 21054 20115 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855448975 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/21054/statm): 531 226 485 147 0 384 0 [pid=21054] vsize: 2124 Raw data (/proc/21058/stat): 21058 (minisat+_64-bit) R 21054 21054 20115 0 -1 0 4181 0 0 0 31929 32 0 0 25 0 1 0 1855448980 17797120 4132 4294967295 134512640 135094434 3221224448 3221223136 134554746 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/21058/statm): 4345 4132 145 145 0 4200 0 [pid=21058] vsize: 17380 Current children cumulated CPU time (s) 319.61 Current children cumulated vsize (Kb) 19504 [startup+330.034 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 21060 Raw data (/proc/21054/stat): 21054 (minisat+_script) S 21053 21054 20115 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855448975 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/21054/statm): 531 226 485 147 0 384 0 [pid=21054] vsize: 2124 Raw data (/proc/21058/stat): 21058 (minisat+_64-bit) R 21054 21054 20115 0 -1 0 4188 0 0 0 32929 32 0 0 25 0 1 0 1855448980 17829888 4139 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/21058/statm): 4353 4139 145 145 0 4208 0 [pid=21058] vsize: 17412 Current children cumulated CPU time (s) 329.61 Current children cumulated vsize (Kb) 19536 [startup+340.035 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 21060 Raw data (/proc/21054/stat): 21054 (minisat+_script) S 21053 21054 20115 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855448975 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/21054/statm): 531 226 485 147 0 384 0 [pid=21054] vsize: 2124 Raw data (/proc/21058/stat): 21058 (minisat+_64-bit) T 21054 21054 20115 0 -1 0 4340 0 0 0 33926 33 0 0 25 0 1 0 1855448980 18452480 4291 4294967295 134512640 135094434 3221224448 3221222828 134870330 0 0 5 16386 3222434794 0 0 17 1 0 0 Raw data (/proc/21058/statm): 4505 4291 145 145 0 4360 0 [pid=21058] vsize: 18020 Current children cumulated CPU time (s) 339.59 Current children cumulated vsize (Kb) 20144 [startup+350.035 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 21060 Raw data (/proc/21054/stat): 21054 (minisat+_script) S 21053 21054 20115 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855448975 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/21054/statm): 531 226 485 147 0 384 0 [pid=21054] vsize: 2124 Raw data (/proc/21058/stat): 21058 (minisat+_64-bit) R 21054 21054 20115 0 -1 0 4641 0 0 0 34921 36 0 0 25 0 1 0 1855448980 19685376 4592 4294967295 134512640 135094434 3221224448 3221223104 134557964 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/21058/statm): 4806 4592 145 145 0 4661 0 [pid=21058] vsize: 19224 Current children cumulated CPU time (s) 349.57 Current children cumulated vsize (Kb) 21348 [startup+360.036 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 21060 Raw data (/proc/21054/stat): 21054 (minisat+_script) S 21053 21054 20115 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855448975 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/21054/statm): 531 226 485 147 0 384 0 [pid=21054] vsize: 2124 Raw data (/proc/21058/stat): 21058 (minisat+_64-bit) R 21054 21054 20115 0 -1 0 4897 0 0 0 35916 38 0 0 18 0 1 0 1855448980 20738048 4848 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/21058/statm): 5063 4848 145 145 0 4918 0 [pid=21058] vsize: 20252 Current children cumulated CPU time (s) 359.54 Current children cumulated vsize (Kb) 22376 [startup+370.038 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 21060 Raw data (/proc/21054/stat): 21054 (minisat+_script) S 21053 21054 20115 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855448975 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/21054/statm): 531 226 485 147 0 384 0 [pid=21054] vsize: 2124 Raw data (/proc/21058/stat): 21058 (minisat+_64-bit) R 21054 21054 20115 0 -1 0 5120 0 0 0 36913 39 0 0 25 0 1 0 1855448980 21639168 5071 4294967295 134512640 135094434 3221224448 3221223104 134558029 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/21058/statm): 5283 5071 145 145 0 5138 0 [pid=21058] vsize: 21132 Current children cumulated CPU time (s) 369.52 Current children cumulated vsize (Kb) 23256 [startup+380.038 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 21060 Raw data (/proc/21054/stat): 21054 (minisat+_script) S 21053 21054 20115 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855448975 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/21054/statm): 531 226 485 147 0 384 0 [pid=21054] vsize: 2124 Raw data (/proc/21058/stat): 21058 (minisat+_64-bit) R 21054 21054 20115 0 -1 0 5276 0 0 0 37908 42 0 0 25 0 1 0 1855448980 22265856 5227 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/21058/statm): 5436 5227 145 145 0 5291 0 [pid=21058] vsize: 21744 Current children cumulated CPU time (s) 379.5 Current children cumulated vsize (Kb) 23868 [startup+390.039 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 21060 Raw data (/proc/21054/stat): 21054 (minisat+_script) S 21053 21054 20115 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855448975 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/21054/statm): 531 226 485 147 0 384 0 [pid=21054] vsize: 2124 Raw data (/proc/21058/stat): 21058 (minisat+_64-bit) R 21054 21054 20115 0 -1 0 5276 0 0 0 38907 43 0 0 25 0 1 0 1855448980 22265856 5227 4294967295 134512640 135094434 3221224448 3221223072 134562113 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/21058/statm): 5436 5227 145 145 0 5291 0 [pid=21058] vsize: 21744 Current children cumulated CPU time (s) 389.5 Current children cumulated vsize (Kb) 23868 [startup+400.04 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 21060 Raw data (/proc/21054/stat): 21054 (minisat+_script) S 21053 21054 20115 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855448975 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/21054/statm): 531 226 485 147 0 384 0 [pid=21054] vsize: 2124 Raw data (/proc/21058/stat): 21058 (minisat+_64-bit) R 21054 21054 20115 0 -1 0 5276 0 0 0 39907 43 0 0 25 0 1 0 1855448980 22265856 5227 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/21058/statm): 5436 5227 145 145 0 5291 0 [pid=21058] vsize: 21744 Current children cumulated CPU time (s) 399.5 Current children cumulated vsize (Kb) 23868 [startup+410.04 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 21060 Raw data (/proc/21054/stat): 21054 (minisat+_script) S 21053 21054 20115 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855448975 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/21054/statm): 531 226 485 147 0 384 0 [pid=21054] vsize: 2124 Raw data (/proc/21058/stat): 21058 (minisat+_64-bit) R 21054 21054 20115 0 -1 0 5276 0 0 0 40907 44 0 0 25 0 1 0 1855448980 22265856 5227 4294967295 134512640 135094434 3221224448 3221223104 134557911 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/21058/statm): 5436 5227 145 145 0 5291 0 [pid=21058] vsize: 21744 Current children cumulated CPU time (s) 409.51 Current children cumulated vsize (Kb) 23868 [startup+420.041 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 21060 Raw data (/proc/21054/stat): 21054 (minisat+_script) S 21053 21054 20115 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855448975 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/21054/statm): 531 226 485 147 0 384 0 [pid=21054] vsize: 2124 Raw data (/proc/21058/stat): 21058 (minisat+_64-bit) R 21054 21054 20115 0 -1 0 5276 0 0 0 41907 44 0 0 25 0 1 0 1855448980 22265856 5227 4294967295 134512640 135094434 3221224448 3221223040 134551463 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/21058/statm): 5436 5227 145 145 0 5291 0 [pid=21058] vsize: 21744 Current children cumulated CPU time (s) 419.51 Current children cumulated vsize (Kb) 23868 [startup+430.043 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 21060 Raw data (/proc/21054/stat): 21054 (minisat+_script) S 21053 21054 20115 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855448975 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/21054/statm): 531 226 485 147 0 384 0 [pid=21054] vsize: 2124 Raw data (/proc/21058/stat): 21058 (minisat+_64-bit) R 21054 21054 20115 0 -1 0 5276 0 0 0 42907 44 0 0 25 0 1 0 1855448980 22265856 5227 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/21058/statm): 5436 5227 145 145 0 5291 0 [pid=21058] vsize: 21744 Current children cumulated CPU time (s) 429.51 Current children cumulated vsize (Kb) 23868 [startup+440.043 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 21060 Raw data (/proc/21054/stat): 21054 (minisat+_script) S 21053 21054 20115 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855448975 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/21054/statm): 531 226 485 147 0 384 0 [pid=21054] vsize: 2124 Raw data (/proc/21058/stat): 21058 (minisat+_64-bit) R 21054 21054 20115 0 -1 0 5276 0 0 0 43907 45 0 0 25 0 1 0 1855448980 22265856 5227 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/21058/statm): 5436 5227 145 145 0 5291 0 [pid=21058] vsize: 21744 Current children cumulated CPU time (s) 439.52 Current children cumulated vsize (Kb) 23868 [startup+450.044 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 21060 Raw data (/proc/21054/stat): 21054 (minisat+_script) S 21053 21054 20115 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855448975 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/21054/statm): 531 226 485 147 0 384 0 [pid=21054] vsize: 2124 Raw data (/proc/21058/stat): 21058 (minisat+_64-bit) R 21054 21054 20115 0 -1 0 5276 0 0 0 44907 45 0 0 25 0 1 0 1855448980 22265856 5227 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/21058/statm): 5436 5227 145 145 0 5291 0 [pid=21058] vsize: 21744 Current children cumulated CPU time (s) 449.52 Current children cumulated vsize (Kb) 23868 [startup+460.045 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 21060 Raw data (/proc/21054/stat): 21054 (minisat+_script) S 21053 21054 20115 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855448975 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/21054/statm): 531 226 485 147 0 384 0 [pid=21054] vsize: 2124 Raw data (/proc/21058/stat): 21058 (minisat+_64-bit) R 21054 21054 20115 0 -1 0 5276 0 0 0 45908 45 0 0 25 0 1 0 1855448980 22265856 5227 4294967295 134512640 135094434 3221224448 3221223104 134557860 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/21058/statm): 5436 5227 145 145 0 5291 0 [pid=21058] vsize: 21744 Current children cumulated CPU time (s) 459.53 Current children cumulated vsize (Kb) 23868 [startup+470.045 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 21060 Raw data (/proc/21054/stat): 21054 (minisat+_script) S 21053 21054 20115 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855448975 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/21054/statm): 531 226 485 147 0 384 0 [pid=21054] vsize: 2124 Raw data (/proc/21058/stat): 21058 (minisat+_64-bit) R 21054 21054 20115 0 -1 0 5276 0 0 0 46908 45 0 0 25 0 1 0 1855448980 22265856 5227 4294967295 134512640 135094434 3221224448 3221223104 134557896 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/21058/statm): 5436 5227 145 145 0 5291 0 [pid=21058] vsize: 21744 Current children cumulated CPU time (s) 469.53 Current children cumulated vsize (Kb) 23868 [startup+480.046 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 21060 Raw data (/proc/21054/stat): 21054 (minisat+_script) S 21053 21054 20115 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855448975 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/21054/statm): 531 226 485 147 0 384 0 [pid=21054] vsize: 2124 Raw data (/proc/21058/stat): 21058 (minisat+_64-bit) R 21054 21054 20115 0 -1 0 5276 0 0 0 47908 45 0 0 25 0 1 0 1855448980 22265856 5227 4294967295 134512640 135094434 3221224448 3221223104 134558159 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/21058/statm): 5436 5227 145 145 0 5291 0 [pid=21058] vsize: 21744 Current children cumulated CPU time (s) 479.53 Current children cumulated vsize (Kb) 23868 [startup+490.047 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 21060 Raw data (/proc/21054/stat): 21054 (minisat+_script) S 21053 21054 20115 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855448975 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/21054/statm): 531 226 485 147 0 384 0 [pid=21054] vsize: 2124 Raw data (/proc/21058/stat): 21058 (minisat+_64-bit) R 21054 21054 20115 0 -1 0 5276 0 0 0 48908 45 0 0 25 0 1 0 1855448980 22265856 5227 4294967295 134512640 135094434 3221224448 3221223136 134554728 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/21058/statm): 5436 5227 145 145 0 5291 0 [pid=21058] vsize: 21744 Current children cumulated CPU time (s) 489.53 Current children cumulated vsize (Kb) 23868 [startup+500.047 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 21060 Raw data (/proc/21054/stat): 21054 (minisat+_script) S 21053 21054 20115 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855448975 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/21054/statm): 531 226 485 147 0 384 0 [pid=21054] vsize: 2124 Raw data (/proc/21058/stat): 21058 (minisat+_64-bit) R 21054 21054 20115 0 -1 0 5276 0 0 0 49908 45 0 0 25 0 1 0 1855448980 22265856 5227 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/21058/statm): 5436 5227 145 145 0 5291 0 [pid=21058] vsize: 21744 Current children cumulated CPU time (s) 499.53 Current children cumulated vsize (Kb) 23868 [startup+510.049 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 21060 Raw data (/proc/21054/stat): 21054 (minisat+_script) S 21053 21054 20115 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855448975 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/21054/statm): 531 226 485 147 0 384 0 [pid=21054] vsize: 2124 Raw data (/proc/21058/stat): 21058 (minisat+_64-bit) R 21054 21054 20115 0 -1 0 5276 0 0 0 50908 45 0 0 25 0 1 0 1855448980 22265856 5227 4294967295 134512640 135094434 3221224448 3221223136 134554746 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/21058/statm): 5436 5227 145 145 0 5291 0 [pid=21058] vsize: 21744 Current children cumulated CPU time (s) 509.53 Current children cumulated vsize (Kb) 23868 [startup+520.05 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 21060 Raw data (/proc/21054/stat): 21054 (minisat+_script) S 21053 21054 20115 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855448975 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/21054/statm): 531 226 485 147 0 384 0 [pid=21054] vsize: 2124 Raw data (/proc/21058/stat): 21058 (minisat+_64-bit) R 21054 21054 20115 0 -1 0 5276 0 0 0 51908 45 0 0 25 0 1 0 1855448980 22265856 5227 4294967295 134512640 135094434 3221224448 3221223104 134558178 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/21058/statm): 5436 5227 145 145 0 5291 0 [pid=21058] vsize: 21744 Current children cumulated CPU time (s) 519.53 Current children cumulated vsize (Kb) 23868 [startup+530.051 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 21060 Raw data (/proc/21054/stat): 21054 (minisat+_script) S 21053 21054 20115 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855448975 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/21054/statm): 531 226 485 147 0 384 0 [pid=21054] vsize: 2124 Raw data (/proc/21058/stat): 21058 (minisat+_64-bit) R 21054 21054 20115 0 -1 0 5276 0 0 0 52908 46 0 0 25 0 1 0 1855448980 22265856 5227 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/21058/statm): 5436 5227 145 145 0 5291 0 [pid=21058] vsize: 21744 Current children cumulated CPU time (s) 529.54 Current children cumulated vsize (Kb) 23868 [startup+540.051 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 21060 Raw data (/proc/21054/stat): 21054 (minisat+_script) S 21053 21054 20115 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855448975 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/21054/statm): 531 226 485 147 0 384 0 [pid=21054] vsize: 2124 Raw data (/proc/21058/stat): 21058 (minisat+_64-bit) R 21054 21054 20115 0 -1 0 5276 0 0 0 53909 46 0 0 25 0 1 0 1855448980 22265856 5227 4294967295 134512640 135094434 3221224448 3221223104 134557849 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/21058/statm): 5436 5227 145 145 0 5291 0 [pid=21058] vsize: 21744 Current children cumulated CPU time (s) 539.55 Current children cumulated vsize (Kb) 23868 [startup+550.052 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 21060 Raw data (/proc/21054/stat): 21054 (minisat+_script) S 21053 21054 20115 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855448975 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/21054/statm): 531 226 485 147 0 384 0 [pid=21054] vsize: 2124 Raw data (/proc/21058/stat): 21058 (minisat+_64-bit) R 21054 21054 20115 0 -1 0 5276 0 0 0 54909 46 0 0 25 0 1 0 1855448980 22265856 5227 4294967295 134512640 135094434 3221224448 3221223104 134558213 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/21058/statm): 5436 5227 145 145 0 5291 0 [pid=21058] vsize: 21744 Current children cumulated CPU time (s) 549.55 Current children cumulated vsize (Kb) 23868 [startup+560.053 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 21060 Raw data (/proc/21054/stat): 21054 (minisat+_script) S 21053 21054 20115 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855448975 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/21054/statm): 531 226 485 147 0 384 0 [pid=21054] vsize: 2124 Raw data (/proc/21058/stat): 21058 (minisat+_64-bit) R 21054 21054 20115 0 -1 0 5276 0 0 0 55909 46 0 0 25 0 1 0 1855448980 22265856 5227 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/21058/statm): 5436 5227 145 145 0 5291 0 [pid=21058] vsize: 21744 Current children cumulated CPU time (s) 559.55 Current children cumulated vsize (Kb) 23868 [startup+570.053 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 21060 Raw data (/proc/21054/stat): 21054 (minisat+_script) S 21053 21054 20115 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855448975 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/21054/statm): 531 226 485 147 0 384 0 [pid=21054] vsize: 2124 Raw data (/proc/21058/stat): 21058 (minisat+_64-bit) R 21054 21054 20115 0 -1 0 5276 0 0 0 56909 46 0 0 25 0 1 0 1855448980 22265856 5227 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/21058/statm): 5436 5227 145 145 0 5291 0 [pid=21058] vsize: 21744 Current children cumulated CPU time (s) 569.55 Current children cumulated vsize (Kb) 23868 [startup+580.055 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 21060 Raw data (/proc/21054/stat): 21054 (minisat+_script) S 21053 21054 20115 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855448975 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/21054/statm): 531 226 485 147 0 384 0 [pid=21054] vsize: 2124 Raw data (/proc/21058/stat): 21058 (minisat+_64-bit) R 21054 21054 20115 0 -1 0 5276 0 0 0 57909 46 0 0 25 0 1 0 1855448980 22265856 5227 4294967295 134512640 135094434 3221224448 3221223104 134557920 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/21058/statm): 5436 5227 145 145 0 5291 0 [pid=21058] vsize: 21744 Current children cumulated CPU time (s) 579.55 Current children cumulated vsize (Kb) 23868 [startup+590.056 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 21060 Raw data (/proc/21054/stat): 21054 (minisat+_script) S 21053 21054 20115 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855448975 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/21054/statm): 531 226 485 147 0 384 0 [pid=21054] vsize: 2124 Raw data (/proc/21058/stat): 21058 (minisat+_64-bit) R 21054 21054 20115 0 -1 0 5276 0 0 0 58910 46 0 0 25 0 1 0 1855448980 22265856 5227 4294967295 134512640 135094434 3221224448 3221223104 134558126 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/21058/statm): 5436 5227 145 145 0 5291 0 [pid=21058] vsize: 21744 Current children cumulated CPU time (s) 589.56 Current children cumulated vsize (Kb) 23868 [startup+600.056 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 21060 Raw data (/proc/21054/stat): 21054 (minisat+_script) S 21053 21054 20115 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855448975 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/21054/statm): 531 226 485 147 0 384 0 [pid=21054] vsize: 2124 Raw data (/proc/21058/stat): 21058 (minisat+_64-bit) R 21054 21054 20115 0 -1 0 5276 0 0 0 59910 46 0 0 25 0 1 0 1855448980 22265856 5227 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/21058/statm): 5436 5227 145 145 0 5291 0 [pid=21058] vsize: 21744 Current children cumulated CPU time (s) 599.56 Current children cumulated vsize (Kb) 23868 [startup+610.058 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 21060 Raw data (/proc/21054/stat): 21054 (minisat+_script) S 21053 21054 20115 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855448975 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/21054/statm): 531 226 485 147 0 384 0 [pid=21054] vsize: 2124 Raw data (/proc/21058/stat): 21058 (minisat+_64-bit) R 21054 21054 20115 0 -1 0 5276 0 0 0 60910 46 0 0 25 0 1 0 1855448980 22265856 5227 4294967295 134512640 135094434 3221224448 3221223104 134557911 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/21058/statm): 5436 5227 145 145 0 5291 0 [pid=21058] vsize: 21744 Current children cumulated CPU time (s) 609.56 Current children cumulated vsize (Kb) 23868 [startup+620.059 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 21060 Raw data (/proc/21054/stat): 21054 (minisat+_script) S 21053 21054 20115 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855448975 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/21054/statm): 531 226 485 147 0 384 0 [pid=21054] vsize: 2124 Raw data (/proc/21058/stat): 21058 (minisat+_64-bit) R 21054 21054 20115 0 -1 0 5276 0 0 0 61910 46 0 0 25 0 1 0 1855448980 22265856 5227 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/21058/statm): 5436 5227 145 145 0 5291 0 [pid=21058] vsize: 21744 Current children cumulated CPU time (s) 619.56 Current children cumulated vsize (Kb) 23868 [startup+630.06 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 21060 Raw data (/proc/21054/stat): 21054 (minisat+_script) S 21053 21054 20115 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855448975 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/21054/statm): 531 226 485 147 0 384 0 [pid=21054] vsize: 2124 Raw data (/proc/21058/stat): 21058 (minisat+_64-bit) R 21054 21054 20115 0 -1 0 5276 0 0 0 62910 46 0 0 25 0 1 0 1855448980 22265856 5227 4294967295 134512640 135094434 3221224448 3221223104 134557928 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/21058/statm): 5436 5227 145 145 0 5291 0 [pid=21058] vsize: 21744 Current children cumulated CPU time (s) 629.56 Current children cumulated vsize (Kb) 23868 [startup+640.061 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 21060 Raw data (/proc/21054/stat): 21054 (minisat+_script) S 21053 21054 20115 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855448975 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/21054/statm): 531 226 485 147 0 384 0 [pid=21054] vsize: 2124 Raw data (/proc/21058/stat): 21058 (minisat+_64-bit) R 21054 21054 20115 0 -1 0 5276 0 0 0 63910 47 0 0 25 0 1 0 1855448980 22265856 5227 4294967295 134512640 135094434 3221224448 3221223104 134558218 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/21058/statm): 5436 5227 145 145 0 5291 0 [pid=21058] vsize: 21744 Current children cumulated CPU time (s) 639.57 Current children cumulated vsize (Kb) 23868 [startup+650.062 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 21060 Raw data (/proc/21054/stat): 21054 (minisat+_script) S 21053 21054 20115 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855448975 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/21054/statm): 531 226 485 147 0 384 0 [pid=21054] vsize: 2124 Raw data (/proc/21058/stat): 21058 (minisat+_64-bit) R 21054 21054 20115 0 -1 0 5276 0 0 0 64911 47 0 0 25 0 1 0 1855448980 22265856 5227 4294967295 134512640 135094434 3221224448 3221223136 134554751 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/21058/statm): 5436 5227 145 145 0 5291 0 [pid=21058] vsize: 21744 Current children cumulated CPU time (s) 649.58 Current children cumulated vsize (Kb) 23868 [startup+660.062 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 21060 Raw data (/proc/21054/stat): 21054 (minisat+_script) S 21053 21054 20115 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855448975 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/21054/statm): 531 226 485 147 0 384 0 [pid=21054] vsize: 2124 Raw data (/proc/21058/stat): 21058 (minisat+_64-bit) R 21054 21054 20115 0 -1 0 5277 0 0 0 65910 47 0 0 25 0 1 0 1855448980 22265856 5228 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/21058/statm): 5436 5228 145 145 0 5291 0 [pid=21058] vsize: 21744 Current children cumulated CPU time (s) 659.57 Current children cumulated vsize (Kb) 23868 [startup+670.063 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 21060 Raw data (/proc/21054/stat): 21054 (minisat+_script) S 21053 21054 20115 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855448975 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/21054/statm): 531 226 485 147 0 384 0 [pid=21054] vsize: 2124 Raw data (/proc/21058/stat): 21058 (minisat+_64-bit) R 21054 21054 20115 0 -1 0 5277 0 0 0 66896 47 0 0 25 0 1 0 1855448980 22265856 5228 4294967295 134512640 135094434 3221224448 3221223104 134558002 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/21058/statm): 5436 5228 145 145 0 5291 0 [pid=21058] vsize: 21744 Current children cumulated CPU time (s) 669.43 Current children cumulated vsize (Kb) 23868 [startup+680.065 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 21060 Raw data (/proc/21054/stat): 21054 (minisat+_script) S 21053 21054 20115 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855448975 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/21054/statm): 531 226 485 147 0 384 0 [pid=21054] vsize: 2124 Raw data (/proc/21058/stat): 21058 (minisat+_64-bit) R 21054 21054 20115 0 -1 0 5277 0 0 0 67896 47 0 0 25 0 1 0 1855448980 22265856 5228 4294967295 134512640 135094434 3221224448 3221223072 134557717 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/21058/statm): 5436 5228 145 145 0 5291 0 [pid=21058] vsize: 21744 Current children cumulated CPU time (s) 679.43 Current children cumulated vsize (Kb) 23868 [startup+690.065 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 21060 Raw data (/proc/21054/stat): 21054 (minisat+_script) S 21053 21054 20115 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855448975 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/21054/statm): 531 226 485 147 0 384 0 [pid=21054] vsize: 2124 Raw data (/proc/21058/stat): 21058 (minisat+_64-bit) R 21054 21054 20115 0 -1 0 5277 0 0 0 68896 47 0 0 25 0 1 0 1855448980 22265856 5228 4294967295 134512640 135094434 3221224448 3221223104 134557937 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/21058/statm): 5436 5228 145 145 0 5291 0 [pid=21058] vsize: 21744 Current children cumulated CPU time (s) 689.43 Current children cumulated vsize (Kb) 23868 [startup+700.066 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 21060 Raw data (/proc/21054/stat): 21054 (minisat+_script) S 21053 21054 20115 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855448975 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/21054/statm): 531 226 485 147 0 384 0 [pid=21054] vsize: 2124 Raw data (/proc/21058/stat): 21058 (minisat+_64-bit) R 21054 21054 20115 0 -1 0 5277 0 0 0 69897 47 0 0 25 0 1 0 1855448980 22265856 5228 4294967295 134512640 135094434 3221224448 3221223120 134555579 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/21058/statm): 5436 5228 145 145 0 5291 0 [pid=21058] vsize: 21744 Current children cumulated CPU time (s) 699.44 Current children cumulated vsize (Kb) 23868 [startup+710.067 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 21060 Raw data (/proc/21054/stat): 21054 (minisat+_script) S 21053 21054 20115 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855448975 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/21054/statm): 531 226 485 147 0 384 0 [pid=21054] vsize: 2124 Raw data (/proc/21058/stat): 21058 (minisat+_64-bit) R 21054 21054 20115 0 -1 0 5277 0 0 0 70897 47 0 0 25 0 1 0 1855448980 22265856 5228 4294967295 134512640 135094434 3221224448 3221223104 134558009 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/21058/statm): 5436 5228 145 145 0 5291 0 [pid=21058] vsize: 21744 Current children cumulated CPU time (s) 709.44 Current children cumulated vsize (Kb) 23868 [startup+720.067 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 21060 Raw data (/proc/21054/stat): 21054 (minisat+_script) S 21053 21054 20115 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855448975 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/21054/statm): 531 226 485 147 0 384 0 [pid=21054] vsize: 2124 Raw data (/proc/21058/stat): 21058 (minisat+_64-bit) R 21054 21054 20115 0 -1 0 5277 0 0 0 71897 47 0 0 25 0 1 0 1855448980 22265856 5228 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/21058/statm): 5436 5228 145 145 0 5291 0 [pid=21058] vsize: 21744 Current children cumulated CPU time (s) 719.44 Current children cumulated vsize (Kb) 23868 [startup+730.069 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 21060 Raw data (/proc/21054/stat): 21054 (minisat+_script) S 21053 21054 20115 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855448975 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/21054/statm): 531 226 485 147 0 384 0 [pid=21054] vsize: 2124 Raw data (/proc/21058/stat): 21058 (minisat+_64-bit) R 21054 21054 20115 0 -1 0 5277 0 0 0 72897 47 0 0 25 0 1 0 1855448980 22265856 5228 4294967295 134512640 135094434 3221224448 3221223040 134557273 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/21058/statm): 5436 5228 145 145 0 5291 0 [pid=21058] vsize: 21744 Current children cumulated CPU time (s) 729.44 Current children cumulated vsize (Kb) 23868 [startup+740.07 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 21060 Raw data (/proc/21054/stat): 21054 (minisat+_script) S 21053 21054 20115 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855448975 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/21054/statm): 531 226 485 147 0 384 0 [pid=21054] vsize: 2124 Raw data (/proc/21058/stat): 21058 (minisat+_64-bit) R 21054 21054 20115 0 -1 0 5277 0 0 0 73897 47 0 0 25 0 1 0 1855448980 22265856 5228 4294967295 134512640 135094434 3221224448 3221223104 134557843 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/21058/statm): 5436 5228 145 145 0 5291 0 [pid=21058] vsize: 21744 Current children cumulated CPU time (s) 739.44 Current children cumulated vsize (Kb) 23868 [startup+750.07 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 21060 Raw data (/proc/21054/stat): 21054 (minisat+_script) S 21053 21054 20115 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855448975 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/21054/statm): 531 226 485 147 0 384 0 [pid=21054] vsize: 2124 Raw data (/proc/21058/stat): 21058 (minisat+_64-bit) R 21054 21054 20115 0 -1 0 5277 0 0 0 74897 47 0 0 25 0 1 0 1855448980 22265856 5228 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/21058/statm): 5436 5228 145 145 0 5291 0 [pid=21058] vsize: 21744 Current children cumulated CPU time (s) 749.44 Current children cumulated vsize (Kb) 23868 [startup+760.071 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 21060 Raw data (/proc/21054/stat): 21054 (minisat+_script) S 21053 21054 20115 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855448975 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/21054/statm): 531 226 485 147 0 384 0 [pid=21054] vsize: 2124 Raw data (/proc/21058/stat): 21058 (minisat+_64-bit) R 21054 21054 20115 0 -1 0 5277 0 0 0 75897 47 0 0 25 0 1 0 1855448980 22265856 5228 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/21058/statm): 5436 5228 145 145 0 5291 0 [pid=21058] vsize: 21744 Current children cumulated CPU time (s) 759.44 Current children cumulated vsize (Kb) 23868 [startup+770.072 s] Raw data (loadavg): 0.99 0.97 0.91 3/57 21060 Raw data (/proc/21054/stat): 21054 (minisat+_script) S 21053 21054 20115 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855448975 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/21054/statm): 531 226 485 147 0 384 0 [pid=21054] vsize: 2124 Raw data (/proc/21058/stat): 21058 (minisat+_64-bit) R 21054 21054 20115 0 -1 0 5277 0 0 0 77198 47 0 0 25 0 1 0 1855448980 22265856 5228 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/21058/statm): 5436 5228 145 145 0 5291 0 [pid=21058] vsize: 21744 Current children cumulated CPU time (s) 772.45 Current children cumulated vsize (Kb) 23868 [startup+783.08 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 21060 Raw data (/proc/21054/stat): 21054 (minisat+_script) S 21053 21054 20115 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855448975 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/21054/statm): 531 226 485 147 0 384 0 [pid=21054] vsize: 2124 Raw data (/proc/21058/stat): 21058 (minisat+_64-bit) R 21054 21054 20115 0 -1 0 5277 0 0 0 78199 47 0 0 25 0 1 0 1855448980 22265856 5228 4294967295 134512640 135094434 3221224448 3221223104 134557884 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/21058/statm): 5436 5228 145 145 0 5291 0 [pid=21058] vsize: 21744 Current children cumulated CPU time (s) 782.46 Current children cumulated vsize (Kb) 23868 [startup+793.08 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 21060 Raw data (/proc/21054/stat): 21054 (minisat+_script) S 21053 21054 20115 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855448975 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/21054/statm): 531 226 485 147 0 384 0 [pid=21054] vsize: 2124 Raw data (/proc/21058/stat): 21058 (minisat+_64-bit) R 21054 21054 20115 0 -1 0 5277 0 0 0 79199 48 0 0 25 0 1 0 1855448980 22265856 5228 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/21058/statm): 5436 5228 145 145 0 5291 0 [pid=21058] vsize: 21744 Current children cumulated CPU time (s) 792.47 Current children cumulated vsize (Kb) 23868 [startup+803.081 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 21060 Raw data (/proc/21054/stat): 21054 (minisat+_script) S 21053 21054 20115 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855448975 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/21054/statm): 531 226 485 147 0 384 0 [pid=21054] vsize: 2124 Raw data (/proc/21058/stat): 21058 (minisat+_64-bit) R 21054 21054 20115 0 -1 0 5277 0 0 0 80199 48 0 0 25 0 1 0 1855448980 22265856 5228 4294967295 134512640 135094434 3221224448 3221223104 134557884 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/21058/statm): 5436 5228 145 145 0 5291 0 [pid=21058] vsize: 21744 Current children cumulated CPU time (s) 802.47 Current children cumulated vsize (Kb) 23868 [startup+813.082 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 21060 Raw data (/proc/21054/stat): 21054 (minisat+_script) S 21053 21054 20115 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855448975 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/21054/statm): 531 226 485 147 0 384 0 [pid=21054] vsize: 2124 Raw data (/proc/21058/stat): 21058 (minisat+_64-bit) R 21054 21054 20115 0 -1 0 5277 0 0 0 81199 48 0 0 25 0 1 0 1855448980 22265856 5228 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/21058/statm): 5436 5228 145 145 0 5291 0 [pid=21058] vsize: 21744 Current children cumulated CPU time (s) 812.47 Current children cumulated vsize (Kb) 23868 [startup+823.082 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 21060 Raw data (/proc/21054/stat): 21054 (minisat+_script) S 21053 21054 20115 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855448975 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/21054/statm): 531 226 485 147 0 384 0 [pid=21054] vsize: 2124 Raw data (/proc/21058/stat): 21058 (minisat+_64-bit) R 21054 21054 20115 0 -1 0 5277 0 0 0 82199 48 0 0 25 0 1 0 1855448980 22265856 5228 4294967295 134512640 135094434 3221224448 3221223072 134557598 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/21058/statm): 5436 5228 145 145 0 5291 0 [pid=21058] vsize: 21744 Current children cumulated CPU time (s) 822.47 Current children cumulated vsize (Kb) 23868 [startup+833.083 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 21060 Raw data (/proc/21054/stat): 21054 (minisat+_script) S 21053 21054 20115 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855448975 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/21054/statm): 531 226 485 147 0 384 0 [pid=21054] vsize: 2124 Raw data (/proc/21058/stat): 21058 (minisat+_64-bit) R 21054 21054 20115 0 -1 0 5277 0 0 0 83199 48 0 0 25 0 1 0 1855448980 22265856 5228 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/21058/statm): 5436 5228 145 145 0 5291 0 [pid=21058] vsize: 21744 Current children cumulated CPU time (s) 832.47 Current children cumulated vsize (Kb) 23868 [startup+843.084 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 21060 Raw data (/proc/21054/stat): 21054 (minisat+_script) S 21053 21054 20115 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855448975 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/21054/statm): 531 226 485 147 0 384 0 [pid=21054] vsize: 2124 Raw data (/proc/21058/stat): 21058 (minisat+_64-bit) R 21054 21054 20115 0 -1 0 5277 0 0 0 84199 48 0 0 25 0 1 0 1855448980 22265856 5228 4294967295 134512640 135094434 3221224448 3221223136 134554687 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/21058/statm): 5436 5228 145 145 0 5291 0 [pid=21058] vsize: 21744 Current children cumulated CPU time (s) 842.47 Current children cumulated vsize (Kb) 23868 [startup+853.084 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 21060 Raw data (/proc/21054/stat): 21054 (minisat+_script) S 21053 21054 20115 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855448975 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/21054/statm): 531 226 485 147 0 384 0 [pid=21054] vsize: 2124 Raw data (/proc/21058/stat): 21058 (minisat+_64-bit) R 21054 21054 20115 0 -1 0 5277 0 0 0 85200 48 0 0 25 0 1 0 1855448980 22265856 5228 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/21058/statm): 5436 5228 145 145 0 5291 0 [pid=21058] vsize: 21744 Current children cumulated CPU time (s) 852.48 Current children cumulated vsize (Kb) 23868 [startup+863.085 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 21060 Raw data (/proc/21054/stat): 21054 (minisat+_script) S 21053 21054 20115 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855448975 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/21054/statm): 531 226 485 147 0 384 0 [pid=21054] vsize: 2124 Raw data (/proc/21058/stat): 21058 (minisat+_64-bit) R 21054 21054 20115 0 -1 0 5277 0 0 0 86199 48 0 0 25 0 1 0 1855448980 22265856 5228 4294967295 134512640 135094434 3221224448 3221223136 134554746 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/21058/statm): 5436 5228 145 145 0 5291 0 [pid=21058] vsize: 21744 Current children cumulated CPU time (s) 862.47 Current children cumulated vsize (Kb) 23868 [startup+873.086 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 21060 Raw data (/proc/21054/stat): 21054 (minisat+_script) S 21053 21054 20115 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855448975 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/21054/statm): 531 226 485 147 0 384 0 [pid=21054] vsize: 2124 Raw data (/proc/21058/stat): 21058 (minisat+_64-bit) R 21054 21054 20115 0 -1 0 5277 0 0 0 87200 48 0 0 25 0 1 0 1855448980 22265856 5228 4294967295 134512640 135094434 3221224448 3221223104 134557948 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/21058/statm): 5436 5228 145 145 0 5291 0 [pid=21058] vsize: 21744 Current children cumulated CPU time (s) 872.48 Current children cumulated vsize (Kb) 23868 [startup+883.086 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 21060 Raw data (/proc/21054/stat): 21054 (minisat+_script) S 21053 21054 20115 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855448975 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/21054/statm): 531 226 485 147 0 384 0 [pid=21054] vsize: 2124 Raw data (/proc/21058/stat): 21058 (minisat+_64-bit) R 21054 21054 20115 0 -1 0 5277 0 0 0 88200 48 0 0 25 0 1 0 1855448980 22265856 5228 4294967295 134512640 135094434 3221224448 3221223120 134556266 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/21058/statm): 5436 5228 145 145 0 5291 0 [pid=21058] vsize: 21744 Current children cumulated CPU time (s) 882.48 Current children cumulated vsize (Kb) 23868 [startup+893.087 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 21060 Raw data (/proc/21054/stat): 21054 (minisat+_script) S 21053 21054 20115 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855448975 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/21054/statm): 531 226 485 147 0 384 0 [pid=21054] vsize: 2124 Raw data (/proc/21058/stat): 21058 (minisat+_64-bit) R 21054 21054 20115 0 -1 0 5277 0 0 0 89200 48 0 0 25 0 1 0 1855448980 22265856 5228 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/21058/statm): 5436 5228 145 145 0 5291 0 [pid=21058] vsize: 21744 Current children cumulated CPU time (s) 892.48 Current children cumulated vsize (Kb) 23868 [startup+903.088 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 21060 Raw data (/proc/21054/stat): 21054 (minisat+_script) S 21053 21054 20115 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855448975 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/21054/statm): 531 226 485 147 0 384 0 [pid=21054] vsize: 2124 Raw data (/proc/21058/stat): 21058 (minisat+_64-bit) R 21054 21054 20115 0 -1 0 5277 0 0 0 90200 48 0 0 25 0 1 0 1855448980 22265856 5228 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/21058/statm): 5436 5228 145 145 0 5291 0 [pid=21058] vsize: 21744 Current children cumulated CPU time (s) 902.48 Current children cumulated vsize (Kb) 23868 [startup+913.088 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 21060 Raw data (/proc/21054/stat): 21054 (minisat+_script) S 21053 21054 20115 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855448975 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/21054/statm): 531 226 485 147 0 384 0 [pid=21054] vsize: 2124 Raw data (/proc/21058/stat): 21058 (minisat+_64-bit) R 21054 21054 20115 0 -1 0 5277 0 0 0 91201 48 0 0 25 0 1 0 1855448980 22265856 5228 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/21058/statm): 5436 5228 145 145 0 5291 0 [pid=21058] vsize: 21744 Current children cumulated CPU time (s) 912.49 Current children cumulated vsize (Kb) 23868 [startup+923.089 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 21060 Raw data (/proc/21054/stat): 21054 (minisat+_script) S 21053 21054 20115 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855448975 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/21054/statm): 531 226 485 147 0 384 0 [pid=21054] vsize: 2124 Raw data (/proc/21058/stat): 21058 (minisat+_64-bit) R 21054 21054 20115 0 -1 0 5277 0 0 0 92201 48 0 0 25 0 1 0 1855448980 22265856 5228 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/21058/statm): 5436 5228 145 145 0 5291 0 [pid=21058] vsize: 21744 Current children cumulated CPU time (s) 922.49 Current children cumulated vsize (Kb) 23868 [startup+933.09 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 21060 Raw data (/proc/21054/stat): 21054 (minisat+_script) S 21053 21054 20115 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855448975 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/21054/statm): 531 226 485 147 0 384 0 [pid=21054] vsize: 2124 Raw data (/proc/21058/stat): 21058 (minisat+_64-bit) R 21054 21054 20115 0 -1 0 5277 0 0 0 93201 48 0 0 25 0 1 0 1855448980 22265856 5228 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/21058/statm): 5436 5228 145 145 0 5291 0 [pid=21058] vsize: 21744 Current children cumulated CPU time (s) 932.49 Current children cumulated vsize (Kb) 23868 [startup+943.09 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 21060 Raw data (/proc/21054/stat): 21054 (minisat+_script) S 21053 21054 20115 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855448975 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/21054/statm): 531 226 485 147 0 384 0 [pid=21054] vsize: 2124 Raw data (/proc/21058/stat): 21058 (minisat+_64-bit) R 21054 21054 20115 0 -1 0 5277 0 0 0 94201 48 0 0 25 0 1 0 1855448980 22265856 5228 4294967295 134512640 135094434 3221224448 3221223104 134558249 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/21058/statm): 5436 5228 145 145 0 5291 0 [pid=21058] vsize: 21744 Current children cumulated CPU time (s) 942.49 Current children cumulated vsize (Kb) 23868 [startup+953.091 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 21060 Raw data (/proc/21054/stat): 21054 (minisat+_script) S 21053 21054 20115 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855448975 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/21054/statm): 531 226 485 147 0 384 0 [pid=21054] vsize: 2124 Raw data (/proc/21058/stat): 21058 (minisat+_64-bit) R 21054 21054 20115 0 -1 0 5277 0 0 0 95201 49 0 0 25 0 1 0 1855448980 22265856 5228 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/21058/statm): 5436 5228 145 145 0 5291 0 [pid=21058] vsize: 21744 Current children cumulated CPU time (s) 952.5 Current children cumulated vsize (Kb) 23868 [startup+963.093 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 21060 Raw data (/proc/21054/stat): 21054 (minisat+_script) S 21053 21054 20115 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855448975 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/21054/statm): 531 226 485 147 0 384 0 [pid=21054] vsize: 2124 Raw data (/proc/21058/stat): 21058 (minisat+_64-bit) R 21054 21054 20115 0 -1 0 5277 0 0 0 96202 49 0 0 25 0 1 0 1855448980 22265856 5228 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/21058/statm): 5436 5228 145 145 0 5291 0 [pid=21058] vsize: 21744 Current children cumulated CPU time (s) 962.51 Current children cumulated vsize (Kb) 23868 [startup+973.093 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 21060 Raw data (/proc/21054/stat): 21054 (minisat+_script) S 21053 21054 20115 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855448975 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/21054/statm): 531 226 485 147 0 384 0 [pid=21054] vsize: 2124 Raw data (/proc/21058/stat): 21058 (minisat+_64-bit) R 21054 21054 20115 0 -1 0 5277 0 0 0 97202 49 0 0 25 0 1 0 1855448980 22265856 5228 4294967295 134512640 135094434 3221224448 3221223104 134557945 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/21058/statm): 5436 5228 145 145 0 5291 0 [pid=21058] vsize: 21744 Current children cumulated CPU time (s) 972.51 Current children cumulated vsize (Kb) 23868 [startup+983.094 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 21060 Raw data (/proc/21054/stat): 21054 (minisat+_script) S 21053 21054 20115 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855448975 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/21054/statm): 531 226 485 147 0 384 0 [pid=21054] vsize: 2124 Raw data (/proc/21058/stat): 21058 (minisat+_64-bit) R 21054 21054 20115 0 -1 0 5277 0 0 0 98201 50 0 0 25 0 1 0 1855448980 22265856 5228 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/21058/statm): 5436 5228 145 145 0 5291 0 [pid=21058] vsize: 21744 Current children cumulated CPU time (s) 982.51 Current children cumulated vsize (Kb) 23868 [startup+993.095 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 21060 Raw data (/proc/21054/stat): 21054 (minisat+_script) S 21053 21054 20115 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855448975 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/21054/statm): 531 226 485 147 0 384 0 [pid=21054] vsize: 2124 Raw data (/proc/21058/stat): 21058 (minisat+_64-bit) R 21054 21054 20115 0 -1 0 5277 0 0 0 99201 50 0 0 25 0 1 0 1855448980 22265856 5228 4294967295 134512640 135094434 3221224448 3221223104 134557863 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/21058/statm): 5436 5228 145 145 0 5291 0 [pid=21058] vsize: 21744 Current children cumulated CPU time (s) 992.51 Current children cumulated vsize (Kb) 23868 [startup+1003.1 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 21060 Raw data (/proc/21054/stat): 21054 (minisat+_script) S 21053 21054 20115 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855448975 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/21054/statm): 531 226 485 147 0 384 0 [pid=21054] vsize: 2124 Raw data (/proc/21058/stat): 21058 (minisat+_64-bit) R 21054 21054 20115 0 -1 0 5442 0 0 0 100198 52 0 0 25 0 1 0 1855448980 22941696 5393 4294967295 134512640 135094434 3221224448 3221223104 134557903 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/21058/statm): 5601 5393 145 145 0 5456 0 [pid=21058] vsize: 22404 Current children cumulated CPU time (s) 1002.5 Current children cumulated vsize (Kb) 24528 [startup+1013.1 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 21060 Raw data (/proc/21054/stat): 21054 (minisat+_script) S 21053 21054 20115 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855448975 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/21054/statm): 531 226 485 147 0 384 0 [pid=21054] vsize: 2124 Raw data (/proc/21058/stat): 21058 (minisat+_64-bit) R 21054 21054 20115 0 -1 0 5443 0 0 0 101198 53 0 0 25 0 1 0 1855448980 22941696 5394 4294967295 134512640 135094434 3221224448 3221223104 134558235 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/21058/statm): 5601 5394 145 145 0 5456 0 [pid=21058] vsize: 22404 Current children cumulated CPU time (s) 1012.51 Current children cumulated vsize (Kb) 24528 [startup+1023.1 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 21060 Raw data (/proc/21054/stat): 21054 (minisat+_script) S 21053 21054 20115 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855448975 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/21054/statm): 531 226 485 147 0 384 0 [pid=21054] vsize: 2124 Raw data (/proc/21058/stat): 21058 (minisat+_64-bit) R 21054 21054 20115 0 -1 0 5443 0 0 0 102198 53 0 0 25 0 1 0 1855448980 22941696 5394 4294967295 134512640 135094434 3221224448 3221223104 134557948 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/21058/statm): 5601 5394 145 145 0 5456 0 [pid=21058] vsize: 22404 Current children cumulated CPU time (s) 1022.51 Current children cumulated vsize (Kb) 24528 [startup+1033.1 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 21060 Raw data (/proc/21054/stat): 21054 (minisat+_script) S 21053 21054 20115 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855448975 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/21054/statm): 531 226 485 147 0 384 0 [pid=21054] vsize: 2124 Raw data (/proc/21058/stat): 21058 (minisat+_64-bit) R 21054 21054 20115 0 -1 0 5443 0 0 0 103198 53 0 0 25 0 1 0 1855448980 22941696 5394 4294967295 134512640 135094434 3221224448 3221223040 134557208 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/21058/statm): 5601 5394 145 145 0 5456 0 [pid=21058] vsize: 22404 Current children cumulated CPU time (s) 1032.51 Current children cumulated vsize (Kb) 24528 [startup+1043.1 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 21060 Raw data (/proc/21054/stat): 21054 (minisat+_script) S 21053 21054 20115 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855448975 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/21054/statm): 531 226 485 147 0 384 0 [pid=21054] vsize: 2124 Raw data (/proc/21058/stat): 21058 (minisat+_64-bit) R 21054 21054 20115 0 -1 0 5443 0 0 0 104198 53 0 0 25 0 1 0 1855448980 22941696 5394 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/21058/statm): 5601 5394 145 145 0 5456 0 [pid=21058] vsize: 22404 Current children cumulated CPU time (s) 1042.51 Current children cumulated vsize (Kb) 24528 [startup+1053.1 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 21060 Raw data (/proc/21054/stat): 21054 (minisat+_script) S 21053 21054 20115 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855448975 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/21054/statm): 531 226 485 147 0 384 0 [pid=21054] vsize: 2124 Raw data (/proc/21058/stat): 21058 (minisat+_64-bit) R 21054 21054 20115 0 -1 0 5443 0 0 0 105199 53 0 0 25 0 1 0 1855448980 22941696 5394 4294967295 134512640 135094434 3221224448 3221223104 134558178 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/21058/statm): 5601 5394 145 145 0 5456 0 [pid=21058] vsize: 22404 Current children cumulated CPU time (s) 1052.52 Current children cumulated vsize (Kb) 24528 [startup+1063.1 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 21060 Raw data (/proc/21054/stat): 21054 (minisat+_script) S 21053 21054 20115 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855448975 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/21054/statm): 531 226 485 147 0 384 0 [pid=21054] vsize: 2124 Raw data (/proc/21058/stat): 21058 (minisat+_64-bit) R 21054 21054 20115 0 -1 0 5443 0 0 0 106199 54 0 0 25 0 1 0 1855448980 22941696 5394 4294967295 134512640 135094434 3221224448 3221223136 134554760 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/21058/statm): 5601 5394 145 145 0 5456 0 [pid=21058] vsize: 22404 Current children cumulated CPU time (s) 1062.53 Current children cumulated vsize (Kb) 24528 [startup+1073.1 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 21060 Raw data (/proc/21054/stat): 21054 (minisat+_script) S 21053 21054 20115 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855448975 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/21054/statm): 531 226 485 147 0 384 0 [pid=21054] vsize: 2124 Raw data (/proc/21058/stat): 21058 (minisat+_64-bit) R 21054 21054 20115 0 -1 0 5448 0 0 0 107199 54 0 0 25 0 1 0 1855448980 22974464 5399 4294967295 134512640 135094434 3221224448 3221223104 134557948 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/21058/statm): 5609 5399 145 145 0 5464 0 [pid=21058] vsize: 22436 Current children cumulated CPU time (s) 1072.53 Current children cumulated vsize (Kb) 24560 [startup+1083.1 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 21060 Raw data (/proc/21054/stat): 21054 (minisat+_script) S 21053 21054 20115 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855448975 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/21054/statm): 531 226 485 147 0 384 0 [pid=21054] vsize: 2124 Raw data (/proc/21058/stat): 21058 (minisat+_64-bit) R 21054 21054 20115 0 -1 0 5537 0 0 0 108197 55 0 0 25 0 1 0 1855448980 23343104 5488 4294967295 134512640 135094434 3221224448 3221223104 134557866 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/21058/statm): 5699 5488 145 145 0 5554 0 [pid=21058] vsize: 22796 Current children cumulated CPU time (s) 1082.52 Current children cumulated vsize (Kb) 24920 [startup+1093.1 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 21060 Raw data (/proc/21054/stat): 21054 (minisat+_script) S 21053 21054 20115 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855448975 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/21054/statm): 531 226 485 147 0 384 0 [pid=21054] vsize: 2124 Raw data (/proc/21058/stat): 21058 (minisat+_64-bit) R 21054 21054 20115 0 -1 0 5728 0 0 0 109193 56 0 0 25 0 1 0 1855448980 24129536 5679 4294967295 134512640 135094434 3221224448 3221223104 134557849 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/21058/statm): 5891 5679 145 145 0 5746 0 [pid=21058] vsize: 23564 Current children cumulated CPU time (s) 1092.49 Current children cumulated vsize (Kb) 25688 [startup+1103.11 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 21060 Raw data (/proc/21054/stat): 21054 (minisat+_script) S 21053 21054 20115 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855448975 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/21054/statm): 531 226 485 147 0 384 0 [pid=21054] vsize: 2124 Raw data (/proc/21058/stat): 21058 (minisat+_64-bit) R 21054 21054 20115 0 -1 0 5893 0 0 0 110189 58 0 0 25 0 1 0 1855448980 24801280 5844 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/21058/statm): 6055 5844 145 145 0 5910 0 [pid=21058] vsize: 24220 Current children cumulated CPU time (s) 1102.47 Current children cumulated vsize (Kb) 26344 [startup+1113.11 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 21060 Raw data (/proc/21054/stat): 21054 (minisat+_script) S 21053 21054 20115 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855448975 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/21054/statm): 531 226 485 147 0 384 0 [pid=21054] vsize: 2124 Raw data (/proc/21058/stat): 21058 (minisat+_64-bit) R 21054 21054 20115 0 -1 0 6036 0 0 0 111187 59 0 0 25 0 1 0 1855448980 25374720 5987 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/21058/statm): 6195 5987 145 145 0 6050 0 [pid=21058] vsize: 24780 Current children cumulated CPU time (s) 1112.46 Current children cumulated vsize (Kb) 26904 [startup+1123.11 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 21060 Raw data (/proc/21054/stat): 21054 (minisat+_script) S 21053 21054 20115 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855448975 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/21054/statm): 531 226 485 147 0 384 0 [pid=21054] vsize: 2124 Raw data (/proc/21058/stat): 21058 (minisat+_64-bit) R 21054 21054 20115 0 -1 0 6036 0 0 0 112187 59 0 0 25 0 1 0 1855448980 25374720 5987 4294967295 134512640 135094434 3221224448 3221223120 134556266 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/21058/statm): 6195 5987 145 145 0 6050 0 [pid=21058] vsize: 24780 Current children cumulated CPU time (s) 1122.46 Current children cumulated vsize (Kb) 26904 [startup+1133.11 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 21060 Raw data (/proc/21054/stat): 21054 (minisat+_script) S 21053 21054 20115 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855448975 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/21054/statm): 531 226 485 147 0 384 0 [pid=21054] vsize: 2124 Raw data (/proc/21058/stat): 21058 (minisat+_64-bit) R 21054 21054 20115 0 -1 0 6036 0 0 0 113187 59 0 0 25 0 1 0 1855448980 25374720 5987 4294967295 134512640 135094434 3221224448 3221223104 134557937 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/21058/statm): 6195 5987 145 145 0 6050 0 [pid=21058] vsize: 24780 Current children cumulated CPU time (s) 1132.46 Current children cumulated vsize (Kb) 26904 [startup+1143.11 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 21060 Raw data (/proc/21054/stat): 21054 (minisat+_script) S 21053 21054 20115 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855448975 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/21054/statm): 531 226 485 147 0 384 0 [pid=21054] vsize: 2124 Raw data (/proc/21058/stat): 21058 (minisat+_64-bit) R 21054 21054 20115 0 -1 0 6036 0 0 0 114188 59 0 0 25 0 1 0 1855448980 25374720 5987 4294967295 134512640 135094434 3221224448 3221223104 134558213 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/21058/statm): 6195 5987 145 145 0 6050 0 [pid=21058] vsize: 24780 Current children cumulated CPU time (s) 1142.47 Current children cumulated vsize (Kb) 26904 [startup+1153.11 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 21060 Raw data (/proc/21054/stat): 21054 (minisat+_script) S 21053 21054 20115 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855448975 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/21054/statm): 531 226 485 147 0 384 0 [pid=21054] vsize: 2124 Raw data (/proc/21058/stat): 21058 (minisat+_64-bit) R 21054 21054 20115 0 -1 0 6036 0 0 0 115188 59 0 0 25 0 1 0 1855448980 25374720 5987 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/21058/statm): 6195 5987 145 145 0 6050 0 [pid=21058] vsize: 24780 Current children cumulated CPU time (s) 1152.47 Current children cumulated vsize (Kb) 26904 [startup+1163.11 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 21060 Raw data (/proc/21054/stat): 21054 (minisat+_script) S 21053 21054 20115 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855448975 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/21054/statm): 531 226 485 147 0 384 0 [pid=21054] vsize: 2124 Raw data (/proc/21058/stat): 21058 (minisat+_64-bit) R 21054 21054 20115 0 -1 0 6036 0 0 0 116188 60 0 0 25 0 1 0 1855448980 25374720 5987 4294967295 134512640 135094434 3221224448 3221223104 134558162 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/21058/statm): 6195 5987 145 145 0 6050 0 [pid=21058] vsize: 24780 Current children cumulated CPU time (s) 1162.48 Current children cumulated vsize (Kb) 26904 [startup+1173.11 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 21060 Raw data (/proc/21054/stat): 21054 (minisat+_script) S 21053 21054 20115 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855448975 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/21054/statm): 531 226 485 147 0 384 0 [pid=21054] vsize: 2124 Raw data (/proc/21058/stat): 21058 (minisat+_64-bit) R 21054 21054 20115 0 -1 0 6036 0 0 0 117188 60 0 0 25 0 1 0 1855448980 25374720 5987 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/21058/statm): 6195 5987 145 145 0 6050 0 [pid=21058] vsize: 24780 Current children cumulated CPU time (s) 1172.48 Current children cumulated vsize (Kb) 26904 [startup+1183.11 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 21060 Raw data (/proc/21054/stat): 21054 (minisat+_script) S 21053 21054 20115 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855448975 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/21054/statm): 531 226 485 147 0 384 0 [pid=21054] vsize: 2124 Raw data (/proc/21058/stat): 21058 (minisat+_64-bit) R 21054 21054 20115 0 -1 0 6036 0 0 0 118188 60 0 0 25 0 1 0 1855448980 25374720 5987 4294967295 134512640 135094434 3221224448 3221223072 134557694 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/21058/statm): 6195 5987 145 145 0 6050 0 [pid=21058] vsize: 24780 Current children cumulated CPU time (s) 1182.48 Current children cumulated vsize (Kb) 26904 [startup+1193.11 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 21060 Raw data (/proc/21054/stat): 21054 (minisat+_script) S 21053 21054 20115 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855448975 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/21054/statm): 531 226 485 147 0 384 0 [pid=21054] vsize: 2124 Raw data (/proc/21058/stat): 21058 (minisat+_64-bit) R 21054 21054 20115 0 -1 0 6036 0 0 0 119189 60 0 0 25 0 1 0 1855448980 25374720 5987 4294967295 134512640 135094434 3221224448 3221223104 134557925 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/21058/statm): 6195 5987 145 145 0 6050 0 [pid=21058] vsize: 24780 Current children cumulated CPU time (s) 1192.49 Current children cumulated vsize (Kb) 26904 [startup+1203.11 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 21060 Raw data (/proc/21054/stat): 21054 (minisat+_script) S 21053 21054 20115 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855448975 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/21054/statm): 531 226 485 147 0 384 0 [pid=21054] vsize: 2124 Raw data (/proc/21058/stat): 21058 (minisat+_64-bit) R 21054 21054 20115 0 -1 0 6036 0 0 0 120189 60 0 0 25 0 1 0 1855448980 25374720 5987 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/21058/statm): 6195 5987 145 145 0 6050 0 [pid=21058] vsize: 24780 Current children cumulated CPU time (s) 1202.49 Current children cumulated vsize (Kb) 26904 Maximum CPU time exceeded: sending SIGTERM then SIGKILL [startup+1203.11 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 21060 Raw data (/proc/21054/stat): 21054 (minisat+_script) S 21053 21054 20115 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855448975 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/21054/statm): 531 226 485 147 0 384 0 [pid=21054] vsize: 2124 Raw data (/proc/21058/stat): 21058 (minisat+_64-bit) R 21054 21054 20115 0 -1 0 6036 0 0 0 120189 60 0 0 25 0 1 0 1855448980 25374720 5987 4294967295 134512640 135094434 3221224448 3221223104 134558159 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/21058/statm): 6195 5987 145 145 0 6050 0 [pid=21058] vsize: 24780 Current children cumulated CPU time (s) 1202.49 Current children cumulated vsize (Kb) 26904 Sending SIGTERM to -21054 Sleeping 2 seconds One traced child (pid=21054) ended because it received signal 15 (SIGTERM) One traced child (pid=21058) exited with status: 10 All traced children have exited ! Game is over. Child status: 10 Real time (s): 1203.13 CPU time (s): 1202.51 CPU user time (s): 1201.9 CPU system time (s): 0.615906 CPU usage (%): 99.9485 Max. virtual memory (cumulated for all children) (Kb): 26904
ERROR: no interpretation found !