Name | web/www.nlsde.buaa.edu.cn/~kexu/benchmarks/frb50-23-opb/normalized-frb50-23-5.opb |
MD5SUM | 54f6acf3ab92bda8abb11350f74de20e |
Bench Category | optimization, small integers (OPTSMALLINT) |
Has Objective Function | YES |
Satisfiable | YES |
(Un)Satisfiability was proved | YES |
Best value of the objective function | -38 |
Optimality of the best value was proved | NO |
Number of terms in the objective function | 1150 |
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 | 1150 |
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 | 1150 |
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 | 1195.05 |
Number of variables | 1150 |
Total number of constraints | 80035 |
Number of constraints which are clauses | 80035 |
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 wulflinc18 THE 2005-09-18 18:50:45 (client local time) PB2005-SCRIPT v4.0 MARKUPS: idlaunch=2708 boxname=wulflinc18 idbench=364 idsolver=3 numberseed=0 MD5SUM SOLVER: MD5SUM BENCH: 54f6acf3ab92bda8abb11350f74de20e /oldhome/oroussel/tmp/wulflinc18/normalized-frb50-23-5.opb REAL COMMAND: minisat+_script /oldhome/oroussel/tmp/wulflinc18/normalized-frb50-23-5.opb IDLAUNCH: 2708 /proc/cpuinfo: processor : 0 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 3 cpu MHz : 451.177 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.177 cache size : 512 KB fdiv_bug : no hlt_bug : no f00f_bug : no coma_bug : no fpu : yes fpu_exception : yes cpuid level : 2 wp : yes flags : fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse bogomips : 899.07 /proc/meminfo: MemTotal: 1034660 kB MemFree: 914332 kB Buffers: 35320 kB Cached: 49992 kB SwapCached: 844 kB Active: 68000 kB Inactive: 19896 kB HighTotal: 131008 kB HighFree: 78120 kB LowTotal: 903652 kB LowFree: 836212 kB SwapTotal: 2097892 kB SwapFree: 2096548 kB Dirty: 28 kB Writeback: 0 kB Mapped: 5764 kB Slab: 26784 kB Committed_AS: 64184 kB PageTables: 328 kB VmallocTotal: 114680 kB VmallocUsed: 1368 kB VmallocChunk: 113252 kB JOB ENDED THE 2005-09-18 19:10:55 (client local time) WITH STATUS 10 IN 1208 SECONDS stats: 2708 7 1208 10
c Parsing PB file... c Converting 80035 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 | 80035 160070 | 26678 0 0 nan | 0.000 % | c ============================================================================== c [1mFound solution: -37[0m c ---[ 0]---> Sorter-cost:63046 Base: c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 0 | 147951 319392 | 49317 0 0 nan | 0.000 % | c | 100 | 147312 318040 | 54248 57 1282 22.5 | 0.772 % | c | 251 | 146773 316900 | 59673 187 2917 15.6 | 1.422 % | c | 476 | 145213 313544 | 65640 368 5352 14.5 | 3.429 % | c | 813 | 143505 309796 | 72205 621 8354 13.5 | 5.644 % | c | 1320 | 139677 301273 | 79425 1008 13306 13.2 | 10.638 % | c | 2079 | 135693 292365 | 87368 1543 19391 12.6 | 15.964 % | c | 3218 | 129784 278974 | 96104 2359 29829 12.6 | 24.035 % | c | 4926 | 122432 262085 | 105715 3616 48944 13.5 | 34.279 % | c | 7488 | 111938 237654 | 116286 5258 69109 13.1 | 49.006 % | c | 11332 | 101310 212553 | 127915 7785 111547 14.3 | 64.438 % | c ============================================================================== c [1mFound solution: -38[0m c ---[ 0]---> Sorter-cost: 0 Base: c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 14084 | 96816 201835 | 32272 9412 143299 15.2 | 64.438 % | c | 14184 | 96772 201727 | 35499 9499 144028 15.2 | 71.052 % | c | 14334 | 96570 201231 | 39049 9550 144833 15.2 | 71.359 % | c | 14560 | 96295 200569 | 42954 9703 147277 15.2 | 71.772 % | c ============================================================================== c [1mFound solution: -40[0m c ---[ 0]---> Sorter-cost: 0 Base: c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 14788 | 96036 200007 | 32012 9819 147145 15.0 | 71.772 % | c | 14888 | 96036 200007 | 35213 9919 148330 15.0 | 72.243 % | c | 15038 | 96036 200007 | 38734 10069 149721 14.9 | 72.243 % | c | 15263 | 96036 200007 | 42607 10294 154570 15.0 | 72.243 % | c | 15600 | 95761 199378 | 46868 10569 160536 15.2 | 72.625 % | c | 16106 | 95153 197892 | 51555 10886 169202 15.5 | 73.553 % | c | 16865 | 94758 196946 | 56711 11525 181628 15.8 | 74.144 % | c | 18004 | 94310 195868 | 62382 12430 205545 16.5 | 74.813 % | c | 19713 | 94001 195126 | 68620 13894 265668 19.1 | 75.275 % | c | 22276 | 92381 191245 | 75482 15687 319719 20.4 | 77.691 % | c | 26120 | 91522 189173 | 83030 19074 495885 26.0 | 78.980 % | c ============================================================================== c [1mFound solution: -41[0m c ---[ 0]---> Sorter-cost: 0 Base: c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 27853 | 91077 188149 | 30359 20461 588458 28.8 | 78.980 % | c | 27953 | 91077 188149 | 33394 20561 590686 28.7 | 79.629 % | c | 28103 | 91026 188021 | 36734 20631 592469 28.7 | 79.706 % | c | 28328 | 91026 188021 | 40407 20856 599678 28.8 | 79.706 % | c | 28665 | 91026 188021 | 44448 21193 622260 29.4 | 79.706 % | c ============================================================================== c [1mFound solution: -42[0m c ---[ 0]---> Sorter-cost: 0 Base: c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 28969 | 90731 187263 | 30243 21322 628608 29.5 | 79.706 % | c | 29069 | 90722 187240 | 33267 21414 632006 29.5 | 80.173 % | c | 29219 | 90593 186934 | 36594 21396 633325 29.6 | 80.358 % | c | 29445 | 90536 186795 | 40253 21617 652375 30.2 | 80.447 % | c | 29782 | 90499 186706 | 44278 21904 668251 30.5 | 80.503 % | c | 30289 | 90299 186216 | 48706 22108 682253 30.9 | 80.809 % | c | 31048 | 90231 186060 | 53577 22782 711877 31.2 | 80.904 % | c | 32187 | 89778 184940 | 58935 23599 766824 32.5 | 81.598 % | c | 33896 | 89773 184929 | 64828 25280 869667 34.4 | 81.605 % | c | 36458 | 89601 184511 | 71311 27781 1104154 39.7 | 81.868 % | c | 40303 | 89001 183057 | 78442 30883 1452224 47.0 | 82.782 % | c | 46069 | 88653 182193 | 86286 36261 1909440 52.7 | 83.326 % | 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 | 53577 | 88651 182222 | 29550 43705 2561808 58.6 | 83.326 % | c | 53677 | 88651 182222 | 32505 43805 2563789 58.5 | 83.359 % | c | 53827 | 88622 182151 | 35755 43811 2568576 58.6 | 83.404 % | c | 54052 | 88622 182151 | 39331 44036 2589935 58.8 | 83.404 % | c | 54389 | 88537 181938 | 43264 44316 2602581 58.7 | 83.542 % | c | 54895 | 88502 181851 | 47590 44743 2640960 59.0 | 83.598 % | c | 55654 | 88489 181818 | 52349 45410 2688658 59.2 | 83.620 % | c | 56795 | 88255 181245 | 57584 46245 2798146 60.5 | 83.970 % | c | 58504 | 88255 181245 | 63343 47954 2931810 61.1 | 83.970 % | c | 61066 | 88117 180910 | 69677 50021 3189748 63.8 | 84.181 % | c | 64910 | 88088 180842 | 76645 53834 3616238 67.2 | 84.220 % | c | 70676 | 88083 180831 | 84309 59598 4123646 69.2 | 84.226 % | 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 | 76602 | 87920 180446 | 29306 64994 4731142 72.8 | 84.226 % | c | 76704 | 87920 180446 | 32236 65096 4739491 72.8 | 84.488 % | c | 76855 | 87920 180446 | 35460 65247 4745429 72.7 | 84.488 % | c | 77080 | 87920 180446 | 39006 65472 4759519 72.7 | 84.488 % | c | 77417 | 87920 180446 | 42906 65809 4783089 72.7 | 84.488 % | c | 77924 | 87920 180446 | 47197 66316 4834519 72.9 | 84.488 % | c | 78684 | 87915 180435 | 51917 67073 4915209 73.3 | 84.494 % | c | 79823 | 87782 180128 | 57109 67701 5020176 74.2 | 84.681 % | c | 81531 | 87629 179763 | 62820 69363 5207979 75.1 | 84.907 % | c | 84093 | 87629 179763 | 69102 71925 5462668 75.9 | 84.907 % | c | 87937 | 87629 179763 | 76012 75769 5852613 77.2 | 84.907 % | c | 93703 | 87615 179727 | 83613 81487 6335995 77.8 | 84.931 % | c | 102352 | 87615 179727 | 91974 90136 7289858 80.9 | 84.931 % | c | 115328 | 87613 179723 | 101172 103111 8798918 85.3 | 84.933 % | c | 134790 | 87540 179550 | 111289 122522 11000809 89.8 | 85.040 % | c | 163982 | 87270 178893 | 122418 150898 14231492 94.3 | 85.455 % | c | 207771 | 87197 178706 | 134660 54694 5876777 107.4 | 85.578 % | c | 273455 | 87182 178671 | 148126 120376 10322069 85.7 | 85.599 % | c c *** TERMINATED *** s SATISFIABLE v -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
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/5448/stat): 5448 (minisat+_script) R 5447 5448 31027 0 -1 0 19 0 0 0 0 0 0 0 23 0 1 0 1843516560 712704 3 4294967295 134512640 135087896 3221224512 3221224512 1073744960 0 0 5 0 0 0 0 17 0 0 0 Raw data (/proc/5448/statm): 174 3 169 147 0 27 0 [pid=5448] 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=5449 New process pid=5450 New process pid=5451 execve syscall for /bin/sed executable One traced child (pid=5450) exited with status: 0 open syscall for file /etc/ld.so.preload open syscall for file tls/i686/mmx/libc.so.6 open syscall for file tls/i686/libc.so.6 open syscall for file tls/mmx/libc.so.6 open syscall for file tls/libc.so.6 open syscall for file i686/mmx/libc.so.6 open syscall for file i686/libc.so.6 open syscall for file mmx/libc.so.6 open syscall for file libc.so.6 open syscall for file /oldhome/oroussel/lib/tls/i686/mmx/libc.so.6 open syscall for file /oldhome/oroussel/lib/tls/i686/libc.so.6 open syscall for file /oldhome/oroussel/lib/tls/mmx/libc.so.6 open syscall for file /oldhome/oroussel/lib/tls/libc.so.6 open syscall for file /oldhome/oroussel/lib/i686/mmx/libc.so.6 open syscall for file /oldhome/oroussel/lib/i686/libc.so.6 open syscall for file /oldhome/oroussel/lib/mmx/libc.so.6 open syscall for file /oldhome/oroussel/lib/libc.so.6 open syscall for file /etc/ld.so.cache open syscall for file /lib/tls/libc.so.6 One traced child (pid=5451) exited with status: 0 One traced child (pid=5449) exited with status: 0 New process pid=5452 execve syscall for /oldhome/oroussel/solvers/minisat+_64-bit_static executable open syscall for file /dev/null open syscall for file /oldhome/oroussel/tmp/wulflinc18/normalized-frb50-23-5.opb [startup+10.0035 s] Raw data (loadavg): 0.95 0.97 0.96 2/57 5452 Raw data (/proc/5448/stat): 5448 (minisat+_script) S 5447 5448 31027 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843516560 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/5448/statm): 531 226 485 147 0 384 0 [pid=5448] vsize: 2124 Raw data (/proc/5452/stat): 5452 (minisat+_64-bit) R 5448 5448 31027 0 -1 0 5059 0 0 0 957 24 0 0 25 0 1 0 1843516564 21630976 5046 4294967295 134512640 135094434 3221224448 3221223108 134553501 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/5452/statm): 5281 5046 145 145 0 5136 0 [pid=5452] vsize: 21124 Current children cumulated CPU time (s) 9.81 Current children cumulated vsize (Kb) 23248 [startup+20.0044 s] Raw data (loadavg): 0.96 0.97 0.96 2/57 5452 Raw data (/proc/5448/stat): 5448 (minisat+_script) S 5447 5448 31027 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843516560 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/5448/statm): 531 226 485 147 0 384 0 [pid=5448] vsize: 2124 Raw data (/proc/5452/stat): 5452 (minisat+_64-bit) R 5448 5448 31027 0 -1 0 5059 0 0 0 1957 24 0 0 25 0 1 0 1843516564 21630976 5046 4294967295 134512640 135094434 3221224448 3221223104 134557840 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/5452/statm): 5281 5046 145 145 0 5136 0 [pid=5452] vsize: 21124 Current children cumulated CPU time (s) 19.81 Current children cumulated vsize (Kb) 23248 [startup+30.0064 s] Raw data (loadavg): 1.04 0.99 0.96 2/57 5452 Raw data (/proc/5448/stat): 5448 (minisat+_script) S 5447 5448 31027 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843516560 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/5448/statm): 531 226 485 147 0 384 0 [pid=5448] vsize: 2124 Raw data (/proc/5452/stat): 5452 (minisat+_64-bit) R 5448 5448 31027 0 -1 0 5059 0 0 0 2956 25 0 0 25 0 1 0 1843516564 21630976 5046 4294967295 134512640 135094434 3221224448 3221223104 134558159 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/5452/statm): 5281 5046 145 145 0 5136 0 [pid=5452] vsize: 21124 Current children cumulated CPU time (s) 29.81 Current children cumulated vsize (Kb) 23248 [startup+40.0073 s] Raw data (loadavg): 1.04 0.99 0.96 2/57 5452 Raw data (/proc/5448/stat): 5448 (minisat+_script) S 5447 5448 31027 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843516560 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/5448/statm): 531 226 485 147 0 384 0 [pid=5448] vsize: 2124 Raw data (/proc/5452/stat): 5452 (minisat+_64-bit) R 5448 5448 31027 0 -1 0 5059 0 0 0 3956 25 0 0 25 0 1 0 1843516564 21630976 5046 4294967295 134512640 135094434 3221224448 3221223116 134553438 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/5452/statm): 5281 5046 145 145 0 5136 0 [pid=5452] vsize: 21124 Current children cumulated CPU time (s) 39.81 Current children cumulated vsize (Kb) 23248 [startup+50.0092 s] Raw data (loadavg): 1.03 0.99 0.96 2/57 5452 Raw data (/proc/5448/stat): 5448 (minisat+_script) S 5447 5448 31027 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843516560 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/5448/statm): 531 226 485 147 0 384 0 [pid=5448] vsize: 2124 Raw data (/proc/5452/stat): 5452 (minisat+_64-bit) R 5448 5448 31027 0 -1 0 5059 0 0 0 4955 26 0 0 25 0 1 0 1843516564 21630976 5046 4294967295 134512640 135094434 3221224448 3221223040 134557180 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/5452/statm): 5281 5046 145 145 0 5136 0 [pid=5452] vsize: 21124 Current children cumulated CPU time (s) 49.81 Current children cumulated vsize (Kb) 23248 [startup+60.0101 s] Raw data (loadavg): 1.02 0.99 0.96 2/57 5452 Raw data (/proc/5448/stat): 5448 (minisat+_script) S 5447 5448 31027 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843516560 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/5448/statm): 531 226 485 147 0 384 0 [pid=5448] vsize: 2124 Raw data (/proc/5452/stat): 5452 (minisat+_64-bit) R 5448 5448 31027 0 -1 0 5061 0 0 0 5955 26 0 0 25 0 1 0 1843516564 21630976 5048 4294967295 134512640 135094434 3221224448 3221223136 134554731 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/5452/statm): 5281 5048 145 145 0 5136 0 [pid=5452] vsize: 21124 Current children cumulated CPU time (s) 59.81 Current children cumulated vsize (Kb) 23248 [startup+70.0111 s] Raw data (loadavg): 1.02 0.99 0.96 2/57 5452 Raw data (/proc/5448/stat): 5448 (minisat+_script) S 5447 5448 31027 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843516560 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/5448/statm): 531 226 485 147 0 384 0 [pid=5448] vsize: 2124 Raw data (/proc/5452/stat): 5452 (minisat+_64-bit) R 5448 5448 31027 0 -1 0 5075 0 0 0 6954 26 0 0 25 0 1 0 1843516564 21688320 5062 4294967295 134512640 135094434 3221224448 3221223108 134553446 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/5452/statm): 5295 5062 145 145 0 5150 0 [pid=5452] vsize: 21180 Current children cumulated CPU time (s) 69.8 Current children cumulated vsize (Kb) 23304 [startup+80.013 s] Raw data (loadavg): 1.02 0.99 0.96 2/57 5452 Raw data (/proc/5448/stat): 5448 (minisat+_script) S 5447 5448 31027 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843516560 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/5448/statm): 531 226 485 147 0 384 0 [pid=5448] vsize: 2124 Raw data (/proc/5452/stat): 5452 (minisat+_64-bit) R 5448 5448 31027 0 -1 0 5107 0 0 0 7954 27 0 0 25 0 1 0 1843516564 21843968 5094 4294967295 134512640 135094434 3221224448 3221223104 134558398 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/5452/statm): 5333 5094 145 145 0 5188 0 [pid=5452] vsize: 21332 Current children cumulated CPU time (s) 79.81 Current children cumulated vsize (Kb) 23456 [startup+90.0139 s] Raw data (loadavg): 1.01 0.99 0.96 2/57 5452 Raw data (/proc/5448/stat): 5448 (minisat+_script) S 5447 5448 31027 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843516560 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/5448/statm): 531 226 485 147 0 384 0 [pid=5448] vsize: 2124 Raw data (/proc/5452/stat): 5452 (minisat+_64-bit) R 5448 5448 31027 0 -1 0 5411 0 0 0 8952 29 0 0 25 0 1 0 1843516564 23953408 5398 4294967295 134512640 135094434 3221224448 3221223104 134557948 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/5452/statm): 5848 5398 145 145 0 5703 0 [pid=5452] vsize: 23392 Current children cumulated CPU time (s) 89.81 Current children cumulated vsize (Kb) 25516 [startup+100.016 s] Raw data (loadavg): 1.09 1.00 0.97 2/57 5452 Raw data (/proc/5448/stat): 5448 (minisat+_script) S 5447 5448 31027 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843516560 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/5448/statm): 531 226 485 147 0 384 0 [pid=5448] vsize: 2124 Raw data (/proc/5452/stat): 5452 (minisat+_64-bit) R 5448 5448 31027 0 -1 0 5465 0 0 0 9950 30 0 0 25 0 1 0 1843516564 24158208 5452 4294967295 134512640 135094434 3221224448 3221223072 134557714 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/5452/statm): 5898 5452 145 145 0 5753 0 [pid=5452] vsize: 23592 Current children cumulated CPU time (s) 99.8 Current children cumulated vsize (Kb) 25716 [startup+110.018 s] Raw data (loadavg): 1.08 1.00 0.97 2/57 5452 Raw data (/proc/5448/stat): 5448 (minisat+_script) S 5447 5448 31027 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843516560 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/5448/statm): 531 226 485 147 0 384 0 [pid=5448] vsize: 2124 Raw data (/proc/5452/stat): 5452 (minisat+_64-bit) R 5448 5448 31027 0 -1 0 5865 0 0 0 10945 32 0 0 25 0 1 0 1843516564 25649152 5805 4294967295 134512640 135094434 3221224448 3221223104 134558213 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/5452/statm): 6262 5805 145 145 0 6117 0 [pid=5452] vsize: 25048 Current children cumulated CPU time (s) 109.77 Current children cumulated vsize (Kb) 27172 [startup+120.019 s] Raw data (loadavg): 1.06 1.00 0.97 2/57 5452 Raw data (/proc/5448/stat): 5448 (minisat+_script) S 5447 5448 31027 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843516560 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/5448/statm): 531 226 485 147 0 384 0 [pid=5448] vsize: 2124 Raw data (/proc/5452/stat): 5452 (minisat+_64-bit) R 5448 5448 31027 0 -1 0 6202 0 0 0 11939 35 0 0 25 0 1 0 1843516564 26824704 6096 4294967295 134512640 135094434 3221224448 3221223084 134557560 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/5452/statm): 6549 6096 145 145 0 6404 0 [pid=5452] vsize: 26196 Current children cumulated CPU time (s) 119.74 Current children cumulated vsize (Kb) 28320 [startup+130.02 s] Raw data (loadavg): 1.05 1.00 0.97 2/57 5452 Raw data (/proc/5448/stat): 5448 (minisat+_script) S 5447 5448 31027 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843516560 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/5448/statm): 531 226 485 147 0 384 0 [pid=5448] vsize: 2124 Raw data (/proc/5452/stat): 5452 (minisat+_64-bit) R 5448 5448 31027 0 -1 0 6777 0 0 0 12929 39 0 0 25 0 1 0 1843516564 29163520 6671 4294967295 134512640 135094434 3221224448 3221223120 134556528 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/5452/statm): 7120 6671 145 145 0 6975 0 [pid=5452] vsize: 28480 Current children cumulated CPU time (s) 129.68 Current children cumulated vsize (Kb) 30604 [startup+140.021 s] Raw data (loadavg): 1.05 1.00 0.97 2/57 5452 Raw data (/proc/5448/stat): 5448 (minisat+_script) S 5447 5448 31027 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843516560 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/5448/statm): 531 226 485 147 0 384 0 [pid=5448] vsize: 2124 Raw data (/proc/5452/stat): 5452 (minisat+_64-bit) R 5448 5448 31027 0 -1 0 7187 0 0 0 13922 42 0 0 25 0 1 0 1843516564 30957568 7081 4294967295 134512640 135094434 3221224448 3221223104 134558187 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/5452/statm): 7558 7081 145 145 0 7413 0 [pid=5452] vsize: 30232 Current children cumulated CPU time (s) 139.64 Current children cumulated vsize (Kb) 32356 [startup+150.022 s] Raw data (loadavg): 1.04 1.00 0.97 2/57 5452 Raw data (/proc/5448/stat): 5448 (minisat+_script) S 5447 5448 31027 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843516560 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/5448/statm): 531 226 485 147 0 384 0 [pid=5448] vsize: 2124 Raw data (/proc/5452/stat): 5452 (minisat+_64-bit) R 5448 5448 31027 0 -1 0 7577 0 0 0 14914 45 0 0 25 0 1 0 1843516564 32530432 7471 4294967295 134512640 135094434 3221224448 3221223104 134558007 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/5452/statm): 7942 7471 145 145 0 7797 0 [pid=5452] vsize: 31768 Current children cumulated CPU time (s) 149.59 Current children cumulated vsize (Kb) 33892 [startup+160.023 s] Raw data (loadavg): 1.03 1.00 0.97 2/57 5452 Raw data (/proc/5448/stat): 5448 (minisat+_script) S 5447 5448 31027 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843516560 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/5448/statm): 531 226 485 147 0 384 0 [pid=5448] vsize: 2124 Raw data (/proc/5452/stat): 5452 (minisat+_64-bit) R 5448 5448 31027 0 -1 0 8104 0 0 0 15905 49 0 0 25 0 1 0 1843516564 34480128 7951 4294967295 134512640 135094434 3221224448 3221223108 134553499 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/5452/statm): 8418 7951 145 145 0 8273 0 [pid=5452] vsize: 33672 Current children cumulated CPU time (s) 159.54 Current children cumulated vsize (Kb) 35796 [startup+170.024 s] Raw data (loadavg): 1.03 1.00 0.97 2/57 5452 Raw data (/proc/5448/stat): 5448 (minisat+_script) S 5447 5448 31027 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843516560 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/5448/statm): 531 226 485 147 0 384 0 [pid=5448] vsize: 2124 Raw data (/proc/5452/stat): 5452 (minisat+_64-bit) R 5448 5448 31027 0 -1 0 8385 0 0 0 16900 50 0 0 25 0 1 0 1843516564 35618816 8232 4294967295 134512640 135094434 3221224448 3221223104 134558235 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/5452/statm): 8696 8232 145 145 0 8551 0 [pid=5452] vsize: 34784 Current children cumulated CPU time (s) 169.5 Current children cumulated vsize (Kb) 36908 [startup+180.025 s] Raw data (loadavg): 1.02 1.00 0.97 2/57 5452 Raw data (/proc/5448/stat): 5448 (minisat+_script) S 5447 5448 31027 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843516560 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/5448/statm): 531 226 485 147 0 384 0 [pid=5448] vsize: 2124 Raw data (/proc/5452/stat): 5452 (minisat+_64-bit) R 5448 5448 31027 0 -1 0 8810 0 0 0 17892 54 0 0 25 0 1 0 1843516564 37347328 8657 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/5452/statm): 9118 8657 145 145 0 8973 0 [pid=5452] vsize: 36472 Current children cumulated CPU time (s) 179.46 Current children cumulated vsize (Kb) 38596 [startup+190.026 s] Raw data (loadavg): 1.02 1.00 0.97 2/57 5452 Raw data (/proc/5448/stat): 5448 (minisat+_script) S 5447 5448 31027 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843516560 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/5448/statm): 531 226 485 147 0 384 0 [pid=5448] vsize: 2124 Raw data (/proc/5452/stat): 5452 (minisat+_64-bit) R 5448 5448 31027 0 -1 0 9289 0 0 0 18881 59 0 0 25 0 1 0 1843516564 39288832 9136 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/5452/statm): 9592 9136 145 145 0 9447 0 [pid=5452] vsize: 38368 Current children cumulated CPU time (s) 189.4 Current children cumulated vsize (Kb) 40492 [startup+200.027 s] Raw data (loadavg): 1.02 1.00 0.97 2/57 5452 Raw data (/proc/5448/stat): 5448 (minisat+_script) S 5447 5448 31027 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843516560 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/5448/statm): 531 226 485 147 0 384 0 [pid=5448] vsize: 2124 Raw data (/proc/5452/stat): 5452 (minisat+_64-bit) R 5448 5448 31027 0 -1 0 9679 0 0 0 19875 62 0 0 25 0 1 0 1843516564 40873984 9526 4294967295 134512640 135094434 3221224448 3221223104 134557900 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/5452/statm): 9979 9526 145 145 0 9834 0 [pid=5452] vsize: 39916 Current children cumulated CPU time (s) 199.37 Current children cumulated vsize (Kb) 42040 [startup+210.028 s] Raw data (loadavg): 1.01 1.00 0.97 2/57 5452 Raw data (/proc/5448/stat): 5448 (minisat+_script) S 5447 5448 31027 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843516560 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/5448/statm): 531 226 485 147 0 384 0 [pid=5448] vsize: 2124 Raw data (/proc/5452/stat): 5452 (minisat+_64-bit) R 5448 5448 31027 0 -1 0 10120 0 0 0 20866 65 0 0 25 0 1 0 1843516564 42663936 9967 4294967295 134512640 135094434 3221224448 3221223108 134553482 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/5452/statm): 10416 9967 145 145 0 10271 0 [pid=5452] vsize: 41664 Current children cumulated CPU time (s) 209.31 Current children cumulated vsize (Kb) 43788 [startup+220.029 s] Raw data (loadavg): 1.01 1.00 0.97 2/57 5452 Raw data (/proc/5448/stat): 5448 (minisat+_script) S 5447 5448 31027 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843516560 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/5448/statm): 531 226 485 147 0 384 0 [pid=5448] vsize: 2124 Raw data (/proc/5452/stat): 5452 (minisat+_64-bit) R 5448 5448 31027 0 -1 0 10405 0 0 0 21862 68 0 0 25 0 1 0 1843516564 43823104 10252 4294967295 134512640 135094434 3221224448 3221223040 134557219 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/5452/statm): 10699 10252 145 145 0 10554 0 [pid=5452] vsize: 42796 Current children cumulated CPU time (s) 219.3 Current children cumulated vsize (Kb) 44920 [startup+230.03 s] Raw data (loadavg): 1.01 1.00 0.97 2/57 5452 Raw data (/proc/5448/stat): 5448 (minisat+_script) S 5447 5448 31027 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843516560 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/5448/statm): 531 226 485 147 0 384 0 [pid=5448] vsize: 2124 Raw data (/proc/5452/stat): 5452 (minisat+_64-bit) R 5448 5448 31027 0 -1 0 10758 0 0 0 22855 71 0 0 25 0 1 0 1843516564 45330432 10559 4294967295 134512640 135094434 3221224448 3221223108 134553489 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/5452/statm): 11067 10559 145 145 0 10922 0 [pid=5452] vsize: 44268 Current children cumulated CPU time (s) 229.26 Current children cumulated vsize (Kb) 46392 [startup+240.031 s] Raw data (loadavg): 1.01 1.00 0.97 2/57 5452 Raw data (/proc/5448/stat): 5448 (minisat+_script) S 5447 5448 31027 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843516560 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/5448/statm): 531 226 485 147 0 384 0 [pid=5448] vsize: 2124 Raw data (/proc/5452/stat): 5452 (minisat+_64-bit) R 5448 5448 31027 0 -1 0 11073 0 0 0 23848 74 0 0 25 0 1 0 1843516564 46612480 10874 4294967295 134512640 135094434 3221224448 3221223040 134557273 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/5452/statm): 11380 10874 145 145 0 11235 0 [pid=5452] vsize: 45520 Current children cumulated CPU time (s) 239.22 Current children cumulated vsize (Kb) 47644 [startup+250.032 s] Raw data (loadavg): 1.00 1.00 0.97 2/57 5452 Raw data (/proc/5448/stat): 5448 (minisat+_script) S 5447 5448 31027 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843516560 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/5448/statm): 531 226 485 147 0 384 0 [pid=5448] vsize: 2124 Raw data (/proc/5452/stat): 5452 (minisat+_64-bit) R 5448 5448 31027 0 -1 0 11413 0 0 0 24841 77 0 0 25 0 1 0 1843516564 47988736 11214 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/5452/statm): 11716 11214 145 145 0 11571 0 [pid=5452] vsize: 46864 Current children cumulated CPU time (s) 249.18 Current children cumulated vsize (Kb) 48988 [startup+260.033 s] Raw data (loadavg): 1.00 1.00 0.97 2/57 5452 Raw data (/proc/5448/stat): 5448 (minisat+_script) S 5447 5448 31027 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843516560 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/5448/statm): 531 226 485 147 0 384 0 [pid=5448] vsize: 2124 Raw data (/proc/5452/stat): 5452 (minisat+_64-bit) R 5448 5448 31027 0 -1 0 11724 0 0 0 25834 80 0 0 25 0 1 0 1843516564 49254400 11525 4294967295 134512640 135094434 3221224448 3221223120 134555547 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/5452/statm): 12025 11525 145 145 0 11880 0 [pid=5452] vsize: 48100 Current children cumulated CPU time (s) 259.14 Current children cumulated vsize (Kb) 50224 [startup+270.034 s] Raw data (loadavg): 1.00 1.00 0.97 2/57 5452 Raw data (/proc/5448/stat): 5448 (minisat+_script) S 5447 5448 31027 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843516560 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/5448/statm): 531 226 485 147 0 384 0 [pid=5448] vsize: 2124 Raw data (/proc/5452/stat): 5452 (minisat+_64-bit) R 5448 5448 31027 0 -1 0 11994 0 0 0 26830 82 0 0 25 0 1 0 1843516564 50348032 11795 4294967295 134512640 135094434 3221224448 3221223104 134558178 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/5452/statm): 12292 11795 145 145 0 12147 0 [pid=5452] vsize: 49168 Current children cumulated CPU time (s) 269.12 Current children cumulated vsize (Kb) 51292 [startup+280.034 s] Raw data (loadavg): 1.00 1.00 0.97 2/57 5452 Raw data (/proc/5448/stat): 5448 (minisat+_script) S 5447 5448 31027 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843516560 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/5448/statm): 531 226 485 147 0 384 0 [pid=5448] vsize: 2124 Raw data (/proc/5452/stat): 5452 (minisat+_64-bit) R 5448 5448 31027 0 -1 0 12318 0 0 0 27824 84 0 0 25 0 1 0 1843516564 51662848 12119 4294967295 134512640 135094434 3221224448 3221223040 134557232 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/5452/statm): 12613 12119 145 145 0 12468 0 [pid=5452] vsize: 50452 Current children cumulated CPU time (s) 279.08 Current children cumulated vsize (Kb) 52576 [startup+290.035 s] Raw data (loadavg): 1.00 1.00 0.97 2/57 5452 Raw data (/proc/5448/stat): 5448 (minisat+_script) S 5447 5448 31027 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843516560 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/5448/statm): 531 226 485 147 0 384 0 [pid=5448] vsize: 2124 Raw data (/proc/5452/stat): 5452 (minisat+_64-bit) R 5448 5448 31027 0 -1 0 12602 0 0 0 28819 86 0 0 25 0 1 0 1843516564 52813824 12403 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/5452/statm): 12894 12403 145 145 0 12749 0 [pid=5452] vsize: 51576 Current children cumulated CPU time (s) 289.05 Current children cumulated vsize (Kb) 53700 [startup+300.037 s] Raw data (loadavg): 1.00 1.00 0.97 2/57 5452 Raw data (/proc/5448/stat): 5448 (minisat+_script) S 5447 5448 31027 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843516560 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/5448/statm): 531 226 485 147 0 384 0 [pid=5448] vsize: 2124 Raw data (/proc/5452/stat): 5452 (minisat+_64-bit) R 5448 5448 31027 0 -1 0 12916 0 0 0 29814 88 0 0 25 0 1 0 1843516564 54087680 12717 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/5452/statm): 13205 12717 145 145 0 13060 0 [pid=5452] vsize: 52820 Current children cumulated CPU time (s) 299.02 Current children cumulated vsize (Kb) 54944 [startup+310.038 s] Raw data (loadavg): 1.00 1.00 0.97 2/57 5452 Raw data (/proc/5448/stat): 5448 (minisat+_script) S 5447 5448 31027 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843516560 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/5448/statm): 531 226 485 147 0 384 0 [pid=5448] vsize: 2124 Raw data (/proc/5452/stat): 5452 (minisat+_64-bit) R 5448 5448 31027 0 -1 0 13318 0 0 0 30806 91 0 0 25 0 1 0 1843516564 55726080 13119 4294967295 134512640 135094434 3221224448 3221223104 134557900 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/5452/statm): 13605 13119 145 145 0 13460 0 [pid=5452] vsize: 54420 Current children cumulated CPU time (s) 308.97 Current children cumulated vsize (Kb) 56544 [startup+320.039 s] Raw data (loadavg): 1.00 1.00 0.97 2/57 5452 Raw data (/proc/5448/stat): 5448 (minisat+_script) S 5447 5448 31027 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843516560 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/5448/statm): 531 226 485 147 0 384 0 [pid=5448] vsize: 2124 Raw data (/proc/5452/stat): 5452 (minisat+_64-bit) R 5448 5448 31027 0 -1 0 13641 0 0 0 31799 95 0 0 25 0 1 0 1843516564 57036800 13442 4294967295 134512640 135094434 3221224448 3221223040 134557429 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/5452/statm): 13925 13442 145 145 0 13780 0 [pid=5452] vsize: 55700 Current children cumulated CPU time (s) 318.94 Current children cumulated vsize (Kb) 57824 [startup+330.041 s] Raw data (loadavg): 1.00 1.00 0.97 2/57 5452 Raw data (/proc/5448/stat): 5448 (minisat+_script) S 5447 5448 31027 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843516560 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/5448/statm): 531 226 485 147 0 384 0 [pid=5448] vsize: 2124 Raw data (/proc/5452/stat): 5452 (minisat+_64-bit) R 5448 5448 31027 0 -1 0 14004 0 0 0 32791 98 0 0 25 0 1 0 1843516564 58511360 13805 4294967295 134512640 135094434 3221224448 3221223100 134558255 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/5452/statm): 14285 13805 145 145 0 14140 0 [pid=5452] vsize: 57140 Current children cumulated CPU time (s) 328.89 Current children cumulated vsize (Kb) 59264 [startup+340.042 s] Raw data (loadavg): 1.00 1.00 0.97 2/57 5452 Raw data (/proc/5448/stat): 5448 (minisat+_script) S 5447 5448 31027 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843516560 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/5448/statm): 531 226 485 147 0 384 0 [pid=5448] vsize: 2124 Raw data (/proc/5452/stat): 5452 (minisat+_64-bit) R 5448 5448 31027 0 -1 0 14321 0 0 0 33785 100 0 0 25 0 1 0 1843516564 59801600 14122 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/5452/statm): 14600 14122 145 145 0 14455 0 [pid=5452] vsize: 58400 Current children cumulated CPU time (s) 338.85 Current children cumulated vsize (Kb) 60524 [startup+350.044 s] Raw data (loadavg): 1.00 1.00 0.97 2/57 5452 Raw data (/proc/5448/stat): 5448 (minisat+_script) S 5447 5448 31027 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843516560 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/5448/statm): 531 226 485 147 0 384 0 [pid=5448] vsize: 2124 Raw data (/proc/5452/stat): 5452 (minisat+_64-bit) R 5448 5448 31027 0 -1 0 14606 0 0 0 34780 102 0 0 25 0 1 0 1843516564 60964864 14407 4294967295 134512640 135094434 3221224448 3221223040 134557273 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/5452/statm): 14884 14407 145 145 0 14739 0 [pid=5452] vsize: 59536 Current children cumulated CPU time (s) 348.82 Current children cumulated vsize (Kb) 61660 [startup+360.046 s] Raw data (loadavg): 1.00 1.00 0.97 2/57 5452 Raw data (/proc/5448/stat): 5448 (minisat+_script) S 5447 5448 31027 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843516560 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/5448/statm): 531 226 485 147 0 384 0 [pid=5448] vsize: 2124 Raw data (/proc/5452/stat): 5452 (minisat+_64-bit) R 5448 5448 31027 0 -1 0 14888 0 0 0 35774 105 0 0 25 0 1 0 1843516564 62107648 14689 4294967295 134512640 135094434 3221224448 3221223104 134557884 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/5452/statm): 15163 14689 145 145 0 15018 0 [pid=5452] vsize: 60652 Current children cumulated CPU time (s) 358.79 Current children cumulated vsize (Kb) 62776 [startup+370.047 s] Raw data (loadavg): 1.00 1.00 0.97 2/57 5452 Raw data (/proc/5448/stat): 5448 (minisat+_script) S 5447 5448 31027 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843516560 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/5448/statm): 531 226 485 147 0 384 0 [pid=5448] vsize: 2124 Raw data (/proc/5452/stat): 5452 (minisat+_64-bit) R 5448 5448 31027 0 -1 0 15115 0 0 0 36768 107 0 0 25 0 1 0 1843516564 63025152 14916 4294967295 134512640 135094434 3221224448 3221223108 134553482 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/5452/statm): 15387 14916 145 145 0 15242 0 [pid=5452] vsize: 61548 Current children cumulated CPU time (s) 368.75 Current children cumulated vsize (Kb) 63672 [startup+380.048 s] Raw data (loadavg): 1.00 1.00 0.97 2/57 5452 Raw data (/proc/5448/stat): 5448 (minisat+_script) S 5447 5448 31027 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843516560 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/5448/statm): 531 226 485 147 0 384 0 [pid=5448] vsize: 2124 Raw data (/proc/5452/stat): 5452 (minisat+_64-bit) R 5448 5448 31027 0 -1 0 15441 0 0 0 37761 110 0 0 25 0 1 0 1843516564 64352256 15242 4294967295 134512640 135094434 3221224448 3221223104 134557911 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/5452/statm): 15711 15242 145 145 0 15566 0 [pid=5452] vsize: 62844 Current children cumulated CPU time (s) 378.71 Current children cumulated vsize (Kb) 64968 [startup+390.049 s] Raw data (loadavg): 1.00 1.00 0.97 2/57 5452 Raw data (/proc/5448/stat): 5448 (minisat+_script) S 5447 5448 31027 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843516560 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/5448/statm): 531 226 485 147 0 384 0 [pid=5448] vsize: 2124 Raw data (/proc/5452/stat): 5452 (minisat+_64-bit) R 5448 5448 31027 0 -1 0 15701 0 0 0 38756 113 0 0 25 0 1 0 1843516564 65404928 15502 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/5452/statm): 15968 15502 145 145 0 15823 0 [pid=5452] vsize: 63872 Current children cumulated CPU time (s) 388.69 Current children cumulated vsize (Kb) 65996 [startup+400.051 s] Raw data (loadavg): 1.00 1.00 0.97 2/57 5452 Raw data (/proc/5448/stat): 5448 (minisat+_script) S 5447 5448 31027 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843516560 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/5448/statm): 531 226 485 147 0 384 0 [pid=5448] vsize: 2124 Raw data (/proc/5452/stat): 5452 (minisat+_64-bit) R 5448 5448 31027 0 -1 0 16034 0 0 0 39748 116 0 0 25 0 1 0 1843516564 66760704 15835 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/5452/statm): 16299 15835 145 145 0 16154 0 [pid=5452] vsize: 65196 Current children cumulated CPU time (s) 398.64 Current children cumulated vsize (Kb) 67320 [startup+410.051 s] Raw data (loadavg): 1.00 1.00 0.97 2/57 5452 Raw data (/proc/5448/stat): 5448 (minisat+_script) S 5447 5448 31027 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843516560 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/5448/statm): 531 226 485 147 0 384 0 [pid=5448] vsize: 2124 Raw data (/proc/5452/stat): 5452 (minisat+_64-bit) R 5448 5448 31027 0 -1 0 16352 0 0 0 40739 120 0 0 25 0 1 0 1843516564 68050944 16153 4294967295 134512640 135094434 3221224448 3221223104 134558402 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/5452/statm): 16614 16153 145 145 0 16469 0 [pid=5452] vsize: 66456 Current children cumulated CPU time (s) 408.59 Current children cumulated vsize (Kb) 68580 [startup+420.052 s] Raw data (loadavg): 1.00 1.00 0.97 2/57 5452 Raw data (/proc/5448/stat): 5448 (minisat+_script) S 5447 5448 31027 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843516560 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/5448/statm): 531 226 485 147 0 384 0 [pid=5448] vsize: 2124 Raw data (/proc/5452/stat): 5452 (minisat+_64-bit) R 5448 5448 31027 0 -1 0 16626 0 0 0 41732 124 0 0 25 0 1 0 1843516564 69165056 16427 4294967295 134512640 135094434 3221224448 3221223104 134558007 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/5452/statm): 16886 16427 145 145 0 16741 0 [pid=5452] vsize: 67544 Current children cumulated CPU time (s) 418.56 Current children cumulated vsize (Kb) 69668 [startup+430.054 s] Raw data (loadavg): 1.00 1.00 0.97 2/57 5452 Raw data (/proc/5448/stat): 5448 (minisat+_script) S 5447 5448 31027 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843516560 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/5448/statm): 531 226 485 147 0 384 0 [pid=5448] vsize: 2124 Raw data (/proc/5452/stat): 5452 (minisat+_64-bit) R 5448 5448 31027 0 -1 0 16864 0 0 0 42728 126 0 0 25 0 1 0 1843516564 70131712 16665 4294967295 134512640 135094434 3221224448 3221223120 134556266 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/5452/statm): 17122 16665 145 145 0 16977 0 [pid=5452] vsize: 68488 Current children cumulated CPU time (s) 428.54 Current children cumulated vsize (Kb) 70612 [startup+440.055 s] Raw data (loadavg): 1.00 1.00 0.97 1/57 5452 Raw data (/proc/5448/stat): 5448 (minisat+_script) S 5447 5448 31027 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843516560 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/5448/statm): 531 226 485 147 0 384 0 [pid=5448] vsize: 2124 Raw data (/proc/5452/stat): 5452 (minisat+_64-bit) T 5448 5448 31027 0 -1 0 17119 0 0 0 43721 128 0 0 25 0 1 0 1843516564 71168000 16920 4294967295 134512640 135094434 3221224448 3221222812 134870330 0 0 5 16386 3222434794 0 0 17 0 0 0 Raw data (/proc/5452/statm): 17375 16920 145 145 0 17230 0 [pid=5452] vsize: 69500 Current children cumulated CPU time (s) 438.49 Current children cumulated vsize (Kb) 71624 [startup+450.057 s] Raw data (loadavg): 1.00 1.00 0.97 2/57 5452 Raw data (/proc/5448/stat): 5448 (minisat+_script) S 5447 5448 31027 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843516560 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/5448/statm): 531 226 485 147 0 384 0 [pid=5448] vsize: 2124 Raw data (/proc/5452/stat): 5452 (minisat+_64-bit) R 5448 5448 31027 0 -1 0 17355 0 0 0 44718 129 0 0 25 0 1 0 1843516564 72126464 17156 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/5452/statm): 17609 17156 145 145 0 17464 0 [pid=5452] vsize: 70436 Current children cumulated CPU time (s) 448.47 Current children cumulated vsize (Kb) 72560 [startup+460.059 s] Raw data (loadavg): 1.00 1.00 0.97 2/57 5452 Raw data (/proc/5448/stat): 5448 (minisat+_script) S 5447 5448 31027 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843516560 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/5448/statm): 531 226 485 147 0 384 0 [pid=5448] vsize: 2124 Raw data (/proc/5452/stat): 5452 (minisat+_64-bit) R 5448 5448 31027 0 -1 0 17620 0 0 0 45713 131 0 0 25 0 1 0 1843516564 73207808 17421 4294967295 134512640 135094434 3221224448 3221223104 134557988 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/5452/statm): 17873 17421 145 145 0 17728 0 [pid=5452] vsize: 71492 Current children cumulated CPU time (s) 458.44 Current children cumulated vsize (Kb) 73616 [startup+470.06 s] Raw data (loadavg): 1.00 1.00 0.97 2/57 5452 Raw data (/proc/5448/stat): 5448 (minisat+_script) S 5447 5448 31027 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843516560 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/5448/statm): 531 226 485 147 0 384 0 [pid=5448] vsize: 2124 Raw data (/proc/5452/stat): 5452 (minisat+_64-bit) R 5448 5448 31027 0 -1 0 17784 0 0 0 46710 133 0 0 25 0 1 0 1843516564 73883648 17585 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/5452/statm): 18038 17585 145 145 0 17893 0 [pid=5452] vsize: 72152 Current children cumulated CPU time (s) 468.43 Current children cumulated vsize (Kb) 74276 [startup+480.062 s] Raw data (loadavg): 1.00 1.00 0.97 2/57 5452 Raw data (/proc/5448/stat): 5448 (minisat+_script) S 5447 5448 31027 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843516560 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/5448/statm): 531 226 485 147 0 384 0 [pid=5448] vsize: 2124 Raw data (/proc/5452/stat): 5452 (minisat+_64-bit) R 5448 5448 31027 0 -1 0 17961 0 0 0 47706 134 0 0 25 0 1 0 1843516564 74596352 17762 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/5452/statm): 18212 17762 145 145 0 18067 0 [pid=5452] vsize: 72848 Current children cumulated CPU time (s) 478.4 Current children cumulated vsize (Kb) 74972 [startup+490.063 s] Raw data (loadavg): 1.00 1.00 0.97 2/57 5452 Raw data (/proc/5448/stat): 5448 (minisat+_script) S 5447 5448 31027 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843516560 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/5448/statm): 531 226 485 147 0 384 0 [pid=5448] vsize: 2124 Raw data (/proc/5452/stat): 5452 (minisat+_64-bit) R 5448 5448 31027 0 -1 0 18227 0 0 0 48700 136 0 0 25 0 1 0 1843516564 75677696 18028 4294967295 134512640 135094434 3221224448 3221223104 134558159 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/5452/statm): 18476 18028 145 145 0 18331 0 [pid=5452] vsize: 73904 Current children cumulated CPU time (s) 488.36 Current children cumulated vsize (Kb) 76028 [startup+500.065 s] Raw data (loadavg): 1.00 1.00 0.97 2/57 5452 Raw data (/proc/5448/stat): 5448 (minisat+_script) S 5447 5448 31027 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843516560 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/5448/statm): 531 226 485 147 0 384 0 [pid=5448] vsize: 2124 Raw data (/proc/5452/stat): 5452 (minisat+_64-bit) R 5448 5448 31027 0 -1 0 18584 0 0 0 49692 140 0 0 25 0 1 0 1843516564 77651968 18385 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/5452/statm): 18958 18385 145 145 0 18813 0 [pid=5452] vsize: 75832 Current children cumulated CPU time (s) 498.32 Current children cumulated vsize (Kb) 77956 [startup+510.066 s] Raw data (loadavg): 1.00 1.00 0.97 2/57 5452 Raw data (/proc/5448/stat): 5448 (minisat+_script) S 5447 5448 31027 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843516560 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/5448/statm): 531 226 485 147 0 384 0 [pid=5448] vsize: 2124 Raw data (/proc/5452/stat): 5452 (minisat+_64-bit) R 5448 5448 31027 0 -1 0 18855 0 0 0 50687 143 0 0 25 0 1 0 1843516564 78753792 18656 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/5452/statm): 19227 18656 145 145 0 19082 0 [pid=5452] vsize: 76908 Current children cumulated CPU time (s) 508.3 Current children cumulated vsize (Kb) 79032 [startup+520.067 s] Raw data (loadavg): 1.00 1.00 0.97 2/57 5452 Raw data (/proc/5448/stat): 5448 (minisat+_script) S 5447 5448 31027 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843516560 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/5448/statm): 531 226 485 147 0 384 0 [pid=5448] vsize: 2124 Raw data (/proc/5452/stat): 5452 (minisat+_64-bit) R 5448 5448 31027 0 -1 0 19151 0 0 0 51681 145 0 0 25 0 1 0 1843516564 79958016 18952 4294967295 134512640 135094434 3221224448 3221223104 134557860 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/5452/statm): 19521 18952 145 145 0 19376 0 [pid=5452] vsize: 78084 Current children cumulated CPU time (s) 518.26 Current children cumulated vsize (Kb) 80208 [startup+530.069 s] Raw data (loadavg): 1.00 1.00 0.97 2/57 5452 Raw data (/proc/5448/stat): 5448 (minisat+_script) S 5447 5448 31027 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843516560 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/5448/statm): 531 226 485 147 0 384 0 [pid=5448] vsize: 2124 Raw data (/proc/5452/stat): 5452 (minisat+_64-bit) R 5448 5448 31027 0 -1 0 19435 0 0 0 52675 148 0 0 25 0 1 0 1843516564 81108992 19236 4294967295 134512640 135094434 3221224448 3221223104 134557948 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/5452/statm): 19802 19236 145 145 0 19657 0 [pid=5452] vsize: 79208 Current children cumulated CPU time (s) 528.23 Current children cumulated vsize (Kb) 81332 [startup+540.069 s] Raw data (loadavg): 1.00 1.00 0.97 2/57 5452 Raw data (/proc/5448/stat): 5448 (minisat+_script) S 5447 5448 31027 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843516560 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/5448/statm): 531 226 485 147 0 384 0 [pid=5448] vsize: 2124 Raw data (/proc/5452/stat): 5452 (minisat+_64-bit) R 5448 5448 31027 0 -1 0 19725 0 0 0 53671 149 0 0 25 0 1 0 1843516564 82292736 19526 4294967295 134512640 135094434 3221224448 3221223104 134558181 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/5452/statm): 20091 19526 145 145 0 19946 0 [pid=5452] vsize: 80364 Current children cumulated CPU time (s) 538.2 Current children cumulated vsize (Kb) 82488 [startup+550.071 s] Raw data (loadavg): 1.00 1.00 0.97 2/57 5452 Raw data (/proc/5448/stat): 5448 (minisat+_script) S 5447 5448 31027 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843516560 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/5448/statm): 531 226 485 147 0 384 0 [pid=5448] vsize: 2124 Raw data (/proc/5452/stat): 5452 (minisat+_64-bit) R 5448 5448 31027 0 -1 0 19997 0 0 0 54665 152 0 0 25 0 1 0 1843516564 83406848 19798 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/5452/statm): 20363 19798 145 145 0 20218 0 [pid=5452] vsize: 81452 Current children cumulated CPU time (s) 548.17 Current children cumulated vsize (Kb) 83576 [startup+560.073 s] Raw data (loadavg): 1.00 1.00 0.97 2/57 5452 Raw data (/proc/5448/stat): 5448 (minisat+_script) S 5447 5448 31027 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843516560 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/5448/statm): 531 226 485 147 0 384 0 [pid=5448] vsize: 2124 Raw data (/proc/5452/stat): 5452 (minisat+_64-bit) R 5448 5448 31027 0 -1 0 20186 0 0 0 55662 153 0 0 25 0 1 0 1843516564 84180992 19987 4294967295 134512640 135094434 3221224448 3221223040 134557287 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/5452/statm): 20552 19987 145 145 0 20407 0 [pid=5452] vsize: 82208 Current children cumulated CPU time (s) 558.15 Current children cumulated vsize (Kb) 84332 [startup+570.074 s] Raw data (loadavg): 1.00 1.00 0.97 2/57 5452 Raw data (/proc/5448/stat): 5448 (minisat+_script) S 5447 5448 31027 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843516560 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/5448/statm): 531 226 485 147 0 384 0 [pid=5448] vsize: 2124 Raw data (/proc/5452/stat): 5452 (minisat+_64-bit) R 5448 5448 31027 0 -1 0 20327 0 0 0 56659 154 0 0 25 0 1 0 1843516564 84754432 20128 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/5452/statm): 20692 20128 145 145 0 20547 0 [pid=5452] vsize: 82768 Current children cumulated CPU time (s) 568.13 Current children cumulated vsize (Kb) 84892 [startup+580.076 s] Raw data (loadavg): 1.00 1.00 0.97 2/57 5452 Raw data (/proc/5448/stat): 5448 (minisat+_script) S 5447 5448 31027 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843516560 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/5448/statm): 531 226 485 147 0 384 0 [pid=5448] vsize: 2124 Raw data (/proc/5452/stat): 5452 (minisat+_64-bit) R 5448 5448 31027 0 -1 0 20523 0 0 0 57654 157 0 0 25 0 1 0 1843516564 85557248 20324 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/5452/statm): 20888 20324 145 145 0 20743 0 [pid=5452] vsize: 83552 Current children cumulated CPU time (s) 578.11 Current children cumulated vsize (Kb) 85676 [startup+590.077 s] Raw data (loadavg): 1.00 1.00 0.97 2/57 5452 Raw data (/proc/5448/stat): 5448 (minisat+_script) S 5447 5448 31027 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843516560 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/5448/statm): 531 226 485 147 0 384 0 [pid=5448] vsize: 2124 Raw data (/proc/5452/stat): 5452 (minisat+_64-bit) R 5448 5448 31027 0 -1 0 20732 0 0 0 58650 159 0 0 25 0 1 0 1843516564 86417408 20533 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/5452/statm): 21098 20533 145 145 0 20953 0 [pid=5452] vsize: 84392 Current children cumulated CPU time (s) 588.09 Current children cumulated vsize (Kb) 86516 [startup+600.079 s] Raw data (loadavg): 1.00 1.00 0.97 2/57 5452 Raw data (/proc/5448/stat): 5448 (minisat+_script) S 5447 5448 31027 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843516560 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/5448/statm): 531 226 485 147 0 384 0 [pid=5448] vsize: 2124 Raw data (/proc/5452/stat): 5452 (minisat+_64-bit) R 5448 5448 31027 0 -1 0 20926 0 0 0 59646 160 0 0 25 0 1 0 1843516564 87203840 20727 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/5452/statm): 21290 20727 145 145 0 21145 0 [pid=5452] vsize: 85160 Current children cumulated CPU time (s) 598.06 Current children cumulated vsize (Kb) 87284 [startup+610.08 s] Raw data (loadavg): 1.00 1.00 0.97 2/57 5452 Raw data (/proc/5448/stat): 5448 (minisat+_script) S 5447 5448 31027 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843516560 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/5448/statm): 531 226 485 147 0 384 0 [pid=5448] vsize: 2124 Raw data (/proc/5452/stat): 5452 (minisat+_64-bit) R 5448 5448 31027 0 -1 0 21132 0 0 0 60642 162 0 0 25 0 1 0 1843516564 88039424 20933 4294967295 134512640 135094434 3221224448 3221223120 134556242 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/5452/statm): 21494 20933 145 145 0 21349 0 [pid=5452] vsize: 85976 Current children cumulated CPU time (s) 608.04 Current children cumulated vsize (Kb) 88100 [startup+620.081 s] Raw data (loadavg): 1.00 1.00 0.97 2/57 5452 Raw data (/proc/5448/stat): 5448 (minisat+_script) S 5447 5448 31027 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843516560 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/5448/statm): 531 226 485 147 0 384 0 [pid=5448] vsize: 2124 Raw data (/proc/5452/stat): 5452 (minisat+_64-bit) R 5448 5448 31027 0 -1 0 21343 0 0 0 61638 164 0 0 25 0 1 0 1843516564 88899584 21144 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/5452/statm): 21704 21144 145 145 0 21559 0 [pid=5452] vsize: 86816 Current children cumulated CPU time (s) 618.02 Current children cumulated vsize (Kb) 88940 [startup+630.082 s] Raw data (loadavg): 1.00 1.00 0.97 2/57 5452 Raw data (/proc/5448/stat): 5448 (minisat+_script) S 5447 5448 31027 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843516560 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/5448/statm): 531 226 485 147 0 384 0 [pid=5448] vsize: 2124 Raw data (/proc/5452/stat): 5452 (minisat+_64-bit) R 5448 5448 31027 0 -1 0 21551 0 0 0 62634 166 0 0 25 0 1 0 1843516564 89735168 21352 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/5452/statm): 21908 21352 145 145 0 21763 0 [pid=5452] vsize: 87632 Current children cumulated CPU time (s) 628 Current children cumulated vsize (Kb) 89756 [startup+640.083 s] Raw data (loadavg): 1.00 1.00 0.97 2/57 5452 Raw data (/proc/5448/stat): 5448 (minisat+_script) S 5447 5448 31027 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843516560 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/5448/statm): 531 226 485 147 0 384 0 [pid=5448] vsize: 2124 Raw data (/proc/5452/stat): 5452 (minisat+_64-bit) R 5448 5448 31027 0 -1 0 21772 0 0 0 63628 169 0 0 25 0 1 0 1843516564 90632192 21573 4294967295 134512640 135094434 3221224448 3221223104 134558159 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/5452/statm): 22127 21573 145 145 0 21982 0 [pid=5452] vsize: 88508 Current children cumulated CPU time (s) 637.97 Current children cumulated vsize (Kb) 90632 [startup+650.085 s] Raw data (loadavg): 1.00 1.00 0.97 2/57 5452 Raw data (/proc/5448/stat): 5448 (minisat+_script) S 5447 5448 31027 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843516560 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/5448/statm): 531 226 485 147 0 384 0 [pid=5448] vsize: 2124 Raw data (/proc/5452/stat): 5452 (minisat+_64-bit) R 5448 5448 31027 0 -1 0 22061 0 0 0 64625 171 0 0 25 0 1 0 1843516564 91811840 21862 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/5452/statm): 22415 21862 145 145 0 22270 0 [pid=5452] vsize: 89660 Current children cumulated CPU time (s) 647.96 Current children cumulated vsize (Kb) 91784 [startup+660.086 s] Raw data (loadavg): 1.00 1.00 0.97 2/57 5452 Raw data (/proc/5448/stat): 5448 (minisat+_script) S 5447 5448 31027 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843516560 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/5448/statm): 531 226 485 147 0 384 0 [pid=5448] vsize: 2124 Raw data (/proc/5452/stat): 5452 (minisat+_64-bit) R 5448 5448 31027 0 -1 0 22316 0 0 0 65619 174 0 0 25 0 1 0 1843516564 92848128 22117 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/5452/statm): 22668 22117 145 145 0 22523 0 [pid=5452] vsize: 90672 Current children cumulated CPU time (s) 657.93 Current children cumulated vsize (Kb) 92796 [startup+670.087 s] Raw data (loadavg): 1.00 1.00 0.97 2/57 5452 Raw data (/proc/5448/stat): 5448 (minisat+_script) S 5447 5448 31027 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843516560 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/5448/statm): 531 226 485 147 0 384 0 [pid=5448] vsize: 2124 Raw data (/proc/5452/stat): 5452 (minisat+_64-bit) R 5448 5448 31027 0 -1 0 22533 0 0 0 66616 175 0 0 25 0 1 0 1843516564 93732864 22334 4294967295 134512640 135094434 3221224448 3221222480 134562780 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/5452/statm): 22884 22334 145 145 0 22739 0 [pid=5452] vsize: 91536 Current children cumulated CPU time (s) 667.91 Current children cumulated vsize (Kb) 93660 [startup+680.088 s] Raw data (loadavg): 1.00 1.00 0.97 2/57 5452 Raw data (/proc/5448/stat): 5448 (minisat+_script) S 5447 5448 31027 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843516560 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/5448/statm): 531 226 485 147 0 384 0 [pid=5448] vsize: 2124 Raw data (/proc/5452/stat): 5452 (minisat+_64-bit) R 5448 5448 31027 0 -1 0 22533 0 0 0 67617 175 0 0 25 0 1 0 1843516564 93732864 22334 4294967295 134512640 135094434 3221224448 3221223088 134562104 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/5452/statm): 22884 22334 145 145 0 22739 0 [pid=5452] vsize: 91536 Current children cumulated CPU time (s) 677.92 Current children cumulated vsize (Kb) 93660 [startup+690.089 s] Raw data (loadavg): 1.00 1.00 0.97 2/57 5452 Raw data (/proc/5448/stat): 5448 (minisat+_script) S 5447 5448 31027 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843516560 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/5448/statm): 531 226 485 147 0 384 0 [pid=5448] vsize: 2124 Raw data (/proc/5452/stat): 5452 (minisat+_64-bit) R 5448 5448 31027 0 -1 0 22533 0 0 0 68617 175 0 0 25 0 1 0 1843516564 93732864 22334 4294967295 134512640 135094434 3221224448 3221223120 134556266 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/5452/statm): 22884 22334 145 145 0 22739 0 [pid=5452] vsize: 91536 Current children cumulated CPU time (s) 687.92 Current children cumulated vsize (Kb) 93660 [startup+700.09 s] Raw data (loadavg): 1.00 1.00 0.97 2/57 5452 Raw data (/proc/5448/stat): 5448 (minisat+_script) S 5447 5448 31027 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843516560 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/5448/statm): 531 226 485 147 0 384 0 [pid=5448] vsize: 2124 Raw data (/proc/5452/stat): 5452 (minisat+_64-bit) R 5448 5448 31027 0 -1 0 22533 0 0 0 69617 175 0 0 25 0 1 0 1843516564 93732864 22334 4294967295 134512640 135094434 3221224448 3221223040 134557202 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/5452/statm): 22884 22334 145 145 0 22739 0 [pid=5452] vsize: 91536 Current children cumulated CPU time (s) 697.92 Current children cumulated vsize (Kb) 93660 [startup+710.091 s] Raw data (loadavg): 1.00 1.00 0.97 2/57 5452 Raw data (/proc/5448/stat): 5448 (minisat+_script) S 5447 5448 31027 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843516560 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/5448/statm): 531 226 485 147 0 384 0 [pid=5448] vsize: 2124 Raw data (/proc/5452/stat): 5452 (minisat+_64-bit) R 5448 5448 31027 0 -1 0 22533 0 0 0 70617 175 0 0 25 0 1 0 1843516564 93732864 22334 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/5452/statm): 22884 22334 145 145 0 22739 0 [pid=5452] vsize: 91536 Current children cumulated CPU time (s) 707.92 Current children cumulated vsize (Kb) 93660 [startup+720.092 s] Raw data (loadavg): 1.00 1.00 0.97 2/57 5452 Raw data (/proc/5448/stat): 5448 (minisat+_script) S 5447 5448 31027 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843516560 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/5448/statm): 531 226 485 147 0 384 0 [pid=5448] vsize: 2124 Raw data (/proc/5452/stat): 5452 (minisat+_64-bit) R 5448 5448 31027 0 -1 0 22533 0 0 0 71618 175 0 0 25 0 1 0 1843516564 93732864 22334 4294967295 134512640 135094434 3221224448 3221223104 134558246 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/5452/statm): 22884 22334 145 145 0 22739 0 [pid=5452] vsize: 91536 Current children cumulated CPU time (s) 717.93 Current children cumulated vsize (Kb) 93660 [startup+730.093 s] Raw data (loadavg): 1.00 1.00 0.97 2/57 5452 Raw data (/proc/5448/stat): 5448 (minisat+_script) S 5447 5448 31027 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843516560 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/5448/statm): 531 226 485 147 0 384 0 [pid=5448] vsize: 2124 Raw data (/proc/5452/stat): 5452 (minisat+_64-bit) R 5448 5448 31027 0 -1 0 22533 0 0 0 72618 175 0 0 25 0 1 0 1843516564 93732864 22334 4294967295 134512640 135094434 3221224448 3221223072 134562104 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/5452/statm): 22884 22334 145 145 0 22739 0 [pid=5452] vsize: 91536 Current children cumulated CPU time (s) 727.93 Current children cumulated vsize (Kb) 93660 [startup+740.094 s] Raw data (loadavg): 1.00 1.00 0.97 2/57 5452 Raw data (/proc/5448/stat): 5448 (minisat+_script) S 5447 5448 31027 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843516560 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/5448/statm): 531 226 485 147 0 384 0 [pid=5448] vsize: 2124 Raw data (/proc/5452/stat): 5452 (minisat+_64-bit) R 5448 5448 31027 0 -1 0 22533 0 0 0 73618 175 0 0 25 0 1 0 1843516564 93732864 22334 4294967295 134512640 135094434 3221224448 3221223040 134557180 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/5452/statm): 22884 22334 145 145 0 22739 0 [pid=5452] vsize: 91536 Current children cumulated CPU time (s) 737.93 Current children cumulated vsize (Kb) 93660 [startup+750.095 s] Raw data (loadavg): 1.00 1.00 0.97 2/57 5452 Raw data (/proc/5448/stat): 5448 (minisat+_script) S 5447 5448 31027 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843516560 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/5448/statm): 531 226 485 147 0 384 0 [pid=5448] vsize: 2124 Raw data (/proc/5452/stat): 5452 (minisat+_64-bit) R 5448 5448 31027 0 -1 0 22533 0 0 0 74618 175 0 0 25 0 1 0 1843516564 93732864 22334 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/5452/statm): 22884 22334 145 145 0 22739 0 [pid=5452] vsize: 91536 Current children cumulated CPU time (s) 747.93 Current children cumulated vsize (Kb) 93660 [startup+760.096 s] Raw data (loadavg): 1.00 1.00 0.97 2/57 5452 Raw data (/proc/5448/stat): 5448 (minisat+_script) S 5447 5448 31027 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843516560 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/5448/statm): 531 226 485 147 0 384 0 [pid=5448] vsize: 2124 Raw data (/proc/5452/stat): 5452 (minisat+_64-bit) R 5448 5448 31027 0 -1 0 22533 0 0 0 75617 176 0 0 25 0 1 0 1843516564 93732864 22334 4294967295 134512640 135094434 3221224448 3221223120 134555853 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/5452/statm): 22884 22334 145 145 0 22739 0 [pid=5452] vsize: 91536 Current children cumulated CPU time (s) 757.93 Current children cumulated vsize (Kb) 93660 [startup+770.097 s] Raw data (loadavg): 1.00 1.00 0.97 2/57 5452 Raw data (/proc/5448/stat): 5448 (minisat+_script) S 5447 5448 31027 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843516560 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/5448/statm): 531 226 485 147 0 384 0 [pid=5448] vsize: 2124 Raw data (/proc/5452/stat): 5452 (minisat+_64-bit) R 5448 5448 31027 0 -1 0 22533 0 0 0 76617 176 0 0 25 0 1 0 1843516564 93732864 22334 4294967295 134512640 135094434 3221224448 3221223104 134557948 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/5452/statm): 22884 22334 145 145 0 22739 0 [pid=5452] vsize: 91536 Current children cumulated CPU time (s) 767.93 Current children cumulated vsize (Kb) 93660 [startup+780.099 s] Raw data (loadavg): 1.00 1.00 0.97 2/57 5452 Raw data (/proc/5448/stat): 5448 (minisat+_script) S 5447 5448 31027 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843516560 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/5448/statm): 531 226 485 147 0 384 0 [pid=5448] vsize: 2124 Raw data (/proc/5452/stat): 5452 (minisat+_64-bit) R 5448 5448 31027 0 -1 0 22533 0 0 0 77617 176 0 0 25 0 1 0 1843516564 93732864 22334 4294967295 134512640 135094434 3221224448 3221223136 134554793 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/5452/statm): 22884 22334 145 145 0 22739 0 [pid=5452] vsize: 91536 Current children cumulated CPU time (s) 777.93 Current children cumulated vsize (Kb) 93660 [startup+790.1 s] Raw data (loadavg): 1.00 1.00 0.97 2/57 5452 Raw data (/proc/5448/stat): 5448 (minisat+_script) S 5447 5448 31027 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843516560 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/5448/statm): 531 226 485 147 0 384 0 [pid=5448] vsize: 2124 Raw data (/proc/5452/stat): 5452 (minisat+_64-bit) R 5448 5448 31027 0 -1 0 22533 0 0 0 78616 177 0 0 25 0 1 0 1843516564 93732864 22334 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/5452/statm): 22884 22334 145 145 0 22739 0 [pid=5452] vsize: 91536 Current children cumulated CPU time (s) 787.93 Current children cumulated vsize (Kb) 93660 [startup+800.101 s] Raw data (loadavg): 1.00 1.00 0.97 2/57 5452 Raw data (/proc/5448/stat): 5448 (minisat+_script) S 5447 5448 31027 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843516560 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/5448/statm): 531 226 485 147 0 384 0 [pid=5448] vsize: 2124 Raw data (/proc/5452/stat): 5452 (minisat+_64-bit) R 5448 5448 31027 0 -1 0 22533 0 0 0 79616 177 0 0 25 0 1 0 1843516564 93732864 22334 4294967295 134512640 135094434 3221224448 3221223104 134557903 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/5452/statm): 22884 22334 145 145 0 22739 0 [pid=5452] vsize: 91536 Current children cumulated CPU time (s) 797.93 Current children cumulated vsize (Kb) 93660 [startup+810.103 s] Raw data (loadavg): 1.00 1.00 0.97 2/57 5452 Raw data (/proc/5448/stat): 5448 (minisat+_script) S 5447 5448 31027 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843516560 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/5448/statm): 531 226 485 147 0 384 0 [pid=5448] vsize: 2124 Raw data (/proc/5452/stat): 5452 (minisat+_64-bit) R 5448 5448 31027 0 -1 0 22533 0 0 0 80615 177 0 0 25 0 1 0 1843516564 93732864 22334 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/5452/statm): 22884 22334 145 145 0 22739 0 [pid=5452] vsize: 91536 Current children cumulated CPU time (s) 807.92 Current children cumulated vsize (Kb) 93660 [startup+820.104 s] Raw data (loadavg): 1.00 1.00 0.97 2/57 5452 Raw data (/proc/5448/stat): 5448 (minisat+_script) S 5447 5448 31027 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843516560 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/5448/statm): 531 226 485 147 0 384 0 [pid=5448] vsize: 2124 Raw data (/proc/5452/stat): 5452 (minisat+_64-bit) R 5448 5448 31027 0 -1 0 22533 0 0 0 81615 178 0 0 25 0 1 0 1843516564 93732864 22334 4294967295 134512640 135094434 3221224448 3221223136 134554731 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/5452/statm): 22884 22334 145 145 0 22739 0 [pid=5452] vsize: 91536 Current children cumulated CPU time (s) 817.93 Current children cumulated vsize (Kb) 93660 [startup+830.106 s] Raw data (loadavg): 1.00 1.00 0.97 2/57 5452 Raw data (/proc/5448/stat): 5448 (minisat+_script) S 5447 5448 31027 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843516560 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/5448/statm): 531 226 485 147 0 384 0 [pid=5448] vsize: 2124 Raw data (/proc/5452/stat): 5452 (minisat+_64-bit) R 5448 5448 31027 0 -1 0 22533 0 0 0 82615 178 0 0 25 0 1 0 1843516564 93732864 22334 4294967295 134512640 135094434 3221224448 3221223104 134558162 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/5452/statm): 22884 22334 145 145 0 22739 0 [pid=5452] vsize: 91536 Current children cumulated CPU time (s) 827.93 Current children cumulated vsize (Kb) 93660 [startup+840.108 s] Raw data (loadavg): 1.00 1.00 0.97 2/57 5452 Raw data (/proc/5448/stat): 5448 (minisat+_script) S 5447 5448 31027 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843516560 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/5448/statm): 531 226 485 147 0 384 0 [pid=5448] vsize: 2124 Raw data (/proc/5452/stat): 5452 (minisat+_64-bit) R 5448 5448 31027 0 -1 0 22533 0 0 0 83614 179 0 0 25 0 1 0 1843516564 93732864 22334 4294967295 134512640 135094434 3221224448 3221223104 134558187 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/5452/statm): 22884 22334 145 145 0 22739 0 [pid=5452] vsize: 91536 Current children cumulated CPU time (s) 837.93 Current children cumulated vsize (Kb) 93660 [startup+850.11 s] Raw data (loadavg): 1.00 1.00 0.97 2/57 5452 Raw data (/proc/5448/stat): 5448 (minisat+_script) S 5447 5448 31027 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843516560 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/5448/statm): 531 226 485 147 0 384 0 [pid=5448] vsize: 2124 Raw data (/proc/5452/stat): 5452 (minisat+_64-bit) R 5448 5448 31027 0 -1 0 22533 0 0 0 84614 179 0 0 25 0 1 0 1843516564 93732864 22334 4294967295 134512640 135094434 3221224448 3221223104 134558159 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/5452/statm): 22884 22334 145 145 0 22739 0 [pid=5452] vsize: 91536 Current children cumulated CPU time (s) 847.93 Current children cumulated vsize (Kb) 93660 [startup+860.111 s] Raw data (loadavg): 1.00 1.00 0.97 2/57 5452 Raw data (/proc/5448/stat): 5448 (minisat+_script) S 5447 5448 31027 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843516560 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/5448/statm): 531 226 485 147 0 384 0 [pid=5448] vsize: 2124 Raw data (/proc/5452/stat): 5452 (minisat+_64-bit) R 5448 5448 31027 0 -1 0 22533 0 0 0 85614 179 0 0 25 0 1 0 1843516564 93732864 22334 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/5452/statm): 22884 22334 145 145 0 22739 0 [pid=5452] vsize: 91536 Current children cumulated CPU time (s) 857.93 Current children cumulated vsize (Kb) 93660 [startup+870.112 s] Raw data (loadavg): 1.00 1.00 0.97 2/57 5452 Raw data (/proc/5448/stat): 5448 (minisat+_script) S 5447 5448 31027 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843516560 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/5448/statm): 531 226 485 147 0 384 0 [pid=5448] vsize: 2124 Raw data (/proc/5452/stat): 5452 (minisat+_64-bit) R 5448 5448 31027 0 -1 0 22533 0 0 0 86613 179 0 0 25 0 1 0 1843516564 93732864 22334 4294967295 134512640 135094434 3221224448 3221223104 134558159 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/5452/statm): 22884 22334 145 145 0 22739 0 [pid=5452] vsize: 91536 Current children cumulated CPU time (s) 867.92 Current children cumulated vsize (Kb) 93660 [startup+880.114 s] Raw data (loadavg): 1.00 1.00 0.97 2/57 5452 Raw data (/proc/5448/stat): 5448 (minisat+_script) S 5447 5448 31027 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843516560 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/5448/statm): 531 226 485 147 0 384 0 [pid=5448] vsize: 2124 Raw data (/proc/5452/stat): 5452 (minisat+_64-bit) R 5448 5448 31027 0 -1 0 22533 0 0 0 87613 180 0 0 25 0 1 0 1843516564 93732864 22334 4294967295 134512640 135094434 3221224448 3221223072 134557696 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/5452/statm): 22884 22334 145 145 0 22739 0 [pid=5452] vsize: 91536 Current children cumulated CPU time (s) 877.93 Current children cumulated vsize (Kb) 93660 [startup+890.115 s] Raw data (loadavg): 1.00 1.00 0.97 2/57 5452 Raw data (/proc/5448/stat): 5448 (minisat+_script) S 5447 5448 31027 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843516560 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/5448/statm): 531 226 485 147 0 384 0 [pid=5448] vsize: 2124 Raw data (/proc/5452/stat): 5452 (minisat+_64-bit) R 5448 5448 31027 0 -1 0 22533 0 0 0 88613 180 0 0 25 0 1 0 1843516564 93732864 22334 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/5452/statm): 22884 22334 145 145 0 22739 0 [pid=5452] vsize: 91536 Current children cumulated CPU time (s) 887.93 Current children cumulated vsize (Kb) 93660 [startup+900.117 s] Raw data (loadavg): 1.00 1.00 0.97 2/57 5452 Raw data (/proc/5448/stat): 5448 (minisat+_script) S 5447 5448 31027 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843516560 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/5448/statm): 531 226 485 147 0 384 0 [pid=5448] vsize: 2124 Raw data (/proc/5452/stat): 5452 (minisat+_64-bit) R 5448 5448 31027 0 -1 0 22533 0 0 0 89612 181 0 0 25 0 1 0 1843516564 93732864 22334 4294967295 134512640 135094434 3221224448 3221223104 134558007 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/5452/statm): 22884 22334 145 145 0 22739 0 [pid=5452] vsize: 91536 Current children cumulated CPU time (s) 897.93 Current children cumulated vsize (Kb) 93660 [startup+910.118 s] Raw data (loadavg): 1.00 1.00 0.97 2/57 5452 Raw data (/proc/5448/stat): 5448 (minisat+_script) S 5447 5448 31027 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843516560 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/5448/statm): 531 226 485 147 0 384 0 [pid=5448] vsize: 2124 Raw data (/proc/5452/stat): 5452 (minisat+_64-bit) R 5448 5448 31027 0 -1 0 22533 0 0 0 90612 181 0 0 25 0 1 0 1843516564 93732864 22334 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/5452/statm): 22884 22334 145 145 0 22739 0 [pid=5452] vsize: 91536 Current children cumulated CPU time (s) 907.93 Current children cumulated vsize (Kb) 93660 [startup+920.119 s] Raw data (loadavg): 1.00 1.00 0.97 2/57 5452 Raw data (/proc/5448/stat): 5448 (minisat+_script) S 5447 5448 31027 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843516560 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/5448/statm): 531 226 485 147 0 384 0 [pid=5448] vsize: 2124 Raw data (/proc/5452/stat): 5452 (minisat+_64-bit) R 5448 5448 31027 0 -1 0 22533 0 0 0 91612 181 0 0 25 0 1 0 1843516564 93732864 22334 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/5452/statm): 22884 22334 145 145 0 22739 0 [pid=5452] vsize: 91536 Current children cumulated CPU time (s) 917.93 Current children cumulated vsize (Kb) 93660 [startup+930.12 s] Raw data (loadavg): 1.00 1.00 0.97 2/57 5452 Raw data (/proc/5448/stat): 5448 (minisat+_script) S 5447 5448 31027 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843516560 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/5448/statm): 531 226 485 147 0 384 0 [pid=5448] vsize: 2124 Raw data (/proc/5452/stat): 5452 (minisat+_64-bit) R 5448 5448 31027 0 -1 0 22533 0 0 0 92611 182 0 0 25 0 1 0 1843516564 93732864 22334 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/5452/statm): 22884 22334 145 145 0 22739 0 [pid=5452] vsize: 91536 Current children cumulated CPU time (s) 927.93 Current children cumulated vsize (Kb) 93660 [startup+940.121 s] Raw data (loadavg): 1.00 1.00 0.97 2/57 5452 Raw data (/proc/5448/stat): 5448 (minisat+_script) S 5447 5448 31027 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843516560 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/5448/statm): 531 226 485 147 0 384 0 [pid=5448] vsize: 2124 Raw data (/proc/5452/stat): 5452 (minisat+_64-bit) R 5448 5448 31027 0 -1 0 22533 0 0 0 93611 182 0 0 25 0 1 0 1843516564 93732864 22334 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/5452/statm): 22884 22334 145 145 0 22739 0 [pid=5452] vsize: 91536 Current children cumulated CPU time (s) 937.93 Current children cumulated vsize (Kb) 93660 [startup+950.123 s] Raw data (loadavg): 1.00 1.00 0.97 2/57 5452 Raw data (/proc/5448/stat): 5448 (minisat+_script) S 5447 5448 31027 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843516560 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/5448/statm): 531 226 485 147 0 384 0 [pid=5448] vsize: 2124 Raw data (/proc/5452/stat): 5452 (minisat+_64-bit) R 5448 5448 31027 0 -1 0 22533 0 0 0 94611 182 0 0 25 0 1 0 1843516564 93732864 22334 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/5452/statm): 22884 22334 145 145 0 22739 0 [pid=5452] vsize: 91536 Current children cumulated CPU time (s) 947.93 Current children cumulated vsize (Kb) 93660 [startup+960.125 s] Raw data (loadavg): 1.00 1.00 0.97 2/57 5452 Raw data (/proc/5448/stat): 5448 (minisat+_script) S 5447 5448 31027 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843516560 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/5448/statm): 531 226 485 147 0 384 0 [pid=5448] vsize: 2124 Raw data (/proc/5452/stat): 5452 (minisat+_64-bit) R 5448 5448 31027 0 -1 0 22533 0 0 0 95610 183 0 0 25 0 1 0 1843516564 93732864 22334 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/5452/statm): 22884 22334 145 145 0 22739 0 [pid=5452] vsize: 91536 Current children cumulated CPU time (s) 957.93 Current children cumulated vsize (Kb) 93660 [startup+970.126 s] Raw data (loadavg): 1.00 1.00 0.97 2/57 5452 Raw data (/proc/5448/stat): 5448 (minisat+_script) S 5447 5448 31027 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843516560 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/5448/statm): 531 226 485 147 0 384 0 [pid=5448] vsize: 2124 Raw data (/proc/5452/stat): 5452 (minisat+_64-bit) R 5448 5448 31027 0 -1 0 22533 0 0 0 96610 183 0 0 25 0 1 0 1843516564 93732864 22334 4294967295 134512640 135094434 3221224448 3221223072 134557685 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/5452/statm): 22884 22334 145 145 0 22739 0 [pid=5452] vsize: 91536 Current children cumulated CPU time (s) 967.93 Current children cumulated vsize (Kb) 93660 [startup+980.128 s] Raw data (loadavg): 1.00 1.00 0.97 2/57 5452 Raw data (/proc/5448/stat): 5448 (minisat+_script) S 5447 5448 31027 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843516560 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/5448/statm): 531 226 485 147 0 384 0 [pid=5448] vsize: 2124 Raw data (/proc/5452/stat): 5452 (minisat+_64-bit) R 5448 5448 31027 0 -1 0 22533 0 0 0 97609 183 0 0 25 0 1 0 1843516564 93732864 22334 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/5452/statm): 22884 22334 145 145 0 22739 0 [pid=5452] vsize: 91536 Current children cumulated CPU time (s) 977.92 Current children cumulated vsize (Kb) 93660 [startup+990.129 s] Raw data (loadavg): 1.00 1.00 0.97 2/57 5452 Raw data (/proc/5448/stat): 5448 (minisat+_script) S 5447 5448 31027 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843516560 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/5448/statm): 531 226 485 147 0 384 0 [pid=5448] vsize: 2124 Raw data (/proc/5452/stat): 5452 (minisat+_64-bit) R 5448 5448 31027 0 -1 0 22533 0 0 0 98609 184 0 0 25 0 1 0 1843516564 93732864 22334 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/5452/statm): 22884 22334 145 145 0 22739 0 [pid=5452] vsize: 91536 Current children cumulated CPU time (s) 987.93 Current children cumulated vsize (Kb) 93660 [startup+1000.13 s] Raw data (loadavg): 1.00 1.00 0.97 2/57 5452 Raw data (/proc/5448/stat): 5448 (minisat+_script) S 5447 5448 31027 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843516560 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/5448/statm): 531 226 485 147 0 384 0 [pid=5448] vsize: 2124 Raw data (/proc/5452/stat): 5452 (minisat+_64-bit) R 5448 5448 31027 0 -1 0 22533 0 0 0 99608 184 0 0 25 0 1 0 1843516564 93732864 22334 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/5452/statm): 22884 22334 145 145 0 22739 0 [pid=5452] vsize: 91536 Current children cumulated CPU time (s) 997.92 Current children cumulated vsize (Kb) 93660 [startup+1010.13 s] Raw data (loadavg): 1.00 1.00 0.97 2/57 5452 Raw data (/proc/5448/stat): 5448 (minisat+_script) S 5447 5448 31027 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843516560 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/5448/statm): 531 226 485 147 0 384 0 [pid=5448] vsize: 2124 Raw data (/proc/5452/stat): 5452 (minisat+_64-bit) R 5448 5448 31027 0 -1 0 22533 0 0 0 100608 184 0 0 25 0 1 0 1843516564 93732864 22334 4294967295 134512640 135094434 3221224448 3221223040 134556802 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/5452/statm): 22884 22334 145 145 0 22739 0 [pid=5452] vsize: 91536 Current children cumulated CPU time (s) 1007.92 Current children cumulated vsize (Kb) 93660 [startup+1020.13 s] Raw data (loadavg): 1.00 1.00 0.97 2/57 5452 Raw data (/proc/5448/stat): 5448 (minisat+_script) S 5447 5448 31027 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843516560 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/5448/statm): 531 226 485 147 0 384 0 [pid=5448] vsize: 2124 Raw data (/proc/5452/stat): 5452 (minisat+_64-bit) R 5448 5448 31027 0 -1 0 22533 0 0 0 101608 185 0 0 25 0 1 0 1843516564 93732864 22334 4294967295 134512640 135094434 3221224448 3221223072 134557585 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/5452/statm): 22884 22334 145 145 0 22739 0 [pid=5452] vsize: 91536 Current children cumulated CPU time (s) 1017.93 Current children cumulated vsize (Kb) 93660 [startup+1030.13 s] Raw data (loadavg): 1.00 1.00 0.97 2/57 5452 Raw data (/proc/5448/stat): 5448 (minisat+_script) S 5447 5448 31027 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843516560 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/5448/statm): 531 226 485 147 0 384 0 [pid=5448] vsize: 2124 Raw data (/proc/5452/stat): 5452 (minisat+_64-bit) R 5448 5448 31027 0 -1 0 22533 0 0 0 102608 185 0 0 25 0 1 0 1843516564 93732864 22334 4294967295 134512640 135094434 3221224448 3221223104 134558210 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/5452/statm): 22884 22334 145 145 0 22739 0 [pid=5452] vsize: 91536 Current children cumulated CPU time (s) 1027.93 Current children cumulated vsize (Kb) 93660 [startup+1040.13 s] Raw data (loadavg): 1.00 1.00 0.97 2/57 5452 Raw data (/proc/5448/stat): 5448 (minisat+_script) S 5447 5448 31027 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843516560 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/5448/statm): 531 226 485 147 0 384 0 [pid=5448] vsize: 2124 Raw data (/proc/5452/stat): 5452 (minisat+_64-bit) R 5448 5448 31027 0 -1 0 22533 0 0 0 103608 185 0 0 25 0 1 0 1843516564 93732864 22334 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/5452/statm): 22884 22334 145 145 0 22739 0 [pid=5452] vsize: 91536 Current children cumulated CPU time (s) 1037.93 Current children cumulated vsize (Kb) 93660 [startup+1050.14 s] Raw data (loadavg): 1.00 1.00 0.97 2/57 5452 Raw data (/proc/5448/stat): 5448 (minisat+_script) S 5447 5448 31027 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843516560 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/5448/statm): 531 226 485 147 0 384 0 [pid=5448] vsize: 2124 Raw data (/proc/5452/stat): 5452 (minisat+_64-bit) R 5448 5448 31027 0 -1 0 22533 0 0 0 104607 186 0 0 25 0 1 0 1843516564 93732864 22334 4294967295 134512640 135094434 3221224448 3221223104 134558249 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/5452/statm): 22884 22334 145 145 0 22739 0 [pid=5452] vsize: 91536 Current children cumulated CPU time (s) 1047.93 Current children cumulated vsize (Kb) 93660 [startup+1060.14 s] Raw data (loadavg): 1.00 1.00 0.97 2/57 5452 Raw data (/proc/5448/stat): 5448 (minisat+_script) S 5447 5448 31027 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843516560 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/5448/statm): 531 226 485 147 0 384 0 [pid=5448] vsize: 2124 Raw data (/proc/5452/stat): 5452 (minisat+_64-bit) R 5448 5448 31027 0 -1 0 22533 0 0 0 105607 186 0 0 25 0 1 0 1843516564 93732864 22334 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/5452/statm): 22884 22334 145 145 0 22739 0 [pid=5452] vsize: 91536 Current children cumulated CPU time (s) 1057.93 Current children cumulated vsize (Kb) 93660 [startup+1070.14 s] Raw data (loadavg): 1.00 1.00 0.97 2/57 5452 Raw data (/proc/5448/stat): 5448 (minisat+_script) S 5447 5448 31027 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843516560 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/5448/statm): 531 226 485 147 0 384 0 [pid=5448] vsize: 2124 Raw data (/proc/5452/stat): 5452 (minisat+_64-bit) R 5448 5448 31027 0 -1 0 22533 0 0 0 106606 187 0 0 25 0 1 0 1843516564 93732864 22334 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/5452/statm): 22884 22334 145 145 0 22739 0 [pid=5452] vsize: 91536 Current children cumulated CPU time (s) 1067.93 Current children cumulated vsize (Kb) 93660 [startup+1080.14 s] Raw data (loadavg): 1.00 1.00 0.97 2/57 5452 Raw data (/proc/5448/stat): 5448 (minisat+_script) S 5447 5448 31027 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843516560 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/5448/statm): 531 226 485 147 0 384 0 [pid=5448] vsize: 2124 Raw data (/proc/5452/stat): 5452 (minisat+_64-bit) R 5448 5448 31027 0 -1 0 22533 0 0 0 107606 187 0 0 25 0 1 0 1843516564 93732864 22334 4294967295 134512640 135094434 3221224448 3221223104 134557996 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/5452/statm): 22884 22334 145 145 0 22739 0 [pid=5452] vsize: 91536 Current children cumulated CPU time (s) 1077.93 Current children cumulated vsize (Kb) 93660 [startup+1090.14 s] Raw data (loadavg): 1.00 1.00 0.97 2/57 5452 Raw data (/proc/5448/stat): 5448 (minisat+_script) S 5447 5448 31027 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843516560 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/5448/statm): 531 226 485 147 0 384 0 [pid=5448] vsize: 2124 Raw data (/proc/5452/stat): 5452 (minisat+_64-bit) R 5448 5448 31027 0 -1 0 22533 0 0 0 108605 187 0 0 25 0 1 0 1843516564 93732864 22334 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/5452/statm): 22884 22334 145 145 0 22739 0 [pid=5452] vsize: 91536 Current children cumulated CPU time (s) 1087.92 Current children cumulated vsize (Kb) 93660 [startup+1100.14 s] Raw data (loadavg): 1.00 1.00 0.97 2/57 5452 Raw data (/proc/5448/stat): 5448 (minisat+_script) S 5447 5448 31027 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843516560 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/5448/statm): 531 226 485 147 0 384 0 [pid=5448] vsize: 2124 Raw data (/proc/5452/stat): 5452 (minisat+_64-bit) R 5448 5448 31027 0 -1 0 22533 0 0 0 109605 188 0 0 25 0 1 0 1843516564 93732864 22334 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/5452/statm): 22884 22334 145 145 0 22739 0 [pid=5452] vsize: 91536 Current children cumulated CPU time (s) 1097.93 Current children cumulated vsize (Kb) 93660 [startup+1110.14 s] Raw data (loadavg): 1.00 1.00 0.97 2/57 5452 Raw data (/proc/5448/stat): 5448 (minisat+_script) S 5447 5448 31027 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843516560 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/5448/statm): 531 226 485 147 0 384 0 [pid=5448] vsize: 2124 Raw data (/proc/5452/stat): 5452 (minisat+_64-bit) R 5448 5448 31027 0 -1 0 22533 0 0 0 110605 188 0 0 25 0 1 0 1843516564 93732864 22334 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/5452/statm): 22884 22334 145 145 0 22739 0 [pid=5452] vsize: 91536 Current children cumulated CPU time (s) 1107.93 Current children cumulated vsize (Kb) 93660 [startup+1120.14 s] Raw data (loadavg): 1.00 1.00 0.97 2/57 5452 Raw data (/proc/5448/stat): 5448 (minisat+_script) S 5447 5448 31027 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843516560 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/5448/statm): 531 226 485 147 0 384 0 [pid=5448] vsize: 2124 Raw data (/proc/5452/stat): 5452 (minisat+_64-bit) R 5448 5448 31027 0 -1 0 22533 0 0 0 111604 189 0 0 25 0 1 0 1843516564 93732864 22334 4294967295 134512640 135094434 3221224448 3221223104 134557900 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/5452/statm): 22884 22334 145 145 0 22739 0 [pid=5452] vsize: 91536 Current children cumulated CPU time (s) 1117.93 Current children cumulated vsize (Kb) 93660 [startup+1130.15 s] Raw data (loadavg): 1.00 1.00 0.97 2/57 5452 Raw data (/proc/5448/stat): 5448 (minisat+_script) S 5447 5448 31027 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843516560 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/5448/statm): 531 226 485 147 0 384 0 [pid=5448] vsize: 2124 Raw data (/proc/5452/stat): 5452 (minisat+_64-bit) R 5448 5448 31027 0 -1 0 22533 0 0 0 112604 189 0 0 25 0 1 0 1843516564 93732864 22334 4294967295 134512640 135094434 3221224448 3221223104 134558213 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/5452/statm): 22884 22334 145 145 0 22739 0 [pid=5452] vsize: 91536 Current children cumulated CPU time (s) 1127.93 Current children cumulated vsize (Kb) 93660 [startup+1140.15 s] Raw data (loadavg): 1.00 1.00 0.97 2/57 5452 Raw data (/proc/5448/stat): 5448 (minisat+_script) S 5447 5448 31027 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843516560 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/5448/statm): 531 226 485 147 0 384 0 [pid=5448] vsize: 2124 Raw data (/proc/5452/stat): 5452 (minisat+_64-bit) R 5448 5448 31027 0 -1 0 22533 0 0 0 113604 189 0 0 25 0 1 0 1843516564 93732864 22334 4294967295 134512640 135094434 3221224448 3221223136 134554717 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/5452/statm): 22884 22334 145 145 0 22739 0 [pid=5452] vsize: 91536 Current children cumulated CPU time (s) 1137.93 Current children cumulated vsize (Kb) 93660 [startup+1150.15 s] Raw data (loadavg): 1.00 1.00 0.97 2/57 5452 Raw data (/proc/5448/stat): 5448 (minisat+_script) S 5447 5448 31027 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843516560 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/5448/statm): 531 226 485 147 0 384 0 [pid=5448] vsize: 2124 Raw data (/proc/5452/stat): 5452 (minisat+_64-bit) R 5448 5448 31027 0 -1 0 22533 0 0 0 114604 190 0 0 25 0 1 0 1843516564 93732864 22334 4294967295 134512640 135094434 3221224448 3221223104 134557945 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/5452/statm): 22884 22334 145 145 0 22739 0 [pid=5452] vsize: 91536 Current children cumulated CPU time (s) 1147.94 Current children cumulated vsize (Kb) 93660 [startup+1160.15 s] Raw data (loadavg): 1.00 1.00 0.97 2/57 5452 Raw data (/proc/5448/stat): 5448 (minisat+_script) S 5447 5448 31027 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843516560 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/5448/statm): 531 226 485 147 0 384 0 [pid=5448] vsize: 2124 Raw data (/proc/5452/stat): 5452 (minisat+_64-bit) R 5448 5448 31027 0 -1 0 22533 0 0 0 115604 190 0 0 25 0 1 0 1843516564 93732864 22334 4294967295 134512640 135094434 3221224448 3221223104 134557948 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/5452/statm): 22884 22334 145 145 0 22739 0 [pid=5452] vsize: 91536 Current children cumulated CPU time (s) 1157.94 Current children cumulated vsize (Kb) 93660 [startup+1170.15 s] Raw data (loadavg): 1.00 1.00 0.97 2/57 5452 Raw data (/proc/5448/stat): 5448 (minisat+_script) S 5447 5448 31027 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843516560 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/5448/statm): 531 226 485 147 0 384 0 [pid=5448] vsize: 2124 Raw data (/proc/5452/stat): 5452 (minisat+_64-bit) R 5448 5448 31027 0 -1 0 22533 0 0 0 116604 190 0 0 25 0 1 0 1843516564 93732864 22334 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/5452/statm): 22884 22334 145 145 0 22739 0 [pid=5452] vsize: 91536 Current children cumulated CPU time (s) 1167.94 Current children cumulated vsize (Kb) 93660 [startup+1180.15 s] Raw data (loadavg): 1.00 1.00 0.97 2/57 5452 Raw data (/proc/5448/stat): 5448 (minisat+_script) S 5447 5448 31027 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843516560 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/5448/statm): 531 226 485 147 0 384 0 [pid=5448] vsize: 2124 Raw data (/proc/5452/stat): 5452 (minisat+_64-bit) R 5448 5448 31027 0 -1 0 22533 0 0 0 117604 191 0 0 25 0 1 0 1843516564 93732864 22334 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/5452/statm): 22884 22334 145 145 0 22739 0 [pid=5452] vsize: 91536 Current children cumulated CPU time (s) 1177.95 Current children cumulated vsize (Kb) 93660 [startup+1190.15 s] Raw data (loadavg): 1.00 1.00 0.97 2/57 5452 Raw data (/proc/5448/stat): 5448 (minisat+_script) S 5447 5448 31027 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843516560 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/5448/statm): 531 226 485 147 0 384 0 [pid=5448] vsize: 2124 Raw data (/proc/5452/stat): 5452 (minisat+_64-bit) R 5448 5448 31027 0 -1 0 22533 0 0 0 118603 191 0 0 25 0 1 0 1843516564 93732864 22334 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/5452/statm): 22884 22334 145 145 0 22739 0 [pid=5452] vsize: 91536 Current children cumulated CPU time (s) 1187.94 Current children cumulated vsize (Kb) 93660 [startup+1200.15 s] Raw data (loadavg): 1.00 1.00 0.97 2/57 5452 Raw data (/proc/5448/stat): 5448 (minisat+_script) S 5447 5448 31027 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843516560 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/5448/statm): 531 226 485 147 0 384 0 [pid=5448] vsize: 2124 Raw data (/proc/5452/stat): 5452 (minisat+_64-bit) R 5448 5448 31027 0 -1 0 22533 0 0 0 119603 192 0 0 25 0 1 0 1843516564 93732864 22334 4294967295 134512640 135094434 3221224448 3221223104 134557860 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/5452/statm): 22884 22334 145 145 0 22739 0 [pid=5452] vsize: 91536 Current children cumulated CPU time (s) 1197.95 Current children cumulated vsize (Kb) 93660 [startup+1210.16 s] Raw data (loadavg): 1.00 1.00 0.97 2/57 5452 Raw data (/proc/5448/stat): 5448 (minisat+_script) S 5447 5448 31027 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843516560 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/5448/statm): 531 226 485 147 0 384 0 [pid=5448] vsize: 2124 Raw data (/proc/5452/stat): 5452 (minisat+_64-bit) R 5448 5448 31027 0 -1 0 22533 0 0 0 120603 192 0 0 25 0 1 0 1843516564 93732864 22334 4294967295 134512640 135094434 3221224448 3221223040 134557040 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/5452/statm): 22884 22334 145 145 0 22739 0 [pid=5452] vsize: 91536 Current children cumulated CPU time (s) 1207.95 Current children cumulated vsize (Kb) 93660 Maximum CPU time exceeded: sending SIGTERM then SIGKILL [startup+1210.16 s] Raw data (loadavg): 1.00 1.00 0.97 2/57 5452 Raw data (/proc/5448/stat): 5448 (minisat+_script) S 5447 5448 31027 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843516560 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/5448/statm): 531 226 485 147 0 384 0 [pid=5448] vsize: 2124 Raw data (/proc/5452/stat): 5452 (minisat+_64-bit) R 5448 5448 31027 0 -1 0 22533 0 0 0 120603 192 0 0 25 0 1 0 1843516564 93732864 22334 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/5452/statm): 22884 22334 145 145 0 22739 0 [pid=5452] vsize: 91536 Current children cumulated CPU time (s) 1207.95 Current children cumulated vsize (Kb) 93660 Sending SIGTERM to -5448 Sleeping 2 seconds One traced child (pid=5448) ended because it received signal 15 (SIGTERM) One traced child (pid=5452) exited with status: 10 All traced children have exited ! Game is over. Child status: 10 Real time (s): 1210.21 CPU time (s): 1208 CPU user time (s): 1206.04 CPU system time (s): 1.9637 CPU usage (%): 99.8177 Max. virtual memory (cumulated for all children) (Kb): 93660
ERROR: no interpretation found !