Name | mps-v2-13-7/MIPLIB/miplib2003/normalized-mps-v2-13-7-pp08aCUTS.opb |
MD5SUM | d1b87efc35bcd73acfc5183bbe3df4f0 |
Bench Category | optimization, medium integers (OPTMEDINT) |
Has Objective Function | YES |
Satisfiable | |
(Un)Satisfiability was proved | |
Best value of the objective function | |
Optimality of the best value was proved | |
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 | |
Best CPU time to get the best result obtained on this benchmark | |
Number of variables | 3288 |
Total number of constraints | 374 |
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 | 310 |
Minimum length of a constraint | 1 |
Maximum length of a constraint | 123 |
LAUNCH ON wulflinc23 THE 2005-09-20 03:52:01 (client local time) PB2005-SCRIPT v4.0 MARKUPS: idlaunch=3319 boxname=wulflinc23 idbench=975 idsolver=3 numberseed=0 MD5SUM SOLVER: MD5SUM BENCH: d1b87efc35bcd73acfc5183bbe3df4f0 /oldhome/oroussel/tmp/wulflinc23/normalized-mps-v2-13-7-pp08aCUTS.opb REAL COMMAND: minisat+_script /oldhome/oroussel/tmp/wulflinc23/normalized-mps-v2-13-7-pp08aCUTS.opb IDLAUNCH: 3319 /proc/cpuinfo: processor : 0 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 3 cpu MHz : 451.037 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 : 3 cpu MHz : 451.037 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: 910388 kB Buffers: 15668 kB Cached: 81072 kB SwapCached: 840 kB Active: 28132 kB Inactive: 71256 kB HighTotal: 131008 kB HighFree: 48776 kB LowTotal: 903652 kB LowFree: 861612 kB SwapTotal: 2097136 kB SwapFree: 2095788 kB Dirty: 28 kB Writeback: 0 kB Mapped: 5668 kB Slab: 19312 kB Committed_AS: 64152 kB PageTables: 328 kB VmallocTotal: 114680 kB VmallocUsed: 1364 kB VmallocChunk: 113256 kB JOB ENDED THE 2005-09-20 04:12:13 (client local time) WITH STATUS 0 IN 1208.76 SECONDS stats: 3319 7 1208.76 0
c Parsing PB file... c Converting 374 PB-constraints to clauses... c -- Unit propagations: (none) c -- Detecting intervals from adjacent constraints: ################################################################ c -- Clauses(.)/Splits(s): ssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssss c ---[ 501]---> BDD-cost: 15 c ---[ 500]---> BDD-cost: 15 c ---[ 499]---> BDD-cost: 15 c ---[ 498]---> BDD-cost: 15 c ---[ 497]---> BDD-cost: 15 c ---[ 496]---> BDD-cost: 15 c ---[ 495]---> BDD-cost: 15 c ---[ 494]---> BDD-cost: 15 c ---[ 485]---> BDD-cost: 15 c ---[ 484]---> BDD-cost: 15 c ---[ 483]---> BDD-cost: 15 c ---[ 482]---> BDD-cost: 15 c ---[ 481]---> BDD-cost: 15 c ---[ 480]---> BDD-cost: 15 c ---[ 479]---> BDD-cost: 15 c ---[ 477]---> BDD-cost: 15 c ---[ 476]---> BDD-cost: 15 c ---[ 475]---> BDD-cost: 15 c ---[ 474]---> BDD-cost: 15 c ---[ 473]---> BDD-cost: 15 c ---[ 472]---> BDD-cost: 15 c ---[ 471]---> BDD-cost: 15 c ---[ 469]---> BDD-cost: 14 c ---[ 468]---> BDD-cost: 14 c ---[ 467]---> BDD-cost: 14 c ---[ 466]---> BDD-cost: 14 c ---[ 465]---> BDD-cost: 14 c ---[ 464]---> BDD-cost: 14 c ---[ 463]---> BDD-cost: 14 c ---[ 462]---> BDD-cost: 14 c ---[ 461]---> BDD-cost: 15 c ---[ 460]---> BDD-cost: 15 c ---[ 459]---> BDD-cost: 15 c ---[ 458]---> BDD-cost: 15 c ---[ 457]---> BDD-cost: 15 c ---[ 456]---> BDD-cost: 15 c ---[ 455]---> BDD-cost: 15 c ---[ 454]---> BDD-cost: 15 c ---[ 445]---> BDD-cost: 13 c ---[ 444]---> BDD-cost: 13 c ---[ 443]---> BDD-cost: 13 c ---[ 442]---> BDD-cost: 13 c ---[ 441]---> BDD-cost: 13 c ---[ 440]---> BDD-cost: 13 c ---[ 439]---> BDD-cost: 13 c ---[ 438]---> BDD-cost: 13 c ---[ 436]---> BDD-cost: 158 c ---[ 434]---> Sorter-cost: 1160 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 433]---> BDD-cost: 6 c ---[ 432]---> BDD-cost: 6 c ---[ 431]---> BDD-cost: 6 c ---[ 430]---> BDD-cost: 6 c ---[ 429]---> BDD-cost: 23 c ---[ 428]---> BDD-cost: 4 c ---[ 427]---> BDD-cost: 4 c ---[ 426]---> BDD-cost: 4 c ---[ 425]---> BDD-cost: 4 c ---[ 424]---> BDD-cost: 4 c ---[ 422]---> Sorter-cost: 1160 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 421]---> BDD-cost: 4 c ---[ 420]---> BDD-cost: 4 c ---[ 419]---> BDD-cost: 4 c ---[ 418]---> BDD-cost: 9 c ---[ 417]---> BDD-cost: 9 c ---[ 416]---> BDD-cost: 9 c ---[ 415]---> BDD-cost: 6 c ---[ 414]---> BDD-cost: 6 c ---[ 413]---> BDD-cost: 6 c ---[ 412]---> BDD-cost: 6 c ---[ 410]---> Sorter-cost: 1160 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 409]---> BDD-cost: 6 c ---[ 408]---> BDD-cost: 19 c ---[ 407]---> BDD-cost: 19 c ---[ 406]---> BDD-cost: 19 c ---[ 405]---> BDD-cost: 19 c ---[ 404]---> BDD-cost: 19 c ---[ 403]---> BDD-cost: 19 c ---[ 402]---> BDD-cost: 19 c ---[ 401]---> BDD-cost: 19 c ---[ 400]---> BDD-cost: 6 c ---[ 398]---> Sorter-cost: 1160 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 397]---> BDD-cost: 6 c ---[ 396]---> BDD-cost: 6 c ---[ 395]---> BDD-cost: 6 c ---[ 394]---> BDD-cost: 6 c ---[ 393]---> BDD-cost: 6 c ---[ 392]---> BDD-cost: 6 c ---[ 391]---> BDD-cost: 6 c ---[ 386]---> Sorter-cost: 1160 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 374]---> Sorter-cost: 1160 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 362]---> Sorter-cost: 418 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 350]---> Sorter-cost: 427 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 338]---> Sorter-cost: 1179 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 326]---> Sorter-cost: 1179 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 314]---> Sorter-cost: 1179 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 312]---> Sorter-cost: 1179 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 300]---> Sorter-cost: 1179 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 288]---> Sorter-cost: 1179 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 276]---> Sorter-cost: 1179 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 264]---> Sorter-cost: 427 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 255]---> BDD-cost: 158 c ---[ 253]---> Sorter-cost: 1179 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 251]---> Sorter-cost: 1179 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 249]---> Sorter-cost: 1179 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 247]---> Sorter-cost: 1179 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 245]---> Sorter-cost: 1179 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 243]---> Sorter-cost: 1179 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 241]---> Sorter-cost: 1179 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 239]---> Sorter-cost: 427 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 237]---> Sorter-cost: 418 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 235]---> Sorter-cost: 1160 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 233]---> Sorter-cost: 1160 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 231]---> Sorter-cost: 1160 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 229]---> Sorter-cost: 1160 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 227]---> Sorter-cost: 1160 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 225]---> Sorter-cost: 1160 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 223]---> Sorter-cost: 1179 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 221]---> Sorter-cost: 418 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 219]---> Sorter-cost: 427 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 217]---> Sorter-cost: 1179 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 215]---> Sorter-cost: 1179 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 213]---> Sorter-cost: 1179 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 211]---> Sorter-cost: 1179 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 209]---> Sorter-cost: 1179 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 207]---> Sorter-cost: 1179 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 205]---> Sorter-cost: 427 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 203]---> BDD-cost: 154 c ---[ 201]---> Sorter-cost: 1179 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 199]---> Sorter-cost: 1160 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 197]---> Sorter-cost: 1160 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 195]---> Sorter-cost: 1160 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 193]---> Sorter-cost: 1160 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 191]---> Sorter-cost: 1160 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 189]---> Sorter-cost: 1160 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 187]---> Sorter-cost: 418 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 185]---> Sorter-cost: 409 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 183]---> Sorter-cost: 1141 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 181]---> Sorter-cost: 1141 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 179]---> Sorter-cost: 1179 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 177]---> Sorter-cost: 1141 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 175]---> Sorter-cost: 1141 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 173]---> Sorter-cost: 1141 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 171]---> Sorter-cost: 1141 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 169]---> Sorter-cost: 409 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 168]---> Sorter-cost: 1961 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 167]---> Sorter-cost: 1961 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 166]---> Sorter-cost: 1961 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 165]---> Sorter-cost: 1961 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 164]---> Sorter-cost: 1961 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 162]---> Sorter-cost: 1179 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 161]---> Sorter-cost: 1961 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 160]---> Sorter-cost: 1961 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 159]---> Sorter-cost: 1961 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 158]---> BDD-cost: 9 c ---[ 157]---> BDD-cost: 9 c ---[ 156]---> BDD-cost: 9 c ---[ 155]---> BDD-cost: 6 c ---[ 154]---> BDD-cost: 6 c ---[ 153]---> BDD-cost: 6 c ---[ 152]---> BDD-cost: 6 c ---[ 150]---> Sorter-cost: 427 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 149]---> BDD-cost: 8 c ---[ 148]---> BDD-cost: 19 c ---[ 147]---> BDD-cost: 19 c ---[ 146]---> BDD-cost: 19 c ---[ 145]---> BDD-cost: 19 c ---[ 144]---> BDD-cost: 19 c ---[ 143]---> BDD-cost: 19 c ---[ 142]---> BDD-cost: 19 c ---[ 141]---> BDD-cost: 19 c ---[ 140]---> BDD-cost: 9 c ---[ 138]---> Sorter-cost: 418 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 137]---> BDD-cost: 9 c ---[ 136]---> BDD-cost: 9 c ---[ 135]---> BDD-cost: 6 c ---[ 134]---> BDD-cost: 6 c ---[ 133]---> BDD-cost: 6 c ---[ 132]---> BDD-cost: 6 c ---[ 131]---> BDD-cost: 23 c ---[ 130]---> BDD-cost: 9 c ---[ 129]---> BDD-cost: 9 c ---[ 128]---> BDD-cost: 9 c ---[ 127]---> BDD-cost: 1 c ---[ 126]---> BDD-cost: 1 c ---[ 125]---> BDD-cost: 1 c ---[ 124]---> BDD-cost: 1 c ---[ 123]---> BDD-cost: 1 c ---[ 122]---> BDD-cost: 1 c ---[ 121]---> BDD-cost: 1 c ---[ 120]---> BDD-cost: 1 c ---[ 119]---> BDD-cost: 1 c ---[ 118]---> BDD-cost: 1 c ---[ 117]---> BDD-cost: 1 c ---[ 116]---> BDD-cost: 1 c ---[ 115]---> BDD-cost: 1 c ---[ 114]---> BDD-cost: 1 c ---[ 113]---> BDD-cost: 1 c ---[ 112]---> BDD-cost: 1 c ---[ 111]---> BDD-cost: 1 c ---[ 110]---> BDD-cost: 1 c ---[ 109]---> BDD-cost: 50 c ---[ 108]---> BDD-cost: 203 c ---[ 107]---> BDD-cost: 45 c ---[ 106]---> BDD-cost: 194 c ---[ 105]---> BDD-cost: 48 c ---[ 104]---> BDD-cost: 191 c ---[ 103]---> BDD-cost: 38 c ---[ 102]---> BDD-cost: 173 c ---[ 101]---> BDD-cost: 44 c ---[ 100]---> BDD-cost: 167 c ---[ 99]---> BDD-cost: 5 c ---[ 98]---> BDD-cost: 73 c ---[ 97]---> BDD-cost: 3 c ---[ 96]---> BDD-cost: 62 c ---[ 95]---> BDD-cost: 41 c ---[ 94]---> BDD-cost: 158 c ---[ 93]---> BDD-cost: 45 c ---[ 92]---> BDD-cost: 182 c ---[ 91]---> BDD-cost: 40 c ---[ 90]---> BDD-cost: 173 c ---[ 89]---> BDD-cost: 35 c ---[ 88]---> BDD-cost: 164 c ---[ 87]---> BDD-cost: 41 c ---[ 86]---> BDD-cost: 158 c ---[ 85]---> BDD-cost: 5 c ---[ 84]---> BDD-cost: 70 c ---[ 83]---> BDD-cost: 3 c ---[ 82]---> BDD-cost: 65 c ---[ 81]---> BDD-cost: 45 c ---[ 80]---> BDD-cost: 194 c ---[ 79]---> BDD-cost: 48 c ---[ 78]---> BDD-cost: 191 c ---[ 77]---> BDD-cost: 41 c ---[ 76]---> BDD-cost: 170 c ---[ 75]---> BDD-cost: 44 c ---[ 74]---> BDD-cost: 167 c ---[ 73]---> BDD-cost: 50 c ---[ 72]---> BDD-cost: 203 c ---[ 71]---> BDD-cost: 3 c ---[ 70]---> BDD-cost: 61 c ---[ 69]---> BDD-cost: 48 c ---[ 68]---> BDD-cost: 191 c ---[ 67]---> BDD-cost: 48 c ---[ 66]---> BDD-cost: 191 c ---[ 65]---> BDD-cost: 55 c ---[ 64]---> Sorter-cost: 751 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 63]---> BDD-cost: 47 c ---[ 62]---> BDD-cost: 161 c ---[ 61]---> BDD-cost: 50 c ---[ 60]---> BDD-cost: 203 c ---[ 59]---> BDD-cost: 48 c ---[ 58]---> BDD-cost: 191 c ---[ 57]---> BDD-cost: 5 c ---[ 56]---> BDD-cost: 73 c ---[ 55]---> BDD-cost: 5 c ---[ 54]---> BDD-cost: 70 c ---[ 53]---> BDD-cost: 38 c ---[ 52]---> BDD-cost: 161 c ---[ 51]---> BDD-cost: 41 c ---[ 50]---> BDD-cost: 158 c ---[ 49]---> BDD-cost: 35 c ---[ 48]---> BDD-cost: 164 c ---[ 47]---> BDD-cost: 35 c ---[ 46]---> BDD-cost: 164 c ---[ 45]---> BDD-cost: 38 c ---[ 44]---> BDD-cost: 161 c ---[ 43]---> BDD-cost: 3 c ---[ 42]---> BDD-cost: 64 c ---[ 41]---> BDD-cost: 6 c ---[ 40]---> BDD-cost: 78 c ---[ 39]---> BDD-cost: 41 c ---[ 38]---> BDD-cost: 170 c ---[ 37]---> BDD-cost: 41 c ---[ 36]---> BDD-cost: 170 c ---[ 35]---> BDD-cost: 41 c ---[ 34]---> BDD-cost: 170 c ---[ 33]---> BDD-cost: 48 c ---[ 32]---> BDD-cost: 191 c ---[ 31]---> BDD-cost: 38 c ---[ 30]---> BDD-cost: 173 c ---[ 29]---> BDD-cost: 41 c ---[ 28]---> BDD-cost: 170 c ---[ 27]---> BDD-cost: 5 c ---[ 26]---> BDD-cost: 75 c ---[ 25]---> BDD-cost: 38 c ---[ 24]---> BDD-cost: 161 c ---[ 23]---> BDD-cost: 45 c ---[ 22]---> BDD-cost: 182 c ---[ 21]---> BDD-cost: 35 c ---[ 20]---> BDD-cost: 164 c ---[ 19]---> BDD-cost: 38 c ---[ 18]---> BDD-cost: 161 c ---[ 17]---> BDD-cost: 43 c ---[ 16]---> BDD-cost: 170 c ---[ 15]---> BDD-cost: 41 c ---[ 14]---> BDD-cost: 158 c ---[ 13]---> BDD-cost: 3 c ---[ 12]---> BDD-cost: 60 c ---[ 11]---> BDD-cost: 3 c ---[ 10]---> BDD-cost: 59 c ---[ 9]---> BDD-cost: 38 c ---[ 8]---> BDD-cost: 149 c ---[ 7]---> BDD-cost: 35 c ---[ 6]---> BDD-cost: 152 c ---[ 5]---> BDD-cost: 35 c ---[ 4]---> BDD-cost: 152 c ---[ 3]---> BDD-cost: 38 c ---[ 2]---> BDD-cost: 149 c ---[ 1]---> BDD-cost: 4 c ---[ 0]---> BDD-cost: 62 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 0 | 215438 519594 | 71812 0 0 nan | 0.000 % | c | 101 | 215326 519346 | 78993 79 271 3.4 | 4.796 % | c | 251 | 215165 518988 | 86892 203 739 3.6 | 4.854 % | c | 476 | 215013 518651 | 95581 405 1451 3.6 | 4.912 % | c | 814 | 214882 518363 | 105139 718 2555 3.6 | 4.964 % | c | 1320 | 214188 516814 | 115653 1138 3953 3.5 | 5.212 % | c | 2079 | 213603 515514 | 127219 1804 6333 3.5 | 5.426 % | c | 3218 | 213209 514630 | 139941 2898 10656 3.7 | 5.562 % | c | 4926 | 212696 513482 | 153935 4545 17723 3.9 | 5.742 % | c | 7488 | 211648 511137 | 169328 6973 28093 4.0 | 6.108 % | c | 11332 | 210588 508770 | 186261 10695 45175 4.2 | 6.481 % | c | 17098 | 208970 505150 | 204888 16237 70107 4.3 | 7.050 % | c | 25747 | 207655 502206 | 225376 24727 121042 4.9 | 7.504 % | c | 38721 | 206711 500085 | 247914 37579 208692 5.6 | 7.832 % | c | 58183 | 206122 498761 | 272705 56950 373165 6.6 | 8.033 % | c | 87375 | 206065 498634 | 299976 86132 1052463 12.2 | 8.053 % | c | 131164 | 205853 498158 | 329974 129888 2014357 15.5 | 8.128 % | c | 196848 | 205590 497567 | 362971 195540 3544352 18.1 | 8.217 % | c | 295374 | 205512 497392 | 399268 294054 6084326 20.7 | 8.247 % | c | 443164 | 205325 496976 | 439195 68442 994490 14.5 | 8.316 % |
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/27245/stat): 27245 (minisat+_script) R 27244 27245 5299 0 -1 0 19 0 0 0 0 0 0 0 22 0 1 0 1855450281 712704 3 4294967295 134512640 135087896 3221224496 3221224496 1073744960 0 0 5 0 0 0 0 17 0 0 0 Raw data (/proc/27245/statm): 174 3 169 147 0 27 0 [pid=27245] 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=27246 New process pid=27247 New process pid=27248 execve syscall for /bin/sed executable One traced child (pid=27247) 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=27248) exited with status: 0 One traced child (pid=27246) exited with status: 0 New process pid=27249 execve syscall for /oldhome/oroussel/solvers/minisat+_64-bit_static executable open syscall for file /dev/null open syscall for file /oldhome/oroussel/tmp/wulflinc23/normalized-mps-v2-13-7-pp08aCUTS.opb [startup+10.004 s] Raw data (loadavg): 1.00 0.97 0.96 2/57 27249 Raw data (/proc/27245/stat): 27245 (minisat+_script) S 27244 27245 5299 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1855450281 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27245/statm): 531 226 485 147 0 384 0 [pid=27245] vsize: 2124 Raw data (/proc/27249/stat): 27249 (minisat+_64-bit) R 27245 27245 5299 0 -1 0 7025 0 0 0 939 30 0 0 25 0 1 0 1855450286 31629312 6668 4294967295 134512640 135094434 3221224432 3221223116 134553432 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27249/statm): 7722 6668 145 145 0 7577 0 [pid=27249] vsize: 30888 Current children cumulated CPU time (s) 9.71 Current children cumulated vsize (Kb) 33012 [startup+20.0046 s] Raw data (loadavg): 1.00 0.97 0.96 2/57 27249 Raw data (/proc/27245/stat): 27245 (minisat+_script) S 27244 27245 5299 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1855450281 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27245/statm): 531 226 485 147 0 384 0 [pid=27245] vsize: 2124 Raw data (/proc/27249/stat): 27249 (minisat+_64-bit) R 27245 27245 5299 0 -1 0 7049 0 0 0 1938 30 0 0 25 0 1 0 1855450286 31727616 6692 4294967295 134512640 135094434 3221224432 3221223088 134561502 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27249/statm): 7746 6692 145 145 0 7601 0 [pid=27249] vsize: 30984 Current children cumulated CPU time (s) 19.7 Current children cumulated vsize (Kb) 33108 [startup+30.0053 s] Raw data (loadavg): 1.00 0.97 0.96 2/57 27249 Raw data (/proc/27245/stat): 27245 (minisat+_script) S 27244 27245 5299 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1855450281 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27245/statm): 531 226 485 147 0 384 0 [pid=27245] vsize: 2124 Raw data (/proc/27249/stat): 27249 (minisat+_64-bit) R 27245 27245 5299 0 -1 0 7085 0 0 0 2937 30 0 0 25 0 1 0 1855450286 31862784 6728 4294967295 134512640 135094434 3221224432 3221223044 134563089 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27249/statm): 7779 6728 145 145 0 7634 0 [pid=27249] vsize: 31116 Current children cumulated CPU time (s) 29.69 Current children cumulated vsize (Kb) 33240 [startup+40.0059 s] Raw data (loadavg): 1.00 0.97 0.96 2/57 27249 Raw data (/proc/27245/stat): 27245 (minisat+_script) S 27244 27245 5299 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1855450281 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27245/statm): 531 226 485 147 0 384 0 [pid=27245] vsize: 2124 Raw data (/proc/27249/stat): 27249 (minisat+_64-bit) R 27245 27245 5299 0 -1 0 7121 0 0 0 3936 31 0 0 25 0 1 0 1855450286 32002048 6764 4294967295 134512640 135094434 3221224432 3221223092 134553446 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27249/statm): 7813 6764 145 145 0 7668 0 [pid=27249] vsize: 31252 Current children cumulated CPU time (s) 39.69 Current children cumulated vsize (Kb) 33376 [startup+50.0066 s] Raw data (loadavg): 1.00 0.97 0.96 2/57 27249 Raw data (/proc/27245/stat): 27245 (minisat+_script) S 27244 27245 5299 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1855450281 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27245/statm): 531 226 485 147 0 384 0 [pid=27245] vsize: 2124 Raw data (/proc/27249/stat): 27249 (minisat+_64-bit) R 27245 27245 5299 0 -1 0 7152 0 0 0 4936 31 0 0 25 0 1 0 1855450286 32096256 6795 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27249/statm): 7836 6795 145 145 0 7691 0 [pid=27249] vsize: 31344 Current children cumulated CPU time (s) 49.69 Current children cumulated vsize (Kb) 33468 [startup+60.0072 s] Raw data (loadavg): 1.00 0.97 0.96 2/57 27249 Raw data (/proc/27245/stat): 27245 (minisat+_script) S 27244 27245 5299 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1855450281 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27245/statm): 531 226 485 147 0 384 0 [pid=27245] vsize: 2124 Raw data (/proc/27249/stat): 27249 (minisat+_64-bit) R 27245 27245 5299 0 -1 0 7174 0 0 0 5936 31 0 0 25 0 1 0 1855450286 32169984 6817 4294967295 134512640 135094434 3221224432 3221223044 134563055 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27249/statm): 7854 6817 145 145 0 7709 0 [pid=27249] vsize: 31416 Current children cumulated CPU time (s) 59.69 Current children cumulated vsize (Kb) 33540 [startup+70.0079 s] Raw data (loadavg): 1.00 0.97 0.96 2/57 27249 Raw data (/proc/27245/stat): 27245 (minisat+_script) S 27244 27245 5299 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1855450281 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27245/statm): 531 226 485 147 0 384 0 [pid=27245] vsize: 2124 Raw data (/proc/27249/stat): 27249 (minisat+_64-bit) R 27245 27245 5299 0 -1 0 7226 0 0 0 6935 32 0 0 25 0 1 0 1855450286 32415744 6869 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27249/statm): 7914 6869 145 145 0 7769 0 [pid=27249] vsize: 31656 Current children cumulated CPU time (s) 69.69 Current children cumulated vsize (Kb) 33780 [startup+80.0085 s] Raw data (loadavg): 1.00 0.97 0.96 2/57 27249 Raw data (/proc/27245/stat): 27245 (minisat+_script) S 27244 27245 5299 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1855450281 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27245/statm): 531 226 485 147 0 384 0 [pid=27245] vsize: 2124 Raw data (/proc/27249/stat): 27249 (minisat+_64-bit) R 27245 27245 5299 0 -1 0 7250 0 0 0 7935 32 0 0 25 0 1 0 1855450286 32501760 6893 4294967295 134512640 135094434 3221224432 3221223088 134558249 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27249/statm): 7935 6893 145 145 0 7790 0 [pid=27249] vsize: 31740 Current children cumulated CPU time (s) 79.69 Current children cumulated vsize (Kb) 33864 [startup+90.0091 s] Raw data (loadavg): 1.00 0.97 0.96 2/57 27249 Raw data (/proc/27245/stat): 27245 (minisat+_script) S 27244 27245 5299 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1855450281 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27245/statm): 531 226 485 147 0 384 0 [pid=27245] vsize: 2124 Raw data (/proc/27249/stat): 27249 (minisat+_64-bit) R 27245 27245 5299 0 -1 0 7277 0 0 0 8935 32 0 0 25 0 1 0 1855450286 32595968 6920 4294967295 134512640 135094434 3221224432 3221223056 134557604 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27249/statm): 7958 6920 145 145 0 7813 0 [pid=27249] vsize: 31832 Current children cumulated CPU time (s) 89.69 Current children cumulated vsize (Kb) 33956 [startup+100.01 s] Raw data (loadavg): 1.00 0.97 0.96 2/57 27249 Raw data (/proc/27245/stat): 27245 (minisat+_script) S 27244 27245 5299 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1855450281 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27245/statm): 531 226 485 147 0 384 0 [pid=27245] vsize: 2124 Raw data (/proc/27249/stat): 27249 (minisat+_64-bit) R 27245 27245 5299 0 -1 0 7307 0 0 0 9935 32 0 0 25 0 1 0 1855450286 32698368 6950 4294967295 134512640 135094434 3221224432 3221223072 134562104 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27249/statm): 7983 6950 145 145 0 7838 0 [pid=27249] vsize: 31932 Current children cumulated CPU time (s) 99.69 Current children cumulated vsize (Kb) 34056 [startup+110.011 s] Raw data (loadavg): 1.00 0.97 0.96 2/57 27249 Raw data (/proc/27245/stat): 27245 (minisat+_script) S 27244 27245 5299 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1855450281 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27245/statm): 531 226 485 147 0 384 0 [pid=27245] vsize: 2124 Raw data (/proc/27249/stat): 27249 (minisat+_64-bit) R 27245 27245 5299 0 -1 0 7332 0 0 0 10933 33 0 0 25 0 1 0 1855450286 32792576 6975 4294967295 134512640 135094434 3221224432 3221223092 134553446 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27249/statm): 8006 6975 145 145 0 7861 0 [pid=27249] vsize: 32024 Current children cumulated CPU time (s) 109.68 Current children cumulated vsize (Kb) 34148 [startup+120.012 s] Raw data (loadavg): 1.00 0.97 0.96 2/57 27249 Raw data (/proc/27245/stat): 27245 (minisat+_script) S 27244 27245 5299 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1855450281 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27245/statm): 531 226 485 147 0 384 0 [pid=27245] vsize: 2124 Raw data (/proc/27249/stat): 27249 (minisat+_64-bit) R 27245 27245 5299 0 -1 0 7365 0 0 0 11933 33 0 0 25 0 1 0 1855450286 32915456 7008 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27249/statm): 8036 7008 145 145 0 7891 0 [pid=27249] vsize: 32144 Current children cumulated CPU time (s) 119.68 Current children cumulated vsize (Kb) 34268 [startup+130.013 s] Raw data (loadavg): 1.00 0.97 0.96 2/57 27249 Raw data (/proc/27245/stat): 27245 (minisat+_script) S 27244 27245 5299 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1855450281 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27245/statm): 531 226 485 147 0 384 0 [pid=27245] vsize: 2124 Raw data (/proc/27249/stat): 27249 (minisat+_64-bit) R 27245 27245 5299 0 -1 0 7399 0 0 0 12932 34 0 0 25 0 1 0 1855450286 33042432 7042 4294967295 134512640 135094434 3221224432 3221223044 134563071 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27249/statm): 8067 7042 145 145 0 7922 0 [pid=27249] vsize: 32268 Current children cumulated CPU time (s) 129.68 Current children cumulated vsize (Kb) 34392 [startup+140.013 s] Raw data (loadavg): 1.00 0.97 0.96 2/57 27249 Raw data (/proc/27245/stat): 27245 (minisat+_script) S 27244 27245 5299 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1855450281 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27245/statm): 531 226 485 147 0 384 0 [pid=27245] vsize: 2124 Raw data (/proc/27249/stat): 27249 (minisat+_64-bit) R 27245 27245 5299 0 -1 0 7441 0 0 0 13932 34 0 0 25 0 1 0 1855450286 33337344 7084 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27249/statm): 8139 7084 145 145 0 7994 0 [pid=27249] vsize: 32556 Current children cumulated CPU time (s) 139.68 Current children cumulated vsize (Kb) 34680 [startup+150.014 s] Raw data (loadavg): 1.00 0.97 0.96 2/57 27249 Raw data (/proc/27245/stat): 27245 (minisat+_script) S 27244 27245 5299 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1855450281 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27245/statm): 531 226 485 147 0 384 0 [pid=27245] vsize: 2124 Raw data (/proc/27249/stat): 27249 (minisat+_64-bit) R 27245 27245 5299 0 -1 0 7473 0 0 0 14931 35 0 0 25 0 1 0 1855450286 33456128 7116 4294967295 134512640 135094434 3221224432 3221223056 134557574 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27249/statm): 8168 7116 145 145 0 8023 0 [pid=27249] vsize: 32672 Current children cumulated CPU time (s) 149.68 Current children cumulated vsize (Kb) 34796 [startup+160.015 s] Raw data (loadavg): 1.00 0.97 0.96 2/57 27249 Raw data (/proc/27245/stat): 27245 (minisat+_script) S 27244 27245 5299 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1855450281 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27245/statm): 531 226 485 147 0 384 0 [pid=27245] vsize: 2124 Raw data (/proc/27249/stat): 27249 (minisat+_64-bit) R 27245 27245 5299 0 -1 0 7517 0 0 0 15930 35 0 0 25 0 1 0 1855450286 33624064 7160 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27249/statm): 8209 7160 145 145 0 8064 0 [pid=27249] vsize: 32836 Current children cumulated CPU time (s) 159.67 Current children cumulated vsize (Kb) 34960 [startup+170.015 s] Raw data (loadavg): 1.00 0.97 0.96 2/57 27251 Raw data (/proc/27245/stat): 27245 (minisat+_script) S 27244 27245 5299 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1855450281 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27245/statm): 531 226 485 147 0 384 0 [pid=27245] vsize: 2124 Raw data (/proc/27249/stat): 27249 (minisat+_64-bit) R 27245 27245 5299 0 -1 0 7558 0 0 0 16930 36 0 0 25 0 1 0 1855450286 33771520 7201 4294967295 134512640 135094434 3221224432 3221223088 134558221 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27249/statm): 8245 7201 145 145 0 8100 0 [pid=27249] vsize: 32980 Current children cumulated CPU time (s) 169.68 Current children cumulated vsize (Kb) 35104 [startup+180.016 s] Raw data (loadavg): 1.00 0.97 0.96 2/57 27251 Raw data (/proc/27245/stat): 27245 (minisat+_script) S 27244 27245 5299 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1855450281 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27245/statm): 531 226 485 147 0 384 0 [pid=27245] vsize: 2124 Raw data (/proc/27249/stat): 27249 (minisat+_64-bit) R 27245 27245 5299 0 -1 0 7594 0 0 0 17930 36 0 0 25 0 1 0 1855450286 33910784 7237 4294967295 134512640 135094434 3221224432 3221223120 134554746 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27249/statm): 8279 7237 145 145 0 8134 0 [pid=27249] vsize: 33116 Current children cumulated CPU time (s) 179.68 Current children cumulated vsize (Kb) 35240 [startup+190.017 s] Raw data (loadavg): 1.00 0.97 0.96 2/57 27251 Raw data (/proc/27245/stat): 27245 (minisat+_script) S 27244 27245 5299 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1855450281 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27245/statm): 531 226 485 147 0 384 0 [pid=27245] vsize: 2124 Raw data (/proc/27249/stat): 27249 (minisat+_64-bit) R 27245 27245 5299 0 -1 0 7660 0 0 0 18929 36 0 0 25 0 1 0 1855450286 34164736 7303 4294967295 134512640 135094434 3221224432 3221223120 134554760 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27249/statm): 8341 7303 145 145 0 8196 0 [pid=27249] vsize: 33364 Current children cumulated CPU time (s) 189.67 Current children cumulated vsize (Kb) 35488 [startup+200.016 s] Raw data (loadavg): 1.00 0.97 0.96 2/57 27251 Raw data (/proc/27245/stat): 27245 (minisat+_script) S 27244 27245 5299 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1855450281 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27245/statm): 531 226 485 147 0 384 0 [pid=27245] vsize: 2124 Raw data (/proc/27249/stat): 27249 (minisat+_64-bit) R 27245 27245 5299 0 -1 0 7694 0 0 0 19928 37 0 0 25 0 1 0 1855450286 34295808 7337 4294967295 134512640 135094434 3221224432 3221223044 134563049 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27249/statm): 8373 7337 145 145 0 8228 0 [pid=27249] vsize: 33492 Current children cumulated CPU time (s) 199.67 Current children cumulated vsize (Kb) 35616 [startup+210.018 s] Raw data (loadavg): 1.00 0.97 0.96 2/57 27251 Raw data (/proc/27245/stat): 27245 (minisat+_script) S 27244 27245 5299 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1855450281 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27245/statm): 531 226 485 147 0 384 0 [pid=27245] vsize: 2124 Raw data (/proc/27249/stat): 27249 (minisat+_64-bit) R 27245 27245 5299 0 -1 0 7736 0 0 0 20928 37 0 0 25 0 1 0 1855450286 34459648 7379 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27249/statm): 8413 7379 145 145 0 8268 0 [pid=27249] vsize: 33652 Current children cumulated CPU time (s) 209.67 Current children cumulated vsize (Kb) 35776 [startup+220.018 s] Raw data (loadavg): 1.00 0.97 0.96 2/57 27251 Raw data (/proc/27245/stat): 27245 (minisat+_script) S 27244 27245 5299 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1855450281 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27245/statm): 531 226 485 147 0 384 0 [pid=27245] vsize: 2124 Raw data (/proc/27249/stat): 27249 (minisat+_64-bit) R 27245 27245 5299 0 -1 0 7827 0 0 0 21927 37 0 0 25 0 1 0 1855450286 34811904 7470 4294967295 134512640 135094434 3221224432 3221223088 134558016 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27249/statm): 8499 7470 145 145 0 8354 0 [pid=27249] vsize: 33996 Current children cumulated CPU time (s) 219.66 Current children cumulated vsize (Kb) 36120 [startup+230.018 s] Raw data (loadavg): 1.00 0.97 0.96 2/57 27251 Raw data (/proc/27245/stat): 27245 (minisat+_script) S 27244 27245 5299 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1855450281 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27245/statm): 531 226 485 147 0 384 0 [pid=27245] vsize: 2124 Raw data (/proc/27249/stat): 27249 (minisat+_64-bit) R 27245 27245 5299 0 -1 0 8207 0 0 0 22921 39 0 0 25 0 1 0 1855450286 36577280 7850 4294967295 134512640 135094434 3221224432 3221223088 134557996 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27249/statm): 8930 7850 145 145 0 8785 0 [pid=27249] vsize: 35720 Current children cumulated CPU time (s) 229.62 Current children cumulated vsize (Kb) 37844 [startup+240.019 s] Raw data (loadavg): 1.00 0.97 0.96 2/57 27251 Raw data (/proc/27245/stat): 27245 (minisat+_script) S 27244 27245 5299 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1855450281 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27245/statm): 531 226 485 147 0 384 0 [pid=27245] vsize: 2124 Raw data (/proc/27249/stat): 27249 (minisat+_64-bit) R 27245 27245 5299 0 -1 0 8712 0 0 0 23913 42 0 0 25 0 1 0 1855450286 38608896 8355 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27249/statm): 9426 8355 145 145 0 9281 0 [pid=27249] vsize: 37704 Current children cumulated CPU time (s) 239.57 Current children cumulated vsize (Kb) 39828 [startup+250.019 s] Raw data (loadavg): 1.00 0.97 0.96 2/57 27251 Raw data (/proc/27245/stat): 27245 (minisat+_script) S 27244 27245 5299 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1855450281 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27245/statm): 531 226 485 147 0 384 0 [pid=27245] vsize: 2124 Raw data (/proc/27249/stat): 27249 (minisat+_64-bit) R 27245 27245 5299 0 -1 0 8922 0 0 0 24910 44 0 0 25 0 1 0 1855450286 39456768 8565 4294967295 134512640 135094434 3221224432 3221223044 134563055 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27249/statm): 9633 8565 145 145 0 9488 0 [pid=27249] vsize: 38532 Current children cumulated CPU time (s) 249.56 Current children cumulated vsize (Kb) 40656 [startup+260.02 s] Raw data (loadavg): 1.00 0.97 0.96 2/57 27251 Raw data (/proc/27245/stat): 27245 (minisat+_script) S 27244 27245 5299 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1855450281 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27245/statm): 531 226 485 147 0 384 0 [pid=27245] vsize: 2124 Raw data (/proc/27249/stat): 27249 (minisat+_64-bit) R 27245 27245 5299 0 -1 0 9067 0 0 0 25908 44 0 0 25 0 1 0 1855450286 40034304 8710 4294967295 134512640 135094434 3221224432 3221223072 134562104 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27249/statm): 9774 8710 145 145 0 9629 0 [pid=27249] vsize: 39096 Current children cumulated CPU time (s) 259.54 Current children cumulated vsize (Kb) 41220 [startup+270.021 s] Raw data (loadavg): 1.00 0.97 0.96 2/57 27251 Raw data (/proc/27245/stat): 27245 (minisat+_script) S 27244 27245 5299 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1855450281 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27245/statm): 531 226 485 147 0 384 0 [pid=27245] vsize: 2124 Raw data (/proc/27249/stat): 27249 (minisat+_64-bit) R 27245 27245 5299 0 -1 0 9144 0 0 0 26905 45 0 0 25 0 1 0 1855450286 40333312 8787 4294967295 134512640 135094434 3221224432 3221223044 134563083 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27249/statm): 9847 8787 145 145 0 9702 0 [pid=27249] vsize: 39388 Current children cumulated CPU time (s) 269.52 Current children cumulated vsize (Kb) 41512 [startup+280.021 s] Raw data (loadavg): 1.00 0.97 0.96 2/57 27251 Raw data (/proc/27245/stat): 27245 (minisat+_script) S 27244 27245 5299 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1855450281 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27245/statm): 531 226 485 147 0 384 0 [pid=27245] vsize: 2124 Raw data (/proc/27249/stat): 27249 (minisat+_64-bit) R 27245 27245 5299 0 -1 0 9270 0 0 0 27903 46 0 0 25 0 1 0 1855450286 40837120 8913 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27249/statm): 9970 8913 145 145 0 9825 0 [pid=27249] vsize: 39880 Current children cumulated CPU time (s) 279.51 Current children cumulated vsize (Kb) 42004 [startup+290.022 s] Raw data (loadavg): 1.00 0.97 0.96 2/57 27251 Raw data (/proc/27245/stat): 27245 (minisat+_script) S 27244 27245 5299 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1855450281 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27245/statm): 531 226 485 147 0 384 0 [pid=27245] vsize: 2124 Raw data (/proc/27249/stat): 27249 (minisat+_64-bit) R 27245 27245 5299 0 -1 0 9490 0 0 0 28898 48 0 0 25 0 1 0 1855450286 41721856 9133 4294967295 134512640 135094434 3221224432 3221223088 134558159 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27249/statm): 10186 9133 145 145 0 10041 0 [pid=27249] vsize: 40744 Current children cumulated CPU time (s) 289.48 Current children cumulated vsize (Kb) 42868 [startup+300.023 s] Raw data (loadavg): 1.00 0.97 0.96 2/57 27251 Raw data (/proc/27245/stat): 27245 (minisat+_script) S 27244 27245 5299 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1855450281 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27245/statm): 531 226 485 147 0 384 0 [pid=27245] vsize: 2124 Raw data (/proc/27249/stat): 27249 (minisat+_64-bit) R 27245 27245 5299 0 -1 0 9588 0 0 0 29897 49 0 0 25 0 1 0 1855450286 42110976 9231 4294967295 134512640 135094434 3221224432 3221223088 134557945 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27249/statm): 10281 9231 145 145 0 10136 0 [pid=27249] vsize: 41124 Current children cumulated CPU time (s) 299.48 Current children cumulated vsize (Kb) 43248 [startup+310.023 s] Raw data (loadavg): 1.00 0.97 0.96 2/57 27251 Raw data (/proc/27245/stat): 27245 (minisat+_script) S 27244 27245 5299 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1855450281 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27245/statm): 531 226 485 147 0 384 0 [pid=27245] vsize: 2124 Raw data (/proc/27249/stat): 27249 (minisat+_64-bit) R 27245 27245 5299 0 -1 0 9714 0 0 0 30895 49 0 0 25 0 1 0 1855450286 42610688 9357 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27249/statm): 10403 9357 145 145 0 10258 0 [pid=27249] vsize: 41612 Current children cumulated CPU time (s) 309.46 Current children cumulated vsize (Kb) 43736 [startup+320.024 s] Raw data (loadavg): 1.00 0.97 0.96 2/57 27251 Raw data (/proc/27245/stat): 27245 (minisat+_script) S 27244 27245 5299 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1855450281 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27245/statm): 531 226 485 147 0 384 0 [pid=27245] vsize: 2124 Raw data (/proc/27249/stat): 27249 (minisat+_64-bit) R 27245 27245 5299 0 -1 0 10011 0 0 0 31889 52 0 0 25 0 1 0 1855450286 43798528 9654 4294967295 134512640 135094434 3221224432 3221223072 134562098 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27249/statm): 10693 9654 145 145 0 10548 0 [pid=27249] vsize: 42772 Current children cumulated CPU time (s) 319.43 Current children cumulated vsize (Kb) 44896 [startup+330.024 s] Raw data (loadavg): 1.00 0.97 0.96 2/57 27251 Raw data (/proc/27245/stat): 27245 (minisat+_script) S 27244 27245 5299 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1855450281 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27245/statm): 531 226 485 147 0 384 0 [pid=27245] vsize: 2124 Raw data (/proc/27249/stat): 27249 (minisat+_64-bit) R 27245 27245 5299 0 -1 0 10140 0 0 0 32886 53 0 0 25 0 1 0 1855450286 44318720 9783 4294967295 134512640 135094434 3221224432 3221223072 134558048 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27249/statm): 10820 9783 145 145 0 10675 0 [pid=27249] vsize: 43280 Current children cumulated CPU time (s) 329.41 Current children cumulated vsize (Kb) 45404 [startup+340.025 s] Raw data (loadavg): 1.00 0.97 0.96 2/57 27251 Raw data (/proc/27245/stat): 27245 (minisat+_script) S 27244 27245 5299 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1855450281 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27245/statm): 531 226 485 147 0 384 0 [pid=27245] vsize: 2124 Raw data (/proc/27249/stat): 27249 (minisat+_64-bit) R 27245 27245 5299 0 -1 0 10282 0 0 0 33883 55 0 0 25 0 1 0 1855450286 45408256 9925 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27249/statm): 11086 9925 145 145 0 10941 0 [pid=27249] vsize: 44344 Current children cumulated CPU time (s) 339.4 Current children cumulated vsize (Kb) 46468 [startup+350.025 s] Raw data (loadavg): 1.00 0.97 0.96 2/57 27251 Raw data (/proc/27245/stat): 27245 (minisat+_script) S 27244 27245 5299 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1855450281 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27245/statm): 531 226 485 147 0 384 0 [pid=27245] vsize: 2124 Raw data (/proc/27249/stat): 27249 (minisat+_64-bit) R 27245 27245 5299 0 -1 0 10422 0 0 0 34881 56 0 0 25 0 1 0 1855450286 45965312 10065 4294967295 134512640 135094434 3221224432 3221223088 134558405 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27249/statm): 11222 10065 145 145 0 11077 0 [pid=27249] vsize: 44888 Current children cumulated CPU time (s) 349.39 Current children cumulated vsize (Kb) 47012 [startup+360.025 s] Raw data (loadavg): 1.00 0.97 0.96 2/57 27251 Raw data (/proc/27245/stat): 27245 (minisat+_script) S 27244 27245 5299 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1855450281 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27245/statm): 531 226 485 147 0 384 0 [pid=27245] vsize: 2124 Raw data (/proc/27249/stat): 27249 (minisat+_64-bit) R 27245 27245 5299 0 -1 0 10621 0 0 0 35877 58 0 0 25 0 1 0 1855450286 46800896 10264 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27249/statm): 11426 10264 145 145 0 11281 0 [pid=27249] vsize: 45704 Current children cumulated CPU time (s) 359.37 Current children cumulated vsize (Kb) 47828 [startup+370.026 s] Raw data (loadavg): 1.00 0.97 0.96 2/57 27251 Raw data (/proc/27245/stat): 27245 (minisat+_script) S 27244 27245 5299 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1855450281 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27245/statm): 531 226 485 147 0 384 0 [pid=27245] vsize: 2124 Raw data (/proc/27249/stat): 27249 (minisat+_64-bit) R 27245 27245 5299 0 -1 0 10699 0 0 0 36876 58 0 0 25 0 1 0 1855450286 47128576 10342 4294967295 134512640 135094434 3221224432 3221223044 134563071 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27249/statm): 11506 10342 145 145 0 11361 0 [pid=27249] vsize: 46024 Current children cumulated CPU time (s) 369.36 Current children cumulated vsize (Kb) 48148 [startup+380.026 s] Raw data (loadavg): 1.00 0.97 0.96 2/57 27251 Raw data (/proc/27245/stat): 27245 (minisat+_script) S 27244 27245 5299 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1855450281 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27245/statm): 531 226 485 147 0 384 0 [pid=27245] vsize: 2124 Raw data (/proc/27249/stat): 27249 (minisat+_64-bit) R 27245 27245 5299 0 -1 0 10831 0 0 0 37874 60 0 0 25 0 1 0 1855450286 47669248 10474 4294967295 134512640 135094434 3221224432 3221223092 134553446 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27249/statm): 11638 10474 145 145 0 11493 0 [pid=27249] vsize: 46552 Current children cumulated CPU time (s) 379.36 Current children cumulated vsize (Kb) 48676 [startup+390.029 s] Raw data (loadavg): 1.00 0.97 0.96 2/57 27251 Raw data (/proc/27245/stat): 27245 (minisat+_script) S 27244 27245 5299 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1855450281 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27245/statm): 531 226 485 147 0 384 0 [pid=27245] vsize: 2124 Raw data (/proc/27249/stat): 27249 (minisat+_64-bit) R 27245 27245 5299 0 -1 0 10973 0 0 0 38871 62 0 0 25 0 1 0 1855450286 48234496 10616 4294967295 134512640 135094434 3221224432 3221223088 134557884 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27249/statm): 11776 10616 145 145 0 11631 0 [pid=27249] vsize: 47104 Current children cumulated CPU time (s) 389.35 Current children cumulated vsize (Kb) 49228 [startup+400.03 s] Raw data (loadavg): 1.00 0.97 0.96 2/57 27251 Raw data (/proc/27245/stat): 27245 (minisat+_script) S 27244 27245 5299 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1855450281 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27245/statm): 531 226 485 147 0 384 0 [pid=27245] vsize: 2124 Raw data (/proc/27249/stat): 27249 (minisat+_64-bit) R 27245 27245 5299 0 -1 0 11079 0 0 0 39869 63 0 0 25 0 1 0 1855450286 48664576 10722 4294967295 134512640 135094434 3221224432 3221223056 134557685 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27249/statm): 11881 10722 145 145 0 11736 0 [pid=27249] vsize: 47524 Current children cumulated CPU time (s) 399.34 Current children cumulated vsize (Kb) 49648 [startup+410.031 s] Raw data (loadavg): 1.00 0.97 0.96 2/57 27251 Raw data (/proc/27245/stat): 27245 (minisat+_script) S 27244 27245 5299 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1855450281 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27245/statm): 531 226 485 147 0 384 0 [pid=27245] vsize: 2124 Raw data (/proc/27249/stat): 27249 (minisat+_64-bit) R 27245 27245 5299 0 -1 0 11247 0 0 0 40866 65 0 0 25 0 1 0 1855450286 49336320 10890 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27249/statm): 12045 10890 145 145 0 11900 0 [pid=27249] vsize: 48180 Current children cumulated CPU time (s) 409.33 Current children cumulated vsize (Kb) 50304 [startup+420.031 s] Raw data (loadavg): 1.00 0.97 0.96 2/57 27251 Raw data (/proc/27245/stat): 27245 (minisat+_script) S 27244 27245 5299 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1855450281 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27245/statm): 531 226 485 147 0 384 0 [pid=27245] vsize: 2124 Raw data (/proc/27249/stat): 27249 (minisat+_64-bit) R 27245 27245 5299 0 -1 0 11402 0 0 0 41863 67 0 0 25 0 1 0 1855450286 49954816 11045 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27249/statm): 12196 11045 145 145 0 12051 0 [pid=27249] vsize: 48784 Current children cumulated CPU time (s) 419.32 Current children cumulated vsize (Kb) 50908 [startup+430.032 s] Raw data (loadavg): 1.00 0.97 0.96 2/57 27251 Raw data (/proc/27245/stat): 27245 (minisat+_script) S 27244 27245 5299 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1855450281 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27245/statm): 531 226 485 147 0 384 0 [pid=27245] vsize: 2124 Raw data (/proc/27249/stat): 27249 (minisat+_64-bit) R 27245 27245 5299 0 -1 0 11485 0 0 0 42861 68 0 0 25 0 1 0 1855450286 50282496 11128 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27249/statm): 12276 11128 145 145 0 12131 0 [pid=27249] vsize: 49104 Current children cumulated CPU time (s) 429.31 Current children cumulated vsize (Kb) 51228 [startup+440.033 s] Raw data (loadavg): 1.00 0.97 0.96 2/57 27251 Raw data (/proc/27245/stat): 27245 (minisat+_script) S 27244 27245 5299 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1855450281 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27245/statm): 531 226 485 147 0 384 0 [pid=27245] vsize: 2124 Raw data (/proc/27249/stat): 27249 (minisat+_64-bit) R 27245 27245 5299 0 -1 0 11547 0 0 0 43861 68 0 0 25 0 1 0 1855450286 50548736 11190 4294967295 134512640 135094434 3221224432 3221223120 134554709 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27249/statm): 12341 11190 145 145 0 12196 0 [pid=27249] vsize: 49364 Current children cumulated CPU time (s) 439.31 Current children cumulated vsize (Kb) 51488 [startup+450.033 s] Raw data (loadavg): 1.00 0.97 0.96 2/57 27251 Raw data (/proc/27245/stat): 27245 (minisat+_script) S 27244 27245 5299 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1855450281 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27245/statm): 531 226 485 147 0 384 0 [pid=27245] vsize: 2124 Raw data (/proc/27249/stat): 27249 (minisat+_64-bit) R 27245 27245 5299 0 -1 0 11629 0 0 0 44860 69 0 0 25 0 1 0 1855450286 50876416 11272 4294967295 134512640 135094434 3221224432 3221223084 134558255 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27249/statm): 12421 11272 145 145 0 12276 0 [pid=27249] vsize: 49684 Current children cumulated CPU time (s) 449.31 Current children cumulated vsize (Kb) 51808 [startup+460.034 s] Raw data (loadavg): 1.00 0.97 0.96 2/57 27251 Raw data (/proc/27245/stat): 27245 (minisat+_script) S 27244 27245 5299 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1855450281 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27245/statm): 531 226 485 147 0 384 0 [pid=27245] vsize: 2124 Raw data (/proc/27249/stat): 27249 (minisat+_64-bit) R 27245 27245 5299 0 -1 0 11709 0 0 0 45859 69 0 0 25 0 1 0 1855450286 51187712 11352 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27249/statm): 12497 11352 145 145 0 12352 0 [pid=27249] vsize: 49988 Current children cumulated CPU time (s) 459.3 Current children cumulated vsize (Kb) 52112 [startup+470.034 s] Raw data (loadavg): 1.00 0.97 0.96 2/57 27251 Raw data (/proc/27245/stat): 27245 (minisat+_script) S 27244 27245 5299 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1855450281 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27245/statm): 531 226 485 147 0 384 0 [pid=27245] vsize: 2124 Raw data (/proc/27249/stat): 27249 (minisat+_64-bit) R 27245 27245 5299 0 -1 0 11841 0 0 0 46856 71 0 0 25 0 1 0 1855450286 51703808 11484 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27249/statm): 12623 11484 145 145 0 12478 0 [pid=27249] vsize: 50492 Current children cumulated CPU time (s) 469.29 Current children cumulated vsize (Kb) 52616 [startup+480.035 s] Raw data (loadavg): 1.00 0.97 0.96 2/57 27251 Raw data (/proc/27245/stat): 27245 (minisat+_script) S 27244 27245 5299 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1855450281 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27245/statm): 531 226 485 147 0 384 0 [pid=27245] vsize: 2124 Raw data (/proc/27249/stat): 27249 (minisat+_64-bit) R 27245 27245 5299 0 -1 0 11954 0 0 0 47854 72 0 0 25 0 1 0 1855450286 52154368 11597 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27249/statm): 12733 11597 145 145 0 12588 0 [pid=27249] vsize: 50932 Current children cumulated CPU time (s) 479.28 Current children cumulated vsize (Kb) 53056 [startup+490.036 s] Raw data (loadavg): 1.00 0.97 0.96 2/57 27251 Raw data (/proc/27245/stat): 27245 (minisat+_script) S 27244 27245 5299 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1855450281 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27245/statm): 531 226 485 147 0 384 0 [pid=27245] vsize: 2124 Raw data (/proc/27249/stat): 27249 (minisat+_64-bit) R 27245 27245 5299 0 -1 0 12119 0 0 0 48852 73 0 0 25 0 1 0 1855450286 52801536 11762 4294967295 134512640 135094434 3221224432 3221223088 134558402 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27249/statm): 12891 11762 145 145 0 12746 0 [pid=27249] vsize: 51564 Current children cumulated CPU time (s) 489.27 Current children cumulated vsize (Kb) 53688 [startup+500.035 s] Raw data (loadavg): 1.00 0.97 0.96 2/57 27251 Raw data (/proc/27245/stat): 27245 (minisat+_script) S 27244 27245 5299 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1855450281 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27245/statm): 531 226 485 147 0 384 0 [pid=27245] vsize: 2124 Raw data (/proc/27249/stat): 27249 (minisat+_64-bit) R 27245 27245 5299 0 -1 0 12245 0 0 0 49849 75 0 0 25 0 1 0 1855450286 53329920 11888 4294967295 134512640 135094434 3221224432 3221223044 134563055 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27249/statm): 13020 11888 145 145 0 12875 0 [pid=27249] vsize: 52080 Current children cumulated CPU time (s) 499.26 Current children cumulated vsize (Kb) 54204 [startup+510.037 s] Raw data (loadavg): 1.00 0.97 0.96 2/57 27251 Raw data (/proc/27245/stat): 27245 (minisat+_script) S 27244 27245 5299 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1855450281 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27245/statm): 531 226 485 147 0 384 0 [pid=27245] vsize: 2124 Raw data (/proc/27249/stat): 27249 (minisat+_64-bit) R 27245 27245 5299 0 -1 0 12336 0 0 0 50847 76 0 0 25 0 1 0 1855450286 53686272 11979 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27249/statm): 13107 11979 145 145 0 12962 0 [pid=27249] vsize: 52428 Current children cumulated CPU time (s) 509.25 Current children cumulated vsize (Kb) 54552 [startup+520.038 s] Raw data (loadavg): 1.00 0.97 0.96 2/57 27251 Raw data (/proc/27245/stat): 27245 (minisat+_script) S 27244 27245 5299 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1855450281 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27245/statm): 531 226 485 147 0 384 0 [pid=27245] vsize: 2124 Raw data (/proc/27249/stat): 27249 (minisat+_64-bit) R 27245 27245 5299 0 -1 0 12434 0 0 0 51844 76 0 0 25 0 1 0 1855450286 54067200 12077 4294967295 134512640 135094434 3221224432 3221223088 134558235 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27249/statm): 13200 12077 145 145 0 13055 0 [pid=27249] vsize: 52800 Current children cumulated CPU time (s) 519.22 Current children cumulated vsize (Kb) 54924 [startup+530.037 s] Raw data (loadavg): 1.00 0.97 0.96 2/57 27251 Raw data (/proc/27245/stat): 27245 (minisat+_script) S 27244 27245 5299 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1855450281 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27245/statm): 531 226 485 147 0 384 0 [pid=27245] vsize: 2124 Raw data (/proc/27249/stat): 27249 (minisat+_64-bit) R 27245 27245 5299 0 -1 0 12501 0 0 0 52842 78 0 0 25 0 1 0 1855450286 54333440 12144 4294967295 134512640 135094434 3221224432 3221223044 134563083 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27249/statm): 13265 12144 145 145 0 13120 0 [pid=27249] vsize: 53060 Current children cumulated CPU time (s) 529.22 Current children cumulated vsize (Kb) 55184 [startup+540.038 s] Raw data (loadavg): 1.00 0.97 0.96 2/57 27251 Raw data (/proc/27245/stat): 27245 (minisat+_script) S 27244 27245 5299 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1855450281 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27245/statm): 531 226 485 147 0 384 0 [pid=27245] vsize: 2124 Raw data (/proc/27249/stat): 27249 (minisat+_64-bit) R 27245 27245 5299 0 -1 0 12563 0 0 0 53842 78 0 0 25 0 1 0 1855450286 54571008 12206 4294967295 134512640 135094434 3221224432 3221223044 134563049 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27249/statm): 13323 12206 145 145 0 13178 0 [pid=27249] vsize: 53292 Current children cumulated CPU time (s) 539.22 Current children cumulated vsize (Kb) 55416 [startup+550.039 s] Raw data (loadavg): 1.00 0.97 0.96 2/57 27251 Raw data (/proc/27245/stat): 27245 (minisat+_script) S 27244 27245 5299 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1855450281 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27245/statm): 531 226 485 147 0 384 0 [pid=27245] vsize: 2124 Raw data (/proc/27249/stat): 27249 (minisat+_64-bit) R 27245 27245 5299 0 -1 0 12665 0 0 0 54839 79 0 0 25 0 1 0 1855450286 54976512 12308 4294967295 134512640 135094434 3221224432 3221223088 134557984 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27249/statm): 13422 12308 145 145 0 13277 0 [pid=27249] vsize: 53688 Current children cumulated CPU time (s) 549.2 Current children cumulated vsize (Kb) 55812 [startup+560.039 s] Raw data (loadavg): 1.00 0.97 0.96 2/57 27251 Raw data (/proc/27245/stat): 27245 (minisat+_script) S 27244 27245 5299 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1855450281 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27245/statm): 531 226 485 147 0 384 0 [pid=27245] vsize: 2124 Raw data (/proc/27249/stat): 27249 (minisat+_64-bit) R 27245 27245 5299 0 -1 0 12718 0 0 0 55838 79 0 0 25 0 1 0 1855450286 55181312 12361 4294967295 134512640 135094434 3221224432 3221223044 134563069 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27249/statm): 13472 12361 145 145 0 13327 0 [pid=27249] vsize: 53888 Current children cumulated CPU time (s) 559.19 Current children cumulated vsize (Kb) 56012 [startup+570.04 s] Raw data (loadavg): 1.00 0.97 0.96 2/57 27251 Raw data (/proc/27245/stat): 27245 (minisat+_script) S 27244 27245 5299 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1855450281 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27245/statm): 531 226 485 147 0 384 0 [pid=27245] vsize: 2124 Raw data (/proc/27249/stat): 27249 (minisat+_64-bit) R 27245 27245 5299 0 -1 0 12792 0 0 0 56837 80 0 0 25 0 1 0 1855450286 55472128 12435 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27249/statm): 13543 12435 145 145 0 13398 0 [pid=27249] vsize: 54172 Current children cumulated CPU time (s) 569.19 Current children cumulated vsize (Kb) 56296 [startup+580.04 s] Raw data (loadavg): 1.00 0.97 0.96 2/57 27251 Raw data (/proc/27245/stat): 27245 (minisat+_script) S 27244 27245 5299 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1855450281 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27245/statm): 531 226 485 147 0 384 0 [pid=27245] vsize: 2124 Raw data (/proc/27249/stat): 27249 (minisat+_64-bit) R 27245 27245 5299 0 -1 0 12933 0 0 0 57833 81 0 0 25 0 1 0 1855450286 56037376 12576 4294967295 134512640 135094434 3221224432 3221223044 134563163 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27249/statm): 13681 12576 145 145 0 13536 0 [pid=27249] vsize: 54724 Current children cumulated CPU time (s) 579.16 Current children cumulated vsize (Kb) 56848 [startup+590.041 s] Raw data (loadavg): 1.00 0.97 0.96 2/57 27251 Raw data (/proc/27245/stat): 27245 (minisat+_script) S 27244 27245 5299 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1855450281 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27245/statm): 531 226 485 147 0 384 0 [pid=27245] vsize: 2124 Raw data (/proc/27249/stat): 27249 (minisat+_64-bit) R 27245 27245 5299 0 -1 0 13054 0 0 0 58832 83 0 0 25 0 1 0 1855450286 56516608 12697 4294967295 134512640 135094434 3221224432 3221223088 134558221 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27249/statm): 13798 12697 145 145 0 13653 0 [pid=27249] vsize: 55192 Current children cumulated CPU time (s) 589.17 Current children cumulated vsize (Kb) 57316 [startup+600.042 s] Raw data (loadavg): 1.00 0.97 0.96 2/57 27251 Raw data (/proc/27245/stat): 27245 (minisat+_script) S 27244 27245 5299 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1855450281 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27245/statm): 531 226 485 147 0 384 0 [pid=27245] vsize: 2124 Raw data (/proc/27249/stat): 27249 (minisat+_64-bit) R 27245 27245 5299 0 -1 0 13223 0 0 0 59829 84 0 0 25 0 1 0 1855450286 57167872 12866 4294967295 134512640 135094434 3221224432 3221223056 134557737 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27249/statm): 13957 12866 145 145 0 13812 0 [pid=27249] vsize: 55828 Current children cumulated CPU time (s) 599.15 Current children cumulated vsize (Kb) 57952 [startup+610.043 s] Raw data (loadavg): 1.00 0.97 0.96 2/57 27251 Raw data (/proc/27245/stat): 27245 (minisat+_script) S 27244 27245 5299 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1855450281 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27245/statm): 531 226 485 147 0 384 0 [pid=27245] vsize: 2124 Raw data (/proc/27249/stat): 27249 (minisat+_64-bit) R 27245 27245 5299 0 -1 0 13340 0 0 0 60827 85 0 0 25 0 1 0 1855450286 57651200 12983 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27249/statm): 14075 12983 145 145 0 13930 0 [pid=27249] vsize: 56300 Current children cumulated CPU time (s) 609.14 Current children cumulated vsize (Kb) 58424 [startup+620.044 s] Raw data (loadavg): 1.00 0.97 0.96 2/57 27251 Raw data (/proc/27245/stat): 27245 (minisat+_script) S 27244 27245 5299 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1855450281 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27245/statm): 531 226 485 147 0 384 0 [pid=27245] vsize: 2124 Raw data (/proc/27249/stat): 27249 (minisat+_64-bit) R 27245 27245 5299 0 -1 0 13445 0 0 0 61826 86 0 0 25 0 1 0 1855450286 58060800 13088 4294967295 134512640 135094434 3221224432 3221223056 134557596 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27249/statm): 14175 13088 145 145 0 14030 0 [pid=27249] vsize: 56700 Current children cumulated CPU time (s) 619.14 Current children cumulated vsize (Kb) 58824 [startup+630.045 s] Raw data (loadavg): 1.00 0.97 0.96 2/57 27251 Raw data (/proc/27245/stat): 27245 (minisat+_script) S 27244 27245 5299 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1855450281 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27245/statm): 531 226 485 147 0 384 0 [pid=27245] vsize: 2124 Raw data (/proc/27249/stat): 27249 (minisat+_64-bit) R 27245 27245 5299 0 -1 0 13550 0 0 0 62825 86 0 0 25 0 1 0 1855450286 58466304 13193 4294967295 134512640 135094434 3221224432 3221223044 134563083 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27249/statm): 14274 13193 145 145 0 14129 0 [pid=27249] vsize: 57096 Current children cumulated CPU time (s) 629.13 Current children cumulated vsize (Kb) 59220 [startup+640.045 s] Raw data (loadavg): 1.00 0.97 0.96 2/57 27251 Raw data (/proc/27245/stat): 27245 (minisat+_script) S 27244 27245 5299 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1855450281 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27245/statm): 531 226 485 147 0 384 0 [pid=27245] vsize: 2124 Raw data (/proc/27249/stat): 27249 (minisat+_64-bit) R 27245 27245 5299 0 -1 0 13691 0 0 0 63822 87 0 0 25 0 1 0 1855450286 59031552 13334 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27249/statm): 14412 13334 145 145 0 14267 0 [pid=27249] vsize: 57648 Current children cumulated CPU time (s) 639.11 Current children cumulated vsize (Kb) 59772 [startup+650.046 s] Raw data (loadavg): 1.00 0.97 0.96 2/57 27251 Raw data (/proc/27245/stat): 27245 (minisat+_script) S 27244 27245 5299 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1855450281 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27245/statm): 531 226 485 147 0 384 0 [pid=27245] vsize: 2124 Raw data (/proc/27249/stat): 27249 (minisat+_64-bit) R 27245 27245 5299 0 -1 0 13783 0 0 0 64821 87 0 0 25 0 1 0 1855450286 59404288 13426 4294967295 134512640 135094434 3221224432 3221223088 134557890 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27249/statm): 14503 13426 145 145 0 14358 0 [pid=27249] vsize: 58012 Current children cumulated CPU time (s) 649.1 Current children cumulated vsize (Kb) 60136 [startup+660.047 s] Raw data (loadavg): 1.00 0.97 0.96 2/57 27251 Raw data (/proc/27245/stat): 27245 (minisat+_script) S 27244 27245 5299 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1855450281 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27245/statm): 531 226 485 147 0 384 0 [pid=27245] vsize: 2124 Raw data (/proc/27249/stat): 27249 (minisat+_64-bit) R 27245 27245 5299 0 -1 0 13871 0 0 0 65819 89 0 0 25 0 1 0 1855450286 59748352 13514 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27249/statm): 14587 13514 145 145 0 14442 0 [pid=27249] vsize: 58348 Current children cumulated CPU time (s) 659.1 Current children cumulated vsize (Kb) 60472 [startup+670.047 s] Raw data (loadavg): 1.00 0.97 0.96 2/57 27251 Raw data (/proc/27245/stat): 27245 (minisat+_script) S 27244 27245 5299 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1855450281 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27245/statm): 531 226 485 147 0 384 0 [pid=27245] vsize: 2124 Raw data (/proc/27249/stat): 27249 (minisat+_64-bit) R 27245 27245 5299 0 -1 0 13959 0 0 0 66817 89 0 0 25 0 1 0 1855450286 60092416 13602 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27249/statm): 14671 13602 145 145 0 14526 0 [pid=27249] vsize: 58684 Current children cumulated CPU time (s) 669.08 Current children cumulated vsize (Kb) 60808 [startup+680.048 s] Raw data (loadavg): 1.00 0.97 0.96 1/57 27251 Raw data (/proc/27245/stat): 27245 (minisat+_script) S 27244 27245 5299 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1855450281 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27245/statm): 531 226 485 147 0 384 0 [pid=27245] vsize: 2124 Raw data (/proc/27249/stat): 27249 (minisat+_64-bit) T 27245 27245 5299 0 -1 0 14068 0 0 0 67816 90 0 0 25 0 1 0 1855450286 60563456 13711 4294967295 134512640 135094434 3221224432 3221222796 134870330 0 0 5 16386 3222434794 0 0 17 1 0 0 Raw data (/proc/27249/statm): 14786 13711 145 145 0 14641 0 [pid=27249] vsize: 59144 Current children cumulated CPU time (s) 679.08 Current children cumulated vsize (Kb) 61268 [startup+690.049 s] Raw data (loadavg): 1.00 0.97 0.96 2/57 27251 Raw data (/proc/27245/stat): 27245 (minisat+_script) S 27244 27245 5299 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1855450281 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27245/statm): 531 226 485 147 0 384 0 [pid=27245] vsize: 2124 Raw data (/proc/27249/stat): 27249 (minisat+_64-bit) R 27245 27245 5299 0 -1 0 14172 0 0 0 68814 91 0 0 25 0 1 0 1855450286 60973056 13815 4294967295 134512640 135094434 3221224432 3221223044 134563046 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27249/statm): 14886 13815 145 145 0 14741 0 [pid=27249] vsize: 59544 Current children cumulated CPU time (s) 689.07 Current children cumulated vsize (Kb) 61668 [startup+700.049 s] Raw data (loadavg): 1.00 0.97 0.96 2/57 27251 Raw data (/proc/27245/stat): 27245 (minisat+_script) S 27244 27245 5299 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1855450281 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27245/statm): 531 226 485 147 0 384 0 [pid=27245] vsize: 2124 Raw data (/proc/27249/stat): 27249 (minisat+_64-bit) R 27245 27245 5299 0 -1 0 14283 0 0 0 69812 92 0 0 25 0 1 0 1855450286 61411328 13926 4294967295 134512640 135094434 3221224432 3221223044 134563121 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27249/statm): 14993 13926 145 145 0 14848 0 [pid=27249] vsize: 59972 Current children cumulated CPU time (s) 699.06 Current children cumulated vsize (Kb) 62096 [startup+710.05 s] Raw data (loadavg): 1.00 0.97 0.96 2/57 27251 Raw data (/proc/27245/stat): 27245 (minisat+_script) S 27244 27245 5299 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1855450281 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27245/statm): 531 226 485 147 0 384 0 [pid=27245] vsize: 2124 Raw data (/proc/27249/stat): 27249 (minisat+_64-bit) R 27245 27245 5299 0 -1 0 14480 0 0 0 70809 93 0 0 25 0 1 0 1855450286 62197760 14123 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27249/statm): 15185 14123 145 145 0 15040 0 [pid=27249] vsize: 60740 Current children cumulated CPU time (s) 709.04 Current children cumulated vsize (Kb) 62864 [startup+720.051 s] Raw data (loadavg): 1.00 0.97 0.96 2/57 27251 Raw data (/proc/27245/stat): 27245 (minisat+_script) S 27244 27245 5299 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1855450281 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27245/statm): 531 226 485 147 0 384 0 [pid=27245] vsize: 2124 Raw data (/proc/27249/stat): 27249 (minisat+_64-bit) R 27245 27245 5299 0 -1 0 14544 0 0 0 71808 94 0 0 25 0 1 0 1855450286 63496192 14187 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27249/statm): 15502 14187 145 145 0 15357 0 [pid=27249] vsize: 62008 Current children cumulated CPU time (s) 719.04 Current children cumulated vsize (Kb) 64132 [startup+730.051 s] Raw data (loadavg): 1.00 0.97 0.96 2/57 27251 Raw data (/proc/27245/stat): 27245 (minisat+_script) S 27244 27245 5299 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1855450281 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27245/statm): 531 226 485 147 0 384 0 [pid=27245] vsize: 2124 Raw data (/proc/27249/stat): 27249 (minisat+_64-bit) R 27245 27245 5299 0 -1 0 14646 0 0 0 72806 94 0 0 25 0 1 0 1855450286 63901696 14289 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27249/statm): 15601 14289 145 145 0 15456 0 [pid=27249] vsize: 62404 Current children cumulated CPU time (s) 729.02 Current children cumulated vsize (Kb) 64528 [startup+740.052 s] Raw data (loadavg): 1.00 0.97 0.96 2/57 27251 Raw data (/proc/27245/stat): 27245 (minisat+_script) S 27244 27245 5299 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1855450281 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27245/statm): 531 226 485 147 0 384 0 [pid=27245] vsize: 2124 Raw data (/proc/27249/stat): 27249 (minisat+_64-bit) R 27245 27245 5299 0 -1 0 15154 0 0 0 73799 98 0 0 25 0 1 0 1855450286 65949696 14797 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27249/statm): 16101 14797 145 145 0 15956 0 [pid=27249] vsize: 64404 Current children cumulated CPU time (s) 738.99 Current children cumulated vsize (Kb) 66528 [startup+750.052 s] Raw data (loadavg): 1.00 0.97 0.96 2/57 27251 Raw data (/proc/27245/stat): 27245 (minisat+_script) S 27244 27245 5299 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1855450281 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27245/statm): 531 226 485 147 0 384 0 [pid=27245] vsize: 2124 Raw data (/proc/27249/stat): 27249 (minisat+_64-bit) R 27245 27245 5299 0 -1 0 15493 0 0 0 74793 101 0 0 25 0 1 0 1855450286 67317760 15136 4294967295 134512640 135094434 3221224432 3221223088 134557866 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27249/statm): 16435 15136 145 145 0 16290 0 [pid=27249] vsize: 65740 Current children cumulated CPU time (s) 748.96 Current children cumulated vsize (Kb) 67864 [startup+760.053 s] Raw data (loadavg): 1.08 0.99 0.97 2/57 27251 Raw data (/proc/27245/stat): 27245 (minisat+_script) S 27244 27245 5299 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1855450281 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27245/statm): 531 226 485 147 0 384 0 [pid=27245] vsize: 2124 Raw data (/proc/27249/stat): 27249 (minisat+_64-bit) T 27245 27245 5299 0 -1 0 15563 0 0 0 75811 101 0 0 25 0 1 0 1855450286 67596288 15206 4294967295 134512640 135094434 3221224432 3221222780 134870330 0 0 5 16386 3222434794 0 0 17 1 0 0 Raw data (/proc/27249/statm): 16503 15206 145 145 0 16358 0 [pid=27249] vsize: 66012 Current children cumulated CPU time (s) 759.14 Current children cumulated vsize (Kb) 68136 [startup+771.337 s] Raw data (loadavg): 1.07 0.99 0.97 2/57 27251 Raw data (/proc/27245/stat): 27245 (minisat+_script) S 27244 27245 5299 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1855450281 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27245/statm): 531 226 485 147 0 384 0 [pid=27245] vsize: 2124 Raw data (/proc/27249/stat): 27249 (minisat+_64-bit) R 27245 27245 5299 0 -1 0 15670 0 0 0 76809 102 0 0 25 0 1 0 1855450286 68022272 15313 4294967295 134512640 135094434 3221224432 3221223088 134558007 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27249/statm): 16607 15313 145 145 0 16462 0 [pid=27249] vsize: 66428 Current children cumulated CPU time (s) 769.13 Current children cumulated vsize (Kb) 68552 [startup+781.338 s] Raw data (loadavg): 1.06 0.99 0.97 3/57 27251 Raw data (/proc/27245/stat): 27245 (minisat+_script) S 27244 27245 5299 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1855450281 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27245/statm): 531 226 485 147 0 384 0 [pid=27245] vsize: 2124 Raw data (/proc/27249/stat): 27249 (minisat+_64-bit) R 27245 27245 5299 0 -1 0 15856 0 0 0 77806 104 0 0 25 0 1 0 1855450286 68767744 15499 4294967295 134512640 135094434 3221224432 3221223044 134563055 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27249/statm): 16789 15499 145 145 0 16644 0 [pid=27249] vsize: 67156 Current children cumulated CPU time (s) 779.12 Current children cumulated vsize (Kb) 69280 [startup+791.339 s] Raw data (loadavg): 1.05 0.99 0.97 3/57 27251 Raw data (/proc/27245/stat): 27245 (minisat+_script) S 27244 27245 5299 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1855450281 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27245/statm): 531 226 485 147 0 384 0 [pid=27245] vsize: 2124 Raw data (/proc/27249/stat): 27249 (minisat+_64-bit) R 27245 27245 5299 0 -1 0 15966 0 0 0 78803 105 0 0 25 0 1 0 1855450286 69201920 15609 4294967295 134512640 135094434 3221224432 3221223088 134558159 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27249/statm): 16895 15609 145 145 0 16750 0 [pid=27249] vsize: 67580 Current children cumulated CPU time (s) 789.1 Current children cumulated vsize (Kb) 69704 [startup+801.339 s] Raw data (loadavg): 1.04 0.99 0.97 3/57 27251 Raw data (/proc/27245/stat): 27245 (minisat+_script) S 27244 27245 5299 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1855450281 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27245/statm): 531 226 485 147 0 384 0 [pid=27245] vsize: 2124 Raw data (/proc/27249/stat): 27249 (minisat+_64-bit) R 27245 27245 5299 0 -1 0 16130 0 0 0 79800 106 0 0 25 0 1 0 1855450286 69857280 15773 4294967295 134512640 135094434 3221224432 3221223088 134557849 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27249/statm): 17055 15773 145 145 0 16910 0 [pid=27249] vsize: 68220 Current children cumulated CPU time (s) 799.08 Current children cumulated vsize (Kb) 70344 [startup+811.341 s] Raw data (loadavg): 1.03 0.99 0.97 2/57 27251 Raw data (/proc/27245/stat): 27245 (minisat+_script) S 27244 27245 5299 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1855450281 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27245/statm): 531 226 485 147 0 384 0 [pid=27245] vsize: 2124 Raw data (/proc/27249/stat): 27249 (minisat+_64-bit) R 27245 27245 5299 0 -1 0 16233 0 0 0 80799 107 0 0 25 0 1 0 1855450286 70262784 15876 4294967295 134512640 135094434 3221224432 3221223044 134563049 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27249/statm): 17154 15876 145 145 0 17009 0 [pid=27249] vsize: 68616 Current children cumulated CPU time (s) 809.08 Current children cumulated vsize (Kb) 70740 [startup+821.341 s] Raw data (loadavg): 1.03 0.99 0.97 2/57 27251 Raw data (/proc/27245/stat): 27245 (minisat+_script) S 27244 27245 5299 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1855450281 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27245/statm): 531 226 485 147 0 384 0 [pid=27245] vsize: 2124 Raw data (/proc/27249/stat): 27249 (minisat+_64-bit) R 27245 27245 5299 0 -1 0 16345 0 0 0 81797 108 0 0 25 0 1 0 1855450286 70709248 15988 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27249/statm): 17263 15988 145 145 0 17118 0 [pid=27249] vsize: 69052 Current children cumulated CPU time (s) 819.07 Current children cumulated vsize (Kb) 71176 [startup+831.342 s] Raw data (loadavg): 1.02 0.99 0.97 2/57 27251 Raw data (/proc/27245/stat): 27245 (minisat+_script) S 27244 27245 5299 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1855450281 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27245/statm): 531 226 485 147 0 384 0 [pid=27245] vsize: 2124 Raw data (/proc/27249/stat): 27249 (minisat+_64-bit) R 27245 27245 5299 0 -1 0 16441 0 0 0 82795 109 0 0 25 0 1 0 1855450286 71090176 16084 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27249/statm): 17356 16084 145 145 0 17211 0 [pid=27249] vsize: 69424 Current children cumulated CPU time (s) 829.06 Current children cumulated vsize (Kb) 71548 [startup+841.343 s] Raw data (loadavg): 1.02 0.99 0.97 2/57 27251 Raw data (/proc/27245/stat): 27245 (minisat+_script) S 27244 27245 5299 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1855450281 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27245/statm): 531 226 485 147 0 384 0 [pid=27245] vsize: 2124 Raw data (/proc/27249/stat): 27249 (minisat+_64-bit) R 27245 27245 5299 0 -1 0 16518 0 0 0 83793 110 0 0 25 0 1 0 1855450286 71393280 16161 4294967295 134512640 135094434 3221224432 3221223024 134557398 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27249/statm): 17430 16161 145 145 0 17285 0 [pid=27249] vsize: 69720 Current children cumulated CPU time (s) 839.05 Current children cumulated vsize (Kb) 71844 [startup+851.343 s] Raw data (loadavg): 1.02 0.99 0.97 2/57 27251 Raw data (/proc/27245/stat): 27245 (minisat+_script) S 27244 27245 5299 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1855450281 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27245/statm): 531 226 485 147 0 384 0 [pid=27245] vsize: 2124 Raw data (/proc/27249/stat): 27249 (minisat+_64-bit) R 27245 27245 5299 0 -1 0 16790 0 0 0 84789 112 0 0 25 0 1 0 1855450286 72482816 16433 4294967295 134512640 135094434 3221224432 3221223088 134558024 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27249/statm): 17696 16433 145 145 0 17551 0 [pid=27249] vsize: 70784 Current children cumulated CPU time (s) 849.03 Current children cumulated vsize (Kb) 72908 [startup+861.344 s] Raw data (loadavg): 1.01 0.99 0.97 2/57 27251 Raw data (/proc/27245/stat): 27245 (minisat+_script) S 27244 27245 5299 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1855450281 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27245/statm): 531 226 485 147 0 384 0 [pid=27245] vsize: 2124 Raw data (/proc/27249/stat): 27249 (minisat+_64-bit) R 27245 27245 5299 0 -1 0 16910 0 0 0 85786 113 0 0 25 0 1 0 1855450286 72957952 16553 4294967295 134512640 135094434 3221224432 3221223088 134558246 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27249/statm): 17812 16553 145 145 0 17667 0 [pid=27249] vsize: 71248 Current children cumulated CPU time (s) 859.01 Current children cumulated vsize (Kb) 73372 [startup+871.345 s] Raw data (loadavg): 1.01 0.99 0.97 2/57 27251 Raw data (/proc/27245/stat): 27245 (minisat+_script) S 27244 27245 5299 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1855450281 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27245/statm): 531 226 485 147 0 384 0 [pid=27245] vsize: 2124 Raw data (/proc/27249/stat): 27249 (minisat+_64-bit) R 27245 27245 5299 0 -1 0 17034 0 0 0 86784 114 0 0 25 0 1 0 1855450286 73453568 16677 4294967295 134512640 135094434 3221224432 3221223088 134558187 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27249/statm): 17933 16677 145 145 0 17788 0 [pid=27249] vsize: 71732 Current children cumulated CPU time (s) 869 Current children cumulated vsize (Kb) 73856 [startup+881.345 s] Raw data (loadavg): 1.01 0.99 0.97 2/57 27251 Raw data (/proc/27245/stat): 27245 (minisat+_script) S 27244 27245 5299 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1855450281 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27245/statm): 531 226 485 147 0 384 0 [pid=27245] vsize: 2124 Raw data (/proc/27249/stat): 27249 (minisat+_64-bit) R 27245 27245 5299 0 -1 0 17148 0 0 0 87781 115 0 0 25 0 1 0 1855450286 73904128 16791 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27249/statm): 18043 16791 145 145 0 17898 0 [pid=27249] vsize: 72172 Current children cumulated CPU time (s) 878.98 Current children cumulated vsize (Kb) 74296 [startup+891.347 s] Raw data (loadavg): 1.01 0.99 0.97 2/57 27251 Raw data (/proc/27245/stat): 27245 (minisat+_script) S 27244 27245 5299 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1855450281 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27245/statm): 531 226 485 147 0 384 0 [pid=27245] vsize: 2124 Raw data (/proc/27249/stat): 27249 (minisat+_64-bit) R 27245 27245 5299 0 -1 0 17246 0 0 0 88778 117 0 0 25 0 1 0 1855450286 74293248 16889 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27249/statm): 18138 16889 145 145 0 17993 0 [pid=27249] vsize: 72552 Current children cumulated CPU time (s) 888.97 Current children cumulated vsize (Kb) 74676 [startup+901.348 s] Raw data (loadavg): 1.00 0.99 0.97 2/57 27251 Raw data (/proc/27245/stat): 27245 (minisat+_script) S 27244 27245 5299 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1855450281 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27245/statm): 531 226 485 147 0 384 0 [pid=27245] vsize: 2124 Raw data (/proc/27249/stat): 27249 (minisat+_64-bit) R 27245 27245 5299 0 -1 0 17348 0 0 0 89776 117 0 0 25 0 1 0 1855450286 74698752 16991 4294967295 134512640 135094434 3221224432 3221223056 134557726 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27249/statm): 18237 16991 145 145 0 18092 0 [pid=27249] vsize: 72948 Current children cumulated CPU time (s) 898.95 Current children cumulated vsize (Kb) 75072 [startup+911.348 s] Raw data (loadavg): 1.00 0.99 0.97 2/57 27251 Raw data (/proc/27245/stat): 27245 (minisat+_script) S 27244 27245 5299 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1855450281 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27245/statm): 531 226 485 147 0 384 0 [pid=27245] vsize: 2124 Raw data (/proc/27249/stat): 27249 (minisat+_64-bit) R 27245 27245 5299 0 -1 0 17423 0 0 0 90775 118 0 0 25 0 1 0 1855450286 74993664 17066 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27249/statm): 18309 17066 145 145 0 18164 0 [pid=27249] vsize: 73236 Current children cumulated CPU time (s) 908.95 Current children cumulated vsize (Kb) 75360 [startup+921.349 s] Raw data (loadavg): 1.00 0.99 0.97 2/57 27251 Raw data (/proc/27245/stat): 27245 (minisat+_script) S 27244 27245 5299 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1855450281 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27245/statm): 531 226 485 147 0 384 0 [pid=27245] vsize: 2124 Raw data (/proc/27249/stat): 27249 (minisat+_64-bit) R 27245 27245 5299 0 -1 0 17491 0 0 0 91774 119 0 0 25 0 1 0 1855450286 75264000 17134 4294967295 134512640 135094434 3221224432 3221223056 134557665 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27249/statm): 18375 17134 145 145 0 18230 0 [pid=27249] vsize: 73500 Current children cumulated CPU time (s) 918.95 Current children cumulated vsize (Kb) 75624 [startup+931.35 s] Raw data (loadavg): 1.00 0.99 0.97 2/57 27251 Raw data (/proc/27245/stat): 27245 (minisat+_script) S 27244 27245 5299 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1855450281 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27245/statm): 531 226 485 147 0 384 0 [pid=27245] vsize: 2124 Raw data (/proc/27249/stat): 27249 (minisat+_64-bit) R 27245 27245 5299 0 -1 0 17631 0 0 0 92771 120 0 0 25 0 1 0 1855450286 75821056 17274 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27249/statm): 18511 17274 145 145 0 18366 0 [pid=27249] vsize: 74044 Current children cumulated CPU time (s) 928.93 Current children cumulated vsize (Kb) 76168 [startup+941.35 s] Raw data (loadavg): 1.00 0.99 0.97 2/57 27251 Raw data (/proc/27245/stat): 27245 (minisat+_script) S 27244 27245 5299 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1855450281 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27245/statm): 531 226 485 147 0 384 0 [pid=27245] vsize: 2124 Raw data (/proc/27249/stat): 27249 (minisat+_64-bit) R 27245 27245 5299 0 -1 0 17727 0 0 0 93770 120 0 0 25 0 1 0 1855450286 76197888 17370 4294967295 134512640 135094434 3221224432 3221223044 134563077 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27249/statm): 18603 17370 145 145 0 18458 0 [pid=27249] vsize: 74412 Current children cumulated CPU time (s) 938.92 Current children cumulated vsize (Kb) 76536 [startup+951.351 s] Raw data (loadavg): 1.00 0.99 0.97 2/57 27251 Raw data (/proc/27245/stat): 27245 (minisat+_script) S 27244 27245 5299 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1855450281 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27245/statm): 531 226 485 147 0 384 0 [pid=27245] vsize: 2124 Raw data (/proc/27249/stat): 27249 (minisat+_64-bit) R 27245 27245 5299 0 -1 0 17914 0 0 0 94766 122 0 0 25 0 1 0 1855450286 76947456 17557 4294967295 134512640 135094434 3221224432 3221223088 134557978 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27249/statm): 18786 17557 145 145 0 18641 0 [pid=27249] vsize: 75144 Current children cumulated CPU time (s) 948.9 Current children cumulated vsize (Kb) 77268 [startup+961.352 s] Raw data (loadavg): 1.00 0.99 0.97 2/57 27251 Raw data (/proc/27245/stat): 27245 (minisat+_script) S 27244 27245 5299 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1855450281 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27245/statm): 531 226 485 147 0 384 0 [pid=27245] vsize: 2124 Raw data (/proc/27249/stat): 27249 (minisat+_64-bit) R 27245 27245 5299 0 -1 0 18114 0 0 0 95764 123 0 0 25 0 1 0 1855450286 77742080 17757 4294967295 134512640 135094434 3221224432 3221223088 134557884 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27249/statm): 18980 17757 145 145 0 18835 0 [pid=27249] vsize: 75920 Current children cumulated CPU time (s) 958.89 Current children cumulated vsize (Kb) 78044 [startup+971.353 s] Raw data (loadavg): 1.00 0.99 0.97 2/57 27251 Raw data (/proc/27245/stat): 27245 (minisat+_script) S 27244 27245 5299 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1855450281 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27245/statm): 531 226 485 147 0 384 0 [pid=27245] vsize: 2124 Raw data (/proc/27249/stat): 27249 (minisat+_64-bit) R 27245 27245 5299 0 -1 0 18263 0 0 0 96762 124 0 0 25 0 1 0 1855450286 78336000 17906 4294967295 134512640 135094434 3221224432 3221223092 134553482 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27249/statm): 19125 17906 145 145 0 18980 0 [pid=27249] vsize: 76500 Current children cumulated CPU time (s) 968.88 Current children cumulated vsize (Kb) 78624 [startup+981.354 s] Raw data (loadavg): 1.00 0.99 0.97 2/57 27251 Raw data (/proc/27245/stat): 27245 (minisat+_script) S 27244 27245 5299 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1855450281 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27245/statm): 531 226 485 147 0 384 0 [pid=27245] vsize: 2124 Raw data (/proc/27249/stat): 27249 (minisat+_64-bit) R 27245 27245 5299 0 -1 0 18413 0 0 0 97758 126 0 0 25 0 1 0 1855450286 78942208 18056 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27249/statm): 19273 18056 145 145 0 19128 0 [pid=27249] vsize: 77092 Current children cumulated CPU time (s) 978.86 Current children cumulated vsize (Kb) 79216 [startup+991.355 s] Raw data (loadavg): 1.00 0.99 0.97 2/57 27251 Raw data (/proc/27245/stat): 27245 (minisat+_script) S 27244 27245 5299 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1855450281 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27245/statm): 531 226 485 147 0 384 0 [pid=27245] vsize: 2124 Raw data (/proc/27249/stat): 27249 (minisat+_64-bit) R 27245 27245 5299 0 -1 0 18545 0 0 0 98753 129 0 0 25 0 1 0 1855450286 79450112 18188 4294967295 134512640 135094434 3221224432 3221223104 134555943 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27249/statm): 19397 18188 145 145 0 19252 0 [pid=27249] vsize: 77588 Current children cumulated CPU time (s) 988.84 Current children cumulated vsize (Kb) 79712 [startup+1001.36 s] Raw data (loadavg): 1.00 0.99 0.97 2/57 27251 Raw data (/proc/27245/stat): 27245 (minisat+_script) S 27244 27245 5299 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1855450281 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27245/statm): 531 226 485 147 0 384 0 [pid=27245] vsize: 2124 Raw data (/proc/27249/stat): 27249 (minisat+_64-bit) R 27245 27245 5299 0 -1 0 18684 0 0 0 99751 130 0 0 25 0 1 0 1855450286 80048128 18327 4294967295 134512640 135094434 3221224432 3221223088 134557988 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27249/statm): 19543 18327 145 145 0 19398 0 [pid=27249] vsize: 78172 Current children cumulated CPU time (s) 998.83 Current children cumulated vsize (Kb) 80296 [startup+1011.36 s] Raw data (loadavg): 1.00 0.99 0.97 2/57 27251 Raw data (/proc/27245/stat): 27245 (minisat+_script) S 27244 27245 5299 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1855450281 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27245/statm): 531 226 485 147 0 384 0 [pid=27245] vsize: 2124 Raw data (/proc/27249/stat): 27249 (minisat+_64-bit) R 27245 27245 5299 0 -1 0 18816 0 0 0 100749 131 0 0 25 0 1 0 1855450286 80625664 18459 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27249/statm): 19684 18459 145 145 0 19539 0 [pid=27249] vsize: 78736 Current children cumulated CPU time (s) 1008.82 Current children cumulated vsize (Kb) 80860 [startup+1021.36 s] Raw data (loadavg): 1.00 0.99 0.97 2/57 27251 Raw data (/proc/27245/stat): 27245 (minisat+_script) S 27244 27245 5299 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1855450281 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27245/statm): 531 226 485 147 0 384 0 [pid=27245] vsize: 2124 Raw data (/proc/27249/stat): 27249 (minisat+_64-bit) R 27245 27245 5299 0 -1 0 18964 0 0 0 101748 132 0 0 25 0 1 0 1855450286 81268736 18607 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27249/statm): 19841 18607 145 145 0 19696 0 [pid=27249] vsize: 79364 Current children cumulated CPU time (s) 1018.82 Current children cumulated vsize (Kb) 81488 [startup+1031.36 s] Raw data (loadavg): 1.00 0.99 0.97 2/57 27251 Raw data (/proc/27245/stat): 27245 (minisat+_script) S 27244 27245 5299 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1855450281 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27245/statm): 531 226 485 147 0 384 0 [pid=27245] vsize: 2124 Raw data (/proc/27249/stat): 27249 (minisat+_64-bit) R 27245 27245 5299 0 -1 0 19095 0 0 0 102745 134 0 0 25 0 1 0 1855450286 81797120 18738 4294967295 134512640 135094434 3221224432 3221223088 134557835 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27249/statm): 19970 18738 145 145 0 19825 0 [pid=27249] vsize: 79880 Current children cumulated CPU time (s) 1028.81 Current children cumulated vsize (Kb) 82004 [startup+1041.36 s] Raw data (loadavg): 1.00 0.99 0.97 2/57 27251 Raw data (/proc/27245/stat): 27245 (minisat+_script) S 27244 27245 5299 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1855450281 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27245/statm): 531 226 485 147 0 384 0 [pid=27245] vsize: 2124 Raw data (/proc/27249/stat): 27249 (minisat+_64-bit) R 27245 27245 5299 0 -1 0 19220 0 0 0 103742 135 0 0 25 0 1 0 1855450286 82292736 18863 4294967295 134512640 135094434 3221224432 3221223088 134558013 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27249/statm): 20091 18863 145 145 0 19946 0 [pid=27249] vsize: 80364 Current children cumulated CPU time (s) 1038.79 Current children cumulated vsize (Kb) 82488 [startup+1051.36 s] Raw data (loadavg): 1.00 0.99 0.97 2/57 27251 Raw data (/proc/27245/stat): 27245 (minisat+_script) S 27244 27245 5299 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1855450281 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27245/statm): 531 226 485 147 0 384 0 [pid=27245] vsize: 2124 Raw data (/proc/27249/stat): 27249 (minisat+_64-bit) R 27245 27245 5299 0 -1 0 19377 0 0 0 104740 136 0 0 25 0 1 0 1855450286 82952192 19020 4294967295 134512640 135094434 3221224432 3221223088 134558249 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27249/statm): 20252 19020 145 145 0 20107 0 [pid=27249] vsize: 81008 Current children cumulated CPU time (s) 1048.78 Current children cumulated vsize (Kb) 83132 [startup+1061.36 s] Raw data (loadavg): 1.00 0.99 0.97 2/57 27251 Raw data (/proc/27245/stat): 27245 (minisat+_script) S 27244 27245 5299 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1855450281 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27245/statm): 531 226 485 147 0 384 0 [pid=27245] vsize: 2124 Raw data (/proc/27249/stat): 27249 (minisat+_64-bit) R 27245 27245 5299 0 -1 0 19534 0 0 0 105738 137 0 0 25 0 1 0 1855450286 83582976 19177 4294967295 134512640 135094434 3221224432 3221223088 134557996 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27249/statm): 20406 19177 145 145 0 20261 0 [pid=27249] vsize: 81624 Current children cumulated CPU time (s) 1058.77 Current children cumulated vsize (Kb) 83748 [startup+1071.36 s] Raw data (loadavg): 1.00 0.99 0.97 2/57 27251 Raw data (/proc/27245/stat): 27245 (minisat+_script) S 27244 27245 5299 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1855450281 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27245/statm): 531 226 485 147 0 384 0 [pid=27245] vsize: 2124 Raw data (/proc/27249/stat): 27249 (minisat+_64-bit) R 27245 27245 5299 0 -1 0 19643 0 0 0 106736 138 0 0 25 0 1 0 1855450286 84013056 19286 4294967295 134512640 135094434 3221224432 3221223088 134558181 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27249/statm): 20511 19286 145 145 0 20366 0 [pid=27249] vsize: 82044 Current children cumulated CPU time (s) 1068.76 Current children cumulated vsize (Kb) 84168 [startup+1081.36 s] Raw data (loadavg): 1.00 0.99 0.97 2/57 27251 Raw data (/proc/27245/stat): 27245 (minisat+_script) S 27244 27245 5299 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1855450281 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27245/statm): 531 226 485 147 0 384 0 [pid=27245] vsize: 2124 Raw data (/proc/27249/stat): 27249 (minisat+_64-bit) R 27245 27245 5299 0 -1 0 19732 0 0 0 107734 138 0 0 25 0 1 0 1855450286 84365312 19375 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27249/statm): 20597 19375 145 145 0 20452 0 [pid=27249] vsize: 82388 Current children cumulated CPU time (s) 1078.74 Current children cumulated vsize (Kb) 84512 [startup+1091.36 s] Raw data (loadavg): 1.00 0.99 0.97 2/57 27251 Raw data (/proc/27245/stat): 27245 (minisat+_script) S 27244 27245 5299 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1855450281 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27245/statm): 531 226 485 147 0 384 0 [pid=27245] vsize: 2124 Raw data (/proc/27249/stat): 27249 (minisat+_64-bit) R 27245 27245 5299 0 -1 0 20014 0 0 0 108728 141 0 0 21 0 1 0 1855450286 85508096 19657 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27249/statm): 20876 19657 145 145 0 20731 0 [pid=27249] vsize: 83504 Current children cumulated CPU time (s) 1088.71 Current children cumulated vsize (Kb) 85628 [startup+1101.36 s] Raw data (loadavg): 1.00 0.99 0.97 2/57 27251 Raw data (/proc/27245/stat): 27245 (minisat+_script) S 27244 27245 5299 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1855450281 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27245/statm): 531 226 485 147 0 384 0 [pid=27245] vsize: 2124 Raw data (/proc/27249/stat): 27249 (minisat+_64-bit) R 27245 27245 5299 0 -1 0 20182 0 0 0 109726 143 0 0 25 0 1 0 1855450286 86183936 19825 4294967295 134512640 135094434 3221224432 3221223024 134551465 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27249/statm): 21041 19825 145 145 0 20896 0 [pid=27249] vsize: 84164 Current children cumulated CPU time (s) 1098.71 Current children cumulated vsize (Kb) 86288 [startup+1111.37 s] Raw data (loadavg): 1.00 0.99 0.97 2/57 27251 Raw data (/proc/27245/stat): 27245 (minisat+_script) S 27244 27245 5299 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1855450281 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27245/statm): 531 226 485 147 0 384 0 [pid=27245] vsize: 2124 Raw data (/proc/27249/stat): 27249 (minisat+_64-bit) R 27245 27245 5299 0 -1 0 20182 0 0 0 110726 143 0 0 25 0 1 0 1855450286 86183936 19825 4294967295 134512640 135094434 3221224432 3221223072 134562149 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27249/statm): 21041 19825 145 145 0 20896 0 [pid=27249] vsize: 84164 Current children cumulated CPU time (s) 1108.71 Current children cumulated vsize (Kb) 86288 [startup+1121.37 s] Raw data (loadavg): 1.00 0.99 0.97 2/57 27251 Raw data (/proc/27245/stat): 27245 (minisat+_script) S 27244 27245 5299 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1855450281 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27245/statm): 531 226 485 147 0 384 0 [pid=27245] vsize: 2124 Raw data (/proc/27249/stat): 27249 (minisat+_64-bit) R 27245 27245 5299 0 -1 0 20182 0 0 0 111726 143 0 0 25 0 1 0 1855450286 86183936 19825 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27249/statm): 21041 19825 145 145 0 20896 0 [pid=27249] vsize: 84164 Current children cumulated CPU time (s) 1118.71 Current children cumulated vsize (Kb) 86288 [startup+1131.37 s] Raw data (loadavg): 1.00 0.99 0.97 2/57 27251 Raw data (/proc/27245/stat): 27245 (minisat+_script) S 27244 27245 5299 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1855450281 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27245/statm): 531 226 485 147 0 384 0 [pid=27245] vsize: 2124 Raw data (/proc/27249/stat): 27249 (minisat+_64-bit) R 27245 27245 5299 0 -1 0 20182 0 0 0 112726 143 0 0 25 0 1 0 1855450286 86183936 19825 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27249/statm): 21041 19825 145 145 0 20896 0 [pid=27249] vsize: 84164 Current children cumulated CPU time (s) 1128.71 Current children cumulated vsize (Kb) 86288 [startup+1141.37 s] Raw data (loadavg): 1.00 0.99 0.97 2/57 27251 Raw data (/proc/27245/stat): 27245 (minisat+_script) S 27244 27245 5299 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1855450281 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27245/statm): 531 226 485 147 0 384 0 [pid=27245] vsize: 2124 Raw data (/proc/27249/stat): 27249 (minisat+_64-bit) R 27245 27245 5299 0 -1 0 20182 0 0 0 113726 143 0 0 25 0 1 0 1855450286 86183936 19825 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27249/statm): 21041 19825 145 145 0 20896 0 [pid=27249] vsize: 84164 Current children cumulated CPU time (s) 1138.71 Current children cumulated vsize (Kb) 86288 [startup+1151.37 s] Raw data (loadavg): 1.00 0.99 0.97 2/57 27251 Raw data (/proc/27245/stat): 27245 (minisat+_script) S 27244 27245 5299 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1855450281 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27245/statm): 531 226 485 147 0 384 0 [pid=27245] vsize: 2124 Raw data (/proc/27249/stat): 27249 (minisat+_64-bit) R 27245 27245 5299 0 -1 0 20182 0 0 0 114727 143 0 0 25 0 1 0 1855450286 86183936 19825 4294967295 134512640 135094434 3221224432 3221223044 134563071 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27249/statm): 21041 19825 145 145 0 20896 0 [pid=27249] vsize: 84164 Current children cumulated CPU time (s) 1148.72 Current children cumulated vsize (Kb) 86288 [startup+1161.37 s] Raw data (loadavg): 1.00 0.99 0.97 2/57 27251 Raw data (/proc/27245/stat): 27245 (minisat+_script) S 27244 27245 5299 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1855450281 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27245/statm): 531 226 485 147 0 384 0 [pid=27245] vsize: 2124 Raw data (/proc/27249/stat): 27249 (minisat+_64-bit) R 27245 27245 5299 0 -1 0 20182 0 0 0 115727 143 0 0 25 0 1 0 1855450286 86183936 19825 4294967295 134512640 135094434 3221224432 3221223088 134558156 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27249/statm): 21041 19825 145 145 0 20896 0 [pid=27249] vsize: 84164 Current children cumulated CPU time (s) 1158.72 Current children cumulated vsize (Kb) 86288 [startup+1171.37 s] Raw data (loadavg): 1.00 0.99 0.97 2/57 27251 Raw data (/proc/27245/stat): 27245 (minisat+_script) S 27244 27245 5299 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1855450281 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27245/statm): 531 226 485 147 0 384 0 [pid=27245] vsize: 2124 Raw data (/proc/27249/stat): 27249 (minisat+_64-bit) R 27245 27245 5299 0 -1 0 20182 0 0 0 116727 144 0 0 25 0 1 0 1855450286 86183936 19825 4294967295 134512640 135094434 3221224432 3221223044 134563049 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27249/statm): 21041 19825 145 145 0 20896 0 [pid=27249] vsize: 84164 Current children cumulated CPU time (s) 1168.73 Current children cumulated vsize (Kb) 86288 [startup+1181.37 s] Raw data (loadavg): 1.00 0.99 0.97 2/57 27251 Raw data (/proc/27245/stat): 27245 (minisat+_script) S 27244 27245 5299 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1855450281 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27245/statm): 531 226 485 147 0 384 0 [pid=27245] vsize: 2124 Raw data (/proc/27249/stat): 27249 (minisat+_64-bit) R 27245 27245 5299 0 -1 0 20182 0 0 0 117727 144 0 0 25 0 1 0 1855450286 86183936 19825 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27249/statm): 21041 19825 145 145 0 20896 0 [pid=27249] vsize: 84164 Current children cumulated CPU time (s) 1178.73 Current children cumulated vsize (Kb) 86288 [startup+1191.37 s] Raw data (loadavg): 1.00 0.99 0.97 2/57 27251 Raw data (/proc/27245/stat): 27245 (minisat+_script) S 27244 27245 5299 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1855450281 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27245/statm): 531 226 485 147 0 384 0 [pid=27245] vsize: 2124 Raw data (/proc/27249/stat): 27249 (minisat+_64-bit) R 27245 27245 5299 0 -1 0 20182 0 0 0 118727 144 0 0 25 0 1 0 1855450286 86183936 19825 4294967295 134512640 135094434 3221224432 3221223056 134557568 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27249/statm): 21041 19825 145 145 0 20896 0 [pid=27249] vsize: 84164 Current children cumulated CPU time (s) 1188.73 Current children cumulated vsize (Kb) 86288 [startup+1201.37 s] Raw data (loadavg): 1.00 0.99 0.97 2/57 27251 Raw data (/proc/27245/stat): 27245 (minisat+_script) S 27244 27245 5299 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1855450281 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27245/statm): 531 226 485 147 0 384 0 [pid=27245] vsize: 2124 Raw data (/proc/27249/stat): 27249 (minisat+_64-bit) R 27245 27245 5299 0 -1 0 20182 0 0 0 119727 144 0 0 25 0 1 0 1855450286 86183936 19825 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27249/statm): 21041 19825 145 145 0 20896 0 [pid=27249] vsize: 84164 Current children cumulated CPU time (s) 1198.73 Current children cumulated vsize (Kb) 86288 [startup+1211.37 s] Raw data (loadavg): 1.00 0.99 0.97 2/57 27251 Raw data (/proc/27245/stat): 27245 (minisat+_script) S 27244 27245 5299 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1855450281 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27245/statm): 531 226 485 147 0 384 0 [pid=27245] vsize: 2124 Raw data (/proc/27249/stat): 27249 (minisat+_64-bit) R 27245 27245 5299 0 -1 0 20182 0 0 0 120727 144 0 0 25 0 1 0 1855450286 86183936 19825 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27249/statm): 21041 19825 145 145 0 20896 0 [pid=27249] vsize: 84164 Current children cumulated CPU time (s) 1208.73 Current children cumulated vsize (Kb) 86288 Maximum CPU time exceeded: sending SIGTERM then SIGKILL [startup+1211.37 s] Raw data (loadavg): 1.00 0.99 0.97 2/57 27251 Raw data (/proc/27245/stat): 27245 (minisat+_script) S 27244 27245 5299 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1855450281 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27245/statm): 531 226 485 147 0 384 0 [pid=27245] vsize: 2124 Raw data (/proc/27249/stat): 27249 (minisat+_64-bit) R 27245 27245 5299 0 -1 0 20182 0 0 0 120727 144 0 0 25 0 1 0 1855450286 86183936 19825 4294967295 134512640 135094434 3221224432 3221223088 134558033 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27249/statm): 21041 19825 145 145 0 20896 0 [pid=27249] vsize: 84164 Current children cumulated CPU time (s) 1208.73 Current children cumulated vsize (Kb) 86288 Sending SIGTERM to -27245 Sleeping 2 seconds One traced child (pid=27245) ended because it received signal 15 (SIGTERM) One traced child (pid=27249) exited with status: 0 All traced children have exited ! Game is over. Child status: 0 Real time (s): 1211.65 CPU time (s): 1208.76 CPU user time (s): 1207.27 CPU system time (s): 1.48477 CPU usage (%): 99.7609 Max. virtual memory (cumulated for all children) (Kb): 86288
ERROR: no interpretation found !