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 20036

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

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

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        498936 kB
Buffers:         33828 kB
Cached:         479472 kB
SwapCached:        440 kB
Active:         119796 kB
Inactive:       395604 kB
HighTotal:      131008 kB
HighFree:          252 kB
LowTotal:       903652 kB
LowFree:        498684 kB
SwapTotal:     2097136 kB
SwapFree:      2095984 kB
Dirty:              40 kB
Writeback:           0 kB
Mapped:           5360 kB
Slab:            14612 kB
Committed_AS:    63484 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-21 20:21:03 (client local time) WITH STATUS 0 IN 1200.47 SECONDS
stats: 15696 7 1200.47 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 ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 | 2504820  7932281 |  834940       0        0     nan |  0.000 % |
c |       102 | 2504767  7932164 |  918434      99      704     7.1 |  4.886 % |
c |       252 | 2504737  7932098 | 1010277     242     1490     6.2 |  4.887 % |
c |       477 | 2504712  7932044 | 1111305     465     2836     6.1 |  4.888 % |
c |       814 | 2504671  7931953 | 1222435     796     4345     5.5 |  4.891 % |
c |      1320 | 2504580  7931751 | 1344679    1288     6653     5.2 |  4.895 % |
c |      2079 | 2504503  7931580 | 1479147    2038    10966     5.4 |  4.899 % |
c |      3218 | 2504358  7931260 | 1627061    3156    16884     5.3 |  4.907 % |
c |      4926 | 2504168  7930838 | 1789768    4843    27387     5.7 |  4.916 % |
c |      7488 | 2504042  7930553 | 1968744    7392    41940     5.7 |  4.921 % |
c |     11332 | 2503583  7929529 | 2165619   11184    64647     5.8 |  4.943 % |
c |     17099 | 2502938  7928095 | 2382181   16863   105135     6.2 |  4.975 % |
c |     25748 | 2502084  7926196 | 2620399   25399   160718     6.3 |  5.016 % |
c |     38722 | 2501119  7924053 | 2882439   38239   250247     6.5 |  5.064 % |
c |     58183 | 2500375  7922394 | 3170683   57593   485948     8.4 |  5.100 % |
c |     87375 | 2498716  7918688 | 3487751   86549   695809     8.0 |  5.178 % |
c |    131164 | 2497411  7915773 | 3836526  130126  1709323    13.1 |  5.241 % |
#### 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): 1.01 1.02 0.93 2/54 15253
Raw data (stat): 15253 (runsolver) R 15252 29151 29150 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 489571985 1052672 99 4294967295 134512640 135381576 3221224512 3221219756 135158418 0 2147483391 7 90112 0 0 0 17 0 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0013 s]
Raw data (loadavg): 1.00 1.02 0.93 2/54 15253
Raw data (stat): 15253 (minisat+) R 15252 29151 29150 0 -1 0 6784 0 0 0 977 21 0 0 25 0 1 0 489571985 30478336 6501 4294967295 134512640 134672761 3221224624 3221224016 134580814 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7441 6501 603 41 0 7400 0
vsize: 29764
[startup+20.0019 s]
Raw data (loadavg): 1.00 1.02 0.93 2/54 15253
Raw data (stat): 15253 (minisat+) R 15252 29151 29150 0 -1 0 7015 0 0 0 1977 22 0 0 25 0 1 0 489571985 30474240 6518 4294967295 134512640 134672761 3221224624 3221222956 134516692 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7440 6518 603 41 0 7399 0
vsize: 29760
[startup+30.002 s]
Raw data (loadavg): 1.00 1.02 0.93 2/54 15255
Raw data (stat): 15253 (minisat+) R 15252 29151 29150 0 -1 0 12550 0 0 0 2965 33 0 0 25 0 1 0 489571985 48824320 10899 4294967295 134512640 134672761 3221224624 3221222544 134522898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11920 10899 603 41 0 11879 0
vsize: 47680
[startup+40.0029 s]
Raw data (loadavg): 1.00 1.02 0.93 2/54 15255
Raw data (stat): 15253 (minisat+) R 15252 29151 29150 0 -1 0 41086 0 0 0 3901 96 0 0 25 0 1 0 489571985 179892224 39435 4294967295 134512640 134672761 3221224624 3221220368 134531888 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 43919 39435 603 41 0 43878 0
vsize: 175676
[startup+50.0035 s]
Raw data (loadavg): 1.00 1.02 0.93 2/54 15255
Raw data (stat): 15253 (minisat+) R 15252 29151 29150 0 -1 0 53865 0 0 0 4869 129 0 0 25 0 1 0 489571985 262840320 52214 4294967295 134512640 134672761 3221224624 3221223796 134556643 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 64170 52214 603 41 0 64129 0
vsize: 256680
[startup+60.0042 s]
Raw data (loadavg): 1.00 1.01 0.93 2/54 15255
Raw data (stat): 15253 (minisat+) R 15252 29151 29150 0 -1 0 53994 0 0 0 5868 130 0 0 25 0 1 0 489571985 263380992 52343 4294967295 134512640 134672761 3221224624 3221223796 134556602 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 64302 52343 603 41 0 64261 0
vsize: 257208
[startup+70.0051 s]
Raw data (loadavg): 1.00 1.01 0.93 2/54 15255
Raw data (stat): 15253 (minisat+) R 15252 29151 29150 0 -1 0 54161 0 0 0 6868 130 0 0 25 0 1 0 489571985 264069120 52510 4294967295 134512640 134672761 3221224624 3221223796 134556602 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 64470 52510 603 41 0 64429 0
vsize: 257880
[startup+80.0059 s]
Raw data (loadavg): 1.00 1.01 0.93 2/54 15255
Raw data (stat): 15253 (minisat+) R 15252 29151 29150 0 -1 0 54209 0 0 0 7868 131 0 0 25 0 1 0 489571985 264204288 52558 4294967295 134512640 134672761 3221224624 3221223796 134556643 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 64503 52558 603 41 0 64462 0
vsize: 258012
[startup+90.0067 s]
Raw data (loadavg): 1.00 1.01 0.93 2/54 15255
Raw data (stat): 15253 (minisat+) R 15252 29151 29150 0 -1 0 54531 0 0 0 8866 132 0 0 25 0 1 0 489571985 265420800 52880 4294967295 134512640 134672761 3221224624 3221223796 134556667 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 64800 52880 603 41 0 64759 0
vsize: 259200
[startup+100.007 s]
Raw data (loadavg): 1.00 1.01 0.93 2/54 15255
Raw data (stat): 15253 (minisat+) R 15252 29151 29150 0 -1 0 54762 0 0 0 9865 133 0 0 25 0 1 0 489571985 266231808 53111 4294967295 134512640 134672761 3221224624 3221223796 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 64998 53111 603 41 0 64957 0
vsize: 259992
[startup+110.007 s]
Raw data (loadavg): 1.00 1.01 0.93 2/54 15255
Raw data (stat): 15253 (minisat+) R 15252 29151 29150 0 -1 0 54798 0 0 0 10865 133 0 0 25 0 1 0 489571985 266502144 53147 4294967295 134512640 134672761 3221224624 3221223792 134560917 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 65064 53147 603 41 0 65023 0
vsize: 260256
[startup+120.008 s]
Raw data (loadavg): 1.00 1.01 0.93 2/54 15255
Raw data (stat): 15253 (minisat+) R 15252 29151 29150 0 -1 0 54846 0 0 0 11865 134 0 0 25 0 1 0 489571985 266637312 53195 4294967295 134512640 134672761 3221224624 3221223824 134557911 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 65097 53195 603 41 0 65056 0
vsize: 260388
[startup+130.008 s]
Raw data (loadavg): 1.00 1.01 0.93 2/54 15255
Raw data (stat): 15253 (minisat+) R 15252 29151 29150 0 -1 0 54875 0 0 0 12865 134 0 0 25 0 1 0 489571985 266772480 53224 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 65130 53224 603 41 0 65089 0
vsize: 260520
[startup+140.009 s]
Raw data (loadavg): 1.00 1.01 0.93 2/54 15255
Raw data (stat): 15253 (minisat+) R 15252 29151 29150 0 -1 0 54912 0 0 0 13864 134 0 0 25 0 1 0 489571985 266907648 53261 4294967295 134512640 134672761 3221224624 3221223820 134556584 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 65163 53261 603 41 0 65122 0
vsize: 260652
[startup+150.01 s]
Raw data (loadavg): 1.00 1.01 0.93 2/54 15255
Raw data (stat): 15253 (minisat+) R 15252 29151 29150 0 -1 0 54943 0 0 0 14864 134 0 0 25 0 1 0 489571985 267042816 53292 4294967295 134512640 134672761 3221224624 3221223792 134560874 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 65196 53292 603 41 0 65155 0
vsize: 260784
[startup+160.01 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 15255
Raw data (stat): 15253 (minisat+) R 15252 29151 29150 0 -1 0 54993 0 0 0 15864 135 0 0 25 0 1 0 489571985 267177984 53342 4294967295 134512640 134672761 3221224624 3221223796 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 65229 53342 603 41 0 65188 0
vsize: 260916
[startup+170.011 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 15255
Raw data (stat): 15253 (minisat+) R 15252 29151 29150 0 -1 0 55003 0 0 0 16864 135 0 0 25 0 1 0 489571985 267313152 53352 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 65262 53352 603 41 0 65221 0
vsize: 261048
[startup+180.011 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 15255
Raw data (stat): 15253 (minisat+) R 15252 29151 29150 0 -1 0 55033 0 0 0 17864 135 0 0 25 0 1 0 489571985 267497472 53382 4294967295 134512640 134672761 3221224624 3221223748 134566024 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 65307 53382 603 41 0 65266 0
vsize: 261228
[startup+190.012 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 15255
Raw data (stat): 15253 (minisat+) R 15252 29151 29150 0 -1 0 55047 0 0 0 18864 135 0 0 25 0 1 0 489571985 267497472 53396 4294967295 134512640 134672761 3221224624 3221223760 134560588 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 65307 53396 603 41 0 65266 0
vsize: 261228
[startup+200.012 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 15255
Raw data (stat): 15253 (minisat+) R 15252 29151 29150 0 -1 0 55080 0 0 0 19864 136 0 0 25 0 1 0 489571985 267632640 53429 4294967295 134512640 134672761 3221224624 3221223748 134566077 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 65340 53429 603 41 0 65299 0
vsize: 261360
[startup+210.013 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 15255
Raw data (stat): 15253 (minisat+) R 15252 29151 29150 0 -1 0 55098 0 0 0 20863 137 0 0 25 0 1 0 489571985 267632640 53447 4294967295 134512640 134672761 3221224624 3221223760 134560625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 65340 53447 603 41 0 65299 0
vsize: 261360
[startup+220.013 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 15255
Raw data (stat): 15253 (minisat+) R 15252 29151 29150 0 -1 0 55113 0 0 0 21863 137 0 0 25 0 1 0 489571985 267763712 53462 4294967295 134512640 134672761 3221224624 3221223796 134556632 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 65372 53462 603 41 0 65331 0
vsize: 261488
[startup+230.013 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 15255
Raw data (stat): 15253 (minisat+) R 15252 29151 29150 0 -1 0 55127 0 0 0 22863 137 0 0 25 0 1 0 489571985 267763712 53476 4294967295 134512640 134672761 3221224624 3221223796 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 65372 53476 603 41 0 65331 0
vsize: 261488
[startup+240.014 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 15255
Raw data (stat): 15253 (minisat+) R 15252 29151 29150 0 -1 0 55145 0 0 0 23863 138 0 0 25 0 1 0 489571985 267894784 53494 4294967295 134512640 134672761 3221224624 3221223748 134566071 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 65404 53494 603 41 0 65363 0
vsize: 261616
[startup+250.014 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 15255
Raw data (stat): 15253 (minisat+) R 15252 29151 29150 0 -1 0 55178 0 0 0 24862 138 0 0 25 0 1 0 489571985 268029952 53527 4294967295 134512640 134672761 3221224624 3221223824 134557895 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 65437 53527 603 41 0 65396 0
vsize: 261748
[startup+260.015 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 15255
Raw data (stat): 15253 (minisat+) R 15252 29151 29150 0 -1 0 55201 0 0 0 25862 139 0 0 25 0 1 0 489571985 268029952 53550 4294967295 134512640 134672761 3221224624 3221223840 134561987 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 65437 53550 603 41 0 65396 0
vsize: 261748
[startup+270.016 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 15255
Raw data (stat): 15253 (minisat+) R 15252 29151 29150 0 -1 0 55230 0 0 0 26862 139 0 0 25 0 1 0 489571985 268165120 53579 4294967295 134512640 134672761 3221224624 3221223792 134564722 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 65470 53579 603 41 0 65429 0
vsize: 261880
[startup+280.016 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 15255
Raw data (stat): 15253 (minisat+) R 15252 29151 29150 0 -1 0 55261 0 0 0 27861 140 0 0 25 0 1 0 489571985 268300288 53610 4294967295 134512640 134672761 3221224624 3221223796 134556649 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 65503 53610 603 41 0 65462 0
vsize: 262012
[startup+290.017 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 15255
Raw data (stat): 15253 (minisat+) R 15252 29151 29150 0 -1 0 55284 0 0 0 28861 140 0 0 25 0 1 0 489571985 268435456 53633 4294967295 134512640 134672761 3221224624 3221223760 134565116 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 65536 53633 603 41 0 65495 0
vsize: 262144
[startup+300.017 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 15257
Raw data (stat): 15253 (minisat+) R 15252 29151 29150 0 -1 0 55316 0 0 0 29860 141 0 0 25 0 1 0 489571985 268570624 53665 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 65569 53665 603 41 0 65528 0
vsize: 262276
[startup+310.018 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 15257
Raw data (stat): 15253 (minisat+) R 15252 29151 29150 0 -1 0 55369 0 0 0 30860 141 0 0 25 0 1 0 489571985 268832768 53718 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 65633 53718 603 41 0 65592 0
vsize: 262532
[startup+320.019 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 15257
Raw data (stat): 15253 (minisat+) R 15252 29151 29150 0 -1 0 55369 0 0 0 31860 142 0 0 25 0 1 0 489571985 268832768 53718 4294967295 134512640 134672761 3221224624 3221223828 134561964 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 65633 53718 603 41 0 65592 0
vsize: 262532
[startup+330.019 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 15257
Raw data (stat): 15253 (minisat+) R 15252 29151 29150 0 -1 0 55371 0 0 0 32860 142 0 0 25 0 1 0 489571985 268832768 53720 4294967295 134512640 134672761 3221224624 3221223796 134556685 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 65633 53720 603 41 0 65592 0
vsize: 262532
[startup+340.02 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 15257
Raw data (stat): 15253 (minisat+) R 15252 29151 29150 0 -1 0 55400 0 0 0 33860 142 0 0 25 0 1 0 489571985 268967936 53749 4294967295 134512640 134672761 3221224624 3221223824 134557911 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 65666 53749 603 41 0 65625 0
vsize: 262664
[startup+350.02 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 15257
Raw data (stat): 15253 (minisat+) R 15252 29151 29150 0 -1 0 55419 0 0 0 34860 143 0 0 25 0 1 0 489571985 269103104 53768 4294967295 134512640 134672761 3221224624 3221223792 134560876 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 65699 53768 603 41 0 65658 0
vsize: 262796
[startup+360.022 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 15257
Raw data (stat): 15253 (minisat+) R 15252 29151 29150 0 -1 0 55447 0 0 0 35859 143 0 0 25 0 1 0 489571985 269103104 53796 4294967295 134512640 134672761 3221224624 3221223796 134556682 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 65699 53796 603 41 0 65658 0
vsize: 262796
[startup+370.023 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 15257
Raw data (stat): 15253 (minisat+) R 15252 29151 29150 0 -1 0 55460 0 0 0 36859 143 0 0 25 0 1 0 489571985 269234176 53809 4294967295 134512640 134672761 3221224624 3221223796 134556660 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 65731 53809 603 41 0 65690 0
vsize: 262924
[startup+380.023 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 15257
Raw data (stat): 15253 (minisat+) R 15252 29151 29150 0 -1 0 55480 0 0 0 37859 143 0 0 25 0 1 0 489571985 269234176 53829 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 65731 53829 603 41 0 65690 0
vsize: 262924
[startup+390.023 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 15257
Raw data (stat): 15253 (minisat+) R 15252 29151 29150 0 -1 0 55505 0 0 0 38859 144 0 0 25 0 1 0 489571985 269369344 53854 4294967295 134512640 134672761 3221224624 3221223760 134560677 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 65764 53854 603 41 0 65723 0
vsize: 263056
[startup+400.024 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 15257
Raw data (stat): 15253 (minisat+) R 15252 29151 29150 0 -1 0 55525 0 0 0 39860 144 0 0 25 0 1 0 489571985 269504512 53874 4294967295 134512640 134672761 3221224624 3221223796 134556682 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 65797 53874 603 41 0 65756 0
vsize: 263188
[startup+410.025 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 15257
Raw data (stat): 15253 (minisat+) R 15252 29151 29150 0 -1 0 55615 0 0 0 40860 144 0 0 25 0 1 0 489571985 269774848 53964 4294967295 134512640 134672761 3221224624 3221223748 134566034 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 65863 53964 603 41 0 65822 0
vsize: 263452
[startup+420.026 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 15257
Raw data (stat): 15253 (minisat+) R 15252 29151 29150 0 -1 0 55639 0 0 0 41860 144 0 0 25 0 1 0 489571985 269910016 53988 4294967295 134512640 134672761 3221224624 3221223824 134561972 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 65896 53988 603 41 0 65855 0
vsize: 263584
[startup+430.026 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 15257
Raw data (stat): 15253 (minisat+) R 15252 29151 29150 0 -1 0 55672 0 0 0 42860 144 0 0 25 0 1 0 489571985 270045184 54021 4294967295 134512640 134672761 3221224624 3221223748 134566142 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 65929 54021 603 41 0 65888 0
vsize: 263716
[startup+440.027 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 15257
Raw data (stat): 15253 (minisat+) R 15252 29151 29150 0 -1 0 55705 0 0 0 43860 144 0 0 25 0 1 0 489571985 270180352 54054 4294967295 134512640 134672761 3221224624 3221223748 134566071 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 65962 54054 603 41 0 65921 0
vsize: 263848
[startup+450.027 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 15257
Raw data (stat): 15253 (minisat+) R 15252 29151 29150 0 -1 0 55732 0 0 0 44860 144 0 0 25 0 1 0 489571985 270315520 54081 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 65995 54081 603 41 0 65954 0
vsize: 263980
[startup+460.028 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 15257
Raw data (stat): 15253 (minisat+) R 15252 29151 29150 0 -1 0 55750 0 0 0 45860 145 0 0 25 0 1 0 489571985 270315520 54099 4294967295 134512640 134672761 3221224624 3221223796 134556651 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 65995 54099 603 41 0 65954 0
vsize: 263980
[startup+470.029 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 15257
Raw data (stat): 15253 (minisat+) R 15252 29151 29150 0 -1 0 55773 0 0 0 46860 145 0 0 25 0 1 0 489571985 270450688 54122 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 66028 54122 603 41 0 65987 0
vsize: 264112
[startup+480.029 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 15257
Raw data (stat): 15253 (minisat+) R 15252 29151 29150 0 -1 0 55875 0 0 0 47860 145 0 0 25 0 1 0 489571985 270852096 54224 4294967295 134512640 134672761 3221224624 3221223760 134560588 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 66126 54224 603 41 0 66085 0
vsize: 264504
[startup+490.03 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 15257
Raw data (stat): 15253 (minisat+) R 15252 29151 29150 0 -1 0 55903 0 0 0 48860 145 0 0 25 0 1 0 489571985 270852096 54252 4294967295 134512640 134672761 3221224624 3221223792 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 66126 54252 603 41 0 66085 0
vsize: 264504
[startup+500.031 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 15257
Raw data (stat): 15253 (minisat+) R 15252 29151 29150 0 -1 0 55940 0 0 0 49860 145 0 0 25 0 1 0 489571985 270987264 54289 4294967295 134512640 134672761 3221224624 3221223796 134556682 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 66159 54289 603 41 0 66118 0
vsize: 264636
[startup+510.031 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 15257
Raw data (stat): 15253 (minisat+) R 15252 29151 29150 0 -1 0 55963 0 0 0 50860 146 0 0 25 0 1 0 489571985 271118336 54312 4294967295 134512640 134672761 3221224624 3221223840 134561948 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 66191 54312 603 41 0 66150 0
vsize: 264764
[startup+520.031 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 15257
Raw data (stat): 15253 (minisat+) R 15252 29151 29150 0 -1 0 55988 0 0 0 51860 146 0 0 25 0 1 0 489571985 271253504 54337 4294967295 134512640 134672761 3221224624 3221223796 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 66224 54337 603 41 0 66183 0
vsize: 264896
[startup+530.032 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 15257
Raw data (stat): 15253 (minisat+) R 15252 29151 29150 0 -1 0 56022 0 0 0 52860 146 0 0 25 0 1 0 489571985 271384576 54371 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 66256 54371 603 41 0 66215 0
vsize: 265024
[startup+540.034 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 15257
Raw data (stat): 15253 (minisat+) R 15252 29151 29150 0 -1 0 56042 0 0 0 53860 146 0 0 25 0 1 0 489571985 271384576 54391 4294967295 134512640 134672761 3221224624 3221223764 134560556 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 66256 54391 603 41 0 66215 0
vsize: 265024
[startup+550.034 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 15257
Raw data (stat): 15253 (minisat+) R 15252 29151 29150 0 -1 0 56057 0 0 0 54860 146 0 0 25 0 1 0 489571985 271781888 54406 4294967295 134512640 134672761 3221224624 3221223796 134556688 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 66353 54406 603 41 0 66312 0
vsize: 265412
[startup+560.035 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 15257
Raw data (stat): 15253 (minisat+) R 15252 29151 29150 0 -1 0 56080 0 0 0 55860 146 0 0 25 0 1 0 489571985 271781888 54429 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 66353 54429 603 41 0 66312 0
vsize: 265412
[startup+570.035 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 15257
Raw data (stat): 15253 (minisat+) R 15252 29151 29150 0 -1 0 56101 0 0 0 56860 146 0 0 25 0 1 0 489571985 271917056 54450 4294967295 134512640 134672761 3221224624 3221223760 134560588 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 66386 54450 603 41 0 66345 0
vsize: 265544
[startup+580.038 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 15257
Raw data (stat): 15253 (minisat+) R 15252 29151 29150 0 -1 0 56128 0 0 0 57861 146 0 0 25 0 1 0 489571985 272048128 54477 4294967295 134512640 134672761 3221224624 3221223796 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 66418 54477 603 41 0 66377 0
vsize: 265672
[startup+590.042 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 15257
Raw data (stat): 15253 (minisat+) R 15252 29151 29150 0 -1 0 56145 0 0 0 58861 147 0 0 25 0 1 0 489571985 272048128 54494 4294967295 134512640 134672761 3221224624 3221223792 134560849 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 66418 54494 603 41 0 66377 0
vsize: 265672
[startup+600.046 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 15257
Raw data (stat): 15253 (minisat+) R 15252 29151 29150 0 -1 0 56163 0 0 0 59862 147 0 0 25 0 1 0 489571985 272183296 54512 4294967295 134512640 134672761 3221224624 3221223796 134556667 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 66451 54512 603 41 0 66410 0
vsize: 265804
[startup+610.047 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 15257
Raw data (stat): 15253 (minisat+) R 15252 29151 29150 0 -1 0 56189 0 0 0 60862 147 0 0 25 0 1 0 489571985 272318464 54538 4294967295 134512640 134672761 3221224624 3221223748 134566118 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 66484 54538 603 41 0 66443 0
vsize: 265936
[startup+620.048 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 15257
Raw data (stat): 15253 (minisat+) R 15252 29151 29150 0 -1 0 56210 0 0 0 61862 147 0 0 25 0 1 0 489571985 272318464 54559 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 66484 54559 603 41 0 66443 0
vsize: 265936
[startup+630.048 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 15257
Raw data (stat): 15253 (minisat+) R 15252 29151 29150 0 -1 0 56235 0 0 0 62862 147 0 0 25 0 1 0 489571985 272449536 54584 4294967295 134512640 134672761 3221224624 3221223820 134556678 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 66516 54584 603 41 0 66475 0
vsize: 266064
[startup+640.049 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 15257
Raw data (stat): 15253 (minisat+) R 15252 29151 29150 0 -1 0 56258 0 0 0 63862 147 0 0 25 0 1 0 489571985 272584704 54607 4294967295 134512640 134672761 3221224624 3221223796 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 66549 54607 603 41 0 66508 0
vsize: 266196
[startup+650.049 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 15257
Raw data (stat): 15253 (minisat+) R 15252 29151 29150 0 -1 0 56275 0 0 0 64862 147 0 0 25 0 1 0 489571985 272584704 54624 4294967295 134512640 134672761 3221224624 3221223760 134560703 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 66549 54624 603 41 0 66508 0
vsize: 266196
[startup+660.05 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 15257
Raw data (stat): 15253 (minisat+) R 15252 29151 29150 0 -1 0 56317 0 0 0 65862 147 0 0 25 0 1 0 489571985 272719872 54666 4294967295 134512640 134672761 3221224624 3221223804 134556674 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 66582 54666 603 41 0 66541 0
vsize: 266328
[startup+670.05 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 15257
Raw data (stat): 15253 (minisat+) R 15252 29151 29150 0 -1 0 56345 0 0 0 66863 147 0 0 25 0 1 0 489571985 272855040 54694 4294967295 134512640 134672761 3221224624 3221223796 134556660 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 66615 54694 603 41 0 66574 0
vsize: 266460
[startup+680.051 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 15257
Raw data (stat): 15253 (minisat+) R 15252 29151 29150 0 -1 0 56376 0 0 0 67863 147 0 0 25 0 1 0 489571985 272990208 54725 4294967295 134512640 134672761 3221224624 3221223748 134566057 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 66648 54725 603 41 0 66607 0
vsize: 266592
[startup+690.051 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 15257
Raw data (stat): 15253 (minisat+) R 15252 29151 29150 0 -1 0 56395 0 0 0 68863 147 0 0 25 0 1 0 489571985 272990208 54744 4294967295 134512640 134672761 3221224624 3221223824 134557895 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 66648 54744 603 41 0 66607 0
vsize: 266592
[startup+700.052 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 15257
Raw data (stat): 15253 (minisat+) R 15252 29151 29150 0 -1 0 56412 0 0 0 69863 147 0 0 25 0 1 0 489571985 273125376 54761 4294967295 134512640 134672761 3221224624 3221223748 134566034 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 66681 54761 603 41 0 66640 0
vsize: 266724
[startup+710.052 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 15257
Raw data (stat): 15253 (minisat+) R 15252 29151 29150 0 -1 0 56425 0 0 0 70863 147 0 0 25 0 1 0 489571985 273125376 54774 4294967295 134512640 134672761 3221224624 3221223796 134556671 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 66681 54774 603 41 0 66640 0
vsize: 266724
[startup+720.052 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 15257
Raw data (stat): 15253 (minisat+) R 15252 29151 29150 0 -1 0 56444 0 0 0 71863 148 0 0 25 0 1 0 489571985 273125376 54793 4294967295 134512640 134672761 3221224624 3221223760 134560598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 66681 54793 603 41 0 66640 0
vsize: 266724
[startup+730.052 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 15257
Raw data (stat): 15253 (minisat+) R 15252 29151 29150 0 -1 0 56467 0 0 0 72863 148 0 0 25 0 1 0 489571985 273260544 54816 4294967295 134512640 134672761 3221224624 3221223796 134556651 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 66714 54816 603 41 0 66673 0
vsize: 266856
[startup+740.055 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 15257
Raw data (stat): 15253 (minisat+) R 15252 29151 29150 0 -1 0 56489 0 0 0 73863 148 0 0 25 0 1 0 489571985 273260544 54838 4294967295 134512640 134672761 3221224624 3221223728 134559908 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 66714 54838 603 41 0 66673 0
vsize: 266856
[startup+750.055 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 15257
Raw data (stat): 15253 (minisat+) R 15252 29151 29150 0 -1 0 56505 0 0 0 74863 148 0 0 25 0 1 0 489571985 273395712 54854 4294967295 134512640 134672761 3221224624 3221223796 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 66747 54854 603 41 0 66706 0
vsize: 266988
[startup+760.063 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 15257
Raw data (stat): 15253 (minisat+) R 15252 29151 29150 0 -1 0 56525 0 0 0 75864 148 0 0 25 0 1 0 489571985 273395712 54874 4294967295 134512640 134672761 3221224624 3221223748 134566037 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 66747 54874 603 41 0 66706 0
vsize: 266988
[startup+770.072 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 15257
Raw data (stat): 15253 (minisat+) R 15252 29151 29150 0 -1 0 56573 0 0 0 76865 148 0 0 25 0 1 0 489571985 273530880 54922 4294967295 134512640 134672761 3221224624 3221223796 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 66780 54922 603 41 0 66739 0
vsize: 267120
[startup+780.072 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 15257
Raw data (stat): 15253 (minisat+) R 15252 29151 29150 0 -1 0 56737 0 0 0 77864 149 0 0 25 0 1 0 489571985 274186240 55086 4294967295 134512640 134672761 3221224624 3221223796 134556667 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 66940 55086 603 41 0 66899 0
vsize: 267760
[startup+790.072 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 15257
Raw data (stat): 15253 (minisat+) R 15252 29151 29150 0 -1 0 56758 0 0 0 78865 149 0 0 25 0 1 0 489571985 274321408 55107 4294967295 134512640 134672761 3221224624 3221223792 134560839 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 66973 55107 603 41 0 66932 0
vsize: 267892
[startup+800.072 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 15257
Raw data (stat): 15253 (minisat+) R 15252 29151 29150 0 -1 0 56774 0 0 0 79865 149 0 0 25 0 1 0 489571985 274321408 55123 4294967295 134512640 134672761 3221224624 3221223796 134556660 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 66973 55123 603 41 0 66932 0
vsize: 267892
[startup+810.073 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 15257
Raw data (stat): 15253 (minisat+) R 15252 29151 29150 0 -1 0 56789 0 0 0 80865 149 0 0 25 0 1 0 489571985 274456576 55138 4294967295 134512640 134672761 3221224624 3221223796 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 67006 55138 603 41 0 66965 0
vsize: 268024
[startup+820.074 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 15257
Raw data (stat): 15253 (minisat+) R 15252 29151 29150 0 -1 0 56804 0 0 0 81865 149 0 0 25 0 1 0 489571985 274456576 55153 4294967295 134512640 134672761 3221224624 3221223748 134566034 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 67006 55153 603 41 0 66965 0
vsize: 268024
[startup+830.081 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 15257
Raw data (stat): 15253 (minisat+) R 15252 29151 29150 0 -1 0 56826 0 0 0 82866 149 0 0 25 0 1 0 489571985 274591744 55175 4294967295 134512640 134672761 3221224624 3221223748 134566037 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 67039 55175 603 41 0 66998 0
vsize: 268156
[startup+840.184 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 15257
Raw data (stat): 15253 (minisat+) R 15252 29151 29150 0 -1 0 56849 0 0 0 83876 149 0 0 25 0 1 0 489571985 274726912 55198 4294967295 134512640 134672761 3221224624 3221223796 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 67072 55198 603 41 0 67031 0
vsize: 268288
[startup+850.184 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 15257
Raw data (stat): 15253 (minisat+) R 15252 29151 29150 0 -1 0 56873 0 0 0 84876 149 0 0 25 0 1 0 489571985 274726912 55222 4294967295 134512640 134672761 3221224624 3221223792 134561011 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 67072 55222 603 41 0 67031 0
vsize: 268288
[startup+860.184 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 15257
Raw data (stat): 15253 (minisat+) R 15252 29151 29150 0 -1 0 56889 0 0 0 85876 149 0 0 25 0 1 0 489571985 274862080 55238 4294967295 134512640 134672761 3221224624 3221223760 134560688 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 67105 55238 603 41 0 67064 0
vsize: 268420
[startup+870.185 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 15257
Raw data (stat): 15253 (minisat+) R 15252 29151 29150 0 -1 0 56913 0 0 0 86877 150 0 0 25 0 1 0 489571985 274862080 55262 4294967295 134512640 134672761 3221224624 3221223824 134557836 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 67105 55262 603 41 0 67064 0
vsize: 268420
[startup+880.186 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 15257
Raw data (stat): 15253 (minisat+) R 15252 29151 29150 0 -1 0 56957 0 0 0 87877 150 0 0 25 0 1 0 489571985 275132416 55306 4294967295 134512640 134672761 3221224624 3221223824 134557887 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 67171 55306 603 41 0 67130 0
vsize: 268684
[startup+890.194 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 15257
Raw data (stat): 15253 (minisat+) R 15252 29151 29150 0 -1 0 56981 0 0 0 88878 150 0 0 25 0 1 0 489571985 275132416 55330 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 67171 55330 603 41 0 67130 0
vsize: 268684
[startup+900.193 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 15257
Raw data (stat): 15253 (minisat+) R 15252 29151 29150 0 -1 0 57347 0 0 0 89877 151 0 0 25 0 1 0 489571985 276602880 55696 4294967295 134512640 134672761 3221224624 3221223760 134560588 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 67530 55696 603 41 0 67489 0
vsize: 270120
[startup+910.193 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 15257
Raw data (stat): 15253 (minisat+) R 15252 29151 29150 0 -1 0 57497 0 0 0 90876 151 0 0 25 0 1 0 489571985 277274624 55846 4294967295 134512640 134672761 3221224624 3221223760 134560642 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 67694 55846 603 41 0 67653 0
vsize: 270776
[startup+920.212 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 15257
Raw data (stat): 15253 (minisat+) R 15252 29151 29150 0 -1 0 57512 0 0 0 91878 151 0 0 25 0 1 0 489571985 277274624 55861 4294967295 134512640 134672761 3221224624 3221223796 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 67694 55861 603 41 0 67653 0
vsize: 270776
[startup+930.212 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 15257
Raw data (stat): 15253 (minisat+) R 15252 29151 29150 0 -1 0 57532 0 0 0 92878 152 0 0 25 0 1 0 489571985 277409792 55881 4294967295 134512640 134672761 3221224624 3221223796 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 67727 55881 603 41 0 67686 0
vsize: 270908
[startup+940.213 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 15257
Raw data (stat): 15253 (minisat+) R 15252 29151 29150 0 -1 0 57543 0 0 0 93878 152 0 0 25 0 1 0 489571985 277409792 55892 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 67727 55892 603 41 0 67686 0
vsize: 270908
[startup+950.213 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 15257
Raw data (stat): 15253 (minisat+) R 15252 29151 29150 0 -1 0 57556 0 0 0 94879 152 0 0 25 0 1 0 489571985 277544960 55905 4294967295 134512640 134672761 3221224624 3221223796 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 67760 55905 603 41 0 67719 0
vsize: 271040
[startup+960.213 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 15257
Raw data (stat): 15253 (minisat+) R 15252 29151 29150 0 -1 0 57575 0 0 0 95879 152 0 0 25 0 1 0 489571985 277544960 55924 4294967295 134512640 134672761 3221224624 3221223792 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 67760 55924 603 41 0 67719 0
vsize: 271040
[startup+970.224 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 15257
Raw data (stat): 15253 (minisat+) R 15252 29151 29150 0 -1 0 57601 0 0 0 96880 152 0 0 25 0 1 0 489571985 277680128 55950 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 67793 55950 603 41 0 67752 0
vsize: 271172
[startup+980.234 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 15257
Raw data (stat): 15253 (minisat+) R 15252 29151 29150 0 -1 0 57635 0 0 0 97881 152 0 0 25 0 1 0 489571985 277815296 55984 4294967295 134512640 134672761 3221224624 3221223824 134557842 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 67826 55984 603 41 0 67785 0
vsize: 271304
[startup+990.235 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 15257
Raw data (stat): 15253 (minisat+) R 15252 29151 29150 0 -1 0 57651 0 0 0 98881 152 0 0 25 0 1 0 489571985 277815296 56000 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 67826 56000 603 41 0 67785 0
vsize: 271304
[startup+1000.23 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 15257
Raw data (stat): 15253 (minisat+) R 15252 29151 29150 0 -1 0 57822 0 0 0 99881 153 0 0 25 0 1 0 489571985 278614016 56171 4294967295 134512640 134672761 3221224624 3221223748 134566109 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 68021 56171 603 41 0 67980 0
vsize: 272084
[startup+1010.23 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 15257
Raw data (stat): 15253 (minisat+) R 15252 29151 29150 0 -1 0 57864 0 0 0 100880 153 0 0 25 0 1 0 489571985 278749184 56213 4294967295 134512640 134672761 3221224624 3221223780 134561032 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 68054 56213 603 41 0 68013 0
vsize: 272216
[startup+1020.24 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 15257
Raw data (stat): 15253 (minisat+) R 15252 29151 29150 0 -1 0 57942 0 0 0 101880 153 0 0 25 0 1 0 489571985 279015424 56291 4294967295 134512640 134672761 3221224624 3221223760 134560675 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 68119 56291 603 41 0 68078 0
vsize: 272476
[startup+1030.24 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 15257
Raw data (stat): 15253 (minisat+) R 15252 29151 29150 0 -1 0 57964 0 0 0 102880 153 0 0 25 0 1 0 489571985 279150592 56313 4294967295 134512640 134672761 3221224624 3221223796 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 68152 56313 603 41 0 68111 0
vsize: 272608
[startup+1040.24 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 15257
Raw data (stat): 15253 (minisat+) R 15252 29151 29150 0 -1 0 57995 0 0 0 103880 154 0 0 25 0 1 0 489571985 279810048 56344 4294967295 134512640 134672761 3221224624 3221223792 134561385 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 68313 56344 603 41 0 68272 0
vsize: 273252
[startup+1050.24 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 15257
Raw data (stat): 15253 (minisat+) R 15252 29151 29150 0 -1 0 58019 0 0 0 104879 154 0 0 25 0 1 0 489571985 279810048 56368 4294967295 134512640 134672761 3221224624 3221223780 134561241 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 68313 56368 603 41 0 68272 0
vsize: 273252
[startup+1060.24 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 15257
Raw data (stat): 15253 (minisat+) R 15252 29151 29150 0 -1 0 58039 0 0 0 105879 154 0 0 25 0 1 0 489571985 279945216 56388 4294967295 134512640 134672761 3221224624 3221223824 134557809 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 68346 56388 603 41 0 68305 0
vsize: 273384
[startup+1070.24 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 15257
Raw data (stat): 15253 (minisat+) R 15252 29151 29150 0 -1 0 58059 0 0 0 106880 154 0 0 25 0 1 0 489571985 279945216 56408 4294967295 134512640 134672761 3221224624 3221223760 134560560 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 68346 56408 603 41 0 68305 0
vsize: 273384
[startup+1080.24 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 15257
Raw data (stat): 15253 (minisat+) R 15252 29151 29150 0 -1 0 58077 0 0 0 107880 154 0 0 25 0 1 0 489571985 280080384 56426 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 68379 56426 603 41 0 68338 0
vsize: 273516
[startup+1090.24 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 15257
Raw data (stat): 15253 (minisat+) R 15252 29151 29150 0 -1 0 58096 0 0 0 108879 154 0 0 25 0 1 0 489571985 280215552 56445 4294967295 134512640 134672761 3221224624 3221223792 134561164 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 68412 56445 603 41 0 68371 0
vsize: 273648
[startup+1100.24 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 15257
Raw data (stat): 15253 (minisat+) R 15252 29151 29150 0 -1 0 58112 0 0 0 109879 154 0 0 25 0 1 0 489571985 280215552 56461 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 68412 56461 603 41 0 68371 0
vsize: 273648
[startup+1110.24 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 15257
Raw data (stat): 15253 (minisat+) R 15252 29151 29150 0 -1 0 58154 0 0 0 110878 154 0 0 25 0 1 0 489571985 280350720 56503 4294967295 134512640 134672761 3221224624 3221223792 134560885 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 68445 56503 603 41 0 68404 0
vsize: 273780
[startup+1120.24 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 15257
Raw data (stat): 15253 (minisat+) R 15252 29151 29150 0 -1 0 58175 0 0 0 111879 154 0 0 25 0 1 0 489571985 280485888 56524 4294967295 134512640 134672761 3221224624 3221223796 134556653 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 68478 56524 603 41 0 68437 0
vsize: 273912
[startup+1130.24 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 15257
Raw data (stat): 15253 (minisat+) R 15252 29151 29150 0 -1 0 58220 0 0 0 112879 154 0 0 25 0 1 0 489571985 280621056 56569 4294967295 134512640 134672761 3221224624 3221223792 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 68511 56569 603 41 0 68470 0
vsize: 274044
[startup+1140.24 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 15257
Raw data (stat): 15253 (minisat+) R 15252 29151 29150 0 -1 0 58266 0 0 0 113879 154 0 0 25 0 1 0 489571985 280756224 56615 4294967295 134512640 134672761 3221224624 3221223760 134560566 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 68544 56615 603 41 0 68503 0
vsize: 274176
[startup+1150.24 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 15257
Raw data (stat): 15253 (minisat+) R 15252 29151 29150 0 -1 0 58316 0 0 0 114879 155 0 0 25 0 1 0 489571985 280887296 56665 4294967295 134512640 134672761 3221224624 3221223776 134565127 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 68576 56665 603 41 0 68535 0
vsize: 274304
[startup+1160.24 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 15257
Raw data (stat): 15253 (minisat+) R 15252 29151 29150 0 -1 0 58335 0 0 0 115879 155 0 0 25 0 1 0 489571985 281022464 56684 4294967295 134512640 134672761 3221224624 3221223776 134565096 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 68609 56684 603 41 0 68568 0
vsize: 274436
[startup+1170.24 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 15257
Raw data (stat): 15253 (minisat+) R 15252 29151 29150 0 -1 0 58355 0 0 0 116879 155 0 0 25 0 1 0 489571985 281157632 56704 4294967295 134512640 134672761 3221224624 3221223824 134557836 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 68642 56704 603 41 0 68601 0
vsize: 274568
[startup+1180.24 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 15257
Raw data (stat): 15253 (minisat+) R 15252 29151 29150 0 -1 0 58371 0 0 0 117879 155 0 0 25 0 1 0 489571985 281157632 56720 4294967295 134512640 134672761 3221224624 3221223796 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 68642 56720 603 41 0 68601 0
vsize: 274568
[startup+1190.24 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 15257
Raw data (stat): 15253 (minisat+) R 15252 29151 29150 0 -1 0 58386 0 0 0 118879 155 0 0 25 0 1 0 489571985 281157632 56735 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 68642 56735 603 41 0 68601 0
vsize: 274568
[startup+1200.25 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 15257
Raw data (stat): 15253 (minisat+) R 15252 29151 29150 0 -1 0 58412 0 0 0 119880 155 0 0 25 0 1 0 489571985 281292800 56761 4294967295 134512640 134672761 3221224624 3221223760 134560588 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 68675 56761 603 41 0 68634 0
vsize: 274700
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.36 s]
Raw data (loadavg): 1.00 1.00 0.93 1/54 15257
Raw data (stat): 15253 (minisat+) Z 15252 29151 29150 0 -1 12 58414 0 0 0 119880 166 0 0 25 0 1 0 489571985 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.36
CPU time (s): 1200.47
CPU user time (s): 1198.8
CPU system time (s): 1.66875
CPU usage (%): 100.009
Max. virtual memory (Kb): 274700
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####