Name | submitted/manquinho/primes-dimacs-cnf/normalized-g125.18.opb |
MD5SUM | a18434ce5469ba587063f7e76ce3e080 |
Bench Category | optimization, small integers (OPTSMALLINT) |
Has Objective Function | YES |
Satisfiable | |
(Un)Satisfiability was proved | |
Best value of the objective function | |
Optimality of the best value was proved | |
Number of terms in the objective function | 4500 |
Biggest coefficient in the objective function | 1 |
Number of bits for the biggest coefficient in the objective function | 1 |
Sum of the numbers in the objective function | 4500 |
Number of bits of the sum of numbers in the objective function | 13 |
Biggest number in a constraint | 1 |
Number of bits of the biggest number in a constraint | 1 |
Biggest sum of numbers in a constraint | 4500 |
Number of bits of the biggest sum of numbers | 13 |
Best result obtained on this benchmark | |
Best CPU time to get the best result obtained on this benchmark | |
Number of variables | 4500 |
Total number of constraints | 72413 |
Number of constraints which are clauses | 72413 |
Number of constraints which are cardinality constraints (but not clauses) | 0 |
Number of constraints which are nor clauses,nor cardinality constraints | 0 |
Minimum length of a constraint | 2 |
Maximum length of a constraint | 18 |
LAUNCH ON wulflinc30 THE 2005-09-18 15:08:59 (client local time) PB2005-SCRIPT v4.0 MARKUPS: idlaunch=2470 boxname=wulflinc30 idbench=126 idsolver=3 numberseed=0 MD5SUM SOLVER: MD5SUM BENCH: a18434ce5469ba587063f7e76ce3e080 /oldhome/oroussel/tmp/wulflinc30/normalized-g125.18.opb REAL COMMAND: minisat+_script /oldhome/oroussel/tmp/wulflinc30/normalized-g125.18.opb IDLAUNCH: 2470 /proc/cpuinfo: processor : 0 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 3 cpu MHz : 451.072 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.072 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 : 901.12 /proc/meminfo: MemTotal: 1034660 kB MemFree: 908008 kB Buffers: 37136 kB Cached: 58976 kB SwapCached: 788 kB Active: 64096 kB Inactive: 34680 kB HighTotal: 131008 kB HighFree: 71260 kB LowTotal: 903652 kB LowFree: 836748 kB SwapTotal: 2097892 kB SwapFree: 2096636 kB Dirty: 28 kB Writeback: 0 kB Mapped: 5732 kB Slab: 22280 kB Committed_AS: 64172 kB PageTables: 328 kB VmallocTotal: 114680 kB VmallocUsed: 1368 kB VmallocChunk: 113252 kB JOB ENDED THE 2005-09-18 15:29:10 (client local time) WITH STATUS 0 IN 1206.16 SECONDS stats: 2470 7 1206.16 0
c Parsing PB file... c Converting 72413 PB-constraints to clauses... c -- Unit propagations: (none) c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): ............................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................. c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 0 | 72413 146826 | 24137 0 0 nan | 0.000 % | c | 100 | 72413 146826 | 26550 100 5662 56.6 | 0.000 % | c | 251 | 72413 146826 | 29205 251 35284 140.6 | 0.000 % | c | 478 | 72413 146826 | 32126 478 80636 168.7 | 0.000 % | c | 815 | 72413 146826 | 35338 815 187600 230.2 | 0.000 % | c | 1322 | 72413 146826 | 38872 1322 375200 283.8 | 0.000 % | c | 2082 | 72413 146826 | 42760 2082 613029 294.4 | 0.000 % | c | 3222 | 72413 146826 | 47036 3222 935358 290.3 | 0.000 % | c | 4930 | 72413 146826 | 51739 4930 1674242 339.6 | 0.000 % | c | 7492 | 72413 146826 | 56913 7492 2548585 340.2 | 0.000 % | c | 11336 | 72413 146826 | 62605 11336 4532097 399.8 | 0.000 % | c | 17105 | 72413 146826 | 68865 17105 7210651 421.6 | 0.000 % | c | 25754 | 72413 146826 | 75752 25754 11332646 440.0 | 0.000 % | c | 38729 | 72413 146826 | 83327 38729 16386246 423.1 | 0.000 % | c | 58190 | 72413 146826 | 91660 58190 22895367 393.5 | 0.000 % | c | 87382 | 72413 146826 | 100826 87382 36504093 417.8 | 0.000 % | c | 131175 | 72413 146826 | 110908 41235 18834474 456.8 | 0.000 % |
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/11561/stat): 11561 (minisat+_script) R 11560 11561 5245 0 -1 0 19 0 0 0 0 0 0 0 23 0 1 0 1842207039 712704 3 4294967295 134512640 135087896 3221224512 3221224512 1073744960 0 0 5 0 0 0 0 17 0 0 0 Raw data (/proc/11561/statm): 174 3 169 147 0 27 0 [pid=11561] 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=11562 New process pid=11563 New process pid=11564 execve syscall for /bin/sed executable One traced child (pid=11563) 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=11564) exited with status: 0 One traced child (pid=11562) exited with status: 0 New process pid=11565 execve syscall for /oldhome/oroussel/solvers/minisat+_64-bit_static executable open syscall for file /dev/null open syscall for file /oldhome/oroussel/tmp/wulflinc30/normalized-g125.18.opb [startup+10.0034 s] Raw data (loadavg): 0.52 0.78 0.91 2/57 11565 Raw data (/proc/11561/stat): 11561 (minisat+_script) S 11560 11561 5245 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1842207039 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/11561/statm): 531 226 485 147 0 384 0 [pid=11561] vsize: 2124 Raw data (/proc/11565/stat): 11565 (minisat+_64-bit) R 11561 11561 5245 0 -1 0 4727 0 0 0 960 19 0 0 25 0 1 0 1842207044 20262912 4714 4294967295 134512640 135094434 3221224448 3221223120 134555574 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/11565/statm): 4947 4714 145 145 0 4802 0 [pid=11565] vsize: 19788 Current children cumulated CPU time (s) 9.8 Current children cumulated vsize (Kb) 21912 [startup+20.0052 s] Raw data (loadavg): 0.59 0.78 0.91 2/57 11565 Raw data (/proc/11561/stat): 11561 (minisat+_script) S 11560 11561 5245 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1842207039 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/11561/statm): 531 226 485 147 0 384 0 [pid=11561] vsize: 2124 Raw data (/proc/11565/stat): 11565 (minisat+_64-bit) R 11561 11561 5245 0 -1 0 5300 0 0 0 1952 23 0 0 25 0 1 0 1842207044 22597632 5287 4294967295 134512640 135094434 3221224448 3221223104 134558208 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/11565/statm): 5517 5287 145 145 0 5372 0 [pid=11565] vsize: 22068 Current children cumulated CPU time (s) 19.76 Current children cumulated vsize (Kb) 24192 [startup+30.006 s] Raw data (loadavg): 0.65 0.79 0.91 2/57 11565 Raw data (/proc/11561/stat): 11561 (minisat+_script) S 11560 11561 5245 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1842207039 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/11561/statm): 531 226 485 147 0 384 0 [pid=11561] vsize: 2124 Raw data (/proc/11565/stat): 11565 (minisat+_64-bit) R 11561 11561 5245 0 -1 0 6660 0 0 0 2933 31 0 0 25 0 1 0 1842207044 28168192 6647 4294967295 134512640 135094434 3221224448 3221223104 134558405 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/11565/statm): 6877 6647 145 145 0 6732 0 [pid=11565] vsize: 27508 Current children cumulated CPU time (s) 29.65 Current children cumulated vsize (Kb) 29632 [startup+40.0058 s] Raw data (loadavg): 0.71 0.80 0.91 2/57 11565 Raw data (/proc/11561/stat): 11561 (minisat+_script) S 11560 11561 5245 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1842207039 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/11561/statm): 531 226 485 147 0 384 0 [pid=11561] vsize: 2124 Raw data (/proc/11565/stat): 11565 (minisat+_64-bit) R 11561 11561 5245 0 -1 0 7871 0 0 0 3915 39 0 0 25 0 1 0 1842207044 33128448 7858 4294967295 134512640 135094434 3221224448 3221223104 134558208 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/11565/statm): 8088 7858 145 145 0 7943 0 [pid=11565] vsize: 32352 Current children cumulated CPU time (s) 39.55 Current children cumulated vsize (Kb) 34476 [startup+50.0075 s] Raw data (loadavg): 0.75 0.80 0.91 2/57 11565 Raw data (/proc/11561/stat): 11561 (minisat+_script) S 11560 11561 5245 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1842207039 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/11561/statm): 531 226 485 147 0 384 0 [pid=11561] vsize: 2124 Raw data (/proc/11565/stat): 11565 (minisat+_64-bit) R 11561 11561 5245 0 -1 0 9066 0 0 0 4894 47 0 0 25 0 1 0 1842207044 38080512 9053 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/11565/statm): 9297 9053 145 145 0 9152 0 [pid=11565] vsize: 37188 Current children cumulated CPU time (s) 49.42 Current children cumulated vsize (Kb) 39312 [startup+60.0083 s] Raw data (loadavg): 0.79 0.81 0.91 2/57 11565 Raw data (/proc/11561/stat): 11561 (minisat+_script) S 11560 11561 5245 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1842207039 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/11561/statm): 531 226 485 147 0 384 0 [pid=11561] vsize: 2124 Raw data (/proc/11565/stat): 11565 (minisat+_64-bit) R 11561 11561 5245 0 -1 0 10509 0 0 0 5875 55 0 0 25 0 1 0 1842207044 43978752 10496 4294967295 134512640 135094434 3221224448 3221223104 134558159 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/11565/statm): 10737 10496 145 145 0 10592 0 [pid=11565] vsize: 42948 Current children cumulated CPU time (s) 59.31 Current children cumulated vsize (Kb) 45072 [startup+70.0101 s] Raw data (loadavg): 0.82 0.81 0.91 2/57 11565 Raw data (/proc/11561/stat): 11561 (minisat+_script) S 11560 11561 5245 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1842207039 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/11561/statm): 531 226 485 147 0 384 0 [pid=11561] vsize: 2124 Raw data (/proc/11565/stat): 11565 (minisat+_64-bit) R 11561 11561 5245 0 -1 0 11692 0 0 0 6855 63 0 0 25 0 1 0 1842207044 48824320 11679 4294967295 134512640 135094434 3221224448 3221223040 134557219 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/11565/statm): 11920 11679 145 145 0 11775 0 [pid=11565] vsize: 47680 Current children cumulated CPU time (s) 69.19 Current children cumulated vsize (Kb) 49804 [startup+80.0109 s] Raw data (loadavg): 0.85 0.82 0.91 2/57 11565 Raw data (/proc/11561/stat): 11561 (minisat+_script) S 11560 11561 5245 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1842207039 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/11561/statm): 531 226 485 147 0 384 0 [pid=11561] vsize: 2124 Raw data (/proc/11565/stat): 11565 (minisat+_64-bit) R 11561 11561 5245 0 -1 0 12720 0 0 0 7837 70 0 0 25 0 1 0 1842207044 53026816 12707 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/11565/statm): 12946 12707 145 145 0 12801 0 [pid=11565] vsize: 51784 Current children cumulated CPU time (s) 79.08 Current children cumulated vsize (Kb) 53908 [startup+90.0117 s] Raw data (loadavg): 0.87 0.83 0.91 2/57 11565 Raw data (/proc/11561/stat): 11561 (minisat+_script) S 11560 11561 5245 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1842207039 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/11561/statm): 531 226 485 147 0 384 0 [pid=11561] vsize: 2124 Raw data (/proc/11565/stat): 11565 (minisat+_64-bit) R 11561 11561 5245 0 -1 0 13828 0 0 0 8820 77 0 0 25 0 1 0 1842207044 57552896 13815 4294967295 134512640 135094434 3221224448 3221223104 134557843 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/11565/statm): 14051 13815 145 145 0 13906 0 [pid=11565] vsize: 56204 Current children cumulated CPU time (s) 88.98 Current children cumulated vsize (Kb) 58328 [startup+100.013 s] Raw data (loadavg): 0.89 0.83 0.91 2/57 11565 Raw data (/proc/11561/stat): 11561 (minisat+_script) S 11560 11561 5245 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1842207039 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/11561/statm): 531 226 485 147 0 384 0 [pid=11561] vsize: 2124 Raw data (/proc/11565/stat): 11565 (minisat+_64-bit) R 11561 11561 5245 0 -1 0 14824 0 0 0 9804 83 0 0 25 0 1 0 1842207044 61620224 14811 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/11565/statm): 15044 14811 145 145 0 14899 0 [pid=11565] vsize: 60176 Current children cumulated CPU time (s) 98.88 Current children cumulated vsize (Kb) 62300 [startup+110.013 s] Raw data (loadavg): 0.91 0.84 0.91 2/57 11565 Raw data (/proc/11561/stat): 11561 (minisat+_script) S 11560 11561 5245 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1842207039 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/11561/statm): 531 226 485 147 0 384 0 [pid=11561] vsize: 2124 Raw data (/proc/11565/stat): 11565 (minisat+_64-bit) R 11561 11561 5245 0 -1 0 15657 0 0 0 10789 90 0 0 25 0 1 0 1842207044 65159168 15644 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/11565/statm): 15908 15644 145 145 0 15763 0 [pid=11565] vsize: 63632 Current children cumulated CPU time (s) 108.8 Current children cumulated vsize (Kb) 65756 [startup+120.015 s] Raw data (loadavg): 0.92 0.84 0.91 2/57 11565 Raw data (/proc/11561/stat): 11561 (minisat+_script) S 11560 11561 5245 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1842207039 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/11561/statm): 531 226 485 147 0 384 0 [pid=11561] vsize: 2124 Raw data (/proc/11565/stat): 11565 (minisat+_64-bit) R 11561 11561 5245 0 -1 0 16547 0 0 0 11773 96 0 0 25 0 1 0 1842207044 68800512 16534 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/11565/statm): 16797 16534 145 145 0 16652 0 [pid=11565] vsize: 67188 Current children cumulated CPU time (s) 118.7 Current children cumulated vsize (Kb) 69312 [startup+130.016 s] Raw data (loadavg): 0.93 0.85 0.91 2/57 11565 Raw data (/proc/11561/stat): 11561 (minisat+_script) S 11560 11561 5245 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1842207039 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/11561/statm): 531 226 485 147 0 384 0 [pid=11561] vsize: 2124 Raw data (/proc/11565/stat): 11565 (minisat+_64-bit) R 11561 11561 5245 0 -1 0 17378 0 0 0 12760 102 0 0 25 0 1 0 1842207044 72196096 17365 4294967295 134512640 135094434 3221224448 3221223136 134554731 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/11565/statm): 17626 17365 145 145 0 17481 0 [pid=11565] vsize: 70504 Current children cumulated CPU time (s) 128.63 Current children cumulated vsize (Kb) 72628 [startup+140.016 s] Raw data (loadavg): 0.94 0.85 0.91 2/57 11565 Raw data (/proc/11561/stat): 11561 (minisat+_script) S 11560 11561 5245 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1842207039 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/11561/statm): 531 226 485 147 0 384 0 [pid=11561] vsize: 2124 Raw data (/proc/11565/stat): 11565 (minisat+_64-bit) R 11561 11561 5245 0 -1 0 18035 0 0 0 13749 107 0 0 25 0 1 0 1842207044 74878976 18022 4294967295 134512640 135094434 3221224448 3221223104 134558019 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/11565/statm): 18281 18022 145 145 0 18136 0 [pid=11565] vsize: 73124 Current children cumulated CPU time (s) 138.57 Current children cumulated vsize (Kb) 75248 [startup+150.017 s] Raw data (loadavg): 0.95 0.85 0.91 2/57 11565 Raw data (/proc/11561/stat): 11561 (minisat+_script) S 11560 11561 5245 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1842207039 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/11561/statm): 531 226 485 147 0 384 0 [pid=11561] vsize: 2124 Raw data (/proc/11565/stat): 11565 (minisat+_64-bit) T 11561 11561 5245 0 -1 0 18824 0 0 0 14736 112 0 0 25 0 1 0 1842207044 78102528 18811 4294967295 134512640 135094434 3221224448 3221222812 134870330 0 0 5 16386 3222434794 0 0 17 1 0 0 Raw data (/proc/11565/statm): 19068 18811 145 145 0 18923 0 [pid=11565] vsize: 76272 Current children cumulated CPU time (s) 148.49 Current children cumulated vsize (Kb) 78396 [startup+160.017 s] Raw data (loadavg): 0.96 0.86 0.91 2/57 11565 Raw data (/proc/11561/stat): 11561 (minisat+_script) S 11560 11561 5245 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1842207039 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/11561/statm): 531 226 485 147 0 384 0 [pid=11561] vsize: 2124 Raw data (/proc/11565/stat): 11565 (minisat+_64-bit) R 11561 11561 5245 0 -1 0 19612 0 0 0 15724 117 0 0 25 0 1 0 1842207044 81321984 19599 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/11565/statm): 19854 19599 145 145 0 19709 0 [pid=11565] vsize: 79416 Current children cumulated CPU time (s) 158.42 Current children cumulated vsize (Kb) 81540 [startup+170.018 s] Raw data (loadavg): 0.96 0.86 0.91 2/57 11565 Raw data (/proc/11561/stat): 11561 (minisat+_script) S 11560 11561 5245 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1842207039 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/11561/statm): 531 226 485 147 0 384 0 [pid=11561] vsize: 2124 Raw data (/proc/11565/stat): 11565 (minisat+_64-bit) R 11561 11561 5245 0 -1 0 20283 0 0 0 16713 121 0 0 25 0 1 0 1842207044 84066304 20270 4294967295 134512640 135094434 3221224448 3221223104 134558213 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/11565/statm): 20524 20270 145 145 0 20379 0 [pid=11565] vsize: 82096 Current children cumulated CPU time (s) 168.35 Current children cumulated vsize (Kb) 84220 [startup+180.019 s] Raw data (loadavg): 0.97 0.87 0.91 2/57 11565 Raw data (/proc/11561/stat): 11561 (minisat+_script) S 11560 11561 5245 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1842207039 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/11561/statm): 531 226 485 147 0 384 0 [pid=11561] vsize: 2124 Raw data (/proc/11565/stat): 11565 (minisat+_64-bit) R 11561 11561 5245 0 -1 0 20897 0 0 0 17704 125 0 0 25 0 1 0 1842207044 86585344 20884 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/11565/statm): 21139 20884 145 145 0 20994 0 [pid=11565] vsize: 84556 Current children cumulated CPU time (s) 178.3 Current children cumulated vsize (Kb) 86680 [startup+190.02 s] Raw data (loadavg): 0.97 0.87 0.91 2/57 11565 Raw data (/proc/11561/stat): 11561 (minisat+_script) S 11560 11561 5245 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1842207039 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/11561/statm): 531 226 485 147 0 384 0 [pid=11561] vsize: 2124 Raw data (/proc/11565/stat): 11565 (minisat+_64-bit) R 11561 11561 5245 0 -1 0 21504 0 0 0 18692 131 0 0 25 0 1 0 1842207044 89071616 21491 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/11565/statm): 21746 21491 145 145 0 21601 0 [pid=11565] vsize: 86984 Current children cumulated CPU time (s) 188.24 Current children cumulated vsize (Kb) 89108 [startup+200.02 s] Raw data (loadavg): 0.98 0.87 0.91 2/57 11565 Raw data (/proc/11561/stat): 11561 (minisat+_script) S 11560 11561 5245 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1842207039 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/11561/statm): 531 226 485 147 0 384 0 [pid=11561] vsize: 2124 Raw data (/proc/11565/stat): 11565 (minisat+_64-bit) R 11561 11561 5245 0 -1 0 22102 0 0 0 19682 136 0 0 25 0 1 0 1842207044 91521024 22089 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/11565/statm): 22344 22089 145 145 0 22199 0 [pid=11565] vsize: 89376 Current children cumulated CPU time (s) 198.19 Current children cumulated vsize (Kb) 91500 [startup+210.021 s] Raw data (loadavg): 0.98 0.88 0.91 2/57 11565 Raw data (/proc/11561/stat): 11561 (minisat+_script) S 11560 11561 5245 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1842207039 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/11561/statm): 531 226 485 147 0 384 0 [pid=11561] vsize: 2124 Raw data (/proc/11565/stat): 11565 (minisat+_64-bit) R 11561 11561 5245 0 -1 0 22640 0 0 0 20673 140 0 0 25 0 1 0 1842207044 93732864 22627 4294967295 134512640 135094434 3221224448 3221223104 134558129 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/11565/statm): 22884 22627 145 145 0 22739 0 [pid=11565] vsize: 91536 Current children cumulated CPU time (s) 208.14 Current children cumulated vsize (Kb) 93660 [startup+220.023 s] Raw data (loadavg): 0.98 0.88 0.91 2/57 11565 Raw data (/proc/11561/stat): 11561 (minisat+_script) S 11560 11561 5245 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1842207039 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/11561/statm): 531 226 485 147 0 384 0 [pid=11561] vsize: 2124 Raw data (/proc/11565/stat): 11565 (minisat+_64-bit) T 11561 11561 5245 0 -1 0 23218 0 0 0 21662 146 0 0 25 0 1 0 1842207044 96088064 23205 4294967295 134512640 135094434 3221224448 3221222828 134870330 0 0 5 16386 3222434794 0 0 17 1 0 0 Raw data (/proc/11565/statm): 23459 23205 145 145 0 23314 0 [pid=11565] vsize: 93836 Current children cumulated CPU time (s) 218.09 Current children cumulated vsize (Kb) 95960 [startup+230.024 s] Raw data (loadavg): 0.98 0.89 0.91 2/57 11565 Raw data (/proc/11561/stat): 11561 (minisat+_script) S 11560 11561 5245 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1842207039 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/11561/statm): 531 226 485 147 0 384 0 [pid=11561] vsize: 2124 Raw data (/proc/11565/stat): 11565 (minisat+_64-bit) R 11561 11561 5245 0 -1 0 23832 0 0 0 22651 151 0 0 25 0 1 0 1842207044 98598912 23819 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/11565/statm): 24072 23819 145 145 0 23927 0 [pid=11565] vsize: 96288 Current children cumulated CPU time (s) 228.03 Current children cumulated vsize (Kb) 98412 [startup+240.025 s] Raw data (loadavg): 0.99 0.89 0.91 2/57 11565 Raw data (/proc/11561/stat): 11561 (minisat+_script) S 11560 11561 5245 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1842207039 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/11561/statm): 531 226 485 147 0 384 0 [pid=11561] vsize: 2124 Raw data (/proc/11565/stat): 11565 (minisat+_64-bit) R 11561 11561 5245 0 -1 0 24494 0 0 0 23642 155 0 0 25 0 1 0 1842207044 101302272 24481 4294967295 134512640 135094434 3221224448 3221223120 134555943 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/11565/statm): 24732 24481 145 145 0 24587 0 [pid=11565] vsize: 98928 Current children cumulated CPU time (s) 237.98 Current children cumulated vsize (Kb) 101052 [startup+250.025 s] Raw data (loadavg): 0.99 0.89 0.91 2/57 11565 Raw data (/proc/11561/stat): 11561 (minisat+_script) S 11560 11561 5245 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1842207039 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/11561/statm): 531 226 485 147 0 384 0 [pid=11561] vsize: 2124 Raw data (/proc/11565/stat): 11565 (minisat+_64-bit) R 11561 11561 5245 0 -1 0 24962 0 0 0 24635 158 0 0 25 0 1 0 1842207044 103235584 24949 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/11565/statm): 25204 24949 145 145 0 25059 0 [pid=11565] vsize: 100816 Current children cumulated CPU time (s) 247.94 Current children cumulated vsize (Kb) 102940 [startup+260.026 s] Raw data (loadavg): 0.99 0.89 0.91 1/57 11565 Raw data (/proc/11561/stat): 11561 (minisat+_script) S 11560 11561 5245 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1842207039 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/11561/statm): 531 226 485 147 0 384 0 [pid=11561] vsize: 2124 Raw data (/proc/11565/stat): 11565 (minisat+_64-bit) T 11561 11561 5245 0 -1 0 25647 0 0 0 25623 163 0 0 25 0 1 0 1842207044 106037248 25634 4294967295 134512640 135094434 3221224448 3221222812 134870330 0 0 5 16386 3222434794 0 0 17 1 0 0 Raw data (/proc/11565/statm): 25888 25634 145 145 0 25743 0 [pid=11565] vsize: 103552 Current children cumulated CPU time (s) 257.87 Current children cumulated vsize (Kb) 105676 [startup+270.027 s] Raw data (loadavg): 0.99 0.90 0.91 2/57 11565 Raw data (/proc/11561/stat): 11561 (minisat+_script) S 11560 11561 5245 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1842207039 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/11561/statm): 531 226 485 147 0 384 0 [pid=11561] vsize: 2124 Raw data (/proc/11565/stat): 11565 (minisat+_64-bit) R 11561 11561 5245 0 -1 0 26351 0 0 0 26611 168 0 0 19 0 1 0 1842207044 108916736 26338 4294967295 134512640 135094434 3221224448 3221223104 134558019 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/11565/statm): 26591 26338 145 145 0 26446 0 [pid=11565] vsize: 106364 Current children cumulated CPU time (s) 267.8 Current children cumulated vsize (Kb) 108488 [startup+280.028 s] Raw data (loadavg): 0.99 0.90 0.91 2/57 11565 Raw data (/proc/11561/stat): 11561 (minisat+_script) S 11560 11561 5245 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1842207039 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/11561/statm): 531 226 485 147 0 384 0 [pid=11561] vsize: 2124 Raw data (/proc/11565/stat): 11565 (minisat+_64-bit) R 11561 11561 5245 0 -1 0 27007 0 0 0 27601 172 0 0 25 0 1 0 1842207044 111595520 26994 4294967295 134512640 135094434 3221224448 3221223120 134556460 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/11565/statm): 27245 26994 145 145 0 27100 0 [pid=11565] vsize: 108980 Current children cumulated CPU time (s) 277.74 Current children cumulated vsize (Kb) 111104 [startup+290.029 s] Raw data (loadavg): 0.99 0.90 0.91 1/57 11565 Raw data (/proc/11561/stat): 11561 (minisat+_script) S 11560 11561 5245 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1842207039 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/11561/statm): 531 226 485 147 0 384 0 [pid=11561] vsize: 2124 Raw data (/proc/11565/stat): 11565 (minisat+_64-bit) T 11561 11561 5245 0 -1 0 27726 0 0 0 28590 176 0 0 25 0 1 0 1842207044 114544640 27713 4294967295 134512640 135094434 3221224448 3221222812 134870330 0 0 5 16386 3222434794 0 0 17 1 0 0 Raw data (/proc/11565/statm): 27965 27713 145 145 0 27820 0 [pid=11565] vsize: 111860 Current children cumulated CPU time (s) 287.67 Current children cumulated vsize (Kb) 113984 [startup+300.029 s] Raw data (loadavg): 0.99 0.91 0.91 2/57 11565 Raw data (/proc/11561/stat): 11561 (minisat+_script) S 11560 11561 5245 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1842207039 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/11561/statm): 531 226 485 147 0 384 0 [pid=11561] vsize: 2124 Raw data (/proc/11565/stat): 11565 (minisat+_64-bit) R 11561 11561 5245 0 -1 0 28380 0 0 0 29578 182 0 0 25 0 1 0 1842207044 117473280 28367 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/11565/statm): 28680 28367 145 145 0 28535 0 [pid=11565] vsize: 114720 Current children cumulated CPU time (s) 297.61 Current children cumulated vsize (Kb) 116844 [startup+310.03 s] Raw data (loadavg): 0.99 0.91 0.91 2/57 11565 Raw data (/proc/11561/stat): 11561 (minisat+_script) S 11560 11561 5245 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1842207039 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/11561/statm): 531 226 485 147 0 384 0 [pid=11561] vsize: 2124 Raw data (/proc/11565/stat): 11565 (minisat+_64-bit) R 11561 11561 5245 0 -1 0 29061 0 0 0 30567 187 0 0 25 0 1 0 1842207044 120262656 29048 4294967295 134512640 135094434 3221224448 3221223104 134558009 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/11565/statm): 29361 29048 145 145 0 29216 0 [pid=11565] vsize: 117444 Current children cumulated CPU time (s) 307.55 Current children cumulated vsize (Kb) 119568 [startup+320.031 s] Raw data (loadavg): 0.99 0.91 0.91 2/57 11565 Raw data (/proc/11561/stat): 11561 (minisat+_script) S 11560 11561 5245 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1842207039 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/11561/statm): 531 226 485 147 0 384 0 [pid=11561] vsize: 2124 Raw data (/proc/11565/stat): 11565 (minisat+_64-bit) R 11561 11561 5245 0 -1 0 29675 0 0 0 31557 190 0 0 25 0 1 0 1842207044 122789888 29662 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/11565/statm): 29978 29662 145 145 0 29833 0 [pid=11565] vsize: 119912 Current children cumulated CPU time (s) 317.48 Current children cumulated vsize (Kb) 122036 [startup+330.032 s] Raw data (loadavg): 0.99 0.91 0.91 2/57 11565 Raw data (/proc/11561/stat): 11561 (minisat+_script) S 11560 11561 5245 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1842207039 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/11561/statm): 531 226 485 147 0 384 0 [pid=11561] vsize: 2124 Raw data (/proc/11565/stat): 11565 (minisat+_64-bit) R 11561 11561 5245 0 -1 0 30306 0 0 0 32547 194 0 0 25 0 1 0 1842207044 125382656 30293 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/11565/statm): 30611 30293 145 145 0 30466 0 [pid=11565] vsize: 122444 Current children cumulated CPU time (s) 327.42 Current children cumulated vsize (Kb) 124568 [startup+340.033 s] Raw data (loadavg): 0.99 0.92 0.91 2/57 11565 Raw data (/proc/11561/stat): 11561 (minisat+_script) S 11560 11561 5245 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1842207039 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/11561/statm): 531 226 485 147 0 384 0 [pid=11561] vsize: 2124 Raw data (/proc/11565/stat): 11565 (minisat+_64-bit) R 11561 11561 5245 0 -1 0 30867 0 0 0 33537 199 0 0 25 0 1 0 1842207044 127672320 30854 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/11565/statm): 31170 30854 145 145 0 31025 0 [pid=11565] vsize: 124680 Current children cumulated CPU time (s) 337.37 Current children cumulated vsize (Kb) 126804 [startup+350.033 s] Raw data (loadavg): 0.99 0.92 0.91 2/57 11565 Raw data (/proc/11561/stat): 11561 (minisat+_script) S 11560 11561 5245 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1842207039 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/11561/statm): 531 226 485 147 0 384 0 [pid=11561] vsize: 2124 Raw data (/proc/11565/stat): 11565 (minisat+_64-bit) R 11561 11561 5245 0 -1 0 31457 0 0 0 34528 202 0 0 25 0 1 0 1842207044 130080768 31444 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/11565/statm): 31758 31444 145 145 0 31613 0 [pid=11565] vsize: 127032 Current children cumulated CPU time (s) 347.31 Current children cumulated vsize (Kb) 129156 [startup+360.034 s] Raw data (loadavg): 0.99 0.92 0.91 2/57 11565 Raw data (/proc/11561/stat): 11561 (minisat+_script) S 11560 11561 5245 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1842207039 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/11561/statm): 531 226 485 147 0 384 0 [pid=11561] vsize: 2124 Raw data (/proc/11565/stat): 11565 (minisat+_64-bit) T 11561 11561 5245 0 -1 0 32072 0 0 0 35519 206 0 0 25 0 1 0 1842207044 132603904 32059 4294967295 134512640 135094434 3221224448 3221222828 134870330 0 0 5 16386 3222434794 0 0 17 1 0 0 Raw data (/proc/11565/statm): 32374 32059 145 145 0 32229 0 [pid=11565] vsize: 129496 Current children cumulated CPU time (s) 357.26 Current children cumulated vsize (Kb) 131620 [startup+370.035 s] Raw data (loadavg): 0.99 0.92 0.91 2/57 11565 Raw data (/proc/11561/stat): 11561 (minisat+_script) S 11560 11561 5245 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1842207039 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/11561/statm): 531 226 485 147 0 384 0 [pid=11561] vsize: 2124 Raw data (/proc/11565/stat): 11565 (minisat+_64-bit) R 11561 11561 5245 0 -1 0 32655 0 0 0 36509 211 0 0 25 0 1 0 1842207044 135000064 32642 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/11565/statm): 32959 32642 145 145 0 32814 0 [pid=11565] vsize: 131836 Current children cumulated CPU time (s) 367.21 Current children cumulated vsize (Kb) 133960 [startup+380.036 s] Raw data (loadavg): 0.99 0.92 0.91 1/57 11565 Raw data (/proc/11561/stat): 11561 (minisat+_script) S 11560 11561 5245 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1842207039 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/11561/statm): 531 226 485 147 0 384 0 [pid=11561] vsize: 2124 Raw data (/proc/11565/stat): 11565 (minisat+_64-bit) T 11561 11561 5245 0 -1 0 33229 0 0 0 37499 215 0 0 25 0 1 0 1842207044 137359360 33216 4294967295 134512640 135094434 3221224448 3221222812 134870330 0 0 5 16386 3222434794 0 0 17 1 0 0 Raw data (/proc/11565/statm): 33535 33216 145 145 0 33390 0 [pid=11565] vsize: 134140 Current children cumulated CPU time (s) 377.15 Current children cumulated vsize (Kb) 136264 [startup+390.036 s] Raw data (loadavg): 0.99 0.93 0.91 2/57 11565 Raw data (/proc/11561/stat): 11561 (minisat+_script) S 11560 11561 5245 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1842207039 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/11561/statm): 531 226 485 147 0 384 0 [pid=11561] vsize: 2124 Raw data (/proc/11565/stat): 11565 (minisat+_64-bit) R 11561 11561 5245 0 -1 0 33780 0 0 0 38491 217 0 0 25 0 1 0 1842207044 139636736 33767 4294967295 134512640 135094434 3221224448 3221223104 134558013 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/11565/statm): 34091 33767 145 145 0 33946 0 [pid=11565] vsize: 136364 Current children cumulated CPU time (s) 387.09 Current children cumulated vsize (Kb) 138488 [startup+400.037 s] Raw data (loadavg): 0.99 0.93 0.91 2/57 11565 Raw data (/proc/11561/stat): 11561 (minisat+_script) S 11560 11561 5245 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1842207039 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/11561/statm): 531 226 485 147 0 384 0 [pid=11561] vsize: 2124 Raw data (/proc/11565/stat): 11565 (minisat+_64-bit) R 11561 11561 5245 0 -1 0 34277 0 0 0 39484 220 0 0 25 0 1 0 1842207044 141684736 34264 4294967295 134512640 135094434 3221224448 3221223104 134558022 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/11565/statm): 34591 34264 145 145 0 34446 0 [pid=11565] vsize: 138364 Current children cumulated CPU time (s) 397.05 Current children cumulated vsize (Kb) 140488 [startup+410.038 s] Raw data (loadavg): 0.99 0.93 0.91 2/57 11565 Raw data (/proc/11561/stat): 11561 (minisat+_script) S 11560 11561 5245 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1842207039 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/11561/statm): 531 226 485 147 0 384 0 [pid=11561] vsize: 2124 Raw data (/proc/11565/stat): 11565 (minisat+_64-bit) R 11561 11561 5245 0 -1 0 34807 0 0 0 40474 224 0 0 25 0 1 0 1842207044 143859712 34794 4294967295 134512640 135094434 3221224448 3221223104 134558013 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/11565/statm): 35122 34794 145 145 0 34977 0 [pid=11565] vsize: 140488 Current children cumulated CPU time (s) 406.99 Current children cumulated vsize (Kb) 142612 [startup+420.04 s] Raw data (loadavg): 0.99 0.93 0.91 2/57 11565 Raw data (/proc/11561/stat): 11561 (minisat+_script) S 11560 11561 5245 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1842207039 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/11561/statm): 531 226 485 147 0 384 0 [pid=11561] vsize: 2124 Raw data (/proc/11565/stat): 11565 (minisat+_64-bit) R 11561 11561 5245 0 -1 0 35263 0 0 0 41468 226 0 0 25 0 1 0 1842207044 145723392 35250 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/11565/statm): 35577 35250 145 145 0 35432 0 [pid=11565] vsize: 142308 Current children cumulated CPU time (s) 416.95 Current children cumulated vsize (Kb) 144432 [startup+430.041 s] Raw data (loadavg): 0.99 0.93 0.91 2/57 11565 Raw data (/proc/11561/stat): 11561 (minisat+_script) S 11560 11561 5245 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1842207039 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/11561/statm): 531 226 485 147 0 384 0 [pid=11561] vsize: 2124 Raw data (/proc/11565/stat): 11565 (minisat+_64-bit) R 11561 11561 5245 0 -1 0 35702 0 0 0 42462 229 0 0 25 0 1 0 1842207044 147525632 35689 4294967295 134512640 135094434 3221224448 3221223104 134558208 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/11565/statm): 36017 35689 145 145 0 35872 0 [pid=11565] vsize: 144068 Current children cumulated CPU time (s) 426.92 Current children cumulated vsize (Kb) 146192 [startup+440.04 s] Raw data (loadavg): 0.99 0.94 0.91 2/57 11565 Raw data (/proc/11561/stat): 11561 (minisat+_script) S 11560 11561 5245 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1842207039 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/11561/statm): 531 226 485 147 0 384 0 [pid=11561] vsize: 2124 Raw data (/proc/11565/stat): 11565 (minisat+_64-bit) R 11561 11561 5245 0 -1 0 36169 0 0 0 43456 231 0 0 25 0 1 0 1842207044 149434368 36156 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/11565/statm): 36483 36156 145 145 0 36338 0 [pid=11565] vsize: 145932 Current children cumulated CPU time (s) 436.88 Current children cumulated vsize (Kb) 148056 [startup+450.041 s] Raw data (loadavg): 0.99 0.94 0.91 2/57 11565 Raw data (/proc/11561/stat): 11561 (minisat+_script) S 11560 11561 5245 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1842207039 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/11561/statm): 531 226 485 147 0 384 0 [pid=11561] vsize: 2124 Raw data (/proc/11565/stat): 11565 (minisat+_64-bit) R 11561 11561 5245 0 -1 0 36622 0 0 0 44449 235 0 0 25 0 1 0 1842207044 151302144 36609 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/11565/statm): 36939 36609 145 145 0 36794 0 [pid=11565] vsize: 147756 Current children cumulated CPU time (s) 446.85 Current children cumulated vsize (Kb) 149880 [startup+460.042 s] Raw data (loadavg): 0.99 0.94 0.91 2/57 11565 Raw data (/proc/11561/stat): 11561 (minisat+_script) S 11560 11561 5245 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1842207039 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/11561/statm): 531 226 485 147 0 384 0 [pid=11561] vsize: 2124 Raw data (/proc/11565/stat): 11565 (minisat+_64-bit) R 11561 11561 5245 0 -1 0 37098 0 0 0 45443 238 0 0 25 0 1 0 1842207044 153255936 37085 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/11565/statm): 37416 37085 145 145 0 37271 0 [pid=11565] vsize: 149664 Current children cumulated CPU time (s) 456.82 Current children cumulated vsize (Kb) 151788 [startup+470.043 s] Raw data (loadavg): 0.99 0.94 0.91 2/57 11565 Raw data (/proc/11561/stat): 11561 (minisat+_script) S 11560 11561 5245 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1842207039 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/11561/statm): 531 226 485 147 0 384 0 [pid=11561] vsize: 2124 Raw data (/proc/11565/stat): 11565 (minisat+_64-bit) R 11561 11561 5245 0 -1 0 37649 0 0 0 46435 241 0 0 25 0 1 0 1842207044 155512832 37636 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/11565/statm): 37967 37636 145 145 0 37822 0 [pid=11565] vsize: 151868 Current children cumulated CPU time (s) 466.77 Current children cumulated vsize (Kb) 153992 [startup+480.044 s] Raw data (loadavg): 0.99 0.94 0.91 2/57 11565 Raw data (/proc/11561/stat): 11561 (minisat+_script) S 11560 11561 5245 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1842207039 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/11561/statm): 531 226 485 147 0 384 0 [pid=11561] vsize: 2124 Raw data (/proc/11565/stat): 11565 (minisat+_64-bit) R 11561 11561 5245 0 -1 0 38224 0 0 0 47427 243 0 0 25 0 1 0 1842207044 157868032 38211 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/11565/statm): 38542 38211 145 145 0 38397 0 [pid=11565] vsize: 154168 Current children cumulated CPU time (s) 476.71 Current children cumulated vsize (Kb) 156292 [startup+490.044 s] Raw data (loadavg): 0.99 0.94 0.91 2/57 11565 Raw data (/proc/11561/stat): 11561 (minisat+_script) S 11560 11561 5245 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1842207039 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/11561/statm): 531 226 485 147 0 384 0 [pid=11561] vsize: 2124 Raw data (/proc/11565/stat): 11565 (minisat+_64-bit) R 11561 11561 5245 0 -1 0 38702 0 0 0 48421 246 0 0 25 0 1 0 1842207044 159821824 38689 4294967295 134512640 135094434 3221224448 3221223104 134558213 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/11565/statm): 39019 38689 145 145 0 38874 0 [pid=11565] vsize: 156076 Current children cumulated CPU time (s) 486.68 Current children cumulated vsize (Kb) 158200 [startup+500.045 s] Raw data (loadavg): 0.99 0.94 0.91 2/57 11565 Raw data (/proc/11561/stat): 11561 (minisat+_script) S 11560 11561 5245 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1842207039 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/11561/statm): 531 226 485 147 0 384 0 [pid=11561] vsize: 2124 Raw data (/proc/11565/stat): 11565 (minisat+_64-bit) R 11561 11561 5245 0 -1 0 39196 0 0 0 49412 250 0 0 19 0 1 0 1842207044 161873920 39183 4294967295 134512640 135094434 3221224448 3221223104 134558178 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/11565/statm): 39520 39183 145 145 0 39375 0 [pid=11565] vsize: 158080 Current children cumulated CPU time (s) 496.63 Current children cumulated vsize (Kb) 160204 [startup+510.046 s] Raw data (loadavg): 0.99 0.95 0.91 2/57 11565 Raw data (/proc/11561/stat): 11561 (minisat+_script) S 11560 11561 5245 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1842207039 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/11561/statm): 531 226 485 147 0 384 0 [pid=11561] vsize: 2124 Raw data (/proc/11565/stat): 11565 (minisat+_64-bit) R 11561 11561 5245 0 -1 0 39580 0 0 0 50407 253 0 0 25 0 1 0 1842207044 163450880 39567 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/11565/statm): 39905 39567 145 145 0 39760 0 [pid=11565] vsize: 159620 Current children cumulated CPU time (s) 506.61 Current children cumulated vsize (Kb) 161744 [startup+520.047 s] Raw data (loadavg): 0.99 0.95 0.91 2/57 11565 Raw data (/proc/11561/stat): 11561 (minisat+_script) S 11560 11561 5245 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1842207039 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/11561/statm): 531 226 485 147 0 384 0 [pid=11561] vsize: 2124 Raw data (/proc/11565/stat): 11565 (minisat+_64-bit) T 11561 11561 5245 0 -1 0 39969 0 0 0 51400 255 0 0 25 0 1 0 1842207044 165048320 39956 4294967295 134512640 135094434 3221224448 3221222828 134870330 0 0 5 16386 3222434794 0 0 17 1 0 0 Raw data (/proc/11565/statm): 40295 39956 145 145 0 40150 0 [pid=11565] vsize: 161180 Current children cumulated CPU time (s) 516.56 Current children cumulated vsize (Kb) 163304 [startup+530.048 s] Raw data (loadavg): 0.99 0.95 0.91 2/57 11565 Raw data (/proc/11561/stat): 11561 (minisat+_script) S 11560 11561 5245 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1842207039 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/11561/statm): 531 226 485 147 0 384 0 [pid=11561] vsize: 2124 Raw data (/proc/11565/stat): 11565 (minisat+_64-bit) R 11561 11561 5245 0 -1 0 40329 0 0 0 52393 257 0 0 25 0 1 0 1842207044 166518784 40316 4294967295 134512640 135094434 3221224448 3221223104 134558009 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/11565/statm): 40654 40316 145 145 0 40509 0 [pid=11565] vsize: 162616 Current children cumulated CPU time (s) 526.51 Current children cumulated vsize (Kb) 164740 [startup+540.048 s] Raw data (loadavg): 0.99 0.95 0.91 2/57 11565 Raw data (/proc/11561/stat): 11561 (minisat+_script) S 11560 11561 5245 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1842207039 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/11561/statm): 531 226 485 147 0 384 0 [pid=11561] vsize: 2124 Raw data (/proc/11565/stat): 11565 (minisat+_64-bit) R 11561 11561 5245 0 -1 0 40666 0 0 0 53388 259 0 0 25 0 1 0 1842207044 167915520 40653 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/11565/statm): 40995 40653 145 145 0 40850 0 [pid=11565] vsize: 163980 Current children cumulated CPU time (s) 536.48 Current children cumulated vsize (Kb) 166104 [startup+550.049 s] Raw data (loadavg): 0.99 0.95 0.91 2/57 11565 Raw data (/proc/11561/stat): 11561 (minisat+_script) S 11560 11561 5245 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1842207039 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/11561/statm): 531 226 485 147 0 384 0 [pid=11561] vsize: 2124 Raw data (/proc/11565/stat): 11565 (minisat+_64-bit) R 11561 11561 5245 0 -1 0 41106 0 0 0 54381 262 0 0 25 0 1 0 1842207044 169713664 41093 4294967295 134512640 135094434 3221224448 3221223040 134557236 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/11565/statm): 41434 41093 145 145 0 41289 0 [pid=11565] vsize: 165736 Current children cumulated CPU time (s) 546.44 Current children cumulated vsize (Kb) 167860 [startup+560.05 s] Raw data (loadavg): 0.99 0.95 0.91 2/57 11565 Raw data (/proc/11561/stat): 11561 (minisat+_script) S 11560 11561 5245 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1842207039 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/11561/statm): 531 226 485 147 0 384 0 [pid=11561] vsize: 2124 Raw data (/proc/11565/stat): 11565 (minisat+_64-bit) R 11561 11561 5245 0 -1 0 41542 0 0 0 55373 265 0 0 25 0 1 0 1842207044 171499520 41529 4294967295 134512640 135094434 3221224448 3221223040 134557208 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/11565/statm): 41870 41529 145 145 0 41725 0 [pid=11565] vsize: 167480 Current children cumulated CPU time (s) 556.39 Current children cumulated vsize (Kb) 169604 [startup+570.051 s] Raw data (loadavg): 0.99 0.95 0.91 2/57 11565 Raw data (/proc/11561/stat): 11561 (minisat+_script) S 11560 11561 5245 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1842207039 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/11561/statm): 531 226 485 147 0 384 0 [pid=11561] vsize: 2124 Raw data (/proc/11565/stat): 11565 (minisat+_64-bit) R 11561 11561 5245 0 -1 0 41976 0 0 0 56365 268 0 0 25 0 1 0 1842207044 173277184 41963 4294967295 134512640 135094434 3221224448 3221223104 134558009 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/11565/statm): 42304 41963 145 145 0 42159 0 [pid=11565] vsize: 169216 Current children cumulated CPU time (s) 566.34 Current children cumulated vsize (Kb) 171340 [startup+580.052 s] Raw data (loadavg): 0.99 0.95 0.91 2/57 11565 Raw data (/proc/11561/stat): 11561 (minisat+_script) S 11560 11561 5245 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1842207039 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/11561/statm): 531 226 485 147 0 384 0 [pid=11561] vsize: 2124 Raw data (/proc/11565/stat): 11565 (minisat+_64-bit) R 11561 11561 5245 0 -1 0 42379 0 0 0 57359 271 0 0 25 0 1 0 1842207044 174936064 42366 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/11565/statm): 42709 42366 145 145 0 42564 0 [pid=11565] vsize: 170836 Current children cumulated CPU time (s) 576.31 Current children cumulated vsize (Kb) 172960 [startup+590.051 s] Raw data (loadavg): 0.99 0.95 0.91 2/57 11565 Raw data (/proc/11561/stat): 11561 (minisat+_script) S 11560 11561 5245 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1842207039 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/11561/statm): 531 226 485 147 0 384 0 [pid=11561] vsize: 2124 Raw data (/proc/11565/stat): 11565 (minisat+_64-bit) R 11561 11561 5245 0 -1 0 42725 0 0 0 58353 273 0 0 25 0 1 0 1842207044 176345088 42712 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/11565/statm): 43053 42712 145 145 0 42908 0 [pid=11565] vsize: 172212 Current children cumulated CPU time (s) 586.27 Current children cumulated vsize (Kb) 174336 [startup+600.053 s] Raw data (loadavg): 0.99 0.95 0.91 2/57 11565 Raw data (/proc/11561/stat): 11561 (minisat+_script) S 11560 11561 5245 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1842207039 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/11561/statm): 531 226 485 147 0 384 0 [pid=11561] vsize: 2124 Raw data (/proc/11565/stat): 11565 (minisat+_64-bit) R 11561 11561 5245 0 -1 0 43084 0 0 0 59345 277 0 0 25 0 1 0 1842207044 177807360 43071 4294967295 134512640 135094434 3221224448 3221223104 134558208 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/11565/statm): 43410 43071 145 145 0 43265 0 [pid=11565] vsize: 173640 Current children cumulated CPU time (s) 596.23 Current children cumulated vsize (Kb) 175764 [startup+610.054 s] Raw data (loadavg): 0.99 0.95 0.91 2/57 11565 Raw data (/proc/11561/stat): 11561 (minisat+_script) S 11560 11561 5245 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1842207039 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/11561/statm): 531 226 485 147 0 384 0 [pid=11561] vsize: 2124 Raw data (/proc/11565/stat): 11565 (minisat+_64-bit) R 11561 11561 5245 0 -1 0 43511 0 0 0 60338 280 0 0 25 0 1 0 1842207044 179548160 43498 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/11565/statm): 43835 43498 145 145 0 43690 0 [pid=11565] vsize: 175340 Current children cumulated CPU time (s) 606.19 Current children cumulated vsize (Kb) 177464 [startup+620.055 s] Raw data (loadavg): 0.99 0.96 0.91 2/57 11565 Raw data (/proc/11561/stat): 11561 (minisat+_script) S 11560 11561 5245 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1842207039 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/11561/statm): 531 226 485 147 0 384 0 [pid=11561] vsize: 2124 Raw data (/proc/11565/stat): 11565 (minisat+_64-bit) R 11561 11561 5245 0 -1 0 43939 0 0 0 61331 283 0 0 25 0 1 0 1842207044 181293056 43926 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/11565/statm): 44261 43926 145 145 0 44116 0 [pid=11565] vsize: 177044 Current children cumulated CPU time (s) 616.15 Current children cumulated vsize (Kb) 179168 [startup+630.056 s] Raw data (loadavg): 0.99 0.96 0.91 2/57 11565 Raw data (/proc/11561/stat): 11561 (minisat+_script) S 11560 11561 5245 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1842207039 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/11561/statm): 531 226 485 147 0 384 0 [pid=11561] vsize: 2124 Raw data (/proc/11565/stat): 11565 (minisat+_64-bit) R 11561 11561 5245 0 -1 0 44354 0 0 0 62324 286 0 0 25 0 1 0 1842207044 182992896 44341 4294967295 134512640 135094434 3221224448 3221223104 134558178 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/11565/statm): 44676 44341 145 145 0 44531 0 [pid=11565] vsize: 178704 Current children cumulated CPU time (s) 626.11 Current children cumulated vsize (Kb) 180828 [startup+640.056 s] Raw data (loadavg): 0.99 0.96 0.91 2/57 11565 Raw data (/proc/11561/stat): 11561 (minisat+_script) S 11560 11561 5245 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1842207039 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/11561/statm): 531 226 485 147 0 384 0 [pid=11561] vsize: 2124 Raw data (/proc/11565/stat): 11565 (minisat+_64-bit) R 11561 11561 5245 0 -1 0 44741 0 0 0 63318 288 0 0 25 0 1 0 1842207044 184569856 44728 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/11565/statm): 45061 44728 145 145 0 44916 0 [pid=11565] vsize: 180244 Current children cumulated CPU time (s) 636.07 Current children cumulated vsize (Kb) 182368 [startup+650.057 s] Raw data (loadavg): 0.99 0.96 0.91 2/57 11565 Raw data (/proc/11561/stat): 11561 (minisat+_script) S 11560 11561 5245 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1842207039 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/11561/statm): 531 226 485 147 0 384 0 [pid=11561] vsize: 2124 Raw data (/proc/11565/stat): 11565 (minisat+_64-bit) R 11561 11561 5245 0 -1 0 45122 0 0 0 64311 291 0 0 25 0 1 0 1842207044 186150912 45109 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/11565/statm): 45447 45109 145 145 0 45302 0 [pid=11565] vsize: 181788 Current children cumulated CPU time (s) 646.03 Current children cumulated vsize (Kb) 183912 [startup+660.058 s] Raw data (loadavg): 0.99 0.96 0.91 2/57 11565 Raw data (/proc/11561/stat): 11561 (minisat+_script) S 11560 11561 5245 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1842207039 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/11561/statm): 531 226 485 147 0 384 0 [pid=11561] vsize: 2124 Raw data (/proc/11565/stat): 11565 (minisat+_64-bit) R 11561 11561 5245 0 -1 0 45520 0 0 0 65304 294 0 0 25 0 1 0 1842207044 187777024 45507 4294967295 134512640 135094434 3221224448 3221223040 134557421 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/11565/statm): 45844 45507 145 145 0 45699 0 [pid=11565] vsize: 183376 Current children cumulated CPU time (s) 655.99 Current children cumulated vsize (Kb) 185500 [startup+670.059 s] Raw data (loadavg): 0.99 0.96 0.91 2/57 11565 Raw data (/proc/11561/stat): 11561 (minisat+_script) S 11560 11561 5245 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1842207039 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/11561/statm): 531 226 485 147 0 384 0 [pid=11561] vsize: 2124 Raw data (/proc/11565/stat): 11565 (minisat+_64-bit) R 11561 11561 5245 0 -1 0 45951 0 0 0 66297 297 0 0 25 0 1 0 1842207044 189538304 45938 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/11565/statm): 46274 45938 145 145 0 46129 0 [pid=11565] vsize: 185096 Current children cumulated CPU time (s) 665.95 Current children cumulated vsize (Kb) 187220 [startup+680.059 s] Raw data (loadavg): 0.99 0.96 0.91 2/57 11565 Raw data (/proc/11561/stat): 11561 (minisat+_script) S 11560 11561 5245 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1842207039 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/11561/statm): 531 226 485 147 0 384 0 [pid=11561] vsize: 2124 Raw data (/proc/11565/stat): 11565 (minisat+_64-bit) R 11561 11561 5245 0 -1 0 45964 0 0 0 67297 297 0 0 25 0 1 0 1842207044 189591552 45951 4294967295 134512640 135094434 3221224448 3221223104 134557863 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/11565/statm): 46287 45951 145 145 0 46142 0 [pid=11565] vsize: 185148 Current children cumulated CPU time (s) 675.95 Current children cumulated vsize (Kb) 187272 [startup+690.06 s] Raw data (loadavg): 0.99 0.96 0.91 2/57 11565 Raw data (/proc/11561/stat): 11561 (minisat+_script) S 11560 11561 5245 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1842207039 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/11561/statm): 531 226 485 147 0 384 0 [pid=11561] vsize: 2124 Raw data (/proc/11565/stat): 11565 (minisat+_64-bit) R 11561 11561 5245 0 -1 0 45964 0 0 0 68298 297 0 0 25 0 1 0 1842207044 189591552 45951 4294967295 134512640 135094434 3221224448 3221223136 134554746 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/11565/statm): 46287 45951 145 145 0 46142 0 [pid=11565] vsize: 185148 Current children cumulated CPU time (s) 685.96 Current children cumulated vsize (Kb) 187272 [startup+700.061 s] Raw data (loadavg): 0.99 0.96 0.91 2/57 11565 Raw data (/proc/11561/stat): 11561 (minisat+_script) S 11560 11561 5245 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1842207039 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/11561/statm): 531 226 485 147 0 384 0 [pid=11561] vsize: 2124 Raw data (/proc/11565/stat): 11565 (minisat+_64-bit) R 11561 11561 5245 0 -1 0 45965 0 0 0 69298 297 0 0 25 0 1 0 1842207044 189591552 45952 4294967295 134512640 135094434 3221224448 3221223104 134558009 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/11565/statm): 46287 45952 145 145 0 46142 0 [pid=11565] vsize: 185148 Current children cumulated CPU time (s) 695.96 Current children cumulated vsize (Kb) 187272 [startup+710.062 s] Raw data (loadavg): 0.99 0.96 0.91 2/57 11565 Raw data (/proc/11561/stat): 11561 (minisat+_script) S 11560 11561 5245 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1842207039 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/11561/statm): 531 226 485 147 0 384 0 [pid=11561] vsize: 2124 Raw data (/proc/11565/stat): 11565 (minisat+_64-bit) R 11561 11561 5245 0 -1 0 45967 0 0 0 70298 297 0 0 25 0 1 0 1842207044 189591552 45954 4294967295 134512640 135094434 3221224448 3221223104 134558213 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/11565/statm): 46287 45954 145 145 0 46142 0 [pid=11565] vsize: 185148 Current children cumulated CPU time (s) 705.96 Current children cumulated vsize (Kb) 187272 [startup+720.064 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 11565 Raw data (/proc/11561/stat): 11561 (minisat+_script) S 11560 11561 5245 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1842207039 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/11561/statm): 531 226 485 147 0 384 0 [pid=11561] vsize: 2124 Raw data (/proc/11565/stat): 11565 (minisat+_64-bit) R 11561 11561 5245 0 -1 0 45967 0 0 0 71298 297 0 0 25 0 1 0 1842207044 189591552 45954 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/11565/statm): 46287 45954 145 145 0 46142 0 [pid=11565] vsize: 185148 Current children cumulated CPU time (s) 715.96 Current children cumulated vsize (Kb) 187272 [startup+730.064 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 11565 Raw data (/proc/11561/stat): 11561 (minisat+_script) S 11560 11561 5245 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1842207039 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/11561/statm): 531 226 485 147 0 384 0 [pid=11561] vsize: 2124 Raw data (/proc/11565/stat): 11565 (minisat+_64-bit) R 11561 11561 5245 0 -1 0 45968 0 0 0 72298 297 0 0 25 0 1 0 1842207044 189591552 45955 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/11565/statm): 46287 45955 145 145 0 46142 0 [pid=11565] vsize: 185148 Current children cumulated CPU time (s) 725.96 Current children cumulated vsize (Kb) 187272 [startup+740.064 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 11565 Raw data (/proc/11561/stat): 11561 (minisat+_script) S 11560 11561 5245 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1842207039 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/11561/statm): 531 226 485 147 0 384 0 [pid=11561] vsize: 2124 Raw data (/proc/11565/stat): 11565 (minisat+_64-bit) R 11561 11561 5245 0 -1 0 45968 0 0 0 73298 297 0 0 25 0 1 0 1842207044 189591552 45955 4294967295 134512640 135094434 3221224448 3221223120 134555849 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/11565/statm): 46287 45955 145 145 0 46142 0 [pid=11565] vsize: 185148 Current children cumulated CPU time (s) 735.96 Current children cumulated vsize (Kb) 187272 [startup+750.065 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 11565 Raw data (/proc/11561/stat): 11561 (minisat+_script) S 11560 11561 5245 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1842207039 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/11561/statm): 531 226 485 147 0 384 0 [pid=11561] vsize: 2124 Raw data (/proc/11565/stat): 11565 (minisat+_64-bit) R 11561 11561 5245 0 -1 0 45968 0 0 0 74299 297 0 0 25 0 1 0 1842207044 189591552 45955 4294967295 134512640 135094434 3221224448 3221223104 134558019 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/11565/statm): 46287 45955 145 145 0 46142 0 [pid=11565] vsize: 185148 Current children cumulated CPU time (s) 745.97 Current children cumulated vsize (Kb) 187272 [startup+760.066 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 11565 Raw data (/proc/11561/stat): 11561 (minisat+_script) S 11560 11561 5245 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1842207039 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/11561/statm): 531 226 485 147 0 384 0 [pid=11561] vsize: 2124 Raw data (/proc/11565/stat): 11565 (minisat+_64-bit) R 11561 11561 5245 0 -1 0 45971 0 0 0 75299 297 0 0 25 0 1 0 1842207044 189591552 45958 4294967295 134512640 135094434 3221224448 3221223104 134557988 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/11565/statm): 46287 45958 145 145 0 46142 0 [pid=11565] vsize: 185148 Current children cumulated CPU time (s) 755.97 Current children cumulated vsize (Kb) 187272 [startup+770.067 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 11565 Raw data (/proc/11561/stat): 11561 (minisat+_script) S 11560 11561 5245 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1842207039 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/11561/statm): 531 226 485 147 0 384 0 [pid=11561] vsize: 2124 Raw data (/proc/11565/stat): 11565 (minisat+_64-bit) R 11561 11561 5245 0 -1 0 45971 0 0 0 76299 297 0 0 25 0 1 0 1842207044 189591552 45958 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/11565/statm): 46287 45958 145 145 0 46142 0 [pid=11565] vsize: 185148 Current children cumulated CPU time (s) 765.97 Current children cumulated vsize (Kb) 187272 [startup+780.067 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 11565 Raw data (/proc/11561/stat): 11561 (minisat+_script) S 11560 11561 5245 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1842207039 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/11561/statm): 531 226 485 147 0 384 0 [pid=11561] vsize: 2124 Raw data (/proc/11565/stat): 11565 (minisat+_64-bit) R 11561 11561 5245 0 -1 0 45971 0 0 0 77299 297 0 0 25 0 1 0 1842207044 189591552 45958 4294967295 134512640 135094434 3221224448 3221223104 134558159 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/11565/statm): 46287 45958 145 145 0 46142 0 [pid=11565] vsize: 185148 Current children cumulated CPU time (s) 775.97 Current children cumulated vsize (Kb) 187272 [startup+790.068 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 11565 Raw data (/proc/11561/stat): 11561 (minisat+_script) S 11560 11561 5245 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1842207039 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/11561/statm): 531 226 485 147 0 384 0 [pid=11561] vsize: 2124 Raw data (/proc/11565/stat): 11565 (minisat+_64-bit) R 11561 11561 5245 0 -1 0 45971 0 0 0 78299 298 0 0 25 0 1 0 1842207044 189591552 45958 4294967295 134512640 135094434 3221224448 3221223104 134557860 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/11565/statm): 46287 45958 145 145 0 46142 0 [pid=11565] vsize: 185148 Current children cumulated CPU time (s) 785.98 Current children cumulated vsize (Kb) 187272 [startup+800.069 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 11565 Raw data (/proc/11561/stat): 11561 (minisat+_script) S 11560 11561 5245 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1842207039 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/11561/statm): 531 226 485 147 0 384 0 [pid=11561] vsize: 2124 Raw data (/proc/11565/stat): 11565 (minisat+_64-bit) R 11561 11561 5245 0 -1 0 45971 0 0 0 79299 298 0 0 25 0 1 0 1842207044 189591552 45958 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/11565/statm): 46287 45958 145 145 0 46142 0 [pid=11565] vsize: 185148 Current children cumulated CPU time (s) 795.98 Current children cumulated vsize (Kb) 187272 [startup+810.07 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 11565 Raw data (/proc/11561/stat): 11561 (minisat+_script) S 11560 11561 5245 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1842207039 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/11561/statm): 531 226 485 147 0 384 0 [pid=11561] vsize: 2124 Raw data (/proc/11565/stat): 11565 (minisat+_64-bit) R 11561 11561 5245 0 -1 0 45971 0 0 0 80300 298 0 0 25 0 1 0 1842207044 189591552 45958 4294967295 134512640 135094434 3221224448 3221223104 134557988 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/11565/statm): 46287 45958 145 145 0 46142 0 [pid=11565] vsize: 185148 Current children cumulated CPU time (s) 805.99 Current children cumulated vsize (Kb) 187272 [startup+820.071 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 11565 Raw data (/proc/11561/stat): 11561 (minisat+_script) S 11560 11561 5245 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1842207039 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/11561/statm): 531 226 485 147 0 384 0 [pid=11561] vsize: 2124 Raw data (/proc/11565/stat): 11565 (minisat+_64-bit) R 11561 11561 5245 0 -1 0 45973 0 0 0 81299 299 0 0 25 0 1 0 1842207044 189591552 45960 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/11565/statm): 46287 45960 145 145 0 46142 0 [pid=11565] vsize: 185148 Current children cumulated CPU time (s) 815.99 Current children cumulated vsize (Kb) 187272 [startup+830.071 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 11565 Raw data (/proc/11561/stat): 11561 (minisat+_script) S 11560 11561 5245 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1842207039 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/11561/statm): 531 226 485 147 0 384 0 [pid=11561] vsize: 2124 Raw data (/proc/11565/stat): 11565 (minisat+_64-bit) R 11561 11561 5245 0 -1 0 45973 0 0 0 82298 300 0 0 25 0 1 0 1842207044 189591552 45960 4294967295 134512640 135094434 3221224448 3221222912 134780484 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/11565/statm): 46287 45960 145 145 0 46142 0 [pid=11565] vsize: 185148 Current children cumulated CPU time (s) 825.99 Current children cumulated vsize (Kb) 187272 [startup+840.072 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 11565 Raw data (/proc/11561/stat): 11561 (minisat+_script) S 11560 11561 5245 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1842207039 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/11561/statm): 531 226 485 147 0 384 0 [pid=11561] vsize: 2124 Raw data (/proc/11565/stat): 11565 (minisat+_64-bit) R 11561 11561 5245 0 -1 0 45973 0 0 0 83298 300 0 0 25 0 1 0 1842207044 189591552 45960 4294967295 134512640 135094434 3221224448 3221223104 134557988 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/11565/statm): 46287 45960 145 145 0 46142 0 [pid=11565] vsize: 185148 Current children cumulated CPU time (s) 835.99 Current children cumulated vsize (Kb) 187272 [startup+850.073 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 11565 Raw data (/proc/11561/stat): 11561 (minisat+_script) S 11560 11561 5245 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1842207039 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/11561/statm): 531 226 485 147 0 384 0 [pid=11561] vsize: 2124 Raw data (/proc/11565/stat): 11565 (minisat+_64-bit) R 11561 11561 5245 0 -1 0 45973 0 0 0 84298 301 0 0 25 0 1 0 1842207044 189591552 45960 4294967295 134512640 135094434 3221224448 3221223104 134558213 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/11565/statm): 46287 45960 145 145 0 46142 0 [pid=11565] vsize: 185148 Current children cumulated CPU time (s) 846 Current children cumulated vsize (Kb) 187272 [startup+860.074 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 11565 Raw data (/proc/11561/stat): 11561 (minisat+_script) S 11560 11561 5245 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1842207039 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/11561/statm): 531 226 485 147 0 384 0 [pid=11561] vsize: 2124 Raw data (/proc/11565/stat): 11565 (minisat+_64-bit) R 11561 11561 5245 0 -1 0 45973 0 0 0 85298 301 0 0 25 0 1 0 1842207044 189591552 45960 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/11565/statm): 46287 45960 145 145 0 46142 0 [pid=11565] vsize: 185148 Current children cumulated CPU time (s) 856 Current children cumulated vsize (Kb) 187272 [startup+870.078 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 11565 Raw data (/proc/11561/stat): 11561 (minisat+_script) S 11560 11561 5245 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1842207039 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/11561/statm): 531 226 485 147 0 384 0 [pid=11561] vsize: 2124 Raw data (/proc/11565/stat): 11565 (minisat+_64-bit) R 11561 11561 5245 0 -1 0 45973 0 0 0 86298 301 0 0 25 0 1 0 1842207044 189591552 45960 4294967295 134512640 135094434 3221224448 3221223104 134557988 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/11565/statm): 46287 45960 145 145 0 46142 0 [pid=11565] vsize: 185148 Current children cumulated CPU time (s) 866 Current children cumulated vsize (Kb) 187272 [startup+880.078 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 11565 Raw data (/proc/11561/stat): 11561 (minisat+_script) S 11560 11561 5245 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1842207039 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/11561/statm): 531 226 485 147 0 384 0 [pid=11561] vsize: 2124 Raw data (/proc/11565/stat): 11565 (minisat+_64-bit) R 11561 11561 5245 0 -1 0 45973 0 0 0 87298 301 0 0 25 0 1 0 1842207044 189591552 45960 4294967295 134512640 135094434 3221224448 3221223120 134556549 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/11565/statm): 46287 45960 145 145 0 46142 0 [pid=11565] vsize: 185148 Current children cumulated CPU time (s) 876 Current children cumulated vsize (Kb) 187272 [startup+890.078 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 11565 Raw data (/proc/11561/stat): 11561 (minisat+_script) S 11560 11561 5245 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1842207039 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/11561/statm): 531 226 485 147 0 384 0 [pid=11561] vsize: 2124 Raw data (/proc/11565/stat): 11565 (minisat+_64-bit) R 11561 11561 5245 0 -1 0 45973 0 0 0 88298 301 0 0 25 0 1 0 1842207044 189591552 45960 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/11565/statm): 46287 45960 145 145 0 46142 0 [pid=11565] vsize: 185148 Current children cumulated CPU time (s) 886 Current children cumulated vsize (Kb) 187272 [startup+900.08 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 11565 Raw data (/proc/11561/stat): 11561 (minisat+_script) S 11560 11561 5245 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1842207039 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/11561/statm): 531 226 485 147 0 384 0 [pid=11561] vsize: 2124 Raw data (/proc/11565/stat): 11565 (minisat+_64-bit) R 11561 11561 5245 0 -1 0 45973 0 0 0 89298 302 0 0 25 0 1 0 1842207044 189591552 45960 4294967295 134512640 135094434 3221224448 3221223104 134558019 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/11565/statm): 46287 45960 145 145 0 46142 0 [pid=11565] vsize: 185148 Current children cumulated CPU time (s) 896.01 Current children cumulated vsize (Kb) 187272 [startup+910.081 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 11565 Raw data (/proc/11561/stat): 11561 (minisat+_script) S 11560 11561 5245 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1842207039 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/11561/statm): 531 226 485 147 0 384 0 [pid=11561] vsize: 2124 Raw data (/proc/11565/stat): 11565 (minisat+_64-bit) R 11561 11561 5245 0 -1 0 45974 0 0 0 90298 302 0 0 25 0 1 0 1842207044 189591552 45961 4294967295 134512640 135094434 3221224448 3221223104 134558213 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/11565/statm): 46287 45961 145 145 0 46142 0 [pid=11565] vsize: 185148 Current children cumulated CPU time (s) 906.01 Current children cumulated vsize (Kb) 187272 [startup+920.082 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 11565 Raw data (/proc/11561/stat): 11561 (minisat+_script) S 11560 11561 5245 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1842207039 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/11561/statm): 531 226 485 147 0 384 0 [pid=11561] vsize: 2124 Raw data (/proc/11565/stat): 11565 (minisat+_64-bit) R 11561 11561 5245 0 -1 0 45974 0 0 0 91299 302 0 0 25 0 1 0 1842207044 189591552 45961 4294967295 134512640 135094434 3221224448 3221223104 134558009 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/11565/statm): 46287 45961 145 145 0 46142 0 [pid=11565] vsize: 185148 Current children cumulated CPU time (s) 916.02 Current children cumulated vsize (Kb) 187272 [startup+930.082 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 11565 Raw data (/proc/11561/stat): 11561 (minisat+_script) S 11560 11561 5245 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1842207039 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/11561/statm): 531 226 485 147 0 384 0 [pid=11561] vsize: 2124 Raw data (/proc/11565/stat): 11565 (minisat+_64-bit) R 11561 11561 5245 0 -1 0 45974 0 0 0 92298 302 0 0 25 0 1 0 1842207044 189591552 45961 4294967295 134512640 135094434 3221224448 3221223104 134558213 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/11565/statm): 46287 45961 145 145 0 46142 0 [pid=11565] vsize: 185148 Current children cumulated CPU time (s) 926.01 Current children cumulated vsize (Kb) 187272 [startup+940.083 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 11565 Raw data (/proc/11561/stat): 11561 (minisat+_script) S 11560 11561 5245 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1842207039 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/11561/statm): 531 226 485 147 0 384 0 [pid=11561] vsize: 2124 Raw data (/proc/11565/stat): 11565 (minisat+_64-bit) R 11561 11561 5245 0 -1 0 45974 0 0 0 93298 302 0 0 25 0 1 0 1842207044 189591552 45961 4294967295 134512640 135094434 3221224448 3221223104 134558159 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/11565/statm): 46287 45961 145 145 0 46142 0 [pid=11565] vsize: 185148 Current children cumulated CPU time (s) 936.01 Current children cumulated vsize (Kb) 187272 [startup+950.084 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 11565 Raw data (/proc/11561/stat): 11561 (minisat+_script) S 11560 11561 5245 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1842207039 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/11561/statm): 531 226 485 147 0 384 0 [pid=11561] vsize: 2124 Raw data (/proc/11565/stat): 11565 (minisat+_64-bit) R 11561 11561 5245 0 -1 0 45974 0 0 0 94298 302 0 0 25 0 1 0 1842207044 189591552 45961 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/11565/statm): 46287 45961 145 145 0 46142 0 [pid=11565] vsize: 185148 Current children cumulated CPU time (s) 946.01 Current children cumulated vsize (Kb) 187272 [startup+960.085 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 11565 Raw data (/proc/11561/stat): 11561 (minisat+_script) S 11560 11561 5245 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1842207039 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/11561/statm): 531 226 485 147 0 384 0 [pid=11561] vsize: 2124 Raw data (/proc/11565/stat): 11565 (minisat+_64-bit) R 11561 11561 5245 0 -1 0 45974 0 0 0 95298 302 0 0 25 0 1 0 1842207044 189591552 45961 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/11565/statm): 46287 45961 145 145 0 46142 0 [pid=11565] vsize: 185148 Current children cumulated CPU time (s) 956.01 Current children cumulated vsize (Kb) 187272 [startup+970.086 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 11565 Raw data (/proc/11561/stat): 11561 (minisat+_script) S 11560 11561 5245 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1842207039 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/11561/statm): 531 226 485 147 0 384 0 [pid=11561] vsize: 2124 Raw data (/proc/11565/stat): 11565 (minisat+_64-bit) R 11561 11561 5245 0 -1 0 45974 0 0 0 96298 302 0 0 25 0 1 0 1842207044 189591552 45961 4294967295 134512640 135094434 3221224448 3221223104 134557911 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/11565/statm): 46287 45961 145 145 0 46142 0 [pid=11565] vsize: 185148 Current children cumulated CPU time (s) 966.01 Current children cumulated vsize (Kb) 187272 [startup+980.086 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 11565 Raw data (/proc/11561/stat): 11561 (minisat+_script) S 11560 11561 5245 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1842207039 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/11561/statm): 531 226 485 147 0 384 0 [pid=11561] vsize: 2124 Raw data (/proc/11565/stat): 11565 (minisat+_64-bit) R 11561 11561 5245 0 -1 0 45974 0 0 0 97298 302 0 0 25 0 1 0 1842207044 189591552 45961 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/11565/statm): 46287 45961 145 145 0 46142 0 [pid=11565] vsize: 185148 Current children cumulated CPU time (s) 976.01 Current children cumulated vsize (Kb) 187272 [startup+990.087 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 11565 Raw data (/proc/11561/stat): 11561 (minisat+_script) S 11560 11561 5245 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1842207039 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/11561/statm): 531 226 485 147 0 384 0 [pid=11561] vsize: 2124 Raw data (/proc/11565/stat): 11565 (minisat+_64-bit) R 11561 11561 5245 0 -1 0 45974 0 0 0 98299 302 0 0 25 0 1 0 1842207044 189591552 45961 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/11565/statm): 46287 45961 145 145 0 46142 0 [pid=11565] vsize: 185148 Current children cumulated CPU time (s) 986.02 Current children cumulated vsize (Kb) 187272 [startup+1000.09 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 11565 Raw data (/proc/11561/stat): 11561 (minisat+_script) S 11560 11561 5245 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1842207039 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/11561/statm): 531 226 485 147 0 384 0 [pid=11561] vsize: 2124 Raw data (/proc/11565/stat): 11565 (minisat+_64-bit) R 11561 11561 5245 0 -1 0 45974 0 0 0 99299 303 0 0 25 0 1 0 1842207044 189591552 45961 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/11565/statm): 46287 45961 145 145 0 46142 0 [pid=11565] vsize: 185148 Current children cumulated CPU time (s) 996.03 Current children cumulated vsize (Kb) 187272 [startup+1010.09 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 11565 Raw data (/proc/11561/stat): 11561 (minisat+_script) S 11560 11561 5245 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1842207039 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/11561/statm): 531 226 485 147 0 384 0 [pid=11561] vsize: 2124 Raw data (/proc/11565/stat): 11565 (minisat+_64-bit) R 11561 11561 5245 0 -1 0 45974 0 0 0 100299 303 0 0 25 0 1 0 1842207044 189591552 45961 4294967295 134512640 135094434 3221224448 3221223104 134558159 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/11565/statm): 46287 45961 145 145 0 46142 0 [pid=11565] vsize: 185148 Current children cumulated CPU time (s) 1006.03 Current children cumulated vsize (Kb) 187272 [startup+1020.09 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 11565 Raw data (/proc/11561/stat): 11561 (minisat+_script) S 11560 11561 5245 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1842207039 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/11561/statm): 531 226 485 147 0 384 0 [pid=11561] vsize: 2124 Raw data (/proc/11565/stat): 11565 (minisat+_64-bit) R 11561 11561 5245 0 -1 0 45974 0 0 0 101299 303 0 0 25 0 1 0 1842207044 189591552 45961 4294967295 134512640 135094434 3221224448 3221223104 134558213 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/11565/statm): 46287 45961 145 145 0 46142 0 [pid=11565] vsize: 185148 Current children cumulated CPU time (s) 1016.03 Current children cumulated vsize (Kb) 187272 [startup+1030.09 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 11565 Raw data (/proc/11561/stat): 11561 (minisat+_script) S 11560 11561 5245 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1842207039 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/11561/statm): 531 226 485 147 0 384 0 [pid=11561] vsize: 2124 Raw data (/proc/11565/stat): 11565 (minisat+_64-bit) R 11561 11561 5245 0 -1 0 45974 0 0 0 102299 303 0 0 25 0 1 0 1842207044 189591552 45961 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/11565/statm): 46287 45961 145 145 0 46142 0 [pid=11565] vsize: 185148 Current children cumulated CPU time (s) 1026.03 Current children cumulated vsize (Kb) 187272 [startup+1040.09 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 11565 Raw data (/proc/11561/stat): 11561 (minisat+_script) S 11560 11561 5245 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1842207039 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/11561/statm): 531 226 485 147 0 384 0 [pid=11561] vsize: 2124 Raw data (/proc/11565/stat): 11565 (minisat+_64-bit) R 11561 11561 5245 0 -1 0 45974 0 0 0 103300 303 0 0 25 0 1 0 1842207044 189591552 45961 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/11565/statm): 46287 45961 145 145 0 46142 0 [pid=11565] vsize: 185148 Current children cumulated CPU time (s) 1036.04 Current children cumulated vsize (Kb) 187272 [startup+1050.09 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 11565 Raw data (/proc/11561/stat): 11561 (minisat+_script) S 11560 11561 5245 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1842207039 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/11561/statm): 531 226 485 147 0 384 0 [pid=11561] vsize: 2124 Raw data (/proc/11565/stat): 11565 (minisat+_64-bit) R 11561 11561 5245 0 -1 0 45974 0 0 0 104299 303 0 0 25 0 1 0 1842207044 189591552 45961 4294967295 134512640 135094434 3221224448 3221223104 134558213 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/11565/statm): 46287 45961 145 145 0 46142 0 [pid=11565] vsize: 185148 Current children cumulated CPU time (s) 1046.03 Current children cumulated vsize (Kb) 187272 [startup+1060.09 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 11565 Raw data (/proc/11561/stat): 11561 (minisat+_script) S 11560 11561 5245 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1842207039 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/11561/statm): 531 226 485 147 0 384 0 [pid=11561] vsize: 2124 Raw data (/proc/11565/stat): 11565 (minisat+_64-bit) R 11561 11561 5245 0 -1 0 45974 0 0 0 105300 303 0 0 25 0 1 0 1842207044 189591552 45961 4294967295 134512640 135094434 3221224448 3221223072 134557621 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/11565/statm): 46287 45961 145 145 0 46142 0 [pid=11565] vsize: 185148 Current children cumulated CPU time (s) 1056.04 Current children cumulated vsize (Kb) 187272 [startup+1070.09 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 11565 Raw data (/proc/11561/stat): 11561 (minisat+_script) S 11560 11561 5245 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1842207039 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/11561/statm): 531 226 485 147 0 384 0 [pid=11561] vsize: 2124 Raw data (/proc/11565/stat): 11565 (minisat+_64-bit) R 11561 11561 5245 0 -1 0 45974 0 0 0 106300 303 0 0 25 0 1 0 1842207044 189591552 45961 4294967295 134512640 135094434 3221224448 3221223104 134557866 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/11565/statm): 46287 45961 145 145 0 46142 0 [pid=11565] vsize: 185148 Current children cumulated CPU time (s) 1066.04 Current children cumulated vsize (Kb) 187272 [startup+1080.1 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 11565 Raw data (/proc/11561/stat): 11561 (minisat+_script) S 11560 11561 5245 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1842207039 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/11561/statm): 531 226 485 147 0 384 0 [pid=11561] vsize: 2124 Raw data (/proc/11565/stat): 11565 (minisat+_64-bit) R 11561 11561 5245 0 -1 0 45974 0 0 0 107300 303 0 0 25 0 1 0 1842207044 189591552 45961 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/11565/statm): 46287 45961 145 145 0 46142 0 [pid=11565] vsize: 185148 Current children cumulated CPU time (s) 1076.04 Current children cumulated vsize (Kb) 187272 [startup+1090.1 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 11565 Raw data (/proc/11561/stat): 11561 (minisat+_script) S 11560 11561 5245 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1842207039 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/11561/statm): 531 226 485 147 0 384 0 [pid=11561] vsize: 2124 Raw data (/proc/11565/stat): 11565 (minisat+_64-bit) R 11561 11561 5245 0 -1 0 45974 0 0 0 108300 303 0 0 25 0 1 0 1842207044 189591552 45961 4294967295 134512640 135094434 3221224448 3221223104 134558208 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/11565/statm): 46287 45961 145 145 0 46142 0 [pid=11565] vsize: 185148 Current children cumulated CPU time (s) 1086.04 Current children cumulated vsize (Kb) 187272 [startup+1100.1 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 11565 Raw data (/proc/11561/stat): 11561 (minisat+_script) S 11560 11561 5245 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1842207039 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/11561/statm): 531 226 485 147 0 384 0 [pid=11561] vsize: 2124 Raw data (/proc/11565/stat): 11565 (minisat+_64-bit) R 11561 11561 5245 0 -1 0 45974 0 0 0 109300 304 0 0 25 0 1 0 1842207044 189591552 45961 4294967295 134512640 135094434 3221224448 3221223104 134557900 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/11565/statm): 46287 45961 145 145 0 46142 0 [pid=11565] vsize: 185148 Current children cumulated CPU time (s) 1096.05 Current children cumulated vsize (Kb) 187272 [startup+1110.1 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 11565 Raw data (/proc/11561/stat): 11561 (minisat+_script) S 11560 11561 5245 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1842207039 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/11561/statm): 531 226 485 147 0 384 0 [pid=11561] vsize: 2124 Raw data (/proc/11565/stat): 11565 (minisat+_64-bit) R 11561 11561 5245 0 -1 0 45974 0 0 0 110300 304 0 0 25 0 1 0 1842207044 189591552 45961 4294967295 134512640 135094434 3221224448 3221223104 134557860 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/11565/statm): 46287 45961 145 145 0 46142 0 [pid=11565] vsize: 185148 Current children cumulated CPU time (s) 1106.05 Current children cumulated vsize (Kb) 187272 [startup+1120.1 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 11565 Raw data (/proc/11561/stat): 11561 (minisat+_script) S 11560 11561 5245 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1842207039 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/11561/statm): 531 226 485 147 0 384 0 [pid=11561] vsize: 2124 Raw data (/proc/11565/stat): 11565 (minisat+_64-bit) R 11561 11561 5245 0 -1 0 45974 0 0 0 111301 304 0 0 25 0 1 0 1842207044 189591552 45961 4294967295 134512640 135094434 3221224448 3221223120 134555574 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/11565/statm): 46287 45961 145 145 0 46142 0 [pid=11565] vsize: 185148 Current children cumulated CPU time (s) 1116.06 Current children cumulated vsize (Kb) 187272 [startup+1130.1 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 11565 Raw data (/proc/11561/stat): 11561 (minisat+_script) S 11560 11561 5245 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1842207039 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/11561/statm): 531 226 485 147 0 384 0 [pid=11561] vsize: 2124 Raw data (/proc/11565/stat): 11565 (minisat+_64-bit) R 11561 11561 5245 0 -1 0 45974 0 0 0 112301 304 0 0 25 0 1 0 1842207044 189591552 45961 4294967295 134512640 135094434 3221224448 3221223104 134557988 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/11565/statm): 46287 45961 145 145 0 46142 0 [pid=11565] vsize: 185148 Current children cumulated CPU time (s) 1126.06 Current children cumulated vsize (Kb) 187272 [startup+1140.1 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 11565 Raw data (/proc/11561/stat): 11561 (minisat+_script) S 11560 11561 5245 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1842207039 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/11561/statm): 531 226 485 147 0 384 0 [pid=11561] vsize: 2124 Raw data (/proc/11565/stat): 11565 (minisat+_64-bit) R 11561 11561 5245 0 -1 0 45974 0 0 0 113301 304 0 0 25 0 1 0 1842207044 189591552 45961 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/11565/statm): 46287 45961 145 145 0 46142 0 [pid=11565] vsize: 185148 Current children cumulated CPU time (s) 1136.06 Current children cumulated vsize (Kb) 187272 [startup+1150.1 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 11565 Raw data (/proc/11561/stat): 11561 (minisat+_script) S 11560 11561 5245 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1842207039 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/11561/statm): 531 226 485 147 0 384 0 [pid=11561] vsize: 2124 Raw data (/proc/11565/stat): 11565 (minisat+_64-bit) R 11561 11561 5245 0 -1 0 45974 0 0 0 114301 304 0 0 25 0 1 0 1842207044 189591552 45961 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/11565/statm): 46287 45961 145 145 0 46142 0 [pid=11565] vsize: 185148 Current children cumulated CPU time (s) 1146.06 Current children cumulated vsize (Kb) 187272 [startup+1160.1 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 11565 Raw data (/proc/11561/stat): 11561 (minisat+_script) S 11560 11561 5245 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1842207039 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/11561/statm): 531 226 485 147 0 384 0 [pid=11561] vsize: 2124 Raw data (/proc/11565/stat): 11565 (minisat+_64-bit) R 11561 11561 5245 0 -1 0 45974 0 0 0 115301 304 0 0 25 0 1 0 1842207044 189591552 45961 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/11565/statm): 46287 45961 145 145 0 46142 0 [pid=11565] vsize: 185148 Current children cumulated CPU time (s) 1156.06 Current children cumulated vsize (Kb) 187272 [startup+1170.1 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 11565 Raw data (/proc/11561/stat): 11561 (minisat+_script) S 11560 11561 5245 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1842207039 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/11561/statm): 531 226 485 147 0 384 0 [pid=11561] vsize: 2124 Raw data (/proc/11565/stat): 11565 (minisat+_64-bit) R 11561 11561 5245 0 -1 0 45974 0 0 0 116302 304 0 0 25 0 1 0 1842207044 189591552 45961 4294967295 134512640 135094434 3221224448 3221223104 134558178 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/11565/statm): 46287 45961 145 145 0 46142 0 [pid=11565] vsize: 185148 Current children cumulated CPU time (s) 1166.07 Current children cumulated vsize (Kb) 187272 [startup+1180.1 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 11565 Raw data (/proc/11561/stat): 11561 (minisat+_script) S 11560 11561 5245 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1842207039 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/11561/statm): 531 226 485 147 0 384 0 [pid=11561] vsize: 2124 Raw data (/proc/11565/stat): 11565 (minisat+_64-bit) R 11561 11561 5245 0 -1 0 45974 0 0 0 117302 304 0 0 25 0 1 0 1842207044 189591552 45961 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/11565/statm): 46287 45961 145 145 0 46142 0 [pid=11565] vsize: 185148 Current children cumulated CPU time (s) 1176.07 Current children cumulated vsize (Kb) 187272 [startup+1190.1 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 11565 Raw data (/proc/11561/stat): 11561 (minisat+_script) S 11560 11561 5245 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1842207039 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/11561/statm): 531 226 485 147 0 384 0 [pid=11561] vsize: 2124 Raw data (/proc/11565/stat): 11565 (minisat+_64-bit) R 11561 11561 5245 0 -1 0 45974 0 0 0 118302 304 0 0 25 0 1 0 1842207044 189591552 45961 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/11565/statm): 46287 45961 145 145 0 46142 0 [pid=11565] vsize: 185148 Current children cumulated CPU time (s) 1186.07 Current children cumulated vsize (Kb) 187272 [startup+1200.1 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 11565 Raw data (/proc/11561/stat): 11561 (minisat+_script) S 11560 11561 5245 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1842207039 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/11561/statm): 531 226 485 147 0 384 0 [pid=11561] vsize: 2124 Raw data (/proc/11565/stat): 11565 (minisat+_64-bit) R 11561 11561 5245 0 -1 0 45974 0 0 0 119302 304 0 0 25 0 1 0 1842207044 189591552 45961 4294967295 134512640 135094434 3221224448 3221223104 134558213 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/11565/statm): 46287 45961 145 145 0 46142 0 [pid=11565] vsize: 185148 Current children cumulated CPU time (s) 1196.07 Current children cumulated vsize (Kb) 187272 [startup+1210.11 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 11565 Raw data (/proc/11561/stat): 11561 (minisat+_script) S 11560 11561 5245 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1842207039 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/11561/statm): 531 226 485 147 0 384 0 [pid=11561] vsize: 2124 Raw data (/proc/11565/stat): 11565 (minisat+_64-bit) R 11561 11561 5245 0 -1 0 45974 0 0 0 120303 304 0 0 25 0 1 0 1842207044 189591552 45961 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/11565/statm): 46287 45961 145 145 0 46142 0 [pid=11565] vsize: 185148 Current children cumulated CPU time (s) 1206.08 Current children cumulated vsize (Kb) 187272 Maximum CPU time exceeded: sending SIGTERM then SIGKILL [startup+1210.11 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 11565 Raw data (/proc/11561/stat): 11561 (minisat+_script) S 11560 11561 5245 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1842207039 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/11561/statm): 531 226 485 147 0 384 0 [pid=11561] vsize: 2124 Raw data (/proc/11565/stat): 11565 (minisat+_64-bit) R 11561 11561 5245 0 -1 0 45974 0 0 0 120303 304 0 0 25 0 1 0 1842207044 189591552 45961 4294967295 134512640 135094434 3221224448 3221223136 134554733 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/11565/statm): 46287 45961 145 145 0 46142 0 [pid=11565] vsize: 185148 Current children cumulated CPU time (s) 1206.08 Current children cumulated vsize (Kb) 187272 Sending SIGTERM to -11561 Sleeping 2 seconds One traced child (pid=11561) ended because it received signal 15 (SIGTERM) One traced child (pid=11565) exited with status: 0 All traced children have exited ! Game is over. Child status: 0 Real time (s): 1210.19 CPU time (s): 1206.16 CPU user time (s): 1203.03 CPU system time (s): 3.12652 CPU usage (%): 99.6666 Max. virtual memory (cumulated for all children) (Kb): 187272
ERROR: no interpretation found !