Name | normalized-opb/web/www.nlsde.buaa.edu.cn/~kexu/benchmarks/frb59-26-opb/normalized-frb59-26-5.opb |
MD5SUM | a5354df485c2b6c1695d0d26c0cdb212 |
Bench Category | optimization, small integers (OPTSMALLINT) |
Has Objective Function | YES |
Satisfiable | YES |
(Un)Satisfiability was proved | YES |
Best value of the objective function | -42 |
Optimality of the best value was proved | NO |
Number of terms in the objective function | 1534 |
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 | 1534 |
Number of bits of the sum of numbers in the objective function | 11 |
Biggest number in a constraint | 1 |
Number of bits of the biggest number in a constraint | 1 |
Biggest sum of numbers in a constraint | 1534 |
Number of bits of the biggest sum of numbers | 11 |
Best result obtained on this benchmark | SAT |
Best CPU time to get the best result obtained on this benchmark | 1175.13 |
Number of variables | 1534 |
Total number of constraints | 125982 |
Number of constraints which are clauses | 125982 |
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 wulflinc12 THE 2005-05-25 17:35:18 (client local time) PB2005-SCRIPT v4.0 MARKUPS: idlaunch=21935 boxname=wulflinc12 idbench=353 idsolver=15 numberseed=0 MD5SUM SOLVER: 34d34154b8ad81f02ee98439942e0814 /oldhome/oroussel/solvers/minisat+_script MD5SUM BENCH: a5354df485c2b6c1695d0d26c0cdb212 /oldhome/oroussel/tmp/wulflinc12/normalized-frb59-26-5.opb REAL COMMAND: minisat+_script /oldhome/oroussel/tmp/wulflinc12/normalized-frb59-26-5.opb IDLAUNCH: 21935 /proc/cpuinfo: processor : 0 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 2 cpu MHz : 451.091 cache size : 512 KB fdiv_bug : no hlt_bug : no f00f_bug : no coma_bug : no fpu : yes fpu_exception : yes cpuid level : 2 wp : yes flags : fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse bogomips : 888.83 processor : 1 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 2 cpu MHz : 451.091 cache size : 512 KB fdiv_bug : no hlt_bug : no f00f_bug : no coma_bug : no fpu : yes fpu_exception : yes cpuid level : 2 wp : yes flags : fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse bogomips : 899.07 /proc/meminfo: MemTotal: 1034660 kB MemFree: 340016 kB Buffers: 34808 kB Cached: 637896 kB SwapCached: 564 kB Active: 59932 kB Inactive: 615228 kB HighTotal: 131008 kB HighFree: 252 kB LowTotal: 903652 kB LowFree: 339764 kB SwapTotal: 2097136 kB SwapFree: 2096076 kB Dirty: 28 kB Writeback: 0 kB Mapped: 5680 kB Slab: 13820 kB Committed_AS: 63600 kB PageTables: 316 kB VmallocTotal: 114680 kB VmallocUsed: 1364 kB VmallocChunk: 113256 kB JOB ENDED THE 2005-05-25 17:55:48 (client local time) WITH STATUS 152 IN 1229.89 SECONDS stats: 21935 7 1229.89 152 #### END LAUNCHER DATA #### #### BEGIN SOLVER DATA #### c Parsing PB file... c Converting 125982 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 | 125982 251964 | 41994 0 0 nan | 0.000 % | c ============================================================================== c [1mFound solution: -42[0m c ---[ 0]---> Sorter-cost:85954 Base: c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 0 | 216721 464825 | 72240 0 0 nan | 0.000 % | c | 100 | 215959 463222 | 79464 65 492 7.6 | 0.688 % | c | 250 | 215163 461534 | 87410 185 1565 8.5 | 1.408 % | c | 475 | 214472 460051 | 96151 367 3201 8.7 | 2.048 % | c | 812 | 213299 457504 | 105766 663 6213 9.4 | 3.198 % | c | 1318 | 210803 452048 | 116343 1052 10471 10.0 | 5.545 % | c | 2078 | 206899 443392 | 127977 1632 16581 10.2 | 9.378 % | c | 3217 | 199960 427819 | 140775 2503 25519 10.2 | 16.335 % | c | 4925 | 192015 409778 | 154852 3695 39888 10.8 | 24.503 % | c | 7488 | 180386 383175 | 170338 5442 62629 11.5 | 36.510 % | c ============================================================================== c [1mFound solution: -43[0m c ---[ 0]---> Sorter-cost: 0 Base: c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 9101 | 174218 369045 | 58072 6524 77488 11.9 | 36.510 % | c | 9201 | 173612 367663 | 63879 6598 78260 11.9 | 43.746 % | c | 9352 | 172254 364438 | 70267 6634 78701 11.9 | 45.220 % | c | 9577 | 171126 361800 | 77293 6770 80672 11.9 | 46.408 % | c | 9915 | 170107 359398 | 85023 7035 83170 11.8 | 47.468 % | c | 10421 | 168416 355375 | 93525 7369 86547 11.7 | 49.288 % | c | 11180 | 166329 350476 | 102878 7889 92417 11.7 | 51.500 % | c | 12319 | 162134 340596 | 113165 8719 103213 11.8 | 56.044 % | c | 14027 | 157622 329892 | 124482 9863 120023 12.2 | 60.978 % | c | 16590 | 154141 321594 | 136930 11740 143012 12.2 | 64.795 % | c | 20434 | 148827 308955 | 150623 14218 196223 13.8 | 70.642 % | c | 26201 | 143510 296212 | 165686 18448 300139 16.3 | 76.485 % | c ============================================================================== c [1mFound solution: -44[0m c ---[ 0]---> Sorter-cost: 0 Base: c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 26706 | 143396 295898 | 47798 18911 307260 16.2 | 76.485 % | c | 26807 | 143365 295823 | 52577 19010 309012 16.3 | 76.650 % | c | 26957 | 143346 295776 | 57835 19153 311224 16.2 | 76.673 % | c | 27182 | 143346 295776 | 63619 19378 315135 16.3 | 76.673 % | c | 27519 | 143147 295303 | 69981 19597 320396 16.3 | 76.894 % | c | 28026 | 143091 295163 | 76979 20091 335810 16.7 | 76.962 % | c | 28786 | 142405 293484 | 84677 20635 354173 17.2 | 77.752 % | c | 29925 | 142052 292643 | 93144 21385 377394 17.6 | 78.191 % | c | 31633 | 141301 290830 | 102459 22900 434457 19.0 | 78.986 % | c ============================================================================== c [1mFound solution: -45[0m c ---[ 0]---> Sorter-cost: 0 Base: c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 32831 | 141162 290523 | 47054 23957 491822 20.5 | 78.986 % | c | 32932 | 140811 289673 | 51759 23932 490747 20.5 | 79.557 % | c | 33082 | 140811 289673 | 56935 24082 494759 20.5 | 79.557 % | c | 33307 | 140758 289546 | 62628 24212 497422 20.5 | 79.617 % | c | 33644 | 140708 289438 | 68891 24539 505279 20.6 | 79.664 % | c | 34150 | 140708 289438 | 75780 25045 526109 21.0 | 79.664 % | c ============================================================================== c [1mFound solution: -47[0m c ---[ 0]---> Sorter-cost: 0 Base: c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 34585 | 140706 289496 | 46902 25409 545666 21.5 | 79.664 % | c | 34685 | 140631 289325 | 51592 25488 547741 21.5 | 79.790 % | c | 34835 | 140502 289012 | 56751 25504 551262 21.6 | 79.937 % | c | 35060 | 140402 288768 | 62426 25617 555828 21.7 | 80.050 % | c | 35397 | 140196 288258 | 68669 25847 566341 21.9 | 80.291 % | c | 35903 | 139974 287726 | 75536 26221 579362 22.1 | 80.531 % | c | 36662 | 139868 287454 | 83089 26872 608330 22.6 | 80.663 % | c | 37801 | 139004 285361 | 91398 27413 642062 23.4 | 81.628 % | c | 39510 | 138731 284704 | 100538 28798 697757 24.2 | 81.934 % | c | 42072 | 138129 283247 | 110592 30903 807101 26.1 | 82.604 % | c | 45917 | 137418 281505 | 121651 33977 991265 29.2 | 83.419 % | c ============================================================================== c [1mFound solution: -48[0m c ---[ 0]---> Sorter-cost: 0 Base: c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 50963 | 136707 279714 | 45569 38071 1355297 35.6 | 83.419 % | c | 51064 | 136665 279612 | 50125 38151 1356275 35.6 | 84.305 % | c | 51214 | 136633 279530 | 55138 38260 1360588 35.6 | 84.344 % | c | 51440 | 136573 279388 | 60652 38306 1366438 35.7 | 84.410 % | c | 51777 | 136483 279176 | 66717 38425 1384832 36.0 | 84.508 % | c | 52284 | 136441 279076 | 73389 38870 1410855 36.3 | 84.555 % | c | 53044 | 136283 278706 | 80728 39261 1464008 37.3 | 84.726 % | c | 54183 | 136243 278610 | 88801 40352 1545061 38.3 | 84.771 % | c | 55891 | 136190 278485 | 97681 41887 1699101 40.6 | 84.827 % | c | 58453 | 136091 278234 | 107449 44175 1922681 43.5 | 84.946 % | c | 62297 | 136041 278108 | 118194 47904 2464514 51.4 | 85.006 % | c | 68063 | 135763 277417 | 130013 53108 3155017 59.4 | 85.333 % | c ============================================================================== c [1mFound solution: -49[0m c ---[ 0]---> Sorter-cost: 0 Base: c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 72442 | 135783 277482 | 45261 57408 3652183 63.6 | 85.333 % | c | 72542 | 135783 277482 | 49787 57508 3657004 63.6 | 85.319 % | c | 72693 | 135749 277402 | 54765 57629 3661230 63.5 | 85.356 % | c | 72918 | 135744 277391 | 60242 57848 3671369 63.5 | 85.361 % | c | 73256 | 135732 277365 | 66266 58171 3703940 63.7 | 85.372 % | c | 73763 | 135695 277274 | 72893 58562 3756826 64.2 | 85.416 % | c | 74522 | 135611 277064 | 80182 59191 3786127 64.0 | 85.514 % | c | 75662 | 135611 277064 | 88200 60331 3934420 65.2 | 85.514 % | c | 77370 | 135597 277030 | 97020 62037 4154789 67.0 | 85.530 % | c ============================================================================== c [1mFound solution: -50[0m c ---[ 0]---> Sorter-cost: 0 Base: c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 78950 | 135575 276913 | 45191 62522 4231397 67.7 | 85.530 % | c | 79050 | 135532 276799 | 49710 62546 4231449 67.7 | 85.609 % | c | 79200 | 135532 276799 | 54681 62696 4238985 67.6 | 85.609 % | c | 79425 | 135529 276792 | 60149 62920 4255939 67.6 | 85.613 % | c | 79762 | 135529 276792 | 66164 63257 4304084 68.0 | 85.613 % | c | 80270 | 135529 276792 | 72780 63765 4359392 68.4 | 85.613 % | c | 81029 | 135444 276590 | 80058 64283 4405638 68.5 | 85.704 % | c | 82168 | 135444 276590 | 88064 65422 4514282 69.0 | 85.704 % | c ============================================================================== c [1mFound solution: -51[0m c ---[ 0]---> Sorter-cost: 0 Base: c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 82761 | 135475 276684 | 45158 66015 4553481 69.0 | 85.704 % | c | 82861 | 135465 276660 | 49673 66081 4556332 69.0 | 85.710 % | c | 83011 | 135465 276660 | 54641 66231 4565254 68.9 | 85.710 % | c | 83236 | 135465 276660 | 60105 66456 4570299 68.8 | 85.710 % | c | 83573 | 135465 276660 | 66115 66793 4594919 68.8 | 85.710 % | c | 84079 | 135342 276354 | 72727 67152 4631108 69.0 | 85.848 % | c | 84839 | 135228 276086 | 80000 67812 4691309 69.2 | 85.972 % | c | 85979 | 135203 276023 | 88000 68603 4777095 69.6 | 86.003 % | c | 87687 | 135029 275598 | 96800 69732 4907965 70.4 | 86.203 % | c | 90249 | 135029 275598 | 106480 72294 5274639 73.0 | 86.203 % | c | 94093 | 134944 275390 | 117128 75951 5693190 75.0 | 86.301 % | c | 99859 | 134883 275249 | 128841 81592 6421159 78.7 | 86.366 % | c | 108508 | 134835 275135 | 141725 90163 7860535 87.2 | 86.419 % | c | 121482 | 134799 275042 | 155897 102952 9664105 93.9 | 86.462 % | c | 140943 | 134747 274910 | 171487 122344 13291931 108.6 | 86.526 % | c | 170136 | 134672 274727 | 188636 151088 19209599 127.1 | 86.613 % | c ============================================================================== c [1mFound solution: -52[0m c ---[ 0]---> Sorter-cost: 0 Base: c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 186163 | 134612 274561 | 44870 165904 21520868 129.7 | 86.613 % | c | 186263 | 134612 274561 | 49357 25515 2207333 86.5 | 86.684 % | c | 186414 | 134601 274534 | 54292 25642 2217650 86.5 | 86.697 % | c | 186639 | 134601 274534 | 59721 25867 2241685 86.7 | 86.697 % | c | 186976 | 134524 274345 | 65694 26124 2249912 86.1 | 86.787 % | c | 187482 | 134420 274095 | 72263 26616 2278339 85.6 | 86.903 % | c | 188241 | 134420 274095 | 79489 27375 2319156 84.7 | 86.903 % | c | 189380 | 134420 274095 | 87438 28514 2435373 85.4 | 86.903 % | c | 191088 | 134420 274095 | 96182 30222 2600030 86.0 | 86.903 % | c | 193650 | 134417 274088 | 105801 32781 3007387 91.7 | 86.906 % | c | 197495 | 134364 273965 | 116381 36616 3563866 97.3 | 86.962 % | c | 203261 | 134364 273965 | 128019 42382 4293921 101.3 | 86.962 % | c | 211910 | 134328 273873 | 140821 51012 5544856 108.7 | 87.005 % | c | 224884 | 134328 273873 | 154903 63986 7907749 123.6 | 87.005 % | c | 244345 | 134328 273873 | 170393 83447 11620820 139.3 | 87.005 % | c ============================================================================== c [1mFound solution: -53[0m c ---[ 0]---> Sorter-cost: 0 Base: c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 251911 | 134341 273909 | 44780 90983 12874260 141.5 | 87.005 % | c | 252011 | 134341 273909 | 49258 91083 12879997 141.4 | 87.002 % | c | 252162 | 134341 273909 | 54183 91234 12893752 141.3 | 87.002 % | c | 252387 | 134341 273909 | 59602 91459 12918345 141.2 | 87.002 % | c | 252725 | 134341 273909 | 65562 91797 12950424 141.1 | 87.002 % | c | 253231 | 134337 273899 | 72118 92302 12995661 140.8 | 87.007 % | c | 253991 | 134323 273863 | 79330 93028 13081442 140.6 | 87.025 % | c | 255130 | 134323 273863 | 87263 94167 13274461 141.0 | 87.025 % | c | 256838 | 134323 273863 | 95989 95875 13445425 140.2 | 87.025 % | c | 259400 | 134283 273763 | 105588 98400 13873992 141.0 | 87.073 % | c | 263244 | 134283 273763 | 116147 102244 14537960 142.2 | 87.073 % | c | 269010 | 134283 273763 | 127762 108010 15238191 141.1 | 87.073 % | c | 277659 | 134277 273749 | 140538 116656 16475671 141.2 | 87.079 % | /oldhome/oroussel/solvers/minisat+_script: line 9: 15396 CPU time limit exceeded $XDIR/minisat+_64-bit_static -try "$@" #### END SOLVER DATA #### #### BEGIN WATCHER DATA #### Enforcing CPU limit (will send SIGTERM then SIGKILL): 1200 seconds Enforcing CPUTime (will send SIGXCPU) limit: 1230 seconds Enforcing VSIZE limit: 943718400 bytes Raw data (loadavg): 0.92 0.95 0.90 2/54 15392 Raw data (stat): 15392 (runsolver) R 15391 32284 32283 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 782493789 1052672 99 4294967295 134512640 135381576 3221224496 3221219704 135158418 0 2147483391 7 90112 0 0 0 17 1 0 0 Raw data (statm): 257 99 215 215 0 42 0 vsize: 1028 [startup+10.0002 s] Raw data (loadavg): 0.93 0.96 0.91 2/55 15396 Raw data (stat): 15392 (minisat+_script) S 15391 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782493789 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+20.0002 s] Raw data (loadavg): 0.94 0.96 0.91 2/55 15396 Raw data (stat): 15392 (minisat+_script) S 15391 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782493789 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+30.001 s] Raw data (loadavg): 0.95 0.96 0.91 2/55 15396 Raw data (stat): 15392 (minisat+_script) S 15391 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782493789 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+40.0007 s] Raw data (loadavg): 0.96 0.96 0.91 2/55 15396 Raw data (stat): 15392 (minisat+_script) S 15391 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782493789 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+50.0005 s] Raw data (loadavg): 0.96 0.96 0.91 2/55 15396 Raw data (stat): 15392 (minisat+_script) S 15391 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782493789 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+60.0004 s] Raw data (loadavg): 0.97 0.96 0.91 2/55 15396 Raw data (stat): 15392 (minisat+_script) S 15391 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782493789 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+70.0002 s] Raw data (loadavg): 0.97 0.96 0.91 2/55 15396 Raw data (stat): 15392 (minisat+_script) S 15391 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782493789 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+80.0011 s] Raw data (loadavg): 0.98 0.96 0.91 2/55 15396 Raw data (stat): 15392 (minisat+_script) S 15391 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782493789 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+90.0009 s] Raw data (loadavg): 0.98 0.96 0.91 2/55 15396 Raw data (stat): 15392 (minisat+_script) S 15391 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782493789 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+100.001 s] Raw data (loadavg): 0.98 0.96 0.91 2/55 15396 Raw data (stat): 15392 (minisat+_script) S 15391 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782493789 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+110.002 s] Raw data (loadavg): 0.98 0.97 0.91 2/55 15396 Raw data (stat): 15392 (minisat+_script) S 15391 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782493789 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+120.001 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 15396 Raw data (stat): 15392 (minisat+_script) S 15391 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782493789 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+130.002 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 15396 Raw data (stat): 15392 (minisat+_script) S 15391 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782493789 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+140.002 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 15396 Raw data (stat): 15392 (minisat+_script) S 15391 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782493789 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+150.002 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 15396 Raw data (stat): 15392 (minisat+_script) S 15391 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782493789 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+160.003 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 15396 Raw data (stat): 15392 (minisat+_script) S 15391 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782493789 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+170.003 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 15396 Raw data (stat): 15392 (minisat+_script) S 15391 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782493789 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+180.003 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 15396 Raw data (stat): 15392 (minisat+_script) S 15391 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782493789 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+190.003 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 15396 Raw data (stat): 15392 (minisat+_script) S 15391 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782493789 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+200.003 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 15396 Raw data (stat): 15392 (minisat+_script) S 15391 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782493789 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+210.003 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 15396 Raw data (stat): 15392 (minisat+_script) S 15391 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782493789 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+220.004 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 15396 Raw data (stat): 15392 (minisat+_script) S 15391 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782493789 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+230.005 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 15396 Raw data (stat): 15392 (minisat+_script) S 15391 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782493789 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+240.005 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 15396 Raw data (stat): 15392 (minisat+_script) S 15391 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782493789 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+250.004 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 15396 Raw data (stat): 15392 (minisat+_script) S 15391 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782493789 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+260.005 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 15396 Raw data (stat): 15392 (minisat+_script) S 15391 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782493789 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+270.005 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 15396 Raw data (stat): 15392 (minisat+_script) S 15391 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782493789 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+280.006 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 15396 Raw data (stat): 15392 (minisat+_script) S 15391 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782493789 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+290.007 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 15396 Raw data (stat): 15392 (minisat+_script) S 15391 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782493789 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+300.007 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 15396 Raw data (stat): 15392 (minisat+_script) S 15391 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782493789 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+310.007 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 15396 Raw data (stat): 15392 (minisat+_script) S 15391 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782493789 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+320.007 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 15396 Raw data (stat): 15392 (minisat+_script) S 15391 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782493789 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+330.008 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 15396 Raw data (stat): 15392 (minisat+_script) S 15391 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782493789 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+340.008 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 15396 Raw data (stat): 15392 (minisat+_script) S 15391 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782493789 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+350.008 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 15396 Raw data (stat): 15392 (minisat+_script) S 15391 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782493789 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+360.009 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 15396 Raw data (stat): 15392 (minisat+_script) S 15391 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782493789 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+370.008 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 15396 Raw data (stat): 15392 (minisat+_script) S 15391 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782493789 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+380.008 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 15396 Raw data (stat): 15392 (minisat+_script) S 15391 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782493789 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+390.009 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 15396 Raw data (stat): 15392 (minisat+_script) S 15391 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782493789 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+400.008 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 15396 Raw data (stat): 15392 (minisat+_script) S 15391 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782493789 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+410.009 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 15396 Raw data (stat): 15392 (minisat+_script) S 15391 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782493789 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+420.009 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 15396 Raw data (stat): 15392 (minisat+_script) S 15391 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782493789 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+430.01 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 15396 Raw data (stat): 15392 (minisat+_script) S 15391 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782493789 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+440.009 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 15396 Raw data (stat): 15392 (minisat+_script) S 15391 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782493789 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+450.01 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 15396 Raw data (stat): 15392 (minisat+_script) S 15391 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782493789 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+460.01 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 15396 Raw data (stat): 15392 (minisat+_script) S 15391 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782493789 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+470.011 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 15396 Raw data (stat): 15392 (minisat+_script) S 15391 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782493789 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+480.012 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 15396 Raw data (stat): 15392 (minisat+_script) S 15391 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782493789 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+490.013 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 15396 Raw data (stat): 15392 (minisat+_script) S 15391 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782493789 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+500.012 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 15396 Raw data (stat): 15392 (minisat+_script) S 15391 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782493789 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+510.013 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 15396 Raw data (stat): 15392 (minisat+_script) S 15391 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782493789 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+520.013 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 15396 Raw data (stat): 15392 (minisat+_script) S 15391 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782493789 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+530.013 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 15396 Raw data (stat): 15392 (minisat+_script) S 15391 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782493789 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+540.014 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 15396 Raw data (stat): 15392 (minisat+_script) S 15391 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782493789 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+550.014 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 15396 Raw data (stat): 15392 (minisat+_script) S 15391 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782493789 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+560.014 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 15396 Raw data (stat): 15392 (minisat+_script) S 15391 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782493789 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+570.014 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 15396 Raw data (stat): 15392 (minisat+_script) S 15391 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782493789 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+580.015 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 15396 Raw data (stat): 15392 (minisat+_script) S 15391 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782493789 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+590.015 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 15396 Raw data (stat): 15392 (minisat+_script) S 15391 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782493789 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+600.015 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 15396 Raw data (stat): 15392 (minisat+_script) S 15391 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782493789 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+610.016 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 15396 Raw data (stat): 15392 (minisat+_script) S 15391 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782493789 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+620.016 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 15396 Raw data (stat): 15392 (minisat+_script) S 15391 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782493789 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+630.017 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 15396 Raw data (stat): 15392 (minisat+_script) S 15391 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782493789 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+640.018 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 15396 Raw data (stat): 15392 (minisat+_script) S 15391 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782493789 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+650.017 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 15396 Raw data (stat): 15392 (minisat+_script) S 15391 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782493789 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+660.017 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 15396 Raw data (stat): 15392 (minisat+_script) S 15391 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782493789 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+670.017 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 15396 Raw data (stat): 15392 (minisat+_script) S 15391 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782493789 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+680.018 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 15396 Raw data (stat): 15392 (minisat+_script) S 15391 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782493789 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+690.018 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 15396 Raw data (stat): 15392 (minisat+_script) S 15391 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782493789 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+700.018 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 15396 Raw data (stat): 15392 (minisat+_script) S 15391 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782493789 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+710.018 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 15396 Raw data (stat): 15392 (minisat+_script) S 15391 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782493789 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+720.018 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 15396 Raw data (stat): 15392 (minisat+_script) S 15391 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782493789 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+730.019 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 15396 Raw data (stat): 15392 (minisat+_script) S 15391 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782493789 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+740.019 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 15396 Raw data (stat): 15392 (minisat+_script) S 15391 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782493789 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+750.019 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 15396 Raw data (stat): 15392 (minisat+_script) S 15391 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782493789 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+760.019 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 15396 Raw data (stat): 15392 (minisat+_script) S 15391 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782493789 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+770.018 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 15396 Raw data (stat): 15392 (minisat+_script) S 15391 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782493789 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+780.019 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 15396 Raw data (stat): 15392 (minisat+_script) S 15391 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782493789 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+790.019 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 15396 Raw data (stat): 15392 (minisat+_script) S 15391 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782493789 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+800.019 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 15396 Raw data (stat): 15392 (minisat+_script) S 15391 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782493789 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+810.019 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 15396 Raw data (stat): 15392 (minisat+_script) S 15391 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782493789 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+820.019 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 15396 Raw data (stat): 15392 (minisat+_script) S 15391 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782493789 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+830.019 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 15396 Raw data (stat): 15392 (minisat+_script) S 15391 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782493789 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+840.019 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 15396 Raw data (stat): 15392 (minisat+_script) S 15391 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782493789 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+850.019 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 15396 Raw data (stat): 15392 (minisat+_script) S 15391 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782493789 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+860.019 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 15396 Raw data (stat): 15392 (minisat+_script) S 15391 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782493789 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+870.019 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 15396 Raw data (stat): 15392 (minisat+_script) S 15391 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782493789 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+880.02 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 15396 Raw data (stat): 15392 (minisat+_script) S 15391 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782493789 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+890.021 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 15396 Raw data (stat): 15392 (minisat+_script) S 15391 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782493789 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+900.02 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 15396 Raw data (stat): 15392 (minisat+_script) S 15391 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782493789 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+910.02 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 15396 Raw data (stat): 15392 (minisat+_script) S 15391 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782493789 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+920.02 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 15396 Raw data (stat): 15392 (minisat+_script) S 15391 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782493789 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+930.021 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 15396 Raw data (stat): 15392 (minisat+_script) S 15391 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782493789 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+940.021 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 15396 Raw data (stat): 15392 (minisat+_script) S 15391 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782493789 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+950.02 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 15396 Raw data (stat): 15392 (minisat+_script) S 15391 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782493789 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+960.02 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 15396 Raw data (stat): 15392 (minisat+_script) S 15391 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782493789 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+970.02 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 15396 Raw data (stat): 15392 (minisat+_script) S 15391 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782493789 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+980.021 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 15396 Raw data (stat): 15392 (minisat+_script) S 15391 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782493789 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+990.022 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 15396 Raw data (stat): 15392 (minisat+_script) S 15391 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782493789 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1000.02 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 15396 Raw data (stat): 15392 (minisat+_script) S 15391 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782493789 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1010.02 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 15396 Raw data (stat): 15392 (minisat+_script) S 15391 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782493789 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1020.02 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 15396 Raw data (stat): 15392 (minisat+_script) S 15391 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782493789 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1030.02 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 15396 Raw data (stat): 15392 (minisat+_script) S 15391 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782493789 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1040.02 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 15396 Raw data (stat): 15392 (minisat+_script) S 15391 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782493789 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1050.02 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 15396 Raw data (stat): 15392 (minisat+_script) S 15391 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782493789 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1060.02 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 15396 Raw data (stat): 15392 (minisat+_script) S 15391 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782493789 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1070.02 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 15396 Raw data (stat): 15392 (minisat+_script) S 15391 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782493789 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1080.02 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 15396 Raw data (stat): 15392 (minisat+_script) S 15391 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782493789 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1090.03 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 15396 Raw data (stat): 15392 (minisat+_script) S 15391 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782493789 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1100.03 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 15396 Raw data (stat): 15392 (minisat+_script) S 15391 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782493789 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1110.03 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 15396 Raw data (stat): 15392 (minisat+_script) S 15391 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782493789 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1120.03 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 15396 Raw data (stat): 15392 (minisat+_script) S 15391 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782493789 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1130.03 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 15396 Raw data (stat): 15392 (minisat+_script) S 15391 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782493789 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1140.03 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 15396 Raw data (stat): 15392 (minisat+_script) S 15391 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782493789 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1150.03 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 15396 Raw data (stat): 15392 (minisat+_script) S 15391 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782493789 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1160.03 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 15396 Raw data (stat): 15392 (minisat+_script) S 15391 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782493789 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1170.03 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 15396 Raw data (stat): 15392 (minisat+_script) S 15391 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782493789 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1180.03 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 15396 Raw data (stat): 15392 (minisat+_script) S 15391 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782493789 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1190.03 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 15396 Raw data (stat): 15392 (minisat+_script) S 15391 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782493789 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1200.03 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 15396 Raw data (stat): 15392 (minisat+_script) S 15391 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782493789 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1210.03 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 15396 Raw data (stat): 15392 (minisat+_script) S 15391 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782493789 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1220.03 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 15396 Raw data (stat): 15392 (minisat+_script) S 15391 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782493789 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1229.78 s] Raw data (loadavg): 0.99 0.97 0.91 1/53 15396 Raw data (stat): 15392 (minisat+_script) S 15391 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782493789 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 0 Child status: 152 Real time (s): 1229.78 CPU time (s): 1229.89 CPU user time (s): 1228.95 CPU system time (s): 0.937857 CPU usage (%): 100.009 Max. virtual memory (Kb): 2124 #### END WATCHER DATA #### #### BEGIN VERIFIER DATA #### ERROR: no interpretation found ! #### END VERIFIER DATA ####