Name | mps-v2-20-10/MIPLIB/miplib/normalized-mps-v2-20-10-bell3b.opb |
MD5SUM | efb36546b6b37df68ff339bb766886b9 |
Bench Category | optimization, big integers (OPTBIGINT) |
Has Objective Function | YES |
Satisfiable | YES |
(Un)Satisfiability was proved | YES |
Best value of the objective function | 4510472947583472 |
Optimality of the best value was proved | NO |
Number of terms in the objective function | 1780 |
Biggest coefficient in the objective function | 50331648000000000 |
Number of bits for the biggest coefficient in the objective function | 56 |
Sum of the numbers in the objective function | 1076758128151185266 |
Number of bits of the sum of numbers in the objective function | 60 |
Biggest number in a constraint | 50331648000000000 |
Number of bits of the biggest number in a constraint | 56 |
Biggest sum of numbers in a constraint | 1076758128151185266 |
Number of bits of the biggest sum of numbers | 60 |
Best result obtained on this benchmark | SAT |
Best CPU time to get the best result obtained on this benchmark | 1195.08 |
Number of variables | 2283 |
Total number of constraints | 194 |
Number of constraints which are clauses | 22 |
Number of constraints which are cardinality constraints (but not clauses) | 39 |
Number of constraints which are nor clauses,nor cardinality constraints | 133 |
Minimum length of a constraint | 1 |
Maximum length of a constraint | 195 |
LAUNCH ON wulflinc5 THE 2005-09-19 17:23:28 (client local time) PB2005-SCRIPT v4.0 MARKUPS: idlaunch=2845 boxname=wulflinc5 idbench=501 idsolver=3 numberseed=0 MD5SUM SOLVER: MD5SUM BENCH: efb36546b6b37df68ff339bb766886b9 /oldhome/oroussel/tmp/wulflinc5/normalized-mps-v2-20-10-bell3b.opb REAL COMMAND: minisat+_script /oldhome/oroussel/tmp/wulflinc5/normalized-mps-v2-20-10-bell3b.opb IDLAUNCH: 2845 /proc/cpuinfo: processor : 0 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 2 cpu MHz : 451.007 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 : 2 cpu MHz : 451.007 cache size : 512 KB fdiv_bug : no hlt_bug : no f00f_bug : no coma_bug : no fpu : yes fpu_exception : yes cpuid level : 2 wp : yes flags : fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse bogomips : 899.07 /proc/meminfo: MemTotal: 1034660 kB MemFree: 901944 kB Buffers: 35560 kB Cached: 72800 kB SwapCached: 780 kB Active: 73124 kB Inactive: 37936 kB HighTotal: 131008 kB HighFree: 54572 kB LowTotal: 903652 kB LowFree: 847372 kB SwapTotal: 2097136 kB SwapFree: 2095888 kB Dirty: 28 kB Writeback: 0 kB Mapped: 5804 kB Slab: 15980 kB Committed_AS: 64300 kB PageTables: 332 kB VmallocTotal: 114680 kB VmallocUsed: 1364 kB VmallocChunk: 113256 kB JOB ENDED THE 2005-09-19 17:43:39 (client local time) WITH STATUS 10 IN 1209.51 SECONDS stats: 2845 7 1209.51 10
c Parsing PB file... c PARSE ERROR! [line 137] Integer overflow. Use BigNum-version. c OK -- Running BigNum-version instead... c Parsing PB file... c Converting 151 PB-constraints to clauses... c -- Unit propagations: ppppppppppppp c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): ssssssss......................ssssss c ---[ 148]---> BDD-cost: 13 c ---[ 147]---> BDD-cost: 13 c ---[ 146]---> BDD-cost: 13 c ---[ 145]---> BDD-cost: 13 c ---[ 144]---> BDD-cost: 13 c ---[ 143]---> BDD-cost: 13 c ---[ 142]---> BDD-cost: 13 c ---[ 141]---> BDD-cost: 13 c ---[ 110]---> BDD-cost: 9 c ---[ 109]---> BDD-cost: 9 c ---[ 108]---> BDD-cost: 9 c ---[ 107]---> BDD-cost: 9 c ---[ 106]---> BDD-cost: 9 c ---[ 105]---> BDD-cost: 9 c ---[ 104]---> BDD-cost: 9 c ---[ 103]---> BDD-cost: 9 c ---[ 102]---> BDD-cost: 9 c ---[ 101]---> BDD-cost: 9 c ---[ 100]---> BDD-cost: 9 c ---[ 99]---> BDD-cost: 9 c ---[ 98]---> BDD-cost: 9 c ---[ 97]---> BDD-cost: 9 c ---[ 96]---> BDD-cost: 9 c ---[ 95]---> BDD-cost: 9 c ---[ 94]---> Sorter-cost: 974 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 93]---> Sorter-cost: 1414 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 92]---> BDD-cost: 70 c ---[ 91]---> Sorter-cost: 921 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 90]---> Sorter-cost: 532 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 89]---> Sorter-cost: 969 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 88]---> Sorter-cost: 969 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 87]---> Sorter-cost: 969 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 86]---> BDD-cost: 70 c ---[ 85]---> Sorter-cost: 986 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 84]---> Sorter-cost: 512 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 83]---> Sorter-cost: 532 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 82]---> Sorter-cost: 986 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 81]---> Sorter-cost: 974 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 80]---> Sorter-cost: 2069 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 79]---> Sorter-cost: 2707 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 78]---> Sorter-cost: 1414 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 77]---> BDD-cost: 70 c ---[ 76]---> Sorter-cost: 552 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 75]---> BDD-cost: 131 c ---[ 74]---> BDD-cost: 106 c ---[ 73]---> BDD-cost: 106 c ---[ 72]---> BDD-cost: 106 c ---[ 71]---> BDD-cost: 106 c ---[ 70]---> BDD-cost: 106 c ---[ 69]---> BDD-cost: 106 c ---[ 68]---> BDD-cost: 131 c ---[ 67]---> BDD-cost: 106 c ---[ 66]---> BDD-cost: 106 c ---[ 65]---> BDD-cost: 131 c ---[ 64]---> BDD-cost: 131 c ---[ 63]---> BDD-cost: 131 c ---[ 62]---> BDD-cost: 140 c ---[ 61]---> BDD-cost: 131 c ---[ 60]---> BDD-cost: 122 c ---[ 59]---> BDD-cost: 219 c ---[ 58]---> Sorter-cost: 859 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 57]---> BDD-cost: 76 c ---[ 56]---> Sorter-cost: 493 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 54]---> BDD-cost: 7 c ---[ 53]---> Sorter-cost: 502 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 52]---> Sorter-cost: 502 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 51]---> Sorter-cost: 503 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 50]---> BDD-cost: 8 c ---[ 49]---> BDD-cost: 61 c ---[ 48]---> Sorter-cost: 510 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 43]---> Sorter-cost: 510 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 42]---> Sorter-cost: 508 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 41]---> Sorter-cost: 1475 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 40]---> Sorter-cost: 1994 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 39]---> Sorter-cost: 849 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 38]---> BDD-cost: 74 c ---[ 36]---> Sorter-cost: 2970 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 5 2 2 c ---[ 35]---> Sorter-cost: 2970 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 5 2 2 c ---[ 34]---> Sorter-cost: 2837 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 5 2 2 c ---[ 33]---> Sorter-cost: 2836 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 5 2 2 c ---[ 32]---> Sorter-cost: 2970 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 5 2 2 c ---[ 31]---> Sorter-cost: 2970 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 5 2 2 c ---[ 30]---> Sorter-cost: 2970 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 5 2 2 c ---[ 29]---> Sorter-cost: 2970 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 5 2 2 c ---[ 28]---> Sorter-cost: 2970 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 5 2 2 c ---[ 27]---> Sorter-cost: 2970 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 5 2 2 c ---[ 26]---> Sorter-cost: 2837 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 5 2 2 c ---[ 25]---> Sorter-cost: 2837 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 5 2 2 c ---[ 24]---> Sorter-cost: 3073 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 5 2 2 c ---[ 23]---> Sorter-cost: 2970 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 5 2 2 c ---[ 22]---> Sorter-cost: 3361 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 5 2 2 2 2 c ---[ 21]---> Sorter-cost: 3682 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 5 5 c ---[ 20]---> Sorter-cost: 2970 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 5 2 2 c ---[ 19]---> Sorter-cost: 2970 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 5 2 2 c ---[ 18]---> Sorter-cost: 3311 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 5 2 2 2 c ---[ 17]---> Sorter-cost: 2970 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 5 2 2 c ---[ 16]---> Sorter-cost: 2837 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 5 2 2 c ---[ 15]---> Sorter-cost: 2837 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 5 2 2 c ---[ 14]---> Sorter-cost: 3311 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 5 2 2 2 c ---[ 13]---> BDD-cost: 5 c ---[ 12]---> BDD-cost: 5 c ---[ 11]---> BDD-cost: 5 c ---[ 10]---> BDD-cost: 5 c ---[ 9]---> BDD-cost: 5 c ---[ 8]---> BDD-cost: 5 c ---[ 7]---> BDD-cost: 5 c ---[ 6]---> BDD-cost: 5 c ---[ 5]---> BDD-cost: 54 c ---[ 4]---> BDD-cost: 78 c ---[ 3]---> BDD-cost: 32 c ---[ 2]---> BDD-cost: 7 c ---[ 1]---> BDD-cost: 7 c ---[ 0]---> BDD-cost: 70 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 0 | 247783 580424 | 82594 0 0 nan | 0.000 % | c | 102 | 247774 580405 | 90853 101 652 6.5 | 0.656 % | c | 252 | 247774 580405 | 99938 251 1692 6.7 | 0.656 % | c | 477 | 246332 577134 | 109932 471 3195 6.8 | 1.152 % | c | 814 | 246332 577134 | 120925 808 6254 7.7 | 1.152 % | c | 1321 | 245579 575421 | 133018 1311 10114 7.7 | 1.409 % | c | 2080 | 245512 575273 | 146320 2066 16014 7.8 | 1.430 % | c | 3219 | 245512 575273 | 160952 3205 71289 22.2 | 1.430 % | c | 4927 | 245325 574849 | 177047 4898 85171 17.4 | 1.492 % | c | 7489 | 245261 574703 | 194752 7458 163056 21.9 | 1.510 % | c | 11335 | 245261 574703 | 214227 11304 309019 27.3 | 1.510 % | c | 17103 | 245261 574703 | 235650 17072 813712 47.7 | 1.510 % | c ============================================================================== c [1mFound solution: 34068288466405961[0m c ---[ 0]---> c *** TERMINATED *** s SATISFIABLE v -d1_bit0 -d2_bit0 d3_bit0 -d4_bit0 d5_bit0 -d6_bit0 -d7_bit0 -d9_bit0 -d10_bit0 -d12_bit0 -d13_bit0 -d15_bit0 -d16_bit0 d17_bit0 -d20_bit0 -d21_bit0 h1_bit0 -h1_bit1 -h1_bit2 -h1_bit3 -h1_bit4 -h1_bit5 -h1_bit6 -h1_bit7 -h1_bit8 -h1_bit9 -h1_bit10 -h1_bit11 -h1_bit12 -h1_bit13 h2_bit0 -h2_bit1 h2_bit2 -h2_bit3 -h2_bit4 -h2_bit5 -h2_bit6 -h2_bit7 -h2_bit8 -h2_bit9 -h2_bit10 -h2_bit11 -h2_bit12 -h2_bit13 -h3_bit0 -h3_bit1 h3_bit2 h3_bit3 -h3_bit4 -h3_bit5 -h3_bit6 -h3_bit7 -h3_bit8 -h3_bit9 -h3_bit10 -h3_bit11 -h3_bit12 -h3_bit13 h4_bit0 -h4_bit1 -h4_bit2 -h4_bit3 h4_bit4 -h4_bit5 -h4_bit6 -h4_bit7 -h4_bit8 -h4_bit9 -h4_bit10 -h4_bit11 -h4_bit12 -h4_bit13 h5_bit0 h5_bit1 -h5_bit2 h5_bit3 -h5_bit4 -h5_bit5 -h5_bit6 -h5_bit7 -h5_bit8 -h5_bit9 -h5_bit10 -h5_bit11 -h5_bit12 -h5_bit13 -h6_bit0 -h6_bit1 h6_bit2 h6_bit3 -h6_bit4 -h6_bit5 -h6_bit6 -h6_bit7 -h6_bit8 -h6_bit9 -h6_bit10 -h6_bit11 -h6_bit12 -h6_bit13 -h7_bit0 -h7_bit1 -h7_bit2 -h7_bit3 -h7_bit4 -h7_bit5 -h7_bit6 -h7_bit7 -h7_bit8 -h7_bit9 -h7_bit10 -h7_bit11 -h7_bit12 -h7_bit13 -h9_bit0 -h9_bit1 -h9_bit2 -h9_bit3 -h9_bit4 -h9_bit5 -h9_bit6 -h9_bit7 -h9_bit8 -h9_bit9 -h9_bit10 -h9_bit11 -h9_bit12 -h9_bit13 -h10_bit0 -h10_bit1 h10_bit2 -h10_bit3 h10_bit4 -h10_bit5 -h10_bit6 -h10_bit7 -h10_bit8 -h10_bit9 -h12_bit0 -h12_bit1 -h12_bit2 -h12_bit3 -h12_bit4 -h12_bit5 -h12_bit6 -h12_bit7 -h12_bit8 -h12_bit9 -h13_bit0 -h13_bit1 -h13_bit2 -h13_bit3 -h13_bit4 -h13_bit5 -h13_bit6 -h13_bit7 -h13_bit8 -h13_bit9 h15_bit0 h15_bit1 -h15_bit2 -h15_bit3 -h15_bit4 -h15_bit5 -h15_bit6 -h15_bit7 -h15_bit8 -h15_bit9 h16_bit0 -h16_bit1 -h16_bit2 h16_bit3 -h16_bit4 -h16_bit5 -h16_bit6 -h16_bit7 -h16_bit8 -h16_bit9 h17_bit0 -h17_bit1 h17_bit2 -h17_bit3 -h17_bit4 -h17_bit5 -h17_bit6 -h17_bit7 -h17_bit8 -h17_bit9 -h20_bit0 -h20_bit1 -h20_bit2 -h20_bit3 -h20_bit4 -h20_bit5 -h20_bit6 -h20_bit7 -h20_bit8 -h20_bit9 -h21_bit0 -h21_bit1 -h21_bit2 -h21_bit3 -h21_bit4 -h21_bit5 -h21_bit6 -h21_bit7 -h21_bit8 -h21_bit9 g1_bit0 -g1_bit1 g1_bit2 -g1_bit3 g1_bit4 -g1_bit5 -g1_bit6 g1_bit7 g1_bit8 g1_bit9 -g1_bit10 -g1_bit11 -g1_bit12 -g1_bit13 g2_bit0 -g2_bit1 -g2_bit2 g2_bit3 g2_bit4 -g2_bit5 g2_bit6 -g2_bit7 g2_bit8 g2_bit9 -g2_bit10 -g2_bit11 g2_bit12 -g2_bit13 -g3_bit0 g3_bit1 g3_bit2 g3_bit3 g3_bit4 -g3_bit5 g3_bit6 -g3_bit7 g3_bit8 -g3_bit9 g3_bit10 -g3_bit11 -g3_bit12 -g3_bit13 -g4_bit0 g4_bit1 -g4_bit2 g4_bit3 g4_bit4 g4_bit5 -g4_bit6 -g4_bit7 -g4_bit8 g4_bit9 g4_bit10 -g4_bit11 -g4_bit12 -g4_bit13 -g5_bit0 -g5_bit1 g5_bit2 g5_bit3 -g5_bit4 g5_bit5 -g5_bit6 g5_bit7 g5_bit8 -g5_bit9 g5_bit10 -g5_bit11 g5_bit12 -g5_bit13 g6_bit0 -g6_bit1 g6_bit2 g6_bit3 -g6_bit4 g6_bit5 g6_bit6 -g6_bit7 g6_bit8 -g6_bit9 -g6_bit10 -g6_bit11 -g6_bit12 g6_bit13 -g7_bit0 g7_bit1 g7_bit2 g7_bit3 g7_bit4 g7_bit5 g7_bit6 g7_bit7 -g7_bit8 -g7_bit9 g7_bit10 -g7_bit11 -g7_bit12 -g7_bit13 g9_bit0 g9_bit1 g9_bit2 g9_bit3 g9_bit4 -g9_bit5 g9_bit6 g9_bit7 g9_bit8 g9_bit9 -g9_bit10 g9_bit11 -g9_bit12 -g9_bit13 g10_bit0 -g10_bit1 -g10_bit2 g10_bit3 g10_bit4 g10_bit5 -g10_bit6 g10_bit7 -g10_bit8 g10_bit9 -g12_bit0 g12_bit1 g12_bit2 -g12_bit3 -g12_bit4 -g12_bit5 g12_bit6 g12_bit7 -g12_bit8 g12_bit9 -g13_bit0 g13_bit1 -g13_bit2 -g13_bit3 -g13_bit4 -g13_bit5 -g13_bit6 g13_bit7 g13_bit8 g13_bit9 g15_bit0 -g15_bit1 g15_bit2 -g15_bit3 g15_bit4 -g15_bit5 g15_bit6 g15_bit7 g15_bit8 g15_bit9 -g16_bit0 g16_bit1 g16_bit2 g16_bit3 g16_bit4 -g16_bit5 g16_bit6 g16_bit7 -g16_bit8 -g16_bit9 g17_bit0 g17_bit1 g17_bit2 -g17_bit3 g17_bit4 -g17_bit5 -g17_bit6 g17_bit7 -g17_bit8 g17_bit9 -g20_bit0 -g20_bit1 -g20_bit2 -g20_bit3 -g20_bit4 g20_bit5 g20_bit6 -g20_bit7 g20_bit8 -g20_bit9 g21_bit0 -g21_bit1 g21_bit2 -g21_bit3 -g21_bit4 -g21_bit5 g21_bit6 -g21_bit7 g21_bit8 g21_bit9 a1_bit_10 -a1_bit_9 -a1_bit_8 a1_bit_7 a1_bit_6 -a1_bit_5 a1_bit_4 a1_bit_3 a1_bit_2 a1_bit_1 -a1_bit0 a1_bit1 -a1_bit2 a1_bit3 -a1_bit4 a1_bit5 a1_bit6 -a1_bit7 -a1_bit8 -a1_bit9 -a1_bit10 -a1_bit11 -a1_bit12 -a1_bit13 -a1_bit14 -a1_bit15 -a1_bit16 -a1_bit17 -a1_bit18 -a1_bit19 a2_bit_10 -a2_bit_9 a2_bit_8 a2_bit_7 a2_bit_6 -a2_bit_5 a2_bit_4 a2_bit_3 -a2_bit_2 -a2_bit_1 a2_bit0 a2_bit1 a2_bit2 -a2_bit3 a2_bit4 a2_bit5 -a2_bit6 -a2_bit7 a2_bit8 -a2_bit9 -a2_bit10 -a2_bit11 -a2_bit12 -a2_bit13 -a2_bit14 -a2_bit15 -a2_bit16 -a2_bit17 -a2_bit18 -a2_bit19 -a3_bit_10 -a3_bit_9 a3_bit_8 -a3_bit_7 a3_bit_6 -a3_bit_5 -a3_bit_4 -a3_bit_3 -a3_bit_2 a3_bit_1 a3_bit0 -a3_bit1 -a3_bit2 -a3_bit3 a3_bit4 a3_bit5 a3_bit6 -a3_bit7 -a3_bit8 -a3_bit9 -a3_bit10 -a3_bit11 -a3_bit12 -a3_bit13 -a3_bit14 -a3_bit15 -a3_bit16 -a3_bit17 -a3_bit18 -a3_bit19 -a4_bit_10 -a4_bit_9 -a4_bit_8 -a4_bit_7 a4_bit_6 -a4_bit_5 -a4_bit_4 -a4_bit_3 -a4_bit_2 a4_bit_1 -a4_bit0 a4_bit1 a4_bit2 a4_bit3 a4_bit4 -a4_bit5 a4_bit6 a4_bit7 -a4_bit8 -a4_bit9 -a4_bit10 -a4_bit11 -a4_bit12 -a4_bit13 -a4_bit14 -a4_bit15 -a4_bit16 -a4_bit17 -a4_bit18 -a4_bit19 -a5_bit_10 a5_bit_9 -a5_bit_8 -a5_bit_7 -a5_bit_6 a5_bit_5 a5_bit_4 a5_bit_3 -a5_bit_2 -a5_bit_1 -a5_bit0 -a5_bit1 -a5_bit2 -a5_bit3 -a5_bit4 -a5_bit5 a5_bit6 a5_bit7 -a5_bit8 -a5_bit9 -a5_bit10 -a5_bit11 -a5_bit12 -a5_bit13 -a5_bit14 -a5_bit15 -a5_bit16 -a5_bit17 -a5_bit18 -a5_bit19 a6_bit_10 a6_bit_9 a6_bit_8 a6_bit_7 a6_bit_6 -a6_bit_5 a6_bit_4 a6_bit_3 a6_bit_2 -a6_bit_1 a6_bit0 a6_bit1 a6_bit2 a6_bit3 -a6_bit4 -a6_bit5 -a6_bit6 -a6_bit7 -a6_bit8 a6_bit9 a6_bit10 -a6_bit11 -a6_bit12 -a6_bit13 -a6_bit14 -a6_bit15 -a6_bit16 -a6_bit17 -a6_bit18 -a6_bit19 -a7_bit_10 -a7_bit_9 a7_bit_8 a7_bit_7 a7_bit_6 -a7_bit_5 a7_bit_4 a7_bit_3 -a7_bit_2 -a7_bit_1 a7_bit0 a7_bit1 -a7_bit2 -a7_bit3 a7_bit4 -a7_bit5 -a7_bit6 a7_bit7 a7_bit8 -a7_bit9 a7_bit10 -a7_bit11 -a7_bit12 -a7_bit13 -a7_bit14 -a7_bit15 -a7_bit16 -a7_bit17 -a7_bit18 -a7_bit19 -a8_bit_10 -a8_bit_9 -a8_bit_8 -a8_bit_7 -a8_bit_6 -a8_bit_5 a8_bit_4 -a8_bit_3 -a8_bit_2 -a8_bit_1 -a8_bit0 a8_bit1 -a8_bit2 -a8_bit3 -a8_bit4 -a8_bit5 -a8_bit6 a8_bit7 a8_bit8 a8_bit9 -a8_bit10 -a8_bit11 -a8_bit12 -a8_bit13 -a8_bit14 -a8_bit15 -a8_bit16 -a8_bit17 -a8_bit18 -a8_bit19 -a9_bit_10 -a9_bit_9 a9_bit_8 -a9_bit_7 a9_bit_6 -a9_bit_5 -a9_bit_4 -a9_bit_3 a9_bit_2 -a9_bit_1 a9_bit0 a9_bit1 a9_bit2 -a9_bit3 a9_bit4 -a9_bit5 a9_bit6 -a9_bit7 -a9_bit8 a9_bit9 -a9_bit10 -a9_bit11 -a9_bit12 -a9_bit13 -a9_bit14 -a9_bit15 -a9_bit16 -a9_bit17 -a9_bit18 -a9_bit19 a10_bit_10 -a10_bit_9 a10_bit_8 a10_bit_7 a10_bit_6 a10_bit_5 a10_bit_4 a10_bit_3 -a10_bit_2 -a10_bit_1 a10_bit0 -a10_bit1 a10_bit2 a10_bit3 a10_bit4 a10_bit5 -a10_bit6 -a10_bit7 -a10_bit8 -a10_bit9 a10_bit10 -a10_bit11 -a10_bit12 -a10_bit13 -a10_bit14 -a10_bit15 -a10_bit16 -a10_bit17 -a10_bit18 -a10_bit19 -a11_bit_10 a11_bit_9 -a11_bit_8 a11_bit_7 -a11_bit_6 a11_bit_5 -a11_bit_4 -a11_bit_3 -a11_bit_2 a11_bit_1 -a11_bit0 a11_bit1 a11_bit2 -a11_bit3 a11_bit4 -a11_bit5 a11_bit6 a11_bit7 a11_bit8 a11_bit9 -a11_bit10 -a11_bit11 -a11_bit12 -a11_bit13 -a11_bit14 -a11_bit15 -a11_bit16 -a11_bit17 -a11_bit18 -a11_bit19 -a12_bit_10 -a12_bit_9 -a12_bit_8 -a12_bit_7 -a12_bit_6 -a12_bit_5 -a12_bit_4 -a12_bit_3 a12_bit_2 a12_bit_1 a12_bit0 -a12_bit1 -a12_bit2 a12_bit3 -a12_bit4 -a12_bit5 -a12_bit6 a12_bit7 a12_bit8 -a12_bit9 -a12_bit10 -a12_bit11 -a12_bit12 -a12_bit13 -a12_bit14 -a12_bit15 -a12_bit16 -a12_bit17 -a12_bit18 -a12_bit19 -a13_bit_10 -a13_bit_9 -a13_bit_8 -a13_bit_7 -a13_bit_6 -a13_bit_5 -a13_bit_4 -a13_bit_3 -a13_bit_2 -a13_bit_1 -a13_bit0 -a13_bit1 -a13_bit2 -a13_bit3 -a13_bit4 -a13_bit5 a13_bit6 -a13_bit7 -a13_bit8 -a13_bit9 -a13_bit10 -a13_bit11 -a13_bit12 -a13_bit13 -a13_bit14 -a13_bit15 -a13_bit16 -a13_bit17 -a13_bit18 -a13_bit19 a14_bit_10 -a14_bit_9 -a14_bit_8 a14_bit_7 -a14_bit_6 -a14_bit_5 a14_bit_4 a14_bit_3 -a14_bit_2 -a14_bit_1 a14_bit0 -a14_bit1 a14_bit2 a14_bit3 -a14_bit4 -a14_bit5 -a14_bit6 -a14_bit7 -a14_bit8 -a14_bit9 -a14_bit10 a14_bit11 -a14_bit12 -a14_bit13 -a14_bit14 -a14_bit15 -a14_bit16 -a14_bit17 -a14_bit18 -a14_bit19 -a15_bit_10 -a15_bit_9 -a15_bit_8 a15_bit_7 -a15_bit_6 -a15_bit_5 -a15_bit_4 -a15_bit_3 -a15_bit_2 -a15_bit_1 -a15_bit0 -a15_bit1 -a15_bit2 a15_bit3 -a15_bit4 a15_bit5 a15_bit6 a15_bit7 a15_bit8 -a15_bit9 -a15_bit10 -a15_bit11 -a15_bit12 -a15_bit13 -a15_bit14 -a15_bit15 -a15_bit16 -a15_bit17 -a15_bit18 -a15_bit19 -a16_bit_10 a16_bit_9 -a16_bit_8 a16_bit_7 a16_bit_6 -a16_bit_5 a16_bit_4 a16_bit_3 -a16_bit_2 a16_bit_1 a16_bit0 a16_bit1 a16_bit2 a16_bit3 a16_bit4 -a16_bit5 -a16_bit6 a16_bit7 -a16_bit8 a16_bit9 -a16_bit10 -a16_bit11 -a16_bit12 -a16_bit13 -a16_bit14 -a16_bit15 -a16_bit16 -a16_bit17 -a16_bit18 -a16_bit19 a17_bit_10 -a17_bit_9 a17_bit_8 -a17_bit_7 -a17_bit_6 -a17_bit_5 a17_bit_4 -a17_bit_3 -a17_bit_2 -a17_bit_1 -a17_bit0 -a17_bit1 -a17_bit2 a17_bit3 -a17_bit4 a17_bit5 a17_bit6 a17_bit7 a17_bit8 -a17_bit9 -a17_bit10 -a17_bit11 -a17_bit12 -a17_bit13 -a17_bit14 -a17_bit15 -a17_bit16 -a17_bit17 -a17_bit18 -a17_bit19 -a18_bit_10 -a18_bit_9 -a18_bit_8 -a18_bit_7 -a18_bit_6 -a18_bit_5 -a18_bit_4 -a18_bit_3 -a18_bit_2 -a18_bit_1 -a18_bit0 -a18_bit1 -a18_bit2 a18_bit3 -a18_bit4 a18_bit5 a18_bit6 a18_bit7 a18_bit8 a18_bit9 -a18_bit10 -a18_bit11 -a18_bit12 -a18_bit13 -a18_bit14 -a18_bit15 -a18_bit16 -a18_bit17 -a18_bit18 -a18_bit19 -a19_bit_10 -a19_bit_9 a19_bit_8 -a19_bit_7 -a19_bit_6 -a19_bit_5 a19_bit_4 -a19_bit_3 -a19_bit_2 a19_bit_1 -a19_bit0 -a19_bit1 a19_bit2 -a19_bit3 a19_bit4 a19_bit5 -a19_bit6 -a19_bit7 -a19_bit8 a19_bit9 -a19_bit10 -a19_bit11 -a19_bit12 -a19_bit13 -a19_bit14 -a19_bit15 -a19_bit16 -a19_bit17 -a19_bit18 -a19_bit19 -a20_bit_10 a20_bit_9 -a20_bit_8 a20_bit_7 a20_bit_6 a20_bit_5 -a20_bit_4 a20_bit_3 a20_bit_2 a20_bit_1 -a20_bit0 -a20_bit1 a20_bit2 a20_bit3 -a20_bit4 -a20_bit5 a20_bit6 a20_bit7 -a20_bit8 -a20_bit9 -a20_bit10 -a20_bit11 -a20_bit12 -a20_bit13 -a20_bit14 -a20_bit15 -a20_bit16 -a20_bit17 -a20_bit18 -a20_bit19 -a21_bit_10 -a21_bit_9 -a21_bit_8 -a21_bit_7 -a21_bit_6 -a21_bit_5 a21_bit_4 a21_bit_3 a21_bit_2 -a21_bit_1 a21_bit0 a21_bit1 -a21_bit2 a21_bit3 a21_bit4 a21_bit5 -a21_bit6 a21_bit7 -a21_bit8 -a21_bit9 a21_bit10 -a21_bit11 -a21_bit12 -a21_bit13 -a21_bit14 -a21_bit15 -a21_bit16 -a21_bit17 -a21_bit18 -a21_bit19 -a22_bit_10 a22_bit_9 -a22_bit_8 a22_bit_7 a22_bit_6 -a22_bit_5 -a22_bit_4 a22_bit_3 a22_bit_2 a22_bit_1 a22_bit0 a22_bit1 -a22_bit2 -a22_bit3 a22_bit4 -a22_bit5 a22_bit6 a22_bit7 a22_bit8 -a22_bit9 a22_bit10 -a22_bit11 -a22_bit12 -a22_bit13 -a22_bit14 -a22_bit15 -a22_bit16 -a22_bit17 -a22_bit18 -a22_bit19 -a23_bit_10 -a23_bit_9 -a23_bit_8 a23_bit_7 -a23_bit_6 a23_bit_5 -a23_bit_4 a23_bit_3 a23_bit_2 a23_bit_1 a23_bit0 a23_bit1 -a23_bit2 -a23_bit3 -a23_bit4 -a23_bit5 -a23_bit6 -a23_bit7 a23_bit8 -a23_bit9 a23_bit10 a23_bit11 -a23_bit12 -a23_bit13 -a23_bit14 -a23_bit15 -a23_bit16 -a23_bit17 -a23_bit18 -a23_bit19 b1_bit_10 -b1_bit_9 -b1_bit_8 -b1_bit_7 b1_bit_6 -b1_bit_5 b1_bit_4 b1_bit_3 b1_bit_2 b1_bit_1 b1_bit0 b1_bit1 -b1_bit2 b1_bit3 b1_bit4 -b1_bit5 -b1_bit6 -b1_bit7 -b1_bit8 b1_bit9 -b1_bit10 -b1_bit11 -b1_bit12 b1_bit13 -b1_bit14 -b1_bit15 -b1_bit16 -b1_bit17 -b1_bit18 -b1_bit19 -b2_bit_10 -b2_bit_9 b2_bit_8 b2_bit_7 -b2_bit_6 b2_bit_5 b2_bit_4 b2_bit_3 b2_bit_2 b2_bit_1 b2_bit0 -b2_bit1 b2_bit2 b2_bit3 -b2_bit4 -b2_bit5 -b2_bit6 b2_bit7 b2_bit8 -b2_bit9 b2_bit10 b2_bit11 b2_bit12 -b2_bit13 -b2_bit14 -b2_bit15 -b2_bit16 -b2_bit17 -b2_bit18 -b2_bit19 -b3_bit_10 b3_bit_9 b3_bit_8 b3_bit_7 -b3_bit_6 b3_bit_5 b3_bit_4 b3_bit_3 b3_bit_2 -b3_bit_1 -b3_bit0 -b3_bit1 -b3_bit2 b3_bit3 b3_bit4 b3_bit5 b3_bit6 b3_bit7 -b3_bit8 b3_bit9 -b3_bit10 b3_bit11 -b3_bit12 -b3_bit13 -b3_bit14 -b3_bit15 -b3_bit16 -b3_bit17 -b3_bit18 -b3_bit19 -b4_bit_10 b4_bit_9 b4_bit_8 b4_bit_7 -b4_bit_6 b4_bit_5 b4_bit_4 b4_bit_3 b4_bit_2 -b4_bit_1 b4_bit0 b4_bit1 b4_bit2 b4_bit3 b4_bit4 b4_bit5 b4_bit6 b4_bit7 -b4_bit8 b4_bit9 -b4_bit10 b4_bit11 b4_bit12 -b4_bit13 -b4_bit14 -b4_bit15 -b4_bit16 -b4_bit17 -b4_bit18 -b4_bit19 b5_bit_10 b5_bit_9 b5_bit_8 -b5_bit_7 b5_bit_6 b5_bit_5 b5_bit_4 b5_bit_3 b5_bit_2 -b5_bit_1 b5_bit0 -b5_bit1 -b5_bit2 -b5_bit3 -b5_bit4 b5_bit5 -b5_bit6 b5_bit7 -b5_bit8 -b5_bit9 -b5_bit10 b5_bit11 b5_bit12 -b5_bit13 -b5_bit14 -b5_bit15 -b5_bit16 -b5_bit17 -b5_bit18 -b5_bit19 -b6_bit_10 b6_bit_9 -b6_bit_8 -b6_bit_7 b6_bit_6 -b6_bit_5 -b6_bit_4 -b6_bit_3 b6_bit_2 b6_bit_1 -b6_bit0 -b6_bit1 -b6_bit2 -b6_bit3 -b6_bit4 -b6_bit5 -b6_bit6 -b6_bit7 -b6_bit8 -b6_bit9 -b6_bit10 b6_bit11 b6_bit12 -b6_bit13 -b6_bit14 -b6_bit15 -b6_bit16 -b6_bit17 -b6_bit18 -b6_bit19 -b7_bit_10 b7_bit_9 -b7_bit_8 -b7_bit_7 -b7_bit_6 -b7_bit_5 b7_bit_4 -b7_bit_3 b7_bit_2 -b7_bit_1 -b7_bit0 b7_bit1 b7_bit2 b7_bit3 b7_bit4 b7_bit5 b7_bit6 b7_bit7 b7_bit8 b7_bit9 b7_bit10 -b7_bit11 b7_bit12 -b7_bit13 -b7_bit14 -b7_bit15 -b7_bit16 -b7_bit17 -b7_bit18 -b7_bit19 b8_bit_10 -b8_bit_9 -b8_bit_8 b8_bit_7 -b8_bit_6 b8_bit_5 -b8_bit_4 -b8_bit_3 -b8_bit_2 b8_bit_1 b8_bit0 -b8_bit1 -b8_bit2 b8_bit3 b8_bit4 -b8_bit5 b8_bit6 b8_bit7 -b8_bit8 -b8_bit9 -b8_bit10 b8_bit11 -b8_bit12 -b8_bit13 -b8_bit14 -b8_bit15 -b8_bit16 -b8_bit17 -b8_bit18 -b8_bit19 -b9_bit_10 -b9_bit_9 -b9_bit_8 b9_bit_7 -b9_bit_6 -b9_bit_5 b9_bit_4 b9_bit_3 b9_bit_2 -b9_bit_1 -b9_bit0 b9_bit1 b9_bit2 -b9_bit3 b9_bit4 b9_bit5 b9_bit6 b9_bit7 b9_bit8 -b9_bit9 -b9_bit10 -b9_bit11 -b9_bit12 -b9_bit13 -b9_bit14 -b9_bit15 -b9_bit16 -b9_bit17 -b9_bit18 -b9_bit19 b10_bit_10 -b10_bit_9 b10_bit_8 b10_bit_7 b10_bit_6 b10_bit_5 -b10_bit_4 -b10_bit_3 -b10_bit_2 -b10_bit_1 -b10_bit0 -b10_bit1 -b10_bit2 -b10_bit3 -b10_bit4 -b10_bit5 -b10_bit6 -b10_bit7 -b10_bit8 -b10_bit9 -b10_bit10 -b10_bit11 b10_bit12 -b10_bit13 -b10_bit14 -b10_bit15 -b10_bit16 -b10_bit17 -b10_bit18 -b10_bit19 -b11_bit_10 -b11_bit_9 -b11_bit_8 -b11_bit_7 -b11_bit_6 b11_bit_5 -b11_bit_4 b11_bit_3 b11_bit_2 b11_bit_1 b11_bit0 b11_bit1 -b11_bit2 b11_bit3 b11_bit4 b11_bit5 b11_bit6 b11_bit7 b11_bit8 -b11_bit9 b11_bit10 -b11_bit11 -b11_bit12 -b11_bit13 -b11_bit14 -b11_bit15 -b11_bit16 -b11_bit17 -b11_bit18 -b11_bit19 -b12_bit_10 b12_bit_9 -b12_bit_8 -b12_bit_7 -b12_bit_6 -b12_bit_5 -b12_bit_4 b12_bit_3 b12_bit_2 -b12_bit_1 -b12_bit0 b12_bit1 -b12_bit2 -b12_bit3 -b12_bit4 -b12_bit5 b12_bit6 b12_bit7 b12_bit8 -b12_bit9 b12_bit10 -b12_bit11 -b12_bit12 -b12_bit13 -b12_bit14 -b12_bit15 -b12_bit16 -b12_bit17 -b12_bit18 -b12_bit19 -b13_bit_10 -b13_bit_9 -b13_bit_8 -b13_bit_7 -b13_bit_6 -b13_bit_5 -b13_bit_4 -b13_bit_3 -b13_bit_2 -b13_bit_1 -b13_bit0 -b13_bit1 -b13_bit2 -b13_bit3 -b13_bit4 -b13_bit5 -b13_bit6 -b13_bit7 -b13_bit8 -b13_bit9 -b13_bit10 -b13_bit11 -b13_bit12 -b13_bit13 -b13_bit14 -b13_bit15 -b13_bit16 -b13_bit17 -b13_bit18 -b13_bit19 -b14_bit_10 b14_bit_9 -b14_bit_8 b14_bit_7 b14_bit_6 -b14_bit_5 -b14_bit_4 b14_bit_3 b14_bit_2 -b14_bit_1 -b14_bit0 -b14_bit1 b14_bit2 -b14_bit3 -b14_bit4 b14_bit5 -b14_bit6 b14_bit7 -b14_bit8 -b14_bit9 -b14_bit10 b14_bit11 -b14_bit12 -b14_bit13 -b14_bit14 -b14_bit15 -b14_bit16 -b14_bit17 -b14_bit18 -b14_bit19 -b15_bit_10 -b15_bit_9 b15_bit_8 -b15_bit_7 -b15_bit_6 b15_bit_5 -b15_bit_4 b15_bit_3 -b15_bit_2 -b15_bit_1 -b15_bit0 -b15_bit1 -b15_bit2 -b15_bit3 -b15_bit4 -b15_bit5 -b15_bit6 -b15_bit7 -b15_bit8 -b15_bit9 -b15_bit10 -b15_bit11 -b15_bit12 -b15_bit13 -b15_bit14 -b15_bit15 -b15_bit16 -b15_bit17 -b15_bit18 -b15_bit19 b16_bit_10 b16_bit_9 -b16_bit_8 -b16_bit_7 -b16_bit_6 b16_bit_5 b16_bit_4 -b16_bit_3 -b16_bit_2 b16_bit_1 b16_bit0 b16_bit1 b16_bit2 -b16_bit3 b16_bit4 b16_bit5 -b16_bit6 -b16_bit7 b16_bit8 -b16_bit9 -b16_bit10 b16_bit11 -b16_bit12 -b16_bit13 -b16_bit14 -b16_bit15 -b16_bit16 -b16_bit17 -b16_bit18 -b16_bit19 -b17_bit_10 b17_bit_9 -b17_bit_8 -b17_bit_7 -b17_bit_6 -b17_bit_5 -b17_bit_4 -b17_bit_3 -b17_bit_2 -b17_bit_1 -b17_bit0 -b17_bit1 -b17_bit2 -b17_bit3 -b17_bit4 b17_bit5 -b17_bit6 -b17_bit7 b17_bit8 b17_bit9 -b17_bit10 b17_bit11 b17_bit12 -b17_bit13 -b17_bit14 -b17_bit15 -b17_bit16 -b17_bit17 -b17_bit18 -b17_bit19 -b18_bit_10 -b18_bit_9 -b18_bit_8 -b18_bit_7 -b18_bit_6 -b18_bit_5 b18_bit_4 -b18_bit_3 -b18_bit_2 -b18_bit_1 -b18_bit0 -b18_bit1 -b18_bit2 -b18_bit3 -b18_bit4 -b18_bit5 -b18_bit6 -b18_bit7 -b18_bit8 -b18_bit9 -b18_bit10 -b18_bit11 -b18_bit12 -b18_bit13 -b18_bit14 -b18_bit15 -b18_bit16 -b18_bit17 -b18_bit18 -b18_bit19 b19_bit_10 b19_bit_9 b19_bit_8 -b19_bit_7 -b19_bit_6 b19_bit_5 -b19_bit_4 -b19_bit_3 -b19_bit_2 -b19_bit_1 -b19_bit0 -b19_bit1 -b19_bit2 -b19_bit3 -b19_bit4 b19_bit5 b19_bit6 -b19_bit7 -b19_bit8 -b19_bit9 b19_bit10 -b19_bit11 b19_bit12 -b19_bit13 -b19_bit14 -b19_bit15 -b19_bit16 -b19_bit17 -b19_bit18 -b19_bit19 -b20_bit_10 -b20_bit_9 b20_bit_8 b20_bit_7 -b20_bit_6 -b20_bit_5 b20_bit_4 -b20_bit_3 b20_bit_2 -b20_bit_1 b20_bit0 -b20_bit1 b20_bit2 b20_bit3 -b20_bit4 -b20_bit5 b20_bit6 -b20_bit7 -b20_bit8 -b20_bit9 b20_bit10 b20_bit11 -b20_bit12 -b20_bit13 -b20_bit14 -b20_bit15 -b20_bit16 -b20_bit17 -b20_bit18 -b20_bit19 -b21_bit_10 b21_bit_9 -b21_bit_8 b21_bit_7 -b21_bit_6 b21_bit_5 -b21_bit_4 -b21_bit_3 b21_bit_2 b21_bit_1 b21_bit0 b21_bit1 -b21_bit2 -b21_bit3 -b21_bit4 b21_bit5 -b21_bit6 b21_bit7 b21_bit8 -b21_bit9 -b21_bit10 -b21_bit11 -b21_bit12 -b21_bit13 -b21_bit14 -b21_bit15 -b21_bit16 -b21_bit17 -b21_bit18 -b21_bit19 b22_bit_10 b22_bit_9 b22_bit_8 b22_bit_7 -b22_bit_6 b22_bit_5 b22_bit_4 -b22_bit_3 -b22_bit_2 -b22_bit_1 -b22_bit0 -b22_bit1 b22_bit2 -b22_bit3 -b22_bit4 -b22_bit5 -b22_bit6 b22_bit7 -b22_bit8 -b22_bit9 -b22_bit10 -b22_bit11 -b22_bit12 -b22_bit13 -b22_bit14 -b22_bit15 -b22_bit16 -b22_bit17 -b22_bit18 -b22_bit19 b23_bit_10 b23_bit_9 b23_bit_8 b23_bit_7 -b23_bit_6 b23_bit_5 b23_bit_4 -b23_bit_3 -b23_bit_2 -b23_bit_1 -b23_bit0 -b23_bit1 -b23_bit2 b23_bit3 b23_bit4 -b23_bit5 -b23_bit6 -b23_bit7 -b23_bit8 -b23_bit9 b23_bit10 -b23_bit11 -b23_bit12 -b23_bit13 -b23_bit14 -b23_bit15 -b23_bit16 -b23_bit17 -b23_bit18 -b23_bit19 c1_bit0 c2_bit0 c3_bit0 c4_bit0 c5_bit0 c6_bit0 -c7_bit0 -c8_bit0 -c9_bit0 c10_bit0 -c11_bit0 -c12_bit0 -c13_bit0 -c14_bit0 c15_bit0 c16_bit0 c17_bit0 c18_bit0 -c19_bit0 -c20_bit0 -c21_bit0 -c22_bit0 c23_bit0 -f1_bit_10 -f1_bit_9 f1_bit_8 -f1_bit_7 -f1_bit_6 f1_bit_5 f1_bit_4 f1_bit_3 f1_bit_2 f1_bit_1 f1_bit0 -f1_bit1 f1_bit2 f1_bit3 -f1_bit4 -f1_bit5 f1_bit6 f1_bit7 f1_bit8 -f1_bit9 -f1_bit10 f1_bit11 -f1_bit12 -f1_bit13 -f1_bit14 -f1_bit15 -f1_bit16 -f1_bit17 -f1_bit18 -f1_bit19 -f10_bit_10 -f10_bit_9 -f10_bit_8 -f10_bit_7 -f10_bit_6 -f10_bit_5 -f10_bit_4 f10_bit_3 f10_bit_2 -f10_bit_1 f10_bit0 f10_bit1 f10_bit2 -f10_bit3 f10_bit4 f10_bit5 -f10_bit6 -f10_bit7 f10_bit8 f10_bit9 f10_bit10 f10_bit11 f10_bit12 -f10_bit13 -f10_bit14 -f10_bit15 -f10_bit16 -f10_bit17 -f10_bit18 -f10_bit19 -f12_bit_10 -f12_bit_9 -f12_bit_8 -f12_bit_7 -f12_bit_6 -f12_bit_5 -f12_bit_4 f12_bit_3 f12_bit_2 -f12_bit_1 -f12_bit0 f12_bit1 f12_bit2 f12_bit3 f12_bit4 f12_bit5 -f12_bit6 f12_bit7 f12_bit8 -f12_bit9 f12_bit10 -f12_bit11 -f12_bit12 -f12_bit13 -f12_bit14 -f12_bit15 -f12_bit16 -f12_bit17 -f12_bit18 -f12_bit19 -f13_bit_10 -f13_bit_9 -f13_bit_8 -f13_bit_7 -f13_bit_6 -f13_bit_5 -f13_bit_4 -f13_bit_3 -f13_bit_2 -f13_bit_1 -f13_bit0 -f13_bit1 -f13_bit2 -f13_bit3 -f13_bit4 -f13_bit5 -f13_bit6 -f13_bit7 -f13_bit8 -f13_bit9 -f13_bit10 -f13_bit11 -f13_bit12 -f13_bit13 -f13_bit14 -f13_bit15 -f13_bit16 -f13_bit17 -f13_bit18 -f13_bit19 f15_bit_10 -f15_bit_9 -f15_bit_8 -f15_bit_7 f15_bit_6 -f15_bit_5 f15_bit_4 f15_bit_3 f15_bit_2 f15_bit_1 f15_bit0 f15_bit1 f15_bit2 f15_bit3 -f15_bit4 -f15_bit5 -f15_bit6 -f15_bit7 f15_bit8 -f15_bit9 f15_bit10 -f15_bit11 -f15_bit12 -f15_bit13 -f15_bit14 -f15_bit15 -f15_bit16 -f15_bit17 -f15_bit18 -f15_bit19 -f16_bit_10 -f16_bit_9 f16_bit_8 -f16_bit_7 -f16_bit_6 -f16_bit_5 f16_bit_4 f16_bit_3 -f16_bit_2 -f16_bit_1 -f16_bit0 f16_bit1 -f16_bit2 f16_bit3 -f16_bit4 -f16_bit5 -f16_bit6 -f16_bit7 -f16_bit8 -f16_bit9 f16_bit10 f16_bit11 -f16_bit12 -f16_bit13 -f16_bit14 -f16_bit15 -f16_bit16 -f16_bit17 -f16_bit18 -f16_bit19 -f17_bit_10 -f17_bit_9 -f17_bit_8 -f17_bit_7 -f17_bit_6 -f17_bit_5 f17_bit_4 f17_bit_3 f17_bit_2 f17_bit_1 f17_bit0 f17_bit1 f17_bit2 f17_bit3 f17_bit4 f17_bit5 f17_bit6 f17_bit7 f17_bit8 -f17_bit9 -f17_bit10 f17_bit11 -f17_bit12 f17_bit13 -f17_bit14 -f17_bit15 -f17_bit16 -f17_bit17 -f17_bit18 -f17_bit19 -f2_bit_10 f2_bit_9 f2_bit_8 f2_bit_7 f2_bit_6 f2_bit_5 f2_bit_4 f2_bit_3 f2_bit_2 f2_bit_1 f2_bit0 -f2_bit1 f2_bit2 -f2_bit3 -f2_bit4 -f2_bit5 -f2_bit6 -f2_bit7 f2_bit8 -f2_bit9 f2_bit10 -f2_bit11 -f2_bit12 f2_bit13 -f2_bit14 -f2_bit15 -f2_bit16 -f2_bit17 -f2_bit18 -f2_bit19 -f20_bit_10 f20_bit_9 -f20_bit_8 -f20_bit_7 f20_bit_6 -f20_bit_5 -f20_bit_4 f20_bit_3 -f20_bit_2 -f20_bit_1 -f20_bit0 -f20_bit1 f20_bit2 f20_bit3 f20_bit4
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/18986/stat): 18986 (minisat+_script) R 18985 18986 824 0 -1 0 19 0 0 0 0 0 0 0 21 0 1 0 1793445351 712704 3 4294967295 134512640 135087896 3221224512 3221224512 1073744960 0 0 5 0 0 0 0 17 1 0 0 Raw data (/proc/18986/statm): 174 3 169 147 0 27 0 [pid=18986] 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=18987 New process pid=18988 New process pid=18989 execve syscall for /bin/sed executable One traced child (pid=18988) 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=18989) exited with status: 0 One traced child (pid=18987) exited with status: 0 New process pid=18990 execve syscall for /oldhome/oroussel/solvers/minisat+_64-bit_static executable open syscall for file /dev/null open syscall for file /oldhome/oroussel/tmp/wulflinc5/normalized-mps-v2-20-10-bell3b.opb One traced child (pid=18990) exited with status: 5 open syscall for file /oldhome/oroussel/solvers/ New process pid=18991 execve syscall for /oldhome/oroussel/solvers/minisat+_bignum_static executable open syscall for file /dev/null open syscall for file /oldhome/oroussel/tmp/wulflinc5/normalized-mps-v2-20-10-bell3b.opb [startup+10.0042 s] Raw data (loadavg): 0.15 0.03 0.01 2/57 18991 Raw data (/proc/18986/stat): 18986 (minisat+_script) S 18985 18986 824 0 -1 0 314 330 0 2 0 1 0 1 17 0 1 0 1793445351 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/18986/statm): 532 234 485 147 0 385 0 [pid=18986] vsize: 2128 Raw data (/proc/18991/stat): 18991 (minisat+_bignum) R 18986 18986 824 0 -1 0 751 0 4 0 971 4 0 0 25 0 1 0 1793445365 3190784 663 4294967295 134512640 135167914 3221224448 3221221036 134723262 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/18991/statm): 779 663 162 162 0 617 0 [pid=18991] vsize: 3116 Current children cumulated CPU time (s) 9.77 Current children cumulated vsize (Kb) 5244 [startup+20.0059 s] Raw data (loadavg): 0.28 0.06 0.02 2/57 18991 Raw data (/proc/18986/stat): 18986 (minisat+_script) S 18985 18986 824 0 -1 0 314 330 0 2 0 1 0 1 17 0 1 0 1793445351 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/18986/statm): 532 234 485 147 0 385 0 [pid=18986] vsize: 2128 Raw data (/proc/18991/stat): 18991 (minisat+_bignum) R 18986 18986 824 0 -1 0 819 0 4 0 1971 4 0 0 25 0 1 0 1793445365 3760128 731 4294967295 134512640 135167914 3221224448 3221219088 134844644 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/18991/statm): 918 731 162 162 0 756 0 [pid=18991] vsize: 3672 Current children cumulated CPU time (s) 19.77 Current children cumulated vsize (Kb) 5800 [startup+30.0066 s] Raw data (loadavg): 0.39 0.09 0.03 2/57 18991 Raw data (/proc/18986/stat): 18986 (minisat+_script) S 18985 18986 824 0 -1 0 314 330 0 2 0 1 0 1 17 0 1 0 1793445351 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/18986/statm): 532 234 485 147 0 385 0 [pid=18986] vsize: 2128 Raw data (/proc/18991/stat): 18991 (minisat+_bignum) R 18986 18986 824 0 -1 0 1032 0 4 0 2971 4 0 0 25 0 1 0 1793445365 4218880 861 4294967295 134512640 135167914 3221224448 3221221280 134849096 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/18991/statm): 1030 861 162 162 0 868 0 [pid=18991] vsize: 4120 Current children cumulated CPU time (s) 29.77 Current children cumulated vsize (Kb) 6248 [startup+40.0073 s] Raw data (loadavg): 0.49 0.12 0.04 2/57 18991 Raw data (/proc/18986/stat): 18986 (minisat+_script) S 18985 18986 824 0 -1 0 314 330 0 2 0 1 0 1 17 0 1 0 1793445351 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/18986/statm): 532 234 485 147 0 385 0 [pid=18986] vsize: 2128 Raw data (/proc/18991/stat): 18991 (minisat+_bignum) R 18986 18986 824 0 -1 0 1079 0 4 0 3970 5 0 0 25 0 1 0 1793445365 4341760 908 4294967295 134512640 135167914 3221224448 3221222080 134844725 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/18991/statm): 1060 908 162 162 0 898 0 [pid=18991] vsize: 4240 Current children cumulated CPU time (s) 39.77 Current children cumulated vsize (Kb) 6368 [startup+50.008 s] Raw data (loadavg): 0.56 0.15 0.05 2/57 18991 Raw data (/proc/18986/stat): 18986 (minisat+_script) S 18985 18986 824 0 -1 0 314 330 0 2 0 1 0 1 17 0 1 0 1793445351 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/18986/statm): 532 234 485 147 0 385 0 [pid=18986] vsize: 2128 Raw data (/proc/18991/stat): 18991 (minisat+_bignum) R 18986 18986 824 0 -1 0 1148 0 4 0 4970 5 0 0 25 0 1 0 1793445365 4517888 977 4294967295 134512640 135167914 3221224448 3221220896 134843123 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/18991/statm): 1103 977 162 162 0 941 0 [pid=18991] vsize: 4412 Current children cumulated CPU time (s) 49.77 Current children cumulated vsize (Kb) 6540 [startup+60.0078 s] Raw data (loadavg): 0.63 0.18 0.06 2/57 18991 Raw data (/proc/18986/stat): 18986 (minisat+_script) S 18985 18986 824 0 -1 0 314 330 0 2 0 1 0 1 17 0 1 0 1793445351 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/18986/statm): 532 234 485 147 0 385 0 [pid=18986] vsize: 2128 Raw data (/proc/18991/stat): 18991 (minisat+_bignum) R 18986 18986 824 0 -1 0 1196 0 4 0 5969 6 0 0 25 0 1 0 1793445365 5431296 1025 4294967295 134512640 135167914 3221224448 3221221904 134843160 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/18991/statm): 1326 1025 162 162 0 1164 0 [pid=18991] vsize: 5304 Current children cumulated CPU time (s) 59.77 Current children cumulated vsize (Kb) 7432 [startup+70.0085 s] Raw data (loadavg): 0.69 0.21 0.07 2/57 18991 Raw data (/proc/18986/stat): 18986 (minisat+_script) S 18985 18986 824 0 -1 0 314 330 0 2 0 1 0 1 17 0 1 0 1793445351 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/18986/statm): 532 234 485 147 0 385 0 [pid=18986] vsize: 2128 Raw data (/proc/18991/stat): 18991 (minisat+_bignum) R 18986 18986 824 0 -1 0 1260 0 4 0 6969 6 0 0 25 0 1 0 1793445365 5615616 1089 4294967295 134512640 135167914 3221224448 3221221392 134843001 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/18991/statm): 1371 1089 162 162 0 1209 0 [pid=18991] vsize: 5484 Current children cumulated CPU time (s) 69.77 Current children cumulated vsize (Kb) 7612 [startup+80.0092 s] Raw data (loadavg): 0.73 0.23 0.08 2/57 18991 Raw data (/proc/18986/stat): 18986 (minisat+_script) S 18985 18986 824 0 -1 0 314 330 0 2 0 1 0 1 17 0 1 0 1793445351 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/18986/statm): 532 234 485 147 0 385 0 [pid=18986] vsize: 2128 Raw data (/proc/18991/stat): 18991 (minisat+_bignum) R 18986 18986 824 0 -1 0 1300 0 4 0 7969 6 0 0 25 0 1 0 1793445365 5701632 1129 4294967295 134512640 135167914 3221224448 3221221472 134629148 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/18991/statm): 1392 1129 162 162 0 1230 0 [pid=18991] vsize: 5568 Current children cumulated CPU time (s) 79.77 Current children cumulated vsize (Kb) 7696 [startup+90.0099 s] Raw data (loadavg): 0.77 0.26 0.09 2/57 18991 Raw data (/proc/18986/stat): 18986 (minisat+_script) S 18985 18986 824 0 -1 0 314 330 0 2 0 1 0 1 17 0 1 0 1793445351 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/18986/statm): 532 234 485 147 0 385 0 [pid=18986] vsize: 2128 Raw data (/proc/18991/stat): 18991 (minisat+_bignum) R 18986 18986 824 0 -1 0 1680 0 4 0 8968 7 0 0 25 0 1 0 1793445365 6508544 1344 4294967295 134512640 135167914 3221224448 3221221280 134693576 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/18991/statm): 1589 1344 162 162 0 1427 0 [pid=18991] vsize: 6356 Current children cumulated CPU time (s) 89.77 Current children cumulated vsize (Kb) 8484 [startup+100.011 s] Raw data (loadavg): 0.89 0.31 0.11 2/57 18999 Raw data (/proc/18986/stat): 18986 (minisat+_script) S 18985 18986 824 0 -1 0 314 330 0 2 0 1 0 1 17 0 1 0 1793445351 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/18986/statm): 532 234 485 147 0 385 0 [pid=18986] vsize: 2128 Raw data (/proc/18991/stat): 18991 (minisat+_bignum) R 18986 18986 824 0 -1 0 1749 0 4 0 9967 7 0 0 25 0 1 0 1793445365 6684672 1413 4294967295 134512640 135167914 3221224448 3221218096 134849153 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/18991/statm): 1632 1413 162 162 0 1470 0 [pid=18991] vsize: 6528 Current children cumulated CPU time (s) 99.76 Current children cumulated vsize (Kb) 8656 [startup+110.011 s] Raw data (loadavg): 0.91 0.33 0.12 2/57 18999 Raw data (/proc/18986/stat): 18986 (minisat+_script) S 18985 18986 824 0 -1 0 314 330 0 2 0 1 0 1 17 0 1 0 1793445351 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/18986/statm): 532 234 485 147 0 385 0 [pid=18986] vsize: 2128 Raw data (/proc/18991/stat): 18991 (minisat+_bignum) R 18986 18986 824 0 -1 0 7706 0 4 0 10914 36 0 0 25 0 1 0 1793445365 33697792 7326 4294967295 134512640 135167914 3221224448 3221223156 134558175 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/18991/statm): 8227 7326 162 162 0 8065 0 [pid=18991] vsize: 32908 Current children cumulated CPU time (s) 109.52 Current children cumulated vsize (Kb) 35036 [startup+120.013 s] Raw data (loadavg): 0.92 0.35 0.12 2/57 18999 Raw data (/proc/18986/stat): 18986 (minisat+_script) S 18985 18986 824 0 -1 0 314 330 0 2 0 1 0 1 17 0 1 0 1793445351 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/18986/statm): 532 234 485 147 0 385 0 [pid=18986] vsize: 2128 Raw data (/proc/18991/stat): 18991 (minisat+_bignum) T 18986 18986 824 0 -1 0 7911 0 4 0 11909 38 0 0 25 0 1 0 1793445365 34471936 7531 4294967295 134512640 135167914 3221224448 3221222876 134934490 0 0 5 16386 3222434794 0 0 17 0 0 0 Raw data (/proc/18991/statm): 8416 7531 162 162 0 8254 0 [pid=18991] vsize: 33664 Current children cumulated CPU time (s) 119.49 Current children cumulated vsize (Kb) 35792 [startup+130.013 s] Raw data (loadavg): 0.93 0.37 0.13 2/57 18999 Raw data (/proc/18986/stat): 18986 (minisat+_script) S 18985 18986 824 0 -1 0 314 330 0 2 0 1 0 1 17 0 1 0 1793445351 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/18986/statm): 532 234 485 147 0 385 0 [pid=18986] vsize: 2128 Raw data (/proc/18991/stat): 18991 (minisat+_bignum) R 18986 18986 824 0 -1 0 8086 0 4 0 12904 40 0 0 25 0 1 0 1793445365 35213312 7706 4294967295 134512640 135167914 3221224448 3221223088 134561462 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/18991/statm): 8597 7706 162 162 0 8435 0 [pid=18991] vsize: 34388 Current children cumulated CPU time (s) 129.46 Current children cumulated vsize (Kb) 36516 [startup+140.015 s] Raw data (loadavg): 0.94 0.39 0.14 2/57 18999 Raw data (/proc/18986/stat): 18986 (minisat+_script) S 18985 18986 824 0 -1 0 314 330 0 2 0 1 0 1 17 0 1 0 1793445351 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/18986/statm): 532 234 485 147 0 385 0 [pid=18986] vsize: 2128 Raw data (/proc/18991/stat): 18991 (minisat+_bignum) R 18986 18986 824 0 -1 0 8340 0 4 0 13900 42 0 0 25 0 1 0 1793445365 36237312 7960 4294967295 134512640 135167914 3221224448 3221223120 134562393 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/18991/statm): 8847 7960 162 162 0 8685 0 [pid=18991] vsize: 35388 Current children cumulated CPU time (s) 139.44 Current children cumulated vsize (Kb) 37516 [startup+150.015 s] Raw data (loadavg): 0.95 0.41 0.15 2/57 18999 Raw data (/proc/18986/stat): 18986 (minisat+_script) S 18985 18986 824 0 -1 0 314 330 0 2 0 1 0 1 17 0 1 0 1793445351 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/18986/statm): 532 234 485 147 0 385 0 [pid=18986] vsize: 2128 Raw data (/proc/18991/stat): 18991 (minisat+_bignum) R 18986 18986 824 0 -1 0 8661 0 4 0 14894 44 0 0 25 0 1 0 1793445365 37609472 8281 4294967295 134512640 135167914 3221224448 3221223184 134559365 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/18991/statm): 9182 8281 162 162 0 9020 0 [pid=18991] vsize: 36728 Current children cumulated CPU time (s) 149.4 Current children cumulated vsize (Kb) 38856 [startup+160.016 s] Raw data (loadavg): 0.96 0.43 0.16 2/57 18999 Raw data (/proc/18986/stat): 18986 (minisat+_script) S 18985 18986 824 0 -1 0 314 330 0 2 0 1 0 1 17 0 1 0 1793445351 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/18986/statm): 532 234 485 147 0 385 0 [pid=18986] vsize: 2128 Raw data (/proc/18991/stat): 18991 (minisat+_bignum) R 18986 18986 824 0 -1 0 10080 0 4 0 15881 49 0 0 25 0 1 0 1793445365 42647552 9575 4294967295 134512640 135167914 3221224448 3220922608 134843118 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/18991/statm): 10412 9575 162 162 0 10250 0 [pid=18991] vsize: 41648 Current children cumulated CPU time (s) 159.32 Current children cumulated vsize (Kb) 43776 [startup+170.017 s] Raw data (loadavg): 0.96 0.45 0.17 2/57 18999 Raw data (/proc/18986/stat): 18986 (minisat+_script) S 18985 18986 824 0 -1 0 314 330 0 2 0 1 0 1 17 0 1 0 1793445351 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/18986/statm): 532 234 485 147 0 385 0 [pid=18986] vsize: 2128 Raw data (/proc/18991/stat): 18991 (minisat+_bignum) R 18986 18986 824 0 -1 0 11683 0 4 0 16868 55 0 0 25 0 1 0 1793445365 48451584 10683 4294967295 134512640 135167914 3221224448 3221215456 134849196 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/18991/statm): 11829 10683 162 162 0 11667 0 [pid=18991] vsize: 47316 Current children cumulated CPU time (s) 169.25 Current children cumulated vsize (Kb) 49444 [startup+180.016 s] Raw data (loadavg): 0.97 0.47 0.18 2/57 18999 Raw data (/proc/18986/stat): 18986 (minisat+_script) S 18985 18986 824 0 -1 0 314 330 0 2 0 1 0 1 17 0 1 0 1793445351 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/18986/statm): 532 234 485 147 0 385 0 [pid=18986] vsize: 2128 Raw data (/proc/18991/stat): 18991 (minisat+_bignum) R 18986 18986 824 0 -1 0 11683 0 4 0 17868 55 0 0 25 0 1 0 1793445365 48451584 10683 4294967295 134512640 135167914 3221224448 3221216348 134722660 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/18991/statm): 11829 10683 162 162 0 11667 0 [pid=18991] vsize: 47316 Current children cumulated CPU time (s) 179.25 Current children cumulated vsize (Kb) 49444 [startup+190.018 s] Raw data (loadavg): 0.97 0.48 0.19 2/57 18999 Raw data (/proc/18986/stat): 18986 (minisat+_script) S 18985 18986 824 0 -1 0 314 330 0 2 0 1 0 1 17 0 1 0 1793445351 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/18986/statm): 532 234 485 147 0 385 0 [pid=18986] vsize: 2128 Raw data (/proc/18991/stat): 18991 (minisat+_bignum) R 18986 18986 824 0 -1 0 11683 0 4 0 18868 55 0 0 25 0 1 0 1793445365 48451584 10683 4294967295 134512640 135167914 3221224448 3221215756 134723262 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/18991/statm): 11829 10683 162 162 0 11667 0 [pid=18991] vsize: 47316 Current children cumulated CPU time (s) 189.25 Current children cumulated vsize (Kb) 49444 [startup+200.019 s] Raw data (loadavg): 0.98 0.50 0.19 2/57 18999 Raw data (/proc/18986/stat): 18986 (minisat+_script) S 18985 18986 824 0 -1 0 314 330 0 2 0 1 0 1 17 0 1 0 1793445351 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/18986/statm): 532 234 485 147 0 385 0 [pid=18986] vsize: 2128 Raw data (/proc/18991/stat): 18991 (minisat+_bignum) R 18986 18986 824 0 -1 0 11683 0 4 0 19868 55 0 0 25 0 1 0 1793445365 48451584 10683 4294967295 134512640 135167914 3221224448 3221216016 134629080 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/18991/statm): 11829 10683 162 162 0 11667 0 [pid=18991] vsize: 47316 Current children cumulated CPU time (s) 199.25 Current children cumulated vsize (Kb) 49444 [startup+210.019 s] Raw data (loadavg): 0.98 0.52 0.20 2/57 18999 Raw data (/proc/18986/stat): 18986 (minisat+_script) S 18985 18986 824 0 -1 0 314 330 0 2 0 1 0 1 17 0 1 0 1793445351 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/18986/statm): 532 234 485 147 0 385 0 [pid=18986] vsize: 2128 Raw data (/proc/18991/stat): 18991 (minisat+_bignum) R 18986 18986 824 0 -1 0 11683 0 4 0 20869 55 0 0 25 0 1 0 1793445365 48451584 10683 4294967295 134512640 135167914 3221224448 3221215824 134849143 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/18991/statm): 11829 10683 162 162 0 11667 0 [pid=18991] vsize: 47316 Current children cumulated CPU time (s) 209.26 Current children cumulated vsize (Kb) 49444 [startup+220.019 s] Raw data (loadavg): 0.98 0.53 0.21 2/57 18999 Raw data (/proc/18986/stat): 18986 (minisat+_script) S 18985 18986 824 0 -1 0 314 330 0 2 0 1 0 1 17 0 1 0 1793445351 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/18986/statm): 532 234 485 147 0 385 0 [pid=18986] vsize: 2128 Raw data (/proc/18991/stat): 18991 (minisat+_bignum) R 18986 18986 824 0 -1 0 11683 0 4 0 21869 55 0 0 25 0 1 0 1793445365 48451584 10683 4294967295 134512640 135167914 3221224448 3221215548 134844632 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/18991/statm): 11829 10683 162 162 0 11667 0 [pid=18991] vsize: 47316 Current children cumulated CPU time (s) 219.26 Current children cumulated vsize (Kb) 49444 [startup+230.02 s] Raw data (loadavg): 0.98 0.55 0.22 2/57 18999 Raw data (/proc/18986/stat): 18986 (minisat+_script) S 18985 18986 824 0 -1 0 314 330 0 2 0 1 0 1 17 0 1 0 1793445351 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/18986/statm): 532 234 485 147 0 385 0 [pid=18986] vsize: 2128 Raw data (/proc/18991/stat): 18991 (minisat+_bignum) R 18986 18986 824 0 -1 0 11683 0 4 0 22869 55 0 0 25 0 1 0 1793445365 48451584 10683 4294967295 134512640 135167914 3221224448 3221215896 134844633 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/18991/statm): 11829 10683 162 162 0 11667 0 [pid=18991] vsize: 47316 Current children cumulated CPU time (s) 229.26 Current children cumulated vsize (Kb) 49444 [startup+240.021 s] Raw data (loadavg): 0.99 0.56 0.22 2/57 18999 Raw data (/proc/18986/stat): 18986 (minisat+_script) S 18985 18986 824 0 -1 0 314 330 0 2 0 1 0 1 17 0 1 0 1793445351 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/18986/statm): 532 234 485 147 0 385 0 [pid=18986] vsize: 2128 Raw data (/proc/18991/stat): 18991 (minisat+_bignum) R 18986 18986 824 0 -1 0 11683 0 4 0 23869 55 0 0 25 0 1 0 1793445365 48451584 10683 4294967295 134512640 135167914 3221224448 3221216032 134844644 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/18991/statm): 11829 10683 162 162 0 11667 0 [pid=18991] vsize: 47316 Current children cumulated CPU time (s) 239.26 Current children cumulated vsize (Kb) 49444 [startup+250.022 s] Raw data (loadavg): 0.99 0.58 0.23 2/57 18999 Raw data (/proc/18986/stat): 18986 (minisat+_script) S 18985 18986 824 0 -1 0 314 330 0 2 0 1 0 1 17 0 1 0 1793445351 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/18986/statm): 532 234 485 147 0 385 0 [pid=18986] vsize: 2128 Raw data (/proc/18991/stat): 18991 (minisat+_bignum) R 18986 18986 824 0 -1 0 11683 0 4 0 24870 55 0 0 25 0 1 0 1793445365 48451584 10683 4294967295 134512640 135167914 3221224448 3221216096 134844644 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/18991/statm): 11829 10683 162 162 0 11667 0 [pid=18991] vsize: 47316 Current children cumulated CPU time (s) 249.27 Current children cumulated vsize (Kb) 49444 [startup+260.022 s] Raw data (loadavg): 0.99 0.59 0.24 2/57 18999 Raw data (/proc/18986/stat): 18986 (minisat+_script) S 18985 18986 824 0 -1 0 314 330 0 2 0 1 0 1 17 0 1 0 1793445351 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/18986/statm): 532 234 485 147 0 385 0 [pid=18986] vsize: 2128 Raw data (/proc/18991/stat): 18991 (minisat+_bignum) R 18986 18986 824 0 -1 0 11683 0 4 0 25870 55 0 0 25 0 1 0 1793445365 48451584 10683 4294967295 134512640 135167914 3221224448 3221215856 134844644 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/18991/statm): 11829 10683 162 162 0 11667 0 [pid=18991] vsize: 47316 Current children cumulated CPU time (s) 259.27 Current children cumulated vsize (Kb) 49444 [startup+270.023 s] Raw data (loadavg): 0.99 0.60 0.25 2/57 18999 Raw data (/proc/18986/stat): 18986 (minisat+_script) S 18985 18986 824 0 -1 0 314 330 0 2 0 1 0 1 17 0 1 0 1793445351 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/18986/statm): 532 234 485 147 0 385 0 [pid=18986] vsize: 2128 Raw data (/proc/18991/stat): 18991 (minisat+_bignum) R 18986 18986 824 0 -1 0 11683 0 4 0 26870 55 0 0 25 0 1 0 1793445365 48451584 10683 4294967295 134512640 135167914 3221224448 3221216540 134842996 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/18991/statm): 11829 10683 162 162 0 11667 0 [pid=18991] vsize: 47316 Current children cumulated CPU time (s) 269.27 Current children cumulated vsize (Kb) 49444 [startup+280.024 s] Raw data (loadavg): 0.99 0.61 0.26 2/57 18999 Raw data (/proc/18986/stat): 18986 (minisat+_script) S 18985 18986 824 0 -1 0 314 330 0 2 0 1 0 1 17 0 1 0 1793445351 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/18986/statm): 532 234 485 147 0 385 0 [pid=18986] vsize: 2128 Raw data (/proc/18991/stat): 18991 (minisat+_bignum) R 18986 18986 824 0 -1 0 11683 0 4 0 27870 55 0 0 25 0 1 0 1793445365 48451584 10683 4294967295 134512640 135167914 3221224448 3221215788 134843033 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/18991/statm): 11829 10683 162 162 0 11667 0 [pid=18991] vsize: 47316 Current children cumulated CPU time (s) 279.27 Current children cumulated vsize (Kb) 49444 [startup+290.025 s] Raw data (loadavg): 0.99 0.63 0.26 2/57 18999 Raw data (/proc/18986/stat): 18986 (minisat+_script) S 18985 18986 824 0 -1 0 314 330 0 2 0 1 0 1 17 0 1 0 1793445351 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/18986/statm): 532 234 485 147 0 385 0 [pid=18986] vsize: 2128 Raw data (/proc/18991/stat): 18991 (minisat+_bignum) R 18986 18986 824 0 -1 0 11683 0 4 0 28871 55 0 0 25 0 1 0 1793445365 48451584 10683 4294967295 134512640 135167914 3221224448 3221216208 134844653 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/18991/statm): 11829 10683 162 162 0 11667 0 [pid=18991] vsize: 47316 Current children cumulated CPU time (s) 289.28 Current children cumulated vsize (Kb) 49444 [startup+300.026 s] Raw data (loadavg): 0.99 0.64 0.27 2/57 18999 Raw data (/proc/18986/stat): 18986 (minisat+_script) S 18985 18986 824 0 -1 0 314 330 0 2 0 1 0 1 17 0 1 0 1793445351 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/18986/statm): 532 234 485 147 0 385 0 [pid=18986] vsize: 2128 Raw data (/proc/18991/stat): 18991 (minisat+_bignum) R 18986 18986 824 0 -1 0 11683 0 4 0 29871 55 0 0 25 0 1 0 1793445365 48451584 10683 4294967295 134512640 135167914 3221224448 3221215936 134843139 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/18991/statm): 11829 10683 162 162 0 11667 0 [pid=18991] vsize: 47316 Current children cumulated CPU time (s) 299.28 Current children cumulated vsize (Kb) 49444 [startup+310.026 s] Raw data (loadavg): 0.99 0.65 0.28 2/57 18999 Raw data (/proc/18986/stat): 18986 (minisat+_script) S 18985 18986 824 0 -1 0 314 330 0 2 0 1 0 1 17 0 1 0 1793445351 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/18986/statm): 532 234 485 147 0 385 0 [pid=18986] vsize: 2128 Raw data (/proc/18991/stat): 18991 (minisat+_bignum) R 18986 18986 824 0 -1 0 11683 0 4 0 30871 55 0 0 25 0 1 0 1793445365 48451584 10683 4294967295 134512640 135167914 3221224448 3221215808 134694517 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/18991/statm): 11829 10683 162 162 0 11667 0 [pid=18991] vsize: 47316 Current children cumulated CPU time (s) 309.28 Current children cumulated vsize (Kb) 49444 [startup+320.027 s] Raw data (loadavg): 0.99 0.66 0.29 2/57 18999 Raw data (/proc/18986/stat): 18986 (minisat+_script) S 18985 18986 824 0 -1 0 314 330 0 2 0 1 0 1 17 0 1 0 1793445351 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/18986/statm): 532 234 485 147 0 385 0 [pid=18986] vsize: 2128 Raw data (/proc/18991/stat): 18991 (minisat+_bignum) R 18986 18986 824 0 -1 0 11683 0 4 0 31871 55 0 0 25 0 1 0 1793445365 48451584 10683 4294967295 134512640 135167914 3221224448 3221216360 134694369 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/18991/statm): 11829 10683 162 162 0 11667 0 [pid=18991] vsize: 47316 Current children cumulated CPU time (s) 319.28 Current children cumulated vsize (Kb) 49444 [startup+330.027 s] Raw data (loadavg): 0.99 0.67 0.29 2/57 18999 Raw data (/proc/18986/stat): 18986 (minisat+_script) S 18985 18986 824 0 -1 0 314 330 0 2 0 1 0 1 17 0 1 0 1793445351 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/18986/statm): 532 234 485 147 0 385 0 [pid=18986] vsize: 2128 Raw data (/proc/18991/stat): 18991 (minisat+_bignum) R 18986 18986 824 0 -1 0 11683 0 4 0 32872 55 0 0 25 0 1 0 1793445365 48451584 10683 4294967295 134512640 135167914 3221224448 3221215680 134844644 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/18991/statm): 11829 10683 162 162 0 11667 0 [pid=18991] vsize: 47316 Current children cumulated CPU time (s) 329.29 Current children cumulated vsize (Kb) 49444 [startup+340.028 s] Raw data (loadavg): 0.99 0.68 0.30 2/57 18999 Raw data (/proc/18986/stat): 18986 (minisat+_script) S 18985 18986 824 0 -1 0 314 330 0 2 0 1 0 1 17 0 1 0 1793445351 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/18986/statm): 532 234 485 147 0 385 0 [pid=18986] vsize: 2128 Raw data (/proc/18991/stat): 18991 (minisat+_bignum) R 18986 18986 824 0 -1 0 11683 0 4 0 33872 55 0 0 25 0 1 0 1793445365 48451584 10683 4294967295 134512640 135167914 3221224448 3221215200 134845927 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/18991/statm): 11829 10683 162 162 0 11667 0 [pid=18991] vsize: 47316 Current children cumulated CPU time (s) 339.29 Current children cumulated vsize (Kb) 49444 [startup+350.029 s] Raw data (loadavg): 0.99 0.69 0.31 2/57 18999 Raw data (/proc/18986/stat): 18986 (minisat+_script) S 18985 18986 824 0 -1 0 314 330 0 2 0 1 0 1 17 0 1 0 1793445351 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/18986/statm): 532 234 485 147 0 385 0 [pid=18986] vsize: 2128 Raw data (/proc/18991/stat): 18991 (minisat+_bignum) R 18986 18986 824 0 -1 0 11683 0 4 0 34872 55 0 0 25 0 1 0 1793445365 48451584 10683 4294967295 134512640 135167914 3221224448 3221217232 134849193 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/18991/statm): 11829 10683 162 162 0 11667 0 [pid=18991] vsize: 47316 Current children cumulated CPU time (s) 349.29 Current children cumulated vsize (Kb) 49444 [startup+360.029 s] Raw data (loadavg): 0.99 0.70 0.31 2/57 18999 Raw data (/proc/18986/stat): 18986 (minisat+_script) S 18985 18986 824 0 -1 0 314 330 0 2 0 1 0 1 17 0 1 0 1793445351 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/18986/statm): 532 234 485 147 0 385 0 [pid=18986] vsize: 2128 Raw data (/proc/18991/stat): 18991 (minisat+_bignum) R 18986 18986 824 0 -1 0 11683 0 4 0 35872 55 0 0 25 0 1 0 1793445365 48451584 10683 4294967295 134512640 135167914 3221224448 3221216512 134843420 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/18991/statm): 11829 10683 162 162 0 11667 0 [pid=18991] vsize: 47316 Current children cumulated CPU time (s) 359.29 Current children cumulated vsize (Kb) 49444 [startup+370.03 s] Raw data (loadavg): 0.99 0.71 0.32 2/57 18999 Raw data (/proc/18986/stat): 18986 (minisat+_script) S 18985 18986 824 0 -1 0 314 330 0 2 0 1 0 1 17 0 1 0 1793445351 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/18986/statm): 532 234 485 147 0 385 0 [pid=18986] vsize: 2128 Raw data (/proc/18991/stat): 18991 (minisat+_bignum) R 18986 18986 824 0 -1 0 11683 0 4 0 36872 55 0 0 25 0 1 0 1793445365 48451584 10683 4294967295 134512640 135167914 3221224448 3221215936 134696587 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/18991/statm): 11829 10683 162 162 0 11667 0 [pid=18991] vsize: 47316 Current children cumulated CPU time (s) 369.29 Current children cumulated vsize (Kb) 49444 [startup+380.03 s] Raw data (loadavg): 0.99 0.72 0.33 2/57 18999 Raw data (/proc/18986/stat): 18986 (minisat+_script) S 18985 18986 824 0 -1 0 314 330 0 2 0 1 0 1 17 0 1 0 1793445351 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/18986/statm): 532 234 485 147 0 385 0 [pid=18986] vsize: 2128 Raw data (/proc/18991/stat): 18991 (minisat+_bignum) R 18986 18986 824 0 -1 0 11683 0 4 0 37873 55 0 0 25 0 1 0 1793445365 48451584 10683 4294967295 134512640 135167914 3221224448 3221216536 134693801 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/18991/statm): 11829 10683 162 162 0 11667 0 [pid=18991] vsize: 47316 Current children cumulated CPU time (s) 379.3 Current children cumulated vsize (Kb) 49444 [startup+390.031 s] Raw data (loadavg): 0.99 0.73 0.33 2/57 18999 Raw data (/proc/18986/stat): 18986 (minisat+_script) S 18985 18986 824 0 -1 0 314 330 0 2 0 1 0 1 17 0 1 0 1793445351 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/18986/statm): 532 234 485 147 0 385 0 [pid=18986] vsize: 2128 Raw data (/proc/18991/stat): 18991 (minisat+_bignum) R 18986 18986 824 0 -1 0 11683 0 4 0 38873 55 0 0 25 0 1 0 1793445365 48451584 10683 4294967295 134512640 135167914 3221224448 3221216652 134842996 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/18991/statm): 11829 10683 162 162 0 11667 0 [pid=18991] vsize: 47316 Current children cumulated CPU time (s) 389.3 Current children cumulated vsize (Kb) 49444 [startup+400.031 s] Raw data (loadavg): 0.99 0.74 0.34 2/57 18999 Raw data (/proc/18986/stat): 18986 (minisat+_script) S 18985 18986 824 0 -1 0 314 330 0 2 0 1 0 1 17 0 1 0 1793445351 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/18986/statm): 532 234 485 147 0 385 0 [pid=18986] vsize: 2128 Raw data (/proc/18991/stat): 18991 (minisat+_bignum) R 18986 18986 824 0 -1 0 11683 0 4 0 39873 55 0 0 25 0 1 0 1793445365 48451584 10683 4294967295 134512640 135167914 3221224448 3221216368 134629358 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/18991/statm): 11829 10683 162 162 0 11667 0 [pid=18991] vsize: 47316 Current children cumulated CPU time (s) 399.3 Current children cumulated vsize (Kb) 49444 [startup+410.032 s] Raw data (loadavg): 0.99 0.74 0.35 2/57 18999 Raw data (/proc/18986/stat): 18986 (minisat+_script) S 18985 18986 824 0 -1 0 314 330 0 2 0 1 0 1 17 0 1 0 1793445351 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/18986/statm): 532 234 485 147 0 385 0 [pid=18986] vsize: 2128 Raw data (/proc/18991/stat): 18991 (minisat+_bignum) R 18986 18986 824 0 -1 0 11683 0 4 0 40873 55 0 0 25 0 1 0 1793445365 48451584 10683 4294967295 134512640 135167914 3221224448 3221216284 134723262 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/18991/statm): 11829 10683 162 162 0 11667 0 [pid=18991] vsize: 47316 Current children cumulated CPU time (s) 409.3 Current children cumulated vsize (Kb) 49444 [startup+420.033 s] Raw data (loadavg): 0.99 0.75 0.35 2/57 18999 Raw data (/proc/18986/stat): 18986 (minisat+_script) S 18985 18986 824 0 -1 0 314 330 0 2 0 1 0 1 17 0 1 0 1793445351 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/18986/statm): 532 234 485 147 0 385 0 [pid=18986] vsize: 2128 Raw data (/proc/18991/stat): 18991 (minisat+_bignum) R 18986 18986 824 0 -1 0 11683 0 4 0 41874 55 0 0 25 0 1 0 1793445365 48451584 10683 4294967295 134512640 135167914 3221224448 3221216256 134718501 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/18991/statm): 11829 10683 162 162 0 11667 0 [pid=18991] vsize: 47316 Current children cumulated CPU time (s) 419.31 Current children cumulated vsize (Kb) 49444 [startup+430.034 s] Raw data (loadavg): 0.99 0.76 0.36 2/57 18999 Raw data (/proc/18986/stat): 18986 (minisat+_script) S 18985 18986 824 0 -1 0 314 330 0 2 0 1 0 1 17 0 1 0 1793445351 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/18986/statm): 532 234 485 147 0 385 0 [pid=18986] vsize: 2128 Raw data (/proc/18991/stat): 18991 (minisat+_bignum) R 18986 18986 824 0 -1 0 11683 0 4 0 42874 55 0 0 25 0 1 0 1793445365 48451584 10683 4294967295 134512640 135167914 3221224448 3221216096 134845927 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/18991/statm): 11829 10683 162 162 0 11667 0 [pid=18991] vsize: 47316 Current children cumulated CPU time (s) 429.31 Current children cumulated vsize (Kb) 49444 [startup+440.034 s] Raw data (loadavg): 0.99 0.77 0.37 2/57 18999 Raw data (/proc/18986/stat): 18986 (minisat+_script) S 18985 18986 824 0 -1 0 314 330 0 2 0 1 0 1 17 0 1 0 1793445351 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/18986/statm): 532 234 485 147 0 385 0 [pid=18986] vsize: 2128 Raw data (/proc/18991/stat): 18991 (minisat+_bignum) R 18986 18986 824 0 -1 0 11683 0 4 0 43874 55 0 0 25 0 1 0 1793445365 48451584 10683 4294967295 134512640 135167914 3221224448 3221215932 134723262 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/18991/statm): 11829 10683 162 162 0 11667 0 [pid=18991] vsize: 47316 Current children cumulated CPU time (s) 439.31 Current children cumulated vsize (Kb) 49444 [startup+450.035 s] Raw data (loadavg): 0.99 0.77 0.37 2/57 18999 Raw data (/proc/18986/stat): 18986 (minisat+_script) S 18985 18986 824 0 -1 0 314 330 0 2 0 1 0 1 17 0 1 0 1793445351 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/18986/statm): 532 234 485 147 0 385 0 [pid=18986] vsize: 2128 Raw data (/proc/18991/stat): 18991 (minisat+_bignum) R 18986 18986 824 0 -1 0 11683 0 4 0 44874 55 0 0 25 0 1 0 1793445365 48451584 10683 4294967295 134512640 135167914 3221224448 3221216992 134696578 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/18991/statm): 11829 10683 162 162 0 11667 0 [pid=18991] vsize: 47316 Current children cumulated CPU time (s) 449.31 Current children cumulated vsize (Kb) 49444 [startup+460.035 s] Raw data (loadavg): 0.99 0.78 0.38 2/57 18999 Raw data (/proc/18986/stat): 18986 (minisat+_script) S 18985 18986 824 0 -1 0 314 330 0 2 0 1 0 1 17 0 1 0 1793445351 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/18986/statm): 532 234 485 147 0 385 0 [pid=18986] vsize: 2128 Raw data (/proc/18991/stat): 18991 (minisat+_bignum) R 18986 18986 824 0 -1 0 11683 0 4 0 45875 55 0 0 25 0 1 0 1793445365 48451584 10683 4294967295 134512640 135167914 3221224448 3221216300 134843033 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/18991/statm): 11829 10683 162 162 0 11667 0 [pid=18991] vsize: 47316 Current children cumulated CPU time (s) 459.32 Current children cumulated vsize (Kb) 49444 [startup+470.035 s] Raw data (loadavg): 0.99 0.79 0.39 2/57 18999 Raw data (/proc/18986/stat): 18986 (minisat+_script) S 18985 18986 824 0 -1 0 314 330 0 2 0 1 0 1 17 0 1 0 1793445351 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/18986/statm): 532 234 485 147 0 385 0 [pid=18986] vsize: 2128 Raw data (/proc/18991/stat): 18991 (minisat+_bignum) R 18986 18986 824 0 -1 0 11683 0 4 0 46875 55 0 0 25 0 1 0 1793445365 48451584 10683 4294967295 134512640 135167914 3221224448 3221216172 134722656 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/18991/statm): 11829 10683 162 162 0 11667 0 [pid=18991] vsize: 47316 Current children cumulated CPU time (s) 469.32 Current children cumulated vsize (Kb) 49444 [startup+480.035 s] Raw data (loadavg): 0.99 0.80 0.39 2/57 18999 Raw data (/proc/18986/stat): 18986 (minisat+_script) S 18985 18986 824 0 -1 0 314 330 0 2 0 1 0 1 17 0 1 0 1793445351 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/18986/statm): 532 234 485 147 0 385 0 [pid=18986] vsize: 2128 Raw data (/proc/18991/stat): 18991 (minisat+_bignum) R 18986 18986 824 0 -1 0 11683 0 4 0 47875 55 0 0 25 0 1 0 1793445365 48451584 10683 4294967295 134512640 135167914 3221224448 3221216624 134843153 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/18991/statm): 11829 10683 162 162 0 11667 0 [pid=18991] vsize: 47316 Current children cumulated CPU time (s) 479.32 Current children cumulated vsize (Kb) 49444 [startup+490.036 s] Raw data (loadavg): 0.99 0.80 0.40 2/57 18999 Raw data (/proc/18986/stat): 18986 (minisat+_script) S 18985 18986 824 0 -1 0 314 330 0 2 0 1 0 1 17 0 1 0 1793445351 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/18986/statm): 532 234 485 147 0 385 0 [pid=18986] vsize: 2128 Raw data (/proc/18991/stat): 18991 (minisat+_bignum) R 18986 18986 824 0 -1 0 11683 0 4 0 48875 55 0 0 25 0 1 0 1793445365 48451584 10683 4294967295 134512640 135167914 3221224448 3221216304 134722527 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/18991/statm): 11829 10683 162 162 0 11667 0 [pid=18991] vsize: 47316 Current children cumulated CPU time (s) 489.32 Current children cumulated vsize (Kb) 49444 [startup+500.037 s] Raw data (loadavg): 0.99 0.81 0.40 2/57 18999 Raw data (/proc/18986/stat): 18986 (minisat+_script) S 18985 18986 824 0 -1 0 314 330 0 2 0 1 0 1 17 0 1 0 1793445351 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/18986/statm): 532 234 485 147 0 385 0 [pid=18986] vsize: 2128 Raw data (/proc/18991/stat): 18991 (minisat+_bignum) R 18986 18986 824 0 -1 0 11683 0 4 0 49875 55 0 0 25 0 1 0 1793445365 48451584 10683 4294967295 134512640 135167914 3221224448 3221215988 134849060 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/18991/statm): 11829 10683 162 162 0 11667 0 [pid=18991] vsize: 47316 Current children cumulated CPU time (s) 499.32 Current children cumulated vsize (Kb) 49444 [startup+510.036 s] Raw data (loadavg): 0.99 0.81 0.41 2/57 18999 Raw data (/proc/18986/stat): 18986 (minisat+_script) S 18985 18986 824 0 -1 0 314 330 0 2 0 1 0 1 17 0 1 0 1793445351 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/18986/statm): 532 234 485 147 0 385 0 [pid=18986] vsize: 2128 Raw data (/proc/18991/stat): 18991 (minisat+_bignum) R 18986 18986 824 0 -1 0 11683 0 4 0 50876 55 0 0 25 0 1 0 1793445365 48451584 10683 4294967295 134512640 135167914 3221224448 3221216140 134844632 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/18991/statm): 11829 10683 162 162 0 11667 0 [pid=18991] vsize: 47316 Current children cumulated CPU time (s) 509.33 Current children cumulated vsize (Kb) 49444 [startup+520.037 s] Raw data (loadavg): 0.99 0.82 0.41 2/57 18999 Raw data (/proc/18986/stat): 18986 (minisat+_script) S 18985 18986 824 0 -1 0 314 330 0 2 0 1 0 1 17 0 1 0 1793445351 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/18986/statm): 532 234 485 147 0 385 0 [pid=18986] vsize: 2128 Raw data (/proc/18991/stat): 18991 (minisat+_bignum) R 18986 18986 824 0 -1 0 11683 0 4 0 51876 55 0 0 25 0 1 0 1793445365 48451584 10683 4294967295 134512640 135167914 3221224448 3221215920 134844718 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/18991/statm): 11829 10683 162 162 0 11667 0 [pid=18991] vsize: 47316 Current children cumulated CPU time (s) 519.33 Current children cumulated vsize (Kb) 49444 [startup+530.038 s] Raw data (loadavg): 0.99 0.82 0.42 2/57 18999 Raw data (/proc/18986/stat): 18986 (minisat+_script) S 18985 18986 824 0 -1 0 314 330 0 2 0 1 0 1 17 0 1 0 1793445351 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/18986/statm): 532 234 485 147 0 385 0 [pid=18986] vsize: 2128 Raw data (/proc/18991/stat): 18991 (minisat+_bignum) R 18986 18986 824 0 -1 0 11683 0 4 0 52876 55 0 0 25 0 1 0 1793445365 48451584 10683 4294967295 134512640 135167914 3221224448 3221216048 134844708 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/18991/statm): 11829 10683 162 162 0 11667 0 [pid=18991] vsize: 47316 Current children cumulated CPU time (s) 529.33 Current children cumulated vsize (Kb) 49444 [startup+540.038 s] Raw data (loadavg): 0.99 0.83 0.43 2/57 18999 Raw data (/proc/18986/stat): 18986 (minisat+_script) S 18985 18986 824 0 -1 0 314 330 0 2 0 1 0 1 17 0 1 0 1793445351 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/18986/statm): 532 234 485 147 0 385 0 [pid=18986] vsize: 2128 Raw data (/proc/18991/stat): 18991 (minisat+_bignum) R 18986 18986 824 0 -1 0 11683 0 4 0 53876 55 0 0 25 0 1 0 1793445365 48451584 10683 4294967295 134512640 135167914 3221224448 3221215920 134844668 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/18991/statm): 11829 10683 162 162 0 11667 0 [pid=18991] vsize: 47316 Current children cumulated CPU time (s) 539.33 Current children cumulated vsize (Kb) 49444 [startup+550.039 s] Raw data (loadavg): 0.99 0.83 0.43 2/57 18999 Raw data (/proc/18986/stat): 18986 (minisat+_script) S 18985 18986 824 0 -1 0 314 330 0 2 0 1 0 1 17 0 1 0 1793445351 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/18986/statm): 532 234 485 147 0 385 0 [pid=18986] vsize: 2128 Raw data (/proc/18991/stat): 18991 (minisat+_bignum) R 18986 18986 824 0 -1 0 11683 0 4 0 54877 55 0 0 25 0 1 0 1793445365 48451584 10683 4294967295 134512640 135167914 3221224448 3221216400 134844676 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/18991/statm): 11829 10683 162 162 0 11667 0 [pid=18991] vsize: 47316 Current children cumulated CPU time (s) 549.34 Current children cumulated vsize (Kb) 49444 [startup+560.04 s] Raw data (loadavg): 0.99 0.84 0.44 2/57 18999 Raw data (/proc/18986/stat): 18986 (minisat+_script) S 18985 18986 824 0 -1 0 314 330 0 2 0 1 0 1 17 0 1 0 1793445351 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/18986/statm): 532 234 485 147 0 385 0 [pid=18986] vsize: 2128 Raw data (/proc/18991/stat): 18991 (minisat+_bignum) R 18986 18986 824 0 -1 0 11683 0 4 0 55877 55 0 0 25 0 1 0 1793445365 48451584 10683 4294967295 134512640 135167914 3221224448 3221217040 134849102 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/18991/statm): 11829 10683 162 162 0 11667 0 [pid=18991] vsize: 47316 Current children cumulated CPU time (s) 559.34 Current children cumulated vsize (Kb) 49444 [startup+570.041 s] Raw data (loadavg): 0.99 0.84 0.44 2/57 18999 Raw data (/proc/18986/stat): 18986 (minisat+_script) S 18985 18986 824 0 -1 0 314 330 0 2 0 1 0 1 17 0 1 0 1793445351 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/18986/statm): 532 234 485 147 0 385 0 [pid=18986] vsize: 2128 Raw data (/proc/18991/stat): 18991 (minisat+_bignum) R 18986 18986 824 0 -1 0 11683 0 4 0 56877 55 0 0 25 0 1 0 1793445365 48451584 10683 4294967295 134512640 135167914 3221224448 3221216512 134849196 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/18991/statm): 11829 10683 162 162 0 11667 0 [pid=18991] vsize: 47316 Current children cumulated CPU time (s) 569.34 Current children cumulated vsize (Kb) 49444 [startup+580.04 s] Raw data (loadavg): 0.99 0.85 0.45 2/57 18999 Raw data (/proc/18986/stat): 18986 (minisat+_script) S 18985 18986 824 0 -1 0 314 330 0 2 0 1 0 1 17 0 1 0 1793445351 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/18986/statm): 532 234 485 147 0 385 0 [pid=18986] vsize: 2128 Raw data (/proc/18991/stat): 18991 (minisat+_bignum) R 18986 18986 824 0 -1 0 11683 0 4 0 57877 55 0 0 25 0 1 0 1793445365 48451584 10683 4294967295 134512640 135167914 3221224448 3221216132 134844636 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/18991/statm): 11829 10683 162 162 0 11667 0 [pid=18991] vsize: 47316 Current children cumulated CPU time (s) 579.34 Current children cumulated vsize (Kb) 49444 [startup+590.042 s] Raw data (loadavg): 0.99 0.85 0.46 2/57 18999 Raw data (/proc/18986/stat): 18986 (minisat+_script) S 18985 18986 824 0 -1 0 314 330 0 2 0 1 0 1 17 0 1 0 1793445351 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/18986/statm): 532 234 485 147 0 385 0 [pid=18986] vsize: 2128 Raw data (/proc/18991/stat): 18991 (minisat+_bignum) R 18986 18986 824 0 -1 0 11683 0 4 0 58877 55 0 0 25 0 1 0 1793445365 48451584 10683 4294967295 134512640 135167914 3221224448 3221216400 134844644 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/18991/statm): 11829 10683 162 162 0 11667 0 [pid=18991] vsize: 47316 Current children cumulated CPU time (s) 589.34 Current children cumulated vsize (Kb) 49444 [startup+600.043 s] Raw data (loadavg): 0.99 0.86 0.46 2/57 18999 Raw data (/proc/18986/stat): 18986 (minisat+_script) S 18985 18986 824 0 -1 0 314 330 0 2 0 1 0 1 17 0 1 0 1793445351 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/18986/statm): 532 234 485 147 0 385 0 [pid=18986] vsize: 2128 Raw data (/proc/18991/stat): 18991 (minisat+_bignum) R 18986 18986 824 0 -1 0 11683 0 4 0 59878 55 0 0 25 0 1 0 1793445365 48451584 10683 4294967295 134512640 135167914 3221224448 3221216636 134723262 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/18991/statm): 11829 10683 162 162 0 11667 0 [pid=18991] vsize: 47316 Current children cumulated CPU time (s) 599.35 Current children cumulated vsize (Kb) 49444 [startup+610.044 s] Raw data (loadavg): 0.99 0.86 0.47 2/57 18999 Raw data (/proc/18986/stat): 18986 (minisat+_script) S 18985 18986 824 0 -1 0 314 330 0 2 0 1 0 1 17 0 1 0 1793445351 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/18986/statm): 532 234 485 147 0 385 0 [pid=18986] vsize: 2128 Raw data (/proc/18991/stat): 18991 (minisat+_bignum) R 18986 18986 824 0 -1 0 11683 0 4 0 60878 55 0 0 25 0 1 0 1793445365 48451584 10683 4294967295 134512640 135167914 3221224448 3221216560 134629442 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/18991/statm): 11829 10683 162 162 0 11667 0 [pid=18991] vsize: 47316 Current children cumulated CPU time (s) 609.35 Current children cumulated vsize (Kb) 49444 [startup+620.044 s] Raw data (loadavg): 0.99 0.87 0.47 2/57 18999 Raw data (/proc/18986/stat): 18986 (minisat+_script) S 18985 18986 824 0 -1 0 314 330 0 2 0 1 0 1 17 0 1 0 1793445351 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/18986/statm): 532 234 485 147 0 385 0 [pid=18986] vsize: 2128 Raw data (/proc/18991/stat): 18991 (minisat+_bignum) R 18986 18986 824 0 -1 0 11683 0 4 0 61878 55 0 0 25 0 1 0 1793445365 48451584 10683 4294967295 134512640 135167914 3221224448 3221217164 134843002 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/18991/statm): 11829 10683 162 162 0 11667 0 [pid=18991] vsize: 47316 Current children cumulated CPU time (s) 619.35 Current children cumulated vsize (Kb) 49444 [startup+630.044 s] Raw data (loadavg): 0.99 0.87 0.47 2/57 18999 Raw data (/proc/18986/stat): 18986 (minisat+_script) S 18985 18986 824 0 -1 0 314 330 0 2 0 1 0 1 17 0 1 0 1793445351 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/18986/statm): 532 234 485 147 0 385 0 [pid=18986] vsize: 2128 Raw data (/proc/18991/stat): 18991 (minisat+_bignum) R 18986 18986 824 0 -1 0 11683 0 4 0 62878 55 0 0 25 0 1 0 1793445365 48451584 10683 4294967295 134512640 135167914 3221224448 3221216640 134843400 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/18991/statm): 11829 10683 162 162 0 11667 0 [pid=18991] vsize: 47316 Current children cumulated CPU time (s) 629.35 Current children cumulated vsize (Kb) 49444 [startup+640.045 s] Raw data (loadavg): 0.99 0.87 0.48 2/57 18999 Raw data (/proc/18986/stat): 18986 (minisat+_script) S 18985 18986 824 0 -1 0 314 330 0 2 0 1 0 1 17 0 1 0 1793445351 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/18986/statm): 532 234 485 147 0 385 0 [pid=18986] vsize: 2128 Raw data (/proc/18991/stat): 18991 (minisat+_bignum) R 18986 18986 824 0 -1 0 11683 0 4 0 63879 55 0 0 25 0 1 0 1793445365 48451584 10683 4294967295 134512640 135167914 3221224448 3221216704 134849102 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/18991/statm): 11829 10683 162 162 0 11667 0 [pid=18991] vsize: 47316 Current children cumulated CPU time (s) 639.36 Current children cumulated vsize (Kb) 49444 [startup+650.045 s] Raw data (loadavg): 0.99 0.88 0.48 2/57 18999 Raw data (/proc/18986/stat): 18986 (minisat+_script) S 18985 18986 824 0 -1 0 314 330 0 2 0 1 0 1 17 0 1 0 1793445351 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/18986/statm): 532 234 485 147 0 385 0 [pid=18986] vsize: 2128 Raw data (/proc/18991/stat): 18991 (minisat+_bignum) R 18986 18986 824 0 -1 0 11683 0 4 0 64879 55 0 0 25 0 1 0 1793445365 48451584 10683 4294967295 134512640 135167914 3221224448 3221216528 134849143 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/18991/statm): 11829 10683 162 162 0 11667 0 [pid=18991] vsize: 47316 Current children cumulated CPU time (s) 649.36 Current children cumulated vsize (Kb) 49444 [startup+660.045 s] Raw data (loadavg): 0.99 0.88 0.49 2/57 18999 Raw data (/proc/18986/stat): 18986 (minisat+_script) S 18985 18986 824 0 -1 0 314 330 0 2 0 1 0 1 17 0 1 0 1793445351 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/18986/statm): 532 234 485 147 0 385 0 [pid=18986] vsize: 2128 Raw data (/proc/18991/stat): 18991 (minisat+_bignum) R 18986 18986 824 0 -1 0 11683 0 4 0 65879 55 0 0 25 0 1 0 1793445365 48451584 10683 4294967295 134512640 135167914 3221224448 3221216284 134723267 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/18991/statm): 11829 10683 162 162 0 11667 0 [pid=18991] vsize: 47316 Current children cumulated CPU time (s) 659.36 Current children cumulated vsize (Kb) 49444 [startup+670.046 s] Raw data (loadavg): 0.99 0.88 0.49 2/57 18999 Raw data (/proc/18986/stat): 18986 (minisat+_script) S 18985 18986 824 0 -1 0 314 330 0 2 0 1 0 1 17 0 1 0 1793445351 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/18986/statm): 532 234 485 147 0 385 0 [pid=18986] vsize: 2128 Raw data (/proc/18991/stat): 18991 (minisat+_bignum) R 18986 18986 824 0 -1 0 11683 0 4 0 66879 55 0 0 25 0 1 0 1793445365 48451584 10683 4294967295 134512640 135167914 3221224448 3221216456 134693626 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/18991/statm): 11829 10683 162 162 0 11667 0 [pid=18991] vsize: 47316 Current children cumulated CPU time (s) 669.36 Current children cumulated vsize (Kb) 49444 [startup+680.047 s] Raw data (loadavg): 0.99 0.89 0.50 2/57 18999 Raw data (/proc/18986/stat): 18986 (minisat+_script) S 18985 18986 824 0 -1 0 314 330 0 2 0 1 0 1 17 0 1 0 1793445351 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/18986/statm): 532 234 485 147 0 385 0 [pid=18986] vsize: 2128 Raw data (/proc/18991/stat): 18991 (minisat+_bignum) R 18986 18986 824 0 -1 0 11683 0 4 0 67879 55 0 0 25 0 1 0 1793445365 48451584 10683 4294967295 134512640 135167914 3221224448 3221216424 134844674 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/18991/statm): 11829 10683 162 162 0 11667 0 [pid=18991] vsize: 47316 Current children cumulated CPU time (s) 679.36 Current children cumulated vsize (Kb) 49444 [startup+690.047 s] Raw data (loadavg): 0.99 0.89 0.50 2/57 18999 Raw data (/proc/18986/stat): 18986 (minisat+_script) S 18985 18986 824 0 -1 0 314 330 0 2 0 1 0 1 17 0 1 0 1793445351 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/18986/statm): 532 234 485 147 0 385 0 [pid=18986] vsize: 2128 Raw data (/proc/18991/stat): 18991 (minisat+_bignum) R 18986 18986 824 0 -1 0 11683 0 4 0 68880 55 0 0 25 0 1 0 1793445365 48451584 10683 4294967295 134512640 135167914 3221224448 3221216608 134845906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/18991/statm): 11829 10683 162 162 0 11667 0 [pid=18991] vsize: 47316 Current children cumulated CPU time (s) 689.37 Current children cumulated vsize (Kb) 49444 [startup+700.048 s] Raw data (loadavg): 0.99 0.89 0.51 2/57 18999 Raw data (/proc/18986/stat): 18986 (minisat+_script) S 18985 18986 824 0 -1 0 314 330 0 2 0 1 0 1 17 0 1 0 1793445351 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/18986/statm): 532 234 485 147 0 385 0 [pid=18986] vsize: 2128 Raw data (/proc/18991/stat): 18991 (minisat+_bignum) R 18986 18986 824 0 -1 0 11683 0 4 0 69880 55 0 0 25 0 1 0 1793445365 48451584 10683 4294967295 134512640 135167914 3221224448 3221216576 134844728 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/18991/statm): 11829 10683 162 162 0 11667 0 [pid=18991] vsize: 47316 Current children cumulated CPU time (s) 699.37 Current children cumulated vsize (Kb) 49444 [startup+710.049 s] Raw data (loadavg): 0.99 0.90 0.51 2/57 18999 Raw data (/proc/18986/stat): 18986 (minisat+_script) S 18985 18986 824 0 -1 0 314 330 0 2 0 1 0 1 17 0 1 0 1793445351 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/18986/statm): 532 234 485 147 0 385 0 [pid=18986] vsize: 2128 Raw data (/proc/18991/stat): 18991 (minisat+_bignum) R 18986 18986 824 0 -1 0 11683 0 4 0 70880 55 0 0 25 0 1 0 1793445365 48451584 10683 4294967295 134512640 135167914 3221224448 3221216084 134718502 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/18991/statm): 11829 10683 162 162 0 11667 0 [pid=18991] vsize: 47316 Current children cumulated CPU time (s) 709.37 Current children cumulated vsize (Kb) 49444 [startup+720.05 s] Raw data (loadavg): 0.99 0.90 0.52 2/57 18999 Raw data (/proc/18986/stat): 18986 (minisat+_script) S 18985 18986 824 0 -1 0 314 330 0 2 0 1 0 1 17 0 1 0 1793445351 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/18986/statm): 532 234 485 147 0 385 0 [pid=18986] vsize: 2128 Raw data (/proc/18991/stat): 18991 (minisat+_bignum) R 18986 18986 824 0 -1 0 11683 0 4 0 71880 55 0 0 25 0 1 0 1793445365 48451584 10683 4294967295 134512640 135167914 3221224448 3221216560 134629448 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/18991/statm): 11829 10683 162 162 0 11667 0 [pid=18991] vsize: 47316 Current children cumulated CPU time (s) 719.37 Current children cumulated vsize (Kb) 49444 [startup+730.049 s] Raw data (loadavg): 0.99 0.90 0.52 2/57 18999 Raw data (/proc/18986/stat): 18986 (minisat+_script) S 18985 18986 824 0 -1 0 314 330 0 2 0 1 0 1 17 0 1 0 1793445351 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/18986/statm): 532 234 485 147 0 385 0 [pid=18986] vsize: 2128 Raw data (/proc/18991/stat): 18991 (minisat+_bignum) R 18986 18986 824 0 -1 0 11683 0 4 0 72881 55 0 0 25 0 1 0 1793445365 48451584 10683 4294967295 134512640 135167914 3221224448 3221216300 134843002 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/18991/statm): 11829 10683 162 162 0 11667 0 [pid=18991] vsize: 47316 Current children cumulated CPU time (s) 729.38 Current children cumulated vsize (Kb) 49444 [startup+740.05 s] Raw data (loadavg): 0.99 0.91 0.53 2/57 18999 Raw data (/proc/18986/stat): 18986 (minisat+_script) S 18985 18986 824 0 -1 0 314 330 0 2 0 1 0 1 17 0 1 0 1793445351 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/18986/statm): 532 234 485 147 0 385 0 [pid=18986] vsize: 2128 Raw data (/proc/18991/stat): 18991 (minisat+_bignum) R 18986 18986 824 0 -1 0 11683 0 4 0 73881 55 0 0 25 0 1 0 1793445365 48451584 10683 4294967295 134512640 135167914 3221224448 3221216128 134693576 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/18991/statm): 11829 10683 162 162 0 11667 0 [pid=18991] vsize: 47316 Current children cumulated CPU time (s) 739.38 Current children cumulated vsize (Kb) 49444 [startup+750.051 s] Raw data (loadavg): 0.99 0.91 0.53 2/57 18999 Raw data (/proc/18986/stat): 18986 (minisat+_script) S 18985 18986 824 0 -1 0 314 330 0 2 0 1 0 1 17 0 1 0 1793445351 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/18986/statm): 532 234 485 147 0 385 0 [pid=18986] vsize: 2128 Raw data (/proc/18991/stat): 18991 (minisat+_bignum) R 18986 18986 824 0 -1 0 11683 0 4 0 74881 55 0 0 25 0 1 0 1793445365 48451584 10683 4294967295 134512640 135167914 3221224448 3221215680 134844647 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/18991/statm): 11829 10683 162 162 0 11667 0 [pid=18991] vsize: 47316 Current children cumulated CPU time (s) 749.38 Current children cumulated vsize (Kb) 49444 [startup+760.051 s] Raw data (loadavg): 0.99 0.91 0.54 2/57 18999 Raw data (/proc/18986/stat): 18986 (minisat+_script) S 18985 18986 824 0 -1 0 314 330 0 2 0 1 0 1 17 0 1 0 1793445351 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/18986/statm): 532 234 485 147 0 385 0 [pid=18986] vsize: 2128 Raw data (/proc/18991/stat): 18991 (minisat+_bignum) R 18986 18986 824 0 -1 0 11683 0 4 0 75881 55 0 0 25 0 1 0 1793445365 48451584 10683 4294967295 134512640 135167914 3221224448 3221216512 134849163 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/18991/statm): 11829 10683 162 162 0 11667 0 [pid=18991] vsize: 47316 Current children cumulated CPU time (s) 759.38 Current children cumulated vsize (Kb) 49444 [startup+770.051 s] Raw data (loadavg): 0.99 0.91 0.54 2/57 18999 Raw data (/proc/18986/stat): 18986 (minisat+_script) S 18985 18986 824 0 -1 0 314 330 0 2 0 1 0 1 17 0 1 0 1793445351 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/18986/statm): 532 234 485 147 0 385 0 [pid=18986] vsize: 2128 Raw data (/proc/18991/stat): 18991 (minisat+_bignum) R 18986 18986 824 0 -1 0 11683 0 4 0 76881 55 0 0 25 0 1 0 1793445365 48451584 10683 4294967295 134512640 135167914 3221224448 3221216432 134845909 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/18991/statm): 11829 10683 162 162 0 11667 0 [pid=18991] vsize: 47316 Current children cumulated CPU time (s) 769.38 Current children cumulated vsize (Kb) 49444 [startup+780.052 s] Raw data (loadavg): 0.99 0.92 0.55 2/57 18999 Raw data (/proc/18986/stat): 18986 (minisat+_script) S 18985 18986 824 0 -1 0 314 330 0 2 0 1 0 1 17 0 1 0 1793445351 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/18986/statm): 532 234 485 147 0 385 0 [pid=18986] vsize: 2128 Raw data (/proc/18991/stat): 18991 (minisat+_bignum) R 18986 18986 824 0 -1 0 11683 0 4 0 77882 55 0 0 25 0 1 0 1793445365 48451584 10683 4294967295 134512640 135167914 3221224448 3221216624 134844728 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/18991/statm): 11829 10683 162 162 0 11667 0 [pid=18991] vsize: 47316 Current children cumulated CPU time (s) 779.39 Current children cumulated vsize (Kb) 49444 [startup+790.053 s] Raw data (loadavg): 0.99 0.92 0.55 2/57 18999 Raw data (/proc/18986/stat): 18986 (minisat+_script) S 18985 18986 824 0 -1 0 314 330 0 2 0 1 0 1 17 0 1 0 1793445351 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/18986/statm): 532 234 485 147 0 385 0 [pid=18986] vsize: 2128 Raw data (/proc/18991/stat): 18991 (minisat+_bignum) R 18986 18986 824 0 -1 0 11683 0 4 0 78882 55 0 0 25 0 1 0 1793445365 48451584 10683 4294967295 134512640 135167914 3221224448 3221216880 134694364 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/18991/statm): 11829 10683 162 162 0 11667 0 [pid=18991] vsize: 47316 Current children cumulated CPU time (s) 789.39 Current children cumulated vsize (Kb) 49444 [startup+800.053 s] Raw data (loadavg): 0.99 0.92 0.56 2/57 18999 Raw data (/proc/18986/stat): 18986 (minisat+_script) S 18985 18986 824 0 -1 0 314 330 0 2 0 1 0 1 17 0 1 0 1793445351 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/18986/statm): 532 234 485 147 0 385 0 [pid=18986] vsize: 2128 Raw data (/proc/18991/stat): 18991 (minisat+_bignum) R 18986 18986 824 0 -1 0 11683 0 4 0 79882 55 0 0 25 0 1 0 1793445365 48451584 10683 4294967295 134512640 135167914 3221224448 3221216540 134849088 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/18991/statm): 11829 10683 162 162 0 11667 0 [pid=18991] vsize: 47316 Current children cumulated CPU time (s) 799.39 Current children cumulated vsize (Kb) 49444 [startup+810.053 s] Raw data (loadavg): 0.99 0.92 0.56 2/57 18999 Raw data (/proc/18986/stat): 18986 (minisat+_script) S 18985 18986 824 0 -1 0 314 330 0 2 0 1 0 1 17 0 1 0 1793445351 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/18986/statm): 532 234 485 147 0 385 0 [pid=18986] vsize: 2128 Raw data (/proc/18991/stat): 18991 (minisat+_bignum) R 18986 18986 824 0 -1 0 11683 0 4 0 80882 55 0 0 25 0 1 0 1793445365 48451584 10683 4294967295 134512640 135167914 3221224448 3221216172 134722660 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/18991/statm): 11829 10683 162 162 0 11667 0 [pid=18991] vsize: 47316 Current children cumulated CPU time (s) 809.39 Current children cumulated vsize (Kb) 49444 [startup+820.054 s] Raw data (loadavg): 0.99 0.92 0.56 2/57 18999 Raw data (/proc/18986/stat): 18986 (minisat+_script) S 18985 18986 824 0 -1 0 314 330 0 2 0 1 0 1 17 0 1 0 1793445351 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/18986/statm): 532 234 485 147 0 385 0 [pid=18986] vsize: 2128 Raw data (/proc/18991/stat): 18991 (minisat+_bignum) R 18986 18986 824 0 -1 0 11683 0 4 0 81883 55 0 0 25 0 1 0 1793445365 48451584 10683 4294967295 134512640 135167914 3221224448 3221216720 134630893 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/18991/statm): 11829 10683 162 162 0 11667 0 [pid=18991] vsize: 47316 Current children cumulated CPU time (s) 819.4 Current children cumulated vsize (Kb) 49444 [startup+830.055 s] Raw data (loadavg): 0.99 0.93 0.57 2/57 18999 Raw data (/proc/18986/stat): 18986 (minisat+_script) S 18985 18986 824 0 -1 0 314 330 0 2 0 1 0 1 17 0 1 0 1793445351 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/18986/statm): 532 234 485 147 0 385 0 [pid=18986] vsize: 2128 Raw data (/proc/18991/stat): 18991 (minisat+_bignum) R 18986 18986 824 0 -1 0 11683 0 4 0 82883 55 0 0 25 0 1 0 1793445365 48451584 10683 4294967295 134512640 135167914 3221224448 3221217168 134696283 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/18991/statm): 11829 10683 162 162 0 11667 0 [pid=18991] vsize: 47316 Current children cumulated CPU time (s) 829.4 Current children cumulated vsize (Kb) 49444 [startup+840.055 s] Raw data (loadavg): 0.99 0.93 0.57 2/57 18999 Raw data (/proc/18986/stat): 18986 (minisat+_script) S 18985 18986 824 0 -1 0 314 330 0 2 0 1 0 1 17 0 1 0 1793445351 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/18986/statm): 532 234 485 147 0 385 0 [pid=18986] vsize: 2128 Raw data (/proc/18991/stat): 18991 (minisat+_bignum) R 18986 18986 824 0 -1 0 11683 0 4 0 83883 55 0 0 25 0 1 0 1793445365 48451584 10683 4294967295 134512640 135167914 3221224448 3221216272 134845911 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/18991/statm): 11829 10683 162 162 0 11667 0 [pid=18991] vsize: 47316 Current children cumulated CPU time (s) 839.4 Current children cumulated vsize (Kb) 49444 [startup+850.056 s] Raw data (loadavg): 0.99 0.93 0.58 2/57 18999 Raw data (/proc/18986/stat): 18986 (minisat+_script) S 18985 18986 824 0 -1 0 314 330 0 2 0 1 0 1 17 0 1 0 1793445351 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/18986/statm): 532 234 485 147 0 385 0 [pid=18986] vsize: 2128 Raw data (/proc/18991/stat): 18991 (minisat+_bignum) R 18986 18986 824 0 -1 0 11683 0 4 0 84883 55 0 0 25 0 1 0 1793445365 48451584 10683 4294967295 134512640 135167914 3221224448 3221216448 134844682 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/18991/statm): 11829 10683 162 162 0 11667 0 [pid=18991] vsize: 47316 Current children cumulated CPU time (s) 849.4 Current children cumulated vsize (Kb) 49444 [startup+860.056 s] Raw data (loadavg): 0.99 0.93 0.58 2/57 18999 Raw data (/proc/18986/stat): 18986 (minisat+_script) S 18985 18986 824 0 -1 0 314 330 0 2 0 1 0 1 17 0 1 0 1793445351 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/18986/statm): 532 234 485 147 0 385 0 [pid=18986] vsize: 2128 Raw data (/proc/18991/stat): 18991 (minisat+_bignum) R 18986 18986 824 0 -1 0 11683 0 4 0 85883 55 0 0 25 0 1 0 1793445365 48451584 10683 4294967295 134512640 135167914 3221224448 3221216524 134722656 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/18991/statm): 11829 10683 162 162 0 11667 0 [pid=18991] vsize: 47316 Current children cumulated CPU time (s) 859.4 Current children cumulated vsize (Kb) 49444 [startup+870.056 s] Raw data (loadavg): 0.99 0.93 0.58 2/57 18999 Raw data (/proc/18986/stat): 18986 (minisat+_script) S 18985 18986 824 0 -1 0 314 330 0 2 0 1 0 1 17 0 1 0 1793445351 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/18986/statm): 532 234 485 147 0 385 0 [pid=18986] vsize: 2128 Raw data (/proc/18991/stat): 18991 (minisat+_bignum) R 18986 18986 824 0 -1 0 11683 0 4 0 86884 55 0 0 25 0 1 0 1793445365 48451584 10683 4294967295 134512640 135167914 3221224448 3221216272 134845888 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/18991/statm): 11829 10683 162 162 0 11667 0 [pid=18991] vsize: 47316 Current children cumulated CPU time (s) 869.41 Current children cumulated vsize (Kb) 49444 [startup+880.056 s] Raw data (loadavg): 0.99 0.93 0.59 2/57 18999 Raw data (/proc/18986/stat): 18986 (minisat+_script) S 18985 18986 824 0 -1 0 314 330 0 2 0 1 0 1 17 0 1 0 1793445351 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/18986/statm): 532 234 485 147 0 385 0 [pid=18986] vsize: 2128 Raw data (/proc/18991/stat): 18991 (minisat+_bignum) R 18986 18986 824 0 -1 0 11683 0 4 0 87884 55 0 0 25 0 1 0 1793445365 48451584 10683 4294967295 134512640 135167914 3221224448 3221216448 134845921 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/18991/statm): 11829 10683 162 162 0 11667 0 [pid=18991] vsize: 47316 Current children cumulated CPU time (s) 879.41 Current children cumulated vsize (Kb) 49444 [startup+890.058 s] Raw data (loadavg): 0.99 0.94 0.59 2/57 18999 Raw data (/proc/18986/stat): 18986 (minisat+_script) S 18985 18986 824 0 -1 0 314 330 0 2 0 1 0 1 17 0 1 0 1793445351 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/18986/statm): 532 234 485 147 0 385 0 [pid=18986] vsize: 2128 Raw data (/proc/18991/stat): 18991 (minisat+_bignum) R 18986 18986 824 0 -1 0 11683 0 4 0 88884 55 0 0 25 0 1 0 1793445365 48451584 10683 4294967295 134512640 135167914 3221224448 3221217428 134629281 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/18991/statm): 11829 10683 162 162 0 11667 0 [pid=18991] vsize: 47316 Current children cumulated CPU time (s) 889.41 Current children cumulated vsize (Kb) 49444 [startup+900.059 s] Raw data (loadavg): 0.99 0.94 0.59 2/57 18999 Raw data (/proc/18986/stat): 18986 (minisat+_script) S 18985 18986 824 0 -1 0 314 330 0 2 0 1 0 1 17 0 1 0 1793445351 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/18986/statm): 532 234 485 147 0 385 0 [pid=18986] vsize: 2128 Raw data (/proc/18991/stat): 18991 (minisat+_bignum) R 18986 18986 824 0 -1 0 11683 0 4 0 89884 55 0 0 25 0 1 0 1793445365 48451584 10683 4294967295 134512640 135167914 3221224448 3221216480 134695319 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/18991/statm): 11829 10683 162 162 0 11667 0 [pid=18991] vsize: 47316 Current children cumulated CPU time (s) 899.41 Current children cumulated vsize (Kb) 49444 [startup+910.058 s] Raw data (loadavg): 0.99 0.94 0.60 2/57 18999 Raw data (/proc/18986/stat): 18986 (minisat+_script) S 18985 18986 824 0 -1 0 314 330 0 2 0 1 0 1 17 0 1 0 1793445351 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/18986/statm): 532 234 485 147 0 385 0 [pid=18986] vsize: 2128 Raw data (/proc/18991/stat): 18991 (minisat+_bignum) R 18986 18986 824 0 -1 0 11683 0 4 0 90885 55 0 0 25 0 1 0 1793445365 48451584 10683 4294967295 134512640 135167914 3221224448 3221216508 134845876 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/18991/statm): 11829 10683 162 162 0 11667 0 [pid=18991] vsize: 47316 Current children cumulated CPU time (s) 909.42 Current children cumulated vsize (Kb) 49444 [startup+920.059 s] Raw data (loadavg): 0.99 0.94 0.60 2/57 18999 Raw data (/proc/18986/stat): 18986 (minisat+_script) S 18985 18986 824 0 -1 0 314 330 0 2 0 1 0 1 17 0 1 0 1793445351 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/18986/statm): 532 234 485 147 0 385 0 [pid=18986] vsize: 2128 Raw data (/proc/18991/stat): 18991 (minisat+_bignum) R 18986 18986 824 0 -1 0 11683 0 4 0 91885 55 0 0 25 0 1 0 1793445365 48451584 10683 4294967295 134512640 135167914 3221224448 3221217008 134849108 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/18991/statm): 11829 10683 162 162 0 11667 0 [pid=18991] vsize: 47316 Current children cumulated CPU time (s) 919.42 Current children cumulated vsize (Kb) 49444 [startup+930.059 s] Raw data (loadavg): 0.99 0.94 0.61 2/57 18999 Raw data (/proc/18986/stat): 18986 (minisat+_script) S 18985 18986 824 0 -1 0 314 330 0 2 0 1 0 1 17 0 1 0 1793445351 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/18986/statm): 532 234 485 147 0 385 0 [pid=18986] vsize: 2128 Raw data (/proc/18991/stat): 18991 (minisat+_bignum) R 18986 18986 824 0 -1 0 11683 0 4 0 92885 55 0 0 25 0 1 0 1793445365 48451584 10683 4294967295 134512640 135167914 3221224448 3221216736 134844703 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/18991/statm): 11829 10683 162 162 0 11667 0 [pid=18991] vsize: 47316 Current children cumulated CPU time (s) 929.42 Current children cumulated vsize (Kb) 49444 [startup+940.059 s] Raw data (loadavg): 0.99 0.94 0.61 2/57 18999 Raw data (/proc/18986/stat): 18986 (minisat+_script) S 18985 18986 824 0 -1 0 314 330 0 2 0 1 0 1 17 0 1 0 1793445351 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/18986/statm): 532 234 485 147 0 385 0 [pid=18986] vsize: 2128 Raw data (/proc/18991/stat): 18991 (minisat+_bignum) R 18986 18986 824 0 -1 0 11683 0 4 0 93885 55 0 0 25 0 1 0 1793445365 48451584 10683 4294967295 134512640 135167914 3221224448 3221216880 134849102 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/18991/statm): 11829 10683 162 162 0 11667 0 [pid=18991] vsize: 47316 Current children cumulated CPU time (s) 939.42 Current children cumulated vsize (Kb) 49444 [startup+950.06 s] Raw data (loadavg): 0.99 0.95 0.61 2/57 18999 Raw data (/proc/18986/stat): 18986 (minisat+_script) S 18985 18986 824 0 -1 0 314 330 0 2 0 1 0 1 17 0 1 0 1793445351 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/18986/statm): 532 234 485 147 0 385 0 [pid=18986] vsize: 2128 Raw data (/proc/18991/stat): 18991 (minisat+_bignum) R 18986 18986 824 0 -1 0 11683 0 4 0 94885 55 0 0 25 0 1 0 1793445365 48451584 10683 4294967295 134512640 135167914 3221224448 3221216560 134844708 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/18991/statm): 11829 10683 162 162 0 11667 0 [pid=18991] vsize: 47316 Current children cumulated CPU time (s) 949.42 Current children cumulated vsize (Kb) 49444 [startup+960.061 s] Raw data (loadavg): 0.99 0.95 0.62 2/57 18999 Raw data (/proc/18986/stat): 18986 (minisat+_script) S 18985 18986 824 0 -1 0 314 330 0 2 0 1 0 1 17 0 1 0 1793445351 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/18986/statm): 532 234 485 147 0 385 0 [pid=18986] vsize: 2128 Raw data (/proc/18991/stat): 18991 (minisat+_bignum) R 18986 18986 824 0 -1 0 11683 0 4 0 95886 55 0 0 25 0 1 0 1793445365 48451584 10683 4294967295 134512640 135167914 3221224448 3221216448 134845901 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/18991/statm): 11829 10683 162 162 0 11667 0 [pid=18991] vsize: 47316 Current children cumulated CPU time (s) 959.43 Current children cumulated vsize (Kb) 49444 [startup+970.062 s] Raw data (loadavg): 0.99 0.95 0.62 2/57 18999 Raw data (/proc/18986/stat): 18986 (minisat+_script) S 18985 18986 824 0 -1 0 314 330 0 2 0 1 0 1 17 0 1 0 1793445351 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/18986/statm): 532 234 485 147 0 385 0 [pid=18986] vsize: 2128 Raw data (/proc/18991/stat): 18991 (minisat+_bignum) R 18986 18986 824 0 -1 0 11683 0 4 0 96886 55 0 0 25 0 1 0 1793445365 48451584 10683 4294967295 134512640 135167914 3221224448 3221216172 134843002 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/18991/statm): 11829 10683 162 162 0 11667 0 [pid=18991] vsize: 47316 Current children cumulated CPU time (s) 969.43 Current children cumulated vsize (Kb) 49444 [startup+980.061 s] Raw data (loadavg): 0.99 0.95 0.63 2/57 18999 Raw data (/proc/18986/stat): 18986 (minisat+_script) S 18985 18986 824 0 -1 0 314 330 0 2 0 1 0 1 17 0 1 0 1793445351 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/18986/statm): 532 234 485 147 0 385 0 [pid=18986] vsize: 2128 Raw data (/proc/18991/stat): 18991 (minisat+_bignum) R 18986 18986 824 0 -1 0 11683 0 4 0 97886 55 0 0 25 0 1 0 1793445365 48451584 10683 4294967295 134512640 135167914 3221224448 3221216684 134845876 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/18991/statm): 11829 10683 162 162 0 11667 0 [pid=18991] vsize: 47316 Current children cumulated CPU time (s) 979.43 Current children cumulated vsize (Kb) 49444 [startup+990.062 s] Raw data (loadavg): 0.99 0.95 0.63 2/57 18999 Raw data (/proc/18986/stat): 18986 (minisat+_script) S 18985 18986 824 0 -1 0 314 330 0 2 0 1 0 1 17 0 1 0 1793445351 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/18986/statm): 532 234 485 147 0 385 0 [pid=18986] vsize: 2128 Raw data (/proc/18991/stat): 18991 (minisat+_bignum) R 18986 18986 824 0 -1 0 11683 0 4 0 98886 55 0 0 25 0 1 0 1793445365 48451584 10683 4294967295 134512640 135167914 3221224448 3221216128 134720503 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/18991/statm): 11829 10683 162 162 0 11667 0 [pid=18991] vsize: 47316 Current children cumulated CPU time (s) 989.43 Current children cumulated vsize (Kb) 49444 [startup+1000.06 s] Raw data (loadavg): 0.99 0.95 0.63 2/57 18999 Raw data (/proc/18986/stat): 18986 (minisat+_script) S 18985 18986 824 0 -1 0 314 330 0 2 0 1 0 1 17 0 1 0 1793445351 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/18986/statm): 532 234 485 147 0 385 0 [pid=18986] vsize: 2128 Raw data (/proc/18991/stat): 18991 (minisat+_bignum) R 18986 18986 824 0 -1 0 11683 0 4 0 99887 55 0 0 25 0 1 0 1793445365 48451584 10683 4294967295 134512640 135167914 3221224448 3221215920 134843036 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/18991/statm): 11829 10683 162 162 0 11667 0 [pid=18991] vsize: 47316 Current children cumulated CPU time (s) 999.44 Current children cumulated vsize (Kb) 49444 [startup+1010.06 s] Raw data (loadavg): 0.99 0.95 0.64 2/57 18999 Raw data (/proc/18986/stat): 18986 (minisat+_script) S 18985 18986 824 0 -1 0 314 330 0 2 0 1 0 1 17 0 1 0 1793445351 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/18986/statm): 532 234 485 147 0 385 0 [pid=18986] vsize: 2128 Raw data (/proc/18991/stat): 18991 (minisat+_bignum) R 18986 18986 824 0 -1 0 11683 0 4 0 100887 55 0 0 25 0 1 0 1793445365 48451584 10683 4294967295 134512640 135167914 3221224448 3221216864 134694386 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/18991/statm): 11829 10683 162 162 0 11667 0 [pid=18991] vsize: 47316 Current children cumulated CPU time (s) 1009.44 Current children cumulated vsize (Kb) 49444 [startup+1020.06 s] Raw data (loadavg): 0.99 0.95 0.64 2/57 18999 Raw data (/proc/18986/stat): 18986 (minisat+_script) S 18985 18986 824 0 -1 0 314 330 0 2 0 1 0 1 17 0 1 0 1793445351 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/18986/statm): 532 234 485 147 0 385 0 [pid=18986] vsize: 2128 Raw data (/proc/18991/stat): 18991 (minisat+_bignum) R 18986 18986 824 0 -1 0 11683 0 4 0 101887 55 0 0 25 0 1 0 1793445365 48451584 10683 4294967295 134512640 135167914 3221224448 3221216540 134842996 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/18991/statm): 11829 10683 162 162 0 11667 0 [pid=18991] vsize: 47316 Current children cumulated CPU time (s) 1019.44 Current children cumulated vsize (Kb) 49444 [startup+1030.07 s] Raw data (loadavg): 0.99 0.95 0.64 2/57 18999 Raw data (/proc/18986/stat): 18986 (minisat+_script) S 18985 18986 824 0 -1 0 314 330 0 2 0 1 0 1 17 0 1 0 1793445351 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/18986/statm): 532 234 485 147 0 385 0 [pid=18986] vsize: 2128 Raw data (/proc/18991/stat): 18991 (minisat+_bignum) R 18986 18986 824 0 -1 0 11683 0 4 0 102887 55 0 0 25 0 1 0 1793445365 48451584 10683 4294967295 134512640 135167914 3221224448 3221216984 134693693 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/18991/statm): 11829 10683 162 162 0 11667 0 [pid=18991] vsize: 47316 Current children cumulated CPU time (s) 1029.44 Current children cumulated vsize (Kb) 49444 [startup+1040.07 s] Raw data (loadavg): 0.99 0.95 0.65 2/57 18999 Raw data (/proc/18986/stat): 18986 (minisat+_script) S 18985 18986 824 0 -1 0 314 330 0 2 0 1 0 1 17 0 1 0 1793445351 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/18986/statm): 532 234 485 147 0 385 0 [pid=18986] vsize: 2128 Raw data (/proc/18991/stat): 18991 (minisat+_bignum) R 18986 18986 824 0 -1 0 11683 0 4 0 103888 55 0 0 25 0 1 0 1793445365 48451584 10683 4294967295 134512640 135167914 3221224448 3221217056 134693563 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/18991/statm): 11829 10683 162 162 0 11667 0 [pid=18991] vsize: 47316 Current children cumulated CPU time (s) 1039.45 Current children cumulated vsize (Kb) 49444 [startup+1050.07 s] Raw data (loadavg): 0.99 0.95 0.65 2/57 18999 Raw data (/proc/18986/stat): 18986 (minisat+_script) S 18985 18986 824 0 -1 0 314 330 0 2 0 1 0 1 17 0 1 0 1793445351 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/18986/statm): 532 234 485 147 0 385 0 [pid=18986] vsize: 2128 Raw data (/proc/18991/stat): 18991 (minisat+_bignum) R 18986 18986 824 0 -1 0 11683 0 4 0 104888 55 0 0 25 0 1 0 1793445365 48451584 10683 4294967295 134512640 135167914 3221224448 3221216256 134845913 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/18991/statm): 11829 10683 162 162 0 11667 0 [pid=18991] vsize: 47316 Current children cumulated CPU time (s) 1049.45 Current children cumulated vsize (Kb) 49444 [startup+1060.07 s] Raw data (loadavg): 0.99 0.96 0.65 2/57 18999 Raw data (/proc/18986/stat): 18986 (minisat+_script) S 18985 18986 824 0 -1 0 314 330 0 2 0 1 0 1 17 0 1 0 1793445351 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/18986/statm): 532 234 485 147 0 385 0 [pid=18986] vsize: 2128 Raw data (/proc/18991/stat): 18991 (minisat+_bignum) R 18986 18986 824 0 -1 0 11683 0 4 0 105888 55 0 0 25 0 1 0 1793445365 48451584 10683 4294967295 134512640 135167914 3221224448 3221216352 134849068 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/18991/statm): 11829 10683 162 162 0 11667 0 [pid=18991] vsize: 47316 Current children cumulated CPU time (s) 1059.45 Current children cumulated vsize (Kb) 49444 [startup+1070.07 s] Raw data (loadavg): 0.99 0.96 0.66 2/57 18999 Raw data (/proc/18986/stat): 18986 (minisat+_script) S 18985 18986 824 0 -1 0 314 330 0 2 0 1 0 1 17 0 1 0 1793445351 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/18986/statm): 532 234 485 147 0 385 0 [pid=18986] vsize: 2128 Raw data (/proc/18991/stat): 18991 (minisat+_bignum) R 18986 18986 824 0 -1 0 11683 0 4 0 106888 55 0 0 25 0 1 0 1793445365 48451584 10683 4294967295 134512640 135167914 3221224448 3221216336 134849163 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/18991/statm): 11829 10683 162 162 0 11667 0 [pid=18991] vsize: 47316 Current children cumulated CPU time (s) 1069.45 Current children cumulated vsize (Kb) 49444 [startup+1080.07 s] Raw data (loadavg): 0.99 0.96 0.66 2/57 18999 Raw data (/proc/18986/stat): 18986 (minisat+_script) S 18985 18986 824 0 -1 0 314 330 0 2 0 1 0 1 17 0 1 0 1793445351 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/18986/statm): 532 234 485 147 0 385 0 [pid=18986] vsize: 2128 Raw data (/proc/18991/stat): 18991 (minisat+_bignum) R 18986 18986 824 0 -1 0 11683 0 4 0 107888 55 0 0 25 0 1 0 1793445365 48451584 10683 4294967295 134512640 135167914 3221224448 3221216108 134723262 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/18991/statm): 11829 10683 162 162 0 11667 0 [pid=18991] vsize: 47316 Current children cumulated CPU time (s) 1079.45 Current children cumulated vsize (Kb) 49444 [startup+1090.07 s] Raw data (loadavg): 0.99 0.96 0.66 2/57 18999 Raw data (/proc/18986/stat): 18986 (minisat+_script) S 18985 18986 824 0 -1 0 314 330 0 2 0 1 0 1 17 0 1 0 1793445351 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/18986/statm): 532 234 485 147 0 385 0 [pid=18986] vsize: 2128 Raw data (/proc/18991/stat): 18991 (minisat+_bignum) R 18986 18986 824 0 -1 0 11683 0 4 0 108889 55 0 0 25 0 1 0 1793445365 48451584 10683 4294967295 134512640 135167914 3221224448 3221216512 134694528 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/18991/statm): 11829 10683 162 162 0 11667 0 [pid=18991] vsize: 47316 Current children cumulated CPU time (s) 1089.46 Current children cumulated vsize (Kb) 49444 [startup+1100.07 s] Raw data (loadavg): 0.99 0.96 0.66 2/57 18999 Raw data (/proc/18986/stat): 18986 (minisat+_script) S 18985 18986 824 0 -1 0 314 330 0 2 0 1 0 1 17 0 1 0 1793445351 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/18986/statm): 532 234 485 147 0 385 0 [pid=18986] vsize: 2128 Raw data (/proc/18991/stat): 18991 (minisat+_bignum) R 18986 18986 824 0 -1 0 11683 0 4 0 109889 55 0 0 25 0 1 0 1793445365 48451584 10683 4294967295 134512640 135167914 3221224448 3221216284 134723267 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/18991/statm): 11829 10683 162 162 0 11667 0 [pid=18991] vsize: 47316 Current children cumulated CPU time (s) 1099.46 Current children cumulated vsize (Kb) 49444 [startup+1110.07 s] Raw data (loadavg): 0.99 0.96 0.67 2/57 18999 Raw data (/proc/18986/stat): 18986 (minisat+_script) S 18985 18986 824 0 -1 0 314 330 0 2 0 1 0 1 17 0 1 0 1793445351 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/18986/statm): 532 234 485 147 0 385 0 [pid=18986] vsize: 2128 Raw data (/proc/18991/stat): 18991 (minisat+_bignum) R 18986 18986 824 0 -1 0 11683 0 4 0 110889 55 0 0 25 0 1 0 1793445365 48451584 10683 4294967295 134512640 135167914 3221224448 3221216256 134718501 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/18991/statm): 11829 10683 162 162 0 11667 0 [pid=18991] vsize: 47316 Current children cumulated CPU time (s) 1109.46 Current children cumulated vsize (Kb) 49444 [startup+1120.07 s] Raw data (loadavg): 0.99 0.96 0.67 2/57 18999 Raw data (/proc/18986/stat): 18986 (minisat+_script) S 18985 18986 824 0 -1 0 314 330 0 2 0 1 0 1 17 0 1 0 1793445351 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/18986/statm): 532 234 485 147 0 385 0 [pid=18986] vsize: 2128 Raw data (/proc/18991/stat): 18991 (minisat+_bignum) R 18986 18986 824 0 -1 0 11683 0 4 0 111889 55 0 0 25 0 1 0 1793445365 48451584 10683 4294967295 134512640 135167914 3221224448 3221216688 134849092 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/18991/statm): 11829 10683 162 162 0 11667 0 [pid=18991] vsize: 47316 Current children cumulated CPU time (s) 1119.46 Current children cumulated vsize (Kb) 49444 [startup+1130.07 s] Raw data (loadavg): 0.99 0.96 0.67 2/57 18999 Raw data (/proc/18986/stat): 18986 (minisat+_script) S 18985 18986 824 0 -1 0 314 330 0 2 0 1 0 1 17 0 1 0 1793445351 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/18986/statm): 532 234 485 147 0 385 0 [pid=18986] vsize: 2128 Raw data (/proc/18991/stat): 18991 (minisat+_bignum) R 18986 18986 824 0 -1 0 11683 0 4 0 112890 55 0 0 25 0 1 0 1793445365 48451584 10683 4294967295 134512640 135167914 3221224448 3221216384 134629024 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/18991/statm): 11829 10683 162 162 0 11667 0 [pid=18991] vsize: 47316 Current children cumulated CPU time (s) 1129.47 Current children cumulated vsize (Kb) 49444 [startup+1140.07 s] Raw data (loadavg): 0.99 0.96 0.68 2/57 18999 Raw data (/proc/18986/stat): 18986 (minisat+_script) S 18985 18986 824 0 -1 0 314 330 0 2 0 1 0 1 17 0 1 0 1793445351 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/18986/statm): 532 234 485 147 0 385 0 [pid=18986] vsize: 2128 Raw data (/proc/18991/stat): 18991 (minisat+_bignum) R 18986 18986 824 0 -1 0 11683 0 4 0 113890 55 0 0 25 0 1 0 1793445365 48451584 10683 4294967295 134512640 135167914 3221224448 3221216360 134693734 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/18991/statm): 11829 10683 162 162 0 11667 0 [pid=18991] vsize: 47316 Current children cumulated CPU time (s) 1139.47 Current children cumulated vsize (Kb) 49444 [startup+1150.07 s] Raw data (loadavg): 0.99 0.96 0.68 2/57 18999 Raw data (/proc/18986/stat): 18986 (minisat+_script) S 18985 18986 824 0 -1 0 314 330 0 2 0 1 0 1 17 0 1 0 1793445351 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/18986/statm): 532 234 485 147 0 385 0 [pid=18986] vsize: 2128 Raw data (/proc/18991/stat): 18991 (minisat+_bignum) R 18986 18986 824 0 -1 0 11683 0 4 0 114890 55 0 0 25 0 1 0 1793445365 48451584 10683 4294967295 134512640 135167914 3221224448 3221216544 134629069 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/18991/statm): 11829 10683 162 162 0 11667 0 [pid=18991] vsize: 47316 Current children cumulated CPU time (s) 1149.47 Current children cumulated vsize (Kb) 49444 [startup+1160.07 s] Raw data (loadavg): 0.99 0.97 0.68 2/57 18999 Raw data (/proc/18986/stat): 18986 (minisat+_script) S 18985 18986 824 0 -1 0 314 330 0 2 0 1 0 1 17 0 1 0 1793445351 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/18986/statm): 532 234 485 147 0 385 0 [pid=18986] vsize: 2128 Raw data (/proc/18991/stat): 18991 (minisat+_bignum) R 18986 18986 824 0 -1 0 11683 0 4 0 115890 55 0 0 25 0 1 0 1793445365 48451584 10683 4294967295 134512640 135167914 3221224448 3221216624 134696710 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/18991/statm): 11829 10683 162 162 0 11667 0 [pid=18991] vsize: 47316 Current children cumulated CPU time (s) 1159.47 Current children cumulated vsize (Kb) 49444 [startup+1170.07 s] Raw data (loadavg): 0.99 0.97 0.68 2/57 18999 Raw data (/proc/18986/stat): 18986 (minisat+_script) S 18985 18986 824 0 -1 0 314 330 0 2 0 1 0 1 17 0 1 0 1793445351 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/18986/statm): 532 234 485 147 0 385 0 [pid=18986] vsize: 2128 Raw data (/proc/18991/stat): 18991 (minisat+_bignum) R 18986 18986 824 0 -1 0 11683 0 4 0 116891 55 0 0 25 0 1 0 1793445365 48451584 10683 4294967295 134512640 135167914 3221224448 3221216688 134843153 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/18991/statm): 11829 10683 162 162 0 11667 0 [pid=18991] vsize: 47316 Current children cumulated CPU time (s) 1169.48 Current children cumulated vsize (Kb) 49444 [startup+1180.07 s] Raw data (loadavg): 0.99 0.97 0.69 2/57 18999 Raw data (/proc/18986/stat): 18986 (minisat+_script) S 18985 18986 824 0 -1 0 314 330 0 2 0 1 0 1 17 0 1 0 1793445351 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/18986/statm): 532 234 485 147 0 385 0 [pid=18986] vsize: 2128 Raw data (/proc/18991/stat): 18991 (minisat+_bignum) R 18986 18986 824 0 -1 0 11683 0 4 0 117891 55 0 0 25 0 1 0 1793445365 48451584 10683 4294967295 134512640 135167914 3221224448 3221216624 134845933 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/18991/statm): 11829 10683 162 162 0 11667 0 [pid=18991] vsize: 47316 Current children cumulated CPU time (s) 1179.48 Current children cumulated vsize (Kb) 49444 [startup+1190.07 s] Raw data (loadavg): 0.99 0.97 0.69 2/57 18999 Raw data (/proc/18986/stat): 18986 (minisat+_script) S 18985 18986 824 0 -1 0 314 330 0 2 0 1 0 1 17 0 1 0 1793445351 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/18986/statm): 532 234 485 147 0 385 0 [pid=18986] vsize: 2128 Raw data (/proc/18991/stat): 18991 (minisat+_bignum) R 18986 18986 824 0 -1 0 11683 0 4 0 118891 55 0 0 25 0 1 0 1793445365 48451584 10683 4294967295 134512640 135167914 3221224448 3221217088 134844689 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/18991/statm): 11829 10683 162 162 0 11667 0 [pid=18991] vsize: 47316 Current children cumulated CPU time (s) 1189.48 Current children cumulated vsize (Kb) 49444 [startup+1200.07 s] Raw data (loadavg): 0.99 0.97 0.69 2/57 18999 Raw data (/proc/18986/stat): 18986 (minisat+_script) S 18985 18986 824 0 -1 0 314 330 0 2 0 1 0 1 17 0 1 0 1793445351 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/18986/statm): 532 234 485 147 0 385 0 [pid=18986] vsize: 2128 Raw data (/proc/18991/stat): 18991 (minisat+_bignum) R 18986 18986 824 0 -1 0 11683 0 4 0 119891 55 0 0 25 0 1 0 1793445365 48451584 10683 4294967295 134512640 135167914 3221224448 3221216976 134845890 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/18991/statm): 11829 10683 162 162 0 11667 0 [pid=18991] vsize: 47316 Current children cumulated CPU time (s) 1199.48 Current children cumulated vsize (Kb) 49444 [startup+1210.07 s] Raw data (loadavg): 0.99 0.97 0.70 2/57 18999 Raw data (/proc/18986/stat): 18986 (minisat+_script) S 18985 18986 824 0 -1 0 314 330 0 2 0 1 0 1 17 0 1 0 1793445351 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/18986/statm): 532 234 485 147 0 385 0 [pid=18986] vsize: 2128 Raw data (/proc/18991/stat): 18991 (minisat+_bignum) R 18986 18986 824 0 -1 0 11683 0 4 0 120891 55 0 0 25 0 1 0 1793445365 48451584 10683 4294967295 134512640 135167914 3221224448 3221216288 134843026 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/18991/statm): 11829 10683 162 162 0 11667 0 [pid=18991] vsize: 47316 Current children cumulated CPU time (s) 1209.48 Current children cumulated vsize (Kb) 49444 Maximum CPU time exceeded: sending SIGTERM then SIGKILL [startup+1210.08 s] Raw data (loadavg): 0.99 0.97 0.70 2/57 18999 Raw data (/proc/18986/stat): 18986 (minisat+_script) S 18985 18986 824 0 -1 0 314 330 0 2 0 1 0 1 17 0 1 0 1793445351 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/18986/statm): 532 234 485 147 0 385 0 [pid=18986] vsize: 2128 Raw data (/proc/18991/stat): 18991 (minisat+_bignum) R 18986 18986 824 0 -1 0 11683 0 4 0 120892 55 0 0 25 0 1 0 1793445365 48451584 10683 4294967295 134512640 135167914 3221224448 3221216288 134843068 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/18991/statm): 11829 10683 162 162 0 11667 0 [pid=18991] vsize: 47316 Current children cumulated CPU time (s) 1209.49 Current children cumulated vsize (Kb) 49444 Sending SIGTERM to -18986 Sleeping 2 seconds One traced child (pid=18986) ended because it received signal 15 (SIGTERM) One traced child (pid=18991) exited with status: 10 All traced children have exited ! Game is over. Child status: 10 Real time (s): 1210.11 CPU time (s): 1209.51 CPU user time (s): 1208.92 CPU system time (s): 0.581911 CPU usage (%): 99.9503 Max. virtual memory (cumulated for all children) (Kb): 49444
ERROR: no interpretation found !