PB'05 competition: run trace

Some explanations

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

Name	normalized-opb/mps-v2-20-10/MIPLIB/miplib3/normalized-mps-v2-20-10-mitre.opb
MD5SUM	cb52c3dd346b4d656b5e715b686fba39
Bench Category	optimization, small integers (OPTSMALLINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	8401
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.27
Number of variables	10724
Total number of constraints	12778
Number of constraints which are clauses	140
Number of constraints which are cardinality constraints (but not clauses)	12255
Number of constraints which are nor clauses,nor cardinality constraints	383
Minimum length of a constraint	1
Maximum length of a constraint	98
Trace number 16378

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc3 THE 2005-04-21 07:04:18 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=13608 boxname=wulflinc3 idbench=1047 idsolver=10 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  cb52c3dd346b4d656b5e715b686fba39  /oldhome/oroussel/tmp/wulflinc3/normalized-mps-v2-20-10-mitre.opb
REAL COMMAND:  minisat+ -ca /oldhome/oroussel/tmp/wulflinc3/normalized-mps-v2-20-10-mitre.opb /oldhome/oroussel/tmp/wulflinc3/normalized-mps-v2-20-10-mitre.opb
IDLAUNCH: 13608
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.190
cache size	: 512 KB
fdiv_bug	: no
hlt_bug		: no
f00f_bug	: no
coma_bug	: no
fpu		: yes
fpu_exception	: yes
cpuid level	: 2
wp		: yes
flags		: fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse
bogomips	: 890.88

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.190
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:        409936 kB
Buffers:         34360 kB
Cached:         566568 kB
SwapCached:         56 kB
Active:         155768 kB
Inactive:       448008 kB
HighTotal:      131008 kB
HighFree:          252 kB
LowTotal:       903652 kB
LowFree:        409684 kB
SwapTotal:     2097136 kB
SwapFree:      2096992 kB
Dirty:              52 kB
Writeback:           0 kB
Mapped:           6840 kB
Slab:            15372 kB
Committed_AS:    71668 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1388 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-21 07:24:20 (client local time) WITH STATUS 0 IN 1200.22 SECONDS
stats: 13608 7 1200.22 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): .................................................................sssssssssssssssssssssss.ss.sss.s.sssssssssssssssssssssssssssssssssssssssssss.ssssss.sss.sssss.sssssssssss.ssss.ss...........................................................................
c ---[2147]---> Adder-cost: 190   maxlim: 87   bits: 7/7
c ---[2146]---> Adder-cost: 190   maxlim: 87   bits: 7/7
c ---[2145]---> Adder-cost: 30   maxlim: 13   bits: 5/4
c ---[2134]---> Adder-cost: 30   maxlim: 13   bits: 5/4
c ---[2123]---> Adder-cost: 30   maxlim: 13   bits: 5/4
c ---[2112]---> Adder-cost: 30   maxlim: 13   bits: 5/4
c ---[2104]---> Adder-cost: 30   maxlim: 13   bits: 5/4
c ---[2103]---> Adder-cost: 30   maxlim: 13   bits: 5/4
c ---[2102]---> Adder-cost: 30   maxlim: 13   bits: 5/4
c ---[2101]---> Adder-cost: 36   maxlim: 16   bits: 5/5
c ---[2100]---> Adder-cost: 36   maxlim: 16   bits: 5/5
c ---[2099]---> Adder-cost: 36   maxlim: 16   bits: 5/5
c ---[2098]---> Adder-cost: 36   maxlim: 16   bits: 5/5
c ---[2097]---> Adder-cost: 36   maxlim: 16   bits: 5/5
c ---[2096]---> Adder-cost: 30   maxlim: 13   bits: 5/4
c ---[2095]---> Adder-cost: 36   maxlim: 16   bits: 5/5
c ---[2094]---> Adder-cost: 36   maxlim: 16   bits: 5/5
c ---[2093]---> Adder-cost: 36   maxlim: 16   bits: 5/5
c ---[2092]---> Adder-cost: 36   maxlim: 16   bits: 5/5
c ---[2091]---> Adder-cost: 36   maxlim: 16   bits: 5/5
c ---[2090]---> Adder-cost: 36   maxlim: 16   bits: 5/5
c ---[2089]---> Adder-cost: 36   maxlim: 16   bits: 5/5
c ---[2088]---> Adder-cost: 36   maxlim: 16   bits: 5/5
c ---[2087]---> Adder-cost: 36   maxlim: 16   bits: 5/5
c ---[2086]---> Adder-cost: 36   maxlim: 16   bits: 5/5
c ---[2085]---> Adder-cost: 30   maxlim: 13   bits: 5/4
c ---[2084]---> Adder-cost: 36   maxlim: 16   bits: 5/5
c ---[2083]---> Adder-cost: 36   maxlim: 16   bits: 5/5
c ---[2082]---> Adder-cost: 36   maxlim: 16   bits: 5/5
c ---[2081]---> Adder-cost: 36   maxlim: 16   bits: 5/5
c ---[2080]---> Adder-cost: 36   maxlim: 16   bits: 5/5
c ---[2079]---> Adder-cost: 36   maxlim: 16   bits: 5/5
c ---[2078]---> Adder-cost: 36   maxlim: 16   bits: 5/5
c ---[2077]---> Adder-cost: 36   maxlim: 16   bits: 5/5
c ---[2076]---> Adder-cost: 36   maxlim: 16   bits: 5/5
c ---[2075]---> Adder-cost: 36   maxlim: 16   bits: 5/5
c ---[2074]---> Adder-cost: 30   maxlim: 13   bits: 5/4
c ---[2073]---> Adder-cost: 36   maxlim: 16   bits: 5/5
c ---[2072]---> Adder-cost: 36   maxlim: 16   bits: 5/5
c ---[2071]---> Adder-cost: 36   maxlim: 16   bits: 5/5
c ---[2070]---> Adder-cost: 190   maxlim: 87   bits: 7/7
c ---[2069]---> Adder-cost: 30   maxlim: 13   bits: 5/4
c ---[2068]---> Adder-cost: 30   maxlim: 13   bits: 5/4
c ---[2067]---> Adder-cost: 30   maxlim: 13   bits: 5/4
c ---[2066]---> Adder-cost: 16   maxlim: 8   bits: 4/4
c ---[2065]---> Adder-cost: 16   maxlim: 8   bits: 4/4
c ---[2064]---> Adder-cost: 16   maxlim: 8   bits: 4/4
c ---[2063]---> Adder-cost: 16   maxlim: 8   bits: 4/4
c ---[2062]---> Adder-cost: 16   maxlim: 8   bits: 4/4
c ---[2061]---> Adder-cost: 16   maxlim: 8   bits: 4/4
c ---[2060]---> Adder-cost: 16   maxlim: 8   bits: 4/4
c ---[2059]---> Adder-cost: 16   maxlim: 8   bits: 4/4
c ---[2058]---> Adder-cost: 16   maxlim: 8   bits: 4/4
c ---[2057]---> Adder-cost: 16   maxlim: 8   bits: 4/4
c ---[2056]---> Adder-cost: 16   maxlim: 8   bits: 4/4
c ---[2055]---> Adder-cost: 16   maxlim: 8   bits: 4/4
c ---[2054]---> Adder-cost: 16   maxlim: 8   bits: 4/4
c ---[2053]---> Adder-cost: 16   maxlim: 8   bits: 4/4
c ---[2052]---> Adder-cost: 16   maxlim: 8   bits: 4/4
c ---[2051]---> Adder-cost: 16   maxlim: 8   bits: 4/4
c ---[2050]---> Adder-cost: 16   maxlim: 8   bits: 4/4
c ---[2049]---> Adder-cost: 16   maxlim: 8   bits: 4/4
c ---[2048]---> Adder-cost: 16   maxlim: 8   bits: 4/4
c ---[2047]---> Adder-cost: 16   maxlim: 8   bits: 4/4
c ---[2046]---> Adder-cost: 16   maxlim: 8   bits: 4/4
c ---[2045]---> Adder-cost: 16   maxlim: 8   bits: 4/4
c ---[2044]---> Adder-cost: 16   maxlim: 8   bits: 4/4
c ---[2043]---> Adder-cost: 16   maxlim: 8   bits: 4/4
c ---[2042]---> Adder-cost: 16   maxlim: 8   bits: 4/4
c ---[2041]---> Adder-cost: 16   maxlim: 8   bits: 4/4
c ---[2040]---> Adder-cost: 16   maxlim: 8   bits: 4/4
c ---[2039]---> Adder-cost: 16   maxlim: 8   bits: 4/4
c ---[2038]---> Adder-cost: 5   maxlim: 1   bits: 2/1
c ---[2037]---> Adder-cost: 5   maxlim: 1   bits: 2/1
c ---[2036]---> 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 ---[2032]---> Adder-cost: 5   maxlim: 1   bits: 2/1
c ---[2031]---> Adder-cost: 5   maxlim: 1   bits: 2/1
c ---[2030]---> Adder-cost: 5   maxlim: 1   bits: 2/1
c ---[2029]---> Adder-cost: 5   maxlim: 1   bits: 2/1
c ---[2028]---> Adder-cost: 5   maxlim: 1   bits: 2/1
c ---[2027]---> Adder-cost: 5   maxlim: 1   bits: 2/1
c ---[2026]---> Adder-cost: 5   maxlim: 1   bits: 2/1
c ---[2025]---> Adder-cost: 5   maxlim: 1   bits: 2/1
c ---[2024]---> Adder-cost: 5   maxlim: 1   bits: 2/1
c ---[2023]---> Adder-cost: 5   maxlim: 1   bits: 2/1
c ---[2022]---> Adder-cost: 5   maxlim: 1   bits: 2/1
c ---[2021]---> Adder-cost: 5   maxlim: 1   bits: 2/1
c ---[2020]---> Adder-cost: 5   maxlim: 1   bits: 2/1
c ---[2019]---> Adder-cost: 5   maxlim: 1   bits: 2/1
c ---[2018]---> Adder-cost: 5   maxlim: 1   bits: 2/1
c ---[2017]---> Adder-cost: 5   maxlim: 1   bits: 2/1
c ---[2016]---> Adder-cost: 5   maxlim: 1   bits: 2/1
c ---[2015]---> Adder-cost: 190   maxlim: 87   bits: 7/7
c ---[2014]---> Adder-cost: 5   maxlim: 1   bits: 2/1
c ---[2013]---> Adder-cost: 5   maxlim: 1   bits: 2/1
c ---[2012]---> Adder-cost: 5   maxlim: 1   bits: 2/1
c ---[2011]---> Adder-cost: 5   maxlim: 1   bits: 2/1
c ---[2010]---> Adder-cost: 5   maxlim: 1   bits: 2/1
c ---[1981]---> Adder-cost: 368   maxlim: 1611   bits: 12/11
c ---[1980]---> Adder-cost: 368   maxlim: 1612   bits: 12/11
c ---[1979]---> Adder-cost: 368   maxlim: 1611   bits: 12/11
c ---[1978]---> Adder-cost: 368   maxlim: 1612   bits: 12/11
c ---[1977]---> Adder-cost: 368   maxlim: 1611   bits: 12/11
c ---[1976]---> Adder-cost: 368   maxlim: 1613   bits: 12/11
c ---[1975]---> Adder-cost: 368   maxlim: 1612   bits: 12/11
c ---[1974]---> Adder-cost: 368   maxlim: 1611   bits: 12/11
c ---[1973]---> Adder-cost: 368   maxlim: 1611   bits: 12/11
c ---[1972]---> Adder-cost: 368   maxlim: 1613   bits: 12/11
c ---[1971]---> Adder-cost: 368   maxlim: 1613   bits: 12/11
c ---[1970]---> Adder-cost: 190   maxlim: 87   bits: 7/7
c ---[1969]---> Adder-cost: 368   maxlim: 1612   bits: 12/11
c ---[1968]---> Adder-cost: 544   maxlim: 24180   bits: 16/15
c ---[1967]---> Adder-cost: 544   maxlim: 24195   bits: 16/15
c ---[1966]---> Adder-cost: 552   maxlim: 24196   bits: 16/15
c ---[1965]---> Adder-cost: 552   maxlim: 24211   bits: 16/15
c ---[1964]---> Adder-cost: 368   maxlim: 1611   bits: 12/11
c ---[1963]---> Adder-cost: 368   maxlim: 1611   bits: 12/11
c ---[1962]---> Adder-cost: 368   maxlim: 1614   bits: 12/11
c ---[1961]---> Adder-cost: 368   maxlim: 1612   bits: 12/11
c ---[1960]---> Adder-cost: 368   maxlim: 1612   bits: 12/11
c ---[1959]---> Adder-cost: 368   maxlim: 1612   bits: 12/11
c ---[1958]---> Adder-cost: 368   maxlim: 1612   bits: 12/11
c ---[1957]---> Adder-cost: 368   maxlim: 1610   bits: 12/11
c ---[1956]---> Adder-cost: 368   maxlim: 1615   bits: 12/11
c ---[1955]---> Adder-cost: 368   maxlim: 1611   bits: 12/11
c ---[1954]---> Adder-cost: 368   maxlim: 1611   bits: 12/11
c ---[1953]---> Adder-cost: 368   maxlim: 1611   bits: 12/11
c ---[1952]---> Adder-cost: 368   maxlim: 1610   bits: 12/11
c ---[1951]---> Adder-cost: 368   maxlim: 1611   bits: 12/11
c ---[1950]---> Adder-cost: 368   maxlim: 1611   bits: 12/11
c ---[1949]---> Adder-cost: 368   maxlim: 1612   bits: 12/11
c ---[1948]---> Adder-cost: 368   maxlim: 1611   bits: 12/11
c ---[1947]---> Adder-cost: 368   maxlim: 1611   bits: 12/11
c ---[1946]---> Adder-cost: 368   maxlim: 1612   bits: 12/11
c ---[1945]---> Adder-cost: 368   maxlim: 1611   bits: 12/11
c ---[1944]---> Adder-cost: 368   maxlim: 1611   bits: 12/11
c ---[1943]---> Adder-cost: 368   maxlim: 1612   bits: 12/11
c ---[1942]---> Adder-cost: 368   maxlim: 1610   bits: 12/11
c ---[1941]---> Adder-cost: 448   maxlim: 8068   bits: 14/13
c ---[1940]---> Adder-cost: 448   maxlim: 8073   bits: 14/13
c ---[1939]---> Adder-cost: 368   maxlim: 1614   bits: 12/11
c ---[1938]---> Adder-cost: 368   maxlim: 1611   bits: 12/11
c ---[1937]---> Adder-cost: 368   maxlim: 1611   bits: 12/11
c ---[1936]---> Adder-cost: 368   maxlim: 1611   bits: 12/11
c ---[1935]---> Adder-cost: 368   maxlim: 1612   bits: 12/11
c ---[1934]---> Adder-cost: 546   maxlim: 24195   bits: 16/15
c ---[1933]---> Adder-cost: 368   maxlim: 1612   bits: 12/11
c ---[1932]---> Adder-cost: 368   maxlim: 1611   bits: 12/11
c ---[1931]---> Adder-cost: 368   maxlim: 1613   bits: 12/11
c ---[1930]---> Adder-cost: 368   maxlim: 1612   bits: 12/11
c ---[1929]---> Adder-cost: 368   maxlim: 1611   bits: 12/11
c ---[1928]---> Adder-cost: 368   maxlim: 1613   bits: 12/11
c ---[1927]---> Adder-cost: 368   maxlim: 1614   bits: 12/11
c ---[1926]---> Adder-cost: 368   maxlim: 1612   bits: 12/11
c ---[1925]---> Adder-cost: 368   maxlim: 1613   bits: 12/11
c ---[1924]---> Adder-cost: 368   maxlim: 1614   bits: 12/11
c ---[1923]---> Adder-cost: 368   maxlim: 1611   bits: 12/11
c ---[1922]---> Adder-cost: 368   maxlim: 1612   bits: 12/11
c ---[1921]---> Adder-cost: 368   maxlim: 1612   bits: 12/11
c ---[1920]---> Adder-cost: 368   maxlim: 1611   bits: 12/11
c ---[1919]---> Adder-cost: 368   maxlim: 1612   bits: 12/11
c ---[1918]---> Adder-cost: 368   maxlim: 1612   bits: 12/11
c ---[1917]---> Adder-cost: 368   maxlim: 1616   bits: 12/11
c ---[1916]---> Adder-cost: 368   maxlim: 1610   bits: 12/11
c ---[1915]---> Adder-cost: 368   maxlim: 1611   bits: 12/11
c ---[1914]---> Adder-cost: 368   maxlim: 1612   bits: 12/11
c ---[1913]---> Adder-cost: 368   maxlim: 1611   bits: 12/11
c ---[1912]---> Adder-cost: 368   maxlim: 1611   bits: 12/11
c ---[1911]---> Adder-cost: 368   maxlim: 1614   bits: 12/11
c ---[1910]---> Adder-cost: 368   maxlim: 1612   bits: 12/11
c ---[1909]---> Adder-cost: 368   maxlim: 1616   bits: 12/11
c ---[1908]---> Adder-cost: 368   maxlim: 1610   bits: 12/11
c ---[1907]---> Adder-cost: 368   maxlim: 1616   bits: 12/11
c ---[1906]---> Adder-cost: 368   maxlim: 1610   bits: 12/11
c ---[1905]---> Adder-cost: 368   maxlim: 1613   bits: 12/11
c ---[1904]---> Adder-cost: 368   maxlim: 1612   bits: 12/11
c ---[1903]---> Adder-cost: 368   maxlim: 1611   bits: 12/11
c ---[1902]---> Adder-cost: 368   maxlim: 1611   bits: 12/11
c ---[1901]---> Adder-cost: 368   maxlim: 1613   bits: 12/11
c ---[1900]---> Adder-cost: 368   maxlim: 1611   bits: 12/11
c ---[1899]---> Adder-cost: 368   maxlim: 1614   bits: 12/11
c ---[1898]---> Adder-cost: 368   maxlim: 1613   bits: 12/11
c ---[1897]---> Adder-cost: 368   maxlim: 1613   bits: 12/11
c ---[1896]---> Adder-cost: 368   maxlim: 1614   bits: 12/11
c ---[1895]---> Adder-cost: 368   maxlim: 1612   bits: 12/11
c ---[1894]---> Adder-cost: 368   maxlim: 1611   bits: 12/11
c ---[1893]---> Adder-cost: 368   maxlim: 1612   bits: 12/11
c ---[1892]---> Adder-cost: 368   maxlim: 1610   bits: 12/11
c ---[1891]---> Adder-cost: 368   maxlim: 1612   bits: 12/11
c ---[1890]---> Adder-cost: 368   maxlim: 1611   bits: 12/11
c ---[1889]---> Adder-cost: 368   maxlim: 1612   bits: 12/11
c ---[1888]---> Adder-cost: 368   maxlim: 1611   bits: 12/11
c ---[1887]---> Adder-cost: 368   maxlim: 1613   bits: 12/11
c ---[1886]---> Adder-cost: 368   maxlim: 1616   bits: 12/11
c ---[1885]---> Adder-cost: 368   maxlim: 1611   bits: 12/11
c ---[1884]---> Adder-cost: 368   maxlim: 1611   bits: 12/11
c ---[1883]---> Adder-cost: 368   maxlim: 1612   bits: 12/11
c ---[1882]---> Adder-cost: 368   maxlim: 1611   bits: 12/11
c ---[1881]---> Adder-cost: 368   maxlim: 1612   bits: 12/11
c ---[1880]---> Adder-cost: 368   maxlim: 1611   bits: 12/11
c ---[1879]---> Adder-cost: 368   maxlim: 1611   bits: 12/11
c ---[1878]---> Adder-cost: 368   maxlim: 1612   bits: 12/11
c ---[1877]---> Adder-cost: 368   maxlim: 1611   bits: 12/11
c ---[1876]---> Adder-cost: 368   maxlim: 1611   bits: 12/11
c ---[1875]---> Adder-cost: 368   maxlim: 1611   bits: 12/11
c ---[1874]---> Adder-cost: 368   maxlim: 1612   bits: 12/11
c ---[1873]---> Adder-cost: 368   maxlim: 1612   bits: 12/11
c ---[1872]---> Adder-cost: 368   maxlim: 1613   bits: 12/11
c ---[1871]---> Adder-cost: 368   maxlim: 1613   bits: 12/11
c ---[1870]---> Adder-cost: 462   maxlim: 8078   bits: 14/13
c ---[1869]---> Adder-cost: 190   maxlim: 87   bits: 7/7
c ---[1868]---> Adder-cost: 462   maxlim: 8083   bits: 14/13
c ---[1867]---> Adder-cost: 368   maxlim: 1611   bits: 12/11
c ---[1866]---> Adder-cost: 368   maxlim: 1612   bits: 12/11
c ---[1865]---> Adder-cost: 368   maxlim: 1611   bits: 12/11
c ---[1864]---> Adder-cost: 368   maxlim: 1611   bits: 12/11
c ---[1863]---> Adder-cost: 368   maxlim: 1612   bits: 12/11
c ---[1862]---> Adder-cost: 368   maxlim: 1611   bits: 12/11
c ---[1861]---> Adder-cost: 368   maxlim: 1611   bits: 12/11
c ---[1860]---> Adder-cost: 368   maxlim: 1612   bits: 12/11
c ---[1859]---> Adder-cost: 368   maxlim: 1611   bits: 12/11
c ---[1858]---> Adder-cost: 14   maxlim: 6   bits: 4/3
c ---[1857]---> Adder-cost: 368   maxlim: 1611   bits: 12/11
c ---[1856]---> Adder-cost: 368   maxlim: 1612   bits: 12/11
c ---[1855]---> Adder-cost: 368   maxlim: 1611   bits: 12/11
c ---[1854]---> Adder-cost: 368   maxlim: 1612   bits: 12/11
c ---[1853]---> Adder-cost: 368   maxlim: 1611   bits: 12/11
c ---[1852]---> Adder-cost: 368   maxlim: 1611   bits: 12/11
c ---[1851]---> Adder-cost: 368   maxlim: 1611   bits: 12/11
c ---[1850]---> Adder-cost: 368   maxlim: 1614   bits: 12/11
c ---[1849]---> Adder-cost: 368   maxlim: 1611   bits: 12/11
c ---[1848]---> Adder-cost: 368   maxlim: 1612   bits: 12/11
c ---[1847]---> Adder-cost: 14   maxlim: 6   bits: 4/3
c ---[1846]---> Adder-cost: 368   maxlim: 1610   bits: 12/11
c ---[1845]---> Adder-cost: 368   maxlim: 1611   bits: 12/11
c ---[1844]---> Adder-cost: 368   maxlim: 1612   bits: 12/11
c ---[1843]---> Adder-cost: 368   maxlim: 1612   bits: 12/11
c ---[1842]---> Adder-cost: 368   maxlim: 1611   bits: 12/11
c ---[1841]---> Adder-cost: 368   maxlim: 1612   bits: 12/11
c ---[1840]---> Adder-cost: 368   maxlim: 1611   bits: 12/11
c ---[1839]---> Adder-cost: 368   maxlim: 1613   bits: 12/11
c ---[1838]---> Adder-cost: 368   maxlim: 1612   bits: 12/11
c ---[1837]---> Adder-cost: 536   maxlim: 24232   bits: 16/15
c ---[1836]---> Adder-cost: 14   maxlim: 6   bits: 4/3
c ---[1835]---> Adder-cost: 536   maxlim: 24247   bits: 16/15
c ---[1834]---> Adder-cost: 368   maxlim: 1611   bits: 12/11
c ---[1833]---> Adder-cost: 368   maxlim: 1612   bits: 12/11
c ---[1832]---> Adder-cost: 368   maxlim: 1610   bits: 12/11
c ---[1831]---> Adder-cost: 424   maxlim: 4849   bits: 14/13
c ---[1830]---> Adder-cost: 424   maxlim: 4852   bits: 14/13
c ---[1829]---> Adder-cost: 552   maxlim: 24190   bits: 16/15
c ---[1828]---> Adder-cost: 552   maxlim: 24205   bits: 16/15
c ---[1827]---> Adder-cost: 552   maxlim: 24190   bits: 16/15
c ---[1826]---> Adder-cost: 368   maxlim: 1613   bits: 12/11
c ---[1825]---> Adder-cost: 14   maxlim: 6   bits: 4/3
c ---[1824]---> Adder-cost: 368   maxlim: 1610   bits: 12/11
c ---[1823]---> Adder-cost: 368   maxlim: 1611   bits: 12/11
c ---[1822]---> Adder-cost: 368   maxlim: 1613   bits: 12/11
c ---[1821]---> Adder-cost: 368   maxlim: 1610   bits: 12/11
c ---[1820]---> Adder-cost: 368   maxlim: 1611   bits: 12/11
c ---[1819]---> Adder-cost: 368   maxlim: 1612   bits: 12/11
c ---[1818]---> Adder-cost: 368   maxlim: 1613   bits: 12/11
c ---[1817]---> Adder-cost: 368   maxlim: 1611   bits: 12/11
c ---[1816]---> Adder-cost: 368   maxlim: 1610   bits: 12/11
c ---[1815]---> Adder-cost: 368   maxlim: 1611   bits: 12/11
c ---[1814]---> Adder-cost: 14   maxlim: 6   bits: 4/3
c ---[1813]---> Adder-cost: 368   maxlim: 1614   bits: 12/11
c ---[1812]---> Adder-cost: 368   maxlim: 1611   bits: 12/11
c ---[1811]---> Adder-cost: 368   maxlim: 1611   bits: 12/11
c ---[1810]---> Adder-cost: 448   maxlim: 8063   bits: 14/13
c ---[1809]---> Adder-cost: 448   maxlim: 8068   bits: 14/13
c ---[1808]---> Adder-cost: 368   maxlim: 1611   bits: 12/11
c ---[1807]---> Adder-cost: 368   maxlim: 1610   bits: 12/11
c ---[1806]---> Adder-cost: 368   maxlim: 1610   bits: 12/11
c ---[1805]---> Adder-cost: 368   maxlim: 1611   bits: 12/11
c ---[1804]---> Adder-cost: 368   maxlim: 1610   bits: 12/11
c ---[1803]---> Adder-cost: 14   maxlim: 6   bits: 4/3
c ---[1802]---> Adder-cost: 368   maxlim: 1611   bits: 12/11
c ---[1801]---> Adder-cost: 368   maxlim: 1611   bits: 12/11
c ---[1800]---> Adder-cost: 368   maxlim: 1614   bits: 12/11
c ---[1799]---> Adder-cost: 368   maxlim: 1613   bits: 12/11
c ---[1798]---> Adder-cost: 368   maxlim: 1612   bits: 12/11
c ---[1797]---> Adder-cost: 368   maxlim: 1611   bits: 12/11
c ---[1796]---> Adder-cost: 368   maxlim: 1610   bits: 12/11
c ---[1795]---> Adder-cost: 368   maxlim: 1611   bits: 12/11
c ---[1794]---> Adder-cost: 368   maxlim: 1611   bits: 12/11
c ---[1793]---> Adder-cost: 368   maxlim: 1611   bits: 12/11
c ---[1792]---> Adder-cost: 14   maxlim: 6   bits: 4/3
c ---[1791]---> Adder-cost: 368   maxlim: 1610   bits: 12/11
c ---[1790]---> Adder-cost: 368   maxlim: 1614   bits: 12/11
c ---[1789]---> Adder-cost: 368   maxlim: 1612   bits: 12/11
c ---[1788]---> Adder-cost: 368   maxlim: 1611   bits: 12/11
c ---[1787]---> Adder-cost: 368   maxlim: 1613   bits: 12/11
c ---[1786]---> Adder-cost: 368   maxlim: 1612   bits: 12/11
c ---[1785]---> Adder-cost: 368   maxlim: 1611   bits: 12/11
c ---[1784]---> Adder-cost: 368   maxlim: 1612   bits: 12/11
c ---[1783]---> Adder-cost: 368   maxlim: 1611   bits: 12/11
c ---[1782]---> Adder-cost: 368   maxlim: 1611   bits: 12/11
c ---[1781]---> Adder-cost: 14   maxlim: 6   bits: 4/3
c ---[1780]---> Adder-cost: 368   maxlim: 1612   bits: 12/11
c ---[1779]---> Adder-cost: 368   maxlim: 1611   bits: 12/11
c ---[1778]---> Adder-cost: 368   maxlim: 1611   bits: 12/11
c ---[1777]---> Adder-cost: 552   maxlim: 24190   bits: 16/15
c ---[1776]---> Adder-cost: 552   maxlim: 24205   bits: 16/15
c ---[1775]---> Adder-cost: 552   maxlim: 24190   bits: 16/15
c ---[1774]---> Adder-cost: 368   maxlim: 1613   bits: 12/11
c ---[1773]---> Adder-cost: 368   maxlim: 1610   bits: 12/11
c ---[1772]---> Adder-cost: 368   maxlim: 1611   bits: 12/11
c ---[1771]---> Adder-cost: 552   maxlim: 24190   bits: 16/15
c ---[1770]---> Adder-cost: 14   maxlim: 6   bits: 4/3
c ---[1769]---> Adder-cost: 552   maxlim: 24205   bits: 16/15
c ---[1768]---> Adder-cost: 552   maxlim: 24190   bits: 16/15
c ---[1767]---> Adder-cost: 368   maxlim: 1613   bits: 12/11
c ---[1766]---> Adder-cost: 368   maxlim: 1610   bits: 12/11
c ---[1765]---> Adder-cost: 368   maxlim: 1611   bits: 12/11
c ---[1764]---> Adder-cost: 368   maxlim: 1611   bits: 12/11
c ---[1763]---> Adder-cost: 368   maxlim: 1612   bits: 12/11
c ---[1762]---> Adder-cost: 368   maxlim: 1610   bits: 12/11
c ---[1761]---> Adder-cost: 368   maxlim: 1611   bits: 12/11
c ---[1760]---> Adder-cost: 368   maxlim: 1614   bits: 12/11
c ---[1759]---> Adder-cost: 190   maxlim: 87   bits: 7/7
c ---[1758]---> Adder-cost: 14   maxlim: 6   bits: 4/3
c ---[1757]---> Adder-cost: 368   maxlim: 1611   bits: 12/11
c ---[1756]---> Adder-cost: 368   maxlim: 1612   bits: 12/11
c ---[1755]---> Adder-cost: 368   maxlim: 1610   bits: 12/11
c ---[1754]---> Adder-cost: 368   maxlim: 1611   bits: 12/11
c ---[1753]---> Adder-cost: 368   maxlim: 1614   bits: 12/11
c ---[1752]---> Adder-cost: 368   maxlim: 1610   bits: 12/11
c ---[1751]---> Adder-cost: 368   maxlim: 1611   bits: 12/11
c ---[1750]---> Adder-cost: 368   maxlim: 1611   bits: 12/11
c ---[1749]---> Adder-cost: 368   maxlim: 1615   bits: 12/11
c ---[1748]---> Adder-cost: 368   maxlim: 1611   bits: 12/11
c ---[1747]---> Adder-cost: 14   maxlim: 6   bits: 4/3
c ---[1746]---> Adder-cost: 368   maxlim: 1611   bits: 12/11
c ---[1745]---> Adder-cost: 368   maxlim: 1612   bits: 12/11
c ---[1744]---> Adder-cost: 368   maxlim: 1612   bits: 12/11
c ---[1743]---> Adder-cost: 368   maxlim: 1612   bits: 12/11
c ---[1742]---> Adder-cost: 368   maxlim: 1612   bits: 12/11
c ---[1741]---> Adder-cost: 368   maxlim: 1611   bits: 12/11
c ---[1740]---> Adder-cost: 368   maxlim: 1612   bits: 12/11
c ---[1739]---> Adder-cost: 368   maxlim: 1611   bits: 12/11
c ---[1738]---> Adder-cost: 552   maxlim: 24211   bits: 16/15
c ---[1737]---> Adder-cost: 552   maxlim: 24196   bits: 16/15
c ---[1736]---> Adder-cost: 14   maxlim: 6   bits: 4/3
c ---[1735]---> Adder-cost: 368   maxlim: 1611   bits: 12/11
c ---[1734]---> Adder-cost: 368   maxlim: 1613   bits: 12/11
c ---[1733]---> Adder-cost: 368   maxlim: 1611   bits: 12/11
c ---[1732]---> Adder-cost: 368   maxlim: 1612   bits: 12/11
c ---[1731]---> Adder-cost: 368   maxlim: 1611   bits: 12/11
c ---[1730]---> Adder-cost: 368   maxlim: 1611   bits: 12/11
c ---[1729]---> Adder-cost: 368   maxlim: 1613   bits: 12/11
c ---[1728]---> Adder-cost: 368   maxlim: 1611   bits: 12/11
c ---[1727]---> Adder-cost: 368   maxlim: 1612   bits: 12/11
c ---[1726]---> Adder-cost: 368   maxlim: 1610   bits: 12/11
c ---[1725]---> Adder-cost: 14   maxlim: 6   bits: 4/3
c ---[1724]---> Adder-cost: 368   maxlim: 1611   bits: 12/11
c ---[1723]---> Adder-cost: 368   maxlim: 1612   bits: 12/11
c ---[1722]---> Adder-cost: 368   maxlim: 1610   bits: 12/11
c ---[1721]---> Adder-cost: 368   maxlim: 1611   bits: 12/11
c ---[1720]---> Adder-cost: 368   maxlim: 1612   bits: 12/11
c ---[1719]---> Adder-cost: 368   maxlim: 1611   bits: 12/11
c ---[1718]---> Adder-cost: 368   maxlim: 1611   bits: 12/11
c ---[1717]---> Adder-cost: 368   maxlim: 1611   bits: 12/11
c ---[1716]---> Adder-cost: 368   maxlim: 1613   bits: 12/11
c ---[1715]---> Adder-cost: 368   maxlim: 1611   bits: 12/11
c ---[1714]---> Adder-cost: 14   maxlim: 6   bits: 4/3
c ---[1713]---> Adder-cost: 368   maxlim: 1611   bits: 12/11
c ---[1712]---> Adder-cost: 368   maxlim: 1611   bits: 12/11
c ---[1711]---> Adder-cost: 368   maxlim: 1611   bits: 12/11
c ---[1710]---> Adder-cost: 368   maxlim: 1610   bits: 12/11
c ---[1709]---> Adder-cost: 368   maxlim: 1612   bits: 12/11
c ---[1708]---> Adder-cost: 368   maxlim: 1612   bits: 12/11
c ---[1707]---> Adder-cost: 368   maxlim: 1612   bits: 12/11
c ---[1706]---> Adder-cost: 368   maxlim: 1614   bits: 12/11
c ---[1705]---> Adder-cost: 368   maxlim: 1610   bits: 12/11
c ---[1704]---> Adder-cost: 368   maxlim: 1611   bits: 12/11
c ---[1703]---> Adder-cost: 14   maxlim: 6   bits: 4/3
c ---[1702]---> Adder-cost: 368   maxlim: 1610   bits: 12/11
c ---[1701]---> Adder-cost: 368   maxlim: 1611   bits: 12/11
c ---[1700]---> Adder-cost: 368   maxlim: 1611   bits: 12/11
c ---[1699]---> Adder-cost: 368   maxlim: 1612   bits: 12/11
c ---[1698]---> Adder-cost: 368   maxlim: 1611   bits: 12/11
c ---[1697]---> Adder-cost: 546   maxlim: 24195   bits: 16/15
c ---[1696]---> Adder-cost: 546   maxlim: 24195   bits: 16/15
c ---[1695]---> Adder-cost: 368   maxlim: 1610   bits: 12/11
c ---[1694]---> Adder-cost: 368   maxlim: 1611   bits: 12/11
c ---[1692]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1691]---> Adder-cost: 14   maxlim: 6   bits: 4/3
c ---[1689]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1687]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1685]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1683]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1681]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1679]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1677]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1675]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1673]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1671]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1670]---> Adder-cost: 14   maxlim: 6   bits: 4/3
c ---[1668]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1666]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1664]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1662]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1660]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1658]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1656]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1654]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1652]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1650]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1649]---> Adder-cost: 14   maxlim: 6   bits: 4/3
c ---[1647]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1645]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1643]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1641]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1639]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1637]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1635]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1633]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1631]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1629]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1628]---> Adder-cost: 14   maxlim: 6   bits: 4/3
c ---[1626]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1624]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1622]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1620]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1618]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1616]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1614]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1612]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1610]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1608]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1607]---> Adder-cost: 190   maxlim: 87   bits: 7/7
c ---[1606]---> Adder-cost: 14   maxlim: 6   bits: 4/3
c ---[1604]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1602]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1600]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1598]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1596]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1594]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1592]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1590]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1588]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1586]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1585]---> Adder-cost: 14   maxlim: 6   bits: 4/3
c ---[1583]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1581]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1579]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1577]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1575]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1573]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1571]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1569]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1567]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1565]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1564]---> Adder-cost: 14   maxlim: 6   bits: 4/3
c ---[1562]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1560]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1558]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1556]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1554]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1552]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1550]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1548]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1546]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1544]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1543]---> Adder-cost: 14   maxlim: 6   bits: 4/3
c ---[1541]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1539]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1537]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1535]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1533]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1531]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1529]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1527]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1525]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1523]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1522]---> Adder-cost: 14   maxlim: 6   bits: 4/3
c ---[1520]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1518]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1516]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1514]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1512]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1510]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1508]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1506]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1504]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1502]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1501]---> Adder-cost: 14   maxlim: 6   bits: 4/3
c ---[1499]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1497]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1495]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1493]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1491]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1489]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1487]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1485]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1483]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1481]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1480]---> Adder-cost: 14   maxlim: 6   bits: 4/3
c ---[1478]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1476]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1474]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1472]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1470]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1468]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1466]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1464]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1462]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1460]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1459]---> Adder-cost: 14   maxlim: 6   bits: 4/3
c ---[1457]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1455]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1453]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1451]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1449]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1447]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1445]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1443]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1441]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1439]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1438]---> Adder-cost: 14   maxlim: 6   bits: 4/3
c ---[1436]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1434]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1432]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1430]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1428]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1426]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1424]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1422]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1420]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1418]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1417]---> Adder-cost: 16   maxlim: 7   bits: 4/3
c ---[1415]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1413]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1411]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1409]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1407]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1405]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1403]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1401]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1399]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1397]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1396]---> Adder-cost: 190   maxlim: 87   bits: 7/7
c ---[1395]---> Adder-cost: 16   maxlim: 7   bits: 4/3
c ---[1393]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1391]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1389]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1387]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1385]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1383]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1381]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1379]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1377]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1375]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1374]---> Adder-cost: 16   maxlim: 7   bits: 4/3
c ---[1372]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1370]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1368]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1366]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1364]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1362]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1360]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1358]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1356]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1354]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1353]---> Adder-cost: 16   maxlim: 7   bits: 4/3
c ---[1351]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1349]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1347]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1345]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1343]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1341]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1339]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1337]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1335]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1333]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1332]---> Adder-cost: 16   maxlim: 7   bits: 4/3
c ---[1330]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1328]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1326]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1324]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1322]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1320]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1318]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1316]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1314]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1312]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1311]---> Adder-cost: 16   maxlim: 7   bits: 4/3
c ---[1309]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1307]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1305]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1303]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1301]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1299]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1297]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1295]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1293]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1291]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1290]---> Adder-cost: 16   maxlim: 7   bits: 4/3
c ---[1288]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1286]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1284]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1282]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1280]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1278]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1276]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1274]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1272]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1270]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1269]---> Adder-cost: 16   maxlim: 7   bits: 4/3
c ---[1267]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1265]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1263]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1261]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1259]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1257]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1255]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1253]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1251]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1249]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1248]---> Adder-cost: 16   maxlim: 7   bits: 4/3
c ---[1246]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1244]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1242]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1240]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1238]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1236]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1234]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1232]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1230]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1228]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1227]---> Adder-cost: 16   maxlim: 7   bits: 4/3
c ---[1225]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1223]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1221]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1219]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1217]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1215]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1213]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1211]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1209]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1207]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1206]---> Adder-cost: 16   maxlim: 7   bits: 4/3
c ---[1204]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1202]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1200]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1198]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1196]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1194]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1192]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1190]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1188]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1186]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1185]---> Adder-cost: 190   maxlim: 87   bits: 7/7
c ---[1184]---> Adder-cost: 16   maxlim: 7   bits: 4/3
c ---[1182]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1180]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1178]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1176]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1174]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1172]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1170]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1168]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1166]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1164]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1163]---> Adder-cost: 16   maxlim: 7   bits: 4/3
c ---[1161]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1159]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1157]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1155]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1153]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1151]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1149]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1147]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1145]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1143]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1142]---> Adder-cost: 16   maxlim: 7   bits: 4/3
c ---[1140]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1138]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1136]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1134]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1132]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1130]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1128]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1126]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1124]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1122]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1121]---> Adder-cost: 16   maxlim: 7   bits: 4/3
c ---[1119]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1117]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1115]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1113]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1111]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1109]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1107]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1105]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1103]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1101]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1100]---> Adder-cost: 16   maxlim: 7   bits: 4/3
c ---[1098]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1096]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1094]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1092]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1090]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1088]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1086]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1084]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1082]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1080]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1079]---> Adder-cost: 16   maxlim: 7   bits: 4/3
c ---[1077]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1075]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1073]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1071]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1069]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1067]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1065]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1063]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1061]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1059]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1058]---> Adder-cost: 16   maxlim: 7   bits: 4/3
c ---[1056]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1054]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1052]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1050]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1048]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1046]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1044]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1042]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1040]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1038]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1037]---> Adder-cost: 16   maxlim: 7   bits: 4/3
c ---[1035]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1033]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1031]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1029]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1027]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1025]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1023]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1021]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1019]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1017]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1016]---> Adder-cost: 16   maxlim: 7   bits: 4/3
c ---[1014]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1012]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1010]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1008]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1006]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1004]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1002]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1000]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[ 998]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[ 996]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[ 995]---> Adder-cost: 16   maxlim: 7   bits: 4/3
c ---[ 993]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[ 991]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[ 989]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[ 987]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[ 985]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[ 983]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[ 981]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[ 979]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[ 977]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[ 975]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[ 974]---> Adder-cost: 190   maxlim: 87   bits: 7/7
c ---[ 973]---> Adder-cost: 16   maxlim: 7   bits: 4/3
c ---[ 971]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[ 969]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[ 967]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[ 965]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[ 963]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[ 961]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[ 959]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[ 957]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[ 955]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[ 953]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[ 952]---> Adder-cost: 16   maxlim: 7   bits: 4/3
c ---[ 950]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[ 948]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[ 946]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[ 944]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[ 942]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[ 940]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[ 938]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[ 936]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[ 934]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[ 932]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[ 931]---> Adder-cost: 16   maxlim: 7   bits: 4/3
c ---[ 929]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[ 927]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[ 925]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[ 923]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[ 921]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[ 919]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[ 917]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[ 915]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[ 913]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[ 911]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[ 910]---> Adder-cost: 16   maxlim: 7   bits: 4/3
c ---[ 908]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[ 906]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[ 904]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[ 902]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[ 900]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[ 898]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[ 896]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[ 894]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[ 892]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[ 890]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[ 889]---> Adder-cost: 16   maxlim: 7   bits: 4/3
c ---[ 887]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[ 885]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[ 876]---> Adder-cost: 16   maxlim: 7   bits: 4/3
c ---[ 865]---> Adder-cost: 16   maxlim: 7   bits: 4/3
c ---[ 854]---> Adder-cost: 14   maxlim: 5   bits: 4/3
c ---[ 843]---> Adder-cost: 14   maxlim: 5   bits: 4/3
c ---[ 832]---> Adder-cost: 14   maxlim: 5   bits: 4/3
c ---[ 821]---> Adder-cost: 190   maxlim: 87   bits: 7/7
c ---[ 820]---> Adder-cost: 190   maxlim: 87   bits: 7/7
c ---[ 819]---> Adder-cost: 14   maxlim: 5   bits: 4/3
c ---[ 808]---> Adder-cost: 14   maxlim: 5   bits: 4/3
c ---[ 797]---> Adder-cost: 14   maxlim: 5   bits: 4/3
c ---[ 786]---> Adder-cost: 14   maxlim: 5   bits: 4/3
c ---[ 775]---> Adder-cost: 14   maxlim: 5   bits: 4/3
c ---[ 764]---> Adder-cost: 14   maxlim: 5   bits: 4/3
c ---[ 758]---> Adder-cost: 14   maxlim: 5   bits: 4/3
c ---[ 757]---> Adder-cost: 14   maxlim: 5   bits: 4/3
c ---[ 756]---> Adder-cost: 14   maxlim: 5   bits: 4/3
c ---[ 755]---> Adder-cost: 14   maxlim: 5   bits: 4/3
c ---[ 754]---> Adder-cost: 190   maxlim: 87   bits: 7/7
c ---[ 753]---> Adder-cost: 14   maxlim: 5   bits: 4/3
c ---[ 752]---> Adder-cost: 14   maxlim: 5   bits: 4/3
c ---[ 751]---> Adder-cost: 14   maxlim: 5   bits: 4/3
c ---[ 750]---> Adder-cost: 14   maxlim: 5   bits: 4/3
c ---[ 749]---> Adder-cost: 14   maxlim: 5   bits: 4/3
c ---[ 748]---> Adder-cost: 14   maxlim: 5   bits: 4/3
c ---[ 747]---> Adder-cost: 14   maxlim: 5   bits: 4/3
c ---[ 746]---> Adder-cost: 14   maxlim: 5   bits: 4/3
c ---[ 745]---> Adder-cost: 14   maxlim: 5   bits: 4/3
c ---[ 744]---> Adder-cost: 14   maxlim: 5   bits: 4/3
c ---[ 743]---> Adder-cost: 190   maxlim: 87   bits: 7/7
c ---[ 742]---> Adder-cost: 14   maxlim: 5   bits: 4/3
c ---[ 741]---> Adder-cost: 14   maxlim: 5   bits: 4/3
c ---[ 740]---> Adder-cost: 14   maxlim: 5   bits: 4/3
c ---[ 739]---> Adder-cost: 14   maxlim: 5   bits: 4/3
c ---[ 738]---> Adder-cost: 14   maxlim: 5   bits: 4/3
c ---[ 737]---> Adder-cost: 5   maxlim: 1   bits: 2/1
c ---[ 736]---> Adder-cost: 5   maxlim: 1   bits: 2/1
c ---[ 735]---> Adder-cost: 5   maxlim: 1   bits: 2/1
c ---[ 734]---> Adder-cost: 5   maxlim: 1   bits: 2/1
c ---[ 733]---> Adder-cost: 5   maxlim: 1   bits: 2/1
c ---[ 732]---> Adder-cost: 190   maxlim: 87   bits: 7/7
c ---[ 731]---> Adder-cost: 5   maxlim: 1   bits: 2/1
c ---[ 730]---> Adder-cost: 5   maxlim: 1   bits: 2/1
c ---[ 729]---> Adder-cost: 5   maxlim: 1   bits: 2/1
c ---[ 728]---> Adder-cost: 5   maxlim: 1   bits: 2/1
c ---[ 727]---> Adder-cost: 5   maxlim: 1   bits: 2/1
c ---[ 726]---> Adder-cost: 5   maxlim: 1   bits: 2/1
c ---[ 725]---> Adder-cost: 5   maxlim: 1   bits: 2/1
c ---[ 724]---> Adder-cost: 5   maxlim: 1   bits: 2/1
c ---[ 723]---> Adder-cost: 5   maxlim: 1   bits: 2/1
c ---[ 722]---> Adder-cost: 5   maxlim: 1   bits: 2/1
c ---[ 721]---> Adder-cost: 190   maxlim: 87   bits: 7/7
c ---[ 720]---> Adder-cost: 5   maxlim: 1   bits: 2/1
c ---[ 719]---> Adder-cost: 5   maxlim: 1   bits: 2/1
c ---[ 718]---> Adder-cost: 5   maxlim: 1   bits: 2/1
c ---[ 717]---> Adder-cost: 5   maxlim: 1   bits: 2/1
c ---[ 716]---> Adder-cost: 5   maxlim: 1   bits: 2/1
c ---[ 715]---> Adder-cost: 5   maxlim: 1   bits: 2/1
c ---[ 714]---> Adder-cost: 5   maxlim: 1   bits: 2/1
c ---[ 713]---> Adder-cost: 5   maxlim: 1   bits: 2/1
c ---[ 712]---> Adder-cost: 5   maxlim: 1   bits: 2/1
c ---[ 711]---> Adder-cost: 5   maxlim: 1   bits: 2/1
c ---[ 710]---> Adder-cost: 190   maxlim: 87   bits: 7/7
c ---[ 709]---> Adder-cost: 5   maxlim: 1   bits: 2/1
c ---[ 708]---> Adder-cost: 5   maxlim: 1   bits: 2/1
c ---[ 707]---> Adder-cost: 5   maxlim: 1   bits: 2/1
c ---[ 706]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 705]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 704]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 703]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 702]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 701]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 700]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 699]---> Adder-cost: 190   maxlim: 87   bits: 7/7
c ---[ 698]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 697]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 696]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 695]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 694]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 693]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 692]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 691]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 690]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 689]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 688]---> Adder-cost: 190   maxlim: 87   bits: 7/7
c ---[ 687]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 686]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 685]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 684]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 683]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 682]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 681]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 680]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 679]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 678]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 677]---> Adder-cost: 190   maxlim: 87   bits: 7/7
c ---[ 676]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 675]---> Adder-cost: 14   maxlim: 5   bits: 4/3
c ---[ 674]---> Adder-cost: 14   maxlim: 5   bits: 4/3
c ---[ 673]---> Adder-cost: 14   maxlim: 5   bits: 4/3
c ---[ 672]---> Adder-cost: 14   maxlim: 5   bits: 4/3
c ---[ 671]---> Adder-cost: 14   maxlim: 5   bits: 4/3
c ---[ 670]---> Adder-cost: 14   maxlim: 5   bits: 4/3
c ---[ 669]---> Adder-cost: 14   maxlim: 5   bits: 4/3
c ---[ 668]---> Adder-cost: 14   maxlim: 5   bits: 4/3
c ---[ 667]---> Adder-cost: 14   maxlim: 5   bits: 4/3
c ---[ 666]---> Adder-cost: 20   maxlim: 10   bits: 4/4
c ---[ 665]---> Adder-cost: 14   maxlim: 5   bits: 4/3
c ---[ 664]---> Adder-cost: 14   maxlim: 5   bits: 4/3
c ---[ 663]---> Adder-cost: 14   maxlim: 5   bits: 4/3
c ---[ 662]---> Adder-cost: 14   maxlim: 5   bits: 4/3
c ---[ 661]---> Adder-cost: 14   maxlim: 5   bits: 4/3
c ---[ 660]---> Adder-cost: 14   maxlim: 5   bits: 4/3
c ---[ 659]---> Adder-cost: 14   maxlim: 5   bits: 4/3
c ---[ 658]---> Adder-cost: 14   maxlim: 5   bits: 4/3
c ---[ 657]---> Adder-cost: 14   maxlim: 5   bits: 4/3
c ---[ 656]---> Adder-cost: 14   maxlim: 5   bits: 4/3
c ---[ 655]---> Adder-cost: 190   maxlim: 87   bits: 7/7
c ---[ 654]---> Adder-cost: 20   maxlim: 10   bits: 4/4
c ---[ 653]---> Adder-cost: 14   maxlim: 5   bits: 4/3
c ---[ 652]---> Adder-cost: 14   maxlim: 5   bits: 4/3
c ---[ 651]---> Adder-cost: 14   maxlim: 5   bits: 4/3
c ---[ 650]---> Adder-cost: 14   maxlim: 5   bits: 4/3
c ---[ 649]---> Adder-cost: 14   maxlim: 5   bits: 4/3
c ---[ 648]---> Adder-cost: 14   maxlim: 5   bits: 4/3
c ---[ 647]---> Adder-cost: 14   maxlim: 5   bits: 4/3
c ---[ 646]---> Adder-cost: 14   maxlim: 5   bits: 4/3
c ---[ 645]---> Adder-cost: 14   maxlim: 5   bits: 4/3
c ---[ 644]---> Adder-cost: 15   maxlim: 3   bits: 3/2
c ---[ 643]---> Adder-cost: 20   maxlim: 10   bits: 4/4
c ---[ 642]---> Adder-cost: 15   maxlim: 3   bits: 3/2
c ---[ 641]---> Adder-cost: 15   maxlim: 3   bits: 3/2
c ---[ 640]---> Adder-cost: 15   maxlim: 3   bits: 3/2
c ---[ 639]---> Adder-cost: 15   maxlim: 3   bits: 3/2
c ---[ 638]---> Adder-cost: 15   maxlim: 3   bits: 3/2
c ---[ 637]---> Adder-cost: 15   maxlim: 3   bits: 3/2
c ---[ 636]---> Adder-cost: 15   maxlim: 3   bits: 3/2
c ---[ 635]---> Adder-cost: 15   maxlim: 3   bits: 3/2
c ---[ 634]---> Adder-cost: 15   maxlim: 3   bits: 3/2
c ---[ 633]---> Adder-cost: 15   maxlim: 3   bits: 3/2
c ---[ 632]---> Adder-cost: 20   maxlim: 10   bits: 4/4
c ---[ 631]---> Adder-cost: 15   maxlim: 3   bits: 3/2
c ---[ 630]---> Adder-cost: 15   maxlim: 3   bits: 3/2
c ---[ 629]---> Adder-cost: 15   maxlim: 3   bits: 3/2
c ---[ 628]---> Adder-cost: 15   maxlim: 3   bits: 3/2
c ---[ 627]---> Adder-cost: 15   maxlim: 3   bits: 3/2
c ---[ 626]---> Adder-cost: 15   maxlim: 3   bits: 3/2
c ---[ 625]---> Adder-cost: 15   maxlim: 3   bits: 3/2
c ---[ 624]---> Adder-cost: 15   maxlim: 3   bits: 3/2
c ---[ 623]---> Adder-cost: 15   maxlim: 3   bits: 3/2
c ---[ 622]---> Adder-cost: 15   maxlim: 3   bits: 3/2
c ---[ 621]---> Adder-cost: 20   maxlim: 10   bits: 4/4
c ---[ 620]---> Adder-cost: 15   maxlim: 3   bits: 3/2
c ---[ 619]---> Adder-cost: 15   maxlim: 3   bits: 3/2
c ---[ 618]---> Adder-cost: 15   maxlim: 3   bits: 3/2
c ---[ 617]---> Adder-cost: 15   maxlim: 3   bits: 3/2
c ---[ 616]---> Adder-cost: 15   maxlim: 3   bits: 3/2
c ---[ 615]---> Adder-cost: 15   maxlim: 3   bits: 3/2
c ---[ 614]---> Adder-cost: 15   maxlim: 3   bits: 3/2
c ---[ 613]---> Adder-cost: 20   maxlim: 10   bits: 4/4
c ---[ 612]---> Adder-cost: 20   maxlim: 10   bits: 4/4
c ---[ 611]---> Adder-cost: 20   maxlim: 10   bits: 4/4
c ---[ 605]---> Adder-cost: 20   maxlim: 10   bits: 4/4
c ---[ 594]---> Adder-cost: 20   maxlim: 10   bits: 4/4
c ---[ 583]---> Adder-cost: 20   maxlim: 10   bits: 4/4
c ---[ 579]---> Adder-cost: 5   maxlim: 1   bits: 2/1
c ---[ 578]---> Adder-cost: 5   maxlim: 1   bits: 2/1
c ---[ 577]---> Adder-cost: 5   maxlim: 1   bits: 2/1
c ---[ 576]---> Adder-cost: 5   maxlim: 1   bits: 2/1
c ---[ 575]---> Adder-cost: 5   maxlim: 1   bits: 2/1
c ---[ 574]---> Adder-cost: 5   maxlim: 1   bits: 2/1
c ---[ 573]---> Adder-cost: 5   maxlim: 1   bits: 2/1
c ---[ 572]---> Adder-cost: 190   maxlim: 87   bits: 7/7
c ---[ 571]---> Adder-cost: 20   maxlim: 10   bits: 4/4
c ---[ 570]---> Adder-cost: 5   maxlim: 1   bits: 2/1
c ---[ 569]---> Adder-cost: 5   maxlim: 1   bits: 2/1
c ---[ 568]---> Adder-cost: 5   maxlim: 1   bits: 2/1
c ---[ 567]---> Adder-cost: 5   maxlim: 1   bits: 2/1
c ---[ 566]---> Adder-cost: 5   maxlim: 1   bits: 2/1
c ---[ 565]---> Adder-cost: 5   maxlim: 1   bits: 2/1
c ---[ 564]---> Adder-cost: 5   maxlim: 1   bits: 2/1
c ---[ 563]---> Adder-cost: 5   maxlim: 1   bits: 2/1
c ---[ 562]---> Adder-cost: 5   maxlim: 1   bits: 2/1
c ---[ 561]---> Adder-cost: 5   maxlim: 1   bits: 2/1
c ---[ 560]---> Adder-cost: 20   maxlim: 10   bits: 4/4
c ---[ 559]---> Adder-cost: 5   maxlim: 1   bits: 2/1
c ---[ 558]---> Adder-cost: 5   maxlim: 1   bits: 2/1
c ---[ 557]---> Adder-cost: 5   maxlim: 1   bits: 2/1
c ---[ 556]---> Adder-cost: 5   maxlim: 1   bits: 2/1
c ---[ 555]---> Adder-cost: 5   maxlim: 1   bits: 2/1
c ---[ 554]---> Adder-cost: 5   maxlim: 1   bits: 2/1
c ---[ 553]---> Adder-cost: 5   maxlim: 1   bits: 2/1
c ---[ 552]---> Adder-cost: 5   maxlim: 1   bits: 2/1
c ---[ 551]---> Adder-cost: 5   maxlim: 1   bits: 2/1
c ---[ 550]---> Adder-cost: 5   maxlim: 1   bits: 2/1
c ---[ 549]---> Adder-cost: 20   maxlim: 10   bits: 4/4
c ---[ 548]---> Adder-cost: 5   maxlim: 1   bits: 2/1
c ---[ 547]---> Adder-cost: 20   maxlim: 10   bits: 4/4
c ---[ 546]---> Adder-cost: 20   maxlim: 10   bits: 4/4
c ---[ 545]---> Adder-cost: 20   maxlim: 10   bits: 4/4
c ---[ 544]---> Adder-cost: 20   maxlim: 10   bits: 4/4
c ---[ 543]---> Adder-cost: 20   maxlim: 10   bits: 4/4
c ---[ 542]---> Adder-cost: 8   maxlim: 3   bits: 3/2
c ---[ 541]---> Adder-cost: 8   maxlim: 3   bits: 3/2
c ---[ 540]---> Adder-cost: 8   maxlim: 3   bits: 3/2
c ---[ 539]---> Adder-cost: 20   maxlim: 10   bits: 4/4
c ---[ 538]---> Adder-cost: 8   maxlim: 3   bits: 3/2
c ---[ 537]---> Adder-cost: 8   maxlim: 3   bits: 3/2
c ---[ 536]---> Adder-cost: 8   maxlim: 3   bits: 3/2
c ---[ 535]---> Adder-cost: 8   maxlim: 3   bits: 3/2
c ---[ 534]---> Adder-cost: 8   maxlim: 3   bits: 3/2
c ---[ 533]---> Adder-cost: 8   maxlim: 3   bits: 3/2
c ---[ 532]---> Adder-cost: 8   maxlim: 3   bits: 3/2
c ---[ 531]---> Adder-cost: 8   maxlim: 3   bits: 3/2
c ---[ 530]---> Adder-cost: 8   maxlim: 3   bits: 3/2
c ---[ 529]---> Adder-cost: 8   maxlim: 3   bits: 3/2
c ---[ 528]---> Adder-cost: 20   maxlim: 10   bits: 4/4
c ---[ 527]---> Adder-cost: 8   maxlim: 3   bits: 3/2
c ---[ 526]---> Adder-cost: 8   maxlim: 3   bits: 3/2
c ---[ 525]---> Adder-cost: 8   maxlim: 3   bits: 3/2
c ---[ 524]---> Adder-cost: 8   maxlim: 3   bits: 3/2
c ---[ 523]---> Adder-cost: 8   maxlim: 3   bits: 3/2
c ---[ 522]---> Adder-cost: 8   maxlim: 3   bits: 3/2
c ---[ 521]---> Adder-cost: 8   maxlim: 3   bits: 3/2
c ---[ 520]---> Adder-cost: 8   maxlim: 3   bits: 3/2
c ---[ 519]---> Adder-cost: 8   maxlim: 3   bits: 3/2
c ---[ 518]---> Adder-cost: 8   maxlim: 3   bits: 3/2
c ---[ 517]---> Adder-cost: 190   maxlim: 87   bits: 7/7
c ---[ 516]---> Adder-cost: 20   maxlim: 10   bits: 4/4
c ---[ 515]---> Adder-cost: 8   maxlim: 3   bits: 3/2
c ---[ 514]---> Adder-cost: 8   maxlim: 3   bits: 3/2
c ---[ 513]---> Adder-cost: 8   maxlim: 3   bits: 3/2
c ---[ 512]---> Adder-cost: 8   maxlim: 3   bits: 3/2
c ---[ 511]---> Adder-cost: 8   maxlim: 3   bits: 3/2
c ---[ 510]---> Adder-cost: 8   maxlim: 3   bits: 3/2
c ---[ 509]---> Adder-cost: 8   maxlim: 3   bits: 3/2
c ---[ 508]---> Adder-cost: 8   maxlim: 3   bits: 3/2
c ---[ 507]---> Adder-cost: 8   maxlim: 3   bits: 3/2
c ---[ 506]---> Adder-cost: 8   maxlim: 3   bits: 3/2
c ---[ 505]---> Adder-cost: 20   maxlim: 10   bits: 4/4
c ---[ 504]---> Adder-cost: 8   maxlim: 3   bits: 3/2
c ---[ 503]---> Adder-cost: 8   maxlim: 3   bits: 3/2
c ---[ 502]---> Adder-cost: 8   maxlim: 3   bits: 3/2
c ---[ 501]---> Adder-cost: 8   maxlim: 3   bits: 3/2
c ---[ 500]---> Adder-cost: 8   maxlim: 3   bits: 3/2
c ---[ 499]---> Adder-cost: 8   maxlim: 3   bits: 3/2
c ---[ 498]---> Adder-cost: 8   maxlim: 3   bits: 3/2
c ---[ 497]---> Adder-cost: 8   maxlim: 3   bits: 3/2
c ---[ 496]---> Adder-cost: 8   maxlim: 3   bits: 3/2
c ---[ 495]---> Adder-cost: 8   maxlim: 3   bits: 3/2
c ---[ 494]---> Adder-cost: 20   maxlim: 10   bits: 4/4
c ---[ 493]---> Adder-cost: 8   maxlim: 3   bits: 3/2
c ---[ 492]---> Adder-cost: 8   maxlim: 3   bits: 3/2
c ---[ 491]---> Adder-cost: 8   maxlim: 3   bits: 3/2
c ---[ 490]---> Adder-cost: 8   maxlim: 3   bits: 3/2
c ---[ 489]---> Adder-cost: 8   maxlim: 3   bits: 3/2
c ---[ 488]---> Adder-cost: 8   maxlim: 3   bits: 3/2
c ---[ 487]---> Adder-cost: 8   maxlim: 3   bits: 3/2
c ---[ 486]---> Adder-cost: 8   maxlim: 3   bits: 3/2
c ---[ 485]---> Adder-cost: 8   maxlim: 3   bits: 3/2
c ---[ 484]---> Adder-cost: 8   maxlim: 3   bits: 3/2
c ---[ 483]---> Adder-cost: 20   maxlim: 10   bits: 4/4
c ---[ 482]---> Adder-cost: 8   maxlim: 3   bits: 3/2
c ---[ 481]---> Adder-cost: 8   maxlim: 3   bits: 3/2
c ---[ 480]---> Adder-cost: 8   maxlim: 3   bits: 3/2
c ---[ 479]---> Adder-cost: 8   maxlim: 3   bits: 3/2
c ---[ 478]---> Adder-cost: 8   maxlim: 3   bits: 3/2
c ---[ 477]---> Adder-cost: 8   maxlim: 3   bits: 3/2
c ---[ 476]---> Adder-cost: 8   maxlim: 3   bits: 3/2
c ---[ 475]---> Adder-cost: 8   maxlim: 3   bits: 3/2
c ---[ 474]---> Adder-cost: 8   maxlim: 3   bits: 3/2
c ---[ 473]---> Adder-cost: 8   maxlim: 3   bits: 3/2
c ---[ 472]---> Adder-cost: 20   maxlim: 10   bits: 4/4
c ---[ 471]---> Adder-cost: 8   maxlim: 3   bits: 3/2
c ---[ 470]---> Adder-cost: 8   maxlim: 3   bits: 3/2
c ---[ 469]---> Adder-cost: 8   maxlim: 3   bits: 3/2
c ---[ 468]---> Adder-cost: 8   maxlim: 3   bits: 3/2
c ---[ 467]---> Adder-cost: 8   maxlim: 3   bits: 3/2
c ---[ 466]---> Adder-cost: 8   maxlim: 3   bits: 3/2
c ---[ 465]---> Adder-cost: 8   maxlim: 3   bits: 3/2
c ---[ 464]---> Adder-cost: 8   maxlim: 3   bits: 3/2
c ---[ 463]---> Adder-cost: 8   maxlim: 3   bits: 3/2
c ---[ 462]---> Adder-cost: 8   maxlim: 3   bits: 3/2
c ---[ 461]---> Adder-cost: 20   maxlim: 10   bits: 4/4
c ---[ 460]---> Adder-cost: 8   maxlim: 3   bits: 3/2
c ---[ 459]---> Adder-cost: 8   maxlim: 3   bits: 3/2
c ---[ 458]---> Adder-cost: 8   maxlim: 3   bits: 3/2
c ---[ 457]---> Adder-cost: 8   maxlim: 3   bits: 3/2
c ---[ 456]---> Adder-cost: 8   maxlim: 3   bits: 3/2
c ---[ 455]---> Adder-cost: 8   maxlim: 3   bits: 3/2
c ---[ 454]---> Adder-cost: 8   maxlim: 3   bits: 3/2
c ---[ 453]---> Adder-cost: 8   maxlim: 3   bits: 3/2
c ---[ 452]---> Adder-cost: 8   maxlim: 3   bits: 3/2
c ---[ 451]---> Adder-cost: 8   maxlim: 3   bits: 3/2
c ---[ 450]---> Adder-cost: 20   maxlim: 10   bits: 4/4
c ---[ 449]---> Adder-cost: 8   maxlim: 3   bits: 3/2
c ---[ 448]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 447]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 446]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 445]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 444]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 443]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 442]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 441]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 440]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 439]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 438]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 437]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 436]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 435]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 434]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 433]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 432]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 431]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 430]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 429]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 428]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 427]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 426]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 425]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 424]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 423]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 422]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 421]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 420]---> Adder-cost: 190   maxlim: 87   bits: 7/7
c ---[ 419]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 418]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 417]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 416]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 415]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 414]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 413]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 412]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 411]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 410]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 409]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 408]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 407]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 406]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 405]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 404]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 403]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 402]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 401]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 400]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 399]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 398]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 397]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 396]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 395]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 394]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 393]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 392]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 391]---> Adder-cost: 14   maxlim: 5   bits: 4/3
c ---[ 390]---> Adder-cost: 14   maxlim: 5   bits: 4/3
c ---[ 389]---> Adder-cost: 14   maxlim: 5   bits: 4/3
c ---[ 388]---> Adder-cost: 14   maxlim: 5   bits: 4/3
c ---[ 387]---> Adder-cost: 14   maxlim: 5   bits: 4/3
c ---[ 386]---> Adder-cost: 14   maxlim: 5   bits: 4/3
c ---[ 385]---> Adder-cost: 14   maxlim: 5   bits: 4/3
c ---[ 384]---> Adder-cost: 14   maxlim: 5   bits: 4/3
c ---[ 383]---> Adder-cost: 14   maxlim: 5   bits: 4/3
c ---[ 382]---> Adder-cost: 14   maxlim: 5   bits: 4/3
c ---[ 381]---> Adder-cost: 14   maxlim: 5   bits: 4/3
c ---[ 380]---> Adder-cost: 14   maxlim: 5   bits: 4/3
c ---[ 379]---> Adder-cost: 14   maxlim: 5   bits: 4/3
c ---[ 378]---> Adder-cost: 14   maxlim: 5   bits: 4/3
c ---[ 377]---> Adder-cost: 14   maxlim: 5   bits: 4/3
c ---[ 376]---> Adder-cost: 14   maxlim: 5   bits: 4/3
c ---[ 375]---> Adder-cost: 14   maxlim: 5   bits: 4/3
c ---[ 374]---> Adder-cost: 14   maxlim: 5   bits: 4/3
c ---[ 373]---> Adder-cost: 14   maxlim: 5   bits: 4/3
c ---[ 372]---> Adder-cost: 14   maxlim: 5   bits: 4/3
c ---[ 371]---> Adder-cost: 14   maxlim: 5   bits: 4/3
c ---[ 370]---> Adder-cost: 14   maxlim: 5   bits: 4/3
c ---[ 369]---> Adder-cost: 14   maxlim: 5   bits: 4/3
c ---[ 368]---> Adder-cost: 14   maxlim: 5   bits: 4/3
c ---[ 367]---> Adder-cost: 14   maxlim: 5   bits: 4/3
c ---[ 366]---> Adder-cost: 14   maxlim: 5   bits: 4/3
c ---[ 365]---> Adder-cost: 14   maxlim: 5   bits: 4/3
c ---[ 364]---> Adder-cost: 190   maxlim: 87   bits: 7/7
c ---[ 363]---> Adder-cost: 14   maxlim: 5   bits: 4/3
c ---[ 362]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 361]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 360]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 359]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 358]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 357]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 356]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 355]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 354]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 353]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 352]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 351]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 350]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 349]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 348]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 347]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 346]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 345]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 344]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 343]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 342]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 341]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 340]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 339]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 338]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 337]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 336]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 335]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 334]---> Adder-cost: 5   maxlim: 1   bits: 2/1
c ---[ 333]---> Adder-cost: 5   maxlim: 1   bits: 2/1
c ---[ 332]---> Adder-cost: 5   maxlim: 1   bits: 2/1
c ---[ 331]---> Adder-cost: 5   maxlim: 1   bits: 2/1
c ---[ 330]---> Adder-cost: 5   maxlim: 1   bits: 2/1
c ---[ 329]---> Adder-cost: 5   maxlim: 1   bits: 2/1
c ---[ 328]---> Adder-cost: 5   maxlim: 1   bits: 2/1
c ---[ 327]---> Adder-cost: 5   maxlim: 1   bits: 2/1
c ---[ 326]---> Adder-cost: 5   maxlim: 1   bits: 2/1
c ---[ 325]---> Adder-cost: 5   maxlim: 1   bits: 2/1
c ---[ 324]---> Adder-cost: 5   maxlim: 1   bits: 2/1
c ---[ 323]---> Adder-cost: 5   maxlim: 1   bits: 2/1
c ---[ 322]---> Adder-cost: 5   maxlim: 1   bits: 2/1
c ---[ 321]---> Adder-cost: 5   maxlim: 1   bits: 2/1
c ---[ 320]---> Adder-cost: 5   maxlim: 1   bits: 2/1
c ---[ 319]---> Adder-cost: 5   maxlim: 1   bits: 2/1
c ---[ 318]---> Adder-cost: 5   maxlim: 1   bits: 2/1
c ---[ 317]---> Adder-cost: 5   maxlim: 1   bits: 2/1
c ---[ 316]---> Adder-cost: 5   maxlim: 1   bits: 2/1
c ---[ 315]---> Adder-cost: 5   maxlim: 1   bits: 2/1
c ---[ 314]---> Adder-cost: 5   maxlim: 1   bits: 2/1
c ---[ 313]---> Adder-cost: 5   maxlim: 1   bits: 2/1
c ---[ 312]---> Adder-cost: 5   maxlim: 1   bits: 2/1
c ---[ 311]---> Adder-cost: 5   maxlim: 1   bits: 2/1
c ---[ 310]---> Adder-cost: 5   maxlim: 1   bits: 2/1
c ---[ 309]---> Adder-cost: 5   maxlim: 1   bits: 2/1
c ---[ 308]---> Adder-cost: 5   maxlim: 1   bits: 2/1
c ---[ 307]---> Adder-cost: 5   maxlim: 1   bits: 2/1
c ---[ 306]---> Adder-cost: 20   maxlim: 8   bits: 4/4
c ---[ 305]---> Adder-cost: 20   maxlim: 8   bits: 4/4
c ---[ 304]---> Adder-cost: 20   maxlim: 8   bits: 4/4
c ---[ 303]---> Adder-cost: 20   maxlim: 8   bits: 4/4
c ---[ 302]---> Adder-cost: 20   maxlim: 8   bits: 4/4
c ---[ 301]---> Adder-cost: 20   maxlim: 8   bits: 4/4
c ---[ 300]---> Adder-cost: 20   maxlim: 8   bits: 4/4
c ---[ 299]---> Adder-cost: 20   maxlim: 8   bits: 4/4
c ---[ 298]---> Adder-cost: 20   maxlim: 8   bits: 4/4
c ---[ 297]---> Adder-cost: 20   maxlim: 8   bits: 4/4
c ---[ 296]---> Adder-cost: 20   maxlim: 8   bits: 4/4
c ---[ 295]---> Adder-cost: 20   maxlim: 8   bits: 4/4
c ---[ 294]---> Adder-cost: 20   maxlim: 8   bits: 4/4
c ---[ 293]---> Adder-cost: 20   maxlim: 8   bits: 4/4
c ---[ 292]---> Adder-cost: 20   maxlim: 8   bits: 4/4
c ---[ 291]---> Adder-cost: 20   maxlim: 8   bits: 4/4
c ---[ 290]---> Adder-cost: 20   maxlim: 8   bits: 4/4
c ---[ 289]---> Adder-cost: 20   maxlim: 8   bits: 4/4
c ---[ 288]---> Adder-cost: 20   maxlim: 8   bits: 4/4
c ---[ 287]---> Adder-cost: 20   maxlim: 8   bits: 4/4
c ---[ 286]---> Adder-cost: 20   maxlim: 8   bits: 4/4
c ---[ 285]---> Adder-cost: 20   maxlim: 8   bits: 4/4
c ---[ 284]---> Adder-cost: 20   maxlim: 8   bits: 4/4
c ---[ 283]---> Adder-cost: 20   maxlim: 8   bits: 4/4
c ---[ 282]---> Adder-cost: 20   maxlim: 8   bits: 4/4
c ---[ 281]---> Adder-cost: 20   maxlim: 8   bits: 4/4
c ---[ 280]---> Adder-cost: 20   maxlim: 8   bits: 4/4
c ---[ 279]---> Adder-cost: 20   maxlim: 8   bits: 4/4
c ---[ 278]---> Adder-cost: 5   maxlim: 1   bits: 2/1
c ---[ 277]---> Adder-cost: 5   maxlim: 1   bits: 2/1
c ---[ 276]---> Adder-cost: 5   maxlim: 1   bits: 2/1
c ---[ 275]---> Adder-cost: 5   maxlim: 1   bits: 2/1
c ---[ 274]---> Adder-cost: 5   maxlim: 1   bits: 2/1
c ---[ 273]---> Adder-cost: 5   maxlim: 1   bits: 2/1
c ---[ 272]---> Adder-cost: 5   maxlim: 1   bits: 2/1
c ---[ 271]---> Adder-cost: 5   maxlim: 1   bits: 2/1
c ---[ 270]---> Adder-cost: 5   maxlim: 1   bits: 2/1
c ---[ 269]---> Adder-cost: 5   maxlim: 1   bits: 2/1
c ---[ 268]---> Adder-cost: 5   maxlim: 1   bits: 2/1
c ---[ 267]---> Adder-cost: 5   maxlim: 1   bits: 2/1
c ---[ 266]---> Adder-cost: 5   maxlim: 1   bits: 2/1
c ---[ 265]---> Adder-cost: 5   maxlim: 1   bits: 2/1
c ---[ 264]---> Adder-cost: 5   maxlim: 1   bits: 2/1
c ---[ 263]---> Adder-cost: 190   maxlim: 87   bits: 7/7
c ---[ 262]---> Adder-cost: 5   maxlim: 1   bits: 2/1
c ---[ 261]---> Adder-cost: 5   maxlim: 1   bits: 2/1
c ---[ 260]---> Adder-cost: 5   maxlim: 1   bits: 2/1
c ---[ 259]---> Adder-cost: 5   maxlim: 1   bits: 2/1
c ---[ 258]---> Adder-cost: 5   maxlim: 1   bits: 2/1
c ---[ 257]---> Adder-cost: 5   maxlim: 1   bits: 2/1
c ---[ 256]---> Adder-cost: 5   maxlim: 1   bits: 2/1
c ---[ 255]---> Adder-cost: 5   maxlim: 1   bits: 2/1
c ---[ 254]---> Adder-cost: 5   maxlim: 1   bits: 2/1
c ---[ 253]---> Adder-cost: 5   maxlim: 1   bits: 2/1
c ---[ 252]---> Adder-cost: 5   maxlim: 1   bits: 2/1
c ---[ 251]---> Adder-cost: 5   maxlim: 1   bits: 2/1
c ---[ 250]---> Adder-cost: 5   maxlim: 1   bits: 2/1
c ---[ 221]---> Adder-cost: 22   maxlim: 11   bits: 4/4
c ---[ 220]---> Adder-cost: 22   maxlim: 11   bits: 4/4
c ---[ 219]---> Adder-cost: 22   maxlim: 11   bits: 4/4
c ---[ 218]---> Adder-cost: 22   maxlim: 11   bits: 4/4
c ---[ 217]---> Adder-cost: 22   maxlim: 11   bits: 4/4
c ---[ 216]---> Adder-cost: 22   maxlim: 11   bits: 4/4
c ---[ 215]---> Adder-cost: 22   maxlim: 11   bits: 4/4
c ---[ 214]---> Adder-cost: 22   maxlim: 11   bits: 4/4
c ---[ 213]---> Adder-cost: 22   maxlim: 11   bits: 4/4
c ---[ 212]---> Adder-cost: 30   maxlim: 13   bits: 5/4
c ---[ 211]---> Adder-cost: 22   maxlim: 11   bits: 4/4
c ---[ 210]---> Adder-cost: 22   maxlim: 11   bits: 4/4
c ---[ 209]---> Adder-cost: 22   maxlim: 11   bits: 4/4
c ---[ 208]---> Adder-cost: 22   maxlim: 11   bits: 4/4
c ---[ 207]---> Adder-cost: 22   maxlim: 11   bits: 4/4
c ---[ 206]---> Adder-cost: 22   maxlim: 11   bits: 4/4
c ---[ 205]---> Adder-cost: 22   maxlim: 11   bits: 4/4
c ---[ 204]---> Adder-cost: 22   maxlim: 11   bits: 4/4
c ---[ 203]---> Adder-cost: 22   maxlim: 11   bits: 4/4
c ---[ 202]---> Adder-cost: 22   maxlim: 11   bits: 4/4
c ---[ 201]---> Adder-cost: 30   maxlim: 13   bits: 5/4
c ---[ 200]---> Adder-cost: 22   maxlim: 11   bits: 4/4
c ---[ 199]---> Adder-cost: 22   maxlim: 11   bits: 4/4
c ---[ 198]---> Adder-cost: 22   maxlim: 11   bits: 4/4
c ---[ 197]---> Adder-cost: 22   maxlim: 11   bits: 4/4
c ---[ 196]---> Adder-cost: 22   maxlim: 11   bits: 4/4
c ---[ 195]---> Adder-cost: 22   maxlim: 11   bits: 4/4
c ---[ 194]---> Adder-cost: 22   maxlim: 11   bits: 4/4
c ---[ 193]---> Adder-cost: 22   maxlim: 11   bits: 4/4
c ---[ 192]---> Adder-cost: 22   maxlim: 11   bits: 4/4
c ---[ 191]---> Adder-cost: 8   maxlim: 3   bits: 3/2
c ---[ 190]---> Adder-cost: 30   maxlim: 13   bits: 5/4
c ---[ 189]---> Adder-cost: 8   maxlim: 3   bits: 3/2
c ---[ 188]---> Adder-cost: 8   maxlim: 3   bits: 3/2
c ---[ 187]---> Adder-cost: 8   maxlim: 3   bits: 3/2
c ---[ 186]---> Adder-cost: 8   maxlim: 3   bits: 3/2
c ---[ 185]---> Adder-cost: 8   maxlim: 3   bits: 3/2
c ---[ 184]---> Adder-cost: 8   maxlim: 3   bits: 3/2
c ---[ 183]---> Adder-cost: 8   maxlim: 3   bits: 3/2
c ---[ 182]---> Adder-cost: 8   maxlim: 3   bits: 3/2
c ---[ 181]---> Adder-cost: 8   maxlim: 3   bits: 3/2
c ---[ 180]---> Adder-cost: 8   maxlim: 3   bits: 3/2
c ---[ 179]---> Adder-cost: 30   maxlim: 13   bits: 5/4
c ---[ 178]---> Adder-cost: 8   maxlim: 3   bits: 3/2
c ---[ 177]---> Adder-cost: 8   maxlim: 3   bits: 3/2
c ---[ 176]---> Adder-cost: 8   maxlim: 3   bits: 3/2
c ---[ 175]---> Adder-cost: 8   maxlim: 3   bits: 3/2
c ---[ 174]---> Adder-cost: 8   maxlim: 3   bits: 3/2
c ---[ 173]---> Adder-cost: 8   maxlim: 3   bits: 3/2
c ---[ 172]---> Adder-cost: 8   maxlim: 3   bits: 3/2
c ---[ 171]---> Adder-cost: 8   maxlim: 3   bits: 3/2
c ---[ 170]---> Adder-cost: 8   maxlim: 3   bits: 3/2
c ---[ 169]---> Adder-cost: 8   maxlim: 3   bits: 3/2
c ---[ 168]---> Adder-cost: 30   maxlim: 13   bits: 5/4
c ---[ 167]---> Adder-cost: 8   maxlim: 3   bits: 3/2
c ---[ 166]---> Adder-cost: 8   maxlim: 3   bits: 3/2
c ---[ 165]---> Adder-cost: 8   maxlim: 3   bits: 3/2
c ---[ 164]---> Adder-cost: 8   maxlim: 3   bits: 3/2
c ---[ 163]---> Adder-cost: 8   maxlim: 3   bits: 3/2
c ---[ 162]---> Adder-cost: 8   maxlim: 3   bits: 3/2
c ---[ 161]---> Adder-cost: 8   maxlim: 3   bits: 3/2
c ---[ 160]---> Adder-cost: 190   maxlim: 87   bits: 7/7
c ---[ 159]---> Adder-cost: 30   maxlim: 13   bits: 5/4
c ---[ 158]---> Adder-cost: 30   maxlim: 13   bits: 5/4
c ---[ 157]---> Adder-cost: 30   maxlim: 13   bits: 5/4
c ---[ 156]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 155]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 154]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 153]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 152]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 151]---> Adder-cost: 30   maxlim: 13   bits: 5/4
c ---[ 150]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 149]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 148]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 147]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 146]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 145]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 144]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 143]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 142]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 141]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 140]---> Adder-cost: 30   maxlim: 13   bits: 5/4
c ---[ 139]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 138]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 137]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 136]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 135]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 134]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 133]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 132]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 131]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 130]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 129]---> Adder-cost: 30   maxlim: 13   bits: 5/4
c ---[ 128]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 127]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 126]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 125]---> Adder-cost: 30   maxlim: 13   bits: 5/4
c ---[ 124]---> Adder-cost: 30   maxlim: 13   bits: 5/4
c ---[ 123]---> Adder-cost: 30   maxlim: 13   bits: 5/4
c ---[ 113]---> Adder-cost: 30   maxlim: 13   bits: 5/4
c ---[ 102]---> Adder-cost: 20   maxlim: 47   bits: 7/6
c ---[ 101]---> Adder-cost: 46   maxlim: 52   bits: 7/6
c ---[ 100]---> Adder-cost: 46   maxlim: 52   bits: 7/6
c ---[  99]---> Adder-cost: 15   maxlim: 46   bits: 7/6
c ---[  98]---> Adder-cost: 20   maxlim: 47   bits: 7/6
c ---[  97]---> Adder-cost: 23   maxlim: 48   bits: 7/6
c ---[  96]---> Adder-cost: 67   maxlim: 55   bits: 7/6
c ---[  95]---> Adder-cost: 43   maxlim: 51   bits: 7/6
c ---[  94]---> Adder-cost: 20   maxlim: 47   bits: 7/6
c ---[  93]---> Adder-cost: 9   maxlim: 45   bits: 7/6
c ---[  92]---> Adder-cost: 64   maxlim: 54   bits: 7/6
c ---[  91]---> Adder-cost: 46   maxlim: 52   bits: 7/6
c ---[  90]---> Adder-cost: 74   maxlim: 56   bits: 7/6
c ---[  89]---> Adder-cost: 117   maxlim: 62   bits: 7/6
c ---[  88]---> Adder-cost: 30   maxlim: 49   bits: 7/6
c ---[  87]---> Adder-cost: 67   maxlim: 55   bits: 7/6
c ---[  86]---> Adder-cost: 34   maxlim: 50   bits: 7/6
c ---[  85]---> Adder-cost: 103   maxlim: 60   bits: 7/6
c ---[  84]---> Adder-cost: 20   maxlim: 47   bits: 7/6
c ---[  83]---> Adder-cost: 23   maxlim: 48   bits: 7/6
c ---[  82]---> Adder-cost: 51   maxlim: 53   bits: 7/6
c ---[  81]---> Adder-cost: 43   maxlim: 51   bits: 7/6
c ---[  80]---> Adder-cost: 15   maxlim: 46   bits: 7/6
c ---[  79]---> Adder-cost: 9   maxlim: 45   bits: 7/6
c ---[  78]---> Adder-cost: 76   maxlim: 57   bits: 7/6
c ---[  77]---> Adder-cost: 76   maxlim: 57   bits: 7/6
c ---[  76]---> Adder-cost: 43   maxlim: 51   bits: 7/6
c ---[  75]---> Adder-cost: 74   maxlim: 56   bits: 7/6
c ---[  74]---> Adder-cost: 34   maxlim: 50   bits: 7/6
c ---[  73]---> Adder-cost: 67   maxlim: 55   bits: 7/6
c ---[  72]---> Adder-cost: 43   maxlim: 51   bits: 7/6
c ---[  71]---> Adder-cost: 67   maxlim: 55   bits: 7/6
c ---[  70]---> Adder-cost: 74   maxlim: 56   bits: 7/6
c ---[  69]---> Adder-cost: 74   maxlim: 56   bits: 7/6
c ---[  68]---> Adder-cost: 15   maxlim: 46   bits: 7/6
c ---[  67]---> Adder-cost: 34   maxlim: 50   bits: 7/6
c ---[  66]---> Adder-cost: 30   maxlim: 49   bits: 7/6
c ---[  65]---> Adder-cost: 94   maxlim: 59   bits: 7/6
c ---[  64]---> Adder-cost: 51   maxlim: 53   bits: 7/6
c ---[  63]---> Adder-cost: 9   maxlim: 45   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: 30   maxlim: 49   bits: 7/6
c ---[  59]---> Adder-cost: 46   maxlim: 52   bits: 7/6
c ---[  58]---> Adder-cost: 67   maxlim: 55   bits: 7/6
c ---[  57]---> Adder-cost: 9   maxlim: 45   bits: 7/6
c ---[  56]---> Adder-cost: 46   maxlim: 52   bits: 7/6
c ---[  55]---> Adder-cost: 103   maxlim: 60   bits: 7/6
c ---[  54]---> Adder-cost: 30   maxlim: 49   bits: 7/6
c ---[  53]---> Adder-cost: 30   maxlim: 49   bits: 7/6
c ---[  52]---> Adder-cost: 30   maxlim: 49   bits: 7/6
c ---[  51]---> Adder-cost: 74   maxlim: 56   bits: 7/6
c ---[  50]---> Adder-cost: 85   maxlim: 58   bits: 7/6
c ---[  49]---> Adder-cost: 30   maxlim: 49   bits: 7/6
c ---[  48]---> Adder-cost: 74   maxlim: 56   bits: 7/6
c ---[  47]---> Adder-cost: 74   maxlim: 56   bits: 7/6
c ---[  46]---> Adder-cost: 34   maxlim: 50   bits: 7/6
c ---[  45]---> Adder-cost: 30   maxlim: 49   bits: 7/6
c ---[  44]---> Adder-cost: 74   maxlim: 56   bits: 7/6
c ---[  43]---> Adder-cost: 34   maxlim: 50   bits: 7/6
c ---[  42]---> Adder-cost: 23   maxlim: 48   bits: 7/6
c ---[  41]---> Adder-cost: 9   maxlim: 45   bits: 7/6
c ---[  40]---> Adder-cost: 118   maxlim: 63   bits: 7/6
c ---[  39]---> Adder-cost: 74   maxlim: 56   bits: 7/6
c ---[  38]---> Adder-cost: 117   maxlim: 62   bits: 7/6
c ---[  37]---> Adder-cost: 23   maxlim: 48   bits: 7/6
c ---[  36]---> Adder-cost: 67   maxlim: 55   bits: 7/6
c ---[  35]---> Adder-cost: 94   maxlim: 59   bits: 7/6
c ---[  34]---> Adder-cost: 46   maxlim: 52   bits: 7/6
c ---[  33]---> Adder-cost: 118   maxlim: 63   bits: 7/6
c ---[  32]---> Adder-cost: 67   maxlim: 55   bits: 7/6
c ---[  31]---> Adder-cost: 30   maxlim: 49   bits: 7/6
c ---[  30]---> Adder-cost: 43   maxlim: 51   bits: 7/6
c ---[  29]---> Adder-cost: 20   maxlim: 47   bits: 7/6
c ---[  28]---> Adder-cost: 104   maxlim: 61   bits: 7/6
c ---[  27]---> Adder-cost: 15   maxlim: 46   bits: 7/6
c ---[  26]---> Adder-cost: 64   maxlim: 54   bits: 7/6
c ---[  25]---> Adder-cost: 43   maxlim: 51   bits: 7/6
c ---[  24]---> Adder-cost: 64   maxlim: 54   bits: 7/6
c ---[  23]---> Adder-cost: 76   maxlim: 57   bits: 7/6
c ---[  22]---> Adder-cost: 20   maxlim: 47   bits: 7/6
c ---[  21]---> Adder-cost: 9   maxlim: 45   bits: 7/6
c ---[  20]---> Adder-cost: 67   maxlim: 55   bits: 7/6
c ---[  19]---> Adder-cost: 46   maxlim: 52   bits: 7/6
c ---[  18]---> Adder-cost: 9   maxlim: 45   bits: 7/6
c ---[  17]---> Adder-cost: 43   maxlim: 51   bits: 7/6
c ---[  16]---> Adder-cost: 51   maxlim: 53   bits: 7/6
c ---[  15]---> Adder-cost: 20   maxlim: 47   bits: 7/6
c ---[  14]---> Adder-cost: 43   maxlim: 51   bits: 7/6
c ---[  13]---> Adder-cost: 9   maxlim: 45   bits: 7/6
c ---[  12]---> Adder-cost: 103   maxlim: 60   bits: 7/6
c ---[  11]---> Adder-cost: 15   maxlim: 46   bits: 7/6
c ---[  10]---> Adder-cost: 74   maxlim: 56   bits: 7/6
c ---[   9]---> Adder-cost: 85   maxlim: 58   bits: 7/6
c ---[   8]---> Adder-cost: 76   maxlim: 57   bits: 7/6
c ---[   7]---> Adder-cost: 51   maxlim: 53   bits: 7/6
c ---[   6]---> Adder-cost: 85   maxlim: 58   bits: 7/6
c ---[   5]---> Adder-cost: 64   maxlim: 54   bits: 7/6
c ---[   4]---> Adder-cost: 34   maxlim: 50   bits: 7/6
c ---[   3]---> Adder-cost: 74   maxlim: 56   bits: 7/6
c ---[   2]---> Adder-cost: 103   maxlim: 60   bits: 7/6
c ---[   1]---> Adder-cost: 103   maxlim: 60   bits: 7/6
c ---[   0]---> Adder-cost: 64   maxlim: 54   bits: 7/6
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |  939742  3345077 |  313247       0        0     nan |  0.000 % |
c |       100 |  939742  3345077 |  344571     100      882     8.8 |  4.490 % |
c |       251 |  939735  3345054 |  379028     250     2114     8.5 |  4.491 % |
c |       477 |  939564  3344469 |  416931     457     3749     8.2 |  4.510 % |
c |       814 |  939551  3344428 |  458624     792     5681     7.2 |  4.511 % |
c |      1320 |  939189  3343198 |  504487    1260     9076     7.2 |  4.552 % |
c |      2081 |  939070  3342801 |  554936    2007    14144     7.0 |  4.566 % |
c |      3220 |  938211  3339804 |  610429    2996    24660     8.2 |  4.638 % |
c |      4928 |  936896  3335280 |  671472    4507    48790    10.8 |  4.756 % |
c |      7490 |  936688  3334554 |  738620    7035   112389    16.0 |  4.776 % |
c |     11334 |  936688  3334554 |  812482   10879   200195    18.4 |  4.776 % |
c |     17100 |  936672  3334502 |  893730   16641   348821    21.0 |  4.778 % |
c |     25749 |  934574  3327162 |  983103   24588   553369    22.5 |  4.937 % |
c |     38723 |  932159  3318732 | 1081413   37057   909252    24.5 |  5.143 % |
c |     58185 |  932153  3318714 | 1189554   56519  1430263    25.3 |  5.143 % |
c |     87378 |  928623  3306355 | 1308510   67968  1567214    23.1 |  5.411 % |
c |    131167 |  926017  3297165 | 1439361  100852  2250634    22.3 |  5.564 % |
c |    196851 |  920628  3278301 | 1583297  157978  3742273    23.7 |  6.017 % |
c |    295377 |  898646  3200703 | 1741627  234569  5493166    23.4 |  7.604 % |
#### 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.70 0.93 0.90 2/54 7768
Raw data (stat): 7768 (runsolver) R 7767 10720 10719 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 484910137 1052672 99 4294967295 134512640 135381576 3221224448 3221219692 135158418 0 2147483391 7 90112 0 0 0 17 1 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+9.9999 s]
Raw data (loadavg): 0.75 0.93 0.91 2/54 7768
Raw data (stat): 7768 (minisat+) R 7767 10720 10719 0 -1 0 17519 0 0 0 958 41 0 0 25 0 1 0 484910137 79413248 16786 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19388 16786 603 41 0 19347 0
vsize: 77552
[startup+20.0011 s]
Raw data (loadavg): 0.79 0.93 0.91 2/54 7768
Raw data (stat): 7768 (minisat+) R 7767 10720 10719 0 -1 0 17586 0 0 0 1957 41 0 0 25 0 1 0 484910137 79683584 16853 4294967295 134512640 134672761 3221224544 3221223748 134561964 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19454 16853 603 41 0 19413 0
vsize: 77816
[startup+30.0015 s]
Raw data (loadavg): 0.82 0.93 0.91 2/54 7768
Raw data (stat): 7768 (minisat+) R 7767 10720 10719 0 -1 0 17627 0 0 0 2957 42 0 0 25 0 1 0 484910137 79831040 16894 4294967295 134512640 134672761 3221224544 3221223716 134556651 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19490 16894 603 41 0 19449 0
vsize: 77960
[startup+40.0023 s]
Raw data (loadavg): 0.85 0.94 0.91 2/54 7768
Raw data (stat): 7768 (minisat+) R 7767 10720 10719 0 -1 0 17664 0 0 0 3956 42 0 0 25 0 1 0 484910137 79966208 16931 4294967295 134512640 134672761 3221224544 3221223748 134561964 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19523 16931 603 41 0 19482 0
vsize: 78092
[startup+50.0036 s]
Raw data (loadavg): 0.87 0.94 0.91 2/54 7768
Raw data (stat): 7768 (minisat+) R 7767 10720 10719 0 -1 0 17708 0 0 0 4956 43 0 0 25 0 1 0 484910137 80232448 16975 4294967295 134512640 134672761 3221224544 3221223716 134556646 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19588 16975 603 41 0 19547 0
vsize: 78352
[startup+60.003 s]
Raw data (loadavg): 0.89 0.94 0.91 2/54 7770
Raw data (stat): 7768 (minisat+) R 7767 10720 10719 0 -1 0 17754 0 0 0 5956 43 0 0 25 0 1 0 484910137 80367616 17021 4294967295 134512640 134672761 3221224544 3221223716 134556682 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19621 17021 603 41 0 19580 0
vsize: 78484
[startup+70.0039 s]
Raw data (loadavg): 0.91 0.94 0.91 2/54 7770
Raw data (stat): 7768 (minisat+) R 7767 10720 10719 0 -1 0 18271 0 0 0 6953 46 0 0 25 0 1 0 484910137 82497536 17538 4294967295 134512640 134672761 3221224544 3221223712 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20141 17538 603 41 0 20100 0
vsize: 80564
[startup+80.0051 s]
Raw data (loadavg): 0.92 0.94 0.91 2/54 7770
Raw data (stat): 7768 (minisat+) R 7767 10720 10719 0 -1 0 18404 0 0 0 7953 46 0 0 25 0 1 0 484910137 83038208 17671 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20273 17671 603 41 0 20232 0
vsize: 81092
[startup+90.0055 s]
Raw data (loadavg): 0.93 0.94 0.91 2/54 7770
Raw data (stat): 7768 (minisat+) R 7767 10720 10719 0 -1 0 18466 0 0 0 8952 47 0 0 25 0 1 0 484910137 83308544 17733 4294967295 134512640 134672761 3221224544 3221223716 134556688 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20339 17733 603 41 0 20298 0
vsize: 81356
[startup+100.005 s]
Raw data (loadavg): 0.94 0.94 0.91 2/54 7770
Raw data (stat): 7768 (minisat+) R 7767 10720 10719 0 -1 0 18526 0 0 0 9952 47 0 0 25 0 1 0 484910137 83578880 17793 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20405 17793 603 41 0 20364 0
vsize: 81620
[startup+110.006 s]
Raw data (loadavg): 0.95 0.95 0.91 2/54 7770
Raw data (stat): 7768 (minisat+) R 7767 10720 10719 0 -1 0 18554 0 0 0 10952 47 0 0 25 0 1 0 484910137 83714048 17821 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20438 17821 603 41 0 20397 0
vsize: 81752
[startup+120.007 s]
Raw data (loadavg): 0.96 0.95 0.91 2/54 7770
Raw data (stat): 7768 (minisat+) R 7767 10720 10719 0 -1 0 18610 0 0 0 11952 48 0 0 25 0 1 0 484910137 83984384 17877 4294967295 134512640 134672761 3221224544 3221223716 134556688 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20504 17877 603 41 0 20463 0
vsize: 82016
[startup+130.007 s]
Raw data (loadavg): 0.96 0.95 0.91 2/54 7770
Raw data (stat): 7768 (minisat+) R 7767 10720 10719 0 -1 0 18637 0 0 0 12952 48 0 0 25 0 1 0 484910137 83984384 17904 4294967295 134512640 134672761 3221224544 3221223760 134561997 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20504 17904 603 41 0 20463 0
vsize: 82016
[startup+140.008 s]
Raw data (loadavg): 0.97 0.95 0.91 2/54 7770
Raw data (stat): 7768 (minisat+) R 7767 10720 10719 0 -1 0 18647 0 0 0 13952 48 0 0 25 0 1 0 484910137 84119552 17914 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20537 17914 603 41 0 20496 0
vsize: 82148
[startup+150.009 s]
Raw data (loadavg): 0.97 0.95 0.91 2/54 7770
Raw data (stat): 7768 (minisat+) R 7767 10720 10719 0 -1 0 19193 0 0 0 14950 50 0 0 25 0 1 0 484910137 86392832 18460 4294967295 134512640 134672761 3221224544 3221223712 134561121 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21092 18460 603 41 0 21051 0
vsize: 84368
[startup+160.008 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 7770
Raw data (stat): 7768 (minisat+) R 7767 10720 10719 0 -1 0 19632 0 0 0 15948 52 0 0 25 0 1 0 484910137 88227840 18899 4294967295 134512640 134672761 3221224544 3221223712 134560813 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21540 18899 603 41 0 21499 0
vsize: 86160
[startup+170.009 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 7770
Raw data (stat): 7768 (minisat+) R 7767 10720 10719 0 -1 0 19900 0 0 0 16947 54 0 0 25 0 1 0 484910137 89354240 19167 4294967295 134512640 134672761 3221224544 3221223716 134556639 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21815 19167 603 41 0 21774 0
vsize: 87260
[startup+180.009 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 7770
Raw data (stat): 7768 (minisat+) R 7767 10720 10719 0 -1 0 19938 0 0 0 17947 54 0 0 25 0 1 0 484910137 89501696 19205 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21851 19205 603 41 0 21810 0
vsize: 87404
[startup+190.01 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 7770
Raw data (stat): 7768 (minisat+) R 7767 10720 10719 0 -1 0 19938 0 0 0 18946 55 0 0 25 0 1 0 484910137 89501696 19205 4294967295 134512640 134672761 3221224544 3221223748 134561964 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21851 19205 603 41 0 21810 0
vsize: 87404
[startup+200.01 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 7770
Raw data (stat): 7768 (minisat+) R 7767 10720 10719 0 -1 0 19938 0 0 0 19946 55 0 0 25 0 1 0 484910137 89501696 19205 4294967295 134512640 134672761 3221224544 3221223716 134556682 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21851 19205 603 41 0 21810 0
vsize: 87404
[startup+210.01 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 7770
Raw data (stat): 7768 (minisat+) R 7767 10720 10719 0 -1 0 19938 0 0 0 20946 55 0 0 25 0 1 0 484910137 89501696 19205 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21851 19205 603 41 0 21810 0
vsize: 87404
[startup+220.01 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 7770
Raw data (stat): 7768 (minisat+) R 7767 10720 10719 0 -1 0 19938 0 0 0 21946 55 0 0 25 0 1 0 484910137 89501696 19205 4294967295 134512640 134672761 3221224544 3221223716 134556664 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21851 19205 603 41 0 21810 0
vsize: 87404
[startup+230.011 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 7770
Raw data (stat): 7768 (minisat+) R 7767 10720 10719 0 -1 0 19938 0 0 0 22946 56 0 0 25 0 1 0 484910137 89501696 19205 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21851 19205 603 41 0 21810 0
vsize: 87404
[startup+240.011 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 7770
Raw data (stat): 7768 (minisat+) R 7767 10720 10719 0 -1 0 19973 0 0 0 23946 56 0 0 25 0 1 0 484910137 89636864 19240 4294967295 134512640 134672761 3221224544 3221223728 134558656 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21884 19240 603 41 0 21843 0
vsize: 87536
[startup+250.011 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 7770
Raw data (stat): 7768 (minisat+) R 7767 10720 10719 0 -1 0 20381 0 0 0 24945 57 0 0 25 0 1 0 484910137 91512832 19648 4294967295 134512640 134672761 3221224544 3221223712 134561164 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22342 19648 603 41 0 22301 0
vsize: 89368
[startup+260.011 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 7770
Raw data (stat): 7768 (minisat+) R 7767 10720 10719 0 -1 0 20610 0 0 0 25944 57 0 0 25 0 1 0 484910137 92487680 19877 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22580 19877 603 41 0 22539 0
vsize: 90320
[startup+270.012 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 7770
Raw data (stat): 7768 (minisat+) R 7767 10720 10719 0 -1 0 20663 0 0 0 26944 58 0 0 25 0 1 0 484910137 92753920 19930 4294967295 134512640 134672761 3221224544 3221223716 134556660 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22645 19930 603 41 0 22604 0
vsize: 90580
[startup+280.011 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 7770
Raw data (stat): 7768 (minisat+) R 7767 10720 10719 0 -1 0 20724 0 0 0 27944 58 0 0 25 0 1 0 484910137 92901376 19991 4294967295 134512640 134672761 3221224544 3221223760 134561999 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22681 19991 603 41 0 22640 0
vsize: 90724
[startup+290.013 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 7770
Raw data (stat): 7768 (minisat+) R 7767 10720 10719 0 -1 0 20737 0 0 0 28944 58 0 0 25 0 1 0 484910137 93036544 20004 4294967295 134512640 134672761 3221224544 3221223648 134560248 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22714 20004 603 41 0 22673 0
vsize: 90856
[startup+300.013 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 7770
Raw data (stat): 7768 (minisat+) R 7767 10720 10719 0 -1 0 20791 0 0 0 29943 59 0 0 25 0 1 0 484910137 93306880 20058 4294967295 134512640 134672761 3221224544 3221223712 134560912 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22780 20058 603 41 0 22739 0
vsize: 91120
[startup+310.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7770
Raw data (stat): 7768 (minisat+) R 7767 10720 10719 0 -1 0 20813 0 0 0 30943 59 0 0 25 0 1 0 484910137 93306880 20080 4294967295 134512640 134672761 3221224544 3221223712 134561207 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22780 20080 603 41 0 22739 0
vsize: 91120
[startup+320.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7770
Raw data (stat): 7768 (minisat+) R 7767 10720 10719 0 -1 0 21205 0 0 0 31943 60 0 0 25 0 1 0 484910137 94928896 20472 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23176 20472 603 41 0 23135 0
vsize: 92704
[startup+330.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7770
Raw data (stat): 7768 (minisat+) R 7767 10720 10719 0 -1 0 21503 0 0 0 32942 61 0 0 25 0 1 0 484910137 96133120 20770 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23470 20770 603 41 0 23429 0
vsize: 93880
[startup+340.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7770
Raw data (stat): 7768 (minisat+) R 7767 10720 10719 0 -1 0 21772 0 0 0 33942 62 0 0 25 0 1 0 484910137 97259520 21039 4294967295 134512640 134672761 3221224544 3221223712 134560994 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23745 21039 603 41 0 23704 0
vsize: 94980
[startup+350.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7770
Raw data (stat): 7768 (minisat+) R 7767 10720 10719 0 -1 0 21882 0 0 0 34942 62 0 0 25 0 1 0 484910137 97673216 21149 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23846 21149 603 41 0 23805 0
vsize: 95384
[startup+360.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7770
Raw data (stat): 7768 (minisat+) R 7767 10720 10719 0 -1 0 21931 0 0 0 35941 62 0 0 25 0 1 0 484910137 97955840 21198 4294967295 134512640 134672761 3221224544 3221223716 134556667 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23915 21198 603 41 0 23874 0
vsize: 95660
[startup+370.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7770
Raw data (stat): 7768 (minisat+) R 7767 10720 10719 0 -1 0 21949 0 0 0 36941 62 0 0 25 0 1 0 484910137 97955840 21216 4294967295 134512640 134672761 3221224544 3221223748 134561964 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23915 21216 603 41 0 23874 0
vsize: 95660
[startup+380.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7770
Raw data (stat): 7768 (minisat+) R 7767 10720 10719 0 -1 0 22003 0 0 0 37941 63 0 0 25 0 1 0 484910137 98246656 21270 4294967295 134512640 134672761 3221224544 3221223744 134561972 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23986 21270 603 41 0 23945 0
vsize: 95944
[startup+390.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7770
Raw data (stat): 7768 (minisat+) R 7767 10720 10719 0 -1 0 22013 0 0 0 38941 63 0 0 25 0 1 0 484910137 98246656 21280 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23986 21280 603 41 0 23945 0
vsize: 95944
[startup+400.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7770
Raw data (stat): 7768 (minisat+) R 7767 10720 10719 0 -1 0 22017 0 0 0 39941 64 0 0 25 0 1 0 484910137 98246656 21284 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23986 21284 603 41 0 23945 0
vsize: 95944
[startup+410.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7770
Raw data (stat): 7768 (minisat+) R 7767 10720 10719 0 -1 0 22073 0 0 0 40940 64 0 0 25 0 1 0 484910137 98512896 21340 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24051 21340 603 41 0 24010 0
vsize: 96204
[startup+420.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7770
Raw data (stat): 7768 (minisat+) R 7767 10720 10719 0 -1 0 22115 0 0 0 41940 65 0 0 25 0 1 0 484910137 98648064 21382 4294967295 134512640 134672761 3221224544 3221223716 134556627 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24084 21382 603 41 0 24043 0
vsize: 96336
[startup+430.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7770
Raw data (stat): 7768 (minisat+) R 7767 10720 10719 0 -1 0 22642 0 0 0 42938 66 0 0 25 0 1 0 484910137 100806656 21909 4294967295 134512640 134672761 3221224544 3221223712 134560929 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24611 21909 603 41 0 24570 0
vsize: 98444
[startup+440.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7770
Raw data (stat): 7768 (minisat+) R 7767 10720 10719 0 -1 0 23038 0 0 0 43937 67 0 0 25 0 1 0 484910137 102961152 22305 4294967295 134512640 134672761 3221224544 3221223712 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25137 22305 603 41 0 25096 0
vsize: 100548
[startup+450.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7770
Raw data (stat): 7768 (minisat+) R 7767 10720 10719 0 -1 0 23350 0 0 0 44935 70 0 0 25 0 1 0 484910137 104165376 22617 4294967295 134512640 134672761 3221224544 3221223712 134560988 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25431 22617 603 41 0 25390 0
vsize: 101724
[startup+460.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7770
Raw data (stat): 7768 (minisat+) R 7767 10720 10719 0 -1 0 23486 0 0 0 45935 70 0 0 25 0 1 0 484910137 104861696 22753 4294967295 134512640 134672761 3221224544 3221223712 134560937 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25601 22753 603 41 0 25560 0
vsize: 102404
[startup+470.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7770
Raw data (stat): 7768 (minisat+) R 7767 10720 10719 0 -1 0 23690 0 0 0 46934 71 0 0 25 0 1 0 484910137 105689088 22957 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25803 22957 603 41 0 25762 0
vsize: 103212
[startup+480.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7770
Raw data (stat): 7768 (minisat+) R 7767 10720 10719 0 -1 0 23847 0 0 0 47933 72 0 0 25 0 1 0 484910137 106373120 23114 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25970 23114 603 41 0 25929 0
vsize: 103880
[startup+490.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7770
Raw data (stat): 7768 (minisat+) R 7767 10720 10719 0 -1 0 23878 0 0 0 48932 73 0 0 25 0 1 0 484910137 106520576 23145 4294967295 134512640 134672761 3221224544 3221223740 134556584 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26006 23145 603 41 0 25965 0
vsize: 104024
[startup+500.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7770
Raw data (stat): 7768 (minisat+) R 7767 10720 10719 0 -1 0 23904 0 0 0 49932 73 0 0 25 0 1 0 484910137 106655744 23171 4294967295 134512640 134672761 3221224544 3221223712 134561164 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26039 23171 603 41 0 25998 0
vsize: 104156
[startup+510.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7770
Raw data (stat): 7768 (minisat+) R 7767 10720 10719 0 -1 0 23919 0 0 0 50932 73 0 0 25 0 1 0 484910137 106655744 23186 4294967295 134512640 134672761 3221224544 3221223744 134561967 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26039 23186 603 41 0 25998 0
vsize: 104156
[startup+520.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7770
Raw data (stat): 7768 (minisat+) R 7767 10720 10719 0 -1 0 23930 0 0 0 51932 73 0 0 25 0 1 0 484910137 106655744 23197 4294967295 134512640 134672761 3221224544 3221223716 134556632 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26039 23197 603 41 0 25998 0
vsize: 104156
[startup+530.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7770
Raw data (stat): 7768 (minisat+) R 7767 10720 10719 0 -1 0 24031 0 0 0 52932 74 0 0 25 0 1 0 484910137 107057152 23298 4294967295 134512640 134672761 3221224544 3221223712 134561190 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26137 23298 603 41 0 26096 0
vsize: 104548
[startup+540.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7770
Raw data (stat): 7768 (minisat+) R 7767 10720 10719 0 -1 0 24220 0 0 0 53931 74 0 0 25 0 1 0 484910137 107859968 23487 4294967295 134512640 134672761 3221224544 3221223748 134561964 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26333 23487 603 41 0 26292 0
vsize: 105332
[startup+550.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7770
Raw data (stat): 7768 (minisat+) R 7767 10720 10719 0 -1 0 24241 0 0 0 54931 75 0 0 25 0 1 0 484910137 108019712 23508 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26372 23508 603 41 0 26331 0
vsize: 105488
[startup+560.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7770
Raw data (stat): 7768 (minisat+) R 7767 10720 10719 0 -1 0 24252 0 0 0 55931 75 0 0 25 0 1 0 484910137 108019712 23519 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26372 23519 603 41 0 26331 0
vsize: 105488
[startup+570.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7770
Raw data (stat): 7768 (minisat+) R 7767 10720 10719 0 -1 0 24282 0 0 0 56930 76 0 0 25 0 1 0 484910137 108150784 23549 4294967295 134512640 134672761 3221224544 3221223716 134556627 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26404 23549 603 41 0 26363 0
vsize: 105616
[startup+580.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7770
Raw data (stat): 7768 (minisat+) R 7767 10720 10719 0 -1 0 24306 0 0 0 57930 76 0 0 25 0 1 0 484910137 108285952 23573 4294967295 134512640 134672761 3221224544 3221223716 134556639 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26437 23573 603 41 0 26396 0
vsize: 105748
[startup+590.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7770
Raw data (stat): 7768 (minisat+) R 7767 10720 10719 0 -1 0 24716 0 0 0 58929 77 0 0 25 0 1 0 484910137 109895680 23983 4294967295 134512640 134672761 3221224544 3221223760 134561950 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26830 23983 603 41 0 26789 0
vsize: 107320
[startup+600.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7770
Raw data (stat): 7768 (minisat+) R 7767 10720 10719 0 -1 0 24760 0 0 0 59929 78 0 0 25 0 1 0 484910137 110030848 24027 4294967295 134512640 134672761 3221224544 3221223716 134556667 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26863 24027 603 41 0 26822 0
vsize: 107452
[startup+610.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7770
Raw data (stat): 7768 (minisat+) R 7767 10720 10719 0 -1 0 25355 0 0 0 60928 79 0 0 25 0 1 0 484910137 112451584 24622 4294967295 134512640 134672761 3221224544 3221223744 134561972 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27454 24622 603 41 0 27413 0
vsize: 109816
[startup+620.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7770
Raw data (stat): 7768 (minisat+) R 7767 10720 10719 0 -1 0 25553 0 0 0 61927 80 0 0 25 0 1 0 484910137 113266688 24820 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27653 24820 603 41 0 27612 0
vsize: 110612
[startup+630.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7770
Raw data (stat): 7768 (minisat+) R 7767 10720 10719 0 -1 0 25575 0 0 0 62927 80 0 0 25 0 1 0 484910137 113401856 24842 4294967295 134512640 134672761 3221224544 3221223716 134556688 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27686 24842 603 41 0 27645 0
vsize: 110744
[startup+640.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7770
Raw data (stat): 7768 (minisat+) R 7767 10720 10719 0 -1 0 25646 0 0 0 63927 80 0 0 25 0 1 0 484910137 113672192 24913 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27752 24913 603 41 0 27711 0
vsize: 111008
[startup+650.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7770
Raw data (stat): 7768 (minisat+) R 7767 10720 10719 0 -1 0 25665 0 0 0 64927 81 0 0 25 0 1 0 484910137 113672192 24932 4294967295 134512640 134672761 3221224544 3221223716 134556667 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27752 24932 603 41 0 27711 0
vsize: 111008
[startup+660.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7770
Raw data (stat): 7768 (minisat+) R 7767 10720 10719 0 -1 0 25704 0 0 0 65927 81 0 0 25 0 1 0 484910137 113942528 24971 4294967295 134512640 134672761 3221224544 3221223712 134564736 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27818 24971 603 41 0 27777 0
vsize: 111272
[startup+670.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7770
Raw data (stat): 7768 (minisat+) R 7767 10720 10719 0 -1 0 25708 0 0 0 66926 81 0 0 25 0 1 0 484910137 113942528 24975 4294967295 134512640 134672761 3221224544 3221223716 134556671 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27818 24975 603 41 0 27777 0
vsize: 111272
[startup+680.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7770
Raw data (stat): 7768 (minisat+) R 7767 10720 10719 0 -1 0 25751 0 0 0 67926 82 0 0 25 0 1 0 484910137 114077696 25018 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27851 25018 603 41 0 27810 0
vsize: 111404
[startup+690.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7770
Raw data (stat): 7768 (minisat+) R 7767 10720 10719 0 -1 0 25774 0 0 0 68926 82 0 0 25 0 1 0 484910137 114212864 25041 4294967295 134512640 134672761 3221224544 3221223716 134556649 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27884 25041 603 41 0 27843 0
vsize: 111536
[startup+700.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7770
Raw data (stat): 7768 (minisat+) R 7767 10720 10719 0 -1 0 25779 0 0 0 69926 82 0 0 25 0 1 0 484910137 114212864 25046 4294967295 134512640 134672761 3221224544 3221223744 134557885 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27884 25046 603 41 0 27843 0
vsize: 111536
[startup+710.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7770
Raw data (stat): 7768 (minisat+) R 7767 10720 10719 0 -1 0 25786 0 0 0 70926 82 0 0 25 0 1 0 484910137 114212864 25053 4294967295 134512640 134672761 3221224544 3221223716 134556688 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27884 25053 603 41 0 27843 0
vsize: 111536
[startup+720.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7770
Raw data (stat): 7768 (minisat+) R 7767 10720 10719 0 -1 0 25830 0 0 0 71926 83 0 0 25 0 1 0 484910137 114348032 25097 4294967295 134512640 134672761 3221224544 3221223716 134556632 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27917 25097 603 41 0 27876 0
vsize: 111668
[startup+730.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7770
Raw data (stat): 7768 (minisat+) R 7767 10720 10719 0 -1 0 25841 0 0 0 72926 83 0 0 25 0 1 0 484910137 114348032 25108 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27917 25108 603 41 0 27876 0
vsize: 111668
[startup+740.031 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7770
Raw data (stat): 7768 (minisat+) R 7767 10720 10719 0 -1 0 25846 0 0 0 73926 83 0 0 25 0 1 0 484910137 114479104 25113 4294967295 134512640 134672761 3221224544 3221223716 134556660 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27949 25113 603 41 0 27908 0
vsize: 111796
[startup+750.032 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7770
Raw data (stat): 7768 (minisat+) R 7767 10720 10719 0 -1 0 25884 0 0 0 74925 84 0 0 25 0 1 0 484910137 114614272 25151 4294967295 134512640 134672761 3221224544 3221223712 134560903 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27982 25151 603 41 0 27941 0
vsize: 111928
[startup+760.032 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7770
Raw data (stat): 7768 (minisat+) R 7767 10720 10719 0 -1 0 25922 0 0 0 75925 84 0 0 25 0 1 0 484910137 114745344 25189 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28014 25189 603 41 0 27973 0
vsize: 112056
[startup+770.032 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7770
Raw data (stat): 7768 (minisat+) R 7767 10720 10719 0 -1 0 25922 0 0 0 76925 84 0 0 25 0 1 0 484910137 114745344 25189 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28014 25189 603 41 0 27973 0
vsize: 112056
[startup+780.032 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7770
Raw data (stat): 7768 (minisat+) R 7767 10720 10719 0 -1 0 25922 0 0 0 77925 84 0 0 25 0 1 0 484910137 114745344 25189 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28014 25189 603 41 0 27973 0
vsize: 112056
[startup+790.033 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7770
Raw data (stat): 7768 (minisat+) R 7767 10720 10719 0 -1 0 25922 0 0 0 78925 84 0 0 25 0 1 0 484910137 114745344 25189 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28014 25189 603 41 0 27973 0
vsize: 112056
[startup+800.033 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7770
Raw data (stat): 7768 (minisat+) R 7767 10720 10719 0 -1 0 25922 0 0 0 79925 85 0 0 25 0 1 0 484910137 114745344 25189 4294967295 134512640 134672761 3221224544 3221223716 134556667 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28014 25189 603 41 0 27973 0
vsize: 112056
[startup+810.033 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7770
Raw data (stat): 7768 (minisat+) R 7767 10720 10719 0 -1 0 25922 0 0 0 80925 85 0 0 25 0 1 0 484910137 114745344 25189 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28014 25189 603 41 0 27973 0
vsize: 112056
[startup+820.034 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7770
Raw data (stat): 7768 (minisat+) R 7767 10720 10719 0 -1 0 25925 0 0 0 81925 85 0 0 25 0 1 0 484910137 114745344 25192 4294967295 134512640 134672761 3221224544 3221223680 134560718 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28014 25192 603 41 0 27973 0
vsize: 112056
[startup+830.034 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7770
Raw data (stat): 7768 (minisat+) R 7767 10720 10719 0 -1 0 25926 0 0 0 82925 85 0 0 25 0 1 0 484910137 114745344 25193 4294967295 134512640 134672761 3221224544 3221223744 134561967 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28014 25193 603 41 0 27973 0
vsize: 112056
[startup+840.034 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7770
Raw data (stat): 7768 (minisat+) R 7767 10720 10719 0 -1 0 25928 0 0 0 83925 85 0 0 25 0 1 0 484910137 114745344 25195 4294967295 134512640 134672761 3221224544 3221223760 134561993 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28014 25195 603 41 0 27973 0
vsize: 112056
[startup+850.035 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7770
Raw data (stat): 7768 (minisat+) R 7767 10720 10719 0 -1 0 25930 0 0 0 84925 86 0 0 25 0 1 0 484910137 114745344 25197 4294967295 134512640 134672761 3221224544 3221223668 134566082 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28014 25197 603 41 0 27973 0
vsize: 112056
[startup+860.035 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7770
Raw data (stat): 7768 (minisat+) R 7767 10720 10719 0 -1 0 25958 0 0 0 85924 87 0 0 25 0 1 0 484910137 114876416 25225 4294967295 134512640 134672761 3221224544 3221223716 134556667 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28046 25225 603 41 0 28005 0
vsize: 112184
[startup+870.036 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7770
Raw data (stat): 7768 (minisat+) R 7767 10720 10719 0 -1 0 25959 0 0 0 86924 87 0 0 25 0 1 0 484910137 114876416 25226 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28046 25226 603 41 0 28005 0
vsize: 112184
[startup+880.036 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7770
Raw data (stat): 7768 (minisat+) R 7767 10720 10719 0 -1 0 25959 0 0 0 87924 87 0 0 25 0 1 0 484910137 114876416 25226 4294967295 134512640 134672761 3221224544 3221223716 134556649 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28046 25226 603 41 0 28005 0
vsize: 112184
[startup+890.037 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7770
Raw data (stat): 7768 (minisat+) R 7767 10720 10719 0 -1 0 25959 0 0 0 88924 87 0 0 25 0 1 0 484910137 114876416 25226 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28046 25226 603 41 0 28005 0
vsize: 112184
[startup+900.037 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7770
Raw data (stat): 7768 (minisat+) R 7767 10720 10719 0 -1 0 25961 0 0 0 89924 87 0 0 25 0 1 0 484910137 114876416 25228 4294967295 134512640 134672761 3221224544 3221223752 134561960 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28046 25228 603 41 0 28005 0
vsize: 112184
[startup+910.037 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7770
Raw data (stat): 7768 (minisat+) R 7767 10720 10719 0 -1 0 25966 0 0 0 90925 87 0 0 25 0 1 0 484910137 114876416 25233 4294967295 134512640 134672761 3221224544 3221223696 134565127 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28046 25233 603 41 0 28005 0
vsize: 112184
[startup+920.038 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7770
Raw data (stat): 7768 (minisat+) R 7767 10720 10719 0 -1 0 26315 0 0 0 91923 88 0 0 25 0 1 0 484910137 116346880 25582 4294967295 134512640 134672761 3221224544 3221223516 1075358820 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28405 25582 603 41 0 28364 0
vsize: 113620
[startup+930.038 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7770
Raw data (stat): 7768 (minisat+) R 7767 10720 10719 0 -1 0 26574 0 0 0 92922 90 0 0 25 0 1 0 484910137 117321728 25841 4294967295 134512640 134672761 3221224544 3221223716 134556660 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28643 25841 603 41 0 28602 0
vsize: 114572
[startup+940.039 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7770
Raw data (stat): 7768 (minisat+) R 7767 10720 10719 0 -1 0 26699 0 0 0 93922 90 0 0 25 0 1 0 484910137 117870592 25966 4294967295 134512640 134672761 3221224544 3221223716 134556643 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28777 25966 603 41 0 28736 0
vsize: 115108
[startup+950.039 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7770
Raw data (stat): 7768 (minisat+) R 7767 10720 10719 0 -1 0 26715 0 0 0 94921 90 0 0 25 0 1 0 484910137 117870592 25982 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28777 25982 603 41 0 28736 0
vsize: 115108
[startup+960.039 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7770
Raw data (stat): 7768 (minisat+) R 7767 10720 10719 0 -1 0 26785 0 0 0 95921 91 0 0 25 0 1 0 484910137 118272000 26052 4294967295 134512640 134672761 3221224544 3221223716 134556632 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28875 26052 603 41 0 28834 0
vsize: 115500
[startup+970.039 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7770
Raw data (stat): 7768 (minisat+) R 7767 10720 10719 0 -1 0 26816 0 0 0 96921 91 0 0 25 0 1 0 484910137 118272000 26083 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28875 26083 603 41 0 28834 0
vsize: 115500
[startup+980.039 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7770
Raw data (stat): 7768 (minisat+) R 7767 10720 10719 0 -1 0 26845 0 0 0 97921 91 0 0 25 0 1 0 484910137 118407168 26112 4294967295 134512640 134672761 3221224544 3221223668 134566071 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28908 26112 603 41 0 28867 0
vsize: 115632
[startup+990.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7770
Raw data (stat): 7768 (minisat+) R 7767 10720 10719 0 -1 0 26879 0 0 0 98921 91 0 0 25 0 1 0 484910137 118538240 26146 4294967295 134512640 134672761 3221224544 3221223748 134561964 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28940 26146 603 41 0 28899 0
vsize: 115760
[startup+1000.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7770
Raw data (stat): 7768 (minisat+) R 7767 10720 10719 0 -1 0 26900 0 0 0 99921 92 0 0 25 0 1 0 484910137 118669312 26167 4294967295 134512640 134672761 3221224544 3221223748 134561964 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28972 26167 603 41 0 28931 0
vsize: 115888
[startup+1010.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7770
Raw data (stat): 7768 (minisat+) R 7767 10720 10719 0 -1 0 26911 0 0 0 100921 92 0 0 25 0 1 0 484910137 118669312 26178 4294967295 134512640 134672761 3221224544 3221223716 134556649 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28972 26178 603 41 0 28931 0
vsize: 115888
[startup+1020.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7770
Raw data (stat): 7768 (minisat+) R 7767 10720 10719 0 -1 0 26917 0 0 0 101921 92 0 0 25 0 1 0 484910137 118669312 26184 4294967295 134512640 134672761 3221224544 3221223748 134561964 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28972 26184 603 41 0 28931 0
vsize: 115888
[startup+1030.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7770
Raw data (stat): 7768 (minisat+) R 7767 10720 10719 0 -1 0 26929 0 0 0 102921 92 0 0 25 0 1 0 484910137 118804480 26196 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29005 26196 603 41 0 28964 0
vsize: 116020
[startup+1040.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7770
Raw data (stat): 7768 (minisat+) R 7767 10720 10719 0 -1 0 26931 0 0 0 103922 92 0 0 25 0 1 0 484910137 118804480 26198 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29005 26198 603 41 0 28964 0
vsize: 116020
[startup+1050.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7770
Raw data (stat): 7768 (minisat+) R 7767 10720 10719 0 -1 0 26932 0 0 0 104922 92 0 0 25 0 1 0 484910137 118804480 26199 4294967295 134512640 134672761 3221224544 3221223716 134556682 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29005 26199 603 41 0 28964 0
vsize: 116020
[startup+1060.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7770
Raw data (stat): 7768 (minisat+) R 7767 10720 10719 0 -1 0 26937 0 0 0 105922 92 0 0 25 0 1 0 484910137 118804480 26204 4294967295 134512640 134672761 3221224544 3221223716 134556680 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29005 26204 603 41 0 28964 0
vsize: 116020
[startup+1070.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7770
Raw data (stat): 7768 (minisat+) R 7767 10720 10719 0 -1 0 26937 0 0 0 106922 92 0 0 25 0 1 0 484910137 118804480 26204 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29005 26204 603 41 0 28964 0
vsize: 116020
[startup+1080.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7770
Raw data (stat): 7768 (minisat+) R 7767 10720 10719 0 -1 0 26939 0 0 0 107922 92 0 0 25 0 1 0 484910137 118804480 26206 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29005 26206 603 41 0 28964 0
vsize: 116020
[startup+1090.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7770
Raw data (stat): 7768 (minisat+) R 7767 10720 10719 0 -1 0 27002 0 0 0 108922 92 0 0 25 0 1 0 484910137 119070720 26269 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29070 26269 603 41 0 29029 0
vsize: 116280
[startup+1100.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7770
Raw data (stat): 7768 (minisat+) R 7767 10720 10719 0 -1 0 27026 0 0 0 109922 92 0 0 25 0 1 0 484910137 119205888 26293 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29103 26293 603 41 0 29062 0
vsize: 116412
[startup+1110.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7770
Raw data (stat): 7768 (minisat+) R 7767 10720 10719 0 -1 0 27028 0 0 0 110922 92 0 0 25 0 1 0 484910137 119205888 26295 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29103 26295 603 41 0 29062 0
vsize: 116412
[startup+1120.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7770
Raw data (stat): 7768 (minisat+) R 7767 10720 10719 0 -1 0 27032 0 0 0 111923 92 0 0 25 0 1 0 484910137 119205888 26299 4294967295 134512640 134672761 3221224544 3221223716 134556646 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29103 26299 603 41 0 29062 0
vsize: 116412
[startup+1130.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7770
Raw data (stat): 7768 (minisat+) R 7767 10720 10719 0 -1 0 27043 0 0 0 112923 92 0 0 25 0 1 0 484910137 119205888 26310 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29103 26310 603 41 0 29062 0
vsize: 116412
[startup+1140.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7770
Raw data (stat): 7768 (minisat+) R 7767 10720 10719 0 -1 0 27330 0 0 0 113922 93 0 0 25 0 1 0 484910137 120418304 26597 4294967295 134512640 134672761 3221224544 3221223648 134560180 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29399 26597 603 41 0 29358 0
vsize: 117596
[startup+1150.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7770
Raw data (stat): 7768 (minisat+) R 7767 10720 10719 0 -1 0 27604 0 0 0 114921 94 0 0 25 0 1 0 484910137 121491456 26871 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29661 26871 603 41 0 29620 0
vsize: 118644
[startup+1160.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7770
Raw data (stat): 7768 (minisat+) R 7767 10720 10719 0 -1 0 27615 0 0 0 115921 94 0 0 25 0 1 0 484910137 121491456 26882 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29661 26882 603 41 0 29620 0
vsize: 118644
[startup+1170.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7770
Raw data (stat): 7768 (minisat+) R 7767 10720 10719 0 -1 0 27636 0 0 0 116921 94 0 0 25 0 1 0 484910137 121622528 26903 4294967295 134512640 134672761 3221224544 3221223760 134561948 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29693 26903 603 41 0 29652 0
vsize: 118772
[startup+1180.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7770
Raw data (stat): 7768 (minisat+) R 7767 10720 10719 0 -1 0 27662 0 0 0 117921 94 0 0 25 0 1 0 484910137 121757696 26929 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29726 26929 603 41 0 29685 0
vsize: 118904
[startup+1190.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7770
Raw data (stat): 7768 (minisat+) R 7767 10720 10719 0 -1 0 27727 0 0 0 118921 95 0 0 25 0 1 0 484910137 122028032 26994 4294967295 134512640 134672761 3221224544 3221223748 134561964 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29792 26994 603 41 0 29751 0
vsize: 119168
[startup+1200.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7770
Raw data (stat): 7768 (minisat+) R 7767 10720 10719 0 -1 0 27751 0 0 0 119921 95 0 0 25 0 1 0 484910137 123076608 27018 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30048 27018 603 41 0 30007 0
vsize: 120192
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.1 s]
Raw data (loadavg): 0.99 0.97 0.91 1/54 7770
Raw data (stat): 7768 (minisat+) Z 7767 10720 10719 0 -1 12 27753 0 0 0 119921 100 0 0 25 0 1 0 484910137 0 0 4294967295 0 0 0 0 0 0 16384 5 16386 3222412051 0 0 17 1 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.1
CPU time (s): 1200.22
CPU user time (s): 1199.22
CPU system time (s): 1.00785
CPU usage (%): 100.01
Max. virtual memory (Kb): 120192
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####