Name | normalized-opb/web/www.nlsde.buaa.edu.cn/~kexu/benchmarks/frb45-21-opb/normalized-frb45-21-2.opb |
MD5SUM | a931f7e9a55cb6836807387327525e8b |
Bench Category | optimization, small integers (OPTSMALLINT) |
Has Objective Function | YES |
Satisfiable | YES |
(Un)Satisfiability was proved | YES |
Best value of the objective function | -35 |
Optimality of the best value was proved | NO |
Number of terms in the objective function | 945 |
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 | 945 |
Number of bits of the sum of numbers in the objective function | 10 |
Biggest number in a constraint | 1 |
Number of bits of the biggest number in a constraint | 1 |
Biggest sum of numbers in a constraint | 945 |
Number of bits of the biggest sum of numbers | 10 |
Best result obtained on this benchmark | SAT |
Best CPU time to get the best result obtained on this benchmark | 1175.08 |
Number of variables | 945 |
Total number of constraints | 58624 |
Number of constraints which are clauses | 58624 |
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 wulflinc27 THE 2005-04-14 04:43:01 (client local time) PB2005-SCRIPT v4.0 MARKUPS: idlaunch=4842 boxname=wulflinc27 idbench=330 idsolver=13 numberseed=0 MD5SUM SOLVER: MD5SUM BENCH: a931f7e9a55cb6836807387327525e8b /oldhome/oroussel/tmp/wulflinc27/normalized-frb45-21-2.opb REAL COMMAND: minisat+ -w /oldhome/oroussel/tmp/wulflinc27/normalized-frb45-21-2.opb /oldhome/oroussel/tmp/wulflinc27/normalized-frb45-21-2.opb IDLAUNCH: 4842 /proc/cpuinfo: processor : 0 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 3 cpu MHz : 451.169 cache size : 512 KB fdiv_bug : no hlt_bug : no f00f_bug : no coma_bug : no fpu : yes fpu_exception : yes cpuid level : 2 wp : yes flags : fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse bogomips : 888.83 processor : 1 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 3 cpu MHz : 451.169 cache size : 512 KB fdiv_bug : no hlt_bug : no f00f_bug : no coma_bug : no fpu : yes fpu_exception : yes cpuid level : 2 wp : yes flags : fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse bogomips : 899.07 /proc/meminfo: MemTotal: 1034660 kB MemFree: 838352 kB Buffers: 35260 kB Cached: 123896 kB SwapCached: 3160 kB Active: 72512 kB Inactive: 92660 kB HighTotal: 131008 kB HighFree: 3724 kB LowTotal: 903652 kB LowFree: 834628 kB SwapTotal: 2097892 kB SwapFree: 2094732 kB Dirty: 52 kB Writeback: 0 kB Mapped: 6924 kB Slab: 25736 kB Committed_AS: 63488 kB PageTables: 316 kB VmallocTotal: 114680 kB VmallocUsed: 1368 kB VmallocChunk: 113252 kB JOB ENDED THE 2005-04-14 05:03:04 (client local time) WITH STATUS 10 IN 1200.6 SECONDS stats: 4842 7 1200.6 10 #### END LAUNCHER DATA #### #### BEGIN SOLVER DATA #### c Parsing PB file... c Converting 58624 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 | 58624 117248 | 19541 0 0 nan | 0.000 % | c ============================================================================== c [1mFound solution: -31[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost:44290 Base: c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 0 | 150265 331770 | 50088 0 0 nan | 0.000 % | c | 102 | 149621 330304 | 55096 88 622 7.1 | 0.607 % | c | 252 | 147443 325336 | 60606 190 1194 6.3 | 2.665 % | c | 477 | 146061 322176 | 66667 391 3388 8.7 | 3.993 % | c | 814 | 144060 317606 | 73333 669 5363 8.0 | 5.901 % | c | 1322 | 141016 310653 | 80667 1091 8171 7.5 | 8.798 % | c | 2081 | 135191 297257 | 88733 1659 13727 8.3 | 14.603 % | c ============================================================================== c [1mFound solution: -32[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 | 2688 | 128575 281978 | 42858 1966 15940 8.1 | 14.603 % | c | 2788 | 127920 280468 | 47143 2043 16739 8.2 | 22.033 % | c | 2941 | 126198 276502 | 51858 2129 17682 8.3 | 23.867 % | c ============================================================================== c [1mFound solution: -34[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 | 2990 | 126052 276204 | 42017 2174 18075 8.3 | 23.867 % | c | 3090 | 125656 275290 | 46218 2260 18736 8.3 | 24.382 % | c | 3240 | 123976 271367 | 50840 2360 19479 8.3 | 26.119 % | c | 3465 | 120499 263265 | 55924 2462 20435 8.3 | 29.717 % | c | 3802 | 116722 254440 | 61517 2619 22406 8.6 | 33.645 % | c | 4308 | 111011 241223 | 67668 2784 23694 8.5 | 39.566 % | c | 5067 | 106769 231359 | 74435 3278 29019 8.9 | 44.116 % | c | 6206 | 99578 214444 | 81879 4009 36180 9.0 | 51.770 % | c | 7915 | 93818 200995 | 90067 5332 51600 9.7 | 57.992 % | c ============================================================================== c [1mFound solution: -35[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 | 9721 | 85580 181727 | 28526 6194 64671 10.4 | 57.992 % | c | 9821 | 85580 181727 | 31378 6294 65907 10.5 | 67.285 % | c | 9972 | 85006 180378 | 34516 6369 67662 10.6 | 67.920 % | c | 10197 | 83505 176851 | 37968 6440 67749 10.5 | 69.533 % | c | 10534 | 82104 173546 | 41764 6620 69981 10.6 | 71.091 % | c | 11040 | 80937 170801 | 45941 6905 72934 10.6 | 72.416 % | c | 11799 | 78858 165914 | 50535 7322 82563 11.3 | 74.762 % | c | 12938 | 76694 160811 | 55589 7978 112961 14.2 | 77.208 % | c | 14646 | 74490 155630 | 61148 9023 141287 15.7 | 79.669 % | c ============================================================================== c [1mFound solution: -36[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 | 17100 | 73304 152815 | 24434 10923 243146 22.3 | 79.669 % | c | 17200 | 72780 151577 | 26877 10818 242510 22.4 | 81.548 % | c | 17351 | 72437 150772 | 29565 10843 244095 22.5 | 81.944 % | c | 17576 | 72213 150246 | 32521 10962 247834 22.6 | 82.199 % | c | 17913 | 72213 150246 | 35773 11299 262481 23.2 | 82.199 % | c | 18420 | 72195 150203 | 39351 11790 278625 23.6 | 82.221 % | c | 19179 | 71850 149391 | 43286 12421 318824 25.7 | 82.611 % | c | 20319 | 71315 148124 | 47614 13307 359412 27.0 | 83.227 % | c ============================================================================== c [1mFound solution: -37[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 | 21015 | 71365 148253 | 23788 13999 403427 28.8 | 83.227 % | c | 21116 | 71365 148253 | 26166 14100 405386 28.8 | 83.202 % | c | 21266 | 71228 147931 | 28783 14156 408061 28.8 | 83.358 % | c | 21491 | 71228 147931 | 31661 14381 415357 28.9 | 83.358 % | c | 21828 | 71228 147931 | 34828 14718 431812 29.3 | 83.358 % | c | 22334 | 71228 147931 | 38310 15224 461679 30.3 | 83.358 % | c | 23093 | 71202 147871 | 42141 15967 490430 30.7 | 83.383 % | c | 24233 | 71196 147857 | 46356 17097 534309 31.3 | 83.390 % | c ============================================================================== c [1mFound solution: -38[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 0 Base: c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 24862 | 71152 147729 | 23717 17482 548285 31.4 | 83.390 % | c | 24962 | 71152 147729 | 26088 17582 551022 31.3 | 83.416 % | c | 25113 | 71088 147579 | 28697 17700 555556 31.4 | 83.490 % | c | 25338 | 71050 147491 | 31567 17897 563743 31.5 | 83.528 % | c | 25675 | 70918 147182 | 34724 18131 569463 31.4 | 83.675 % | c ============================================================================== c [1mFound solution: -39[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 0 Base: c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 26090 | 70998 147386 | 23666 18546 607889 32.8 | 83.675 % | c | 26190 | 70948 147264 | 26032 18612 608354 32.7 | 83.732 % | c | 26341 | 70876 147090 | 28635 18685 610503 32.7 | 83.824 % | c | 26566 | 70876 147090 | 31499 18910 627342 33.2 | 83.824 % | c | 26905 | 70876 147090 | 34649 19249 641026 33.3 | 83.824 % | c | 27411 | 70659 146586 | 38114 19689 661910 33.6 | 84.056 % | c | 28171 | 70659 146586 | 41925 20449 698680 34.2 | 84.056 % | c | 29310 | 70534 146292 | 46118 21417 756833 35.3 | 84.199 % | c | 31019 | 70435 146059 | 50730 23093 886673 38.4 | 84.316 % | c | 33581 | 70346 145850 | 55803 25497 1002966 39.3 | 84.418 % | c | 37425 | 70340 145836 | 61383 29337 1307865 44.6 | 84.424 % | c | 43192 | 70188 145477 | 67521 34976 1729464 49.4 | 84.596 % | c | 51843 | 70115 145303 | 74274 43385 2460605 56.7 | 84.688 % | c | 64817 | 70115 145303 | 81701 56359 4366303 77.5 | 84.688 % | c | 84278 | 69736 144417 | 89871 75312 6288685 83.5 | 85.114 % | c ============================================================================== c [1mFound solution: -40[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 0 Base: c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 93879 | 69704 144320 | 23234 84811 7521407 88.7 | 85.114 % | c | 93979 | 69704 144320 | 25557 18078 1621853 89.7 | 85.143 % | c | 94129 | 69704 144320 | 28113 18228 1628210 89.3 | 85.143 % | c | 94354 | 69700 144311 | 30924 18452 1635894 88.7 | 85.147 % | c | 94691 | 69700 144311 | 34016 18789 1659233 88.3 | 85.146 % | c | 95197 | 69700 144311 | 37418 19295 1693089 87.7 | 85.147 % | c | 95956 | 69494 143830 | 41160 19917 1734076 87.1 | 85.378 % | c | 97095 | 69494 143830 | 45276 21056 1844300 87.6 | 85.378 % | c | 98805 | 69416 143646 | 49804 22751 1965716 86.4 | 85.471 % | c | 101369 | 69392 143589 | 54784 25305 2217487 87.6 | 85.499 % | c | 105213 | 69277 143309 | 60263 29127 2558867 87.9 | 85.639 % | c | 110980 | 69111 142920 | 66289 34798 3117212 89.6 | 85.817 % | c | 119629 | 69093 142877 | 72918 43440 4235069 97.5 | 85.839 % | c | 132603 | 69093 142877 | 80210 56414 5576869 98.9 | 85.839 % | c | 152064 | 69065 142810 | 88231 75872 7616650 100.4 | 85.874 % | c | 181258 | 69065 142810 | 97054 105066 10024052 95.4 | 85.874 % | c ============================================================================== c [1mFound solution: -41[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 0 Base: c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 191395 | 69106 142911 | 23035 115203 10750465 93.3 | 85.874 % | c | 191495 | 69106 142911 | 25338 20512 1002443 48.9 | 85.846 % | c | 191646 | 69106 142911 | 27872 20663 1011230 48.9 | 85.846 % | c | 191871 | 69106 142911 | 30659 20888 1021380 48.9 | 85.846 % | c | 192209 | 69100 142897 | 33725 21224 1044884 49.2 | 85.853 % | c | 192715 | 69068 142822 | 37098 21721 1076125 49.5 | 85.888 % | c | 193474 | 69064 142813 | 40807 22477 1115946 49.6 | 85.891 % | c | 194613 | 69064 142813 | 44888 23616 1216667 51.5 | 85.891 % | c | 196322 | 69064 142813 | 49377 25325 1336840 52.8 | 85.891 % | c | 198884 | 69064 142813 | 54315 27887 1572706 56.4 | 85.891 % | c | 202730 | 69064 142813 | 59746 31733 1991772 62.8 | 85.891 % | c | 208496 | 68940 142520 | 65721 37419 2526781 67.5 | 86.040 % | c | 217145 | 68894 142413 | 72293 46020 3326724 72.3 | 86.087 % | c | 230120 | 68894 142413 | 79523 58995 4653243 78.9 | 86.088 % | c | 249581 | 68894 142413 | 87475 78456 6260896 79.8 | 86.088 % | c | 278775 | 68888 142399 | 96222 107647 8248566 76.6 | 86.094 % | c | 322565 | 68888 142399 | 105845 45990 2221490 48.3 | 86.094 % | c | 388249 | 68838 142281 | 116429 111662 8760719 78.5 | 86.151 % | c c *** TERMINATED *** s SATISFIABLE v -C945 -C944 -C943 -C942 -C941 -C940 -C939 -C938 -C937 -C936 -C935 -C934 -C933 -C932 -C931 -C930 -C929 C928 -C927 -C926 -C925 -C924 -C923 -C922 -C921 -C920 -C919 -C918 -C917 -C916 -C915 -C914 -C913 -C912 -C911 -C910 -C909 -C908 C907 -C906 -C905 -C904 -C903 -C902 -C901 -C900 -C899 -C898 -C897 C896 -C895 -C894 -C893 -C892 -C891 -C890 -C889 -C888 -C887 -C886 -C885 -C884 -C883 -C882 -C881 -C880 -C879 -C878 -C877 -C876 -C875 -C874 C873 -C872 -C871 -C870 -C869 -C868 -C867 -C866 -C865 -C864 -C863 -C862 -C861 -C860 -C859 C858 -C857 -C856 -C855 -C854 -C853 -C852 -C851 -C850 -C849 -C848 -C847 -C846 -C845 -C844 -C843 -C842 -C841 -C840 -C839 -C838 -C837 -C836 -C835 -C834 -C833 -C832 -C831 -C830 -C829 -C828 -C827 C826 -C825 -C824 -C823 -C822 -C821 -C820 -C819 -C818 -C817 -C816 C815 -C814 -C813 -C812 -C811 -C810 -C809 -C808 -C807 -C806 -C805 -C804 -C803 -C802 -C801 -C800 -C799 -C798 -C797 -C796 C795 -C794 -C793 -C792 -C791 -C790 -C789 -C788 -C787 -C786 -C785 -C784 -C783 -C782 -C781 -C780 -C779 -C778 -C777 -C776 -C775 -C774 -C773 -C772 -C771 -C770 -C769 C768 -C767 -C766 -C765 -C764 -C763 -C762 -C761 -C760 -C759 -C758 -C757 -C756 -C755 -C754 -C753 -C752 -C751 -C750 -C749 -C748 -C747 -C746 -C745 -C744 C743 -C742 -C741 -C740 -C739 -C738 -C737 -C736 -C735 -C734 -C733 -C732 -C731 -C730 -C729 -C728 -C727 C726 -C725 -C724 -C723 -C722 -C721 -C720 -C719 -C718 -C717 -C716 -C715 -C714 -C713 -C712 -C711 -C710 -C709 -C708 -C707 -C706 -C705 -C704 -C703 -C702 -C701 -C700 C699 -C698 -C697 -C696 -C695 -C694 C693 -C692 -C691 -C690 -C689 -C688 -C687 -C686 -C685 -C684 -C683 -C682 -C681 -C680 -C679 -C678 -C677 -C676 -C675 -C674 -C673 -C672 -C671 -C670 -C669 -C668 -C667 -C666 -C665 -C664 -C663 -C662 -C661 -C660 -C659 -C658 -C657 -C656 -C655 C654 -C653 -C652 -C651 -C650 -C649 -C648 -C647 -C646 -C645 -C644 -C643 -C642 -C641 -C640 -C639 C638 -C637 -C636 -C635 -C634 -C633 -C632 -C631 -C630 -C629 -C628 -C627 C626 -C625 -C624 -C623 -C622 -C621 -C620 -C619 -C618 -C617 -C616 -C615 -C614 -C613 -C612 -C611 -C610 -C609 -C608 -C607 -C606 -C605 -C604 -C603 -C602 -C601 -C600 -C599 -C598 -C597 -C596 -C595 -C594 -C593 -C592 -C591 -C590 C589 -C588 -C587 -C586 -C585 -C584 -C583 -C582 -C581 -C580 -C579 -C578 -C577 C576 -C575 -C574 -C573 -C572 -C571 -C570 -C569 -C568 -C567 C566 -C565 -C564 -C563 -C562 -C561 -C560 -C559 -C558 -C557 -C556 -C555 -C554 -C553 -C552 -C551 -C550 -C549 -C548 -C547 -C546 -C545 C544 -C543 -C542 -C541 -C540 -C539 -C538 -C537 -C536 -C535 -C534 -C533 -C532 -C531 -C530 -C529 -C528 -C527 -C526 -C525 -C524 -C523 C522 -C521 -C520 -C519 -C518 -C517 -C516 -C515 -C514 -C513 -C512 -C511 -C510 -C509 -C508 -C507 -C506 -C505 -C504 -C503 -C502 -C501 -C500 -C499 -C498 -C497 -C496 -C495 -C494 C493 -C492 -C491 -C490 -C489 -C488 -C487 -C486 -C485 -C484 -C483 -C482 -C481 -C480 -C479 C478 -C477 -C476 -C475 -C474 -C473 -C472 -C471 -C470 -C469 -C468 -C467 -C466 -C465 -C464 -C463 -C462 -C461 -C460 -C459 -C458 -C457 -C456 -C455 -C454 -C453 -C452 -C451 -C450 -C449 -C448 -C447 -C446 C445 -C444 -C443 -C442 -C441 -C440 -C439 -C438 C437 -C436 -C435 -C434 -C433 -C432 -C431 -C430 -C429 -C428 -C427 -C426 -C425 -C424 -C423 -C422 -C421 -C420 -C419 -C418 -C417 -C416 -C415 -C414 -C413 -C412 C411 -C410 -C409 -C408 -C407 -C406 -C405 -C404 -C403 -C402 -C401 -C400 -C399 -C398 -C397 -C396 -C395 -C394 -C393 -C392 C391 -C390 -C389 -C388 -C387 -C386 -C385 -C384 -C383 -C382 -C381 -C380 -C379 -C378 -C377 -C376 -C375 -C374 -C373 -C372 -C371 -C370 -C369 -C368 -C367 -C366 -C365 -C364 -C363 -C362 -C361 -C360 -C359 -C358 -C357 -C356 -C355 -C354 -C353 -C352 -C351 -C350 -C349 -C348 -C347 -C346 -C345 -C344 -C343 -C342 -C341 -C340 -C339 -C338 C337 -C336 -C335 C334 -C333 -C332 -C331 -C330 -C329 -C328 -C327 -C326 -C325 -C324 -C323 -C322 -C321 -C320 -C319 -C318 -C317 -C316 -C315 -C314 -C313 -C312 -C311 -C310 -C309 -C308 -C307 -C306 -C305 -C304 -C303 C302 -C301 -C300 -C299 -C298 -C297 -C296 -C295 -C294 -C293 -C292 -C291 -C290 -C289 -C288 -C287 C286 -C285 -C284 -C283 -C282 -C281 -C280 -C279 -C278 -C277 -C276 -C275 -C274 C273 -C272 -C271 -C270 -C269 -C268 -C267 -C266 -C265 -C#### 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 25210 Raw data (stat): 25210 (runsolver) R 25209 18865 18864 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 481797659 1052672 99 4294967295 134512640 135381576 3221224464 3221219708 135158418 0 2147483391 7 90112 0 0 0 17 0 0 0 Raw data (statm): 257 99 215 215 0 42 0 vsize: 1028 [startup+9.99954 s] Raw data (loadavg): 0.87 0.94 0.90 2/54 25210 Raw data (stat): 25210 (minisat+) R 25209 18865 18864 0 -1 0 3820 0 0 0 986 11 0 0 25 0 1 0 481797659 17629184 3798 4294967295 134512640 134672761 3221224560 3221223732 134556598 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 4304 3798 603 41 0 4263 0 vsize: 17216 [startup+20.0007 s] Raw data (loadavg): 0.89 0.94 0.90 2/54 25210 Raw data (stat): 25210 (minisat+) R 25209 18865 18864 0 -1 0 3826 0 0 0 1986 11 0 0 25 0 1 0 481797659 17629184 3804 4294967295 134512640 134672761 3221224560 3221223712 134561244 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 4304 3804 603 41 0 4263 0 vsize: 17216 [startup+30.0015 s] Raw data (loadavg): 0.90 0.94 0.90 2/54 25210 Raw data (stat): 25210 (minisat+) R 25209 18865 18864 0 -1 0 3943 0 0 0 2985 12 0 0 25 0 1 0 481797659 18513920 3921 4294967295 134512640 134672761 3221224560 3221223760 134561972 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 4520 3921 603 41 0 4479 0 vsize: 18080 [startup+40.002 s] Raw data (loadavg): 0.92 0.94 0.90 2/54 25210 Raw data (stat): 25210 (minisat+) R 25209 18865 18864 0 -1 0 3943 0 0 0 3985 12 0 0 25 0 1 0 481797659 18513920 3921 4294967295 134512640 134672761 3221224560 3221223732 134556598 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 4520 3921 603 41 0 4479 0 vsize: 18080 [startup+50.0031 s] Raw data (loadavg): 0.93 0.94 0.90 2/54 25210 Raw data (stat): 25210 (minisat+) R 25209 18865 18864 0 -1 0 3945 0 0 0 4986 12 0 0 25 0 1 0 481797659 18513920 3923 4294967295 134512640 134672761 3221224560 3221223664 134560158 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 4520 3923 603 41 0 4479 0 vsize: 18080 [startup+60.0031 s] Raw data (loadavg): 0.94 0.95 0.90 2/54 25210 Raw data (stat): 25210 (minisat+) R 25209 18865 18864 0 -1 0 4108 0 0 0 5985 13 0 0 25 0 1 0 481797659 19103744 4086 4294967295 134512640 134672761 3221224560 3221223732 134556643 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 4664 4086 603 41 0 4623 0 vsize: 18656 [startup+70.0034 s] Raw data (loadavg): 0.95 0.95 0.91 2/54 25210 Raw data (stat): 25210 (minisat+) R 25209 18865 18864 0 -1 0 4490 0 0 0 6984 14 0 0 25 0 1 0 481797659 20709376 4468 4294967295 134512640 134672761 3221224560 3221223732 134556602 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 5056 4468 603 41 0 5015 0 vsize: 20224 [startup+80.0035 s] Raw data (loadavg): 0.96 0.95 0.91 2/54 25210 Raw data (stat): 25210 (minisat+) R 25209 18865 18864 0 -1 0 4912 0 0 0 7983 15 0 0 25 0 1 0 481797659 22425600 4890 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 5475 4890 603 41 0 5434 0 vsize: 21900 [startup+90.0046 s] Raw data (loadavg): 0.96 0.95 0.91 2/54 25210 Raw data (stat): 25210 (minisat+) R 25209 18865 18864 0 -1 0 5451 0 0 0 8981 17 0 0 25 0 1 0 481797659 24576000 5429 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 6000 5429 603 41 0 5959 0 vsize: 24000 [startup+100.005 s] Raw data (loadavg): 0.97 0.95 0.91 2/54 25210 Raw data (stat): 25210 (minisat+) R 25209 18865 18864 0 -1 0 6019 0 0 0 9979 19 0 0 25 0 1 0 481797659 27111424 5997 4294967295 134512640 134672761 3221224560 3221223664 134560054 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 6619 5997 603 41 0 6578 0 vsize: 26476 [startup+110.005 s] Raw data (loadavg): 0.97 0.95 0.91 2/54 25210 Raw data (stat): 25210 (minisat+) R 25209 18865 18864 0 -1 0 6517 0 0 0 10978 20 0 0 25 0 1 0 481797659 29122560 6495 4294967295 134512640 134672761 3221224560 3221223728 134560929 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 7110 6495 603 41 0 7069 0 vsize: 28440 [startup+120.006 s] Raw data (loadavg): 0.98 0.95 0.91 2/54 25210 Raw data (stat): 25210 (minisat+) R 25209 18865 18864 0 -1 0 7046 0 0 0 11976 22 0 0 25 0 1 0 481797659 31256576 7024 4294967295 134512640 134672761 3221224560 3221223728 134561218 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 7631 7024 603 41 0 7590 0 vsize: 30524 [startup+130.006 s] Raw data (loadavg): 0.98 0.95 0.91 2/54 25210 Raw data (stat): 25210 (minisat+) R 25209 18865 18864 0 -1 0 7659 0 0 0 12975 24 0 0 25 0 1 0 481797659 33669120 7637 4294967295 134512640 134672761 3221224560 3221223728 134561207 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 8220 7637 603 41 0 8179 0 vsize: 32880 [startup+140.006 s] Raw data (loadavg): 0.98 0.95 0.91 2/54 25210 Raw data (stat): 25210 (minisat+) R 25209 18865 18864 0 -1 0 8252 0 0 0 13973 25 0 0 25 0 1 0 481797659 36188160 8230 4294967295 134512640 134672761 3221224560 3221223664 134559925 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 8835 8230 603 41 0 8794 0 vsize: 35340 [startup+150.007 s] Raw data (loadavg): 0.98 0.95 0.91 2/54 25210 Raw data (stat): 25210 (minisat+) R 25209 18865 18864 0 -1 0 8711 0 0 0 14972 27 0 0 25 0 1 0 481797659 38060032 8689 4294967295 134512640 134672761 3221224560 3221223728 134560937 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 9292 8689 603 41 0 9251 0 vsize: 37168 [startup+160.007 s] Raw data (loadavg): 0.99 0.96 0.91 2/54 25210 Raw data (stat): 25210 (minisat+) R 25209 18865 18864 0 -1 0 9143 0 0 0 15971 28 0 0 25 0 1 0 481797659 39792640 9121 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 9715 9121 603 41 0 9674 0 vsize: 38860 [startup+170.007 s] Raw data (loadavg): 0.99 0.96 0.91 2/54 25210 Raw data (stat): 25210 (minisat+) R 25209 18865 18864 0 -1 0 9553 0 0 0 16970 29 0 0 25 0 1 0 481797659 41394176 9531 4294967295 134512640 134672761 3221224560 3221223700 134560556 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 10106 9531 603 41 0 10065 0 vsize: 40424 [startup+180.014 s] Raw data (loadavg): 0.99 0.96 0.91 2/54 25210 Raw data (stat): 25210 (minisat+) R 25209 18865 18864 0 -1 0 9980 0 0 0 17970 30 0 0 25 0 1 0 481797659 43397120 9958 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 10595 9958 603 41 0 10554 0 vsize: 42380 [startup+190.02 s] Raw data (loadavg): 0.99 0.96 0.91 2/54 25210 Raw data (stat): 25210 (minisat+) R 25209 18865 18864 0 -1 0 10225 0 0 0 18970 30 0 0 25 0 1 0 481797659 44474368 10203 4294967295 134512640 134672761 3221224560 3221223744 134559607 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 10858 10203 603 41 0 10817 0 vsize: 43432 [startup+200.019 s] Raw data (loadavg): 0.99 0.96 0.91 2/54 25210 Raw data (stat): 25210 (minisat+) R 25209 18865 18864 0 -1 0 10650 0 0 0 19969 31 0 0 25 0 1 0 481797659 46211072 10628 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 11282 10628 603 41 0 11241 0 vsize: 45128 [startup+210.019 s] Raw data (loadavg): 0.99 0.96 0.91 2/54 25210 Raw data (stat): 25210 (minisat+) R 25209 18865 18864 0 -1 0 11058 0 0 0 20968 33 0 0 25 0 1 0 481797659 47808512 11036 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 11672 11036 603 41 0 11631 0 vsize: 46688 [startup+220.02 s] Raw data (loadavg): 0.99 0.96 0.91 2/54 25210 Raw data (stat): 25210 (minisat+) R 25209 18865 18864 0 -1 0 11437 0 0 0 21967 34 0 0 25 0 1 0 481797659 49278976 11415 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 12031 11415 603 41 0 11990 0 vsize: 48124 [startup+230.02 s] Raw data (loadavg): 0.99 0.96 0.91 2/54 25210 Raw data (stat): 25210 (minisat+) R 25209 18865 18864 0 -1 0 11824 0 0 0 22967 35 0 0 25 0 1 0 481797659 50880512 11802 4294967295 134512640 134672761 3221224560 3221223728 134561229 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 12422 11802 603 41 0 12381 0 vsize: 49688 [startup+240.021 s] Raw data (loadavg): 0.99 0.96 0.91 2/54 25210 Raw data (stat): 25210 (minisat+) R 25209 18865 18864 0 -1 0 11969 0 0 0 23966 35 0 0 25 0 1 0 481797659 51466240 11947 4294967295 134512640 134672761 3221224560 3221223696 134565045 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 12565 11947 603 41 0 12524 0 vsize: 50260 [startup+250.02 s] Raw data (loadavg): 0.99 0.96 0.91 2/54 25210 Raw data (stat): 25210 (minisat+) R 25209 18865 18864 0 -1 0 11969 0 0 0 24966 35 0 0 25 0 1 0 481797659 51466240 11947 4294967295 134512640 134672761 3221224560 3221223728 134561406 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 12565 11947 603 41 0 12524 0 vsize: 50260 [startup+260.02 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 25210 Raw data (stat): 25210 (minisat+) R 25209 18865 18864 0 -1 0 11969 0 0 0 25966 35 0 0 25 0 1 0 481797659 51466240 11947 4294967295 134512640 134672761 3221224560 3221223696 134565096 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 12565 11947 603 41 0 12524 0 vsize: 50260 [startup+270.021 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 25210 Raw data (stat): 25210 (minisat+) R 25209 18865 18864 0 -1 0 11969 0 0 0 26967 35 0 0 25 0 1 0 481797659 51466240 11947 4294967295 134512640 134672761 3221224560 3221223728 134560996 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 12565 11947 603 41 0 12524 0 vsize: 50260 [startup+280.021 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 25210 Raw data (stat): 25210 (minisat+) R 25209 18865 18864 0 -1 0 11969 0 0 0 27967 35 0 0 25 0 1 0 481797659 51466240 11947 4294967295 134512640 134672761 3221224560 3221223728 134560909 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 12565 11947 603 41 0 12524 0 vsize: 50260 [startup+290.022 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 25210 Raw data (stat): 25210 (minisat+) R 25209 18865 18864 0 -1 0 11969 0 0 0 28967 35 0 0 25 0 1 0 481797659 51466240 11947 4294967295 134512640 134672761 3221224560 3221223696 134560642 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 12565 11947 603 41 0 12524 0 vsize: 50260 [startup+300.022 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 25210 Raw data (stat): 25210 (minisat+) R 25209 18865 18864 0 -1 0 11969 0 0 0 29967 35 0 0 25 0 1 0 481797659 51466240 11947 4294967295 134512640 134672761 3221224560 3221223664 134560402 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 12565 11947 603 41 0 12524 0 vsize: 50260 [startup+310.021 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 25210 Raw data (stat): 25210 (minisat+) R 25209 18865 18864 0 -1 0 11969 0 0 0 30967 35 0 0 25 0 1 0 481797659 51466240 11947 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 12565 11947 603 41 0 12524 0 vsize: 50260 [startup+320.022 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 25210 Raw data (stat): 25210 (minisat+) R 25209 18865 18864 0 -1 0 11969 0 0 0 31967 35 0 0 25 0 1 0 481797659 51466240 11947 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 12565 11947 603 41 0 12524 0 vsize: 50260 [startup+330.023 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 25210 Raw data (stat): 25210 (minisat+) R 25209 18865 18864 0 -1 0 11969 0 0 0 32968 35 0 0 25 0 1 0 481797659 51466240 11947 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 12565 11947 603 41 0 12524 0 vsize: 50260 [startup+340.024 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 25210 Raw data (stat): 25210 (minisat+) R 25209 18865 18864 0 -1 0 11969 0 0 0 33968 35 0 0 25 0 1 0 481797659 51466240 11947 4294967295 134512640 134672761 3221224560 3221223664 134560293 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 12565 11947 603 41 0 12524 0 vsize: 50260 [startup+350.024 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 25210 Raw data (stat): 25210 (minisat+) R 25209 18865 18864 0 -1 0 11969 0 0 0 34968 35 0 0 25 0 1 0 481797659 51466240 11947 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 12565 11947 603 41 0 12524 0 vsize: 50260 [startup+360.023 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 25210 Raw data (stat): 25210 (minisat+) R 25209 18865 18864 0 -1 0 11969 0 0 0 35968 35 0 0 25 0 1 0 481797659 51466240 11947 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 12565 11947 603 41 0 12524 0 vsize: 50260 [startup+370.024 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 25210 Raw data (stat): 25210 (minisat+) R 25209 18865 18864 0 -1 0 11969 0 0 0 36968 35 0 0 25 0 1 0 481797659 51466240 11947 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 12565 11947 603 41 0 12524 0 vsize: 50260 [startup+380.024 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 25210 Raw data (stat): 25210 (minisat+) R 25209 18865 18864 0 -1 0 12223 0 0 0 37968 36 0 0 25 0 1 0 481797659 52527104 12201 4294967295 134512640 134672761 3221224560 3221223516 1075350517 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 12824 12201 603 41 0 12783 0 vsize: 51296 [startup+390.025 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 25210 Raw data (stat): 25210 (minisat+) R 25209 18865 18864 0 -1 0 12534 0 0 0 38968 37 0 0 25 0 1 0 481797659 53850112 12512 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 13147 12512 603 41 0 13106 0 vsize: 52588 [startup+400.024 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 25210 Raw data (stat): 25210 (minisat+) R 25209 18865 18864 0 -1 0 12823 0 0 0 39967 38 0 0 25 0 1 0 481797659 55037952 12801 4294967295 134512640 134672761 3221224560 3221223664 134559974 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 13437 12801 603 41 0 13396 0 vsize: 53748 [startup+410.025 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 25210 Raw data (stat): 25210 (minisat+) R 25209 18865 18864 0 -1 0 13064 0 0 0 40967 38 0 0 25 0 1 0 481797659 55963648 13042 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 13663 13042 603 41 0 13622 0 vsize: 54652 [startup+420.025 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 25210 Raw data (stat): 25210 (minisat+) R 25209 18865 18864 0 -1 0 13348 0 0 0 41966 38 0 0 25 0 1 0 481797659 57147392 13326 4294967295 134512640 134672761 3221224560 3221223728 134561205 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 13952 13326 603 41 0 13911 0 vsize: 55808 [startup+430.026 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 25210 Raw data (stat): 25210 (minisat+) R 25209 18865 18864 0 -1 0 13609 0 0 0 42966 39 0 0 25 0 1 0 481797659 58212352 13587 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 14212 13587 603 41 0 14171 0 vsize: 56848 [startup+440.027 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 25210 Raw data (stat): 25210 (minisat+) R 25209 18865 18864 0 -1 0 13831 0 0 0 43966 40 0 0 25 0 1 0 481797659 59142144 13809 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 14439 13809 603 41 0 14398 0 vsize: 57756 [startup+450.027 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 25210 Raw data (stat): 25210 (minisat+) R 25209 18865 18864 0 -1 0 14052 0 0 0 44965 41 0 0 25 0 1 0 481797659 60067840 14030 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 14665 14030 603 41 0 14624 0 vsize: 58660 [startup+460.026 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 25210 Raw data (stat): 25210 (minisat+) R 25209 18865 18864 0 -1 0 14311 0 0 0 45964 41 0 0 25 0 1 0 481797659 61120512 14289 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 14922 14289 603 41 0 14881 0 vsize: 59688 [startup+470.027 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 25210 Raw data (stat): 25210 (minisat+) R 25209 18865 18864 0 -1 0 14526 0 0 0 46964 42 0 0 25 0 1 0 481797659 61911040 14504 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 15115 14504 603 41 0 15074 0 vsize: 60460 [startup+480.026 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 25210 Raw data (stat): 25210 (minisat+) R 25209 18865 18864 0 -1 0 14692 0 0 0 47964 42 0 0 25 0 1 0 481797659 62574592 14670 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 15277 14670 603 41 0 15236 0 vsize: 61108 [startup+490.027 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 25210 Raw data (stat): 25210 (minisat+) R 25209 18865 18864 0 -1 0 14870 0 0 0 48963 43 0 0 25 0 1 0 481797659 63365120 14848 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 15470 14848 603 41 0 15429 0 vsize: 61880 [startup+500.027 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 25210 Raw data (stat): 25210 (minisat+) R 25209 18865 18864 0 -1 0 15077 0 0 0 49962 44 0 0 25 0 1 0 481797659 64159744 15055 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 15664 15055 603 41 0 15623 0 vsize: 62656 [startup+510.027 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 25210 Raw data (stat): 25210 (minisat+) R 25209 18865 18864 0 -1 0 15283 0 0 0 50962 45 0 0 25 0 1 0 481797659 64958464 15261 4294967295 134512640 134672761 3221224560 3221223728 134560909 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 15859 15261 603 41 0 15818 0 vsize: 63436 [startup+520.028 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 25210 Raw data (stat): 25210 (minisat+) R 25209 18865 18864 0 -1 0 15453 0 0 0 51961 46 0 0 25 0 1 0 481797659 65748992 15431 4294967295 134512640 134672761 3221224560 3221223728 134561025 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 16052 15431 603 41 0 16011 0 vsize: 64208 [startup+530.028 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 25210 Raw data (stat): 25210 (minisat+) R 25209 18865 18864 0 -1 0 15664 0 0 0 52961 46 0 0 25 0 1 0 481797659 66502656 15642 4294967295 134512640 134672761 3221224560 3221223664 134554671 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 16236 15642 603 41 0 16195 0 vsize: 64944 [startup+540.028 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 25210 Raw data (stat): 25210 (minisat+) R 25209 18865 18864 0 -1 0 15664 0 0 0 53961 46 0 0 25 0 1 0 481797659 66502656 15642 4294967295 134512640 134672761 3221224560 3221223664 134559818 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 16236 15642 603 41 0 16195 0 vsize: 64944 [startup+550.028 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 25210 Raw data (stat): 25210 (minisat+) R 25209 18865 18864 0 -1 0 15664 0 0 0 54961 46 0 0 25 0 1 0 481797659 66502656 15642 4294967295 134512640 134672761 3221224560 3221223728 134561164 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 16236 15642 603 41 0 16195 0 vsize: 64944 [startup+560.029 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 25210 Raw data (stat): 25210 (minisat+) R 25209 18865 18864 0 -1 0 15664 0 0 0 55961 46 0 0 25 0 1 0 481797659 66502656 15642 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 16236 15642 603 41 0 16195 0 vsize: 64944 [startup+570.029 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 25210 Raw data (stat): 25210 (minisat+) R 25209 18865 18864 0 -1 0 15664 0 0 0 56962 46 0 0 25 0 1 0 481797659 66502656 15642 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 16236 15642 603 41 0 16195 0 vsize: 64944 [startup+580.029 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 25210 Raw data (stat): 25210 (minisat+) R 25209 18865 18864 0 -1 0 15664 0 0 0 57962 46 0 0 25 0 1 0 481797659 66502656 15642 4294967295 134512640 134672761 3221224560 3221223664 134560235 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 16236 15642 603 41 0 16195 0 vsize: 64944 [startup+590.029 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 25210 Raw data (stat): 25210 (minisat+) R 25209 18865 18864 0 -1 0 15664 0 0 0 58962 46 0 0 25 0 1 0 481797659 66502656 15642 4294967295 134512640 134672761 3221224560 3221223728 134560852 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 16236 15642 603 41 0 16195 0 vsize: 64944 [startup+600.03 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 25210 Raw data (stat): 25210 (minisat+) R 25209 18865 18864 0 -1 0 15664 0 0 0 59962 46 0 0 25 0 1 0 481797659 66502656 15642 4294967295 134512640 134672761 3221224560 3221223728 134560892 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 16236 15642 603 41 0 16195 0 vsize: 64944 [startup+610.03 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 25210 Raw data (stat): 25210 (minisat+) R 25209 18865 18864 0 -1 0 15664 0 0 0 60962 46 0 0 25 0 1 0 481797659 66502656 15642 4294967295 134512640 134672761 3221224560 3221223728 134561190 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 16236 15642 603 41 0 16195 0 vsize: 64944 [startup+620.03 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 25210 Raw data (stat): 25210 (minisat+) R 25209 18865 18864 0 -1 0 15664 0 0 0 61963 46 0 0 25 0 1 0 481797659 66502656 15642 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 16236 15642 603 41 0 16195 0 vsize: 64944 [startup+630.031 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 25210 Raw data (stat): 25210 (minisat+) R 25209 18865 18864 0 -1 0 15664 0 0 0 62963 46 0 0 25 0 1 0 481797659 66502656 15642 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 16236 15642 603 41 0 16195 0 vsize: 64944 [startup+640.031 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 25210 Raw data (stat): 25210 (minisat+) R 25209 18865 18864 0 -1 0 15664 0 0 0 63963 46 0 0 25 0 1 0 481797659 66502656 15642 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 16236 15642 603 41 0 16195 0 vsize: 64944 [startup+650.031 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 25210 Raw data (stat): 25210 (minisat+) R 25209 18865 18864 0 -1 0 15664 0 0 0 64963 46 0 0 25 0 1 0 481797659 66502656 15642 4294967295 134512640 134672761 3221224560 3221223712 134565092 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 16236 15642 603 41 0 16195 0 vsize: 64944 [startup+660.031 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 25210 Raw data (stat): 25210 (minisat+) R 25209 18865 18864 0 -1 0 15664 0 0 0 65963 46 0 0 25 0 1 0 481797659 66502656 15642 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 16236 15642 603 41 0 16195 0 vsize: 64944 [startup+670.032 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 25210 Raw data (stat): 25210 (minisat+) R 25209 18865 18864 0 -1 0 15664 0 0 0 66964 46 0 0 25 0 1 0 481797659 66502656 15642 4294967295 134512640 134672761 3221224560 3221223664 134560198 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 16236 15642 603 41 0 16195 0 vsize: 64944 [startup+680.032 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 25210 Raw data (stat): 25210 (minisat+) R 25209 18865 18864 0 -1 0 15664 0 0 0 67964 46 0 0 25 0 1 0 481797659 66502656 15642 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 16236 15642 603 41 0 16195 0 vsize: 64944 [startup+690.034 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 25210 Raw data (stat): 25210 (minisat+) R 25209 18865 18864 0 -1 0 15664 0 0 0 68964 46 0 0 25 0 1 0 481797659 66502656 15642 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 16236 15642 603 41 0 16195 0 vsize: 64944 [startup+700.034 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 25210 Raw data (stat): 25210 (minisat+) R 25209 18865 18864 0 -1 0 15664 0 0 0 69964 46 0 0 25 0 1 0 481797659 66502656 15642 4294967295 134512640 134672761 3221224560 3221223664 134560350 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 16236 15642 603 41 0 16195 0 vsize: 64944 [startup+710.034 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 25210 Raw data (stat): 25210 (minisat+) R 25209 18865 18864 0 -1 0 15664 0 0 0 70965 46 0 0 25 0 1 0 481797659 66502656 15642 4294967295 134512640 134672761 3221224560 3221223728 134561167 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 16236 15642 603 41 0 16195 0 vsize: 64944 [startup+720.034 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 25210 Raw data (stat): 25210 (minisat+) R 25209 18865 18864 0 -1 0 15664 0 0 0 71965 46 0 0 25 0 1 0 481797659 66502656 15642 4294967295 134512640 134672761 3221224560 3221223728 134561198 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 16236 15642 603 41 0 16195 0 vsize: 64944 [startup+730.035 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 25210 Raw data (stat): 25210 (minisat+) R 25209 18865 18864 0 -1 0 15665 0 0 0 72965 46 0 0 25 0 1 0 481797659 66502656 15643 4294967295 134512640 134672761 3221224560 3221223664 134560196 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 16236 15643 603 41 0 16195 0 vsize: 64944 [startup+740.035 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 25210 Raw data (stat): 25210 (minisat+) R 25209 18865 18864 0 -1 0 15665 0 0 0 73965 46 0 0 25 0 1 0 481797659 66502656 15643 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 16236 15643 603 41 0 16195 0 vsize: 64944 [startup+750.035 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 25210 Raw data (stat): 25210 (minisat+) R 25209 18865 18864 0 -1 0 15665 0 0 0 74965 46 0 0 25 0 1 0 481797659 66502656 15643 4294967295 134512640 134672761 3221224560 3221223696 134560634 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 16236 15643 603 41 0 16195 0 vsize: 64944 [startup+760.035 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 25210 Raw data (stat): 25210 (minisat+) R 25209 18865 18864 0 -1 0 15665 0 0 0 75965 46 0 0 25 0 1 0 481797659 66502656 15643 4294967295 134512640 134672761 3221224560 3221223696 134560577 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 16236 15643 603 41 0 16195 0 vsize: 64944 [startup+770.036 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 25210 Raw data (stat): 25210 (minisat+) R 25209 18865 18864 0 -1 0 15665 0 0 0 76966 46 0 0 25 0 1 0 481797659 66502656 15643 4294967295 134512640 134672761 3221224560 3221223760 134557828 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 16236 15643 603 41 0 16195 0 vsize: 64944 [startup+780.036 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 25210 Raw data (stat): 25210 (minisat+) R 25209 18865 18864 0 -1 0 15665 0 0 0 77966 46 0 0 25 0 1 0 481797659 66502656 15643 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 16236 15643 603 41 0 16195 0 vsize: 64944 [startup+790.037 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 25210 Raw data (stat): 25210 (minisat+) R 25209 18865 18864 0 -1 0 15665 0 0 0 78966 46 0 0 25 0 1 0 481797659 66502656 15643 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 16236 15643 603 41 0 16195 0 vsize: 64944 [startup+800.037 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 25210 Raw data (stat): 25210 (minisat+) R 25209 18865 18864 0 -1 0 15665 0 0 0 79966 46 0 0 25 0 1 0 481797659 66502656 15643 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 16236 15643 603 41 0 16195 0 vsize: 64944 [startup+810.037 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 25210 Raw data (stat): 25210 (minisat+) R 25209 18865 18864 0 -1 0 15667 0 0 0 80966 46 0 0 25 0 1 0 481797659 66502656 15645 4294967295 134512640 134672761 3221224560 3221223728 134561151 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 16236 15645 603 41 0 16195 0 vsize: 64944 [startup+820.038 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 25210 Raw data (stat): 25210 (minisat+) R 25209 18865 18864 0 -1 0 15669 0 0 0 81967 46 0 0 25 0 1 0 481797659 66502656 15647 4294967295 134512640 134672761 3221224560 3221223728 134561008 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 16236 15647 603 41 0 16195 0 vsize: 64944 [startup+830.039 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 25210 Raw data (stat): 25210 (minisat+) R 25209 18865 18864 0 -1 0 15671 0 0 0 82967 46 0 0 25 0 1 0 481797659 66502656 15649 4294967295 134512640 134672761 3221224560 3221223728 134560903 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 16236 15649 603 41 0 16195 0 vsize: 64944 [startup+840.04 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 25210 Raw data (stat): 25210 (minisat+) R 25209 18865 18864 0 -1 0 15673 0 0 0 83967 46 0 0 25 0 1 0 481797659 66502656 15651 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 16236 15651 603 41 0 16195 0 vsize: 64944 [startup+850.04 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 25210 Raw data (stat): 25210 (minisat+) R 25209 18865 18864 0 -1 0 15675 0 0 0 84967 46 0 0 25 0 1 0 481797659 66494464 15653 4294967295 134512640 134672761 3221224560 3221223664 134554662 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 16234 15653 603 41 0 16193 0 vsize: 64936 [startup+860.039 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 25210 Raw data (stat): 25210 (minisat+) R 25209 18865 18864 0 -1 0 15675 0 0 0 85967 46 0 0 25 0 1 0 481797659 66494464 15653 4294967295 134512640 134672761 3221224560 3221223728 134560852 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 16234 15653 603 41 0 16193 0 vsize: 64936 [startup+870.04 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 25210 Raw data (stat): 25210 (minisat+) R 25209 18865 18864 0 -1 0 15675 0 0 0 86968 46 0 0 25 0 1 0 481797659 66494464 15653 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 16234 15653 603 41 0 16193 0 vsize: 64936 [startup+880.04 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 25210 Raw data (stat): 25210 (minisat+) R 25209 18865 18864 0 -1 0 15675 0 0 0 87968 46 0 0 25 0 1 0 481797659 66494464 15653 4294967295 134512640 134672761 3221224560 3221223760 134557849 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 16234 15653 603 41 0 16193 0 vsize: 64936 [startup+890.041 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 25210 Raw data (stat): 25210 (minisat+) R 25209 18865 18864 0 -1 0 15675 0 0 0 88968 46 0 0 25 0 1 0 481797659 66494464 15653 4294967295 134512640 134672761 3221224560 3221223728 134561151 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 16234 15653 603 41 0 16193 0 vsize: 64936 [startup+900.042 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 25210 Raw data (stat): 25210 (minisat+) R 25209 18865 18864 0 -1 0 15675 0 0 0 89968 46 0 0 25 0 1 0 481797659 66494464 15653 4294967295 134512640 134672761 3221224560 3221223744 134559424 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 16234 15653 603 41 0 16193 0 vsize: 64936 [startup+910.042 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 25210 Raw data (stat): 25210 (minisat+) R 25209 18865 18864 0 -1 0 15675 0 0 0 90968 46 0 0 25 0 1 0 481797659 66494464 15653 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 16234 15653 603 41 0 16193 0 vsize: 64936 [startup+920.042 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 25210 Raw data (stat): 25210 (minisat+) R 25209 18865 18864 0 -1 0 15675 0 0 0 91968 46 0 0 25 0 1 0 481797659 66494464 15653 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 16234 15653 603 41 0 16193 0 vsize: 64936 [startup+930.042 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 25210 Raw data (stat): 25210 (minisat+) R 25209 18865 18864 0 -1 0 15675 0 0 0 92968 46 0 0 25 0 1 0 481797659 66494464 15653 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 16234 15653 603 41 0 16193 0 vsize: 64936 [startup+940.043 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 25210 Raw data (stat): 25210 (minisat+) R 25209 18865 18864 0 -1 0 15675 0 0 0 93968 46 0 0 25 0 1 0 481797659 66494464 15653 4294967295 134512640 134672761 3221224560 3221223728 134560996 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 16234 15653 603 41 0 16193 0 vsize: 64936 [startup+950.043 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 25210 Raw data (stat): 25210 (minisat+) R 25209 18865 18864 0 -1 0 15675 0 0 0 94968 46 0 0 25 0 1 0 481797659 66494464 15653 4294967295 134512640 134672761 3221224560 3221223472 1075352323 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 16234 15653 603 41 0 16193 0 vsize: 64936 [startup+960.043 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 25210 Raw data (stat): 25210 (minisat+) R 25209 18865 18864 0 -1 0 15675 0 0 0 95968 46 0 0 25 0 1 0 481797659 66494464 15653 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 16234 15653 603 41 0 16193 0 vsize: 64936 [startup+970.044 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 25210 Raw data (stat): 25210 (minisat+) R 25209 18865 18864 0 -1 0 15675 0 0 0 96969 46 0 0 25 0 1 0 481797659 66494464 15653 4294967295 134512640 134672761 3221224560 3221223728 134560892 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 16234 15653 603 41 0 16193 0 vsize: 64936 [startup+980.044 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 25210 Raw data (stat): 25210 (minisat+) R 25209 18865 18864 0 -1 0 15675 0 0 0 97969 46 0 0 25 0 1 0 481797659 66494464 15653 4294967295 134512640 134672761 3221224560 3221223728 134560855 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 16234 15653 603 41 0 16193 0 vsize: 64936 [startup+990.045 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 25210 Raw data (stat): 25210 (minisat+) R 25209 18865 18864 0 -1 0 15675 0 0 0 98969 46 0 0 25 0 1 0 481797659 66494464 15653 4294967295 134512640 134672761 3221224560 3221223728 134561229 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 16234 15653 603 41 0 16193 0 vsize: 64936 [startup+1000.05 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 25210 Raw data (stat): 25210 (minisat+) R 25209 18865 18864 0 -1 0 15675 0 0 0 99969 46 0 0 25 0 1 0 481797659 66494464 15653 4294967295 134512640 134672761 3221224560 3221223684 134566031 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 16234 15653 603 41 0 16193 0 vsize: 64936 [startup+1010.05 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 25210 Raw data (stat): 25210 (minisat+) R 25209 18865 18864 0 -1 0 15675 0 0 0 100969 46 0 0 25 0 1 0 481797659 66494464 15653 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 16234 15653 603 41 0 16193 0 vsize: 64936 [startup+1020.16 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 25210 Raw data (stat): 25210 (minisat+) R 25209 18865 18864 0 -1 0 15675 0 0 0 101981 46 0 0 25 0 1 0 481797659 66494464 15653 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 16234 15653 603 41 0 16193 0 vsize: 64936 [startup+1030.3 s] Raw data (loadavg): 1.07 0.99 0.91 2/56 25250 Raw data (stat): 25210 (minisat+) R 25209 18865 18864 0 -1 0 15675 0 0 0 102994 47 0 0 25 0 1 0 481797659 66494464 15653 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 16234 15653 603 41 0 16193 0 vsize: 64936 [startup+1040.31 s] Raw data (loadavg): 1.22 1.02 0.93 2/54 25263 Raw data (stat): 25210 (minisat+) R 25209 18865 18864 0 -1 0 15675 0 0 0 103995 47 0 0 25 0 1 0 481797659 66494464 15653 4294967295 134512640 134672761 3221224560 3221223728 134561118 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 16234 15653 603 41 0 16193 0 vsize: 64936 [startup+1050.41 s] Raw data (loadavg): 1.18 1.02 0.93 2/54 25263 Raw data (stat): 25210 (minisat+) R 25209 18865 18864 0 -1 0 15675 0 0 0 105006 47 0 0 25 0 1 0 481797659 66494464 15653 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 16234 15653 603 41 0 16193 0 vsize: 64936 [startup+1060.41 s] Raw data (loadavg): 1.15 1.02 0.93 2/54 25263 Raw data (stat): 25210 (minisat+) R 25209 18865 18864 0 -1 0 15675 0 0 0 106006 47 0 0 25 0 1 0 481797659 66494464 15653 4294967295 134512640 134672761 3221224560 3221223664 134560254 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 16234 15653 603 41 0 16193 0 vsize: 64936 [startup+1070.42 s] Raw data (loadavg): 1.13 1.02 0.93 2/54 25263 Raw data (stat): 25210 (minisat+) R 25209 18865 18864 0 -1 0 15675 0 0 0 107006 47 0 0 25 0 1 0 481797659 66494464 15653 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 16234 15653 603 41 0 16193 0 vsize: 64936 [startup+1080.42 s] Raw data (loadavg): 1.11 1.02 0.93 2/54 25263 Raw data (stat): 25210 (minisat+) R 25209 18865 18864 0 -1 0 15675 0 0 0 108006 47 0 0 25 0 1 0 481797659 66494464 15653 4294967295 134512640 134672761 3221224560 3221223728 134561266 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 16234 15653 603 41 0 16193 0 vsize: 64936 [startup+1090.42 s] Raw data (loadavg): 1.09 1.02 0.93 2/54 25263 Raw data (stat): 25210 (minisat+) R 25209 18865 18864 0 -1 0 15675 0 0 0 109007 47 0 0 25 0 1 0 481797659 66494464 15653 4294967295 134512640 134672761 3221224560 3221223728 134561201 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 16234 15653 603 41 0 16193 0 vsize: 64936 [startup+1100.42 s] Raw data (loadavg): 1.08 1.01 0.93 2/54 25263 Raw data (stat): 25210 (minisat+) R 25209 18865 18864 0 -1 0 15675 0 0 0 110007 47 0 0 25 0 1 0 481797659 66494464 15653 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 16234 15653 603 41 0 16193 0 vsize: 64936 [startup+1110.42 s] Raw data (loadavg): 1.06 1.01 0.93 2/54 25265 Raw data (stat): 25210 (minisat+) R 25209 18865 18864 0 -1 0 15675 0 0 0 111006 47 0 0 25 0 1 0 481797659 66494464 15653 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 16234 15653 603 41 0 16193 0 vsize: 64936 [startup+1120.42 s] Raw data (loadavg): 1.05 1.01 0.93 2/54 25265 Raw data (stat): 25210 (minisat+) R 25209 18865 18864 0 -1 0 15675 0 0 0 112007 47 0 0 25 0 1 0 481797659 66494464 15653 4294967295 134512640 134672761 3221224560 3221223728 134561205 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 16234 15653 603 41 0 16193 0 vsize: 64936 [startup+1130.42 s] Raw data (loadavg): 1.05 1.01 0.93 2/54 25265 Raw data (stat): 25210 (minisat+) R 25209 18865 18864 0 -1 0 15675 0 0 0 113007 47 0 0 25 0 1 0 481797659 66494464 15653 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 16234 15653 603 41 0 16193 0 vsize: 64936 [startup+1140.42 s] Raw data (loadavg): 1.04 1.01 0.93 2/54 25265 Raw data (stat): 25210 (minisat+) R 25209 18865 18864 0 -1 0 15675 0 0 0 114007 47 0 0 25 0 1 0 481797659 66494464 15653 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 16234 15653 603 41 0 16193 0 vsize: 64936 [startup+1150.42 s] Raw data (loadavg): 1.03 1.01 0.93 2/54 25265 Raw data (stat): 25210 (minisat+) R 25209 18865 18864 0 -1 0 15675 0 0 0 115007 47 0 0 25 0 1 0 481797659 66494464 15653 4294967295 134512640 134672761 3221224560 3221223728 134560882 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 16234 15653 603 41 0 16193 0 vsize: 64936 [startup+1160.42 s] Raw data (loadavg): 1.03 1.01 0.93 2/54 25265 Raw data (stat): 25210 (minisat+) R 25209 18865 18864 0 -1 0 15676 0 0 0 116007 47 0 0 25 0 1 0 481797659 66494464 15654 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 16234 15654 603 41 0 16193 0 vsize: 64936 [startup+1170.42 s] Raw data (loadavg): 1.02 1.01 0.93 2/54 25265 Raw data (stat): 25210 (minisat+) R 25209 18865 18864 0 -1 0 15678 0 0 0 117008 47 0 0 25 0 1 0 481797659 66494464 15656 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 16234 15656 603 41 0 16193 0 vsize: 64936 [startup+1180.42 s] Raw data (loadavg): 1.02 1.01 0.93 2/54 25265 Raw data (stat): 25210 (minisat+) R 25209 18865 18864 0 -1 0 15680 0 0 0 118008 47 0 0 25 0 1 0 481797659 66494464 15658 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 16234 15658 603 41 0 16193 0 vsize: 64936 [startup+1190.42 s] Raw data (loadavg): 1.02 1.01 0.93 2/54 25265 Raw data (stat): 25210 (minisat+) R 25209 18865 18864 0 -1 0 15683 0 0 0 119008 48 0 0 25 0 1 0 481797659 67018752 15661 4294967295 134512640 134672761 3221224560 3221223728 134560988 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 16362 15661 603 41 0 16321 0 vsize: 65448 [startup+1200.42 s] Raw data (loadavg): 1.01 1.00 0.93 2/54 25265 Raw data (stat): 25210 (minisat+) R 25209 18865 18864 0 -1 0 15754 0 0 0 120008 48 0 0 25 0 1 0 481797659 67284992 15732 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 16427 15732 603 41 0 16386 0 vsize: 65708 Maximum CPU time exceeded: sending SIGTERM and SIGKILL [startup+1200.45 s] Raw data (loadavg): 1.01 1.00 0.93 1/54 25265 Raw data (stat): 25210 (minisat+) Z 25209 18865 18864 0 -1 12 15757 0 0 0 120008 51 0 0 25 0 1 0 481797659 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.45 CPU time (s): 1200.6 CPU user time (s): 1200.09 CPU system time (s): 0.511922 CPU usage (%): 100.012 Max. virtual memory (Kb): 65708 #### END WATCHER DATA #### #### BEGIN VERIFIER DATA #### ERROR: no interpretation found ! #### END VERIFIER DATA ####