PB'05 competition: run trace

Some explanations

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

Name	normalized-opb/mps-v2-13-7/ftp.netlib.org/lp/data/normalized-mps-v2-13-7-degen3.opb
MD5SUM	60f638829868e3a2820fb14a59c3225e
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	31460
Biggest coefficient in the objective function	977797120
Number of bits for the biggest coefficient in the objective function	30
Sum of the numbers in the objective function	331425197400
Number of bits of the sum of numbers in the objective function	39
Biggest number in a constraint	977797120
Number of bits of the biggest number in a constraint	30
Biggest sum of numbers in a constraint	331425197400
Number of bits of the biggest sum of numbers	39
Best result obtained on this benchmark	UNSAT
Best CPU time to get the best result obtained on this benchmark	0.311952
Number of variables	36360
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	40
Maximum length of a constraint	4060
Trace number 20013

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc31 THE 2005-04-21 19:59:36 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=15702 boxname=wulflinc31 idbench=1208 idsolver=11 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  60f638829868e3a2820fb14a59c3225e  /oldhome/oroussel/tmp/wulflinc31/normalized-mps-v2-13-7-degen3.opb
REAL COMMAND:  minisat+ -S /oldhome/oroussel/tmp/wulflinc31/normalized-mps-v2-13-7-degen3.opb /oldhome/oroussel/tmp/wulflinc31/normalized-mps-v2-13-7-degen3.opb
IDLAUNCH: 15702
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.153
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	: 3
cpu MHz		: 451.153
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	: 901.12

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        718552 kB
Buffers:         31572 kB
Cached:         258628 kB
SwapCached:        636 kB
Active:          74948 kB
Inactive:       217200 kB
HighTotal:      131008 kB
HighFree:          252 kB
LowTotal:       903652 kB
LowFree:        718300 kB
SwapTotal:     2097892 kB
SwapFree:      2096356 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           5024 kB
Slab:            18340 kB
Committed_AS:    63592 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-21 20:19:38 (client local time) WITH STATUS 0 IN 1200.53 SECONDS
stats: 15702 7 1200.53 0
#### 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: 4174   maxlim: 1316290   bits: 21/21
c ---[2218]---> Adder-cost: 3858   maxlim: 621634   bits: 20/20
c ---[2217]---> Adder-cost: 3962   maxlim: 679235   bits: 20/20
c ---[2215]---> Adder-cost: 304   maxlim: 2550   bits: 13/12
c ---[2213]---> Adder-cost: 304   maxlim: 2550   bits: 13/12
c ---[2211]---> Sorter-cost:  280     Base: 2 2 2 2 2 2 2
c ---[2209]---> Sorter-cost:  280     Base: 2 2 2 2 2 2 2
c ---[2207]---> Sorter-cost:  602     Base: 2 2 2 2 2 2 2
c ---[2205]---> Sorter-cost:  602     Base: 2 2 2 2 2 2 2
c ---[2203]---> Sorter-cost:  280     Base: 2 2 2 2 2 2 2
c ---[2201]---> Sorter-cost:  280     Base: 2 2 2 2 2 2 2
c ---[2199]---> Sorter-cost:  280     Base: 2 2 2 2 2 2 2
c ---[2197]---> Sorter-cost:  280     Base: 2 2 2 2 2 2 2
c ---[2195]---> Sorter-cost:  280     Base: 2 2 2 2 2 2 2
c ---[2193]---> Sorter-cost:  920     Base: 2 2 2 2 2 2 2
c ---[2191]---> Sorter-cost:  920     Base: 2 2 2 2 2 2 2
c ---[2189]---> Sorter-cost: 1441     Base: 2 2 2 2 2 2 2
c ---[2187]---> Sorter-cost:  920     Base: 2 2 2 2 2 2 2
c ---[2185]---> Sorter-cost:  602     Base: 2 2 2 2 2 2 2
c ---[2183]---> Sorter-cost:  433     Base: 2 2 2 2 2 2 2
c ---[2181]---> Sorter-cost:  602     Base: 2 2 2 2 2 2 2
c ---[2179]---> Sorter-cost:  602     Base: 2 2 2 2 2 2 2
c ---[2177]---> Sorter-cost:  920     Base: 2 2 2 2 2 2 2
c ---[2175]---> Sorter-cost:  280     Base: 2 2 2 2 2 2 2
c ---[2173]---> BDD-cost:   22
c ---[2171]---> BDD-cost:   22
c ---[2169]---> Adder-cost: 688   maxlim: 5610   bits: 14/13
c ---[2167]---> Adder-cost: 640   maxlim: 5100   bits: 14/13
c ---[2165]---> Sorter-cost:  280     Base: 2 2 2 2 2 2 2
c ---[2163]---> Sorter-cost:  280     Base: 2 2 2 2 2 2 2
c ---[2161]---> Sorter-cost:  280     Base: 2 2 2 2 2 2 2
c ---[2159]---> Sorter-cost:  280     Base: 2 2 2 2 2 2 2
c ---[2157]---> Sorter-cost:  280     Base: 2 2 2 2 2 2 2
c ---[2155]---> Sorter-cost:  280     Base: 2 2 2 2 2 2 2
c ---[2153]---> Sorter-cost:  602     Base: 2 2 2 2 2 2 2
c ---[2151]---> Sorter-cost:  433     Base: 2 2 2 2 2 2 2
c ---[2149]---> Sorter-cost:  280     Base: 2 2 2 2 2 2 2
c ---[2147]---> Sorter-cost:  280     Base: 2 2 2 2 2 2 2
c ---[2145]---> Sorter-cost: 1893     Base: 2 2 2 2 2 2 2
c ---[2143]---> Sorter-cost: 1637     Base: 2 2 2 2 2 2 2
c ---[2141]---> Adder-cost: 2720   maxlim: 22185   bits: 16/15
c ---[2139]---> Adder-cost: 1880   maxlim: 11475   bits: 15/14
c ---[2137]---> Adder-cost: 240   maxlim: 2040   bits: 12/11
c ---[2135]---> Adder-cost: 240   maxlim: 2040   bits: 12/11
c ---[2133]---> Sorter-cost:  280     Base: 2 2 2 2 2 2 2
c ---[2131]---> Sorter-cost:  280     Base: 2 2 2 2 2 2 2
c ---[2129]---> Sorter-cost:  280     Base: 2 2 2 2 2 2 2
c ---[2127]---> Sorter-cost:  280     Base: 2 2 2 2 2 2 2
c ---[2125]---> Sorter-cost:  280     Base: 2 2 2 2 2 2 2
c ---[2123]---> Sorter-cost:  280     Base: 2 2 2 2 2 2 2
c ---[2121]---> Sorter-cost:  920     Base: 2 2 2 2 2 2 2
c ---[2119]---> Sorter-cost:  920     Base: 2 2 2 2 2 2 2
c ---[2117]---> Sorter-cost: 1441     Base: 2 2 2 2 2 2 2
c ---[2115]---> Sorter-cost: 1441     Base: 2 2 2 2 2 2 2
c ---[2113]---> Sorter-cost:  602     Base: 2 2 2 2 2 2 2
c ---[2111]---> Sorter-cost:  433     Base: 2 2 2 2 2 2 2
c ---[2109]---> Sorter-cost:  602     Base: 2 2 2 2 2 2 2
c ---[2107]---> Sorter-cost:  433     Base: 2 2 2 2 2 2 2
c ---[2105]---> Sorter-cost:  602     Base: 2 2 2 2 2 2 2
c ---[2103]---> Sorter-cost:  602     Base: 2 2 2 2 2 2 2
c ---[2101]---> Sorter-cost:  602     Base: 2 2 2 2 2 2 2
c ---[2099]---> Sorter-cost:  602     Base: 2 2 2 2 2 2 2
c ---[2097]---> Sorter-cost:  280     Base: 2 2 2 2 2 2 2
c ---[2095]---> Sorter-cost:  280     Base: 2 2 2 2 2 2 2
c ---[2093]---> Adder-cost: 208   maxlim: 1785   bits: 12/11
c ---[2091]---> Sorter-cost: 1442     Base: 2 2 2 2 2 2 2
c ---[2089]---> Sorter-cost:  280     Base: 2 2 2 2 2 2 2
c ---[2087]---> Sorter-cost:  280     Base: 2 2 2 2 2 2 2
c ---[2085]---> Sorter-cost:  920     Base: 2 2 2 2 2 2 2
c ---[2083]---> Sorter-cost:  433     Base: 2 2 2 2 2 2 2
c ---[2081]---> Sorter-cost:  280     Base: 2 2 2 2 2 2 2
c ---[2079]---> Sorter-cost:  602     Base: 2 2 2 2 2 2 2
c ---[2077]---> Sorter-cost:  280     Base: 2 2 2 2 2 2 2
c ---[2075]---> Sorter-cost: 1637     Base: 2 2 2 2 2 2 2
c ---[2073]---> Sorter-cost: 1637     Base: 2 2 2 2 2 2 2
c ---[2071]---> Sorter-cost:  280     Base: 2 2 2 2 2 2 2
c ---[2069]---> Sorter-cost:  280     Base: 2 2 2 2 2 2 2
c ---[2067]---> Sorter-cost:  280     Base: 2 2 2 2 2 2 2
c ---[2065]---> Sorter-cost:  280     Base: 2 2 2 2 2 2 2
c ---[2063]---> Sorter-cost:  280     Base: 2 2 2 2 2 2 2
c ---[2061]---> Sorter-cost:  280     Base: 2 2 2 2 2 2 2
c ---[2059]---> Sorter-cost:  280     Base: 2 2 2 2 2 2 2
c ---[2057]---> BDD-cost:   64
c ---[2055]---> Adder-cost: 1040   maxlim: 8415   bits: 15/14
c ---[2053]---> Adder-cost: 896   maxlim: 8160   bits: 14/13
c ---[2051]---> Sorter-cost:  602     Base: 2 2 2 2 2 2 2
c ---[2049]---> Sorter-cost:  602     Base: 2 2 2 2 2 2 2
c ---[2047]---> Adder-cost: 544   maxlim: 4590   bits: 14/13
c ---[2045]---> Adder-cost: 528   maxlim: 4590   bits: 14/13
c ---[2043]---> Sorter-cost:  920     Base: 2 2 2 2 2 2 2
c ---[2041]---> Sorter-cost:  920     Base: 2 2 2 2 2 2 2
c ---[2039]---> Sorter-cost:  920     Base: 2 2 2 2 2 2 2
c ---[2037]---> Sorter-cost:  920     Base: 2 2 2 2 2 2 2
c ---[2035]---> Sorter-cost:  920     Base: 2 2 2 2 2 2 2
c ---[2033]---> Sorter-cost:  920     Base: 2 2 2 2 2 2 2
c ---[2031]---> Sorter-cost:  920     Base: 2 2 2 2 2 2 2
c ---[2029]---> Sorter-cost:  920     Base: 2 2 2 2 2 2 2
c ---[2027]---> Sorter-cost:  920     Base: 2 2 2 2 2 2 2
c ---[2025]---> Sorter-cost:  602     Base: 2 2 2 2 2 2 2
c ---[2023]---> Sorter-cost:  280     Base: 2 2 2 2 2 2 2
c ---[2021]---> Sorter-cost:  280     Base: 2 2 2 2 2 2 2
c ---[2019]---> Sorter-cost:  602     Base: 2 2 2 2 2 2 2
c ---[2017]---> Sorter-cost:  433     Base: 2 2 2 2 2 2 2
c ---[2015]---> Sorter-cost:  602     Base: 2 2 2 2 2 2 2
c ---[2013]---> Sorter-cost:  280     Base: 2 2 2 2 2 2 2
c ---[2011]---> Sorter-cost:  280     Base: 2 2 2 2 2 2 2
c ---[2009]---> Sorter-cost:  280     Base: 2 2 2 2 2 2 2
c ---[2007]---> Sorter-cost: 1441     Base: 2 2 2 2 2 2 2
c ---[2005]---> Sorter-cost: 1441     Base: 2 2 2 2 2 2 2
c ---[2003]---> Sorter-cost:  602     Base: 2 2 2 2 2 2 2
c ---[2001]---> Sorter-cost:  602     Base: 2 2 2 2 2 2 2
c ---[1999]---> Sorter-cost:  280     Base: 2 2 2 2 2 2 2
c ---[1997]---> Sorter-cost:  280     Base: 2 2 2 2 2 2 2
c ---[1995]---> Sorter-cost:  920     Base: 2 2 2 2 2 2 2
c ---[1993]---> Sorter-cost:  750     Base: 2 2 2 2 2 2 2
c ---[1991]---> Sorter-cost:  920     Base: 2 2 2 2 2 2 2
c ---[1989]---> Sorter-cost:  433     Base: 2 2 2 2 2 2 2
c ---[1987]---> Sorter-cost:  602     Base: 2 2 2 2 2 2 2
c ---[1985]---> Sorter-cost: 1893     Base: 2 2 2 2 2 2 2
c ---[1983]---> Sorter-cost:  920     Base: 2 2 2 2 2 2 2
c ---[1981]---> Adder-cost: 2736   maxlim: 22440   bits: 16/15
c ---[1979]---> Adder-cost: 2544   maxlim: 21930   bits: 16/15
c ---[1977]---> Sorter-cost: 1893     Base: 2 2 2 2 2 2 2
c ---[1975]---> Sorter-cost: 1638     Base: 2 2 2 2 2 2 2
c ---[1973]---> Sorter-cost:  602     Base: 2 2 2 2 2 2 2
c ---[1971]---> Sorter-cost:  602     Base: 2 2 2 2 2 2 2
c ---[1969]---> Sorter-cost: 1893     Base: 2 2 2 2 2 2 2
c ---[1967]---> Sorter-cost: 1441     Base: 2 2 2 2 2 2 2
c ---[1965]---> Sorter-cost:  602     Base: 2 2 2 2 2 2 2
c ---[1963]---> BDD-cost:   22
c ---[1961]---> Sorter-cost: 1893     Base: 2 2 2 2 2 2 2
c ---[1959]---> Sorter-cost: 1638     Base: 2 2 2 2 2 2 2
c ---[1957]---> Sorter-cost:  920     Base: 2 2 2 2 2 2 2
c ---[1955]---> Sorter-cost:  920     Base: 2 2 2 2 2 2 2
c ---[1953]---> Sorter-cost:  602     Base: 2 2 2 2 2 2 2
c ---[1951]---> Sorter-cost:  433     Base: 2 2 2 2 2 2 2
c ---[1949]---> Sorter-cost: 1441     Base: 2 2 2 2 2 2 2
c ---[1947]---> Sorter-cost: 1441     Base: 2 2 2 2 2 2 2
c ---[1945]---> Sorter-cost:  602     Base: 2 2 2 2 2 2 2
c ---[1943]---> Sorter-cost:  602     Base: 2 2 2 2 2 2 2
c ---[1941]---> Sorter-cost:  586     Base: 2 2 2 2 2 2 2
c ---[1939]---> Sorter-cost:  433     Base: 2 2 2 2 2 2 2
c ---[1937]---> Adder-cost: 720   maxlim: 5865   bits: 14/13
c ---[1935]---> Adder-cost: 608   maxlim: 5355   bits: 14/13
c ---[1933]---> Sorter-cost: 1893     Base: 2 2 2 2 2 2 2
c ---[1931]---> Sorter-cost: 1638     Base: 2 2 2 2 2 2 2
c ---[1929]---> Sorter-cost: 1637     Base: 2 2 2 2 2 2 2
c ---[1927]---> Sorter-cost: 1893     Base: 2 2 2 2 2 2 2
c ---[1925]---> Sorter-cost:  280     Base: 2 2 2 2 2 2 2
c ---[1923]---> BDD-cost:   64
c ---[1921]---> Sorter-cost:  280     Base: 2 2 2 2 2 2 2
c ---[1919]---> BDD-cost:   64
c ---[1917]---> Sorter-cost: 1893     Base: 2 2 2 2 2 2 2
c ---[1915]---> Sorter-cost: 1893     Base: 2 2 2 2 2 2 2
c ---[1913]---> Sorter-cost:  602     Base: 2 2 2 2 2 2 2
c ---[1911]---> BDD-cost:   64
c ---[1909]---> Sorter-cost:  920     Base: 2 2 2 2 2 2 2
c ---[1907]---> Sorter-cost:  601     Base: 2 2 2 2 2 2 2
c ---[1905]---> Sorter-cost:  280     Base: 2 2 2 2 2 2 2
c ---[1903]---> BDD-cost:   64
c ---[1901]---> Sorter-cost:  280     Base: 2 2 2 2 2 2 2
c ---[1899]---> BDD-cost:   64
c ---[1898]---> BDD-cost:   69
c ---[1897]---> BDD-cost:   68
c ---[1896]---> BDD-cost:   68
c ---[1895]---> Sorter-cost:  830     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1894]---> Sorter-cost:  826     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[1893]---> Sorter-cost:  826     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[1892]---> Sorter-cost: 1208     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1891]---> Sorter-cost: 1204     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[1890]---> Sorter-cost: 1204     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[1889]---> Adder-cost: 166   maxlim: 1529   bits: 12/11
c ---[1888]---> Adder-cost: 165   maxlim: 1529   bits: 12/11
c ---[1887]---> Adder-cost: 197   maxlim: 1529   bits: 12/11
c ---[1886]---> BDD-cost:   69
c ---[1885]---> BDD-cost:   68
c ---[1884]---> BDD-cost:   68
c ---[1883]---> BDD-cost:   69
c ---[1882]---> BDD-cost:   68
c ---[1881]---> BDD-cost:   68
c ---[1880]---> Sorter-cost:  450     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1879]---> Sorter-cost:  446     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[1878]---> Sorter-cost:  478     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[1877]---> BDD-cost:   69
c ---[1876]---> BDD-cost:   68
c ---[1875]---> BDD-cost:   68
c ---[1874]---> BDD-cost:   67
c ---[1873]---> BDD-cost:   68
c ---[1872]---> BDD-cost:   69
c ---[1871]---> BDD-cost:   68
c ---[1870]---> BDD-cost:   68
c ---[1869]---> BDD-cost:   69
c ---[1868]---> BDD-cost:   68
c ---[1867]---> BDD-cost:   68
c ---[1866]---> Sorter-cost:  480     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1865]---> Sorter-cost:  476     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[1864]---> Sorter-cost:  476     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[1863]---> Sorter-cost:  780     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1862]---> Sorter-cost:  776     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[1861]---> Sorter-cost:  808     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[1860]---> Sorter-cost:  402     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1859]---> BDD-cost:   66
c ---[1858]---> Sorter-cost:  478     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[1857]---> Sorter-cost: 1240     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1856]---> Sorter-cost:  778     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[1855]---> Sorter-cost: 1268     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[1854]---> BDD-cost:   69
c ---[1853]---> BDD-cost:   68
c ---[1852]---> Sorter-cost:  450     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1851]---> BDD-cost:   68
c ---[1850]---> Sorter-cost:  478     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[1849]---> BDD-cost:   67
c ---[1848]---> BDD-cost:   66
c ---[1847]---> BDD-cost:   68
c ---[1846]---> Sorter-cost:  670     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1845]---> Sorter-cost:  666     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[1844]---> Sorter-cost:  666     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[1843]---> BDD-cost:   69
c ---[1842]---> BDD-cost:   68
c ---[1841]---> Sorter-cost:  482     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1840]---> Sorter-cost:  478     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[1839]---> Sorter-cost:  780     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1838]---> Sorter-cost:  315     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[1837]---> Sorter-cost:  808     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[1836]---> Sorter-cost:  482     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1835]---> Sorter-cost:  478     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[1834]---> Sorter-cost:  478     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[1833]---> Sorter-cost:  828     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1832]---> Sorter-cost:  808     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[1831]---> Sorter-cost:  824     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[1830]---> Sorter-cost: 1718     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1829]---> Adder-cost: 167   maxlim: 1274   bits: 12/11
c ---[1828]---> Adder-cost: 167   maxlim: 1274   bits: 12/11
c ---[1827]---> Adder-cost: 198   maxlim: 1529   bits: 12/11
c ---[1826]---> Adder-cost: 181   maxlim: 1529   bits: 12/11
c ---[1825]---> Adder-cost: 163   maxlim: 1529   bits: 12/11
c ---[1824]---> Adder-cost: 242   maxlim: 2039   bits: 12/11
c ---[1823]---> Adder-cost: 215   maxlim: 1784   bits: 12/11
c ---[1822]---> Adder-cost: 257   maxlim: 2039   bits: 12/11
c ---[1821]---> Adder-cost: 263   maxlim: 2294   bits: 13/12
c ---[1820]---> Adder-cost: 223   maxlim: 2039   bits: 12/11
c ---[1819]---> Adder-cost: 246   maxlim: 2294   bits: 13/12
c ---[1818]---> Adder-cost: 277   maxlim: 2549   bits: 13/12
c ---[1817]---> Adder-cost: 262   maxlim: 2294   bits: 13/12
c ---[1816]---> Adder-cost: 292   maxlim: 2549   bits: 13/12
c ---[1815]---> Adder-cost: 307   maxlim: 3059   bits: 13/12
c ---[1814]---> Adder-cost: 310   maxlim: 2804   bits: 13/12
c ---[1813]---> Adder-cost: 306   maxlim: 3059   bits: 13/12
c ---[1812]---> Adder-cost: 357   maxlim: 3059   bits: 13/12
c ---[1811]---> Adder-cost: 344   maxlim: 2804   bits: 13/12
c ---[1810]---> Adder-cost: 356   maxlim: 3059   bits: 13/12
c ---[1809]---> Adder-cost: 327   maxlim: 3314   bits: 13/12
c ---[1808]---> Adder-cost: 322   maxlim: 3059   bits: 13/12
c ---[1807]---> Adder-cost: 342   maxlim: 3314   bits: 13/12
c ---[1806]---> Adder-cost: 355   maxlim: 3569   bits: 13/12
c ---[1805]---> Adder-cost: 294   maxlim: 3314   bits: 13/12
c ---[1804]---> Adder-cost: 354   maxlim: 3569   bits: 13/12
c ---[1803]---> Adder-cost: 409   maxlim: 3824   bits: 13/12
c ---[1802]---> Adder-cost: 390   maxlim: 3569   bits: 13/12
c ---[1801]---> Adder-cost: 440   maxlim: 3824   bits: 13/12
c ---[1800]---> Adder-cost: 433   maxlim: 4079   bits: 13/12
c ---[1799]---> Adder-cost: 432   maxlim: 4079   bits: 13/12
c ---[1798]---> Adder-cost: 408   maxlim: 4334   bits: 14/13
c ---[1797]---> Adder-cost: 332   maxlim: 3824   bits: 13/12
c ---[1796]---> Adder-cost: 423   maxlim: 4334   bits: 14/13
c ---[1795]---> BDD-cost:   67
c ---[1794]---> BDD-cost:   66
c ---[1793]---> BDD-cost:   68
c ---[1792]---> BDD-cost:   69
c ---[1791]---> BDD-cost:   68
c ---[1790]---> BDD-cost:   68
c ---[1789]---> BDD-cost:   67
c ---[1788]---> BDD-cost:   66
c ---[1787]---> BDD-cost:   68
c ---[1786]---> BDD-cost:   69
c ---[1785]---> BDD-cost:   68
c ---[1784]---> BDD-cost:   68
c ---[1783]---> Sorter-cost:  482     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1782]---> Sorter-cost:  478     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[1781]---> BDD-cost:   67
c ---[1780]---> BDD-cost:   66
c ---[1779]---> BDD-cost:   68
c ---[1778]---> BDD-cost:   68
c ---[1777]---> BDD-cost:   69
c ---[1776]---> BDD-cost:   66
c ---[1775]---> Sorter-cost:  476     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[1774]---> Sorter-cost:  482     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1773]---> Sorter-cost:  478     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[1772]---> Sorter-cost:  824     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[1771]---> Sorter-cost:  796     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1770]---> Sorter-cost:  792     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[1769]---> Sorter-cost: 1268     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[1768]---> Sorter-cost: 1240     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1767]---> Adder-cost: 167   maxlim: 1274   bits: 12/11
c ---[1766]---> Sorter-cost: 1670     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1765]---> Sorter-cost: 1603     Base: 2 2 2 2 2 2 2 7
c ---[1764]---> Adder-cost: 147   maxlim: 1529   bits: 12/11
c ---[1763]---> Adder-cost: 425   maxlim: 4589   bits: 14/13
c ---[1762]---> Adder-cost: 424   maxlim: 4589   bits: 14/13
c ---[1761]---> Adder-cost: 600   maxlim: 6629   bits: 14/13
c ---[1760]---> Adder-cost: 217   maxlim: 1274   bits: 12/11
c ---[1759]---> Adder-cost: 679   maxlim: 6885   bits: 14/13
c ---[1758]---> Adder-cost: 441   maxlim: 2039   bits: 12/11
c ---[1757]---> Adder-cost: 794   maxlim: 9434   bits: 15/14
c ---[1756]---> Adder-cost: 786   maxlim: 9434   bits: 15/14
c ---[1755]---> Adder-cost: 847   maxlim: 10709   bits: 15/14
c ---[1754]---> Adder-cost: 475   maxlim: 3059   bits: 13/12
c ---[1753]---> Adder-cost: 844   maxlim: 10709   bits: 15/14
c ---[1752]---> Adder-cost: 1299   maxlim: 12749   bits: 15/14
c ---[1751]---> Adder-cost: 635   maxlim: 4334   bits: 14/13
c ---[1750]---> Adder-cost: 1358   maxlim: 12877   bits: 15/14
c ---[1749]---> Adder-cost: 973   maxlim: 13004   bits: 15/14
c ---[1748]---> Adder-cost: 1128   maxlim: 13132   bits: 15/14
c ---[1747]---> Adder-cost: 607   maxlim: 4589   bits: 14/13
c ---[1746]---> Adder-cost: 915   maxlim: 14789   bits: 15/14
c ---[1745]---> Adder-cost: 961   maxlim: 14661   bits: 15/14
c ---[1744]---> Adder-cost: 1049   maxlim: 15044   bits: 15/14
c ---[1743]---> Adder-cost: 1213   maxlim: 14916   bits: 15/14
c ---[1742]---> Adder-cost: 1099   maxlim: 15299   bits: 15/14
c ---[1741]---> Adder-cost: 987   maxlim: 15171   bits: 15/14
c ---[1740]---> Adder-cost: 1588   maxlim: 17849   bits: 16/15
c ---[1739]---> Adder-cost: 1096   maxlim: 6629   bits: 14/13
c ---[1738]---> Adder-cost: 1706   maxlim: 17849   bits: 16/15
c ---[1737]---> Adder-cost: 1418   maxlim: 18104   bits: 16/15
c ---[1736]---> Adder-cost: 1404   maxlim: 18104   bits: 16/15
c ---[1735]---> Adder-cost: 1474   maxlim: 20399   bits: 16/15
c ---[1734]---> Adder-cost: 884   maxlim: 8414   bits: 15/14
c ---[1733]---> Adder-cost: 1698   maxlim: 20271   bits: 16/15
c ---[1732]---> Adder-cost: 1374   maxlim: 20654   bits: 16/15
c ---[1731]---> Adder-cost: 1588   maxlim: 20526   bits: 16/15
c ---[1730]---> Adder-cost: 1383   maxlim: 9434   bits: 15/14
c ---[1729]---> Adder-cost: 2168   maxlim: 21674   bits: 16/15
c ---[1728]---> Adder-cost: 2018   maxlim: 21546   bits: 16/15
c ---[1727]---> Adder-cost: 1238   maxlim: 21929   bits: 16/15
c ---[1726]---> Adder-cost: 1728   maxlim: 21801   bits: 16/15
c ---[1725]---> BDD-cost:   69
c ---[1724]---> BDD-cost:   68
c ---[1723]---> BDD-cost:   68
c ---[1722]---> Sorter-cost:  482     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1721]---> Sorter-cost:  478     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[1720]---> Sorter-cost:  478     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[1719]---> Sorter-cost:  826     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1718]---> Sorter-cost:  822     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[1717]---> Sorter-cost:  822     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[1716]---> Sorter-cost: 1272     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1715]---> Sorter-cost: 1268     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[1714]---> Sorter-cost: 1268     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[1713]---> Adder-cost: 150   maxlim: 1529   bits: 12/11
c ---[1712]---> Adder-cost: 165   maxlim: 1529   bits: 12/11
c ---[1711]---> Adder-cost: 197   maxlim: 1529   bits: 12/11
c ---[1710]---> Adder-cost: 182   maxlim: 1784   bits: 12/11
c ---[1709]---> Adder-cost: 181   maxlim: 1784   bits: 12/11
c ---[1708]---> Adder-cost: 181   maxlim: 1784   bits: 12/11
c ---[1707]---> BDD-cost:   67
c ---[1706]---> BDD-cost:   66
c ---[1705]---> BDD-cost:   68
c ---[1704]---> BDD-cost:   69
c ---[1703]---> BDD-cost:   68
c ---[1702]---> BDD-cost:   68
c ---[1701]---> BDD-cost:   69
c ---[1700]---> BDD-cost:   68
c ---[1699]---> BDD-cost:   68
c ---[1698]---> BDD-cost:   69
c ---[1697]---> BDD-cost:   68
c ---[1696]---> BDD-cost:   68
c ---[1695]---> Sorter-cost:  482     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1694]---> Sorter-cost:  478     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[1693]---> Sorter-cost:  478     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[1692]---> Sorter-cost:  780     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1691]---> Sorter-cost:  776     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[1690]---> Sorter-cost:  808     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[1689]---> BDD-cost:   69
c ---[1688]---> BDD-cost:   68
c ---[1687]---> BDD-cost:   68
c ---[1686]---> Sorter-cost:  464     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1685]---> Sorter-cost:  460     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[1684]---> Sorter-cost:  476     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[1683]---> Sorter-cost:  795     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1682]---> Sorter-cost:  791     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[1681]---> Sorter-cost:  791     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[1680]---> Sorter-cost: 1208     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1679]---> Sorter-cost: 1204     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[1678]---> Sorter-cost: 1204     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[1677]---> BDD-cost:   69
c ---[1676]---> BDD-cost:   68
c ---[1675]---> BDD-cost:   68
c ---[1674]---> Sorter-cost:  480     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1673]---> Sorter-cost:  460     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[1672]---> Sorter-cost:  476     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[1671]---> BDD-cost:   67
c ---[1670]---> BDD-cost:   68
c ---[1669]---> Sorter-cost:  466     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1668]---> BDD-cost:   68
c ---[1667]---> Sorter-cost:  476     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[1666]---> BDD-cost:   69
c ---[1665]---> BDD-cost:   68
c ---[1664]---> BDD-cost:   68
c ---[1663]---> BDD-cost:   67
c ---[1662]---> BDD-cost:   66
c ---[1661]---> BDD-cost:   68
c ---[1660]---> Sorter-cost:  466     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1659]---> Sorter-cost:  462     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[1658]---> Sorter-cost:  476     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[1657]---> BDD-cost:   69
c ---[1656]---> BDD-cost:   68
c ---[1655]---> BDD-cost:   68
c ---[1654]---> BDD-cost:   69
c ---[1653]---> BDD-cost:   68
c ---[1652]---> Sorter-cost:  480     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1651]---> Sorter-cost:  476     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[1650]---> Sorter-cost:  812     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1649]---> Sorter-cost:  298     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[1648]---> Sorter-cost:  808     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[1647]---> Sorter-cost: 1782     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1646]---> Sorter-cost:  742     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[1645]---> Adder-cost: 167   maxlim: 1274   bits: 12/11
c ---[1644]---> BDD-cost:   67
c ---[1643]---> BDD-cost:   66
c ---[1642]---> BDD-cost:   68
c ---[1641]---> BDD-cost:   69
c ---[1640]---> BDD-cost:   68
c ---[1639]---> Sorter-cost:  480     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1638]---> BDD-cost:   66
c ---[1637]---> Sorter-cost:  476     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[1636]---> BDD-cost:   66
c ---[1635]---> BDD-cost:   68
c ---[1634]---> BDD-cost:   69
c ---[1633]---> BDD-cost:   68
c ---[1632]---> Sorter-cost:  450     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1631]---> BDD-cost:   68
c ---[1630]---> Sorter-cost:  478     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[1629]---> Sorter-cost:  478     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[1628]---> BDD-cost:   67
c ---[1627]---> BDD-cost:   66
c ---[1626]---> Sorter-cost:  792     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[1625]---> Sorter-cost:  466     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1624]---> Sorter-cost:  462     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[1623]---> Sorter-cost: 1204     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[1622]---> Sorter-cost:  780     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1621]---> Sorter-cost:  776     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[1620]---> Adder-cost: 167   maxlim: 1274   bits: 12/11
c ---[1619]---> BDD-cost:   67
c ---[1618]---> BDD-cost:   66
c ---[1617]---> BDD-cost:   68
c ---[1616]---> BDD-cost:   69
c ---[1615]---> BDD-cost:   68
c ---[1614]---> BDD-cost:   68
c ---[1613]---> BDD-cost:   67
c ---[1612]---> BDD-cost:   66
c ---[1611]---> BDD-cost:   68
c ---[1610]---> BDD-cost:   69
c ---[1609]---> BDD-cost:   68
c ---[1608]---> BDD-cost:   69
c ---[1607]---> BDD-cost:   68
c ---[1606]---> BDD-cost:   68
c ---[1605]---> Sorter-cost:  478     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[1604]---> Sorter-cost:  478     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[1603]---> Sorter-cost:  671     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1602]---> Sorter-cost:  808     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[1601]---> Sorter-cost:  808     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[1600]---> Sorter-cost:  967     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1599]---> Sorter-cost: 1268     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[1598]---> Sorter-cost: 1268     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[1597]---> Sorter-cost: 1539     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1596]---> Adder-cost: 167   maxlim: 1274   bits: 12/11
c ---[1595]---> Adder-cost: 167   maxlim: 1274   bits: 12/11
c ---[1594]---> Adder-cost: 182   maxlim: 1529   bits: 12/11
c ---[1593]---> Adder-cost: 181   maxlim: 1529   bits: 12/11
c ---[1592]---> Adder-cost: 181   maxlim: 1529   bits: 12/11
c ---[1591]---> Adder-cost: 199   maxlim: 1784   bits: 12/11
c ---[1590]---> Adder-cost: 199   maxlim: 1784   bits: 12/11
c ---[1589]---> Adder-cost: 186   maxlim: 2039   bits: 12/11
c ---[1588]---> Adder-cost: 207   maxlim: 2039   bits: 12/11
c ---[1587]---> Adder-cost: 207   maxlim: 2039   bits: 12/11
c ---[1586]---> Adder-cost: 293   maxlim: 2549   bits: 13/12
c ---[1585]---> Adder-cost: 264   maxlim: 2549   bits: 13/12
c ---[1584]---> Adder-cost: 292   maxlim: 2549   bits: 13/12
c ---[1583]---> Adder-cost: 323   maxlim: 3059   bits: 13/12
c ---[1582]---> Adder-cost: 338   maxlim: 3059   bits: 13/12
c ---[1581]---> Adder-cost: 359   maxlim: 3314   bits: 13/12
c ---[1580]---> Adder-cost: 374   maxlim: 3314   bits: 13/12
c ---[1579]---> Adder-cost: 293   maxlim: 3569   bits: 13/12
c ---[1578]---> Adder-cost: 310   maxlim: 3569   bits: 13/12
c ---[1577]---> Adder-cost: 421   maxlim: 3824   bits: 13/12
c ---[1576]---> Adder-cost: 374   maxlim: 3824   bits: 13/12
c ---[1575]---> Adder-cost: 404   maxlim: 3824   bits: 13/12
c ---[1574]---> Adder-cost: 394   maxlim: 4334   bits: 14/13
c ---[1573]---> Adder-cost: 368   maxlim: 4334   bits: 14/13
c ---[1572]---> Adder-cost: 393   maxlim: 4334   bits: 14/13
c ---[1571]---> Adder-cost: 420   maxlim: 4589   bits: 14/13
c ---[1570]---> Adder-cost: 457   maxlim: 4844   bits: 14/13
c ---[1569]---> Adder-cost: 517   maxlim: 4844   bits: 14/13
c ---[1568]---> Adder-cost: 434   maxlim: 5099   bits: 14/13
c ---[1567]---> Adder-cost: 483   maxlim: 5099   bits: 14/13
c ---[1566]---> Adder-cost: 543   maxlim: 5099   bits: 14/13
c ---[1565]---> Adder-cost: 508   maxlim: 5354   bits: 14/13
c ---[1564]---> Adder-cost: 453   maxlim: 5354   bits: 14/13
c ---[1563]---> Adder-cost: 495   maxlim: 5354   bits: 14/13
c ---[1562]---> Adder-cost: 457   maxlim: 5864   bits: 14/13
c ---[1561]---> Adder-cost: 563   maxlim: 5864   bits: 14/13
c ---[1560]---> Adder-cost: 588   maxlim: 6374   bits: 14/13
c ---[1559]---> Adder-cost: 535   maxlim: 6374   bits: 14/13
c ---[1558]---> Adder-cost: 615   maxlim: 6374   bits: 14/13
c ---[1557]---> Adder-cost: 654   maxlim: 6629   bits: 14/13
c ---[1556]---> Adder-cost: 541   maxlim: 6629   bits: 14/13
c ---[1555]---> Adder-cost: 763   maxlim: 6629   bits: 14/13
c ---[1554]---> Adder-cost: 740   maxlim: 6884   bits: 14/13
c ---[1553]---> Adder-cost: 579   maxlim: 6884   bits: 14/13
c ---[1552]---> Adder-cost: 669   maxlim: 6884   bits: 14/13
c ---[1551]---> Adder-cost: 684   maxlim: 7139   bits: 14/13
c ---[1550]---> Adder-cost: 549   maxlim: 7139   bits: 14/13
c ---[1549]---> Adder-cost: 633   maxlim: 7139   bits: 14/13
c ---[1548]---> Adder-cost: 644   maxlim: 7394   bits: 14/13
c ---[1547]---> Adder-cost: 483   maxlim: 7394   bits: 14/13
c ---[1546]---> Adder-cost: 599   maxlim: 7394   bits: 14/13
c ---[1545]---> Adder-cost: 794   maxlim: 7649   bits: 14/13
c ---[1544]---> Adder-cost: 799   maxlim: 7649   bits: 14/13
c ---[1543]---> BDD-cost:   69
c ---[1542]---> BDD-cost:   68
c ---[1541]---> BDD-cost:   68
c ---[1540]---> Sorter-cost:  466     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1539]---> Sorter-cost:  462     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[1538]---> Sorter-cost:  478     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[1537]---> BDD-cost:   69
c ---[1536]---> BDD-cost:   68
c ---[1535]---> Sorter-cost:  830     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1534]---> Sorter-cost:  478     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[1533]---> Sorter-cost:  826     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[1532]---> Sorter-cost: 1288     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1531]---> Sorter-cost:  808     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[1530]---> Sorter-cost: 1284     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[1529]---> Sorter-cost: 1766     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1528]---> Sorter-cost: 1284     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[1527]---> Adder-cost: 167   maxlim: 1274   bits: 12/11
c ---[1526]---> Adder-cost: 232   maxlim: 1784   bits: 12/11
c ---[1525]---> Adder-cost: 197   maxlim: 1529   bits: 12/11
c ---[1524]---> Adder-cost: 215   maxlim: 1784   bits: 12/11
c ---[1523]---> Adder-cost: 208   maxlim: 2039   bits: 12/11
c ---[1522]---> Adder-cost: 183   maxlim: 1784   bits: 12/11
c ---[1521]---> Adder-cost: 225   maxlim: 2039   bits: 12/11
c ---[1520]---> Adder-cost: 215   maxlim: 2294   bits: 13/12
c ---[1519]---> Adder-cost: 187   maxlim: 2039   bits: 12/11
c ---[1518]---> Adder-cost: 230   maxlim: 2294   bits: 13/12
c ---[1517]---> Adder-cost: 265   maxlim: 2549   bits: 13/12
c ---[1516]---> Adder-cost: 248   maxlim: 2294   bits: 13/12
c ---[1515]---> Adder-cost: 264   maxlim: 2549   bits: 13/12
c ---[1514]---> Adder-cost: 307   maxlim: 3059   bits: 13/12
c ---[1513]---> Adder-cost: 262   maxlim: 2804   bits: 13/12
c ---[1512]---> Adder-cost: 322   maxlim: 3059   bits: 13/12
c ---[1511]---> Adder-cost: 343   maxlim: 3314   bits: 13/12
c ---[1510]---> Adder-cost: 306   maxlim: 3059   bits: 13/12
c ---[1509]---> Adder-cost: 326   maxlim: 3314   bits: 13/12
c ---[1508]---> Adder-cost: 315   maxlim: 3569   bits: 13/12
c ---[1507]---> Adder-cost: 304   maxlim: 3314   bits: 13/12
c ---[1506]---> Adder-cost: 314   maxlim: 3569   bits: 13/12
c ---[1505]---> Adder-cost: 335   maxlim: 3824   bits: 13/12
c ---[1504]---> Adder-cost: 308   maxlim: 3569   bits: 13/12
c ---[1503]---> Adder-cost: 330   maxlim: 3824   bits: 13/12
c ---[1502]---> Adder-cost: 356   maxlim: 4079   bits: 13/12
c ---[1501]---> Adder-cost: 364   maxlim: 3824   bits: 13/12
c ---[1500]---> Adder-cost: 383   maxlim: 4079   bits: 13/12
c ---[1499]---> BDD-cost:   69
c ---[1498]---> BDD-cost:   68
c ---[1497]---> BDD-cost:   68
c ---[1496]---> Sorter-cost:  480     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1495]---> Sorter-cost:  476     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[1494]---> Sorter-cost:  476     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[1493]---> Sorter-cost:  732     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1492]---> Sorter-cost:  728     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[1491]---> Sorter-cost:  808     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[1490]---> BDD-cost:   67
c ---[1489]---> BDD-cost:   66
c ---[1488]---> BDD-cost:   68
c ---[1487]---> Sorter-cost:  466     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1486]---> Sorter-cost:  462     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[1485]---> Sorter-cost:  476     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[1484]---> BDD-cost:   69
c ---[1483]---> BDD-cost:   68
c ---[1482]---> BDD-cost:   68
c ---[1481]---> Sorter-cost:  464     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1480]---> Sorter-cost:  460     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[1479]---> Sorter-cost:  476     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[1478]---> Sorter-cost:  780     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1477]---> Sorter-cost:  776     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[1476]---> Sorter-cost:  792     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[1475]---> BDD-cost:   67
c ---[1474]---> BDD-cost:   66
c ---[1473]---> BDD-cost:   68
c ---[1472]---> Sorter-cost:  466     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1471]---> Sorter-cost:  462     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[1470]---> Sorter-cost:  476     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[1469]---> Sorter-cost:  812     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1468]---> Sorter-cost:  808     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[1467]---> Sorter-cost:  808     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[1466]---> BDD-cost:   69
c ---[1465]---> BDD-cost:   68
c ---[1464]---> BDD-cost:   68
c ---[1463]---> Sorter-cost:  466     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1462]---> Sorter-cost:  462     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[1461]---> Sorter-cost:  478     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[1460]---> BDD-cost:   67
c ---[1459]---> BDD-cost:   66
c ---[1458]---> BDD-cost:   68
c ---[1457]---> Sorter-cost:  466     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1456]---> Sorter-cost:  314     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[1455]---> Sorter-cost:  478     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[1454]---> BDD-cost:   67
c ---[1453]---> BDD-cost:   68
c ---[1452]---> Sorter-cost:  466     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1451]---> BDD-cost:   68
c ---[1450]---> Sorter-cost:  476     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[1449]---> BDD-cost:   67
c ---[1448]---> BDD-cost:   66
c ---[1447]---> BDD-cost:   68
c ---[1446]---> BDD-cost:   69
c ---[1445]---> BDD-cost:   68
c ---[1444]---> BDD-cost:   68
c ---[1443]---> Sorter-cost:  482     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1442]---> Sorter-cost:  478     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[1441]---> Sorter-cost:  478     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[1440]---> Sorter-cost:  812     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1439]---> Sorter-cost:  808     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[1438]---> Sorter-cost:  808     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[1437]---> Sorter-cost: 1192     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1436]---> Sorter-cost: 1188     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[1435]---> Sorter-cost: 1284     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[1434]---> BDD-cost:   69
c ---[1433]---> BDD-cost:   68
c ---[1432]---> BDD-cost:   68
c ---[1431]---> Sorter-cost:  466     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1430]---> Sorter-cost:  462     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[1429]---> Sorter-cost:  478     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[1428]---> BDD-cost:   67
c ---[1427]---> BDD-cost:   66
c ---[1426]---> BDD-cost:   68
c ---[1425]---> BDD-cost:   69
c ---[1424]---> BDD-cost:   68
c ---[1423]---> Sorter-cost:  466     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1422]---> Sorter-cost:  478     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[1421]---> Sorter-cost:  780     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1420]---> Sorter-cost:  808     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[1419]---> Sorter-cost:  478     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[1418]---> Sorter-cost:  478     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[1417]---> BDD-cost:   69
c ---[1416]---> Sorter-cost:  776     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[1415]---> Sorter-cost:  824     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[1414]---> BDD-cost:   68
c ---[1413]---> BDD-cost:   68
c ---[1412]---> BDD-cost:   67
c ---[1411]---> Sorter-cost:  462     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[1410]---> Sorter-cost:  478     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[1409]---> Sorter-cost:  466     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1408]---> Sorter-cost:  478     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[1407]---> Sorter-cost:  780     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1406]---> Sorter-cost:  447     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[1405]---> Sorter-cost:  808     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[1404]---> Sorter-cost: 1192     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1403]---> Sorter-cost:  726     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[1402]---> Sorter-cost: 1252     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[1401]---> Sorter-cost: 1762     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1400]---> Adder-cost: 167   maxlim: 1274   bits: 12/11
c ---[1399]---> Adder-cost: 186   maxlim: 2294   bits: 13/12
c ---[1398]---> Adder-cost: 197   maxlim: 2549   bits: 13/12
c ---[1397]---> Adder-cost: 202   maxlim: 2549   bits: 13/12
c ---[1396]---> BDD-cost:   68
c ---[1395]---> Adder-cost: 215   maxlim: 2804   bits: 13/12
c ---[1394]---> Adder-cost: 234   maxlim: 2804   bits: 13/12
c ---[1393]---> Sorter-cost:  478     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[1392]---> Adder-cost: 241   maxlim: 3059   bits: 13/12
c ---[1391]---> Adder-cost: 389   maxlim: 3059   bits: 13/12
c ---[1390]---> Adder-cost: 216   maxlim: 764   bits: 11/10
c ---[1389]---> Adder-cost: 410   maxlim: 3314   bits: 13/12
c ---[1388]---> Adder-cost: 395   maxlim: 3569   bits: 13/12
c ---[1387]---> Adder-cost: 257   maxlim: 1274   bits: 12/11
c ---[1386]---> Adder-cost: 422   maxlim: 3824   bits: 13/12
c ---[1385]---> Adder-cost: 524   maxlim: 4844   bits: 14/13
c ---[1384]---> Adder-cost: 360   maxlim: 2549   bits: 13/12
c ---[1383]---> Adder-cost: 553   maxlim: 5099   bits: 14/13
c ---[1382]---> Adder-cost: 620   maxlim: 6629   bits: 14/13
c ---[1381]---> Adder-cost: 458   maxlim: 4079   bits: 13/12
c ---[1380]---> Adder-cost: 601   maxlim: 6884   bits: 14/13
c ---[1379]---> Adder-cost: 566   maxlim: 6884   bits: 14/13
c ---[1378]---> Adder-cost: 400   maxlim: 4334   bits: 14/13
c ---[1377]---> Adder-cost: 565   maxlim: 7395   bits: 14/13
c ---[1376]---> Adder-cost: 708   maxlim: 7139   bits: 14/13
c ---[1375]---> Adder-cost: 583   maxlim: 4589   bits: 14/13
c ---[1374]---> Adder-cost: 763   maxlim: 7650   bits: 14/13
c ---[1373]---> Adder-cost: 824   maxlim: 8924   bits: 15/14
c ---[1372]---> Adder-cost: 761   maxlim: 6629   bits: 14/13
c ---[1371]---> Adder-cost: 844   maxlim: 9435   bits: 15/14
c ---[1370]---> Adder-cost: 816   maxlim: 9179   bits: 15/14
c ---[1369]---> Adder-cost: 711   maxlim: 6884   bits: 14/13
c ---[1368]---> Adder-cost: 852   maxlim: 9690   bits: 15/14
c ---[1367]---> Adder-cost: 742   maxlim: 9434   bits: 15/14
c ---[1366]---> Adder-cost: 673   maxlim: 7139   bits: 14/13
c ---[1365]---> Adder-cost: 850   maxlim: 9945   bits: 15/14
c ---[1364]---> Adder-cost: 759   maxlim: 9689   bits: 15/14
c ---[1363]---> Adder-cost: 661   maxlim: 7394   bits: 14/13
c ---[1362]---> Adder-cost: 782   maxlim: 10200   bits: 15/14
c ---[1361]---> Adder-cost: 749   maxlim: 9944   bits: 15/14
c ---[1360]---> Adder-cost: 599   maxlim: 7649   bits: 14/13
c ---[1359]---> Adder-cost: 716   maxlim: 10455   bits: 15/14
c ---[1358]---> Adder-cost: 671   maxlim: 9944   bits: 15/14
c ---[1357]---> Adder-cost: 799   maxlim: 7904   bits: 14/13
c ---[1356]---> Adder-cost: 686   maxlim: 10455   bits: 15/14
c ---[1355]---> Adder-cost: 923   maxlim: 10964   bits: 15/14
c ---[1354]---> Adder-cost: 762   maxlim: 8924   bits: 15/14
c ---[1353]---> Adder-cost: 938   maxlim: 11475   bits: 15/14
c ---[1352]---> Adder-cost: 1005   maxlim: 11729   bits: 15/14
c ---[1351]---> Adder-cost: 888   maxlim: 9689   bits: 15/14
c ---[1350]---> Adder-cost: 1024   maxlim: 12112   bits: 15/14
c ---[1349]---> Adder-cost: 933   maxlim: 11984   bits: 15/14
c ---[1348]---> Adder-cost: 854   maxlim: 9944   bits: 15/14
c ---[1347]---> Adder-cost: 922   maxlim: 12367   bits: 15/14
c ---[1346]---> Adder-cost: 1087   maxlim: 12749   bits: 15/14
c ---[1345]---> Adder-cost: 962   maxlim: 10709   bits: 15/14
c ---[1344]---> Adder-cost: 1132   maxlim: 13132   bits: 15/14
c ---[1343]---> Adder-cost: 1027   maxlim: 13004   bits: 15/14
c ---[1342]---> Adder-cost: 928   maxlim: 10964   bits: 15/14
c ---[1341]---> Adder-cost: 1020   maxlim: 13387   bits: 15/14
c ---[1340]---> Adder-cost: 1221   maxlim: 13259   bits: 15/14
c ---[1339]---> Adder-cost: 1084   maxlim: 11219   bits: 15/14
c ---[1338]---> Adder-cost: 1235   maxlim: 13642   bits: 15/14
c ---[1337]---> Adder-cost: 697   maxlim: 13259   bits: 15/14
c ---[1336]---> Adder-cost: 642   maxlim: 11219   bits: 15/14
c ---[1335]---> Adder-cost: 707   maxlim: 13642   bits: 15/14
c ---[1334]---> Adder-cost: 1131   maxlim: 14279   bits: 15/14
c ---[1333]---> Adder-cost: 1058   maxlim: 12239   bits: 15/14
c ---[1332]---> Adder-cost: 1161   maxlim: 14662   bits: 15/14
c ---[1331]---> Adder-cost: 1267   maxlim: 14279   bits: 15/14
c ---[1330]---> Adder-cost: 1323   maxlim: 14662   bits: 15/14
c ---[1329]---> Adder-cost: 1091   maxlim: 14789   bits: 15/14
c ---[1328]---> Adder-cost: 982   maxlim: 12494   bits: 15/14
c ---[1327]---> Adder-cost: 1141   maxlim: 15427   bits: 15/14
c ---[1326]---> Adder-cost: 1163   maxlim: 15044   bits: 15/14
c ---[1325]---> Adder-cost: 1153   maxlim: 12749   bits: 15/14
c ---[1324]---> Adder-cost: 1263   maxlim: 15682   bits: 15/14
c ---[1323]---> Adder-cost: 1283   maxlim: 15044   bits: 15/14
c ---[1322]---> Adder-cost: 1211   maxlim: 12749   bits: 15/14
c ---[1321]---> Adder-cost: 1309   maxlim: 15682   bits: 15/14
c ---[1320]---> Adder-cost: 1237   maxlim: 15809   bits: 15/14
c ---[1319]---> Adder-cost: 1295   maxlim: 13514   bits: 15/14
c ---[1318]---> Adder-cost: 1450   maxlim: 16447   bits: 16/15
c ---[1317]---> Adder-cost: 1316   maxlim: 16957   bits: 16/15
c ---[1316]---> Adder-cost: 1288   maxlim: 16574   bits: 16/15
c ---[1315]---> Adder-cost: 1193   maxlim: 14279   bits: 15/14
c ---[1314]---> Adder-cost: 1196   maxlim: 17340   bits: 16/15
c ---[1313]---> Adder-cost: 1320   maxlim: 17084   bits: 16/15
c ---[1312]---> Adder-cost: 1109   maxlim: 14789   bits: 15/14
c ---[1311]---> Adder-cost: 1220   maxlim: 17594   bits: 16/15
c ---[1310]---> Adder-cost: 1342   maxlim: 17339   bits: 16/15
c ---[1309]---> Adder-cost: 1293   maxlim: 15044   bits: 15/14
c ---[1308]---> Adder-cost: 1504   maxlim: 17849   bits: 16/15
c ---[1307]---> Adder-cost: 1564   maxlim: 18104   bits: 16/15
c ---[1306]---> Adder-cost: 1407   maxlim: 15809   bits: 15/14
c ---[1305]---> Adder-cost: 1628   maxlim: 18614   bits: 16/15
c ---[1304]---> Adder-cost: 1512   maxlim: 18359   bits: 16/15
c ---[1303]---> Adder-cost: 1512   maxlim: 19124   bits: 16/15
c ---[1302]---> Adder-cost: 1464   maxlim: 16829   bits: 16/15
c ---[1301]---> Adder-cost: 1612   maxlim: 19634   bits: 16/15
c ---[1300]---> Adder-cost: 1250   maxlim: 17339   bits: 16/15
c ---[1299]---> Adder-cost: 1626   maxlim: 20144   bits: 16/15
c ---[1298]---> Adder-cost: 1468   maxlim: 19634   bits: 16/15
c ---[1297]---> Adder-cost: 718   maxlim: 17339   bits: 16/15
c ---[1296]---> Adder-cost: 736   maxlim: 20144   bits: 16/15
c ---[1295]---> Adder-cost: 1500   maxlim: 19889   bits: 16/15
c ---[1294]---> Adder-cost: 1454   maxlim: 17594   bits: 16/15
c ---[1293]---> Adder-cost: 1654   maxlim: 20399   bits: 16/15
c ---[1292]---> Adder-cost: 1736   maxlim: 19889   bits: 16/15
c ---[1291]---> Adder-cost: 1664   maxlim: 17594   bits: 16/15
c ---[1290]---> Adder-cost: 1808   maxlim: 20399   bits: 16/15
c ---[1289]---> Adder-cost: 1728   maxlim: 21419   bits: 16/15
c ---[1288]---> Adder-cost: 1614   maxlim: 19124   bits: 16/15
c ---[1287]---> Adder-cost: 1836   maxlim: 21929   bits: 16/15
c ---[1286]---> Adder-cost: 1662   maxlim: 22184   bits: 16/15
c ---[1285]---> Adder-cost: 1560   maxlim: 19634   bits: 16/15
c ---[1284]---> Adder-cost: 2100   maxlim: 22694   bits: 16/15
c ---[1283]---> BDD-cost:   69
c ---[1282]---> BDD-cost:   68
c ---[1281]---> BDD-cost:   68
c ---[1280]---> Sorter-cost:  482     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1279]---> Sorter-cost:  478     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[1278]---> Sorter-cost:  478     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[1277]---> Sorter-cost:  826     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1276]---> Sorter-cost:  806     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[1275]---> Sorter-cost:  822     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[1274]---> Sorter-cost: 1489     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1273]---> Sorter-cost: 1204     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[1272]---> Sorter-cost: 1699     Base: 2 2 2 2 2 2 2 7
c ---[1271]---> BDD-cost:   67
c ---[1270]---> BDD-cost:   66
c ---[1269]---> BDD-cost:   68
c ---[1268]---> Sorter-cost:  450     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1267]---> Sorter-cost:  446     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[1266]---> Sorter-cost:  476     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[1265]---> BDD-cost:   69
c ---[1264]---> BDD-cost:   68
c ---[1263]---> Sorter-cost:  315     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[1262]---> Sorter-cost:  814     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1261]---> Sorter-cost:  826     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[1260]---> BDD-cost:   69
c ---[1259]---> BDD-cost:   68
c ---[1258]---> Sorter-cost:  466     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1257]---> Sorter-cost:  478     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[1256]---> BDD-cost:   69
c ---[1255]---> BDD-cost:   68
c ---[1254]---> BDD-cost:   68
c ---[1253]---> Sorter-cost:  482     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1252]---> Sorter-cost:  478     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[1251]---> Sorter-cost:  478     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[1250]---> Sorter-cost:  812     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1249]---> Sorter-cost:  808     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[1248]---> Sorter-cost:  824     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[1247]---> Sorter-cost: 1208     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1246]---> Sorter-cost: 1204     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[1245]---> Sorter-cost: 1284     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[1244]---> Sorter-cost: 2008     Base: 2 2 2 2 2 2 2 7 3
c ---[1243]---> Sorter-cost: 1698     Base: 2 2 2 2 2 2 2 7
c ---[1242]---> Adder-cost: 185   maxlim: 1274   bits: 12/11
c ---[1241]---> BDD-cost:   69
c ---[1240]---> BDD-cost:   68
c ---[1239]---> BDD-cost:   68
c ---[1238]---> Sorter-cost:  464     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1237]---> Sorter-cost:  460     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[1236]---> Sorter-cost:  476     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[1235]---> BDD-cost:   69
c ---[1234]---> BDD-cost:   66
c ---[1233]---> BDD-cost:   68
c ---[1232]---> BDD-cost:   69
c ---[1231]---> BDD-cost:   68
c ---[1230]---> BDD-cost:   68
c ---[1229]---> Sorter-cost:  480     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1228]---> Sorter-cost:  476     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[1227]---> Sorter-cost:  476     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[1226]---> Sorter-cost:  780     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1225]---> Sorter-cost:  776     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[1224]---> Sorter-cost:  792     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[1223]---> BDD-cost:   67
c ---[1222]---> BDD-cost:   66
c ---[1221]---> BDD-cost:   68
c ---[1220]---> Sorter-cost:  466     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1219]---> Sorter-cost:  462     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[1218]---> Sorter-cost:  476     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[1217]---> BDD-cost:   66
c ---[1216]---> BDD-cost:   68
c ---[1215]---> Sorter-cost:  302     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1214]---> Sorter-cost:  476     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[1213]---> BDD-cost:   69
c ---[1212]---> BDD-cost:   68
c ---[1211]---> Sorter-cost:  482     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1210]---> Sorter-cost:  478     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[1209]---> Sorter-cost:  812     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1208]---> Sorter-cost:  479     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[1207]---> Sorter-cost:  808     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[1206]---> Sorter-cost: 1208     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1205]---> Sorter-cost:  791     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[1204]---> Sorter-cost: 1204     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[1203]---> Sorter-cost: 1718     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1202]---> Sorter-cost: 1286     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[1201]---> Adder-cost: 167   maxlim: 1274   bits: 12/11
c ---[1200]---> Adder-cost: 198   maxlim: 1529   bits: 12/11
c ---[1199]---> Adder-cost: 165   maxlim: 1019   bits: 11/10
c ---[1198]---> Adder-cost: 163   maxlim: 1529   bits: 12/11
c ---[1197]---> Adder-cost: 150   maxlim: 1529   bits: 12/11
c ---[1196]---> Adder-cost: 117   maxlim: 1019   bits: 11/10
c ---[1195]---> Adder-cost: 165   maxlim: 1529   bits: 12/11
c ---[1194]---> Adder-cost: 198   maxlim: 1784   bits: 12/11
c ---[1193]---> Adder-cost: 181   maxlim: 1274   bits: 12/11
c ---[1192]---> Adder-cost: 197   maxlim: 1784   bits: 12/11
c ---[1191]---> Adder-cost: 224   maxlim: 2039   bits: 12/11
c ---[1190]---> Adder-cost: 207   maxlim: 2039   bits: 12/11
c ---[1189]---> Adder-cost: 265   maxlim: 2294   bits: 13/12
c ---[1188]---> Adder-cost: 217   maxlim: 1784   bits: 12/11
c ---[1187]---> Adder-cost: 264   maxlim: 2294   bits: 13/12
c ---[1186]---> Adder-cost: 245   maxlim: 2549   bits: 13/12
c ---[1185]---> Adder-cost: 226   maxlim: 2039   bits: 12/11
c ---[1184]---> Adder-cost: 260   maxlim: 2549   bits: 13/12
c ---[1183]---> Adder-cost: 313   maxlim: 2804   bits: 13/12
c ---[1182]---> Adder-cost: 266   maxlim: 2294   bits: 13/12
c ---[1181]---> Adder-cost: 312   maxlim: 2804   bits: 13/12
c ---[1180]---> Adder-cost: 303   maxlim: 3059   bits: 13/12
c ---[1179]---> Adder-cost: 260   maxlim: 2549   bits: 13/12
c ---[1178]---> Adder-cost: 302   maxlim: 3059   bits: 13/12
c ---[1177]---> Adder-cost: 345   maxlim: 3314   bits: 13/12
c ---[1176]---> Adder-cost: 298   maxlim: 2804   bits: 13/12
c ---[1175]---> Adder-cost: 344   maxlim: 3314   bits: 13/12
c ---[1174]---> Adder-cost: 389   maxlim: 3824   bits: 13/12
c ---[1173]---> Adder-cost: 374   maxlim: 3314   bits: 13/12
c ---[1172]---> Adder-cost: 404   maxlim: 3824   bits: 13/12
c ---[1171]---> Adder-cost: 459   maxlim: 3824   bits: 13/12
c ---[1170]---> Adder-cost: 474   maxlim: 3824   bits: 13/12
c ---[1169]---> Adder-cost: 342   maxlim: 4334   bits: 14/13
c ---[1168]---> Adder-cost: 354   maxlim: 3824   bits: 13/12
c ---[1167]---> Adder-cost: 357   maxlim: 4334   bits: 14/13
c ---[1166]---> BDD-cost:   67
c ---[1165]---> BDD-cost:   68
c ---[1164]---> BDD-cost:   68
c ---[1163]---> Sorter-cost:  466     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1162]---> Sorter-cost:  476     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[1161]---> Sorter-cost:  476     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[1160]---> Sorter-cost:  812     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1159]---> Sorter-cost:  824     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[1158]---> Sorter-cost: 1208     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1157]---> Sorter-cost:  979     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[1156]---> Sorter-cost: 1268     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[1155]---> BDD-cost:   69
c ---[1154]---> BDD-cost:   68
c ---[1153]---> BDD-cost:   68
c ---[1152]---> Sorter-cost:  480     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1151]---> Sorter-cost:  476     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[1150]---> Sorter-cost:  476     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[1149]---> Sorter-cost: 1272     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1148]---> Sorter-cost: 1268     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[1147]---> Sorter-cost: 1300     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[1146]---> Sorter-cost: 1698     Base: 2 2 2 2 2 2 2 7
c ---[1145]---> Adder-cost: 167   maxlim: 1274   bits: 12/11
c ---[1144]---> BDD-cost:   69
c ---[1143]---> BDD-cost:   68
c ---[1142]---> BDD-cost:   67
c ---[1141]---> BDD-cost:   66
c ---[1140]---> BDD-cost:   68
c ---[1139]---> BDD-cost:   67
c ---[1138]---> BDD-cost:   66
c ---[1137]---> BDD-cost:   68
c ---[1136]---> Sorter-cost:  450     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1135]---> Sorter-cost:  446     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[1134]---> Sorter-cost:  476     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[1133]---> Sorter-cost: 1192     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1132]---> Sorter-cost: 1188     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[1131]---> Sorter-cost: 1268     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[1130]---> BDD-cost:   69
c ---[1129]---> BDD-cost:   68
c ---[1128]---> Sorter-cost:  466     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1127]---> Sorter-cost:  478     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[1126]---> BDD-cost:   69
c ---[1125]---> BDD-cost:   68
c ---[1124]---> BDD-cost:   68
c ---[1123]---> Sorter-cost:  750     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1122]---> Sorter-cost:  587     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[1121]---> Sorter-cost:  826     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[1120]---> BDD-cost:   69
c ---[1119]---> BDD-cost:   68
c ---[1118]---> BDD-cost:   68
c ---[1117]---> BDD-cost:   67
c ---[1116]---> BDD-cost:   68
c ---[1114]---> BDD-cost:   35
c ---[1112]---> BDD-cost:   35
c ---[1110]---> BDD-cost:   35
c ---[1108]---> BDD-cost:   35
c ---[1106]---> BDD-cost:   76
c ---[1104]---> BDD-cost:   76
c ---[1102]---> BDD-cost:   76
c ---[1100]---> BDD-cost:   76
c ---[1098]---> BDD-cost:   76
c ---[1096]---> BDD-cost:   76
c ---[1094]---> BDD-cost:   76
c ---[1092]---> BDD-cost:   76
c ---[1090]---> BDD-cost:   76
c ---[1088]---> BDD-cost:   76
c ---[1086]---> BDD-cost:   76
c ---[1084]---> BDD-cost:   76
c ---[1082]---> BDD-cost:   76
c ---[1080]---> BDD-cost:   76
c ---[1078]---> BDD-cost:   76
c ---[1076]---> BDD-cost:   76
c ---[1074]---> BDD-cost:   76
c ---[1072]---> BDD-cost:   76
c ---[1070]---> BDD-cost:   76
c ---[1068]---> BDD-cost:   76
c ---[1066]---> BDD-cost:   76
c ---[1064]---> BDD-cost:   76
c ---[1062]---> BDD-cost:   76
c ---[1060]---> BDD-cost:   76
c ---[1058]---> BDD-cost:   76
c ---[1056]---> BDD-cost:   76
c ---[1054]---> BDD-cost:   35
c ---[1052]---> BDD-cost:   76
c ---[1050]---> BDD-cost:   76
c ---[1048]---> BDD-cost:   76
c ---[1046]---> BDD-cost:   76
c ---[1044]---> BDD-cost:   76
c ---[1042]---> BDD-cost:   76
c ---[1040]---> BDD-cost:   76
c ---[1038]---> BDD-cost:   76
c ---[1036]---> BDD-cost:   76
c ---[1034]---> BDD-cost:   76
c ---[1032]---> BDD-cost:   76
c ---[1030]---> BDD-cost:   76
c ---[1028]---> BDD-cost:   76
c ---[1026]---> BDD-cost:   76
c ---[1024]---> BDD-cost:   76
c ---[1022]---> BDD-cost:   76
c ---[1020]---> BDD-cost:   76
c ---[1018]---> BDD-cost:   76
c ---[1016]---> BDD-cost:   76
c ---[1014]---> BDD-cost:   76
c ---[1012]---> BDD-cost:   35
c ---[1010]---> BDD-cost:   76
c ---[1008]---> BDD-cost:   76
c ---[1006]---> BDD-cost:   76
c ---[1004]---> BDD-cost:   76
c ---[1002]---> BDD-cost:   76
c ---[1000]---> BDD-cost:   76
c ---[ 998]---> BDD-cost:   76
c ---[ 996]---> BDD-cost:   76
c ---[ 994]---> BDD-cost:   76
c ---[ 992]---> BDD-cost:   35
c ---[ 990]---> BDD-cost:   76
c ---[ 988]---> BDD-cost:   35
c ---[ 986]---> BDD-cost:   35
c ---[ 984]---> BDD-cost:   76
c ---[ 982]---> BDD-cost:   76
c ---[ 980]---> BDD-cost:   76
c ---[ 978]---> BDD-cost:   76
c ---[ 976]---> BDD-cost:   76
c ---[ 974]---> BDD-cost:   76
c ---[ 972]---> BDD-cost:   76
c ---[ 970]---> BDD-cost:   76
c ---[ 968]---> BDD-cost:   76
c ---[ 966]---> BDD-cost:   76
c ---[ 964]---> BDD-cost:   76
c ---[ 962]---> BDD-cost:   76
c ---[ 960]---> BDD-cost:   76
c ---[ 958]---> BDD-cost:   76
c ---[ 956]---> BDD-cost:   76
c ---[ 954]---> BDD-cost:   76
c ---[ 952]---> BDD-cost:   76
c ---[ 950]---> BDD-cost:   35
c ---[ 948]---> BDD-cost:   76
c ---[ 946]---> BDD-cost:   35
c ---[ 944]---> BDD-cost:   35
c ---[ 942]---> BDD-cost:   35
c ---[ 940]---> BDD-cost:   76
c ---[ 938]---> BDD-cost:   76
c ---[ 936]---> BDD-cost:   76
c ---[ 934]---> BDD-cost:   76
c ---[ 932]---> BDD-cost:   76
c ---[ 930]---> BDD-cost:   76
c ---[ 928]---> BDD-cost:   76
c ---[ 926]---> BDD-cost:   76
c ---[ 924]---> BDD-cost:   76
c ---[ 922]---> BDD-cost:   76
c ---[ 920]---> BDD-cost:   76
c ---[ 918]---> BDD-cost:   35
c ---[ 916]---> BDD-cost:   76
c ---[ 914]---> BDD-cost:   35
c ---[ 912]---> BDD-cost:   76
c ---[ 910]---> BDD-cost:   76
c ---[ 908]---> BDD-cost:   76
c ---[ 906]---> BDD-cost:   76
c ---[ 904]---> BDD-cost:   76
c ---[ 902]---> BDD-cost:   76
c ---[ 900]---> BDD-cost:   76
c ---[ 898]---> BDD-cost:   76
c ---[ 896]---> BDD-cost:   35
c ---[ 894]---> BDD-cost:   76
c ---[ 892]---> BDD-cost:   76
c ---[ 890]---> BDD-cost:   76
c ---[ 888]---> BDD-cost:   76
c ---[ 886]---> BDD-cost:   76
c ---[ 884]---> BDD-cost:   76
c ---[ 882]---> BDD-cost:   76
c ---[ 880]---> BDD-cost:   76
c ---[ 878]---> BDD-cost:   76
c ---[ 876]---> BDD-cost:   76
c ---[ 874]---> BDD-cost:   76
c ---[ 872]---> BDD-cost:   76
c ---[ 870]---> BDD-cost:   35
c ---[ 868]---> BDD-cost:   76
c ---[ 866]---> BDD-cost:   35
c ---[ 864]---> BDD-cost:   76
c ---[ 862]---> BDD-cost:   76
c ---[ 860]---> BDD-cost:   76
c ---[ 858]---> BDD-cost:   76
c ---[ 856]---> BDD-cost:   76
c ---[ 854]---> BDD-cost:   76
c ---[ 852]---> BDD-cost:   76
c ---[ 850]---> BDD-cost:   76
c ---[ 848]---> BDD-cost:   35
c ---[ 846]---> BDD-cost:   76
c ---[ 844]---> BDD-cost:   76
c ---[ 842]---> BDD-cost:   76
c ---[ 840]---> BDD-cost:   76
c ---[ 838]---> BDD-cost:   35
c ---[ 836]---> BDD-cost:   76
c ---[ 834]---> BDD-cost:   76
c ---[ 832]---> BDD-cost:   76
c ---[ 830]---> BDD-cost:   76
c ---[ 828]---> BDD-cost:   76
c ---[ 826]---> BDD-cost:   35
c ---[ 824]---> BDD-cost:   35
c ---[ 822]---> BDD-cost:   35
c ---[ 820]---> BDD-cost:   35
c ---[ 818]---> BDD-cost:   76
c ---[ 816]---> BDD-cost:   35
c ---[ 814]---> BDD-cost:   76
c ---[ 812]---> BDD-cost:   76
c ---[ 810]---> BDD-cost:   76
c ---[ 808]---> BDD-cost:   76
c ---[ 806]---> BDD-cost:   76
c ---[ 804]---> BDD-cost:   76
c ---[ 802]---> BDD-cost:   76
c ---[ 800]---> BDD-cost:   76
c ---[ 798]---> BDD-cost:   76
c ---[ 796]---> BDD-cost:   76
c ---[ 794]---> BDD-cost:   76
c ---[ 792]---> BDD-cost:   76
c ---[ 790]---> BDD-cost:   76
c ---[ 788]---> BDD-cost:   76
c ---[ 786]---> BDD-cost:   76
c ---[ 784]---> BDD-cost:   76
c ---[ 782]---> BDD-cost:   76
c ---[ 780]---> BDD-cost:   76
c ---[ 778]---> BDD-cost:   76
c ---[ 776]---> BDD-cost:   76
c ---[ 774]---> BDD-cost:   76
c ---[ 772]---> BDD-cost:   76
c ---[ 770]---> BDD-cost:   76
c ---[ 768]---> BDD-cost:   76
c ---[ 766]---> BDD-cost:   76
c ---[ 764]---> BDD-cost:   76
c ---[ 762]---> BDD-cost:   76
c ---[ 760]---> BDD-cost:   76
c ---[ 758]---> BDD-cost:   76
c ---[ 756]---> BDD-cost:   76
c ---[ 754]---> BDD-cost:   76
c ---[ 752]---> BDD-cost:   76
c ---[ 750]---> BDD-cost:   76
c ---[ 748]---> BDD-cost:   76
c ---[ 746]---> BDD-cost:   76
c ---[ 744]---> BDD-cost:   76
c ---[ 742]---> BDD-cost:   76
c ---[ 740]---> BDD-cost:   76
c ---[ 738]---> BDD-cost:   76
c ---[ 736]---> BDD-cost:   76
c ---[ 734]---> BDD-cost:   76
c ---[ 732]---> BDD-cost:   76
c ---[ 730]---> BDD-cost:   76
c ---[ 728]---> BDD-cost:   76
c ---[ 726]---> BDD-cost:   76
c ---[ 724]---> BDD-cost:   76
c ---[ 722]---> BDD-cost:   76
c ---[ 720]---> BDD-cost:   76
c ---[ 718]---> BDD-cost:   76
c ---[ 716]---> BDD-cost:   76
c ---[ 714]---> BDD-cost:   76
c ---[ 712]---> BDD-cost:   76
c ---[ 710]---> BDD-cost:   76
c ---[ 708]---> BDD-cost:   76
c ---[ 706]---> BDD-cost:   76
c ---[ 704]---> BDD-cost:   76
c ---[ 702]---> BDD-cost:   76
c ---[ 700]---> BDD-cost:   76
c ---[ 698]---> BDD-cost:   76
c ---[ 696]---> BDD-cost:   76
c ---[ 694]---> BDD-cost:   76
c ---[ 692]---> BDD-cost:   76
c ---[ 690]---> BDD-cost:   76
c ---[ 688]---> BDD-cost:   76
c ---[ 686]---> BDD-cost:   76
c ---[ 684]---> BDD-cost:   76
c ---[ 682]---> BDD-cost:   76
c ---[ 680]---> BDD-cost:   76
c ---[ 678]---> BDD-cost:   76
c ---[ 676]---> BDD-cost:   76
c ---[ 674]---> BDD-cost:   76
c ---[ 672]---> BDD-cost:   76
c ---[ 670]---> BDD-cost:   76
c ---[ 668]---> BDD-cost:   76
c ---[ 666]---> BDD-cost:   76
c ---[ 664]---> BDD-cost:   76
c ---[ 662]---> BDD-cost:   76
c ---[ 660]---> BDD-cost:   76
c ---[ 658]---> BDD-cost:   76
c ---[ 656]---> BDD-cost:   76
c ---[ 654]---> BDD-cost:   76
c ---[ 652]---> BDD-cost:   76
c ---[ 650]---> BDD-cost:   76
c ---[ 648]---> BDD-cost:   76
c ---[ 646]---> BDD-cost:   76
c ---[ 644]---> BDD-cost:   76
c ---[ 642]---> BDD-cost:   76
c ---[ 640]---> BDD-cost:   76
c ---[ 638]---> BDD-cost:   76
c ---[ 636]---> BDD-cost:   76
c ---[ 634]---> BDD-cost:   76
c ---[ 632]---> BDD-cost:   76
c ---[ 630]---> BDD-cost:   76
c ---[ 628]---> BDD-cost:   76
c ---[ 626]---> BDD-cost:   76
c ---[ 624]---> BDD-cost:   76
c ---[ 622]---> BDD-cost:   76
c ---[ 620]---> BDD-cost:   76
c ---[ 618]---> BDD-cost:   76
c ---[ 616]---> BDD-cost:   76
c ---[ 614]---> BDD-cost:   76
c ---[ 612]---> BDD-cost:   76
c ---[ 610]---> BDD-cost:   76
c ---[ 608]---> BDD-cost:   76
c ---[ 606]---> BDD-cost:   76
c ---[ 604]---> BDD-cost:   76
c ---[ 602]---> BDD-cost:   76
c ---[ 600]---> BDD-cost:   76
c ---[ 598]---> BDD-cost:   76
c ---[ 596]---> BDD-cost:   76
c ---[ 594]---> BDD-cost:   76
c ---[ 592]---> BDD-cost:   76
c ---[ 590]---> BDD-cost:   76
c ---[ 588]---> BDD-cost:   76
c ---[ 586]---> BDD-cost:   76
c ---[ 584]---> BDD-cost:   76
c ---[ 582]---> BDD-cost:   76
c ---[ 580]---> BDD-cost:   76
c ---[ 578]---> BDD-cost:   76
c ---[ 576]---> BDD-cost:   76
c ---[ 574]---> BDD-cost:   76
c ---[ 572]---> BDD-cost:   76
c ---[ 570]---> BDD-cost:   76
c ---[ 568]---> BDD-cost:   76
c ---[ 566]---> BDD-cost:   76
c ---[ 564]---> BDD-cost:   76
c ---[ 562]---> BDD-cost:   76
c ---[ 560]---> BDD-cost:   76
c ---[ 558]---> BDD-cost:   76
c ---[ 556]---> BDD-cost:   76
c ---[ 554]---> BDD-cost:   76
c ---[ 552]---> BDD-cost:   76
c ---[ 550]---> BDD-cost:   76
c ---[ 548]---> BDD-cost:   76
c ---[ 546]---> BDD-cost:   76
c ---[ 544]---> BDD-cost:   76
c ---[ 542]---> BDD-cost:   76
c ---[ 540]---> BDD-cost:   76
c ---[ 538]---> BDD-cost:   76
c ---[ 536]---> BDD-cost:   76
c ---[ 534]---> BDD-cost:   76
c ---[ 532]---> BDD-cost:   76
c ---[ 530]---> BDD-cost:   76
c ---[ 528]---> BDD-cost:   76
c ---[ 526]---> BDD-cost:   76
c ---[ 524]---> BDD-cost:   76
c ---[ 522]---> BDD-cost:   76
c ---[ 520]---> BDD-cost:   76
c ---[ 518]---> BDD-cost:   76
c ---[ 516]---> BDD-cost:   76
c ---[ 514]---> BDD-cost:   76
c ---[ 512]---> BDD-cost:   76
c ---[ 510]---> BDD-cost:   76
c ---[ 508]---> BDD-cost:   76
c ---[ 506]---> BDD-cost:   76
c ---[ 504]---> BDD-cost:   76
c ---[ 502]---> BDD-cost:   76
c ---[ 500]---> BDD-cost:   76
c ---[ 498]---> BDD-cost:   76
c ---[ 496]---> BDD-cost:   76
c ---[ 494]---> BDD-cost:   76
c ---[ 492]---> BDD-cost:   76
c ---[ 490]---> BDD-cost:   76
c ---[ 488]---> BDD-cost:   76
c ---[ 486]---> BDD-cost:   76
c ---[ 484]---> BDD-cost:   76
c ---[ 482]---> BDD-cost:   76
c ---[ 480]---> BDD-cost:   76
c ---[ 478]---> BDD-cost:   76
c ---[ 476]---> BDD-cost:   76
c ---[ 474]---> BDD-cost:   76
c ---[ 472]---> BDD-cost:   35
c ---[ 470]---> BDD-cost:   76
c ---[ 468]---> BDD-cost:   76
c ---[ 466]---> BDD-cost:   35
c ---[ 464]---> BDD-cost:   76
c ---[ 462]---> BDD-cost:   76
c ---[ 460]---> BDD-cost:   76
c ---[ 458]---> BDD-cost:   76
c ---[ 456]---> BDD-cost:   35
c ---[ 454]---> BDD-cost:   35
c ---[ 452]---> BDD-cost:   76
c ---[ 450]---> BDD-cost:   76
c ---[ 448]---> BDD-cost:   76
c ---[ 446]---> BDD-cost:   76
c ---[ 444]---> BDD-cost:   35
c ---[ 442]---> BDD-cost:   76
c ---[ 440]---> BDD-cost:   76
c ---[ 438]---> BDD-cost:   76
c ---[ 436]---> BDD-cost:   76
c ---[ 434]---> BDD-cost:   76
c ---[ 432]---> BDD-cost:   76
c ---[ 430]---> BDD-cost:   76
c ---[ 428]---> BDD-cost:   35
c ---[ 426]---> BDD-cost:   35
c ---[ 424]---> BDD-cost:   76
c ---[ 422]---> BDD-cost:   76
c ---[ 420]---> BDD-cost:   76
c ---[ 418]---> BDD-cost:   76
c ---[ 416]---> BDD-cost:   76
c ---[ 414]---> BDD-cost:   76
c ---[ 412]---> BDD-cost:   76
c ---[ 410]---> BDD-cost:   76
c ---[ 408]---> BDD-cost:   76
c ---[ 406]---> BDD-cost:   76
c ---[ 404]---> BDD-cost:   76
c ---[ 402]---> BDD-cost:   35
c ---[ 400]---> BDD-cost:   35
c ---[ 398]---> BDD-cost:   76
c ---[ 396]---> BDD-cost:   76
c ---[ 394]---> BDD-cost:   76
c ---[ 392]---> BDD-cost:   76
c ---[ 390]---> BDD-cost:   76
c ---[ 388]---> BDD-cost:   76
c ---[ 386]---> BDD-cost:   76
c ---[ 384]---> BDD-cost:   76
c ---[ 382]---> BDD-cost:   76
c ---[ 380]---> BDD-cost:   76
c ---[ 378]---> BDD-cost:   76
c ---[ 376]---> BDD-cost:   76
c ---[ 374]---> BDD-cost:   76
c ---[ 372]---> BDD-cost:   76
c ---[ 370]---> BDD-cost:   76
c ---[ 368]---> BDD-cost:   76
c ---[ 366]---> BDD-cost:   76
c ---[ 364]---> BDD-cost:   76
c ---[ 362]---> BDD-cost:   76
c ---[ 360]---> BDD-cost:   76
c ---[ 358]---> BDD-cost:   76
c ---[ 356]---> BDD-cost:   76
c ---[ 354]---> BDD-cost:   76
c ---[ 352]---> BDD-cost:   76
c ---[ 350]---> BDD-cost:   76
c ---[ 348]---> BDD-cost:   76
c ---[ 346]---> BDD-cost:   76
c ---[ 344]---> BDD-cost:   76
c ---[ 342]---> BDD-cost:   76
c ---[ 340]---> BDD-cost:   35
c ---[ 338]---> BDD-cost:   35
c ---[ 336]---> BDD-cost:   35
c ---[ 334]---> BDD-cost:   76
c ---[ 332]---> BDD-cost:   76
c ---[ 330]---> BDD-cost:   76
c ---[ 328]---> BDD-cost:   76
c ---[ 326]---> BDD-cost:   76
c ---[ 324]---> BDD-cost:   76
c ---[ 322]---> BDD-cost:   76
c ---[ 320]---> BDD-cost:   76
c ---[ 318]---> BDD-cost:   76
c ---[ 316]---> BDD-cost:   76
c ---[ 314]---> BDD-cost:   76
c ---[ 312]---> BDD-cost:   76
c ---[ 310]---> BDD-cost:   76
c ---[ 308]---> BDD-cost:   76
c ---[ 306]---> BDD-cost:   76
c ---[ 304]---> BDD-cost:   76
c ---[ 302]---> BDD-cost:   76
c ---[ 300]---> BDD-cost:   76
c ---[ 298]---> BDD-cost:   76
c ---[ 296]---> BDD-cost:   76
c ---[ 294]---> BDD-cost:   76
c ---[ 292]---> BDD-cost:   35
c ---[ 290]---> BDD-cost:   76
c ---[ 288]---> BDD-cost:   76
c ---[ 286]---> BDD-cost:   76
c ---[ 284]---> BDD-cost:   76
c ---[ 282]---> BDD-cost:   76
c ---[ 280]---> BDD-cost:   76
c ---[ 278]---> BDD-cost:   76
c ---[ 276]---> BDD-cost:   76
c ---[ 274]---> BDD-cost:   76
c ---[ 272]---> BDD-cost:   76
c ---[ 270]---> BDD-cost:   76
c ---[ 268]---> BDD-cost:   76
c ---[ 266]---> BDD-cost:   76
c ---[ 264]---> BDD-cost:   76
c ---[ 262]---> BDD-cost:   76
c ---[ 260]---> BDD-cost:   35
c ---[ 258]---> BDD-cost:   76
c ---[ 256]---> BDD-cost:   76
c ---[ 254]---> BDD-cost:   76
c ---[ 252]---> BDD-cost:   76
c ---[ 250]---> BDD-cost:   76
c ---[ 248]---> BDD-cost:   76
c ---[ 246]---> BDD-cost:   76
c ---[ 244]---> BDD-cost:   76
c ---[ 242]---> BDD-cost:   35
c ---[ 240]---> BDD-cost:   76
c ---[ 238]---> BDD-cost:   76
c ---[ 236]---> BDD-cost:   35
c ---[ 234]---> BDD-cost:   35
c ---[ 232]---> BDD-cost:   35
c ---[ 230]---> BDD-cost:   35
c ---[ 228]---> BDD-cost:   76
c ---[ 226]---> BDD-cost:   76
c ---[ 224]---> BDD-cost:   76
c ---[ 222]---> BDD-cost:   76
c ---[ 220]---> BDD-cost:   76
c ---[ 218]---> BDD-cost:   76
c ---[ 216]---> BDD-cost:   76
c ---[ 214]---> BDD-cost:   76
c ---[ 212]---> BDD-cost:   76
c ---[ 210]---> BDD-cost:   35
c ---[ 208]---> BDD-cost:   35
c ---[ 206]---> BDD-cost:   76
c ---[ 204]---> BDD-cost:   76
c ---[ 202]---> BDD-cost:   76
c ---[ 200]---> BDD-cost:   76
c ---[ 198]---> BDD-cost:   76
c ---[ 196]---> BDD-cost:   76
c ---[ 194]---> BDD-cost:   76
c ---[ 192]---> BDD-cost:   76
c ---[ 190]---> BDD-cost:   76
c ---[ 188]---> BDD-cost:   76
c ---[ 186]---> BDD-cost:   35
c ---[ 184]---> BDD-cost:   76
c ---[ 182]---> BDD-cost:   76
c ---[ 180]---> BDD-cost:   76
c ---[ 178]---> BDD-cost:   35
c ---[ 176]---> BDD-cost:   35
c ---[ 174]---> BDD-cost:   35
c ---[ 172]---> BDD-cost:   76
c ---[ 170]---> BDD-cost:   76
c ---[ 168]---> BDD-cost:   35
c ---[ 166]---> BDD-cost:   35
c ---[ 164]---> BDD-cost:   76
c ---[ 162]---> BDD-cost:   76
c ---[ 160]---> BDD-cost:   76
c ---[ 158]---> BDD-cost:   35
c ---[ 156]---> BDD-cost:   35
c ---[ 154]---> BDD-cost:   76
c ---[ 152]---> BDD-cost:   76
c ---[ 150]---> BDD-cost:   35
c ---[ 148]---> BDD-cost:   35
c ---[ 146]---> BDD-cost:   35
c ---[ 144]---> BDD-cost:   76
c ---[ 142]---> BDD-cost:   76
c ---[ 140]---> BDD-cost:   76
c ---[ 138]---> BDD-cost:   76
c ---[ 136]---> BDD-cost:   76
c ---[ 134]---> BDD-cost:   76
c ---[ 132]---> BDD-cost:   35
c ---[ 130]---> BDD-cost:   76
c ---[ 128]---> BDD-cost:   35
c ---[ 126]---> BDD-cost:   76
c ---[ 124]---> BDD-cost:   76
c ---[ 122]---> BDD-cost:   76
c ---[ 120]---> BDD-cost:   76
c ---[ 118]---> BDD-cost:   35
c ---[ 116]---> BDD-cost:   76
c ---[ 114]---> BDD-cost:   35
c ---[ 112]---> BDD-cost:   76
c ---[ 110]---> BDD-cost:   76
c ---[ 108]---> BDD-cost:   35
c ---[ 106]---> BDD-cost:   35
c ---[ 104]---> BDD-cost:   76
c ---[ 102]---> BDD-cost:   76
c ---[ 100]---> BDD-cost:   76
c ---[  98]---> BDD-cost:   35
c ---[  96]---> BDD-cost:   76
c ---[  94]---> BDD-cost:   76
c ---[  92]---> BDD-cost:   76
c ---[  90]---> BDD-cost:   76
c ---[  88]---> BDD-cost:   35
c ---[  86]---> BDD-cost:   35
c ---[  84]---> BDD-cost:   35
c ---[  82]---> BDD-cost:   35
c ---[  80]---> BDD-cost:   35
c ---[  78]---> BDD-cost:   35
c ---[  76]---> BDD-cost:   35
c ---[  74]---> BDD-cost:   76
c ---[  72]---> BDD-cost:   35
c ---[  70]---> BDD-cost:   35
c ---[  68]---> BDD-cost:   76
c ---[  66]---> BDD-cost:   35
c ---[  64]---> BDD-cost:   35
c ---[  62]---> BDD-cost:   35
c ---[  60]---> BDD-cost:   35
c ---[  58]---> BDD-cost:   35
c ---[  56]---> BDD-cost:   76
c ---[  54]---> BDD-cost:   35
c ---[  52]---> BDD-cost:   35
c ---[  50]---> BDD-cost:   76
c ---[  48]---> BDD-cost:   35
c ---[  46]---> BDD-cost:   35
c ---[  44]---> BDD-cost:   76
c ---[  42]---> BDD-cost:   76
c ---[  40]---> BDD-cost:   35
c ---[  38]---> BDD-cost:   76
c ---[  36]---> BDD-cost:   35
c ---[  34]---> BDD-cost:   35
c ---[  32]---> BDD-cost:   76
c ---[  30]---> BDD-cost:   76
c ---[  28]---> BDD-cost:   76
c ---[  26]---> BDD-cost:   76
c ---[  24]---> BDD-cost:   76
c ---[  22]---> BDD-cost:   35
c ---[  20]---> BDD-cost:   76
c ---[  18]---> BDD-cost:   35
c ---[  16]---> BDD-cost:   76
c ---[  14]---> BDD-cost:   76
c ---[  12]---> BDD-cost:   35
c ---[  10]---> BDD-cost:   76
c ---[   8]---> BDD-cost:   76
c ---[   6]---> BDD-cost:   76
c ---[   4]---> BDD-cost:   76
c ---[   2]---> BDD-cost:   76
c ---[   0]---> BDD-cost:   76
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |         0 | 2516819  7961042 |  755045       0        0     nan |  0.000 % |
c   -- subsuming                       
c   -- var.elim.:  1000/548370          
c   -- var.elim.:  2000/548370          
c   -- var.elim.:  3000/548370          
c   -- var.elim.:  4000/548370          
c   -- var.elim.:  5000/548370          
c   -- var.elim.:  6000/548370          
c   -- var.elim.:  7000/548370          
c   -- var.elim.:  8000/548370          
c   -- var.elim.:  9000/548370          
c   -- var.elim.:  10000/548370          
c   -- var.elim.:  11000/548370          
c   -- var.elim.:  12000/548370          
c   -- var.elim.:  13000/548370          
c   -- var.elim.:  14000/548370          
c   -- var.elim.:  15000/548370          
c   -- var.elim.:  16000/548370          
c   -- var.elim.:  17000/548370          
c   -- var.elim.:  18000/548370          
c   -- var.elim.:  19000/548370          
c   -- var.elim.:  20000/548370          
c   -- var.elim.:  21000/548370          
c   -- var.elim.:  22000/548370          
c   -- var.elim.:  23000/548370          
c   -- var.elim.:  24000/548370          
c   -- var.elim.:  25000/548370          
c   -- var.elim.:  26000/548370          
c   -- var.elim.:  27000/548370          
c   -- var.elim.:  28000/548370          
c   -- var.elim.:  29000/548370          
c   -- var.elim.:  30000/548370          
c   -- var.elim.:  31000/548370          
c   -- var.elim.:  32000/548370          
c   -- var.elim.:  33000/548370          
c   -- var.elim.:  34000/548370          
c   -- var.elim.:  35000/548370          
c   -- var.elim.:  36000/548370          
c   -- var.elim.:  37000/548370          
c   -- var.elim.:  38000/548370          
c   -- var.elim.:  39000/548370          
c   -- var.elim.:  40000/548370          
c   -- var.elim.:  41000/548370          
c   -- var.elim.:  42000/548370          
c   -- var.elim.:  43000/548370          
c   -- var.elim.:  44000/548370          
c   -- var.elim.:  45000/548370          
c   -- var.elim.:  46000/548370          
c   -- var.elim.:  47000/548370          
c   -- var.elim.:  48000/548370          
c   -- var.elim.:  49000/548370          
c   -- var.elim.:  50000/548370          
c   -- var.elim.:  51000/548370          
c   -- var.elim.:  52000/548370          
c   -- var.elim.:  53000/548370          
c   -- var.elim.:  54000/548370          
c   -- var.elim.:  55000/548370          
c   -- var.elim.:  56000/548370          
c   -- var.elim.:  57000/548370          
c   -- var.elim.:  58000/548370          
c   -- var.elim.:  59000/548370          
c   -- var.elim.:  60000/548370          
c   -- var.elim.:  61000/548370          
c   -- var.elim.:  62000/548370          
c   -- var.elim.:  63000/548370          
c   -- var.elim.:  64000/548370          
c   -- var.elim.:  65000/548370          
c   -- var.elim.:  66000/548370          
c   -- var.elim.:  67000/548370          
c   -- var.elim.:  68000/548370          
c   -- var.elim.:  69000/548370          
c   -- var.elim.:  70000/548370          
c   -- var.elim.:  71000/548370          
c   -- var.elim.:  72000/548370          
c   -- var.elim.:  73000/548370          
c   -- var.elim.:  74000/548370          
c   -- var.elim.:  75000/548370          
c   -- var.elim.:  76000/548370          
c   -- var.elim.:  77000/548370          
c   -- var.elim.:  78000/548370          
c   -- var.elim.:  79000/548370          
c   -- var.elim.:  80000/548370          
c   -- var.elim.:  81000/548370          
c   -- var.elim.:  82000/548370          
c   -- var.elim.:  83000/548370          
c   -- var.elim.:  84000/548370          
c   -- var.elim.:  85000/548370          
c   -- var.elim.:  86000/548370          
c   -- var.elim.:  87000/548370          
c   -- var.elim.:  88000/548370          
c   -- var.elim.:  89000/548370          
c   -- var.elim.:  90000/548370          
c   -- var.elim.:  91000/548370          
c   -- var.elim.:  92000/548370          
c   -- var.elim.:  93000/548370          
c   -- var.elim.:  94000/548370          
c   -- var.elim.:  95000/548370          
c   -- var.elim.:  96000/548370          
c   -- var.elim.:  97000/548370          
c   -- var.elim.:  98000/548370          
c   -- var.elim.:  99000/548370          
c   -- var.elim.:  100000/548370          
c   -- var.elim.:  101000/548370          
c   -- var.elim.:  102000/548370          
c   -- var.elim.:  103000/548370          
c   -- var.elim.:  104000/548370          
c   -- var.elim.:  105000/548370          
c   -- var.elim.:  106000/548370          
c   -- var.elim.:  107000/548370          
c   -- var.elim.:  108000/548370          
c   -- var.elim.:  109000/548370          
c   -- var.elim.:  110000/548370          
c   -- var.elim.:  111000/548370          
c   -- var.elim.:  112000/548370          
c   -- var.elim.:  113000/548370          
c   -- var.elim.:  114000/548370          
c   -- var.elim.:  115000/548370          
c   -- var.elim.:  116000/548370          
c   -- var.elim.:  117000/548370          
c   -- var.elim.:  118000/548370          
c   -- var.elim.:  119000/548370          
c   -- var.elim.:  120000/548370          
c   -- var.elim.:  121000/548370          
c   -- var.elim.:  122000/548370          
c   -- var.elim.:  123000/548370          
c   -- var.elim.:  124000/548370          
c   -- var.elim.:  125000/548370          
c   -- var.elim.:  126000/548370          
c   -- var.elim.:  127000/548370          
c   -- var.elim.:  128000/548370          
c   -- var.elim.:  129000/548370          
c   -- var.elim.:  130000/548370          
c   -- var.elim.:  131000/548370          
c   -- var.elim.:  132000/548370          
c   -- var.elim.:  133000/548370          
c   -- var.elim.:  134000/548370          
c   -- var.elim.:  135000/548370          
c   -- var.elim.:  136000/548370          
c   -- var.elim.:  137000/548370          
c   -- var.elim.:  138000/548370          
c   -- var.elim.:  139000/548370          
c   -- var.elim.:  140000/548370          
c   -- var.elim.:  141000/548370          
c   -- var.elim.:  142000/548370          
c   -- var.elim.:  143000/548370          
c   -- var.elim.:  144000/548370          
c   -- var.elim.:  145000/548370          
c   -- var.elim.:  146000/548370          
c   -- var.elim.:  147000/548370          
c   -- var.elim.:  148000/548370          
c   -- var.elim.:  149000/548370          
c   -- var.elim.:  150000/548370          
c   -- var.elim.:  151000/548370          
c   -- var.elim.:  152000/548370          
c   -- var.elim.:  153000/548370          
c   -- var.elim.:  154000/548370          
c   -- var.elim.:  155000/548370          
c   -- var.elim.:  156000/548370          
c   -- var.elim.:  157000/548370          
c   -- var.elim.:  158000/548370          
c   -- var.elim.:  159000/548370          
c   -- var.elim.:  160000/548370          
c   -- var.elim.:  161000/548370          
c   -- var.elim.:  162000/548370          
c   -- var.elim.:  163000/548370          
c   -- var.elim.:  164000/548370          
c   -- var.elim.:  165000/548370          
c   -- var.elim.:  166000/548370          
c   -- var.elim.:  167000/548370          
c   -- var.elim.:  168000/548370          
c   -- var.elim.:  169000/548370          
c   -- var.elim.:  170000/548370          
c   -- var.elim.:  171000/548370          
c   -- var.elim.:  172000/548370          
c   -- var.elim.:  173000/548370          
c   -- var.elim.:  174000/548370          
c   -- var.elim.:  175000/548370          
c   -- var.elim.:  176000/548370          
c   -- var.elim.:  177000/548370          
c   -- var.elim.:  178000/548370          
c   -- var.elim.:  179000/548370          
c   -- var.elim.:  180000/548370          
c   -- var.elim.:  181000/548370          
c   -- var.elim.:  182000/548370          
c   -- var.elim.:  183000/548370          
c   -- var.elim.:  184000/548370          
c   -- var.elim.:  185000/548370          
c   -- var.elim.:  186000/548370          
c   -- var.elim.:  187000/548370          
c   -- var.elim.:  188000/548370          
c   -- var.elim.:  189000/548370          
c   -- var.elim.:  190000/548370          
c   -- var.elim.:  191000/548370          
c   -- var.elim.:  192000/548370          
c   -- var.elim.:  193000/548370          
c   -- var.elim.:  194000/548370          
c   -- var.elim.:  195000/548370          
c   -- var.elim.:  196000/548370          
c   -- var.elim.:  197000/548370          
c   -- var.elim.:  198000/548370          
c   -- var.elim.:  199000/548370          
c   -- var.elim.:  200000/548370          
c   -- var.elim.:  201000/548370          
c   -- var.elim.:  202000/548370          
c   -- var.elim.:  203000/548370          
c   -- var.elim.:  204000/548370          
c   -- var.elim.:  205000/548370          
c   -- var.elim.:  206000/548370          
c   -- var.elim.:  207000/548370          
c   -- var.elim.:  208000/548370          
c   -- var.elim.:  209000/548370          
c   -- var.elim.:  210000/548370          
c   -- var.elim.:  211000/548370          
c   -- var.elim.:  212000/548370          
c   -- var.elim.:  213000/548370          
c   -- var.elim.:  214000/548370          
c   -- var.elim.:  215000/548370          
c   -- var.elim.:  216000/548370          
c   -- var.elim.:  217000/548370          
c   -- var.elim.:  218000/548370          
c   -- var.elim.:  219000/548370          
c   -- var.elim.:  220000/548370          
c   -- var.elim.:  221000/548370          
c   -- var.elim.:  222000/548370          
c   -- var.elim.:  223000/548370          
c   -- var.elim.:  224000/548370          
c   -- var.elim.:  225000/548370          
c   -- var.elim.:  226000/548370          
c   -- var.elim.:  227000/548370          
c   -- var.elim.:  228000/548370          
c   -- var.elim.:  229000/548370          
c   -- var.elim.:  230000/548370          
c   -- var.elim.:  231000/548370          
c   -- var.elim.:  232000/548370          
c   -- var.elim.:  233000/548370          
c   -- var.elim.:  234000/548370          
c   -- var.elim.:  235000/548370          
c   -- var.elim.:  236000/548370          
c   -- var.elim.:  237000/548370          
c   -- var.elim.:  238000/548370          
c   -- var.elim.:  239000/548370          
c   -- var.elim.:  240000/548370          
c   -- var.elim.:  241000/548370          
c   -- var.elim.:  242000/548370          
c   -- var.elim.:  243000/548370          
c   -- var.elim.:  244000/548370          
c   -- var.elim.:  245000/548370          
c   -- var.elim.:  246000/548370          
c   -- var.elim.:  247000/548370          
c   -- var.elim.:  248000/548370          
c   -- var.elim.:  249000/548370          
c   -- var.elim.:  250000/548370          
c   -- var.elim.:  251000/548370          
c   -- var.elim.:  252000/548370          
c   -- var.elim.:  253000/548370          
c   -- var.elim.:  254000/548370          
c   -- var.elim.:  255000/548370          
c   -- var.elim.:  256000/548370          
c   -- var.elim.:  257000/548370          
c   -- var.elim.:  258000/548370          
c   -- var.elim.:  259000/548370          
c   -- var.elim.:  260000/548370          
c   -- var.elim.:  261000/548370          
c   -- var.elim.:  262000/548370          
c   -- var.elim.:  263000/548370          
c   -- var.elim.:  264000/548370          
c   -- var.elim.:  265000/548370          
c   -- var.elim.:  266000/548370          
c   -- var.elim.:  267000/548370          
c   -- var.elim.:  268000/548370          
c   -- var.elim.:  269000/548370          
c   -- var.elim.:  270000/548370          
c   -- var.elim.:  271000/548370          
c   -- var.elim.:  272000/548370          
c   -- var.elim.:  273000/548370          
c   -- var.elim.:  274000/548370          
c   -- var.elim.:  275000/548370          
c   -- var.elim.:  276000/548370          
c   -- var.elim.:  277000/548370          
c   -- var.elim.:  278000/548370          
c   -- var.elim.:  279000/548370          
c   -- var.elim.:  280000/548370          
c   -- var.elim.:  281000/548370          
c   -- var.elim.:  282000/548370          
c   -- var.elim.:  283000/548370          
c   -- var.elim.:  284000/548370          
c   -- var.elim.:  285000/548370          
c   -- var.elim.:  286000/548370          
c   -- var.elim.:  287000/548370          
c   -- var.elim.:  288000/548370          
c   -- var.elim.:  289000/548370          
c   -- var.elim.:  290000/548370          
c   -- var.elim.:  291000/548370          
c   -- var.elim.:  292000/548370          
c   -- var.elim.:  293000/548370          
c   -- var.elim.:  294000/548370          
c   -- var.elim.:  295000/548370          
c   -- var.elim.:  296000/548370          
c   -- var.elim.:  297000/548370          
c   -- var.elim.:  298000/548370          
c   -- var.elim.:  299000/548370          
c   -- var.elim.:  300000/548370          
c   -- var.elim.:  301000/548370          
c   -- var.elim.:  302000/548370          
c   -- var.elim.:  303000/548370          
c   -- var.elim.:  304000/548370          
c   -- var.elim.:  305000/548370          
c   -- var.elim.:  306000/548370          
c   -- var.elim.:  307000/548370          
c   -- var.elim.:  308000/548370          
c   -- var.elim.:  309000/548370          
c   -- var.elim.:  310000/548370          
c   -- var.elim.:  311000/548370          
c   -- var.elim.:  312000/548370          
c   -- var.elim.:  313000/548370          
c   -- var.elim.:  314000/548370          
c   -- var.elim.:  315000/548370          
c   -- var.elim.:  316000/548370          
c   -- var.elim.:  317000/548370          
c   -- var.elim.:  318000/548370          
c   -- var.elim.:  319000/548370          
c   -- var.elim.:  320000/548370          
c   -- var.elim.:  321000/548370          
c   -- var.elim.:  322000/548370          
c   -- var.elim.:  323000/548370          
c   -- var.elim.:  324000/548370          
c   -- var.elim.:  325000/548370          
c   -- var.elim.:  326000/548370          
c   -- var.elim.:  327000/548370          
c   -- var.elim.:  328000/548370          
c   -- var.elim.:  329000/548370          
c   -- var.elim.:  330000/548370          
c   -- var.elim.:  331000/548370          
c   -- var.elim.:  332000/548370          
c   -- var.elim.:  333000/548370          
c   -- var.elim.:  334000/548370          
c   -- var.elim.:  335000/548370          
c   -- var.elim.:  336000/548370          
c   -- var.elim.:  337000/548370          
c   -- var.elim.:  338000/548370          
c   -- var.elim.:  339000/548370          
c   -- var.elim.:  340000/548370          
c   -- var.elim.:  341000/548370          
c   -- var.elim.:  342000/548370          
c   -- var.elim.:  343000/548370          
c   -- var.elim.:  344000/548370          
c   -- var.elim.:  345000/548370          
c   -- var.elim.:  346000/548370          
c   -- var.elim.:  347000/548370          
c   -- var.elim.:  348000/548370          
c   -- var.elim.:  349000/548370          
c   -- var.elim.:  350000/548370          
c   -- var.elim.:  351000/548370          
c   -- var.elim.:  352000/548370          
c   -- var.elim.:  353000/548370          
c   -- var.elim.:  354000/548370          
c   -- var.elim.:  355000/548370          
c   -- var.elim.:  356000/548370          
c   -- var.elim.:  357000/548370          
c   -- var.elim.:  358000/548370          
c   -- var.elim.:  359000/548370          
c   -- var.elim.:  360000/548370          
c   -- var.elim.:  361000/548370          
c   -- var.elim.:  362000/548370          
c   -- var.elim.:  363000/548370          
c   -- var.elim.:  364000/548370          
c   -- var.elim.:  365000/548370          
c   -- var.elim.:  366000/548370          
c   -- var.elim.:  367000/548370          
c   -- var.elim.:  368000/548370          
c   -- var.elim.:  369000/548370          
c   -- var.elim.:  370000/548370          
c   -- var.elim.:  371000/548370          
c   -- var.elim.:  372000/548370          
c   -- var.elim.:  373000/548370          
c   -- var.elim.:  374000/548370          
c   -- var.elim.:  375000/548370          
c   -- var.elim.:  376000/548370          
c   -- var.elim.:  377000/548370          
c   -- var.elim.:  378000/548370          
c   -- var.elim.:  379000/548370          
c   -- var.elim.:  380000/548370          
c   -- var.elim.:  381000/548370          
c   -- var.elim.:  382000/548370          
c   -- var.elim.:  383000/548370          
c   -- var.elim.:  384000/548370          
c   -- var.elim.:  385000/548370          
c   -- var.elim.:  386000/548370          
c   -- var.elim.:  387000/548370          
c   -- var.elim.:  388000/548370          
c   -- var.elim.:  389000/548370          
c   -- var.elim.:  390000/548370          
c   -- var.elim.:  391000/548370          
c   -- var.elim.:  392000/548370          
c   -- var.elim.:  393000/548370          
c   -- var.elim.:  394000/548370          
c   -- var.elim.:  395000/548370          
c   -- var.elim.:  396000/548370          
c   -- var.elim.:  397000/548370          
c   -- var.elim.:  398000/548370          
c   -- var.elim.:  399000/548370          
c   -- var.elim.:  400000/548370          
c   -- var.elim.:  401000/548370          
c   -- var.elim.:  402000/548370          
c   -- var.elim.:  403000/548370          
c   -- var.elim.:  404000/548370          
c   -- var.elim.:  405000/548370          
c   -- var.elim.:  406000/548370          
c   -- var.elim.:  407000/548370          
c   -- var.elim.:  408000/548370          
c   -- var.elim.:  409000/548370          
c   -- var.elim.:  410000/548370          
c   -- var.elim.:  411000/548370          
c   -- var.elim.:  412000/548370          
c   -- var.elim.:  413000/548370          
c   -- var.elim.:  414000/548370          
c   -- var.elim.:  415000/548370          
c   -- var.elim.:  416000/548370          
c   -- var.elim.:  417000/548370          
c   -- var.elim.:  418000/548370          
c   -- var.elim.:  419000/548370          
c   -- var.elim.:  420000/548370          
c   -- var.elim.:  421000/548370          
c   -- var.elim.:  422000/548370          
c   -- var.elim.:  423000/548370          
c   -- var.elim.:  424000/548370          
c   -- var.elim.:  425000/548370          
c   -- var.elim.:  426000/548370          
c   -- var.elim.:  427000/548370          
c   -- var.elim.:  428000/548370          
c   -- var.elim.:  429000/548370          
c   -- var.elim.:  430000/548370          
c   -- var.elim.:  431000/548370          
c   -- var.elim.:  432000/548370          
c   -- var.elim.:  433000/548370          
c   -- var.elim.:  434000/548370          
c   -- var.elim.:  435000/548370          
c   -- var.elim.:  436000/548370          
c   -- var.elim.:  437000/548370          
c   -- var.elim.:  438000/548370          
c   -- var.elim.:  439000/548370          
c   -- var.elim.:  440000/548370          
c   -- var.elim.:  441000/548370          
c   -- var.elim.:  442000/548370          
c   -- var.elim.:  443000/548370          
c   -- var.elim.:  444000/548370          
c   -- var.elim.:  445000/548370          
c   -- var.elim.:  446000/548370          
c   -- var.elim.:  447000/548370          
c   -- var.elim.:  448000/548370          
c   -- var.elim.:  449000/548370          
c   -- var.elim.:  450000/548370          
c   -- var.elim.:  451000/548370          
c   -- var.elim.:  452000/548370          
c   -- var.elim.:  453000/548370          
c   -- var.elim.:  454000/548370          
c   -- var.elim.:  455000/548370          
c   -- var.elim.:  456000/548370          
c   -- var.elim.:  457000/548370          
c   -- var.elim.:  458000/548370          
c   -- var.elim.:  459000/548370          
c   -- var.elim.:  460000/548370          
c   -- var.elim.:  461000/548370          
c   -- var.elim.:  462000/548370          
c   -- var.elim.:  463000/548370          
c   -- var.elim.:  464000/548370          
c   -- var.elim.:  465000/548370          
c   -- var.elim.:  466000/548370          
c   -- var.elim.:  467000/548370          
c   -- var.elim.:  468000/548370          
c   -- var.elim.:  469000/548370          
c   -- var.elim.:  470000/548370          
c   -- var.elim.:  471000/548370          
c   -- var.elim.:  472000/548370          
c   -- var.elim.:  473000/548370          
c   -- var.elim.:  474000/548370          
c   -- var.elim.:  475000/548370          
c   -- var.elim.:  476000/548370          
c   -- var.elim.:  477000/548370          
c   -- var.elim.:  478000/548370          
c   -- var.elim.:  479000/548370          
c   -- var.elim.:  480000/548370          
c   -- var.elim.:  481000/548370          
c   -- var.elim.:  482000/548370          
c   -- var.elim.:  483000/548370          
c   -- var.elim.:  484000/548370          
c   -- var.elim.:  485000/548370          
c   -- var.elim.:  486000/548370          
c   -- var.elim.:  487000/548370          
c   -- var.elim.:  488000/548370          
c   -- var.elim.:  489000/548370          
c   -- var.elim.:  490000/548370          
c   -- var.elim.:  491000/548370          
c   -- var.elim.:  492000/548370          
c   -- var.elim.:  493000/548370          
c   -- var.elim.:  494000/548370          
c   -- var.elim.:  495000/548370          
c   -- var.elim.:  496000/548370          
c   -- var.elim.:  497000/548370          
c   -- var.elim.:  498000/548370          
c   -- var.elim.:  499000/548370          
c   -- var.elim.:  500000/548370          
c   -- var.elim.:  501000/548370          
c   -- var.elim.:  502000/548370          
c   -- var.elim.:  503000/548370          
c   -- var.elim.:  504000/548370          
c   -- var.elim.:  505000/548370          
c   -- var.elim.:  506000/548370          
c   -- var.elim.:  507000/548370          
c   -- var.elim.:  508000/548370          
c   -- var.elim.:  509000/548370          
c   -- var.elim.:  510000/548370          
c   -- var.elim.:  511000/548370          
c   -- var.elim.:  512000/548370          
c   -- var.elim.:  513000/548370          
c   -- var.elim.:  514000/548370          
c   -- var.elim.:  515000/548370          
c   -- var.elim.:  516000/548370          
c   -- var.elim.:  517000/548370          
c   -- var.elim.:  518000/548370          
c   -- var.elim.:  519000/548370          
c   -- var.elim.:  520000/548370          
c   -- var.elim.:  521000/548370          
c   -- var.elim.:  522000/548370          
c   -- var.elim.:  523000/548370          
c   -- var.elim.:  524000/548370          
c   -- var.elim.:  525000/548370          
c   -- var.elim.:  526000/548370          
c   -- var.elim.:  527000/548370          
c   -- var.elim.:  528000/548370          
c   -- var.elim.:  529000/548370          
c   -- var.elim.:  530000/548370          
c   -- var.elim.:  531000/548370          
c   -- var.elim.:  532000/548370          
c   -- var.elim.:  533000/548370          
c   -- var.elim.:  534000/548370          
c   -- var.elim.:  535000/548370          
c   -- var.elim.:  536000/548370          
c   -- var.elim.:  537000/548370          
c   -- var.elim.:  538000/548370          
c   -- var.elim.:  539000/548370          
c   -- var.elim.:  540000/548370          
c   -- var.elim.:  541000/548370          
c   -- var.elim.:  542000/548370          
c   -- var.elim.:  543000/548370          
c   -- var.elim.:  544000/548370          
c   -- var.elim.:  545000/548370          
c   -- var.elim.:  546000/548370          
c   -- var.elim.:  547000/548370          
c   -- var.elim.:  548000/548370          
c   -- var.elim.:  548370/548370          
c   -- var.elim.:  1000/172427          
c   -- var.elim.:  2000/172427          
c   -- var.elim.:  3000/172427          
c   -- var.elim.:  4000/172427          
c   -- var.elim.:  5000/172427          
c   -- var.elim.:  6000/172427          
c   -- var.elim.:  7000/172427          
c   -- var.elim.:  8000/172427          
c   -- var.elim.:  9000/172427          
c   -- var.elim.:  10000/172427          
c   -- var.elim.:  11000/172427          
c   -- var.elim.:  12000/172427          
c   -- var.elim.:  13000/172427          
c   -- var.elim.:  14000/172427          
c   -- var.elim.:  15000/172427          
c   -- var.elim.:  16000/172427          
c   -- var.elim.:  17000/172427          
c   -- var.elim.:  18000/172427          
c   -- var.elim.:  19000/172427          
c   -- var.elim.:  20000/172427          
c   -- var.elim.:  21000/172427          
c   -- var.elim.:  22000/172427          
c   -- var.elim.:  23000/172427          
c   -- var.elim.:  24000/172427          
c   -- var.elim.:  25000/172427          
c   -- var.elim.:  26000/172427          
c   -- var.elim.:  27000/172427          
c   -- var.elim.:  28000/172427          
c   -- var.elim.:  29000/172427          
c   -- var.elim.:  30000/172427          
c   -- var.elim.:  31000/172427          
c   -- var.elim.:  32000/172427          
c   -- var.elim.:  33000/172427          
c   -- var.elim.:  34000/172427          
c   -- var.elim.:  35000/172427          
c   -- var.elim.:  36000/172427          
c   -- var.elim.:  37000/172427          
c   -- var.elim.:  38000/172427          
c   -- var.elim.:  39000/172427          
c   -- var.elim.:  40000/172427          
c   -- var.elim.:  41000/172427          
c   -- var.elim.:  42000/172427          
c   -- var.elim.:  43000/172427          
c   -- var.elim.:  44000/172427          
c   -- var.elim.:  45000/172427          
c   -- var.elim.:  46000/172427          
c   -- var.elim.:  47000/172427          
c   -- var.elim.:  48000/172427          
c   -- var.elim.:  49000/172427          
c   -- var.elim.:  50000/172427          
c   -- var.elim.:  51000/172427          
c   -- var.elim.:  52000/172427          
c   -- var.elim.:  53000/172427          
c   -- var.elim.:  54000/172427          
c   -- var.elim.:  55000/172427          
c   -- var.elim.:  56000/172427          
c   -- var.elim.:  57000/172427          
c   -- var.elim.:  58000/172427          
c   -- var.elim.:  59000/172427          
c   -- var.elim.:  60000/172427          
c   -- var.elim.:  61000/172427          
c   -- var.elim.:  62000/172427          
c   -- var.elim.:  63000/172427          
c   -- var.elim.:  64000/172427          
c   -- var.elim.:  65000/172427          
c   -- var.elim.:  66000/172427          
c   -- var.elim.:  67000/172427          
c   -- var.elim.:  68000/172427          
c   -- var.elim.:  69000/172427          
c   -- var.elim.:  70000/172427          
c   -- var.elim.:  71000/172427          
c   -- var.elim.:  72000/172427          
c   -- var.elim.:  73000/172427          
c   -- var.elim.:  74000/172427          
c   -- var.elim.:  75000/172427          
c   -- var.elim.:  76000/172427          
c   -- var.elim.:  77000/172427          
c   -- var.elim.:  78000/172427          
c   -- var.elim.:  79000/172427          
c   -- var.elim.:  80000/172427          
c   -- var.elim.:  81000/172427          
c   -- var.elim.:  82000/172427          
c   -- var.elim.:  83000/172427          
c   -- var.elim.:  84000/172427          
c   -- var.elim.:  85000/172427          
c   -- var.elim.:  86000/172427          
c   -- var.elim.:  87000/172427          
c   -- var.elim.:  88000/172427          
c   -- var.elim.:  89000/172427          
c   -- var.elim.:  90000/172427          
c   -- var.elim.:  91000/172427          
c   -- var.elim.:  92000/172427          
c   -- var.elim.:  93000/172427          
c   -- var.elim.:  94000/172427          
c   -- var.elim.:  95000/172427          
c   -- var.elim.:  96000/172427          
c   -- var.elim.:  97000/172427          
c   -- var.elim.:  98000/172427          
c   -- var.elim.:  99000/172427          
c   -- var.elim.:  100000/172427          
c   -- var.elim.:  101000/172427          
c   -- var.elim.:  102000/172427          
c   -- var.elim.:  103000/172427          
c   -- var.elim.:  104000/172427          
c   -- var.elim.:  105000/172427          
c   -- var.elim.:  106000/172427          
c   -- var.elim.:  107000/172427          
c   -- var.elim.:  108000/172427          
c   -- var.elim.:  109000/172427          
c   -- var.elim.:  110000/172427          
c   -- var.elim.:  111000/172427          
c   -- var.elim.:  112000/172427          
c   -- var.elim.:  113000/172427          
c   -- var.elim.:  114000/172427          
c   -- var.elim.:  115000/172427          
c   -- var.elim.:  116000/172427          
c   -- var.elim.:  117000/172427          
c   -- var.elim.:  118000/172427          
c   -- var.elim.:  119000/172427          
c   -- var.elim.:  120000/172427          
c   -- var.elim.:  121000/172427          
c   -- var.elim.:  122000/172427          
c   -- var.elim.:  123000/172427          
c   -- var.elim.:  124000/172427          
c   -- var.elim.:  125000/172427          
c   -- var.elim.:  126000/172427          
c   -- var.elim.:  127000/172427          
c   -- var.elim.:  128000/172427          
c   -- var.elim.:  129000/172427          
c   -- var.elim.:  130000/172427          
c   -- var.elim.:  131000/172427          
c   -- var.elim.:  132000/172427          
c   -- var.elim.:  133000/172427          
c   -- var.elim.:  134000/172427          
c   -- var.elim.:  135000/172427          
c   -- var.elim.:  136000/172427          
c   -- var.elim.:  137000/172427          
c   -- var.elim.:  138000/172427          
c   -- var.elim.:  139000/172427          
c   -- var.elim.:  140000/172427          
c   -- var.elim.:  141000/172427          
c   -- var.elim.:  142000/172427          
c   -- var.elim.:  143000/172427          
c   -- var.elim.:  144000/172427          
c   -- var.elim.:  145000/172427          
c   -- var.elim.:  146000/172427          
c   -- var.elim.:  147000/172427          
c   -- var.elim.:  148000/172427          
c   -- var.elim.:  149000/172427          
c   -- var.elim.:  150000/172427          
c   -- var.elim.:  151000/172427          
c   -- var.elim.:  152000/172427          
c   -- var.elim.:  153000/172427          
c   -- var.elim.:  154000/172427          
c   -- var.elim.:  155000/172427          
c   -- var.elim.:  156000/172427          
c   -- var.elim.:  157000/172427          
c   -- var.elim.:  158000/172427          
c   -- var.elim.:  159000/172427          
c   -- var.elim.:  160000/172427          
c   -- var.elim.:  161000/172427          
c   -- var.elim.:  162000/172427          
c   -- var.elim.:  163000/172427          
c   -- var.elim.:  164000/172427          
c   -- var.elim.:  165000/172427          
c   -- var.elim.:  166000/172427          
c   -- var.elim.:  167000/172427          
c   -- var.elim.:  168000/172427          
c   -- var.elim.:  169000/172427          
c   -- var.elim.:  170000/172427          
c   -- var.elim.:  171000/172427          
c   -- var.elim.:  172000/172427          
c   -- var.elim.:  172427/172427          
c   -- var.elim.:  1000/1418          
c   -- var.elim.:  1418/1418          
c   -- var.elim.:  30/30          
c   -- subsuming                       
c   -- var.elim.:  1000/33756          
c   -- var.elim.:  2000/33756          
c   -- var.elim.:  3000/33756          
c   -- var.elim.:  4000/33756          
c   -- var.elim.:  5000/33756          
c   -- var.elim.:  6000/33756          
c   -- var.elim.:  7000/33756          
c   -- var.elim.:  8000/33756          
c   -- var.elim.:  9000/33756          
c   -- #### 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.66 0.79 0.85 2/54 687
Raw data (stat): 687 (runsolver) R 686 23176 23175 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 547774218 1052672 99 4294967295 134512640 135381576 3221224448 3221219692 135158418 0 2147483391 7 90112 0 0 0 17 1 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0014 s]
Raw data (loadavg): 0.72 0.80 0.85 2/54 687
Raw data (stat): 687 (minisat+) R 686 23176 23175 0 -1 0 7091 0 0 0 975 24 0 0 25 0 1 0 547774218 33140736 6831 4294967295 134512640 134672761 3221224544 3221223936 134580771 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8091 6831 603 41 0 8050 0
vsize: 32364
[startup+20.0023 s]
Raw data (loadavg): 0.76 0.81 0.85 2/54 687
Raw data (stat): 687 (minisat+) R 686 23176 23175 0 -1 0 7320 0 0 0 1974 25 0 0 25 0 1 0 547774218 33136640 6846 4294967295 134512640 134672761 3221224544 3221223528 1075286480 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8090 6846 603 41 0 8049 0
vsize: 32360
[startup+30.0018 s]
Raw data (loadavg): 0.80 0.81 0.85 3/57 725
Raw data (stat): 687 (minisat+) R 686 23176 23175 0 -1 0 12764 0 0 0 2955 42 0 0 25 0 1 0 547774218 51273728 11136 4294967295 134512640 134672761 3221224544 3221173744 134592562 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12518 11136 603 41 0 12477 0
vsize: 50072
[startup+40.0042 s]
Raw data (loadavg): 0.90 0.83 0.86 2/54 740
Raw data (stat): 687 (minisat+) R 686 23176 23175 0 -1 0 44036 0 0 0 3873 123 0 0 25 0 1 0 547774218 183697408 42408 4294967295 134512640 134672761 3221224544 3221213984 134604097 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 44848 42408 603 41 0 44807 0
vsize: 179392
[startup+50.0047 s]
Raw data (loadavg): 0.91 0.84 0.86 2/54 740
Raw data (stat): 687 (minisat+) R 686 23176 23175 0 -1 0 94599 0 0 0 4745 251 0 0 25 0 1 0 547774218 459771904 92946 4294967295 134512640 134672761 3221224544 3221223392 134542427 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 112249 92946 603 41 0 112208 0
vsize: 448996
[startup+60.0059 s]
Raw data (loadavg): 0.93 0.84 0.86 2/54 740
Raw data (stat): 687 (minisat+) R 686 23176 23175 0 -1 0 95516 0 0 0 5742 253 0 0 25 0 1 0 547774218 467484672 93863 4294967295 134512640 134672761 3221224544 3221223088 134621512 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 114132 93863 603 41 0 114091 0
vsize: 456528
[startup+70.0066 s]
Raw data (loadavg): 0.94 0.85 0.86 2/54 740
Raw data (stat): 687 (minisat+) R 686 23176 23175 0 -1 0 100110 0 0 0 6731 265 0 0 25 0 1 0 547774218 473874432 94971 4294967295 134512640 134672761 3221224544 3221222980 1075347048 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 115692 94971 603 41 0 115651 0
vsize: 462768
[startup+80.0064 s]
Raw data (loadavg): 0.95 0.85 0.86 2/54 740
Raw data (stat): 687 (minisat+) R 686 23176 23175 0 -1 0 100206 0 0 0 7707 285 0 0 25 0 1 0 547774218 474398720 95067 4294967295 134512640 134672761 3221224544 3221222746 134566630 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 115820 95067 603 41 0 115779 0
vsize: 463280
[startup+90.0065 s]
Raw data (loadavg): 0.95 0.86 0.86 2/54 740
Raw data (stat): 687 (minisat+) R 686 23176 23175 0 -1 0 100479 0 0 0 8693 299 0 0 25 0 1 0 547774218 473440256 94772 4294967295 134512640 134672761 3221224544 3221222992 134643612 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 115586 94772 603 41 0 115545 0
vsize: 462344
[startup+100.006 s]
Raw data (loadavg): 0.96 0.86 0.86 2/54 740
Raw data (stat): 687 (minisat+) R 686 23176 23175 0 -1 0 106502 0 0 0 9681 312 0 0 25 0 1 0 547774218 495345664 100003 4294967295 134512640 134672761 3221224544 3221223088 134621186 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 120934 100003 603 41 0 120893 0
vsize: 483736
[startup+110.008 s]
Raw data (loadavg): 0.97 0.87 0.86 2/54 742
Raw data (stat): 687 (minisat+) R 686 23176 23175 0 -1 0 117184 0 0 0 10651 341 0 0 25 0 1 0 547774218 470294528 94389 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 114818 94389 603 41 0 114777 0
vsize: 459272
[startup+120.008 s]
Raw data (loadavg): 0.97 0.87 0.86 2/54 742
Raw data (stat): 687 (minisat+) R 686 23176 23175 0 -1 0 117184 0 0 0 11651 342 0 0 25 0 1 0 547774218 470294528 94389 4294967295 134512640 134672761 3221224544 3221223728 134615676 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 114818 94389 603 41 0 114777 0
vsize: 459272
[startup+130.008 s]
Raw data (loadavg): 0.98 0.87 0.86 2/54 742
Raw data (stat): 687 (minisat+) R 686 23176 23175 0 -1 0 117198 0 0 0 12651 342 0 0 25 0 1 0 547774218 470429696 94403 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 114851 94403 603 41 0 114810 0
vsize: 459404
[startup+140.008 s]
Raw data (loadavg): 0.98 0.88 0.87 2/54 742
Raw data (stat): 687 (minisat+) R 686 23176 23175 0 -1 0 117214 0 0 0 13652 342 0 0 25 0 1 0 547774218 470429696 94419 4294967295 134512640 134672761 3221224544 3221223728 134615991 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 114851 94419 603 41 0 114810 0
vsize: 459404
[startup+150.009 s]
Raw data (loadavg): 0.98 0.88 0.87 2/54 742
Raw data (stat): 687 (minisat+) R 686 23176 23175 0 -1 0 117238 0 0 0 14652 342 0 0 25 0 1 0 547774218 470687744 94443 4294967295 134512640 134672761 3221224544 3221223728 134615549 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 114914 94443 603 41 0 114873 0
vsize: 459656
[startup+160.009 s]
Raw data (loadavg): 0.98 0.88 0.87 2/54 742
Raw data (stat): 687 (minisat+) R 686 23176 23175 0 -1 0 117242 0 0 0 15652 342 0 0 25 0 1 0 547774218 470687744 94447 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 114914 94447 603 41 0 114873 0
vsize: 459656
[startup+170.009 s]
Raw data (loadavg): 0.99 0.89 0.87 2/54 742
Raw data (stat): 687 (minisat+) R 686 23176 23175 0 -1 0 117245 0 0 0 16652 342 0 0 25 0 1 0 547774218 470687744 94450 4294967295 134512640 134672761 3221224544 3221223744 134610707 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 114914 94450 603 41 0 114873 0
vsize: 459656
[startup+180.009 s]
Raw data (loadavg): 0.99 0.89 0.87 2/54 742
Raw data (stat): 687 (minisat+) R 686 23176 23175 0 -1 0 117249 0 0 0 17652 342 0 0 25 0 1 0 547774218 470687744 94454 4294967295 134512640 134672761 3221224544 3221223668 134566043 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 114914 94454 603 41 0 114873 0
vsize: 459656
[startup+190.01 s]
Raw data (loadavg): 0.99 0.89 0.87 2/54 742
Raw data (stat): 687 (minisat+) R 686 23176 23175 0 -1 0 117251 0 0 0 18652 342 0 0 25 0 1 0 547774218 470687744 94456 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 114914 94456 603 41 0 114873 0
vsize: 459656
[startup+200.01 s]
Raw data (loadavg): 0.99 0.90 0.87 2/54 742
Raw data (stat): 687 (minisat+) R 686 23176 23175 0 -1 0 117253 0 0 0 19653 342 0 0 25 0 1 0 547774218 470687744 94458 4294967295 134512640 134672761 3221224544 3221223688 134616299 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 114914 94458 603 41 0 114873 0
vsize: 459656
[startup+210.011 s]
Raw data (loadavg): 0.99 0.90 0.87 2/54 742
Raw data (stat): 687 (minisat+) R 686 23176 23175 0 -1 0 117256 0 0 0 20653 342 0 0 25 0 1 0 547774218 470687744 94461 4294967295 134512640 134672761 3221224544 3221223728 134615549 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 114914 94461 603 41 0 114873 0
vsize: 459656
[startup+220.012 s]
Raw data (loadavg): 0.99 0.90 0.87 2/54 742
Raw data (stat): 687 (minisat+) R 686 23176 23175 0 -1 0 117259 0 0 0 21653 342 0 0 25 0 1 0 547774218 470822912 94464 4294967295 134512640 134672761 3221224544 3221223728 134615549 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 114947 94464 603 41 0 114906 0
vsize: 459788
[startup+230.012 s]
Raw data (loadavg): 0.99 0.91 0.87 2/54 742
Raw data (stat): 687 (minisat+) R 686 23176 23175 0 -1 0 117269 0 0 0 22653 342 0 0 25 0 1 0 547774218 470822912 94474 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 114947 94474 603 41 0 114906 0
vsize: 459788
[startup+240.012 s]
Raw data (loadavg): 0.99 0.91 0.88 2/54 742
Raw data (stat): 687 (minisat+) R 686 23176 23175 0 -1 0 117306 0 0 0 23653 342 0 0 25 0 1 0 547774218 470958080 94511 4294967295 134512640 134672761 3221224544 3221223584 134612739 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 114980 94511 603 41 0 114939 0
vsize: 459920
[startup+250.012 s]
Raw data (loadavg): 0.99 0.91 0.88 2/54 742
Raw data (stat): 687 (minisat+) R 686 23176 23175 0 -1 0 117329 0 0 0 24653 342 0 0 25 0 1 0 547774218 470958080 94534 4294967295 134512640 134672761 3221224544 3221223728 134615940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 114980 94534 603 41 0 114939 0
vsize: 459920
[startup+260.013 s]
Raw data (loadavg): 0.99 0.91 0.88 2/54 742
Raw data (stat): 687 (minisat+) R 686 23176 23175 0 -1 0 117361 0 0 0 25654 342 0 0 25 0 1 0 547774218 471089152 94566 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 115012 94566 603 41 0 114971 0
vsize: 460048
[startup+270.013 s]
Raw data (loadavg): 0.99 0.92 0.88 2/54 742
Raw data (stat): 687 (minisat+) R 686 23176 23175 0 -1 0 117383 0 0 0 26654 342 0 0 25 0 1 0 547774218 471224320 94588 4294967295 134512640 134672761 3221224544 3221223728 134615732 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 115045 94588 603 41 0 115004 0
vsize: 460180
[startup+280.013 s]
Raw data (loadavg): 0.99 0.92 0.88 2/54 742
Raw data (stat): 687 (minisat+) R 686 23176 23175 0 -1 0 117638 0 0 0 27653 343 0 0 25 0 1 0 547774218 472281088 94843 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 115303 94843 603 41 0 115262 0
vsize: 461212
[startup+290.014 s]
Raw data (loadavg): 0.99 0.92 0.88 2/54 742
Raw data (stat): 687 (minisat+) R 686 23176 23175 0 -1 0 117754 0 0 0 28653 344 0 0 25 0 1 0 547774218 472682496 94959 4294967295 134512640 134672761 3221224544 3221223728 134615991 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 115401 94959 603 41 0 115360 0
vsize: 461604
[startup+300.014 s]
Raw data (loadavg): 0.99 0.92 0.88 2/54 742
Raw data (stat): 687 (minisat+) R 686 23176 23175 0 -1 0 117775 0 0 0 29653 344 0 0 25 0 1 0 547774218 472817664 94980 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 115434 94980 603 41 0 115393 0
vsize: 461736
[startup+310.015 s]
Raw data (loadavg): 0.99 0.92 0.88 2/54 742
Raw data (stat): 687 (minisat+) R 686 23176 23175 0 -1 0 117796 0 0 0 30653 344 0 0 25 0 1 0 547774218 472817664 95001 4294967295 134512640 134672761 3221224544 3221223728 134615663 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 115434 95001 603 41 0 115393 0
vsize: 461736
[startup+320.016 s]
Raw data (loadavg): 0.99 0.93 0.88 2/54 742
Raw data (stat): 687 (minisat+) R 686 23176 23175 0 -1 0 117870 0 0 0 31653 344 0 0 25 0 1 0 547774218 473341952 95075 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 115562 95075 603 41 0 115521 0
vsize: 462248
[startup+330.016 s]
Raw data (loadavg): 0.99 0.93 0.88 2/54 742
Raw data (stat): 687 (minisat+) R 686 23176 23175 0 -1 0 117872 0 0 0 32653 344 0 0 25 0 1 0 547774218 473341952 95077 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 115562 95077 603 41 0 115521 0
vsize: 462248
[startup+340.017 s]
Raw data (loadavg): 0.99 0.93 0.89 2/54 744
Raw data (stat): 687 (minisat+) R 686 23176 23175 0 -1 0 117874 0 0 0 33653 344 0 0 25 0 1 0 547774218 473341952 95079 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 115562 95079 603 41 0 115521 0
vsize: 462248
[startup+350.017 s]
Raw data (loadavg): 0.99 0.93 0.89 2/54 744
Raw data (stat): 687 (minisat+) R 686 23176 23175 0 -1 0 117896 0 0 0 34653 344 0 0 25 0 1 0 547774218 473477120 95101 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 115595 95101 603 41 0 115554 0
vsize: 462380
[startup+360.017 s]
Raw data (loadavg): 0.99 0.93 0.89 2/54 744
Raw data (stat): 687 (minisat+) R 686 23176 23175 0 -1 0 117914 0 0 0 35653 344 0 0 25 0 1 0 547774218 473608192 95119 4294967295 134512640 134672761 3221224544 3221223668 134566034 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 115627 95119 603 41 0 115586 0
vsize: 462508
[startup+370.017 s]
Raw data (loadavg): 0.99 0.94 0.89 2/54 744
Raw data (stat): 687 (minisat+) R 686 23176 23175 0 -1 0 117933 0 0 0 36653 344 0 0 25 0 1 0 547774218 473608192 95138 4294967295 134512640 134672761 3221224544 3221223728 134615663 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 115627 95138 603 41 0 115586 0
vsize: 462508
[startup+380.018 s]
Raw data (loadavg): 0.99 0.94 0.89 2/54 744
Raw data (stat): 687 (minisat+) R 686 23176 23175 0 -1 0 117971 0 0 0 37653 344 0 0 25 0 1 0 547774218 473739264 95176 4294967295 134512640 134672761 3221224544 3221223728 134615663 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 115659 95176 603 41 0 115618 0
vsize: 462636
[startup+390.019 s]
Raw data (loadavg): 0.99 0.94 0.89 2/54 744
Raw data (stat): 687 (minisat+) R 686 23176 23175 0 -1 0 118019 0 0 0 38653 345 0 0 25 0 1 0 547774218 474009600 95224 4294967295 134512640 134672761 3221224544 3221223712 134615859 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 115725 95224 603 41 0 115684 0
vsize: 462900
[startup+400.018 s]
Raw data (loadavg): 0.99 0.94 0.89 2/54 744
Raw data (stat): 687 (minisat+) R 686 23176 23175 0 -1 0 118189 0 0 0 39653 345 0 0 25 0 1 0 547774218 474669056 95394 4294967295 134512640 134672761 3221224544 3221223696 134565137 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 115886 95394 603 41 0 115845 0
vsize: 463544
[startup+410.019 s]
Raw data (loadavg): 0.99 0.94 0.89 2/54 744
Raw data (stat): 687 (minisat+) R 686 23176 23175 0 -1 0 118207 0 0 0 40653 345 0 0 25 0 1 0 547774218 474669056 95412 4294967295 134512640 134672761 3221224544 3221223728 134615583 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 115886 95412 603 41 0 115845 0
vsize: 463544
[startup+420.019 s]
Raw data (loadavg): 0.99 0.94 0.89 2/54 744
Raw data (stat): 687 (minisat+) R 686 23176 23175 0 -1 0 118228 0 0 0 41653 345 0 0 25 0 1 0 547774218 474800128 95433 4294967295 134512640 134672761 3221224544 3221223728 134615916 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 115918 95433 603 41 0 115877 0
vsize: 463672
[startup+430.019 s]
Raw data (loadavg): 0.99 0.94 0.89 2/54 744
Raw data (stat): 687 (minisat+) R 686 23176 23175 0 -1 0 118247 0 0 0 42654 345 0 0 25 0 1 0 547774218 474800128 95452 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 115918 95452 603 41 0 115877 0
vsize: 463672
[startup+440.019 s]
Raw data (loadavg): 0.99 0.95 0.89 2/54 744
Raw data (stat): 687 (minisat+) R 686 23176 23175 0 -1 0 118493 0 0 0 43653 346 0 0 25 0 1 0 547774218 475860992 95698 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 116177 95698 603 41 0 116136 0
vsize: 464708
[startup+450.019 s]
Raw data (loadavg): 0.99 0.95 0.90 2/54 744
Raw data (stat): 687 (minisat+) R 686 23176 23175 0 -1 0 118819 0 0 0 44652 347 0 0 25 0 1 0 547774218 477179904 96024 4294967295 134512640 134672761 3221224544 3221223728 134615549 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 116499 96024 603 41 0 116458 0
vsize: 465996
[startup+460.02 s]
Raw data (loadavg): 0.99 0.95 0.90 2/54 744
Raw data (stat): 687 (minisat+) R 686 23176 23175 0 -1 0 118848 0 0 0 45652 347 0 0 25 0 1 0 547774218 477179904 96053 4294967295 134512640 134672761 3221224544 3221223696 134565086 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 116499 96053 603 41 0 116458 0
vsize: 465996
[startup+470.02 s]
Raw data (loadavg): 0.99 0.95 0.90 2/54 744
Raw data (stat): 687 (minisat+) R 686 23176 23175 0 -1 0 118861 0 0 0 46652 347 0 0 25 0 1 0 547774218 477315072 96066 4294967295 134512640 134672761 3221224544 3221223744 134610661 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 116532 96066 603 41 0 116491 0
vsize: 466128
[startup+480.02 s]
Raw data (loadavg): 0.99 0.95 0.90 2/54 744
Raw data (stat): 687 (minisat+) R 686 23176 23175 0 -1 0 119028 0 0 0 47652 348 0 0 25 0 1 0 547774218 477978624 96233 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 116694 96233 603 41 0 116653 0
vsize: 466776
[startup+490.021 s]
Raw data (loadavg): 0.99 0.95 0.90 2/54 744
Raw data (stat): 687 (minisat+) R 686 23176 23175 0 -1 0 119052 0 0 0 48652 348 0 0 25 0 1 0 547774218 478113792 96257 4294967295 134512640 134672761 3221224544 3221223536 134565092 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 116727 96257 603 41 0 116686 0
vsize: 466908
[startup+500.021 s]
Raw data (loadavg): 0.99 0.95 0.90 2/54 744
Raw data (stat): 687 (minisat+) R 686 23176 23175 0 -1 0 119075 0 0 0 49652 348 0 0 25 0 1 0 547774218 478113792 96280 4294967295 134512640 134672761 3221224544 3221223728 134615951 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 116727 96280 603 41 0 116686 0
vsize: 466908
[startup+510.021 s]
Raw data (loadavg): 0.99 0.95 0.90 2/54 744
Raw data (stat): 687 (minisat+) R 686 23176 23175 0 -1 0 119091 0 0 0 50652 348 0 0 25 0 1 0 547774218 478248960 96296 4294967295 134512640 134672761 3221224544 3221223728 134615549 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 116760 96296 603 41 0 116719 0
vsize: 467040
[startup+520.022 s]
Raw data (loadavg): 0.99 0.95 0.90 2/54 744
Raw data (stat): 687 (minisat+) R 686 23176 23175 0 -1 0 119110 0 0 0 51652 348 0 0 25 0 1 0 547774218 478248960 96315 4294967295 134512640 134672761 3221224544 3221223744 134610661 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 116760 96315 603 41 0 116719 0
vsize: 467040
[startup+530.022 s]
Raw data (loadavg): 0.99 0.95 0.90 2/54 744
Raw data (stat): 687 (minisat+) R 686 23176 23175 0 -1 0 119122 0 0 0 52652 348 0 0 25 0 1 0 547774218 478248960 96327 4294967295 134512640 134672761 3221224544 3221223728 134615594 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 116760 96327 603 41 0 116719 0
vsize: 467040
[startup+540.022 s]
Raw data (loadavg): 0.99 0.95 0.90 2/54 744
Raw data (stat): 687 (minisat+) R 686 23176 23175 0 -1 0 119264 0 0 0 53652 349 0 0 25 0 1 0 547774218 478912512 96469 4294967295 134512640 134672761 3221224544 3221223728 134615940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 116922 96469 603 41 0 116881 0
vsize: 467688
[startup+550.022 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 744
Raw data (stat): 687 (minisat+) R 686 23176 23175 0 -1 0 119296 0 0 0 54652 349 0 0 25 0 1 0 547774218 479047680 96501 4294967295 134512640 134672761 3221224544 3221223688 134616136 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 116955 96501 603 41 0 116914 0
vsize: 467820
[startup+560.023 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 744
Raw data (stat): 687 (minisat+) R 686 23176 23175 0 -1 0 119354 0 0 0 55652 349 0 0 25 0 1 0 547774218 479178752 96559 4294967295 134512640 134672761 3221224544 3221223728 134615739 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 116987 96559 603 41 0 116946 0
vsize: 467948
[startup+570.024 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 744
Raw data (stat): 687 (minisat+) R 686 23176 23175 0 -1 0 119398 0 0 0 56652 349 0 0 25 0 1 0 547774218 479449088 96603 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 117053 96603 603 41 0 117012 0
vsize: 468212
[startup+580.024 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 744
Raw data (stat): 687 (minisat+) R 686 23176 23175 0 -1 0 119434 0 0 0 57652 350 0 0 25 0 1 0 547774218 479580160 96639 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 117085 96639 603 41 0 117044 0
vsize: 468340
[startup+590.025 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 744
Raw data (stat): 687 (minisat+) R 686 23176 23175 0 -1 0 119471 0 0 0 58652 350 0 0 25 0 1 0 547774218 480239616 96676 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 117246 96676 603 41 0 117205 0
vsize: 468984
[startup+600.025 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 744
Raw data (stat): 687 (minisat+) R 686 23176 23175 0 -1 0 119571 0 0 0 59652 350 0 0 25 0 1 0 547774218 480636928 96776 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 117343 96776 603 41 0 117302 0
vsize: 469372
[startup+610.026 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 744
Raw data (stat): 687 (minisat+) R 686 23176 23175 0 -1 0 120101 0 0 0 60651 352 0 0 25 0 1 0 547774218 482750464 97306 4294967295 134512640 134672761 3221224544 3221223728 134615627 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 117859 97306 603 41 0 117818 0
vsize: 471436
[startup+620.026 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 744
Raw data (stat): 687 (minisat+) R 686 23176 23175 0 -1 0 120596 0 0 0 61650 353 0 0 25 0 1 0 547774218 484737024 97801 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 118344 97801 603 41 0 118303 0
vsize: 473376
[startup+630.026 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 744
Raw data (stat): 687 (minisat+) R 686 23176 23175 0 -1 0 121030 0 0 0 62649 354 0 0 25 0 1 0 547774218 486576128 98235 4294967295 134512640 134672761 3221224544 3221223680 134614701 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 118793 98235 603 41 0 118752 0
vsize: 475172
[startup+640.032 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 744
Raw data (stat): 687 (minisat+) R 686 23176 23175 0 -1 0 121405 0 0 0 63649 355 0 0 25 0 1 0 547774218 488026112 98610 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 119147 98610 603 41 0 119106 0
vsize: 476588
[startup+650.031 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 744
Raw data (stat): 687 (minisat+) R 686 23176 23175 0 -1 0 121561 0 0 0 64648 355 0 0 25 0 1 0 547774218 488693760 98766 4294967295 134512640 134672761 3221224544 3221223728 134615929 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 119310 98766 603 41 0 119269 0
vsize: 477240
[startup+660.033 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 744
Raw data (stat): 687 (minisat+) R 686 23176 23175 0 -1 0 121796 0 0 0 65648 356 0 0 25 0 1 0 547774218 489627648 99001 4294967295 134512640 134672761 3221224544 3221223356 1075352235 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 119538 99001 603 41 0 119497 0
vsize: 478152
[startup+670.033 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 744
Raw data (stat): 687 (minisat+) R 686 23176 23175 0 -1 0 122050 0 0 0 66648 356 0 0 25 0 1 0 547774218 490688512 99255 4294967295 134512640 134672761 3221224544 3221223728 134615720 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 119797 99255 603 41 0 119756 0
vsize: 479188
[startup+680.034 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 744
Raw data (stat): 687 (minisat+) R 686 23176 23175 0 -1 0 122239 0 0 0 67647 357 0 0 25 0 1 0 547774218 491474944 99444 4294967295 134512640 134672761 3221224544 3221223728 134615788 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 119989 99444 603 41 0 119948 0
vsize: 479956
[startup+690.034 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 744
Raw data (stat): 687 (minisat+) R 686 23176 23175 0 -1 0 122436 0 0 0 68647 357 0 0 25 0 1 0 547774218 492281856 99641 4294967295 134512640 134672761 3221224544 3221223728 134615705 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 120186 99641 603 41 0 120145 0
vsize: 480744
[startup+700.034 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 744
Raw data (stat): 687 (minisat+) R 686 23176 23175 0 -1 0 122602 0 0 0 69647 358 0 0 25 0 1 0 547774218 492941312 99807 4294967295 134512640 134672761 3221224544 3221223728 134615564 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 120347 99807 603 41 0 120306 0
vsize: 481388
[startup+710.036 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 744
Raw data (stat): 687 (minisat+) R 686 23176 23175 0 -1 0 122786 0 0 0 70646 358 0 0 25 0 1 0 547774218 493608960 99991 4294967295 134512640 134672761 3221224544 3221223728 134615601 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 120510 99991 603 41 0 120469 0
vsize: 482040
[startup+720.036 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 744
Raw data (stat): 687 (minisat+) R 686 23176 23175 0 -1 0 122985 0 0 0 71646 359 0 0 25 0 1 0 547774218 494399488 100190 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 120703 100190 603 41 0 120662 0
vsize: 482812
[startup+730.036 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 744
Raw data (stat): 687 (minisat+) R 686 23176 23175 0 -1 0 123169 0 0 0 72646 359 0 0 25 0 1 0 547774218 495267840 100374 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 120915 100374 603 41 0 120874 0
vsize: 483660
[startup+740.037 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 744
Raw data (stat): 687 (minisat+) R 686 23176 23175 0 -1 0 123376 0 0 0 73646 360 0 0 25 0 1 0 547774218 496070656 100581 4294967295 134512640 134672761 3221224544 3221223680 134614488 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 121111 100581 603 41 0 121070 0
vsize: 484444
[startup+750.037 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 744
Raw data (stat): 687 (minisat+) R 686 23176 23175 0 -1 0 123572 0 0 0 74645 360 0 0 25 0 1 0 547774218 496861184 100777 4294967295 134512640 134672761 3221224544 3221223728 134615663 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 121304 100777 603 41 0 121263 0
vsize: 485216
[startup+760.038 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 744
Raw data (stat): 687 (minisat+) R 686 23176 23175 0 -1 0 123755 0 0 0 75645 361 0 0 25 0 1 0 547774218 497651712 100960 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 121497 100960 603 41 0 121456 0
vsize: 485988
[startup+770.038 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 744
Raw data (stat): 687 (minisat+) R 686 23176 23175 0 -1 0 123948 0 0 0 76644 362 0 0 25 0 1 0 547774218 498454528 101153 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 121693 101153 603 41 0 121652 0
vsize: 486772
[startup+780.038 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 744
Raw data (stat): 687 (minisat+) R 686 23176 23175 0 -1 0 124117 0 0 0 77643 363 0 0 25 0 1 0 547774218 499122176 101322 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 121856 101322 603 41 0 121815 0
vsize: 487424
[startup+790.038 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 744
Raw data (stat): 687 (minisat+) R 686 23176 23175 0 -1 0 124315 0 0 0 78643 363 0 0 25 0 1 0 547774218 499933184 101520 4294967295 134512640 134672761 3221224544 3221223728 134615638 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 122054 101520 603 41 0 122013 0
vsize: 488216
[startup+800.039 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 744
Raw data (stat): 687 (minisat+) R 686 23176 23175 0 -1 0 124391 0 0 0 79643 363 0 0 25 0 1 0 547774218 500203520 101596 4294967295 134512640 134672761 3221224544 3221223728 134615929 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 122120 101596 603 41 0 122079 0
vsize: 488480
[startup+810.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 744
Raw data (stat): 687 (minisat+) R 686 23176 23175 0 -1 0 124426 0 0 0 80643 363 0 0 25 0 1 0 547774218 500338688 101631 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 122153 101631 603 41 0 122112 0
vsize: 488612
[startup+820.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 744
Raw data (stat): 687 (minisat+) R 686 23176 23175 0 -1 0 124770 0 0 0 81642 364 0 0 25 0 1 0 547774218 501792768 101975 4294967295 134512640 134672761 3221224544 3221223584 134614286 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 122508 101975 603 41 0 122467 0
vsize: 490032
[startup+830.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 744
Raw data (stat): 687 (minisat+) R 686 23176 23175 0 -1 0 124965 0 0 0 82642 365 0 0 25 0 1 0 547774218 502591488 102170 4294967295 134512640 134672761 3221224544 3221223728 134615681 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 122703 102170 603 41 0 122662 0
vsize: 490812
[startup+840.043 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 744
Raw data (stat): 687 (minisat+) R 686 23176 23175 0 -1 0 124988 0 0 0 83642 365 0 0 25 0 1 0 547774218 502591488 102193 4294967295 134512640 134672761 3221224544 3221223696 134565092 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 122703 102193 603 41 0 122662 0
vsize: 490812
[startup+850.045 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 744
Raw data (stat): 687 (minisat+) R 686 23176 23175 0 -1 0 125011 0 0 0 84643 365 0 0 25 0 1 0 547774218 502726656 102216 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 122736 102216 603 41 0 122695 0
vsize: 490944
[startup+860.047 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 744
Raw data (stat): 687 (minisat+) R 686 23176 23175 0 -1 0 125045 0 0 0 85643 365 0 0 25 0 1 0 547774218 502857728 102250 4294967295 134512640 134672761 3221224544 3221223744 134610707 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 122768 102250 603 41 0 122727 0
vsize: 491072
[startup+870.047 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 744
Raw data (stat): 687 (minisat+) R 686 23176 23175 0 -1 0 125083 0 0 0 86643 366 0 0 25 0 1 0 547774218 502988800 102288 4294967295 134512640 134672761 3221224544 3221223696 134565073 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 122800 102288 603 41 0 122759 0
vsize: 491200
[startup+880.048 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 744
Raw data (stat): 687 (minisat+) R 686 23176 23175 0 -1 0 125139 0 0 0 87643 366 0 0 25 0 1 0 547774218 503259136 102344 4294967295 134512640 134672761 3221224544 3221223680 134614690 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 122866 102344 603 41 0 122825 0
vsize: 491464
[startup+890.049 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 744
Raw data (stat): 687 (minisat+) R 686 23176 23175 0 -1 0 125176 0 0 0 88643 366 0 0 25 0 1 0 547774218 503390208 102381 4294967295 134512640 134672761 3221224544 3221223728 134615747 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 122898 102381 603 41 0 122857 0
vsize: 491592
[startup+900.049 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 744
Raw data (stat): 687 (minisat+) R 686 23176 23175 0 -1 0 125210 0 0 0 89643 366 0 0 25 0 1 0 547774218 503521280 102415 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 122930 102415 603 41 0 122889 0
vsize: 491720
[startup+910.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 744
Raw data (stat): 687 (minisat+) R 686 23176 23175 0 -1 0 125243 0 0 0 90643 366 0 0 25 0 1 0 547774218 503652352 102448 4294967295 134512640 134672761 3221224544 3221223728 134615673 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 122962 102448 603 41 0 122921 0
vsize: 491848
[startup+920.051 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 744
Raw data (stat): 687 (minisat+) R 686 23176 23175 0 -1 0 125270 0 0 0 91643 366 0 0 25 0 1 0 547774218 503787520 102475 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 122995 102475 603 41 0 122954 0
vsize: 491980
[startup+930.061 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 744
Raw data (stat): 687 (minisat+) R 686 23176 23175 0 -1 0 125306 0 0 0 92645 366 0 0 25 0 1 0 547774218 503922688 102511 4294967295 134512640 134672761 3221224544 3221223744 134610646 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 123028 102511 603 41 0 122987 0
vsize: 492112
[startup+940.062 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 744
Raw data (stat): 687 (minisat+) R 686 23176 23175 0 -1 0 125435 0 0 0 93644 367 0 0 25 0 1 0 547774218 504451072 102640 4294967295 134512640 134672761 3221224544 3221223728 134615705 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 123157 102640 603 41 0 123116 0
vsize: 492628
[startup+950.063 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 744
Raw data (stat): 687 (minisat+) R 686 23176 23175 0 -1 0 125854 0 0 0 94643 368 0 0 25 0 1 0 547774218 506167296 103059 4294967295 134512640 134672761 3221224544 3221223744 134610661 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 123576 103059 603 41 0 123535 0
vsize: 494304
[startup+960.071 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 744
Raw data (stat): 687 (minisat+) R 686 23176 23175 0 -1 0 126221 0 0 0 95643 369 0 0 25 0 1 0 547774218 507629568 103426 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 123933 103426 603 41 0 123892 0
vsize: 495732
[startup+970.173 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 744
Raw data (stat): 687 (minisat+) R 686 23176 23175 0 -1 0 126577 0 0 0 96651 372 0 0 25 0 1 0 547774218 509087744 103782 4294967295 134512640 134672761 3221224544 3221223728 134615791 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 124289 103782 603 41 0 124248 0
vsize: 497156
[startup+980.174 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 744
Raw data (stat): 687 (minisat+) R 686 23176 23175 0 -1 0 126810 0 0 0 97650 373 0 0 25 0 1 0 547774218 510017536 104015 4294967295 134512640 134672761 3221224544 3221223728 134615579 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 124516 104015 603 41 0 124475 0
vsize: 498064
[startup+990.174 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 744
Raw data (stat): 687 (minisat+) R 686 23176 23175 0 -1 0 126919 0 0 0 98650 373 0 0 25 0 1 0 547774218 510414848 104124 4294967295 134512640 134672761 3221224544 3221223744 134610707 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 124613 104124 603 41 0 124572 0
vsize: 498452
[startup+1000.17 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 744
Raw data (stat): 687 (minisat+) R 686 23176 23175 0 -1 0 126948 0 0 0 99650 373 0 0 25 0 1 0 547774218 510550016 104153 4294967295 134512640 134672761 3221224544 3221223668 134566012 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 124646 104153 603 41 0 124605 0
vsize: 498584
[startup+1010.18 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 744
Raw data (stat): 687 (minisat+) R 686 23176 23175 0 -1 0 126974 0 0 0 100651 373 0 0 25 0 1 0 547774218 510685184 104179 4294967295 134512640 134672761 3221224544 3221223728 134615660 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 124679 104179 603 41 0 124638 0
vsize: 498716
[startup+1020.18 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 744
Raw data (stat): 687 (minisat+) R 686 23176 23175 0 -1 0 126998 0 0 0 101651 373 0 0 25 0 1 0 547774218 510816256 104203 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 124711 104203 603 41 0 124670 0
vsize: 498844
[startup+1030.18 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 744
Raw data (stat): 687 (minisat+) R 686 23176 23175 0 -1 0 127045 0 0 0 102651 373 0 0 25 0 1 0 547774218 510951424 104250 4294967295 134512640 134672761 3221224544 3221223728 134615549 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 124744 104250 603 41 0 124703 0
vsize: 498976
[startup+1040.18 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 744
Raw data (stat): 687 (minisat+) R 686 23176 23175 0 -1 0 127070 0 0 0 103651 373 0 0 25 0 1 0 547774218 511082496 104275 4294967295 134512640 134672761 3221224544 3221223728 134615549 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 124776 104275 603 41 0 124735 0
vsize: 499104
[startup+1050.18 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 744
Raw data (stat): 687 (minisat+) R 686 23176 23175 0 -1 0 127099 0 0 0 104651 373 0 0 25 0 1 0 547774218 511082496 104304 4294967295 134512640 134672761 3221224544 3221223728 134615807 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 124776 104304 603 41 0 124735 0
vsize: 499104
[startup+1060.19 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 744
Raw data (stat): 687 (minisat+) R 686 23176 23175 0 -1 0 127126 0 0 0 105652 373 0 0 25 0 1 0 547774218 511217664 104331 4294967295 134512640 134672761 3221224544 3221223744 134610707 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 124809 104331 603 41 0 124768 0
vsize: 499236
[startup+1070.19 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 744
Raw data (stat): 687 (minisat+) R 686 23176 23175 0 -1 0 127146 0 0 0 106652 374 0 0 25 0 1 0 547774218 511352832 104351 4294967295 134512640 134672761 3221224544 3221223688 134616111 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 124842 104351 603 41 0 124801 0
vsize: 499368
[startup+1080.19 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 744
Raw data (stat): 687 (minisat+) R 686 23176 23175 0 -1 0 127187 0 0 0 107652 374 0 0 25 0 1 0 547774218 511488000 104392 4294967295 134512640 134672761 3221224544 3221223688 134616293 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 124875 104392 603 41 0 124834 0
vsize: 499500
[startup+1090.19 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 744
Raw data (stat): 687 (minisat+) R 686 23176 23175 0 -1 0 127208 0 0 0 108653 374 0 0 25 0 1 0 547774218 511623168 104413 4294967295 134512640 134672761 3221224544 3221223728 134615940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 124908 104413 603 41 0 124867 0
vsize: 499632
[startup+1100.19 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 744
Raw data (stat): 687 (minisat+) R 686 23176 23175 0 -1 0 127227 0 0 0 109653 374 0 0 25 0 1 0 547774218 511623168 104432 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 124908 104432 603 41 0 124867 0
vsize: 499632
[startup+1110.19 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 744
Raw data (stat): 687 (minisat+) R 686 23176 23175 0 -1 0 127266 0 0 0 110653 374 0 0 25 0 1 0 547774218 511758336 104471 4294967295 134512640 134672761 3221224544 3221223668 134566031 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 124941 104471 603 41 0 124900 0
vsize: 499764
[startup+1120.2 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 744
Raw data (stat): 687 (minisat+) R 686 23176 23175 0 -1 0 127285 0 0 0 111653 374 0 0 25 0 1 0 547774218 511889408 104490 4294967295 134512640 134672761 3221224544 3221223728 134615671 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 124973 104490 603 41 0 124932 0
vsize: 499892
[startup+1130.2 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 744
Raw data (stat): 687 (minisat+) R 686 23176 23175 0 -1 0 127308 0 0 0 112653 374 0 0 25 0 1 0 547774218 512024576 104513 4294967295 134512640 134672761 3221224544 3221223688 134616156 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 125006 104513 603 41 0 124965 0
vsize: 500024
[startup+1140.2 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 744
Raw data (stat): 687 (minisat+) R 686 23176 23175 0 -1 0 127338 0 0 0 113653 374 0 0 25 0 1 0 547774218 512155648 104543 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 125038 104543 603 41 0 124997 0
vsize: 500152
[startup+1150.2 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 744
Raw data (stat): 687 (minisat+) R 686 23176 23175 0 -1 0 127355 0 0 0 114653 374 0 0 25 0 1 0 547774218 512155648 104560 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 125038 104560 603 41 0 124997 0
vsize: 500152
[startup+1160.2 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 744
Raw data (stat): 687 (minisat+) R 686 23176 23175 0 -1 0 127380 0 0 0 115653 375 0 0 25 0 1 0 547774218 512290816 104585 4294967295 134512640 134672761 3221224544 3221223744 134610661 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 125071 104585 603 41 0 125030 0
vsize: 500284
[startup+1170.2 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 744
Raw data (stat): 687 (minisat+) R 686 23176 23175 0 -1 0 127427 0 0 0 116653 375 0 0 25 0 1 0 547774218 512421888 104632 4294967295 134512640 134672761 3221224544 3221223744 134610707 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 125103 104632 603 41 0 125062 0
vsize: 500412
[startup+1180.2 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 744
Raw data (stat): 687 (minisat+) R 686 23176 23175 0 -1 0 127444 0 0 0 117653 375 0 0 25 0 1 0 547774218 512557056 104649 4294967295 134512640 134672761 3221224544 3221223728 134615652 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 125136 104649 603 41 0 125095 0
vsize: 500544
[startup+1190.2 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 744
Raw data (stat): 687 (minisat+) R 686 23176 23175 0 -1 0 127463 0 0 0 118653 375 0 0 25 0 1 0 547774218 512557056 104668 4294967295 134512640 134672761 3221224544 3221223728 134615594 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 125136 104668 603 41 0 125095 0
vsize: 500544
[startup+1200.2 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 744
Raw data (stat): 687 (minisat+) R 686 23176 23175 0 -1 0 127496 0 0 0 119653 375 0 0 25 0 1 0 547774218 512692224 104701 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 125169 104701 603 41 0 125128 0
vsize: 500676
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.43 s]
Raw data (loadavg): 0.99 0.97 0.91 1/54 744
Raw data (stat): 687 (minisat+) Z 686 23176 23175 0 -1 12 127496 0 0 0 119653 398 0 0 25 0 1 0 547774218 0 0 4294967295 0 0 0 0 0 0 16384 5 16386 3222412051 0 0 17 1 0 0
Raw data (statm): 0 0 0 0 0 0 0
vsize: 0
Maximum CPU time exceeded: sending SIGTERM and SIGKILL

Child status: 0
Real time (s): 1200.43
CPU time (s): 1200.53
CPU user time (s): 1196.54
CPU system time (s): 3.98639
CPU usage (%): 100.008
Max. virtual memory (Kb): 500676
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####