Name | web/www.nlsde.buaa.edu.cn/~kexu/benchmarks/frb56-25-opb/normalized-frb56-25-3.opb |
MD5SUM | 3f087816af6a7fb75be2e9f81cc24df7 |
Bench Category | optimization, small integers (OPTSMALLINT) |
Has Objective Function | YES |
Satisfiable | YES |
(Un)Satisfiability was proved | YES |
Best value of the objective function | -43 |
Optimality of the best value was proved | NO |
Number of terms in the objective function | 1400 |
Biggest coefficient in the objective function | 1 |
Number of bits for the biggest coefficient in the objective function | 1 |
Sum of the numbers in the objective function | 1400 |
Number of bits of the sum of numbers in the objective function | 11 |
Biggest number in a constraint | 1 |
Number of bits of the biggest number in a constraint | 1 |
Biggest sum of numbers in a constraint | 1400 |
Number of bits of the biggest sum of numbers | 11 |
Best result obtained on this benchmark | SAT |
Best CPU time to get the best result obtained on this benchmark | 1203.19 |
Number of variables | 1400 |
Total number of constraints | 109379 |
Number of constraints which are clauses | 109379 |
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 wulflinc19 THE 2005-09-18 18:59:46 (client local time) PB2005-SCRIPT v4.0 MARKUPS: idlaunch=2719 boxname=wulflinc19 idbench=375 idsolver=3 numberseed=0 MD5SUM SOLVER: MD5SUM BENCH: 3f087816af6a7fb75be2e9f81cc24df7 /oldhome/oroussel/tmp/wulflinc19/normalized-frb56-25-3.opb REAL COMMAND: minisat+_script /oldhome/oroussel/tmp/wulflinc19/normalized-frb56-25-3.opb IDLAUNCH: 2719 /proc/cpuinfo: processor : 0 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 3 cpu MHz : 451.037 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 : 890.88 processor : 1 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 3 cpu MHz : 451.037 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: 919992 kB Buffers: 34528 kB Cached: 52904 kB SwapCached: 832 kB Active: 62924 kB Inactive: 27052 kB HighTotal: 131008 kB HighFree: 77420 kB LowTotal: 903652 kB LowFree: 842572 kB SwapTotal: 2097892 kB SwapFree: 2096460 kB Dirty: 28 kB Writeback: 0 kB Mapped: 5700 kB Slab: 19132 kB Committed_AS: 64184 kB PageTables: 328 kB VmallocTotal: 114680 kB VmallocUsed: 1368 kB VmallocChunk: 113252 kB JOB ENDED THE 2005-09-18 19:19:57 (client local time) WITH STATUS 10 IN 1207.53 SECONDS stats: 2719 7 1207.53 10
c Parsing PB file... c Converting 109379 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 | 109379 218758 | 36459 0 0 nan | 0.000 % | c ============================================================================== c [1mFound solution: -40[0m c ---[ 0]---> Sorter-cost:78076 Base: c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 0 | 193072 415055 | 64357 0 0 nan | 0.000 % | c | 100 | 192289 413380 | 70792 76 438 5.8 | 0.796 % | c | 250 | 191308 411295 | 77871 154 1089 7.1 | 1.765 % | c | 475 | 189986 408459 | 85659 332 3281 9.9 | 3.095 % | c | 812 | 188252 404641 | 94225 591 5859 9.9 | 4.924 % | c | 1318 | 185282 398055 | 103647 966 10783 11.2 | 8.159 % | c | 2077 | 180838 388205 | 114012 1540 17472 11.3 | 12.913 % | c | 3216 | 174564 374091 | 125413 2383 27299 11.5 | 19.709 % | c | 4924 | 165519 353508 | 137954 3677 43819 11.9 | 29.753 % | c | 7486 | 155664 330749 | 151750 5389 63888 11.9 | 40.969 % | 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 | 7678 | 155277 329891 | 51759 5555 66399 12.0 | 40.969 % | c | 7778 | 155112 329513 | 56934 5646 67027 11.9 | 41.617 % | c | 7928 | 154703 328544 | 62628 5760 68552 11.9 | 42.108 % | c | 8153 | 153653 326101 | 68891 5917 70305 11.9 | 43.312 % | c | 8491 | 152864 324267 | 75780 6136 73256 11.9 | 44.216 % | c | 8997 | 150953 319781 | 83358 6468 76139 11.8 | 46.384 % | c | 9756 | 148474 313934 | 91694 6960 82237 11.8 | 49.283 % | c | 10895 | 144799 305265 | 100863 7805 92930 11.9 | 53.569 % | c | 12603 | 139793 293375 | 110950 8870 106020 12.0 | 59.496 % | c | 15165 | 135051 282169 | 122045 10462 131410 12.6 | 65.125 % | c | 19010 | 129965 270060 | 134249 13548 195200 14.4 | 71.137 % | c | 24776 | 126588 261988 | 147674 18369 339931 18.5 | 75.205 % | c ============================================================================== c [1mFound solution: -44[0m c ---[ 0]---> Sorter-cost: 0 Base: c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 32090 | 124714 257528 | 41571 24908 642270 25.8 | 75.205 % | c | 32190 | 124620 257302 | 45728 24877 642286 25.8 | 77.650 % | c | 32340 | 124503 257023 | 50300 24964 645321 25.9 | 77.792 % | c | 32565 | 124503 257023 | 55331 25189 657624 26.1 | 77.792 % | c | 32902 | 124248 256413 | 60864 25322 668588 26.4 | 78.100 % | c | 33409 | 124048 255923 | 66950 25747 685296 26.6 | 78.349 % | c | 34169 | 123814 255346 | 73645 26344 707362 26.9 | 78.659 % | c | 35308 | 123314 254145 | 81010 26766 734139 27.4 | 79.251 % | c | 37016 | 122980 253317 | 89111 28310 800471 28.3 | 79.671 % | 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 | 38041 | 122955 253294 | 40985 29330 878435 30.0 | 79.671 % | c | 38141 | 122908 253175 | 45083 29428 881494 30.0 | 79.772 % | c | 38292 | 122808 252938 | 49591 29459 884935 30.0 | 79.889 % | c | 38517 | 122701 252678 | 54551 29640 893182 30.1 | 80.022 % | c | 38854 | 122469 252128 | 60006 29755 899984 30.2 | 80.300 % | c | 39360 | 122418 251995 | 66006 30229 921921 30.5 | 80.369 % | c | 40120 | 122408 251969 | 72607 30944 953783 30.8 | 80.383 % | c | 41259 | 121915 250781 | 79868 31596 1004535 31.8 | 80.976 % | c | 42967 | 121553 249906 | 87854 32982 1091208 33.1 | 81.405 % | c ============================================================================== c [1mFound solution: -46[0m c ---[ 0]---> Sorter-cost: 0 Base: c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 43880 | 120877 248170 | 40292 33490 1122781 33.5 | 81.405 % | c | 43981 | 120746 247855 | 44321 33468 1122634 33.5 | 82.436 % | c | 44131 | 120643 247601 | 48753 33534 1125930 33.6 | 82.568 % | c | 44356 | 120639 247591 | 53628 33757 1134632 33.6 | 82.573 % | c | 44694 | 120639 247591 | 58991 34095 1167457 34.2 | 82.573 % | c | 45202 | 120555 247389 | 64890 34455 1205966 35.0 | 82.676 % | c | 45961 | 120449 247139 | 71379 35097 1268003 36.1 | 82.802 % | c | 47100 | 120449 247139 | 78517 36236 1343983 37.1 | 82.802 % | c | 48808 | 120381 246969 | 86369 37873 1461540 38.6 | 82.891 % | c | 51370 | 120381 246969 | 95006 40435 1758124 43.5 | 82.891 % | c | 55214 | 120194 246508 | 104507 44166 2049429 46.4 | 83.131 % | c ============================================================================== c [1mFound solution: -47[0m c ---[ 0]---> Sorter-cost: 0 Base: c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 59419 | 120236 246644 | 40078 48283 2571328 53.3 | 83.131 % | c | 59519 | 120236 246644 | 44085 48383 2577827 53.3 | 83.121 % | c | 59669 | 120046 246170 | 48494 48153 2573782 53.5 | 83.366 % | c | 59894 | 120046 246170 | 53343 48378 2587917 53.5 | 83.366 % | c | 60231 | 120046 246170 | 58678 48715 2610106 53.6 | 83.366 % | c | 60737 | 119972 245994 | 64546 49150 2641554 53.7 | 83.455 % | c | 61496 | 119972 245994 | 71000 49909 2689717 53.9 | 83.455 % | c | 62635 | 119972 245994 | 78100 51048 2778866 54.4 | 83.455 % | c | 64345 | 119928 245882 | 85910 52609 2939154 55.9 | 83.512 % | c | 66908 | 119762 245470 | 94501 54951 3124242 56.9 | 83.722 % | c | 70752 | 119678 245269 | 103952 58681 3464776 59.0 | 83.821 % | c | 76518 | 119245 244229 | 114347 63705 4075621 64.0 | 84.345 % | c | 85167 | 119220 244168 | 125781 72202 4873608 67.5 | 84.377 % | c ============================================================================== c [1mFound solution: -48[0m c ---[ 0]---> Sorter-cost: 0 Base: c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 89191 | 119133 243922 | 39711 75689 5308024 70.1 | 84.377 % | c | 89293 | 119097 243838 | 43682 75747 5308704 70.1 | 84.538 % | c | 89443 | 119097 243838 | 48050 75897 5313532 70.0 | 84.538 % | c | 89668 | 119097 243838 | 52855 76122 5343666 70.2 | 84.538 % | c | 90005 | 119097 243838 | 58140 76459 5376009 70.3 | 84.538 % | c | 90511 | 119097 243838 | 63954 76965 5418238 70.4 | 84.538 % | c | 91270 | 119092 243827 | 70350 77719 5484685 70.6 | 84.543 % | c | 92410 | 119061 243749 | 77385 78821 5576081 70.7 | 84.583 % | c | 94119 | 119009 243626 | 85124 79969 5732669 71.7 | 84.641 % | c | 96681 | 118880 243323 | 93636 82103 6068614 73.9 | 84.793 % | c | 100525 | 118867 243294 | 103000 85937 6618201 77.0 | 84.807 % | c | 106291 | 118844 243239 | 113300 91697 7472440 81.5 | 84.835 % | c | 114941 | 118836 243219 | 124630 100333 8787645 87.6 | 84.845 % | c | 127915 | 118830 243203 | 137093 113301 10621442 93.7 | 84.854 % | c | 147376 | 118811 243160 | 150802 132530 13627869 102.8 | 84.875 % | c | 176568 | 118770 243067 | 165882 161493 19013368 117.7 | 84.920 % | c ============================================================================== c [1mFound solution: -49[0m c ---[ 0]---> Sorter-cost: 0 Base: c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 194891 | 118792 243133 | 39597 179816 22236738 123.7 | 84.920 % | c | 194991 | 118792 243133 | 43556 25721 2608842 101.4 | 84.904 % | c | 195141 | 118792 243133 | 47912 25871 2618895 101.2 | 84.904 % | c | 195366 | 118792 243133 | 52703 26096 2633968 100.9 | 84.904 % | c | 195703 | 118792 243133 | 57973 26433 2658439 100.6 | 84.904 % | c | 196209 | 118746 243016 | 63771 26900 2696719 100.2 | 84.960 % | c | 196968 | 118746 243016 | 70148 27659 2783846 100.6 | 84.960 % | c | 198107 | 118746 243016 | 77163 28798 2904085 100.8 | 84.960 % | c | 199815 | 118708 242922 | 84879 30503 3038914 99.6 | 85.009 % | c | 202377 | 118561 242559 | 93367 33010 3263398 98.9 | 85.195 % | c | 206221 | 118438 242259 | 102704 36848 3708724 100.6 | 85.347 % | c | 211987 | 118423 242224 | 112974 42603 4394753 103.2 | 85.365 % | c | 220636 | 118399 242168 | 124272 51236 5537942 108.1 | 85.393 % | c ============================================================================== c [1mFound solution: -50[0m c ---[ 0]---> Sorter-cost: 0 Base: c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 229090 | 118286 241857 | 39428 59647 6700392 112.3 | 85.393 % | c | 229190 | 118286 241857 | 43370 59747 6707785 112.3 | 85.535 % | c | 229342 | 118286 241857 | 47707 59899 6717998 112.2 | 85.535 % | c | 229567 | 118286 241857 | 52478 60124 6753812 112.3 | 85.535 % | c | 229904 | 118286 241857 | 57726 60461 6781159 112.2 | 85.535 % | c | 230410 | 118286 241857 | 63499 60967 6854467 112.4 | 85.535 % | c | 231169 | 118286 241857 | 69849 61726 6920330 112.1 | 85.535 % | c | 232308 | 118286 241857 | 76834 62865 7085436 112.7 | 85.535 % | c | 234016 | 118286 241857 | 84517 64573 7329189 113.5 | 85.535 % | c | 236578 | 118280 241843 | 92969 67081 7761358 115.7 | 85.542 % | c | 240423 | 118280 241843 | 102266 70926 8364204 117.9 | 85.542 % | c | 246189 | 118195 241640 | 112492 76643 9241235 120.6 | 85.644 % | c | 254838 | 118192 241633 | 123741 85290 10512072 123.3 | 85.648 % | c | 267813 | 118081 241357 | 136116 98069 12211460 124.5 | 85.791 % | c c *** TERMINATED *** s SATISFIABLE v -C1400 -C1399 -C1398 -C1397 -C1396 -C1395 -C1394 -C1393 -C1392 -C1391 -C1390 -C1389 -C1388 C1387 -C1386 -C1385 -C1384 -C1383 -C1382 -C1381 -C1380 -C1379 -C1378 -C1377 -C1376 -C1375 -C1374 -C1373 -C1372 -C1371 -C1370 -C1369 -C1368 -C1367 -C1366 -C1365 -C1364 -C1363 -C1362 -C1361 -C1360 -C1359 -C1358 -C1357 -C1356 -C1355 -C1354 -C1353 -C1352 -C1351 -C1350 -C1349 -C1348 -C1347 -C1346 -C1345 -C1344 -C1343 -C1342 -C1341 -C1340 -C1339 -C1338 -C1337 C1336 -C1335 -C1334 -C1333 -C1332 -C1331 -C1330 -C1329 -C1328 -C1327 -C1326 -C1325 -C1324 -C1323 -C1322 -C1321 -C1320 -C1319 -C1318 -C1317 -C1316 -C1315 -C1314 -C1313 -C1312 -C1311 -C1310 C1309 -C1308 -C1307 -C1306 -C1305 -C1304 -C1303 -C1302 -C1301 -C1300 -C1299 -C1298 -C1297 -C1296 -C1295 -C1294 -C1293 -C1292 -C1291 C1290 -C1289 -C1288 -C1287 -C1286 -C1285 -C1284 -C1283 -C1282 -C1281 -C1280 -C1279 -C1278 -C1277 -C1276 C1275 -C1274 -C1273 -C1272 -C1271 -C1270 -C1269 -C1268 -C1267 -C1266 -C1265 -C1264 -C1263 -C1262 -C1261 -C1260 -C1259 -C1258 -C1257 -C1256 -C1255 -C1254 -C1253 -C1252 -C1251 -C1250 -C1249 -C1248 -C1247 -C1246 -C1245 -C1244 -C1243 -C1242 -C1241 -C1240 -C1239 -C1238 -C1237 -C1236 -C1235 -C1234 -C1233 -C1232 -C1231 -C1230 -C1229 C1228 -C1227 -C1226 -C1225 -C1224 -C1223 -C1222 -C1221 -C1220 -C1219 -C1218 -C1217 -C1216 -C1215 -C1214 -C1213 -C1212 -C1211 -C1210 -C1209 -C1208 -C1207 -C1206 -C1205 -C1204 -C1203 -C1202 -C1201 -C1200 -C1199 -C1198 -C1197 -C1196 -C1195 -C1194 -C1193 -C1192 -C1191 -C1190 -C1189 -C1188 -C1187 -C1186 -C1185 -C1184 -C1183 -C1182 -C1181 -C1180 -C1179 -C1178 C1177 -C1176 -C1175 -C1174 C1173 -C1172 -C1171 -C1170 -C1169 -C1168 -C1167 -C1166 -C1165 -C1164 -C1163 -C1162 -C1161 -C1160 -C1159 -C1158 -C1157 -C1156 -C1155 -C1154 -C1153 -C1152 -C1151 -C1150 -C1149 -C1148 -C1147 -C1146 -C1145 -C1144 -C1143 -C1142 -C1141 -C1140 -C1139 -C1138 -C1137 -C1136 -C1135 -C1134 -C1133 -C1132 -C1131 -C1130 C1129 -C1128 -C1127 -C1126 -C1125 -C1124 -C1123 -C1122 -C1121 -C1120 -C1119 -C1118 -C1117 -C1116 -C1115 C1114 -C1113 -C1112 -C1111 -C1110 -C1109 -C1108 -C1107 -C1106 -C1105 -C1104 -C1103 -C1102 -C1101 -C1100 -C1099 -C1098 -C1097 -C1096 -C1095 -C1094 -C1093 -C1092 -C1091 -C1090 -C1089 -C1088 -C1087 -C1086 -C1085 -C1084 -C1083 -C1082 -C1081 -C1080 -C1079 -C1078 -C1077 -C1076 -C1075 -C1074 -C1073 -C1072 -C1071 -C1070 -C1069 -C1068 -C1067 -C1066 -C1065 -C1064 -C1063 -C1062 C1061 -C1060 -C1059 -C1058 -C1057 -C1056 -C1055 -C1054 -C1053 -C1052 -C1051 -C1050 -C1049 -C1048 -C1047 -C1046 -C1045 -C1044 -C1043 -C1042 -C1041 C1040 -C1039 -C1038 -C1037 -C1036 -C1035 -C1034 -C1033 -C1032 -C1031 -C1030 -C1029 -C1028 -C1027 -C1026 -C1025 -C1024 -C1023 -C1022 -C1021 -C1020 -C1019 -C1018 -C1017 -C1016 -C1015 -C1014 -C1013 -C1012 -C1011 -C1010 -C1009 -C1008 -C1007 -C1006 -C1005 -C1004 -C1003 C1002 -C1001 -C1000 -C999 -C998 -C997 -C996 -C995 C994 -C993 -C992 -C991 -C990 -C989 -C988 -C987 -C986 -C985 -C984 -C983 -C982 -C981 -C980 -C979 -C978 -C977 -C976 -C975 -C974 -C973 -C972 -C971 C970 -C969 -C968 -C967 -C966 -C965 -C964 -C963 -C962 -C961 -C960 -C959 -C958 -C957 -C956 -C955 -C954 -C953 -C952 -C951 -C950 -C949 -C948 C947 -C946 -C945 -C944 -C943 -C942 -C941 -C940 -C939 -C938 -C937 -C936 -C935 -C934 -C933 -C932 -C931 -C930 -C929 -C928 -C927 -C926 -C925 -C924 -C923 -C922 -C921 -C920 -C919 -C918 -C917 -C916 -C915 -C914 -C913 -C912 -C911 -C910 -C909 -C908 -C907 -C906 C905 -C904 -C903 -C902 -C901 -C900 -C899 -C898 -C897 -C896 -C895 -C894 -C893 -C892 -C891 -C890 -C889 -C888 -C887 -C886 -C885 -C884 -C883 -C882 -C881 -C880 -C879 C878 -C877 -C876 -C875 -C874 -C873 -C872 -C871 -C870 -C869 -C868 -C867 -C866 -C865 -C864 -C863 -C862 -C861 -C860 -C859 -C858 -C857 -C856 -C855 C854 -C853 -C852 -C851 -C850 -C849 C848 -C847 -C846 -C845 -C844 -C843 -C842 -C841 -C840 -C839 -C838 -C837 -C836 -C835 -C834 -C833 -C832 -C831 -C830 -C829 -C828 -C827 -C826 -C825 C824 -C823 -C822 -C821 -C820 -C819 -C818 -C817 -C816 -C815 -C814 -C813 -C812 -C811 -C810 -C809 -C808 -C807 -C806 -C805 -C804 -C803 -C802 -C801 -C800 -C799 -C798 -C797 -C796 -C795 -C794 -C793 -C792 -C791 -C790 -C789 -C788 -C787 -C786 -C785 -C784 -C783 -C782 -C781 -C780 -C779 -C778 -C777 C776 -C775 -C774 -C773 -C772 -C771 -C770 -C769 -C768 -C767 -C766 -C765 -C764 -C763 -C762 C761 -C760 -C759 -C758 -C757 -C756 -C755 -C754 -C753 -C752 -C751 -C750 -C749 -C748 -C747 -C746 -C745 -C744 -C743 -C742 -C741 -C740 -C739 -C738 -C737 -C736 -C735 -C734 -C733 -C732 -C731 -C730 -C729 -C728 -C727 C726 -C725 -C724 -C723 -C722 -C721 -C720 -C719 -C718 -C717 -C716 -C715 -C714 -C713 -C712 -C711 -C710 -C709 -C708 -C707 -C706 -C705 C704 -C703 -C702 -C701 -C700 C699 -C698 -C697 -C696 -C695 -C694 -C693 -C692 -C691 -C690 -C689 -C688 -C687 -C686 -C685 -C684 -C683 -C682 -C681 -C680 -C679 -C678 -C677 -C676 -C675 -C674 -C673 -C672 -C671 -C670 -C669 -C668 -C667 -C666 C665 -C664 -C663 -C662 -C661 -C660 -C659 -C658 -C657 -C656 -C655 -C654 -C653 -C652 -C651 -C650 -C649 -C648 -C647 -C646 -C645 -C644 -C643 -C642 -C641 -C640 -C639 -C638 -C637 -C636 -C635 C634 -C633 -C632 -C631 -C630 -C629 -C628 -C627 -C626 -C625 -C624 -C623 -C622 -C621 -C620 -C619 -C618 -C617 -C616 -C615 -C614 -C613 -C612 -C611 -C610 -C609 -C608 -C607 C606 -C605 -C604 -C603 -C602 -C601 -C600 C599 -C598 -C597 -C596 -C595 -C594 -C593 -C592 -C591 -C590 -C589 -C588 -C587 -C586 -C585 -C584 -C583 -C582 -C581 -C580 -C579 -C578 -C577 -C576 -C575 -C574 -C573 -C572 -C571 -C570 -C569 -C568 -C567 -C566 -C565 -C564 -C563 -C562 -C561 -C560 C559 -C558 -C557 -C556 -C555 -C554 -C553 -C552 -C551 -C550 -C549 -C548 -C547 C546 -C545 -C544 -C543 -C542 -C541 -C540 -C539 -C538 -C537 -C536 -C535 -C534 -C533 -C532 -C531 -C530 -C529 -C528 -C527 -C526 -C525 -C524 -C523 -C522 -C521 -C520 -C519 -C518 -C517 -C516 -C515 -C514 -C513 -C512 -C511 -C510 -C509 -C508 -C507 -C506 -C505 -C504 -C503 C502 -C501 -C500 -C499 -C498 -C497 -C496 C495 -C494 -C493 -C492 -C491 -C490 -C489 -C488 -C487 -C486 -C485 -C484 -C483 -C482 -C481 -C480 -C479 -C478 -C477 -C476 -C475 -C474 -C473 -C472 -C471 -C470 -C469 -C468 -C467 -C466 -C465 -C464 -C463 -C462 -C461 -C460 -C459 -C458 -C457 -C456 -C455 -C454 -C453 C452 -C451 -C450 C449 -C448 -C447 -C446 -C445 -C444 -C443 -C442 -C441 -C440 -C439 -C438 -C437 -C436 -C435 -C434 -C433 -C432 -C431 -C430 -C429 -C428 -C427 -C426 -C425 -C424 -C423 -C422 -C421 -C420 -C419 -C418 -C417 -C416 -C415 -C414 -C413 -C412 -C411 -C410 -C409 -C408 -C407 -C406 -C405 C404 -C403 -C402 -C401 -C400 -C399 -C398 -C397 -C396 -C395 -C394 -C393 -C392 -C391 -C390 -C389 -C388 -C387 -C386 -C385 -C384 -C383 -C382 -C381 -C380 -C379 -C378 -C377 -C376 -C375 -C374 -C373 -C372 -C371 -C370 -C369 -C368 -C367 -C366 -C365 -C364 -C363 -C362 -C361 -C360 -C359 -C358 -C357 -C356 -C355 -C354 -C353 -C352 -C351 -C350 -C349 -C348 -C347 -C346 -C345 -C344 -C343 -C342 -C341 -C340 -C339 -C338 -C337 -C336 -C335 -C334 -C333 -C332 -C331 -C330 -C329 -C328 C327 -C326 -C325 -C324 -C323 -C322 C321 -C320 -C319 -C318 -C317 -C316 -C315 -C314 -C313 -C312 -C311 -C310 -C309 -C308 -C307 -C306 -C305 -C304 -C303 -C302 -C301 -C300 -C299 -C298 -C297 -C296 -C295 -C294 -C293 -C292 -C291 -C290 -C289 -C288 -C287 -C286 -C285 -C284 C283 -C282 -C281 -C280 -C279 -C278 -C277 -C276 -C275 -C274 -C273 -C272 -C271 -C270 -C269 -C268 -C267 -C266 -C265 -C264 -C263 -C262 -C261 -C260 -C259 -C258 -C257 -C256 -C255 -C254 -C253 -C252 -C251 -C250 C249 -C248 -C247 -C246 -C245 -C244 -C243 -C242 -C241 -C240 -C239 -C238 -C237 -C236 -C235 -C234 -C233 -C232 -C231 -C230 -C229 -C228 -C227 -C226 -C225 -C224 -C223 -C222 -C221 -C220 -C219 -C218 -C217 -C216 -C215 -C214 -C213 -C212 -C211 -C210 -C209 -C208 -C207 -C206 -C205 -C204 -C203 -C202 C201 -C200 -C199 -C198 -C197 -C196 -C195 -C194 -C193 -C192 -C191 -C190 -C189 -C188 -C187 -C186 -C185 -C184 C183 -C182 -C181 -C180 -C179 -C178 -C177 -C176 -C175 -C174 -C173 -C172 -C171 -C170 -C169 -C168 -C167 -C166 -C165 -C164 -C163 C162 -C161 -C160 -C159 -C158 -C157 -C156 -C155 -C154 -C153 -C152 -C151 -C150 -C149 -C148 -C147 C146 -C145 -C144 -C143 -C142 -C141 -C140 -C139 -C138 -C137 -C136 -C135 -C134 -C133 -C132 -C131 -C130 -C129 -C128 -C127 -C126 -C125 -C124 -C123 -C122 -C121 -C120 -C119 -C118 -C117 -C116 -C115 -C114 -C113 -C112 -C111 -C110 -C109 -C108 -C107 -C106 -C105 -C104 C103 -C102 -C1
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/12864/stat): 12864 (minisat+_script) R 12863 12864 5929 0 -1 0 19 0 0 0 0 0 0 0 23 0 1 0 1843588559 712704 3 4294967295 134512640 135087896 3221224512 3221224512 1073744960 0 0 5 0 0 0 0 17 1 0 0 Raw data (/proc/12864/statm): 174 3 169 147 0 27 0 [pid=12864] 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=12865 New process pid=12866 New process pid=12867 One traced child (pid=12866) exited with status: 0 execve syscall for /bin/sed executable open syscall for file /etc/ld.so.preload open syscall for file tls/i686/mmx/libc.so.6 open syscall for file tls/i686/libc.so.6 open syscall for file tls/mmx/libc.so.6 open syscall for file tls/libc.so.6 open syscall for file i686/mmx/libc.so.6 open syscall for file i686/libc.so.6 open syscall for file mmx/libc.so.6 open syscall for file libc.so.6 open syscall for file /oldhome/oroussel/lib/tls/i686/mmx/libc.so.6 open syscall for file /oldhome/oroussel/lib/tls/i686/libc.so.6 open syscall for file /oldhome/oroussel/lib/tls/mmx/libc.so.6 open syscall for file /oldhome/oroussel/lib/tls/libc.so.6 open syscall for file /oldhome/oroussel/lib/i686/mmx/libc.so.6 open syscall for file /oldhome/oroussel/lib/i686/libc.so.6 open syscall for file /oldhome/oroussel/lib/mmx/libc.so.6 open syscall for file /oldhome/oroussel/lib/libc.so.6 open syscall for file /etc/ld.so.cache open syscall for file /lib/tls/libc.so.6 One traced child (pid=12867) exited with status: 0 One traced child (pid=12865) exited with status: 0 New process pid=12868 execve syscall for /oldhome/oroussel/solvers/minisat+_64-bit_static executable open syscall for file /dev/null open syscall for file /oldhome/oroussel/tmp/wulflinc19/normalized-frb56-25-3.opb [startup+10.0034 s] Raw data (loadavg): 0.93 0.95 0.94 2/57 12868 Raw data (/proc/12864/stat): 12864 (minisat+_script) S 12863 12864 5929 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843588559 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/12864/statm): 531 226 485 147 0 384 0 [pid=12864] vsize: 2124 Raw data (/proc/12868/stat): 12868 (minisat+_64-bit) R 12864 12864 5929 0 -1 0 6833 0 0 0 947 27 0 0 25 0 1 0 1843588564 28594176 6820 4294967295 134512640 135094434 3221224448 3221223108 134553450 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/12868/statm): 6981 6820 145 145 0 6836 0 [pid=12868] vsize: 27924 Current children cumulated CPU time (s) 9.75 Current children cumulated vsize (Kb) 30048 [startup+20.0052 s] Raw data (loadavg): 0.94 0.96 0.94 2/57 12868 Raw data (/proc/12864/stat): 12864 (minisat+_script) S 12863 12864 5929 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843588559 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/12864/statm): 531 226 485 147 0 384 0 [pid=12864] vsize: 2124 Raw data (/proc/12868/stat): 12868 (minisat+_64-bit) R 12864 12864 5929 0 -1 0 6833 0 0 0 1947 27 0 0 25 0 1 0 1843588564 28594176 6820 4294967295 134512640 135094434 3221224448 3221223108 134553446 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/12868/statm): 6981 6820 145 145 0 6836 0 [pid=12868] vsize: 27924 Current children cumulated CPU time (s) 19.75 Current children cumulated vsize (Kb) 30048 [startup+30.007 s] Raw data (loadavg): 0.95 0.96 0.94 2/57 12868 Raw data (/proc/12864/stat): 12864 (minisat+_script) S 12863 12864 5929 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843588559 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/12864/statm): 531 226 485 147 0 384 0 [pid=12864] vsize: 2124 Raw data (/proc/12868/stat): 12868 (minisat+_64-bit) R 12864 12864 5929 0 -1 0 6833 0 0 0 2946 28 0 0 25 0 1 0 1843588564 28594176 6820 4294967295 134512640 135094434 3221224448 3221223108 134553450 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/12868/statm): 6981 6820 145 145 0 6836 0 [pid=12868] vsize: 27924 Current children cumulated CPU time (s) 29.75 Current children cumulated vsize (Kb) 30048 [startup+40.0078 s] Raw data (loadavg): 0.96 0.96 0.94 2/57 12868 Raw data (/proc/12864/stat): 12864 (minisat+_script) S 12863 12864 5929 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843588559 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/12864/statm): 531 226 485 147 0 384 0 [pid=12864] vsize: 2124 Raw data (/proc/12868/stat): 12868 (minisat+_64-bit) R 12864 12864 5929 0 -1 0 6833 0 0 0 3946 28 0 0 25 0 1 0 1843588564 28594176 6820 4294967295 134512640 135094434 3221224448 3221223136 134554746 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/12868/statm): 6981 6820 145 145 0 6836 0 [pid=12868] vsize: 27924 Current children cumulated CPU time (s) 39.75 Current children cumulated vsize (Kb) 30048 [startup+50.0096 s] Raw data (loadavg): 0.96 0.96 0.94 2/57 12868 Raw data (/proc/12864/stat): 12864 (minisat+_script) S 12863 12864 5929 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843588559 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/12864/statm): 531 226 485 147 0 384 0 [pid=12864] vsize: 2124 Raw data (/proc/12868/stat): 12868 (minisat+_64-bit) R 12864 12864 5929 0 -1 0 6833 0 0 0 4946 28 0 0 25 0 1 0 1843588564 28594176 6820 4294967295 134512640 135094434 3221224448 3221223140 134558984 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/12868/statm): 6981 6820 145 145 0 6836 0 [pid=12868] vsize: 27924 Current children cumulated CPU time (s) 49.75 Current children cumulated vsize (Kb) 30048 [startup+60.0104 s] Raw data (loadavg): 0.97 0.96 0.94 2/57 12868 Raw data (/proc/12864/stat): 12864 (minisat+_script) S 12863 12864 5929 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843588559 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/12864/statm): 531 226 485 147 0 384 0 [pid=12864] vsize: 2124 Raw data (/proc/12868/stat): 12868 (minisat+_64-bit) R 12864 12864 5929 0 -1 0 6833 0 0 0 5946 28 0 0 25 0 1 0 1843588564 28594176 6820 4294967295 134512640 135094434 3221224448 3221223108 134553446 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/12868/statm): 6981 6820 145 145 0 6836 0 [pid=12868] vsize: 27924 Current children cumulated CPU time (s) 59.75 Current children cumulated vsize (Kb) 30048 [startup+70.0122 s] Raw data (loadavg): 0.97 0.96 0.94 2/57 12868 Raw data (/proc/12864/stat): 12864 (minisat+_script) S 12863 12864 5929 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843588559 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/12864/statm): 531 226 485 147 0 384 0 [pid=12864] vsize: 2124 Raw data (/proc/12868/stat): 12868 (minisat+_64-bit) R 12864 12864 5929 0 -1 0 6833 0 0 0 6946 28 0 0 25 0 1 0 1843588564 28594176 6820 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/12868/statm): 6981 6820 145 145 0 6836 0 [pid=12868] vsize: 27924 Current children cumulated CPU time (s) 69.75 Current children cumulated vsize (Kb) 30048 [startup+80.013 s] Raw data (loadavg): 0.98 0.96 0.94 2/57 12868 Raw data (/proc/12864/stat): 12864 (minisat+_script) S 12863 12864 5929 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843588559 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/12864/statm): 531 226 485 147 0 384 0 [pid=12864] vsize: 2124 Raw data (/proc/12868/stat): 12868 (minisat+_64-bit) R 12864 12864 5929 0 -1 0 6833 0 0 0 7946 28 0 0 25 0 1 0 1843588564 28594176 6820 4294967295 134512640 135094434 3221224448 3221223132 134553432 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/12868/statm): 6981 6820 145 145 0 6836 0 [pid=12868] vsize: 27924 Current children cumulated CPU time (s) 79.75 Current children cumulated vsize (Kb) 30048 [startup+90.0138 s] Raw data (loadavg): 0.98 0.96 0.94 2/57 12868 Raw data (/proc/12864/stat): 12864 (minisat+_script) S 12863 12864 5929 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843588559 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/12864/statm): 531 226 485 147 0 384 0 [pid=12864] vsize: 2124 Raw data (/proc/12868/stat): 12868 (minisat+_64-bit) R 12864 12864 5929 0 -1 0 6833 0 0 0 8947 28 0 0 25 0 1 0 1843588564 28594176 6820 4294967295 134512640 135094434 3221224448 3221223108 134553450 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/12868/statm): 6981 6820 145 145 0 6836 0 [pid=12868] vsize: 27924 Current children cumulated CPU time (s) 89.76 Current children cumulated vsize (Kb) 30048 [startup+100.015 s] Raw data (loadavg): 0.98 0.96 0.94 2/57 12868 Raw data (/proc/12864/stat): 12864 (minisat+_script) S 12863 12864 5929 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843588559 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/12864/statm): 531 226 485 147 0 384 0 [pid=12864] vsize: 2124 Raw data (/proc/12868/stat): 12868 (minisat+_64-bit) R 12864 12864 5929 0 -1 0 6833 0 0 0 9947 28 0 0 25 0 1 0 1843588564 28594176 6820 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/12868/statm): 6981 6820 145 145 0 6836 0 [pid=12868] vsize: 27924 Current children cumulated CPU time (s) 99.76 Current children cumulated vsize (Kb) 30048 [startup+110.015 s] Raw data (loadavg): 0.98 0.96 0.94 2/57 12868 Raw data (/proc/12864/stat): 12864 (minisat+_script) S 12863 12864 5929 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843588559 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/12864/statm): 531 226 485 147 0 384 0 [pid=12864] vsize: 2124 Raw data (/proc/12868/stat): 12868 (minisat+_64-bit) R 12864 12864 5929 0 -1 0 6833 0 0 0 10947 28 0 0 25 0 1 0 1843588564 28594176 6820 4294967295 134512640 135094434 3221224448 3221223108 134553446 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/12868/statm): 6981 6820 145 145 0 6836 0 [pid=12868] vsize: 27924 Current children cumulated CPU time (s) 109.76 Current children cumulated vsize (Kb) 30048 [startup+120.017 s] Raw data (loadavg): 0.99 0.97 0.94 2/57 12868 Raw data (/proc/12864/stat): 12864 (minisat+_script) S 12863 12864 5929 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843588559 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/12864/statm): 531 226 485 147 0 384 0 [pid=12864] vsize: 2124 Raw data (/proc/12868/stat): 12868 (minisat+_64-bit) R 12864 12864 5929 0 -1 0 6833 0 0 0 11947 28 0 0 25 0 1 0 1843588564 28594176 6820 4294967295 134512640 135094434 3221224448 3221223108 134553446 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/12868/statm): 6981 6820 145 145 0 6836 0 [pid=12868] vsize: 27924 Current children cumulated CPU time (s) 119.76 Current children cumulated vsize (Kb) 30048 [startup+130.018 s] Raw data (loadavg): 0.99 0.97 0.94 2/57 12868 Raw data (/proc/12864/stat): 12864 (minisat+_script) S 12863 12864 5929 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843588559 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/12864/statm): 531 226 485 147 0 384 0 [pid=12864] vsize: 2124 Raw data (/proc/12868/stat): 12868 (minisat+_64-bit) R 12864 12864 5929 0 -1 0 6833 0 0 0 12948 28 0 0 25 0 1 0 1843588564 28594176 6820 4294967295 134512640 135094434 3221224448 3221223108 134553491 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/12868/statm): 6981 6820 145 145 0 6836 0 [pid=12868] vsize: 27924 Current children cumulated CPU time (s) 129.77 Current children cumulated vsize (Kb) 30048 [startup+140.019 s] Raw data (loadavg): 0.99 0.97 0.94 2/57 12868 Raw data (/proc/12864/stat): 12864 (minisat+_script) S 12863 12864 5929 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843588559 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/12864/statm): 531 226 485 147 0 384 0 [pid=12864] vsize: 2124 Raw data (/proc/12868/stat): 12868 (minisat+_64-bit) R 12864 12864 5929 0 -1 0 6833 0 0 0 13948 28 0 0 25 0 1 0 1843588564 28594176 6820 4294967295 134512640 135094434 3221224448 3221223108 134553450 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/12868/statm): 6981 6820 145 145 0 6836 0 [pid=12868] vsize: 27924 Current children cumulated CPU time (s) 139.77 Current children cumulated vsize (Kb) 30048 [startup+150.021 s] Raw data (loadavg): 0.99 0.97 0.94 2/57 12868 Raw data (/proc/12864/stat): 12864 (minisat+_script) S 12863 12864 5929 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843588559 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/12864/statm): 531 226 485 147 0 384 0 [pid=12864] vsize: 2124 Raw data (/proc/12868/stat): 12868 (minisat+_64-bit) R 12864 12864 5929 0 -1 0 6963 0 0 0 14946 29 0 0 25 0 1 0 1843588564 29122560 6950 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/12868/statm): 7110 6950 145 145 0 6965 0 [pid=12868] vsize: 28440 Current children cumulated CPU time (s) 149.76 Current children cumulated vsize (Kb) 30564 [startup+160.021 s] Raw data (loadavg): 0.99 0.97 0.94 2/57 12868 Raw data (/proc/12864/stat): 12864 (minisat+_script) S 12863 12864 5929 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843588559 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/12864/statm): 531 226 485 147 0 384 0 [pid=12864] vsize: 2124 Raw data (/proc/12868/stat): 12868 (minisat+_64-bit) R 12864 12864 5929 0 -1 0 7288 0 0 0 15941 31 0 0 25 0 1 0 1843588564 30146560 7200 4294967295 134512640 135094434 3221224448 3221223040 134557152 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/12868/statm): 7360 7200 145 145 0 7215 0 [pid=12868] vsize: 29440 Current children cumulated CPU time (s) 159.73 Current children cumulated vsize (Kb) 31564 [startup+170.023 s] Raw data (loadavg): 0.99 0.97 0.94 2/57 12868 Raw data (/proc/12864/stat): 12864 (minisat+_script) S 12863 12864 5929 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843588559 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/12864/statm): 531 226 485 147 0 384 0 [pid=12864] vsize: 2124 Raw data (/proc/12868/stat): 12868 (minisat+_64-bit) R 12864 12864 5929 0 -1 0 7591 0 0 0 16936 34 0 0 25 0 1 0 1843588564 31076352 7427 4294967295 134512640 135094434 3221224448 3221223140 134558984 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/12868/statm): 7587 7427 145 145 0 7442 0 [pid=12868] vsize: 30348 Current children cumulated CPU time (s) 169.71 Current children cumulated vsize (Kb) 32472 [startup+180.024 s] Raw data (loadavg): 0.99 0.97 0.94 2/57 12868 Raw data (/proc/12864/stat): 12864 (minisat+_script) S 12863 12864 5929 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843588559 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/12864/statm): 531 226 485 147 0 384 0 [pid=12864] vsize: 2124 Raw data (/proc/12868/stat): 12868 (minisat+_64-bit) R 12864 12864 5929 0 -1 0 7832 0 0 0 17931 35 0 0 25 0 1 0 1843588564 32190464 7668 4294967295 134512640 135094434 3221224448 3221223108 134553530 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/12868/statm): 7859 7668 145 145 0 7714 0 [pid=12868] vsize: 31436 Current children cumulated CPU time (s) 179.67 Current children cumulated vsize (Kb) 33560 [startup+190.025 s] Raw data (loadavg): 0.99 0.97 0.94 2/57 12868 Raw data (/proc/12864/stat): 12864 (minisat+_script) S 12863 12864 5929 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843588559 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/12864/statm): 531 226 485 147 0 384 0 [pid=12864] vsize: 2124 Raw data (/proc/12868/stat): 12868 (minisat+_64-bit) R 12864 12864 5929 0 -1 0 8174 0 0 0 18926 38 0 0 25 0 1 0 1843588564 33271808 7935 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/12868/statm): 8123 7935 145 145 0 7978 0 [pid=12868] vsize: 32492 Current children cumulated CPU time (s) 189.65 Current children cumulated vsize (Kb) 34616 [startup+200.026 s] Raw data (loadavg): 0.99 0.97 0.94 2/57 12868 Raw data (/proc/12864/stat): 12864 (minisat+_script) S 12863 12864 5929 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843588559 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/12864/statm): 531 226 485 147 0 384 0 [pid=12864] vsize: 2124 Raw data (/proc/12868/stat): 12868 (minisat+_64-bit) R 12864 12864 5929 0 -1 0 8676 0 0 0 19917 41 0 0 25 0 1 0 1843588564 35307520 8437 4294967295 134512640 135094434 3221224448 3221223108 134553482 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/12868/statm): 8620 8437 145 145 0 8475 0 [pid=12868] vsize: 34480 Current children cumulated CPU time (s) 199.59 Current children cumulated vsize (Kb) 36604 [startup+210.026 s] Raw data (loadavg): 0.99 0.97 0.94 2/57 12868 Raw data (/proc/12864/stat): 12864 (minisat+_script) S 12863 12864 5929 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843588559 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/12864/statm): 531 226 485 147 0 384 0 [pid=12864] vsize: 2124 Raw data (/proc/12868/stat): 12868 (minisat+_64-bit) R 12864 12864 5929 0 -1 0 9072 0 0 0 20910 45 0 0 25 0 1 0 1843588564 36913152 8833 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/12868/statm): 9012 8833 145 145 0 8867 0 [pid=12868] vsize: 36048 Current children cumulated CPU time (s) 209.56 Current children cumulated vsize (Kb) 38172 [startup+220.028 s] Raw data (loadavg): 0.99 0.97 0.94 2/57 12868 Raw data (/proc/12864/stat): 12864 (minisat+_script) S 12863 12864 5929 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843588559 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/12864/statm): 531 226 485 147 0 384 0 [pid=12864] vsize: 2124 Raw data (/proc/12868/stat): 12868 (minisat+_64-bit) R 12864 12864 5929 0 -1 0 9615 0 0 0 21901 49 0 0 25 0 1 0 1843588564 38813696 9300 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/12868/statm): 9476 9300 145 145 0 9331 0 [pid=12868] vsize: 37904 Current children cumulated CPU time (s) 219.51 Current children cumulated vsize (Kb) 40028 [startup+230.029 s] Raw data (loadavg): 0.99 0.97 0.94 2/57 12868 Raw data (/proc/12864/stat): 12864 (minisat+_script) S 12863 12864 5929 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843588559 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/12864/statm): 531 226 485 147 0 384 0 [pid=12864] vsize: 2124 Raw data (/proc/12868/stat): 12868 (minisat+_64-bit) R 12864 12864 5929 0 -1 0 9975 0 0 0 22896 51 0 0 25 0 1 0 1843588564 40271872 9660 4294967295 134512640 135094434 3221224448 3221223104 134558232 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/12868/statm): 9832 9660 145 145 0 9687 0 [pid=12868] vsize: 39328 Current children cumulated CPU time (s) 229.48 Current children cumulated vsize (Kb) 41452 [startup+240.03 s] Raw data (loadavg): 0.99 0.97 0.94 2/57 12868 Raw data (/proc/12864/stat): 12864 (minisat+_script) S 12863 12864 5929 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843588559 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/12864/statm): 531 226 485 147 0 384 0 [pid=12864] vsize: 2124 Raw data (/proc/12868/stat): 12868 (minisat+_64-bit) R 12864 12864 5929 0 -1 0 10297 0 0 0 23890 53 0 0 25 0 1 0 1843588564 41578496 9982 4294967295 134512640 135094434 3221224448 3221223072 134557650 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/12868/statm): 10151 9982 145 145 0 10006 0 [pid=12868] vsize: 40604 Current children cumulated CPU time (s) 239.44 Current children cumulated vsize (Kb) 42728 [startup+250.031 s] Raw data (loadavg): 0.99 0.97 0.94 2/57 12868 Raw data (/proc/12864/stat): 12864 (minisat+_script) S 12863 12864 5929 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843588559 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/12864/statm): 531 226 485 147 0 384 0 [pid=12864] vsize: 2124 Raw data (/proc/12868/stat): 12868 (minisat+_64-bit) R 12864 12864 5929 0 -1 0 10606 0 0 0 24883 55 0 0 25 0 1 0 1843588564 42831872 10291 4294967295 134512640 135094434 3221224448 3221223108 134553491 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/12868/statm): 10457 10291 145 145 0 10312 0 [pid=12868] vsize: 41828 Current children cumulated CPU time (s) 249.39 Current children cumulated vsize (Kb) 43952 [startup+260.032 s] Raw data (loadavg): 0.99 0.97 0.94 1/57 12868 Raw data (/proc/12864/stat): 12864 (minisat+_script) S 12863 12864 5929 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843588559 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/12864/statm): 531 226 485 147 0 384 0 [pid=12864] vsize: 2124 Raw data (/proc/12868/stat): 12868 (minisat+_64-bit) T 12864 12864 5929 0 -1 0 11038 0 0 0 25877 58 0 0 25 0 1 0 1843588564 44593152 10723 4294967295 134512640 135094434 3221224448 3221222812 134870330 0 0 5 16386 3222434794 0 0 17 0 0 0 Raw data (/proc/12868/statm): 10887 10723 145 145 0 10742 0 [pid=12868] vsize: 43548 Current children cumulated CPU time (s) 259.36 Current children cumulated vsize (Kb) 45672 [startup+270.033 s] Raw data (loadavg): 0.99 0.97 0.94 2/57 12868 Raw data (/proc/12864/stat): 12864 (minisat+_script) S 12863 12864 5929 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843588559 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/12864/statm): 531 226 485 147 0 384 0 [pid=12864] vsize: 2124 Raw data (/proc/12868/stat): 12868 (minisat+_64-bit) R 12864 12864 5929 0 -1 0 11375 0 0 0 26870 61 0 0 25 0 1 0 1843588564 45957120 11060 4294967295 134512640 135094434 3221224448 3221223104 134561720 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/12868/statm): 11220 11060 145 145 0 11075 0 [pid=12868] vsize: 44880 Current children cumulated CPU time (s) 269.32 Current children cumulated vsize (Kb) 47004 [startup+280.034 s] Raw data (loadavg): 0.99 0.97 0.94 2/57 12868 Raw data (/proc/12864/stat): 12864 (minisat+_script) S 12863 12864 5929 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843588559 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/12864/statm): 531 226 485 147 0 384 0 [pid=12864] vsize: 2124 Raw data (/proc/12868/stat): 12868 (minisat+_64-bit) R 12864 12864 5929 0 -1 0 11745 0 0 0 27863 64 0 0 25 0 1 0 1843588564 47718400 11430 4294967295 134512640 135094434 3221224448 3221223104 134558007 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/12868/statm): 11650 11430 145 145 0 11505 0 [pid=12868] vsize: 46600 Current children cumulated CPU time (s) 279.28 Current children cumulated vsize (Kb) 48724 [startup+290.035 s] Raw data (loadavg): 0.99 0.97 0.94 2/57 12868 Raw data (/proc/12864/stat): 12864 (minisat+_script) S 12863 12864 5929 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843588559 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/12864/statm): 531 226 485 147 0 384 0 [pid=12864] vsize: 2124 Raw data (/proc/12868/stat): 12868 (minisat+_64-bit) R 12864 12864 5929 0 -1 0 12124 0 0 0 28857 67 0 0 25 0 1 0 1843588564 49258496 11809 4294967295 134512640 135094434 3221224448 3221223104 134557900 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/12868/statm): 12026 11809 145 145 0 11881 0 [pid=12868] vsize: 48104 Current children cumulated CPU time (s) 289.25 Current children cumulated vsize (Kb) 50228 [startup+300.036 s] Raw data (loadavg): 0.99 0.97 0.94 2/57 12868 Raw data (/proc/12864/stat): 12864 (minisat+_script) S 12863 12864 5929 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843588559 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/12864/statm): 531 226 485 147 0 384 0 [pid=12864] vsize: 2124 Raw data (/proc/12868/stat): 12868 (minisat+_64-bit) R 12864 12864 5929 0 -1 0 12481 0 0 0 29849 71 0 0 25 0 1 0 1843588564 50708480 12166 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/12868/statm): 12380 12166 145 145 0 12235 0 [pid=12868] vsize: 49520 Current children cumulated CPU time (s) 299.21 Current children cumulated vsize (Kb) 51644 [startup+310.037 s] Raw data (loadavg): 0.99 0.97 0.94 2/57 12868 Raw data (/proc/12864/stat): 12864 (minisat+_script) S 12863 12864 5929 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843588559 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/12864/statm): 531 226 485 147 0 384 0 [pid=12864] vsize: 2124 Raw data (/proc/12868/stat): 12868 (minisat+_64-bit) R 12864 12864 5929 0 -1 0 12844 0 0 0 30843 73 0 0 25 0 1 0 1843588564 51879936 12454 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/12868/statm): 12666 12454 145 145 0 12521 0 [pid=12868] vsize: 50664 Current children cumulated CPU time (s) 309.17 Current children cumulated vsize (Kb) 52788 [startup+320.038 s] Raw data (loadavg): 0.99 0.97 0.94 2/57 12868 Raw data (/proc/12864/stat): 12864 (minisat+_script) S 12863 12864 5929 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843588559 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/12864/statm): 531 226 485 147 0 384 0 [pid=12864] vsize: 2124 Raw data (/proc/12868/stat): 12868 (minisat+_64-bit) R 12864 12864 5929 0 -1 0 13128 0 0 0 31839 75 0 0 25 0 1 0 1843588564 53035008 12738 4294967295 134512640 135094434 3221224448 3221223104 134557948 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/12868/statm): 12948 12738 145 145 0 12803 0 [pid=12868] vsize: 51792 Current children cumulated CPU time (s) 319.15 Current children cumulated vsize (Kb) 53916 [startup+330.039 s] Raw data (loadavg): 0.99 0.97 0.94 2/57 12868 Raw data (/proc/12864/stat): 12864 (minisat+_script) S 12863 12864 5929 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843588559 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/12864/statm): 531 226 485 147 0 384 0 [pid=12864] vsize: 2124 Raw data (/proc/12868/stat): 12868 (minisat+_64-bit) R 12864 12864 5929 0 -1 0 13467 0 0 0 32833 78 0 0 25 0 1 0 1843588564 54415360 13077 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/12868/statm): 13285 13077 145 145 0 13140 0 [pid=12868] vsize: 53140 Current children cumulated CPU time (s) 329.12 Current children cumulated vsize (Kb) 55264 [startup+340.04 s] Raw data (loadavg): 0.99 0.97 0.94 2/57 12868 Raw data (/proc/12864/stat): 12864 (minisat+_script) S 12863 12864 5929 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843588559 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/12864/statm): 531 226 485 147 0 384 0 [pid=12864] vsize: 2124 Raw data (/proc/12868/stat): 12868 (minisat+_64-bit) R 12864 12864 5929 0 -1 0 13888 0 0 0 33826 80 0 0 25 0 1 0 1843588564 56127488 13498 4294967295 134512640 135094434 3221224448 3221223040 134556826 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/12868/statm): 13703 13498 145 145 0 13558 0 [pid=12868] vsize: 54812 Current children cumulated CPU time (s) 339.07 Current children cumulated vsize (Kb) 56936 [startup+350.041 s] Raw data (loadavg): 0.99 0.97 0.94 2/57 12868 Raw data (/proc/12864/stat): 12864 (minisat+_script) S 12863 12864 5929 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843588559 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/12864/statm): 531 226 485 147 0 384 0 [pid=12864] vsize: 2124 Raw data (/proc/12868/stat): 12868 (minisat+_64-bit) R 12864 12864 5929 0 -1 0 14189 0 0 0 34822 82 0 0 25 0 1 0 1843588564 57352192 13799 4294967295 134512640 135094434 3221224448 3221223076 134557564 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/12868/statm): 14002 13799 145 145 0 13857 0 [pid=12868] vsize: 56008 Current children cumulated CPU time (s) 349.05 Current children cumulated vsize (Kb) 58132 [startup+360.042 s] Raw data (loadavg): 0.99 0.97 0.94 2/57 12868 Raw data (/proc/12864/stat): 12864 (minisat+_script) S 12863 12864 5929 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843588559 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/12864/statm): 531 226 485 147 0 384 0 [pid=12864] vsize: 2124 Raw data (/proc/12868/stat): 12868 (minisat+_64-bit) R 12864 12864 5929 0 -1 0 14607 0 0 0 35815 85 0 0 25 0 1 0 1843588564 59056128 14217 4294967295 134512640 135094434 3221224448 3221223040 134557180 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/12868/statm): 14418 14217 145 145 0 14273 0 [pid=12868] vsize: 57672 Current children cumulated CPU time (s) 359.01 Current children cumulated vsize (Kb) 59796 [startup+370.042 s] Raw data (loadavg): 0.99 0.97 0.94 2/57 12868 Raw data (/proc/12864/stat): 12864 (minisat+_script) S 12863 12864 5929 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843588559 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/12864/statm): 531 226 485 147 0 384 0 [pid=12864] vsize: 2124 Raw data (/proc/12868/stat): 12868 (minisat+_64-bit) R 12864 12864 5929 0 -1 0 15001 0 0 0 36809 87 0 0 25 0 1 0 1843588564 60657664 14611 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/12868/statm): 14809 14611 145 145 0 14664 0 [pid=12868] vsize: 59236 Current children cumulated CPU time (s) 368.97 Current children cumulated vsize (Kb) 61360 [startup+380.043 s] Raw data (loadavg): 0.99 0.97 0.94 2/57 12868 Raw data (/proc/12864/stat): 12864 (minisat+_script) S 12863 12864 5929 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843588559 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/12864/statm): 531 226 485 147 0 384 0 [pid=12864] vsize: 2124 Raw data (/proc/12868/stat): 12868 (minisat+_64-bit) R 12864 12864 5929 0 -1 0 15347 0 0 0 37802 91 0 0 25 0 1 0 1843588564 62066688 14957 4294967295 134512640 135094434 3221224448 3221223120 134556317 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/12868/statm): 15153 14957 145 145 0 15008 0 [pid=12868] vsize: 60612 Current children cumulated CPU time (s) 378.94 Current children cumulated vsize (Kb) 62736 [startup+390.044 s] Raw data (loadavg): 0.99 0.97 0.94 2/57 12868 Raw data (/proc/12864/stat): 12864 (minisat+_script) S 12863 12864 5929 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843588559 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/12864/statm): 531 226 485 147 0 384 0 [pid=12864] vsize: 2124 Raw data (/proc/12868/stat): 12868 (minisat+_64-bit) R 12864 12864 5929 0 -1 0 15726 0 0 0 38795 93 0 0 25 0 1 0 1843588564 63606784 15336 4294967295 134512640 135094434 3221224448 3221223040 134556941 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/12868/statm): 15529 15336 145 145 0 15384 0 [pid=12868] vsize: 62116 Current children cumulated CPU time (s) 388.89 Current children cumulated vsize (Kb) 64240 [startup+400.046 s] Raw data (loadavg): 0.99 0.97 0.94 2/57 12868 Raw data (/proc/12864/stat): 12864 (minisat+_script) S 12863 12864 5929 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843588559 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/12864/statm): 531 226 485 147 0 384 0 [pid=12864] vsize: 2124 Raw data (/proc/12868/stat): 12868 (minisat+_64-bit) R 12864 12864 5929 0 -1 0 16141 0 0 0 39788 96 0 0 25 0 1 0 1843588564 65298432 15751 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/12868/statm): 15942 15751 145 145 0 15797 0 [pid=12868] vsize: 63768 Current children cumulated CPU time (s) 398.85 Current children cumulated vsize (Kb) 65892 [startup+410.047 s] Raw data (loadavg): 0.99 0.97 0.94 2/57 12868 Raw data (/proc/12864/stat): 12864 (minisat+_script) S 12863 12864 5929 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843588559 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/12864/statm): 531 226 485 147 0 384 0 [pid=12864] vsize: 2124 Raw data (/proc/12868/stat): 12868 (minisat+_64-bit) R 12864 12864 5929 0 -1 0 16488 0 0 0 40783 98 0 0 25 0 1 0 1843588564 66711552 16098 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/12868/statm): 16287 16098 145 145 0 16142 0 [pid=12868] vsize: 65148 Current children cumulated CPU time (s) 408.82 Current children cumulated vsize (Kb) 67272 [startup+420.047 s] Raw data (loadavg): 0.99 0.97 0.94 2/57 12868 Raw data (/proc/12864/stat): 12864 (minisat+_script) S 12863 12864 5929 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843588559 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/12864/statm): 531 226 485 147 0 384 0 [pid=12864] vsize: 2124 Raw data (/proc/12868/stat): 12868 (minisat+_64-bit) R 12864 12864 5929 0 -1 0 16788 0 0 0 41777 100 0 0 25 0 1 0 1843588564 67932160 16398 4294967295 134512640 135094434 3221224448 3221223104 134558016 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/12868/statm): 16585 16398 145 145 0 16440 0 [pid=12868] vsize: 66340 Current children cumulated CPU time (s) 418.78 Current children cumulated vsize (Kb) 68464 [startup+430.048 s] Raw data (loadavg): 0.99 0.97 0.94 2/57 12868 Raw data (/proc/12864/stat): 12864 (minisat+_script) S 12863 12864 5929 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843588559 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/12864/statm): 531 226 485 147 0 384 0 [pid=12864] vsize: 2124 Raw data (/proc/12868/stat): 12868 (minisat+_64-bit) R 12864 12864 5929 0 -1 0 17116 0 0 0 42773 101 0 0 25 0 1 0 1843588564 69267456 16726 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/12868/statm): 16911 16726 145 145 0 16766 0 [pid=12868] vsize: 67644 Current children cumulated CPU time (s) 428.75 Current children cumulated vsize (Kb) 69768 [startup+440.049 s] Raw data (loadavg): 0.99 0.97 0.94 2/57 12868 Raw data (/proc/12864/stat): 12864 (minisat+_script) S 12863 12864 5929 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843588559 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/12864/statm): 531 226 485 147 0 384 0 [pid=12864] vsize: 2124 Raw data (/proc/12868/stat): 12868 (minisat+_64-bit) R 12864 12864 5929 0 -1 0 17433 0 0 0 43767 104 0 0 25 0 1 0 1843588564 70553600 17043 4294967295 134512640 135094434 3221224448 3221223104 134558159 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/12868/statm): 17225 17043 145 145 0 17080 0 [pid=12868] vsize: 68900 Current children cumulated CPU time (s) 438.72 Current children cumulated vsize (Kb) 71024 [startup+450.05 s] Raw data (loadavg): 0.99 0.97 0.94 2/57 12868 Raw data (/proc/12864/stat): 12864 (minisat+_script) S 12863 12864 5929 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843588559 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/12864/statm): 531 226 485 147 0 384 0 [pid=12864] vsize: 2124 Raw data (/proc/12868/stat): 12868 (minisat+_64-bit) R 12864 12864 5929 0 -1 0 17810 0 0 0 44760 107 0 0 25 0 1 0 1843588564 72089600 17420 4294967295 134512640 135094434 3221224448 3221223040 134557180 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/12868/statm): 17600 17420 145 145 0 17455 0 [pid=12868] vsize: 70400 Current children cumulated CPU time (s) 448.68 Current children cumulated vsize (Kb) 72524 [startup+460.052 s] Raw data (loadavg): 0.99 0.97 0.94 2/57 12868 Raw data (/proc/12864/stat): 12864 (minisat+_script) S 12863 12864 5929 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843588559 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/12864/statm): 531 226 485 147 0 384 0 [pid=12864] vsize: 2124 Raw data (/proc/12868/stat): 12868 (minisat+_64-bit) R 12864 12864 5929 0 -1 0 18179 0 0 0 45752 110 0 0 25 0 1 0 1843588564 73592832 17789 4294967295 134512640 135094434 3221224448 3221223104 134558178 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/12868/statm): 17967 17789 145 145 0 17822 0 [pid=12868] vsize: 71868 Current children cumulated CPU time (s) 458.63 Current children cumulated vsize (Kb) 73992 [startup+470.051 s] Raw data (loadavg): 0.99 0.97 0.94 2/57 12868 Raw data (/proc/12864/stat): 12864 (minisat+_script) S 12863 12864 5929 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843588559 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/12864/statm): 531 226 485 147 0 384 0 [pid=12864] vsize: 2124 Raw data (/proc/12868/stat): 12868 (minisat+_64-bit) R 12864 12864 5929 0 -1 0 18444 0 0 0 46748 112 0 0 25 0 1 0 1843588564 74674176 18054 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/12868/statm): 18231 18054 145 145 0 18086 0 [pid=12868] vsize: 72924 Current children cumulated CPU time (s) 468.61 Current children cumulated vsize (Kb) 75048 [startup+480.052 s] Raw data (loadavg): 0.99 0.97 0.94 2/57 12868 Raw data (/proc/12864/stat): 12864 (minisat+_script) S 12863 12864 5929 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843588559 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/12864/statm): 531 226 485 147 0 384 0 [pid=12864] vsize: 2124 Raw data (/proc/12868/stat): 12868 (minisat+_64-bit) T 12864 12864 5929 0 -1 0 18799 0 0 0 47740 116 0 0 25 0 1 0 1843588564 76124160 18409 4294967295 134512640 135094434 3221224448 3221222812 134870330 0 0 5 16386 3222434794 0 0 17 0 0 0 Raw data (/proc/12868/statm): 18585 18409 145 145 0 18440 0 [pid=12868] vsize: 74340 Current children cumulated CPU time (s) 478.57 Current children cumulated vsize (Kb) 76464 [startup+490.053 s] Raw data (loadavg): 0.99 0.97 0.94 2/57 12868 Raw data (/proc/12864/stat): 12864 (minisat+_script) S 12863 12864 5929 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843588559 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/12864/statm): 531 226 485 147 0 384 0 [pid=12864] vsize: 2124 Raw data (/proc/12868/stat): 12868 (minisat+_64-bit) R 12864 12864 5929 0 -1 0 19136 0 0 0 48734 120 0 0 25 0 1 0 1843588564 77496320 18746 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/12868/statm): 18920 18746 145 145 0 18775 0 [pid=12868] vsize: 75680 Current children cumulated CPU time (s) 488.55 Current children cumulated vsize (Kb) 77804 [startup+500.055 s] Raw data (loadavg): 0.99 0.97 0.94 2/57 12868 Raw data (/proc/12864/stat): 12864 (minisat+_script) S 12863 12864 5929 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843588559 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/12864/statm): 531 226 485 147 0 384 0 [pid=12864] vsize: 2124 Raw data (/proc/12868/stat): 12868 (minisat+_64-bit) R 12864 12864 5929 0 -1 0 19406 0 0 0 49729 121 0 0 25 0 1 0 1843588564 78594048 19016 4294967295 134512640 135094434 3221224448 3221223120 134555821 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/12868/statm): 19188 19016 145 145 0 19043 0 [pid=12868] vsize: 76752 Current children cumulated CPU time (s) 498.51 Current children cumulated vsize (Kb) 78876 [startup+510.056 s] Raw data (loadavg): 0.99 0.97 0.94 2/57 12868 Raw data (/proc/12864/stat): 12864 (minisat+_script) S 12863 12864 5929 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843588559 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/12864/statm): 531 226 485 147 0 384 0 [pid=12864] vsize: 2124 Raw data (/proc/12868/stat): 12868 (minisat+_64-bit) R 12864 12864 5929 0 -1 0 19736 0 0 0 50724 124 0 0 25 0 1 0 1843588564 79937536 19346 4294967295 134512640 135094434 3221224448 3221223040 134556894 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/12868/statm): 19516 19346 145 145 0 19371 0 [pid=12868] vsize: 78064 Current children cumulated CPU time (s) 508.49 Current children cumulated vsize (Kb) 80188 [startup+520.057 s] Raw data (loadavg): 0.99 0.97 0.94 2/57 12868 Raw data (/proc/12864/stat): 12864 (minisat+_script) S 12863 12864 5929 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843588559 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/12864/statm): 531 226 485 147 0 384 0 [pid=12864] vsize: 2124 Raw data (/proc/12868/stat): 12868 (minisat+_64-bit) R 12864 12864 5929 0 -1 0 20033 0 0 0 51719 127 0 0 25 0 1 0 1843588564 81145856 19643 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/12868/statm): 19811 19643 145 145 0 19666 0 [pid=12868] vsize: 79244 Current children cumulated CPU time (s) 518.47 Current children cumulated vsize (Kb) 81368 [startup+530.057 s] Raw data (loadavg): 0.99 0.97 0.94 2/57 12868 Raw data (/proc/12864/stat): 12864 (minisat+_script) S 12863 12864 5929 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843588559 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/12864/statm): 531 226 485 147 0 384 0 [pid=12864] vsize: 2124 Raw data (/proc/12868/stat): 12868 (minisat+_64-bit) R 12864 12864 5929 0 -1 0 20327 0 0 0 52713 129 0 0 25 0 1 0 1843588564 82345984 19937 4294967295 134512640 135094434 3221224448 3221223104 134558013 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/12868/statm): 20104 19937 145 145 0 19959 0 [pid=12868] vsize: 80416 Current children cumulated CPU time (s) 528.43 Current children cumulated vsize (Kb) 82540 [startup+540.058 s] Raw data (loadavg): 0.99 0.97 0.94 1/57 12868 Raw data (/proc/12864/stat): 12864 (minisat+_script) S 12863 12864 5929 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843588559 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/12864/statm): 531 226 485 147 0 384 0 [pid=12864] vsize: 2124 Raw data (/proc/12868/stat): 12868 (minisat+_64-bit) T 12864 12864 5929 0 -1 0 20682 0 0 0 53706 132 0 0 25 0 1 0 1843588564 83791872 20292 4294967295 134512640 135094434 3221224448 3221222828 134870330 0 0 5 16386 3222434794 0 0 17 0 0 0 Raw data (/proc/12868/statm): 20457 20292 145 145 0 20312 0 [pid=12868] vsize: 81828 Current children cumulated CPU time (s) 538.39 Current children cumulated vsize (Kb) 83952 [startup+550.059 s] Raw data (loadavg): 0.99 0.97 0.94 2/57 12868 Raw data (/proc/12864/stat): 12864 (minisat+_script) S 12863 12864 5929 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843588559 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/12864/statm): 531 226 485 147 0 384 0 [pid=12864] vsize: 2124 Raw data (/proc/12868/stat): 12868 (minisat+_64-bit) R 12864 12864 5929 0 -1 0 20974 0 0 0 54701 134 0 0 25 0 1 0 1843588564 84979712 20584 4294967295 134512640 135094434 3221224448 3221223104 134557950 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/12868/statm): 20747 20584 145 145 0 20602 0 [pid=12868] vsize: 82988 Current children cumulated CPU time (s) 548.36 Current children cumulated vsize (Kb) 85112 [startup+560.06 s] Raw data (loadavg): 0.99 0.97 0.94 2/57 12868 Raw data (/proc/12864/stat): 12864 (minisat+_script) S 12863 12864 5929 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843588559 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/12864/statm): 531 226 485 147 0 384 0 [pid=12864] vsize: 2124 Raw data (/proc/12868/stat): 12868 (minisat+_64-bit) R 12864 12864 5929 0 -1 0 21241 0 0 0 55697 136 0 0 25 0 1 0 1843588564 86065152 20851 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/12868/statm): 21012 20851 145 145 0 20867 0 [pid=12868] vsize: 84048 Current children cumulated CPU time (s) 558.34 Current children cumulated vsize (Kb) 86172 [startup+570.061 s] Raw data (loadavg): 0.99 0.97 0.94 2/57 12868 Raw data (/proc/12864/stat): 12864 (minisat+_script) S 12863 12864 5929 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843588559 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/12864/statm): 531 226 485 147 0 384 0 [pid=12864] vsize: 2124 Raw data (/proc/12868/stat): 12868 (minisat+_64-bit) R 12864 12864 5929 0 -1 0 21494 0 0 0 56692 139 0 0 25 0 1 0 1843588564 87621632 21104 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/12868/statm): 21392 21104 145 145 0 21247 0 [pid=12868] vsize: 85568 Current children cumulated CPU time (s) 568.32 Current children cumulated vsize (Kb) 87692 [startup+580.061 s] Raw data (loadavg): 0.99 0.97 0.94 2/57 12868 Raw data (/proc/12864/stat): 12864 (minisat+_script) S 12863 12864 5929 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843588559 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/12864/statm): 531 226 485 147 0 384 0 [pid=12864] vsize: 2124 Raw data (/proc/12868/stat): 12868 (minisat+_64-bit) R 12864 12864 5929 0 -1 0 21759 0 0 0 57688 140 0 0 25 0 1 0 1843588564 88698880 21369 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/12868/statm): 21655 21369 145 145 0 21510 0 [pid=12868] vsize: 86620 Current children cumulated CPU time (s) 578.29 Current children cumulated vsize (Kb) 88744 [startup+590.062 s] Raw data (loadavg): 0.99 0.97 0.94 2/57 12868 Raw data (/proc/12864/stat): 12864 (minisat+_script) S 12863 12864 5929 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843588559 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/12864/statm): 531 226 485 147 0 384 0 [pid=12864] vsize: 2124 Raw data (/proc/12868/stat): 12868 (minisat+_64-bit) R 12864 12864 5929 0 -1 0 22037 0 0 0 58683 142 0 0 25 0 1 0 1843588564 89829376 21647 4294967295 134512640 135094434 3221224448 3221223104 134558213 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/12868/statm): 21931 21647 145 145 0 21786 0 [pid=12868] vsize: 87724 Current children cumulated CPU time (s) 588.26 Current children cumulated vsize (Kb) 89848 [startup+600.064 s] Raw data (loadavg): 0.99 0.97 0.94 2/57 12868 Raw data (/proc/12864/stat): 12864 (minisat+_script) S 12863 12864 5929 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843588559 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/12864/statm): 531 226 485 147 0 384 0 [pid=12864] vsize: 2124 Raw data (/proc/12868/stat): 12868 (minisat+_64-bit) R 12864 12864 5929 0 -1 0 22319 0 0 0 59679 143 0 0 25 0 1 0 1843588564 90980352 21929 4294967295 134512640 135094434 3221224448 3221223104 134557835 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/12868/statm): 22212 21929 145 145 0 22067 0 [pid=12868] vsize: 88848 Current children cumulated CPU time (s) 598.23 Current children cumulated vsize (Kb) 90972 [startup+610.065 s] Raw data (loadavg): 0.99 0.97 0.94 2/57 12868 Raw data (/proc/12864/stat): 12864 (minisat+_script) S 12863 12864 5929 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843588559 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/12864/statm): 531 226 485 147 0 384 0 [pid=12864] vsize: 2124 Raw data (/proc/12868/stat): 12868 (minisat+_64-bit) R 12864 12864 5929 0 -1 0 22608 0 0 0 60674 146 0 0 25 0 1 0 1843588564 92155904 22218 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/12868/statm): 22499 22218 145 145 0 22354 0 [pid=12868] vsize: 89996 Current children cumulated CPU time (s) 608.21 Current children cumulated vsize (Kb) 92120 [startup+620.066 s] Raw data (loadavg): 0.99 0.97 0.94 2/57 12868 Raw data (/proc/12864/stat): 12864 (minisat+_script) S 12863 12864 5929 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843588559 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/12864/statm): 531 226 485 147 0 384 0 [pid=12864] vsize: 2124 Raw data (/proc/12868/stat): 12868 (minisat+_64-bit) R 12864 12864 5929 0 -1 0 22885 0 0 0 61670 148 0 0 25 0 1 0 1843588564 93286400 22495 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/12868/statm): 22775 22495 145 145 0 22630 0 [pid=12868] vsize: 91100 Current children cumulated CPU time (s) 618.19 Current children cumulated vsize (Kb) 93224 [startup+630.066 s] Raw data (loadavg): 0.99 0.97 0.94 2/57 12868 Raw data (/proc/12864/stat): 12864 (minisat+_script) S 12863 12864 5929 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843588559 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/12864/statm): 531 226 485 147 0 384 0 [pid=12864] vsize: 2124 Raw data (/proc/12868/stat): 12868 (minisat+_64-bit) R 12864 12864 5929 0 -1 0 23231 0 0 0 62663 151 0 0 25 0 1 0 1843588564 94699520 22841 4294967295 134512640 135094434 3221224448 3221223040 134557227 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/12868/statm): 23120 22841 145 145 0 22975 0 [pid=12868] vsize: 92480 Current children cumulated CPU time (s) 628.15 Current children cumulated vsize (Kb) 94604 [startup+640.067 s] Raw data (loadavg): 0.99 0.97 0.94 2/57 12868 Raw data (/proc/12864/stat): 12864 (minisat+_script) S 12863 12864 5929 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843588559 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/12864/statm): 531 226 485 147 0 384 0 [pid=12864] vsize: 2124 Raw data (/proc/12868/stat): 12868 (minisat+_64-bit) R 12864 12864 5929 0 -1 0 23640 0 0 0 63656 154 0 0 25 0 1 0 1843588564 96370688 23250 4294967295 134512640 135094434 3221224448 3221223104 134558208 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/12868/statm): 23528 23250 145 145 0 23383 0 [pid=12868] vsize: 94112 Current children cumulated CPU time (s) 638.11 Current children cumulated vsize (Kb) 96236 [startup+650.068 s] Raw data (loadavg): 0.99 0.97 0.94 2/57 12868 Raw data (/proc/12864/stat): 12864 (minisat+_script) S 12863 12864 5929 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843588559 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/12864/statm): 531 226 485 147 0 384 0 [pid=12864] vsize: 2124 Raw data (/proc/12868/stat): 12868 (minisat+_64-bit) R 12864 12864 5929 0 -1 0 23927 0 0 0 64651 156 0 0 25 0 1 0 1843588564 97538048 23537 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/12868/statm): 23813 23537 145 145 0 23668 0 [pid=12868] vsize: 95252 Current children cumulated CPU time (s) 648.08 Current children cumulated vsize (Kb) 97376 [startup+660.069 s] Raw data (loadavg): 0.99 0.97 0.94 2/57 12868 Raw data (/proc/12864/stat): 12864 (minisat+_script) S 12863 12864 5929 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843588559 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/12864/statm): 531 226 485 147 0 384 0 [pid=12864] vsize: 2124 Raw data (/proc/12868/stat): 12868 (minisat+_64-bit) R 12864 12864 5929 0 -1 0 24199 0 0 0 65646 158 0 0 25 0 1 0 1843588564 98648064 23809 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/12868/statm): 24084 23809 145 145 0 23939 0 [pid=12868] vsize: 96336 Current children cumulated CPU time (s) 658.05 Current children cumulated vsize (Kb) 98460 [startup+670.07 s] Raw data (loadavg): 0.99 0.97 0.94 2/57 12868 Raw data (/proc/12864/stat): 12864 (minisat+_script) S 12863 12864 5929 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843588559 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/12864/statm): 531 226 485 147 0 384 0 [pid=12864] vsize: 2124 Raw data (/proc/12868/stat): 12868 (minisat+_64-bit) R 12864 12864 5929 0 -1 0 24504 0 0 0 66640 161 0 0 25 0 1 0 1843588564 99889152 24114 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/12868/statm): 24387 24114 145 145 0 24242 0 [pid=12868] vsize: 97548 Current children cumulated CPU time (s) 668.02 Current children cumulated vsize (Kb) 99672 [startup+680.07 s] Raw data (loadavg): 0.99 0.97 0.94 2/57 12868 Raw data (/proc/12864/stat): 12864 (minisat+_script) S 12863 12864 5929 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843588559 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/12864/statm): 531 226 485 147 0 384 0 [pid=12864] vsize: 2124 Raw data (/proc/12868/stat): 12868 (minisat+_64-bit) R 12864 12864 5929 0 -1 0 24811 0 0 0 67634 163 0 0 25 0 1 0 1843588564 101142528 24421 4294967295 134512640 135094434 3221224448 3221223104 134558235 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/12868/statm): 24693 24421 145 145 0 24548 0 [pid=12868] vsize: 98772 Current children cumulated CPU time (s) 677.98 Current children cumulated vsize (Kb) 100896 [startup+690.071 s] Raw data (loadavg): 0.99 0.97 0.94 2/57 12868 Raw data (/proc/12864/stat): 12864 (minisat+_script) S 12863 12864 5929 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843588559 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/12864/statm): 531 226 485 147 0 384 0 [pid=12864] vsize: 2124 Raw data (/proc/12868/stat): 12868 (minisat+_64-bit) R 12864 12864 5929 0 -1 0 25158 0 0 0 68627 166 0 0 25 0 1 0 1843588564 102555648 24768 4294967295 134512640 135094434 3221224448 3221223040 134557219 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/12868/statm): 25038 24768 145 145 0 24893 0 [pid=12868] vsize: 100152 Current children cumulated CPU time (s) 687.94 Current children cumulated vsize (Kb) 102276 [startup+700.073 s] Raw data (loadavg): 0.99 0.97 0.94 2/57 12868 Raw data (/proc/12864/stat): 12864 (minisat+_script) S 12863 12864 5929 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843588559 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/12864/statm): 531 226 485 147 0 384 0 [pid=12864] vsize: 2124 Raw data (/proc/12868/stat): 12868 (minisat+_64-bit) R 12864 12864 5929 0 -1 0 25485 0 0 0 69622 167 0 0 25 0 1 0 1843588564 103890944 25095 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/12868/statm): 25364 25095 145 145 0 25219 0 [pid=12868] vsize: 101456 Current children cumulated CPU time (s) 697.9 Current children cumulated vsize (Kb) 103580 [startup+710.074 s] Raw data (loadavg): 0.99 0.97 0.94 2/57 12868 Raw data (/proc/12864/stat): 12864 (minisat+_script) S 12863 12864 5929 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843588559 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/12864/statm): 531 226 485 147 0 384 0 [pid=12864] vsize: 2124 Raw data (/proc/12868/stat): 12868 (minisat+_64-bit) R 12864 12864 5929 0 -1 0 25801 0 0 0 70618 168 0 0 25 0 1 0 1843588564 105181184 25411 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/12868/statm): 25679 25411 145 145 0 25534 0 [pid=12868] vsize: 102716 Current children cumulated CPU time (s) 707.87 Current children cumulated vsize (Kb) 104840 [startup+720.075 s] Raw data (loadavg): 0.99 0.97 0.94 2/57 12868 Raw data (/proc/12864/stat): 12864 (minisat+_script) S 12863 12864 5929 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843588559 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/12864/statm): 531 226 485 147 0 384 0 [pid=12864] vsize: 2124 Raw data (/proc/12868/stat): 12868 (minisat+_64-bit) R 12864 12864 5929 0 -1 0 26074 0 0 0 71613 170 0 0 25 0 1 0 1843588564 106295296 25684 4294967295 134512640 135094434 3221224448 3221223040 134557416 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/12868/statm): 25951 25684 145 145 0 25806 0 [pid=12868] vsize: 103804 Current children cumulated CPU time (s) 717.84 Current children cumulated vsize (Kb) 105928 [startup+730.076 s] Raw data (loadavg): 0.99 0.97 0.94 1/57 12868 Raw data (/proc/12864/stat): 12864 (minisat+_script) S 12863 12864 5929 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843588559 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/12864/statm): 531 226 485 147 0 384 0 [pid=12864] vsize: 2124 Raw data (/proc/12868/stat): 12868 (minisat+_64-bit) T 12864 12864 5929 0 -1 0 26371 0 0 0 72607 172 0 0 25 0 1 0 1843588564 107507712 25981 4294967295 134512640 135094434 3221224448 3221222828 134870330 0 0 5 16386 3222434794 0 0 17 0 0 0 Raw data (/proc/12868/statm): 26247 25981 145 145 0 26102 0 [pid=12868] vsize: 104988 Current children cumulated CPU time (s) 727.8 Current children cumulated vsize (Kb) 107112 [startup+740.076 s] Raw data (loadavg): 0.99 0.97 0.94 2/57 12868 Raw data (/proc/12864/stat): 12864 (minisat+_script) S 12863 12864 5929 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843588559 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/12864/statm): 531 226 485 147 0 384 0 [pid=12864] vsize: 2124 Raw data (/proc/12868/stat): 12868 (minisat+_64-bit) R 12864 12864 5929 0 -1 0 26645 0 0 0 73603 174 0 0 25 0 1 0 1843588564 108621824 26255 4294967295 134512640 135094434 3221224448 3221223040 134557180 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/12868/statm): 26519 26255 145 145 0 26374 0 [pid=12868] vsize: 106076 Current children cumulated CPU time (s) 737.78 Current children cumulated vsize (Kb) 108200 [startup+750.077 s] Raw data (loadavg): 0.99 0.97 0.94 2/57 12868 Raw data (/proc/12864/stat): 12864 (minisat+_script) S 12863 12864 5929 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843588559 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/12864/statm): 531 226 485 147 0 384 0 [pid=12864] vsize: 2124 Raw data (/proc/12868/stat): 12868 (minisat+_64-bit) R 12864 12864 5929 0 -1 0 26911 0 0 0 74598 176 0 0 25 0 1 0 1843588564 109703168 26521 4294967295 134512640 135094434 3221224448 3221223040 134557413 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/12868/statm): 26783 26521 145 145 0 26638 0 [pid=12868] vsize: 107132 Current children cumulated CPU time (s) 747.75 Current children cumulated vsize (Kb) 109256 [startup+760.078 s] Raw data (loadavg): 0.99 0.97 0.94 2/57 12868 Raw data (/proc/12864/stat): 12864 (minisat+_script) S 12863 12864 5929 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843588559 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/12864/statm): 531 226 485 147 0 384 0 [pid=12864] vsize: 2124 Raw data (/proc/12868/stat): 12868 (minisat+_64-bit) R 12864 12864 5929 0 -1 0 27170 0 0 0 75595 177 0 0 25 0 1 0 1843588564 110759936 26780 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/12868/statm): 27041 26780 145 145 0 26896 0 [pid=12868] vsize: 108164 Current children cumulated CPU time (s) 757.73 Current children cumulated vsize (Kb) 110288 [startup+770.079 s] Raw data (loadavg): 0.99 0.97 0.94 2/57 12868 Raw data (/proc/12864/stat): 12864 (minisat+_script) S 12863 12864 5929 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843588559 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/12864/statm): 531 226 485 147 0 384 0 [pid=12864] vsize: 2124 Raw data (/proc/12868/stat): 12868 (minisat+_64-bit) R 12864 12864 5929 0 -1 0 27423 0 0 0 76591 179 0 0 25 0 1 0 1843588564 111788032 27033 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/12868/statm): 27292 27033 145 145 0 27147 0 [pid=12868] vsize: 109168 Current children cumulated CPU time (s) 767.71 Current children cumulated vsize (Kb) 111292 [startup+780.08 s] Raw data (loadavg): 0.99 0.97 0.94 2/57 12868 Raw data (/proc/12864/stat): 12864 (minisat+_script) S 12863 12864 5929 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843588559 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/12864/statm): 531 226 485 147 0 384 0 [pid=12864] vsize: 2124 Raw data (/proc/12868/stat): 12868 (minisat+_64-bit) R 12864 12864 5929 0 -1 0 27665 0 0 0 77586 181 0 0 25 0 1 0 1843588564 112775168 27275 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/12868/statm): 27533 27275 145 145 0 27388 0 [pid=12868] vsize: 110132 Current children cumulated CPU time (s) 777.68 Current children cumulated vsize (Kb) 112256 [startup+790.08 s] Raw data (loadavg): 0.99 0.97 0.94 2/57 12868 Raw data (/proc/12864/stat): 12864 (minisat+_script) S 12863 12864 5929 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843588559 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/12864/statm): 531 226 485 147 0 384 0 [pid=12864] vsize: 2124 Raw data (/proc/12868/stat): 12868 (minisat+_64-bit) R 12864 12864 5929 0 -1 0 27921 0 0 0 78581 184 0 0 25 0 1 0 1843588564 113819648 27531 4294967295 134512640 135094434 3221224448 3221223040 134557219 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/12868/statm): 27788 27531 145 145 0 27643 0 [pid=12868] vsize: 111152 Current children cumulated CPU time (s) 787.66 Current children cumulated vsize (Kb) 113276 [startup+800.082 s] Raw data (loadavg): 0.99 0.97 0.94 2/57 12868 Raw data (/proc/12864/stat): 12864 (minisat+_script) S 12863 12864 5929 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843588559 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/12864/statm): 531 226 485 147 0 384 0 [pid=12864] vsize: 2124 Raw data (/proc/12868/stat): 12868 (minisat+_64-bit) T 12864 12864 5929 0 -1 0 28255 0 0 0 79576 186 0 0 25 0 1 0 1843588564 115187712 27865 4294967295 134512640 135094434 3221224448 3221222828 134870330 0 0 5 16386 3222434794 0 0 17 0 0 0 Raw data (/proc/12868/statm): 28122 27865 145 145 0 27977 0 [pid=12868] vsize: 112488 Current children cumulated CPU time (s) 797.63 Current children cumulated vsize (Kb) 114612 [startup+810.083 s] Raw data (loadavg): 0.99 0.97 0.94 2/57 12868 Raw data (/proc/12864/stat): 12864 (minisat+_script) S 12863 12864 5929 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843588559 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/12864/statm): 531 226 485 147 0 384 0 [pid=12864] vsize: 2124 Raw data (/proc/12868/stat): 12868 (minisat+_64-bit) R 12864 12864 5929 0 -1 0 28530 0 0 0 80571 189 0 0 25 0 1 0 1843588564 116305920 28140 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/12868/statm): 28395 28140 145 145 0 28250 0 [pid=12868] vsize: 113580 Current children cumulated CPU time (s) 807.61 Current children cumulated vsize (Kb) 115704 [startup+820.084 s] Raw data (loadavg): 0.99 0.97 0.94 2/57 12868 Raw data (/proc/12864/stat): 12864 (minisat+_script) S 12863 12864 5929 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843588559 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/12864/statm): 531 226 485 147 0 384 0 [pid=12864] vsize: 2124 Raw data (/proc/12868/stat): 12868 (minisat+_64-bit) R 12864 12864 5929 0 -1 0 28805 0 0 0 81567 190 0 0 25 0 1 0 1843588564 117420032 28415 4294967295 134512640 135094434 3221224448 3221223104 134558159 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/12868/statm): 28667 28415 145 145 0 28522 0 [pid=12868] vsize: 114668 Current children cumulated CPU time (s) 817.58 Current children cumulated vsize (Kb) 116792 [startup+830.085 s] Raw data (loadavg): 0.99 0.97 0.94 2/57 12868 Raw data (/proc/12864/stat): 12864 (minisat+_script) S 12863 12864 5929 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843588559 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/12864/statm): 531 226 485 147 0 384 0 [pid=12864] vsize: 2124 Raw data (/proc/12868/stat): 12868 (minisat+_64-bit) R 12864 12864 5929 0 -1 0 29114 0 0 0 82561 193 0 0 25 0 1 0 1843588564 118685696 28724 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/12868/statm): 28976 28724 145 145 0 28831 0 [pid=12868] vsize: 115904 Current children cumulated CPU time (s) 827.55 Current children cumulated vsize (Kb) 118028 [startup+840.085 s] Raw data (loadavg): 0.99 0.97 0.94 2/57 12868 Raw data (/proc/12864/stat): 12864 (minisat+_script) S 12863 12864 5929 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843588559 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/12864/statm): 531 226 485 147 0 384 0 [pid=12864] vsize: 2124 Raw data (/proc/12868/stat): 12868 (minisat+_64-bit) R 12864 12864 5929 0 -1 0 29419 0 0 0 83556 195 0 0 25 0 1 0 1843588564 119926784 29029 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/12868/statm): 29279 29029 145 145 0 29134 0 [pid=12868] vsize: 117116 Current children cumulated CPU time (s) 837.52 Current children cumulated vsize (Kb) 119240 [startup+850.086 s] Raw data (loadavg): 0.99 0.97 0.94 2/57 12868 Raw data (/proc/12864/stat): 12864 (minisat+_script) S 12863 12864 5929 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843588559 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/12864/statm): 531 226 485 147 0 384 0 [pid=12864] vsize: 2124 Raw data (/proc/12868/stat): 12868 (minisat+_64-bit) R 12864 12864 5929 0 -1 0 29666 0 0 0 84552 197 0 0 25 0 1 0 1843588564 120930304 29276 4294967295 134512640 135094434 3221224448 3221223040 134556951 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/12868/statm): 29524 29276 145 145 0 29379 0 [pid=12868] vsize: 118096 Current children cumulated CPU time (s) 847.5 Current children cumulated vsize (Kb) 120220 [startup+860.087 s] Raw data (loadavg): 0.99 0.97 0.94 2/57 12868 Raw data (/proc/12864/stat): 12864 (minisat+_script) S 12863 12864 5929 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843588559 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/12864/statm): 531 226 485 147 0 384 0 [pid=12864] vsize: 2124 Raw data (/proc/12868/stat): 12868 (minisat+_64-bit) R 12864 12864 5929 0 -1 0 29958 0 0 0 85547 198 0 0 25 0 1 0 1843588564 122122240 29568 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/12868/statm): 29815 29568 145 145 0 29670 0 [pid=12868] vsize: 119260 Current children cumulated CPU time (s) 857.46 Current children cumulated vsize (Kb) 121384 [startup+870.088 s] Raw data (loadavg): 0.99 0.97 0.94 2/57 12868 Raw data (/proc/12864/stat): 12864 (minisat+_script) S 12863 12864 5929 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843588559 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/12864/statm): 531 226 485 147 0 384 0 [pid=12864] vsize: 2124 Raw data (/proc/12868/stat): 12868 (minisat+_64-bit) R 12864 12864 5929 0 -1 0 30282 0 0 0 86541 201 0 0 25 0 1 0 1843588564 123441152 29892 4294967295 134512640 135094434 3221224448 3221223040 134556812 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/12868/statm): 30137 29892 145 145 0 29992 0 [pid=12868] vsize: 120548 Current children cumulated CPU time (s) 867.43 Current children cumulated vsize (Kb) 122672 [startup+880.089 s] Raw data (loadavg): 0.99 0.97 0.94 2/57 12868 Raw data (/proc/12864/stat): 12864 (minisat+_script) S 12863 12864 5929 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843588559 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/12864/statm): 531 226 485 147 0 384 0 [pid=12864] vsize: 2124 Raw data (/proc/12868/stat): 12868 (minisat+_64-bit) R 12864 12864 5929 0 -1 0 30673 0 0 0 87536 202 0 0 25 0 1 0 1843588564 124731392 30207 4294967295 134512640 135094434 3221224448 3221223236 134553497 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/12868/statm): 30452 30207 145 145 0 30307 0 [pid=12868] vsize: 121808 Current children cumulated CPU time (s) 877.39 Current children cumulated vsize (Kb) 123932 [startup+890.089 s] Raw data (loadavg): 0.99 0.97 0.94 2/57 12868 Raw data (/proc/12864/stat): 12864 (minisat+_script) S 12863 12864 5929 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843588559 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/12864/statm): 531 226 485 147 0 384 0 [pid=12864] vsize: 2124 Raw data (/proc/12868/stat): 12868 (minisat+_64-bit) R 12864 12864 5929 0 -1 0 30673 0 0 0 88536 202 0 0 25 0 1 0 1843588564 124731392 30207 4294967295 134512640 135094434 3221224448 3221223136 134554731 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/12868/statm): 30452 30207 145 145 0 30307 0 [pid=12868] vsize: 121808 Current children cumulated CPU time (s) 887.39 Current children cumulated vsize (Kb) 123932 [startup+900.091 s] Raw data (loadavg): 0.99 0.97 0.94 2/57 12868 Raw data (/proc/12864/stat): 12864 (minisat+_script) S 12863 12864 5929 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843588559 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/12864/statm): 531 226 485 147 0 384 0 [pid=12864] vsize: 2124 Raw data (/proc/12868/stat): 12868 (minisat+_64-bit) R 12864 12864 5929 0 -1 0 30673 0 0 0 89535 203 0 0 25 0 1 0 1843588564 124731392 30207 4294967295 134512640 135094434 3221224448 3221223040 134551873 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/12868/statm): 30452 30207 145 145 0 30307 0 [pid=12868] vsize: 121808 Current children cumulated CPU time (s) 897.39 Current children cumulated vsize (Kb) 123932 [startup+910.093 s] Raw data (loadavg): 0.99 0.97 0.94 2/57 12868 Raw data (/proc/12864/stat): 12864 (minisat+_script) S 12863 12864 5929 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843588559 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/12864/statm): 531 226 485 147 0 384 0 [pid=12864] vsize: 2124 Raw data (/proc/12868/stat): 12868 (minisat+_64-bit) R 12864 12864 5929 0 -1 0 30673 0 0 0 90536 203 0 0 25 0 1 0 1843588564 124731392 30207 4294967295 134512640 135094434 3221224448 3221223040 134557208 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/12868/statm): 30452 30207 145 145 0 30307 0 [pid=12868] vsize: 121808 Current children cumulated CPU time (s) 907.4 Current children cumulated vsize (Kb) 123932 [startup+920.094 s] Raw data (loadavg): 0.99 0.97 0.94 2/57 12868 Raw data (/proc/12864/stat): 12864 (minisat+_script) S 12863 12864 5929 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843588559 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/12864/statm): 531 226 485 147 0 384 0 [pid=12864] vsize: 2124 Raw data (/proc/12868/stat): 12868 (minisat+_64-bit) R 12864 12864 5929 0 -1 0 30673 0 0 0 91536 203 0 0 25 0 1 0 1843588564 124731392 30207 4294967295 134512640 135094434 3221224448 3221223104 134558126 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/12868/statm): 30452 30207 145 145 0 30307 0 [pid=12868] vsize: 121808 Current children cumulated CPU time (s) 917.4 Current children cumulated vsize (Kb) 123932 [startup+930.095 s] Raw data (loadavg): 0.99 0.97 0.94 2/57 12868 Raw data (/proc/12864/stat): 12864 (minisat+_script) S 12863 12864 5929 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843588559 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/12864/statm): 531 226 485 147 0 384 0 [pid=12864] vsize: 2124 Raw data (/proc/12868/stat): 12868 (minisat+_64-bit) R 12864 12864 5929 0 -1 0 30673 0 0 0 92536 203 0 0 25 0 1 0 1843588564 124731392 30207 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/12868/statm): 30452 30207 145 145 0 30307 0 [pid=12868] vsize: 121808 Current children cumulated CPU time (s) 927.4 Current children cumulated vsize (Kb) 123932 [startup+940.095 s] Raw data (loadavg): 0.99 0.97 0.94 2/57 12868 Raw data (/proc/12864/stat): 12864 (minisat+_script) S 12863 12864 5929 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843588559 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/12864/statm): 531 226 485 147 0 384 0 [pid=12864] vsize: 2124 Raw data (/proc/12868/stat): 12868 (minisat+_64-bit) R 12864 12864 5929 0 -1 0 30673 0 0 0 93537 203 0 0 25 0 1 0 1843588564 124731392 30207 4294967295 134512640 135094434 3221224448 3221223072 134562104 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/12868/statm): 30452 30207 145 145 0 30307 0 [pid=12868] vsize: 121808 Current children cumulated CPU time (s) 937.41 Current children cumulated vsize (Kb) 123932 [startup+950.096 s] Raw data (loadavg): 0.99 0.97 0.94 2/57 12868 Raw data (/proc/12864/stat): 12864 (minisat+_script) S 12863 12864 5929 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843588559 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/12864/statm): 531 226 485 147 0 384 0 [pid=12864] vsize: 2124 Raw data (/proc/12868/stat): 12868 (minisat+_64-bit) R 12864 12864 5929 0 -1 0 30673 0 0 0 94537 203 0 0 25 0 1 0 1843588564 124731392 30207 4294967295 134512640 135094434 3221224448 3221223120 134555599 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/12868/statm): 30452 30207 145 145 0 30307 0 [pid=12868] vsize: 121808 Current children cumulated CPU time (s) 947.41 Current children cumulated vsize (Kb) 123932 [startup+960.097 s] Raw data (loadavg): 0.99 0.97 0.94 2/57 12868 Raw data (/proc/12864/stat): 12864 (minisat+_script) S 12863 12864 5929 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843588559 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/12864/statm): 531 226 485 147 0 384 0 [pid=12864] vsize: 2124 Raw data (/proc/12868/stat): 12868 (minisat+_64-bit) R 12864 12864 5929 0 -1 0 30673 0 0 0 95537 203 0 0 25 0 1 0 1843588564 124731392 30207 4294967295 134512640 135094434 3221224448 3221223040 134556802 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/12868/statm): 30452 30207 145 145 0 30307 0 [pid=12868] vsize: 121808 Current children cumulated CPU time (s) 957.41 Current children cumulated vsize (Kb) 123932 [startup+970.098 s] Raw data (loadavg): 0.99 0.97 0.94 2/57 12868 Raw data (/proc/12864/stat): 12864 (minisat+_script) S 12863 12864 5929 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843588559 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/12864/statm): 531 226 485 147 0 384 0 [pid=12864] vsize: 2124 Raw data (/proc/12868/stat): 12868 (minisat+_64-bit) R 12864 12864 5929 0 -1 0 30673 0 0 0 96537 203 0 0 25 0 1 0 1843588564 124731392 30207 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/12868/statm): 30452 30207 145 145 0 30307 0 [pid=12868] vsize: 121808 Current children cumulated CPU time (s) 967.41 Current children cumulated vsize (Kb) 123932 [startup+980.1 s] Raw data (loadavg): 0.99 0.97 0.94 2/57 12868 Raw data (/proc/12864/stat): 12864 (minisat+_script) S 12863 12864 5929 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843588559 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/12864/statm): 531 226 485 147 0 384 0 [pid=12864] vsize: 2124 Raw data (/proc/12868/stat): 12868 (minisat+_64-bit) R 12864 12864 5929 0 -1 0 30673 0 0 0 97537 203 0 0 25 0 1 0 1843588564 124731392 30207 4294967295 134512640 135094434 3221224448 3221223040 134557180 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/12868/statm): 30452 30207 145 145 0 30307 0 [pid=12868] vsize: 121808 Current children cumulated CPU time (s) 977.41 Current children cumulated vsize (Kb) 123932 [startup+990.1 s] Raw data (loadavg): 0.99 0.97 0.94 2/57 12868 Raw data (/proc/12864/stat): 12864 (minisat+_script) S 12863 12864 5929 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843588559 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/12864/statm): 531 226 485 147 0 384 0 [pid=12864] vsize: 2124 Raw data (/proc/12868/stat): 12868 (minisat+_64-bit) R 12864 12864 5929 0 -1 0 30673 0 0 0 98538 203 0 0 25 0 1 0 1843588564 124731392 30207 4294967295 134512640 135094434 3221224448 3221223104 134557860 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/12868/statm): 30452 30207 145 145 0 30307 0 [pid=12868] vsize: 121808 Current children cumulated CPU time (s) 987.42 Current children cumulated vsize (Kb) 123932 [startup+1000.1 s] Raw data (loadavg): 0.99 0.97 0.94 2/57 12868 Raw data (/proc/12864/stat): 12864 (minisat+_script) S 12863 12864 5929 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843588559 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/12864/statm): 531 226 485 147 0 384 0 [pid=12864] vsize: 2124 Raw data (/proc/12868/stat): 12868 (minisat+_64-bit) R 12864 12864 5929 0 -1 0 30673 0 0 0 99538 203 0 0 25 0 1 0 1843588564 124731392 30207 4294967295 134512640 135094434 3221224448 3221223104 134557962 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/12868/statm): 30452 30207 145 145 0 30307 0 [pid=12868] vsize: 121808 Current children cumulated CPU time (s) 997.42 Current children cumulated vsize (Kb) 123932 [startup+1010.1 s] Raw data (loadavg): 0.99 0.97 0.94 2/57 12868 Raw data (/proc/12864/stat): 12864 (minisat+_script) S 12863 12864 5929 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843588559 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/12864/statm): 531 226 485 147 0 384 0 [pid=12864] vsize: 2124 Raw data (/proc/12868/stat): 12868 (minisat+_64-bit) R 12864 12864 5929 0 -1 0 30673 0 0 0 100538 203 0 0 25 0 1 0 1843588564 124731392 30207 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/12868/statm): 30452 30207 145 145 0 30307 0 [pid=12868] vsize: 121808 Current children cumulated CPU time (s) 1007.42 Current children cumulated vsize (Kb) 123932 [startup+1020.1 s] Raw data (loadavg): 0.99 0.97 0.94 2/57 12868 Raw data (/proc/12864/stat): 12864 (minisat+_script) S 12863 12864 5929 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843588559 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/12864/statm): 531 226 485 147 0 384 0 [pid=12864] vsize: 2124 Raw data (/proc/12868/stat): 12868 (minisat+_64-bit) R 12864 12864 5929 0 -1 0 30673 0 0 0 101538 203 0 0 25 0 1 0 1843588564 124731392 30207 4294967295 134512640 135094434 3221224448 3221223108 134553482 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/12868/statm): 30452 30207 145 145 0 30307 0 [pid=12868] vsize: 121808 Current children cumulated CPU time (s) 1017.42 Current children cumulated vsize (Kb) 123932 [startup+1030.1 s] Raw data (loadavg): 0.99 0.97 0.94 2/57 12868 Raw data (/proc/12864/stat): 12864 (minisat+_script) S 12863 12864 5929 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843588559 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/12864/statm): 531 226 485 147 0 384 0 [pid=12864] vsize: 2124 Raw data (/proc/12868/stat): 12868 (minisat+_64-bit) R 12864 12864 5929 0 -1 0 30673 0 0 0 102539 203 0 0 25 0 1 0 1843588564 124731392 30207 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/12868/statm): 30452 30207 145 145 0 30307 0 [pid=12868] vsize: 121808 Current children cumulated CPU time (s) 1027.43 Current children cumulated vsize (Kb) 123932 [startup+1040.11 s] Raw data (loadavg): 0.99 0.97 0.94 2/57 12868 Raw data (/proc/12864/stat): 12864 (minisat+_script) S 12863 12864 5929 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843588559 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/12864/statm): 531 226 485 147 0 384 0 [pid=12864] vsize: 2124 Raw data (/proc/12868/stat): 12868 (minisat+_64-bit) R 12864 12864 5929 0 -1 0 30673 0 0 0 103539 203 0 0 25 0 1 0 1843588564 124731392 30207 4294967295 134512640 135094434 3221224448 3221223104 134557996 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/12868/statm): 30452 30207 145 145 0 30307 0 [pid=12868] vsize: 121808 Current children cumulated CPU time (s) 1037.43 Current children cumulated vsize (Kb) 123932 [startup+1050.11 s] Raw data (loadavg): 0.99 0.97 0.94 2/57 12868 Raw data (/proc/12864/stat): 12864 (minisat+_script) S 12863 12864 5929 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843588559 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/12864/statm): 531 226 485 147 0 384 0 [pid=12864] vsize: 2124 Raw data (/proc/12868/stat): 12868 (minisat+_64-bit) R 12864 12864 5929 0 -1 0 30673 0 0 0 104539 203 0 0 25 0 1 0 1843588564 124731392 30207 4294967295 134512640 135094434 3221224448 3221223008 134562165 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/12868/statm): 30452 30207 145 145 0 30307 0 [pid=12868] vsize: 121808 Current children cumulated CPU time (s) 1047.43 Current children cumulated vsize (Kb) 123932 [startup+1060.11 s] Raw data (loadavg): 0.99 0.97 0.94 2/57 12868 Raw data (/proc/12864/stat): 12864 (minisat+_script) S 12863 12864 5929 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843588559 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/12864/statm): 531 226 485 147 0 384 0 [pid=12864] vsize: 2124 Raw data (/proc/12868/stat): 12868 (minisat+_64-bit) R 12864 12864 5929 0 -1 0 30673 0 0 0 105539 203 0 0 25 0 1 0 1843588564 124731392 30207 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/12868/statm): 30452 30207 145 145 0 30307 0 [pid=12868] vsize: 121808 Current children cumulated CPU time (s) 1057.43 Current children cumulated vsize (Kb) 123932 [startup+1070.11 s] Raw data (loadavg): 0.99 0.97 0.94 2/57 12868 Raw data (/proc/12864/stat): 12864 (minisat+_script) S 12863 12864 5929 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843588559 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/12864/statm): 531 226 485 147 0 384 0 [pid=12864] vsize: 2124 Raw data (/proc/12868/stat): 12868 (minisat+_64-bit) R 12864 12864 5929 0 -1 0 30673 0 0 0 106539 203 0 0 25 0 1 0 1843588564 124731392 30207 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/12868/statm): 30452 30207 145 145 0 30307 0 [pid=12868] vsize: 121808 Current children cumulated CPU time (s) 1067.43 Current children cumulated vsize (Kb) 123932 [startup+1080.11 s] Raw data (loadavg): 0.99 0.97 0.94 2/57 12868 Raw data (/proc/12864/stat): 12864 (minisat+_script) S 12863 12864 5929 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843588559 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/12864/statm): 531 226 485 147 0 384 0 [pid=12864] vsize: 2124 Raw data (/proc/12868/stat): 12868 (minisat+_64-bit) R 12864 12864 5929 0 -1 0 30673 0 0 0 107540 203 0 0 25 0 1 0 1843588564 124731392 30207 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/12868/statm): 30452 30207 145 145 0 30307 0 [pid=12868] vsize: 121808 Current children cumulated CPU time (s) 1077.44 Current children cumulated vsize (Kb) 123932 [startup+1090.11 s] Raw data (loadavg): 0.99 0.97 0.94 2/57 12868 Raw data (/proc/12864/stat): 12864 (minisat+_script) S 12863 12864 5929 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843588559 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/12864/statm): 531 226 485 147 0 384 0 [pid=12864] vsize: 2124 Raw data (/proc/12868/stat): 12868 (minisat+_64-bit) R 12864 12864 5929 0 -1 0 30673 0 0 0 108540 203 0 0 25 0 1 0 1843588564 124731392 30207 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/12868/statm): 30452 30207 145 145 0 30307 0 [pid=12868] vsize: 121808 Current children cumulated CPU time (s) 1087.44 Current children cumulated vsize (Kb) 123932 [startup+1100.11 s] Raw data (loadavg): 0.99 0.97 0.94 2/57 12868 Raw data (/proc/12864/stat): 12864 (minisat+_script) S 12863 12864 5929 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843588559 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/12864/statm): 531 226 485 147 0 384 0 [pid=12864] vsize: 2124 Raw data (/proc/12868/stat): 12868 (minisat+_64-bit) R 12864 12864 5929 0 -1 0 30673 0 0 0 109540 203 0 0 25 0 1 0 1843588564 124731392 30207 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/12868/statm): 30452 30207 145 145 0 30307 0 [pid=12868] vsize: 121808 Current children cumulated CPU time (s) 1097.44 Current children cumulated vsize (Kb) 123932 [startup+1110.11 s] Raw data (loadavg): 0.99 0.97 0.94 2/57 12868 Raw data (/proc/12864/stat): 12864 (minisat+_script) S 12863 12864 5929 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843588559 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/12864/statm): 531 226 485 147 0 384 0 [pid=12864] vsize: 2124 Raw data (/proc/12868/stat): 12868 (minisat+_64-bit) R 12864 12864 5929 0 -1 0 30673 0 0 0 110540 204 0 0 25 0 1 0 1843588564 124731392 30207 4294967295 134512640 135094434 3221224448 3221223104 134557945 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/12868/statm): 30452 30207 145 145 0 30307 0 [pid=12868] vsize: 121808 Current children cumulated CPU time (s) 1107.45 Current children cumulated vsize (Kb) 123932 [startup+1120.11 s] Raw data (loadavg): 0.99 0.97 0.94 2/57 12868 Raw data (/proc/12864/stat): 12864 (minisat+_script) S 12863 12864 5929 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843588559 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/12864/statm): 531 226 485 147 0 384 0 [pid=12864] vsize: 2124 Raw data (/proc/12868/stat): 12868 (minisat+_64-bit) R 12864 12864 5929 0 -1 0 30673 0 0 0 111540 204 0 0 25 0 1 0 1843588564 124731392 30207 4294967295 134512640 135094434 3221224448 3221223104 134558162 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/12868/statm): 30452 30207 145 145 0 30307 0 [pid=12868] vsize: 121808 Current children cumulated CPU time (s) 1117.45 Current children cumulated vsize (Kb) 123932 [startup+1130.11 s] Raw data (loadavg): 0.99 0.97 0.94 2/57 12868 Raw data (/proc/12864/stat): 12864 (minisat+_script) S 12863 12864 5929 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843588559 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/12864/statm): 531 226 485 147 0 384 0 [pid=12864] vsize: 2124 Raw data (/proc/12868/stat): 12868 (minisat+_64-bit) R 12864 12864 5929 0 -1 0 30673 0 0 0 112541 204 0 0 25 0 1 0 1843588564 124731392 30207 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/12868/statm): 30452 30207 145 145 0 30307 0 [pid=12868] vsize: 121808 Current children cumulated CPU time (s) 1127.46 Current children cumulated vsize (Kb) 123932 [startup+1140.11 s] Raw data (loadavg): 0.99 0.97 0.94 2/57 12868 Raw data (/proc/12864/stat): 12864 (minisat+_script) S 12863 12864 5929 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843588559 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/12864/statm): 531 226 485 147 0 384 0 [pid=12864] vsize: 2124 Raw data (/proc/12868/stat): 12868 (minisat+_64-bit) R 12864 12864 5929 0 -1 0 30673 0 0 0 113541 204 0 0 25 0 1 0 1843588564 124731392 30207 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/12868/statm): 30452 30207 145 145 0 30307 0 [pid=12868] vsize: 121808 Current children cumulated CPU time (s) 1137.46 Current children cumulated vsize (Kb) 123932 [startup+1150.12 s] Raw data (loadavg): 0.99 0.97 0.94 2/57 12868 Raw data (/proc/12864/stat): 12864 (minisat+_script) S 12863 12864 5929 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843588559 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/12864/statm): 531 226 485 147 0 384 0 [pid=12864] vsize: 2124 Raw data (/proc/12868/stat): 12868 (minisat+_64-bit) R 12864 12864 5929 0 -1 0 30673 0 0 0 114541 204 0 0 25 0 1 0 1843588564 124731392 30207 4294967295 134512640 135094434 3221224448 3221223120 134556502 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/12868/statm): 30452 30207 145 145 0 30307 0 [pid=12868] vsize: 121808 Current children cumulated CPU time (s) 1147.46 Current children cumulated vsize (Kb) 123932 [startup+1160.12 s] Raw data (loadavg): 0.99 0.97 0.94 2/57 12868 Raw data (/proc/12864/stat): 12864 (minisat+_script) S 12863 12864 5929 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843588559 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/12864/statm): 531 226 485 147 0 384 0 [pid=12864] vsize: 2124 Raw data (/proc/12868/stat): 12868 (minisat+_64-bit) R 12864 12864 5929 0 -1 0 30673 0 0 0 115541 204 0 0 25 0 1 0 1843588564 124731392 30207 4294967295 134512640 135094434 3221224448 3221223104 134555980 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/12868/statm): 30452 30207 145 145 0 30307 0 [pid=12868] vsize: 121808 Current children cumulated CPU time (s) 1157.46 Current children cumulated vsize (Kb) 123932 [startup+1170.12 s] Raw data (loadavg): 0.99 0.97 0.94 2/57 12868 Raw data (/proc/12864/stat): 12864 (minisat+_script) S 12863 12864 5929 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843588559 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/12864/statm): 531 226 485 147 0 384 0 [pid=12864] vsize: 2124 Raw data (/proc/12868/stat): 12868 (minisat+_64-bit) R 12864 12864 5929 0 -1 0 30673 0 0 0 116541 204 0 0 25 0 1 0 1843588564 124731392 30207 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/12868/statm): 30452 30207 145 145 0 30307 0 [pid=12868] vsize: 121808 Current children cumulated CPU time (s) 1167.46 Current children cumulated vsize (Kb) 123932 [startup+1180.12 s] Raw data (loadavg): 0.99 0.97 0.94 2/57 12868 Raw data (/proc/12864/stat): 12864 (minisat+_script) S 12863 12864 5929 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843588559 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/12864/statm): 531 226 485 147 0 384 0 [pid=12864] vsize: 2124 Raw data (/proc/12868/stat): 12868 (minisat+_64-bit) R 12864 12864 5929 0 -1 0 30673 0 0 0 117542 204 0 0 25 0 1 0 1843588564 124731392 30207 4294967295 134512640 135094434 3221224448 3221223104 134558007 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/12868/statm): 30452 30207 145 145 0 30307 0 [pid=12868] vsize: 121808 Current children cumulated CPU time (s) 1177.47 Current children cumulated vsize (Kb) 123932 [startup+1190.12 s] Raw data (loadavg): 0.99 0.97 0.94 2/57 12868 Raw data (/proc/12864/stat): 12864 (minisat+_script) S 12863 12864 5929 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843588559 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/12864/statm): 531 226 485 147 0 384 0 [pid=12864] vsize: 2124 Raw data (/proc/12868/stat): 12868 (minisat+_64-bit) R 12864 12864 5929 0 -1 0 30673 0 0 0 118542 204 0 0 25 0 1 0 1843588564 124731392 30207 4294967295 134512640 135094434 3221224448 3221223088 134562139 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/12868/statm): 30452 30207 145 145 0 30307 0 [pid=12868] vsize: 121808 Current children cumulated CPU time (s) 1187.47 Current children cumulated vsize (Kb) 123932 [startup+1200.12 s] Raw data (loadavg): 0.99 0.97 0.94 2/57 12868 Raw data (/proc/12864/stat): 12864 (minisat+_script) S 12863 12864 5929 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843588559 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/12864/statm): 531 226 485 147 0 384 0 [pid=12864] vsize: 2124 Raw data (/proc/12868/stat): 12868 (minisat+_64-bit) R 12864 12864 5929 0 -1 0 30673 0 0 0 119542 204 0 0 25 0 1 0 1843588564 124731392 30207 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/12868/statm): 30452 30207 145 145 0 30307 0 [pid=12868] vsize: 121808 Current children cumulated CPU time (s) 1197.47 Current children cumulated vsize (Kb) 123932 [startup+1210.12 s] Raw data (loadavg): 0.99 0.97 0.94 2/57 12868 Raw data (/proc/12864/stat): 12864 (minisat+_script) S 12863 12864 5929 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843588559 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/12864/statm): 531 226 485 147 0 384 0 [pid=12864] vsize: 2124 Raw data (/proc/12868/stat): 12868 (minisat+_64-bit) R 12864 12864 5929 0 -1 0 30673 0 0 0 120542 204 0 0 25 0 1 0 1843588564 124731392 30207 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/12868/statm): 30452 30207 145 145 0 30307 0 [pid=12868] vsize: 121808 Current children cumulated CPU time (s) 1207.47 Current children cumulated vsize (Kb) 123932 Maximum CPU time exceeded: sending SIGTERM then SIGKILL [startup+1210.12 s] Raw data (loadavg): 0.99 0.97 0.94 2/57 12868 Raw data (/proc/12864/stat): 12864 (minisat+_script) S 12863 12864 5929 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843588559 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/12864/statm): 531 226 485 147 0 384 0 [pid=12864] vsize: 2124 Raw data (/proc/12868/stat): 12868 (minisat+_64-bit) R 12864 12864 5929 0 -1 0 30673 0 0 0 120542 204 0 0 25 0 1 0 1843588564 124731392 30207 4294967295 134512640 135094434 3221224448 3221223104 134558159 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/12868/statm): 30452 30207 145 145 0 30307 0 [pid=12868] vsize: 121808 Current children cumulated CPU time (s) 1207.47 Current children cumulated vsize (Kb) 123932 Sending SIGTERM to -12864 Sleeping 2 seconds One traced child (pid=12864) ended because it received signal 15 (SIGTERM) One traced child (pid=12868) exited with status: 10 All traced children have exited ! Game is over. Child status: 10 Real time (s): 1210.19 CPU time (s): 1207.53 CPU user time (s): 1205.43 CPU system time (s): 2.09968 CPU usage (%): 99.7807 Max. virtual memory (cumulated for all children) (Kb): 123932
ERROR: no interpretation found !