| Name | mps-v2-20-10/MIPLIB/miplib2003/normalized-mps-v2-20-10-misc07.opb |
| MD5SUM | b8ad25b48a93aa2545086c9eaeaee0ef |
| Bench Category | optimization, big integers (OPTBIGINT) |
| Has Objective Function | YES |
| Satisfiable | YES |
| (Un)Satisfiability was proved | YES |
| Best value of the objective function | 1076618240 |
| Optimality of the best value was proved | NO |
| Number of terms in the objective function | 31 |
| Biggest coefficient in the objective function | 1073741824 |
| Number of bits for the biggest coefficient in the objective function | 31 |
| Sum of the numbers in the objective function | 2147483647 |
| Number of bits of the sum of numbers in the objective function | 31 |
| Biggest number in a constraint | 1073741824 |
| Number of bits of the biggest number in a constraint | 31 |
| Biggest sum of numbers in a constraint | 3287948287 |
| Number of bits of the biggest sum of numbers | 32 |
| Best result obtained on this benchmark | SAT |
| Best CPU time to get the best result obtained on this benchmark | 1195.12 |
| Number of variables | 290 |
| Total number of constraints | 471 |
| Number of constraints which are clauses | 127 |
| Number of constraints which are cardinality constraints (but not clauses) | 272 |
| Number of constraints which are nor clauses,nor cardinality constraints | 72 |
| Minimum length of a constraint | 1 |
| Maximum length of a constraint | 263 |
LAUNCH ON wulflinc3 THE 2005-09-19 03:46:02 (client local time) PB2005-SCRIPT v4.0 MARKUPS: idlaunch=2920 boxname=wulflinc3 idbench=576 idsolver=3 numberseed=0 MD5SUM SOLVER: MD5SUM BENCH: b8ad25b48a93aa2545086c9eaeaee0ef /oldhome/oroussel/tmp/wulflinc3/normalized-mps-v2-20-10-misc07.opb REAL COMMAND: minisat+_script /oldhome/oroussel/tmp/wulflinc3/normalized-mps-v2-20-10-misc07.opb IDLAUNCH: 2920 /proc/cpuinfo: processor : 0 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 2 cpu MHz : 451.190 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 : 451.190 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: 911148 kB Buffers: 35340 kB Cached: 62132 kB SwapCached: 856 kB Active: 65428 kB Inactive: 34680 kB HighTotal: 131008 kB HighFree: 67368 kB LowTotal: 903652 kB LowFree: 843780 kB SwapTotal: 2097136 kB SwapFree: 2095712 kB Dirty: 28 kB Writeback: 0 kB Mapped: 5720 kB Slab: 17844 kB Committed_AS: 72360 kB PageTables: 328 kB VmallocTotal: 114680 kB VmallocUsed: 1388 kB VmallocChunk: 113256 kB JOB ENDED THE 2005-09-19 04:06:12 (client local time) WITH STATUS 10 IN 1209.71 SECONDS stats: 2920 7 1209.71 10
c Parsing PB file... c Converting 247 PB-constraints to clauses... c -- Unit propagations: (none) c -- Detecting intervals from adjacent constraints: ################################### c -- Clauses(.)/Splits(s): ............................................................................................................................... c ---[ 245]---> Adder-cost: 1708 maxlim: 1073742847 bits: 32/31 c ---[ 244]---> BDD-cost: 239 c ---[ 233]---> BDD-cost: 239 c ---[ 200]---> Sorter-cost: 127 Base: c ---[ 197]---> Sorter-cost: 127 Base: c ---[ 195]---> Sorter-cost: 127 Base: c ---[ 193]---> Sorter-cost: 127 Base: c ---[ 191]---> Sorter-cost: 127 Base: c ---[ 189]---> Sorter-cost: 127 Base: c ---[ 187]---> Sorter-cost: 127 Base: c ---[ 185]---> Sorter-cost: 127 Base: c ---[ 183]---> Sorter-cost: 127 Base: c ---[ 181]---> Sorter-cost: 127 Base: c ---[ 179]---> Sorter-cost: 127 Base: c ---[ 176]---> Sorter-cost: 127 Base: c ---[ 174]---> Sorter-cost: 127 Base: c ---[ 172]---> Sorter-cost: 127 Base: c ---[ 170]---> Sorter-cost: 127 Base: c ---[ 168]---> Sorter-cost: 127 Base: c ---[ 166]---> Sorter-cost: 127 Base: c ---[ 164]---> Sorter-cost: 127 Base: c ---[ 162]---> Sorter-cost: 127 Base: c ---[ 160]---> Sorter-cost: 127 Base: c ---[ 158]---> Sorter-cost: 127 Base: c ---[ 155]---> Sorter-cost: 127 Base: c ---[ 153]---> Sorter-cost: 127 Base: c ---[ 151]---> Sorter-cost: 127 Base: c ---[ 149]---> Sorter-cost: 127 Base: c ---[ 147]---> Sorter-cost: 127 Base: c ---[ 145]---> Sorter-cost: 127 Base: c ---[ 144]---> BDD-cost: 23 c ---[ 143]---> BDD-cost: 23 c ---[ 142]---> BDD-cost: 23 c ---[ 141]---> BDD-cost: 7 c ---[ 139]---> BDD-cost: 7 c ---[ 138]---> BDD-cost: 50 c ---[ 137]---> BDD-cost: 27 c ---[ 136]---> BDD-cost: 27 c ---[ 135]---> BDD-cost: 27 c ---[ 134]---> BDD-cost: 27 c ---[ 133]---> BDD-cost: 27 c ---[ 132]---> BDD-cost: 50 c ---[ 131]---> BDD-cost: 50 c ---[ 130]---> BDD-cost: 50 c ---[ 128]---> BDD-cost: 27 c ---[ 127]---> BDD-cost: 27 c ---[ 126]---> BDD-cost: 27 c ---[ 125]---> BDD-cost: 48 c ---[ 124]---> BDD-cost: 48 c ---[ 123]---> BDD-cost: 48 c ---[ 122]---> BDD-cost: 27 c ---[ 121]---> BDD-cost: 27 c ---[ 120]---> BDD-cost: 27 c ---[ 119]---> BDD-cost: 50 c ---[ 117]---> BDD-cost: 50 c ---[ 116]---> BDD-cost: 50 c ---[ 115]---> BDD-cost: 27 c ---[ 114]---> BDD-cost: 27 c ---[ 113]---> BDD-cost: 27 c ---[ 112]---> BDD-cost: 48 c ---[ 111]---> BDD-cost: 48 c ---[ 110]---> BDD-cost: 48 c ---[ 109]---> BDD-cost: 27 c ---[ 108]---> BDD-cost: 27 c ---[ 106]---> BDD-cost: 51 c ---[ 104]---> BDD-cost: 27 c ---[ 103]---> BDD-cost: 50 c ---[ 102]---> BDD-cost: 50 c ---[ 101]---> BDD-cost: 50 c ---[ 100]---> BDD-cost: 27 c ---[ 99]---> BDD-cost: 27 c ---[ 98]---> BDD-cost: 27 c ---[ 97]---> BDD-cost: 48 c ---[ 96]---> BDD-cost: 48 c ---[ 95]---> BDD-cost: 48 c ---[ 93]---> BDD-cost: 27 c ---[ 92]---> BDD-cost: 27 c ---[ 91]---> BDD-cost: 27 c ---[ 81]---> BDD-cost: 51 c ---[ 69]---> BDD-cost: 51 c ---[ 57]---> BDD-cost: 51 c ---[ 45]---> BDD-cost: 51 c ---[ 33]---> BDD-cost: 51 c ---[ 21]---> BDD-cost: 51 c ---[ 10]---> BDD-cost: 216 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 0 | 25851 84536 | 8617 0 0 nan | 0.000 % | c ============================================================================== c [1mFound solution: 1079342080[0m c ---[ 0]---> BDD-cost: 20 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 11 | 25847 84530 | 8615 4 91 22.8 | 0.000 % | c ============================================================================== c [1mFound solution: 1078517760[0m c ---[ 0]---> BDD-cost: 17 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 64 | 25866 84573 | 8622 57 1765 31.0 | 0.000 % | c | 164 | 25866 84573 | 9484 157 10915 69.5 | 3.029 % | c | 318 | 25866 84573 | 10432 311 16922 54.4 | 3.029 % | c ============================================================================== c [1mFound solution: 1078481920[0m c ---[ 0]---> BDD-cost: 18 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 339 | 25889 84624 | 8629 332 17661 53.2 | 3.029 % | c | 439 | 25889 84624 | 9491 432 21117 48.9 | 3.039 % | c ============================================================================== c [1mFound solution: 1078420480[0m c ---[ 0]---> BDD-cost: 19 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 520 | 25856 84552 | 8618 509 24798 48.7 | 3.039 % | c | 620 | 25814 84402 | 9479 604 26766 44.3 | 3.279 % | c ============================================================================== c [1mFound solution: 1078205440[0m c ---[ 0]---> BDD-cost: 20 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 647 | 25825 84427 | 8608 630 27468 43.6 | 3.279 % | c | 747 | 25825 84427 | 9468 730 37287 51.1 | 3.333 % | c | 897 | 25825 84427 | 10415 880 44135 50.2 | 3.333 % | c ============================================================================== c [1mFound solution: 1078133760[0m c ---[ 0]---> BDD-cost: 18 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 961 | 25838 84456 | 8612 942 47501 50.4 | 3.333 % | c | 1067 | 25838 84456 | 9473 1048 48813 46.6 | 3.373 % | c ============================================================================== c [1mFound solution: 1078128640[0m c ---[ 0]---> BDD-cost: 18 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 1115 | 25857 84500 | 8619 1096 54832 50.0 | 3.373 % | c | 1215 | 25857 84500 | 9480 1196 55960 46.8 | 3.384 % | c | 1366 | 25857 84500 | 10428 1347 67021 49.8 | 3.384 % | c | 1591 | 25785 84246 | 11471 1565 74693 47.7 | 3.456 % | c ============================================================================== c [1mFound solution: 1078056960[0m c ---[ 0]---> BDD-cost: 19 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 1704 | 25805 84292 | 8601 1678 81511 48.6 | 3.456 % | c ============================================================================== c [1mFound solution: 1077985280[0m c ---[ 0]---> BDD-cost: 16 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 1752 | 25812 84307 | 8604 1725 85915 49.8 | 3.456 % | c | 1853 | 25812 84307 | 9464 1826 86621 47.4 | 3.521 % | c ============================================================================== c [1mFound solution: 1077949440[0m c ---[ 0]---> BDD-cost: 17 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 1938 | 25791 84259 | 8597 1905 89268 46.9 | 3.521 % | c | 2042 | 25791 84259 | 9456 2009 97273 48.4 | 3.704 % | c | 2192 | 25731 84043 | 10402 2153 101486 47.1 | 3.732 % | c ============================================================================== c [1mFound solution: 1077944320[0m c ---[ 0]---> BDD-cost: 17 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 2274 | 25750 84083 | 8583 2235 106881 47.8 | 3.732 % | c | 2376 | 25750 84083 | 9441 2337 110992 47.5 | 3.744 % | c ============================================================================== c [1mFound solution: 1077898240[0m c ---[ 0]---> BDD-cost: 19 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 2455 | 25767 84127 | 8589 2416 117335 48.6 | 3.744 % | c | 2556 | 25746 84052 | 9447 2514 119722 47.6 | 3.769 % | c | 2708 | 25731 83999 | 10392 2664 127317 47.8 | 3.783 % | c | 2934 | 25718 83969 | 11431 2888 162522 56.3 | 3.826 % | c ============================================================================== c [1mFound solution: 1077724160[0m c ---[ 0]---> BDD-cost: 17 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 3124 | 25720 83957 | 8573 3073 171984 56.0 | 3.826 % | c | 3226 | 25720 83957 | 9430 3175 176631 55.6 | 3.851 % | c | 3378 | 25720 83957 | 10373 3327 198826 59.8 | 3.851 % | c | 3604 | 25720 83957 | 11410 3553 206694 58.2 | 3.851 % | c | 3941 | 25720 83957 | 12551 3890 257360 66.2 | 3.851 % | c ============================================================================== c [1mFound solution: 1077611520[0m c ---[ 0]---> BDD-cost: 18 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 4345 | 25705 83882 | 8568 4292 298875 69.6 | 3.851 % | c | 4445 | 25609 83544 | 9424 4381 301713 68.9 | 3.990 % | c | 4595 | 25609 83544 | 10367 4531 311528 68.8 | 3.990 % | c | 4820 | 25609 83544 | 11404 4756 331547 69.7 | 3.990 % | c | 5157 | 25591 83505 | 12544 5089 376075 73.9 | 4.061 % | c ============================================================================== c [1mFound solution: 1077565440[0m c ---[ 0]---> BDD-cost: 16 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 5223 | 25609 83547 | 8536 5155 380655 73.8 | 4.061 % | c | 5323 | 25609 83547 | 9389 5255 386864 73.6 | 4.071 % | c | 5474 | 25609 83547 | 10328 5406 407086 75.3 | 4.071 % | c | 5702 | 25541 83359 | 11361 5605 421575 75.2 | 4.255 % | c | 6039 | 25541 83359 | 12497 5942 453221 76.3 | 4.255 % | c ============================================================================== c [1mFound solution: 1077478400[0m c ---[ 0]---> BDD-cost: 14 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 6099 | 25556 83394 | 8518 6002 460270 76.7 | 4.255 % | c | 6199 | 25556 83394 | 9369 6102 465232 76.2 | 4.266 % | c | 6350 | 25556 83394 | 10306 6253 486947 77.9 | 4.266 % | c | 6575 | 25493 83175 | 11337 6471 490780 75.8 | 4.352 % | c | 6913 | 25482 83151 | 12471 6807 508713 74.7 | 4.394 % | c | 7420 | 25482 83151 | 13718 7314 553071 75.6 | 4.394 % | c | 8179 | 25482 83151 | 15090 8073 641561 79.5 | 4.394 % | c ============================================================================== c [1mFound solution: 1077457920[0m c ---[ 0]---> BDD-cost: 16 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 8472 | 25500 83192 | 8500 8366 660683 79.0 | 4.394 % | c | 8573 | 25500 83192 | 9350 8467 668523 79.0 | 4.404 % | c | 8723 | 25500 83192 | 10285 8617 692126 80.3 | 4.404 % | c | 8949 | 25472 83110 | 11313 8840 704972 79.7 | 4.475 % | c | 9289 | 25472 83110 | 12444 9180 740265 80.6 | 4.475 % | c | 9795 | 25472 83110 | 13689 9686 793671 81.9 | 4.475 % | c ============================================================================== c [1mFound solution: 1077345280[0m c ---[ 0]---> BDD-cost: 18 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 9842 | 25489 83152 | 8496 9733 795140 81.7 | 4.475 % | c | 9942 | 25489 83152 | 9345 4967 337006 67.8 | 4.485 % | c | 10094 | 25489 83152 | 10280 5119 341325 66.7 | 4.485 % | c | 10323 | 25478 83128 | 11308 5347 364771 68.2 | 4.527 % | c | 10664 | 25478 83128 | 12438 5688 383232 67.4 | 4.527 % | c ============================================================================== c [1mFound solution: 1076710400[0m c ---[ 0]---> BDD-cost: 17 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 10744 | 25500 83178 | 8500 5768 393632 68.2 | 4.527 % | c | 10844 | 25500 83178 | 9350 5868 395656 67.4 | 4.535 % | c | 10998 | 25418 82996 | 10285 6006 411279 68.5 | 4.874 % | c | 11225 | 25418 82996 | 11313 6233 426973 68.5 | 4.874 % | c | 11563 | 25418 82996 | 12444 6571 466696 71.0 | 4.874 % | c | 12071 | 25418 82996 | 13689 7079 493302 69.7 | 4.874 % | c | 12830 | 25418 82996 | 15058 7838 591857 75.5 | 4.874 % | c | 13970 | 25401 82958 | 16564 8977 714946 79.6 | 4.945 % | c | 15678 | 25390 82934 | 18220 10684 897257 84.0 | 4.987 % | c | 18244 | 25352 82816 | 20042 13246 1116382 84.3 | 5.086 % | c | 22088 | 25309 82665 | 22046 17087 1618618 94.7 | 5.171 % | c | 27858 | 25259 82519 | 24251 22843 1989220 87.1 | 5.284 % | c | 36507 | 25128 82090 | 26676 18784 1656576 88.2 | 5.538 % | c | 49481 | 25077 81913 | 29344 17628 1387747 78.7 | 5.609 % | c | 68945 | 25045 81842 | 32278 21913 2178315 99.4 | 5.736 % | c | 98137 | 24726 80932 | 35506 33927 3079942 90.8 | 6.654 % | c ============================================================================== c [1mFound solution: 1076705280[0m c ---[ 0]---> BDD-cost: 18 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 127765 | 24673 80815 | 8224 23020 2111284 91.7 | 6.654 % | c | 127866 | 24673 80815 | 9046 5856 311589 53.2 | 6.985 % | c | 128016 | 24673 80815 | 9951 6006 314957 52.4 | 6.985 % | c | 128241 | 24673 80815 | 10946 6231 333603 53.5 | 6.985 % | c | 128578 | 24666 80800 | 12040 6567 366560 55.8 | 7.013 % | c | 129084 | 24666 80800 | 13244 7073 399224 56.4 | 7.013 % | c | 129843 | 24666 80800 | 14569 7832 460274 58.8 | 7.013 % | c | 130982 | 24666 80800 | 16026 8971 574639 64.1 | 7.013 % | c | 132690 | 24629 80718 | 17628 10673 736057 69.0 | 7.168 % | c | 135252 | 24622 80703 | 19391 13233 1087697 82.2 | 7.196 % | c ============================================================================== c [1mFound solution: 1076674560[0m c ---[ 0]---> BDD-cost: 13 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 138836 | 24639 80741 | 8213 16817 1536401 91.4 | 7.196 % | c | 138937 | 24639 80741 | 9034 8510 711192 83.6 | 7.204 % | c | 139088 | 24639 80741 | 9937 8661 724525 83.7 | 7.204 % | c | 139313 | 24639 80741 | 10931 8886 743774 83.7 | 7.204 % | c | 139652 | 24639 80741 | 12024 9225 781501 84.7 | 7.204 % | c | 140158 | 24639 80741 | 13227 9731 854334 87.8 | 7.204 % | c | 140917 | 24527 80364 | 14549 10482 920049 87.8 | 7.430 % | c | 142057 | 24527 80364 | 16004 11622 1096546 94.4 | 7.430 % | c | 143765 | 24510 80326 | 17605 13329 1275622 95.7 | 7.500 % | c | 146328 | 24477 80254 | 19365 15885 1484207 93.4 | 7.627 % | c | 150176 | 24463 80221 | 21302 19731 1818948 92.2 | 7.670 % | c | 155942 | 24463 80221 | 23432 13932 973168 69.9 | 7.670 % | c | 164593 | 24392 79987 | 25775 22563 1808661 80.2 | 7.782 % | c ============================================================================== c [1mFound solution: 1076618240[0m c ---[ 0]---> BDD-cost: 16 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 171481 | 24409 80027 | 8136 15404 1317756 85.5 | 7.782 % | c | 171583 | 24409 80027 | 8949 7804 576344 73.9 | 7.789 % | c | 171733 | 24409 80027 | 9844 7954 588964 74.0 | 7.789 % | c | 171958 | 24409 80027 | 10829 8179 607574 74.3 | 7.789 % | c | 172296 | 24409 80027 | 11911 8517 636233 74.7 | 7.789 % | c | 172803 | 24409 80027 | 13103 9024 692041 76.7 | 7.789 % | c | 173562 | 24409 80027 | 14413 9783 788676 80.6 | 7.789 % | c | 174702 | 24400 80007 | 15854 10922 851407 78.0 | 7.831 % | c | 176413 | 24400 80007 | 17440 12633 1095521 86.7 | 7.831 % | c | 178977 | 24363 79914 | 19184 15189 1334750 87.9 | 7.958 % | c | 182825 | 24356 79899 | 21102 19035 1658896 87.1 | 7.986 % | c | 188591 | 24356 79899 | 23212 13144 933338 71.0 | 7.986 % | c | 197240 | 24356 79899 | 25534 21793 1707844 78.4 | 7.986 % | c | 210214 | 24320 79788 | 28087 21107 1426821 67.6 | 8.070 % | c | 229675 | 24311 79768 | 30896 25479 1931526 75.8 | 8.113 % | c | 258870 | 24252 79596 | 33986 21829 1523178 69.8 | 8.254 % | c | 302660 | 24206 79495 | 37384 26569 2716830 102.3 | 8.437 % | c | 368346 | 24189 79457 | 41123 26723 2058177 77.0 | 8.507 % |
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/24586/stat): 24586 (minisat+_script) R 24585 24586 31915 0 -1 0 19 0 0 0 0 0 0 0 23 0 1 0 1788522941 712704 3 4294967295 134512640 135087896 3221224512 3221224512 1073744960 0 0 5 0 0 0 0 17 1 0 0 Raw data (/proc/24586/statm): 174 3 169 147 0 27 0 [pid=24586] 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=24587 New process pid=24588 New process pid=24589 execve syscall for /bin/sed executable open syscall for file /etc/ld.so.preload One traced child (pid=24588) exited with status: 0 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=24589) exited with status: 0 One traced child (pid=24587) exited with status: 0 New process pid=24590 execve syscall for /oldhome/oroussel/solvers/minisat+_64-bit_static executable open syscall for file /dev/null open syscall for file /oldhome/oroussel/tmp/wulflinc3/normalized-mps-v2-20-10-misc07.opb [startup+10.0034 s] Raw data (loadavg): 0.93 0.99 0.98 2/57 24590 Raw data (/proc/24586/stat): 24586 (minisat+_script) S 24585 24586 31915 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1788522941 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/24586/statm): 531 226 485 147 0 384 0 [pid=24586] vsize: 2124 Raw data (/proc/24590/stat): 24590 (minisat+_64-bit) R 24586 24586 31915 0 -1 0 1246 0 0 0 983 6 0 0 25 0 1 0 1788522946 5169152 1152 4294967295 134512640 135094434 3221224432 3221223088 134557903 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/24590/statm): 1262 1152 145 145 0 1117 0 [pid=24590] vsize: 5048 Current children cumulated CPU time (s) 9.89 Current children cumulated vsize (Kb) 7172 [startup+20.0042 s] Raw data (loadavg): 0.94 0.99 0.98 1/57 24590 Raw data (/proc/24586/stat): 24586 (minisat+_script) S 24585 24586 31915 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1788522941 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/24586/statm): 531 226 485 147 0 384 0 [pid=24586] vsize: 2124 Raw data (/proc/24590/stat): 24590 (minisat+_64-bit) T 24586 24586 31915 0 -1 0 1924 0 0 0 1971 10 0 0 25 0 1 0 1788522946 7966720 1830 4294967295 134512640 135094434 3221224432 3221222812 134870330 0 0 5 16386 3222434794 0 0 17 0 0 0 Raw data (/proc/24590/statm): 1945 1830 145 145 0 1800 0 [pid=24590] vsize: 7780 Current children cumulated CPU time (s) 19.81 Current children cumulated vsize (Kb) 9904 [startup+30.0051 s] Raw data (loadavg): 0.95 0.99 0.98 2/57 24590 Raw data (/proc/24586/stat): 24586 (minisat+_script) S 24585 24586 31915 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1788522941 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/24586/statm): 531 226 485 147 0 384 0 [pid=24586] vsize: 2124 Raw data (/proc/24590/stat): 24590 (minisat+_64-bit) R 24586 24586 31915 0 -1 0 2045 0 0 0 2968 11 0 0 25 0 1 0 1788522946 8458240 1951 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/24590/statm): 2065 1951 145 145 0 1920 0 [pid=24590] vsize: 8260 Current children cumulated CPU time (s) 29.79 Current children cumulated vsize (Kb) 10384 [startup+40.0059 s] Raw data (loadavg): 0.96 0.99 0.98 2/57 24590 Raw data (/proc/24586/stat): 24586 (minisat+_script) S 24585 24586 31915 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1788522941 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/24586/statm): 531 226 485 147 0 384 0 [pid=24586] vsize: 2124 Raw data (/proc/24590/stat): 24590 (minisat+_64-bit) R 24586 24586 31915 0 -1 0 2536 0 0 0 3959 16 0 0 25 0 1 0 1788522946 10448896 2442 4294967295 134512640 135094434 3221224432 3221223088 134558225 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/24590/statm): 2551 2442 145 145 0 2406 0 [pid=24590] vsize: 10204 Current children cumulated CPU time (s) 39.75 Current children cumulated vsize (Kb) 12328 [startup+50.0067 s] Raw data (loadavg): 0.96 0.99 0.98 2/57 24590 Raw data (/proc/24586/stat): 24586 (minisat+_script) S 24585 24586 31915 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1788522941 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/24586/statm): 531 226 485 147 0 384 0 [pid=24586] vsize: 2124 Raw data (/proc/24590/stat): 24590 (minisat+_64-bit) R 24586 24586 31915 0 -1 0 3038 0 0 0 4950 20 0 0 25 0 1 0 1788522946 12550144 2944 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/24590/statm): 3064 2944 145 145 0 2919 0 [pid=24590] vsize: 12256 Current children cumulated CPU time (s) 49.7 Current children cumulated vsize (Kb) 14380 [startup+60.0066 s] Raw data (loadavg): 0.97 0.99 0.98 2/57 24590 Raw data (/proc/24586/stat): 24586 (minisat+_script) S 24585 24586 31915 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1788522941 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/24586/statm): 531 226 485 147 0 384 0 [pid=24586] vsize: 2124 Raw data (/proc/24590/stat): 24590 (minisat+_64-bit) R 24586 24586 31915 0 -1 0 3385 0 0 0 5943 23 0 0 25 0 1 0 1788522946 13955072 3291 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/24590/statm): 3407 3291 145 145 0 3262 0 [pid=24590] vsize: 13628 Current children cumulated CPU time (s) 59.66 Current children cumulated vsize (Kb) 15752 [startup+70.0084 s] Raw data (loadavg): 0.97 0.99 0.98 2/57 24590 Raw data (/proc/24586/stat): 24586 (minisat+_script) S 24585 24586 31915 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1788522941 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/24586/statm): 531 226 485 147 0 384 0 [pid=24586] vsize: 2124 Raw data (/proc/24590/stat): 24590 (minisat+_64-bit) R 24586 24586 31915 0 -1 0 3703 0 0 0 6939 26 0 0 25 0 1 0 1788522946 15249408 3609 4294967295 134512640 135094434 3221224432 3221223088 134558007 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/24590/statm): 3723 3609 145 145 0 3578 0 [pid=24590] vsize: 14892 Current children cumulated CPU time (s) 69.65 Current children cumulated vsize (Kb) 17016 [startup+80.0093 s] Raw data (loadavg): 0.98 0.99 0.98 2/57 24590 Raw data (/proc/24586/stat): 24586 (minisat+_script) S 24585 24586 31915 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1788522941 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/24586/statm): 531 226 485 147 0 384 0 [pid=24586] vsize: 2124 Raw data (/proc/24590/stat): 24590 (minisat+_64-bit) R 24586 24586 31915 0 -1 0 3703 0 0 0 7939 26 0 0 25 0 1 0 1788522946 15249408 3609 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/24590/statm): 3723 3609 145 145 0 3578 0 [pid=24590] vsize: 14892 Current children cumulated CPU time (s) 79.65 Current children cumulated vsize (Kb) 17016 [startup+90.0091 s] Raw data (loadavg): 0.98 0.99 0.98 2/57 24590 Raw data (/proc/24586/stat): 24586 (minisat+_script) S 24585 24586 31915 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1788522941 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/24586/statm): 531 226 485 147 0 384 0 [pid=24586] vsize: 2124 Raw data (/proc/24590/stat): 24590 (minisat+_64-bit) R 24586 24586 31915 0 -1 0 3703 0 0 0 8939 26 0 0 25 0 1 0 1788522946 15249408 3609 4294967295 134512640 135094434 3221224432 3221223024 134557369 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/24590/statm): 3723 3609 145 145 0 3578 0 [pid=24590] vsize: 14892 Current children cumulated CPU time (s) 89.65 Current children cumulated vsize (Kb) 17016 [startup+100.01 s] Raw data (loadavg): 0.98 0.99 0.98 2/57 24590 Raw data (/proc/24586/stat): 24586 (minisat+_script) S 24585 24586 31915 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1788522941 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/24586/statm): 531 226 485 147 0 384 0 [pid=24586] vsize: 2124 Raw data (/proc/24590/stat): 24590 (minisat+_64-bit) R 24586 24586 31915 0 -1 0 3879 0 0 0 9937 27 0 0 25 0 1 0 1788522946 15966208 3785 4294967295 134512640 135094434 3221224432 3221223088 134558013 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/24590/statm): 3898 3785 145 145 0 3753 0 [pid=24590] vsize: 15592 Current children cumulated CPU time (s) 99.64 Current children cumulated vsize (Kb) 17716 [startup+110.011 s] Raw data (loadavg): 0.98 0.99 0.98 2/57 24590 Raw data (/proc/24586/stat): 24586 (minisat+_script) S 24585 24586 31915 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1788522941 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/24586/statm): 531 226 485 147 0 384 0 [pid=24586] vsize: 2124 Raw data (/proc/24590/stat): 24590 (minisat+_64-bit) R 24586 24586 31915 0 -1 0 3975 0 0 0 10935 28 0 0 25 0 1 0 1788522946 16355328 3881 4294967295 134512640 135094434 3221224432 3221223024 134551908 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/24590/statm): 3993 3881 145 145 0 3848 0 [pid=24590] vsize: 15972 Current children cumulated CPU time (s) 109.63 Current children cumulated vsize (Kb) 18096 [startup+120.012 s] Raw data (loadavg): 0.99 0.99 0.98 2/57 24590 Raw data (/proc/24586/stat): 24586 (minisat+_script) S 24585 24586 31915 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1788522941 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/24586/statm): 531 226 485 147 0 384 0 [pid=24586] vsize: 2124 Raw data (/proc/24590/stat): 24590 (minisat+_64-bit) R 24586 24586 31915 0 -1 0 3975 0 0 0 11935 28 0 0 25 0 1 0 1788522946 16355328 3881 4294967295 134512640 135094434 3221224432 3221223088 134558235 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/24590/statm): 3993 3881 145 145 0 3848 0 [pid=24590] vsize: 15972 Current children cumulated CPU time (s) 119.63 Current children cumulated vsize (Kb) 18096 [startup+130.012 s] Raw data (loadavg): 0.99 0.99 0.98 2/57 24590 Raw data (/proc/24586/stat): 24586 (minisat+_script) S 24585 24586 31915 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1788522941 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/24586/statm): 531 226 485 147 0 384 0 [pid=24586] vsize: 2124 Raw data (/proc/24590/stat): 24590 (minisat+_64-bit) R 24586 24586 31915 0 -1 0 3975 0 0 0 12935 28 0 0 25 0 1 0 1788522946 16355328 3881 4294967295 134512640 135094434 3221224432 3221223088 134558022 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/24590/statm): 3993 3881 145 145 0 3848 0 [pid=24590] vsize: 15972 Current children cumulated CPU time (s) 129.63 Current children cumulated vsize (Kb) 18096 [startup+140.012 s] Raw data (loadavg): 0.99 0.99 0.98 2/57 24590 Raw data (/proc/24586/stat): 24586 (minisat+_script) S 24585 24586 31915 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1788522941 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/24586/statm): 531 226 485 147 0 384 0 [pid=24586] vsize: 2124 Raw data (/proc/24590/stat): 24590 (minisat+_64-bit) R 24586 24586 31915 0 -1 0 4321 0 0 0 13929 30 0 0 25 0 1 0 1788522946 17768448 4227 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/24590/statm): 4338 4227 145 145 0 4193 0 [pid=24590] vsize: 17352 Current children cumulated CPU time (s) 139.59 Current children cumulated vsize (Kb) 19476 [startup+150.013 s] Raw data (loadavg): 0.99 0.99 0.98 2/57 24590 Raw data (/proc/24586/stat): 24586 (minisat+_script) S 24585 24586 31915 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1788522941 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/24586/statm): 531 226 485 147 0 384 0 [pid=24586] vsize: 2124 Raw data (/proc/24590/stat): 24590 (minisat+_64-bit) R 24586 24586 31915 0 -1 0 4379 0 0 0 14928 31 0 0 25 0 1 0 1788522946 18006016 4285 4294967295 134512640 135094434 3221224432 3221223088 134557925 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/24590/statm): 4396 4285 145 145 0 4251 0 [pid=24590] vsize: 17584 Current children cumulated CPU time (s) 149.59 Current children cumulated vsize (Kb) 19708 [startup+160.014 s] Raw data (loadavg): 0.99 0.99 0.98 2/57 24590 Raw data (/proc/24586/stat): 24586 (minisat+_script) S 24585 24586 31915 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1788522941 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/24586/statm): 531 226 485 147 0 384 0 [pid=24586] vsize: 2124 Raw data (/proc/24590/stat): 24590 (minisat+_64-bit) R 24586 24586 31915 0 -1 0 4379 0 0 0 15928 31 0 0 25 0 1 0 1788522946 18006016 4285 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/24590/statm): 4396 4285 145 145 0 4251 0 [pid=24590] vsize: 17584 Current children cumulated CPU time (s) 159.59 Current children cumulated vsize (Kb) 19708 [startup+170.016 s] Raw data (loadavg): 0.99 0.99 0.98 2/57 24590 Raw data (/proc/24586/stat): 24586 (minisat+_script) S 24585 24586 31915 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1788522941 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/24586/statm): 531 226 485 147 0 384 0 [pid=24586] vsize: 2124 Raw data (/proc/24590/stat): 24590 (minisat+_64-bit) R 24586 24586 31915 0 -1 0 4489 0 0 0 16926 32 0 0 25 0 1 0 1788522946 18456576 4395 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/24590/statm): 4506 4395 145 145 0 4361 0 [pid=24590] vsize: 18024 Current children cumulated CPU time (s) 169.58 Current children cumulated vsize (Kb) 20148 [startup+180.017 s] Raw data (loadavg): 0.99 0.99 0.98 2/57 24590 Raw data (/proc/24586/stat): 24586 (minisat+_script) S 24585 24586 31915 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1788522941 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/24586/statm): 531 226 485 147 0 384 0 [pid=24586] vsize: 2124 Raw data (/proc/24590/stat): 24590 (minisat+_64-bit) R 24586 24586 31915 0 -1 0 4811 0 0 0 17920 34 0 0 25 0 1 0 1788522946 19771392 4717 4294967295 134512640 135094434 3221224432 3221223088 134558159 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/24590/statm): 4827 4717 145 145 0 4682 0 [pid=24590] vsize: 19308 Current children cumulated CPU time (s) 179.54 Current children cumulated vsize (Kb) 21432 [startup+190.018 s] Raw data (loadavg): 0.99 0.99 0.98 2/57 24590 Raw data (/proc/24586/stat): 24586 (minisat+_script) S 24585 24586 31915 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1788522941 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/24586/statm): 531 226 485 147 0 384 0 [pid=24586] vsize: 2124 Raw data (/proc/24590/stat): 24590 (minisat+_64-bit) R 24586 24586 31915 0 -1 0 5016 0 0 0 18919 34 0 0 25 0 1 0 1788522946 20746240 4922 4294967295 134512640 135094434 3221224432 3221223104 134556317 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/24590/statm): 5065 4922 145 145 0 4920 0 [pid=24590] vsize: 20260 Current children cumulated CPU time (s) 189.53 Current children cumulated vsize (Kb) 22384 [startup+200.018 s] Raw data (loadavg): 0.99 0.99 0.98 2/57 24590 Raw data (/proc/24586/stat): 24586 (minisat+_script) S 24585 24586 31915 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1788522941 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/24586/statm): 531 226 485 147 0 384 0 [pid=24586] vsize: 2124 Raw data (/proc/24590/stat): 24590 (minisat+_64-bit) R 24586 24586 31915 0 -1 0 5016 0 0 0 19919 34 0 0 25 0 1 0 1788522946 20746240 4922 4294967295 134512640 135094434 3221224432 3221223092 134553515 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/24590/statm): 5065 4922 145 145 0 4920 0 [pid=24590] vsize: 20260 Current children cumulated CPU time (s) 199.53 Current children cumulated vsize (Kb) 22384 [startup+210.018 s] Raw data (loadavg): 0.99 0.99 0.98 2/57 24590 Raw data (/proc/24586/stat): 24586 (minisat+_script) S 24585 24586 31915 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1788522941 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/24586/statm): 531 226 485 147 0 384 0 [pid=24586] vsize: 2124 Raw data (/proc/24590/stat): 24590 (minisat+_64-bit) R 24586 24586 31915 0 -1 0 5016 0 0 0 20919 34 0 0 25 0 1 0 1788522946 20746240 4922 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/24590/statm): 5065 4922 145 145 0 4920 0 [pid=24590] vsize: 20260 Current children cumulated CPU time (s) 209.53 Current children cumulated vsize (Kb) 22384 [startup+220.02 s] Raw data (loadavg): 0.99 0.99 0.98 2/57 24590 Raw data (/proc/24586/stat): 24586 (minisat+_script) S 24585 24586 31915 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1788522941 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/24586/statm): 531 226 485 147 0 384 0 [pid=24586] vsize: 2124 Raw data (/proc/24590/stat): 24590 (minisat+_64-bit) R 24586 24586 31915 0 -1 0 5016 0 0 0 21919 34 0 0 25 0 1 0 1788522946 20746240 4922 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/24590/statm): 5065 4922 145 145 0 4920 0 [pid=24590] vsize: 20260 Current children cumulated CPU time (s) 219.53 Current children cumulated vsize (Kb) 22384 [startup+230.021 s] Raw data (loadavg): 0.99 0.99 0.98 2/57 24590 Raw data (/proc/24586/stat): 24586 (minisat+_script) S 24585 24586 31915 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1788522941 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/24586/statm): 531 226 485 147 0 384 0 [pid=24586] vsize: 2124 Raw data (/proc/24590/stat): 24590 (minisat+_64-bit) R 24586 24586 31915 0 -1 0 5024 0 0 0 22920 34 0 0 25 0 1 0 1788522946 20779008 4930 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/24590/statm): 5073 4930 145 145 0 4928 0 [pid=24590] vsize: 20292 Current children cumulated CPU time (s) 229.54 Current children cumulated vsize (Kb) 22416 [startup+240.021 s] Raw data (loadavg): 0.99 0.99 0.98 2/57 24590 Raw data (/proc/24586/stat): 24586 (minisat+_script) S 24585 24586 31915 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1788522941 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/24586/statm): 531 226 485 147 0 384 0 [pid=24586] vsize: 2124 Raw data (/proc/24590/stat): 24590 (minisat+_64-bit) R 24586 24586 31915 0 -1 0 5043 0 0 0 23919 34 0 0 25 0 1 0 1788522946 20860928 4949 4294967295 134512640 135094434 3221224432 3221223088 134558249 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/24590/statm): 5093 4949 145 145 0 4948 0 [pid=24590] vsize: 20372 Current children cumulated CPU time (s) 239.53 Current children cumulated vsize (Kb) 22496 [startup+250.023 s] Raw data (loadavg): 0.99 0.99 0.98 2/57 24590 Raw data (/proc/24586/stat): 24586 (minisat+_script) S 24585 24586 31915 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1788522941 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/24586/statm): 531 226 485 147 0 384 0 [pid=24586] vsize: 2124 Raw data (/proc/24590/stat): 24590 (minisat+_64-bit) R 24586 24586 31915 0 -1 0 5224 0 0 0 24916 36 0 0 25 0 1 0 1788522946 21594112 5130 4294967295 134512640 135094434 3221224432 3221223088 134558162 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/24590/statm): 5272 5130 145 145 0 5127 0 [pid=24590] vsize: 21088 Current children cumulated CPU time (s) 249.52 Current children cumulated vsize (Kb) 23212 [startup+260.023 s] Raw data (loadavg): 0.99 0.99 0.98 2/57 24590 Raw data (/proc/24586/stat): 24586 (minisat+_script) S 24585 24586 31915 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1788522941 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/24586/statm): 531 226 485 147 0 384 0 [pid=24586] vsize: 2124 Raw data (/proc/24590/stat): 24590 (minisat+_64-bit) R 24586 24586 31915 0 -1 0 5224 0 0 0 25916 36 0 0 25 0 1 0 1788522946 21594112 5130 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/24590/statm): 5272 5130 145 145 0 5127 0 [pid=24590] vsize: 21088 Current children cumulated CPU time (s) 259.52 Current children cumulated vsize (Kb) 23212 [startup+270.024 s] Raw data (loadavg): 0.99 0.99 0.98 2/57 24590 Raw data (/proc/24586/stat): 24586 (minisat+_script) S 24585 24586 31915 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1788522941 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/24586/statm): 531 226 485 147 0 384 0 [pid=24586] vsize: 2124 Raw data (/proc/24590/stat): 24590 (minisat+_64-bit) R 24586 24586 31915 0 -1 0 5224 0 0 0 26917 36 0 0 25 0 1 0 1788522946 21594112 5130 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/24590/statm): 5272 5130 145 145 0 5127 0 [pid=24590] vsize: 21088 Current children cumulated CPU time (s) 269.53 Current children cumulated vsize (Kb) 23212 [startup+280.025 s] Raw data (loadavg): 0.99 0.99 0.98 2/57 24590 Raw data (/proc/24586/stat): 24586 (minisat+_script) S 24585 24586 31915 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1788522941 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/24586/statm): 531 226 485 147 0 384 0 [pid=24586] vsize: 2124 Raw data (/proc/24590/stat): 24590 (minisat+_64-bit) R 24586 24586 31915 0 -1 0 5260 0 0 0 27917 36 0 0 25 0 1 0 1788522946 21753856 5166 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/24590/statm): 5311 5166 145 145 0 5166 0 [pid=24590] vsize: 21244 Current children cumulated CPU time (s) 279.53 Current children cumulated vsize (Kb) 23368 [startup+290.026 s] Raw data (loadavg): 0.99 0.99 0.98 2/57 24590 Raw data (/proc/24586/stat): 24586 (minisat+_script) S 24585 24586 31915 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1788522941 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/24586/statm): 531 226 485 147 0 384 0 [pid=24586] vsize: 2124 Raw data (/proc/24590/stat): 24590 (minisat+_64-bit) R 24586 24586 31915 0 -1 0 5294 0 0 0 28917 36 0 0 25 0 1 0 1788522946 21950464 5200 4294967295 134512640 135094434 3221224432 3221223088 134557911 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/24590/statm): 5359 5200 145 145 0 5214 0 [pid=24590] vsize: 21436 Current children cumulated CPU time (s) 289.53 Current children cumulated vsize (Kb) 23560 [startup+300.027 s] Raw data (loadavg): 0.99 0.99 0.98 2/57 24590 Raw data (/proc/24586/stat): 24586 (minisat+_script) S 24585 24586 31915 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1788522941 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/24586/statm): 531 226 485 147 0 384 0 [pid=24586] vsize: 2124 Raw data (/proc/24590/stat): 24590 (minisat+_64-bit) R 24586 24586 31915 0 -1 0 5309 0 0 0 29917 36 0 0 25 0 1 0 1788522946 22032384 5215 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/24590/statm): 5379 5215 145 145 0 5234 0 [pid=24590] vsize: 21516 Current children cumulated CPU time (s) 299.53 Current children cumulated vsize (Kb) 23640 [startup+310.028 s] Raw data (loadavg): 0.99 0.99 0.98 2/57 24590 Raw data (/proc/24586/stat): 24586 (minisat+_script) S 24585 24586 31915 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1788522941 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/24586/statm): 531 226 485 147 0 384 0 [pid=24586] vsize: 2124 Raw data (/proc/24590/stat): 24590 (minisat+_64-bit) R 24586 24586 31915 0 -1 0 5310 0 0 0 30917 36 0 0 25 0 1 0 1788522946 22032384 5216 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/24590/statm): 5379 5216 145 145 0 5234 0 [pid=24590] vsize: 21516 Current children cumulated CPU time (s) 309.53 Current children cumulated vsize (Kb) 23640 [startup+320.028 s] Raw data (loadavg): 0.99 0.99 0.98 2/57 24590 Raw data (/proc/24586/stat): 24586 (minisat+_script) S 24585 24586 31915 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1788522941 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/24586/statm): 531 226 485 147 0 384 0 [pid=24586] vsize: 2124 Raw data (/proc/24590/stat): 24590 (minisat+_64-bit) R 24586 24586 31915 0 -1 0 5310 0 0 0 31918 36 0 0 25 0 1 0 1788522946 22032384 5216 4294967295 134512640 135094434 3221224432 3221223088 134557948 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/24590/statm): 5379 5216 145 145 0 5234 0 [pid=24590] vsize: 21516 Current children cumulated CPU time (s) 319.54 Current children cumulated vsize (Kb) 23640 [startup+330.029 s] Raw data (loadavg): 0.99 0.99 0.98 2/57 24590 Raw data (/proc/24586/stat): 24586 (minisat+_script) S 24585 24586 31915 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1788522941 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/24586/statm): 531 226 485 147 0 384 0 [pid=24586] vsize: 2124 Raw data (/proc/24590/stat): 24590 (minisat+_64-bit) R 24586 24586 31915 0 -1 0 5310 0 0 0 32917 36 0 0 25 0 1 0 1788522946 22032384 5216 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/24590/statm): 5379 5216 145 145 0 5234 0 [pid=24590] vsize: 21516 Current children cumulated CPU time (s) 329.53 Current children cumulated vsize (Kb) 23640 [startup+340.03 s] Raw data (loadavg): 0.99 0.99 0.98 2/57 24590 Raw data (/proc/24586/stat): 24586 (minisat+_script) S 24585 24586 31915 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1788522941 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/24586/statm): 531 226 485 147 0 384 0 [pid=24586] vsize: 2124 Raw data (/proc/24590/stat): 24590 (minisat+_64-bit) R 24586 24586 31915 0 -1 0 5310 0 0 0 33918 36 0 0 25 0 1 0 1788522946 22032384 5216 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/24590/statm): 5379 5216 145 145 0 5234 0 [pid=24590] vsize: 21516 Current children cumulated CPU time (s) 339.54 Current children cumulated vsize (Kb) 23640 [startup+350.031 s] Raw data (loadavg): 0.99 0.99 0.98 2/57 24590 Raw data (/proc/24586/stat): 24586 (minisat+_script) S 24585 24586 31915 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1788522941 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/24586/statm): 531 226 485 147 0 384 0 [pid=24586] vsize: 2124 Raw data (/proc/24590/stat): 24590 (minisat+_64-bit) R 24586 24586 31915 0 -1 0 5310 0 0 0 34918 36 0 0 25 0 1 0 1788522946 22032384 5216 4294967295 134512640 135094434 3221224432 3221223088 134558126 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/24590/statm): 5379 5216 145 145 0 5234 0 [pid=24590] vsize: 21516 Current children cumulated CPU time (s) 349.54 Current children cumulated vsize (Kb) 23640 [startup+360.032 s] Raw data (loadavg): 0.99 0.99 0.98 2/57 24590 Raw data (/proc/24586/stat): 24586 (minisat+_script) S 24585 24586 31915 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1788522941 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/24586/statm): 531 226 485 147 0 384 0 [pid=24586] vsize: 2124 Raw data (/proc/24590/stat): 24590 (minisat+_64-bit) R 24586 24586 31915 0 -1 0 5310 0 0 0 35917 36 0 0 25 0 1 0 1788522946 22032384 5216 4294967295 134512640 135094434 3221224432 3221223088 134558398 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/24590/statm): 5379 5216 145 145 0 5234 0 [pid=24590] vsize: 21516 Current children cumulated CPU time (s) 359.53 Current children cumulated vsize (Kb) 23640 [startup+370.034 s] Raw data (loadavg): 0.99 0.99 0.98 2/57 24590 Raw data (/proc/24586/stat): 24586 (minisat+_script) S 24585 24586 31915 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1788522941 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/24586/statm): 531 226 485 147 0 384 0 [pid=24586] vsize: 2124 Raw data (/proc/24590/stat): 24590 (minisat+_64-bit) R 24586 24586 31915 0 -1 0 5310 0 0 0 36917 36 0 0 25 0 1 0 1788522946 22032384 5216 4294967295 134512640 135094434 3221224432 3221223088 134558004 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/24590/statm): 5379 5216 145 145 0 5234 0 [pid=24590] vsize: 21516 Current children cumulated CPU time (s) 369.53 Current children cumulated vsize (Kb) 23640 [startup+380.034 s] Raw data (loadavg): 0.99 0.99 0.98 2/57 24590 Raw data (/proc/24586/stat): 24586 (minisat+_script) S 24585 24586 31915 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1788522941 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/24586/statm): 531 226 485 147 0 384 0 [pid=24586] vsize: 2124 Raw data (/proc/24590/stat): 24590 (minisat+_64-bit) R 24586 24586 31915 0 -1 0 5310 0 0 0 37918 36 0 0 25 0 1 0 1788522946 22032384 5216 4294967295 134512640 135094434 3221224432 3221223088 134558213 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/24590/statm): 5379 5216 145 145 0 5234 0 [pid=24590] vsize: 21516 Current children cumulated CPU time (s) 379.54 Current children cumulated vsize (Kb) 23640 [startup+390.035 s] Raw data (loadavg): 0.99 0.99 0.98 2/57 24590 Raw data (/proc/24586/stat): 24586 (minisat+_script) S 24585 24586 31915 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1788522941 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/24586/statm): 531 226 485 147 0 384 0 [pid=24586] vsize: 2124 Raw data (/proc/24590/stat): 24590 (minisat+_64-bit) R 24586 24586 31915 0 -1 0 5310 0 0 0 38918 36 0 0 25 0 1 0 1788522946 22032384 5216 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/24590/statm): 5379 5216 145 145 0 5234 0 [pid=24590] vsize: 21516 Current children cumulated CPU time (s) 389.54 Current children cumulated vsize (Kb) 23640 [startup+400.036 s] Raw data (loadavg): 0.99 0.99 0.98 2/57 24590 Raw data (/proc/24586/stat): 24586 (minisat+_script) S 24585 24586 31915 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1788522941 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/24586/statm): 531 226 485 147 0 384 0 [pid=24586] vsize: 2124 Raw data (/proc/24590/stat): 24590 (minisat+_64-bit) R 24586 24586 31915 0 -1 0 5310 0 0 0 39918 36 0 0 25 0 1 0 1788522946 22032384 5216 4294967295 134512640 135094434 3221224432 3221223056 134557627 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/24590/statm): 5379 5216 145 145 0 5234 0 [pid=24590] vsize: 21516 Current children cumulated CPU time (s) 399.54 Current children cumulated vsize (Kb) 23640 [startup+410.037 s] Raw data (loadavg): 0.99 0.99 0.98 2/57 24590 Raw data (/proc/24586/stat): 24586 (minisat+_script) S 24585 24586 31915 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1788522941 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/24586/statm): 531 226 485 147 0 384 0 [pid=24586] vsize: 2124 Raw data (/proc/24590/stat): 24590 (minisat+_64-bit) R 24586 24586 31915 0 -1 0 5310 0 0 0 40918 36 0 0 25 0 1 0 1788522946 22032384 5216 4294967295 134512640 135094434 3221224432 3221223024 134557336 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/24590/statm): 5379 5216 145 145 0 5234 0 [pid=24590] vsize: 21516 Current children cumulated CPU time (s) 409.54 Current children cumulated vsize (Kb) 23640 [startup+420.038 s] Raw data (loadavg): 0.99 0.99 0.98 2/57 24590 Raw data (/proc/24586/stat): 24586 (minisat+_script) S 24585 24586 31915 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1788522941 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/24586/statm): 531 226 485 147 0 384 0 [pid=24586] vsize: 2124 Raw data (/proc/24590/stat): 24590 (minisat+_64-bit) R 24586 24586 31915 0 -1 0 5310 0 0 0 41919 36 0 0 25 0 1 0 1788522946 22032384 5216 4294967295 134512640 135094434 3221224432 3221223088 134558159 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/24590/statm): 5379 5216 145 145 0 5234 0 [pid=24590] vsize: 21516 Current children cumulated CPU time (s) 419.55 Current children cumulated vsize (Kb) 23640 [startup+430.039 s] Raw data (loadavg): 0.99 0.99 0.98 2/57 24590 Raw data (/proc/24586/stat): 24586 (minisat+_script) S 24585 24586 31915 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1788522941 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/24586/statm): 531 226 485 147 0 384 0 [pid=24586] vsize: 2124 Raw data (/proc/24590/stat): 24590 (minisat+_64-bit) R 24586 24586 31915 0 -1 0 5310 0 0 0 42919 36 0 0 25 0 1 0 1788522946 22032384 5216 4294967295 134512640 135094434 3221224432 3221223024 134557404 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/24590/statm): 5379 5216 145 145 0 5234 0 [pid=24590] vsize: 21516 Current children cumulated CPU time (s) 429.55 Current children cumulated vsize (Kb) 23640 [startup+440.038 s] Raw data (loadavg): 0.99 0.99 0.98 2/57 24590 Raw data (/proc/24586/stat): 24586 (minisat+_script) S 24585 24586 31915 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1788522941 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/24586/statm): 531 226 485 147 0 384 0 [pid=24586] vsize: 2124 Raw data (/proc/24590/stat): 24590 (minisat+_64-bit) R 24586 24586 31915 0 -1 0 5311 0 0 0 43919 36 0 0 25 0 1 0 1788522946 22032384 5217 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/24590/statm): 5379 5217 145 145 0 5234 0 [pid=24590] vsize: 21516 Current children cumulated CPU time (s) 439.55 Current children cumulated vsize (Kb) 23640 [startup+450.039 s] Raw data (loadavg): 0.99 0.99 0.98 2/57 24590 Raw data (/proc/24586/stat): 24586 (minisat+_script) S 24585 24586 31915 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1788522941 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/24586/statm): 531 226 485 147 0 384 0 [pid=24586] vsize: 2124 Raw data (/proc/24590/stat): 24590 (minisat+_64-bit) R 24586 24586 31915 0 -1 0 5311 0 0 0 44919 36 0 0 25 0 1 0 1788522946 22032384 5217 4294967295 134512640 135094434 3221224432 3221223024 134556900 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/24590/statm): 5379 5217 145 145 0 5234 0 [pid=24590] vsize: 21516 Current children cumulated CPU time (s) 449.55 Current children cumulated vsize (Kb) 23640 [startup+460.04 s] Raw data (loadavg): 0.99 0.99 0.98 2/57 24590 Raw data (/proc/24586/stat): 24586 (minisat+_script) S 24585 24586 31915 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1788522941 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/24586/statm): 531 226 485 147 0 384 0 [pid=24586] vsize: 2124 Raw data (/proc/24590/stat): 24590 (minisat+_64-bit) R 24586 24586 31915 0 -1 0 5311 0 0 0 45919 36 0 0 25 0 1 0 1788522946 22032384 5217 4294967295 134512640 135094434 3221224432 3221222896 134780607 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/24590/statm): 5379 5217 145 145 0 5234 0 [pid=24590] vsize: 21516 Current children cumulated CPU time (s) 459.55 Current children cumulated vsize (Kb) 23640 [startup+470.041 s] Raw data (loadavg): 0.99 0.99 0.98 2/57 24590 Raw data (/proc/24586/stat): 24586 (minisat+_script) S 24585 24586 31915 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1788522941 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/24586/statm): 531 226 485 147 0 384 0 [pid=24586] vsize: 2124 Raw data (/proc/24590/stat): 24590 (minisat+_64-bit) R 24586 24586 31915 0 -1 0 5311 0 0 0 46919 37 0 0 25 0 1 0 1788522946 22032384 5217 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/24590/statm): 5379 5217 145 145 0 5234 0 [pid=24590] vsize: 21516 Current children cumulated CPU time (s) 469.56 Current children cumulated vsize (Kb) 23640 [startup+480.042 s] Raw data (loadavg): 0.99 0.99 0.98 2/57 24590 Raw data (/proc/24586/stat): 24586 (minisat+_script) S 24585 24586 31915 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1788522941 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/24586/statm): 531 226 485 147 0 384 0 [pid=24586] vsize: 2124 Raw data (/proc/24590/stat): 24590 (minisat+_64-bit) R 24586 24586 31915 0 -1 0 5311 0 0 0 47920 37 0 0 25 0 1 0 1788522946 22032384 5217 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/24590/statm): 5379 5217 145 145 0 5234 0 [pid=24590] vsize: 21516 Current children cumulated CPU time (s) 479.57 Current children cumulated vsize (Kb) 23640 [startup+490.043 s] Raw data (loadavg): 0.99 0.99 0.98 2/57 24590 Raw data (/proc/24586/stat): 24586 (minisat+_script) S 24585 24586 31915 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1788522941 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/24586/statm): 531 226 485 147 0 384 0 [pid=24586] vsize: 2124 Raw data (/proc/24590/stat): 24590 (minisat+_64-bit) R 24586 24586 31915 0 -1 0 5312 0 0 0 48920 37 0 0 25 0 1 0 1788522946 22032384 5218 4294967295 134512640 135094434 3221224432 3221223088 134557792 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/24590/statm): 5379 5218 145 145 0 5234 0 [pid=24590] vsize: 21516 Current children cumulated CPU time (s) 489.57 Current children cumulated vsize (Kb) 23640 [startup+500.044 s] Raw data (loadavg): 0.99 0.99 0.98 2/57 24590 Raw data (/proc/24586/stat): 24586 (minisat+_script) S 24585 24586 31915 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1788522941 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/24586/statm): 531 226 485 147 0 384 0 [pid=24586] vsize: 2124 Raw data (/proc/24590/stat): 24590 (minisat+_64-bit) R 24586 24586 31915 0 -1 0 5313 0 0 0 49920 37 0 0 25 0 1 0 1788522946 22032384 5219 4294967295 134512640 135094434 3221224432 3221223088 134558225 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/24590/statm): 5379 5219 145 145 0 5234 0 [pid=24590] vsize: 21516 Current children cumulated CPU time (s) 499.57 Current children cumulated vsize (Kb) 23640 [startup+510.044 s] Raw data (loadavg): 0.99 0.99 0.98 2/57 24590 Raw data (/proc/24586/stat): 24586 (minisat+_script) S 24585 24586 31915 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1788522941 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/24586/statm): 531 226 485 147 0 384 0 [pid=24586] vsize: 2124 Raw data (/proc/24590/stat): 24590 (minisat+_64-bit) R 24586 24586 31915 0 -1 0 5313 0 0 0 50920 37 0 0 25 0 1 0 1788522946 22032384 5219 4294967295 134512640 135094434 3221224432 3221223088 134558213 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/24590/statm): 5379 5219 145 145 0 5234 0 [pid=24590] vsize: 21516 Current children cumulated CPU time (s) 509.57 Current children cumulated vsize (Kb) 23640 [startup+520.045 s] Raw data (loadavg): 0.99 0.99 0.98 2/57 24590 Raw data (/proc/24586/stat): 24586 (minisat+_script) S 24585 24586 31915 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1788522941 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/24586/statm): 531 226 485 147 0 384 0 [pid=24586] vsize: 2124 Raw data (/proc/24590/stat): 24590 (minisat+_64-bit) R 24586 24586 31915 0 -1 0 5313 0 0 0 51920 37 0 0 25 0 1 0 1788522946 22032384 5219 4294967295 134512640 135094434 3221224432 3221223088 134557948 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/24590/statm): 5379 5219 145 145 0 5234 0 [pid=24590] vsize: 21516 Current children cumulated CPU time (s) 519.57 Current children cumulated vsize (Kb) 23640 [startup+530.047 s] Raw data (loadavg): 0.99 0.99 0.98 2/57 24590 Raw data (/proc/24586/stat): 24586 (minisat+_script) S 24585 24586 31915 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1788522941 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/24586/statm): 531 226 485 147 0 384 0 [pid=24586] vsize: 2124 Raw data (/proc/24590/stat): 24590 (minisat+_64-bit) R 24586 24586 31915 0 -1 0 5313 0 0 0 52921 37 0 0 25 0 1 0 1788522946 22032384 5219 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/24590/statm): 5379 5219 145 145 0 5234 0 [pid=24590] vsize: 21516 Current children cumulated CPU time (s) 529.58 Current children cumulated vsize (Kb) 23640 [startup+540.047 s] Raw data (loadavg): 0.99 0.99 0.98 2/57 24590 Raw data (/proc/24586/stat): 24586 (minisat+_script) S 24585 24586 31915 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1788522941 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/24586/statm): 531 226 485 147 0 384 0 [pid=24586] vsize: 2124 Raw data (/proc/24590/stat): 24590 (minisat+_64-bit) R 24586 24586 31915 0 -1 0 5313 0 0 0 53921 37 0 0 25 0 1 0 1788522946 22032384 5219 4294967295 134512640 135094434 3221224432 3221223088 134558009 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/24590/statm): 5379 5219 145 145 0 5234 0 [pid=24590] vsize: 21516 Current children cumulated CPU time (s) 539.58 Current children cumulated vsize (Kb) 23640 [startup+550.048 s] Raw data (loadavg): 0.99 0.99 0.98 2/57 24590 Raw data (/proc/24586/stat): 24586 (minisat+_script) S 24585 24586 31915 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1788522941 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/24586/statm): 531 226 485 147 0 384 0 [pid=24586] vsize: 2124 Raw data (/proc/24590/stat): 24590 (minisat+_64-bit) R 24586 24586 31915 0 -1 0 5313 0 0 0 54921 37 0 0 25 0 1 0 1788522946 22032384 5219 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/24590/statm): 5379 5219 145 145 0 5234 0 [pid=24590] vsize: 21516 Current children cumulated CPU time (s) 549.58 Current children cumulated vsize (Kb) 23640 [startup+560.049 s] Raw data (loadavg): 0.99 0.99 0.98 2/57 24590 Raw data (/proc/24586/stat): 24586 (minisat+_script) S 24585 24586 31915 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1788522941 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/24586/statm): 531 226 485 147 0 384 0 [pid=24586] vsize: 2124 Raw data (/proc/24590/stat): 24590 (minisat+_64-bit) R 24586 24586 31915 0 -1 0 5313 0 0 0 55921 37 0 0 25 0 1 0 1788522946 22032384 5219 4294967295 134512640 135094434 3221224432 3221223104 134555797 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/24590/statm): 5379 5219 145 145 0 5234 0 [pid=24590] vsize: 21516 Current children cumulated CPU time (s) 559.58 Current children cumulated vsize (Kb) 23640 [startup+570.049 s] Raw data (loadavg): 0.99 0.99 0.98 2/57 24590 Raw data (/proc/24586/stat): 24586 (minisat+_script) S 24585 24586 31915 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1788522941 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/24586/statm): 531 226 485 147 0 384 0 [pid=24586] vsize: 2124 Raw data (/proc/24590/stat): 24590 (minisat+_64-bit) R 24586 24586 31915 0 -1 0 5313 0 0 0 56922 37 0 0 25 0 1 0 1788522946 22032384 5219 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/24590/statm): 5379 5219 145 145 0 5234 0 [pid=24590] vsize: 21516 Current children cumulated CPU time (s) 569.59 Current children cumulated vsize (Kb) 23640 [startup+580.05 s] Raw data (loadavg): 0.99 0.99 0.98 2/57 24590 Raw data (/proc/24586/stat): 24586 (minisat+_script) S 24585 24586 31915 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1788522941 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/24586/statm): 531 226 485 147 0 384 0 [pid=24586] vsize: 2124 Raw data (/proc/24590/stat): 24590 (minisat+_64-bit) R 24586 24586 31915 0 -1 0 5313 0 0 0 57922 37 0 0 25 0 1 0 1788522946 22032384 5219 4294967295 134512640 135094434 3221224432 3221223088 134558402 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/24590/statm): 5379 5219 145 145 0 5234 0 [pid=24590] vsize: 21516 Current children cumulated CPU time (s) 579.59 Current children cumulated vsize (Kb) 23640 [startup+590.051 s] Raw data (loadavg): 0.99 0.99 0.98 2/57 24590 Raw data (/proc/24586/stat): 24586 (minisat+_script) S 24585 24586 31915 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1788522941 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/24586/statm): 531 226 485 147 0 384 0 [pid=24586] vsize: 2124 Raw data (/proc/24590/stat): 24590 (minisat+_64-bit) R 24586 24586 31915 0 -1 0 5313 0 0 0 58922 37 0 0 25 0 1 0 1788522946 22032384 5219 4294967295 134512640 135094434 3221224432 3221223088 134557884 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/24590/statm): 5379 5219 145 145 0 5234 0 [pid=24590] vsize: 21516 Current children cumulated CPU time (s) 589.59 Current children cumulated vsize (Kb) 23640 [startup+600.052 s] Raw data (loadavg): 0.99 0.99 0.98 2/57 24590 Raw data (/proc/24586/stat): 24586 (minisat+_script) S 24585 24586 31915 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1788522941 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/24586/statm): 531 226 485 147 0 384 0 [pid=24586] vsize: 2124 Raw data (/proc/24590/stat): 24590 (minisat+_64-bit) R 24586 24586 31915 0 -1 0 5334 0 0 0 59922 37 0 0 25 0 1 0 1788522946 22130688 5240 4294967295 134512640 135094434 3221224432 3221223088 134558213 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/24590/statm): 5403 5240 145 145 0 5258 0 [pid=24590] vsize: 21612 Current children cumulated CPU time (s) 599.59 Current children cumulated vsize (Kb) 23736 [startup+610.053 s] Raw data (loadavg): 0.99 0.99 0.98 2/57 24590 Raw data (/proc/24586/stat): 24586 (minisat+_script) S 24585 24586 31915 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1788522941 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/24586/statm): 531 226 485 147 0 384 0 [pid=24586] vsize: 2124 Raw data (/proc/24590/stat): 24590 (minisat+_64-bit) R 24586 24586 31915 0 -1 0 5346 0 0 0 60922 37 0 0 25 0 1 0 1788522946 22196224 5252 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/24590/statm): 5419 5252 145 145 0 5274 0 [pid=24590] vsize: 21676 Current children cumulated CPU time (s) 609.59 Current children cumulated vsize (Kb) 23800 [startup+620.054 s] Raw data (loadavg): 0.99 0.99 0.98 2/57 24590 Raw data (/proc/24586/stat): 24586 (minisat+_script) S 24585 24586 31915 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1788522941 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/24586/statm): 531 226 485 147 0 384 0 [pid=24586] vsize: 2124 Raw data (/proc/24590/stat): 24590 (minisat+_64-bit) R 24586 24586 31915 0 -1 0 5353 0 0 0 61922 37 0 0 25 0 1 0 1788522946 22228992 5259 4294967295 134512640 135094434 3221224432 3221223088 134557900 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/24590/statm): 5427 5259 145 145 0 5282 0 [pid=24590] vsize: 21708 Current children cumulated CPU time (s) 619.59 Current children cumulated vsize (Kb) 23832 [startup+630.054 s] Raw data (loadavg): 0.99 0.99 0.98 2/57 24590 Raw data (/proc/24586/stat): 24586 (minisat+_script) S 24585 24586 31915 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1788522941 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/24586/statm): 531 226 485 147 0 384 0 [pid=24586] vsize: 2124 Raw data (/proc/24590/stat): 24590 (minisat+_64-bit) R 24586 24586 31915 0 -1 0 5381 0 0 0 62923 37 0 0 25 0 1 0 1788522946 22392832 5287 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/24590/statm): 5467 5287 145 145 0 5322 0 [pid=24590] vsize: 21868 Current children cumulated CPU time (s) 629.6 Current children cumulated vsize (Kb) 23992 [startup+640.055 s] Raw data (loadavg): 0.99 0.99 0.98 2/57 24590 Raw data (/proc/24586/stat): 24586 (minisat+_script) S 24585 24586 31915 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1788522941 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/24586/statm): 531 226 485 147 0 384 0 [pid=24586] vsize: 2124 Raw data (/proc/24590/stat): 24590 (minisat+_64-bit) R 24586 24586 31915 0 -1 0 5391 0 0 0 63923 37 0 0 25 0 1 0 1788522946 22425600 5297 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/24590/statm): 5475 5297 145 145 0 5330 0 [pid=24590] vsize: 21900 Current children cumulated CPU time (s) 639.6 Current children cumulated vsize (Kb) 24024 [startup+650.056 s] Raw data (loadavg): 0.99 0.99 0.98 2/57 24590 Raw data (/proc/24586/stat): 24586 (minisat+_script) S 24585 24586 31915 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1788522941 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/24586/statm): 531 226 485 147 0 384 0 [pid=24586] vsize: 2124 Raw data (/proc/24590/stat): 24590 (minisat+_64-bit) R 24586 24586 31915 0 -1 0 5414 0 0 0 64923 37 0 0 25 0 1 0 1788522946 22589440 5320 4294967295 134512640 135094434 3221224432 3221223024 134557500 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/24590/statm): 5515 5320 145 145 0 5370 0 [pid=24590] vsize: 22060 Current children cumulated CPU time (s) 649.6 Current children cumulated vsize (Kb) 24184 [startup+660.056 s] Raw data (loadavg): 0.99 0.99 0.98 2/57 24590 Raw data (/proc/24586/stat): 24586 (minisat+_script) S 24585 24586 31915 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1788522941 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/24586/statm): 531 226 485 147 0 384 0 [pid=24586] vsize: 2124 Raw data (/proc/24590/stat): 24590 (minisat+_64-bit) R 24586 24586 31915 0 -1 0 5414 0 0 0 65923 37 0 0 25 0 1 0 1788522946 22589440 5320 4294967295 134512640 135094434 3221224432 3221223104 134555585 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/24590/statm): 5515 5320 145 145 0 5370 0 [pid=24590] vsize: 22060 Current children cumulated CPU time (s) 659.6 Current children cumulated vsize (Kb) 24184 [startup+670.058 s] Raw data (loadavg): 0.99 0.99 0.98 2/57 24590 Raw data (/proc/24586/stat): 24586 (minisat+_script) S 24585 24586 31915 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1788522941 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/24586/statm): 531 226 485 147 0 384 0 [pid=24586] vsize: 2124 Raw data (/proc/24590/stat): 24590 (minisat+_64-bit) R 24586 24586 31915 0 -1 0 5414 0 0 0 66924 37 0 0 25 0 1 0 1788522946 22589440 5320 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/24590/statm): 5515 5320 145 145 0 5370 0 [pid=24590] vsize: 22060 Current children cumulated CPU time (s) 669.61 Current children cumulated vsize (Kb) 24184 [startup+680.059 s] Raw data (loadavg): 0.99 0.99 0.98 2/57 24590 Raw data (/proc/24586/stat): 24586 (minisat+_script) S 24585 24586 31915 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1788522941 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/24586/statm): 531 226 485 147 0 384 0 [pid=24586] vsize: 2124 Raw data (/proc/24590/stat): 24590 (minisat+_64-bit) R 24586 24586 31915 0 -1 0 5414 0 0 0 67924 37 0 0 25 0 1 0 1788522946 22589440 5320 4294967295 134512640 135094434 3221224432 3221223024 134557357 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/24590/statm): 5515 5320 145 145 0 5370 0 [pid=24590] vsize: 22060 Current children cumulated CPU time (s) 679.61 Current children cumulated vsize (Kb) 24184 [startup+690.058 s] Raw data (loadavg): 0.99 0.99 0.98 2/57 24590 Raw data (/proc/24586/stat): 24586 (minisat+_script) S 24585 24586 31915 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1788522941 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/24586/statm): 531 226 485 147 0 384 0 [pid=24586] vsize: 2124 Raw data (/proc/24590/stat): 24590 (minisat+_64-bit) R 24586 24586 31915 0 -1 0 5414 0 0 0 68924 37 0 0 25 0 1 0 1788522946 22589440 5320 4294967295 134512640 135094434 3221224432 3221223120 134554746 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/24590/statm): 5515 5320 145 145 0 5370 0 [pid=24590] vsize: 22060 Current children cumulated CPU time (s) 689.61 Current children cumulated vsize (Kb) 24184 [startup+700.06 s] Raw data (loadavg): 0.99 0.99 0.98 2/57 24590 Raw data (/proc/24586/stat): 24586 (minisat+_script) S 24585 24586 31915 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1788522941 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/24586/statm): 531 226 485 147 0 384 0 [pid=24586] vsize: 2124 Raw data (/proc/24590/stat): 24590 (minisat+_64-bit) R 24586 24586 31915 0 -1 0 5419 0 0 0 69924 37 0 0 25 0 1 0 1788522946 22589440 5325 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/24590/statm): 5515 5325 145 145 0 5370 0 [pid=24590] vsize: 22060 Current children cumulated CPU time (s) 699.61 Current children cumulated vsize (Kb) 24184 [startup+710.061 s] Raw data (loadavg): 0.99 0.99 0.98 2/57 24590 Raw data (/proc/24586/stat): 24586 (minisat+_script) S 24585 24586 31915 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1788522941 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/24586/statm): 531 226 485 147 0 384 0 [pid=24586] vsize: 2124 Raw data (/proc/24590/stat): 24590 (minisat+_64-bit) R 24586 24586 31915 0 -1 0 5419 0 0 0 70925 37 0 0 25 0 1 0 1788522946 22589440 5325 4294967295 134512640 135094434 3221224432 3221223104 134555940 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/24590/statm): 5515 5325 145 145 0 5370 0 [pid=24590] vsize: 22060 Current children cumulated CPU time (s) 709.62 Current children cumulated vsize (Kb) 24184 [startup+720.062 s] Raw data (loadavg): 0.99 0.99 0.98 2/57 24590 Raw data (/proc/24586/stat): 24586 (minisat+_script) S 24585 24586 31915 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1788522941 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/24586/statm): 531 226 485 147 0 384 0 [pid=24586] vsize: 2124 Raw data (/proc/24590/stat): 24590 (minisat+_64-bit) R 24586 24586 31915 0 -1 0 5419 0 0 0 71924 37 0 0 25 0 1 0 1788522946 22589440 5325 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/24590/statm): 5515 5325 145 145 0 5370 0 [pid=24590] vsize: 22060 Current children cumulated CPU time (s) 719.61 Current children cumulated vsize (Kb) 24184 [startup+730.063 s] Raw data (loadavg): 0.99 0.99 0.98 2/57 24590 Raw data (/proc/24586/stat): 24586 (minisat+_script) S 24585 24586 31915 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1788522941 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/24586/statm): 531 226 485 147 0 384 0 [pid=24586] vsize: 2124 Raw data (/proc/24590/stat): 24590 (minisat+_64-bit) R 24586 24586 31915 0 -1 0 5419 0 0 0 72925 37 0 0 25 0 1 0 1788522946 22589440 5325 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/24590/statm): 5515 5325 145 145 0 5370 0 [pid=24590] vsize: 22060 Current children cumulated CPU time (s) 729.62 Current children cumulated vsize (Kb) 24184 [startup+740.063 s] Raw data (loadavg): 0.99 0.99 0.98 2/57 24590 Raw data (/proc/24586/stat): 24586 (minisat+_script) S 24585 24586 31915 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1788522941 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/24586/statm): 531 226 485 147 0 384 0 [pid=24586] vsize: 2124 Raw data (/proc/24590/stat): 24590 (minisat+_64-bit) R 24586 24586 31915 0 -1 0 5419 0 0 0 73925 37 0 0 25 0 1 0 1788522946 22589440 5325 4294967295 134512640 135094434 3221224432 3221223088 134558178 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/24590/statm): 5515 5325 145 145 0 5370 0 [pid=24590] vsize: 22060 Current children cumulated CPU time (s) 739.62 Current children cumulated vsize (Kb) 24184 [startup+750.064 s] Raw data (loadavg): 0.99 0.99 0.98 2/57 24590 Raw data (/proc/24586/stat): 24586 (minisat+_script) S 24585 24586 31915 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1788522941 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/24586/statm): 531 226 485 147 0 384 0 [pid=24586] vsize: 2124 Raw data (/proc/24590/stat): 24590 (minisat+_64-bit) R 24586 24586 31915 0 -1 0 5432 0 0 0 74925 37 0 0 25 0 1 0 1788522946 22654976 5338 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/24590/statm): 5531 5338 145 145 0 5386 0 [pid=24590] vsize: 22124 Current children cumulated CPU time (s) 749.62 Current children cumulated vsize (Kb) 24248 [startup+760.064 s] Raw data (loadavg): 0.99 0.99 0.98 2/57 24590 Raw data (/proc/24586/stat): 24586 (minisat+_script) S 24585 24586 31915 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1788522941 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/24586/statm): 531 226 485 147 0 384 0 [pid=24586] vsize: 2124 Raw data (/proc/24590/stat): 24590 (minisat+_64-bit) R 24586 24586 31915 0 -1 0 5444 0 0 0 75925 37 0 0 25 0 1 0 1788522946 22720512 5350 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/24590/statm): 5547 5350 145 145 0 5402 0 [pid=24590] vsize: 22188 Current children cumulated CPU time (s) 759.62 Current children cumulated vsize (Kb) 24312 [startup+770.066 s] Raw data (loadavg): 0.99 0.99 0.98 2/57 24590 Raw data (/proc/24586/stat): 24586 (minisat+_script) S 24585 24586 31915 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1788522941 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/24586/statm): 531 226 485 147 0 384 0 [pid=24586] vsize: 2124 Raw data (/proc/24590/stat): 24590 (minisat+_64-bit) R 24586 24586 31915 0 -1 0 5468 0 0 0 76925 37 0 0 25 0 1 0 1788522946 22851584 5374 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/24590/statm): 5579 5374 145 145 0 5434 0 [pid=24590] vsize: 22316 Current children cumulated CPU time (s) 769.62 Current children cumulated vsize (Kb) 24440 [startup+780.067 s] Raw data (loadavg): 0.99 0.99 0.98 2/57 24590 Raw data (/proc/24586/stat): 24586 (minisat+_script) S 24585 24586 31915 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1788522941 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/24586/statm): 531 226 485 147 0 384 0 [pid=24586] vsize: 2124 Raw data (/proc/24590/stat): 24590 (minisat+_64-bit) R 24586 24586 31915 0 -1 0 5479 0 0 0 77925 38 0 0 25 0 1 0 1788522946 22917120 5385 4294967295 134512640 135094434 3221224432 3221223024 134557219 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/24590/statm): 5595 5385 145 145 0 5450 0 [pid=24590] vsize: 22380 Current children cumulated CPU time (s) 779.63 Current children cumulated vsize (Kb) 24504 [startup+790.068 s] Raw data (loadavg): 0.99 0.99 0.98 2/57 24590 Raw data (/proc/24586/stat): 24586 (minisat+_script) S 24585 24586 31915 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1788522941 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/24586/statm): 531 226 485 147 0 384 0 [pid=24586] vsize: 2124 Raw data (/proc/24590/stat): 24590 (minisat+_64-bit) R 24586 24586 31915 0 -1 0 5485 0 0 0 78926 38 0 0 25 0 1 0 1788522946 22949888 5391 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/24590/statm): 5603 5391 145 145 0 5458 0 [pid=24590] vsize: 22412 Current children cumulated CPU time (s) 789.64 Current children cumulated vsize (Kb) 24536 [startup+800.069 s] Raw data (loadavg): 0.99 0.99 0.98 2/57 24590 Raw data (/proc/24586/stat): 24586 (minisat+_script) S 24585 24586 31915 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1788522941 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/24586/statm): 531 226 485 147 0 384 0 [pid=24586] vsize: 2124 Raw data (/proc/24590/stat): 24590 (minisat+_64-bit) R 24586 24586 31915 0 -1 0 5489 0 0 0 79926 38 0 0 25 0 1 0 1788522946 23015424 5395 4294967295 134512640 135094434 3221224432 3221223024 134557389 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/24590/statm): 5619 5395 145 145 0 5474 0 [pid=24590] vsize: 22476 Current children cumulated CPU time (s) 799.64 Current children cumulated vsize (Kb) 24600 [startup+810.069 s] Raw data (loadavg): 0.99 0.99 0.98 2/57 24590 Raw data (/proc/24586/stat): 24586 (minisat+_script) S 24585 24586 31915 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1788522941 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/24586/statm): 531 226 485 147 0 384 0 [pid=24586] vsize: 2124 Raw data (/proc/24590/stat): 24590 (minisat+_64-bit) R 24586 24586 31915 0 -1 0 5494 0 0 0 80926 38 0 0 25 0 1 0 1788522946 23015424 5400 4294967295 134512640 135094434 3221224432 3221223088 134558208 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/24590/statm): 5619 5400 145 145 0 5474 0 [pid=24590] vsize: 22476 Current children cumulated CPU time (s) 809.64 Current children cumulated vsize (Kb) 24600 [startup+820.069 s] Raw data (loadavg): 0.99 0.99 0.98 2/57 24590 Raw data (/proc/24586/stat): 24586 (minisat+_script) S 24585 24586 31915 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1788522941 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/24586/statm): 531 226 485 147 0 384 0 [pid=24586] vsize: 2124 Raw data (/proc/24590/stat): 24590 (minisat+_64-bit) R 24586 24586 31915 0 -1 0 5495 0 0 0 81926 38 0 0 25 0 1 0 1788522946 23015424 5401 4294967295 134512640 135094434 3221224432 3221223088 134558022 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/24590/statm): 5619 5401 145 145 0 5474 0 [pid=24590] vsize: 22476 Current children cumulated CPU time (s) 819.64 Current children cumulated vsize (Kb) 24600 [startup+830.07 s] Raw data (loadavg): 0.99 0.99 0.98 2/57 24590 Raw data (/proc/24586/stat): 24586 (minisat+_script) S 24585 24586 31915 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1788522941 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/24586/statm): 531 226 485 147 0 384 0 [pid=24586] vsize: 2124 Raw data (/proc/24590/stat): 24590 (minisat+_64-bit) R 24586 24586 31915 0 -1 0 5524 0 0 0 82926 38 0 0 25 0 1 0 1788522946 23130112 5430 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/24590/statm): 5647 5430 145 145 0 5502 0 [pid=24590] vsize: 22588 Current children cumulated CPU time (s) 829.64 Current children cumulated vsize (Kb) 24712 [startup+840.07 s] Raw data (loadavg): 0.99 0.99 0.98 2/57 24590 Raw data (/proc/24586/stat): 24586 (minisat+_script) S 24585 24586 31915 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1788522941 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/24586/statm): 531 226 485 147 0 384 0 [pid=24586] vsize: 2124 Raw data (/proc/24590/stat): 24590 (minisat+_64-bit) R 24586 24586 31915 0 -1 0 5524 0 0 0 83926 38 0 0 25 0 1 0 1788522946 23130112 5430 4294967295 134512640 135094434 3221224432 3221223088 134557988 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/24590/statm): 5647 5430 145 145 0 5502 0 [pid=24590] vsize: 22588 Current children cumulated CPU time (s) 839.64 Current children cumulated vsize (Kb) 24712 [startup+850.071 s] Raw data (loadavg): 0.99 0.99 0.98 2/57 24590 Raw data (/proc/24586/stat): 24586 (minisat+_script) S 24585 24586 31915 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1788522941 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/24586/statm): 531 226 485 147 0 384 0 [pid=24586] vsize: 2124 Raw data (/proc/24590/stat): 24590 (minisat+_64-bit) R 24586 24586 31915 0 -1 0 5527 0 0 0 84926 38 0 0 25 0 1 0 1788522946 23146496 5433 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/24590/statm): 5651 5433 145 145 0 5506 0 [pid=24590] vsize: 22604 Current children cumulated CPU time (s) 849.64 Current children cumulated vsize (Kb) 24728 [startup+860.072 s] Raw data (loadavg): 0.99 0.99 0.98 2/57 24590 Raw data (/proc/24586/stat): 24586 (minisat+_script) S 24585 24586 31915 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1788522941 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/24586/statm): 531 226 485 147 0 384 0 [pid=24586] vsize: 2124 Raw data (/proc/24590/stat): 24590 (minisat+_64-bit) R 24586 24586 31915 0 -1 0 5540 0 0 0 85924 39 0 0 25 0 1 0 1788522946 23212032 5446 4294967295 134512640 135094434 3221224432 3221223088 134558178 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/24590/statm): 5667 5446 145 145 0 5522 0 [pid=24590] vsize: 22668 Current children cumulated CPU time (s) 859.63 Current children cumulated vsize (Kb) 24792 [startup+870.074 s] Raw data (loadavg): 0.99 0.99 0.98 2/57 24590 Raw data (/proc/24586/stat): 24586 (minisat+_script) S 24585 24586 31915 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1788522941 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/24586/statm): 531 226 485 147 0 384 0 [pid=24586] vsize: 2124 Raw data (/proc/24590/stat): 24590 (minisat+_64-bit) R 24586 24586 31915 0 -1 0 5559 0 0 0 86924 39 0 0 25 0 1 0 1788522946 23306240 5465 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/24590/statm): 5690 5465 145 145 0 5545 0 [pid=24590] vsize: 22760 Current children cumulated CPU time (s) 869.63 Current children cumulated vsize (Kb) 24884 [startup+880.074 s] Raw data (loadavg): 0.99 0.99 0.98 2/57 24590 Raw data (/proc/24586/stat): 24586 (minisat+_script) S 24585 24586 31915 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1788522941 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/24586/statm): 531 226 485 147 0 384 0 [pid=24586] vsize: 2124 Raw data (/proc/24590/stat): 24590 (minisat+_64-bit) R 24586 24586 31915 0 -1 0 5738 0 0 0 87922 40 0 0 25 0 1 0 1788522946 24051712 5644 4294967295 134512640 135094434 3221224432 3221223088 134558208 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/24590/statm): 5872 5644 145 145 0 5727 0 [pid=24590] vsize: 23488 Current children cumulated CPU time (s) 879.62 Current children cumulated vsize (Kb) 25612 [startup+890.075 s] Raw data (loadavg): 0.99 0.99 0.98 2/57 24590 Raw data (/proc/24586/stat): 24586 (minisat+_script) S 24585 24586 31915 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1788522941 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/24586/statm): 531 226 485 147 0 384 0 [pid=24586] vsize: 2124 Raw data (/proc/24590/stat): 24590 (minisat+_64-bit) R 24586 24586 31915 0 -1 0 5916 0 0 0 88919 41 0 0 25 0 1 0 1788522946 24813568 5822 4294967295 134512640 135094434 3221224432 3221223024 134557230 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/24590/statm): 6058 5822 145 145 0 5913 0 [pid=24590] vsize: 24232 Current children cumulated CPU time (s) 889.6 Current children cumulated vsize (Kb) 26356 [startup+900.076 s] Raw data (loadavg): 0.99 0.99 0.98 2/57 24590 Raw data (/proc/24586/stat): 24586 (minisat+_script) S 24585 24586 31915 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1788522941 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/24586/statm): 531 226 485 147 0 384 0 [pid=24586] vsize: 2124 Raw data (/proc/24590/stat): 24590 (minisat+_64-bit) R 24586 24586 31915 0 -1 0 6085 0 0 0 89917 42 0 0 25 0 1 0 1788522946 25513984 5991 4294967295 134512640 135094434 3221224432 3221223104 134556244 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/24590/statm): 6229 5991 145 145 0 6084 0 [pid=24590] vsize: 24916 Current children cumulated CPU time (s) 899.59 Current children cumulated vsize (Kb) 27040 [startup+910.077 s] Raw data (loadavg): 0.99 0.99 0.98 2/57 24590 Raw data (/proc/24586/stat): 24586 (minisat+_script) S 24585 24586 31915 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1788522941 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/24586/statm): 531 226 485 147 0 384 0 [pid=24586] vsize: 2124 Raw data (/proc/24590/stat): 24590 (minisat+_64-bit) R 24586 24586 31915 0 -1 0 6268 0 0 0 90914 43 0 0 25 0 1 0 1788522946 26284032 6174 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/24590/statm): 6417 6174 145 145 0 6272 0 [pid=24590] vsize: 25668 Current children cumulated CPU time (s) 909.57 Current children cumulated vsize (Kb) 27792 [startup+920.078 s] Raw data (loadavg): 0.99 0.99 0.98 2/57 24590 Raw data (/proc/24586/stat): 24586 (minisat+_script) S 24585 24586 31915 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1788522941 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/24586/statm): 531 226 485 147 0 384 0 [pid=24586] vsize: 2124 Raw data (/proc/24590/stat): 24590 (minisat+_64-bit) R 24586 24586 31915 0 -1 0 6268 0 0 0 91915 43 0 0 25 0 1 0 1788522946 26284032 6174 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/24590/statm): 6417 6174 145 145 0 6272 0 [pid=24590] vsize: 25668 Current children cumulated CPU time (s) 919.58 Current children cumulated vsize (Kb) 27792 [startup+930.079 s] Raw data (loadavg): 0.99 0.99 0.98 2/57 24590 Raw data (/proc/24586/stat): 24586 (minisat+_script) S 24585 24586 31915 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1788522941 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/24586/statm): 531 226 485 147 0 384 0 [pid=24586] vsize: 2124 Raw data (/proc/24590/stat): 24590 (minisat+_64-bit) R 24586 24586 31915 0 -1 0 6268 0 0 0 92915 43 0 0 25 0 1 0 1788522946 26284032 6174 4294967295 134512640 135094434 3221224432 3221223088 134558398 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/24590/statm): 6417 6174 145 145 0 6272 0 [pid=24590] vsize: 25668 Current children cumulated CPU time (s) 929.58 Current children cumulated vsize (Kb) 27792 [startup+940.08 s] Raw data (loadavg): 0.99 0.99 0.98 2/57 24590 Raw data (/proc/24586/stat): 24586 (minisat+_script) S 24585 24586 31915 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1788522941 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/24586/statm): 531 226 485 147 0 384 0 [pid=24586] vsize: 2124 Raw data (/proc/24590/stat): 24590 (minisat+_64-bit) R 24586 24586 31915 0 -1 0 6275 0 0 0 93915 43 0 0 25 0 1 0 1788522946 26316800 6181 4294967295 134512640 135094434 3221224432 3221223024 134557500 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/24590/statm): 6425 6181 145 145 0 6280 0 [pid=24590] vsize: 25700 Current children cumulated CPU time (s) 939.58 Current children cumulated vsize (Kb) 27824 [startup+950.08 s] Raw data (loadavg): 0.99 0.99 0.98 2/57 24590 Raw data (/proc/24586/stat): 24586 (minisat+_script) S 24585 24586 31915 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1788522941 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/24586/statm): 531 226 485 147 0 384 0 [pid=24586] vsize: 2124 Raw data (/proc/24590/stat): 24590 (minisat+_64-bit) R 24586 24586 31915 0 -1 0 6298 0 0 0 94915 44 0 0 25 0 1 0 1788522946 26447872 6204 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/24590/statm): 6457 6204 145 145 0 6312 0 [pid=24590] vsize: 25828 Current children cumulated CPU time (s) 949.59 Current children cumulated vsize (Kb) 27952 [startup+960.081 s] Raw data (loadavg): 0.99 0.99 0.98 2/57 24590 Raw data (/proc/24586/stat): 24586 (minisat+_script) S 24585 24586 31915 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1788522941 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/24586/statm): 531 226 485 147 0 384 0 [pid=24586] vsize: 2124 Raw data (/proc/24590/stat): 24590 (minisat+_64-bit) R 24586 24586 31915 0 -1 0 6310 0 0 0 95919 44 0 0 25 0 1 0 1788522946 26546176 6216 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/24590/statm): 6481 6216 145 145 0 6336 0 [pid=24590] vsize: 25924 Current children cumulated CPU time (s) 959.63 Current children cumulated vsize (Kb) 28048 [startup+970.12 s] Raw data (loadavg): 0.99 0.99 0.98 2/57 24590 Raw data (/proc/24586/stat): 24586 (minisat+_script) S 24585 24586 31915 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1788522941 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/24586/statm): 531 226 485 147 0 384 0 [pid=24586] vsize: 2124 Raw data (/proc/24590/stat): 24590 (minisat+_64-bit) R 24586 24586 31915 0 -1 0 6329 0 0 0 96919 44 0 0 25 0 1 0 1788522946 26611712 6235 4294967295 134512640 135094434 3221224432 3221223088 134558395 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/24590/statm): 6497 6235 145 145 0 6352 0 [pid=24590] vsize: 25988 Current children cumulated CPU time (s) 969.63 Current children cumulated vsize (Kb) 28112 [startup+980.121 s] Raw data (loadavg): 0.99 0.99 0.98 2/57 24590 Raw data (/proc/24586/stat): 24586 (minisat+_script) S 24585 24586 31915 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1788522941 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/24586/statm): 531 226 485 147 0 384 0 [pid=24586] vsize: 2124 Raw data (/proc/24590/stat): 24590 (minisat+_64-bit) R 24586 24586 31915 0 -1 0 6350 0 0 0 97919 44 0 0 25 0 1 0 1788522946 26742784 6256 4294967295 134512640 135094434 3221224432 3221223088 134558249 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/24590/statm): 6529 6256 145 145 0 6384 0 [pid=24590] vsize: 26116 Current children cumulated CPU time (s) 979.63 Current children cumulated vsize (Kb) 28240 [startup+990.121 s] Raw data (loadavg): 0.99 0.99 0.98 2/57 24590 Raw data (/proc/24586/stat): 24586 (minisat+_script) S 24585 24586 31915 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1788522941 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/24586/statm): 531 226 485 147 0 384 0 [pid=24586] vsize: 2124 Raw data (/proc/24590/stat): 24590 (minisat+_64-bit) R 24586 24586 31915 0 -1 0 6380 0 0 0 98919 44 0 0 25 0 1 0 1788522946 26939392 6286 4294967295 134512640 135094434 3221224432 3221223024 134557180 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/24590/statm): 6577 6286 145 145 0 6432 0 [pid=24590] vsize: 26308 Current children cumulated CPU time (s) 989.63 Current children cumulated vsize (Kb) 28432 [startup+1000.12 s] Raw data (loadavg): 0.99 0.99 0.98 2/57 24590 Raw data (/proc/24586/stat): 24586 (minisat+_script) S 24585 24586 31915 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1788522941 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/24586/statm): 531 226 485 147 0 384 0 [pid=24586] vsize: 2124 Raw data (/proc/24590/stat): 24590 (minisat+_64-bit) R 24586 24586 31915 0 -1 0 6380 0 0 0 99920 44 0 0 25 0 1 0 1788522946 26939392 6286 4294967295 134512640 135094434 3221224432 3221223104 134556242 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/24590/statm): 6577 6286 145 145 0 6432 0 [pid=24590] vsize: 26308 Current children cumulated CPU time (s) 999.64 Current children cumulated vsize (Kb) 28432 [startup+1010.12 s] Raw data (loadavg): 0.99 0.99 0.98 2/57 24590 Raw data (/proc/24586/stat): 24586 (minisat+_script) S 24585 24586 31915 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1788522941 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/24586/statm): 531 226 485 147 0 384 0 [pid=24586] vsize: 2124 Raw data (/proc/24590/stat): 24590 (minisat+_64-bit) R 24586 24586 31915 0 -1 0 6380 0 0 0 100920 44 0 0 25 0 1 0 1788522946 26939392 6286 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/24590/statm): 6577 6286 145 145 0 6432 0 [pid=24590] vsize: 26308 Current children cumulated CPU time (s) 1009.64 Current children cumulated vsize (Kb) 28432 [startup+1020.12 s] Raw data (loadavg): 0.99 0.99 0.98 2/57 24590 Raw data (/proc/24586/stat): 24586 (minisat+_script) S 24585 24586 31915 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1788522941 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/24586/statm): 531 226 485 147 0 384 0 [pid=24586] vsize: 2124 Raw data (/proc/24590/stat): 24590 (minisat+_64-bit) R 24586 24586 31915 0 -1 0 6380 0 0 0 101920 44 0 0 25 0 1 0 1788522946 26939392 6286 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/24590/statm): 6577 6286 145 145 0 6432 0 [pid=24590] vsize: 26308 Current children cumulated CPU time (s) 1019.64 Current children cumulated vsize (Kb) 28432 [startup+1030.13 s] Raw data (loadavg): 0.99 0.99 0.98 2/57 24590 Raw data (/proc/24586/stat): 24586 (minisat+_script) S 24585 24586 31915 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1788522941 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/24586/statm): 531 226 485 147 0 384 0 [pid=24586] vsize: 2124 Raw data (/proc/24590/stat): 24590 (minisat+_64-bit) R 24586 24586 31915 0 -1 0 6380 0 0 0 102920 44 0 0 25 0 1 0 1788522946 26939392 6286 4294967295 134512640 135094434 3221224432 3221223088 134558208 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/24590/statm): 6577 6286 145 145 0 6432 0 [pid=24590] vsize: 26308 Current children cumulated CPU time (s) 1029.64 Current children cumulated vsize (Kb) 28432 [startup+1040.12 s] Raw data (loadavg): 0.99 0.99 0.98 2/57 24590 Raw data (/proc/24586/stat): 24586 (minisat+_script) S 24585 24586 31915 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1788522941 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/24586/statm): 531 226 485 147 0 384 0 [pid=24586] vsize: 2124 Raw data (/proc/24590/stat): 24590 (minisat+_64-bit) R 24586 24586 31915 0 -1 0 6380 0 0 0 103920 44 0 0 25 0 1 0 1788522946 26939392 6286 4294967295 134512640 135094434 3221224432 3221223088 134558019 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/24590/statm): 6577 6286 145 145 0 6432 0 [pid=24590] vsize: 26308 Current children cumulated CPU time (s) 1039.64 Current children cumulated vsize (Kb) 28432 [startup+1050.13 s] Raw data (loadavg): 0.99 0.99 0.98 2/57 24590 Raw data (/proc/24586/stat): 24586 (minisat+_script) S 24585 24586 31915 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1788522941 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/24586/statm): 531 226 485 147 0 384 0 [pid=24586] vsize: 2124 Raw data (/proc/24590/stat): 24590 (minisat+_64-bit) R 24586 24586 31915 0 -1 0 6381 0 0 0 104926 44 0 0 25 0 1 0 1788522946 26939392 6287 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/24590/statm): 6577 6287 145 145 0 6432 0 [pid=24590] vsize: 26308 Current children cumulated CPU time (s) 1049.7 Current children cumulated vsize (Kb) 28432 [startup+1060.18 s] Raw data (loadavg): 0.99 0.99 0.98 2/57 24590 Raw data (/proc/24586/stat): 24586 (minisat+_script) S 24585 24586 31915 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1788522941 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/24586/statm): 531 226 485 147 0 384 0 [pid=24586] vsize: 2124 Raw data (/proc/24590/stat): 24590 (minisat+_64-bit) R 24586 24586 31915 0 -1 0 6381 0 0 0 105926 44 0 0 25 0 1 0 1788522946 26939392 6287 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/24590/statm): 6577 6287 145 145 0 6432 0 [pid=24590] vsize: 26308 Current children cumulated CPU time (s) 1059.7 Current children cumulated vsize (Kb) 28432 [startup+1070.18 s] Raw data (loadavg): 0.99 0.99 0.98 2/57 24590 Raw data (/proc/24586/stat): 24586 (minisat+_script) S 24585 24586 31915 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1788522941 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/24586/statm): 531 226 485 147 0 384 0 [pid=24586] vsize: 2124 Raw data (/proc/24590/stat): 24590 (minisat+_64-bit) R 24586 24586 31915 0 -1 0 6381 0 0 0 106927 44 0 0 25 0 1 0 1788522946 26939392 6287 4294967295 134512640 135094434 3221224432 3221223104 134556244 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/24590/statm): 6577 6287 145 145 0 6432 0 [pid=24590] vsize: 26308 Current children cumulated CPU time (s) 1069.71 Current children cumulated vsize (Kb) 28432 [startup+1080.19 s] Raw data (loadavg): 0.99 0.99 0.98 2/57 24590 Raw data (/proc/24586/stat): 24586 (minisat+_script) S 24585 24586 31915 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1788522941 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/24586/statm): 531 226 485 147 0 384 0 [pid=24586] vsize: 2124 Raw data (/proc/24590/stat): 24590 (minisat+_64-bit) R 24586 24586 31915 0 -1 0 6381 0 0 0 107927 44 0 0 25 0 1 0 1788522946 26939392 6287 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/24590/statm): 6577 6287 145 145 0 6432 0 [pid=24590] vsize: 26308 Current children cumulated CPU time (s) 1079.71 Current children cumulated vsize (Kb) 28432 [startup+1090.19 s] Raw data (loadavg): 0.99 0.99 0.98 2/57 24590 Raw data (/proc/24586/stat): 24586 (minisat+_script) S 24585 24586 31915 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1788522941 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/24586/statm): 531 226 485 147 0 384 0 [pid=24586] vsize: 2124 Raw data (/proc/24590/stat): 24590 (minisat+_64-bit) R 24586 24586 31915 0 -1 0 6382 0 0 0 108927 44 0 0 25 0 1 0 1788522946 26939392 6288 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/24590/statm): 6577 6288 145 145 0 6432 0 [pid=24590] vsize: 26308 Current children cumulated CPU time (s) 1089.71 Current children cumulated vsize (Kb) 28432 [startup+1100.19 s] Raw data (loadavg): 0.99 0.99 0.98 2/57 24590 Raw data (/proc/24586/stat): 24586 (minisat+_script) S 24585 24586 31915 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1788522941 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/24586/statm): 531 226 485 147 0 384 0 [pid=24586] vsize: 2124 Raw data (/proc/24590/stat): 24590 (minisat+_64-bit) R 24586 24586 31915 0 -1 0 6382 0 0 0 109927 44 0 0 25 0 1 0 1788522946 26939392 6288 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/24590/statm): 6577 6288 145 145 0 6432 0 [pid=24590] vsize: 26308 Current children cumulated CPU time (s) 1099.71 Current children cumulated vsize (Kb) 28432 [startup+1110.19 s] Raw data (loadavg): 0.99 0.99 0.98 2/57 24590 Raw data (/proc/24586/stat): 24586 (minisat+_script) S 24585 24586 31915 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1788522941 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/24586/statm): 531 226 485 147 0 384 0 [pid=24586] vsize: 2124 Raw data (/proc/24590/stat): 24590 (minisat+_64-bit) R 24586 24586 31915 0 -1 0 6382 0 0 0 110927 44 0 0 25 0 1 0 1788522946 26939392 6288 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/24590/statm): 6577 6288 145 145 0 6432 0 [pid=24590] vsize: 26308 Current children cumulated CPU time (s) 1109.71 Current children cumulated vsize (Kb) 28432 [startup+1120.19 s] Raw data (loadavg): 0.99 0.99 0.98 2/57 24590 Raw data (/proc/24586/stat): 24586 (minisat+_script) S 24585 24586 31915 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1788522941 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/24586/statm): 531 226 485 147 0 384 0 [pid=24586] vsize: 2124 Raw data (/proc/24590/stat): 24590 (minisat+_64-bit) R 24586 24586 31915 0 -1 0 6388 0 0 0 111927 44 0 0 25 0 1 0 1788522946 26968064 6294 4294967295 134512640 135094434 3221224432 3221223088 134558016 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/24590/statm): 6584 6294 145 145 0 6439 0 [pid=24590] vsize: 26336 Current children cumulated CPU time (s) 1119.71 Current children cumulated vsize (Kb) 28460 [startup+1130.19 s] Raw data (loadavg): 0.99 0.99 0.98 2/57 24590 Raw data (/proc/24586/stat): 24586 (minisat+_script) S 24585 24586 31915 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1788522941 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/24586/statm): 531 226 485 147 0 384 0 [pid=24586] vsize: 2124 Raw data (/proc/24590/stat): 24590 (minisat+_64-bit) R 24586 24586 31915 0 -1 0 6398 0 0 0 112927 44 0 0 25 0 1 0 1788522946 27000832 6304 4294967295 134512640 135094434 3221224432 3221223088 134558116 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/24590/statm): 6592 6304 145 145 0 6447 0 [pid=24590] vsize: 26368 Current children cumulated CPU time (s) 1129.71 Current children cumulated vsize (Kb) 28492 [startup+1140.19 s] Raw data (loadavg): 0.99 0.99 0.98 2/57 24590 Raw data (/proc/24586/stat): 24586 (minisat+_script) S 24585 24586 31915 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1788522941 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/24586/statm): 531 226 485 147 0 384 0 [pid=24586] vsize: 2124 Raw data (/proc/24590/stat): 24590 (minisat+_64-bit) R 24586 24586 31915 0 -1 0 6463 0 0 0 113927 45 0 0 25 0 1 0 1788522946 27267072 6369 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/24590/statm): 6657 6369 145 145 0 6512 0 [pid=24590] vsize: 26628 Current children cumulated CPU time (s) 1139.72 Current children cumulated vsize (Kb) 28752 [startup+1150.19 s] Raw data (loadavg): 0.99 0.99 0.98 2/57 24590 Raw data (/proc/24586/stat): 24586 (minisat+_script) S 24585 24586 31915 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1788522941 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/24586/statm): 531 226 485 147 0 384 0 [pid=24586] vsize: 2124 Raw data (/proc/24590/stat): 24590 (minisat+_64-bit) R 24586 24586 31915 0 -1 0 6463 0 0 0 114927 45 0 0 25 0 1 0 1788522946 27267072 6369 4294967295 134512640 135094434 3221224432 3221223088 134557911 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/24590/statm): 6657 6369 145 145 0 6512 0 [pid=24590] vsize: 26628 Current children cumulated CPU time (s) 1149.72 Current children cumulated vsize (Kb) 28752 [startup+1160.19 s] Raw data (loadavg): 0.99 0.99 0.98 2/57 24590 Raw data (/proc/24586/stat): 24586 (minisat+_script) S 24585 24586 31915 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1788522941 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/24586/statm): 531 226 485 147 0 384 0 [pid=24586] vsize: 2124 Raw data (/proc/24590/stat): 24590 (minisat+_64-bit) R 24586 24586 31915 0 -1 0 6464 0 0 0 115928 45 0 0 25 0 1 0 1788522946 27267072 6370 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/24590/statm): 6657 6370 145 145 0 6512 0 [pid=24590] vsize: 26628 Current children cumulated CPU time (s) 1159.73 Current children cumulated vsize (Kb) 28752 [startup+1170.19 s] Raw data (loadavg): 0.99 0.99 0.98 2/57 24590 Raw data (/proc/24586/stat): 24586 (minisat+_script) S 24585 24586 31915 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1788522941 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/24586/statm): 531 226 485 147 0 384 0 [pid=24586] vsize: 2124 Raw data (/proc/24590/stat): 24590 (minisat+_64-bit) R 24586 24586 31915 0 -1 0 6464 0 0 0 116928 45 0 0 25 0 1 0 1788522946 27267072 6370 4294967295 134512640 135094434 3221224432 3221223104 134556073 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/24590/statm): 6657 6370 145 145 0 6512 0 [pid=24590] vsize: 26628 Current children cumulated CPU time (s) 1169.73 Current children cumulated vsize (Kb) 28752 [startup+1180.2 s] Raw data (loadavg): 0.99 0.99 0.98 2/57 24590 Raw data (/proc/24586/stat): 24586 (minisat+_script) S 24585 24586 31915 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1788522941 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/24586/statm): 531 226 485 147 0 384 0 [pid=24586] vsize: 2124 Raw data (/proc/24590/stat): 24590 (minisat+_64-bit) R 24586 24586 31915 0 -1 0 6464 0 0 0 117928 45 0 0 25 0 1 0 1788522946 27267072 6370 4294967295 134512640 135094434 3221224432 3221223088 134558208 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/24590/statm): 6657 6370 145 145 0 6512 0 [pid=24590] vsize: 26628 Current children cumulated CPU time (s) 1179.73 Current children cumulated vsize (Kb) 28752 [startup+1190.2 s] Raw data (loadavg): 0.99 0.99 0.98 2/57 24590 Raw data (/proc/24586/stat): 24586 (minisat+_script) S 24585 24586 31915 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1788522941 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/24586/statm): 531 226 485 147 0 384 0 [pid=24586] vsize: 2124 Raw data (/proc/24590/stat): 24590 (minisat+_64-bit) R 24586 24586 31915 0 -1 0 6466 0 0 0 118928 45 0 0 25 0 1 0 1788522946 27267072 6372 4294967295 134512640 135094434 3221224432 3221223088 134558210 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/24590/statm): 6657 6372 145 145 0 6512 0 [pid=24590] vsize: 26628 Current children cumulated CPU time (s) 1189.73 Current children cumulated vsize (Kb) 28752 [startup+1200.2 s] Raw data (loadavg): 0.99 0.99 0.98 2/57 24590 Raw data (/proc/24586/stat): 24586 (minisat+_script) S 24585 24586 31915 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1788522941 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/24586/statm): 531 226 485 147 0 384 0 [pid=24586] vsize: 2124 Raw data (/proc/24590/stat): 24590 (minisat+_64-bit) R 24586 24586 31915 0 -1 0 6696 0 0 0 119925 47 0 0 25 0 1 0 1788522946 28209152 6602 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/24590/statm): 6887 6602 145 145 0 6742 0 [pid=24590] vsize: 27548 Current children cumulated CPU time (s) 1199.72 Current children cumulated vsize (Kb) 29672 [startup+1210.2 s] Raw data (loadavg): 0.99 0.99 0.98 2/57 24590 Raw data (/proc/24586/stat): 24586 (minisat+_script) S 24585 24586 31915 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1788522941 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/24586/statm): 531 226 485 147 0 384 0 [pid=24586] vsize: 2124 Raw data (/proc/24590/stat): 24590 (minisat+_64-bit) R 24586 24586 31915 0 -1 0 7071 0 0 0 120919 50 0 0 25 0 1 0 1788522946 29745152 6977 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/24590/statm): 7262 6977 145 145 0 7117 0 [pid=24590] vsize: 29048 Current children cumulated CPU time (s) 1209.69 Current children cumulated vsize (Kb) 31172 Maximum CPU time exceeded: sending SIGTERM then SIGKILL [startup+1210.2 s] Raw data (loadavg): 0.99 0.99 0.98 2/57 24590 Raw data (/proc/24586/stat): 24586 (minisat+_script) S 24585 24586 31915 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1788522941 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/24586/statm): 531 226 485 147 0 384 0 [pid=24586] vsize: 2124 Raw data (/proc/24590/stat): 24590 (minisat+_64-bit) R 24586 24586 31915 0 -1 0 7071 0 0 0 120919 50 0 0 25 0 1 0 1788522946 29745152 6977 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/24590/statm): 7262 6977 145 145 0 7117 0 [pid=24590] vsize: 29048 Current children cumulated CPU time (s) 1209.69 Current children cumulated vsize (Kb) 31172 Sending SIGTERM to -24586 Sleeping 2 seconds One traced child (pid=24586) ended because it received signal 15 (SIGTERM) One traced child (pid=24590) exited with status: 10 All traced children have exited ! Game is over. Child status: 10 Real time (s): 1210.22 CPU time (s): 1209.71 CPU user time (s): 1209.19 CPU system time (s): 0.517921 CPU usage (%): 99.958 Max. virtual memory (cumulated for all children) (Kb): 31172
ERROR: no interpretation found !