| Name | mps-v2-13-7/MIPLIB/miplib3/normalized-mps-v2-13-7-pk1.opb |
| MD5SUM | b6007187ad037f56a5e2b97a0b86cea8 |
| 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 wulflinc10 THE 2005-09-20 04:34:47 (client local time) PB2005-SCRIPT v4.0 MARKUPS: idlaunch=3384 boxname=wulflinc10 idbench=1040 idsolver=3 numberseed=0 MD5SUM SOLVER: MD5SUM BENCH: b6007187ad037f56a5e2b97a0b86cea8 /oldhome/oroussel/tmp/wulflinc10/normalized-mps-v2-13-7-pk1.opb REAL COMMAND: minisat+_script /oldhome/oroussel/tmp/wulflinc10/normalized-mps-v2-13-7-pk1.opb IDLAUNCH: 3384 /proc/cpuinfo: processor : 0 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 2 cpu MHz : 450.999 cache size : 512 KB fdiv_bug : no hlt_bug : no f00f_bug : no coma_bug : no fpu : yes fpu_exception : yes cpuid level : 2 wp : yes flags : fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse bogomips : 890.88 processor : 1 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 2 cpu MHz : 450.999 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: 785316 kB Buffers: 38508 kB Cached: 183556 kB SwapCached: 228 kB Active: 83776 kB Inactive: 141264 kB HighTotal: 131008 kB HighFree: 6328 kB LowTotal: 903652 kB LowFree: 778988 kB SwapTotal: 2097136 kB SwapFree: 2096756 kB Dirty: 24 kB Writeback: 0 kB Mapped: 6280 kB Slab: 18696 kB Committed_AS: 64128 kB PageTables: 328 kB VmallocTotal: 114680 kB VmallocUsed: 1364 kB VmallocChunk: 113256 kB JOB ENDED THE 2005-09-20 04:54:57 (client local time) WITH STATUS 10 IN 1209.6 SECONDS stats: 3384 7 1209.6 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 -d_bit_7 -d_bit_6 -d_bit_5 d_bit_4 d_bit_3 -d_bit_2 -d_bit_1 -d_bit0 d_bit1 -d_bit2 -d_bit3 d_bit4 -d_bit5 d_bit6 -d_bit7 -d_bit8 -d_bit9 -d_bit10 -d_bit11 -d_bit12 -X1_bit0 -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 -S1_bit_7 -S1_bit_6 -S1_bit_5 -S1_bit_4 -S1_bit_3 -S1_bit_2 -S1_bit_1 -S1_bit0 -S1_bit1 S1_bit2 -S1_bit3 S1_bit4 -S1_bit5 -S1_bit6 -S1_bit7 -S1_bit8 -S1_bit9 -S1_bit10 -S1_bit11 -S1_bit12 -T1_bit_7 -T1_bit_6 -T1_bit_5 -T1_bit_4 -T1_bit_3 -T1_bit_2 -T1_bit_1 T1_bit0 T1_bit1 -T1_bit2 -T1_bit3 T1_bit4 T1_bit5 -T1_bit6 -T1_bit7 -T1_bit8 -T1_bit9 -T1_bit10 -T1_bit11 -T1_bit12 -S10_bit_7 -S10_bit_6 -S10_bit_5 -S10_bit_4 -S10_bit_3 -S10_bit_2 -S10_bit_1 -S10_bit0 -S10_bit1 -S10_bit2 S10_bit3 -S10_bit4 -S10_bit5 -S10_bit6 -S10_bit7 -S10_bit8 -S10_bit9 -S10_bit10 -S10_bit11 -S10_bit12 -T10_bit_7 -T10_bit_6 -T10_bit_5 -T10_bit_4 -T10_bit_3 -T10_bit_2 -T10_bit_1 T10_bit0 -T10_bit1 -T10_bit2 -T10_bit3 T10_bit4 -T10_bit5 T10_bit6 -T10_bit7 -T10_bit8 -T10_bit9 -T10_bit10 -T10_bit11 -T10_bit12 -S11_bit_7 -S11_bit_6 -S11_bit_5 -S11_bit_4 -S11_bit_3 -S11_bit_2 -S11_bit_1 -S11_bit0 -S11_bit1 -S11_bit2 -S11_bit3 S11_bit4 S11_bit5 -S11_bit6 -S11_bit7 -S11_bit8 -S11_bit9 -S11_bit10 -S11_bit11 -S11_bit12 -T11_bit_7 -T11_bit_6 -T11_bit_5 -T11_bit_4 -T11_bit_3 -T11_bit_2 -T11_bit_1 T11_bit0 -T11_bit1 T11_bit2 T11_bit3 -T11_bit4 -T11_bit5 -T11_bit6 -T11_bit7 -T11_bit8 -T11_bit9 -T11_bit10 -T11_bit11 -T11_bit12 -S12_bit_7 -S12_bit_6 -S12_bit_5 -S12_bit_4 -S12_bit_3 -S12_bit_2 -S12_bit_1 -S12_bit0 S12_bit1 -S12_bit2 S12_bit3 S12_bit4 -S12_bit5 -S12_bit6 -S12_bit7 -S12_bit8 -S12_bit9 -S12_bit10 -S12_bit11 -S12_bit12 -T12_bit_7 -T12_bit_6 -T12_bit_5 -T12_bit_4 -T12_bit_3 -T12_bit_2 -T12_bit_1 T12_bit0 -T12_bit1 T12_bit2 -T12_bit3 -T12_bit4 -T12_bit5 T12_bit6 -T12_bit7 -T12_bit8 -T12_bit9 -T12_bit10 -T12_bit11 -T12_bit12 -S13_bit_7 -S13_bit_6 -S13_bit_5 -S13_bit_4 -S13_bit_3 -S13_bit_2 -S13_bit_1 S13_bit0 -S13_bit1 -S13_bit2 -S13_bit3 S13_bit4 -S13_bit5 -S13_bit6 -S13_bit7 -S13_bit8 -S13_bit9 -S13_bit10 -S13_bit11 -S13_bit12 -T13_bit_7 -T13_bit_6 -T13_bit_5 -T13_bit_4 -T13_bit_3 -T13_bit_2 -T13_bit_1 -T13_bit0 -T13_bit1 -T13_bit2 T13_bit3 -T13_bit4 -T13_bit5 T13_bit6 -T13_bit7 -T13_bit8 -T13_bit9 -T13_bit10 -T13_bit11 -T13_bit12 -S14_bit_7 -S14_bit_6 -S14_bit_5 -S14_bit_4 -S14_bit_3 -S14_bit_2 -S14_bit_1 -S14_bit0 S14_bit1 S14_bit2 -S14_bit3 -S14_bit4 -S14_bit5 S14_bit6 -S14_bit7 -S14_bit8 -S14_bit9 -S14_bit10 -S14_bit11 -S14_bit12 -T14_bit_7 -T14_bit_6 -T14_bit_5 -T14_bit_4 -T14_bit_3 -T14_bit_2 -T14_bit_1 T14_bit0 -T14_bit1 -T14_bit2 T14_bit3 T14_bit4 T14_bit5 -T14_bit6 -T14_bit7 -T14_bit8 -T14_bit9 -T14_bit10 -T14_bit11 -T14_bit12 -S15_bit_7 -S15_bit_6 -S15_bit_5 -S15_bit_4 -S15_bit_3 -S15_bit_2 -S15_bit_1 -S15_bit0 S15_bit1 -S15_bit2 -S15_bit3 -S15_bit4 S15_bit5 -S15_bit6 -S15_bit7 -S15_bit8 -S15_bit9 -S15_bit10 -S15_bit11 -S15_bit12 -T15_bit_7 -T15_bit_6 -T15_bit_5 -T15_bit_4 -T15_bit_3 -T15_bit_2 -T15_bit_1 -T15_bit0 -T15_bit1 -T15_bit2 -T15_bit3 T15_bit4 T15_bit5 -T15_bit6 -T15_bit7 -T15_bit8 -T15_bit9 -T15_bit10 -T15_bit11 -T15_bit12 -S2_bit_7 -S2_bit_6 -S2_bit_5 -S2_bit_4 -S2_bit_3 -S2_bit_2 -S2_bit_1 -S2_bit0 S2_bit1 -S2_bit2 -S2_bit3 -S2_bit4 -S2_bit5 -S2_bit6 -S2_bit7 -S2_bit8 -S2_bit9 -S2_bit10 -S2_bit11 -S2_bit12 -T2_bit_7 -T2_bit_6 -T2_bit_5 -T2_bit_4 -T2_bit_3 -T2_bit_2 -T2_bit_1 -T2_bit0 -T2_bit1 -T2_bit2 -T2_bit3 -T2_bit4 -T2_bit5 -T2_bit6 -T2_bit7 -T2_bit8 -T2_bit9 -T2_bit10 -T2_bit11 -T2_bit12 -S3_bit_7 -S3_bit_6 -S3_bit_5 -S3_bit_4 -S3_bit_3 -S3_bit_2 -S3_bit_1 -S3_bit0 S3_bit1 -S3_bit2 -S3_bit3 S3_bit4 -S3_bit5 S3_bit6 -
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/14644/stat): 14644 (minisat+_script) R 14643 14644 22582 0 -1 0 19 0 0 0 0 0 0 0 23 0 1 0 1797505173 712704 3 4294967295 134512640 135087896 3221224512 3221224512 1073744960 0 0 5 0 0 0 0 17 1 0 0 Raw data (/proc/14644/statm): 174 3 169 147 0 27 0 [pid=14644] 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=14645 New process pid=14646 New process pid=14647 execve syscall for /bin/sed executable One traced child (pid=14646) 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=14647) exited with status: 0 One traced child (pid=14645) exited with status: 0 New process pid=14648 execve syscall for /oldhome/oroussel/solvers/minisat+_64-bit_static executable open syscall for file /dev/null open syscall for file /oldhome/oroussel/tmp/wulflinc10/normalized-mps-v2-13-7-pk1.opb [startup+10.0028 s] Raw data (loadavg): 0.93 0.95 0.90 2/57 14648 Raw data (/proc/14644/stat): 14644 (minisat+_script) S 14643 14644 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797505173 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14644/statm): 531 226 485 147 0 384 0 [pid=14644] vsize: 2124 Raw data (/proc/14648/stat): 14648 (minisat+_64-bit) R 14644 14644 22582 0 -1 0 1329 0 0 0 981 6 0 0 25 0 1 0 1797505178 5672960 1280 4294967295 134512640 135094434 3221224448 3221223108 134553533 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/14648/statm): 1385 1280 145 145 0 1240 0 [pid=14648] vsize: 5540 Current children cumulated CPU time (s) 9.87 Current children cumulated vsize (Kb) 7664 [startup+20.0043 s] Raw data (loadavg): 0.94 0.96 0.91 2/57 14648 Raw data (/proc/14644/stat): 14644 (minisat+_script) S 14643 14644 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797505173 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14644/statm): 531 226 485 147 0 384 0 [pid=14644] vsize: 2124 Raw data (/proc/14648/stat): 14648 (minisat+_64-bit) R 14644 14644 22582 0 -1 0 1475 0 0 0 1976 9 0 0 25 0 1 0 1797505178 6643712 1426 4294967295 134512640 135094434 3221224448 3221223060 134563080 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14648/statm): 1622 1426 145 145 0 1477 0 [pid=14648] vsize: 6488 Current children cumulated CPU time (s) 19.85 Current children cumulated vsize (Kb) 8612 [startup+30.0049 s] Raw data (loadavg): 0.95 0.96 0.91 2/57 14648 Raw data (/proc/14644/stat): 14644 (minisat+_script) S 14643 14644 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797505173 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14644/statm): 531 226 485 147 0 384 0 [pid=14644] vsize: 2124 Raw data (/proc/14648/stat): 14648 (minisat+_64-bit) R 14644 14644 22582 0 -1 0 1585 0 0 0 2973 10 0 0 25 0 1 0 1797505178 7086080 1536 4294967295 134512640 135094434 3221224448 3221223104 134557856 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14648/statm): 1730 1536 145 145 0 1585 0 [pid=14648] vsize: 6920 Current children cumulated CPU time (s) 29.83 Current children cumulated vsize (Kb) 9044 [startup+40.0044 s] Raw data (loadavg): 0.95 0.96 0.91 2/57 14648 Raw data (/proc/14644/stat): 14644 (minisat+_script) S 14643 14644 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797505173 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14644/statm): 531 226 485 147 0 384 0 [pid=14644] vsize: 2124 Raw data (/proc/14648/stat): 14648 (minisat+_64-bit) R 14644 14644 22582 0 -1 0 1785 0 0 0 3970 12 0 0 25 0 1 0 1797505178 7905280 1736 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14648/statm): 1930 1736 145 145 0 1785 0 [pid=14648] vsize: 7720 Current children cumulated CPU time (s) 39.82 Current children cumulated vsize (Kb) 9844 [startup+50.005 s] Raw data (loadavg): 0.96 0.96 0.91 2/57 14648 Raw data (/proc/14644/stat): 14644 (minisat+_script) S 14643 14644 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797505173 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14644/statm): 531 226 485 147 0 384 0 [pid=14644] vsize: 2124 Raw data (/proc/14648/stat): 14648 (minisat+_64-bit) R 14644 14644 22582 0 -1 0 1967 0 0 0 4967 13 0 0 25 0 1 0 1797505178 8704000 1918 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14648/statm): 2125 1918 145 145 0 1980 0 [pid=14648] vsize: 8500 Current children cumulated CPU time (s) 49.8 Current children cumulated vsize (Kb) 10624 [startup+60.0055 s] Raw data (loadavg): 0.97 0.96 0.91 2/57 14648 Raw data (/proc/14644/stat): 14644 (minisat+_script) S 14643 14644 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797505173 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14644/statm): 531 226 485 147 0 384 0 [pid=14644] vsize: 2124 Raw data (/proc/14648/stat): 14648 (minisat+_64-bit) R 14644 14644 22582 0 -1 0 2107 0 0 0 5964 15 0 0 25 0 1 0 1797505178 9269248 2058 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14648/statm): 2263 2058 145 145 0 2118 0 [pid=14648] vsize: 9052 Current children cumulated CPU time (s) 59.79 Current children cumulated vsize (Kb) 11176 [startup+70.0061 s] Raw data (loadavg): 0.97 0.96 0.91 2/57 14648 Raw data (/proc/14644/stat): 14644 (minisat+_script) S 14643 14644 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797505173 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14644/statm): 531 226 485 147 0 384 0 [pid=14644] vsize: 2124 Raw data (/proc/14648/stat): 14648 (minisat+_64-bit) R 14644 14644 22582 0 -1 0 2393 0 0 0 6958 18 0 0 25 0 1 0 1797505178 10420224 2344 4294967295 134512640 135094434 3221224448 3221223104 134558227 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/14648/statm): 2544 2344 145 145 0 2399 0 [pid=14648] vsize: 10176 Current children cumulated CPU time (s) 69.76 Current children cumulated vsize (Kb) 12300 [startup+80.0077 s] Raw data (loadavg): 0.98 0.96 0.91 2/57 14648 Raw data (/proc/14644/stat): 14644 (minisat+_script) S 14643 14644 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797505173 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14644/statm): 531 226 485 147 0 384 0 [pid=14644] vsize: 2124 Raw data (/proc/14648/stat): 14648 (minisat+_64-bit) R 14644 14644 22582 0 -1 0 2469 0 0 0 7955 18 0 0 25 0 1 0 1797505178 10723328 2420 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/14648/statm): 2618 2420 145 145 0 2473 0 [pid=14648] vsize: 10472 Current children cumulated CPU time (s) 79.73 Current children cumulated vsize (Kb) 12596 [startup+90.0082 s] Raw data (loadavg): 0.98 0.96 0.91 2/57 14648 Raw data (/proc/14644/stat): 14644 (minisat+_script) S 14643 14644 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797505173 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14644/statm): 531 226 485 147 0 384 0 [pid=14644] vsize: 2124 Raw data (/proc/14648/stat): 14648 (minisat+_64-bit) R 14644 14644 22582 0 -1 0 2665 0 0 0 8950 20 0 0 25 0 1 0 1797505178 11509760 2616 4294967295 134512640 135094434 3221224448 3221223072 134557734 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14648/statm): 2810 2616 145 145 0 2665 0 [pid=14648] vsize: 11240 Current children cumulated CPU time (s) 89.7 Current children cumulated vsize (Kb) 13364 [startup+100.009 s] Raw data (loadavg): 0.98 0.96 0.91 2/57 14648 Raw data (/proc/14644/stat): 14644 (minisat+_script) S 14643 14644 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797505173 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14644/statm): 531 226 485 147 0 384 0 [pid=14644] vsize: 2124 Raw data (/proc/14648/stat): 14648 (minisat+_64-bit) R 14644 14644 22582 0 -1 0 2793 0 0 0 9949 21 0 0 25 0 1 0 1797505178 12156928 2744 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14648/statm): 2968 2744 145 145 0 2823 0 [pid=14648] vsize: 11872 Current children cumulated CPU time (s) 99.7 Current children cumulated vsize (Kb) 13996 [startup+110.009 s] Raw data (loadavg): 0.98 0.96 0.91 2/57 14648 Raw data (/proc/14644/stat): 14644 (minisat+_script) S 14643 14644 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797505173 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14644/statm): 531 226 485 147 0 384 0 [pid=14644] vsize: 2124 Raw data (/proc/14648/stat): 14648 (minisat+_64-bit) R 14644 14644 22582 0 -1 0 2793 0 0 0 10949 21 0 0 25 0 1 0 1797505178 12156928 2744 4294967295 134512640 135094434 3221224448 3221223104 134558398 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14648/statm): 2968 2744 145 145 0 2823 0 [pid=14648] vsize: 11872 Current children cumulated CPU time (s) 109.7 Current children cumulated vsize (Kb) 13996 [startup+120.011 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 14648 Raw data (/proc/14644/stat): 14644 (minisat+_script) S 14643 14644 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797505173 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14644/statm): 531 226 485 147 0 384 0 [pid=14644] vsize: 2124 Raw data (/proc/14648/stat): 14648 (minisat+_64-bit) R 14644 14644 22582 0 -1 0 2793 0 0 0 11949 21 0 0 25 0 1 0 1797505178 12156928 2744 4294967295 134512640 135094434 3221224448 3221223120 134556073 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14648/statm): 2968 2744 145 145 0 2823 0 [pid=14648] vsize: 11872 Current children cumulated CPU time (s) 119.7 Current children cumulated vsize (Kb) 13996 [startup+130.011 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 14648 Raw data (/proc/14644/stat): 14644 (minisat+_script) S 14643 14644 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797505173 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14644/statm): 531 226 485 147 0 384 0 [pid=14644] vsize: 2124 Raw data (/proc/14648/stat): 14648 (minisat+_64-bit) R 14644 14644 22582 0 -1 0 2793 0 0 0 12950 21 0 0 25 0 1 0 1797505178 12156928 2744 4294967295 134512640 135094434 3221224448 3221223104 134558402 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14648/statm): 2968 2744 145 145 0 2823 0 [pid=14648] vsize: 11872 Current children cumulated CPU time (s) 129.71 Current children cumulated vsize (Kb) 13996 [startup+140.012 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 14648 Raw data (/proc/14644/stat): 14644 (minisat+_script) S 14643 14644 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797505173 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14644/statm): 531 226 485 147 0 384 0 [pid=14644] vsize: 2124 Raw data (/proc/14648/stat): 14648 (minisat+_64-bit) R 14644 14644 22582 0 -1 0 2966 0 0 0 13948 23 0 0 25 0 1 0 1797505178 12853248 2917 4294967295 134512640 135094434 3221224448 3221223084 134557560 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14648/statm): 3138 2917 145 145 0 2993 0 [pid=14648] vsize: 12552 Current children cumulated CPU time (s) 139.71 Current children cumulated vsize (Kb) 14676 [startup+150.013 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 14648 Raw data (/proc/14644/stat): 14644 (minisat+_script) S 14643 14644 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797505173 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14644/statm): 531 226 485 147 0 384 0 [pid=14644] vsize: 2124 Raw data (/proc/14648/stat): 14648 (minisat+_64-bit) R 14644 14644 22582 0 -1 0 2970 0 0 0 14948 23 0 0 25 0 1 0 1797505178 12869632 2921 4294967295 134512640 135094434 3221224448 3221223104 134558402 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14648/statm): 3142 2921 145 145 0 2997 0 [pid=14648] vsize: 12568 Current children cumulated CPU time (s) 149.71 Current children cumulated vsize (Kb) 14692 [startup+160.012 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 14648 Raw data (/proc/14644/stat): 14644 (minisat+_script) S 14643 14644 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797505173 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14644/statm): 531 226 485 147 0 384 0 [pid=14644] vsize: 2124 Raw data (/proc/14648/stat): 14648 (minisat+_64-bit) R 14644 14644 22582 0 -1 0 3181 0 0 0 15944 24 0 0 25 0 1 0 1797505178 13733888 3132 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14648/statm): 3353 3132 145 145 0 3208 0 [pid=14648] vsize: 13412 Current children cumulated CPU time (s) 159.68 Current children cumulated vsize (Kb) 15536 [startup+170.013 s] Raw data (loadavg): 1.07 0.99 0.91 2/57 14648 Raw data (/proc/14644/stat): 14644 (minisat+_script) S 14643 14644 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797505173 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14644/statm): 531 226 485 147 0 384 0 [pid=14644] vsize: 2124 Raw data (/proc/14648/stat): 14648 (minisat+_64-bit) R 14644 14644 22582 0 -1 0 3551 0 0 0 16938 26 0 0 25 0 1 0 1797505178 15241216 3502 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14648/statm): 3721 3502 145 145 0 3576 0 [pid=14648] vsize: 14884 Current children cumulated CPU time (s) 169.64 Current children cumulated vsize (Kb) 17008 [startup+180.013 s] Raw data (loadavg): 1.06 0.99 0.91 2/57 14648 Raw data (/proc/14644/stat): 14644 (minisat+_script) S 14643 14644 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797505173 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14644/statm): 531 226 485 147 0 384 0 [pid=14644] vsize: 2124 Raw data (/proc/14648/stat): 14648 (minisat+_64-bit) R 14644 14644 22582 0 -1 0 3814 0 0 0 17933 29 0 0 25 0 1 0 1797505178 16297984 3765 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14648/statm): 3979 3765 145 145 0 3834 0 [pid=14648] vsize: 15916 Current children cumulated CPU time (s) 179.62 Current children cumulated vsize (Kb) 18040 [startup+190.014 s] Raw data (loadavg): 1.05 0.99 0.91 2/57 14648 Raw data (/proc/14644/stat): 14644 (minisat+_script) S 14643 14644 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797505173 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14644/statm): 531 226 485 147 0 384 0 [pid=14644] vsize: 2124 Raw data (/proc/14648/stat): 14648 (minisat+_64-bit) R 14644 14644 22582 0 -1 0 3814 0 0 0 18933 29 0 0 25 0 1 0 1797505178 16297984 3765 4294967295 134512640 135094434 3221224448 3221223136 134554746 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14648/statm): 3979 3765 145 145 0 3834 0 [pid=14648] vsize: 15916 Current children cumulated CPU time (s) 189.62 Current children cumulated vsize (Kb) 18040 [startup+200.014 s] Raw data (loadavg): 1.04 0.99 0.91 2/57 14648 Raw data (/proc/14644/stat): 14644 (minisat+_script) S 14643 14644 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797505173 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14644/statm): 531 226 485 147 0 384 0 [pid=14644] vsize: 2124 Raw data (/proc/14648/stat): 14648 (minisat+_64-bit) R 14644 14644 22582 0 -1 0 3814 0 0 0 19934 29 0 0 25 0 1 0 1797505178 16297984 3765 4294967295 134512640 135094434 3221224448 3221223104 134557996 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14648/statm): 3979 3765 145 145 0 3834 0 [pid=14648] vsize: 15916 Current children cumulated CPU time (s) 199.63 Current children cumulated vsize (Kb) 18040 [startup+210.015 s] Raw data (loadavg): 1.03 0.99 0.91 2/57 14648 Raw data (/proc/14644/stat): 14644 (minisat+_script) S 14643 14644 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797505173 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14644/statm): 531 226 485 147 0 384 0 [pid=14644] vsize: 2124 Raw data (/proc/14648/stat): 14648 (minisat+_64-bit) R 14644 14644 22582 0 -1 0 3814 0 0 0 20934 29 0 0 25 0 1 0 1797505178 16297984 3765 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14648/statm): 3979 3765 145 145 0 3834 0 [pid=14648] vsize: 15916 Current children cumulated CPU time (s) 209.63 Current children cumulated vsize (Kb) 18040 [startup+220.016 s] Raw data (loadavg): 1.03 0.99 0.91 2/57 14648 Raw data (/proc/14644/stat): 14644 (minisat+_script) S 14643 14644 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797505173 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14644/statm): 531 226 485 147 0 384 0 [pid=14644] vsize: 2124 Raw data (/proc/14648/stat): 14648 (minisat+_64-bit) R 14644 14644 22582 0 -1 0 3814 0 0 0 21934 29 0 0 25 0 1 0 1797505178 16297984 3765 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14648/statm): 3979 3765 145 145 0 3834 0 [pid=14648] vsize: 15916 Current children cumulated CPU time (s) 219.63 Current children cumulated vsize (Kb) 18040 [startup+230.017 s] Raw data (loadavg): 1.02 0.99 0.91 2/57 14648 Raw data (/proc/14644/stat): 14644 (minisat+_script) S 14643 14644 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797505173 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14644/statm): 531 226 485 147 0 384 0 [pid=14644] vsize: 2124 Raw data (/proc/14648/stat): 14648 (minisat+_64-bit) R 14644 14644 22582 0 -1 0 3814 0 0 0 22934 29 0 0 25 0 1 0 1797505178 16297984 3765 4294967295 134512640 135094434 3221224448 3221223104 134557948 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14648/statm): 3979 3765 145 145 0 3834 0 [pid=14648] vsize: 15916 Current children cumulated CPU time (s) 229.63 Current children cumulated vsize (Kb) 18040 [startup+240.018 s] Raw data (loadavg): 1.02 0.99 0.91 2/57 14648 Raw data (/proc/14644/stat): 14644 (minisat+_script) S 14643 14644 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797505173 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14644/statm): 531 226 485 147 0 384 0 [pid=14644] vsize: 2124 Raw data (/proc/14648/stat): 14648 (minisat+_64-bit) R 14644 14644 22582 0 -1 0 3814 0 0 0 23934 29 0 0 25 0 1 0 1797505178 16297984 3765 4294967295 134512640 135094434 3221224448 3221223120 134556526 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14648/statm): 3979 3765 145 145 0 3834 0 [pid=14648] vsize: 15916 Current children cumulated CPU time (s) 239.63 Current children cumulated vsize (Kb) 18040 [startup+250.018 s] Raw data (loadavg): 1.02 0.99 0.91 2/57 14648 Raw data (/proc/14644/stat): 14644 (minisat+_script) S 14643 14644 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797505173 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14644/statm): 531 226 485 147 0 384 0 [pid=14644] vsize: 2124 Raw data (/proc/14648/stat): 14648 (minisat+_64-bit) R 14644 14644 22582 0 -1 0 3814 0 0 0 24935 29 0 0 25 0 1 0 1797505178 16297984 3765 4294967295 134512640 135094434 3221224448 3221223136 134554746 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14648/statm): 3979 3765 145 145 0 3834 0 [pid=14648] vsize: 15916 Current children cumulated CPU time (s) 249.64 Current children cumulated vsize (Kb) 18040 [startup+260.019 s] Raw data (loadavg): 1.01 0.99 0.91 2/57 14648 Raw data (/proc/14644/stat): 14644 (minisat+_script) S 14643 14644 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797505173 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14644/statm): 531 226 485 147 0 384 0 [pid=14644] vsize: 2124 Raw data (/proc/14648/stat): 14648 (minisat+_64-bit) R 14644 14644 22582 0 -1 0 3814 0 0 0 25935 29 0 0 25 0 1 0 1797505178 16297984 3765 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14648/statm): 3979 3765 145 145 0 3834 0 [pid=14648] vsize: 15916 Current children cumulated CPU time (s) 259.64 Current children cumulated vsize (Kb) 18040 [startup+270.019 s] Raw data (loadavg): 1.01 0.99 0.91 2/57 14648 Raw data (/proc/14644/stat): 14644 (minisat+_script) S 14643 14644 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797505173 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14644/statm): 531 226 485 147 0 384 0 [pid=14644] vsize: 2124 Raw data (/proc/14648/stat): 14648 (minisat+_64-bit) R 14644 14644 22582 0 -1 0 3827 0 0 0 26934 29 0 0 25 0 1 0 1797505178 16351232 3778 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14648/statm): 3992 3778 145 145 0 3847 0 [pid=14648] vsize: 15968 Current children cumulated CPU time (s) 269.63 Current children cumulated vsize (Kb) 18092 [startup+280.02 s] Raw data (loadavg): 1.01 0.99 0.91 2/57 14648 Raw data (/proc/14644/stat): 14644 (minisat+_script) S 14643 14644 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797505173 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14644/statm): 531 226 485 147 0 384 0 [pid=14644] vsize: 2124 Raw data (/proc/14648/stat): 14648 (minisat+_64-bit) R 14644 14644 22582 0 -1 0 4137 0 0 0 27928 31 0 0 25 0 1 0 1797505178 17604608 4088 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14648/statm): 4298 4088 145 145 0 4153 0 [pid=14648] vsize: 17192 Current children cumulated CPU time (s) 279.59 Current children cumulated vsize (Kb) 19316 [startup+290.02 s] Raw data (loadavg): 1.01 0.99 0.91 2/57 14648 Raw data (/proc/14644/stat): 14644 (minisat+_script) S 14643 14644 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797505173 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14644/statm): 531 226 485 147 0 384 0 [pid=14644] vsize: 2124 Raw data (/proc/14648/stat): 14648 (minisat+_64-bit) R 14644 14644 22582 0 -1 0 4144 0 0 0 28928 31 0 0 25 0 1 0 1797505178 17633280 4095 4294967295 134512640 135094434 3221224448 3221223104 134558402 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14648/statm): 4305 4095 145 145 0 4160 0 [pid=14648] vsize: 17220 Current children cumulated CPU time (s) 289.59 Current children cumulated vsize (Kb) 19344 [startup+300.021 s] Raw data (loadavg): 1.00 0.99 0.91 2/57 14648 Raw data (/proc/14644/stat): 14644 (minisat+_script) S 14643 14644 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797505173 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14644/statm): 531 226 485 147 0 384 0 [pid=14644] vsize: 2124 Raw data (/proc/14648/stat): 14648 (minisat+_64-bit) R 14644 14644 22582 0 -1 0 4159 0 0 0 29928 31 0 0 25 0 1 0 1797505178 17698816 4110 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14648/statm): 4321 4110 145 145 0 4176 0 [pid=14648] vsize: 17284 Current children cumulated CPU time (s) 299.59 Current children cumulated vsize (Kb) 19408 [startup+310.021 s] Raw data (loadavg): 1.00 0.99 0.91 2/57 14648 Raw data (/proc/14644/stat): 14644 (minisat+_script) S 14643 14644 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797505173 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14644/statm): 531 226 485 147 0 384 0 [pid=14644] vsize: 2124 Raw data (/proc/14648/stat): 14648 (minisat+_64-bit) R 14644 14644 22582 0 -1 0 4171 0 0 0 30928 31 0 0 25 0 1 0 1797505178 17747968 4122 4294967295 134512640 135094434 3221224448 3221223104 134557917 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14648/statm): 4333 4122 145 145 0 4188 0 [pid=14648] vsize: 17332 Current children cumulated CPU time (s) 309.59 Current children cumulated vsize (Kb) 19456 [startup+320.022 s] Raw data (loadavg): 1.00 0.99 0.91 2/57 14648 Raw data (/proc/14644/stat): 14644 (minisat+_script) S 14643 14644 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797505173 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14644/statm): 531 226 485 147 0 384 0 [pid=14644] vsize: 2124 Raw data (/proc/14648/stat): 14648 (minisat+_64-bit) R 14644 14644 22582 0 -1 0 4181 0 0 0 31928 31 0 0 25 0 1 0 1797505178 17797120 4132 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14648/statm): 4345 4132 145 145 0 4200 0 [pid=14648] vsize: 17380 Current children cumulated CPU time (s) 319.59 Current children cumulated vsize (Kb) 19504 [startup+330.023 s] Raw data (loadavg): 1.00 0.99 0.91 2/57 14648 Raw data (/proc/14644/stat): 14644 (minisat+_script) S 14643 14644 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797505173 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14644/statm): 531 226 485 147 0 384 0 [pid=14644] vsize: 2124 Raw data (/proc/14648/stat): 14648 (minisat+_64-bit) R 14644 14644 22582 0 -1 0 4188 0 0 0 32929 31 0 0 25 0 1 0 1797505178 17829888 4139 4294967295 134512640 135094434 3221224448 3221223104 134558208 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14648/statm): 4353 4139 145 145 0 4208 0 [pid=14648] vsize: 17412 Current children cumulated CPU time (s) 329.6 Current children cumulated vsize (Kb) 19536 [startup+340.024 s] Raw data (loadavg): 1.00 0.99 0.91 2/57 14648 Raw data (/proc/14644/stat): 14644 (minisat+_script) S 14643 14644 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797505173 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14644/statm): 531 226 485 147 0 384 0 [pid=14644] vsize: 2124 Raw data (/proc/14648/stat): 14648 (minisat+_64-bit) R 14644 14644 22582 0 -1 0 4379 0 0 0 33925 33 0 0 25 0 1 0 1797505178 18612224 4330 4294967295 134512640 135094434 3221224448 3221223104 134558178 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14648/statm): 4544 4330 145 145 0 4399 0 [pid=14648] vsize: 18176 Current children cumulated CPU time (s) 339.58 Current children cumulated vsize (Kb) 20300 [startup+350.025 s] Raw data (loadavg): 1.00 0.99 0.91 2/57 14648 Raw data (/proc/14644/stat): 14644 (minisat+_script) S 14643 14644 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797505173 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14644/statm): 531 226 485 147 0 384 0 [pid=14644] vsize: 2124 Raw data (/proc/14648/stat): 14648 (minisat+_64-bit) R 14644 14644 22582 0 -1 0 4677 0 0 0 34918 35 0 0 25 0 1 0 1797505178 19832832 4628 4294967295 134512640 135094434 3221224448 3221223104 134558208 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14648/statm): 4842 4628 145 145 0 4697 0 [pid=14648] vsize: 19368 Current children cumulated CPU time (s) 349.53 Current children cumulated vsize (Kb) 21492 [startup+360.025 s] Raw data (loadavg): 1.00 0.99 0.91 2/57 14648 Raw data (/proc/14644/stat): 14644 (minisat+_script) S 14643 14644 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797505173 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14644/statm): 531 226 485 147 0 384 0 [pid=14644] vsize: 2124 Raw data (/proc/14648/stat): 14648 (minisat+_64-bit) R 14644 14644 22582 0 -1 0 4928 0 0 0 35914 37 0 0 25 0 1 0 1797505178 20865024 4879 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14648/statm): 5094 4879 145 145 0 4949 0 [pid=14648] vsize: 20376 Current children cumulated CPU time (s) 359.51 Current children cumulated vsize (Kb) 22500 [startup+370.026 s] Raw data (loadavg): 1.00 0.99 0.91 2/57 14648 Raw data (/proc/14644/stat): 14644 (minisat+_script) S 14643 14644 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797505173 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14644/statm): 531 226 485 147 0 384 0 [pid=14644] vsize: 2124 Raw data (/proc/14648/stat): 14648 (minisat+_64-bit) R 14644 14644 22582 0 -1 0 5155 0 0 0 36910 39 0 0 25 0 1 0 1797505178 21774336 5106 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14648/statm): 5316 5106 145 145 0 5171 0 [pid=14648] vsize: 21264 Current children cumulated CPU time (s) 369.49 Current children cumulated vsize (Kb) 23388 [startup+380.026 s] Raw data (loadavg): 1.00 0.99 0.91 2/57 14648 Raw data (/proc/14644/stat): 14644 (minisat+_script) S 14643 14644 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797505173 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14644/statm): 531 226 485 147 0 384 0 [pid=14644] vsize: 2124 Raw data (/proc/14648/stat): 14648 (minisat+_64-bit) R 14644 14644 22582 0 -1 0 5276 0 0 0 37906 41 0 0 25 0 1 0 1797505178 22265856 5227 4294967295 134512640 135094434 3221224448 3221223104 134558395 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14648/statm): 5436 5227 145 145 0 5291 0 [pid=14648] vsize: 21744 Current children cumulated CPU time (s) 379.47 Current children cumulated vsize (Kb) 23868 [startup+390.027 s] Raw data (loadavg): 1.00 0.99 0.91 2/57 14648 Raw data (/proc/14644/stat): 14644 (minisat+_script) S 14643 14644 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797505173 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14644/statm): 531 226 485 147 0 384 0 [pid=14644] vsize: 2124 Raw data (/proc/14648/stat): 14648 (minisat+_64-bit) R 14644 14644 22582 0 -1 0 5276 0 0 0 38906 41 0 0 25 0 1 0 1797505178 22265856 5227 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14648/statm): 5436 5227 145 145 0 5291 0 [pid=14648] vsize: 21744 Current children cumulated CPU time (s) 389.47 Current children cumulated vsize (Kb) 23868 [startup+400.027 s] Raw data (loadavg): 1.00 0.99 0.91 2/57 14648 Raw data (/proc/14644/stat): 14644 (minisat+_script) S 14643 14644 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797505173 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14644/statm): 531 226 485 147 0 384 0 [pid=14644] vsize: 2124 Raw data (/proc/14648/stat): 14648 (minisat+_64-bit) R 14644 14644 22582 0 -1 0 5276 0 0 0 39907 41 0 0 25 0 1 0 1797505178 22265856 5227 4294967295 134512640 135094434 3221224448 3221223104 134557945 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14648/statm): 5436 5227 145 145 0 5291 0 [pid=14648] vsize: 21744 Current children cumulated CPU time (s) 399.48 Current children cumulated vsize (Kb) 23868 [startup+410.028 s] Raw data (loadavg): 1.07 1.00 0.92 2/57 14648 Raw data (/proc/14644/stat): 14644 (minisat+_script) S 14643 14644 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797505173 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14644/statm): 531 226 485 147 0 384 0 [pid=14644] vsize: 2124 Raw data (/proc/14648/stat): 14648 (minisat+_64-bit) R 14644 14644 22582 0 -1 0 5276 0 0 0 40907 41 0 0 25 0 1 0 1797505178 22265856 5227 4294967295 134512640 135094434 3221224448 3221223104 134558249 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14648/statm): 5436 5227 145 145 0 5291 0 [pid=14648] vsize: 21744 Current children cumulated CPU time (s) 409.48 Current children cumulated vsize (Kb) 23868 [startup+420.028 s] Raw data (loadavg): 1.06 1.00 0.92 2/57 14648 Raw data (/proc/14644/stat): 14644 (minisat+_script) S 14643 14644 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797505173 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14644/statm): 531 226 485 147 0 384 0 [pid=14644] vsize: 2124 Raw data (/proc/14648/stat): 14648 (minisat+_64-bit) R 14644 14644 22582 0 -1 0 5276 0 0 0 41907 41 0 0 25 0 1 0 1797505178 22265856 5227 4294967295 134512640 135094434 3221224448 3221223104 134557908 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14648/statm): 5436 5227 145 145 0 5291 0 [pid=14648] vsize: 21744 Current children cumulated CPU time (s) 419.48 Current children cumulated vsize (Kb) 23868 [startup+430.029 s] Raw data (loadavg): 1.05 1.00 0.92 2/57 14648 Raw data (/proc/14644/stat): 14644 (minisat+_script) S 14643 14644 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797505173 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14644/statm): 531 226 485 147 0 384 0 [pid=14644] vsize: 2124 Raw data (/proc/14648/stat): 14648 (minisat+_64-bit) R 14644 14644 22582 0 -1 0 5276 0 0 0 42907 41 0 0 25 0 1 0 1797505178 22265856 5227 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14648/statm): 5436 5227 145 145 0 5291 0 [pid=14648] vsize: 21744 Current children cumulated CPU time (s) 429.48 Current children cumulated vsize (Kb) 23868 [startup+440.029 s] Raw data (loadavg): 1.04 1.00 0.92 2/57 14648 Raw data (/proc/14644/stat): 14644 (minisat+_script) S 14643 14644 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797505173 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14644/statm): 531 226 485 147 0 384 0 [pid=14644] vsize: 2124 Raw data (/proc/14648/stat): 14648 (minisat+_64-bit) R 14644 14644 22582 0 -1 0 5276 0 0 0 43907 41 0 0 25 0 1 0 1797505178 22265856 5227 4294967295 134512640 135094434 3221224448 3221223136 134554731 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14648/statm): 5436 5227 145 145 0 5291 0 [pid=14648] vsize: 21744 Current children cumulated CPU time (s) 439.48 Current children cumulated vsize (Kb) 23868 [startup+450.03 s] Raw data (loadavg): 1.04 1.00 0.92 2/57 14648 Raw data (/proc/14644/stat): 14644 (minisat+_script) S 14643 14644 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797505173 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14644/statm): 531 226 485 147 0 384 0 [pid=14644] vsize: 2124 Raw data (/proc/14648/stat): 14648 (minisat+_64-bit) R 14644 14644 22582 0 -1 0 5276 0 0 0 44907 41 0 0 25 0 1 0 1797505178 22265856 5227 4294967295 134512640 135094434 3221224448 3221223104 134558004 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14648/statm): 5436 5227 145 145 0 5291 0 [pid=14648] vsize: 21744 Current children cumulated CPU time (s) 449.48 Current children cumulated vsize (Kb) 23868 [startup+460.03 s] Raw data (loadavg): 1.03 1.00 0.92 2/57 14648 Raw data (/proc/14644/stat): 14644 (minisat+_script) S 14643 14644 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797505173 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14644/statm): 531 226 485 147 0 384 0 [pid=14644] vsize: 2124 Raw data (/proc/14648/stat): 14648 (minisat+_64-bit) R 14644 14644 22582 0 -1 0 5276 0 0 0 45907 41 0 0 25 0 1 0 1797505178 22265856 5227 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14648/statm): 5436 5227 145 145 0 5291 0 [pid=14648] vsize: 21744 Current children cumulated CPU time (s) 459.48 Current children cumulated vsize (Kb) 23868 [startup+470.031 s] Raw data (loadavg): 1.02 1.00 0.92 2/57 14648 Raw data (/proc/14644/stat): 14644 (minisat+_script) S 14643 14644 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797505173 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14644/statm): 531 226 485 147 0 384 0 [pid=14644] vsize: 2124 Raw data (/proc/14648/stat): 14648 (minisat+_64-bit) R 14644 14644 22582 0 -1 0 5276 0 0 0 46908 41 0 0 25 0 1 0 1797505178 22265856 5227 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14648/statm): 5436 5227 145 145 0 5291 0 [pid=14648] vsize: 21744 Current children cumulated CPU time (s) 469.49 Current children cumulated vsize (Kb) 23868 [startup+480.031 s] Raw data (loadavg): 1.02 1.00 0.92 2/57 14648 Raw data (/proc/14644/stat): 14644 (minisat+_script) S 14643 14644 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797505173 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14644/statm): 531 226 485 147 0 384 0 [pid=14644] vsize: 2124 Raw data (/proc/14648/stat): 14648 (minisat+_64-bit) R 14644 14644 22582 0 -1 0 5276 0 0 0 47908 41 0 0 25 0 1 0 1797505178 22265856 5227 4294967295 134512640 135094434 3221224448 3221223072 134557714 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14648/statm): 5436 5227 145 145 0 5291 0 [pid=14648] vsize: 21744 Current children cumulated CPU time (s) 479.49 Current children cumulated vsize (Kb) 23868 [startup+490.032 s] Raw data (loadavg): 1.02 1.00 0.92 2/57 14648 Raw data (/proc/14644/stat): 14644 (minisat+_script) S 14643 14644 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797505173 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14644/statm): 531 226 485 147 0 384 0 [pid=14644] vsize: 2124 Raw data (/proc/14648/stat): 14648 (minisat+_64-bit) R 14644 14644 22582 0 -1 0 5276 0 0 0 48908 41 0 0 25 0 1 0 1797505178 22265856 5227 4294967295 134512640 135094434 3221224448 3221223040 134557248 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14648/statm): 5436 5227 145 145 0 5291 0 [pid=14648] vsize: 21744 Current children cumulated CPU time (s) 489.49 Current children cumulated vsize (Kb) 23868 [startup+500.033 s] Raw data (loadavg): 1.01 1.00 0.92 2/57 14648 Raw data (/proc/14644/stat): 14644 (minisat+_script) S 14643 14644 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797505173 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14644/statm): 531 226 485 147 0 384 0 [pid=14644] vsize: 2124 Raw data (/proc/14648/stat): 14648 (minisat+_64-bit) R 14644 14644 22582 0 -1 0 5276 0 0 0 49909 41 0 0 25 0 1 0 1797505178 22265856 5227 4294967295 134512640 135094434 3221224448 3221223104 134558235 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14648/statm): 5436 5227 145 145 0 5291 0 [pid=14648] vsize: 21744 Current children cumulated CPU time (s) 499.5 Current children cumulated vsize (Kb) 23868 [startup+510.033 s] Raw data (loadavg): 1.01 1.00 0.92 2/57 14648 Raw data (/proc/14644/stat): 14644 (minisat+_script) S 14643 14644 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797505173 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14644/statm): 531 226 485 147 0 384 0 [pid=14644] vsize: 2124 Raw data (/proc/14648/stat): 14648 (minisat+_64-bit) R 14644 14644 22582 0 -1 0 5276 0 0 0 50909 41 0 0 25 0 1 0 1797505178 22265856 5227 4294967295 134512640 135094434 3221224448 3221223120 134555943 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14648/statm): 5436 5227 145 145 0 5291 0 [pid=14648] vsize: 21744 Current children cumulated CPU time (s) 509.5 Current children cumulated vsize (Kb) 23868 [startup+520.035 s] Raw data (loadavg): 1.01 1.00 0.92 2/57 14648 Raw data (/proc/14644/stat): 14644 (minisat+_script) S 14643 14644 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797505173 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14644/statm): 531 226 485 147 0 384 0 [pid=14644] vsize: 2124 Raw data (/proc/14648/stat): 14648 (minisat+_64-bit) R 14644 14644 22582 0 -1 0 5276 0 0 0 51909 41 0 0 25 0 1 0 1797505178 22265856 5227 4294967295 134512640 135094434 3221224448 3221222752 134562757 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14648/statm): 5436 5227 145 145 0 5291 0 [pid=14648] vsize: 21744 Current children cumulated CPU time (s) 519.5 Current children cumulated vsize (Kb) 23868 [startup+530.035 s] Raw data (loadavg): 1.01 1.00 0.92 2/57 14648 Raw data (/proc/14644/stat): 14644 (minisat+_script) S 14643 14644 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797505173 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14644/statm): 531 226 485 147 0 384 0 [pid=14644] vsize: 2124 Raw data (/proc/14648/stat): 14648 (minisat+_64-bit) R 14644 14644 22582 0 -1 0 5276 0 0 0 52909 41 0 0 25 0 1 0 1797505178 22265856 5227 4294967295 134512640 135094434 3221224448 3221223104 134557911 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14648/statm): 5436 5227 145 145 0 5291 0 [pid=14648] vsize: 21744 Current children cumulated CPU time (s) 529.5 Current children cumulated vsize (Kb) 23868 [startup+540.036 s] Raw data (loadavg): 1.01 1.00 0.92 2/57 14648 Raw data (/proc/14644/stat): 14644 (minisat+_script) S 14643 14644 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797505173 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14644/statm): 531 226 485 147 0 384 0 [pid=14644] vsize: 2124 Raw data (/proc/14648/stat): 14648 (minisat+_64-bit) R 14644 14644 22582 0 -1 0 5276 0 0 0 53910 41 0 0 25 0 1 0 1797505178 22265856 5227 4294967295 134512640 135094434 3221224448 3221223040 134557180 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14648/statm): 5436 5227 145 145 0 5291 0 [pid=14648] vsize: 21744 Current children cumulated CPU time (s) 539.51 Current children cumulated vsize (Kb) 23868 [startup+550.036 s] Raw data (loadavg): 1.00 1.00 0.92 2/57 14648 Raw data (/proc/14644/stat): 14644 (minisat+_script) S 14643 14644 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797505173 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14644/statm): 531 226 485 147 0 384 0 [pid=14644] vsize: 2124 Raw data (/proc/14648/stat): 14648 (minisat+_64-bit) R 14644 14644 22582 0 -1 0 5276 0 0 0 54910 41 0 0 25 0 1 0 1797505178 22265856 5227 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14648/statm): 5436 5227 145 145 0 5291 0 [pid=14648] vsize: 21744 Current children cumulated CPU time (s) 549.51 Current children cumulated vsize (Kb) 23868 [startup+560.037 s] Raw data (loadavg): 1.00 1.00 0.92 2/57 14648 Raw data (/proc/14644/stat): 14644 (minisat+_script) S 14643 14644 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797505173 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14644/statm): 531 226 485 147 0 384 0 [pid=14644] vsize: 2124 Raw data (/proc/14648/stat): 14648 (minisat+_64-bit) R 14644 14644 22582 0 -1 0 5276 0 0 0 55910 41 0 0 25 0 1 0 1797505178 22265856 5227 4294967295 134512640 135094434 3221224448 3221223136 134554731 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14648/statm): 5436 5227 145 145 0 5291 0 [pid=14648] vsize: 21744 Current children cumulated CPU time (s) 559.51 Current children cumulated vsize (Kb) 23868 [startup+570.037 s] Raw data (loadavg): 1.00 1.00 0.92 2/57 14648 Raw data (/proc/14644/stat): 14644 (minisat+_script) S 14643 14644 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797505173 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14644/statm): 531 226 485 147 0 384 0 [pid=14644] vsize: 2124 Raw data (/proc/14648/stat): 14648 (minisat+_64-bit) R 14644 14644 22582 0 -1 0 5276 0 0 0 56910 41 0 0 25 0 1 0 1797505178 22265856 5227 4294967295 134512640 135094434 3221224448 3221223104 134557925 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14648/statm): 5436 5227 145 145 0 5291 0 [pid=14648] vsize: 21744 Current children cumulated CPU time (s) 569.51 Current children cumulated vsize (Kb) 23868 [startup+580.038 s] Raw data (loadavg): 1.00 1.00 0.92 2/57 14648 Raw data (/proc/14644/stat): 14644 (minisat+_script) S 14643 14644 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797505173 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14644/statm): 531 226 485 147 0 384 0 [pid=14644] vsize: 2124 Raw data (/proc/14648/stat): 14648 (minisat+_64-bit) R 14644 14644 22582 0 -1 0 5276 0 0 0 57910 41 0 0 25 0 1 0 1797505178 22265856 5227 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14648/statm): 5436 5227 145 145 0 5291 0 [pid=14648] vsize: 21744 Current children cumulated CPU time (s) 579.51 Current children cumulated vsize (Kb) 23868 [startup+590.037 s] Raw data (loadavg): 1.00 1.00 0.92 2/57 14648 Raw data (/proc/14644/stat): 14644 (minisat+_script) S 14643 14644 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797505173 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14644/statm): 531 226 485 147 0 384 0 [pid=14644] vsize: 2124 Raw data (/proc/14648/stat): 14648 (minisat+_64-bit) R 14644 14644 22582 0 -1 0 5276 0 0 0 58910 41 0 0 25 0 1 0 1797505178 22265856 5227 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14648/statm): 5436 5227 145 145 0 5291 0 [pid=14648] vsize: 21744 Current children cumulated CPU time (s) 589.51 Current children cumulated vsize (Kb) 23868 [startup+600.039 s] Raw data (loadavg): 1.00 1.00 0.92 2/57 14648 Raw data (/proc/14644/stat): 14644 (minisat+_script) S 14643 14644 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797505173 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14644/statm): 531 226 485 147 0 384 0 [pid=14644] vsize: 2124 Raw data (/proc/14648/stat): 14648 (minisat+_64-bit) R 14644 14644 22582 0 -1 0 5276 0 0 0 59911 41 0 0 25 0 1 0 1797505178 22265856 5227 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14648/statm): 5436 5227 145 145 0 5291 0 [pid=14648] vsize: 21744 Current children cumulated CPU time (s) 599.52 Current children cumulated vsize (Kb) 23868 [startup+610.039 s] Raw data (loadavg): 1.00 1.00 0.92 2/57 14648 Raw data (/proc/14644/stat): 14644 (minisat+_script) S 14643 14644 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797505173 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14644/statm): 531 226 485 147 0 384 0 [pid=14644] vsize: 2124 Raw data (/proc/14648/stat): 14648 (minisat+_64-bit) R 14644 14644 22582 0 -1 0 5276 0 0 0 60911 41 0 0 25 0 1 0 1797505178 22265856 5227 4294967295 134512640 135094434 3221224448 3221223136 134554723 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14648/statm): 5436 5227 145 145 0 5291 0 [pid=14648] vsize: 21744 Current children cumulated CPU time (s) 609.52 Current children cumulated vsize (Kb) 23868 [startup+620.04 s] Raw data (loadavg): 1.00 1.00 0.92 2/57 14648 Raw data (/proc/14644/stat): 14644 (minisat+_script) S 14643 14644 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797505173 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14644/statm): 531 226 485 147 0 384 0 [pid=14644] vsize: 2124 Raw data (/proc/14648/stat): 14648 (minisat+_64-bit) R 14644 14644 22582 0 -1 0 5276 0 0 0 61911 41 0 0 25 0 1 0 1797505178 22265856 5227 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14648/statm): 5436 5227 145 145 0 5291 0 [pid=14648] vsize: 21744 Current children cumulated CPU time (s) 619.52 Current children cumulated vsize (Kb) 23868 [startup+630.041 s] Raw data (loadavg): 1.00 1.00 0.92 2/57 14648 Raw data (/proc/14644/stat): 14644 (minisat+_script) S 14643 14644 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797505173 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14644/statm): 531 226 485 147 0 384 0 [pid=14644] vsize: 2124 Raw data (/proc/14648/stat): 14648 (minisat+_64-bit) R 14644 14644 22582 0 -1 0 5276 0 0 0 62911 42 0 0 25 0 1 0 1797505178 22265856 5227 4294967295 134512640 135094434 3221224448 3221223104 134558178 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14648/statm): 5436 5227 145 145 0 5291 0 [pid=14648] vsize: 21744 Current children cumulated CPU time (s) 629.53 Current children cumulated vsize (Kb) 23868 [startup+640.041 s] Raw data (loadavg): 1.00 1.00 0.92 2/57 14648 Raw data (/proc/14644/stat): 14644 (minisat+_script) S 14643 14644 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797505173 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14644/statm): 531 226 485 147 0 384 0 [pid=14644] vsize: 2124 Raw data (/proc/14648/stat): 14648 (minisat+_64-bit) R 14644 14644 22582 0 -1 0 5276 0 0 0 63911 42 0 0 25 0 1 0 1797505178 22265856 5227 4294967295 134512640 135094434 3221224448 3221223104 134558227 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14648/statm): 5436 5227 145 145 0 5291 0 [pid=14648] vsize: 21744 Current children cumulated CPU time (s) 639.53 Current children cumulated vsize (Kb) 23868 [startup+650.042 s] Raw data (loadavg): 1.00 1.00 0.92 2/57 14648 Raw data (/proc/14644/stat): 14644 (minisat+_script) S 14643 14644 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797505173 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14644/statm): 531 226 485 147 0 384 0 [pid=14644] vsize: 2124 Raw data (/proc/14648/stat): 14648 (minisat+_64-bit) R 14644 14644 22582 0 -1 0 5276 0 0 0 64912 42 0 0 25 0 1 0 1797505178 22265856 5227 4294967295 134512640 135094434 3221224448 3221223104 134557937 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14648/statm): 5436 5227 145 145 0 5291 0 [pid=14648] vsize: 21744 Current children cumulated CPU time (s) 649.54 Current children cumulated vsize (Kb) 23868 [startup+660.042 s] Raw data (loadavg): 1.00 1.00 0.92 2/57 14648 Raw data (/proc/14644/stat): 14644 (minisat+_script) S 14643 14644 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797505173 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14644/statm): 531 226 485 147 0 384 0 [pid=14644] vsize: 2124 Raw data (/proc/14648/stat): 14648 (minisat+_64-bit) R 14644 14644 22582 0 -1 0 5277 0 0 0 65912 42 0 0 25 0 1 0 1797505178 22265856 5228 4294967295 134512640 135094434 3221224448 3221223040 134557213 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14648/statm): 5436 5228 145 145 0 5291 0 [pid=14648] vsize: 21744 Current children cumulated CPU time (s) 659.54 Current children cumulated vsize (Kb) 23868 [startup+670.044 s] Raw data (loadavg): 1.00 1.00 0.92 2/57 14648 Raw data (/proc/14644/stat): 14644 (minisat+_script) S 14643 14644 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797505173 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14644/statm): 531 226 485 147 0 384 0 [pid=14644] vsize: 2124 Raw data (/proc/14648/stat): 14648 (minisat+_64-bit) R 14644 14644 22582 0 -1 0 5277 0 0 0 66912 42 0 0 25 0 1 0 1797505178 22265856 5228 4294967295 134512640 135094434 3221224448 3221223104 134558016 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14648/statm): 5436 5228 145 145 0 5291 0 [pid=14648] vsize: 21744 Current children cumulated CPU time (s) 669.54 Current children cumulated vsize (Kb) 23868 [startup+680.044 s] Raw data (loadavg): 1.00 1.00 0.92 2/57 14648 Raw data (/proc/14644/stat): 14644 (minisat+_script) S 14643 14644 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797505173 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14644/statm): 531 226 485 147 0 384 0 [pid=14644] vsize: 2124 Raw data (/proc/14648/stat): 14648 (minisat+_64-bit) R 14644 14644 22582 0 -1 0 5277 0 0 0 67912 42 0 0 25 0 1 0 1797505178 22265856 5228 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14648/statm): 5436 5228 145 145 0 5291 0 [pid=14648] vsize: 21744 Current children cumulated CPU time (s) 679.54 Current children cumulated vsize (Kb) 23868 [startup+690.045 s] Raw data (loadavg): 1.00 1.00 0.92 2/57 14648 Raw data (/proc/14644/stat): 14644 (minisat+_script) S 14643 14644 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797505173 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14644/statm): 531 226 485 147 0 384 0 [pid=14644] vsize: 2124 Raw data (/proc/14648/stat): 14648 (minisat+_64-bit) R 14644 14644 22582 0 -1 0 5277 0 0 0 68912 42 0 0 25 0 1 0 1797505178 22265856 5228 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14648/statm): 5436 5228 145 145 0 5291 0 [pid=14648] vsize: 21744 Current children cumulated CPU time (s) 689.54 Current children cumulated vsize (Kb) 23868 [startup+700.047 s] Raw data (loadavg): 1.00 1.00 0.92 2/57 14648 Raw data (/proc/14644/stat): 14644 (minisat+_script) S 14643 14644 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797505173 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14644/statm): 531 226 485 147 0 384 0 [pid=14644] vsize: 2124 Raw data (/proc/14648/stat): 14648 (minisat+_64-bit) R 14644 14644 22582 0 -1 0 5277 0 0 0 69913 42 0 0 25 0 1 0 1797505178 22265856 5228 4294967295 134512640 135094434 3221224448 3221223104 134558016 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14648/statm): 5436 5228 145 145 0 5291 0 [pid=14648] vsize: 21744 Current children cumulated CPU time (s) 699.55 Current children cumulated vsize (Kb) 23868 [startup+710.047 s] Raw data (loadavg): 1.00 1.00 0.92 2/57 14648 Raw data (/proc/14644/stat): 14644 (minisat+_script) S 14643 14644 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797505173 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14644/statm): 531 226 485 147 0 384 0 [pid=14644] vsize: 2124 Raw data (/proc/14648/stat): 14648 (minisat+_64-bit) R 14644 14644 22582 0 -1 0 5277 0 0 0 70913 42 0 0 25 0 1 0 1797505178 22265856 5228 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14648/statm): 5436 5228 145 145 0 5291 0 [pid=14648] vsize: 21744 Current children cumulated CPU time (s) 709.55 Current children cumulated vsize (Kb) 23868 [startup+720.048 s] Raw data (loadavg): 1.00 1.00 0.92 2/57 14648 Raw data (/proc/14644/stat): 14644 (minisat+_script) S 14643 14644 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797505173 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14644/statm): 531 226 485 147 0 384 0 [pid=14644] vsize: 2124 Raw data (/proc/14648/stat): 14648 (minisat+_64-bit) R 14644 14644 22582 0 -1 0 5277 0 0 0 71913 42 0 0 25 0 1 0 1797505178 22265856 5228 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14648/statm): 5436 5228 145 145 0 5291 0 [pid=14648] vsize: 21744 Current children cumulated CPU time (s) 719.55 Current children cumulated vsize (Kb) 23868 [startup+730.048 s] Raw data (loadavg): 1.00 1.00 0.92 2/57 14648 Raw data (/proc/14644/stat): 14644 (minisat+_script) S 14643 14644 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797505173 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14644/statm): 531 226 485 147 0 384 0 [pid=14644] vsize: 2124 Raw data (/proc/14648/stat): 14648 (minisat+_64-bit) R 14644 14644 22582 0 -1 0 5277 0 0 0 72913 42 0 0 25 0 1 0 1797505178 22265856 5228 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14648/statm): 5436 5228 145 145 0 5291 0 [pid=14648] vsize: 21744 Current children cumulated CPU time (s) 729.55 Current children cumulated vsize (Kb) 23868 [startup+740.048 s] Raw data (loadavg): 1.00 1.00 0.92 2/57 14648 Raw data (/proc/14644/stat): 14644 (minisat+_script) S 14643 14644 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797505173 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14644/statm): 531 226 485 147 0 384 0 [pid=14644] vsize: 2124 Raw data (/proc/14648/stat): 14648 (minisat+_64-bit) R 14644 14644 22582 0 -1 0 5277 0 0 0 73913 42 0 0 25 0 1 0 1797505178 22265856 5228 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14648/statm): 5436 5228 145 145 0 5291 0 [pid=14648] vsize: 21744 Current children cumulated CPU time (s) 739.55 Current children cumulated vsize (Kb) 23868 [startup+750.048 s] Raw data (loadavg): 1.00 1.00 0.92 2/57 14648 Raw data (/proc/14644/stat): 14644 (minisat+_script) S 14643 14644 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797505173 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14644/statm): 531 226 485 147 0 384 0 [pid=14644] vsize: 2124 Raw data (/proc/14648/stat): 14648 (minisat+_64-bit) R 14644 14644 22582 0 -1 0 5277 0 0 0 74913 42 0 0 25 0 1 0 1797505178 22265856 5228 4294967295 134512640 135094434 3221224448 3221222560 134562757 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14648/statm): 5436 5228 145 145 0 5291 0 [pid=14648] vsize: 21744 Current children cumulated CPU time (s) 749.55 Current children cumulated vsize (Kb) 23868 [startup+760.049 s] Raw data (loadavg): 1.00 1.00 0.92 2/57 14648 Raw data (/proc/14644/stat): 14644 (minisat+_script) S 14643 14644 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797505173 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14644/statm): 531 226 485 147 0 384 0 [pid=14644] vsize: 2124 Raw data (/proc/14648/stat): 14648 (minisat+_64-bit) R 14644 14644 22582 0 -1 0 5277 0 0 0 75914 42 0 0 25 0 1 0 1797505178 22265856 5228 4294967295 134512640 135094434 3221224448 3221223104 134557925 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14648/statm): 5436 5228 145 145 0 5291 0 [pid=14648] vsize: 21744 Current children cumulated CPU time (s) 759.56 Current children cumulated vsize (Kb) 23868 [startup+770.05 s] Raw data (loadavg): 1.00 1.00 0.92 2/57 14648 Raw data (/proc/14644/stat): 14644 (minisat+_script) S 14643 14644 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797505173 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14644/statm): 531 226 485 147 0 384 0 [pid=14644] vsize: 2124 Raw data (/proc/14648/stat): 14648 (minisat+_64-bit) R 14644 14644 22582 0 -1 0 5277 0 0 0 76914 42 0 0 25 0 1 0 1797505178 22265856 5228 4294967295 134512640 135094434 3221224448 3221223104 134558235 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14648/statm): 5436 5228 145 145 0 5291 0 [pid=14648] vsize: 21744 Current children cumulated CPU time (s) 769.56 Current children cumulated vsize (Kb) 23868 [startup+780.051 s] Raw data (loadavg): 1.00 1.00 0.92 2/57 14648 Raw data (/proc/14644/stat): 14644 (minisat+_script) S 14643 14644 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797505173 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14644/statm): 531 226 485 147 0 384 0 [pid=14644] vsize: 2124 Raw data (/proc/14648/stat): 14648 (minisat+_64-bit) R 14644 14644 22582 0 -1 0 5277 0 0 0 77914 42 0 0 25 0 1 0 1797505178 22265856 5228 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14648/statm): 5436 5228 145 145 0 5291 0 [pid=14648] vsize: 21744 Current children cumulated CPU time (s) 779.56 Current children cumulated vsize (Kb) 23868 [startup+790.05 s] Raw data (loadavg): 1.00 1.00 0.92 2/57 14648 Raw data (/proc/14644/stat): 14644 (minisat+_script) S 14643 14644 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797505173 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14644/statm): 531 226 485 147 0 384 0 [pid=14644] vsize: 2124 Raw data (/proc/14648/stat): 14648 (minisat+_64-bit) R 14644 14644 22582 0 -1 0 5277 0 0 0 78914 42 0 0 25 0 1 0 1797505178 22265856 5228 4294967295 134512640 135094434 3221224448 3221223104 134558029 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14648/statm): 5436 5228 145 145 0 5291 0 [pid=14648] vsize: 21744 Current children cumulated CPU time (s) 789.56 Current children cumulated vsize (Kb) 23868 [startup+800.051 s] Raw data (loadavg): 1.00 1.00 0.92 2/57 14648 Raw data (/proc/14644/stat): 14644 (minisat+_script) S 14643 14644 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797505173 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14644/statm): 531 226 485 147 0 384 0 [pid=14644] vsize: 2124 Raw data (/proc/14648/stat): 14648 (minisat+_64-bit) R 14644 14644 22582 0 -1 0 5277 0 0 0 79915 42 0 0 25 0 1 0 1797505178 22265856 5228 4294967295 134512640 135094434 3221224448 3221223104 134557976 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14648/statm): 5436 5228 145 145 0 5291 0 [pid=14648] vsize: 21744 Current children cumulated CPU time (s) 799.57 Current children cumulated vsize (Kb) 23868 [startup+810.052 s] Raw data (loadavg): 1.00 1.00 0.92 2/57 14648 Raw data (/proc/14644/stat): 14644 (minisat+_script) S 14643 14644 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797505173 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14644/statm): 531 226 485 147 0 384 0 [pid=14644] vsize: 2124 Raw data (/proc/14648/stat): 14648 (minisat+_64-bit) R 14644 14644 22582 0 -1 0 5277 0 0 0 80915 42 0 0 25 0 1 0 1797505178 22265856 5228 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14648/statm): 5436 5228 145 145 0 5291 0 [pid=14648] vsize: 21744 Current children cumulated CPU time (s) 809.57 Current children cumulated vsize (Kb) 23868 [startup+820.053 s] Raw data (loadavg): 1.00 1.00 0.92 2/57 14648 Raw data (/proc/14644/stat): 14644 (minisat+_script) S 14643 14644 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797505173 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14644/statm): 531 226 485 147 0 384 0 [pid=14644] vsize: 2124 Raw data (/proc/14648/stat): 14648 (minisat+_64-bit) R 14644 14644 22582 0 -1 0 5277 0 0 0 81915 42 0 0 25 0 1 0 1797505178 22265856 5228 4294967295 134512640 135094434 3221224448 3221223104 134558210 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14648/statm): 5436 5228 145 145 0 5291 0 [pid=14648] vsize: 21744 Current children cumulated CPU time (s) 819.57 Current children cumulated vsize (Kb) 23868 [startup+830.054 s] Raw data (loadavg): 1.00 1.00 0.92 2/57 14648 Raw data (/proc/14644/stat): 14644 (minisat+_script) S 14643 14644 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797505173 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14644/statm): 531 226 485 147 0 384 0 [pid=14644] vsize: 2124 Raw data (/proc/14648/stat): 14648 (minisat+_64-bit) R 14644 14644 22582 0 -1 0 5277 0 0 0 82915 42 0 0 25 0 1 0 1797505178 22265856 5228 4294967295 134512640 135094434 3221224448 3221223104 134558420 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14648/statm): 5436 5228 145 145 0 5291 0 [pid=14648] vsize: 21744 Current children cumulated CPU time (s) 829.57 Current children cumulated vsize (Kb) 23868 [startup+840.054 s] Raw data (loadavg): 1.00 1.00 0.92 2/57 14648 Raw data (/proc/14644/stat): 14644 (minisat+_script) S 14643 14644 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797505173 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14644/statm): 531 226 485 147 0 384 0 [pid=14644] vsize: 2124 Raw data (/proc/14648/stat): 14648 (minisat+_64-bit) R 14644 14644 22582 0 -1 0 5277 0 0 0 83915 42 0 0 25 0 1 0 1797505178 22265856 5228 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14648/statm): 5436 5228 145 145 0 5291 0 [pid=14648] vsize: 21744 Current children cumulated CPU time (s) 839.57 Current children cumulated vsize (Kb) 23868 [startup+850.055 s] Raw data (loadavg): 1.00 1.00 0.92 2/57 14648 Raw data (/proc/14644/stat): 14644 (minisat+_script) S 14643 14644 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797505173 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14644/statm): 531 226 485 147 0 384 0 [pid=14644] vsize: 2124 Raw data (/proc/14648/stat): 14648 (minisat+_64-bit) R 14644 14644 22582 0 -1 0 5277 0 0 0 84915 42 0 0 25 0 1 0 1797505178 22265856 5228 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14648/statm): 5436 5228 145 145 0 5291 0 [pid=14648] vsize: 21744 Current children cumulated CPU time (s) 849.57 Current children cumulated vsize (Kb) 23868 [startup+860.055 s] Raw data (loadavg): 1.00 1.00 0.92 2/57 14648 Raw data (/proc/14644/stat): 14644 (minisat+_script) S 14643 14644 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797505173 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14644/statm): 531 226 485 147 0 384 0 [pid=14644] vsize: 2124 Raw data (/proc/14648/stat): 14648 (minisat+_64-bit) R 14644 14644 22582 0 -1 0 5277 0 0 0 85916 42 0 0 25 0 1 0 1797505178 22265856 5228 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14648/statm): 5436 5228 145 145 0 5291 0 [pid=14648] vsize: 21744 Current children cumulated CPU time (s) 859.58 Current children cumulated vsize (Kb) 23868 [startup+870.057 s] Raw data (loadavg): 1.00 1.00 0.92 2/57 14648 Raw data (/proc/14644/stat): 14644 (minisat+_script) S 14643 14644 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797505173 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14644/statm): 531 226 485 147 0 384 0 [pid=14644] vsize: 2124 Raw data (/proc/14648/stat): 14648 (minisat+_64-bit) R 14644 14644 22582 0 -1 0 5277 0 0 0 86916 42 0 0 25 0 1 0 1797505178 22265856 5228 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14648/statm): 5436 5228 145 145 0 5291 0 [pid=14648] vsize: 21744 Current children cumulated CPU time (s) 869.58 Current children cumulated vsize (Kb) 23868 [startup+880.057 s] Raw data (loadavg): 1.00 1.00 0.92 2/57 14648 Raw data (/proc/14644/stat): 14644 (minisat+_script) S 14643 14644 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797505173 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14644/statm): 531 226 485 147 0 384 0 [pid=14644] vsize: 2124 Raw data (/proc/14648/stat): 14648 (minisat+_64-bit) R 14644 14644 22582 0 -1 0 5277 0 0 0 87916 42 0 0 25 0 1 0 1797505178 22265856 5228 4294967295 134512640 135094434 3221224448 3221223104 134557875 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14648/statm): 5436 5228 145 145 0 5291 0 [pid=14648] vsize: 21744 Current children cumulated CPU time (s) 879.58 Current children cumulated vsize (Kb) 23868 [startup+890.057 s] Raw data (loadavg): 1.00 1.00 0.92 2/57 14648 Raw data (/proc/14644/stat): 14644 (minisat+_script) S 14643 14644 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797505173 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14644/statm): 531 226 485 147 0 384 0 [pid=14644] vsize: 2124 Raw data (/proc/14648/stat): 14648 (minisat+_64-bit) R 14644 14644 22582 0 -1 0 5277 0 0 0 88916 43 0 0 25 0 1 0 1797505178 22265856 5228 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14648/statm): 5436 5228 145 145 0 5291 0 [pid=14648] vsize: 21744 Current children cumulated CPU time (s) 889.59 Current children cumulated vsize (Kb) 23868 [startup+900.059 s] Raw data (loadavg): 1.00 1.00 0.92 2/57 14648 Raw data (/proc/14644/stat): 14644 (minisat+_script) S 14643 14644 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797505173 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14644/statm): 531 226 485 147 0 384 0 [pid=14644] vsize: 2124 Raw data (/proc/14648/stat): 14648 (minisat+_64-bit) R 14644 14644 22582 0 -1 0 5277 0 0 0 89917 43 0 0 25 0 1 0 1797505178 22265856 5228 4294967295 134512640 135094434 3221224448 3221223104 134557860 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14648/statm): 5436 5228 145 145 0 5291 0 [pid=14648] vsize: 21744 Current children cumulated CPU time (s) 899.6 Current children cumulated vsize (Kb) 23868 [startup+910.059 s] Raw data (loadavg): 1.00 1.00 0.92 2/57 14648 Raw data (/proc/14644/stat): 14644 (minisat+_script) S 14643 14644 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797505173 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14644/statm): 531 226 485 147 0 384 0 [pid=14644] vsize: 2124 Raw data (/proc/14648/stat): 14648 (minisat+_64-bit) R 14644 14644 22582 0 -1 0 5277 0 0 0 90917 43 0 0 25 0 1 0 1797505178 22265856 5228 4294967295 134512640 135094434 3221224448 3221223104 134558235 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14648/statm): 5436 5228 145 145 0 5291 0 [pid=14648] vsize: 21744 Current children cumulated CPU time (s) 909.6 Current children cumulated vsize (Kb) 23868 [startup+920.06 s] Raw data (loadavg): 1.00 1.00 0.92 2/57 14648 Raw data (/proc/14644/stat): 14644 (minisat+_script) S 14643 14644 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797505173 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14644/statm): 531 226 485 147 0 384 0 [pid=14644] vsize: 2124 Raw data (/proc/14648/stat): 14648 (minisat+_64-bit) R 14644 14644 22582 0 -1 0 5277 0 0 0 91917 43 0 0 25 0 1 0 1797505178 22265856 5228 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14648/statm): 5436 5228 145 145 0 5291 0 [pid=14648] vsize: 21744 Current children cumulated CPU time (s) 919.6 Current children cumulated vsize (Kb) 23868 [startup+930.061 s] Raw data (loadavg): 1.00 1.00 0.92 2/57 14648 Raw data (/proc/14644/stat): 14644 (minisat+_script) S 14643 14644 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797505173 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14644/statm): 531 226 485 147 0 384 0 [pid=14644] vsize: 2124 Raw data (/proc/14648/stat): 14648 (minisat+_64-bit) R 14644 14644 22582 0 -1 0 5277 0 0 0 92917 43 0 0 25 0 1 0 1797505178 22265856 5228 4294967295 134512640 135094434 3221224448 3221223072 134562139 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14648/statm): 5436 5228 145 145 0 5291 0 [pid=14648] vsize: 21744 Current children cumulated CPU time (s) 929.6 Current children cumulated vsize (Kb) 23868 [startup+940.062 s] Raw data (loadavg): 1.00 1.00 0.92 2/57 14648 Raw data (/proc/14644/stat): 14644 (minisat+_script) S 14643 14644 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797505173 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14644/statm): 531 226 485 147 0 384 0 [pid=14644] vsize: 2124 Raw data (/proc/14648/stat): 14648 (minisat+_64-bit) R 14644 14644 22582 0 -1 0 5277 0 0 0 93918 43 0 0 25 0 1 0 1797505178 22265856 5228 4294967295 134512640 135094434 3221224448 3221223104 134558213 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14648/statm): 5436 5228 145 145 0 5291 0 [pid=14648] vsize: 21744 Current children cumulated CPU time (s) 939.61 Current children cumulated vsize (Kb) 23868 [startup+950.062 s] Raw data (loadavg): 1.00 1.00 0.92 2/57 14648 Raw data (/proc/14644/stat): 14644 (minisat+_script) S 14643 14644 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797505173 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14644/statm): 531 226 485 147 0 384 0 [pid=14644] vsize: 2124 Raw data (/proc/14648/stat): 14648 (minisat+_64-bit) R 14644 14644 22582 0 -1 0 5277 0 0 0 94918 43 0 0 25 0 1 0 1797505178 22265856 5228 4294967295 134512640 135094434 3221224448 3221223104 134557928 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14648/statm): 5436 5228 145 145 0 5291 0 [pid=14648] vsize: 21744 Current children cumulated CPU time (s) 949.61 Current children cumulated vsize (Kb) 23868 [startup+960.063 s] Raw data (loadavg): 1.00 1.00 0.92 2/57 14648 Raw data (/proc/14644/stat): 14644 (minisat+_script) S 14643 14644 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797505173 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14644/statm): 531 226 485 147 0 384 0 [pid=14644] vsize: 2124 Raw data (/proc/14648/stat): 14648 (minisat+_64-bit) R 14644 14644 22582 0 -1 0 5277 0 0 0 95918 43 0 0 25 0 1 0 1797505178 22265856 5228 4294967295 134512640 135094434 3221224448 3221223104 134558249 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14648/statm): 5436 5228 145 145 0 5291 0 [pid=14648] vsize: 21744 Current children cumulated CPU time (s) 959.61 Current children cumulated vsize (Kb) 23868 [startup+970.064 s] Raw data (loadavg): 1.00 1.00 0.92 2/57 14648 Raw data (/proc/14644/stat): 14644 (minisat+_script) S 14643 14644 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797505173 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14644/statm): 531 226 485 147 0 384 0 [pid=14644] vsize: 2124 Raw data (/proc/14648/stat): 14648 (minisat+_64-bit) R 14644 14644 22582 0 -1 0 5277 0 0 0 96918 43 0 0 25 0 1 0 1797505178 22265856 5228 4294967295 134512640 135094434 3221224448 3221223104 134557917 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14648/statm): 5436 5228 145 145 0 5291 0 [pid=14648] vsize: 21744 Current children cumulated CPU time (s) 969.61 Current children cumulated vsize (Kb) 23868 [startup+980.065 s] Raw data (loadavg): 1.00 1.00 0.92 2/57 14648 Raw data (/proc/14644/stat): 14644 (minisat+_script) S 14643 14644 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797505173 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14644/statm): 531 226 485 147 0 384 0 [pid=14644] vsize: 2124 Raw data (/proc/14648/stat): 14648 (minisat+_64-bit) R 14644 14644 22582 0 -1 0 5277 0 0 0 97919 43 0 0 25 0 1 0 1797505178 22265856 5228 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14648/statm): 5436 5228 145 145 0 5291 0 [pid=14648] vsize: 21744 Current children cumulated CPU time (s) 979.62 Current children cumulated vsize (Kb) 23868 [startup+990.066 s] Raw data (loadavg): 1.00 1.00 0.92 2/57 14648 Raw data (/proc/14644/stat): 14644 (minisat+_script) S 14643 14644 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797505173 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14644/statm): 531 226 485 147 0 384 0 [pid=14644] vsize: 2124 Raw data (/proc/14648/stat): 14648 (minisat+_64-bit) R 14644 14644 22582 0 -1 0 5277 0 0 0 98919 43 0 0 25 0 1 0 1797505178 22265856 5228 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14648/statm): 5436 5228 145 145 0 5291 0 [pid=14648] vsize: 21744 Current children cumulated CPU time (s) 989.62 Current children cumulated vsize (Kb) 23868 [startup+1000.07 s] Raw data (loadavg): 1.00 1.00 0.92 2/57 14648 Raw data (/proc/14644/stat): 14644 (minisat+_script) S 14643 14644 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797505173 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14644/statm): 531 226 485 147 0 384 0 [pid=14644] vsize: 2124 Raw data (/proc/14648/stat): 14648 (minisat+_64-bit) R 14644 14644 22582 0 -1 0 5442 0 0 0 99916 43 0 0 25 0 1 0 1797505178 22941696 5393 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14648/statm): 5601 5393 145 145 0 5456 0 [pid=14648] vsize: 22404 Current children cumulated CPU time (s) 999.59 Current children cumulated vsize (Kb) 24528 [startup+1010.07 s] Raw data (loadavg): 1.00 1.00 0.92 2/57 14648 Raw data (/proc/14644/stat): 14644 (minisat+_script) S 14643 14644 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797505173 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14644/statm): 531 226 485 147 0 384 0 [pid=14644] vsize: 2124 Raw data (/proc/14648/stat): 14648 (minisat+_64-bit) R 14644 14644 22582 0 -1 0 5443 0 0 0 100917 43 0 0 25 0 1 0 1797505178 22941696 5394 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14648/statm): 5601 5394 145 145 0 5456 0 [pid=14648] vsize: 22404 Current children cumulated CPU time (s) 1009.6 Current children cumulated vsize (Kb) 24528 [startup+1020.07 s] Raw data (loadavg): 1.00 1.00 0.92 2/57 14648 Raw data (/proc/14644/stat): 14644 (minisat+_script) S 14643 14644 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797505173 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14644/statm): 531 226 485 147 0 384 0 [pid=14644] vsize: 2124 Raw data (/proc/14648/stat): 14648 (minisat+_64-bit) R 14644 14644 22582 0 -1 0 5443 0 0 0 101917 44 0 0 25 0 1 0 1797505178 22941696 5394 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14648/statm): 5601 5394 145 145 0 5456 0 [pid=14648] vsize: 22404 Current children cumulated CPU time (s) 1019.61 Current children cumulated vsize (Kb) 24528 [startup+1030.07 s] Raw data (loadavg): 1.00 1.00 0.92 2/57 14648 Raw data (/proc/14644/stat): 14644 (minisat+_script) S 14643 14644 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797505173 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14644/statm): 531 226 485 147 0 384 0 [pid=14644] vsize: 2124 Raw data (/proc/14648/stat): 14648 (minisat+_64-bit) R 14644 14644 22582 0 -1 0 5443 0 0 0 102917 44 0 0 25 0 1 0 1797505178 22941696 5394 4294967295 134512640 135094434 3221224448 3221223104 134558235 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14648/statm): 5601 5394 145 145 0 5456 0 [pid=14648] vsize: 22404 Current children cumulated CPU time (s) 1029.61 Current children cumulated vsize (Kb) 24528 [startup+1040.07 s] Raw data (loadavg): 1.00 1.00 0.92 2/57 14648 Raw data (/proc/14644/stat): 14644 (minisat+_script) S 14643 14644 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797505173 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14644/statm): 531 226 485 147 0 384 0 [pid=14644] vsize: 2124 Raw data (/proc/14648/stat): 14648 (minisat+_64-bit) R 14644 14644 22582 0 -1 0 5443 0 0 0 103917 44 0 0 25 0 1 0 1797505178 22941696 5394 4294967295 134512640 135094434 3221224448 3221223104 134558178 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14648/statm): 5601 5394 145 145 0 5456 0 [pid=14648] vsize: 22404 Current children cumulated CPU time (s) 1039.61 Current children cumulated vsize (Kb) 24528 [startup+1050.07 s] Raw data (loadavg): 1.00 1.00 0.92 2/57 14648 Raw data (/proc/14644/stat): 14644 (minisat+_script) S 14643 14644 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797505173 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14644/statm): 531 226 485 147 0 384 0 [pid=14644] vsize: 2124 Raw data (/proc/14648/stat): 14648 (minisat+_64-bit) R 14644 14644 22582 0 -1 0 5443 0 0 0 104917 44 0 0 25 0 1 0 1797505178 22941696 5394 4294967295 134512640 135094434 3221224448 3221223104 134557950 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14648/statm): 5601 5394 145 145 0 5456 0 [pid=14648] vsize: 22404 Current children cumulated CPU time (s) 1049.61 Current children cumulated vsize (Kb) 24528 [startup+1060.07 s] Raw data (loadavg): 1.00 1.00 0.92 2/57 14648 Raw data (/proc/14644/stat): 14644 (minisat+_script) S 14643 14644 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797505173 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14644/statm): 531 226 485 147 0 384 0 [pid=14644] vsize: 2124 Raw data (/proc/14648/stat): 14648 (minisat+_64-bit) R 14644 14644 22582 0 -1 0 5443 0 0 0 105918 44 0 0 25 0 1 0 1797505178 22941696 5394 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14648/statm): 5601 5394 145 145 0 5456 0 [pid=14648] vsize: 22404 Current children cumulated CPU time (s) 1059.62 Current children cumulated vsize (Kb) 24528 [startup+1070.07 s] Raw data (loadavg): 1.00 1.00 0.92 2/57 14648 Raw data (/proc/14644/stat): 14644 (minisat+_script) S 14643 14644 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797505173 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14644/statm): 531 226 485 147 0 384 0 [pid=14644] vsize: 2124 Raw data (/proc/14648/stat): 14648 (minisat+_64-bit) R 14644 14644 22582 0 -1 0 5448 0 0 0 106918 44 0 0 25 0 1 0 1797505178 22974464 5399 4294967295 134512640 135094434 3221224448 3221223104 134558235 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14648/statm): 5609 5399 145 145 0 5464 0 [pid=14648] vsize: 22436 Current children cumulated CPU time (s) 1069.62 Current children cumulated vsize (Kb) 24560 [startup+1080.07 s] Raw data (loadavg): 1.00 1.00 0.92 2/57 14648 Raw data (/proc/14644/stat): 14644 (minisat+_script) S 14643 14644 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797505173 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14644/statm): 531 226 485 147 0 384 0 [pid=14644] vsize: 2124 Raw data (/proc/14648/stat): 14648 (minisat+_64-bit) R 14644 14644 22582 0 -1 0 5589 0 0 0 107915 45 0 0 25 0 1 0 1797505178 23556096 5540 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14648/statm): 5751 5540 145 145 0 5606 0 [pid=14648] vsize: 23004 Current children cumulated CPU time (s) 1079.6 Current children cumulated vsize (Kb) 25128 [startup+1090.07 s] Raw data (loadavg): 1.00 1.00 0.92 2/57 14648 Raw data (/proc/14644/stat): 14644 (minisat+_script) S 14643 14644 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797505173 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14644/statm): 531 226 485 147 0 384 0 [pid=14644] vsize: 2124 Raw data (/proc/14648/stat): 14648 (minisat+_64-bit) R 14644 14644 22582 0 -1 0 5769 0 0 0 108912 46 0 0 25 0 1 0 1797505178 24297472 5720 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14648/statm): 5932 5720 145 145 0 5787 0 [pid=14648] vsize: 23728 Current children cumulated CPU time (s) 1089.58 Current children cumulated vsize (Kb) 25852 [startup+1100.07 s] Raw data (loadavg): 1.00 1.00 0.92 2/57 14648 Raw data (/proc/14644/stat): 14644 (minisat+_script) S 14643 14644 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797505173 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14644/statm): 531 226 485 147 0 384 0 [pid=14644] vsize: 2124 Raw data (/proc/14648/stat): 14648 (minisat+_64-bit) R 14644 14644 22582 0 -1 0 5929 0 0 0 109908 48 0 0 25 0 1 0 1797505178 24944640 5880 4294967295 134512640 135094434 3221224448 3221223104 134558159 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14648/statm): 6090 5880 145 145 0 5945 0 [pid=14648] vsize: 24360 Current children cumulated CPU time (s) 1099.56 Current children cumulated vsize (Kb) 26484 [startup+1110.07 s] Raw data (loadavg): 1.00 1.00 0.92 2/57 14648 Raw data (/proc/14644/stat): 14644 (minisat+_script) S 14643 14644 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797505173 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14644/statm): 531 226 485 147 0 384 0 [pid=14644] vsize: 2124 Raw data (/proc/14648/stat): 14648 (minisat+_64-bit) R 14644 14644 22582 0 -1 0 6036 0 0 0 110906 48 0 0 25 0 1 0 1797505178 25374720 5987 4294967295 134512640 135094434 3221224448 3221223120 134555673 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14648/statm): 6195 5987 145 145 0 6050 0 [pid=14648] vsize: 24780 Current children cumulated CPU time (s) 1109.54 Current children cumulated vsize (Kb) 26904 [startup+1120.07 s] Raw data (loadavg): 1.00 1.00 0.92 2/57 14648 Raw data (/proc/14644/stat): 14644 (minisat+_script) S 14643 14644 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797505173 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14644/statm): 531 226 485 147 0 384 0 [pid=14644] vsize: 2124 Raw data (/proc/14648/stat): 14648 (minisat+_64-bit) R 14644 14644 22582 0 -1 0 6036 0 0 0 111907 48 0 0 25 0 1 0 1797505178 25374720 5987 4294967295 134512640 135094434 3221224448 3221223104 134557911 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14648/statm): 6195 5987 145 145 0 6050 0 [pid=14648] vsize: 24780 Current children cumulated CPU time (s) 1119.55 Current children cumulated vsize (Kb) 26904 [startup+1130.08 s] Raw data (loadavg): 1.00 1.00 0.92 2/57 14648 Raw data (/proc/14644/stat): 14644 (minisat+_script) S 14643 14644 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797505173 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14644/statm): 531 226 485 147 0 384 0 [pid=14644] vsize: 2124 Raw data (/proc/14648/stat): 14648 (minisat+_64-bit) R 14644 14644 22582 0 -1 0 6036 0 0 0 112907 48 0 0 25 0 1 0 1797505178 25374720 5987 4294967295 134512640 135094434 3221224448 3221223120 134555568 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14648/statm): 6195 5987 145 145 0 6050 0 [pid=14648] vsize: 24780 Current children cumulated CPU time (s) 1129.55 Current children cumulated vsize (Kb) 26904 [startup+1140.08 s] Raw data (loadavg): 1.00 1.00 0.92 2/57 14648 Raw data (/proc/14644/stat): 14644 (minisat+_script) S 14643 14644 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797505173 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14644/statm): 531 226 485 147 0 384 0 [pid=14644] vsize: 2124 Raw data (/proc/14648/stat): 14648 (minisat+_64-bit) R 14644 14644 22582 0 -1 0 6036 0 0 0 113907 48 0 0 25 0 1 0 1797505178 25374720 5987 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14648/statm): 6195 5987 145 145 0 6050 0 [pid=14648] vsize: 24780 Current children cumulated CPU time (s) 1139.55 Current children cumulated vsize (Kb) 26904 [startup+1150.08 s] Raw data (loadavg): 1.00 1.00 0.92 2/57 14648 Raw data (/proc/14644/stat): 14644 (minisat+_script) S 14643 14644 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797505173 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14644/statm): 531 226 485 147 0 384 0 [pid=14644] vsize: 2124 Raw data (/proc/14648/stat): 14648 (minisat+_64-bit) R 14644 14644 22582 0 -1 0 6036 0 0 0 114908 48 0 0 25 0 1 0 1797505178 25374720 5987 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14648/statm): 6195 5987 145 145 0 6050 0 [pid=14648] vsize: 24780 Current children cumulated CPU time (s) 1149.56 Current children cumulated vsize (Kb) 26904 [startup+1160.08 s] Raw data (loadavg): 1.00 1.00 0.92 2/57 14648 Raw data (/proc/14644/stat): 14644 (minisat+_script) S 14643 14644 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797505173 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14644/statm): 531 226 485 147 0 384 0 [pid=14644] vsize: 2124 Raw data (/proc/14648/stat): 14648 (minisat+_64-bit) R 14644 14644 22582 0 -1 0 6036 0 0 0 115908 48 0 0 25 0 1 0 1797505178 25374720 5987 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14648/statm): 6195 5987 145 145 0 6050 0 [pid=14648] vsize: 24780 Current children cumulated CPU time (s) 1159.56 Current children cumulated vsize (Kb) 26904 [startup+1170.08 s] Raw data (loadavg): 1.00 1.00 0.92 2/57 14648 Raw data (/proc/14644/stat): 14644 (minisat+_script) S 14643 14644 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797505173 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14644/statm): 531 226 485 147 0 384 0 [pid=14644] vsize: 2124 Raw data (/proc/14648/stat): 14648 (minisat+_64-bit) R 14644 14644 22582 0 -1 0 6036 0 0 0 116908 48 0 0 25 0 1 0 1797505178 25374720 5987 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14648/statm): 6195 5987 145 145 0 6050 0 [pid=14648] vsize: 24780 Current children cumulated CPU time (s) 1169.56 Current children cumulated vsize (Kb) 26904 [startup+1180.08 s] Raw data (loadavg): 1.00 1.00 0.92 2/57 14648 Raw data (/proc/14644/stat): 14644 (minisat+_script) S 14643 14644 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797505173 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14644/statm): 531 226 485 147 0 384 0 [pid=14644] vsize: 2124 Raw data (/proc/14648/stat): 14648 (minisat+_64-bit) R 14644 14644 22582 0 -1 0 6036 0 0 0 117908 48 0 0 25 0 1 0 1797505178 25374720 5987 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14648/statm): 6195 5987 145 145 0 6050 0 [pid=14648] vsize: 24780 Current children cumulated CPU time (s) 1179.56 Current children cumulated vsize (Kb) 26904 [startup+1190.08 s] Raw data (loadavg): 1.00 1.00 0.92 2/57 14648 Raw data (/proc/14644/stat): 14644 (minisat+_script) S 14643 14644 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797505173 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14644/statm): 531 226 485 147 0 384 0 [pid=14644] vsize: 2124 Raw data (/proc/14648/stat): 14648 (minisat+_64-bit) R 14644 14644 22582 0 -1 0 6036 0 0 0 118909 48 0 0 25 0 1 0 1797505178 25374720 5987 4294967295 134512640 135094434 3221224448 3221223104 134557860 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14648/statm): 6195 5987 145 145 0 6050 0 [pid=14648] vsize: 24780 Current children cumulated CPU time (s) 1189.57 Current children cumulated vsize (Kb) 26904 [startup+1200.08 s] Raw data (loadavg): 1.00 1.00 0.92 2/57 14648 Raw data (/proc/14644/stat): 14644 (minisat+_script) S 14643 14644 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797505173 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14644/statm): 531 226 485 147 0 384 0 [pid=14644] vsize: 2124 Raw data (/proc/14648/stat): 14648 (minisat+_64-bit) R 14644 14644 22582 0 -1 0 6036 0 0 0 119909 48 0 0 25 0 1 0 1797505178 25374720 5987 4294967295 134512640 135094434 3221224448 3221223104 134558007 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14648/statm): 6195 5987 145 145 0 6050 0 [pid=14648] vsize: 24780 Current children cumulated CPU time (s) 1199.57 Current children cumulated vsize (Kb) 26904 [startup+1210.08 s] Raw data (loadavg): 1.00 1.00 0.92 2/57 14648 Raw data (/proc/14644/stat): 14644 (minisat+_script) S 14643 14644 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797505173 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14644/statm): 531 226 485 147 0 384 0 [pid=14644] vsize: 2124 Raw data (/proc/14648/stat): 14648 (minisat+_64-bit) R 14644 14644 22582 0 -1 0 6036 0 0 0 120909 48 0 0 25 0 1 0 1797505178 25374720 5987 4294967295 134512640 135094434 3221224448 3221223136 134554676 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14648/statm): 6195 5987 145 145 0 6050 0 [pid=14648] vsize: 24780 Current children cumulated CPU time (s) 1209.57 Current children cumulated vsize (Kb) 26904 Maximum CPU time exceeded: sending SIGTERM then SIGKILL [startup+1210.08 s] Raw data (loadavg): 1.00 1.00 0.92 2/57 14648 Raw data (/proc/14644/stat): 14644 (minisat+_script) S 14643 14644 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1797505173 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14644/statm): 531 226 485 147 0 384 0 [pid=14644] vsize: 2124 Raw data (/proc/14648/stat): 14648 (minisat+_64-bit) R 14644 14644 22582 0 -1 0 6036 0 0 0 120909 48 0 0 25 0 1 0 1797505178 25374720 5987 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14648/statm): 6195 5987 145 145 0 6050 0 [pid=14648] vsize: 24780 Current children cumulated CPU time (s) 1209.57 Current children cumulated vsize (Kb) 26904 Sending SIGTERM to -14644 Sleeping 2 seconds One traced child (pid=14644) ended because it received signal 15 (SIGTERM) One traced child (pid=14648) exited with status: 10 All traced children have exited ! Game is over. Child status: 10 Real time (s): 1210.1 CPU time (s): 1209.6 CPU user time (s): 1209.1 CPU system time (s): 0.501923 CPU usage (%): 99.9586 Max. virtual memory (cumulated for all children) (Kb): 26904
ERROR: no interpretation found !