Name | normalized-opb/web/www.nlsde.buaa.edu.cn/~kexu/benchmarks/frb53-24-opb/normalized-frb53-24-2.opb |
MD5SUM | 45b026c6b351128e9764d865ca917a59 |
Bench Category | optimization, small integers (OPTSMALLINT) |
Has Objective Function | YES |
Satisfiable | YES |
(Un)Satisfiability was proved | YES |
Best value of the objective function | -40 |
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.11 |
Number of variables | 1272 |
Total number of constraints | 94289 |
Number of constraints which are clauses | 94289 |
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 wulflinc6 THE 2005-04-14 02:57:53 (client local time) PB2005-SCRIPT v4.0 MARKUPS: idlaunch=4476 boxname=wulflinc6 idbench=340 idsolver=12 numberseed=0 MD5SUM SOLVER: MD5SUM BENCH: 45b026c6b351128e9764d865ca917a59 /oldhome/oroussel/tmp/wulflinc6/normalized-frb53-24-2.opb REAL COMMAND: minisat+ -cb -gs /oldhome/oroussel/tmp/wulflinc6/normalized-frb53-24-2.opb /oldhome/oroussel/tmp/wulflinc6/normalized-frb53-24-2.opb IDLAUNCH: 4476 /proc/cpuinfo: processor : 0 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 2 cpu MHz : 451.042 cache size : 512 KB fdiv_bug : no hlt_bug : no f00f_bug : no coma_bug : no fpu : yes fpu_exception : yes cpuid level : 2 wp : yes flags : fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse bogomips : 888.83 processor : 1 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 2 cpu MHz : 451.042 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: 876012 kB Buffers: 36436 kB Cached: 99572 kB SwapCached: 2644 kB Active: 55884 kB Inactive: 85664 kB HighTotal: 131008 kB HighFree: 27580 kB LowTotal: 903652 kB LowFree: 848432 kB SwapTotal: 2097136 kB SwapFree: 2094492 kB Dirty: 28 kB Writeback: 0 kB Mapped: 6928 kB Slab: 11512 kB Committed_AS: 63484 kB PageTables: 316 kB VmallocTotal: 114680 kB VmallocUsed: 1364 kB VmallocChunk: 113256 kB JOB ENDED THE 2005-04-14 03:17:55 (client local time) WITH STATUS 10 IN 1200.41 SECONDS stats: 4476 7 1200.41 10 #### END LAUNCHER DATA #### #### BEGIN SOLVER DATA #### c Parsing PB file... c Converting 94289 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 | 94289 188578 | 31429 0 0 nan | 0.000 % | c ============================================================================== c [1mFound solution: -38[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 | 169363 364695 | 56454 0 0 nan | 0.000 % | c | 100 | 168931 363803 | 62099 75 961 12.8 | 0.464 % | c | 251 | 168226 362304 | 68309 195 2080 10.7 | 1.241 % | c | 477 | 166908 359478 | 75140 361 4481 12.4 | 2.716 % | c | 814 | 165085 355491 | 82654 634 6941 10.9 | 4.833 % | c | 1320 | 161650 347896 | 90919 1002 11746 11.7 | 8.903 % | c | 2079 | 157439 338515 | 100011 1501 17642 11.8 | 13.952 % | c | 3218 | 149574 320611 | 110012 2257 27487 12.2 | 23.762 % | c | 4926 | 140077 298909 | 121014 3343 40938 12.2 | 35.604 % | c | 7488 | 129263 273622 | 133115 4970 57038 11.5 | 49.390 % | c | 11332 | 118074 247204 | 146427 7283 85078 11.7 | 64.089 % | 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 | 14173 | 112053 232947 | 37351 8812 110869 12.6 | 64.089 % | c | 14273 | 111956 232718 | 41086 8872 112201 12.6 | 72.341 % | c | 14423 | 111733 232187 | 45194 9002 114113 12.7 | 72.561 % | c | 14649 | 111451 231507 | 49714 9151 118315 12.9 | 72.945 % | c | 14986 | 111001 230402 | 54685 9390 121727 13.0 | 73.568 % | c | 15492 | 110268 228664 | 60154 9746 131154 13.5 | 74.539 % | c | 16252 | 109470 226728 | 66169 10246 139678 13.6 | 75.632 % | c | 17391 | 108305 223901 | 72786 11038 156782 14.2 | 77.225 % | c | 19099 | 106843 220411 | 80065 12116 192204 15.9 | 79.176 % | c | 21662 | 105578 217316 | 88071 13811 254342 18.4 | 80.914 % | c | 25506 | 104256 214065 | 96878 16859 438700 26.0 | 82.765 % | 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 | 29128 | 104139 213840 | 34713 20366 654650 32.1 | 82.765 % | c | 29229 | 104025 213562 | 38184 20446 657035 32.1 | 83.099 % | c | 29380 | 103872 213177 | 42002 20466 657976 32.1 | 83.323 % | c | 29605 | 103872 213177 | 46203 20691 675471 32.6 | 83.323 % | c | 29942 | 103872 213177 | 50823 21028 685274 32.6 | 83.323 % | c | 30448 | 103722 212801 | 55905 21442 702839 32.8 | 83.539 % | c | 31207 | 103261 211676 | 61496 21792 727090 33.4 | 84.177 % | c | 32346 | 103261 211676 | 67645 22931 784028 34.2 | 84.177 % | 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 | 33412 | 103252 211633 | 34417 23944 928774 38.8 | 84.177 % | c | 33512 | 103242 211609 | 37858 24024 929884 38.7 | 84.207 % | c | 33663 | 103242 211609 | 41644 24175 937156 38.8 | 84.207 % | c | 33888 | 103242 211609 | 45809 24400 945982 38.8 | 84.207 % | c | 34225 | 103106 211272 | 50389 24656 961580 39.0 | 84.396 % | c | 34731 | 103096 211246 | 55428 25109 984488 39.2 | 84.412 % | c | 35491 | 103053 211129 | 60971 25751 1012426 39.3 | 84.478 % | c | 36631 | 102901 210759 | 67068 26726 1066796 39.9 | 84.686 % | c | 38339 | 102881 210709 | 73775 28397 1192012 42.0 | 84.715 % | c | 40901 | 102881 210709 | 81153 30959 1469684 47.5 | 84.715 % | c | 44746 | 102871 210685 | 89268 34788 1844984 53.0 | 84.729 % | 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 | 49083 | 102808 210537 | 34269 39065 2552883 65.3 | 84.729 % | c | 49183 | 102715 210319 | 37695 39094 2554059 65.3 | 84.952 % | c | 49333 | 102715 210319 | 41465 39244 2564935 65.4 | 84.952 % | c | 49559 | 102638 210132 | 45612 39228 2570691 65.5 | 85.059 % | c | 49896 | 102638 210132 | 50173 39565 2591937 65.5 | 85.059 % | c | 50403 | 102638 210132 | 55190 40072 2655788 66.3 | 85.059 % | c | 51162 | 102638 210132 | 60709 40831 2713978 66.5 | 85.059 % | c | 52301 | 102627 210103 | 66780 41795 2803087 67.1 | 85.076 % | c | 54009 | 102492 209776 | 73458 43288 3004323 69.4 | 85.263 % | c | 56573 | 102482 209754 | 80804 45807 3307196 72.2 | 85.275 % | c | 60417 | 102434 209638 | 88884 49598 3816497 76.9 | 85.341 % | c | 66183 | 102321 209365 | 97773 54712 4533488 82.9 | 85.496 % | c | 74832 | 102098 208818 | 107550 62430 5539945 88.7 | 85.806 % | c | 87807 | 101884 208284 | 118305 75224 8117231 107.9 | 86.117 % | 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 | 89873 | 101873 208219 | 33957 77213 8366826 108.4 | 86.117 % | c | 89973 | 101813 208079 | 37352 77250 8370963 108.4 | 86.209 % | c | 90123 | 101813 208079 | 41087 77400 8384920 108.3 | 86.209 % | c | 90348 | 101813 208079 | 45196 77625 8402830 108.2 | 86.209 % | c | 90685 | 101813 208079 | 49716 77962 8425118 108.1 | 86.209 % | c | 91191 | 101808 208066 | 54688 78418 8477500 108.1 | 86.217 % | c | 91950 | 101769 207969 | 60156 79147 8535292 107.8 | 86.273 % | c | 93089 | 101732 207878 | 66172 79954 8650341 108.2 | 86.324 % | c | 94797 | 101691 207781 | 72789 81587 8836109 108.3 | 86.378 % | c | 97360 | 101678 207750 | 80068 84139 9093070 108.1 | 86.396 % | c | 101204 | 101587 207532 | 88075 87350 9467343 108.4 | 86.516 % | c | 106970 | 101584 207525 | 96883 93115 10262644 110.2 | 86.520 % | c | 115619 | 101584 207525 | 106571 101764 11400274 112.0 | 86.520 % | 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 | 128246 | 101576 207519 | 33858 113993 13276183 116.5 | 86.520 % | c | 128346 | 101576 207519 | 37243 20346 1966312 96.6 | 86.569 % | c | 128496 | 101576 207519 | 40968 20496 1972565 96.2 | 86.569 % | c | 128722 | 101576 207519 | 45064 20722 1990233 96.0 | 86.569 % | c | 129059 | 101576 207519 | 49571 21059 2010034 95.4 | 86.569 % | c | 129565 | 101573 207512 | 54528 21564 2043549 94.8 | 86.573 % | c | 130325 | 101573 207512 | 59981 22324 2119304 94.9 | 86.573 % | c | 131466 | 101573 207512 | 65979 23465 2227953 94.9 | 86.573 % | c | 133174 | 101566 207497 | 72577 25171 2440505 97.0 | 86.580 % | c | 135736 | 101564 207493 | 79835 27732 2748292 99.1 | 86.582 % | c | 139581 | 101564 207493 | 87818 31577 3280586 103.9 | 86.582 % | c | 145347 | 101564 207493 | 96600 37343 4140110 110.9 | 86.582 % | c | 153996 | 101564 207493 | 106260 45992 5223572 113.6 | 86.582 % | c | 166970 | 101517 207383 | 116886 58757 6847744 116.5 | 86.641 % | c | 186431 | 101502 207348 | 128575 78195 9333628 119.4 | 86.660 % | c | 215624 | 101465 207263 | 141433 107203 13487587 125.8 | 86.705 % | c | 259413 | 101459 207249 | 155576 150988 19357146 128.2 | 86.712 % | 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 #### 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.84 0.94 0.90 2/54 2555 Raw data (stat): 2555 (runsolver) R 2554 29653 29652 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 422947198 1052672 99 4294967295 134512640 135381576 3221224448 3221219692 135158418 0 2147483391 7 90112 0 0 0 17 0 0 0 Raw data (statm): 257 99 215 215 0 42 0 vsize: 1028 [startup+9.99957 s] Raw data (loadavg): 0.87 0.94 0.90 2/54 2555 Raw data (stat): 2555 (minisat+) R 2554 29653 29652 0 -1 0 5637 0 0 0 983 14 0 0 25 0 1 0 422947198 26091520 5615 4294967295 134512640 134672761 3221224560 3221223732 134556634 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 6370 5615 603 41 0 6329 0 vsize: 25480 [startup+19.9997 s] Raw data (loadavg): 0.89 0.94 0.90 2/54 2555 Raw data (stat): 2555 (minisat+) R 2554 29653 29652 0 -1 0 5647 0 0 0 1983 14 0 0 25 0 1 0 422947198 26091520 5625 4294967295 134512640 134672761 3221224560 3221223732 134556602 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 6370 5625 603 41 0 6329 0 vsize: 25480 [startup+29.9999 s] Raw data (loadavg): 0.90 0.94 0.90 2/54 2555 Raw data (stat): 2555 (minisat+) R 2554 29653 29652 0 -1 0 5653 0 0 0 2983 15 0 0 25 0 1 0 422947198 26226688 5631 4294967295 134512640 134672761 3221224560 3221223760 134557830 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 6403 5631 603 41 0 6362 0 vsize: 25612 [startup+39.9989 s] Raw data (loadavg): 0.92 0.94 0.90 2/54 2555 Raw data (stat): 2555 (minisat+) R 2554 29653 29652 0 -1 0 5660 0 0 0 3983 15 0 0 25 0 1 0 422947198 26226688 5638 4294967295 134512640 134672761 3221224560 3221223732 134556598 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 6403 5638 603 41 0 6362 0 vsize: 25612 [startup+49.9991 s] Raw data (loadavg): 0.93 0.94 0.90 2/54 2555 Raw data (stat): 2555 (minisat+) R 2554 29653 29652 0 -1 0 5667 0 0 0 4983 15 0 0 25 0 1 0 422947198 26226688 5645 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 6403 5645 603 41 0 6362 0 vsize: 25612 [startup+59.9986 s] Raw data (loadavg): 0.94 0.95 0.90 2/54 2555 Raw data (stat): 2555 (minisat+) R 2554 29653 29652 0 -1 0 5675 0 0 0 5984 15 0 0 25 0 1 0 422947198 26226688 5653 4294967295 134512640 134672761 3221224560 3221223732 134556634 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 6403 5653 603 41 0 6362 0 vsize: 25612 [startup+69.9984 s] Raw data (loadavg): 0.95 0.95 0.91 2/54 2555 Raw data (stat): 2555 (minisat+) R 2554 29653 29652 0 -1 0 5677 0 0 0 6984 15 0 0 25 0 1 0 422947198 26226688 5655 4294967295 134512640 134672761 3221224560 3221223756 134556584 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 6403 5655 603 41 0 6362 0 vsize: 25612 [startup+79.9985 s] Raw data (loadavg): 0.96 0.95 0.91 2/54 2555 Raw data (stat): 2555 (minisat+) R 2554 29653 29652 0 -1 0 5684 0 0 0 7984 15 0 0 25 0 1 0 422947198 26357760 5662 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 6435 5662 603 41 0 6394 0 vsize: 25740 [startup+89.9977 s] Raw data (loadavg): 0.96 0.95 0.91 2/54 2555 Raw data (stat): 2555 (minisat+) R 2554 29653 29652 0 -1 0 5698 0 0 0 8985 15 0 0 25 0 1 0 422947198 26357760 5676 4294967295 134512640 134672761 3221224560 3221223696 134560588 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 6435 5676 603 41 0 6394 0 vsize: 25740 [startup+99.9969 s] Raw data (loadavg): 0.97 0.95 0.91 2/54 2555 Raw data (stat): 2555 (minisat+) R 2554 29653 29652 0 -1 0 5863 0 0 0 9984 15 0 0 25 0 1 0 422947198 27406336 5841 4294967295 134512640 134672761 3221224560 3221223732 134556598 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 6691 5841 603 41 0 6650 0 vsize: 26764 [startup+109.997 s] Raw data (loadavg): 0.97 0.95 0.91 2/54 2555 Raw data (stat): 2555 (minisat+) R 2554 29653 29652 0 -1 0 5866 0 0 0 10983 16 0 0 25 0 1 0 422947198 27406336 5844 4294967295 134512640 134672761 3221224560 3221223732 134556598 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 6691 5844 603 41 0 6650 0 vsize: 26764 [startup+119.997 s] Raw data (loadavg): 0.98 0.95 0.91 2/54 2555 Raw data (stat): 2555 (minisat+) R 2554 29653 29652 0 -1 0 6091 0 0 0 11983 16 0 0 25 0 1 0 422947198 28344320 6069 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 6920 6069 603 41 0 6879 0 vsize: 27680 [startup+129.997 s] Raw data (loadavg): 0.98 0.95 0.91 2/54 2555 Raw data (stat): 2555 (minisat+) R 2554 29653 29652 0 -1 0 6450 0 0 0 12983 17 0 0 25 0 1 0 422947198 29827072 6428 4294967295 134512640 134672761 3221224560 3221223732 134556634 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 7282 6428 603 41 0 7241 0 vsize: 29128 [startup+139.996 s] Raw data (loadavg): 0.98 0.95 0.91 2/54 2608 Raw data (stat): 2555 (minisat+) R 2554 29653 29652 0 -1 0 6830 0 0 0 13981 19 0 0 25 0 1 0 422947198 31379456 6808 4294967295 134512640 134672761 3221224560 3221223728 134560833 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 7661 6808 603 41 0 7620 0 vsize: 30644 [startup+149.997 s] Raw data (loadavg): 1.05 0.97 0.91 2/54 2608 Raw data (stat): 2555 (minisat+) R 2554 29653 29652 0 -1 0 7399 0 0 0 14979 21 0 0 25 0 1 0 422947198 33669120 7377 4294967295 134512640 134672761 3221224560 3221223732 134556598 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 8220 7377 603 41 0 8179 0 vsize: 32880 [startup+159.996 s] Raw data (loadavg): 1.04 0.97 0.91 2/54 2608 Raw data (stat): 2555 (minisat+) R 2554 29653 29652 0 -1 0 8001 0 0 0 15978 23 0 0 25 0 1 0 422947198 36343808 7979 4294967295 134512640 134672761 3221224560 3221223696 134565045 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 8873 7979 603 41 0 8832 0 vsize: 35492 [startup+169.995 s] Raw data (loadavg): 1.04 0.97 0.91 2/54 2608 Raw data (stat): 2555 (minisat+) R 2554 29653 29652 0 -1 0 8627 0 0 0 16977 24 0 0 25 0 1 0 422947198 38817792 8605 4294967295 134512640 134672761 3221224560 3221223576 1075352757 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 9477 8605 603 41 0 9436 0 vsize: 37908 [startup+179.994 s] Raw data (loadavg): 1.03 0.97 0.91 2/54 2608 Raw data (stat): 2555 (minisat+) R 2554 29653 29652 0 -1 0 9069 0 0 0 17975 26 0 0 25 0 1 0 422947198 40697856 9047 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 9936 9047 603 41 0 9895 0 vsize: 39744 [startup+189.994 s] Raw data (loadavg): 1.03 0.97 0.91 2/54 2608 Raw data (stat): 2555 (minisat+) R 2554 29653 29652 0 -1 0 9646 0 0 0 18973 28 0 0 25 0 1 0 422947198 42979328 9624 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 10493 9624 603 41 0 10452 0 vsize: 41972 [startup+199.993 s] Raw data (loadavg): 1.02 0.97 0.91 2/54 2608 Raw data (stat): 2555 (minisat+) R 2554 29653 29652 0 -1 0 10037 0 0 0 19972 29 0 0 25 0 1 0 422947198 44589056 10015 4294967295 134512640 134672761 3221224560 3221223732 134556634 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 10886 10015 603 41 0 10845 0 vsize: 43544 [startup+209.992 s] Raw data (loadavg): 1.02 0.97 0.91 2/54 2610 Raw data (stat): 2555 (minisat+) R 2554 29653 29652 0 -1 0 10592 0 0 0 20970 31 0 0 25 0 1 0 422947198 46870528 10570 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 11443 10570 603 41 0 11402 0 vsize: 45772 [startup+219.993 s] Raw data (loadavg): 1.01 0.97 0.91 2/54 2610 Raw data (stat): 2555 (minisat+) R 2554 29653 29652 0 -1 0 11049 0 0 0 21969 33 0 0 25 0 1 0 422947198 48742400 11027 4294967295 134512640 134672761 3221224560 3221223664 134560246 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 11900 11027 603 41 0 11859 0 vsize: 47600 [startup+229.993 s] Raw data (loadavg): 1.01 0.97 0.91 2/54 2610 Raw data (stat): 2555 (minisat+) R 2554 29653 29652 0 -1 0 11418 0 0 0 22968 34 0 0 25 0 1 0 422947198 50204672 11396 4294967295 134512640 134672761 3221224560 3221223664 134555114 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 12257 11396 603 41 0 12216 0 vsize: 49028 [startup+239.992 s] Raw data (loadavg): 1.01 0.97 0.91 2/54 2610 Raw data (stat): 2555 (minisat+) R 2554 29653 29652 0 -1 0 11720 0 0 0 23967 35 0 0 25 0 1 0 422947198 51412992 11698 4294967295 134512640 134672761 3221224560 3221223664 134560169 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 12552 11698 603 41 0 12511 0 vsize: 50208 [startup+249.992 s] Raw data (loadavg): 1.01 0.97 0.91 2/54 2610 Raw data (stat): 2555 (minisat+) R 2554 29653 29652 0 -1 0 12231 0 0 0 24966 37 0 0 25 0 1 0 422947198 53821440 12209 4294967295 134512640 134672761 3221224560 3221223728 134560980 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 13140 12209 603 41 0 13099 0 vsize: 52560 [startup+259.992 s] Raw data (loadavg): 1.01 0.97 0.91 2/54 2610 Raw data (stat): 2555 (minisat+) R 2554 29653 29652 0 -1 0 12777 0 0 0 25965 38 0 0 25 0 1 0 422947198 55967744 12755 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 13664 12755 603 41 0 13623 0 vsize: 54656 [startup+269.991 s] Raw data (loadavg): 1.00 0.97 0.91 2/54 2610 Raw data (stat): 2555 (minisat+) R 2554 29653 29652 0 -1 0 13305 0 0 0 26964 39 0 0 25 0 1 0 422947198 58101760 13283 4294967295 134512640 134672761 3221224560 3221223664 134560196 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 14185 13283 603 41 0 14144 0 vsize: 56740 [startup+279.991 s] Raw data (loadavg): 1.00 0.97 0.91 2/54 2610 Raw data (stat): 2555 (minisat+) R 2554 29653 29652 0 -1 0 13825 0 0 0 27963 41 0 0 25 0 1 0 422947198 60243968 13803 4294967295 134512640 134672761 3221224560 3221223728 134560996 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 14708 13803 603 41 0 14667 0 vsize: 58832 [startup+289.991 s] Raw data (loadavg): 1.00 0.97 0.91 2/54 2610 Raw data (stat): 2555 (minisat+) R 2554 29653 29652 0 -1 0 14326 0 0 0 28961 43 0 0 25 0 1 0 422947198 62251008 14304 4294967295 134512640 134672761 3221224560 3221223728 134561205 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 15198 14304 603 41 0 15157 0 vsize: 60792 [startup+299.99 s] Raw data (loadavg): 1.00 0.97 0.91 2/54 2610 Raw data (stat): 2555 (minisat+) R 2554 29653 29652 0 -1 0 14630 0 0 0 29961 43 0 0 25 0 1 0 422947198 63508480 14608 4294967295 134512640 134672761 3221224560 3221223744 134558654 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 15505 14608 603 41 0 15464 0 vsize: 62020 [startup+309.99 s] Raw data (loadavg): 1.00 0.97 0.91 2/54 2610 Raw data (stat): 2555 (minisat+) R 2554 29653 29652 0 -1 0 14879 0 0 0 30961 44 0 0 25 0 1 0 422947198 64581632 14857 4294967295 134512640 134672761 3221224560 3221223728 134561188 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 15767 14857 603 41 0 15726 0 vsize: 63068 [startup+319.99 s] Raw data (loadavg): 1.00 0.97 0.91 2/54 2610 Raw data (stat): 2555 (minisat+) R 2554 29653 29652 0 -1 0 15202 0 0 0 31961 44 0 0 25 0 1 0 422947198 65921024 15180 4294967295 134512640 134672761 3221224560 3221223696 134560677 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 16094 15180 603 41 0 16053 0 vsize: 64376 [startup+329.99 s] Raw data (loadavg): 1.00 0.97 0.91 2/54 2610 Raw data (stat): 2555 (minisat+) R 2554 29653 29652 0 -1 0 15471 0 0 0 32960 45 0 0 25 0 1 0 422947198 66994176 15449 4294967295 134512640 134672761 3221224560 3221223728 134560940 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 16356 15449 603 41 0 16315 0 vsize: 65424 [startup+339.99 s] Raw data (loadavg): 1.00 0.97 0.91 2/54 2610 Raw data (stat): 2555 (minisat+) R 2554 29653 29652 0 -1 0 15737 0 0 0 33960 46 0 0 25 0 1 0 422947198 68067328 15715 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 16618 15715 603 41 0 16577 0 vsize: 66472 [startup+349.99 s] Raw data (loadavg): 1.00 0.97 0.91 2/54 2610 Raw data (stat): 2555 (minisat+) R 2554 29653 29652 0 -1 0 16078 0 0 0 34959 47 0 0 25 0 1 0 422947198 69410816 16056 4294967295 134512640 134672761 3221224560 3221223728 134561190 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 16946 16056 603 41 0 16905 0 vsize: 67784 [startup+359.99 s] Raw data (loadavg): 1.00 0.97 0.91 2/54 2610 Raw data (stat): 2555 (minisat+) R 2554 29653 29652 0 -1 0 16405 0 0 0 35958 48 0 0 25 0 1 0 422947198 70750208 16383 4294967295 134512640 134672761 3221224560 3221223728 134560929 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 17273 16383 603 41 0 17232 0 vsize: 69092 [startup+369.99 s] Raw data (loadavg): 1.00 0.97 0.91 2/54 2610 Raw data (stat): 2555 (minisat+) R 2554 29653 29652 0 -1 0 16742 0 0 0 36957 50 0 0 25 0 1 0 422947198 72093696 16720 4294967295 134512640 134672761 3221224560 3221223728 134561167 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 17601 16720 603 41 0 17560 0 vsize: 70404 [startup+379.99 s] Raw data (loadavg): 1.00 0.97 0.91 2/54 2610 Raw data (stat): 2555 (minisat+) R 2554 29653 29652 0 -1 0 17029 0 0 0 37957 50 0 0 25 0 1 0 422947198 73277440 17007 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 17890 17007 603 41 0 17849 0 vsize: 71560 [startup+389.99 s] Raw data (loadavg): 1.00 0.97 0.91 2/54 2610 Raw data (stat): 2555 (minisat+) R 2554 29653 29652 0 -1 0 17327 0 0 0 38956 51 0 0 25 0 1 0 422947198 74469376 17305 4294967295 134512640 134672761 3221224560 3221223744 134558662 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 18181 17305 603 41 0 18140 0 vsize: 72724 [startup+399.991 s] Raw data (loadavg): 1.00 0.97 0.91 2/54 2610 Raw data (stat): 2555 (minisat+) R 2554 29653 29652 0 -1 0 17627 0 0 0 39956 52 0 0 25 0 1 0 422947198 75792384 17605 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 18504 17605 603 41 0 18463 0 vsize: 74016 [startup+409.99 s] Raw data (loadavg): 1.00 0.97 0.91 2/54 2610 Raw data (stat): 2555 (minisat+) R 2554 29653 29652 0 -1 0 17914 0 0 0 40955 53 0 0 25 0 1 0 422947198 76849152 17892 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 18762 17892 603 41 0 18721 0 vsize: 75048 [startup+419.991 s] Raw data (loadavg): 1.00 0.97 0.91 2/54 2610 Raw data (stat): 2555 (minisat+) R 2554 29653 29652 0 -1 0 18190 0 0 0 41955 54 0 0 25 0 1 0 422947198 78049280 18168 4294967295 134512640 134672761 3221224560 3221223728 134560999 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 19055 18168 603 41 0 19014 0 vsize: 76220 [startup+429.992 s] Raw data (loadavg): 1.00 0.97 0.91 2/54 2610 Raw data (stat): 2555 (minisat+) R 2554 29653 29652 0 -1 0 18481 0 0 0 42955 54 0 0 25 0 1 0 422947198 79245312 18459 4294967295 134512640 134672761 3221224560 3221223728 134560876 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 19347 18459 603 41 0 19306 0 vsize: 77388 [startup+439.992 s] Raw data (loadavg): 1.00 0.97 0.91 2/54 2610 Raw data (stat): 2555 (minisat+) R 2554 29653 29652 0 -1 0 18832 0 0 0 43954 55 0 0 25 0 1 0 422947198 80580608 18810 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 19673 18810 603 41 0 19632 0 vsize: 78692 [startup+449.992 s] Raw data (loadavg): 1.00 0.97 0.91 2/54 2612 Raw data (stat): 2555 (minisat+) R 2554 29653 29652 0 -1 0 19207 0 0 0 44953 56 0 0 25 0 1 0 422947198 82178048 19185 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 20063 19185 603 41 0 20022 0 vsize: 80252 [startup+459.993 s] Raw data (loadavg): 1.00 0.97 0.91 2/54 2612 Raw data (stat): 2555 (minisat+) R 2554 29653 29652 0 -1 0 19574 0 0 0 45953 57 0 0 25 0 1 0 422947198 83648512 19552 4294967295 134512640 134672761 3221224560 3221223728 134561215 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 20422 19552 603 41 0 20381 0 vsize: 81688 [startup+469.992 s] Raw data (loadavg): 1.00 0.97 0.91 2/54 2612 Raw data (stat): 2555 (minisat+) R 2554 29653 29652 0 -1 0 19857 0 0 0 46953 57 0 0 25 0 1 0 422947198 84770816 19835 4294967295 134512640 134672761 3221224560 3221223664 134554671 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 20696 19835 603 41 0 20655 0 vsize: 82784 [startup+479.992 s] Raw data (loadavg): 1.00 0.97 0.91 2/54 2612 Raw data (stat): 2555 (minisat+) R 2554 29653 29652 0 -1 0 19857 0 0 0 47953 57 0 0 25 0 1 0 422947198 84770816 19835 4294967295 134512640 134672761 3221224560 3221223696 134565092 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 20696 19835 603 41 0 20655 0 vsize: 82784 [startup+489.992 s] Raw data (loadavg): 1.00 0.97 0.91 2/54 2612 Raw data (stat): 2555 (minisat+) R 2554 29653 29652 0 -1 0 19857 0 0 0 48953 57 0 0 25 0 1 0 422947198 84770816 19835 4294967295 134512640 134672761 3221224560 3221223728 134561164 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 20696 19835 603 41 0 20655 0 vsize: 82784 [startup+499.992 s] Raw data (loadavg): 1.00 0.97 0.91 2/54 2612 Raw data (stat): 2555 (minisat+) R 2554 29653 29652 0 -1 0 19857 0 0 0 49954 57 0 0 25 0 1 0 422947198 84770816 19835 4294967295 134512640 134672761 3221224560 3221223728 134560996 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 20696 19835 603 41 0 20655 0 vsize: 82784 [startup+509.992 s] Raw data (loadavg): 1.00 0.97 0.91 2/54 2612 Raw data (stat): 2555 (minisat+) R 2554 29653 29652 0 -1 0 19857 0 0 0 50954 57 0 0 25 0 1 0 422947198 84770816 19835 4294967295 134512640 134672761 3221224560 3221223712 134561244 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 20696 19835 603 41 0 20655 0 vsize: 82784 [startup+519.992 s] Raw data (loadavg): 1.00 0.97 0.91 2/54 2612 Raw data (stat): 2555 (minisat+) R 2554 29653 29652 0 -1 0 19857 0 0 0 51954 57 0 0 25 0 1 0 422947198 84770816 19835 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 20696 19835 603 41 0 20655 0 vsize: 82784 [startup+529.992 s] Raw data (loadavg): 1.00 0.97 0.91 2/54 2612 Raw data (stat): 2555 (minisat+) R 2554 29653 29652 0 -1 0 19857 0 0 0 52955 57 0 0 25 0 1 0 422947198 84770816 19835 4294967295 134512640 134672761 3221224560 3221223712 134561244 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 20696 19835 603 41 0 20655 0 vsize: 82784 [startup+539.993 s] Raw data (loadavg): 1.00 0.97 0.91 2/54 2612 Raw data (stat): 2555 (minisat+) R 2554 29653 29652 0 -1 0 19857 0 0 0 53955 57 0 0 25 0 1 0 422947198 84770816 19835 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 20696 19835 603 41 0 20655 0 vsize: 82784 [startup+549.993 s] Raw data (loadavg): 1.00 0.97 0.91 2/54 2612 Raw data (stat): 2555 (minisat+) R 2554 29653 29652 0 -1 0 19857 0 0 0 54955 57 0 0 25 0 1 0 422947198 84770816 19835 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 20696 19835 603 41 0 20655 0 vsize: 82784 [startup+559.993 s] Raw data (loadavg): 1.00 0.97 0.91 2/54 2612 Raw data (stat): 2555 (minisat+) R 2554 29653 29652 0 -1 0 19857 0 0 0 55956 57 0 0 25 0 1 0 422947198 84770816 19835 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 20696 19835 603 41 0 20655 0 vsize: 82784 [startup+569.993 s] Raw data (loadavg): 1.00 0.97 0.91 2/54 2612 Raw data (stat): 2555 (minisat+) R 2554 29653 29652 0 -1 0 19857 0 0 0 56956 57 0 0 25 0 1 0 422947198 84770816 19835 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 20696 19835 603 41 0 20655 0 vsize: 82784 [startup+579.993 s] Raw data (loadavg): 1.00 0.97 0.91 2/54 2612 Raw data (stat): 2555 (minisat+) R 2554 29653 29652 0 -1 0 19857 0 0 0 57956 57 0 0 25 0 1 0 422947198 84770816 19835 4294967295 134512640 134672761 3221224560 3221223760 134557852 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 20696 19835 603 41 0 20655 0 vsize: 82784 [startup+589.993 s] Raw data (loadavg): 1.00 0.97 0.91 2/54 2612 Raw data (stat): 2555 (minisat+) R 2554 29653 29652 0 -1 0 19857 0 0 0 58957 57 0 0 25 0 1 0 422947198 84770816 19835 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 20696 19835 603 41 0 20655 0 vsize: 82784 [startup+599.994 s] Raw data (loadavg): 1.00 0.97 0.91 2/54 2612 Raw data (stat): 2555 (minisat+) R 2554 29653 29652 0 -1 0 19857 0 0 0 59957 57 0 0 25 0 1 0 422947198 84770816 19835 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 20696 19835 603 41 0 20655 0 vsize: 82784 [startup+609.994 s] Raw data (loadavg): 1.00 0.97 0.91 2/54 2612 Raw data (stat): 2555 (minisat+) R 2554 29653 29652 0 -1 0 19857 0 0 0 60958 57 0 0 25 0 1 0 422947198 84770816 19835 4294967295 134512640 134672761 3221224560 3221223712 134565045 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 20696 19835 603 41 0 20655 0 vsize: 82784 [startup+619.994 s] Raw data (loadavg): 1.00 0.97 0.91 2/54 2612 Raw data (stat): 2555 (minisat+) R 2554 29653 29652 0 -1 0 19857 0 0 0 61958 57 0 0 25 0 1 0 422947198 84770816 19835 4294967295 134512640 134672761 3221224560 3221223664 134560246 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 20696 19835 603 41 0 20655 0 vsize: 82784 [startup+629.994 s] Raw data (loadavg): 1.00 0.97 0.91 2/54 2612 Raw data (stat): 2555 (minisat+) R 2554 29653 29652 0 -1 0 19857 0 0 0 62958 57 0 0 25 0 1 0 422947198 84770816 19835 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 20696 19835 603 41 0 20655 0 vsize: 82784 [startup+639.994 s] Raw data (loadavg): 1.00 0.97 0.91 2/54 2612 Raw data (stat): 2555 (minisat+) R 2554 29653 29652 0 -1 0 19857 0 0 0 63959 57 0 0 25 0 1 0 422947198 84770816 19835 4294967295 134512640 134672761 3221224560 3221223728 134561215 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 20696 19835 603 41 0 20655 0 vsize: 82784 [startup+649.994 s] Raw data (loadavg): 1.00 0.97 0.91 2/54 2612 Raw data (stat): 2555 (minisat+) R 2554 29653 29652 0 -1 0 19857 0 0 0 64959 57 0 0 25 0 1 0 422947198 84770816 19835 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 20696 19835 603 41 0 20655 0 vsize: 82784 [startup+659.995 s] Raw data (loadavg): 1.00 0.97 0.91 2/54 2612 Raw data (stat): 2555 (minisat+) R 2554 29653 29652 0 -1 0 19857 0 0 0 65959 57 0 0 25 0 1 0 422947198 84770816 19835 4294967295 134512640 134672761 3221224560 3221223728 134560858 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 20696 19835 603 41 0 20655 0 vsize: 82784 [startup+669.995 s] Raw data (loadavg): 1.00 0.97 0.91 2/54 2612 Raw data (stat): 2555 (minisat+) R 2554 29653 29652 0 -1 0 19857 0 0 0 66960 57 0 0 25 0 1 0 422947198 84770816 19835 4294967295 134512640 134672761 3221224560 3221223728 134561151 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 20696 19835 603 41 0 20655 0 vsize: 82784 [startup+679.995 s] Raw data (loadavg): 1.00 0.97 0.91 2/54 2612 Raw data (stat): 2555 (minisat+) R 2554 29653 29652 0 -1 0 19857 0 0 0 67960 57 0 0 25 0 1 0 422947198 84770816 19835 4294967295 134512640 134672761 3221224560 3221223728 134561151 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 20696 19835 603 41 0 20655 0 vsize: 82784 [startup+689.995 s] Raw data (loadavg): 1.00 0.97 0.91 2/54 2612 Raw data (stat): 2555 (minisat+) R 2554 29653 29652 0 -1 0 19857 0 0 0 68960 57 0 0 25 0 1 0 422947198 84770816 19835 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 20696 19835 603 41 0 20655 0 vsize: 82784 [startup+699.995 s] Raw data (loadavg): 1.00 0.97 0.91 2/54 2612 Raw data (stat): 2555 (minisat+) R 2554 29653 29652 0 -1 0 19857 0 0 0 69961 57 0 0 25 0 1 0 422947198 84770816 19835 4294967295 134512640 134672761 3221224560 3221223664 134560196 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 20696 19835 603 41 0 20655 0 vsize: 82784 [startup+709.995 s] Raw data (loadavg): 1.00 0.97 0.91 2/54 2612 Raw data (stat): 2555 (minisat+) R 2554 29653 29652 0 -1 0 19857 0 0 0 70961 57 0 0 25 0 1 0 422947198 84770816 19835 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 20696 19835 603 41 0 20655 0 vsize: 82784 [startup+719.995 s] Raw data (loadavg): 1.00 0.97 0.91 2/54 2612 Raw data (stat): 2555 (minisat+) R 2554 29653 29652 0 -1 0 19857 0 0 0 71961 57 0 0 25 0 1 0 422947198 84770816 19835 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 20696 19835 603 41 0 20655 0 vsize: 82784 [startup+729.996 s] Raw data (loadavg): 1.00 0.97 0.91 2/54 2612 Raw data (stat): 2555 (minisat+) R 2554 29653 29652 0 -1 0 19857 0 0 0 72962 57 0 0 25 0 1 0 422947198 84770816 19835 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 20696 19835 603 41 0 20655 0 vsize: 82784 [startup+739.995 s] Raw data (loadavg): 1.00 0.97 0.91 2/54 2612 Raw data (stat): 2555 (minisat+) R 2554 29653 29652 0 -1 0 19857 0 0 0 73962 57 0 0 25 0 1 0 422947198 84770816 19835 4294967295 134512640 134672761 3221224560 3221223728 134560876 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 20696 19835 603 41 0 20655 0 vsize: 82784 [startup+749.996 s] Raw data (loadavg): 1.00 0.97 0.91 2/54 2612 Raw data (stat): 2555 (minisat+) R 2554 29653 29652 0 -1 0 19857 0 0 0 74962 57 0 0 25 0 1 0 422947198 84770816 19835 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 20696 19835 603 41 0 20655 0 vsize: 82784 [startup+759.996 s] Raw data (loadavg): 1.00 0.97 0.91 2/54 2612 Raw data (stat): 2555 (minisat+) R 2554 29653 29652 0 -1 0 20159 0 0 0 75962 58 0 0 25 0 1 0 422947198 86110208 20137 4294967295 134512640 134672761 3221224560 3221223728 134561229 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 21023 20137 603 41 0 20982 0 vsize: 84092 [startup+769.996 s] Raw data (loadavg): 1.00 0.97 0.91 2/54 2612 Raw data (stat): 2555 (minisat+) R 2554 29653 29652 0 -1 0 20481 0 0 0 76961 59 0 0 25 0 1 0 422947198 87306240 20459 4294967295 134512640 134672761 3221224560 3221223760 134557911 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 21315 20459 603 41 0 21274 0 vsize: 85260 [startup+779.996 s] Raw data (loadavg): 1.00 0.97 0.91 2/54 2612 Raw data (stat): 2555 (minisat+) R 2554 29653 29652 0 -1 0 20755 0 0 0 77961 60 0 0 25 0 1 0 422947198 88506368 20733 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 21608 20733 603 41 0 21567 0 vsize: 86432 [startup+789.997 s] Raw data (loadavg): 1.00 0.97 0.91 2/54 2612 Raw data (stat): 2555 (minisat+) R 2554 29653 29652 0 -1 0 20997 0 0 0 78960 61 0 0 25 0 1 0 422947198 89436160 20975 4294967295 134512640 134672761 3221224560 3221223704 134560630 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 21835 20975 603 41 0 21794 0 vsize: 87340 [startup+799.996 s] Raw data (loadavg): 1.00 0.97 0.91 2/54 2612 Raw data (stat): 2555 (minisat+) R 2554 29653 29652 0 -1 0 21252 0 0 0 79959 62 0 0 25 0 1 0 422947198 90488832 21230 4294967295 134512640 134672761 3221224560 3221223728 134561008 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 22092 21230 603 41 0 22051 0 vsize: 88368 [startup+809.996 s] Raw data (loadavg): 1.00 0.97 0.91 2/54 2612 Raw data (stat): 2555 (minisat+) R 2554 29653 29652 0 -1 0 21567 0 0 0 80958 63 0 0 25 0 1 0 422947198 91828224 21545 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 22419 21545 603 41 0 22378 0 vsize: 89676 [startup+819.997 s] Raw data (loadavg): 1.00 0.97 0.91 2/54 2612 Raw data (stat): 2555 (minisat+) R 2554 29653 29652 0 -1 0 21851 0 0 0 81958 64 0 0 25 0 1 0 422947198 93032448 21829 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 22713 21829 603 41 0 22672 0 vsize: 90852 [startup+829.997 s] Raw data (loadavg): 1.00 0.97 0.91 2/54 2612 Raw data (stat): 2555 (minisat+) R 2554 29653 29652 0 -1 0 22148 0 0 0 82958 65 0 0 25 0 1 0 422947198 94232576 22126 4294967295 134512640 134672761 3221224560 3221223728 134561278 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 23006 22126 603 41 0 22965 0 vsize: 92024 [startup+839.997 s] Raw data (loadavg): 1.00 0.97 0.91 2/54 2612 Raw data (stat): 2555 (minisat+) R 2554 29653 29652 0 -1 0 22419 0 0 0 83958 65 0 0 25 0 1 0 422947198 95297536 22397 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 23266 22397 603 41 0 23225 0 vsize: 93064 [startup+849.997 s] Raw data (loadavg): 1.00 0.97 0.91 2/54 2612 Raw data (stat): 2555 (minisat+) R 2554 29653 29652 0 -1 0 22681 0 0 0 84957 66 0 0 25 0 1 0 422947198 96358400 22659 4294967295 134512640 134672761 3221224560 3221223728 134561212 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 23525 22659 603 41 0 23484 0 vsize: 94100 [startup+859.997 s] Raw data (loadavg): 1.00 0.97 0.91 2/54 2612 Raw data (stat): 2555 (minisat+) R 2554 29653 29652 0 -1 0 22936 0 0 0 85956 67 0 0 25 0 1 0 422947198 97427456 22914 4294967295 134512640 134672761 3221224560 3221223728 134560940 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 23786 22914 603 41 0 23745 0 vsize: 95144 [startup+869.997 s] Raw data (loadavg): 1.00 0.97 0.91 2/54 2612 Raw data (stat): 2555 (minisat+) R 2554 29653 29652 0 -1 0 23244 0 0 0 86956 68 0 0 25 0 1 0 422947198 98639872 23222 4294967295 134512640 134672761 3221224560 3221223728 134561118 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 24082 23222 603 41 0 24041 0 vsize: 96328 [startup+879.997 s] Raw data (loadavg): 1.00 0.97 0.91 2/54 2612 Raw data (stat): 2555 (minisat+) R 2554 29653 29652 0 -1 0 23509 0 0 0 87955 69 0 0 25 0 1 0 422947198 100229120 23487 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 24470 23487 603 41 0 24429 0 vsize: 97880 [startup+889.998 s] Raw data (loadavg): 1.00 0.97 0.91 2/54 2612 Raw data (stat): 2555 (minisat+) R 2554 29653 29652 0 -1 0 23785 0 0 0 88954 70 0 0 25 0 1 0 422947198 101433344 23763 4294967295 134512640 134672761 3221224560 3221223664 134560529 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 24764 23763 603 41 0 24723 0 vsize: 99056 [startup+899.998 s] Raw data (loadavg): 1.00 0.97 0.91 2/54 2612 Raw data (stat): 2555 (minisat+) R 2554 29653 29652 0 -1 0 24044 0 0 0 89953 72 0 0 25 0 1 0 422947198 102367232 24022 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 24992 24022 603 41 0 24951 0 vsize: 99968 [startup+909.998 s] Raw data (loadavg): 1.00 0.97 0.91 2/54 2612 Raw data (stat): 2555 (minisat+) R 2554 29653 29652 0 -1 0 24310 0 0 0 90952 73 0 0 25 0 1 0 422947198 103444480 24288 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 25255 24288 603 41 0 25214 0 vsize: 101020 [startup+919.998 s] Raw data (loadavg): 1.00 0.97 0.91 2/54 2612 Raw data (stat): 2555 (minisat+) R 2554 29653 29652 0 -1 0 24565 0 0 0 91952 74 0 0 25 0 1 0 422947198 104505344 24543 4294967295 134512640 134672761 3221224560 3221223664 134559925 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 25514 24543 603 41 0 25473 0 vsize: 102056 [startup+929.998 s] Raw data (loadavg): 1.00 0.97 0.91 2/54 2612 Raw data (stat): 2555 (minisat+) R 2554 29653 29652 0 -1 0 24817 0 0 0 92951 74 0 0 25 0 1 0 422947198 105570304 24795 4294967295 134512640 134672761 3221224560 3221223728 134561193 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 25774 24795 603 41 0 25733 0 vsize: 103096 [startup+939.998 s] Raw data (loadavg): 1.00 0.97 0.91 2/54 2612 Raw data (stat): 2555 (minisat+) R 2554 29653 29652 0 -1 0 25054 0 0 0 93951 75 0 0 25 0 1 0 422947198 106487808 25032 4294967295 134512640 134672761 3221224560 3221223728 134561193 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 25998 25032 603 41 0 25957 0 vsize: 103992 [startup+949.999 s] Raw data (loadavg): 1.00 0.97 0.91 2/54 2612 Raw data (stat): 2555 (minisat+) R 2554 29653 29652 0 -1 0 25301 0 0 0 94950 76 0 0 25 0 1 0 422947198 107552768 25279 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 26258 25279 603 41 0 26217 0 vsize: 105032 [startup+959.999 s] Raw data (loadavg): 1.00 0.97 0.91 2/54 2612 Raw data (stat): 2555 (minisat+) R 2554 29653 29652 0 -1 0 25538 0 0 0 95949 77 0 0 25 0 1 0 422947198 108494848 25516 4294967295 134512640 134672761 3221224560 3221223728 134561001 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 26488 25516 603 41 0 26447 0 vsize: 105952 [startup+969.999 s] Raw data (loadavg): 1.00 0.97 0.91 2/54 2612 Raw data (stat): 2555 (minisat+) R 2554 29653 29652 0 -1 0 25778 0 0 0 96949 78 0 0 25 0 1 0 422947198 109547520 25756 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 26745 25756 603 41 0 26704 0 vsize: 106980 [startup+979.999 s] Raw data (loadavg): 1.00 0.97 0.91 2/54 2612 Raw data (stat): 2555 (minisat+) R 2554 29653 29652 0 -1 0 26004 0 0 0 97949 79 0 0 25 0 1 0 422947198 110501888 25982 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 26978 25982 603 41 0 26937 0 vsize: 107912 [startup+989.999 s] Raw data (loadavg): 1.00 0.97 0.91 2/54 2612 Raw data (stat): 2555 (minisat+) R 2554 29653 29652 0 -1 0 26216 0 0 0 98949 79 0 0 25 0 1 0 422947198 111296512 26194 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 27172 26194 603 41 0 27131 0 vsize: 108688 [startup+999.999 s] Raw data (loadavg): 1.00 0.97 0.91 2/54 2612 Raw data (stat): 2555 (minisat+) R 2554 29653 29652 0 -1 0 26461 0 0 0 99948 80 0 0 25 0 1 0 422947198 112361472 26439 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 27432 26439 603 41 0 27391 0 vsize: 109728 [startup+1010 s] Raw data (loadavg): 1.00 0.97 0.91 2/54 2612 Raw data (stat): 2555 (minisat+) R 2554 29653 29652 0 -1 0 26705 0 0 0 100947 81 0 0 25 0 1 0 422947198 113299456 26683 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 27661 26683 603 41 0 27620 0 vsize: 110644 [startup+1020 s] Raw data (loadavg): 1.00 0.97 0.91 2/54 2612 Raw data (stat): 2555 (minisat+) R 2554 29653 29652 0 -1 0 26945 0 0 0 101947 81 0 0 25 0 1 0 422947198 114245632 26923 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 27892 26923 603 41 0 27851 0 vsize: 111568 [startup+1030 s] Raw data (loadavg): 1.00 0.97 0.91 2/54 2612 Raw data (stat): 2555 (minisat+) R 2554 29653 29652 0 -1 0 27186 0 0 0 102946 82 0 0 25 0 1 0 422947198 115187712 27164 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 28122 27164 603 41 0 28081 0 vsize: 112488 [startup+1040 s] Raw data (loadavg): 1.00 0.97 0.91 2/54 2612 Raw data (stat): 2555 (minisat+) R 2554 29653 29652 0 -1 0 27437 0 0 0 103945 84 0 0 25 0 1 0 422947198 116240384 27415 4294967295 134512640 134672761 3221224560 3221223696 134560566 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 28379 27415 603 41 0 28338 0 vsize: 113516 [startup+1050 s] Raw data (loadavg): 1.00 0.97 0.91 2/54 2612 Raw data (stat): 2555 (minisat+) R 2554 29653 29652 0 -1 0 27669 0 0 0 104944 85 0 0 25 0 1 0 422947198 117166080 27647 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 28605 27647 603 41 0 28564 0 vsize: 114420 [startup+1060 s] Raw data (loadavg): 1.00 0.97 0.91 2/54 2612 Raw data (stat): 2555 (minisat+) R 2554 29653 29652 0 -1 0 27916 0 0 0 105944 86 0 0 25 0 1 0 422947198 118235136 27894 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 28866 27894 603 41 0 28825 0 vsize: 115464 [startup+1070 s] Raw data (loadavg): 1.00 0.97 0.91 2/54 2612 Raw data (stat): 2555 (minisat+) R 2554 29653 29652 0 -1 0 28154 0 0 0 106943 87 0 0 25 0 1 0 422947198 119164928 28132 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 29093 28132 603 41 0 29052 0 vsize: 116372 [startup+1080 s] Raw data (loadavg): 1.00 0.97 0.91 2/54 2612 Raw data (stat): 2555 (minisat+) R 2554 29653 29652 0 -1 0 28386 0 0 0 107943 87 0 0 25 0 1 0 422947198 120098816 28364 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 29321 28364 603 41 0 29280 0 vsize: 117284 [startup+1090 s] Raw data (loadavg): 1.00 0.97 0.91 2/54 2612 Raw data (stat): 2555 (minisat+) R 2554 29653 29652 0 -1 0 28630 0 0 0 108942 88 0 0 25 0 1 0 422947198 121167872 28608 4294967295 134512640 134672761 3221224560 3221223664 134560235 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 29582 28608 603 41 0 29541 0 vsize: 118328 [startup+1100 s] Raw data (loadavg): 1.00 0.97 0.91 2/54 2612 Raw data (stat): 2555 (minisat+) R 2554 29653 29652 0 -1 0 28876 0 0 0 109942 89 0 0 25 0 1 0 422947198 122093568 28854 4294967295 134512640 134672761 3221224560 3221223728 134561151 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 29808 28854 603 41 0 29767 0 vsize: 119232 [startup+1110 s] Raw data (loadavg): 1.00 0.97 0.91 2/54 2612 Raw data (stat): 2555 (minisat+) R 2554 29653 29652 0 -1 0 29104 0 0 0 110941 90 0 0 25 0 1 0 422947198 123027456 29082 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 30036 29082 603 41 0 29995 0 vsize: 120144 [startup+1120 s] Raw data (loadavg): 1.00 0.97 0.91 2/54 2612 Raw data (stat): 2555 (minisat+) R 2554 29653 29652 0 -1 0 29311 0 0 0 111941 91 0 0 25 0 1 0 422947198 123961344 29289 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 30264 29289 603 41 0 30223 0 vsize: 121056 [startup+1130 s] Raw data (loadavg): 1.00 0.97 0.91 2/54 2612 Raw data (stat): 2555 (minisat+) R 2554 29653 29652 0 -1 0 29491 0 0 0 112941 91 0 0 25 0 1 0 422947198 124624896 29469 4294967295 134512640 134672761 3221224560 3221223720 134561238 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 30426 29469 603 41 0 30385 0 vsize: 121704 [startup+1140 s] Raw data (loadavg): 1.00 0.97 0.91 2/54 2612 Raw data (stat): 2555 (minisat+) R 2554 29653 29652 0 -1 0 29657 0 0 0 113940 92 0 0 25 0 1 0 422947198 125296640 29635 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 30590 29635 603 41 0 30549 0 vsize: 122360 [startup+1150 s] Raw data (loadavg): 1.00 0.97 0.91 2/54 2612 Raw data (stat): 2555 (minisat+) R 2554 29653 29652 0 -1 0 29832 0 0 0 114940 92 0 0 25 0 1 0 422947198 126099456 29810 4294967295 134512640 134672761 3221224560 3221223728 134560940 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 30786 29810 603 41 0 30745 0 vsize: 123144 [startup+1160 s] Raw data (loadavg): 1.00 0.97 0.91 2/54 2612 Raw data (stat): 2555 (minisat+) R 2554 29653 29652 0 -1 0 30024 0 0 0 115940 93 0 0 25 0 1 0 422947198 126767104 30002 4294967295 134512640 134672761 3221224560 3221223760 134557836 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 30949 30002 603 41 0 30908 0 vsize: 123796 [startup+1170 s] Raw data (loadavg): 1.00 0.97 0.91 2/54 2612 Raw data (stat): 2555 (minisat+) R 2554 29653 29652 0 -1 0 30203 0 0 0 116940 94 0 0 25 0 1 0 422947198 127569920 30181 4294967295 134512640 134672761 3221224560 3221223728 134560920 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 31145 30181 603 41 0 31104 0 vsize: 124580 [startup+1180 s] Raw data (loadavg): 1.00 0.97 0.91 2/54 2612 Raw data (stat): 2555 (minisat+) R 2554 29653 29652 0 -1 0 30417 0 0 0 117939 94 0 0 25 0 1 0 422947198 128372736 30395 4294967295 134512640 134672761 3221224560 3221223728 134560996 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 31341 30395 603 41 0 31300 0 vsize: 125364 [startup+1190 s] Raw data (loadavg): 1.00 0.97 0.91 2/54 2612 Raw data (stat): 2555 (minisat+) R 2554 29653 29652 0 -1 0 30677 0 0 0 118940 94 0 0 25 0 1 0 422947198 129568768 30655 4294967295 134512640 134672761 3221224560 3221223728 134561193 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 31633 30655 603 41 0 31592 0 vsize: 126532 [startup+1200 s] Raw data (loadavg): 1.00 0.97 0.91 2/54 2612 Raw data (stat): 2555 (minisat+) R 2554 29653 29652 0 -1 0 30941 0 0 0 119939 95 0 0 25 0 1 0 422947198 130625536 30919 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 31891 30919 603 41 0 31850 0 vsize: 127564 Maximum CPU time exceeded: sending SIGTERM and SIGKILL [startup+1200.07 s] Raw data (loadavg): 1.00 0.97 0.91 1/54 2612 Raw data (stat): 2555 (minisat+) Z 2554 29653 29652 0 -1 12 30944 0 0 0 119940 101 0 0 25 0 1 0 422947198 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.07 CPU time (s): 1200.41 CPU user time (s): 1199.4 CPU system time (s): 1.01285 CPU usage (%): 100.029 Max. virtual memory (Kb): 127564 #### END WATCHER DATA #### #### BEGIN VERIFIER DATA #### ERROR: no interpretation found ! #### END VERIFIER DATA ####