PB'05 competition: run trace

Some explanations

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

Name	normalized-opb/mps-v2-13-7/plato.asu.edu/pub/unibo/normalized-mps-v2-13-7-sp97ar.opb
MD5SUM	978e3479aff123296d0a3461e698e01d
Bench Category	optimization, medium integers (OPTMEDINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	2147483647
Optimality of the best value was proved	NO
Number of terms in the objective function	14101
Biggest coefficient in the objective function	292878668
Number of bits for the biggest coefficient in the objective function	29
Sum of the numbers in the objective function	975388850291
Number of bits of the sum of numbers in the objective function	40
Biggest number in a constraint	292878668
Number of bits of the biggest number in a constraint	29
Biggest sum of numbers in a constraint	975388850291
Number of bits of the biggest sum of numbers	40
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	10.9833
Number of variables	14101
Total number of constraints	15862
Number of constraints which are clauses	181
Number of constraints which are cardinality constraints (but not clauses)	15263
Number of constraints which are nor clauses,nor cardinality constraints	418
Minimum length of a constraint	1
Maximum length of a constraint	2463
Trace number 13873

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

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.091
cache size	: 512 KB
fdiv_bug	: no
hlt_bug		: no
f00f_bug	: no
coma_bug	: no
fpu		: yes
fpu_exception	: yes
cpuid level	: 2
wp		: yes
flags		: fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse
bogomips	: 899.07

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        470184 kB
Buffers:         35524 kB
Cached:         505820 kB
SwapCached:          4 kB
Active:         230832 kB
Inactive:       313308 kB
HighTotal:      131008 kB
HighFree:          252 kB
LowTotal:       903652 kB
LowFree:        469932 kB
SwapTotal:     2097136 kB
SwapFree:      2097044 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6816 kB
Slab:            14744 kB
Committed_AS:    63584 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-20 22:27:27 (client local time) WITH STATUS 0 IN 1210.05 SECONDS
stats: 20238 7 1210.05 0
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 1739 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: ===========
c   -- Clauses(.)/Splits(s): s...s.ssssssss.ss........ss...ssss..ss.s..ss.s..s..ssssssssssss...s.s.ss.s.s..s.s..s..s...sss.ss.s...s.s.s..ssss..s.ss.s..ss.s.s......sss..ss.ss...sssss.s..ssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssss.ssssssssss.ssssssssssssssss.ssss..sss..s..s...sss...s.s..ssssss.ss.ssss.sss...s....ssssssss..s.ss....sssssss.s.sssssssssssssss.ss.ss.ssss.s..sssssssssss..ss.ssssss.sss.sss..ss..s...ss.s.ss.sss.ssssss...ss.sssssssss.sss.ss.ss.s.sssssssss.ssss..ss..s.ssss.s.s.....ssss...s.s..sssss.ss....s...s.
c ---[2139]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[2138]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[2137]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[2136]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[2135]---> Adder-cost: 22   maxlim: 12   bits: 4/4
c ---[2134]---> Adder-cost: 22   maxlim: 12   bits: 4/4
c ---[2133]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[2132]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[2130]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[2127]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[2126]---> Adder-cost: 8   maxlim: 5   bits: 3/3
c ---[2125]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[2124]---> Adder-cost: 8   maxlim: 5   bits: 3/3
c ---[2123]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[2122]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[2121]---> Adder-cost: 8   maxlim: 5   bits: 3/3
c ---[2120]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[2119]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[2117]---> Adder-cost: 30   maxlim: 15   bits: 5/4
c ---[2116]---> Adder-cost: 30   maxlim: 15   bits: 5/4
c ---[2115]---> Adder-cost: 20   maxlim: 10   bits: 4/4
c ---[2114]---> Adder-cost: 20   maxlim: 11   bits: 4/4
c ---[2113]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[2112]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[2111]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[2110]---> Adder-cost: 32   maxlim: 16   bits: 5/5
c ---[2109]---> Adder-cost: 30   maxlim: 14   bits: 5/4
c ---[2108]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[2106]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[2105]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[2104]---> Adder-cost: 32   maxlim: 16   bits: 5/5
c ---[2103]---> Adder-cost: 36   maxlim: 18   bits: 5/5
c ---[2102]---> Adder-cost: 36   maxlim: 18   bits: 5/5
c ---[2101]---> Adder-cost: 36   maxlim: 18   bits: 5/5
c ---[2100]---> Adder-cost: 36   maxlim: 18   bits: 5/5
c ---[2099]---> Adder-cost: 36   maxlim: 18   bits: 5/5
c ---[2098]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[2097]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[2095]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[2094]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[2093]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[2092]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[2091]---> Adder-cost: 20   maxlim: 11   bits: 4/4
c ---[2090]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[2089]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[2088]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[2087]---> Adder-cost: 30   maxlim: 14   bits: 5/4
c ---[2086]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[2084]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[2083]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[2082]---> Adder-cost: 30   maxlim: 15   bits: 5/4
c ---[2081]---> Adder-cost: 36   maxlim: 18   bits: 5/5
c ---[2080]---> Adder-cost: 30   maxlim: 15   bits: 5/4
c ---[2079]---> Adder-cost: 36   maxlim: 18   bits: 5/5
c ---[2078]---> Adder-cost: 8   maxlim: 5   bits: 3/3
c ---[2077]---> Adder-cost: 14   maxlim: 6   bits: 4/3
c ---[2076]---> Adder-cost: 14   maxlim: 6   bits: 4/3
c ---[2075]---> Adder-cost: 36   maxlim: 18   bits: 5/5
c ---[2073]---> Adder-cost: 36   maxlim: 18   bits: 5/5
c ---[2072]---> Adder-cost: 36   maxlim: 18   bits: 5/5
c ---[2071]---> Adder-cost: 36   maxlim: 18   bits: 5/5
c ---[2070]---> Adder-cost: 30   maxlim: 15   bits: 5/4
c ---[2069]---> Adder-cost: 36   maxlim: 18   bits: 5/5
c ---[2068]---> Adder-cost: 30   maxlim: 15   bits: 5/4
c ---[2067]---> Adder-cost: 36   maxlim: 18   bits: 5/5
c ---[2066]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[2065]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[2064]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[2062]---> Adder-cost: 8   maxlim: 5   bits: 3/3
c ---[2061]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[2060]---> Adder-cost: 30   maxlim: 15   bits: 5/4
c ---[2059]---> Adder-cost: 36   maxlim: 18   bits: 5/5
c ---[2058]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[2057]---> Adder-cost: 36   maxlim: 18   bits: 5/5
c ---[2056]---> Adder-cost: 30   maxlim: 14   bits: 5/4
c ---[2055]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[2054]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[2053]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[2051]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[2050]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[2049]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[2048]---> Adder-cost: 36   maxlim: 18   bits: 5/5
c ---[2047]---> Adder-cost: 8   maxlim: 5   bits: 3/3
c ---[2046]---> Adder-cost: 36   maxlim: 18   bits: 5/5
c ---[2045]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[2044]---> Adder-cost: 8   maxlim: 5   bits: 3/3
c ---[2043]---> Adder-cost: 20   maxlim: 11   bits: 4/4
c ---[2042]---> Adder-cost: 30   maxlim: 14   bits: 5/4
c ---[2040]---> Adder-cost: 36   maxlim: 18   bits: 5/5
c ---[2039]---> Adder-cost: 30   maxlim: 14   bits: 5/4
c ---[2038]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[2037]---> Adder-cost: 30   maxlim: 14   bits: 5/4
c ---[2036]---> Adder-cost: 36   maxlim: 18   bits: 5/5
c ---[2035]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[2034]---> Adder-cost: 30   maxlim: 14   bits: 5/4
c ---[2033]---> Adder-cost: 36   maxlim: 18   bits: 5/5
c ---[2032]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[2031]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[2028]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[2027]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[2026]---> Adder-cost: 20   maxlim: 10   bits: 4/4
c ---[2025]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[2024]---> Adder-cost: 8   maxlim: 5   bits: 3/3
c ---[2023]---> Adder-cost: 30   maxlim: 14   bits: 5/4
c ---[2022]---> Adder-cost: 36   maxlim: 18   bits: 5/5
c ---[2021]---> Adder-cost: 36   maxlim: 18   bits: 5/5
c ---[2020]---> Adder-cost: 36   maxlim: 18   bits: 5/5
c ---[2019]---> Adder-cost: 36   maxlim: 18   bits: 5/5
c ---[2017]---> Adder-cost: 36   maxlim: 18   bits: 5/5
c ---[2016]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[2015]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[2014]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[2013]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[2012]---> Adder-cost: 36   maxlim: 18   bits: 5/5
c ---[2011]---> Adder-cost: 22   maxlim: 12   bits: 4/4
c ---[2010]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[2009]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[2008]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[2006]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[2005]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[2004]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[2003]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[2002]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[2001]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[2000]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[1999]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[1998]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[1997]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[1994]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[1993]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[1991]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[1990]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1989]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[1988]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[1985]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[1984]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[1983]---> Adder-cost: 22   maxlim: 12   bits: 4/4
c ---[1982]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[1981]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[1979]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1977]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[1976]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[1975]---> Adder-cost: 20   maxlim: 11   bits: 4/4
c ---[1974]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[1973]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[1972]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[1971]---> Adder-cost: 20   maxlim: 11   bits: 4/4
c ---[1970]---> Adder-cost: 36   maxlim: 18   bits: 5/5
c ---[1969]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[1968]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[1966]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[1965]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[1964]---> Adder-cost: 36   maxlim: 18   bits: 5/5
c ---[1963]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[1962]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[1961]---> Adder-cost: 20   maxlim: 11   bits: 4/4
c ---[1960]---> Adder-cost: 20   maxlim: 11   bits: 4/4
c ---[1959]---> Adder-cost: 20   maxlim: 11   bits: 4/4
c ---[1958]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[1957]---> Adder-cost: 20   maxlim: 11   bits: 4/4
c ---[1955]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[1953]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[1952]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[1951]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[1949]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[1947]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[1946]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[1944]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[1943]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[1942]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[1941]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[1940]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[1939]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[1938]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[1937]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[1936]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[1935]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[1933]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[1932]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[1931]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[1930]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[1929]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[1928]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[1927]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[1926]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[1925]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[1924]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[1921]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[1920]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[1919]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[1918]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[1917]---> Adder-cost: 30   maxlim: 15   bits: 5/4
c ---[1916]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[1915]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[1914]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[1913]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[1912]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[1910]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[1909]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[1908]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[1907]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[1906]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[1905]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[1904]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[1903]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[1902]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[1901]---> Adder-cost: 36   maxlim: 18   bits: 5/5
c ---[1899]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[1898]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[1897]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[1896]---> Adder-cost: 36   maxlim: 18   bits: 5/5
c ---[1895]---> Adder-cost: 36   maxlim: 18   bits: 5/5
c ---[1894]---> Adder-cost: 36   maxlim: 18   bits: 5/5
c ---[1893]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[1892]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[1891]---> Adder-cost: 32   maxlim: 16   bits: 5/5
c ---[1890]---> Adder-cost: 36   maxlim: 18   bits: 5/5
c ---[1888]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[1887]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[1886]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[1885]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1884]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1883]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[1882]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[1881]---> Adder-cost: 922   maxlim: 5   bits: 4/3
c ---[1880]---> Adder-cost: 8   maxlim: 5   bits: 3/3
c ---[1879]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[1878]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[1877]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[1876]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[1875]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[1874]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[1873]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1872]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1870]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[1869]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[1868]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[1867]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[1866]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[1865]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1864]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[1863]---> Adder-cost: 14   maxlim: 6   bits: 4/3
c ---[1862]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[1861]---> Adder-cost: 30   maxlim: 15   bits: 5/4
c ---[1859]---> Adder-cost: 36   maxlim: 18   bits: 5/5
c ---[1858]---> Adder-cost: 14   maxlim: 6   bits: 4/3
c ---[1857]---> Adder-cost: 36   maxlim: 18   bits: 5/5
c ---[1856]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[1855]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[1854]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[1853]---> Adder-cost: 30   maxlim: 15   bits: 5/4
c ---[1852]---> Adder-cost: 36   maxlim: 18   bits: 5/5
c ---[1851]---> Adder-cost: 14   maxlim: 7   bits: 4/3
c ---[1850]---> Adder-cost: 36   maxlim: 18   bits: 5/5
c ---[1848]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[1847]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[1846]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[1845]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[1844]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[1843]---> Adder-cost: 30   maxlim: 14   bits: 5/4
c ---[1842]---> Adder-cost: 36   maxlim: 18   bits: 5/5
c ---[1841]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[1840]---> Adder-cost: 14   maxlim: 7   bits: 4/3
c ---[1839]---> Adder-cost: 36   maxlim: 18   bits: 5/5
c ---[1837]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[1836]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[1835]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[1834]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[1833]---> Adder-cost: 30   maxlim: 15   bits: 5/4
c ---[1832]---> Adder-cost: 36   maxlim: 18   bits: 5/5
c ---[1831]---> Adder-cost: 16   maxlim: 8   bits: 4/4
c ---[1830]---> Adder-cost: 36   maxlim: 18   bits: 5/5
c ---[1829]---> Adder-cost: 14   maxlim: 7   bits: 4/3
c ---[1828]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[1826]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[1825]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[1824]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[1823]---> Adder-cost: 36   maxlim: 18   bits: 5/5
c ---[1822]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[1821]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1820]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[1819]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[1818]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[1817]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[1814]---> Adder-cost: 8   maxlim: 5   bits: 3/3
c ---[1813]---> Adder-cost: 30   maxlim: 14   bits: 5/4
c ---[1812]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[1811]---> Adder-cost: 20   maxlim: 11   bits: 4/4
c ---[1810]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[1809]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[1808]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[1806]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1805]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[1802]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[1801]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[1800]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1799]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1798]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[1797]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1796]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[1795]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[1791]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[1790]---> Adder-cost: 8   maxlim: 5   bits: 3/3
c ---[1789]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1788]---> Adder-cost: 14   maxlim: 6   bits: 4/3
c ---[1786]---> Adder-cost: 14   maxlim: 6   bits: 4/3
c ---[1785]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[1784]---> Adder-cost: 36   maxlim: 18   bits: 5/5
c ---[1783]---> Adder-cost: 36   maxlim: 18   bits: 5/5
c ---[1781]---> Adder-cost: 30   maxlim: 15   bits: 5/4
c ---[1780]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[1779]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[1778]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[1777]---> Adder-cost: 8   maxlim: 5   bits: 3/3
c ---[1776]---> Adder-cost: 8   maxlim: 5   bits: 3/3
c ---[1775]---> Adder-cost: 30   maxlim: 14   bits: 5/4
c ---[1774]---> Adder-cost: 20   maxlim: 10   bits: 4/4
c ---[1773]---> Adder-cost: 36   maxlim: 18   bits: 5/5
c ---[1772]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[1770]---> Adder-cost: 36   maxlim: 18   bits: 5/5
c ---[1769]---> Adder-cost: 30   maxlim: 14   bits: 5/4
c ---[1768]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[1767]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[1766]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[1765]---> Adder-cost: 8   maxlim: 5   bits: 3/3
c ---[1764]---> Adder-cost: 8   maxlim: 5   bits: 3/3
c ---[1763]---> Adder-cost: 30   maxlim: 15   bits: 5/4
c ---[1762]---> Adder-cost: 20   maxlim: 10   bits: 4/4
c ---[1761]---> Adder-cost: 8   maxlim: 5   bits: 3/3
c ---[1759]---> Adder-cost: 30   maxlim: 14   bits: 5/4
c ---[1758]---> Adder-cost: 30   maxlim: 14   bits: 5/4
c ---[1757]---> Adder-cost: 8   maxlim: 5   bits: 3/3
c ---[1756]---> Adder-cost: 30   maxlim: 15   bits: 5/4
c ---[1755]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[1754]---> Adder-cost: 36   maxlim: 18   bits: 5/5
c ---[1753]---> Adder-cost: 32   maxlim: 17   bits: 5/5
c ---[1752]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[1751]---> Adder-cost: 30   maxlim: 15   bits: 5/4
c ---[1750]---> Adder-cost: 14   maxlim: 7   bits: 4/3
c ---[1748]---> Adder-cost: 30   maxlim: 15   bits: 5/4
c ---[1747]---> Adder-cost: 30   maxlim: 15   bits: 5/4
c ---[1746]---> Adder-cost: 30   maxlim: 15   bits: 5/4
c ---[1745]---> Adder-cost: 14   maxlim: 7   bits: 4/3
c ---[1744]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[1743]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[1742]---> Adder-cost: 30   maxlim: 14   bits: 5/4
c ---[1741]---> Adder-cost: 14   maxlim: 7   bits: 4/3
c ---[1740]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[1739]---> Adder-cost: 30   maxlim: 14   bits: 5/4
c ---[1737]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[1736]---> Adder-cost: 36   maxlim: 18   bits: 5/5
c ---[1735]---> Adder-cost: 36   maxlim: 18   bits: 5/5
c ---[1734]---> Adder-cost: 32   maxlim: 17   bits: 5/5
c ---[1733]---> Adder-cost: 30   maxlim: 14   bits: 5/4
c ---[1732]---> Adder-cost: 36   maxlim: 18   bits: 5/5
c ---[1731]---> Adder-cost: 30   maxlim: 14   bits: 5/4
c ---[1730]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[1729]---> Adder-cost: 36   maxlim: 18   bits: 5/5
c ---[1728]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[1726]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[1725]---> Adder-cost: 30   maxlim: 14   bits: 5/4
c ---[1724]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[1723]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[1722]---> Adder-cost: 30   maxlim: 15   bits: 5/4
c ---[1721]---> Adder-cost: 30   maxlim: 15   bits: 5/4
c ---[1720]---> Adder-cost: 30   maxlim: 14   bits: 5/4
c ---[1719]---> Adder-cost: 14   maxlim: 7   bits: 4/3
c ---[1718]---> Adder-cost: 22   maxlim: 12   bits: 4/4
c ---[1717]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[1715]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[1714]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1713]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[1712]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[1711]---> Adder-cost: 30   maxlim: 15   bits: 5/4
c ---[1710]---> Adder-cost: 30   maxlim: 14   bits: 5/4
c ---[1709]---> Adder-cost: 30   maxlim: 15   bits: 5/4
c ---[1708]---> Adder-cost: 30   maxlim: 14   bits: 5/4
c ---[1707]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[1706]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[1703]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[1702]---> Adder-cost: 8   maxlim: 5   bits: 3/3
c ---[1701]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[1700]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[1699]---> Adder-cost: 36   maxlim: 18   bits: 5/5
c ---[1698]---> Adder-cost: 30   maxlim: 14   bits: 5/4
c ---[1697]---> Adder-cost: 30   maxlim: 15   bits: 5/4
c ---[1696]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[1695]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[1694]---> Adder-cost: 36   maxlim: 18   bits: 5/5
c ---[1692]---> Adder-cost: 20   maxlim: 10   bits: 4/4
c ---[1691]---> Adder-cost: 36   maxlim: 18   bits: 5/5
c ---[1690]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[1689]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[1688]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[1687]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[1686]---> Adder-cost: 30   maxlim: 15   bits: 5/4
c ---[1685]---> Adder-cost: 30   maxlim: 15   bits: 5/4
c ---[1684]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[1683]---> Adder-cost: 14   maxlim: 6   bits: 4/3
c ---[1681]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[1680]---> Adder-cost: 8   maxlim: 5   bits: 3/3
c ---[1679]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[1678]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[1677]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[1676]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[1675]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[1674]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[1673]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[1672]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[1670]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[1669]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[1668]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1667]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[1666]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[1664]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1663]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[1662]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[1660]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[1659]---> Adder-cost: 30   maxlim: 14   bits: 5/4
c ---[1658]---> Adder-cost: 30   maxlim: 14   bits: 5/4
c ---[1657]---> Adder-cost: 30   maxlim: 15   bits: 5/4
c ---[1656]---> Adder-cost: 30   maxlim: 15   bits: 5/4
c ---[1655]---> Adder-cost: 36   maxlim: 18   bits: 5/5
c ---[1654]---> Adder-cost: 36   maxlim: 18   bits: 5/5
c ---[1653]---> Adder-cost: 30   maxlim: 15   bits: 5/4
c ---[1652]---> Adder-cost: 22   maxlim: 12   bits: 4/4
c ---[1651]---> Adder-cost: 22   maxlim: 12   bits: 4/4
c ---[1649]---> Adder-cost: 32   maxlim: 16   bits: 5/5
c ---[1648]---> Adder-cost: 36   maxlim: 18   bits: 5/5
c ---[1647]---> Adder-cost: 30   maxlim: 15   bits: 5/4
c ---[1646]---> Adder-cost: 30   maxlim: 14   bits: 5/4
c ---[1645]---> Adder-cost: 30   maxlim: 14   bits: 5/4
c ---[1644]---> Adder-cost: 36   maxlim: 18   bits: 5/5
c ---[1643]---> Adder-cost: 30   maxlim: 15   bits: 5/4
c ---[1642]---> Adder-cost: 36   maxlim: 18   bits: 5/5
c ---[1641]---> Adder-cost: 14   maxlim: 7   bits: 4/3
c ---[1640]---> Adder-cost: 30   maxlim: 15   bits: 5/4
c ---[1638]---> Adder-cost: 36   maxlim: 18   bits: 5/5
c ---[1637]---> Adder-cost: 30   maxlim: 14   bits: 5/4
c ---[1636]---> Adder-cost: 30   maxlim: 14   bits: 5/4
c ---[1635]---> Adder-cost: 36   maxlim: 18   bits: 5/5
c ---[1634]---> Adder-cost: 30   maxlim: 14   bits: 5/4
c ---[1633]---> Adder-cost: 22   maxlim: 12   bits: 4/4
c ---[1632]---> Adder-cost: 30   maxlim: 15   bits: 5/4
c ---[1631]---> Adder-cost: 36   maxlim: 18   bits: 5/5
c ---[1629]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[1626]---> Adder-cost: 36   maxlim: 18   bits: 5/5
c ---[1625]---> Adder-cost: 22   maxlim: 12   bits: 4/4
c ---[1624]---> Adder-cost: 36   maxlim: 18   bits: 5/5
c ---[1623]---> Adder-cost: 22   maxlim: 12   bits: 4/4
c ---[1622]---> Adder-cost: 36   maxlim: 18   bits: 5/5
c ---[1621]---> Adder-cost: 8   maxlim: 5   bits: 3/3
c ---[1620]---> Adder-cost: 36   maxlim: 18   bits: 5/5
c ---[1619]---> Adder-cost: 36   maxlim: 18   bits: 5/5
c ---[1618]---> Adder-cost: 30   maxlim: 15   bits: 5/4
c ---[1616]---> Adder-cost: 30   maxlim: 14   bits: 5/4
c ---[1615]---> Adder-cost: 36   maxlim: 18   bits: 5/5
c ---[1614]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[1613]---> Adder-cost: 36   maxlim: 18   bits: 5/5
c ---[1612]---> Adder-cost: 36   maxlim: 18   bits: 5/5
c ---[1611]---> Adder-cost: 14   maxlim: 7   bits: 4/3
c ---[1610]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[1609]---> Adder-cost: 30   maxlim: 14   bits: 5/4
c ---[1608]---> Adder-cost: 30   maxlim: 15   bits: 5/4
c ---[1607]---> Adder-cost: 14   maxlim: 6   bits: 4/3
c ---[1605]---> Adder-cost: 36   maxlim: 18   bits: 5/5
c ---[1603]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[1602]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[1601]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[1600]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[1599]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[1598]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[1597]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[1596]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[1593]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1592]---> Adder-cost: 36   maxlim: 18   bits: 5/5
c ---[1591]---> Adder-cost: 36   maxlim: 18   bits: 5/5
c ---[1590]---> Adder-cost: 36   maxlim: 18   bits: 5/5
c ---[1589]---> Adder-cost: 36   maxlim: 18   bits: 5/5
c ---[1588]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1587]---> Adder-cost: 36   maxlim: 18   bits: 5/5
c ---[1586]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[1585]---> Adder-cost: 28   maxlim: 16   bits: 5/5
c ---[1584]---> Adder-cost: 36   maxlim: 18   bits: 5/5
c ---[1582]---> Adder-cost: 36   maxlim: 18   bits: 5/5
c ---[1581]---> Adder-cost: 22   maxlim: 12   bits: 4/4
c ---[1580]---> Adder-cost: 36   maxlim: 18   bits: 5/5
c ---[1579]---> Adder-cost: 36   maxlim: 18   bits: 5/5
c ---[1578]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[1577]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[1576]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1572]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[1570]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[1569]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[1568]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[1567]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[1566]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[1565]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[1564]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[1562]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[1561]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[1560]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[1559]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[1558]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[1557]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[1556]---> Adder-cost: 8   maxlim: 5   bits: 3/3
c ---[1555]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[1554]---> Adder-cost: 8   maxlim: 5   bits: 3/3
c ---[1553]---> Adder-cost: 30   maxlim: 15   bits: 5/4
c ---[1551]---> Adder-cost: 30   maxlim: 15   bits: 5/4
c ---[1550]---> Adder-cost: 30   maxlim: 15   bits: 5/4
c ---[1549]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[1548]---> Adder-cost: 8   maxlim: 5   bits: 3/3
c ---[1547]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[1546]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[1545]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[1544]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[1543]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1542]---> Adder-cost: 20   maxlim: 11   bits: 4/4
c ---[1540]---> Adder-cost: 36   maxlim: 18   bits: 5/5
c ---[1539]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[1538]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[1537]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[1536]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[1535]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[1534]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[1533]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[1532]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[1531]---> Adder-cost: 22   maxlim: 12   bits: 4/4
c ---[1529]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[1528]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[1527]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[1526]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[1525]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[1524]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[1523]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[1522]---> Adder-cost: 36   maxlim: 18   bits: 5/5
c ---[1521]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[1520]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[1518]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[1517]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[1516]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[1515]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[1514]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[1513]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[1512]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[1511]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[1510]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[1509]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[1507]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1506]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1505]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1504]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[1503]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[1502]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[1501]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[1500]---> Adder-cost: 32   maxlim: 17   bits: 5/5
c ---[1499]---> Adder-cost: 14   maxlim: 7   bits: 4/3
c ---[1498]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[1496]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[1495]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[1494]---> Adder-cost: 30   maxlim: 18   bits: 5/5
c ---[1493]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[1492]---> Adder-cost: 36   maxlim: 18   bits: 5/5
c ---[1491]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[1490]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[1489]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[1484]---> Adder-cost: 8   maxlim: 5   bits: 3/3
c ---[1483]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1482]---> Adder-cost: 14   maxlim: 6   bits: 4/3
c ---[1481]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[1480]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[1479]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[1478]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[1477]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[1476]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[1475]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[1473]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[1472]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1471]---> Adder-cost: 36   maxlim: 18   bits: 5/5
c ---[1470]---> Adder-cost: 30   maxlim: 14   bits: 5/4
c ---[1469]---> Adder-cost: 32   maxlim: 16   bits: 5/5
c ---[1468]---> Adder-cost: 30   maxlim: 14   bits: 5/4
c ---[1467]---> Adder-cost: 36   maxlim: 18   bits: 5/5
c ---[1466]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1464]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1462]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1461]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1460]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1459]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[1458]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[1457]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[1456]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[1455]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[1453]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[1452]---> Adder-cost: 14   maxlim: 6   bits: 4/3
c ---[1451]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[1450]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[1449]---> Adder-cost: 20   maxlim: 11   bits: 4/4
c ---[1448]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[1447]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[1446]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[1445]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[1444]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[1442]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[1441]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[1440]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[1439]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[1438]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[1437]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[1436]---> Adder-cost: 22   maxlim: 12   bits: 4/4
c ---[1435]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[1434]---> Adder-cost: 20   maxlim: 11   bits: 4/4
c ---[1433]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1431]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[1430]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[1429]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[1428]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[1427]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[1426]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[1425]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1424]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1423]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1422]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1420]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[1419]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[1417]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1416]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[1415]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[1413]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[1409]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[1408]---> Adder-cost: 36   maxlim: 18   bits: 5/5
c ---[1407]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[1406]---> Adder-cost: 20   maxlim: 11   bits: 4/4
c ---[1405]---> Adder-cost: 30   maxlim: 14   bits: 5/4
c ---[1404]---> Adder-cost: 30   maxlim: 15   bits: 5/4
c ---[1403]---> Adder-cost: 30   maxlim: 15   bits: 5/4
c ---[1401]---> Adder-cost: 36   maxlim: 18   bits: 5/5
c ---[1400]---> Adder-cost: 8   maxlim: 5   bits: 3/3
c ---[1399]---> Adder-cost: 8   maxlim: 5   bits: 3/3
c ---[1398]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[1396]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[1395]---> Adder-cost: 8   maxlim: 5   bits: 3/3
c ---[1394]---> Adder-cost: 20   maxlim: 10   bits: 4/4
c ---[1393]---> Adder-cost: 36   maxlim: 18   bits: 5/5
c ---[1392]---> Adder-cost: 30   maxlim: 15   bits: 5/4
c ---[1390]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[1389]---> Adder-cost: 30   maxlim: 15   bits: 5/4
c ---[1388]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[1387]---> Adder-cost: 30   maxlim: 14   bits: 5/4
c ---[1386]---> Adder-cost: 36   maxlim: 18   bits: 5/5
c ---[1385]---> Adder-cost: 30   maxlim: 14   bits: 5/4
c ---[1384]---> Adder-cost: 30   maxlim: 15   bits: 5/4
c ---[1383]---> Adder-cost: 20   maxlim: 10   bits: 4/4
c ---[1382]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[1378]---> Adder-cost: 30   maxlim: 15   bits: 5/4
c ---[1377]---> Adder-cost: 36   maxlim: 18   bits: 5/5
c ---[1376]---> Adder-cost: 30   maxlim: 14   bits: 5/4
c ---[1375]---> Adder-cost: 30   maxlim: 15   bits: 5/4
c ---[1374]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[1373]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[1372]---> Adder-cost: 36   maxlim: 18   bits: 5/5
c ---[1371]---> Adder-cost: 36   maxlim: 18   bits: 5/5
c ---[1370]---> Adder-cost: 30   maxlim: 14   bits: 5/4
c ---[1369]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[1367]---> Adder-cost: 36   maxlim: 18   bits: 5/5
c ---[1366]---> Adder-cost: 20   maxlim: 11   bits: 4/4
c ---[1365]---> Adder-cost: 32   maxlim: 17   bits: 5/5
c ---[1364]---> Adder-cost: 36   maxlim: 18   bits: 5/5
c ---[1363]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[1362]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[1361]---> Adder-cost: 20   maxlim: 11   bits: 4/4
c ---[1360]---> Adder-cost: 14   maxlim: 7   bits: 4/3
c ---[1359]---> Adder-cost: 14   maxlim: 7   bits: 4/3
c ---[1358]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[1357]---> Adder-cost: 3270   maxlim: 5   bits: 4/3
c ---[1356]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1355]---> Adder-cost: 20   maxlim: 10   bits: 4/4
c ---[1354]---> Adder-cost: 20   maxlim: 11   bits: 4/4
c ---[1353]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[1352]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[1351]---> Adder-cost: 20   maxlim: 11   bits: 4/4
c ---[1350]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[1349]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[1348]---> Adder-cost: 36   maxlim: 18   bits: 5/5
c ---[1347]---> Adder-cost: 30   maxlim: 14   bits: 5/4
c ---[1346]---> Adder-cost: 4750   maxlim: 20   bits: 6/5
c ---[1345]---> Adder-cost: 34   maxlim: 18   bits: 5/5
c ---[1344]---> Adder-cost: 14   maxlim: 7   bits: 4/3
c ---[1343]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[1342]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[1341]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[1340]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[1339]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[1338]---> Adder-cost: 30   maxlim: 15   bits: 5/4
c ---[1337]---> Adder-cost: 22   maxlim: 12   bits: 4/4
c ---[1336]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[1334]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[1333]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[1332]---> Adder-cost: 36   maxlim: 18   bits: 5/5
c ---[1331]---> Adder-cost: 14   maxlim: 7   bits: 4/3
c ---[1330]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1329]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[1328]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[1327]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[1325]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[1324]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[1323]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[1322]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[1321]---> Adder-cost: 8   maxlim: 5   bits: 3/3
c ---[1319]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1317]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1316]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1305]---> Adder-cost: 3080   maxlim: 5   bits: 4/3
c ---[1225]---> Adder-cost: 2070   maxlim: 5   bits: 4/3
c ---[1160]---> Adder-cost: 4255   maxlim: 12   bits: 5/4
c ---[1135]---> Adder-cost: 946   maxlim: 12   bits: 5/4
c ---[1115]---> Adder-cost: 12   maxlim: 1   bits: 2/1
c ---[1054]---> Adder-cost: 1028   maxlim: 5   bits: 4/3
c ---[ 898]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[ 897]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[ 896]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[ 895]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[ 894]---> Adder-cost: 14   maxlim: 7   bits: 4/3
c ---[ 893]---> Adder-cost: 30   maxlim: 14   bits: 5/4
c ---[ 892]---> Adder-cost: 28   maxlim: 15   bits: 5/4
c ---[ 891]---> Adder-cost: 28   maxlim: 18   bits: 5/5
c ---[ 890]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[ 889]---> Adder-cost: 32   maxlim: 18   bits: 5/5
c ---[ 887]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[ 886]---> Adder-cost: 20   maxlim: 14   bits: 5/4
c ---[ 885]---> Adder-cost: 16   maxlim: 8   bits: 4/4
c ---[ 884]---> Adder-cost: 30   maxlim: 14   bits: 5/4
c ---[ 883]---> Adder-cost: 32   maxlim: 18   bits: 5/5
c ---[ 882]---> Adder-cost: 36   maxlim: 18   bits: 5/5
c ---[ 881]---> Adder-cost: 34   maxlim: 18   bits: 5/5
c ---[ 880]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[ 879]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[ 878]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[ 876]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[ 875]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[ 874]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[ 873]---> Adder-cost: 36   maxlim: 18   bits: 5/5
c ---[ 872]---> Adder-cost: 14   maxlim: 7   bits: 4/3
c ---[ 871]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[ 870]---> Adder-cost: 14   maxlim: 7   bits: 4/3
c ---[ 869]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[ 868]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[ 867]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[ 865]---> Adder-cost: 20   maxlim: 11   bits: 4/4
c ---[ 864]---> Adder-cost: 20   maxlim: 11   bits: 4/4
c ---[ 863]---> Adder-cost: 20   maxlim: 11   bits: 4/4
c ---[ 862]---> Adder-cost: 20   maxlim: 11   bits: 4/4
c ---[ 861]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[ 860]---> Adder-cost: 30   maxlim: 15   bits: 5/4
c ---[ 859]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[ 858]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[ 857]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 856]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[ 854]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[ 853]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[ 852]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[ 851]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[ 850]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[ 849]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 848]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[ 847]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[ 846]---> Adder-cost: 20   maxlim: 11   bits: 4/4
c ---[ 845]---> Adder-cost: 20   maxlim: 11   bits: 4/4
c ---[ 842]---> Adder-cost: 20   maxlim: 11   bits: 4/4
c ---[ 841]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 840]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[ 839]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[ 838]---> Adder-cost: 20   maxlim: 11   bits: 4/4
c ---[ 837]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[ 836]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[ 835]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[ 834]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[ 833]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[ 831]---> Adder-cost: 20   maxlim: 11   bits: 4/4
c ---[ 830]---> Adder-cost: 20   maxlim: 11   bits: 4/4
c ---[ 829]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[ 828]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[ 827]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[ 826]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[ 825]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[ 824]---> Adder-cost: 20   maxlim: 11   bits: 4/4
c ---[ 823]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[ 822]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[ 820]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[ 819]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[ 818]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[ 817]---> Adder-cost: 20   maxlim: 11   bits: 4/4
c ---[ 816]---> Adder-cost: 20   maxlim: 11   bits: 4/4
c ---[ 815]---> Adder-cost: 20   maxlim: 11   bits: 4/4
c ---[ 814]---> Adder-cost: 20   maxlim: 11   bits: 4/4
c ---[ 813]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[ 812]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[ 811]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[ 809]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[ 808]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[ 807]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[ 806]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[ 805]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[ 804]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[ 803]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[ 802]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[ 801]---> Adder-cost: 22   maxlim: 12   bits: 4/4
c ---[ 800]---> Adder-cost: 22   maxlim: 12   bits: 4/4
c ---[ 799]---> Adder-cost: 3968   maxlim: 5   bits: 4/3
c ---[ 798]---> Adder-cost: 20   maxlim: 11   bits: 4/4
c ---[ 797]---> Adder-cost: 20   maxlim: 11   bits: 4/4
c ---[ 796]---> Adder-cost: 20   maxlim: 11   bits: 4/4
c ---[ 795]---> Adder-cost: 22   maxlim: 12   bits: 4/4
c ---[ 794]---> Adder-cost: 20   maxlim: 11   bits: 4/4
c ---[ 793]---> Adder-cost: 22   maxlim: 12   bits: 4/4
c ---[ 792]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[ 791]---> Adder-cost: 30   maxlim: 15   bits: 5/4
c ---[ 790]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[ 789]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 787]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 786]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[ 785]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[ 784]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[ 783]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[ 782]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[ 781]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 780]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[ 779]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 778]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 777]---> Adder-cost: 2652   maxlim: 5   bits: 4/3
c ---[ 776]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 775]---> Adder-cost: 22   maxlim: 12   bits: 4/4
c ---[ 774]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[ 773]---> Adder-cost: 28   maxlim: 18   bits: 5/5
c ---[ 772]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[ 771]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[ 770]---> Adder-cost: 30   maxlim: 14   bits: 5/4
c ---[ 769]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[ 768]---> Adder-cost: 22   maxlim: 12   bits: 4/4
c ---[ 767]---> Adder-cost: 30   maxlim: 18   bits: 5/5
c ---[ 766]---> Adder-cost: 4736   maxlim: 26   bits: 6/5
c ---[ 765]---> Adder-cost: 32   maxlim: 18   bits: 5/5
c ---[ 764]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[ 763]---> Adder-cost: 30   maxlim: 18   bits: 5/5
c ---[ 762]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[ 761]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[ 760]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[ 759]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[ 758]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[ 757]---> Adder-cost: 30   maxlim: 15   bits: 5/4
c ---[ 756]---> Adder-cost: 16   maxlim: 15   bits: 5/4
c ---[ 754]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[ 753]---> Adder-cost: 22   maxlim: 12   bits: 4/4
c ---[ 752]---> Adder-cost: 34   maxlim: 18   bits: 5/5
c ---[ 751]---> Adder-cost: 32   maxlim: 18   bits: 5/5
c ---[ 750]---> Adder-cost: 30   maxlim: 18   bits: 5/5
c ---[ 749]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[ 748]---> Adder-cost: 22   maxlim: 12   bits: 4/4
c ---[ 747]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[ 746]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 745]---> Adder-cost: 22   maxlim: 12   bits: 4/4
c ---[ 743]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[ 742]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[ 741]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[ 740]---> Adder-cost: 32   maxlim: 18   bits: 5/5
c ---[ 739]---> Adder-cost: 32   maxlim: 18   bits: 5/5
c ---[ 738]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[ 737]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[ 736]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[ 735]---> Adder-cost: 30   maxlim: 18   bits: 5/5
c ---[ 734]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[ 731]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[ 730]---> Adder-cost: 34   maxlim: 18   bits: 5/5
c ---[ 729]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[ 728]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[ 727]---> Adder-cost: 30   maxlim: 18   bits: 5/5
c ---[ 725]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[ 724]---> Adder-cost: 30   maxlim: 15   bits: 5/4
c ---[ 723]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[ 720]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[ 719]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[ 718]---> Adder-cost: 28   maxlim: 18   bits: 5/5
c ---[ 717]---> Adder-cost: 30   maxlim: 18   bits: 5/5
c ---[ 716]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[ 715]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[ 714]---> Adder-cost: 20   maxlim: 11   bits: 4/4
c ---[ 712]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 711]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[ 709]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[ 708]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[ 707]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[ 706]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[ 705]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[ 704]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[ 703]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[ 702]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[ 701]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[ 700]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[ 698]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[ 697]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[ 696]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[ 695]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 694]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[ 693]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[ 692]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 691]---> Adder-cost: 34   maxlim: 18   bits: 5/5
c ---[ 690]---> Adder-cost: 28   maxlim: 18   bits: 5/5
c ---[ 689]---> Adder-cost: 30   maxlim: 18   bits: 5/5
c ---[ 687]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[ 686]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[ 685]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[ 684]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[ 683]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[ 682]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[ 681]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[ 680]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[ 679]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[ 678]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[ 675]---> Adder-cost: 30   maxlim: 14   bits: 5/4
c ---[ 674]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[ 673]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[ 672]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[ 671]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[ 670]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[ 669]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 668]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 667]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[ 664]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[ 663]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 662]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[ 661]---> Adder-cost: 30   maxlim: 18   bits: 5/5
c ---[ 660]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[ 659]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[ 658]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[ 657]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[ 656]---> Adder-cost: 14   maxlim: 7   bits: 4/3
c ---[ 654]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[ 653]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[ 652]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[ 651]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[ 650]---> Adder-cost: 22   maxlim: 12   bits: 4/4
c ---[ 649]---> Adder-cost: 30   maxlim: 18   bits: 5/5
c ---[ 648]---> Adder-cost: 30   maxlim: 15   bits: 5/4
c ---[ 647]---> Adder-cost: 32   maxlim: 18   bits: 5/5
c ---[ 646]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[ 645]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[ 643]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[ 642]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 640]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[ 638]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 636]---> Adder-cost: 26   maxlim: 15   bits: 5/4
c ---[ 635]---> Adder-cost: 20   maxlim: 11   bits: 4/4
c ---[ 634]---> Adder-cost: 22   maxlim: 12   bits: 4/4
c ---[ 632]---> Adder-cost: 28   maxlim: 18   bits: 5/5
c ---[ 631]---> Adder-cost: 28   maxlim: 15   bits: 5/4
c ---[ 630]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[ 629]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[ 628]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[ 627]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[ 626]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[ 625]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[ 624]---> Adder-cost: 32   maxlim: 18   bits: 5/5
c ---[ 623]---> Adder-cost: 30   maxlim: 18   bits: 5/5
c ---[ 620]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[ 619]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[ 618]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[ 617]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[ 616]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[ 615]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[ 614]---> Adder-cost: 36   maxlim: 18   bits: 5/5
c ---[ 613]---> Adder-cost: 22   maxlim: 12   bits: 4/4
c ---[ 612]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[ 611]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[ 609]---> Adder-cost: 14   maxlim: 6   bits: 4/3
c ---[ 608]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[ 607]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[ 606]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[ 605]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[ 604]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[ 603]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[ 602]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[ 601]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[ 600]---> Adder-cost: 3845   maxlim: 5   bits: 4/3
c ---[ 599]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[ 598]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[ 597]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 596]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[ 595]---> Adder-cost: 24   maxlim: 17   bits: 5/5
c ---[ 594]---> Adder-cost: 32   maxlim: 18   bits: 5/5
c ---[ 593]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[ 592]---> Adder-cost: 16   maxlim: 15   bits: 5/4
c ---[ 591]---> Adder-cost: 14   maxlim: 7   bits: 4/3
c ---[ 589]---> Adder-cost: 22   maxlim: 12   bits: 4/4
c ---[ 588]---> Adder-cost: 14   maxlim: 7   bits: 4/3
c ---[ 587]---> Adder-cost: 30   maxlim: 18   bits: 5/5
c ---[ 586]---> Adder-cost: 30   maxlim: 18   bits: 5/5
c ---[ 585]---> Adder-cost: 26   maxlim: 14   bits: 5/4
c ---[ 584]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 583]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[ 582]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[ 580]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[ 578]---> Adder-cost: 30   maxlim: 18   bits: 5/5
c ---[ 577]---> Adder-cost: 16   maxlim: 13   bits: 4/4
c ---[ 576]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[ 575]---> Adder-cost: 22   maxlim: 12   bits: 4/4
c ---[ 574]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[ 573]---> Adder-cost: 16   maxlim: 13   bits: 4/4
c ---[ 572]---> Adder-cost: 18   maxlim: 13   bits: 4/4
c ---[ 571]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 567]---> Adder-cost: 32   maxlim: 16   bits: 5/5
c ---[ 566]---> Adder-cost: 26   maxlim: 14   bits: 5/4
c ---[ 565]---> Adder-cost: 30   maxlim: 15   bits: 5/4
c ---[ 564]---> Adder-cost: 30   maxlim: 18   bits: 5/5
c ---[ 563]---> Adder-cost: 30   maxlim: 15   bits: 5/4
c ---[ 562]---> Adder-cost: 14   maxlim: 7   bits: 4/3
c ---[ 561]---> Adder-cost: 14   maxlim: 6   bits: 4/3
c ---[ 560]---> Adder-cost: 30   maxlim: 14   bits: 5/4
c ---[ 559]---> Adder-cost: 32   maxlim: 18   bits: 5/5
c ---[ 557]---> Adder-cost: 14   maxlim: 6   bits: 4/3
c ---[ 556]---> Adder-cost: 36   maxlim: 18   bits: 5/5
c ---[ 555]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[ 554]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[ 553]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[ 552]---> Adder-cost: 14   maxlim: 7   bits: 4/3
c ---[ 551]---> Adder-cost: 36   maxlim: 18   bits: 5/5
c ---[ 550]---> Adder-cost: 14   maxlim: 7   bits: 4/3
c ---[ 549]---> Adder-cost: 16   maxlim: 13   bits: 4/4
c ---[ 548]---> Adder-cost: 30   maxlim: 14   bits: 5/4
c ---[ 546]---> Adder-cost: 26   maxlim: 14   bits: 5/4
c ---[ 545]---> Adder-cost: 28   maxlim: 15   bits: 5/4
c ---[ 544]---> Adder-cost: 32   maxlim: 18   bits: 5/5
c ---[ 543]---> Adder-cost: 30   maxlim: 18   bits: 5/5
c ---[ 542]---> Adder-cost: 28   maxlim: 15   bits: 5/4
c ---[ 541]---> Adder-cost: 26   maxlim: 14   bits: 5/4
c ---[ 540]---> Adder-cost: 30   maxlim: 15   bits: 5/4
c ---[ 539]---> Adder-cost: 30   maxlim: 15   bits: 5/4
c ---[ 538]---> Adder-cost: 26   maxlim: 15   bits: 5/4
c ---[ 537]---> Adder-cost: 34   maxlim: 18   bits: 5/5
c ---[ 535]---> Adder-cost: 30   maxlim: 15   bits: 5/4
c ---[ 534]---> Adder-cost: 30   maxlim: 15   bits: 5/4
c ---[ 533]---> Adder-cost: 26   maxlim: 15   bits: 5/4
c ---[ 532]---> Adder-cost: 28   maxlim: 14   bits: 5/4
c ---[ 531]---> Adder-cost: 28   maxlim: 14   bits: 5/4
c ---[ 530]---> Adder-cost: 24   maxlim: 14   bits: 5/4
c ---[ 529]---> Adder-cost: 28   maxlim: 14   bits: 5/4
c ---[ 528]---> Adder-cost: 28   maxlim: 15   bits: 5/4
c ---[ 527]---> Adder-cost: 30   maxlim: 18   bits: 5/5
c ---[ 526]---> Adder-cost: 18   maxlim: 18   bits: 5/5
c ---[ 524]---> Adder-cost: 32   maxlim: 18   bits: 5/5
c ---[ 523]---> Adder-cost: 32   maxlim: 18   bits: 5/5
c ---[ 522]---> Adder-cost: 30   maxlim: 17   bits: 5/5
c ---[ 521]---> Adder-cost: 30   maxlim: 16   bits: 5/5
c ---[ 520]---> Adder-cost: 34   maxlim: 18   bits: 5/5
c ---[ 519]---> Adder-cost: 30   maxlim: 17   bits: 5/5
c ---[ 518]---> Adder-cost: 34   maxlim: 18   bits: 5/5
c ---[ 517]---> Adder-cost: 28   maxlim: 15   bits: 5/4
c ---[ 516]---> Adder-cost: 28   maxlim: 15   bits: 5/4
c ---[ 515]---> Adder-cost: 30   maxlim: 15   bits: 5/4
c ---[ 512]---> Adder-cost: 30   maxlim: 16   bits: 5/5
c ---[ 511]---> Adder-cost: 34   maxlim: 18   bits: 5/5
c ---[ 510]---> Adder-cost: 28   maxlim: 15   bits: 5/4
c ---[ 509]---> Adder-cost: 28   maxlim: 15   bits: 5/4
c ---[ 508]---> Adder-cost: 30   maxlim: 15   bits: 5/4
c ---[ 507]---> Adder-cost: 28   maxlim: 15   bits: 5/4
c ---[ 506]---> Adder-cost: 24   maxlim: 14   bits: 5/4
c ---[ 505]---> Adder-cost: 28   maxlim: 15   bits: 5/4
c ---[ 504]---> Adder-cost: 30   maxlim: 18   bits: 5/5
c ---[ 503]---> Adder-cost: 30   maxlim: 14   bits: 5/4
c ---[ 501]---> Adder-cost: 28   maxlim: 18   bits: 5/5
c ---[ 500]---> Adder-cost: 28   maxlim: 16   bits: 5/5
c ---[ 499]---> Adder-cost: 30   maxlim: 15   bits: 5/4
c ---[ 498]---> Adder-cost: 24   maxlim: 14   bits: 5/4
c ---[ 497]---> Adder-cost: 30   maxlim: 15   bits: 5/4
c ---[ 496]---> Adder-cost: 28   maxlim: 14   bits: 5/4
c ---[ 495]---> Adder-cost: 26   maxlim: 15   bits: 5/4
c ---[ 494]---> Adder-cost: 26   maxlim: 17   bits: 5/5
c ---[ 493]---> Adder-cost: 36   maxlim: 18   bits: 5/5
c ---[ 492]---> Adder-cost: 26   maxlim: 14   bits: 5/4
c ---[ 490]---> Adder-cost: 30   maxlim: 14   bits: 5/4
c ---[ 489]---> Adder-cost: 28   maxlim: 15   bits: 5/4
c ---[ 488]---> Adder-cost: 30   maxlim: 15   bits: 5/4
c ---[ 487]---> Adder-cost: 32   maxlim: 17   bits: 5/5
c ---[ 485]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[ 484]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 483]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 482]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 481]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[ 479]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[ 478]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[ 477]---> Adder-cost: 32   maxlim: 18   bits: 5/5
c ---[ 476]---> Adder-cost: 32   maxlim: 18   bits: 5/5
c ---[ 475]---> Adder-cost: 26   maxlim: 14   bits: 5/4
c ---[ 474]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[ 473]---> Adder-cost: 14   maxlim: 6   bits: 4/3
c ---[ 472]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 471]---> Adder-cost: 8   maxlim: 5   bits: 3/3
c ---[ 470]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 468]---> Adder-cost: 30   maxlim: 15   bits: 5/4
c ---[ 467]---> Adder-cost: 20   maxlim: 10   bits: 4/4
c ---[ 466]---> Adder-cost: 20   maxlim: 11   bits: 4/4
c ---[ 465]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[ 464]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[ 463]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[ 462]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[ 461]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[ 460]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[ 459]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[ 457]---> Adder-cost: 30   maxlim: 18   bits: 5/5
c ---[ 456]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[ 455]---> Adder-cost: 8   maxlim: 5   bits: 3/3
c ---[ 454]---> Adder-cost: 26   maxlim: 15   bits: 5/4
c ---[ 453]---> Adder-cost: 30   maxlim: 15   bits: 5/4
c ---[ 451]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[ 450]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 449]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[ 448]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[ 446]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[ 445]---> Adder-cost: 20   maxlim: 11   bits: 4/4
c ---[ 443]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[ 442]---> Adder-cost: 16   maxlim: 13   bits: 4/4
c ---[ 441]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[ 440]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 439]---> Adder-cost: 30   maxlim: 18   bits: 5/5
c ---[ 438]---> Adder-cost: 16   maxlim: 13   bits: 4/4
c ---[ 437]---> Adder-cost: 18   maxlim: 13   bits: 4/4
c ---[ 435]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[ 434]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[ 433]---> Adder-cost: 16   maxlim: 13   bits: 4/4
c ---[ 432]---> Adder-cost: 16   maxlim: 13   bits: 4/4
c ---[ 431]---> Adder-cost: 18   maxlim: 13   bits: 4/4
c ---[ 430]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[ 428]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 424]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 423]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 422]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[ 421]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[ 420]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[ 419]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[ 418]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 417]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[ 416]---> Adder-cost: 16   maxlim: 13   bits: 4/4
c ---[ 415]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[ 413]---> Adder-cost: 16   maxlim: 13   bits: 4/4
c ---[ 412]---> Adder-cost: 18   maxlim: 13   bits: 4/4
c ---[ 411]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[ 410]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 409]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[ 408]---> Adder-cost: 32   maxlim: 18   bits: 5/5
c ---[ 407]---> Adder-cost: 30   maxlim: 18   bits: 5/5
c ---[ 406]---> Adder-cost: 16   maxlim: 13   bits: 4/4
c ---[ 405]---> Adder-cost: 16   maxlim: 13   bits: 4/4
c ---[ 404]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[ 403]---> Adder-cost: 1150   maxlim: 2   bits: 3/2
c ---[ 402]---> Adder-cost: 486   maxlim: 2   bits: 3/2
c ---[ 401]---> Adder-cost: 197   maxlim: 2   bits: 3/2
c ---[ 400]---> Adder-cost: 51   maxlim: 1   bits: 2/1
c ---[ 399]---> Adder-cost: 18   maxlim: 1   bits: 2/1
c ---[ 398]---> Adder-cost: 272   maxlim: 2   bits: 3/2
c ---[ 397]---> Adder-cost: 74   maxlim: 2   bits: 3/2
c ---[ 396]---> Adder-cost: 102   maxlim: 2   bits: 3/2
c ---[ 395]---> Adder-cost: 38   maxlim: 2   bits: 3/2
c ---[ 394]---> Adder-cost: 50   maxlim: 3   bits: 3/2
c ---[ 393]---> Adder-cost: 133   maxlim: 1   bits: 2/1
c ---[ 392]---> Adder-cost: 45   maxlim: 1   bits: 2/1
c ---[ 391]---> Adder-cost: 197   maxlim: 1   bits: 2/1
c ---[ 390]---> Adder-cost: 57   maxlim: 1   bits: 2/1
c ---[ 389]---> Adder-cost: 105   maxlim: 1   bits: 2/1
c ---[ 388]---> Adder-cost: 147   maxlim: 2   bits: 3/2
c ---[ 387]---> Adder-cost: 195   maxlim: 1   bits: 2/1
c ---[ 386]---> Adder-cost: 946   maxlim: 3   bits: 3/2
c ---[ 385]---> Adder-cost: 1302   maxlim: 3   bits: 3/2
c ---[ 384]---> Adder-cost: 957   maxlim: 14   bits: 5/4
c ---[ 383]---> Adder-cost: 48   maxlim: 1   bits: 2/1
c ---[ 382]---> Adder-cost: 54   maxlim: 1   bits: 2/1
c ---[ 381]---> Adder-cost: 28   maxlim: 1   bits: 2/1
c ---[ 380]---> Adder-cost: 18   maxlim: 1   bits: 2/1
c ---[ 379]---> Adder-cost: 27   maxlim: 1   bits: 2/1
c ---[ 378]---> Adder-cost: 40   maxlim: 2   bits: 3/2
c ---[ 377]---> Adder-cost: 816   maxlim: 3   bits: 3/2
c ---[ 376]---> Adder-cost: 824   maxlim: 2   bits: 3/2
c ---[ 375]---> Adder-cost: 472   maxlim: 2   bits: 3/2
c ---[ 374]---> Adder-cost: 47   maxlim: 2   bits: 3/2
c ---[ 373]---> Adder-cost: 97   maxlim: 4   bits: 4/3
c ---[ 372]---> Adder-cost: 241   maxlim: 2   bits: 3/2
c ---[ 371]---> Adder-cost: 190   maxlim: 1   bits: 2/1
c ---[ 370]---> Adder-cost: 316   maxlim: 4   bits: 4/3
c ---[ 369]---> Adder-cost: 104   maxlim: 3   bits: 3/2
c ---[ 368]---> Adder-cost: 110   maxlim: 11   bits: 5/4
c ---[ 367]---> Adder-cost: 2027   maxlim: 3   bits: 3/2
c ---[ 366]---> Adder-cost: 173   maxlim: 1   bits: 2/1
c ---[ 365]---> Adder-cost: 57   maxlim: 1   bits: 2/1
c ---[ 364]---> Adder-cost: 18   maxlim: 1   bits: 2/1
c ---[ 363]---> Adder-cost: 10   maxlim: 1   bits: 2/1
c ---[ 362]---> Adder-cost: 54   maxlim: 1   bits: 2/1
c ---[ 361]---> Adder-cost: 6   maxlim: 1   bits: 2/1
c ---[ 360]---> Adder-cost: 58   maxlim: 1   bits: 2/1
c ---[ 359]---> Adder-cost: 26   maxlim: 1   bits: 2/1
c ---[ 358]---> Adder-cost: 1730   maxlim: 3   bits: 3/2
c ---[ 357]---> Adder-cost: 43   maxlim: 1   bits: 2/1
c ---[ 356]---> Adder-cost: 55   maxlim: 2   bits: 3/2
c ---[ 355]---> Adder-cost: 79   maxlim: 1   bits: 2/1
c ---[ 354]---> Adder-cost: 21   maxlim: 1   bits: 2/1
c ---[ 353]---> Adder-cost: 178   maxlim: 1   bits: 2/1
c ---[ 352]---> Adder-cost: 54   maxlim: 1   bits: 2/1
c ---[ 351]---> Adder-cost: 60   maxlim: 1   bits: 2/1
c ---[ 350]---> Adder-cost: 350   maxlim: 2   bits: 3/2
c ---[ 349]---> Adder-cost: 687   maxlim: 2   bits: 3/2
c ---[ 348]---> Adder-cost: 169   maxlim: 3   bits: 3/2
c ---[ 347]---> Adder-cost: 65   maxlim: 1   bits: 2/1
c ---[ 346]---> Adder-cost: 21   maxlim: 1   bits: 2/1
c ---[ 345]---> Adder-cost: 526   maxlim: 2   bits: 3/2
c ---[ 344]---> Adder-cost: 10   maxlim: 1   bits: 2/1
c ---[ 343]---> Adder-cost: 6   maxlim: 1   bits: 2/1
c ---[ 342]---> Adder-cost: 77   maxlim: 1   bits: 2/1
c ---[ 341]---> Adder-cost: 21   maxlim: 1   bits: 2/1
c ---[ 340]---> Adder-cost: 287   maxlim: 2   bits: 3/2
c ---[ 339]---> Adder-cost: 751   maxlim: 3   bits: 3/2
c ---[ 338]---> Adder-cost: 296   maxlim: 2   bits: 3/2
c ---[ 337]---> Adder-cost: 1051   maxlim: 2   bits: 3/2
c ---[ 336]---> Adder-cost: 1367   maxlim: 3   bits: 3/2
c ---[ 335]---> Adder-cost: 1534   maxlim: 4   bits: 4/3
c ---[ 334]---> Adder-cost: 1609   maxlim: 7   bits: 4/3
c ---[ 333]---> Adder-cost: 30   maxlim: 1   bits: 2/1
c ---[ 332]---> Adder-cost: 1196   maxlim: 3   bits: 3/2
c ---[ 331]---> Adder-cost: 1226   maxlim: 7   bits: 4/3
c ---[ 330]---> Adder-cost: 14   maxlim: 1   bits: 2/1
c ---[ 329]---> Adder-cost: 66   maxlim: 2   bits: 3/2
c ---[ 328]---> Adder-cost: 36   maxlim: 1   bits: 2/1
c ---[ 327]---> Adder-cost: 228   maxlim: 1   bits: 2/1
c ---[ 326]---> Adder-cost: 72   maxlim: 1   bits: 2/1
c ---[ 325]---> Adder-cost: 36   maxlim: 1   bits: 2/1
c ---[ 324]---> Adder-cost: 15   maxlim: 1   bits: 2/1
c ---[ 323]---> Adder-cost: 48   maxlim: 1   bits: 2/1
c ---[ 322]---> Adder-cost: 6   maxlim: 1   bits: 2/1
c ---[ 321]---> Adder-cost: 187   maxlim: 1   bits: 2/1
c ---[ 320]---> Adder-cost: 203   maxlim: 2   bits: 3/2
c ---[ 319]---> Adder-cost: 2504   maxlim: 6   bits: 4/3
c ---[ 318]---> Adder-cost: 332   maxlim: 1   bits: 2/1
c ---[ 317]---> Adder-cost: 582   maxlim: 4   bits: 4/3
c ---[ 316]---> Adder-cost: 410   maxlim: 3   bits: 3/2
c ---[ 315]---> Adder-cost: 940   maxlim: 3   bits: 3/2
c ---[ 314]---> Adder-cost: 412   maxlim: 2   bits: 3/2
c ---[ 313]---> Adder-cost: 582   maxlim: 4   bits: 4/3
c ---[ 312]---> Adder-cost: 1684   maxlim: 8   bits: 5/4
c ---[ 311]---> Adder-cost: 1709   maxlim: 3   bits: 3/2
c ---[ 310]---> Adder-cost: 1691   maxlim: 8   bits: 5/4
c ---[ 309]---> Adder-cost: 1237   maxlim: 6   bits: 4/3
c ---[ 308]---> Adder-cost: 1774   maxlim: 4   bits: 4/3
c ---[ 307]---> Adder-cost: 395   maxlim: 5   bits: 4/3
c ---[ 306]---> Adder-cost: 282   maxlim: 1   bits: 2/1
c ---[ 305]---> Adder-cost: 121   maxlim: 1   bits: 2/1
c ---[ 304]---> Adder-cost: 818   maxlim: 3   bits: 3/2
c ---[ 303]---> Adder-cost: 467   maxlim: 2   bits: 3/2
c ---[ 302]---> Adder-cost: 686   maxlim: 3   bits: 3/2
c ---[ 301]---> Adder-cost: 131   maxlim: 1   bits: 2/1
c ---[ 300]---> Adder-cost: 140   maxlim: 2   bits: 3/2
c ---[ 299]---> Adder-cost: 1510   maxlim: 4   bits: 4/3
c ---[ 298]---> Adder-cost: 1239   maxlim: 3   bits: 3/2
c ---[ 297]---> Adder-cost: 1602   maxlim: 8   bits: 5/4
c ---[ 296]---> Adder-cost: 159   maxlim: 2   bits: 3/2
c ---[ 295]---> Adder-cost: 223   maxlim: 3   bits: 3/2
c ---[ 294]---> Adder-cost: 2161   maxlim: 6   bits: 4/3
c ---[ 293]---> Adder-cost: 307   maxlim: 1   bits: 2/1
c ---[ 292]---> Adder-cost: 1720   maxlim: 5   bits: 4/3
c ---[ 291]---> Adder-cost: 571   maxlim: 1   bits: 2/1
c ---[ 290]---> Adder-cost: 647   maxlim: 2   bits: 3/2
c ---[ 289]---> Adder-cost: 534   maxlim: 2   bits: 3/2
c ---[ 288]---> Adder-cost: 802   maxlim: 4   bits: 4/3
c ---[ 287]---> Adder-cost: 1360   maxlim: 5   bits: 4/3
c ---[ 286]---> Adder-cost: 1657   maxlim: 4   bits: 4/3
c ---[ 285]---> Adder-cost: 165   maxlim: 1   bits: 2/1
c ---[ 284]---> Adder-cost: 185   maxlim: 2   bits: 3/2
c ---[ 283]---> Adder-cost: 118   maxlim: 1   bits: 2/1
c ---[ 282]---> Adder-cost: 474   maxlim: 3   bits: 3/2
c ---[ 281]---> Adder-cost: 2302   maxlim: 3   bits: 3/2
c ---[ 280]---> Adder-cost: 2969   maxlim: 5   bits: 4/3
c ---[ 279]---> Adder-cost: 2689   maxlim: 3   bits: 3/2
c ---[ 278]---> Adder-cost: 1720   maxlim: 5   bits: 4/3
c ---[ 277]---> Adder-cost: 107   maxlim: 1   bits: 2/1
c ---[ 276]---> Adder-cost: 130   maxlim: 2   bits: 3/2
c ---[ 275]---> Adder-cost: 831   maxlim: 6   bits: 4/3
c ---[ 274]---> Adder-cost: 66   maxlim: 1   bits: 2/1
c ---[ 273]---> Adder-cost: 74   maxlim: 2   bits: 3/2
c ---[ 272]---> Adder-cost: 183   maxlim: 1   bits: 2/1
c ---[ 271]---> Adder-cost: 898   maxlim: 2   bits: 3/2
c ---[ 270]---> Adder-cost: 1174   maxlim: 4   bits: 4/3
c ---[ 269]---> Adder-cost: 353   maxlim: 1   bits: 2/1
c ---[ 268]---> Adder-cost: 402   maxlim: 2   bits: 3/2
c ---[ 267]---> Adder-cost: 692   maxlim: 2   bits: 3/2
c ---[ 266]---> Adder-cost: 902   maxlim: 4   bits: 4/3
c ---[ 265]---> Adder-cost: 346   maxlim: 3   bits: 3/2
c ---[ 264]---> Adder-cost: 310   maxlim: 1   bits: 2/1
c ---[ 263]---> Adder-cost: 374   maxlim: 2   bits: 3/2
c ---[ 262]---> Adder-cost: 252   maxlim: 1   bits: 2/1
c ---[ 261]---> Adder-cost: 55   maxlim: 1   bits: 2/1
c ---[ 260]---> Adder-cost: 290   maxlim: 2   bits: 3/2
c ---[ 259]---> Adder-cost: 1491   maxlim: 6   bits: 4/3
c ---[ 258]---> Adder-cost: 1882   maxlim: 6   bits: 4/3
c ---[ 257]---> Adder-cost: 806   maxlim: 2   bits: 3/2
c ---[ 256]---> Adder-cost: 1292   maxlim: 4   bits: 4/3
c ---[ 255]---> Adder-cost: 150   maxlim: 1   bits: 2/1
c ---[ 254]---> Adder-cost: 176   maxlim: 2   bits: 3/2
c ---[ 253]---> Adder-cost: 492   maxlim: 1   bits: 2/1
c ---[ 252]---> Adder-cost: 532   maxlim: 2   bits: 3/2
c ---[ 251]---> Adder-cost: 2047   maxlim: 3   bits: 3/2
c ---[ 250]---> Adder-cost: 333   maxlim: 1   bits: 2/1
c ---[ 249]---> Adder-cost: 2784   maxlim: 5   bits: 4/3
c ---[ 248]---> Adder-cost: 490   maxlim: 2   bits: 3/2
c ---[ 247]---> Adder-cost: 664   maxlim: 3   bits: 3/2
c ---[ 246]---> Adder-cost: 282   maxlim: 4   bits: 4/3
c ---[ 245]---> Adder-cost: 693   maxlim: 3   bits: 3/2
c ---[ 244]---> Adder-cost: 111   maxlim: 1   bits: 2/1
c ---[ 243]---> Adder-cost: 167   maxlim: 2   bits: 3/2
c ---[ 242]---> Adder-cost: 3086   maxlim: 10   bits: 5/4
c ---[ 241]---> Adder-cost: 640   maxlim: 3   bits: 3/2
c ---[ 240]---> Adder-cost: 812   maxlim: 8   bits: 5/4
c ---[ 239]---> Adder-cost: 1400   maxlim: 3   bits: 3/2
c ---[ 238]---> Adder-cost: 96   maxlim: 1   bits: 2/1
c ---[ 237]---> Adder-cost: 105   maxlim: 1   bits: 2/1
c ---[ 236]---> Adder-cost: 116   maxlim: 2   bits: 3/2
c ---[ 235]---> Adder-cost: 2235   maxlim: 5   bits: 4/3
c ---[ 234]---> Adder-cost: 682   maxlim: 4   bits: 4/3
c ---[ 233]---> Adder-cost: 1014   maxlim: 3   bits: 3/2
c ---[ 232]---> Adder-cost: 203   maxlim: 2   bits: 3/2
c ---[ 231]---> Adder-cost: 828   maxlim: 4   bits: 4/3
c ---[ 230]---> Adder-cost: 64   maxlim: 1   bits: 2/1
c ---[ 229]---> Adder-cost: 75   maxlim: 2   bits: 3/2
c ---[ 228]---> Adder-cost: 572   maxlim: 2   bits: 3/2
c ---[ 227]---> Adder-cost: 237   maxlim: 2   bits: 3/2
c ---[ 226]---> Adder-cost: 1141   maxlim: 5   bits: 4/3
c ---[ 225]---> Adder-cost: 243   maxlim: 2   bits: 3/2
c ---[ 224]---> Adder-cost: 322   maxlim: 3   bits: 3/2
c ---[ 223]---> Adder-cost: 997   maxlim: 5   bits: 4/3
c ---[ 222]---> Adder-cost: 420   maxlim: 3   bits: 3/2
c ---[ 221]---> Adder-cost: 1528   maxlim: 3   bits: 3/2
c ---[ 220]---> Adder-cost: 53   maxlim: 1   bits: 2/1
c ---[ 219]---> Adder-cost: 64   maxlim: 2   bits: 3/2
c ---[ 218]---> Adder-cost: 1848   maxlim: 3   bits: 3/2
c ---[ 217]---> Adder-cost: 300   maxlim: 2   bits: 3/2
c ---[ 216]---> Adder-cost: 2613   maxlim: 6   bits: 4/3
c ---[ 215]---> Adder-cost: 61   maxlim: 1   bits: 2/1
c ---[ 214]---> Adder-cost: 305   maxlim: 2   bits: 3/2
c ---[ 213]---> Adder-cost: 454   maxlim: 4   bits: 4/3
c ---[ 212]---> Adder-cost: 250   maxlim: 3   bits: 3/2
c ---[ 211]---> Adder-cost: 374   maxlim: 8   bits: 5/4
c ---[ 210]---> Adder-cost: 277   maxlim: 1   bits: 2/1
c ---[ 209]---> Adder-cost: 343   maxlim: 2   bits: 3/2
c ---[ 208]---> Adder-cost: 416   maxlim: 1   bits: 2/1
c ---[ 207]---> Adder-cost: 473   maxlim: 2   bits: 3/2
c ---[ 206]---> Adder-cost: 242   maxlim: 3   bits: 3/2
c ---[ 205]---> Adder-cost: 292   maxlim: 2   bits: 3/2
c ---[ 204]---> Adder-cost: 338   maxlim: 3   bits: 3/2
c ---[ 203]---> Adder-cost: 1903   maxlim: 7   bits: 4/3
c ---[ 202]---> Adder-cost: 1246   maxlim: 8   bits: 5/4
c ---[ 201]---> Adder-cost: 957   maxlim: 6   bits: 4/3
c ---[ 200]---> Adder-cost: 535   maxlim: 1   bits: 2/1
c ---[ 199]---> Adder-cost: 508   maxlim: 5   bits: 4/3
c ---[ 198]---> Adder-cost: 451   maxlim: 2   bits: 3/2
c ---[ 197]---> Adder-cost: 1253   maxlim: 5   bits: 4/3
c ---[ 196]---> Adder-cost: 218   maxlim: 1   bits: 2/1
c ---[ 195]---> Adder-cost: 1280   maxlim: 4   bits: 4/3
c ---[ 194]---> Adder-cost: 1119   maxlim: 5   bits: 4/3
c ---[ 193]---> Adder-cost: 161   maxlim: 2   bits: 3/2
c ---[ 192]---> Adder-cost: 219   maxlim: 2   bits: 3/2
c ---[ 191]---> Adder-cost: 1063   maxlim: 4   bits: 4/3
c ---[ 190]---> Adder-cost: 2187   maxlim: 7   bits: 4/3
c ---[ 189]---> Adder-cost: 420   maxlim: 2   bits: 3/2
c ---[ 188]---> Adder-cost: 112   maxlim: 1   bits: 2/1
c ---[ 187]---> Adder-cost: 373   maxlim: 2   bits: 3/2
c ---[ 186]---> Adder-cost: 104   maxlim: 2   bits: 3/2
c ---[ 185]---> Adder-cost: 698   maxlim: 3   bits: 3/2
c ---[ 184]---> Adder-cost: 365   maxlim: 4   bits: 4/3
c ---[ 183]---> Adder-cost: 2374   maxlim: 10   bits: 5/4
c ---[ 182]---> Adder-cost: 970   maxlim: 8   bits: 5/4
c ---[ 181]---> Adder-cost: 1574   maxlim: 5   bits: 4/3
c ---[ 180]---> Adder-cost: 475   maxlim: 1   bits: 2/1
c ---[ 179]---> Adder-cost: 557   maxlim: 4   bits: 4/3
c ---[ 178]---> Adder-cost: 5113   maxlim: 20   bits: 6/5
c ---[ 177]---> Adder-cost: 95   maxlim: 1   bits: 2/1
c ---[ 176]---> Adder-cost: 86   maxlim: 2   bits: 3/2
c ---[ 175]---> Adder-cost: 981   maxlim: 5   bits: 4/3
c ---[ 174]---> Adder-cost: 808   maxlim: 5   bits: 4/3
c ---[ 173]---> Adder-cost: 990   maxlim: 5   bits: 4/3
c ---[ 172]---> Adder-cost: 357   maxlim: 3   bits: 3/2
c ---[ 171]---> Adder-cost: 2466   maxlim: 6   bits: 4/3
c ---[ 170]---> Adder-cost: 617   maxlim: 1   bits: 2/1
c ---[ 169]---> Adder-cost: 158   maxlim: 1   bits: 2/1
c ---[ 168]---> Adder-cost: 106   maxlim: 1   bits: 2/1
c ---[ 167]---> Adder-cost: 135   maxlim: 2   bits: 3/2
c ---[ 166]---> Adder-cost: 292   maxlim: 1   bits: 2/1
c ---[ 165]---> Adder-cost: 522   maxlim: 1   bits: 2/1
c ---[ 164]---> Adder-cost: 623   maxlim: 1   bits: 2/1
c ---[ 163]---> Adder-cost: 126   maxlim: 1   bits: 2/1
c ---[ 162]---> Adder-cost: 325   maxlim: 3   bits: 3/2
c ---[ 161]---> Adder-cost: 9   maxlim: 1   bits: 2/1
c ---[ 160]---> Adder-cost: 673   maxlim: 1   bits: 2/1
c ---[ 159]---> Adder-cost: 384   maxlim: 1   bits: 2/1
c ---[ 158]---> Adder-cost: 246   maxlim: 1   bits: 2/1
c ---[ 157]---> Adder-cost: 1056   maxlim: 1   bits: 2/1
c ---[ 156]---> Adder-cost: 417   maxlim: 1   bits: 2/1
c ---[ 155]---> Adder-cost: 265   maxlim: 1   bits: 2/1
c ---[ 154]---> Adder-cost: 533   maxlim: 1   bits: 2/1
c ---[ 153]---> Adder-cost: 44   maxlim: 1   bits: 2/1
c ---[ 152]---> Adder-cost: 20   maxlim: 1   bits: 2/1
c ---[ 151]---> Adder-cost: 4   maxlim: 1   bits: 2/1
c ---[ 150]---> Adder-cost: 2246   maxlim: 8   bits: 5/4
c ---[ 149]---> Adder-cost: 21   maxlim: 1   bits: 2/1
c ---[ 148]---> Adder-cost: 43   maxlim: 1   bits: 2/1
c ---[ 147]---> Adder-cost: 378   maxlim: 1   bits: 2/1
c ---[ 146]---> Adder-cost: 604   maxlim: 1   bits: 2/1
c ---[ 145]---> Adder-cost: 314   maxlim: 1   bits: 2/1
c ---[ 144]---> Adder-cost: 976   maxlim: 1   bits: 2/1
c ---[ 143]---> Adder-cost: 193   maxlim: 1   bits: 2/1
c ---[ 142]---> Adder-cost: 185   maxlim: 1   bits: 2/1
c ---[ 141]---> Adder-cost: 58   maxlim: 1   bits: 2/1
c ---[ 140]---> Adder-cost: 326   maxlim: 1   bits: 2/1
c ---[ 139]---> Adder-cost: 255   maxlim: 1   bits: 2/1
c ---[ 138]---> Adder-cost: 25   maxlim: 1   bits: 2/1
c ---[ 137]---> Adder-cost: 1203   maxlim: 12   bits: 5/4
c ---[ 136]---> Adder-cost: 11   maxlim: 1   bits: 2/1
c ---[ 135]---> Adder-cost: 492   maxlim: 1   bits: 2/1
c ---[ 134]---> Adder-cost: 14   maxlim: 1   bits: 2/1
c ---[ 133]---> Adder-cost: 320   maxlim: 1   bits: 2/1
c ---[ 132]---> Adder-cost: 567   maxlim: 1   bits: 2/1
c ---[ 131]---> Adder-cost: 254   maxlim: 1   bits: 2/1
c ---[ 130]---> Adder-cost: 91   maxlim: 1   bits: 2/1
c ---[ 129]---> Adder-cost: 202   maxlim: 4   bits: 4/3
c ---[ 128]---> Adder-cost: 350   maxlim: 4   bits: 4/3
c ---[ 127]---> Adder-cost: 188   maxlim: 3   bits: 3/2
c ---[ 126]---> Adder-cost: 246   maxlim: 4   bits: 4/3
c ---[ 125]---> Adder-cost: 333   maxlim: 3   bits: 3/2
c ---[ 124]---> Adder-cost: 1107   maxlim: 4   bits: 4/3
c ---[ 123]---> Adder-cost: 950   maxlim: 3   bits: 3/2
c ---[ 122]---> Adder-cost: 359   maxlim: 4   bits: 4/3
c ---[ 121]---> Adder-cost: 165   maxlim: 4   bits: 4/3
c ---[ 120]---> Adder-cost: 744   maxlim: 2   bits: 3/2
c ---[ 119]---> Adder-cost: 685   maxlim: 4   bits: 4/3
c ---[ 118]---> Adder-cost: 520   maxlim: 3   bits: 3/2
c ---[ 117]---> Adder-cost: 226   maxlim: 4   bits: 4/3
c ---[ 116]---> Adder-cost: 643   maxlim: 5   bits: 4/3
c ---[ 115]---> Adder-cost: 123   maxlim: 4   bits: 4/3
c ---[ 114]---> Adder-cost: 463   maxlim: 3   bits: 3/2
c ---[ 113]---> Adder-cost: 121   maxlim: 2   bits: 3/2
c ---[ 112]---> Adder-cost: 101   maxlim: 4   bits: 4/3
c ---[ 111]---> Adder-cost: 772   maxlim: 3   bits: 3/2
c ---[ 110]---> Adder-cost: 339   maxlim: 4   bits: 4/3
c ---[ 109]---> Adder-cost: 626   maxlim: 3   bits: 3/2
c ---[ 108]---> Adder-cost: 11   maxlim: 4   bits: 4/3
c ---[ 107]---> Adder-cost: 227   maxlim: 4   bits: 4/3
c ---[ 106]---> Adder-cost: 41   maxlim: 2   bits: 3/2
c ---[ 105]---> Adder-cost: 855   maxlim: 3   bits: 3/2
c ---[ 104]---> Adder-cost: 107   maxlim: 2   bits: 3/2
c ---[ 103]---> Adder-cost: 151   maxlim: 2   bits: 3/2
c ---[ 102]---> Adder-cost: 192   maxlim: 4   bits: 4/3
c ---[ 101]---> Adder-cost: 166   maxlim: 4   bits: 4/3
c ---[ 100]---> Adder-cost: 129   maxlim: 5   bits: 4/3
c ---[  99]---> Adder-cost: 2270   maxlim: 5   bits: 4/3
c ---[  98]---> Adder-cost: 132   maxlim: 4   bits: 4/3
c ---[  97]---> Adder-cost: 45   maxlim: 2   bits: 3/2
c ---[  96]---> Adder-cost: 350   maxlim: 2   bits: 3/2
c ---[  95]---> Adder-cost: 477   maxlim: 4   bits: 4/3
c ---[  94]---> Adder-cost: 20   maxlim: 1   bits: 2/1
c ---[  93]---> Adder-cost: 516   maxlim: 2   bits: 3/2
c ---[  92]---> Adder-cost: 8   maxlim: 2   bits: 3/2
c ---[  91]---> Adder-cost: 979   maxlim: 4   bits: 4/3
c ---[  90]---> Adder-cost: 141   maxlim: 5   bits: 4/3
c ---[  89]---> Adder-cost: 55   maxlim: 4   bits: 4/3
c ---[  88]---> Adder-cost: 1283   maxlim: 5   bits: 4/3
c ---[  87]---> Adder-cost: 2065   maxlim: 5   bits: 4/3
c ---[  86]---> Adder-cost: 329   maxlim: 3   bits: 3/2
c ---[  85]---> Adder-cost: 297   maxlim: 4   bits: 4/3
c ---[  84]---> Adder-cost: 982   maxlim: 2   bits: 3/2
c ---[  83]---> Adder-cost: 510   maxlim: 5   bits: 4/3
c ---[  82]---> Adder-cost: 895   maxlim: 2   bits: 3/2
c ---[  81]---> Adder-cost: 534   maxlim: 6   bits: 4/3
c ---[  80]---> Adder-cost: 1123   maxlim: 5   bits: 4/3
c ---[  79]---> Adder-cost: 129   maxlim: 1   bits: 2/1
c ---[  78]---> Adder-cost: 138   maxlim: 2   bits: 3/2
c ---[  77]---> Adder-cost: 1877   maxlim: 8   bits: 5/4
c ---[  76]---> Adder-cost: 166   maxlim: 2   bits: 3/2
c ---[  75]---> Adder-cost: 25   maxlim: 1   bits: 2/1
c ---[  74]---> Adder-cost: 97   maxlim: 1   bits: 2/1
c ---[  73]---> Adder-cost: 442   maxlim: 1   bits: 2/1
c ---[  72]---> Adder-cost: 158   maxlim: 1   bits: 2/1
c ---[  71]---> Adder-cost: 1501   maxlim: 3   bits: 3/2
c ---[  70]---> Adder-cost: 419   maxlim: 1   bits: 2/1
c ---[  69]---> Adder-cost: 581   maxlim: 1   bits: 2/1
c ---[  68]---> Adder-cost: 322   maxlim: 1   bits: 2/1
c ---[  67]---> Adder-cost: 219   maxlim: 1   bits: 2/1
c ---[  66]---> Adder-cost: 76   maxlim: 1   bits: 2/1
c ---[  65]---> Adder-cost: 79   maxlim: 1   bits: 2/1
c ---[  64]---> Adder-cost: 378   maxlim: 1   bits: 2/1
c ---[  63]---> Adder-cost: 124   maxlim: 1   bits: 2/1
c ---[  62]---> Adder-cost: 42   maxlim: 1   bits: 2/1
c ---[  61]---> Adder-cost: 197   maxlim: 1   bits: 2/1
c ---[  60]---> Adder-cost: 25   maxlim: 1   bits: 2/1
c ---[  59]---> Adder-cost: 446   maxlim: 1   bits: 2/1
c ---[  58]---> Adder-cost: 160   maxlim: 1   bits: 2/1
c ---[  57]---> Adder-cost: 127   maxlim: 2   bits: 3/2
c ---[  56]---> Adder-cost: 33   maxlim: 1   bits: 2/1
c ---[  55]---> Adder-cost: 260   maxlim: 2   bits: 3/2
c ---[  54]---> Adder-cost: 722   maxlim: 2   bits: 3/2
c ---[  53]---> Adder-cost: 1121   maxlim: 4   bits: 4/3
c ---[  52]---> Adder-cost: 390   maxlim: 2   bits: 3/2
c ---[  51]---> Adder-cost: 160   maxlim: 2   bits: 3/2
c ---[  50]---> Adder-cost: 180   maxlim: 2   bits: 3/2
c ---[  49]---> Adder-cost: 648   maxlim: 2   bits: 3/2
c ---[  48]---> Adder-cost: 193   maxlim: 2   bits: 3/2
c ---[  47]---> Adder-cost: 832   maxlim: 4   bits: 4/3
c ---[  46]---> Adder-cost: 216   maxlim: 4   bits: 4/3
c ---[  45]---> Adder-cost: 21   maxlim: 1   bits: 2/1
c ---[  44]---> Adder-cost: 497   maxlim: 1   bits: 2/1
c ---[  43]---> Adder-cost: 253   maxlim: 1   bits: 2/1
c ---[  42]---> Adder-cost: 311   maxlim: 1   bits: 2/1
c ---[  41]---> Adder-cost: 197   maxlim: 2   bits: 3/2
c ---[  40]---> Adder-cost: 99   maxlim: 1   bits: 2/1
c ---[  39]---> Adder-cost: 86   maxlim: 1   bits: 2/1
c ---[  38]---> Adder-cost: 110   maxlim: 1   bits: 2/1
c ---[  37]---> Adder-cost: 24   maxlim: 1   bits: 2/1
c ---[  36]---> Adder-cost: 1408   maxlim: 3   bits: 3/2
c ---[  35]---> Adder-cost: 330   maxlim: 4   bits: 4/3
c ---[  34]---> Adder-cost: 271   maxlim: 5   bits: 4/3
c ---[  33]---> Adder-cost: 82   maxlim: 2   bits: 3/2
c ---[  32]---> Adder-cost: 45   maxlim: 1   bits: 2/1
c ---[  31]---> Adder-cost: 21   maxlim: 1   bits: 2/1
c ---[  30]---> Adder-cost: 15   maxlim: 1   bits: 2/1
c ---[  29]---> Adder-cost: 9   maxlim: 1   bits: 2/1
c ---[  28]---> Adder-cost: 53   maxlim: 1   bits: 2/1
c ---[  27]---> Adder-cost: 6   maxlim: 1   bits: 2/1
c ---[  26]---> Adder-cost: 1555   maxlim: 3   bits: 3/2
c ---[  25]---> Adder-cost: 1311   maxlim: 5   bits: 4/3
c ---[  24]---> Adder-cost: 3494   maxlim: 12   bits: 5/4
c ---[  23]---> Adder-cost: 13   maxlim: 1   bits: 2/1
c ---[  22]---> Adder-cost: 1210   maxlim: 3   bits: 3/2
c ---[  21]---> Adder-cost: 29   maxlim: 1   bits: 2/1
c ---[  20]---> Adder-cost: 18   maxlim: 1   bits: 2/1
c ---[  19]---> Adder-cost: 878   maxlim: 3   bits: 3/2
c ---[  18]---> Adder-cost: 2501   maxlim: 18   bits: 6/5
c ---[  17]---> Adder-cost: 85   maxlim: 1   bits: 2/1
c ---[  16]---> Adder-cost: 40   maxlim: 1   bits: 2/1
c ---[  15]---> Adder-cost: 729   maxlim: 2   bits: 3/2
c ---[  14]---> Adder-cost: 119   maxlim: 2   bits: 3/2
c ---[  13]---> Adder-cost: 65   maxlim: 1   bits: 2/1
c ---[  12]---> Adder-cost: 91   maxlim: 2   bits: 3/2
c ---[  11]---> Adder-cost: 4401   maxlim: 11   bits: 5/4
c ---[  10]---> Adder-cost: 3   maxlim: 1   bits: 2/1
c ---[   9]---> Adder-cost: 3318   maxlim: 9   bits: 5/4
c ---[   8]---> Adder-cost: 1067   maxlim: 3   bits: 3/2
c ---[   7]---> Adder-cost: 273   maxlim: 2   bits: 3/2
c ---[   6]---> Adder-cost: 6   maxlim: 1   bits: 2/1
c ---[   5]---> Adder-cost: 3   maxlim: 1   bits: 2/1
c ---[   4]---> Adder-cost: 497   maxlim: 3   bits: 3/2
c ---[   3]---> Adder-cost: 1542   maxlim: 3   bits: 3/2
c ---[   2]---> Adder-cost: 1633   maxlim: 7   bits: 4/3
c ---[   1]---> Adder-cost: 256   maxlim: 1   bits: 2/1
c ---[   0]---> Adder-cost: 68   maxlim: 1   bits: 2/1
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 | 1397768  5242928 |  465922       0        0     nan |  0.000 % |
c |       100 | 1397768  5242928 |  512514     100      388     3.9 |  2.348 % |
c |       250 | 1397768  5242928 |  563765     250      977     3.9 |  2.348 % |
c |       475 | 1397761  5242905 |  620142     474     1844     3.9 |  2.348 % |
c |       812 | 1397735  5242813 |  682156     809     4088     5.1 |  2.350 % |
c |      1318 | 1397662  5242562 |  750372    1307     6379     4.9 |  2.356 % |
c |      2079 | 1397527  5242085 |  825409    2054     9553     4.7 |  2.365 % |
c |      3218 | 1397298  5241275 |  907950    3160    16823     5.3 |  2.378 % |
c |      4928 | 1397024  5240313 |  998745    4832    27889     5.8 |  2.394 % |
c |      7490 | 1396055  5236890 | 1098619    7235    42078     5.8 |  2.449 % |
c |     11334 | 1393517  5228000 | 1208481   10712    64628     6.0 |  2.592 % |
c |     17100 | 1387533  5207159 | 1329329   15526    98156     6.3 |  2.923 % |
c |     25749 | 1381238  5185208 | 1462262   23273   157474     6.8 |  3.273 % |
c |     38723 | 1375895  5166735 | 1608489   35448   288184     8.1 |  3.584 % |
#### 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.97 1.00 0.93 2/54 14358
Raw data (stat): 14358 (runsolver) R 14357 25285 25284 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 481688120 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+10.0001 s]
Raw data (loadavg): 0.98 1.00 0.93 2/54 14358
Raw data (stat): 14358 (minisat+) R 14357 25285 25284 0 -1 0 25753 0 0 0 934 64 0 0 25 0 1 0 481688120 113520640 25015 4294967295 134512640 134672761 3221224544 3221223668 134565995 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27715 25015 603 41 0 27674 0
vsize: 110860
[startup+20.0079 s]
Raw data (loadavg): 0.98 1.00 0.93 2/54 14358
Raw data (stat): 14358 (minisat+) R 14357 25285 25284 0 -1 0 26419 0 0 0 1934 65 0 0 25 0 1 0 481688120 116183040 25681 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28365 25681 603 41 0 28324 0
vsize: 113460
[startup+30.0089 s]
Raw data (loadavg): 0.98 1.00 0.93 2/54 14358
Raw data (stat): 14358 (minisat+) R 14357 25285 25284 0 -1 0 26719 0 0 0 2933 66 0 0 25 0 1 0 481688120 117399552 25981 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28662 25981 603 41 0 28621 0
vsize: 114648
[startup+40.0096 s]
Raw data (loadavg): 0.98 1.00 0.93 2/54 14358
Raw data (stat): 14358 (minisat+) R 14357 25285 25284 0 -1 0 26906 0 0 0 3922 66 0 0 25 0 1 0 481688120 118210560 26168 4294967295 134512640 134672761 3221224544 3221223744 134557911 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28860 26168 603 41 0 28819 0
vsize: 115440
[startup+50.0124 s]
Raw data (loadavg): 0.99 1.00 0.93 2/54 14358
Raw data (stat): 14358 (minisat+) R 14357 25285 25284 0 -1 0 27038 0 0 0 4923 66 0 0 25 0 1 0 481688120 118751232 26300 4294967295 134512640 134672761 3221224544 3221223716 134556651 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28992 26300 603 41 0 28951 0
vsize: 115968
[startup+60.0123 s]
Raw data (loadavg): 0.99 1.00 0.93 2/54 14358
Raw data (stat): 14358 (minisat+) R 14357 25285 25284 0 -1 0 27158 0 0 0 5912 66 0 0 25 0 1 0 481688120 119291904 26420 4294967295 134512640 134672761 3221224544 3221223696 134565086 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29124 26420 603 41 0 29083 0
vsize: 116496
[startup+70.0121 s]
Raw data (loadavg): 0.99 1.00 0.93 2/54 14358
Raw data (stat): 14358 (minisat+) R 14357 25285 25284 0 -1 0 27227 0 0 0 6912 67 0 0 25 0 1 0 481688120 119562240 26489 4294967295 134512640 134672761 3221224544 3221223668 134566109 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29190 26489 603 41 0 29149 0
vsize: 116760
[startup+80.015 s]
Raw data (loadavg): 0.99 1.00 0.93 2/54 14358
Raw data (stat): 14358 (minisat+) R 14357 25285 25284 0 -1 0 27263 0 0 0 7912 67 0 0 25 0 1 0 481688120 119697408 26525 4294967295 134512640 134672761 3221224544 3221223716 134556649 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29223 26525 603 41 0 29182 0
vsize: 116892
[startup+90.0202 s]
Raw data (loadavg): 0.99 1.00 0.93 2/54 14358
Raw data (stat): 14358 (minisat+) R 14357 25285 25284 0 -1 0 27294 0 0 0 8912 67 0 0 25 0 1 0 481688120 119832576 26556 4294967295 134512640 134672761 3221224544 3221223744 134557895 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29256 26556 603 41 0 29215 0
vsize: 117024
[startup+100.021 s]
Raw data (loadavg): 0.99 1.00 0.93 2/54 14358
Raw data (stat): 14358 (minisat+) R 14357 25285 25284 0 -1 0 27321 0 0 0 9913 67 0 0 25 0 1 0 481688120 119967744 26583 4294967295 134512640 134672761 3221224544 3221223716 134556643 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29289 26583 603 41 0 29248 0
vsize: 117156
[startup+110.022 s]
Raw data (loadavg): 0.99 1.00 0.93 2/54 14358
Raw data (stat): 14358 (minisat+) R 14357 25285 25284 0 -1 0 27332 0 0 0 10913 67 0 0 25 0 1 0 481688120 119967744 26594 4294967295 134512640 134672761 3221224544 3221223716 134556632 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29289 26594 603 41 0 29248 0
vsize: 117156
[startup+120.021 s]
Raw data (loadavg): 0.99 1.00 0.93 2/54 14358
Raw data (stat): 14358 (minisat+) R 14357 25285 25284 0 -1 0 27340 0 0 0 11913 67 0 0 25 0 1 0 481688120 119967744 26602 4294967295 134512640 134672761 3221224544 3221223716 134556639 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29289 26602 603 41 0 29248 0
vsize: 117156
[startup+130.038 s]
Raw data (loadavg): 0.99 1.00 0.93 2/54 14358
Raw data (stat): 14358 (minisat+) R 14357 25285 25284 0 -1 0 27360 0 0 0 12914 67 0 0 25 0 1 0 481688120 120102912 26622 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29322 26622 603 41 0 29281 0
vsize: 117288
[startup+140.037 s]
Raw data (loadavg): 0.99 1.00 0.93 2/54 14358
Raw data (stat): 14358 (minisat+) R 14357 25285 25284 0 -1 0 27378 0 0 0 13914 67 0 0 25 0 1 0 481688120 120102912 26640 4294967295 134512640 134672761 3221224544 3221223696 134565092 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29322 26640 603 41 0 29281 0
vsize: 117288
[startup+150.039 s]
Raw data (loadavg): 0.99 1.00 0.93 2/54 14358
Raw data (stat): 14358 (minisat+) R 14357 25285 25284 0 -1 0 27387 0 0 0 14915 67 0 0 25 0 1 0 481688120 120102912 26649 4294967295 134512640 134672761 3221224544 3221223668 134566037 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29322 26649 603 41 0 29281 0
vsize: 117288
[startup+160.039 s]
Raw data (loadavg): 0.99 1.00 0.93 2/54 14358
Raw data (stat): 14358 (minisat+) R 14357 25285 25284 0 -1 0 27401 0 0 0 15915 67 0 0 25 0 1 0 481688120 120238080 26663 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29355 26663 603 41 0 29314 0
vsize: 117420
[startup+170.038 s]
Raw data (loadavg): 0.99 1.00 0.93 2/54 14358
Raw data (stat): 14358 (minisat+) R 14357 25285 25284 0 -1 0 27421 0 0 0 16915 68 0 0 25 0 1 0 481688120 120238080 26683 4294967295 134512640 134672761 3221224544 3221223716 134556606 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29355 26683 603 41 0 29314 0
vsize: 117420
[startup+180.038 s]
Raw data (loadavg): 0.99 1.00 0.93 2/54 14358
Raw data (stat): 14358 (minisat+) R 14357 25285 25284 0 -1 0 27434 0 0 0 17915 68 0 0 25 0 1 0 481688120 120373248 26696 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29388 26696 603 41 0 29347 0
vsize: 117552
[startup+190.038 s]
Raw data (loadavg): 0.99 1.00 0.93 2/54 14358
Raw data (stat): 14358 (minisat+) R 14357 25285 25284 0 -1 0 27494 0 0 0 18915 68 0 0 25 0 1 0 481688120 120508416 26756 4294967295 134512640 134672761 3221224544 3221223712 134560956 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29421 26756 603 41 0 29380 0
vsize: 117684
[startup+200.038 s]
Raw data (loadavg): 0.99 1.00 0.93 2/54 14358
Raw data (stat): 14358 (minisat+) R 14357 25285 25284 0 -1 0 27515 0 0 0 19915 68 0 0 25 0 1 0 481688120 120643584 26777 4294967295 134512640 134672761 3221224544 3221223748 134561964 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29454 26777 603 41 0 29413 0
vsize: 117816
[startup+210.038 s]
Raw data (loadavg): 0.99 1.00 0.93 2/54 14358
Raw data (stat): 14358 (minisat+) R 14357 25285 25284 0 -1 0 27523 0 0 0 20915 68 0 0 25 0 1 0 481688120 120643584 26785 4294967295 134512640 134672761 3221224544 3221223696 134565086 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29454 26785 603 41 0 29413 0
vsize: 117816
[startup+220.038 s]
Raw data (loadavg): 0.99 1.00 0.93 2/54 14358
Raw data (stat): 14358 (minisat+) R 14357 25285 25284 0 -1 0 27531 0 0 0 21915 68 0 0 25 0 1 0 481688120 120643584 26793 4294967295 134512640 134672761 3221224544 3221223744 134557852 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29454 26793 603 41 0 29413 0
vsize: 117816
[startup+230.038 s]
Raw data (loadavg): 0.99 1.00 0.93 2/54 14358
Raw data (stat): 14358 (minisat+) R 14357 25285 25284 0 -1 0 27545 0 0 0 22915 68 0 0 25 0 1 0 481688120 120778752 26807 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29487 26807 603 41 0 29446 0
vsize: 117948
[startup+240.037 s]
Raw data (loadavg): 0.99 1.00 0.93 2/54 14358
Raw data (stat): 14358 (minisat+) R 14357 25285 25284 0 -1 0 27564 0 0 0 23915 68 0 0 25 0 1 0 481688120 120778752 26826 4294967295 134512640 134672761 3221224544 3221223716 134556602 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29487 26826 603 41 0 29446 0
vsize: 117948
[startup+250.037 s]
Raw data (loadavg): 0.99 1.00 0.93 2/54 14358
Raw data (stat): 14358 (minisat+) R 14357 25285 25284 0 -1 0 27568 0 0 0 24915 68 0 0 25 0 1 0 481688120 120778752 26830 4294967295 134512640 134672761 3221224544 3221223716 134556651 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29487 26830 603 41 0 29446 0
vsize: 117948
[startup+260.037 s]
Raw data (loadavg): 0.99 1.00 0.93 2/54 14358
Raw data (stat): 14358 (minisat+) R 14357 25285 25284 0 -1 0 27576 0 0 0 25915 68 0 0 25 0 1 0 481688120 120913920 26838 4294967295 134512640 134672761 3221224544 3221223760 134561987 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29520 26838 603 41 0 29479 0
vsize: 118080
[startup+270.037 s]
Raw data (loadavg): 0.99 1.00 0.93 2/54 14358
Raw data (stat): 14358 (minisat+) R 14357 25285 25284 0 -1 0 27585 0 0 0 26915 68 0 0 25 0 1 0 481688120 120913920 26847 4294967295 134512640 134672761 3221224544 3221223668 134566122 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29520 26847 603 41 0 29479 0
vsize: 118080
[startup+280.038 s]
Raw data (loadavg): 0.99 1.00 0.93 2/54 14358
Raw data (stat): 14358 (minisat+) R 14357 25285 25284 0 -1 0 27595 0 0 0 27916 68 0 0 25 0 1 0 481688120 120913920 26857 4294967295 134512640 134672761 3221224544 3221223668 134566037 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29520 26857 603 41 0 29479 0
vsize: 118080
[startup+290.038 s]
Raw data (loadavg): 0.99 1.00 0.93 2/54 14358
Raw data (stat): 14358 (minisat+) R 14357 25285 25284 0 -1 0 27609 0 0 0 28915 68 0 0 25 0 1 0 481688120 121049088 26871 4294967295 134512640 134672761 3221224544 3221223716 134556682 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29553 26871 603 41 0 29512 0
vsize: 118212
[startup+300.038 s]
Raw data (loadavg): 0.99 1.00 0.93 2/54 14358
Raw data (stat): 14358 (minisat+) R 14357 25285 25284 0 -1 0 27618 0 0 0 29915 68 0 0 25 0 1 0 481688120 121049088 26880 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29553 26880 603 41 0 29512 0
vsize: 118212
[startup+310.038 s]
Raw data (loadavg): 0.99 1.00 0.93 2/54 14358
Raw data (stat): 14358 (minisat+) R 14357 25285 25284 0 -1 0 27623 0 0 0 30915 68 0 0 25 0 1 0 481688120 121049088 26885 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29553 26885 603 41 0 29512 0
vsize: 118212
[startup+320.038 s]
Raw data (loadavg): 0.99 1.00 0.93 2/54 14358
Raw data (stat): 14358 (minisat+) R 14357 25285 25284 0 -1 0 27625 0 0 0 31915 68 0 0 25 0 1 0 481688120 121049088 26887 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29553 26887 603 41 0 29512 0
vsize: 118212
[startup+330.039 s]
Raw data (loadavg): 0.99 1.00 0.93 2/54 14358
Raw data (stat): 14358 (minisat+) R 14357 25285 25284 0 -1 0 27629 0 0 0 32915 68 0 0 25 0 1 0 481688120 121049088 26891 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29553 26891 603 41 0 29512 0
vsize: 118212
[startup+340.039 s]
Raw data (loadavg): 0.99 1.00 0.93 2/54 14358
Raw data (stat): 14358 (minisat+) R 14357 25285 25284 0 -1 0 27631 0 0 0 33915 68 0 0 25 0 1 0 481688120 121049088 26893 4294967295 134512640 134672761 3221224544 3221223716 134556649 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29553 26893 603 41 0 29512 0
vsize: 118212
[startup+350.039 s]
Raw data (loadavg): 0.99 1.00 0.93 2/54 14358
Raw data (stat): 14358 (minisat+) R 14357 25285 25284 0 -1 0 27635 0 0 0 34915 68 0 0 25 0 1 0 481688120 121049088 26897 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29553 26897 603 41 0 29512 0
vsize: 118212
[startup+360.038 s]
Raw data (loadavg): 0.99 1.00 0.93 2/54 14358
Raw data (stat): 14358 (minisat+) R 14357 25285 25284 0 -1 0 27643 0 0 0 35916 68 0 0 25 0 1 0 481688120 121184256 26905 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29586 26905 603 41 0 29545 0
vsize: 118344
[startup+370.038 s]
Raw data (loadavg): 0.99 1.00 0.93 2/54 14358
Raw data (stat): 14358 (minisat+) R 14357 25285 25284 0 -1 0 27645 0 0 0 36916 68 0 0 25 0 1 0 481688120 121184256 26907 4294967295 134512640 134672761 3221224544 3221223716 134556643 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29586 26907 603 41 0 29545 0
vsize: 118344
[startup+380.038 s]
Raw data (loadavg): 0.99 1.00 0.93 2/54 14358
Raw data (stat): 14358 (minisat+) R 14357 25285 25284 0 -1 0 27647 0 0 0 37916 68 0 0 25 0 1 0 481688120 121184256 26909 4294967295 134512640 134672761 3221224544 3221223728 134556589 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29586 26909 603 41 0 29545 0
vsize: 118344
[startup+390.038 s]
Raw data (loadavg): 0.99 1.00 0.93 2/54 14358
Raw data (stat): 14358 (minisat+) R 14357 25285 25284 0 -1 0 27657 0 0 0 38916 68 0 0 25 0 1 0 481688120 121184256 26919 4294967295 134512640 134672761 3221224544 3221223716 134556688 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29586 26919 603 41 0 29545 0
vsize: 118344
[startup+400.039 s]
Raw data (loadavg): 0.99 1.00 0.93 2/54 14358
Raw data (stat): 14358 (minisat+) R 14357 25285 25284 0 -1 0 27659 0 0 0 39916 69 0 0 25 0 1 0 481688120 121184256 26921 4294967295 134512640 134672761 3221224544 3221223668 134566012 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29586 26921 603 41 0 29545 0
vsize: 118344
[startup+410.039 s]
Raw data (loadavg): 0.99 1.00 0.93 2/54 14358
Raw data (stat): 14358 (minisat+) R 14357 25285 25284 0 -1 0 27680 0 0 0 40916 69 0 0 25 0 1 0 481688120 121184256 26942 4294967295 134512640 134672761 3221224544 3221223760 134561948 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29586 26942 603 41 0 29545 0
vsize: 118344
[startup+420.038 s]
Raw data (loadavg): 0.99 1.00 0.93 2/54 14358
Raw data (stat): 14358 (minisat+) R 14357 25285 25284 0 -1 0 27682 0 0 0 41916 69 0 0 25 0 1 0 481688120 121319424 26944 4294967295 134512640 134672761 3221224544 3221223716 134556651 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29619 26944 603 41 0 29578 0
vsize: 118476
[startup+430.039 s]
Raw data (loadavg): 0.99 1.00 0.93 2/54 14358
Raw data (stat): 14358 (minisat+) R 14357 25285 25284 0 -1 0 27684 0 0 0 42917 69 0 0 25 0 1 0 481688120 121319424 26946 4294967295 134512640 134672761 3221224544 3221223716 134556632 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29619 26946 603 41 0 29578 0
vsize: 118476
[startup+440.039 s]
Raw data (loadavg): 0.99 1.00 0.93 2/54 14358
Raw data (stat): 14358 (minisat+) R 14357 25285 25284 0 -1 0 27686 0 0 0 43917 69 0 0 25 0 1 0 481688120 121319424 26948 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29619 26948 603 41 0 29578 0
vsize: 118476
[startup+450.039 s]
Raw data (loadavg): 0.99 1.00 0.93 2/54 14358
Raw data (stat): 14358 (minisat+) R 14357 25285 25284 0 -1 0 27688 0 0 0 44917 69 0 0 25 0 1 0 481688120 121319424 26950 4294967295 134512640 134672761 3221224544 3221223716 134556649 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29619 26950 603 41 0 29578 0
vsize: 118476
[startup+460.039 s]
Raw data (loadavg): 0.99 1.00 0.93 2/54 14358
Raw data (stat): 14358 (minisat+) R 14357 25285 25284 0 -1 0 27691 0 0 0 45917 69 0 0 25 0 1 0 481688120 121319424 26953 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29619 26953 603 41 0 29578 0
vsize: 118476
[startup+470.039 s]
Raw data (loadavg): 0.99 1.00 0.93 2/54 14358
Raw data (stat): 14358 (minisat+) R 14357 25285 25284 0 -1 0 27706 0 0 0 46917 69 0 0 25 0 1 0 481688120 121319424 26968 4294967295 134512640 134672761 3221224544 3221223744 134557842 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29619 26968 603 41 0 29578 0
vsize: 118476
[startup+480.038 s]
Raw data (loadavg): 0.99 1.00 0.93 2/54 14358
Raw data (stat): 14358 (minisat+) R 14357 25285 25284 0 -1 0 27716 0 0 0 47917 69 0 0 25 0 1 0 481688120 121319424 26978 4294967295 134512640 134672761 3221224544 3221223740 134556678 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29619 26978 603 41 0 29578 0
vsize: 118476
[startup+490.038 s]
Raw data (loadavg): 0.99 1.00 0.93 2/54 14358
Raw data (stat): 14358 (minisat+) R 14357 25285 25284 0 -1 0 27728 0 0 0 48917 69 0 0 25 0 1 0 481688120 121454592 26990 4294967295 134512640 134672761 3221224544 3221223716 134556680 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29652 26990 603 41 0 29611 0
vsize: 118608
[startup+500.039 s]
Raw data (loadavg): 0.99 1.00 0.93 2/54 14358
Raw data (stat): 14358 (minisat+) R 14357 25285 25284 0 -1 0 27731 0 0 0 49918 69 0 0 25 0 1 0 481688120 121454592 26993 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29652 26993 603 41 0 29611 0
vsize: 118608
[startup+510.039 s]
Raw data (loadavg): 0.99 1.00 0.93 2/54 14358
Raw data (stat): 14358 (minisat+) R 14357 25285 25284 0 -1 0 27735 0 0 0 50918 69 0 0 25 0 1 0 481688120 121454592 26997 4294967295 134512640 134672761 3221224544 3221223696 134565092 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29652 26997 603 41 0 29611 0
vsize: 118608
[startup+520.039 s]
Raw data (loadavg): 0.99 1.00 0.93 2/54 14358
Raw data (stat): 14358 (minisat+) R 14357 25285 25284 0 -1 0 27740 0 0 0 51918 69 0 0 25 0 1 0 481688120 121454592 27002 4294967295 134512640 134672761 3221224544 3221223744 134557842 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29652 27002 603 41 0 29611 0
vsize: 118608
[startup+530.039 s]
Raw data (loadavg): 0.99 1.00 0.93 2/54 14358
Raw data (stat): 14358 (minisat+) R 14357 25285 25284 0 -1 0 27746 0 0 0 52918 69 0 0 25 0 1 0 481688120 121454592 27008 4294967295 134512640 134672761 3221224544 3221223712 134560845 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29652 27008 603 41 0 29611 0
vsize: 118608
[startup+540.039 s]
Raw data (loadavg): 0.99 1.00 0.93 2/54 14358
Raw data (stat): 14358 (minisat+) R 14357 25285 25284 0 -1 0 27748 0 0 0 53917 69 0 0 25 0 1 0 481688120 121454592 27010 4294967295 134512640 134672761 3221224544 3221223712 134561008 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29652 27010 603 41 0 29611 0
vsize: 118608
[startup+550.04 s]
Raw data (loadavg): 0.99 1.00 0.93 2/54 14358
Raw data (stat): 14358 (minisat+) R 14357 25285 25284 0 -1 0 27751 0 0 0 54917 69 0 0 25 0 1 0 481688120 121454592 27013 4294967295 134512640 134672761 3221224544 3221223716 134556660 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29652 27013 603 41 0 29611 0
vsize: 118608
[startup+560.04 s]
Raw data (loadavg): 0.99 1.00 0.93 2/54 14358
Raw data (stat): 14358 (minisat+) R 14357 25285 25284 0 -1 0 27764 0 0 0 55917 69 0 0 25 0 1 0 481688120 121589760 27026 4294967295 134512640 134672761 3221224544 3221223712 134560822 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29685 27026 603 41 0 29644 0
vsize: 118740
[startup+570.04 s]
Raw data (loadavg): 0.99 1.00 0.93 2/54 14358
Raw data (stat): 14358 (minisat+) R 14357 25285 25284 0 -1 0 27783 0 0 0 56917 69 0 0 25 0 1 0 481688120 121749504 27045 4294967295 134512640 134672761 3221224544 3221223716 134556680 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29724 27045 603 41 0 29683 0
vsize: 118896
[startup+580.041 s]
Raw data (loadavg): 0.99 1.00 0.93 2/54 14358
Raw data (stat): 14358 (minisat+) R 14357 25285 25284 0 -1 0 27783 0 0 0 57918 69 0 0 25 0 1 0 481688120 121749504 27045 4294967295 134512640 134672761 3221224544 3221223712 134560839 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29724 27045 603 41 0 29683 0
vsize: 118896
[startup+590.041 s]
Raw data (loadavg): 0.99 1.00 0.93 2/54 14358
Raw data (stat): 14358 (minisat+) R 14357 25285 25284 0 -1 0 27791 0 0 0 58918 69 0 0 25 0 1 0 481688120 121749504 27053 4294967295 134512640 134672761 3221224544 3221223744 134561972 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29724 27053 603 41 0 29683 0
vsize: 118896
[startup+600.04 s]
Raw data (loadavg): 0.99 1.00 0.93 2/54 14358
Raw data (stat): 14358 (minisat+) R 14357 25285 25284 0 -1 0 27794 0 0 0 59918 70 0 0 25 0 1 0 481688120 121749504 27056 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29724 27056 603 41 0 29683 0
vsize: 118896
[startup+610.041 s]
Raw data (loadavg): 0.99 1.00 0.93 2/54 14358
Raw data (stat): 14358 (minisat+) R 14357 25285 25284 0 -1 0 27805 0 0 0 60918 70 0 0 25 0 1 0 481688120 121749504 27067 4294967295 134512640 134672761 3221224544 3221223716 134556688 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29724 27067 603 41 0 29683 0
vsize: 118896
[startup+620.041 s]
Raw data (loadavg): 0.99 1.00 0.93 2/54 14358
Raw data (stat): 14358 (minisat+) R 14357 25285 25284 0 -1 0 27809 0 0 0 61918 70 0 0 25 0 1 0 481688120 121749504 27071 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29724 27071 603 41 0 29683 0
vsize: 118896
[startup+630.041 s]
Raw data (loadavg): 0.99 1.00 0.93 2/54 14358
Raw data (stat): 14358 (minisat+) R 14357 25285 25284 0 -1 0 27816 0 0 0 62918 70 0 0 25 0 1 0 481688120 121749504 27078 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29724 27078 603 41 0 29683 0
vsize: 118896
[startup+640.042 s]
Raw data (loadavg): 0.99 1.00 0.93 2/54 14358
Raw data (stat): 14358 (minisat+) R 14357 25285 25284 0 -1 0 27826 0 0 0 63919 70 0 0 25 0 1 0 481688120 121749504 27088 4294967295 134512640 134672761 3221224544 3221223668 134566057 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29724 27088 603 41 0 29683 0
vsize: 118896
[startup+650.043 s]
Raw data (loadavg): 0.99 1.00 0.93 2/54 14358
Raw data (stat): 14358 (minisat+) R 14357 25285 25284 0 -1 0 27836 0 0 0 64919 70 0 0 25 0 1 0 481688120 121884672 27098 4294967295 134512640 134672761 3221224544 3221223716 134556667 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29757 27098 603 41 0 29716 0
vsize: 119028
[startup+660.042 s]
Raw data (loadavg): 0.99 1.00 0.93 2/54 14358
Raw data (stat): 14358 (minisat+) R 14357 25285 25284 0 -1 0 27839 0 0 0 65919 70 0 0 25 0 1 0 481688120 121884672 27101 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29757 27101 603 41 0 29716 0
vsize: 119028
[startup+670.042 s]
Raw data (loadavg): 0.99 1.00 0.93 2/54 14358
Raw data (stat): 14358 (minisat+) R 14357 25285 25284 0 -1 0 27842 0 0 0 66919 70 0 0 25 0 1 0 481688120 121884672 27104 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29757 27104 603 41 0 29716 0
vsize: 119028
[startup+680.043 s]
Raw data (loadavg): 0.99 1.00 0.93 2/54 14358
Raw data (stat): 14358 (minisat+) R 14357 25285 25284 0 -1 0 27847 0 0 0 67919 70 0 0 25 0 1 0 481688120 121884672 27109 4294967295 134512640 134672761 3221224544 3221223744 134557842 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29757 27109 603 41 0 29716 0
vsize: 119028
[startup+690.043 s]
Raw data (loadavg): 0.99 1.00 0.93 2/54 14358
Raw data (stat): 14358 (minisat+) R 14357 25285 25284 0 -1 0 27854 0 0 0 68919 70 0 0 25 0 1 0 481688120 121884672 27116 4294967295 134512640 134672761 3221224544 3221223716 134556639 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29757 27116 603 41 0 29716 0
vsize: 119028
[startup+700.044 s]
Raw data (loadavg): 0.99 1.00 0.93 2/54 14358
Raw data (stat): 14358 (minisat+) R 14357 25285 25284 0 -1 0 27857 0 0 0 69920 70 0 0 25 0 1 0 481688120 121884672 27119 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29757 27119 603 41 0 29716 0
vsize: 119028
[startup+710.045 s]
Raw data (loadavg): 0.99 1.00 0.93 2/54 14358
Raw data (stat): 14358 (minisat+) R 14357 25285 25284 0 -1 0 27865 0 0 0 70920 70 0 0 25 0 1 0 481688120 121884672 27127 4294967295 134512640 134672761 3221224544 3221223668 134566075 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29757 27127 603 41 0 29716 0
vsize: 119028
[startup+720.044 s]
Raw data (loadavg): 0.99 1.00 0.93 2/54 14358
Raw data (stat): 14358 (minisat+) R 14357 25285 25284 0 -1 0 27871 0 0 0 71920 70 0 0 25 0 1 0 481688120 121884672 27133 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29757 27133 603 41 0 29716 0
vsize: 119028
[startup+730.044 s]
Raw data (loadavg): 0.99 1.00 0.93 2/54 14358
Raw data (stat): 14358 (minisat+) R 14357 25285 25284 0 -1 0 27874 0 0 0 72920 70 0 0 25 0 1 0 481688120 122019840 27136 4294967295 134512640 134672761 3221224544 3221223744 134557842 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29790 27136 603 41 0 29749 0
vsize: 119160
[startup+740.044 s]
Raw data (loadavg): 0.99 1.00 0.93 2/54 14358
Raw data (stat): 14358 (minisat+) R 14357 25285 25284 0 -1 0 27879 0 0 0 73920 70 0 0 25 0 1 0 481688120 122019840 27141 4294967295 134512640 134672761 3221224544 3221223716 134556649 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29790 27141 603 41 0 29749 0
vsize: 119160
[startup+750.045 s]
Raw data (loadavg): 0.99 1.00 0.93 2/54 14358
Raw data (stat): 14358 (minisat+) R 14357 25285 25284 0 -1 0 27886 0 0 0 74920 70 0 0 25 0 1 0 481688120 122019840 27148 4294967295 134512640 134672761 3221224544 3221223712 134560852 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29790 27148 603 41 0 29749 0
vsize: 119160
[startup+760.045 s]
Raw data (loadavg): 0.99 1.00 0.93 2/54 14358
Raw data (stat): 14358 (minisat+) R 14357 25285 25284 0 -1 0 27889 0 0 0 75920 70 0 0 25 0 1 0 481688120 122019840 27151 4294967295 134512640 134672761 3221224544 3221223752 134561960 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29790 27151 603 41 0 29749 0
vsize: 119160
[startup+770.045 s]
Raw data (loadavg): 0.99 1.00 0.93 2/54 14358
Raw data (stat): 14358 (minisat+) R 14357 25285 25284 0 -1 0 27902 0 0 0 76921 70 0 0 25 0 1 0 481688120 122019840 27164 4294967295 134512640 134672761 3221224544 3221223712 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29790 27164 603 41 0 29749 0
vsize: 119160
[startup+780.045 s]
Raw data (loadavg): 0.99 1.00 0.93 2/54 14358
Raw data (stat): 14358 (minisat+) R 14357 25285 25284 0 -1 0 27912 0 0 0 77921 70 0 0 25 0 1 0 481688120 122019840 27174 4294967295 134512640 134672761 3221224544 3221223712 134560948 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29790 27174 603 41 0 29749 0
vsize: 119160
[startup+790.045 s]
Raw data (loadavg): 0.99 1.00 0.93 2/54 14358
Raw data (stat): 14358 (minisat+) R 14357 25285 25284 0 -1 0 27916 0 0 0 78921 70 0 0 25 0 1 0 481688120 122155008 27178 4294967295 134512640 134672761 3221224544 3221223716 134556596 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29823 27178 603 41 0 29782 0
vsize: 119292
[startup+800.045 s]
Raw data (loadavg): 0.99 1.00 0.93 2/54 14358
Raw data (stat): 14358 (minisat+) R 14357 25285 25284 0 -1 0 27919 0 0 0 79921 70 0 0 25 0 1 0 481688120 122155008 27181 4294967295 134512640 134672761 3221224544 3221223668 134566037 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29823 27181 603 41 0 29782 0
vsize: 119292
[startup+810.045 s]
Raw data (loadavg): 0.99 1.00 0.93 2/54 14358
Raw data (stat): 14358 (minisat+) R 14357 25285 25284 0 -1 0 27924 0 0 0 80921 70 0 0 25 0 1 0 481688120 122155008 27186 4294967295 134512640 134672761 3221224544 3221223696 134565073 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29823 27186 603 41 0 29782 0
vsize: 119292
[startup+820.046 s]
Raw data (loadavg): 0.99 1.00 0.93 2/54 14358
Raw data (stat): 14358 (minisat+) R 14357 25285 25284 0 -1 0 27929 0 0 0 81921 70 0 0 25 0 1 0 481688120 122155008 27191 4294967295 134512640 134672761 3221224544 3221223668 134566052 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29823 27191 603 41 0 29782 0
vsize: 119292
[startup+830.046 s]
Raw data (loadavg): 0.99 1.00 0.93 2/54 14358
Raw data (stat): 14358 (minisat+) R 14357 25285 25284 0 -1 0 27935 0 0 0 82921 70 0 0 25 0 1 0 481688120 122155008 27197 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29823 27197 603 41 0 29782 0
vsize: 119292
[startup+840.045 s]
Raw data (loadavg): 0.99 1.00 0.93 2/54 14358
Raw data (stat): 14358 (minisat+) R 14357 25285 25284 0 -1 0 27946 0 0 0 83921 71 0 0 25 0 1 0 481688120 122155008 27208 4294967295 134512640 134672761 3221224544 3221223668 134566122 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29823 27208 603 41 0 29782 0
vsize: 119292
[startup+850.046 s]
Raw data (loadavg): 0.99 1.00 0.93 2/54 14358
Raw data (stat): 14358 (minisat+) R 14357 25285 25284 0 -1 0 27958 0 0 0 84921 71 0 0 25 0 1 0 481688120 122290176 27220 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29856 27220 603 41 0 29815 0
vsize: 119424
[startup+860.046 s]
Raw data (loadavg): 0.99 1.00 0.93 2/54 14358
Raw data (stat): 14358 (minisat+) R 14357 25285 25284 0 -1 0 27964 0 0 0 85921 71 0 0 25 0 1 0 481688120 122290176 27226 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29856 27226 603 41 0 29815 0
vsize: 119424
[startup+870.046 s]
Raw data (loadavg): 0.99 1.00 0.93 2/54 14358
Raw data (stat): 14358 (minisat+) R 14357 25285 25284 0 -1 0 27972 0 0 0 86921 71 0 0 25 0 1 0 481688120 122290176 27234 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29856 27234 603 41 0 29815 0
vsize: 119424
[startup+880.047 s]
Raw data (loadavg): 0.99 1.00 0.93 2/54 14358
Raw data (stat): 14358 (minisat+) R 14357 25285 25284 0 -1 0 27978 0 0 0 87921 71 0 0 25 0 1 0 481688120 122290176 27240 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29856 27240 603 41 0 29815 0
vsize: 119424
[startup+890.047 s]
Raw data (loadavg): 0.99 1.00 0.93 2/54 14358
Raw data (stat): 14358 (minisat+) R 14357 25285 25284 0 -1 0 27985 0 0 0 88921 71 0 0 25 0 1 0 481688120 122290176 27247 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29856 27247 603 41 0 29815 0
vsize: 119424
[startup+900.047 s]
Raw data (loadavg): 0.99 1.00 0.93 2/54 14358
Raw data (stat): 14358 (minisat+) R 14357 25285 25284 0 -1 0 27989 0 0 0 89922 71 0 0 25 0 1 0 481688120 122290176 27251 4294967295 134512640 134672761 3221224544 3221223716 134556643 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29856 27251 603 41 0 29815 0
vsize: 119424
[startup+910.047 s]
Raw data (loadavg): 0.99 1.00 0.93 2/54 14358
Raw data (stat): 14358 (minisat+) R 14357 25285 25284 0 -1 0 27996 0 0 0 90922 71 0 0 25 0 1 0 481688120 122425344 27258 4294967295 134512640 134672761 3221224544 3221223712 134560839 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29889 27258 603 41 0 29848 0
vsize: 119556
[startup+920.047 s]
Raw data (loadavg): 0.99 1.00 0.93 2/54 14358
Raw data (stat): 14358 (minisat+) R 14357 25285 25284 0 -1 0 28001 0 0 0 91922 71 0 0 25 0 1 0 481688120 122425344 27263 4294967295 134512640 134672761 3221224544 3221223728 134556589 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29889 27263 603 41 0 29848 0
vsize: 119556
[startup+930.047 s]
Raw data (loadavg): 0.99 1.00 0.93 2/54 14358
Raw data (stat): 14358 (minisat+) R 14357 25285 25284 0 -1 0 28017 0 0 0 92922 71 0 0 25 0 1 0 481688120 122425344 27279 4294967295 134512640 134672761 3221224544 3221223716 134556651 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29889 27279 603 41 0 29848 0
vsize: 119556
[startup+940.047 s]
Raw data (loadavg): 0.99 1.00 0.93 2/54 14358
Raw data (stat): 14358 (minisat+) R 14357 25285 25284 0 -1 0 28022 0 0 0 93922 71 0 0 25 0 1 0 481688120 122425344 27284 4294967295 134512640 134672761 3221224544 3221223668 134566034 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29889 27284 603 41 0 29848 0
vsize: 119556
[startup+950.048 s]
Raw data (loadavg): 0.99 1.00 0.93 2/54 14358
Raw data (stat): 14358 (minisat+) R 14357 25285 25284 0 -1 0 28027 0 0 0 94922 71 0 0 25 0 1 0 481688120 122560512 27289 4294967295 134512640 134672761 3221224544 3221223712 134560858 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29922 27289 603 41 0 29881 0
vsize: 119688
[startup+960.052 s]
Raw data (loadavg): 0.99 1.00 0.93 2/54 14358
Raw data (stat): 14358 (minisat+) R 14357 25285 25284 0 -1 0 28031 0 0 0 95923 71 0 0 25 0 1 0 481688120 122560512 27293 4294967295 134512640 134672761 3221224544 3221223712 134560858 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29922 27293 603 41 0 29881 0
vsize: 119688
[startup+970.052 s]
Raw data (loadavg): 0.99 1.00 0.93 2/54 14358
Raw data (stat): 14358 (minisat+) R 14357 25285 25284 0 -1 0 28041 0 0 0 96923 71 0 0 25 0 1 0 481688120 122560512 27303 4294967295 134512640 134672761 3221224544 3221223712 134561188 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29922 27303 603 41 0 29881 0
vsize: 119688
[startup+980.052 s]
Raw data (loadavg): 0.99 1.00 0.93 2/54 14358
Raw data (stat): 14358 (minisat+) R 14357 25285 25284 0 -1 0 28047 0 0 0 97923 71 0 0 25 0 1 0 481688120 122560512 27309 4294967295 134512640 134672761 3221224544 3221223668 134566037 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29922 27309 603 41 0 29881 0
vsize: 119688
[startup+990.052 s]
Raw data (loadavg): 0.99 1.00 0.93 2/54 14358
Raw data (stat): 14358 (minisat+) R 14357 25285 25284 0 -1 0 28056 0 0 0 98923 71 0 0 25 0 1 0 481688120 122560512 27318 4294967295 134512640 134672761 3221224544 3221223716 134556632 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29922 27318 603 41 0 29881 0
vsize: 119688
[startup+1000.05 s]
Raw data (loadavg): 0.99 1.00 0.93 2/54 14358
Raw data (stat): 14358 (minisat+) R 14357 25285 25284 0 -1 0 28061 0 0 0 99924 71 0 0 25 0 1 0 481688120 122695680 27323 4294967295 134512640 134672761 3221224544 3221223748 134561964 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29955 27323 603 41 0 29914 0
vsize: 119820
[startup+1010.05 s]
Raw data (loadavg): 0.99 1.00 0.93 2/54 14358
Raw data (stat): 14358 (minisat+) R 14357 25285 25284 0 -1 0 28072 0 0 0 100924 71 0 0 25 0 1 0 481688120 122695680 27334 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29955 27334 603 41 0 29914 0
vsize: 119820
[startup+1020.05 s]
Raw data (loadavg): 0.99 1.00 0.93 2/54 14358
Raw data (stat): 14358 (minisat+) R 14357 25285 25284 0 -1 0 28083 0 0 0 101924 71 0 0 25 0 1 0 481688120 122695680 27345 4294967295 134512640 134672761 3221224544 3221223680 134560706 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29955 27345 603 41 0 29914 0
vsize: 119820
[startup+1030.05 s]
Raw data (loadavg): 0.99 1.00 0.93 2/54 14358
Raw data (stat): 14358 (minisat+) R 14357 25285 25284 0 -1 0 28093 0 0 0 102924 71 0 0 25 0 1 0 481688120 122695680 27355 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29955 27355 603 41 0 29914 0
vsize: 119820
[startup+1040.05 s]
Raw data (loadavg): 0.99 1.00 0.93 2/54 14358
Raw data (stat): 14358 (minisat+) R 14357 25285 25284 0 -1 0 28101 0 0 0 103924 71 0 0 25 0 1 0 481688120 122830848 27363 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29988 27363 603 41 0 29947 0
vsize: 119952
[startup+1050.05 s]
Raw data (loadavg): 0.99 1.00 0.93 2/54 14358
Raw data (stat): 14358 (minisat+) R 14357 25285 25284 0 -1 0 28106 0 0 0 104924 71 0 0 25 0 1 0 481688120 122830848 27368 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29988 27368 603 41 0 29947 0
vsize: 119952
[startup+1060.05 s]
Raw data (loadavg): 0.99 1.00 0.93 2/54 14358
Raw data (stat): 14358 (minisat+) R 14357 25285 25284 0 -1 0 28113 0 0 0 105925 71 0 0 25 0 1 0 481688120 122830848 27375 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29988 27375 603 41 0 29947 0
vsize: 119952
[startup+1070.05 s]
Raw data (loadavg): 0.99 1.00 0.93 2/54 14358
Raw data (stat): 14358 (minisat+) R 14357 25285 25284 0 -1 0 28116 0 0 0 106925 71 0 0 25 0 1 0 481688120 122830848 27378 4294967295 134512640 134672761 3221224544 3221223760 134561990 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29988 27378 603 41 0 29947 0
vsize: 119952
[startup+1080.05 s]
Raw data (loadavg): 0.99 1.00 0.93 2/54 14358
Raw data (stat): 14358 (minisat+) R 14357 25285 25284 0 -1 0 28124 0 0 0 107925 71 0 0 25 0 1 0 481688120 122830848 27386 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29988 27386 603 41 0 29947 0
vsize: 119952
[startup+1090.05 s]
Raw data (loadavg): 0.99 1.00 0.93 2/54 14358
Raw data (stat): 14358 (minisat+) R 14357 25285 25284 0 -1 0 28127 0 0 0 108925 71 0 0 25 0 1 0 481688120 122830848 27389 4294967295 134512640 134672761 3221224544 3221223712 134561375 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29988 27389 603 41 0 29947 0
vsize: 119952
[startup+1100.06 s]
Raw data (loadavg): 0.99 1.00 0.93 2/54 14358
Raw data (stat): 14358 (minisat+) R 14357 25285 25284 0 -1 0 28130 0 0 0 109925 71 0 0 25 0 1 0 481688120 122830848 27392 4294967295 134512640 134672761 3221224544 3221223668 134566043 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29988 27392 603 41 0 29947 0
vsize: 119952
[startup+1110.06 s]
Raw data (loadavg): 0.99 1.00 0.93 2/54 14358
Raw data (stat): 14358 (minisat+) R 14357 25285 25284 0 -1 0 28165 0 0 0 110925 71 0 0 25 0 1 0 481688120 123092992 27427 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30052 27427 603 41 0 30011 0
vsize: 120208
[startup+1120.05 s]
Raw data (loadavg): 0.99 1.00 0.93 2/54 14358
Raw data (stat): 14358 (minisat+) R 14357 25285 25284 0 -1 0 28165 0 0 0 111925 71 0 0 25 0 1 0 481688120 123092992 27427 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30052 27427 603 41 0 30011 0
vsize: 120208
[startup+1130.06 s]
Raw data (loadavg): 0.99 1.00 0.93 2/54 14358
Raw data (stat): 14358 (minisat+) R 14357 25285 25284 0 -1 0 28172 0 0 0 112926 71 0 0 25 0 1 0 481688120 123228160 27434 4294967295 134512640 134672761 3221224544 3221223736 134556677 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30085 27434 603 41 0 30044 0
vsize: 120340
[startup+1140.06 s]
Raw data (loadavg): 0.99 1.00 0.93 2/54 14358
Raw data (stat): 14358 (minisat+) R 14357 25285 25284 0 -1 0 28187 0 0 0 113926 72 0 0 25 0 1 0 481688120 123228160 27449 4294967295 134512640 134672761 3221224544 3221223744 134561972 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30085 27449 603 41 0 30044 0
vsize: 120340
[startup+1150.06 s]
Raw data (loadavg): 0.99 1.00 0.93 2/54 14358
Raw data (stat): 14358 (minisat+) R 14357 25285 25284 0 -1 0 28199 0 0 0 114925 72 0 0 25 0 1 0 481688120 123228160 27461 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30085 27461 603 41 0 30044 0
vsize: 120340
[startup+1160.06 s]
Raw data (loadavg): 0.99 1.00 0.93 2/54 14358
Raw data (stat): 14358 (minisat+) R 14357 25285 25284 0 -1 0 28201 0 0 0 115925 72 0 0 25 0 1 0 481688120 123228160 27463 4294967295 134512640 134672761 3221224544 3221223716 134556639 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30085 27463 603 41 0 30044 0
vsize: 120340
[startup+1170.06 s]
Raw data (loadavg): 0.99 1.00 0.93 2/54 14358
Raw data (stat): 14358 (minisat+) R 14357 25285 25284 0 -1 0 28212 0 0 0 116924 72 0 0 25 0 1 0 481688120 123363328 27474 4294967295 134512640 134672761 3221224544 3221223668 134566037 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30118 27474 603 41 0 30077 0
vsize: 120472
[startup+1180.06 s]
Raw data (loadavg): 0.99 1.00 0.93 2/54 14358
Raw data (stat): 14358 (minisat+) R 14357 25285 25284 0 -1 0 28221 0 0 0 117924 72 0 0 25 0 1 0 481688120 123363328 27483 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30118 27483 603 41 0 30077 0
vsize: 120472
[startup+1190.06 s]
Raw data (loadavg): 0.99 1.00 0.93 2/54 14358
Raw data (stat): 14358 (minisat+) R 14357 25285 25284 0 -1 0 28230 0 0 0 118925 72 0 0 25 0 1 0 481688120 123363328 27492 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30118 27492 603 41 0 30077 0
vsize: 120472
[startup+1200.06 s]
Raw data (loadavg): 0.99 1.00 0.93 2/54 14358
Raw data (stat): 14358 (minisat+) R 14357 25285 25284 0 -1 0 28236 0 0 0 119925 72 0 0 25 0 1 0 481688120 123363328 27498 4294967295 134512640 134672761 3221224544 3221223712 134560811 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30118 27498 603 41 0 30077 0
vsize: 120472
[startup+1210.07 s]
Raw data (loadavg): 0.99 1.00 0.93 3/54 14358
Raw data (stat): 14358 (minisat+) R 14357 25285 25284 0 -1 0 28253 0 0 0 120926 72 0 0 25 0 1 0 481688120 123498496 27515 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30151 27515 603 41 0 30110 0
vsize: 120604
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1210.21 s]
Raw data (loadavg): 0.99 1.00 0.93 1/54 14358
Raw data (stat): 14358 (minisat+) Z 14357 25285 25284 0 -1 12 28255 0 0 0 120926 77 0 0 20 0 1 0 481688120 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): 1210.21
CPU time (s): 1210.05
CPU user time (s): 1209.27
CPU system time (s): 0.779881
CPU usage (%): 99.9867
Max. virtual memory (Kb): 120604
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####