Name | normalized-opb/web/www.nlsde.buaa.edu.cn/~kexu/benchmarks/frb53-24-opb/normalized-frb53-24-1.opb |
MD5SUM | 20fc65112f36a5d10cc9eaa82c0beb63 |
Bench Category | optimization, small integers (OPTSMALLINT) |
Has Objective Function | YES |
Satisfiable | YES |
(Un)Satisfiability was proved | YES |
Best value of the objective function | -38 |
Optimality of the best value was proved | NO |
Number of terms in the objective function | 1272 |
Biggest coefficient in the objective function | 1 |
Number of bits for the biggest coefficient in the objective function | 1 |
Sum of the numbers in the objective function | 1272 |
Number of bits of the sum of numbers in the objective function | 11 |
Biggest number in a constraint | 1 |
Number of bits of the biggest number in a constraint | 1 |
Biggest sum of numbers in a constraint | 1272 |
Number of bits of the biggest sum of numbers | 11 |
Best result obtained on this benchmark | SAT |
Best CPU time to get the best result obtained on this benchmark | 1175.1 |
Number of variables | 1272 |
Total number of constraints | 94227 |
Number of constraints which are clauses | 94227 |
Number of constraints which are cardinality constraints (but not clauses) | 0 |
Number of constraints which are nor clauses,nor cardinality constraints | 0 |
Minimum length of a constraint | 2 |
Maximum length of a constraint | 2 |
#### BEGIN LAUNCHER DATA #### LAUNCH ON wulflinc25 THE 2005-04-14 04:49:03 (client local time) PB2005-SCRIPT v4.0 MARKUPS: idlaunch=4851 boxname=wulflinc25 idbench=339 idsolver=13 numberseed=0 MD5SUM SOLVER: MD5SUM BENCH: 20fc65112f36a5d10cc9eaa82c0beb63 /oldhome/oroussel/tmp/wulflinc25/normalized-frb53-24-1.opb REAL COMMAND: minisat+ -w /oldhome/oroussel/tmp/wulflinc25/normalized-frb53-24-1.opb /oldhome/oroussel/tmp/wulflinc25/normalized-frb53-24-1.opb IDLAUNCH: 4851 /proc/cpuinfo: processor : 0 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 2 cpu MHz : 451.220 cache size : 512 KB fdiv_bug : no hlt_bug : no f00f_bug : no coma_bug : no fpu : yes fpu_exception : yes cpuid level : 2 wp : yes flags : fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse bogomips : 888.83 processor : 1 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 3 cpu MHz : 451.220 cache size : 512 KB fdiv_bug : no hlt_bug : no f00f_bug : no coma_bug : no fpu : yes fpu_exception : yes cpuid level : 2 wp : yes flags : fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse bogomips : 901.12 /proc/meminfo: MemTotal: 1034660 kB MemFree: 856648 kB Buffers: 35184 kB Cached: 107580 kB SwapCached: 36 kB Active: 53224 kB Inactive: 92456 kB HighTotal: 131008 kB HighFree: 19628 kB LowTotal: 903652 kB LowFree: 837020 kB SwapTotal: 2097892 kB SwapFree: 2097856 kB Dirty: 28 kB Writeback: 0 kB Mapped: 6920 kB Slab: 26528 kB Committed_AS: 63484 kB PageTables: 316 kB VmallocTotal: 114680 kB VmallocUsed: 1368 kB VmallocChunk: 113252 kB JOB ENDED THE 2005-04-14 05:09:06 (client local time) WITH STATUS 10 IN 1200.47 SECONDS stats: 4851 7 1200.47 10 #### END LAUNCHER DATA #### #### BEGIN SOLVER DATA #### c Parsing PB file... c Converting 94227 PB-constraints to clauses... c -- Unit propagations: (none) c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): ................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................... c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 0 | 94227 188454 | 31409 0 0 nan | 0.000 % | c ============================================================================== c [1mFound solution: -36[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost:70300 Base: c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 0 | 244947 541084 | 81649 0 0 nan | 0.000 % | c | 100 | 244947 541084 | 89813 100 1082 10.8 | 0.014 % | c | 251 | 244414 539871 | 98795 237 2012 8.5 | 0.372 % | c | 476 | 240587 531087 | 108674 389 3113 8.0 | 2.599 % | c | 813 | 235181 518674 | 119542 614 4746 7.7 | 5.835 % | c | 1319 | 226313 498257 | 131496 916 7106 7.8 | 11.250 % | c | 2078 | 215022 472171 | 144646 1421 11823 8.3 | 18.298 % | c | 3217 | 199573 436478 | 159110 2233 18781 8.4 | 27.854 % | c | 4925 | 178575 387582 | 175021 3311 27851 8.4 | 41.181 % | c ============================================================================== c [1mFound solution: -38[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 0 Base: c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 5587 | 169033 365226 | 56344 3520 29503 8.4 | 41.181 % | c | 5688 | 168623 364274 | 61978 3599 30725 8.5 | 47.811 % | c | 5838 | 167224 361036 | 68176 3697 31581 8.5 | 48.691 % | c | 6063 | 166129 358484 | 74993 3874 33139 8.6 | 49.341 % | c | 6400 | 163008 351161 | 82493 4057 34550 8.5 | 51.463 % | c | 6906 | 159352 342601 | 90742 4397 37323 8.5 | 53.897 % | c | 7665 | 153177 328119 | 99816 4723 43693 9.3 | 58.073 % | c | 8804 | 141454 300749 | 109798 5207 47906 9.2 | 65.709 % | c | 10513 | 129713 273157 | 120778 5800 57461 9.9 | 73.591 % | c ============================================================================== c [1mFound solution: -39[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 0 Base: c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 11112 | 125735 263896 | 41911 5940 59548 10.0 | 73.591 % | c | 11212 | 125242 262739 | 46102 5958 59531 10.0 | 76.704 % | c | 11362 | 124288 260476 | 50712 5956 59254 9.9 | 77.379 % | c | 11587 | 122380 256006 | 55783 6065 60757 10.0 | 78.667 % | c | 11924 | 121348 253577 | 61361 6219 60725 9.8 | 79.373 % | c | 12431 | 119633 249531 | 67498 6507 66069 10.2 | 80.556 % | c | 13191 | 118333 246466 | 74247 6956 71403 10.3 | 81.432 % | c ============================================================================== c [1mFound solution: -40[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 0 Base: c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 14134 | 113554 235196 | 37851 7039 72150 10.3 | 81.432 % | c | 14234 | 113372 234758 | 41636 7036 72002 10.2 | 84.835 % | c | 14384 | 112513 232749 | 45799 6930 71045 10.3 | 85.421 % | c | 14609 | 112404 232492 | 50379 7142 75264 10.5 | 85.497 % | c | 14947 | 111609 230614 | 55417 7238 75720 10.5 | 86.063 % | c | 15454 | 110820 228765 | 60959 7384 82571 11.2 | 86.595 % | c | 16213 | 109537 225718 | 67055 7442 91384 12.3 | 87.514 % | c ============================================================================== c [1mFound solution: -41[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 0 Base: c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 16799 | 108153 222488 | 36051 7670 94769 12.4 | 87.514 % | c | 16902 | 107584 221146 | 39656 7595 94373 12.4 | 88.879 % | c | 17052 | 107584 221146 | 43621 7745 97344 12.6 | 88.879 % | c | 17279 | 107481 220901 | 47983 7935 100720 12.7 | 88.957 % | c | 17616 | 107218 220280 | 52782 8089 103453 12.8 | 89.142 % | c | 18122 | 107069 219925 | 58060 8520 121593 14.3 | 89.255 % | c | 18881 | 106453 218468 | 63866 8868 148675 16.8 | 89.684 % | c | 20020 | 106329 218172 | 70253 9856 198305 20.1 | 89.774 % | c ============================================================================== c [1mFound solution: -42[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 0 Base: c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 20823 | 106076 217556 | 35358 10561 265515 25.1 | 89.774 % | c | 20923 | 106076 217556 | 38893 10661 268738 25.2 | 89.938 % | c | 21073 | 106076 217556 | 42783 10811 275129 25.4 | 89.938 % | c | 21298 | 106076 217556 | 47061 11036 285202 25.8 | 89.938 % | c | 21635 | 106076 217556 | 51767 11373 291931 25.7 | 89.938 % | c | 22142 | 106076 217556 | 56944 11880 321705 27.1 | 89.938 % | c | 22902 | 105776 216861 | 62638 12408 355411 28.6 | 90.131 % | c | 24041 | 105776 216861 | 68902 13547 444666 32.8 | 90.131 % | c ============================================================================== c [1mFound solution: -43[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 0 Base: c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 24522 | 105716 216733 | 35238 13715 481917 35.1 | 90.131 % | c | 24623 | 105716 216733 | 38761 13816 486032 35.2 | 90.194 % | c | 24774 | 105653 216586 | 42637 13945 493773 35.4 | 90.239 % | c ============================================================================== c [1mFound solution: -44[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 0 Base: c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 24847 | 105568 216370 | 35189 13966 492372 35.3 | 90.239 % | c | 24947 | 105568 216370 | 38707 14066 496882 35.3 | 90.290 % | c | 25097 | 105568 216370 | 42578 14216 501821 35.3 | 90.290 % | c | 25322 | 105568 216370 | 46836 14441 514536 35.6 | 90.290 % | c | 25659 | 105504 216219 | 51520 14668 528058 36.0 | 90.334 % | c | 26169 | 105504 216219 | 56672 15178 555755 36.6 | 90.334 % | c | 26928 | 105504 216219 | 62339 15937 637260 40.0 | 90.334 % | c ============================================================================== c [1mFound solution: -45[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 0 Base: c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 27994 | 105415 216019 | 35138 16897 717188 42.4 | 90.334 % | c | 28094 | 105415 216019 | 38651 16997 720879 42.4 | 90.398 % | c | 28244 | 105344 215850 | 42516 17081 729292 42.7 | 90.453 % | c | 28470 | 105300 215745 | 46768 17241 741085 43.0 | 90.486 % | c | 28809 | 105294 215731 | 51445 17559 769342 43.8 | 90.490 % | c | 29315 | 105254 215636 | 56590 18051 785080 43.5 | 90.519 % | c | 30074 | 105254 215636 | 62249 18810 834235 44.4 | 90.519 % | c | 31213 | 105168 215439 | 68474 19854 969745 48.8 | 90.565 % | c | 32921 | 105010 215064 | 75321 21367 1094901 51.2 | 90.684 % | c | 35483 | 105010 215064 | 82853 23929 1454753 60.8 | 90.684 % | c ============================================================================== c [1mFound solution: -46[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 0 Base: c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 36476 | 104833 214626 | 34944 24560 1529898 62.3 | 90.684 % | c | 36576 | 104833 214626 | 38438 24660 1533499 62.2 | 90.799 % | c | 36727 | 104833 214626 | 42282 24811 1540136 62.1 | 90.799 % | c | 36952 | 104799 214549 | 46510 25011 1546646 61.8 | 90.819 % | c | 37289 | 104799 214549 | 51161 25348 1561273 61.6 | 90.819 % | c | 37795 | 104799 214549 | 56277 25854 1595462 61.7 | 90.819 % | c | 38554 | 104773 214487 | 61905 26582 1642013 61.8 | 90.838 % | c | 39693 | 104773 214487 | 68095 27721 1735576 62.6 | 90.838 % | c | 41402 | 104711 214338 | 74905 29309 1872631 63.9 | 90.885 % | c | 43964 | 104711 214338 | 82396 31871 2163660 67.9 | 90.885 % | c | 47808 | 104711 214338 | 90635 35715 2594699 72.7 | 90.885 % | c ============================================================================== c [1mFound solution: -47[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 0 Base: c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 49791 | 104753 214439 | 34917 37698 2839908 75.3 | 90.885 % | c | 49891 | 104753 214439 | 38408 37798 2848511 75.4 | 90.881 % | c | 50041 | 104753 214439 | 42249 37948 2859638 75.4 | 90.881 % | c | 50266 | 104753 214439 | 46474 38173 2871725 75.2 | 90.881 % | c | 50603 | 104753 214439 | 51121 38510 2896709 75.2 | 90.881 % | c | 51109 | 104753 214439 | 56234 39016 2926834 75.0 | 90.881 % | c | 51868 | 104753 214439 | 61857 39775 2981249 75.0 | 90.881 % | c | 53007 | 104753 214439 | 68043 40914 3120209 76.3 | 90.881 % | c | 54715 | 104753 214439 | 74847 42622 3285217 77.1 | 90.881 % | c | 57277 | 104753 214439 | 82332 45184 3563599 78.9 | 90.881 % | c | 61122 | 104753 214439 | 90565 49029 3960352 80.8 | 90.881 % | c | 66888 | 104753 214439 | 99622 54795 4629161 84.5 | 90.881 % | c | 75537 | 104691 214292 | 109584 63274 5877856 92.9 | 90.926 % | c | 88512 | 104691 214292 | 120542 76249 7484684 98.2 | 90.926 % | c | 107973 | 104691 214292 | 132597 95710 9561126 99.9 | 90.926 % | c ============================================================================== c [1mFound solution: -48[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 0 Base: c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 132860 | 104615 214103 | 34871 120421 12201442 101.3 | 90.926 % | c | 132961 | 104615 214103 | 38358 18037 1463940 81.2 | 90.975 % | c | 133111 | 104615 214103 | 42193 18187 1468598 80.7 | 90.975 % | c | 133337 | 104553 213957 | 46413 18409 1482285 80.5 | 91.017 % | c | 133674 | 104553 213957 | 51054 18746 1503771 80.2 | 91.017 % | c | 134180 | 104547 213943 | 56160 19251 1544268 80.2 | 91.021 % | c | 134939 | 104477 213775 | 61776 19995 1579039 79.0 | 91.074 % | c | 136079 | 104463 213741 | 67953 21132 1671797 79.1 | 91.085 % | c | 137789 | 104463 213741 | 74749 22842 1858804 81.4 | 91.085 % | c | 140351 | 104463 213741 | 82223 25404 2144978 84.4 | 91.085 % | c | 144196 | 104463 213741 | 90446 29249 2519784 86.1 | 91.085 % | c | 149962 | 104463 213741 | 99491 35015 3270196 93.4 | 91.085 % | c | 158611 | 104451 213713 | 109440 43663 4298987 98.5 | 91.093 % | c | 171587 | 104451 213713 | 120384 56639 6410910 113.2 | 91.093 % | c ============================================================================== c [1mFound solution: -49[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 0 Base: c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 185156 | 104482 213787 | 34827 70208 8068756 114.9 | 91.093 % | c | 185256 | 104482 213787 | 38309 70308 8075584 114.9 | 91.077 % | c | 185408 | 104482 213787 | 42140 70460 8081704 114.7 | 91.077 % | c | 185633 | 104472 213763 | 46354 70635 8097561 114.6 | 91.084 % | c | 185970 | 104472 213763 | 50990 70972 8131396 114.6 | 91.084 % | c | 186478 | 104472 213763 | 56089 71480 8185430 114.5 | 91.084 % | c | 187237 | 104472 213763 | 61698 72239 8257138 114.3 | 91.084 % | c | 188376 | 104472 213763 | 67867 73378 8347232 113.8 | 91.084 % | c | 190086 | 104472 213763 | 74654 75088 8478132 112.9 | 91.084 % | c | 192649 | 104472 213763 | 82120 77651 8714812 112.2 | 91.084 % | c | 196494 | 104472 213763 | 90332 81496 9061128 111.2 | 91.084 % | c | 202261 | 104472 213763 | 99365 87263 9594982 110.0 | 91.084 % | c | 210910 | 104472 213763 | 109302 95912 10290527 107.3 | 91.084 % | c | 223885 | 104468 213754 | 120232 108884 11255497 103.4 | 91.086 % | c | 243349 | 104468 213754 | 132255 128348 12674336 98.7 | 91.086 % | c | 272541 | 104468 213754 | 145481 157540 14398735 91.4 | 91.086 % | c | 316330 | 104468 213754 | 160029 29601 1100197 37.2 | 91.086 % | c c *** TERMINATED *** s SATISFIABLE v -C1272 -C1271 -C1270 -C1269 -C1268 -C1267 -C1266 -C1265 -C1264 -C1263 -C1262 -C1261 -C1260 -C1259 -C1258 -C1257 C1256 -C1255 -C1254 -C1253 -C1252 -C1251 -C1250 -C1249 -C1248 -C1247 -C1246 -C1245 -C1244 -C1243 -C1242 -C1241 -C1240 -C1239 -C1238 -C1237 -C1236 -C1235 -C1234 -C1233 -C1232 -C1231 -C1230 C1229 -C1228 -C1227 -C1226 -C1225 -C1224 -C1223 -C1222 -C1221 -C1220 -C1219 -C1218 -C1217 -C1216 -C1215 -C1214 -C1213 -C1212 -C1211 -C1210 -C1209 -C1208 -C1207 -C1206 -C1205 -C1204 C1203 -C1202 -C1201 -C1200 -C1199 -C1198 -C1197 -C1196 -C1195 -C1194 -C1193 -C1192 -C1191 -C1190 -C1189 -C1188 -C1187 -C1186 -C1185 -C1184 -C1183 -C1182 C1181 -C1180 -C1179 -C1178 -C1177 -C1176 -C1175 -C1174 -C1173 -C1172 -C1171 -C1170 -C1169 -C1168 -C1167 -C1166 -C1165 -C1164 -C1163 -C1162 -C1161 -C1160 C1159 -C1158 -C1157 -C1156 -C1155 -C1154 -C1153 -C1152 -C1151 -C1150 -C1149 -C1148 -C1147 -C1146 -C1145 -C1144 -C1143 C1142 -C1141 -C1140 -C1139 -C1138 -C1137 -C1136 -C1135 -C1134 -C1133 -C1132 -C1131 -C1130 -C1129 -C1128 -C1127 -C1126 -C1125 -C1124 -C1123 -C1122 -C1121 -C1120 C1119 -C1118 -C1117 -C1116 -C1115 -C1114 -C1113 -C1112 -C1111 -C1110 -C1109 -C1108 -C1107 -C1106 -C1105 -C1104 C1103 -C1102 -C1101 -C1100 -C1099 -C1098 -C1097 -C1096 -C1095 -C1094 -C1093 -C1092 -C1091 -C1090 -C1089 -C1088 -C1087 -C1086 -C1085 -C1084 -C1083 -C1082 -C1081 -C1080 -C1079 -C1078 -C1077 -C1076 -C1075 -C1074 -C1073 -C1072 -C1071 -C1070 -C1069 -C1068 -C1067 -C1066 -C1065 -C1064 -C1063 C1062 -C1061 -C1060 -C1059 -C1058 -C1057 -C1056 -C1055 -C1054 -C1053 -C1052 -C1051 -C1050 -C1049 -C1048 -C1047 -C1046 -C1045 -C1044 -C1043 -C1042 -C1041 -C1040 C1039 -C1038 -C1037 -C1036 -C1035 -C1034 -C1033 -C1032 -C1031 -C1030 -C1029 -C1028 -C1027 -C1026 -C1025 -C1024 -C1023 -C1022 -C1021 -C1020 -C1019 -C1018 -C1017 -C1016 -C1015 -C1014 C1013 -C1012 -C1011 -C1010 -C1009 -C1008 C1007 -C1006 -C1005 -C1004 -C1003 -C1002 -C1001 -C1000 -C999 -C998 -C997 -C996 -C995 -C994 -C993 -C992 -C991 -C990 -C989 -C988 -C987 -C986 -C985 -C984 C983 -C982 -C981 -C980 -C979 -C978 -C977 -C976 -C975 -C974 -C973 -C972 -C971 -C970 -C969 -C968 -C967 -C966 -C965 -C964 -C963 -C962 -C961 -C960 -C959 -C958 -C957 -C956 -C955 -C954 -C953 -C952 -C951 -C950 -C949 -C948 -C947 -C946 -C945 -C944 -C943 -C942 C941 -C940 -C939 -C938 -C937 -C936 -C935 -C934 -C933 -C932 -C931 -C930 -C929 -C928 -C927 -C926 -C925 -C924 -C923 -C922 -C921 -C920 -C919 -C918 -C917 -C916 -C915 C914 -C913 -C912 -C911 -C910 -C909 C908 -C907 -C906 -C905 -C904 -C903 -C902 -C901 -C900 -C899 -C898 -C897 -C896 -C895 -C894 -C893 -C892 -C891 -C890 -C889 C888 -C887 -C886 -C885 -C884 -C883 -C882 -C881 -C880 -C879 -C878 -C877 -C876 -C875 -C874 -C873 -C872 -C871 -C870 -C869 -C868 -C867 -C866 -C865 -C864 -C863 -C862 -C861 -C860 -C859 -C858 -C857 -C856 -C855 -C854 -C853 -C852 -C851 -C850 -C849 -C848 -C847 -C846 -C845 -C844 C843 -C842 -C841 -C840 -C839 -C838 -C837 -C836 -C835 -C834 -C833 -C832 -C831 -C830 -C829 -C828 -C827 -C826 -C825 -C824 -C823 -C822 -C821 -C820 -C819 C818 -C817 -C816 -C815 -C814 -C813 -C812 -C811 -C810 -C809 -C808 -C807 -C806 -C805 -C804 -C803 -C802 -C801 -C800 -C799 -C798 -C797 -C796 -C795 -C794 C793 -C792 -C791 -C790 -C789 -C788 -C787 -C786 -C785 -C784 -C783 -C782 -C781 -C780 -C779 -C778 -C777 -C776 -C775 -C774 -C773 -C772 -C771 -C770 -C769 -C768 -C767 -C766 -C765 -C764 -C763 -C762 -C761 -C760 -C759 -C758 -C757 -C756 -C755 -C754 -C753 -C752 -C751 C750 -C749 -C748 -C747 -C746 -C745 -C744 -C743 -C742 -C741 -C740 -C739 -C738 C737 -C736 -C735 -C734 -C733 -C732 -C731 -C730 -C729 -C728 -C727 -C726 -C725 -C724 -C723 -C722 -C721 -C720 -C719 -C718 -C717 -C716 -C715 -C714 -C713 -C712 -C711 -C710 -C709 -C708 -C707 -C706 -C705 -C704 -C703 -C702 -C701 -C700 -C699 -C698 -C697 -C696 -C695 -C694 -C693 -C692 C691 -C690 -C689 -C688 -C687 -C686 -C685 -C684 -C683 -C682 -C681 -C680 -C679 -C678 -C677 -C676 -C675 -C674 -C673 -C672 C671 -C670 -C669 -C668 -C667 -C666 -C665 -C664 -C663 -C662 -C661 -C660 -C659 -C658 -C657 -C656 -C655 -C654 -C653 -C652 -C651 -C650 -C649 -C648 -C647 -C646 -C645 -C644 -C643 -C642 -C641 -C640 -C639 -C6#### END SOLVER DATA #### #### BEGIN WATCHER DATA #### Enforcing CPU limit (will send SIGTERM then SIGKILL): 1200 seconds Enforcing CPUTime (will send SIGXCPU) limit: 1230 seconds Enforcing VSIZE limit: 943718400 bytes Raw data (loadavg): 0.92 0.95 0.90 2/54 3439 Raw data (stat): 3439 (runsolver) R 3438 28099 28098 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 481845856 1052672 99 4294967295 134512640 135381576 3221224464 3221219708 135158418 0 2147483391 7 90112 0 0 0 17 0 0 0 Raw data (statm): 257 99 215 215 0 42 0 vsize: 1028 [startup+10.0001 s] Raw data (loadavg): 0.93 0.96 0.91 2/54 3439 Raw data (stat): 3439 (minisat+) R 3438 28099 28098 0 -1 0 6016 0 0 0 982 16 0 0 25 0 1 0 481845856 27267072 5994 4294967295 134512640 134672761 3221224560 3221223732 134556632 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 6657 5994 603 41 0 6616 0 vsize: 26628 [startup+20.0007 s] Raw data (loadavg): 0.94 0.96 0.91 2/54 3439 Raw data (stat): 3439 (minisat+) R 3438 28099 28098 0 -1 0 6024 0 0 0 1982 16 0 0 25 0 1 0 481845856 27267072 6002 4294967295 134512640 134672761 3221224560 3221223732 134556598 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 6657 6002 603 41 0 6616 0 vsize: 26628 [startup+30.0008 s] Raw data (loadavg): 0.95 0.96 0.91 2/54 3439 Raw data (stat): 3439 (minisat+) R 3438 28099 28098 0 -1 0 6025 0 0 0 2982 16 0 0 25 0 1 0 481845856 27267072 6003 4294967295 134512640 134672761 3221224560 3221223696 134560590 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 6657 6003 603 41 0 6616 0 vsize: 26628 [startup+40.0009 s] Raw data (loadavg): 0.96 0.96 0.91 2/54 3439 Raw data (stat): 3439 (minisat+) R 3438 28099 28098 0 -1 0 6025 0 0 0 3981 16 0 0 25 0 1 0 481845856 27267072 6003 4294967295 134512640 134672761 3221224560 3221223732 134556634 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 6657 6003 603 41 0 6616 0 vsize: 26628 [startup+50.001 s] Raw data (loadavg): 0.96 0.96 0.91 2/54 3439 Raw data (stat): 3439 (minisat+) R 3438 28099 28098 0 -1 0 6025 0 0 0 4982 16 0 0 25 0 1 0 481845856 27267072 6003 4294967295 134512640 134672761 3221224560 3221223728 134561272 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 6657 6003 603 41 0 6616 0 vsize: 26628 [startup+60.0014 s] Raw data (loadavg): 0.97 0.96 0.91 2/54 3439 Raw data (stat): 3439 (minisat+) R 3438 28099 28098 0 -1 0 6165 0 0 0 5981 16 0 0 25 0 1 0 481845856 28311552 6143 4294967295 134512640 134672761 3221224560 3221223732 134556598 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 6912 6143 603 41 0 6871 0 vsize: 27648 [startup+70.0017 s] Raw data (loadavg): 0.97 0.96 0.91 2/54 3439 Raw data (stat): 3439 (minisat+) R 3438 28099 28098 0 -1 0 6165 0 0 0 6981 17 0 0 25 0 1 0 481845856 28311552 6143 4294967295 134512640 134672761 3221224560 3221223732 134556660 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 6912 6143 603 41 0 6871 0 vsize: 27648 [startup+80.0013 s] Raw data (loadavg): 0.98 0.96 0.91 2/54 3439 Raw data (stat): 3439 (minisat+) R 3438 28099 28098 0 -1 0 6165 0 0 0 7981 17 0 0 25 0 1 0 481845856 28311552 6143 4294967295 134512640 134672761 3221224560 3221223732 134556598 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 6912 6143 603 41 0 6871 0 vsize: 27648 [startup+90.0012 s] Raw data (loadavg): 0.98 0.96 0.91 2/54 3439 Raw data (stat): 3439 (minisat+) R 3438 28099 28098 0 -1 0 6169 0 0 0 8982 17 0 0 25 0 1 0 481845856 28311552 6147 4294967295 134512640 134672761 3221224560 3221223732 134556598 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 6912 6147 603 41 0 6871 0 vsize: 27648 [startup+100 s] Raw data (loadavg): 0.98 0.96 0.91 2/54 3439 Raw data (stat): 3439 (minisat+) R 3438 28099 28098 0 -1 0 6171 0 0 0 9982 17 0 0 25 0 1 0 481845856 28311552 6149 4294967295 134512640 134672761 3221224560 3221223732 134556598 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 6912 6149 603 41 0 6871 0 vsize: 27648 [startup+110.001 s] Raw data (loadavg): 0.98 0.97 0.91 2/54 3439 Raw data (stat): 3439 (minisat+) R 3438 28099 28098 0 -1 0 6477 0 0 0 10980 18 0 0 25 0 1 0 481845856 29536256 6446 4294967295 134512640 134672761 3221224560 3221223760 134557836 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 7211 6446 603 41 0 7170 0 vsize: 28844 [startup+120.002 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 3439 Raw data (stat): 3439 (minisat+) R 3438 28099 28098 0 -1 0 7032 0 0 0 11979 19 0 0 25 0 1 0 481845856 31666176 6974 4294967295 134512640 134672761 3221224560 3221223732 134556682 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 7731 6974 603 41 0 7690 0 vsize: 30924 [startup+130.001 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 3439 Raw data (stat): 3439 (minisat+) R 3438 28099 28098 0 -1 0 7659 0 0 0 12977 21 0 0 25 0 1 0 481845856 34160640 7592 4294967295 134512640 134672761 3221224560 3221223728 134561005 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 8340 7592 603 41 0 8299 0 vsize: 33360 [startup+140.001 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 3439 Raw data (stat): 3439 (minisat+) R 3438 28099 28098 0 -1 0 8190 0 0 0 13976 23 0 0 25 0 1 0 481845856 36311040 8123 4294967295 134512640 134672761 3221224560 3221223728 134560980 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 8865 8123 603 41 0 8824 0 vsize: 35460 [startup+150 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 3439 Raw data (stat): 3439 (minisat+) R 3438 28099 28098 0 -1 0 8781 0 0 0 14974 25 0 0 25 0 1 0 481845856 38854656 8714 4294967295 134512640 134672761 3221224560 3221223728 134561193 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 9486 8714 603 41 0 9445 0 vsize: 37944 [startup+160 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 3439 Raw data (stat): 3439 (minisat+) R 3438 28099 28098 0 -1 0 9276 0 0 0 15973 27 0 0 25 0 1 0 481845856 40898560 9201 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 9985 9201 603 41 0 9944 0 vsize: 39940 [startup+170 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 3439 Raw data (stat): 3439 (minisat+) R 3438 28099 28098 0 -1 0 9765 0 0 0 16971 28 0 0 25 0 1 0 481845856 42913792 9690 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 10477 9690 603 41 0 10436 0 vsize: 41908 [startup+179.999 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 3439 Raw data (stat): 3439 (minisat+) R 3438 28099 28098 0 -1 0 10196 0 0 0 17970 30 0 0 25 0 1 0 481845856 44642304 10121 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 10899 10121 603 41 0 10858 0 vsize: 43596 [startup+189.999 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 3439 Raw data (stat): 3439 (minisat+) R 3438 28099 28098 0 -1 0 10638 0 0 0 18968 31 0 0 25 0 1 0 481845856 46374912 10563 4294967295 134512640 134672761 3221224560 3221223728 134561025 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 11322 10563 603 41 0 11281 0 vsize: 45288 [startup+199.998 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 3439 Raw data (stat): 3439 (minisat+) R 3438 28099 28098 0 -1 0 11050 0 0 0 19967 33 0 0 25 0 1 0 481845856 48095232 10975 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 11742 10975 603 41 0 11701 0 vsize: 46968 [startup+209.999 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 3439 Raw data (stat): 3439 (minisat+) R 3438 28099 28098 0 -1 0 11596 0 0 0 20966 34 0 0 25 0 1 0 481845856 50356224 11521 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 12294 11521 603 41 0 12253 0 vsize: 49176 [startup+219.999 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 3439 Raw data (stat): 3439 (minisat+) R 3438 28099 28098 0 -1 0 12168 0 0 0 21965 35 0 0 25 0 1 0 481845856 52617216 12093 4294967295 134512640 134672761 3221224560 3221223700 134560556 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 12846 12093 603 41 0 12805 0 vsize: 51384 [startup+229.999 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 3439 Raw data (stat): 3439 (minisat+) R 3438 28099 28098 0 -1 0 12601 0 0 0 22964 36 0 0 25 0 1 0 481845856 54616064 12526 4294967295 134512640 134672761 3221224560 3221223744 134558899 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 13334 12526 603 41 0 13293 0 vsize: 53336 [startup+239.999 s] Raw data (loadavg): 0.99 0.97 0.91 3/54 3439 Raw data (stat): 3439 (minisat+) R 3438 28099 28098 0 -1 0 13037 0 0 0 23963 38 0 0 25 0 1 0 481845856 56479744 12962 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 13789 12962 603 41 0 13748 0 vsize: 55156 [startup+249.998 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 3439 Raw data (stat): 3439 (minisat+) R 3438 28099 28098 0 -1 0 13418 0 0 0 24962 39 0 0 25 0 1 0 481845856 57946112 13343 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 14147 13343 603 41 0 14106 0 vsize: 56588 [startup+259.998 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 3439 Raw data (stat): 3439 (minisat+) R 3438 28099 28098 0 -1 0 13822 0 0 0 25961 40 0 0 25 0 1 0 481845856 59670528 13747 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 14568 13747 603 41 0 14527 0 vsize: 58272 [startup+269.998 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 3439 Raw data (stat): 3439 (minisat+) R 3438 28099 28098 0 -1 0 14197 0 0 0 26960 41 0 0 25 0 1 0 481845856 61145088 14122 4294967295 134512640 134672761 3221224560 3221223664 134560289 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 14928 14122 603 41 0 14887 0 vsize: 59712 [startup+279.997 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 3439 Raw data (stat): 3439 (minisat+) R 3438 28099 28098 0 -1 0 14558 0 0 0 27959 42 0 0 25 0 1 0 481845856 62611456 14483 4294967295 134512640 134672761 3221224560 3221223728 134561215 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 15286 14483 603 41 0 15245 0 vsize: 61144 [startup+289.997 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 3439 Raw data (stat): 3439 (minisat+) R 3438 28099 28098 0 -1 0 14884 0 0 0 28958 43 0 0 25 0 1 0 481845856 63950848 14809 4294967295 134512640 134672761 3221224560 3221223664 134560128 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 15613 14809 603 41 0 15572 0 vsize: 62452 [startup+299.997 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 3439 Raw data (stat): 3439 (minisat+) R 3438 28099 28098 0 -1 0 15242 0 0 0 29957 44 0 0 25 0 1 0 481845856 65425408 15167 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 15973 15167 603 41 0 15932 0 vsize: 63892 [startup+309.997 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 3439 Raw data (stat): 3439 (minisat+) R 3438 28099 28098 0 -1 0 15556 0 0 0 30956 46 0 0 25 0 1 0 481845856 66625536 15481 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 16266 15481 603 41 0 16225 0 vsize: 65064 [startup+319.997 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 3439 Raw data (stat): 3439 (minisat+) R 3438 28099 28098 0 -1 0 15815 0 0 0 31955 46 0 0 25 0 1 0 481845856 67682304 15740 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 16524 15740 603 41 0 16483 0 vsize: 66096 [startup+329.996 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 3439 Raw data (stat): 3439 (minisat+) R 3438 28099 28098 0 -1 0 16117 0 0 0 32954 47 0 0 25 0 1 0 481845856 69013504 16042 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 16849 16042 603 41 0 16808 0 vsize: 67396 [startup+339.996 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 3439 Raw data (stat): 3439 (minisat+) R 3438 28099 28098 0 -1 0 16380 0 0 0 33954 48 0 0 25 0 1 0 481845856 70074368 16305 4294967295 134512640 134672761 3221224560 3221223696 134560688 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 17108 16305 603 41 0 17067 0 vsize: 68432 [startup+349.996 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 3439 Raw data (stat): 3439 (minisat+) R 3438 28099 28098 0 -1 0 16670 0 0 0 34953 49 0 0 25 0 1 0 481845856 71131136 16595 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 17366 16595 603 41 0 17325 0 vsize: 69464 [startup+359.996 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 3439 Raw data (stat): 3439 (minisat+) R 3438 28099 28098 0 -1 0 16946 0 0 0 35953 50 0 0 25 0 1 0 481845856 72318976 16871 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 17656 16871 603 41 0 17615 0 vsize: 70624 [startup+369.996 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 3439 Raw data (stat): 3439 (minisat+) R 3438 28099 28098 0 -1 0 17203 0 0 0 36952 50 0 0 25 0 1 0 481845856 73379840 17128 4294967295 134512640 134672761 3221224560 3221223732 134556634 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 17915 17128 603 41 0 17874 0 vsize: 71660 [startup+379.995 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 3439 Raw data (stat): 3439 (minisat+) R 3438 28099 28098 0 -1 0 17518 0 0 0 37951 51 0 0 25 0 1 0 481845856 74571776 17443 4294967295 134512640 134672761 3221224560 3221223728 134560892 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 18206 17443 603 41 0 18165 0 vsize: 72824 [startup+389.995 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 3439 Raw data (stat): 3439 (minisat+) R 3438 28099 28098 0 -1 0 17840 0 0 0 38950 52 0 0 25 0 1 0 481845856 75902976 17765 4294967295 134512640 134672761 3221224560 3221223728 134561215 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 18531 17765 603 41 0 18490 0 vsize: 74124 [startup+399.995 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 3439 Raw data (stat): 3439 (minisat+) R 3438 28099 28098 0 -1 0 18104 0 0 0 39949 53 0 0 25 0 1 0 481845856 76967936 18029 4294967295 134512640 134672761 3221224560 3221223728 134561190 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 18791 18029 603 41 0 18750 0 vsize: 75164 [startup+409.994 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 3439 Raw data (stat): 3439 (minisat+) R 3438 28099 28098 0 -1 0 18367 0 0 0 40949 54 0 0 25 0 1 0 481845856 78028800 18292 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 19050 18292 603 41 0 19009 0 vsize: 76200 [startup+419.994 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 3439 Raw data (stat): 3439 (minisat+) R 3438 28099 28098 0 -1 0 18602 0 0 0 41949 55 0 0 25 0 1 0 481845856 79097856 18527 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 19311 18527 603 41 0 19270 0 vsize: 77244 [startup+429.993 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 3439 Raw data (stat): 3439 (minisat+) R 3438 28099 28098 0 -1 0 18852 0 0 0 42948 55 0 0 25 0 1 0 481845856 80027648 18777 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 19538 18777 603 41 0 19497 0 vsize: 78152 [startup+439.993 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 3439 Raw data (stat): 3439 (minisat+) R 3438 28099 28098 0 -1 0 19088 0 0 0 43947 56 0 0 25 0 1 0 481845856 80916480 19004 4294967295 134512640 134672761 3221224560 3221223744 134558899 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 19755 19004 603 41 0 19714 0 vsize: 79020 [startup+449.992 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 3439 Raw data (stat): 3439 (minisat+) R 3438 28099 28098 0 -1 0 19088 0 0 0 44947 56 0 0 25 0 1 0 481845856 80916480 19004 4294967295 134512640 134672761 3221224560 3221223760 134557814 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 19755 19004 603 41 0 19714 0 vsize: 79020 [startup+459.992 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 3439 Raw data (stat): 3439 (minisat+) R 3438 28099 28098 0 -1 0 19088 0 0 0 45947 56 0 0 25 0 1 0 481845856 80916480 19004 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 19755 19004 603 41 0 19714 0 vsize: 79020 [startup+469.993 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 3439 Raw data (stat): 3439 (minisat+) R 3438 28099 28098 0 -1 0 19088 0 0 0 46947 56 0 0 25 0 1 0 481845856 80916480 19004 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 19755 19004 603 41 0 19714 0 vsize: 79020 [startup+479.992 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 3439 Raw data (stat): 3439 (minisat+) R 3438 28099 28098 0 -1 0 19088 0 0 0 47947 56 0 0 25 0 1 0 481845856 80916480 19004 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 19755 19004 603 41 0 19714 0 vsize: 79020 [startup+489.992 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 3439 Raw data (stat): 3439 (minisat+) R 3438 28099 28098 0 -1 0 19088 0 0 0 48948 56 0 0 25 0 1 0 481845856 80916480 19004 4294967295 134512640 134672761 3221224560 3221223724 134561235 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 19755 19004 603 41 0 19714 0 vsize: 79020 [startup+499.991 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 3439 Raw data (stat): 3439 (minisat+) R 3438 28099 28098 0 -1 0 19088 0 0 0 49948 56 0 0 25 0 1 0 481845856 80916480 19004 4294967295 134512640 134672761 3221224560 3221223696 134560634 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 19755 19004 603 41 0 19714 0 vsize: 79020 [startup+509.991 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 3439 Raw data (stat): 3439 (minisat+) R 3438 28099 28098 0 -1 0 19088 0 0 0 50948 56 0 0 25 0 1 0 481845856 80916480 19004 4294967295 134512640 134672761 3221224560 3221223664 134560246 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 19755 19004 603 41 0 19714 0 vsize: 79020 [startup+519.991 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 3439 Raw data (stat): 3439 (minisat+) R 3438 28099 28098 0 -1 0 19088 0 0 0 51948 56 0 0 25 0 1 0 481845856 80916480 19004 4294967295 134512640 134672761 3221224560 3221223744 134559613 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 19755 19004 603 41 0 19714 0 vsize: 79020 [startup+529.991 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 3439 Raw data (stat): 3439 (minisat+) R 3438 28099 28098 0 -1 0 19088 0 0 0 52948 57 0 0 25 0 1 0 481845856 80916480 19004 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 19755 19004 603 41 0 19714 0 vsize: 79020 [startup+539.991 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 3439 Raw data (stat): 3439 (minisat+) R 3438 28099 28098 0 -1 0 19088 0 0 0 53948 57 0 0 25 0 1 0 481845856 80916480 19004 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 19755 19004 603 41 0 19714 0 vsize: 79020 [startup+549.99 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 3439 Raw data (stat): 3439 (minisat+) R 3438 28099 28098 0 -1 0 19088 0 0 0 54948 57 0 0 25 0 1 0 481845856 80916480 19004 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 19755 19004 603 41 0 19714 0 vsize: 79020 [startup+559.99 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 3439 Raw data (stat): 3439 (minisat+) R 3438 28099 28098 0 -1 0 19088 0 0 0 55949 57 0 0 25 0 1 0 481845856 80916480 19004 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 19755 19004 603 41 0 19714 0 vsize: 79020 [startup+569.99 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 3439 Raw data (stat): 3439 (minisat+) R 3438 28099 28098 0 -1 0 19088 0 0 0 56949 57 0 0 25 0 1 0 481845856 80916480 19004 4294967295 134512640 134672761 3221224560 3221223728 134560940 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 19755 19004 603 41 0 19714 0 vsize: 79020 [startup+579.989 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 3439 Raw data (stat): 3439 (minisat+) R 3438 28099 28098 0 -1 0 19088 0 0 0 57949 57 0 0 25 0 1 0 481845856 80916480 19004 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 19755 19004 603 41 0 19714 0 vsize: 79020 [startup+589.989 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 3439 Raw data (stat): 3439 (minisat+) R 3438 28099 28098 0 -1 0 19088 0 0 0 58949 57 0 0 25 0 1 0 481845856 80916480 19004 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 19755 19004 603 41 0 19714 0 vsize: 79020 [startup+599.99 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 3439 Raw data (stat): 3439 (minisat+) R 3438 28099 28098 0 -1 0 19088 0 0 0 59949 57 0 0 25 0 1 0 481845856 80916480 19004 4294967295 134512640 134672761 3221224560 3221223696 134560688 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 19755 19004 603 41 0 19714 0 vsize: 79020 [startup+609.989 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 3439 Raw data (stat): 3439 (minisat+) R 3438 28099 28098 0 -1 0 19088 0 0 0 60949 57 0 0 25 0 1 0 481845856 80916480 19004 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 19755 19004 603 41 0 19714 0 vsize: 79020 [startup+619.989 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 3439 Raw data (stat): 3439 (minisat+) R 3438 28099 28098 0 -1 0 19088 0 0 0 61950 57 0 0 25 0 1 0 481845856 80916480 19004 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 19755 19004 603 41 0 19714 0 vsize: 79020 [startup+629.988 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 3439 Raw data (stat): 3439 (minisat+) R 3438 28099 28098 0 -1 0 19088 0 0 0 62950 57 0 0 25 0 1 0 481845856 80916480 19004 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 19755 19004 603 41 0 19714 0 vsize: 79020 [startup+639.989 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 3439 Raw data (stat): 3439 (minisat+) R 3438 28099 28098 0 -1 0 19088 0 0 0 63950 57 0 0 25 0 1 0 481845856 80916480 19004 4294967295 134512640 134672761 3221224560 3221223728 134561198 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 19755 19004 603 41 0 19714 0 vsize: 79020 [startup+649.989 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 3439 Raw data (stat): 3439 (minisat+) R 3438 28099 28098 0 -1 0 19088 0 0 0 64950 57 0 0 25 0 1 0 481845856 80916480 19004 4294967295 134512640 134672761 3221224560 3221223728 134560909 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 19755 19004 603 41 0 19714 0 vsize: 79020 [startup+659.989 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 3439 Raw data (stat): 3439 (minisat+) R 3438 28099 28098 0 -1 0 19088 0 0 0 65950 57 0 0 25 0 1 0 481845856 80916480 19004 4294967295 134512640 134672761 3221224560 3221223728 134561167 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 19755 19004 603 41 0 19714 0 vsize: 79020 [startup+670.075 s] Raw data (loadavg): 1.15 1.00 0.92 2/57 3488 Raw data (stat): 3439 (minisat+) R 3438 28099 28098 0 -1 0 19088 0 0 0 66959 57 0 0 25 0 1 0 481845856 80916480 19004 4294967295 134512640 134672761 3221224560 3221223728 134561229 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 19755 19004 603 41 0 19714 0 vsize: 79020 [startup+680.074 s] Raw data (loadavg): 1.12 1.00 0.92 2/54 3492 Raw data (stat): 3439 (minisat+) R 3438 28099 28098 0 -1 0 19088 0 0 0 67959 57 0 0 25 0 1 0 481845856 80916480 19004 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 19755 19004 603 41 0 19714 0 vsize: 79020 [startup+690.248 s] Raw data (loadavg): 1.10 1.00 0.92 2/54 3492 Raw data (stat): 3439 (minisat+) R 3438 28099 28098 0 -1 0 19088 0 0 0 68977 57 0 0 25 0 1 0 481845856 80916480 19004 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 19755 19004 603 41 0 19714 0 vsize: 79020 [startup+700.248 s] Raw data (loadavg): 1.09 1.00 0.92 2/54 3492 Raw data (stat): 3439 (minisat+) R 3438 28099 28098 0 -1 0 19088 0 0 0 69977 57 0 0 25 0 1 0 481845856 80916480 19004 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 19755 19004 603 41 0 19714 0 vsize: 79020 [startup+710.25 s] Raw data (loadavg): 1.07 1.00 0.92 2/54 3492 Raw data (stat): 3439 (minisat+) R 3438 28099 28098 0 -1 0 19088 0 0 0 70977 57 0 0 25 0 1 0 481845856 80916480 19004 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 19755 19004 603 41 0 19714 0 vsize: 79020 [startup+720.25 s] Raw data (loadavg): 1.06 1.00 0.92 2/54 3492 Raw data (stat): 3439 (minisat+) R 3438 28099 28098 0 -1 0 19088 0 0 0 71977 57 0 0 25 0 1 0 481845856 80916480 19004 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 19755 19004 603 41 0 19714 0 vsize: 79020 [startup+730.249 s] Raw data (loadavg): 1.05 1.00 0.92 2/54 3492 Raw data (stat): 3439 (minisat+) R 3438 28099 28098 0 -1 0 19088 0 0 0 72977 57 0 0 25 0 1 0 481845856 80916480 19004 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 19755 19004 603 41 0 19714 0 vsize: 79020 [startup+740.25 s] Raw data (loadavg): 1.04 1.00 0.92 2/54 3494 Raw data (stat): 3439 (minisat+) R 3438 28099 28098 0 -1 0 19158 0 0 0 73978 57 0 0 25 0 1 0 481845856 81313792 19074 4294967295 134512640 134672761 3221224560 3221223728 134561229 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 19852 19074 603 41 0 19811 0 vsize: 79408 [startup+750.249 s] Raw data (loadavg): 1.04 1.00 0.92 2/54 3494 Raw data (stat): 3439 (minisat+) R 3438 28099 28098 0 -1 0 19340 0 0 0 74977 57 0 0 25 0 1 0 481845856 81977344 19256 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 20014 19256 603 41 0 19973 0 vsize: 80056 [startup+760.25 s] Raw data (loadavg): 1.03 1.00 0.92 2/54 3494 Raw data (stat): 3439 (minisat+) R 3438 28099 28098 0 -1 0 19514 0 0 0 75977 57 0 0 25 0 1 0 481845856 82780160 19430 4294967295 134512640 134672761 3221224560 3221223728 134561193 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 20210 19430 603 41 0 20169 0 vsize: 80840 [startup+770.25 s] Raw data (loadavg): 1.03 1.00 0.92 2/54 3494 Raw data (stat): 3439 (minisat+) R 3438 28099 28098 0 -1 0 19669 0 0 0 76977 58 0 0 25 0 1 0 481845856 83304448 19585 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 20338 19585 603 41 0 20297 0 vsize: 81352 [startup+780.249 s] Raw data (loadavg): 1.02 1.00 0.92 2/54 3494 Raw data (stat): 3439 (minisat+) R 3438 28099 28098 0 -1 0 19844 0 0 0 77977 58 0 0 25 0 1 0 481845856 84090880 19760 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 20530 19760 603 41 0 20489 0 vsize: 82120 [startup+790.249 s] Raw data (loadavg): 1.02 1.00 0.92 2/54 3494 Raw data (stat): 3439 (minisat+) R 3438 28099 28098 0 -1 0 20029 0 0 0 78977 58 0 0 25 0 1 0 481845856 84877312 19945 4294967295 134512640 134672761 3221224560 3221223728 134561151 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 20722 19945 603 41 0 20681 0 vsize: 82888 [startup+800.249 s] Raw data (loadavg): 1.01 1.00 0.92 2/54 3494 Raw data (stat): 3439 (minisat+) R 3438 28099 28098 0 -1 0 20217 0 0 0 79976 59 0 0 25 0 1 0 481845856 86061056 20133 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 21011 20133 603 41 0 20970 0 vsize: 84044 [startup+810.249 s] Raw data (loadavg): 1.01 1.00 0.92 2/54 3494 Raw data (stat): 3439 (minisat+) R 3438 28099 28098 0 -1 0 20392 0 0 0 80976 59 0 0 25 0 1 0 481845856 86859776 20308 4294967295 134512640 134672761 3221224560 3221223728 134560940 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 21206 20308 603 41 0 21165 0 vsize: 84824 [startup+820.249 s] Raw data (loadavg): 1.01 1.00 0.92 2/54 3494 Raw data (stat): 3439 (minisat+) R 3438 28099 28098 0 -1 0 20556 0 0 0 81976 60 0 0 25 0 1 0 481845856 87523328 20472 4294967295 134512640 134672761 3221224560 3221223664 134560381 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 21368 20472 603 41 0 21327 0 vsize: 85472 [startup+830.249 s] Raw data (loadavg): 1.01 1.00 0.92 2/54 3494 Raw data (stat): 3439 (minisat+) R 3438 28099 28098 0 -1 0 20706 0 0 0 82976 60 0 0 25 0 1 0 481845856 88059904 20622 4294967295 134512640 134672761 3221224560 3221223744 134559031 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 21499 20622 603 41 0 21458 0 vsize: 85996 [startup+840.249 s] Raw data (loadavg): 1.01 1.00 0.92 2/54 3494 Raw data (stat): 3439 (minisat+) R 3438 28099 28098 0 -1 0 20835 0 0 0 83975 61 0 0 25 0 1 0 481845856 88584192 20751 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 21627 20751 603 41 0 21586 0 vsize: 86508 [startup+850.248 s] Raw data (loadavg): 1.00 1.00 0.92 2/54 3494 Raw data (stat): 3439 (minisat+) R 3438 28099 28098 0 -1 0 20968 0 0 0 84975 61 0 0 25 0 1 0 481845856 89112576 20884 4294967295 134512640 134672761 3221224560 3221223728 134561215 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 21756 20884 603 41 0 21715 0 vsize: 87024 [startup+860.248 s] Raw data (loadavg): 1.00 1.00 0.92 2/54 3494 Raw data (stat): 3439 (minisat+) R 3438 28099 28098 0 -1 0 21092 0 0 0 85975 61 0 0 25 0 1 0 481845856 89636864 21008 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 21884 21008 603 41 0 21843 0 vsize: 87536 [startup+870.248 s] Raw data (loadavg): 1.00 1.00 0.92 2/54 3494 Raw data (stat): 3439 (minisat+) R 3438 28099 28098 0 -1 0 21207 0 0 0 86975 62 0 0 25 0 1 0 481845856 90034176 21123 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 21981 21123 603 41 0 21940 0 vsize: 87924 [startup+880.247 s] Raw data (loadavg): 1.00 1.00 0.92 2/54 3494 Raw data (stat): 3439 (minisat+) R 3438 28099 28098 0 -1 0 21325 0 0 0 87975 62 0 0 25 0 1 0 481845856 90566656 21241 4294967295 134512640 134672761 3221224560 3221223696 134560588 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 22111 21241 603 41 0 22070 0 vsize: 88444 [startup+890.247 s] Raw data (loadavg): 1.00 1.00 0.92 2/54 3494 Raw data (stat): 3439 (minisat+) R 3438 28099 28098 0 -1 0 21444 0 0 0 88974 62 0 0 25 0 1 0 481845856 91090944 21360 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 22239 21360 603 41 0 22198 0 vsize: 88956 [startup+900.246 s] Raw data (loadavg): 1.00 1.00 0.92 2/54 3494 Raw data (stat): 3439 (minisat+) R 3438 28099 28098 0 -1 0 21561 0 0 0 89974 63 0 0 25 0 1 0 481845856 91484160 21477 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 22335 21477 603 41 0 22294 0 vsize: 89340 [startup+910.247 s] Raw data (loadavg): 1.00 1.00 0.92 2/54 3494 Raw data (stat): 3439 (minisat+) R 3438 28099 28098 0 -1 0 21677 0 0 0 90974 63 0 0 25 0 1 0 481845856 92012544 21593 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 22464 21593 603 41 0 22423 0 vsize: 89856 [startup+920.247 s] Raw data (loadavg): 1.00 1.00 0.92 2/54 3494 Raw data (stat): 3439 (minisat+) R 3438 28099 28098 0 -1 0 21781 0 0 0 91974 63 0 0 25 0 1 0 481845856 92409856 21697 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 22561 21697 603 41 0 22520 0 vsize: 90244 [startup+930.246 s] Raw data (loadavg): 1.00 1.00 0.92 2/54 3494 Raw data (stat): 3439 (minisat+) R 3438 28099 28098 0 -1 0 21904 0 0 0 92973 64 0 0 25 0 1 0 481845856 92934144 21820 4294967295 134512640 134672761 3221224560 3221223656 1075347133 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 22689 21820 603 41 0 22648 0 vsize: 90756 [startup+940.246 s] Raw data (loadavg): 1.00 1.00 0.92 2/54 3494 Raw data (stat): 3439 (minisat+) R 3438 28099 28098 0 -1 0 22015 0 0 0 93973 64 0 0 25 0 1 0 481845856 93462528 21931 4294967295 134512640 134672761 3221224560 3221223728 134560839 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 22818 21931 603 41 0 22777 0 vsize: 91272 [startup+950.246 s] Raw data (loadavg): 1.00 1.00 0.92 2/54 3494 Raw data (stat): 3439 (minisat+) R 3438 28099 28098 0 -1 0 22129 0 0 0 94973 65 0 0 25 0 1 0 481845856 93859840 22045 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 22915 22045 603 41 0 22874 0 vsize: 91660 [startup+960.246 s] Raw data (loadavg): 1.00 1.00 0.92 2/54 3494 Raw data (stat): 3439 (minisat+) R 3438 28099 28098 0 -1 0 22250 0 0 0 95973 65 0 0 25 0 1 0 481845856 94384128 22166 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 23043 22166 603 41 0 23002 0 vsize: 92172 [startup+970.246 s] Raw data (loadavg): 1.00 1.00 0.92 2/54 3494 Raw data (stat): 3439 (minisat+) R 3438 28099 28098 0 -1 0 22361 0 0 0 96972 65 0 0 25 0 1 0 481845856 94777344 22277 4294967295 134512640 134672761 3221224560 3221223728 134561190 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 23139 22277 603 41 0 23098 0 vsize: 92556 [startup+980.246 s] Raw data (loadavg): 1.00 1.00 0.92 2/54 3494 Raw data (stat): 3439 (minisat+) R 3438 28099 28098 0 -1 0 22460 0 0 0 97972 65 0 0 25 0 1 0 481845856 95174656 22376 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 23236 22376 603 41 0 23195 0 vsize: 92944 [startup+990.246 s] Raw data (loadavg): 1.00 1.00 0.92 2/54 3494 Raw data (stat): 3439 (minisat+) R 3438 28099 28098 0 -1 0 22576 0 0 0 98972 66 0 0 25 0 1 0 481845856 95703040 22492 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 23365 22492 603 41 0 23324 0 vsize: 93460 [startup+1000.25 s] Raw data (loadavg): 1.00 1.00 0.92 2/54 3494 Raw data (stat): 3439 (minisat+) R 3438 28099 28098 0 -1 0 22707 0 0 0 99972 66 0 0 25 0 1 0 481845856 96227328 22623 4294967295 134512640 134672761 3221224560 3221223696 134565092 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 23493 22623 603 41 0 23452 0 vsize: 93972 [startup+1010.25 s] Raw data (loadavg): 1.00 1.00 0.92 2/54 3496 Raw data (stat): 3439 (minisat+) R 3438 28099 28098 0 -1 0 22817 0 0 0 100972 67 0 0 25 0 1 0 481845856 96620544 22733 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 23589 22733 603 41 0 23548 0 vsize: 94356 [startup+1020.25 s] Raw data (loadavg): 1.00 1.00 0.92 2/54 3496 Raw data (stat): 3439 (minisat+) R 3438 28099 28098 0 -1 0 22918 0 0 0 101972 67 0 0 25 0 1 0 481845856 97017856 22834 4294967295 134512640 134672761 3221224560 3221223728 134560940 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 23686 22834 603 41 0 23645 0 vsize: 94744 [startup+1030.25 s] Raw data (loadavg): 1.00 1.00 0.92 2/54 3496 Raw data (stat): 3439 (minisat+) R 3438 28099 28098 0 -1 0 23010 0 0 0 102972 67 0 0 25 0 1 0 481845856 97431552 22926 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 23787 22926 603 41 0 23746 0 vsize: 95148 [startup+1040.25 s] Raw data (loadavg): 1.00 1.00 0.92 2/54 3496 Raw data (stat): 3439 (minisat+) R 3438 28099 28098 0 -1 0 23092 0 0 0 103972 67 0 0 25 0 1 0 481845856 97828864 23008 4294967295 134512640 134672761 3221224560 3221223728 134561001 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 23884 23008 603 41 0 23843 0 vsize: 95536 [startup+1050.25 s] Raw data (loadavg): 1.00 1.00 0.92 2/54 3496 Raw data (stat): 3439 (minisat+) R 3438 28099 28098 0 -1 0 23185 0 0 0 104972 68 0 0 25 0 1 0 481845856 98230272 23101 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 23982 23101 603 41 0 23941 0 vsize: 95928 [startup+1060.25 s] Raw data (loadavg): 1.00 1.00 0.92 2/54 3496 Raw data (stat): 3439 (minisat+) R 3438 28099 28098 0 -1 0 23267 0 0 0 105972 68 0 0 25 0 1 0 481845856 98496512 23183 4294967295 134512640 134672761 3221224560 3221223728 134560892 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 24047 23183 603 41 0 24006 0 vsize: 96188 [startup+1070.25 s] Raw data (loadavg): 1.00 1.00 0.92 2/54 3496 Raw data (stat): 3439 (minisat+) R 3438 28099 28098 0 -1 0 23340 0 0 0 106972 68 0 0 25 0 1 0 481845856 98758656 23256 4294967295 134512640 134672761 3221224560 3221223728 134561229 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 24111 23256 603 41 0 24070 0 vsize: 96444 [startup+1080.25 s] Raw data (loadavg): 1.00 1.00 0.92 2/54 3496 Raw data (stat): 3439 (minisat+) R 3438 28099 28098 0 -1 0 23435 0 0 0 107972 68 0 0 25 0 1 0 481845856 99151872 23351 4294967295 134512640 134672761 3221224560 3221223696 134560677 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 24207 23351 603 41 0 24166 0 vsize: 96828 [startup+1090.25 s] Raw data (loadavg): 1.00 1.00 0.92 2/54 3496 Raw data (stat): 3439 (minisat+) R 3438 28099 28098 0 -1 0 23542 0 0 0 108972 68 0 0 25 0 1 0 481845856 99549184 23458 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 24304 23458 603 41 0 24263 0 vsize: 97216 [startup+1100.25 s] Raw data (loadavg): 1.00 1.00 0.92 2/54 3496 Raw data (stat): 3439 (minisat+) R 3438 28099 28098 0 -1 0 23641 0 0 0 109971 69 0 0 25 0 1 0 481845856 99950592 23557 4294967295 134512640 134672761 3221224560 3221223728 134561151 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 24402 23557 603 41 0 24361 0 vsize: 97608 [startup+1110.25 s] Raw data (loadavg): 1.00 1.00 0.92 2/54 3496 Raw data (stat): 3439 (minisat+) R 3438 28099 28098 0 -1 0 23723 0 0 0 110971 69 0 0 25 0 1 0 481845856 100343808 23639 4294967295 134512640 134672761 3221224560 3221223744 134559463 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 24498 23639 603 41 0 24457 0 vsize: 97992 [startup+1120.25 s] Raw data (loadavg): 1.00 1.00 0.92 2/54 3496 Raw data (stat): 3439 (minisat+) R 3438 28099 28098 0 -1 0 23804 0 0 0 111971 69 0 0 25 0 1 0 481845856 100630528 23720 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 24568 23720 603 41 0 24527 0 vsize: 98272 [startup+1130.25 s] Raw data (loadavg): 1.00 1.00 0.92 2/54 3496 Raw data (stat): 3439 (minisat+) R 3438 28099 28098 0 -1 0 23908 0 0 0 112971 69 0 0 25 0 1 0 481845856 101027840 23824 4294967295 134512640 134672761 3221224560 3221223728 134561193 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 24665 23824 603 41 0 24624 0 vsize: 98660 [startup+1140.25 s] Raw data (loadavg): 1.00 1.00 0.92 2/54 3496 Raw data (stat): 3439 (minisat+) R 3438 28099 28098 0 -1 0 23944 0 0 0 113972 69 0 0 25 0 1 0 481845856 101158912 23860 4294967295 134512640 134672761 3221224560 3221223664 134560196 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 24697 23860 603 41 0 24656 0 vsize: 98788 [startup+1150.25 s] Raw data (loadavg): 1.00 1.00 0.92 2/54 3496 Raw data (stat): 3439 (minisat+) R 3438 28099 28098 0 -1 0 23944 0 0 0 114972 69 0 0 25 0 1 0 481845856 101158912 23860 4294967295 134512640 134672761 3221224560 3221223728 134560994 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 24697 23860 603 41 0 24656 0 vsize: 98788 [startup+1160.25 s] Raw data (loadavg): 1.00 1.00 0.92 2/54 3496 Raw data (stat): 3439 (minisat+) R 3438 28099 28098 0 -1 0 23944 0 0 0 115971 70 0 0 25 0 1 0 481845856 101158912 23860 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 24697 23860 603 41 0 24656 0 vsize: 98788 [startup+1170.25 s] Raw data (loadavg): 1.00 1.00 0.92 2/54 3496 Raw data (stat): 3439 (minisat+) R 3438 28099 28098 0 -1 0 23944 0 0 0 116971 70 0 0 25 0 1 0 481845856 101158912 23860 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 24697 23860 603 41 0 24656 0 vsize: 98788 [startup+1180.25 s] Raw data (loadavg): 1.00 1.00 0.92 2/54 3496 Raw data (stat): 3439 (minisat+) R 3438 28099 28098 0 -1 0 23944 0 0 0 117971 70 0 0 25 0 1 0 481845856 101158912 23860 4294967295 134512640 134672761 3221224560 3221223728 134560871 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 24697 23860 603 41 0 24656 0 vsize: 98788 [startup+1190.25 s] Raw data (loadavg): 1.00 1.00 0.92 2/54 3496 Raw data (stat): 3439 (minisat+) R 3438 28099 28098 0 -1 0 23944 0 0 0 118972 70 0 0 25 0 1 0 481845856 101158912 23860 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 24697 23860 603 41 0 24656 0 vsize: 98788 [startup+1200.25 s] Raw data (loadavg): 1.00 1.00 0.92 2/54 3496 Raw data (stat): 3439 (minisat+) R 3438 28099 28098 0 -1 0 23944 0 0 0 119972 70 0 0 25 0 1 0 481845856 101158912 23860 4294967295 134512640 134672761 3221224560 3221223728 134560882 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 24697 23860 603 41 0 24656 0 vsize: 98788 Maximum CPU time exceeded: sending SIGTERM and SIGKILL [startup+1200.3 s] Raw data (loadavg): 1.00 1.00 0.92 1/54 3496 Raw data (stat): 3439 (minisat+) Z 3438 28099 28098 0 -1 12 23947 0 0 0 119972 74 0 0 25 0 1 0 481845856 0 0 4294967295 0 0 0 0 0 0 16384 5 16386 3222412051 0 0 17 0 0 0 Raw data (statm): 0 0 0 0 0 0 0 vsize: 0 Maximum CPU time exceeded: sending SIGTERM and SIGKILL Child status: 10 Real time (s): 1200.3 CPU time (s): 1200.47 CPU user time (s): 1199.72 CPU system time (s): 0.743886 CPU usage (%): 100.014 Max. virtual memory (Kb): 98788 #### END WATCHER DATA #### #### BEGIN VERIFIER DATA #### ERROR: no interpretation found ! #### END VERIFIER DATA ####