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/ftp.netlib.org/lp/data/normalized-mps-v2-20-10-degen3.opb
MD5SUM	7312c1a4c94073cc51821da54f781db8
Bench Category	optimization, big integers (OPTBIGINT)
Has Objective Function	YES
Satisfiable	NO
(Un)Satisfiability was proved
Best value of the objective function
Optimality of the best value was proved
Number of terms in the objective function	47190
Biggest coefficient in the objective function	1001264250880
Number of bits for the biggest coefficient in the objective function	40
Sum of the numbers in the objective function	339379725479256
Number of bits of the sum of numbers in the objective function	49
Biggest number in a constraint	1001264250880
Number of bits of the biggest number in a constraint	40
Biggest sum of numbers in a constraint	339379725479256
Number of bits of the biggest sum of numbers	49
Best result obtained on this benchmark	UNSAT
Best CPU time to get the best result obtained on this benchmark	0.474927
Number of variables	54540
Total number of constraints	1503
Number of constraints which are clauses	0
Number of constraints which are cardinality constraints (but not clauses)	0
Number of constraints which are nor clauses,nor cardinality constraints	1503
Minimum length of a constraint	60
Maximum length of a constraint	6090
Trace number 30627

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

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.042
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:        650892 kB
Buffers:         34580 kB
Cached:         323640 kB
SwapCached:        412 kB
Active:         108284 kB
Inactive:       252276 kB
HighTotal:      131008 kB
HighFree:          252 kB
LowTotal:       903652 kB
LowFree:        650640 kB
SwapTotal:     2097136 kB
SwapFree:      2096036 kB
Dirty:              24 kB
Writeback:           0 kB
Mapped:           5696 kB
Slab:            17596 kB
Committed_AS:    63732 kB
PageTables:        320 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-05-25 18:24:56 (client local time) WITH STATUS 152 IN 1229.99 SECONDS
stats: 22008 7 1229.99 152
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 2220 PB-constraints to clauses...
c   -- Unit propagations: ppp
c   -- Detecting intervals from adjacent constraints: #############################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################
c   -- Clauses(.)/Splits(s): (none)
c ---[2219]---> Adder-cost: 5386   maxlim: 10531650   bits: 24/24
c ---[2218]---> Adder-cost: 5034   maxlim: 4974402   bits: 23/23
c ---[2217]---> Adder-cost: 5150   maxlim: 5435203   bits: 23/23
c ---[2215]---> Adder-cost: 418   maxlim: 20470   bits: 16/15
c ---[2213]---> Adder-cost: 418   maxlim: 20470   bits: 16/15
c ---[2211]---> Sorter-cost:  400     Base: 2 2 2 2 2 2 2 2 2 2
c ---[2209]---> Sorter-cost:  400     Base: 2 2 2 2 2 2 2 2 2 2
c ---[2207]---> Sorter-cost:  866     Base: 2 2 2 2 2 2 2 2 2 2
c ---[2205]---> Sorter-cost:  866     Base: 2 2 2 2 2 2 2 2 2 2
c ---[2203]---> Sorter-cost:  400     Base: 2 2 2 2 2 2 2 2 2 2
c ---[2201]---> Sorter-cost:  400     Base: 2 2 2 2 2 2 2 2 2 2
c ---[2199]---> Sorter-cost:  400     Base: 2 2 2 2 2 2 2 2 2 2
c ---[2197]---> Sorter-cost:  400     Base: 2 2 2 2 2 2 2 2 2 2
c ---[2195]---> Sorter-cost:  400     Base: 2 2 2 2 2 2 2 2 2 2
c ---[2193]---> Sorter-cost: 1322     Base: 2 2 2 2 2 2 2 2 2 2
c ---[2191]---> Sorter-cost: 1322     Base: 2 2 2 2 2 2 2 2 2 2
c ---[2189]---> Sorter-cost: 2089     Base: 2 2 2 2 2 2 2 2 2 2
c ---[2187]---> Sorter-cost: 1322     Base: 2 2 2 2 2 2 2 2 2 2
c ---[2185]---> Sorter-cost:  866     Base: 2 2 2 2 2 2 2 2 2 2
c ---[2183]---> Sorter-cost:  631     Base: 2 2 2 2 2 2 2 2 2 2
c ---[2181]---> Sorter-cost:  866     Base: 2 2 2 2 2 2 2 2 2 2
c ---[2179]---> Sorter-cost:  866     Base: 2 2 2 2 2 2 2 2 2 2
c ---[2177]---> Sorter-cost: 1322     Base: 2 2 2 2 2 2 2 2 2 2
c ---[2175]---> Sorter-cost:  400     Base: 2 2 2 2 2 2 2 2 2 2
c ---[2173]---> BDD-cost:   31
c ---[2171]---> BDD-cost:   31
c ---[2169]---> Adder-cost: 946   maxlim: 45034   bits: 17/16
c ---[2167]---> Adder-cost: 880   maxlim: 40940   bits: 17/16
c ---[2165]---> Sorter-cost:  400     Base: 2 2 2 2 2 2 2 2 2 2
c ---[2163]---> Sorter-cost:  400     Base: 2 2 2 2 2 2 2 2 2 2
c ---[2161]---> Sorter-cost:  400     Base: 2 2 2 2 2 2 2 2 2 2
c ---[2159]---> Sorter-cost:  400     Base: 2 2 2 2 2 2 2 2 2 2
c ---[2157]---> Sorter-cost:  400     Base: 2 2 2 2 2 2 2 2 2 2
c ---[2155]---> Sorter-cost:  400     Base: 2 2 2 2 2 2 2 2 2 2
c ---[2153]---> Sorter-cost:  866     Base: 2 2 2 2 2 2 2 2 2 2
c ---[2151]---> Sorter-cost:  631     Base: 2 2 2 2 2 2 2 2 2 2
c ---[2149]---> Sorter-cost:  400     Base: 2 2 2 2 2 2 2 2 2 2
c ---[2147]---> Sorter-cost:  400     Base: 2 2 2 2 2 2 2 2 2 2
c ---[2145]---> Adder-cost: 242   maxlim: 12282   bits: 15/14
c ---[2143]---> Sorter-cost: 2375     Base: 2 2 2 2 2 2 2 2 2 2
c ---[2141]---> Adder-cost: 3740   maxlim: 178089   bits: 19/18
c ---[2139]---> Adder-cost: 2585   maxlim: 92115   bits: 18/17
c ---[2137]---> Adder-cost: 330   maxlim: 16376   bits: 15/14
c ---[2135]---> Adder-cost: 330   maxlim: 16376   bits: 15/14
c ---[2133]---> Sorter-cost:  400     Base: 2 2 2 2 2 2 2 2 2 2
c ---[2131]---> Sorter-cost:  400     Base: 2 2 2 2 2 2 2 2 2 2
c ---[2129]---> Sorter-cost:  400     Base: 2 2 2 2 2 2 2 2 2 2
c ---[2127]---> Sorter-cost:  400     Base: 2 2 2 2 2 2 2 2 2 2
c ---[2125]---> Sorter-cost:  400     Base: 2 2 2 2 2 2 2 2 2 2
c ---[2123]---> Sorter-cost:  400     Base: 2 2 2 2 2 2 2 2 2 2
c ---[2121]---> Sorter-cost: 1322     Base: 2 2 2 2 2 2 2 2 2 2
c ---[2119]---> Sorter-cost: 1322     Base: 2 2 2 2 2 2 2 2 2 2
c ---[2117]---> Sorter-cost: 2089     Base: 2 2 2 2 2 2 2 2 2 2
c ---[2115]---> Sorter-cost: 2089     Base: 2 2 2 2 2 2 2 2 2 2
c ---[2113]---> Sorter-cost:  866     Base: 2 2 2 2 2 2 2 2 2 2
c ---[2111]---> Sorter-cost:  631     Base: 2 2 2 2 2 2 2 2 2 2
c ---[2109]---> Sorter-cost:  866     Base: 2 2 2 2 2 2 2 2 2 2
c ---[2107]---> Sorter-cost:  631     Base: 2 2 2 2 2 2 2 2 2 2
c ---[2105]---> Sorter-cost:  866     Base: 2 2 2 2 2 2 2 2 2 2
c ---[2103]---> Sorter-cost:  866     Base: 2 2 2 2 2 2 2 2 2 2
c ---[2101]---> Sorter-cost:  866     Base: 2 2 2 2 2 2 2 2 2 2
c ---[2099]---> Sorter-cost:  866     Base: 2 2 2 2 2 2 2 2 2 2
c ---[2097]---> Sorter-cost:  400     Base: 2 2 2 2 2 2 2 2 2 2
c ---[2095]---> Sorter-cost:  400     Base: 2 2 2 2 2 2 2 2 2 2
c ---[2093]---> Adder-cost: 286   maxlim: 14329   bits: 15/14
c ---[2091]---> Sorter-cost: 2090     Base: 2 2 2 2 2 2 2 2 2 2
c ---[2089]---> Sorter-cost:  400     Base: 2 2 2 2 2 2 2 2 2 2
c ---[2087]---> Sorter-cost:  400     Base: 2 2 2 2 2 2 2 2 2 2
c ---[2085]---> Sorter-cost: 1322     Base: 2 2 2 2 2 2 2 2 2 2
c ---[2083]---> Sorter-cost:  631     Base: 2 2 2 2 2 2 2 2 2 2
c ---[2081]---> Sorter-cost:  400     Base: 2 2 2 2 2 2 2 2 2 2
c ---[2079]---> Sorter-cost:  866     Base: 2 2 2 2 2 2 2 2 2 2
c ---[2077]---> Sorter-cost:  400     Base: 2 2 2 2 2 2 2 2 2 2
c ---[2075]---> Sorter-cost: 2375     Base: 2 2 2 2 2 2 2 2 2 2
c ---[2073]---> Sorter-cost: 2375     Base: 2 2 2 2 2 2 2 2 2 2
c ---[2071]---> Sorter-cost:  400     Base: 2 2 2 2 2 2 2 2 2 2
c ---[2069]---> Sorter-cost:  400     Base: 2 2 2 2 2 2 2 2 2 2
c ---[2067]---> Sorter-cost:  400     Base: 2 2 2 2 2 2 2 2 2 2
c ---[2065]---> Sorter-cost:  400     Base: 2 2 2 2 2 2 2 2 2 2
c ---[2063]---> Sorter-cost:  400     Base: 2 2 2 2 2 2 2 2 2 2
c ---[2061]---> Sorter-cost:  400     Base: 2 2 2 2 2 2 2 2 2 2
c ---[2059]---> Sorter-cost:  400     Base: 2 2 2 2 2 2 2 2 2 2
c ---[2057]---> BDD-cost:   91
c ---[2055]---> Adder-cost: 1430   maxlim: 67551   bits: 18/17
c ---[2053]---> Adder-cost: 1232   maxlim: 65504   bits: 17/16
c ---[2051]---> Sorter-cost:  866     Base: 2 2 2 2 2 2 2 2 2 2
c ---[2049]---> Sorter-cost:  866     Base: 2 2 2 2 2 2 2 2 2 2
c ---[2047]---> Adder-cost: 748   maxlim: 36846   bits: 17/16
c ---[2045]---> Adder-cost: 726   maxlim: 36846   bits: 17/16
c ---[2043]---> Sorter-cost: 1322     Base: 2 2 2 2 2 2 2 2 2 2
c ---[2041]---> Sorter-cost: 1322     Base: 2 2 2 2 2 2 2 2 2 2
c ---[2039]---> Sorter-cost: 1322     Base: 2 2 2 2 2 2 2 2 2 2
c ---[2037]---> Sorter-cost: 1322     Base: 2 2 2 2 2 2 2 2 2 2
c ---[2035]---> Sorter-cost: 1322     Base: 2 2 2 2 2 2 2 2 2 2
c ---[2033]---> Sorter-cost: 1322     Base: 2 2 2 2 2 2 2 2 2 2
c ---[2031]---> Sorter-cost: 1322     Base: 2 2 2 2 2 2 2 2 2 2
c ---[2029]---> Sorter-cost: 1322     Base: 2 2 2 2 2 2 2 2 2 2
c ---[2027]---> Sorter-cost: 1322     Base: 2 2 2 2 2 2 2 2 2 2
c ---[2025]---> Sorter-cost:  866     Base: 2 2 2 2 2 2 2 2 2 2
c ---[2023]---> Sorter-cost:  400     Base: 2 2 2 2 2 2 2 2 2 2
c ---[2021]---> Sorter-cost:  400     Base: 2 2 2 2 2 2 2 2 2 2
c ---[2019]---> Sorter-cost:  866     Base: 2 2 2 2 2 2 2 2 2 2
c ---[2017]---> Sorter-cost:  631     Base: 2 2 2 2 2 2 2 2 2 2
c ---[2015]---> Sorter-cost:  866     Base: 2 2 2 2 2 2 2 2 2 2
c ---[2013]---> Sorter-cost:  400     Base: 2 2 2 2 2 2 2 2 2 2
c ---[2011]---> Sorter-cost:  400     Base: 2 2 2 2 2 2 2 2 2 2
c ---[2009]---> Sorter-cost:  400     Base: 2 2 2 2 2 2 2 2 2 2
c ---[2007]---> Sorter-cost: 2089     Base: 2 2 2 2 2 2 2 2 2 2
c ---[2005]---> Sorter-cost: 2089     Base: 2 2 2 2 2 2 2 2 2 2
c ---[2003]---> Sorter-cost:  866     Base: 2 2 2 2 2 2 2 2 2 2
c ---[2001]---> Sorter-cost:  866     Base: 2 2 2 2 2 2 2 2 2 2
c ---[1999]---> Sorter-cost:  400     Base: 2 2 2 2 2 2 2 2 2 2
c ---[1997]---> Sorter-cost:  400     Base: 2 2 2 2 2 2 2 2 2 2
c ---[1995]---> Sorter-cost: 1322     Base: 2 2 2 2 2 2 2 2 2 2
c ---[1993]---> Sorter-cost: 1080     Base: 2 2 2 2 2 2 2 2 2 2
c ---[1991]---> Sorter-cost: 1322     Base: 2 2 2 2 2 2 2 2 2 2
c ---[1989]---> Sorter-cost:  631     Base: 2 2 2 2 2 2 2 2 2 2
c ---[1987]---> Sorter-cost:  866     Base: 2 2 2 2 2 2 2 2 2 2
c ---[1985]---> Adder-cost: 242   maxlim: 12282   bits: 15/14
c ---[1983]---> Sorter-cost: 1322     Base: 2 2 2 2 2 2 2 2 2 2
c ---[1981]---> Adder-cost: 3762   maxlim: 180136   bits: 19/18
c ---[1979]---> Adder-cost: 3498   maxlim: 176042   bits: 19/18
c ---[1977]---> Adder-cost: 242   maxlim: 12282   bits: 15/14
c ---[1975]---> Sorter-cost: 2376     Base: 2 2 2 2 2 2 2 2 2 2
c ---[1973]---> Sorter-cost:  866     Base: 2 2 2 2 2 2 2 2 2 2
c ---[1971]---> Sorter-cost:  866     Base: 2 2 2 2 2 2 2 2 2 2
c ---[1969]---> Adder-cost: 242   maxlim: 12282   bits: 15/14
c ---[1967]---> Sorter-cost: 2089     Base: 2 2 2 2 2 2 2 2 2 2
c ---[1965]---> Sorter-cost:  866     Base: 2 2 2 2 2 2 2 2 2 2
c ---[1963]---> BDD-cost:   31
c ---[1961]---> Adder-cost: 242   maxlim: 12282   bits: 15/14
c ---[1959]---> Sorter-cost: 2376     Base: 2 2 2 2 2 2 2 2 2 2
c ---[1957]---> Sorter-cost: 1322     Base: 2 2 2 2 2 2 2 2 2 2
c ---[1955]---> Sorter-cost: 1322     Base: 2 2 2 2 2 2 2 2 2 2
c ---[1953]---> Sorter-cost:  866     Base: 2 2 2 2 2 2 2 2 2 2
c ---[1951]---> Sorter-cost:  631     Base: 2 2 2 2 2 2 2 2 2 2
c ---[1949]---> Sorter-cost: 2089     Base: 2 2 2 2 2 2 2 2 2 2
c ---[1947]---> Sorter-cost: 2089     Base: 2 2 2 2 2 2 2 2 2 2
c ---[1945]---> Sorter-cost:  866     Base: 2 2 2 2 2 2 2 2 2 2
c ---[1943]---> Sorter-cost:  866     Base: 2 2 2 2 2 2 2 2 2 2
c ---[1941]---> Sorter-cost:  844     Base: 2 2 2 2 2 2 2 2 2 2
c ---[1939]---> Sorter-cost:  631     Base: 2 2 2 2 2 2 2 2 2 2
c ---[1937]---> Adder-cost: 990   maxlim: 47081   bits: 17/16
c ---[1935]---> Adder-cost: 836   maxlim: 42987   bits: 17/16
c ---[1933]---> Adder-cost: 242   maxlim: 12282   bits: 15/14
c ---[1931]---> Sorter-cost: 2376     Base: 2 2 2 2 2 2 2 2 2 2
c ---[1929]---> Sorter-cost: 2375     Base: 2 2 2 2 2 2 2 2 2 2
c ---[1927]---> Adder-cost: 242   maxlim: 12282   bits: 15/14
c ---[1925]---> Sorter-cost:  400     Base: 2 2 2 2 2 2 2 2 2 2
c ---[1923]---> BDD-cost:   91
c ---[1921]---> Sorter-cost:  400     Base: 2 2 2 2 2 2 2 2 2 2
c ---[1919]---> BDD-cost:   91
c ---[1917]---> Adder-cost: 242   maxlim: 12282   bits: 15/14
c ---[1915]---> Adder-cost: 242   maxlim: 12282   bits: 15/14
c ---[1913]---> Sorter-cost:  866     Base: 2 2 2 2 2 2 2 2 2 2
c ---[1911]---> BDD-cost:   91
c ---[1909]---> Sorter-cost: 1322     Base: 2 2 2 2 2 2 2 2 2 2
c ---[1907]---> Sorter-cost:  865     Base: 2 2 2 2 2 2 2 2 2 2
c ---[1905]---> Sorter-cost:  400     Base: 2 2 2 2 2 2 2 2 2 2
c ---[1903]---> BDD-cost:   91
c ---[1901]---> Sorter-cost:  400     Base: 2 2 2 2 2 2 2 2 2 2
c ---[1899]---> BDD-cost:   91
c ---[1898]---> BDD-cost:   96
c ---[1897]---> BDD-cost:   95
c ---[1896]---> BDD-cost:   95
c ---[1895]---> Sorter-cost: 1157     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1894]---> Sorter-cost: 1153     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1893]---> Sorter-cost: 1153     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1892]---> Sorter-cost: 1733     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1891]---> Sorter-cost: 1729     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1890]---> Sorter-cost: 1729     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1889]---> Adder-cost: 226   maxlim: 12281   bits: 15/14
c ---[1888]---> Adder-cost: 225   maxlim: 12281   bits: 15/14
c ---[1887]---> Adder-cost: 269   maxlim: 12281   bits: 15/14
c ---[1886]---> BDD-cost:   96
c ---[1885]---> BDD-cost:   95
c ---[1884]---> BDD-cost:   95
c ---[1883]---> BDD-cost:   96
c ---[1882]---> BDD-cost:   95
c ---[1881]---> BDD-cost:   95
c ---[1880]---> Sorter-cost:  633     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1879]---> Sorter-cost:  629     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1878]---> Sorter-cost:  673     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1877]---> BDD-cost:   96
c ---[1876]---> BDD-cost:   95
c ---[1875]---> BDD-cost:   95
c ---[1874]---> BDD-cost:   94
c ---[1873]---> BDD-cost:   95
c ---[1872]---> BDD-cost:   96
c ---[1871]---> BDD-cost:   95
c ---[1870]---> BDD-cost:   95
c ---[1869]---> BDD-cost:   96
c ---[1868]---> BDD-cost:   95
c ---[1867]---> BDD-cost:   95
c ---[1866]---> Sorter-cost:  675     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1865]---> Sorter-cost:  671     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1864]---> Sorter-cost:  671     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1863]---> Sorter-cost: 1089     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1862]---> Sorter-cost: 1085     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1861]---> Sorter-cost: 1129     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1860]---> Sorter-cost:  567     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1859]---> BDD-cost:   93
c ---[1858]---> Sorter-cost:  673     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1857]---> Sorter-cost: 1777     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1856]---> Sorter-cost: 1087     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1855]---> Sorter-cost: 1817     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1854]---> BDD-cost:   96
c ---[1853]---> BDD-cost:   95
c ---[1852]---> Sorter-cost:  633     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1851]---> BDD-cost:   95
c ---[1850]---> Sorter-cost:  673     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1849]---> BDD-cost:   94
c ---[1848]---> BDD-cost:   93
c ---[1847]---> BDD-cost:   95
c ---[1846]---> Sorter-cost:  931     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1845]---> Sorter-cost:  927     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1844]---> Sorter-cost:  927     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1843]---> BDD-cost:   96
c ---[1842]---> BDD-cost:   95
c ---[1841]---> Sorter-cost:  677     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1840]---> Sorter-cost:  673     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1839]---> Sorter-cost: 1089     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1838]---> Sorter-cost:  432     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1837]---> Sorter-cost: 1129     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1836]---> Sorter-cost:  677     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1835]---> Sorter-cost:  673     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1834]---> Sorter-cost:  673     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1833]---> Sorter-cost: 1155     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1832]---> Sorter-cost: 1129     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1831]---> Sorter-cost: 1151     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1830]---> Sorter-cost: 2423     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1829]---> Adder-cost: 227   maxlim: 10234   bits: 15/14
c ---[1828]---> Adder-cost: 227   maxlim: 10234   bits: 15/14
c ---[1827]---> Adder-cost: 270   maxlim: 12281   bits: 15/14
c ---[1826]---> Adder-cost: 247   maxlim: 12281   bits: 15/14
c ---[1825]---> Adder-cost: 223   maxlim: 12281   bits: 15/14
c ---[1824]---> Adder-cost: 332   maxlim: 16375   bits: 15/14
c ---[1823]---> Adder-cost: 293   maxlim: 14328   bits: 15/14
c ---[1822]---> Adder-cost: 353   maxlim: 16375   bits: 15/14
c ---[1821]---> Adder-cost: 359   maxlim: 18422   bits: 16/15
c ---[1820]---> Adder-cost: 307   maxlim: 16375   bits: 15/14
c ---[1819]---> Adder-cost: 336   maxlim: 18422   bits: 16/15
c ---[1818]---> Adder-cost: 379   maxlim: 20469   bits: 16/15
c ---[1817]---> Adder-cost: 358   maxlim: 18422   bits: 16/15
c ---[1816]---> Adder-cost: 400   maxlim: 20469   bits: 16/15
c ---[1815]---> Adder-cost: 421   maxlim: 24563   bits: 16/15
c ---[1814]---> Adder-cost: 424   maxlim: 22516   bits: 16/15
c ---[1813]---> Adder-cost: 420   maxlim: 24563   bits: 16/15
c ---[1812]---> Adder-cost: 489   maxlim: 24563   bits: 16/15
c ---[1811]---> Adder-cost: 470   maxlim: 22516   bits: 16/15
c ---[1810]---> Adder-cost: 488   maxlim: 24563   bits: 16/15
c ---[1809]---> Adder-cost: 447   maxlim: 26610   bits: 16/15
c ---[1808]---> Adder-cost: 442   maxlim: 24563   bits: 16/15
c ---[1807]---> Adder-cost: 468   maxlim: 26610   bits: 16/15
c ---[1806]---> Adder-cost: 487   maxlim: 28657   bits: 16/15
c ---[1805]---> Adder-cost: 402   maxlim: 26610   bits: 16/15
c ---[1804]---> Adder-cost: 486   maxlim: 28657   bits: 16/15
c ---[1803]---> Adder-cost: 559   maxlim: 30704   bits: 16/15
c ---[1802]---> Adder-cost: 534   maxlim: 28657   bits: 16/15
c ---[1801]---> Adder-cost: 602   maxlim: 30704   bits: 16/15
c ---[1800]---> Adder-cost: 595   maxlim: 32751   bits: 16/15
c ---[1799]---> Adder-cost: 594   maxlim: 32751   bits: 16/15
c ---[1798]---> Adder-cost: 558   maxlim: 34798   bits: 17/16
c ---[1797]---> Adder-cost: 452   maxlim: 30704   bits: 16/15
c ---[1796]---> Adder-cost: 579   maxlim: 34798   bits: 17/16
c ---[1795]---> BDD-cost:   94
c ---[1794]---> BDD-cost:   93
c ---[1793]---> BDD-cost:   95
c ---[1792]---> BDD-cost:   96
c ---[1791]---> BDD-cost:   95
c ---[1790]---> BDD-cost:   95
c ---[1789]---> BDD-cost:   94
c ---[1788]---> BDD-cost:   93
c ---[1787]---> BDD-cost:   95
c ---[1786]---> BDD-cost:   96
c ---[1785]---> BDD-cost:   95
c ---[1784]---> BDD-cost:   95
c ---[1783]---> Sorter-cost:  677     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1782]---> Sorter-cost:  673     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1781]---> BDD-cost:   94
c ---[1780]---> BDD-cost:   93
c ---[1779]---> BDD-cost:   95
c ---[1778]---> BDD-cost:   95
c ---[1777]---> BDD-cost:   96
c ---[1776]---> BDD-cost:   93
c ---[1775]---> Sorter-cost:  671     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1774]---> Sorter-cost:  677     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1773]---> Sorter-cost:  673     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1772]---> Sorter-cost: 1151     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1771]---> Sorter-cost: 1133     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1770]---> Sorter-cost: 1107     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1769]---> Sorter-cost: 1817     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1768]---> Sorter-cost: 1821     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1767]---> Adder-cost: 227   maxlim: 10234   bits: 15/14
c ---[1766]---> Sorter-cost: 2401     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1765]---> Sorter-cost: 2204     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[1764]---> Adder-cost: 201   maxlim: 12281   bits: 15/14
c ---[1763]---> Adder-cost: 581   maxlim: 36845   bits: 17/16
c ---[1762]---> Adder-cost: 580   maxlim: 36845   bits: 17/16
c ---[1761]---> Adder-cost: 810   maxlim: 53221   bits: 17/16
c ---[1760]---> Adder-cost: 295   maxlim: 10234   bits: 15/14
c ---[1759]---> Adder-cost: 931   maxlim: 55269   bits: 17/16
c ---[1758]---> Adder-cost: 603   maxlim: 16375   bits: 15/14
c ---[1757]---> Adder-cost: 1100   maxlim: 75738   bits: 18/17
c ---[1756]---> Adder-cost: 1086   maxlim: 75738   bits: 18/17
c ---[1755]---> Adder-cost: 1159   maxlim: 85973   bits: 18/17
c ---[1754]---> Adder-cost: 655   maxlim: 24563   bits: 16/15
c ---[1753]---> Adder-cost: 1156   maxlim: 85973   bits: 18/17
c ---[1752]---> Adder-cost: 1785   maxlim: 102349   bits: 18/17
c ---[1751]---> Adder-cost: 869   maxlim: 34798   bits: 17/16
c ---[1750]---> Adder-cost: 1862   maxlim: 103373   bits: 18/17
c ---[1749]---> Adder-cost: 1351   maxlim: 104396   bits: 18/17
c ---[1748]---> Adder-cost: 1566   maxlim: 105420   bits: 18/17
c ---[1747]---> Adder-cost: 841   maxlim: 36845   bits: 17/16
c ---[1746]---> Adder-cost: 1257   maxlim: 118725   bits: 18/17
c ---[1745]---> Adder-cost: 1327   maxlim: 117701   bits: 18/17
c ---[1744]---> Adder-cost: 1481   maxlim: 120772   bits: 18/17
c ---[1743]---> Adder-cost: 1693   maxlim: 119748   bits: 18/17
c ---[1742]---> Adder-cost: 1501   maxlim: 122819   bits: 18/17
c ---[1741]---> Adder-cost: 1353   maxlim: 121795   bits: 18/17
c ---[1740]---> Adder-cost: 2170   maxlim: 143289   bits: 19/18
c ---[1739]---> Adder-cost: 1504   maxlim: 53221   bits: 17/16
c ---[1738]---> Adder-cost: 2348   maxlim: 143289   bits: 19/18
c ---[1737]---> Adder-cost: 1970   maxlim: 145336   bits: 19/18
c ---[1736]---> Adder-cost: 1950   maxlim: 145336   bits: 19/18
c ---[1735]---> Adder-cost: 2038   maxlim: 163759   bits: 19/18
c ---[1734]---> Adder-cost: 1196   maxlim: 67550   bits: 18/17
c ---[1733]---> Adder-cost: 2328   maxlim: 162735   bits: 19/18
c ---[1732]---> Adder-cost: 1920   maxlim: 165806   bits: 19/18
c ---[1731]---> Adder-cost: 2200   maxlim: 164782   bits: 19/18
c ---[1730]---> Adder-cost: 1893   maxlim: 75738   bits: 18/17
c ---[1729]---> Adder-cost: 2960   maxlim: 173994   bits: 19/18
c ---[1728]---> Adder-cost: 2774   maxlim: 172970   bits: 19/18
c ---[1727]---> Adder-cost: 1658   maxlim: 176041   bits: 19/18
c ---[1726]---> Adder-cost: 2376   maxlim: 175017   bits: 19/18
c ---[1725]---> BDD-cost:   96
c ---[1724]---> BDD-cost:   95
c ---[1723]---> BDD-cost:   95
c ---[1722]---> Sorter-cost:  677     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1721]---> Sorter-cost:  673     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1720]---> Sorter-cost:  673     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1719]---> Sorter-cost: 1153     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1718]---> Sorter-cost: 1149     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1717]---> Sorter-cost: 1149     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1716]---> Sorter-cost: 1821     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1715]---> Sorter-cost: 1817     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1714]---> Sorter-cost: 1817     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1713]---> Adder-cost: 204   maxlim: 12281   bits: 15/14
c ---[1712]---> Adder-cost: 225   maxlim: 12281   bits: 15/14
c ---[1711]---> Adder-cost: 269   maxlim: 12281   bits: 15/14
c ---[1710]---> Adder-cost: 248   maxlim: 14328   bits: 15/14
c ---[1709]---> Adder-cost: 247   maxlim: 14328   bits: 15/14
c ---[1708]---> Adder-cost: 247   maxlim: 14328   bits: 15/14
c ---[1707]---> BDD-cost:   94
c ---[1706]---> BDD-cost:   93
c ---[1705]---> BDD-cost:   95
c ---[1704]---> BDD-cost:   96
c ---[1703]---> BDD-cost:   95
c ---[1702]---> BDD-cost:   95
c ---[1701]---> BDD-cost:   96
c ---[1700]---> BDD-cost:   95
c ---[1699]---> BDD-cost:   95
c ---[1698]---> BDD-cost:   96
c ---[1697]---> BDD-cost:   95
c ---[1696]---> BDD-cost:   95
c ---[1695]---> Sorter-cost:  677     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1694]---> Sorter-cost:  673     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1693]---> Sorter-cost:  673     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1692]---> Sorter-cost: 1089     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1691]---> Sorter-cost: 1085     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1690]---> Sorter-cost: 1129     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1689]---> BDD-cost:   96
c ---[1688]---> BDD-cost:   95
c ---[1687]---> BDD-cost:   95
c ---[1686]---> Sorter-cost:  653     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1685]---> Sorter-cost:  649     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1684]---> Sorter-cost:  671     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1683]---> Sorter-cost: 1110     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1682]---> Sorter-cost: 1106     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1681]---> Sorter-cost: 1106     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1680]---> Sorter-cost: 1733     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1679]---> Sorter-cost: 1729     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1678]---> Sorter-cost: 1729     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1677]---> BDD-cost:   96
c ---[1676]---> BDD-cost:   95
c ---[1675]---> BDD-cost:   95
c ---[1674]---> Sorter-cost:  675     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1673]---> Sorter-cost:  649     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1672]---> Sorter-cost:  671     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1671]---> BDD-cost:   94
c ---[1670]---> BDD-cost:   95
c ---[1669]---> Sorter-cost:  655     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1668]---> BDD-cost:   95
c ---[1667]---> Sorter-cost:  671     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1666]---> BDD-cost:   96
c ---[1665]---> BDD-cost:   95
c ---[1664]---> BDD-cost:   95
c ---[1663]---> BDD-cost:   94
c ---[1662]---> BDD-cost:   93
c ---[1661]---> BDD-cost:   95
c ---[1660]---> Sorter-cost:  655     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1659]---> Sorter-cost:  651     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1658]---> Sorter-cost:  671     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1657]---> BDD-cost:   96
c ---[1656]---> BDD-cost:   95
c ---[1655]---> BDD-cost:   95
c ---[1654]---> BDD-cost:   96
c ---[1653]---> BDD-cost:   95
c ---[1652]---> Sorter-cost:  675     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1651]---> Sorter-cost:  671     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1650]---> Sorter-cost: 1133     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1649]---> Sorter-cost:  409     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1648]---> Sorter-cost: 1129     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1647]---> Sorter-cost: 2511     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1646]---> Sorter-cost: 1039     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1645]---> Adder-cost: 227   maxlim: 10234   bits: 15/14
c ---[1644]---> BDD-cost:   94
c ---[1643]---> BDD-cost:   93
c ---[1642]---> BDD-cost:   95
c ---[1641]---> BDD-cost:   96
c ---[1640]---> BDD-cost:   95
c ---[1639]---> Sorter-cost:  675     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1638]---> BDD-cost:   93
c ---[1637]---> Sorter-cost:  671     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1636]---> BDD-cost:   93
c ---[1635]---> BDD-cost:   95
c ---[1634]---> BDD-cost:   96
c ---[1633]---> BDD-cost:   95
c ---[1632]---> Sorter-cost:  633     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1631]---> BDD-cost:   95
c ---[1630]---> Sorter-cost:  673     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1629]---> Sorter-cost:  673     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1628]---> BDD-cost:   94
c ---[1627]---> BDD-cost:   93
c ---[1626]---> Sorter-cost: 1107     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1625]---> Sorter-cost:  655     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1624]---> Sorter-cost:  651     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1623]---> Sorter-cost: 1729     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1622]---> Sorter-cost: 1089     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1621]---> Sorter-cost: 1085     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1620]---> Adder-cost: 227   maxlim: 10234   bits: 15/14
c ---[1619]---> BDD-cost:   94
c ---[1618]---> BDD-cost:   93
c ---[1617]---> BDD-cost:   95
c ---[1616]---> BDD-cost:   96
c ---[1615]---> BDD-cost:   95
c ---[1614]---> BDD-cost:   95
c ---[1613]---> BDD-cost:   94
c ---[1612]---> BDD-cost:   93
c ---[1611]---> BDD-cost:   95
c ---[1610]---> BDD-cost:   96
c ---[1609]---> BDD-cost:   95
c ---[1608]---> BDD-cost:   96
c ---[1607]---> BDD-cost:   95
c ---[1606]---> BDD-cost:   95
c ---[1605]---> Sorter-cost:  673     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1604]---> Sorter-cost:  673     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1603]---> Sorter-cost:  932     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1602]---> Sorter-cost: 1129     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1601]---> Sorter-cost: 1129     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1600]---> Sorter-cost: 1348     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1599]---> Sorter-cost: 1817     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1598]---> Sorter-cost: 1817     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1597]---> Sorter-cost: 2166     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1596]---> Adder-cost: 227   maxlim: 10234   bits: 15/14
c ---[1595]---> Adder-cost: 227   maxlim: 10234   bits: 15/14
c ---[1594]---> Adder-cost: 248   maxlim: 12281   bits: 15/14
c ---[1593]---> Adder-cost: 247   maxlim: 12281   bits: 15/14
c ---[1592]---> Adder-cost: 247   maxlim: 12281   bits: 15/14
c ---[1591]---> Adder-cost: 271   maxlim: 14328   bits: 15/14
c ---[1590]---> Adder-cost: 271   maxlim: 14328   bits: 15/14
c ---[1589]---> Adder-cost: 252   maxlim: 16375   bits: 15/14
c ---[1588]---> Adder-cost: 285   maxlim: 16375   bits: 15/14
c ---[1587]---> Adder-cost: 285   maxlim: 16375   bits: 15/14
c ---[1586]---> Adder-cost: 401   maxlim: 20469   bits: 16/15
c ---[1585]---> Adder-cost: 360   maxlim: 20469   bits: 16/15
c ---[1584]---> Adder-cost: 400   maxlim: 20469   bits: 16/15
c ---[1583]---> Adder-cost: 443   maxlim: 24563   bits: 16/15
c ---[1582]---> Adder-cost: 464   maxlim: 24563   bits: 16/15
c ---[1581]---> Adder-cost: 491   maxlim: 26610   bits: 16/15
c ---[1580]---> Adder-cost: 512   maxlim: 26610   bits: 16/15
c ---[1579]---> Adder-cost: 401   maxlim: 28657   bits: 16/15
c ---[1578]---> Adder-cost: 430   maxlim: 28657   bits: 16/15
c ---[1577]---> Adder-cost: 577   maxlim: 30704   bits: 16/15
c ---[1576]---> Adder-cost: 512   maxlim: 30704   bits: 16/15
c ---[1575]---> Adder-cost: 554   maxlim: 30704   bits: 16/15
c ---[1574]---> Adder-cost: 538   maxlim: 34798   bits: 17/16
c ---[1573]---> Adder-cost: 506   maxlim: 34798   bits: 17/16
c ---[1572]---> Adder-cost: 537   maxlim: 34798   bits: 17/16
c ---[1571]---> Adder-cost: 576   maxlim: 36845   bits: 17/16
c ---[1570]---> Adder-cost: 625   maxlim: 38892   bits: 17/16
c ---[1569]---> Adder-cost: 709   maxlim: 38892   bits: 17/16
c ---[1568]---> Adder-cost: 596   maxlim: 40939   bits: 17/16
c ---[1567]---> Adder-cost: 663   maxlim: 40939   bits: 17/16
c ---[1566]---> Adder-cost: 741   maxlim: 40939   bits: 17/16
c ---[1565]---> Adder-cost: 700   maxlim: 42986   bits: 17/16
c ---[1564]---> Adder-cost: 621   maxlim: 42986   bits: 17/16
c ---[1563]---> Adder-cost: 681   maxlim: 42986   bits: 17/16
c ---[1562]---> Adder-cost: 619   maxlim: 47080   bits: 17/16
c ---[1561]---> Adder-cost: 773   maxlim: 47080   bits: 17/16
c ---[1560]---> Adder-cost: 782   maxlim: 51174   bits: 17/16
c ---[1559]---> Adder-cost: 727   maxlim: 51174   bits: 17/16
c ---[1558]---> Adder-cost: 843   maxlim: 51174   bits: 17/16
c ---[1557]---> Adder-cost: 888   maxlim: 53221   bits: 17/16
c ---[1556]---> Adder-cost: 739   maxlim: 53221   bits: 17/16
c ---[1555]---> Adder-cost: 1045   maxlim: 53221   bits: 17/16
c ---[1554]---> Adder-cost: 1016   maxlim: 55268   bits: 17/16
c ---[1553]---> Adder-cost: 795   maxlim: 55268   bits: 17/16
c ---[1552]---> Adder-cost: 915   maxlim: 55268   bits: 17/16
c ---[1551]---> Adder-cost: 936   maxlim: 57315   bits: 17/16
c ---[1550]---> Adder-cost: 759   maxlim: 57315   bits: 17/16
c ---[1549]---> Adder-cost: 873   maxlim: 57315   bits: 17/16
c ---[1548]---> Adder-cost: 872   maxlim: 59362   bits: 17/16
c ---[1547]---> Adder-cost: 657   maxlim: 59362   bits: 17/16
c ---[1546]---> Adder-cost: 815   maxlim: 59362   bits: 17/16
c ---[1545]---> Adder-cost: 1094   maxlim: 61409   bits: 17/16
c ---[1544]---> Adder-cost: 1093   maxlim: 61409   bits: 17/16
c ---[1543]---> BDD-cost:   96
c ---[1542]---> BDD-cost:   95
c ---[1541]---> BDD-cost:   95
c ---[1540]---> Sorter-cost:  655     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1539]---> Sorter-cost:  651     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1538]---> Sorter-cost:  673     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1537]---> BDD-cost:   96
c ---[1536]---> BDD-cost:   95
c ---[1535]---> Sorter-cost: 1157     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1534]---> Sorter-cost:  673     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1533]---> Sorter-cost: 1153     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1532]---> Sorter-cost: 1843     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1531]---> Sorter-cost: 1129     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1530]---> Sorter-cost: 1839     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1529]---> Sorter-cost: 2489     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1528]---> Sorter-cost: 1839     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1527]---> Adder-cost: 227   maxlim: 10234   bits: 15/14
c ---[1526]---> Adder-cost: 316   maxlim: 14328   bits: 15/14
c ---[1525]---> Adder-cost: 269   maxlim: 12281   bits: 15/14
c ---[1524]---> Adder-cost: 293   maxlim: 14328   bits: 15/14
c ---[1523]---> Adder-cost: 286   maxlim: 16375   bits: 15/14
c ---[1522]---> Adder-cost: 249   maxlim: 14328   bits: 15/14
c ---[1521]---> Adder-cost: 309   maxlim: 16375   bits: 15/14
c ---[1520]---> Adder-cost: 293   maxlim: 18422   bits: 16/15
c ---[1519]---> Adder-cost: 259   maxlim: 16375   bits: 15/14
c ---[1518]---> Adder-cost: 314   maxlim: 18422   bits: 16/15
c ---[1517]---> Adder-cost: 361   maxlim: 20469   bits: 16/15
c ---[1516]---> Adder-cost: 338   maxlim: 18422   bits: 16/15
c ---[1515]---> Adder-cost: 360   maxlim: 20469   bits: 16/15
c ---[1514]---> Adder-cost: 421   maxlim: 24563   bits: 16/15
c ---[1513]---> Adder-cost: 358   maxlim: 22516   bits: 16/15
c ---[1512]---> Adder-cost: 442   maxlim: 24563   bits: 16/15
c ---[1511]---> Adder-cost: 469   maxlim: 26610   bits: 16/15
c ---[1510]---> Adder-cost: 420   maxlim: 24563   bits: 16/15
c ---[1509]---> Adder-cost: 446   maxlim: 26610   bits: 16/15
c ---[1508]---> Adder-cost: 435   maxlim: 28657   bits: 16/15
c ---[1507]---> Adder-cost: 418   maxlim: 26610   bits: 16/15
c ---[1506]---> Adder-cost: 434   maxlim: 28657   bits: 16/15
c ---[1505]---> Adder-cost: 461   maxlim: 30704   bits: 16/15
c ---[1504]---> Adder-cost: 422   maxlim: 28657   bits: 16/15
c ---[1503]---> Adder-cost: 456   maxlim: 30704   bits: 16/15
c ---[1502]---> Adder-cost: 488   maxlim: 32751   bits: 16/15
c ---[1501]---> Adder-cost: 496   maxlim: 30704   bits: 16/15
c ---[1500]---> Adder-cost: 527   maxlim: 32751   bits: 16/15
c ---[1499]---> BDD-cost:   96
c ---[1498]---> BDD-cost:   95
c ---[1497]---> BDD-cost:   95
c ---[1496]---> Sorter-cost:  675     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1495]---> Sorter-cost:  671     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1494]---> Sorter-cost:  671     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1493]---> Sorter-cost: 1023     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1492]---> Sorter-cost: 1019     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1491]---> Sorter-cost: 1129     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1490]---> BDD-cost:   94
c ---[1489]---> BDD-cost:   93
c ---[1488]---> BDD-cost:   95
c ---[1487]---> Sorter-cost:  655     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1486]---> Sorter-cost:  651     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1485]---> Sorter-cost:  671     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1484]---> BDD-cost:   96
c ---[1483]---> BDD-cost:   95
c ---[1482]---> BDD-cost:   95
c ---[1481]---> Sorter-cost:  653     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1480]---> Sorter-cost:  649     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1479]---> Sorter-cost:  671     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1478]---> Sorter-cost: 1089     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1477]---> Sorter-cost: 1085     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1476]---> Sorter-cost: 1107     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1475]---> BDD-cost:   94
c ---[1474]---> BDD-cost:   93
c ---[1473]---> BDD-cost:   95
c ---[1472]---> Sorter-cost:  655     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1471]---> Sorter-cost:  651     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1470]---> Sorter-cost:  671     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1469]---> Sorter-cost: 1133     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1468]---> Sorter-cost: 1129     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1467]---> Sorter-cost: 1129     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1466]---> BDD-cost:   96
c ---[1465]---> BDD-cost:   95
c ---[1464]---> BDD-cost:   95
c ---[1463]---> Sorter-cost:  655     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1462]---> Sorter-cost:  651     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1461]---> Sorter-cost:  673     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1460]---> BDD-cost:   94
c ---[1459]---> BDD-cost:   93
c ---[1458]---> BDD-cost:   95
c ---[1457]---> Sorter-cost:  655     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1456]---> Sorter-cost:  431     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1455]---> Sorter-cost:  673     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1454]---> BDD-cost:   94
c ---[1453]---> BDD-cost:   95
c ---[1452]---> Sorter-cost:  655     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1451]---> BDD-cost:   95
c ---[1450]---> Sorter-cost:  671     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1449]---> BDD-cost:   94
c ---[1448]---> BDD-cost:   93
c ---[1447]---> BDD-cost:   95
c ---[1446]---> BDD-cost:   96
c ---[1445]---> BDD-cost:   95
c ---[1444]---> BDD-cost:   95
c ---[1443]---> Sorter-cost:  677     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1442]---> Sorter-cost:  673     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1441]---> Sorter-cost:  673     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1440]---> Sorter-cost: 1133     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1439]---> Sorter-cost: 1129     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1438]---> Sorter-cost: 1129     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1437]---> Sorter-cost: 1711     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1436]---> Sorter-cost: 1707     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1435]---> Sorter-cost: 1839     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1434]---> BDD-cost:   96
c ---[1433]---> BDD-cost:   95
c ---[1432]---> BDD-cost:   95
c ---[1431]---> Sorter-cost:  655     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1430]---> Sorter-cost:  651     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1429]---> Sorter-cost:  673     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1428]---> BDD-cost:   94
c ---[1427]---> BDD-cost:   93
c ---[1426]---> BDD-cost:   95
c ---[1425]---> BDD-cost:   96
c ---[1424]---> BDD-cost:   95
c ---[1423]---> Sorter-cost:  655     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1422]---> Sorter-cost:  673     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1421]---> Sorter-cost: 1089     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1420]---> Sorter-cost: 1129     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1419]---> Sorter-cost:  673     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1418]---> Sorter-cost:  673     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1417]---> BDD-cost:   96
c ---[1416]---> Sorter-cost: 1085     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1415]---> Sorter-cost: 1151     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1414]---> BDD-cost:   95
c ---[1413]---> BDD-cost:   95
c ---[1412]---> BDD-cost:   94
c ---[1411]---> Sorter-cost:  651     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1410]---> Sorter-cost:  673     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1409]---> Sorter-cost:  677     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1408]---> Sorter-cost:  673     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1407]---> Sorter-cost: 1133     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1406]---> Sorter-cost:  630     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1405]---> Sorter-cost: 1129     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1404]---> Sorter-cost: 1799     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1403]---> Sorter-cost: 1017     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1402]---> Sorter-cost: 1795     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1401]---> Sorter-cost: 2485     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1400]---> Adder-cost: 227   maxlim: 10234   bits: 15/14
c ---[1399]---> Adder-cost: 252   maxlim: 18422   bits: 16/15
c ---[1398]---> Adder-cost: 269   maxlim: 20469   bits: 16/15
c ---[1397]---> Adder-cost: 274   maxlim: 20469   bits: 16/15
c ---[1396]---> BDD-cost:   95
c ---[1395]---> Adder-cost: 293   maxlim: 22516   bits: 16/15
c ---[1394]---> Adder-cost: 318   maxlim: 22516   bits: 16/15
c ---[1393]---> Sorter-cost:  673     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1392]---> Adder-cost: 331   maxlim: 24563   bits: 16/15
c ---[1391]---> Adder-cost: 533   maxlim: 24563   bits: 16/15
c ---[1390]---> Adder-cost: 294   maxlim: 6140   bits: 14/13
c ---[1389]---> Adder-cost: 560   maxlim: 26610   bits: 16/15
c ---[1388]---> Adder-cost: 539   maxlim: 28657   bits: 16/15
c ---[1387]---> Adder-cost: 353   maxlim: 10234   bits: 15/14
c ---[1386]---> Adder-cost: 578   maxlim: 30704   bits: 16/15
c ---[1385]---> Adder-cost: 716   maxlim: 38892   bits: 17/16
c ---[1384]---> Adder-cost: 492   maxlim: 20469   bits: 16/15
c ---[1383]---> Adder-cost: 757   maxlim: 40939   bits: 17/16
c ---[1382]---> Adder-cost: 848   maxlim: 53221   bits: 17/16
c ---[1381]---> Adder-cost: 626   maxlim: 32751   bits: 16/15
c ---[1380]---> Adder-cost: 823   maxlim: 55268   bits: 17/16
c ---[1379]---> Adder-cost: 776   maxlim: 55268   bits: 17/16
c ---[1378]---> Adder-cost: 550   maxlim: 34798   bits: 17/16
c ---[1377]---> Adder-cost: 775   maxlim: 59363   bits: 17/16
c ---[1376]---> Adder-cost: 972   maxlim: 57315   bits: 17/16
c ---[1375]---> Adder-cost: 799   maxlim: 36845   bits: 17/16
c ---[1374]---> Adder-cost: 1045   maxlim: 61410   bits: 17/16
c ---[1373]---> Adder-cost: 1130   maxlim: 71644   bits: 18/17
c ---[1372]---> Adder-cost: 1043   maxlim: 53221   bits: 17/16
c ---[1371]---> Adder-cost: 1156   maxlim: 75739   bits: 18/17
c ---[1370]---> Adder-cost: 1116   maxlim: 73691   bits: 18/17
c ---[1369]---> Adder-cost: 975   maxlim: 55268   bits: 17/16
c ---[1368]---> Adder-cost: 1164   maxlim: 77786   bits: 18/17
c ---[1367]---> Adder-cost: 1024   maxlim: 75738   bits: 18/17
c ---[1366]---> Adder-cost: 925   maxlim: 57315   bits: 17/16
c ---[1365]---> Adder-cost: 1174   maxlim: 79833   bits: 18/17
c ---[1364]---> Adder-cost: 1047   maxlim: 77785   bits: 18/17
c ---[1363]---> Adder-cost: 913   maxlim: 59362   bits: 17/16
c ---[1362]---> Adder-cost: 1076   maxlim: 81880   bits: 18/17
c ---[1361]---> Adder-cost: 1025   maxlim: 79832   bits: 18/17
c ---[1360]---> Adder-cost: 821   maxlim: 61409   bits: 17/16
c ---[1359]---> Adder-cost: 974   maxlim: 83927   bits: 18/17
c ---[1358]---> Adder-cost: 923   maxlim: 79832   bits: 18/17
c ---[1357]---> Adder-cost: 1093   maxlim: 63456   bits: 17/16
c ---[1356]---> Adder-cost: 938   maxlim: 83927   bits: 18/17
c ---[1355]---> Adder-cost: 1265   maxlim: 88020   bits: 18/17
c ---[1354]---> Adder-cost: 1032   maxlim: 71644   bits: 18/17
c ---[1353]---> Adder-cost: 1292   maxlim: 92115   bits: 18/17
c ---[1352]---> Adder-cost: 1377   maxlim: 94161   bits: 18/17
c ---[1351]---> Adder-cost: 1218   maxlim: 77785   bits: 18/17
c ---[1350]---> Adder-cost: 1408   maxlim: 97232   bits: 18/17
c ---[1349]---> Adder-cost: 1287   maxlim: 96208   bits: 18/17
c ---[1348]---> Adder-cost: 1184   maxlim: 79832   bits: 18/17
c ---[1347]---> Adder-cost: 1276   maxlim: 99279   bits: 18/17
c ---[1346]---> Adder-cost: 1495   maxlim: 102349   bits: 18/17
c ---[1345]---> Adder-cost: 1328   maxlim: 85973   bits: 18/17
c ---[1344]---> Adder-cost: 1558   maxlim: 105420   bits: 18/17
c ---[1343]---> Adder-cost: 1417   maxlim: 104396   bits: 18/17
c ---[1342]---> Adder-cost: 1282   maxlim: 88020   bits: 18/17
c ---[1341]---> Adder-cost: 1410   maxlim: 107467   bits: 18/17
c ---[1340]---> Adder-cost: 1677   maxlim: 106443   bits: 18/17
c ---[1339]---> Adder-cost: 1492   maxlim: 90067   bits: 18/17
c ---[1338]---> Adder-cost: 1697   maxlim: 109514   bits: 18/17
c ---[1337]---> Adder-cost: 943   maxlim: 106443   bits: 18/17
c ---[1336]---> Adder-cost: 888   maxlim: 90067   bits: 18/17
c ---[1335]---> Adder-cost: 965   maxlim: 109514   bits: 18/17
c ---[1334]---> Adder-cost: 1563   maxlim: 114631   bits: 18/17
c ---[1333]---> Adder-cost: 1460   maxlim: 98255   bits: 18/17
c ---[1332]---> Adder-cost: 1599   maxlim: 117702   bits: 18/17
c ---[1331]---> Adder-cost: 1741   maxlim: 114631   bits: 18/17
c ---[1330]---> Adder-cost: 1821   maxlim: 117702   bits: 18/17
c ---[1329]---> Adder-cost: 1505   maxlim: 118725   bits: 18/17
c ---[1328]---> Adder-cost: 1354   maxlim: 100302   bits: 18/17
c ---[1327]---> Adder-cost: 1573   maxlim: 123843   bits: 18/17
c ---[1326]---> Adder-cost: 1601   maxlim: 120772   bits: 18/17
c ---[1325]---> Adder-cost: 1591   maxlim: 102349   bits: 18/17
c ---[1324]---> Adder-cost: 1737   maxlim: 125890   bits: 18/17
c ---[1323]---> Adder-cost: 1763   maxlim: 120772   bits: 18/17
c ---[1322]---> Adder-cost: 1661   maxlim: 102349   bits: 18/17
c ---[1321]---> Adder-cost: 1807   maxlim: 125890   bits: 18/17
c ---[1320]---> Adder-cost: 1675   maxlim: 126913   bits: 18/17
c ---[1319]---> Adder-cost: 1775   maxlim: 108490   bits: 18/17
c ---[1318]---> Adder-cost: 1990   maxlim: 132031   bits: 19/18
c ---[1317]---> Adder-cost: 1814   maxlim: 136125   bits: 19/18
c ---[1316]---> Adder-cost: 1756   maxlim: 133054   bits: 19/18
c ---[1315]---> Adder-cost: 1637   maxlim: 114631   bits: 18/17
c ---[1314]---> Adder-cost: 1664   maxlim: 139196   bits: 19/18
c ---[1313]---> Adder-cost: 1800   maxlim: 137148   bits: 19/18
c ---[1312]---> Adder-cost: 1511   maxlim: 118725   bits: 18/17
c ---[1311]---> Adder-cost: 1682   maxlim: 141242   bits: 19/18
c ---[1310]---> Adder-cost: 1834   maxlim: 139195   bits: 19/18
c ---[1309]---> Adder-cost: 1785   maxlim: 120772   bits: 18/17
c ---[1308]---> Adder-cost: 2074   maxlim: 143289   bits: 19/18
c ---[1307]---> Adder-cost: 2158   maxlim: 145336   bits: 19/18
c ---[1306]---> Adder-cost: 1941   maxlim: 126913   bits: 18/17
c ---[1305]---> Adder-cost: 2222   maxlim: 149430   bits: 19/18
c ---[1304]---> Adder-cost: 2070   maxlim: 147383   bits: 19/18
c ---[1303]---> Adder-cost: 2070   maxlim: 153524   bits: 19/18
c ---[1302]---> Adder-cost: 2010   maxlim: 135101   bits: 19/18
c ---[1301]---> Adder-cost: 2224   maxlim: 157618   bits: 19/18
c ---[1300]---> Adder-cost: 1700   maxlim: 139195   bits: 19/18
c ---[1299]---> Adder-cost: 2244   maxlim: 161712   bits: 19/18
c ---[1298]---> Adder-cost: 2020   maxlim: 157618   bits: 19/18
c ---[1297]---> Adder-cost: 994   maxlim: 139195   bits: 19/18
c ---[1296]---> Adder-cost: 1012   maxlim: 161712   bits: 19/18
c ---[1295]---> Adder-cost: 2058   maxlim: 159665   bits: 19/18
c ---[1294]---> Adder-cost: 1988   maxlim: 141242   bits: 19/18
c ---[1293]---> Adder-cost: 2272   maxlim: 163759   bits: 19/18
c ---[1292]---> Adder-cost: 2390   maxlim: 159665   bits: 19/18
c ---[1291]---> Adder-cost: 2300   maxlim: 141242   bits: 19/18
c ---[1290]---> Adder-cost: 2492   maxlim: 163759   bits: 19/18
c ---[1289]---> Adder-cost: 2376   maxlim: 171947   bits: 19/18
c ---[1288]---> Adder-cost: 2196   maxlim: 153524   bits: 19/18
c ---[1287]---> Adder-cost: 2532   maxlim: 176041   bits: 19/18
c ---[1286]---> Adder-cost: 2268   maxlim: 178088   bits: 19/18
c ---[1285]---> Adder-cost: 2154   maxlim: 157618   bits: 19/18
c ---[1284]---> Adder-cost: 2886   maxlim: 182182   bits: 19/18
c ---[1283]---> BDD-cost:   96
c ---[1282]---> BDD-cost:   95
c ---[1281]---> BDD-cost:   95
c ---[1280]---> Sorter-cost:  677     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1279]---> Sorter-cost:  673     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1278]---> Sorter-cost:  673     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1277]---> Sorter-cost: 1153     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1276]---> Sorter-cost: 1127     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1275]---> Sorter-cost: 1149     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1274]---> Sorter-cost: 2208     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1273]---> Sorter-cost: 1729     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1272]---> Adder-cost: 205   maxlim: 8187   bits: 14/13
c ---[1271]---> BDD-cost:   94
c ---[1270]---> BDD-cost:   93
c ---[1269]---> BDD-cost:   95
c ---[1268]---> Sorter-cost:  633     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1267]---> Sorter-cost:  629     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1266]---> Sorter-cost:  671     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1265]---> BDD-cost:   96
c ---[1264]---> BDD-cost:   95
c ---[1263]---> Sorter-cost:  432     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1262]---> Sorter-cost: 1157     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1261]---> Sorter-cost: 1153     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1260]---> BDD-cost:   96
c ---[1259]---> BDD-cost:   95
c ---[1258]---> Sorter-cost:  655     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1257]---> Sorter-cost:  673     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1256]---> BDD-cost:   96
c ---[1255]---> BDD-cost:   95
c ---[1254]---> BDD-cost:   95
c ---[1253]---> Sorter-cost:  677     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1252]---> Sorter-cost:  673     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1251]---> Sorter-cost:  673     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1250]---> Sorter-cost: 1155     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1249]---> Sorter-cost: 1129     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1248]---> Sorter-cost: 1151     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1247]---> Sorter-cost: 1843     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1246]---> Sorter-cost: 1729     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1245]---> Sorter-cost: 1839     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1244]---> Adder-cost: 160   maxlim: 10234   bits: 15/14
c ---[1243]---> Sorter-cost: 2313     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[1242]---> Adder-cost: 251   maxlim: 10234   bits: 15/14
c ---[1241]---> BDD-cost:   96
c ---[1240]---> BDD-cost:   95
c ---[1239]---> BDD-cost:   95
c ---[1238]---> Sorter-cost:  653     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1237]---> Sorter-cost:  649     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1236]---> Sorter-cost:  671     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1235]---> BDD-cost:   96
c ---[1234]---> BDD-cost:   93
c ---[1233]---> BDD-cost:   95
c ---[1232]---> BDD-cost:   96
c ---[1231]---> BDD-cost:   95
c ---[1230]---> BDD-cost:   95
c ---[1229]---> Sorter-cost:  675     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1228]---> Sorter-cost:  671     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1227]---> Sorter-cost:  671     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1226]---> Sorter-cost: 1089     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1225]---> Sorter-cost: 1085     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1224]---> Sorter-cost: 1107     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1223]---> BDD-cost:   94
c ---[1222]---> BDD-cost:   93
c ---[1221]---> BDD-cost:   95
c ---[1220]---> Sorter-cost:  655     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1219]---> Sorter-cost:  651     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1218]---> Sorter-cost:  671     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1217]---> BDD-cost:   93
c ---[1216]---> BDD-cost:   95
c ---[1215]---> Sorter-cost:  413     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1214]---> Sorter-cost:  671     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1213]---> BDD-cost:   96
c ---[1212]---> BDD-cost:   95
c ---[1211]---> Sorter-cost:  677     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1210]---> Sorter-cost:  673     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1209]---> Sorter-cost: 1133     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1208]---> Sorter-cost:  674     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1207]---> Sorter-cost: 1129     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1206]---> Sorter-cost: 1733     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1205]---> Sorter-cost: 1106     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1204]---> Sorter-cost: 1729     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1203]---> Sorter-cost: 2423     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1202]---> Sorter-cost: 1841     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1201]---> Adder-cost: 227   maxlim: 10234   bits: 15/14
c ---[1200]---> Adder-cost: 270   maxlim: 12281   bits: 15/14
c ---[1199]---> Adder-cost: 225   maxlim: 8187   bits: 14/13
c ---[1198]---> Adder-cost: 223   maxlim: 12281   bits: 15/14
c ---[1197]---> Adder-cost: 204   maxlim: 12281   bits: 15/14
c ---[1196]---> Adder-cost: 159   maxlim: 8187   bits: 14/13
c ---[1195]---> Adder-cost: 225   maxlim: 12281   bits: 15/14
c ---[1194]---> Adder-cost: 270   maxlim: 14328   bits: 15/14
c ---[1193]---> Adder-cost: 247   maxlim: 10234   bits: 15/14
c ---[1192]---> Adder-cost: 269   maxlim: 14328   bits: 15/14
c ---[1191]---> Adder-cost: 308   maxlim: 16375   bits: 15/14
c ---[1190]---> Adder-cost: 285   maxlim: 16375   bits: 15/14
c ---[1189]---> Adder-cost: 361   maxlim: 18422   bits: 16/15
c ---[1188]---> Adder-cost: 295   maxlim: 14328   bits: 15/14
c ---[1187]---> Adder-cost: 360   maxlim: 18422   bits: 16/15
c ---[1186]---> Adder-cost: 335   maxlim: 20469   bits: 16/15
c ---[1185]---> Adder-cost: 310   maxlim: 16375   bits: 15/14
c ---[1184]---> Adder-cost: 356   maxlim: 20469   bits: 16/15
c ---[1183]---> Adder-cost: 427   maxlim: 22516   bits: 16/15
c ---[1182]---> Adder-cost: 362   maxlim: 18422   bits: 16/15
c ---[1181]---> Adder-cost: 426   maxlim: 22516   bits: 16/15
c ---[1180]---> Adder-cost: 417   maxlim: 24563   bits: 16/15
c ---[1179]---> Adder-cost: 356   maxlim: 20469   bits: 16/15
c ---[1178]---> Adder-cost: 416   maxlim: 24563   bits: 16/15
c ---[1177]---> Adder-cost: 471   maxlim: 26610   bits: 16/15
c ---[1176]---> Adder-cost: 406   maxlim: 22516   bits: 16/15
c ---[1175]---> Adder-cost: 470   maxlim: 26610   bits: 16/15
c ---[1174]---> Adder-cost: 533   maxlim: 30704   bits: 16/15
c ---[1173]---> Adder-cost: 512   maxlim: 26610   bits: 16/15
c ---[1172]---> Adder-cost: 554   maxlim: 30704   bits: 16/15
c ---[1171]---> Adder-cost: 627   maxlim: 30704   bits: 16/15
c ---[1170]---> Adder-cost: 648   maxlim: 30704   bits: 16/15
c ---[1169]---> Adder-cost: 462   maxlim: 34798   bits: 17/16
c ---[1168]---> Adder-cost: 486   maxlim: 30704   bits: 16/15
c ---[1167]---> Adder-cost: 483   maxlim: 34798   bits: 17/16
c ---[1166]---> BDD-cost:   96
c ---[1165]---> BDD-cost:   95
c ---[1164]---> BDD-cost:   95
c ---[1163]---> Sorter-cost:  675     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1162]---> Sorter-cost:  671     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1161]---> Sorter-cost:  671     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1160]---> Sorter-cost: 1155     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1159]---> Sorter-cost: 1151     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1158]---> Sorter-cost: 1821     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1157]---> Sorter-cost: 1366     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1156]---> Sorter-cost: 1817     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1155]---> BDD-cost:   96
c ---[1154]---> BDD-cost:   95
c ---[1153]---> BDD-cost:   95
c ---[1152]---> Sorter-cost:  675     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1151]---> Sorter-cost:  671     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1150]---> Sorter-cost:  671     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1149]---> Sorter-cost: 1821     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1148]---> Sorter-cost: 1861     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1147]---> Sorter-cost: 1861     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1146]---> Adder-cost: 183   maxlim: 10234   bits: 15/14
c ---[1145]---> Adder-cost: 227   maxlim: 10234   bits: 15/14
c ---[1144]---> BDD-cost:   96
c ---[1143]---> BDD-cost:   95
c ---[1142]---> BDD-cost:   94
c ---[1141]---> BDD-cost:   93
c ---[1140]---> BDD-cost:   95
c ---[1139]---> BDD-cost:   96
c ---[1138]---> BDD-cost:   95
c ---[1137]---> BDD-cost:   95
c ---[1136]---> Sorter-cost:  675     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1135]---> Sorter-cost:  671     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1134]---> Sorter-cost:  671     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1133]---> Sorter-cost: 1821     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1132]---> Sorter-cost: 1817     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1131]---> Sorter-cost: 1817     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1130]---> BDD-cost:   96
c ---[1129]---> BDD-cost:   95
c ---[1128]---> Sorter-cost:  655     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1127]---> Sorter-cost:  673     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1126]---> BDD-cost:   96
c ---[1125]---> BDD-cost:   95
c ---[1124]---> BDD-cost:   95
c ---[1123]---> Sorter-cost: 1047     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1122]---> Sorter-cost:  818     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1121]---> Sorter-cost: 1153     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1120]---> BDD-cost:   96
c ---[1119]---> BDD-cost:   95
c ---[1118]---> BDD-cost:   95
c ---[1117]---> BDD-cost:   94
c ---[1116]---> BDD-cost:   95
c ---[1114]---> BDD-cost:   50
c ---[1112]---> BDD-cost:   50
c ---[1110]---> BDD-cost:   50
c ---[1108]---> BDD-cost:   50
c ---[1106]---> Sorter-cost:  237     Base: 2 2 2 2 2 2 2 2 2 2
c ---[1104]---> Sorter-cost:  237     Base: 2 2 2 2 2 2 2 2 2 2
c ---[1102]---> Sorter-cost:  237     Base: 2 2 2 2 2 2 2 2 2 2
c ---[1100]---> Sorter-cost:  237     Base: 2 2 2 2 2 2 2 2 2 2
c ---[1098]---> Sorter-cost:  237     Base: 2 2 2 2 2 2 2 2 2 2
c ---[1096]---> Sorter-cost:  237     Base: 2 2 2 2 2 2 2 2 2 2
c ---[1094]---> Sorter-cost:  237     Base: 2 2 2 2 2 2 2 2 2 2
c ---[1092]---> Sorter-cost:  237     Base: 2 2 2 2 2 2 2 2 2 2
c ---[1090]---> Sorter-cost:  237     Base: 2 2 2 2 2 2 2 2 2 2
c ---[1088]---> Sorter-cost:  237     Base: 2 2 2 2 2 2 2 2 2 2
c ---[1086]---> Sorter-cost:  237     Base: 2 2 2 2 2 2 2 2 2 2
c ---[1084]---> Sorter-cost:  237     Base: 2 2 2 2 2 2 2 2 2 2
c ---[1082]---> Sorter-cost:  237     Base: 2 2 2 2 2 2 2 2 2 2
c ---[1080]---> Sorter-cost:  237     Base: 2 2 2 2 2 2 2 2 2 2
c ---[1078]---> Sorter-cost:  237     Base: 2 2 2 2 2 2 2 2 2 2
c ---[1076]---> Sorter-cost:  237     Base: 2 2 2 2 2 2 2 2 2 2
c ---[1074]---> Sorter-cost:  237     Base: 2 2 2 2 2 2 2 2 2 2
c ---[1072]---> Sorter-cost:  237     Base: 2 2 2 2 2 2 2 2 2 2
c ---[1070]---> Sorter-cost:  237     Base: 2 2 2 2 2 2 2 2 2 2
c ---[1068]---> Sorter-cost:  237     Base: 2 2 2 2 2 2 2 2 2 2
c ---[1066]---> Sorter-cost:  237     Base: 2 2 2 2 2 2 2 2 2 2
c ---[1064]---> Sorter-cost:  237     Base: 2 2 2 2 2 2 2 2 2 2
c ---[1062]---> Sorter-cost:  237     Base: 2 2 2 2 2 2 2 2 2 2
c ---[1060]---> Sorter-cost:  237     Base: 2 2 2 2 2 2 2 2 2 2
c ---[1058]---> Sorter-cost:  237     Base: 2 2 2 2 2 2 2 2 2 2
c ---[1056]---> Sorter-cost:  237     Base: 2 2 2 2 2 2 2 2 2 2
c ---[1054]---> BDD-cost:   50
c ---[1052]---> Sorter-cost:  237     Base: 2 2 2 2 2 2 2 2 2 2
c ---[1050]---> Sorter-cost:  237     Base: 2 2 2 2 2 2 2 2 2 2
c ---[1048]---> Sorter-cost:  237     Base: 2 2 2 2 2 2 2 2 2 2
c ---[1046]---> Sorter-cost:  237     Base: 2 2 2 2 2 2 2 2 2 2
c ---[1044]---> Sorter-cost:  237     Base: 2 2 2 2 2 2 2 2 2 2
c ---[1042]---> Sorter-cost:  237     Base: 2 2 2 2 2 2 2 2 2 2
c ---[1040]---> Sorter-cost:  237     Base: 2 2 2 2 2 2 2 2 2 2
c ---[1038]---> Sorter-cost:  237     Base: 2 2 2 2 2 2 2 2 2 2
c ---[1036]---> Sorter-cost:  237     Base: 2 2 2 2 2 2 2 2 2 2
c ---[1034]---> Sorter-cost:  237     Base: 2 2 2 2 2 2 2 2 2 2
c ---[1032]---> Sorter-cost:  237     Base: 2 2 2 2 2 2 2 2 2 2
c ---[1030]---> Sorter-cost:  237     Base: 2 2 2 2 2 2 2 2 2 2
c ---[1028]---> Sorter-cost:  237     Base: 2 2 2 2 2 2 2 2 2 2
c ---[1026]---> Sorter-cost:  237     Base: 2 2 2 2 2 2 2 2 2 2
c ---[1024]---> Sorter-cost:  237     Base: 2 2 2 2 2 2 2 2 2 2
c ---[1022]---> Sorter-cost:  237     Base: 2 2 2 2 2 2 2 2 2 2
c ---[1020]---> Sorter-cost:  237     Base: 2 2 2 2 2 2 2 2 2 2
c ---[1018]---> Sorter-cost:  237     Base: 2 2 2 2 2 2 2 2 2 2
c ---[1016]---> Sorter-cost:  237     Base: 2 2 2 2 2 2 2 2 2 2
c ---[1014]---> Sorter-cost:  237     Base: 2 2 2 2 2 2 2 2 2 2
c ---[1012]---> BDD-cost:   50
c ---[1010]---> Sorter-cost:  237     Base: 2 2 2 2 2 2 2 2 2 2
c ---[1008]---> Sorter-cost:  237     Base: 2 2 2 2 2 2 2 2 2 2
c ---[1006]---> Sorter-cost:  237     Base: 2 2 2 2 2 2 2 2 2 2
c ---[1004]---> Sorter-cost:  237     Base: 2 2 2 2 2 2 2 2 2 2
c ---[1002]---> Sorter-cost:  237     Base: 2 2 2 2 2 2 2 2 2 2
c ---[1000]---> Sorter-cost:  237     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 998]---> Sorter-cost:  237     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 996]---> Sorter-cost:  237     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 994]---> Sorter-cost:  237     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 992]---> BDD-cost:   50
c ---[ 990]---> Sorter-cost:  237     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 988]---> BDD-cost:   50
c ---[ 986]---> BDD-cost:   50
c ---[ 984]---> Sorter-cost:  237     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 982]---> Sorter-cost:  237     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 980]---> Sorter-cost:  237     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 978]---> Sorter-cost:  237     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 976]---> Sorter-cost:  237     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 974]---> Sorter-cost:  237     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 972]---> Sorter-cost:  237     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 970]---> Sorter-cost:  237     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 968]---> Sorter-cost:  237     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 966]---> Sorter-cost:  237     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 964]---> Sorter-cost:  237     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 962]---> Sorter-cost:  237     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 960]---> Sorter-cost:  237     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 958]---> Sorter-cost:  237     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 956]---> Sorter-cost:  237     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 954]---> Sorter-cost:  237     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 952]---> Sorter-cost:  237     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 950]---> BDD-cost:   50
c ---[ 948]---> Sorter-cost:  237     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 946]---> BDD-cost:   50
c ---[ 944]---> BDD-cost:   50
c ---[ 942]---> BDD-cost:   50
c ---[ 940]---> Sorter-cost:  237     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 938]---> Sorter-cost:  237     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 936]---> Sorter-cost:  237     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 934]---> Sorter-cost:  237     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 932]---> Sorter-cost:  237     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 930]---> Sorter-cost:  237     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 928]---> Sorter-cost:  237     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 926]---> Sorter-cost:  237     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 924]---> Sorter-cost:  237     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 922]---> Sorter-cost:  237     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 920]---> Sorter-cost:  237     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 918]---> BDD-cost:   50
c ---[ 916]---> Sorter-cost:  237     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 914]---> BDD-cost:   50
c ---[ 912]---> Sorter-cost:  237     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 910]---> Sorter-cost:  237     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 908]---> Sorter-cost:  237     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 906]---> Sorter-cost:  237     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 904]---> Sorter-cost:  237     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 902]---> Sorter-cost:  237     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 900]---> Sorter-cost:  237     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 898]---> Sorter-cost:  237     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 896]---> BDD-cost:   50
c ---[ 894]---> Sorter-cost:  237     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 892]---> Sorter-cost:  237     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 890]---> Sorter-cost:  237     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 888]---> Sorter-cost:  237     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 886]---> Sorter-cost:  237     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 884]---> Sorter-cost:  237     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 882]---> Sorter-cost:  237     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 880]---> Sorter-cost:  237     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 878]---> Sorter-cost:  237     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 876]---> Sorter-cost:  237     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 874]---> Sorter-cost:  237     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 872]---> Sorter-cost:  237     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 870]---> BDD-cost:   50
c ---[ 868]---> Sorter-cost:  237     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 866]---> BDD-cost:   50
c ---[ 864]---> Sorter-cost:  237     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 862]---> Sorter-cost:  237     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 860]---> Sorter-cost:  237     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 858]---> Sorter-cost:  237     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 856]---> Sorter-cost:  237     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 854]---> Sorter-cost:  237     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 852]---> Sorter-cost:  237     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 850]---> Sorter-cost:  237     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 848]---> BDD-cost:   50
c ---[ 846]---> Sorter-cost:  237     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 844]---> Sorter-cost:  237     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 842]---> Sorter-cost:  237     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 840]---> Sorter-cost:  237     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 838]---> BDD-cost:   50
c ---[ 836]---> Sorter-cost:  237     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 834]---> Sorter-cost:  237     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 832]---> Sorter-cost:  237     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 830]---> Sorter-cost:  237     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 828]---> Sorter-cost:  237     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 826]---> BDD-cost:   50
c ---[ 824]---> BDD-cost:   50
c ---[ 822]---> BDD-cost:   50
c ---[ 820]---> BDD-cost:   50
c ---[ 818]---> Sorter-cost:  237     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 816]---> BDD-cost:   50
c ---[ 814]---> Sorter-cost:  237     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 812]---> Sorter-cost:  237     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 810]---> Sorter-cost:  237     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 808]---> Sorter-cost:  237     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 806]---> Sorter-cost:  237     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 804]---> Sorter-cost:  237     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 802]---> Sorter-cost:  237     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 800]---> Sorter-cost:  237     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 798]---> Sorter-cost:  237     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 796]---> Sorter-cost:  237     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 794]---> Sorter-cost:  237     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 792]---> Sorter-cost:  237     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 790]---> Sorter-cost:  237     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 788]---> Sorter-cost:  237     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 786]---> Sorter-cost:  237     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 784]---> Sorter-cost:  237     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 782]---> Sorter-cost:  237     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 780]---> Sorter-cost:  237     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 778]---> Sorter-cost:  237     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 776]---> Sorter-cost:  237     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 774]---> Sorter-cost:  237     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 772]---> Sorter-cost:  237     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 770]---> Sorter-cost:  237     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 768]---> Sorter-cost:  237     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 766]---> Sorter-cost:  237     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 764]---> Sorter-cost:  237     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 762]---> Sorter-cost:  237     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 760]---> Sorter-cost:  237     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 758]---> Sorter-cost:  237     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 756]---> Sorter-cost:  237     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 754]---> Sorter-cost:  237     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 752]---> Sorter-cost:  237     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 750]---> Sorter-cost:  237     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 748]---> Sorter-cost:  237     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 746]---> Sorter-cost:  237     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 744]---> Sorter-cost:  237     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 742]---> Sorter-cost:  237     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 740]---> Sorter-cost:  237     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 738]---> Sorter-cost:  237     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 736]---> Sorter-cost:  237     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 734]---> Sorter-cost:  237     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 732]---> Sorter-cost:  237     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 730]---> Sorter-cost:  237     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 728]---> Sorter-cost:  237     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 726]---> Sorter-cost:  237     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 724]---> Sorter-cost:  237     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 722]---> Sorter-cost:  237     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 720]---> Sorter-cost:  237     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 718]---> Sorter-cost:  237     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 716]---> Sorter-cost:  237     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 714]---> Sorter-cost:  237     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 712]---> Sorter-cost:  237     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 710]---> Sorter-cost:  237     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 708]---> Sorter-cost:  237     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 706]---> Sorter-cost:  237     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 704]---> Sorter-cost:  237     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 702]---> Sorter-cost:  237     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 700]---> Sorter-cost:  237     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 698]---> Sorter-cost:  237     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 696]---> Sorter-cost:  237     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 694]---> Sorter-cost:  237     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 692]---> Sorter-cost:  237     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 690]---> Sorter-cost:  237     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 688]---> Sorter-cost:  237     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 686]---> Sorter-cost:  237     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 684]---> Sorter-cost:  237     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 682]---> Sorter-cost:  237     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 680]---> Sorter-cost:  237     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 678]---> Sorter-cost:  237     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 676]---> Sorter-cost:  237     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 674]---> Sorter-cost:  237     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 672]---> Sorter-cost:  237     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 670]---> Sorter-cost:  237     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 668]---> Sorter-cost:  237     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 666]---> Sorter-cost:  237     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 664]---> Sorter-cost:  237     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 662]---> Sorter-cost:  237     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 660]---> Sorter-cost:  237     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 658]---> Sorter-cost:  237     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 656]---> Sorter-cost:  237     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 654]---> Sorter-cost:  237     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 652]---> Sorter-cost:  237     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 650]---> Sorter-cost:  237     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 648]---> Sorter-cost:  237     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 646]---> Sorter-cost:  237     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 644]---> Sorter-cost:  237     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 642]---> Sorter-cost:  237     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 640]---> Sorter-cost:  237     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 638]---> Sorter-cost:  237     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 636]---> Sorter-cost:  237     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 634]---> Sorter-cost:  237     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 632]---> Sorter-cost:  237     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 630]---> Sorter-cost:  237     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 628]---> Sorter-cost:  237     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 626]---> Sorter-cost:  237     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 624]---> Sorter-cost:  237     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 622]---> Sorter-cost:  237     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 620]---> Sorter-cost:  237     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 618]---> Sorter-cost:  237     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 616]---> Sorter-cost:  237     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 614]---> Sorter-cost:  237     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 612]---> Sorter-cost:  237     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 610]---> Sorter-cost:  237     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 608]---> Sorter-cost:  237     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 606]---> Sorter-cost:  237     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 604]---> Sorter-cost:  237     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 602]---> Sorter-cost:  237     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 600]---> Sorter-cost:  237     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 598]---> Sorter-cost:  237     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 596]---> Sorter-cost:  237     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 594]---> Sorter-cost:  237     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 592]---> Sorter-cost:  237     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 590]---> Sorter-cost:  237     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 588]---> Sorter-cost:  237     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 586]---> Sorter-cost:  237     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 584]---> Sorter-cost:  237     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 582]---> Sorter-cost:  237     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 580]---> Sorter-cost:  237     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 578]---> Sorter-cost:  237     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 576]---> Sorter-cost:  237     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 574]---> Sorter-cost:  237     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 572]---> Sorter-cost:  237     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 570]---> Sorter-cost:  237     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 568]---> Sorter-cost:  237     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 566]---> Sorter-cost:  237     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 564]---> Sorter-cost:  237     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 562]---> Sorter-cost:  237     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 560]---> Sorter-cost:  237     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 558]---> Sorter-cost:  237     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 556]---> Sorter-cost:  237     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 554]---> Sorter-cost:  237     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 552]---> Sorter-cost:  237     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 550]---> Sorter-cost:  237     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 548]---> Sorter-cost:  237     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 546]---> Sorter-cost:  237     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 544]---> Sorter-cost:  237     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 542]---> Sorter-cost:  237     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 540]---> Sorter-cost:  237     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 538]---> Sorter-cost:  237     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 536]---> Sorter-cost:  237     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 534]---> Sorter-cost:  237     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 532]---> Sorter-cost:  237     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 530]---> Sorter-cost:  237     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 528]---> Sorter-cost:  237     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 526]---> Sorter-cost:  237     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 524]---> Sorter-cost:  237     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 522]---> Sorter-cost:  237     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 520]---> Sorter-cost:  237     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 518]---> Sorter-cost:  237     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 516]---> Sorter-cost:  237     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 514]---> Sorter-cost:  237     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 512]---> Sorter-cost:  237     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 510]---> Sorter-cost:  237     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 508]---> Sorter-cost:  237     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 506]---> Sorter-cost:  237     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 504]---> Sorter-cost:  237     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 502]---> Sorter-cost:  237     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 500]---> Sorter-cost:  237     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 498]---> Sorter-cost:  237     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 496]---> Sorter-cost:  237     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 494]---> Sorter-cost:  237     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 492]---> Sorter-cost:  237     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 490]---> Sorter-cost:  237     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 488]---> Sorter-cost:  237     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 486]---> Sorter-cost:  237     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 484]---> Sorter-cost:  237     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 482]---> Sorter-cost:  237     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 480]---> Sorter-cost:  237     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 478]---> Sorter-cost:  237     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 476]---> Sorter-cost:  237     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 474]---> Sorter-cost:  237     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 472]---> BDD-cost:   50
c ---[ 470]---> Sorter-cost:  237     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 468]---> Sorter-cost:  237     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 466]---> BDD-cost:   50
c ---[ 464]---> Sorter-cost:  237     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 462]---> Sorter-cost:  237     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 460]---> Sorter-cost:  237     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 458]---> Sorter-cost:  237     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 456]---> BDD-cost:   50
c ---[ 454]---> BDD-cost:   50
c ---[ 452]---> Sorter-cost:  237     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 450]---> Sorter-cost:  237     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 448]---> Sorter-cost:  237     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 446]---> Sorter-cost:  237     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 444]---> BDD-cost:   50
c ---[ 442]---> Sorter-cost:  237     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 440]---> Sorter-cost:  237     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 438]---> Sorter-cost:  237     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 436]---> Sorter-cost:  237     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 434]---> Sorter-cost:  237     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 432]---> Sorter-cost:  237     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 430]---> Sorter-cost:  237     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 428]---> BDD-cost:   50
c ---[ 426]---> BDD-cost:   50
c ---[ 424]---> Sorter-cost:  237     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 422]---> Sorter-cost:  237     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 420]---> Sorter-cost:  237     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 418]---> Sorter-cost:  237     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 416]---> Sorter-cost:  237     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 414]---> Sorter-cost:  237     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 412]---> Sorter-cost:  237     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 410]---> Sorter-cost:  237     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 408]---> Sorter-cost:  237     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 406]---> Sorter-cost:  237     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 404]---> Sorter-cost:  237     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 402]---> BDD-cost:   50
c ---[ 400]---> BDD-cost:   50
c ---[ 398]---> Sorter-cost:  237     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 396]---> Sorter-cost:  237     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 394]---> Sorter-cost:  237     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 392]---> Sorter-cost:  237     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 390]---> Sorter-cost:  237     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 388]---> Sorter-cost:  237     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 386]---> Sorter-cost:  237     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 384]---> Sorter-cost:  237     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 382]---> Sorter-cost:  237     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 380]---> Sorter-cost:  237     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 378]---> Sorter-cost:  237     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 376]---> Sorter-cost:  237     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 374]---> Sorter-cost:  237     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 372]---> Sorter-cost:  237     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 370]---> Sorter-cost:  237     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 368]---> Sorter-cost:  237     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 366]---> Sorter-cost:  237     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 364]---> Sorter-cost:  237     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 362]---> Sorter-cost:  237     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 360]---> Sorter-cost:  237     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 358]---> Sorter-cost:  237     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 356]---> Sorter-cost:  237     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 354]---> Sorter-cost:  237     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 352]---> Sorter-cost:  237     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 350]---> Sorter-cost:  237     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 348]---> Sorter-cost:  237     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 346]---> Sorter-cost:  237     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 344]---> Sorter-cost:  237     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 342]---> Sorter-cost:  237     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 340]---> BDD-cost:   50
c ---[ 338]---> BDD-cost:   50
c ---[ 336]---> BDD-cost:   50
c ---[ 334]---> Sorter-cost:  237     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 332]---> Sorter-cost:  237     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 330]---> Sorter-cost:  237     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 328]---> Sorter-cost:  237     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 326]---> Sorter-cost:  237     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 324]---> Sorter-cost:  237     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 322]---> Sorter-cost:  237     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 320]---> Sorter-cost:  237     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 318]---> Sorter-cost:  237     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 316]---> Sorter-cost:  237     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 314]---> Sorter-cost:  237     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 312]---> Sorter-cost:  237     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 310]---> Sorter-cost:  237     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 308]---> Sorter-cost:  237     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 306]---> Sorter-cost:  237     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 304]---> Sorter-cost:  237     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 302]---> Sorter-cost:  237     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 300]---> Sorter-cost:  237     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 298]---> Sorter-cost:  237     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 296]---> Sorter-cost:  237     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 294]---> Sorter-cost:  237     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 292]---> BDD-cost:   50
c ---[ 290]---> Sorter-cost:  237     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 288]---> Sorter-cost:  237     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 286]---> Sorter-cost:  237     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 284]---> Sorter-cost:  237     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 282]---> Sorter-cost:  237     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 280]---> Sorter-cost:  237     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 278]---> Sorter-cost:  237     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 276]---> Sorter-cost:  237     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 274]---> Sorter-cost:  237     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 272]---> Sorter-cost:  237     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 270]---> Sorter-cost:  237     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 268]---> Sorter-cost:  237     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 266]---> Sorter-cost:  237     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 264]---> Sorter-cost:  237     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 262]---> Sorter-cost:  237     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 260]---> BDD-cost:   50
c ---[ 258]---> Sorter-cost:  237     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 256]---> Sorter-cost:  237     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 254]---> Sorter-cost:  237     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 252]---> Sorter-cost:  237     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 250]---> Sorter-cost:  237     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 248]---> Sorter-cost:  237     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 246]---> Sorter-cost:  237     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 244]---> Sorter-cost:  237     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 242]---> BDD-cost:   50
c ---[ 240]---> Sorter-cost:  237     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 238]---> Sorter-cost:  237     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 236]---> BDD-cost:   50
c ---[ 234]---> BDD-cost:   50
c ---[ 232]---> BDD-cost:   50
c ---[ 230]---> BDD-cost:   50
c ---[ 228]---> Sorter-cost:  237     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 226]---> Sorter-cost:  237     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 224]---> Sorter-cost:  237     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 222]---> Sorter-cost:  237     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 220]---> Sorter-cost:  237     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 218]---> Sorter-cost:  237     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 216]---> Sorter-cost:  237     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 214]---> Sorter-cost:  237     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 212]---> Sorter-cost:  237     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 210]---> BDD-cost:   50
c ---[ 208]---> BDD-cost:   50
c ---[ 206]---> Sorter-cost:  237     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 204]---> Sorter-cost:  237     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 202]---> Sorter-cost:  237     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 200]---> Sorter-cost:  237     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 198]---> Sorter-cost:  237     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 196]---> Sorter-cost:  237     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 194]---> Sorter-cost:  237     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 192]---> Sorter-cost:  237     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 190]---> Sorter-cost:  237     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 188]---> Sorter-cost:  237     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 186]---> BDD-cost:   50
c ---[ 184]---> Sorter-cost:  237     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 182]---> Sorter-cost:  237     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 180]---> Sorter-cost:  237     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 178]---> BDD-cost:   50
c ---[ 176]---> BDD-cost:   50
c ---[ 174]---> BDD-cost:   50
c ---[ 172]---> Sorter-cost:  237     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 170]---> Sorter-cost:  237     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 168]---> BDD-cost:   50
c ---[ 166]---> BDD-cost:   50
c ---[ 164]---> Sorter-cost:  237     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 162]---> Sorter-cost:  237     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 160]---> Sorter-cost:  237     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 158]---> BDD-cost:   50
c ---[ 156]---> BDD-cost:   50
c ---[ 154]---> Sorter-cost:  237     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 152]---> Sorter-cost:  237     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 150]---> BDD-cost:   50
c ---[ 148]---> BDD-cost:   50
c ---[ 146]---> BDD-cost:   50
c ---[ 144]---> Sorter-cost:  237     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 142]---> Sorter-cost:  237     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 140]---> Sorter-cost:  237     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 138]---> Sorter-cost:  237     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 136]---> Sorter-cost:  237     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 134]---> Sorter-cost:  237     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 132]---> BDD-cost:   50
c ---[ 130]---> Sorter-cost:  237     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 128]---> BDD-cost:   50
c ---[ 126]---> Sorter-cost:  237     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 124]---> Sorter-cost:  237     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 122]---> Sorter-cost:  237     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 120]---> Sorter-cost:  237     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 118]---> BDD-cost:   50
c ---[ 116]---> Sorter-cost:  237     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 114]---> BDD-cost:   50
c ---[ 112]---> Sorter-cost:  237     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 110]---> Sorter-cost:  237     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 108]---> BDD-cost:   50
c ---[ 106]---> BDD-cost:   50
c ---[ 104]---> Sorter-cost:  237     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 102]---> Sorter-cost:  237     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 100]---> Sorter-cost:  237     Base: 2 2 2 2 2 2 2 2 2 2
c ---[  98]---> BDD-cost:   50
c ---[  96]---> Sorter-cost:  237     Base: 2 2 2 2 2 2 2 2 2 2
c ---[  94]---> Sorter-cost:  237     Base: 2 2 2 2 2 2 2 2 2 2
c ---[  92]---> Sorter-cost:  237     Base: 2 2 2 2 2 2 2 2 2 2
c ---[  90]---> Sorter-cost:  237     Base: 2 2 2 2 2 2 2 2 2 2
c ---[  88]---> BDD-cost:   50
c ---[  86]---> BDD-cost:   50
c ---[  84]---> BDD-cost:   50
c ---[  82]---> BDD-cost:   50
c ---[  80]---> BDD-cost:   50
c ---[  78]---> BDD-cost:   50
c ---[  76]---> BDD-cost:   50
c ---[  74]---> Sorter-cost:  237     Base: 2 2 2 2 2 2 2 2 2 2
c ---[  72]---> BDD-cost:   50
c ---[  70]---> BDD-cost:   50
c ---[  68]---> Sorter-cost:  237     Base: 2 2 2 2 2 2 2 2 2 2
c ---[  66]---> BDD-cost:   50
c ---[  64]---> BDD-cost:   50
c ---[  62]---> BDD-cost:   50
c ---[  60]---> BDD-cost:   50
c ---[  58]---> BDD-cost:   50
c ---[  56]---> Sorter-cost:  237     Base: 2 2 2 2 2 2 2 2 2 2
c ---[  54]---> BDD-cost:   50
c ---[  52]---> BDD-cost:   50
c ---[  50]---> Sorter-cost:  237     Base: 2 2 2 2 2 2 2 2 2 2
c ---[  48]---> BDD-cost:   50
c ---[  46]---> BDD-cost:   50
c ---[  44]---> Sorter-cost:  237     Base: 2 2 2 2 2 2 2 2 2 2
c ---[  42]---> Sorter-cost:  237     Base: 2 2 2 2 2 2 2 2 2 2
c ---[  40]---> BDD-cost:   50
c ---[  38]---> Sorter-cost:  237     Base: 2 2 2 2 2 2 2 2 2 2
c ---[  36]---> BDD-cost:   50
c ---[  34]---> BDD-cost:   50
c ---[  32]---> Sorter-cost:  237     Base: 2 2 2 2 2 2 2 2 2 2
c ---[  30]---> Sorter-cost:  237     Base: 2 2 2 2 2 2 2 2 2 2
c ---[  28]---> Sorter-cost:  237     Base: 2 2 2 2 2 2 2 2 2 2
c ---[  26]---> Sorter-cost:  237     Base: 2 2 2 2 2 2 2 2 2 2
c ---[  24]---> Sorter-cost:  237     Base: 2 2 2 2 2 2 2 2 2 2
c ---[  22]---> BDD-cost:   50
c ---[  20]---> Sorter-cost:  237     Base: 2 2 2 2 2 2 2 2 2 2
c ---[  18]---> BDD-cost:   50
c ---[  16]---> Sorter-cost:  237     Base: 2 2 2 2 2 2 2 2 2 2
c ---[  14]---> Sorter-cost:  237     Base: 2 2 2 2 2 2 2 2 2 2
c ---[  12]---> BDD-cost:   50
c ---[  10]---> Sorter-cost:  237     Base: 2 2 2 2 2 2 2 2 2 2
c ---[   8]---> Sorter-cost:  237     Base: 2 2 2 2 2 2 2 2 2 2
c ---[   6]---> Sorter-cost:  237     Base: 2 2 2 2 2 2 2 2 2 2
c ---[   4]---> Sorter-cost:  237     Base: 2 2 2 2 2 2 2 2 2 2
c ---[   2]---> Sorter-cost:  237     Base: 2 2 2 2 2 2 2 2 2 2
c ---[   0]---> Sorter-cost:  237     Base: 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 | 3567829 11196487 | 1189276       0        0     nan |  0.000 % |
c |       100 | 3567829 11196487 | 1308203     100      781     7.8 |  6.018 % |
c |       250 | 3567821 11196461 | 1439023     249     1346     5.4 |  6.018 % |
c |       475 | 3567739 11196279 | 1582926     463     2031     4.4 |  6.021 % |
c |       813 | 3567600 11195964 | 1741218     782     3058     3.9 |  6.026 % |
c |      1319 | 3567461 11195657 | 1915340    1269     4818     3.8 |  6.031 % |
c |      2078 | 3567207 11195095 | 2106874    1998     7109     3.6 |  6.040 % |
c |      3217 | 3567146 11194959 | 2317562    3131    26169     8.4 |  6.042 % |
c |      4926 | 3566980 11194596 | 2549318    4814    33029     6.9 |  6.048 % |
c |      7491 | 3566744 11194073 | 2804250    7353    44912     6.1 |  6.056 % |
c |     11336 | 3566433 11193382 | 3084675   11161    65856     5.9 |  6.067 % |
c |     17102 | 3566103 11192647 | 3393143   16892   102752     6.1 |  6.078 % |
c |     25752 | 3565774 11191898 | 3732457   25506   169430     6.6 |  6.088 % |
c |     38726 | 3564870 11189882 | 4105703   38339   257582     6.7 |  6.118 % |
c |     58189 | 3564639 11189366 | 4516273   57769   992314    17.2 |  6.126 % |
c |     87381 | 3563568 11186972 | 4967900   86820  1816764    20.9 |  6.162 % |
c |    131170 | 3562087 11183609 | 5464691  130391  3009134    23.1 |  6.211 % |
/oldhome/oroussel/solvers/minisat+_script: line 9: 10003 CPU time limit exceeded $XDIR/minisat+_64-bit_static -try "$@"
#### 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.93 0.98 0.95 2/54 9999
Raw data (stat): 9999 (runsolver) R 9998 25568 25567 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 782674587 1052672 99 4294967295 134512640 135381576 3221224480 3221219688 135158418 0 2147483391 7 90112 0 0 0 17 0 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0009 s]
Raw data (loadavg): 0.94 0.98 0.95 2/55 10003
Raw data (stat): 9999 (minisat+_script) S 9998 25568 25567 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782674587 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+20.0022 s]
Raw data (loadavg): 0.95 0.98 0.95 2/55 10003
Raw data (stat): 9999 (minisat+_script) S 9998 25568 25567 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782674587 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+30.0206 s]
Raw data (loadavg): 0.96 0.98 0.95 2/55 10003
Raw data (stat): 9999 (minisat+_script) S 9998 25568 25567 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782674587 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+40.0375 s]
Raw data (loadavg): 0.96 0.98 0.95 2/55 10003
Raw data (stat): 9999 (minisat+_script) S 9998 25568 25567 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782674587 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+50.0386 s]
Raw data (loadavg): 0.97 0.98 0.95 2/55 10003
Raw data (stat): 9999 (minisat+_script) S 9998 25568 25567 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782674587 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+60.0395 s]
Raw data (loadavg): 0.97 0.98 0.95 2/55 10005
Raw data (stat): 9999 (minisat+_script) S 9998 25568 25567 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782674587 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+70.0395 s]
Raw data (loadavg): 0.98 0.98 0.95 2/55 10005
Raw data (stat): 9999 (minisat+_script) S 9998 25568 25567 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782674587 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+80.0413 s]
Raw data (loadavg): 0.98 0.98 0.95 2/55 10005
Raw data (stat): 9999 (minisat+_script) S 9998 25568 25567 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782674587 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+90.0425 s]
Raw data (loadavg): 0.98 0.98 0.95 2/55 10005
Raw data (stat): 9999 (minisat+_script) S 9998 25568 25567 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782674587 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+100.043 s]
Raw data (loadavg): 0.98 0.98 0.95 2/55 10005
Raw data (stat): 9999 (minisat+_script) S 9998 25568 25567 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782674587 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+110.051 s]
Raw data (loadavg): 0.99 0.98 0.95 2/55 10005
Raw data (stat): 9999 (minisat+_script) S 9998 25568 25567 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782674587 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+120.058 s]
Raw data (loadavg): 0.99 0.98 0.95 2/55 10005
Raw data (stat): 9999 (minisat+_script) S 9998 25568 25567 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782674587 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+130.058 s]
Raw data (loadavg): 0.99 0.98 0.95 2/55 10005
Raw data (stat): 9999 (minisat+_script) S 9998 25568 25567 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782674587 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+140.059 s]
Raw data (loadavg): 0.99 0.98 0.95 2/55 10005
Raw data (stat): 9999 (minisat+_script) S 9998 25568 25567 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782674587 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+150.06 s]
Raw data (loadavg): 0.99 0.98 0.95 2/55 10005
Raw data (stat): 9999 (minisat+_script) S 9998 25568 25567 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782674587 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+160.061 s]
Raw data (loadavg): 0.99 0.98 0.95 2/55 10005
Raw data (stat): 9999 (minisat+_script) S 9998 25568 25567 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782674587 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+170.061 s]
Raw data (loadavg): 0.99 0.98 0.95 2/55 10005
Raw data (stat): 9999 (minisat+_script) S 9998 25568 25567 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782674587 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+180.062 s]
Raw data (loadavg): 0.99 0.98 0.95 2/55 10005
Raw data (stat): 9999 (minisat+_script) S 9998 25568 25567 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782674587 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+190.063 s]
Raw data (loadavg): 0.99 0.98 0.95 2/55 10005
Raw data (stat): 9999 (minisat+_script) S 9998 25568 25567 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782674587 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+200.063 s]
Raw data (loadavg): 0.99 0.98 0.95 2/55 10005
Raw data (stat): 9999 (minisat+_script) S 9998 25568 25567 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782674587 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+210.064 s]
Raw data (loadavg): 0.99 0.98 0.95 2/55 10005
Raw data (stat): 9999 (minisat+_script) S 9998 25568 25567 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782674587 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+220.065 s]
Raw data (loadavg): 0.99 0.98 0.95 2/55 10005
Raw data (stat): 9999 (minisat+_script) S 9998 25568 25567 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782674587 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+230.065 s]
Raw data (loadavg): 0.99 0.98 0.95 2/55 10005
Raw data (stat): 9999 (minisat+_script) S 9998 25568 25567 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782674587 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+240.065 s]
Raw data (loadavg): 0.99 0.98 0.95 2/55 10005
Raw data (stat): 9999 (minisat+_script) S 9998 25568 25567 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782674587 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+250.066 s]
Raw data (loadavg): 0.99 0.98 0.95 2/55 10005
Raw data (stat): 9999 (minisat+_script) S 9998 25568 25567 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782674587 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+260.065 s]
Raw data (loadavg): 0.99 0.98 0.95 2/55 10005
Raw data (stat): 9999 (minisat+_script) S 9998 25568 25567 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782674587 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+270.065 s]
Raw data (loadavg): 0.99 0.98 0.95 2/55 10005
Raw data (stat): 9999 (minisat+_script) S 9998 25568 25567 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782674587 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+280.064 s]
Raw data (loadavg): 0.99 0.98 0.95 2/55 10005
Raw data (stat): 9999 (minisat+_script) S 9998 25568 25567 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782674587 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+290.064 s]
Raw data (loadavg): 0.99 0.98 0.95 2/55 10005
Raw data (stat): 9999 (minisat+_script) S 9998 25568 25567 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782674587 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+300.064 s]
Raw data (loadavg): 0.99 0.98 0.95 2/55 10005
Raw data (stat): 9999 (minisat+_script) S 9998 25568 25567 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782674587 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+310.064 s]
Raw data (loadavg): 0.99 0.98 0.95 2/55 10005
Raw data (stat): 9999 (minisat+_script) S 9998 25568 25567 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782674587 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+320.063 s]
Raw data (loadavg): 0.99 0.98 0.95 2/55 10005
Raw data (stat): 9999 (minisat+_script) S 9998 25568 25567 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782674587 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+330.064 s]
Raw data (loadavg): 0.99 0.98 0.95 2/55 10005
Raw data (stat): 9999 (minisat+_script) S 9998 25568 25567 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782674587 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+340.063 s]
Raw data (loadavg): 0.99 0.98 0.95 2/55 10005
Raw data (stat): 9999 (minisat+_script) S 9998 25568 25567 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782674587 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+350.063 s]
Raw data (loadavg): 0.99 0.98 0.95 2/55 10005
Raw data (stat): 9999 (minisat+_script) S 9998 25568 25567 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782674587 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+360.063 s]
Raw data (loadavg): 0.99 0.98 0.95 2/55 10005
Raw data (stat): 9999 (minisat+_script) S 9998 25568 25567 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782674587 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+370.063 s]
Raw data (loadavg): 0.99 0.98 0.95 2/55 10005
Raw data (stat): 9999 (minisat+_script) S 9998 25568 25567 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782674587 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+380.063 s]
Raw data (loadavg): 0.99 0.98 0.95 2/55 10005
Raw data (stat): 9999 (minisat+_script) S 9998 25568 25567 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782674587 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+390.063 s]
Raw data (loadavg): 0.99 0.98 0.95 2/55 10005
Raw data (stat): 9999 (minisat+_script) S 9998 25568 25567 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782674587 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+400.062 s]
Raw data (loadavg): 0.99 0.98 0.95 2/55 10005
Raw data (stat): 9999 (minisat+_script) S 9998 25568 25567 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782674587 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+410.062 s]
Raw data (loadavg): 0.99 0.98 0.95 2/55 10005
Raw data (stat): 9999 (minisat+_script) S 9998 25568 25567 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782674587 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+420.061 s]
Raw data (loadavg): 0.99 0.98 0.95 2/55 10005
Raw data (stat): 9999 (minisat+_script) S 9998 25568 25567 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782674587 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+430.061 s]
Raw data (loadavg): 0.99 0.98 0.95 2/55 10005
Raw data (stat): 9999 (minisat+_script) S 9998 25568 25567 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782674587 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+440.061 s]
Raw data (loadavg): 0.99 0.98 0.95 2/55 10005
Raw data (stat): 9999 (minisat+_script) S 9998 25568 25567 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782674587 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+450.061 s]
Raw data (loadavg): 0.99 0.98 0.95 2/55 10005
Raw data (stat): 9999 (minisat+_script) S 9998 25568 25567 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782674587 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+460.06 s]
Raw data (loadavg): 0.99 0.98 0.95 2/55 10005
Raw data (stat): 9999 (minisat+_script) S 9998 25568 25567 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782674587 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+470.06 s]
Raw data (loadavg): 0.99 0.98 0.95 2/55 10005
Raw data (stat): 9999 (minisat+_script) S 9998 25568 25567 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782674587 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+480.06 s]
Raw data (loadavg): 0.99 0.98 0.95 2/55 10005
Raw data (stat): 9999 (minisat+_script) S 9998 25568 25567 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782674587 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+490.06 s]
Raw data (loadavg): 0.99 0.98 0.95 2/55 10005
Raw data (stat): 9999 (minisat+_script) S 9998 25568 25567 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782674587 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+500.06 s]
Raw data (loadavg): 0.99 0.98 0.95 2/55 10005
Raw data (stat): 9999 (minisat+_script) S 9998 25568 25567 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782674587 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+510.059 s]
Raw data (loadavg): 0.99 0.98 0.95 2/55 10005
Raw data (stat): 9999 (minisat+_script) S 9998 25568 25567 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782674587 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+520.059 s]
Raw data (loadavg): 0.99 0.98 0.95 2/55 10005
Raw data (stat): 9999 (minisat+_script) S 9998 25568 25567 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782674587 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+530.058 s]
Raw data (loadavg): 0.99 0.98 0.95 2/55 10005
Raw data (stat): 9999 (minisat+_script) S 9998 25568 25567 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782674587 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+540.059 s]
Raw data (loadavg): 0.99 0.98 0.95 2/55 10005
Raw data (stat): 9999 (minisat+_script) S 9998 25568 25567 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782674587 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+550.059 s]
Raw data (loadavg): 0.99 0.98 0.95 2/55 10005
Raw data (stat): 9999 (minisat+_script) S 9998 25568 25567 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782674587 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+560.059 s]
Raw data (loadavg): 0.99 0.98 0.95 2/55 10005
Raw data (stat): 9999 (minisat+_script) S 9998 25568 25567 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782674587 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+570.059 s]
Raw data (loadavg): 0.99 0.98 0.95 2/55 10005
Raw data (stat): 9999 (minisat+_script) S 9998 25568 25567 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782674587 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+580.059 s]
Raw data (loadavg): 0.99 0.98 0.95 2/55 10005
Raw data (stat): 9999 (minisat+_script) S 9998 25568 25567 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782674587 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+590.058 s]
Raw data (loadavg): 0.99 0.98 0.95 2/55 10005
Raw data (stat): 9999 (minisat+_script) S 9998 25568 25567 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782674587 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+600.058 s]
Raw data (loadavg): 0.99 0.98 0.95 2/55 10005
Raw data (stat): 9999 (minisat+_script) S 9998 25568 25567 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782674587 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+610.058 s]
Raw data (loadavg): 0.99 0.98 0.95 2/55 10005
Raw data (stat): 9999 (minisat+_script) S 9998 25568 25567 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782674587 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+620.058 s]
Raw data (loadavg): 0.99 0.98 0.95 2/55 10005
Raw data (stat): 9999 (minisat+_script) S 9998 25568 25567 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782674587 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+630.057 s]
Raw data (loadavg): 0.99 0.98 0.95 2/55 10005
Raw data (stat): 9999 (minisat+_script) S 9998 25568 25567 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782674587 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+640.057 s]
Raw data (loadavg): 0.99 0.98 0.95 2/55 10005
Raw data (stat): 9999 (minisat+_script) S 9998 25568 25567 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782674587 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+650.056 s]
Raw data (loadavg): 0.99 0.98 0.95 2/55 10005
Raw data (stat): 9999 (minisat+_script) S 9998 25568 25567 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782674587 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+660.056 s]
Raw data (loadavg): 0.99 0.98 0.95 2/55 10005
Raw data (stat): 9999 (minisat+_script) S 9998 25568 25567 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782674587 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+670.06 s]
Raw data (loadavg): 0.99 0.98 0.95 2/55 10005
Raw data (stat): 9999 (minisat+_script) S 9998 25568 25567 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782674587 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+680.059 s]
Raw data (loadavg): 0.99 0.98 0.95 2/55 10005
Raw data (stat): 9999 (minisat+_script) S 9998 25568 25567 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782674587 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+690.059 s]
Raw data (loadavg): 0.99 0.98 0.95 2/55 10005
Raw data (stat): 9999 (minisat+_script) S 9998 25568 25567 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782674587 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+700.059 s]
Raw data (loadavg): 0.99 0.98 0.95 2/55 10005
Raw data (stat): 9999 (minisat+_script) S 9998 25568 25567 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782674587 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+710.059 s]
Raw data (loadavg): 0.99 0.98 0.95 2/55 10005
Raw data (stat): 9999 (minisat+_script) S 9998 25568 25567 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782674587 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+720.058 s]
Raw data (loadavg): 0.99 0.98 0.95 2/55 10005
Raw data (stat): 9999 (minisat+_script) S 9998 25568 25567 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782674587 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+730.059 s]
Raw data (loadavg): 0.99 0.98 0.95 2/55 10005
Raw data (stat): 9999 (minisat+_script) S 9998 25568 25567 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782674587 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+740.058 s]
Raw data (loadavg): 0.99 0.98 0.95 2/55 10005
Raw data (stat): 9999 (minisat+_script) S 9998 25568 25567 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782674587 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+750.059 s]
Raw data (loadavg): 0.99 0.98 0.95 2/55 10005
Raw data (stat): 9999 (minisat+_script) S 9998 25568 25567 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782674587 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+760.059 s]
Raw data (loadavg): 0.99 0.98 0.95 2/55 10005
Raw data (stat): 9999 (minisat+_script) S 9998 25568 25567 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782674587 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+770.058 s]
Raw data (loadavg): 0.99 0.98 0.95 2/55 10005
Raw data (stat): 9999 (minisat+_script) S 9998 25568 25567 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782674587 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+780.058 s]
Raw data (loadavg): 0.99 0.98 0.95 2/55 10005
Raw data (stat): 9999 (minisat+_script) S 9998 25568 25567 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782674587 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+790.072 s]
Raw data (loadavg): 0.99 0.98 0.95 2/55 10005
Raw data (stat): 9999 (minisat+_script) S 9998 25568 25567 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782674587 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+800.072 s]
Raw data (loadavg): 0.99 0.98 0.95 2/55 10005
Raw data (stat): 9999 (minisat+_script) S 9998 25568 25567 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782674587 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+810.072 s]
Raw data (loadavg): 0.99 0.98 0.95 2/55 10005
Raw data (stat): 9999 (minisat+_script) S 9998 25568 25567 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782674587 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+820.072 s]
Raw data (loadavg): 0.99 0.98 0.95 2/55 10005
Raw data (stat): 9999 (minisat+_script) S 9998 25568 25567 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782674587 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+830.071 s]
Raw data (loadavg): 0.99 0.98 0.95 2/55 10005
Raw data (stat): 9999 (minisat+_script) S 9998 25568 25567 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782674587 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+840.071 s]
Raw data (loadavg): 0.99 0.98 0.95 2/55 10005
Raw data (stat): 9999 (minisat+_script) S 9998 25568 25567 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782674587 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+850.072 s]
Raw data (loadavg): 0.99 0.98 0.95 2/55 10005
Raw data (stat): 9999 (minisat+_script) S 9998 25568 25567 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782674587 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+860.071 s]
Raw data (loadavg): 0.99 0.98 0.95 2/55 10005
Raw data (stat): 9999 (minisat+_script) S 9998 25568 25567 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782674587 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+870.072 s]
Raw data (loadavg): 0.99 0.98 0.95 2/55 10005
Raw data (stat): 9999 (minisat+_script) S 9998 25568 25567 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782674587 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+880.072 s]
Raw data (loadavg): 0.99 0.98 0.95 2/55 10005
Raw data (stat): 9999 (minisat+_script) S 9998 25568 25567 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782674587 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+890.072 s]
Raw data (loadavg): 0.99 0.98 0.95 2/55 10005
Raw data (stat): 9999 (minisat+_script) S 9998 25568 25567 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782674587 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+900.072 s]
Raw data (loadavg): 0.99 0.98 0.95 2/55 10005
Raw data (stat): 9999 (minisat+_script) S 9998 25568 25567 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782674587 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+910.073 s]
Raw data (loadavg): 0.99 0.98 0.95 2/55 10005
Raw data (stat): 9999 (minisat+_script) S 9998 25568 25567 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782674587 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+920.072 s]
Raw data (loadavg): 0.99 0.98 0.95 2/55 10005
Raw data (stat): 9999 (minisat+_script) S 9998 25568 25567 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782674587 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+930.073 s]
Raw data (loadavg): 0.99 0.98 0.95 2/55 10005
Raw data (stat): 9999 (minisat+_script) S 9998 25568 25567 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782674587 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+940.072 s]
Raw data (loadavg): 0.99 0.98 0.95 2/55 10005
Raw data (stat): 9999 (minisat+_script) S 9998 25568 25567 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782674587 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+950.073 s]
Raw data (loadavg): 0.99 0.98 0.95 2/55 10005
Raw data (stat): 9999 (minisat+_script) S 9998 25568 25567 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782674587 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+960.073 s]
Raw data (loadavg): 0.99 0.98 0.95 2/55 10005
Raw data (stat): 9999 (minisat+_script) S 9998 25568 25567 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782674587 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+970.073 s]
Raw data (loadavg): 0.99 0.98 0.95 2/55 10005
Raw data (stat): 9999 (minisat+_script) S 9998 25568 25567 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782674587 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+980.073 s]
Raw data (loadavg): 0.99 0.98 0.95 2/55 10005
Raw data (stat): 9999 (minisat+_script) S 9998 25568 25567 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782674587 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+990.074 s]
Raw data (loadavg): 0.99 0.98 0.95 2/55 10005
Raw data (stat): 9999 (minisat+_script) S 9998 25568 25567 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782674587 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1000.07 s]
Raw data (loadavg): 0.99 0.98 0.95 2/55 10005
Raw data (stat): 9999 (minisat+_script) S 9998 25568 25567 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782674587 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1010.07 s]
Raw data (loadavg): 0.99 0.98 0.95 2/55 10005
Raw data (stat): 9999 (minisat+_script) S 9998 25568 25567 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782674587 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1020.08 s]
Raw data (loadavg): 0.99 0.98 0.95 2/55 10005
Raw data (stat): 9999 (minisat+_script) S 9998 25568 25567 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782674587 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1030.08 s]
Raw data (loadavg): 0.99 0.98 0.95 2/55 10005
Raw data (stat): 9999 (minisat+_script) S 9998 25568 25567 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782674587 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1040.08 s]
Raw data (loadavg): 0.99 0.98 0.95 2/55 10005
Raw data (stat): 9999 (minisat+_script) S 9998 25568 25567 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782674587 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1050.08 s]
Raw data (loadavg): 0.99 0.98 0.95 2/55 10005
Raw data (stat): 9999 (minisat+_script) S 9998 25568 25567 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782674587 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1060.08 s]
Raw data (loadavg): 0.99 0.98 0.95 2/55 10005
Raw data (stat): 9999 (minisat+_script) S 9998 25568 25567 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782674587 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1070.08 s]
Raw data (loadavg): 0.99 0.98 0.95 2/55 10005
Raw data (stat): 9999 (minisat+_script) S 9998 25568 25567 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782674587 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1080.08 s]
Raw data (loadavg): 0.99 0.98 0.95 2/55 10005
Raw data (stat): 9999 (minisat+_script) S 9998 25568 25567 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782674587 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1090.08 s]
Raw data (loadavg): 0.99 0.98 0.95 2/55 10005
Raw data (stat): 9999 (minisat+_script) S 9998 25568 25567 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782674587 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1100.08 s]
Raw data (loadavg): 0.99 0.98 0.95 2/55 10005
Raw data (stat): 9999 (minisat+_script) S 9998 25568 25567 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782674587 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1110.08 s]
Raw data (loadavg): 0.99 0.98 0.95 2/55 10005
Raw data (stat): 9999 (minisat+_script) S 9998 25568 25567 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782674587 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1120.08 s]
Raw data (loadavg): 0.99 0.98 0.95 2/55 10005
Raw data (stat): 9999 (minisat+_script) S 9998 25568 25567 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782674587 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1130.08 s]
Raw data (loadavg): 0.99 0.98 0.95 2/55 10005
Raw data (stat): 9999 (minisat+_script) S 9998 25568 25567 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782674587 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1140.08 s]
Raw data (loadavg): 0.99 0.98 0.95 2/55 10005
Raw data (stat): 9999 (minisat+_script) S 9998 25568 25567 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782674587 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1150.08 s]
Raw data (loadavg): 0.99 0.98 0.95 2/55 10005
Raw data (stat): 9999 (minisat+_script) S 9998 25568 25567 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782674587 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1160.08 s]
Raw data (loadavg): 0.99 0.98 0.95 2/55 10005
Raw data (stat): 9999 (minisat+_script) S 9998 25568 25567 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782674587 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1170.08 s]
Raw data (loadavg): 0.99 0.98 0.95 2/55 10005
Raw data (stat): 9999 (minisat+_script) S 9998 25568 25567 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782674587 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1180.08 s]
Raw data (loadavg): 0.99 0.98 0.95 2/55 10005
Raw data (stat): 9999 (minisat+_script) S 9998 25568 25567 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782674587 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1190.08 s]
Raw data (loadavg): 0.99 0.98 0.95 2/55 10005
Raw data (stat): 9999 (minisat+_script) S 9998 25568 25567 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782674587 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1200.08 s]
Raw data (loadavg): 0.99 0.98 0.95 2/55 10005
Raw data (stat): 9999 (minisat+_script) S 9998 25568 25567 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782674587 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1210.08 s]
Raw data (loadavg): 0.99 0.98 0.95 2/55 10005
Raw data (stat): 9999 (minisat+_script) S 9998 25568 25567 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782674587 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1220.08 s]
Raw data (loadavg): 0.99 0.98 0.95 2/55 10005
Raw data (stat): 9999 (minisat+_script) S 9998 25568 25567 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782674587 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1229.68 s]
Raw data (loadavg): 0.99 0.98 0.95 1/53 10005
Raw data (stat): 9999 (minisat+_script) S 9998 25568 25567 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782674587 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 0

Child status: 152
Real time (s): 1229.68
CPU time (s): 1229.99
CPU user time (s): 1227.4
CPU system time (s): 2.58561
CPU usage (%): 100.025
Max. virtual memory (Kb): 2124
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####