PB'05 competition: run trace

Some explanations

A solver is run under the control of another program named runsolver. runsolver is in charge of imposing the CPU time limit and the memory limit to the solver. It also monitors some information about the process. The trace of the execution of a solver is divided in four parts:
LAUNCHER DATA
These informations are related to the script which will launch the solver. The most important informations are the command line given to the solver, the md5sum of the different files and the dump of the /proc/cpuinfo and /proc/meminfo which provide some useful information on the computer.
SOLVER DATA
This is the output of the solver (stdout and stderr).
WATCHER DATA
This is the informations gathered by the runsolver program. It first prints the different limits. There's a first limit on CPU time set to 1200 seconds. After this time has ellapsed, runsolver sends a SIGTERM and 2 seconds later a SIGKILL to the solver. For safety, there's also another limit set to 1230 seconds which will send a SIGXPU to the solver. The last limit is on the virtual memory used by the process (900Mb).
Every ten seconds, the runsolver process fetches the content of /proc/loadavg, /proc/pid/stat and /proc/pid/statm (see man proc) and prints it as raw data. This is only recorded in case we need to investigate the behaviour of a solver. The memory used by the solver (vsize) is also given every ten seconds.
When the solver exits, runsolver prints some informations such as status and time. CPU usage is the ratio CPU Time/Real Time.
VERIFIER DATA
The output of the solver is piped to a verifier program which will search a value line "v " and, if found, will check that the given interpretation satisfies all constraints.
General information on the benchmark

Name	normalized-opb/mps-v2-13-7/plato.asu.edu/pub/unibo/normalized-mps-v2-13-7-biella1.opb
MD5SUM	fc29c960bdd0cb480a316491664519da
Bench Category	optimization, big integers (OPTBIGINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	2147483647
Optimality of the best value was proved	NO
Number of terms in the objective function	30470
Biggest coefficient in the objective function	524288000000000000
Number of bits for the biggest coefficient in the objective function	59
Sum of the numbers in the objective function	4667772661205021200
Number of bits of the sum of numbers in the objective function	63
Biggest number in a constraint	524288000000000000
Number of bits of the biggest number in a constraint	59
Biggest sum of numbers in a constraint	4680572661205021200
Number of bits of the biggest sum of numbers	63
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	1250.4
Number of variables	30470
Total number of constraints	7313
Number of constraints which are clauses	0
Number of constraints which are cardinality constraints (but not clauses)	6111
Number of constraints which are nor clauses,nor cardinality constraints	1202
Minimum length of a constraint	1
Maximum length of a constraint	30470
Trace number 31325

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc7 THE 2005-05-26 00:09:22 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=22719 boxname=wulflinc7 idbench=1535 idsolver=15 numberseed=0
MD5SUM SOLVER: 34d34154b8ad81f02ee98439942e0814  /oldhome/oroussel/solvers/minisat+_script
MD5SUM BENCH:  fc29c960bdd0cb480a316491664519da  /oldhome/oroussel/tmp/wulflinc7/normalized-mps-v2-13-7-biella1.opb
REAL COMMAND:  minisat+_script /oldhome/oroussel/tmp/wulflinc7/normalized-mps-v2-13-7-biella1.opb
IDLAUNCH: 22719
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.050
cache size	: 512 KB
fdiv_bug	: no
hlt_bug		: no
f00f_bug	: no
coma_bug	: no
fpu		: yes
fpu_exception	: yes
cpuid level	: 2
wp		: yes
flags		: fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse
bogomips	: 890.88

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.050
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:        873888 kB
Buffers:         32116 kB
Cached:         108512 kB
SwapCached:        676 kB
Active:          26952 kB
Inactive:       115672 kB
HighTotal:      131008 kB
HighFree:        61600 kB
LowTotal:       903652 kB
LowFree:        812288 kB
SwapTotal:     2097136 kB
SwapFree:      2095524 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           5068 kB
Slab:            12520 kB
Committed_AS:    63604 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-05-26 00:29:52 (client local time) WITH STATUS 152 IN 1230.11 SECONDS
stats: 22719 7 1230.11 152
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c PARSE ERROR! [line 7332] Integer overflow. Use BigNum-version.
c OK -- Running BigNum-version instead...
c Parsing PB file...
c Converting 2399 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: #############################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################
c   -- Clauses(.)/Splits(s): (none)
c ---[2397]---> Adder-cost: 76   maxlim: 4352   bits: 14/13
c ---[2395]---> Sorter-cost:  996     Base: 2 2 2 2 2 2 2 7
c ---[2393]---> Adder-cost: 276   maxlim: 16896   bits: 16/15
c ---[2391]---> Adder-cost: 280   maxlim: 19456   bits: 16/15
c ---[2389]---> Adder-cost: 200   maxlim: 15104   bits: 15/14
c ---[2387]---> Sorter-cost:  467     Base: 2 2 2 2 2 2 2 7
c ---[2385]---> Sorter-cost:  266     Base: 2 2 2 2 2 2 2 2
c ---[2383]---> Sorter-cost:  308     Base: 2 2 2 2 2 2 2 2
c ---[2381]---> Sorter-cost:  443     Base: 2 2 2 2 2 2 2 7
c ---[2379]---> Adder-cost: 254   maxlim: 16128   bits: 15/14
c ---[2377]---> Sorter-cost:  637     Base: 2 2 2 2 2 2 2 7
c ---[2375]---> Adder-cost: 76   maxlim: 16128   bits: 15/14
c ---[2373]---> Adder-cost: 220   maxlim: 15104   bits: 15/14
c ---[2371]---> Adder-cost: 80   maxlim: 15104   bits: 15/14
c ---[2369]---> Adder-cost: 186   maxlim: 13312   bits: 15/14
c ---[2367]---> Adder-cost: 116   maxlim: 13440   bits: 15/14
c ---[2365]---> Adder-cost: 184   maxlim: 12544   bits: 15/14
c ---[2363]---> Adder-cost: 72   maxlim: 12544   bits: 15/14
c ---[2361]---> Adder-cost: 72   maxlim: 12544   bits: 15/14
c ---[2359]---> Adder-cost: 72   maxlim: 12544   bits: 15/14
c ---[2357]---> Adder-cost: 190   maxlim: 13312   bits: 15/14
c ---[2355]---> Sorter-cost:  473     Base: 2 2 2 2 2 2 2 7
c ---[2353]---> Adder-cost: 78   maxlim: 13312   bits: 15/14
c ---[2351]---> Adder-cost: 158   maxlim: 9984   bits: 15/14
c ---[2349]---> Adder-cost: 62   maxlim: 9984   bits: 15/14
c ---[2347]---> Adder-cost: 162   maxlim: 11136   bits: 15/14
c ---[2345]---> Adder-cost: 68   maxlim: 11136   bits: 15/14
c ---[2343]---> Adder-cost: 114   maxlim: 8064   bits: 14/13
c ---[2341]---> Adder-cost: 50   maxlim: 8064   bits: 14/13
c ---[2339]---> Adder-cost: 90   maxlim: 6016   bits: 14/13
c ---[2337]---> Adder-cost: 40   maxlim: 6016   bits: 14/13
c ---[2335]---> Adder-cost: 96   maxlim: 6272   bits: 14/13
c ---[2333]---> Adder-cost: 80   maxlim: 6144   bits: 14/13
c ---[2331]---> Adder-cost: 76   maxlim: 5120   bits: 14/13
c ---[2329]---> Adder-cost: 84   maxlim: 5376   bits: 14/13
c ---[2327]---> Sorter-cost:  786     Base: 2 2 2 2 2 2 2 7
c ---[2325]---> Sorter-cost:  404     Base: 2 2 2 2 2 2 2 7
c ---[2323]---> Sorter-cost:  734     Base: 2 2 2 2 2 2 2 7
c ---[2321]---> Sorter-cost:  560     Base: 2 2 2 2 2 2 2 7
c ---[2319]---> Sorter-cost:  575     Base: 2 2 2 2 2 2 2 7
c ---[2317]---> Adder-cost: 96   maxlim: 5888   bits: 14/13
c ---[2315]---> Sorter-cost:  362     Base: 2 2 2 2 2 2 2 7
c ---[2313]---> Sorter-cost:  304     Base: 2 2 2 2 2 2 2 2
c ---[2311]---> Sorter-cost:  176     Base: 2 2 2 2 2 2 2 2
c ---[2309]---> Sorter-cost:  425     Base: 2 2 2 2 2 2 2 7
c ---[2307]---> Sorter-cost:  431     Base: 2 2 2 2 2 2 2 7
c ---[2305]---> Sorter-cost:  442     Base: 2 2 2 2 2 2 2 7
c ---[2303]---> Sorter-cost:  306     Base: 2 2 2 2 2 2 2 7
c ---[2301]---> Sorter-cost:  534     Base: 2 2 2 2 2 2 2 7
c ---[2299]---> Adder-cost: 68   maxlim: 6016   bits: 14/13
c ---[2297]---> Sorter-cost:  366     Base: 2 2 2 2 2 2 2 7
c ---[2295]---> Sorter-cost:  246     Base: 2 2 2 2 2 2 2 7
c ---[2293]---> Sorter-cost:  246     Base: 2 2 2 2 2 2 2 7
c ---[2291]---> Sorter-cost:  310     Base: 2 2 2 2 2 2 2 2
c ---[2289]---> Sorter-cost:  768     Base: 2 2 2 2 2 2 2 7
c ---[2287]---> Sorter-cost:  404     Base: 2 2 2 2 2 2 2 7
c ---[2285]---> Sorter-cost:  598     Base: 2 2 2 2 2 2 2 7
c ---[2283]---> Sorter-cost:  560     Base: 2 2 2 2 2 2 2 7
c ---[2281]---> Sorter-cost:  665     Base: 2 2 2 2 2 2 2 7
c ---[2279]---> Sorter-cost:  517     Base: 2 2 2 2 2 2 2 7
c ---[2277]---> Sorter-cost:  610     Base: 2 2 2 2 2 2 2 7
c ---[2275]---> Sorter-cost:  452     Base: 2 2 2 2 2 2 2 7
c ---[2273]---> Sorter-cost:  877     Base: 2 2 2 2 2 2 2 7
c ---[2271]---> Sorter-cost:  621     Base: 2 2 2 2 2 2 2 7
c ---[2269]---> Sorter-cost:  665     Base: 2 2 2 2 2 2 2 7
c ---[2267]---> Sorter-cost:  517     Base: 2 2 2 2 2 2 2 7
c ---[2265]---> Sorter-cost:  629     Base: 2 2 2 2 2 2 2 7
c ---[2263]---> Sorter-cost:  517     Base: 2 2 2 2 2 2 2 7
c ---[2261]---> Sorter-cost:  517     Base: 2 2 2 2 2 2 2 7
c ---[2259]---> Sorter-cost:  517     Base: 2 2 2 2 2 2 2 7
c ---[2257]---> Sorter-cost: 1072     Base: 2 2 2 2 2 2 2 7
c ---[2255]---> Sorter-cost:  710     Base: 2 2 2 2 2 2 2 7
c ---[2253]---> Sorter-cost:  268     Base: 2 2 2 2 2 2 2 2
c ---[2251]---> Sorter-cost:  358     Base: 2 2 2 2 2 2 2 7
c ---[2249]---> Sorter-cost:  616     Base: 2 2 2 2 2 2 2 7
c ---[2247]---> Sorter-cost:  452     Base: 2 2 2 2 2 2 2 7
c ---[2245]---> Sorter-cost: 1019     Base: 2 2 2 2 2 2 2 7
c ---[2243]---> Adder-cost: 82   maxlim: 4864   bits: 14/13
c ---[2241]---> Adder-cost: 88   maxlim: 5120   bits: 14/13
c ---[2239]---> Sorter-cost:  717     Base: 2 2 2 2 2 2 2 7
c ---[2237]---> Sorter-cost:  541     Base: 2 2 2 2 2 2 2 7
c ---[2235]---> Adder-cost: 134   maxlim: 8320   bits: 15/14
c ---[2233]---> Adder-cost: 88   maxlim: 5120   bits: 14/13
c ---[2231]---> Sorter-cost:  736     Base: 2 2 2 2 2 2 2 7
c ---[2229]---> Sorter-cost:  713     Base: 2 2 2 2 2 2 2 7
c ---[2227]---> Adder-cost: 62   maxlim: 4480   bits: 14/13
c ---[2225]---> Sorter-cost:  266     Base: 2 2 2 2 2 2 2 2
c ---[2223]---> Sorter-cost:  907     Base: 2 2 2 2 2 2 2 7
c ---[2221]---> Sorter-cost:  730     Base: 2 2 2 2 2 2 2 7
c ---[2219]---> Sorter-cost:  421     Base: 2 2 2 2 2 2 2 7
c ---[2217]---> Sorter-cost:  352     Base: 2 2 2 2 2 2 2 7
c ---[2215]---> Sorter-cost:  314     Base: 2 2 2 2 2 2 2 2
c ---[2213]---> Adder-cost: 80   maxlim: 4992   bits: 14/13
c ---[2211]---> Adder-cost: 118   maxlim: 7296   bits: 14/13
c ---[2209]---> Sorter-cost:  419     Base: 2 2 2 2 2 2 2 7
c ---[2207]---> Sorter-cost:  934     Base: 2 2 2 2 2 2 2 7
c ---[2205]---> Sorter-cost:  691     Base: 2 2 2 2 2 2 2 7
c ---[2203]---> Sorter-cost:  441     Base: 2 2 2 2 2 2 2 7
c ---[2201]---> Sorter-cost:  329     Base: 2 2 2 2 2 2 2 7
c ---[2199]---> Sorter-cost:  329     Base: 2 2 2 2 2 2 2 7
c ---[2197]---> Adder-cost: 48   maxlim: 7296   bits: 14/13
c ---[2195]---> Sorter-cost:  329     Base: 2 2 2 2 2 2 2 7
c ---[2193]---> Sorter-cost:  648     Base: 2 2 2 2 2 2 2 7
c ---[2191]---> Sorter-cost:  561     Base: 2 2 2 2 2 2 2 7
c ---[2189]---> Sorter-cost:  402     Base: 2 2 2 2 2 2 2 7
c ---[2187]---> Sorter-cost:  397     Base: 2 2 2 2 2 2 2 7
c ---[2185]---> Sorter-cost:  388     Base: 2 2 2 2 2 2 2 7
c ---[2183]---> Sorter-cost:  290     Base: 2 2 2 2 2 2 2 2
c ---[2181]---> Sorter-cost:  426     Base: 2 2 2 2 2 2 2 7
c ---[2179]---> Sorter-cost:  713     Base: 2 2 2 2 2 2 2 7
c ---[2177]---> Adder-cost: 192   maxlim: 12928   bits: 15/14
c ---[2175]---> Adder-cost: 76   maxlim: 12928   bits: 15/14
c ---[2173]---> Adder-cost: 124   maxlim: 8704   bits: 15/14
c ---[2171]---> Adder-cost: 62   maxlim: 8704   bits: 15/14
c ---[2169]---> Adder-cost: 138   maxlim: 10752   bits: 15/14
c ---[2167]---> Adder-cost: 66   maxlim: 10752   bits: 15/14
c ---[2165]---> Adder-cost: 112   maxlim: 7680   bits: 14/13
c ---[2163]---> Adder-cost: 50   maxlim: 7680   bits: 14/13
c ---[2161]---> Adder-cost: 66   maxlim: 6784   bits: 14/13
c ---[2159]---> Adder-cost: 46   maxlim: 6784   bits: 14/13
c ---[2157]---> Adder-cost: 82   maxlim: 5632   bits: 14/13
c ---[2155]---> Adder-cost: 42   maxlim: 5632   bits: 14/13
c ---[2153]---> Adder-cost: 84   maxlim: 5888   bits: 14/13
c ---[2151]---> Adder-cost: 40   maxlim: 5888   bits: 14/13
c ---[2149]---> Sorter-cost:  711     Base: 2 2 2 2 2 2 2 7
c ---[2147]---> Sorter-cost:  541     Base: 2 2 2 2 2 2 2 7
c ---[2145]---> Adder-cost: 110   maxlim: 8320   bits: 15/14
c ---[2143]---> Adder-cost: 94   maxlim: 5760   bits: 14/13
c ---[2141]---> Adder-cost: 60   maxlim: 8320   bits: 15/14
c ---[2139]---> Adder-cost: 144   maxlim: 9216   bits: 15/14
c ---[2137]---> Adder-cost: 62   maxlim: 9216   bits: 15/14
c ---[2135]---> Adder-cost: 90   maxlim: 6400   bits: 14/13
c ---[2133]---> Adder-cost: 44   maxlim: 6400   bits: 14/13
c ---[2131]---> Adder-cost: 98   maxlim: 6400   bits: 14/13
c ---[2129]---> Adder-cost: 82   maxlim: 6144   bits: 14/13
c ---[2127]---> Sorter-cost:  691     Base: 2 2 2 2 2 2 2 7
c ---[2125]---> Adder-cost: 90   maxlim: 5888   bits: 14/13
c ---[2123]---> Sorter-cost:  715     Base: 2 2 2 2 2 2 2 7
c ---[2121]---> Sorter-cost:  541     Base: 2 2 2 2 2 2 2 7
c ---[2119]---> Adder-cost: 74   maxlim: 4352   bits: 14/13
c ---[2117]---> Sorter-cost:  561     Base: 2 2 2 2 2 2 2 7
c ---[2115]---> Sorter-cost:  515     Base: 2 2 2 2 2 2 2 7
c ---[2113]---> Sorter-cost:  437     Base: 2 2 2 2 2 2 2 7
c ---[2111]---> Sorter-cost:  386     Base: 2 2 2 2 2 2 2 7
c ---[2109]---> Sorter-cost:  280     Base: 2 2 2 2 2 2 2 7
c ---[2107]---> Sorter-cost:  686     Base: 2 2 2 2 2 2 2 7
c ---[2105]---> Sorter-cost:  560     Base: 2 2 2 2 2 2 2 7
c ---[2103]---> Sorter-cost:  760     Base: 2 2 2 2 2 2 2 7
c ---[2101]---> Sorter-cost:  404     Base: 2 2 2 2 2 2 2 7
c ---[2099]---> Sorter-cost:  954     Base: 2 2 2 2 2 2 2 7
c ---[2097]---> Sorter-cost:  584     Base: 2 2 2 2 2 2 2 7
c ---[2095]---> Adder-cost: 118   maxlim: 7424   bits: 14/13
c ---[2093]---> Sorter-cost:  593     Base: 2 2 2 2 2 2 2 7
c ---[2091]---> Sorter-cost:  473     Base: 2 2 2 2 2 2 2 7
c ---[2089]---> Sorter-cost:  683     Base: 2 2 2 2 2 2 2 7
c ---[2087]---> Sorter-cost:  517     Base: 2 2 2 2 2 2 2 7
c ---[2085]---> Sorter-cost:  465     Base: 2 2 2 2 2 2 2 7
c ---[2083]---> Sorter-cost:  433     Base: 2 2 2 2 2 2 2 7
c ---[2081]---> Sorter-cost:  430     Base: 2 2 2 2 2 2 2 7
c ---[2079]---> Sorter-cost:  306     Base: 2 2 2 2 2 2 2 7
c ---[2077]---> Sorter-cost:  586     Base: 2 2 2 2 2 2 2 7
c ---[2075]---> Sorter-cost:  564     Base: 2 2 2 2 2 2 2 7
c ---[2073]---> Adder-cost: 70   maxlim: 7040   bits: 14/13
c ---[2071]---> Sorter-cost:  546     Base: 2 2 2 2 2 2 2 7
c ---[2069]---> Sorter-cost:  580     Base: 2 2 2 2 2 2 2 7
c ---[2067]---> Sorter-cost:  714     Base: 2 2 2 2 2 2 2 7
c ---[2065]---> Adder-cost: 76   maxlim: 4480   bits: 14/13
c ---[2063]---> Adder-cost: 184   maxlim: 11392   bits: 15/14
c ---[2061]---> Adder-cost: 168   maxlim: 11008   bits: 15/14
c ---[2059]---> Sorter-cost:  370     Base: 2 2 2 2 2 2 2 7
c ---[2057]---> Adder-cost: 104   maxlim: 7680   bits: 14/13
c ---[2055]---> Adder-cost: 50   maxlim: 7680   bits: 14/13
c ---[2053]---> Adder-cost: 88   maxlim: 7296   bits: 14/13
c ---[2051]---> Adder-cost: 48   maxlim: 7296   bits: 14/13
c ---[2049]---> Adder-cost: 86   maxlim: 6528   bits: 14/13
c ---[2047]---> Adder-cost: 44   maxlim: 6528   bits: 14/13
c ---[2045]---> Adder-cost: 68   maxlim: 4736   bits: 14/13
c ---[2043]---> Adder-cost: 90   maxlim: 5504   bits: 14/13
c ---[2041]---> Adder-cost: 74   maxlim: 6656   bits: 14/13
c ---[2039]---> Adder-cost: 48   maxlim: 6656   bits: 14/13
c ---[2037]---> Adder-cost: 80   maxlim: 7040   bits: 14/13
c ---[2035]---> Adder-cost: 90   maxlim: 5760   bits: 14/13
c ---[2033]---> Adder-cost: 82   maxlim: 5504   bits: 14/13
c ---[2031]---> Sorter-cost:  994     Base: 2 2 2 2 2 2 2 7
c ---[2029]---> Sorter-cost:  732     Base: 2 2 2 2 2 2 2 7
c ---[2027]---> Adder-cost: 82   maxlim: 4992   bits: 14/13
c ---[2025]---> Adder-cost: 154   maxlim: 9344   bits: 15/14
c ---[2023]---> Sorter-cost:  730     Base: 2 2 2 2 2 2 2 7
c ---[2021]---> Adder-cost: 100   maxlim: 7808   bits: 14/13
c ---[2019]---> Sorter-cost:  633     Base: 2 2 2 2 2 2 2 7
c ---[2017]---> Sorter-cost:  681     Base: 2 2 2 2 2 2 2 7
c ---[2015]---> Sorter-cost:  976     Base: 2 2 2 2 2 2 2 7
c ---[2013]---> Sorter-cost:  976     Base: 2 2 2 2 2 2 2 7
c ---[2011]---> Adder-cost: 146   maxlim: 8704   bits: 15/14
c ---[2009]---> Adder-cost: 82   maxlim: 4992   bits: 14/13
c ---[2007]---> Sorter-cost:  691     Base: 2 2 2 2 2 2 2 7
c ---[2005]---> Adder-cost: 76   maxlim: 4352   bits: 14/13
c ---[2003]---> Sorter-cost:  786     Base: 2 2 2 2 2 2 2 7
c ---[2001]---> Sorter-cost:  560     Base: 2 2 2 2 2 2 2 7
c ---[1999]---> Adder-cost: 120   maxlim: 7552   bits: 14/13
c ---[1997]---> Sorter-cost:  370     Base: 2 2 2 2 2 2 2 7
c ---[1995]---> Sorter-cost:  734     Base: 2 2 2 2 2 2 2 7
c ---[1993]---> Sorter-cost:  695     Base: 2 2 2 2 2 2 2 7
c ---[1991]---> Sorter-cost:  541     Base: 2 2 2 2 2 2 2 7
c ---[1989]---> Sorter-cost:  310     Base: 2 2 2 2 2 2 2 2
c ---[1987]---> Adder-cost: 230   maxlim: 14336   bits: 15/14
c ---[1985]---> Adder-cost: 140   maxlim: 14208   bits: 15/14
c ---[1983]---> Adder-cost: 104   maxlim: 6528   bits: 14/13
c ---[1981]---> Adder-cost: 184   maxlim: 12800   bits: 15/14
c ---[1979]---> Adder-cost: 248   maxlim: 15616   bits: 15/14
c ---[1977]---> Adder-cost: 78   maxlim: 15616   bits: 15/14
c ---[1975]---> Adder-cost: 166   maxlim: 10624   bits: 15/14
c ---[1973]---> Sorter-cost:  996     Base: 2 2 2 2 2 2 2 7
c ---[1971]---> Sorter-cost:  571     Base: 2 2 2 2 2 2 2 7
c ---[1969]---> Sorter-cost:  437     Base: 2 2 2 2 2 2 2 7
c ---[1967]---> Sorter-cost:  681     Base: 2 2 2 2 2 2 2 7
c ---[1965]---> Adder-cost: 76   maxlim: 4480   bits: 14/13
c ---[1963]---> Adder-cost: 48   maxlim: 4480   bits: 14/13
c ---[1961]---> Sorter-cost:  438     Base: 2 2 2 2 2 2 2 7
c ---[1959]---> Adder-cost: 112   maxlim: 7040   bits: 14/13
c ---[1957]---> Sorter-cost:  372     Base: 2 2 2 2 2 2 2 7
c ---[1955]---> Sorter-cost:  784     Base: 2 2 2 2 2 2 2 7
c ---[1953]---> Sorter-cost:  421     Base: 2 2 2 2 2 2 2 7
c ---[1951]---> Sorter-cost:  569     Base: 2 2 2 2 2 2 2 7
c ---[1949]---> Sorter-cost:  645     Base: 2 2 2 2 2 2 2 7
c ---[1947]---> Sorter-cost:  602     Base: 2 2 2 2 2 2 2 7
c ---[1945]---> Sorter-cost:  631     Base: 2 2 2 2 2 2 2 7
c ---[1943]---> Adder-cost: 96   maxlim: 6016   bits: 14/13
c ---[1941]---> Sorter-cost:  726     Base: 2 2 2 2 2 2 2 7
c ---[1939]---> Sorter-cost:  663     Base: 2 2 2 2 2 2 2 7
c ---[1937]---> Sorter-cost:  507     Base: 2 2 2 2 2 2 2 7
c ---[1935]---> Adder-cost: 184   maxlim: 11392   bits: 15/14
c ---[1933]---> Adder-cost: 268   maxlim: 16896   bits: 16/15
c ---[1931]---> Adder-cost: 82   maxlim: 4992   bits: 14/13
c ---[1929]---> Adder-cost: 40   maxlim: 6016   bits: 14/13
c ---[1927]---> Adder-cost: 136   maxlim: 8448   bits: 15/14
c ---[1925]---> Adder-cost: 208   maxlim: 12800   bits: 15/14
c ---[1923]---> Adder-cost: 88   maxlim: 5248   bits: 14/13
c ---[1921]---> Sorter-cost:  639     Base: 2 2 2 2 2 2 2 7
c ---[1919]---> Sorter-cost:  717     Base: 2 2 2 2 2 2 2 7
c ---[1917]---> Adder-cost: 72   maxlim: 6016   bits: 14/13
c ---[1915]---> Adder-cost: 234   maxlim: 14848   bits: 15/14
c ---[1913]---> Adder-cost: 80   maxlim: 14848   bits: 15/14
c ---[1911]---> Adder-cost: 214   maxlim: 14336   bits: 15/14
c ---[1909]---> Adder-cost: 132   maxlim: 8192   bits: 15/14
c ---[1907]---> Adder-cost: 202   maxlim: 12928   bits: 15/14
c ---[1905]---> Adder-cost: 104   maxlim: 6528   bits: 14/13
c ---[1903]---> Adder-cost: 74   maxlim: 4992   bits: 14/13
c ---[1901]---> Adder-cost: 40   maxlim: 6016   bits: 14/13
c ---[1899]---> Sorter-cost:  268     Base: 2 2 2 2 2 2 2 2
c ---[1897]---> Sorter-cost:  440     Base: 2 2 2 2 2 2 2 7
c ---[1895]---> Sorter-cost:  419     Base: 2 2 2 2 2 2 2 7
c ---[1893]---> Sorter-cost:  266     Base: 2 2 2 2 2 2 2 2
c ---[1891]---> Adder-cost: 202   maxlim: 15104   bits: 15/14
c ---[1889]---> Adder-cost: 230   maxlim: 15616   bits: 15/14
c ---[1887]---> Adder-cost: 182   maxlim: 11648   bits: 15/14
c ---[1885]---> Adder-cost: 92   maxlim: 5760   bits: 14/13
c ---[1883]---> Adder-cost: 182   maxlim: 11520   bits: 15/14
c ---[1881]---> Adder-cost: 138   maxlim: 9728   bits: 15/14
c ---[1879]---> Adder-cost: 126   maxlim: 9088   bits: 15/14
c ---[1877]---> Adder-cost: 102   maxlim: 8960   bits: 15/14
c ---[1875]---> Adder-cost: 222   maxlim: 14208   bits: 15/14
c ---[1873]---> Adder-cost: 270   maxlim: 17280   bits: 16/15
c ---[1871]---> Adder-cost: 190   maxlim: 17408   bits: 16/15
c ---[1869]---> Adder-cost: 42   maxlim: 5760   bits: 14/13
c ---[1867]---> Adder-cost: 102   maxlim: 6144   bits: 14/13
c ---[1865]---> Sorter-cost:  447     Base: 2 2 2 2 2 2 2 7
c ---[1863]---> Adder-cost: 112   maxlim: 6912   bits: 14/13
c ---[1861]---> Adder-cost: 112   maxlim: 7552   bits: 14/13
c ---[1859]---> Adder-cost: 364   maxlim: 23296   bits: 16/15
c ---[1857]---> Adder-cost: 174   maxlim: 11136   bits: 15/14
c ---[1855]---> Adder-cost: 112   maxlim: 9344   bits: 15/14
c ---[1853]---> Adder-cost: 96   maxlim: 8192   bits: 15/14
c ---[1851]---> Adder-cost: 154   maxlim: 9216   bits: 15/14
c ---[1849]---> Adder-cost: 104   maxlim: 6528   bits: 14/13
c ---[1847]---> Adder-cost: 88   maxlim: 5376   bits: 14/13
c ---[1845]---> Sorter-cost:  419     Base: 2 2 2 2 2 2 2 7
c ---[1843]---> Adder-cost: 82   maxlim: 4864   bits: 14/13
c ---[1841]---> Adder-cost: 260   maxlim: 16768   bits: 16/15
c ---[1839]---> Adder-cost: 98   maxlim: 6272   bits: 14/13
c ---[1837]---> Sorter-cost:  996     Base: 2 2 2 2 2 2 2 7
c ---[1835]---> Sorter-cost:  573     Base: 2 2 2 2 2 2 2 7
c ---[1833]---> Adder-cost: 162   maxlim: 10112   bits: 15/14
c ---[1831]---> Adder-cost: 142   maxlim: 9088   bits: 15/14
c ---[1829]---> Adder-cost: 156   maxlim: 9600   bits: 15/14
c ---[1827]---> Adder-cost: 62   maxlim: 9600   bits: 15/14
c ---[1825]---> Adder-cost: 102   maxlim: 6144   bits: 14/13
c ---[1823]---> Adder-cost: 184   maxlim: 11776   bits: 15/14
c ---[1821]---> Adder-cost: 112   maxlim: 7424   bits: 14/13
c ---[1819]---> Adder-cost: 168   maxlim: 10496   bits: 15/14
c ---[1817]---> Adder-cost: 92   maxlim: 9856   bits: 15/14
c ---[1815]---> Adder-cost: 162   maxlim: 10112   bits: 15/14
c ---[1813]---> Adder-cost: 74   maxlim: 10112   bits: 15/14
c ---[1811]---> Adder-cost: 110   maxlim: 7040   bits: 14/13
c ---[1809]---> Adder-cost: 176   maxlim: 12800   bits: 15/14
c ---[1807]---> Adder-cost: 212   maxlim: 15360   bits: 15/14
c ---[1805]---> Adder-cost: 172   maxlim: 17536   bits: 16/15
c ---[1803]---> Adder-cost: 174   maxlim: 17152   bits: 16/15
c ---[1801]---> Adder-cost: 108   maxlim: 6784   bits: 14/13
c ---[1799]---> Adder-cost: 136   maxlim: 8192   bits: 15/14
c ---[1797]---> Sorter-cost:  578     Base: 2 2 2 2 2 2 2 7
c ---[1795]---> Sorter-cost:  467     Base: 2 2 2 2 2 2 2 7
c ---[1793]---> Sorter-cost:  640     Base: 2 2 2 2 2 2 2 7
c ---[1791]---> Adder-cost: 140   maxlim: 8448   bits: 15/14
c ---[1789]---> Sorter-cost:  594     Base: 2 2 2 2 2 2 2 7
c ---[1787]---> Adder-cost: 204   maxlim: 12800   bits: 15/14
c ---[1785]---> Adder-cost: 336   maxlim: 22528   bits: 16/15
c ---[1783]---> Adder-cost: 82   maxlim: 4864   bits: 14/13
c ---[1781]---> Sorter-cost:  314     Base: 2 2 2 2 2 2 2 2
c ---[1779]---> Adder-cost: 98   maxlim: 6144   bits: 14/13
c ---[1777]---> Adder-cost: 60   maxlim: 8448   bits: 15/14
c ---[1775]---> Adder-cost: 58   maxlim: 6016   bits: 14/13
c ---[1773]---> Sorter-cost:  715     Base: 2 2 2 2 2 2 2 7
c ---[1771]---> Sorter-cost:  691     Base: 2 2 2 2 2 2 2 7
c ---[1769]---> Adder-cost: 136   maxlim: 8832   bits: 15/14
c ---[1767]---> Adder-cost: 144   maxlim: 8960   bits: 15/14
c ---[1765]---> Sorter-cost:  590     Base: 2 2 2 2 2 2 2 7
c ---[1763]---> Sorter-cost:  430     Base: 2 2 2 2 2 2 2 7
c ---[1761]---> Adder-cost: 68   maxlim: 4352   bits: 14/13
c ---[1759]---> Adder-cost: 144   maxlim: 8704   bits: 15/14
c ---[1757]---> Sorter-cost:  264     Base: 2 2 2 2 2 2 2 2
c ---[1755]---> Adder-cost: 156   maxlim: 14208   bits: 15/14
c ---[1753]---> Sorter-cost:  264     Base: 2 2 2 2 2 2 2 2
c ---[1751]---> Adder-cost: 136   maxlim: 8576   bits: 15/14
c ---[1749]---> Adder-cost: 216   maxlim: 13952   bits: 15/14
c ---[1747]---> Adder-cost: 170   maxlim: 10752   bits: 15/14
c ---[1745]---> Adder-cost: 94   maxlim: 5760   bits: 14/13
c ---[1743]---> Adder-cost: 112   maxlim: 7424   bits: 14/13
c ---[1741]---> Adder-cost: 78   maxlim: 5504   bits: 14/13
c ---[1739]---> Adder-cost: 110   maxlim: 7040   bits: 14/13
c ---[1737]---> Adder-cost: 220   maxlim: 15744   bits: 15/14
c ---[1735]---> Adder-cost: 146   maxlim: 9472   bits: 15/14
c ---[1733]---> Adder-cost: 132   maxlim: 8448   bits: 15/14
c ---[1731]---> Sorter-cost:  934     Base: 2 2 2 2 2 2 2 7
c ---[1729]---> Adder-cost: 178   maxlim: 11008   bits: 15/14
c ---[1727]---> Adder-cost: 90   maxlim: 5504   bits: 14/13
c ---[1725]---> Adder-cost: 68   maxlim: 11008   bits: 15/14
c ---[1723]---> Adder-cost: 216   maxlim: 13696   bits: 15/14
c ---[1721]---> Adder-cost: 176   maxlim: 11904   bits: 15/14
c ---[1719]---> Adder-cost: 152   maxlim: 12032   bits: 15/14
c ---[1717]---> Adder-cost: 120   maxlim: 7424   bits: 14/13
c ---[1715]---> Sorter-cost:  408     Base: 2 2 2 2 2 2 2 7
c ---[1713]---> Sorter-cost:  248     Base: 2 2 2 2 2 2 2 2
c ---[1711]---> Sorter-cost:  996     Base: 2 2 2 2 2 2 2 7
c ---[1709]---> Sorter-cost:  465     Base: 2 2 2 2 2 2 2 7
c ---[1707]---> Sorter-cost:  358     Base: 2 2 2 2 2 2 2 7
c ---[1705]---> Adder-cost: 332   maxlim: 20480   bits: 16/15
c ---[1703]---> Adder-cost: 314   maxlim: 20352   bits: 16/15
c ---[1701]---> Adder-cost: 234   maxlim: 16768   bits: 16/15
c ---[1699]---> Adder-cost: 168   maxlim: 11008   bits: 15/14
c ---[1697]---> Adder-cost: 112   maxlim: 7168   bits: 14/13
c ---[1695]---> Adder-cost: 160   maxlim: 9984   bits: 15/14
c ---[1693]---> Sorter-cost: 1078     Base: 2 2 2 2 2 2 2 7
c ---[1691]---> Adder-cost: 212   maxlim: 15104   bits: 15/14
c ---[1689]---> Adder-cost: 172   maxlim: 14976   bits: 15/14
c ---[1687]---> Adder-cost: 76   maxlim: 4736   bits: 14/13
c ---[1685]---> Adder-cost: 142   maxlim: 8576   bits: 15/14
c ---[1683]---> Sorter-cost:  736     Base: 2 2 2 2 2 2 2 7
c ---[1681]---> Sorter-cost:  963     Base: 2 2 2 2 2 2 2 7
c ---[1679]---> Adder-cost: 162   maxlim: 10112   bits: 15/14
c ---[1677]---> Adder-cost: 120   maxlim: 7424   bits: 14/13
c ---[1675]---> Adder-cost: 124   maxlim: 7808   bits: 14/13
c ---[1673]---> Sorter-cost:  421     Base: 2 2 2 2 2 2 2 7
c ---[1671]---> Sorter-cost:  616     Base: 2 2 2 2 2 2 2 7
c ---[1669]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 7
c ---[1667]---> Sorter-cost:  571     Base: 2 2 2 2 2 2 2 7
c ---[1665]---> Sorter-cost: 1001     Base: 2 2 2 2 2 2 2 7
c ---[1663]---> Sorter-cost:  463     Base: 2 2 2 2 2 2 2 7
c ---[1661]---> Sorter-cost:  586     Base: 2 2 2 2 2 2 2 7
c ---[1659]---> Sorter-cost:  463     Base: 2 2 2 2 2 2 2 7
c ---[1657]---> Sorter-cost:  590     Base: 2 2 2 2 2 2 2 7
c ---[1655]---> Adder-cost: 120   maxlim: 7552   bits: 14/13
c ---[1653]---> Sorter-cost:  930     Base: 2 2 2 2 2 2 2 7
c ---[1651]---> Sorter-cost:  892     Base: 2 2 2 2 2 2 2 7
c ---[1649]---> Sorter-cost:  314     Base: 2 2 2 2 2 2 2 2
c ---[1647]---> Sorter-cost:  176     Base: 2 2 2 2 2 2 2 2
c ---[1645]---> Adder-cost: 394   maxlim: 25088   bits: 16/15
c ---[1643]---> Adder-cost: 354   maxlim: 23040   bits: 16/15
c ---[1641]---> Adder-cost: 208   maxlim: 23296   bits: 16/15
c ---[1639]---> Sorter-cost:  907     Base: 2 2 2 2 2 2 2 7
c ---[1637]---> Adder-cost: 86   maxlim: 5376   bits: 14/13
c ---[1635]---> Sorter-cost:  878     Base: 2 2 2 2 2 2 2 7
c ---[1633]---> Adder-cost: 228   maxlim: 15232   bits: 15/14
c ---[1631]---> Sorter-cost:  312     Base: 2 2 2 2 2 2 2 2
c ---[1629]---> Adder-cost: 142   maxlim: 9216   bits: 15/14
c ---[1627]---> Adder-cost: 124   maxlim: 7808   bits: 14/13
c ---[1625]---> Adder-cost: 104   maxlim: 7680   bits: 14/13
c ---[1623]---> Sorter-cost:  575     Base: 2 2 2 2 2 2 2 7
c ---[1621]---> Sorter-cost:  731     Base: 2 2 2 2 2 2 2 7
c ---[1619]---> Adder-cost: 90   maxlim: 5760   bits: 14/13
c ---[1617]---> Adder-cost: 76   maxlim: 6272   bits: 14/13
c ---[1615]---> Adder-cost: 76   maxlim: 4864   bits: 14/13
c ---[1613]---> Adder-cost: 62   maxlim: 4736   bits: 14/13
c ---[1611]---> Sorter-cost:  635     Base: 2 2 2 2 2 2 2 7
c ---[1609]---> Sorter-cost:  314     Base: 2 2 2 2 2 2 2 2
c ---[1607]---> Adder-cost: 110   maxlim: 6784   bits: 14/13
c ---[1605]---> Adder-cost: 150   maxlim: 9728   bits: 15/14
c ---[1603]---> Adder-cost: 112   maxlim: 7168   bits: 14/13
c ---[1601]---> Adder-cost: 104   maxlim: 6272   bits: 14/13
c ---[1599]---> Sorter-cost:  447     Base: 2 2 2 2 2 2 2 7
c ---[1597]---> Sorter-cost:  316     Base: 2 2 2 2 2 2 2 7
c ---[1595]---> Sorter-cost:  443     Base: 2 2 2 2 2 2 2 7
c ---[1593]---> Sorter-cost:  311     Base: 2 2 2 2 2 2 2 7
c ---[1591]---> Sorter-cost:  396     Base: 2 2 2 2 2 2 2 7
c ---[1589]---> Sorter-cost:  268     Base: 2 2 2 2 2 2 2 2
c ---[1587]---> Adder-cost: 160   maxlim: 10112   bits: 15/14
c ---[1585]---> Adder-cost: 152   maxlim: 10112   bits: 15/14
c ---[1583]---> Sorter-cost:  786     Base: 2 2 2 2 2 2 2 7
c ---[1581]---> Adder-cost: 82   maxlim: 4992   bits: 14/13
c ---[1579]---> Sorter-cost:  268     Base: 2 2 2 2 2 2 2 2
c ---[1577]---> Adder-cost: 88   maxlim: 5376   bits: 14/13
c ---[1575]---> Adder-cost: 106   maxlim: 7552   bits: 14/13
c ---[1573]---> Adder-cost: 166   maxlim: 10240   bits: 15/14
c ---[1571]---> Sorter-cost:  996     Base: 2 2 2 2 2 2 2 7
c ---[1569]---> Sorter-cost:  268     Base: 2 2 2 2 2 2 2 2
c ---[1567]---> Sorter-cost:  180     Base: 2 2 2 2 2 2 2 2
c ---[1565]---> Adder-cost: 336   maxlim: 20992   bits: 16/15
c ---[1563]---> Adder-cost: 324   maxlim: 21120   bits: 16/15
c ---[1561]---> Adder-cost: 246   maxlim: 15360   bits: 15/14
c ---[1559]---> Adder-cost: 200   maxlim: 13312   bits: 15/14
c ---[1557]---> Sorter-cost:  874     Base: 2 2 2 2 2 2 2 7
c ---[1555]---> Adder-cost: 296   maxlim: 18944   bits: 16/15
c ---[1553]---> Adder-cost: 244   maxlim: 24064   bits: 16/15
c ---[1551]---> Adder-cost: 240   maxlim: 16384   bits: 16/15
c ---[1549]---> Adder-cost: 188   maxlim: 11904   bits: 15/14
c ---[1547]---> Adder-cost: 124   maxlim: 9856   bits: 15/14
c ---[1545]---> Sorter-cost:  910     Base: 2 2 2 2 2 2 2 7
c ---[1543]---> Adder-cost: 92   maxlim: 5888   bits: 14/13
c ---[1541]---> Sorter-cost:  895     Base: 2 2 2 2 2 2 2 7
c ---[1539]---> Sorter-cost:  758     Base: 2 2 2 2 2 2 2 7
c ---[1537]---> Sorter-cost:  670     Base: 2 2 2 2 2 2 2 7
c ---[1535]---> BDD-cost:   56
c ---[1533]---> Sorter-cost:  246     Base: 2 2 2 2 2 2 2 2
c ---[1531]---> Sorter-cost:  676     Base: 2 2 2 2 2 2 2 7
c ---[1529]---> Adder-cost: 96   maxlim: 5888   bits: 14/13
c ---[1527]---> Sorter-cost:  736     Base: 2 2 2 2 2 2 2 7
c ---[1525]---> Adder-cost: 108   maxlim: 6784   bits: 14/13
c ---[1523]---> Adder-cost: 104   maxlim: 6272   bits: 14/13
c ---[1521]---> Adder-cost: 46   maxlim: 6272   bits: 14/13
c ---[1519]---> Adder-cost: 102   maxlim: 6400   bits: 14/13
c ---[1517]---> Adder-cost: 44   maxlim: 6400   bits: 14/13
c ---[1515]---> Adder-cost: 116   maxlim: 8192   bits: 15/14
c ---[1513]---> Sorter-cost:  268     Base: 2 2 2 2 2 2 2 2
c ---[1511]---> Adder-cost: 96   maxlim: 8576   bits: 15/14
c ---[1509]---> Adder-cost: 202   maxlim: 12800   bits: 15/14
c ---[1507]---> Adder-cost: 240   maxlim: 15360   bits: 15/14
c ---[1505]---> Adder-cost: 150   maxlim: 9856   bits: 15/14
c ---[1503]---> Adder-cost: 140   maxlim: 9344   bits: 15/14
c ---[1501]---> Adder-cost: 128   maxlim: 9088   bits: 15/14
c ---[1499]---> Sorter-cost:  996     Base: 2 2 2 2 2 2 2 7
c ---[1497]---> Sorter-cost:  604     Base: 2 2 2 2 2 2 2 7
c ---[1495]---> Adder-cost: 90   maxlim: 6144   bits: 14/13
c ---[1493]---> Adder-cost: 74   maxlim: 5120   bits: 14/13
c ---[1491]---> Adder-cost: 76   maxlim: 5376   bits: 14/13
c ---[1489]---> Sorter-cost:  786     Base: 2 2 2 2 2 2 2 7
c ---[1487]---> Adder-cost: 196   maxlim: 13568   bits: 15/14
c ---[1485]---> Adder-cost: 200   maxlim: 13440   bits: 15/14
c ---[1483]---> Adder-cost: 198   maxlim: 16256   bits: 15/14
c ---[1481]---> Sorter-cost:  928     Base: 2 2 2 2 2 2 2 7
c ---[1479]---> Adder-cost: 74   maxlim: 16256   bits: 15/14
c ---[1477]---> Adder-cost: 134   maxlim: 8832   bits: 15/14
c ---[1475]---> Adder-cost: 78   maxlim: 7552   bits: 14/13
c ---[1473]---> Adder-cost: 146   maxlim: 10112   bits: 15/14
c ---[1471]---> Adder-cost: 82   maxlim: 5504   bits: 14/13
c ---[1469]---> Adder-cost: 68   maxlim: 4992   bits: 14/13
c ---[1467]---> Adder-cost: 114   maxlim: 7424   bits: 14/13
c ---[1465]---> Sorter-cost:  268     Base: 2 2 2 2 2 2 2 2
c ---[1463]---> Adder-cost: 116   maxlim: 7808   bits: 14/13
c ---[1461]---> Adder-cost: 194   maxlim: 12544   bits: 15/14
c ---[1459]---> Adder-cost: 200   maxlim: 14080   bits: 15/14
c ---[1457]---> Adder-cost: 178   maxlim: 14720   bits: 15/14
c ---[1455]---> Sorter-cost:  266     Base: 2 2 2 2 2 2 2 2
c ---[1453]---> Sorter-cost:  435     Base: 2 2 2 2 2 2 2 7
c ---[1451]---> Sorter-cost:  994     Base: 2 2 2 2 2 2 2 7
c ---[1449]---> Adder-cost: 86   maxlim: 5120   bits: 14/13
c ---[1447]---> Sorter-cost:  447     Base: 2 2 2 2 2 2 2 7
c ---[1445]---> Adder-cost: 82   maxlim: 4864   bits: 14/13
c ---[1443]---> Adder-cost: 40   maxlim: 4864   bits: 14/13
c ---[1441]---> Adder-cost: 84   maxlim: 5760   bits: 14/13
c ---[1439]---> Sorter-cost:  554     Base: 2 2 2 2 2 2 2 7
c ---[1437]---> Sorter-cost:  592     Base: 2 2 2 2 2 2 2 7
c ---[1435]---> Sorter-cost:  786     Base: 2 2 2 2 2 2 2 7
c ---[1433]---> Adder-cost: 92   maxlim: 5760   bits: 14/13
c ---[1431]---> Adder-cost: 94   maxlim: 5760   bits: 14/13
c ---[1429]---> Adder-cost: 42   maxlim: 5760   bits: 14/13
c ---[1427]---> Adder-cost: 106   maxlim: 6400   bits: 14/13
c ---[1425]---> Sorter-cost:  447     Base: 2 2 2 2 2 2 2 7
c ---[1423]---> Adder-cost: 84   maxlim: 5632   bits: 14/13
c ---[1421]---> Sorter-cost:  268     Base: 2 2 2 2 2 2 2 2
c ---[1419]---> Adder-cost: 276   maxlim: 20096   bits: 16/15
c ---[1417]---> Adder-cost: 222   maxlim: 15744   bits: 15/14
c ---[1415]---> Adder-cost: 76   maxlim: 4352   bits: 14/13
c ---[1413]---> Sorter-cost:  420     Base: 2 2 2 2 2 2 2 7
c ---[1411]---> Sorter-cost:  928     Base: 2 2 2 2 2 2 2 7
c ---[1409]---> Sorter-cost:  282     Base: 2 2 2 2 2 2 2 7
c ---[1407]---> Sorter-cost:  516     Base: 2 2 2 2 2 2 2 7
c ---[1405]---> Sorter-cost:  430     Base: 2 2 2 2 2 2 2 7
c ---[1403]---> Adder-cost: 110   maxlim: 7296   bits: 14/13
c ---[1401]---> Adder-cost: 106   maxlim: 6656   bits: 14/13
c ---[1399]---> Sorter-cost:  427     Base: 2 2 2 2 2 2 2 7
c ---[1397]---> Sorter-cost:  734     Base: 2 2 2 2 2 2 2 7
c ---[1395]---> Adder-cost: 104   maxlim: 6144   bits: 14/13
c ---[1393]---> Adder-cost: 138   maxlim: 8192   bits: 15/14
c ---[1391]---> Adder-cost: 76   maxlim: 8960   bits: 15/14
c ---[1389]---> Adder-cost: 138   maxlim: 8832   bits: 15/14
c ---[1387]---> Sorter-cost:  715     Base: 2 2 2 2 2 2 2 7
c ---[1385]---> Sorter-cost:  385     Base: 2 2 2 2 2 2 2 7
c ---[1383]---> Adder-cost: 140   maxlim: 9600   bits: 15/14
c ---[1381]---> Sorter-cost:  715     Base: 2 2 2 2 2 2 2 7
c ---[1379]---> Sorter-cost:  541     Base: 2 2 2 2 2 2 2 7
c ---[1377]---> Adder-cost: 100   maxlim: 6144   bits: 14/13
c ---[1375]---> Adder-cost: 102   maxlim: 6656   bits: 14/13
c ---[1373]---> Adder-cost: 94   maxlim: 5632   bits: 14/13
c ---[1371]---> Sorter-cost:  637     Base: 2 2 2 2 2 2 2 7
c ---[1369]---> Sorter-cost:  652     Base: 2 2 2 2 2 2 2 7
c ---[1367]---> Sorter-cost:  639     Base: 2 2 2 2 2 2 2 7
c ---[1365]---> Sorter-cost:  491     Base: 2 2 2 2 2 2 2 7
c ---[1363]---> Adder-cost: 42   maxlim: 5632   bits: 14/13
c ---[1361]---> Sorter-cost:  677     Base: 2 2 2 2 2 2 2 7
c ---[1359]---> Adder-cost: 146   maxlim: 8832   bits: 15/14
c ---[1357]---> Adder-cost: 112   maxlim: 7552   bits: 14/13
c ---[1355]---> Sorter-cost:  442     Base: 2 2 2 2 2 2 2 7
c ---[1353]---> Sorter-cost:  319     Base: 2 2 2 2 2 2 2 7
c ---[1351]---> Sorter-cost:  637     Base: 2 2 2 2 2 2 2 7
c ---[1349]---> Sorter-cost:  652     Base: 2 2 2 2 2 2 2 7
c ---[1347]---> Sorter-cost:  492     Base: 2 2 2 2 2 2 2 7
c ---[1345]---> Sorter-cost: 1003     Base: 2 2 2 2 2 2 2 7
c ---[1343]---> Adder-cost: 82   maxlim: 4864   bits: 14/13
c ---[1341]---> Sorter-cost:  604     Base: 2 2 2 2 2 2 2 7
c ---[1339]---> Sorter-cost:  932     Base: 2 2 2 2 2 2 2 7
c ---[1337]---> Sorter-cost:  412     Base: 2 2 2 2 2 2 2 7
c ---[1335]---> Sorter-cost:  683     Base: 2 2 2 2 2 2 2 7
c ---[1333]---> Sorter-cost:  517     Base: 2 2 2 2 2 2 2 7
c ---[1331]---> Sorter-cost:  952     Base: 2 2 2 2 2 2 2 7
c ---[1329]---> Sorter-cost:  700     Base: 2 2 2 2 2 2 2 7
c ---[1328]---> Adder-cost: 1054   maxlim: 71935   bits: 18/17
c ---[1327]---> Adder-cost: 2484   maxlim: 171263   bits: 19/18
c ---[1326]---> Adder-cost: 2298   maxlim: 160255   bits: 19/18
c ---[1325]---> Adder-cost: 31973   maxlim: 8145791   bits: 24/23
c ---[1323]---> Adder-cost: 76   maxlim: 4480   bits: 14/13
c ---[1321]---> Adder-cost: 60   maxlim: 4736   bits: 14/13
c ---[1319]---> Adder-cost: 76   maxlim: 5376   bits: 14/13
c ---[1317]---> Adder-cost: 102   maxlim: 6272   bits: 14/13
c ---[1315]---> Sorter-cost:  439     Base: 2 2 2 2 2 2 2 7
c ---[1313]---> Sorter-cost:  573     Base: 2 2 2 2 2 2 2 7
c ---[1311]---> Sorter-cost:  440     Base: 2 2 2 2 2 2 2 7
c ---[1309]---> Sorter-cost:  590     Base: 2 2 2 2 2 2 2 7
c ---[1307]---> Sorter-cost:  369     Base: 2 2 2 2 2 2 2 7
c ---[1305]---> Sorter-cost:  293     Base: 2 2 2 2 2 2 2 7
c ---[1303]---> Sorter-cost:  380     Base: 2 2 2 2 2 2 2 7
c ---[1301]---> Sorter-cost:  293     Base: 2 2 2 2 2 2 2 7
c ---[1299]---> Sorter-cost:  324     Base: 2 2 2 2 2 2 2 7
c ---[1297]---> Sorter-cost:  594     Base: 2 2 2 2 2 2 2 7
c ---[1295]---> Sorter-cost:  625     Base: 2 2 2 2 2 2 2 7
c ---[1293]---> Sorter-cost:  440     Base: 2 2 2 2 2 2 2 7
c ---[1291]---> Sorter-cost:  370     Base: 2 2 2 2 2 2 2 7
c ---[1289]---> Sorter-cost:  264     Base: 2 2 2 2 2 2 2 2
c ---[1287]---> Sorter-cost:  176     Base: 2 2 2 2 2 2 2 2
c ---[1285]---> Sorter-cost:  396     Base: 2 2 2 2 2 2 2 7
c ---[1283]---> Sorter-cost:  310     Base: 2 2 2 2 2 2 2 2
c ---[1281]---> Adder-cost: 170   maxlim: 10752   bits: 15/14
c ---[1279]---> Adder-cost: 162   maxlim: 12032   bits: 15/14
c ---[1277]---> Adder-cost: 84   maxlim: 6144   bits: 14/13
c ---[1275]---> Adder-cost: 146   maxlim: 8832   bits: 15/14
c ---[1273]---> Adder-cost: 142   maxlim: 10112   bits: 15/14
c ---[1271]---> Adder-cost: 80   maxlim: 6016   bits: 14/13
c ---[1269]---> Adder-cost: 76   maxlim: 6400   bits: 14/13
c ---[1267]---> Sorter-cost:  625     Base: 2 2 2 2 2 2 2 7
c ---[1265]---> Sorter-cost:  473     Base: 2 2 2 2 2 2 2 7
c ---[1263]---> Sorter-cost:  440     Base: 2 2 2 2 2 2 2 7
c ---[1261]---> Sorter-cost:  306     Base: 2 2 2 2 2 2 2 7
c ---[1259]---> Sorter-cost:  652     Base: 2 2 2 2 2 2 2 7
c ---[1257]---> Sorter-cost:  566     Base: 2 2 2 2 2 2 2 7
c ---[1255]---> Sorter-cost:  786     Base: 2 2 2 2 2 2 2 7
c ---[1253]---> Sorter-cost:  404     Base: 2 2 2 2 2 2 2 7
c ---[1251]---> Sorter-cost:  447     Base: 2 2 2 2 2 2 2 7
c ---[1249]---> Sorter-cost:  584     Base: 2 2 2 2 2 2 2 7
c ---[1247]---> Sorter-cost:  430     Base: 2 2 2 2 2 2 2 7
c ---[1245]---> Sorter-cost:  256     Base: 2 2 2 2 2 2 2 2
c ---[1243]---> Sorter-cost:  218     Base: 2 2 2 2 2 2 2 2
c ---[1241]---> Sorter-cost:  616     Base: 2 2 2 2 2 2 2 7
c ---[1239]---> Sorter-cost:  452     Base: 2 2 2 2 2 2 2 7
c ---[1237]---> Sorter-cost:  465     Base: 2 2 2 2 2 2 2 7
c ---[1235]---> Sorter-cost:  329     Base: 2 2 2 2 2 2 2 7
c ---[1233]---> Sorter-cost:  582     Base: 2 2 2 2 2 2 2 7
c ---[1231]---> Sorter-cost:  430     Base: 2 2 2 2 2 2 2 7
c ---[1229]---> Sorter-cost:  417     Base: 2 2 2 2 2 2 2 7
c ---[1227]---> Adder-cost: 88   maxlim: 5248   bits: 14/13
c ---[1225]---> Sorter-cost:  928     Base: 2 2 2 2 2 2 2 7
c ---[1223]---> Sorter-cost:  794     Base: 2 2 2 2 2 2 2 7
c ---[1221]---> Sorter-cost:  312     Base: 2 2 2 2 2 2 2 2
c ---[1219]---> Sorter-cost:  176     Base: 2 2 2 2 2 2 2 2
c ---[1217]---> Sorter-cost:  563     Base: 2 2 2 2 2 2 2 7
c ---[1215]---> Sorter-cost:  293     Base: 2 2 2 2 2 2 2 7
c ---[1213]---> Sorter-cost:  437     Base: 2 2 2 2 2 2 2 7
c ---[1211]---> Adder-cost: 88   maxlim: 6016   bits: 14/13
c ---[1209]---> Sorter-cost:  408     Base: 2 2 2 2 2 2 2 7
c ---[1207]---> Sorter-cost:  280     Base: 2 2 2 2 2 2 2 7
c ---[1205]---> Sorter-cost:  681     Base: 2 2 2 2 2 2 2 7
c ---[1203]---> Sorter-cost:  886     Base: 2 2 2 2 2 2 2 7
c ---[1201]---> Sorter-cost:  310     Base: 2 2 2 2 2 2 2 2
c ---[1199]---> Sorter-cost:  569     Base: 2 2 2 2 2 2 2 7
c ---[1197]---> Sorter-cost:  557     Base: 2 2 2 2 2 2 2 7
c ---[1195]---> Sorter-cost:  617     Base: 2 2 2 2 2 2 2 7
c ---[1193]---> Sorter-cost:  616     Base: 2 2 2 2 2 2 2 7
c ---[1191]---> Sorter-cost:  573     Base: 2 2 2 2 2 2 2 7
c ---[1189]---> Sorter-cost:  420     Base: 2 2 2 2 2 2 2 7
c ---[1187]---> Sorter-cost:  447     Base: 2 2 2 2 2 2 2 7
c ---[1185]---> Sorter-cost:  392     Base: 2 2 2 2 2 2 2 7
c ---[1183]---> Sorter-cost:  639     Base: 2 2 2 2 2 2 2 7
c ---[1181]---> Sorter-cost:  649     Base: 2 2 2 2 2 2 2 7
c ---[1179]---> Sorter-cost:  310     Base: 2 2 2 2 2 2 2 2
c ---[1177]---> Sorter-cost:  176     Base: 2 2 2 2 2 2 2 2
c ---[1175]---> Sorter-cost:  262     Base: 2 2 2 2 2 2 2 2
c ---[1173]---> Sorter-cost:  218     Base: 2 2 2 2 2 2 2 2
c ---[1171]---> Sorter-cost:  442     Base: 2 2 2 2 2 2 2 7
c ---[1169]---> Sorter-cost:  571     Base: 2 2 2 2 2 2 2 7
c ---[1167]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 7
c ---[1165]---> Sorter-cost:  311     Base: 2 2 2 2 2 2 2 7
c ---[1163]---> Sorter-cost:  302     Base: 2 2 2 2 2 2 2 2
c ---[1161]---> Sorter-cost:  176     Base: 2 2 2 2 2 2 2 2
c ---[1159]---> Sorter-cost:  314     Base: 2 2 2 2 2 2 2 2
c ---[1157]---> Sorter-cost:  176     Base: 2 2 2 2 2 2 2 2
c ---[1155]---> Sorter-cost:  386     Base: 2 2 2 2 2 2 2 7
c ---[1153]---> Sorter-cost:  280     Base: 2 2 2 2 2 2 2 7
c ---[1151]---> Adder-cost: 82   maxlim: 4992   bits: 14/13
c ---[1149]---> Sorter-cost:  438     Base: 2 2 2 2 2 2 2 7
c ---[1147]---> Sorter-cost:  407     Base: 2 2 2 2 2 2 2 7
c ---[1145]---> Sorter-cost:  424     Base: 2 2 2 2 2 2 2 7
c ---[1143]---> Adder-cost: 90   maxlim: 5504   bits: 14/13
c ---[1141]---> Adder-cost: 78   maxlim: 4864   bits: 14/13
c ---[1139]---> Adder-cost: 148   maxlim: 9600   bits: 15/14
c ---[1137]---> Adder-cost: 40   maxlim: 4992   bits: 14/13
c ---[1135]---> Adder-cost: 130   maxlim: 9088   bits: 15/14
c ---[1133]---> Sorter-cost:  264     Base: 2 2 2 2 2 2 2 2
c ---[1131]---> Sorter-cost:  218     Base: 2 2 2 2 2 2 2 2
c ---[1129]---> Adder-cost: 82   maxlim: 4992   bits: 14/13
c ---[1127]---> Adder-cost: 88   maxlim: 5248   bits: 14/13
c ---[1125]---> Adder-cost: 48   maxlim: 5248   bits: 14/13
c ---[1123]---> Sorter-cost:  897     Base: 2 2 2 2 2 2 2 7
c ---[1121]---> Sorter-cost:  928     Base: 2 2 2 2 2 2 2 7
c ---[1119]---> Sorter-cost:  996     Base: 2 2 2 2 2 2 2 7
c ---[1117]---> Sorter-cost:  736     Base: 2 2 2 2 2 2 2 7
c ---[1115]---> Sorter-cost:  404     Base: 2 2 2 2 2 2 2 7
c ---[1113]---> Sorter-cost:  404     Base: 2 2 2 2 2 2 2 7
c ---[1111]---> Sorter-cost:  954     Base: 2 2 2 2 2 2 2 7
c ---[1109]---> Sorter-cost:  604     Base: 2 2 2 2 2 2 2 7
c ---[1107]---> Sorter-cost:  928     Base: 2 2 2 2 2 2 2 7
c ---[1105]---> Sorter-cost:  575     Base: 2 2 2 2 2 2 2 7
c ---[1103]---> Sorter-cost:  366     Base: 2 2 2 2 2 2 2 7
c ---[1101]---> Sorter-cost:  994     Base: 2 2 2 2 2 2 2 7
c ---[1099]---> Sorter-cost:  944     Base: 2 2 2 2 2 2 2 7
c ---[1097]---> Adder-cost: 138   maxlim: 8960   bits: 15/14
c ---[1095]---> Adder-cost: 104   maxlim: 7296   bits: 14/13
c ---[1093]---> Adder-cost: 84   maxlim: 5120   bits: 14/13
c ---[1091]---> Sorter-cost:  730     Base: 2 2 2 2 2 2 2 7
c ---[1089]---> Sorter-cost:  314     Base: 2 2 2 2 2 2 2 2
c ---[1087]---> Sorter-cost:  715     Base: 2 2 2 2 2 2 2 7
c ---[1085]---> Sorter-cost:  944     Base: 2 2 2 2 2 2 2 7
c ---[1083]---> Adder-cost: 90   maxlim: 5376   bits: 14/13
c ---[1081]---> Adder-cost: 56   maxlim: 4992   bits: 14/13
c ---[1079]---> Adder-cost: 76   maxlim: 5504   bits: 14/13
c ---[1077]---> Adder-cost: 54   maxlim: 5376   bits: 14/13
c ---[1075]---> Adder-cost: 74   maxlim: 5632   bits: 14/13
c ---[1073]---> Sorter-cost:  562     Base: 2 2 2 2 2 2 2 7
c ---[1071]---> Adder-cost: 42   maxlim: 5632   bits: 14/13
c ---[1069]---> Adder-cost: 64   maxlim: 5760   bits: 14/13
c ---[1067]---> Adder-cost: 88   maxlim: 5248   bits: 14/13
c ---[1065]---> Adder-cost: 78   maxlim: 4864   bits: 14/13
c ---[1063]---> Adder-cost: 40   maxlim: 4864   bits: 14/13
c ---[1061]---> Adder-cost: 80   maxlim: 4992   bits: 14/13
c ---[1059]---> Sorter-cost:  934     Base: 2 2 2 2 2 2 2 7
c ---[1057]---> Sorter-cost:  703     Base: 2 2 2 2 2 2 2 7
c ---[1055]---> Sorter-cost:  588     Base: 2 2 2 2 2 2 2 7
c ---[1053]---> Sorter-cost:  432     Base: 2 2 2 2 2 2 2 7
c ---[1051]---> Sorter-cost:  594     Base: 2 2 2 2 2 2 2 7
c ---[1049]---> Adder-cost: 96   maxlim: 6016   bits: 14/13
c ---[1047]---> Sorter-cost:  907     Base: 2 2 2 2 2 2 2 7
c ---[1045]---> Adder-cost: 118   maxlim: 7552   bits: 14/13
c ---[1043]---> Adder-cost: 146   maxlim: 9728   bits: 15/14
c ---[1041]---> Sorter-cost:  889     Base: 2 2 2 2 2 2 2 7
c ---[1039]---> Sorter-cost:  306     Base: 2 2 2 2 2 2 2 7
c ---[1037]---> Adder-cost: 96   maxlim: 6016   bits: 14/13
c ---[1035]---> Adder-cost: 40   maxlim: 6016   bits: 14/13
c ---[1033]---> Adder-cost: 76   maxlim: 4864   bits: 14/13
c ---[1031]---> Adder-cost: 70   maxlim: 4992   bits: 14/13
c ---[1029]---> Sorter-cost: 1019     Base: 2 2 2 2 2 2 2 7
c ---[1027]---> Sorter-cost:  924     Base: 2 2 2 2 2 2 2 7
c ---[1025]---> Adder-cost: 118   maxlim: 7424   bits: 14/13
c ---[1023]---> Sorter-cost:  637     Base: 2 2 2 2 2 2 2 7
c ---[1021]---> Adder-cost: 138   maxlim: 8320   bits: 15/14
c ---[1019]---> Adder-cost: 108   maxlim: 7552   bits: 14/13
c ---[1017]---> Sorter-cost:  786     Base: 2 2 2 2 2 2 2 7
c ---[1015]---> Adder-cost: 90   maxlim: 5376   bits: 14/13
c ---[1013]---> Adder-cost: 90   maxlim: 5632   bits: 14/13
c ---[1011]---> Adder-cost: 76   maxlim: 4992   bits: 14/13
c ---[1009]---> Sorter-cost:  657     Base: 2 2 2 2 2 2 2 7
c ---[1007]---> Sorter-cost: 1076     Base: 2 2 2 2 2 2 2 7
c ---[1005]---> Sorter-cost:  778     Base: 2 2 2 2 2 2 2 7
c ---[1003]---> Sorter-cost:  404     Base: 2 2 2 2 2 2 2 7
c ---[1001]---> Adder-cost: 146   maxlim: 9344   bits: 15/14
c ---[ 999]---> Adder-cost: 60   maxlim: 9344   bits: 15/14
c ---[ 997]---> Adder-cost: 84   maxlim: 5120   bits: 14/13
c ---[ 995]---> Adder-cost: 44   maxlim: 5120   bits: 14/13
c ---[ 993]---> Sorter-cost:  683     Base: 2 2 2 2 2 2 2 7
c ---[ 991]---> Sorter-cost:  627     Base: 2 2 2 2 2 2 2 7
c ---[ 989]---> Sorter-cost:  473     Base: 2 2 2 2 2 2 2 7
c ---[ 987]---> Adder-cost: 70   maxlim: 4480   bits: 14/13
c ---[ 985]---> Adder-cost: 74   maxlim: 4992   bits: 14/13
c ---[ 983]---> Adder-cost: 82   maxlim: 5504   bits: 14/13
c ---[ 981]---> Adder-cost: 40   maxlim: 5504   bits: 14/13
c ---[ 979]---> Adder-cost: 92   maxlim: 5632   bits: 14/13
c ---[ 977]---> Sorter-cost:  744     Base: 2 2 2 2 2 2 2 7
c ---[ 975]---> Sorter-cost:  449     Base: 2 2 2 2 2 2 2 7
c ---[ 973]---> Sorter-cost:  443     Base: 2 2 2 2 2 2 2 7
c ---[ 971]---> Sorter-cost:  409     Base: 2 2 2 2 2 2 2 7
c ---[ 969]---> Sorter-cost:  356     Base: 2 2 2 2 2 2 2 7
c ---[ 967]---> Sorter-cost:  407     Base: 2 2 2 2 2 2 2 7
c ---[ 965]---> Adder-cost: 124   maxlim: 7680   bits: 14/13
c ---[ 963]---> Adder-cost: 94   maxlim: 8192   bits: 15/14
c ---[ 961]---> Sorter-cost:  991     Base: 2 2 2 2 2 2 2 7
c ---[ 959]---> Adder-cost: 76   maxlim: 5376   bits: 14/13
c ---[ 957]---> Sorter-cost: 1172     Base: 2 2 2 2 2 2 2 7
c ---[ 955]---> Sorter-cost: 1053     Base: 2 2 2 2 2 2 2 7
c ---[ 953]---> Sorter-cost: 1118     Base: 2 2 2 2 2 2 2 7
c ---[ 951]---> Adder-cost: 78   maxlim: 4992   bits: 14/13
c ---[ 949]---> Adder-cost: 78   maxlim: 4992   bits: 14/13
c ---[ 947]---> Sorter-cost: 1028     Base: 2 2 2 2 2 2 2 7
c ---[ 945]---> Sorter-cost:  980     Base: 2 2 2 2 2 2 2 7
c ---[ 943]---> Sorter-cost: 1060     Base: 2 2 2 2 2 2 2 7
c ---[ 941]---> Sorter-cost:  908     Base: 2 2 2 2 2 2 2 7
c ---[ 939]---> Sorter-cost:  554     Base: 2 2 2 2 2 2 2 7
c ---[ 937]---> Sorter-cost:  689     Base: 2 2 2 2 2 2 2 7
c ---[ 935]---> Sorter-cost:  570     Base: 2 2 2 2 2 2 2 7
c ---[ 933]---> Adder-cost: 86   maxlim: 5248   bits: 14/13
c ---[ 931]---> Adder-cost: 76   maxlim: 4480   bits: 14/13
c ---[ 929]---> Sorter-cost:  996     Base: 2 2 2 2 2 2 2 7
c ---[ 927]---> Adder-cost: 82   maxlim: 4864   bits: 14/13
c ---[ 925]---> Adder-cost: 74   maxlim: 6016   bits: 14/13
c ---[ 923]---> Adder-cost: 102   maxlim: 6656   bits: 14/13
c ---[ 921]---> Adder-cost: 48   maxlim: 6656   bits: 14/13
c ---[ 919]---> Adder-cost: 88   maxlim: 5120   bits: 14/13
c ---[ 917]---> Adder-cost: 104   maxlim: 6656   bits: 14/13
c ---[ 915]---> Adder-cost: 68   maxlim: 6272   bits: 14/13
c ---[ 913]---> Adder-cost: 178   maxlim: 11264   bits: 15/14
c ---[ 911]---> Adder-cost: 192   maxlim: 12928   bits: 15/14
c ---[ 909]---> Sorter-cost:  639     Base: 2 2 2 2 2 2 2 7
c ---[ 907]---> Sorter-cost:  473     Base: 2 2 2 2 2 2 2 7
c ---[ 905]---> Sorter-cost:  635     Base: 2 2 2 2 2 2 2 7
c ---[ 903]---> Adder-cost: 96   maxlim: 5888   bits: 14/13
c ---[ 901]---> Adder-cost: 76   maxlim: 6528   bits: 14/13
c ---[ 899]---> Adder-cost: 94   maxlim: 6016   bits: 14/13
c ---[ 897]---> Adder-cost: 64   maxlim: 5760   bits: 14/13
c ---[ 895]---> Sorter-cost:  310     Base: 2 2 2 2 2 2 2 2
c ---[ 893]---> Sorter-cost:  246     Base: 2 2 2 2 2 2 2 2
c ---[ 891]---> Sorter-cost:  314     Base: 2 2 2 2 2 2 2 2
c ---[ 889]---> Sorter-cost:  176     Base: 2 2 2 2 2 2 2 2
c ---[ 887]---> Sorter-cost:  629     Base: 2 2 2 2 2 2 2 7
c ---[ 885]---> Sorter-cost:  421     Base: 2 2 2 2 2 2 2 7
c ---[ 883]---> Sorter-cost:  293     Base: 2 2 2 2 2 2 2 7
c ---[ 881]---> Adder-cost: 112   maxlim: 6912   bits: 14/13
c ---[ 879]---> Adder-cost: 80   maxlim: 5760   bits: 14/13
c ---[ 877]---> Adder-cost: 90   maxlim: 5888   bits: 14/13
c ---[ 875]---> Adder-cost: 40   maxlim: 5888   bits: 14/13
c ---[ 873]---> Sorter-cost:  467     Base: 2 2 2 2 2 2 2 7
c ---[ 871]---> Sorter-cost:  695     Base: 2 2 2 2 2 2 2 7
c ---[ 869]---> Sorter-cost:  420     Base: 2 2 2 2 2 2 2 7
c ---[ 867]---> Adder-cost: 132   maxlim: 8576   bits: 15/14
c ---[ 865]---> Adder-cost: 96   maxlim: 7040   bits: 14/13
c ---[ 863]---> Adder-cost: 136   maxlim: 8320   bits: 15/14
c ---[ 861]---> Adder-cost: 98   maxlim: 6144   bits: 14/13
c ---[ 859]---> Sorter-cost:  718     Base: 2 2 2 2 2 2 2 7
c ---[ 857]---> Adder-cost: 46   maxlim: 6144   bits: 14/13
c ---[ 855]---> Adder-cost: 200   maxlim: 13184   bits: 15/14
c ---[ 853]---> Adder-cost: 184   maxlim: 12160   bits: 15/14
c ---[ 851]---> Adder-cost: 152   maxlim: 10752   bits: 15/14
c ---[ 849]---> Adder-cost: 130   maxlim: 10624   bits: 15/14
c ---[ 847]---> Adder-cost: 108   maxlim: 6784   bits: 14/13
c ---[ 845]---> Adder-cost: 90   maxlim: 6400   bits: 14/13
c ---[ 843]---> Adder-cost: 90   maxlim: 5504   bits: 14/13
c ---[ 841]---> Sorter-cost:  404     Base: 2 2 2 2 2 2 2 7
c ---[ 839]---> Sorter-cost:  358     Base: 2 2 2 2 2 2 2 7
c ---[ 837]---> Sorter-cost:  691     Base: 2 2 2 2 2 2 2 7
c ---[ 835]---> Sorter-cost:  419     Base: 2 2 2 2 2 2 2 7
c ---[ 833]---> Adder-cost: 110   maxlim: 8064   bits: 14/13
c ---[ 831]---> Sorter-cost: 1072     Base: 2 2 2 2 2 2 2 7
c ---[ 829]---> Sorter-cost:  984     Base: 2 2 2 2 2 2 2 7
c ---[ 827]---> Sorter-cost:  683     Base: 2 2 2 2 2 2 2 7
c ---[ 825]---> Sorter-cost:  680     Base: 2 2 2 2 2 2 2 7
c ---[ 823]---> Sorter-cost:  675     Base: 2 2 2 2 2 2 2 7
c ---[ 821]---> Sorter-cost:  517     Base: 2 2 2 2 2 2 2 7
c ---[ 819]---> Sorter-cost:  635     Base: 2 2 2 2 2 2 2 7
c ---[ 817]---> Sorter-cost:  507     Base: 2 2 2 2 2 2 2 7
c ---[ 815]---> Sorter-cost: 1047     Base: 2 2 2 2 2 2 2 7
c ---[ 813]---> Sorter-cost:  661     Base: 2 2 2 2 2 2 2 7
c ---[ 811]---> Sorter-cost: 1015     Base: 2 2 2 2 2 2 2 7
c ---[ 809]---> Sorter-cost:  633     Base: 2 2 2 2 2 2 2 7
c ---[ 807]---> Sorter-cost:  604     Base: 2 2 2 2 2 2 2 7
c ---[ 805]---> Adder-cost: 82   maxlim: 4864   bits: 14/13
c ---[ 803]---> Adder-cost: 40   maxlim: 4864   bits: 14/13
c ---[ 801]---> Sorter-cost:  573     Base: 2 2 2 2 2 2 2 7
c ---[ 799]---> Sorter-cost:  701     Base: 2 2 2 2 2 2 2 7
c ---[ 797]---> Sorter-cost:  394     Base: 2 2 2 2 2 2 2 7
c ---[ 795]---> Sorter-cost:  406     Base: 2 2 2 2 2 2 2 7
c ---[ 793]---> Sorter-cost:  358     Base: 2 2 2 2 2 2 2 7
c ---[ 791]---> Sorter-cost:  611     Base: 2 2 2 2 2 2 2 7
c ---[ 789]---> Sorter-cost:  294     Base: 2 2 2 2 2 2 2 2
c ---[ 787]---> Sorter-cost:  574     Base: 2 2 2 2 2 2 2 7
c ---[ 785]---> Sorter-cost:  675     Base: 2 2 2 2 2 2 2 7
c ---[ 783]---> Adder-cost: 68   maxlim: 5760   bits: 14/13
c ---[ 781]---> Adder-cost: 70   maxlim: 6016   bits: 14/13
c ---[ 779]---> Adder-cost: 94   maxlim: 6528   bits: 14/13
c ---[ 777]---> Sorter-cost:  423     Base: 2 2 2 2 2 2 2 7
c ---[ 775]---> Sorter-cost:  632     Base: 2 2 2 2 2 2 2 7
c ---[ 773]---> Sorter-cost:  928     Base: 2 2 2 2 2 2 2 7
c ---[ 771]---> Sorter-cost:  634     Base: 2 2 2 2 2 2 2 7
c ---[ 769]---> Sorter-cost:  949     Base: 2 2 2 2 2 2 2 7
c ---[ 767]---> Sorter-cost:  433     Base: 2 2 2 2 2 2 2 7
c ---[ 765]---> Sorter-cost:  403     Base: 2 2 2 2 2 2 2 7
c ---[ 763]---> Sorter-cost:  352     Base: 2 2 2 2 2 2 2 7
c ---[ 761]---> Sorter-cost:  311     Base: 2 2 2 2 2 2 2 7
c ---[ 759]---> Sorter-cost:  440     Base: 2 2 2 2 2 2 2 7
c ---[ 757]---> Sorter-cost:  433     Base: 2 2 2 2 2 2 2 7
c ---[ 755]---> Sorter-cost:  250     Base: 2 2 2 2 2 2 2 2
c ---[ 753]---> Sorter-cost:  928     Base: 2 2 2 2 2 2 2 7
c ---[ 751]---> Sorter-cost:  895     Base: 2 2 2 2 2 2 2 7
c ---[ 749]---> Sorter-cost:  632     Base: 2 2 2 2 2 2 2 7
c ---[ 747]---> Sorter-cost:  577     Base: 2 2 2 2 2 2 2 7
c ---[ 745]---> Sorter-cost:  576     Base: 2 2 2 2 2 2 2 7
c ---[ 743]---> Sorter-cost:  288     Base: 2 2 2 2 2 2 2 2
c ---[ 741]---> Sorter-cost:  621     Base: 2 2 2 2 2 2 2 7
c ---[ 739]---> Sorter-cost:  968     Base: 2 2 2 2 2 2 2 7
c ---[ 737]---> Sorter-cost: 1038     Base: 2 2 2 2 2 2 2 7
c ---[ 735]---> Adder-cost: 88   maxlim: 5376   bits: 14/13
c ---[ 733]---> Adder-cost: 58   maxlim: 5504   bits: 14/13
c ---[ 731]---> Sorter-cost:  978     Base: 2 2 2 2 2 2 2 7
c ---[ 729]---> Sorter-cost:  573     Base: 2 2 2 2 2 2 2 7
c ---[ 727]---> Sorter-cost:  590     Base: 2 2 2 2 2 2 2 7
c ---[ 725]---> Sorter-cost:  176     Base: 2 2 2 2 2 2 2 2
c ---[ 723]---> Sorter-cost:  639     Base: 2 2 2 2 2 2 2 7
c ---[ 721]---> Sorter-cost:  592     Base: 2 2 2 2 2 2 2 7
c ---[ 719]---> Sorter-cost:  449     Base: 2 2 2 2 2 2 2 7
c ---[ 717]---> Sorter-cost:  592     Base: 2 2 2 2 2 2 2 7
c ---[ 715]---> Sorter-cost:  290     Base: 2 2 2 2 2 2 2 2
c ---[ 713]---> Sorter-cost:  176     Base: 2 2 2 2 2 2 2 2
c ---[ 711]---> Sorter-cost:  360     Base: 2 2 2 2 2 2 2 7
c ---[ 709]---> Sorter-cost:  402     Base: 2 2 2 2 2 2 2 7
c ---[ 707]---> Adder-cost: 76   maxlim: 5504   bits: 14/13
c ---[ 705]---> Adder-cost: 62   maxlim: 5120   bits: 14/13
c ---[ 703]---> Sorter-cost: 1078     Base: 2 2 2 2 2 2 2 7
c ---[ 701]---> Sorter-cost:  996     Base: 2 2 2 2 2 2 2 7
c ---[ 699]---> Sorter-cost: 1049     Base: 2 2 2 2 2 2 2 7
c ---[ 697]---> Sorter-cost: 1039     Base: 2 2 2 2 2 2 2 7
c ---[ 695]---> Sorter-cost:  932     Base: 2 2 2 2 2 2 2 7
c ---[ 693]---> Sorter-cost:  839     Base: 2 2 2 2 2 2 2 7
c ---[ 691]---> Sorter-cost:  651     Base: 2 2 2 2 2 2 2 7
c ---[ 689]---> Sorter-cost:  920     Base: 2 2 2 2 2 2 2 7
c ---[ 687]---> Sorter-cost:  626     Base: 2 2 2 2 2 2 2 7
c ---[ 685]---> Sorter-cost:  529     Base: 2 2 2 2 2 2 2 7
c ---[ 683]---> Sorter-cost:  621     Base: 2 2 2 2 2 2 2 7
c ---[ 681]---> Sorter-cost:  639     Base: 2 2 2 2 2 2 2 7
c ---[ 679]---> Sorter-cost:  507     Base: 2 2 2 2 2 2 2 7
c ---[ 677]---> Sorter-cost:  507     Base: 2 2 2 2 2 2 2 7
c ---[ 675]---> Sorter-cost: 1041     Base: 2 2 2 2 2 2 2 7
c ---[ 673]---> Sorter-cost:  619     Base: 2 2 2 2 2 2 2 7
c ---[ 671]---> Adder-cost: 104   maxlim: 7168   bits: 14/13
c ---[ 669]---> Sorter-cost:  370     Base: 2 2 2 2 2 2 2 7
c ---[ 667]---> Adder-cost: 74   maxlim: 7040   bits: 14/13
c ---[ 665]---> Adder-cost: 88   maxlim: 6016   bits: 14/13
c ---[ 663]---> Adder-cost: 94   maxlim: 6656   bits: 14/13
c ---[ 661]---> Adder-cost: 76   maxlim: 4736   bits: 14/13
c ---[ 659]---> Adder-cost: 38   maxlim: 4736   bits: 14/13
c ---[ 657]---> Adder-cost: 114   maxlim: 7168   bits: 14/13
c ---[ 655]---> Adder-cost: 82   maxlim: 4992   bits: 14/13
c ---[ 653]---> Sorter-cost:  246     Base: 2 2 2 2 2 2 2 7
c ---[ 651]---> Adder-cost: 120   maxlim: 8448   bits: 15/14
c ---[ 649]---> Adder-cost: 178   maxlim: 11392   bits: 15/14
c ---[ 647]---> Adder-cost: 96   maxlim: 7040   bits: 14/13
c ---[ 645]---> Adder-cost: 180   maxlim: 11904   bits: 15/14
c ---[ 643]---> Adder-cost: 92   maxlim: 11904   bits: 15/14
c ---[ 641]---> Sorter-cost:  575     Base: 2 2 2 2 2 2 2 7
c ---[ 639]---> Sorter-cost:  437     Base: 2 2 2 2 2 2 2 7
c ---[ 637]---> Sorter-cost:  443     Base: 2 2 2 2 2 2 2 7
c ---[ 635]---> Sorter-cost:  311     Base: 2 2 2 2 2 2 2 7
c ---[ 633]---> Sorter-cost:  246     Base: 2 2 2 2 2 2 2 7
c ---[ 631]---> Sorter-cost:  713     Base: 2 2 2 2 2 2 2 7
c ---[ 629]---> Sorter-cost:  396     Base: 2 2 2 2 2 2 2 7
c ---[ 627]---> Adder-cost: 82   maxlim: 5248   bits: 14/13
c ---[ 625]---> Adder-cost: 106   maxlim: 6912   bits: 14/13
c ---[ 623]---> Sorter-cost:  901     Base: 2 2 2 2 2 2 2 7
c ---[ 621]---> Sorter-cost:  404     Base: 2 2 2 2 2 2 2 7
c ---[ 619]---> Adder-cost: 206   maxlim: 15104   bits: 15/14
c ---[ 617]---> Adder-cost: 232   maxlim: 17024   bits: 16/15
c ---[ 615]---> Adder-cost: 214   maxlim: 16768   bits: 16/15
c ---[ 613]---> Adder-cost: 104   maxlim: 6144   bits: 14/13
c ---[ 611]---> Adder-cost: 64   maxlim: 5760   bits: 14/13
c ---[ 609]---> Adder-cost: 100   maxlim: 6912   bits: 14/13
c ---[ 607]---> Adder-cost: 72   maxlim: 6912   bits: 14/13
c ---[ 605]---> Sorter-cost:  567     Base: 2 2 2 2 2 2 2 7
c ---[ 603]---> Sorter-cost:  405     Base: 2 2 2 2 2 2 2 7
c ---[ 601]---> Sorter-cost:  293     Base: 2 2 2 2 2 2 2 7
c ---[ 599]---> Adder-cost: 116   maxlim: 7168   bits: 14/13
c ---[ 597]---> Adder-cost: 134   maxlim: 8192   bits: 15/14
c ---[ 595]---> Adder-cost: 142   maxlim: 10112   bits: 15/14
c ---[ 593]---> Adder-cost: 152   maxlim: 10496   bits: 15/14
c ---[ 591]---> Adder-cost: 84   maxlim: 5504   bits: 14/13
c ---[ 589]---> Sorter-cost:  392     Base: 2 2 2 2 2 2 2 7
c ---[ 587]---> Adder-cost: 88   maxlim: 5120   bits: 14/13
c ---[ 585]---> Sorter-cost:  996     Base: 2 2 2 2 2 2 2 7
c ---[ 583]---> Sorter-cost:  604     Base: 2 2 2 2 2 2 2 7
c ---[ 581]---> Adder-cost: 84   maxlim: 6144   bits: 14/13
c ---[ 579]---> Adder-cost: 80   maxlim: 6912   bits: 14/13
c ---[ 577]---> Sorter-cost:  308     Base: 2 2 2 2 2 2 2 2
c ---[ 575]---> Adder-cost: 146   maxlim: 9728   bits: 15/14
c ---[ 573]---> Adder-cost: 64   maxlim: 9728   bits: 15/14
c ---[ 571]---> Adder-cost: 214   maxlim: 14976   bits: 15/14
c ---[ 569]---> Adder-cost: 184   maxlim: 15104   bits: 15/14
c ---[ 567]---> Adder-cost: 178   maxlim: 14592   bits: 15/14
c ---[ 565]---> Adder-cost: 78   maxlim: 14592   bits: 15/14
c ---[ 563]---> Adder-cost: 82   maxlim: 5760   bits: 14/13
c ---[ 561]---> Sorter-cost:  362     Base: 2 2 2 2 2 2 2 7
c ---[ 559]---> Adder-cost: 66   maxlim: 5504   bits: 14/13
c ---[ 557]---> Adder-cost: 68   maxlim: 6016   bits: 14/13
c ---[ 555]---> Adder-cost: 104   maxlim: 6400   bits: 14/13
c ---[ 553]---> Adder-cost: 44   maxlim: 6400   bits: 14/13
c ---[ 551]---> Adder-cost: 88   maxlim: 6016   bits: 14/13
c ---[ 549]---> Sorter-cost:  590     Base: 2 2 2 2 2 2 2 7
c ---[ 547]---> Sorter-cost:  956     Base: 2 2 2 2 2 2 2 7
c ---[ 545]---> Sorter-cost:  820     Base: 2 2 2 2 2 2 2 7
c ---[ 543]---> Sorter-cost:  678     Base: 2 2 2 2 2 2 2 7
c ---[ 541]---> Adder-cost: 104   maxlim: 6400   bits: 14/13
c ---[ 539]---> Adder-cost: 44   maxlim: 6400   bits: 14/13
c ---[ 537]---> Adder-cost: 104   maxlim: 6912   bits: 14/13
c ---[ 535]---> Adder-cost: 70   maxlim: 6528   bits: 14/13
c ---[ 533]---> Sorter-cost:  563     Base: 2 2 2 2 2 2 2 7
c ---[ 531]---> Sorter-cost:  423     Base: 2 2 2 2 2 2 2 7
c ---[ 529]---> Sorter-cost:  594     Base: 2 2 2 2 2 2 2 7
c ---[ 527]---> Sorter-cost:  615     Base: 2 2 2 2 2 2 2 7
c ---[ 525]---> Sorter-cost:  555     Base: 2 2 2 2 2 2 2 7
c ---[ 523]---> Sorter-cost:  605     Base: 2 2 2 2 2 2 2 7
c ---[ 521]---> Sorter-cost:  423     Base: 2 2 2 2 2 2 2 7
c ---[ 519]---> Sorter-cost:  515     Base: 2 2 2 2 2 2 2 7
c ---[ 517]---> Sorter-cost:  530     Base: 2 2 2 2 2 2 2 7
c ---[ 515]---> Sorter-cost:  427     Base: 2 2 2 2 2 2 2 7
c ---[ 513]---> Sorter-cost:  319     Base: 2 2 2 2 2 2 2 7
c ---[ 511]---> Sorter-cost:  311     Base: 2 2 2 2 2 2 2 7
c ---[ 509]---> Sorter-cost:  576     Base: 2 2 2 2 2 2 2 7
c ---[ 507]---> Adder-cost: 76   maxlim: 4352   bits: 14/13
c ---[ 505]---> Sorter-cost:  430     Base: 2 2 2 2 2 2 2 7
c ---[ 503]---> Sorter-cost:  418     Base: 2 2 2 2 2 2 2 7
c ---[ 501]---> Sorter-cost:  399     Base: 2 2 2 2 2 2 2 7
c ---[ 499]---> Sorter-cost:  459     Base: 2 2 2 2 2 2 2 7
c ---[ 497]---> Sorter-cost:  555     Base: 2 2 2 2 2 2 2 7
c ---[ 495]---> Sorter-cost:  675     Base: 2 2 2 2 2 2 2 7
c ---[ 493]---> Sorter-cost:  691     Base: 2 2 2 2 2 2 2 7
c ---[ 491]---> Sorter-cost: 1080     Base: 2 2 2 2 2 2 2 7
c ---[ 489]---> Sorter-cost: 1020     Base: 2 2 2 2 2 2 2 7
c ---[ 487]---> Sorter-cost:  667     Base: 2 2 2 2 2 2 2 7
c ---[ 485]---> Adder-cost: 40   maxlim: 4352   bits: 14/13
c ---[ 483]---> Adder-cost: 98   maxlim: 7296   bits: 14/13
c ---[ 481]---> Adder-cost: 76   maxlim: 7680   bits: 14/13
c ---[ 479]---> Adder-cost: 100   maxlim: 7808   bits: 14/13
c ---[ 477]---> Adder-cost: 114   maxlim: 9088   bits: 15/14
c ---[ 475]---> Adder-cost: 98   maxlim: 6272   bits: 14/13
c ---[ 473]---> Adder-cost: 70   maxlim: 6272   bits: 14/13
c ---[ 471]---> Adder-cost: 74   maxlim: 4480   bits: 14/13
c ---[ 469]---> Sorter-cost:  557     Base: 2 2 2 2 2 2 2 7
c ---[ 467]---> Sorter-cost:  437     Base: 2 2 2 2 2 2 2 7
c ---[ 465]---> Adder-cost: 100   maxlim: 6784   bits: 14/13
c ---[ 463]---> Adder-cost: 88   maxlim: 5376   bits: 14/13
c ---[ 461]---> Adder-cost: 50   maxlim: 5504   bits: 14/13
c ---[ 459]---> Adder-cost: 78   maxlim: 5632   bits: 14/13
c ---[ 457]---> Adder-cost: 40   maxlim: 4480   bits: 14/13
c ---[ 455]---> Sorter-cost:  663     Base: 2 2 2 2 2 2 2 7
c ---[ 453]---> Sorter-cost:  644     Base: 2 2 2 2 2 2 2 7
c ---[ 451]---> Adder-cost: 94   maxlim: 6272   bits: 14/13
c ---[ 449]---> Sorter-cost: 1066     Base: 2 2 2 2 2 2 2 7
c ---[ 447]---> Sorter-cost:  869     Base: 2 2 2 2 2 2 2 7
c ---[ 445]---> Sorter-cost: 1057     Base: 2 2 2 2 2 2 2 7
c ---[ 443]---> Sorter-cost:  964     Base: 2 2 2 2 2 2 2 7
c ---[ 441]---> Adder-cost: 84   maxlim: 5504   bits: 14/13
c ---[ 439]---> Adder-cost: 72   maxlim: 5504   bits: 14/13
c ---[ 437]---> Adder-cost: 40   maxlim: 5504   bits: 14/13
c ---[ 435]---> Adder-cost: 90   maxlim: 6016   bits: 14/13
c ---[ 433]---> Sorter-cost:  467     Base: 2 2 2 2 2 2 2 7
c ---[ 431]---> Sorter-cost:  573     Base: 2 2 2 2 2 2 2 7
c ---[ 429]---> Sorter-cost:  456     Base: 2 2 2 2 2 2 2 7
c ---[ 427]---> Adder-cost: 102   maxlim: 6272   bits: 14/13
c ---[ 425]---> Adder-cost: 80   maxlim: 6144   bits: 14/13
c ---[ 423]---> Adder-cost: 132   maxlim: 8576   bits: 15/14
c ---[ 421]---> Adder-cost: 84   maxlim: 7680   bits: 14/13
c ---[ 419]---> Sorter-cost:  438     Base: 2 2 2 2 2 2 2 7
c ---[ 417]---> Sorter-cost:  715     Base: 2 2 2 2 2 2 2 7
c ---[ 415]---> Sorter-cost:  571     Base: 2 2 2 2 2 2 2 7
c ---[ 413]---> Sorter-cost:  400     Base: 2 2 2 2 2 2 2 7
c ---[ 411]---> Adder-cost: 88   maxlim: 6016   bits: 14/13
c ---[ 409]---> Adder-cost: 80   maxlim: 4864   bits: 14/13
c ---[ 407]---> Adder-cost: 80   maxlim: 5760   bits: 14/13
c ---[ 405]---> Adder-cost: 112   maxlim: 8064   bits: 14/13
c ---[ 403]---> Adder-cost: 50   maxlim: 8064   bits: 14/13
c ---[ 401]---> Adder-cost: 72   maxlim: 5120   bits: 14/13
c ---[ 399]---> Adder-cost: 98   maxlim: 7552   bits: 14/13
c ---[ 397]---> Adder-cost: 48   maxlim: 7552   bits: 14/13
c ---[ 395]---> Sorter-cost:  616     Base: 2 2 2 2 2 2 2 7
c ---[ 393]---> Sorter-cost:  452     Base: 2 2 2 2 2 2 2 7
c ---[ 391]---> Sorter-cost:  441     Base: 2 2 2 2 2 2 2 7
c ---[ 389]---> Sorter-cost:  252     Base: 2 2 2 2 2 2 2 2
c ---[ 387]---> Sorter-cost:  218     Base: 2 2 2 2 2 2 2 2
c ---[ 385]---> Sorter-cost:  218     Base: 2 2 2 2 2 2 2 2
c ---[ 383]---> Sorter-cost:  302     Base: 2 2 2 2 2 2 2 2
c ---[ 381]---> Sorter-cost:  400     Base: 2 2 2 2 2 2 2 7
c ---[ 379]---> Sorter-cost:  620     Base: 2 2 2 2 2 2 2 7
c ---[ 377]---> Sorter-cost:  605     Base: 2 2 2 2 2 2 2 7
c ---[ 375]---> Sorter-cost:  632     Base: 2 2 2 2 2 2 2 7
c ---[ 373]---> Sorter-cost:  696     Base: 2 2 2 2 2 2 2 7
c ---[ 371]---> Sorter-cost:  764     Base: 2 2 2 2 2 2 2 7
c ---[ 369]---> Sorter-cost: 1115     Base: 2 2 2 2 2 2 2 7
c ---[ 367]---> Sorter-cost:  756     Base: 2 2 2 2 2 2 2 7
c ---[ 365]---> Sorter-cost:  681     Base: 2 2 2 2 2 2 2 7
c ---[ 363]---> Sorter-cost:  667     Base: 2 2 2 2 2 2 2 7
c ---[ 361]---> Sorter-cost:  628     Base: 2 2 2 2 2 2 2 7
c ---[ 359]---> Adder-cost: 130   maxlim: 8192   bits: 15/14
c ---[ 357]---> Sorter-cost:  266     Base: 2 2 2 2 2 2 2 2
c ---[ 355]---> Sorter-cost:  218     Base: 2 2 2 2 2 2 2 2
c ---[ 353]---> Sorter-cost:  310     Base: 2 2 2 2 2 2 2 2
c ---[ 351]---> Sorter-cost:  176     Base: 2 2 2 2 2 2 2 2
c ---[ 349]---> Adder-cost: 146   maxlim: 10112   bits: 15/14
c ---[ 347]---> Sorter-cost:  614     Base: 2 2 2 2 2 2 2 7
c ---[ 345]---> Sorter-cost:  627     Base: 2 2 2 2 2 2 2 7
c ---[ 343]---> Adder-cost: 104   maxlim: 6784   bits: 14/13
c ---[ 341]---> Adder-cost: 186   maxlim: 12672   bits: 15/14
c ---[ 339]---> Adder-cost: 72   maxlim: 12672   bits: 15/14
c ---[ 337]---> Sorter-cost:  266     Base: 2 2 2 2 2 2 2 2
c ---[ 335]---> Sorter-cost:  262     Base: 2 2 2 2 2 2 2 2
c ---[ 333]---> Sorter-cost:  703     Base: 2 2 2 2 2 2 2 7
c ---[ 331]---> Adder-cost: 158   maxlim: 10624   bits: 15/14
c ---[ 329]---> Sorter-cost:  176     Base: 2 2 2 2 2 2 2 2
c ---[ 327]---> Sorter-cost:  176     Base: 2 2 2 2 2 2 2 2
c ---[ 325]---> Adder-cost: 128   maxlim: 9856   bits: 15/14
c ---[ 323]---> Adder-cost: 150   maxlim: 11008   bits: 15/14
c ---[ 321]---> Adder-cost: 94   maxlim: 5632   bits: 14/13
c ---[ 319]---> Adder-cost: 74   maxlim: 4480   bits: 14/13
c ---[ 317]---> Adder-cost: 80   maxlim: 6912   bits: 14/13
c ---[ 315]---> Sorter-cost:  426     Base: 2 2 2 2 2 2 2 7
c ---[ 313]---> Sorter-cost:  554     Base: 2 2 2 2 2 2 2 7
c ---[ 311]---> Sorter-cost:  371     Base: 2 2 2 2 2 2 2 7
c ---[ 309]---> Sorter-cost:  293     Base: 2 2 2 2 2 2 2 7
c ---[ 307]---> Sorter-cost:  293     Base: 2 2 2 2 2 2 2 7
c ---[ 305]---> Adder-cost: 130   maxlim: 9600   bits: 15/14
c ---[ 303]---> Sorter-cost:  314     Base: 2 2 2 2 2 2 2 7
c ---[ 301]---> Sorter-cost:  521     Base: 2 2 2 2 2 2 2 7
c ---[ 299]---> Sorter-cost:  616     Base: 2 2 2 2 2 2 2 7
c ---[ 297]---> Sorter-cost:  360     Base: 2 2 2 2 2 2 2 7
c ---[ 295]---> Sorter-cost:  436     Base: 2 2 2 2 2 2 2 7
c ---[ 293]---> Sorter-cost:  306     Base: 2 2 2 2 2 2 2 7
c ---[ 291]---> Adder-cost: 62   maxlim: 9600   bits: 15/14
c ---[ 289]---> Sorter-cost:  629     Base: 2 2 2 2 2 2 2 7
c ---[ 287]---> Sorter-cost:  473     Base: 2 2 2 2 2 2 2 7
c ---[ 285]---> Sorter-cost:  306     Base: 2 2 2 2 2 2 2 2
c ---[ 283]---> Sorter-cost:  176     Base: 2 2 2 2 2 2 2 2
c ---[ 281]---> Sorter-cost:  408     Base: 2 2 2 2 2 2 2 7
c ---[ 279]---> Sorter-cost:  280     Base: 2 2 2 2 2 2 2 7
c ---[ 277]---> Sorter-cost:  280     Base: 2 2 2 2 2 2 2 7
c ---[ 275]---> Sorter-cost:  280     Base: 2 2 2 2 2 2 2 7
c ---[ 273]---> Sorter-cost:  421     Base: 2 2 2 2 2 2 2 7
c ---[ 271]---> Sorter-cost:  293     Base: 2 2 2 2 2 2 2 7
c ---[ 269]---> Sorter-cost:  330     Base: 2 2 2 2 2 2 2 7
c ---[ 267]---> Sorter-cost:  246     Base: 2 2 2 2 2 2 2 7
c ---[ 265]---> Adder-cost: 140   maxlim: 9216   bits: 15/14
c ---[ 263]---> Adder-cost: 138   maxlim: 10496   bits: 15/14
c ---[ 261]---> Adder-cost: 80   maxlim: 5888   bits: 14/13
c ---[ 259]---> Adder-cost: 54   maxlim: 5760   bits: 14/13
c ---[ 257]---> Adder-cost: 44   maxlim: 5376   bits: 14/13
c ---[ 255]---> Sorter-cost:  268     Base: 2 2 2 2 2 2 2 2
c ---[ 253]---> Sorter-cost:  218     Base: 2 2 2 2 2 2 2 2
c ---[ 251]---> Sorter-cost:  362     Base: 2 2 2 2 2 2 2 7
c ---[ 249]---> Sorter-cost:  427     Base: 2 2 2 2 2 2 2 7
c ---[ 247]---> Sorter-cost:  413     Base: 2 2 2 2 2 2 2 7
c ---[ 245]---> Sorter-cost:  432     Base: 2 2 2 2 2 2 2 7
c ---[ 243]---> Sorter-cost:  526     Base: 2 2 2 2 2 2 2 7
c ---[ 241]---> Sorter-cost:  308     Base: 2 2 2 2 2 2 2 2
c ---[ 239]---> Adder-cost: 110   maxlim: 7040   bits: 14/13
c ---[ 237]---> Sorter-cost:  392     Base: 2 2 2 2 2 2 2 7
c ---[ 235]---> Sorter-cost:  888     Base: 2 2 2 2 2 2 2 7
c ---[ 233]---> Sorter-cost:  550     Base: 2 2 2 2 2 2 2 7
c ---[ 231]---> Sorter-cost:  398     Base: 2 2 2 2 2 2 2 7
c ---[ 229]---> Sorter-cost:  322     Base: 2 2 2 2 2 2 2 7
c ---[ 227]---> Sorter-cost:  398     Base: 2 2 2 2 2 2 2 7
c ---[ 225]---> Sorter-cost:  417     Base: 2 2 2 2 2 2 2 7
c ---[ 223]---> Sorter-cost:  280     Base: 2 2 2 2 2 2 2 7
c ---[ 221]---> Sorter-cost:  629     Base: 2 2 2 2 2 2 2 7
c ---[ 219]---> Sorter-cost:  473     Base: 2 2 2 2 2 2 2 7
c ---[ 217]---> Adder-cost: 94   maxlim: 6528   bits: 14/13
c ---[ 215]---> Sorter-cost:  934     Base: 2 2 2 2 2 2 2 7
c ---[ 213]---> Sorter-cost:  984     Base: 2 2 2 2 2 2 2 7
c ---[ 211]---> Sorter-cost:  293     Base: 2 2 2 2 2 2 2 7
c ---[ 209]---> Sorter-cost:  254     Base: 2 2 2 2 2 2 2 2
c ---[ 207]---> Sorter-cost:  980     Base: 2 2 2 2 2 2 2 7
c ---[ 205]---> Adder-cost: 106   maxlim: 7040   bits: 14/13
c ---[ 203]---> Sorter-cost:  689     Base: 2 2 2 2 2 2 2 7
c ---[ 201]---> Sorter-cost:  517     Base: 2 2 2 2 2 2 2 7
c ---[ 199]---> Adder-cost: 92   maxlim: 5888   bits: 14/13
c ---[ 197]---> Adder-cost: 180   maxlim: 12928   bits: 15/14
c ---[ 195]---> Sorter-cost:  296     Base: 2 2 2 2 2 2 2 2
c ---[ 193]---> Adder-cost: 84   maxlim: 5248   bits: 14/13
c ---[ 191]---> Adder-cost: 200   maxlim: 17792   bits: 16/15
c ---[ 189]---> Adder-cost: 92   maxlim: 17792   bits: 16/15
c ---[ 187]---> Adder-cost: 92   maxlim: 17792   bits: 16/15
c ---[ 185]---> Adder-cost: 92   maxlim: 17792   bits: 16/15
c ---[ 183]---> Adder-cost: 156   maxlim: 18048   bits: 16/15
c ---[ 181]---> Adder-cost: 166   maxlim: 15616   bits: 15/14
c ---[ 179]---> Adder-cost: 78   maxlim: 15616   bits: 15/14
c ---[ 177]---> Sorter-cost:  541     Base: 2 2 2 2 2 2 2 7
c ---[ 175]---> Sorter-cost:  430     Base: 2 2 2 2 2 2 2 7
c ---[ 173]---> Adder-cost: 194   maxlim: 18176   bits: 16/15
c ---[ 171]---> Adder-cost: 88   maxlim: 18176   bits: 16/15
c ---[ 169]---> Adder-cost: 154   maxlim: 12672   bits: 15/14
c ---[ 167]---> Adder-cost: 72   maxlim: 12672   bits: 15/14
c ---[ 165]---> Adder-cost: 150   maxlim: 13056   bits: 15/14
c ---[ 163]---> Adder-cost: 74   maxlim: 13056   bits: 15/14
c ---[ 161]---> Adder-cost: 130   maxlim: 12928   bits: 15/14
c ---[ 159]---> Adder-cost: 76   maxlim: 12928   bits: 15/14
c ---[ 157]---> Sorter-cost:  441     Base: 2 2 2 2 2 2 2 7
c ---[ 155]---> Sorter-cost: 1117     Base: 2 2 2 2 2 2 2 7
c ---[ 153]---> Sorter-cost: 1007     Base: 2 2 2 2 2 2 2 7
c ---[ 151]---> Sorter-cost:  759     Base: 2 2 2 2 2 2 2 7
c ---[ 149]---> Sorter-cost:  753     Base: 2 2 2 2 2 2 2 7
c ---[ 147]---> Sorter-cost:  525     Base: 2 2 2 2 2 2 2 7
c ---[ 145]---> Sorter-cost: 1138     Base: 2 2 2 2 2 2 2 7
c ---[ 143]---> Sorter-cost: 1011     Base: 2 2 2 2 2 2 2 7
c ---[ 141]---> Sorter-cost:  956     Base: 2 2 2 2 2 2 2 7
c ---[ 139]---> Sorter-cost:  904     Base: 2 2 2 2 2 2 2 7
c ---[ 137]---> Sorter-cost:  989     Base: 2 2 2 2 2 2 2 7
c ---[ 135]---> Sorter-cost:  664     Base: 2 2 2 2 2 2 2 7
c ---[ 133]---> Sorter-cost:  962     Base: 2 2 2 2 2 2 2 7
c ---[ 131]---> Sorter-cost:  944     Base: 2 2 2 2 2 2 2 7
c ---[ 129]---> Sorter-cost:  606     Base: 2 2 2 2 2 2 2 7
c ---[ 127]---> Adder-cost: 86   maxlim: 5504   bits: 14/13
c ---[ 125]---> Sorter-cost:  398     Base: 2 2 2 2 2 2 2 7
c ---[ 123]---> Sorter-cost:  440     Base: 2 2 2 2 2 2 2 7
c ---[ 121]---> Sorter-cost:  441     Base: 2 2 2 2 2 2 2 7
c ---[ 119]---> Sorter-cost:  980     Base: 2 2 2 2 2 2 2 7
c ---[ 117]---> Adder-cost: 94   maxlim: 5632   bits: 14/13
c ---[ 115]---> Adder-cost: 80   maxlim: 5248   bits: 14/13
c ---[ 113]---> Adder-cost: 128   maxlim: 8448   bits: 15/14
c ---[ 111]---> Adder-cost: 104   maxlim: 7808   bits: 14/13
c ---[ 109]---> Sorter-cost:  635     Base: 2 2 2 2 2 2 2 7
c ---[ 107]---> Adder-cost: 152   maxlim: 9600   bits: 15/14
c ---[ 105]---> Adder-cost: 86   maxlim: 6016   bits: 14/13
c ---[ 103]---> Sorter-cost:  442     Base: 2 2 2 2 2 2 2 7
c ---[ 101]---> Adder-cost: 68   maxlim: 5888   bits: 14/13
c ---[  99]---> Sorter-cost:  417     Base: 2 2 2 2 2 2 2 7
c ---[  97]---> Sorter-cost:  400     Base: 2 2 2 2 2 2 2 7
c ---[  95]---> Sorter-cost:  944     Base: 2 2 2 2 2 2 2 7
c ---[  93]---> Sorter-cost:  314     Base: 2 2 2 2 2 2 2 2
c ---[  91]---> Sorter-cost:  423     Base: 2 2 2 2 2 2 2 7
c ---[  89]---> Sorter-cost:  663     Base: 2 2 2 2 2 2 2 7
c ---[  87]---> Sorter-cost:  593     Base: 2 2 2 2 2 2 2 7
c ---[  85]---> Sorter-cost:  473     Base: 2 2 2 2 2 2 2 7
c ---[  83]---> Sorter-cost:  772     Base: 2 2 2 2 2 2 2 7
c ---[  81]---> Sorter-cost:  404     Base: 2 2 2 2 2 2 2 7
c ---[  79]---> Sorter-cost:  657     Base: 2 2 2 2 2 2 2 7
c ---[  77]---> Sorter-cost:  585     Base: 2 2 2 2 2 2 2 7
c ---[  75]---> Sorter-cost: 1013     Base: 2 2 2 2 2 2 2 7
c ---[  73]---> Sorter-cost:  656     Base: 2 2 2 2 2 2 2 7
c ---[  71]---> Sorter-cost:  665     Base: 2 2 2 2 2 2 2 7
c ---[  69]---> Sorter-cost:  970     Base: 2 2 2 2 2 2 2 7
c ---[  67]---> Adder-cost: 94   maxlim: 6272   bits: 14/13
c ---[  65]---> Adder-cost: 78   maxlim: 4864   bits: 14/13
c ---[  63]---> Adder-cost: 94   maxlim: 6912   bits: 14/13
c ---[  61]---> Adder-cost: 142   maxlim: 11264   bits: 15/14
c ---[  59]---> Adder-cost: 140   maxlim: 10240   bits: 15/14
c ---[  57]---> Sorter-cost:  600     Base: 2 2 2 2 2 2 2 7
c ---[  55]---> Sorter-cost:  411     Base: 2 2 2 2 2 2 2 7
c ---[  53]---> Sorter-cost:  367     Base: 2 2 2 2 2 2 2 7
c ---[  51]---> Sorter-cost:  300     Base: 2 2 2 2 2 2 2 2
c ---[  49]---> Sorter-cost:  396     Base: 2 2 2 2 2 2 2 7
c ---[  47]---> Adder-cost: 80   maxlim: 4992   bits: 14/13
c ---[  45]---> Adder-cost: 88   maxlim: 5248   bits: 14/13
c ---[  43]---> Sorter-cost:  681     Base: 2 2 2 2 2 2 2 7
c ---[  41]---> Sorter-cost:  901     Base: 2 2 2 2 2 2 2 7
c ---[  39]---> Sorter-cost:  958     Base: 2 2 2 2 2 2 2 7
c ---[  37]---> Adder-cost: 80   maxlim: 5888   bits: 14/13
c ---[  35]---> Adder-cost: 72   maxlim: 5760   bits: 14/13
c ---[  33]---> Adder-cost: 78   maxlim: 4864   bits: 14/13
c ---[  31]---> Sorter-cost:  984     Base: 2 2 2 2 2 2 2 7
c ---[  29]---> Sorter-cost:  452     Base: 2 2 2 2 2 2 2 7
c ---[  27]---> Adder-cost: 90   maxlim: 5888   bits: 14/13
c ---[  25]---> Adder-cost: 86   maxlim: 6272   bits: 14/13
c ---[  23]---> Adder-cost: 96   maxlim: 6272   bits: 14/13
c ---[  21]---> Adder-cost: 88   maxlim: 6656   bits: 14/13
c ---[  19]---> Sorter-cost:  604     Base: 2 2 2 2 2 2 2 7
c ---[  17]---> Adder-cost: 106   maxlim: 6656   bits: 14/13
c ---[  15]---> Adder-cost: 72   maxlim: 4352   bits: 14/13
c ---[  13]---> Adder-cost: 88   maxlim: 5888   bits: 14/13
c ---[  11]---> Adder-cost: 90   maxlim: 6784   bits: 14/13
c ---[   9]---> Adder-cost: 96   maxlim: 7424   bits: 14/13
c ---[   7]---> Sorter-cost:  565     Base: 2 2 2 2 2 2 2 7
c ---[   5]---> Sorter-cost:  621     Base: 2 2 2 2 2 2 2 7
c ---[   3]---> /oldhome/oroussel/solvers/minisat+_script: line 16: 15677 CPU time limit exceeded $XDIR/minisat+_bignum_static* "$@"
#### END SOLVER DATA ####
#### BEGIN WATCHER DATA ####
Enforcing CPU limit (will send SIGTERM then SIGKILL): 1200 seconds
Enforcing CPUTime (will send SIGXCPU) limit: 1230 seconds
Enforcing VSIZE limit: 943718400 bytes
Raw data (loadavg): 0.91 0.95 0.90 2/54 15672
Raw data (stat): 15672 (runsolver) R 15671 24300 24299 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 784873522 1052672 99 4294967295 134512640 135381576 3221224480 3221219688 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.0006 s]
Raw data (loadavg): 0.93 0.95 0.90 2/55 15677
Raw data (stat): 15672 (minisat+_script) S 15671 24300 24299 0 -1 0 300 1322 0 0 0 0 17 4 17 0 1 0 784873522 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+20.0006 s]
Raw data (loadavg): 0.94 0.96 0.91 2/55 15677
Raw data (stat): 15672 (minisat+_script) S 15671 24300 24299 0 -1 0 300 1322 0 0 0 0 17 4 17 0 1 0 784873522 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+30.0012 s]
Raw data (loadavg): 0.95 0.96 0.91 2/55 15677
Raw data (stat): 15672 (minisat+_script) S 15671 24300 24299 0 -1 0 300 1322 0 0 0 0 17 4 17 0 1 0 784873522 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+40.0009 s]
Raw data (loadavg): 0.95 0.96 0.91 2/55 15677
Raw data (stat): 15672 (minisat+_script) S 15671 24300 24299 0 -1 0 300 1322 0 0 0 0 17 4 17 0 1 0 784873522 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+50.0009 s]
Raw data (loadavg): 0.96 0.96 0.91 2/55 15677
Raw data (stat): 15672 (minisat+_script) S 15671 24300 24299 0 -1 0 300 1322 0 0 0 0 17 4 17 0 1 0 784873522 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+60.0015 s]
Raw data (loadavg): 0.97 0.96 0.91 2/55 15677
Raw data (stat): 15672 (minisat+_script) S 15671 24300 24299 0 -1 0 300 1322 0 0 0 0 17 4 17 0 1 0 784873522 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+70.0008 s]
Raw data (loadavg): 0.97 0.96 0.91 2/55 15677
Raw data (stat): 15672 (minisat+_script) S 15671 24300 24299 0 -1 0 300 1322 0 0 0 0 17 4 17 0 1 0 784873522 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+80.0015 s]
Raw data (loadavg): 0.98 0.96 0.91 2/55 15677
Raw data (stat): 15672 (minisat+_script) S 15671 24300 24299 0 -1 0 300 1322 0 0 0 0 17 4 17 0 1 0 784873522 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+90.0014 s]
Raw data (loadavg): 0.98 0.96 0.91 2/55 15677
Raw data (stat): 15672 (minisat+_script) S 15671 24300 24299 0 -1 0 300 1322 0 0 0 0 17 4 17 0 1 0 784873522 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+100.001 s]
Raw data (loadavg): 0.98 0.96 0.91 2/55 15677
Raw data (stat): 15672 (minisat+_script) S 15671 24300 24299 0 -1 0 300 1322 0 0 0 0 17 4 17 0 1 0 784873522 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+110.002 s]
Raw data (loadavg): 0.98 0.96 0.91 2/55 15677
Raw data (stat): 15672 (minisat+_script) S 15671 24300 24299 0 -1 0 300 1322 0 0 0 0 17 4 17 0 1 0 784873522 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+120.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 15677
Raw data (stat): 15672 (minisat+_script) S 15671 24300 24299 0 -1 0 300 1322 0 0 0 0 17 4 17 0 1 0 784873522 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+130.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 15677
Raw data (stat): 15672 (minisat+_script) S 15671 24300 24299 0 -1 0 300 1322 0 0 0 0 17 4 17 0 1 0 784873522 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+140.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 15677
Raw data (stat): 15672 (minisat+_script) S 15671 24300 24299 0 -1 0 300 1322 0 0 0 0 17 4 17 0 1 0 784873522 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+150.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 15677
Raw data (stat): 15672 (minisat+_script) S 15671 24300 24299 0 -1 0 300 1322 0 0 0 0 17 4 17 0 1 0 784873522 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+160.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 15677
Raw data (stat): 15672 (minisat+_script) S 15671 24300 24299 0 -1 0 300 1322 0 0 0 0 17 4 17 0 1 0 784873522 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+170.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 15677
Raw data (stat): 15672 (minisat+_script) S 15671 24300 24299 0 -1 0 300 1322 0 0 0 0 17 4 17 0 1 0 784873522 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+180.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 15677
Raw data (stat): 15672 (minisat+_script) S 15671 24300 24299 0 -1 0 300 1322 0 0 0 0 17 4 17 0 1 0 784873522 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+190.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 15677
Raw data (stat): 15672 (minisat+_script) S 15671 24300 24299 0 -1 0 300 1322 0 0 0 0 17 4 17 0 1 0 784873522 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+200.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 15677
Raw data (stat): 15672 (minisat+_script) S 15671 24300 24299 0 -1 0 300 1322 0 0 0 0 17 4 17 0 1 0 784873522 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+210.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 15677
Raw data (stat): 15672 (minisat+_script) S 15671 24300 24299 0 -1 0 300 1322 0 0 0 0 17 4 17 0 1 0 784873522 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+220.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 15677
Raw data (stat): 15672 (minisat+_script) S 15671 24300 24299 0 -1 0 300 1322 0 0 0 0 17 4 17 0 1 0 784873522 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+230.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 15677
Raw data (stat): 15672 (minisat+_script) S 15671 24300 24299 0 -1 0 300 1322 0 0 0 0 17 4 17 0 1 0 784873522 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+240.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 15677
Raw data (stat): 15672 (minisat+_script) S 15671 24300 24299 0 -1 0 300 1322 0 0 0 0 17 4 17 0 1 0 784873522 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+250.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 15677
Raw data (stat): 15672 (minisat+_script) S 15671 24300 24299 0 -1 0 300 1322 0 0 0 0 17 4 17 0 1 0 784873522 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+260.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 15677
Raw data (stat): 15672 (minisat+_script) S 15671 24300 24299 0 -1 0 300 1322 0 0 0 0 17 4 17 0 1 0 784873522 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+270.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 15677
Raw data (stat): 15672 (minisat+_script) S 15671 24300 24299 0 -1 0 300 1322 0 0 0 0 17 4 17 0 1 0 784873522 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+280.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 15677
Raw data (stat): 15672 (minisat+_script) S 15671 24300 24299 0 -1 0 300 1322 0 0 0 0 17 4 17 0 1 0 784873522 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+290.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 15677
Raw data (stat): 15672 (minisat+_script) S 15671 24300 24299 0 -1 0 300 1322 0 0 0 0 17 4 17 0 1 0 784873522 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+300.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 15677
Raw data (stat): 15672 (minisat+_script) S 15671 24300 24299 0 -1 0 300 1322 0 0 0 0 17 4 17 0 1 0 784873522 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+310.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 15677
Raw data (stat): 15672 (minisat+_script) S 15671 24300 24299 0 -1 0 300 1322 0 0 0 0 17 4 17 0 1 0 784873522 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+320.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 15677
Raw data (stat): 15672 (minisat+_script) S 15671 24300 24299 0 -1 0 300 1322 0 0 0 0 17 4 17 0 1 0 784873522 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+330.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 15677
Raw data (stat): 15672 (minisat+_script) S 15671 24300 24299 0 -1 0 300 1322 0 0 0 0 17 4 17 0 1 0 784873522 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+340.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 15677
Raw data (stat): 15672 (minisat+_script) S 15671 24300 24299 0 -1 0 300 1322 0 0 0 0 17 4 17 0 1 0 784873522 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+350.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 15677
Raw data (stat): 15672 (minisat+_script) S 15671 24300 24299 0 -1 0 300 1322 0 0 0 0 17 4 17 0 1 0 784873522 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+360.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 15677
Raw data (stat): 15672 (minisat+_script) S 15671 24300 24299 0 -1 0 300 1322 0 0 0 0 17 4 17 0 1 0 784873522 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+370.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 15677
Raw data (stat): 15672 (minisat+_script) S 15671 24300 24299 0 -1 0 300 1322 0 0 0 0 17 4 17 0 1 0 784873522 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+380.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 15677
Raw data (stat): 15672 (minisat+_script) S 15671 24300 24299 0 -1 0 300 1322 0 0 0 0 17 4 17 0 1 0 784873522 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+390.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 15677
Raw data (stat): 15672 (minisat+_script) S 15671 24300 24299 0 -1 0 300 1322 0 0 0 0 17 4 17 0 1 0 784873522 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+400.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 15677
Raw data (stat): 15672 (minisat+_script) S 15671 24300 24299 0 -1 0 300 1322 0 0 0 0 17 4 17 0 1 0 784873522 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+410.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 15677
Raw data (stat): 15672 (minisat+_script) S 15671 24300 24299 0 -1 0 300 1322 0 0 0 0 17 4 17 0 1 0 784873522 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+420.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 15677
Raw data (stat): 15672 (minisat+_script) S 15671 24300 24299 0 -1 0 300 1322 0 0 0 0 17 4 17 0 1 0 784873522 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+430.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 15677
Raw data (stat): 15672 (minisat+_script) S 15671 24300 24299 0 -1 0 300 1322 0 0 0 0 17 4 17 0 1 0 784873522 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+440.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 15677
Raw data (stat): 15672 (minisat+_script) S 15671 24300 24299 0 -1 0 300 1322 0 0 0 0 17 4 17 0 1 0 784873522 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+450.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 15677
Raw data (stat): 15672 (minisat+_script) S 15671 24300 24299 0 -1 0 300 1322 0 0 0 0 17 4 17 0 1 0 784873522 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+460.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 15677
Raw data (stat): 15672 (minisat+_script) S 15671 24300 24299 0 -1 0 300 1322 0 0 0 0 17 4 17 0 1 0 784873522 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+470.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 15677
Raw data (stat): 15672 (minisat+_script) S 15671 24300 24299 0 -1 0 300 1322 0 0 0 0 17 4 17 0 1 0 784873522 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+480.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 15677
Raw data (stat): 15672 (minisat+_script) S 15671 24300 24299 0 -1 0 300 1322 0 0 0 0 17 4 17 0 1 0 784873522 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+490.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 15677
Raw data (stat): 15672 (minisat+_script) S 15671 24300 24299 0 -1 0 300 1322 0 0 0 0 17 4 17 0 1 0 784873522 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+500.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 15677
Raw data (stat): 15672 (minisat+_script) S 15671 24300 24299 0 -1 0 300 1322 0 0 0 0 17 4 17 0 1 0 784873522 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+510.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 15677
Raw data (stat): 15672 (minisat+_script) S 15671 24300 24299 0 -1 0 300 1322 0 0 0 0 17 4 17 0 1 0 784873522 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+520.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 15677
Raw data (stat): 15672 (minisat+_script) S 15671 24300 24299 0 -1 0 300 1322 0 0 0 0 17 4 17 0 1 0 784873522 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+530.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 15677
Raw data (stat): 15672 (minisat+_script) S 15671 24300 24299 0 -1 0 300 1322 0 0 0 0 17 4 17 0 1 0 784873522 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+540.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 15677
Raw data (stat): 15672 (minisat+_script) S 15671 24300 24299 0 -1 0 300 1322 0 0 0 0 17 4 17 0 1 0 784873522 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+550.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 15677
Raw data (stat): 15672 (minisat+_script) S 15671 24300 24299 0 -1 0 300 1322 0 0 0 0 17 4 17 0 1 0 784873522 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+560.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 15677
Raw data (stat): 15672 (minisat+_script) S 15671 24300 24299 0 -1 0 300 1322 0 0 0 0 17 4 17 0 1 0 784873522 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+570.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 15677
Raw data (stat): 15672 (minisat+_script) S 15671 24300 24299 0 -1 0 300 1322 0 0 0 0 17 4 17 0 1 0 784873522 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+580.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 15677
Raw data (stat): 15672 (minisat+_script) S 15671 24300 24299 0 -1 0 300 1322 0 0 0 0 17 4 17 0 1 0 784873522 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+590.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 15677
Raw data (stat): 15672 (minisat+_script) S 15671 24300 24299 0 -1 0 300 1322 0 0 0 0 17 4 17 0 1 0 784873522 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+600.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 15677
Raw data (stat): 15672 (minisat+_script) S 15671 24300 24299 0 -1 0 300 1322 0 0 0 0 17 4 17 0 1 0 784873522 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+610.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 15677
Raw data (stat): 15672 (minisat+_script) S 15671 24300 24299 0 -1 0 300 1322 0 0 0 0 17 4 17 0 1 0 784873522 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+620.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 15677
Raw data (stat): 15672 (minisat+_script) S 15671 24300 24299 0 -1 0 300 1322 0 0 0 0 17 4 17 0 1 0 784873522 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+630.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 15677
Raw data (stat): 15672 (minisat+_script) S 15671 24300 24299 0 -1 0 300 1322 0 0 0 0 17 4 17 0 1 0 784873522 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+640.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 15677
Raw data (stat): 15672 (minisat+_script) S 15671 24300 24299 0 -1 0 300 1322 0 0 0 0 17 4 17 0 1 0 784873522 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+650.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 15677
Raw data (stat): 15672 (minisat+_script) S 15671 24300 24299 0 -1 0 300 1322 0 0 0 0 17 4 17 0 1 0 784873522 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+660.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 15677
Raw data (stat): 15672 (minisat+_script) S 15671 24300 24299 0 -1 0 300 1322 0 0 0 0 17 4 17 0 1 0 784873522 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+670.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 15677
Raw data (stat): 15672 (minisat+_script) S 15671 24300 24299 0 -1 0 300 1322 0 0 0 0 17 4 17 0 1 0 784873522 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+680.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 15677
Raw data (stat): 15672 (minisat+_script) S 15671 24300 24299 0 -1 0 300 1322 0 0 0 0 17 4 17 0 1 0 784873522 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+690.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 15677
Raw data (stat): 15672 (minisat+_script) S 15671 24300 24299 0 -1 0 300 1322 0 0 0 0 17 4 17 0 1 0 784873522 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+700.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 15677
Raw data (stat): 15672 (minisat+_script) S 15671 24300 24299 0 -1 0 300 1322 0 0 0 0 17 4 17 0 1 0 784873522 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+710.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 15677
Raw data (stat): 15672 (minisat+_script) S 15671 24300 24299 0 -1 0 300 1322 0 0 0 0 17 4 17 0 1 0 784873522 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+720.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 15677
Raw data (stat): 15672 (minisat+_script) S 15671 24300 24299 0 -1 0 300 1322 0 0 0 0 17 4 17 0 1 0 784873522 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+730.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 15677
Raw data (stat): 15672 (minisat+_script) S 15671 24300 24299 0 -1 0 300 1322 0 0 0 0 17 4 17 0 1 0 784873522 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+740.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 15677
Raw data (stat): 15672 (minisat+_script) S 15671 24300 24299 0 -1 0 300 1322 0 0 0 0 17 4 17 0 1 0 784873522 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+750.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 15677
Raw data (stat): 15672 (minisat+_script) S 15671 24300 24299 0 -1 0 300 1322 0 0 0 0 17 4 17 0 1 0 784873522 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+760.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 15677
Raw data (stat): 15672 (minisat+_script) S 15671 24300 24299 0 -1 0 300 1322 0 0 0 0 17 4 17 0 1 0 784873522 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+770.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 15677
Raw data (stat): 15672 (minisat+_script) S 15671 24300 24299 0 -1 0 300 1322 0 0 0 0 17 4 17 0 1 0 784873522 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+780.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 15677
Raw data (stat): 15672 (minisat+_script) S 15671 24300 24299 0 -1 0 300 1322 0 0 0 0 17 4 17 0 1 0 784873522 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+790.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 15677
Raw data (stat): 15672 (minisat+_script) S 15671 24300 24299 0 -1 0 300 1322 0 0 0 0 17 4 17 0 1 0 784873522 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+800.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 15677
Raw data (stat): 15672 (minisat+_script) S 15671 24300 24299 0 -1 0 300 1322 0 0 0 0 17 4 17 0 1 0 784873522 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+810.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 15677
Raw data (stat): 15672 (minisat+_script) S 15671 24300 24299 0 -1 0 300 1322 0 0 0 0 17 4 17 0 1 0 784873522 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+820.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 15677
Raw data (stat): 15672 (minisat+_script) S 15671 24300 24299 0 -1 0 300 1322 0 0 0 0 17 4 17 0 1 0 784873522 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+830.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 15677
Raw data (stat): 15672 (minisat+_script) S 15671 24300 24299 0 -1 0 300 1322 0 0 0 0 17 4 17 0 1 0 784873522 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+840.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 15677
Raw data (stat): 15672 (minisat+_script) S 15671 24300 24299 0 -1 0 300 1322 0 0 0 0 17 4 17 0 1 0 784873522 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+850.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 15677
Raw data (stat): 15672 (minisat+_script) S 15671 24300 24299 0 -1 0 300 1322 0 0 0 0 17 4 17 0 1 0 784873522 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+860.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 15677
Raw data (stat): 15672 (minisat+_script) S 15671 24300 24299 0 -1 0 300 1322 0 0 0 0 17 4 17 0 1 0 784873522 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+870.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 15677
Raw data (stat): 15672 (minisat+_script) S 15671 24300 24299 0 -1 0 300 1322 0 0 0 0 17 4 17 0 1 0 784873522 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+880.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 15677
Raw data (stat): 15672 (minisat+_script) S 15671 24300 24299 0 -1 0 300 1322 0 0 0 0 17 4 17 0 1 0 784873522 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+890.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 15677
Raw data (stat): 15672 (minisat+_script) S 15671 24300 24299 0 -1 0 300 1322 0 0 0 0 17 4 17 0 1 0 784873522 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+900.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 15677
Raw data (stat): 15672 (minisat+_script) S 15671 24300 24299 0 -1 0 300 1322 0 0 0 0 17 4 17 0 1 0 784873522 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+910.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 15677
Raw data (stat): 15672 (minisat+_script) S 15671 24300 24299 0 -1 0 300 1322 0 0 0 0 17 4 17 0 1 0 784873522 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+920.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 15677
Raw data (stat): 15672 (minisat+_script) S 15671 24300 24299 0 -1 0 300 1322 0 0 0 0 17 4 17 0 1 0 784873522 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+930.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 15677
Raw data (stat): 15672 (minisat+_script) S 15671 24300 24299 0 -1 0 300 1322 0 0 0 0 17 4 17 0 1 0 784873522 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+940.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 15677
Raw data (stat): 15672 (minisat+_script) S 15671 24300 24299 0 -1 0 300 1322 0 0 0 0 17 4 17 0 1 0 784873522 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+950.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 15677
Raw data (stat): 15672 (minisat+_script) S 15671 24300 24299 0 -1 0 300 1322 0 0 0 0 17 4 17 0 1 0 784873522 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+960.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 15677
Raw data (stat): 15672 (minisat+_script) S 15671 24300 24299 0 -1 0 300 1322 0 0 0 0 17 4 17 0 1 0 784873522 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+970.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 15677
Raw data (stat): 15672 (minisat+_script) S 15671 24300 24299 0 -1 0 300 1322 0 0 0 0 17 4 17 0 1 0 784873522 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+980.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 15677
Raw data (stat): 15672 (minisat+_script) S 15671 24300 24299 0 -1 0 300 1322 0 0 0 0 17 4 17 0 1 0 784873522 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+990.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 15677
Raw data (stat): 15672 (minisat+_script) S 15671 24300 24299 0 -1 0 300 1322 0 0 0 0 17 4 17 0 1 0 784873522 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+1000 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 15677
Raw data (stat): 15672 (minisat+_script) S 15671 24300 24299 0 -1 0 300 1322 0 0 0 0 17 4 17 0 1 0 784873522 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+1010.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 15677
Raw data (stat): 15672 (minisat+_script) S 15671 24300 24299 0 -1 0 300 1322 0 0 0 0 17 4 17 0 1 0 784873522 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+1020 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 15677
Raw data (stat): 15672 (minisat+_script) S 15671 24300 24299 0 -1 0 300 1322 0 0 0 0 17 4 17 0 1 0 784873522 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+1030.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 15677
Raw data (stat): 15672 (minisat+_script) S 15671 24300 24299 0 -1 0 300 1322 0 0 0 0 17 4 17 0 1 0 784873522 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+1040.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 15677
Raw data (stat): 15672 (minisat+_script) S 15671 24300 24299 0 -1 0 300 1322 0 0 0 0 17 4 17 0 1 0 784873522 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+1050.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 15677
Raw data (stat): 15672 (minisat+_script) S 15671 24300 24299 0 -1 0 300 1322 0 0 0 0 17 4 17 0 1 0 784873522 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+1060.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 15677
Raw data (stat): 15672 (minisat+_script) S 15671 24300 24299 0 -1 0 300 1322 0 0 0 0 17 4 17 0 1 0 784873522 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+1070.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 15677
Raw data (stat): 15672 (minisat+_script) S 15671 24300 24299 0 -1 0 300 1322 0 0 0 0 17 4 17 0 1 0 784873522 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+1080.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 15677
Raw data (stat): 15672 (minisat+_script) S 15671 24300 24299 0 -1 0 300 1322 0 0 0 0 17 4 17 0 1 0 784873522 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+1090.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 15677
Raw data (stat): 15672 (minisat+_script) S 15671 24300 24299 0 -1 0 300 1322 0 0 0 0 17 4 17 0 1 0 784873522 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+1100.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 15677
Raw data (stat): 15672 (minisat+_script) S 15671 24300 24299 0 -1 0 300 1322 0 0 0 0 17 4 17 0 1 0 784873522 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+1110.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 15677
Raw data (stat): 15672 (minisat+_script) S 15671 24300 24299 0 -1 0 300 1322 0 0 0 0 17 4 17 0 1 0 784873522 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+1120.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 15677
Raw data (stat): 15672 (minisat+_script) S 15671 24300 24299 0 -1 0 300 1322 0 0 0 0 17 4 17 0 1 0 784873522 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+1130.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 15677
Raw data (stat): 15672 (minisat+_script) S 15671 24300 24299 0 -1 0 300 1322 0 0 0 0 17 4 17 0 1 0 784873522 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+1140.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 15677
Raw data (stat): 15672 (minisat+_script) S 15671 24300 24299 0 -1 0 300 1322 0 0 0 0 17 4 17 0 1 0 784873522 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+1150.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 15677
Raw data (stat): 15672 (minisat+_script) S 15671 24300 24299 0 -1 0 300 1322 0 0 0 0 17 4 17 0 1 0 784873522 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+1160.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 15677
Raw data (stat): 15672 (minisat+_script) S 15671 24300 24299 0 -1 0 300 1322 0 0 0 0 17 4 17 0 1 0 784873522 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+1170.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 15677
Raw data (stat): 15672 (minisat+_script) S 15671 24300 24299 0 -1 0 300 1322 0 0 0 0 17 4 17 0 1 0 784873522 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+1180.02 s]
Raw data (loadavg): 1.07 0.99 0.91 2/55 15677
Raw data (stat): 15672 (minisat+_script) S 15671 24300 24299 0 -1 0 300 1322 0 0 0 0 17 4 17 0 1 0 784873522 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+1190.02 s]
Raw data (loadavg): 1.06 0.99 0.91 2/55 15677
Raw data (stat): 15672 (minisat+_script) S 15671 24300 24299 0 -1 0 300 1322 0 0 0 0 17 4 17 0 1 0 784873522 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+1200.02 s]
Raw data (loadavg): 1.05 0.99 0.91 2/55 15677
Raw data (stat): 15672 (minisat+_script) S 15671 24300 24299 0 -1 0 300 1322 0 0 0 0 17 4 17 0 1 0 784873522 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+1210.02 s]
Raw data (loadavg): 1.04 0.99 0.91 2/55 15677
Raw data (stat): 15672 (minisat+_script) S 15671 24300 24299 0 -1 0 300 1322 0 0 0 0 17 4 17 0 1 0 784873522 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+1220.01 s]
Raw data (loadavg): 1.04 0.99 0.91 2/55 15677
Raw data (stat): 15672 (minisat+_script) S 15671 24300 24299 0 -1 0 300 1322 0 0 0 0 17 4 17 0 1 0 784873522 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+1229.93 s]
Raw data (loadavg): 1.03 0.99 0.91 1/53 15677
Raw data (stat): 15672 (minisat+_script) S 15671 24300 24299 0 -1 0 300 1322 0 0 0 0 17 4 17 0 1 0 784873522 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 0

Child status: 152
Real time (s): 1229.93
CPU time (s): 1230.11
CPU user time (s): 1228.91
CPU system time (s): 1.19782
CPU usage (%): 100.015
Max. virtual memory (Kb): 2128
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####