Name | normalized-opb/mps-v2-13-7/MIPLIB/miplib2003/normalized-mps-v2-13-7-pp08a.opb |
MD5SUM | 962e64054cef66ff1ace4918a032c24a |
Bench Category | optimization, medium integers (OPTMEDINT) |
Has Objective Function | YES |
Satisfiable | YES |
(Un)Satisfiability was proved | YES |
Best value of the objective function | 1983976 |
Optimality of the best value was proved | NO |
Number of terms in the objective function | 2304 |
Biggest coefficient in the objective function | 1048576 |
Number of bits for the biggest coefficient in the objective function | 21 |
Sum of the numbers in the objective function | 178464600 |
Number of bits of the sum of numbers in the objective function | 28 |
Biggest number in a constraint | 1048576 |
Number of bits of the biggest number in a constraint | 21 |
Biggest sum of numbers in a constraint | 178464600 |
Number of bits of the biggest sum of numbers | 28 |
Best result obtained on this benchmark | SAT |
Best CPU time to get the best result obtained on this benchmark | 1189.01 |
Number of variables | 3584 |
Total number of constraints | 200 |
Number of constraints which are clauses | 0 |
Number of constraints which are cardinality constraints (but not clauses) | 64 |
Number of constraints which are nor clauses,nor cardinality constraints | 136 |
Minimum length of a constraint | 1 |
Maximum length of a constraint | 160 |
#### BEGIN LAUNCHER DATA #### LAUNCH ON wulflinc7 THE 2005-04-21 15:14:20 (client local time) PB2005-SCRIPT v4.0 MARKUPS: idlaunch=17925 boxname=wulflinc7 idbench=1379 idsolver=11 numberseed=0 MD5SUM SOLVER: MD5SUM BENCH: 962e64054cef66ff1ace4918a032c24a /oldhome/oroussel/tmp/wulflinc7/normalized-mps-v2-13-7-pp08a.opb REAL COMMAND: minisat+ -S /oldhome/oroussel/tmp/wulflinc7/normalized-mps-v2-13-7-pp08a.opb /oldhome/oroussel/tmp/wulflinc7/normalized-mps-v2-13-7-pp08a.opb IDLAUNCH: 17925 /proc/cpuinfo: processor : 0 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 2 cpu MHz : 451.050 cache size : 512 KB fdiv_bug : no hlt_bug : no f00f_bug : no coma_bug : no fpu : yes fpu_exception : yes cpuid level : 2 wp : yes flags : fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse bogomips : 890.88 processor : 1 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 2 cpu MHz : 451.050 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: 470480 kB Buffers: 26192 kB Cached: 515628 kB SwapCached: 4 kB Active: 191492 kB Inactive: 353156 kB HighTotal: 131008 kB HighFree: 252 kB LowTotal: 903652 kB LowFree: 470228 kB SwapTotal: 2097136 kB SwapFree: 2097128 kB Dirty: 28 kB Writeback: 0 kB Mapped: 6940 kB Slab: 13904 kB Committed_AS: 63584 kB PageTables: 316 kB VmallocTotal: 114680 kB VmallocUsed: 1364 kB VmallocChunk: 113256 kB JOB ENDED THE 2005-04-21 15:34:22 (client local time) WITH STATUS 0 IN 1200.27 SECONDS stats: 17925 7 1200.27 0 #### END LAUNCHER DATA #### #### BEGIN SOLVER DATA #### c Parsing PB file... c Converting 200 PB-constraints to clauses... c -- Unit propagations: (none) c -- Detecting intervals from adjacent constraints: ################################################################ c -- Clauses(.)/Splits(s): (none) c ---[ 198]---> BDD-cost: 158 c ---[ 196]---> Sorter-cost: 1160 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 195]---> BDD-cost: 21 c ---[ 194]---> BDD-cost: 21 c ---[ 193]---> BDD-cost: 21 c ---[ 192]---> BDD-cost: 21 c ---[ 191]---> BDD-cost: 23 c ---[ 190]---> BDD-cost: 18 c ---[ 189]---> BDD-cost: 18 c ---[ 188]---> BDD-cost: 18 c ---[ 187]---> BDD-cost: 18 c ---[ 186]---> BDD-cost: 18 c ---[ 184]---> Sorter-cost: 1160 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 183]---> BDD-cost: 18 c ---[ 182]---> BDD-cost: 18 c ---[ 181]---> BDD-cost: 18 c ---[ 180]---> BDD-cost: 24 c ---[ 179]---> BDD-cost: 24 c ---[ 178]---> BDD-cost: 24 c ---[ 177]---> BDD-cost: 21 c ---[ 176]---> BDD-cost: 21 c ---[ 175]---> BDD-cost: 21 c ---[ 174]---> BDD-cost: 21 c ---[ 172]---> Sorter-cost: 1160 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 171]---> BDD-cost: 21 c ---[ 170]---> BDD-cost: 19 c ---[ 169]---> BDD-cost: 19 c ---[ 168]---> BDD-cost: 19 c ---[ 167]---> BDD-cost: 19 c ---[ 166]---> BDD-cost: 19 c ---[ 165]---> BDD-cost: 19 c ---[ 164]---> BDD-cost: 19 c ---[ 163]---> BDD-cost: 19 c ---[ 162]---> BDD-cost: 19 c ---[ 160]---> Sorter-cost: 1160 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 159]---> BDD-cost: 19 c ---[ 158]---> BDD-cost: 19 c ---[ 157]---> BDD-cost: 19 c ---[ 156]---> BDD-cost: 19 c ---[ 155]---> BDD-cost: 19 c ---[ 154]---> BDD-cost: 19 c ---[ 153]---> BDD-cost: 19 c ---[ 151]---> Sorter-cost: 1160 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 149]---> Sorter-cost: 1160 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 147]---> Sorter-cost: 418 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 145]---> Sorter-cost: 427 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 143]---> Sorter-cost: 1179 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 141]---> Sorter-cost: 1179 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 139]---> Sorter-cost: 1179 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 137]---> Sorter-cost: 1179 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 135]---> Sorter-cost: 1179 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 133]---> Sorter-cost: 1179 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 131]---> Sorter-cost: 1179 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 129]---> Sorter-cost: 427 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 127]---> BDD-cost: 158 c ---[ 125]---> Sorter-cost: 1179 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 123]---> Sorter-cost: 1179 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 121]---> Sorter-cost: 1179 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 119]---> Sorter-cost: 1179 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 117]---> Sorter-cost: 1179 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 115]---> Sorter-cost: 1179 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 113]---> Sorter-cost: 1179 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 111]---> Sorter-cost: 427 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 109]---> Sorter-cost: 418 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 107]---> Sorter-cost: 1160 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 105]---> Sorter-cost: 1160 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 103]---> Sorter-cost: 1160 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 101]---> Sorter-cost: 1160 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 99]---> Sorter-cost: 1160 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 97]---> Sorter-cost: 1160 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 95]---> Sorter-cost: 1179 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 93]---> Sorter-cost: 418 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 91]---> Sorter-cost: 427 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 89]---> Sorter-cost: 1179 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 87]---> Sorter-cost: 1179 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 85]---> Sorter-cost: 1179 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 83]---> Sorter-cost: 1179 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 81]---> Sorter-cost: 1179 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 79]---> Sorter-cost: 1179 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 77]---> Sorter-cost: 427 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 75]---> BDD-cost: 154 c ---[ 73]---> Sorter-cost: 1179 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 71]---> Sorter-cost: 1160 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 69]---> Sorter-cost: 1160 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 67]---> Sorter-cost: 1160 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 65]---> Sorter-cost: 1160 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 63]---> Sorter-cost: 1160 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 61]---> Sorter-cost: 1160 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 59]---> Sorter-cost: 418 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 57]---> Sorter-cost: 409 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 55]---> Sorter-cost: 1141 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 53]---> Sorter-cost: 1141 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 51]---> Sorter-cost: 1179 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 49]---> Sorter-cost: 1141 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 47]---> Sorter-cost: 1141 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 45]---> Sorter-cost: 1141 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 43]---> Sorter-cost: 1141 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 41]---> Sorter-cost: 409 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 40]---> Sorter-cost: 1961 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 39]---> Sorter-cost: 1961 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 38]---> Sorter-cost: 1961 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 37]---> Sorter-cost: 1961 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 36]---> Sorter-cost: 1961 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 34]---> Sorter-cost: 1179 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 33]---> Sorter-cost: 1961 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 32]---> Sorter-cost: 1961 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 31]---> Sorter-cost: 1961 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 30]---> BDD-cost: 24 c ---[ 29]---> BDD-cost: 24 c ---[ 28]---> BDD-cost: 24 c ---[ 27]---> BDD-cost: 21 c ---[ 26]---> BDD-cost: 21 c ---[ 25]---> BDD-cost: 21 c ---[ 24]---> BDD-cost: 21 c ---[ 22]---> Sorter-cost: 427 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 21]---> BDD-cost: 23 c ---[ 20]---> BDD-cost: 19 c ---[ 19]---> BDD-cost: 19 c ---[ 18]---> BDD-cost: 19 c ---[ 17]---> BDD-cost: 19 c ---[ 16]---> BDD-cost: 19 c ---[ 15]---> BDD-cost: 19 c ---[ 14]---> BDD-cost: 19 c ---[ 13]---> BDD-cost: 19 c ---[ 12]---> BDD-cost: 24 c ---[ 10]---> Sorter-cost: 418 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 9]---> BDD-cost: 24 c ---[ 8]---> BDD-cost: 24 c ---[ 7]---> BDD-cost: 21 c ---[ 6]---> BDD-cost: 21 c ---[ 5]---> BDD-cost: 21 c ---[ 4]---> BDD-cost: 21 c ---[ 3]---> BDD-cost: 23 c ---[ 2]---> BDD-cost: 24 c ---[ 1]---> BDD-cost: 24 c ---[ 0]---> BDD-cost: 24 c =================================[SATELITE+]================================== c | | ORIGINAL | LEARNT | | c | Conflicts | Clauses Literals | Limit Clauses Literals Lit/Cl | Progress | c ============================================================================== c | 0 | 203261 478788 | 60978 0 0 nan | 0.000 % | c -- subsuming c -- var.elim.: 1000/66517 c -- var.elim.: 2000/66517 c -- var.elim.: 3000/66517 c -- var.elim.: 4000/66517 c -- var.elim.: 5000/66517 c -- var.elim.: 6000/66517 c -- var.elim.: 7000/66517 c -- var.elim.: 8000/66517 c -- var.elim.: 9000/66517 c -- var.elim.: 10000/66517 c -- var.elim.: 11000/66517 c -- var.elim.: 12000/66517 c -- var.elim.: 13000/66517 c -- var.elim.: 14000/66517 c -- var.elim.: 15000/66517 c -- var.elim.: 16000/66517 c -- var.elim.: 17000/66517 c -- var.elim.: 18000/66517 c -- var.elim.: 19000/66517 c -- var.elim.: 20000/66517 c -- var.elim.: 21000/66517 c -- var.elim.: 22000/66517 c -- var.elim.: 23000/66517 c -- var.elim.: 24000/66517 c -- var.elim.: 25000/66517 c -- var.elim.: 26000/66517 c -- var.elim.: 27000/66517 c -- var.elim.: 28000/66517 c -- var.elim.: 29000/66517 c -- var.elim.: 30000/66517 c -- var.elim.: 31000/66517 c -- var.elim.: 32000/66517 c -- var.elim.: 33000/66517 c -- var.elim.: 34000/66517 c -- var.elim.: 35000/66517 c -- var.elim.: 36000/66517 c -- var.elim.: 37000/66517 c -- var.elim.: 38000/66517 c -- var.elim.: 39000/66517 c -- var.elim.: 40000/66517 c -- var.elim.: 41000/66517 c -- var.elim.: 42000/66517 c -- var.elim.: 43000/66517 c -- var.elim.: 44000/66517 c -- var.elim.: 45000/66517 c -- var.elim.: 46000/66517 c -- var.elim.: 47000/66517 c -- var.elim.: 48000/66517 c -- var.elim.: 49000/66517 c -- var.elim.: 50000/66517 c -- var.elim.: 51000/66517 c -- var.elim.: 52000/66517 c -- var.elim.: 53000/66517 c -- var.elim.: 54000/66517 c -- var.elim.: 55000/66517 c -- var.elim.: 56000/66517 c -- var.elim.: 57000/66517 c -- var.elim.: 58000/66517 c -- var.elim.: 59000/66517 c -- var.elim.: 60000/66517 c -- var.elim.: 61000/66517 c -- var.elim.: 62000/66517 c -- var.elim.: 63000/66517 c -- var.elim.: 64000/66517 c -- var.elim.: 65000/66517 c -- var.elim.: 66000/66517 c -- var.elim.: 66517/66517 c -- var.elim.: 1000/36898 c -- var.elim.: 2000/36898 c -- var.elim.: 3000/36898 c -- var.elim.: 4000/36898 c -- var.elim.: 5000/36898 c -- var.elim.: 6000/36898 c -- var.elim.: 7000/36898 c -- var.elim.: 8000/36898 c -- var.elim.: 9000/36898 c -- var.elim.: 10000/36898 c -- var.elim.: 11000/36898 c -- var.elim.: 12000/36898 c -- var.elim.: 13000/36898 c -- var.elim.: 14000/36898 c -- var.elim.: 15000/36898 c -- var.elim.: 16000/36898 c -- var.elim.: 17000/36898 c -- var.elim.: 18000/36898 c -- var.elim.: 19000/36898 c -- var.elim.: 20000/36898 c -- var.elim.: 21000/36898 c -- var.elim.: 22000/36898 c -- var.elim.: 23000/36898 c -- var.elim.: 24000/36898 c -- var.elim.: 25000/36898 c -- var.elim.: 26000/36898 c -- var.elim.: 27000/36898 c -- var.elim.: 28000/36898 c -- var.elim.: 29000/36898 c -- var.elim.: 30000/36898 c -- var.elim.: 31000/36898 c -- var.elim.: 32000/36898 c -- var.eli#### END SOLVER DATA #### #### BEGIN WATCHER DATA #### Enforcing CPU limit (will send SIGTERM then SIGKILL): 1200 seconds Enforcing CPUTime (will send SIGXCPU) limit: 1230 seconds Enforcing VSIZE limit: 943718400 bytes Raw data (loadavg): 0.69 0.85 0.88 2/54 10316 Raw data (stat): 10316 (runsolver) R 10315 22932 22931 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 487860135 1052672 99 4294967295 134512640 135381576 3221224448 3221219692 135158418 0 2147483391 7 90112 0 0 0 17 1 0 0 Raw data (statm): 257 99 215 215 0 42 0 vsize: 1028 [startup+10.0199 s] Raw data (loadavg): 0.74 0.86 0.88 2/54 10316 Raw data (stat): 10316 (minisat+) R 10315 22932 22931 0 -1 0 11088 0 0 0 968 32 0 0 25 0 1 0 487860135 51642368 10411 4294967295 134512640 134672761 3221224544 3221223056 134637231 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 12608 10411 603 41 0 12567 0 vsize: 50432 [startup+20.0402 s] Raw data (loadavg): 0.78 0.86 0.88 2/54 10316 Raw data (stat): 10316 (minisat+) R 10315 22932 22931 0 -1 0 11556 0 0 0 1969 33 0 0 25 0 1 0 487860135 51789824 10446 4294967295 134512640 134672761 3221224544 3221223744 134610707 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 12644 10446 603 41 0 12603 0 vsize: 50576 [startup+30.0403 s] Raw data (loadavg): 0.81 0.87 0.88 2/54 10316 Raw data (stat): 10316 (minisat+) R 10315 22932 22931 0 -1 0 11567 0 0 0 2969 34 0 0 25 0 1 0 487860135 51986432 10457 4294967295 134512640 134672761 3221224544 3221223688 134616350 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 12692 10457 603 41 0 12651 0 vsize: 50768 [startup+40.0407 s] Raw data (loadavg): 0.84 0.87 0.88 2/54 10316 Raw data (stat): 10316 (minisat+) R 10315 22932 22931 0 -1 0 11575 0 0 0 3968 34 0 0 25 0 1 0 487860135 51986432 10465 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 12692 10465 603 41 0 12651 0 vsize: 50768 [startup+50.042 s] Raw data (loadavg): 0.86 0.87 0.88 2/54 10316 Raw data (stat): 10316 (minisat+) R 10315 22932 22931 0 -1 0 11582 0 0 0 4969 34 0 0 25 0 1 0 487860135 51986432 10472 4294967295 134512640 134672761 3221224544 3221223668 134566037 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 12692 10472 603 41 0 12651 0 vsize: 50768 [startup+60.0422 s] Raw data (loadavg): 0.88 0.88 0.88 2/54 10316 Raw data (stat): 10316 (minisat+) R 10315 22932 22931 0 -1 0 11586 0 0 0 5968 34 0 0 25 0 1 0 487860135 51986432 10476 4294967295 134512640 134672761 3221224544 3221223688 134616111 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 12692 10476 603 41 0 12651 0 vsize: 50768 [startup+70.0433 s] Raw data (loadavg): 0.90 0.88 0.88 2/54 10316 Raw data (stat): 10316 (minisat+) R 10315 22932 22931 0 -1 0 11592 0 0 0 6968 35 0 0 25 0 1 0 487860135 51986432 10482 4294967295 134512640 134672761 3221224544 3221223712 134553613 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 12692 10482 603 41 0 12651 0 vsize: 50768 [startup+80.0439 s] Raw data (loadavg): 0.92 0.88 0.88 2/54 10316 Raw data (stat): 10316 (minisat+) R 10315 22932 22931 0 -1 0 11629 0 0 0 7968 35 0 0 25 0 1 0 487860135 52248576 10519 4294967295 134512640 134672761 3221224544 3221223728 134615937 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 12756 10519 603 41 0 12715 0 vsize: 51024 [startup+90.0431 s] Raw data (loadavg): 0.93 0.89 0.89 2/54 10316 Raw data (stat): 10316 (minisat+) R 10315 22932 22931 0 -1 0 11634 0 0 0 8968 35 0 0 25 0 1 0 487860135 52248576 10524 4294967295 134512640 134672761 3221224544 3221223668 134566075 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 12756 10524 603 41 0 12715 0 vsize: 51024 [startup+100.044 s] Raw data (loadavg): 0.94 0.89 0.89 2/54 10316 Raw data (stat): 10316 (minisat+) R 10315 22932 22931 0 -1 0 11637 0 0 0 9968 36 0 0 25 0 1 0 487860135 52248576 10527 4294967295 134512640 134672761 3221224544 3221223728 134615549 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 12756 10527 603 41 0 12715 0 vsize: 51024 [startup+110.045 s] Raw data (loadavg): 0.95 0.89 0.89 2/54 10316 Raw data (stat): 10316 (minisat+) R 10315 22932 22931 0 -1 0 11643 0 0 0 10967 36 0 0 25 0 1 0 487860135 52248576 10533 4294967295 134512640 134672761 3221224544 3221223728 134615526 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 12756 10533 603 41 0 12715 0 vsize: 51024 [startup+120.045 s] Raw data (loadavg): 0.96 0.90 0.89 2/54 10316 Raw data (stat): 10316 (minisat+) R 10315 22932 22931 0 -1 0 11652 0 0 0 11967 36 0 0 25 0 1 0 487860135 52383744 10542 4294967295 134512640 134672761 3221224544 3221223728 134615585 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 12789 10542 603 41 0 12748 0 vsize: 51156 [startup+130.045 s] Raw data (loadavg): 0.96 0.90 0.89 2/54 10316 Raw data (stat): 10316 (minisat+) R 10315 22932 22931 0 -1 0 11687 0 0 0 12967 37 0 0 25 0 1 0 487860135 52518912 10577 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 12822 10577 603 41 0 12781 0 vsize: 51288 [startup+140.046 s] Raw data (loadavg): 0.97 0.90 0.89 2/54 10316 Raw data (stat): 10316 (minisat+) R 10315 22932 22931 0 -1 0 11731 0 0 0 13966 38 0 0 25 0 1 0 487860135 52649984 10621 4294967295 134512640 134672761 3221224544 3221223728 134615791 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 12854 10621 603 41 0 12813 0 vsize: 51416 [startup+150.046 s] Raw data (loadavg): 0.97 0.90 0.89 2/54 10316 Raw data (stat): 10316 (minisat+) R 10315 22932 22931 0 -1 0 11827 0 0 0 14966 38 0 0 25 0 1 0 487860135 53338112 10717 4294967295 134512640 134672761 3221224544 3221223744 134610707 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 13022 10717 603 41 0 12981 0 vsize: 52088 [startup+160.046 s] Raw data (loadavg): 0.98 0.91 0.89 2/54 10316 Raw data (stat): 10316 (minisat+) R 10315 22932 22931 0 -1 0 11908 0 0 0 15966 38 0 0 25 0 1 0 487860135 53608448 10798 4294967295 134512640 134672761 3221224544 3221223728 134615652 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 13088 10798 603 41 0 13047 0 vsize: 52352 [startup+170.048 s] Raw data (loadavg): 0.98 0.91 0.89 2/54 10316 Raw data (stat): 10316 (minisat+) R 10315 22932 22931 0 -1 0 11995 0 0 0 16966 39 0 0 25 0 1 0 487860135 53878784 10885 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 13154 10885 603 41 0 13113 0 vsize: 52616 [startup+180.048 s] Raw data (loadavg): 0.98 0.91 0.89 2/54 10316 Raw data (stat): 10316 (minisat+) R 10315 22932 22931 0 -1 0 12087 0 0 0 17965 40 0 0 25 0 1 0 487860135 54280192 10977 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 13252 10977 603 41 0 13211 0 vsize: 53008 [startup+190.048 s] Raw data (loadavg): 0.98 0.91 0.89 2/54 10316 Raw data (stat): 10316 (minisat+) R 10315 22932 22931 0 -1 0 12171 0 0 0 18965 40 0 0 25 0 1 0 487860135 54685696 11061 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 13351 11061 603 41 0 13310 0 vsize: 53404 [startup+200.049 s] Raw data (loadavg): 0.99 0.92 0.90 2/54 10316 Raw data (stat): 10316 (minisat+) R 10315 22932 22931 0 -1 0 12305 0 0 0 19964 41 0 0 25 0 1 0 487860135 55218176 11195 4294967295 134512640 134672761 3221224544 3221223744 134610646 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 13481 11195 603 41 0 13440 0 vsize: 53924 [startup+210.049 s] Raw data (loadavg): 0.99 0.92 0.90 2/54 10316 Raw data (stat): 10316 (minisat+) R 10315 22932 22931 0 -1 0 12414 0 0 0 20964 41 0 0 25 0 1 0 487860135 55619584 11304 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 13579 11304 603 41 0 13538 0 vsize: 54316 [startup+220.05 s] Raw data (loadavg): 0.99 0.92 0.90 2/54 10316 Raw data (stat): 10316 (minisat+) R 10315 22932 22931 0 -1 0 12490 0 0 0 21964 42 0 0 25 0 1 0 487860135 55885824 11380 4294967295 134512640 134672761 3221224544 3221223668 134566037 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 13644 11380 603 41 0 13603 0 vsize: 54576 [startup+230.05 s] Raw data (loadavg): 0.99 0.92 0.90 2/54 10316 Raw data (stat): 10316 (minisat+) R 10315 22932 22931 0 -1 0 12629 0 0 0 22963 42 0 0 25 0 1 0 487860135 56414208 11519 4294967295 134512640 134672761 3221224544 3221223744 134610646 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 13773 11519 603 41 0 13732 0 vsize: 55092 [startup+240.05 s] Raw data (loadavg): 0.99 0.92 0.90 2/54 10316 Raw data (stat): 10316 (minisat+) R 10315 22932 22931 0 -1 0 12720 0 0 0 23963 42 0 0 25 0 1 0 487860135 56815616 11610 4294967295 134512640 134672761 3221224544 3221223728 134615761 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 13871 11610 603 41 0 13830 0 vsize: 55484 [startup+250.051 s] Raw data (loadavg): 0.99 0.93 0.90 2/54 10316 Raw data (stat): 10316 (minisat+) R 10315 22932 22931 0 -1 0 12849 0 0 0 24963 43 0 0 25 0 1 0 487860135 57339904 11739 4294967295 134512640 134672761 3221224544 3221223716 134565154 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 13999 11739 603 41 0 13958 0 vsize: 55996 [startup+260.051 s] Raw data (loadavg): 0.99 0.93 0.90 2/54 10316 Raw data (stat): 10316 (minisat+) R 10315 22932 22931 0 -1 0 12966 0 0 0 25962 44 0 0 25 0 1 0 487860135 57741312 11856 4294967295 134512640 134672761 3221224544 3221223728 134615608 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 14097 11856 603 41 0 14056 0 vsize: 56388 [startup+270.051 s] Raw data (loadavg): 0.99 0.93 0.90 2/54 10316 Raw data (stat): 10316 (minisat+) R 10315 22932 22931 0 -1 0 13044 0 0 0 26962 44 0 0 25 0 1 0 487860135 58007552 11934 4294967295 134512640 134672761 3221224544 3221223728 134616023 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 14162 11934 603 41 0 14121 0 vsize: 56648 [startup+280.051 s] Raw data (loadavg): 0.99 0.93 0.90 2/54 10316 Raw data (stat): 10316 (minisat+) R 10315 22932 22931 0 -1 0 13173 0 0 0 27961 45 0 0 25 0 1 0 487860135 58540032 12063 4294967295 134512640 134672761 3221224544 3221223728 134615549 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 14292 12063 603 41 0 14251 0 vsize: 57168 [startup+290.051 s] Raw data (loadavg): 0.99 0.93 0.90 2/54 10316 Raw data (stat): 10316 (minisat+) R 10315 22932 22931 0 -1 0 13306 0 0 0 28960 46 0 0 25 0 1 0 487860135 59064320 12196 4294967295 134512640 134672761 3221224544 3221223728 134615940 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 14420 12196 603 41 0 14379 0 vsize: 57680 [startup+300.051 s] Raw data (loadavg): 0.99 0.94 0.91 2/54 10316 Raw data (stat): 10316 (minisat+) R 10315 22932 22931 0 -1 0 13552 0 0 0 29959 47 0 0 25 0 1 0 487860135 60125184 12442 4294967295 134512640 134672761 3221224544 3221223728 134615549 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 14679 12442 603 41 0 14638 0 vsize: 58716 [startup+310.052 s] Raw data (loadavg): 0.99 0.94 0.91 2/54 10316 Raw data (stat): 10316 (minisat+) R 10315 22932 22931 0 -1 0 13644 0 0 0 30959 47 0 0 25 0 1 0 487860135 60919808 12534 4294967295 134512640 134672761 3221224544 3221223744 134610526 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 14873 12534 603 41 0 14832 0 vsize: 59492 [startup+320.052 s] Raw data (loadavg): 0.99 0.94 0.91 2/54 10316 Raw data (stat): 10316 (minisat+) R 10315 22932 22931 0 -1 0 13746 0 0 0 31958 48 0 0 25 0 1 0 487860135 61448192 12636 4294967295 134512640 134672761 3221224544 3221223696 134614481 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 15002 12636 603 41 0 14961 0 vsize: 60008 [startup+330.052 s] Raw data (loadavg): 0.99 0.94 0.91 2/54 10316 Raw data (stat): 10316 (minisat+) R 10315 22932 22931 0 -1 0 13952 0 0 0 32957 49 0 0 25 0 1 0 487860135 62246912 12842 4294967295 134512640 134672761 3221224544 3221223668 134566062 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 15197 12842 603 41 0 15156 0 vsize: 60788 [startup+340.053 s] Raw data (loadavg): 0.99 0.94 0.91 2/54 10316 Raw data (stat): 10316 (minisat+) R 10315 22932 22931 0 -1 0 14136 0 0 0 33956 50 0 0 25 0 1 0 487860135 62914560 13026 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 15360 13026 603 41 0 15319 0 vsize: 61440 [startup+350.053 s] Raw data (loadavg): 0.99 0.94 0.91 2/54 10316 Raw data (stat): 10316 (minisat+) R 10315 22932 22931 0 -1 0 14296 0 0 0 34956 51 0 0 25 0 1 0 487860135 63569920 13186 4294967295 134512640 134672761 3221224544 3221223728 134615985 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 15520 13186 603 41 0 15479 0 vsize: 62080 [startup+360.053 s] Raw data (loadavg): 0.99 0.94 0.91 2/54 10316 Raw data (stat): 10316 (minisat+) R 10315 22932 22931 0 -1 0 14721 0 0 0 35954 52 0 0 25 0 1 0 487860135 65294336 13611 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 15941 13611 603 41 0 15900 0 vsize: 63764 [startup+370.053 s] Raw data (loadavg): 0.99 0.95 0.91 2/54 10316 Raw data (stat): 10316 (minisat+) R 10315 22932 22931 0 -1 0 15312 0 0 0 36953 54 0 0 25 0 1 0 487860135 67678208 14202 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 16523 14202 603 41 0 16482 0 vsize: 66092 [startup+380.054 s] Raw data (loadavg): 0.99 0.95 0.91 2/54 10316 Raw data (stat): 10316 (minisat+) R 10315 22932 22931 0 -1 0 15441 0 0 0 37952 54 0 0 25 0 1 0 487860135 68218880 14331 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 16655 14331 603 41 0 16614 0 vsize: 66620 [startup+390.054 s] Raw data (loadavg): 0.99 0.95 0.91 2/54 10316 Raw data (stat): 10316 (minisat+) R 10315 22932 22931 0 -1 0 15540 0 0 0 38952 55 0 0 25 0 1 0 487860135 68620288 14430 4294967295 134512640 134672761 3221224544 3221223728 134615791 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 16753 14430 603 41 0 16712 0 vsize: 67012 [startup+400.055 s] Raw data (loadavg): 0.99 0.95 0.91 2/54 10316 Raw data (stat): 10316 (minisat+) R 10315 22932 22931 0 -1 0 15681 0 0 0 39952 55 0 0 25 0 1 0 487860135 69148672 14571 4294967295 134512640 134672761 3221224544 3221223728 134615929 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 16882 14571 603 41 0 16841 0 vsize: 67528 [startup+410.055 s] Raw data (loadavg): 0.99 0.95 0.91 2/54 10316 Raw data (stat): 10316 (minisat+) R 10315 22932 22931 0 -1 0 15774 0 0 0 40951 56 0 0 25 0 1 0 487860135 69550080 14664 4294967295 134512640 134672761 3221224544 3221223728 134615724 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 16980 14664 603 41 0 16939 0 vsize: 67920 [startup+420.055 s] Raw data (loadavg): 0.99 0.95 0.91 2/54 10316 Raw data (stat): 10316 (minisat+) R 10315 22932 22931 0 -1 0 15884 0 0 0 41950 57 0 0 25 0 1 0 487860135 69951488 14774 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 17078 14774 603 41 0 17037 0 vsize: 68312 [startup+430.056 s] Raw data (loadavg): 0.99 0.95 0.91 2/54 10316 Raw data (stat): 10316 (minisat+) R 10315 22932 22931 0 -1 0 16055 0 0 0 42950 57 0 0 25 0 1 0 487860135 70623232 14945 4294967295 134512640 134672761 3221224544 3221223728 134615591 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 17242 14945 603 41 0 17201 0 vsize: 68968 [startup+440.055 s] Raw data (loadavg): 0.99 0.95 0.91 2/54 10316 Raw data (stat): 10316 (minisat+) R 10315 22932 22931 0 -1 0 16219 0 0 0 43950 58 0 0 25 0 1 0 487860135 71286784 15109 4294967295 134512640 134672761 3221224544 3221223728 134615791 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 17404 15109 603 41 0 17363 0 vsize: 69616 [startup+450.056 s] Raw data (loadavg): 0.99 0.95 0.91 2/54 10316 Raw data (stat): 10316 (minisat+) R 10315 22932 22931 0 -1 0 16337 0 0 0 44949 59 0 0 25 0 1 0 487860135 71815168 15227 4294967295 134512640 134672761 3221224544 3221223668 134566037 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 17533 15227 603 41 0 17492 0 vsize: 70132 [startup+460.057 s] Raw data (loadavg): 0.99 0.95 0.91 2/54 10316 Raw data (stat): 10316 (minisat+) R 10315 22932 22931 0 -1 0 16506 0 0 0 45949 59 0 0 25 0 1 0 487860135 72486912 15396 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 17697 15396 603 41 0 17656 0 vsize: 70788 [startup+470.056 s] Raw data (loadavg): 0.99 0.96 0.91 2/54 10316 Raw data (stat): 10316 (minisat+) R 10315 22932 22931 0 -1 0 16610 0 0 0 46948 60 0 0 25 0 1 0 487860135 72888320 15500 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 17795 15500 603 41 0 17754 0 vsize: 71180 [startup+480.056 s] Raw data (loadavg): 0.99 0.96 0.91 2/54 10316 Raw data (stat): 10316 (minisat+) R 10315 22932 22931 0 -1 0 16691 0 0 0 47948 60 0 0 25 0 1 0 487860135 73158656 15581 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 17861 15581 603 41 0 17820 0 vsize: 71444 [startup+490.055 s] Raw data (loadavg): 0.99 0.96 0.91 2/54 10316 Raw data (stat): 10316 (minisat+) R 10315 22932 22931 0 -1 0 16847 0 0 0 48947 61 0 0 25 0 1 0 487860135 73830400 15737 4294967295 134512640 134672761 3221224544 3221223728 134615940 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 18025 15737 603 41 0 17984 0 vsize: 72100 [startup+500.056 s] Raw data (loadavg): 0.99 0.96 0.91 2/54 10316 Raw data (stat): 10316 (minisat+) R 10315 22932 22931 0 -1 0 16961 0 0 0 49947 62 0 0 25 0 1 0 487860135 74231808 15851 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 18123 15851 603 41 0 18082 0 vsize: 72492 [startup+510.056 s] Raw data (loadavg): 0.99 0.96 0.91 2/54 10316 Raw data (stat): 10316 (minisat+) R 10315 22932 22931 0 -1 0 17047 0 0 0 50947 62 0 0 25 0 1 0 487860135 74633216 15937 4294967295 134512640 134672761 3221224544 3221223728 134615720 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 18221 15937 603 41 0 18180 0 vsize: 72884 [startup+520.056 s] Raw data (loadavg): 0.99 0.96 0.91 2/54 10316 Raw data (stat): 10316 (minisat+) R 10315 22932 22931 0 -1 0 17193 0 0 0 51946 62 0 0 25 0 1 0 487860135 75165696 16083 4294967295 134512640 134672761 3221224544 3221223668 134566142 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 18351 16083 603 41 0 18310 0 vsize: 73404 [startup+530.056 s] Raw data (loadavg): 0.99 0.96 0.91 2/54 10316 Raw data (stat): 10316 (minisat+) R 10315 22932 22931 0 -1 0 17308 0 0 0 52946 63 0 0 25 0 1 0 487860135 75567104 16198 4294967295 134512640 134672761 3221224544 3221223728 134615703 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 18449 16198 603 41 0 18408 0 vsize: 73796 [startup+540.056 s] Raw data (loadavg): 0.99 0.96 0.91 2/54 10316 Raw data (stat): 10316 (minisat+) R 10315 22932 22931 0 -1 0 17471 0 0 0 53945 64 0 0 25 0 1 0 487860135 76234752 16361 4294967295 134512640 134672761 3221224544 3221223728 134615929 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 18612 16361 603 41 0 18571 0 vsize: 74448 [startup+550.056 s] Raw data (loadavg): 0.99 0.96 0.91 2/54 10316 Raw data (stat): 10316 (minisat+) R 10315 22932 22931 0 -1 0 17769 0 0 0 54945 65 0 0 25 0 1 0 487860135 77430784 16659 4294967295 134512640 134672761 3221224544 3221223728 134615752 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 18904 16659 603 41 0 18863 0 vsize: 75616 [startup+560.056 s] Raw data (loadavg): 0.99 0.96 0.91 2/54 10316 Raw data (stat): 10316 (minisat+) R 10315 22932 22931 0 -1 0 18035 0 0 0 55944 66 0 0 25 0 1 0 487860135 78491648 16925 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 19163 16925 603 41 0 19122 0 vsize: 76652 [startup+570.056 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 10316 Raw data (stat): 10316 (minisat+) R 10315 22932 22931 0 -1 0 18225 0 0 0 56942 67 0 0 25 0 1 0 487860135 79286272 17115 4294967295 134512640 134672761 3221224544 3221223728 134615632 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 19357 17115 603 41 0 19316 0 vsize: 77428 [startup+580.056 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 10316 Raw data (stat): 10316 (minisat+) R 10315 22932 22931 0 -1 0 18301 0 0 0 57942 67 0 0 25 0 1 0 487860135 79548416 17191 4294967295 134512640 134672761 3221224544 3221223728 134615549 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 19421 17191 603 41 0 19380 0 vsize: 77684 [startup+590.056 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 10316 Raw data (stat): 10316 (minisat+) R 10315 22932 22931 0 -1 0 18391 0 0 0 58942 68 0 0 25 0 1 0 487860135 79949824 17281 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 19519 17281 603 41 0 19478 0 vsize: 78076 [startup+600.057 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 10316 Raw data (stat): 10316 (minisat+) R 10315 22932 22931 0 -1 0 18540 0 0 0 59941 68 0 0 25 0 1 0 487860135 80613376 17430 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 19681 17430 603 41 0 19640 0 vsize: 78724 [startup+610.056 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 10316 Raw data (stat): 10316 (minisat+) R 10315 22932 22931 0 -1 0 18692 0 0 0 60941 69 0 0 25 0 1 0 487860135 81145856 17582 4294967295 134512640 134672761 3221224544 3221223728 134615665 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 19811 17582 603 41 0 19770 0 vsize: 79244 [startup+620.056 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 10316 Raw data (stat): 10316 (minisat+) R 10315 22932 22931 0 -1 0 18771 0 0 0 61941 69 0 0 25 0 1 0 487860135 81551360 17661 4294967295 134512640 134672761 3221224544 3221223728 134615739 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 19910 17661 603 41 0 19869 0 vsize: 79640 [startup+630.055 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 10316 Raw data (stat): 10316 (minisat+) R 10315 22932 22931 0 -1 0 18902 0 0 0 62941 69 0 0 25 0 1 0 487860135 81948672 17792 4294967295 134512640 134672761 3221224544 3221223536 134565045 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 20007 17792 603 41 0 19966 0 vsize: 80028 [startup+640.056 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 10316 Raw data (stat): 10316 (minisat+) R 10315 22932 22931 0 -1 0 19354 0 0 0 63940 70 0 0 25 0 1 0 487860135 84865024 18244 4294967295 134512640 134672761 3221224544 3221223728 134615736 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 20719 18244 603 41 0 20678 0 vsize: 82876 [startup+650.056 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 10316 Raw data (stat): 10316 (minisat+) R 10315 22932 22931 0 -1 0 19975 0 0 0 64939 72 0 0 25 0 1 0 487860135 87375872 18865 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 21332 18865 603 41 0 21291 0 vsize: 85328 [startup+660.056 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 10316 Raw data (stat): 10316 (minisat+) R 10315 22932 22931 0 -1 0 20162 0 0 0 65938 73 0 0 25 0 1 0 487860135 88166400 19052 4294967295 134512640 134672761 3221224544 3221223728 134615929 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 21525 19052 603 41 0 21484 0 vsize: 86100 [startup+670.056 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 10316 Raw data (stat): 10316 (minisat+) R 10315 22932 22931 0 -1 0 20349 0 0 0 66938 73 0 0 25 0 1 0 487860135 88956928 19239 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 21718 19239 603 41 0 21677 0 vsize: 86872 [startup+680.055 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 10316 Raw data (stat): 10316 (minisat+) R 10315 22932 22931 0 -1 0 20573 0 0 0 67937 74 0 0 25 0 1 0 487860135 89747456 19463 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 21911 19463 603 41 0 21870 0 vsize: 87644 [startup+690.055 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 10316 Raw data (stat): 10316 (minisat+) R 10315 22932 22931 0 -1 0 20861 0 0 0 68937 75 0 0 25 0 1 0 487860135 90939392 19751 4294967295 134512640 134672761 3221224544 3221223668 134566029 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 22202 19751 603 41 0 22161 0 vsize: 88808 [startup+700.056 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 10316 Raw data (stat): 10316 (minisat+) R 10315 22932 22931 0 -1 0 21644 0 0 0 69935 77 0 0 25 0 1 0 487860135 94105600 20534 4294967295 134512640 134672761 3221224544 3221223728 134615964 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 22975 20534 603 41 0 22934 0 vsize: 91900 [startup+710.056 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 10316 Raw data (stat): 10316 (minisat+) R 10315 22932 22931 0 -1 0 21839 0 0 0 70935 77 0 0 25 0 1 0 487860135 94900224 20729 4294967295 134512640 134672761 3221224544 3221223728 134615807 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 23169 20729 603 41 0 23128 0 vsize: 92676 [startup+720.056 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 10316 Raw data (stat): 10316 (minisat+) R 10315 22932 22931 0 -1 0 22065 0 0 0 71934 78 0 0 25 0 1 0 487860135 95830016 20955 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 23396 20956 603 41 0 23355 0 vsize: 93584 [startup+730.057 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 10316 Raw data (stat): 10316 (minisat+) R 10315 22932 22931 0 -1 0 22318 0 0 0 72933 79 0 0 25 0 1 0 487860135 96894976 21208 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 23656 21208 603 41 0 23615 0 vsize: 94624 [startup+740.056 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 10316 Raw data (stat): 10316 (minisat+) R 10315 22932 22931 0 -1 0 22598 0 0 0 73933 80 0 0 25 0 1 0 487860135 97955840 21488 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 23915 21488 603 41 0 23874 0 vsize: 95660 [startup+750.056 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 10316 Raw data (stat): 10316 (minisat+) R 10315 22932 22931 0 -1 0 22745 0 0 0 74932 80 0 0 25 0 1 0 487860135 98623488 21635 4294967295 134512640 134672761 3221224544 3221223728 134615807 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 24078 21635 603 41 0 24037 0 vsize: 96312 [startup+760.056 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 10316 Raw data (stat): 10316 (minisat+) R 10315 22932 22931 0 -1 0 22938 0 0 0 75932 81 0 0 25 0 1 0 487860135 99291136 21828 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 24241 21828 603 41 0 24200 0 vsize: 96964 [startup+770.056 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 10316 Raw data (stat): 10316 (minisat+) R 10315 22932 22931 0 -1 0 23207 0 0 0 76931 82 0 0 25 0 1 0 487860135 100487168 22097 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 24533 22097 603 41 0 24492 0 vsize: 98132 [startup+780.056 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 10316 Raw data (stat): 10316 (minisat+) R 10315 22932 22931 0 -1 0 23480 0 0 0 77930 83 0 0 25 0 1 0 487860135 101560320 22370 4294967295 134512640 134672761 3221224544 3221223728 134615791 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 24795 22370 603 41 0 24754 0 vsize: 99180 [startup+790.055 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 10316 Raw data (stat): 10316 (minisat+) R 10315 22932 22931 0 -1 0 23801 0 0 0 78929 84 0 0 25 0 1 0 487860135 102760448 22691 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 25088 22691 603 41 0 25047 0 vsize: 100352 [startup+800.055 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 10316 Raw data (stat): 10316 (minisat+) R 10315 22932 22931 0 -1 0 24030 0 0 0 79928 85 0 0 25 0 1 0 487860135 103698432 22920 4294967295 134512640 134672761 3221224544 3221223584 134612632 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 25317 22920 603 41 0 25276 0 vsize: 101268 [startup+810.055 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 10316 Raw data (stat): 10316 (minisat+) R 10315 22932 22931 0 -1 0 24228 0 0 0 80927 86 0 0 25 0 1 0 487860135 104501248 23118 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 25513 23118 603 41 0 25472 0 vsize: 102052 [startup+820.054 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 10316 Raw data (stat): 10316 (minisat+) R 10315 22932 22931 0 -1 0 24454 0 0 0 81927 87 0 0 25 0 1 0 487860135 105431040 23344 4294967295 134512640 134672761 3221224544 3221223728 134615608 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 25740 23344 603 41 0 25699 0 vsize: 102960 [startup+830.055 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 10316 Raw data (stat): 10316 (minisat+) R 10315 22932 22931 0 -1 0 24630 0 0 0 82926 88 0 0 25 0 1 0 487860135 106094592 23520 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 25902 23520 603 41 0 25861 0 vsize: 103608 [startup+840.055 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 10316 Raw data (stat): 10316 (minisat+) R 10315 22932 22931 0 -1 0 25502 0 0 0 83925 90 0 0 25 0 1 0 487860135 109068288 24048 4294967295 134512640 134672761 3221224544 3221223728 134615705 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 26628 24048 603 41 0 26587 0 vsize: 106512 [startup+850.055 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 10316 Raw data (stat): 10316 (minisat+) R 10315 22932 22931 0 -1 0 25502 0 0 0 84925 90 0 0 25 0 1 0 487860135 109068288 24048 4294967295 134512640 134672761 3221224544 3221223728 134615705 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 26628 24048 603 41 0 26587 0 vsize: 106512 [startup+860.055 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 10316 Raw data (stat): 10316 (minisat+) R 10315 22932 22931 0 -1 0 25502 0 0 0 85925 90 0 0 25 0 1 0 487860135 109068288 24048 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 26628 24048 603 41 0 26587 0 vsize: 106512 [startup+870.055 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 10316 Raw data (stat): 10316 (minisat+) R 10315 22932 22931 0 -1 0 25502 0 0 0 86925 90 0 0 25 0 1 0 487860135 109068288 24048 4294967295 134512640 134672761 3221224544 3221223728 134615601 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 26628 24048 603 41 0 26587 0 vsize: 106512 [startup+880.055 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 10316 Raw data (stat): 10316 (minisat+) R 10315 22932 22931 0 -1 0 25502 0 0 0 87925 90 0 0 25 0 1 0 487860135 109068288 24048 4294967295 134512640 134672761 3221224544 3221223696 134565045 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 26628 24048 603 41 0 26587 0 vsize: 106512 [startup+890.055 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 10316 Raw data (stat): 10316 (minisat+) R 10315 22932 22931 0 -1 0 25502 0 0 0 88925 90 0 0 25 0 1 0 487860135 109068288 24048 4294967295 134512640 134672761 3221224544 3221223680 134614753 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 26628 24048 603 41 0 26587 0 vsize: 106512 [startup+900.055 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 10316 Raw data (stat): 10316 (minisat+) R 10315 22932 22931 0 -1 0 25502 0 0 0 89926 90 0 0 25 0 1 0 487860135 109068288 24048 4294967295 134512640 134672761 3221224544 3221223728 134615804 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 26628 24048 603 41 0 26587 0 vsize: 106512 [startup+910.055 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 10316 Raw data (stat): 10316 (minisat+) R 10315 22932 22931 0 -1 0 25502 0 0 0 90926 90 0 0 25 0 1 0 487860135 109068288 24048 4294967295 134512640 134672761 3221224544 3221223712 134564729 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 26628 24048 603 41 0 26587 0 vsize: 106512 [startup+920.054 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 10316 Raw data (stat): 10316 (minisat+) R 10315 22932 22931 0 -1 0 25502 0 0 0 91926 90 0 0 25 0 1 0 487860135 109068288 24048 4294967295 134512640 134672761 3221224544 3221223728 134615549 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 26628 24048 603 41 0 26587 0 vsize: 106512 [startup+930.054 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 10316 Raw data (stat): 10316 (minisat+) R 10315 22932 22931 0 -1 0 25502 0 0 0 92926 90 0 0 25 0 1 0 487860135 109068288 24048 4294967295 134512640 134672761 3221224544 3221223668 134566043 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 26628 24048 603 41 0 26587 0 vsize: 106512 [startup+940.055 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 10316 Raw data (stat): 10316 (minisat+) R 10315 22932 22931 0 -1 0 25502 0 0 0 93926 90 0 0 25 0 1 0 487860135 109068288 24048 4294967295 134512640 134672761 3221224544 3221223728 134615673 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 26628 24048 603 41 0 26587 0 vsize: 106512 [startup+950.055 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 10316 Raw data (stat): 10316 (minisat+) R 10315 22932 22931 0 -1 0 25502 0 0 0 94927 90 0 0 25 0 1 0 487860135 109068288 24048 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 26628 24048 603 41 0 26587 0 vsize: 106512 [startup+960.055 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 10316 Raw data (stat): 10316 (minisat+) R 10315 22932 22931 0 -1 0 25502 0 0 0 95927 90 0 0 25 0 1 0 487860135 109068288 24048 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 26628 24048 603 41 0 26587 0 vsize: 106512 [startup+970.055 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 10316 Raw data (stat): 10316 (minisat+) R 10315 22932 22931 0 -1 0 25502 0 0 0 96927 90 0 0 25 0 1 0 487860135 109068288 24048 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 26628 24048 603 41 0 26587 0 vsize: 106512 [startup+980.054 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 10316 Raw data (stat): 10316 (minisat+) R 10315 22932 22931 0 -1 0 25502 0 0 0 97927 90 0 0 25 0 1 0 487860135 109068288 24048 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 26628 24048 603 41 0 26587 0 vsize: 106512 [startup+990.054 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 10316 Raw data (stat): 10316 (minisat+) R 10315 22932 22931 0 -1 0 25502 0 0 0 98927 90 0 0 25 0 1 0 487860135 109068288 24048 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 26628 24048 603 41 0 26587 0 vsize: 106512 [startup+1000.05 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 10316 Raw data (stat): 10316 (minisat+) R 10315 22932 22931 0 -1 0 25502 0 0 0 99928 90 0 0 25 0 1 0 487860135 109068288 24048 4294967295 134512640 134672761 3221224544 3221223680 134614724 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 26628 24048 603 41 0 26587 0 vsize: 106512 [startup+1010.05 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 10316 Raw data (stat): 10316 (minisat+) R 10315 22932 22931 0 -1 0 25502 0 0 0 100928 90 0 0 25 0 1 0 487860135 109068288 24048 4294967295 134512640 134672761 3221224544 3221223728 134615693 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 26628 24048 603 41 0 26587 0 vsize: 106512 [startup+1020.05 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 10316 Raw data (stat): 10316 (minisat+) R 10315 22932 22931 0 -1 0 25502 0 0 0 101928 90 0 0 25 0 1 0 487860135 109068288 24048 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 26628 24048 603 41 0 26587 0 vsize: 106512 [startup+1030.05 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 10316 Raw data (stat): 10316 (minisat+) R 10315 22932 22931 0 -1 0 25502 0 0 0 102928 90 0 0 25 0 1 0 487860135 109068288 24048 4294967295 134512640 134672761 3221224544 3221223536 134565092 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 26628 24048 603 41 0 26587 0 vsize: 106512 [startup+1040.05 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 10316 Raw data (stat): 10316 (minisat+) R 10315 22932 22931 0 -1 0 25502 0 0 0 103928 90 0 0 25 0 1 0 487860135 109068288 24048 4294967295 134512640 134672761 3221224544 3221223728 134615705 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 26628 24048 603 41 0 26587 0 vsize: 106512 [startup+1050.05 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 10316 Raw data (stat): 10316 (minisat+) R 10315 22932 22931 0 -1 0 25502 0 0 0 104928 90 0 0 25 0 1 0 487860135 109068288 24048 4294967295 134512640 134672761 3221224544 3221223728 134615705 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 26628 24048 603 41 0 26587 0 vsize: 106512 [startup+1060.06 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 10316 Raw data (stat): 10316 (minisat+) R 10315 22932 22931 0 -1 0 25502 0 0 0 105929 90 0 0 25 0 1 0 487860135 109068288 24048 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 26628 24048 603 41 0 26587 0 vsize: 106512 [startup+1070.05 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 10316 Raw data (stat): 10316 (minisat+) R 10315 22932 22931 0 -1 0 25502 0 0 0 106929 90 0 0 25 0 1 0 487860135 109068288 24048 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 26628 24048 603 41 0 26587 0 vsize: 106512 [startup+1080.05 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 10316 Raw data (stat): 10316 (minisat+) R 10315 22932 22931 0 -1 0 25502 0 0 0 107929 90 0 0 25 0 1 0 487860135 109068288 24048 4294967295 134512640 134672761 3221224544 3221223668 134566059 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 26628 24048 603 41 0 26587 0 vsize: 106512 [startup+1090.05 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 10316 Raw data (stat): 10316 (minisat+) R 10315 22932 22931 0 -1 0 25502 0 0 0 108929 90 0 0 25 0 1 0 487860135 109068288 24048 4294967295 134512640 134672761 3221224544 3221223680 134614800 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 26628 24048 603 41 0 26587 0 vsize: 106512 [startup+1100.05 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 10316 Raw data (stat): 10316 (minisat+) R 10315 22932 22931 0 -1 0 25502 0 0 0 109929 90 0 0 25 0 1 0 487860135 109068288 24048 4294967295 134512640 134672761 3221224544 3221223712 134614516 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 26628 24048 603 41 0 26587 0 vsize: 106512 [startup+1110.05 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 10316 Raw data (stat): 10316 (minisat+) R 10315 22932 22931 0 -1 0 25502 0 0 0 110930 90 0 0 25 0 1 0 487860135 109068288 24048 4294967295 134512640 134672761 3221224544 3221223668 134566071 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 26628 24048 603 41 0 26587 0 vsize: 106512 [startup+1120.05 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 10316 Raw data (stat): 10316 (minisat+) R 10315 22932 22931 0 -1 0 25502 0 0 0 111930 90 0 0 25 0 1 0 487860135 109068288 24048 4294967295 134512640 134672761 3221224544 3221223668 134566071 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 26628 24048 603 41 0 26587 0 vsize: 106512 [startup+1130.05 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 10316 Raw data (stat): 10316 (minisat+) R 10315 22932 22931 0 -1 0 25502 0 0 0 112930 90 0 0 25 0 1 0 487860135 109068288 24048 4294967295 134512640 134672761 3221224544 3221223728 134615736 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 26628 24048 603 41 0 26587 0 vsize: 106512 [startup+1140.05 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 10316 Raw data (stat): 10316 (minisat+) R 10315 22932 22931 0 -1 0 25502 0 0 0 113930 90 0 0 25 0 1 0 487860135 109068288 24048 4294967295 134512640 134672761 3221224544 3221223728 134615505 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 26628 24048 603 41 0 26587 0 vsize: 106512 [startup+1150.06 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 10316 Raw data (stat): 10316 (minisat+) R 10315 22932 22931 0 -1 0 25502 0 0 0 114930 90 0 0 25 0 1 0 487860135 109068288 24048 4294967295 134512640 134672761 3221224544 3221223728 134615663 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 26628 24048 603 41 0 26587 0 vsize: 106512 [startup+1160.05 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 10316 Raw data (stat): 10316 (minisat+) R 10315 22932 22931 0 -1 0 25502 0 0 0 115930 90 0 0 25 0 1 0 487860135 109068288 24048 4294967295 134512640 134672761 3221224544 3221223728 134615948 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 26628 24048 603 41 0 26587 0 vsize: 106512 [startup+1170.05 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 10316 Raw data (stat): 10316 (minisat+) R 10315 22932 22931 0 -1 0 25502 0 0 0 116931 90 0 0 25 0 1 0 487860135 109068288 24048 4294967295 134512640 134672761 3221224544 3221223728 134615652 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 26628 24048 603 41 0 26587 0 vsize: 106512 [startup+1180.06 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 10316 Raw data (stat): 10316 (minisat+) R 10315 22932 22931 0 -1 0 25502 0 0 0 117931 90 0 0 25 0 1 0 487860135 109068288 24048 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 26628 24048 603 41 0 26587 0 vsize: 106512 [startup+1190.06 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 10316 Raw data (stat): 10316 (minisat+) R 10315 22932 22931 0 -1 0 25502 0 0 0 118931 90 0 0 25 0 1 0 487860135 109068288 24048 4294967295 134512640 134672761 3221224544 3221223728 134615498 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 26628 24048 603 41 0 26587 0 vsize: 106512 [startup+1200.06 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 10316 Raw data (stat): 10316 (minisat+) R 10315 22932 22931 0 -1 0 25502 0 0 0 119931 90 0 0 25 0 1 0 487860135 109068288 24048 4294967295 134512640 134672761 3221224544 3221223728 134615681 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 26628 24048 603 41 0 26587 0 vsize: 106512 Maximum CPU time exceeded: sending SIGTERM and SIGKILL [startup+1200.11 s] Raw data (loadavg): 0.99 0.97 0.91 1/54 10316 Raw data (stat): 10316 (minisat+) Z 10315 22932 22931 0 -1 12 25502 0 0 0 119931 95 0 0 25 0 1 0 487860135 0 0 4294967295 0 0 0 0 0 0 16384 5 16386 3222412051 0 0 17 1 0 0 Raw data (statm): 0 0 0 0 0 0 0 vsize: 0 Maximum CPU time exceeded: sending SIGTERM and SIGKILL Child status: 0 Real time (s): 1200.11 CPU time (s): 1200.27 CPU user time (s): 1199.32 CPU system time (s): 0.952855 CPU usage (%): 100.014 Max. virtual memory (Kb): 106512 #### END WATCHER DATA #### #### BEGIN VERIFIER DATA #### ERROR: no interpretation found ! #### END VERIFIER DATA ####