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 wulflinc4 THE 2005-04-14 02:57:46 (client local time) PB2005-SCRIPT v4.0 MARKUPS: idlaunch=4475 boxname=wulflinc4 idbench=339 idsolver=12 numberseed=0 MD5SUM SOLVER: MD5SUM BENCH: 20fc65112f36a5d10cc9eaa82c0beb63 /oldhome/oroussel/tmp/wulflinc4/normalized-frb53-24-1.opb REAL COMMAND: minisat+ -cb -gs /oldhome/oroussel/tmp/wulflinc4/normalized-frb53-24-1.opb /oldhome/oroussel/tmp/wulflinc4/normalized-frb53-24-1.opb IDLAUNCH: 4475 /proc/cpuinfo: processor : 0 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 2 cpu MHz : 451.169 cache size : 512 KB fdiv_bug : no hlt_bug : no f00f_bug : no coma_bug : no fpu : yes fpu_exception : yes cpuid level : 2 wp : yes flags : fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse bogomips : 890.88 processor : 1 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 2 cpu MHz : 451.169 cache size : 512 KB fdiv_bug : no hlt_bug : no f00f_bug : no coma_bug : no fpu : yes fpu_exception : yes cpuid level : 2 wp : yes flags : fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse bogomips : 899.07 /proc/meminfo: MemTotal: 1034660 kB MemFree: 890196 kB Buffers: 36288 kB Cached: 87676 kB SwapCached: 0 kB Active: 57328 kB Inactive: 69516 kB HighTotal: 131008 kB HighFree: 39508 kB LowTotal: 903652 kB LowFree: 850688 kB SwapTotal: 2097136 kB SwapFree: 2097136 kB Dirty: 28 kB Writeback: 0 kB Mapped: 6920 kB Slab: 11976 kB Committed_AS: 71676 kB PageTables: 316 kB VmallocTotal: 114680 kB VmallocUsed: 1388 kB VmallocChunk: 113256 kB JOB ENDED THE 2005-04-14 03:17:48 (client local time) WITH STATUS 10 IN 1200.22 SECONDS stats: 4475 7 1200.22 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 | 169273 364509 | 56424 0 0 nan | 0.000 % | c | 100 | 168899 363733 | 62066 65 591 9.1 | 0.407 % | c | 250 | 168502 362906 | 68273 198 1311 6.6 | 0.828 % | c | 475 | 167076 359832 | 75100 351 2932 8.4 | 2.494 % | c | 812 | 165133 355593 | 82610 631 5067 8.0 | 4.688 % | c | 1319 | 162313 349369 | 90871 972 8957 9.2 | 8.080 % | c | 2078 | 157982 339700 | 99958 1468 15263 10.4 | 13.235 % | 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 | 2296 | 157388 338635 | 52462 1645 17452 10.6 | 13.235 % | c | 2397 | 157059 337878 | 57708 1732 17985 10.4 | 14.608 % | c | 2548 | 155840 335129 | 63479 1821 18984 10.4 | 16.160 % | c | 2773 | 154165 331306 | 69826 1966 20681 10.5 | 18.177 % | c | 3110 | 151458 325155 | 76809 2174 23582 10.8 | 21.604 % | c | 3616 | 147626 316455 | 84490 2526 28129 11.1 | 26.258 % | c | 4375 | 143472 307009 | 92939 3028 34893 11.5 | 31.480 % | c | 5514 | 137035 292201 | 102233 3700 43332 11.7 | 39.456 % | c | 7223 | 129643 274879 | 112456 4787 55808 11.7 | 48.879 % | c | 9785 | 121178 254842 | 123702 6238 75388 12.1 | 60.010 % | c | 13629 | 111810 232544 | 136072 8363 107856 12.9 | 72.370 % | 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 | 13714 | 111791 232457 | 37263 8438 110430 13.1 | 72.370 % | c | 13815 | 111736 232336 | 40989 8517 111608 13.1 | 72.463 % | c | 13965 | 111449 231624 | 45088 8613 112090 13.0 | 72.865 % | c | 14191 | 110875 230219 | 49597 8726 114161 13.1 | 73.663 % | c | 14528 | 110330 228918 | 54556 8862 116391 13.1 | 74.395 % | c | 15034 | 109915 227905 | 60012 9207 123608 13.4 | 74.966 % | 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 | 15297 | 109425 226747 | 36475 9363 132070 14.1 | 74.966 % | c | 15397 | 108928 225548 | 40122 9368 131994 14.1 | 76.327 % | c | 15547 | 108861 225391 | 44134 9505 134463 14.1 | 76.414 % | c | 15772 | 108187 223757 | 48548 9615 136618 14.2 | 77.343 % | c | 16110 | 108184 223750 | 53403 9952 143364 14.4 | 77.347 % | c | 16616 | 107846 222930 | 58743 10285 150811 14.7 | 77.809 % | c | 17375 | 107492 222096 | 64617 10880 162733 15.0 | 78.273 % | c | 18516 | 106409 219476 | 71079 11485 183931 16.0 | 79.751 % | c | 20224 | 105563 217441 | 78187 12695 231153 18.2 | 80.890 % | 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 | 22454 | 104461 214676 | 34820 14284 295984 20.7 | 80.890 % | c | 22554 | 104247 214159 | 38302 14343 296650 20.7 | 82.669 % | c | 22704 | 104230 214116 | 42132 14478 302277 20.9 | 82.695 % | c | 22929 | 104077 213747 | 46345 14609 305744 20.9 | 82.903 % | c | 23266 | 103810 213088 | 50979 14674 310610 21.2 | 83.278 % | c | 23772 | 103661 212727 | 56077 15056 324943 21.6 | 83.483 % | c | 24531 | 103661 212727 | 61685 15815 342397 21.7 | 83.483 % | 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 | 24866 | 103578 212555 | 34526 15940 354982 22.3 | 83.483 % | c | 24966 | 103452 212229 | 37978 15957 356178 22.3 | 83.832 % | c | 25116 | 103157 211504 | 41776 15858 355829 22.4 | 84.245 % | c | 25342 | 103098 211357 | 45954 15982 361200 22.6 | 84.328 % | c | 25679 | 103060 211263 | 50549 16275 374557 23.0 | 84.383 % | c | 26186 | 103044 211225 | 55604 16717 403210 24.1 | 84.404 % | c | 26946 | 102964 211037 | 61164 17402 448444 25.8 | 84.509 % | c | 28085 | 102796 210627 | 67281 18302 513844 28.1 | 84.741 % | c | 29794 | 102287 209397 | 74009 19277 595883 30.9 | 85.430 % | 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 | 30805 | 102185 209122 | 34061 19877 649107 32.7 | 85.430 % | c | 30905 | 102181 209112 | 37467 19960 650513 32.6 | 85.578 % | c | 31055 | 102181 209112 | 41213 20110 656361 32.6 | 85.578 % | c | 31280 | 102181 209112 | 45335 20335 662267 32.6 | 85.578 % | c | 31617 | 102139 209012 | 49868 20565 689479 33.5 | 85.635 % | c | 32123 | 102135 209002 | 54855 21042 708226 33.7 | 85.640 % | c | 32883 | 102044 208779 | 60341 21692 763522 35.2 | 85.765 % | c | 34023 | 101908 208436 | 66375 22590 857752 38.0 | 85.961 % | c | 35731 | 101761 208078 | 73012 24035 977376 40.7 | 86.166 % | c | 38294 | 101248 206822 | 80314 25704 1211706 47.1 | 86.880 % | 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 | 40062 | 101189 206683 | 33729 27299 1370590 50.2 | 86.880 % | c | 40164 | 101153 206593 | 37101 27290 1368576 50.1 | 87.022 % | c | 40314 | 101153 206593 | 40812 27440 1373157 50.0 | 87.022 % | c | 40539 | 101153 206593 | 44893 27665 1390604 50.3 | 87.022 % | c | 40877 | 101147 206579 | 49382 27982 1417890 50.7 | 87.029 % | c | 41383 | 101089 206432 | 54320 28284 1476102 52.2 | 87.111 % | c | 42142 | 101046 206333 | 59752 28842 1548069 53.7 | 87.164 % | c | 43281 | 101030 206295 | 65728 29940 1653263 55.2 | 87.185 % | 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 | 43660 | 101019 206233 | 33673 30108 1656622 55.0 | 87.185 % | c | 43762 | 100999 206179 | 37040 30194 1661991 55.0 | 87.234 % | c | 43912 | 100999 206179 | 40744 30344 1674049 55.2 | 87.234 % | c | 44138 | 100999 206179 | 44818 30570 1677140 54.9 | 87.234 % | c | 44476 | 100999 206179 | 49300 30908 1697757 54.9 | 87.234 % | c | 44983 | 100999 206179 | 54230 31415 1748048 55.6 | 87.234 % | c | 45742 | 100961 206093 | 59653 32036 1808118 56.4 | 87.281 % | c | 46881 | 100961 206093 | 65619 33175 1962362 59.2 | 87.281 % | c | 48589 | 100961 206093 | 72181 34883 2133447 61.2 | 87.281 % | c | 51151 | 100916 205984 | 79399 37289 2446159 65.6 | 87.343 % | c | 54995 | 100889 205925 | 87339 40682 2985421 73.4 | 87.374 % | c | 60761 | 100889 205925 | 96072 46448 3854427 83.0 | 87.374 % | 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 | 65334 | 100853 205854 | 33617 50820 4571720 90.0 | 87.374 % | c | 65434 | 100853 205854 | 36978 50920 4575895 89.9 | 87.450 % | c | 65584 | 100853 205854 | 40676 51070 4590180 89.9 | 87.450 % | c | 65809 | 100853 205854 | 44744 51295 4602588 89.7 | 87.450 % | c | 66148 | 100853 205854 | 49218 51634 4624017 89.6 | 87.450 % | c | 66654 | 100853 205854 | 54140 52140 4670967 89.6 | 87.450 % | c | 67414 | 100814 205757 | 59554 52773 4715984 89.4 | 87.506 % | c | 68553 | 100814 205757 | 65510 53912 4839522 89.8 | 87.506 % | c | 70261 | 100814 205757 | 72061 55620 5031215 90.5 | 87.506 % | c | 72824 | 100814 205757 | 79267 58183 5325863 91.5 | 87.506 % | c | 76668 | 100814 205757 | 87193 62027 5737838 92.5 | 87.506 % | c | 82434 | 100720 205535 | 95913 67266 6413842 95.4 | 87.630 % | c | 91084 | 100718 205529 | 105504 75912 7268264 95.7 | 87.634 % | 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 | 94590 | 100693 205448 | 33564 79088 7509816 95.0 | 87.634 % | c | 94690 | 100693 205448 | 36920 19014 1203514 63.3 | 87.669 % | c | 94840 | 100693 205448 | 40612 19164 1215224 63.4 | 87.669 % | c | 95066 | 100610 205251 | 44673 19386 1226784 63.3 | 87.776 % | c | 95404 | 100605 205238 | 49141 19716 1247119 63.3 | 87.784 % | c | 95910 | 100605 205238 | 54055 20222 1293892 64.0 | 87.784 % | c | 96671 | 100605 205238 | 59460 20983 1362659 64.9 | 87.784 % | c | 97810 | 100602 205231 | 65406 22119 1452373 65.7 | 87.788 % | c | 99519 | 100602 205231 | 71947 23828 1570680 65.9 | 87.788 % | c | 102082 | 100602 205231 | 79142 26391 1796590 68.1 | 87.788 % | c | 105926 | 100524 205033 | 87056 30221 2254790 74.6 | 87.904 % | c | 111693 | 100513 205008 | 95762 35977 2865103 79.6 | 87.917 % | c | 120342 | 100496 204969 | 105338 44621 3803842 85.2 | 87.939 % | c | 133316 | 100496 204969 | 115872 57595 5193648 90.2 | 87.939 % | c | 152777 | 100477 204922 | 127459 77043 7291374 94.6 | 87.966 % | c | 181969 | 100467 204900 | 140205 106227 10898164 102.6 | 87.978 % | c | 225758 | 100436 204820 | 154225 149983 15472459 103.2 | 88.024 % | c | 291443 | 100430 204806 | 169648 36460 2449536 67.2 | 88.032 % | 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.91 0.95 0.90 2/54 12687 Raw data (stat): 12687 (runsolver) R 12686 5897 5896 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 422943196 1052672 99 4294967295 134512640 135381576 3221224448 3221219692 135158418 0 2147483391 7 90112 0 0 0 17 1 0 0 Raw data (statm): 257 99 215 215 0 42 0 vsize: 1028 [startup+10.0005 s] Raw data (loadavg): 0.93 0.95 0.90 2/54 12687 Raw data (stat): 12687 (minisat+) R 12686 5897 5896 0 -1 0 5627 0 0 0 983 16 0 0 25 0 1 0 422943196 26091520 5605 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 6370 5605 603 41 0 6329 0 vsize: 25480 [startup+20.0012 s] Raw data (loadavg): 0.94 0.96 0.91 2/54 12687 Raw data (stat): 12687 (minisat+) R 12686 5897 5896 0 -1 0 5634 0 0 0 1982 16 0 0 25 0 1 0 422943196 26091520 5612 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 6370 5612 603 41 0 6329 0 vsize: 25480 [startup+30.0016 s] Raw data (loadavg): 0.95 0.96 0.91 2/54 12687 Raw data (stat): 12687 (minisat+) R 12686 5897 5896 0 -1 0 5783 0 0 0 2982 17 0 0 25 0 1 0 422943196 27074560 5761 4294967295 134512640 134672761 3221224560 3221223732 134556660 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 6610 5761 603 41 0 6569 0 vsize: 26440 [startup+40.0033 s] Raw data (loadavg): 0.95 0.96 0.91 2/54 12687 Raw data (stat): 12687 (minisat+) R 12686 5897 5896 0 -1 0 5783 0 0 0 3982 17 0 0 25 0 1 0 422943196 27074560 5761 4294967295 134512640 134672761 3221224560 3221223728 134561001 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 6610 5761 603 41 0 6569 0 vsize: 26440 [startup+50.0038 s] Raw data (loadavg): 0.96 0.96 0.91 2/54 12687 Raw data (stat): 12687 (minisat+) R 12686 5897 5896 0 -1 0 5783 0 0 0 4981 17 0 0 25 0 1 0 422943196 27074560 5761 4294967295 134512640 134672761 3221224560 3221223764 134561964 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 6610 5761 603 41 0 6569 0 vsize: 26440 [startup+60.0032 s] Raw data (loadavg): 0.97 0.96 0.91 2/54 12687 Raw data (stat): 12687 (minisat+) R 12686 5897 5896 0 -1 0 5783 0 0 0 5981 17 0 0 25 0 1 0 422943196 27074560 5761 4294967295 134512640 134672761 3221224560 3221223752 134556585 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 6610 5761 603 41 0 6569 0 vsize: 26440 [startup+70.0045 s] Raw data (loadavg): 0.97 0.96 0.91 2/54 12687 Raw data (stat): 12687 (minisat+) R 12686 5897 5896 0 -1 0 5783 0 0 0 6981 18 0 0 25 0 1 0 422943196 27074560 5761 4294967295 134512640 134672761 3221224560 3221223776 134561997 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 6610 5761 603 41 0 6569 0 vsize: 26440 [startup+80.0053 s] Raw data (loadavg): 0.98 0.96 0.91 2/54 12687 Raw data (stat): 12687 (minisat+) R 12686 5897 5896 0 -1 0 5783 0 0 0 7980 18 0 0 25 0 1 0 422943196 27074560 5761 4294967295 134512640 134672761 3221224560 3221223764 134561964 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 6610 5761 603 41 0 6569 0 vsize: 26440 [startup+90.0049 s] Raw data (loadavg): 0.98 0.96 0.91 2/54 12687 Raw data (stat): 12687 (minisat+) R 12686 5897 5896 0 -1 0 5783 0 0 0 8981 18 0 0 25 0 1 0 422943196 27074560 5761 4294967295 134512640 134672761 3221224560 3221223728 134561372 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 6610 5761 603 41 0 6569 0 vsize: 26440 [startup+100.005 s] Raw data (loadavg): 0.98 0.96 0.91 2/54 12687 Raw data (stat): 12687 (minisat+) R 12686 5897 5896 0 -1 0 5799 0 0 0 9980 18 0 0 25 0 1 0 422943196 27140096 5777 4294967295 134512640 134672761 3221224560 3221223732 134556596 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 6626 5777 603 41 0 6585 0 vsize: 26504 [startup+110.006 s] Raw data (loadavg): 0.98 0.96 0.91 2/54 12687 Raw data (stat): 12687 (minisat+) R 12686 5897 5896 0 -1 0 5824 0 0 0 10980 19 0 0 25 0 1 0 422943196 27332608 5802 4294967295 134512640 134672761 3221224560 3221223728 134561378 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 6673 5802 603 41 0 6632 0 vsize: 26692 [startup+120.006 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 12687 Raw data (stat): 12687 (minisat+) R 12686 5897 5896 0 -1 0 5994 0 0 0 11979 20 0 0 25 0 1 0 422943196 27930624 5972 4294967295 134512640 134672761 3221224560 3221223776 134561993 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 6819 5972 603 41 0 6778 0 vsize: 27276 [startup+130.007 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 12687 Raw data (stat): 12687 (minisat+) R 12686 5897 5896 0 -1 0 6247 0 0 0 12978 20 0 0 25 0 1 0 422943196 29110272 6225 4294967295 134512640 134672761 3221224560 3221223684 134565998 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 7107 6225 603 41 0 7066 0 vsize: 28428 [startup+140.015 s] Raw data (loadavg): 0.99 0.97 0.91 2/56 12727 Raw data (stat): 12687 (minisat+) R 12686 5897 5896 0 -1 0 6692 0 0 0 13973 26 0 0 25 0 1 0 422943196 30818304 6670 4294967295 134512640 134672761 3221224560 3221223744 134558687 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 7524 6670 603 41 0 7483 0 vsize: 30096 [startup+150.016 s] Raw data (loadavg): 1.14 1.00 0.92 2/54 12740 Raw data (stat): 12687 (minisat+) R 12686 5897 5896 0 -1 0 7184 0 0 0 14970 29 0 0 25 0 1 0 422943196 32833536 7162 4294967295 134512640 134672761 3221224560 3221223196 134545055 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 8016 7162 603 41 0 7975 0 vsize: 32064 [startup+160.016 s] Raw data (loadavg): 1.12 1.00 0.92 2/54 12740 Raw data (stat): 12687 (minisat+) R 12686 5897 5896 0 -1 0 7586 0 0 0 15969 30 0 0 25 0 1 0 422943196 34496512 7564 4294967295 134512640 134672761 3221224560 3221223744 134559553 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 8422 7564 603 41 0 8381 0 vsize: 33688 [startup+170.017 s] Raw data (loadavg): 1.17 1.02 0.93 2/54 12740 Raw data (stat): 12687 (minisat+) R 12686 5897 5896 0 -1 0 8143 0 0 0 16968 31 0 0 25 0 1 0 422943196 36909056 8121 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 9011 8121 603 41 0 8970 0 vsize: 36044 [startup+180.016 s] Raw data (loadavg): 1.14 1.02 0.93 2/54 12740 Raw data (stat): 12687 (minisat+) R 12686 5897 5896 0 -1 0 8663 0 0 0 17966 33 0 0 25 0 1 0 422943196 39055360 8641 4294967295 134512640 134672761 3221224560 3221223728 134561005 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 9535 8641 603 41 0 9494 0 vsize: 38140 [startup+190.017 s] Raw data (loadavg): 1.12 1.01 0.93 2/54 12740 Raw data (stat): 12687 (minisat+) R 12686 5897 5896 0 -1 0 9256 0 0 0 18964 35 0 0 25 0 1 0 422943196 41472000 9234 4294967295 134512640 134672761 3221224560 3221223744 134558899 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 10125 9234 603 41 0 10084 0 vsize: 40500 [startup+200.017 s] Raw data (loadavg): 1.10 1.01 0.93 2/54 12740 Raw data (stat): 12687 (minisat+) R 12686 5897 5896 0 -1 0 9816 0 0 0 19963 37 0 0 25 0 1 0 422943196 43745280 9794 4294967295 134512640 134672761 3221224560 3221223516 1075350517 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 10680 9794 603 41 0 10639 0 vsize: 42720 [startup+210.017 s] Raw data (loadavg): 1.09 1.01 0.93 2/54 12740 Raw data (stat): 12687 (minisat+) R 12686 5897 5896 0 -1 0 10412 0 0 0 20961 39 0 0 25 0 1 0 422943196 46149632 10390 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 11267 10390 603 41 0 11226 0 vsize: 45068 [startup+220.018 s] Raw data (loadavg): 1.07 1.01 0.93 2/54 12742 Raw data (stat): 12687 (minisat+) R 12686 5897 5896 0 -1 0 10794 0 0 0 21960 40 0 0 25 0 1 0 422943196 47702016 10772 4294967295 134512640 134672761 3221224560 3221223760 134557809 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 11646 10772 603 41 0 11605 0 vsize: 46584 [startup+230.019 s] Raw data (loadavg): 1.06 1.01 0.93 2/54 12742 Raw data (stat): 12687 (minisat+) R 12686 5897 5896 0 -1 0 11182 0 0 0 22959 41 0 0 25 0 1 0 422943196 49299456 11160 4294967295 134512640 134672761 3221224560 3221223684 134566037 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 12036 11160 603 41 0 11995 0 vsize: 48144 [startup+240.018 s] Raw data (loadavg): 1.05 1.01 0.93 2/54 12742 Raw data (stat): 12687 (minisat+) R 12686 5897 5896 0 -1 0 11579 0 0 0 23958 42 0 0 25 0 1 0 422943196 50896896 11557 4294967295 134512640 134672761 3221224560 3221223728 134561382 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 12426 11557 603 41 0 12385 0 vsize: 49704 [startup+250.019 s] Raw data (loadavg): 1.04 1.01 0.93 2/54 12742 Raw data (stat): 12687 (minisat+) R 12686 5897 5896 0 -1 0 11942 0 0 0 24957 43 0 0 25 0 1 0 422943196 52359168 11920 4294967295 134512640 134672761 3221224560 3221223664 134560196 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 12783 11920 603 41 0 12742 0 vsize: 51132 [startup+260.019 s] Raw data (loadavg): 1.04 1.01 0.93 2/54 12742 Raw data (stat): 12687 (minisat+) R 12686 5897 5896 0 -1 0 12342 0 0 0 25956 44 0 0 25 0 1 0 422943196 53960704 12320 4294967295 134512640 134672761 3221224560 3221223744 134559367 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 13174 12320 603 41 0 13133 0 vsize: 52696 [startup+270.019 s] Raw data (loadavg): 1.03 1.01 0.93 2/54 12742 Raw data (stat): 12687 (minisat+) R 12686 5897 5896 0 -1 0 12670 0 0 0 26956 45 0 0 25 0 1 0 422943196 55558144 12648 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 13564 12648 603 41 0 13523 0 vsize: 54256 [startup+280.019 s] Raw data (loadavg): 1.02 1.01 0.93 2/54 12742 Raw data (stat): 12687 (minisat+) R 12686 5897 5896 0 -1 0 12987 0 0 0 27955 45 0 0 25 0 1 0 422943196 56872960 12965 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 13885 12965 603 41 0 13844 0 vsize: 55540 [startup+290.02 s] Raw data (loadavg): 1.02 1.00 0.93 2/54 12742 Raw data (stat): 12687 (minisat+) R 12686 5897 5896 0 -1 0 13304 0 0 0 28954 47 0 0 25 0 1 0 422943196 58068992 13282 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 14177 13282 603 41 0 14136 0 vsize: 56708 [startup+300.02 s] Raw data (loadavg): 1.02 1.00 0.93 2/54 12742 Raw data (stat): 12687 (minisat+) R 12686 5897 5896 0 -1 0 13636 0 0 0 29954 48 0 0 25 0 1 0 422943196 59539456 13614 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 14536 13614 603 41 0 14495 0 vsize: 58144 [startup+310.02 s] Raw data (loadavg): 1.01 1.00 0.93 2/54 12742 Raw data (stat): 12687 (minisat+) R 12686 5897 5896 0 -1 0 13816 0 0 0 30953 48 0 0 25 0 1 0 422943196 60162048 13794 4294967295 134512640 134672761 3221224560 3221223684 134566109 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 14688 13794 603 41 0 14647 0 vsize: 58752 [startup+320.02 s] Raw data (loadavg): 1.01 1.00 0.93 2/54 12742 Raw data (stat): 12687 (minisat+) R 12686 5897 5896 0 -1 0 13816 0 0 0 31953 48 0 0 25 0 1 0 422943196 60162048 13794 4294967295 134512640 134672761 3221224560 3221223760 134557836 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 14688 13794 603 41 0 14647 0 vsize: 58752 [startup+330.02 s] Raw data (loadavg): 1.01 1.00 0.93 2/54 12742 Raw data (stat): 12687 (minisat+) R 12686 5897 5896 0 -1 0 13816 0 0 0 32954 48 0 0 25 0 1 0 422943196 60162048 13794 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 14688 13794 603 41 0 14647 0 vsize: 58752 [startup+340.021 s] Raw data (loadavg): 1.01 1.00 0.93 2/54 12742 Raw data (stat): 12687 (minisat+) R 12686 5897 5896 0 -1 0 13816 0 0 0 33954 48 0 0 25 0 1 0 422943196 60162048 13794 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 14688 13794 603 41 0 14647 0 vsize: 58752 [startup+350.021 s] Raw data (loadavg): 1.01 1.00 0.93 2/54 12742 Raw data (stat): 12687 (minisat+) R 12686 5897 5896 0 -1 0 13816 0 0 0 34954 48 0 0 25 0 1 0 422943196 60162048 13794 4294967295 134512640 134672761 3221224560 3221223728 134561198 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 14688 13794 603 41 0 14647 0 vsize: 58752 [startup+360.021 s] Raw data (loadavg): 1.00 1.00 0.93 2/54 12742 Raw data (stat): 12687 (minisat+) R 12686 5897 5896 0 -1 0 13816 0 0 0 35954 48 0 0 25 0 1 0 422943196 60162048 13794 4294967295 134512640 134672761 3221224560 3221223728 134561011 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 14688 13794 603 41 0 14647 0 vsize: 58752 [startup+370.021 s] Raw data (loadavg): 1.00 1.00 0.93 2/54 12742 Raw data (stat): 12687 (minisat+) R 12686 5897 5896 0 -1 0 13816 0 0 0 36954 48 0 0 25 0 1 0 422943196 60162048 13794 4294967295 134512640 134672761 3221224560 3221223664 134560196 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 14688 13794 603 41 0 14647 0 vsize: 58752 [startup+380.02 s] Raw data (loadavg): 1.00 1.00 0.93 2/54 12742 Raw data (stat): 12687 (minisat+) R 12686 5897 5896 0 -1 0 13816 0 0 0 37954 48 0 0 25 0 1 0 422943196 60162048 13794 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 14688 13794 603 41 0 14647 0 vsize: 58752 [startup+390.02 s] Raw data (loadavg): 1.00 1.00 0.93 2/54 12742 Raw data (stat): 12687 (minisat+) R 12686 5897 5896 0 -1 0 13816 0 0 0 38955 48 0 0 25 0 1 0 422943196 60162048 13794 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 14688 13794 603 41 0 14647 0 vsize: 58752 [startup+400.022 s] Raw data (loadavg): 1.00 1.00 0.93 2/54 12742 Raw data (stat): 12687 (minisat+) R 12686 5897 5896 0 -1 0 13816 0 0 0 39955 48 0 0 25 0 1 0 422943196 60162048 13794 4294967295 134512640 134672761 3221224560 3221223744 134559405 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 14688 13794 603 41 0 14647 0 vsize: 58752 [startup+410.021 s] Raw data (loadavg): 1.00 1.00 0.93 2/54 12742 Raw data (stat): 12687 (minisat+) R 12686 5897 5896 0 -1 0 13816 0 0 0 40955 48 0 0 25 0 1 0 422943196 60162048 13794 4294967295 134512640 134672761 3221224560 3221223728 134560980 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 14688 13794 603 41 0 14647 0 vsize: 58752 [startup+420.021 s] Raw data (loadavg): 1.00 1.00 0.93 2/54 12742 Raw data (stat): 12687 (minisat+) R 12686 5897 5896 0 -1 0 13816 0 0 0 41955 48 0 0 25 0 1 0 422943196 60162048 13794 4294967295 134512640 134672761 3221224560 3221223744 134559031 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 14688 13794 603 41 0 14647 0 vsize: 58752 [startup+430.021 s] Raw data (loadavg): 1.00 1.00 0.93 2/54 12742 Raw data (stat): 12687 (minisat+) R 12686 5897 5896 0 -1 0 13816 0 0 0 42955 48 0 0 25 0 1 0 422943196 60162048 13794 4294967295 134512640 134672761 3221224560 3221223728 134561001 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 14688 13794 603 41 0 14647 0 vsize: 58752 [startup+440.021 s] Raw data (loadavg): 1.00 1.00 0.93 2/54 12742 Raw data (stat): 12687 (minisat+) R 12686 5897 5896 0 -1 0 13816 0 0 0 43955 48 0 0 25 0 1 0 422943196 60162048 13794 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 14688 13794 603 41 0 14647 0 vsize: 58752 [startup+450.02 s] Raw data (loadavg): 1.00 1.00 0.93 2/54 12742 Raw data (stat): 12687 (minisat+) R 12686 5897 5896 0 -1 0 13816 0 0 0 44955 48 0 0 25 0 1 0 422943196 60162048 13794 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 14688 13794 603 41 0 14647 0 vsize: 58752 [startup+460.021 s] Raw data (loadavg): 1.00 1.00 0.93 2/54 12742 Raw data (stat): 12687 (minisat+) R 12686 5897 5896 0 -1 0 14191 0 0 0 45955 49 0 0 25 0 1 0 422943196 61767680 14169 4294967295 134512640 134672761 3221224560 3221223728 134561385 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 15080 14169 603 41 0 15039 0 vsize: 60320 [startup+470.021 s] Raw data (loadavg): 1.00 1.00 0.93 2/54 12742 Raw data (stat): 12687 (minisat+) R 12686 5897 5896 0 -1 0 14616 0 0 0 46954 50 0 0 25 0 1 0 422943196 63504384 14594 4294967295 134512640 134672761 3221224560 3221223728 134560999 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 15504 14594 603 41 0 15463 0 vsize: 62016 [startup+480.021 s] Raw data (loadavg): 1.00 1.00 0.93 2/54 12742 Raw data (stat): 12687 (minisat+) R 12686 5897 5896 0 -1 0 14973 0 0 0 47953 51 0 0 25 0 1 0 422943196 64983040 14951 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 15865 14951 603 41 0 15824 0 vsize: 63460 [startup+490.021 s] Raw data (loadavg): 1.00 1.00 0.93 2/54 12742 Raw data (stat): 12687 (minisat+) R 12686 5897 5896 0 -1 0 15379 0 0 0 48952 52 0 0 25 0 1 0 422943196 66576384 15357 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 16254 15357 603 41 0 16213 0 vsize: 65016 [startup+500.022 s] Raw data (loadavg): 1.00 1.00 0.93 2/54 12742 Raw data (stat): 12687 (minisat+) R 12686 5897 5896 0 -1 0 15758 0 0 0 49951 53 0 0 25 0 1 0 422943196 68169728 15736 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 16643 15736 603 41 0 16602 0 vsize: 66572 [startup+510.022 s] Raw data (loadavg): 1.08 1.02 0.93 2/54 12744 Raw data (stat): 12687 (minisat+) R 12686 5897 5896 0 -1 0 16138 0 0 0 50950 54 0 0 25 0 1 0 422943196 69640192 16116 4294967295 134512640 134672761 3221224560 3221223744 134559332 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 17002 16116 603 41 0 16961 0 vsize: 68008 [startup+520.022 s] Raw data (loadavg): 1.07 1.02 0.93 2/54 12744 Raw data (stat): 12687 (minisat+) R 12686 5897 5896 0 -1 0 16497 0 0 0 51949 55 0 0 25 0 1 0 422943196 71094272 16475 4294967295 134512640 134672761 3221224560 3221223728 134560999 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 17357 16475 603 41 0 17316 0 vsize: 69428 [startup+530.022 s] Raw data (loadavg): 1.06 1.01 0.93 2/54 12744 Raw data (stat): 12687 (minisat+) R 12686 5897 5896 0 -1 0 16833 0 0 0 52949 56 0 0 25 0 1 0 422943196 72552448 16811 4294967295 134512640 134672761 3221224560 3221223728 134560940 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 17713 16811 603 41 0 17672 0 vsize: 70852 [startup+540.022 s] Raw data (loadavg): 1.05 1.01 0.93 2/54 12744 Raw data (stat): 12687 (minisat+) R 12686 5897 5896 0 -1 0 17127 0 0 0 53948 57 0 0 25 0 1 0 422943196 73752576 17105 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 18006 17105 603 41 0 17965 0 vsize: 72024 [startup+550.022 s] Raw data (loadavg): 1.04 1.01 0.93 2/54 12744 Raw data (stat): 12687 (minisat+) R 12686 5897 5896 0 -1 0 17452 0 0 0 54948 57 0 0 25 0 1 0 422943196 74952704 17430 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 18299 17430 603 41 0 18258 0 vsize: 73196 [startup+560.022 s] Raw data (loadavg): 1.03 1.01 0.93 2/54 12744 Raw data (stat): 12687 (minisat+) R 12686 5897 5896 0 -1 0 17688 0 0 0 55947 58 0 0 25 0 1 0 422943196 76021760 17666 4294967295 134512640 134672761 3221224560 3221223664 134560198 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 18560 17666 603 41 0 18519 0 vsize: 74240 [startup+570.023 s] Raw data (loadavg): 1.03 1.01 0.93 2/54 12744 Raw data (stat): 12687 (minisat+) R 12686 5897 5896 0 -1 0 17942 0 0 0 56947 58 0 0 25 0 1 0 422943196 76955648 17920 4294967295 134512640 134672761 3221224560 3221223728 134561167 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 18788 17920 603 41 0 18747 0 vsize: 75152 [startup+580.023 s] Raw data (loadavg): 1.02 1.01 0.93 2/54 12744 Raw data (stat): 12687 (minisat+) R 12686 5897 5896 0 -1 0 18204 0 0 0 57946 59 0 0 25 0 1 0 422943196 78024704 18182 4294967295 134512640 134672761 3221224560 3221223732 134556688 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 19049 18182 603 41 0 19008 0 vsize: 76196 [startup+590.022 s] Raw data (loadavg): 1.02 1.01 0.93 2/54 12744 Raw data (stat): 12687 (minisat+) R 12686 5897 5896 0 -1 0 18473 0 0 0 58945 60 0 0 25 0 1 0 422943196 79097856 18451 4294967295 134512640 134672761 3221224560 3221223696 134560606 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 19311 18451 603 41 0 19270 0 vsize: 77244 [startup+600.022 s] Raw data (loadavg): 1.02 1.01 0.93 2/54 12744 Raw data (stat): 12687 (minisat+) R 12686 5897 5896 0 -1 0 18788 0 0 0 59945 61 0 0 25 0 1 0 422943196 80433152 18766 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 19637 18766 603 41 0 19596 0 vsize: 78548 [startup+610.022 s] Raw data (loadavg): 1.01 1.01 0.93 2/54 12744 Raw data (stat): 12687 (minisat+) R 12686 5897 5896 0 -1 0 19044 0 0 0 60944 62 0 0 25 0 1 0 422943196 81498112 19022 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 19897 19022 603 41 0 19856 0 vsize: 79588 [startup+620.023 s] Raw data (loadavg): 1.01 1.01 0.93 2/54 12744 Raw data (stat): 12687 (minisat+) R 12686 5897 5896 0 -1 0 19306 0 0 0 61944 62 0 0 25 0 1 0 422943196 82558976 19284 4294967295 134512640 134672761 3221224560 3221223728 134561118 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 20156 19284 603 41 0 20115 0 vsize: 80624 [startup+630.023 s] Raw data (loadavg): 1.01 1.00 0.93 2/54 12744 Raw data (stat): 12687 (minisat+) R 12686 5897 5896 0 -1 0 19564 0 0 0 62943 63 0 0 25 0 1 0 422943196 83615744 19542 4294967295 134512640 134672761 3221224560 3221223744 134559405 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 20414 19542 603 41 0 20373 0 vsize: 81656 [startup+640.023 s] Raw data (loadavg): 1.01 1.00 0.93 2/54 12744 Raw data (stat): 12687 (minisat+) R 12686 5897 5896 0 -1 0 19839 0 0 0 63943 63 0 0 25 0 1 0 422943196 84684800 19817 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 20675 19817 603 41 0 20634 0 vsize: 82700 [startup+650.024 s] Raw data (loadavg): 1.00 1.00 0.93 2/54 12744 Raw data (stat): 12687 (minisat+) R 12686 5897 5896 0 -1 0 20108 0 0 0 64942 64 0 0 25 0 1 0 422943196 85753856 20086 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 20936 20086 603 41 0 20895 0 vsize: 83744 [startup+660.023 s] Raw data (loadavg): 1.00 1.00 0.93 2/54 12744 Raw data (stat): 12687 (minisat+) R 12686 5897 5896 0 -1 0 20399 0 0 0 65941 65 0 0 25 0 1 0 422943196 87482368 20377 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 21358 20377 603 41 0 21317 0 vsize: 85432 [startup+670.024 s] Raw data (loadavg): 1.00 1.00 0.93 2/54 12744 Raw data (stat): 12687 (minisat+) R 12686 5897 5896 0 -1 0 20660 0 0 0 66941 66 0 0 25 0 1 0 422943196 88543232 20638 4294967295 134512640 134672761 3221224560 3221223704 134560553 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 21617 20638 603 41 0 21576 0 vsize: 86468 [startup+680.024 s] Raw data (loadavg): 1.00 1.00 0.93 2/54 12744 Raw data (stat): 12687 (minisat+) R 12686 5897 5896 0 -1 0 20911 0 0 0 67940 67 0 0 25 0 1 0 422943196 89608192 20889 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 21877 20889 603 41 0 21836 0 vsize: 87508 [startup+690.024 s] Raw data (loadavg): 1.00 1.00 0.93 2/54 12744 Raw data (stat): 12687 (minisat+) R 12686 5897 5896 0 -1 0 21187 0 0 0 68940 67 0 0 25 0 1 0 422943196 90673152 21165 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 22137 21165 603 41 0 22096 0 vsize: 88548 [startup+700.024 s] Raw data (loadavg): 1.00 1.00 0.93 2/54 12744 Raw data (stat): 12687 (minisat+) R 12686 5897 5896 0 -1 0 21453 0 0 0 69939 68 0 0 25 0 1 0 422943196 91742208 21431 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 22398 21431 603 41 0 22357 0 vsize: 89592 [startup+710.025 s] Raw data (loadavg): 1.00 1.00 0.93 2/54 12744 Raw data (stat): 12687 (minisat+) R 12686 5897 5896 0 -1 0 21747 0 0 0 70939 69 0 0 25 0 1 0 422943196 92930048 21725 4294967295 134512640 134672761 3221224560 3221223744 134559405 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 22688 21725 603 41 0 22647 0 vsize: 90752 [startup+720.024 s] Raw data (loadavg): 1.00 1.00 0.93 2/54 12744 Raw data (stat): 12687 (minisat+) R 12686 5897 5896 0 -1 0 21986 0 0 0 71938 70 0 0 25 0 1 0 422943196 94007296 21964 4294967295 134512640 134672761 3221224560 3221223760 134557895 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 22951 21964 603 41 0 22910 0 vsize: 91804 [startup+730.025 s] Raw data (loadavg): 1.00 1.00 0.93 2/54 12744 Raw data (stat): 12687 (minisat+) R 12686 5897 5896 0 -1 0 22227 0 0 0 72938 70 0 0 25 0 1 0 422943196 94941184 22205 4294967295 134512640 134672761 3221224560 3221223760 134557911 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 23179 22205 603 41 0 23138 0 vsize: 92716 [startup+740.025 s] Raw data (loadavg): 1.00 1.00 0.93 2/54 12744 Raw data (stat): 12687 (minisat+) R 12686 5897 5896 0 -1 0 22460 0 0 0 73936 72 0 0 25 0 1 0 422943196 95883264 22438 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 23409 22438 603 41 0 23368 0 vsize: 93636 [startup+750.025 s] Raw data (loadavg): 1.00 1.00 0.93 2/54 12744 Raw data (stat): 12687 (minisat+) R 12686 5897 5896 0 -1 0 22718 0 0 0 74935 73 0 0 25 0 1 0 422943196 96944128 22696 4294967295 134512640 134672761 3221224560 3221223728 134561001 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 23668 22696 603 41 0 23627 0 vsize: 94672 [startup+760.025 s] Raw data (loadavg): 1.00 1.00 0.93 2/54 12744 Raw data (stat): 12687 (minisat+) R 12686 5897 5896 0 -1 0 22949 0 0 0 75934 73 0 0 25 0 1 0 422943196 97873920 22927 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 23895 22927 603 41 0 23854 0 vsize: 95580 [startup+770.026 s] Raw data (loadavg): 1.00 1.00 0.93 2/54 12744 Raw data (stat): 12687 (minisat+) R 12686 5897 5896 0 -1 0 23129 0 0 0 76934 74 0 0 25 0 1 0 422943196 98660352 23107 4294967295 134512640 134672761 3221224560 3221223728 134560871 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 24087 23107 603 41 0 24046 0 vsize: 96348 [startup+780.027 s] Raw data (loadavg): 1.00 1.00 0.93 2/54 12744 Raw data (stat): 12687 (minisat+) R 12686 5897 5896 0 -1 0 23375 0 0 0 77934 74 0 0 25 0 1 0 422943196 99590144 23353 4294967295 134512640 134672761 3221224560 3221223728 134561190 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 24314 23353 603 41 0 24273 0 vsize: 97256 [startup+790.027 s] Raw data (loadavg): 1.00 1.00 0.93 2/54 12744 Raw data (stat): 12687 (minisat+) R 12686 5897 5896 0 -1 0 23624 0 0 0 78933 75 0 0 25 0 1 0 422943196 100655104 23602 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 24574 23602 603 41 0 24533 0 vsize: 98296 [startup+800.027 s] Raw data (loadavg): 1.00 1.00 0.93 2/54 12744 Raw data (stat): 12687 (minisat+) R 12686 5897 5896 0 -1 0 23848 0 0 0 79933 76 0 0 25 0 1 0 422943196 101453824 23826 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 24769 23826 603 41 0 24728 0 vsize: 99076 [startup+810.027 s] Raw data (loadavg): 1.00 1.00 0.93 2/54 12744 Raw data (stat): 12687 (minisat+) R 12686 5897 5896 0 -1 0 24038 0 0 0 80932 76 0 0 25 0 1 0 422943196 102256640 24016 4294967295 134512640 134672761 3221224560 3221223728 134561198 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 24965 24016 603 41 0 24924 0 vsize: 99860 [startup+820.028 s] Raw data (loadavg): 1.00 1.00 0.93 2/54 12744 Raw data (stat): 12687 (minisat+) R 12686 5897 5896 0 -1 0 24221 0 0 0 81932 77 0 0 25 0 1 0 422943196 103051264 24199 4294967295 134512640 134672761 3221224560 3221223728 134561198 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 25159 24199 603 41 0 25118 0 vsize: 100636 [startup+830.028 s] Raw data (loadavg): 1.00 1.00 0.93 2/54 12744 Raw data (stat): 12687 (minisat+) R 12686 5897 5896 0 -1 0 24393 0 0 0 82931 78 0 0 25 0 1 0 422943196 103714816 24371 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 25321 24371 603 41 0 25280 0 vsize: 101284 [startup+840.028 s] Raw data (loadavg): 1.00 1.00 0.93 2/54 12744 Raw data (stat): 12687 (minisat+) R 12686 5897 5896 0 -1 0 24566 0 0 0 83931 78 0 0 25 0 1 0 422943196 104378368 24544 4294967295 134512640 134672761 3221224560 3221223728 134560980 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 25483 24544 603 41 0 25442 0 vsize: 101932 [startup+850.029 s] Raw data (loadavg): 1.00 1.00 0.93 2/54 12744 Raw data (stat): 12687 (minisat+) R 12686 5897 5896 0 -1 0 24753 0 0 0 84931 79 0 0 25 0 1 0 422943196 105172992 24731 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 25677 24731 603 41 0 25636 0 vsize: 102708 [startup+860.029 s] Raw data (loadavg): 1.00 1.00 0.93 2/54 12744 Raw data (stat): 12687 (minisat+) R 12686 5897 5896 0 -1 0 24944 0 0 0 85930 79 0 0 25 0 1 0 422943196 105971712 24922 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 25872 24922 603 41 0 25831 0 vsize: 103488 [startup+870.029 s] Raw data (loadavg): 1.00 1.00 0.93 2/54 12744 Raw data (stat): 12687 (minisat+) R 12686 5897 5896 0 -1 0 25136 0 0 0 86930 80 0 0 25 0 1 0 422943196 106762240 25114 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 26065 25114 603 41 0 26024 0 vsize: 104260 [startup+880.031 s] Raw data (loadavg): 1.00 1.00 0.93 2/54 12744 Raw data (stat): 12687 (minisat+) R 12686 5897 5896 0 -1 0 25320 0 0 0 87929 80 0 0 25 0 1 0 422943196 107438080 25298 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 26230 25298 603 41 0 26189 0 vsize: 104920 [startup+890.03 s] Raw data (loadavg): 1.00 1.00 0.93 2/54 12744 Raw data (stat): 12687 (minisat+) R 12686 5897 5896 0 -1 0 25517 0 0 0 88929 81 0 0 25 0 1 0 422943196 108363776 25495 4294967295 134512640 134672761 3221224560 3221223724 134561235 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 26456 25495 603 41 0 26415 0 vsize: 105824 [startup+900.031 s] Raw data (loadavg): 1.00 1.00 0.93 2/54 12744 Raw data (stat): 12687 (minisat+) R 12686 5897 5896 0 -1 0 25711 0 0 0 89929 81 0 0 25 0 1 0 422943196 109027328 25689 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 26618 25689 603 41 0 26577 0 vsize: 106472 [startup+910.031 s] Raw data (loadavg): 1.00 1.00 0.93 2/54 12744 Raw data (stat): 12687 (minisat+) R 12686 5897 5896 0 -1 0 25882 0 0 0 90929 81 0 0 25 0 1 0 422943196 109821952 25860 4294967295 134512640 134672761 3221224560 3221223696 134560588 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 26812 25860 603 41 0 26771 0 vsize: 107248 [startup+920.032 s] Raw data (loadavg): 1.00 1.00 0.93 2/54 12744 Raw data (stat): 12687 (minisat+) R 12686 5897 5896 0 -1 0 26064 0 0 0 91929 82 0 0 25 0 1 0 422943196 110489600 26042 4294967295 134512640 134672761 3221224560 3221223728 134560906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 26975 26042 603 41 0 26934 0 vsize: 107900 [startup+930.031 s] Raw data (loadavg): 1.00 1.00 0.93 2/54 12744 Raw data (stat): 12687 (minisat+) R 12686 5897 5896 0 -1 0 26234 0 0 0 92929 82 0 0 25 0 1 0 422943196 111149056 26212 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 27136 26212 603 41 0 27095 0 vsize: 108544 [startup+940.032 s] Raw data (loadavg): 1.00 1.00 0.93 2/54 12744 Raw data (stat): 12687 (minisat+) R 12686 5897 5896 0 -1 0 26406 0 0 0 93928 83 0 0 25 0 1 0 422943196 111968256 26384 4294967295 134512640 134672761 3221224560 3221223664 134560399 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 27336 26384 603 41 0 27295 0 vsize: 109344 [startup+950.033 s] Raw data (loadavg): 1.00 1.00 0.93 2/54 12744 Raw data (stat): 12687 (minisat+) R 12686 5897 5896 0 -1 0 26559 0 0 0 94928 83 0 0 25 0 1 0 422943196 112627712 26537 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 27497 26537 603 41 0 27456 0 vsize: 109988 [startup+960.032 s] Raw data (loadavg): 1.00 1.00 0.93 2/54 12744 Raw data (stat): 12687 (minisat+) R 12686 5897 5896 0 -1 0 26688 0 0 0 95928 83 0 0 25 0 1 0 422943196 113156096 26666 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 27626 26666 603 41 0 27585 0 vsize: 110504 [startup+970.032 s] Raw data (loadavg): 1.00 1.00 0.93 2/54 12744 Raw data (stat): 12687 (minisat+) R 12686 5897 5896 0 -1 0 26832 0 0 0 96928 83 0 0 25 0 1 0 422943196 113680384 26810 4294967295 134512640 134672761 3221224560 3221223760 134557919 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 27754 26810 603 41 0 27713 0 vsize: 111016 [startup+980.032 s] Raw data (loadavg): 1.00 1.00 0.93 2/54 12744 Raw data (stat): 12687 (minisat+) R 12686 5897 5896 0 -1 0 26974 0 0 0 97928 84 0 0 25 0 1 0 422943196 114335744 26952 4294967295 134512640 134672761 3221224560 3221223744 134559354 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 27914 26952 603 41 0 27873 0 vsize: 111656 [startup+990.032 s] Raw data (loadavg): 1.00 1.00 0.93 2/54 12744 Raw data (stat): 12687 (minisat+) R 12686 5897 5896 0 -1 0 27121 0 0 0 98928 84 0 0 25 0 1 0 422943196 114860032 27099 4294967295 134512640 134672761 3221224560 3221223728 134561139 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 28042 27099 603 41 0 28001 0 vsize: 112168 [startup+1000.03 s] Raw data (loadavg): 1.00 1.00 0.93 2/54 12744 Raw data (stat): 12687 (minisat+) R 12686 5897 5896 0 -1 0 27266 0 0 0 99928 84 0 0 25 0 1 0 422943196 115523584 27244 4294967295 134512640 134672761 3221224560 3221223760 134557842 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 28204 27244 603 41 0 28163 0 vsize: 112816 [startup+1010.03 s] Raw data (loadavg): 1.00 1.00 0.93 2/54 12744 Raw data (stat): 12687 (minisat+) R 12686 5897 5896 0 -1 0 27406 0 0 0 100927 85 0 0 25 0 1 0 422943196 116051968 27384 4294967295 134512640 134672761 3221224560 3221223728 134561151 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 28333 27384 603 41 0 28292 0 vsize: 113332 [startup+1020.03 s] Raw data (loadavg): 1.00 1.00 0.93 2/54 12744 Raw data (stat): 12687 (minisat+) R 12686 5897 5896 0 -1 0 27542 0 0 0 101928 85 0 0 25 0 1 0 422943196 116580352 27520 4294967295 134512640 134672761 3221224560 3221223744 134558687 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 28462 27520 603 41 0 28421 0 vsize: 113848 [startup+1030.03 s] Raw data (loadavg): 1.00 1.00 0.93 2/54 12744 Raw data (stat): 12687 (minisat+) R 12686 5897 5896 0 -1 0 27682 0 0 0 102927 85 0 0 25 0 1 0 422943196 117104640 27660 4294967295 134512640 134672761 3221224560 3221223648 134565852 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 28590 27660 603 41 0 28549 0 vsize: 114360 [startup+1040.03 s] Raw data (loadavg): 1.00 1.00 0.93 2/54 12744 Raw data (stat): 12687 (minisat+) R 12686 5897 5896 0 -1 0 27682 0 0 0 103928 85 0 0 25 0 1 0 422943196 117104640 27660 4294967295 134512640 134672761 3221224560 3221223696 134560677 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 28590 27660 603 41 0 28549 0 vsize: 114360 [startup+1050.03 s] Raw data (loadavg): 1.00 1.00 0.93 2/54 12744 Raw data (stat): 12687 (minisat+) R 12686 5897 5896 0 -1 0 27682 0 0 0 104928 85 0 0 25 0 1 0 422943196 117104640 27660 4294967295 134512640 134672761 3221224560 3221223728 134561375 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 28590 27660 603 41 0 28549 0 vsize: 114360 [startup+1060.03 s] Raw data (loadavg): 1.00 1.00 0.93 2/54 12744 Raw data (stat): 12687 (minisat+) R 12686 5897 5896 0 -1 0 27682 0 0 0 105928 85 0 0 25 0 1 0 422943196 117104640 27660 4294967295 134512640 134672761 3221224560 3221223728 134561151 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 28590 27660 603 41 0 28549 0 vsize: 114360 [startup+1070.03 s] Raw data (loadavg): 1.00 1.00 0.93 2/54 12744 Raw data (stat): 12687 (minisat+) R 12686 5897 5896 0 -1 0 27682 0 0 0 106927 85 0 0 25 0 1 0 422943196 117104640 27660 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 28590 27660 603 41 0 28549 0 vsize: 114360 [startup+1080.03 s] Raw data (loadavg): 1.00 1.00 0.93 2/54 12744 Raw data (stat): 12687 (minisat+) R 12686 5897 5896 0 -1 0 27682 0 0 0 107928 85 0 0 25 0 1 0 422943196 117104640 27660 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 28590 27660 603 41 0 28549 0 vsize: 114360 [startup+1090.03 s] Raw data (loadavg): 1.00 1.00 0.93 2/54 12744 Raw data (stat): 12687 (minisat+) R 12686 5897 5896 0 -1 0 27682 0 0 0 108928 85 0 0 25 0 1 0 422943196 117104640 27660 4294967295 134512640 134672761 3221224560 3221223760 134557830 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 28590 27660 603 41 0 28549 0 vsize: 114360 [startup+1100.04 s] Raw data (loadavg): 1.00 1.00 0.93 2/54 12744 Raw data (stat): 12687 (minisat+) R 12686 5897 5896 0 -1 0 27682 0 0 0 109928 85 0 0 25 0 1 0 422943196 117104640 27660 4294967295 134512640 134672761 3221224560 3221223744 134559161 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 28590 27660 603 41 0 28549 0 vsize: 114360 [startup+1110.03 s] Raw data (loadavg): 1.00 1.00 0.93 2/54 12744 Raw data (stat): 12687 (minisat+) R 12686 5897 5896 0 -1 0 27682 0 0 0 110928 85 0 0 25 0 1 0 422943196 117104640 27660 4294967295 134512640 134672761 3221224560 3221223728 134561229 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 28590 27660 603 41 0 28549 0 vsize: 114360 [startup+1120.04 s] Raw data (loadavg): 1.00 1.00 0.93 2/54 12744 Raw data (stat): 12687 (minisat+) R 12686 5897 5896 0 -1 0 27682 0 0 0 111928 85 0 0 25 0 1 0 422943196 117104640 27660 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 28590 27660 603 41 0 28549 0 vsize: 114360 [startup+1130.04 s] Raw data (loadavg): 1.00 1.00 0.93 2/54 12744 Raw data (stat): 12687 (minisat+) R 12686 5897 5896 0 -1 0 27682 0 0 0 112929 85 0 0 25 0 1 0 422943196 117104640 27660 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 28590 27660 603 41 0 28549 0 vsize: 114360 [startup+1140.04 s] Raw data (loadavg): 1.00 1.00 0.93 2/54 12744 Raw data (stat): 12687 (minisat+) R 12686 5897 5896 0 -1 0 27682 0 0 0 113929 85 0 0 25 0 1 0 422943196 117104640 27660 4294967295 134512640 134672761 3221224560 3221223728 134560895 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 28590 27660 603 41 0 28549 0 vsize: 114360 [startup+1150.04 s] Raw data (loadavg): 1.00 1.00 0.93 2/54 12744 Raw data (stat): 12687 (minisat+) R 12686 5897 5896 0 -1 0 27682 0 0 0 114929 85 0 0 25 0 1 0 422943196 117104640 27660 4294967295 134512640 134672761 3221224560 3221223724 134561235 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 28590 27660 603 41 0 28549 0 vsize: 114360 [startup+1160.04 s] Raw data (loadavg): 1.00 1.00 0.93 2/54 12744 Raw data (stat): 12687 (minisat+) R 12686 5897 5896 0 -1 0 27682 0 0 0 115929 85 0 0 25 0 1 0 422943196 117104640 27660 4294967295 134512640 134672761 3221224560 3221223716 134561241 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 28590 27660 603 41 0 28549 0 vsize: 114360 [startup+1170.04 s] Raw data (loadavg): 1.00 1.00 0.93 2/54 12744 Raw data (stat): 12687 (minisat+) R 12686 5897 5896 0 -1 0 27683 0 0 0 116929 85 0 0 25 0 1 0 422943196 117104640 27661 4294967295 134512640 134672761 3221224560 3221223700 134560556 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 28590 27661 603 41 0 28549 0 vsize: 114360 [startup+1180.04 s] Raw data (loadavg): 1.00 1.00 0.93 2/54 12744 Raw data (stat): 12687 (minisat+) R 12686 5897 5896 0 -1 0 27683 0 0 0 117929 85 0 0 25 0 1 0 422943196 117104640 27661 4294967295 134512640 134672761 3221224560 3221223760 134557895 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 28590 27661 603 41 0 28549 0 vsize: 114360 [startup+1190.04 s] Raw data (loadavg): 1.00 1.00 0.93 2/54 12744 Raw data (stat): 12687 (minisat+) R 12686 5897 5896 0 -1 0 27683 0 0 0 118930 85 0 0 25 0 1 0 422943196 117104640 27661 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 28590 27661 603 41 0 28549 0 vsize: 114360 [startup+1200.04 s] Raw data (loadavg): 1.00 1.00 0.93 2/54 12744 Raw data (stat): 12687 (minisat+) R 12686 5897 5896 0 -1 0 27685 0 0 0 119930 85 0 0 25 0 1 0 422943196 117104640 27663 4294967295 134512640 134672761 3221224560 3221223664 134559872 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 28590 27663 603 41 0 28549 0 vsize: 114360 Maximum CPU time exceeded: sending SIGTERM and SIGKILL [startup+1200.1 s] Raw data (loadavg): 1.00 1.00 0.93 1/54 12744 Raw data (stat): 12687 (minisat+) Z 12686 5897 5896 0 -1 12 27688 0 0 0 119930 91 0 0 25 0 1 0 422943196 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.1 CPU time (s): 1200.22 CPU user time (s): 1199.31 CPU system time (s): 0.912861 CPU usage (%): 100.01 Max. virtual memory (Kb): 114360 #### END WATCHER DATA #### #### BEGIN VERIFIER DATA #### ERROR: no interpretation found ! #### END VERIFIER DATA ####