Name | web/www.nlsde.buaa.edu.cn/~kexu/benchmarks/frb56-25-opb/normalized-frb56-25-1.opb |
MD5SUM | 02058527b1ad27d5be75faa6974ffa0f |
Bench Category | optimization, small integers (OPTSMALLINT) |
Has Objective Function | YES |
Satisfiable | YES |
(Un)Satisfiability was proved | YES |
Best value of the objective function | -41 |
Optimality of the best value was proved | NO |
Number of terms in the objective function | 1400 |
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 | 1400 |
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 | 1400 |
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 | 1204.33 |
Number of variables | 1400 |
Total number of constraints | 109676 |
Number of constraints which are clauses | 109676 |
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 wulflinc31 THE 2005-09-18 18:53:07 (client local time) PB2005-SCRIPT v4.0 MARKUPS: idlaunch=2715 boxname=wulflinc31 idbench=371 idsolver=3 numberseed=0 MD5SUM SOLVER: MD5SUM BENCH: 02058527b1ad27d5be75faa6974ffa0f /oldhome/oroussel/tmp/wulflinc31/normalized-frb56-25-1.opb REAL COMMAND: minisat+_script /oldhome/oroussel/tmp/wulflinc31/normalized-frb56-25-1.opb IDLAUNCH: 2715 /proc/cpuinfo: processor : 0 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 3 cpu MHz : 451.153 cache size : 512 KB fdiv_bug : no hlt_bug : no f00f_bug : no coma_bug : no fpu : yes fpu_exception : yes cpuid level : 2 wp : yes flags : fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse bogomips : 888.83 processor : 1 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 3 cpu MHz : 451.153 cache size : 512 KB fdiv_bug : no hlt_bug : no f00f_bug : no coma_bug : no fpu : yes fpu_exception : yes cpuid level : 2 wp : yes flags : fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse bogomips : 901.12 /proc/meminfo: MemTotal: 1034660 kB MemFree: 688072 kB Buffers: 35972 kB Cached: 279552 kB SwapCached: 1016 kB Active: 108116 kB Inactive: 210172 kB HighTotal: 131008 kB HighFree: 252 kB LowTotal: 903652 kB LowFree: 687820 kB SwapTotal: 2097892 kB SwapFree: 2096404 kB Dirty: 28 kB Writeback: 0 kB Mapped: 5772 kB Slab: 22628 kB Committed_AS: 64376 kB PageTables: 340 kB VmallocTotal: 114680 kB VmallocUsed: 1368 kB VmallocChunk: 113252 kB JOB ENDED THE 2005-09-18 19:13:17 (client local time) WITH STATUS 10 IN 1207.11 SECONDS stats: 2715 7 1207.11 10
c Parsing PB file... c Converting 109676 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 | 109676 219352 | 36558 0 0 nan | 0.000 % | c ============================================================================== c [1mFound solution: -39[0m c ---[ 0]---> Sorter-cost:78076 Base: c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 0 | 193374 415660 | 64458 0 0 nan | 0.000 % | c | 100 | 192719 414299 | 70903 63 1093 17.3 | 0.622 % | c | 250 | 192264 413332 | 77994 193 3275 17.0 | 1.071 % | c | 476 | 191415 411505 | 85793 346 4129 11.9 | 1.930 % | c | 813 | 188955 406147 | 94372 570 6726 11.8 | 4.475 % | c | 1319 | 186406 400564 | 103810 962 13044 13.6 | 7.139 % | c | 2078 | 180912 388275 | 114191 1479 18824 12.7 | 13.094 % | c | 3217 | 175709 376585 | 125610 2357 32192 13.7 | 18.778 % | c | 4925 | 166673 356010 | 138171 3574 49702 13.9 | 28.824 % | c | 7487 | 157658 335240 | 151988 5415 74543 13.8 | 39.079 % | c | 11331 | 143138 301148 | 167187 7961 113671 14.3 | 55.865 % | 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 | 12525 | 140763 295746 | 46921 8929 130833 14.7 | 55.865 % | c | 12625 | 139918 293726 | 51613 8922 130380 14.6 | 59.751 % | c | 12775 | 139671 293133 | 56774 9032 131953 14.6 | 60.052 % | c | 13000 | 139283 292232 | 62451 9203 135203 14.7 | 60.501 % | c | 13337 | 138691 290861 | 68697 9414 138503 14.7 | 61.171 % | c | 13843 | 138328 290009 | 75566 9866 147954 15.0 | 61.597 % | c | 14602 | 137121 287145 | 83123 10409 155824 15.0 | 63.131 % | c | 15741 | 135695 283700 | 91435 11210 169938 15.2 | 64.772 % | c | 17449 | 133720 279037 | 100579 12512 198089 15.8 | 67.074 % | c | 20011 | 128643 266845 | 110637 13856 224025 16.2 | 73.177 % | c | 23856 | 125354 258987 | 121700 16543 306442 18.5 | 77.142 % | c | 29622 | 122874 253024 | 133871 20367 492068 24.2 | 80.137 % | 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 | 30967 | 122645 252423 | 40881 21516 531155 24.7 | 80.137 % | c | 31067 | 122645 252423 | 44969 21616 531997 24.6 | 80.427 % | c | 31217 | 122636 252402 | 49466 21757 536269 24.6 | 80.437 % | c | 31442 | 122593 252300 | 54412 21951 542487 24.7 | 80.488 % | c | 31779 | 122436 251912 | 59853 22120 548490 24.8 | 80.684 % | c | 32285 | 122436 251912 | 65839 22626 572074 25.3 | 80.684 % | c | 33044 | 122390 251788 | 72423 23361 600618 25.7 | 80.751 % | c | 34183 | 122320 251616 | 79665 24453 657839 26.9 | 80.840 % | c | 35892 | 122035 250934 | 87632 26003 710446 27.3 | 81.185 % | c | 38454 | 121806 250367 | 96395 28222 984902 34.9 | 81.476 % | 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 | 38938 | 121634 249984 | 40544 28578 1022037 35.8 | 81.476 % | c | 39038 | 121617 249941 | 44598 28653 1023964 35.7 | 81.716 % | c | 39188 | 121349 249292 | 49058 28508 1022934 35.9 | 82.043 % | c | 39413 | 121349 249292 | 53964 28733 1031080 35.9 | 82.043 % | c | 39750 | 121213 248952 | 59360 29014 1043187 36.0 | 82.215 % | c | 40256 | 121088 248654 | 65296 29472 1065725 36.2 | 82.365 % | c | 41015 | 121034 248515 | 71826 30083 1084053 36.0 | 82.437 % | c | 42154 | 120996 248419 | 79008 31210 1134841 36.4 | 82.488 % | c | 43862 | 120814 247954 | 86909 32806 1219139 37.2 | 82.733 % | c | 46425 | 120660 247566 | 95600 35272 1481711 42.0 | 82.934 % | c | 50269 | 120426 247002 | 105160 38769 1679322 43.3 | 83.221 % | 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 | 55508 | 120404 246861 | 40134 43705 2184532 50.0 | 83.221 % | c | 55608 | 120404 246861 | 44147 43805 2187268 49.9 | 83.253 % | c | 55759 | 120401 246854 | 48562 43919 2198441 50.1 | 83.257 % | c | 55984 | 120297 246612 | 53418 44129 2204023 49.9 | 83.377 % | c | 56322 | 120297 246612 | 58760 44467 2221646 50.0 | 83.377 % | c | 56828 | 120262 246523 | 64636 44943 2244896 49.9 | 83.425 % | c | 57588 | 120262 246523 | 71099 45703 2321279 50.8 | 83.425 % | c | 58727 | 120173 246296 | 78209 45708 2347180 51.4 | 83.542 % | c | 60435 | 120173 246296 | 86030 47416 2483476 52.4 | 83.542 % | c | 62998 | 119939 245717 | 94633 49359 2778436 56.3 | 83.841 % | 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 | 65455 | 119986 245861 | 39995 51816 3103184 59.9 | 83.841 % | c | 65555 | 119986 245861 | 43994 51916 3106425 59.8 | 83.823 % | c | 65705 | 119842 245523 | 48393 51870 3106898 59.9 | 83.990 % | c | 65931 | 119801 245428 | 53233 52001 3128578 60.2 | 84.037 % | c | 66268 | 119776 245371 | 58556 52307 3156736 60.4 | 84.064 % | c | 66774 | 119755 245323 | 64412 52795 3188273 60.4 | 84.086 % | c | 67533 | 119752 245316 | 70853 53553 3227607 60.3 | 84.090 % | c | 68672 | 119752 245316 | 77938 54692 3351972 61.3 | 84.090 % | c | 70380 | 119623 244995 | 85732 55978 3468009 62.0 | 84.254 % | c | 72942 | 119551 244815 | 94306 58246 3772441 64.8 | 84.346 % | c | 76786 | 119544 244798 | 103736 62089 4097900 66.0 | 84.355 % | c | 82552 | 119337 244296 | 114110 67497 4883125 72.3 | 84.607 % | 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 | 91183 | 119326 244244 | 39775 75532 5875208 77.8 | 84.607 % | c | 91283 | 119326 244244 | 43752 75632 5876836 77.7 | 84.623 % | c | 91433 | 119326 244244 | 48127 75782 5886804 77.7 | 84.623 % | c | 91658 | 119174 243872 | 52940 75571 5878542 77.8 | 84.815 % | c | 91995 | 119169 243861 | 58234 75798 5913726 78.0 | 84.820 % | c | 92501 | 119169 243861 | 64058 76304 5962450 78.1 | 84.820 % | c | 93260 | 119169 243861 | 70463 77063 6047017 78.5 | 84.820 % | c | 94399 | 119169 243861 | 77510 78202 6141731 78.5 | 84.820 % | c | 96107 | 119164 243850 | 85261 79903 6346087 79.4 | 84.825 % | c | 98670 | 119164 243850 | 93787 82466 6693670 81.2 | 84.825 % | c | 102515 | 119130 243772 | 103166 86111 7282535 84.6 | 84.864 % | c | 108281 | 119010 243470 | 113482 91427 8357465 91.4 | 85.016 % | c | 116930 | 118952 243328 | 124830 100035 9709566 97.1 | 85.089 % | c | 129904 | 118839 243050 | 137314 112031 11367601 101.5 | 85.232 % | c ============================================================================== c [1mFound solution: -49[0m c ---[ 0]---> Sorter-cost: 0 Base: c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 142656 | 118861 243115 | 39620 124783 13424185 107.6 | 85.232 % | c | 142756 | 118809 242989 | 43582 22640 2136428 94.4 | 85.280 % | c | 142906 | 118809 242989 | 47940 22790 2140780 93.9 | 85.280 % | c | 143131 | 118741 242820 | 52734 22993 2162172 94.0 | 85.368 % | c | 143468 | 118741 242820 | 58007 23330 2174648 93.2 | 85.368 % | c | 143974 | 118733 242802 | 63808 23832 2203863 92.5 | 85.376 % | c | 144733 | 118722 242773 | 70189 24588 2263679 92.1 | 85.392 % | c | 145872 | 118722 242773 | 77208 25727 2328778 90.5 | 85.392 % | c | 147580 | 118596 242466 | 84928 27418 2490341 90.8 | 85.549 % | c | 150144 | 118596 242466 | 93421 29982 2825667 94.2 | 85.549 % | c | 153988 | 118581 242431 | 102764 33809 3133516 92.7 | 85.567 % | c | 159757 | 118486 242200 | 113040 39498 3825619 96.9 | 85.685 % | c | 168406 | 118465 242145 | 124344 48141 5116869 106.3 | 85.715 % | c | 181380 | 118409 242007 | 136778 61109 6776970 110.9 | 85.787 % | c | 200842 | 118409 242007 | 150456 80571 9946562 123.5 | 85.787 % | c | 230034 | 118372 241919 | 165502 109697 15616229 142.4 | 85.830 % | c | 273823 | 118197 241494 | 182052 153345 23390472 152.5 | 86.048 % | c c *** TERMINATED *** s SATISFIABLE v -C1400 -C1399 -C1398 -C1397 -C1396 -C1395 -C1394 -C1393 -C1392 -C1391 -C1390 -C1389 -C1388 -C1387 -C1386 -C1385 -C1384 -C1383 C1382 -C1381 -C1380 -C1379 -C1378 -C1377 -C1376 -C1375 -C1374 -C1373 -C1372 -C1371 -C1370 -C1369 -C1368 -C1367 -C1366 -C1365 -C1364 -C1363 -C1362 C1361 -C1360 -C1359 -C1358 -C1357 -C1356 -C1355 -C1354 -C1353 -C1352 -C1351 -C1350 -C1349 -C1348 -C1347 -C1346 -C1345 -C1344 -C1343 -C1342 -C1341 -C1340 -C1339 -C1338 -C1337 -C1336 -C1335 -C1334 -C1333 -C1332 -C1331 -C1330 -C1329 -C1328 C1327 -C1326 -C1325 -C1324 -C1323 -C1322 -C1321 -C1320 -C1319 -C1318 -C1317 -C1316 -C1315 -C1314 -C1313 -C1312 -C1311 -C1310 -C1309 -C1308 -C1307 -C1306 -C1305 -C1304 -C1303 -C1302 C1301 -C1300 -C1299 -C1298 -C1297 -C1296 -C1295 -C1294 -C1293 -C1292 -C1291 -C1290 -C1289 -C1288 -C1287 -C1286 -C1285 -C1284 -C1283 -C1282 -C1281 C1280 -C1279 -C1278 -C1277 -C1276 -C1275 -C1274 -C1273 -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 -C638 -C637 -C636 -C635 -C634 -C633 -C632 -C631 -C630 -C629 -C628 -C627 -C626 -C625 C624 -C623 -C622 -C621 -C620 -C619 -C618 -C617 -C616 -C615 -C614 -C613 -C612 -C611 -C610 -C609 -C608 -C607 -C606 -C605 -C604 -C603 -C602 -C601 -C600 -C599 -C598 -C597 -C596 -C595 -C594 -C593 -C592 -C591 -C590 -C589 -C588 -C587 -C586 -C585 -C584 C583 -C582 -C581 -C580 -C579 -C578 -C577 -C576 C575 -C574 -C573 -C572 -C571 -C570 -C569 -C568 -C567 -C566 -C565 -C564 -C563 -C562 -C561 -C560 -C559 -C558 -C557 -C556 -C555 -C554 -C553 -C552 -C551 -C550 -C549 -C548 -C547 -C546 -C545 -C544 -C543 -C542 -C541 -C540 -C539 -C538 -C537 -C536 -C535 -C534 C533 -C532 -C531 -C530 -C529 -C528 -C527 -C526 -C525 C524 -C523 -C522 -C521 -C520 -C519 -C518 -C517 -C516 -C515 -C514 -C513 -C512 -C511 -C510 -C509 -C508 -C507 -C506 -C505 -C504 -C503 -C502 -C501 -C500 -C499 -C498 -C497 -C496 -C495 -C494 -C493 -C492 -C491 -C490 -C489 -C488 -C487 -C486 -C485 -C484 -C483 -C482 -C481 -C480 -C479 -C478 -C477 C476 -C475 -C474 -C473 -C472 -C471 -C470 -C469 -C468 -C467 -C466 -C465 -C464 -C463 -C462 -C461 -C460 -C459 -C458 C457 -C456 -C455 -C454 -C453 -C452 -C451 -C450 -C449 -C448 -C447 -C446 -C445 -C444 -C443 -C442 -C441 -C440 -C439 -C438 C437 -C436 -C435 -C434 -C433 -C432 -C431 -C430 -C429 -C428 -C427 -C426 -C425 -C424 -C423 -C422 -C421 -C420 -C419 -C418 -C417 -C416 -C415 -C414 -C413 -C412 -C411 -C410 -C409 -C408 -C407 -C406 -C405 -C404 -C403 -C402 -C401 -C400 -C399 -C398 -C397 -C396 -C395 -C394 -C393 -C392 -C391 -C390 -C389 C388 -C387 -C386 -C385 -C384 -C383 -C382 -C381 -C380 -C379 -C378 -C377 -C376 -C375 -C374 -C373 -C372 -C371 -C370 -C369 -C368 -C367 C366 -C365 -C364 -C363 -C362 -C361 -C360 -C359 -C358 -C357 -C356 -C355 -C354 -C353 -C352 -C351 -C350 -C349 -C348 -C347 -C346 -C345 -C344 -C343 -C342 -C341 -C340 -C339 -C338 -C337 -C336 -C335 -C334 -C333 -C332 -C331 -C330 -C329 -C328 -C327 -C326 -C325 -C324 -C323 -C322 -C321 -C320 -C319 -C318 -C317 -C316 -C315 -C314 -C313 -C312 -C311 -C310 -C309 -C308 -C307 -C306 C305 -C304 -C303 -C302 -C301 -C300 -C299 -C298 -C297 -C296 -C295 -C294 -C293 -C292 -C291 -C290 -C289 -C288 -C287 -C286 -C285 -C284 -C283 -C282 -C281 -C280 -C279 C278 -C277 -C276 -C275 -C274 -C273 -C272 -C271 -C270 -C269 -C268 -C267 -C266 -C265 -C264 C263 -C262 -C261 -C260 -C259 -C258 -C257 -C256 -C255 -C254 -C253 -C252 -C251 -C250 C249 -C248 -C247 -C246 -C245 -C244 -C243 -C242 -C241 -C240 -C239 -C238 -C237 -C236 -C235 -C234 -C233 -C232 -C231 -C230 -C229 -C228 -C227 -C226 -C225 C224 -C223 -C222 -C221 -C220 -C219 -C218 -C217 -C216 -C215 -C214 -C213 -C212 -C211 -C210 -C209 -C208 -C207 -C206 -C205 -C204 -C203 -C202 -C201 -C200 C199 -C198 -C197 -C196 -C195 -C194 -C193 -C192 -C191 -C190 -C189 -C188 -C187 -C186 -C185 -C184 -C183 -C182 -C181 -C180 -C179 -C178 -C177 -C176 -C175 -C174 -C173 -C172 -C171 -C170 -C169 -C168 -C167 -C166 -C165 -C164 -C163 -C162 -C161 -C160 -C159 -C158 -C157 -C156 -C155 -C154 -C153 -C152 -C151 -C150 -C149 -C148 -C147 -C146 -C145 -C144 -C143 -C142 -C141 -C140 -C139 -C138 -C137 -C136 -C135 -C134 -C133 -C132 -C131 C130 -C129 -C128 -C127 -C126 -C125 -C124 -C123 -C122 -C121 -C120 -C119 -C118 -C117 -C116 -C115 -C114 -C113 -C112 -C111 -C110 -C109 -C108 -C107 -C106 -C105 -C104 -C103 C102 -C
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/16974/stat): 16974 (minisat+_script) R 16973 16974 9102 0 -1 0 19 0 0 0 0 0 0 0 23 0 1 0 1843524583 712704 3 4294967295 134512640 135087896 3221224512 3221224512 1073744960 0 0 5 0 0 0 0 17 1 0 0 Raw data (/proc/16974/statm): 174 3 169 147 0 27 0 [pid=16974] 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=16975 New process pid=16976 New process pid=16977 One traced child (pid=16976) exited with status: 0 execve syscall for /bin/sed executable 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=16977) exited with status: 0 One traced child (pid=16975) exited with status: 0 New process pid=16978 execve syscall for /oldhome/oroussel/solvers/minisat+_64-bit_static executable open syscall for file /dev/null open syscall for file /oldhome/oroussel/tmp/wulflinc31/normalized-frb56-25-1.opb [startup+10.0045 s] Raw data (loadavg): 0.93 0.96 0.97 2/58 16978 Raw data (/proc/16974/stat): 16974 (minisat+_script) S 16973 16974 9102 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843524583 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/16974/statm): 531 226 485 147 0 384 0 [pid=16974] vsize: 2124 Raw data (/proc/16978/stat): 16978 (minisat+_64-bit) R 16974 16974 9102 0 -1 0 6850 0 0 0 945 28 0 0 25 0 1 0 1843524588 28680192 6837 4294967295 134512640 135094434 3221224448 3221223152 134559005 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/16978/statm): 7002 6837 145 145 0 6857 0 [pid=16978] vsize: 28008 Current children cumulated CPU time (s) 9.73 Current children cumulated vsize (Kb) 30132 [startup+20.0054 s] Raw data (loadavg): 0.94 0.96 0.97 2/58 16980 Raw data (/proc/16974/stat): 16974 (minisat+_script) S 16973 16974 9102 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843524583 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/16974/statm): 531 226 485 147 0 384 0 [pid=16974] vsize: 2124 Raw data (/proc/16978/stat): 16978 (minisat+_64-bit) R 16974 16974 9102 0 -1 0 6850 0 0 0 1944 29 0 0 25 0 1 0 1843524588 28680192 6837 4294967295 134512640 135094434 3221224448 3221223140 134558984 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/16978/statm): 7002 6837 145 145 0 6857 0 [pid=16978] vsize: 28008 Current children cumulated CPU time (s) 19.73 Current children cumulated vsize (Kb) 30132 [startup+30.0064 s] Raw data (loadavg): 0.95 0.96 0.97 2/58 16980 Raw data (/proc/16974/stat): 16974 (minisat+_script) S 16973 16974 9102 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843524583 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/16974/statm): 531 226 485 147 0 384 0 [pid=16974] vsize: 2124 Raw data (/proc/16978/stat): 16978 (minisat+_64-bit) R 16974 16974 9102 0 -1 0 6850 0 0 0 2944 29 0 0 25 0 1 0 1843524588 28680192 6837 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/16978/statm): 7002 6837 145 145 0 6857 0 [pid=16978] vsize: 28008 Current children cumulated CPU time (s) 29.73 Current children cumulated vsize (Kb) 30132 [startup+40.0073 s] Raw data (loadavg): 0.96 0.96 0.97 2/58 16980 Raw data (/proc/16974/stat): 16974 (minisat+_script) S 16973 16974 9102 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843524583 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/16974/statm): 531 226 485 147 0 384 0 [pid=16974] vsize: 2124 Raw data (/proc/16978/stat): 16978 (minisat+_64-bit) R 16974 16974 9102 0 -1 0 6850 0 0 0 3943 29 0 0 25 0 1 0 1843524588 28680192 6837 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/16978/statm): 7002 6837 145 145 0 6857 0 [pid=16978] vsize: 28008 Current children cumulated CPU time (s) 39.72 Current children cumulated vsize (Kb) 30132 [startup+50.0082 s] Raw data (loadavg): 0.96 0.96 0.97 2/58 16980 Raw data (/proc/16974/stat): 16974 (minisat+_script) S 16973 16974 9102 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843524583 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/16974/statm): 531 226 485 147 0 384 0 [pid=16974] vsize: 2124 Raw data (/proc/16978/stat): 16978 (minisat+_64-bit) R 16974 16974 9102 0 -1 0 6850 0 0 0 4943 30 0 0 25 0 1 0 1843524588 28680192 6837 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/16978/statm): 7002 6837 145 145 0 6857 0 [pid=16978] vsize: 28008 Current children cumulated CPU time (s) 49.73 Current children cumulated vsize (Kb) 30132 [startup+60.0091 s] Raw data (loadavg): 0.97 0.96 0.97 2/58 16980 Raw data (/proc/16974/stat): 16974 (minisat+_script) S 16973 16974 9102 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843524583 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/16974/statm): 531 226 485 147 0 384 0 [pid=16974] vsize: 2124 Raw data (/proc/16978/stat): 16978 (minisat+_64-bit) R 16974 16974 9102 0 -1 0 6850 0 0 0 5942 30 0 0 25 0 1 0 1843524588 28680192 6837 4294967295 134512640 135094434 3221224448 3221223132 134553432 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/16978/statm): 7002 6837 145 145 0 6857 0 [pid=16978] vsize: 28008 Current children cumulated CPU time (s) 59.72 Current children cumulated vsize (Kb) 30132 [startup+70.0101 s] Raw data (loadavg): 0.97 0.96 0.97 2/58 16980 Raw data (/proc/16974/stat): 16974 (minisat+_script) S 16973 16974 9102 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843524583 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/16974/statm): 531 226 485 147 0 384 0 [pid=16974] vsize: 2124 Raw data (/proc/16978/stat): 16978 (minisat+_64-bit) R 16974 16974 9102 0 -1 0 6850 0 0 0 6941 31 0 0 25 0 1 0 1843524588 28680192 6837 4294967295 134512640 135094434 3221224448 3221223120 134553437 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/16978/statm): 7002 6837 145 145 0 6857 0 [pid=16978] vsize: 28008 Current children cumulated CPU time (s) 69.72 Current children cumulated vsize (Kb) 30132 [startup+80.011 s] Raw data (loadavg): 0.98 0.96 0.97 2/58 16982 Raw data (/proc/16974/stat): 16974 (minisat+_script) S 16973 16974 9102 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843524583 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/16974/statm): 531 226 485 147 0 384 0 [pid=16974] vsize: 2124 Raw data (/proc/16978/stat): 16978 (minisat+_64-bit) R 16974 16974 9102 0 -1 0 6850 0 0 0 7941 31 0 0 25 0 1 0 1843524588 28680192 6837 4294967295 134512640 135094434 3221224448 3221223108 134553446 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/16978/statm): 7002 6837 145 145 0 6857 0 [pid=16978] vsize: 28008 Current children cumulated CPU time (s) 79.72 Current children cumulated vsize (Kb) 30132 [startup+90.0119 s] Raw data (loadavg): 0.98 0.96 0.97 2/58 16982 Raw data (/proc/16974/stat): 16974 (minisat+_script) S 16973 16974 9102 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843524583 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/16974/statm): 531 226 485 147 0 384 0 [pid=16974] vsize: 2124 Raw data (/proc/16978/stat): 16978 (minisat+_64-bit) R 16974 16974 9102 0 -1 0 6850 0 0 0 8941 32 0 0 25 0 1 0 1843524588 28680192 6837 4294967295 134512640 135094434 3221224448 3221223108 134553482 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/16978/statm): 7002 6837 145 145 0 6857 0 [pid=16978] vsize: 28008 Current children cumulated CPU time (s) 89.73 Current children cumulated vsize (Kb) 30132 [startup+100.013 s] Raw data (loadavg): 0.98 0.96 0.97 2/58 16982 Raw data (/proc/16974/stat): 16974 (minisat+_script) S 16973 16974 9102 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843524583 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/16974/statm): 531 226 485 147 0 384 0 [pid=16974] vsize: 2124 Raw data (/proc/16978/stat): 16978 (minisat+_64-bit) R 16974 16974 9102 0 -1 0 6850 0 0 0 9941 32 0 0 25 0 1 0 1843524588 28680192 6837 4294967295 134512640 135094434 3221224448 3221223116 134553438 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/16978/statm): 7002 6837 145 145 0 6857 0 [pid=16978] vsize: 28008 Current children cumulated CPU time (s) 99.73 Current children cumulated vsize (Kb) 30132 [startup+110.015 s] Raw data (loadavg): 0.98 0.97 0.97 2/58 16982 Raw data (/proc/16974/stat): 16974 (minisat+_script) S 16973 16974 9102 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843524583 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/16974/statm): 531 226 485 147 0 384 0 [pid=16974] vsize: 2124 Raw data (/proc/16978/stat): 16978 (minisat+_64-bit) R 16974 16974 9102 0 -1 0 6850 0 0 0 10941 32 0 0 25 0 1 0 1843524588 28680192 6837 4294967295 134512640 135094434 3221224448 3221223108 134553515 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/16978/statm): 7002 6837 145 145 0 6857 0 [pid=16978] vsize: 28008 Current children cumulated CPU time (s) 109.73 Current children cumulated vsize (Kb) 30132 [startup+120.016 s] Raw data (loadavg): 0.99 0.97 0.97 2/58 16982 Raw data (/proc/16974/stat): 16974 (minisat+_script) S 16973 16974 9102 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843524583 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/16974/statm): 531 226 485 147 0 384 0 [pid=16974] vsize: 2124 Raw data (/proc/16978/stat): 16978 (minisat+_64-bit) R 16974 16974 9102 0 -1 0 6850 0 0 0 11941 32 0 0 25 0 1 0 1843524588 28680192 6837 4294967295 134512640 135094434 3221224448 3221223108 134553446 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/16978/statm): 7002 6837 145 145 0 6857 0 [pid=16978] vsize: 28008 Current children cumulated CPU time (s) 119.73 Current children cumulated vsize (Kb) 30132 [startup+130.016 s] Raw data (loadavg): 0.99 0.97 0.97 2/58 16982 Raw data (/proc/16974/stat): 16974 (minisat+_script) S 16973 16974 9102 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843524583 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/16974/statm): 531 226 485 147 0 384 0 [pid=16974] vsize: 2124 Raw data (/proc/16978/stat): 16978 (minisat+_64-bit) R 16974 16974 9102 0 -1 0 6850 0 0 0 12941 32 0 0 25 0 1 0 1843524588 28680192 6837 4294967295 134512640 135094434 3221224448 3221223108 134553501 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/16978/statm): 7002 6837 145 145 0 6857 0 [pid=16978] vsize: 28008 Current children cumulated CPU time (s) 129.73 Current children cumulated vsize (Kb) 30132 [startup+140.017 s] Raw data (loadavg): 0.99 0.97 0.97 2/58 16984 Raw data (/proc/16974/stat): 16974 (minisat+_script) S 16973 16974 9102 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843524583 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/16974/statm): 531 226 485 147 0 384 0 [pid=16974] vsize: 2124 Raw data (/proc/16978/stat): 16978 (minisat+_64-bit) R 16974 16974 9102 0 -1 0 6850 0 0 0 13941 32 0 0 25 0 1 0 1843524588 28680192 6837 4294967295 134512640 135094434 3221224448 3221223072 134557612 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/16978/statm): 7002 6837 145 145 0 6857 0 [pid=16978] vsize: 28008 Current children cumulated CPU time (s) 139.73 Current children cumulated vsize (Kb) 30132 [startup+150.017 s] Raw data (loadavg): 0.99 0.97 0.97 2/58 16984 Raw data (/proc/16974/stat): 16974 (minisat+_script) S 16973 16974 9102 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843524583 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/16974/statm): 531 226 485 147 0 384 0 [pid=16974] vsize: 2124 Raw data (/proc/16978/stat): 16978 (minisat+_64-bit) R 16974 16974 9102 0 -1 0 6850 0 0 0 14941 32 0 0 25 0 1 0 1843524588 28680192 6837 4294967295 134512640 135094434 3221224448 3221223108 134553446 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/16978/statm): 7002 6837 145 145 0 6857 0 [pid=16978] vsize: 28008 Current children cumulated CPU time (s) 149.73 Current children cumulated vsize (Kb) 30132 [startup+160.018 s] Raw data (loadavg): 0.99 0.97 0.97 2/58 16984 Raw data (/proc/16974/stat): 16974 (minisat+_script) S 16973 16974 9102 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843524583 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/16974/statm): 531 226 485 147 0 384 0 [pid=16974] vsize: 2124 Raw data (/proc/16978/stat): 16978 (minisat+_64-bit) R 16974 16974 9102 0 -1 0 7092 0 0 0 15938 34 0 0 25 0 1 0 1843524588 29339648 7004 4294967295 134512640 135094434 3221224448 3221223104 134670074 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/16978/statm): 7163 7004 145 145 0 7018 0 [pid=16978] vsize: 28652 Current children cumulated CPU time (s) 159.72 Current children cumulated vsize (Kb) 30776 [startup+170.019 s] Raw data (loadavg): 0.99 0.97 0.97 2/58 16984 Raw data (/proc/16974/stat): 16974 (minisat+_script) S 16973 16974 9102 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843524583 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/16974/statm): 531 226 485 147 0 384 0 [pid=16974] vsize: 2124 Raw data (/proc/16978/stat): 16978 (minisat+_64-bit) R 16974 16974 9102 0 -1 0 7345 0 0 0 16933 35 0 0 25 0 1 0 1843524588 30375936 7257 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/16978/statm): 7416 7257 145 145 0 7271 0 [pid=16978] vsize: 29664 Current children cumulated CPU time (s) 169.68 Current children cumulated vsize (Kb) 31788 [startup+180.019 s] Raw data (loadavg): 0.99 0.97 0.97 2/58 16984 Raw data (/proc/16974/stat): 16974 (minisat+_script) S 16973 16974 9102 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843524583 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/16974/statm): 531 226 485 147 0 384 0 [pid=16974] vsize: 2124 Raw data (/proc/16978/stat): 16978 (minisat+_64-bit) R 16974 16974 9102 0 -1 0 7801 0 0 0 17928 37 0 0 25 0 1 0 1843524588 31936512 7638 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/16978/statm): 7797 7638 145 145 0 7652 0 [pid=16978] vsize: 31188 Current children cumulated CPU time (s) 179.65 Current children cumulated vsize (Kb) 33312 [startup+190.02 s] Raw data (loadavg): 0.99 0.97 0.97 1/58 16984 Raw data (/proc/16974/stat): 16974 (minisat+_script) S 16973 16974 9102 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843524583 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/16974/statm): 531 226 485 147 0 384 0 [pid=16974] vsize: 2124 Raw data (/proc/16978/stat): 16978 (minisat+_64-bit) T 16974 16974 9102 0 -1 0 8219 0 0 0 18921 39 0 0 25 0 1 0 1843524588 33767424 8056 4294967295 134512640 135094434 3221224448 3221222828 134870330 0 0 5 16386 3222434794 0 0 17 0 0 0 Raw data (/proc/16978/statm): 8244 8056 145 145 0 8099 0 [pid=16978] vsize: 32976 Current children cumulated CPU time (s) 189.6 Current children cumulated vsize (Kb) 35100 [startup+200.021 s] Raw data (loadavg): 0.99 0.97 0.97 2/58 16986 Raw data (/proc/16974/stat): 16974 (minisat+_script) S 16973 16974 9102 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843524583 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/16974/statm): 531 226 485 147 0 384 0 [pid=16974] vsize: 2124 Raw data (/proc/16978/stat): 16978 (minisat+_64-bit) R 16974 16974 9102 0 -1 0 8592 0 0 0 19914 42 0 0 25 0 1 0 1843524588 35274752 8429 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/16978/statm): 8612 8429 145 145 0 8467 0 [pid=16978] vsize: 34448 Current children cumulated CPU time (s) 199.56 Current children cumulated vsize (Kb) 36572 [startup+210.022 s] Raw data (loadavg): 0.99 0.97 0.97 2/58 16986 Raw data (/proc/16974/stat): 16974 (minisat+_script) S 16973 16974 9102 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843524583 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/16974/statm): 531 226 485 147 0 384 0 [pid=16974] vsize: 2124 Raw data (/proc/16978/stat): 16978 (minisat+_64-bit) R 16974 16974 9102 0 -1 0 9140 0 0 0 20905 45 0 0 25 0 1 0 1843524588 37191680 8901 4294967295 134512640 135094434 3221224448 3221223108 134553482 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/16978/statm): 9080 8901 145 145 0 8935 0 [pid=16978] vsize: 36320 Current children cumulated CPU time (s) 209.5 Current children cumulated vsize (Kb) 38444 [startup+220.023 s] Raw data (loadavg): 0.99 0.97 0.97 2/58 16986 Raw data (/proc/16974/stat): 16974 (minisat+_script) S 16973 16974 9102 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843524583 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/16974/statm): 531 226 485 147 0 384 0 [pid=16974] vsize: 2124 Raw data (/proc/16978/stat): 16978 (minisat+_64-bit) R 16974 16974 9102 0 -1 0 9436 0 0 0 21899 47 0 0 25 0 1 0 1843524588 38391808 9197 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/16978/statm): 9373 9197 145 145 0 9228 0 [pid=16978] vsize: 37492 Current children cumulated CPU time (s) 219.46 Current children cumulated vsize (Kb) 39616 [startup+230.023 s] Raw data (loadavg): 0.99 0.97 0.97 2/58 16986 Raw data (/proc/16974/stat): 16974 (minisat+_script) S 16973 16974 9102 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843524583 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/16974/statm): 531 226 485 147 0 384 0 [pid=16974] vsize: 2124 Raw data (/proc/16978/stat): 16978 (minisat+_64-bit) R 16974 16974 9102 0 -1 0 9864 0 0 0 22892 51 0 0 25 0 1 0 1843524588 40132608 9625 4294967295 134512640 135094434 3221224448 3221223120 134556252 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/16978/statm): 9798 9625 145 145 0 9653 0 [pid=16978] vsize: 39192 Current children cumulated CPU time (s) 229.43 Current children cumulated vsize (Kb) 41316 [startup+240.024 s] Raw data (loadavg): 0.99 0.97 0.97 2/58 16986 Raw data (/proc/16974/stat): 16974 (minisat+_script) S 16973 16974 9102 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843524583 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/16974/statm): 531 226 485 147 0 384 0 [pid=16974] vsize: 2124 Raw data (/proc/16978/stat): 16978 (minisat+_64-bit) R 16974 16974 9102 0 -1 0 10278 0 0 0 23886 53 0 0 25 0 1 0 1843524588 41508864 9963 4294967295 134512640 135094434 3221224448 3221223104 134558235 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/16978/statm): 10134 9963 145 145 0 9989 0 [pid=16978] vsize: 40536 Current children cumulated CPU time (s) 239.39 Current children cumulated vsize (Kb) 42660 [startup+250.025 s] Raw data (loadavg): 0.99 0.97 0.97 2/58 16986 Raw data (/proc/16974/stat): 16974 (minisat+_script) S 16973 16974 9102 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843524583 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/16974/statm): 531 226 485 147 0 384 0 [pid=16974] vsize: 2124 Raw data (/proc/16978/stat): 16978 (minisat+_64-bit) R 16974 16974 9102 0 -1 0 10594 0 0 0 24881 56 0 0 25 0 1 0 1843524588 42790912 10279 4294967295 134512640 135094434 3221224448 3221223108 134553508 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/16978/statm): 10447 10279 145 145 0 10302 0 [pid=16978] vsize: 41788 Current children cumulated CPU time (s) 249.37 Current children cumulated vsize (Kb) 43912 [startup+260.027 s] Raw data (loadavg): 0.99 0.97 0.97 2/58 16988 Raw data (/proc/16974/stat): 16974 (minisat+_script) S 16973 16974 9102 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843524583 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/16974/statm): 531 226 485 147 0 384 0 [pid=16974] vsize: 2124 Raw data (/proc/16978/stat): 16978 (minisat+_64-bit) R 16974 16974 9102 0 -1 0 11012 0 0 0 25873 61 0 0 25 0 1 0 1843524588 44490752 10697 4294967295 134512640 135094434 3221224448 3221223104 134557964 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/16978/statm): 10862 10697 145 145 0 10717 0 [pid=16978] vsize: 43448 Current children cumulated CPU time (s) 259.34 Current children cumulated vsize (Kb) 45572 [startup+270.028 s] Raw data (loadavg): 0.99 0.97 0.97 2/58 16988 Raw data (/proc/16974/stat): 16974 (minisat+_script) S 16973 16974 9102 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843524583 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/16974/statm): 531 226 485 147 0 384 0 [pid=16974] vsize: 2124 Raw data (/proc/16978/stat): 16978 (minisat+_64-bit) R 16974 16974 9102 0 -1 0 11356 0 0 0 26866 64 0 0 25 0 1 0 1843524588 45883392 11041 4294967295 134512640 135094434 3221224448 3221223104 134558221 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/16978/statm): 11202 11041 145 145 0 11057 0 [pid=16978] vsize: 44808 Current children cumulated CPU time (s) 269.3 Current children cumulated vsize (Kb) 46932 [startup+280.029 s] Raw data (loadavg): 0.99 0.97 0.97 2/58 16988 Raw data (/proc/16974/stat): 16974 (minisat+_script) S 16973 16974 9102 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843524583 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/16974/statm): 531 226 485 147 0 384 0 [pid=16974] vsize: 2124 Raw data (/proc/16978/stat): 16978 (minisat+_64-bit) R 16974 16974 9102 0 -1 0 11802 0 0 0 27858 67 0 0 25 0 1 0 1843524588 47960064 11487 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/16978/statm): 11709 11487 145 145 0 11564 0 [pid=16978] vsize: 46836 Current children cumulated CPU time (s) 279.25 Current children cumulated vsize (Kb) 48960 [startup+290.031 s] Raw data (loadavg): 0.99 0.97 0.97 2/58 16988 Raw data (/proc/16974/stat): 16974 (minisat+_script) S 16973 16974 9102 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843524583 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/16974/statm): 531 226 485 147 0 384 0 [pid=16974] vsize: 2124 Raw data (/proc/16978/stat): 16978 (minisat+_64-bit) R 16974 16974 9102 0 -1 0 12189 0 0 0 28849 71 0 0 25 0 1 0 1843524588 49537024 11874 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/16978/statm): 12094 11874 145 145 0 11949 0 [pid=16978] vsize: 48376 Current children cumulated CPU time (s) 289.2 Current children cumulated vsize (Kb) 50500 [startup+300.031 s] Raw data (loadavg): 0.99 0.97 0.97 2/58 16988 Raw data (/proc/16974/stat): 16974 (minisat+_script) S 16973 16974 9102 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843524583 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/16974/statm): 531 226 485 147 0 384 0 [pid=16974] vsize: 2124 Raw data (/proc/16978/stat): 16978 (minisat+_64-bit) R 16974 16974 9102 0 -1 0 12614 0 0 0 29841 74 0 0 25 0 1 0 1843524588 51265536 12299 4294967295 134512640 135094434 3221224448 3221223104 134558249 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/16978/statm): 12516 12299 145 145 0 12371 0 [pid=16978] vsize: 50064 Current children cumulated CPU time (s) 299.15 Current children cumulated vsize (Kb) 52188 [startup+310.032 s] Raw data (loadavg): 0.99 0.97 0.97 2/58 16988 Raw data (/proc/16974/stat): 16974 (minisat+_script) S 16973 16974 9102 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843524583 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/16974/statm): 531 226 485 147 0 384 0 [pid=16974] vsize: 2124 Raw data (/proc/16978/stat): 16978 (minisat+_64-bit) R 16974 16974 9102 0 -1 0 13069 0 0 0 30833 78 0 0 25 0 1 0 1843524588 53112832 12754 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/16978/statm): 12967 12754 145 145 0 12822 0 [pid=16978] vsize: 51868 Current children cumulated CPU time (s) 309.11 Current children cumulated vsize (Kb) 53992 [startup+320.033 s] Raw data (loadavg): 0.99 0.97 0.97 2/58 16990 Raw data (/proc/16974/stat): 16974 (minisat+_script) S 16973 16974 9102 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843524583 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/16974/statm): 531 226 485 147 0 384 0 [pid=16974] vsize: 2124 Raw data (/proc/16978/stat): 16978 (minisat+_64-bit) R 16974 16974 9102 0 -1 0 13381 0 0 0 31826 82 0 0 25 0 1 0 1843524588 54079488 12991 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/16978/statm): 13203 12991 145 145 0 13058 0 [pid=16978] vsize: 52812 Current children cumulated CPU time (s) 319.08 Current children cumulated vsize (Kb) 54936 [startup+330.034 s] Raw data (loadavg): 0.99 0.97 0.97 2/58 16990 Raw data (/proc/16974/stat): 16974 (minisat+_script) S 16973 16974 9102 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843524583 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/16974/statm): 531 226 485 147 0 384 0 [pid=16974] vsize: 2124 Raw data (/proc/16978/stat): 16978 (minisat+_64-bit) R 16974 16974 9102 0 -1 0 13698 0 0 0 32821 83 0 0 25 0 1 0 1843524588 55365632 13308 4294967295 134512640 135094434 3221224448 3221223104 134558004 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/16978/statm): 13517 13308 145 145 0 13372 0 [pid=16978] vsize: 54068 Current children cumulated CPU time (s) 329.04 Current children cumulated vsize (Kb) 56192 [startup+340.035 s] Raw data (loadavg): 0.99 0.97 0.97 2/58 16990 Raw data (/proc/16974/stat): 16974 (minisat+_script) S 16973 16974 9102 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843524583 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/16974/statm): 531 226 485 147 0 384 0 [pid=16974] vsize: 2124 Raw data (/proc/16978/stat): 16978 (minisat+_64-bit) R 16974 16974 9102 0 -1 0 14120 0 0 0 33813 88 0 0 25 0 1 0 1843524588 57081856 13730 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/16978/statm): 13936 13730 145 145 0 13791 0 [pid=16978] vsize: 55744 Current children cumulated CPU time (s) 339.01 Current children cumulated vsize (Kb) 57868 [startup+350.036 s] Raw data (loadavg): 0.99 0.97 0.97 2/58 16990 Raw data (/proc/16974/stat): 16974 (minisat+_script) S 16973 16974 9102 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843524583 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/16974/statm): 531 226 485 147 0 384 0 [pid=16974] vsize: 2124 Raw data (/proc/16978/stat): 16978 (minisat+_64-bit) R 16974 16974 9102 0 -1 0 14519 0 0 0 34806 90 0 0 25 0 1 0 1843524588 58707968 14129 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/16978/statm): 14333 14129 145 145 0 14188 0 [pid=16978] vsize: 57332 Current children cumulated CPU time (s) 348.96 Current children cumulated vsize (Kb) 59456 [startup+360.038 s] Raw data (loadavg): 0.99 0.97 0.97 2/58 16990 Raw data (/proc/16974/stat): 16974 (minisat+_script) S 16973 16974 9102 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843524583 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/16974/statm): 531 226 485 147 0 384 0 [pid=16974] vsize: 2124 Raw data (/proc/16978/stat): 16978 (minisat+_64-bit) R 16974 16974 9102 0 -1 0 14919 0 0 0 35800 93 0 0 25 0 1 0 1843524588 60338176 14529 4294967295 134512640 135094434 3221224448 3221223104 134558249 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/16978/statm): 14731 14529 145 145 0 14586 0 [pid=16978] vsize: 58924 Current children cumulated CPU time (s) 358.93 Current children cumulated vsize (Kb) 61048 [startup+370.039 s] Raw data (loadavg): 0.99 0.97 0.97 2/58 16990 Raw data (/proc/16974/stat): 16974 (minisat+_script) S 16973 16974 9102 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843524583 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/16974/statm): 531 226 485 147 0 384 0 [pid=16974] vsize: 2124 Raw data (/proc/16978/stat): 16978 (minisat+_64-bit) R 16974 16974 9102 0 -1 0 15396 0 0 0 36792 96 0 0 25 0 1 0 1843524588 62279680 15006 4294967295 134512640 135094434 3221224448 3221223104 134558218 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/16978/statm): 15205 15006 145 145 0 15060 0 [pid=16978] vsize: 60820 Current children cumulated CPU time (s) 368.88 Current children cumulated vsize (Kb) 62944 [startup+380.039 s] Raw data (loadavg): 0.99 0.97 0.97 2/58 16992 Raw data (/proc/16974/stat): 16974 (minisat+_script) S 16973 16974 9102 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843524583 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/16974/statm): 531 226 485 147 0 384 0 [pid=16974] vsize: 2124 Raw data (/proc/16978/stat): 16978 (minisat+_64-bit) R 16974 16974 9102 0 -1 0 15912 0 0 0 37783 100 0 0 25 0 1 0 1843524588 64385024 15522 4294967295 134512640 135094434 3221224448 3221223108 134553482 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/16978/statm): 15719 15522 145 145 0 15574 0 [pid=16978] vsize: 62876 Current children cumulated CPU time (s) 378.83 Current children cumulated vsize (Kb) 65000 [startup+390.04 s] Raw data (loadavg): 0.99 0.97 0.97 2/58 16992 Raw data (/proc/16974/stat): 16974 (minisat+_script) S 16973 16974 9102 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843524583 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/16974/statm): 531 226 485 147 0 384 0 [pid=16974] vsize: 2124 Raw data (/proc/16978/stat): 16978 (minisat+_64-bit) R 16974 16974 9102 0 -1 0 16250 0 0 0 38778 103 0 0 25 0 1 0 1843524588 65761280 15860 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/16978/statm): 16055 15860 145 145 0 15910 0 [pid=16978] vsize: 64220 Current children cumulated CPU time (s) 388.81 Current children cumulated vsize (Kb) 66344 [startup+400.041 s] Raw data (loadavg): 0.99 0.97 0.97 2/58 16992 Raw data (/proc/16974/stat): 16974 (minisat+_script) S 16973 16974 9102 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843524583 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/16974/statm): 531 226 485 147 0 384 0 [pid=16974] vsize: 2124 Raw data (/proc/16978/stat): 16978 (minisat+_64-bit) R 16974 16974 9102 0 -1 0 16603 0 0 0 39772 105 0 0 25 0 1 0 1843524588 67198976 16213 4294967295 134512640 135094434 3221224448 3221223136 134554793 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/16978/statm): 16406 16213 145 145 0 16261 0 [pid=16978] vsize: 65624 Current children cumulated CPU time (s) 398.77 Current children cumulated vsize (Kb) 67748 [startup+410.042 s] Raw data (loadavg): 0.99 0.97 0.97 2/58 16992 Raw data (/proc/16974/stat): 16974 (minisat+_script) S 16973 16974 9102 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843524583 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/16974/statm): 531 226 485 147 0 384 0 [pid=16974] vsize: 2124 Raw data (/proc/16978/stat): 16978 (minisat+_64-bit) R 16974 16974 9102 0 -1 0 16980 0 0 0 40766 107 0 0 25 0 1 0 1843524588 68730880 16590 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/16978/statm): 16780 16590 145 145 0 16635 0 [pid=16978] vsize: 67120 Current children cumulated CPU time (s) 408.73 Current children cumulated vsize (Kb) 69244 [startup+420.043 s] Raw data (loadavg): 0.99 0.97 0.97 2/58 16992 Raw data (/proc/16974/stat): 16974 (minisat+_script) S 16973 16974 9102 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843524583 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/16974/statm): 531 226 485 147 0 384 0 [pid=16974] vsize: 2124 Raw data (/proc/16978/stat): 16978 (minisat+_64-bit) R 16974 16974 9102 0 -1 0 17381 0 0 0 41758 110 0 0 25 0 1 0 1843524588 70365184 16991 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/16978/statm): 17179 16991 145 145 0 17034 0 [pid=16978] vsize: 68716 Current children cumulated CPU time (s) 418.68 Current children cumulated vsize (Kb) 70840 [startup+430.044 s] Raw data (loadavg): 0.99 0.97 0.97 2/58 16992 Raw data (/proc/16974/stat): 16974 (minisat+_script) S 16973 16974 9102 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843524583 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/16974/statm): 531 226 485 147 0 384 0 [pid=16974] vsize: 2124 Raw data (/proc/16978/stat): 16978 (minisat+_64-bit) R 16974 16974 9102 0 -1 0 17839 0 0 0 42751 113 0 0 25 0 1 0 1843524588 72232960 17449 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/16978/statm): 17635 17449 145 145 0 17490 0 [pid=16978] vsize: 70540 Current children cumulated CPU time (s) 428.64 Current children cumulated vsize (Kb) 72664 [startup+440.045 s] Raw data (loadavg): 0.99 0.97 0.97 2/58 16994 Raw data (/proc/16974/stat): 16974 (minisat+_script) S 16973 16974 9102 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843524583 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/16974/statm): 531 226 485 147 0 384 0 [pid=16974] vsize: 2124 Raw data (/proc/16978/stat): 16978 (minisat+_64-bit) R 16974 16974 9102 0 -1 0 18162 0 0 0 43745 115 0 0 25 0 1 0 1843524588 73547776 17772 4294967295 134512640 135094434 3221224448 3221223104 134558007 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/16978/statm): 17956 17772 145 145 0 17811 0 [pid=16978] vsize: 71824 Current children cumulated CPU time (s) 438.6 Current children cumulated vsize (Kb) 73948 [startup+450.045 s] Raw data (loadavg): 0.99 0.97 0.97 2/58 16994 Raw data (/proc/16974/stat): 16974 (minisat+_script) S 16973 16974 9102 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843524583 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/16974/statm): 531 226 485 147 0 384 0 [pid=16974] vsize: 2124 Raw data (/proc/16978/stat): 16978 (minisat+_64-bit) R 16974 16974 9102 0 -1 0 18386 0 0 0 44741 118 0 0 25 0 1 0 1843524588 74457088 17996 4294967295 134512640 135094434 3221224448 3221223040 134557180 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/16978/statm): 18178 17996 145 145 0 18033 0 [pid=16978] vsize: 72712 Current children cumulated CPU time (s) 448.59 Current children cumulated vsize (Kb) 74836 [startup+460.046 s] Raw data (loadavg): 0.99 0.97 0.97 2/58 16994 Raw data (/proc/16974/stat): 16974 (minisat+_script) S 16973 16974 9102 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843524583 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/16974/statm): 531 226 485 147 0 384 0 [pid=16974] vsize: 2124 Raw data (/proc/16978/stat): 16978 (minisat+_64-bit) R 16974 16974 9102 0 -1 0 18689 0 0 0 45737 119 0 0 25 0 1 0 1843524588 75694080 18299 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/16978/statm): 18480 18299 145 145 0 18335 0 [pid=16978] vsize: 73920 Current children cumulated CPU time (s) 458.56 Current children cumulated vsize (Kb) 76044 [startup+470.047 s] Raw data (loadavg): 0.99 0.97 0.97 2/58 16994 Raw data (/proc/16974/stat): 16974 (minisat+_script) S 16973 16974 9102 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843524583 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/16974/statm): 531 226 485 147 0 384 0 [pid=16974] vsize: 2124 Raw data (/proc/16978/stat): 16978 (minisat+_64-bit) R 16974 16974 9102 0 -1 0 18965 0 0 0 46732 121 0 0 25 0 1 0 1843524588 76812288 18575 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/16978/statm): 18753 18575 145 145 0 18608 0 [pid=16978] vsize: 75012 Current children cumulated CPU time (s) 468.53 Current children cumulated vsize (Kb) 77136 [startup+480.048 s] Raw data (loadavg): 0.99 0.97 0.97 2/58 16994 Raw data (/proc/16974/stat): 16974 (minisat+_script) S 16973 16974 9102 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843524583 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/16974/statm): 531 226 485 147 0 384 0 [pid=16974] vsize: 2124 Raw data (/proc/16978/stat): 16978 (minisat+_64-bit) R 16974 16974 9102 0 -1 0 19288 0 0 0 47726 124 0 0 25 0 1 0 1843524588 78127104 18898 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/16978/statm): 19074 18898 145 145 0 18929 0 [pid=16978] vsize: 76296 Current children cumulated CPU time (s) 478.5 Current children cumulated vsize (Kb) 78420 [startup+490.049 s] Raw data (loadavg): 0.99 0.97 0.97 2/58 16994 Raw data (/proc/16974/stat): 16974 (minisat+_script) S 16973 16974 9102 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843524583 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/16974/statm): 531 226 485 147 0 384 0 [pid=16974] vsize: 2124 Raw data (/proc/16978/stat): 16978 (minisat+_64-bit) R 16974 16974 9102 0 -1 0 19598 0 0 0 48721 125 0 0 25 0 1 0 1843524588 79392768 19208 4294967295 134512640 135094434 3221224448 3221223104 134557911 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/16978/statm): 19383 19208 145 145 0 19238 0 [pid=16978] vsize: 77532 Current children cumulated CPU time (s) 488.46 Current children cumulated vsize (Kb) 79656 [startup+500.05 s] Raw data (loadavg): 0.99 0.97 0.97 2/58 16996 Raw data (/proc/16974/stat): 16974 (minisat+_script) S 16973 16974 9102 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843524583 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/16974/statm): 531 226 485 147 0 384 0 [pid=16974] vsize: 2124 Raw data (/proc/16978/stat): 16978 (minisat+_64-bit) R 16974 16974 9102 0 -1 0 19987 0 0 0 49714 129 0 0 25 0 1 0 1843524588 80977920 19597 4294967295 134512640 135094434 3221224448 3221223088 134538541 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/16978/statm): 19770 19597 145 145 0 19625 0 [pid=16978] vsize: 79080 Current children cumulated CPU time (s) 498.43 Current children cumulated vsize (Kb) 81204 [startup+510.051 s] Raw data (loadavg): 0.99 0.97 0.97 2/58 16996 Raw data (/proc/16974/stat): 16974 (minisat+_script) S 16973 16974 9102 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843524583 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/16974/statm): 531 226 485 147 0 384 0 [pid=16974] vsize: 2124 Raw data (/proc/16978/stat): 16978 (minisat+_64-bit) R 16974 16974 9102 0 -1 0 20346 0 0 0 50707 131 0 0 25 0 1 0 1843524588 82440192 19956 4294967295 134512640 135094434 3221224448 3221223040 134557230 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/16978/statm): 20127 19956 145 145 0 19982 0 [pid=16978] vsize: 80508 Current children cumulated CPU time (s) 508.38 Current children cumulated vsize (Kb) 82632 [startup+520.052 s] Raw data (loadavg): 0.99 0.97 0.97 2/58 16996 Raw data (/proc/16974/stat): 16974 (minisat+_script) S 16973 16974 9102 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843524583 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/16974/statm): 531 226 485 147 0 384 0 [pid=16974] vsize: 2124 Raw data (/proc/16978/stat): 16978 (minisat+_64-bit) R 16974 16974 9102 0 -1 0 20645 0 0 0 51701 134 0 0 25 0 1 0 1843524588 83656704 20255 4294967295 134512640 135094434 3221224448 3221223104 134558159 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/16978/statm): 20424 20255 145 145 0 20279 0 [pid=16978] vsize: 81696 Current children cumulated CPU time (s) 518.35 Current children cumulated vsize (Kb) 83820 [startup+530.052 s] Raw data (loadavg): 0.99 0.97 0.97 2/58 16996 Raw data (/proc/16974/stat): 16974 (minisat+_script) S 16973 16974 9102 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843524583 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/16974/statm): 531 226 485 147 0 384 0 [pid=16974] vsize: 2124 Raw data (/proc/16978/stat): 16978 (minisat+_64-bit) R 16974 16974 9102 0 -1 0 20945 0 0 0 52695 136 0 0 25 0 1 0 1843524588 84881408 20555 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/16978/statm): 20723 20555 145 145 0 20578 0 [pid=16978] vsize: 82892 Current children cumulated CPU time (s) 528.31 Current children cumulated vsize (Kb) 85016 [startup+540.054 s] Raw data (loadavg): 0.99 0.97 0.97 2/58 16996 Raw data (/proc/16974/stat): 16974 (minisat+_script) S 16973 16974 9102 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843524583 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/16974/statm): 531 226 485 147 0 384 0 [pid=16974] vsize: 2124 Raw data (/proc/16978/stat): 16978 (minisat+_64-bit) R 16974 16974 9102 0 -1 0 21204 0 0 0 53691 138 0 0 25 0 1 0 1843524588 85934080 20814 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/16978/statm): 20980 20814 145 145 0 20835 0 [pid=16978] vsize: 83920 Current children cumulated CPU time (s) 538.29 Current children cumulated vsize (Kb) 86044 [startup+550.055 s] Raw data (loadavg): 0.99 0.97 0.97 2/58 16996 Raw data (/proc/16974/stat): 16974 (minisat+_script) S 16973 16974 9102 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843524583 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/16974/statm): 531 226 485 147 0 384 0 [pid=16974] vsize: 2124 Raw data (/proc/16978/stat): 16978 (minisat+_64-bit) R 16974 16974 9102 0 -1 0 21372 0 0 0 54689 139 0 0 25 0 1 0 1843524588 86315008 20907 4294967295 134512640 135094434 3221224448 3221223104 134558187 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/16978/statm): 21073 20907 145 145 0 20928 0 [pid=16978] vsize: 84292 Current children cumulated CPU time (s) 548.28 Current children cumulated vsize (Kb) 86416 [startup+560.056 s] Raw data (loadavg): 0.99 0.97 0.97 2/58 16998 Raw data (/proc/16974/stat): 16974 (minisat+_script) S 16973 16974 9102 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843524583 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/16974/statm): 531 226 485 147 0 384 0 [pid=16974] vsize: 2124 Raw data (/proc/16978/stat): 16978 (minisat+_64-bit) R 16974 16974 9102 0 -1 0 21372 0 0 0 55689 139 0 0 25 0 1 0 1843524588 86315008 20907 4294967295 134512640 135094434 3221224448 3221223072 134557737 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/16978/statm): 21073 20907 145 145 0 20928 0 [pid=16978] vsize: 84292 Current children cumulated CPU time (s) 558.28 Current children cumulated vsize (Kb) 86416 [startup+570.057 s] Raw data (loadavg): 0.99 0.97 0.97 2/58 16998 Raw data (/proc/16974/stat): 16974 (minisat+_script) S 16973 16974 9102 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843524583 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/16974/statm): 531 226 485 147 0 384 0 [pid=16974] vsize: 2124 Raw data (/proc/16978/stat): 16978 (minisat+_64-bit) R 16974 16974 9102 0 -1 0 21372 0 0 0 56690 139 0 0 25 0 1 0 1843524588 86315008 20907 4294967295 134512640 135094434 3221224448 3221223104 134557914 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/16978/statm): 21073 20907 145 145 0 20928 0 [pid=16978] vsize: 84292 Current children cumulated CPU time (s) 568.29 Current children cumulated vsize (Kb) 86416 [startup+580.057 s] Raw data (loadavg): 0.99 0.97 0.97 2/58 16998 Raw data (/proc/16974/stat): 16974 (minisat+_script) S 16973 16974 9102 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843524583 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/16974/statm): 531 226 485 147 0 384 0 [pid=16974] vsize: 2124 Raw data (/proc/16978/stat): 16978 (minisat+_64-bit) R 16974 16974 9102 0 -1 0 21372 0 0 0 57690 139 0 0 25 0 1 0 1843524588 86315008 20907 4294967295 134512640 135094434 3221224448 3221223072 134557596 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/16978/statm): 21073 20907 145 145 0 20928 0 [pid=16978] vsize: 84292 Current children cumulated CPU time (s) 578.29 Current children cumulated vsize (Kb) 86416 [startup+590.057 s] Raw data (loadavg): 0.99 0.97 0.97 2/58 16998 Raw data (/proc/16974/stat): 16974 (minisat+_script) S 16973 16974 9102 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843524583 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/16974/statm): 531 226 485 147 0 384 0 [pid=16974] vsize: 2124 Raw data (/proc/16978/stat): 16978 (minisat+_64-bit) R 16974 16974 9102 0 -1 0 21372 0 0 0 58690 139 0 0 25 0 1 0 1843524588 86315008 20907 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/16978/statm): 21073 20907 145 145 0 20928 0 [pid=16978] vsize: 84292 Current children cumulated CPU time (s) 588.29 Current children cumulated vsize (Kb) 86416 [startup+600.058 s] Raw data (loadavg): 0.99 0.97 0.97 2/58 16998 Raw data (/proc/16974/stat): 16974 (minisat+_script) S 16973 16974 9102 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843524583 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/16974/statm): 531 226 485 147 0 384 0 [pid=16974] vsize: 2124 Raw data (/proc/16978/stat): 16978 (minisat+_64-bit) R 16974 16974 9102 0 -1 0 21372 0 0 0 59690 139 0 0 25 0 1 0 1843524588 86315008 20907 4294967295 134512640 135094434 3221224448 3221223104 134558176 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/16978/statm): 21073 20907 145 145 0 20928 0 [pid=16978] vsize: 84292 Current children cumulated CPU time (s) 598.29 Current children cumulated vsize (Kb) 86416 [startup+610.06 s] Raw data (loadavg): 0.99 0.97 0.97 2/58 16998 Raw data (/proc/16974/stat): 16974 (minisat+_script) S 16973 16974 9102 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843524583 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/16974/statm): 531 226 485 147 0 384 0 [pid=16974] vsize: 2124 Raw data (/proc/16978/stat): 16978 (minisat+_64-bit) R 16974 16974 9102 0 -1 0 21372 0 0 0 60690 139 0 0 25 0 1 0 1843524588 86315008 20907 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/16978/statm): 21073 20907 145 145 0 20928 0 [pid=16978] vsize: 84292 Current children cumulated CPU time (s) 608.29 Current children cumulated vsize (Kb) 86416 [startup+620.061 s] Raw data (loadavg): 0.99 0.97 0.97 2/58 17000 Raw data (/proc/16974/stat): 16974 (minisat+_script) S 16973 16974 9102 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843524583 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/16974/statm): 531 226 485 147 0 384 0 [pid=16974] vsize: 2124 Raw data (/proc/16978/stat): 16978 (minisat+_64-bit) R 16974 16974 9102 0 -1 0 21372 0 0 0 61691 139 0 0 25 0 1 0 1843524588 86315008 20907 4294967295 134512640 135094434 3221224448 3221223104 134557996 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/16978/statm): 21073 20907 145 145 0 20928 0 [pid=16978] vsize: 84292 Current children cumulated CPU time (s) 618.3 Current children cumulated vsize (Kb) 86416 [startup+630.061 s] Raw data (loadavg): 0.99 0.97 0.97 2/58 17000 Raw data (/proc/16974/stat): 16974 (minisat+_script) S 16973 16974 9102 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843524583 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/16974/statm): 531 226 485 147 0 384 0 [pid=16974] vsize: 2124 Raw data (/proc/16978/stat): 16978 (minisat+_64-bit) R 16974 16974 9102 0 -1 0 21372 0 0 0 62691 139 0 0 25 0 1 0 1843524588 86315008 20907 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/16978/statm): 21073 20907 145 145 0 20928 0 [pid=16978] vsize: 84292 Current children cumulated CPU time (s) 628.3 Current children cumulated vsize (Kb) 86416 [startup+640.062 s] Raw data (loadavg): 0.99 0.97 0.97 2/58 17000 Raw data (/proc/16974/stat): 16974 (minisat+_script) S 16973 16974 9102 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843524583 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/16974/statm): 531 226 485 147 0 384 0 [pid=16974] vsize: 2124 Raw data (/proc/16978/stat): 16978 (minisat+_64-bit) R 16974 16974 9102 0 -1 0 21372 0 0 0 63691 139 0 0 25 0 1 0 1843524588 86315008 20907 4294967295 134512640 135094434 3221224448 3221223040 134557435 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/16978/statm): 21073 20907 145 145 0 20928 0 [pid=16978] vsize: 84292 Current children cumulated CPU time (s) 638.3 Current children cumulated vsize (Kb) 86416 [startup+650.063 s] Raw data (loadavg): 0.99 0.97 0.97 2/58 17000 Raw data (/proc/16974/stat): 16974 (minisat+_script) S 16973 16974 9102 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843524583 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/16974/statm): 531 226 485 147 0 384 0 [pid=16974] vsize: 2124 Raw data (/proc/16978/stat): 16978 (minisat+_64-bit) R 16974 16974 9102 0 -1 0 21372 0 0 0 64691 139 0 0 25 0 1 0 1843524588 86315008 20907 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/16978/statm): 21073 20907 145 145 0 20928 0 [pid=16978] vsize: 84292 Current children cumulated CPU time (s) 648.3 Current children cumulated vsize (Kb) 86416 [startup+660.064 s] Raw data (loadavg): 0.99 0.97 0.97 2/58 17000 Raw data (/proc/16974/stat): 16974 (minisat+_script) S 16973 16974 9102 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843524583 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/16974/statm): 531 226 485 147 0 384 0 [pid=16974] vsize: 2124 Raw data (/proc/16978/stat): 16978 (minisat+_64-bit) R 16974 16974 9102 0 -1 0 21372 0 0 0 65691 139 0 0 25 0 1 0 1843524588 86315008 20907 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/16978/statm): 21073 20907 145 145 0 20928 0 [pid=16978] vsize: 84292 Current children cumulated CPU time (s) 658.3 Current children cumulated vsize (Kb) 86416 [startup+670.065 s] Raw data (loadavg): 0.99 0.97 0.97 2/58 17000 Raw data (/proc/16974/stat): 16974 (minisat+_script) S 16973 16974 9102 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843524583 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/16974/statm): 531 226 485 147 0 384 0 [pid=16974] vsize: 2124 Raw data (/proc/16978/stat): 16978 (minisat+_64-bit) R 16974 16974 9102 0 -1 0 21372 0 0 0 66692 139 0 0 25 0 1 0 1843524588 86315008 20907 4294967295 134512640 135094434 3221224448 3221223104 134557937 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/16978/statm): 21073 20907 145 145 0 20928 0 [pid=16978] vsize: 84292 Current children cumulated CPU time (s) 668.31 Current children cumulated vsize (Kb) 86416 [startup+680.066 s] Raw data (loadavg): 0.99 0.97 0.97 2/58 17002 Raw data (/proc/16974/stat): 16974 (minisat+_script) S 16973 16974 9102 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843524583 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/16974/statm): 531 226 485 147 0 384 0 [pid=16974] vsize: 2124 Raw data (/proc/16978/stat): 16978 (minisat+_64-bit) R 16974 16974 9102 0 -1 0 21372 0 0 0 67692 139 0 0 25 0 1 0 1843524588 86315008 20907 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/16978/statm): 21073 20907 145 145 0 20928 0 [pid=16978] vsize: 84292 Current children cumulated CPU time (s) 678.31 Current children cumulated vsize (Kb) 86416 [startup+690.067 s] Raw data (loadavg): 0.99 0.97 0.97 2/58 17002 Raw data (/proc/16974/stat): 16974 (minisat+_script) S 16973 16974 9102 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843524583 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/16974/statm): 531 226 485 147 0 384 0 [pid=16974] vsize: 2124 Raw data (/proc/16978/stat): 16978 (minisat+_64-bit) R 16974 16974 9102 0 -1 0 21372 0 0 0 68692 139 0 0 25 0 1 0 1843524588 86315008 20907 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/16978/statm): 21073 20907 145 145 0 20928 0 [pid=16978] vsize: 84292 Current children cumulated CPU time (s) 688.31 Current children cumulated vsize (Kb) 86416 [startup+700.068 s] Raw data (loadavg): 0.99 0.97 0.97 2/58 17002 Raw data (/proc/16974/stat): 16974 (minisat+_script) S 16973 16974 9102 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843524583 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/16974/statm): 531 226 485 147 0 384 0 [pid=16974] vsize: 2124 Raw data (/proc/16978/stat): 16978 (minisat+_64-bit) R 16974 16974 9102 0 -1 0 21372 0 0 0 69692 139 0 0 25 0 1 0 1843524588 86315008 20907 4294967295 134512640 135094434 3221224448 3221223104 134558235 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/16978/statm): 21073 20907 145 145 0 20928 0 [pid=16978] vsize: 84292 Current children cumulated CPU time (s) 698.31 Current children cumulated vsize (Kb) 86416 [startup+710.07 s] Raw data (loadavg): 0.99 0.97 0.97 2/58 17002 Raw data (/proc/16974/stat): 16974 (minisat+_script) S 16973 16974 9102 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843524583 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/16974/statm): 531 226 485 147 0 384 0 [pid=16974] vsize: 2124 Raw data (/proc/16978/stat): 16978 (minisat+_64-bit) R 16974 16974 9102 0 -1 0 21372 0 0 0 70693 139 0 0 25 0 1 0 1843524588 86315008 20907 4294967295 134512640 135094434 3221224448 3221223104 134558004 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/16978/statm): 21073 20907 145 145 0 20928 0 [pid=16978] vsize: 84292 Current children cumulated CPU time (s) 708.32 Current children cumulated vsize (Kb) 86416 [startup+720.071 s] Raw data (loadavg): 0.99 0.97 0.97 2/58 17002 Raw data (/proc/16974/stat): 16974 (minisat+_script) S 16973 16974 9102 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843524583 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/16974/statm): 531 226 485 147 0 384 0 [pid=16974] vsize: 2124 Raw data (/proc/16978/stat): 16978 (minisat+_64-bit) R 16974 16974 9102 0 -1 0 21372 0 0 0 71693 139 0 0 25 0 1 0 1843524588 86315008 20907 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/16978/statm): 21073 20907 145 145 0 20928 0 [pid=16978] vsize: 84292 Current children cumulated CPU time (s) 718.32 Current children cumulated vsize (Kb) 86416 [startup+730.071 s] Raw data (loadavg): 0.99 0.97 0.97 2/58 17002 Raw data (/proc/16974/stat): 16974 (minisat+_script) S 16973 16974 9102 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843524583 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/16974/statm): 531 226 485 147 0 384 0 [pid=16974] vsize: 2124 Raw data (/proc/16978/stat): 16978 (minisat+_64-bit) R 16974 16974 9102 0 -1 0 21372 0 0 0 72693 139 0 0 25 0 1 0 1843524588 86315008 20907 4294967295 134512640 135094434 3221224448 3221223104 134557884 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/16978/statm): 21073 20907 145 145 0 20928 0 [pid=16978] vsize: 84292 Current children cumulated CPU time (s) 728.32 Current children cumulated vsize (Kb) 86416 [startup+740.071 s] Raw data (loadavg): 0.99 0.97 0.97 2/58 17004 Raw data (/proc/16974/stat): 16974 (minisat+_script) S 16973 16974 9102 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843524583 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/16974/statm): 531 226 485 147 0 384 0 [pid=16974] vsize: 2124 Raw data (/proc/16978/stat): 16978 (minisat+_64-bit) R 16974 16974 9102 0 -1 0 21372 0 0 0 73693 139 0 0 25 0 1 0 1843524588 86315008 20907 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/16978/statm): 21073 20907 145 145 0 20928 0 [pid=16978] vsize: 84292 Current children cumulated CPU time (s) 738.32 Current children cumulated vsize (Kb) 86416 [startup+750.072 s] Raw data (loadavg): 0.99 0.97 0.97 2/58 17004 Raw data (/proc/16974/stat): 16974 (minisat+_script) S 16973 16974 9102 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843524583 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/16974/statm): 531 226 485 147 0 384 0 [pid=16974] vsize: 2124 Raw data (/proc/16978/stat): 16978 (minisat+_64-bit) R 16974 16974 9102 0 -1 0 21372 0 0 0 74693 139 0 0 25 0 1 0 1843524588 86315008 20907 4294967295 134512640 135094434 3221224448 3221223104 134558159 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/16978/statm): 21073 20907 145 145 0 20928 0 [pid=16978] vsize: 84292 Current children cumulated CPU time (s) 748.32 Current children cumulated vsize (Kb) 86416 [startup+760.073 s] Raw data (loadavg): 0.99 0.97 0.97 2/58 17004 Raw data (/proc/16974/stat): 16974 (minisat+_script) S 16973 16974 9102 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843524583 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/16974/statm): 531 226 485 147 0 384 0 [pid=16974] vsize: 2124 Raw data (/proc/16978/stat): 16978 (minisat+_64-bit) R 16974 16974 9102 0 -1 0 21372 0 0 0 75694 139 0 0 25 0 1 0 1843524588 86315008 20907 4294967295 134512640 135094434 3221224448 3221223104 134558159 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/16978/statm): 21073 20907 145 145 0 20928 0 [pid=16978] vsize: 84292 Current children cumulated CPU time (s) 758.33 Current children cumulated vsize (Kb) 86416 [startup+770.074 s] Raw data (loadavg): 0.99 0.97 0.97 2/58 17004 Raw data (/proc/16974/stat): 16974 (minisat+_script) S 16973 16974 9102 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843524583 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/16974/statm): 531 226 485 147 0 384 0 [pid=16974] vsize: 2124 Raw data (/proc/16978/stat): 16978 (minisat+_64-bit) R 16974 16974 9102 0 -1 0 21372 0 0 0 76694 139 0 0 25 0 1 0 1843524588 86315008 20907 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/16978/statm): 21073 20907 145 145 0 20928 0 [pid=16978] vsize: 84292 Current children cumulated CPU time (s) 768.33 Current children cumulated vsize (Kb) 86416 [startup+780.075 s] Raw data (loadavg): 0.99 0.97 0.97 2/58 17004 Raw data (/proc/16974/stat): 16974 (minisat+_script) S 16973 16974 9102 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843524583 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/16974/statm): 531 226 485 147 0 384 0 [pid=16974] vsize: 2124 Raw data (/proc/16978/stat): 16978 (minisat+_64-bit) R 16974 16974 9102 0 -1 0 21372 0 0 0 77694 139 0 0 25 0 1 0 1843524588 86315008 20907 4294967295 134512640 135094434 3221224448 3221223104 134557939 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/16978/statm): 21073 20907 145 145 0 20928 0 [pid=16978] vsize: 84292 Current children cumulated CPU time (s) 778.33 Current children cumulated vsize (Kb) 86416 [startup+790.076 s] Raw data (loadavg): 0.99 0.97 0.97 2/58 17004 Raw data (/proc/16974/stat): 16974 (minisat+_script) S 16973 16974 9102 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843524583 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/16974/statm): 531 226 485 147 0 384 0 [pid=16974] vsize: 2124 Raw data (/proc/16978/stat): 16978 (minisat+_64-bit) R 16974 16974 9102 0 -1 0 21372 0 0 0 78694 139 0 0 25 0 1 0 1843524588 86315008 20907 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/16978/statm): 21073 20907 145 145 0 20928 0 [pid=16978] vsize: 84292 Current children cumulated CPU time (s) 788.33 Current children cumulated vsize (Kb) 86416 [startup+800.077 s] Raw data (loadavg): 0.99 0.97 0.97 2/58 17006 Raw data (/proc/16974/stat): 16974 (minisat+_script) S 16973 16974 9102 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843524583 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/16974/statm): 531 226 485 147 0 384 0 [pid=16974] vsize: 2124 Raw data (/proc/16978/stat): 16978 (minisat+_64-bit) R 16974 16974 9102 0 -1 0 21372 0 0 0 79694 139 0 0 25 0 1 0 1843524588 86315008 20907 4294967295 134512640 135094434 3221224448 3221223104 134557903 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/16978/statm): 21073 20907 145 145 0 20928 0 [pid=16978] vsize: 84292 Current children cumulated CPU time (s) 798.33 Current children cumulated vsize (Kb) 86416 [startup+810.078 s] Raw data (loadavg): 0.99 0.97 0.97 2/58 17006 Raw data (/proc/16974/stat): 16974 (minisat+_script) S 16973 16974 9102 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843524583 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/16974/statm): 531 226 485 147 0 384 0 [pid=16974] vsize: 2124 Raw data (/proc/16978/stat): 16978 (minisat+_64-bit) R 16974 16974 9102 0 -1 0 21472 0 0 0 80693 140 0 0 25 0 1 0 1843524588 86724608 21007 4294967295 134512640 135094434 3221224448 3221223120 134555931 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/16978/statm): 21173 21007 145 145 0 21028 0 [pid=16978] vsize: 84692 Current children cumulated CPU time (s) 808.33 Current children cumulated vsize (Kb) 86816 [startup+820.079 s] Raw data (loadavg): 0.99 0.97 0.97 2/58 17006 Raw data (/proc/16974/stat): 16974 (minisat+_script) S 16973 16974 9102 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843524583 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/16974/statm): 531 226 485 147 0 384 0 [pid=16974] vsize: 2124 Raw data (/proc/16978/stat): 16978 (minisat+_64-bit) R 16974 16974 9102 0 -1 0 21883 0 0 0 81685 144 0 0 25 0 1 0 1843524588 88408064 21418 4294967295 134512640 135094434 3221224448 3221223104 134558159 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/16978/statm): 21584 21418 145 145 0 21439 0 [pid=16978] vsize: 86336 Current children cumulated CPU time (s) 818.29 Current children cumulated vsize (Kb) 88460 [startup+830.079 s] Raw data (loadavg): 0.99 0.97 0.97 2/58 17006 Raw data (/proc/16974/stat): 16974 (minisat+_script) S 16973 16974 9102 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843524583 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/16974/statm): 531 226 485 147 0 384 0 [pid=16974] vsize: 2124 Raw data (/proc/16978/stat): 16978 (minisat+_64-bit) R 16974 16974 9102 0 -1 0 22256 0 0 0 82679 146 0 0 25 0 1 0 1843524588 89935872 21791 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/16978/statm): 21957 21791 145 145 0 21812 0 [pid=16978] vsize: 87828 Current children cumulated CPU time (s) 828.25 Current children cumulated vsize (Kb) 89952 [startup+840.08 s] Raw data (loadavg): 0.99 0.97 0.97 2/58 17006 Raw data (/proc/16974/stat): 16974 (minisat+_script) S 16973 16974 9102 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843524583 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/16974/statm): 531 226 485 147 0 384 0 [pid=16974] vsize: 2124 Raw data (/proc/16978/stat): 16978 (minisat+_64-bit) R 16974 16974 9102 0 -1 0 22627 0 0 0 83672 149 0 0 25 0 1 0 1843524588 91455488 22162 4294967295 134512640 135094434 3221224448 3221223104 134557948 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/16978/statm): 22328 22162 145 145 0 22183 0 [pid=16978] vsize: 89312 Current children cumulated CPU time (s) 838.21 Current children cumulated vsize (Kb) 91436 [startup+850.081 s] Raw data (loadavg): 0.99 0.97 0.97 2/58 17006 Raw data (/proc/16974/stat): 16974 (minisat+_script) S 16973 16974 9102 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843524583 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/16974/statm): 531 226 485 147 0 384 0 [pid=16974] vsize: 2124 Raw data (/proc/16978/stat): 16978 (minisat+_64-bit) R 16974 16974 9102 0 -1 0 23015 0 0 0 84665 152 0 0 25 0 1 0 1843524588 93044736 22550 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/16978/statm): 22716 22550 145 145 0 22571 0 [pid=16978] vsize: 90864 Current children cumulated CPU time (s) 848.17 Current children cumulated vsize (Kb) 92988 [startup+860.082 s] Raw data (loadavg): 0.99 0.97 0.97 2/58 17008 Raw data (/proc/16974/stat): 16974 (minisat+_script) S 16973 16974 9102 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843524583 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/16974/statm): 531 226 485 147 0 384 0 [pid=16974] vsize: 2124 Raw data (/proc/16978/stat): 16978 (minisat+_64-bit) R 16974 16974 9102 0 -1 0 23399 0 0 0 85659 154 0 0 25 0 1 0 1843524588 94617600 22934 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/16978/statm): 23100 22934 145 145 0 22955 0 [pid=16978] vsize: 92400 Current children cumulated CPU time (s) 858.13 Current children cumulated vsize (Kb) 94524 [startup+870.083 s] Raw data (loadavg): 0.99 0.97 0.97 2/58 17008 Raw data (/proc/16974/stat): 16974 (minisat+_script) S 16973 16974 9102 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843524583 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/16974/statm): 531 226 485 147 0 384 0 [pid=16974] vsize: 2124 Raw data (/proc/16978/stat): 16978 (minisat+_64-bit) R 16974 16974 9102 0 -1 0 23818 0 0 0 86652 157 0 0 25 0 1 0 1843524588 96337920 23353 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/16978/statm): 23520 23353 145 145 0 23375 0 [pid=16978] vsize: 94080 Current children cumulated CPU time (s) 868.09 Current children cumulated vsize (Kb) 96204 [startup+880.083 s] Raw data (loadavg): 0.99 0.97 0.97 2/58 17008 Raw data (/proc/16974/stat): 16974 (minisat+_script) S 16973 16974 9102 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843524583 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/16974/statm): 531 226 485 147 0 384 0 [pid=16974] vsize: 2124 Raw data (/proc/16978/stat): 16978 (minisat+_64-bit) R 16974 16974 9102 0 -1 0 24078 0 0 0 87646 159 0 0 25 0 1 0 1843524588 97411072 23613 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/16978/statm): 23782 23613 145 145 0 23637 0 [pid=16978] vsize: 95128 Current children cumulated CPU time (s) 878.05 Current children cumulated vsize (Kb) 97252 [startup+890.085 s] Raw data (loadavg): 0.99 0.97 0.97 2/58 17008 Raw data (/proc/16974/stat): 16974 (minisat+_script) S 16973 16974 9102 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843524583 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/16974/statm): 531 226 485 147 0 384 0 [pid=16974] vsize: 2124 Raw data (/proc/16978/stat): 16978 (minisat+_64-bit) R 16974 16974 9102 0 -1 0 24348 0 0 0 88642 161 0 0 25 0 1 0 1843524588 98516992 23883 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/16978/statm): 24052 23883 145 145 0 23907 0 [pid=16978] vsize: 96208 Current children cumulated CPU time (s) 888.03 Current children cumulated vsize (Kb) 98332 [startup+900.086 s] Raw data (loadavg): 0.99 0.97 0.97 2/58 17008 Raw data (/proc/16974/stat): 16974 (minisat+_script) S 16973 16974 9102 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843524583 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/16974/statm): 531 226 485 147 0 384 0 [pid=16974] vsize: 2124 Raw data (/proc/16978/stat): 16978 (minisat+_64-bit) R 16974 16974 9102 0 -1 0 24712 0 0 0 89636 164 0 0 25 0 1 0 1843524588 100007936 24247 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/16978/statm): 24416 24247 145 145 0 24271 0 [pid=16978] vsize: 97664 Current children cumulated CPU time (s) 898 Current children cumulated vsize (Kb) 99788 [startup+910.087 s] Raw data (loadavg): 0.99 0.97 0.97 2/58 17008 Raw data (/proc/16974/stat): 16974 (minisat+_script) S 16973 16974 9102 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843524583 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/16974/statm): 531 226 485 147 0 384 0 [pid=16974] vsize: 2124 Raw data (/proc/16978/stat): 16978 (minisat+_64-bit) R 16974 16974 9102 0 -1 0 25067 0 0 0 90629 167 0 0 25 0 1 0 1843524588 101462016 24602 4294967295 134512640 135094434 3221224448 3221223104 134558187 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/16978/statm): 24771 24602 145 145 0 24626 0 [pid=16978] vsize: 99084 Current children cumulated CPU time (s) 907.96 Current children cumulated vsize (Kb) 101208 [startup+920.088 s] Raw data (loadavg): 0.99 0.97 0.97 2/58 17010 Raw data (/proc/16974/stat): 16974 (minisat+_script) S 16973 16974 9102 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843524583 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/16974/statm): 531 226 485 147 0 384 0 [pid=16974] vsize: 2124 Raw data (/proc/16978/stat): 16978 (minisat+_64-bit) R 16974 16974 9102 0 -1 0 25484 0 0 0 91621 170 0 0 25 0 1 0 1843524588 103170048 25019 4294967295 134512640 135094434 3221224448 3221223104 134558232 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/16978/statm): 25188 25019 145 145 0 25043 0 [pid=16978] vsize: 100752 Current children cumulated CPU time (s) 917.91 Current children cumulated vsize (Kb) 102876 [startup+930.088 s] Raw data (loadavg): 0.99 0.97 0.97 2/58 17010 Raw data (/proc/16974/stat): 16974 (minisat+_script) S 16973 16974 9102 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843524583 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/16974/statm): 531 226 485 147 0 384 0 [pid=16974] vsize: 2124 Raw data (/proc/16978/stat): 16978 (minisat+_64-bit) R 16974 16974 9102 0 -1 0 25925 0 0 0 92613 173 0 0 25 0 1 0 1843524588 104976384 25460 4294967295 134512640 135094434 3221224448 3221223104 134558013 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/16978/statm): 25629 25460 145 145 0 25484 0 [pid=16978] vsize: 102516 Current children cumulated CPU time (s) 927.86 Current children cumulated vsize (Kb) 104640 [startup+940.089 s] Raw data (loadavg): 0.99 0.97 0.97 2/58 17010 Raw data (/proc/16974/stat): 16974 (minisat+_script) S 16973 16974 9102 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843524583 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/16974/statm): 531 226 485 147 0 384 0 [pid=16974] vsize: 2124 Raw data (/proc/16978/stat): 16978 (minisat+_64-bit) R 16974 16974 9102 0 -1 0 26314 0 0 0 93606 176 0 0 25 0 1 0 1843524588 106569728 25849 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/16978/statm): 26018 25849 145 145 0 25873 0 [pid=16978] vsize: 104072 Current children cumulated CPU time (s) 937.82 Current children cumulated vsize (Kb) 106196 [startup+950.09 s] Raw data (loadavg): 0.99 0.97 0.97 2/58 17010 Raw data (/proc/16974/stat): 16974 (minisat+_script) S 16973 16974 9102 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843524583 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/16974/statm): 531 226 485 147 0 384 0 [pid=16974] vsize: 2124 Raw data (/proc/16978/stat): 16978 (minisat+_64-bit) R 16974 16974 9102 0 -1 0 26691 0 0 0 94601 178 0 0 25 0 1 0 1843524588 108113920 26226 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/16978/statm): 26395 26226 145 145 0 26250 0 [pid=16978] vsize: 105580 Current children cumulated CPU time (s) 947.79 Current children cumulated vsize (Kb) 107704 [startup+960.092 s] Raw data (loadavg): 0.99 0.97 0.97 2/58 17010 Raw data (/proc/16974/stat): 16974 (minisat+_script) S 16973 16974 9102 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843524583 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/16974/statm): 531 226 485 147 0 384 0 [pid=16974] vsize: 2124 Raw data (/proc/16978/stat): 16978 (minisat+_64-bit) R 16974 16974 9102 0 -1 0 27124 0 0 0 95593 181 0 0 25 0 1 0 1843524588 109879296 26659 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/16978/statm): 26826 26659 145 145 0 26681 0 [pid=16978] vsize: 107304 Current children cumulated CPU time (s) 957.74 Current children cumulated vsize (Kb) 109428 [startup+970.093 s] Raw data (loadavg): 0.99 0.97 0.97 2/58 17010 Raw data (/proc/16974/stat): 16974 (minisat+_script) S 16973 16974 9102 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843524583 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/16974/statm): 531 226 485 147 0 384 0 [pid=16974] vsize: 2124 Raw data (/proc/16978/stat): 16978 (minisat+_64-bit) R 16974 16974 9102 0 -1 0 27464 0 0 0 96587 184 0 0 25 0 1 0 1843524588 111267840 26999 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/16978/statm): 27165 26999 145 145 0 27020 0 [pid=16978] vsize: 108660 Current children cumulated CPU time (s) 967.71 Current children cumulated vsize (Kb) 110784 [startup+980.093 s] Raw data (loadavg): 0.99 0.97 0.97 2/58 17012 Raw data (/proc/16974/stat): 16974 (minisat+_script) S 16973 16974 9102 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843524583 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/16974/statm): 531 226 485 147 0 384 0 [pid=16974] vsize: 2124 Raw data (/proc/16978/stat): 16978 (minisat+_64-bit) R 16974 16974 9102 0 -1 0 27778 0 0 0 97582 186 0 0 25 0 1 0 1843524588 112549888 27313 4294967295 134512640 135094434 3221224448 3221223108 134553482 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/16978/statm): 27478 27313 145 145 0 27333 0 [pid=16978] vsize: 109912 Current children cumulated CPU time (s) 977.68 Current children cumulated vsize (Kb) 112036 [startup+990.094 s] Raw data (loadavg): 0.99 0.97 0.97 2/58 17012 Raw data (/proc/16974/stat): 16974 (minisat+_script) S 16973 16974 9102 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843524583 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/16974/statm): 531 226 485 147 0 384 0 [pid=16974] vsize: 2124 Raw data (/proc/16978/stat): 16978 (minisat+_64-bit) R 16974 16974 9102 0 -1 0 28027 0 0 0 98577 188 0 0 25 0 1 0 1843524588 113569792 27562 4294967295 134512640 135094434 3221224448 3221223108 134553482 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/16978/statm): 27727 27562 145 145 0 27582 0 [pid=16978] vsize: 110908 Current children cumulated CPU time (s) 987.65 Current children cumulated vsize (Kb) 113032 [startup+1000.09 s] Raw data (loadavg): 0.99 0.97 0.97 2/58 17012 Raw data (/proc/16974/stat): 16974 (minisat+_script) S 16973 16974 9102 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843524583 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/16974/statm): 531 226 485 147 0 384 0 [pid=16974] vsize: 2124 Raw data (/proc/16978/stat): 16978 (minisat+_64-bit) R 16974 16974 9102 0 -1 0 28365 0 0 0 99571 189 0 0 25 0 1 0 1843524588 115474432 27900 4294967295 134512640 135094434 3221224448 3221223072 134557598 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/16978/statm): 28192 27900 145 145 0 28047 0 [pid=16978] vsize: 112768 Current children cumulated CPU time (s) 997.6 Current children cumulated vsize (Kb) 114892 [startup+1010.1 s] Raw data (loadavg): 0.99 0.97 0.97 2/58 17012 Raw data (/proc/16974/stat): 16974 (minisat+_script) S 16973 16974 9102 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843524583 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/16974/statm): 531 226 485 147 0 384 0 [pid=16974] vsize: 2124 Raw data (/proc/16978/stat): 16978 (minisat+_64-bit) R 16974 16974 9102 0 -1 0 28636 0 0 0 100567 191 0 0 25 0 1 0 1843524588 116580352 28171 4294967295 134512640 135094434 3221224448 3221223104 134558016 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/16978/statm): 28462 28171 145 145 0 28317 0 [pid=16978] vsize: 113848 Current children cumulated CPU time (s) 1007.58 Current children cumulated vsize (Kb) 115972 [startup+1020.1 s] Raw data (loadavg): 0.99 0.97 0.97 2/58 17012 Raw data (/proc/16974/stat): 16974 (minisat+_script) S 16973 16974 9102 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843524583 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/16974/statm): 531 226 485 147 0 384 0 [pid=16974] vsize: 2124 Raw data (/proc/16978/stat): 16978 (minisat+_64-bit) R 16974 16974 9102 0 -1 0 28725 0 0 0 101566 192 0 0 25 0 1 0 1843524588 116948992 28260 4294967295 134512640 135094434 3221224448 3221223108 134553497 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/16978/statm): 28552 28260 145 145 0 28407 0 [pid=16978] vsize: 114208 Current children cumulated CPU time (s) 1017.58 Current children cumulated vsize (Kb) 116332 [startup+1030.1 s] Raw data (loadavg): 0.99 0.97 0.97 2/58 17012 Raw data (/proc/16974/stat): 16974 (minisat+_script) S 16973 16974 9102 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843524583 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/16974/statm): 531 226 485 147 0 384 0 [pid=16974] vsize: 2124 Raw data (/proc/16978/stat): 16978 (minisat+_64-bit) R 16974 16974 9102 0 -1 0 29020 0 0 0 102561 194 0 0 25 0 1 0 1843524588 118153216 28555 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/16978/statm): 28846 28555 145 145 0 28701 0 [pid=16978] vsize: 115384 Current children cumulated CPU time (s) 1027.55 Current children cumulated vsize (Kb) 117508 [startup+1040.1 s] Raw data (loadavg): 0.99 0.97 0.97 2/58 17014 Raw data (/proc/16974/stat): 16974 (minisat+_script) S 16973 16974 9102 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843524583 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/16974/statm): 531 226 485 147 0 384 0 [pid=16974] vsize: 2124 Raw data (/proc/16978/stat): 16978 (minisat+_64-bit) R 16974 16974 9102 0 -1 0 29358 0 0 0 103556 196 0 0 25 0 1 0 1843524588 119529472 28893 4294967295 134512640 135094434 3221224448 3221223040 134556928 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/16978/statm): 29182 28893 145 145 0 29037 0 [pid=16978] vsize: 116728 Current children cumulated CPU time (s) 1037.52 Current children cumulated vsize (Kb) 118852 [startup+1050.1 s] Raw data (loadavg): 0.99 0.97 0.97 2/58 17014 Raw data (/proc/16974/stat): 16974 (minisat+_script) S 16973 16974 9102 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843524583 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/16974/statm): 531 226 485 147 0 384 0 [pid=16974] vsize: 2124 Raw data (/proc/16978/stat): 16978 (minisat+_64-bit) R 16974 16974 9102 0 -1 0 29759 0 0 0 104550 199 0 0 25 0 1 0 1843524588 121167872 29294 4294967295 134512640 135094434 3221224448 3221223040 134557230 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/16978/statm): 29582 29294 145 145 0 29437 0 [pid=16978] vsize: 118328 Current children cumulated CPU time (s) 1047.49 Current children cumulated vsize (Kb) 120452 [startup+1060.1 s] Raw data (loadavg): 0.99 0.97 0.97 2/58 17014 Raw data (/proc/16974/stat): 16974 (minisat+_script) S 16973 16974 9102 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843524583 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/16974/statm): 531 226 485 147 0 384 0 [pid=16974] vsize: 2124 Raw data (/proc/16978/stat): 16978 (minisat+_64-bit) R 16974 16974 9102 0 -1 0 30081 0 0 0 105545 201 0 0 25 0 1 0 1843524588 122478592 29616 4294967295 134512640 135094434 3221224448 3221223100 134558255 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/16978/statm): 29902 29616 145 145 0 29757 0 [pid=16978] vsize: 119608 Current children cumulated CPU time (s) 1057.46 Current children cumulated vsize (Kb) 121732 [startup+1070.1 s] Raw data (loadavg): 0.99 0.97 0.97 2/58 17014 Raw data (/proc/16974/stat): 16974 (minisat+_script) S 16973 16974 9102 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843524583 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/16974/statm): 531 226 485 147 0 384 0 [pid=16974] vsize: 2124 Raw data (/proc/16978/stat): 16978 (minisat+_64-bit) R 16974 16974 9102 0 -1 0 30353 0 0 0 106539 203 0 0 25 0 1 0 1843524588 123588608 29888 4294967295 134512640 135094434 3221224448 3221223108 134553530 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/16978/statm): 30173 29888 145 145 0 30028 0 [pid=16978] vsize: 120692 Current children cumulated CPU time (s) 1067.42 Current children cumulated vsize (Kb) 122816 [startup+1080.1 s] Raw data (loadavg): 0.99 0.97 0.97 2/58 17014 Raw data (/proc/16974/stat): 16974 (minisat+_script) S 16973 16974 9102 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843524583 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/16974/statm): 531 226 485 147 0 384 0 [pid=16974] vsize: 2124 Raw data (/proc/16978/stat): 16978 (minisat+_64-bit) R 16974 16974 9102 0 -1 0 30563 0 0 0 107535 205 0 0 25 0 1 0 1843524588 124448768 30098 4294967295 134512640 135094434 3221224448 3221223104 134558225 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/16978/statm): 30383 30098 145 145 0 30238 0 [pid=16978] vsize: 121532 Current children cumulated CPU time (s) 1077.4 Current children cumulated vsize (Kb) 123656 [startup+1090.1 s] Raw data (loadavg): 0.99 0.97 0.97 2/58 17014 Raw data (/proc/16974/stat): 16974 (minisat+_script) S 16973 16974 9102 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843524583 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/16974/statm): 531 226 485 147 0 384 0 [pid=16974] vsize: 2124 Raw data (/proc/16978/stat): 16978 (minisat+_64-bit) R 16974 16974 9102 0 -1 0 30791 0 0 0 108531 207 0 0 25 0 1 0 1843524588 125378560 30326 4294967295 134512640 135094434 3221224448 3221223104 134558159 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/16978/statm): 30610 30326 145 145 0 30465 0 [pid=16978] vsize: 122440 Current children cumulated CPU time (s) 1087.38 Current children cumulated vsize (Kb) 124564 [startup+1100.1 s] Raw data (loadavg): 0.99 0.97 0.97 2/58 17016 Raw data (/proc/16974/stat): 16974 (minisat+_script) S 16973 16974 9102 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843524583 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/16974/statm): 531 226 485 147 0 384 0 [pid=16974] vsize: 2124 Raw data (/proc/16978/stat): 16978 (minisat+_64-bit) R 16974 16974 9102 0 -1 0 31076 0 0 0 109525 210 0 0 25 0 1 0 1843524588 126537728 30611 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/16978/statm): 30893 30611 145 145 0 30748 0 [pid=16978] vsize: 123572 Current children cumulated CPU time (s) 1097.35 Current children cumulated vsize (Kb) 125696 [startup+1110.11 s] Raw data (loadavg): 0.99 0.97 0.97 2/58 17016 Raw data (/proc/16974/stat): 16974 (minisat+_script) S 16973 16974 9102 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843524583 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/16974/statm): 531 226 485 147 0 384 0 [pid=16974] vsize: 2124 Raw data (/proc/16978/stat): 16978 (minisat+_64-bit) R 16974 16974 9102 0 -1 0 31310 0 0 0 110520 212 0 0 25 0 1 0 1843524588 127500288 30845 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/16978/statm): 31128 30845 145 145 0 30983 0 [pid=16978] vsize: 124512 Current children cumulated CPU time (s) 1107.32 Current children cumulated vsize (Kb) 126636 [startup+1120.11 s] Raw data (loadavg): 0.99 0.97 0.97 2/58 17016 Raw data (/proc/16974/stat): 16974 (minisat+_script) S 16973 16974 9102 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843524583 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/16974/statm): 531 226 485 147 0 384 0 [pid=16974] vsize: 2124 Raw data (/proc/16978/stat): 16978 (minisat+_64-bit) R 16974 16974 9102 0 -1 0 31543 0 0 0 111516 213 0 0 25 0 1 0 1843524588 128442368 31078 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/16978/statm): 31358 31078 145 145 0 31213 0 [pid=16978] vsize: 125432 Current children cumulated CPU time (s) 1117.29 Current children cumulated vsize (Kb) 127556 [startup+1130.11 s] Raw data (loadavg): 0.99 0.97 0.97 2/58 17016 Raw data (/proc/16974/stat): 16974 (minisat+_script) S 16973 16974 9102 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843524583 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/16974/statm): 531 226 485 147 0 384 0 [pid=16974] vsize: 2124 Raw data (/proc/16978/stat): 16978 (minisat+_64-bit) R 16974 16974 9102 0 -1 0 31873 0 0 0 112510 217 0 0 25 0 1 0 1843524588 129789952 31408 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/16978/statm): 31687 31408 145 145 0 31542 0 [pid=16978] vsize: 126748 Current children cumulated CPU time (s) 1127.27 Current children cumulated vsize (Kb) 128872 [startup+1140.11 s] Raw data (loadavg): 0.99 0.97 0.97 2/58 17016 Raw data (/proc/16974/stat): 16974 (minisat+_script) S 16973 16974 9102 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843524583 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/16974/statm): 531 226 485 147 0 384 0 [pid=16974] vsize: 2124 Raw data (/proc/16978/stat): 16978 (minisat+_64-bit) R 16974 16974 9102 0 -1 0 32100 0 0 0 113505 218 0 0 25 0 1 0 1843524588 130711552 31635 4294967295 134512640 135094434 3221224448 3221223104 134558004 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/16978/statm): 31912 31635 145 145 0 31767 0 [pid=16978] vsize: 127648 Current children cumulated CPU time (s) 1137.23 Current children cumulated vsize (Kb) 129772 [startup+1150.11 s] Raw data (loadavg): 0.99 0.97 0.97 2/58 17016 Raw data (/proc/16974/stat): 16974 (minisat+_script) S 16973 16974 9102 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843524583 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/16974/statm): 531 226 485 147 0 384 0 [pid=16974] vsize: 2124 Raw data (/proc/16978/stat): 16978 (minisat+_64-bit) R 16974 16974 9102 0 -1 0 32316 0 0 0 114501 220 0 0 25 0 1 0 1843524588 131596288 31851 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/16978/statm): 32128 31851 145 145 0 31983 0 [pid=16978] vsize: 128512 Current children cumulated CPU time (s) 1147.21 Current children cumulated vsize (Kb) 130636 [startup+1160.11 s] Raw data (loadavg): 0.99 0.97 0.97 2/58 17018 Raw data (/proc/16974/stat): 16974 (minisat+_script) S 16973 16974 9102 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843524583 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/16974/statm): 531 226 485 147 0 384 0 [pid=16974] vsize: 2124 Raw data (/proc/16978/stat): 16978 (minisat+_64-bit) R 16974 16974 9102 0 -1 0 32605 0 0 0 115496 222 0 0 25 0 1 0 1843524588 132780032 32140 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/16978/statm): 32417 32140 145 145 0 32272 0 [pid=16978] vsize: 129668 Current children cumulated CPU time (s) 1157.18 Current children cumulated vsize (Kb) 131792 [startup+1170.11 s] Raw data (loadavg): 0.99 0.97 0.97 2/58 17018 Raw data (/proc/16974/stat): 16974 (minisat+_script) S 16973 16974 9102 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843524583 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/16974/statm): 531 226 485 147 0 384 0 [pid=16974] vsize: 2124 Raw data (/proc/16978/stat): 16978 (minisat+_64-bit) R 16974 16974 9102 0 -1 0 32842 0 0 0 116491 224 0 0 25 0 1 0 1843524588 133734400 32377 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/16978/statm): 32650 32377 145 145 0 32505 0 [pid=16978] vsize: 130600 Current children cumulated CPU time (s) 1167.15 Current children cumulated vsize (Kb) 132724 [startup+1180.11 s] Raw data (loadavg): 0.99 0.97 0.97 2/58 17018 Raw data (/proc/16974/stat): 16974 (minisat+_script) S 16973 16974 9102 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843524583 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/16974/statm): 531 226 485 147 0 384 0 [pid=16974] vsize: 2124 Raw data (/proc/16978/stat): 16978 (minisat+_64-bit) R 16974 16974 9102 0 -1 0 33092 0 0 0 117485 226 0 0 25 0 1 0 1843524588 134754304 32627 4294967295 134512640 135094434 3221224448 3221223136 134554733 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/16978/statm): 32899 32627 145 145 0 32754 0 [pid=16978] vsize: 131596 Current children cumulated CPU time (s) 1177.11 Current children cumulated vsize (Kb) 133720 [startup+1190.11 s] Raw data (loadavg): 0.99 0.97 0.97 2/58 17018 Raw data (/proc/16974/stat): 16974 (minisat+_script) S 16973 16974 9102 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843524583 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/16974/statm): 531 226 485 147 0 384 0 [pid=16974] vsize: 2124 Raw data (/proc/16978/stat): 16978 (minisat+_64-bit) R 16974 16974 9102 0 -1 0 33345 0 0 0 118481 228 0 0 25 0 1 0 1843524588 135790592 32880 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/16978/statm): 33152 32880 145 145 0 33007 0 [pid=16978] vsize: 132608 Current children cumulated CPU time (s) 1187.09 Current children cumulated vsize (Kb) 134732 [startup+1200.11 s] Raw data (loadavg): 0.99 0.97 0.97 2/58 17018 Raw data (/proc/16974/stat): 16974 (minisat+_script) S 16973 16974 9102 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843524583 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/16974/statm): 531 226 485 147 0 384 0 [pid=16974] vsize: 2124 Raw data (/proc/16978/stat): 16978 (minisat+_64-bit) R 16974 16974 9102 0 -1 0 33594 0 0 0 119476 229 0 0 25 0 1 0 1843524588 136806400 33129 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/16978/statm): 33400 33129 145 145 0 33255 0 [pid=16978] vsize: 133600 Current children cumulated CPU time (s) 1197.05 Current children cumulated vsize (Kb) 135724 [startup+1210.12 s] Raw data (loadavg): 0.99 0.97 0.97 2/58 17018 Raw data (/proc/16974/stat): 16974 (minisat+_script) S 16973 16974 9102 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843524583 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/16974/statm): 531 226 485 147 0 384 0 [pid=16974] vsize: 2124 Raw data (/proc/16978/stat): 16978 (minisat+_64-bit) R 16974 16974 9102 0 -1 0 33805 0 0 0 120473 231 0 0 25 0 1 0 1843524588 137670656 33340 4294967295 134512640 135094434 3221224448 3221223104 134558235 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/16978/statm): 33611 33340 145 145 0 33466 0 [pid=16978] vsize: 134444 Current children cumulated CPU time (s) 1207.04 Current children cumulated vsize (Kb) 136568 Maximum CPU time exceeded: sending SIGTERM then SIGKILL [startup+1210.12 s] Raw data (loadavg): 0.99 0.97 0.97 2/58 17018 Raw data (/proc/16974/stat): 16974 (minisat+_script) S 16973 16974 9102 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843524583 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/16974/statm): 531 226 485 147 0 384 0 [pid=16974] vsize: 2124 Raw data (/proc/16978/stat): 16978 (minisat+_64-bit) R 16974 16974 9102 0 -1 0 33805 0 0 0 120473 231 0 0 25 0 1 0 1843524588 137670656 33340 4294967295 134512640 135094434 3221224448 3221223104 134557914 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/16978/statm): 33611 33340 145 145 0 33466 0 [pid=16978] vsize: 134444 Current children cumulated CPU time (s) 1207.04 Current children cumulated vsize (Kb) 136568 Sending SIGTERM to -16974 Sleeping 2 seconds One traced child (pid=16974) ended because it received signal 15 (SIGTERM) One traced child (pid=16978) exited with status: 10 All traced children have exited ! Game is over. Child status: 10 Real time (s): 1210.19 CPU time (s): 1207.11 CPU user time (s): 1204.73 CPU system time (s): 2.37964 CPU usage (%): 99.746 Max. virtual memory (cumulated for all children) (Kb): 136568
ERROR: no interpretation found !