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/submitted/een/normalized-mitre.opb
MD5SUM	a32373ce42835aed9464b28f5a9ed13c
Bench Category	optimization, small integers (OPTSMALLINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	8818
Optimality of the best value was proved	NO
Number of terms in the objective function	9324
Biggest coefficient in the objective function	213
Number of bits for the biggest coefficient in the objective function	8
Sum of the numbers in the objective function	909647
Number of bits of the sum of numbers in the objective function	20
Biggest number in a constraint	1069
Number of bits of the biggest number in a constraint	11
Biggest sum of numbers in a constraint	909647
Number of bits of the biggest sum of numbers	20
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	1189.18
Number of variables	10724
Total number of constraints	2045
Number of constraints which are clauses	523
Number of constraints which are cardinality constraints (but not clauses)	1139
Number of constraints which are nor clauses,nor cardinality constraints	383
Minimum length of a constraint	3
Maximum length of a constraint	98
Trace number 7096

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc24 THE 2005-04-14 21:12:32 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=5132 boxname=wulflinc24 idbench=395 idsolver=10 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  a32373ce42835aed9464b28f5a9ed13c  /oldhome/oroussel/tmp/wulflinc24/normalized-mitre.opb
REAL COMMAND:  minisat+ -ca /oldhome/oroussel/tmp/wulflinc24/normalized-mitre.opb /oldhome/oroussel/tmp/wulflinc24/normalized-mitre.opb
IDLAUNCH: 5132
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.080
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	: 3
cpu MHz		: 451.080
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:        807700 kB
Buffers:         36128 kB
Cached:         147656 kB
SwapCached:       3828 kB
Active:          68116 kB
Inactive:       122368 kB
HighTotal:      131008 kB
HighFree:          252 kB
LowTotal:       903652 kB
LowFree:        807448 kB
SwapTotal:     2097892 kB
SwapFree:      2094064 kB
Dirty:              40 kB
Writeback:           0 kB
Mapped:           6924 kB
Slab:            30860 kB
Committed_AS:    63484 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-14 21:32:34 (client local time) WITH STATUS 0 IN 1200.24 SECONDS
stats: 5132 7 1200.24 0
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 2045 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: ===============================================================================================================================================================================================================================================================================================================================================================
c   -- Clauses(.)/Splits(s): ......................................................................................................................................................s...................sssss.sss.ssssss.sss.sssssssssssssssssssssssssssss.ssss.ssssssssssssssssssss..sssssssssssssss.s.sss.ss.ss.sssssssss
c ---[2116]---> Adder-cost: 5   maxlim: 1   bits: 2/1
c ---[2115]---> Adder-cost: 5   maxlim: 1   bits: 2/1
c ---[2114]---> Adder-cost: 5   maxlim: 1   bits: 2/1
c ---[2113]---> Adder-cost: 5   maxlim: 1   bits: 2/1
c ---[2112]---> Adder-cost: 5   maxlim: 1   bits: 2/1
c ---[2111]---> Adder-cost: 5   maxlim: 1   bits: 2/1
c ---[2110]---> Adder-cost: 5   maxlim: 1   bits: 2/1
c ---[2098]---> Adder-cost: 5   maxlim: 1   bits: 2/1
c ---[2097]---> Adder-cost: 5   maxlim: 1   bits: 2/1
c ---[2096]---> Adder-cost: 5   maxlim: 1   bits: 2/1
c ---[2095]---> Adder-cost: 5   maxlim: 1   bits: 2/1
c ---[2094]---> Adder-cost: 5   maxlim: 1   bits: 2/1
c ---[2093]---> Adder-cost: 5   maxlim: 1   bits: 2/1
c ---[2092]---> Adder-cost: 5   maxlim: 1   bits: 2/1
c ---[2091]---> Adder-cost: 5   maxlim: 1   bits: 2/1
c ---[2090]---> Adder-cost: 5   maxlim: 1   bits: 2/1
c ---[2089]---> Adder-cost: 5   maxlim: 1   bits: 2/1
c ---[2088]---> Adder-cost: 5   maxlim: 1   bits: 2/1
c ---[2087]---> Adder-cost: 5   maxlim: 1   bits: 2/1
c ---[2086]---> Adder-cost: 5   maxlim: 1   bits: 2/1
c ---[2085]---> Adder-cost: 5   maxlim: 1   bits: 2/1
c ---[2074]---> Adder-cost: 5   maxlim: 1   bits: 2/1
c ---[2073]---> Adder-cost: 5   maxlim: 1   bits: 2/1
c ---[2072]---> Adder-cost: 5   maxlim: 1   bits: 2/1
c ---[2071]---> Adder-cost: 5   maxlim: 1   bits: 2/1
c ---[2070]---> Adder-cost: 5   maxlim: 1   bits: 2/1
c ---[2069]---> Adder-cost: 5   maxlim: 1   bits: 2/1
c ---[2068]---> Adder-cost: 5   maxlim: 1   bits: 2/1
c ---[2067]---> Adder-cost: 5   maxlim: 1   bits: 2/1
c ---[2066]---> Adder-cost: 5   maxlim: 1   bits: 2/1
c ---[2065]---> Adder-cost: 5   maxlim: 1   bits: 2/1
c ---[2064]---> Adder-cost: 5   maxlim: 1   bits: 2/1
c ---[2063]---> Adder-cost: 5   maxlim: 1   bits: 2/1
c ---[2062]---> Adder-cost: 5   maxlim: 1   bits: 2/1
c ---[2061]---> Adder-cost: 5   maxlim: 1   bits: 2/1
c ---[2060]---> Adder-cost: 5   maxlim: 1   bits: 2/1
c ---[2059]---> Adder-cost: 5   maxlim: 1   bits: 2/1
c ---[2058]---> Adder-cost: 5   maxlim: 1   bits: 2/1
c ---[2057]---> Adder-cost: 5   maxlim: 1   bits: 2/1
c ---[2049]---> Adder-cost: 5   maxlim: 1   bits: 2/1
c ---[2048]---> Adder-cost: 5   maxlim: 1   bits: 2/1
c ---[2047]---> Adder-cost: 5   maxlim: 1   bits: 2/1
c ---[2035]---> Adder-cost: 5   maxlim: 1   bits: 2/1
c ---[2034]---> Adder-cost: 5   maxlim: 1   bits: 2/1
c ---[2033]---> Adder-cost: 5   maxlim: 1   bits: 2/1
c ---[1997]---> Adder-cost: 5   maxlim: 1   bits: 2/1
c ---[1996]---> Adder-cost: 5   maxlim: 1   bits: 2/1
c ---[1995]---> Adder-cost: 5   maxlim: 1   bits: 2/1
c ---[1994]---> Adder-cost: 5   maxlim: 1   bits: 2/1
c ---[1993]---> Adder-cost: 5   maxlim: 1   bits: 2/1
c ---[1992]---> Adder-cost: 5   maxlim: 1   bits: 2/1
c ---[1991]---> Adder-cost: 5   maxlim: 1   bits: 2/1
c ---[1990]---> Adder-cost: 5   maxlim: 1   bits: 2/1
c ---[1989]---> Adder-cost: 5   maxlim: 1   bits: 2/1
c ---[1988]---> Adder-cost: 5   maxlim: 1   bits: 2/1
c ---[1987]---> Adder-cost: 5   maxlim: 1   bits: 2/1
c ---[1986]---> Adder-cost: 5   maxlim: 1   bits: 2/1
c ---[1985]---> Adder-cost: 5   maxlim: 1   bits: 2/1
c ---[1984]---> Adder-cost: 5   maxlim: 1   bits: 2/1
c ---[1983]---> Adder-cost: 5   maxlim: 1   bits: 2/1
c ---[1982]---> Adder-cost: 5   maxlim: 1   bits: 2/1
c ---[1981]---> Adder-cost: 5   maxlim: 1   bits: 2/1
c ---[1980]---> Adder-cost: 5   maxlim: 1   bits: 2/1
c ---[1979]---> Adder-cost: 5   maxlim: 1   bits: 2/1
c ---[1978]---> Adder-cost: 5   maxlim: 1   bits: 2/1
c ---[1977]---> Adder-cost: 5   maxlim: 1   bits: 2/1
c ---[1976]---> Adder-cost: 5   maxlim: 1   bits: 2/1
c ---[1975]---> Adder-cost: 5   maxlim: 1   bits: 2/1
c ---[1974]---> Adder-cost: 5   maxlim: 1   bits: 2/1
c ---[1973]---> Adder-cost: 5   maxlim: 1   bits: 2/1
c ---[1965]---> Adder-cost: 5   maxlim: 1   bits: 2/1
c ---[1964]---> Adder-cost: 5   maxlim: 1   bits: 2/1
c ---[1963]---> Adder-cost: 5   maxlim: 1   bits: 2/1
c ---[1962]---> Adder-cost: 5   maxlim: 1   bits: 2/1
c ---[1961]---> Adder-cost: 5   maxlim: 1   bits: 2/1
c ---[1960]---> Adder-cost: 5   maxlim: 1   bits: 2/1
c ---[1959]---> Adder-cost: 5   maxlim: 1   bits: 2/1
c ---[1958]---> Adder-cost: 5   maxlim: 1   bits: 2/1
c ---[1957]---> Adder-cost: 5   maxlim: 1   bits: 2/1
c ---[1956]---> Adder-cost: 5   maxlim: 1   bits: 2/1
c ---[1955]---> Adder-cost: 5   maxlim: 1   bits: 2/1
c ---[1954]---> Adder-cost: 5   maxlim: 1   bits: 2/1
c ---[1953]---> Adder-cost: 5   maxlim: 1   bits: 2/1
c ---[1952]---> Adder-cost: 5   maxlim: 1   bits: 2/1
c ---[1951]---> Adder-cost: 5   maxlim: 1   bits: 2/1
c ---[1950]---> Adder-cost: 5   maxlim: 1   bits: 2/1
c ---[1949]---> Adder-cost: 5   maxlim: 1   bits: 2/1
c ---[1948]---> Adder-cost: 5   maxlim: 1   bits: 2/1
c ---[1947]---> Adder-cost: 5   maxlim: 1   bits: 2/1
c ---[1946]---> Adder-cost: 5   maxlim: 1   bits: 2/1
c ---[1945]---> Adder-cost: 5   maxlim: 1   bits: 2/1
c ---[1944]---> Adder-cost: 5   maxlim: 1   bits: 2/1
c ---[1943]---> Adder-cost: 5   maxlim: 1   bits: 2/1
c ---[1942]---> Adder-cost: 5   maxlim: 1   bits: 2/1
c ---[1941]---> Adder-cost: 5   maxlim: 1   bits: 2/1
c ---[1940]---> Adder-cost: 5   maxlim: 1   bits: 2/1
c ---[1939]---> Adder-cost: 5   maxlim: 1   bits: 2/1
c ---[1938]---> Adder-cost: 5   maxlim: 1   bits: 2/1
c ---[1937]---> Adder-cost: 5   maxlim: 1   bits: 2/1
c ---[1936]---> Adder-cost: 5   maxlim: 1   bits: 2/1
c ---[1935]---> Adder-cost: 5   maxlim: 1   bits: 2/1
c ---[1934]---> Adder-cost: 5   maxlim: 1   bits: 2/1
c ---[1933]---> Adder-cost: 5   maxlim: 1   bits: 2/1
c ---[1932]---> Adder-cost: 5   maxlim: 1   bits: 2/1
c ---[1931]---> Adder-cost: 5   maxlim: 1   bits: 2/1
c ---[1930]---> Adder-cost: 5   maxlim: 1   bits: 2/1
c ---[1929]---> Adder-cost: 5   maxlim: 1   bits: 2/1
c ---[1928]---> Adder-cost: 5   maxlim: 1   bits: 2/1
c ---[1927]---> Adder-cost: 5   maxlim: 1   bits: 2/1
c ---[1926]---> Adder-cost: 5   maxlim: 1   bits: 2/1
c ---[1925]---> Adder-cost: 5   maxlim: 1   bits: 2/1
c ---[1924]---> Adder-cost: 5   maxlim: 1   bits: 2/1
c ---[1923]---> Adder-cost: 5   maxlim: 1   bits: 2/1
c ---[1922]---> Adder-cost: 5   maxlim: 1   bits: 2/1
c ---[1921]---> Adder-cost: 5   maxlim: 1   bits: 2/1
c ---[1920]---> Adder-cost: 5   maxlim: 1   bits: 2/1
c ---[1919]---> Adder-cost: 5   maxlim: 1   bits: 2/1
c ---[1918]---> Adder-cost: 5   maxlim: 1   bits: 2/1
c ---[1917]---> Adder-cost: 5   maxlim: 1   bits: 2/1
c ---[1916]---> Adder-cost: 5   maxlim: 1   bits: 2/1
c ---[1915]---> Adder-cost: 5   maxlim: 1   bits: 2/1
c ---[1914]---> Adder-cost: 5   maxlim: 1   bits: 2/1
c ---[1913]---> Adder-cost: 5   maxlim: 1   bits: 2/1
c ---[1912]---> Adder-cost: 5   maxlim: 1   bits: 2/1
c ---[1911]---> Adder-cost: 5   maxlim: 1   bits: 2/1
c ---[1910]---> Adder-cost: 5   maxlim: 1   bits: 2/1
c ---[1909]---> Adder-cost: 5   maxlim: 1   bits: 2/1
c ---[1908]---> Adder-cost: 5   maxlim: 1   bits: 2/1
c ---[1907]---> Adder-cost: 5   maxlim: 1   bits: 2/1
c ---[1906]---> Adder-cost: 5   maxlim: 1   bits: 2/1
c ---[1905]---> Adder-cost: 5   maxlim: 1   bits: 2/1
c ---[1904]---> Adder-cost: 5   maxlim: 1   bits: 2/1
c ---[1903]---> Adder-cost: 5   maxlim: 1   bits: 2/1
c ---[1902]---> Adder-cost: 5   maxlim: 1   bits: 2/1
c ---[1901]---> Adder-cost: 5   maxlim: 1   bits: 2/1
c ---[1900]---> Adder-cost: 5   maxlim: 1   bits: 2/1
c ---[1899]---> Adder-cost: 5   maxlim: 1   bits: 2/1
c ---[1898]---> Adder-cost: 5   maxlim: 1   bits: 2/1
c ---[1897]---> Adder-cost: 5   maxlim: 1   bits: 2/1
c ---[1896]---> Adder-cost: 5   maxlim: 1   bits: 2/1
c ---[1895]---> Adder-cost: 8   maxlim: 3   bits: 3/2
c ---[1894]---> Adder-cost: 8   maxlim: 3   bits: 3/2
c ---[1893]---> Adder-cost: 8   maxlim: 3   bits: 3/2
c ---[1892]---> Adder-cost: 8   maxlim: 3   bits: 3/2
c ---[1891]---> Adder-cost: 8   maxlim: 3   bits: 3/2
c ---[1890]---> Adder-cost: 8   maxlim: 3   bits: 3/2
c ---[1889]---> Adder-cost: 8   maxlim: 3   bits: 3/2
c ---[1888]---> Adder-cost: 8   maxlim: 3   bits: 3/2
c ---[1887]---> Adder-cost: 8   maxlim: 3   bits: 3/2
c ---[1886]---> Adder-cost: 8   maxlim: 3   bits: 3/2
c ---[1885]---> Adder-cost: 8   maxlim: 3   bits: 3/2
c ---[1884]---> Adder-cost: 8   maxlim: 3   bits: 3/2
c ---[1883]---> Adder-cost: 8   maxlim: 3   bits: 3/2
c ---[1882]---> Adder-cost: 8   maxlim: 3   bits: 3/2
c ---[1881]---> Adder-cost: 8   maxlim: 3   bits: 3/2
c ---[1880]---> Adder-cost: 8   maxlim: 3   bits: 3/2
c ---[1879]---> Adder-cost: 8   maxlim: 3   bits: 3/2
c ---[1878]---> Adder-cost: 8   maxlim: 3   bits: 3/2
c ---[1877]---> Adder-cost: 8   maxlim: 3   bits: 3/2
c ---[1876]---> Adder-cost: 8   maxlim: 3   bits: 3/2
c ---[1875]---> Adder-cost: 8   maxlim: 3   bits: 3/2
c ---[1874]---> Adder-cost: 8   maxlim: 3   bits: 3/2
c ---[1873]---> Adder-cost: 8   maxlim: 3   bits: 3/2
c ---[1872]---> Adder-cost: 8   maxlim: 3   bits: 3/2
c ---[1871]---> Adder-cost: 8   maxlim: 3   bits: 3/2
c ---[1870]---> Adder-cost: 8   maxlim: 3   bits: 3/2
c ---[1869]---> Adder-cost: 8   maxlim: 3   bits: 3/2
c ---[1868]---> Adder-cost: 8   maxlim: 3   bits: 3/2
c ---[1867]---> Adder-cost: 8   maxlim: 3   bits: 3/2
c ---[1866]---> Adder-cost: 8   maxlim: 3   bits: 3/2
c ---[1865]---> Adder-cost: 8   maxlim: 3   bits: 3/2
c ---[1864]---> Adder-cost: 8   maxlim: 3   bits: 3/2
c ---[1863]---> Adder-cost: 8   maxlim: 3   bits: 3/2
c ---[1862]---> Adder-cost: 8   maxlim: 3   bits: 3/2
c ---[1861]---> Adder-cost: 8   maxlim: 3   bits: 3/2
c ---[1843]---> Adder-cost: 8   maxlim: 3   bits: 3/2
c ---[1842]---> Adder-cost: 8   maxlim: 3   bits: 3/2
c ---[1841]---> Adder-cost: 8   maxlim: 3   bits: 3/2
c ---[1840]---> Adder-cost: 8   maxlim: 3   bits: 3/2
c ---[1839]---> Adder-cost: 8   maxlim: 3   bits: 3/2
c ---[1838]---> Adder-cost: 8   maxlim: 3   bits: 3/2
c ---[1837]---> Adder-cost: 8   maxlim: 3   bits: 3/2
c ---[1825]---> Adder-cost: 8   maxlim: 3   bits: 3/2
c ---[1824]---> Adder-cost: 8   maxlim: 3   bits: 3/2
c ---[1823]---> Adder-cost: 8   maxlim: 3   bits: 3/2
c ---[1822]---> Adder-cost: 8   maxlim: 3   bits: 3/2
c ---[1821]---> Adder-cost: 8   maxlim: 3   bits: 3/2
c ---[1820]---> Adder-cost: 8   maxlim: 3   bits: 3/2
c ---[1819]---> Adder-cost: 8   maxlim: 3   bits: 3/2
c ---[1818]---> Adder-cost: 8   maxlim: 3   bits: 3/2
c ---[1817]---> Adder-cost: 8   maxlim: 3   bits: 3/2
c ---[1816]---> Adder-cost: 8   maxlim: 3   bits: 3/2
c ---[1815]---> Adder-cost: 8   maxlim: 3   bits: 3/2
c ---[1814]---> Adder-cost: 8   maxlim: 3   bits: 3/2
c ---[1813]---> Adder-cost: 8   maxlim: 3   bits: 3/2
c ---[1812]---> Adder-cost: 8   maxlim: 3   bits: 3/2
c ---[1811]---> Adder-cost: 8   maxlim: 3   bits: 3/2
c ---[1810]---> Adder-cost: 8   maxlim: 3   bits: 3/2
c ---[1809]---> Adder-cost: 8   maxlim: 3   bits: 3/2
c ---[1808]---> Adder-cost: 8   maxlim: 3   bits: 3/2
c ---[1807]---> Adder-cost: 8   maxlim: 3   bits: 3/2
c ---[1806]---> Adder-cost: 8   maxlim: 3   bits: 3/2
c ---[1805]---> Adder-cost: 8   maxlim: 3   bits: 3/2
c ---[1804]---> Adder-cost: 8   maxlim: 3   bits: 3/2
c ---[1803]---> Adder-cost: 8   maxlim: 3   bits: 3/2
c ---[1802]---> Adder-cost: 8   maxlim: 3   bits: 3/2
c ---[1801]---> Adder-cost: 8   maxlim: 3   bits: 3/2
c ---[1800]---> Adder-cost: 8   maxlim: 3   bits: 3/2
c ---[1799]---> Adder-cost: 8   maxlim: 3   bits: 3/2
c ---[1798]---> Adder-cost: 8   maxlim: 3   bits: 3/2
c ---[1797]---> Adder-cost: 8   maxlim: 3   bits: 3/2
c ---[1796]---> Adder-cost: 8   maxlim: 3   bits: 3/2
c ---[1795]---> Adder-cost: 8   maxlim: 3   bits: 3/2
c ---[1794]---> Adder-cost: 8   maxlim: 3   bits: 3/2
c ---[1793]---> Adder-cost: 8   maxlim: 3   bits: 3/2
c ---[1792]---> Adder-cost: 8   maxlim: 3   bits: 3/2
c ---[1791]---> Adder-cost: 8   maxlim: 3   bits: 3/2
c ---[1790]---> Adder-cost: 8   maxlim: 3   bits: 3/2
c ---[1789]---> Adder-cost: 8   maxlim: 3   bits: 3/2
c ---[1788]---> Adder-cost: 8   maxlim: 3   bits: 3/2
c ---[1787]---> Adder-cost: 8   maxlim: 3   bits: 3/2
c ---[1786]---> Adder-cost: 8   maxlim: 3   bits: 3/2
c ---[1785]---> Adder-cost: 8   maxlim: 3   bits: 3/2
c ---[1784]---> Adder-cost: 8   maxlim: 3   bits: 3/2
c ---[1783]---> Adder-cost: 8   maxlim: 3   bits: 3/2
c ---[1782]---> Adder-cost: 8   maxlim: 3   bits: 3/2
c ---[1781]---> Adder-cost: 8   maxlim: 3   bits: 3/2
c ---[1780]---> Adder-cost: 8   maxlim: 3   bits: 3/2
c ---[1779]---> Adder-cost: 8   maxlim: 3   bits: 3/2
c ---[1778]---> Adder-cost: 8   maxlim: 3   bits: 3/2
c ---[1777]---> Adder-cost: 8   maxlim: 3   bits: 3/2
c ---[1776]---> Adder-cost: 8   maxlim: 3   bits: 3/2
c ---[1775]---> Adder-cost: 8   maxlim: 3   bits: 3/2
c ---[1774]---> Adder-cost: 8   maxlim: 3   bits: 3/2
c ---[1773]---> Adder-cost: 8   maxlim: 3   bits: 3/2
c ---[1772]---> Adder-cost: 8   maxlim: 3   bits: 3/2
c ---[1771]---> Adder-cost: 8   maxlim: 3   bits: 3/2
c ---[1770]---> Adder-cost: 8   maxlim: 3   bits: 3/2
c ---[1769]---> Adder-cost: 8   maxlim: 3   bits: 3/2
c ---[1768]---> Adder-cost: 8   maxlim: 3   bits: 3/2
c ---[1767]---> Adder-cost: 8   maxlim: 3   bits: 3/2
c ---[1766]---> Adder-cost: 8   maxlim: 3   bits: 3/2
c ---[1765]---> Adder-cost: 8   maxlim: 3   bits: 3/2
c ---[1764]---> Adder-cost: 8   maxlim: 3   bits: 3/2
c ---[1763]---> Adder-cost: 8   maxlim: 3   bits: 3/2
c ---[1762]---> Adder-cost: 8   maxlim: 3   bits: 3/2
c ---[1761]---> Adder-cost: 8   maxlim: 3   bits: 3/2
c ---[1760]---> Adder-cost: 8   maxlim: 3   bits: 3/2
c ---[1759]---> Adder-cost: 8   maxlim: 3   bits: 3/2
c ---[1758]---> Adder-cost: 8   maxlim: 3   bits: 3/2
c ---[1757]---> Adder-cost: 8   maxlim: 3   bits: 3/2
c ---[1756]---> Adder-cost: 8   maxlim: 3   bits: 3/2
c ---[1755]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[1754]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[1753]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[1752]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[1751]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[1750]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[1749]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[1748]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[1747]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[1746]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[1745]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[1744]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[1743]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[1742]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[1741]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[1740]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[1739]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[1738]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[1737]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[1736]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[1735]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[1734]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[1733]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[1732]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[1731]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[1730]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[1729]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[1728]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[1727]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[1726]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[1725]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[1724]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[1723]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[1722]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[1721]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[1720]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[1719]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[1718]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[1717]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[1716]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[1715]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[1714]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[1713]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[1712]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[1711]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[1710]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[1709]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[1708]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[1707]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[1706]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[1705]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[1704]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[1703]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[1702]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[1701]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[1700]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[1699]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[1698]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[1697]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[1696]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[1695]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[1694]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[1693]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[1692]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[1691]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[1690]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[1689]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[1688]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[1687]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[1686]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[1685]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[1684]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[1683]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[1682]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[1681]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[1680]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[1679]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[1678]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[1677]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[1676]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[1675]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[1674]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[1673]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[1672]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[1671]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[1670]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[1669]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[1668]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[1667]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[1666]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[1665]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[1664]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[1663]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[1662]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[1661]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[1660]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[1659]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[1658]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[1657]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[1656]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[1655]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[1654]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[1653]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[1652]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[1651]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[1650]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[1649]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[1648]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[1647]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[1646]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[1645]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[1644]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[1643]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[1642]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[1641]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[1640]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[1639]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[1638]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[1637]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[1636]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[1635]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[1634]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[1633]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[1632]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[1631]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[1630]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[1629]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[1628]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[1627]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[1626]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[1625]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[1624]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[1623]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[1622]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[1621]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[1620]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[1619]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[1618]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[1617]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[1616]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[1615]---> Adder-cost: 14   maxlim: 5   bits: 4/3
c ---[1614]---> Adder-cost: 14   maxlim: 5   bits: 4/3
c ---[1613]---> Adder-cost: 14   maxlim: 5   bits: 4/3
c ---[1612]---> Adder-cost: 14   maxlim: 5   bits: 4/3
c ---[1611]---> Adder-cost: 14   maxlim: 5   bits: 4/3
c ---[1610]---> Adder-cost: 14   maxlim: 5   bits: 4/3
c ---[1609]---> Adder-cost: 14   maxlim: 5   bits: 4/3
c ---[1608]---> Adder-cost: 14   maxlim: 5   bits: 4/3
c ---[1607]---> Adder-cost: 14   maxlim: 5   bits: 4/3
c ---[1606]---> Adder-cost: 14   maxlim: 5   bits: 4/3
c ---[1605]---> Adder-cost: 14   maxlim: 5   bits: 4/3
c ---[1604]---> Adder-cost: 14   maxlim: 5   bits: 4/3
c ---[1603]---> Adder-cost: 14   maxlim: 5   bits: 4/3
c ---[1602]---> Adder-cost: 14   maxlim: 5   bits: 4/3
c ---[1601]---> Adder-cost: 14   maxlim: 5   bits: 4/3
c ---[1600]---> Adder-cost: 14   maxlim: 5   bits: 4/3
c ---[1599]---> Adder-cost: 14   maxlim: 5   bits: 4/3
c ---[1598]---> Adder-cost: 14   maxlim: 5   bits: 4/3
c ---[1597]---> Adder-cost: 14   maxlim: 5   bits: 4/3
c ---[1596]---> Adder-cost: 14   maxlim: 5   bits: 4/3
c ---[1595]---> Adder-cost: 14   maxlim: 5   bits: 4/3
c ---[1594]---> Adder-cost: 14   maxlim: 5   bits: 4/3
c ---[1593]---> Adder-cost: 14   maxlim: 5   bits: 4/3
c ---[1592]---> Adder-cost: 14   maxlim: 5   bits: 4/3
c ---[1591]---> Adder-cost: 14   maxlim: 5   bits: 4/3
c ---[1590]---> Adder-cost: 14   maxlim: 5   bits: 4/3
c ---[1589]---> Adder-cost: 14   maxlim: 5   bits: 4/3
c ---[1588]---> Adder-cost: 14   maxlim: 5   bits: 4/3
c ---[1587]---> Adder-cost: 14   maxlim: 5   bits: 4/3
c ---[1586]---> Adder-cost: 14   maxlim: 5   bits: 4/3
c ---[1585]---> Adder-cost: 14   maxlim: 5   bits: 4/3
c ---[1584]---> Adder-cost: 14   maxlim: 5   bits: 4/3
c ---[1583]---> Adder-cost: 14   maxlim: 5   bits: 4/3
c ---[1582]---> Adder-cost: 14   maxlim: 5   bits: 4/3
c ---[1581]---> Adder-cost: 14   maxlim: 5   bits: 4/3
c ---[1580]---> Adder-cost: 14   maxlim: 5   bits: 4/3
c ---[1579]---> Adder-cost: 14   maxlim: 5   bits: 4/3
c ---[1578]---> Adder-cost: 14   maxlim: 5   bits: 4/3
c ---[1577]---> Adder-cost: 14   maxlim: 5   bits: 4/3
c ---[1576]---> Adder-cost: 14   maxlim: 5   bits: 4/3
c ---[1575]---> Adder-cost: 14   maxlim: 5   bits: 4/3
c ---[1574]---> Adder-cost: 14   maxlim: 5   bits: 4/3
c ---[1573]---> Adder-cost: 14   maxlim: 5   bits: 4/3
c ---[1572]---> Adder-cost: 14   maxlim: 5   bits: 4/3
c ---[1571]---> Adder-cost: 14   maxlim: 5   bits: 4/3
c ---[1570]---> Adder-cost: 14   maxlim: 5   bits: 4/3
c ---[1569]---> Adder-cost: 14   maxlim: 5   bits: 4/3
c ---[1568]---> Adder-cost: 14   maxlim: 5   bits: 4/3
c ---[1567]---> Adder-cost: 14   maxlim: 5   bits: 4/3
c ---[1566]---> Adder-cost: 14   maxlim: 5   bits: 4/3
c ---[1565]---> Adder-cost: 14   maxlim: 5   bits: 4/3
c ---[1564]---> Adder-cost: 14   maxlim: 5   bits: 4/3
c ---[1563]---> Adder-cost: 14   maxlim: 5   bits: 4/3
c ---[1562]---> Adder-cost: 14   maxlim: 5   bits: 4/3
c ---[1561]---> Adder-cost: 14   maxlim: 5   bits: 4/3
c ---[1560]---> Adder-cost: 14   maxlim: 5   bits: 4/3
c ---[1559]---> Adder-cost: 14   maxlim: 5   bits: 4/3
c ---[1558]---> Adder-cost: 14   maxlim: 5   bits: 4/3
c ---[1557]---> Adder-cost: 14   maxlim: 5   bits: 4/3
c ---[1556]---> Adder-cost: 14   maxlim: 5   bits: 4/3
c ---[1555]---> Adder-cost: 14   maxlim: 5   bits: 4/3
c ---[1554]---> Adder-cost: 14   maxlim: 5   bits: 4/3
c ---[1553]---> Adder-cost: 14   maxlim: 5   bits: 4/3
c ---[1552]---> Adder-cost: 14   maxlim: 5   bits: 4/3
c ---[1551]---> Adder-cost: 14   maxlim: 5   bits: 4/3
c ---[1550]---> Adder-cost: 14   maxlim: 5   bits: 4/3
c ---[1549]---> Adder-cost: 14   maxlim: 5   bits: 4/3
c ---[1548]---> Adder-cost: 14   maxlim: 5   bits: 4/3
c ---[1547]---> Adder-cost: 14   maxlim: 5   bits: 4/3
c ---[1546]---> Adder-cost: 14   maxlim: 5   bits: 4/3
c ---[1545]---> Adder-cost: 14   maxlim: 5   bits: 4/3
c ---[1544]---> Adder-cost: 14   maxlim: 5   bits: 4/3
c ---[1543]---> Adder-cost: 14   maxlim: 5   bits: 4/3
c ---[1542]---> Adder-cost: 14   maxlim: 5   bits: 4/3
c ---[1541]---> Adder-cost: 14   maxlim: 5   bits: 4/3
c ---[1540]---> Adder-cost: 14   maxlim: 5   bits: 4/3
c ---[1539]---> Adder-cost: 14   maxlim: 5   bits: 4/3
c ---[1538]---> Adder-cost: 14   maxlim: 5   bits: 4/3
c ---[1537]---> Adder-cost: 14   maxlim: 5   bits: 4/3
c ---[1536]---> Adder-cost: 14   maxlim: 5   bits: 4/3
c ---[1535]---> Adder-cost: 14   maxlim: 5   bits: 4/3
c ---[1534]---> Adder-cost: 14   maxlim: 5   bits: 4/3
c ---[1533]---> Adder-cost: 14   maxlim: 5   bits: 4/3
c ---[1532]---> Adder-cost: 14   maxlim: 5   bits: 4/3
c ---[1531]---> Adder-cost: 14   maxlim: 6   bits: 4/3
c ---[1530]---> Adder-cost: 14   maxlim: 6   bits: 4/3
c ---[1529]---> Adder-cost: 14   maxlim: 6   bits: 4/3
c ---[1528]---> Adder-cost: 14   maxlim: 6   bits: 4/3
c ---[1527]---> Adder-cost: 14   maxlim: 6   bits: 4/3
c ---[1526]---> Adder-cost: 14   maxlim: 6   bits: 4/3
c ---[1525]---> Adder-cost: 14   maxlim: 6   bits: 4/3
c ---[1524]---> Adder-cost: 14   maxlim: 6   bits: 4/3
c ---[1523]---> Adder-cost: 14   maxlim: 6   bits: 4/3
c ---[1522]---> Adder-cost: 14   maxlim: 6   bits: 4/3
c ---[1521]---> Adder-cost: 14   maxlim: 6   bits: 4/3
c ---[1520]---> Adder-cost: 14   maxlim: 6   bits: 4/3
c ---[1519]---> Adder-cost: 14   maxlim: 6   bits: 4/3
c ---[1518]---> Adder-cost: 14   maxlim: 6   bits: 4/3
c ---[1517]---> Adder-cost: 14   maxlim: 6   bits: 4/3
c ---[1516]---> Adder-cost: 14   maxlim: 6   bits: 4/3
c ---[1515]---> Adder-cost: 14   maxlim: 6   bits: 4/3
c ---[1514]---> Adder-cost: 14   maxlim: 6   bits: 4/3
c ---[1513]---> Adder-cost: 14   maxlim: 6   bits: 4/3
c ---[1512]---> Adder-cost: 14   maxlim: 6   bits: 4/3
c ---[1511]---> Adder-cost: 14   maxlim: 6   bits: 4/3
c ---[1510]---> Adder-cost: 14   maxlim: 6   bits: 4/3
c ---[1509]---> Adder-cost: 14   maxlim: 6   bits: 4/3
c ---[1508]---> Adder-cost: 14   maxlim: 6   bits: 4/3
c ---[1507]---> Adder-cost: 14   maxlim: 6   bits: 4/3
c ---[1506]---> Adder-cost: 14   maxlim: 6   bits: 4/3
c ---[1505]---> Adder-cost: 14   maxlim: 6   bits: 4/3
c ---[1504]---> Adder-cost: 14   maxlim: 6   bits: 4/3
c ---[1503]---> Adder-cost: 16   maxlim: 7   bits: 4/3
c ---[1502]---> Adder-cost: 16   maxlim: 7   bits: 4/3
c ---[1501]---> Adder-cost: 16   maxlim: 7   bits: 4/3
c ---[1500]---> Adder-cost: 16   maxlim: 7   bits: 4/3
c ---[1499]---> Adder-cost: 16   maxlim: 7   bits: 4/3
c ---[1498]---> Adder-cost: 16   maxlim: 7   bits: 4/3
c ---[1497]---> Adder-cost: 16   maxlim: 7   bits: 4/3
c ---[1496]---> Adder-cost: 16   maxlim: 7   bits: 4/3
c ---[1495]---> Adder-cost: 16   maxlim: 7   bits: 4/3
c ---[1494]---> Adder-cost: 16   maxlim: 7   bits: 4/3
c ---[1493]---> Adder-cost: 16   maxlim: 7   bits: 4/3
c ---[1492]---> Adder-cost: 16   maxlim: 7   bits: 4/3
c ---[1491]---> Adder-cost: 16   maxlim: 7   bits: 4/3
c ---[1490]---> Adder-cost: 16   maxlim: 7   bits: 4/3
c ---[1489]---> Adder-cost: 16   maxlim: 7   bits: 4/3
c ---[1488]---> Adder-cost: 16   maxlim: 7   bits: 4/3
c ---[1487]---> Adder-cost: 16   maxlim: 7   bits: 4/3
c ---[1486]---> Adder-cost: 16   maxlim: 7   bits: 4/3
c ---[1485]---> Adder-cost: 16   maxlim: 7   bits: 4/3
c ---[1484]---> Adder-cost: 16   maxlim: 7   bits: 4/3
c ---[1483]---> Adder-cost: 16   maxlim: 7   bits: 4/3
c ---[1482]---> Adder-cost: 16   maxlim: 7   bits: 4/3
c ---[1481]---> Adder-cost: 16   maxlim: 7   bits: 4/3
c ---[1480]---> Adder-cost: 16   maxlim: 7   bits: 4/3
c ---[1479]---> Adder-cost: 16   maxlim: 7   bits: 4/3
c ---[1478]---> Adder-cost: 16   maxlim: 7   bits: 4/3
c ---[1477]---> Adder-cost: 16   maxlim: 7   bits: 4/3
c ---[1476]---> Adder-cost: 16   maxlim: 7   bits: 4/3
c ---[1475]---> Adder-cost: 15   maxlim: 3   bits: 3/2
c ---[1474]---> Adder-cost: 15   maxlim: 3   bits: 3/2
c ---[1473]---> Adder-cost: 15   maxlim: 3   bits: 3/2
c ---[1472]---> Adder-cost: 15   maxlim: 3   bits: 3/2
c ---[1471]---> Adder-cost: 15   maxlim: 3   bits: 3/2
c ---[1470]---> Adder-cost: 15   maxlim: 3   bits: 3/2
c ---[1469]---> Adder-cost: 15   maxlim: 3   bits: 3/2
c ---[1468]---> Adder-cost: 15   maxlim: 3   bits: 3/2
c ---[1467]---> Adder-cost: 15   maxlim: 3   bits: 3/2
c ---[1466]---> Adder-cost: 15   maxlim: 3   bits: 3/2
c ---[1465]---> Adder-cost: 15   maxlim: 3   bits: 3/2
c ---[1464]---> Adder-cost: 15   maxlim: 3   bits: 3/2
c ---[1463]---> Adder-cost: 15   maxlim: 3   bits: 3/2
c ---[1462]---> Adder-cost: 15   maxlim: 3   bits: 3/2
c ---[1461]---> Adder-cost: 15   maxlim: 3   bits: 3/2
c ---[1460]---> Adder-cost: 15   maxlim: 3   bits: 3/2
c ---[1459]---> Adder-cost: 15   maxlim: 3   bits: 3/2
c ---[1458]---> Adder-cost: 15   maxlim: 3   bits: 3/2
c ---[1457]---> Adder-cost: 15   maxlim: 3   bits: 3/2
c ---[1456]---> Adder-cost: 15   maxlim: 3   bits: 3/2
c ---[1455]---> Adder-cost: 15   maxlim: 3   bits: 3/2
c ---[1454]---> Adder-cost: 15   maxlim: 3   bits: 3/2
c ---[1453]---> Adder-cost: 15   maxlim: 3   bits: 3/2
c ---[1452]---> Adder-cost: 15   maxlim: 3   bits: 3/2
c ---[1451]---> Adder-cost: 15   maxlim: 3   bits: 3/2
c ---[1450]---> Adder-cost: 15   maxlim: 3   bits: 3/2
c ---[1449]---> Adder-cost: 15   maxlim: 3   bits: 3/2
c ---[1448]---> Adder-cost: 15   maxlim: 3   bits: 3/2
c ---[1447]---> Adder-cost: 16   maxlim: 8   bits: 4/4
c ---[1446]---> Adder-cost: 16   maxlim: 8   bits: 4/4
c ---[1445]---> Adder-cost: 16   maxlim: 8   bits: 4/4
c ---[1444]---> Adder-cost: 16   maxlim: 8   bits: 4/4
c ---[1443]---> Adder-cost: 16   maxlim: 8   bits: 4/4
c ---[1442]---> Adder-cost: 16   maxlim: 8   bits: 4/4
c ---[1441]---> Adder-cost: 16   maxlim: 8   bits: 4/4
c ---[1440]---> Adder-cost: 16   maxlim: 8   bits: 4/4
c ---[1439]---> Adder-cost: 16   maxlim: 8   bits: 4/4
c ---[1438]---> Adder-cost: 16   maxlim: 8   bits: 4/4
c ---[1437]---> Adder-cost: 16   maxlim: 8   bits: 4/4
c ---[1436]---> Adder-cost: 16   maxlim: 8   bits: 4/4
c ---[1435]---> Adder-cost: 16   maxlim: 8   bits: 4/4
c ---[1434]---> Adder-cost: 16   maxlim: 8   bits: 4/4
c ---[1433]---> Adder-cost: 16   maxlim: 8   bits: 4/4
c ---[1432]---> Adder-cost: 16   maxlim: 8   bits: 4/4
c ---[1431]---> Adder-cost: 16   maxlim: 8   bits: 4/4
c ---[1430]---> Adder-cost: 16   maxlim: 8   bits: 4/4
c ---[1429]---> Adder-cost: 16   maxlim: 8   bits: 4/4
c ---[1428]---> Adder-cost: 16   maxlim: 8   bits: 4/4
c ---[1427]---> Adder-cost: 16   maxlim: 8   bits: 4/4
c ---[1426]---> Adder-cost: 16   maxlim: 8   bits: 4/4
c ---[1425]---> Adder-cost: 16   maxlim: 8   bits: 4/4
c ---[1424]---> Adder-cost: 16   maxlim: 8   bits: 4/4
c ---[1423]---> Adder-cost: 16   maxlim: 8   bits: 4/4
c ---[1422]---> Adder-cost: 16   maxlim: 8   bits: 4/4
c ---[1421]---> Adder-cost: 16   maxlim: 8   bits: 4/4
c ---[1420]---> Adder-cost: 16   maxlim: 8   bits: 4/4
c ---[1419]---> Adder-cost: 20   maxlim: 8   bits: 4/4
c ---[1418]---> Adder-cost: 20   maxlim: 8   bits: 4/4
c ---[1417]---> Adder-cost: 20   maxlim: 8   bits: 4/4
c ---[1416]---> Adder-cost: 20   maxlim: 8   bits: 4/4
c ---[1415]---> Adder-cost: 20   maxlim: 8   bits: 4/4
c ---[1414]---> Adder-cost: 20   maxlim: 8   bits: 4/4
c ---[1413]---> Adder-cost: 20   maxlim: 8   bits: 4/4
c ---[1412]---> Adder-cost: 20   maxlim: 8   bits: 4/4
c ---[1411]---> Adder-cost: 20   maxlim: 8   bits: 4/4
c ---[1410]---> Adder-cost: 20   maxlim: 8   bits: 4/4
c ---[1409]---> Adder-cost: 20   maxlim: 8   bits: 4/4
c ---[1408]---> Adder-cost: 20   maxlim: 8   bits: 4/4
c ---[1407]---> Adder-cost: 20   maxlim: 8   bits: 4/4
c ---[1406]---> Adder-cost: 20   maxlim: 8   bits: 4/4
c ---[1405]---> Adder-cost: 20   maxlim: 8   bits: 4/4
c ---[1404]---> Adder-cost: 20   maxlim: 8   bits: 4/4
c ---[1403]---> Adder-cost: 20   maxlim: 8   bits: 4/4
c ---[1402]---> Adder-cost: 20   maxlim: 8   bits: 4/4
c ---[1401]---> Adder-cost: 20   maxlim: 8   bits: 4/4
c ---[1400]---> Adder-cost: 20   maxlim: 8   bits: 4/4
c ---[1399]---> Adder-cost: 20   maxlim: 8   bits: 4/4
c ---[1398]---> Adder-cost: 20   maxlim: 8   bits: 4/4
c ---[1397]---> Adder-cost: 20   maxlim: 8   bits: 4/4
c ---[1396]---> Adder-cost: 20   maxlim: 8   bits: 4/4
c ---[1395]---> Adder-cost: 20   maxlim: 8   bits: 4/4
c ---[1394]---> Adder-cost: 20   maxlim: 8   bits: 4/4
c ---[1393]---> Adder-cost: 20   maxlim: 8   bits: 4/4
c ---[1392]---> Adder-cost: 20   maxlim: 8   bits: 4/4
c ---[1391]---> Adder-cost: 20   maxlim: 10   bits: 4/4
c ---[1390]---> Adder-cost: 20   maxlim: 10   bits: 4/4
c ---[1389]---> Adder-cost: 20   maxlim: 10   bits: 4/4
c ---[1388]---> Adder-cost: 20   maxlim: 10   bits: 4/4
c ---[1387]---> Adder-cost: 20   maxlim: 10   bits: 4/4
c ---[1386]---> Adder-cost: 20   maxlim: 10   bits: 4/4
c ---[1385]---> Adder-cost: 20   maxlim: 10   bits: 4/4
c ---[1384]---> Adder-cost: 20   maxlim: 10   bits: 4/4
c ---[1383]---> Adder-cost: 20   maxlim: 10   bits: 4/4
c ---[1382]---> Adder-cost: 20   maxlim: 10   bits: 4/4
c ---[1381]---> Adder-cost: 20   maxlim: 10   bits: 4/4
c ---[1380]---> Adder-cost: 20   maxlim: 10   bits: 4/4
c ---[1379]---> Adder-cost: 20   maxlim: 10   bits: 4/4
c ---[1378]---> Adder-cost: 20   maxlim: 10   bits: 4/4
c ---[1377]---> Adder-cost: 20   maxlim: 10   bits: 4/4
c ---[1376]---> Adder-cost: 20   maxlim: 10   bits: 4/4
c ---[1375]---> Adder-cost: 20   maxlim: 10   bits: 4/4
c ---[1374]---> Adder-cost: 20   maxlim: 10   bits: 4/4
c ---[1373]---> Adder-cost: 20   maxlim: 10   bits: 4/4
c ---[1372]---> Adder-cost: 20   maxlim: 10   bits: 4/4
c ---[1371]---> Adder-cost: 20   maxlim: 10   bits: 4/4
c ---[1370]---> Adder-cost: 20   maxlim: 10   bits: 4/4
c ---[1369]---> Adder-cost: 20   maxlim: 10   bits: 4/4
c ---[1368]---> Adder-cost: 20   maxlim: 10   bits: 4/4
c ---[1367]---> Adder-cost: 20   maxlim: 10   bits: 4/4
c ---[1366]---> Adder-cost: 20   maxlim: 10   bits: 4/4
c ---[1365]---> Adder-cost: 20   maxlim: 10   bits: 4/4
c ---[1364]---> Adder-cost: 20   maxlim: 10   bits: 4/4
c ---[1363]---> Adder-cost: 22   maxlim: 11   bits: 4/4
c ---[1362]---> Adder-cost: 22   maxlim: 11   bits: 4/4
c ---[1361]---> Adder-cost: 22   maxlim: 11   bits: 4/4
c ---[1360]---> Adder-cost: 22   maxlim: 11   bits: 4/4
c ---[1359]---> Adder-cost: 22   maxlim: 11   bits: 4/4
c ---[1358]---> Adder-cost: 22   maxlim: 11   bits: 4/4
c ---[1357]---> Adder-cost: 22   maxlim: 11   bits: 4/4
c ---[1356]---> Adder-cost: 22   maxlim: 11   bits: 4/4
c ---[1355]---> Adder-cost: 22   maxlim: 11   bits: 4/4
c ---[1354]---> Adder-cost: 22   maxlim: 11   bits: 4/4
c ---[1353]---> Adder-cost: 22   maxlim: 11   bits: 4/4
c ---[1352]---> Adder-cost: 22   maxlim: 11   bits: 4/4
c ---[1351]---> Adder-cost: 22   maxlim: 11   bits: 4/4
c ---[1350]---> Adder-cost: 22   maxlim: 11   bits: 4/4
c ---[1349]---> Adder-cost: 22   maxlim: 11   bits: 4/4
c ---[1348]---> Adder-cost: 22   maxlim: 11   bits: 4/4
c ---[1347]---> Adder-cost: 22   maxlim: 11   bits: 4/4
c ---[1346]---> Adder-cost: 22   maxlim: 11   bits: 4/4
c ---[1345]---> Adder-cost: 22   maxlim: 11   bits: 4/4
c ---[1344]---> Adder-cost: 22   maxlim: 11   bits: 4/4
c ---[1343]---> Adder-cost: 22   maxlim: 11   bits: 4/4
c ---[1342]---> Adder-cost: 22   maxlim: 11   bits: 4/4
c ---[1341]---> Adder-cost: 22   maxlim: 11   bits: 4/4
c ---[1340]---> Adder-cost: 22   maxlim: 11   bits: 4/4
c ---[1339]---> Adder-cost: 22   maxlim: 11   bits: 4/4
c ---[1338]---> Adder-cost: 22   maxlim: 11   bits: 4/4
c ---[1337]---> Adder-cost: 22   maxlim: 11   bits: 4/4
c ---[1336]---> Adder-cost: 22   maxlim: 11   bits: 4/4
c ---[1335]---> Adder-cost: 30   maxlim: 13   bits: 5/4
c ---[1334]---> Adder-cost: 30   maxlim: 13   bits: 5/4
c ---[1333]---> Adder-cost: 30   maxlim: 13   bits: 5/4
c ---[1332]---> Adder-cost: 30   maxlim: 13   bits: 5/4
c ---[1331]---> Adder-cost: 30   maxlim: 13   bits: 5/4
c ---[1330]---> Adder-cost: 30   maxlim: 13   bits: 5/4
c ---[1329]---> Adder-cost: 30   maxlim: 13   bits: 5/4
c ---[1328]---> Adder-cost: 30   maxlim: 13   bits: 5/4
c ---[1327]---> Adder-cost: 30   maxlim: 13   bits: 5/4
c ---[1326]---> Adder-cost: 30   maxlim: 13   bits: 5/4
c ---[1325]---> Adder-cost: 30   maxlim: 13   bits: 5/4
c ---[1324]---> Adder-cost: 30   maxlim: 13   bits: 5/4
c ---[1323]---> Adder-cost: 30   maxlim: 13   bits: 5/4
c ---[1322]---> Adder-cost: 30   maxlim: 13   bits: 5/4
c ---[1321]---> Adder-cost: 30   maxlim: 13   bits: 5/4
c ---[1320]---> Adder-cost: 30   maxlim: 13   bits: 5/4
c ---[1319]---> Adder-cost: 30   maxlim: 13   bits: 5/4
c ---[1318]---> Adder-cost: 30   maxlim: 13   bits: 5/4
c ---[1317]---> Adder-cost: 30   maxlim: 13   bits: 5/4
c ---[1316]---> Adder-cost: 30   maxlim: 13   bits: 5/4
c ---[1315]---> Adder-cost: 30   maxlim: 13   bits: 5/4
c ---[1314]---> Adder-cost: 30   maxlim: 13   bits: 5/4
c ---[1313]---> Adder-cost: 30   maxlim: 13   bits: 5/4
c ---[1312]---> Adder-cost: 30   maxlim: 13   bits: 5/4
c ---[1311]---> Adder-cost: 30   maxlim: 13   bits: 5/4
c ---[1310]---> Adder-cost: 30   maxlim: 13   bits: 5/4
c ---[1309]---> Adder-cost: 30   maxlim: 13   bits: 5/4
c ---[1308]---> Adder-cost: 30   maxlim: 13   bits: 5/4
c ---[1307]---> Adder-cost: 36   maxlim: 16   bits: 5/5
c ---[1306]---> Adder-cost: 36   maxlim: 16   bits: 5/5
c ---[1305]---> Adder-cost: 36   maxlim: 16   bits: 5/5
c ---[1304]---> Adder-cost: 36   maxlim: 16   bits: 5/5
c ---[1303]---> Adder-cost: 36   maxlim: 16   bits: 5/5
c ---[1302]---> Adder-cost: 36   maxlim: 16   bits: 5/5
c ---[1301]---> Adder-cost: 36   maxlim: 16   bits: 5/5
c ---[1300]---> Adder-cost: 36   maxlim: 16   bits: 5/5
c ---[1299]---> Adder-cost: 36   maxlim: 16   bits: 5/5
c ---[1298]---> Adder-cost: 36   maxlim: 16   bits: 5/5
c ---[1297]---> Adder-cost: 36   maxlim: 16   bits: 5/5
c ---[1296]---> Adder-cost: 36   maxlim: 16   bits: 5/5
c ---[1295]---> Adder-cost: 36   maxlim: 16   bits: 5/5
c ---[1294]---> Adder-cost: 36   maxlim: 16   bits: 5/5
c ---[1293]---> Adder-cost: 36   maxlim: 16   bits: 5/5
c ---[1292]---> Adder-cost: 36   maxlim: 16   bits: 5/5
c ---[1291]---> Adder-cost: 36   maxlim: 16   bits: 5/5
c ---[1290]---> Adder-cost: 36   maxlim: 16   bits: 5/5
c ---[1289]---> Adder-cost: 36   maxlim: 16   bits: 5/5
c ---[1288]---> Adder-cost: 36   maxlim: 16   bits: 5/5
c ---[1287]---> Adder-cost: 36   maxlim: 16   bits: 5/5
c ---[1286]---> Adder-cost: 36   maxlim: 16   bits: 5/5
c ---[1285]---> Adder-cost: 36   maxlim: 16   bits: 5/5
c ---[1284]---> Adder-cost: 36   maxlim: 16   bits: 5/5
c ---[1283]---> Adder-cost: 36   maxlim: 16   bits: 5/5
c ---[1282]---> Adder-cost: 36   maxlim: 16   bits: 5/5
c ---[1281]---> Adder-cost: 36   maxlim: 16   bits: 5/5
c ---[1280]---> Adder-cost: 36   maxlim: 16   bits: 5/5
c ---[1278]---> Adder-cost: 50   maxlim: 26   bits: 5/5
c ---[1276]---> Adder-cost: 50   maxlim: 26   bits: 5/5
c ---[1274]---> Adder-cost: 50   maxlim: 26   bits: 5/5
c ---[1272]---> Adder-cost: 50   maxlim: 26   bits: 5/5
c ---[1270]---> Adder-cost: 50   maxlim: 26   bits: 5/5
c ---[1268]---> Adder-cost: 50   maxlim: 26   bits: 5/5
c ---[1267]---> Adder-cost: 50   maxlim: 26   bits: 5/5
c ---[1264]---> Adder-cost: 50   maxlim: 26   bits: 5/5
c ---[1262]---> Adder-cost: 50   maxlim: 26   bits: 5/5
c ---[1260]---> Adder-cost: 50   maxlim: 26   bits: 5/5
c ---[1258]---> Adder-cost: 50   maxlim: 26   bits: 5/5
c ---[1256]---> Adder-cost: 50   maxlim: 26   bits: 5/5
c ---[1254]---> Adder-cost: 50   maxlim: 26   bits: 5/5
c ---[1253]---> Adder-cost: 50   maxlim: 26   bits: 5/5
c ---[1250]---> Adder-cost: 50   maxlim: 26   bits: 5/5
c ---[1248]---> Adder-cost: 50   maxlim: 26   bits: 5/5
c ---[1246]---> Adder-cost: 50   maxlim: 26   bits: 5/5
c ---[1244]---> Adder-cost: 50   maxlim: 26   bits: 5/5
c ---[1242]---> Adder-cost: 50   maxlim: 26   bits: 5/5
c ---[1240]---> Adder-cost: 50   maxlim: 26   bits: 5/5
c ---[1238]---> Adder-cost: 50   maxlim: 26   bits: 5/5
c ---[1236]---> Adder-cost: 50   maxlim: 26   bits: 5/5
c ---[1234]---> Adder-cost: 50   maxlim: 26   bits: 5/5
c ---[1233]---> Adder-cost: 50   maxlim: 26   bits: 5/5
c ---[1231]---> Adder-cost: 50   maxlim: 26   bits: 5/5
c ---[1229]---> Adder-cost: 50   maxlim: 26   bits: 5/5
c ---[1227]---> Adder-cost: 50   maxlim: 26   bits: 5/5
c ---[1223]---> Adder-cost: 50   maxlim: 26   bits: 5/5
c ---[1221]---> Adder-cost: 50   maxlim: 26   bits: 5/5
c ---[1219]---> Adder-cost: 50   maxlim: 26   bits: 5/5
c ---[1217]---> Adder-cost: 50   maxlim: 26   bits: 5/5
c ---[1216]---> Adder-cost: 50   maxlim: 26   bits: 5/5
c ---[1213]---> Adder-cost: 50   maxlim: 26   bits: 5/5
c ---[1211]---> Adder-cost: 50   maxlim: 26   bits: 5/5
c ---[1209]---> Adder-cost: 50   maxlim: 26   bits: 5/5
c ---[1207]---> Adder-cost: 50   maxlim: 26   bits: 5/5
c ---[1205]---> Adder-cost: 50   maxlim: 26   bits: 5/5
c ---[1203]---> Adder-cost: 50   maxlim: 26   bits: 5/5
c ---[1201]---> Adder-cost: 50   maxlim: 26   bits: 5/5
c ---[1199]---> Adder-cost: 50   maxlim: 26   bits: 5/5
c ---[1197]---> Adder-cost: 50   maxlim: 26   bits: 5/5
c ---[1194]---> Adder-cost: 50   maxlim: 26   bits: 5/5
c ---[1192]---> Adder-cost: 50   maxlim: 26   bits: 5/5
c ---[1190]---> Adder-cost: 50   maxlim: 26   bits: 5/5
c ---[1188]---> Adder-cost: 50   maxlim: 26   bits: 5/5
c ---[1186]---> Adder-cost: 50   maxlim: 26   bits: 5/5
c ---[1184]---> Adder-cost: 50   maxlim: 26   bits: 5/5
c ---[1182]---> Adder-cost: 50   maxlim: 26   bits: 5/5
c ---[1180]---> Adder-cost: 50   maxlim: 26   bits: 5/5
c ---[1179]---> Adder-cost: 50   maxlim: 26   bits: 5/5
c ---[1176]---> Adder-cost: 50   maxlim: 26   bits: 5/5
c ---[1174]---> Adder-cost: 50   maxlim: 26   bits: 5/5
c ---[1172]---> Adder-cost: 50   maxlim: 26   bits: 5/5
c ---[1171]---> Adder-cost: 50   maxlim: 26   bits: 5/5
c ---[1170]---> Adder-cost: 50   maxlim: 26   bits: 5/5
c ---[1168]---> Adder-cost: 50   maxlim: 26   bits: 5/5
c ---[1166]---> Adder-cost: 50   maxlim: 26   bits: 5/5
c ---[1164]---> Adder-cost: 50   maxlim: 26   bits: 5/5
c ---[1162]---> Adder-cost: 50   maxlim: 26   bits: 5/5
c ---[1161]---> Adder-cost: 50   maxlim: 26   bits: 5/5
c ---[1159]---> Adder-cost: 50   maxlim: 26   bits: 5/5
c ---[1157]---> Adder-cost: 50   maxlim: 26   bits: 5/5
c ---[1155]---> Adder-cost: 50   maxlim: 26   bits: 5/5
c ---[1153]---> Adder-cost: 50   maxlim: 26   bits: 5/5
c ---[1151]---> Adder-cost: 50   maxlim: 26   bits: 5/5
c ---[1149]---> Adder-cost: 50   maxlim: 26   bits: 5/5
c ---[1147]---> Adder-cost: 50   maxlim: 26   bits: 5/5
c ---[1145]---> Adder-cost: 50   maxlim: 26   bits: 5/5
c ---[1141]---> Adder-cost: 50   maxlim: 26   bits: 5/5
c ---[1139]---> Adder-cost: 50   maxlim: 26   bits: 5/5
c ---[1137]---> Adder-cost: 50   maxlim: 26   bits: 5/5
c ---[1135]---> Adder-cost: 50   maxlim: 26   bits: 5/5
c ---[1133]---> Adder-cost: 50   maxlim: 26   bits: 5/5
c ---[1131]---> Adder-cost: 50   maxlim: 26   bits: 5/5
c ---[1129]---> Adder-cost: 50   maxlim: 26   bits: 5/5
c ---[1127]---> Adder-cost: 50   maxlim: 26   bits: 5/5
c ---[1125]---> Adder-cost: 50   maxlim: 26   bits: 5/5
c ---[1123]---> Adder-cost: 50   maxlim: 26   bits: 5/5
c ---[1121]---> Adder-cost: 50   maxlim: 26   bits: 5/5
c ---[1119]---> Adder-cost: 50   maxlim: 26   bits: 5/5
c ---[1117]---> Adder-cost: 50   maxlim: 26   bits: 5/5
c ---[1114]---> Adder-cost: 50   maxlim: 26   bits: 5/5
c ---[1112]---> Adder-cost: 50   maxlim: 26   bits: 5/5
c ---[1110]---> Adder-cost: 50   maxlim: 26   bits: 5/5
c ---[1108]---> Adder-cost: 50   maxlim: 26   bits: 5/5
c ---[1105]---> Adder-cost: 50   maxlim: 26   bits: 5/5
c ---[1103]---> Adder-cost: 50   maxlim: 26   bits: 5/5
c ---[1101]---> Adder-cost: 50   maxlim: 26   bits: 5/5
c ---[1099]---> Adder-cost: 50   maxlim: 26   bits: 5/5
c ---[1097]---> Adder-cost: 50   maxlim: 26   bits: 5/5
c ---[1095]---> Adder-cost: 50   maxlim: 26   bits: 5/5
c ---[1093]---> Adder-cost: 50   maxlim: 26   bits: 5/5
c ---[1091]---> Adder-cost: 50   maxlim: 26   bits: 5/5
c ---[1089]---> Adder-cost: 50   maxlim: 26   bits: 5/5
c ---[1087]---> Adder-cost: 50   maxlim: 26   bits: 5/5
c ---[1085]---> Adder-cost: 50   maxlim: 26   bits: 5/5
c ---[1083]---> Adder-cost: 50   maxlim: 26   bits: 5/5
c ---[1081]---> Adder-cost: 50   maxlim: 26   bits: 5/5
c ---[1079]---> Adder-cost: 50   maxlim: 26   bits: 5/5
c ---[1077]---> Adder-cost: 50   maxlim: 26   bits: 5/5
c ---[1075]---> Adder-cost: 50   maxlim: 26   bits: 5/5
c ---[1073]---> Adder-cost: 50   maxlim: 26   bits: 5/5
c ---[1071]---> Adder-cost: 50   maxlim: 26   bits: 5/5
c ---[1069]---> Adder-cost: 50   maxlim: 26   bits: 5/5
c ---[1067]---> Adder-cost: 50   maxlim: 26   bits: 5/5
c ---[1065]---> Adder-cost: 50   maxlim: 26   bits: 5/5
c ---[1063]---> Adder-cost: 50   maxlim: 26   bits: 5/5
c ---[1061]---> Adder-cost: 50   maxlim: 26   bits: 5/5
c ---[1059]---> Adder-cost: 50   maxlim: 26   bits: 5/5
c ---[1057]---> Adder-cost: 50   maxlim: 26   bits: 5/5
c ---[1055]---> Adder-cost: 50   maxlim: 26   bits: 5/5
c ---[1053]---> Adder-cost: 50   maxlim: 26   bits: 5/5
c ---[1052]---> Adder-cost: 50   maxlim: 26   bits: 5/5
c ---[1049]---> Adder-cost: 50   maxlim: 26   bits: 5/5
c ---[1047]---> Adder-cost: 50   maxlim: 26   bits: 5/5
c ---[1045]---> Adder-cost: 50   maxlim: 26   bits: 5/5
c ---[1043]---> Adder-cost: 50   maxlim: 26   bits: 5/5
c ---[1041]---> Adder-cost: 50   maxlim: 26   bits: 5/5
c ---[1039]---> Adder-cost: 50   maxlim: 26   bits: 5/5
c ---[1037]---> Adder-cost: 50   maxlim: 26   bits: 5/5
c ---[1035]---> Adder-cost: 50   maxlim: 26   bits: 5/5
c ---[1034]---> Adder-cost: 50   maxlim: 26   bits: 5/5
c ---[1031]---> Adder-cost: 50   maxlim: 26   bits: 5/5
c ---[1029]---> Adder-cost: 50   maxlim: 26   bits: 5/5
c ---[1027]---> Adder-cost: 50   maxlim: 26   bits: 5/5
c ---[1025]---> Adder-cost: 50   maxlim: 26   bits: 5/5
c ---[1023]---> Adder-cost: 50   maxlim: 26   bits: 5/5
c ---[1021]---> Adder-cost: 50   maxlim: 26   bits: 5/5
c ---[1019]---> Adder-cost: 50   maxlim: 26   bits: 5/5
c ---[1017]---> Adder-cost: 50   maxlim: 26   bits: 5/5
c ---[1016]---> Adder-cost: 50   maxlim: 26   bits: 5/5
c ---[1014]---> Adder-cost: 50   maxlim: 26   bits: 5/5
c ---[1012]---> Adder-cost: 50   maxlim: 26   bits: 5/5
c ---[1010]---> Adder-cost: 50   maxlim: 26   bits: 5/5
c ---[1008]---> Adder-cost: 50   maxlim: 26   bits: 5/5
c ---[1006]---> Adder-cost: 50   maxlim: 26   bits: 5/5
c ---[1004]---> Adder-cost: 50   maxlim: 26   bits: 5/5
c ---[1002]---> Adder-cost: 50   maxlim: 26   bits: 5/5
c ---[1000]---> Adder-cost: 50   maxlim: 26   bits: 5/5
c ---[ 998]---> Adder-cost: 50   maxlim: 26   bits: 5/5
c ---[ 995]---> Adder-cost: 50   maxlim: 26   bits: 5/5
c ---[ 993]---> Adder-cost: 50   maxlim: 26   bits: 5/5
c ---[ 991]---> Adder-cost: 50   maxlim: 26   bits: 5/5
c ---[ 989]---> Adder-cost: 50   maxlim: 26   bits: 5/5
c ---[ 987]---> Adder-cost: 50   maxlim: 26   bits: 5/5
c ---[ 985]---> Adder-cost: 50   maxlim: 26   bits: 5/5
c ---[ 983]---> Adder-cost: 50   maxlim: 26   bits: 5/5
c ---[ 981]---> Adder-cost: 50   maxlim: 26   bits: 5/5
c ---[ 979]---> Adder-cost: 50   maxlim: 26   bits: 5/5
c ---[ 976]---> Adder-cost: 50   maxlim: 26   bits: 5/5
c ---[ 974]---> Adder-cost: 50   maxlim: 26   bits: 5/5
c ---[ 972]---> Adder-cost: 50   maxlim: 26   bits: 5/5
c ---[ 970]---> Adder-cost: 50   maxlim: 26   bits: 5/5
c ---[ 968]---> Adder-cost: 50   maxlim: 26   bits: 5/5
c ---[ 966]---> Adder-cost: 50   maxlim: 26   bits: 5/5
c ---[ 964]---> Adder-cost: 50   maxlim: 26   bits: 5/5
c ---[ 962]---> Adder-cost: 50   maxlim: 26   bits: 5/5
c ---[ 961]---> Adder-cost: 50   maxlim: 26   bits: 5/5
c ---[ 959]---> Adder-cost: 50   maxlim: 26   bits: 5/5
c ---[ 957]---> Adder-cost: 50   maxlim: 26   bits: 5/5
c ---[ 955]---> Adder-cost: 50   maxlim: 26   bits: 5/5
c ---[ 953]---> Adder-cost: 50   maxlim: 26   bits: 5/5
c ---[ 951]---> Adder-cost: 50   maxlim: 26   bits: 5/5
c ---[ 948]---> Adder-cost: 50   maxlim: 26   bits: 5/5
c ---[ 946]---> Adder-cost: 50   maxlim: 26   bits: 5/5
c ---[ 944]---> Adder-cost: 50   maxlim: 26   bits: 5/5
c ---[ 942]---> Adder-cost: 50   maxlim: 26   bits: 5/5
c ---[ 939]---> Adder-cost: 50   maxlim: 26   bits: 5/5
c ---[ 937]---> Adder-cost: 50   maxlim: 26   bits: 5/5
c ---[ 935]---> Adder-cost: 50   maxlim: 26   bits: 5/5
c ---[ 933]---> Adder-cost: 50   maxlim: 26   bits: 5/5
c ---[ 931]---> Adder-cost: 50   maxlim: 26   bits: 5/5
c ---[ 929]---> Adder-cost: 50   maxlim: 26   bits: 5/5
c ---[ 927]---> Adder-cost: 50   maxlim: 26   bits: 5/5
c ---[ 925]---> Adder-cost: 50   maxlim: 26   bits: 5/5
c ---[ 924]---> Adder-cost: 50   maxlim: 26   bits: 5/5
c ---[ 923]---> Adder-cost: 50   maxlim: 26   bits: 5/5
c ---[ 921]---> Adder-cost: 50   maxlim: 26   bits: 5/5
c ---[ 919]---> Adder-cost: 50   maxlim: 26   bits: 5/5
c ---[ 917]---> Adder-cost: 50   maxlim: 26   bits: 5/5
c ---[ 915]---> Adder-cost: 50   maxlim: 26   bits: 5/5
c ---[ 913]---> Adder-cost: 50   maxlim: 26   bits: 5/5
c ---[ 911]---> Adder-cost: 50   maxlim: 26   bits: 5/5
c ---[ 909]---> Adder-cost: 50   maxlim: 26   bits: 5/5
c ---[ 907]---> Adder-cost: 50   maxlim: 26   bits: 5/5
c ---[ 905]---> Adder-cost: 50   maxlim: 26   bits: 5/5
c ---[ 903]---> Adder-cost: 50   maxlim: 26   bits: 5/5
c ---[ 901]---> Adder-cost: 50   maxlim: 26   bits: 5/5
c ---[ 899]---> Adder-cost: 50   maxlim: 26   bits: 5/5
c ---[ 897]---> Adder-cost: 50   maxlim: 26   bits: 5/5
c ---[ 896]---> Adder-cost: 50   maxlim: 26   bits: 5/5
c ---[ 893]---> Adder-cost: 50   maxlim: 26   bits: 5/5
c ---[ 891]---> Adder-cost: 50   maxlim: 26   bits: 5/5
c ---[ 889]---> Adder-cost: 50   maxlim: 26   bits: 5/5
c ---[ 887]---> Adder-cost: 50   maxlim: 26   bits: 5/5
c ---[ 885]---> Adder-cost: 50   maxlim: 26   bits: 5/5
c ---[ 883]---> Adder-cost: 50   maxlim: 26   bits: 5/5
c ---[ 881]---> Adder-cost: 50   maxlim: 26   bits: 5/5
c ---[ 879]---> Adder-cost: 50   maxlim: 26   bits: 5/5
c ---[ 877]---> Adder-cost: 50   maxlim: 26   bits: 5/5
c ---[ 875]---> Adder-cost: 50   maxlim: 26   bits: 5/5
c ---[ 873]---> Adder-cost: 50   maxlim: 26   bits: 5/5
c ---[ 871]---> Adder-cost: 50   maxlim: 26   bits: 5/5
c ---[ 869]---> Adder-cost: 50   maxlim: 26   bits: 5/5
c ---[ 867]---> Adder-cost: 50   maxlim: 26   bits: 5/5
c ---[ 865]---> Adder-cost: 50   maxlim: 26   bits: 5/5
c ---[ 863]---> Adder-cost: 50   maxlim: 26   bits: 5/5
c ---[ 861]---> Adder-cost: 50   maxlim: 26   bits: 5/5
c ---[ 859]---> Adder-cost: 50   maxlim: 26   bits: 5/5
c ---[ 857]---> Adder-cost: 50   maxlim: 26   bits: 5/5
c ---[ 855]---> Adder-cost: 50   maxlim: 26   bits: 5/5
c ---[ 853]---> Adder-cost: 50   maxlim: 26   bits: 5/5
c ---[ 851]---> Adder-cost: 50   maxlim: 26   bits: 5/5
c ---[ 850]---> Adder-cost: 50   maxlim: 26   bits: 5/5
c ---[ 848]---> Adder-cost: 50   maxlim: 26   bits: 5/5
c ---[ 846]---> Adder-cost: 50   maxlim: 26   bits: 5/5
c ---[ 844]---> Adder-cost: 50   maxlim: 26   bits: 5/5
c ---[ 842]---> Adder-cost: 50   maxlim: 26   bits: 5/5
c ---[ 841]---> Adder-cost: 50   maxlim: 26   bits: 5/5
c ---[ 839]---> Adder-cost: 50   maxlim: 26   bits: 5/5
c ---[ 837]---> Adder-cost: 50   maxlim: 26   bits: 5/5
c ---[ 835]---> Adder-cost: 50   maxlim: 26   bits: 5/5
c ---[ 833]---> Adder-cost: 50   maxlim: 26   bits: 5/5
c ---[ 830]---> Adder-cost: 50   maxlim: 26   bits: 5/5
c ---[ 828]---> Adder-cost: 50   maxlim: 26   bits: 5/5
c ---[ 826]---> Adder-cost: 50   maxlim: 26   bits: 5/5
c ---[ 824]---> Adder-cost: 50   maxlim: 26   bits: 5/5
c ---[ 822]---> Adder-cost: 50   maxlim: 26   bits: 5/5
c ---[ 820]---> Adder-cost: 50   maxlim: 26   bits: 5/5
c ---[ 818]---> Adder-cost: 50   maxlim: 26   bits: 5/5
c ---[ 816]---> Adder-cost: 50   maxlim: 26   bits: 5/5
c ---[ 814]---> Adder-cost: 50   maxlim: 26   bits: 5/5
c ---[ 813]---> Adder-cost: 50   maxlim: 26   bits: 5/5
c ---[ 811]---> Adder-cost: 50   maxlim: 26   bits: 5/5
c ---[ 809]---> Adder-cost: 50   maxlim: 26   bits: 5/5
c ---[ 807]---> Adder-cost: 50   maxlim: 26   bits: 5/5
c ---[ 805]---> Adder-cost: 50   maxlim: 26   bits: 5/5
c ---[ 803]---> Adder-cost: 50   maxlim: 26   bits: 5/5
c ---[ 801]---> Adder-cost: 50   maxlim: 26   bits: 5/5
c ---[ 799]---> Adder-cost: 50   maxlim: 26   bits: 5/5
c ---[ 797]---> Adder-cost: 50   maxlim: 26   bits: 5/5
c ---[ 794]---> Adder-cost: 50   maxlim: 26   bits: 5/5
c ---[ 792]---> Adder-cost: 50   maxlim: 26   bits: 5/5
c ---[ 790]---> Adder-cost: 50   maxlim: 26   bits: 5/5
c ---[ 788]---> Adder-cost: 50   maxlim: 26   bits: 5/5
c ---[ 786]---> Adder-cost: 50   maxlim: 26   bits: 5/5
c ---[ 785]---> Adder-cost: 50   maxlim: 26   bits: 5/5
c ---[ 783]---> Adder-cost: 50   maxlim: 26   bits: 5/5
c ---[ 781]---> Adder-cost: 50   maxlim: 26   bits: 5/5
c ---[ 779]---> Adder-cost: 50   maxlim: 26   bits: 5/5
c ---[ 776]---> Adder-cost: 50   maxlim: 26   bits: 5/5
c ---[ 774]---> Adder-cost: 50   maxlim: 26   bits: 5/5
c ---[ 772]---> Adder-cost: 50   maxlim: 26   bits: 5/5
c ---[ 770]---> Adder-cost: 50   maxlim: 26   bits: 5/5
c ---[ 768]---> Adder-cost: 50   maxlim: 26   bits: 5/5
c ---[ 766]---> Adder-cost: 50   maxlim: 26   bits: 5/5
c ---[ 764]---> Adder-cost: 50   maxlim: 26   bits: 5/5
c ---[ 762]---> Adder-cost: 50   maxlim: 26   bits: 5/5
c ---[ 760]---> Adder-cost: 50   maxlim: 26   bits: 5/5
c ---[ 757]---> Adder-cost: 50   maxlim: 26   bits: 5/5
c ---[ 755]---> Adder-cost: 50   maxlim: 26   bits: 5/5
c ---[ 753]---> Adder-cost: 50   maxlim: 26   bits: 5/5
c ---[ 751]---> Adder-cost: 50   maxlim: 26   bits: 5/5
c ---[ 749]---> Adder-cost: 50   maxlim: 26   bits: 5/5
c ---[ 747]---> Adder-cost: 50   maxlim: 26   bits: 5/5
c ---[ 745]---> Adder-cost: 50   maxlim: 26   bits: 5/5
c ---[ 743]---> Adder-cost: 50   maxlim: 26   bits: 5/5
c ---[ 741]---> Adder-cost: 50   maxlim: 26   bits: 5/5
c ---[ 740]---> Adder-cost: 50   maxlim: 26   bits: 5/5
c ---[ 738]---> Adder-cost: 50   maxlim: 26   bits: 5/5
c ---[ 736]---> Adder-cost: 50   maxlim: 26   bits: 5/5
c ---[ 734]---> Adder-cost: 50   maxlim: 26   bits: 5/5
c ---[ 732]---> Adder-cost: 50   maxlim: 26   bits: 5/5
c ---[ 730]---> Adder-cost: 50   maxlim: 26   bits: 5/5
c ---[ 728]---> Adder-cost: 50   maxlim: 26   bits: 5/5
c ---[ 726]---> Adder-cost: 50   maxlim: 26   bits: 5/5
c ---[ 724]---> Adder-cost: 50   maxlim: 26   bits: 5/5
c ---[ 721]---> Adder-cost: 50   maxlim: 26   bits: 5/5
c ---[ 719]---> Adder-cost: 50   maxlim: 26   bits: 5/5
c ---[ 717]---> Adder-cost: 50   maxlim: 26   bits: 5/5
c ---[ 715]---> Adder-cost: 50   maxlim: 26   bits: 5/5
c ---[ 713]---> Adder-cost: 50   maxlim: 26   bits: 5/5
c ---[ 711]---> Adder-cost: 50   maxlim: 26   bits: 5/5
c ---[ 709]---> Adder-cost: 50   maxlim: 26   bits: 5/5
c ---[ 707]---> Adder-cost: 50   maxlim: 26   bits: 5/5
c ---[ 705]---> Adder-cost: 50   maxlim: 26   bits: 5/5
c ---[ 704]---> Adder-cost: 50   maxlim: 26   bits: 5/5
c ---[ 702]---> Adder-cost: 50   maxlim: 26   bits: 5/5
c ---[ 700]---> Adder-cost: 50   maxlim: 26   bits: 5/5
c ---[ 698]---> Adder-cost: 50   maxlim: 26   bits: 5/5
c ---[ 696]---> Adder-cost: 50   maxlim: 26   bits: 5/5
c ---[ 695]---> Adder-cost: 50   maxlim: 26   bits: 5/5
c ---[ 693]---> Adder-cost: 50   maxlim: 26   bits: 5/5
c ---[ 691]---> Adder-cost: 50   maxlim: 26   bits: 5/5
c ---[ 689]---> Adder-cost: 50   maxlim: 26   bits: 5/5
c ---[ 687]---> Adder-cost: 50   maxlim: 26   bits: 5/5
c ---[ 685]---> Adder-cost: 50   maxlim: 26   bits: 5/5
c ---[ 683]---> Adder-cost: 50   maxlim: 26   bits: 5/5
c ---[ 681]---> Adder-cost: 50   maxlim: 26   bits: 5/5
c ---[ 679]---> Adder-cost: 50   maxlim: 26   bits: 5/5
c ---[ 677]---> Adder-cost: 50   maxlim: 26   bits: 5/5
c ---[ 674]---> Adder-cost: 50   maxlim: 26   bits: 5/5
c ---[ 672]---> Adder-cost: 50   maxlim: 26   bits: 5/5
c ---[ 670]---> Adder-cost: 50   maxlim: 26   bits: 5/5
c ---[ 668]---> Adder-cost: 50   maxlim: 26   bits: 5/5
c ---[ 667]---> Adder-cost: 50   maxlim: 26   bits: 5/5
c ---[ 665]---> Adder-cost: 50   maxlim: 26   bits: 5/5
c ---[ 663]---> Adder-cost: 50   maxlim: 26   bits: 5/5
c ---[ 661]---> Adder-cost: 50   maxlim: 26   bits: 5/5
c ---[ 659]---> Adder-cost: 50   maxlim: 26   bits: 5/5
c ---[ 657]---> Adder-cost: 50   maxlim: 26   bits: 5/5
c ---[ 655]---> Adder-cost: 50   maxlim: 26   bits: 5/5
c ---[ 653]---> Adder-cost: 50   maxlim: 26   bits: 5/5
c ---[ 651]---> Adder-cost: 50   maxlim: 26   bits: 5/5
c ---[ 649]---> Adder-cost: 50   maxlim: 26   bits: 5/5
c ---[ 647]---> Adder-cost: 50   maxlim: 26   bits: 5/5
c ---[ 645]---> Adder-cost: 50   maxlim: 26   bits: 5/5
c ---[ 643]---> Adder-cost: 50   maxlim: 26   bits: 5/5
c ---[ 641]---> Adder-cost: 50   maxlim: 26   bits: 5/5
c ---[ 639]---> Adder-cost: 50   maxlim: 26   bits: 5/5
c ---[ 637]---> Adder-cost: 50   maxlim: 26   bits: 5/5
c ---[ 635]---> Adder-cost: 50   maxlim: 26   bits: 5/5
c ---[ 633]---> Adder-cost: 50   maxlim: 26   bits: 5/5
c ---[ 631]---> Adder-cost: 50   maxlim: 26   bits: 5/5
c ---[ 629]---> Adder-cost: 50   maxlim: 26   bits: 5/5
c ---[ 627]---> Adder-cost: 50   maxlim: 26   bits: 5/5
c ---[ 625]---> Adder-cost: 50   maxlim: 26   bits: 5/5
c ---[ 623]---> Adder-cost: 50   maxlim: 26   bits: 5/5
c ---[ 621]---> Adder-cost: 50   maxlim: 26   bits: 5/5
c ---[ 620]---> Adder-cost: 50   maxlim: 26   bits: 5/5
c ---[ 618]---> Adder-cost: 50   maxlim: 26   bits: 5/5
c ---[ 616]---> Adder-cost: 50   maxlim: 26   bits: 5/5
c ---[ 614]---> Adder-cost: 50   maxlim: 26   bits: 5/5
c ---[ 612]---> Adder-cost: 50   maxlim: 26   bits: 5/5
c ---[ 592]---> Adder-cost: 50   maxlim: 26   bits: 5/5
c ---[ 590]---> Adder-cost: 50   maxlim: 26   bits: 5/5
c ---[ 588]---> Adder-cost: 50   maxlim: 26   bits: 5/5
c ---[ 586]---> Adder-cost: 50   maxlim: 26   bits: 5/5
c ---[ 584]---> Adder-cost: 50   maxlim: 26   bits: 5/5
c ---[ 582]---> Adder-cost: 50   maxlim: 26   bits: 5/5
c ---[ 580]---> Adder-cost: 50   maxlim: 26   bits: 5/5
c ---[ 578]---> Adder-cost: 50   maxlim: 26   bits: 5/5
c ---[ 576]---> Adder-cost: 50   maxlim: 26   bits: 5/5
c ---[ 571]---> Adder-cost: 50   maxlim: 26   bits: 5/5
c ---[ 569]---> Adder-cost: 50   maxlim: 26   bits: 5/5
c ---[ 567]---> Adder-cost: 50   maxlim: 26   bits: 5/5
c ---[ 509]---> Adder-cost: 50   maxlim: 26   bits: 5/5
c ---[ 507]---> Adder-cost: 50   maxlim: 26   bits: 5/5
c ---[ 505]---> Adder-cost: 50   maxlim: 26   bits: 5/5
c ---[ 503]---> Adder-cost: 50   maxlim: 26   bits: 5/5
c ---[ 500]---> Adder-cost: 50   maxlim: 26   bits: 5/5
c ---[ 498]---> Adder-cost: 50   maxlim: 26   bits: 5/5
c ---[ 496]---> Adder-cost: 50   maxlim: 26   bits: 5/5
c ---[ 494]---> Adder-cost: 50   maxlim: 26   bits: 5/5
c ---[ 492]---> Adder-cost: 50   maxlim: 26   bits: 5/5
c ---[ 490]---> Adder-cost: 50   maxlim: 26   bits: 5/5
c ---[ 488]---> Adder-cost: 50   maxlim: 26   bits: 5/5
c ---[ 486]---> Adder-cost: 50   maxlim: 26   bits: 5/5
c ---[ 484]---> Adder-cost: 50   maxlim: 26   bits: 5/5
c ---[ 483]---> Adder-cost: 50   maxlim: 26   bits: 5/5
c ---[ 481]---> Adder-cost: 50   maxlim: 26   bits: 5/5
c ---[ 479]---> Adder-cost: 50   maxlim: 26   bits: 5/5
c ---[ 477]---> Adder-cost: 50   maxlim: 26   bits: 5/5
c ---[ 475]---> Adder-cost: 50   maxlim: 26   bits: 5/5
c ---[ 473]---> Adder-cost: 50   maxlim: 26   bits: 5/5
c ---[ 471]---> Adder-cost: 50   maxlim: 26   bits: 5/5
c ---[ 469]---> Adder-cost: 50   maxlim: 26   bits: 5/5
c ---[ 467]---> Adder-cost: 50   maxlim: 26   bits: 5/5
c ---[ 464]---> Adder-cost: 50   maxlim: 26   bits: 5/5
c ---[ 462]---> Adder-cost: 50   maxlim: 26   bits: 5/5
c ---[ 460]---> Adder-cost: 50   maxlim: 26   bits: 5/5
c ---[ 458]---> Adder-cost: 50   maxlim: 26   bits: 5/5
c ---[ 456]---> Adder-cost: 50   maxlim: 26   bits: 5/5
c ---[ 428]---> Adder-cost: 50   maxlim: 26   bits: 5/5
c ---[ 426]---> Adder-cost: 50   maxlim: 26   bits: 5/5
c ---[ 424]---> Adder-cost: 50   maxlim: 26   bits: 5/5
c ---[ 422]---> Adder-cost: 50   maxlim: 26   bits: 5/5
c ---[ 420]---> Adder-cost: 50   maxlim: 26   bits: 5/5
c ---[ 418]---> Adder-cost: 50   maxlim: 26   bits: 5/5
c ---[ 416]---> Adder-cost: 50   maxlim: 26   bits: 5/5
c ---[ 404]---> Adder-cost: 50   maxlim: 26   bits: 5/5
c ---[ 402]---> Adder-cost: 50   maxlim: 26   bits: 5/5
c ---[ 401]---> Adder-cost: 50   maxlim: 26   bits: 5/5
c ---[ 400]---> Adder-cost: 368   maxlim: 1611   bits: 12/11
c ---[ 399]---> Adder-cost: 368   maxlim: 1610   bits: 12/11
c ---[ 398]---> Adder-cost: 546   maxlim: 24195   bits: 16/15
c ---[ 397]---> Adder-cost: 546   maxlim: 24195   bits: 16/15
c ---[ 396]---> Adder-cost: 368   maxlim: 1611   bits: 12/11
c ---[ 395]---> Adder-cost: 368   maxlim: 1612   bits: 12/11
c ---[ 394]---> Adder-cost: 368   maxlim: 1611   bits: 12/11
c ---[ 393]---> Adder-cost: 368   maxlim: 1611   bits: 12/11
c ---[ 392]---> Adder-cost: 368   maxlim: 1610   bits: 12/11
c ---[ 391]---> Adder-cost: 368   maxlim: 1611   bits: 12/11
c ---[ 390]---> Adder-cost: 368   maxlim: 1610   bits: 12/11
c ---[ 389]---> Adder-cost: 368   maxlim: 1614   bits: 12/11
c ---[ 388]---> Adder-cost: 368   maxlim: 1612   bits: 12/11
c ---[ 387]---> Adder-cost: 368   maxlim: 1612   bits: 12/11
c ---[ 386]---> Adder-cost: 368   maxlim: 1612   bits: 12/11
c ---[ 385]---> Adder-cost: 368   maxlim: 1610   bits: 12/11
c ---[ 384]---> Adder-cost: 368   maxlim: 1611   bits: 12/11
c ---[ 383]---> Adder-cost: 368   maxlim: 1611   bits: 12/11
c ---[ 382]---> Adder-cost: 368   maxlim: 1611   bits: 12/11
c ---[ 381]---> Adder-cost: 368   maxlim: 1613   bits: 12/11
c ---[ 380]---> Adder-cost: 368   maxlim: 1611   bits: 12/11
c ---[ 379]---> Adder-cost: 368   maxlim: 1611   bits: 12/11
c ---[ 378]---> Adder-cost: 368   maxlim: 1611   bits: 12/11
c ---[ 377]---> Adder-cost: 368   maxlim: 1612   bits: 12/11
c ---[ 376]---> Adder-cost: 368   maxlim: 1611   bits: 12/11
c ---[ 375]---> Adder-cost: 368   maxlim: 1610   bits: 12/11
c ---[ 374]---> Adder-cost: 368   maxlim: 1612   bits: 12/11
c ---[ 373]---> Adder-cost: 368   maxlim: 1611   bits: 12/11
c ---[ 372]---> Adder-cost: 368   maxlim: 1610   bits: 12/11
c ---[ 371]---> Adder-cost: 368   maxlim: 1612   bits: 12/11
c ---[ 370]---> Adder-cost: 368   maxlim: 1611   bits: 12/11
c ---[ 369]---> Adder-cost: 368   maxlim: 1613   bits: 12/11
c ---[ 368]---> Adder-cost: 368   maxlim: 1611   bits: 12/11
c ---[ 367]---> Adder-cost: 368   maxlim: 1613   bits: 12/11
c ---[ 366]---> Adder-cost: 368   maxlim: 1611   bits: 12/11
c ---[ 365]---> Adder-cost: 368   maxlim: 1612   bits: 12/11
c ---[ 364]---> Adder-cost: 368   maxlim: 1611   bits: 12/11
c ---[ 363]---> Adder-cost: 368   maxlim: 1613   bits: 12/11
c ---[ 362]---> Adder-cost: 368   maxlim: 1611   bits: 12/11
c ---[ 361]---> Adder-cost: 552   maxlim: 24196   bits: 16/15
c ---[ 360]---> Adder-cost: 552   maxlim: 24211   bits: 16/15
c ---[ 359]---> Adder-cost: 368   maxlim: 1611   bits: 12/11
c ---[ 358]---> Adder-cost: 368   maxlim: 1612   bits: 12/11
c ---[ 357]---> Adder-cost: 368   maxlim: 1611   bits: 12/11
c ---[ 356]---> Adder-cost: 368   maxlim: 1612   bits: 12/11
c ---[ 355]---> Adder-cost: 368   maxlim: 1612   bits: 12/11
c ---[ 354]---> Adder-cost: 368   maxlim: 1612   bits: 12/11
c ---[ 353]---> Adder-cost: 368   maxlim: 1612   bits: 12/11
c ---[ 352]---> Adder-cost: 368   maxlim: 1611   bits: 12/11
c ---[ 351]---> Adder-cost: 368   maxlim: 1611   bits: 12/11
c ---[ 350]---> Adder-cost: 368   maxlim: 1611   bits: 12/11
c ---[ 349]---> Adder-cost: 368   maxlim: 1615   bits: 12/11
c ---[ 348]---> Adder-cost: 368   maxlim: 1611   bits: 12/11
c ---[ 347]---> Adder-cost: 368   maxlim: 1611   bits: 12/11
c ---[ 346]---> Adder-cost: 368   maxlim: 1610   bits: 12/11
c ---[ 345]---> Adder-cost: 368   maxlim: 1614   bits: 12/11
c ---[ 344]---> Adder-cost: 368   maxlim: 1611   bits: 12/11
c ---[ 343]---> Adder-cost: 368   maxlim: 1610   bits: 12/11
c ---[ 342]---> Adder-cost: 368   maxlim: 1612   bits: 12/11
c ---[ 341]---> Adder-cost: 368   maxlim: 1611   bits: 12/11
c ---[ 340]---> Adder-cost: 368   maxlim: 1614   bits: 12/11
c ---[ 339]---> Adder-cost: 368   maxlim: 1611   bits: 12/11
c ---[ 338]---> Adder-cost: 368   maxlim: 1610   bits: 12/11
c ---[ 337]---> Adder-cost: 368   maxlim: 1612   bits: 12/11
c ---[ 336]---> Adder-cost: 368   maxlim: 1611   bits: 12/11
c ---[ 335]---> Adder-cost: 368   maxlim: 1611   bits: 12/11
c ---[ 334]---> Adder-cost: 368   maxlim: 1610   bits: 12/11
c ---[ 333]---> Adder-cost: 552   maxlim: 24190   bits: 16/15
c ---[ 332]---> Adder-cost: 552   maxlim: 24205   bits: 16/15
c ---[ 331]---> Adder-cost: 552   maxlim: 24190   bits: 16/15
c ---[ 330]---> Adder-cost: 368   maxlim: 1611   bits: 12/11
c ---[ 329]---> Adder-cost: 368   maxlim: 1610   bits: 12/11
c ---[ 328]---> Adder-cost: 368   maxlim: 1613   bits: 12/11
c ---[ 327]---> Adder-cost: 552   maxlim: 24190   bits: 16/15
c ---[ 326]---> Adder-cost: 552   maxlim: 24205   bits: 16/15
c ---[ 325]---> Adder-cost: 552   maxlim: 24190   bits: 16/15
c ---[ 324]---> Adder-cost: 368   maxlim: 1611   bits: 12/11
c ---[ 323]---> Adder-cost: 368   maxlim: 1611   bits: 12/11
c ---[ 322]---> Adder-cost: 368   maxlim: 1612   bits: 12/11
c ---[ 321]---> Adder-cost: 368   maxlim: 1611   bits: 12/11
c ---[ 320]---> Adder-cost: 368   maxlim: 1611   bits: 12/11
c ---[ 319]---> Adder-cost: 368   maxlim: 1612   bits: 12/11
c ---[ 318]---> Adder-cost: 368   maxlim: 1611   bits: 12/11
c ---[ 317]---> Adder-cost: 368   maxlim: 1612   bits: 12/11
c ---[ 316]---> Adder-cost: 368   maxlim: 1613   bits: 12/11
c ---[ 315]---> Adder-cost: 368   maxlim: 1611   bits: 12/11
c ---[ 314]---> Adder-cost: 368   maxlim: 1612   bits: 12/11
c ---[ 313]---> Adder-cost: 368   maxlim: 1614   bits: 12/11
c ---[ 312]---> Adder-cost: 368   maxlim: 1610   bits: 12/11
c ---[ 311]---> Adder-cost: 368   maxlim: 1611   bits: 12/11
c ---[ 310]---> Adder-cost: 368   maxlim: 1611   bits: 12/11
c ---[ 309]---> Adder-cost: 368   maxlim: 1611   bits: 12/11
c ---[ 308]---> Adder-cost: 368   maxlim: 1610   bits: 12/11
c ---[ 307]---> Adder-cost: 368   maxlim: 1611   bits: 12/11
c ---[ 306]---> Adder-cost: 368   maxlim: 1612   bits: 12/11
c ---[ 305]---> Adder-cost: 368   maxlim: 1613   bits: 12/11
c ---[ 304]---> Adder-cost: 368   maxlim: 1614   bits: 12/11
c ---[ 303]---> Adder-cost: 368   maxlim: 1611   bits: 12/11
c ---[ 302]---> Adder-cost: 368   maxlim: 1611   bits: 12/11
c ---[ 301]---> Adder-cost: 368   maxlim: 1610   bits: 12/11
c ---[ 300]---> Adder-cost: 368   maxlim: 1611   bits: 12/11
c ---[ 299]---> Adder-cost: 368   maxlim: 1610   bits: 12/11
c ---[ 298]---> Adder-cost: 368   maxlim: 1610   bits: 12/11
c ---[ 297]---> Adder-cost: 368   maxlim: 1611   bits: 12/11
c ---[ 296]---> Adder-cost: 448   maxlim: 8068   bits: 14/13
c ---[ 295]---> Adder-cost: 448   maxlim: 8063   bits: 14/13
c ---[ 294]---> Adder-cost: 368   maxlim: 1611   bits: 12/11
c ---[ 293]---> Adder-cost: 368   maxlim: 1611   bits: 12/11
c ---[ 292]---> Adder-cost: 368   maxlim: 1614   bits: 12/11
c ---[ 291]---> Adder-cost: 368   maxlim: 1611   bits: 12/11
c ---[ 290]---> Adder-cost: 368   maxlim: 1610   bits: 12/11
c ---[ 289]---> Adder-cost: 368   maxlim: 1611   bits: 12/11
c ---[ 288]---> Adder-cost: 368   maxlim: 1613   bits: 12/11
c ---[ 287]---> Adder-cost: 368   maxlim: 1612   bits: 12/11
c ---[ 286]---> Adder-cost: 368   maxlim: 1611   bits: 12/11
c ---[ 285]---> Adder-cost: 368   maxlim: 1610   bits: 12/11
c ---[ 284]---> Adder-cost: 368   maxlim: 1613   bits: 12/11
c ---[ 283]---> Adder-cost: 368   maxlim: 1611   bits: 12/11
c ---[ 282]---> Adder-cost: 368   maxlim: 1610   bits: 12/11
c ---[ 281]---> Adder-cost: 368   maxlim: 1613   bits: 12/11
c ---[ 280]---> Adder-cost: 552   maxlim: 24190   bits: 16/15
c ---[ 279]---> Adder-cost: 552   maxlim: 24205   bits: 16/15
c ---[ 278]---> Adder-cost: 552   maxlim: 24190   bits: 16/15
c ---[ 277]---> Adder-cost: 424   maxlim: 4852   bits: 14/13
c ---[ 276]---> Adder-cost: 424   maxlim: 4849   bits: 14/13
c ---[ 275]---> Adder-cost: 368   maxlim: 1610   bits: 12/11
c ---[ 274]---> Adder-cost: 368   maxlim: 1612   bits: 12/11
c ---[ 273]---> Adder-cost: 368   maxlim: 1611   bits: 12/11
c ---[ 272]---> Adder-cost: 536   maxlim: 24247   bits: 16/15
c ---[ 271]---> Adder-cost: 536   maxlim: 24232   bits: 16/15
c ---[ 270]---> Adder-cost: 368   maxlim: 1612   bits: 12/11
c ---[ 269]---> Adder-cost: 368   maxlim: 1613   bits: 12/11
c ---[ 268]---> Adder-cost: 368   maxlim: 1611   bits: 12/11
c ---[ 267]---> Adder-cost: 368   maxlim: 1612   bits: 12/11
c ---[ 266]---> Adder-cost: 368   maxlim: 1611   bits: 12/11
c ---[ 265]---> Adder-cost: 368   maxlim: 1612   bits: 12/11
c ---[ 264]---> Adder-cost: 368   maxlim: 1612   bits: 12/11
c ---[ 263]---> Adder-cost: 368   maxlim: 1611   bits: 12/11
c ---[ 262]---> Adder-cost: 368   maxlim: 1610   bits: 12/11
c ---[ 261]---> Adder-cost: 368   maxlim: 1612   bits: 12/11
c ---[ 260]---> Adder-cost: 368   maxlim: 1611   bits: 12/11
c ---[ 259]---> Adder-cost: 368   maxlim: 1614   bits: 12/11
c ---[ 258]---> Adder-cost: 368   maxlim: 1611   bits: 12/11
c ---[ 257]---> Adder-cost: 368   maxlim: 1611   bits: 12/11
c ---[ 256]---> Adder-cost: 368   maxlim: 1611   bits: 12/11
c ---[ 255]---> Adder-cost: 368   maxlim: 1612   bits: 12/11
c ---[ 254]---> Adder-cost: 368   maxlim: 1611   bits: 12/11
c ---[ 253]---> Adder-cost: 368   maxlim: 1612   bits: 12/11
c ---[ 252]---> Adder-cost: 368   maxlim: 1611   bits: 12/11
c ---[ 251]---> Adder-cost: 368   maxlim: 1611   bits: 12/11
c ---[ 250]---> Adder-cost: 368   maxlim: 1612   bits: 12/11
c ---[ 249]---> Adder-cost: 368   maxlim: 1611   bits: 12/11
c ---[ 248]---> Adder-cost: 368   maxlim: 1612   bits: 12/11
c ---[ 247]---> Adder-cost: 368   maxlim: 1611   bits: 12/11
c ---[ 246]---> Adder-cost: 368   maxlim: 1611   bits: 12/11
c ---[ 245]---> Adder-cost: 368   maxlim: 1612   bits: 12/11
c ---[ 244]---> Adder-cost: 368   maxlim: 1611   bits: 12/11
c ---[ 243]---> Adder-cost: 462   maxlim: 8083   bits: 14/13
c ---[ 242]---> Adder-cost: 462   maxlim: 8078   bits: 14/13
c ---[ 241]---> Adder-cost: 368   maxlim: 1613   bits: 12/11
c ---[ 240]---> Adder-cost: 368   maxlim: 1613   bits: 12/11
c ---[ 239]---> Adder-cost: 368   maxlim: 1612   bits: 12/11
c ---[ 238]---> Adder-cost: 368   maxlim: 1612   bits: 12/11
c ---[ 237]---> Adder-cost: 368   maxlim: 1611   bits: 12/11
c ---[ 236]---> Adder-cost: 368   maxlim: 1611   bits: 12/11
c ---[ 235]---> Adder-cost: 368   maxlim: 1611   bits: 12/11
c ---[ 234]---> Adder-cost: 368   maxlim: 1612   bits: 12/11
c ---[ 233]---> Adder-cost: 368   maxlim: 1611   bits: 12/11
c ---[ 232]---> Adder-cost: 368   maxlim: 1611   bits: 12/11
c ---[ 231]---> Adder-cost: 368   maxlim: 1611   bits: 12/11
c ---[ 230]---> Adder-cost: 368   maxlim: 1612   bits: 12/11
c ---[ 229]---> Adder-cost: 368   maxlim: 1611   bits: 12/11
c ---[ 228]---> Adder-cost: 368   maxlim: 1612   bits: 12/11
c ---[ 227]---> Adder-cost: 368   maxlim: 1611   bits: 12/11
c ---[ 226]---> Adder-cost: 368   maxlim: 1611   bits: 12/11
c ---[ 225]---> Adder-cost: 368   maxlim: 1616   bits: 12/11
c ---[ 224]---> Adder-cost: 368   maxlim: 1613   bits: 12/11
c ---[ 223]---> Adder-cost: 368   maxlim: 1611   bits: 12/11
c ---[ 222]---> Adder-cost: 368   maxlim: 1612   bits: 12/11
c ---[ 221]---> Adder-cost: 368   maxlim: 1611   bits: 12/11
c ---[ 220]---> Adder-cost: 368   maxlim: 1612   bits: 12/11
c ---[ 219]---> Adder-cost: 368   maxlim: 1610   bits: 12/11
c ---[ 218]---> Adder-cost: 368   maxlim: 1612   bits: 12/11
c ---[ 217]---> Adder-cost: 368   maxlim: 1611   bits: 12/11
c ---[ 216]---> Adder-cost: 368   maxlim: 1612   bits: 12/11
c ---[ 215]---> Adder-cost: 368   maxlim: 1611   bits: 12/11
c ---[ 214]---> Adder-cost: 368   maxlim: 1614   bits: 12/11
c ---[ 213]---> Adder-cost: 368   maxlim: 1613   bits: 12/11
c ---[ 212]---> Adder-cost: 368   maxlim: 1613   bits: 12/11
c ---[ 211]---> Adder-cost: 368   maxlim: 1614   bits: 12/11
c ---[ 210]---> Adder-cost: 368   maxlim: 1611   bits: 12/11
c ---[ 209]---> Adder-cost: 368   maxlim: 1613   bits: 12/11
c ---[ 208]---> Adder-cost: 368   maxlim: 1611   bits: 12/11
c ---[ 207]---> Adder-cost: 368   maxlim: 1611   bits: 12/11
c ---[ 206]---> Adder-cost: 368   maxlim: 1612   bits: 12/11
c ---[ 205]---> Adder-cost: 368   maxlim: 1613   bits: 12/11
c ---[ 204]---> Adder-cost: 368   maxlim: 1610   bits: 12/11
c ---[ 203]---> Adder-cost: 368   maxlim: 1616   bits: 12/11
c ---[ 202]---> Adder-cost: 368   maxlim: 1610   bits: 12/11
c ---[ 201]---> Adder-cost: 368   maxlim: 1616   bits: 12/11
c ---[ 200]---> Adder-cost: 368   maxlim: 1612   bits: 12/11
c ---[ 199]---> Adder-cost: 368   maxlim: 1614   bits: 12/11
c ---[ 198]---> Adder-cost: 368   maxlim: 1611   bits: 12/11
c ---[ 197]---> Adder-cost: 368   maxlim: 1612   bits: 12/11
c ---[ 196]---> Adder-cost: 368   maxlim: 1611   bits: 12/11
c ---[ 195]---> Adder-cost: 368   maxlim: 1610   bits: 12/11
c ---[ 194]---> Adder-cost: 368   maxlim: 1616   bits: 12/11
c ---[ 193]---> Adder-cost: 368   maxlim: 1612   bits: 12/11
c ---[ 192]---> Adder-cost: 368   maxlim: 1612   bits: 12/11
c ---[ 191]---> Adder-cost: 368   maxlim: 1611   bits: 12/11
c ---[ 190]---> Adder-cost: 368   maxlim: 1612   bits: 12/11
c ---[ 189]---> Adder-cost: 368   maxlim: 1612   bits: 12/11
c ---[ 188]---> Adder-cost: 368   maxlim: 1611   bits: 12/11
c ---[ 187]---> Adder-cost: 368   maxlim: 1614   bits: 12/11
c ---[ 186]---> Adder-cost: 368   maxlim: 1613   bits: 12/11
c ---[ 185]---> Adder-cost: 368   maxlim: 1612   bits: 12/11
c ---[ 184]---> Adder-cost: 368   maxlim: 1614   bits: 12/11
c ---[ 183]---> Adder-cost: 368   maxlim: 1613   bits: 12/11
c ---[ 182]---> Adder-cost: 368   maxlim: 1611   bits: 12/11
c ---[ 181]---> Adder-cost: 368   maxlim: 1612   bits: 12/11
c ---[ 180]---> Adder-cost: 368   maxlim: 1613   bits: 12/11
c ---[ 179]---> Adder-cost: 368   maxlim: 1611   bits: 12/11
c ---[ 178]---> Adder-cost: 368   maxlim: 1612   bits: 12/11
c ---[ 177]---> Adder-cost: 546   maxlim: 24195   bits: 16/15
c ---[ 176]---> Adder-cost: 368   maxlim: 1612   bits: 12/11
c ---[ 175]---> Adder-cost: 368   maxlim: 1611   bits: 12/11
c ---[ 174]---> Adder-cost: 368   maxlim: 1611   bits: 12/11
c ---[ 173]---> Adder-cost: 368   maxlim: 1611   bits: 12/11
c ---[ 172]---> Adder-cost: 368   maxlim: 1614   bits: 12/11
c ---[ 171]---> Adder-cost: 448   maxlim: 8073   bits: 14/13
c ---[ 170]---> Adder-cost: 448   maxlim: 8068   bits: 14/13
c ---[ 169]---> Adder-cost: 368   maxlim: 1610   bits: 12/11
c ---[ 168]---> Adder-cost: 368   maxlim: 1612   bits: 12/11
c ---[ 167]---> Adder-cost: 368   maxlim: 1611   bits: 12/11
c ---[ 166]---> Adder-cost: 368   maxlim: 1611   bits: 12/11
c ---[ 165]---> Adder-cost: 368   maxlim: 1612   bits: 12/11
c ---[ 164]---> Adder-cost: 368   maxlim: 1611   bits: 12/11
c ---[ 163]---> Adder-cost: 368   maxlim: 1611   bits: 12/11
c ---[ 162]---> Adder-cost: 368   maxlim: 1612   bits: 12/11
c ---[ 161]---> Adder-cost: 368   maxlim: 1611   bits: 12/11
c ---[ 160]---> Adder-cost: 368   maxlim: 1611   bits: 12/11
c ---[ 159]---> Adder-cost: 368   maxlim: 1610   bits: 12/11
c ---[ 158]---> Adder-cost: 368   maxlim: 1611   bits: 12/11
c ---[ 157]---> Adder-cost: 368   maxlim: 1611   bits: 12/11
c ---[ 156]---> Adder-cost: 368   maxlim: 1611   bits: 12/11
c ---[ 155]---> Adder-cost: 368   maxlim: 1615   bits: 12/11
c ---[ 154]---> Adder-cost: 368   maxlim: 1610   bits: 12/11
c ---[ 153]---> Adder-cost: 368   maxlim: 1612   bits: 12/11
c ---[ 152]---> Adder-cost: 368   maxlim: 1612   bits: 12/11
c ---[ 151]---> Adder-cost: 368   maxlim: 1612   bits: 12/11
c ---[ 150]---> Adder-cost: 368   maxlim: 1612   bits: 12/11
c ---[ 149]---> Adder-cost: 368   maxlim: 1614   bits: 12/11
c ---[ 148]---> Adder-cost: 368   maxlim: 1611   bits: 12/11
c ---[ 147]---> Adder-cost: 368   maxlim: 1611   bits: 12/11
c ---[ 146]---> Adder-cost: 552   maxlim: 24211   bits: 16/15
c ---[ 145]---> Adder-cost: 552   maxlim: 24196   bits: 16/15
c ---[ 144]---> Adder-cost: 544   maxlim: 24195   bits: 16/15
c ---[ 143]---> Adder-cost: 544   maxlim: 24180   bits: 16/15
c ---[ 142]---> Adder-cost: 368   maxlim: 1612   bits: 12/11
c ---[ 141]---> Adder-cost: 368   maxlim: 1613   bits: 12/11
c ---[ 140]---> Adder-cost: 368   maxlim: 1613   bits: 12/11
c ---[ 139]---> Adder-cost: 368   maxlim: 1611   bits: 12/11
c ---[ 138]---> Adder-cost: 368   maxlim: 1611   bits: 12/11
c ---[ 137]---> Adder-cost: 368   maxlim: 1612   bits: 12/11
c ---[ 136]---> Adder-cost: 368   maxlim: 1613   bits: 12/11
c ---[ 135]---> Adder-cost: 368   maxlim: 1611   bits: 12/11
c ---[ 134]---> Adder-cost: 368   maxlim: 1612   bits: 12/11
c ---[ 133]---> Adder-cost: 368   maxlim: 1611   bits: 12/11
c ---[ 132]---> Adder-cost: 368   maxlim: 1612   bits: 12/11
c ---[ 131]---> Adder-cost: 368   maxlim: 1611   bits: 12/11
c ---[ 130]---> Adder-cost: 190   maxlim: 87   bits: 7/7
c ---[ 129]---> Adder-cost: 190   maxlim: 87   bits: 7/7
c ---[ 128]---> Adder-cost: 190   maxlim: 87   bits: 7/7
c ---[ 127]---> Adder-cost: 190   maxlim: 87   bits: 7/7
c ---[ 126]---> Adder-cost: 190   maxlim: 87   bits: 7/7
c ---[ 125]---> Adder-cost: 190   maxlim: 87   bits: 7/7
c ---[ 124]---> Adder-cost: 190   maxlim: 87   bits: 7/7
c ---[ 123]---> Adder-cost: 190   maxlim: 87   bits: 7/7
c ---[ 122]---> Adder-cost: 190   maxlim: 87   bits: 7/7
c ---[ 121]---> Adder-cost: 190   maxlim: 87   bits: 7/7
c ---[ 120]---> Adder-cost: 190   maxlim: 87   bits: 7/7
c ---[ 119]---> Adder-cost: 190   maxlim: 87   bits: 7/7
c ---[ 118]---> Adder-cost: 190   maxlim: 87   bits: 7/7
c ---[ 117]---> Adder-cost: 190   maxlim: 87   bits: 7/7
c ---[ 116]---> Adder-cost: 190   maxlim: 87   bits: 7/7
c ---[ 115]---> Adder-cost: 190   maxlim: 87   bits: 7/7
c ---[ 114]---> Adder-cost: 190   maxlim: 87   bits: 7/7
c ---[ 113]---> Adder-cost: 190   maxlim: 87   bits: 7/7
c ---[ 112]---> Adder-cost: 190   maxlim: 87   bits: 7/7
c ---[ 111]---> Adder-cost: 190   maxlim: 87   bits: 7/7
c ---[ 110]---> Adder-cost: 190   maxlim: 87   bits: 7/7
c ---[ 109]---> Adder-cost: 190   maxlim: 87   bits: 7/7
c ---[ 108]---> Adder-cost: 190   maxlim: 87   bits: 7/7
c ---[ 107]---> Adder-cost: 190   maxlim: 87   bits: 7/7
c ---[ 106]---> Adder-cost: 190   maxlim: 87   bits: 7/7
c ---[ 105]---> Adder-cost: 190   maxlim: 87   bits: 7/7
c ---[ 104]---> Adder-cost: 190   maxlim: 87   bits: 7/7
c ---[ 103]---> Adder-cost: 190   maxlim: 87   bits: 7/7
c ---[ 102]---> Adder-cost: 30   maxlim: 49   bits: 7/6
c ---[ 101]---> Adder-cost: 43   maxlim: 51   bits: 7/6
c ---[ 100]---> Adder-cost: 9   maxlim: 45   bits: 7/6
c ---[  99]---> Adder-cost: 46   maxlim: 52   bits: 7/6
c ---[  98]---> Adder-cost: 67   maxlim: 55   bits: 7/6
c ---[  97]---> Adder-cost: 9   maxlim: 45   bits: 7/6
c ---[  96]---> Adder-cost: 20   maxlim: 47   bits: 7/6
c ---[  95]---> Adder-cost: 76   maxlim: 57   bits: 7/6
c ---[  94]---> Adder-cost: 64   maxlim: 54   bits: 7/6
c ---[  93]---> Adder-cost: 43   maxlim: 51   bits: 7/6
c ---[  92]---> Adder-cost: 64   maxlim: 54   bits: 7/6
c ---[  91]---> Adder-cost: 15   maxlim: 46   bits: 7/6
c ---[  90]---> Adder-cost: 104   maxlim: 61   bits: 7/6
c ---[  89]---> Adder-cost: 20   maxlim: 47   bits: 7/6
c ---[  88]---> Adder-cost: 43   maxlim: 51   bits: 7/6
c ---[  87]---> Adder-cost: 46   maxlim: 52   bits: 7/6
c ---[  86]---> Adder-cost: 46   maxlim: 52   bits: 7/6
c ---[  85]---> Adder-cost: 20   maxlim: 47   bits: 7/6
c ---[  84]---> Adder-cost: 46   maxlim: 52   bits: 7/6
c ---[  83]---> Adder-cost: 30   maxlim: 49   bits: 7/6
c ---[  82]---> Adder-cost: 30   maxlim: 49   bits: 7/6
c ---[  81]---> Adder-cost: 74   maxlim: 56   bits: 7/6
c ---[  80]---> Adder-cost: 9   maxlim: 45   bits: 7/6
c ---[  79]---> Adder-cost: 51   maxlim: 53   bits: 7/6
c ---[  78]---> Adder-cost: 94   maxlim: 59   bits: 7/6
c ---[  77]---> Adder-cost: 30   maxlim: 49   bits: 7/6
c ---[  76]---> Adder-cost: 34   maxlim: 50   bits: 7/6
c ---[  75]---> Adder-cost: 30   maxlim: 49   bits: 7/6
c ---[  74]---> Adder-cost: 67   maxlim: 55   bits: 7/6
c ---[  73]---> Adder-cost: 118   maxlim: 63   bits: 7/6
c ---[  72]---> Adder-cost: 46   maxlim: 52   bits: 7/6
c ---[  71]---> Adder-cost: 94   maxlim: 59   bits: 7/6
c ---[  70]---> Adder-cost: 67   maxlim: 55   bits: 7/6
c ---[  69]---> Adder-cost: 23   maxlim: 48   bits: 7/6
c ---[  68]---> Adder-cost: 117   maxlim: 62   bits: 7/6
c ---[  67]---> Adder-cost: 74   maxlim: 56   bits: 7/6
c ---[  66]---> Adder-cost: 118   maxlim: 63   bits: 7/6
c ---[  65]---> Adder-cost: 9   maxlim: 45   bits: 7/6
c ---[  64]---> Adder-cost: 23   maxlim: 48   bits: 7/6
c ---[  63]---> Adder-cost: 34   maxlim: 50   bits: 7/6
c ---[  62]---> Adder-cost: 74   maxlim: 56   bits: 7/6
c ---[  61]---> Adder-cost: 30   maxlim: 49   bits: 7/6
c ---[  60]---> Adder-cost: 34   maxlim: 50   bits: 7/6
c ---[  59]---> Adder-cost: 74   maxlim: 56   bits: 7/6
c ---[  58]---> Adder-cost: 74   maxlim: 56   bits: 7/6
c ---[  57]---> Adder-cost: 64   maxlim: 54   bits: 7/6
c ---[  56]---> Adder-cost: 103   maxlim: 60   bits: 7/6
c ---[  55]---> Adder-cost: 103   maxlim: 60   bits: 7/6
c ---[  54]---> Adder-cost: 74   maxlim: 56   bits: 7/6
c ---[  53]---> Adder-cost: 34   maxlim: 50   bits: 7/6
c ---[  52]---> Adder-cost: 64   maxlim: 54   bits: 7/6
c ---[  51]---> Adder-cost: 85   maxlim: 58   bits: 7/6
c ---[  50]---> Adder-cost: 51   maxlim: 53   bits: 7/6
c ---[  49]---> Adder-cost: 76   maxlim: 57   bits: 7/6
c ---[  48]---> Adder-cost: 85   maxlim: 58   bits: 7/6
c ---[  47]---> Adder-cost: 74   maxlim: 56   bits: 7/6
c ---[  46]---> Adder-cost: 15   maxlim: 46   bits: 7/6
c ---[  45]---> Adder-cost: 103   maxlim: 60   bits: 7/6
c ---[  44]---> Adder-cost: 9   maxlim: 45   bits: 7/6
c ---[  43]---> Adder-cost: 43   maxlim: 51   bits: 7/6
c ---[  42]---> Adder-cost: 20   maxlim: 47   bits: 7/6
c ---[  41]---> Adder-cost: 51   maxlim: 53   bits: 7/6
c ---[  40]---> Adder-cost: 85   maxlim: 58   bits: 7/6
c ---[  39]---> Adder-cost: 74   maxlim: 56   bits: 7/6
c ---[  38]---> Adder-cost: 30   maxlim: 49   bits: 7/6
c ---[  37]---> Adder-cost: 30   maxlim: 49   bits: 7/6
c ---[  36]---> Adder-cost: 30   maxlim: 49   bits: 7/6
c ---[  35]---> Adder-cost: 103   maxlim: 60   bits: 7/6
c ---[  34]---> Adder-cost: 46   maxlim: 52   bits: 7/6
c ---[  33]---> Adder-cost: 9   maxlim: 45   bits: 7/6
c ---[  32]---> Adder-cost: 67   maxlim: 55   bits: 7/6
c ---[  31]---> Adder-cost: 46   maxlim: 52   bits: 7/6
c ---[  30]---> Adder-cost: 64   maxlim: 54   bits: 7/6
c ---[  29]---> Adder-cost: 9   maxlim: 45   bits: 7/6
c ---[  28]---> Adder-cost: 20   maxlim: 47   bits: 7/6
c ---[  27]---> Adder-cost: 43   maxlim: 51   bits: 7/6
c ---[  26]---> Adder-cost: 67   maxlim: 55   bits: 7/6
c ---[  25]---> Adder-cost: 23   maxlim: 48   bits: 7/6
c ---[  24]---> Adder-cost: 20   maxlim: 47   bits: 7/6
c ---[  23]---> Adder-cost: 15   maxlim: 46   bits: 7/6
c ---[  22]---> Adder-cost: 15   maxlim: 46   bits: 7/6
c ---[  21]---> Adder-cost: 74   maxlim: 56   bits: 7/6
c ---[  20]---> Adder-cost: 74   maxlim: 56   bits: 7/6
c ---[  19]---> Adder-cost: 67   maxlim: 55   bits: 7/6
c ---[  18]---> Adder-cost: 43   maxlim: 51   bits: 7/6
c ---[  17]---> Adder-cost: 67   maxlim: 55   bits: 7/6
c ---[  16]---> Adder-cost: 34   maxlim: 50   bits: 7/6
c ---[  15]---> Adder-cost: 74   maxlim: 56   bits: 7/6
c ---[  14]---> Adder-cost: 43   maxlim: 51   bits: 7/6
c ---[  13]---> Adder-cost: 76   maxlim: 57   bits: 7/6
c ---[  12]---> Adder-cost: 76   maxlim: 57   bits: 7/6
c ---[  11]---> Adder-cost: 9   maxlim: 45   bits: 7/6
c ---[  10]---> Adder-cost: 15   maxlim: 46   bits: 7/6
c ---[   9]---> Adder-cost: 43   maxlim: 51   bits: 7/6
c ---[   8]---> Adder-cost: 74   maxlim: 56   bits: 7/6
c ---[   7]---> Adder-cost: 117   maxlim: 62   bits: 7/6
c ---[   6]---> Adder-cost: 30   maxlim: 49   bits: 7/6
c ---[   5]---> Adder-cost: 67   maxlim: 55   bits: 7/6
c ---[   4]---> Adder-cost: 34   maxlim: 50   bits: 7/6
c ---[   3]---> Adder-cost: 103   maxlim: 60   bits: 7/6
c ---[   2]---> Adder-cost: 20   maxlim: 47   bits: 7/6
c ---[   1]---> Adder-cost: 23   maxlim: 48   bits: 7/6
c ---[   0]---> Adder-cost: 51   maxlim: 53   bits: 7/6
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |  941306  3352484 |  313768       0        0     nan |  0.000 % |
c |       100 |  941306  3352484 |  345144     100      694     6.9 |  3.516 % |
c |       250 |  941299  3352461 |  379659     249     1484     6.0 |  3.517 % |
c |       475 |  941299  3352461 |  417625     474     2729     5.8 |  3.517 % |
c |       816 |  941259  3352327 |  459387     810     6154     7.6 |  3.522 % |
c |      1323 |  941116  3351842 |  505326    1294    11158     8.6 |  3.538 % |
c |      2083 |  941116  3351842 |  555859    2054    27869    13.6 |  3.538 % |
c |      3222 |  941116  3351842 |  611445    3193    49152    15.4 |  3.538 % |
c |      4930 |  941116  3351842 |  672589    4901    81320    16.6 |  3.538 % |
c |      7492 |  940417  3349343 |  739848    6786   102505    15.1 |  3.578 % |
c |     11339 |  937566  3339401 |  813833    8939   127439    14.3 |  3.811 % |
c |     17105 |  935737  3333127 |  895216   14336   200202    14.0 |  3.993 % |
c |     25754 |  932140  3320631 |  984738   20858   366896    17.6 |  4.313 % |
c |     38730 |  927556  3304714 | 1083212   32283   687269    21.3 |  4.710 % |
c |     58191 |  927509  3304544 | 1191533   51702  1264068    24.4 |  4.712 % |
c |     87384 |  927500  3304513 | 1310686   80894  1932738    23.9 |  4.712 % |
c |    131175 |  923696  3291146 | 1441755  121999  2951906    24.2 |  5.023 % |
c |    196860 |  923298  3289720 | 1585931  168205  3984336    23.7 |  5.038 % |
c |    295386 |  910425  3244089 | 1744524  250309  6093108    24.3 |  5.908 % |
#### 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.65 0.88 0.86 2/54 9773
Raw data (stat): 9773 (runsolver) R 9772 28546 28545 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 487734221 1052672 99 4294967295 134512640 135381576 3221224464 3221219708 135158418 0 2147483391 7 90112 0 0 0 17 0 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0007 s]
Raw data (loadavg): 0.70 0.89 0.86 2/54 9773
Raw data (stat): 9773 (minisat+) R 9772 28546 28545 0 -1 0 16836 0 0 0 957 41 0 0 25 0 1 0 487734221 78053376 16435 4294967295 134512640 134672761 3221224576 3221223792 134561948 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19056 16435 603 41 0 19015 0
vsize: 76224
[startup+20.001 s]
Raw data (loadavg): 0.75 0.89 0.86 2/54 9773
Raw data (stat): 9773 (minisat+) R 9772 28546 28545 0 -1 0 17044 0 0 0 1957 42 0 0 25 0 1 0 487734221 78991360 16643 4294967295 134512640 134672761 3221224576 3221223748 134556602 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19285 16643 603 41 0 19244 0
vsize: 77140
[startup+30.0017 s]
Raw data (loadavg): 0.78 0.89 0.86 2/54 9773
Raw data (stat): 9773 (minisat+) R 9772 28546 28545 0 -1 0 17053 0 0 0 2956 42 0 0 25 0 1 0 487734221 78991360 16652 4294967295 134512640 134672761 3221224576 3221223792 134561993 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19285 16652 603 41 0 19244 0
vsize: 77140
[startup+40.0018 s]
Raw data (loadavg): 0.82 0.89 0.86 2/54 9773
Raw data (stat): 9773 (minisat+) R 9772 28546 28545 0 -1 0 17090 0 0 0 3956 43 0 0 25 0 1 0 487734221 79126528 16689 4294967295 134512640 134672761 3221224576 3221223748 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19318 16689 603 41 0 19277 0
vsize: 77272
[startup+50.0021 s]
Raw data (loadavg): 0.84 0.90 0.86 2/54 9773
Raw data (stat): 9773 (minisat+) R 9772 28546 28545 0 -1 0 17134 0 0 0 4956 43 0 0 25 0 1 0 487734221 79261696 16733 4294967295 134512640 134672761 3221224576 3221223748 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19351 16733 603 41 0 19310 0
vsize: 77404
[startup+60.0018 s]
Raw data (loadavg): 0.87 0.90 0.86 2/54 9773
Raw data (stat): 9773 (minisat+) R 9772 28546 28545 0 -1 0 17176 0 0 0 5955 43 0 0 25 0 1 0 487734221 79572992 16775 4294967295 134512640 134672761 3221224576 3221223748 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19427 16775 603 41 0 19386 0
vsize: 77708
[startup+70.0019 s]
Raw data (loadavg): 0.89 0.90 0.86 2/54 9773
Raw data (stat): 9773 (minisat+) R 9772 28546 28545 0 -1 0 17252 0 0 0 6955 44 0 0 25 0 1 0 487734221 79839232 16851 4294967295 134512640 134672761 3221224576 3221223748 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19492 16851 603 41 0 19451 0
vsize: 77968
[startup+80.0022 s]
Raw data (loadavg): 0.90 0.91 0.87 2/54 9773
Raw data (stat): 9773 (minisat+) R 9772 28546 28545 0 -1 0 17338 0 0 0 7955 44 0 0 25 0 1 0 487734221 80109568 16937 4294967295 134512640 134672761 3221224576 3221223748 134556688 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19558 16937 603 41 0 19517 0
vsize: 78232
[startup+90.0019 s]
Raw data (loadavg): 0.92 0.91 0.87 2/54 9773
Raw data (stat): 9773 (minisat+) R 9772 28546 28545 0 -1 0 17388 0 0 0 8955 45 0 0 25 0 1 0 487734221 80379904 16987 4294967295 134512640 134672761 3221224576 3221223748 134556688 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19624 16987 603 41 0 19583 0
vsize: 78496
[startup+100.002 s]
Raw data (loadavg): 0.93 0.91 0.87 2/54 9773
Raw data (stat): 9773 (minisat+) R 9772 28546 28545 0 -1 0 17405 0 0 0 9954 45 0 0 25 0 1 0 487734221 80379904 17004 4294967295 134512640 134672761 3221224576 3221223748 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19624 17004 603 41 0 19583 0
vsize: 78496
[startup+110.002 s]
Raw data (loadavg): 0.94 0.91 0.87 2/54 9773
Raw data (stat): 9773 (minisat+) R 9772 28546 28545 0 -1 0 17433 0 0 0 10954 46 0 0 25 0 1 0 487734221 80510976 17032 4294967295 134512640 134672761 3221224576 3221223748 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19656 17032 603 41 0 19615 0
vsize: 78624
[startup+120.002 s]
Raw data (loadavg): 0.95 0.92 0.87 2/54 9773
Raw data (stat): 9773 (minisat+) R 9772 28546 28545 0 -1 0 17489 0 0 0 11954 46 0 0 25 0 1 0 487734221 80781312 17088 4294967295 134512640 134672761 3221224576 3221223748 134556649 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19722 17088 603 41 0 19681 0
vsize: 78888
[startup+130.003 s]
Raw data (loadavg): 0.96 0.92 0.87 2/54 9773
Raw data (stat): 9773 (minisat+) R 9772 28546 28545 0 -1 0 17511 0 0 0 12953 47 0 0 25 0 1 0 487734221 80973824 17110 4294967295 134512640 134672761 3221224576 3221223792 134561950 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19769 17110 603 41 0 19728 0
vsize: 79076
[startup+140.003 s]
Raw data (loadavg): 0.96 0.92 0.87 2/54 9773
Raw data (stat): 9773 (minisat+) R 9772 28546 28545 0 -1 0 17527 0 0 0 13953 47 0 0 25 0 1 0 487734221 80973824 17126 4294967295 134512640 134672761 3221224576 3221223748 134556682 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19769 17126 603 41 0 19728 0
vsize: 79076
[startup+150.003 s]
Raw data (loadavg): 0.97 0.92 0.87 2/54 9773
Raw data (stat): 9773 (minisat+) R 9772 28546 28545 0 -1 0 17576 0 0 0 14953 47 0 0 25 0 1 0 487734221 81104896 17175 4294967295 134512640 134672761 3221224576 3221223748 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19801 17175 603 41 0 19760 0
vsize: 79204
[startup+160.003 s]
Raw data (loadavg): 0.97 0.92 0.87 2/54 9773
Raw data (stat): 9773 (minisat+) R 9772 28546 28545 0 -1 0 17584 0 0 0 15953 47 0 0 25 0 1 0 487734221 81240064 17183 4294967295 134512640 134672761 3221224576 3221223748 134556671 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19834 17183 603 41 0 19793 0
vsize: 79336
[startup+170.003 s]
Raw data (loadavg): 0.98 0.93 0.87 2/54 9773
Raw data (stat): 9773 (minisat+) R 9772 28546 28545 0 -1 0 17706 0 0 0 16952 48 0 0 25 0 1 0 487734221 81645568 17305 4294967295 134512640 134672761 3221224576 3221223748 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19933 17305 603 41 0 19892 0
vsize: 79732
[startup+180.004 s]
Raw data (loadavg): 0.98 0.93 0.88 2/54 9773
Raw data (stat): 9773 (minisat+) R 9772 28546 28545 0 -1 0 17748 0 0 0 17952 48 0 0 25 0 1 0 487734221 81915904 17347 4294967295 134512640 134672761 3221224576 3221223748 134556639 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19999 17347 603 41 0 19958 0
vsize: 79996
[startup+190.004 s]
Raw data (loadavg): 0.98 0.93 0.88 2/54 9773
Raw data (stat): 9773 (minisat+) R 9772 28546 28545 0 -1 0 17808 0 0 0 18952 49 0 0 25 0 1 0 487734221 82046976 17407 4294967295 134512640 134672761 3221224576 3221223748 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20031 17407 603 41 0 19990 0
vsize: 80124
[startup+200.004 s]
Raw data (loadavg): 0.98 0.93 0.88 2/54 9773
Raw data (stat): 9773 (minisat+) R 9772 28546 28545 0 -1 0 17875 0 0 0 19951 49 0 0 25 0 1 0 487734221 82313216 17474 4294967295 134512640 134672761 3221224576 3221223748 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20096 17474 603 41 0 20055 0
vsize: 80384
[startup+210.003 s]
Raw data (loadavg): 0.99 0.93 0.88 2/54 9773
Raw data (stat): 9773 (minisat+) R 9772 28546 28545 0 -1 0 17894 0 0 0 20951 50 0 0 25 0 1 0 487734221 82448384 17493 4294967295 134512640 134672761 3221224576 3221223748 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20129 17493 603 41 0 20088 0
vsize: 80516
[startup+220.004 s]
Raw data (loadavg): 0.99 0.94 0.88 2/54 9773
Raw data (stat): 9773 (minisat+) R 9772 28546 28545 0 -1 0 17920 0 0 0 21951 50 0 0 25 0 1 0 487734221 82583552 17519 4294967295 134512640 134672761 3221224576 3221223748 134556688 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20162 17519 603 41 0 20121 0
vsize: 80648
[startup+230.004 s]
Raw data (loadavg): 0.99 0.94 0.88 2/54 9773
Raw data (stat): 9773 (minisat+) R 9772 28546 28545 0 -1 0 17982 0 0 0 22950 51 0 0 25 0 1 0 487734221 82853888 17581 4294967295 134512640 134672761 3221224576 3221223748 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20228 17581 603 41 0 20187 0
vsize: 80912
[startup+240.004 s]
Raw data (loadavg): 0.99 0.94 0.88 2/54 9773
Raw data (stat): 9773 (minisat+) R 9772 28546 28545 0 -1 0 18084 0 0 0 23950 52 0 0 25 0 1 0 487734221 83247104 17683 4294967295 134512640 134672761 3221224576 3221223748 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20324 17683 603 41 0 20283 0
vsize: 81296
[startup+250.004 s]
Raw data (loadavg): 0.99 0.94 0.88 2/54 9773
Raw data (stat): 9773 (minisat+) R 9772 28546 28545 0 -1 0 18114 0 0 0 24949 52 0 0 25 0 1 0 487734221 83382272 17713 4294967295 134512640 134672761 3221224576 3221223748 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20357 17713 603 41 0 20316 0
vsize: 81428
[startup+260.005 s]
Raw data (loadavg): 0.99 0.94 0.88 2/54 9773
Raw data (stat): 9773 (minisat+) R 9772 28546 28545 0 -1 0 18764 0 0 0 25948 54 0 0 25 0 1 0 487734221 86052864 18363 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21009 18363 603 41 0 20968 0
vsize: 84036
[startup+270.004 s]
Raw data (loadavg): 0.99 0.94 0.88 2/54 9773
Raw data (stat): 9773 (minisat+) R 9772 28546 28545 0 -1 0 19160 0 0 0 26946 55 0 0 25 0 1 0 487734221 87678976 18759 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21406 18759 603 41 0 21365 0
vsize: 85624
[startup+280.004 s]
Raw data (loadavg): 0.99 0.94 0.89 2/54 9773
Raw data (stat): 9773 (minisat+) R 9772 28546 28545 0 -1 0 19447 0 0 0 27946 56 0 0 25 0 1 0 487734221 88903680 19046 4294967295 134512640 134672761 3221224576 3221223744 134561011 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21705 19046 603 41 0 21664 0
vsize: 86820
[startup+290.005 s]
Raw data (loadavg): 0.99 0.95 0.89 2/54 9773
Raw data (stat): 9773 (minisat+) R 9772 28546 28545 0 -1 0 19641 0 0 0 28945 57 0 0 25 0 1 0 487734221 89833472 19240 4294967295 134512640 134672761 3221224576 3221223744 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21932 19240 603 41 0 21891 0
vsize: 87728
[startup+300.005 s]
Raw data (loadavg): 0.99 0.95 0.89 2/54 9773
Raw data (stat): 9773 (minisat+) R 9772 28546 28545 0 -1 0 19827 0 0 0 29944 58 0 0 25 0 1 0 487734221 90632192 19426 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22127 19426 603 41 0 22086 0
vsize: 88508
[startup+310.006 s]
Raw data (loadavg): 0.99 0.95 0.89 2/54 9773
Raw data (stat): 9773 (minisat+) R 9772 28546 28545 0 -1 0 20031 0 0 0 30944 58 0 0 25 0 1 0 487734221 91496448 19630 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22338 19630 603 41 0 22297 0
vsize: 89352
[startup+320.006 s]
Raw data (loadavg): 0.99 0.95 0.89 2/54 9773
Raw data (stat): 9773 (minisat+) R 9772 28546 28545 0 -1 0 20193 0 0 0 31944 59 0 0 25 0 1 0 487734221 92307456 19792 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22536 19792 603 41 0 22495 0
vsize: 90144
[startup+330.007 s]
Raw data (loadavg): 0.99 0.95 0.89 2/54 9773
Raw data (stat): 9773 (minisat+) R 9772 28546 28545 0 -1 0 20300 0 0 0 32943 59 0 0 25 0 1 0 487734221 92712960 19899 4294967295 134512640 134672761 3221224576 3221223748 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22635 19899 603 41 0 22594 0
vsize: 90540
[startup+340.007 s]
Raw data (loadavg): 0.99 0.95 0.89 2/54 9773
Raw data (stat): 9773 (minisat+) R 9772 28546 28545 0 -1 0 20413 0 0 0 33943 60 0 0 25 0 1 0 487734221 93204480 20012 4294967295 134512640 134672761 3221224576 3221223748 134556653 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22755 20012 603 41 0 22714 0
vsize: 91020
[startup+350.006 s]
Raw data (loadavg): 0.99 0.95 0.89 2/54 9773
Raw data (stat): 9773 (minisat+) R 9772 28546 28545 0 -1 0 20504 0 0 0 34943 60 0 0 25 0 1 0 487734221 93601792 20103 4294967295 134512640 134672761 3221224576 3221223748 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22852 20103 603 41 0 22811 0
vsize: 91408
[startup+360.006 s]
Raw data (loadavg): 0.99 0.95 0.89 2/54 9773
Raw data (stat): 9773 (minisat+) R 9772 28546 28545 0 -1 0 20589 0 0 0 35943 61 0 0 25 0 1 0 487734221 93872128 20188 4294967295 134512640 134672761 3221224576 3221223748 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22918 20188 603 41 0 22877 0
vsize: 91672
[startup+370.006 s]
Raw data (loadavg): 0.99 0.95 0.89 2/54 9773
Raw data (stat): 9773 (minisat+) R 9772 28546 28545 0 -1 0 20642 0 0 0 36943 61 0 0 25 0 1 0 487734221 94134272 20241 4294967295 134512640 134672761 3221224576 3221223748 134556660 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22982 20241 603 41 0 22941 0
vsize: 91928
[startup+380.006 s]
Raw data (loadavg): 0.99 0.95 0.89 2/54 9773
Raw data (stat): 9773 (minisat+) R 9772 28546 28545 0 -1 0 20690 0 0 0 37943 61 0 0 25 0 1 0 487734221 94269440 20289 4294967295 134512640 134672761 3221224576 3221223748 134556649 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23015 20289 603 41 0 22974 0
vsize: 92060
[startup+390.006 s]
Raw data (loadavg): 0.99 0.95 0.90 2/54 9773
Raw data (stat): 9773 (minisat+) R 9772 28546 28545 0 -1 0 20740 0 0 0 38943 61 0 0 25 0 1 0 487734221 94539776 20339 4294967295 134512640 134672761 3221224576 3221223748 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23081 20339 603 41 0 23040 0
vsize: 92324
[startup+400.006 s]
Raw data (loadavg): 0.99 0.96 0.90 2/54 9773
Raw data (stat): 9773 (minisat+) R 9772 28546 28545 0 -1 0 20802 0 0 0 39943 61 0 0 25 0 1 0 487734221 94674944 20401 4294967295 134512640 134672761 3221224576 3221223748 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23114 20401 603 41 0 23073 0
vsize: 92456
[startup+410.006 s]
Raw data (loadavg): 0.99 0.96 0.90 2/54 9773
Raw data (stat): 9773 (minisat+) R 9772 28546 28545 0 -1 0 21251 0 0 0 40942 62 0 0 25 0 1 0 487734221 96546816 20850 4294967295 134512640 134672761 3221224576 3221223744 134561154 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23571 20850 603 41 0 23530 0
vsize: 94284
[startup+420.007 s]
Raw data (loadavg): 0.99 0.96 0.90 2/54 9773
Raw data (stat): 9773 (minisat+) R 9772 28546 28545 0 -1 0 21614 0 0 0 41941 63 0 0 25 0 1 0 487734221 98017280 21213 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23930 21213 603 41 0 23889 0
vsize: 95720
[startup+430.007 s]
Raw data (loadavg): 0.99 0.96 0.90 2/54 9773
Raw data (stat): 9773 (minisat+) R 9772 28546 28545 0 -1 0 21842 0 0 0 42940 64 0 0 25 0 1 0 487734221 99479552 21441 4294967295 134512640 134672761 3221224576 3221223760 134559332 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24287 21441 603 41 0 24246 0
vsize: 97148
[startup+440.007 s]
Raw data (loadavg): 0.99 0.96 0.90 2/54 9773
Raw data (stat): 9773 (minisat+) R 9772 28546 28545 0 -1 0 22019 0 0 0 43940 64 0 0 25 0 1 0 487734221 100143104 21618 4294967295 134512640 134672761 3221224576 3221223744 134560988 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24449 21618 603 41 0 24408 0
vsize: 97796
[startup+450.007 s]
Raw data (loadavg): 0.99 0.96 0.90 2/54 9773
Raw data (stat): 9773 (minisat+) R 9772 28546 28545 0 -1 0 22162 0 0 0 44940 65 0 0 25 0 1 0 487734221 100683776 21761 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24581 21761 603 41 0 24540 0
vsize: 98324
[startup+460.007 s]
Raw data (loadavg): 0.99 0.96 0.90 2/54 9773
Raw data (stat): 9773 (minisat+) R 9772 28546 28545 0 -1 0 22277 0 0 0 45939 65 0 0 25 0 1 0 487734221 101224448 21876 4294967295 134512640 134672761 3221224576 3221223744 134560920 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24713 21876 603 41 0 24672 0
vsize: 98852
[startup+470.008 s]
Raw data (loadavg): 0.99 0.96 0.90 2/54 9773
Raw data (stat): 9773 (minisat+) R 9772 28546 28545 0 -1 0 22330 0 0 0 46940 65 0 0 25 0 1 0 487734221 101355520 21929 4294967295 134512640 134672761 3221224576 3221223744 134561164 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24745 21929 603 41 0 24704 0
vsize: 98980
[startup+480.008 s]
Raw data (loadavg): 0.99 0.96 0.90 2/54 9773
Raw data (stat): 9773 (minisat+) R 9772 28546 28545 0 -1 0 22354 0 0 0 47940 66 0 0 25 0 1 0 487734221 101502976 21953 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24781 21953 603 41 0 24740 0
vsize: 99124
[startup+490.007 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 9773
Raw data (stat): 9773 (minisat+) R 9772 28546 28545 0 -1 0 22404 0 0 0 48940 66 0 0 25 0 1 0 487734221 101785600 22003 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24850 22003 603 41 0 24809 0
vsize: 99400
[startup+500.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 9773
Raw data (stat): 9773 (minisat+) R 9772 28546 28545 0 -1 0 22513 0 0 0 49939 66 0 0 25 0 1 0 487734221 102199296 22112 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24951 22112 603 41 0 24910 0
vsize: 99804
[startup+510.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 9773
Raw data (stat): 9773 (minisat+) R 9772 28546 28545 0 -1 0 22673 0 0 0 50939 67 0 0 25 0 1 0 487734221 102883328 22272 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25118 22272 603 41 0 25077 0
vsize: 100472
[startup+520.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 9773
Raw data (stat): 9773 (minisat+) R 9772 28546 28545 0 -1 0 22808 0 0 0 51939 67 0 0 25 0 1 0 487734221 103419904 22407 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25249 22407 603 41 0 25208 0
vsize: 100996
[startup+530.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 9773
Raw data (stat): 9773 (minisat+) R 9772 28546 28545 0 -1 0 22931 0 0 0 52938 68 0 0 25 0 1 0 487734221 103952384 22530 4294967295 134512640 134672761 3221224576 3221223728 134565092 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25379 22530 603 41 0 25338 0
vsize: 101516
[startup+540.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 9773
Raw data (stat): 9773 (minisat+) R 9772 28546 28545 0 -1 0 23026 0 0 0 53938 68 0 0 25 0 1 0 487734221 104243200 22625 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25450 22625 603 41 0 25409 0
vsize: 101800
[startup+550.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 9773
Raw data (stat): 9773 (minisat+) R 9772 28546 28545 0 -1 0 23130 0 0 0 54937 69 0 0 25 0 1 0 487734221 104681472 22729 4294967295 134512640 134672761 3221224576 3221223748 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25557 22729 603 41 0 25516 0
vsize: 102228
[startup+560.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 9773
Raw data (stat): 9773 (minisat+) R 9772 28546 28545 0 -1 0 23150 0 0 0 55938 69 0 0 25 0 1 0 487734221 104816640 22749 4294967295 134512640 134672761 3221224576 3221223748 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25590 22749 603 41 0 25549 0
vsize: 102360
[startup+570.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 9773
Raw data (stat): 9773 (minisat+) R 9772 28546 28545 0 -1 0 23176 0 0 0 56938 69 0 0 25 0 1 0 487734221 104951808 22775 4294967295 134512640 134672761 3221224576 3221223748 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25623 22775 603 41 0 25582 0
vsize: 102492
[startup+580.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 9773
Raw data (stat): 9773 (minisat+) R 9772 28546 28545 0 -1 0 23206 0 0 0 57938 69 0 0 25 0 1 0 487734221 105086976 22805 4294967295 134512640 134672761 3221224576 3221223748 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25656 22805 603 41 0 25615 0
vsize: 102624
[startup+590.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 9773
Raw data (stat): 9773 (minisat+) R 9772 28546 28545 0 -1 0 23271 0 0 0 58938 69 0 0 25 0 1 0 487734221 105357312 22870 4294967295 134512640 134672761 3221224576 3221223748 134556632 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25722 22870 603 41 0 25681 0
vsize: 102888
[startup+600.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 9773
Raw data (stat): 9773 (minisat+) R 9772 28546 28545 0 -1 0 23375 0 0 0 59937 70 0 0 25 0 1 0 487734221 105762816 22974 4294967295 134512640 134672761 3221224576 3221223748 134556685 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25821 22974 603 41 0 25780 0
vsize: 103284
[startup+610.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 9773
Raw data (stat): 9773 (minisat+) R 9772 28546 28545 0 -1 0 23397 0 0 0 60937 70 0 0 25 0 1 0 487734221 105762816 22996 4294967295 134512640 134672761 3221224576 3221223748 134556639 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25821 22996 603 41 0 25780 0
vsize: 103284
[startup+620.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 9773
Raw data (stat): 9773 (minisat+) R 9772 28546 28545 0 -1 0 23432 0 0 0 61937 70 0 0 25 0 1 0 487734221 105897984 23031 4294967295 134512640 134672761 3221224576 3221223748 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25854 23031 603 41 0 25813 0
vsize: 103416
[startup+630.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 9773
Raw data (stat): 9773 (minisat+) R 9772 28546 28545 0 -1 0 23447 0 0 0 62937 70 0 0 25 0 1 0 487734221 106033152 23046 4294967295 134512640 134672761 3221224576 3221223744 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25887 23046 603 41 0 25846 0
vsize: 103548
[startup+640.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 9773
Raw data (stat): 9773 (minisat+) R 9772 28546 28545 0 -1 0 23475 0 0 0 63937 70 0 0 25 0 1 0 487734221 106168320 23074 4294967295 134512640 134672761 3221224576 3221223744 134560956 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25920 23074 603 41 0 25879 0
vsize: 103680
[startup+650.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 9773
Raw data (stat): 9773 (minisat+) R 9772 28546 28545 0 -1 0 23504 0 0 0 64938 70 0 0 25 0 1 0 487734221 106303488 23103 4294967295 134512640 134672761 3221224576 3221223748 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25953 23103 603 41 0 25912 0
vsize: 103812
[startup+660.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 9773
Raw data (stat): 9773 (minisat+) R 9772 28546 28545 0 -1 0 23680 0 0 0 65937 71 0 0 25 0 1 0 487734221 106967040 23279 4294967295 134512640 134672761 3221224576 3221223712 134565092 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26115 23279 603 41 0 26074 0
vsize: 104460
[startup+670.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 9773
Raw data (stat): 9773 (minisat+) R 9772 28546 28545 0 -1 0 23794 0 0 0 66937 71 0 0 25 0 1 0 487734221 107364352 23393 4294967295 134512640 134672761 3221224576 3221223748 134556649 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26212 23393 603 41 0 26171 0
vsize: 104848
[startup+680.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 9773
Raw data (stat): 9773 (minisat+) R 9772 28546 28545 0 -1 0 23795 0 0 0 67938 71 0 0 25 0 1 0 487734221 107364352 23394 4294967295 134512640 134672761 3221224576 3221223748 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26212 23394 603 41 0 26171 0
vsize: 104848
[startup+690.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 9773
Raw data (stat): 9773 (minisat+) R 9772 28546 28545 0 -1 0 23807 0 0 0 68938 71 0 0 25 0 1 0 487734221 107495424 23406 4294967295 134512640 134672761 3221224576 3221223780 134561964 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26244 23406 603 41 0 26203 0
vsize: 104976
[startup+700.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 9773
Raw data (stat): 9773 (minisat+) R 9772 28546 28545 0 -1 0 23868 0 0 0 69938 71 0 0 25 0 1 0 487734221 107626496 23467 4294967295 134512640 134672761 3221224576 3221223748 134556649 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26276 23467 603 41 0 26235 0
vsize: 105104
[startup+710.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 9773
Raw data (stat): 9773 (minisat+) R 9772 28546 28545 0 -1 0 23931 0 0 0 70938 71 0 0 25 0 1 0 487734221 107892736 23530 4294967295 134512640 134672761 3221224576 3221223760 134559254 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26341 23530 603 41 0 26300 0
vsize: 105364
[startup+720.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 9773
Raw data (stat): 9773 (minisat+) R 9772 28546 28545 0 -1 0 24451 0 0 0 71937 72 0 0 25 0 1 0 487734221 110022656 24050 4294967295 134512640 134672761 3221224576 3221223744 134560956 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26861 24050 603 41 0 26820 0
vsize: 107444
[startup+730.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 9773
Raw data (stat): 9773 (minisat+) R 9772 28546 28545 0 -1 0 24575 0 0 0 72937 73 0 0 25 0 1 0 487734221 110555136 24174 4294967295 134512640 134672761 3221224576 3221223748 134556682 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26991 24174 603 41 0 26950 0
vsize: 107964
[startup+740.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 9773
Raw data (stat): 9773 (minisat+) R 9772 28546 28545 0 -1 0 24607 0 0 0 73937 73 0 0 25 0 1 0 487734221 110686208 24206 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27023 24206 603 41 0 26982 0
vsize: 108092
[startup+750.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 9773
Raw data (stat): 9773 (minisat+) R 9772 28546 28545 0 -1 0 24618 0 0 0 74937 73 0 0 25 0 1 0 487734221 110686208 24217 4294967295 134512640 134672761 3221224576 3221223776 134561972 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27023 24217 603 41 0 26982 0
vsize: 108092
[startup+760.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 9773
Raw data (stat): 9773 (minisat+) R 9772 28546 28545 0 -1 0 24620 0 0 0 75937 73 0 0 25 0 1 0 487734221 110686208 24219 4294967295 134512640 134672761 3221224576 3221223748 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27023 24219 603 41 0 26982 0
vsize: 108092
[startup+770.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 9773
Raw data (stat): 9773 (minisat+) R 9772 28546 28545 0 -1 0 24621 0 0 0 76937 73 0 0 25 0 1 0 487734221 110686208 24220 4294967295 134512640 134672761 3221224576 3221223780 134561964 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27023 24220 603 41 0 26982 0
vsize: 108092
[startup+780.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 9773
Raw data (stat): 9773 (minisat+) R 9772 28546 28545 0 -1 0 24621 0 0 0 77937 73 0 0 25 0 1 0 487734221 110686208 24220 4294967295 134512640 134672761 3221224576 3221223780 134561964 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27023 24220 603 41 0 26982 0
vsize: 108092
[startup+790.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 9773
Raw data (stat): 9773 (minisat+) R 9772 28546 28545 0 -1 0 24633 0 0 0 78937 73 0 0 25 0 1 0 487734221 110821376 24232 4294967295 134512640 134672761 3221224576 3221223744 134560929 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27056 24232 603 41 0 27015 0
vsize: 108224
[startup+800.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 9773
Raw data (stat): 9773 (minisat+) R 9772 28546 28545 0 -1 0 25012 0 0 0 79936 74 0 0 25 0 1 0 487734221 112291840 24611 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27415 24611 603 41 0 27374 0
vsize: 109660
[startup+810.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 9773
Raw data (stat): 9773 (minisat+) R 9772 28546 28545 0 -1 0 25324 0 0 0 80936 75 0 0 25 0 1 0 487734221 113524736 24923 4294967295 134512640 134672761 3221224576 3221223748 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27716 24923 603 41 0 27675 0
vsize: 110864
[startup+820.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 9773
Raw data (stat): 9773 (minisat+) R 9772 28546 28545 0 -1 0 25652 0 0 0 81935 76 0 0 25 0 1 0 487734221 114905088 25251 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28053 25251 603 41 0 28012 0
vsize: 112212
[startup+830.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 9773
Raw data (stat): 9773 (minisat+) R 9772 28546 28545 0 -1 0 25928 0 0 0 82934 77 0 0 25 0 1 0 487734221 116166656 25527 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28361 25527 603 41 0 28320 0
vsize: 113444
[startup+840.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 9773
Raw data (stat): 9773 (minisat+) R 9772 28546 28545 0 -1 0 26155 0 0 0 83934 78 0 0 25 0 1 0 487734221 116965376 25754 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28556 25754 603 41 0 28515 0
vsize: 114224
[startup+850.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 9773
Raw data (stat): 9773 (minisat+) R 9772 28546 28545 0 -1 0 26332 0 0 0 84933 78 0 0 25 0 1 0 487734221 117837824 25931 4294967295 134512640 134672761 3221224576 3221223744 134561218 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28769 25931 603 41 0 28728 0
vsize: 115076
[startup+860.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 9773
Raw data (stat): 9773 (minisat+) R 9772 28546 28545 0 -1 0 26494 0 0 0 85932 79 0 0 25 0 1 0 487734221 118517760 26093 4294967295 134512640 134672761 3221224576 3221223744 134561011 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28935 26093 603 41 0 28894 0
vsize: 115740
[startup+870.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 9773
Raw data (stat): 9773 (minisat+) R 9772 28546 28545 0 -1 0 26623 0 0 0 86931 79 0 0 25 0 1 0 487734221 119001088 26222 4294967295 134512640 134672761 3221224576 3221223668 1075351236 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29053 26222 603 41 0 29012 0
vsize: 116212
[startup+880.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 9773
Raw data (stat): 9773 (minisat+) R 9772 28546 28545 0 -1 0 26729 0 0 0 87931 80 0 0 25 0 1 0 487734221 119459840 26328 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29165 26328 603 41 0 29124 0
vsize: 116660
[startup+890.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 9773
Raw data (stat): 9773 (minisat+) R 9772 28546 28545 0 -1 0 26870 0 0 0 88931 80 0 0 25 0 1 0 487734221 121044992 26469 4294967295 134512640 134672761 3221224576 3221223744 134560937 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29552 26469 603 41 0 29511 0
vsize: 118208
[startup+900.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 9773
Raw data (stat): 9773 (minisat+) R 9772 28546 28545 0 -1 0 27017 0 0 0 89930 81 0 0 25 0 1 0 487734221 121724928 26616 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29718 26616 603 41 0 29677 0
vsize: 118872
[startup+910.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 9773
Raw data (stat): 9773 (minisat+) R 9772 28546 28545 0 -1 0 27141 0 0 0 90930 81 0 0 25 0 1 0 487734221 122273792 26740 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29852 26740 603 41 0 29811 0
vsize: 119408
[startup+920.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 9773
Raw data (stat): 9773 (minisat+) R 9772 28546 28545 0 -1 0 27307 0 0 0 91930 82 0 0 25 0 1 0 487734221 122953728 26906 4294967295 134512640 134672761 3221224576 3221223744 134560948 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30018 26906 603 41 0 29977 0
vsize: 120072
[startup+930.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 9773
Raw data (stat): 9773 (minisat+) R 9772 28546 28545 0 -1 0 27407 0 0 0 92930 82 0 0 25 0 1 0 487734221 123416576 27006 4294967295 134512640 134672761 3221224576 3221223744 134560876 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30131 27006 603 41 0 30090 0
vsize: 120524
[startup+940.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 9773
Raw data (stat): 9773 (minisat+) R 9772 28546 28545 0 -1 0 27524 0 0 0 93929 83 0 0 25 0 1 0 487734221 123834368 27123 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30233 27123 603 41 0 30192 0
vsize: 120932
[startup+950.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 9773
Raw data (stat): 9773 (minisat+) R 9772 28546 28545 0 -1 0 27643 0 0 0 94929 83 0 0 25 0 1 0 487734221 124375040 27242 4294967295 134512640 134672761 3221224576 3221223744 134561198 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30365 27242 603 41 0 30324 0
vsize: 121460
[startup+960.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 9773
Raw data (stat): 9773 (minisat+) R 9772 28546 28545 0 -1 0 27760 0 0 0 95929 84 0 0 25 0 1 0 487734221 124776448 27359 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30463 27359 603 41 0 30422 0
vsize: 121852
[startup+970.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 9773
Raw data (stat): 9773 (minisat+) R 9772 28546 28545 0 -1 0 27890 0 0 0 96928 84 0 0 25 0 1 0 487734221 125390848 27489 4294967295 134512640 134672761 3221224576 3221223744 134560996 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30613 27489 603 41 0 30572 0
vsize: 122452
[startup+980.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 9773
Raw data (stat): 9773 (minisat+) R 9772 28546 28545 0 -1 0 28010 0 0 0 97928 84 0 0 25 0 1 0 487734221 125784064 27609 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30709 27609 603 41 0 30668 0
vsize: 122836
[startup+990.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 9773
Raw data (stat): 9773 (minisat+) R 9772 28546 28545 0 -1 0 28129 0 0 0 98928 85 0 0 25 0 1 0 487734221 126308352 27728 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30837 27728 603 41 0 30796 0
vsize: 123348
[startup+1000.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 9773
Raw data (stat): 9773 (minisat+) R 9772 28546 28545 0 -1 0 28222 0 0 0 99928 85 0 0 25 0 1 0 487734221 126795776 27821 4294967295 134512640 134672761 3221224576 3221223744 134560903 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30956 27821 603 41 0 30915 0
vsize: 123824
[startup+1010.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 9773
Raw data (stat): 9773 (minisat+) R 9772 28546 28545 0 -1 0 28293 0 0 0 100928 85 0 0 25 0 1 0 487734221 127057920 27892 4294967295 134512640 134672761 3221224576 3221223744 134560909 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31020 27892 603 41 0 30979 0
vsize: 124080
[startup+1020.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 9773
Raw data (stat): 9773 (minisat+) R 9772 28546 28545 0 -1 0 28370 0 0 0 101928 85 0 0 25 0 1 0 487734221 127340544 27969 4294967295 134512640 134672761 3221224576 3221223744 134561215 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31089 27969 603 41 0 31048 0
vsize: 124356
[startup+1030.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 9773
Raw data (stat): 9773 (minisat+) R 9772 28546 28545 0 -1 0 28453 0 0 0 102928 86 0 0 25 0 1 0 487734221 127881216 28052 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31221 28052 603 41 0 31180 0
vsize: 124884
[startup+1040.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 9773
Raw data (stat): 9773 (minisat+) R 9772 28546 28545 0 -1 0 28532 0 0 0 103928 86 0 0 25 0 1 0 487734221 128262144 28131 4294967295 134512640 134672761 3221224576 3221223744 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31314 28131 603 41 0 31273 0
vsize: 125256
[startup+1050.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 9773
Raw data (stat): 9773 (minisat+) R 9772 28546 28545 0 -1 0 28593 0 0 0 104928 86 0 0 25 0 1 0 487734221 128532480 28192 4294967295 134512640 134672761 3221224576 3221223744 134560937 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31380 28192 603 41 0 31339 0
vsize: 125520
[startup+1060.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 9773
Raw data (stat): 9773 (minisat+) R 9772 28546 28545 0 -1 0 28656 0 0 0 105928 86 0 0 25 0 1 0 487734221 128679936 28255 4294967295 134512640 134672761 3221224576 3221223744 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31416 28255 603 41 0 31375 0
vsize: 125664
[startup+1070.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 9773
Raw data (stat): 9773 (minisat+) R 9772 28546 28545 0 -1 0 28759 0 0 0 106928 87 0 0 25 0 1 0 487734221 129110016 28358 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31521 28358 603 41 0 31480 0
vsize: 126084
[startup+1080.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 9773
Raw data (stat): 9773 (minisat+) R 9772 28546 28545 0 -1 0 28853 0 0 0 107928 87 0 0 25 0 1 0 487734221 129536000 28452 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31625 28452 603 41 0 31584 0
vsize: 126500
[startup+1090.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 9773
Raw data (stat): 9773 (minisat+) R 9772 28546 28545 0 -1 0 28951 0 0 0 108928 87 0 0 25 0 1 0 487734221 129929216 28550 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31721 28550 603 41 0 31680 0
vsize: 126884
[startup+1100.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 9773
Raw data (stat): 9773 (minisat+) R 9772 28546 28545 0 -1 0 29044 0 0 0 109928 87 0 0 25 0 1 0 487734221 130334720 28643 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31820 28643 603 41 0 31779 0
vsize: 127280
[startup+1110.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 9773
Raw data (stat): 9773 (minisat+) R 9772 28546 28545 0 -1 0 29132 0 0 0 110928 88 0 0 25 0 1 0 487734221 130719744 28731 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31914 28731 603 41 0 31873 0
vsize: 127656
[startup+1120.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 9773
Raw data (stat): 9773 (minisat+) R 9772 28546 28545 0 -1 0 29217 0 0 0 111928 88 0 0 25 0 1 0 487734221 130985984 28816 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31979 28816 603 41 0 31938 0
vsize: 127916
[startup+1130.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 9773
Raw data (stat): 9773 (minisat+) R 9772 28546 28545 0 -1 0 29294 0 0 0 112928 88 0 0 25 0 1 0 487734221 131256320 28893 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32045 28893 603 41 0 32004 0
vsize: 128180
[startup+1140.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 9773
Raw data (stat): 9773 (minisat+) R 9772 28546 28545 0 -1 0 29366 0 0 0 113928 88 0 0 25 0 1 0 487734221 131522560 28965 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32110 28965 603 41 0 32069 0
vsize: 128440
[startup+1150.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 9773
Raw data (stat): 9773 (minisat+) R 9772 28546 28545 0 -1 0 29439 0 0 0 114928 88 0 0 25 0 1 0 487734221 131788800 29038 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32175 29038 603 41 0 32134 0
vsize: 128700
[startup+1160.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 9773
Raw data (stat): 9773 (minisat+) R 9772 28546 28545 0 -1 0 29506 0 0 0 115928 88 0 0 25 0 1 0 487734221 132059136 29105 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32241 29105 603 41 0 32200 0
vsize: 128964
[startup+1170.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 9773
Raw data (stat): 9773 (minisat+) R 9772 28546 28545 0 -1 0 29590 0 0 0 116929 88 0 0 25 0 1 0 487734221 132497408 29189 4294967295 134512640 134672761 3221224576 3221223744 134560892 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32348 29189 603 41 0 32307 0
vsize: 129392
[startup+1180.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 9773
Raw data (stat): 9773 (minisat+) R 9772 28546 28545 0 -1 0 29664 0 0 0 117928 89 0 0 25 0 1 0 487734221 132870144 29263 4294967295 134512640 134672761 3221224576 3221223744 134561167 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32439 29263 603 41 0 32398 0
vsize: 129756
[startup+1190.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 9773
Raw data (stat): 9773 (minisat+) R 9772 28546 28545 0 -1 0 29717 0 0 0 118928 89 0 0 25 0 1 0 487734221 133115904 29316 4294967295 134512640 134672761 3221224576 3221223744 134560948 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32499 29316 603 41 0 32458 0
vsize: 129996
[startup+1200.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 9773
Raw data (stat): 9773 (minisat+) R 9772 28546 28545 0 -1 0 29782 0 0 0 119928 89 0 0 25 0 1 0 487734221 133312512 29381 4294967295 134512640 134672761 3221224576 3221223748 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32547 29381 603 41 0 32506 0
vsize: 130188
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.08 s]
Raw data (loadavg): 0.99 0.97 0.91 1/54 9773
Raw data (stat): 9773 (minisat+) Z 9772 28546 28545 0 -1 12 29784 0 0 0 119928 95 0 0 25 0 1 0 487734221 0 0 4294967295 0 0 0 0 0 0 16384 5 16386 3222412051 0 0 17 0 0 0
Raw data (statm): 0 0 0 0 0 0 0
vsize: 0
Maximum CPU time exceeded: sending SIGTERM and SIGKILL

Child status: 0
Real time (s): 1200.08
CPU time (s): 1200.24
CPU user time (s): 1199.29
CPU system time (s): 0.954854
CPU usage (%): 100.014
Max. virtual memory (Kb): 130188
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####