Name | web/www.nlsde.buaa.edu.cn/~kexu/benchmarks/frb53-24-opb/normalized-frb53-24-1.opb |
MD5SUM | 20fc65112f36a5d10cc9eaa82c0beb63 |
Bench Category | optimization, small integers (OPTSMALLINT) |
Has Objective Function | YES |
Satisfiable | YES |
(Un)Satisfiability was proved | YES |
Best value of the objective function | -39 |
Optimality of the best value was proved | NO |
Number of terms in the objective function | 1272 |
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 | 1272 |
Number of bits of the sum of numbers in the objective function | 11 |
Biggest number in a constraint | 1 |
Number of bits of the biggest number in a constraint | 1 |
Biggest sum of numbers in a constraint | 1272 |
Number of bits of the biggest sum of numbers | 11 |
Best result obtained on this benchmark | SAT |
Best CPU time to get the best result obtained on this benchmark | 1207.03 |
Number of variables | 1272 |
Total number of constraints | 94227 |
Number of constraints which are clauses | 94227 |
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 | 2 |
LAUNCH ON wulflinc9 THE 2005-09-18 18:51:40 (client local time) PB2005-SCRIPT v4.0 MARKUPS: idlaunch=2710 boxname=wulflinc9 idbench=366 idsolver=3 numberseed=0 MD5SUM SOLVER: MD5SUM BENCH: 20fc65112f36a5d10cc9eaa82c0beb63 /oldhome/oroussel/tmp/wulflinc9/normalized-frb53-24-1.opb REAL COMMAND: minisat+_script /oldhome/oroussel/tmp/wulflinc9/normalized-frb53-24-1.opb IDLAUNCH: 2710 /proc/cpuinfo: processor : 0 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 2 cpu MHz : 451.242 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.242 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: 923516 kB Buffers: 30512 kB Cached: 54056 kB SwapCached: 1044 kB Active: 49728 kB Inactive: 37564 kB HighTotal: 131008 kB HighFree: 73332 kB LowTotal: 903652 kB LowFree: 850184 kB SwapTotal: 2097136 kB SwapFree: 2095568 kB Dirty: 28 kB Writeback: 0 kB Mapped: 5660 kB Slab: 18028 kB Committed_AS: 64168 kB PageTables: 328 kB VmallocTotal: 114680 kB VmallocUsed: 1364 kB VmallocChunk: 113256 kB JOB ENDED THE 2005-09-18 19:11:51 (client local time) WITH STATUS 10 IN 1207.61 SECONDS stats: 2710 7 1207.61 10
c Parsing PB file... c Converting 94227 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 | 94227 188454 | 31409 0 0 nan | 0.000 % | c ============================================================================== c [1mFound solution: -36[0m c ---[ 0]---> Sorter-cost:70300 Base: c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 0 | 169273 364509 | 56424 0 0 nan | 0.000 % | c | 100 | 168899 363733 | 62066 65 591 9.1 | 0.407 % | c | 250 | 168502 362906 | 68273 198 1311 6.6 | 0.828 % | c | 475 | 167076 359832 | 75100 351 2932 8.4 | 2.494 % | c | 812 | 165133 355593 | 82610 631 5067 8.0 | 4.688 % | c | 1319 | 162313 349369 | 90871 972 8957 9.2 | 8.080 % | c | 2078 | 157982 339700 | 99958 1468 15263 10.4 | 13.235 % | c ============================================================================== c [1mFound solution: -39[0m c ---[ 0]---> Sorter-cost: 0 Base: c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 2296 | 157388 338635 | 52462 1645 17452 10.6 | 13.235 % | c | 2397 | 157059 337878 | 57708 1732 17985 10.4 | 14.608 % | c | 2548 | 155840 335129 | 63479 1821 18984 10.4 | 16.160 % | c | 2773 | 154165 331306 | 69826 1966 20681 10.5 | 18.177 % | c | 3110 | 151458 325155 | 76809 2174 23582 10.8 | 21.604 % | c | 3616 | 147626 316455 | 84490 2526 28129 11.1 | 26.258 % | c | 4375 | 143472 307009 | 92939 3028 34893 11.5 | 31.480 % | c | 5514 | 137035 292201 | 102233 3700 43332 11.7 | 39.456 % | c | 7223 | 129643 274879 | 112456 4787 55808 11.7 | 48.879 % | c | 9785 | 121178 254842 | 123702 6238 75388 12.1 | 60.010 % | c | 13629 | 111810 232544 | 136072 8363 107856 12.9 | 72.370 % | c ============================================================================== c [1mFound solution: -40[0m c ---[ 0]---> Sorter-cost: 0 Base: c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 13714 | 111791 232457 | 37263 8438 110430 13.1 | 72.370 % | c | 13815 | 111736 232336 | 40989 8517 111608 13.1 | 72.463 % | c | 13965 | 111449 231624 | 45088 8613 112090 13.0 | 72.865 % | c | 14191 | 110875 230219 | 49597 8726 114161 13.1 | 73.663 % | c | 14528 | 110330 228918 | 54556 8862 116391 13.1 | 74.395 % | c | 15034 | 109915 227905 | 60012 9207 123608 13.4 | 74.966 % | c ============================================================================== c [1mFound solution: -41[0m c ---[ 0]---> Sorter-cost: 0 Base: c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 15297 | 109425 226747 | 36475 9363 132070 14.1 | 74.966 % | c | 15397 | 108928 225548 | 40122 9368 131994 14.1 | 76.327 % | c | 15547 | 108861 225391 | 44134 9505 134463 14.1 | 76.414 % | c | 15772 | 108187 223757 | 48548 9615 136618 14.2 | 77.343 % | c | 16110 | 108184 223750 | 53403 9952 143364 14.4 | 77.347 % | c | 16616 | 107846 222930 | 58743 10285 150811 14.7 | 77.809 % | c | 17375 | 107492 222096 | 64617 10880 162733 15.0 | 78.273 % | c | 18516 | 106409 219476 | 71079 11485 183931 16.0 | 79.751 % | c | 20224 | 105563 217441 | 78187 12695 231153 18.2 | 80.890 % | c ============================================================================== c [1mFound solution: -42[0m c ---[ 0]---> Sorter-cost: 0 Base: c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 22454 | 104461 214676 | 34820 14284 295984 20.7 | 80.890 % | c | 22554 | 104247 214159 | 38302 14343 296650 20.7 | 82.669 % | c | 22704 | 104230 214116 | 42132 14478 302277 20.9 | 82.695 % | c | 22929 | 104077 213747 | 46345 14609 305744 20.9 | 82.903 % | c | 23266 | 103810 213088 | 50979 14674 310610 21.2 | 83.278 % | c | 23772 | 103661 212727 | 56077 15056 324943 21.6 | 83.483 % | c | 24531 | 103661 212727 | 61685 15815 342397 21.7 | 83.483 % | c ============================================================================== c [1mFound solution: -43[0m c ---[ 0]---> Sorter-cost: 0 Base: c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 24866 | 103578 212555 | 34526 15940 354982 22.3 | 83.483 % | c | 24966 | 103452 212229 | 37978 15957 356178 22.3 | 83.832 % | c | 25116 | 103157 211504 | 41776 15858 355829 22.4 | 84.245 % | c | 25342 | 103098 211357 | 45954 15982 361200 22.6 | 84.328 % | c | 25679 | 103060 211263 | 50549 16275 374557 23.0 | 84.383 % | c | 26186 | 103044 211225 | 55604 16717 403210 24.1 | 84.404 % | c | 26946 | 102964 211037 | 61164 17402 448444 25.8 | 84.509 % | c | 28085 | 102796 210627 | 67281 18302 513844 28.1 | 84.741 % | c | 29794 | 102287 209397 | 74009 19277 595883 30.9 | 85.430 % | c ============================================================================== c [1mFound solution: -44[0m c ---[ 0]---> Sorter-cost: 0 Base: c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 30805 | 102185 209122 | 34061 19877 649107 32.7 | 85.430 % | c | 30905 | 102181 209112 | 37467 19960 650513 32.6 | 85.578 % | c | 31055 | 102181 209112 | 41213 20110 656361 32.6 | 85.578 % | c | 31280 | 102181 209112 | 45335 20335 662267 32.6 | 85.578 % | c | 31617 | 102139 209012 | 49868 20565 689479 33.5 | 85.635 % | c | 32123 | 102135 209002 | 54855 21042 708226 33.7 | 85.640 % | c | 32883 | 102044 208779 | 60341 21692 763522 35.2 | 85.765 % | c | 34023 | 101908 208436 | 66375 22590 857752 38.0 | 85.961 % | c | 35731 | 101761 208078 | 73012 24035 977376 40.7 | 86.166 % | c | 38294 | 101248 206822 | 80314 25704 1211706 47.1 | 86.880 % | c ============================================================================== c [1mFound solution: -45[0m c ---[ 0]---> Sorter-cost: 0 Base: c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 40062 | 101189 206683 | 33729 27299 1370590 50.2 | 86.880 % | c | 40164 | 101153 206593 | 37101 27290 1368576 50.1 | 87.022 % | c | 40314 | 101153 206593 | 40812 27440 1373157 50.0 | 87.022 % | c | 40539 | 101153 206593 | 44893 27665 1390604 50.3 | 87.022 % | c | 40877 | 101147 206579 | 49382 27982 1417890 50.7 | 87.029 % | c | 41383 | 101089 206432 | 54320 28284 1476102 52.2 | 87.111 % | c | 42142 | 101046 206333 | 59752 28842 1548069 53.7 | 87.164 % | c | 43281 | 101030 206295 | 65728 29940 1653263 55.2 | 87.185 % | c ============================================================================== c [1mFound solution: -46[0m c ---[ 0]---> Sorter-cost: 0 Base: c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 43660 | 101019 206233 | 33673 30108 1656622 55.0 | 87.185 % | c | 43762 | 100999 206179 | 37040 30194 1661991 55.0 | 87.234 % | c | 43912 | 100999 206179 | 40744 30344 1674049 55.2 | 87.234 % | c | 44138 | 100999 206179 | 44818 30570 1677140 54.9 | 87.234 % | c | 44476 | 100999 206179 | 49300 30908 1697757 54.9 | 87.234 % | c | 44983 | 100999 206179 | 54230 31415 1748048 55.6 | 87.234 % | c | 45742 | 100961 206093 | 59653 32036 1808118 56.4 | 87.281 % | c | 46881 | 100961 206093 | 65619 33175 1962362 59.2 | 87.281 % | c | 48589 | 100961 206093 | 72181 34883 2133447 61.2 | 87.281 % | c | 51151 | 100916 205984 | 79399 37289 2446159 65.6 | 87.343 % | c | 54995 | 100889 205925 | 87339 40682 2985421 73.4 | 87.374 % | c | 60761 | 100889 205925 | 96072 46448 3854427 83.0 | 87.374 % | c ============================================================================== c [1mFound solution: -47[0m c ---[ 0]---> Sorter-cost: 0 Base: c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 65334 | 100853 205854 | 33617 50820 4571720 90.0 | 87.374 % | c | 65434 | 100853 205854 | 36978 50920 4575895 89.9 | 87.450 % | c | 65584 | 100853 205854 | 40676 51070 4590180 89.9 | 87.450 % | c | 65809 | 100853 205854 | 44744 51295 4602588 89.7 | 87.450 % | c | 66148 | 100853 205854 | 49218 51634 4624017 89.6 | 87.450 % | c | 66654 | 100853 205854 | 54140 52140 4670967 89.6 | 87.450 % | c | 67414 | 100814 205757 | 59554 52773 4715984 89.4 | 87.506 % | c | 68553 | 100814 205757 | 65510 53912 4839522 89.8 | 87.506 % | c | 70261 | 100814 205757 | 72061 55620 5031215 90.5 | 87.506 % | c | 72824 | 100814 205757 | 79267 58183 5325863 91.5 | 87.506 % | c | 76668 | 100814 205757 | 87193 62027 5737838 92.5 | 87.506 % | c | 82434 | 100720 205535 | 95913 67266 6413842 95.4 | 87.630 % | c | 91084 | 100718 205529 | 105504 75912 7268264 95.7 | 87.634 % | c ============================================================================== c [1mFound solution: -48[0m c ---[ 0]---> Sorter-cost: 0 Base: c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 94590 | 100693 205448 | 33564 79088 7509816 95.0 | 87.634 % | c | 94690 | 100693 205448 | 36920 19014 1203514 63.3 | 87.669 % | c | 94840 | 100693 205448 | 40612 19164 1215224 63.4 | 87.669 % | c | 95066 | 100610 205251 | 44673 19386 1226784 63.3 | 87.776 % | c | 95404 | 100605 205238 | 49141 19716 1247119 63.3 | 87.784 % | c | 95910 | 100605 205238 | 54055 20222 1293892 64.0 | 87.784 % | c | 96671 | 100605 205238 | 59460 20983 1362659 64.9 | 87.784 % | c | 97810 | 100602 205231 | 65406 22119 1452373 65.7 | 87.788 % | c | 99519 | 100602 205231 | 71947 23828 1570680 65.9 | 87.788 % | c | 102082 | 100602 205231 | 79142 26391 1796590 68.1 | 87.788 % | c | 105926 | 100524 205033 | 87056 30221 2254790 74.6 | 87.904 % | c | 111693 | 100513 205008 | 95762 35977 2865103 79.6 | 87.917 % | c | 120342 | 100496 204969 | 105338 44621 3803842 85.2 | 87.939 % | c | 133316 | 100496 204969 | 115872 57595 5193648 90.2 | 87.939 % | c | 152777 | 100477 204922 | 127459 77043 7291374 94.6 | 87.966 % | c | 181969 | 100467 204900 | 140205 106227 10898164 102.6 | 87.978 % | c | 225758 | 100436 204820 | 154225 149983 15472459 103.2 | 88.024 % | c | 291443 | 100430 204806 | 169648 36460 2449536 67.2 | 88.032 % | c c *** TERMINATED *** s SATISFIABLE v -C1272 -C1271 -C1270 -C1269 -C1268 -C1267 -C1266 -C1265 -C1264 -C1263 -C1262 -C1261 -C1260 -C1259 -C1258 -C1257 -C1256 -C1255 -C1254 -C1253 -C1252 -C1251 C1250 -C1249 -C1248 -C1247 C1246 -C1245 -C1244 -C1243 -C1242 -C1241 -C1240 -C1239 -C1238 -C1237 -C1236 -C1235 -C1234 -C1233 -C1232 -C1231 -C1230 -C1229 -C1228 -C1227 -C1226 -C1225 -C1224 -C1223 -C1222 -C1221 -C1220 -C1219 -C1218 -C1217 -C1216 -C1215 -C1214 -C1213 -C1212 -C1211 -C1210 -C1209 -C1208 C1207 -C1206 -C1205 -C1204 -C1203 -C1202 -C1201 -C1200 -C1199 -C1198 -C1197 -C1196 -C1195 -C1194 -C1193 -C1192 -C1191 -C1190 -C1189 -C1188 -C1187 -C1186 -C1185 -C1184 -C1183 -C1182 -C1181 -C1180 -C1179 -C1178 -C1177 -C1176 -C1175 -C1174 -C1173 -C1172 -C1171 -C1170 -C1169 C1168 -C1167 -C1166 -C1165 -C1164 -C1163 -C1162 -C1161 -C1160 -C1159 -C1158 -C1157 -C1156 -C1155 -C1154 -C1153 -C1152 -C1151 -C1150 -C1149 -C1148 -C1147 -C1146 -C1145 -C1144 -C1143 -C1142 C1141 -C1140 -C1139 -C1138 -C1137 -C1136 -C1135 -C1134 -C1133 -C1132 -C1131 -C1130 -C1129 -C1128 -C1127 -C1126 -C1125 -C1124 -C1123 -C1122 C1121 -C1120 -C1119 -C1118 -C1117 -C1116 -C1115 -C1114 -C1113 -C1112 -C1111 -C1110 -C1109 -C1108 -C1107 -C1106 -C1105 -C1104 -C1103 C1102 -C1101 -C1100 -C1099 -C1098 -C1097 -C1096 -C1095 -C1094 -C1093 -C1092 -C1091 -C1090 -C1089 -C1088 -C1087 -C1086 -C1085 -C1084 -C1083 -C1082 -C1081 -C1080 -C1079 -C1078 -C1077 -C1076 -C1075 -C1074 -C1073 -C1072 -C1071 -C1070 -C1069 -C1068 -C1067 -C1066 -C1065 -C1064 -C1063 -C1062 -C1061 -C1060 -C1059 -C1058 C1057 -C1056 -C1055 -C1054 -C1053 -C1052 -C1051 -C1050 C1049 -C1048 -C1047 -C1046 -C1045 -C1044 -C1043 -C1042 -C1041 -C1040 -C1039 -C1038 -C1037 -C1036 -C1035 -C1034 -C1033 -C1032 -C1031 -C1030 -C1029 C1028 -C1027 -C1026 -C1025 -C1024 -C1023 -C1022 -C1021 -C1020 -C1019 -C1018 -C1017 -C1016 -C1015 -C1014 -C1013 -C1012 -C1011 -C1010 -C1009 -C1008 -C1007 -C1006 -C1005 -C1004 -C1003 -C1002 -C1001 -C1000 -C999 -C998 -C997 -C996 -C995 -C994 -C993 C992 -C991 -C990 -C989 -C988 -C987 -C986 -C985 -C984 -C983 -C982 -C981 -C980 -C979 -C978 -C977 -C976 -C975 -C974 -C973 -C972 -C971 -C970 -C969 C968 -C967 -C966 -C965 -C964 -C963 -C962 -C961 -C960 -C959 -C958 -C957 -C956 -C955 -C954 -C953 -C952 C951 -C950 -C949 -C948 -C947 -C946 -C945 -C944 -C943 -C942 -C941 -C940 -C939 -C938 -C937 -C936 -C935 -C934 C933 -C932 -C931 -C930 -C929 -C928 -C927 -C926 -C925 -C924 -C923 -C922 -C921 -C920 -C919 -C918 -C917 -C916 -C915 -C914 -C913 -C912 -C911 -C910 C909 -C908 -C907 -C906 -C905 -C904 -C903 -C902 -C901 -C900 -C899 -C898 -C897 -C896 -C895 -C894 -C893 -C892 -C891 -C890 -C889 -C888 -C887 -C886 -C885 -C884 -C883 -C882 -C881 -C880 -C879 -C878 -C877 -C876 -C875 -C874 -C873 -C872 -C871 -C870 -C869 -C868 C867 -C866 -C865 -C864 -C863 -C862 -C861 -C860 -C859 -C858 C857 -C856 -C855 -C854 -C853 -C852 -C851 -C850 -C849 -C848 -C847 -C846 -C845 -C844 -C843 -C842 -C841 -C840 -C839 -C838 -C837 -C836 -C835 -C834 -C833 -C832 -C831 -C830 -C829 -C828 -C827 -C826 -C825 C824 -C823 -C822 -C821 -C820 -C819 -C818 -C817 -C816 -C815 -C814 -C813 -C812 -C811 -C810 -C809 -C808 -C807 -C806 -C805 -C804 -C803 -C802 -C801 -C800 -C799 -C798 -C797 -C796 C795 -C794 -C793 -C792 -C791 -C790 -C789 -C788 -C787 -C786 -C785 -C784 -C783 -C782 -C781 -C780 -C779 -C778 C777 -C776 -C775 -C774 -C773 -C772 -C771 -C770 -C769 -C768 -C767 -C766 -C765 -C764 -C763 -C762 -C761 -C760 -C759 -C758 -C757 C756 -C755 -C754 -C753 -C752 -C751 -C750 -C749 -C748 -C747 -C746 -C745 -C744 -C743 -C742 -C741 -C740 -C739 C738 -C737 -C736 -C735 -C734 -C733 -C732 -C731 -C730 -C729 -C728 -C727 -C726 -C725 -C724 -C723 -C722 -C721 -C720 -C719 -C718 -C717 -C716 -C715 -C714 -C713 -C712 -C711 -C710 -C709 -C708 -C707 -C706 -C705 -C704 -C703 -C702 -C701 -C700 -C699 -C698 -C697 -C696 -C695 -C694 -C693 -C692 -C691 -C690 -C689 -C688 -C687 -C686 -C685 -C684 -C683 -C682 -C681 -C680 C679 -C678 -C677 -C676 -C675 -C674 -C673 -C672 -C671 -C670 -C669 -C668 -C667 -C666 -C665 C664 -C663 -C662 -C661 -C660 -C659 -C658 -C657 -C656 -C655 -C654 -C653 -C652 -C651 -C650 -C649 -C648 -C647 -C646 -C645 -C644 -C643 -C642 -C641 -C640 -C639 -C6
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/8492/stat): 8492 (minisat+_script) R 8491 8492 30740 0 -1 0 19 0 0 0 0 0 0 0 22 0 1 0 1785328358 712704 3 4294967295 134512640 135087896 3221224512 3221224512 1073744960 0 0 5 0 0 0 0 17 1 0 0 Raw data (/proc/8492/statm): 174 3 169 147 0 27 0 [pid=8492] 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=8493 New process pid=8494 New process pid=8495 execve syscall for /bin/sed executable One traced child (pid=8494) 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=8495) exited with status: 0 One traced child (pid=8493) exited with status: 0 New process pid=8496 execve syscall for /oldhome/oroussel/solvers/minisat+_64-bit_static executable open syscall for file /dev/null open syscall for file /oldhome/oroussel/tmp/wulflinc9/normalized-frb53-24-1.opb [startup+10.0036 s] Raw data (loadavg): 0.93 0.95 0.91 2/57 8496 Raw data (/proc/8492/stat): 8492 (minisat+_script) S 8491 8492 30740 0 -1 0 289 239 0 0 0 0 0 1 18 0 1 0 1785328358 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/8492/statm): 531 226 485 147 0 384 0 [pid=8492] vsize: 2124 Raw data (/proc/8496/stat): 8496 (minisat+_64-bit) R 8492 8492 30740 0 -1 0 5916 0 0 0 953 25 0 0 25 0 1 0 1785328363 25022464 5903 4294967295 134512640 135094434 3221224448 3221223108 134553446 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/8496/statm): 6109 5903 145 145 0 5964 0 [pid=8496] vsize: 24436 Current children cumulated CPU time (s) 9.79 Current children cumulated vsize (Kb) 26560 [startup+20.0044 s] Raw data (loadavg): 0.94 0.96 0.91 2/57 8496 Raw data (/proc/8492/stat): 8492 (minisat+_script) S 8491 8492 30740 0 -1 0 289 239 0 0 0 0 0 1 18 0 1 0 1785328358 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/8492/statm): 531 226 485 147 0 384 0 [pid=8492] vsize: 2124 Raw data (/proc/8496/stat): 8496 (minisat+_64-bit) R 8492 8492 30740 0 -1 0 5916 0 0 0 1953 25 0 0 25 0 1 0 1785328363 25022464 5903 4294967295 134512640 135094434 3221224448 3221223108 134553446 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/8496/statm): 6109 5903 145 145 0 5964 0 [pid=8496] vsize: 24436 Current children cumulated CPU time (s) 19.79 Current children cumulated vsize (Kb) 26560 [startup+30.0062 s] Raw data (loadavg): 0.95 0.96 0.91 2/57 8496 Raw data (/proc/8492/stat): 8492 (minisat+_script) S 8491 8492 30740 0 -1 0 289 239 0 0 0 0 0 1 18 0 1 0 1785328358 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/8492/statm): 531 226 485 147 0 384 0 [pid=8492] vsize: 2124 Raw data (/proc/8496/stat): 8496 (minisat+_64-bit) R 8492 8492 30740 0 -1 0 5997 0 0 0 2952 26 0 0 25 0 1 0 1785328363 25600000 5984 4294967295 134512640 135094434 3221224448 3221223108 134553501 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/8496/statm): 6250 5984 145 145 0 6105 0 [pid=8496] vsize: 25000 Current children cumulated CPU time (s) 29.79 Current children cumulated vsize (Kb) 27124 [startup+40.0069 s] Raw data (loadavg): 0.95 0.96 0.91 2/57 8496 Raw data (/proc/8492/stat): 8492 (minisat+_script) S 8491 8492 30740 0 -1 0 289 239 0 0 0 0 0 1 18 0 1 0 1785328358 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/8492/statm): 531 226 485 147 0 384 0 [pid=8492] vsize: 2124 Raw data (/proc/8496/stat): 8496 (minisat+_64-bit) R 8492 8492 30740 0 -1 0 5997 0 0 0 3952 26 0 0 25 0 1 0 1785328363 25600000 5984 4294967295 134512640 135094434 3221224448 3221223120 134553523 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/8496/statm): 6250 5984 145 145 0 6105 0 [pid=8496] vsize: 25000 Current children cumulated CPU time (s) 39.79 Current children cumulated vsize (Kb) 27124 [startup+50.0077 s] Raw data (loadavg): 0.96 0.96 0.91 2/57 8496 Raw data (/proc/8492/stat): 8492 (minisat+_script) S 8491 8492 30740 0 -1 0 289 239 0 0 0 0 0 1 18 0 1 0 1785328358 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/8492/statm): 531 226 485 147 0 384 0 [pid=8492] vsize: 2124 Raw data (/proc/8496/stat): 8496 (minisat+_64-bit) R 8492 8492 30740 0 -1 0 5997 0 0 0 4951 27 0 0 25 0 1 0 1785328363 25600000 5984 4294967295 134512640 135094434 3221224448 3221223136 134554687 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/8496/statm): 6250 5984 145 145 0 6105 0 [pid=8496] vsize: 25000 Current children cumulated CPU time (s) 49.79 Current children cumulated vsize (Kb) 27124 [startup+60.0085 s] Raw data (loadavg): 0.97 0.96 0.91 2/57 8496 Raw data (/proc/8492/stat): 8492 (minisat+_script) S 8491 8492 30740 0 -1 0 289 239 0 0 0 0 0 1 18 0 1 0 1785328358 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/8492/statm): 531 226 485 147 0 384 0 [pid=8492] vsize: 2124 Raw data (/proc/8496/stat): 8496 (minisat+_64-bit) R 8492 8492 30740 0 -1 0 5997 0 0 0 5951 27 0 0 25 0 1 0 1785328363 25600000 5984 4294967295 134512640 135094434 3221224448 3221223108 134553446 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/8496/statm): 6250 5984 145 145 0 6105 0 [pid=8496] vsize: 25000 Current children cumulated CPU time (s) 59.79 Current children cumulated vsize (Kb) 27124 [startup+70.0092 s] Raw data (loadavg): 0.97 0.96 0.91 2/57 8496 Raw data (/proc/8492/stat): 8492 (minisat+_script) S 8491 8492 30740 0 -1 0 289 239 0 0 0 0 0 1 18 0 1 0 1785328358 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/8492/statm): 531 226 485 147 0 384 0 [pid=8492] vsize: 2124 Raw data (/proc/8496/stat): 8496 (minisat+_64-bit) R 8492 8492 30740 0 -1 0 5997 0 0 0 6950 27 0 0 25 0 1 0 1785328363 25600000 5984 4294967295 134512640 135094434 3221224448 3221223108 134553446 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/8496/statm): 6250 5984 145 145 0 6105 0 [pid=8496] vsize: 25000 Current children cumulated CPU time (s) 69.78 Current children cumulated vsize (Kb) 27124 [startup+80.011 s] Raw data (loadavg): 0.98 0.96 0.91 2/57 8496 Raw data (/proc/8492/stat): 8492 (minisat+_script) S 8491 8492 30740 0 -1 0 289 239 0 0 0 0 0 1 18 0 1 0 1785328358 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/8492/statm): 531 226 485 147 0 384 0 [pid=8492] vsize: 2124 Raw data (/proc/8496/stat): 8496 (minisat+_64-bit) R 8492 8492 30740 0 -1 0 5998 0 0 0 7950 27 0 0 25 0 1 0 1785328363 25600000 5985 4294967295 134512640 135094434 3221224448 3221223072 134557696 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/8496/statm): 6250 5985 145 145 0 6105 0 [pid=8496] vsize: 25000 Current children cumulated CPU time (s) 79.78 Current children cumulated vsize (Kb) 27124 [startup+90.0118 s] Raw data (loadavg): 0.98 0.96 0.91 2/57 8496 Raw data (/proc/8492/stat): 8492 (minisat+_script) S 8491 8492 30740 0 -1 0 289 239 0 0 0 0 0 1 18 0 1 0 1785328358 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/8492/statm): 531 226 485 147 0 384 0 [pid=8492] vsize: 2124 Raw data (/proc/8496/stat): 8496 (minisat+_64-bit) R 8492 8492 30740 0 -1 0 5998 0 0 0 8950 28 0 0 25 0 1 0 1785328363 25600000 5985 4294967295 134512640 135094434 3221224448 3221223104 134558249 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/8496/statm): 6250 5985 145 145 0 6105 0 [pid=8496] vsize: 25000 Current children cumulated CPU time (s) 89.79 Current children cumulated vsize (Kb) 27124 [startup+100.012 s] Raw data (loadavg): 0.98 0.96 0.91 2/57 8496 Raw data (/proc/8492/stat): 8492 (minisat+_script) S 8491 8492 30740 0 -1 0 289 239 0 0 0 0 0 1 18 0 1 0 1785328358 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/8492/statm): 531 226 485 147 0 384 0 [pid=8492] vsize: 2124 Raw data (/proc/8496/stat): 8496 (minisat+_64-bit) R 8492 8492 30740 0 -1 0 6005 0 0 0 9950 28 0 0 25 0 1 0 1785328363 25624576 5992 4294967295 134512640 135094434 3221224448 3221221536 134519219 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/8496/statm): 6256 5992 145 145 0 6111 0 [pid=8496] vsize: 25024 Current children cumulated CPU time (s) 99.79 Current children cumulated vsize (Kb) 27148 [startup+110.013 s] Raw data (loadavg): 0.98 0.96 0.91 2/57 8496 Raw data (/proc/8492/stat): 8492 (minisat+_script) S 8491 8492 30740 0 -1 0 289 239 0 0 0 0 0 1 18 0 1 0 1785328358 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/8492/statm): 531 226 485 147 0 384 0 [pid=8492] vsize: 2124 Raw data (/proc/8496/stat): 8496 (minisat+_64-bit) R 8492 8492 30740 0 -1 0 6023 0 0 0 10949 28 0 0 25 0 1 0 1785328363 25702400 6010 4294967295 134512640 135094434 3221224448 3221223152 134559005 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/8496/statm): 6275 6010 145 145 0 6130 0 [pid=8496] vsize: 25100 Current children cumulated CPU time (s) 109.78 Current children cumulated vsize (Kb) 27224 [startup+120.014 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 8496 Raw data (/proc/8492/stat): 8492 (minisat+_script) S 8491 8492 30740 0 -1 0 289 239 0 0 0 0 0 1 18 0 1 0 1785328358 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/8492/statm): 531 226 485 147 0 384 0 [pid=8492] vsize: 2124 Raw data (/proc/8496/stat): 8496 (minisat+_64-bit) R 8492 8492 30740 0 -1 0 6202 0 0 0 11946 30 0 0 25 0 1 0 1785328363 26226688 6139 4294967295 134512640 135094434 3221224448 3221223108 134553482 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/8496/statm): 6403 6139 145 145 0 6258 0 [pid=8496] vsize: 25612 Current children cumulated CPU time (s) 119.77 Current children cumulated vsize (Kb) 27736 [startup+130.015 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 8496 Raw data (/proc/8492/stat): 8492 (minisat+_script) S 8491 8492 30740 0 -1 0 289 239 0 0 0 0 0 1 18 0 1 0 1785328358 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/8492/statm): 531 226 485 147 0 384 0 [pid=8492] vsize: 2124 Raw data (/proc/8496/stat): 8496 (minisat+_64-bit) R 8492 8492 30740 0 -1 0 6524 0 0 0 12942 32 0 0 25 0 1 0 1785328363 27389952 6410 4294967295 134512640 135094434 3221224448 3221223108 134553494 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/8496/statm): 6687 6410 145 145 0 6542 0 [pid=8496] vsize: 26748 Current children cumulated CPU time (s) 129.75 Current children cumulated vsize (Kb) 28872 [startup+140.016 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 8496 Raw data (/proc/8492/stat): 8492 (minisat+_script) S 8491 8492 30740 0 -1 0 289 239 0 0 0 0 0 1 18 0 1 0 1785328358 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/8492/statm): 531 226 485 147 0 384 0 [pid=8492] vsize: 2124 Raw data (/proc/8496/stat): 8496 (minisat+_64-bit) R 8492 8492 30740 0 -1 0 6989 0 0 0 13934 35 0 0 25 0 1 0 1785328363 29069312 6824 4294967295 134512640 135094434 3221224448 3221223104 134558411 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/8496/statm): 7097 6824 145 145 0 6952 0 [pid=8496] vsize: 28388 Current children cumulated CPU time (s) 139.7 Current children cumulated vsize (Kb) 30512 [startup+150.016 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 8496 Raw data (/proc/8492/stat): 8492 (minisat+_script) S 8491 8492 30740 0 -1 0 289 239 0 0 0 0 0 1 18 0 1 0 1785328358 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/8492/statm): 531 226 485 147 0 384 0 [pid=8492] vsize: 2124 Raw data (/proc/8496/stat): 8496 (minisat+_64-bit) R 8492 8492 30740 0 -1 0 7481 0 0 0 14925 39 0 0 25 0 1 0 1785328363 31068160 7316 4294967295 134512640 135094434 3221224448 3221223108 134553530 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/8496/statm): 7585 7316 145 145 0 7440 0 [pid=8496] vsize: 30340 Current children cumulated CPU time (s) 149.65 Current children cumulated vsize (Kb) 32464 [startup+160.017 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 8496 Raw data (/proc/8492/stat): 8492 (minisat+_script) S 8491 8492 30740 0 -1 0 289 239 0 0 0 0 0 1 18 0 1 0 1785328358 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/8492/statm): 531 226 485 147 0 384 0 [pid=8492] vsize: 2124 Raw data (/proc/8496/stat): 8496 (minisat+_64-bit) R 8492 8492 30740 0 -1 0 7995 0 0 0 15917 43 0 0 25 0 1 0 1785328363 32743424 7729 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/8496/statm): 7994 7729 145 145 0 7849 0 [pid=8496] vsize: 31976 Current children cumulated CPU time (s) 159.61 Current children cumulated vsize (Kb) 34100 [startup+170.018 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 8496 Raw data (/proc/8492/stat): 8492 (minisat+_script) S 8491 8492 30740 0 -1 0 289 239 0 0 0 0 0 1 18 0 1 0 1785328358 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/8492/statm): 531 226 485 147 0 384 0 [pid=8492] vsize: 2124 Raw data (/proc/8496/stat): 8496 (minisat+_64-bit) R 8492 8492 30740 0 -1 0 8521 0 0 0 16909 46 0 0 25 0 1 0 1785328363 35012608 8255 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/8496/statm): 8548 8255 145 145 0 8403 0 [pid=8496] vsize: 34192 Current children cumulated CPU time (s) 169.56 Current children cumulated vsize (Kb) 36316 [startup+180.019 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 8496 Raw data (/proc/8492/stat): 8492 (minisat+_script) S 8491 8492 30740 0 -1 0 289 239 0 0 0 0 0 1 18 0 1 0 1785328358 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/8492/statm): 531 226 485 147 0 384 0 [pid=8492] vsize: 2124 Raw data (/proc/8496/stat): 8496 (minisat+_64-bit) R 8492 8492 30740 0 -1 0 9032 0 0 0 17899 49 0 0 25 0 1 0 1785328363 37089280 8766 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/8496/statm): 9055 8766 145 145 0 8910 0 [pid=8496] vsize: 36220 Current children cumulated CPU time (s) 179.49 Current children cumulated vsize (Kb) 38344 [startup+190.019 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 8496 Raw data (/proc/8492/stat): 8492 (minisat+_script) S 8491 8492 30740 0 -1 0 289 239 0 0 0 0 0 1 18 0 1 0 1785328358 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/8492/statm): 531 226 485 147 0 384 0 [pid=8492] vsize: 2124 Raw data (/proc/8496/stat): 8496 (minisat+_64-bit) R 8492 8492 30740 0 -1 0 9613 0 0 0 18891 53 0 0 25 0 1 0 1785328363 39452672 9347 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/8496/statm): 9632 9347 145 145 0 9487 0 [pid=8496] vsize: 38528 Current children cumulated CPU time (s) 189.45 Current children cumulated vsize (Kb) 40652 [startup+200.02 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 8496 Raw data (/proc/8492/stat): 8492 (minisat+_script) S 8491 8492 30740 0 -1 0 289 239 0 0 0 0 0 1 18 0 1 0 1785328358 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/8492/statm): 531 226 485 147 0 384 0 [pid=8492] vsize: 2124 Raw data (/proc/8496/stat): 8496 (minisat+_64-bit) R 8492 8492 30740 0 -1 0 10215 0 0 0 19879 59 0 0 25 0 1 0 1785328363 41906176 9949 4294967295 134512640 135094434 3221224448 3221223104 134558213 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/8496/statm): 10231 9949 145 145 0 10086 0 [pid=8496] vsize: 40924 Current children cumulated CPU time (s) 199.39 Current children cumulated vsize (Kb) 43048 [startup+210.021 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 8496 Raw data (/proc/8492/stat): 8492 (minisat+_script) S 8491 8492 30740 0 -1 0 289 239 0 0 0 0 0 1 18 0 1 0 1785328358 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/8492/statm): 531 226 485 147 0 384 0 [pid=8492] vsize: 2124 Raw data (/proc/8496/stat): 8496 (minisat+_64-bit) R 8492 8492 30740 0 -1 0 10750 0 0 0 20868 64 0 0 25 0 1 0 1785328363 44085248 10484 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/8496/statm): 10763 10484 145 145 0 10618 0 [pid=8496] vsize: 43052 Current children cumulated CPU time (s) 209.33 Current children cumulated vsize (Kb) 45176 [startup+220.022 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 8496 Raw data (/proc/8492/stat): 8492 (minisat+_script) S 8491 8492 30740 0 -1 0 289 239 0 0 0 0 0 1 18 0 1 0 1785328358 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/8492/statm): 531 226 485 147 0 384 0 [pid=8492] vsize: 2124 Raw data (/proc/8496/stat): 8496 (minisat+_64-bit) R 8492 8492 30740 0 -1 0 11206 0 0 0 21860 68 0 0 25 0 1 0 1785328363 45731840 10889 4294967295 134512640 135094434 3221224448 3221222976 134780519 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/8496/statm): 11165 10889 145 145 0 11020 0 [pid=8496] vsize: 44660 Current children cumulated CPU time (s) 219.29 Current children cumulated vsize (Kb) 46784 [startup+230.024 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 8496 Raw data (/proc/8492/stat): 8492 (minisat+_script) S 8491 8492 30740 0 -1 0 289 239 0 0 0 0 0 1 18 0 1 0 1785328358 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/8492/statm): 531 226 485 147 0 384 0 [pid=8492] vsize: 2124 Raw data (/proc/8496/stat): 8496 (minisat+_64-bit) R 8492 8492 30740 0 -1 0 11586 0 0 0 22851 72 0 0 25 0 1 0 1785328363 47276032 11269 4294967295 134512640 135094434 3221224448 3221223104 134557920 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/8496/statm): 11542 11269 145 145 0 11397 0 [pid=8496] vsize: 46168 Current children cumulated CPU time (s) 229.24 Current children cumulated vsize (Kb) 48292 [startup+240.024 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 8496 Raw data (/proc/8492/stat): 8492 (minisat+_script) S 8491 8492 30740 0 -1 0 289 239 0 0 0 0 0 1 18 0 1 0 1785328358 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/8492/statm): 531 226 485 147 0 384 0 [pid=8492] vsize: 2124 Raw data (/proc/8496/stat): 8496 (minisat+_64-bit) R 8492 8492 30740 0 -1 0 11965 0 0 0 23844 74 0 0 25 0 1 0 1785328363 48816128 11648 4294967295 134512640 135094434 3221224448 3221223040 134556862 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/8496/statm): 11918 11648 145 145 0 11773 0 [pid=8496] vsize: 47672 Current children cumulated CPU time (s) 239.19 Current children cumulated vsize (Kb) 49796 [startup+250.025 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 8496 Raw data (/proc/8492/stat): 8492 (minisat+_script) S 8491 8492 30740 0 -1 0 289 239 0 0 0 0 0 1 18 0 1 0 1785328358 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/8492/statm): 531 226 485 147 0 384 0 [pid=8492] vsize: 2124 Raw data (/proc/8496/stat): 8496 (minisat+_64-bit) R 8492 8492 30740 0 -1 0 12328 0 0 0 24836 77 0 0 25 0 1 0 1785328363 50290688 12011 4294967295 134512640 135094434 3221224448 3221223104 134558159 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/8496/statm): 12278 12011 145 145 0 12133 0 [pid=8496] vsize: 49112 Current children cumulated CPU time (s) 249.14 Current children cumulated vsize (Kb) 51236 [startup+260.027 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 8496 Raw data (/proc/8492/stat): 8492 (minisat+_script) S 8491 8492 30740 0 -1 0 289 239 0 0 0 0 0 1 18 0 1 0 1785328358 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/8492/statm): 531 226 485 147 0 384 0 [pid=8492] vsize: 2124 Raw data (/proc/8496/stat): 8496 (minisat+_64-bit) R 8492 8492 30740 0 -1 0 12727 0 0 0 25828 80 0 0 25 0 1 0 1785328363 51912704 12410 4294967295 134512640 135094434 3221224448 3221223056 134781733 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/8496/statm): 12674 12410 145 145 0 12529 0 [pid=8496] vsize: 50696 Current children cumulated CPU time (s) 259.09 Current children cumulated vsize (Kb) 52820 [startup+270.027 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 8496 Raw data (/proc/8492/stat): 8492 (minisat+_script) S 8491 8492 30740 0 -1 0 289 239 0 0 0 0 0 1 18 0 1 0 1785328358 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/8492/statm): 531 226 485 147 0 384 0 [pid=8492] vsize: 2124 Raw data (/proc/8496/stat): 8496 (minisat+_64-bit) R 8492 8492 30740 0 -1 0 13064 0 0 0 26822 83 0 0 25 0 1 0 1785328363 53542912 12747 4294967295 134512640 135094434 3221224448 3221223040 134556785 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/8496/statm): 13072 12747 145 145 0 12927 0 [pid=8496] vsize: 52288 Current children cumulated CPU time (s) 269.06 Current children cumulated vsize (Kb) 54412 [startup+280.027 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 8496 Raw data (/proc/8492/stat): 8492 (minisat+_script) S 8491 8492 30740 0 -1 0 289 239 0 0 0 0 0 1 18 0 1 0 1785328358 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/8492/statm): 531 226 485 147 0 384 0 [pid=8492] vsize: 2124 Raw data (/proc/8496/stat): 8496 (minisat+_64-bit) R 8492 8492 30740 0 -1 0 13362 0 0 0 27817 85 0 0 25 0 1 0 1785328363 54755328 13045 4294967295 134512640 135094434 3221224448 3221223136 134554731 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/8496/statm): 13368 13045 145 145 0 13223 0 [pid=8496] vsize: 53472 Current children cumulated CPU time (s) 279.03 Current children cumulated vsize (Kb) 55596 [startup+290.029 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 8496 Raw data (/proc/8492/stat): 8492 (minisat+_script) S 8491 8492 30740 0 -1 0 289 239 0 0 0 0 0 1 18 0 1 0 1785328358 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/8492/statm): 531 226 485 147 0 384 0 [pid=8492] vsize: 2124 Raw data (/proc/8496/stat): 8496 (minisat+_64-bit) R 8492 8492 30740 0 -1 0 13676 0 0 0 28810 88 0 0 25 0 1 0 1785328363 56029184 13359 4294967295 134512640 135094434 3221224448 3221223104 134558159 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/8496/statm): 13679 13359 145 145 0 13534 0 [pid=8496] vsize: 54716 Current children cumulated CPU time (s) 288.99 Current children cumulated vsize (Kb) 56840 [startup+300.029 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 8496 Raw data (/proc/8492/stat): 8492 (minisat+_script) S 8491 8492 30740 0 -1 0 289 239 0 0 0 0 0 1 18 0 1 0 1785328358 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/8492/statm): 531 226 485 147 0 384 0 [pid=8492] vsize: 2124 Raw data (/proc/8496/stat): 8496 (minisat+_64-bit) R 8492 8492 30740 0 -1 0 13978 0 0 0 29804 90 0 0 25 0 1 0 1785328363 57253888 13661 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/8496/statm): 13978 13661 145 145 0 13833 0 [pid=8496] vsize: 55912 Current children cumulated CPU time (s) 298.95 Current children cumulated vsize (Kb) 58036 [startup+310.03 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 8496 Raw data (/proc/8492/stat): 8492 (minisat+_script) S 8491 8492 30740 0 -1 0 289 239 0 0 0 0 0 1 18 0 1 0 1785328358 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/8492/statm): 531 226 485 147 0 384 0 [pid=8492] vsize: 2124 Raw data (/proc/8496/stat): 8496 (minisat+_64-bit) R 8492 8492 30740 0 -1 0 14328 0 0 0 30799 92 0 0 25 0 1 0 1785328363 58466304 13960 4294967295 134512640 135094434 3221224448 3221223120 134556552 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/8496/statm): 14274 13960 145 145 0 14129 0 [pid=8496] vsize: 57096 Current children cumulated CPU time (s) 308.92 Current children cumulated vsize (Kb) 59220 [startup+320.03 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 8496 Raw data (/proc/8492/stat): 8492 (minisat+_script) S 8491 8492 30740 0 -1 0 289 239 0 0 0 0 0 1 18 0 1 0 1785328358 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/8492/statm): 531 226 485 147 0 384 0 [pid=8492] vsize: 2124 Raw data (/proc/8496/stat): 8496 (minisat+_64-bit) R 8492 8492 30740 0 -1 0 14328 0 0 0 31799 92 0 0 25 0 1 0 1785328363 58466304 13960 4294967295 134512640 135094434 3221224448 3221223120 134556252 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/8496/statm): 14274 13960 145 145 0 14129 0 [pid=8496] vsize: 57096 Current children cumulated CPU time (s) 318.92 Current children cumulated vsize (Kb) 59220 [startup+330.031 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 8496 Raw data (/proc/8492/stat): 8492 (minisat+_script) S 8491 8492 30740 0 -1 0 289 239 0 0 0 0 0 1 18 0 1 0 1785328358 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/8492/statm): 531 226 485 147 0 384 0 [pid=8492] vsize: 2124 Raw data (/proc/8496/stat): 8496 (minisat+_64-bit) R 8492 8492 30740 0 -1 0 14328 0 0 0 32799 92 0 0 25 0 1 0 1785328363 58466304 13960 4294967295 134512640 135094434 3221224448 3221223060 134563055 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/8496/statm): 14274 13960 145 145 0 14129 0 [pid=8496] vsize: 57096 Current children cumulated CPU time (s) 328.92 Current children cumulated vsize (Kb) 59220 [startup+340.032 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 8496 Raw data (/proc/8492/stat): 8492 (minisat+_script) S 8491 8492 30740 0 -1 0 289 239 0 0 0 0 0 1 18 0 1 0 1785328358 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/8492/statm): 531 226 485 147 0 384 0 [pid=8492] vsize: 2124 Raw data (/proc/8496/stat): 8496 (minisat+_64-bit) R 8492 8492 30740 0 -1 0 14328 0 0 0 33799 92 0 0 25 0 1 0 1785328363 58466304 13960 4294967295 134512640 135094434 3221224448 3221223104 134558187 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/8496/statm): 14274 13960 145 145 0 14129 0 [pid=8496] vsize: 57096 Current children cumulated CPU time (s) 338.92 Current children cumulated vsize (Kb) 59220 [startup+350.033 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 8496 Raw data (/proc/8492/stat): 8492 (minisat+_script) S 8491 8492 30740 0 -1 0 289 239 0 0 0 0 0 1 18 0 1 0 1785328358 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/8492/statm): 531 226 485 147 0 384 0 [pid=8492] vsize: 2124 Raw data (/proc/8496/stat): 8496 (minisat+_64-bit) R 8492 8492 30740 0 -1 0 14328 0 0 0 34800 92 0 0 25 0 1 0 1785328363 58466304 13960 4294967295 134512640 135094434 3221224448 3221223120 134555574 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/8496/statm): 14274 13960 145 145 0 14129 0 [pid=8496] vsize: 57096 Current children cumulated CPU time (s) 348.93 Current children cumulated vsize (Kb) 59220 [startup+360.035 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 8496 Raw data (/proc/8492/stat): 8492 (minisat+_script) S 8491 8492 30740 0 -1 0 289 239 0 0 0 0 0 1 18 0 1 0 1785328358 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/8492/statm): 531 226 485 147 0 384 0 [pid=8492] vsize: 2124 Raw data (/proc/8496/stat): 8496 (minisat+_64-bit) R 8492 8492 30740 0 -1 0 14328 0 0 0 35800 92 0 0 25 0 1 0 1785328363 58466304 13960 4294967295 134512640 135094434 3221224448 3221223072 134562104 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/8496/statm): 14274 13960 145 145 0 14129 0 [pid=8496] vsize: 57096 Current children cumulated CPU time (s) 358.93 Current children cumulated vsize (Kb) 59220 [startup+370.034 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 8496 Raw data (/proc/8492/stat): 8492 (minisat+_script) S 8491 8492 30740 0 -1 0 289 239 0 0 0 0 0 1 18 0 1 0 1785328358 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/8492/statm): 531 226 485 147 0 384 0 [pid=8492] vsize: 2124 Raw data (/proc/8496/stat): 8496 (minisat+_64-bit) R 8492 8492 30740 0 -1 0 14328 0 0 0 36800 92 0 0 25 0 1 0 1785328363 58466304 13960 4294967295 134512640 135094434 3221224448 3221223120 134556091 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/8496/statm): 14274 13960 145 145 0 14129 0 [pid=8496] vsize: 57096 Current children cumulated CPU time (s) 368.93 Current children cumulated vsize (Kb) 59220 [startup+380.035 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 8496 Raw data (/proc/8492/stat): 8492 (minisat+_script) S 8491 8492 30740 0 -1 0 289 239 0 0 0 0 0 1 18 0 1 0 1785328358 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/8492/statm): 531 226 485 147 0 384 0 [pid=8492] vsize: 2124 Raw data (/proc/8496/stat): 8496 (minisat+_64-bit) R 8492 8492 30740 0 -1 0 14328 0 0 0 37800 92 0 0 25 0 1 0 1785328363 58466304 13960 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/8496/statm): 14274 13960 145 145 0 14129 0 [pid=8496] vsize: 57096 Current children cumulated CPU time (s) 378.93 Current children cumulated vsize (Kb) 59220 [startup+390.036 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 8496 Raw data (/proc/8492/stat): 8492 (minisat+_script) S 8491 8492 30740 0 -1 0 289 239 0 0 0 0 0 1 18 0 1 0 1785328358 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/8492/statm): 531 226 485 147 0 384 0 [pid=8492] vsize: 2124 Raw data (/proc/8496/stat): 8496 (minisat+_64-bit) R 8492 8492 30740 0 -1 0 14328 0 0 0 38800 92 0 0 25 0 1 0 1785328363 58466304 13960 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/8496/statm): 14274 13960 145 145 0 14129 0 [pid=8496] vsize: 57096 Current children cumulated CPU time (s) 388.93 Current children cumulated vsize (Kb) 59220 [startup+400.036 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 8496 Raw data (/proc/8492/stat): 8492 (minisat+_script) S 8491 8492 30740 0 -1 0 289 239 0 0 0 0 0 1 18 0 1 0 1785328358 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/8492/statm): 531 226 485 147 0 384 0 [pid=8492] vsize: 2124 Raw data (/proc/8496/stat): 8496 (minisat+_64-bit) R 8492 8492 30740 0 -1 0 14328 0 0 0 39800 92 0 0 25 0 1 0 1785328363 58466304 13960 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/8496/statm): 14274 13960 145 145 0 14129 0 [pid=8496] vsize: 57096 Current children cumulated CPU time (s) 398.93 Current children cumulated vsize (Kb) 59220 [startup+410.036 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 8496 Raw data (/proc/8492/stat): 8492 (minisat+_script) S 8491 8492 30740 0 -1 0 289 239 0 0 0 0 0 1 18 0 1 0 1785328358 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/8492/statm): 531 226 485 147 0 384 0 [pid=8492] vsize: 2124 Raw data (/proc/8496/stat): 8496 (minisat+_64-bit) R 8492 8492 30740 0 -1 0 14328 0 0 0 40801 92 0 0 25 0 1 0 1785328363 58466304 13960 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/8496/statm): 14274 13960 145 145 0 14129 0 [pid=8496] vsize: 57096 Current children cumulated CPU time (s) 408.94 Current children cumulated vsize (Kb) 59220 [startup+420.036 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 8496 Raw data (/proc/8492/stat): 8492 (minisat+_script) S 8491 8492 30740 0 -1 0 289 239 0 0 0 0 0 1 18 0 1 0 1785328358 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/8492/statm): 531 226 485 147 0 384 0 [pid=8492] vsize: 2124 Raw data (/proc/8496/stat): 8496 (minisat+_64-bit) R 8492 8492 30740 0 -1 0 14328 0 0 0 41801 92 0 0 25 0 1 0 1785328363 58466304 13960 4294967295 134512640 135094434 3221224448 3221223104 134558249 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/8496/statm): 14274 13960 145 145 0 14129 0 [pid=8496] vsize: 57096 Current children cumulated CPU time (s) 418.94 Current children cumulated vsize (Kb) 59220 [startup+430.037 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 8496 Raw data (/proc/8492/stat): 8492 (minisat+_script) S 8491 8492 30740 0 -1 0 289 239 0 0 0 0 0 1 18 0 1 0 1785328358 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/8492/statm): 531 226 485 147 0 384 0 [pid=8492] vsize: 2124 Raw data (/proc/8496/stat): 8496 (minisat+_64-bit) R 8492 8492 30740 0 -1 0 14328 0 0 0 42801 92 0 0 25 0 1 0 1785328363 58466304 13960 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/8496/statm): 14274 13960 145 145 0 14129 0 [pid=8496] vsize: 57096 Current children cumulated CPU time (s) 428.94 Current children cumulated vsize (Kb) 59220 [startup+440.038 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 8496 Raw data (/proc/8492/stat): 8492 (minisat+_script) S 8491 8492 30740 0 -1 0 289 239 0 0 0 0 0 1 18 0 1 0 1785328358 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/8492/statm): 531 226 485 147 0 384 0 [pid=8492] vsize: 2124 Raw data (/proc/8496/stat): 8496 (minisat+_64-bit) R 8492 8492 30740 0 -1 0 14328 0 0 0 43801 92 0 0 25 0 1 0 1785328363 58466304 13960 4294967295 134512640 135094434 3221224448 3221223040 134557180 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/8496/statm): 14274 13960 145 145 0 14129 0 [pid=8496] vsize: 57096 Current children cumulated CPU time (s) 438.94 Current children cumulated vsize (Kb) 59220 [startup+450.038 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 8496 Raw data (/proc/8492/stat): 8492 (minisat+_script) S 8491 8492 30740 0 -1 0 289 239 0 0 0 0 0 1 18 0 1 0 1785328358 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/8492/statm): 531 226 485 147 0 384 0 [pid=8492] vsize: 2124 Raw data (/proc/8496/stat): 8496 (minisat+_64-bit) R 8492 8492 30740 0 -1 0 14328 0 0 0 44801 92 0 0 25 0 1 0 1785328363 58466304 13960 4294967295 134512640 135094434 3221224448 3221223104 134558178 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/8496/statm): 14274 13960 145 145 0 14129 0 [pid=8496] vsize: 57096 Current children cumulated CPU time (s) 448.94 Current children cumulated vsize (Kb) 59220 [startup+460.038 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 8496 Raw data (/proc/8492/stat): 8492 (minisat+_script) S 8491 8492 30740 0 -1 0 289 239 0 0 0 0 0 1 18 0 1 0 1785328358 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/8492/statm): 531 226 485 147 0 384 0 [pid=8492] vsize: 2124 Raw data (/proc/8496/stat): 8496 (minisat+_64-bit) R 8492 8492 30740 0 -1 0 14432 0 0 0 45800 93 0 0 25 0 1 0 1785328363 58892288 14064 4294967295 134512640 135094434 3221224448 3221223104 134558187 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/8496/statm): 14378 14064 145 145 0 14233 0 [pid=8496] vsize: 57512 Current children cumulated CPU time (s) 458.94 Current children cumulated vsize (Kb) 59636 [startup+470.039 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 8496 Raw data (/proc/8492/stat): 8492 (minisat+_script) S 8491 8492 30740 0 -1 0 289 239 0 0 0 0 0 1 18 0 1 0 1785328358 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/8492/statm): 531 226 485 147 0 384 0 [pid=8492] vsize: 2124 Raw data (/proc/8496/stat): 8496 (minisat+_64-bit) R 8492 8492 30740 0 -1 0 14827 0 0 0 46792 96 0 0 25 0 1 0 1785328363 60502016 14459 4294967295 134512640 135094434 3221224448 3221223104 134557988 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/8496/statm): 14771 14459 145 145 0 14626 0 [pid=8496] vsize: 59084 Current children cumulated CPU time (s) 468.89 Current children cumulated vsize (Kb) 61208 [startup+480.04 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 8496 Raw data (/proc/8492/stat): 8492 (minisat+_script) S 8491 8492 30740 0 -1 0 289 239 0 0 0 0 0 1 18 0 1 0 1785328358 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/8492/statm): 531 226 485 147 0 384 0 [pid=8492] vsize: 2124 Raw data (/proc/8496/stat): 8496 (minisat+_64-bit) R 8492 8492 30740 0 -1 0 15236 0 0 0 47785 99 0 0 25 0 1 0 1785328363 62164992 14868 4294967295 134512640 135094434 3221224448 3221223104 134557948 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/8496/statm): 15177 14868 145 145 0 15032 0 [pid=8496] vsize: 60708 Current children cumulated CPU time (s) 478.85 Current children cumulated vsize (Kb) 62832 [startup+490.041 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 8496 Raw data (/proc/8492/stat): 8492 (minisat+_script) S 8491 8492 30740 0 -1 0 289 239 0 0 0 0 0 1 18 0 1 0 1785328358 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/8492/statm): 531 226 485 147 0 384 0 [pid=8492] vsize: 2124 Raw data (/proc/8496/stat): 8496 (minisat+_64-bit) R 8492 8492 30740 0 -1 0 15591 0 0 0 48779 101 0 0 25 0 1 0 1785328363 63623168 15223 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/8496/statm): 15533 15223 145 145 0 15388 0 [pid=8496] vsize: 62132 Current children cumulated CPU time (s) 488.81 Current children cumulated vsize (Kb) 64256 [startup+500.041 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 8496 Raw data (/proc/8492/stat): 8492 (minisat+_script) S 8491 8492 30740 0 -1 0 289 239 0 0 0 0 0 1 18 0 1 0 1785328358 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/8492/statm): 531 226 485 147 0 384 0 [pid=8492] vsize: 2124 Raw data (/proc/8496/stat): 8496 (minisat+_64-bit) R 8492 8492 30740 0 -1 0 15972 0 0 0 49772 104 0 0 25 0 1 0 1785328363 65171456 15604 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/8496/statm): 15911 15604 145 145 0 15766 0 [pid=8496] vsize: 63644 Current children cumulated CPU time (s) 498.77 Current children cumulated vsize (Kb) 65768 [startup+510.042 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 8496 Raw data (/proc/8492/stat): 8492 (minisat+_script) S 8491 8492 30740 0 -1 0 289 239 0 0 0 0 0 1 18 0 1 0 1785328358 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/8492/statm): 531 226 485 147 0 384 0 [pid=8492] vsize: 2124 Raw data (/proc/8496/stat): 8496 (minisat+_64-bit) R 8492 8492 30740 0 -1 0 16349 0 0 0 50764 107 0 0 25 0 1 0 1785328363 66703360 15981 4294967295 134512640 135094434 3221224448 3221223072 134557662 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/8496/statm): 16285 15981 145 145 0 16140 0 [pid=8496] vsize: 65140 Current children cumulated CPU time (s) 508.72 Current children cumulated vsize (Kb) 67264 [startup+520.043 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 8496 Raw data (/proc/8492/stat): 8492 (minisat+_script) S 8491 8492 30740 0 -1 0 289 239 0 0 0 0 0 1 18 0 1 0 1785328358 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/8492/statm): 531 226 485 147 0 384 0 [pid=8492] vsize: 2124 Raw data (/proc/8496/stat): 8496 (minisat+_64-bit) R 8492 8492 30740 0 -1 0 16711 0 0 0 51758 111 0 0 25 0 1 0 1785328363 68177920 16343 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/8496/statm): 16645 16343 145 145 0 16500 0 [pid=8496] vsize: 66580 Current children cumulated CPU time (s) 518.7 Current children cumulated vsize (Kb) 68704 [startup+530.044 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 8496 Raw data (/proc/8492/stat): 8492 (minisat+_script) S 8491 8492 30740 0 -1 0 289 239 0 0 0 0 0 1 18 0 1 0 1785328358 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/8492/statm): 531 226 485 147 0 384 0 [pid=8492] vsize: 2124 Raw data (/proc/8496/stat): 8496 (minisat+_64-bit) R 8492 8492 30740 0 -1 0 17054 0 0 0 52752 113 0 0 25 0 1 0 1785328363 69574656 16686 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/8496/statm): 16986 16686 145 145 0 16841 0 [pid=8496] vsize: 67944 Current children cumulated CPU time (s) 528.66 Current children cumulated vsize (Kb) 70068 [startup+540.044 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 8496 Raw data (/proc/8492/stat): 8492 (minisat+_script) S 8491 8492 30740 0 -1 0 289 239 0 0 0 0 0 1 18 0 1 0 1785328358 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/8492/statm): 531 226 485 147 0 384 0 [pid=8492] vsize: 2124 Raw data (/proc/8496/stat): 8496 (minisat+_64-bit) R 8492 8492 30740 0 -1 0 17378 0 0 0 53746 116 0 0 25 0 1 0 1785328363 70893568 17010 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/8496/statm): 17308 17010 145 145 0 17163 0 [pid=8496] vsize: 69232 Current children cumulated CPU time (s) 538.63 Current children cumulated vsize (Kb) 71356 [startup+550.045 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 8496 Raw data (/proc/8492/stat): 8492 (minisat+_script) S 8491 8492 30740 0 -1 0 289 239 0 0 0 0 0 1 18 0 1 0 1785328358 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/8492/statm): 531 226 485 147 0 384 0 [pid=8492] vsize: 2124 Raw data (/proc/8496/stat): 8496 (minisat+_64-bit) R 8492 8492 30740 0 -1 0 17663 0 0 0 54741 119 0 0 25 0 1 0 1785328363 72052736 17295 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/8496/statm): 17591 17295 145 145 0 17446 0 [pid=8496] vsize: 70364 Current children cumulated CPU time (s) 548.61 Current children cumulated vsize (Kb) 72488 [startup+560.046 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 8496 Raw data (/proc/8492/stat): 8492 (minisat+_script) S 8491 8492 30740 0 -1 0 289 239 0 0 0 0 0 1 18 0 1 0 1785328358 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/8492/statm): 531 226 485 147 0 384 0 [pid=8492] vsize: 2124 Raw data (/proc/8496/stat): 8496 (minisat+_64-bit) R 8492 8492 30740 0 -1 0 17979 0 0 0 55736 121 0 0 25 0 1 0 1785328363 73334784 17611 4294967295 134512640 135094434 3221224448 3221223104 134558174 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/8496/statm): 17904 17611 145 145 0 17759 0 [pid=8496] vsize: 71616 Current children cumulated CPU time (s) 558.58 Current children cumulated vsize (Kb) 73740 [startup+570.046 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 8496 Raw data (/proc/8492/stat): 8492 (minisat+_script) S 8491 8492 30740 0 -1 0 289 239 0 0 0 0 0 1 18 0 1 0 1785328358 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/8492/statm): 531 226 485 147 0 384 0 [pid=8492] vsize: 2124 Raw data (/proc/8496/stat): 8496 (minisat+_64-bit) R 8492 8492 30740 0 -1 0 18216 0 0 0 56732 122 0 0 25 0 1 0 1785328363 74301440 17848 4294967295 134512640 135094434 3221224448 3221223040 134557236 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/8496/statm): 18140 17848 145 145 0 17995 0 [pid=8496] vsize: 72560 Current children cumulated CPU time (s) 568.55 Current children cumulated vsize (Kb) 74684 [startup+580.047 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 8496 Raw data (/proc/8492/stat): 8492 (minisat+_script) S 8491 8492 30740 0 -1 0 289 239 0 0 0 0 0 1 18 0 1 0 1785328358 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/8492/statm): 531 226 485 147 0 384 0 [pid=8492] vsize: 2124 Raw data (/proc/8496/stat): 8496 (minisat+_64-bit) R 8492 8492 30740 0 -1 0 18456 0 0 0 57727 125 0 0 25 0 1 0 1785328363 75276288 18088 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/8496/statm): 18378 18088 145 145 0 18233 0 [pid=8496] vsize: 73512 Current children cumulated CPU time (s) 578.53 Current children cumulated vsize (Kb) 75636 [startup+590.047 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 8496 Raw data (/proc/8492/stat): 8492 (minisat+_script) S 8491 8492 30740 0 -1 0 289 239 0 0 0 0 0 1 18 0 1 0 1785328358 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/8492/statm): 531 226 485 147 0 384 0 [pid=8492] vsize: 2124 Raw data (/proc/8496/stat): 8496 (minisat+_64-bit) R 8492 8492 30740 0 -1 0 18718 0 0 0 58723 126 0 0 25 0 1 0 1785328363 76341248 18350 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/8496/statm): 18638 18350 145 145 0 18493 0 [pid=8496] vsize: 74552 Current children cumulated CPU time (s) 588.5 Current children cumulated vsize (Kb) 76676 [startup+600.047 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 8496 Raw data (/proc/8492/stat): 8492 (minisat+_script) S 8491 8492 30740 0 -1 0 289 239 0 0 0 0 0 1 18 0 1 0 1785328358 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/8492/statm): 531 226 485 147 0 384 0 [pid=8492] vsize: 2124 Raw data (/proc/8496/stat): 8496 (minisat+_64-bit) R 8492 8492 30740 0 -1 0 18980 0 0 0 59719 128 0 0 25 0 1 0 1785328363 77402112 18612 4294967295 134512640 135094434 3221224448 3221223084 134557560 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/8496/statm): 18897 18612 145 145 0 18752 0 [pid=8496] vsize: 75588 Current children cumulated CPU time (s) 598.48 Current children cumulated vsize (Kb) 77712 [startup+610.048 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 8496 Raw data (/proc/8492/stat): 8492 (minisat+_script) S 8491 8492 30740 0 -1 0 289 239 0 0 0 0 0 1 18 0 1 0 1785328358 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/8492/statm): 531 226 485 147 0 384 0 [pid=8492] vsize: 2124 Raw data (/proc/8496/stat): 8496 (minisat+_64-bit) R 8492 8492 30740 0 -1 0 19274 0 0 0 60714 129 0 0 25 0 1 0 1785328363 78602240 18906 4294967295 134512640 135094434 3221224448 3221223104 134557950 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/8496/statm): 19190 18906 145 145 0 19045 0 [pid=8496] vsize: 76760 Current children cumulated CPU time (s) 608.44 Current children cumulated vsize (Kb) 78884 [startup+620.049 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 8496 Raw data (/proc/8492/stat): 8492 (minisat+_script) S 8491 8492 30740 0 -1 0 289 239 0 0 0 0 0 1 18 0 1 0 1785328358 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/8492/statm): 531 226 485 147 0 384 0 [pid=8492] vsize: 2124 Raw data (/proc/8496/stat): 8496 (minisat+_64-bit) R 8492 8492 30740 0 -1 0 19533 0 0 0 61710 131 0 0 25 0 1 0 1785328363 79650816 19165 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/8496/statm): 19446 19165 145 145 0 19301 0 [pid=8496] vsize: 77784 Current children cumulated CPU time (s) 618.42 Current children cumulated vsize (Kb) 79908 [startup+630.049 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 8496 Raw data (/proc/8492/stat): 8492 (minisat+_script) S 8491 8492 30740 0 -1 0 289 239 0 0 0 0 0 1 18 0 1 0 1785328358 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/8492/statm): 531 226 485 147 0 384 0 [pid=8492] vsize: 2124 Raw data (/proc/8496/stat): 8496 (minisat+_64-bit) R 8492 8492 30740 0 -1 0 19793 0 0 0 62706 133 0 0 25 0 1 0 1785328363 80711680 19425 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/8496/statm): 19705 19425 145 145 0 19560 0 [pid=8496] vsize: 78820 Current children cumulated CPU time (s) 628.4 Current children cumulated vsize (Kb) 80944 [startup+640.05 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 8496 Raw data (/proc/8492/stat): 8492 (minisat+_script) S 8491 8492 30740 0 -1 0 289 239 0 0 0 0 0 1 18 0 1 0 1785328358 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/8492/statm): 531 226 485 147 0 384 0 [pid=8492] vsize: 2124 Raw data (/proc/8496/stat): 8496 (minisat+_64-bit) R 8492 8492 30740 0 -1 0 20031 0 0 0 63701 135 0 0 25 0 1 0 1785328363 81678336 19663 4294967295 134512640 135094434 3221224448 3221223104 134557948 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/8496/statm): 19941 19663 145 145 0 19796 0 [pid=8496] vsize: 79764 Current children cumulated CPU time (s) 638.37 Current children cumulated vsize (Kb) 81888 [startup+650.051 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 8496 Raw data (/proc/8492/stat): 8492 (minisat+_script) S 8491 8492 30740 0 -1 0 289 239 0 0 0 0 0 1 18 0 1 0 1785328358 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/8492/statm): 531 226 485 147 0 384 0 [pid=8492] vsize: 2124 Raw data (/proc/8496/stat): 8496 (minisat+_64-bit) R 8492 8492 30740 0 -1 0 20301 0 0 0 64696 137 0 0 25 0 1 0 1785328363 82776064 19933 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/8496/statm): 20209 19933 145 145 0 20064 0 [pid=8496] vsize: 80836 Current children cumulated CPU time (s) 648.34 Current children cumulated vsize (Kb) 82960 [startup+660.052 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 8496 Raw data (/proc/8492/stat): 8492 (minisat+_script) S 8491 8492 30740 0 -1 0 289 239 0 0 0 0 0 1 18 0 1 0 1785328358 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/8492/statm): 531 226 485 147 0 384 0 [pid=8492] vsize: 2124 Raw data (/proc/8496/stat): 8496 (minisat+_64-bit) R 8492 8492 30740 0 -1 0 20570 0 0 0 65691 139 0 0 25 0 1 0 1785328363 83869696 20202 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/8496/statm): 20476 20202 145 145 0 20331 0 [pid=8496] vsize: 81904 Current children cumulated CPU time (s) 658.31 Current children cumulated vsize (Kb) 84028 [startup+670.051 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 8496 Raw data (/proc/8492/stat): 8492 (minisat+_script) S 8491 8492 30740 0 -1 0 289 239 0 0 0 0 0 1 18 0 1 0 1785328358 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/8492/statm): 531 226 485 147 0 384 0 [pid=8492] vsize: 2124 Raw data (/proc/8496/stat): 8496 (minisat+_64-bit) R 8492 8492 30740 0 -1 0 20834 0 0 0 66685 142 0 0 25 0 1 0 1785328363 85471232 20466 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/8496/statm): 20867 20466 145 145 0 20722 0 [pid=8496] vsize: 83468 Current children cumulated CPU time (s) 668.28 Current children cumulated vsize (Kb) 85592 [startup+680.052 s] Raw data (loadavg): 1.07 0.99 0.92 2/57 8496 Raw data (/proc/8492/stat): 8492 (minisat+_script) S 8491 8492 30740 0 -1 0 289 239 0 0 0 0 0 1 18 0 1 0 1785328358 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/8492/statm): 531 226 485 147 0 384 0 [pid=8492] vsize: 2124 Raw data (/proc/8496/stat): 8496 (minisat+_64-bit) R 8492 8492 30740 0 -1 0 21114 0 0 0 67680 144 0 0 25 0 1 0 1785328363 86605824 20746 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/8496/statm): 21144 20746 145 145 0 20999 0 [pid=8496] vsize: 84576 Current children cumulated CPU time (s) 678.25 Current children cumulated vsize (Kb) 86700 [startup+690.053 s] Raw data (loadavg): 1.06 0.99 0.92 2/57 8496 Raw data (/proc/8492/stat): 8492 (minisat+_script) S 8491 8492 30740 0 -1 0 289 239 0 0 0 0 0 1 18 0 1 0 1785328358 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/8492/statm): 531 226 485 147 0 384 0 [pid=8492] vsize: 2124 Raw data (/proc/8496/stat): 8496 (minisat+_64-bit) R 8492 8492 30740 0 -1 0 21368 0 0 0 68676 146 0 0 25 0 1 0 1785328363 87638016 21000 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/8496/statm): 21396 21000 145 145 0 21251 0 [pid=8496] vsize: 85584 Current children cumulated CPU time (s) 688.23 Current children cumulated vsize (Kb) 87708 [startup+700.053 s] Raw data (loadavg): 1.05 0.99 0.92 2/57 8496 Raw data (/proc/8492/stat): 8492 (minisat+_script) S 8491 8492 30740 0 -1 0 289 239 0 0 0 0 0 1 18 0 1 0 1785328358 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/8492/statm): 531 226 485 147 0 384 0 [pid=8492] vsize: 2124 Raw data (/proc/8496/stat): 8496 (minisat+_64-bit) R 8492 8492 30740 0 -1 0 21613 0 0 0 69672 147 0 0 25 0 1 0 1785328363 88629248 21245 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/8496/statm): 21638 21245 145 145 0 21493 0 [pid=8496] vsize: 86552 Current children cumulated CPU time (s) 698.2 Current children cumulated vsize (Kb) 88676 [startup+710.054 s] Raw data (loadavg): 1.04 0.99 0.92 2/57 8496 Raw data (/proc/8492/stat): 8492 (minisat+_script) S 8491 8492 30740 0 -1 0 289 239 0 0 0 0 0 1 18 0 1 0 1785328358 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/8492/statm): 531 226 485 147 0 384 0 [pid=8492] vsize: 2124 Raw data (/proc/8496/stat): 8496 (minisat+_64-bit) R 8492 8492 30740 0 -1 0 21883 0 0 0 70667 149 0 0 25 0 1 0 1785328363 89722880 21515 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/8496/statm): 21905 21515 145 145 0 21760 0 [pid=8496] vsize: 87620 Current children cumulated CPU time (s) 708.17 Current children cumulated vsize (Kb) 89744 [startup+720.055 s] Raw data (loadavg): 1.04 0.99 0.92 2/57 8496 Raw data (/proc/8492/stat): 8492 (minisat+_script) S 8491 8492 30740 0 -1 0 289 239 0 0 0 0 0 1 18 0 1 0 1785328358 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/8492/statm): 531 226 485 147 0 384 0 [pid=8492] vsize: 2124 Raw data (/proc/8496/stat): 8496 (minisat+_64-bit) R 8492 8492 30740 0 -1 0 22152 0 0 0 71662 151 0 0 25 0 1 0 1785328363 90816512 21784 4294967295 134512640 135094434 3221224448 3221223104 134557860 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/8496/statm): 22172 21784 145 145 0 22027 0 [pid=8496] vsize: 88688 Current children cumulated CPU time (s) 718.14 Current children cumulated vsize (Kb) 90812 [startup+730.056 s] Raw data (loadavg): 1.03 0.99 0.92 3/57 8496 Raw data (/proc/8492/stat): 8492 (minisat+_script) S 8491 8492 30740 0 -1 0 289 239 0 0 0 0 0 1 18 0 1 0 1785328358 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/8492/statm): 531 226 485 147 0 384 0 [pid=8492] vsize: 2124 Raw data (/proc/8496/stat): 8496 (minisat+_64-bit) R 8492 8492 30740 0 -1 0 22427 0 0 0 72658 153 0 0 25 0 1 0 1785328363 91934720 22059 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/8496/statm): 22445 22059 145 145 0 22300 0 [pid=8496] vsize: 89780 Current children cumulated CPU time (s) 728.12 Current children cumulated vsize (Kb) 91904 [startup+740.057 s] Raw data (loadavg): 1.03 0.99 0.92 2/57 8496 Raw data (/proc/8492/stat): 8492 (minisat+_script) S 8491 8492 30740 0 -1 0 289 239 0 0 0 0 0 1 18 0 1 0 1785328358 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/8492/statm): 531 226 485 147 0 384 0 [pid=8492] vsize: 2124 Raw data (/proc/8496/stat): 8496 (minisat+_64-bit) R 8492 8492 30740 0 -1 0 22646 0 0 0 73653 154 0 0 25 0 1 0 1785328363 92823552 22278 4294967295 134512640 135094434 3221224448 3221223136 134554746 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/8496/statm): 22662 22278 145 145 0 22517 0 [pid=8496] vsize: 90648 Current children cumulated CPU time (s) 738.08 Current children cumulated vsize (Kb) 92772 [startup+750.058 s] Raw data (loadavg): 1.02 0.99 0.92 2/57 8496 Raw data (/proc/8492/stat): 8492 (minisat+_script) S 8491 8492 30740 0 -1 0 289 239 0 0 0 0 0 1 18 0 1 0 1785328358 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/8492/statm): 531 226 485 147 0 384 0 [pid=8492] vsize: 2124 Raw data (/proc/8496/stat): 8496 (minisat+_64-bit) R 8492 8492 30740 0 -1 0 22883 0 0 0 74648 156 0 0 25 0 1 0 1785328363 93790208 22515 4294967295 134512640 135094434 3221224448 3221223104 134558221 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/8496/statm): 22898 22515 145 145 0 22753 0 [pid=8496] vsize: 91592 Current children cumulated CPU time (s) 748.05 Current children cumulated vsize (Kb) 93716 [startup+760.058 s] Raw data (loadavg): 1.02 0.99 0.92 2/57 8496 Raw data (/proc/8492/stat): 8492 (minisat+_script) S 8491 8492 30740 0 -1 0 289 239 0 0 0 0 0 1 18 0 1 0 1785328358 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/8492/statm): 531 226 485 147 0 384 0 [pid=8492] vsize: 2124 Raw data (/proc/8496/stat): 8496 (minisat+_64-bit) R 8492 8492 30740 0 -1 0 23118 0 0 0 75644 158 0 0 25 0 1 0 1785328363 94744576 22750 4294967295 134512640 135094434 3221224448 3221223104 134558007 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/8496/statm): 23131 22750 145 145 0 22986 0 [pid=8496] vsize: 92524 Current children cumulated CPU time (s) 758.03 Current children cumulated vsize (Kb) 94648 [startup+770.059 s] Raw data (loadavg): 1.01 0.99 0.92 2/57 8496 Raw data (/proc/8492/stat): 8492 (minisat+_script) S 8491 8492 30740 0 -1 0 289 239 0 0 0 0 0 1 18 0 1 0 1785328358 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/8492/statm): 531 226 485 147 0 384 0 [pid=8492] vsize: 2124 Raw data (/proc/8496/stat): 8496 (minisat+_64-bit) R 8492 8492 30740 0 -1 0 23356 0 0 0 76641 159 0 0 25 0 1 0 1785328363 95707136 22988 4294967295 134512640 135094434 3221224448 3221223104 134557945 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/8496/statm): 23366 22988 145 145 0 23221 0 [pid=8496] vsize: 93464 Current children cumulated CPU time (s) 768.01 Current children cumulated vsize (Kb) 95588 [startup+780.061 s] Raw data (loadavg): 1.01 0.99 0.92 2/57 8496 Raw data (/proc/8492/stat): 8492 (minisat+_script) S 8491 8492 30740 0 -1 0 289 239 0 0 0 0 0 1 18 0 1 0 1785328358 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/8492/statm): 531 226 485 147 0 384 0 [pid=8492] vsize: 2124 Raw data (/proc/8496/stat): 8496 (minisat+_64-bit) R 8492 8492 30740 0 -1 0 23562 0 0 0 77637 161 0 0 25 0 1 0 1785328363 96542720 23194 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/8496/statm): 23570 23194 145 145 0 23425 0 [pid=8496] vsize: 94280 Current children cumulated CPU time (s) 777.99 Current children cumulated vsize (Kb) 96404 [startup+790.062 s] Raw data (loadavg): 1.01 0.99 0.92 2/57 8496 Raw data (/proc/8492/stat): 8492 (minisat+_script) S 8491 8492 30740 0 -1 0 289 239 0 0 0 0 0 1 18 0 1 0 1785328358 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/8492/statm): 531 226 485 147 0 384 0 [pid=8492] vsize: 2124 Raw data (/proc/8496/stat): 8496 (minisat+_64-bit) R 8492 8492 30740 0 -1 0 23760 0 0 0 78633 162 0 0 25 0 1 0 1785328363 97345536 23392 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/8496/statm): 23766 23392 145 145 0 23621 0 [pid=8496] vsize: 95064 Current children cumulated CPU time (s) 787.96 Current children cumulated vsize (Kb) 97188 [startup+800.061 s] Raw data (loadavg): 1.01 0.99 0.92 2/57 8496 Raw data (/proc/8492/stat): 8492 (minisat+_script) S 8491 8492 30740 0 -1 0 289 239 0 0 0 0 0 1 18 0 1 0 1785328358 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/8492/statm): 531 226 485 147 0 384 0 [pid=8492] vsize: 2124 Raw data (/proc/8496/stat): 8496 (minisat+_64-bit) R 8492 8492 30740 0 -1 0 24000 0 0 0 79629 164 0 0 25 0 1 0 1785328363 98320384 23632 4294967295 134512640 135094434 3221224448 3221223120 134556073 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/8496/statm): 24004 23632 145 145 0 23859 0 [pid=8496] vsize: 96016 Current children cumulated CPU time (s) 797.94 Current children cumulated vsize (Kb) 98140 [startup+810.062 s] Raw data (loadavg): 1.01 0.99 0.92 2/57 8496 Raw data (/proc/8492/stat): 8492 (minisat+_script) S 8491 8492 30740 0 -1 0 289 239 0 0 0 0 0 1 18 0 1 0 1785328358 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/8492/statm): 531 226 485 147 0 384 0 [pid=8492] vsize: 2124 Raw data (/proc/8496/stat): 8496 (minisat+_64-bit) R 8492 8492 30740 0 -1 0 24242 0 0 0 80625 166 0 0 25 0 1 0 1785328363 99303424 23874 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/8496/statm): 24244 23874 145 145 0 24099 0 [pid=8496] vsize: 96976 Current children cumulated CPU time (s) 807.92 Current children cumulated vsize (Kb) 99100 [startup+820.063 s] Raw data (loadavg): 1.00 0.99 0.92 2/57 8496 Raw data (/proc/8492/stat): 8492 (minisat+_script) S 8491 8492 30740 0 -1 0 289 239 0 0 0 0 0 1 18 0 1 0 1785328358 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/8492/statm): 531 226 485 147 0 384 0 [pid=8492] vsize: 2124 Raw data (/proc/8496/stat): 8496 (minisat+_64-bit) R 8492 8492 30740 0 -1 0 24445 0 0 0 81621 168 0 0 25 0 1 0 1785328363 100126720 24077 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/8496/statm): 24445 24077 145 145 0 24300 0 [pid=8496] vsize: 97780 Current children cumulated CPU time (s) 817.9 Current children cumulated vsize (Kb) 99904 [startup+830.064 s] Raw data (loadavg): 1.00 0.99 0.92 2/57 8496 Raw data (/proc/8492/stat): 8492 (minisat+_script) S 8491 8492 30740 0 -1 0 289 239 0 0 0 0 0 1 18 0 1 0 1785328358 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/8492/statm): 531 226 485 147 0 384 0 [pid=8492] vsize: 2124 Raw data (/proc/8496/stat): 8496 (minisat+_64-bit) R 8492 8492 30740 0 -1 0 24624 0 0 0 82619 169 0 0 25 0 1 0 1785328363 100851712 24256 4294967295 134512640 135094434 3221224448 3221223104 134558249 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/8496/statm): 24622 24256 145 145 0 24477 0 [pid=8496] vsize: 98488 Current children cumulated CPU time (s) 827.89 Current children cumulated vsize (Kb) 100612 [startup+840.064 s] Raw data (loadavg): 1.00 0.99 0.92 2/57 8496 Raw data (/proc/8492/stat): 8492 (minisat+_script) S 8491 8492 30740 0 -1 0 289 239 0 0 0 0 0 1 18 0 1 0 1785328358 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/8492/statm): 531 226 485 147 0 384 0 [pid=8492] vsize: 2124 Raw data (/proc/8496/stat): 8496 (minisat+_64-bit) R 8492 8492 30740 0 -1 0 24807 0 0 0 83614 171 0 0 25 0 1 0 1785328363 101593088 24439 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/8496/statm): 24803 24439 145 145 0 24658 0 [pid=8496] vsize: 99212 Current children cumulated CPU time (s) 837.86 Current children cumulated vsize (Kb) 101336 [startup+850.065 s] Raw data (loadavg): 1.00 0.99 0.92 2/57 8496 Raw data (/proc/8492/stat): 8492 (minisat+_script) S 8491 8492 30740 0 -1 0 289 239 0 0 0 0 0 1 18 0 1 0 1785328358 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/8492/statm): 531 226 485 147 0 384 0 [pid=8492] vsize: 2124 Raw data (/proc/8496/stat): 8496 (minisat+_64-bit) R 8492 8492 30740 0 -1 0 24974 0 0 0 84610 173 0 0 25 0 1 0 1785328363 102273024 24606 4294967295 134512640 135094434 3221224448 3221223040 134557143 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/8496/statm): 24969 24606 145 145 0 24824 0 [pid=8496] vsize: 99876 Current children cumulated CPU time (s) 847.84 Current children cumulated vsize (Kb) 102000 [startup+860.066 s] Raw data (loadavg): 1.00 0.99 0.92 2/57 8496 Raw data (/proc/8492/stat): 8492 (minisat+_script) S 8491 8492 30740 0 -1 0 289 239 0 0 0 0 0 1 18 0 1 0 1785328358 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/8492/statm): 531 226 485 147 0 384 0 [pid=8492] vsize: 2124 Raw data (/proc/8496/stat): 8496 (minisat+_64-bit) R 8492 8492 30740 0 -1 0 25142 0 0 0 85607 174 0 0 25 0 1 0 1785328363 102952960 24774 4294967295 134512640 135094434 3221224448 3221223104 134558181 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/8496/statm): 25135 24774 145 145 0 24990 0 [pid=8496] vsize: 100540 Current children cumulated CPU time (s) 857.82 Current children cumulated vsize (Kb) 102664 [startup+870.067 s] Raw data (loadavg): 1.00 0.99 0.92 2/57 8496 Raw data (/proc/8492/stat): 8492 (minisat+_script) S 8491 8492 30740 0 -1 0 289 239 0 0 0 0 0 1 18 0 1 0 1785328358 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/8492/statm): 531 226 485 147 0 384 0 [pid=8492] vsize: 2124 Raw data (/proc/8496/stat): 8496 (minisat+_64-bit) R 8492 8492 30740 0 -1 0 25335 0 0 0 86604 175 0 0 25 0 1 0 1785328363 103739392 24967 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/8496/statm): 25327 24967 145 145 0 25182 0 [pid=8496] vsize: 101308 Current children cumulated CPU time (s) 867.8 Current children cumulated vsize (Kb) 103432 [startup+880.068 s] Raw data (loadavg): 1.00 0.99 0.92 2/57 8496 Raw data (/proc/8492/stat): 8492 (minisat+_script) S 8491 8492 30740 0 -1 0 289 239 0 0 0 0 0 1 18 0 1 0 1785328358 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/8492/statm): 531 226 485 147 0 384 0 [pid=8492] vsize: 2124 Raw data (/proc/8496/stat): 8496 (minisat+_64-bit) R 8492 8492 30740 0 -1 0 25525 0 0 0 87601 177 0 0 25 0 1 0 1785328363 104505344 25157 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/8496/statm): 25514 25157 145 145 0 25369 0 [pid=8496] vsize: 102056 Current children cumulated CPU time (s) 877.79 Current children cumulated vsize (Kb) 104180 [startup+890.068 s] Raw data (loadavg): 1.00 0.99 0.92 2/57 8496 Raw data (/proc/8492/stat): 8492 (minisat+_script) S 8491 8492 30740 0 -1 0 289 239 0 0 0 0 0 1 18 0 1 0 1785328358 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/8492/statm): 531 226 485 147 0 384 0 [pid=8492] vsize: 2124 Raw data (/proc/8496/stat): 8496 (minisat+_64-bit) R 8492 8492 30740 0 -1 0 25704 0 0 0 88598 178 0 0 25 0 1 0 1785328363 105234432 25336 4294967295 134512640 135094434 3221224448 3221223104 134557948 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/8496/statm): 25692 25336 145 145 0 25547 0 [pid=8496] vsize: 102768 Current children cumulated CPU time (s) 887.77 Current children cumulated vsize (Kb) 104892 [startup+900.069 s] Raw data (loadavg): 1.00 0.99 0.92 2/57 8496 Raw data (/proc/8492/stat): 8492 (minisat+_script) S 8491 8492 30740 0 -1 0 289 239 0 0 0 0 0 1 18 0 1 0 1785328358 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/8492/statm): 531 226 485 147 0 384 0 [pid=8492] vsize: 2124 Raw data (/proc/8496/stat): 8496 (minisat+_64-bit) R 8492 8492 30740 0 -1 0 25892 0 0 0 89595 179 0 0 25 0 1 0 1785328363 106016768 25524 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/8496/statm): 25883 25524 145 145 0 25738 0 [pid=8496] vsize: 103532 Current children cumulated CPU time (s) 897.75 Current children cumulated vsize (Kb) 105656 [startup+910.07 s] Raw data (loadavg): 1.00 0.99 0.92 2/57 8496 Raw data (/proc/8492/stat): 8492 (minisat+_script) S 8491 8492 30740 0 -1 0 289 239 0 0 0 0 0 1 18 0 1 0 1785328358 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/8492/statm): 531 226 485 147 0 384 0 [pid=8492] vsize: 2124 Raw data (/proc/8496/stat): 8496 (minisat+_64-bit) R 8492 8492 30740 0 -1 0 26078 0 0 0 90592 181 0 0 25 0 1 0 1785328363 106770432 25710 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/8496/statm): 26067 25710 145 145 0 25922 0 [pid=8496] vsize: 104268 Current children cumulated CPU time (s) 907.74 Current children cumulated vsize (Kb) 106392 [startup+920.073 s] Raw data (loadavg): 1.00 0.99 0.92 2/57 8496 Raw data (/proc/8492/stat): 8492 (minisat+_script) S 8491 8492 30740 0 -1 0 289 239 0 0 0 0 0 1 18 0 1 0 1785328358 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/8492/statm): 531 226 485 147 0 384 0 [pid=8492] vsize: 2124 Raw data (/proc/8496/stat): 8496 (minisat+_64-bit) R 8492 8492 30740 0 -1 0 26264 0 0 0 91588 182 0 0 25 0 1 0 1785328363 107520000 25896 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/8496/statm): 26250 25896 145 145 0 26105 0 [pid=8496] vsize: 105000 Current children cumulated CPU time (s) 917.71 Current children cumulated vsize (Kb) 107124 [startup+930.073 s] Raw data (loadavg): 1.00 0.99 0.92 2/57 8496 Raw data (/proc/8492/stat): 8492 (minisat+_script) S 8491 8492 30740 0 -1 0 289 239 0 0 0 0 0 1 18 0 1 0 1785328358 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/8492/statm): 531 226 485 147 0 384 0 [pid=8492] vsize: 2124 Raw data (/proc/8496/stat): 8496 (minisat+_64-bit) R 8492 8492 30740 0 -1 0 26436 0 0 0 92585 184 0 0 25 0 1 0 1785328363 108224512 26068 4294967295 134512640 135094434 3221224448 3221223040 134557202 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/8496/statm): 26422 26068 145 145 0 26277 0 [pid=8496] vsize: 105688 Current children cumulated CPU time (s) 927.7 Current children cumulated vsize (Kb) 107812 [startup+940.074 s] Raw data (loadavg): 1.00 0.99 0.92 2/57 8496 Raw data (/proc/8492/stat): 8492 (minisat+_script) S 8491 8492 30740 0 -1 0 289 239 0 0 0 0 0 1 18 0 1 0 1785328358 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/8492/statm): 531 226 485 147 0 384 0 [pid=8492] vsize: 2124 Raw data (/proc/8496/stat): 8496 (minisat+_64-bit) R 8492 8492 30740 0 -1 0 26615 0 0 0 93582 185 0 0 25 0 1 0 1785328363 108949504 26247 4294967295 134512640 135094434 3221224448 3221223104 134558225 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/8496/statm): 26599 26247 145 145 0 26454 0 [pid=8496] vsize: 106396 Current children cumulated CPU time (s) 937.68 Current children cumulated vsize (Kb) 108520 [startup+950.075 s] Raw data (loadavg): 1.00 0.99 0.92 2/57 8496 Raw data (/proc/8492/stat): 8492 (minisat+_script) S 8491 8492 30740 0 -1 0 289 239 0 0 0 0 0 1 18 0 1 0 1785328358 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/8492/statm): 531 226 485 147 0 384 0 [pid=8492] vsize: 2124 Raw data (/proc/8496/stat): 8496 (minisat+_64-bit) R 8492 8492 30740 0 -1 0 26777 0 0 0 94580 186 0 0 25 0 1 0 1785328363 109600768 26409 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/8496/statm): 26758 26409 145 145 0 26613 0 [pid=8496] vsize: 107032 Current children cumulated CPU time (s) 947.67 Current children cumulated vsize (Kb) 109156 [startup+960.076 s] Raw data (loadavg): 1.00 0.99 0.92 2/57 8496 Raw data (/proc/8492/stat): 8492 (minisat+_script) S 8491 8492 30740 0 -1 0 289 239 0 0 0 0 0 1 18 0 1 0 1785328358 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/8492/statm): 531 226 485 147 0 384 0 [pid=8492] vsize: 2124 Raw data (/proc/8496/stat): 8496 (minisat+_64-bit) R 8492 8492 30740 0 -1 0 26948 0 0 0 95576 188 0 0 25 0 1 0 1785328363 110346240 26580 4294967295 134512640 135094434 3221224448 3221223136 134554685 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/8496/statm): 26940 26580 145 145 0 26795 0 [pid=8496] vsize: 107760 Current children cumulated CPU time (s) 957.65 Current children cumulated vsize (Kb) 109884 [startup+970.076 s] Raw data (loadavg): 1.00 0.99 0.92 2/57 8496 Raw data (/proc/8492/stat): 8492 (minisat+_script) S 8491 8492 30740 0 -1 0 289 239 0 0 0 0 0 1 18 0 1 0 1785328358 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/8492/statm): 531 226 485 147 0 384 0 [pid=8492] vsize: 2124 Raw data (/proc/8496/stat): 8496 (minisat+_64-bit) R 8492 8492 30740 0 -1 0 27097 0 0 0 96575 189 0 0 25 0 1 0 1785328363 110956544 26729 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/8496/statm): 27089 26729 145 145 0 26944 0 [pid=8496] vsize: 108356 Current children cumulated CPU time (s) 967.65 Current children cumulated vsize (Kb) 110480 [startup+980.076 s] Raw data (loadavg): 1.00 0.99 0.92 2/57 8496 Raw data (/proc/8492/stat): 8492 (minisat+_script) S 8491 8492 30740 0 -1 0 289 239 0 0 0 0 0 1 18 0 1 0 1785328358 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/8492/statm): 531 226 485 147 0 384 0 [pid=8492] vsize: 2124 Raw data (/proc/8496/stat): 8496 (minisat+_64-bit) R 8492 8492 30740 0 -1 0 27223 0 0 0 97572 189 0 0 25 0 1 0 1785328363 111472640 26855 4294967295 134512640 135094434 3221224448 3221223104 134558249 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/8496/statm): 27215 26855 145 145 0 27070 0 [pid=8496] vsize: 108860 Current children cumulated CPU time (s) 977.62 Current children cumulated vsize (Kb) 110984 [startup+990.077 s] Raw data (loadavg): 1.00 0.99 0.92 2/57 8496 Raw data (/proc/8492/stat): 8492 (minisat+_script) S 8491 8492 30740 0 -1 0 289 239 0 0 0 0 0 1 18 0 1 0 1785328358 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/8492/statm): 531 226 485 147 0 384 0 [pid=8492] vsize: 2124 Raw data (/proc/8496/stat): 8496 (minisat+_64-bit) R 8492 8492 30740 0 -1 0 27362 0 0 0 98569 191 0 0 25 0 1 0 1785328363 112033792 26994 4294967295 134512640 135094434 3221224448 3221223104 134558227 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/8496/statm): 27352 26994 145 145 0 27207 0 [pid=8496] vsize: 109408 Current children cumulated CPU time (s) 987.61 Current children cumulated vsize (Kb) 111532 [startup+1000.08 s] Raw data (loadavg): 1.00 0.99 0.92 2/57 8496 Raw data (/proc/8492/stat): 8492 (minisat+_script) S 8491 8492 30740 0 -1 0 289 239 0 0 0 0 0 1 18 0 1 0 1785328358 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/8492/statm): 531 226 485 147 0 384 0 [pid=8492] vsize: 2124 Raw data (/proc/8496/stat): 8496 (minisat+_64-bit) R 8492 8492 30740 0 -1 0 27506 0 0 0 99567 192 0 0 25 0 1 0 1785328363 112656384 27138 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/8496/statm): 27504 27138 145 145 0 27359 0 [pid=8496] vsize: 110016 Current children cumulated CPU time (s) 997.6 Current children cumulated vsize (Kb) 112140 [startup+1010.08 s] Raw data (loadavg): 1.00 0.99 0.92 2/57 8496 Raw data (/proc/8492/stat): 8492 (minisat+_script) S 8491 8492 30740 0 -1 0 289 239 0 0 0 0 0 1 18 0 1 0 1785328358 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/8492/statm): 531 226 485 147 0 384 0 [pid=8492] vsize: 2124 Raw data (/proc/8496/stat): 8496 (minisat+_64-bit) R 8492 8492 30740 0 -1 0 27646 0 0 0 100565 194 0 0 25 0 1 0 1785328363 113217536 27278 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/8496/statm): 27641 27278 145 145 0 27496 0 [pid=8496] vsize: 110564 Current children cumulated CPU time (s) 1007.6 Current children cumulated vsize (Kb) 112688 [startup+1020.08 s] Raw data (loadavg): 1.00 0.99 0.92 2/57 8496 Raw data (/proc/8492/stat): 8492 (minisat+_script) S 8491 8492 30740 0 -1 0 289 239 0 0 0 0 0 1 18 0 1 0 1785328358 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/8492/statm): 531 226 485 147 0 384 0 [pid=8492] vsize: 2124 Raw data (/proc/8496/stat): 8496 (minisat+_64-bit) R 8492 8492 30740 0 -1 0 27789 0 0 0 101562 195 0 0 25 0 1 0 1785328363 113799168 27421 4294967295 134512640 135094434 3221224448 3221223104 134557948 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/8496/statm): 27783 27421 145 145 0 27638 0 [pid=8496] vsize: 111132 Current children cumulated CPU time (s) 1017.58 Current children cumulated vsize (Kb) 113256 [startup+1030.08 s] Raw data (loadavg): 1.00 0.99 0.92 3/57 8496 Raw data (/proc/8492/stat): 8492 (minisat+_script) S 8491 8492 30740 0 -1 0 289 239 0 0 0 0 0 1 18 0 1 0 1785328358 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/8492/statm): 531 226 485 147 0 384 0 [pid=8492] vsize: 2124 Raw data (/proc/8496/stat): 8496 (minisat+_64-bit) R 8492 8492 30740 0 -1 0 27927 0 0 0 102559 196 0 0 25 0 1 0 1785328363 114356224 27559 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/8496/statm): 27919 27559 145 145 0 27774 0 [pid=8496] vsize: 111676 Current children cumulated CPU time (s) 1027.56 Current children cumulated vsize (Kb) 113800 [startup+1040.08 s] Raw data (loadavg): 1.00 0.99 0.92 2/57 8496 Raw data (/proc/8492/stat): 8492 (minisat+_script) S 8491 8492 30740 0 -1 0 289 239 0 0 0 0 0 1 18 0 1 0 1785328358 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/8492/statm): 531 226 485 147 0 384 0 [pid=8492] vsize: 2124 Raw data (/proc/8496/stat): 8496 (minisat+_64-bit) R 8492 8492 30740 0 -1 0 28058 0 0 0 103557 197 0 0 25 0 1 0 1785328363 114884608 27690 4294967295 134512640 135094434 3221224448 3221223104 134557996 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/8496/statm): 28048 27690 145 145 0 27903 0 [pid=8496] vsize: 112192 Current children cumulated CPU time (s) 1037.55 Current children cumulated vsize (Kb) 114316 [startup+1050.08 s] Raw data (loadavg): 1.00 0.99 0.92 2/57 8496 Raw data (/proc/8492/stat): 8492 (minisat+_script) S 8491 8492 30740 0 -1 0 289 239 0 0 0 0 0 1 18 0 1 0 1785328358 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/8492/statm): 531 226 485 147 0 384 0 [pid=8492] vsize: 2124 Raw data (/proc/8496/stat): 8496 (minisat+_64-bit) R 8492 8492 30740 0 -1 0 28191 0 0 0 104555 198 0 0 25 0 1 0 1785328363 115421184 27823 4294967295 134512640 135094434 3221224448 3221223104 134557948 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/8496/statm): 28179 27823 145 145 0 28034 0 [pid=8496] vsize: 112716 Current children cumulated CPU time (s) 1047.54 Current children cumulated vsize (Kb) 114840 [startup+1060.08 s] Raw data (loadavg): 1.00 0.99 0.92 2/57 8496 Raw data (/proc/8492/stat): 8492 (minisat+_script) S 8491 8492 30740 0 -1 0 289 239 0 0 0 0 0 1 18 0 1 0 1785328358 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/8492/statm): 531 226 485 147 0 384 0 [pid=8492] vsize: 2124 Raw data (/proc/8496/stat): 8496 (minisat+_64-bit) R 8492 8492 30740 0 -1 0 28213 0 0 0 105555 198 0 0 25 0 1 0 1785328363 115511296 27845 4294967295 134512640 135094434 3221224448 3221223040 134557037 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/8496/statm): 28201 27845 145 145 0 28056 0 [pid=8496] vsize: 112804 Current children cumulated CPU time (s) 1057.54 Current children cumulated vsize (Kb) 114928 [startup+1070.08 s] Raw data (loadavg): 1.00 0.99 0.92 2/57 8496 Raw data (/proc/8492/stat): 8492 (minisat+_script) S 8491 8492 30740 0 -1 0 289 239 0 0 0 0 0 1 18 0 1 0 1785328358 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/8492/statm): 531 226 485 147 0 384 0 [pid=8492] vsize: 2124 Raw data (/proc/8496/stat): 8496 (minisat+_64-bit) R 8492 8492 30740 0 -1 0 28213 0 0 0 106555 198 0 0 25 0 1 0 1785328363 115511296 27845 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/8496/statm): 28201 27845 145 145 0 28056 0 [pid=8496] vsize: 112804 Current children cumulated CPU time (s) 1067.54 Current children cumulated vsize (Kb) 114928 [startup+1080.08 s] Raw data (loadavg): 1.00 0.99 0.92 2/57 8496 Raw data (/proc/8492/stat): 8492 (minisat+_script) S 8491 8492 30740 0 -1 0 289 239 0 0 0 0 0 1 18 0 1 0 1785328358 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/8492/statm): 531 226 485 147 0 384 0 [pid=8492] vsize: 2124 Raw data (/proc/8496/stat): 8496 (minisat+_64-bit) R 8492 8492 30740 0 -1 0 28213 0 0 0 107555 198 0 0 25 0 1 0 1785328363 115511296 27845 4294967295 134512640 135094434 3221224448 3221223040 134557248 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/8496/statm): 28201 27845 145 145 0 28056 0 [pid=8496] vsize: 112804 Current children cumulated CPU time (s) 1077.54 Current children cumulated vsize (Kb) 114928 [startup+1090.08 s] Raw data (loadavg): 1.00 0.99 0.92 2/57 8496 Raw data (/proc/8492/stat): 8492 (minisat+_script) S 8491 8492 30740 0 -1 0 289 239 0 0 0 0 0 1 18 0 1 0 1785328358 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/8492/statm): 531 226 485 147 0 384 0 [pid=8492] vsize: 2124 Raw data (/proc/8496/stat): 8496 (minisat+_64-bit) R 8492 8492 30740 0 -1 0 28213 0 0 0 108554 199 0 0 25 0 1 0 1785328363 115511296 27845 4294967295 134512640 135094434 3221224448 3221222912 134780543 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/8496/statm): 28201 27845 145 145 0 28056 0 [pid=8496] vsize: 112804 Current children cumulated CPU time (s) 1087.54 Current children cumulated vsize (Kb) 114928 [startup+1100.08 s] Raw data (loadavg): 1.00 0.99 0.92 2/57 8496 Raw data (/proc/8492/stat): 8492 (minisat+_script) S 8491 8492 30740 0 -1 0 289 239 0 0 0 0 0 1 18 0 1 0 1785328358 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/8492/statm): 531 226 485 147 0 384 0 [pid=8492] vsize: 2124 Raw data (/proc/8496/stat): 8496 (minisat+_64-bit) R 8492 8492 30740 0 -1 0 28213 0 0 0 109553 199 0 0 25 0 1 0 1785328363 115511296 27845 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/8496/statm): 28201 27845 145 145 0 28056 0 [pid=8496] vsize: 112804 Current children cumulated CPU time (s) 1097.53 Current children cumulated vsize (Kb) 114928 [startup+1110.08 s] Raw data (loadavg): 1.00 0.99 0.92 2/57 8496 Raw data (/proc/8492/stat): 8492 (minisat+_script) S 8491 8492 30740 0 -1 0 289 239 0 0 0 0 0 1 18 0 1 0 1785328358 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/8492/statm): 531 226 485 147 0 384 0 [pid=8492] vsize: 2124 Raw data (/proc/8496/stat): 8496 (minisat+_64-bit) R 8492 8492 30740 0 -1 0 28213 0 0 0 110553 199 0 0 25 0 1 0 1785328363 115511296 27845 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/8496/statm): 28201 27845 145 145 0 28056 0 [pid=8496] vsize: 112804 Current children cumulated CPU time (s) 1107.53 Current children cumulated vsize (Kb) 114928 [startup+1120.09 s] Raw data (loadavg): 1.00 0.99 0.92 2/57 8496 Raw data (/proc/8492/stat): 8492 (minisat+_script) S 8491 8492 30740 0 -1 0 289 239 0 0 0 0 0 1 18 0 1 0 1785328358 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/8492/statm): 531 226 485 147 0 384 0 [pid=8492] vsize: 2124 Raw data (/proc/8496/stat): 8496 (minisat+_64-bit) R 8492 8492 30740 0 -1 0 28213 0 0 0 111553 199 0 0 25 0 1 0 1785328363 115511296 27845 4294967295 134512640 135094434 3221224448 3221223080 134557561 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/8496/statm): 28201 27845 145 145 0 28056 0 [pid=8496] vsize: 112804 Current children cumulated CPU time (s) 1117.53 Current children cumulated vsize (Kb) 114928 [startup+1130.09 s] Raw data (loadavg): 1.00 0.99 0.92 2/57 8496 Raw data (/proc/8492/stat): 8492 (minisat+_script) S 8491 8492 30740 0 -1 0 289 239 0 0 0 0 0 1 18 0 1 0 1785328358 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/8492/statm): 531 226 485 147 0 384 0 [pid=8492] vsize: 2124 Raw data (/proc/8496/stat): 8496 (minisat+_64-bit) R 8492 8492 30740 0 -1 0 28213 0 0 0 112554 199 0 0 25 0 1 0 1785328363 115511296 27845 4294967295 134512640 135094434 3221224448 3221223104 134558249 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/8496/statm): 28201 27845 145 145 0 28056 0 [pid=8496] vsize: 112804 Current children cumulated CPU time (s) 1127.54 Current children cumulated vsize (Kb) 114928 [startup+1140.09 s] Raw data (loadavg): 1.00 0.99 0.92 2/57 8496 Raw data (/proc/8492/stat): 8492 (minisat+_script) S 8491 8492 30740 0 -1 0 289 239 0 0 0 0 0 1 18 0 1 0 1785328358 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/8492/statm): 531 226 485 147 0 384 0 [pid=8492] vsize: 2124 Raw data (/proc/8496/stat): 8496 (minisat+_64-bit) R 8492 8492 30740 0 -1 0 28213 0 0 0 113554 199 0 0 25 0 1 0 1785328363 115511296 27845 4294967295 134512640 135094434 3221224448 3221223104 134558218 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/8496/statm): 28201 27845 145 145 0 28056 0 [pid=8496] vsize: 112804 Current children cumulated CPU time (s) 1137.54 Current children cumulated vsize (Kb) 114928 [startup+1150.09 s] Raw data (loadavg): 1.00 0.99 0.92 2/57 8496 Raw data (/proc/8492/stat): 8492 (minisat+_script) S 8491 8492 30740 0 -1 0 289 239 0 0 0 0 0 1 18 0 1 0 1785328358 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/8492/statm): 531 226 485 147 0 384 0 [pid=8492] vsize: 2124 Raw data (/proc/8496/stat): 8496 (minisat+_64-bit) R 8492 8492 30740 0 -1 0 28213 0 0 0 114554 199 0 0 25 0 1 0 1785328363 115511296 27845 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/8496/statm): 28201 27845 145 145 0 28056 0 [pid=8496] vsize: 112804 Current children cumulated CPU time (s) 1147.54 Current children cumulated vsize (Kb) 114928 [startup+1160.09 s] Raw data (loadavg): 1.00 0.99 0.92 2/57 8496 Raw data (/proc/8492/stat): 8492 (minisat+_script) S 8491 8492 30740 0 -1 0 289 239 0 0 0 0 0 1 18 0 1 0 1785328358 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/8492/statm): 531 226 485 147 0 384 0 [pid=8492] vsize: 2124 Raw data (/proc/8496/stat): 8496 (minisat+_64-bit) R 8492 8492 30740 0 -1 0 28213 0 0 0 115554 199 0 0 25 0 1 0 1785328363 115511296 27845 4294967295 134512640 135094434 3221224448 3221223072 134562085 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/8496/statm): 28201 27845 145 145 0 28056 0 [pid=8496] vsize: 112804 Current children cumulated CPU time (s) 1157.54 Current children cumulated vsize (Kb) 114928 [startup+1170.09 s] Raw data (loadavg): 1.00 0.99 0.92 2/57 8496 Raw data (/proc/8492/stat): 8492 (minisat+_script) S 8491 8492 30740 0 -1 0 289 239 0 0 0 0 0 1 18 0 1 0 1785328358 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/8492/statm): 531 226 485 147 0 384 0 [pid=8492] vsize: 2124 Raw data (/proc/8496/stat): 8496 (minisat+_64-bit) R 8492 8492 30740 0 -1 0 28213 0 0 0 116554 199 0 0 25 0 1 0 1785328363 115511296 27845 4294967295 134512640 135094434 3221224448 3221223136 134554731 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/8496/statm): 28201 27845 145 145 0 28056 0 [pid=8496] vsize: 112804 Current children cumulated CPU time (s) 1167.54 Current children cumulated vsize (Kb) 114928 [startup+1180.09 s] Raw data (loadavg): 1.00 0.99 0.92 2/57 8496 Raw data (/proc/8492/stat): 8492 (minisat+_script) S 8491 8492 30740 0 -1 0 289 239 0 0 0 0 0 1 18 0 1 0 1785328358 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/8492/statm): 531 226 485 147 0 384 0 [pid=8492] vsize: 2124 Raw data (/proc/8496/stat): 8496 (minisat+_64-bit) R 8492 8492 30740 0 -1 0 28213 0 0 0 117555 199 0 0 25 0 1 0 1785328363 115511296 27845 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/8496/statm): 28201 27845 145 145 0 28056 0 [pid=8496] vsize: 112804 Current children cumulated CPU time (s) 1177.55 Current children cumulated vsize (Kb) 114928 [startup+1190.09 s] Raw data (loadavg): 1.00 0.99 0.92 2/57 8496 Raw data (/proc/8492/stat): 8492 (minisat+_script) S 8491 8492 30740 0 -1 0 289 239 0 0 0 0 0 1 18 0 1 0 1785328358 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/8492/statm): 531 226 485 147 0 384 0 [pid=8492] vsize: 2124 Raw data (/proc/8496/stat): 8496 (minisat+_64-bit) R 8492 8492 30740 0 -1 0 28213 0 0 0 118555 199 0 0 25 0 1 0 1785328363 115511296 27845 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/8496/statm): 28201 27845 145 145 0 28056 0 [pid=8496] vsize: 112804 Current children cumulated CPU time (s) 1187.55 Current children cumulated vsize (Kb) 114928 [startup+1200.09 s] Raw data (loadavg): 1.00 0.99 0.92 2/57 8496 Raw data (/proc/8492/stat): 8492 (minisat+_script) S 8491 8492 30740 0 -1 0 289 239 0 0 0 0 0 1 18 0 1 0 1785328358 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/8492/statm): 531 226 485 147 0 384 0 [pid=8492] vsize: 2124 Raw data (/proc/8496/stat): 8496 (minisat+_64-bit) R 8492 8492 30740 0 -1 0 28213 0 0 0 119555 199 0 0 25 0 1 0 1785328363 115511296 27845 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/8496/statm): 28201 27845 145 145 0 28056 0 [pid=8496] vsize: 112804 Current children cumulated CPU time (s) 1197.55 Current children cumulated vsize (Kb) 114928 [startup+1210.09 s] Raw data (loadavg): 1.00 0.99 0.92 2/57 8496 Raw data (/proc/8492/stat): 8492 (minisat+_script) S 8491 8492 30740 0 -1 0 289 239 0 0 0 0 0 1 18 0 1 0 1785328358 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/8492/statm): 531 226 485 147 0 384 0 [pid=8492] vsize: 2124 Raw data (/proc/8496/stat): 8496 (minisat+_64-bit) R 8492 8492 30740 0 -1 0 28213 0 0 0 120556 199 0 0 25 0 1 0 1785328363 115511296 27845 4294967295 134512640 135094434 3221224448 3221223104 134558213 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/8496/statm): 28201 27845 145 145 0 28056 0 [pid=8496] vsize: 112804 Current children cumulated CPU time (s) 1207.56 Current children cumulated vsize (Kb) 114928 Maximum CPU time exceeded: sending SIGTERM then SIGKILL [startup+1210.09 s] Raw data (loadavg): 1.00 0.99 0.92 2/57 8496 Raw data (/proc/8492/stat): 8492 (minisat+_script) S 8491 8492 30740 0 -1 0 289 239 0 0 0 0 0 1 18 0 1 0 1785328358 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/8492/statm): 531 226 485 147 0 384 0 [pid=8492] vsize: 2124 Raw data (/proc/8496/stat): 8496 (minisat+_64-bit) R 8492 8492 30740 0 -1 0 28213 0 0 0 120556 199 0 0 25 0 1 0 1785328363 115511296 27845 4294967295 134512640 135094434 3221224448 3221223040 134557273 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/8496/statm): 28201 27845 145 145 0 28056 0 [pid=8496] vsize: 112804 Current children cumulated CPU time (s) 1207.56 Current children cumulated vsize (Kb) 114928 Sending SIGTERM to -8492 Sleeping 2 seconds One traced child (pid=8492) ended because it received signal 15 (SIGTERM) One traced child (pid=8496) exited with status: 10 All traced children have exited ! Game is over. Child status: 10 Real time (s): 1210.15 CPU time (s): 1207.61 CPU user time (s): 1205.56 CPU system time (s): 2.04869 CPU usage (%): 99.7901 Max. virtual memory (cumulated for all children) (Kb): 114928
ERROR: no interpretation found !