PB'05 competition: run trace

Some explanations

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

Name	normalized-opb/mps-v2-20-10/plato.asu.edu/pub/unibo/normalized-mps-v2-20-10-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.9513
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 20281

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

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.037
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:        571636 kB
Buffers:         30216 kB
Cached:         406964 kB
SwapCached:        536 kB
Active:          73052 kB
Inactive:       366184 kB
HighTotal:      131008 kB
HighFree:          252 kB
LowTotal:       903652 kB
LowFree:        571384 kB
SwapTotal:     2097136 kB
SwapFree:      2095852 kB
Dirty:              40 kB
Writeback:           0 kB
Mapped:           5224 kB
Slab:            18176 kB
Committed_AS:    63584 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-21 20:54:19 (client local time) WITH STATUS 0 IN 1200.32 SECONDS
stats: 15233 7 1200.32 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.79 0.95 0.90 2/54 12288
Raw data (stat): 12288 (runsolver) R 12287 3260 3259 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 547996069 1052672 99 4294967295 134512640 135381576 3221224432 3221219676 135158418 0 2147483391 7 90112 0 0 0 17 1 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0002 s]
Raw data (loadavg): 0.82 0.95 0.90 2/54 12288
Raw data (stat): 12288 (minisat+) R 12287 3260 3259 0 -1 0 25712 0 0 0 936 63 0 0 25 0 1 0 547996069 113250304 24974 4294967295 134512640 134672761 3221224544 3221223744 134557842 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27649 24974 603 41 0 27608 0
vsize: 110596
[startup+20.0007 s]
Raw data (loadavg): 0.85 0.95 0.91 2/54 12288
Raw data (stat): 12288 (minisat+) R 12287 3260 3259 0 -1 0 26418 0 0 0 1934 65 0 0 25 0 1 0 547996069 116183040 25680 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28365 25680 603 41 0 28324 0
vsize: 113460
[startup+30.0011 s]
Raw data (loadavg): 0.87 0.95 0.91 2/54 12288
Raw data (stat): 12288 (minisat+) R 12287 3260 3259 0 -1 0 26701 0 0 0 2933 66 0 0 25 0 1 0 547996069 117399552 25963 4294967295 134512640 134672761 3221224544 3221223744 134557895 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28662 25963 603 41 0 28621 0
vsize: 114648
[startup+40.0012 s]
Raw data (loadavg): 0.89 0.95 0.91 2/54 12288
Raw data (stat): 12288 (minisat+) R 12287 3260 3259 0 -1 0 26892 0 0 0 3931 67 0 0 25 0 1 0 547996069 118210560 26154 4294967295 134512640 134672761 3221224544 3221223712 134564689 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28860 26154 603 41 0 28819 0
vsize: 115440
[startup+50.0017 s]
Raw data (loadavg): 0.91 0.96 0.91 2/54 12288
Raw data (stat): 12288 (minisat+) R 12287 3260 3259 0 -1 0 27020 0 0 0 4931 68 0 0 25 0 1 0 547996069 118751232 26282 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28992 26282 603 41 0 28951 0
vsize: 115968
[startup+60.0009 s]
Raw data (loadavg): 0.92 0.96 0.91 2/54 12288
Raw data (stat): 12288 (minisat+) R 12287 3260 3259 0 -1 0 27152 0 0 0 5929 69 0 0 25 0 1 0 547996069 119156736 26414 4294967295 134512640 134672761 3221224544 3221223760 134561993 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29091 26414 603 41 0 29050 0
vsize: 116364
[startup+70.002 s]
Raw data (loadavg): 0.93 0.96 0.91 2/54 12288
Raw data (stat): 12288 (minisat+) R 12287 3260 3259 0 -1 0 27212 0 0 0 6929 70 0 0 25 0 1 0 547996069 119427072 26474 4294967295 134512640 134672761 3221224544 3221223716 134556649 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29157 26474 603 41 0 29116 0
vsize: 116628
[startup+80.0026 s]
Raw data (loadavg): 0.94 0.96 0.91 2/54 12288
Raw data (stat): 12288 (minisat+) R 12287 3260 3259 0 -1 0 27256 0 0 0 7929 70 0 0 25 0 1 0 547996069 119697408 26518 4294967295 134512640 134672761 3221224544 3221223716 134556688 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29223 26518 603 41 0 29182 0
vsize: 116892
[startup+90.0018 s]
Raw data (loadavg): 0.95 0.96 0.91 2/54 12288
Raw data (stat): 12288 (minisat+) R 12287 3260 3259 0 -1 0 27292 0 0 0 8929 70 0 0 25 0 1 0 547996069 119832576 26554 4294967295 134512640 134672761 3221224544 3221223716 134556639 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29256 26554 603 41 0 29215 0
vsize: 117024
[startup+100.002 s]
Raw data (loadavg): 0.96 0.96 0.91 2/54 12288
Raw data (stat): 12288 (minisat+) R 12287 3260 3259 0 -1 0 27313 0 0 0 9929 70 0 0 25 0 1 0 547996069 119832576 26575 4294967295 134512640 134672761 3221224544 3221223740 134556584 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29256 26575 603 41 0 29215 0
vsize: 117024
[startup+110.003 s]
Raw data (loadavg): 0.96 0.96 0.91 2/54 12288
Raw data (stat): 12288 (minisat+) R 12287 3260 3259 0 -1 0 27331 0 0 0 10928 71 0 0 25 0 1 0 547996069 119967744 26593 4294967295 134512640 134672761 3221224544 3221223724 134553584 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29289 26593 603 41 0 29248 0
vsize: 117156
[startup+120.004 s]
Raw data (loadavg): 0.97 0.96 0.91 2/54 12288
Raw data (stat): 12288 (minisat+) R 12287 3260 3259 0 -1 0 27338 0 0 0 11928 71 0 0 25 0 1 0 547996069 119967744 26600 4294967295 134512640 134672761 3221224544 3221223744 134557830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29289 26600 603 41 0 29248 0
vsize: 117156
[startup+130.004 s]
Raw data (loadavg): 0.97 0.96 0.91 2/54 12288
Raw data (stat): 12288 (minisat+) R 12287 3260 3259 0 -1 0 27353 0 0 0 12928 72 0 0 25 0 1 0 547996069 119967744 26615 4294967295 134512640 134672761 3221224544 3221223716 134556653 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29289 26615 603 41 0 29248 0
vsize: 117156
[startup+140.003 s]
Raw data (loadavg): 0.98 0.96 0.91 2/54 12288
Raw data (stat): 12288 (minisat+) R 12287 3260 3259 0 -1 0 27370 0 0 0 13927 72 0 0 25 0 1 0 547996069 120102912 26632 4294967295 134512640 134672761 3221224544 3221223716 134556602 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29322 26632 603 41 0 29281 0
vsize: 117288
[startup+150.004 s]
Raw data (loadavg): 0.98 0.97 0.91 2/54 12288
Raw data (stat): 12288 (minisat+) R 12287 3260 3259 0 -1 0 27382 0 0 0 14927 73 0 0 25 0 1 0 547996069 120102912 26644 4294967295 134512640 134672761 3221224544 3221223716 134556649 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29322 26644 603 41 0 29281 0
vsize: 117288
[startup+160.003 s]
Raw data (loadavg): 0.98 0.97 0.91 2/54 12288
Raw data (stat): 12288 (minisat+) R 12287 3260 3259 0 -1 0 27395 0 0 0 15926 73 0 0 25 0 1 0 547996069 120238080 26657 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29355 26657 603 41 0 29314 0
vsize: 117420
[startup+170.004 s]
Raw data (loadavg): 0.98 0.97 0.91 2/54 12288
Raw data (stat): 12288 (minisat+) R 12287 3260 3259 0 -1 0 27418 0 0 0 16926 74 0 0 25 0 1 0 547996069 120238080 26680 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29355 26680 603 41 0 29314 0
vsize: 117420
[startup+180.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12288
Raw data (stat): 12288 (minisat+) R 12287 3260 3259 0 -1 0 27424 0 0 0 17926 74 0 0 25 0 1 0 547996069 120373248 26686 4294967295 134512640 134672761 3221224544 3221223716 134556653 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29388 26686 603 41 0 29347 0
vsize: 117552
[startup+190.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12288
Raw data (stat): 12288 (minisat+) R 12287 3260 3259 0 -1 0 27457 0 0 0 18926 74 0 0 25 0 1 0 547996069 120508416 26719 4294967295 134512640 134672761 3221224544 3221223740 134556584 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29421 26719 603 41 0 29380 0
vsize: 117684
[startup+200.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12288
Raw data (stat): 12288 (minisat+) R 12287 3260 3259 0 -1 0 27511 0 0 0 19926 74 0 0 25 0 1 0 547996069 120643584 26773 4294967295 134512640 134672761 3221224544 3221223716 134556671 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29454 26773 603 41 0 29413 0
vsize: 117816
[startup+210.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12288
Raw data (stat): 12288 (minisat+) R 12287 3260 3259 0 -1 0 27517 0 0 0 20926 75 0 0 25 0 1 0 547996069 120643584 26779 4294967295 134512640 134672761 3221224544 3221223716 134556602 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29454 26779 603 41 0 29413 0
vsize: 117816
[startup+220.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12288
Raw data (stat): 12288 (minisat+) R 12287 3260 3259 0 -1 0 27527 0 0 0 21925 75 0 0 25 0 1 0 547996069 120643584 26789 4294967295 134512640 134672761 3221224544 3221223716 134556682 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29454 26789 603 41 0 29413 0
vsize: 117816
[startup+230.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12288
Raw data (stat): 12288 (minisat+) R 12287 3260 3259 0 -1 0 27535 0 0 0 22925 75 0 0 25 0 1 0 547996069 120778752 26797 4294967295 134512640 134672761 3221224544 3221223716 134556641 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29487 26797 603 41 0 29446 0
vsize: 117948
[startup+240.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12288
Raw data (stat): 12288 (minisat+) R 12287 3260 3259 0 -1 0 27561 0 0 0 23925 76 0 0 25 0 1 0 547996069 120778752 26823 4294967295 134512640 134672761 3221224544 3221223716 134556667 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29487 26823 603 41 0 29446 0
vsize: 117948
[startup+250.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12288
Raw data (stat): 12288 (minisat+) R 12287 3260 3259 0 -1 0 27565 0 0 0 24925 76 0 0 25 0 1 0 547996069 120778752 26827 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29487 26827 603 41 0 29446 0
vsize: 117948
[startup+260.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12288
Raw data (stat): 12288 (minisat+) R 12287 3260 3259 0 -1 0 27569 0 0 0 25925 76 0 0 25 0 1 0 547996069 120778752 26831 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29487 26831 603 41 0 29446 0
vsize: 117948
[startup+270.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12288
Raw data (stat): 12288 (minisat+) R 12287 3260 3259 0 -1 0 27577 0 0 0 26925 76 0 0 25 0 1 0 547996069 120913920 26839 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29520 26839 603 41 0 29479 0
vsize: 118080
[startup+280.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12288
Raw data (stat): 12288 (minisat+) R 12287 3260 3259 0 -1 0 27586 0 0 0 27925 76 0 0 25 0 1 0 547996069 120913920 26848 4294967295 134512640 134672761 3221224544 3221223668 134566034 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29520 26848 603 41 0 29479 0
vsize: 118080
[startup+290.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12288
Raw data (stat): 12288 (minisat+) R 12287 3260 3259 0 -1 0 27599 0 0 0 28925 76 0 0 25 0 1 0 547996069 120913920 26861 4294967295 134512640 134672761 3221224544 3221223708 134564518 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29520 26861 603 41 0 29479 0
vsize: 118080
[startup+300.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12288
Raw data (stat): 12288 (minisat+) R 12287 3260 3259 0 -1 0 27609 0 0 0 29926 76 0 0 25 0 1 0 547996069 121049088 26871 4294967295 134512640 134672761 3221224544 3221223716 134556643 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29553 26871 603 41 0 29512 0
vsize: 118212
[startup+310.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12288
Raw data (stat): 12288 (minisat+) R 12287 3260 3259 0 -1 0 27619 0 0 0 30926 76 0 0 25 0 1 0 547996069 121049088 26881 4294967295 134512640 134672761 3221224544 3221223712 134561415 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29553 26881 603 41 0 29512 0
vsize: 118212
[startup+320.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12288
Raw data (stat): 12288 (minisat+) R 12287 3260 3259 0 -1 0 27624 0 0 0 31926 76 0 0 25 0 1 0 547996069 121049088 26886 4294967295 134512640 134672761 3221224544 3221223748 134561964 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29553 26886 603 41 0 29512 0
vsize: 118212
[startup+330.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12288
Raw data (stat): 12288 (minisat+) R 12287 3260 3259 0 -1 0 27626 0 0 0 32926 76 0 0 25 0 1 0 547996069 121049088 26888 4294967295 134512640 134672761 3221224544 3221223716 134556649 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29553 26888 603 41 0 29512 0
vsize: 118212
[startup+340.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12288
Raw data (stat): 12288 (minisat+) R 12287 3260 3259 0 -1 0 27629 0 0 0 33927 76 0 0 25 0 1 0 547996069 121049088 26891 4294967295 134512640 134672761 3221224544 3221223760 134561999 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29553 26891 603 41 0 29512 0
vsize: 118212
[startup+350.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12288
Raw data (stat): 12288 (minisat+) R 12287 3260 3259 0 -1 0 27631 0 0 0 34927 76 0 0 25 0 1 0 547996069 121049088 26893 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29553 26893 603 41 0 29512 0
vsize: 118212
[startup+360.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12288
Raw data (stat): 12288 (minisat+) R 12287 3260 3259 0 -1 0 27635 0 0 0 35927 76 0 0 25 0 1 0 547996069 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+370.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12288
Raw data (stat): 12288 (minisat+) R 12287 3260 3259 0 -1 0 27643 0 0 0 36927 76 0 0 25 0 1 0 547996069 121184256 26905 4294967295 134512640 134672761 3221224544 3221223712 134560988 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29586 26905 603 41 0 29545 0
vsize: 118344
[startup+380.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12288
Raw data (stat): 12288 (minisat+) R 12287 3260 3259 0 -1 0 27645 0 0 0 37928 76 0 0 25 0 1 0 547996069 121184256 26907 4294967295 134512640 134672761 3221224544 3221223760 134561997 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29586 26907 603 41 0 29545 0
vsize: 118344
[startup+390.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12288
Raw data (stat): 12288 (minisat+) R 12287 3260 3259 0 -1 0 27647 0 0 0 38928 76 0 0 25 0 1 0 547996069 121184256 26909 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29586 26909 603 41 0 29545 0
vsize: 118344
[startup+400.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12288
Raw data (stat): 12288 (minisat+) R 12287 3260 3259 0 -1 0 27657 0 0 0 39928 76 0 0 25 0 1 0 547996069 121184256 26919 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29586 26919 603 41 0 29545 0
vsize: 118344
[startup+410.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12288
Raw data (stat): 12288 (minisat+) R 12287 3260 3259 0 -1 0 27659 0 0 0 40929 76 0 0 25 0 1 0 547996069 121184256 26921 4294967295 134512640 134672761 3221224544 3221223748 134561964 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29586 26921 603 41 0 29545 0
vsize: 118344
[startup+420.02 s]
Raw data (loadavg): 0.99 0.97 0.91 3/54 12288
Raw data (stat): 12288 (minisat+) R 12287 3260 3259 0 -1 0 27674 0 0 0 41929 76 0 0 25 0 1 0 547996069 121184256 26936 4294967295 134512640 134672761 3221224544 3221223648 134560510 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29586 26936 603 41 0 29545 0
vsize: 118344
[startup+430.039 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12288
Raw data (stat): 12288 (minisat+) R 12287 3260 3259 0 -1 0 27682 0 0 0 42931 76 0 0 25 0 1 0 547996069 121319424 26944 4294967295 134512640 134672761 3221224544 3221223716 134556660 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29619 26944 603 41 0 29578 0
vsize: 118476
[startup+440.047 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12288
Raw data (stat): 12288 (minisat+) R 12287 3260 3259 0 -1 0 27684 0 0 0 43932 76 0 0 25 0 1 0 547996069 121319424 26946 4294967295 134512640 134672761 3221224544 3221223748 134561964 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29619 26946 603 41 0 29578 0
vsize: 118476
[startup+450.047 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12288
Raw data (stat): 12288 (minisat+) R 12287 3260 3259 0 -1 0 27686 0 0 0 44932 77 0 0 25 0 1 0 547996069 121319424 26948 4294967295 134512640 134672761 3221224544 3221223716 134556651 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29619 26948 603 41 0 29578 0
vsize: 118476
[startup+460.047 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12288
Raw data (stat): 12288 (minisat+) R 12287 3260 3259 0 -1 0 27688 0 0 0 45932 77 0 0 25 0 1 0 547996069 121319424 26950 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29619 26950 603 41 0 29578 0
vsize: 118476
[startup+470.048 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12288
Raw data (stat): 12288 (minisat+) R 12287 3260 3259 0 -1 0 27691 0 0 0 46932 77 0 0 25 0 1 0 547996069 121319424 26953 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29619 26953 603 41 0 29578 0
vsize: 118476
[startup+480.047 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12288
Raw data (stat): 12288 (minisat+) R 12287 3260 3259 0 -1 0 27699 0 0 0 47932 77 0 0 25 0 1 0 547996069 121319424 26961 4294967295 134512640 134672761 3221224544 3221223716 134556602 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29619 26961 603 41 0 29578 0
vsize: 118476
[startup+490.047 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12288
Raw data (stat): 12288 (minisat+) R 12287 3260 3259 0 -1 0 27715 0 0 0 48932 77 0 0 25 0 1 0 547996069 121319424 26977 4294967295 134512640 134672761 3221224544 3221223744 134557911 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29619 26977 603 41 0 29578 0
vsize: 118476
[startup+500.047 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12288
Raw data (stat): 12288 (minisat+) R 12287 3260 3259 0 -1 0 27728 0 0 0 49932 77 0 0 25 0 1 0 547996069 121454592 26990 4294967295 134512640 134672761 3221224544 3221223760 134561987 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29652 26990 603 41 0 29611 0
vsize: 118608
[startup+510.047 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12288
Raw data (stat): 12288 (minisat+) R 12287 3260 3259 0 -1 0 27730 0 0 0 50933 77 0 0 25 0 1 0 547996069 121454592 26992 4294967295 134512640 134672761 3221224544 3221223744 134557913 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29652 26992 603 41 0 29611 0
vsize: 118608
[startup+520.048 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12288
Raw data (stat): 12288 (minisat+) R 12287 3260 3259 0 -1 0 27733 0 0 0 51933 77 0 0 25 0 1 0 547996069 121454592 26995 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29652 26995 603 41 0 29611 0
vsize: 118608
[startup+530.048 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12288
Raw data (stat): 12288 (minisat+) R 12287 3260 3259 0 -1 0 27740 0 0 0 52933 77 0 0 25 0 1 0 547996069 121454592 27002 4294967295 134512640 134672761 3221224544 3221223716 134556682 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29652 27002 603 41 0 29611 0
vsize: 118608
[startup+540.048 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12288
Raw data (stat): 12288 (minisat+) R 12287 3260 3259 0 -1 0 27744 0 0 0 53932 77 0 0 25 0 1 0 547996069 121454592 27006 4294967295 134512640 134672761 3221224544 3221223716 134556618 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29652 27006 603 41 0 29611 0
vsize: 118608
[startup+550.048 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12288
Raw data (stat): 12288 (minisat+) R 12287 3260 3259 0 -1 0 27748 0 0 0 54932 77 0 0 25 0 1 0 547996069 121454592 27010 4294967295 134512640 134672761 3221224544 3221223712 134560871 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29652 27010 603 41 0 29611 0
vsize: 118608
[startup+560.048 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12288
Raw data (stat): 12288 (minisat+) R 12287 3260 3259 0 -1 0 27751 0 0 0 55932 78 0 0 25 0 1 0 547996069 121454592 27013 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29652 27013 603 41 0 29611 0
vsize: 118608
[startup+570.049 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12288
Raw data (stat): 12288 (minisat+) R 12287 3260 3259 0 -1 0 27753 0 0 0 56932 78 0 0 25 0 1 0 547996069 121454592 27015 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29652 27015 603 41 0 29611 0
vsize: 118608
[startup+580.049 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12288
Raw data (stat): 12288 (minisat+) R 12287 3260 3259 0 -1 0 27765 0 0 0 57932 78 0 0 25 0 1 0 547996069 121589760 27027 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29685 27027 603 41 0 29644 0
vsize: 118740
[startup+590.048 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12288
Raw data (stat): 12288 (minisat+) R 12287 3260 3259 0 -1 0 27783 0 0 0 58932 78 0 0 25 0 1 0 547996069 121749504 27045 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29724 27045 603 41 0 29683 0
vsize: 118896
[startup+600.049 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12288
Raw data (stat): 12288 (minisat+) R 12287 3260 3259 0 -1 0 27791 0 0 0 59933 78 0 0 25 0 1 0 547996069 121749504 27053 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29724 27053 603 41 0 29683 0
vsize: 118896
[startup+610.049 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12288
Raw data (stat): 12288 (minisat+) R 12287 3260 3259 0 -1 0 27792 0 0 0 60933 78 0 0 25 0 1 0 547996069 121749504 27054 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29724 27054 603 41 0 29683 0
vsize: 118896
[startup+620.049 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12288
Raw data (stat): 12288 (minisat+) R 12287 3260 3259 0 -1 0 27802 0 0 0 61933 78 0 0 25 0 1 0 547996069 121749504 27064 4294967295 134512640 134672761 3221224544 3221223716 134556667 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29724 27064 603 41 0 29683 0
vsize: 118896
[startup+630.049 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12288
Raw data (stat): 12288 (minisat+) R 12287 3260 3259 0 -1 0 27807 0 0 0 62933 78 0 0 25 0 1 0 547996069 121749504 27069 4294967295 134512640 134672761 3221224544 3221223716 134556651 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29724 27069 603 41 0 29683 0
vsize: 118896
[startup+640.049 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12288
Raw data (stat): 12288 (minisat+) R 12287 3260 3259 0 -1 0 27814 0 0 0 63933 78 0 0 25 0 1 0 547996069 121749504 27076 4294967295 134512640 134672761 3221224544 3221223716 134556651 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29724 27076 603 41 0 29683 0
vsize: 118896
[startup+650.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12288
Raw data (stat): 12288 (minisat+) R 12287 3260 3259 0 -1 0 27818 0 0 0 64933 78 0 0 25 0 1 0 547996069 121749504 27080 4294967295 134512640 134672761 3221224544 3221223724 134556590 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29724 27080 603 41 0 29683 0
vsize: 118896
[startup+660.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12288
Raw data (stat): 12288 (minisat+) R 12287 3260 3259 0 -1 0 27833 0 0 0 65933 78 0 0 25 0 1 0 547996069 121749504 27095 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29724 27095 603 41 0 29683 0
vsize: 118896
[startup+670.052 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12288
Raw data (stat): 12288 (minisat+) R 12287 3260 3259 0 -1 0 27837 0 0 0 66934 78 0 0 25 0 1 0 547996069 121884672 27099 4294967295 134512640 134672761 3221224544 3221223760 134561985 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29757 27099 603 41 0 29716 0
vsize: 119028
[startup+680.052 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12288
Raw data (stat): 12288 (minisat+) R 12287 3260 3259 0 -1 0 27840 0 0 0 67934 78 0 0 25 0 1 0 547996069 121884672 27102 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29757 27102 603 41 0 29716 0
vsize: 119028
[startup+690.051 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12288
Raw data (stat): 12288 (minisat+) R 12287 3260 3259 0 -1 0 27843 0 0 0 68934 78 0 0 25 0 1 0 547996069 121884672 27105 4294967295 134512640 134672761 3221224544 3221223668 134566075 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29757 27105 603 41 0 29716 0
vsize: 119028
[startup+700.051 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12288
Raw data (stat): 12288 (minisat+) R 12287 3260 3259 0 -1 0 27853 0 0 0 69934 78 0 0 25 0 1 0 547996069 121884672 27115 4294967295 134512640 134672761 3221224544 3221223740 134556678 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29757 27115 603 41 0 29716 0
vsize: 119028
[startup+710.051 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12288
Raw data (stat): 12288 (minisat+) R 12287 3260 3259 0 -1 0 27855 0 0 0 70934 79 0 0 25 0 1 0 547996069 121884672 27117 4294967295 134512640 134672761 3221224544 3221223740 134556584 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29757 27117 603 41 0 29716 0
vsize: 119028
[startup+720.051 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12288
Raw data (stat): 12288 (minisat+) R 12287 3260 3259 0 -1 0 27860 0 0 0 71934 79 0 0 25 0 1 0 547996069 121884672 27122 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29757 27122 603 41 0 29716 0
vsize: 119028
[startup+730.052 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12288
Raw data (stat): 12288 (minisat+) R 12287 3260 3259 0 -1 0 27866 0 0 0 72934 79 0 0 25 0 1 0 547996069 121884672 27128 4294967295 134512640 134672761 3221224544 3221223668 134566120 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29757 27128 603 41 0 29716 0
vsize: 119028
[startup+740.051 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12288
Raw data (stat): 12288 (minisat+) R 12287 3260 3259 0 -1 0 27872 0 0 0 73934 79 0 0 25 0 1 0 547996069 121884672 27134 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29757 27134 603 41 0 29716 0
vsize: 119028
[startup+750.051 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12288
Raw data (stat): 12288 (minisat+) R 12287 3260 3259 0 -1 0 27875 0 0 0 74935 79 0 0 25 0 1 0 547996069 122019840 27137 4294967295 134512640 134672761 3221224544 3221223716 134556649 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29790 27137 603 41 0 29749 0
vsize: 119160
[startup+760.051 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12288
Raw data (stat): 12288 (minisat+) R 12287 3260 3259 0 -1 0 27882 0 0 0 75935 79 0 0 25 0 1 0 547996069 122019840 27144 4294967295 134512640 134672761 3221224544 3221223716 134556682 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29790 27144 603 41 0 29749 0
vsize: 119160
[startup+770.052 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12288
Raw data (stat): 12288 (minisat+) R 12287 3260 3259 0 -1 0 27886 0 0 0 76935 79 0 0 25 0 1 0 547996069 122019840 27148 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29790 27148 603 41 0 29749 0
vsize: 119160
[startup+780.052 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12288
Raw data (stat): 12288 (minisat+) R 12287 3260 3259 0 -1 0 27893 0 0 0 77935 79 0 0 25 0 1 0 547996069 122019840 27155 4294967295 134512640 134672761 3221224544 3221223712 134560852 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29790 27155 603 41 0 29749 0
vsize: 119160
[startup+790.052 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12288
Raw data (stat): 12288 (minisat+) R 12287 3260 3259 0 -1 0 27906 0 0 0 78935 79 0 0 25 0 1 0 547996069 122019840 27168 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29790 27168 603 41 0 29749 0
vsize: 119160
[startup+800.058 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12288
Raw data (stat): 12288 (minisat+) R 12287 3260 3259 0 -1 0 27912 0 0 0 79936 79 0 0 25 0 1 0 547996069 122019840 27174 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29790 27174 603 41 0 29749 0
vsize: 119160
[startup+810.067 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12288
Raw data (stat): 12288 (minisat+) R 12287 3260 3259 0 -1 0 27916 0 0 0 80937 79 0 0 25 0 1 0 547996069 122155008 27178 4294967295 134512640 134672761 3221224544 3221223680 134560557 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29823 27178 603 41 0 29782 0
vsize: 119292
[startup+820.073 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12288
Raw data (stat): 12288 (minisat+) R 12287 3260 3259 0 -1 0 27920 0 0 0 81938 79 0 0 25 0 1 0 547996069 122155008 27182 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29823 27182 603 41 0 29782 0
vsize: 119292
[startup+830.074 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12288
Raw data (stat): 12288 (minisat+) R 12287 3260 3259 0 -1 0 27924 0 0 0 82938 79 0 0 25 0 1 0 547996069 122155008 27186 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29823 27186 603 41 0 29782 0
vsize: 119292
[startup+840.073 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12288
Raw data (stat): 12288 (minisat+) R 12287 3260 3259 0 -1 0 27930 0 0 0 83938 79 0 0 25 0 1 0 547996069 122155008 27192 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29823 27192 603 41 0 29782 0
vsize: 119292
[startup+850.081 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12288
Raw data (stat): 12288 (minisat+) R 12287 3260 3259 0 -1 0 27935 0 0 0 84939 80 0 0 25 0 1 0 547996069 122155008 27197 4294967295 134512640 134672761 3221224544 3221223716 134556646 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29823 27197 603 41 0 29782 0
vsize: 119292
[startup+860.082 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12288
Raw data (stat): 12288 (minisat+) R 12287 3260 3259 0 -1 0 27946 0 0 0 85938 80 0 0 25 0 1 0 547996069 122155008 27208 4294967295 134512640 134672761 3221224544 3221223748 134561964 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29823 27208 603 41 0 29782 0
vsize: 119292
[startup+870.082 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12288
Raw data (stat): 12288 (minisat+) R 12287 3260 3259 0 -1 0 27958 0 0 0 86938 80 0 0 25 0 1 0 547996069 122290176 27220 4294967295 134512640 134672761 3221224544 3221223712 134561198 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29856 27220 603 41 0 29815 0
vsize: 119424
[startup+880.083 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12288
Raw data (stat): 12288 (minisat+) R 12287 3260 3259 0 -1 0 27964 0 0 0 87938 80 0 0 25 0 1 0 547996069 122290176 27226 4294967295 134512640 134672761 3221224544 3221223712 134561391 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29856 27226 603 41 0 29815 0
vsize: 119424
[startup+890.091 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12288
Raw data (stat): 12288 (minisat+) R 12287 3260 3259 0 -1 0 27972 0 0 0 88939 80 0 0 25 0 1 0 547996069 122290176 27234 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29856 27234 603 41 0 29815 0
vsize: 119424
[startup+900.094 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12288
Raw data (stat): 12288 (minisat+) R 12287 3260 3259 0 -1 0 27978 0 0 0 89939 80 0 0 25 0 1 0 547996069 122290176 27240 4294967295 134512640 134672761 3221224544 3221223668 134566049 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29856 27240 603 41 0 29815 0
vsize: 119424
[startup+910.094 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12288
Raw data (stat): 12288 (minisat+) R 12287 3260 3259 0 -1 0 27985 0 0 0 90939 80 0 0 25 0 1 0 547996069 122290176 27247 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29856 27247 603 41 0 29815 0
vsize: 119424
[startup+920.094 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12288
Raw data (stat): 12288 (minisat+) R 12287 3260 3259 0 -1 0 27988 0 0 0 91940 80 0 0 25 0 1 0 547996069 122290176 27250 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29856 27250 603 41 0 29815 0
vsize: 119424
[startup+930.095 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12288
Raw data (stat): 12288 (minisat+) R 12287 3260 3259 0 -1 0 27991 0 0 0 92940 80 0 0 25 0 1 0 547996069 122425344 27253 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29889 27253 603 41 0 29848 0
vsize: 119556
[startup+940.095 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12288
Raw data (stat): 12288 (minisat+) R 12287 3260 3259 0 -1 0 28001 0 0 0 93940 80 0 0 25 0 1 0 547996069 122425344 27263 4294967295 134512640 134672761 3221224544 3221223708 134561028 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29889 27263 603 41 0 29848 0
vsize: 119556
[startup+950.095 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12288
Raw data (stat): 12288 (minisat+) R 12287 3260 3259 0 -1 0 28016 0 0 0 94940 81 0 0 25 0 1 0 547996069 122425344 27278 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29889 27278 603 41 0 29848 0
vsize: 119556
[startup+960.095 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12288
Raw data (stat): 12288 (minisat+) R 12287 3260 3259 0 -1 0 28021 0 0 0 95940 81 0 0 25 0 1 0 547996069 122425344 27283 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29889 27283 603 41 0 29848 0
vsize: 119556
[startup+970.096 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12288
Raw data (stat): 12288 (minisat+) R 12287 3260 3259 0 -1 0 28026 0 0 0 96940 81 0 0 25 0 1 0 547996069 122560512 27288 4294967295 134512640 134672761 3221224544 3221223716 134556682 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29922 27288 603 41 0 29881 0
vsize: 119688
[startup+980.096 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12288
Raw data (stat): 12288 (minisat+) R 12287 3260 3259 0 -1 0 28030 0 0 0 97940 81 0 0 25 0 1 0 547996069 122560512 27292 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29922 27292 603 41 0 29881 0
vsize: 119688
[startup+990.096 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12288
Raw data (stat): 12288 (minisat+) R 12287 3260 3259 0 -1 0 28036 0 0 0 98940 81 0 0 25 0 1 0 547996069 122560512 27298 4294967295 134512640 134672761 3221224544 3221223744 134557885 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29922 27298 603 41 0 29881 0
vsize: 119688
[startup+1000.1 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12288
Raw data (stat): 12288 (minisat+) R 12287 3260 3259 0 -1 0 28046 0 0 0 99941 81 0 0 25 0 1 0 547996069 122560512 27308 4294967295 134512640 134672761 3221224544 3221223760 134561990 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29922 27308 603 41 0 29881 0
vsize: 119688
[startup+1010.1 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12288
Raw data (stat): 12288 (minisat+) R 12287 3260 3259 0 -1 0 28054 0 0 0 100941 81 0 0 25 0 1 0 547996069 122560512 27316 4294967295 134512640 134672761 3221224544 3221223668 134566037 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29922 27316 603 41 0 29881 0
vsize: 119688
[startup+1020.1 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12288
Raw data (stat): 12288 (minisat+) R 12287 3260 3259 0 -1 0 28060 0 0 0 101941 81 0 0 25 0 1 0 547996069 122560512 27322 4294967295 134512640 134672761 3221224544 3221223740 134556678 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29922 27322 603 41 0 29881 0
vsize: 119688
[startup+1030.1 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12288
Raw data (stat): 12288 (minisat+) R 12287 3260 3259 0 -1 0 28070 0 0 0 102941 81 0 0 25 0 1 0 547996069 122695680 27332 4294967295 134512640 134672761 3221224544 3221223712 134560785 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29955 27332 603 41 0 29914 0
vsize: 119820
[startup+1040.1 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12288
Raw data (stat): 12288 (minisat+) R 12287 3260 3259 0 -1 0 28075 0 0 0 103941 81 0 0 25 0 1 0 547996069 122695680 27337 4294967295 134512640 134672761 3221224544 3221223712 134561021 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29955 27337 603 41 0 29914 0
vsize: 119820
[startup+1050.1 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12288
Raw data (stat): 12288 (minisat+) R 12287 3260 3259 0 -1 0 28091 0 0 0 104941 81 0 0 25 0 1 0 547996069 122695680 27353 4294967295 134512640 134672761 3221224544 3221223744 134557911 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29955 27353 603 41 0 29914 0
vsize: 119820
[startup+1060.1 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12288
Raw data (stat): 12288 (minisat+) R 12287 3260 3259 0 -1 0 28099 0 0 0 105942 81 0 0 25 0 1 0 547996069 122695680 27361 4294967295 134512640 134672761 3221224544 3221223712 134561201 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29955 27361 603 41 0 29914 0
vsize: 119820
[startup+1070.1 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12288
Raw data (stat): 12288 (minisat+) R 12287 3260 3259 0 -1 0 28103 0 0 0 106942 81 0 0 25 0 1 0 547996069 122830848 27365 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29988 27365 603 41 0 29947 0
vsize: 119952
[startup+1080.1 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12288
Raw data (stat): 12288 (minisat+) R 12287 3260 3259 0 -1 0 28110 0 0 0 107942 82 0 0 25 0 1 0 547996069 122830848 27372 4294967295 134512640 134672761 3221224544 3221223668 134566034 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29988 27372 603 41 0 29947 0
vsize: 119952
[startup+1090.11 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12288
Raw data (stat): 12288 (minisat+) R 12287 3260 3259 0 -1 0 28115 0 0 0 108943 82 0 0 25 0 1 0 547996069 122830848 27377 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29988 27377 603 41 0 29947 0
vsize: 119952
[startup+1100.11 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12288
Raw data (stat): 12288 (minisat+) R 12287 3260 3259 0 -1 0 28121 0 0 0 109943 82 0 0 25 0 1 0 547996069 122830848 27383 4294967295 134512640 134672761 3221224544 3221223668 134566034 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29988 27383 603 41 0 29947 0
vsize: 119952
[startup+1110.11 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12288
Raw data (stat): 12288 (minisat+) R 12287 3260 3259 0 -1 0 28126 0 0 0 110943 82 0 0 25 0 1 0 547996069 122830848 27388 4294967295 134512640 134672761 3221224544 3221223712 134564722 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29988 27388 603 41 0 29947 0
vsize: 119952
[startup+1120.11 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12288
Raw data (stat): 12288 (minisat+) R 12287 3260 3259 0 -1 0 28128 0 0 0 111943 82 0 0 25 0 1 0 547996069 122830848 27390 4294967295 134512640 134672761 3221224544 3221223716 134556641 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29988 27390 603 41 0 29947 0
vsize: 119952
[startup+1130.11 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12288
Raw data (stat): 12288 (minisat+) R 12287 3260 3259 0 -1 0 28131 0 0 0 112943 82 0 0 25 0 1 0 547996069 122830848 27393 4294967295 134512640 134672761 3221224544 3221223680 134560566 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29988 27393 603 41 0 29947 0
vsize: 119952
[startup+1140.11 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12288
Raw data (stat): 12288 (minisat+) R 12287 3260 3259 0 -1 0 28165 0 0 0 113943 82 0 0 25 0 1 0 547996069 123092992 27427 4294967295 134512640 134672761 3221224544 3221223668 134566109 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30052 27427 603 41 0 30011 0
vsize: 120208
[startup+1150.11 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12288
Raw data (stat): 12288 (minisat+) R 12287 3260 3259 0 -1 0 28165 0 0 0 114943 82 0 0 25 0 1 0 547996069 123092992 27427 4294967295 134512640 134672761 3221224544 3221223732 134556588 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30052 27427 603 41 0 30011 0
vsize: 120208
[startup+1160.11 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12288
Raw data (stat): 12288 (minisat+) R 12287 3260 3259 0 -1 0 28178 0 0 0 115943 83 0 0 25 0 1 0 547996069 123228160 27440 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30085 27440 603 41 0 30044 0
vsize: 120340
[startup+1170.11 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12288
Raw data (stat): 12288 (minisat+) R 12287 3260 3259 0 -1 0 28188 0 0 0 116943 83 0 0 25 0 1 0 547996069 123228160 27450 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30085 27450 603 41 0 30044 0
vsize: 120340
[startup+1180.11 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12288
Raw data (stat): 12288 (minisat+) R 12287 3260 3259 0 -1 0 28200 0 0 0 117943 83 0 0 25 0 1 0 547996069 123228160 27462 4294967295 134512640 134672761 3221224544 3221223716 134556688 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30085 27462 603 41 0 30044 0
vsize: 120340
[startup+1190.11 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12288
Raw data (stat): 12288 (minisat+) R 12287 3260 3259 0 -1 0 28205 0 0 0 118943 83 0 0 25 0 1 0 547996069 123363328 27467 4294967295 134512640 134672761 3221224544 3221223744 134557809 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30118 27467 603 41 0 30077 0
vsize: 120472
[startup+1200.11 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12288
Raw data (stat): 12288 (minisat+) R 12287 3260 3259 0 -1 0 28215 0 0 0 119943 83 0 0 25 0 1 0 547996069 123363328 27477 4294967295 134512640 134672761 3221224544 3221223712 134560806 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30118 27477 603 41 0 30077 0
vsize: 120472
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.17 s]
Raw data (loadavg): 0.99 0.97 0.91 1/54 12288
Raw data (stat): 12288 (minisat+) Z 12287 3260 3259 0 -1 12 28217 0 0 0 119943 88 0 0 25 0 1 0 547996069 0 0 4294967295 0 0 0 0 0 0 16384 5 16386 3222412051 0 0 17 1 0 0
Raw data (statm): 0 0 0 0 0 0 0
vsize: 0
Maximum CPU time exceeded: sending SIGTERM and SIGKILL

Child status: 0
Real time (s): 1200.17
CPU time (s): 1200.32
CPU user time (s): 1199.43
CPU system time (s): 0.888864
CPU usage (%): 100.013
Max. virtual memory (Kb): 120472
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####