Name | submitted/manquinho/primes-dimacs-cnf/normalized-g125.17.opb |
MD5SUM | ed503628984a48598e5d5a4b8388e97a |
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 | 4250 |
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 | 4250 |
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 | 4250 |
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 | 4250 |
Total number of constraints | 68397 |
Number of constraints which are clauses | 68397 |
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 | 17 |
LAUNCH ON wulflinc8 THE 2005-09-18 15:08:59 (client local time) PB2005-SCRIPT v4.0 MARKUPS: idlaunch=2469 boxname=wulflinc8 idbench=125 idsolver=3 numberseed=0 MD5SUM SOLVER: MD5SUM BENCH: ed503628984a48598e5d5a4b8388e97a /oldhome/oroussel/tmp/wulflinc8/normalized-g125.17.opb REAL COMMAND: minisat+_script /oldhome/oroussel/tmp/wulflinc8/normalized-g125.17.opb IDLAUNCH: 2469 /proc/cpuinfo: processor : 0 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 2 cpu MHz : 451.007 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 : 2 cpu MHz : 451.007 cache size : 512 KB fdiv_bug : no hlt_bug : no f00f_bug : no coma_bug : no fpu : yes fpu_exception : yes cpuid level : 2 wp : yes flags : fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse bogomips : 899.07 /proc/meminfo: MemTotal: 1034660 kB MemFree: 920356 kB Buffers: 34196 kB Cached: 54908 kB SwapCached: 792 kB Active: 65036 kB Inactive: 26756 kB HighTotal: 131008 kB HighFree: 72296 kB LowTotal: 903652 kB LowFree: 848060 kB SwapTotal: 2097136 kB SwapFree: 2095876 kB Dirty: 28 kB Writeback: 0 kB Mapped: 5752 kB Slab: 16912 kB Committed_AS: 64168 kB PageTables: 328 kB VmallocTotal: 114680 kB VmallocUsed: 1364 kB VmallocChunk: 113256 kB JOB ENDED THE 2005-09-18 15:29:09 (client local time) WITH STATUS 0 IN 1206.37 SECONDS stats: 2469 7 1206.37 0
c Parsing PB file... c Converting 68397 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 | 68397 138669 | 22799 0 0 nan | 0.000 % | c | 100 | 68397 138669 | 25078 100 5288 52.9 | 0.000 % | c | 250 | 68397 138669 | 27586 250 27345 109.4 | 0.000 % | c | 476 | 68397 138669 | 30345 476 55808 117.2 | 0.000 % | c | 813 | 68397 138669 | 33380 813 105508 129.8 | 0.000 % | c | 1319 | 68397 138669 | 36718 1319 238948 181.2 | 0.000 % | c | 2080 | 68397 138669 | 40389 2080 408552 196.4 | 0.000 % | c | 3220 | 68397 138669 | 44428 3220 720088 223.6 | 0.000 % | c | 4930 | 68397 138669 | 48871 4930 1260193 255.6 | 0.000 % | c | 7492 | 68397 138669 | 53758 7492 2077236 277.3 | 0.000 % | c | 11336 | 68397 138669 | 59134 11336 3292984 290.5 | 0.000 % | c | 17103 | 68397 138669 | 65048 17103 5370978 314.0 | 0.000 % | c | 25752 | 68397 138669 | 71553 25752 8706513 338.1 | 0.000 % | c | 38727 | 68397 138669 | 78708 38727 13018646 336.2 | 0.000 % | c | 58190 | 68397 138669 | 86579 58190 20743435 356.5 | 0.000 % | c | 87385 | 68397 138669 | 95237 87385 30964013 354.3 | 0.000 % | c | 131175 | 68397 138669 | 104760 47058 17880606 380.0 | 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/950/stat): 950 (minisat+_script) R 949 950 27660 0 -1 0 19 0 0 0 0 0 0 0 21 0 1 0 1770426787 712704 3 4294967295 134512640 135087896 3221224512 3221224512 1073744960 0 0 5 0 0 0 0 17 1 0 0 Raw data (/proc/950/statm): 174 3 169 147 0 27 0 [pid=950] 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=951 New process pid=952 New process pid=953 execve syscall for /bin/sed executable One traced child (pid=952) 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=953) exited with status: 0 One traced child (pid=951) exited with status: 0 New process pid=954 execve syscall for /oldhome/oroussel/solvers/minisat+_64-bit_static executable open syscall for file /dev/null open syscall for file /oldhome/oroussel/tmp/wulflinc8/normalized-g125.17.opb [startup+10.0032 s] Raw data (loadavg): 0.52 0.72 0.88 2/57 954 Raw data (/proc/950/stat): 950 (minisat+_script) S 949 950 27660 0 -1 0 288 239 0 0 0 1 0 0 20 0 1 0 1770426787 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/950/statm): 531 226 485 147 0 384 0 [pid=950] vsize: 2124 Raw data (/proc/954/stat): 954 (minisat+_64-bit) R 950 950 27660 0 -1 0 4474 0 0 0 963 20 0 0 25 0 1 0 1770426792 19288064 4461 4294967295 134512640 135094434 3221224448 3221223104 134558232 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/954/statm): 4709 4461 145 145 0 4564 0 [pid=954] vsize: 18836 Current children cumulated CPU time (s) 9.84 Current children cumulated vsize (Kb) 20960 [startup+20.005 s] Raw data (loadavg): 0.60 0.73 0.88 2/57 954 Raw data (/proc/950/stat): 950 (minisat+_script) S 949 950 27660 0 -1 0 288 239 0 0 0 1 0 0 20 0 1 0 1770426787 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/950/statm): 531 226 485 147 0 384 0 [pid=950] vsize: 2124 Raw data (/proc/954/stat): 954 (minisat+_64-bit) R 950 950 27660 0 -1 0 4730 0 0 0 1958 22 0 0 25 0 1 0 1770426792 20312064 4717 4294967295 134512640 135094434 3221224448 3221223104 134558208 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/954/statm): 4959 4717 145 145 0 4814 0 [pid=954] vsize: 19836 Current children cumulated CPU time (s) 19.81 Current children cumulated vsize (Kb) 21960 [startup+30.0068 s] Raw data (loadavg): 0.66 0.74 0.88 2/57 954 Raw data (/proc/950/stat): 950 (minisat+_script) S 949 950 27660 0 -1 0 288 239 0 0 0 1 0 0 20 0 1 0 1770426787 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/950/statm): 531 226 485 147 0 384 0 [pid=950] vsize: 2124 Raw data (/proc/954/stat): 954 (minisat+_64-bit) R 950 950 27660 0 -1 0 6247 0 0 0 2936 30 0 0 25 0 1 0 1770426792 26525696 6234 4294967295 134512640 135094434 3221224448 3221223104 134558213 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/954/statm): 6476 6234 145 145 0 6331 0 [pid=954] vsize: 25904 Current children cumulated CPU time (s) 29.67 Current children cumulated vsize (Kb) 28028 [startup+40.0076 s] Raw data (loadavg): 0.71 0.75 0.88 2/57 954 Raw data (/proc/950/stat): 950 (minisat+_script) S 949 950 27660 0 -1 0 288 239 0 0 0 1 0 0 20 0 1 0 1770426787 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/950/statm): 531 226 485 147 0 384 0 [pid=950] vsize: 2124 Raw data (/proc/954/stat): 954 (minisat+_64-bit) R 950 950 27660 0 -1 0 7569 0 0 0 3915 37 0 0 25 0 1 0 1770426792 31993856 7556 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/954/statm): 7811 7556 145 145 0 7666 0 [pid=954] vsize: 31244 Current children cumulated CPU time (s) 39.53 Current children cumulated vsize (Kb) 33368 [startup+50.0094 s] Raw data (loadavg): 0.75 0.75 0.89 2/57 954 Raw data (/proc/950/stat): 950 (minisat+_script) S 949 950 27660 0 -1 0 288 239 0 0 0 1 0 0 20 0 1 0 1770426787 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/950/statm): 531 226 485 147 0 384 0 [pid=950] vsize: 2124 Raw data (/proc/954/stat): 954 (minisat+_64-bit) R 950 950 27660 0 -1 0 8826 0 0 0 4895 47 0 0 25 0 1 0 1770426792 37126144 8813 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/954/statm): 9064 8813 145 145 0 8919 0 [pid=954] vsize: 36256 Current children cumulated CPU time (s) 49.43 Current children cumulated vsize (Kb) 38380 [startup+60.0101 s] Raw data (loadavg): 0.79 0.76 0.89 2/57 954 Raw data (/proc/950/stat): 950 (minisat+_script) S 949 950 27660 0 -1 0 288 239 0 0 0 1 0 0 20 0 1 0 1770426787 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/950/statm): 531 226 485 147 0 384 0 [pid=950] vsize: 2124 Raw data (/proc/954/stat): 954 (minisat+_64-bit) R 950 950 27660 0 -1 0 9809 0 0 0 5878 54 0 0 25 0 1 0 1770426792 41144320 9796 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/954/statm): 10045 9796 145 145 0 9900 0 [pid=954] vsize: 40180 Current children cumulated CPU time (s) 59.33 Current children cumulated vsize (Kb) 42304 [startup+70.0119 s] Raw data (loadavg): 0.82 0.77 0.89 2/57 954 Raw data (/proc/950/stat): 950 (minisat+_script) S 949 950 27660 0 -1 0 288 239 0 0 0 1 0 0 20 0 1 0 1770426787 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/950/statm): 531 226 485 147 0 384 0 [pid=950] vsize: 2124 Raw data (/proc/954/stat): 954 (minisat+_64-bit) R 950 950 27660 0 -1 0 10565 0 0 0 6865 60 0 0 25 0 1 0 1770426792 44232704 10552 4294967295 134512640 135094434 3221224448 3221223136 134554726 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/954/statm): 10799 10552 145 145 0 10654 0 [pid=954] vsize: 43196 Current children cumulated CPU time (s) 69.26 Current children cumulated vsize (Kb) 45320 [startup+80.0127 s] Raw data (loadavg): 0.85 0.78 0.89 2/57 954 Raw data (/proc/950/stat): 950 (minisat+_script) S 949 950 27660 0 -1 0 288 239 0 0 0 1 0 0 20 0 1 0 1770426787 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/950/statm): 531 226 485 147 0 384 0 [pid=950] vsize: 2124 Raw data (/proc/954/stat): 954 (minisat+_64-bit) R 950 950 27660 0 -1 0 11188 0 0 0 7854 64 0 0 25 0 1 0 1770426792 46776320 11175 4294967295 134512640 135094434 3221224448 3221223104 134558395 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/954/statm): 11420 11175 145 145 0 11275 0 [pid=954] vsize: 45680 Current children cumulated CPU time (s) 79.19 Current children cumulated vsize (Kb) 47804 [startup+90.0145 s] Raw data (loadavg): 0.87 0.78 0.89 2/57 954 Raw data (/proc/950/stat): 950 (minisat+_script) S 949 950 27660 0 -1 0 288 239 0 0 0 1 0 0 20 0 1 0 1770426787 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/950/statm): 531 226 485 147 0 384 0 [pid=950] vsize: 2124 Raw data (/proc/954/stat): 954 (minisat+_64-bit) R 950 950 27660 0 -1 0 11806 0 0 0 8842 69 0 0 25 0 1 0 1770426792 49303552 11793 4294967295 134512640 135094434 3221224448 3221223104 134558019 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/954/statm): 12037 11793 145 145 0 11892 0 [pid=954] vsize: 48148 Current children cumulated CPU time (s) 89.12 Current children cumulated vsize (Kb) 50272 [startup+100.015 s] Raw data (loadavg): 0.89 0.79 0.89 2/57 954 Raw data (/proc/950/stat): 950 (minisat+_script) S 949 950 27660 0 -1 0 288 239 0 0 0 1 0 0 20 0 1 0 1770426787 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/950/statm): 531 226 485 147 0 384 0 [pid=950] vsize: 2124 Raw data (/proc/954/stat): 954 (minisat+_64-bit) R 950 950 27660 0 -1 0 12439 0 0 0 9831 74 0 0 25 0 1 0 1770426792 51888128 12426 4294967295 134512640 135094434 3221224448 3221223104 134558249 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/954/statm): 12668 12426 145 145 0 12523 0 [pid=954] vsize: 50672 Current children cumulated CPU time (s) 99.06 Current children cumulated vsize (Kb) 52796 [startup+110.016 s] Raw data (loadavg): 0.91 0.80 0.89 2/57 954 Raw data (/proc/950/stat): 950 (minisat+_script) S 949 950 27660 0 -1 0 288 239 0 0 0 1 0 0 20 0 1 0 1770426787 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/950/statm): 531 226 485 147 0 384 0 [pid=950] vsize: 2124 Raw data (/proc/954/stat): 954 (minisat+_64-bit) R 950 950 27660 0 -1 0 13132 0 0 0 10818 80 0 0 25 0 1 0 1770426792 54857728 13119 4294967295 134512640 135094434 3221224448 3221223104 134558123 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/954/statm): 13393 13119 145 145 0 13248 0 [pid=954] vsize: 53572 Current children cumulated CPU time (s) 108.99 Current children cumulated vsize (Kb) 55696 [startup+120.018 s] Raw data (loadavg): 0.92 0.80 0.89 2/57 954 Raw data (/proc/950/stat): 950 (minisat+_script) S 949 950 27660 0 -1 0 288 239 0 0 0 1 0 0 20 0 1 0 1770426787 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/950/statm): 531 226 485 147 0 384 0 [pid=950] vsize: 2124 Raw data (/proc/954/stat): 954 (minisat+_64-bit) R 950 950 27660 0 -1 0 13711 0 0 0 11806 84 0 0 25 0 1 0 1770426792 57221120 13698 4294967295 134512640 135094434 3221224448 3221223104 134558210 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/954/statm): 13970 13698 145 145 0 13825 0 [pid=954] vsize: 55880 Current children cumulated CPU time (s) 118.91 Current children cumulated vsize (Kb) 58004 [startup+130.019 s] Raw data (loadavg): 0.93 0.81 0.89 2/57 954 Raw data (/proc/950/stat): 950 (minisat+_script) S 949 950 27660 0 -1 0 288 239 0 0 0 1 0 0 20 0 1 0 1770426787 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/950/statm): 531 226 485 147 0 384 0 [pid=950] vsize: 2124 Raw data (/proc/954/stat): 954 (minisat+_64-bit) R 950 950 27660 0 -1 0 14299 0 0 0 12794 88 0 0 25 0 1 0 1770426792 59625472 14286 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/954/statm): 14557 14286 145 145 0 14412 0 [pid=954] vsize: 58228 Current children cumulated CPU time (s) 128.83 Current children cumulated vsize (Kb) 60352 [startup+140.02 s] Raw data (loadavg): 0.94 0.81 0.89 2/57 954 Raw data (/proc/950/stat): 950 (minisat+_script) S 949 950 27660 0 -1 0 288 239 0 0 0 1 0 0 20 0 1 0 1770426787 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/950/statm): 531 226 485 147 0 384 0 [pid=950] vsize: 2124 Raw data (/proc/954/stat): 954 (minisat+_64-bit) R 950 950 27660 0 -1 0 14859 0 0 0 13784 92 0 0 25 0 1 0 1770426792 61915136 14846 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/954/statm): 15116 14846 145 145 0 14971 0 [pid=954] vsize: 60464 Current children cumulated CPU time (s) 138.77 Current children cumulated vsize (Kb) 62588 [startup+150.022 s] Raw data (loadavg): 0.95 0.82 0.90 2/57 954 Raw data (/proc/950/stat): 950 (minisat+_script) S 949 950 27660 0 -1 0 288 239 0 0 0 1 0 0 20 0 1 0 1770426787 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/950/statm): 531 226 485 147 0 384 0 [pid=950] vsize: 2124 Raw data (/proc/954/stat): 954 (minisat+_64-bit) R 950 950 27660 0 -1 0 15715 0 0 0 14771 98 0 0 25 0 1 0 1770426792 65413120 15702 4294967295 134512640 135094434 3221224448 3221223104 134558178 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/954/statm): 15970 15702 145 145 0 15825 0 [pid=954] vsize: 63880 Current children cumulated CPU time (s) 148.7 Current children cumulated vsize (Kb) 66004 [startup+160.023 s] Raw data (loadavg): 0.96 0.83 0.90 2/57 954 Raw data (/proc/950/stat): 950 (minisat+_script) S 949 950 27660 0 -1 0 288 239 0 0 0 1 0 0 20 0 1 0 1770426787 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/950/statm): 531 226 485 147 0 384 0 [pid=950] vsize: 2124 Raw data (/proc/954/stat): 954 (minisat+_64-bit) R 950 950 27660 0 -1 0 16457 0 0 0 15758 104 0 0 25 0 1 0 1770426792 68444160 16444 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/954/statm): 16710 16444 145 145 0 16565 0 [pid=954] vsize: 66840 Current children cumulated CPU time (s) 158.63 Current children cumulated vsize (Kb) 68964 [startup+170.025 s] Raw data (loadavg): 0.96 0.83 0.90 2/57 954 Raw data (/proc/950/stat): 950 (minisat+_script) S 949 950 27660 0 -1 0 288 239 0 0 0 1 0 0 20 0 1 0 1770426787 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/950/statm): 531 226 485 147 0 384 0 [pid=950] vsize: 2124 Raw data (/proc/954/stat): 954 (minisat+_64-bit) R 950 950 27660 0 -1 0 17117 0 0 0 16745 109 0 0 25 0 1 0 1770426792 71143424 17104 4294967295 134512640 135094434 3221224448 3221223104 134558213 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/954/statm): 17369 17104 145 145 0 17224 0 [pid=954] vsize: 69476 Current children cumulated CPU time (s) 168.55 Current children cumulated vsize (Kb) 71600 [startup+180.026 s] Raw data (loadavg): 0.97 0.84 0.90 2/57 954 Raw data (/proc/950/stat): 950 (minisat+_script) S 949 950 27660 0 -1 0 288 239 0 0 0 1 0 0 20 0 1 0 1770426787 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/950/statm): 531 226 485 147 0 384 0 [pid=950] vsize: 2124 Raw data (/proc/954/stat): 954 (minisat+_64-bit) R 950 950 27660 0 -1 0 17844 0 0 0 17733 114 0 0 25 0 1 0 1770426792 74113024 17831 4294967295 134512640 135094434 3221224448 3221223104 134558159 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/954/statm): 18094 17831 145 145 0 17949 0 [pid=954] vsize: 72376 Current children cumulated CPU time (s) 178.48 Current children cumulated vsize (Kb) 74500 [startup+190.027 s] Raw data (loadavg): 0.97 0.84 0.90 2/57 954 Raw data (/proc/950/stat): 950 (minisat+_script) S 949 950 27660 0 -1 0 288 239 0 0 0 1 0 0 20 0 1 0 1770426787 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/950/statm): 531 226 485 147 0 384 0 [pid=950] vsize: 2124 Raw data (/proc/954/stat): 954 (minisat+_64-bit) R 950 950 27660 0 -1 0 18608 0 0 0 18718 120 0 0 25 0 1 0 1770426792 77238272 18595 4294967295 134512640 135094434 3221224448 3221223104 134558009 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/954/statm): 18857 18595 145 145 0 18712 0 [pid=954] vsize: 75428 Current children cumulated CPU time (s) 188.39 Current children cumulated vsize (Kb) 77552 [startup+200.028 s] Raw data (loadavg): 0.98 0.85 0.90 1/57 954 Raw data (/proc/950/stat): 950 (minisat+_script) S 949 950 27660 0 -1 0 288 239 0 0 0 1 0 0 20 0 1 0 1770426787 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/950/statm): 531 226 485 147 0 384 0 [pid=950] vsize: 2124 Raw data (/proc/954/stat): 954 (minisat+_64-bit) T 950 950 27660 0 -1 0 19271 0 0 0 19707 124 0 0 25 0 1 0 1770426792 79953920 19258 4294967295 134512640 135094434 3221224448 3221222828 134870330 0 0 5 16386 3222434794 0 0 17 1 0 0 Raw data (/proc/954/statm): 19520 19258 145 145 0 19375 0 [pid=954] vsize: 78080 Current children cumulated CPU time (s) 198.32 Current children cumulated vsize (Kb) 80204 [startup+210.029 s] Raw data (loadavg): 0.98 0.85 0.90 2/57 954 Raw data (/proc/950/stat): 950 (minisat+_script) S 949 950 27660 0 -1 0 288 239 0 0 0 1 0 0 20 0 1 0 1770426787 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/950/statm): 531 226 485 147 0 384 0 [pid=950] vsize: 2124 Raw data (/proc/954/stat): 954 (minisat+_64-bit) R 950 950 27660 0 -1 0 19966 0 0 0 20694 129 0 0 25 0 1 0 1770426792 82788352 19953 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/954/statm): 20212 19953 145 145 0 20067 0 [pid=954] vsize: 80848 Current children cumulated CPU time (s) 208.24 Current children cumulated vsize (Kb) 82972 [startup+220.031 s] Raw data (loadavg): 0.98 0.85 0.90 2/57 954 Raw data (/proc/950/stat): 950 (minisat+_script) S 949 950 27660 0 -1 0 288 239 0 0 0 1 0 0 20 0 1 0 1770426787 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/950/statm): 531 226 485 147 0 384 0 [pid=950] vsize: 2124 Raw data (/proc/954/stat): 954 (minisat+_64-bit) R 950 950 27660 0 -1 0 20654 0 0 0 21681 135 0 0 25 0 1 0 1770426792 85602304 20641 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/954/statm): 20899 20641 145 145 0 20754 0 [pid=954] vsize: 83596 Current children cumulated CPU time (s) 218.17 Current children cumulated vsize (Kb) 85720 [startup+230.031 s] Raw data (loadavg): 0.98 0.86 0.90 2/57 954 Raw data (/proc/950/stat): 950 (minisat+_script) S 949 950 27660 0 -1 0 288 239 0 0 0 1 0 0 20 0 1 0 1770426787 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/950/statm): 531 226 485 147 0 384 0 [pid=950] vsize: 2124 Raw data (/proc/954/stat): 954 (minisat+_64-bit) R 950 950 27660 0 -1 0 21279 0 0 0 22672 139 0 0 25 0 1 0 1770426792 88170496 21266 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/954/statm): 21526 21266 145 145 0 21381 0 [pid=954] vsize: 86104 Current children cumulated CPU time (s) 228.12 Current children cumulated vsize (Kb) 88228 [startup+240.033 s] Raw data (loadavg): 0.99 0.86 0.90 2/57 954 Raw data (/proc/950/stat): 950 (minisat+_script) S 949 950 27660 0 -1 0 288 239 0 0 0 1 0 0 20 0 1 0 1770426787 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/950/statm): 531 226 485 147 0 384 0 [pid=950] vsize: 2124 Raw data (/proc/954/stat): 954 (minisat+_64-bit) R 950 950 27660 0 -1 0 21936 0 0 0 23661 144 0 0 25 0 1 0 1770426792 90845184 21923 4294967295 134512640 135094434 3221224448 3221223104 134558213 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/954/statm): 22179 21923 145 145 0 22034 0 [pid=954] vsize: 88716 Current children cumulated CPU time (s) 238.06 Current children cumulated vsize (Kb) 90840 [startup+250.034 s] Raw data (loadavg): 0.99 0.87 0.91 2/57 954 Raw data (/proc/950/stat): 950 (minisat+_script) S 949 950 27660 0 -1 0 288 239 0 0 0 1 0 0 20 0 1 0 1770426787 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/950/statm): 531 226 485 147 0 384 0 [pid=950] vsize: 2124 Raw data (/proc/954/stat): 954 (minisat+_64-bit) R 950 950 27660 0 -1 0 22626 0 0 0 24648 150 0 0 25 0 1 0 1770426792 93663232 22613 4294967295 134512640 135094434 3221224448 3221223072 134557705 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/954/statm): 22867 22613 145 145 0 22722 0 [pid=954] vsize: 91468 Current children cumulated CPU time (s) 247.99 Current children cumulated vsize (Kb) 93592 [startup+260.035 s] Raw data (loadavg): 0.99 0.87 0.91 2/57 954 Raw data (/proc/950/stat): 950 (minisat+_script) S 949 950 27660 0 -1 0 288 239 0 0 0 1 0 0 20 0 1 0 1770426787 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/950/statm): 531 226 485 147 0 384 0 [pid=950] vsize: 2124 Raw data (/proc/954/stat): 954 (minisat+_64-bit) R 950 950 27660 0 -1 0 23249 0 0 0 25636 155 0 0 25 0 1 0 1770426792 96206848 23236 4294967295 134512640 135094434 3221224448 3221223040 134557500 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/954/statm): 23488 23236 145 145 0 23343 0 [pid=954] vsize: 93952 Current children cumulated CPU time (s) 257.92 Current children cumulated vsize (Kb) 96076 [startup+270.037 s] Raw data (loadavg): 0.99 0.87 0.91 2/57 954 Raw data (/proc/950/stat): 950 (minisat+_script) S 949 950 27660 0 -1 0 288 239 0 0 0 1 0 0 20 0 1 0 1770426787 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/950/statm): 531 226 485 147 0 384 0 [pid=950] vsize: 2124 Raw data (/proc/954/stat): 954 (minisat+_64-bit) R 950 950 27660 0 -1 0 23828 0 0 0 26626 159 0 0 25 0 1 0 1770426792 98574336 23815 4294967295 134512640 135094434 3221224448 3221223072 134557711 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/954/statm): 24066 23815 145 145 0 23921 0 [pid=954] vsize: 96264 Current children cumulated CPU time (s) 267.86 Current children cumulated vsize (Kb) 98388 [startup+280.037 s] Raw data (loadavg): 0.99 0.88 0.91 2/57 954 Raw data (/proc/950/stat): 950 (minisat+_script) S 949 950 27660 0 -1 0 288 239 0 0 0 1 0 0 20 0 1 0 1770426787 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/950/statm): 531 226 485 147 0 384 0 [pid=950] vsize: 2124 Raw data (/proc/954/stat): 954 (minisat+_64-bit) R 950 950 27660 0 -1 0 24317 0 0 0 27616 163 0 0 25 0 1 0 1770426792 100577280 24304 4294967295 134512640 135094434 3221224448 3221223092 134558261 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/954/statm): 24555 24304 145 145 0 24410 0 [pid=954] vsize: 98220 Current children cumulated CPU time (s) 277.8 Current children cumulated vsize (Kb) 100344 [startup+290.039 s] Raw data (loadavg): 0.99 0.88 0.91 2/57 954 Raw data (/proc/950/stat): 950 (minisat+_script) S 949 950 27660 0 -1 0 288 239 0 0 0 1 0 0 20 0 1 0 1770426787 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/950/statm): 531 226 485 147 0 384 0 [pid=950] vsize: 2124 Raw data (/proc/954/stat): 954 (minisat+_64-bit) R 950 950 27660 0 -1 0 24909 0 0 0 28606 168 0 0 25 0 1 0 1770426792 102993920 24896 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/954/statm): 25145 24896 145 145 0 25000 0 [pid=954] vsize: 100580 Current children cumulated CPU time (s) 287.75 Current children cumulated vsize (Kb) 102704 [startup+300.04 s] Raw data (loadavg): 0.99 0.89 0.91 2/57 954 Raw data (/proc/950/stat): 950 (minisat+_script) S 949 950 27660 0 -1 0 288 239 0 0 0 1 0 0 20 0 1 0 1770426787 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/950/statm): 531 226 485 147 0 384 0 [pid=950] vsize: 2124 Raw data (/proc/954/stat): 954 (minisat+_64-bit) R 950 950 27660 0 -1 0 25506 0 0 0 29595 172 0 0 25 0 1 0 1770426792 105697280 25493 4294967295 134512640 135094434 3221224448 3221223096 134557061 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/954/statm): 25805 25493 145 145 0 25660 0 [pid=954] vsize: 103220 Current children cumulated CPU time (s) 297.68 Current children cumulated vsize (Kb) 105344 [startup+310.041 s] Raw data (loadavg): 0.99 0.89 0.91 2/57 954 Raw data (/proc/950/stat): 950 (minisat+_script) S 949 950 27660 0 -1 0 288 239 0 0 0 1 0 0 20 0 1 0 1770426787 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/950/statm): 531 226 485 147 0 384 0 [pid=950] vsize: 2124 Raw data (/proc/954/stat): 954 (minisat+_64-bit) R 950 950 27660 0 -1 0 26094 0 0 0 30585 176 0 0 25 0 1 0 1770426792 108101632 26081 4294967295 134512640 135094434 3221224448 3221223104 134558159 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/954/statm): 26392 26081 145 145 0 26247 0 [pid=954] vsize: 105568 Current children cumulated CPU time (s) 307.62 Current children cumulated vsize (Kb) 107692 [startup+320.041 s] Raw data (loadavg): 0.99 0.89 0.91 2/57 954 Raw data (/proc/950/stat): 950 (minisat+_script) S 949 950 27660 0 -1 0 288 239 0 0 0 1 0 0 20 0 1 0 1770426787 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/950/statm): 531 226 485 147 0 384 0 [pid=950] vsize: 2124 Raw data (/proc/954/stat): 954 (minisat+_64-bit) R 950 950 27660 0 -1 0 26683 0 0 0 31576 180 0 0 25 0 1 0 1770426792 110530560 26670 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/954/statm): 26985 26670 145 145 0 26840 0 [pid=954] vsize: 107940 Current children cumulated CPU time (s) 317.57 Current children cumulated vsize (Kb) 110064 [startup+330.043 s] Raw data (loadavg): 0.99 0.89 0.91 2/57 954 Raw data (/proc/950/stat): 950 (minisat+_script) S 949 950 27660 0 -1 0 288 239 0 0 0 1 0 0 20 0 1 0 1770426787 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/950/statm): 531 226 485 147 0 384 0 [pid=950] vsize: 2124 Raw data (/proc/954/stat): 954 (minisat+_64-bit) R 950 950 27660 0 -1 0 27149 0 0 0 32568 183 0 0 25 0 1 0 1770426792 112435200 27136 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/954/statm): 27450 27136 145 145 0 27305 0 [pid=954] vsize: 109800 Current children cumulated CPU time (s) 327.52 Current children cumulated vsize (Kb) 111924 [startup+340.044 s] Raw data (loadavg): 0.99 0.90 0.91 2/57 954 Raw data (/proc/950/stat): 950 (minisat+_script) S 949 950 27660 0 -1 0 288 239 0 0 0 1 0 0 20 0 1 0 1770426787 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/950/statm): 531 226 485 147 0 384 0 [pid=950] vsize: 2124 Raw data (/proc/954/stat): 954 (minisat+_64-bit) R 950 950 27660 0 -1 0 27663 0 0 0 33557 187 0 0 25 0 1 0 1770426792 114544640 27650 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/954/statm): 27965 27650 145 145 0 27820 0 [pid=954] vsize: 111860 Current children cumulated CPU time (s) 337.45 Current children cumulated vsize (Kb) 113984 [startup+350.045 s] Raw data (loadavg): 0.99 0.90 0.91 2/57 954 Raw data (/proc/950/stat): 950 (minisat+_script) S 949 950 27660 0 -1 0 288 239 0 0 0 1 0 0 20 0 1 0 1770426787 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/950/statm): 531 226 485 147 0 384 0 [pid=950] vsize: 2124 Raw data (/proc/954/stat): 954 (minisat+_64-bit) R 950 950 27660 0 -1 0 28206 0 0 0 34547 190 0 0 25 0 1 0 1770426792 116764672 28193 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/954/statm): 28507 28193 145 145 0 28362 0 [pid=954] vsize: 114028 Current children cumulated CPU time (s) 347.38 Current children cumulated vsize (Kb) 116152 [startup+360.046 s] Raw data (loadavg): 0.99 0.90 0.91 1/57 954 Raw data (/proc/950/stat): 950 (minisat+_script) S 949 950 27660 0 -1 0 288 239 0 0 0 1 0 0 20 0 1 0 1770426787 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/950/statm): 531 226 485 147 0 384 0 [pid=950] vsize: 2124 Raw data (/proc/954/stat): 954 (minisat+_64-bit) T 950 950 27660 0 -1 0 28755 0 0 0 35537 195 0 0 25 0 1 0 1770426792 119005184 28742 4294967295 134512640 135094434 3221224448 3221222812 134870330 0 0 5 16386 3222434794 0 0 17 0 0 0 Raw data (/proc/954/statm): 29054 28742 145 145 0 28909 0 [pid=954] vsize: 116216 Current children cumulated CPU time (s) 357.33 Current children cumulated vsize (Kb) 118340 [startup+370.046 s] Raw data (loadavg): 0.99 0.91 0.91 2/57 954 Raw data (/proc/950/stat): 950 (minisat+_script) S 949 950 27660 0 -1 0 288 239 0 0 0 1 0 0 20 0 1 0 1770426787 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/950/statm): 531 226 485 147 0 384 0 [pid=950] vsize: 2124 Raw data (/proc/954/stat): 954 (minisat+_64-bit) R 950 950 27660 0 -1 0 29225 0 0 0 36526 198 0 0 25 0 1 0 1770426792 120942592 29212 4294967295 134512640 135094434 3221224448 3221223104 134558235 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/954/statm): 29527 29212 145 145 0 29382 0 [pid=954] vsize: 118108 Current children cumulated CPU time (s) 367.25 Current children cumulated vsize (Kb) 120232 [startup+380.047 s] Raw data (loadavg): 0.99 0.91 0.91 2/57 954 Raw data (/proc/950/stat): 950 (minisat+_script) S 949 950 27660 0 -1 0 288 239 0 0 0 1 0 0 20 0 1 0 1770426787 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/950/statm): 531 226 485 147 0 384 0 [pid=950] vsize: 2124 Raw data (/proc/954/stat): 954 (minisat+_64-bit) R 950 950 27660 0 -1 0 29720 0 0 0 37517 202 0 0 25 0 1 0 1770426792 122970112 29707 4294967295 134512640 135094434 3221224448 3221223104 134558213 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/954/statm): 30022 29707 145 145 0 29877 0 [pid=954] vsize: 120088 Current children cumulated CPU time (s) 377.2 Current children cumulated vsize (Kb) 122212 [startup+390.049 s] Raw data (loadavg): 0.99 0.91 0.91 1/57 954 Raw data (/proc/950/stat): 950 (minisat+_script) S 949 950 27660 0 -1 0 288 239 0 0 0 1 0 0 20 0 1 0 1770426787 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/950/statm): 531 226 485 147 0 384 0 [pid=950] vsize: 2124 Raw data (/proc/954/stat): 954 (minisat+_64-bit) T 950 950 27660 0 -1 0 30241 0 0 0 38508 205 0 0 25 0 1 0 1770426792 125104128 30228 4294967295 134512640 135094434 3221224448 3221222812 134870330 0 0 5 16386 3222434794 0 0 17 0 0 0 Raw data (/proc/954/statm): 30543 30228 145 145 0 30398 0 [pid=954] vsize: 122172 Current children cumulated CPU time (s) 387.14 Current children cumulated vsize (Kb) 124296 [startup+400.05 s] Raw data (loadavg): 0.99 0.91 0.91 2/57 954 Raw data (/proc/950/stat): 950 (minisat+_script) S 949 950 27660 0 -1 0 288 239 0 0 0 1 0 0 20 0 1 0 1770426787 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/950/statm): 531 226 485 147 0 384 0 [pid=950] vsize: 2124 Raw data (/proc/954/stat): 954 (minisat+_64-bit) R 950 950 27660 0 -1 0 30591 0 0 0 39503 208 0 0 25 0 1 0 1770426792 126537728 30578 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/954/statm): 30893 30578 145 145 0 30748 0 [pid=954] vsize: 123572 Current children cumulated CPU time (s) 397.12 Current children cumulated vsize (Kb) 125696 [startup+410.05 s] Raw data (loadavg): 0.99 0.92 0.91 2/57 954 Raw data (/proc/950/stat): 950 (minisat+_script) S 949 950 27660 0 -1 0 288 239 0 0 0 1 0 0 20 0 1 0 1770426787 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/950/statm): 531 226 485 147 0 384 0 [pid=950] vsize: 2124 Raw data (/proc/954/stat): 954 (minisat+_64-bit) T 950 950 27660 0 -1 0 30987 0 0 0 40496 210 0 0 25 0 1 0 1770426792 128159744 30974 4294967295 134512640 135094434 3221224448 3221222828 134870330 0 0 5 16386 3222434794 0 0 17 0 0 0 Raw data (/proc/954/statm): 31289 30974 145 145 0 31144 0 [pid=954] vsize: 125156 Current children cumulated CPU time (s) 407.07 Current children cumulated vsize (Kb) 127280 [startup+420.05 s] Raw data (loadavg): 0.99 0.92 0.91 2/57 954 Raw data (/proc/950/stat): 950 (minisat+_script) S 949 950 27660 0 -1 0 288 239 0 0 0 1 0 0 20 0 1 0 1770426787 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/950/statm): 531 226 485 147 0 384 0 [pid=950] vsize: 2124 Raw data (/proc/954/stat): 954 (minisat+_64-bit) R 950 950 27660 0 -1 0 31398 0 0 0 41489 214 0 0 25 0 1 0 1770426792 129839104 31385 4294967295 134512640 135094434 3221224448 3221223104 134558159 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/954/statm): 31699 31385 145 145 0 31554 0 [pid=954] vsize: 126796 Current children cumulated CPU time (s) 417.04 Current children cumulated vsize (Kb) 128920 [startup+430.051 s] Raw data (loadavg): 0.99 0.92 0.91 2/57 954 Raw data (/proc/950/stat): 950 (minisat+_script) S 949 950 27660 0 -1 0 288 239 0 0 0 1 0 0 20 0 1 0 1770426787 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/950/statm): 531 226 485 147 0 384 0 [pid=950] vsize: 2124 Raw data (/proc/954/stat): 954 (minisat+_64-bit) R 950 950 27660 0 -1 0 31746 0 0 0 42484 215 0 0 25 0 1 0 1770426792 131264512 31733 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/954/statm): 32047 31733 145 145 0 31902 0 [pid=954] vsize: 128188 Current children cumulated CPU time (s) 427 Current children cumulated vsize (Kb) 130312 [startup+440.052 s] Raw data (loadavg): 0.99 0.92 0.91 2/57 954 Raw data (/proc/950/stat): 950 (minisat+_script) S 949 950 27660 0 -1 0 288 239 0 0 0 1 0 0 20 0 1 0 1770426787 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/950/statm): 531 226 485 147 0 384 0 [pid=950] vsize: 2124 Raw data (/proc/954/stat): 954 (minisat+_64-bit) R 950 950 27660 0 -1 0 32036 0 0 0 43479 218 0 0 25 0 1 0 1770426792 132456448 32023 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/954/statm): 32338 32023 145 145 0 32193 0 [pid=954] vsize: 129352 Current children cumulated CPU time (s) 436.98 Current children cumulated vsize (Kb) 131476 [startup+450.053 s] Raw data (loadavg): 0.99 0.92 0.91 2/57 954 Raw data (/proc/950/stat): 950 (minisat+_script) S 949 950 27660 0 -1 0 288 239 0 0 0 1 0 0 20 0 1 0 1770426787 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/950/statm): 531 226 485 147 0 384 0 [pid=950] vsize: 2124 Raw data (/proc/954/stat): 954 (minisat+_64-bit) R 950 950 27660 0 -1 0 32352 0 0 0 44474 219 0 0 25 0 1 0 1770426792 133746688 32339 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/954/statm): 32653 32339 145 145 0 32508 0 [pid=954] vsize: 130612 Current children cumulated CPU time (s) 446.94 Current children cumulated vsize (Kb) 132736 [startup+460.052 s] Raw data (loadavg): 0.99 0.93 0.91 2/57 954 Raw data (/proc/950/stat): 950 (minisat+_script) S 949 950 27660 0 -1 0 288 239 0 0 0 1 0 0 20 0 1 0 1770426787 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/950/statm): 531 226 485 147 0 384 0 [pid=950] vsize: 2124 Raw data (/proc/954/stat): 954 (minisat+_64-bit) R 950 950 27660 0 -1 0 32624 0 0 0 45469 221 0 0 25 0 1 0 1770426792 134877184 32611 4294967295 134512640 135094434 3221224448 3221223104 134558213 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/954/statm): 32929 32611 145 145 0 32784 0 [pid=954] vsize: 131716 Current children cumulated CPU time (s) 456.91 Current children cumulated vsize (Kb) 133840 [startup+470.053 s] Raw data (loadavg): 0.99 0.93 0.91 2/57 954 Raw data (/proc/950/stat): 950 (minisat+_script) S 949 950 27660 0 -1 0 288 239 0 0 0 1 0 0 20 0 1 0 1770426787 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/950/statm): 531 226 485 147 0 384 0 [pid=950] vsize: 2124 Raw data (/proc/954/stat): 954 (minisat+_64-bit) R 950 950 27660 0 -1 0 32893 0 0 0 46465 223 0 0 25 0 1 0 1770426792 135983104 32880 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/954/statm): 33199 32880 145 145 0 33054 0 [pid=954] vsize: 132796 Current children cumulated CPU time (s) 466.89 Current children cumulated vsize (Kb) 134920 [startup+480.054 s] Raw data (loadavg): 0.99 0.93 0.91 2/57 954 Raw data (/proc/950/stat): 950 (minisat+_script) S 949 950 27660 0 -1 0 288 239 0 0 0 1 0 0 20 0 1 0 1770426787 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/950/statm): 531 226 485 147 0 384 0 [pid=950] vsize: 2124 Raw data (/proc/954/stat): 954 (minisat+_64-bit) R 950 950 27660 0 -1 0 33153 0 0 0 47461 225 0 0 25 0 1 0 1770426792 137048064 33140 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/954/statm): 33459 33140 145 145 0 33314 0 [pid=954] vsize: 133836 Current children cumulated CPU time (s) 476.87 Current children cumulated vsize (Kb) 135960 [startup+490.055 s] Raw data (loadavg): 0.99 0.93 0.91 2/57 954 Raw data (/proc/950/stat): 950 (minisat+_script) S 949 950 27660 0 -1 0 288 239 0 0 0 1 0 0 20 0 1 0 1770426787 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/950/statm): 531 226 485 147 0 384 0 [pid=950] vsize: 2124 Raw data (/proc/954/stat): 954 (minisat+_64-bit) R 950 950 27660 0 -1 0 33558 0 0 0 48453 229 0 0 25 0 1 0 1770426792 138719232 33545 4294967295 134512640 135094434 3221224448 3221223104 134558235 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/954/statm): 33867 33545 145 145 0 33722 0 [pid=954] vsize: 135468 Current children cumulated CPU time (s) 486.83 Current children cumulated vsize (Kb) 137592 [startup+500.056 s] Raw data (loadavg): 0.99 0.93 0.91 2/57 954 Raw data (/proc/950/stat): 950 (minisat+_script) S 949 950 27660 0 -1 0 288 239 0 0 0 1 0 0 20 0 1 0 1770426787 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/950/statm): 531 226 485 147 0 384 0 [pid=950] vsize: 2124 Raw data (/proc/954/stat): 954 (minisat+_64-bit) R 950 950 27660 0 -1 0 33906 0 0 0 49446 232 0 0 25 0 1 0 1770426792 140152832 33893 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/954/statm): 34217 33893 145 145 0 34072 0 [pid=954] vsize: 136868 Current children cumulated CPU time (s) 496.79 Current children cumulated vsize (Kb) 138992 [startup+510.056 s] Raw data (loadavg): 0.99 0.94 0.91 2/57 954 Raw data (/proc/950/stat): 950 (minisat+_script) S 949 950 27660 0 -1 0 288 239 0 0 0 1 0 0 20 0 1 0 1770426787 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/950/statm): 531 226 485 147 0 384 0 [pid=950] vsize: 2124 Raw data (/proc/954/stat): 954 (minisat+_64-bit) R 950 950 27660 0 -1 0 34262 0 0 0 50438 236 0 0 25 0 1 0 1770426792 141615104 34249 4294967295 134512640 135094434 3221224448 3221223120 134555574 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/954/statm): 34574 34249 145 145 0 34429 0 [pid=954] vsize: 138296 Current children cumulated CPU time (s) 506.75 Current children cumulated vsize (Kb) 140420 [startup+520.057 s] Raw data (loadavg): 0.99 0.94 0.91 2/57 954 Raw data (/proc/950/stat): 950 (minisat+_script) S 949 950 27660 0 -1 0 288 239 0 0 0 1 0 0 20 0 1 0 1770426787 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/950/statm): 531 226 485 147 0 384 0 [pid=950] vsize: 2124 Raw data (/proc/954/stat): 954 (minisat+_64-bit) R 950 950 27660 0 -1 0 34687 0 0 0 51431 239 0 0 25 0 1 0 1770426792 143347712 34674 4294967295 134512640 135094434 3221224448 3221223104 134558213 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/954/statm): 34997 34674 145 145 0 34852 0 [pid=954] vsize: 139988 Current children cumulated CPU time (s) 516.71 Current children cumulated vsize (Kb) 142112 [startup+530.058 s] Raw data (loadavg): 0.99 0.94 0.91 2/57 954 Raw data (/proc/950/stat): 950 (minisat+_script) S 949 950 27660 0 -1 0 288 239 0 0 0 1 0 0 20 0 1 0 1770426787 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/950/statm): 531 226 485 147 0 384 0 [pid=950] vsize: 2124 Raw data (/proc/954/stat): 954 (minisat+_64-bit) R 950 950 27660 0 -1 0 35111 0 0 0 52422 243 0 0 25 0 1 0 1770426792 145080320 35098 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/954/statm): 35420 35098 145 145 0 35275 0 [pid=954] vsize: 141680 Current children cumulated CPU time (s) 526.66 Current children cumulated vsize (Kb) 143804 [startup+540.06 s] Raw data (loadavg): 0.99 0.94 0.91 2/57 954 Raw data (/proc/950/stat): 950 (minisat+_script) S 949 950 27660 0 -1 0 288 239 0 0 0 1 0 0 20 0 1 0 1770426787 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/950/statm): 531 226 485 147 0 384 0 [pid=950] vsize: 2124 Raw data (/proc/954/stat): 954 (minisat+_64-bit) R 950 950 27660 0 -1 0 35483 0 0 0 53413 248 0 0 25 0 1 0 1770426792 146604032 35470 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/954/statm): 35792 35470 145 145 0 35647 0 [pid=954] vsize: 143168 Current children cumulated CPU time (s) 536.62 Current children cumulated vsize (Kb) 145292 [startup+550.061 s] Raw data (loadavg): 0.99 0.94 0.91 2/57 954 Raw data (/proc/950/stat): 950 (minisat+_script) S 949 950 27660 0 -1 0 288 239 0 0 0 1 0 0 20 0 1 0 1770426787 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/950/statm): 531 226 485 147 0 384 0 [pid=950] vsize: 2124 Raw data (/proc/954/stat): 954 (minisat+_64-bit) R 950 950 27660 0 -1 0 35881 0 0 0 54405 252 0 0 25 0 1 0 1770426792 148238336 35868 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/954/statm): 36191 35868 145 145 0 36046 0 [pid=954] vsize: 144764 Current children cumulated CPU time (s) 546.58 Current children cumulated vsize (Kb) 146888 [startup+560.061 s] Raw data (loadavg): 0.99 0.94 0.91 2/57 954 Raw data (/proc/950/stat): 950 (minisat+_script) S 949 950 27660 0 -1 0 288 239 0 0 0 1 0 0 20 0 1 0 1770426787 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/950/statm): 531 226 485 147 0 384 0 [pid=950] vsize: 2124 Raw data (/proc/954/stat): 954 (minisat+_64-bit) R 950 950 27660 0 -1 0 36294 0 0 0 55396 256 0 0 25 0 1 0 1770426792 149938176 36281 4294967295 134512640 135094434 3221224448 3221223104 134557911 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/954/statm): 36606 36281 145 145 0 36461 0 [pid=954] vsize: 146424 Current children cumulated CPU time (s) 556.53 Current children cumulated vsize (Kb) 148548 [startup+570.063 s] Raw data (loadavg): 0.99 0.94 0.91 2/57 954 Raw data (/proc/950/stat): 950 (minisat+_script) S 949 950 27660 0 -1 0 288 239 0 0 0 1 0 0 20 0 1 0 1770426787 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/950/statm): 531 226 485 147 0 384 0 [pid=950] vsize: 2124 Raw data (/proc/954/stat): 954 (minisat+_64-bit) R 950 950 27660 0 -1 0 36735 0 0 0 56389 259 0 0 25 0 1 0 1770426792 151744512 36722 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/954/statm): 37047 36722 145 145 0 36902 0 [pid=954] vsize: 148188 Current children cumulated CPU time (s) 566.49 Current children cumulated vsize (Kb) 150312 [startup+580.064 s] Raw data (loadavg): 0.99 0.95 0.91 2/57 954 Raw data (/proc/950/stat): 950 (minisat+_script) S 949 950 27660 0 -1 0 288 239 0 0 0 1 0 0 20 0 1 0 1770426787 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/950/statm): 531 226 485 147 0 384 0 [pid=950] vsize: 2124 Raw data (/proc/954/stat): 954 (minisat+_64-bit) R 950 950 27660 0 -1 0 37086 0 0 0 57382 263 0 0 25 0 1 0 1770426792 153186304 37073 4294967295 134512640 135094434 3221224448 3221223040 134551718 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/954/statm): 37399 37073 145 145 0 37254 0 [pid=954] vsize: 149596 Current children cumulated CPU time (s) 576.46 Current children cumulated vsize (Kb) 151720 [startup+590.065 s] Raw data (loadavg): 0.99 0.95 0.91 2/57 954 Raw data (/proc/950/stat): 950 (minisat+_script) S 949 950 27660 0 -1 0 288 239 0 0 0 1 0 0 20 0 1 0 1770426787 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/950/statm): 531 226 485 147 0 384 0 [pid=950] vsize: 2124 Raw data (/proc/954/stat): 954 (minisat+_64-bit) R 950 950 27660 0 -1 0 37229 0 0 0 58379 264 0 0 25 0 1 0 1770426792 153767936 37216 4294967295 134512640 135094434 3221224448 3221223104 134558178 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/954/statm): 37541 37216 145 145 0 37396 0 [pid=954] vsize: 150164 Current children cumulated CPU time (s) 586.44 Current children cumulated vsize (Kb) 152288 [startup+600.066 s] Raw data (loadavg): 0.99 0.95 0.91 2/57 954 Raw data (/proc/950/stat): 950 (minisat+_script) S 949 950 27660 0 -1 0 288 239 0 0 0 1 0 0 20 0 1 0 1770426787 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/950/statm): 531 226 485 147 0 384 0 [pid=950] vsize: 2124 Raw data (/proc/954/stat): 954 (minisat+_64-bit) R 950 950 27660 0 -1 0 37229 0 0 0 59378 265 0 0 25 0 1 0 1770426792 153767936 37216 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/954/statm): 37541 37216 145 145 0 37396 0 [pid=954] vsize: 150164 Current children cumulated CPU time (s) 596.44 Current children cumulated vsize (Kb) 152288 [startup+610.067 s] Raw data (loadavg): 0.99 0.95 0.91 2/57 954 Raw data (/proc/950/stat): 950 (minisat+_script) S 949 950 27660 0 -1 0 288 239 0 0 0 1 0 0 20 0 1 0 1770426787 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/950/statm): 531 226 485 147 0 384 0 [pid=950] vsize: 2124 Raw data (/proc/954/stat): 954 (minisat+_64-bit) R 950 950 27660 0 -1 0 37229 0 0 0 60378 265 0 0 25 0 1 0 1770426792 153767936 37216 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/954/statm): 37541 37216 145 145 0 37396 0 [pid=954] vsize: 150164 Current children cumulated CPU time (s) 606.44 Current children cumulated vsize (Kb) 152288 [startup+620.068 s] Raw data (loadavg): 0.99 0.95 0.91 2/57 954 Raw data (/proc/950/stat): 950 (minisat+_script) S 949 950 27660 0 -1 0 288 239 0 0 0 1 0 0 20 0 1 0 1770426787 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/950/statm): 531 226 485 147 0 384 0 [pid=950] vsize: 2124 Raw data (/proc/954/stat): 954 (minisat+_64-bit) R 950 950 27660 0 -1 0 37229 0 0 0 61378 265 0 0 25 0 1 0 1770426792 153767936 37216 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/954/statm): 37541 37216 145 145 0 37396 0 [pid=954] vsize: 150164 Current children cumulated CPU time (s) 616.44 Current children cumulated vsize (Kb) 152288 [startup+630.07 s] Raw data (loadavg): 0.99 0.95 0.91 2/57 954 Raw data (/proc/950/stat): 950 (minisat+_script) S 949 950 27660 0 -1 0 288 239 0 0 0 1 0 0 20 0 1 0 1770426787 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/950/statm): 531 226 485 147 0 384 0 [pid=950] vsize: 2124 Raw data (/proc/954/stat): 954 (minisat+_64-bit) R 950 950 27660 0 -1 0 37230 0 0 0 62378 265 0 0 25 0 1 0 1770426792 153767936 37217 4294967295 134512640 135094434 3221224448 3221223104 134558213 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/954/statm): 37541 37217 145 145 0 37396 0 [pid=954] vsize: 150164 Current children cumulated CPU time (s) 626.44 Current children cumulated vsize (Kb) 152288 [startup+640.071 s] Raw data (loadavg): 0.99 0.95 0.91 2/57 954 Raw data (/proc/950/stat): 950 (minisat+_script) S 949 950 27660 0 -1 0 288 239 0 0 0 1 0 0 20 0 1 0 1770426787 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/950/statm): 531 226 485 147 0 384 0 [pid=950] vsize: 2124 Raw data (/proc/954/stat): 954 (minisat+_64-bit) R 950 950 27660 0 -1 0 37230 0 0 0 63377 266 0 0 25 0 1 0 1770426792 153767936 37217 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/954/statm): 37541 37217 145 145 0 37396 0 [pid=954] vsize: 150164 Current children cumulated CPU time (s) 636.44 Current children cumulated vsize (Kb) 152288 [startup+650.071 s] Raw data (loadavg): 0.99 0.95 0.91 2/57 954 Raw data (/proc/950/stat): 950 (minisat+_script) S 949 950 27660 0 -1 0 288 239 0 0 0 1 0 0 20 0 1 0 1770426787 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/950/statm): 531 226 485 147 0 384 0 [pid=950] vsize: 2124 Raw data (/proc/954/stat): 954 (minisat+_64-bit) R 950 950 27660 0 -1 0 37230 0 0 0 64377 266 0 0 25 0 1 0 1770426792 153767936 37217 4294967295 134512640 135094434 3221224448 3221223104 134557988 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/954/statm): 37541 37217 145 145 0 37396 0 [pid=954] vsize: 150164 Current children cumulated CPU time (s) 646.44 Current children cumulated vsize (Kb) 152288 [startup+660.072 s] Raw data (loadavg): 0.99 0.95 0.91 2/57 954 Raw data (/proc/950/stat): 950 (minisat+_script) S 949 950 27660 0 -1 0 288 239 0 0 0 1 0 0 20 0 1 0 1770426787 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/950/statm): 531 226 485 147 0 384 0 [pid=950] vsize: 2124 Raw data (/proc/954/stat): 954 (minisat+_64-bit) R 950 950 27660 0 -1 0 37230 0 0 0 65377 267 0 0 25 0 1 0 1770426792 153767936 37217 4294967295 134512640 135094434 3221224448 3221223080 134557563 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/954/statm): 37541 37217 145 145 0 37396 0 [pid=954] vsize: 150164 Current children cumulated CPU time (s) 656.45 Current children cumulated vsize (Kb) 152288 [startup+670.074 s] Raw data (loadavg): 0.99 0.95 0.91 2/57 954 Raw data (/proc/950/stat): 950 (minisat+_script) S 949 950 27660 0 -1 0 288 239 0 0 0 1 0 0 20 0 1 0 1770426787 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/950/statm): 531 226 485 147 0 384 0 [pid=950] vsize: 2124 Raw data (/proc/954/stat): 954 (minisat+_64-bit) R 950 950 27660 0 -1 0 37230 0 0 0 66376 267 0 0 25 0 1 0 1770426792 153767936 37217 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/954/statm): 37541 37217 145 145 0 37396 0 [pid=954] vsize: 150164 Current children cumulated CPU time (s) 666.44 Current children cumulated vsize (Kb) 152288 [startup+680.075 s] Raw data (loadavg): 0.99 0.95 0.91 2/57 954 Raw data (/proc/950/stat): 950 (minisat+_script) S 949 950 27660 0 -1 0 288 239 0 0 0 1 0 0 20 0 1 0 1770426787 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/950/statm): 531 226 485 147 0 384 0 [pid=950] vsize: 2124 Raw data (/proc/954/stat): 954 (minisat+_64-bit) R 950 950 27660 0 -1 0 37230 0 0 0 67376 268 0 0 25 0 1 0 1770426792 153767936 37217 4294967295 134512640 135094434 3221224448 3221223104 134557996 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/954/statm): 37541 37217 145 145 0 37396 0 [pid=954] vsize: 150164 Current children cumulated CPU time (s) 676.45 Current children cumulated vsize (Kb) 152288 [startup+690.076 s] Raw data (loadavg): 0.99 0.96 0.91 2/57 954 Raw data (/proc/950/stat): 950 (minisat+_script) S 949 950 27660 0 -1 0 288 239 0 0 0 1 0 0 20 0 1 0 1770426787 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/950/statm): 531 226 485 147 0 384 0 [pid=950] vsize: 2124 Raw data (/proc/954/stat): 954 (minisat+_64-bit) R 950 950 27660 0 -1 0 37230 0 0 0 68376 268 0 0 25 0 1 0 1770426792 153767936 37217 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/954/statm): 37541 37217 145 145 0 37396 0 [pid=954] vsize: 150164 Current children cumulated CPU time (s) 686.45 Current children cumulated vsize (Kb) 152288 [startup+700.076 s] Raw data (loadavg): 0.99 0.96 0.91 2/57 954 Raw data (/proc/950/stat): 950 (minisat+_script) S 949 950 27660 0 -1 0 288 239 0 0 0 1 0 0 20 0 1 0 1770426787 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/950/statm): 531 226 485 147 0 384 0 [pid=950] vsize: 2124 Raw data (/proc/954/stat): 954 (minisat+_64-bit) R 950 950 27660 0 -1 0 37231 0 0 0 69375 268 0 0 25 0 1 0 1770426792 153767936 37218 4294967295 134512640 135094434 3221224448 3221223104 134558213 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/954/statm): 37541 37218 145 145 0 37396 0 [pid=954] vsize: 150164 Current children cumulated CPU time (s) 696.44 Current children cumulated vsize (Kb) 152288 [startup+710.077 s] Raw data (loadavg): 0.99 0.96 0.91 2/57 954 Raw data (/proc/950/stat): 950 (minisat+_script) S 949 950 27660 0 -1 0 288 239 0 0 0 1 0 0 20 0 1 0 1770426787 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/950/statm): 531 226 485 147 0 384 0 [pid=950] vsize: 2124 Raw data (/proc/954/stat): 954 (minisat+_64-bit) R 950 950 27660 0 -1 0 37232 0 0 0 70375 268 0 0 25 0 1 0 1770426792 153767936 37219 4294967295 134512640 135094434 3221224448 3221223104 134558208 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/954/statm): 37541 37219 145 145 0 37396 0 [pid=954] vsize: 150164 Current children cumulated CPU time (s) 706.44 Current children cumulated vsize (Kb) 152288 [startup+720.079 s] Raw data (loadavg): 0.99 0.96 0.91 2/57 954 Raw data (/proc/950/stat): 950 (minisat+_script) S 949 950 27660 0 -1 0 288 239 0 0 0 1 0 0 20 0 1 0 1770426787 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/950/statm): 531 226 485 147 0 384 0 [pid=950] vsize: 2124 Raw data (/proc/954/stat): 954 (minisat+_64-bit) R 950 950 27660 0 -1 0 37233 0 0 0 71375 269 0 0 25 0 1 0 1770426792 153767936 37220 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/954/statm): 37541 37220 145 145 0 37396 0 [pid=954] vsize: 150164 Current children cumulated CPU time (s) 716.45 Current children cumulated vsize (Kb) 152288 [startup+730.08 s] Raw data (loadavg): 0.99 0.96 0.91 2/57 954 Raw data (/proc/950/stat): 950 (minisat+_script) S 949 950 27660 0 -1 0 288 239 0 0 0 1 0 0 20 0 1 0 1770426787 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/950/statm): 531 226 485 147 0 384 0 [pid=950] vsize: 2124 Raw data (/proc/954/stat): 954 (minisat+_64-bit) R 950 950 27660 0 -1 0 37233 0 0 0 72375 269 0 0 25 0 1 0 1770426792 153767936 37220 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/954/statm): 37541 37220 145 145 0 37396 0 [pid=954] vsize: 150164 Current children cumulated CPU time (s) 726.45 Current children cumulated vsize (Kb) 152288 [startup+740.079 s] Raw data (loadavg): 0.99 0.96 0.91 2/57 954 Raw data (/proc/950/stat): 950 (minisat+_script) S 949 950 27660 0 -1 0 288 239 0 0 0 1 0 0 20 0 1 0 1770426787 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/950/statm): 531 226 485 147 0 384 0 [pid=950] vsize: 2124 Raw data (/proc/954/stat): 954 (minisat+_64-bit) R 950 950 27660 0 -1 0 37233 0 0 0 73374 269 0 0 25 0 1 0 1770426792 153767936 37220 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/954/statm): 37541 37220 145 145 0 37396 0 [pid=954] vsize: 150164 Current children cumulated CPU time (s) 736.44 Current children cumulated vsize (Kb) 152288 [startup+750.081 s] Raw data (loadavg): 0.99 0.96 0.91 2/57 954 Raw data (/proc/950/stat): 950 (minisat+_script) S 949 950 27660 0 -1 0 288 239 0 0 0 1 0 0 20 0 1 0 1770426787 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/950/statm): 531 226 485 147 0 384 0 [pid=950] vsize: 2124 Raw data (/proc/954/stat): 954 (minisat+_64-bit) R 950 950 27660 0 -1 0 37233 0 0 0 74374 270 0 0 25 0 1 0 1770426792 153767936 37220 4294967295 134512640 135094434 3221224448 3221223104 134557988 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/954/statm): 37541 37220 145 145 0 37396 0 [pid=954] vsize: 150164 Current children cumulated CPU time (s) 746.45 Current children cumulated vsize (Kb) 152288 [startup+760.082 s] Raw data (loadavg): 0.99 0.96 0.91 2/57 954 Raw data (/proc/950/stat): 950 (minisat+_script) S 949 950 27660 0 -1 0 288 239 0 0 0 1 0 0 20 0 1 0 1770426787 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/950/statm): 531 226 485 147 0 384 0 [pid=950] vsize: 2124 Raw data (/proc/954/stat): 954 (minisat+_64-bit) R 950 950 27660 0 -1 0 37233 0 0 0 75373 270 0 0 25 0 1 0 1770426792 153767936 37220 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/954/statm): 37541 37220 145 145 0 37396 0 [pid=954] vsize: 150164 Current children cumulated CPU time (s) 756.44 Current children cumulated vsize (Kb) 152288 [startup+770.084 s] Raw data (loadavg): 0.99 0.96 0.91 2/57 954 Raw data (/proc/950/stat): 950 (minisat+_script) S 949 950 27660 0 -1 0 288 239 0 0 0 1 0 0 20 0 1 0 1770426787 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/950/statm): 531 226 485 147 0 384 0 [pid=950] vsize: 2124 Raw data (/proc/954/stat): 954 (minisat+_64-bit) R 950 950 27660 0 -1 0 37233 0 0 0 76373 270 0 0 25 0 1 0 1770426792 153767936 37220 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/954/statm): 37541 37220 145 145 0 37396 0 [pid=954] vsize: 150164 Current children cumulated CPU time (s) 766.44 Current children cumulated vsize (Kb) 152288 [startup+780.085 s] Raw data (loadavg): 0.99 0.96 0.91 2/57 954 Raw data (/proc/950/stat): 950 (minisat+_script) S 949 950 27660 0 -1 0 288 239 0 0 0 1 0 0 20 0 1 0 1770426787 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/950/statm): 531 226 485 147 0 384 0 [pid=950] vsize: 2124 Raw data (/proc/954/stat): 954 (minisat+_64-bit) R 950 950 27660 0 -1 0 37234 0 0 0 77373 271 0 0 25 0 1 0 1770426792 153767936 37221 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/954/statm): 37541 37221 145 145 0 37396 0 [pid=954] vsize: 150164 Current children cumulated CPU time (s) 776.45 Current children cumulated vsize (Kb) 152288 [startup+790.084 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 954 Raw data (/proc/950/stat): 950 (minisat+_script) S 949 950 27660 0 -1 0 288 239 0 0 0 1 0 0 20 0 1 0 1770426787 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/950/statm): 531 226 485 147 0 384 0 [pid=950] vsize: 2124 Raw data (/proc/954/stat): 954 (minisat+_64-bit) R 950 950 27660 0 -1 0 37234 0 0 0 78372 271 0 0 25 0 1 0 1770426792 153767936 37221 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/954/statm): 37541 37221 145 145 0 37396 0 [pid=954] vsize: 150164 Current children cumulated CPU time (s) 786.44 Current children cumulated vsize (Kb) 152288 [startup+800.086 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 954 Raw data (/proc/950/stat): 950 (minisat+_script) S 949 950 27660 0 -1 0 288 239 0 0 0 1 0 0 20 0 1 0 1770426787 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/950/statm): 531 226 485 147 0 384 0 [pid=950] vsize: 2124 Raw data (/proc/954/stat): 954 (minisat+_64-bit) R 950 950 27660 0 -1 0 37234 0 0 0 79372 272 0 0 25 0 1 0 1770426792 153767936 37221 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/954/statm): 37541 37221 145 145 0 37396 0 [pid=954] vsize: 150164 Current children cumulated CPU time (s) 796.45 Current children cumulated vsize (Kb) 152288 [startup+810.087 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 954 Raw data (/proc/950/stat): 950 (minisat+_script) S 949 950 27660 0 -1 0 288 239 0 0 0 1 0 0 20 0 1 0 1770426787 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/950/statm): 531 226 485 147 0 384 0 [pid=950] vsize: 2124 Raw data (/proc/954/stat): 954 (minisat+_64-bit) R 950 950 27660 0 -1 0 37234 0 0 0 80371 272 0 0 25 0 1 0 1770426792 153767936 37221 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/954/statm): 37541 37221 145 145 0 37396 0 [pid=954] vsize: 150164 Current children cumulated CPU time (s) 806.44 Current children cumulated vsize (Kb) 152288 [startup+820.088 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 954 Raw data (/proc/950/stat): 950 (minisat+_script) S 949 950 27660 0 -1 0 288 239 0 0 0 1 0 0 20 0 1 0 1770426787 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/950/statm): 531 226 485 147 0 384 0 [pid=950] vsize: 2124 Raw data (/proc/954/stat): 954 (minisat+_64-bit) R 950 950 27660 0 -1 0 37234 0 0 0 81371 272 0 0 25 0 1 0 1770426792 153767936 37221 4294967295 134512640 135094434 3221224448 3221223104 134558009 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/954/statm): 37541 37221 145 145 0 37396 0 [pid=954] vsize: 150164 Current children cumulated CPU time (s) 816.44 Current children cumulated vsize (Kb) 152288 [startup+830.088 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 954 Raw data (/proc/950/stat): 950 (minisat+_script) S 949 950 27660 0 -1 0 288 239 0 0 0 1 0 0 20 0 1 0 1770426787 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/950/statm): 531 226 485 147 0 384 0 [pid=950] vsize: 2124 Raw data (/proc/954/stat): 954 (minisat+_64-bit) R 950 950 27660 0 -1 0 37234 0 0 0 82370 273 0 0 25 0 1 0 1770426792 153767936 37221 4294967295 134512640 135094434 3221224448 3221223104 134558019 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/954/statm): 37541 37221 145 145 0 37396 0 [pid=954] vsize: 150164 Current children cumulated CPU time (s) 826.44 Current children cumulated vsize (Kb) 152288 [startup+840.089 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 954 Raw data (/proc/950/stat): 950 (minisat+_script) S 949 950 27660 0 -1 0 288 239 0 0 0 1 0 0 20 0 1 0 1770426787 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/950/statm): 531 226 485 147 0 384 0 [pid=950] vsize: 2124 Raw data (/proc/954/stat): 954 (minisat+_64-bit) R 950 950 27660 0 -1 0 37234 0 0 0 83370 273 0 0 25 0 1 0 1770426792 153767936 37221 4294967295 134512640 135094434 3221224448 3221223040 134556826 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/954/statm): 37541 37221 145 145 0 37396 0 [pid=954] vsize: 150164 Current children cumulated CPU time (s) 836.44 Current children cumulated vsize (Kb) 152288 [startup+850.09 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 954 Raw data (/proc/950/stat): 950 (minisat+_script) S 949 950 27660 0 -1 0 288 239 0 0 0 1 0 0 20 0 1 0 1770426787 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/950/statm): 531 226 485 147 0 384 0 [pid=950] vsize: 2124 Raw data (/proc/954/stat): 954 (minisat+_64-bit) R 950 950 27660 0 -1 0 37234 0 0 0 84370 273 0 0 25 0 1 0 1770426792 153767936 37221 4294967295 134512640 135094434 3221224448 3221223104 134557988 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/954/statm): 37541 37221 145 145 0 37396 0 [pid=954] vsize: 150164 Current children cumulated CPU time (s) 846.44 Current children cumulated vsize (Kb) 152288 [startup+860.091 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 954 Raw data (/proc/950/stat): 950 (minisat+_script) S 949 950 27660 0 -1 0 288 239 0 0 0 1 0 0 20 0 1 0 1770426787 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/950/statm): 531 226 485 147 0 384 0 [pid=950] vsize: 2124 Raw data (/proc/954/stat): 954 (minisat+_64-bit) R 950 950 27660 0 -1 0 37234 0 0 0 85370 273 0 0 25 0 1 0 1770426792 153767936 37221 4294967295 134512640 135094434 3221224448 3221223040 134557236 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/954/statm): 37541 37221 145 145 0 37396 0 [pid=954] vsize: 150164 Current children cumulated CPU time (s) 856.44 Current children cumulated vsize (Kb) 152288 [startup+870.093 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 954 Raw data (/proc/950/stat): 950 (minisat+_script) S 949 950 27660 0 -1 0 288 239 0 0 0 1 0 0 20 0 1 0 1770426787 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/950/statm): 531 226 485 147 0 384 0 [pid=950] vsize: 2124 Raw data (/proc/954/stat): 954 (minisat+_64-bit) R 950 950 27660 0 -1 0 37234 0 0 0 86370 273 0 0 25 0 1 0 1770426792 153767936 37221 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/954/statm): 37541 37221 145 145 0 37396 0 [pid=954] vsize: 150164 Current children cumulated CPU time (s) 866.44 Current children cumulated vsize (Kb) 152288 [startup+880.093 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 954 Raw data (/proc/950/stat): 950 (minisat+_script) S 949 950 27660 0 -1 0 288 239 0 0 0 1 0 0 20 0 1 0 1770426787 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/950/statm): 531 226 485 147 0 384 0 [pid=950] vsize: 2124 Raw data (/proc/954/stat): 954 (minisat+_64-bit) R 950 950 27660 0 -1 0 37234 0 0 0 87370 273 0 0 25 0 1 0 1770426792 153767936 37221 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/954/statm): 37541 37221 145 145 0 37396 0 [pid=954] vsize: 150164 Current children cumulated CPU time (s) 876.44 Current children cumulated vsize (Kb) 152288 [startup+890.094 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 954 Raw data (/proc/950/stat): 950 (minisat+_script) S 949 950 27660 0 -1 0 288 239 0 0 0 1 0 0 20 0 1 0 1770426787 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/950/statm): 531 226 485 147 0 384 0 [pid=950] vsize: 2124 Raw data (/proc/954/stat): 954 (minisat+_64-bit) R 950 950 27660 0 -1 0 37234 0 0 0 88370 273 0 0 25 0 1 0 1770426792 153767936 37221 4294967295 134512640 135094434 3221224448 3221223104 134558019 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/954/statm): 37541 37221 145 145 0 37396 0 [pid=954] vsize: 150164 Current children cumulated CPU time (s) 886.44 Current children cumulated vsize (Kb) 152288 [startup+900.095 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 954 Raw data (/proc/950/stat): 950 (minisat+_script) S 949 950 27660 0 -1 0 288 239 0 0 0 1 0 0 20 0 1 0 1770426787 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/950/statm): 531 226 485 147 0 384 0 [pid=950] vsize: 2124 Raw data (/proc/954/stat): 954 (minisat+_64-bit) R 950 950 27660 0 -1 0 37234 0 0 0 89371 273 0 0 25 0 1 0 1770426792 153767936 37221 4294967295 134512640 135094434 3221224448 3221223104 134558178 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/954/statm): 37541 37221 145 145 0 37396 0 [pid=954] vsize: 150164 Current children cumulated CPU time (s) 896.45 Current children cumulated vsize (Kb) 152288 [startup+910.096 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 954 Raw data (/proc/950/stat): 950 (minisat+_script) S 949 950 27660 0 -1 0 288 239 0 0 0 1 0 0 20 0 1 0 1770426787 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/950/statm): 531 226 485 147 0 384 0 [pid=950] vsize: 2124 Raw data (/proc/954/stat): 954 (minisat+_64-bit) R 950 950 27660 0 -1 0 37234 0 0 0 90371 273 0 0 25 0 1 0 1770426792 153767936 37221 4294967295 134512640 135094434 3221224448 3221223104 134557988 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/954/statm): 37541 37221 145 145 0 37396 0 [pid=954] vsize: 150164 Current children cumulated CPU time (s) 906.45 Current children cumulated vsize (Kb) 152288 [startup+920.096 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 954 Raw data (/proc/950/stat): 950 (minisat+_script) S 949 950 27660 0 -1 0 288 239 0 0 0 1 0 0 20 0 1 0 1770426787 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/950/statm): 531 226 485 147 0 384 0 [pid=950] vsize: 2124 Raw data (/proc/954/stat): 954 (minisat+_64-bit) R 950 950 27660 0 -1 0 37234 0 0 0 91371 273 0 0 25 0 1 0 1770426792 153767936 37221 4294967295 134512640 135094434 3221224448 3221223104 134557900 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/954/statm): 37541 37221 145 145 0 37396 0 [pid=954] vsize: 150164 Current children cumulated CPU time (s) 916.45 Current children cumulated vsize (Kb) 152288 [startup+930.097 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 954 Raw data (/proc/950/stat): 950 (minisat+_script) S 949 950 27660 0 -1 0 288 239 0 0 0 1 0 0 20 0 1 0 1770426787 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/950/statm): 531 226 485 147 0 384 0 [pid=950] vsize: 2124 Raw data (/proc/954/stat): 954 (minisat+_64-bit) R 950 950 27660 0 -1 0 37234 0 0 0 92371 273 0 0 25 0 1 0 1770426792 153767936 37221 4294967295 134512640 135094434 3221224448 3221223104 134557988 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/954/statm): 37541 37221 145 145 0 37396 0 [pid=954] vsize: 150164 Current children cumulated CPU time (s) 926.45 Current children cumulated vsize (Kb) 152288 [startup+940.098 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 954 Raw data (/proc/950/stat): 950 (minisat+_script) S 949 950 27660 0 -1 0 288 239 0 0 0 1 0 0 20 0 1 0 1770426787 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/950/statm): 531 226 485 147 0 384 0 [pid=950] vsize: 2124 Raw data (/proc/954/stat): 954 (minisat+_64-bit) R 950 950 27660 0 -1 0 37234 0 0 0 93372 273 0 0 25 0 1 0 1770426792 153767936 37221 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/954/statm): 37541 37221 145 145 0 37396 0 [pid=954] vsize: 150164 Current children cumulated CPU time (s) 936.46 Current children cumulated vsize (Kb) 152288 [startup+950.099 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 954 Raw data (/proc/950/stat): 950 (minisat+_script) S 949 950 27660 0 -1 0 288 239 0 0 0 1 0 0 20 0 1 0 1770426787 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/950/statm): 531 226 485 147 0 384 0 [pid=950] vsize: 2124 Raw data (/proc/954/stat): 954 (minisat+_64-bit) R 950 950 27660 0 -1 0 37234 0 0 0 94372 273 0 0 25 0 1 0 1770426792 153767936 37221 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/954/statm): 37541 37221 145 145 0 37396 0 [pid=954] vsize: 150164 Current children cumulated CPU time (s) 946.46 Current children cumulated vsize (Kb) 152288 [startup+960.1 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 954 Raw data (/proc/950/stat): 950 (minisat+_script) S 949 950 27660 0 -1 0 288 239 0 0 0 1 0 0 20 0 1 0 1770426787 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/950/statm): 531 226 485 147 0 384 0 [pid=950] vsize: 2124 Raw data (/proc/954/stat): 954 (minisat+_64-bit) R 950 950 27660 0 -1 0 37234 0 0 0 95372 273 0 0 25 0 1 0 1770426792 153767936 37221 4294967295 134512640 135094434 3221224448 3221223040 134556715 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/954/statm): 37541 37221 145 145 0 37396 0 [pid=954] vsize: 150164 Current children cumulated CPU time (s) 956.46 Current children cumulated vsize (Kb) 152288 [startup+970.1 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 954 Raw data (/proc/950/stat): 950 (minisat+_script) S 949 950 27660 0 -1 0 288 239 0 0 0 1 0 0 20 0 1 0 1770426787 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/950/statm): 531 226 485 147 0 384 0 [pid=950] vsize: 2124 Raw data (/proc/954/stat): 954 (minisat+_64-bit) R 950 950 27660 0 -1 0 37234 0 0 0 96372 273 0 0 25 0 1 0 1770426792 153767936 37221 4294967295 134512640 135094434 3221224448 3221223104 134558019 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/954/statm): 37541 37221 145 145 0 37396 0 [pid=954] vsize: 150164 Current children cumulated CPU time (s) 966.46 Current children cumulated vsize (Kb) 152288 [startup+980.101 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 954 Raw data (/proc/950/stat): 950 (minisat+_script) S 949 950 27660 0 -1 0 288 239 0 0 0 1 0 0 20 0 1 0 1770426787 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/950/statm): 531 226 485 147 0 384 0 [pid=950] vsize: 2124 Raw data (/proc/954/stat): 954 (minisat+_64-bit) R 950 950 27660 0 -1 0 37234 0 0 0 97373 273 0 0 25 0 1 0 1770426792 153767936 37221 4294967295 134512640 135094434 3221224448 3221223104 134558013 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/954/statm): 37541 37221 145 145 0 37396 0 [pid=954] vsize: 150164 Current children cumulated CPU time (s) 976.47 Current children cumulated vsize (Kb) 152288 [startup+990.102 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 954 Raw data (/proc/950/stat): 950 (minisat+_script) S 949 950 27660 0 -1 0 288 239 0 0 0 1 0 0 20 0 1 0 1770426787 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/950/statm): 531 226 485 147 0 384 0 [pid=950] vsize: 2124 Raw data (/proc/954/stat): 954 (minisat+_64-bit) R 950 950 27660 0 -1 0 37234 0 0 0 98373 273 0 0 25 0 1 0 1770426792 153767936 37221 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/954/statm): 37541 37221 145 145 0 37396 0 [pid=954] vsize: 150164 Current children cumulated CPU time (s) 986.47 Current children cumulated vsize (Kb) 152288 [startup+1000.1 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 954 Raw data (/proc/950/stat): 950 (minisat+_script) S 949 950 27660 0 -1 0 288 239 0 0 0 1 0 0 20 0 1 0 1770426787 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/950/statm): 531 226 485 147 0 384 0 [pid=950] vsize: 2124 Raw data (/proc/954/stat): 954 (minisat+_64-bit) R 950 950 27660 0 -1 0 37234 0 0 0 99373 273 0 0 25 0 1 0 1770426792 153767936 37221 4294967295 134512640 135094434 3221224448 3221223104 134558249 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/954/statm): 37541 37221 145 145 0 37396 0 [pid=954] vsize: 150164 Current children cumulated CPU time (s) 996.47 Current children cumulated vsize (Kb) 152288 [startup+1010.1 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 954 Raw data (/proc/950/stat): 950 (minisat+_script) S 949 950 27660 0 -1 0 288 239 0 0 0 1 0 0 20 0 1 0 1770426787 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/950/statm): 531 226 485 147 0 384 0 [pid=950] vsize: 2124 Raw data (/proc/954/stat): 954 (minisat+_64-bit) R 950 950 27660 0 -1 0 37234 0 0 0 100373 273 0 0 25 0 1 0 1770426792 153767936 37221 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/954/statm): 37541 37221 145 145 0 37396 0 [pid=954] vsize: 150164 Current children cumulated CPU time (s) 1006.47 Current children cumulated vsize (Kb) 152288 [startup+1020.1 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 954 Raw data (/proc/950/stat): 950 (minisat+_script) S 949 950 27660 0 -1 0 288 239 0 0 0 1 0 0 20 0 1 0 1770426787 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/950/statm): 531 226 485 147 0 384 0 [pid=950] vsize: 2124 Raw data (/proc/954/stat): 954 (minisat+_64-bit) R 950 950 27660 0 -1 0 37234 0 0 0 101373 273 0 0 25 0 1 0 1770426792 153767936 37221 4294967295 134512640 135094434 3221224448 3221223104 134557849 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/954/statm): 37541 37221 145 145 0 37396 0 [pid=954] vsize: 150164 Current children cumulated CPU time (s) 1016.47 Current children cumulated vsize (Kb) 152288 [startup+1030.11 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 954 Raw data (/proc/950/stat): 950 (minisat+_script) S 949 950 27660 0 -1 0 288 239 0 0 0 1 0 0 20 0 1 0 1770426787 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/950/statm): 531 226 485 147 0 384 0 [pid=950] vsize: 2124 Raw data (/proc/954/stat): 954 (minisat+_64-bit) R 950 950 27660 0 -1 0 37234 0 0 0 102374 273 0 0 25 0 1 0 1770426792 153767936 37221 4294967295 134512640 135094434 3221224448 3221223104 134558022 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/954/statm): 37541 37221 145 145 0 37396 0 [pid=954] vsize: 150164 Current children cumulated CPU time (s) 1026.48 Current children cumulated vsize (Kb) 152288 [startup+1040.11 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 954 Raw data (/proc/950/stat): 950 (minisat+_script) S 949 950 27660 0 -1 0 288 239 0 0 0 1 0 0 20 0 1 0 1770426787 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/950/statm): 531 226 485 147 0 384 0 [pid=950] vsize: 2124 Raw data (/proc/954/stat): 954 (minisat+_64-bit) R 950 950 27660 0 -1 0 37234 0 0 0 103374 273 0 0 25 0 1 0 1770426792 153767936 37221 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/954/statm): 37541 37221 145 145 0 37396 0 [pid=954] vsize: 150164 Current children cumulated CPU time (s) 1036.48 Current children cumulated vsize (Kb) 152288 [startup+1050.11 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 954 Raw data (/proc/950/stat): 950 (minisat+_script) S 949 950 27660 0 -1 0 288 239 0 0 0 1 0 0 20 0 1 0 1770426787 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/950/statm): 531 226 485 147 0 384 0 [pid=950] vsize: 2124 Raw data (/proc/954/stat): 954 (minisat+_64-bit) R 950 950 27660 0 -1 0 37234 0 0 0 104374 273 0 0 25 0 1 0 1770426792 153767936 37221 4294967295 134512640 135094434 3221224448 3221223104 134558176 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/954/statm): 37541 37221 145 145 0 37396 0 [pid=954] vsize: 150164 Current children cumulated CPU time (s) 1046.48 Current children cumulated vsize (Kb) 152288 [startup+1060.11 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 954 Raw data (/proc/950/stat): 950 (minisat+_script) S 949 950 27660 0 -1 0 288 239 0 0 0 1 0 0 20 0 1 0 1770426787 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/950/statm): 531 226 485 147 0 384 0 [pid=950] vsize: 2124 Raw data (/proc/954/stat): 954 (minisat+_64-bit) R 950 950 27660 0 -1 0 37234 0 0 0 105374 273 0 0 25 0 1 0 1770426792 153767936 37221 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/954/statm): 37541 37221 145 145 0 37396 0 [pid=954] vsize: 150164 Current children cumulated CPU time (s) 1056.48 Current children cumulated vsize (Kb) 152288 [startup+1070.11 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 954 Raw data (/proc/950/stat): 950 (minisat+_script) S 949 950 27660 0 -1 0 288 239 0 0 0 1 0 0 20 0 1 0 1770426787 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/950/statm): 531 226 485 147 0 384 0 [pid=950] vsize: 2124 Raw data (/proc/954/stat): 954 (minisat+_64-bit) R 950 950 27660 0 -1 0 37234 0 0 0 106375 273 0 0 25 0 1 0 1770426792 153767936 37221 4294967295 134512640 135094434 3221224448 3221223104 134558009 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/954/statm): 37541 37221 145 145 0 37396 0 [pid=954] vsize: 150164 Current children cumulated CPU time (s) 1066.49 Current children cumulated vsize (Kb) 152288 [startup+1080.11 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 954 Raw data (/proc/950/stat): 950 (minisat+_script) S 949 950 27660 0 -1 0 288 239 0 0 0 1 0 0 20 0 1 0 1770426787 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/950/statm): 531 226 485 147 0 384 0 [pid=950] vsize: 2124 Raw data (/proc/954/stat): 954 (minisat+_64-bit) R 950 950 27660 0 -1 0 37234 0 0 0 107375 273 0 0 25 0 1 0 1770426792 153767936 37221 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/954/statm): 37541 37221 145 145 0 37396 0 [pid=954] vsize: 150164 Current children cumulated CPU time (s) 1076.49 Current children cumulated vsize (Kb) 152288 [startup+1090.11 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 954 Raw data (/proc/950/stat): 950 (minisat+_script) S 949 950 27660 0 -1 0 288 239 0 0 0 1 0 0 20 0 1 0 1770426787 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/950/statm): 531 226 485 147 0 384 0 [pid=950] vsize: 2124 Raw data (/proc/954/stat): 954 (minisat+_64-bit) R 950 950 27660 0 -1 0 37234 0 0 0 108375 273 0 0 25 0 1 0 1770426792 153767936 37221 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/954/statm): 37541 37221 145 145 0 37396 0 [pid=954] vsize: 150164 Current children cumulated CPU time (s) 1086.49 Current children cumulated vsize (Kb) 152288 [startup+1100.11 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 954 Raw data (/proc/950/stat): 950 (minisat+_script) S 949 950 27660 0 -1 0 288 239 0 0 0 1 0 0 20 0 1 0 1770426787 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/950/statm): 531 226 485 147 0 384 0 [pid=950] vsize: 2124 Raw data (/proc/954/stat): 954 (minisat+_64-bit) R 950 950 27660 0 -1 0 37234 0 0 0 109375 273 0 0 25 0 1 0 1770426792 153767936 37221 4294967295 134512640 135094434 3221224448 3221223104 134557988 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/954/statm): 37541 37221 145 145 0 37396 0 [pid=954] vsize: 150164 Current children cumulated CPU time (s) 1096.49 Current children cumulated vsize (Kb) 152288 [startup+1110.11 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 954 Raw data (/proc/950/stat): 950 (minisat+_script) S 949 950 27660 0 -1 0 288 239 0 0 0 1 0 0 20 0 1 0 1770426787 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/950/statm): 531 226 485 147 0 384 0 [pid=950] vsize: 2124 Raw data (/proc/954/stat): 954 (minisat+_64-bit) R 950 950 27660 0 -1 0 37234 0 0 0 110376 273 0 0 25 0 1 0 1770426792 153767936 37221 4294967295 134512640 135094434 3221224448 3221223104 134558249 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/954/statm): 37541 37221 145 145 0 37396 0 [pid=954] vsize: 150164 Current children cumulated CPU time (s) 1106.5 Current children cumulated vsize (Kb) 152288 [startup+1120.11 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 954 Raw data (/proc/950/stat): 950 (minisat+_script) S 949 950 27660 0 -1 0 288 239 0 0 0 1 0 0 20 0 1 0 1770426787 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/950/statm): 531 226 485 147 0 384 0 [pid=950] vsize: 2124 Raw data (/proc/954/stat): 954 (minisat+_64-bit) R 950 950 27660 0 -1 0 37234 0 0 0 111376 273 0 0 25 0 1 0 1770426792 153767936 37221 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/954/statm): 37541 37221 145 145 0 37396 0 [pid=954] vsize: 150164 Current children cumulated CPU time (s) 1116.5 Current children cumulated vsize (Kb) 152288 [startup+1130.11 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 954 Raw data (/proc/950/stat): 950 (minisat+_script) S 949 950 27660 0 -1 0 288 239 0 0 0 1 0 0 20 0 1 0 1770426787 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/950/statm): 531 226 485 147 0 384 0 [pid=950] vsize: 2124 Raw data (/proc/954/stat): 954 (minisat+_64-bit) R 950 950 27660 0 -1 0 37234 0 0 0 112376 273 0 0 25 0 1 0 1770426792 153767936 37221 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/954/statm): 37541 37221 145 145 0 37396 0 [pid=954] vsize: 150164 Current children cumulated CPU time (s) 1126.5 Current children cumulated vsize (Kb) 152288 [startup+1140.11 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 954 Raw data (/proc/950/stat): 950 (minisat+_script) S 949 950 27660 0 -1 0 288 239 0 0 0 1 0 0 20 0 1 0 1770426787 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/950/statm): 531 226 485 147 0 384 0 [pid=950] vsize: 2124 Raw data (/proc/954/stat): 954 (minisat+_64-bit) R 950 950 27660 0 -1 0 37234 0 0 0 113376 273 0 0 25 0 1 0 1770426792 153767936 37221 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/954/statm): 37541 37221 145 145 0 37396 0 [pid=954] vsize: 150164 Current children cumulated CPU time (s) 1136.5 Current children cumulated vsize (Kb) 152288 [startup+1150.11 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 954 Raw data (/proc/950/stat): 950 (minisat+_script) S 949 950 27660 0 -1 0 288 239 0 0 0 1 0 0 20 0 1 0 1770426787 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/950/statm): 531 226 485 147 0 384 0 [pid=950] vsize: 2124 Raw data (/proc/954/stat): 954 (minisat+_64-bit) R 950 950 27660 0 -1 0 37234 0 0 0 114377 273 0 0 25 0 1 0 1770426792 153767936 37221 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/954/statm): 37541 37221 145 145 0 37396 0 [pid=954] vsize: 150164 Current children cumulated CPU time (s) 1146.51 Current children cumulated vsize (Kb) 152288 [startup+1160.11 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 954 Raw data (/proc/950/stat): 950 (minisat+_script) S 949 950 27660 0 -1 0 288 239 0 0 0 1 0 0 20 0 1 0 1770426787 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/950/statm): 531 226 485 147 0 384 0 [pid=950] vsize: 2124 Raw data (/proc/954/stat): 954 (minisat+_64-bit) R 950 950 27660 0 -1 0 37292 0 0 0 115376 274 0 0 25 0 1 0 1770426792 154005504 37279 4294967295 134512640 135094434 3221224448 3221223104 134558016 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/954/statm): 37599 37279 145 145 0 37454 0 [pid=954] vsize: 150396 Current children cumulated CPU time (s) 1156.51 Current children cumulated vsize (Kb) 152520 [startup+1170.12 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 954 Raw data (/proc/950/stat): 950 (minisat+_script) S 949 950 27660 0 -1 0 288 239 0 0 0 1 0 0 20 0 1 0 1770426787 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/950/statm): 531 226 485 147 0 384 0 [pid=950] vsize: 2124 Raw data (/proc/954/stat): 954 (minisat+_64-bit) R 950 950 27660 0 -1 0 37667 0 0 0 116368 278 0 0 25 0 1 0 1770426792 155541504 37654 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/954/statm): 37974 37654 145 145 0 37829 0 [pid=954] vsize: 151896 Current children cumulated CPU time (s) 1166.47 Current children cumulated vsize (Kb) 154020 [startup+1180.12 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 954 Raw data (/proc/950/stat): 950 (minisat+_script) S 949 950 27660 0 -1 0 288 239 0 0 0 1 0 0 20 0 1 0 1770426787 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/950/statm): 531 226 485 147 0 384 0 [pid=950] vsize: 2124 Raw data (/proc/954/stat): 954 (minisat+_64-bit) R 950 950 27660 0 -1 0 38129 0 0 0 117361 282 0 0 25 0 1 0 1770426792 157433856 38116 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/954/statm): 38436 38116 145 145 0 38291 0 [pid=954] vsize: 153744 Current children cumulated CPU time (s) 1176.44 Current children cumulated vsize (Kb) 155868 [startup+1190.12 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 954 Raw data (/proc/950/stat): 950 (minisat+_script) S 949 950 27660 0 -1 0 288 239 0 0 0 1 0 0 20 0 1 0 1770426787 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/950/statm): 531 226 485 147 0 384 0 [pid=950] vsize: 2124 Raw data (/proc/954/stat): 954 (minisat+_64-bit) R 950 950 27660 0 -1 0 38554 0 0 0 118352 285 0 0 25 0 1 0 1770426792 159174656 38541 4294967295 134512640 135094434 3221224448 3221223104 134558213 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/954/statm): 38861 38541 145 145 0 38716 0 [pid=954] vsize: 155444 Current children cumulated CPU time (s) 1186.38 Current children cumulated vsize (Kb) 157568 [startup+1200.12 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 954 Raw data (/proc/950/stat): 950 (minisat+_script) S 949 950 27660 0 -1 0 288 239 0 0 0 1 0 0 20 0 1 0 1770426787 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/950/statm): 531 226 485 147 0 384 0 [pid=950] vsize: 2124 Raw data (/proc/954/stat): 954 (minisat+_64-bit) R 950 950 27660 0 -1 0 39021 0 0 0 119346 287 0 0 25 0 1 0 1770426792 161091584 39008 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/954/statm): 39329 39008 145 145 0 39184 0 [pid=954] vsize: 157316 Current children cumulated CPU time (s) 1196.34 Current children cumulated vsize (Kb) 159440 [startup+1210.12 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 954 Raw data (/proc/950/stat): 950 (minisat+_script) S 949 950 27660 0 -1 0 288 239 0 0 0 1 0 0 20 0 1 0 1770426787 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/950/statm): 531 226 485 147 0 384 0 [pid=950] vsize: 2124 Raw data (/proc/954/stat): 954 (minisat+_64-bit) R 950 950 27660 0 -1 0 39447 0 0 0 120338 290 0 0 25 0 1 0 1770426792 162840576 39434 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/954/statm): 39756 39434 145 145 0 39611 0 [pid=954] vsize: 159024 Current children cumulated CPU time (s) 1206.29 Current children cumulated vsize (Kb) 161148 Maximum CPU time exceeded: sending SIGTERM then SIGKILL [startup+1210.12 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 954 Raw data (/proc/950/stat): 950 (minisat+_script) S 949 950 27660 0 -1 0 288 239 0 0 0 1 0 0 20 0 1 0 1770426787 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/950/statm): 531 226 485 147 0 384 0 [pid=950] vsize: 2124 Raw data (/proc/954/stat): 954 (minisat+_64-bit) R 950 950 27660 0 -1 0 39447 0 0 0 120338 290 0 0 25 0 1 0 1770426792 162840576 39434 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/954/statm): 39756 39434 145 145 0 39611 0 [pid=954] vsize: 159024 Current children cumulated CPU time (s) 1206.29 Current children cumulated vsize (Kb) 161148 Sending SIGTERM to -950 Sleeping 2 seconds One traced child (pid=950) ended because it received signal 15 (SIGTERM) One traced child (pid=954) exited with status: 0 All traced children have exited ! Game is over. Child status: 0 Real time (s): 1210.2 CPU time (s): 1206.37 CPU user time (s): 1203.39 CPU system time (s): 2.98255 CPU usage (%): 99.6841 Max. virtual memory (cumulated for all children) (Kb): 161148
ERROR: no interpretation found !