Name | mps-v2-20-10/ftp.netlib.org/lp/data/normalized-mps-v2-20-10-sctap1.opb |
MD5SUM | 3742d8a4a6db91830db1829244573c45 |
Bench Category | optimization, big integers (OPTBIGINT) |
Has Objective Function | YES |
Satisfiable | YES |
(Un)Satisfiability was proved | YES |
Best value of the objective function | 49064968192 |
Optimality of the best value was proved | NO |
Number of terms in the objective function | 10800 |
Biggest coefficient in the objective function | 42949672960 |
Number of bits for the biggest coefficient in the objective function | 36 |
Sum of the numbers in the objective function | 6356551592160 |
Number of bits of the sum of numbers in the objective function | 43 |
Biggest number in a constraint | 42949672960 |
Number of bits of the biggest number in a constraint | 36 |
Biggest sum of numbers in a constraint | 6356551592160 |
Number of bits of the biggest sum of numbers | 43 |
Best result obtained on this benchmark | SAT |
Best CPU time to get the best result obtained on this benchmark | 1218.61 |
Number of variables | 14400 |
Total number of constraints | 300 |
Number of constraints which are clauses | 0 |
Number of constraints which are cardinality constraints (but not clauses) | 0 |
Number of constraints which are nor clauses,nor cardinality constraints | 300 |
Minimum length of a constraint | 90 |
Maximum length of a constraint | 660 |
LAUNCH ON wulflinc27 THE 2005-09-18 20:33:43 (client local time) PB2005-SCRIPT v4.0 MARKUPS: idlaunch=2810 boxname=wulflinc27 idbench=466 idsolver=3 numberseed=0 MD5SUM SOLVER: MD5SUM BENCH: 3742d8a4a6db91830db1829244573c45 /oldhome/oroussel/tmp/wulflinc27/normalized-mps-v2-20-10-sctap1.opb REAL COMMAND: minisat+_script /oldhome/oroussel/tmp/wulflinc27/normalized-mps-v2-20-10-sctap1.opb IDLAUNCH: 2810 /proc/cpuinfo: processor : 0 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 3 cpu MHz : 451.169 cache size : 512 KB fdiv_bug : no hlt_bug : no f00f_bug : no coma_bug : no fpu : yes fpu_exception : yes cpuid level : 2 wp : yes flags : fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse bogomips : 888.83 processor : 1 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 3 cpu MHz : 451.169 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: 904432 kB Buffers: 36152 kB Cached: 61480 kB SwapCached: 764 kB Active: 68688 kB Inactive: 31580 kB HighTotal: 131008 kB HighFree: 66892 kB LowTotal: 903652 kB LowFree: 837540 kB SwapTotal: 2097892 kB SwapFree: 2096616 kB Dirty: 28 kB Writeback: 0 kB Mapped: 5724 kB Slab: 24344 kB Committed_AS: 64168 kB PageTables: 328 kB VmallocTotal: 114680 kB VmallocUsed: 1368 kB VmallocChunk: 113252 kB JOB ENDED THE 2005-09-18 20:53:53 (client local time) WITH STATUS 0 IN 1208.49 SECONDS stats: 2810 7 1208.49 0
c Parsing PB file... c Converting 404 PB-constraints to clauses... c -- Unit propagations: (none) c -- Detecting intervals from adjacent constraints: ######################################################################################################################## c -- Clauses(.)/Splits(s): ss c ---[ 405]---> Sorter-cost: 1645 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 ---[ 404]---> Sorter-cost: 1645 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 ---[ 403]---> Sorter-cost: 1645 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 ---[ 402]---> Sorter-cost: 1645 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 ---[ 401]---> Sorter-cost: 1645 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 ---[ 400]---> Sorter-cost: 1645 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 ---[ 399]---> Sorter-cost: 1645 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 ---[ 398]---> Sorter-cost: 1645 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]---> Sorter-cost: 1645 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 ---[ 396]---> Sorter-cost: 3051 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 ---[ 395]---> Sorter-cost: 3051 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 ---[ 394]---> Sorter-cost: 3051 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 ---[ 393]---> Sorter-cost: 3051 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 ---[ 392]---> Sorter-cost: 3051 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 ---[ 391]---> Sorter-cost: 3051 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 ---[ 390]---> Sorter-cost: 3051 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 ---[ 389]---> Sorter-cost: 3051 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 ---[ 388]---> Sorter-cost: 3051 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 ---[ 387]---> Sorter-cost: 2697 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 ---[ 386]---> Sorter-cost: 2697 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 ---[ 385]---> Sorter-cost: 2697 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 ---[ 384]---> Sorter-cost: 2697 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 ---[ 383]---> Sorter-cost: 2697 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 ---[ 382]---> Sorter-cost: 2697 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 ---[ 381]---> Sorter-cost: 2697 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 ---[ 380]---> Sorter-cost: 2697 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 ---[ 379]---> Sorter-cost: 2697 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 ---[ 378]---> Sorter-cost: 1645 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 ---[ 377]---> Sorter-cost: 1645 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 ---[ 376]---> Sorter-cost: 1645 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 ---[ 375]---> Sorter-cost: 1645 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: 1645 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 ---[ 373]---> Sorter-cost: 1645 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 ---[ 372]---> Sorter-cost: 1645 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 ---[ 371]---> Sorter-cost: 1645 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 ---[ 370]---> Sorter-cost: 1645 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 ---[ 369]---> Sorter-cost: 3051 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 ---[ 368]---> Sorter-cost: 3051 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 ---[ 367]---> Sorter-cost: 3051 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 ---[ 366]---> Sorter-cost: 3051 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 ---[ 365]---> Sorter-cost: 3051 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 ---[ 364]---> Sorter-cost: 3051 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 ---[ 363]---> Sorter-cost: 3051 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: 3051 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 ---[ 361]---> Sorter-cost: 3051 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 ---[ 360]---> Sorter-cost: 1645 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 ---[ 359]---> Sorter-cost: 1645 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 ---[ 358]---> Sorter-cost: 1645 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 ---[ 357]---> Sorter-cost: 1645 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 ---[ 356]---> Sorter-cost: 1645 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 ---[ 355]---> Sorter-cost: 1645 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 ---[ 354]---> Sorter-cost: 1645 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 ---[ 353]---> Sorter-cost: 1645 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 ---[ 352]---> Sorter-cost: 1645 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 ---[ 351]---> Sorter-cost: 3051 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: 3051 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 ---[ 349]---> Sorter-cost: 3051 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 ---[ 348]---> Sorter-cost: 3051 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 ---[ 347]---> Sorter-cost: 3051 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 ---[ 346]---> Sorter-cost: 3051 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 ---[ 345]---> Sorter-cost: 3051 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 ---[ 344]---> Sorter-cost: 3051 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 ---[ 343]---> Sorter-cost: 3051 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 ---[ 342]---> Sorter-cost: 3051 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 ---[ 341]---> Sorter-cost: 3051 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 ---[ 340]---> Sorter-cost: 3051 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 ---[ 339]---> Sorter-cost: 3051 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: 3051 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 ---[ 337]---> Sorter-cost: 3051 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 ---[ 336]---> Sorter-cost: 3051 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 ---[ 335]---> Sorter-cost: 3051 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 ---[ 334]---> Sorter-cost: 3051 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 ---[ 333]---> Sorter-cost: 1645 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 ---[ 332]---> Sorter-cost: 1645 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 ---[ 331]---> Sorter-cost: 1645 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 ---[ 330]---> Sorter-cost: 1645 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 ---[ 329]---> Sorter-cost: 1645 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 ---[ 328]---> Sorter-cost: 1645 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 ---[ 327]---> Sorter-cost: 1645 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: 1645 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 ---[ 325]---> Sorter-cost: 1645 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 ---[ 324]---> Sorter-cost: 1645 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 ---[ 323]---> Sorter-cost: 1645 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 ---[ 322]---> Sorter-cost: 1645 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 ---[ 321]---> Sorter-cost: 1645 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 ---[ 320]---> Sorter-cost: 1645 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 ---[ 319]---> Sorter-cost: 1645 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 ---[ 318]---> Sorter-cost: 1645 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 ---[ 317]---> Sorter-cost: 1645 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 ---[ 316]---> Sorter-cost: 1645 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 ---[ 315]---> Sorter-cost: 2746 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: 2746 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 ---[ 313]---> Sorter-cost: 2746 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: 2746 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 ---[ 311]---> Sorter-cost: 2746 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 ---[ 310]---> Sorter-cost: 2746 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 ---[ 309]---> Sorter-cost: 2746 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 ---[ 308]---> Sorter-cost: 2746 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 ---[ 307]---> Sorter-cost: 2746 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 ---[ 306]---> Sorter-cost: 2746 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 ---[ 305]---> Sorter-cost: 2746 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 ---[ 304]---> Sorter-cost: 2746 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 ---[ 303]---> Sorter-cost: 2746 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 ---[ 302]---> Sorter-cost: 2746 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 ---[ 301]---> Sorter-cost: 2746 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: 2746 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 ---[ 299]---> Sorter-cost: 2746 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 ---[ 298]---> Sorter-cost: 2746 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 ---[ 296]---> Sorter-cost: 237 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 294]---> Sorter-cost: 237 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 292]---> Sorter-cost: 237 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 290]---> Sorter-cost: 237 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 288]---> Sorter-cost: 237 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 286]---> Sorter-cost: 237 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 284]---> Sorter-cost: 237 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 282]---> Sorter-cost: 237 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 280]---> Sorter-cost: 237 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 278]---> Sorter-cost: 237 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 276]---> Sorter-cost: 217 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 274]---> Sorter-cost: 237 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 272]---> Sorter-cost: 217 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 270]---> Sorter-cost: 217 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 268]---> Sorter-cost: 217 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 266]---> Sorter-cost: 217 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 264]---> Sorter-cost: 217 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 262]---> Sorter-cost: 217 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 260]---> Sorter-cost: 217 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 258]---> Sorter-cost: 217 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 256]---> Sorter-cost: 235 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 254]---> Sorter-cost: 237 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 252]---> Sorter-cost: 235 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 250]---> Sorter-cost: 235 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 248]---> Sorter-cost: 235 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 246]---> Sorter-cost: 235 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 244]---> Sorter-cost: 235 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 242]---> Sorter-cost: 235 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 240]---> Sorter-cost: 235 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 238]---> Sorter-cost: 235 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 236]---> Sorter-cost: 237 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 234]---> Sorter-cost: 237 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 232]---> Sorter-cost: 237 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 230]---> Sorter-cost: 237 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 228]---> Sorter-cost: 237 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 226]---> Sorter-cost: 237 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 224]---> Sorter-cost: 237 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 222]---> Sorter-cost: 237 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 220]---> Sorter-cost: 237 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 218]---> Sorter-cost: 237 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 216]---> Sorter-cost: 217 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 214]---> Sorter-cost: 237 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 212]---> Sorter-cost: 217 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 210]---> Sorter-cost: 217 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 208]---> Sorter-cost: 217 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 206]---> Sorter-cost: 217 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 204]---> Sorter-cost: 217 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 202]---> Sorter-cost: 217 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 200]---> Sorter-cost: 217 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 198]---> Sorter-cost: 217 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 196]---> Sorter-cost: 237 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 194]---> Sorter-cost: 237 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 192]---> Sorter-cost: 237 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 190]---> Sorter-cost: 237 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 188]---> Sorter-cost: 237 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 186]---> Sorter-cost: 237 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 184]---> Sorter-cost: 237 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 182]---> Sorter-cost: 237 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 180]---> Sorter-cost: 237 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 178]---> Sorter-cost: 237 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 176]---> Sorter-cost: 217 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 174]---> Sorter-cost: 237 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 172]---> Sorter-cost: 217 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 170]---> Sorter-cost: 217 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 168]---> Sorter-cost: 217 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 166]---> Sorter-cost: 217 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 164]---> Sorter-cost: 217 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 162]---> Sorter-cost: 217 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 160]---> Sorter-cost: 217 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 158]---> Sorter-cost: 217 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 156]---> Sorter-cost: 217 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 154]---> Sorter-cost: 237 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 152]---> Sorter-cost: 217 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 150]---> Sorter-cost: 217 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 148]---> Sorter-cost: 217 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 146]---> Sorter-cost: 217 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 144]---> Sorter-cost: 217 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 142]---> Sorter-cost: 217 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 140]---> Sorter-cost: 217 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 138]---> Sorter-cost: 217 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 136]---> Sorter-cost: 237 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 134]---> Sorter-cost: 237 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 132]---> Sorter-cost: 237 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 130]---> Sorter-cost: 237 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 128]---> Sorter-cost: 237 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 126]---> Sorter-cost: 237 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 124]---> Sorter-cost: 237 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 122]---> Sorter-cost: 237 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 120]---> Sorter-cost: 237 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 118]---> Sorter-cost: 237 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 116]---> Sorter-cost: 237 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 114]---> Sorter-cost: 237 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 112]---> Sorter-cost: 237 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 110]---> Sorter-cost: 237 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 108]---> Sorter-cost: 237 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 106]---> Sorter-cost: 237 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 104]---> Sorter-cost: 237 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 102]---> Sorter-cost: 237 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 100]---> Sorter-cost: 237 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 98]---> Sorter-cost: 237 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 96]---> Sorter-cost: 219 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 94]---> Sorter-cost: 237 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 92]---> Sorter-cost: 219 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 90]---> Sorter-cost: 219 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 88]---> Sorter-cost: 219 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 86]---> Sorter-cost: 219 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 84]---> Sorter-cost: 219 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 82]---> Sorter-cost: 219 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 80]---> Sorter-cost: 219 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 78]---> Sorter-cost: 219 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 76]---> Sorter-cost: 219 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 74]---> Sorter-cost: 237 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 72]---> Sorter-cost: 219 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 70]---> Sorter-cost: 219 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 68]---> Sorter-cost: 219 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 66]---> Sorter-cost: 219 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 64]---> Sorter-cost: 219 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 62]---> Sorter-cost: 219 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 60]---> Sorter-cost: 219 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 58]---> Sorter-cost: 219 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 57]---> Adder-cost: 700 maxlim: 2147559384 bits: 33/32 c ---[ 55]---> Adder-cost: 700 maxlim: 2147569624 bits: 33/32 c ---[ 54]---> Adder-cost: 700 maxlim: 2147579864 bits: 33/32 c ---[ 53]---> Adder-cost: 700 maxlim: 2147569624 bits: 33/32 c ---[ 52]---> Adder-cost: 700 maxlim: 2147562456 bits: 33/32 c ---[ 51]---> Adder-cost: 700 maxlim: 2147559384 bits: 33/32 c ---[ 50]---> Adder-cost: 700 maxlim: 2147559384 bits: 33/32 c ---[ 49]---> Adder-cost: 700 maxlim: 2147559384 bits: 33/32 c ---[ 48]---> Adder-cost: 700 maxlim: 2147559384 bits: 33/32 c ---[ 47]---> Adder-cost: 1224 maxlim: 4295067594 bits: 34/33 c ---[ 45]---> Adder-cost: 1224 maxlim: 4295098314 bits: 34/33 c ---[ 44]---> Adder-cost: 1224 maxlim: 4295108554 bits: 34/33 c ---[ 43]---> Adder-cost: 1224 maxlim: 4295098314 bits: 34/33 c ---[ 42]---> Adder-cost: 1224 maxlim: 4295093194 bits: 34/33 c ---[ 41]---> Adder-cost: 1224 maxlim: 4295088074 bits: 34/33 c ---[ 40]---> Adder-cost: 1224 maxlim: 4295077834 bits: 34/33 c ---[ 39]---> Adder-cost: 1224 maxlim: 4295067594 bits: 34/33 c ---[ 38]---> Adder-cost: 1224 maxlim: 4295067594 bits: 34/33 c ---[ 37]---> Sorter-cost: 3604 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 ---[ 36]---> Sorter-cost: 3612 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 ---[ 35]---> Sorter-cost: 3604 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 ---[ 34]---> Sorter-cost: 3604 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 ---[ 33]---> Sorter-cost: 3604 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 ---[ 32]---> Sorter-cost: 3604 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 ---[ 31]---> Sorter-cost: 3604 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 ---[ 30]---> Sorter-cost: 3604 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 ---[ 29]---> Sorter-cost: 3604 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 ---[ 28]---> Adder-cost: 906 maxlim: 2147772272 bits: 33/32 c ---[ 27]---> Adder-cost: 906 maxlim: 2147777392 bits: 33/32 c ---[ 26]---> Adder-cost: 906 maxlim: 2147782512 bits: 33/32 c ---[ 25]---> Adder-cost: 906 maxlim: 2147792752 bits: 33/32 c ---[ 24]---> Adder-cost: 906 maxlim: 2147787632 bits: 33/32 c ---[ 23]---> Adder-cost: 906 maxlim: 2147782512 bits: 33/32 c ---[ 22]---> Adder-cost: 906 maxlim: 2147782512 bits: 33/32 c ---[ 21]---> Adder-cost: 906 maxlim: 2147777392 bits: 33/32 c ---[ 20]---> Adder-cost: 906 maxlim: 2147772272 bits: 33/32 c ---[ 19]---> Adder-cost: 968 maxlim: 2147759990 bits: 33/32 c ---[ 18]---> Adder-cost: 968 maxlim: 2147759990 bits: 33/32 c ---[ 17]---> Adder-cost: 968 maxlim: 2147775350 bits: 33/32 c ---[ 16]---> Adder-cost: 968 maxlim: 2147800950 bits: 33/32 c ---[ 15]---> Adder-cost: 968 maxlim: 2147790710 bits: 33/32 c ---[ 14]---> Adder-cost: 968 maxlim: 2147780470 bits: 33/32 c ---[ 13]---> Adder-cost: 968 maxlim: 2147770230 bits: 33/32 c ---[ 12]---> Adder-cost: 968 maxlim: 2147759990 bits: 33/32 c ---[ 11]---> Adder-cost: 968 maxlim: 2147759990 bits: 33/32 c ---[ 10]---> Adder-cost: 442 maxlim: 1073807326 bits: 32/31 c ---[ 9]---> Adder-cost: 442 maxlim: 1073807326 bits: 32/31 c ---[ 8]---> Adder-cost: 442 maxlim: 1073807326 bits: 32/31 c ---[ 7]---> Adder-cost: 442 maxlim: 1073807326 bits: 32/31 c ---[ 6]---> Adder-cost: 442 maxlim: 1073812446 bits: 32/31 c ---[ 5]---> Adder-cost: 442 maxlim: 1073822686 bits: 32/31 c ---[ 4]---> Adder-cost: 442 maxlim: 1073827806 bits: 32/31 c ---[ 3]---> Adder-cost: 442 maxlim: 1073817566 bits: 32/31 c ---[ 2]---> Adder-cost: 442 maxlim: 1073812446 bits: 32/31 c ---[ 1]---> Adder-cost: 226 maxlim: 5119 bits: 14/13 c ---[ 0]---> Adder-cost: 435 maxlim: 5119 bits: 14/13 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 0 | 1087332 2874465 | 362444 0 0 nan | 0.000 % | c | 100 | 1087332 2874465 | 398688 100 786 7.9 | 2.890 % | c | 253 | 1087302 2874399 | 438557 252 1656 6.6 | 2.893 % | c | 478 | 1087281 2874353 | 482412 476 3907 8.2 | 2.894 % | c | 815 | 1087232 2874245 | 530654 810 6543 8.1 | 2.899 % | c | 1321 | 1087218 2874214 | 583719 1315 10917 8.3 | 2.900 % | c | 2080 | 1087167 2874103 | 642091 2070 19416 9.4 | 2.904 % | c | 3219 | 1087108 2873972 | 706300 3202 30209 9.4 | 2.909 % | c | 4928 | 1087108 2873972 | 776930 4911 46317 9.4 | 2.909 % | c | 7492 | 1087078 2873905 | 854623 7473 66923 9.0 | 2.912 % | c | 11336 | 1087040 2873821 | 940086 11316 100803 8.9 | 2.915 % | c | 17102 | 1086682 2873027 | 1034095 17062 146933 8.6 | 2.943 % | c | 25751 | 1085819 2871117 | 1137504 25671 237679 9.3 | 3.012 % | c | 38726 | 1085257 2869872 | 1251254 38617 345891 9.0 | 3.057 % | c | 58187 | 1083917 2866886 | 1376380 58015 530876 9.2 | 3.167 % | c | 87380 | 1082317 2863339 | 1514018 87084 827993 9.5 | 3.300 % | c | 131169 | 1079997 2858186 | 1665420 130771 1237628 9.5 | 3.489 % | c | 196855 | 1076637 2850709 | 1831962 196279 1940424 9.9 | 3.768 % |
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/10668/stat): 10668 (minisat+_script) R 10667 10668 28974 0 -1 0 19 0 0 0 0 0 0 0 23 0 1 0 1844152611 712704 3 4294967295 134512640 135087896 3221224496 3221224496 1073744960 0 0 5 0 0 0 0 17 0 0 0 Raw data (/proc/10668/statm): 174 3 169 147 0 27 0 [pid=10668] 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=10669 New process pid=10670 New process pid=10671 execve syscall for /bin/sed executable One traced child (pid=10670) 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=10671) exited with status: 0 One traced child (pid=10669) exited with status: 0 New process pid=10672 execve syscall for /oldhome/oroussel/solvers/minisat+_64-bit_static executable open syscall for file /dev/null open syscall for file /oldhome/oroussel/tmp/wulflinc27/normalized-mps-v2-20-10-sctap1.opb [startup+10.0036 s] Raw data (loadavg): 0.93 0.95 0.90 2/57 10672 Raw data (/proc/10668/stat): 10668 (minisat+_script) S 10667 10668 28974 0 -1 0 289 239 0 0 0 0 0 0 18 0 1 0 1844152611 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/10668/statm): 531 226 485 147 0 384 0 [pid=10668] vsize: 2124 Raw data (/proc/10672/stat): 10672 (minisat+_64-bit) R 10668 10668 28974 0 -1 0 6693 0 0 0 952 23 0 0 25 0 1 0 1844152616 24170496 5313 4294967295 134512640 135094434 3221224432 3221222324 134600671 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/10672/statm): 5901 5313 145 145 0 5756 0 [pid=10672] vsize: 23604 Current children cumulated CPU time (s) 9.75 Current children cumulated vsize (Kb) 25728 [startup+20.0044 s] Raw data (loadavg): 0.94 0.96 0.91 2/57 10672 Raw data (/proc/10668/stat): 10668 (minisat+_script) S 10667 10668 28974 0 -1 0 289 239 0 0 0 0 0 0 18 0 1 0 1844152611 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/10668/statm): 531 226 485 147 0 384 0 [pid=10668] vsize: 2124 Raw data (/proc/10672/stat): 10672 (minisat+_64-bit) R 10668 10668 28974 0 -1 0 26538 0 0 0 1779 109 0 0 22 0 1 0 1844152616 120233984 25151 4294967295 134512640 135094434 3221224432 3221185804 134563744 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/10672/statm): 29354 25151 145 145 0 29209 0 [pid=10672] vsize: 117416 Current children cumulated CPU time (s) 18.88 Current children cumulated vsize (Kb) 119540 [startup+30.0063 s] Raw data (loadavg): 0.95 0.96 0.91 2/57 10672 Raw data (/proc/10668/stat): 10668 (minisat+_script) S 10667 10668 28974 0 -1 0 289 239 0 0 0 0 0 0 18 0 1 0 1844152611 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/10668/statm): 531 226 485 147 0 384 0 [pid=10668] vsize: 2124 Raw data (/proc/10672/stat): 10672 (minisat+_64-bit) R 10668 10668 28974 0 -1 0 29490 0 0 0 2751 122 0 0 25 0 1 0 1844152616 133668864 28103 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/10672/statm): 32634 28103 145 145 0 32489 0 [pid=10672] vsize: 130536 Current children cumulated CPU time (s) 28.73 Current children cumulated vsize (Kb) 132660 [startup+40.0071 s] Raw data (loadavg): 0.95 0.96 0.91 2/57 10672 Raw data (/proc/10668/stat): 10668 (minisat+_script) S 10667 10668 28974 0 -1 0 289 239 0 0 0 0 0 0 18 0 1 0 1844152611 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/10668/statm): 531 226 485 147 0 384 0 [pid=10668] vsize: 2124 Raw data (/proc/10672/stat): 10672 (minisat+_64-bit) R 10668 10668 28974 0 -1 0 29663 0 0 0 3748 122 0 0 25 0 1 0 1844152616 134250496 28276 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/10672/statm): 32776 28276 145 145 0 32631 0 [pid=10672] vsize: 131104 Current children cumulated CPU time (s) 38.7 Current children cumulated vsize (Kb) 133228 [startup+50.0089 s] Raw data (loadavg): 0.96 0.96 0.91 2/57 10672 Raw data (/proc/10668/stat): 10668 (minisat+_script) S 10667 10668 28974 0 -1 0 289 239 0 0 0 0 0 0 18 0 1 0 1844152611 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/10668/statm): 531 226 485 147 0 384 0 [pid=10668] vsize: 2124 Raw data (/proc/10672/stat): 10672 (minisat+_64-bit) R 10668 10668 28974 0 -1 0 29735 0 0 0 4747 123 0 0 25 0 1 0 1844152616 134512640 28348 4294967295 134512640 135094434 3221224432 3221223120 134554746 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/10672/statm): 32840 28348 145 145 0 32695 0 [pid=10672] vsize: 131360 Current children cumulated CPU time (s) 48.7 Current children cumulated vsize (Kb) 133484 [startup+60.0097 s] Raw data (loadavg): 0.97 0.96 0.91 2/57 10672 Raw data (/proc/10668/stat): 10668 (minisat+_script) S 10667 10668 28974 0 -1 0 289 239 0 0 0 0 0 0 18 0 1 0 1844152611 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/10668/statm): 531 226 485 147 0 384 0 [pid=10668] vsize: 2124 Raw data (/proc/10672/stat): 10672 (minisat+_64-bit) R 10668 10668 28974 0 -1 0 29828 0 0 0 5745 124 0 0 25 0 1 0 1844152616 134836224 28441 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/10672/statm): 32919 28441 145 145 0 32774 0 [pid=10672] vsize: 131676 Current children cumulated CPU time (s) 58.69 Current children cumulated vsize (Kb) 133800 [startup+70.0105 s] Raw data (loadavg): 0.97 0.96 0.91 2/57 10672 Raw data (/proc/10668/stat): 10668 (minisat+_script) S 10667 10668 28974 0 -1 0 289 239 0 0 0 0 0 0 18 0 1 0 1844152611 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/10668/statm): 531 226 485 147 0 384 0 [pid=10668] vsize: 2124 Raw data (/proc/10672/stat): 10672 (minisat+_64-bit) R 10668 10668 28974 0 -1 0 29921 0 0 0 6744 125 0 0 25 0 1 0 1844152616 135147520 28534 4294967295 134512640 135094434 3221224432 3221223120 134554746 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/10672/statm): 32995 28534 145 145 0 32850 0 [pid=10672] vsize: 131980 Current children cumulated CPU time (s) 68.69 Current children cumulated vsize (Kb) 134104 [startup+80.0114 s] Raw data (loadavg): 0.98 0.96 0.91 2/57 10672 Raw data (/proc/10668/stat): 10668 (minisat+_script) S 10667 10668 28974 0 -1 0 289 239 0 0 0 0 0 0 18 0 1 0 1844152611 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/10668/statm): 531 226 485 147 0 384 0 [pid=10668] vsize: 2124 Raw data (/proc/10672/stat): 10672 (minisat+_64-bit) R 10668 10668 28974 0 -1 0 30008 0 0 0 7742 126 0 0 25 0 1 0 1844152616 135426048 28621 4294967295 134512640 135094434 3221224432 3221223092 134553515 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/10672/statm): 33063 28621 145 145 0 32918 0 [pid=10672] vsize: 132252 Current children cumulated CPU time (s) 78.68 Current children cumulated vsize (Kb) 134376 [startup+90.0122 s] Raw data (loadavg): 0.98 0.96 0.91 2/57 10672 Raw data (/proc/10668/stat): 10668 (minisat+_script) S 10667 10668 28974 0 -1 0 289 239 0 0 0 0 0 0 18 0 1 0 1844152611 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/10668/statm): 531 226 485 147 0 384 0 [pid=10668] vsize: 2124 Raw data (/proc/10672/stat): 10672 (minisat+_64-bit) R 10668 10668 28974 0 -1 0 30079 0 0 0 8741 126 0 0 25 0 1 0 1844152616 135647232 28692 4294967295 134512640 135094434 3221224432 3221223120 134554746 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/10672/statm): 33117 28692 145 145 0 32972 0 [pid=10672] vsize: 132468 Current children cumulated CPU time (s) 88.67 Current children cumulated vsize (Kb) 134592 [startup+100.014 s] Raw data (loadavg): 0.98 0.96 0.91 2/57 10672 Raw data (/proc/10668/stat): 10668 (minisat+_script) S 10667 10668 28974 0 -1 0 289 239 0 0 0 0 0 0 18 0 1 0 1844152611 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/10668/statm): 531 226 485 147 0 384 0 [pid=10668] vsize: 2124 Raw data (/proc/10672/stat): 10672 (minisat+_64-bit) R 10668 10668 28974 0 -1 0 30164 0 0 0 9740 127 0 0 25 0 1 0 1844152616 135974912 28777 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/10672/statm): 33197 28777 145 145 0 33052 0 [pid=10672] vsize: 132788 Current children cumulated CPU time (s) 98.67 Current children cumulated vsize (Kb) 134912 [startup+110.015 s] Raw data (loadavg): 0.98 0.96 0.91 2/57 10672 Raw data (/proc/10668/stat): 10668 (minisat+_script) S 10667 10668 28974 0 -1 0 289 239 0 0 0 0 0 0 18 0 1 0 1844152611 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/10668/statm): 531 226 485 147 0 384 0 [pid=10668] vsize: 2124 Raw data (/proc/10672/stat): 10672 (minisat+_64-bit) R 10668 10668 28974 0 -1 0 30238 0 0 0 10739 128 0 0 25 0 1 0 1844152616 136249344 28851 4294967295 134512640 135094434 3221224432 3221223056 134557596 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/10672/statm): 33264 28851 145 145 0 33119 0 [pid=10672] vsize: 133056 Current children cumulated CPU time (s) 108.67 Current children cumulated vsize (Kb) 135180 [startup+120.016 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 10672 Raw data (/proc/10668/stat): 10668 (minisat+_script) S 10667 10668 28974 0 -1 0 289 239 0 0 0 0 0 0 18 0 1 0 1844152611 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/10668/statm): 531 226 485 147 0 384 0 [pid=10668] vsize: 2124 Raw data (/proc/10672/stat): 10672 (minisat+_64-bit) R 10668 10668 28974 0 -1 0 30278 0 0 0 11739 128 0 0 25 0 1 0 1844152616 136404992 28891 4294967295 134512640 135094434 3221224432 3221223072 134562104 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/10672/statm): 33302 28891 145 145 0 33157 0 [pid=10672] vsize: 133208 Current children cumulated CPU time (s) 118.67 Current children cumulated vsize (Kb) 135332 [startup+130.016 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 10672 Raw data (/proc/10668/stat): 10668 (minisat+_script) S 10667 10668 28974 0 -1 0 289 239 0 0 0 0 0 0 18 0 1 0 1844152611 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/10668/statm): 531 226 485 147 0 384 0 [pid=10668] vsize: 2124 Raw data (/proc/10672/stat): 10672 (minisat+_64-bit) R 10668 10668 28974 0 -1 0 30317 0 0 0 12738 128 0 0 25 0 1 0 1844152616 136556544 28930 4294967295 134512640 135094434 3221224432 3221223092 134553512 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/10672/statm): 33339 28930 145 145 0 33194 0 [pid=10672] vsize: 133356 Current children cumulated CPU time (s) 128.66 Current children cumulated vsize (Kb) 135480 [startup+140.017 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 10672 Raw data (/proc/10668/stat): 10668 (minisat+_script) S 10667 10668 28974 0 -1 0 289 239 0 0 0 0 0 0 18 0 1 0 1844152611 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/10668/statm): 531 226 485 147 0 384 0 [pid=10668] vsize: 2124 Raw data (/proc/10672/stat): 10672 (minisat+_64-bit) R 10668 10668 28974 0 -1 0 30394 0 0 0 13737 128 0 0 25 0 1 0 1844152616 136994816 29007 4294967295 134512640 135094434 3221224432 3221223120 134554788 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/10672/statm): 33446 29007 145 145 0 33301 0 [pid=10672] vsize: 133784 Current children cumulated CPU time (s) 138.65 Current children cumulated vsize (Kb) 135908 [startup+150.019 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 10672 Raw data (/proc/10668/stat): 10668 (minisat+_script) S 10667 10668 28974 0 -1 0 289 239 0 0 0 0 0 0 18 0 1 0 1844152611 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/10668/statm): 531 226 485 147 0 384 0 [pid=10668] vsize: 2124 Raw data (/proc/10672/stat): 10672 (minisat+_64-bit) R 10668 10668 28974 0 -1 0 30398 0 0 0 14737 129 0 0 25 0 1 0 1844152616 137007104 29011 4294967295 134512640 135094434 3221224432 3221223056 134557596 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/10672/statm): 33449 29011 145 145 0 33304 0 [pid=10672] vsize: 133796 Current children cumulated CPU time (s) 148.66 Current children cumulated vsize (Kb) 135920 [startup+160.02 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 10672 Raw data (/proc/10668/stat): 10668 (minisat+_script) S 10667 10668 28974 0 -1 0 289 239 0 0 0 0 0 0 18 0 1 0 1844152611 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/10668/statm): 531 226 485 147 0 384 0 [pid=10668] vsize: 2124 Raw data (/proc/10672/stat): 10672 (minisat+_64-bit) R 10668 10668 28974 0 -1 0 30444 0 0 0 15736 129 0 0 25 0 1 0 1844152616 137158656 29057 4294967295 134512640 135094434 3221224432 3221223092 134553446 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/10672/statm): 33486 29057 145 145 0 33341 0 [pid=10672] vsize: 133944 Current children cumulated CPU time (s) 158.65 Current children cumulated vsize (Kb) 136068 [startup+170.02 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 10672 Raw data (/proc/10668/stat): 10668 (minisat+_script) S 10667 10668 28974 0 -1 0 289 239 0 0 0 0 0 0 18 0 1 0 1844152611 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/10668/statm): 531 226 485 147 0 384 0 [pid=10668] vsize: 2124 Raw data (/proc/10672/stat): 10672 (minisat+_64-bit) R 10668 10668 28974 0 -1 0 30487 0 0 0 16736 129 0 0 25 0 1 0 1844152616 137326592 29100 4294967295 134512640 135094434 3221224432 3221223120 134554731 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/10672/statm): 33527 29100 145 145 0 33382 0 [pid=10672] vsize: 134108 Current children cumulated CPU time (s) 168.65 Current children cumulated vsize (Kb) 136232 [startup+180.021 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 10672 Raw data (/proc/10668/stat): 10668 (minisat+_script) S 10667 10668 28974 0 -1 0 289 239 0 0 0 0 0 0 18 0 1 0 1844152611 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/10668/statm): 531 226 485 147 0 384 0 [pid=10668] vsize: 2124 Raw data (/proc/10672/stat): 10672 (minisat+_64-bit) R 10668 10668 28974 0 -1 0 30534 0 0 0 17735 130 0 0 25 0 1 0 1844152616 137469952 29147 4294967295 134512640 135094434 3221224432 3221223044 134563049 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/10672/statm): 33562 29147 145 145 0 33417 0 [pid=10672] vsize: 134248 Current children cumulated CPU time (s) 178.65 Current children cumulated vsize (Kb) 136372 [startup+190.022 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 10672 Raw data (/proc/10668/stat): 10668 (minisat+_script) S 10667 10668 28974 0 -1 0 289 239 0 0 0 0 0 0 18 0 1 0 1844152611 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/10668/statm): 531 226 485 147 0 384 0 [pid=10668] vsize: 2124 Raw data (/proc/10672/stat): 10672 (minisat+_64-bit) R 10668 10668 28974 0 -1 0 30578 0 0 0 18733 131 0 0 25 0 1 0 1844152616 137641984 29191 4294967295 134512640 135094434 3221224432 3221223120 134554746 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/10672/statm): 33604 29191 145 145 0 33459 0 [pid=10672] vsize: 134416 Current children cumulated CPU time (s) 188.64 Current children cumulated vsize (Kb) 136540 [startup+200.023 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 10672 Raw data (/proc/10668/stat): 10668 (minisat+_script) S 10667 10668 28974 0 -1 0 289 239 0 0 0 0 0 0 18 0 1 0 1844152611 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/10668/statm): 531 226 485 147 0 384 0 [pid=10668] vsize: 2124 Raw data (/proc/10672/stat): 10672 (minisat+_64-bit) R 10668 10668 28974 0 -1 0 30624 0 0 0 19733 131 0 0 25 0 1 0 1844152616 137809920 29237 4294967295 134512640 135094434 3221224432 3221223044 134563055 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/10672/statm): 33645 29237 145 145 0 33500 0 [pid=10672] vsize: 134580 Current children cumulated CPU time (s) 198.64 Current children cumulated vsize (Kb) 136704 [startup+210.024 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 10672 Raw data (/proc/10668/stat): 10668 (minisat+_script) S 10667 10668 28974 0 -1 0 289 239 0 0 0 0 0 0 18 0 1 0 1844152611 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/10668/statm): 531 226 485 147 0 384 0 [pid=10668] vsize: 2124 Raw data (/proc/10672/stat): 10672 (minisat+_64-bit) R 10668 10668 28974 0 -1 0 30674 0 0 0 20732 132 0 0 25 0 1 0 1844152616 138006528 29287 4294967295 134512640 135094434 3221224432 3221223044 134563059 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/10672/statm): 33693 29287 145 145 0 33548 0 [pid=10672] vsize: 134772 Current children cumulated CPU time (s) 208.64 Current children cumulated vsize (Kb) 136896 [startup+220.025 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 10672 Raw data (/proc/10668/stat): 10668 (minisat+_script) S 10667 10668 28974 0 -1 0 289 239 0 0 0 0 0 0 18 0 1 0 1844152611 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/10668/statm): 531 226 485 147 0 384 0 [pid=10668] vsize: 2124 Raw data (/proc/10672/stat): 10672 (minisat+_64-bit) R 10668 10668 28974 0 -1 0 30703 0 0 0 21731 132 0 0 25 0 1 0 1844152616 138117120 29316 4294967295 134512640 135094434 3221224432 3221223088 134558402 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/10672/statm): 33720 29316 145 145 0 33575 0 [pid=10672] vsize: 134880 Current children cumulated CPU time (s) 218.63 Current children cumulated vsize (Kb) 137004 [startup+230.026 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 10672 Raw data (/proc/10668/stat): 10668 (minisat+_script) S 10667 10668 28974 0 -1 0 289 239 0 0 0 0 0 0 18 0 1 0 1844152611 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/10668/statm): 531 226 485 147 0 384 0 [pid=10668] vsize: 2124 Raw data (/proc/10672/stat): 10672 (minisat+_64-bit) R 10668 10668 28974 0 -1 0 30739 0 0 0 22731 132 0 0 25 0 1 0 1844152616 138256384 29352 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/10672/statm): 33754 29352 145 145 0 33609 0 [pid=10672] vsize: 135016 Current children cumulated CPU time (s) 228.63 Current children cumulated vsize (Kb) 137140 [startup+240.027 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 10672 Raw data (/proc/10668/stat): 10668 (minisat+_script) S 10667 10668 28974 0 -1 0 289 239 0 0 0 0 0 0 18 0 1 0 1844152611 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/10668/statm): 531 226 485 147 0 384 0 [pid=10668] vsize: 2124 Raw data (/proc/10672/stat): 10672 (minisat+_64-bit) R 10668 10668 28974 0 -1 0 30766 0 0 0 23731 133 0 0 25 0 1 0 1844152616 138362880 29379 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/10672/statm): 33780 29379 145 145 0 33635 0 [pid=10672] vsize: 135120 Current children cumulated CPU time (s) 238.64 Current children cumulated vsize (Kb) 137244 [startup+250.028 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 10672 Raw data (/proc/10668/stat): 10668 (minisat+_script) S 10667 10668 28974 0 -1 0 289 239 0 0 0 0 0 0 18 0 1 0 1844152611 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/10668/statm): 531 226 485 147 0 384 0 [pid=10668] vsize: 2124 Raw data (/proc/10672/stat): 10672 (minisat+_64-bit) R 10668 10668 28974 0 -1 0 30810 0 0 0 24730 133 0 0 25 0 1 0 1844152616 138510336 29423 4294967295 134512640 135094434 3221224432 3221223116 134553432 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/10672/statm): 33816 29423 145 145 0 33671 0 [pid=10672] vsize: 135264 Current children cumulated CPU time (s) 248.63 Current children cumulated vsize (Kb) 137388 [startup+260.029 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 10672 Raw data (/proc/10668/stat): 10668 (minisat+_script) S 10667 10668 28974 0 -1 0 289 239 0 0 0 0 0 0 18 0 1 0 1844152611 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/10668/statm): 531 226 485 147 0 384 0 [pid=10668] vsize: 2124 Raw data (/proc/10672/stat): 10672 (minisat+_64-bit) R 10668 10668 28974 0 -1 0 30853 0 0 0 25730 133 0 0 25 0 1 0 1844152616 138678272 29466 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/10672/statm): 33857 29466 145 145 0 33712 0 [pid=10672] vsize: 135428 Current children cumulated CPU time (s) 258.63 Current children cumulated vsize (Kb) 137552 [startup+270.03 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 10672 Raw data (/proc/10668/stat): 10668 (minisat+_script) S 10667 10668 28974 0 -1 0 289 239 0 0 0 0 0 0 18 0 1 0 1844152611 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/10668/statm): 531 226 485 147 0 384 0 [pid=10668] vsize: 2124 Raw data (/proc/10672/stat): 10672 (minisat+_64-bit) R 10668 10668 28974 0 -1 0 30906 0 0 0 26729 133 0 0 25 0 1 0 1844152616 138887168 29519 4294967295 134512640 135094434 3221224432 3221223056 134557612 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/10672/statm): 33908 29519 145 145 0 33763 0 [pid=10672] vsize: 135632 Current children cumulated CPU time (s) 268.62 Current children cumulated vsize (Kb) 137756 [startup+280.031 s] Raw data (loadavg): 1.07 0.99 0.91 2/57 10672 Raw data (/proc/10668/stat): 10668 (minisat+_script) S 10667 10668 28974 0 -1 0 289 239 0 0 0 0 0 0 18 0 1 0 1844152611 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/10668/statm): 531 226 485 147 0 384 0 [pid=10668] vsize: 2124 Raw data (/proc/10672/stat): 10672 (minisat+_64-bit) R 10668 10668 28974 0 -1 0 30964 0 0 0 27728 134 0 0 25 0 1 0 1844152616 139112448 29577 4294967295 134512640 135094434 3221224432 3221223056 134557596 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/10672/statm): 33963 29577 145 145 0 33818 0 [pid=10672] vsize: 135852 Current children cumulated CPU time (s) 278.62 Current children cumulated vsize (Kb) 137976 [startup+290.032 s] Raw data (loadavg): 1.06 0.99 0.91 2/57 10672 Raw data (/proc/10668/stat): 10668 (minisat+_script) S 10667 10668 28974 0 -1 0 289 239 0 0 0 0 0 0 18 0 1 0 1844152611 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/10668/statm): 531 226 485 147 0 384 0 [pid=10668] vsize: 2124 Raw data (/proc/10672/stat): 10672 (minisat+_64-bit) R 10668 10668 28974 0 -1 0 31003 0 0 0 28727 134 0 0 25 0 1 0 1844152616 139264000 29616 4294967295 134512640 135094434 3221224432 3221223056 134557685 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/10672/statm): 34000 29616 145 145 0 33855 0 [pid=10672] vsize: 136000 Current children cumulated CPU time (s) 288.61 Current children cumulated vsize (Kb) 138124 [startup+300.033 s] Raw data (loadavg): 1.05 0.99 0.91 2/57 10672 Raw data (/proc/10668/stat): 10668 (minisat+_script) S 10667 10668 28974 0 -1 0 289 239 0 0 0 0 0 0 18 0 1 0 1844152611 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/10668/statm): 531 226 485 147 0 384 0 [pid=10668] vsize: 2124 Raw data (/proc/10672/stat): 10672 (minisat+_64-bit) R 10668 10668 28974 0 -1 0 31055 0 0 0 29726 135 0 0 25 0 1 0 1844152616 139436032 29668 4294967295 134512640 135094434 3221224432 3221223136 134559019 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/10672/statm): 34042 29668 145 145 0 33897 0 [pid=10672] vsize: 136168 Current children cumulated CPU time (s) 298.61 Current children cumulated vsize (Kb) 138292 [startup+310.034 s] Raw data (loadavg): 1.04 0.99 0.91 2/57 10672 Raw data (/proc/10668/stat): 10668 (minisat+_script) S 10667 10668 28974 0 -1 0 289 239 0 0 0 0 0 0 18 0 1 0 1844152611 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/10668/statm): 531 226 485 147 0 384 0 [pid=10668] vsize: 2124 Raw data (/proc/10672/stat): 10672 (minisat+_64-bit) R 10668 10668 28974 0 -1 0 31084 0 0 0 30726 135 0 0 25 0 1 0 1844152616 139808768 29697 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/10672/statm): 34133 29697 145 145 0 33988 0 [pid=10672] vsize: 136532 Current children cumulated CPU time (s) 308.61 Current children cumulated vsize (Kb) 138656 [startup+320.034 s] Raw data (loadavg): 1.04 0.99 0.91 2/57 10672 Raw data (/proc/10668/stat): 10668 (minisat+_script) S 10667 10668 28974 0 -1 0 289 239 0 0 0 0 0 0 18 0 1 0 1844152611 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/10668/statm): 531 226 485 147 0 384 0 [pid=10668] vsize: 2124 Raw data (/proc/10672/stat): 10672 (minisat+_64-bit) R 10668 10668 28974 0 -1 0 31114 0 0 0 31725 135 0 0 25 0 1 0 1844152616 139927552 29727 4294967295 134512640 135094434 3221224432 3221223184 134559282 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/10672/statm): 34162 29727 145 145 0 34017 0 [pid=10672] vsize: 136648 Current children cumulated CPU time (s) 318.6 Current children cumulated vsize (Kb) 138772 [startup+330.036 s] Raw data (loadavg): 1.03 0.99 0.91 2/57 10672 Raw data (/proc/10668/stat): 10668 (minisat+_script) S 10667 10668 28974 0 -1 0 289 239 0 0 0 0 0 0 18 0 1 0 1844152611 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/10668/statm): 531 226 485 147 0 384 0 [pid=10668] vsize: 2124 Raw data (/proc/10672/stat): 10672 (minisat+_64-bit) R 10668 10668 28974 0 -1 0 31143 0 0 0 32725 136 0 0 25 0 1 0 1844152616 140038144 29756 4294967295 134512640 135094434 3221224432 3221223120 134554746 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/10672/statm): 34189 29756 145 145 0 34044 0 [pid=10672] vsize: 136756 Current children cumulated CPU time (s) 328.61 Current children cumulated vsize (Kb) 138880 [startup+340.037 s] Raw data (loadavg): 1.03 0.99 0.91 2/57 10672 Raw data (/proc/10668/stat): 10668 (minisat+_script) S 10667 10668 28974 0 -1 0 289 239 0 0 0 0 0 0 18 0 1 0 1844152611 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/10668/statm): 531 226 485 147 0 384 0 [pid=10668] vsize: 2124 Raw data (/proc/10672/stat): 10672 (minisat+_64-bit) R 10668 10668 28974 0 -1 0 31255 0 0 0 33723 136 0 0 25 0 1 0 1844152616 140480512 29868 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/10672/statm): 34297 29868 145 145 0 34152 0 [pid=10672] vsize: 137188 Current children cumulated CPU time (s) 338.59 Current children cumulated vsize (Kb) 139312 [startup+350.038 s] Raw data (loadavg): 1.02 0.99 0.91 2/57 10672 Raw data (/proc/10668/stat): 10668 (minisat+_script) S 10667 10668 28974 0 -1 0 289 239 0 0 0 0 0 0 18 0 1 0 1844152611 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/10668/statm): 531 226 485 147 0 384 0 [pid=10668] vsize: 2124 Raw data (/proc/10672/stat): 10672 (minisat+_64-bit) R 10668 10668 28974 0 -1 0 31277 0 0 0 34723 136 0 0 25 0 1 0 1844152616 140566528 29890 4294967295 134512640 135094434 3221224432 3221223044 134563049 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/10672/statm): 34318 29890 145 145 0 34173 0 [pid=10672] vsize: 137272 Current children cumulated CPU time (s) 348.59 Current children cumulated vsize (Kb) 139396 [startup+360.038 s] Raw data (loadavg): 1.02 0.99 0.91 2/57 10672 Raw data (/proc/10668/stat): 10668 (minisat+_script) S 10667 10668 28974 0 -1 0 289 239 0 0 0 0 0 0 18 0 1 0 1844152611 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/10668/statm): 531 226 485 147 0 384 0 [pid=10668] vsize: 2124 Raw data (/proc/10672/stat): 10672 (minisat+_64-bit) R 10668 10668 28974 0 -1 0 31306 0 0 0 35722 136 0 0 25 0 1 0 1844152616 140677120 29919 4294967295 134512640 135094434 3221224432 3221223092 134553480 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/10672/statm): 34345 29919 145 145 0 34200 0 [pid=10672] vsize: 137380 Current children cumulated CPU time (s) 358.58 Current children cumulated vsize (Kb) 139504 [startup+370.039 s] Raw data (loadavg): 1.01 0.99 0.91 2/57 10672 Raw data (/proc/10668/stat): 10668 (minisat+_script) S 10667 10668 28974 0 -1 0 289 239 0 0 0 0 0 0 18 0 1 0 1844152611 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/10668/statm): 531 226 485 147 0 384 0 [pid=10668] vsize: 2124 Raw data (/proc/10672/stat): 10672 (minisat+_64-bit) R 10668 10668 28974 0 -1 0 31332 0 0 0 36722 137 0 0 25 0 1 0 1844152616 140779520 29945 4294967295 134512640 135094434 3221224432 3221223088 134558246 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/10672/statm): 34370 29945 145 145 0 34225 0 [pid=10672] vsize: 137480 Current children cumulated CPU time (s) 368.59 Current children cumulated vsize (Kb) 139604 [startup+380.04 s] Raw data (loadavg): 1.01 0.99 0.91 2/57 10672 Raw data (/proc/10668/stat): 10668 (minisat+_script) S 10667 10668 28974 0 -1 0 289 239 0 0 0 0 0 0 18 0 1 0 1844152611 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/10668/statm): 531 226 485 147 0 384 0 [pid=10668] vsize: 2124 Raw data (/proc/10672/stat): 10672 (minisat+_64-bit) R 10668 10668 28974 0 -1 0 31379 0 0 0 37722 137 0 0 25 0 1 0 1844152616 140963840 29992 4294967295 134512640 135094434 3221224432 3221223088 134558210 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/10672/statm): 34415 29992 145 145 0 34270 0 [pid=10672] vsize: 137660 Current children cumulated CPU time (s) 378.59 Current children cumulated vsize (Kb) 139784 [startup+390.041 s] Raw data (loadavg): 1.01 0.99 0.91 2/57 10672 Raw data (/proc/10668/stat): 10668 (minisat+_script) S 10667 10668 28974 0 -1 0 289 239 0 0 0 0 0 0 18 0 1 0 1844152611 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/10668/statm): 531 226 485 147 0 384 0 [pid=10668] vsize: 2124 Raw data (/proc/10672/stat): 10672 (minisat+_64-bit) R 10668 10668 28974 0 -1 0 31410 0 0 0 38721 137 0 0 25 0 1 0 1844152616 141082624 30023 4294967295 134512640 135094434 3221224432 3221223044 134563130 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/10672/statm): 34444 30023 145 145 0 34299 0 [pid=10672] vsize: 137776 Current children cumulated CPU time (s) 388.58 Current children cumulated vsize (Kb) 139900 [startup+400.043 s] Raw data (loadavg): 1.01 0.99 0.91 2/57 10672 Raw data (/proc/10668/stat): 10668 (minisat+_script) S 10667 10668 28974 0 -1 0 289 239 0 0 0 0 0 0 18 0 1 0 1844152611 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/10668/statm): 531 226 485 147 0 384 0 [pid=10668] vsize: 2124 Raw data (/proc/10672/stat): 10672 (minisat+_64-bit) R 10668 10668 28974 0 -1 0 31441 0 0 0 39720 137 0 0 25 0 1 0 1844152616 141201408 30054 4294967295 134512640 135094434 3221224432 3221223092 134553482 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/10672/statm): 34473 30054 145 145 0 34328 0 [pid=10672] vsize: 137892 Current children cumulated CPU time (s) 398.57 Current children cumulated vsize (Kb) 140016 [startup+410.043 s] Raw data (loadavg): 1.01 0.99 0.91 2/57 10672 Raw data (/proc/10668/stat): 10668 (minisat+_script) S 10667 10668 28974 0 -1 0 289 239 0 0 0 0 0 0 18 0 1 0 1844152611 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/10668/statm): 531 226 485 147 0 384 0 [pid=10668] vsize: 2124 Raw data (/proc/10672/stat): 10672 (minisat+_64-bit) R 10668 10668 28974 0 -1 0 31477 0 0 0 40720 138 0 0 25 0 1 0 1844152616 141340672 30090 4294967295 134512640 135094434 3221224432 3221223044 134563043 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/10672/statm): 34507 30090 145 145 0 34362 0 [pid=10672] vsize: 138028 Current children cumulated CPU time (s) 408.58 Current children cumulated vsize (Kb) 140152 [startup+420.044 s] Raw data (loadavg): 1.00 0.99 0.91 2/57 10672 Raw data (/proc/10668/stat): 10668 (minisat+_script) S 10667 10668 28974 0 -1 0 289 239 0 0 0 0 0 0 18 0 1 0 1844152611 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/10668/statm): 531 226 485 147 0 384 0 [pid=10668] vsize: 2124 Raw data (/proc/10672/stat): 10672 (minisat+_64-bit) R 10668 10668 28974 0 -1 0 31513 0 0 0 41720 138 0 0 25 0 1 0 1844152616 141479936 30126 4294967295 134512640 135094434 3221224432 3221223056 134557685 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/10672/statm): 34541 30126 145 145 0 34396 0 [pid=10672] vsize: 138164 Current children cumulated CPU time (s) 418.58 Current children cumulated vsize (Kb) 140288 [startup+430.046 s] Raw data (loadavg): 1.00 0.99 0.91 2/57 10672 Raw data (/proc/10668/stat): 10668 (minisat+_script) S 10667 10668 28974 0 -1 0 289 239 0 0 0 0 0 0 18 0 1 0 1844152611 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/10668/statm): 531 226 485 147 0 384 0 [pid=10668] vsize: 2124 Raw data (/proc/10672/stat): 10672 (minisat+_64-bit) R 10668 10668 28974 0 -1 0 31544 0 0 0 42718 139 0 0 25 0 1 0 1844152616 141598720 30157 4294967295 134512640 135094434 3221224432 3221223064 134557638 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/10672/statm): 34570 30157 145 145 0 34425 0 [pid=10672] vsize: 138280 Current children cumulated CPU time (s) 428.57 Current children cumulated vsize (Kb) 140404 [startup+440.047 s] Raw data (loadavg): 1.00 0.99 0.91 2/57 10672 Raw data (/proc/10668/stat): 10668 (minisat+_script) S 10667 10668 28974 0 -1 0 289 239 0 0 0 0 0 0 18 0 1 0 1844152611 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/10668/statm): 531 226 485 147 0 384 0 [pid=10668] vsize: 2124 Raw data (/proc/10672/stat): 10672 (minisat+_64-bit) R 10668 10668 28974 0 -1 0 31566 0 0 0 43717 139 0 0 25 0 1 0 1844152616 141684736 30179 4294967295 134512640 135094434 3221224432 3221223120 134554731 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/10672/statm): 34591 30179 145 145 0 34446 0 [pid=10672] vsize: 138364 Current children cumulated CPU time (s) 438.56 Current children cumulated vsize (Kb) 140488 [startup+450.049 s] Raw data (loadavg): 1.00 0.99 0.91 2/57 10672 Raw data (/proc/10668/stat): 10668 (minisat+_script) S 10667 10668 28974 0 -1 0 289 239 0 0 0 0 0 0 18 0 1 0 1844152611 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/10668/statm): 531 226 485 147 0 384 0 [pid=10668] vsize: 2124 Raw data (/proc/10672/stat): 10672 (minisat+_64-bit) R 10668 10668 28974 0 -1 0 31603 0 0 0 44716 140 0 0 25 0 1 0 1844152616 141799424 30216 4294967295 134512640 135094434 3221224432 3221223124 134558984 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/10672/statm): 34619 30216 145 145 0 34474 0 [pid=10672] vsize: 138476 Current children cumulated CPU time (s) 448.56 Current children cumulated vsize (Kb) 140600 [startup+460.05 s] Raw data (loadavg): 1.00 0.99 0.91 2/57 10672 Raw data (/proc/10668/stat): 10668 (minisat+_script) S 10667 10668 28974 0 -1 0 289 239 0 0 0 0 0 0 18 0 1 0 1844152611 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/10668/statm): 531 226 485 147 0 384 0 [pid=10668] vsize: 2124 Raw data (/proc/10672/stat): 10672 (minisat+_64-bit) R 10668 10668 28974 0 -1 0 31626 0 0 0 45716 140 0 0 25 0 1 0 1844152616 141889536 30239 4294967295 134512640 135094434 3221224432 3221223088 134557911 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/10672/statm): 34641 30239 145 145 0 34496 0 [pid=10672] vsize: 138564 Current children cumulated CPU time (s) 458.56 Current children cumulated vsize (Kb) 140688 [startup+470.05 s] Raw data (loadavg): 1.00 0.99 0.91 2/57 10672 Raw data (/proc/10668/stat): 10668 (minisat+_script) S 10667 10668 28974 0 -1 0 289 239 0 0 0 0 0 0 18 0 1 0 1844152611 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/10668/statm): 531 226 485 147 0 384 0 [pid=10668] vsize: 2124 Raw data (/proc/10672/stat): 10672 (minisat+_64-bit) R 10668 10668 28974 0 -1 0 31666 0 0 0 46715 141 0 0 25 0 1 0 1844152616 142012416 30279 4294967295 134512640 135094434 3221224432 3221223056 134557685 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/10672/statm): 34671 30279 145 145 0 34526 0 [pid=10672] vsize: 138684 Current children cumulated CPU time (s) 468.56 Current children cumulated vsize (Kb) 140808 [startup+480.051 s] Raw data (loadavg): 1.00 0.99 0.91 2/57 10672 Raw data (/proc/10668/stat): 10668 (minisat+_script) S 10667 10668 28974 0 -1 0 289 239 0 0 0 0 0 0 18 0 1 0 1844152611 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/10668/statm): 531 226 485 147 0 384 0 [pid=10668] vsize: 2124 Raw data (/proc/10672/stat): 10672 (minisat+_64-bit) R 10668 10668 28974 0 -1 0 31710 0 0 0 47715 141 0 0 25 0 1 0 1844152616 142184448 30323 4294967295 134512640 135094434 3221224432 3221223088 134558249 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/10672/statm): 34713 30323 145 145 0 34568 0 [pid=10672] vsize: 138852 Current children cumulated CPU time (s) 478.56 Current children cumulated vsize (Kb) 140976 [startup+490.052 s] Raw data (loadavg): 1.00 0.99 0.91 2/57 10672 Raw data (/proc/10668/stat): 10668 (minisat+_script) S 10667 10668 28974 0 -1 0 289 239 0 0 0 0 0 0 18 0 1 0 1844152611 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/10668/statm): 531 226 485 147 0 384 0 [pid=10668] vsize: 2124 Raw data (/proc/10672/stat): 10672 (minisat+_64-bit) R 10668 10668 28974 0 -1 0 31763 0 0 0 48715 141 0 0 25 0 1 0 1844152616 142348288 30376 4294967295 134512640 135094434 3221224432 3221223088 134557996 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/10672/statm): 34753 30376 145 145 0 34608 0 [pid=10672] vsize: 139012 Current children cumulated CPU time (s) 488.56 Current children cumulated vsize (Kb) 141136 [startup+500.053 s] Raw data (loadavg): 1.00 0.99 0.91 2/57 10672 Raw data (/proc/10668/stat): 10668 (minisat+_script) S 10667 10668 28974 0 -1 0 289 239 0 0 0 0 0 0 18 0 1 0 1844152611 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/10668/statm): 531 226 485 147 0 384 0 [pid=10668] vsize: 2124 Raw data (/proc/10672/stat): 10672 (minisat+_64-bit) R 10668 10668 28974 0 -1 0 31793 0 0 0 49715 141 0 0 25 0 1 0 1844152616 142467072 30406 4294967295 134512640 135094434 3221224432 3221223088 134557964 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/10672/statm): 34782 30406 145 145 0 34637 0 [pid=10672] vsize: 139128 Current children cumulated CPU time (s) 498.56 Current children cumulated vsize (Kb) 141252 [startup+510.054 s] Raw data (loadavg): 1.00 0.99 0.91 2/57 10672 Raw data (/proc/10668/stat): 10668 (minisat+_script) S 10667 10668 28974 0 -1 0 289 239 0 0 0 0 0 0 18 0 1 0 1844152611 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/10668/statm): 531 226 485 147 0 384 0 [pid=10668] vsize: 2124 Raw data (/proc/10672/stat): 10672 (minisat+_64-bit) R 10668 10668 28974 0 -1 0 31821 0 0 0 50715 141 0 0 25 0 1 0 1844152616 142573568 30434 4294967295 134512640 135094434 3221224432 3221223056 134557717 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/10672/statm): 34808 30434 145 145 0 34663 0 [pid=10672] vsize: 139232 Current children cumulated CPU time (s) 508.56 Current children cumulated vsize (Kb) 141356 [startup+520.054 s] Raw data (loadavg): 1.00 0.99 0.91 2/57 10672 Raw data (/proc/10668/stat): 10668 (minisat+_script) S 10667 10668 28974 0 -1 0 289 239 0 0 0 0 0 0 18 0 1 0 1844152611 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/10668/statm): 531 226 485 147 0 384 0 [pid=10668] vsize: 2124 Raw data (/proc/10672/stat): 10672 (minisat+_64-bit) R 10668 10668 28974 0 -1 0 31848 0 0 0 51714 142 0 0 25 0 1 0 1844152616 142680064 30461 4294967295 134512640 135094434 3221224432 3221223056 134557696 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/10672/statm): 34834 30461 145 145 0 34689 0 [pid=10672] vsize: 139336 Current children cumulated CPU time (s) 518.56 Current children cumulated vsize (Kb) 141460 [startup+530.055 s] Raw data (loadavg): 1.00 0.99 0.91 2/57 10672 Raw data (/proc/10668/stat): 10668 (minisat+_script) S 10667 10668 28974 0 -1 0 289 239 0 0 0 0 0 0 18 0 1 0 1844152611 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/10668/statm): 531 226 485 147 0 384 0 [pid=10668] vsize: 2124 Raw data (/proc/10672/stat): 10672 (minisat+_64-bit) R 10668 10668 28974 0 -1 0 31878 0 0 0 52714 142 0 0 25 0 1 0 1844152616 142794752 30491 4294967295 134512640 135094434 3221224432 3221223120 134554746 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/10672/statm): 34862 30491 145 145 0 34717 0 [pid=10672] vsize: 139448 Current children cumulated CPU time (s) 528.56 Current children cumulated vsize (Kb) 141572 [startup+540.056 s] Raw data (loadavg): 1.00 0.99 0.91 2/57 10672 Raw data (/proc/10668/stat): 10668 (minisat+_script) S 10667 10668 28974 0 -1 0 289 239 0 0 0 0 0 0 18 0 1 0 1844152611 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/10668/statm): 531 226 485 147 0 384 0 [pid=10668] vsize: 2124 Raw data (/proc/10672/stat): 10672 (minisat+_64-bit) R 10668 10668 28974 0 -1 0 31924 0 0 0 53714 142 0 0 25 0 1 0 1844152616 142946304 30537 4294967295 134512640 135094434 3221224432 3221223044 134563069 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/10672/statm): 34899 30537 145 145 0 34754 0 [pid=10672] vsize: 139596 Current children cumulated CPU time (s) 538.56 Current children cumulated vsize (Kb) 141720 [startup+550.057 s] Raw data (loadavg): 1.00 0.99 0.91 2/57 10672 Raw data (/proc/10668/stat): 10668 (minisat+_script) S 10667 10668 28974 0 -1 0 289 239 0 0 0 0 0 0 18 0 1 0 1844152611 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/10668/statm): 531 226 485 147 0 384 0 [pid=10668] vsize: 2124 Raw data (/proc/10672/stat): 10672 (minisat+_64-bit) R 10668 10668 28974 0 -1 0 31961 0 0 0 54713 143 0 0 25 0 1 0 1844152616 143093760 30574 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/10672/statm): 34935 30574 145 145 0 34790 0 [pid=10672] vsize: 139740 Current children cumulated CPU time (s) 548.56 Current children cumulated vsize (Kb) 141864 [startup+560.058 s] Raw data (loadavg): 1.00 0.99 0.91 2/57 10672 Raw data (/proc/10668/stat): 10668 (minisat+_script) S 10667 10668 28974 0 -1 0 289 239 0 0 0 0 0 0 18 0 1 0 1844152611 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/10668/statm): 531 226 485 147 0 384 0 [pid=10668] vsize: 2124 Raw data (/proc/10672/stat): 10672 (minisat+_64-bit) R 10668 10668 28974 0 -1 0 31990 0 0 0 55712 144 0 0 25 0 1 0 1844152616 143204352 30603 4294967295 134512640 135094434 3221224432 3221223092 134553491 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/10672/statm): 34962 30603 145 145 0 34817 0 [pid=10672] vsize: 139848 Current children cumulated CPU time (s) 558.56 Current children cumulated vsize (Kb) 141972 [startup+570.061 s] Raw data (loadavg): 1.00 0.99 0.91 2/57 10672 Raw data (/proc/10668/stat): 10668 (minisat+_script) S 10667 10668 28974 0 -1 0 289 239 0 0 0 0 0 0 18 0 1 0 1844152611 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/10668/statm): 531 226 485 147 0 384 0 [pid=10668] vsize: 2124 Raw data (/proc/10672/stat): 10672 (minisat+_64-bit) R 10668 10668 28974 0 -1 0 32020 0 0 0 56712 145 0 0 25 0 1 0 1844152616 143323136 30633 4294967295 134512640 135094434 3221224432 3221223088 134558411 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/10672/statm): 34991 30633 145 145 0 34846 0 [pid=10672] vsize: 139964 Current children cumulated CPU time (s) 568.57 Current children cumulated vsize (Kb) 142088 [startup+580.061 s] Raw data (loadavg): 1.00 0.99 0.91 2/57 10672 Raw data (/proc/10668/stat): 10668 (minisat+_script) S 10667 10668 28974 0 -1 0 289 239 0 0 0 0 0 0 18 0 1 0 1844152611 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/10668/statm): 531 226 485 147 0 384 0 [pid=10668] vsize: 2124 Raw data (/proc/10672/stat): 10672 (minisat+_64-bit) R 10668 10668 28974 0 -1 0 32049 0 0 0 57711 146 0 0 25 0 1 0 1844152616 143433728 30662 4294967295 134512640 135094434 3221224432 3221223088 134558213 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/10672/statm): 35018 30662 145 145 0 34873 0 [pid=10672] vsize: 140072 Current children cumulated CPU time (s) 578.57 Current children cumulated vsize (Kb) 142196 [startup+590.062 s] Raw data (loadavg): 1.00 0.99 0.91 2/57 10672 Raw data (/proc/10668/stat): 10668 (minisat+_script) S 10667 10668 28974 0 -1 0 289 239 0 0 0 0 0 0 18 0 1 0 1844152611 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/10668/statm): 531 226 485 147 0 384 0 [pid=10668] vsize: 2124 Raw data (/proc/10672/stat): 10672 (minisat+_64-bit) R 10668 10668 28974 0 -1 0 32102 0 0 0 58709 147 0 0 25 0 1 0 1844152616 143642624 30715 4294967295 134512640 135094434 3221224432 3221223056 134557596 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/10672/statm): 35069 30715 145 145 0 34924 0 [pid=10672] vsize: 140276 Current children cumulated CPU time (s) 588.56 Current children cumulated vsize (Kb) 142400 [startup+600.063 s] Raw data (loadavg): 1.00 0.99 0.91 2/57 10672 Raw data (/proc/10668/stat): 10668 (minisat+_script) S 10667 10668 28974 0 -1 0 289 239 0 0 0 0 0 0 18 0 1 0 1844152611 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/10668/statm): 531 226 485 147 0 384 0 [pid=10668] vsize: 2124 Raw data (/proc/10672/stat): 10672 (minisat+_64-bit) R 10668 10668 28974 0 -1 0 32145 0 0 0 59708 147 0 0 25 0 1 0 1844152616 143810560 30758 4294967295 134512640 135094434 3221224432 3221223072 134562115 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/10672/statm): 35110 30758 145 145 0 34965 0 [pid=10672] vsize: 140440 Current children cumulated CPU time (s) 598.55 Current children cumulated vsize (Kb) 142564 [startup+610.064 s] Raw data (loadavg): 1.00 0.99 0.91 2/57 10672 Raw data (/proc/10668/stat): 10668 (minisat+_script) S 10667 10668 28974 0 -1 0 289 239 0 0 0 0 0 0 18 0 1 0 1844152611 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/10668/statm): 531 226 485 147 0 384 0 [pid=10668] vsize: 2124 Raw data (/proc/10672/stat): 10672 (minisat+_64-bit) R 10668 10668 28974 0 -1 0 32165 0 0 0 60708 148 0 0 25 0 1 0 1844152616 143888384 30778 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/10672/statm): 35129 30778 145 145 0 34984 0 [pid=10672] vsize: 140516 Current children cumulated CPU time (s) 608.56 Current children cumulated vsize (Kb) 142640 [startup+620.064 s] Raw data (loadavg): 1.00 0.99 0.91 2/57 10672 Raw data (/proc/10668/stat): 10668 (minisat+_script) S 10667 10668 28974 0 -1 0 289 239 0 0 0 0 0 0 18 0 1 0 1844152611 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/10668/statm): 531 226 485 147 0 384 0 [pid=10668] vsize: 2124 Raw data (/proc/10672/stat): 10672 (minisat+_64-bit) R 10668 10668 28974 0 -1 0 32190 0 0 0 61707 148 0 0 25 0 1 0 1844152616 143986688 30803 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/10672/statm): 35153 30803 145 145 0 35008 0 [pid=10672] vsize: 140612 Current children cumulated CPU time (s) 618.55 Current children cumulated vsize (Kb) 142736 [startup+630.065 s] Raw data (loadavg): 1.00 0.99 0.91 2/57 10672 Raw data (/proc/10668/stat): 10668 (minisat+_script) S 10667 10668 28974 0 -1 0 289 239 0 0 0 0 0 0 18 0 1 0 1844152611 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/10668/statm): 531 226 485 147 0 384 0 [pid=10668] vsize: 2124 Raw data (/proc/10672/stat): 10672 (minisat+_64-bit) R 10668 10668 28974 0 -1 0 32237 0 0 0 62706 149 0 0 25 0 1 0 1844152616 144171008 30850 4294967295 134512640 135094434 3221224432 3221223088 134557903 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/10672/statm): 35198 30850 145 145 0 35053 0 [pid=10672] vsize: 140792 Current children cumulated CPU time (s) 628.55 Current children cumulated vsize (Kb) 142916 [startup+640.065 s] Raw data (loadavg): 1.00 0.99 0.91 2/57 10672 Raw data (/proc/10668/stat): 10668 (minisat+_script) S 10667 10668 28974 0 -1 0 289 239 0 0 0 0 0 0 18 0 1 0 1844152611 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/10668/statm): 531 226 485 147 0 384 0 [pid=10668] vsize: 2124 Raw data (/proc/10672/stat): 10672 (minisat+_64-bit) R 10668 10668 28974 0 -1 0 32272 0 0 0 63706 149 0 0 25 0 1 0 1844152616 144306176 30885 4294967295 134512640 135094434 3221224432 3221223124 134558984 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/10672/statm): 35231 30885 145 145 0 35086 0 [pid=10672] vsize: 140924 Current children cumulated CPU time (s) 638.55 Current children cumulated vsize (Kb) 143048 [startup+650.065 s] Raw data (loadavg): 1.00 0.99 0.91 2/57 10672 Raw data (/proc/10668/stat): 10668 (minisat+_script) S 10667 10668 28974 0 -1 0 289 239 0 0 0 0 0 0 18 0 1 0 1844152611 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/10668/statm): 531 226 485 147 0 384 0 [pid=10668] vsize: 2124 Raw data (/proc/10672/stat): 10672 (minisat+_64-bit) R 10668 10668 28974 0 -1 0 32309 0 0 0 64705 149 0 0 25 0 1 0 1844152616 144449536 30922 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/10672/statm): 35266 30922 145 145 0 35121 0 [pid=10672] vsize: 141064 Current children cumulated CPU time (s) 648.54 Current children cumulated vsize (Kb) 143188 [startup+660.066 s] Raw data (loadavg): 1.00 0.99 0.91 2/57 10672 Raw data (/proc/10668/stat): 10668 (minisat+_script) S 10667 10668 28974 0 -1 0 289 239 0 0 0 0 0 0 18 0 1 0 1844152611 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/10668/statm): 531 226 485 147 0 384 0 [pid=10668] vsize: 2124 Raw data (/proc/10672/stat): 10672 (minisat+_64-bit) R 10668 10668 28974 0 -1 0 32347 0 0 0 65705 150 0 0 25 0 1 0 1844152616 144596992 30960 4294967295 134512640 135094434 3221224432 3221223120 134554731 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/10672/statm): 35302 30960 145 145 0 35157 0 [pid=10672] vsize: 141208 Current children cumulated CPU time (s) 658.55 Current children cumulated vsize (Kb) 143332 [startup+670.067 s] Raw data (loadavg): 1.00 0.99 0.91 2/57 10672 Raw data (/proc/10668/stat): 10668 (minisat+_script) S 10667 10668 28974 0 -1 0 289 239 0 0 0 0 0 0 18 0 1 0 1844152611 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/10668/statm): 531 226 485 147 0 384 0 [pid=10668] vsize: 2124 Raw data (/proc/10672/stat): 10672 (minisat+_64-bit) R 10668 10668 28974 0 -1 0 32382 0 0 0 66703 151 0 0 25 0 1 0 1844152616 144732160 30995 4294967295 134512640 135094434 3221224432 3221223056 134557636 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/10672/statm): 35335 30995 145 145 0 35190 0 [pid=10672] vsize: 141340 Current children cumulated CPU time (s) 668.54 Current children cumulated vsize (Kb) 143464 [startup+680.068 s] Raw data (loadavg): 1.00 0.99 0.91 2/57 10672 Raw data (/proc/10668/stat): 10668 (minisat+_script) S 10667 10668 28974 0 -1 0 289 239 0 0 0 0 0 0 18 0 1 0 1844152611 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/10668/statm): 531 226 485 147 0 384 0 [pid=10668] vsize: 2124 Raw data (/proc/10672/stat): 10672 (minisat+_64-bit) R 10668 10668 28974 0 -1 0 32412 0 0 0 67703 152 0 0 25 0 1 0 1844152616 145379328 31025 4294967295 134512640 135094434 3221224432 3221223120 134554746 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/10672/statm): 35493 31025 145 145 0 35348 0 [pid=10672] vsize: 141972 Current children cumulated CPU time (s) 678.55 Current children cumulated vsize (Kb) 144096 [startup+690.068 s] Raw data (loadavg): 1.00 0.99 0.91 2/57 10672 Raw data (/proc/10668/stat): 10668 (minisat+_script) S 10667 10668 28974 0 -1 0 289 239 0 0 0 0 0 0 18 0 1 0 1844152611 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/10668/statm): 531 226 485 147 0 384 0 [pid=10668] vsize: 2124 Raw data (/proc/10672/stat): 10672 (minisat+_64-bit) R 10668 10668 28974 0 -1 0 32446 0 0 0 68702 152 0 0 25 0 1 0 1844152616 145506304 31059 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/10672/statm): 35524 31059 145 145 0 35379 0 [pid=10672] vsize: 142096 Current children cumulated CPU time (s) 688.54 Current children cumulated vsize (Kb) 144220 [startup+700.069 s] Raw data (loadavg): 1.00 0.99 0.91 2/57 10672 Raw data (/proc/10668/stat): 10668 (minisat+_script) S 10667 10668 28974 0 -1 0 289 239 0 0 0 0 0 0 18 0 1 0 1844152611 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/10668/statm): 531 226 485 147 0 384 0 [pid=10668] vsize: 2124 Raw data (/proc/10672/stat): 10672 (minisat+_64-bit) R 10668 10668 28974 0 -1 0 32481 0 0 0 69702 152 0 0 25 0 1 0 1844152616 145641472 31094 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/10672/statm): 35557 31094 145 145 0 35412 0 [pid=10672] vsize: 142228 Current children cumulated CPU time (s) 698.54 Current children cumulated vsize (Kb) 144352 [startup+710.07 s] Raw data (loadavg): 1.00 0.99 0.91 2/57 10672 Raw data (/proc/10668/stat): 10668 (minisat+_script) S 10667 10668 28974 0 -1 0 289 239 0 0 0 0 0 0 18 0 1 0 1844152611 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/10668/statm): 531 226 485 147 0 384 0 [pid=10668] vsize: 2124 Raw data (/proc/10672/stat): 10672 (minisat+_64-bit) R 10668 10668 28974 0 -1 0 32528 0 0 0 70701 153 0 0 25 0 1 0 1844152616 145825792 31141 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/10672/statm): 35602 31141 145 145 0 35457 0 [pid=10672] vsize: 142408 Current children cumulated CPU time (s) 708.54 Current children cumulated vsize (Kb) 144532 [startup+720.071 s] Raw data (loadavg): 1.00 0.99 0.91 2/57 10672 Raw data (/proc/10668/stat): 10668 (minisat+_script) S 10667 10668 28974 0 -1 0 289 239 0 0 0 0 0 0 18 0 1 0 1844152611 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/10668/statm): 531 226 485 147 0 384 0 [pid=10668] vsize: 2124 Raw data (/proc/10672/stat): 10672 (minisat+_64-bit) R 10668 10668 28974 0 -1 0 32553 0 0 0 71701 153 0 0 25 0 1 0 1844152616 145924096 31166 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/10672/statm): 35626 31166 145 145 0 35481 0 [pid=10672] vsize: 142504 Current children cumulated CPU time (s) 718.54 Current children cumulated vsize (Kb) 144628 [startup+730.073 s] Raw data (loadavg): 1.00 0.99 0.91 2/57 10672 Raw data (/proc/10668/stat): 10668 (minisat+_script) S 10667 10668 28974 0 -1 0 289 239 0 0 0 0 0 0 18 0 1 0 1844152611 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/10668/statm): 531 226 485 147 0 384 0 [pid=10668] vsize: 2124 Raw data (/proc/10672/stat): 10672 (minisat+_64-bit) R 10668 10668 28974 0 -1 0 32584 0 0 0 72700 154 0 0 25 0 1 0 1844152616 146042880 31197 4294967295 134512640 135094434 3221224432 3221223056 134557669 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/10672/statm): 35655 31197 145 145 0 35510 0 [pid=10672] vsize: 142620 Current children cumulated CPU time (s) 728.54 Current children cumulated vsize (Kb) 144744 [startup+740.074 s] Raw data (loadavg): 1.00 0.99 0.91 2/57 10672 Raw data (/proc/10668/stat): 10668 (minisat+_script) S 10667 10668 28974 0 -1 0 289 239 0 0 0 0 0 0 18 0 1 0 1844152611 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/10668/statm): 531 226 485 147 0 384 0 [pid=10668] vsize: 2124 Raw data (/proc/10672/stat): 10672 (minisat+_64-bit) R 10668 10668 28974 0 -1 0 32608 0 0 0 73700 154 0 0 25 0 1 0 1844152616 146137088 31221 4294967295 134512640 135094434 3221224432 3221223056 134557696 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/10672/statm): 35678 31221 145 145 0 35533 0 [pid=10672] vsize: 142712 Current children cumulated CPU time (s) 738.54 Current children cumulated vsize (Kb) 144836 [startup+750.074 s] Raw data (loadavg): 1.00 0.99 0.91 2/57 10672 Raw data (/proc/10668/stat): 10668 (minisat+_script) S 10667 10668 28974 0 -1 0 289 239 0 0 0 0 0 0 18 0 1 0 1844152611 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/10668/statm): 531 226 485 147 0 384 0 [pid=10668] vsize: 2124 Raw data (/proc/10672/stat): 10672 (minisat+_64-bit) R 10668 10668 28974 0 -1 0 32643 0 0 0 74699 155 0 0 25 0 1 0 1844152616 146272256 31256 4294967295 134512640 135094434 3221224432 3221223044 134563069 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/10672/statm): 35711 31256 145 145 0 35566 0 [pid=10672] vsize: 142844 Current children cumulated CPU time (s) 748.54 Current children cumulated vsize (Kb) 144968 [startup+760.075 s] Raw data (loadavg): 1.00 0.99 0.91 2/57 10672 Raw data (/proc/10668/stat): 10668 (minisat+_script) S 10667 10668 28974 0 -1 0 289 239 0 0 0 0 0 0 18 0 1 0 1844152611 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/10668/statm): 531 226 485 147 0 384 0 [pid=10668] vsize: 2124 Raw data (/proc/10672/stat): 10672 (minisat+_64-bit) R 10668 10668 28974 0 -1 0 32674 0 0 0 75699 155 0 0 25 0 1 0 1844152616 146391040 31287 4294967295 134512640 135094434 3221224432 3221223088 134557840 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/10672/statm): 35740 31287 145 145 0 35595 0 [pid=10672] vsize: 142960 Current children cumulated CPU time (s) 758.54 Current children cumulated vsize (Kb) 145084 [startup+770.075 s] Raw data (loadavg): 1.00 0.99 0.91 2/57 10672 Raw data (/proc/10668/stat): 10668 (minisat+_script) S 10667 10668 28974 0 -1 0 289 239 0 0 0 0 0 0 18 0 1 0 1844152611 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/10668/statm): 531 226 485 147 0 384 0 [pid=10668] vsize: 2124 Raw data (/proc/10672/stat): 10672 (minisat+_64-bit) R 10668 10668 28974 0 -1 0 32703 0 0 0 76699 155 0 0 25 0 1 0 1844152616 146505728 31316 4294967295 134512640 135094434 3221224432 3221223088 134557948 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/10672/statm): 35768 31316 145 145 0 35623 0 [pid=10672] vsize: 143072 Current children cumulated CPU time (s) 768.54 Current children cumulated vsize (Kb) 145196 [startup+780.077 s] Raw data (loadavg): 1.00 0.99 0.91 2/57 10672 Raw data (/proc/10668/stat): 10668 (minisat+_script) S 10667 10668 28974 0 -1 0 289 239 0 0 0 0 0 0 18 0 1 0 1844152611 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/10668/statm): 531 226 485 147 0 384 0 [pid=10668] vsize: 2124 Raw data (/proc/10672/stat): 10672 (minisat+_64-bit) R 10668 10668 28974 0 -1 0 32734 0 0 0 77698 155 0 0 25 0 1 0 1844152616 146624512 31347 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/10672/statm): 35797 31347 145 145 0 35652 0 [pid=10672] vsize: 143188 Current children cumulated CPU time (s) 778.53 Current children cumulated vsize (Kb) 145312 [startup+790.078 s] Raw data (loadavg): 1.00 0.99 0.91 2/57 10672 Raw data (/proc/10668/stat): 10668 (minisat+_script) S 10667 10668 28974 0 -1 0 289 239 0 0 0 0 0 0 18 0 1 0 1844152611 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/10668/statm): 531 226 485 147 0 384 0 [pid=10668] vsize: 2124 Raw data (/proc/10672/stat): 10672 (minisat+_64-bit) R 10668 10668 28974 0 -1 0 32779 0 0 0 78698 156 0 0 25 0 1 0 1844152616 146800640 31392 4294967295 134512640 135094434 3221224432 3221223120 134554731 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/10672/statm): 35840 31392 145 145 0 35695 0 [pid=10672] vsize: 143360 Current children cumulated CPU time (s) 788.54 Current children cumulated vsize (Kb) 145484 [startup+800.077 s] Raw data (loadavg): 1.00 0.99 0.91 2/57 10672 Raw data (/proc/10668/stat): 10668 (minisat+_script) S 10667 10668 28974 0 -1 0 289 239 0 0 0 0 0 0 18 0 1 0 1844152611 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/10668/statm): 531 226 485 147 0 384 0 [pid=10668] vsize: 2124 Raw data (/proc/10672/stat): 10672 (minisat+_64-bit) R 10668 10668 28974 0 -1 0 32816 0 0 0 79697 156 0 0 25 0 1 0 1844152616 146944000 31429 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/10672/statm): 35875 31429 145 145 0 35730 0 [pid=10672] vsize: 143500 Current children cumulated CPU time (s) 798.53 Current children cumulated vsize (Kb) 145624 [startup+810.079 s] Raw data (loadavg): 1.00 0.99 0.91 2/57 10672 Raw data (/proc/10668/stat): 10668 (minisat+_script) S 10667 10668 28974 0 -1 0 289 239 0 0 0 0 0 0 18 0 1 0 1844152611 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/10668/statm): 531 226 485 147 0 384 0 [pid=10668] vsize: 2124 Raw data (/proc/10672/stat): 10672 (minisat+_64-bit) R 10668 10668 28974 0 -1 0 32857 0 0 0 80696 157 0 0 25 0 1 0 1844152616 147103744 31470 4294967295 134512640 135094434 3221224432 3221223136 134559005 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/10672/statm): 35914 31470 145 145 0 35769 0 [pid=10672] vsize: 143656 Current children cumulated CPU time (s) 808.53 Current children cumulated vsize (Kb) 145780 [startup+820.08 s] Raw data (loadavg): 1.00 0.99 0.91 2/57 10672 Raw data (/proc/10668/stat): 10668 (minisat+_script) S 10667 10668 28974 0 -1 0 289 239 0 0 0 0 0 0 18 0 1 0 1844152611 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/10668/statm): 531 226 485 147 0 384 0 [pid=10668] vsize: 2124 Raw data (/proc/10672/stat): 10672 (minisat+_64-bit) R 10668 10668 28974 0 -1 0 32891 0 0 0 81696 157 0 0 25 0 1 0 1844152616 147234816 31504 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/10672/statm): 35946 31504 145 145 0 35801 0 [pid=10672] vsize: 143784 Current children cumulated CPU time (s) 818.53 Current children cumulated vsize (Kb) 145908 [startup+830.081 s] Raw data (loadavg): 1.00 0.99 0.91 2/57 10672 Raw data (/proc/10668/stat): 10668 (minisat+_script) S 10667 10668 28974 0 -1 0 289 239 0 0 0 0 0 0 18 0 1 0 1844152611 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/10668/statm): 531 226 485 147 0 384 0 [pid=10668] vsize: 2124 Raw data (/proc/10672/stat): 10672 (minisat+_64-bit) R 10668 10668 28974 0 -1 0 32936 0 0 0 82695 157 0 0 25 0 1 0 1844152616 147365888 31549 4294967295 134512640 135094434 3221224432 3221223120 134554731 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/10672/statm): 35978 31549 145 145 0 35833 0 [pid=10672] vsize: 143912 Current children cumulated CPU time (s) 828.52 Current children cumulated vsize (Kb) 146036 [startup+840.082 s] Raw data (loadavg): 1.00 0.99 0.91 2/57 10672 Raw data (/proc/10668/stat): 10668 (minisat+_script) S 10667 10668 28974 0 -1 0 289 239 0 0 0 0 0 0 18 0 1 0 1844152611 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/10668/statm): 531 226 485 147 0 384 0 [pid=10668] vsize: 2124 Raw data (/proc/10672/stat): 10672 (minisat+_64-bit) R 10668 10668 28974 0 -1 0 32978 0 0 0 83694 158 0 0 25 0 1 0 1844152616 147529728 31591 4294967295 134512640 135094434 3221224432 3221223088 134557866 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/10672/statm): 36018 31591 145 145 0 35873 0 [pid=10672] vsize: 144072 Current children cumulated CPU time (s) 838.52 Current children cumulated vsize (Kb) 146196 [startup+850.083 s] Raw data (loadavg): 1.00 0.99 0.91 2/57 10672 Raw data (/proc/10668/stat): 10668 (minisat+_script) S 10667 10668 28974 0 -1 0 289 239 0 0 0 0 0 0 18 0 1 0 1844152611 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/10668/statm): 531 226 485 147 0 384 0 [pid=10668] vsize: 2124 Raw data (/proc/10672/stat): 10672 (minisat+_64-bit) R 10668 10668 28974 0 -1 0 33018 0 0 0 84694 159 0 0 25 0 1 0 1844152616 147685376 31631 4294967295 134512640 135094434 3221224432 3221223056 134562104 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/10672/statm): 36056 31631 145 145 0 35911 0 [pid=10672] vsize: 144224 Current children cumulated CPU time (s) 848.53 Current children cumulated vsize (Kb) 146348 [startup+860.083 s] Raw data (loadavg): 1.00 0.99 0.91 2/57 10672 Raw data (/proc/10668/stat): 10668 (minisat+_script) S 10667 10668 28974 0 -1 0 289 239 0 0 0 0 0 0 18 0 1 0 1844152611 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/10668/statm): 531 226 485 147 0 384 0 [pid=10668] vsize: 2124 Raw data (/proc/10672/stat): 10672 (minisat+_64-bit) R 10668 10668 28974 0 -1 0 33053 0 0 0 85693 159 0 0 25 0 1 0 1844152616 147820544 31666 4294967295 134512640 135094434 3221224432 3221223092 134553519 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/10672/statm): 36089 31666 145 145 0 35944 0 [pid=10672] vsize: 144356 Current children cumulated CPU time (s) 858.52 Current children cumulated vsize (Kb) 146480 [startup+870.084 s] Raw data (loadavg): 1.00 0.99 0.91 2/57 10672 Raw data (/proc/10668/stat): 10668 (minisat+_script) S 10667 10668 28974 0 -1 0 289 239 0 0 0 0 0 0 18 0 1 0 1844152611 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/10668/statm): 531 226 485 147 0 384 0 [pid=10668] vsize: 2124 Raw data (/proc/10672/stat): 10672 (minisat+_64-bit) R 10668 10668 28974 0 -1 0 33075 0 0 0 86693 159 0 0 25 0 1 0 1844152616 147906560 31688 4294967295 134512640 135094434 3221224432 3221223092 134553446 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/10672/statm): 36110 31688 145 145 0 35965 0 [pid=10672] vsize: 144440 Current children cumulated CPU time (s) 868.52 Current children cumulated vsize (Kb) 146564 [startup+880.086 s] Raw data (loadavg): 1.00 0.99 0.91 2/57 10672 Raw data (/proc/10668/stat): 10668 (minisat+_script) S 10667 10668 28974 0 -1 0 289 239 0 0 0 0 0 0 18 0 1 0 1844152611 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/10668/statm): 531 226 485 147 0 384 0 [pid=10668] vsize: 2124 Raw data (/proc/10672/stat): 10672 (minisat+_64-bit) R 10668 10668 28974 0 -1 0 33105 0 0 0 87693 159 0 0 25 0 1 0 1844152616 148021248 31718 4294967295 134512640 135094434 3221224432 3221223092 134553482 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/10672/statm): 36138 31718 145 145 0 35993 0 [pid=10672] vsize: 144552 Current children cumulated CPU time (s) 878.52 Current children cumulated vsize (Kb) 146676 [startup+890.087 s] Raw data (loadavg): 1.00 0.99 0.91 2/57 10672 Raw data (/proc/10668/stat): 10668 (minisat+_script) S 10667 10668 28974 0 -1 0 289 239 0 0 0 0 0 0 18 0 1 0 1844152611 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/10668/statm): 531 226 485 147 0 384 0 [pid=10668] vsize: 2124 Raw data (/proc/10672/stat): 10672 (minisat+_64-bit) R 10668 10668 28974 0 -1 0 33136 0 0 0 88692 160 0 0 25 0 1 0 1844152616 148140032 31749 4294967295 134512640 135094434 3221224432 3221223088 134557950 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/10672/statm): 36167 31749 145 145 0 36022 0 [pid=10672] vsize: 144668 Current children cumulated CPU time (s) 888.52 Current children cumulated vsize (Kb) 146792 [startup+900.088 s] Raw data (loadavg): 1.00 0.99 0.91 2/57 10672 Raw data (/proc/10668/stat): 10668 (minisat+_script) S 10667 10668 28974 0 -1 0 289 239 0 0 0 0 0 0 18 0 1 0 1844152611 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/10668/statm): 531 226 485 147 0 384 0 [pid=10668] vsize: 2124 Raw data (/proc/10672/stat): 10672 (minisat+_64-bit) R 10668 10668 28974 0 -1 0 33169 0 0 0 89691 160 0 0 25 0 1 0 1844152616 148267008 31782 4294967295 134512640 135094434 3221224432 3221223088 134558178 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/10672/statm): 36198 31782 145 145 0 36053 0 [pid=10672] vsize: 144792 Current children cumulated CPU time (s) 898.51 Current children cumulated vsize (Kb) 146916 [startup+910.089 s] Raw data (loadavg): 1.00 0.99 0.91 2/57 10672 Raw data (/proc/10668/stat): 10668 (minisat+_script) S 10667 10668 28974 0 -1 0 289 239 0 0 0 0 0 0 18 0 1 0 1844152611 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/10668/statm): 531 226 485 147 0 384 0 [pid=10668] vsize: 2124 Raw data (/proc/10672/stat): 10672 (minisat+_64-bit) R 10668 10668 28974 0 -1 0 33194 0 0 0 90691 161 0 0 25 0 1 0 1844152616 148365312 31807 4294967295 134512640 135094434 3221224432 3221223044 134563046 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/10672/statm): 36222 31807 145 145 0 36077 0 [pid=10672] vsize: 144888 Current children cumulated CPU time (s) 908.52 Current children cumulated vsize (Kb) 147012 [startup+920.089 s] Raw data (loadavg): 1.00 0.99 0.91 2/57 10672 Raw data (/proc/10668/stat): 10668 (minisat+_script) S 10667 10668 28974 0 -1 0 289 239 0 0 0 0 0 0 18 0 1 0 1844152611 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/10668/statm): 531 226 485 147 0 384 0 [pid=10668] vsize: 2124 Raw data (/proc/10672/stat): 10672 (minisat+_64-bit) R 10668 10668 28974 0 -1 0 33224 0 0 0 91691 161 0 0 25 0 1 0 1844152616 148480000 31837 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/10672/statm): 36250 31837 145 145 0 36105 0 [pid=10672] vsize: 145000 Current children cumulated CPU time (s) 918.52 Current children cumulated vsize (Kb) 147124 [startup+930.09 s] Raw data (loadavg): 1.00 0.99 0.91 2/57 10672 Raw data (/proc/10668/stat): 10668 (minisat+_script) S 10667 10668 28974 0 -1 0 289 239 0 0 0 0 0 0 18 0 1 0 1844152611 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/10668/statm): 531 226 485 147 0 384 0 [pid=10668] vsize: 2124 Raw data (/proc/10672/stat): 10672 (minisat+_64-bit) R 10668 10668 28974 0 -1 0 33253 0 0 0 92690 161 0 0 25 0 1 0 1844152616 148594688 31866 4294967295 134512640 135094434 3221224432 3221223044 134563083 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/10672/statm): 36278 31866 145 145 0 36133 0 [pid=10672] vsize: 145112 Current children cumulated CPU time (s) 928.51 Current children cumulated vsize (Kb) 147236 [startup+940.091 s] Raw data (loadavg): 1.00 0.99 0.91 2/57 10672 Raw data (/proc/10668/stat): 10668 (minisat+_script) S 10667 10668 28974 0 -1 0 289 239 0 0 0 0 0 0 18 0 1 0 1844152611 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/10668/statm): 531 226 485 147 0 384 0 [pid=10668] vsize: 2124 Raw data (/proc/10672/stat): 10672 (minisat+_64-bit) R 10668 10668 28974 0 -1 0 33283 0 0 0 93690 161 0 0 25 0 1 0 1844152616 148709376 31896 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/10672/statm): 36306 31896 145 145 0 36161 0 [pid=10672] vsize: 145224 Current children cumulated CPU time (s) 938.51 Current children cumulated vsize (Kb) 147348 [startup+950.092 s] Raw data (loadavg): 1.00 0.99 0.91 2/57 10672 Raw data (/proc/10668/stat): 10668 (minisat+_script) S 10667 10668 28974 0 -1 0 289 239 0 0 0 0 0 0 18 0 1 0 1844152611 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/10668/statm): 531 226 485 147 0 384 0 [pid=10668] vsize: 2124 Raw data (/proc/10672/stat): 10672 (minisat+_64-bit) R 10668 10668 28974 0 -1 0 33307 0 0 0 94690 161 0 0 25 0 1 0 1844152616 148799488 31920 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/10672/statm): 36328 31920 145 145 0 36183 0 [pid=10672] vsize: 145312 Current children cumulated CPU time (s) 948.51 Current children cumulated vsize (Kb) 147436 [startup+960.093 s] Raw data (loadavg): 1.00 0.99 0.91 2/57 10672 Raw data (/proc/10668/stat): 10668 (minisat+_script) S 10667 10668 28974 0 -1 0 289 239 0 0 0 0 0 0 18 0 1 0 1844152611 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/10668/statm): 531 226 485 147 0 384 0 [pid=10668] vsize: 2124 Raw data (/proc/10672/stat): 10672 (minisat+_64-bit) R 10668 10668 28974 0 -1 0 33340 0 0 0 95689 162 0 0 25 0 1 0 1844152616 148926464 31953 4294967295 134512640 135094434 3221224432 3221223088 134557840 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/10672/statm): 36359 31953 145 145 0 36214 0 [pid=10672] vsize: 145436 Current children cumulated CPU time (s) 958.51 Current children cumulated vsize (Kb) 147560 [startup+970.093 s] Raw data (loadavg): 1.00 0.99 0.91 2/57 10672 Raw data (/proc/10668/stat): 10668 (minisat+_script) S 10667 10668 28974 0 -1 0 289 239 0 0 0 0 0 0 18 0 1 0 1844152611 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/10668/statm): 531 226 485 147 0 384 0 [pid=10668] vsize: 2124 Raw data (/proc/10672/stat): 10672 (minisat+_64-bit) R 10668 10668 28974 0 -1 0 33367 0 0 0 96689 162 0 0 25 0 1 0 1844152616 149032960 31980 4294967295 134512640 135094434 3221224432 3221223072 134562110 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/10672/statm): 36385 31980 145 145 0 36240 0 [pid=10672] vsize: 145540 Current children cumulated CPU time (s) 968.51 Current children cumulated vsize (Kb) 147664 [startup+980.095 s] Raw data (loadavg): 1.00 0.99 0.91 2/57 10672 Raw data (/proc/10668/stat): 10668 (minisat+_script) S 10667 10668 28974 0 -1 0 289 239 0 0 0 0 0 0 18 0 1 0 1844152611 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/10668/statm): 531 226 485 147 0 384 0 [pid=10668] vsize: 2124 Raw data (/proc/10672/stat): 10672 (minisat+_64-bit) R 10668 10668 28974 0 -1 0 33421 0 0 0 97688 163 0 0 25 0 1 0 1844152616 149245952 32034 4294967295 134512640 135094434 3221224432 3221223088 134558004 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/10672/statm): 36437 32034 145 145 0 36292 0 [pid=10672] vsize: 145748 Current children cumulated CPU time (s) 978.51 Current children cumulated vsize (Kb) 147872 [startup+990.096 s] Raw data (loadavg): 1.00 0.99 0.91 2/57 10672 Raw data (/proc/10668/stat): 10668 (minisat+_script) S 10667 10668 28974 0 -1 0 289 239 0 0 0 0 0 0 18 0 1 0 1844152611 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/10668/statm): 531 226 485 147 0 384 0 [pid=10668] vsize: 2124 Raw data (/proc/10672/stat): 10672 (minisat+_64-bit) R 10668 10668 28974 0 -1 0 33463 0 0 0 98687 163 0 0 25 0 1 0 1844152616 149405696 32076 4294967295 134512640 135094434 3221224432 3221223092 134553480 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/10672/statm): 36476 32076 145 145 0 36331 0 [pid=10672] vsize: 145904 Current children cumulated CPU time (s) 988.5 Current children cumulated vsize (Kb) 148028 [startup+1000.1 s] Raw data (loadavg): 1.00 0.99 0.91 2/57 10672 Raw data (/proc/10668/stat): 10668 (minisat+_script) S 10667 10668 28974 0 -1 0 289 239 0 0 0 0 0 0 18 0 1 0 1844152611 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/10668/statm): 531 226 485 147 0 384 0 [pid=10668] vsize: 2124 Raw data (/proc/10672/stat): 10672 (minisat+_64-bit) R 10668 10668 28974 0 -1 0 33589 0 0 0 99685 164 0 0 25 0 1 0 1844152616 149909504 32202 4294967295 134512640 135094434 3221224432 3221223056 134557596 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/10672/statm): 36599 32202 145 145 0 36454 0 [pid=10672] vsize: 146396 Current children cumulated CPU time (s) 998.49 Current children cumulated vsize (Kb) 148520 [startup+1010.1 s] Raw data (loadavg): 1.00 0.99 0.91 2/57 10672 Raw data (/proc/10668/stat): 10668 (minisat+_script) S 10667 10668 28974 0 -1 0 289 239 0 0 0 0 0 0 18 0 1 0 1844152611 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/10668/statm): 531 226 485 147 0 384 0 [pid=10668] vsize: 2124 Raw data (/proc/10672/stat): 10672 (minisat+_64-bit) R 10668 10668 28974 0 -1 0 33623 0 0 0 100684 165 0 0 25 0 1 0 1844152616 150040576 32236 4294967295 134512640 135094434 3221224432 3221223120 134554796 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/10672/statm): 36631 32236 145 145 0 36486 0 [pid=10672] vsize: 146524 Current children cumulated CPU time (s) 1008.49 Current children cumulated vsize (Kb) 148648 [startup+1020.1 s] Raw data (loadavg): 1.00 0.99 0.91 2/57 10672 Raw data (/proc/10668/stat): 10668 (minisat+_script) S 10667 10668 28974 0 -1 0 289 239 0 0 0 0 0 0 18 0 1 0 1844152611 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/10668/statm): 531 226 485 147 0 384 0 [pid=10668] vsize: 2124 Raw data (/proc/10672/stat): 10672 (minisat+_64-bit) R 10668 10668 28974 0 -1 0 33661 0 0 0 101684 165 0 0 25 0 1 0 1844152616 150188032 32274 4294967295 134512640 135094434 3221224432 3221223088 134558249 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/10672/statm): 36667 32274 145 145 0 36522 0 [pid=10672] vsize: 146668 Current children cumulated CPU time (s) 1018.49 Current children cumulated vsize (Kb) 148792 [startup+1030.1 s] Raw data (loadavg): 1.00 0.99 0.91 2/57 10672 Raw data (/proc/10668/stat): 10668 (minisat+_script) S 10667 10668 28974 0 -1 0 289 239 0 0 0 0 0 0 18 0 1 0 1844152611 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/10668/statm): 531 226 485 147 0 384 0 [pid=10668] vsize: 2124 Raw data (/proc/10672/stat): 10672 (minisat+_64-bit) R 10668 10668 28974 0 -1 0 33688 0 0 0 102683 165 0 0 25 0 1 0 1844152616 150290432 32301 4294967295 134512640 135094434 3221224432 3221223092 134553480 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/10672/statm): 36692 32301 145 145 0 36547 0 [pid=10672] vsize: 146768 Current children cumulated CPU time (s) 1028.48 Current children cumulated vsize (Kb) 148892 [startup+1040.1 s] Raw data (loadavg): 1.00 0.99 0.91 2/57 10672 Raw data (/proc/10668/stat): 10668 (minisat+_script) S 10667 10668 28974 0 -1 0 289 239 0 0 0 0 0 0 18 0 1 0 1844152611 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/10668/statm): 531 226 485 147 0 384 0 [pid=10668] vsize: 2124 Raw data (/proc/10672/stat): 10672 (minisat+_64-bit) R 10668 10668 28974 0 -1 0 33712 0 0 0 103683 166 0 0 25 0 1 0 1844152616 150384640 32325 4294967295 134512640 135094434 3221224432 3221223088 134558249 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/10672/statm): 36715 32325 145 145 0 36570 0 [pid=10672] vsize: 146860 Current children cumulated CPU time (s) 1038.49 Current children cumulated vsize (Kb) 148984 [startup+1050.1 s] Raw data (loadavg): 1.00 0.99 0.91 2/57 10672 Raw data (/proc/10668/stat): 10668 (minisat+_script) S 10667 10668 28974 0 -1 0 289 239 0 0 0 0 0 0 18 0 1 0 1844152611 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/10668/statm): 531 226 485 147 0 384 0 [pid=10668] vsize: 2124 Raw data (/proc/10672/stat): 10672 (minisat+_64-bit) R 10668 10668 28974 0 -1 0 33753 0 0 0 104681 167 0 0 25 0 1 0 1844152616 150540288 32366 4294967295 134512640 135094434 3221224432 3221223120 134554746 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/10672/statm): 36753 32366 145 145 0 36608 0 [pid=10672] vsize: 147012 Current children cumulated CPU time (s) 1048.48 Current children cumulated vsize (Kb) 149136 [startup+1060.1 s] Raw data (loadavg): 1.00 0.99 0.91 2/57 10672 Raw data (/proc/10668/stat): 10668 (minisat+_script) S 10667 10668 28974 0 -1 0 289 239 0 0 0 0 0 0 18 0 1 0 1844152611 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/10668/statm): 531 226 485 147 0 384 0 [pid=10668] vsize: 2124 Raw data (/proc/10672/stat): 10672 (minisat+_64-bit) R 10668 10668 28974 0 -1 0 33780 0 0 0 105680 167 0 0 25 0 1 0 1844152616 150646784 32393 4294967295 134512640 135094434 3221224432 3221223092 134553450 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/10672/statm): 36779 32393 145 145 0 36634 0 [pid=10672] vsize: 147116 Current children cumulated CPU time (s) 1058.47 Current children cumulated vsize (Kb) 149240 [startup+1070.1 s] Raw data (loadavg): 1.00 0.99 0.91 2/57 10672 Raw data (/proc/10668/stat): 10668 (minisat+_script) S 10667 10668 28974 0 -1 0 289 239 0 0 0 0 0 0 18 0 1 0 1844152611 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/10668/statm): 531 226 485 147 0 384 0 [pid=10668] vsize: 2124 Raw data (/proc/10672/stat): 10672 (minisat+_64-bit) R 10668 10668 28974 0 -1 0 33896 0 0 0 106678 169 0 0 25 0 1 0 1844152616 151105536 32509 4294967295 134512640 135094434 3221224432 3221223088 134558249 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/10672/statm): 36891 32509 145 145 0 36746 0 [pid=10672] vsize: 147564 Current children cumulated CPU time (s) 1068.47 Current children cumulated vsize (Kb) 149688 [startup+1080.1 s] Raw data (loadavg): 1.00 0.99 0.91 2/57 10672 Raw data (/proc/10668/stat): 10668 (minisat+_script) S 10667 10668 28974 0 -1 0 289 239 0 0 0 0 0 0 18 0 1 0 1844152611 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/10668/statm): 531 226 485 147 0 384 0 [pid=10668] vsize: 2124 Raw data (/proc/10672/stat): 10672 (minisat+_64-bit) R 10668 10668 28974 0 -1 0 33925 0 0 0 107678 169 0 0 25 0 1 0 1844152616 151216128 32538 4294967295 134512640 135094434 3221224432 3221223116 134553526 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/10672/statm): 36918 32538 145 145 0 36773 0 [pid=10672] vsize: 147672 Current children cumulated CPU time (s) 1078.47 Current children cumulated vsize (Kb) 149796 [startup+1090.11 s] Raw data (loadavg): 1.00 0.99 0.91 2/57 10672 Raw data (/proc/10668/stat): 10668 (minisat+_script) S 10667 10668 28974 0 -1 0 289 239 0 0 0 0 0 0 18 0 1 0 1844152611 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/10668/statm): 531 226 485 147 0 384 0 [pid=10668] vsize: 2124 Raw data (/proc/10672/stat): 10672 (minisat+_64-bit) R 10668 10668 28974 0 -1 0 33952 0 0 0 108677 169 0 0 25 0 1 0 1844152616 151322624 32565 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/10672/statm): 36944 32565 145 145 0 36799 0 [pid=10672] vsize: 147776 Current children cumulated CPU time (s) 1088.46 Current children cumulated vsize (Kb) 149900 [startup+1100.11 s] Raw data (loadavg): 1.00 0.99 0.91 2/57 10672 Raw data (/proc/10668/stat): 10668 (minisat+_script) S 10667 10668 28974 0 -1 0 289 239 0 0 0 0 0 0 18 0 1 0 1844152611 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/10668/statm): 531 226 485 147 0 384 0 [pid=10668] vsize: 2124 Raw data (/proc/10672/stat): 10672 (minisat+_64-bit) R 10668 10668 28974 0 -1 0 33977 0 0 0 109677 170 0 0 25 0 1 0 1844152616 151416832 32590 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/10672/statm): 36967 32590 145 145 0 36822 0 [pid=10672] vsize: 147868 Current children cumulated CPU time (s) 1098.47 Current children cumulated vsize (Kb) 149992 [startup+1110.11 s] Raw data (loadavg): 1.00 0.99 0.91 2/57 10672 Raw data (/proc/10668/stat): 10668 (minisat+_script) S 10667 10668 28974 0 -1 0 289 239 0 0 0 0 0 0 18 0 1 0 1844152611 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/10668/statm): 531 226 485 147 0 384 0 [pid=10668] vsize: 2124 Raw data (/proc/10672/stat): 10672 (minisat+_64-bit) R 10668 10668 28974 0 -1 0 34002 0 0 0 110677 170 0 0 25 0 1 0 1844152616 151515136 32615 4294967295 134512640 135094434 3221224432 3221223060 134557564 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/10672/statm): 36991 32615 145 145 0 36846 0 [pid=10672] vsize: 147964 Current children cumulated CPU time (s) 1108.47 Current children cumulated vsize (Kb) 150088 [startup+1120.11 s] Raw data (loadavg): 1.00 0.99 0.91 2/57 10672 Raw data (/proc/10668/stat): 10668 (minisat+_script) S 10667 10668 28974 0 -1 0 289 239 0 0 0 0 0 0 18 0 1 0 1844152611 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/10668/statm): 531 226 485 147 0 384 0 [pid=10668] vsize: 2124 Raw data (/proc/10672/stat): 10672 (minisat+_64-bit) R 10668 10668 28974 0 -1 0 34037 0 0 0 111676 170 0 0 25 0 1 0 1844152616 151650304 32650 4294967295 134512640 135094434 3221224432 3221223120 134554746 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/10672/statm): 37024 32650 145 145 0 36879 0 [pid=10672] vsize: 148096 Current children cumulated CPU time (s) 1118.46 Current children cumulated vsize (Kb) 150220 [startup+1130.11 s] Raw data (loadavg): 1.00 0.99 0.91 2/57 10672 Raw data (/proc/10668/stat): 10668 (minisat+_script) S 10667 10668 28974 0 -1 0 289 239 0 0 0 0 0 0 18 0 1 0 1844152611 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/10668/statm): 531 226 485 147 0 384 0 [pid=10668] vsize: 2124 Raw data (/proc/10672/stat): 10672 (minisat+_64-bit) R 10668 10668 28974 0 -1 0 34163 0 0 0 112674 171 0 0 25 0 1 0 1844152616 152150016 32776 4294967295 134512640 135094434 3221224432 3221223124 134558984 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/10672/statm): 37146 32776 145 145 0 37001 0 [pid=10672] vsize: 148584 Current children cumulated CPU time (s) 1128.45 Current children cumulated vsize (Kb) 150708 [startup+1140.11 s] Raw data (loadavg): 1.00 0.99 0.91 2/57 10672 Raw data (/proc/10668/stat): 10668 (minisat+_script) S 10667 10668 28974 0 -1 0 289 239 0 0 0 0 0 0 18 0 1 0 1844152611 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/10668/statm): 531 226 485 147 0 384 0 [pid=10668] vsize: 2124 Raw data (/proc/10672/stat): 10672 (minisat+_64-bit) R 10668 10668 28974 0 -1 0 34284 0 0 0 113672 172 0 0 25 0 1 0 1844152616 152625152 32897 4294967295 134512640 135094434 3221224432 3221223044 134563049 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/10672/statm): 37262 32897 145 145 0 37117 0 [pid=10672] vsize: 149048 Current children cumulated CPU time (s) 1138.44 Current children cumulated vsize (Kb) 151172 [startup+1150.11 s] Raw data (loadavg): 1.00 0.99 0.91 2/57 10672 Raw data (/proc/10668/stat): 10668 (minisat+_script) S 10667 10668 28974 0 -1 0 289 239 0 0 0 0 0 0 18 0 1 0 1844152611 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/10668/statm): 531 226 485 147 0 384 0 [pid=10668] vsize: 2124 Raw data (/proc/10672/stat): 10672 (minisat+_64-bit) R 10668 10668 28974 0 -1 0 34321 0 0 0 114671 172 0 0 25 0 1 0 1844152616 152772608 32934 4294967295 134512640 135094434 3221224432 3221223120 134554746 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/10672/statm): 37298 32934 145 145 0 37153 0 [pid=10672] vsize: 149192 Current children cumulated CPU time (s) 1148.43 Current children cumulated vsize (Kb) 151316 [startup+1160.11 s] Raw data (loadavg): 1.00 0.99 0.91 2/57 10672 Raw data (/proc/10668/stat): 10668 (minisat+_script) S 10667 10668 28974 0 -1 0 289 239 0 0 0 0 0 0 18 0 1 0 1844152611 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/10668/statm): 531 226 485 147 0 384 0 [pid=10668] vsize: 2124 Raw data (/proc/10672/stat): 10672 (minisat+_64-bit) R 10668 10668 28974 0 -1 0 34426 0 0 0 115669 174 0 0 25 0 1 0 1844152616 153186304 33039 4294967295 134512640 135094434 3221224432 3221223044 134563069 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/10672/statm): 37399 33039 145 145 0 37254 0 [pid=10672] vsize: 149596 Current children cumulated CPU time (s) 1158.43 Current children cumulated vsize (Kb) 151720 [startup+1170.11 s] Raw data (loadavg): 1.00 0.99 0.91 2/57 10672 Raw data (/proc/10668/stat): 10668 (minisat+_script) S 10667 10668 28974 0 -1 0 289 239 0 0 0 0 0 0 18 0 1 0 1844152611 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/10668/statm): 531 226 485 147 0 384 0 [pid=10668] vsize: 2124 Raw data (/proc/10672/stat): 10672 (minisat+_64-bit) R 10668 10668 28974 0 -1 0 34472 0 0 0 116668 175 0 0 25 0 1 0 1844152616 153366528 33085 4294967295 134512640 135094434 3221224432 3221223092 134553494 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/10672/statm): 37443 33085 145 145 0 37298 0 [pid=10672] vsize: 149772 Current children cumulated CPU time (s) 1168.43 Current children cumulated vsize (Kb) 151896 [startup+1180.11 s] Raw data (loadavg): 1.00 0.99 0.91 2/57 10672 Raw data (/proc/10668/stat): 10668 (minisat+_script) S 10667 10668 28974 0 -1 0 289 239 0 0 0 0 0 0 18 0 1 0 1844152611 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/10668/statm): 531 226 485 147 0 384 0 [pid=10668] vsize: 2124 Raw data (/proc/10672/stat): 10672 (minisat+_64-bit) R 10668 10668 28974 0 -1 0 34537 0 0 0 117666 176 0 0 25 0 1 0 1844152616 153620480 33150 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/10672/statm): 37505 33150 145 145 0 37360 0 [pid=10672] vsize: 150020 Current children cumulated CPU time (s) 1178.42 Current children cumulated vsize (Kb) 152144 [startup+1190.12 s] Raw data (loadavg): 1.00 0.99 0.91 2/57 10672 Raw data (/proc/10668/stat): 10668 (minisat+_script) S 10667 10668 28974 0 -1 0 289 239 0 0 0 0 0 0 18 0 1 0 1844152611 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/10668/statm): 531 226 485 147 0 384 0 [pid=10668] vsize: 2124 Raw data (/proc/10672/stat): 10672 (minisat+_64-bit) R 10668 10668 28974 0 -1 0 34586 0 0 0 118664 177 0 0 25 0 1 0 1844152616 153812992 33199 4294967295 134512640 135094434 3221224432 3221223056 134557696 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/10672/statm): 37552 33199 145 145 0 37407 0 [pid=10672] vsize: 150208 Current children cumulated CPU time (s) 1188.41 Current children cumulated vsize (Kb) 152332 [startup+1200.12 s] Raw data (loadavg): 1.00 0.99 0.91 2/57 10672 Raw data (/proc/10668/stat): 10668 (minisat+_script) S 10667 10668 28974 0 -1 0 289 239 0 0 0 0 0 0 18 0 1 0 1844152611 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/10668/statm): 531 226 485 147 0 384 0 [pid=10668] vsize: 2124 Raw data (/proc/10672/stat): 10672 (minisat+_64-bit) R 10668 10668 28974 0 -1 0 34633 0 0 0 119664 177 0 0 25 0 1 0 1844152616 153997312 33246 4294967295 134512640 135094434 3221224432 3221223120 134554796 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/10672/statm): 37597 33246 145 145 0 37452 0 [pid=10672] vsize: 150388 Current children cumulated CPU time (s) 1198.41 Current children cumulated vsize (Kb) 152512 [startup+1210.12 s] Raw data (loadavg): 1.00 0.99 0.91 2/57 10672 Raw data (/proc/10668/stat): 10668 (minisat+_script) S 10667 10668 28974 0 -1 0 289 239 0 0 0 0 0 0 18 0 1 0 1844152611 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/10668/statm): 531 226 485 147 0 384 0 [pid=10668] vsize: 2124 Raw data (/proc/10672/stat): 10672 (minisat+_64-bit) R 10668 10668 28974 0 -1 0 34666 0 0 0 120663 178 0 0 25 0 1 0 1844152616 154124288 33279 4294967295 134512640 135094434 3221224432 3221223056 134557598 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/10672/statm): 37628 33279 145 145 0 37483 0 [pid=10672] vsize: 150512 Current children cumulated CPU time (s) 1208.41 Current children cumulated vsize (Kb) 152636 Maximum CPU time exceeded: sending SIGTERM then SIGKILL [startup+1210.12 s] Raw data (loadavg): 1.00 0.99 0.91 2/57 10672 Raw data (/proc/10668/stat): 10668 (minisat+_script) S 10667 10668 28974 0 -1 0 289 239 0 0 0 0 0 0 18 0 1 0 1844152611 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/10668/statm): 531 226 485 147 0 384 0 [pid=10668] vsize: 2124 Raw data (/proc/10672/stat): 10672 (minisat+_64-bit) R 10668 10668 28974 0 -1 0 34666 0 0 0 120663 178 0 0 25 0 1 0 1844152616 154124288 33279 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/10672/statm): 37628 33279 145 145 0 37483 0 [pid=10672] vsize: 150512 Current children cumulated CPU time (s) 1208.41 Current children cumulated vsize (Kb) 152636 Sending SIGTERM to -10668 Sleeping 2 seconds One traced child (pid=10668) ended because it received signal 15 (SIGTERM) One traced child (pid=10672) exited with status: 0 All traced children have exited ! Game is over. Child status: 0 Real time (s): 1210.19 CPU time (s): 1208.49 CPU user time (s): 1206.64 CPU system time (s): 1.84872 CPU usage (%): 99.8596 Max. virtual memory (cumulated for all children) (Kb): 152636
ERROR: no interpretation found !