Name | web/www.nlsde.buaa.edu.cn/~kexu/benchmarks/frb50-23-opb/normalized-frb50-23-4.opb |
MD5SUM | b85a90571dde4fe12541342d5605d680 |
Bench Category | optimization, small integers (OPTSMALLINT) |
Has Objective Function | YES |
Satisfiable | YES |
(Un)Satisfiability was proved | YES |
Best value of the objective function | -39 |
Optimality of the best value was proved | NO |
Number of terms in the objective function | 1150 |
Biggest coefficient in the objective function | 1 |
Number of bits for the biggest coefficient in the objective function | 1 |
Sum of the numbers in the objective function | 1150 |
Number of bits of the sum of numbers in the objective function | 11 |
Biggest number in a constraint | 1 |
Number of bits of the biggest number in a constraint | 1 |
Biggest sum of numbers in a constraint | 1150 |
Number of bits of the biggest sum of numbers | 11 |
Best result obtained on this benchmark | SAT |
Best CPU time to get the best result obtained on this benchmark | 1195.05 |
Number of variables | 1150 |
Total number of constraints | 80258 |
Number of constraints which are clauses | 80258 |
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 wulflinc12 THE 2005-09-18 18:50:42 (client local time) PB2005-SCRIPT v4.0 MARKUPS: idlaunch=2707 boxname=wulflinc12 idbench=363 idsolver=3 numberseed=0 MD5SUM SOLVER: MD5SUM BENCH: b85a90571dde4fe12541342d5605d680 /oldhome/oroussel/tmp/wulflinc12/normalized-frb50-23-4.opb REAL COMMAND: minisat+_script /oldhome/oroussel/tmp/wulflinc12/normalized-frb50-23-4.opb IDLAUNCH: 2707 /proc/cpuinfo: processor : 0 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 2 cpu MHz : 451.091 cache size : 512 KB fdiv_bug : no hlt_bug : no f00f_bug : no coma_bug : no fpu : yes fpu_exception : yes cpuid level : 2 wp : yes flags : fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse bogomips : 888.83 processor : 1 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 2 cpu MHz : 451.091 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: 896456 kB Buffers: 38660 kB Cached: 59192 kB SwapCached: 544 kB Active: 68676 kB Inactive: 41376 kB HighTotal: 131008 kB HighFree: 71820 kB LowTotal: 903652 kB LowFree: 824636 kB SwapTotal: 2097136 kB SwapFree: 2096072 kB Dirty: 24 kB Writeback: 0 kB Mapped: 5884 kB Slab: 22508 kB Committed_AS: 64164 kB PageTables: 328 kB VmallocTotal: 114680 kB VmallocUsed: 1364 kB VmallocChunk: 113256 kB JOB ENDED THE 2005-09-18 19:10:53 (client local time) WITH STATUS 10 IN 1207.99 SECONDS stats: 2707 7 1207.99 10
c Parsing PB file... c Converting 80258 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 | 80258 160516 | 26752 0 0 nan | 0.000 % | c ============================================================================== c [1mFound solution: -36[0m c ---[ 0]---> Sorter-cost:63046 Base: c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 0 | 148144 319772 | 49381 0 0 nan | 0.000 % | c | 100 | 147820 319103 | 54319 84 567 6.8 | 0.388 % | c | 250 | 147145 317664 | 59751 188 1432 7.6 | 1.214 % | c | 476 | 146024 315267 | 65726 361 3068 8.5 | 2.595 % | c | 813 | 143729 310234 | 72298 619 5841 9.4 | 5.557 % | c | 1319 | 140833 303816 | 79528 968 9121 9.4 | 9.437 % | c | 2079 | 136692 294527 | 87481 1586 15869 10.0 | 15.004 % | c | 3218 | 131314 282313 | 96229 2417 27902 11.5 | 22.323 % | c | 4926 | 122752 262701 | 105852 3528 39936 11.3 | 34.222 % | c | 7488 | 112044 237857 | 116437 5289 62605 11.8 | 49.090 % | c ============================================================================== c [1mFound solution: -40[0m c ---[ 0]---> Sorter-cost: 0 Base: c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 7928 | 111198 235994 | 37066 5633 66805 11.9 | 49.090 % | c | 8028 | 110897 235287 | 40772 5710 67536 11.8 | 50.901 % | c | 8178 | 110452 234225 | 44849 5792 68387 11.8 | 51.548 % | c | 8403 | 109585 232234 | 49334 5952 71118 11.9 | 52.759 % | c | 8741 | 108728 230226 | 54268 6208 74433 12.0 | 53.995 % | c | 9247 | 107763 227961 | 59695 6556 79030 12.1 | 55.393 % | c | 10006 | 106198 224277 | 65664 7058 87476 12.4 | 57.665 % | c | 11146 | 103552 218006 | 72231 7914 103965 13.1 | 61.514 % | c | 12854 | 100400 210497 | 79454 9088 124554 13.7 | 66.138 % | c | 15416 | 97019 202392 | 87399 10804 161729 15.0 | 71.090 % | c | 19260 | 94852 197144 | 96139 14054 253306 18.0 | 74.363 % | c | 25026 | 93592 194098 | 105753 19178 576284 30.0 | 76.268 % | c ============================================================================== c [1mFound solution: -41[0m c ---[ 0]---> Sorter-cost: 0 Base: c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 29121 | 92780 192183 | 30926 22895 940622 41.1 | 76.268 % | c | 29221 | 92677 191930 | 34018 22961 941837 41.0 | 77.647 % | c | 29371 | 92612 191776 | 37420 23105 945249 40.9 | 77.742 % | c | 29597 | 92612 191776 | 41162 23331 954744 40.9 | 77.742 % | c | 29934 | 92495 191494 | 45278 23662 962311 40.7 | 77.917 % | 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 | 30329 | 92131 190575 | 30710 23891 984433 41.2 | 77.917 % | c | 30429 | 92064 190426 | 33781 23974 986115 41.1 | 78.509 % | c | 30579 | 91949 190146 | 37159 24115 994438 41.2 | 78.683 % | c | 30804 | 91850 189911 | 40875 24280 1003798 41.3 | 78.828 % | c | 31141 | 91766 189701 | 44962 24546 1013462 41.3 | 78.962 % | c | 31647 | 91650 189414 | 49458 25021 1032977 41.3 | 79.143 % | c | 32406 | 91601 189300 | 54404 25733 1089814 42.4 | 79.212 % | c | 33545 | 91498 189059 | 59845 26813 1189985 44.4 | 79.358 % | c | 35253 | 91064 187999 | 65829 28271 1265964 44.8 | 80.005 % | c | 37817 | 90592 186879 | 72412 30523 1417125 46.4 | 80.691 % | c | 41661 | 90247 186028 | 79653 34043 1688146 49.6 | 81.219 % | c | 47427 | 89873 185101 | 87619 39490 2309222 58.5 | 81.806 % | c ============================================================================== c [1mFound solution: -43[0m c ---[ 0]---> Sorter-cost: 0 Base: c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 55522 | 89822 185003 | 29940 47545 3314007 69.7 | 81.806 % | c | 55622 | 89822 185003 | 32934 47645 3321718 69.7 | 81.930 % | c | 55772 | 89822 185003 | 36227 47795 3326427 69.6 | 81.931 % | c | 55998 | 89822 185003 | 39850 48021 3341366 69.6 | 81.930 % | c | 56336 | 89822 185003 | 43835 48359 3370021 69.7 | 81.931 % | c | 56842 | 89822 185003 | 48218 48865 3409651 69.8 | 81.930 % | c | 57601 | 89177 183450 | 53040 48863 3434237 70.3 | 82.894 % | c | 58740 | 89177 183450 | 58344 50002 3579676 71.6 | 82.894 % | c | 60448 | 89117 183296 | 64179 51669 3732132 72.2 | 82.996 % | c | 63011 | 89039 183106 | 70596 54124 3965144 73.3 | 83.114 % | c | 66855 | 89039 183106 | 77656 57968 4599226 79.3 | 83.114 % | c | 72622 | 88752 182402 | 85422 63069 5112366 81.1 | 83.557 % | c | 81271 | 88748 182392 | 93964 71717 6426102 89.6 | 83.564 % | c | 94245 | 88748 182392 | 103361 84691 8009047 94.6 | 83.564 % | c | 113707 | 88741 182375 | 113697 104135 11319413 108.7 | 83.574 % | 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 | 140871 | 88488 181720 | 29496 130980 15028721 114.7 | 83.574 % | c | 140971 | 88488 181720 | 32445 23657 1604034 67.8 | 83.975 % | c | 141121 | 88488 181720 | 35690 23807 1613264 67.8 | 83.975 % | c | 141346 | 88488 181720 | 39259 24032 1631251 67.9 | 83.975 % | c | 141683 | 88328 181322 | 43185 24359 1642586 67.4 | 84.221 % | c | 142189 | 88328 181322 | 47503 24865 1700627 68.4 | 84.221 % | c | 142948 | 88328 181322 | 52253 25624 1787151 69.7 | 84.221 % | c | 144087 | 88328 181322 | 57479 26763 1947089 72.8 | 84.221 % | c | 145797 | 88226 181078 | 63227 28458 2159705 75.9 | 84.369 % | c | 148359 | 88221 181067 | 69550 31016 2379812 76.7 | 84.375 % | c | 152203 | 88221 181067 | 76505 34860 2924276 83.9 | 84.375 % | c | 157969 | 88221 181067 | 84155 40626 3769186 92.8 | 84.375 % | c | 166618 | 88180 180970 | 92571 49077 4992109 101.7 | 84.436 % | c | 179592 | 88139 180873 | 101828 61925 6663510 107.6 | 84.496 % | 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 | 193053 | 88160 180935 | 29386 75386 9039640 119.9 | 84.496 % | c | 193153 | 88154 180921 | 32324 20076 2226072 110.9 | 84.484 % | c | 193303 | 88149 180908 | 35557 20222 2233119 110.4 | 84.492 % | c | 193528 | 88149 180908 | 39112 20447 2240695 109.6 | 84.492 % | c | 193865 | 87960 180457 | 43024 20704 2251356 108.7 | 84.765 % | c | 194373 | 87960 180457 | 47326 21212 2285864 107.8 | 84.765 % | c | 195133 | 87928 180387 | 52059 21969 2317828 105.5 | 84.806 % | c | 196272 | 87928 180387 | 57265 23108 2390481 103.4 | 84.806 % | c | 197981 | 87877 180262 | 62991 24808 2557155 103.1 | 84.886 % | c | 200543 | 87877 180262 | 69290 27370 2839758 103.8 | 84.886 % | c | 204387 | 87859 180218 | 76219 31206 3310018 106.1 | 84.914 % | c | 210154 | 87728 179913 | 83841 36956 3914827 105.9 | 85.101 % | c | 218803 | 87618 179642 | 92225 45444 4968749 109.3 | 85.273 % | c | 231778 | 87612 179628 | 101448 58416 6873546 117.7 | 85.281 % | c | 251240 | 87602 179602 | 111593 77876 9366492 120.3 | 85.299 % | c | 280433 | 87500 179360 | 122752 106975 13247285 123.8 | 85.449 % | c c *** TERMINATED *** s SATISFIABLE v -C1150 -C1149 -C1148 -C1147 -C1146 -C1145 -C1144 -C1143 -C1142 -C1141 -C1140 -C1139 -C1138 -C1137 -C1136 -C1135 -C1134 -C1133 -C1132 -C1131 C1130 -C1129 -C1128 -C1127 -C1126 -C1125 -C1124 -C1123 -C1122 -C1121 -C1120 -C1119 -C1118 -C1117 -C1116 -C1115 -C1114 -C1113 -C1112 -C1111 -C1110 -C1109 -C1108 -C1107 C1106 -C1105 -C1104 -C1103 -C1102 -C1101 -C1100 C1099 -C1098 -C1097 -C1096 -C1095 -C1094 -C1093 -C1092 -C1091 -C1090 -C1089 -C1088 -C1087 -C1086 -C1085 -C1084 -C1083 -C1082 -C1081 -C1080 -C1079 -C1078 -C1077 -C1076 -C1075 -C1074 -C1073 -C1072 C1071 -C1070 -C1069 -C1068 -C1067 -C1066 -C1065 -C1064 -C1063 -C1062 -C1061 -C1060 -C1059 -C1058 -C1057 -C1056 -C1055 -C1054 -C1053 -C1052 -C1051 -C1050 -C1049 -C1048 -C1047 -C1046 -C1045 -C1044 -C1043 -C1042 C1041 -C1040 -C1039 -C1038 -C1037 -C1036 -C1035 -C1034 -C1033 -C1032 -C1031 -C1030 -C1029 -C1028 -C1027 -C1026 -C1025 -C1024 -C1023 -C1022 -C1021 C1020 -C1019 -C1018 -C1017 -C1016 -C1015 -C1014 -C1013 -C1012 -C1011 -C1010 -C1009 -C1008 -C1007 -C1006 -C1005 C1004 -C1003 -C1002 -C1001 -C1000 -C999 -C998 -C997 -C996 -C995 -C994 -C993 -C992 -C991 -C990 -C989 C988 -C987 -C986 -C985 -C984 -C983 -C982 -C981 -C980 -C979 -C978 -C977 -C976 -C975 -C974 -C973 -C972 -C971 -C970 -C969 -C968 -C967 C966 -C965 -C964 -C963 -C962 -C961 -C960 -C959 -C958 -C957 -C956 -C955 -C954 -C953 -C952 -C951 -C950 -C949 -C948 -C947 -C946 -C945 -C944 -C943 -C942 -C941 -C940 -C939 -C938 -C937 -C936 -C935 -C934 -C933 -C932 -C931 -C930 -C929 -C928 -C927 -C926 -C925 -C924 -C923 -C922 -C921 C920 -C919 -C918 -C917 -C916 -C915 -C914 -C913 -C912 -C911 -C910 -C909 -C908 -C907 -C906 -C905 -C904 -C903 -C902 -C901 -C900 -C899 -C898 -C897 -C896 -C895 -C894 C893 -C892 -C891 -C890 -C889 -C888 -C887 -C886 -C885 -C884 -C883 -C882 -C881 -C880 -C879 -C878 -C877 -C876 -C875 -C874 -C873 -C872 -C871 -C870 -C869 -C868 -C867 -C866 -C865 -C864 -C863 C862 -C861 -C860 -C859 -C858 -C857 -C856 -C855 -C854 -C853 -C852 -C851 -C850 -C849 -C848 -C847 C846 -C845 -C844 -C843 -C842 -C841 -C840 -C839 -C838 -C837 -C836 -C835 -C834 -C833 -C832 -C831 -C830 -C829 -C828 -C827 -C826 -C825 -C824 -C823 -C822 -C821 -C820 -C819 -C818 -C817 -C816 -C815 -C814 -C813 -C812 -C811 -C810 C809 -C808 -C807 -C806 -C805 -C804 -C803 -C802 -C801 C800 -C799 -C798 -C797 -C796 -C795 -C794 -C793 -C792 -C791 -C790 -C789 -C788 -C787 -C786 -C785 -C784 -C783 -C782 -C781 -C780 -C779 -C778 -C777 C776 -C775 -C774 -C773 -C772 -C771 -C770 -C769 -C768 -C767 -C766 -C765 -C764 -C763 -C762 -C761 -C760 -C759 -C758 -C757 -C756 -C755 -C754 -C753 -C752 -C751 -C750 -C749 -C748 -C747 -C746 -C745 -C744 -C743 -C742 -C741 C740 -C739 -C738 -C737 -C736 -C735 -C734 -C733 -C732 -C731 -C730 -C729 -C728 -C727 -C726 -C725 -C724 -C723 -C722 C721 -C720 -C719 -C718 -C717 -C716 -C715 -C714 -C713 -C712 -C711 -C710 -C709 -C708 -C707 -C706 -C705 -C704 -C703 -C702 C701 -C700 -C699 -C698 -C697 -C696 -C695 -C694 -C693 -C692 -C691 C690 -C689 -C688 -C687 -C686 -C685 -C684 -C683 -C682 -C681 -C680 -C679 -C678 -C677 -C676 -C675 -C674 -C673 -C672 -C671 -C670 -C669 -C668 -C667 -C666 -C665 C664 -C663 -C662 -C661 -C660 -C659 -C658 -C657 -C656 -C655 -C654 -C653 -C652 -C651 -C650 -C649 -C648 -C647 -C646 -C645 -C644 -C643 -C642 -C641 -C640 C639 -C638 -C637 -C636 -C635 -C634 -C633 -C632 -C631 -C630 -C629 -C628 -C627 -C626 -C625 -C624 -C623 -C622 -C621 -C620 -C619 -C618 -C617 -C616 -C615 -C614 C613 -C612 -C611 -C610 -C609 -C608 -C607 -C606 -C605 -C604 -C603 -C602 -C601 -C600 -C599 -C598 -C597 -C596 -C595 -C594 -C593 -C592 -C591 -C590 -C589 C588 -C587 -C586 -C585 -C584 -C583 -C582 -C581 -C580 -C579 -C578 -C577 -C576 C575 -C574 -C573 -C572 -C571 -C570 -C569 -C568 -C567 -C566 -C565 -C564 -C563 -C562 -C561 -C560 -C559 -C558 -C557 -C556 -C555 -C554 -C553 -C552 -C551 -C550 -C549 -C548 -C547 -C546 -C545 -C544 -C543 -C542 -C541 C540 -C539 -C538 -C537 -C536 -C535 -C534 -C533 -C532 -C531 -C530 -C529 -C528 -C527 -C526 -C525 -C524 -C523 C522 -C521 -C520 -C519 -C518 -C517 -C516 -C515 -C514 -C513 -C512 -C511 -C510 -C509 -C508 -C507 -C506 -C505 -C504 -C503 -C502 -C501 -C500 -C499 -C498 -C497 -C496 C4
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/25273/stat): 25273 (minisat+_script) R 25272 25273 8263 0 -1 0 19 0 0 0 0 0 0 0 23 0 1 0 1785310562 712704 3 4294967295 134512640 135087896 3221224512 3221224512 1073744960 0 0 5 0 0 0 0 17 0 0 0 Raw data (/proc/25273/statm): 174 3 169 147 0 27 0 [pid=25273] 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=25274 New process pid=25275 New process pid=25276 One traced child (pid=25275) 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=25276) exited with status: 0 One traced child (pid=25274) exited with status: 0 New process pid=25277 execve syscall for /oldhome/oroussel/solvers/minisat+_64-bit_static executable open syscall for file /dev/null open syscall for file /oldhome/oroussel/tmp/wulflinc12/normalized-frb50-23-4.opb [startup+10.0041 s] Raw data (loadavg): 0.93 0.97 0.91 2/57 25277 Raw data (/proc/25273/stat): 25273 (minisat+_script) S 25272 25273 8263 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785310562 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/25273/statm): 531 226 485 147 0 384 0 [pid=25273] vsize: 2124 Raw data (/proc/25277/stat): 25277 (minisat+_64-bit) R 25273 25273 8263 0 -1 0 5076 0 0 0 960 20 0 0 25 0 1 0 1785310567 21692416 5063 4294967295 134512640 135094434 3221224448 3221223104 134557846 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/25277/statm): 5296 5063 145 145 0 5151 0 [pid=25277] vsize: 21184 Current children cumulated CPU time (s) 9.8 Current children cumulated vsize (Kb) 23308 [startup+20.0049 s] Raw data (loadavg): 0.94 0.97 0.91 2/57 25277 Raw data (/proc/25273/stat): 25273 (minisat+_script) S 25272 25273 8263 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785310562 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/25273/statm): 531 226 485 147 0 384 0 [pid=25273] vsize: 2124 Raw data (/proc/25277/stat): 25277 (minisat+_64-bit) R 25273 25273 8263 0 -1 0 5076 0 0 0 1959 20 0 0 25 0 1 0 1785310567 21692416 5063 4294967295 134512640 135094434 3221224448 3221223108 134553487 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/25277/statm): 5296 5063 145 145 0 5151 0 [pid=25277] vsize: 21184 Current children cumulated CPU time (s) 19.79 Current children cumulated vsize (Kb) 23308 [startup+30.0068 s] Raw data (loadavg): 0.95 0.97 0.91 2/57 25277 Raw data (/proc/25273/stat): 25273 (minisat+_script) S 25272 25273 8263 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785310562 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/25273/statm): 531 226 485 147 0 384 0 [pid=25273] vsize: 2124 Raw data (/proc/25277/stat): 25277 (minisat+_64-bit) R 25273 25273 8263 0 -1 0 5076 0 0 0 2959 21 0 0 25 0 1 0 1785310567 21692416 5063 4294967295 134512640 135094434 3221224448 3221223092 134558040 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/25277/statm): 5296 5063 145 145 0 5151 0 [pid=25277] vsize: 21184 Current children cumulated CPU time (s) 29.8 Current children cumulated vsize (Kb) 23308 [startup+40.0076 s] Raw data (loadavg): 0.96 0.97 0.91 2/57 25277 Raw data (/proc/25273/stat): 25273 (minisat+_script) S 25272 25273 8263 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785310562 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/25273/statm): 531 226 485 147 0 384 0 [pid=25273] vsize: 2124 Raw data (/proc/25277/stat): 25277 (minisat+_64-bit) R 25273 25273 8263 0 -1 0 5076 0 0 0 3958 21 0 0 25 0 1 0 1785310567 21692416 5063 4294967295 134512640 135094434 3221224448 3221223108 134553446 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/25277/statm): 5296 5063 145 145 0 5151 0 [pid=25277] vsize: 21184 Current children cumulated CPU time (s) 39.79 Current children cumulated vsize (Kb) 23308 [startup+50.0085 s] Raw data (loadavg): 0.96 0.97 0.91 2/57 25277 Raw data (/proc/25273/stat): 25273 (minisat+_script) S 25272 25273 8263 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785310562 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/25273/statm): 531 226 485 147 0 384 0 [pid=25273] vsize: 2124 Raw data (/proc/25277/stat): 25277 (minisat+_64-bit) R 25273 25273 8263 0 -1 0 5076 0 0 0 4959 21 0 0 25 0 1 0 1785310567 21692416 5063 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/25277/statm): 5296 5063 145 145 0 5151 0 [pid=25277] vsize: 21184 Current children cumulated CPU time (s) 49.8 Current children cumulated vsize (Kb) 23308 [startup+60.0093 s] Raw data (loadavg): 0.97 0.97 0.91 2/57 25277 Raw data (/proc/25273/stat): 25273 (minisat+_script) S 25272 25273 8263 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785310562 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/25273/statm): 531 226 485 147 0 384 0 [pid=25273] vsize: 2124 Raw data (/proc/25277/stat): 25277 (minisat+_64-bit) R 25273 25273 8263 0 -1 0 5076 0 0 0 5959 21 0 0 25 0 1 0 1785310567 21692416 5063 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/25277/statm): 5296 5063 145 145 0 5151 0 [pid=25277] vsize: 21184 Current children cumulated CPU time (s) 59.8 Current children cumulated vsize (Kb) 23308 [startup+70.0101 s] Raw data (loadavg): 0.97 0.97 0.91 2/57 25277 Raw data (/proc/25273/stat): 25273 (minisat+_script) S 25272 25273 8263 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785310562 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/25273/statm): 531 226 485 147 0 384 0 [pid=25273] vsize: 2124 Raw data (/proc/25277/stat): 25277 (minisat+_64-bit) R 25273 25273 8263 0 -1 0 5342 0 0 0 6958 22 0 0 25 0 1 0 1785310567 23666688 5329 4294967295 134512640 135094434 3221224448 3221223200 134559238 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/25277/statm): 5778 5329 145 145 0 5633 0 [pid=25277] vsize: 23112 Current children cumulated CPU time (s) 69.8 Current children cumulated vsize (Kb) 25236 [startup+80.011 s] Raw data (loadavg): 0.98 0.97 0.91 2/57 25277 Raw data (/proc/25273/stat): 25273 (minisat+_script) S 25272 25273 8263 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785310562 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/25273/statm): 531 226 485 147 0 384 0 [pid=25273] vsize: 2124 Raw data (/proc/25277/stat): 25277 (minisat+_64-bit) R 25273 25273 8263 0 -1 0 5345 0 0 0 7958 22 0 0 25 0 1 0 1785310567 23666688 5332 4294967295 134512640 135094434 3221224448 3221223060 134563055 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/25277/statm): 5778 5332 145 145 0 5633 0 [pid=25277] vsize: 23112 Current children cumulated CPU time (s) 79.8 Current children cumulated vsize (Kb) 25236 [startup+90.0118 s] Raw data (loadavg): 0.98 0.97 0.91 2/57 25277 Raw data (/proc/25273/stat): 25273 (minisat+_script) S 25272 25273 8263 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785310562 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/25273/statm): 531 226 485 147 0 384 0 [pid=25273] vsize: 2124 Raw data (/proc/25277/stat): 25277 (minisat+_64-bit) R 25273 25273 8263 0 -1 0 5345 0 0 0 8958 22 0 0 25 0 1 0 1785310567 23666688 5332 4294967295 134512640 135094434 3221224448 3221223104 134558246 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/25277/statm): 5778 5332 145 145 0 5633 0 [pid=25277] vsize: 23112 Current children cumulated CPU time (s) 89.8 Current children cumulated vsize (Kb) 25236 [startup+100.013 s] Raw data (loadavg): 0.98 0.97 0.91 2/57 25277 Raw data (/proc/25273/stat): 25273 (minisat+_script) S 25272 25273 8263 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785310562 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/25273/statm): 531 226 485 147 0 384 0 [pid=25273] vsize: 2124 Raw data (/proc/25277/stat): 25277 (minisat+_64-bit) R 25273 25273 8263 0 -1 0 5645 0 0 0 9953 24 0 0 25 0 1 0 1785310567 24952832 5632 4294967295 134512640 135094434 3221224448 3221223108 134553482 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/25277/statm): 6092 5632 145 145 0 5947 0 [pid=25277] vsize: 24368 Current children cumulated CPU time (s) 99.77 Current children cumulated vsize (Kb) 26492 [startup+110.014 s] Raw data (loadavg): 0.98 0.97 0.91 2/57 25277 Raw data (/proc/25273/stat): 25273 (minisat+_script) S 25272 25273 8263 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785310562 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/25273/statm): 531 226 485 147 0 384 0 [pid=25273] vsize: 2124 Raw data (/proc/25277/stat): 25277 (minisat+_64-bit) R 25273 25273 8263 0 -1 0 6204 0 0 0 10943 29 0 0 25 0 1 0 1785310567 27029504 6143 4294967295 134512640 135094434 3221224448 3221223236 134553482 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/25277/statm): 6599 6143 145 145 0 6454 0 [pid=25277] vsize: 26396 Current children cumulated CPU time (s) 109.72 Current children cumulated vsize (Kb) 28520 [startup+120.014 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 25277 Raw data (/proc/25273/stat): 25273 (minisat+_script) S 25272 25273 8263 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785310562 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/25273/statm): 531 226 485 147 0 384 0 [pid=25273] vsize: 2124 Raw data (/proc/25277/stat): 25277 (minisat+_64-bit) R 25273 25273 8263 0 -1 0 6542 0 0 0 11936 32 0 0 25 0 1 0 1785310567 28213248 6436 4294967295 134512640 135094434 3221224448 3221223108 134553497 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/25277/statm): 6888 6436 145 145 0 6743 0 [pid=25277] vsize: 27552 Current children cumulated CPU time (s) 119.68 Current children cumulated vsize (Kb) 29676 [startup+130.015 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 25277 Raw data (/proc/25273/stat): 25273 (minisat+_script) S 25272 25273 8263 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785310562 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/25273/statm): 531 226 485 147 0 384 0 [pid=25273] vsize: 2124 Raw data (/proc/25277/stat): 25277 (minisat+_64-bit) R 25273 25273 8263 0 -1 0 6857 0 0 0 12930 34 0 0 25 0 1 0 1785310567 29487104 6751 4294967295 134512640 135094434 3221224448 3221223104 134558402 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/25277/statm): 7199 6751 145 145 0 7054 0 [pid=25277] vsize: 28796 Current children cumulated CPU time (s) 129.64 Current children cumulated vsize (Kb) 30920 [startup+140.016 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 25277 Raw data (/proc/25273/stat): 25273 (minisat+_script) S 25272 25273 8263 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785310562 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/25273/statm): 531 226 485 147 0 384 0 [pid=25273] vsize: 2124 Raw data (/proc/25277/stat): 25277 (minisat+_64-bit) R 25273 25273 8263 0 -1 0 7271 0 0 0 13924 37 0 0 25 0 1 0 1785310567 31297536 7165 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/25277/statm): 7641 7165 145 145 0 7496 0 [pid=25277] vsize: 30564 Current children cumulated CPU time (s) 139.61 Current children cumulated vsize (Kb) 32688 [startup+150.017 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 25277 Raw data (/proc/25273/stat): 25273 (minisat+_script) S 25272 25273 8263 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785310562 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/25273/statm): 531 226 485 147 0 384 0 [pid=25273] vsize: 2124 Raw data (/proc/25277/stat): 25277 (minisat+_64-bit) R 25273 25273 8263 0 -1 0 7770 0 0 0 14916 40 0 0 25 0 1 0 1785310567 33320960 7664 4294967295 134512640 135094434 3221224448 3221223040 134556834 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/25277/statm): 8135 7664 145 145 0 7990 0 [pid=25277] vsize: 32540 Current children cumulated CPU time (s) 149.56 Current children cumulated vsize (Kb) 34664 [startup+160.018 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 25277 Raw data (/proc/25273/stat): 25273 (minisat+_script) S 25272 25273 8263 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785310562 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/25273/statm): 531 226 485 147 0 384 0 [pid=25273] vsize: 2124 Raw data (/proc/25277/stat): 25277 (minisat+_64-bit) R 25273 25273 8263 0 -1 0 8259 0 0 0 15907 42 0 0 25 0 1 0 1785310567 35307520 8153 4294967295 134512640 135094434 3221224448 3221223104 134558178 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/25277/statm): 8620 8153 145 145 0 8475 0 [pid=25277] vsize: 34480 Current children cumulated CPU time (s) 159.49 Current children cumulated vsize (Kb) 36604 [startup+170.019 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 25277 Raw data (/proc/25273/stat): 25273 (minisat+_script) S 25272 25273 8263 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785310562 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/25273/statm): 531 226 485 147 0 384 0 [pid=25273] vsize: 2124 Raw data (/proc/25277/stat): 25277 (minisat+_64-bit) R 25273 25273 8263 0 -1 0 8790 0 0 0 16897 46 0 0 25 0 1 0 1785310567 37466112 8684 4294967295 134512640 135094434 3221224448 3221223072 134562057 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/25277/statm): 9147 8684 145 145 0 9002 0 [pid=25277] vsize: 36588 Current children cumulated CPU time (s) 169.43 Current children cumulated vsize (Kb) 38712 [startup+180.019 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 25277 Raw data (/proc/25273/stat): 25273 (minisat+_script) S 25272 25273 8263 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785310562 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/25273/statm): 531 226 485 147 0 384 0 [pid=25273] vsize: 2124 Raw data (/proc/25277/stat): 25277 (minisat+_64-bit) R 25273 25273 8263 0 -1 0 9058 0 0 0 17893 48 0 0 25 0 1 0 1785310567 38367232 8905 4294967295 134512640 135094434 3221224448 3221223136 134554746 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/25277/statm): 9367 8905 145 145 0 9222 0 [pid=25277] vsize: 37468 Current children cumulated CPU time (s) 179.41 Current children cumulated vsize (Kb) 39592 [startup+190.02 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 25277 Raw data (/proc/25273/stat): 25273 (minisat+_script) S 25272 25273 8263 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785310562 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/25273/statm): 531 226 485 147 0 384 0 [pid=25273] vsize: 2124 Raw data (/proc/25277/stat): 25277 (minisat+_64-bit) R 25273 25273 8263 0 -1 0 9456 0 0 0 18886 51 0 0 25 0 1 0 1785310567 39981056 9303 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/25277/statm): 9761 9303 145 145 0 9616 0 [pid=25277] vsize: 39044 Current children cumulated CPU time (s) 189.37 Current children cumulated vsize (Kb) 41168 [startup+200.02 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 25277 Raw data (/proc/25273/stat): 25273 (minisat+_script) S 25272 25273 8263 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785310562 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/25273/statm): 531 226 485 147 0 384 0 [pid=25273] vsize: 2124 Raw data (/proc/25277/stat): 25277 (minisat+_64-bit) R 25273 25273 8263 0 -1 0 10007 0 0 0 19875 56 0 0 25 0 1 0 1785310567 42221568 9854 4294967295 134512640 135094434 3221224448 3221223104 134557840 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/25277/statm): 10308 9854 145 145 0 10163 0 [pid=25277] vsize: 41232 Current children cumulated CPU time (s) 199.31 Current children cumulated vsize (Kb) 43356 [startup+210.021 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 25277 Raw data (/proc/25273/stat): 25273 (minisat+_script) S 25272 25273 8263 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785310562 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/25273/statm): 531 226 485 147 0 384 0 [pid=25273] vsize: 2124 Raw data (/proc/25277/stat): 25277 (minisat+_64-bit) R 25273 25273 8263 0 -1 0 10379 0 0 0 20869 59 0 0 25 0 1 0 1785310567 43737088 10226 4294967295 134512640 135094434 3221224448 3221223104 134558126 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/25277/statm): 10678 10226 145 145 0 10533 0 [pid=25277] vsize: 42712 Current children cumulated CPU time (s) 209.28 Current children cumulated vsize (Kb) 44836 [startup+220.022 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 25277 Raw data (/proc/25273/stat): 25273 (minisat+_script) S 25272 25273 8263 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785310562 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/25273/statm): 531 226 485 147 0 384 0 [pid=25273] vsize: 2124 Raw data (/proc/25277/stat): 25277 (minisat+_64-bit) R 25273 25273 8263 0 -1 0 10741 0 0 0 21862 62 0 0 25 0 1 0 1785310567 45207552 10588 4294967295 134512640 135094434 3221224448 3221223108 134553482 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/25277/statm): 11037 10588 145 145 0 10892 0 [pid=25277] vsize: 44148 Current children cumulated CPU time (s) 219.24 Current children cumulated vsize (Kb) 46272 [startup+230.023 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 25277 Raw data (/proc/25273/stat): 25273 (minisat+_script) S 25272 25273 8263 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785310562 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/25273/statm): 531 226 485 147 0 384 0 [pid=25273] vsize: 2124 Raw data (/proc/25277/stat): 25277 (minisat+_64-bit) R 25273 25273 8263 0 -1 0 11221 0 0 0 22853 66 0 0 25 0 1 0 1785310567 47161344 11068 4294967295 134512640 135094434 3221224448 3221223104 134558187 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/25277/statm): 11514 11068 145 145 0 11369 0 [pid=25277] vsize: 46056 Current children cumulated CPU time (s) 229.19 Current children cumulated vsize (Kb) 48180 [startup+240.023 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 25277 Raw data (/proc/25273/stat): 25273 (minisat+_script) S 25272 25273 8263 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785310562 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/25273/statm): 531 226 485 147 0 384 0 [pid=25273] vsize: 2124 Raw data (/proc/25277/stat): 25277 (minisat+_64-bit) R 25273 25273 8263 0 -1 0 11694 0 0 0 23845 70 0 0 25 0 1 0 1785310567 49348608 11541 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/25277/statm): 12048 11541 145 145 0 11903 0 [pid=25277] vsize: 48192 Current children cumulated CPU time (s) 239.15 Current children cumulated vsize (Kb) 50316 [startup+250.024 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 25277 Raw data (/proc/25273/stat): 25273 (minisat+_script) S 25272 25273 8263 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785310562 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/25273/statm): 531 226 485 147 0 384 0 [pid=25273] vsize: 2124 Raw data (/proc/25277/stat): 25277 (minisat+_64-bit) R 25273 25273 8263 0 -1 0 12129 0 0 0 24837 73 0 0 25 0 1 0 1785310567 51118080 11976 4294967295 134512640 135094434 3221224448 3221223104 134557956 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/25277/statm): 12480 11976 145 145 0 12335 0 [pid=25277] vsize: 49920 Current children cumulated CPU time (s) 249.1 Current children cumulated vsize (Kb) 52044 [startup+260.025 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 25277 Raw data (/proc/25273/stat): 25273 (minisat+_script) S 25272 25273 8263 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785310562 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/25273/statm): 531 226 485 147 0 384 0 [pid=25273] vsize: 2124 Raw data (/proc/25277/stat): 25277 (minisat+_64-bit) R 25273 25273 8263 0 -1 0 12586 0 0 0 25828 77 0 0 25 0 1 0 1785310567 52977664 12433 4294967295 134512640 135094434 3221224448 3221223072 134557596 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/25277/statm): 12934 12433 145 145 0 12789 0 [pid=25277] vsize: 51736 Current children cumulated CPU time (s) 259.05 Current children cumulated vsize (Kb) 53860 [startup+270.026 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 25277 Raw data (/proc/25273/stat): 25273 (minisat+_script) S 25272 25273 8263 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785310562 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/25273/statm): 531 226 485 147 0 384 0 [pid=25273] vsize: 2124 Raw data (/proc/25277/stat): 25277 (minisat+_64-bit) R 25273 25273 8263 0 -1 0 12936 0 0 0 26823 79 0 0 25 0 1 0 1785310567 54398976 12783 4294967295 134512640 135094434 3221224448 3221223104 134557956 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/25277/statm): 13281 12783 145 145 0 13136 0 [pid=25277] vsize: 53124 Current children cumulated CPU time (s) 269.02 Current children cumulated vsize (Kb) 55248 [startup+280.027 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 25277 Raw data (/proc/25273/stat): 25273 (minisat+_script) S 25272 25273 8263 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785310562 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/25273/statm): 531 226 485 147 0 384 0 [pid=25273] vsize: 2124 Raw data (/proc/25277/stat): 25277 (minisat+_64-bit) R 25273 25273 8263 0 -1 0 13279 0 0 0 27817 81 0 0 25 0 1 0 1785310567 55795712 13126 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/25277/statm): 13622 13126 145 145 0 13477 0 [pid=25277] vsize: 54488 Current children cumulated CPU time (s) 278.98 Current children cumulated vsize (Kb) 56612 [startup+290.028 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 25277 Raw data (/proc/25273/stat): 25273 (minisat+_script) S 25272 25273 8263 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785310562 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/25273/statm): 531 226 485 147 0 384 0 [pid=25273] vsize: 2124 Raw data (/proc/25277/stat): 25277 (minisat+_64-bit) R 25273 25273 8263 0 -1 0 13671 0 0 0 28810 84 0 0 25 0 1 0 1785310567 57389056 13518 4294967295 134512640 135094434 3221224448 3221223040 134557273 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/25277/statm): 14011 13518 145 145 0 13866 0 [pid=25277] vsize: 56044 Current children cumulated CPU time (s) 288.94 Current children cumulated vsize (Kb) 58168 [startup+300.028 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 25277 Raw data (/proc/25273/stat): 25273 (minisat+_script) S 25272 25273 8263 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785310562 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/25273/statm): 531 226 485 147 0 384 0 [pid=25273] vsize: 2124 Raw data (/proc/25277/stat): 25277 (minisat+_64-bit) R 25273 25273 8263 0 -1 0 14024 0 0 0 29803 88 0 0 25 0 1 0 1785310567 58822656 13871 4294967295 134512640 135094434 3221224448 3221223104 134558213 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/25277/statm): 14361 13871 145 145 0 14216 0 [pid=25277] vsize: 57444 Current children cumulated CPU time (s) 298.91 Current children cumulated vsize (Kb) 59568 [startup+310.029 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 25277 Raw data (/proc/25273/stat): 25273 (minisat+_script) S 25272 25273 8263 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785310562 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/25273/statm): 531 226 485 147 0 384 0 [pid=25273] vsize: 2124 Raw data (/proc/25277/stat): 25277 (minisat+_64-bit) R 25273 25273 8263 0 -1 0 14369 0 0 0 30796 90 0 0 25 0 1 0 1785310567 60227584 14216 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/25277/statm): 14704 14216 145 145 0 14559 0 [pid=25277] vsize: 58816 Current children cumulated CPU time (s) 308.86 Current children cumulated vsize (Kb) 60940 [startup+320.03 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 25277 Raw data (/proc/25273/stat): 25273 (minisat+_script) S 25272 25273 8263 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785310562 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/25273/statm): 531 226 485 147 0 384 0 [pid=25273] vsize: 2124 Raw data (/proc/25277/stat): 25277 (minisat+_64-bit) R 25273 25273 8263 0 -1 0 14764 0 0 0 31790 93 0 0 25 0 1 0 1785310567 61833216 14611 4294967295 134512640 135094434 3221224448 3221223120 134556329 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/25277/statm): 15096 14611 145 145 0 14951 0 [pid=25277] vsize: 60384 Current children cumulated CPU time (s) 318.83 Current children cumulated vsize (Kb) 62508 [startup+330.031 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 25277 Raw data (/proc/25273/stat): 25273 (minisat+_script) S 25272 25273 8263 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785310562 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/25273/statm): 531 226 485 147 0 384 0 [pid=25273] vsize: 2124 Raw data (/proc/25277/stat): 25277 (minisat+_64-bit) R 25273 25273 8263 0 -1 0 15130 0 0 0 32784 96 0 0 25 0 1 0 1785310567 63324160 14977 4294967295 134512640 135094434 3221224448 3221223040 134557202 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/25277/statm): 15460 14977 145 145 0 15315 0 [pid=25277] vsize: 61840 Current children cumulated CPU time (s) 328.8 Current children cumulated vsize (Kb) 63964 [startup+340.032 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 25277 Raw data (/proc/25273/stat): 25273 (minisat+_script) S 25272 25273 8263 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785310562 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/25273/statm): 531 226 485 147 0 384 0 [pid=25273] vsize: 2124 Raw data (/proc/25277/stat): 25277 (minisat+_64-bit) R 25273 25273 8263 0 -1 0 15492 0 0 0 33777 98 0 0 25 0 1 0 1785310567 64798720 15339 4294967295 134512640 135094434 3221224448 3221223104 134558235 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/25277/statm): 15820 15339 145 145 0 15675 0 [pid=25277] vsize: 63280 Current children cumulated CPU time (s) 338.75 Current children cumulated vsize (Kb) 65404 [startup+350.033 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 25277 Raw data (/proc/25273/stat): 25273 (minisat+_script) S 25272 25273 8263 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785310562 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/25273/statm): 531 226 485 147 0 384 0 [pid=25273] vsize: 2124 Raw data (/proc/25277/stat): 25277 (minisat+_64-bit) R 25273 25273 8263 0 -1 0 15879 0 0 0 34769 101 0 0 25 0 1 0 1785310567 66375680 15726 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/25277/statm): 16205 15726 145 145 0 16060 0 [pid=25277] vsize: 64820 Current children cumulated CPU time (s) 348.7 Current children cumulated vsize (Kb) 66944 [startup+360.034 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 25277 Raw data (/proc/25273/stat): 25273 (minisat+_script) S 25272 25273 8263 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785310562 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/25273/statm): 531 226 485 147 0 384 0 [pid=25273] vsize: 2124 Raw data (/proc/25277/stat): 25277 (minisat+_64-bit) R 25273 25273 8263 0 -1 0 16301 0 0 0 35762 105 0 0 25 0 1 0 1785310567 68096000 16148 4294967295 134512640 135094434 3221224448 3221223104 134558159 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/25277/statm): 16625 16148 145 145 0 16480 0 [pid=25277] vsize: 66500 Current children cumulated CPU time (s) 358.67 Current children cumulated vsize (Kb) 68624 [startup+370.035 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 25277 Raw data (/proc/25273/stat): 25273 (minisat+_script) S 25272 25273 8263 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785310562 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/25273/statm): 531 226 485 147 0 384 0 [pid=25273] vsize: 2124 Raw data (/proc/25277/stat): 25277 (minisat+_64-bit) R 25273 25273 8263 0 -1 0 16669 0 0 0 36754 109 0 0 25 0 1 0 1785310567 69595136 16516 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/25277/statm): 16991 16516 145 145 0 16846 0 [pid=25277] vsize: 67964 Current children cumulated CPU time (s) 368.63 Current children cumulated vsize (Kb) 70088 [startup+380.036 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 25277 Raw data (/proc/25273/stat): 25273 (minisat+_script) S 25272 25273 8263 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785310562 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/25273/statm): 531 226 485 147 0 384 0 [pid=25273] vsize: 2124 Raw data (/proc/25277/stat): 25277 (minisat+_64-bit) R 25273 25273 8263 0 -1 0 17055 0 0 0 37747 112 0 0 25 0 1 0 1785310567 71168000 16902 4294967295 134512640 135094434 3221224448 3221223104 134558007 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/25277/statm): 17375 16902 145 145 0 17230 0 [pid=25277] vsize: 69500 Current children cumulated CPU time (s) 378.59 Current children cumulated vsize (Kb) 71624 [startup+390.037 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 25277 Raw data (/proc/25273/stat): 25273 (minisat+_script) S 25272 25273 8263 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785310562 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/25273/statm): 531 226 485 147 0 384 0 [pid=25273] vsize: 2124 Raw data (/proc/25277/stat): 25277 (minisat+_64-bit) R 25273 25273 8263 0 -1 0 17414 0 0 0 38740 115 0 0 25 0 1 0 1785310567 72634368 17261 4294967295 134512640 135094434 3221224448 3221223104 134557914 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/25277/statm): 17733 17261 145 145 0 17588 0 [pid=25277] vsize: 70932 Current children cumulated CPU time (s) 388.55 Current children cumulated vsize (Kb) 73056 [startup+400.037 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 25277 Raw data (/proc/25273/stat): 25273 (minisat+_script) S 25272 25273 8263 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785310562 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/25273/statm): 531 226 485 147 0 384 0 [pid=25273] vsize: 2124 Raw data (/proc/25277/stat): 25277 (minisat+_64-bit) R 25273 25273 8263 0 -1 0 17695 0 0 0 39734 117 0 0 25 0 1 0 1785310567 73781248 17542 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/25277/statm): 18013 17542 145 145 0 17868 0 [pid=25277] vsize: 72052 Current children cumulated CPU time (s) 398.51 Current children cumulated vsize (Kb) 74176 [startup+410.038 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 25277 Raw data (/proc/25273/stat): 25273 (minisat+_script) S 25272 25273 8263 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785310562 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/25273/statm): 531 226 485 147 0 384 0 [pid=25273] vsize: 2124 Raw data (/proc/25277/stat): 25277 (minisat+_64-bit) R 25273 25273 8263 0 -1 0 18007 0 0 0 40729 119 0 0 25 0 1 0 1785310567 75046912 17854 4294967295 134512640 135094434 3221224448 3221223104 134558159 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/25277/statm): 18322 17854 145 145 0 18177 0 [pid=25277] vsize: 73288 Current children cumulated CPU time (s) 408.48 Current children cumulated vsize (Kb) 75412 [startup+420.038 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 25277 Raw data (/proc/25273/stat): 25273 (minisat+_script) S 25272 25273 8263 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785310562 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/25273/statm): 531 226 485 147 0 384 0 [pid=25273] vsize: 2124 Raw data (/proc/25277/stat): 25277 (minisat+_64-bit) R 25273 25273 8263 0 -1 0 18362 0 0 0 41722 122 0 0 25 0 1 0 1785310567 76492800 18209 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/25277/statm): 18675 18209 145 145 0 18530 0 [pid=25277] vsize: 74700 Current children cumulated CPU time (s) 418.44 Current children cumulated vsize (Kb) 76824 [startup+430.039 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 25277 Raw data (/proc/25273/stat): 25273 (minisat+_script) S 25272 25273 8263 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785310562 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/25273/statm): 531 226 485 147 0 384 0 [pid=25273] vsize: 2124 Raw data (/proc/25277/stat): 25277 (minisat+_64-bit) R 25273 25273 8263 0 -1 0 18717 0 0 0 42716 124 0 0 25 0 1 0 1785310567 77942784 18564 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/25277/statm): 19029 18564 145 145 0 18884 0 [pid=25277] vsize: 76116 Current children cumulated CPU time (s) 428.4 Current children cumulated vsize (Kb) 78240 [startup+440.04 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 25277 Raw data (/proc/25273/stat): 25273 (minisat+_script) S 25272 25273 8263 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785310562 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/25273/statm): 531 226 485 147 0 384 0 [pid=25273] vsize: 2124 Raw data (/proc/25277/stat): 25277 (minisat+_64-bit) R 25273 25273 8263 0 -1 0 19122 0 0 0 43709 128 0 0 25 0 1 0 1785310567 79593472 18969 4294967295 134512640 135094434 3221224448 3221223120 134556252 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/25277/statm): 19432 18969 145 145 0 19287 0 [pid=25277] vsize: 77728 Current children cumulated CPU time (s) 438.37 Current children cumulated vsize (Kb) 79852 [startup+450.041 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 25277 Raw data (/proc/25273/stat): 25273 (minisat+_script) S 25272 25273 8263 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785310562 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/25273/statm): 531 226 485 147 0 384 0 [pid=25273] vsize: 2124 Raw data (/proc/25277/stat): 25277 (minisat+_64-bit) R 25273 25273 8263 0 -1 0 19481 0 0 0 44703 130 0 0 25 0 1 0 1785310567 81055744 19328 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/25277/statm): 19789 19328 145 145 0 19644 0 [pid=25277] vsize: 79156 Current children cumulated CPU time (s) 448.33 Current children cumulated vsize (Kb) 81280 [startup+460.043 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 25277 Raw data (/proc/25273/stat): 25273 (minisat+_script) S 25272 25273 8263 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785310562 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/25273/statm): 531 226 485 147 0 384 0 [pid=25273] vsize: 2124 Raw data (/proc/25277/stat): 25277 (minisat+_64-bit) R 25273 25273 8263 0 -1 0 19727 0 0 0 45698 132 0 0 25 0 1 0 1785310567 82055168 19574 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/25277/statm): 20033 19574 145 145 0 19888 0 [pid=25277] vsize: 80132 Current children cumulated CPU time (s) 458.3 Current children cumulated vsize (Kb) 82256 [startup+470.044 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 25277 Raw data (/proc/25273/stat): 25273 (minisat+_script) S 25272 25273 8263 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785310562 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/25273/statm): 531 226 485 147 0 384 0 [pid=25273] vsize: 2124 Raw data (/proc/25277/stat): 25277 (minisat+_64-bit) R 25273 25273 8263 0 -1 0 19996 0 0 0 46693 134 0 0 25 0 1 0 1785310567 83148800 19843 4294967295 134512640 135094434 3221224448 3221223108 134553482 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/25277/statm): 20300 19843 145 145 0 20155 0 [pid=25277] vsize: 81200 Current children cumulated CPU time (s) 468.27 Current children cumulated vsize (Kb) 83324 [startup+480.044 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 25277 Raw data (/proc/25273/stat): 25273 (minisat+_script) S 25272 25273 8263 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785310562 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/25273/statm): 531 226 485 147 0 384 0 [pid=25273] vsize: 2124 Raw data (/proc/25277/stat): 25277 (minisat+_64-bit) R 25273 25273 8263 0 -1 0 20258 0 0 0 47688 137 0 0 25 0 1 0 1785310567 84217856 20105 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/25277/statm): 20561 20105 145 145 0 20416 0 [pid=25277] vsize: 82244 Current children cumulated CPU time (s) 478.25 Current children cumulated vsize (Kb) 84368 [startup+490.045 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 25277 Raw data (/proc/25273/stat): 25273 (minisat+_script) S 25272 25273 8263 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785310562 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/25273/statm): 531 226 485 147 0 384 0 [pid=25273] vsize: 2124 Raw data (/proc/25277/stat): 25277 (minisat+_64-bit) R 25273 25273 8263 0 -1 0 20516 0 0 0 48682 139 0 0 25 0 1 0 1785310567 85266432 20363 4294967295 134512640 135094434 3221224448 3221223040 134557416 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/25277/statm): 20817 20363 145 145 0 20672 0 [pid=25277] vsize: 83268 Current children cumulated CPU time (s) 488.21 Current children cumulated vsize (Kb) 85392 [startup+500.045 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 25277 Raw data (/proc/25273/stat): 25273 (minisat+_script) S 25272 25273 8263 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785310562 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/25273/statm): 531 226 485 147 0 384 0 [pid=25273] vsize: 2124 Raw data (/proc/25277/stat): 25277 (minisat+_64-bit) R 25273 25273 8263 0 -1 0 20768 0 0 0 49678 142 0 0 25 0 1 0 1785310567 86290432 20615 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/25277/statm): 21067 20615 145 145 0 20922 0 [pid=25277] vsize: 84268 Current children cumulated CPU time (s) 498.2 Current children cumulated vsize (Kb) 86392 [startup+510.047 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 25277 Raw data (/proc/25273/stat): 25273 (minisat+_script) S 25272 25273 8263 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785310562 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/25273/statm): 531 226 485 147 0 384 0 [pid=25273] vsize: 2124 Raw data (/proc/25277/stat): 25277 (minisat+_64-bit) R 25273 25273 8263 0 -1 0 20939 0 0 0 50675 143 0 0 25 0 1 0 1785310567 86990848 20786 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/25277/statm): 21238 20786 145 145 0 21093 0 [pid=25277] vsize: 84952 Current children cumulated CPU time (s) 508.18 Current children cumulated vsize (Kb) 87076 [startup+520.048 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 25277 Raw data (/proc/25273/stat): 25273 (minisat+_script) S 25272 25273 8263 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785310562 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/25273/statm): 531 226 485 147 0 384 0 [pid=25273] vsize: 2124 Raw data (/proc/25277/stat): 25277 (minisat+_64-bit) R 25273 25273 8263 0 -1 0 21195 0 0 0 51670 145 0 0 24 0 1 0 1785310567 88035328 21042 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/25277/statm): 21493 21042 145 145 0 21348 0 [pid=25277] vsize: 85972 Current children cumulated CPU time (s) 518.15 Current children cumulated vsize (Kb) 88096 [startup+530.05 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 25277 Raw data (/proc/25273/stat): 25273 (minisat+_script) S 25272 25273 8263 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785310562 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/25273/statm): 531 226 485 147 0 384 0 [pid=25273] vsize: 2124 Raw data (/proc/25277/stat): 25277 (minisat+_64-bit) R 25273 25273 8263 0 -1 0 21444 0 0 0 52665 148 0 0 25 0 1 0 1785310567 88858624 21244 4294967295 134512640 135094434 3221224448 3221223040 134784942 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/25277/statm): 21694 21244 145 145 0 21549 0 [pid=25277] vsize: 86776 Current children cumulated CPU time (s) 528.13 Current children cumulated vsize (Kb) 88900 [startup+540.052 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 25277 Raw data (/proc/25273/stat): 25273 (minisat+_script) S 25272 25273 8263 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785310562 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/25273/statm): 531 226 485 147 0 384 0 [pid=25273] vsize: 2124 Raw data (/proc/25277/stat): 25277 (minisat+_64-bit) R 25273 25273 8263 0 -1 0 21444 0 0 0 53665 148 0 0 25 0 1 0 1785310567 88858624 21244 4294967295 134512640 135094434 3221224448 3221223040 134557273 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/25277/statm): 21694 21244 145 145 0 21549 0 [pid=25277] vsize: 86776 Current children cumulated CPU time (s) 538.13 Current children cumulated vsize (Kb) 88900 [startup+550.052 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 25277 Raw data (/proc/25273/stat): 25273 (minisat+_script) S 25272 25273 8263 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785310562 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/25273/statm): 531 226 485 147 0 384 0 [pid=25273] vsize: 2124 Raw data (/proc/25277/stat): 25277 (minisat+_64-bit) R 25273 25273 8263 0 -1 0 21444 0 0 0 54665 148 0 0 25 0 1 0 1785310567 88858624 21244 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/25277/statm): 21694 21244 145 145 0 21549 0 [pid=25277] vsize: 86776 Current children cumulated CPU time (s) 548.13 Current children cumulated vsize (Kb) 88900 [startup+560.053 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 25277 Raw data (/proc/25273/stat): 25273 (minisat+_script) S 25272 25273 8263 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785310562 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/25273/statm): 531 226 485 147 0 384 0 [pid=25273] vsize: 2124 Raw data (/proc/25277/stat): 25277 (minisat+_64-bit) R 25273 25273 8263 0 -1 0 21444 0 0 0 55664 149 0 0 25 0 1 0 1785310567 88858624 21244 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/25277/statm): 21694 21244 145 145 0 21549 0 [pid=25277] vsize: 86776 Current children cumulated CPU time (s) 558.13 Current children cumulated vsize (Kb) 88900 [startup+570.055 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 25277 Raw data (/proc/25273/stat): 25273 (minisat+_script) S 25272 25273 8263 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785310562 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/25273/statm): 531 226 485 147 0 384 0 [pid=25273] vsize: 2124 Raw data (/proc/25277/stat): 25277 (minisat+_64-bit) R 25273 25273 8263 0 -1 0 21444 0 0 0 56664 149 0 0 25 0 1 0 1785310567 88858624 21244 4294967295 134512640 135094434 3221224448 3221223120 134555560 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/25277/statm): 21694 21244 145 145 0 21549 0 [pid=25277] vsize: 86776 Current children cumulated CPU time (s) 568.13 Current children cumulated vsize (Kb) 88900 [startup+580.057 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 25277 Raw data (/proc/25273/stat): 25273 (minisat+_script) S 25272 25273 8263 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785310562 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/25273/statm): 531 226 485 147 0 384 0 [pid=25273] vsize: 2124 Raw data (/proc/25277/stat): 25277 (minisat+_64-bit) R 25273 25273 8263 0 -1 0 21444 0 0 0 57664 150 0 0 25 0 1 0 1785310567 88858624 21244 4294967295 134512640 135094434 3221224448 3221223100 134558255 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/25277/statm): 21694 21244 145 145 0 21549 0 [pid=25277] vsize: 86776 Current children cumulated CPU time (s) 578.14 Current children cumulated vsize (Kb) 88900 [startup+590.058 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 25277 Raw data (/proc/25273/stat): 25273 (minisat+_script) S 25272 25273 8263 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785310562 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/25273/statm): 531 226 485 147 0 384 0 [pid=25273] vsize: 2124 Raw data (/proc/25277/stat): 25277 (minisat+_64-bit) R 25273 25273 8263 0 -1 0 21444 0 0 0 58663 150 0 0 25 0 1 0 1785310567 88858624 21244 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/25277/statm): 21694 21244 145 145 0 21549 0 [pid=25277] vsize: 86776 Current children cumulated CPU time (s) 588.13 Current children cumulated vsize (Kb) 88900 [startup+600.058 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 25277 Raw data (/proc/25273/stat): 25273 (minisat+_script) S 25272 25273 8263 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785310562 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/25273/statm): 531 226 485 147 0 384 0 [pid=25273] vsize: 2124 Raw data (/proc/25277/stat): 25277 (minisat+_64-bit) R 25273 25273 8263 0 -1 0 21444 0 0 0 59663 150 0 0 25 0 1 0 1785310567 88858624 21244 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/25277/statm): 21694 21244 145 145 0 21549 0 [pid=25277] vsize: 86776 Current children cumulated CPU time (s) 598.13 Current children cumulated vsize (Kb) 88900 [startup+610.06 s] Raw data (loadavg): 0.99 0.97 0.91 3/57 25277 Raw data (/proc/25273/stat): 25273 (minisat+_script) S 25272 25273 8263 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785310562 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/25273/statm): 531 226 485 147 0 384 0 [pid=25273] vsize: 2124 Raw data (/proc/25277/stat): 25277 (minisat+_64-bit) R 25273 25273 8263 0 -1 0 21444 0 0 0 60663 151 0 0 25 0 1 0 1785310567 88858624 21244 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/25277/statm): 21694 21244 145 145 0 21549 0 [pid=25277] vsize: 86776 Current children cumulated CPU time (s) 608.14 Current children cumulated vsize (Kb) 88900 [startup+620.061 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 25277 Raw data (/proc/25273/stat): 25273 (minisat+_script) S 25272 25273 8263 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785310562 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/25273/statm): 531 226 485 147 0 384 0 [pid=25273] vsize: 2124 Raw data (/proc/25277/stat): 25277 (minisat+_64-bit) R 25273 25273 8263 0 -1 0 21444 0 0 0 61662 151 0 0 25 0 1 0 1785310567 88858624 21244 4294967295 134512640 135094434 3221224448 3221223104 134558002 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/25277/statm): 21694 21244 145 145 0 21549 0 [pid=25277] vsize: 86776 Current children cumulated CPU time (s) 618.13 Current children cumulated vsize (Kb) 88900 [startup+630.063 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 25277 Raw data (/proc/25273/stat): 25273 (minisat+_script) S 25272 25273 8263 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785310562 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/25273/statm): 531 226 485 147 0 384 0 [pid=25273] vsize: 2124 Raw data (/proc/25277/stat): 25277 (minisat+_64-bit) R 25273 25273 8263 0 -1 0 21444 0 0 0 62662 152 0 0 25 0 1 0 1785310567 88858624 21244 4294967295 134512640 135094434 3221224448 3221223104 134558159 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/25277/statm): 21694 21244 145 145 0 21549 0 [pid=25277] vsize: 86776 Current children cumulated CPU time (s) 628.14 Current children cumulated vsize (Kb) 88900 [startup+640.065 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 25277 Raw data (/proc/25273/stat): 25273 (minisat+_script) S 25272 25273 8263 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785310562 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/25273/statm): 531 226 485 147 0 384 0 [pid=25273] vsize: 2124 Raw data (/proc/25277/stat): 25277 (minisat+_64-bit) R 25273 25273 8263 0 -1 0 21444 0 0 0 63662 152 0 0 25 0 1 0 1785310567 88858624 21244 4294967295 134512640 135094434 3221224448 3221223104 134558026 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/25277/statm): 21694 21244 145 145 0 21549 0 [pid=25277] vsize: 86776 Current children cumulated CPU time (s) 638.14 Current children cumulated vsize (Kb) 88900 [startup+650.066 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 25277 Raw data (/proc/25273/stat): 25273 (minisat+_script) S 25272 25273 8263 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785310562 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/25273/statm): 531 226 485 147 0 384 0 [pid=25273] vsize: 2124 Raw data (/proc/25277/stat): 25277 (minisat+_64-bit) R 25273 25273 8263 0 -1 0 21444 0 0 0 64661 152 0 0 25 0 1 0 1785310567 88858624 21244 4294967295 134512640 135094434 3221224448 3221223120 134555830 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/25277/statm): 21694 21244 145 145 0 21549 0 [pid=25277] vsize: 86776 Current children cumulated CPU time (s) 648.13 Current children cumulated vsize (Kb) 88900 [startup+660.067 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 25277 Raw data (/proc/25273/stat): 25273 (minisat+_script) S 25272 25273 8263 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785310562 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/25273/statm): 531 226 485 147 0 384 0 [pid=25273] vsize: 2124 Raw data (/proc/25277/stat): 25277 (minisat+_64-bit) R 25273 25273 8263 0 -1 0 21444 0 0 0 65661 153 0 0 25 0 1 0 1785310567 88858624 21244 4294967295 134512640 135094434 3221224448 3221223104 134557962 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/25277/statm): 21694 21244 145 145 0 21549 0 [pid=25277] vsize: 86776 Current children cumulated CPU time (s) 658.14 Current children cumulated vsize (Kb) 88900 [startup+670.069 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 25277 Raw data (/proc/25273/stat): 25273 (minisat+_script) S 25272 25273 8263 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785310562 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/25273/statm): 531 226 485 147 0 384 0 [pid=25273] vsize: 2124 Raw data (/proc/25277/stat): 25277 (minisat+_64-bit) R 25273 25273 8263 0 -1 0 21444 0 0 0 66660 153 0 0 25 0 1 0 1785310567 88858624 21244 4294967295 134512640 135094434 3221224448 3221223072 134562057 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/25277/statm): 21694 21244 145 145 0 21549 0 [pid=25277] vsize: 86776 Current children cumulated CPU time (s) 668.13 Current children cumulated vsize (Kb) 88900 [startup+680.07 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 25277 Raw data (/proc/25273/stat): 25273 (minisat+_script) S 25272 25273 8263 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785310562 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/25273/statm): 531 226 485 147 0 384 0 [pid=25273] vsize: 2124 Raw data (/proc/25277/stat): 25277 (minisat+_64-bit) R 25273 25273 8263 0 -1 0 21444 0 0 0 67661 153 0 0 25 0 1 0 1785310567 88858624 21244 4294967295 134512640 135094434 3221224448 3221223104 134557956 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/25277/statm): 21694 21244 145 145 0 21549 0 [pid=25277] vsize: 86776 Current children cumulated CPU time (s) 678.14 Current children cumulated vsize (Kb) 88900 [startup+690.071 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 25277 Raw data (/proc/25273/stat): 25273 (minisat+_script) S 25272 25273 8263 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785310562 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/25273/statm): 531 226 485 147 0 384 0 [pid=25273] vsize: 2124 Raw data (/proc/25277/stat): 25277 (minisat+_64-bit) R 25273 25273 8263 0 -1 0 21444 0 0 0 68661 153 0 0 25 0 1 0 1785310567 88858624 21244 4294967295 134512640 135094434 3221224448 3221223040 134557157 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/25277/statm): 21694 21244 145 145 0 21549 0 [pid=25277] vsize: 86776 Current children cumulated CPU time (s) 688.14 Current children cumulated vsize (Kb) 88900 [startup+700.072 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 25277 Raw data (/proc/25273/stat): 25273 (minisat+_script) S 25272 25273 8263 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785310562 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/25273/statm): 531 226 485 147 0 384 0 [pid=25273] vsize: 2124 Raw data (/proc/25277/stat): 25277 (minisat+_64-bit) R 25273 25273 8263 0 -1 0 21444 0 0 0 69661 154 0 0 25 0 1 0 1785310567 88858624 21244 4294967295 134512640 135094434 3221224448 3221223120 134555576 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/25277/statm): 21694 21244 145 145 0 21549 0 [pid=25277] vsize: 86776 Current children cumulated CPU time (s) 698.15 Current children cumulated vsize (Kb) 88900 [startup+710.074 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 25277 Raw data (/proc/25273/stat): 25273 (minisat+_script) S 25272 25273 8263 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785310562 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/25273/statm): 531 226 485 147 0 384 0 [pid=25273] vsize: 2124 Raw data (/proc/25277/stat): 25277 (minisat+_64-bit) R 25273 25273 8263 0 -1 0 21444 0 0 0 70661 154 0 0 25 0 1 0 1785310567 88858624 21244 4294967295 134512640 135094434 3221224448 3221223104 134558004 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/25277/statm): 21694 21244 145 145 0 21549 0 [pid=25277] vsize: 86776 Current children cumulated CPU time (s) 708.15 Current children cumulated vsize (Kb) 88900 [startup+720.074 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 25277 Raw data (/proc/25273/stat): 25273 (minisat+_script) S 25272 25273 8263 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785310562 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/25273/statm): 531 226 485 147 0 384 0 [pid=25273] vsize: 2124 Raw data (/proc/25277/stat): 25277 (minisat+_64-bit) R 25273 25273 8263 0 -1 0 21444 0 0 0 71661 154 0 0 25 0 1 0 1785310567 88858624 21244 4294967295 134512640 135094434 3221224448 3221223104 134558395 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/25277/statm): 21694 21244 145 145 0 21549 0 [pid=25277] vsize: 86776 Current children cumulated CPU time (s) 718.15 Current children cumulated vsize (Kb) 88900 [startup+730.075 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 25277 Raw data (/proc/25273/stat): 25273 (minisat+_script) S 25272 25273 8263 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785310562 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/25273/statm): 531 226 485 147 0 384 0 [pid=25273] vsize: 2124 Raw data (/proc/25277/stat): 25277 (minisat+_64-bit) R 25273 25273 8263 0 -1 0 21444 0 0 0 72661 154 0 0 25 0 1 0 1785310567 88858624 21244 4294967295 134512640 135094434 3221224448 3221223136 134554746 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/25277/statm): 21694 21244 145 145 0 21549 0 [pid=25277] vsize: 86776 Current children cumulated CPU time (s) 728.15 Current children cumulated vsize (Kb) 88900 [startup+740.076 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 25277 Raw data (/proc/25273/stat): 25273 (minisat+_script) S 25272 25273 8263 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785310562 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/25273/statm): 531 226 485 147 0 384 0 [pid=25273] vsize: 2124 Raw data (/proc/25277/stat): 25277 (minisat+_64-bit) R 25273 25273 8263 0 -1 0 21444 0 0 0 73661 154 0 0 25 0 1 0 1785310567 88858624 21244 4294967295 134512640 135094434 3221224448 3221223104 134558159 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/25277/statm): 21694 21244 145 145 0 21549 0 [pid=25277] vsize: 86776 Current children cumulated CPU time (s) 738.15 Current children cumulated vsize (Kb) 88900 [startup+750.077 s] Raw data (loadavg): 0.99 0.97 0.91 3/57 25277 Raw data (/proc/25273/stat): 25273 (minisat+_script) S 25272 25273 8263 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785310562 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/25273/statm): 531 226 485 147 0 384 0 [pid=25273] vsize: 2124 Raw data (/proc/25277/stat): 25277 (minisat+_64-bit) R 25273 25273 8263 0 -1 0 21444 0 0 0 74662 154 0 0 25 0 1 0 1785310567 88858624 21244 4294967295 134512640 135094434 3221224448 3221223072 134557696 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/25277/statm): 21694 21244 145 145 0 21549 0 [pid=25277] vsize: 86776 Current children cumulated CPU time (s) 748.16 Current children cumulated vsize (Kb) 88900 [startup+760.078 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 25277 Raw data (/proc/25273/stat): 25273 (minisat+_script) S 25272 25273 8263 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785310562 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/25273/statm): 531 226 485 147 0 384 0 [pid=25273] vsize: 2124 Raw data (/proc/25277/stat): 25277 (minisat+_64-bit) R 25273 25273 8263 0 -1 0 21444 0 0 0 75662 154 0 0 25 0 1 0 1785310567 88858624 21244 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/25277/statm): 21694 21244 145 145 0 21549 0 [pid=25277] vsize: 86776 Current children cumulated CPU time (s) 758.16 Current children cumulated vsize (Kb) 88900 [startup+770.079 s] Raw data (loadavg): 1.06 0.99 0.91 2/57 25277 Raw data (/proc/25273/stat): 25273 (minisat+_script) S 25272 25273 8263 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785310562 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/25273/statm): 531 226 485 147 0 384 0 [pid=25273] vsize: 2124 Raw data (/proc/25277/stat): 25277 (minisat+_64-bit) R 25273 25273 8263 0 -1 0 21444 0 0 0 76662 154 0 0 25 0 1 0 1785310567 88858624 21244 4294967295 134512640 135094434 3221224448 3221223104 134557846 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/25277/statm): 21694 21244 145 145 0 21549 0 [pid=25277] vsize: 86776 Current children cumulated CPU time (s) 768.16 Current children cumulated vsize (Kb) 88900 [startup+780.08 s] Raw data (loadavg): 1.05 0.99 0.91 2/57 25277 Raw data (/proc/25273/stat): 25273 (minisat+_script) S 25272 25273 8263 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785310562 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/25273/statm): 531 226 485 147 0 384 0 [pid=25273] vsize: 2124 Raw data (/proc/25277/stat): 25277 (minisat+_64-bit) R 25273 25273 8263 0 -1 0 21444 0 0 0 77662 154 0 0 25 0 1 0 1785310567 88858624 21244 4294967295 134512640 135094434 3221224448 3221223040 134556834 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/25277/statm): 21694 21244 145 145 0 21549 0 [pid=25277] vsize: 86776 Current children cumulated CPU time (s) 778.16 Current children cumulated vsize (Kb) 88900 [startup+790.081 s] Raw data (loadavg): 1.04 0.99 0.91 2/57 25277 Raw data (/proc/25273/stat): 25273 (minisat+_script) S 25272 25273 8263 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785310562 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/25273/statm): 531 226 485 147 0 384 0 [pid=25273] vsize: 2124 Raw data (/proc/25277/stat): 25277 (minisat+_64-bit) R 25273 25273 8263 0 -1 0 21444 0 0 0 78662 154 0 0 25 0 1 0 1785310567 88858624 21244 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/25277/statm): 21694 21244 145 145 0 21549 0 [pid=25277] vsize: 86776 Current children cumulated CPU time (s) 788.16 Current children cumulated vsize (Kb) 88900 [startup+800.081 s] Raw data (loadavg): 1.04 0.99 0.91 2/57 25277 Raw data (/proc/25273/stat): 25273 (minisat+_script) S 25272 25273 8263 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785310562 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/25273/statm): 531 226 485 147 0 384 0 [pid=25273] vsize: 2124 Raw data (/proc/25277/stat): 25277 (minisat+_64-bit) R 25273 25273 8263 0 -1 0 21444 0 0 0 79662 154 0 0 25 0 1 0 1785310567 88858624 21244 4294967295 134512640 135094434 3221224448 3221223040 134556826 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/25277/statm): 21694 21244 145 145 0 21549 0 [pid=25277] vsize: 86776 Current children cumulated CPU time (s) 798.16 Current children cumulated vsize (Kb) 88900 [startup+810.083 s] Raw data (loadavg): 1.03 0.99 0.91 2/57 25277 Raw data (/proc/25273/stat): 25273 (minisat+_script) S 25272 25273 8263 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785310562 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/25273/statm): 531 226 485 147 0 384 0 [pid=25273] vsize: 2124 Raw data (/proc/25277/stat): 25277 (minisat+_64-bit) R 25273 25273 8263 0 -1 0 21444 0 0 0 80663 154 0 0 25 0 1 0 1785310567 88858624 21244 4294967295 134512640 135094434 3221224448 3221223104 134557860 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/25277/statm): 21694 21244 145 145 0 21549 0 [pid=25277] vsize: 86776 Current children cumulated CPU time (s) 808.17 Current children cumulated vsize (Kb) 88900 [startup+820.084 s] Raw data (loadavg): 1.03 0.99 0.91 2/57 25277 Raw data (/proc/25273/stat): 25273 (minisat+_script) S 25272 25273 8263 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785310562 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/25273/statm): 531 226 485 147 0 384 0 [pid=25273] vsize: 2124 Raw data (/proc/25277/stat): 25277 (minisat+_64-bit) R 25273 25273 8263 0 -1 0 21444 0 0 0 81663 154 0 0 25 0 1 0 1785310567 88858624 21244 4294967295 134512640 135094434 3221224448 3221223088 134538541 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/25277/statm): 21694 21244 145 145 0 21549 0 [pid=25277] vsize: 86776 Current children cumulated CPU time (s) 818.17 Current children cumulated vsize (Kb) 88900 [startup+830.086 s] Raw data (loadavg): 1.02 0.99 0.91 2/57 25277 Raw data (/proc/25273/stat): 25273 (minisat+_script) S 25272 25273 8263 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785310562 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/25273/statm): 531 226 485 147 0 384 0 [pid=25273] vsize: 2124 Raw data (/proc/25277/stat): 25277 (minisat+_64-bit) R 25273 25273 8263 0 -1 0 21444 0 0 0 82663 155 0 0 25 0 1 0 1785310567 88858624 21244 4294967295 134512640 135094434 3221224448 3221223040 134557271 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/25277/statm): 21694 21244 145 145 0 21549 0 [pid=25277] vsize: 86776 Current children cumulated CPU time (s) 828.18 Current children cumulated vsize (Kb) 88900 [startup+840.086 s] Raw data (loadavg): 1.02 0.99 0.91 2/57 25277 Raw data (/proc/25273/stat): 25273 (minisat+_script) S 25272 25273 8263 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785310562 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/25273/statm): 531 226 485 147 0 384 0 [pid=25273] vsize: 2124 Raw data (/proc/25277/stat): 25277 (minisat+_64-bit) R 25273 25273 8263 0 -1 0 21444 0 0 0 83663 155 0 0 25 0 1 0 1785310567 88858624 21244 4294967295 134512640 135094434 3221224448 3221223072 134557696 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/25277/statm): 21694 21244 145 145 0 21549 0 [pid=25277] vsize: 86776 Current children cumulated CPU time (s) 838.18 Current children cumulated vsize (Kb) 88900 [startup+850.086 s] Raw data (loadavg): 1.01 0.99 0.91 2/57 25277 Raw data (/proc/25273/stat): 25273 (minisat+_script) S 25272 25273 8263 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785310562 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/25273/statm): 531 226 485 147 0 384 0 [pid=25273] vsize: 2124 Raw data (/proc/25277/stat): 25277 (minisat+_64-bit) R 25273 25273 8263 0 -1 0 21444 0 0 0 84663 155 0 0 25 0 1 0 1785310567 88858624 21244 4294967295 134512640 135094434 3221224448 3221223104 134558246 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/25277/statm): 21694 21244 145 145 0 21549 0 [pid=25277] vsize: 86776 Current children cumulated CPU time (s) 848.18 Current children cumulated vsize (Kb) 88900 [startup+860.087 s] Raw data (loadavg): 1.01 0.99 0.91 2/57 25277 Raw data (/proc/25273/stat): 25273 (minisat+_script) S 25272 25273 8263 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785310562 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/25273/statm): 531 226 485 147 0 384 0 [pid=25273] vsize: 2124 Raw data (/proc/25277/stat): 25277 (minisat+_64-bit) R 25273 25273 8263 0 -1 0 21444 0 0 0 85664 155 0 0 25 0 1 0 1785310567 88858624 21244 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/25277/statm): 21694 21244 145 145 0 21549 0 [pid=25277] vsize: 86776 Current children cumulated CPU time (s) 858.19 Current children cumulated vsize (Kb) 88900 [startup+870.088 s] Raw data (loadavg): 1.01 0.99 0.91 2/57 25277 Raw data (/proc/25273/stat): 25273 (minisat+_script) S 25272 25273 8263 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785310562 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/25273/statm): 531 226 485 147 0 384 0 [pid=25273] vsize: 2124 Raw data (/proc/25277/stat): 25277 (minisat+_64-bit) R 25273 25273 8263 0 -1 0 21444 0 0 0 86664 155 0 0 25 0 1 0 1785310567 88858624 21244 4294967295 134512640 135094434 3221224448 3221223104 134558187 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/25277/statm): 21694 21244 145 145 0 21549 0 [pid=25277] vsize: 86776 Current children cumulated CPU time (s) 868.19 Current children cumulated vsize (Kb) 88900 [startup+880.089 s] Raw data (loadavg): 1.01 0.99 0.91 2/57 25277 Raw data (/proc/25273/stat): 25273 (minisat+_script) S 25272 25273 8263 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785310562 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/25273/statm): 531 226 485 147 0 384 0 [pid=25273] vsize: 2124 Raw data (/proc/25277/stat): 25277 (minisat+_64-bit) R 25273 25273 8263 0 -1 0 21444 0 0 0 87664 155 0 0 25 0 1 0 1785310567 88858624 21244 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/25277/statm): 21694 21244 145 145 0 21549 0 [pid=25277] vsize: 86776 Current children cumulated CPU time (s) 878.19 Current children cumulated vsize (Kb) 88900 [startup+890.09 s] Raw data (loadavg): 1.01 0.99 0.91 2/57 25277 Raw data (/proc/25273/stat): 25273 (minisat+_script) S 25272 25273 8263 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785310562 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/25273/statm): 531 226 485 147 0 384 0 [pid=25273] vsize: 2124 Raw data (/proc/25277/stat): 25277 (minisat+_64-bit) R 25273 25273 8263 0 -1 0 21444 0 0 0 88664 155 0 0 25 0 1 0 1785310567 88858624 21244 4294967295 134512640 135094434 3221224448 3221223040 134557269 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/25277/statm): 21694 21244 145 145 0 21549 0 [pid=25277] vsize: 86776 Current children cumulated CPU time (s) 888.19 Current children cumulated vsize (Kb) 88900 [startup+900.09 s] Raw data (loadavg): 1.00 0.99 0.91 2/57 25277 Raw data (/proc/25273/stat): 25273 (minisat+_script) S 25272 25273 8263 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785310562 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/25273/statm): 531 226 485 147 0 384 0 [pid=25273] vsize: 2124 Raw data (/proc/25277/stat): 25277 (minisat+_64-bit) R 25273 25273 8263 0 -1 0 21444 0 0 0 89664 155 0 0 25 0 1 0 1785310567 88858624 21244 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/25277/statm): 21694 21244 145 145 0 21549 0 [pid=25277] vsize: 86776 Current children cumulated CPU time (s) 898.19 Current children cumulated vsize (Kb) 88900 [startup+910.091 s] Raw data (loadavg): 1.00 0.99 0.91 2/57 25277 Raw data (/proc/25273/stat): 25273 (minisat+_script) S 25272 25273 8263 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785310562 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/25273/statm): 531 226 485 147 0 384 0 [pid=25273] vsize: 2124 Raw data (/proc/25277/stat): 25277 (minisat+_64-bit) R 25273 25273 8263 0 -1 0 21444 0 0 0 90665 155 0 0 25 0 1 0 1785310567 88858624 21244 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/25277/statm): 21694 21244 145 145 0 21549 0 [pid=25277] vsize: 86776 Current children cumulated CPU time (s) 908.2 Current children cumulated vsize (Kb) 88900 [startup+920.092 s] Raw data (loadavg): 1.00 0.99 0.91 2/57 25277 Raw data (/proc/25273/stat): 25273 (minisat+_script) S 25272 25273 8263 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785310562 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/25273/statm): 531 226 485 147 0 384 0 [pid=25273] vsize: 2124 Raw data (/proc/25277/stat): 25277 (minisat+_64-bit) R 25273 25273 8263 0 -1 0 21444 0 0 0 91665 155 0 0 25 0 1 0 1785310567 88858624 21244 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/25277/statm): 21694 21244 145 145 0 21549 0 [pid=25277] vsize: 86776 Current children cumulated CPU time (s) 918.2 Current children cumulated vsize (Kb) 88900 [startup+930.093 s] Raw data (loadavg): 1.00 0.99 0.91 2/57 25277 Raw data (/proc/25273/stat): 25273 (minisat+_script) S 25272 25273 8263 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785310562 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/25273/statm): 531 226 485 147 0 384 0 [pid=25273] vsize: 2124 Raw data (/proc/25277/stat): 25277 (minisat+_64-bit) R 25273 25273 8263 0 -1 0 21444 0 0 0 92665 155 0 0 25 0 1 0 1785310567 88858624 21244 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/25277/statm): 21694 21244 145 145 0 21549 0 [pid=25277] vsize: 86776 Current children cumulated CPU time (s) 928.2 Current children cumulated vsize (Kb) 88900 [startup+940.094 s] Raw data (loadavg): 1.00 0.99 0.91 2/57 25277 Raw data (/proc/25273/stat): 25273 (minisat+_script) S 25272 25273 8263 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785310562 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/25273/statm): 531 226 485 147 0 384 0 [pid=25273] vsize: 2124 Raw data (/proc/25277/stat): 25277 (minisat+_64-bit) R 25273 25273 8263 0 -1 0 21444 0 0 0 93665 155 0 0 25 0 1 0 1785310567 88858624 21244 4294967295 134512640 135094434 3221224448 3221223040 134557202 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/25277/statm): 21694 21244 145 145 0 21549 0 [pid=25277] vsize: 86776 Current children cumulated CPU time (s) 938.2 Current children cumulated vsize (Kb) 88900 [startup+950.095 s] Raw data (loadavg): 1.00 0.99 0.91 2/57 25277 Raw data (/proc/25273/stat): 25273 (minisat+_script) S 25272 25273 8263 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785310562 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/25273/statm): 531 226 485 147 0 384 0 [pid=25273] vsize: 2124 Raw data (/proc/25277/stat): 25277 (minisat+_64-bit) R 25273 25273 8263 0 -1 0 21444 0 0 0 94666 155 0 0 25 0 1 0 1785310567 88858624 21244 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/25277/statm): 21694 21244 145 145 0 21549 0 [pid=25277] vsize: 86776 Current children cumulated CPU time (s) 948.21 Current children cumulated vsize (Kb) 88900 [startup+960.095 s] Raw data (loadavg): 1.00 0.99 0.91 2/57 25277 Raw data (/proc/25273/stat): 25273 (minisat+_script) S 25272 25273 8263 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785310562 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/25273/statm): 531 226 485 147 0 384 0 [pid=25273] vsize: 2124 Raw data (/proc/25277/stat): 25277 (minisat+_64-bit) R 25273 25273 8263 0 -1 0 21444 0 0 0 95666 155 0 0 25 0 1 0 1785310567 88858624 21244 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/25277/statm): 21694 21244 145 145 0 21549 0 [pid=25277] vsize: 86776 Current children cumulated CPU time (s) 958.21 Current children cumulated vsize (Kb) 88900 [startup+970.096 s] Raw data (loadavg): 1.00 0.99 0.91 2/57 25277 Raw data (/proc/25273/stat): 25273 (minisat+_script) S 25272 25273 8263 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785310562 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/25273/statm): 531 226 485 147 0 384 0 [pid=25273] vsize: 2124 Raw data (/proc/25277/stat): 25277 (minisat+_64-bit) R 25273 25273 8263 0 -1 0 21444 0 0 0 96666 155 0 0 25 0 1 0 1785310567 88858624 21244 4294967295 134512640 135094434 3221224448 3221223104 134557866 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/25277/statm): 21694 21244 145 145 0 21549 0 [pid=25277] vsize: 86776 Current children cumulated CPU time (s) 968.21 Current children cumulated vsize (Kb) 88900 [startup+980.097 s] Raw data (loadavg): 1.00 0.99 0.91 2/57 25277 Raw data (/proc/25273/stat): 25273 (minisat+_script) S 25272 25273 8263 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785310562 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/25273/statm): 531 226 485 147 0 384 0 [pid=25273] vsize: 2124 Raw data (/proc/25277/stat): 25277 (minisat+_64-bit) R 25273 25273 8263 0 -1 0 21444 0 0 0 97666 155 0 0 25 0 1 0 1785310567 88858624 21244 4294967295 134512640 135094434 3221224448 3221223072 134557726 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/25277/statm): 21694 21244 145 145 0 21549 0 [pid=25277] vsize: 86776 Current children cumulated CPU time (s) 978.21 Current children cumulated vsize (Kb) 88900 [startup+990.098 s] Raw data (loadavg): 1.00 0.99 0.91 2/57 25277 Raw data (/proc/25273/stat): 25273 (minisat+_script) S 25272 25273 8263 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785310562 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/25273/statm): 531 226 485 147 0 384 0 [pid=25273] vsize: 2124 Raw data (/proc/25277/stat): 25277 (minisat+_64-bit) R 25273 25273 8263 0 -1 0 21444 0 0 0 98666 155 0 0 25 0 1 0 1785310567 88858624 21244 4294967295 134512640 135094434 3221224448 3221223104 134558159 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/25277/statm): 21694 21244 145 145 0 21549 0 [pid=25277] vsize: 86776 Current children cumulated CPU time (s) 988.21 Current children cumulated vsize (Kb) 88900 [startup+1000.1 s] Raw data (loadavg): 1.00 0.99 0.91 2/57 25277 Raw data (/proc/25273/stat): 25273 (minisat+_script) S 25272 25273 8263 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785310562 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/25273/statm): 531 226 485 147 0 384 0 [pid=25273] vsize: 2124 Raw data (/proc/25277/stat): 25277 (minisat+_64-bit) R 25273 25273 8263 0 -1 0 21444 0 0 0 99665 156 0 0 25 0 1 0 1785310567 88858624 21244 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/25277/statm): 21694 21244 145 145 0 21549 0 [pid=25277] vsize: 86776 Current children cumulated CPU time (s) 998.21 Current children cumulated vsize (Kb) 88900 [startup+1010.1 s] Raw data (loadavg): 1.00 0.99 0.91 2/57 25277 Raw data (/proc/25273/stat): 25273 (minisat+_script) S 25272 25273 8263 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785310562 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/25273/statm): 531 226 485 147 0 384 0 [pid=25273] vsize: 2124 Raw data (/proc/25277/stat): 25277 (minisat+_64-bit) R 25273 25273 8263 0 -1 0 21444 0 0 0 100665 156 0 0 25 0 1 0 1785310567 88858624 21244 4294967295 134512640 135094434 3221224448 3221223136 134554723 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/25277/statm): 21694 21244 145 145 0 21549 0 [pid=25277] vsize: 86776 Current children cumulated CPU time (s) 1008.21 Current children cumulated vsize (Kb) 88900 [startup+1020.1 s] Raw data (loadavg): 1.00 0.99 0.91 2/57 25277 Raw data (/proc/25273/stat): 25273 (minisat+_script) S 25272 25273 8263 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785310562 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/25273/statm): 531 226 485 147 0 384 0 [pid=25273] vsize: 2124 Raw data (/proc/25277/stat): 25277 (minisat+_64-bit) R 25273 25273 8263 0 -1 0 21444 0 0 0 101665 156 0 0 25 0 1 0 1785310567 88858624 21244 4294967295 134512640 135094434 3221224448 3221223136 134554731 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/25277/statm): 21694 21244 145 145 0 21549 0 [pid=25277] vsize: 86776 Current children cumulated CPU time (s) 1018.21 Current children cumulated vsize (Kb) 88900 [startup+1030.1 s] Raw data (loadavg): 1.00 0.99 0.91 2/57 25277 Raw data (/proc/25273/stat): 25273 (minisat+_script) S 25272 25273 8263 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785310562 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/25273/statm): 531 226 485 147 0 384 0 [pid=25273] vsize: 2124 Raw data (/proc/25277/stat): 25277 (minisat+_64-bit) R 25273 25273 8263 0 -1 0 21445 0 0 0 102665 156 0 0 25 0 1 0 1785310567 88858624 21245 4294967295 134512640 135094434 3221224448 3221223104 134558123 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/25277/statm): 21694 21245 145 145 0 21549 0 [pid=25277] vsize: 86776 Current children cumulated CPU time (s) 1028.21 Current children cumulated vsize (Kb) 88900 [startup+1040.1 s] Raw data (loadavg): 1.00 0.99 0.91 2/57 25277 Raw data (/proc/25273/stat): 25273 (minisat+_script) S 25272 25273 8263 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785310562 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/25273/statm): 531 226 485 147 0 384 0 [pid=25273] vsize: 2124 Raw data (/proc/25277/stat): 25277 (minisat+_64-bit) R 25273 25273 8263 0 -1 0 21445 0 0 0 103666 156 0 0 25 0 1 0 1785310567 88858624 21245 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/25277/statm): 21694 21245 145 145 0 21549 0 [pid=25277] vsize: 86776 Current children cumulated CPU time (s) 1038.22 Current children cumulated vsize (Kb) 88900 [startup+1050.1 s] Raw data (loadavg): 1.00 0.99 0.91 2/57 25277 Raw data (/proc/25273/stat): 25273 (minisat+_script) S 25272 25273 8263 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785310562 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/25273/statm): 531 226 485 147 0 384 0 [pid=25273] vsize: 2124 Raw data (/proc/25277/stat): 25277 (minisat+_64-bit) R 25273 25273 8263 0 -1 0 21445 0 0 0 104666 156 0 0 25 0 1 0 1785310567 88858624 21245 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/25277/statm): 21694 21245 145 145 0 21549 0 [pid=25277] vsize: 86776 Current children cumulated CPU time (s) 1048.22 Current children cumulated vsize (Kb) 88900 [startup+1060.1 s] Raw data (loadavg): 1.00 0.99 0.91 2/57 25277 Raw data (/proc/25273/stat): 25273 (minisat+_script) S 25272 25273 8263 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785310562 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/25273/statm): 531 226 485 147 0 384 0 [pid=25273] vsize: 2124 Raw data (/proc/25277/stat): 25277 (minisat+_64-bit) R 25273 25273 8263 0 -1 0 21456 0 0 0 105666 156 0 0 25 0 1 0 1785310567 88903680 21256 4294967295 134512640 135094434 3221224448 3221223104 134557937 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/25277/statm): 21705 21256 145 145 0 21560 0 [pid=25277] vsize: 86820 Current children cumulated CPU time (s) 1058.22 Current children cumulated vsize (Kb) 88944 [startup+1070.1 s] Raw data (loadavg): 1.00 0.99 0.91 2/57 25277 Raw data (/proc/25273/stat): 25273 (minisat+_script) S 25272 25273 8263 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785310562 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/25273/statm): 531 226 485 147 0 384 0 [pid=25273] vsize: 2124 Raw data (/proc/25277/stat): 25277 (minisat+_64-bit) R 25273 25273 8263 0 -1 0 21712 0 0 0 106661 159 0 0 25 0 1 0 1785310567 89952256 21512 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/25277/statm): 21961 21512 145 145 0 21816 0 [pid=25277] vsize: 87844 Current children cumulated CPU time (s) 1068.2 Current children cumulated vsize (Kb) 89968 [startup+1080.11 s] Raw data (loadavg): 1.00 0.99 0.91 2/57 25277 Raw data (/proc/25273/stat): 25273 (minisat+_script) S 25272 25273 8263 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785310562 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/25273/statm): 531 226 485 147 0 384 0 [pid=25273] vsize: 2124 Raw data (/proc/25277/stat): 25277 (minisat+_64-bit) R 25273 25273 8263 0 -1 0 21940 0 0 0 107658 160 0 0 25 0 1 0 1785310567 90886144 21740 4294967295 134512640 135094434 3221224448 3221223136 134554739 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/25277/statm): 22189 21740 145 145 0 22044 0 [pid=25277] vsize: 88756 Current children cumulated CPU time (s) 1078.18 Current children cumulated vsize (Kb) 90880 [startup+1090.11 s] Raw data (loadavg): 1.00 0.99 0.91 2/57 25277 Raw data (/proc/25273/stat): 25273 (minisat+_script) S 25272 25273 8263 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785310562 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/25273/statm): 531 226 485 147 0 384 0 [pid=25273] vsize: 2124 Raw data (/proc/25277/stat): 25277 (minisat+_64-bit) R 25273 25273 8263 0 -1 0 22121 0 0 0 108654 162 0 0 25 0 1 0 1785310567 91627520 21921 4294967295 134512640 135094434 3221224448 3221223104 134557948 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/25277/statm): 22370 21921 145 145 0 22225 0 [pid=25277] vsize: 89480 Current children cumulated CPU time (s) 1088.16 Current children cumulated vsize (Kb) 91604 [startup+1100.11 s] Raw data (loadavg): 1.00 0.99 0.91 2/57 25277 Raw data (/proc/25273/stat): 25273 (minisat+_script) S 25272 25273 8263 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785310562 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/25273/statm): 531 226 485 147 0 384 0 [pid=25273] vsize: 2124 Raw data (/proc/25277/stat): 25277 (minisat+_64-bit) R 25273 25273 8263 0 -1 0 22341 0 0 0 109651 164 0 0 25 0 1 0 1785310567 92532736 22141 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/25277/statm): 22591 22141 145 145 0 22446 0 [pid=25277] vsize: 90364 Current children cumulated CPU time (s) 1098.15 Current children cumulated vsize (Kb) 92488 [startup+1110.11 s] Raw data (loadavg): 1.00 0.99 0.91 2/57 25277 Raw data (/proc/25273/stat): 25273 (minisat+_script) S 25272 25273 8263 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785310562 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/25273/statm): 531 226 485 147 0 384 0 [pid=25273] vsize: 2124 Raw data (/proc/25277/stat): 25277 (minisat+_64-bit) R 25273 25273 8263 0 -1 0 22580 0 0 0 110646 166 0 0 25 0 1 0 1785310567 93515776 22380 4294967295 134512640 135094434 3221224448 3221223104 134558126 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/25277/statm): 22831 22380 145 145 0 22686 0 [pid=25277] vsize: 91324 Current children cumulated CPU time (s) 1108.12 Current children cumulated vsize (Kb) 93448 [startup+1120.11 s] Raw data (loadavg): 1.00 0.99 0.91 2/57 25277 Raw data (/proc/25273/stat): 25273 (minisat+_script) S 25272 25273 8263 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785310562 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/25273/statm): 531 226 485 147 0 384 0 [pid=25273] vsize: 2124 Raw data (/proc/25277/stat): 25277 (minisat+_64-bit) R 25273 25273 8263 0 -1 0 22806 0 0 0 111642 169 0 0 25 0 1 0 1785310567 94961664 22606 4294967295 134512640 135094434 3221224448 3221223104 134558153 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/25277/statm): 23184 22606 145 145 0 23039 0 [pid=25277] vsize: 92736 Current children cumulated CPU time (s) 1118.11 Current children cumulated vsize (Kb) 94860 [startup+1130.11 s] Raw data (loadavg): 1.00 0.99 0.91 2/57 25277 Raw data (/proc/25273/stat): 25273 (minisat+_script) S 25272 25273 8263 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785310562 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/25273/statm): 531 226 485 147 0 384 0 [pid=25273] vsize: 2124 Raw data (/proc/25277/stat): 25277 (minisat+_64-bit) R 25273 25273 8263 0 -1 0 23019 0 0 0 112638 171 0 0 25 0 1 0 1785310567 95825920 22819 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/25277/statm): 23395 22819 145 145 0 23250 0 [pid=25277] vsize: 93580 Current children cumulated CPU time (s) 1128.09 Current children cumulated vsize (Kb) 95704 [startup+1140.11 s] Raw data (loadavg): 1.00 0.99 0.91 2/57 25277 Raw data (/proc/25273/stat): 25273 (minisat+_script) S 25272 25273 8263 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785310562 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/25273/statm): 531 226 485 147 0 384 0 [pid=25273] vsize: 2124 Raw data (/proc/25277/stat): 25277 (minisat+_64-bit) R 25273 25273 8263 0 -1 0 23226 0 0 0 113634 173 0 0 25 0 1 0 1785310567 96665600 23026 4294967295 134512640 135094434 3221224448 3221223104 134557928 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/25277/statm): 23600 23026 145 145 0 23455 0 [pid=25277] vsize: 94400 Current children cumulated CPU time (s) 1138.07 Current children cumulated vsize (Kb) 96524 [startup+1150.11 s] Raw data (loadavg): 1.00 0.99 0.91 2/57 25277 Raw data (/proc/25273/stat): 25273 (minisat+_script) S 25272 25273 8263 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785310562 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/25273/statm): 531 226 485 147 0 384 0 [pid=25273] vsize: 2124 Raw data (/proc/25277/stat): 25277 (minisat+_64-bit) R 25273 25273 8263 0 -1 0 23426 0 0 0 114631 175 0 0 25 0 1 0 1785310567 97476608 23226 4294967295 134512640 135094434 3221224448 3221223120 134556244 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/25277/statm): 23798 23226 145 145 0 23653 0 [pid=25277] vsize: 95192 Current children cumulated CPU time (s) 1148.06 Current children cumulated vsize (Kb) 97316 [startup+1160.11 s] Raw data (loadavg): 1.00 0.99 0.91 2/57 25277 Raw data (/proc/25273/stat): 25273 (minisat+_script) S 25272 25273 8263 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785310562 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/25273/statm): 531 226 485 147 0 384 0 [pid=25273] vsize: 2124 Raw data (/proc/25277/stat): 25277 (minisat+_64-bit) R 25273 25273 8263 0 -1 0 23612 0 0 0 115628 176 0 0 25 0 1 0 1785310567 98242560 23412 4294967295 134512640 135094434 3221224448 3221223104 134558178 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/25277/statm): 23985 23412 145 145 0 23840 0 [pid=25277] vsize: 95940 Current children cumulated CPU time (s) 1158.04 Current children cumulated vsize (Kb) 98064 [startup+1170.11 s] Raw data (loadavg): 1.00 0.99 0.91 2/57 25277 Raw data (/proc/25273/stat): 25273 (minisat+_script) S 25272 25273 8263 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785310562 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/25273/statm): 531 226 485 147 0 384 0 [pid=25273] vsize: 2124 Raw data (/proc/25277/stat): 25277 (minisat+_64-bit) R 25273 25273 8263 0 -1 0 23796 0 0 0 116624 178 0 0 25 0 1 0 1785310567 98996224 23596 4294967295 134512640 135094434 3221224448 3221223104 134557840 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/25277/statm): 24169 23596 145 145 0 24024 0 [pid=25277] vsize: 96676 Current children cumulated CPU time (s) 1168.02 Current children cumulated vsize (Kb) 98800 [startup+1180.12 s] Raw data (loadavg): 1.00 0.99 0.91 2/57 25277 Raw data (/proc/25273/stat): 25273 (minisat+_script) S 25272 25273 8263 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785310562 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/25273/statm): 531 226 485 147 0 384 0 [pid=25273] vsize: 2124 Raw data (/proc/25277/stat): 25277 (minisat+_64-bit) R 25273 25273 8263 0 -1 0 23983 0 0 0 117620 179 0 0 25 0 1 0 1785310567 99753984 23783 4294967295 134512640 135094434 3221224448 3221223104 134558249 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/25277/statm): 24354 23783 145 145 0 24209 0 [pid=25277] vsize: 97416 Current children cumulated CPU time (s) 1177.99 Current children cumulated vsize (Kb) 99540 [startup+1190.12 s] Raw data (loadavg): 1.00 0.99 0.91 3/57 25277 Raw data (/proc/25273/stat): 25273 (minisat+_script) S 25272 25273 8263 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785310562 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/25273/statm): 531 226 485 147 0 384 0 [pid=25273] vsize: 2124 Raw data (/proc/25277/stat): 25277 (minisat+_64-bit) R 25273 25273 8263 0 -1 0 24110 0 0 0 118618 180 0 0 25 0 1 0 1785310567 100286464 23910 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/25277/statm): 24484 23910 145 145 0 24339 0 [pid=25277] vsize: 97936 Current children cumulated CPU time (s) 1187.98 Current children cumulated vsize (Kb) 100060 [startup+1200.12 s] Raw data (loadavg): 1.00 0.99 0.91 2/57 25277 Raw data (/proc/25273/stat): 25273 (minisat+_script) S 25272 25273 8263 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785310562 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/25273/statm): 531 226 485 147 0 384 0 [pid=25273] vsize: 2124 Raw data (/proc/25277/stat): 25277 (minisat+_64-bit) R 25273 25273 8263 0 -1 0 24329 0 0 0 119615 181 0 0 25 0 1 0 1785310567 101183488 24129 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/25277/statm): 24703 24129 145 145 0 24558 0 [pid=25277] vsize: 98812 Current children cumulated CPU time (s) 1197.96 Current children cumulated vsize (Kb) 100936 [startup+1210.12 s] Raw data (loadavg): 1.00 0.99 0.91 2/57 25277 Raw data (/proc/25273/stat): 25273 (minisat+_script) S 25272 25273 8263 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785310562 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/25273/statm): 531 226 485 147 0 384 0 [pid=25273] vsize: 2124 Raw data (/proc/25277/stat): 25277 (minisat+_64-bit) R 25273 25273 8263 0 -1 0 24570 0 0 0 120610 183 0 0 25 0 1 0 1785310567 102178816 24370 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/25277/statm): 24946 24370 145 145 0 24801 0 [pid=25277] vsize: 99784 Current children cumulated CPU time (s) 1207.93 Current children cumulated vsize (Kb) 101908 Maximum CPU time exceeded: sending SIGTERM then SIGKILL [startup+1210.12 s] Raw data (loadavg): 1.00 0.99 0.91 2/57 25277 Raw data (/proc/25273/stat): 25273 (minisat+_script) S 25272 25273 8263 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1785310562 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/25273/statm): 531 226 485 147 0 384 0 [pid=25273] vsize: 2124 Raw data (/proc/25277/stat): 25277 (minisat+_64-bit) R 25273 25273 8263 0 -1 0 24570 0 0 0 120610 183 0 0 25 0 1 0 1785310567 102178816 24370 4294967295 134512640 135094434 3221224448 3221223104 134558213 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/25277/statm): 24946 24370 145 145 0 24801 0 [pid=25277] vsize: 99784 Current children cumulated CPU time (s) 1207.93 Current children cumulated vsize (Kb) 101908 Sending SIGTERM to -25273 Sleeping 2 seconds One traced child (pid=25273) ended because it received signal 15 (SIGTERM) One traced child (pid=25277) exited with status: 10 All traced children have exited ! Game is over. Child status: 10 Real time (s): 1210.17 CPU time (s): 1207.99 CPU user time (s): 1206.11 CPU system time (s): 1.88371 CPU usage (%): 99.8198 Max. virtual memory (cumulated for all children) (Kb): 101908
ERROR: no interpretation found !