Name | mps-v2-20-10/ftp.netlib.org/lp/data/normalized-mps-v2-20-10-sc50b.opb |
MD5SUM | f10dfcccbc5d23245c6e708690ee08ea |
Bench Category | optimization, big integers (OPTBIGINT) |
Has Objective Function | YES |
Satisfiable | YES |
(Un)Satisfiability was proved | YES |
Best value of the objective function | -60000 |
Optimality of the best value was proved | NO |
Number of terms in the objective function | 30 |
Biggest coefficient in the objective function | 536870912 |
Number of bits for the biggest coefficient in the objective function | 30 |
Sum of the numbers in the objective function | 1073741823 |
Number of bits of the sum of numbers in the objective function | 30 |
Biggest number in a constraint | 5905580032 |
Number of bits of the biggest number in a constraint | 33 |
Biggest sum of numbers in a constraint | 22548578283 |
Number of bits of the biggest sum of numbers | 35 |
Best result obtained on this benchmark | SAT |
Best CPU time to get the best result obtained on this benchmark | 1195.38 |
Number of variables | 1440 |
Total number of constraints | 48 |
Number of constraints which are clauses | 0 |
Number of constraints which are cardinality constraints (but not clauses) | 0 |
Number of constraints which are nor clauses,nor cardinality constraints | 48 |
Minimum length of a constraint | 60 |
Maximum length of a constraint | 120 |
LAUNCH ON wulflinc25 THE 2005-09-18 20:30:31 (client local time) PB2005-SCRIPT v4.0 MARKUPS: idlaunch=2800 boxname=wulflinc25 idbench=456 idsolver=3 numberseed=0 MD5SUM SOLVER: MD5SUM BENCH: f10dfcccbc5d23245c6e708690ee08ea /oldhome/oroussel/tmp/wulflinc25/normalized-mps-v2-20-10-sc50b.opb REAL COMMAND: minisat+_script /oldhome/oroussel/tmp/wulflinc25/normalized-mps-v2-20-10-sc50b.opb IDLAUNCH: 2800 /proc/cpuinfo: processor : 0 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 2 cpu MHz : 451.220 cache size : 512 KB fdiv_bug : no hlt_bug : no f00f_bug : no coma_bug : no fpu : yes fpu_exception : yes cpuid level : 2 wp : yes flags : fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse bogomips : 888.83 processor : 1 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 3 cpu MHz : 451.220 cache size : 512 KB fdiv_bug : no hlt_bug : no f00f_bug : no coma_bug : no fpu : yes fpu_exception : yes cpuid level : 2 wp : yes flags : fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse bogomips : 901.12 /proc/meminfo: MemTotal: 1034660 kB MemFree: 902672 kB Buffers: 35584 kB Cached: 69464 kB SwapCached: 896 kB Active: 70148 kB Inactive: 37528 kB HighTotal: 131008 kB HighFree: 60172 kB LowTotal: 903652 kB LowFree: 842500 kB SwapTotal: 2097892 kB SwapFree: 2096496 kB Dirty: 28 kB Writeback: 0 kB Mapped: 5716 kB Slab: 18724 kB Committed_AS: 64132 kB PageTables: 328 kB VmallocTotal: 114680 kB VmallocUsed: 1368 kB VmallocChunk: 113252 kB JOB ENDED THE 2005-09-18 20:50:41 (client local time) WITH STATUS 10 IN 1208.77 SECONDS stats: 2800 7 1208.77 10
c Parsing PB file... c Converting 68 PB-constraints to clauses... c -- Unit propagations: ppppppp c -- Detecting intervals from adjacent constraints: #################### c -- Clauses(.)/Splits(s): (none) c ---[ 67]---> Sorter-cost: 364 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 65]---> BDD-cost: 52 c ---[ 63]---> BDD-cost: 49 c ---[ 61]---> BDD-cost: 49 c ---[ 59]---> BDD-cost: 49 c ---[ 58]---> BDD-cost: 49 c ---[ 57]---> BDD-cost: 49 c ---[ 56]---> BDD-cost: 49 c ---[ 55]---> Sorter-cost: 1585 Base: 2 2 2 2 2 2 2 2 2 2 2 2 3 2 2 2 2 c ---[ 54]---> Sorter-cost: 375 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 53]---> Sorter-cost: 658 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 5 c ---[ 51]---> Sorter-cost: 977 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 5 2 2 c ---[ 49]---> BDD-cost: 164 c ---[ 47]---> BDD-cost: 155 c ---[ 45]---> BDD-cost: 155 c ---[ 43]---> BDD-cost: 155 c ---[ 42]---> BDD-cost: 55 c ---[ 41]---> BDD-cost: 55 c ---[ 40]---> BDD-cost: 55 c ---[ 39]---> Sorter-cost: 1776 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 3 2 2 2 c ---[ 38]---> Sorter-cost: 421 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 37]---> Sorter-cost: 736 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 5 c ---[ 35]---> Sorter-cost: 1041 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 5 2 2 c ---[ 33]---> BDD-cost: 177 c ---[ 31]---> BDD-cost: 168 c ---[ 29]---> BDD-cost: 168 c ---[ 27]---> BDD-cost: 168 c ---[ 26]---> BDD-cost: 58 c ---[ 25]---> BDD-cost: 58 c ---[ 24]---> BDD-cost: 58 c ---[ 23]---> Sorter-cost: 1841 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 3 2 2 c ---[ 22]---> Sorter-cost: 444 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 21]---> Sorter-cost: 775 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 5 c ---[ 19]---> Sorter-cost: 1105 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 5 2 2 c ---[ 17]---> BDD-cost: 186 c ---[ 15]---> BDD-cost: 173 c ---[ 13]---> BDD-cost: 173 c ---[ 11]---> BDD-cost: 173 c ---[ 10]---> BDD-cost: 61 c ---[ 9]---> BDD-cost: 61 c ---[ 8]---> BDD-cost: 61 c ---[ 7]---> Sorter-cost: 1951 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 3 2 2 c ---[ 6]---> Sorter-cost: 467 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 5]---> Sorter-cost: 814 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 5 c ---[ 3]---> Sorter-cost: 1166 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 5 2 c ---[ 2]---> Sorter-cost: 1785 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 3 2 2 2 2 c ---[ 1]---> Sorter-cost: 444 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 0]---> Sorter-cost: 775 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 5 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 0 | 54002 128500 | 18000 0 0 nan | 0.000 % | c | 100 | 53990 128473 | 19800 96 994 10.4 | 4.908 % | c | 250 | 53990 128473 | 21780 246 2835 11.5 | 4.908 % | c | 475 | 53888 128241 | 23958 466 8025 17.2 | 5.026 % | c | 813 | 53840 128134 | 26353 801 15304 19.1 | 5.093 % | c | 1319 | 53838 128130 | 28989 1306 24435 18.7 | 5.097 % | c | 2079 | 53838 128130 | 31888 2066 34611 16.8 | 5.097 % | c | 3218 | 53668 127750 | 35076 3160 52130 16.5 | 5.339 % | c | 4928 | 53642 127698 | 38584 4856 80042 16.5 | 5.400 % | c | 7491 | 52982 126198 | 42443 7363 112577 15.3 | 6.412 % | c ============================================================================== c [1mFound solution: 0[0m c ---[ 0]---> BDD-cost: 12 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 8656 | 52983 126212 | 17661 8528 138481 16.2 | 6.412 % | c | 8756 | 52956 126154 | 19427 8622 139763 16.2 | 6.459 % | c | 8907 | 52956 126154 | 21369 8773 142202 16.2 | 6.459 % | c | 9132 | 52956 126154 | 23506 8998 146306 16.3 | 6.459 % | c | 9469 | 52956 126154 | 25857 9335 150772 16.2 | 6.459 % | c | 9975 | 52956 126154 | 28443 9841 159424 16.2 | 6.459 % | c | 10734 | 52932 126102 | 31287 10596 170984 16.1 | 6.497 % | c | 11873 | 52912 126061 | 34416 11725 192917 16.5 | 6.539 % | c | 13581 | 52065 124063 | 37857 12978 214968 16.6 | 7.684 % | c ============================================================================== c [1mFound solution: -30000[0m c ---[ 0]---> BDD-cost: 10 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 15637 | 52075 124088 | 17358 15033 265477 17.7 | 7.684 % | c | 15737 | 52075 124088 | 19093 15133 267118 17.7 | 7.690 % | c | 15887 | 52075 124088 | 21003 15283 272259 17.8 | 7.690 % | c | 16112 | 52054 124041 | 23103 15507 276466 17.8 | 7.719 % | c | 16449 | 52032 123992 | 25413 15843 285028 18.0 | 7.752 % | c | 16956 | 52032 123992 | 27955 16350 296518 18.1 | 7.752 % | c | 17715 | 52030 123988 | 30750 17108 310980 18.2 | 7.757 % | c | 18854 | 52026 123980 | 33825 18244 330875 18.1 | 7.766 % | c ============================================================================== c [1mFound solution: -50000[0m c ---[ 0]---> BDD-cost: 11 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 19376 | 52037 124008 | 17345 18766 339167 18.1 | 7.766 % | c | 19476 | 52037 124008 | 19079 18866 340216 18.0 | 7.769 % | c | 19627 | 52037 124008 | 20987 19017 342688 18.0 | 7.769 % | c | 19852 | 52037 124008 | 23086 19242 348402 18.1 | 7.769 % | c | 20189 | 51774 123409 | 25394 19532 352536 18.0 | 8.166 % | c | 20697 | 51705 123245 | 27934 20037 363238 18.1 | 8.303 % | c | 21456 | 51508 122779 | 30727 20682 376383 18.2 | 8.619 % | c | 22595 | 51408 122541 | 33800 21808 402624 18.5 | 8.822 % | c ============================================================================== c [1mFound solution: -60000[0m c ---[ 0]---> BDD-cost: 12 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 22735 | 51383 122483 | 17127 21640 397595 18.4 | 8.822 % | c | 22835 | 51383 122483 | 18839 10920 167739 15.4 | 8.824 % | c | 22987 | 51376 122468 | 20723 11071 169187 15.3 | 8.833 % | c | 23212 | 51376 122468 | 22796 11296 171562 15.2 | 8.833 % | c | 23552 | 51376 122468 | 25075 11636 181634 15.6 | 8.833 % | c | 24058 | 51278 122237 | 27583 12071 198172 16.4 | 8.999 % | c | 24817 | 51151 121930 | 30341 12756 233513 18.3 | 9.192 % | c | 25958 | 51144 121915 | 33375 13895 270608 19.5 | 9.202 % | c | 27668 | 51056 121705 | 36713 15564 364382 23.4 | 9.391 % | c | 30230 | 51056 121705 | 40384 18126 454277 25.1 | 9.391 % | c | 34074 | 51013 121609 | 44423 21784 661037 30.3 | 9.448 % | c | 39840 | 50905 121361 | 48865 27427 1030725 37.6 | 9.617 % | c | 48490 | 49715 118579 | 53751 34568 1531234 44.3 | 11.308 % | c | 61464 | 49553 118205 | 59127 47449 2188975 46.1 | 11.540 % | c | 80925 | 49553 118205 | 65039 66910 3006402 44.9 | 11.540 % | c | 110119 | 49553 118205 | 71543 38940 3121225 80.2 | 11.541 % | c | 153908 | 49496 118079 | 78698 19529 1721062 88.1 | 11.630 % | c | 219593 | 49251 117508 | 86567 85205 8444929 99.1 | 12.009 % | c | 318121 | 49249 117504 | 95224 30743 2877854 93.6 | 12.012 % | c c *** TERMINATED *** s SATISFIABLE v -COL00004_bit_10 -COL00004_bit_9 -COL00004_bit_8 -COL00004_bit_7 -COL00004_bit_6 COL00004_bit_5 COL00004_bit_4 -COL00004_bit_3 -COL00004_bit_2 COL00004_bit_1 -COL00004_bit0 COL00004_bit1 -COL00004_bit2 COL00004_bit3 COL00004_bit4 COL00004_bit5 -COL00004_bit6 -COL00004_bit7 -COL00004_bit8 -COL00004_bit9 -COL00004_bit10 -COL00004_bit11 -COL00004_bit12 -COL00004_bit13 -COL00004_bit14 -COL00004_bit15 -COL00004_bit16 -COL00004_bit17 -COL00004_bit18 -COL00004_bit19 -COL00001_bit_10 -COL00001_bit_9 -COL00001_bit_8 -COL00001_bit_7 -COL00001_bit_6 -COL00001_bit_5 -COL00001_bit_4 -COL00001_bit_3 -COL00001_bit_2 -COL00001_bit_1 -COL00001_bit0 -COL00001_bit1 -COL00001_bit2 -COL00001_bit3 -COL00001_bit4 -COL00001_bit5 -COL00001_bit6 -COL00001_bit7 -COL00001_bit8 -COL00001_bit9 -COL00001_bit10 -COL00001_bit11 -COL00001_bit12 -COL00001_bit13 -COL00001_bit14 -COL00001_bit15 -COL00001_bit16 -COL00001_bit17 -COL00001_bit18 -COL00001_bit19 -COL00002_bit_10 -COL00002_bit_9 -COL00002_bit_8 -COL00002_bit_7 -COL00002_bit_6 -COL00002_bit_5 -COL00002_bit_4 -COL00002_bit_3 -COL00002_bit_2 -COL00002_bit_1 -COL00002_bit0 -COL00002_bit1 -COL00002_bit2 COL00002_bit3 COL00002_bit4 -COL00002_bit5 -COL00002_bit6 -COL00002_bit7 -COL00002_bit8 -COL00002_bit9 -COL00002_bit10 -COL00002_bit11 -COL00002_bit12 -COL00002_bit13 -COL00002_bit14 -COL00002_bit15 -COL00002_bit16 -COL00002_bit17 -COL00002_bit18 -COL00002_bit19 -COL00003_bit_10 -COL00003_bit_9 -COL00003_bit_8 -COL00003_bit_7 -COL00003_bit_6 -COL00003_bit_5 -COL00003_bit_4 -COL00003_bit_3 -COL00003_bit_2 -COL00003_bit_1 -COL00003_bit0 -COL00003_bit1 COL00003_bit2 COL00003_bit3 -COL00003_bit4 -COL00003_bit5 COL00003_bit6 -COL00003_bit7 -COL00003_bit8 -COL00003_bit9 -COL00003_bit10 -COL00003_bit11 -COL00003_bit12 -COL00003_bit13 -COL00003_bit14 -COL00003_bit15 -COL00003_bit16 -COL00003_bit17 -COL00003_bit18 -COL00003_bit19 -COL00005_bit_10 -COL00005_bit_9 -COL00005_bit_8 -COL00005_bit_7 -COL00005_bit_6 COL00005_bit_5 COL00005_bit_4 -COL00005_bit_3 -COL00005_bit_2 COL00005_bit_1 -COL00005_bit0 COL00005_bit1 -COL00005_bit2 COL00005_bit3 COL00005_bit4 COL00005_bit5 -COL00005_bit6 -COL00005_bit7 -COL00005_bit8 -COL00005_bit9 -COL00005_bit10 -COL00005_bit11 -COL00005_bit12 -COL00005_bit13 -COL00005_bit14 -COL00005_bit15 -COL00005_bit16 -COL00005_bit17 -COL00005_bit18 -COL00005_bit19 -COL00006_bit_10 -COL00006_bit_9 -COL00006_bit_8 -COL00006_bit_7 -COL00006_bit_6 -COL00006_bit_5 -COL00006_bit_4 -COL00006_bit_3 -COL00006_bit_2 -COL00006_bit_1 -COL00006_bit0 -COL00006_bit1 -COL00006_bit2 -COL00006_bit3 -COL00006_bit4 -COL00006_bit5 -COL00006_bit6 -COL00006_bit7 -COL00006_bit8 -COL00006_bit9 -COL00006_bit10 -COL00006_bit11 -COL00006_bit12 -COL00006_bit13 -COL00006_bit14 -COL00006_bit15 -COL00006_bit16 -COL00006_bit17 -COL00006_bit18 -COL00006_bit19 -COL00007_bit_10 -COL00007_bit_9 -COL00007_bit_8 -COL00007_bit_7 -COL00007_bit_6 -COL00007_bit_5 -COL00007_bit_4 -COL00007_bit_3 -COL00007_bit_2 -COL00007_bit_1 -COL00007_bit0 -COL00007_bit1 -COL00007_bit2 COL00007_bit3 COL00007_bit4 -COL00007_bit5 -COL00007_bit6 -COL00007_bit7 -COL00007_bit8 -COL00007_bit9 -COL00007_bit10 -COL00007_bit11 -COL00007_bit12 -COL00007_bit13 -COL00007_bit14 -COL00007_bit15 -COL00007_bit16 -COL00007_bit17 -COL00007_bit18 -COL00007_bit19 -COL00008_bit_10 -COL00008_bit_9 -COL00008_bit_8 -COL00008_bit_7 -COL00008_bit_6 -COL00008_bit_5 -COL00008_bit_4 -COL00008_bit_3 -COL00008_bit_2 -COL00008_bit_1 -COL00008_bit0 -COL00008_bit1 COL00008_bit2 COL00008_bit3 -COL00008_bit4 -COL00008_bit5 COL00008_bit6 -COL00008_bit7 -COL00008_bit8 -COL00008_bit9 -COL00008_bit10 -COL00008_bit11 -COL00008_bit12 -COL00008_bit13 -COL00008_bit14 -COL00008_bit15 -COL00008_bit16 -COL00008_bit17 -COL00008_bit18 -COL00008_bit19 -COL00009_bit_10 -COL00009_bit_9 -COL00009_bit_8 -COL00009_bit_7 -COL00009_bit_6 -COL00009_bit_5 -COL00009_bit_4 -COL00009_bit_3 -COL00009_bit_2 -COL00009_bit_1 -COL00009_bit0 -COL00009_bit1 -COL00009_bit2 -COL00009_bit3 -COL00009_bit4 -COL00009_bit5 -COL00009_bit6 -COL00009_bit7 -COL00009_bit8 -COL00009_bit9 -COL00009_bit10 -COL00009_bit11 -COL00009_bit12 -COL00009_bit13 -COL00009_bit14 -COL00009_bit15 -COL00009_bit16 -COL00009_bit17 -COL00009_bit18 -COL00009_bit19 -COL00010_bit_10 -COL00010_bit_9 -COL00010_bit_8 -COL00010_bit_7 -COL00010_bit_6 -COL00010_bit_5 COL00010_bit_4 COL00010_bit_3 COL00010_bit_2 -COL00010_bit_1 COL00010_bit0 COL00010_bit1 COL00010_bit2 -COL00010_bit3 COL00010_bit4 -COL00010_bit5 -COL00010_bit6 -COL00010_bit7 -COL00010_bit8 -COL00010_bit9 -COL00010_bit10 -COL00010_bit11 -COL00010_bit12 -COL00010_bit13 -COL00010_bit14 -COL00010_bit15 -COL00010_bit16 -COL00010_bit17 -COL00010_bit18 -COL00010_bit19 COL00011_bit_10 COL00011_bit_9 -COL00011_bit_8 COL00011_bit_7 COL00011_bit_6 COL00011_bit_5 -COL00011_bit_4 -COL00011_bit_3 -COL00011_bit_2 -COL00011_bit_1 COL00011_bit0 COL00011_bit1 -COL00011_bit2 COL00011_bit3 -COL00011_bit4 -COL00011_bit5 COL00011_bit6 -COL00011_bit7 -COL00011_bit8 -COL00011_bit9 -COL00011_bit10 -COL00011_bit11 -COL00011_bit12 -COL00011_bit13 -COL00011_bit14 -COL00011_bit15 -COL00011_bit16 -COL00011_bit17 -COL00011_bit18 -COL00011_bit19 -COL00012_bit_10 -COL00012_bit_9 -COL00012_bit_8 -COL00012_bit_7 -COL00012_bit_6 -COL00012_bit_5 -COL00012_bit_4 -COL00012_bit_3 -COL00012_bit_2 -COL00012_bit_1 -COL00012_bit0 -COL00012_bit1 -COL00012_bit2 -COL00012_bit3 -COL00012_bit4 -COL00012_bit5 -COL00012_bit6 -COL00012_bit7 -COL00012_bit8 -COL00012_bit9 -COL00012_bit10 -COL00012_bit11 -COL00012_bit12 -COL00012_bit13 -COL00012_bit14 -COL00012_bit15 -COL00012_bit16 -COL00012_bit17 -COL00012_bit18 -COL00012_bit19 -COL00013_bit_10 -COL00013_bit_9 -COL00013_bit_8 -COL00013_bit_7 -COL00013_bit_6 -COL00013_bit_5 -COL00013_bit_4 -COL00013_bit_3 -COL00013_bit_2 -COL00013_bit_1 -COL00013_bit0 -COL00013_bit1 COL00013_bit2 COL00013_bit3 COL00013_bit4 -COL00013_bit5 -COL00013_bit6 -COL00013_bit7 -COL00013_bit8 -COL00013_bit9 -COL00013_bit10 -COL00013_bit11 -COL00013_bit12 -COL00013_bit13 -COL00013_bit14 -COL00013_bit15 -COL00013_bit16 -COL00013_bit17 -COL00013_bit18 -COL00013_bit19 -COL00014_bit_10 -COL00014_bit_9 -COL00014_bit_8 -COL00014_bit_7 -COL00014_bit_6 -COL00014_bit_5 -COL00014_bit_4 -COL00014_bit_3 -COL00014_bit_2 -COL00014_bit_1 -COL00014_bit0 -COL00014_bit1 -COL00014_bit2 COL00014_bit3 -COL00014_bit4 -COL00014_bit5 COL00014_bit6 -COL00014_bit7 -COL00014_bit8 -COL00014_bit9 -COL00014_bit10 -COL00014_bit11 -COL00014_bit12 -COL00014_bit13 -COL00014_bit14 -COL00014_bit15 -COL00014_bit16 -COL00014_bit17 -COL00014_bit18 -COL00014_bit19 -COL00015_bit_10 -COL00015_bit_9 -COL00015_bit_8 -COL00015_bit_7 COL00015_bit_6 -COL00015_bit_5 COL00015_bit_4 COL00015_bit_3 COL00015_bit_2 -COL00015_bit_1 -COL00015_bit0 -COL00015_bit1 -COL00015_bit2 -COL00015_bit3 -COL00015_bit4 -COL00015_bit5 COL00015_bit6 -COL00015_bit7 -COL00015_bit8 -COL00015_bit9 -COL00015_bit10 -COL00015_bit11 -COL00015_bit12 -COL00015_bit13 -COL00015_bit14 -COL00015_bit15 -COL00015_bit16 -COL00015_bit17 -COL00015_bit18 -COL00015_bit19 -COL00016_bit_10 -COL00016_bit_9 -COL00016_bit_8 -COL00016_bit_7 COL00016_bit_6 COL00016_bit_5 -COL00016_bit_4 -COL00016_bit_3 -COL00016_bit_2 -COL00016_bit_1 COL00016_bit0 COL00016_bit1 -COL00016_bit2 COL00016_bit3 COL00016_bit4 COL00016_bit5 COL00016_bit6 -COL00016_bit7 -COL00016_bit8 -COL00016_bit9 -COL00016_bit10 -COL00016_bit11 -COL00016_bit12 -COL00016_bit13 -COL00016_bit14 -COL00016_bit15 -COL00016_bit16 -COL00016_bit17 -COL00016_bit18 -COL00016_bit19 -COL00017_bit_10 -COL00017_bit_9 -COL00017_bit_8 -COL00017_bit_7 -COL00017_bit_6 -COL00017_bit_5 -COL00017_bit_4 -COL00017_bit_3 -COL00017_bit_2 -COL00017_bit_1 -COL00017_bit0 -COL00017_bit1 -COL00017_bit2 -COL00017_bit3 -COL00017_bit4 -COL00017_bit5 -COL00017_bit6 -COL00017_bit7 -COL00017_bit8 -COL00017_bit9 -COL00017_bit10 -COL00017_bit11 -COL00017_bit12 -COL00017_bit13 -COL00017_bit14 -COL00017_bit15 -COL00017_bit16 -COL00017_bit17 -COL00017_bit18 -COL00017_bit19 -COL00018_bit_10 -COL00018_bit_9 -COL00018_bit_8 -COL00018_bit_7 -COL00018_bit_6 -COL00018_bit_5 -COL00018_bit_4 -COL00018_bit_3 -COL00018_bit_2 -COL00018_bit_1 -COL00018_bit0 -COL00018_bit1 COL00018_bit2 -COL00018_bit3 COL00018_bit4 COL00018_bit5 -COL00018_bit6 -COL00018_bit7 -COL00018_bit8 -COL00018_bit9 -COL00018_bit10 -COL00018_bit11 -COL00018_bit12 -COL00018_bit13 -COL00018_bit14 -COL00018_bit15 -COL00018_bit16 -COL00018_bit17 -COL00018_bit18 -COL00018_bit19 -COL00019_bit_10 -COL00019_bit_9 -COL00019_bit_8 -COL00019_bit_7 -COL00019_bit_6 -COL00019_bit_5 -COL00019_bit_4 -COL00019_bit_3 -COL00019_bit_2 -COL00019_bit_1 -COL00019_bit0 -COL00019_bit1 COL00019_bit2 -COL00019_bit3 COL00019_bit4 -COL00019_bit5 -COL00019_bit6 COL00019_bit7 -COL00019_bit8 -COL00019_bit9 -COL00019_bit10 -COL00019_bit11 -COL00019_bit12 -COL00019_bit13 -COL00019_bit14 -COL00019_bit15 -COL00019_bit16 -COL00019_bit17 -COL00019_bit18 -COL00019_bit19 -COL00020_bit_10 -COL00020_bit_9 -COL00020_bit_8 -COL00020_bit_7 -COL00020_bit_6 -COL00020_bit_5 -COL00020_bit_4 -COL00020_bit_3 -COL00020_bit_2 -COL00020_bit_1 -COL00020_bit0 -COL00020_bit1 -COL00020_bit2 -COL00020_bit3 -COL00020_bit4 -COL00020_bit5 -COL00020_bit6 -COL00020_bit7 -COL00020_bit8 -COL00020_bit9 -COL00020_bit10 -COL00020_bit11 -COL00020_bit12 -COL00020_bit13 -COL00020_bit14 -COL00020_bit15 -COL00020_bit16 -COL00020_bit17 -COL00020_bit18 -COL00020_bit19 -COL00021_bit_10 COL00021_bit_9 -COL00021_bit_8 -COL00021_bit_7 COL00021_bit_6 COL00021_bit_5 -COL00021_bit_4 -COL00021_bit_3 -COL00021_bit_2 COL00021_bit_1 COL00021_bit0 -COL00021_bit1 -COL00021_bit2 -COL00021_bit3 COL00021_bit4 COL00021_bit5 -COL00021_bit6 -COL00021_bit7 -COL00021_bit8 -COL00021_bit9 -COL00021_bit10 -COL00021_bit11 -COL00021_bit12 -COL00021_bit13 -COL00021_bit14 -COL00021_bit15 -COL00021_bit16 -COL00021_bit17 -COL00021_bit18 -COL00021_bit19 COL00022_bit_10 COL00022_bit_9 -COL00022_bit_8 COL00022_bit_7 COL00022_bit_6 COL00022_bit_5 -COL00022_bit_4 -COL00022_bit_3 -COL00022_bit_2 COL00022_bit_1 -COL00022_bit0 COL00022_bit1 COL00022_bit2 -COL00022_bit3 COL00022_bit4 -COL00022_bit5 COL00022_bit6 -COL00022_bit7 -COL00022_bit8 -COL00022_bit9 -COL00022_bit10 -COL00022_bit11 -COL00022_bit12 -COL00022_bit13 -COL00022_bit14 -COL00022_bit15 -COL00022_bit16 -COL00022_bit17 -COL00022_bit18 -COL00022_bit19 -COL00023_bit_10 -COL00023_bit_9 -COL00023_bit_8 -COL00023_bit_7 -COL00023_bit_6 -COL00023_bit_5 COL00023_bit_4 COL00023_bit_3 COL00023_bit_2 COL00023_bit_1 -COL00023_bit0 COL00023_bit1 COL00023_bit2 -COL00023_bit3 COL00023_bit4 COL00023_bit5 -COL00023_bit6 -COL00023_bit7 -COL00023_bit8 -COL00023_bit9 -COL00023_bit10 -COL00023_bit11 -COL00023_bit12 -COL00023_bit13 -COL00023_bit14 -COL00023_bit15 -COL00023_bit16 -COL00023_bit17 -COL00023_bit18 -COL00023_bit19 -COL00024_bit_10 -COL00024_bit_9 -COL00024_bit_8 -COL00024_bit_7 -COL00024_bit_6 COL00024_bit_5 -COL00024_bit_4 COL00024_bit_3 COL00024_bit_2 COL00024_bit_1 COL00024_bit0 COL00024_bit1 COL00024_bit2 COL00024_bit3 COL00024_bit4 -COL00024_bit5 -COL00024_bit6 -COL00024_bit7 -COL00024_bit8 -COL00024_bit9 -COL00024_bit10 -COL00024_bit11 -COL00024_bit12 -COL00024_bit13 -COL00024_bit14 -COL00024_bit15 -COL00024_bit16 -COL00024_bit17 -COL00024_bit18 -COL00024_bit19 -COL00025_bit_10 -COL00025_bit_9 -COL00025_bit_8 -COL00025_bit_7 -COL00025_bit_6 -COL00025_bit_5 -COL00025_bit_4 COL00025_bit_3 COL00025_bit_2 COL00025_bit_1 -COL00025_bit0 COL00025_bit1 COL00025_bit2 -COL00025_bit3 -COL00025_bit4 -COL00025_bit5 -COL00025_bit6 -COL00025_bit7 -COL00025_bit8 -COL00025_bit9 -COL00025_bit10 -COL00025_bit11 -COL00025_bit12 -COL00025_bit13 -COL00025_bit14 -COL00025_bit15 -COL00025_bit16 -COL00025_bit17 -COL00025_bit18 -COL00025_bit19 -COL00026_bit_10 -COL00026_bit_9 -COL00026_bit_8 COL00026_bit_7 COL00026_bit_6 -COL00026_bit_5 -COL00026_bit_4 COL00026_bit_3 COL00026_bit_2 COL00026_bit_1 -COL00026_bit0 COL00026_bit1 COL00026_bit2 -COL00026_bit3 -COL00026_bit4 -COL00026_bit5 COL00026_bit6 -COL00026_bit7 -COL00026_bit8 -COL00026_bit9 -COL00026_bit10 -COL00026_bit11 -COL00026_bit12 -COL00026_bit13 -COL00026_bit14 -COL00026_bit15 -COL00026_bit16 -COL00026_bit17 -COL00026_bit18 -COL00026_bit19 -COL00027_bit_10 -COL00027_bit_9 -COL00027_bit_8 COL00027_bit_7 -COL00027_bit_6 -COL00027_bit_5 COL00027_bit_4 COL00027_bit_3 COL00027_bit_2 COL00027_bit_1 COL00027_bit0 -COL00027_bit1 -COL00027_bit2 -COL00027_bit3 -COL00027_bit4 -COL00027_bit5 COL00027_bit6 COL00027_bit7 -COL00027_bit8 -COL00027_bit9 -COL00027_bit10 -COL00027_bit11 -COL00027_bit12 -COL00027_bit13 -COL00027_bit14 -COL00027_bit15 -COL00027_bit16 -COL00027_bit17 -COL00027_bit18 -COL00027_bit19 -COL00028_bit_10 -COL00028_bit_9 -COL00028_bit_8 -COL00028_bit_7 -COL00028_bit_6 -COL00028_bit_5 COL00028_bit_4 COL00028_bit_3 COL00028_bit_2 COL00028_bit_1 -COL00028_bit0 COL00028_bit1 COL00028_bit2 -COL00028_bit3 COL00028_bit4 COL00028_bit5 -COL00028_bit6 -COL00028_bit7 -COL00028_bit8 -COL00028_bit9 -COL00028_bit10 -COL00028_bit11 -COL00028_bit12 -COL00028_bit13 -COL00028_bit14 -COL00028_bit15 -COL00028_bit16 -COL00028_bit17 -COL00028_bit18 -COL00028_bit19 -COL00029_bit_10 -COL00029_bit_9 -COL00029_bit_8 -COL00029_bit_7 -COL00029_bit_6 COL00029_bit_5 -COL00029_bit_4 COL00029_bit_3 COL00029_bit_2 COL00029_bit_1 COL00029_bit0 COL00029_bit1 -COL00029_bit2 -COL00029_bit3 COL00029_bit4 -COL00029_bit5 COL00029_bit6 -COL00029_bit7 -COL00029_bit8 -COL00029_bit9 -COL00029_bit10 -COL00029_bit11 -COL00029_bit12 -COL00029_bit13 -COL00029_bit14 -COL00029_bit15 -COL00029_bit16 -COL00029_bit17 -COL00029_bit18 -COL00029_bit19 -COL00030_bit_10 -COL00030_bit_9 -COL00030_bit_8 -COL00030_bit_7 -COL00030_bit_6 -COL00030_bit_5 -COL00030_bit_4 COL00030_bit_3 COL00030_bit_2 COL00030_bit_1 -COL00030_bit0 COL00030_bit1 -COL00030_bit2 COL00030_bit3 COL00030_bit4 -COL00030_bit5 -COL00030_bit6 COL00030_bit7 -COL00030_bit8 -COL00030_bit9 -COL00030_bit10 -COL00030_bit11 -COL00030_bit12 -COL00030_bit13 -COL00030_bit14 -COL00030_bit15 -COL00030_bit16 -COL00030_bit17 -COL00030_bit18 -COL00030_bit19 COL00031_bit_10 COL00031_bit_9 -COL00031_bit_8 COL00031_bit_7 COL00031_bit_6 -COL00031_bit_5 -COL00031_bit_4 -COL00031_bit_3 COL00031_bit_2 COL00031_bit_1 COL00031_bit0 COL00031_bit1 -COL00031_bit2 -COL00031_bit3 COL00031_bit4 COL00031_bit5 -COL00031_bit6 -COL00031_bit7 -COL00031_bit8 -COL00031_bit9 -COL00031_bit10 -COL00031_bit11 -COL00031_bit12 -COL00031_bit13 -COL00031_bit14 -COL00031_bit15 -COL00031_bit16 -COL00031_bit17 -COL00031_bit18 -COL00031_bit19 COL00032_bit_10 COL00032_bit_9 -COL00032_bit_8 COL00032_bit_7 COL00032_bit_6 COL00032_bit_5 COL00032_bit_4 -COL00032_bit_3 -COL00032_bit_2 COL00032_bit_1 COL00032_bit0 -COL00032_bit1 COL00032_bit2 COL00032_bit3 -COL00032_bit4 -COL00032_bit5 COL00032_bit6 -COL00032_bit7 -COL00032_bit8 -COL00032_bit9 -COL00032_bit10 -COL00032_bit11 -COL00032_bit12 -COL00032_bit13 -COL00032_bit14 -COL00032_bit15 -COL00032_bit16 -COL00032_bit17 -COL00032_bit18 -COL00032_bit19 -COL00033_bit_10 -COL00033_bit_9 -COL00033_bit_8 -COL00033_bit_7 COL00033_bit_6 -COL00033_bit_5 -COL00033_bit_4 COL00033_bit_3 -COL00033_bit_2 -COL00033_bit_1 -COL00033_bit0 COL00033_bit1 COL00033_bit2 -COL00033_bit3 COL00033_bit4 -COL00033_bit5 -COL00033_bit6 COL00033_bit7 -COL00033_bit8 -COL00033_bit9 -COL00033_bit10 -COL00033_bit11 -COL00033_bit12 -COL00033_bit13 -COL00033_bit14 -COL00033_bit15 -COL00033_bit16 -COL00033_bit17 -COL00033_bit18 -COL00033_bit19 -COL00034_bit_10 COL00034_bit_9 COL00034_bit_8 COL00034_bit_7 COL00034_bit_6 COL00034_bit_5 COL00034_bit_4 COL00034_bit_3 COL00034_bit_2 COL00034_bit_1 COL00034_bit0 COL00034_bit1 COL00034_bit2 COL00034_bit3 -COL00034_bit4 -COL00034_bit5 -COL00034_bit6 -COL00034_bit7 -COL00034_bit8 -COL00034_bit9 -COL00034_bit10 -COL00034_bit11 -COL00034_bit12 -COL00034_bit13 -COL00034_bit14 -COL00034_bit15 -COL00034_bit16 -COL00034_bit17 -COL00034_bit18 -COL00034_bit19 -COL00035_bit_10 -COL00035_bit_9 -COL00035_bit_8 COL00035_bit_7 COL00035_bit_6 -COL00035_bit_5 COL00035_bit_4 -COL00035_bit_3 -COL00035_bit_2 -COL00035_bit_1 -COL00035_bit0 -COL00035_bit1 COL00035_bit2 -COL00035_bit3 -COL00035_bit4 COL00035_bit5 -COL00035_bit6 -COL00035_bit7 -COL00035_bit8 -COL00035_bit9 -COL00035_bit10 -COL00035_bit11 -COL00035_bit12 -COL00035_bit13 -COL00035_bit14 -COL00035_bit15 -COL00035_bit16 -COL00035_bit17 -COL00035_bit18 -COL00035_bit19 -COL00036_bit_10 -COL00036_bit_9 -COL00036_bit_8 -COL00036_bit_7 COL00036_bit_6 -COL00036_bit_5 -COL00036_bit_4 -COL00036_bit_3 -COL00036_bit_2 -COL00036_bit_1 COL00036_bit0 -COL00036_bit1 -COL00036_bit2 -COL00036_bit3 -COL00036_bit4 -COL00036_bit5 COL00036_bit6 -COL00036_bit7 -COL00036_bit8 -COL00036_bit9 -COL00036_bit10 -COL00036_bit11 -COL00036_bit12 -COL00036_bit13 -COL00036_bit14 -COL00036_bit15 -COL00036_bit16 -COL00036_bit17 -COL00036_bit18 -COL00036_bit19 -COL00037_bit_10 -COL00037_bit_9 COL00037_bit_8 -COL00037_bit_7 COL00037_bit_6 COL00037_bit_5 COL00037_bit_4 COL00037_bit_3 COL00037_bit_2 COL00037_bit_1 COL00037_bit0 -COL00037_bit1 COL00037_bit2 COL00037_bit3 -COL00037_bit4 -COL00037_bit5 COL00037_bit6 -COL00037_bit7 -COL00037_bit8 -COL00037_bit9 -COL00037_bit10 -COL00037_bit11 -COL00037_bit12 -COL00037_bit13 -COL00037_bit14 -COL00037_bit15 -COL00037_bit16 -COL00037_bit17 -COL00037_bit18 -COL00037_bit19 -COL00038_bit_10 -COL00038_bit_9 COL00038_bit_8 COL00038_bit_7 COL00038_bit_6 COL00038_bit_5 -COL00038_bit_4 COL00038_bit_3 COL00038_bit_2 COL00038_bit_1 COL00038_bit0 COL00038_bit1 COL00038_bit2 COL00038_bit3 -COL00038_bit4 -COL00038_bit5 -COL00038_bit6 -COL00038_bit7 COL00038_bit8 -COL00038_bit9 -COL00038_bit10 -COL00038_bit11 -COL00038_bit12 -COL00038_bit13 -COL00038_bit14 -COL00038_bit15 -COL00038_bit16 -COL00038_bit17 -COL00038_bit18 -COL00038_bit19 -COL00039_bit_10 COL00039_bit_9 COL00039_bit_8 COL00039_bit_7 COL00039_bit_6 COL00039_bit_5 -COL00039_bit_4 COL00039_bit_3 COL00039_bit_2 COL00039_bit_1 -COL00039_bit0 COL00039_bit1 COL00039_bit2 -COL00039_bit3 -COL00039_bit4 -COL00039_bit5 COL00039_bit6 -COL00039_bit7 -COL00039_bit8 -COL00039_bit9 -COL00039_bit10 -COL00039_bit11 -COL00039_bit12 -COL00039_bit13 -COL00039_bit14 -COL00039_bit15 -COL00039_bit16 -COL00039_bit17 -COL00039_bit18 -COL00039_bit19 -COL00040_bit_10 -COL00040_bit_9 -COL00040_bit_8 COL00040_bit_7 COL00040_bit_6 COL00040_bit_5 COL00040_bit_4 COL00040_bit_3 COL00040_bit_2 COL00040_bit_1 COL00040_bit0 COL00040_bit1 COL00040_bit2 -COL00040_bit3 COL00040_bit4 COL00040_bit5 COL00040_bit6 -COL00040_bit7 -COL00040_bit8 -COL00040_bit9 -COL00040_bit10 -COL00040_bit11 -COL00040_bit12 -COL00040_bit13 -COL00040_bit14 -COL00040_bit15 -COL00040_bit16 -COL00040_bit17 -COL00040_bit18 -COL00040_bit19 -COL00041_bit_10 -COL00041_bit_9 -COL00041_bit_8 -COL00041_bit_7 COL00041_bit_6 -COL00041_bit_5 -COL00041_bit_4 COL00041_bit_3 COL00041_bit_2 COL00041_bit_1 COL00041_bit0 COL00041_bit1 -COL00041_bit2 COL00041_bit3 COL00041_bit4 -COL00041_bit5 COL00041_bit6 COL00041_bit7 -COL00041_bit8 -COL00041_bit9 -COL00041_bit10 -COL00041_bit11 -COL00041_bit12 -COL00041_bit13 -COL00041_bit14 -COL00041_bit15 -COL00041_bit16 -COL00041_bit17 -COL00041_bit18 -COL00041_bit19 -COL00042_bit_10 COL00042_bit_9 COL00042_bit_8 COL00042_bit_7 COL00042_bit_6 COL00042_bit_5 -COL00042_bit_4 COL00042_bit_3 COL00042_bit_2 COL00042_bit_1 -COL00042_bit0 COL00042_bit1 COL00042_bit2 -COL00042_bit3 -COL00042_bit4 -COL00042_bit5 COL00042_bit6 -COL00042_bit7 -COL00042_bit8 -COL00042_bit9 -COL00042_bit10 -COL00042_bit11 -COL00042_bit12 -COL00042_bit13 -COL00042_bit14 -COL00042_bit15 -COL00042_bit16 -COL00042_bit17 -COL00042_bit18 -COL00042_bit19 -COL00043_bit_10 -COL00043_bit_9 -COL00043_bit_8 COL00043_bit_7 COL00043_bit_6 -COL00043_bit_5 -COL00043_bit_4 -COL00043_bit_3 COL00043_bit_2 COL00043_bit_1 -COL00043_bit0 -COL00043_bit1 COL00043_bit2 COL00043_bit3 -COL00043_bit4 COL00043_bit5 COL00043_bit6 -COL00043_bit7 -COL00043_bit8 -COL00043_bit9 -COL00043_bit10 -COL00043_bit11 -COL00043_bit12 -COL00043_bit13 -COL00043_bit14 -COL00043_bit15 -COL00043_bit16 -COL00043_bit17 -COL00043_bit18 -COL00043_bit19 COL00044_bit_10 COL00044_bit_9 -COL00044_bit_8 -COL00044_bit_7 -COL00044_bit_6 COL00044_bit_5 COL00044_bit_4 COL00044_bit_3 COL00044_bit_2 COL00044_bit_1 COL00044_bit0 COL00044_bit1 COL00044_bit2 -COL00044_bit3 -COL00044_bit4 -COL00044_bit5 COL00044_bit6 COL00044_bit7 -COL00044_bit8 -COL00044_bit9 -COL00044_bit10 -COL00044_bit11 -COL00044_bit12 -COL00044_bit13 -COL00044_bit14 -COL00044_bit15 -COL00044_bit16 -COL00044_bit17 -COL00044_bit18 -COL00044_
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/16380/stat): 16380 (minisat+_script) R 16379 16380 4419 0 -1 0 19 0 0 0 0 0 0 0 23 0 1 0 1844176082 712704 3 4294967295 134512640 135087896 3221224496 3221224496 1073744960 0 0 5 0 0 0 0 17 0 0 0 Raw data (/proc/16380/statm): 174 3 169 147 0 27 0 [pid=16380] 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=16381 New process pid=16382 New process pid=16383 execve syscall for /bin/sed executable One traced child (pid=16382) exited with status: 0 open syscall for file /etc/ld.so.preload open syscall for file tls/i686/mmx/libc.so.6 open syscall for file tls/i686/libc.so.6 open syscall for file tls/mmx/libc.so.6 open syscall for file tls/libc.so.6 open syscall for file i686/mmx/libc.so.6 open syscall for file i686/libc.so.6 open syscall for file mmx/libc.so.6 open syscall for file libc.so.6 open syscall for file /oldhome/oroussel/lib/tls/i686/mmx/libc.so.6 open syscall for file /oldhome/oroussel/lib/tls/i686/libc.so.6 open syscall for file /oldhome/oroussel/lib/tls/mmx/libc.so.6 open syscall for file /oldhome/oroussel/lib/tls/libc.so.6 open syscall for file /oldhome/oroussel/lib/i686/mmx/libc.so.6 open syscall for file /oldhome/oroussel/lib/i686/libc.so.6 open syscall for file /oldhome/oroussel/lib/mmx/libc.so.6 open syscall for file /oldhome/oroussel/lib/libc.so.6 open syscall for file /etc/ld.so.cache open syscall for file /lib/tls/libc.so.6 One traced child (pid=16383) exited with status: 0 One traced child (pid=16381) exited with status: 0 New process pid=16384 execve syscall for /oldhome/oroussel/solvers/minisat+_64-bit_static executable open syscall for file /dev/null open syscall for file /oldhome/oroussel/tmp/wulflinc25/normalized-mps-v2-20-10-sc50b.opb [startup+10.0034 s] Raw data (loadavg): 0.87 0.93 0.90 2/57 16384 Raw data (/proc/16380/stat): 16380 (minisat+_script) S 16379 16380 4419 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1844176082 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/16380/statm): 531 226 485 147 0 384 0 [pid=16380] vsize: 2124 Raw data (/proc/16384/stat): 16384 (minisat+_64-bit) R 16380 16380 4419 0 -1 0 2111 0 0 0 977 9 0 0 25 0 1 0 1844176087 9388032 2006 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/16384/statm): 2292 2006 145 145 0 2147 0 [pid=16384] vsize: 9168 Current children cumulated CPU time (s) 9.87 Current children cumulated vsize (Kb) 11292 [startup+20.005 s] Raw data (loadavg): 0.89 0.93 0.90 2/57 16384 Raw data (/proc/16380/stat): 16380 (minisat+_script) S 16379 16380 4419 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1844176082 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/16380/statm): 531 226 485 147 0 384 0 [pid=16380] vsize: 2124 Raw data (/proc/16384/stat): 16384 (minisat+_64-bit) R 16380 16380 4419 0 -1 0 2368 0 0 0 1973 11 0 0 25 0 1 0 1844176087 10518528 2263 4294967295 134512640 135094434 3221224432 3221223024 134557219 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/16384/statm): 2568 2263 145 145 0 2423 0 [pid=16384] vsize: 10272 Current children cumulated CPU time (s) 19.85 Current children cumulated vsize (Kb) 12396 [startup+30.0056 s] Raw data (loadavg): 0.90 0.93 0.90 2/57 16384 Raw data (/proc/16380/stat): 16380 (minisat+_script) S 16379 16380 4419 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1844176082 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/16380/statm): 531 226 485 147 0 384 0 [pid=16380] vsize: 2124 Raw data (/proc/16384/stat): 16384 (minisat+_64-bit) R 16380 16380 4419 0 -1 0 2547 0 0 0 2969 13 0 0 25 0 1 0 1844176087 11284480 2442 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/16384/statm): 2755 2442 145 145 0 2610 0 [pid=16384] vsize: 11020 Current children cumulated CPU time (s) 29.83 Current children cumulated vsize (Kb) 13144 [startup+40.0062 s] Raw data (loadavg): 0.99 0.95 0.91 2/57 16384 Raw data (/proc/16380/stat): 16380 (minisat+_script) S 16379 16380 4419 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1844176082 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/16380/statm): 531 226 485 147 0 384 0 [pid=16380] vsize: 2124 Raw data (/proc/16384/stat): 16384 (minisat+_64-bit) R 16380 16380 4419 0 -1 0 2842 0 0 0 3964 15 0 0 25 0 1 0 1844176087 12496896 2737 4294967295 134512640 135094434 3221224432 3221223088 134558395 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/16384/statm): 3051 2737 145 145 0 2906 0 [pid=16384] vsize: 12204 Current children cumulated CPU time (s) 39.8 Current children cumulated vsize (Kb) 14328 [startup+50.0068 s] Raw data (loadavg): 0.99 0.95 0.91 2/57 16384 Raw data (/proc/16380/stat): 16380 (minisat+_script) S 16379 16380 4419 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1844176082 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/16380/statm): 531 226 485 147 0 384 0 [pid=16380] vsize: 2124 Raw data (/proc/16384/stat): 16384 (minisat+_64-bit) R 16380 16380 4419 0 -1 0 3304 0 0 0 4956 19 0 0 25 0 1 0 1844176087 14364672 3199 4294967295 134512640 135094434 3221224432 3221223024 134557421 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/16384/statm): 3507 3199 145 145 0 3362 0 [pid=16384] vsize: 14028 Current children cumulated CPU time (s) 49.76 Current children cumulated vsize (Kb) 16152 [startup+60.0064 s] Raw data (loadavg): 0.99 0.95 0.91 2/57 16384 Raw data (/proc/16380/stat): 16380 (minisat+_script) S 16379 16380 4419 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1844176082 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/16380/statm): 531 226 485 147 0 384 0 [pid=16380] vsize: 2124 Raw data (/proc/16384/stat): 16384 (minisat+_64-bit) R 16380 16380 4419 0 -1 0 3669 0 0 0 5949 21 0 0 25 0 1 0 1844176087 15843328 3564 4294967295 134512640 135094434 3221224432 3221223024 134557273 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/16384/statm): 3868 3564 145 145 0 3723 0 [pid=16384] vsize: 15472 Current children cumulated CPU time (s) 59.71 Current children cumulated vsize (Kb) 17596 [startup+70.008 s] Raw data (loadavg): 0.99 0.95 0.91 2/57 16384 Raw data (/proc/16380/stat): 16380 (minisat+_script) S 16379 16380 4419 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1844176082 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/16380/statm): 531 226 485 147 0 384 0 [pid=16380] vsize: 2124 Raw data (/proc/16384/stat): 16384 (minisat+_64-bit) R 16380 16380 4419 0 -1 0 4029 0 0 0 6941 24 0 0 25 0 1 0 1844176087 17428480 3924 4294967295 134512640 135094434 3221224432 3221223104 134555957 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/16384/statm): 4255 3924 145 145 0 4110 0 [pid=16384] vsize: 17020 Current children cumulated CPU time (s) 69.66 Current children cumulated vsize (Kb) 19144 [startup+80.0096 s] Raw data (loadavg): 0.99 0.96 0.91 2/57 16384 Raw data (/proc/16380/stat): 16380 (minisat+_script) S 16379 16380 4419 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1844176082 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/16380/statm): 531 226 485 147 0 384 0 [pid=16380] vsize: 2124 Raw data (/proc/16384/stat): 16384 (minisat+_64-bit) R 16380 16380 4419 0 -1 0 4361 0 0 0 7934 27 0 0 25 0 1 0 1844176087 18759680 4256 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/16384/statm): 4580 4256 145 145 0 4435 0 [pid=16384] vsize: 18320 Current children cumulated CPU time (s) 79.62 Current children cumulated vsize (Kb) 20444 [startup+90.0102 s] Raw data (loadavg): 0.99 0.96 0.91 2/57 16384 Raw data (/proc/16380/stat): 16380 (minisat+_script) S 16379 16380 4419 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1844176082 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/16380/statm): 531 226 485 147 0 384 0 [pid=16380] vsize: 2124 Raw data (/proc/16384/stat): 16384 (minisat+_64-bit) R 16380 16380 4419 0 -1 0 4748 0 0 0 8927 31 0 0 25 0 1 0 1844176087 20332544 4643 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/16384/statm): 4964 4643 145 145 0 4819 0 [pid=16384] vsize: 19856 Current children cumulated CPU time (s) 89.59 Current children cumulated vsize (Kb) 21980 [startup+100.011 s] Raw data (loadavg): 0.99 0.96 0.91 2/57 16384 Raw data (/proc/16380/stat): 16380 (minisat+_script) S 16379 16380 4419 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1844176082 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/16380/statm): 531 226 485 147 0 384 0 [pid=16380] vsize: 2124 Raw data (/proc/16384/stat): 16384 (minisat+_64-bit) R 16380 16380 4419 0 -1 0 4959 0 0 0 9923 33 0 0 25 0 1 0 1844176087 21180416 4854 4294967295 134512640 135094434 3221224432 3221223088 134557950 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/16384/statm): 5171 4854 145 145 0 5026 0 [pid=16384] vsize: 20684 Current children cumulated CPU time (s) 99.57 Current children cumulated vsize (Kb) 22808 [startup+110.011 s] Raw data (loadavg): 0.99 0.96 0.91 2/57 16384 Raw data (/proc/16380/stat): 16380 (minisat+_script) S 16379 16380 4419 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1844176082 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/16380/statm): 531 226 485 147 0 384 0 [pid=16380] vsize: 2124 Raw data (/proc/16384/stat): 16384 (minisat+_64-bit) R 16380 16380 4419 0 -1 0 5127 0 0 0 10920 34 0 0 25 0 1 0 1844176087 21864448 5022 4294967295 134512640 135094434 3221224432 3221223056 134562085 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/16384/statm): 5338 5022 145 145 0 5193 0 [pid=16384] vsize: 21352 Current children cumulated CPU time (s) 109.55 Current children cumulated vsize (Kb) 23476 [startup+120.013 s] Raw data (loadavg): 0.99 0.96 0.91 2/57 16384 Raw data (/proc/16380/stat): 16380 (minisat+_script) S 16379 16380 4419 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1844176082 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/16380/statm): 531 226 485 147 0 384 0 [pid=16380] vsize: 2124 Raw data (/proc/16384/stat): 16384 (minisat+_64-bit) R 16380 16380 4419 0 -1 0 5309 0 0 0 11917 35 0 0 25 0 1 0 1844176087 22589440 5204 4294967295 134512640 135094434 3221224432 3221223024 134556964 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/16384/statm): 5515 5204 145 145 0 5370 0 [pid=16384] vsize: 22060 Current children cumulated CPU time (s) 119.53 Current children cumulated vsize (Kb) 24184 [startup+130.014 s] Raw data (loadavg): 0.99 0.96 0.91 2/57 16384 Raw data (/proc/16380/stat): 16380 (minisat+_script) S 16379 16380 4419 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1844176082 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/16380/statm): 531 226 485 147 0 384 0 [pid=16380] vsize: 2124 Raw data (/proc/16384/stat): 16384 (minisat+_64-bit) R 16380 16380 4419 0 -1 0 5473 0 0 0 12912 36 0 0 25 0 1 0 1844176087 23257088 5368 4294967295 134512640 135094434 3221224432 3221223024 134557230 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/16384/statm): 5678 5368 145 145 0 5533 0 [pid=16384] vsize: 22712 Current children cumulated CPU time (s) 129.49 Current children cumulated vsize (Kb) 24836 [startup+140.015 s] Raw data (loadavg): 0.99 0.96 0.91 2/57 16384 Raw data (/proc/16380/stat): 16380 (minisat+_script) S 16379 16380 4419 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1844176082 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/16380/statm): 531 226 485 147 0 384 0 [pid=16380] vsize: 2124 Raw data (/proc/16384/stat): 16384 (minisat+_64-bit) R 16380 16380 4419 0 -1 0 5669 0 0 0 13908 38 0 0 25 0 1 0 1844176087 24322048 5564 4294967295 134512640 135094434 3221224432 3221223088 134558187 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/16384/statm): 5938 5564 145 145 0 5793 0 [pid=16384] vsize: 23752 Current children cumulated CPU time (s) 139.47 Current children cumulated vsize (Kb) 25876 [startup+150.017 s] Raw data (loadavg): 0.99 0.96 0.91 2/57 16384 Raw data (/proc/16380/stat): 16380 (minisat+_script) S 16379 16380 4419 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1844176082 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/16380/statm): 531 226 485 147 0 384 0 [pid=16380] vsize: 2124 Raw data (/proc/16384/stat): 16384 (minisat+_64-bit) R 16380 16380 4419 0 -1 0 5898 0 0 0 14905 40 0 0 25 0 1 0 1844176087 25251840 5793 4294967295 134512640 135094434 3221224432 3221223044 134563121 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/16384/statm): 6165 5793 145 145 0 6020 0 [pid=16384] vsize: 24660 Current children cumulated CPU time (s) 149.46 Current children cumulated vsize (Kb) 26784 [startup+160.017 s] Raw data (loadavg): 0.99 0.96 0.91 2/57 16384 Raw data (/proc/16380/stat): 16380 (minisat+_script) S 16379 16380 4419 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1844176082 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/16380/statm): 531 226 485 147 0 384 0 [pid=16380] vsize: 2124 Raw data (/proc/16384/stat): 16384 (minisat+_64-bit) R 16380 16380 4419 0 -1 0 6230 0 0 0 15898 43 0 0 25 0 1 0 1844176087 26599424 6125 4294967295 134512640 135094434 3221224432 3221223024 134557042 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/16384/statm): 6494 6125 145 145 0 6349 0 [pid=16384] vsize: 25976 Current children cumulated CPU time (s) 159.42 Current children cumulated vsize (Kb) 28100 [startup+170.019 s] Raw data (loadavg): 0.99 0.96 0.91 2/57 16384 Raw data (/proc/16380/stat): 16380 (minisat+_script) S 16379 16380 4419 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1844176082 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/16380/statm): 531 226 485 147 0 384 0 [pid=16380] vsize: 2124 Raw data (/proc/16384/stat): 16384 (minisat+_64-bit) R 16380 16380 4419 0 -1 0 6460 0 0 0 16894 45 0 0 25 0 1 0 1844176087 27533312 6355 4294967295 134512640 135094434 3221224432 3221223024 134556806 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/16384/statm): 6722 6355 145 145 0 6577 0 [pid=16384] vsize: 26888 Current children cumulated CPU time (s) 169.4 Current children cumulated vsize (Kb) 29012 [startup+180.02 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 16384 Raw data (/proc/16380/stat): 16380 (minisat+_script) S 16379 16380 4419 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1844176082 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/16380/statm): 531 226 485 147 0 384 0 [pid=16380] vsize: 2124 Raw data (/proc/16384/stat): 16384 (minisat+_64-bit) R 16380 16380 4419 0 -1 0 6508 0 0 0 17893 45 0 0 25 0 1 0 1844176087 27729920 6403 4294967295 134512640 135094434 3221224432 3221223024 134557334 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/16384/statm): 6770 6403 145 145 0 6625 0 [pid=16384] vsize: 27080 Current children cumulated CPU time (s) 179.39 Current children cumulated vsize (Kb) 29204 [startup+190.02 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 16384 Raw data (/proc/16380/stat): 16380 (minisat+_script) S 16379 16380 4419 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1844176082 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/16380/statm): 531 226 485 147 0 384 0 [pid=16380] vsize: 2124 Raw data (/proc/16384/stat): 16384 (minisat+_64-bit) R 16380 16380 4419 0 -1 0 6508 0 0 0 18892 46 0 0 25 0 1 0 1844176087 27729920 6403 4294967295 134512640 135094434 3221224432 3221223024 134557429 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/16384/statm): 6770 6403 145 145 0 6625 0 [pid=16384] vsize: 27080 Current children cumulated CPU time (s) 189.39 Current children cumulated vsize (Kb) 29204 [startup+200.021 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 16384 Raw data (/proc/16380/stat): 16380 (minisat+_script) S 16379 16380 4419 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1844176082 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/16380/statm): 531 226 485 147 0 384 0 [pid=16380] vsize: 2124 Raw data (/proc/16384/stat): 16384 (minisat+_64-bit) R 16380 16380 4419 0 -1 0 6508 0 0 0 19892 46 0 0 25 0 1 0 1844176087 27729920 6403 4294967295 134512640 135094434 3221224432 3221223024 134556880 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/16384/statm): 6770 6403 145 145 0 6625 0 [pid=16384] vsize: 27080 Current children cumulated CPU time (s) 199.39 Current children cumulated vsize (Kb) 29204 [startup+210.021 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 16384 Raw data (/proc/16380/stat): 16380 (minisat+_script) S 16379 16380 4419 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1844176082 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/16380/statm): 531 226 485 147 0 384 0 [pid=16380] vsize: 2124 Raw data (/proc/16384/stat): 16384 (minisat+_64-bit) R 16380 16380 4419 0 -1 0 6508 0 0 0 20891 46 0 0 25 0 1 0 1844176087 27729920 6403 4294967295 134512640 135094434 3221224432 3221223024 134556933 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/16384/statm): 6770 6403 145 145 0 6625 0 [pid=16384] vsize: 27080 Current children cumulated CPU time (s) 209.38 Current children cumulated vsize (Kb) 29204 [startup+220.023 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 16384 Raw data (/proc/16380/stat): 16380 (minisat+_script) S 16379 16380 4419 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1844176082 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/16380/statm): 531 226 485 147 0 384 0 [pid=16380] vsize: 2124 Raw data (/proc/16384/stat): 16384 (minisat+_64-bit) R 16380 16380 4419 0 -1 0 6508 0 0 0 21891 47 0 0 25 0 1 0 1844176087 27729920 6403 4294967295 134512640 135094434 3221224432 3221223024 134557413 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/16384/statm): 6770 6403 145 145 0 6625 0 [pid=16384] vsize: 27080 Current children cumulated CPU time (s) 219.39 Current children cumulated vsize (Kb) 29204 [startup+230.024 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 16384 Raw data (/proc/16380/stat): 16380 (minisat+_script) S 16379 16380 4419 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1844176082 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/16380/statm): 531 226 485 147 0 384 0 [pid=16380] vsize: 2124 Raw data (/proc/16384/stat): 16384 (minisat+_64-bit) R 16380 16380 4419 0 -1 0 6508 0 0 0 22891 47 0 0 25 0 1 0 1844176087 27729920 6403 4294967295 134512640 135094434 3221224432 3221223024 134557512 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/16384/statm): 6770 6403 145 145 0 6625 0 [pid=16384] vsize: 27080 Current children cumulated CPU time (s) 229.39 Current children cumulated vsize (Kb) 29204 [startup+240.024 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 16384 Raw data (/proc/16380/stat): 16380 (minisat+_script) S 16379 16380 4419 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1844176082 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/16380/statm): 531 226 485 147 0 384 0 [pid=16380] vsize: 2124 Raw data (/proc/16384/stat): 16384 (minisat+_64-bit) R 16380 16380 4419 0 -1 0 6508 0 0 0 23891 47 0 0 25 0 1 0 1844176087 27729920 6403 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/16384/statm): 6770 6403 145 145 0 6625 0 [pid=16384] vsize: 27080 Current children cumulated CPU time (s) 239.39 Current children cumulated vsize (Kb) 29204 [startup+250.025 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 16384 Raw data (/proc/16380/stat): 16380 (minisat+_script) S 16379 16380 4419 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1844176082 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/16380/statm): 531 226 485 147 0 384 0 [pid=16380] vsize: 2124 Raw data (/proc/16384/stat): 16384 (minisat+_64-bit) R 16380 16380 4419 0 -1 0 6508 0 0 0 24891 48 0 0 25 0 1 0 1844176087 27729920 6403 4294967295 134512640 135094434 3221224432 3221223024 134557236 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/16384/statm): 6770 6403 145 145 0 6625 0 [pid=16384] vsize: 27080 Current children cumulated CPU time (s) 249.4 Current children cumulated vsize (Kb) 29204 [startup+260.025 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 16384 Raw data (/proc/16380/stat): 16380 (minisat+_script) S 16379 16380 4419 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1844176082 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/16380/statm): 531 226 485 147 0 384 0 [pid=16380] vsize: 2124 Raw data (/proc/16384/stat): 16384 (minisat+_64-bit) R 16380 16380 4419 0 -1 0 6508 0 0 0 25890 48 0 0 25 0 1 0 1844176087 27729920 6403 4294967295 134512640 135094434 3221224432 3221223104 134555953 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/16384/statm): 6770 6403 145 145 0 6625 0 [pid=16384] vsize: 27080 Current children cumulated CPU time (s) 259.39 Current children cumulated vsize (Kb) 29204 [startup+270.026 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 16384 Raw data (/proc/16380/stat): 16380 (minisat+_script) S 16379 16380 4419 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1844176082 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/16380/statm): 531 226 485 147 0 384 0 [pid=16380] vsize: 2124 Raw data (/proc/16384/stat): 16384 (minisat+_64-bit) R 16380 16380 4419 0 -1 0 6508 0 0 0 26889 49 0 0 25 0 1 0 1844176087 27729920 6403 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/16384/statm): 6770 6403 145 145 0 6625 0 [pid=16384] vsize: 27080 Current children cumulated CPU time (s) 269.39 Current children cumulated vsize (Kb) 29204 [startup+280.027 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 16384 Raw data (/proc/16380/stat): 16380 (minisat+_script) S 16379 16380 4419 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1844176082 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/16380/statm): 531 226 485 147 0 384 0 [pid=16380] vsize: 2124 Raw data (/proc/16384/stat): 16384 (minisat+_64-bit) R 16380 16380 4419 0 -1 0 6810 0 0 0 27884 51 0 0 25 0 1 0 1844176087 28966912 6705 4294967295 134512640 135094434 3221224432 3221223088 134558153 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/16384/statm): 7072 6705 145 145 0 6927 0 [pid=16384] vsize: 28288 Current children cumulated CPU time (s) 279.36 Current children cumulated vsize (Kb) 30412 [startup+290.027 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 16384 Raw data (/proc/16380/stat): 16380 (minisat+_script) S 16379 16380 4419 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1844176082 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/16380/statm): 531 226 485 147 0 384 0 [pid=16380] vsize: 2124 Raw data (/proc/16384/stat): 16384 (minisat+_64-bit) R 16380 16380 4419 0 -1 0 7345 0 0 0 28874 55 0 0 25 0 1 0 1844176087 31162368 7240 4294967295 134512640 135094434 3221224432 3221223088 134558235 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/16384/statm): 7608 7240 145 145 0 7463 0 [pid=16384] vsize: 30432 Current children cumulated CPU time (s) 289.3 Current children cumulated vsize (Kb) 32556 [startup+300.028 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 16384 Raw data (/proc/16380/stat): 16380 (minisat+_script) S 16379 16380 4419 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1844176082 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/16380/statm): 531 226 485 147 0 384 0 [pid=16380] vsize: 2124 Raw data (/proc/16384/stat): 16384 (minisat+_64-bit) R 16380 16380 4419 0 -1 0 7839 0 0 0 29865 59 0 0 25 0 1 0 1844176087 33189888 7734 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/16384/statm): 8103 7734 145 145 0 7958 0 [pid=16384] vsize: 32412 Current children cumulated CPU time (s) 299.25 Current children cumulated vsize (Kb) 34536 [startup+310.028 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 16384 Raw data (/proc/16380/stat): 16380 (minisat+_script) S 16379 16380 4419 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1844176082 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/16380/statm): 531 226 485 147 0 384 0 [pid=16380] vsize: 2124 Raw data (/proc/16384/stat): 16384 (minisat+_64-bit) R 16380 16380 4419 0 -1 0 8238 0 0 0 30857 62 0 0 25 0 1 0 1844176087 34832384 8133 4294967295 134512640 135094434 3221224432 3221223088 134557911 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/16384/statm): 8504 8133 145 145 0 8359 0 [pid=16384] vsize: 34016 Current children cumulated CPU time (s) 309.2 Current children cumulated vsize (Kb) 36140 [startup+320.03 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 16384 Raw data (/proc/16380/stat): 16380 (minisat+_script) S 16379 16380 4419 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1844176082 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/16380/statm): 531 226 485 147 0 384 0 [pid=16380] vsize: 2124 Raw data (/proc/16384/stat): 16384 (minisat+_64-bit) R 16380 16380 4419 0 -1 0 8630 0 0 0 31850 66 0 0 25 0 1 0 1844176087 36450304 8525 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/16384/statm): 8899 8525 145 145 0 8754 0 [pid=16384] vsize: 35596 Current children cumulated CPU time (s) 319.17 Current children cumulated vsize (Kb) 37720 [startup+330.031 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 16384 Raw data (/proc/16380/stat): 16380 (minisat+_script) S 16379 16380 4419 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1844176082 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/16380/statm): 531 226 485 147 0 384 0 [pid=16380] vsize: 2124 Raw data (/proc/16384/stat): 16384 (minisat+_64-bit) R 16380 16380 4419 0 -1 0 9159 0 0 0 32839 71 0 0 25 0 1 0 1844176087 38617088 9054 4294967295 134512640 135094434 3221224432 3221223104 134556394 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/16384/statm): 9428 9054 145 145 0 9283 0 [pid=16384] vsize: 37712 Current children cumulated CPU time (s) 329.11 Current children cumulated vsize (Kb) 39836 [startup+340.031 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 16384 Raw data (/proc/16380/stat): 16380 (minisat+_script) S 16379 16380 4419 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1844176082 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/16380/statm): 531 226 485 147 0 384 0 [pid=16380] vsize: 2124 Raw data (/proc/16384/stat): 16384 (minisat+_64-bit) R 16380 16380 4419 0 -1 0 9522 0 0 0 33831 74 0 0 25 0 1 0 1844176087 40095744 9417 4294967295 134512640 135094434 3221224432 3221223088 134557884 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/16384/statm): 9789 9417 145 145 0 9644 0 [pid=16384] vsize: 39156 Current children cumulated CPU time (s) 339.06 Current children cumulated vsize (Kb) 41280 [startup+350.032 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 16384 Raw data (/proc/16380/stat): 16380 (minisat+_script) S 16379 16380 4419 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1844176082 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/16380/statm): 531 226 485 147 0 384 0 [pid=16380] vsize: 2124 Raw data (/proc/16384/stat): 16384 (minisat+_64-bit) R 16380 16380 4419 0 -1 0 9872 0 0 0 34825 77 0 0 25 0 1 0 1844176087 41521152 9767 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/16384/statm): 10137 9767 145 145 0 9992 0 [pid=16384] vsize: 40548 Current children cumulated CPU time (s) 349.03 Current children cumulated vsize (Kb) 42672 [startup+360.032 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 16384 Raw data (/proc/16380/stat): 16380 (minisat+_script) S 16379 16380 4419 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1844176082 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/16380/statm): 531 226 485 147 0 384 0 [pid=16380] vsize: 2124 Raw data (/proc/16384/stat): 16384 (minisat+_64-bit) R 16380 16380 4419 0 -1 0 10173 0 0 0 35818 80 0 0 25 0 1 0 1844176087 42741760 10068 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/16384/statm): 10435 10068 145 145 0 10290 0 [pid=16384] vsize: 41740 Current children cumulated CPU time (s) 358.99 Current children cumulated vsize (Kb) 43864 [startup+370.034 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 16384 Raw data (/proc/16380/stat): 16380 (minisat+_script) S 16379 16380 4419 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1844176082 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/16380/statm): 531 226 485 147 0 384 0 [pid=16380] vsize: 2124 Raw data (/proc/16384/stat): 16384 (minisat+_64-bit) R 16380 16380 4419 0 -1 0 10173 0 0 0 36818 80 0 0 25 0 1 0 1844176087 42741760 10068 4294967295 134512640 135094434 3221224432 3221223056 134557669 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/16384/statm): 10435 10068 145 145 0 10290 0 [pid=16384] vsize: 41740 Current children cumulated CPU time (s) 368.99 Current children cumulated vsize (Kb) 43864 [startup+380.035 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 16384 Raw data (/proc/16380/stat): 16380 (minisat+_script) S 16379 16380 4419 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1844176082 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/16380/statm): 531 226 485 147 0 384 0 [pid=16380] vsize: 2124 Raw data (/proc/16384/stat): 16384 (minisat+_64-bit) R 16380 16380 4419 0 -1 0 10173 0 0 0 37817 80 0 0 25 0 1 0 1844176087 42741760 10068 4294967295 134512640 135094434 3221224432 3221223104 134555943 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/16384/statm): 10435 10068 145 145 0 10290 0 [pid=16384] vsize: 41740 Current children cumulated CPU time (s) 378.98 Current children cumulated vsize (Kb) 43864 [startup+390.034 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 16384 Raw data (/proc/16380/stat): 16380 (minisat+_script) S 16379 16380 4419 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1844176082 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/16380/statm): 531 226 485 147 0 384 0 [pid=16380] vsize: 2124 Raw data (/proc/16384/stat): 16384 (minisat+_64-bit) R 16380 16380 4419 0 -1 0 10173 0 0 0 38816 81 0 0 25 0 1 0 1844176087 42741760 10068 4294967295 134512640 135094434 3221224432 3221223088 134558208 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/16384/statm): 10435 10068 145 145 0 10290 0 [pid=16384] vsize: 41740 Current children cumulated CPU time (s) 388.98 Current children cumulated vsize (Kb) 43864 [startup+400.036 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 16384 Raw data (/proc/16380/stat): 16380 (minisat+_script) S 16379 16380 4419 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1844176082 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/16380/statm): 531 226 485 147 0 384 0 [pid=16380] vsize: 2124 Raw data (/proc/16384/stat): 16384 (minisat+_64-bit) R 16380 16380 4419 0 -1 0 10173 0 0 0 39816 81 0 0 25 0 1 0 1844176087 42741760 10068 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/16384/statm): 10435 10068 145 145 0 10290 0 [pid=16384] vsize: 41740 Current children cumulated CPU time (s) 398.98 Current children cumulated vsize (Kb) 43864 [startup+410.036 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 16384 Raw data (/proc/16380/stat): 16380 (minisat+_script) S 16379 16380 4419 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1844176082 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/16380/statm): 531 226 485 147 0 384 0 [pid=16380] vsize: 2124 Raw data (/proc/16384/stat): 16384 (minisat+_64-bit) R 16380 16380 4419 0 -1 0 10173 0 0 0 40816 82 0 0 25 0 1 0 1844176087 42741760 10068 4294967295 134512640 135094434 3221224432 3221223024 134557319 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/16384/statm): 10435 10068 145 145 0 10290 0 [pid=16384] vsize: 41740 Current children cumulated CPU time (s) 408.99 Current children cumulated vsize (Kb) 43864 [startup+420.038 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 16384 Raw data (/proc/16380/stat): 16380 (minisat+_script) S 16379 16380 4419 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1844176082 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/16380/statm): 531 226 485 147 0 384 0 [pid=16380] vsize: 2124 Raw data (/proc/16384/stat): 16384 (minisat+_64-bit) R 16380 16380 4419 0 -1 0 10173 0 0 0 41815 82 0 0 25 0 1 0 1844176087 42741760 10068 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/16384/statm): 10435 10068 145 145 0 10290 0 [pid=16384] vsize: 41740 Current children cumulated CPU time (s) 418.98 Current children cumulated vsize (Kb) 43864 [startup+430.04 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 16384 Raw data (/proc/16380/stat): 16380 (minisat+_script) S 16379 16380 4419 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1844176082 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/16380/statm): 531 226 485 147 0 384 0 [pid=16380] vsize: 2124 Raw data (/proc/16384/stat): 16384 (minisat+_64-bit) R 16380 16380 4419 0 -1 0 10173 0 0 0 42815 83 0 0 25 0 1 0 1844176087 42741760 10068 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/16384/statm): 10435 10068 145 145 0 10290 0 [pid=16384] vsize: 41740 Current children cumulated CPU time (s) 428.99 Current children cumulated vsize (Kb) 43864 [startup+440.04 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 16384 Raw data (/proc/16380/stat): 16380 (minisat+_script) S 16379 16380 4419 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1844176082 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/16380/statm): 531 226 485 147 0 384 0 [pid=16380] vsize: 2124 Raw data (/proc/16384/stat): 16384 (minisat+_64-bit) R 16380 16380 4419 0 -1 0 10173 0 0 0 43814 83 0 0 25 0 1 0 1844176087 42741760 10068 4294967295 134512640 135094434 3221224432 3221223088 134557945 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/16384/statm): 10435 10068 145 145 0 10290 0 [pid=16384] vsize: 41740 Current children cumulated CPU time (s) 438.98 Current children cumulated vsize (Kb) 43864 [startup+450.041 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 16384 Raw data (/proc/16380/stat): 16380 (minisat+_script) S 16379 16380 4419 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1844176082 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/16380/statm): 531 226 485 147 0 384 0 [pid=16380] vsize: 2124 Raw data (/proc/16384/stat): 16384 (minisat+_64-bit) R 16380 16380 4419 0 -1 0 10173 0 0 0 44814 84 0 0 25 0 1 0 1844176087 42741760 10068 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/16384/statm): 10435 10068 145 145 0 10290 0 [pid=16384] vsize: 41740 Current children cumulated CPU time (s) 448.99 Current children cumulated vsize (Kb) 43864 [startup+460.041 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 16384 Raw data (/proc/16380/stat): 16380 (minisat+_script) S 16379 16380 4419 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1844176082 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/16380/statm): 531 226 485 147 0 384 0 [pid=16380] vsize: 2124 Raw data (/proc/16384/stat): 16384 (minisat+_64-bit) R 16380 16380 4419 0 -1 0 10173 0 0 0 45814 84 0 0 25 0 1 0 1844176087 42741760 10068 4294967295 134512640 135094434 3221224432 3221223024 134557180 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/16384/statm): 10435 10068 145 145 0 10290 0 [pid=16384] vsize: 41740 Current children cumulated CPU time (s) 458.99 Current children cumulated vsize (Kb) 43864 [startup+470.043 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 16384 Raw data (/proc/16380/stat): 16380 (minisat+_script) S 16379 16380 4419 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1844176082 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/16380/statm): 531 226 485 147 0 384 0 [pid=16380] vsize: 2124 Raw data (/proc/16384/stat): 16384 (minisat+_64-bit) R 16380 16380 4419 0 -1 0 10173 0 0 0 46813 84 0 0 25 0 1 0 1844176087 42741760 10068 4294967295 134512640 135094434 3221224432 3221223088 134558210 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/16384/statm): 10435 10068 145 145 0 10290 0 [pid=16384] vsize: 41740 Current children cumulated CPU time (s) 468.98 Current children cumulated vsize (Kb) 43864 [startup+480.044 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 16384 Raw data (/proc/16380/stat): 16380 (minisat+_script) S 16379 16380 4419 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1844176082 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/16380/statm): 531 226 485 147 0 384 0 [pid=16380] vsize: 2124 Raw data (/proc/16384/stat): 16384 (minisat+_64-bit) R 16380 16380 4419 0 -1 0 10173 0 0 0 47813 85 0 0 25 0 1 0 1844176087 42741760 10068 4294967295 134512640 135094434 3221224432 3221223088 134557882 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/16384/statm): 10435 10068 145 145 0 10290 0 [pid=16384] vsize: 41740 Current children cumulated CPU time (s) 478.99 Current children cumulated vsize (Kb) 43864 [startup+490.044 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 16384 Raw data (/proc/16380/stat): 16380 (minisat+_script) S 16379 16380 4419 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1844176082 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/16380/statm): 531 226 485 147 0 384 0 [pid=16380] vsize: 2124 Raw data (/proc/16384/stat): 16384 (minisat+_64-bit) R 16380 16380 4419 0 -1 0 10173 0 0 0 48813 85 0 0 25 0 1 0 1844176087 42741760 10068 4294967295 134512640 135094434 3221224432 3221223104 134556068 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/16384/statm): 10435 10068 145 145 0 10290 0 [pid=16384] vsize: 41740 Current children cumulated CPU time (s) 488.99 Current children cumulated vsize (Kb) 43864 [startup+500.046 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 16384 Raw data (/proc/16380/stat): 16380 (minisat+_script) S 16379 16380 4419 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1844176082 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/16380/statm): 531 226 485 147 0 384 0 [pid=16380] vsize: 2124 Raw data (/proc/16384/stat): 16384 (minisat+_64-bit) R 16380 16380 4419 0 -1 0 10173 0 0 0 49813 85 0 0 25 0 1 0 1844176087 42741760 10068 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/16384/statm): 10435 10068 145 145 0 10290 0 [pid=16384] vsize: 41740 Current children cumulated CPU time (s) 498.99 Current children cumulated vsize (Kb) 43864 [startup+510.046 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 16384 Raw data (/proc/16380/stat): 16380 (minisat+_script) S 16379 16380 4419 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1844176082 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/16380/statm): 531 226 485 147 0 384 0 [pid=16380] vsize: 2124 Raw data (/proc/16384/stat): 16384 (minisat+_64-bit) R 16380 16380 4419 0 -1 0 10173 0 0 0 50812 85 0 0 25 0 1 0 1844176087 42741760 10068 4294967295 134512640 135094434 3221224432 3221223088 134558159 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/16384/statm): 10435 10068 145 145 0 10290 0 [pid=16384] vsize: 41740 Current children cumulated CPU time (s) 508.98 Current children cumulated vsize (Kb) 43864 [startup+520.048 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 16384 Raw data (/proc/16380/stat): 16380 (minisat+_script) S 16379 16380 4419 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1844176082 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/16380/statm): 531 226 485 147 0 384 0 [pid=16380] vsize: 2124 Raw data (/proc/16384/stat): 16384 (minisat+_64-bit) R 16380 16380 4419 0 -1 0 10370 0 0 0 51809 87 0 0 25 0 1 0 1844176087 43569152 10265 4294967295 134512640 135094434 3221224432 3221223088 134558235 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/16384/statm): 10637 10265 145 145 0 10492 0 [pid=16384] vsize: 42548 Current children cumulated CPU time (s) 518.97 Current children cumulated vsize (Kb) 44672 [startup+530.049 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 16384 Raw data (/proc/16380/stat): 16380 (minisat+_script) S 16379 16380 4419 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1844176082 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/16380/statm): 531 226 485 147 0 384 0 [pid=16380] vsize: 2124 Raw data (/proc/16384/stat): 16384 (minisat+_64-bit) R 16380 16380 4419 0 -1 0 10646 0 0 0 52803 90 0 0 25 0 1 0 1844176087 44699648 10541 4294967295 134512640 135094434 3221224432 3221223088 134558011 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/16384/statm): 10913 10541 145 145 0 10768 0 [pid=16384] vsize: 43652 Current children cumulated CPU time (s) 528.94 Current children cumulated vsize (Kb) 45776 [startup+540.049 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 16384 Raw data (/proc/16380/stat): 16380 (minisat+_script) S 16379 16380 4419 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1844176082 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/16380/statm): 531 226 485 147 0 384 0 [pid=16380] vsize: 2124 Raw data (/proc/16384/stat): 16384 (minisat+_64-bit) R 16380 16380 4419 0 -1 0 10910 0 0 0 53797 92 0 0 25 0 1 0 1844176087 45780992 10805 4294967295 134512640 135094434 3221224432 3221223104 134556487 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/16384/statm): 11177 10805 145 145 0 11032 0 [pid=16384] vsize: 44708 Current children cumulated CPU time (s) 538.9 Current children cumulated vsize (Kb) 46832 [startup+550.05 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 16384 Raw data (/proc/16380/stat): 16380 (minisat+_script) S 16379 16380 4419 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1844176082 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/16380/statm): 531 226 485 147 0 384 0 [pid=16380] vsize: 2124 Raw data (/proc/16384/stat): 16384 (minisat+_64-bit) R 16380 16380 4419 0 -1 0 11172 0 0 0 54793 94 0 0 25 0 1 0 1844176087 46850048 11067 4294967295 134512640 135094434 3221224432 3221223056 134557737 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/16384/statm): 11438 11067 145 145 0 11293 0 [pid=16384] vsize: 45752 Current children cumulated CPU time (s) 548.88 Current children cumulated vsize (Kb) 47876 [startup+560.05 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 16384 Raw data (/proc/16380/stat): 16380 (minisat+_script) S 16379 16380 4419 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1844176082 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/16380/statm): 531 226 485 147 0 384 0 [pid=16380] vsize: 2124 Raw data (/proc/16384/stat): 16384 (minisat+_64-bit) R 16380 16380 4419 0 -1 0 11437 0 0 0 55787 97 0 0 25 0 1 0 1844176087 47935488 11332 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/16384/statm): 11703 11332 145 145 0 11558 0 [pid=16384] vsize: 46812 Current children cumulated CPU time (s) 558.85 Current children cumulated vsize (Kb) 48936 [startup+570.052 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 16384 Raw data (/proc/16380/stat): 16380 (minisat+_script) S 16379 16380 4419 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1844176082 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/16380/statm): 531 226 485 147 0 384 0 [pid=16380] vsize: 2124 Raw data (/proc/16384/stat): 16384 (minisat+_64-bit) R 16380 16380 4419 0 -1 0 11708 0 0 0 56782 99 0 0 25 0 1 0 1844176087 49029120 11603 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/16384/statm): 11970 11603 145 145 0 11825 0 [pid=16384] vsize: 47880 Current children cumulated CPU time (s) 568.82 Current children cumulated vsize (Kb) 50004 [startup+580.053 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 16384 Raw data (/proc/16380/stat): 16380 (minisat+_script) S 16379 16380 4419 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1844176082 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/16380/statm): 531 226 485 147 0 384 0 [pid=16380] vsize: 2124 Raw data (/proc/16384/stat): 16384 (minisat+_64-bit) R 16380 16380 4419 0 -1 0 11907 0 0 0 57779 101 0 0 25 0 1 0 1844176087 49909760 11802 4294967295 134512640 135094434 3221224432 3221223024 134557219 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/16384/statm): 12185 11802 145 145 0 12040 0 [pid=16384] vsize: 48740 Current children cumulated CPU time (s) 578.81 Current children cumulated vsize (Kb) 50864 [startup+590.052 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 16384 Raw data (/proc/16380/stat): 16380 (minisat+_script) S 16379 16380 4419 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1844176082 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/16380/statm): 531 226 485 147 0 384 0 [pid=16380] vsize: 2124 Raw data (/proc/16384/stat): 16384 (minisat+_64-bit) R 16380 16380 4419 0 -1 0 12029 0 0 0 58777 102 0 0 25 0 1 0 1844176087 50397184 11924 4294967295 134512640 135094434 3221224432 3221223088 134558007 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/16384/statm): 12304 11924 145 145 0 12159 0 [pid=16384] vsize: 49216 Current children cumulated CPU time (s) 588.8 Current children cumulated vsize (Kb) 51340 [startup+600.053 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 16384 Raw data (/proc/16380/stat): 16380 (minisat+_script) S 16379 16380 4419 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1844176082 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/16380/statm): 531 226 485 147 0 384 0 [pid=16380] vsize: 2124 Raw data (/proc/16384/stat): 16384 (minisat+_64-bit) R 16380 16380 4419 0 -1 0 12187 0 0 0 59774 104 0 0 25 0 1 0 1844176087 51032064 12082 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/16384/statm): 12459 12082 145 145 0 12314 0 [pid=16384] vsize: 49836 Current children cumulated CPU time (s) 598.79 Current children cumulated vsize (Kb) 51960 [startup+610.053 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 16384 Raw data (/proc/16380/stat): 16380 (minisat+_script) S 16379 16380 4419 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1844176082 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/16380/statm): 531 226 485 147 0 384 0 [pid=16380] vsize: 2124 Raw data (/proc/16384/stat): 16384 (minisat+_64-bit) R 16380 16380 4419 0 -1 0 12381 0 0 0 60771 105 0 0 25 0 1 0 1844176087 51814400 12276 4294967295 134512640 135094434 3221224432 3221223088 134557893 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/16384/statm): 12650 12276 145 145 0 12505 0 [pid=16384] vsize: 50600 Current children cumulated CPU time (s) 608.77 Current children cumulated vsize (Kb) 52724 [startup+620.054 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 16384 Raw data (/proc/16380/stat): 16380 (minisat+_script) S 16379 16380 4419 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1844176082 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/16380/statm): 531 226 485 147 0 384 0 [pid=16380] vsize: 2124 Raw data (/proc/16384/stat): 16384 (minisat+_64-bit) R 16380 16380 4419 0 -1 0 12691 0 0 0 61766 108 0 0 25 0 1 0 1844176087 53071872 12586 4294967295 134512640 135094434 3221224432 3221221088 134562642 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/16384/statm): 12957 12586 145 145 0 12812 0 [pid=16384] vsize: 51828 Current children cumulated CPU time (s) 618.75 Current children cumulated vsize (Kb) 53952 [startup+630.055 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 16384 Raw data (/proc/16380/stat): 16380 (minisat+_script) S 16379 16380 4419 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1844176082 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/16380/statm): 531 226 485 147 0 384 0 [pid=16380] vsize: 2124 Raw data (/proc/16384/stat): 16384 (minisat+_64-bit) R 16380 16380 4419 0 -1 0 12691 0 0 0 62765 108 0 0 25 0 1 0 1844176087 53071872 12586 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/16384/statm): 12957 12586 145 145 0 12812 0 [pid=16384] vsize: 51828 Current children cumulated CPU time (s) 628.74 Current children cumulated vsize (Kb) 53952 [startup+640.055 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 16384 Raw data (/proc/16380/stat): 16380 (minisat+_script) S 16379 16380 4419 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1844176082 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/16380/statm): 531 226 485 147 0 384 0 [pid=16380] vsize: 2124 Raw data (/proc/16384/stat): 16384 (minisat+_64-bit) R 16380 16380 4419 0 -1 0 12691 0 0 0 63765 108 0 0 25 0 1 0 1844176087 53071872 12586 4294967295 134512640 135094434 3221224432 3221223088 134558208 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/16384/statm): 12957 12586 145 145 0 12812 0 [pid=16384] vsize: 51828 Current children cumulated CPU time (s) 638.74 Current children cumulated vsize (Kb) 53952 [startup+650.056 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 16384 Raw data (/proc/16380/stat): 16380 (minisat+_script) S 16379 16380 4419 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1844176082 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/16380/statm): 531 226 485 147 0 384 0 [pid=16380] vsize: 2124 Raw data (/proc/16384/stat): 16384 (minisat+_64-bit) R 16380 16380 4419 0 -1 0 12691 0 0 0 64765 108 0 0 25 0 1 0 1844176087 53071872 12586 4294967295 134512640 135094434 3221224432 3221223024 134557230 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/16384/statm): 12957 12586 145 145 0 12812 0 [pid=16384] vsize: 51828 Current children cumulated CPU time (s) 648.74 Current children cumulated vsize (Kb) 53952 [startup+660.056 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 16384 Raw data (/proc/16380/stat): 16380 (minisat+_script) S 16379 16380 4419 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1844176082 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/16380/statm): 531 226 485 147 0 384 0 [pid=16380] vsize: 2124 Raw data (/proc/16384/stat): 16384 (minisat+_64-bit) R 16380 16380 4419 0 -1 0 12691 0 0 0 65765 108 0 0 25 0 1 0 1844176087 53071872 12586 4294967295 134512640 135094434 3221224432 3221223104 134555855 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/16384/statm): 12957 12586 145 145 0 12812 0 [pid=16384] vsize: 51828 Current children cumulated CPU time (s) 658.74 Current children cumulated vsize (Kb) 53952 [startup+670.058 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 16384 Raw data (/proc/16380/stat): 16380 (minisat+_script) S 16379 16380 4419 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1844176082 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/16380/statm): 531 226 485 147 0 384 0 [pid=16380] vsize: 2124 Raw data (/proc/16384/stat): 16384 (minisat+_64-bit) R 16380 16380 4419 0 -1 0 12691 0 0 0 66764 109 0 0 25 0 1 0 1844176087 53071872 12586 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/16384/statm): 12957 12586 145 145 0 12812 0 [pid=16384] vsize: 51828 Current children cumulated CPU time (s) 668.74 Current children cumulated vsize (Kb) 53952 [startup+680.059 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 16384 Raw data (/proc/16380/stat): 16380 (minisat+_script) S 16379 16380 4419 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1844176082 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/16380/statm): 531 226 485 147 0 384 0 [pid=16380] vsize: 2124 Raw data (/proc/16384/stat): 16384 (minisat+_64-bit) R 16380 16380 4419 0 -1 0 12691 0 0 0 67764 109 0 0 25 0 1 0 1844176087 53071872 12586 4294967295 134512640 135094434 3221224432 3221223056 134557717 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/16384/statm): 12957 12586 145 145 0 12812 0 [pid=16384] vsize: 51828 Current children cumulated CPU time (s) 678.74 Current children cumulated vsize (Kb) 53952 [startup+690.058 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 16384 Raw data (/proc/16380/stat): 16380 (minisat+_script) S 16379 16380 4419 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1844176082 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/16380/statm): 531 226 485 147 0 384 0 [pid=16380] vsize: 2124 Raw data (/proc/16384/stat): 16384 (minisat+_64-bit) R 16380 16380 4419 0 -1 0 12691 0 0 0 68764 109 0 0 25 0 1 0 1844176087 53071872 12586 4294967295 134512640 135094434 3221224432 3221223024 134557339 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/16384/statm): 12957 12586 145 145 0 12812 0 [pid=16384] vsize: 51828 Current children cumulated CPU time (s) 688.74 Current children cumulated vsize (Kb) 53952 [startup+700.059 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 16384 Raw data (/proc/16380/stat): 16380 (minisat+_script) S 16379 16380 4419 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1844176082 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/16380/statm): 531 226 485 147 0 384 0 [pid=16380] vsize: 2124 Raw data (/proc/16384/stat): 16384 (minisat+_64-bit) R 16380 16380 4419 0 -1 0 12691 0 0 0 69763 110 0 0 25 0 1 0 1844176087 53071872 12586 4294967295 134512640 135094434 3221224432 3221223024 134557518 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/16384/statm): 12957 12586 145 145 0 12812 0 [pid=16384] vsize: 51828 Current children cumulated CPU time (s) 698.74 Current children cumulated vsize (Kb) 53952 [startup+710.059 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 16384 Raw data (/proc/16380/stat): 16380 (minisat+_script) S 16379 16380 4419 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1844176082 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/16380/statm): 531 226 485 147 0 384 0 [pid=16380] vsize: 2124 Raw data (/proc/16384/stat): 16384 (minisat+_64-bit) R 16380 16380 4419 0 -1 0 12691 0 0 0 70763 110 0 0 25 0 1 0 1844176087 53071872 12586 4294967295 134512640 135094434 3221224432 3221223024 134557175 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/16384/statm): 12957 12586 145 145 0 12812 0 [pid=16384] vsize: 51828 Current children cumulated CPU time (s) 708.74 Current children cumulated vsize (Kb) 53952 [startup+720.061 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 16384 Raw data (/proc/16380/stat): 16380 (minisat+_script) S 16379 16380 4419 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1844176082 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/16380/statm): 531 226 485 147 0 384 0 [pid=16380] vsize: 2124 Raw data (/proc/16384/stat): 16384 (minisat+_64-bit) R 16380 16380 4419 0 -1 0 12691 0 0 0 71762 110 0 0 25 0 1 0 1844176087 53071872 12586 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/16384/statm): 12957 12586 145 145 0 12812 0 [pid=16384] vsize: 51828 Current children cumulated CPU time (s) 718.73 Current children cumulated vsize (Kb) 53952 [startup+730.062 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 16384 Raw data (/proc/16380/stat): 16380 (minisat+_script) S 16379 16380 4419 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1844176082 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/16380/statm): 531 226 485 147 0 384 0 [pid=16380] vsize: 2124 Raw data (/proc/16384/stat): 16384 (minisat+_64-bit) R 16380 16380 4419 0 -1 0 12691 0 0 0 72762 111 0 0 25 0 1 0 1844176087 53071872 12586 4294967295 134512640 135094434 3221224432 3221223024 134556931 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/16384/statm): 12957 12586 145 145 0 12812 0 [pid=16384] vsize: 51828 Current children cumulated CPU time (s) 728.74 Current children cumulated vsize (Kb) 53952 [startup+740.062 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 16384 Raw data (/proc/16380/stat): 16380 (minisat+_script) S 16379 16380 4419 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1844176082 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/16380/statm): 531 226 485 147 0 384 0 [pid=16380] vsize: 2124 Raw data (/proc/16384/stat): 16384 (minisat+_64-bit) R 16380 16380 4419 0 -1 0 12691 0 0 0 73762 111 0 0 25 0 1 0 1844176087 53071872 12586 4294967295 134512640 135094434 3221224432 3221223024 134557528 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/16384/statm): 12957 12586 145 145 0 12812 0 [pid=16384] vsize: 51828 Current children cumulated CPU time (s) 738.74 Current children cumulated vsize (Kb) 53952 [startup+750.063 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 16384 Raw data (/proc/16380/stat): 16380 (minisat+_script) S 16379 16380 4419 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1844176082 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/16380/statm): 531 226 485 147 0 384 0 [pid=16380] vsize: 2124 Raw data (/proc/16384/stat): 16384 (minisat+_64-bit) R 16380 16380 4419 0 -1 0 12691 0 0 0 74762 111 0 0 25 0 1 0 1844176087 53071872 12586 4294967295 134512640 135094434 3221224432 3221223024 134557518 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/16384/statm): 12957 12586 145 145 0 12812 0 [pid=16384] vsize: 51828 Current children cumulated CPU time (s) 748.74 Current children cumulated vsize (Kb) 53952 [startup+760.063 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 16384 Raw data (/proc/16380/stat): 16380 (minisat+_script) S 16379 16380 4419 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1844176082 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/16380/statm): 531 226 485 147 0 384 0 [pid=16380] vsize: 2124 Raw data (/proc/16384/stat): 16384 (minisat+_64-bit) R 16380 16380 4419 0 -1 0 12691 0 0 0 75761 112 0 0 25 0 1 0 1844176087 53071872 12586 4294967295 134512640 135094434 3221224432 3221223024 134557230 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/16384/statm): 12957 12586 145 145 0 12812 0 [pid=16384] vsize: 51828 Current children cumulated CPU time (s) 758.74 Current children cumulated vsize (Kb) 53952 [startup+770.065 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 16384 Raw data (/proc/16380/stat): 16380 (minisat+_script) S 16379 16380 4419 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1844176082 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/16380/statm): 531 226 485 147 0 384 0 [pid=16380] vsize: 2124 Raw data (/proc/16384/stat): 16384 (minisat+_64-bit) R 16380 16380 4419 0 -1 0 12691 0 0 0 76761 112 0 0 25 0 1 0 1844176087 53071872 12586 4294967295 134512640 135094434 3221224432 3221223088 134558159 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/16384/statm): 12957 12586 145 145 0 12812 0 [pid=16384] vsize: 51828 Current children cumulated CPU time (s) 768.74 Current children cumulated vsize (Kb) 53952 [startup+780.067 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 16384 Raw data (/proc/16380/stat): 16380 (minisat+_script) S 16379 16380 4419 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1844176082 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/16380/statm): 531 226 485 147 0 384 0 [pid=16380] vsize: 2124 Raw data (/proc/16384/stat): 16384 (minisat+_64-bit) R 16380 16380 4419 0 -1 0 12691 0 0 0 77761 112 0 0 25 0 1 0 1844176087 53071872 12586 4294967295 134512640 135094434 3221224432 3221223024 134556928 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/16384/statm): 12957 12586 145 145 0 12812 0 [pid=16384] vsize: 51828 Current children cumulated CPU time (s) 778.74 Current children cumulated vsize (Kb) 53952 [startup+790.067 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 16384 Raw data (/proc/16380/stat): 16380 (minisat+_script) S 16379 16380 4419 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1844176082 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/16380/statm): 531 226 485 147 0 384 0 [pid=16380] vsize: 2124 Raw data (/proc/16384/stat): 16384 (minisat+_64-bit) R 16380 16380 4419 0 -1 0 12691 0 0 0 78761 112 0 0 25 0 1 0 1844176087 53071872 12586 4294967295 134512640 135094434 3221224432 3221223024 134556862 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/16384/statm): 12957 12586 145 145 0 12812 0 [pid=16384] vsize: 51828 Current children cumulated CPU time (s) 788.74 Current children cumulated vsize (Kb) 53952 [startup+800.068 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 16384 Raw data (/proc/16380/stat): 16380 (minisat+_script) S 16379 16380 4419 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1844176082 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/16380/statm): 531 226 485 147 0 384 0 [pid=16380] vsize: 2124 Raw data (/proc/16384/stat): 16384 (minisat+_64-bit) R 16380 16380 4419 0 -1 0 12691 0 0 0 79760 113 0 0 25 0 1 0 1844176087 53071872 12586 4294967295 134512640 135094434 3221224432 3221223024 134556987 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/16384/statm): 12957 12586 145 145 0 12812 0 [pid=16384] vsize: 51828 Current children cumulated CPU time (s) 798.74 Current children cumulated vsize (Kb) 53952 [startup+810.068 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 16384 Raw data (/proc/16380/stat): 16380 (minisat+_script) S 16379 16380 4419 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1844176082 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/16380/statm): 531 226 485 147 0 384 0 [pid=16380] vsize: 2124 Raw data (/proc/16384/stat): 16384 (minisat+_64-bit) R 16380 16380 4419 0 -1 0 12691 0 0 0 80760 113 0 0 25 0 1 0 1844176087 53071872 12586 4294967295 134512640 135094434 3221224432 3221223024 134557219 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/16384/statm): 12957 12586 145 145 0 12812 0 [pid=16384] vsize: 51828 Current children cumulated CPU time (s) 808.74 Current children cumulated vsize (Kb) 53952 [startup+820.07 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 16384 Raw data (/proc/16380/stat): 16380 (minisat+_script) S 16379 16380 4419 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1844176082 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/16380/statm): 531 226 485 147 0 384 0 [pid=16380] vsize: 2124 Raw data (/proc/16384/stat): 16384 (minisat+_64-bit) R 16380 16380 4419 0 -1 0 12691 0 0 0 81760 113 0 0 25 0 1 0 1844176087 53071872 12586 4294967295 134512640 135094434 3221224432 3221223088 134558178 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/16384/statm): 12957 12586 145 145 0 12812 0 [pid=16384] vsize: 51828 Current children cumulated CPU time (s) 818.74 Current children cumulated vsize (Kb) 53952 [startup+830.071 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 16384 Raw data (/proc/16380/stat): 16380 (minisat+_script) S 16379 16380 4419 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1844176082 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/16380/statm): 531 226 485 147 0 384 0 [pid=16380] vsize: 2124 Raw data (/proc/16384/stat): 16384 (minisat+_64-bit) R 16380 16380 4419 0 -1 0 12691 0 0 0 82759 114 0 0 25 0 1 0 1844176087 53071872 12586 4294967295 134512640 135094434 3221224432 3221223024 134557040 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/16384/statm): 12957 12586 145 145 0 12812 0 [pid=16384] vsize: 51828 Current children cumulated CPU time (s) 828.74 Current children cumulated vsize (Kb) 53952 [startup+840.071 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 16384 Raw data (/proc/16380/stat): 16380 (minisat+_script) S 16379 16380 4419 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1844176082 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/16380/statm): 531 226 485 147 0 384 0 [pid=16380] vsize: 2124 Raw data (/proc/16384/stat): 16384 (minisat+_64-bit) R 16380 16380 4419 0 -1 0 12691 0 0 0 83759 114 0 0 25 0 1 0 1844176087 53071872 12586 4294967295 134512640 135094434 3221224432 3221223088 134557964 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/16384/statm): 12957 12586 145 145 0 12812 0 [pid=16384] vsize: 51828 Current children cumulated CPU time (s) 838.74 Current children cumulated vsize (Kb) 53952 [startup+850.073 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 16384 Raw data (/proc/16380/stat): 16380 (minisat+_script) S 16379 16380 4419 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1844176082 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/16380/statm): 531 226 485 147 0 384 0 [pid=16380] vsize: 2124 Raw data (/proc/16384/stat): 16384 (minisat+_64-bit) R 16380 16380 4419 0 -1 0 12691 0 0 0 84758 115 0 0 25 0 1 0 1844176087 53071872 12586 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/16384/statm): 12957 12586 145 145 0 12812 0 [pid=16384] vsize: 51828 Current children cumulated CPU time (s) 848.74 Current children cumulated vsize (Kb) 53952 [startup+860.073 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 16384 Raw data (/proc/16380/stat): 16380 (minisat+_script) S 16379 16380 4419 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1844176082 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/16380/statm): 531 226 485 147 0 384 0 [pid=16380] vsize: 2124 Raw data (/proc/16384/stat): 16384 (minisat+_64-bit) R 16380 16380 4419 0 -1 0 12691 0 0 0 85758 115 0 0 25 0 1 0 1844176087 53071872 12586 4294967295 134512640 135094434 3221224432 3221223024 134557202 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/16384/statm): 12957 12586 145 145 0 12812 0 [pid=16384] vsize: 51828 Current children cumulated CPU time (s) 858.74 Current children cumulated vsize (Kb) 53952 [startup+870.074 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 16384 Raw data (/proc/16380/stat): 16380 (minisat+_script) S 16379 16380 4419 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1844176082 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/16380/statm): 531 226 485 147 0 384 0 [pid=16380] vsize: 2124 Raw data (/proc/16384/stat): 16384 (minisat+_64-bit) R 16380 16380 4419 0 -1 0 12692 0 0 0 86758 115 0 0 25 0 1 0 1844176087 53071872 12587 4294967295 134512640 135094434 3221224432 3221223120 134554746 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/16384/statm): 12957 12587 145 145 0 12812 0 [pid=16384] vsize: 51828 Current children cumulated CPU time (s) 868.74 Current children cumulated vsize (Kb) 53952 [startup+880.075 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 16384 Raw data (/proc/16380/stat): 16380 (minisat+_script) S 16379 16380 4419 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1844176082 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/16380/statm): 531 226 485 147 0 384 0 [pid=16380] vsize: 2124 Raw data (/proc/16384/stat): 16384 (minisat+_64-bit) R 16380 16380 4419 0 -1 0 12694 0 0 0 87757 115 0 0 25 0 1 0 1844176087 53071872 12589 4294967295 134512640 135094434 3221224432 3221223024 134557236 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/16384/statm): 12957 12589 145 145 0 12812 0 [pid=16384] vsize: 51828 Current children cumulated CPU time (s) 878.73 Current children cumulated vsize (Kb) 53952 [startup+890.075 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 16384 Raw data (/proc/16380/stat): 16380 (minisat+_script) S 16379 16380 4419 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1844176082 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/16380/statm): 531 226 485 147 0 384 0 [pid=16380] vsize: 2124 Raw data (/proc/16384/stat): 16384 (minisat+_64-bit) R 16380 16380 4419 0 -1 0 12694 0 0 0 88757 116 0 0 25 0 1 0 1844176087 53071872 12589 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/16384/statm): 12957 12589 145 145 0 12812 0 [pid=16384] vsize: 51828 Current children cumulated CPU time (s) 888.74 Current children cumulated vsize (Kb) 53952 [startup+900.076 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 16384 Raw data (/proc/16380/stat): 16380 (minisat+_script) S 16379 16380 4419 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1844176082 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/16380/statm): 531 226 485 147 0 384 0 [pid=16380] vsize: 2124 Raw data (/proc/16384/stat): 16384 (minisat+_64-bit) R 16380 16380 4419 0 -1 0 12694 0 0 0 89757 116 0 0 25 0 1 0 1844176087 53071872 12589 4294967295 134512640 135094434 3221224432 3221223056 134562085 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/16384/statm): 12957 12589 145 145 0 12812 0 [pid=16384] vsize: 51828 Current children cumulated CPU time (s) 898.74 Current children cumulated vsize (Kb) 53952 [startup+910.076 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 16384 Raw data (/proc/16380/stat): 16380 (minisat+_script) S 16379 16380 4419 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1844176082 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/16380/statm): 531 226 485 147 0 384 0 [pid=16380] vsize: 2124 Raw data (/proc/16384/stat): 16384 (minisat+_64-bit) R 16380 16380 4419 0 -1 0 12694 0 0 0 90756 117 0 0 25 0 1 0 1844176087 53071872 12589 4294967295 134512640 135094434 3221224432 3221223024 134557300 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/16384/statm): 12957 12589 145 145 0 12812 0 [pid=16384] vsize: 51828 Current children cumulated CPU time (s) 908.74 Current children cumulated vsize (Kb) 53952 [startup+920.078 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 16384 Raw data (/proc/16380/stat): 16380 (minisat+_script) S 16379 16380 4419 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1844176082 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/16380/statm): 531 226 485 147 0 384 0 [pid=16380] vsize: 2124 Raw data (/proc/16384/stat): 16384 (minisat+_64-bit) R 16380 16380 4419 0 -1 0 12694 0 0 0 91756 117 0 0 25 0 1 0 1844176087 53071872 12589 4294967295 134512640 135094434 3221224432 3221223024 134556941 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/16384/statm): 12957 12589 145 145 0 12812 0 [pid=16384] vsize: 51828 Current children cumulated CPU time (s) 918.74 Current children cumulated vsize (Kb) 53952 [startup+930.079 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 16384 Raw data (/proc/16380/stat): 16380 (minisat+_script) S 16379 16380 4419 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1844176082 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/16380/statm): 531 226 485 147 0 384 0 [pid=16380] vsize: 2124 Raw data (/proc/16384/stat): 16384 (minisat+_64-bit) R 16380 16380 4419 0 -1 0 12694 0 0 0 92755 118 0 0 25 0 1 0 1844176087 53071872 12589 4294967295 134512640 135094434 3221224432 3221223120 134554731 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/16384/statm): 12957 12589 145 145 0 12812 0 [pid=16384] vsize: 51828 Current children cumulated CPU time (s) 928.74 Current children cumulated vsize (Kb) 53952 [startup+940.079 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 16384 Raw data (/proc/16380/stat): 16380 (minisat+_script) S 16379 16380 4419 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1844176082 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/16380/statm): 531 226 485 147 0 384 0 [pid=16380] vsize: 2124 Raw data (/proc/16384/stat): 16384 (minisat+_64-bit) R 16380 16380 4419 0 -1 0 12694 0 0 0 93754 119 0 0 25 0 1 0 1844176087 53071872 12589 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/16384/statm): 12957 12589 145 145 0 12812 0 [pid=16384] vsize: 51828 Current children cumulated CPU time (s) 938.74 Current children cumulated vsize (Kb) 53952 [startup+950.08 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 16384 Raw data (/proc/16380/stat): 16380 (minisat+_script) S 16379 16380 4419 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1844176082 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/16380/statm): 531 226 485 147 0 384 0 [pid=16380] vsize: 2124 Raw data (/proc/16384/stat): 16384 (minisat+_64-bit) R 16380 16380 4419 0 -1 0 12694 0 0 0 94754 119 0 0 25 0 1 0 1844176087 53071872 12589 4294967295 134512640 135094434 3221224432 3221223024 134556894 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/16384/statm): 12957 12589 145 145 0 12812 0 [pid=16384] vsize: 51828 Current children cumulated CPU time (s) 948.74 Current children cumulated vsize (Kb) 53952 [startup+960.081 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 16384 Raw data (/proc/16380/stat): 16380 (minisat+_script) S 16379 16380 4419 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1844176082 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/16380/statm): 531 226 485 147 0 384 0 [pid=16380] vsize: 2124 Raw data (/proc/16384/stat): 16384 (minisat+_64-bit) R 16380 16380 4419 0 -1 0 12694 0 0 0 95753 120 0 0 25 0 1 0 1844176087 53071872 12589 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/16384/statm): 12957 12589 145 145 0 12812 0 [pid=16384] vsize: 51828 Current children cumulated CPU time (s) 958.74 Current children cumulated vsize (Kb) 53952 [startup+970.082 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 16384 Raw data (/proc/16380/stat): 16380 (minisat+_script) S 16379 16380 4419 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1844176082 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/16380/statm): 531 226 485 147 0 384 0 [pid=16380] vsize: 2124 Raw data (/proc/16384/stat): 16384 (minisat+_64-bit) R 16380 16380 4419 0 -1 0 12694 0 0 0 96753 120 0 0 25 0 1 0 1844176087 53071872 12589 4294967295 134512640 135094434 3221224432 3221223056 134557685 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/16384/statm): 12957 12589 145 145 0 12812 0 [pid=16384] vsize: 51828 Current children cumulated CPU time (s) 968.74 Current children cumulated vsize (Kb) 53952 [startup+980.083 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 16384 Raw data (/proc/16380/stat): 16380 (minisat+_script) S 16379 16380 4419 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1844176082 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/16380/statm): 531 226 485 147 0 384 0 [pid=16380] vsize: 2124 Raw data (/proc/16384/stat): 16384 (minisat+_64-bit) R 16380 16380 4419 0 -1 0 12694 0 0 0 97753 120 0 0 25 0 1 0 1844176087 53071872 12589 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/16384/statm): 12957 12589 145 145 0 12812 0 [pid=16384] vsize: 51828 Current children cumulated CPU time (s) 978.74 Current children cumulated vsize (Kb) 53952 [startup+990.083 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 16384 Raw data (/proc/16380/stat): 16380 (minisat+_script) S 16379 16380 4419 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1844176082 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/16380/statm): 531 226 485 147 0 384 0 [pid=16380] vsize: 2124 Raw data (/proc/16384/stat): 16384 (minisat+_64-bit) R 16380 16380 4419 0 -1 0 12694 0 0 0 98752 121 0 0 25 0 1 0 1844176087 53071872 12589 4294967295 134512640 135094434 3221224432 3221223088 134558213 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/16384/statm): 12957 12589 145 145 0 12812 0 [pid=16384] vsize: 51828 Current children cumulated CPU time (s) 988.74 Current children cumulated vsize (Kb) 53952 [startup+1000.08 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 16384 Raw data (/proc/16380/stat): 16380 (minisat+_script) S 16379 16380 4419 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1844176082 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/16380/statm): 531 226 485 147 0 384 0 [pid=16380] vsize: 2124 Raw data (/proc/16384/stat): 16384 (minisat+_64-bit) R 16380 16380 4419 0 -1 0 12694 0 0 0 99752 121 0 0 25 0 1 0 1844176087 53071872 12589 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/16384/statm): 12957 12589 145 145 0 12812 0 [pid=16384] vsize: 51828 Current children cumulated CPU time (s) 998.74 Current children cumulated vsize (Kb) 53952 [startup+1010.08 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 16384 Raw data (/proc/16380/stat): 16380 (minisat+_script) S 16379 16380 4419 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1844176082 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/16380/statm): 531 226 485 147 0 384 0 [pid=16380] vsize: 2124 Raw data (/proc/16384/stat): 16384 (minisat+_64-bit) R 16380 16380 4419 0 -1 0 12694 0 0 0 100752 121 0 0 25 0 1 0 1844176087 53071872 12589 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/16384/statm): 12957 12589 145 145 0 12812 0 [pid=16384] vsize: 51828 Current children cumulated CPU time (s) 1008.74 Current children cumulated vsize (Kb) 53952 [startup+1020.09 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 16384 Raw data (/proc/16380/stat): 16380 (minisat+_script) S 16379 16380 4419 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1844176082 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/16380/statm): 531 226 485 147 0 384 0 [pid=16380] vsize: 2124 Raw data (/proc/16384/stat): 16384 (minisat+_64-bit) R 16380 16380 4419 0 -1 0 12694 0 0 0 101752 121 0 0 25 0 1 0 1844176087 53071872 12589 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/16384/statm): 12957 12589 145 145 0 12812 0 [pid=16384] vsize: 51828 Current children cumulated CPU time (s) 1018.74 Current children cumulated vsize (Kb) 53952 [startup+1030.09 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 16384 Raw data (/proc/16380/stat): 16380 (minisat+_script) S 16379 16380 4419 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1844176082 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/16380/statm): 531 226 485 147 0 384 0 [pid=16380] vsize: 2124 Raw data (/proc/16384/stat): 16384 (minisat+_64-bit) R 16380 16380 4419 0 -1 0 12694 0 0 0 102751 122 0 0 25 0 1 0 1844176087 53071872 12589 4294967295 134512640 135094434 3221224432 3221223088 134558235 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/16384/statm): 12957 12589 145 145 0 12812 0 [pid=16384] vsize: 51828 Current children cumulated CPU time (s) 1028.74 Current children cumulated vsize (Kb) 53952 [startup+1040.09 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 16384 Raw data (/proc/16380/stat): 16380 (minisat+_script) S 16379 16380 4419 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1844176082 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/16380/statm): 531 226 485 147 0 384 0 [pid=16380] vsize: 2124 Raw data (/proc/16384/stat): 16384 (minisat+_64-bit) R 16380 16380 4419 0 -1 0 12694 0 0 0 103751 122 0 0 25 0 1 0 1844176087 53071872 12589 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/16384/statm): 12957 12589 145 145 0 12812 0 [pid=16384] vsize: 51828 Current children cumulated CPU time (s) 1038.74 Current children cumulated vsize (Kb) 53952 [startup+1050.09 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 16384 Raw data (/proc/16380/stat): 16380 (minisat+_script) S 16379 16380 4419 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1844176082 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/16380/statm): 531 226 485 147 0 384 0 [pid=16380] vsize: 2124 Raw data (/proc/16384/stat): 16384 (minisat+_64-bit) R 16380 16380 4419 0 -1 0 12694 0 0 0 104751 122 0 0 25 0 1 0 1844176087 53071872 12589 4294967295 134512640 135094434 3221224432 3221223024 134557202 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/16384/statm): 12957 12589 145 145 0 12812 0 [pid=16384] vsize: 51828 Current children cumulated CPU time (s) 1048.74 Current children cumulated vsize (Kb) 53952 [startup+1060.09 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 16384 Raw data (/proc/16380/stat): 16380 (minisat+_script) S 16379 16380 4419 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1844176082 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/16380/statm): 531 226 485 147 0 384 0 [pid=16380] vsize: 2124 Raw data (/proc/16384/stat): 16384 (minisat+_64-bit) R 16380 16380 4419 0 -1 0 12694 0 0 0 105750 123 0 0 25 0 1 0 1844176087 53071872 12589 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/16384/statm): 12957 12589 145 145 0 12812 0 [pid=16384] vsize: 51828 Current children cumulated CPU time (s) 1058.74 Current children cumulated vsize (Kb) 53952 [startup+1070.09 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 16384 Raw data (/proc/16380/stat): 16380 (minisat+_script) S 16379 16380 4419 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1844176082 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/16380/statm): 531 226 485 147 0 384 0 [pid=16380] vsize: 2124 Raw data (/proc/16384/stat): 16384 (minisat+_64-bit) R 16380 16380 4419 0 -1 0 12698 0 0 0 106750 123 0 0 25 0 1 0 1844176087 53071872 12593 4294967295 134512640 135094434 3221224432 3221223024 134557273 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/16384/statm): 12957 12593 145 145 0 12812 0 [pid=16384] vsize: 51828 Current children cumulated CPU time (s) 1068.74 Current children cumulated vsize (Kb) 53952 [startup+1080.09 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 16384 Raw data (/proc/16380/stat): 16380 (minisat+_script) S 16379 16380 4419 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1844176082 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/16380/statm): 531 226 485 147 0 384 0 [pid=16380] vsize: 2124 Raw data (/proc/16384/stat): 16384 (minisat+_64-bit) R 16380 16380 4419 0 -1 0 12698 0 0 0 107750 123 0 0 25 0 1 0 1844176087 53071872 12593 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/16384/statm): 12957 12593 145 145 0 12812 0 [pid=16384] vsize: 51828 Current children cumulated CPU time (s) 1078.74 Current children cumulated vsize (Kb) 53952 [startup+1090.09 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 16384 Raw data (/proc/16380/stat): 16380 (minisat+_script) S 16379 16380 4419 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1844176082 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/16380/statm): 531 226 485 147 0 384 0 [pid=16380] vsize: 2124 Raw data (/proc/16384/stat): 16384 (minisat+_64-bit) R 16380 16380 4419 0 -1 0 12699 0 0 0 108749 124 0 0 25 0 1 0 1844176087 53071872 12594 4294967295 134512640 135094434 3221224432 3221223024 134557202 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/16384/statm): 12957 12594 145 145 0 12812 0 [pid=16384] vsize: 51828 Current children cumulated CPU time (s) 1088.74 Current children cumulated vsize (Kb) 53952 [startup+1100.09 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 16384 Raw data (/proc/16380/stat): 16380 (minisat+_script) S 16379 16380 4419 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1844176082 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/16380/statm): 531 226 485 147 0 384 0 [pid=16380] vsize: 2124 Raw data (/proc/16384/stat): 16384 (minisat+_64-bit) R 16380 16380 4419 0 -1 0 12702 0 0 0 109749 124 0 0 25 0 1 0 1844176087 53071872 12597 4294967295 134512640 135094434 3221224432 3221223056 134557705 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/16384/statm): 12957 12597 145 145 0 12812 0 [pid=16384] vsize: 51828 Current children cumulated CPU time (s) 1098.74 Current children cumulated vsize (Kb) 53952 [startup+1110.09 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 16384 Raw data (/proc/16380/stat): 16380 (minisat+_script) S 16379 16380 4419 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1844176082 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/16380/statm): 531 226 485 147 0 384 0 [pid=16380] vsize: 2124 Raw data (/proc/16384/stat): 16384 (minisat+_64-bit) R 16380 16380 4419 0 -1 0 12704 0 0 0 110749 124 0 0 25 0 1 0 1844176087 53071872 12599 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/16384/statm): 12957 12599 145 145 0 12812 0 [pid=16384] vsize: 51828 Current children cumulated CPU time (s) 1108.74 Current children cumulated vsize (Kb) 53952 [startup+1120.1 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 16384 Raw data (/proc/16380/stat): 16380 (minisat+_script) S 16379 16380 4419 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1844176082 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/16380/statm): 531 226 485 147 0 384 0 [pid=16380] vsize: 2124 Raw data (/proc/16384/stat): 16384 (minisat+_64-bit) R 16380 16380 4419 0 -1 0 12704 0 0 0 111748 125 0 0 25 0 1 0 1844176087 53071872 12599 4294967295 134512640 135094434 3221224432 3221223088 134558213 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/16384/statm): 12957 12599 145 145 0 12812 0 [pid=16384] vsize: 51828 Current children cumulated CPU time (s) 1118.74 Current children cumulated vsize (Kb) 53952 [startup+1130.1 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 16384 Raw data (/proc/16380/stat): 16380 (minisat+_script) S 16379 16380 4419 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1844176082 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/16380/statm): 531 226 485 147 0 384 0 [pid=16380] vsize: 2124 Raw data (/proc/16384/stat): 16384 (minisat+_64-bit) R 16380 16380 4419 0 -1 0 12704 0 0 0 112748 125 0 0 25 0 1 0 1844176087 53071872 12599 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/16384/statm): 12957 12599 145 145 0 12812 0 [pid=16384] vsize: 51828 Current children cumulated CPU time (s) 1128.74 Current children cumulated vsize (Kb) 53952 [startup+1140.1 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 16384 Raw data (/proc/16380/stat): 16380 (minisat+_script) S 16379 16380 4419 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1844176082 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/16380/statm): 531 226 485 147 0 384 0 [pid=16380] vsize: 2124 Raw data (/proc/16384/stat): 16384 (minisat+_64-bit) R 16380 16380 4419 0 -1 0 12704 0 0 0 113748 125 0 0 25 0 1 0 1844176087 53071872 12599 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/16384/statm): 12957 12599 145 145 0 12812 0 [pid=16384] vsize: 51828 Current children cumulated CPU time (s) 1138.74 Current children cumulated vsize (Kb) 53952 [startup+1150.1 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 16384 Raw data (/proc/16380/stat): 16380 (minisat+_script) S 16379 16380 4419 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1844176082 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/16380/statm): 531 226 485 147 0 384 0 [pid=16380] vsize: 2124 Raw data (/proc/16384/stat): 16384 (minisat+_64-bit) R 16380 16380 4419 0 -1 0 12704 0 0 0 114747 126 0 0 25 0 1 0 1844176087 53071872 12599 4294967295 134512640 135094434 3221224432 3221223024 134557413 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/16384/statm): 12957 12599 145 145 0 12812 0 [pid=16384] vsize: 51828 Current children cumulated CPU time (s) 1148.74 Current children cumulated vsize (Kb) 53952 [startup+1160.1 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 16384 Raw data (/proc/16380/stat): 16380 (minisat+_script) S 16379 16380 4419 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1844176082 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/16380/statm): 531 226 485 147 0 384 0 [pid=16380] vsize: 2124 Raw data (/proc/16384/stat): 16384 (minisat+_64-bit) R 16380 16380 4419 0 -1 0 12704 0 0 0 115747 126 0 0 25 0 1 0 1844176087 53071872 12599 4294967295 134512640 135094434 3221224432 3221223024 134557180 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/16384/statm): 12957 12599 145 145 0 12812 0 [pid=16384] vsize: 51828 Current children cumulated CPU time (s) 1158.74 Current children cumulated vsize (Kb) 53952 [startup+1170.1 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 16384 Raw data (/proc/16380/stat): 16380 (minisat+_script) S 16379 16380 4419 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1844176082 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/16380/statm): 531 226 485 147 0 384 0 [pid=16380] vsize: 2124 Raw data (/proc/16384/stat): 16384 (minisat+_64-bit) R 16380 16380 4419 0 -1 0 12704 0 0 0 116747 127 0 0 25 0 1 0 1844176087 53071872 12599 4294967295 134512640 135094434 3221224432 3221223088 134558395 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/16384/statm): 12957 12599 145 145 0 12812 0 [pid=16384] vsize: 51828 Current children cumulated CPU time (s) 1168.75 Current children cumulated vsize (Kb) 53952 [startup+1180.1 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 16384 Raw data (/proc/16380/stat): 16380 (minisat+_script) S 16379 16380 4419 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1844176082 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/16380/statm): 531 226 485 147 0 384 0 [pid=16380] vsize: 2124 Raw data (/proc/16384/stat): 16384 (minisat+_64-bit) R 16380 16380 4419 0 -1 0 12704 0 0 0 117746 127 0 0 25 0 1 0 1844176087 53071872 12599 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/16384/statm): 12957 12599 145 145 0 12812 0 [pid=16384] vsize: 51828 Current children cumulated CPU time (s) 1178.74 Current children cumulated vsize (Kb) 53952 [startup+1190.1 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 16384 Raw data (/proc/16380/stat): 16380 (minisat+_script) S 16379 16380 4419 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1844176082 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/16380/statm): 531 226 485 147 0 384 0 [pid=16380] vsize: 2124 Raw data (/proc/16384/stat): 16384 (minisat+_64-bit) R 16380 16380 4419 0 -1 0 12704 0 0 0 118746 128 0 0 25 0 1 0 1844176087 53071872 12599 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/16384/statm): 12957 12599 145 145 0 12812 0 [pid=16384] vsize: 51828 Current children cumulated CPU time (s) 1188.75 Current children cumulated vsize (Kb) 53952 [startup+1200.1 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 16384 Raw data (/proc/16380/stat): 16380 (minisat+_script) S 16379 16380 4419 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1844176082 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/16380/statm): 531 226 485 147 0 384 0 [pid=16380] vsize: 2124 Raw data (/proc/16384/stat): 16384 (minisat+_64-bit) R 16380 16380 4419 0 -1 0 12718 0 0 0 119745 128 0 0 25 0 1 0 1844176087 53190656 12613 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/16384/statm): 12986 12613 145 145 0 12841 0 [pid=16384] vsize: 51944 Current children cumulated CPU time (s) 1198.74 Current children cumulated vsize (Kb) 54068 [startup+1210.1 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 16384 Raw data (/proc/16380/stat): 16380 (minisat+_script) S 16379 16380 4419 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1844176082 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/16380/statm): 531 226 485 147 0 384 0 [pid=16380] vsize: 2124 Raw data (/proc/16384/stat): 16384 (minisat+_64-bit) R 16380 16380 4419 0 -1 0 12719 0 0 0 120745 128 0 0 25 0 1 0 1844176087 53190656 12614 4294967295 134512640 135094434 3221224432 3221223088 134558159 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/16384/statm): 12986 12614 145 145 0 12841 0 [pid=16384] vsize: 51944 Current children cumulated CPU time (s) 1208.74 Current children cumulated vsize (Kb) 54068 Maximum CPU time exceeded: sending SIGTERM then SIGKILL [startup+1210.11 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 16384 Raw data (/proc/16380/stat): 16380 (minisat+_script) S 16379 16380 4419 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1844176082 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/16380/statm): 531 226 485 147 0 384 0 [pid=16380] vsize: 2124 Raw data (/proc/16384/stat): 16384 (minisat+_64-bit) R 16380 16380 4419 0 -1 0 12719 0 0 0 120745 128 0 0 25 0 1 0 1844176087 53190656 12614 4294967295 134512640 135094434 3221224432 3221223088 134558159 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/16384/statm): 12986 12614 145 145 0 12841 0 [pid=16384] vsize: 51944 Current children cumulated CPU time (s) 1208.74 Current children cumulated vsize (Kb) 54068 Sending SIGTERM to -16380 Sleeping 2 seconds One traced child (pid=16380) ended because it received signal 15 (SIGTERM) One traced child (pid=16384) exited with status: 10 All traced children have exited ! Game is over. Child status: 10 Real time (s): 1210.14 CPU time (s): 1208.77 CPU user time (s): 1207.46 CPU system time (s): 1.3128 CPU usage (%): 99.8869 Max. virtual memory (cumulated for all children) (Kb): 54068
ERROR: no interpretation found !