Name | mps-v2-20-10/MIPLIB/miplib2003/normalized-mps-v2-20-10-pp08aCUTS.opb |
MD5SUM | d9b143d593d6c40f70d01400b968fa76 |
Bench Category | optimization, big integers (OPTBIGINT) |
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 | 3424 |
Biggest coefficient in the objective function | 1073741824 |
Number of bits for the biggest coefficient in the objective function | 31 |
Sum of the numbers in the objective function | 180407058264 |
Number of bits of the sum of numbers in the objective function | 38 |
Biggest number in a constraint | 1073741824 |
Number of bits of the biggest number in a constraint | 31 |
Biggest sum of numbers in a constraint | 180407058264 |
Number of bits of the biggest sum of numbers | 38 |
Best result obtained on this benchmark | |
Best CPU time to get the best result obtained on this benchmark | |
Number of variables | 4600 |
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 | 147 |
LAUNCH ON wulflinc10 THE 2005-09-19 03:50:20 (client local time) PB2005-SCRIPT v4.0 MARKUPS: idlaunch=2935 boxname=wulflinc10 idbench=591 idsolver=3 numberseed=0 MD5SUM SOLVER: MD5SUM BENCH: d9b143d593d6c40f70d01400b968fa76 /oldhome/oroussel/tmp/wulflinc10/normalized-mps-v2-20-10-pp08aCUTS.opb REAL COMMAND: minisat+_script /oldhome/oroussel/tmp/wulflinc10/normalized-mps-v2-20-10-pp08aCUTS.opb IDLAUNCH: 2935 /proc/cpuinfo: processor : 0 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 2 cpu MHz : 450.999 cache size : 512 KB fdiv_bug : no hlt_bug : no f00f_bug : no coma_bug : no fpu : yes fpu_exception : yes cpuid level : 2 wp : yes flags : fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse bogomips : 890.88 processor : 1 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 2 cpu MHz : 450.999 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: 864940 kB Buffers: 37000 kB Cached: 105640 kB SwapCached: 228 kB Active: 68160 kB Inactive: 77460 kB HighTotal: 131008 kB HighFree: 56336 kB LowTotal: 903652 kB LowFree: 808604 kB SwapTotal: 2097136 kB SwapFree: 2096756 kB Dirty: 28 kB Writeback: 0 kB Mapped: 6272 kB Slab: 18480 kB Committed_AS: 64128 kB PageTables: 328 kB VmallocTotal: 114680 kB VmallocUsed: 1364 kB VmallocChunk: 113256 kB JOB ENDED THE 2005-09-19 04:10:31 (client local time) WITH STATUS 0 IN 1208.83 SECONDS stats: 2935 7 1208.83 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: 18 c ---[ 500]---> BDD-cost: 18 c ---[ 499]---> BDD-cost: 18 c ---[ 498]---> BDD-cost: 18 c ---[ 497]---> BDD-cost: 18 c ---[ 496]---> BDD-cost: 18 c ---[ 495]---> BDD-cost: 18 c ---[ 494]---> BDD-cost: 18 c ---[ 485]---> BDD-cost: 18 c ---[ 484]---> BDD-cost: 18 c ---[ 483]---> BDD-cost: 18 c ---[ 482]---> BDD-cost: 18 c ---[ 481]---> BDD-cost: 18 c ---[ 480]---> BDD-cost: 18 c ---[ 479]---> BDD-cost: 18 c ---[ 477]---> BDD-cost: 18 c ---[ 476]---> BDD-cost: 18 c ---[ 475]---> BDD-cost: 18 c ---[ 474]---> BDD-cost: 18 c ---[ 473]---> BDD-cost: 18 c ---[ 472]---> BDD-cost: 18 c ---[ 471]---> BDD-cost: 18 c ---[ 469]---> BDD-cost: 17 c ---[ 468]---> BDD-cost: 17 c ---[ 467]---> BDD-cost: 17 c ---[ 466]---> BDD-cost: 17 c ---[ 465]---> BDD-cost: 17 c ---[ 464]---> BDD-cost: 17 c ---[ 463]---> BDD-cost: 17 c ---[ 462]---> BDD-cost: 17 c ---[ 461]---> BDD-cost: 18 c ---[ 460]---> BDD-cost: 18 c ---[ 459]---> BDD-cost: 18 c ---[ 458]---> BDD-cost: 18 c ---[ 457]---> BDD-cost: 18 c ---[ 456]---> BDD-cost: 18 c ---[ 455]---> BDD-cost: 18 c ---[ 454]---> BDD-cost: 18 c ---[ 445]---> BDD-cost: 16 c ---[ 444]---> BDD-cost: 16 c ---[ 443]---> BDD-cost: 16 c ---[ 442]---> BDD-cost: 16 c ---[ 441]---> BDD-cost: 16 c ---[ 440]---> BDD-cost: 16 c ---[ 439]---> BDD-cost: 16 c ---[ 438]---> BDD-cost: 16 c ---[ 436]---> BDD-cost: 220 c ---[ 434]---> Sorter-cost: 1687 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 433]---> BDD-cost: 6 c ---[ 432]---> BDD-cost: 6 c ---[ 431]---> BDD-cost: 6 c ---[ 430]---> BDD-cost: 6 c ---[ 429]---> BDD-cost: 26 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: 1687 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 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: 1687 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 409]---> BDD-cost: 6 c ---[ 408]---> BDD-cost: 22 c ---[ 407]---> BDD-cost: 22 c ---[ 406]---> BDD-cost: 22 c ---[ 405]---> BDD-cost: 22 c ---[ 404]---> BDD-cost: 22 c ---[ 403]---> BDD-cost: 22 c ---[ 402]---> BDD-cost: 22 c ---[ 401]---> BDD-cost: 22 c ---[ 400]---> BDD-cost: 6 c ---[ 398]---> Sorter-cost: 1687 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 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: 1687 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 374]---> Sorter-cost: 1687 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 362]---> Sorter-cost: 595 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 350]---> Sorter-cost: 604 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 338]---> Sorter-cost: 1706 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 326]---> Sorter-cost: 1706 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 314]---> Sorter-cost: 1706 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 312]---> Sorter-cost: 1706 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 300]---> Sorter-cost: 1706 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 288]---> Sorter-cost: 1706 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 276]---> Sorter-cost: 1706 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 264]---> Sorter-cost: 604 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 255]---> BDD-cost: 220 c ---[ 253]---> Sorter-cost: 1706 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 251]---> Sorter-cost: 1706 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 249]---> Sorter-cost: 1706 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 247]---> Sorter-cost: 1706 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 245]---> Sorter-cost: 1706 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 243]---> Sorter-cost: 1706 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 241]---> Sorter-cost: 1706 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 239]---> Sorter-cost: 604 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 237]---> Sorter-cost: 595 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 235]---> Sorter-cost: 1687 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 233]---> Sorter-cost: 1687 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 231]---> Sorter-cost: 1687 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 229]---> Sorter-cost: 1687 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 227]---> Sorter-cost: 1687 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 225]---> Sorter-cost: 1687 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 223]---> Sorter-cost: 1706 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 221]---> Sorter-cost: 595 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 219]---> Sorter-cost: 604 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 217]---> Sorter-cost: 1706 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 215]---> Sorter-cost: 1706 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 213]---> Sorter-cost: 1706 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 211]---> Sorter-cost: 1706 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 209]---> Sorter-cost: 1706 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 207]---> Sorter-cost: 1706 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 205]---> Sorter-cost: 604 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 203]---> BDD-cost: 216 c ---[ 201]---> Sorter-cost: 1706 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 199]---> Sorter-cost: 1687 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 197]---> Sorter-cost: 1687 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 195]---> Sorter-cost: 1687 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 193]---> Sorter-cost: 1687 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 191]---> Sorter-cost: 1687 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 189]---> Sorter-cost: 1687 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 187]---> Sorter-cost: 595 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 185]---> Sorter-cost: 586 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 183]---> Sorter-cost: 1668 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 181]---> Sorter-cost: 1668 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 179]---> Sorter-cost: 1706 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 177]---> Sorter-cost: 1668 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 175]---> Sorter-cost: 1668 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 173]---> Sorter-cost: 1668 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 171]---> Sorter-cost: 1668 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 169]---> Sorter-cost: 586 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 168]---> Sorter-cost: 2360 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 167]---> Sorter-cost: 2360 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 166]---> Sorter-cost: 2360 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 165]---> Sorter-cost: 2360 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 164]---> Sorter-cost: 2360 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 162]---> Sorter-cost: 1706 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 161]---> Sorter-cost: 2360 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 160]---> Sorter-cost: 2360 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 159]---> Sorter-cost: 2360 Base: 2 2 2 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: 604 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 149]---> BDD-cost: 8 c ---[ 148]---> BDD-cost: 22 c ---[ 147]---> BDD-cost: 22 c ---[ 146]---> BDD-cost: 22 c ---[ 145]---> BDD-cost: 22 c ---[ 144]---> BDD-cost: 22 c ---[ 143]---> BDD-cost: 22 c ---[ 142]---> BDD-cost: 22 c ---[ 141]---> BDD-cost: 22 c ---[ 140]---> BDD-cost: 9 c ---[ 138]---> Sorter-cost: 595 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 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: 26 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: 59 c ---[ 108]---> BDD-cost: 230 c ---[ 107]---> BDD-cost: 54 c ---[ 106]---> BDD-cost: 221 c ---[ 105]---> BDD-cost: 57 c ---[ 104]---> BDD-cost: 218 c ---[ 103]---> BDD-cost: 47 c ---[ 102]---> BDD-cost: 200 c ---[ 101]---> BDD-cost: 53 c ---[ 100]---> BDD-cost: 194 c ---[ 99]---> BDD-cost: 5 c ---[ 98]---> BDD-cost: 82 c ---[ 97]---> BDD-cost: 3 c ---[ 96]---> BDD-cost: 71 c ---[ 95]---> BDD-cost: 50 c ---[ 94]---> BDD-cost: 185 c ---[ 93]---> BDD-cost: 54 c ---[ 92]---> BDD-cost: 209 c ---[ 91]---> BDD-cost: 49 c ---[ 90]---> BDD-cost: 200 c ---[ 89]---> BDD-cost: 44 c ---[ 88]---> BDD-cost: 191 c ---[ 87]---> BDD-cost: 50 c ---[ 86]---> BDD-cost: 185 c ---[ 85]---> BDD-cost: 5 c ---[ 84]---> BDD-cost: 79 c ---[ 83]---> BDD-cost: 3 c ---[ 82]---> BDD-cost: 74 c ---[ 81]---> BDD-cost: 54 c ---[ 80]---> BDD-cost: 221 c ---[ 79]---> BDD-cost: 57 c ---[ 78]---> BDD-cost: 218 c ---[ 77]---> BDD-cost: 50 c ---[ 76]---> BDD-cost: 197 c ---[ 75]---> BDD-cost: 53 c ---[ 74]---> BDD-cost: 194 c ---[ 73]---> BDD-cost: 59 c ---[ 72]---> BDD-cost: 230 c ---[ 71]---> BDD-cost: 3 c ---[ 70]---> BDD-cost: 70 c ---[ 69]---> BDD-cost: 57 c ---[ 68]---> BDD-cost: 218 c ---[ 67]---> BDD-cost: 57 c ---[ 66]---> BDD-cost: 218 c ---[ 65]---> BDD-cost: 64 c ---[ 64]---> BDD-cost: 236 c ---[ 63]---> BDD-cost: 56 c ---[ 62]---> BDD-cost: 188 c ---[ 61]---> BDD-cost: 59 c ---[ 60]---> BDD-cost: 230 c ---[ 59]---> BDD-cost: 57 c ---[ 58]---> BDD-cost: 218 c ---[ 57]---> BDD-cost: 5 c ---[ 56]---> BDD-cost: 82 c ---[ 55]---> BDD-cost: 5 c ---[ 54]---> BDD-cost: 79 c ---[ 53]---> BDD-cost: 47 c ---[ 52]---> BDD-cost: 188 c ---[ 51]---> BDD-cost: 50 c ---[ 50]---> BDD-cost: 185 c ---[ 49]---> BDD-cost: 44 c ---[ 48]---> BDD-cost: 191 c ---[ 47]---> BDD-cost: 44 c ---[ 46]---> BDD-cost: 191 c ---[ 45]---> BDD-cost: 47 c ---[ 44]---> BDD-cost: 188 c ---[ 43]---> BDD-cost: 3 c ---[ 42]---> BDD-cost: 73 c ---[ 41]---> BDD-cost: 6 c ---[ 40]---> BDD-cost: 87 c ---[ 39]---> BDD-cost: 50 c ---[ 38]---> BDD-cost: 197 c ---[ 37]---> BDD-cost: 50 c ---[ 36]---> BDD-cost: 197 c ---[ 35]---> BDD-cost: 50 c ---[ 34]---> BDD-cost: 197 c ---[ 33]---> BDD-cost: 57 c ---[ 32]---> BDD-cost: 218 c ---[ 31]---> BDD-cost: 47 c ---[ 30]---> BDD-cost: 200 c ---[ 29]---> BDD-cost: 50 c ---[ 28]---> BDD-cost: 197 c ---[ 27]---> BDD-cost: 5 c ---[ 26]---> BDD-cost: 84 c ---[ 25]---> BDD-cost: 47 c ---[ 24]---> BDD-cost: 188 c ---[ 23]---> BDD-cost: 54 c ---[ 22]---> BDD-cost: 209 c ---[ 21]---> BDD-cost: 44 c ---[ 20]---> BDD-cost: 191 c ---[ 19]---> BDD-cost: 47 c ---[ 18]---> BDD-cost: 188 c ---[ 17]---> BDD-cost: 52 c ---[ 16]---> BDD-cost: 197 c ---[ 15]---> BDD-cost: 50 c ---[ 14]---> BDD-cost: 185 c ---[ 13]---> BDD-cost: 3 c ---[ 12]---> BDD-cost: 69 c ---[ 11]---> BDD-cost: 3 c ---[ 10]---> BDD-cost: 68 c ---[ 9]---> BDD-cost: 47 c ---[ 8]---> BDD-cost: 176 c ---[ 7]---> BDD-cost: 44 c ---[ 6]---> BDD-cost: 179 c ---[ 5]---> BDD-cost: 44 c ---[ 4]---> BDD-cost: 179 c ---[ 3]---> BDD-cost: 47 c ---[ 2]---> BDD-cost: 176 c ---[ 1]---> BDD-cost: 4 c ---[ 0]---> BDD-cost: 71 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 0 | 293828 708752 | 97942 0 0 nan | 0.000 % | c | 102 | 293828 708752 | 107736 102 1729 17.0 | 5.437 % | c | 252 | 293580 708205 | 118509 205 2048 10.0 | 5.506 % | c | 477 | 293283 707547 | 130360 379 2708 7.1 | 5.588 % | c | 814 | 292918 706734 | 143396 663 3741 5.6 | 5.685 % | c | 1320 | 292567 705955 | 157736 1112 5656 5.1 | 5.778 % | c | 2079 | 292264 705281 | 173510 1823 8280 4.5 | 5.859 % | c | 3218 | 291104 702687 | 190861 2795 11659 4.2 | 6.160 % | c | 4926 | 290177 700612 | 209947 4382 17505 4.0 | 6.400 % | c | 7488 | 289431 698939 | 230942 6835 28361 4.1 | 6.590 % | c | 11332 | 288000 695744 | 254036 10480 45363 4.3 | 6.961 % | c | 17098 | 285661 690509 | 279439 15921 69297 4.4 | 7.565 % | c | 25747 | 284320 687510 | 307383 24371 121941 5.0 | 7.913 % | c | 38721 | 282947 684426 | 338122 37163 203491 5.5 | 8.263 % | c | 58182 | 281504 681186 | 371934 56426 329775 5.8 | 8.630 % | c | 87375 | 280774 679550 | 409128 85513 594418 7.0 | 8.818 % | c | 131164 | 280133 678112 | 450040 129227 1122688 8.7 | 8.980 % | c | 196849 | 279930 677656 | 495044 194867 2298140 11.8 | 9.037 % | c | 295375 | 279694 677128 | 544549 293374 4559670 15.5 | 9.097 % |
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/3247/stat): 3247 (minisat+_script) R 3246 3247 22582 0 -1 0 19 0 0 0 0 0 0 0 23 0 1 0 1788597116 712704 3 4294967295 134512640 135087896 3221224496 3221224496 1073744960 0 0 5 0 0 0 0 17 0 0 0 Raw data (/proc/3247/statm): 174 3 169 147 0 27 0 [pid=3247] 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=3248 New process pid=3249 New process pid=3250 execve syscall for /bin/sed executable One traced child (pid=3249) 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=3250) exited with status: 0 One traced child (pid=3248) exited with status: 0 New process pid=3251 execve syscall for /oldhome/oroussel/solvers/minisat+_64-bit_static executable open syscall for file /dev/null open syscall for file /oldhome/oroussel/tmp/wulflinc10/normalized-mps-v2-20-10-pp08aCUTS.opb [startup+10.0032 s] Raw data (loadavg): 0.93 0.95 0.98 2/57 3251 Raw data (/proc/3247/stat): 3247 (minisat+_script) S 3246 3247 22582 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788597116 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/3247/statm): 531 226 485 147 0 384 0 [pid=3247] vsize: 2124 Raw data (/proc/3251/stat): 3251 (minisat+_64-bit) R 3247 3247 22582 0 -1 0 9171 0 0 0 924 37 0 0 25 0 1 0 1788597121 39129088 8835 4294967295 134512640 135094434 3221224432 3221223092 134553530 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/3251/statm): 9553 8835 145 145 0 9408 0 [pid=3251] vsize: 38212 Current children cumulated CPU time (s) 9.62 Current children cumulated vsize (Kb) 40336 [startup+20.0037 s] Raw data (loadavg): 0.94 0.95 0.98 2/57 3251 Raw data (/proc/3247/stat): 3247 (minisat+_script) S 3246 3247 22582 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788597116 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/3247/statm): 531 226 485 147 0 384 0 [pid=3247] vsize: 2124 Raw data (/proc/3251/stat): 3251 (minisat+_64-bit) R 3247 3247 22582 0 -1 0 9215 0 0 0 1922 38 0 0 25 0 1 0 1788597121 39305216 8879 4294967295 134512640 135094434 3221224432 3221223092 134553482 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/3251/statm): 9596 8879 145 145 0 9451 0 [pid=3251] vsize: 38384 Current children cumulated CPU time (s) 19.61 Current children cumulated vsize (Kb) 40508 [startup+30.0043 s] Raw data (loadavg): 0.95 0.96 0.98 2/57 3251 Raw data (/proc/3247/stat): 3247 (minisat+_script) S 3246 3247 22582 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788597116 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/3247/statm): 531 226 485 147 0 384 0 [pid=3247] vsize: 2124 Raw data (/proc/3251/stat): 3251 (minisat+_64-bit) R 3247 3247 22582 0 -1 0 9221 0 0 0 2922 38 0 0 25 0 1 0 1788597121 39325696 8885 4294967295 134512640 135094434 3221224432 3221223088 134557917 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/3251/statm): 9601 8885 145 145 0 9456 0 [pid=3251] vsize: 38404 Current children cumulated CPU time (s) 29.61 Current children cumulated vsize (Kb) 40528 [startup+40.0049 s] Raw data (loadavg): 0.96 0.96 0.98 2/57 3251 Raw data (/proc/3247/stat): 3247 (minisat+_script) S 3246 3247 22582 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788597116 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/3247/statm): 531 226 485 147 0 384 0 [pid=3247] vsize: 2124 Raw data (/proc/3251/stat): 3251 (minisat+_64-bit) R 3247 3247 22582 0 -1 0 9253 0 0 0 3922 38 0 0 25 0 1 0 1788597121 39448576 8917 4294967295 134512640 135094434 3221224432 3221223072 134562085 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/3251/statm): 9631 8917 145 145 0 9486 0 [pid=3251] vsize: 38524 Current children cumulated CPU time (s) 39.61 Current children cumulated vsize (Kb) 40648 [startup+50.0054 s] Raw data (loadavg): 0.96 0.96 0.98 2/57 3251 Raw data (/proc/3247/stat): 3247 (minisat+_script) S 3246 3247 22582 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788597116 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/3247/statm): 531 226 485 147 0 384 0 [pid=3247] vsize: 2124 Raw data (/proc/3251/stat): 3251 (minisat+_64-bit) R 3247 3247 22582 0 -1 0 9287 0 0 0 4921 39 0 0 25 0 1 0 1788597121 39596032 8951 4294967295 134512640 135094434 3221224432 3221223136 134559017 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/3251/statm): 9667 8951 145 145 0 9522 0 [pid=3251] vsize: 38668 Current children cumulated CPU time (s) 49.61 Current children cumulated vsize (Kb) 40792 [startup+60.006 s] Raw data (loadavg): 0.97 0.96 0.98 2/57 3251 Raw data (/proc/3247/stat): 3247 (minisat+_script) S 3246 3247 22582 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788597116 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/3247/statm): 531 226 485 147 0 384 0 [pid=3247] vsize: 2124 Raw data (/proc/3251/stat): 3251 (minisat+_64-bit) R 3247 3247 22582 0 -1 0 9309 0 0 0 5920 39 0 0 25 0 1 0 1788597121 39645184 8973 4294967295 134512640 135094434 3221224432 3221223092 134553446 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/3251/statm): 9679 8973 145 145 0 9534 0 [pid=3251] vsize: 38716 Current children cumulated CPU time (s) 59.6 Current children cumulated vsize (Kb) 40840 [startup+70.0066 s] Raw data (loadavg): 0.97 0.96 0.98 2/57 3251 Raw data (/proc/3247/stat): 3247 (minisat+_script) S 3246 3247 22582 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788597116 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/3247/statm): 531 226 485 147 0 384 0 [pid=3247] vsize: 2124 Raw data (/proc/3251/stat): 3251 (minisat+_64-bit) R 3247 3247 22582 0 -1 0 9327 0 0 0 6919 39 0 0 25 0 1 0 1788597121 39694336 8991 4294967295 134512640 135094434 3221224432 3221223044 134563069 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/3251/statm): 9691 8991 145 145 0 9546 0 [pid=3251] vsize: 38764 Current children cumulated CPU time (s) 69.59 Current children cumulated vsize (Kb) 40888 [startup+80.0081 s] Raw data (loadavg): 0.98 0.96 0.98 2/57 3251 Raw data (/proc/3247/stat): 3247 (minisat+_script) S 3246 3247 22582 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788597116 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/3247/statm): 531 226 485 147 0 384 0 [pid=3247] vsize: 2124 Raw data (/proc/3251/stat): 3251 (minisat+_64-bit) R 3247 3247 22582 0 -1 0 9351 0 0 0 7919 40 0 0 25 0 1 0 1788597121 39776256 9015 4294967295 134512640 135094434 3221224432 3221223044 134563030 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/3251/statm): 9711 9015 145 145 0 9566 0 [pid=3251] vsize: 38844 Current children cumulated CPU time (s) 79.6 Current children cumulated vsize (Kb) 40968 [startup+90.0087 s] Raw data (loadavg): 0.98 0.96 0.98 2/57 3251 Raw data (/proc/3247/stat): 3247 (minisat+_script) S 3246 3247 22582 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788597116 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/3247/statm): 531 226 485 147 0 384 0 [pid=3247] vsize: 2124 Raw data (/proc/3251/stat): 3251 (minisat+_64-bit) R 3247 3247 22582 0 -1 0 9373 0 0 0 8919 40 0 0 25 0 1 0 1788597121 39849984 9037 4294967295 134512640 135094434 3221224432 3221223044 134563055 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/3251/statm): 9729 9037 145 145 0 9584 0 [pid=3251] vsize: 38916 Current children cumulated CPU time (s) 89.6 Current children cumulated vsize (Kb) 41040 [startup+100.008 s] Raw data (loadavg): 0.98 0.96 0.98 2/57 3251 Raw data (/proc/3247/stat): 3247 (minisat+_script) S 3246 3247 22582 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788597116 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/3247/statm): 531 226 485 147 0 384 0 [pid=3247] vsize: 2124 Raw data (/proc/3251/stat): 3251 (minisat+_64-bit) R 3247 3247 22582 0 -1 0 9403 0 0 0 9918 40 0 0 25 0 1 0 1788597121 39993344 9067 4294967295 134512640 135094434 3221224432 3221223056 134557565 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/3251/statm): 9764 9067 145 145 0 9619 0 [pid=3251] vsize: 39056 Current children cumulated CPU time (s) 99.59 Current children cumulated vsize (Kb) 41180 [startup+110.009 s] Raw data (loadavg): 1.06 0.98 0.98 2/57 3251 Raw data (/proc/3247/stat): 3247 (minisat+_script) S 3246 3247 22582 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788597116 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/3247/statm): 531 226 485 147 0 384 0 [pid=3247] vsize: 2124 Raw data (/proc/3251/stat): 3251 (minisat+_64-bit) R 3247 3247 22582 0 -1 0 9436 0 0 0 10918 41 0 0 25 0 1 0 1788597121 40116224 9100 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/3251/statm): 9794 9100 145 145 0 9649 0 [pid=3251] vsize: 39176 Current children cumulated CPU time (s) 109.6 Current children cumulated vsize (Kb) 41300 [startup+120.009 s] Raw data (loadavg): 1.05 0.98 0.98 2/57 3251 Raw data (/proc/3247/stat): 3247 (minisat+_script) S 3246 3247 22582 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788597116 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/3247/statm): 531 226 485 147 0 384 0 [pid=3247] vsize: 2124 Raw data (/proc/3251/stat): 3251 (minisat+_64-bit) R 3247 3247 22582 0 -1 0 9471 0 0 0 11918 41 0 0 25 0 1 0 1788597121 40251392 9135 4294967295 134512640 135094434 3221224432 3221223044 134563049 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/3251/statm): 9827 9135 145 145 0 9682 0 [pid=3251] vsize: 39308 Current children cumulated CPU time (s) 119.6 Current children cumulated vsize (Kb) 41432 [startup+130.01 s] Raw data (loadavg): 1.04 0.98 0.98 2/57 3251 Raw data (/proc/3247/stat): 3247 (minisat+_script) S 3246 3247 22582 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788597116 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/3247/statm): 531 226 485 147 0 384 0 [pid=3247] vsize: 2124 Raw data (/proc/3251/stat): 3251 (minisat+_64-bit) R 3247 3247 22582 0 -1 0 9510 0 0 0 12917 41 0 0 25 0 1 0 1788597121 40398848 9174 4294967295 134512640 135094434 3221224432 3221223072 134562070 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/3251/statm): 9863 9174 145 145 0 9718 0 [pid=3251] vsize: 39452 Current children cumulated CPU time (s) 129.59 Current children cumulated vsize (Kb) 41576 [startup+140.01 s] Raw data (loadavg): 1.04 0.98 0.98 2/57 3251 Raw data (/proc/3247/stat): 3247 (minisat+_script) S 3246 3247 22582 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788597116 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/3247/statm): 531 226 485 147 0 384 0 [pid=3247] vsize: 2124 Raw data (/proc/3251/stat): 3251 (minisat+_64-bit) R 3247 3247 22582 0 -1 0 9535 0 0 0 13917 41 0 0 25 0 1 0 1788597121 40488960 9199 4294967295 134512640 135094434 3221224432 3221223092 134553446 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/3251/statm): 9885 9199 145 145 0 9740 0 [pid=3251] vsize: 39540 Current children cumulated CPU time (s) 139.59 Current children cumulated vsize (Kb) 41664 [startup+150.011 s] Raw data (loadavg): 1.03 0.98 0.98 2/57 3251 Raw data (/proc/3247/stat): 3247 (minisat+_script) S 3246 3247 22582 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788597116 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/3247/statm): 531 226 485 147 0 384 0 [pid=3247] vsize: 2124 Raw data (/proc/3251/stat): 3251 (minisat+_64-bit) R 3247 3247 22582 0 -1 0 9563 0 0 0 14916 42 0 0 25 0 1 0 1788597121 40595456 9227 4294967295 134512640 135094434 3221224432 3221223044 134563087 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/3251/statm): 9911 9227 145 145 0 9766 0 [pid=3251] vsize: 39644 Current children cumulated CPU time (s) 149.59 Current children cumulated vsize (Kb) 41768 [startup+160.012 s] Raw data (loadavg): 1.03 0.98 0.98 2/57 3251 Raw data (/proc/3247/stat): 3247 (minisat+_script) S 3246 3247 22582 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788597116 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/3247/statm): 531 226 485 147 0 384 0 [pid=3247] vsize: 2124 Raw data (/proc/3251/stat): 3251 (minisat+_64-bit) R 3247 3247 22582 0 -1 0 9612 0 0 0 15916 42 0 0 25 0 1 0 1788597121 40919040 9276 4294967295 134512640 135094434 3221224432 3221223072 134562068 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/3251/statm): 9990 9276 145 145 0 9845 0 [pid=3251] vsize: 39960 Current children cumulated CPU time (s) 159.59 Current children cumulated vsize (Kb) 42084 [startup+170.012 s] Raw data (loadavg): 1.02 0.98 0.98 2/57 3251 Raw data (/proc/3247/stat): 3247 (minisat+_script) S 3246 3247 22582 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788597116 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/3247/statm): 531 226 485 147 0 384 0 [pid=3247] vsize: 2124 Raw data (/proc/3251/stat): 3251 (minisat+_64-bit) R 3247 3247 22582 0 -1 0 9632 0 0 0 16916 42 0 0 25 0 1 0 1788597121 40988672 9296 4294967295 134512640 135094434 3221224432 3221223088 134558159 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/3251/statm): 10007 9296 145 145 0 9862 0 [pid=3251] vsize: 40028 Current children cumulated CPU time (s) 169.59 Current children cumulated vsize (Kb) 42152 [startup+180.013 s] Raw data (loadavg): 1.02 0.98 0.98 2/57 3251 Raw data (/proc/3247/stat): 3247 (minisat+_script) S 3246 3247 22582 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788597116 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/3247/statm): 531 226 485 147 0 384 0 [pid=3247] vsize: 2124 Raw data (/proc/3251/stat): 3251 (minisat+_64-bit) R 3247 3247 22582 0 -1 0 9665 0 0 0 17916 43 0 0 25 0 1 0 1788597121 41115648 9329 4294967295 134512640 135094434 3221224432 3221223092 134553482 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/3251/statm): 10038 9329 145 145 0 9893 0 [pid=3251] vsize: 40152 Current children cumulated CPU time (s) 179.6 Current children cumulated vsize (Kb) 42276 [startup+190.013 s] Raw data (loadavg): 1.01 0.98 0.98 2/57 3251 Raw data (/proc/3247/stat): 3247 (minisat+_script) S 3246 3247 22582 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788597116 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/3247/statm): 531 226 485 147 0 384 0 [pid=3247] vsize: 2124 Raw data (/proc/3251/stat): 3251 (minisat+_64-bit) R 3247 3247 22582 0 -1 0 9698 0 0 0 18915 43 0 0 25 0 1 0 1788597121 41238528 9362 4294967295 134512640 135094434 3221224432 3221223044 134563059 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/3251/statm): 10068 9362 145 145 0 9923 0 [pid=3251] vsize: 40272 Current children cumulated CPU time (s) 189.59 Current children cumulated vsize (Kb) 42396 [startup+200.014 s] Raw data (loadavg): 1.01 0.98 0.98 2/57 3251 Raw data (/proc/3247/stat): 3247 (minisat+_script) S 3246 3247 22582 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788597116 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/3247/statm): 531 226 485 147 0 384 0 [pid=3247] vsize: 2124 Raw data (/proc/3251/stat): 3251 (minisat+_64-bit) R 3247 3247 22582 0 -1 0 9724 0 0 0 19914 44 0 0 25 0 1 0 1788597121 41336832 9388 4294967295 134512640 135094434 3221224432 3221223044 134563049 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/3251/statm): 10092 9388 145 145 0 9947 0 [pid=3251] vsize: 40368 Current children cumulated CPU time (s) 199.59 Current children cumulated vsize (Kb) 42492 [startup+210.014 s] Raw data (loadavg): 1.01 0.98 0.98 2/57 3251 Raw data (/proc/3247/stat): 3247 (minisat+_script) S 3246 3247 22582 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788597116 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/3247/statm): 531 226 485 147 0 384 0 [pid=3247] vsize: 2124 Raw data (/proc/3251/stat): 3251 (minisat+_64-bit) R 3247 3247 22582 0 -1 0 9756 0 0 0 20913 44 0 0 25 0 1 0 1788597121 41447424 9420 4294967295 134512640 135094434 3221224432 3221223044 134563121 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/3251/statm): 10119 9420 145 145 0 9974 0 [pid=3251] vsize: 40476 Current children cumulated CPU time (s) 209.58 Current children cumulated vsize (Kb) 42600 [startup+220.015 s] Raw data (loadavg): 1.01 0.98 0.98 2/57 3251 Raw data (/proc/3247/stat): 3247 (minisat+_script) S 3246 3247 22582 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788597116 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/3247/statm): 531 226 485 147 0 384 0 [pid=3247] vsize: 2124 Raw data (/proc/3251/stat): 3251 (minisat+_64-bit) R 3247 3247 22582 0 -1 0 9783 0 0 0 21913 44 0 0 25 0 1 0 1788597121 41549824 9447 4294967295 134512640 135094434 3221224432 3221223044 134563094 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/3251/statm): 10144 9447 145 145 0 9999 0 [pid=3251] vsize: 40576 Current children cumulated CPU time (s) 219.58 Current children cumulated vsize (Kb) 42700 [startup+230.016 s] Raw data (loadavg): 1.01 0.98 0.98 2/57 3251 Raw data (/proc/3247/stat): 3247 (minisat+_script) S 3246 3247 22582 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788597116 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/3247/statm): 531 226 485 147 0 384 0 [pid=3247] vsize: 2124 Raw data (/proc/3251/stat): 3251 (minisat+_64-bit) R 3247 3247 22582 0 -1 0 9822 0 0 0 22913 45 0 0 25 0 1 0 1788597121 41693184 9486 4294967295 134512640 135094434 3221224432 3221223136 134559005 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/3251/statm): 10179 9486 145 145 0 10034 0 [pid=3251] vsize: 40716 Current children cumulated CPU time (s) 229.59 Current children cumulated vsize (Kb) 42840 [startup+240.016 s] Raw data (loadavg): 1.00 0.98 0.98 2/57 3251 Raw data (/proc/3247/stat): 3247 (minisat+_script) S 3246 3247 22582 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788597116 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/3247/statm): 531 226 485 147 0 384 0 [pid=3247] vsize: 2124 Raw data (/proc/3251/stat): 3251 (minisat+_64-bit) R 3247 3247 22582 0 -1 0 9861 0 0 0 23913 45 0 0 25 0 1 0 1788597121 41844736 9525 4294967295 134512640 135094434 3221224432 3221223088 134558164 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/3251/statm): 10216 9525 145 145 0 10071 0 [pid=3251] vsize: 40864 Current children cumulated CPU time (s) 239.59 Current children cumulated vsize (Kb) 42988 [startup+250.016 s] Raw data (loadavg): 1.00 0.98 0.98 2/57 3251 Raw data (/proc/3247/stat): 3247 (minisat+_script) S 3246 3247 22582 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788597116 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/3247/statm): 531 226 485 147 0 384 0 [pid=3247] vsize: 2124 Raw data (/proc/3251/stat): 3251 (minisat+_64-bit) R 3247 3247 22582 0 -1 0 9887 0 0 0 24912 45 0 0 25 0 1 0 1788597121 41943040 9551 4294967295 134512640 135094434 3221224432 3221223136 134559013 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/3251/statm): 10240 9551 145 145 0 10095 0 [pid=3251] vsize: 40960 Current children cumulated CPU time (s) 249.58 Current children cumulated vsize (Kb) 43084 [startup+260.016 s] Raw data (loadavg): 1.00 0.98 0.98 2/57 3251 Raw data (/proc/3247/stat): 3247 (minisat+_script) S 3246 3247 22582 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788597116 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/3247/statm): 531 226 485 147 0 384 0 [pid=3247] vsize: 2124 Raw data (/proc/3251/stat): 3251 (minisat+_64-bit) R 3247 3247 22582 0 -1 0 9916 0 0 0 25911 46 0 0 25 0 1 0 1788597121 42053632 9580 4294967295 134512640 135094434 3221224432 3221223064 134557561 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/3251/statm): 10267 9580 145 145 0 10122 0 [pid=3251] vsize: 41068 Current children cumulated CPU time (s) 259.58 Current children cumulated vsize (Kb) 43192 [startup+270.017 s] Raw data (loadavg): 1.00 0.98 0.98 2/57 3251 Raw data (/proc/3247/stat): 3247 (minisat+_script) S 3246 3247 22582 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788597116 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/3247/statm): 531 226 485 147 0 384 0 [pid=3247] vsize: 2124 Raw data (/proc/3251/stat): 3251 (minisat+_64-bit) R 3247 3247 22582 0 -1 0 9947 0 0 0 26911 46 0 0 25 0 1 0 1788597121 42172416 9611 4294967295 134512640 135094434 3221224432 3221223120 134554746 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/3251/statm): 10296 9611 145 145 0 10151 0 [pid=3251] vsize: 41184 Current children cumulated CPU time (s) 269.58 Current children cumulated vsize (Kb) 43308 [startup+280.017 s] Raw data (loadavg): 1.00 0.98 0.98 2/57 3251 Raw data (/proc/3247/stat): 3247 (minisat+_script) S 3246 3247 22582 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788597116 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/3247/statm): 531 226 485 147 0 384 0 [pid=3247] vsize: 2124 Raw data (/proc/3251/stat): 3251 (minisat+_64-bit) R 3247 3247 22582 0 -1 0 9974 0 0 0 27911 46 0 0 25 0 1 0 1788597121 42274816 9638 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/3251/statm): 10321 9638 145 145 0 10176 0 [pid=3251] vsize: 41284 Current children cumulated CPU time (s) 279.58 Current children cumulated vsize (Kb) 43408 [startup+290.018 s] Raw data (loadavg): 1.00 0.98 0.98 2/57 3251 Raw data (/proc/3247/stat): 3247 (minisat+_script) S 3246 3247 22582 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788597116 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/3247/statm): 531 226 485 147 0 384 0 [pid=3247] vsize: 2124 Raw data (/proc/3251/stat): 3251 (minisat+_64-bit) R 3247 3247 22582 0 -1 0 10005 0 0 0 28911 46 0 0 25 0 1 0 1788597121 42393600 9669 4294967295 134512640 135094434 3221224432 3221223136 134554538 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/3251/statm): 10350 9669 145 145 0 10205 0 [pid=3251] vsize: 41400 Current children cumulated CPU time (s) 289.58 Current children cumulated vsize (Kb) 43524 [startup+300.017 s] Raw data (loadavg): 1.00 0.98 0.98 2/57 3251 Raw data (/proc/3247/stat): 3247 (minisat+_script) S 3246 3247 22582 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788597116 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/3247/statm): 531 226 485 147 0 384 0 [pid=3247] vsize: 2124 Raw data (/proc/3251/stat): 3251 (minisat+_64-bit) R 3247 3247 22582 0 -1 0 10039 0 0 0 29910 47 0 0 25 0 1 0 1788597121 42786816 9703 4294967295 134512640 135094434 3221224432 3221223044 134563061 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/3251/statm): 10446 9703 145 145 0 10301 0 [pid=3251] vsize: 41784 Current children cumulated CPU time (s) 299.58 Current children cumulated vsize (Kb) 43908 [startup+310.018 s] Raw data (loadavg): 1.00 0.98 0.98 2/57 3251 Raw data (/proc/3247/stat): 3247 (minisat+_script) S 3246 3247 22582 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788597116 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/3247/statm): 531 226 485 147 0 384 0 [pid=3247] vsize: 2124 Raw data (/proc/3251/stat): 3251 (minisat+_64-bit) R 3247 3247 22582 0 -1 0 10071 0 0 0 30910 47 0 0 25 0 1 0 1788597121 42909696 9735 4294967295 134512640 135094434 3221224432 3221223092 134553446 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/3251/statm): 10476 9735 145 145 0 10331 0 [pid=3251] vsize: 41904 Current children cumulated CPU time (s) 309.58 Current children cumulated vsize (Kb) 44028 [startup+320.019 s] Raw data (loadavg): 1.00 0.98 0.98 2/57 3251 Raw data (/proc/3247/stat): 3247 (minisat+_script) S 3246 3247 22582 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788597116 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/3247/statm): 531 226 485 147 0 384 0 [pid=3247] vsize: 2124 Raw data (/proc/3251/stat): 3251 (minisat+_64-bit) R 3247 3247 22582 0 -1 0 10107 0 0 0 31909 47 0 0 25 0 1 0 1788597121 43044864 9771 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/3251/statm): 10509 9771 145 145 0 10364 0 [pid=3251] vsize: 42036 Current children cumulated CPU time (s) 319.57 Current children cumulated vsize (Kb) 44160 [startup+330.02 s] Raw data (loadavg): 1.00 0.98 0.98 2/57 3251 Raw data (/proc/3247/stat): 3247 (minisat+_script) S 3246 3247 22582 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788597116 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/3247/statm): 531 226 485 147 0 384 0 [pid=3247] vsize: 2124 Raw data (/proc/3251/stat): 3251 (minisat+_64-bit) R 3247 3247 22582 0 -1 0 10154 0 0 0 32909 47 0 0 25 0 1 0 1788597121 43229184 9818 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/3251/statm): 10554 9818 145 145 0 10409 0 [pid=3251] vsize: 42216 Current children cumulated CPU time (s) 329.57 Current children cumulated vsize (Kb) 44340 [startup+340.021 s] Raw data (loadavg): 1.00 0.98 0.98 2/57 3251 Raw data (/proc/3247/stat): 3247 (minisat+_script) S 3246 3247 22582 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788597116 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/3247/statm): 531 226 485 147 0 384 0 [pid=3247] vsize: 2124 Raw data (/proc/3251/stat): 3251 (minisat+_64-bit) R 3247 3247 22582 0 -1 0 10212 0 0 0 33908 48 0 0 25 0 1 0 1788597121 43454464 9876 4294967295 134512640 135094434 3221224432 3221223068 134557560 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/3251/statm): 10609 9876 145 145 0 10464 0 [pid=3251] vsize: 42436 Current children cumulated CPU time (s) 339.57 Current children cumulated vsize (Kb) 44560 [startup+350.021 s] Raw data (loadavg): 1.00 0.98 0.98 2/57 3251 Raw data (/proc/3247/stat): 3247 (minisat+_script) S 3246 3247 22582 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788597116 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/3247/statm): 531 226 485 147 0 384 0 [pid=3247] vsize: 2124 Raw data (/proc/3251/stat): 3251 (minisat+_64-bit) R 3247 3247 22582 0 -1 0 10268 0 0 0 34907 48 0 0 25 0 1 0 1788597121 43671552 9932 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/3251/statm): 10662 9932 145 145 0 10517 0 [pid=3251] vsize: 42648 Current children cumulated CPU time (s) 349.56 Current children cumulated vsize (Kb) 44772 [startup+360.022 s] Raw data (loadavg): 1.00 0.98 0.98 2/57 3251 Raw data (/proc/3247/stat): 3247 (minisat+_script) S 3246 3247 22582 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788597116 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/3247/statm): 531 226 485 147 0 384 0 [pid=3247] vsize: 2124 Raw data (/proc/3251/stat): 3251 (minisat+_64-bit) R 3247 3247 22582 0 -1 0 10348 0 0 0 35905 49 0 0 25 0 1 0 1788597121 43982848 10012 4294967295 134512640 135094434 3221224432 3221223088 134558426 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/3251/statm): 10738 10012 145 145 0 10593 0 [pid=3251] vsize: 42952 Current children cumulated CPU time (s) 359.55 Current children cumulated vsize (Kb) 45076 [startup+370.021 s] Raw data (loadavg): 1.00 0.98 0.98 2/57 3251 Raw data (/proc/3247/stat): 3247 (minisat+_script) S 3246 3247 22582 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788597116 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/3247/statm): 531 226 485 147 0 384 0 [pid=3247] vsize: 2124 Raw data (/proc/3251/stat): 3251 (minisat+_64-bit) R 3247 3247 22582 0 -1 0 10384 0 0 0 36905 49 0 0 25 0 1 0 1788597121 44122112 10048 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/3251/statm): 10772 10048 145 145 0 10627 0 [pid=3251] vsize: 43088 Current children cumulated CPU time (s) 369.55 Current children cumulated vsize (Kb) 45212 [startup+380.023 s] Raw data (loadavg): 1.00 0.98 0.98 2/57 3251 Raw data (/proc/3247/stat): 3247 (minisat+_script) S 3246 3247 22582 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788597116 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/3247/statm): 531 226 485 147 0 384 0 [pid=3247] vsize: 2124 Raw data (/proc/3251/stat): 3251 (minisat+_64-bit) R 3247 3247 22582 0 -1 0 10474 0 0 0 37904 50 0 0 25 0 1 0 1788597121 44478464 10138 4294967295 134512640 135094434 3221224432 3221223120 134554746 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/3251/statm): 10859 10138 145 145 0 10714 0 [pid=3251] vsize: 43436 Current children cumulated CPU time (s) 379.55 Current children cumulated vsize (Kb) 45560 [startup+390.024 s] Raw data (loadavg): 1.00 0.98 0.98 2/57 3251 Raw data (/proc/3247/stat): 3247 (minisat+_script) S 3246 3247 22582 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788597116 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/3247/statm): 531 226 485 147 0 384 0 [pid=3247] vsize: 2124 Raw data (/proc/3251/stat): 3251 (minisat+_64-bit) R 3247 3247 22582 0 -1 0 10520 0 0 0 38903 50 0 0 25 0 1 0 1788597121 44650496 10184 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/3251/statm): 10901 10184 145 145 0 10756 0 [pid=3251] vsize: 43604 Current children cumulated CPU time (s) 389.54 Current children cumulated vsize (Kb) 45728 [startup+400.024 s] Raw data (loadavg): 1.00 0.98 0.98 1/57 3251 Raw data (/proc/3247/stat): 3247 (minisat+_script) S 3246 3247 22582 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788597116 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/3247/statm): 531 226 485 147 0 384 0 [pid=3247] vsize: 2124 Raw data (/proc/3251/stat): 3251 (minisat+_64-bit) T 3247 3247 22582 0 -1 0 10557 0 0 0 39902 50 0 0 25 0 1 0 1788597121 44793856 10221 4294967295 134512640 135094434 3221224432 3221222796 134870330 0 0 5 16386 3222434794 0 0 17 1 0 0 Raw data (/proc/3251/statm): 10936 10221 145 145 0 10791 0 [pid=3251] vsize: 43744 Current children cumulated CPU time (s) 399.53 Current children cumulated vsize (Kb) 45868 [startup+410.025 s] Raw data (loadavg): 1.00 0.98 0.98 2/57 3251 Raw data (/proc/3247/stat): 3247 (minisat+_script) S 3246 3247 22582 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788597116 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/3247/statm): 531 226 485 147 0 384 0 [pid=3247] vsize: 2124 Raw data (/proc/3251/stat): 3251 (minisat+_64-bit) R 3247 3247 22582 0 -1 0 10600 0 0 0 40902 51 0 0 25 0 1 0 1788597121 44957696 10264 4294967295 134512640 135094434 3221224432 3221223088 134558232 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/3251/statm): 10976 10264 145 145 0 10831 0 [pid=3251] vsize: 43904 Current children cumulated CPU time (s) 409.54 Current children cumulated vsize (Kb) 46028 [startup+420.024 s] Raw data (loadavg): 1.00 0.98 0.98 2/57 3251 Raw data (/proc/3247/stat): 3247 (minisat+_script) S 3246 3247 22582 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788597116 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/3247/statm): 531 226 485 147 0 384 0 [pid=3247] vsize: 2124 Raw data (/proc/3251/stat): 3251 (minisat+_64-bit) R 3247 3247 22582 0 -1 0 10660 0 0 0 41901 51 0 0 25 0 1 0 1788597121 45191168 10324 4294967295 134512640 135094434 3221224432 3221223044 134563055 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/3251/statm): 11033 10324 145 145 0 10888 0 [pid=3251] vsize: 44132 Current children cumulated CPU time (s) 419.53 Current children cumulated vsize (Kb) 46256 [startup+430.025 s] Raw data (loadavg): 1.00 0.98 0.98 2/57 3251 Raw data (/proc/3247/stat): 3247 (minisat+_script) S 3246 3247 22582 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788597116 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/3247/statm): 531 226 485 147 0 384 0 [pid=3247] vsize: 2124 Raw data (/proc/3251/stat): 3251 (minisat+_64-bit) R 3247 3247 22582 0 -1 0 10698 0 0 0 42900 52 0 0 25 0 1 0 1788597121 45338624 10362 4294967295 134512640 135094434 3221224432 3221223088 134557866 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/3251/statm): 11069 10362 145 145 0 10924 0 [pid=3251] vsize: 44276 Current children cumulated CPU time (s) 429.53 Current children cumulated vsize (Kb) 46400 [startup+440.025 s] Raw data (loadavg): 1.00 0.98 0.98 2/57 3251 Raw data (/proc/3247/stat): 3247 (minisat+_script) S 3246 3247 22582 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788597116 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/3247/statm): 531 226 485 147 0 384 0 [pid=3247] vsize: 2124 Raw data (/proc/3251/stat): 3251 (minisat+_64-bit) R 3247 3247 22582 0 -1 0 10751 0 0 0 43899 52 0 0 25 0 1 0 1788597121 45543424 10415 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/3251/statm): 11119 10415 145 145 0 10974 0 [pid=3251] vsize: 44476 Current children cumulated CPU time (s) 439.52 Current children cumulated vsize (Kb) 46600 [startup+450.026 s] Raw data (loadavg): 1.00 0.98 0.98 2/57 3251 Raw data (/proc/3247/stat): 3247 (minisat+_script) S 3246 3247 22582 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788597116 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/3247/statm): 531 226 485 147 0 384 0 [pid=3247] vsize: 2124 Raw data (/proc/3251/stat): 3251 (minisat+_64-bit) R 3247 3247 22582 0 -1 0 10792 0 0 0 44898 52 0 0 25 0 1 0 1788597121 45699072 10456 4294967295 134512640 135094434 3221224432 3221223044 134563069 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/3251/statm): 11157 10456 145 145 0 11012 0 [pid=3251] vsize: 44628 Current children cumulated CPU time (s) 449.51 Current children cumulated vsize (Kb) 46752 [startup+460.026 s] Raw data (loadavg): 1.00 0.98 0.98 2/57 3251 Raw data (/proc/3247/stat): 3247 (minisat+_script) S 3246 3247 22582 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788597116 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/3247/statm): 531 226 485 147 0 384 0 [pid=3247] vsize: 2124 Raw data (/proc/3251/stat): 3251 (minisat+_64-bit) R 3247 3247 22582 0 -1 0 10830 0 0 0 45898 52 0 0 25 0 1 0 1788597121 45846528 10494 4294967295 134512640 135094434 3221224432 3221223044 134563049 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/3251/statm): 11193 10494 145 145 0 11048 0 [pid=3251] vsize: 44772 Current children cumulated CPU time (s) 459.51 Current children cumulated vsize (Kb) 46896 [startup+470.027 s] Raw data (loadavg): 1.00 0.98 0.98 2/57 3251 Raw data (/proc/3247/stat): 3247 (minisat+_script) S 3246 3247 22582 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788597116 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/3247/statm): 531 226 485 147 0 384 0 [pid=3247] vsize: 2124 Raw data (/proc/3251/stat): 3251 (minisat+_64-bit) R 3247 3247 22582 0 -1 0 10882 0 0 0 46897 53 0 0 25 0 1 0 1788597121 46047232 10546 4294967295 134512640 135094434 3221224432 3221223084 134558255 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/3251/statm): 11242 10546 145 145 0 11097 0 [pid=3251] vsize: 44968 Current children cumulated CPU time (s) 469.51 Current children cumulated vsize (Kb) 47092 [startup+480.028 s] Raw data (loadavg): 1.00 0.98 0.98 2/57 3251 Raw data (/proc/3247/stat): 3247 (minisat+_script) S 3246 3247 22582 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788597116 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/3247/statm): 531 226 485 147 0 384 0 [pid=3247] vsize: 2124 Raw data (/proc/3251/stat): 3251 (minisat+_64-bit) R 3247 3247 22582 0 -1 0 10948 0 0 0 47896 53 0 0 25 0 1 0 1788597121 46305280 10612 4294967295 134512640 135094434 3221224432 3221223088 134557879 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/3251/statm): 11305 10612 145 145 0 11160 0 [pid=3251] vsize: 45220 Current children cumulated CPU time (s) 479.5 Current children cumulated vsize (Kb) 47344 [startup+490.028 s] Raw data (loadavg): 1.00 0.98 0.98 2/57 3251 Raw data (/proc/3247/stat): 3247 (minisat+_script) S 3246 3247 22582 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788597116 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/3247/statm): 531 226 485 147 0 384 0 [pid=3247] vsize: 2124 Raw data (/proc/3251/stat): 3251 (minisat+_64-bit) R 3247 3247 22582 0 -1 0 11022 0 0 0 48895 54 0 0 25 0 1 0 1788597121 46600192 10686 4294967295 134512640 135094434 3221224432 3221223120 134554746 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/3251/statm): 11377 10686 145 145 0 11232 0 [pid=3251] vsize: 45508 Current children cumulated CPU time (s) 489.5 Current children cumulated vsize (Kb) 47632 [startup+500.029 s] Raw data (loadavg): 1.00 0.98 0.98 2/57 3251 Raw data (/proc/3247/stat): 3247 (minisat+_script) S 3246 3247 22582 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788597116 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/3247/statm): 531 226 485 147 0 384 0 [pid=3247] vsize: 2124 Raw data (/proc/3251/stat): 3251 (minisat+_64-bit) R 3247 3247 22582 0 -1 0 11076 0 0 0 49894 54 0 0 25 0 1 0 1788597121 46809088 10740 4294967295 134512640 135094434 3221224432 3221223072 134558269 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/3251/statm): 11428 10740 145 145 0 11283 0 [pid=3251] vsize: 45712 Current children cumulated CPU time (s) 499.49 Current children cumulated vsize (Kb) 47836 [startup+510.029 s] Raw data (loadavg): 1.00 0.98 0.98 2/57 3251 Raw data (/proc/3247/stat): 3247 (minisat+_script) S 3246 3247 22582 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788597116 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/3247/statm): 531 226 485 147 0 384 0 [pid=3247] vsize: 2124 Raw data (/proc/3251/stat): 3251 (minisat+_64-bit) R 3247 3247 22582 0 -1 0 11121 0 0 0 50892 55 0 0 25 0 1 0 1788597121 46985216 10785 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/3251/statm): 11471 10785 145 145 0 11326 0 [pid=3251] vsize: 45884 Current children cumulated CPU time (s) 509.48 Current children cumulated vsize (Kb) 48008 [startup+520.03 s] Raw data (loadavg): 1.00 0.98 0.98 2/57 3251 Raw data (/proc/3247/stat): 3247 (minisat+_script) S 3246 3247 22582 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788597116 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/3247/statm): 531 226 485 147 0 384 0 [pid=3247] vsize: 2124 Raw data (/proc/3251/stat): 3251 (minisat+_64-bit) R 3247 3247 22582 0 -1 0 11221 0 0 0 51891 56 0 0 25 0 1 0 1788597121 47378432 10885 4294967295 134512640 135094434 3221224432 3221223088 134558298 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/3251/statm): 11567 10885 145 145 0 11422 0 [pid=3251] vsize: 46268 Current children cumulated CPU time (s) 519.48 Current children cumulated vsize (Kb) 48392 [startup+530.03 s] Raw data (loadavg): 1.00 0.98 0.98 2/57 3251 Raw data (/proc/3247/stat): 3247 (minisat+_script) S 3246 3247 22582 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788597116 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/3247/statm): 531 226 485 147 0 384 0 [pid=3247] vsize: 2124 Raw data (/proc/3251/stat): 3251 (minisat+_64-bit) R 3247 3247 22582 0 -1 0 11282 0 0 0 52890 56 0 0 25 0 1 0 1788597121 47616000 10946 4294967295 134512640 135094434 3221224432 3221223044 134563071 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/3251/statm): 11625 10946 145 145 0 11480 0 [pid=3251] vsize: 46500 Current children cumulated CPU time (s) 529.47 Current children cumulated vsize (Kb) 48624 [startup+540.031 s] Raw data (loadavg): 1.00 0.98 0.98 2/57 3251 Raw data (/proc/3247/stat): 3247 (minisat+_script) S 3246 3247 22582 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788597116 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/3247/statm): 531 226 485 147 0 384 0 [pid=3247] vsize: 2124 Raw data (/proc/3251/stat): 3251 (minisat+_64-bit) R 3247 3247 22582 0 -1 0 11332 0 0 0 53890 56 0 0 25 0 1 0 1788597121 47812608 10996 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/3251/statm): 11673 10996 145 145 0 11528 0 [pid=3251] vsize: 46692 Current children cumulated CPU time (s) 539.47 Current children cumulated vsize (Kb) 48816 [startup+550.032 s] Raw data (loadavg): 1.00 0.98 0.98 2/57 3251 Raw data (/proc/3247/stat): 3247 (minisat+_script) S 3246 3247 22582 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788597116 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/3247/statm): 531 226 485 147 0 384 0 [pid=3247] vsize: 2124 Raw data (/proc/3251/stat): 3251 (minisat+_64-bit) R 3247 3247 22582 0 -1 0 11376 0 0 0 54889 57 0 0 25 0 1 0 1788597121 48508928 11040 4294967295 134512640 135094434 3221224432 3221223088 134558213 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/3251/statm): 11843 11040 145 145 0 11698 0 [pid=3251] vsize: 47372 Current children cumulated CPU time (s) 549.47 Current children cumulated vsize (Kb) 49496 [startup+560.032 s] Raw data (loadavg): 1.00 0.98 0.98 2/57 3251 Raw data (/proc/3247/stat): 3247 (minisat+_script) S 3246 3247 22582 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788597116 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/3247/statm): 531 226 485 147 0 384 0 [pid=3247] vsize: 2124 Raw data (/proc/3251/stat): 3251 (minisat+_64-bit) R 3247 3247 22582 0 -1 0 11439 0 0 0 55888 57 0 0 25 0 1 0 1788597121 48754688 11103 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/3251/statm): 11903 11103 145 145 0 11758 0 [pid=3251] vsize: 47612 Current children cumulated CPU time (s) 559.46 Current children cumulated vsize (Kb) 49736 [startup+570.033 s] Raw data (loadavg): 1.00 0.98 0.98 2/57 3251 Raw data (/proc/3247/stat): 3247 (minisat+_script) S 3246 3247 22582 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788597116 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/3247/statm): 531 226 485 147 0 384 0 [pid=3247] vsize: 2124 Raw data (/proc/3251/stat): 3251 (minisat+_64-bit) R 3247 3247 22582 0 -1 0 11529 0 0 0 56887 57 0 0 25 0 1 0 1788597121 49111040 11193 4294967295 134512640 135094434 3221224432 3221223056 134557596 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/3251/statm): 11990 11193 145 145 0 11845 0 [pid=3251] vsize: 47960 Current children cumulated CPU time (s) 569.45 Current children cumulated vsize (Kb) 50084 [startup+580.033 s] Raw data (loadavg): 1.00 0.98 0.98 2/57 3251 Raw data (/proc/3247/stat): 3247 (minisat+_script) S 3246 3247 22582 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788597116 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/3247/statm): 531 226 485 147 0 384 0 [pid=3247] vsize: 2124 Raw data (/proc/3251/stat): 3251 (minisat+_64-bit) R 3247 3247 22582 0 -1 0 11585 0 0 0 57886 58 0 0 25 0 1 0 1788597121 49328128 11249 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/3251/statm): 12043 11249 145 145 0 11898 0 [pid=3251] vsize: 48172 Current children cumulated CPU time (s) 579.45 Current children cumulated vsize (Kb) 50296 [startup+590.034 s] Raw data (loadavg): 1.00 0.98 0.98 2/57 3251 Raw data (/proc/3247/stat): 3247 (minisat+_script) S 3246 3247 22582 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788597116 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/3247/statm): 531 226 485 147 0 384 0 [pid=3247] vsize: 2124 Raw data (/proc/3251/stat): 3251 (minisat+_64-bit) R 3247 3247 22582 0 -1 0 11634 0 0 0 58885 58 0 0 25 0 1 0 1788597121 49520640 11298 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/3251/statm): 12090 11298 145 145 0 11945 0 [pid=3251] vsize: 48360 Current children cumulated CPU time (s) 589.44 Current children cumulated vsize (Kb) 50484 [startup+600.034 s] Raw data (loadavg): 1.00 0.98 0.98 2/57 3251 Raw data (/proc/3247/stat): 3247 (minisat+_script) S 3246 3247 22582 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788597116 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/3247/statm): 531 226 485 147 0 384 0 [pid=3247] vsize: 2124 Raw data (/proc/3251/stat): 3251 (minisat+_64-bit) R 3247 3247 22582 0 -1 0 11706 0 0 0 59884 59 0 0 25 0 1 0 1788597121 49803264 11370 4294967295 134512640 135094434 3221224432 3221223088 134557964 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/3251/statm): 12159 11370 145 145 0 12014 0 [pid=3251] vsize: 48636 Current children cumulated CPU time (s) 599.44 Current children cumulated vsize (Kb) 50760 [startup+610.035 s] Raw data (loadavg): 1.00 0.98 0.98 2/57 3251 Raw data (/proc/3247/stat): 3247 (minisat+_script) S 3246 3247 22582 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788597116 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/3247/statm): 531 226 485 147 0 384 0 [pid=3247] vsize: 2124 Raw data (/proc/3251/stat): 3251 (minisat+_64-bit) R 3247 3247 22582 0 -1 0 11833 0 0 0 60883 59 0 0 25 0 1 0 1788597121 50307072 11497 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/3251/statm): 12282 11497 145 145 0 12137 0 [pid=3251] vsize: 49128 Current children cumulated CPU time (s) 609.43 Current children cumulated vsize (Kb) 51252 [startup+620.035 s] Raw data (loadavg): 1.00 0.98 0.98 2/57 3251 Raw data (/proc/3247/stat): 3247 (minisat+_script) S 3246 3247 22582 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788597116 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/3247/statm): 531 226 485 147 0 384 0 [pid=3247] vsize: 2124 Raw data (/proc/3251/stat): 3251 (minisat+_64-bit) R 3247 3247 22582 0 -1 0 11889 0 0 0 61881 61 0 0 25 0 1 0 1788597121 50528256 11553 4294967295 134512640 135094434 3221224432 3221223024 134551908 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/3251/statm): 12336 11553 145 145 0 12191 0 [pid=3251] vsize: 49344 Current children cumulated CPU time (s) 619.43 Current children cumulated vsize (Kb) 51468 [startup+630.036 s] Raw data (loadavg): 1.00 0.98 0.98 2/57 3251 Raw data (/proc/3247/stat): 3247 (minisat+_script) S 3246 3247 22582 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788597116 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/3247/statm): 531 226 485 147 0 384 0 [pid=3247] vsize: 2124 Raw data (/proc/3251/stat): 3251 (minisat+_64-bit) R 3247 3247 22582 0 -1 0 11977 0 0 0 62880 62 0 0 25 0 1 0 1788597121 50876416 11641 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/3251/statm): 12421 11641 145 145 0 12276 0 [pid=3251] vsize: 49684 Current children cumulated CPU time (s) 629.43 Current children cumulated vsize (Kb) 51808 [startup+640.037 s] Raw data (loadavg): 1.00 0.98 0.98 2/57 3251 Raw data (/proc/3247/stat): 3247 (minisat+_script) S 3246 3247 22582 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788597116 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/3247/statm): 531 226 485 147 0 384 0 [pid=3247] vsize: 2124 Raw data (/proc/3251/stat): 3251 (minisat+_64-bit) R 3247 3247 22582 0 -1 0 12054 0 0 0 63879 62 0 0 25 0 1 0 1788597121 51179520 11718 4294967295 134512640 135094434 3221224432 3221223120 134554746 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/3251/statm): 12495 11718 145 145 0 12350 0 [pid=3251] vsize: 49980 Current children cumulated CPU time (s) 639.42 Current children cumulated vsize (Kb) 52104 [startup+650.037 s] Raw data (loadavg): 1.00 0.98 0.98 2/57 3251 Raw data (/proc/3247/stat): 3247 (minisat+_script) S 3246 3247 22582 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788597116 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/3247/statm): 531 226 485 147 0 384 0 [pid=3247] vsize: 2124 Raw data (/proc/3251/stat): 3251 (minisat+_64-bit) R 3247 3247 22582 0 -1 0 12120 0 0 0 64877 63 0 0 25 0 1 0 1788597121 51441664 11784 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/3251/statm): 12559 11784 145 145 0 12414 0 [pid=3251] vsize: 50236 Current children cumulated CPU time (s) 649.41 Current children cumulated vsize (Kb) 52360 [startup+660.038 s] Raw data (loadavg): 1.00 0.98 0.98 2/57 3251 Raw data (/proc/3247/stat): 3247 (minisat+_script) S 3246 3247 22582 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788597116 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/3247/statm): 531 226 485 147 0 384 0 [pid=3247] vsize: 2124 Raw data (/proc/3251/stat): 3251 (minisat+_64-bit) R 3247 3247 22582 0 -1 0 12213 0 0 0 65875 64 0 0 25 0 1 0 1788597121 51810304 11877 4294967295 134512640 135094434 3221224432 3221223088 134558126 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/3251/statm): 12649 11877 145 145 0 12504 0 [pid=3251] vsize: 50596 Current children cumulated CPU time (s) 659.4 Current children cumulated vsize (Kb) 52720 [startup+670.038 s] Raw data (loadavg): 1.00 0.98 0.98 2/57 3251 Raw data (/proc/3247/stat): 3247 (minisat+_script) S 3246 3247 22582 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788597116 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/3247/statm): 531 226 485 147 0 384 0 [pid=3247] vsize: 2124 Raw data (/proc/3251/stat): 3251 (minisat+_64-bit) R 3247 3247 22582 0 -1 0 12278 0 0 0 66874 65 0 0 25 0 1 0 1788597121 52064256 11942 4294967295 134512640 135094434 3221224432 3221223056 134557685 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/3251/statm): 12711 11942 145 145 0 12566 0 [pid=3251] vsize: 50844 Current children cumulated CPU time (s) 669.4 Current children cumulated vsize (Kb) 52968 [startup+680.039 s] Raw data (loadavg): 1.00 0.98 0.98 2/57 3251 Raw data (/proc/3247/stat): 3247 (minisat+_script) S 3246 3247 22582 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788597116 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/3247/statm): 531 226 485 147 0 384 0 [pid=3247] vsize: 2124 Raw data (/proc/3251/stat): 3251 (minisat+_64-bit) R 3247 3247 22582 0 -1 0 12356 0 0 0 67872 66 0 0 25 0 1 0 1788597121 52371456 12020 4294967295 134512640 135094434 3221224432 3221223044 134563154 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/3251/statm): 12786 12020 145 145 0 12641 0 [pid=3251] vsize: 51144 Current children cumulated CPU time (s) 679.39 Current children cumulated vsize (Kb) 53268 [startup+690.039 s] Raw data (loadavg): 1.00 0.98 0.98 2/57 3251 Raw data (/proc/3247/stat): 3247 (minisat+_script) S 3246 3247 22582 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788597116 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/3247/statm): 531 226 485 147 0 384 0 [pid=3247] vsize: 2124 Raw data (/proc/3251/stat): 3251 (minisat+_64-bit) R 3247 3247 22582 0 -1 0 12435 0 0 0 68870 67 0 0 25 0 1 0 1788597121 52682752 12099 4294967295 134512640 135094434 3221224432 3221223024 134556789 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/3251/statm): 12862 12099 145 145 0 12717 0 [pid=3251] vsize: 51448 Current children cumulated CPU time (s) 689.38 Current children cumulated vsize (Kb) 53572 [startup+700.039 s] Raw data (loadavg): 1.00 0.98 0.98 2/57 3251 Raw data (/proc/3247/stat): 3247 (minisat+_script) S 3246 3247 22582 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788597116 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/3247/statm): 531 226 485 147 0 384 0 [pid=3247] vsize: 2124 Raw data (/proc/3251/stat): 3251 (minisat+_64-bit) R 3247 3247 22582 0 -1 0 12556 0 0 0 69869 67 0 0 25 0 1 0 1788597121 53161984 12220 4294967295 134512640 135094434 3221224432 3221223088 134558159 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/3251/statm): 12979 12220 145 145 0 12834 0 [pid=3251] vsize: 51916 Current children cumulated CPU time (s) 699.37 Current children cumulated vsize (Kb) 54040 [startup+710.04 s] Raw data (loadavg): 1.00 0.98 0.98 2/57 3251 Raw data (/proc/3247/stat): 3247 (minisat+_script) S 3246 3247 22582 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788597116 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/3247/statm): 531 226 485 147 0 384 0 [pid=3247] vsize: 2124 Raw data (/proc/3251/stat): 3251 (minisat+_64-bit) R 3247 3247 22582 0 -1 0 12607 0 0 0 70868 68 0 0 25 0 1 0 1788597121 53362688 12271 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/3251/statm): 13028 12271 145 145 0 12883 0 [pid=3251] vsize: 52112 Current children cumulated CPU time (s) 709.37 Current children cumulated vsize (Kb) 54236 [startup+720.04 s] Raw data (loadavg): 1.00 0.98 0.98 2/57 3251 Raw data (/proc/3247/stat): 3247 (minisat+_script) S 3246 3247 22582 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788597116 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/3247/statm): 531 226 485 147 0 384 0 [pid=3247] vsize: 2124 Raw data (/proc/3251/stat): 3251 (minisat+_64-bit) R 3247 3247 22582 0 -1 0 12675 0 0 0 71867 68 0 0 25 0 1 0 1788597121 53633024 12339 4294967295 134512640 135094434 3221224432 3221223088 134558420 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/3251/statm): 13094 12339 145 145 0 12949 0 [pid=3251] vsize: 52376 Current children cumulated CPU time (s) 719.36 Current children cumulated vsize (Kb) 54500 [startup+730.041 s] Raw data (loadavg): 1.00 0.98 0.98 2/57 3251 Raw data (/proc/3247/stat): 3247 (minisat+_script) S 3246 3247 22582 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788597116 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/3247/statm): 531 226 485 147 0 384 0 [pid=3247] vsize: 2124 Raw data (/proc/3251/stat): 3251 (minisat+_64-bit) R 3247 3247 22582 0 -1 0 12781 0 0 0 72865 69 0 0 25 0 1 0 1788597121 54050816 12445 4294967295 134512640 135094434 3221224432 3221223044 134563061 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/3251/statm): 13196 12445 145 145 0 13051 0 [pid=3251] vsize: 52784 Current children cumulated CPU time (s) 729.35 Current children cumulated vsize (Kb) 54908 [startup+740.041 s] Raw data (loadavg): 1.00 0.98 0.98 2/57 3251 Raw data (/proc/3247/stat): 3247 (minisat+_script) S 3246 3247 22582 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788597116 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/3247/statm): 531 226 485 147 0 384 0 [pid=3247] vsize: 2124 Raw data (/proc/3251/stat): 3251 (minisat+_64-bit) R 3247 3247 22582 0 -1 0 13116 0 0 0 73858 72 0 0 25 0 1 0 1788597121 55390208 12780 4294967295 134512640 135094434 3221224432 3221223120 134554746 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/3251/statm): 13523 12780 145 145 0 13378 0 [pid=3251] vsize: 54092 Current children cumulated CPU time (s) 739.31 Current children cumulated vsize (Kb) 56216 [startup+750.042 s] Raw data (loadavg): 1.00 0.98 0.98 2/57 3251 Raw data (/proc/3247/stat): 3247 (minisat+_script) S 3246 3247 22582 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788597116 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/3247/statm): 531 226 485 147 0 384 0 [pid=3247] vsize: 2124 Raw data (/proc/3251/stat): 3251 (minisat+_64-bit) R 3247 3247 22582 0 -1 0 13235 0 0 0 74857 73 0 0 25 0 1 0 1788597121 55861248 12899 4294967295 134512640 135094434 3221224432 3221223044 134563049 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/3251/statm): 13638 12899 145 145 0 13493 0 [pid=3251] vsize: 54552 Current children cumulated CPU time (s) 749.31 Current children cumulated vsize (Kb) 56676 [startup+760.042 s] Raw data (loadavg): 1.00 0.98 0.98 2/57 3251 Raw data (/proc/3247/stat): 3247 (minisat+_script) S 3246 3247 22582 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788597116 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/3247/statm): 531 226 485 147 0 384 0 [pid=3247] vsize: 2124 Raw data (/proc/3251/stat): 3251 (minisat+_64-bit) R 3247 3247 22582 0 -1 0 13297 0 0 0 75855 74 0 0 25 0 1 0 1788597121 56107008 12961 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/3251/statm): 13698 12961 145 145 0 13553 0 [pid=3251] vsize: 54792 Current children cumulated CPU time (s) 759.3 Current children cumulated vsize (Kb) 56916 [startup+770.043 s] Raw data (loadavg): 1.00 0.98 0.98 2/57 3251 Raw data (/proc/3247/stat): 3247 (minisat+_script) S 3246 3247 22582 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788597116 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/3247/statm): 531 226 485 147 0 384 0 [pid=3247] vsize: 2124 Raw data (/proc/3251/stat): 3251 (minisat+_64-bit) R 3247 3247 22582 0 -1 0 13350 0 0 0 76854 75 0 0 25 0 1 0 1788597121 56315904 13014 4294967295 134512640 135094434 3221224432 3221223044 134563055 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/3251/statm): 13749 13014 145 145 0 13604 0 [pid=3251] vsize: 54996 Current children cumulated CPU time (s) 769.3 Current children cumulated vsize (Kb) 57120 [startup+780.044 s] Raw data (loadavg): 1.00 0.98 0.98 2/57 3251 Raw data (/proc/3247/stat): 3247 (minisat+_script) S 3246 3247 22582 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788597116 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/3247/statm): 531 226 485 147 0 384 0 [pid=3247] vsize: 2124 Raw data (/proc/3251/stat): 3251 (minisat+_64-bit) R 3247 3247 22582 0 -1 0 13497 0 0 0 77850 77 0 0 25 0 1 0 1788597121 56905728 13161 4294967295 134512640 135094434 3221224432 3221223068 134557560 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/3251/statm): 13893 13161 145 145 0 13748 0 [pid=3251] vsize: 55572 Current children cumulated CPU time (s) 779.28 Current children cumulated vsize (Kb) 57696 [startup+790.045 s] Raw data (loadavg): 1.00 0.98 0.98 1/57 3251 Raw data (/proc/3247/stat): 3247 (minisat+_script) S 3246 3247 22582 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788597116 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/3247/statm): 531 226 485 147 0 384 0 [pid=3247] vsize: 2124 Raw data (/proc/3251/stat): 3251 (minisat+_64-bit) T 3247 3247 22582 0 -1 0 13604 0 0 0 78853 78 0 0 25 0 1 0 1788597121 57331712 13268 4294967295 134512640 135094434 3221224432 3221222796 134870330 0 0 5 16386 3222434794 0 0 17 0 0 0 Raw data (/proc/3251/statm): 13997 13268 145 145 0 13852 0 [pid=3251] vsize: 55988 Current children cumulated CPU time (s) 789.32 Current children cumulated vsize (Kb) 58112 [startup+800.646 s] Raw data (loadavg): 1.00 0.98 0.98 2/57 3251 Raw data (/proc/3247/stat): 3247 (minisat+_script) S 3246 3247 22582 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788597116 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/3247/statm): 531 226 485 147 0 384 0 [pid=3247] vsize: 2124 Raw data (/proc/3251/stat): 3251 (minisat+_64-bit) R 3247 3247 22582 0 -1 0 13650 0 0 0 79852 78 0 0 25 0 1 0 1788597121 57511936 13314 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/3251/statm): 14041 13314 145 145 0 13896 0 [pid=3251] vsize: 56164 Current children cumulated CPU time (s) 799.31 Current children cumulated vsize (Kb) 58288 [startup+810.648 s] Raw data (loadavg): 1.00 0.98 0.98 3/57 3251 Raw data (/proc/3247/stat): 3247 (minisat+_script) S 3246 3247 22582 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788597116 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/3247/statm): 531 226 485 147 0 384 0 [pid=3247] vsize: 2124 Raw data (/proc/3251/stat): 3251 (minisat+_64-bit) R 3247 3247 22582 0 -1 0 13712 0 0 0 80850 79 0 0 25 0 1 0 1788597121 57757696 13376 4294967295 134512640 135094434 3221224432 3221223088 134561460 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/3251/statm): 14101 13376 145 145 0 13956 0 [pid=3251] vsize: 56404 Current children cumulated CPU time (s) 809.3 Current children cumulated vsize (Kb) 58528 [startup+820.648 s] Raw data (loadavg): 1.00 0.98 0.98 2/57 3251 Raw data (/proc/3247/stat): 3247 (minisat+_script) S 3246 3247 22582 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788597116 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/3247/statm): 531 226 485 147 0 384 0 [pid=3247] vsize: 2124 Raw data (/proc/3251/stat): 3251 (minisat+_64-bit) R 3247 3247 22582 0 -1 0 13798 0 0 0 81849 80 0 0 25 0 1 0 1788597121 58093568 13462 4294967295 134512640 135094434 3221224432 3221223080 134558258 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/3251/statm): 14183 13462 145 145 0 14038 0 [pid=3251] vsize: 56732 Current children cumulated CPU time (s) 819.3 Current children cumulated vsize (Kb) 58856 [startup+830.65 s] Raw data (loadavg): 1.00 0.98 0.98 2/57 3251 Raw data (/proc/3247/stat): 3247 (minisat+_script) S 3246 3247 22582 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788597116 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/3247/statm): 531 226 485 147 0 384 0 [pid=3247] vsize: 2124 Raw data (/proc/3251/stat): 3251 (minisat+_64-bit) R 3247 3247 22582 0 -1 0 13869 0 0 0 82847 81 0 0 25 0 1 0 1788597121 58376192 13533 4294967295 134512640 135094434 3221224432 3221222976 134562082 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/3251/statm): 14252 13533 145 145 0 14107 0 [pid=3251] vsize: 57008 Current children cumulated CPU time (s) 829.29 Current children cumulated vsize (Kb) 59132 [startup+840.651 s] Raw data (loadavg): 1.00 0.98 0.98 2/57 3251 Raw data (/proc/3247/stat): 3247 (minisat+_script) S 3246 3247 22582 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788597116 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/3247/statm): 531 226 485 147 0 384 0 [pid=3247] vsize: 2124 Raw data (/proc/3251/stat): 3251 (minisat+_64-bit) R 3247 3247 22582 0 -1 0 13981 0 0 0 83844 83 0 0 25 0 1 0 1788597121 58822656 13645 4294967295 134512640 135094434 3221224432 3221223088 134557846 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/3251/statm): 14361 13645 145 145 0 14216 0 [pid=3251] vsize: 57444 Current children cumulated CPU time (s) 839.28 Current children cumulated vsize (Kb) 59568 [startup+850.65 s] Raw data (loadavg): 1.00 0.98 0.98 2/57 3251 Raw data (/proc/3247/stat): 3247 (minisat+_script) S 3246 3247 22582 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788597116 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/3247/statm): 531 226 485 147 0 384 0 [pid=3247] vsize: 2124 Raw data (/proc/3251/stat): 3251 (minisat+_64-bit) R 3247 3247 22582 0 -1 0 14204 0 0 0 84839 85 0 0 25 0 1 0 1788597121 59715584 13868 4294967295 134512640 135094434 3221224432 3221223088 134558254 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/3251/statm): 14579 13868 145 145 0 14434 0 [pid=3251] vsize: 58316 Current children cumulated CPU time (s) 849.25 Current children cumulated vsize (Kb) 60440 [startup+860.651 s] Raw data (loadavg): 1.00 0.98 0.98 2/57 3251 Raw data (/proc/3247/stat): 3247 (minisat+_script) S 3246 3247 22582 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788597116 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/3247/statm): 531 226 485 147 0 384 0 [pid=3247] vsize: 2124 Raw data (/proc/3251/stat): 3251 (minisat+_64-bit) R 3247 3247 22582 0 -1 0 14343 0 0 0 85836 86 0 0 25 0 1 0 1788597121 60264448 14007 4294967295 134512640 135094434 3221224432 3221223044 134563094 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/3251/statm): 14713 14007 145 145 0 14568 0 [pid=3251] vsize: 58852 Current children cumulated CPU time (s) 859.23 Current children cumulated vsize (Kb) 60976 [startup+870.652 s] Raw data (loadavg): 1.00 0.98 0.98 3/57 3251 Raw data (/proc/3247/stat): 3247 (minisat+_script) S 3246 3247 22582 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788597116 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/3247/statm): 531 226 485 147 0 384 0 [pid=3247] vsize: 2124 Raw data (/proc/3251/stat): 3251 (minisat+_64-bit) R 3247 3247 22582 0 -1 0 14423 0 0 0 86834 87 0 0 25 0 1 0 1788597121 60579840 14087 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/3251/statm): 14790 14087 145 145 0 14645 0 [pid=3251] vsize: 59160 Current children cumulated CPU time (s) 869.22 Current children cumulated vsize (Kb) 61284 [startup+880.653 s] Raw data (loadavg): 1.00 0.98 0.98 2/57 3251 Raw data (/proc/3247/stat): 3247 (minisat+_script) S 3246 3247 22582 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788597116 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/3247/statm): 531 226 485 147 0 384 0 [pid=3247] vsize: 2124 Raw data (/proc/3251/stat): 3251 (minisat+_64-bit) R 3247 3247 22582 0 -1 0 14483 0 0 0 87834 87 0 0 25 0 1 0 1788597121 60817408 14147 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/3251/statm): 14848 14147 145 145 0 14703 0 [pid=3251] vsize: 59392 Current children cumulated CPU time (s) 879.22 Current children cumulated vsize (Kb) 61516 [startup+890.653 s] Raw data (loadavg): 1.00 0.98 0.98 2/57 3251 Raw data (/proc/3247/stat): 3247 (minisat+_script) S 3246 3247 22582 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788597116 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/3247/statm): 531 226 485 147 0 384 0 [pid=3247] vsize: 2124 Raw data (/proc/3251/stat): 3251 (minisat+_64-bit) R 3247 3247 22582 0 -1 0 14540 0 0 0 88833 88 0 0 25 0 1 0 1788597121 61042688 14204 4294967295 134512640 135094434 3221224432 3221223088 134558213 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/3251/statm): 14903 14204 145 145 0 14758 0 [pid=3251] vsize: 59612 Current children cumulated CPU time (s) 889.22 Current children cumulated vsize (Kb) 61736 [startup+900.654 s] Raw data (loadavg): 1.00 0.98 0.98 2/57 3251 Raw data (/proc/3247/stat): 3247 (minisat+_script) S 3246 3247 22582 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788597116 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/3247/statm): 531 226 485 147 0 384 0 [pid=3247] vsize: 2124 Raw data (/proc/3251/stat): 3251 (minisat+_64-bit) R 3247 3247 22582 0 -1 0 14609 0 0 0 89832 88 0 0 25 0 1 0 1788597121 61313024 14273 4294967295 134512640 135094434 3221224432 3221223120 134554726 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/3251/statm): 14969 14273 145 145 0 14824 0 [pid=3251] vsize: 59876 Current children cumulated CPU time (s) 899.21 Current children cumulated vsize (Kb) 62000 [startup+910.654 s] Raw data (loadavg): 1.00 0.98 0.98 2/57 3251 Raw data (/proc/3247/stat): 3247 (minisat+_script) S 3246 3247 22582 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788597116 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/3247/statm): 531 226 485 147 0 384 0 [pid=3247] vsize: 2124 Raw data (/proc/3251/stat): 3251 (minisat+_64-bit) R 3247 3247 22582 0 -1 0 14700 0 0 0 90830 89 0 0 25 0 1 0 1788597121 61665280 14364 4294967295 134512640 135094434 3221224432 3221223088 134558426 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/3251/statm): 15055 14364 145 145 0 14910 0 [pid=3251] vsize: 60220 Current children cumulated CPU time (s) 909.2 Current children cumulated vsize (Kb) 62344 [startup+920.655 s] Raw data (loadavg): 1.00 0.98 0.98 2/57 3251 Raw data (/proc/3247/stat): 3247 (minisat+_script) S 3246 3247 22582 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788597116 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/3247/statm): 531 226 485 147 0 384 0 [pid=3247] vsize: 2124 Raw data (/proc/3251/stat): 3251 (minisat+_64-bit) R 3247 3247 22582 0 -1 0 14768 0 0 0 91829 90 0 0 25 0 1 0 1788597121 61935616 14432 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/3251/statm): 15121 14432 145 145 0 14976 0 [pid=3251] vsize: 60484 Current children cumulated CPU time (s) 919.2 Current children cumulated vsize (Kb) 62608 [startup+930.657 s] Raw data (loadavg): 1.00 0.98 0.98 2/57 3251 Raw data (/proc/3247/stat): 3247 (minisat+_script) S 3246 3247 22582 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788597116 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/3247/statm): 531 226 485 147 0 384 0 [pid=3247] vsize: 2124 Raw data (/proc/3251/stat): 3251 (minisat+_64-bit) R 3247 3247 22582 0 -1 0 14832 0 0 0 92828 90 0 0 25 0 1 0 1788597121 62189568 14496 4294967295 134512640 135094434 3221224432 3221223072 134562088 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/3251/statm): 15183 14496 145 145 0 15038 0 [pid=3251] vsize: 60732 Current children cumulated CPU time (s) 929.19 Current children cumulated vsize (Kb) 62856 [startup+940.657 s] Raw data (loadavg): 1.00 0.98 0.98 2/57 3251 Raw data (/proc/3247/stat): 3247 (minisat+_script) S 3246 3247 22582 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788597116 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/3247/statm): 531 226 485 147 0 384 0 [pid=3247] vsize: 2124 Raw data (/proc/3251/stat): 3251 (minisat+_64-bit) R 3247 3247 22582 0 -1 0 14929 0 0 0 93826 91 0 0 25 0 1 0 1788597121 62574592 14593 4294967295 134512640 135094434 3221224432 3221223076 134558261 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/3251/statm): 15277 14593 145 145 0 15132 0 [pid=3251] vsize: 61108 Current children cumulated CPU time (s) 939.18 Current children cumulated vsize (Kb) 63232 [startup+950.658 s] Raw data (loadavg): 1.00 0.98 0.98 2/57 3251 Raw data (/proc/3247/stat): 3247 (minisat+_script) S 3246 3247 22582 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788597116 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/3247/statm): 531 226 485 147 0 384 0 [pid=3247] vsize: 2124 Raw data (/proc/3251/stat): 3251 (minisat+_64-bit) R 3247 3247 22582 0 -1 0 14975 0 0 0 94826 92 0 0 25 0 1 0 1788597121 62754816 14639 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/3251/statm): 15321 14639 145 145 0 15176 0 [pid=3251] vsize: 61284 Current children cumulated CPU time (s) 949.19 Current children cumulated vsize (Kb) 63408 [startup+960.658 s] Raw data (loadavg): 1.00 0.98 0.98 2/57 3251 Raw data (/proc/3247/stat): 3247 (minisat+_script) S 3246 3247 22582 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788597116 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/3247/statm): 531 226 485 147 0 384 0 [pid=3247] vsize: 2124 Raw data (/proc/3251/stat): 3251 (minisat+_64-bit) R 3247 3247 22582 0 -1 0 15031 0 0 0 95824 92 0 0 25 0 1 0 1788597121 62976000 14695 4294967295 134512640 135094434 3221224432 3221223044 134563049 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/3251/statm): 15375 14695 145 145 0 15230 0 [pid=3251] vsize: 61500 Current children cumulated CPU time (s) 959.17 Current children cumulated vsize (Kb) 63624 [startup+970.659 s] Raw data (loadavg): 1.00 0.98 0.98 2/57 3251 Raw data (/proc/3247/stat): 3247 (minisat+_script) S 3246 3247 22582 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788597116 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/3247/statm): 531 226 485 147 0 384 0 [pid=3247] vsize: 2124 Raw data (/proc/3251/stat): 3251 (minisat+_64-bit) R 3247 3247 22582 0 -1 0 15127 0 0 0 96824 93 0 0 25 0 1 0 1788597121 63356928 14791 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/3251/statm): 15468 14791 145 145 0 15323 0 [pid=3251] vsize: 61872 Current children cumulated CPU time (s) 969.18 Current children cumulated vsize (Kb) 63996 [startup+980.659 s] Raw data (loadavg): 1.00 0.98 0.98 2/57 3251 Raw data (/proc/3247/stat): 3247 (minisat+_script) S 3246 3247 22582 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788597116 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/3247/statm): 531 226 485 147 0 384 0 [pid=3247] vsize: 2124 Raw data (/proc/3251/stat): 3251 (minisat+_64-bit) R 3247 3247 22582 0 -1 0 15250 0 0 0 97821 95 0 0 25 0 1 0 1788597121 63844352 14914 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/3251/statm): 15587 14914 145 145 0 15442 0 [pid=3251] vsize: 62348 Current children cumulated CPU time (s) 979.17 Current children cumulated vsize (Kb) 64472 [startup+990.66 s] Raw data (loadavg): 1.00 0.98 0.98 2/57 3251 Raw data (/proc/3247/stat): 3247 (minisat+_script) S 3246 3247 22582 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788597116 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/3247/statm): 531 226 485 147 0 384 0 [pid=3247] vsize: 2124 Raw data (/proc/3251/stat): 3251 (minisat+_64-bit) R 3247 3247 22582 0 -1 0 15317 0 0 0 98820 95 0 0 25 0 1 0 1788597121 65159168 14981 4294967295 134512640 135094434 3221224432 3221223104 134554891 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/3251/statm): 15908 14981 145 145 0 15763 0 [pid=3251] vsize: 63632 Current children cumulated CPU time (s) 989.16 Current children cumulated vsize (Kb) 65756 [startup+1000.66 s] Raw data (loadavg): 1.00 0.98 0.98 2/57 3251 Raw data (/proc/3247/stat): 3247 (minisat+_script) S 3246 3247 22582 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788597116 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/3247/statm): 531 226 485 147 0 384 0 [pid=3247] vsize: 2124 Raw data (/proc/3251/stat): 3251 (minisat+_64-bit) R 3247 3247 22582 0 -1 0 15375 0 0 0 99819 95 0 0 25 0 1 0 1788597121 65388544 15039 4294967295 134512640 135094434 3221224432 3221223088 134557879 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/3251/statm): 15964 15039 145 145 0 15819 0 [pid=3251] vsize: 63856 Current children cumulated CPU time (s) 999.15 Current children cumulated vsize (Kb) 65980 [startup+1010.66 s] Raw data (loadavg): 1.00 0.98 0.98 2/57 3251 Raw data (/proc/3247/stat): 3247 (minisat+_script) S 3246 3247 22582 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788597116 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/3247/statm): 531 226 485 147 0 384 0 [pid=3247] vsize: 2124 Raw data (/proc/3251/stat): 3251 (minisat+_64-bit) R 3247 3247 22582 0 -1 0 15483 0 0 0 100817 97 0 0 25 0 1 0 1788597121 65814528 15147 4294967295 134512640 135094434 3221224432 3221223076 134558261 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/3251/statm): 16068 15147 145 145 0 15923 0 [pid=3251] vsize: 64272 Current children cumulated CPU time (s) 1009.15 Current children cumulated vsize (Kb) 66396 [startup+1020.66 s] Raw data (loadavg): 1.00 0.98 0.98 2/57 3251 Raw data (/proc/3247/stat): 3247 (minisat+_script) S 3246 3247 22582 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788597116 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/3247/statm): 531 226 485 147 0 384 0 [pid=3247] vsize: 2124 Raw data (/proc/3251/stat): 3251 (minisat+_64-bit) R 3247 3247 22582 0 -1 0 15609 0 0 0 101815 97 0 0 25 0 1 0 1788597121 66314240 15273 4294967295 134512640 135094434 3221224432 3221223120 134784967 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/3251/statm): 16190 15273 145 145 0 16045 0 [pid=3251] vsize: 64760 Current children cumulated CPU time (s) 1019.13 Current children cumulated vsize (Kb) 66884 [startup+1030.66 s] Raw data (loadavg): 1.00 0.98 0.98 2/57 3251 Raw data (/proc/3247/stat): 3247 (minisat+_script) S 3246 3247 22582 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788597116 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/3247/statm): 531 226 485 147 0 384 0 [pid=3247] vsize: 2124 Raw data (/proc/3251/stat): 3251 (minisat+_64-bit) R 3247 3247 22582 0 -1 0 15828 0 0 0 102810 100 0 0 25 0 1 0 1788597121 67190784 15492 4294967295 134512640 135094434 3221224432 3221223088 134557937 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/3251/statm): 16404 15492 145 145 0 16259 0 [pid=3251] vsize: 65616 Current children cumulated CPU time (s) 1029.11 Current children cumulated vsize (Kb) 67740 [startup+1040.66 s] Raw data (loadavg): 1.00 0.98 0.98 2/57 3251 Raw data (/proc/3247/stat): 3247 (minisat+_script) S 3246 3247 22582 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788597116 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/3247/statm): 531 226 485 147 0 384 0 [pid=3247] vsize: 2124 Raw data (/proc/3251/stat): 3251 (minisat+_64-bit) R 3247 3247 22582 0 -1 0 15893 0 0 0 103809 100 0 0 25 0 1 0 1788597121 67444736 15557 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/3251/statm): 16466 15557 145 145 0 16321 0 [pid=3251] vsize: 65864 Current children cumulated CPU time (s) 1039.1 Current children cumulated vsize (Kb) 67988 [startup+1050.66 s] Raw data (loadavg): 1.00 0.98 0.98 2/57 3251 Raw data (/proc/3247/stat): 3247 (minisat+_script) S 3246 3247 22582 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788597116 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/3247/statm): 531 226 485 147 0 384 0 [pid=3247] vsize: 2124 Raw data (/proc/3251/stat): 3251 (minisat+_64-bit) R 3247 3247 22582 0 -1 0 16312 0 0 0 104802 103 0 0 25 0 1 0 1788597121 69132288 15976 4294967295 134512640 135094434 3221224432 3221223044 134563055 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/3251/statm): 16878 15976 145 145 0 16733 0 [pid=3251] vsize: 67512 Current children cumulated CPU time (s) 1049.06 Current children cumulated vsize (Kb) 69636 [startup+1060.66 s] Raw data (loadavg): 1.00 0.98 0.98 2/57 3251 Raw data (/proc/3247/stat): 3247 (minisat+_script) S 3246 3247 22582 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788597116 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/3247/statm): 531 226 485 147 0 384 0 [pid=3247] vsize: 2124 Raw data (/proc/3251/stat): 3251 (minisat+_64-bit) R 3247 3247 22582 0 -1 0 16569 0 0 0 105797 106 0 0 25 0 1 0 1788597121 70168576 16233 4294967295 134512640 135094434 3221224432 3221223000 134538517 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/3251/statm): 17131 16233 145 145 0 16986 0 [pid=3251] vsize: 68524 Current children cumulated CPU time (s) 1059.04 Current children cumulated vsize (Kb) 70648 [startup+1070.66 s] Raw data (loadavg): 1.00 0.98 0.98 2/57 3251 Raw data (/proc/3247/stat): 3247 (minisat+_script) S 3246 3247 22582 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788597116 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/3247/statm): 531 226 485 147 0 384 0 [pid=3247] vsize: 2124 Raw data (/proc/3251/stat): 3251 (minisat+_64-bit) R 3247 3247 22582 0 -1 0 16687 0 0 0 106795 107 0 0 25 0 1 0 1788597121 70635520 16351 4294967295 134512640 135094434 3221224432 3221223056 134557596 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/3251/statm): 17245 16351 145 145 0 17100 0 [pid=3251] vsize: 68980 Current children cumulated CPU time (s) 1069.03 Current children cumulated vsize (Kb) 71104 [startup+1080.66 s] Raw data (loadavg): 1.00 0.98 0.98 2/57 3251 Raw data (/proc/3247/stat): 3247 (minisat+_script) S 3246 3247 22582 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788597116 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/3247/statm): 531 226 485 147 0 384 0 [pid=3247] vsize: 2124 Raw data (/proc/3251/stat): 3251 (minisat+_64-bit) R 3247 3247 22582 0 -1 0 17037 0 0 0 107789 110 0 0 25 0 1 0 1788597121 72044544 16701 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/3251/statm): 17589 16701 145 145 0 17444 0 [pid=3251] vsize: 70356 Current children cumulated CPU time (s) 1079 Current children cumulated vsize (Kb) 72480 [startup+1090.67 s] Raw data (loadavg): 1.00 0.98 0.98 2/57 3251 Raw data (/proc/3247/stat): 3247 (minisat+_script) S 3246 3247 22582 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788597116 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/3247/statm): 531 226 485 147 0 384 0 [pid=3247] vsize: 2124 Raw data (/proc/3251/stat): 3251 (minisat+_64-bit) R 3247 3247 22582 0 -1 0 17316 0 0 0 108782 113 0 0 25 0 1 0 1788597121 73162752 16980 4294967295 134512640 135094434 3221224432 3221223088 134557879 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/3251/statm): 17862 16980 145 145 0 17717 0 [pid=3251] vsize: 71448 Current children cumulated CPU time (s) 1088.96 Current children cumulated vsize (Kb) 73572 [startup+1100.67 s] Raw data (loadavg): 1.00 0.98 0.98 2/57 3251 Raw data (/proc/3247/stat): 3247 (minisat+_script) S 3246 3247 22582 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788597116 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/3247/statm): 531 226 485 147 0 384 0 [pid=3247] vsize: 2124 Raw data (/proc/3251/stat): 3251 (minisat+_64-bit) R 3247 3247 22582 0 -1 0 17490 0 0 0 109779 114 0 0 25 0 1 0 1788597121 73867264 17154 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/3251/statm): 18034 17154 145 145 0 17889 0 [pid=3251] vsize: 72136 Current children cumulated CPU time (s) 1098.94 Current children cumulated vsize (Kb) 74260 [startup+1110.67 s] Raw data (loadavg): 1.00 0.98 0.98 2/57 3251 Raw data (/proc/3247/stat): 3247 (minisat+_script) S 3246 3247 22582 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788597116 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/3247/statm): 531 226 485 147 0 384 0 [pid=3247] vsize: 2124 Raw data (/proc/3251/stat): 3251 (minisat+_64-bit) R 3247 3247 22582 0 -1 0 17675 0 0 0 110776 116 0 0 25 0 1 0 1788597121 74608640 17339 4294967295 134512640 135094434 3221224432 3221223056 134557669 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/3251/statm): 18215 17339 145 145 0 18070 0 [pid=3251] vsize: 72860 Current children cumulated CPU time (s) 1108.93 Current children cumulated vsize (Kb) 74984 [startup+1120.67 s] Raw data (loadavg): 1.00 0.98 0.98 2/57 3251 Raw data (/proc/3247/stat): 3247 (minisat+_script) S 3246 3247 22582 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788597116 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/3247/statm): 531 226 485 147 0 384 0 [pid=3247] vsize: 2124 Raw data (/proc/3251/stat): 3251 (minisat+_64-bit) R 3247 3247 22582 0 -1 0 17740 0 0 0 111774 117 0 0 25 0 1 0 1788597121 74858496 17404 4294967295 134512640 135094434 3221224432 3221223044 134563049 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/3251/statm): 18276 17404 145 145 0 18131 0 [pid=3251] vsize: 73104 Current children cumulated CPU time (s) 1118.92 Current children cumulated vsize (Kb) 75228 [startup+1130.67 s] Raw data (loadavg): 1.00 0.98 0.98 2/57 3251 Raw data (/proc/3247/stat): 3247 (minisat+_script) S 3246 3247 22582 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788597116 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/3247/statm): 531 226 485 147 0 384 0 [pid=3247] vsize: 2124 Raw data (/proc/3251/stat): 3251 (minisat+_64-bit) R 3247 3247 22582 0 -1 0 17886 0 0 0 112771 119 0 0 25 0 1 0 1788597121 75444224 17550 4294967295 134512640 135094434 3221224432 3221223088 134558013 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/3251/statm): 18419 17550 145 145 0 18274 0 [pid=3251] vsize: 73676 Current children cumulated CPU time (s) 1128.91 Current children cumulated vsize (Kb) 75800 [startup+1140.67 s] Raw data (loadavg): 1.00 0.98 0.98 2/57 3251 Raw data (/proc/3247/stat): 3247 (minisat+_script) S 3246 3247 22582 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788597116 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/3247/statm): 531 226 485 147 0 384 0 [pid=3247] vsize: 2124 Raw data (/proc/3251/stat): 3251 (minisat+_64-bit) R 3247 3247 22582 0 -1 0 18103 0 0 0 113767 120 0 0 25 0 1 0 1788597121 76316672 17767 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/3251/statm): 18632 17767 145 145 0 18487 0 [pid=3251] vsize: 74528 Current children cumulated CPU time (s) 1138.88 Current children cumulated vsize (Kb) 76652 [startup+1150.67 s] Raw data (loadavg): 1.00 0.98 0.98 2/57 3251 Raw data (/proc/3247/stat): 3247 (minisat+_script) S 3246 3247 22582 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788597116 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/3247/statm): 531 226 485 147 0 384 0 [pid=3247] vsize: 2124 Raw data (/proc/3251/stat): 3251 (minisat+_64-bit) R 3247 3247 22582 0 -1 0 18171 0 0 0 114765 121 0 0 25 0 1 0 1788597121 76582912 17835 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/3251/statm): 18697 17835 145 145 0 18552 0 [pid=3251] vsize: 74788 Current children cumulated CPU time (s) 1148.87 Current children cumulated vsize (Kb) 76912 [startup+1160.67 s] Raw data (loadavg): 1.00 0.98 0.98 2/57 3251 Raw data (/proc/3247/stat): 3247 (minisat+_script) S 3246 3247 22582 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788597116 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/3247/statm): 531 226 485 147 0 384 0 [pid=3247] vsize: 2124 Raw data (/proc/3251/stat): 3251 (minisat+_64-bit) R 3247 3247 22582 0 -1 0 18298 0 0 0 115763 123 0 0 25 0 1 0 1788597121 77090816 17962 4294967295 134512640 135094434 3221224432 3221223088 134558156 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/3251/statm): 18821 17962 145 145 0 18676 0 [pid=3251] vsize: 75284 Current children cumulated CPU time (s) 1158.87 Current children cumulated vsize (Kb) 77408 [startup+1170.67 s] Raw data (loadavg): 1.00 0.98 0.98 2/57 3251 Raw data (/proc/3247/stat): 3247 (minisat+_script) S 3246 3247 22582 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788597116 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/3247/statm): 531 226 485 147 0 384 0 [pid=3247] vsize: 2124 Raw data (/proc/3251/stat): 3251 (minisat+_64-bit) R 3247 3247 22582 0 -1 0 18449 0 0 0 116760 125 0 0 25 0 1 0 1788597121 77692928 18113 4294967295 134512640 135094434 3221224432 3221223072 134562104 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/3251/statm): 18968 18113 145 145 0 18823 0 [pid=3251] vsize: 75872 Current children cumulated CPU time (s) 1168.86 Current children cumulated vsize (Kb) 77996 [startup+1180.67 s] Raw data (loadavg): 1.00 0.98 0.98 2/57 3251 Raw data (/proc/3247/stat): 3247 (minisat+_script) S 3246 3247 22582 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788597116 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/3247/statm): 531 226 485 147 0 384 0 [pid=3247] vsize: 2124 Raw data (/proc/3251/stat): 3251 (minisat+_64-bit) R 3247 3247 22582 0 -1 0 18590 0 0 0 117756 127 0 0 25 0 1 0 1788597121 78262272 18254 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/3251/statm): 19107 18254 145 145 0 18962 0 [pid=3251] vsize: 76428 Current children cumulated CPU time (s) 1178.84 Current children cumulated vsize (Kb) 78552 [startup+1190.68 s] Raw data (loadavg): 1.00 0.98 0.98 2/57 3251 Raw data (/proc/3247/stat): 3247 (minisat+_script) S 3246 3247 22582 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788597116 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/3247/statm): 531 226 485 147 0 384 0 [pid=3247] vsize: 2124 Raw data (/proc/3251/stat): 3251 (minisat+_64-bit) R 3247 3247 22582 0 -1 0 18713 0 0 0 118753 129 0 0 25 0 1 0 1788597121 78749696 18377 4294967295 134512640 135094434 3221224432 3221223088 134558159 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/3251/statm): 19226 18377 145 145 0 19081 0 [pid=3251] vsize: 76904 Current children cumulated CPU time (s) 1188.83 Current children cumulated vsize (Kb) 79028 [startup+1200.68 s] Raw data (loadavg): 1.00 0.98 0.98 2/57 3251 Raw data (/proc/3247/stat): 3247 (minisat+_script) S 3246 3247 22582 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788597116 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/3247/statm): 531 226 485 147 0 384 0 [pid=3247] vsize: 2124 Raw data (/proc/3251/stat): 3251 (minisat+_64-bit) R 3247 3247 22582 0 -1 0 18828 0 0 0 119749 130 0 0 25 0 1 0 1788597121 79208448 18492 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/3251/statm): 19338 18492 145 145 0 19193 0 [pid=3251] vsize: 77352 Current children cumulated CPU time (s) 1198.8 Current children cumulated vsize (Kb) 79476 [startup+1210.68 s] Raw data (loadavg): 1.00 0.98 0.98 2/57 3251 Raw data (/proc/3247/stat): 3247 (minisat+_script) S 3246 3247 22582 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788597116 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/3247/statm): 531 226 485 147 0 384 0 [pid=3247] vsize: 2124 Raw data (/proc/3251/stat): 3251 (minisat+_64-bit) R 3247 3247 22582 0 -1 0 18965 0 0 0 120746 132 0 0 25 0 1 0 1788597121 79753216 18629 4294967295 134512640 135094434 3221224432 3221223056 134557606 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/3251/statm): 19471 18629 145 145 0 19326 0 [pid=3251] vsize: 77884 Current children cumulated CPU time (s) 1208.79 Current children cumulated vsize (Kb) 80008 Maximum CPU time exceeded: sending SIGTERM then SIGKILL [startup+1210.68 s] Raw data (loadavg): 1.00 0.98 0.98 2/57 3251 Raw data (/proc/3247/stat): 3247 (minisat+_script) S 3246 3247 22582 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788597116 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/3247/statm): 531 226 485 147 0 384 0 [pid=3247] vsize: 2124 Raw data (/proc/3251/stat): 3251 (minisat+_64-bit) R 3247 3247 22582 0 -1 0 18965 0 0 0 120746 132 0 0 25 0 1 0 1788597121 79753216 18629 4294967295 134512640 135094434 3221224432 3221223056 134557606 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/3251/statm): 19471 18629 145 145 0 19326 0 [pid=3251] vsize: 77884 Current children cumulated CPU time (s) 1208.79 Current children cumulated vsize (Kb) 80008 Sending SIGTERM to -3247 Sleeping 2 seconds One traced child (pid=3247) ended because it received signal 15 (SIGTERM) One traced child (pid=3251) exited with status: 0 All traced children have exited ! Game is over. Child status: 0 Real time (s): 1210.72 CPU time (s): 1208.83 CPU user time (s): 1207.47 CPU system time (s): 1.36179 CPU usage (%): 99.8438 Max. virtual memory (cumulated for all children) (Kb): 80008
ERROR: no interpretation found !