Name | mps-v2-20-10/MIPLIB/miplib/normalized-mps-v2-20-10-bell4.opb |
MD5SUM | 3cce8c056d32fd25c784b4e9cbdd2db6 |
Bench Category | optimization, big integers (OPTBIGINT) |
Has Objective Function | YES |
Satisfiable | YES |
(Un)Satisfiability was proved | YES |
Best value of the objective function | 540233279610250 |
Optimality of the best value was proved | NO |
Number of terms in the objective function | 1527 |
Biggest coefficient in the objective function | 4949278720000000 |
Number of bits for the biggest coefficient in the objective function | 53 |
Sum of the numbers in the objective function | 114314457147588882 |
Number of bits of the sum of numbers in the objective function | 57 |
Biggest number in a constraint | 4949278720000000 |
Number of bits of the biggest number in a constraint | 53 |
Biggest sum of numbers in a constraint | 114314457147588882 |
Number of bits of the biggest sum of numbers | 57 |
Best result obtained on this benchmark | SAT |
Best CPU time to get the best result obtained on this benchmark | 1195.07 |
Number of variables | 1996 |
Total number of constraints | 169 |
Number of constraints which are clauses | 18 |
Number of constraints which are cardinality constraints (but not clauses) | 34 |
Number of constraints which are nor clauses,nor cardinality constraints | 117 |
Minimum length of a constraint | 1 |
Maximum length of a constraint | 135 |
LAUNCH ON wulflinc18 THE 2005-09-19 03:05:14 (client local time) PB2005-SCRIPT v4.0 MARKUPS: idlaunch=2846 boxname=wulflinc18 idbench=502 idsolver=3 numberseed=0 MD5SUM SOLVER: MD5SUM BENCH: 3cce8c056d32fd25c784b4e9cbdd2db6 /oldhome/oroussel/tmp/wulflinc18/normalized-mps-v2-20-10-bell4.opb REAL COMMAND: minisat+_script /oldhome/oroussel/tmp/wulflinc18/normalized-mps-v2-20-10-bell4.opb IDLAUNCH: 2846 /proc/cpuinfo: processor : 0 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 3 cpu MHz : 451.177 cache size : 512 KB fdiv_bug : no hlt_bug : no f00f_bug : no coma_bug : no fpu : yes fpu_exception : yes cpuid level : 2 wp : yes flags : fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse bogomips : 888.83 processor : 1 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 3 cpu MHz : 451.177 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: 891056 kB Buffers: 35220 kB Cached: 74164 kB SwapCached: 844 kB Active: 48428 kB Inactive: 63588 kB HighTotal: 131008 kB HighFree: 53648 kB LowTotal: 903652 kB LowFree: 837408 kB SwapTotal: 2097892 kB SwapFree: 2096548 kB Dirty: 28 kB Writeback: 0 kB Mapped: 5764 kB Slab: 25848 kB Committed_AS: 64184 kB PageTables: 328 kB VmallocTotal: 114680 kB VmallocUsed: 1368 kB VmallocChunk: 113252 kB JOB ENDED THE 2005-09-19 03:25:25 (client local time) WITH STATUS 10 IN 1209.95 SECONDS stats: 2846 7 1209.95 10
c Parsing PB file... c PARSE ERROR! [line 121] Integer overflow. Use BigNum-version. c OK -- Running BigNum-version instead... c Parsing PB file... c Converting 134 PB-constraints to clauses... c -- Unit propagations: ppppppppppp c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): ssssss..................ssss c ---[ 128]---> BDD-cost: 13 c ---[ 127]---> BDD-cost: 13 c ---[ 126]---> BDD-cost: 13 c ---[ 125]---> BDD-cost: 13 c ---[ 124]---> BDD-cost: 13 c ---[ 123]---> BDD-cost: 13 c ---[ 122]---> BDD-cost: 13 c ---[ 121]---> BDD-cost: 13 c ---[ 120]---> BDD-cost: 13 c ---[ 95]---> BDD-cost: 9 c ---[ 94]---> BDD-cost: 9 c ---[ 93]---> BDD-cost: 9 c ---[ 92]---> BDD-cost: 9 c ---[ 91]---> BDD-cost: 9 c ---[ 90]---> BDD-cost: 9 c ---[ 89]---> BDD-cost: 9 c ---[ 88]---> BDD-cost: 9 c ---[ 87]---> BDD-cost: 9 c ---[ 86]---> BDD-cost: 9 c ---[ 85]---> BDD-cost: 9 c ---[ 84]---> BDD-cost: 9 c ---[ 83]---> BDD-cost: 9 c ---[ 82]---> BDD-cost: 9 c ---[ 81]---> BDD-cost: 9 c ---[ 80]---> 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 ---[ 79]---> Sorter-cost: 513 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 ---[ 78]---> Sorter-cost: 1482 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]---> Sorter-cost: 1469 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 ---[ 76]---> 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 ---[ 75]---> BDD-cost: 73 c ---[ 74]---> 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 ---[ 73]---> BDD-cost: 75 c ---[ 72]---> BDD-cost: 71 c ---[ 71]---> 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 ---[ 70]---> Sorter-cost: 978 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 ---[ 69]---> Sorter-cost: 978 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 ---[ 68]---> Sorter-cost: 978 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 ---[ 67]---> Sorter-cost: 1482 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 ---[ 66]---> Sorter-cost: 1458 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 ---[ 65]---> Sorter-cost: 952 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 ---[ 64]---> 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 ---[ 63]---> Sorter-cost: 557 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 ---[ 62]---> BDD-cost: 131 c ---[ 61]---> BDD-cost: 106 c ---[ 60]---> BDD-cost: 106 c ---[ 59]---> BDD-cost: 106 c ---[ 58]---> BDD-cost: 106 c ---[ 57]---> BDD-cost: 106 c ---[ 56]---> BDD-cost: 106 c ---[ 55]---> BDD-cost: 131 c ---[ 54]---> BDD-cost: 131 c ---[ 53]---> BDD-cost: 131 c ---[ 52]---> BDD-cost: 131 c ---[ 51]---> BDD-cost: 131 c ---[ 50]---> BDD-cost: 122 c ---[ 49]---> BDD-cost: 131 c ---[ 48]---> BDD-cost: 131 c ---[ 47]---> BDD-cost: 219 c ---[ 45]---> Sorter-cost: 883 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 ---[ 44]---> Sorter-cost: 877 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 42]---> BDD-cost: 79 c ---[ 41]---> Sorter-cost: 494 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 ---[ 39]---> BDD-cost: 85 c ---[ 38]---> BDD-cost: 81 c ---[ 37]---> BDD-cost: 81 c ---[ 36]---> 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 ---[ 35]---> 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 ---[ 34]---> BDD-cost: 216 c ---[ 33]---> Sorter-cost: 858 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 ---[ 32]---> Sorter-cost: 851 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 ---[ 31]---> Sorter-cost: 497 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 ---[ 30]---> BDD-cost: 216 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: 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 ---[ 26]---> 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 ---[ 25]---> 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 ---[ 24]---> 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 ---[ 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: 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 ---[ 21]---> 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 ---[ 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: 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 ---[ 17]---> 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 ---[ 16]---> 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 ---[ 15]---> 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 ---[ 14]---> 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 ---[ 13]---> 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 ---[ 12]---> 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 ---[ 11]---> 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 ---[ 10]---> 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 ---[ 9]---> BDD-cost: 5 c ---[ 8]---> BDD-cost: 5 c ---[ 7]---> BDD-cost: 5 c ---[ 6]---> BDD-cost: 5 c ---[ 5]---> BDD-cost: 5 c ---[ 4]---> BDD-cost: 5 c ---[ 3]---> BDD-cost: 72 c ---[ 2]---> BDD-cost: 55 c ---[ 1]---> BDD-cost: 3 c ---[ 0]---> BDD-cost: 75 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 0 | 192158 451028 | 64052 0 0 nan | 0.000 % | c | 100 | 192145 451000 | 70457 99 926 9.4 | 0.743 % | c | 250 | 192145 451000 | 77502 249 2104 8.4 | 0.743 % | c | 475 | 192089 450872 | 85253 471 4080 8.7 | 0.764 % | c | 812 | 192089 450872 | 93778 808 7766 9.6 | 0.764 % | c | 1318 | 192089 450872 | 103156 1314 12104 9.2 | 0.764 % | c | 2078 | 192087 450868 | 113472 2073 20214 9.8 | 0.766 % | c | 3217 | 192087 450868 | 124819 3212 30436 9.5 | 0.766 % | c | 4926 | 192073 450838 | 137301 4919 63407 12.9 | 0.772 % | c | 7488 | 190577 447433 | 151031 7452 154345 20.7 | 1.397 % | c ============================================================================== c [1mFound solution: 4386416678763260[0m c ---[ 0]---> c *** TERMINATED *** s SATISFIABLE v d1_bit0 -d2_bit0 -d3_bit0 d4_bit0 d5_bit0 d6_bit0 -d7_bit0 -d8_bit0 -d9_bit0 d10_bit0 -d11_bit0 d12_bit0 -d13_bit0 -d15_bit0 -d19_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 -h8_bit0 -h8_bit1 -h8_bit2 -h8_bit3 -h8_bit4 -h8_bit5 -h8_bit6 -h8_bit7 -h8_bit8 -h8_bit9 -h8_bit10 -h8_bit11 -h8_bit12 -h8_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 h11_bit0 -h11_bit1 h11_bit2 -h11_bit3 -h11_bit4 -h11_bit5 -h11_bit6 -h11_bit7 -h11_bit8 -h11_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 -h19_bit0 -h19_bit1 -h19_bit2 -h19_bit3 -h19_bit4 -h19_bit5 -h19_bit6 -h19_bit7 -h19_bit8 -h19_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 g8_bit0 -g8_bit1 g8_bit2 g8_bit3 g8_bit4 -g8_bit5 g8_bit6 g8_bit7 -g8_bit8 -g8_bit9 g8_bit10 -g8_bit11 g8_bit12 -g8_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 g11_bit0 -g11_bit1 g11_bit2 -g11_bit3 g11_bit4 g11_bit5 g11_bit6 -g11_bit7 g11_bit8 g11_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 g19_bit0 -g19_bit1 g19_bit2 g19_bit3 g19_bit4 -g19_bit5 g19_bit6 g19_bit7 g19_bit8 -g19_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 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 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 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 -f11_bit_10 -f11_bit_9 f11_bit_8 -f11_bit_7 f11_bit_6 f11_bit_5 -f11_bit_4 -f11_bit_3 -f11_bit_2 f11_bit_1 -f11_bit0 f11_bit1 f11_bit2 -f11_bit3 -f11_bit4 f11_bit5 f11_bit6 f11_bit7 f11_bit8 f11_bit9 f11_bit10 -f11_bit11 f11_bit12 -f11_bit13 -f11_bit14 -f11_bit15 -f11_bit16 -f11_bit17 -f11_bit18 -f11_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_bit
Enforcing CPU limit (will send SIGTERM then SIGKILL): 1200 seconds Enforcing CPUTime (will send SIGXCPU) limit: 1230 seconds Enforcing Stack size limit: 67108864 bytes Enforcing memory limit (will send SIGTERM then SIGKILL): 921600 Kb Enforcing VSIZE limit: 994918400 bytes Current StackSize limit: 67108864 bytes Raw data (/proc/16370/stat): 16370 (minisat+_script) R 16369 16370 31027 0 -1 0 19 0 0 0 0 0 0 0 22 0 1 0 1846483845 712704 3 4294967295 134512640 135087896 3221224496 3221224496 1073744960 0 0 5 0 0 0 0 17 0 0 0 Raw data (/proc/16370/statm): 174 3 169 147 0 27 0 [pid=16370] 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=16371 New process pid=16372 New process pid=16373 execve syscall for /bin/sed executable One traced child (pid=16372) 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=16373) exited with status: 0 One traced child (pid=16371) exited with status: 0 New process pid=16374 execve syscall for /oldhome/oroussel/solvers/minisat+_64-bit_static executable open syscall for file /dev/null open syscall for file /oldhome/oroussel/tmp/wulflinc18/normalized-mps-v2-20-10-bell4.opb One traced child (pid=16374) exited with status: 5 open syscall for file /oldhome/oroussel/solvers/ New process pid=16375 execve syscall for /oldhome/oroussel/solvers/minisat+_bignum_static executable open syscall for file /dev/null open syscall for file /oldhome/oroussel/tmp/wulflinc18/normalized-mps-v2-20-10-bell4.opb [startup+10.0044 s] Raw data (loadavg): 0.57 0.86 0.95 2/57 16375 Raw data (/proc/16370/stat): 16370 (minisat+_script) S 16369 16370 31027 0 -1 0 314 332 0 0 0 0 0 1 21 0 1 0 1846483845 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/16370/statm): 532 234 485 147 0 385 0 [pid=16370] vsize: 2128 Raw data (/proc/16375/stat): 16375 (minisat+_bignum) R 16370 16370 31027 0 -1 0 673 0 0 0 989 2 0 0 25 0 1 0 1846483851 2830336 583 4294967295 134512640 135167914 3221224448 3221221440 134843406 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/16375/statm): 691 583 162 162 0 529 0 [pid=16375] vsize: 2764 Current children cumulated CPU time (s) 9.92 Current children cumulated vsize (Kb) 4892 [startup+20.0053 s] Raw data (loadavg): 0.63 0.86 0.95 2/57 16375 Raw data (/proc/16370/stat): 16370 (minisat+_script) S 16369 16370 31027 0 -1 0 314 332 0 0 0 0 0 1 21 0 1 0 1846483845 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/16370/statm): 532 234 485 147 0 385 0 [pid=16370] vsize: 2128 Raw data (/proc/16375/stat): 16375 (minisat+_bignum) R 16370 16370 31027 0 -1 0 721 0 0 0 1988 3 0 0 25 0 1 0 1846483851 3346432 631 4294967295 134512640 135167914 3221224448 3221222144 134849061 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/16375/statm): 817 631 162 162 0 655 0 [pid=16375] vsize: 3268 Current children cumulated CPU time (s) 19.92 Current children cumulated vsize (Kb) 5396 [startup+30.0063 s] Raw data (loadavg): 0.69 0.87 0.95 2/57 16375 Raw data (/proc/16370/stat): 16370 (minisat+_script) S 16369 16370 31027 0 -1 0 314 332 0 0 0 0 0 1 21 0 1 0 1846483845 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/16370/statm): 532 234 485 147 0 385 0 [pid=16370] vsize: 2128 Raw data (/proc/16375/stat): 16375 (minisat+_bignum) R 16370 16370 31027 0 -1 0 791 0 0 0 2988 3 0 0 25 0 1 0 1846483851 3530752 701 4294967295 134512640 135167914 3221224448 3221221528 134844674 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/16375/statm): 862 701 162 162 0 700 0 [pid=16375] vsize: 3448 Current children cumulated CPU time (s) 29.92 Current children cumulated vsize (Kb) 5576 [startup+40.0142 s] Raw data (loadavg): 0.74 0.87 0.95 2/57 16375 Raw data (/proc/16370/stat): 16370 (minisat+_script) S 16369 16370 31027 0 -1 0 314 332 0 0 0 0 0 1 21 0 1 0 1846483845 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/16370/statm): 532 234 485 147 0 385 0 [pid=16370] vsize: 2128 Raw data (/proc/16375/stat): 16375 (minisat+_bignum) R 16370 16370 31027 0 -1 0 1003 0 0 0 3988 4 0 0 25 0 1 0 1846483851 3989504 830 4294967295 134512640 135167914 3221224448 3221222320 134849196 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/16375/statm): 974 830 162 162 0 812 0 [pid=16375] vsize: 3896 Current children cumulated CPU time (s) 39.93 Current children cumulated vsize (Kb) 6024 [startup+50.0151 s] Raw data (loadavg): 0.78 0.87 0.95 2/57 16375 Raw data (/proc/16370/stat): 16370 (minisat+_script) S 16369 16370 31027 0 -1 0 314 332 0 0 0 0 0 1 21 0 1 0 1846483845 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/16370/statm): 532 234 485 147 0 385 0 [pid=16370] vsize: 2128 Raw data (/proc/16375/stat): 16375 (minisat+_bignum) R 16370 16370 31027 0 -1 0 1076 0 0 0 4987 5 0 0 25 0 1 0 1846483851 4177920 903 4294967295 134512640 135167914 3221224448 3221220848 134844644 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/16375/statm): 1020 903 162 162 0 858 0 [pid=16375] vsize: 4080 Current children cumulated CPU time (s) 49.93 Current children cumulated vsize (Kb) 6208 [startup+60.016 s] Raw data (loadavg): 0.81 0.88 0.95 2/57 16375 Raw data (/proc/16370/stat): 16370 (minisat+_script) S 16369 16370 31027 0 -1 0 314 332 0 0 0 0 0 1 21 0 1 0 1846483845 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/16370/statm): 532 234 485 147 0 385 0 [pid=16370] vsize: 2128 Raw data (/proc/16375/stat): 16375 (minisat+_bignum) R 16370 16370 31027 0 -1 0 1126 0 0 0 5987 6 0 0 25 0 1 0 1846483851 4308992 953 4294967295 134512640 135167914 3221224448 3221221536 134843123 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/16375/statm): 1052 953 162 162 0 890 0 [pid=16375] vsize: 4208 Current children cumulated CPU time (s) 59.94 Current children cumulated vsize (Kb) 6336 [startup+70.024 s] Raw data (loadavg): 0.84 0.88 0.95 2/57 16375 Raw data (/proc/16370/stat): 16370 (minisat+_script) S 16369 16370 31027 0 -1 0 314 332 0 0 0 0 0 1 21 0 1 0 1846483845 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/16370/statm): 532 234 485 147 0 385 0 [pid=16370] vsize: 2128 Raw data (/proc/16375/stat): 16375 (minisat+_bignum) R 16370 16370 31027 0 -1 0 1173 0 0 0 6987 6 0 0 25 0 1 0 1846483851 5218304 1000 4294967295 134512640 135167914 3221224448 3221222336 134849187 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/16375/statm): 1274 1000 162 162 0 1112 0 [pid=16375] vsize: 5096 Current children cumulated CPU time (s) 69.94 Current children cumulated vsize (Kb) 7224 [startup+80.0249 s] Raw data (loadavg): 0.86 0.88 0.95 1/57 16375 Raw data (/proc/16370/stat): 16370 (minisat+_script) S 16369 16370 31027 0 -1 0 314 332 0 0 0 0 0 1 21 0 1 0 1846483845 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/16370/statm): 532 234 485 147 0 385 0 [pid=16370] vsize: 2128 Raw data (/proc/16375/stat): 16375 (minisat+_bignum) T 16370 16370 31027 0 -1 0 5167 0 0 0 7956 21 0 0 23 0 1 0 1846483851 22745088 4953 4294967295 134512640 135167914 3221224448 3221213212 134934490 0 0 5 16386 3222434794 0 0 17 1 0 0 Raw data (/proc/16375/statm): 5553 4953 162 162 0 5391 0 [pid=16375] vsize: 22212 Current children cumulated CPU time (s) 79.78 Current children cumulated vsize (Kb) 24340 [startup+90.0259 s] Raw data (loadavg): 0.88 0.89 0.95 2/57 16375 Raw data (/proc/16370/stat): 16370 (minisat+_script) S 16369 16370 31027 0 -1 0 314 332 0 0 0 0 0 1 21 0 1 0 1846483845 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/16370/statm): 532 234 485 147 0 385 0 [pid=16370] vsize: 2128 Raw data (/proc/16375/stat): 16375 (minisat+_bignum) R 16370 16370 31027 0 -1 0 6083 0 0 0 8945 28 0 0 25 0 1 0 1846483851 29450240 5869 4294967295 134512640 135167914 3221224448 3221223152 134562877 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/16375/statm): 7190 5869 162 162 0 7028 0 [pid=16375] vsize: 28760 Current children cumulated CPU time (s) 89.74 Current children cumulated vsize (Kb) 30888 [startup+100.027 s] Raw data (loadavg): 0.90 0.89 0.95 2/57 16375 Raw data (/proc/16370/stat): 16370 (minisat+_script) S 16369 16370 31027 0 -1 0 314 332 0 0 0 0 0 1 21 0 1 0 1846483845 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/16370/statm): 532 234 485 147 0 385 0 [pid=16370] vsize: 2128 Raw data (/proc/16375/stat): 16375 (minisat+_bignum) R 16370 16370 31027 0 -1 0 7922 0 0 0 9930 35 0 0 25 0 1 0 1846483851 34762752 7253 4294967295 134512640 135167914 3221224448 3221215900 134844632 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/16375/statm): 8487 7253 162 162 0 8325 0 [pid=16375] vsize: 33948 Current children cumulated CPU time (s) 99.66 Current children cumulated vsize (Kb) 36076 [startup+110.029 s] Raw data (loadavg): 0.92 0.89 0.95 2/57 16375 Raw data (/proc/16370/stat): 16370 (minisat+_script) S 16369 16370 31027 0 -1 0 314 332 0 0 0 0 0 1 21 0 1 0 1846483845 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/16370/statm): 532 234 485 147 0 385 0 [pid=16370] vsize: 2128 Raw data (/proc/16375/stat): 16375 (minisat+_bignum) R 16370 16370 31027 0 -1 0 7922 0 0 0 10930 35 0 0 25 0 1 0 1846483851 34762752 7253 4294967295 134512640 135167914 3221224448 3221216096 134696376 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/16375/statm): 8487 7253 162 162 0 8325 0 [pid=16375] vsize: 33948 Current children cumulated CPU time (s) 109.66 Current children cumulated vsize (Kb) 36076 [startup+120.03 s] Raw data (loadavg): 0.93 0.90 0.95 2/57 16375 Raw data (/proc/16370/stat): 16370 (minisat+_script) S 16369 16370 31027 0 -1 0 314 332 0 0 0 0 0 1 21 0 1 0 1846483845 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/16370/statm): 532 234 485 147 0 385 0 [pid=16370] vsize: 2128 Raw data (/proc/16375/stat): 16375 (minisat+_bignum) R 16370 16370 31027 0 -1 0 7922 0 0 0 11930 35 0 0 25 0 1 0 1846483851 34762752 7253 4294967295 134512640 135167914 3221224448 3221216348 134696182 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/16375/statm): 8487 7253 162 162 0 8325 0 [pid=16375] vsize: 33948 Current children cumulated CPU time (s) 119.66 Current children cumulated vsize (Kb) 36076 [startup+130.031 s] Raw data (loadavg): 0.94 0.90 0.95 2/57 16375 Raw data (/proc/16370/stat): 16370 (minisat+_script) S 16369 16370 31027 0 -1 0 314 332 0 0 0 0 0 1 21 0 1 0 1846483845 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/16370/statm): 532 234 485 147 0 385 0 [pid=16370] vsize: 2128 Raw data (/proc/16375/stat): 16375 (minisat+_bignum) R 16370 16370 31027 0 -1 0 7922 0 0 0 12930 35 0 0 25 0 1 0 1846483851 34762752 7253 4294967295 134512640 135167914 3221224448 3221216624 134843406 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/16375/statm): 8487 7253 162 162 0 8325 0 [pid=16375] vsize: 33948 Current children cumulated CPU time (s) 129.66 Current children cumulated vsize (Kb) 36076 [startup+140.031 s] Raw data (loadavg): 0.95 0.90 0.95 2/57 16375 Raw data (/proc/16370/stat): 16370 (minisat+_script) S 16369 16370 31027 0 -1 0 314 332 0 0 0 0 0 1 21 0 1 0 1846483845 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/16370/statm): 532 234 485 147 0 385 0 [pid=16370] vsize: 2128 Raw data (/proc/16375/stat): 16375 (minisat+_bignum) R 16370 16370 31027 0 -1 0 7922 0 0 0 13931 35 0 0 25 0 1 0 1846483851 34762752 7253 4294967295 134512640 135167914 3221224448 3221217040 134694517 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/16375/statm): 8487 7253 162 162 0 8325 0 [pid=16375] vsize: 33948 Current children cumulated CPU time (s) 139.67 Current children cumulated vsize (Kb) 36076 [startup+150.032 s] Raw data (loadavg): 0.95 0.91 0.95 2/57 16375 Raw data (/proc/16370/stat): 16370 (minisat+_script) S 16369 16370 31027 0 -1 0 314 332 0 0 0 0 0 1 21 0 1 0 1846483845 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/16370/statm): 532 234 485 147 0 385 0 [pid=16370] vsize: 2128 Raw data (/proc/16375/stat): 16375 (minisat+_bignum) R 16370 16370 31027 0 -1 0 7922 0 0 0 14931 35 0 0 25 0 1 0 1846483851 34762752 7253 4294967295 134512640 135167914 3221224448 3221216528 134694338 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/16375/statm): 8487 7253 162 162 0 8325 0 [pid=16375] vsize: 33948 Current children cumulated CPU time (s) 149.67 Current children cumulated vsize (Kb) 36076 [startup+160.033 s] Raw data (loadavg): 0.96 0.91 0.95 2/57 16375 Raw data (/proc/16370/stat): 16370 (minisat+_script) S 16369 16370 31027 0 -1 0 314 332 0 0 0 0 0 1 21 0 1 0 1846483845 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/16370/statm): 532 234 485 147 0 385 0 [pid=16370] vsize: 2128 Raw data (/proc/16375/stat): 16375 (minisat+_bignum) R 16370 16370 31027 0 -1 0 7922 0 0 0 15931 36 0 0 25 0 1 0 1846483851 34762752 7253 4294967295 134512640 135167914 3221224448 3221215932 134723236 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/16375/statm): 8487 7253 162 162 0 8325 0 [pid=16375] vsize: 33948 Current children cumulated CPU time (s) 159.68 Current children cumulated vsize (Kb) 36076 [startup+170.034 s] Raw data (loadavg): 0.97 0.91 0.95 2/57 16375 Raw data (/proc/16370/stat): 16370 (minisat+_script) S 16369 16370 31027 0 -1 0 314 332 0 0 0 0 0 1 21 0 1 0 1846483845 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/16370/statm): 532 234 485 147 0 385 0 [pid=16370] vsize: 2128 Raw data (/proc/16375/stat): 16375 (minisat+_bignum) R 16370 16370 31027 0 -1 0 7922 0 0 0 16931 36 0 0 25 0 1 0 1846483851 34762752 7253 4294967295 134512640 135167914 3221224448 3221216864 134843139 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/16375/statm): 8487 7253 162 162 0 8325 0 [pid=16375] vsize: 33948 Current children cumulated CPU time (s) 169.68 Current children cumulated vsize (Kb) 36076 [startup+180.035 s] Raw data (loadavg): 0.97 0.91 0.95 2/57 16375 Raw data (/proc/16370/stat): 16370 (minisat+_script) S 16369 16370 31027 0 -1 0 314 332 0 0 0 0 0 1 21 0 1 0 1846483845 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/16370/statm): 532 234 485 147 0 385 0 [pid=16370] vsize: 2128 Raw data (/proc/16375/stat): 16375 (minisat+_bignum) R 16370 16370 31027 0 -1 0 7922 0 0 0 17931 36 0 0 25 0 1 0 1846483851 34762752 7253 4294967295 134512640 135167914 3221224448 3221216528 134849068 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/16375/statm): 8487 7253 162 162 0 8325 0 [pid=16375] vsize: 33948 Current children cumulated CPU time (s) 179.68 Current children cumulated vsize (Kb) 36076 [startup+190.036 s] Raw data (loadavg): 0.98 0.92 0.95 2/57 16375 Raw data (/proc/16370/stat): 16370 (minisat+_script) S 16369 16370 31027 0 -1 0 314 332 0 0 0 0 0 1 21 0 1 0 1846483845 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/16370/statm): 532 234 485 147 0 385 0 [pid=16370] vsize: 2128 Raw data (/proc/16375/stat): 16375 (minisat+_bignum) R 16370 16370 31027 0 -1 0 7922 0 0 0 18931 36 0 0 25 0 1 0 1846483851 34762752 7253 4294967295 134512640 135167914 3221224448 3221216160 134849099 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/16375/statm): 8487 7253 162 162 0 8325 0 [pid=16375] vsize: 33948 Current children cumulated CPU time (s) 189.68 Current children cumulated vsize (Kb) 36076 [startup+200.037 s] Raw data (loadavg): 0.98 0.92 0.95 2/57 16375 Raw data (/proc/16370/stat): 16370 (minisat+_script) S 16369 16370 31027 0 -1 0 314 332 0 0 0 0 0 1 21 0 1 0 1846483845 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/16370/statm): 532 234 485 147 0 385 0 [pid=16370] vsize: 2128 Raw data (/proc/16375/stat): 16375 (minisat+_bignum) R 16370 16370 31027 0 -1 0 7922 0 0 0 19931 36 0 0 25 0 1 0 1846483851 34762752 7253 4294967295 134512640 135167914 3221224448 3221216988 134723262 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/16375/statm): 8487 7253 162 162 0 8325 0 [pid=16375] vsize: 33948 Current children cumulated CPU time (s) 199.68 Current children cumulated vsize (Kb) 36076 [startup+210.038 s] Raw data (loadavg): 0.98 0.92 0.95 2/57 16375 Raw data (/proc/16370/stat): 16370 (minisat+_script) S 16369 16370 31027 0 -1 0 314 332 0 0 0 0 0 1 21 0 1 0 1846483845 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/16370/statm): 532 234 485 147 0 385 0 [pid=16370] vsize: 2128 Raw data (/proc/16375/stat): 16375 (minisat+_bignum) R 16370 16370 31027 0 -1 0 7922 0 0 0 20932 36 0 0 25 0 1 0 1846483851 34762752 7253 4294967295 134512640 135167914 3221224448 3221216716 134694459 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/16375/statm): 8487 7253 162 162 0 8325 0 [pid=16375] vsize: 33948 Current children cumulated CPU time (s) 209.69 Current children cumulated vsize (Kb) 36076 [startup+220.039 s] Raw data (loadavg): 0.98 0.92 0.95 2/57 16375 Raw data (/proc/16370/stat): 16370 (minisat+_script) S 16369 16370 31027 0 -1 0 314 332 0 0 0 0 0 1 21 0 1 0 1846483845 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/16370/statm): 532 234 485 147 0 385 0 [pid=16370] vsize: 2128 Raw data (/proc/16375/stat): 16375 (minisat+_bignum) R 16370 16370 31027 0 -1 0 7922 0 0 0 21932 36 0 0 25 0 1 0 1846483851 34762752 7253 4294967295 134512640 135167914 3221224448 3221216624 134843406 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/16375/statm): 8487 7253 162 162 0 8325 0 [pid=16375] vsize: 33948 Current children cumulated CPU time (s) 219.69 Current children cumulated vsize (Kb) 36076 [startup+230.039 s] Raw data (loadavg): 0.99 0.92 0.95 2/57 16375 Raw data (/proc/16370/stat): 16370 (minisat+_script) S 16369 16370 31027 0 -1 0 314 332 0 0 0 0 0 1 21 0 1 0 1846483845 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/16370/statm): 532 234 485 147 0 385 0 [pid=16370] vsize: 2128 Raw data (/proc/16375/stat): 16375 (minisat+_bignum) R 16370 16370 31027 0 -1 0 7922 0 0 0 22932 36 0 0 25 0 1 0 1846483851 34762752 7253 4294967295 134512640 135167914 3221224448 3221216336 134849153 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/16375/statm): 8487 7253 162 162 0 8325 0 [pid=16375] vsize: 33948 Current children cumulated CPU time (s) 229.69 Current children cumulated vsize (Kb) 36076 [startup+240.04 s] Raw data (loadavg): 0.99 0.93 0.95 2/57 16375 Raw data (/proc/16370/stat): 16370 (minisat+_script) S 16369 16370 31027 0 -1 0 314 332 0 0 0 0 0 1 21 0 1 0 1846483845 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/16370/statm): 532 234 485 147 0 385 0 [pid=16370] vsize: 2128 Raw data (/proc/16375/stat): 16375 (minisat+_bignum) R 16370 16370 31027 0 -1 0 7922 0 0 0 23932 36 0 0 25 0 1 0 1846483851 34762752 7253 4294967295 134512640 135167914 3221224448 3221215932 134723246 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/16375/statm): 8487 7253 162 162 0 8325 0 [pid=16375] vsize: 33948 Current children cumulated CPU time (s) 239.69 Current children cumulated vsize (Kb) 36076 [startup+250.041 s] Raw data (loadavg): 0.99 0.93 0.95 2/57 16375 Raw data (/proc/16370/stat): 16370 (minisat+_script) S 16369 16370 31027 0 -1 0 314 332 0 0 0 0 0 1 21 0 1 0 1846483845 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/16370/statm): 532 234 485 147 0 385 0 [pid=16370] vsize: 2128 Raw data (/proc/16375/stat): 16375 (minisat+_bignum) R 16370 16370 31027 0 -1 0 7922 0 0 0 24932 36 0 0 25 0 1 0 1846483851 34762752 7253 4294967295 134512640 135167914 3221224448 3221217680 134844644 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/16375/statm): 8487 7253 162 162 0 8325 0 [pid=16375] vsize: 33948 Current children cumulated CPU time (s) 249.69 Current children cumulated vsize (Kb) 36076 [startup+260.042 s] Raw data (loadavg): 0.99 0.93 0.95 2/57 16375 Raw data (/proc/16370/stat): 16370 (minisat+_script) S 16369 16370 31027 0 -1 0 314 332 0 0 0 0 0 1 21 0 1 0 1846483845 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/16370/statm): 532 234 485 147 0 385 0 [pid=16370] vsize: 2128 Raw data (/proc/16375/stat): 16375 (minisat+_bignum) R 16370 16370 31027 0 -1 0 7922 0 0 0 25933 36 0 0 25 0 1 0 1846483851 34762752 7253 4294967295 134512640 135167914 3221224448 3221217056 134849110 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/16375/statm): 8487 7253 162 162 0 8325 0 [pid=16375] vsize: 33948 Current children cumulated CPU time (s) 259.7 Current children cumulated vsize (Kb) 36076 [startup+270.043 s] Raw data (loadavg): 0.99 0.93 0.95 2/57 16375 Raw data (/proc/16370/stat): 16370 (minisat+_script) S 16369 16370 31027 0 -1 0 314 332 0 0 0 0 0 1 21 0 1 0 1846483845 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/16370/statm): 532 234 485 147 0 385 0 [pid=16370] vsize: 2128 Raw data (/proc/16375/stat): 16375 (minisat+_bignum) R 16370 16370 31027 0 -1 0 7922 0 0 0 26933 36 0 0 25 0 1 0 1846483851 34762752 7253 4294967295 134512640 135167914 3221224448 3221216900 134629088 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/16375/statm): 8487 7253 162 162 0 8325 0 [pid=16375] vsize: 33948 Current children cumulated CPU time (s) 269.7 Current children cumulated vsize (Kb) 36076 [startup+280.043 s] Raw data (loadavg): 0.99 0.93 0.95 2/57 16375 Raw data (/proc/16370/stat): 16370 (minisat+_script) S 16369 16370 31027 0 -1 0 314 332 0 0 0 0 0 1 21 0 1 0 1846483845 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/16370/statm): 532 234 485 147 0 385 0 [pid=16370] vsize: 2128 Raw data (/proc/16375/stat): 16375 (minisat+_bignum) R 16370 16370 31027 0 -1 0 7922 0 0 0 27933 37 0 0 25 0 1 0 1846483851 34762752 7253 4294967295 134512640 135167914 3221224448 3221217252 134629088 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/16375/statm): 8487 7253 162 162 0 8325 0 [pid=16375] vsize: 33948 Current children cumulated CPU time (s) 279.71 Current children cumulated vsize (Kb) 36076 [startup+290.044 s] Raw data (loadavg): 0.99 0.93 0.95 2/57 16375 Raw data (/proc/16370/stat): 16370 (minisat+_script) S 16369 16370 31027 0 -1 0 314 332 0 0 0 0 0 1 21 0 1 0 1846483845 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/16370/statm): 532 234 485 147 0 385 0 [pid=16370] vsize: 2128 Raw data (/proc/16375/stat): 16375 (minisat+_bignum) R 16370 16370 31027 0 -1 0 7922 0 0 0 28933 37 0 0 25 0 1 0 1846483851 34762752 7253 4294967295 134512640 135167914 3221224448 3221217056 134849179 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/16375/statm): 8487 7253 162 162 0 8325 0 [pid=16375] vsize: 33948 Current children cumulated CPU time (s) 289.71 Current children cumulated vsize (Kb) 36076 [startup+300.044 s] Raw data (loadavg): 0.99 0.94 0.95 2/57 16375 Raw data (/proc/16370/stat): 16370 (minisat+_script) S 16369 16370 31027 0 -1 0 314 332 0 0 0 0 0 1 21 0 1 0 1846483845 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/16370/statm): 532 234 485 147 0 385 0 [pid=16370] vsize: 2128 Raw data (/proc/16375/stat): 16375 (minisat+_bignum) R 16370 16370 31027 0 -1 0 7922 0 0 0 29933 37 0 0 25 0 1 0 1846483851 34762752 7253 4294967295 134512640 135167914 3221224448 3221216864 134843130 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/16375/statm): 8487 7253 162 162 0 8325 0 [pid=16375] vsize: 33948 Current children cumulated CPU time (s) 299.71 Current children cumulated vsize (Kb) 36076 [startup+310.045 s] Raw data (loadavg): 0.99 0.94 0.95 2/57 16375 Raw data (/proc/16370/stat): 16370 (minisat+_script) S 16369 16370 31027 0 -1 0 314 332 0 0 0 0 0 1 21 0 1 0 1846483845 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/16370/statm): 532 234 485 147 0 385 0 [pid=16370] vsize: 2128 Raw data (/proc/16375/stat): 16375 (minisat+_bignum) R 16370 16370 31027 0 -1 0 7922 0 0 0 30933 37 0 0 25 0 1 0 1846483851 34762752 7253 4294967295 134512640 135167914 3221224448 3221217216 134694528 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/16375/statm): 8487 7253 162 162 0 8325 0 [pid=16375] vsize: 33948 Current children cumulated CPU time (s) 309.71 Current children cumulated vsize (Kb) 36076 [startup+320.046 s] Raw data (loadavg): 0.99 0.94 0.95 2/57 16375 Raw data (/proc/16370/stat): 16370 (minisat+_script) S 16369 16370 31027 0 -1 0 314 332 0 0 0 0 0 1 21 0 1 0 1846483845 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/16370/statm): 532 234 485 147 0 385 0 [pid=16370] vsize: 2128 Raw data (/proc/16375/stat): 16375 (minisat+_bignum) R 16370 16370 31027 0 -1 0 7922 0 0 0 31934 37 0 0 25 0 1 0 1846483851 34762752 7253 4294967295 134512640 135167914 3221224448 3221216524 134722512 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/16375/statm): 8487 7253 162 162 0 8325 0 [pid=16375] vsize: 33948 Current children cumulated CPU time (s) 319.72 Current children cumulated vsize (Kb) 36076 [startup+330.046 s] Raw data (loadavg): 0.99 0.94 0.95 2/57 16375 Raw data (/proc/16370/stat): 16370 (minisat+_script) S 16369 16370 31027 0 -1 0 314 332 0 0 0 0 0 1 21 0 1 0 1846483845 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/16370/statm): 532 234 485 147 0 385 0 [pid=16370] vsize: 2128 Raw data (/proc/16375/stat): 16375 (minisat+_bignum) R 16370 16370 31027 0 -1 0 7922 0 0 0 32934 37 0 0 25 0 1 0 1846483851 34762752 7253 4294967295 134512640 135167914 3221224448 3221217040 134843139 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/16375/statm): 8487 7253 162 162 0 8325 0 [pid=16375] vsize: 33948 Current children cumulated CPU time (s) 329.72 Current children cumulated vsize (Kb) 36076 [startup+340.047 s] Raw data (loadavg): 0.99 0.94 0.95 2/57 16375 Raw data (/proc/16370/stat): 16370 (minisat+_script) S 16369 16370 31027 0 -1 0 314 332 0 0 0 0 0 1 21 0 1 0 1846483845 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/16370/statm): 532 234 485 147 0 385 0 [pid=16370] vsize: 2128 Raw data (/proc/16375/stat): 16375 (minisat+_bignum) R 16370 16370 31027 0 -1 0 7922 0 0 0 33934 37 0 0 25 0 1 0 1846483851 34762752 7253 4294967295 134512640 135167914 3221224448 3221217412 134849060 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/16375/statm): 8487 7253 162 162 0 8325 0 [pid=16375] vsize: 33948 Current children cumulated CPU time (s) 339.72 Current children cumulated vsize (Kb) 36076 [startup+350.048 s] Raw data (loadavg): 0.99 0.94 0.95 2/57 16375 Raw data (/proc/16370/stat): 16370 (minisat+_script) S 16369 16370 31027 0 -1 0 314 332 0 0 0 0 0 1 21 0 1 0 1846483845 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/16370/statm): 532 234 485 147 0 385 0 [pid=16370] vsize: 2128 Raw data (/proc/16375/stat): 16375 (minisat+_bignum) R 16370 16370 31027 0 -1 0 7922 0 0 0 34934 37 0 0 25 0 1 0 1846483851 34762752 7253 4294967295 134512640 135167914 3221224448 3221216976 134844689 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/16375/statm): 8487 7253 162 162 0 8325 0 [pid=16375] vsize: 33948 Current children cumulated CPU time (s) 349.72 Current children cumulated vsize (Kb) 36076 [startup+360.049 s] Raw data (loadavg): 0.99 0.95 0.95 2/57 16375 Raw data (/proc/16370/stat): 16370 (minisat+_script) S 16369 16370 31027 0 -1 0 314 332 0 0 0 0 0 1 21 0 1 0 1846483845 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/16370/statm): 532 234 485 147 0 385 0 [pid=16370] vsize: 2128 Raw data (/proc/16375/stat): 16375 (minisat+_bignum) R 16370 16370 31027 0 -1 0 7922 0 0 0 35934 37 0 0 25 0 1 0 1846483851 34762752 7253 4294967295 134512640 135167914 3221224448 3221217724 134843033 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/16375/statm): 8487 7253 162 162 0 8325 0 [pid=16375] vsize: 33948 Current children cumulated CPU time (s) 359.72 Current children cumulated vsize (Kb) 36076 [startup+370.05 s] Raw data (loadavg): 0.99 0.95 0.95 2/57 16375 Raw data (/proc/16370/stat): 16370 (minisat+_script) S 16369 16370 31027 0 -1 0 314 332 0 0 0 0 0 1 21 0 1 0 1846483845 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/16370/statm): 532 234 485 147 0 385 0 [pid=16370] vsize: 2128 Raw data (/proc/16375/stat): 16375 (minisat+_bignum) R 16370 16370 31027 0 -1 0 7922 0 0 0 36935 37 0 0 25 0 1 0 1846483851 34762752 7253 4294967295 134512640 135167914 3221224448 3221216812 134723262 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/16375/statm): 8487 7253 162 162 0 8325 0 [pid=16375] vsize: 33948 Current children cumulated CPU time (s) 369.73 Current children cumulated vsize (Kb) 36076 [startup+380.05 s] Raw data (loadavg): 0.99 0.95 0.95 2/57 16375 Raw data (/proc/16370/stat): 16370 (minisat+_script) S 16369 16370 31027 0 -1 0 314 332 0 0 0 0 0 1 21 0 1 0 1846483845 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/16370/statm): 532 234 485 147 0 385 0 [pid=16370] vsize: 2128 Raw data (/proc/16375/stat): 16375 (minisat+_bignum) R 16370 16370 31027 0 -1 0 7922 0 0 0 37935 37 0 0 25 0 1 0 1846483851 34762752 7253 4294967295 134512640 135167914 3221224448 3221217152 134845911 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/16375/statm): 8487 7253 162 162 0 8325 0 [pid=16375] vsize: 33948 Current children cumulated CPU time (s) 379.73 Current children cumulated vsize (Kb) 36076 [startup+390.051 s] Raw data (loadavg): 0.99 0.95 0.95 2/57 16375 Raw data (/proc/16370/stat): 16370 (minisat+_script) S 16369 16370 31027 0 -1 0 314 332 0 0 0 0 0 1 21 0 1 0 1846483845 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/16370/statm): 532 234 485 147 0 385 0 [pid=16370] vsize: 2128 Raw data (/proc/16375/stat): 16375 (minisat+_bignum) R 16370 16370 31027 0 -1 0 7922 0 0 0 38935 37 0 0 25 0 1 0 1846483851 34762752 7253 4294967295 134512640 135167914 3221224448 3221216896 134630183 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/16375/statm): 8487 7253 162 162 0 8325 0 [pid=16375] vsize: 33948 Current children cumulated CPU time (s) 389.73 Current children cumulated vsize (Kb) 36076 [startup+400.052 s] Raw data (loadavg): 0.99 0.95 0.95 2/57 16375 Raw data (/proc/16370/stat): 16370 (minisat+_script) S 16369 16370 31027 0 -1 0 314 332 0 0 0 0 0 1 21 0 1 0 1846483845 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/16370/statm): 532 234 485 147 0 385 0 [pid=16370] vsize: 2128 Raw data (/proc/16375/stat): 16375 (minisat+_bignum) R 16370 16370 31027 0 -1 0 7922 0 0 0 39935 37 0 0 25 0 1 0 1846483851 34762752 7253 4294967295 134512640 135167914 3221224448 3221216624 134844728 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/16375/statm): 8487 7253 162 162 0 8325 0 [pid=16375] vsize: 33948 Current children cumulated CPU time (s) 399.73 Current children cumulated vsize (Kb) 36076 [startup+410.053 s] Raw data (loadavg): 0.99 0.95 0.95 2/57 16375 Raw data (/proc/16370/stat): 16370 (minisat+_script) S 16369 16370 31027 0 -1 0 314 332 0 0 0 0 0 1 21 0 1 0 1846483845 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/16370/statm): 532 234 485 147 0 385 0 [pid=16370] vsize: 2128 Raw data (/proc/16375/stat): 16375 (minisat+_bignum) R 16370 16370 31027 0 -1 0 7922 0 0 0 40935 37 0 0 25 0 1 0 1846483851 34762752 7253 4294967295 134512640 135167914 3221224448 3221217056 134693566 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/16375/statm): 8487 7253 162 162 0 8325 0 [pid=16375] vsize: 33948 Current children cumulated CPU time (s) 409.73 Current children cumulated vsize (Kb) 36076 [startup+420.054 s] Raw data (loadavg): 0.99 0.95 0.95 2/57 16375 Raw data (/proc/16370/stat): 16370 (minisat+_script) S 16369 16370 31027 0 -1 0 314 332 0 0 0 0 0 1 21 0 1 0 1846483845 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/16370/statm): 532 234 485 147 0 385 0 [pid=16370] vsize: 2128 Raw data (/proc/16375/stat): 16375 (minisat+_bignum) R 16370 16370 31027 0 -1 0 7922 0 0 0 41935 37 0 0 25 0 1 0 1846483851 34762752 7253 4294967295 134512640 135167914 3221224448 3221217040 134849068 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/16375/statm): 8487 7253 162 162 0 8325 0 [pid=16375] vsize: 33948 Current children cumulated CPU time (s) 419.73 Current children cumulated vsize (Kb) 36076 [startup+430.054 s] Raw data (loadavg): 0.99 0.95 0.95 2/57 16375 Raw data (/proc/16370/stat): 16370 (minisat+_script) S 16369 16370 31027 0 -1 0 314 332 0 0 0 0 0 1 21 0 1 0 1846483845 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/16370/statm): 532 234 485 147 0 385 0 [pid=16370] vsize: 2128 Raw data (/proc/16375/stat): 16375 (minisat+_bignum) R 16370 16370 31027 0 -1 0 7922 0 0 0 42936 37 0 0 25 0 1 0 1846483851 34762752 7253 4294967295 134512640 135167914 3221224448 3221217072 134629045 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/16375/statm): 8487 7253 162 162 0 8325 0 [pid=16375] vsize: 33948 Current children cumulated CPU time (s) 429.74 Current children cumulated vsize (Kb) 36076 [startup+440.055 s] Raw data (loadavg): 0.99 0.95 0.95 2/57 16375 Raw data (/proc/16370/stat): 16370 (minisat+_script) S 16369 16370 31027 0 -1 0 314 332 0 0 0 0 0 1 21 0 1 0 1846483845 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/16370/statm): 532 234 485 147 0 385 0 [pid=16370] vsize: 2128 Raw data (/proc/16375/stat): 16375 (minisat+_bignum) R 16370 16370 31027 0 -1 0 7922 0 0 0 43936 37 0 0 25 0 1 0 1846483851 34762752 7253 4294967295 134512640 135167914 3221224448 3221216536 134843032 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/16375/statm): 8487 7253 162 162 0 8325 0 [pid=16375] vsize: 33948 Current children cumulated CPU time (s) 439.74 Current children cumulated vsize (Kb) 36076 [startup+450.056 s] Raw data (loadavg): 0.99 0.95 0.95 2/57 16375 Raw data (/proc/16370/stat): 16370 (minisat+_script) S 16369 16370 31027 0 -1 0 314 332 0 0 0 0 0 1 21 0 1 0 1846483845 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/16370/statm): 532 234 485 147 0 385 0 [pid=16370] vsize: 2128 Raw data (/proc/16375/stat): 16375 (minisat+_bignum) R 16370 16370 31027 0 -1 0 7922 0 0 0 44936 37 0 0 25 0 1 0 1846483851 34762752 7253 4294967295 134512640 135167914 3221224448 3221217088 134845911 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/16375/statm): 8487 7253 162 162 0 8325 0 [pid=16375] vsize: 33948 Current children cumulated CPU time (s) 449.74 Current children cumulated vsize (Kb) 36076 [startup+460.057 s] Raw data (loadavg): 0.99 0.95 0.95 2/57 16375 Raw data (/proc/16370/stat): 16370 (minisat+_script) S 16369 16370 31027 0 -1 0 314 332 0 0 0 0 0 1 21 0 1 0 1846483845 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/16370/statm): 532 234 485 147 0 385 0 [pid=16370] vsize: 2128 Raw data (/proc/16375/stat): 16375 (minisat+_bignum) R 16370 16370 31027 0 -1 0 7922 0 0 0 45936 37 0 0 25 0 1 0 1846483851 34762752 7253 4294967295 134512640 135167914 3221224448 3221217420 134696788 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/16375/statm): 8487 7253 162 162 0 8325 0 [pid=16375] vsize: 33948 Current children cumulated CPU time (s) 459.74 Current children cumulated vsize (Kb) 36076 [startup+470.058 s] Raw data (loadavg): 0.99 0.96 0.95 2/57 16375 Raw data (/proc/16370/stat): 16370 (minisat+_script) S 16369 16370 31027 0 -1 0 314 332 0 0 0 0 0 1 21 0 1 0 1846483845 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/16370/statm): 532 234 485 147 0 385 0 [pid=16370] vsize: 2128 Raw data (/proc/16375/stat): 16375 (minisat+_bignum) R 16370 16370 31027 0 -1 0 7922 0 0 0 46936 37 0 0 25 0 1 0 1846483851 34762752 7253 4294967295 134512640 135167914 3221224448 3221216864 134694517 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/16375/statm): 8487 7253 162 162 0 8325 0 [pid=16375] vsize: 33948 Current children cumulated CPU time (s) 469.74 Current children cumulated vsize (Kb) 36076 [startup+480.058 s] Raw data (loadavg): 0.99 0.96 0.95 2/57 16375 Raw data (/proc/16370/stat): 16370 (minisat+_script) S 16369 16370 31027 0 -1 0 314 332 0 0 0 0 0 1 21 0 1 0 1846483845 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/16370/statm): 532 234 485 147 0 385 0 [pid=16370] vsize: 2128 Raw data (/proc/16375/stat): 16375 (minisat+_bignum) R 16370 16370 31027 0 -1 0 7922 0 0 0 47937 37 0 0 25 0 1 0 1846483851 34762752 7253 4294967295 134512640 135167914 3221224448 3221217180 134722227 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/16375/statm): 8487 7253 162 162 0 8325 0 [pid=16375] vsize: 33948 Current children cumulated CPU time (s) 479.75 Current children cumulated vsize (Kb) 36076 [startup+490.06 s] Raw data (loadavg): 0.99 0.96 0.95 2/57 16375 Raw data (/proc/16370/stat): 16370 (minisat+_script) S 16369 16370 31027 0 -1 0 314 332 0 0 0 0 0 1 21 0 1 0 1846483845 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/16370/statm): 532 234 485 147 0 385 0 [pid=16370] vsize: 2128 Raw data (/proc/16375/stat): 16375 (minisat+_bignum) R 16370 16370 31027 0 -1 0 7922 0 0 0 48937 37 0 0 25 0 1 0 1846483851 34762752 7253 4294967295 134512640 135167914 3221224448 3221216864 134843026 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/16375/statm): 8487 7253 162 162 0 8325 0 [pid=16375] vsize: 33948 Current children cumulated CPU time (s) 489.75 Current children cumulated vsize (Kb) 36076 [startup+500.061 s] Raw data (loadavg): 0.99 0.96 0.95 2/57 16375 Raw data (/proc/16370/stat): 16370 (minisat+_script) S 16369 16370 31027 0 -1 0 314 332 0 0 0 0 0 1 21 0 1 0 1846483845 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/16370/statm): 532 234 485 147 0 385 0 [pid=16370] vsize: 2128 Raw data (/proc/16375/stat): 16375 (minisat+_bignum) R 16370 16370 31027 0 -1 0 7922 0 0 0 49937 37 0 0 25 0 1 0 1846483851 34762752 7253 4294967295 134512640 135167914 3221224448 3221217356 134842996 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/16375/statm): 8487 7253 162 162 0 8325 0 [pid=16375] vsize: 33948 Current children cumulated CPU time (s) 499.75 Current children cumulated vsize (Kb) 36076 [startup+510.062 s] Raw data (loadavg): 0.99 0.96 0.95 2/57 16375 Raw data (/proc/16370/stat): 16370 (minisat+_script) S 16369 16370 31027 0 -1 0 314 332 0 0 0 0 0 1 21 0 1 0 1846483845 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/16370/statm): 532 234 485 147 0 385 0 [pid=16370] vsize: 2128 Raw data (/proc/16375/stat): 16375 (minisat+_bignum) R 16370 16370 31027 0 -1 0 7922 0 0 0 50937 37 0 0 25 0 1 0 1846483851 34762752 7253 4294967295 134512640 135167914 3221224448 3221216996 134723216 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/16375/statm): 8487 7253 162 162 0 8325 0 [pid=16375] vsize: 33948 Current children cumulated CPU time (s) 509.75 Current children cumulated vsize (Kb) 36076 [startup+520.063 s] Raw data (loadavg): 0.99 0.96 0.95 2/57 16375 Raw data (/proc/16370/stat): 16370 (minisat+_script) S 16369 16370 31027 0 -1 0 314 332 0 0 0 0 0 1 21 0 1 0 1846483845 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/16370/statm): 532 234 485 147 0 385 0 [pid=16370] vsize: 2128 Raw data (/proc/16375/stat): 16375 (minisat+_bignum) R 16370 16370 31027 0 -1 0 7922 0 0 0 51938 37 0 0 25 0 1 0 1846483851 34762752 7253 4294967295 134512640 135167914 3221224448 3221217004 134722227 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/16375/statm): 8487 7253 162 162 0 8325 0 [pid=16375] vsize: 33948 Current children cumulated CPU time (s) 519.76 Current children cumulated vsize (Kb) 36076 [startup+530.063 s] Raw data (loadavg): 0.99 0.96 0.95 2/57 16375 Raw data (/proc/16370/stat): 16370 (minisat+_script) S 16369 16370 31027 0 -1 0 314 332 0 0 0 0 0 1 21 0 1 0 1846483845 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/16370/statm): 532 234 485 147 0 385 0 [pid=16370] vsize: 2128 Raw data (/proc/16375/stat): 16375 (minisat+_bignum) R 16370 16370 31027 0 -1 0 7922 0 0 0 52937 38 0 0 25 0 1 0 1846483851 34762752 7253 4294967295 134512640 135167914 3221224448 3221217120 134845720 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/16375/statm): 8487 7253 162 162 0 8325 0 [pid=16375] vsize: 33948 Current children cumulated CPU time (s) 529.76 Current children cumulated vsize (Kb) 36076 [startup+540.064 s] Raw data (loadavg): 0.99 0.96 0.95 2/57 16375 Raw data (/proc/16370/stat): 16370 (minisat+_script) S 16369 16370 31027 0 -1 0 314 332 0 0 0 0 0 1 21 0 1 0 1846483845 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/16370/statm): 532 234 485 147 0 385 0 [pid=16370] vsize: 2128 Raw data (/proc/16375/stat): 16375 (minisat+_bignum) R 16370 16370 31027 0 -1 0 7922 0 0 0 53938 38 0 0 25 0 1 0 1846483851 34762752 7253 4294967295 134512640 135167914 3221224448 3221216912 134629476 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/16375/statm): 8487 7253 162 162 0 8325 0 [pid=16375] vsize: 33948 Current children cumulated CPU time (s) 539.77 Current children cumulated vsize (Kb) 36076 [startup+550.065 s] Raw data (loadavg): 0.99 0.96 0.95 2/57 16375 Raw data (/proc/16370/stat): 16370 (minisat+_script) S 16369 16370 31027 0 -1 0 314 332 0 0 0 0 0 1 21 0 1 0 1846483845 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/16370/statm): 532 234 485 147 0 385 0 [pid=16370] vsize: 2128 Raw data (/proc/16375/stat): 16375 (minisat+_bignum) R 16370 16370 31027 0 -1 0 7922 0 0 0 54938 38 0 0 25 0 1 0 1846483851 34762752 7253 4294967295 134512640 135167914 3221224448 3221217136 134843118 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/16375/statm): 8487 7253 162 162 0 8325 0 [pid=16375] vsize: 33948 Current children cumulated CPU time (s) 549.77 Current children cumulated vsize (Kb) 36076 [startup+560.066 s] Raw data (loadavg): 0.99 0.96 0.95 2/57 16375 Raw data (/proc/16370/stat): 16370 (minisat+_script) S 16369 16370 31027 0 -1 0 314 332 0 0 0 0 0 1 21 0 1 0 1846483845 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/16370/statm): 532 234 485 147 0 385 0 [pid=16370] vsize: 2128 Raw data (/proc/16375/stat): 16375 (minisat+_bignum) R 16370 16370 31027 0 -1 0 7922 0 0 0 55938 38 0 0 25 0 1 0 1846483851 34762752 7253 4294967295 134512640 135167914 3221224448 3221216864 134843404 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/16375/statm): 8487 7253 162 162 0 8325 0 [pid=16375] vsize: 33948 Current children cumulated CPU time (s) 559.77 Current children cumulated vsize (Kb) 36076 [startup+570.066 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 16375 Raw data (/proc/16370/stat): 16370 (minisat+_script) S 16369 16370 31027 0 -1 0 314 332 0 0 0 0 0 1 21 0 1 0 1846483845 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/16370/statm): 532 234 485 147 0 385 0 [pid=16370] vsize: 2128 Raw data (/proc/16375/stat): 16375 (minisat+_bignum) R 16370 16370 31027 0 -1 0 7922 0 0 0 56938 38 0 0 25 0 1 0 1846483851 34762752 7253 4294967295 134512640 135167914 3221224448 3221217052 134722656 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/16375/statm): 8487 7253 162 162 0 8325 0 [pid=16375] vsize: 33948 Current children cumulated CPU time (s) 569.77 Current children cumulated vsize (Kb) 36076 [startup+580.067 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 16375 Raw data (/proc/16370/stat): 16370 (minisat+_script) S 16369 16370 31027 0 -1 0 314 332 0 0 0 0 0 1 21 0 1 0 1846483845 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/16370/statm): 532 234 485 147 0 385 0 [pid=16370] vsize: 2128 Raw data (/proc/16375/stat): 16375 (minisat+_bignum) R 16370 16370 31027 0 -1 0 7922 0 0 0 57939 38 0 0 25 0 1 0 1846483851 34762752 7253 4294967295 134512640 135167914 3221224448 3221217500 134844632 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/16375/statm): 8487 7253 162 162 0 8325 0 [pid=16375] vsize: 33948 Current children cumulated CPU time (s) 579.78 Current children cumulated vsize (Kb) 36076 [startup+590.068 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 16375 Raw data (/proc/16370/stat): 16370 (minisat+_script) S 16369 16370 31027 0 -1 0 314 332 0 0 0 0 0 1 21 0 1 0 1846483845 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/16370/statm): 532 234 485 147 0 385 0 [pid=16370] vsize: 2128 Raw data (/proc/16375/stat): 16375 (minisat+_bignum) R 16370 16370 31027 0 -1 0 7922 0 0 0 58939 38 0 0 25 0 1 0 1846483851 34762752 7253 4294967295 134512640 135167914 3221224448 3221217040 134694392 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/16375/statm): 8487 7253 162 162 0 8325 0 [pid=16375] vsize: 33948 Current children cumulated CPU time (s) 589.78 Current children cumulated vsize (Kb) 36076 [startup+600.068 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 16375 Raw data (/proc/16370/stat): 16370 (minisat+_script) S 16369 16370 31027 0 -1 0 314 332 0 0 0 0 0 1 21 0 1 0 1846483845 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/16370/statm): 532 234 485 147 0 385 0 [pid=16370] vsize: 2128 Raw data (/proc/16375/stat): 16375 (minisat+_bignum) R 16370 16370 31027 0 -1 0 7922 0 0 0 59939 38 0 0 25 0 1 0 1846483851 34762752 7253 4294967295 134512640 135167914 3221224448 3221217388 134845940 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/16375/statm): 8487 7253 162 162 0 8325 0 [pid=16375] vsize: 33948 Current children cumulated CPU time (s) 599.78 Current children cumulated vsize (Kb) 36076 [startup+610.07 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 16375 Raw data (/proc/16370/stat): 16370 (minisat+_script) S 16369 16370 31027 0 -1 0 314 332 0 0 0 0 0 1 21 0 1 0 1846483845 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/16370/statm): 532 234 485 147 0 385 0 [pid=16370] vsize: 2128 Raw data (/proc/16375/stat): 16375 (minisat+_bignum) R 16370 16370 31027 0 -1 0 7922 0 0 0 60939 38 0 0 25 0 1 0 1846483851 34762752 7253 4294967295 134512640 135167914 3221224448 3221217568 134694495 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/16375/statm): 8487 7253 162 162 0 8325 0 [pid=16375] vsize: 33948 Current children cumulated CPU time (s) 609.78 Current children cumulated vsize (Kb) 36076 [startup+620.071 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 16375 Raw data (/proc/16370/stat): 16370 (minisat+_script) S 16369 16370 31027 0 -1 0 314 332 0 0 0 0 0 1 21 0 1 0 1846483845 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/16370/statm): 532 234 485 147 0 385 0 [pid=16370] vsize: 2128 Raw data (/proc/16375/stat): 16375 (minisat+_bignum) R 16370 16370 31027 0 -1 0 7922 0 0 0 61939 38 0 0 25 0 1 0 1846483851 34762752 7253 4294967295 134512640 135167914 3221224448 3221217264 134844647 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/16375/statm): 8487 7253 162 162 0 8325 0 [pid=16375] vsize: 33948 Current children cumulated CPU time (s) 619.78 Current children cumulated vsize (Kb) 36076 [startup+630.071 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 16375 Raw data (/proc/16370/stat): 16370 (minisat+_script) S 16369 16370 31027 0 -1 0 314 332 0 0 0 0 0 1 21 0 1 0 1846483845 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/16370/statm): 532 234 485 147 0 385 0 [pid=16370] vsize: 2128 Raw data (/proc/16375/stat): 16375 (minisat+_bignum) R 16370 16370 31027 0 -1 0 7922 0 0 0 62940 38 0 0 25 0 1 0 1846483851 34762752 7253 4294967295 134512640 135167914 3221224448 3221217744 134843139 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/16375/statm): 8487 7253 162 162 0 8325 0 [pid=16375] vsize: 33948 Current children cumulated CPU time (s) 629.79 Current children cumulated vsize (Kb) 36076 [startup+640.072 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 16375 Raw data (/proc/16370/stat): 16370 (minisat+_script) S 16369 16370 31027 0 -1 0 314 332 0 0 0 0 0 1 21 0 1 0 1846483845 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/16370/statm): 532 234 485 147 0 385 0 [pid=16370] vsize: 2128 Raw data (/proc/16375/stat): 16375 (minisat+_bignum) R 16370 16370 31027 0 -1 0 7922 0 0 0 63940 38 0 0 25 0 1 0 1846483851 34762752 7253 4294967295 134512640 135167914 3221224448 3221216456 134693662 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/16375/statm): 8487 7253 162 162 0 8325 0 [pid=16375] vsize: 33948 Current children cumulated CPU time (s) 639.79 Current children cumulated vsize (Kb) 36076 [startup+650.073 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 16375 Raw data (/proc/16370/stat): 16370 (minisat+_script) S 16369 16370 31027 0 -1 0 314 332 0 0 0 0 0 1 21 0 1 0 1846483845 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/16370/statm): 532 234 485 147 0 385 0 [pid=16370] vsize: 2128 Raw data (/proc/16375/stat): 16375 (minisat+_bignum) R 16370 16370 31027 0 -1 0 7922 0 0 0 64939 39 0 0 25 0 1 0 1846483851 34762752 7253 4294967295 134512640 135167914 3221224448 3221216736 134844715 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/16375/statm): 8487 7253 162 162 0 8325 0 [pid=16375] vsize: 33948 Current children cumulated CPU time (s) 649.79 Current children cumulated vsize (Kb) 36076 [startup+660.076 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 16375 Raw data (/proc/16370/stat): 16370 (minisat+_script) S 16369 16370 31027 0 -1 0 314 332 0 0 0 0 0 1 21 0 1 0 1846483845 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/16370/statm): 532 234 485 147 0 385 0 [pid=16370] vsize: 2128 Raw data (/proc/16375/stat): 16375 (minisat+_bignum) R 16370 16370 31027 0 -1 0 7922 0 0 0 65939 40 0 0 25 0 1 0 1846483851 34762752 7253 4294967295 134512640 135167914 3221224448 3221217224 134849057 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/16375/statm): 8487 7253 162 162 0 8325 0 [pid=16375] vsize: 33948 Current children cumulated CPU time (s) 659.8 Current children cumulated vsize (Kb) 36076 [startup+670.077 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 16375 Raw data (/proc/16370/stat): 16370 (minisat+_script) S 16369 16370 31027 0 -1 0 314 332 0 0 0 0 0 1 21 0 1 0 1846483845 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/16370/statm): 532 234 485 147 0 385 0 [pid=16370] vsize: 2128 Raw data (/proc/16375/stat): 16375 (minisat+_bignum) R 16370 16370 31027 0 -1 0 7922 0 0 0 66939 40 0 0 25 0 1 0 1846483851 34762752 7253 4294967295 134512640 135167914 3221224448 3221217664 134845911 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/16375/statm): 8487 7253 162 162 0 8325 0 [pid=16375] vsize: 33948 Current children cumulated CPU time (s) 669.8 Current children cumulated vsize (Kb) 36076 [startup+680.078 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 16375 Raw data (/proc/16370/stat): 16370 (minisat+_script) S 16369 16370 31027 0 -1 0 314 332 0 0 0 0 0 1 21 0 1 0 1846483845 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/16370/statm): 532 234 485 147 0 385 0 [pid=16370] vsize: 2128 Raw data (/proc/16375/stat): 16375 (minisat+_bignum) R 16370 16370 31027 0 -1 0 7922 0 0 0 67939 40 0 0 25 0 1 0 1846483851 34762752 7253 4294967295 134512640 135167914 3221224448 3221217204 134845880 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/16375/statm): 8487 7253 162 162 0 8325 0 [pid=16375] vsize: 33948 Current children cumulated CPU time (s) 679.8 Current children cumulated vsize (Kb) 36076 [startup+690.079 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 16375 Raw data (/proc/16370/stat): 16370 (minisat+_script) S 16369 16370 31027 0 -1 0 314 332 0 0 0 0 0 1 21 0 1 0 1846483845 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/16370/statm): 532 234 485 147 0 385 0 [pid=16370] vsize: 2128 Raw data (/proc/16375/stat): 16375 (minisat+_bignum) R 16370 16370 31027 0 -1 0 7922 0 0 0 68939 41 0 0 25 0 1 0 1846483851 34762752 7253 4294967295 134512640 135167914 3221224448 3221216876 134722656 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/16375/statm): 8487 7253 162 162 0 8325 0 [pid=16375] vsize: 33948 Current children cumulated CPU time (s) 689.81 Current children cumulated vsize (Kb) 36076 [startup+700.08 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 16375 Raw data (/proc/16370/stat): 16370 (minisat+_script) S 16369 16370 31027 0 -1 0 314 332 0 0 0 0 0 1 21 0 1 0 1846483845 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/16370/statm): 532 234 485 147 0 385 0 [pid=16370] vsize: 2128 Raw data (/proc/16375/stat): 16375 (minisat+_bignum) R 16370 16370 31027 0 -1 0 7922 0 0 0 69939 41 0 0 25 0 1 0 1846483851 34762752 7253 4294967295 134512640 135167914 3221224448 3221217232 134693576 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/16375/statm): 8487 7253 162 162 0 8325 0 [pid=16375] vsize: 33948 Current children cumulated CPU time (s) 699.81 Current children cumulated vsize (Kb) 36076 [startup+710.081 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 16375 Raw data (/proc/16370/stat): 16370 (minisat+_script) S 16369 16370 31027 0 -1 0 314 332 0 0 0 0 0 1 21 0 1 0 1846483845 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/16370/statm): 532 234 485 147 0 385 0 [pid=16370] vsize: 2128 Raw data (/proc/16375/stat): 16375 (minisat+_bignum) R 16370 16370 31027 0 -1 0 7922 0 0 0 70939 41 0 0 25 0 1 0 1846483851 34762752 7253 4294967295 134512640 135167914 3221224448 3221217344 134696578 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/16375/statm): 8487 7253 162 162 0 8325 0 [pid=16375] vsize: 33948 Current children cumulated CPU time (s) 709.81 Current children cumulated vsize (Kb) 36076 [startup+720.081 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 16375 Raw data (/proc/16370/stat): 16370 (minisat+_script) S 16369 16370 31027 0 -1 0 314 332 0 0 0 0 0 1 21 0 1 0 1846483845 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/16370/statm): 532 234 485 147 0 385 0 [pid=16370] vsize: 2128 Raw data (/proc/16375/stat): 16375 (minisat+_bignum) R 16370 16370 31027 0 -1 0 7922 0 0 0 71939 41 0 0 25 0 1 0 1846483851 34762752 7253 4294967295 134512640 135167914 3221224448 3221217052 134722542 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/16375/statm): 8487 7253 162 162 0 8325 0 [pid=16375] vsize: 33948 Current children cumulated CPU time (s) 719.81 Current children cumulated vsize (Kb) 36076 [startup+730.082 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 16375 Raw data (/proc/16370/stat): 16370 (minisat+_script) S 16369 16370 31027 0 -1 0 314 332 0 0 0 0 0 1 21 0 1 0 1846483845 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/16370/statm): 532 234 485 147 0 385 0 [pid=16370] vsize: 2128 Raw data (/proc/16375/stat): 16375 (minisat+_bignum) R 16370 16370 31027 0 -1 0 7922 0 0 0 72939 41 0 0 25 0 1 0 1846483851 34762752 7253 4294967295 134512640 135167914 3221224448 3221217004 134843033 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/16375/statm): 8487 7253 162 162 0 8325 0 [pid=16375] vsize: 33948 Current children cumulated CPU time (s) 729.81 Current children cumulated vsize (Kb) 36076 [startup+740.083 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 16375 Raw data (/proc/16370/stat): 16370 (minisat+_script) S 16369 16370 31027 0 -1 0 314 332 0 0 0 0 0 1 21 0 1 0 1846483845 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/16370/statm): 532 234 485 147 0 385 0 [pid=16370] vsize: 2128 Raw data (/proc/16375/stat): 16375 (minisat+_bignum) R 16370 16370 31027 0 -1 0 7922 0 0 0 73939 41 0 0 25 0 1 0 1846483851 34762752 7253 4294967295 134512640 135167914 3221224448 3221217380 134845880 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/16375/statm): 8487 7253 162 162 0 8325 0 [pid=16375] vsize: 33948 Current children cumulated CPU time (s) 739.81 Current children cumulated vsize (Kb) 36076 [startup+750.083 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 16375 Raw data (/proc/16370/stat): 16370 (minisat+_script) S 16369 16370 31027 0 -1 0 314 332 0 0 0 0 0 1 21 0 1 0 1846483845 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/16370/statm): 532 234 485 147 0 385 0 [pid=16370] vsize: 2128 Raw data (/proc/16375/stat): 16375 (minisat+_bignum) R 16370 16370 31027 0 -1 0 7922 0 0 0 74940 41 0 0 25 0 1 0 1846483851 34762752 7253 4294967295 134512640 135167914 3221224448 3221218112 134693576 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/16375/statm): 8487 7253 162 162 0 8325 0 [pid=16375] vsize: 33948 Current children cumulated CPU time (s) 749.82 Current children cumulated vsize (Kb) 36076 [startup+760.085 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 16375 Raw data (/proc/16370/stat): 16370 (minisat+_script) S 16369 16370 31027 0 -1 0 314 332 0 0 0 0 0 1 21 0 1 0 1846483845 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/16370/statm): 532 234 485 147 0 385 0 [pid=16370] vsize: 2128 Raw data (/proc/16375/stat): 16375 (minisat+_bignum) R 16370 16370 31027 0 -1 0 7922 0 0 0 75940 41 0 0 25 0 1 0 1846483851 34762752 7253 4294967295 134512640 135167914 3221224448 3221217344 134843026 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/16375/statm): 8487 7253 162 162 0 8325 0 [pid=16375] vsize: 33948 Current children cumulated CPU time (s) 759.82 Current children cumulated vsize (Kb) 36076 [startup+770.086 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 16375 Raw data (/proc/16370/stat): 16370 (minisat+_script) S 16369 16370 31027 0 -1 0 314 332 0 0 0 0 0 1 21 0 1 0 1846483845 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/16370/statm): 532 234 485 147 0 385 0 [pid=16370] vsize: 2128 Raw data (/proc/16375/stat): 16375 (minisat+_bignum) R 16370 16370 31027 0 -1 0 7922 0 0 0 76940 41 0 0 25 0 1 0 1846483851 34762752 7253 4294967295 134512640 135167914 3221224448 3221217552 134845937 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/16375/statm): 8487 7253 162 162 0 8325 0 [pid=16375] vsize: 33948 Current children cumulated CPU time (s) 769.82 Current children cumulated vsize (Kb) 36076 [startup+780.086 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 16375 Raw data (/proc/16370/stat): 16370 (minisat+_script) S 16369 16370 31027 0 -1 0 314 332 0 0 0 0 0 1 21 0 1 0 1846483845 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/16370/statm): 532 234 485 147 0 385 0 [pid=16370] vsize: 2128 Raw data (/proc/16375/stat): 16375 (minisat+_bignum) R 16370 16370 31027 0 -1 0 7922 0 0 0 77940 41 0 0 25 0 1 0 1846483851 34762752 7253 4294967295 134512640 135167914 3221224448 3221216716 134849088 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/16375/statm): 8487 7253 162 162 0 8325 0 [pid=16375] vsize: 33948 Current children cumulated CPU time (s) 779.82 Current children cumulated vsize (Kb) 36076 [startup+790.087 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 16375 Raw data (/proc/16370/stat): 16370 (minisat+_script) S 16369 16370 31027 0 -1 0 314 332 0 0 0 0 0 1 21 0 1 0 1846483845 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/16370/statm): 532 234 485 147 0 385 0 [pid=16370] vsize: 2128 Raw data (/proc/16375/stat): 16375 (minisat+_bignum) R 16370 16370 31027 0 -1 0 7922 0 0 0 78940 42 0 0 25 0 1 0 1846483851 34762752 7253 4294967295 134512640 135167914 3221224448 3221216608 134845906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/16375/statm): 8487 7253 162 162 0 8325 0 [pid=16375] vsize: 33948 Current children cumulated CPU time (s) 789.83 Current children cumulated vsize (Kb) 36076 [startup+800.088 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 16375 Raw data (/proc/16370/stat): 16370 (minisat+_script) S 16369 16370 31027 0 -1 0 314 332 0 0 0 0 0 1 21 0 1 0 1846483845 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/16370/statm): 532 234 485 147 0 385 0 [pid=16370] vsize: 2128 Raw data (/proc/16375/stat): 16375 (minisat+_bignum) R 16370 16370 31027 0 -1 0 7922 0 0 0 79940 42 0 0 25 0 1 0 1846483851 34762752 7253 4294967295 134512640 135167914 3221224448 3221216688 134694517 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/16375/statm): 8487 7253 162 162 0 8325 0 [pid=16375] vsize: 33948 Current children cumulated CPU time (s) 799.83 Current children cumulated vsize (Kb) 36076 [startup+810.089 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 16375 Raw data (/proc/16370/stat): 16370 (minisat+_script) S 16369 16370 31027 0 -1 0 314 332 0 0 0 0 0 1 21 0 1 0 1846483845 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/16370/statm): 532 234 485 147 0 385 0 [pid=16370] vsize: 2128 Raw data (/proc/16375/stat): 16375 (minisat+_bignum) R 16370 16370 31027 0 -1 0 7922 0 0 0 80940 42 0 0 25 0 1 0 1846483851 34762752 7253 4294967295 134512640 135167914 3221224448 3221217240 134694369 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/16375/statm): 8487 7253 162 162 0 8325 0 [pid=16375] vsize: 33948 Current children cumulated CPU time (s) 809.83 Current children cumulated vsize (Kb) 36076 [startup+820.09 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 16375 Raw data (/proc/16370/stat): 16370 (minisat+_script) S 16369 16370 31027 0 -1 0 314 332 0 0 0 0 0 1 21 0 1 0 1846483845 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/16370/statm): 532 234 485 147 0 385 0 [pid=16370] vsize: 2128 Raw data (/proc/16375/stat): 16375 (minisat+_bignum) R 16370 16370 31027 0 -1 0 7922 0 0 0 81941 42 0 0 25 0 1 0 1846483851 34762752 7253 4294967295 134512640 135167914 3221224448 3221216976 134844694 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/16375/statm): 8487 7253 162 162 0 8325 0 [pid=16375] vsize: 33948 Current children cumulated CPU time (s) 819.84 Current children cumulated vsize (Kb) 36076 [startup+830.091 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 16375 Raw data (/proc/16370/stat): 16370 (minisat+_script) S 16369 16370 31027 0 -1 0 314 332 0 0 0 0 0 1 21 0 1 0 1846483845 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/16370/statm): 532 234 485 147 0 385 0 [pid=16370] vsize: 2128 Raw data (/proc/16375/stat): 16375 (minisat+_bignum) R 16370 16370 31027 0 -1 0 7922 0 0 0 82940 42 0 0 25 0 1 0 1846483851 34762752 7253 4294967295 134512640 135167914 3221224448 3221217424 134629172 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/16375/statm): 8487 7253 162 162 0 8325 0 [pid=16375] vsize: 33948 Current children cumulated CPU time (s) 829.83 Current children cumulated vsize (Kb) 36076 [startup+840.092 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 16375 Raw data (/proc/16370/stat): 16370 (minisat+_script) S 16369 16370 31027 0 -1 0 314 332 0 0 0 0 0 1 21 0 1 0 1846483845 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/16370/statm): 532 234 485 147 0 385 0 [pid=16370] vsize: 2128 Raw data (/proc/16375/stat): 16375 (minisat+_bignum) R 16370 16370 31027 0 -1 0 7922 0 0 0 83941 42 0 0 25 0 1 0 1846483851 34762752 7253 4294967295 134512640 135167914 3221224448 3221217072 134630853 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/16375/statm): 8487 7253 162 162 0 8325 0 [pid=16375] vsize: 33948 Current children cumulated CPU time (s) 839.84 Current children cumulated vsize (Kb) 36076 [startup+850.092 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 16375 Raw data (/proc/16370/stat): 16370 (minisat+_script) S 16369 16370 31027 0 -1 0 314 332 0 0 0 0 0 1 21 0 1 0 1846483845 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/16370/statm): 532 234 485 147 0 385 0 [pid=16370] vsize: 2128 Raw data (/proc/16375/stat): 16375 (minisat+_bignum) R 16370 16370 31027 0 -1 0 7922 0 0 0 84941 42 0 0 25 0 1 0 1846483851 34762752 7253 4294967295 134512640 135167914 3221224448 3221217584 134843030 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/16375/statm): 8487 7253 162 162 0 8325 0 [pid=16375] vsize: 33948 Current children cumulated CPU time (s) 849.84 Current children cumulated vsize (Kb) 36076 [startup+860.094 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 16375 Raw data (/proc/16370/stat): 16370 (minisat+_script) S 16369 16370 31027 0 -1 0 314 332 0 0 0 0 0 1 21 0 1 0 1846483845 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/16370/statm): 532 234 485 147 0 385 0 [pid=16370] vsize: 2128 Raw data (/proc/16375/stat): 16375 (minisat+_bignum) R 16370 16370 31027 0 -1 0 7922 0 0 0 85941 42 0 0 25 0 1 0 1846483851 34762752 7253 4294967295 134512640 135167914 3221224448 3221217732 134849147 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/16375/statm): 8487 7253 162 162 0 8325 0 [pid=16375] vsize: 33948 Current children cumulated CPU time (s) 859.84 Current children cumulated vsize (Kb) 36076 [startup+870.095 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 16375 Raw data (/proc/16370/stat): 16370 (minisat+_script) S 16369 16370 31027 0 -1 0 314 332 0 0 0 0 0 1 21 0 1 0 1846483845 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/16370/statm): 532 234 485 147 0 385 0 [pid=16370] vsize: 2128 Raw data (/proc/16375/stat): 16375 (minisat+_bignum) R 16370 16370 31027 0 -1 0 7922 0 0 0 86942 42 0 0 25 0 1 0 1846483851 34762752 7253 4294967295 134512640 135167914 3221224448 3221217856 134696738 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/16375/statm): 8487 7253 162 162 0 8325 0 [pid=16375] vsize: 33948 Current children cumulated CPU time (s) 869.85 Current children cumulated vsize (Kb) 36076 [startup+880.096 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 16375 Raw data (/proc/16370/stat): 16370 (minisat+_script) S 16369 16370 31027 0 -1 0 314 332 0 0 0 0 0 1 21 0 1 0 1846483845 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/16370/statm): 532 234 485 147 0 385 0 [pid=16370] vsize: 2128 Raw data (/proc/16375/stat): 16375 (minisat+_bignum) R 16370 16370 31027 0 -1 0 7922 0 0 0 87942 42 0 0 25 0 1 0 1846483851 34762752 7253 4294967295 134512640 135167914 3221224448 3221217060 134849060 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/16375/statm): 8487 7253 162 162 0 8325 0 [pid=16375] vsize: 33948 Current children cumulated CPU time (s) 879.85 Current children cumulated vsize (Kb) 36076 [startup+890.097 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 16375 Raw data (/proc/16370/stat): 16370 (minisat+_script) S 16369 16370 31027 0 -1 0 314 332 0 0 0 0 0 1 21 0 1 0 1846483845 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/16370/statm): 532 234 485 147 0 385 0 [pid=16370] vsize: 2128 Raw data (/proc/16375/stat): 16375 (minisat+_bignum) R 16370 16370 31027 0 -1 0 7922 0 0 0 88942 42 0 0 25 0 1 0 1846483851 34762752 7253 4294967295 134512640 135167914 3221224448 3221217040 134849092 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/16375/statm): 8487 7253 162 162 0 8325 0 [pid=16375] vsize: 33948 Current children cumulated CPU time (s) 889.85 Current children cumulated vsize (Kb) 36076 [startup+900.098 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 16375 Raw data (/proc/16370/stat): 16370 (minisat+_script) S 16369 16370 31027 0 -1 0 314 332 0 0 0 0 0 1 21 0 1 0 1846483845 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/16370/statm): 532 234 485 147 0 385 0 [pid=16370] vsize: 2128 Raw data (/proc/16375/stat): 16375 (minisat+_bignum) R 16370 16370 31027 0 -1 0 7922 0 0 0 89942 42 0 0 25 0 1 0 1846483851 34762752 7253 4294967295 134512640 135167914 3221224448 3221217392 134849110 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/16375/statm): 8487 7253 162 162 0 8325 0 [pid=16375] vsize: 33948 Current children cumulated CPU time (s) 899.85 Current children cumulated vsize (Kb) 36076 [startup+910.1 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 16375 Raw data (/proc/16370/stat): 16370 (minisat+_script) S 16369 16370 31027 0 -1 0 314 332 0 0 0 0 0 1 21 0 1 0 1846483845 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/16370/statm): 532 234 485 147 0 385 0 [pid=16370] vsize: 2128 Raw data (/proc/16375/stat): 16375 (minisat+_bignum) R 16370 16370 31027 0 -1 0 7922 0 0 0 90942 42 0 0 25 0 1 0 1846483851 34762752 7253 4294967295 134512640 135167914 3221224448 3221217024 134522331 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/16375/statm): 8487 7253 162 162 0 8325 0 [pid=16375] vsize: 33948 Current children cumulated CPU time (s) 909.85 Current children cumulated vsize (Kb) 36076 [startup+920.101 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 16375 Raw data (/proc/16370/stat): 16370 (minisat+_script) S 16369 16370 31027 0 -1 0 314 332 0 0 0 0 0 1 21 0 1 0 1846483845 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/16370/statm): 532 234 485 147 0 385 0 [pid=16370] vsize: 2128 Raw data (/proc/16375/stat): 16375 (minisat+_bignum) R 16370 16370 31027 0 -1 0 7922 0 0 0 91943 42 0 0 25 0 1 0 1846483851 34762752 7253 4294967295 134512640 135167914 3221224448 3221217212 134630279 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/16375/statm): 8487 7253 162 162 0 8325 0 [pid=16375] vsize: 33948 Current children cumulated CPU time (s) 919.86 Current children cumulated vsize (Kb) 36076 [startup+930.102 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 16375 Raw data (/proc/16370/stat): 16370 (minisat+_script) S 16369 16370 31027 0 -1 0 314 332 0 0 0 0 0 1 21 0 1 0 1846483845 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/16370/statm): 532 234 485 147 0 385 0 [pid=16370] vsize: 2128 Raw data (/proc/16375/stat): 16375 (minisat+_bignum) R 16370 16370 31027 0 -1 0 7922 0 0 0 92943 43 0 0 25 0 1 0 1846483851 34762752 7253 4294967295 134512640 135167914 3221224448 3221217392 134849061 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/16375/statm): 8487 7253 162 162 0 8325 0 [pid=16375] vsize: 33948 Current children cumulated CPU time (s) 929.87 Current children cumulated vsize (Kb) 36076 [startup+940.103 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 16375 Raw data (/proc/16370/stat): 16370 (minisat+_script) S 16369 16370 31027 0 -1 0 314 332 0 0 0 0 0 1 21 0 1 0 1846483845 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/16370/statm): 532 234 485 147 0 385 0 [pid=16370] vsize: 2128 Raw data (/proc/16375/stat): 16375 (minisat+_bignum) R 16370 16370 31027 0 -1 0 7922 0 0 0 93943 43 0 0 25 0 1 0 1846483851 34762752 7253 4294967295 134512640 135167914 3221224448 3221216516 134849147 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/16375/statm): 8487 7253 162 162 0 8325 0 [pid=16375] vsize: 33948 Current children cumulated CPU time (s) 939.87 Current children cumulated vsize (Kb) 36076 [startup+950.104 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 16375 Raw data (/proc/16370/stat): 16370 (minisat+_script) S 16369 16370 31027 0 -1 0 314 332 0 0 0 0 0 1 21 0 1 0 1846483845 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/16370/statm): 532 234 485 147 0 385 0 [pid=16370] vsize: 2128 Raw data (/proc/16375/stat): 16375 (minisat+_bignum) R 16370 16370 31027 0 -1 0 7922 0 0 0 94943 43 0 0 25 0 1 0 1846483851 34762752 7253 4294967295 134512640 135167914 3221224448 3221217068 134522184 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/16375/statm): 8487 7253 162 162 0 8325 0 [pid=16375] vsize: 33948 Current children cumulated CPU time (s) 949.87 Current children cumulated vsize (Kb) 36076 [startup+960.105 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 16375 Raw data (/proc/16370/stat): 16370 (minisat+_script) S 16369 16370 31027 0 -1 0 314 332 0 0 0 0 0 1 21 0 1 0 1846483845 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/16370/statm): 532 234 485 147 0 385 0 [pid=16370] vsize: 2128 Raw data (/proc/16375/stat): 16375 (minisat+_bignum) R 16370 16370 31027 0 -1 0 7922 0 0 0 95943 43 0 0 25 0 1 0 1846483851 34762752 7253 4294967295 134512640 135167914 3221224448 3221217372 134845940 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/16375/statm): 8487 7253 162 162 0 8325 0 [pid=16375] vsize: 33948 Current children cumulated CPU time (s) 959.87 Current children cumulated vsize (Kb) 36076 [startup+970.106 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 16375 Raw data (/proc/16370/stat): 16370 (minisat+_script) S 16369 16370 31027 0 -1 0 314 332 0 0 0 0 0 1 21 0 1 0 1846483845 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/16370/statm): 532 234 485 147 0 385 0 [pid=16370] vsize: 2128 Raw data (/proc/16375/stat): 16375 (minisat+_bignum) R 16370 16370 31027 0 -1 0 7922 0 0 0 96944 43 0 0 25 0 1 0 1846483851 34762752 7253 4294967295 134512640 135167914 3221224448 3221217596 134693552 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/16375/statm): 8487 7253 162 162 0 8325 0 [pid=16375] vsize: 33948 Current children cumulated CPU time (s) 969.88 Current children cumulated vsize (Kb) 36076 [startup+980.107 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 16375 Raw data (/proc/16370/stat): 16370 (minisat+_script) S 16369 16370 31027 0 -1 0 314 332 0 0 0 0 0 1 21 0 1 0 1846483845 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/16370/statm): 532 234 485 147 0 385 0 [pid=16370] vsize: 2128 Raw data (/proc/16375/stat): 16375 (minisat+_bignum) R 16370 16370 31027 0 -1 0 7922 0 0 0 97944 43 0 0 25 0 1 0 1846483851 34762752 7253 4294967295 134512640 135167914 3221224448 3221217536 134722532 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/16375/statm): 8487 7253 162 162 0 8325 0 [pid=16375] vsize: 33948 Current children cumulated CPU time (s) 979.88 Current children cumulated vsize (Kb) 36076 [startup+990.107 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 16375 Raw data (/proc/16370/stat): 16370 (minisat+_script) S 16369 16370 31027 0 -1 0 314 332 0 0 0 0 0 1 21 0 1 0 1846483845 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/16370/statm): 532 234 485 147 0 385 0 [pid=16370] vsize: 2128 Raw data (/proc/16375/stat): 16375 (minisat+_bignum) R 16370 16370 31027 0 -1 0 7922 0 0 0 98944 43 0 0 25 0 1 0 1846483851 34762752 7253 4294967295 134512640 135167914 3221224448 3221217152 134844644 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/16375/statm): 8487 7253 162 162 0 8325 0 [pid=16375] vsize: 33948 Current children cumulated CPU time (s) 989.88 Current children cumulated vsize (Kb) 36076 [startup+1000.11 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 16375 Raw data (/proc/16370/stat): 16370 (minisat+_script) S 16369 16370 31027 0 -1 0 314 332 0 0 0 0 0 1 21 0 1 0 1846483845 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/16370/statm): 532 234 485 147 0 385 0 [pid=16370] vsize: 2128 Raw data (/proc/16375/stat): 16375 (minisat+_bignum) R 16370 16370 31027 0 -1 0 7922 0 0 0 99944 43 0 0 25 0 1 0 1846483851 34762752 7253 4294967295 134512640 135167914 3221224448 3221218240 134845937 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/16375/statm): 8487 7253 162 162 0 8325 0 [pid=16375] vsize: 33948 Current children cumulated CPU time (s) 999.88 Current children cumulated vsize (Kb) 36076 [startup+1010.11 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 16375 Raw data (/proc/16370/stat): 16370 (minisat+_script) S 16369 16370 31027 0 -1 0 314 332 0 0 0 0 0 1 21 0 1 0 1846483845 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/16370/statm): 532 234 485 147 0 385 0 [pid=16370] vsize: 2128 Raw data (/proc/16375/stat): 16375 (minisat+_bignum) R 16370 16370 31027 0 -1 0 7922 0 0 0 100944 43 0 0 25 0 1 0 1846483851 34762752 7253 4294967295 134512640 135167914 3221224448 3221217136 134843123 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/16375/statm): 8487 7253 162 162 0 8325 0 [pid=16375] vsize: 33948 Current children cumulated CPU time (s) 1009.88 Current children cumulated vsize (Kb) 36076 [startup+1020.11 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 16375 Raw data (/proc/16370/stat): 16370 (minisat+_script) S 16369 16370 31027 0 -1 0 314 332 0 0 0 0 0 1 21 0 1 0 1846483845 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/16370/statm): 532 234 485 147 0 385 0 [pid=16370] vsize: 2128 Raw data (/proc/16375/stat): 16375 (minisat+_bignum) R 16370 16370 31027 0 -1 0 7922 0 0 0 101945 43 0 0 25 0 1 0 1846483851 34762752 7253 4294967295 134512640 135167914 3221224448 3221217240 134693744 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/16375/statm): 8487 7253 162 162 0 8325 0 [pid=16375] vsize: 33948 Current children cumulated CPU time (s) 1019.89 Current children cumulated vsize (Kb) 36076 [startup+1030.11 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 16375 Raw data (/proc/16370/stat): 16370 (minisat+_script) S 16369 16370 31027 0 -1 0 314 332 0 0 0 0 0 1 21 0 1 0 1846483845 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/16370/statm): 532 234 485 147 0 385 0 [pid=16370] vsize: 2128 Raw data (/proc/16375/stat): 16375 (minisat+_bignum) R 16370 16370 31027 0 -1 0 7922 0 0 0 102945 43 0 0 25 0 1 0 1846483851 34762752 7253 4294967295 134512640 135167914 3221224448 3221217568 134843400 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/16375/statm): 8487 7253 162 162 0 8325 0 [pid=16375] vsize: 33948 Current children cumulated CPU time (s) 1029.89 Current children cumulated vsize (Kb) 36076 [startup+1040.11 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 16375 Raw data (/proc/16370/stat): 16370 (minisat+_script) S 16369 16370 31027 0 -1 0 314 332 0 0 0 0 0 1 21 0 1 0 1846483845 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/16370/statm): 532 234 485 147 0 385 0 [pid=16370] vsize: 2128 Raw data (/proc/16375/stat): 16375 (minisat+_bignum) R 16370 16370 31027 0 -1 0 7922 0 0 0 103945 43 0 0 25 0 1 0 1846483851 34762752 7253 4294967295 134512640 135167914 3221224448 3221217680 134844682 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/16375/statm): 8487 7253 162 162 0 8325 0 [pid=16375] vsize: 33948 Current children cumulated CPU time (s) 1039.89 Current children cumulated vsize (Kb) 36076 [startup+1050.11 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 16375 Raw data (/proc/16370/stat): 16370 (minisat+_script) S 16369 16370 31027 0 -1 0 314 332 0 0 0 0 0 1 21 0 1 0 1846483845 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/16370/statm): 532 234 485 147 0 385 0 [pid=16370] vsize: 2128 Raw data (/proc/16375/stat): 16375 (minisat+_bignum) R 16370 16370 31027 0 -1 0 7922 0 0 0 104945 43 0 0 25 0 1 0 1846483851 34762752 7253 4294967295 134512640 135167914 3221224448 3221217740 134722225 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/16375/statm): 8487 7253 162 162 0 8325 0 [pid=16375] vsize: 33948 Current children cumulated CPU time (s) 1049.89 Current children cumulated vsize (Kb) 36076 [startup+1060.11 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 16375 Raw data (/proc/16370/stat): 16370 (minisat+_script) S 16369 16370 31027 0 -1 0 314 332 0 0 0 0 0 1 21 0 1 0 1846483845 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/16370/statm): 532 234 485 147 0 385 0 [pid=16370] vsize: 2128 Raw data (/proc/16375/stat): 16375 (minisat+_bignum) R 16370 16370 31027 0 -1 0 7922 0 0 0 105945 43 0 0 25 0 1 0 1846483851 34762752 7253 4294967295 134512640 135167914 3221224448 3221217312 134845895 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/16375/statm): 8487 7253 162 162 0 8325 0 [pid=16375] vsize: 33948 Current children cumulated CPU time (s) 1059.89 Current children cumulated vsize (Kb) 36076 [startup+1070.11 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 16375 Raw data (/proc/16370/stat): 16370 (minisat+_script) S 16369 16370 31027 0 -1 0 314 332 0 0 0 0 0 1 21 0 1 0 1846483845 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/16370/statm): 532 234 485 147 0 385 0 [pid=16370] vsize: 2128 Raw data (/proc/16375/stat): 16375 (minisat+_bignum) R 16370 16370 31027 0 -1 0 7922 0 0 0 106945 43 0 0 25 0 1 0 1846483851 34762752 7253 4294967295 134512640 135167914 3221224448 3221217568 134849163 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/16375/statm): 8487 7253 162 162 0 8325 0 [pid=16375] vsize: 33948 Current children cumulated CPU time (s) 1069.89 Current children cumulated vsize (Kb) 36076 [startup+1080.11 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 16375 Raw data (/proc/16370/stat): 16370 (minisat+_script) S 16369 16370 31027 0 -1 0 314 332 0 0 0 0 0 1 21 0 1 0 1846483845 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/16370/statm): 532 234 485 147 0 385 0 [pid=16370] vsize: 2128 Raw data (/proc/16375/stat): 16375 (minisat+_bignum) R 16370 16370 31027 0 -1 0 7922 0 0 0 107946 43 0 0 25 0 1 0 1846483851 34762752 7253 4294967295 134512640 135167914 3221224448 3221217600 134629358 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/16375/statm): 8487 7253 162 162 0 8325 0 [pid=16375] vsize: 33948 Current children cumulated CPU time (s) 1079.9 Current children cumulated vsize (Kb) 36076 [startup+1090.11 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 16375 Raw data (/proc/16370/stat): 16370 (minisat+_script) S 16369 16370 31027 0 -1 0 314 332 0 0 0 0 0 1 21 0 1 0 1846483845 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/16370/statm): 532 234 485 147 0 385 0 [pid=16370] vsize: 2128 Raw data (/proc/16375/stat): 16375 (minisat+_bignum) R 16370 16370 31027 0 -1 0 7922 0 0 0 108946 43 0 0 25 0 1 0 1846483851 34762752 7253 4294967295 134512640 135167914 3221224448 3221217496 134718503 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/16375/statm): 8487 7253 162 162 0 8325 0 [pid=16375] vsize: 33948 Current children cumulated CPU time (s) 1089.9 Current children cumulated vsize (Kb) 36076 [startup+1100.12 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 16375 Raw data (/proc/16370/stat): 16370 (minisat+_script) S 16369 16370 31027 0 -1 0 314 332 0 0 0 0 0 1 21 0 1 0 1846483845 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/16370/statm): 532 234 485 147 0 385 0 [pid=16370] vsize: 2128 Raw data (/proc/16375/stat): 16375 (minisat+_bignum) R 16370 16370 31027 0 -1 0 7922 0 0 0 109946 43 0 0 25 0 1 0 1846483851 34762752 7253 4294967295 134512640 135167914 3221224448 3221217968 134844703 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/16375/statm): 8487 7253 162 162 0 8325 0 [pid=16375] vsize: 33948 Current children cumulated CPU time (s) 1099.9 Current children cumulated vsize (Kb) 36076 [startup+1110.12 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 16375 Raw data (/proc/16370/stat): 16370 (minisat+_script) S 16369 16370 31027 0 -1 0 314 332 0 0 0 0 0 1 21 0 1 0 1846483845 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/16370/statm): 532 234 485 147 0 385 0 [pid=16370] vsize: 2128 Raw data (/proc/16375/stat): 16375 (minisat+_bignum) R 16370 16370 31027 0 -1 0 7922 0 0 0 110946 43 0 0 25 0 1 0 1846483851 34762752 7253 4294967295 134512640 135167914 3221224448 3221216976 134844644 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/16375/statm): 8487 7253 162 162 0 8325 0 [pid=16375] vsize: 33948 Current children cumulated CPU time (s) 1109.9 Current children cumulated vsize (Kb) 36076 [startup+1120.12 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 16375 Raw data (/proc/16370/stat): 16370 (minisat+_script) S 16369 16370 31027 0 -1 0 314 332 0 0 0 0 0 1 21 0 1 0 1846483845 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/16370/statm): 532 234 485 147 0 385 0 [pid=16370] vsize: 2128 Raw data (/proc/16375/stat): 16375 (minisat+_bignum) R 16370 16370 31027 0 -1 0 7922 0 0 0 111947 43 0 0 25 0 1 0 1846483851 34762752 7253 4294967295 134512640 135167914 3221224448 3221217088 134844668 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/16375/statm): 8487 7253 162 162 0 8325 0 [pid=16375] vsize: 33948 Current children cumulated CPU time (s) 1119.91 Current children cumulated vsize (Kb) 36076 [startup+1130.12 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 16375 Raw data (/proc/16370/stat): 16370 (minisat+_script) S 16369 16370 31027 0 -1 0 314 332 0 0 0 0 0 1 21 0 1 0 1846483845 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/16370/statm): 532 234 485 147 0 385 0 [pid=16370] vsize: 2128 Raw data (/proc/16375/stat): 16375 (minisat+_bignum) R 16370 16370 31027 0 -1 0 7922 0 0 0 112947 44 0 0 25 0 1 0 1846483851 34762752 7253 4294967295 134512640 135167914 3221224448 3221217632 134844676 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/16375/statm): 8487 7253 162 162 0 8325 0 [pid=16375] vsize: 33948 Current children cumulated CPU time (s) 1129.92 Current children cumulated vsize (Kb) 36076 [startup+1140.12 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 16375 Raw data (/proc/16370/stat): 16370 (minisat+_script) S 16369 16370 31027 0 -1 0 314 332 0 0 0 0 0 1 21 0 1 0 1846483845 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/16370/statm): 532 234 485 147 0 385 0 [pid=16370] vsize: 2128 Raw data (/proc/16375/stat): 16375 (minisat+_bignum) R 16370 16370 31027 0 -1 0 7922 0 0 0 113947 44 0 0 25 0 1 0 1846483851 34762752 7253 4294967295 134512640 135167914 3221224448 3221216960 134843123 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/16375/statm): 8487 7253 162 162 0 8325 0 [pid=16375] vsize: 33948 Current children cumulated CPU time (s) 1139.92 Current children cumulated vsize (Kb) 36076 [startup+1150.12 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 16375 Raw data (/proc/16370/stat): 16370 (minisat+_script) S 16369 16370 31027 0 -1 0 314 332 0 0 0 0 0 1 21 0 1 0 1846483845 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/16370/statm): 532 234 485 147 0 385 0 [pid=16370] vsize: 2128 Raw data (/proc/16375/stat): 16375 (minisat+_bignum) R 16370 16370 31027 0 -1 0 7922 0 0 0 114947 44 0 0 25 0 1 0 1846483851 34762752 7253 4294967295 134512640 135167914 3221224448 3221216816 134696578 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/16375/statm): 8487 7253 162 162 0 8325 0 [pid=16375] vsize: 33948 Current children cumulated CPU time (s) 1149.92 Current children cumulated vsize (Kb) 36076 [startup+1160.12 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 16375 Raw data (/proc/16370/stat): 16370 (minisat+_script) S 16369 16370 31027 0 -1 0 314 332 0 0 0 0 0 1 21 0 1 0 1846483845 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/16370/statm): 532 234 485 147 0 385 0 [pid=16370] vsize: 2128 Raw data (/proc/16375/stat): 16375 (minisat+_bignum) R 16370 16370 31027 0 -1 0 7922 0 0 0 115947 44 0 0 25 0 1 0 1846483851 34762752 7253 4294967295 134512640 135167914 3221224448 3221216640 134696656 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/16375/statm): 8487 7253 162 162 0 8325 0 [pid=16375] vsize: 33948 Current children cumulated CPU time (s) 1159.92 Current children cumulated vsize (Kb) 36076 [startup+1170.12 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 16375 Raw data (/proc/16370/stat): 16370 (minisat+_script) S 16369 16370 31027 0 -1 0 314 332 0 0 0 0 0 1 21 0 1 0 1846483845 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/16370/statm): 532 234 485 147 0 385 0 [pid=16370] vsize: 2128 Raw data (/proc/16375/stat): 16375 (minisat+_bignum) R 16370 16370 31027 0 -1 0 7922 0 0 0 116948 44 0 0 25 0 1 0 1846483851 34762752 7253 4294967295 134512640 135167914 3221224448 3221216800 134843160 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/16375/statm): 8487 7253 162 162 0 8325 0 [pid=16375] vsize: 33948 Current children cumulated CPU time (s) 1169.93 Current children cumulated vsize (Kb) 36076 [startup+1180.12 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 16375 Raw data (/proc/16370/stat): 16370 (minisat+_script) S 16369 16370 31027 0 -1 0 314 332 0 0 0 0 0 1 21 0 1 0 1846483845 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/16370/statm): 532 234 485 147 0 385 0 [pid=16370] vsize: 2128 Raw data (/proc/16375/stat): 16375 (minisat+_bignum) R 16370 16370 31027 0 -1 0 7922 0 0 0 117948 44 0 0 25 0 1 0 1846483851 34762752 7253 4294967295 134512640 135167914 3221224448 3221217036 134722227 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/16375/statm): 8487 7253 162 162 0 8325 0 [pid=16375] vsize: 33948 Current children cumulated CPU time (s) 1179.93 Current children cumulated vsize (Kb) 36076 [startup+1190.12 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 16375 Raw data (/proc/16370/stat): 16370 (minisat+_script) S 16369 16370 31027 0 -1 0 314 332 0 0 0 0 0 1 21 0 1 0 1846483845 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/16370/statm): 532 234 485 147 0 385 0 [pid=16370] vsize: 2128 Raw data (/proc/16375/stat): 16375 (minisat+_bignum) R 16370 16370 31027 0 -1 0 7922 0 0 0 118948 44 0 0 25 0 1 0 1846483851 34762752 7253 4294967295 134512640 135167914 3221224448 3221217388 134845876 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/16375/statm): 8487 7253 162 162 0 8325 0 [pid=16375] vsize: 33948 Current children cumulated CPU time (s) 1189.93 Current children cumulated vsize (Kb) 36076 [startup+1200.12 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 16375 Raw data (/proc/16370/stat): 16370 (minisat+_script) S 16369 16370 31027 0 -1 0 314 332 0 0 0 0 0 1 21 0 1 0 1846483845 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/16370/statm): 532 234 485 147 0 385 0 [pid=16370] vsize: 2128 Raw data (/proc/16375/stat): 16375 (minisat+_bignum) R 16370 16370 31027 0 -1 0 7922 0 0 0 119948 44 0 0 25 0 1 0 1846483851 34762752 7253 4294967295 134512640 135167914 3221224448 3221216928 134845906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/16375/statm): 8487 7253 162 162 0 8325 0 [pid=16375] vsize: 33948 Current children cumulated CPU time (s) 1199.93 Current children cumulated vsize (Kb) 36076 [startup+1210.13 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 16375 Raw data (/proc/16370/stat): 16370 (minisat+_script) S 16369 16370 31027 0 -1 0 314 332 0 0 0 0 0 1 21 0 1 0 1846483845 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/16370/statm): 532 234 485 147 0 385 0 [pid=16370] vsize: 2128 Raw data (/proc/16375/stat): 16375 (minisat+_bignum) R 16370 16370 31027 0 -1 0 7922 0 0 0 120949 44 0 0 25 0 1 0 1846483851 34762752 7253 4294967295 134512640 135167914 3221224448 3221217488 134845930 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/16375/statm): 8487 7253 162 162 0 8325 0 [pid=16375] vsize: 33948 Current children cumulated CPU time (s) 1209.94 Current children cumulated vsize (Kb) 36076 Maximum CPU time exceeded: sending SIGTERM then SIGKILL [startup+1210.13 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 16375 Raw data (/proc/16370/stat): 16370 (minisat+_script) S 16369 16370 31027 0 -1 0 314 332 0 0 0 0 0 1 21 0 1 0 1846483845 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/16370/statm): 532 234 485 147 0 385 0 [pid=16370] vsize: 2128 Raw data (/proc/16375/stat): 16375 (minisat+_bignum) R 16370 16370 31027 0 -1 0 7922 0 0 0 120949 44 0 0 25 0 1 0 1846483851 34762752 7253 4294967295 134512640 135167914 3221224448 3221217440 134844731 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/16375/statm): 8487 7253 162 162 0 8325 0 [pid=16375] vsize: 33948 Current children cumulated CPU time (s) 1209.94 Current children cumulated vsize (Kb) 36076 Sending SIGTERM to -16370 Sleeping 2 seconds One traced child (pid=16370) ended because it received signal 15 (SIGTERM) One traced child (pid=16375) exited with status: 10 All traced children have exited ! Game is over. Child status: 10 Real time (s): 1210.15 CPU time (s): 1209.95 CPU user time (s): 1209.5 CPU system time (s): 0.45493 CPU usage (%): 99.9833 Max. virtual memory (cumulated for all children) (Kb): 36076
ERROR: no interpretation found !