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 20011

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

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.072
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:        554664 kB
Buffers:         22432 kB
Cached:         431060 kB
SwapCached:        408 kB
Active:         118684 kB
Inactive:       337448 kB
HighTotal:      131008 kB
HighFree:          252 kB
LowTotal:       903652 kB
LowFree:        554412 kB
SwapTotal:     2097892 kB
SwapFree:      2097056 kB
Dirty:               4 kB
Writeback:           0 kB
Mapped:           5856 kB
Slab:            18248 kB
Committed_AS:    63820 kB
PageTables:        328 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-21 20:19:34 (client local time) WITH STATUS 0 IN 1200.36 SECONDS
stats: 15704 7 1200.36 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 | 2648734  8356434 |  882911       0        0     nan |  0.000 % |
c |       101 | 2648659  8356267 |  971202      97      687     7.1 |  4.886 % |
c |       251 | 2648593  8356120 | 1068322     236     1513     6.4 |  4.890 % |
c |       476 | 2648593  8356120 | 1175154     461     2571     5.6 |  4.890 % |
c |       813 | 2648505  8355924 | 1292669     790     4533     5.7 |  4.894 % |
c |      1319 | 2648412  8355713 | 1421936    1286     6713     5.2 |  4.899 % |
c |      2078 | 2648305  8355474 | 1564130    2028    10435     5.1 |  4.904 % |
c |      3217 | 2648305  8355474 | 1720543    3167    19076     6.0 |  4.904 % |
c |      4925 | 2648179  8355194 | 1892598    4860    29624     6.1 |  4.910 % |
c |      7487 | 2647740  8354216 | 2081857    7360    49233     6.7 |  4.931 % |
c |     11331 | 2647317  8353272 | 2290043   11152    74499     6.7 |  4.951 % |
c |     17097 | 2646706  8351890 | 2519048   16822   107263     6.4 |  4.980 % |
c |     25746 | 2645986  8350274 | 2770952   25384   163387     6.4 |  5.014 % |
c |     38720 | 2644911  8347878 | 3048048   38212   545239    14.3 |  5.065 % |
c |     58181 | 2643793  8345376 | 3352853   57540   755930    13.1 |  5.118 % |
c |     87374 | 2642526  8342538 | 3688138   86566  1096022    12.7 |  5.179 % |
c |    131164 | 2641458  8340133 | 4056952  130197  1802043    13.8 |  5.230 % |
#### END SOLVER DATA ####
#### BEGIN WATCHER DATA ####
Enforcing CPU limit (will send SIGTERM then SIGKILL): 1200 seconds
Enforcing CPUTime (will send SIGXCPU) limit: 1230 seconds
Enforcing VSIZE limit: 943718400 bytes
Raw data (loadavg): 0.61 0.83 0.89 2/55 4428
Raw data (stat): 4428 (runsolver) R 4427 20838 20837 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 547796183 1052672 99 4294967295 134512640 135381576 3221224448 3221219692 135158418 0 2147483391 7 90112 0 0 0 17 1 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+9.99982 s]
Raw data (loadavg): 0.67 0.83 0.89 2/55 4428
Raw data (stat): 4428 (minisat+) R 4427 20838 20837 0 -1 0 6783 0 0 0 978 20 0 0 25 0 1 0 547796183 30478336 6501 4294967295 134512640 134672761 3221224544 3221223936 134581441 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7441 6501 603 41 0 7400 0
vsize: 29764
[startup+19.9994 s]
Raw data (loadavg): 0.72 0.84 0.89 2/55 4428
Raw data (stat): 4428 (minisat+) R 4427 20838 20837 0 -1 0 6783 0 0 0 1978 20 0 0 25 0 1 0 547796183 30478336 6501 4294967295 134512640 134672761 3221224544 3221223936 134580831 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7441 6501 603 41 0 7400 0
vsize: 29764
[startup+29.9994 s]
Raw data (loadavg): 0.76 0.84 0.89 2/55 4428
Raw data (stat): 4428 (minisat+) R 4427 20838 20837 0 -1 0 12210 0 0 0 2965 34 0 0 25 0 1 0 547796183 47915008 10560 4294967295 134512640 134672761 3221224544 3221223728 134593685 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11698 10560 603 41 0 11657 0
vsize: 46792
[startup+40.007 s]
Raw data (loadavg): 0.88 0.87 0.90 2/55 4481
Raw data (stat): 4428 (minisat+) R 4427 20838 20837 0 -1 0 36636 0 0 0 3907 92 0 0 25 0 1 0 547796183 165322752 34986 4294967295 134512640 134672761 3221224544 3221219544 1075350517 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 40362 34993 603 41 0 40321 0
vsize: 161448
[startup+50.0153 s]
Raw data (loadavg): 0.89 0.87 0.90 2/55 4481
Raw data (stat): 4428 (minisat+) R 4427 20838 20837 0 -1 0 54720 0 0 0 4865 134 0 0 25 0 1 0 547796183 264159232 53070 4294967295 134512640 134672761 3221224544 3221223716 134556671 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 64492 53070 603 41 0 64451 0
vsize: 257968
[startup+60.0146 s]
Raw data (loadavg): 0.91 0.87 0.90 2/55 4481
Raw data (stat): 4428 (minisat+) R 4427 20838 20837 0 -1 0 54790 0 0 0 5865 134 0 0 25 0 1 0 547796183 264429568 53140 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 64558 53140 603 41 0 64517 0
vsize: 258232
[startup+70.0146 s]
Raw data (loadavg): 0.92 0.88 0.90 2/55 4481
Raw data (stat): 4428 (minisat+) R 4427 20838 20837 0 -1 0 54901 0 0 0 6865 135 0 0 25 0 1 0 547796183 264835072 53251 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 64657 53251 603 41 0 64616 0
vsize: 258628
[startup+80.0148 s]
Raw data (loadavg): 0.93 0.88 0.90 2/55 4481
Raw data (stat): 4428 (minisat+) R 4427 20838 20837 0 -1 0 55088 0 0 0 7864 136 0 0 25 0 1 0 547796183 265646080 53438 4294967295 134512640 134672761 3221224544 3221223716 134556606 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 64855 53438 603 41 0 64814 0
vsize: 259420
[startup+90.0144 s]
Raw data (loadavg): 0.94 0.88 0.90 2/55 4481
Raw data (stat): 4428 (minisat+) R 4427 20838 20837 0 -1 0 55358 0 0 0 8864 136 0 0 25 0 1 0 547796183 266604544 53708 4294967295 134512640 134672761 3221224544 3221223712 134561382 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 65089 53708 603 41 0 65048 0
vsize: 260356
[startup+100.014 s]
Raw data (loadavg): 0.95 0.89 0.90 2/55 4481
Raw data (stat): 4428 (minisat+) R 4427 20838 20837 0 -1 0 55384 0 0 0 9863 137 0 0 25 0 1 0 547796183 266739712 53734 4294967295 134512640 134672761 3221224544 3221223716 134556602 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 65122 53734 603 41 0 65081 0
vsize: 260488
[startup+110.015 s]
Raw data (loadavg): 0.96 0.89 0.90 2/55 4483
Raw data (stat): 4428 (minisat+) R 4427 20838 20837 0 -1 0 55473 0 0 0 10863 138 0 0 25 0 1 0 547796183 267010048 53823 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 65188 53823 603 41 0 65147 0
vsize: 260752
[startup+120.015 s]
Raw data (loadavg): 0.97 0.89 0.90 2/55 4483
Raw data (stat): 4428 (minisat+) R 4427 20838 20837 0 -1 0 55477 0 0 0 11863 138 0 0 25 0 1 0 547796183 267010048 53827 4294967295 134512640 134672761 3221224544 3221223760 134561948 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 65188 53827 603 41 0 65147 0
vsize: 260752
[startup+130.015 s]
Raw data (loadavg): 0.97 0.90 0.90 2/55 4483
Raw data (stat): 4428 (minisat+) R 4427 20838 20837 0 -1 0 55527 0 0 0 12862 138 0 0 25 0 1 0 547796183 267337728 53877 4294967295 134512640 134672761 3221224544 3221223716 134556649 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 65268 53877 603 41 0 65227 0
vsize: 261072
[startup+140.014 s]
Raw data (loadavg): 0.97 0.90 0.91 2/55 4483
Raw data (stat): 4428 (minisat+) R 4427 20838 20837 0 -1 0 55676 0 0 0 13862 138 0 0 25 0 1 0 547796183 267878400 54026 4294967295 134512640 134672761 3221224544 3221223716 134556653 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 65400 54026 603 41 0 65359 0
vsize: 261600
[startup+150.014 s]
Raw data (loadavg): 0.98 0.90 0.91 2/55 4483
Raw data (stat): 4428 (minisat+) R 4427 20838 20837 0 -1 0 55702 0 0 0 14862 138 0 0 25 0 1 0 547796183 267878400 54052 4294967295 134512640 134672761 3221224544 3221223680 134560588 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 65400 54052 603 41 0 65359 0
vsize: 261600
[startup+160.014 s]
Raw data (loadavg): 0.98 0.90 0.91 2/55 4483
Raw data (stat): 4428 (minisat+) R 4427 20838 20837 0 -1 0 55712 0 0 0 15862 139 0 0 25 0 1 0 547796183 268013568 54062 4294967295 134512640 134672761 3221224544 3221223712 134560917 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 65433 54062 603 41 0 65392 0
vsize: 261732
[startup+170.014 s]
Raw data (loadavg): 0.98 0.91 0.91 2/55 4483
Raw data (stat): 4428 (minisat+) R 4427 20838 20837 0 -1 0 55731 0 0 0 16862 139 0 0 25 0 1 0 547796183 268013568 54081 4294967295 134512640 134672761 3221224544 3221223692 134560552 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 65433 54081 603 41 0 65392 0
vsize: 261732
[startup+180.014 s]
Raw data (loadavg): 0.98 0.91 0.91 2/55 4483
Raw data (stat): 4428 (minisat+) R 4427 20838 20837 0 -1 0 55758 0 0 0 17862 139 0 0 25 0 1 0 547796183 268148736 54108 4294967295 134512640 134672761 3221224544 3221223716 134556688 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 65466 54108 603 41 0 65425 0
vsize: 261864
[startup+190.013 s]
Raw data (loadavg): 0.99 0.91 0.91 2/55 4483
Raw data (stat): 4428 (minisat+) R 4427 20838 20837 0 -1 0 55800 0 0 0 18862 139 0 0 25 0 1 0 547796183 268431360 54150 4294967295 134512640 134672761 3221224544 3221223712 134560892 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 65535 54150 603 41 0 65494 0
vsize: 262140
[startup+200.013 s]
Raw data (loadavg): 0.99 0.91 0.91 2/55 4483
Raw data (stat): 4428 (minisat+) R 4427 20838 20837 0 -1 0 55801 0 0 0 19862 139 0 0 25 0 1 0 547796183 268431360 54151 4294967295 134512640 134672761 3221224544 3221223680 134560588 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 65535 54151 603 41 0 65494 0
vsize: 262140
[startup+210.013 s]
Raw data (loadavg): 0.99 0.92 0.91 2/55 4483
Raw data (stat): 4428 (minisat+) R 4427 20838 20837 0 -1 0 55817 0 0 0 20863 139 0 0 25 0 1 0 547796183 268431360 54167 4294967295 134512640 134672761 3221224544 3221223740 134556584 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 65535 54167 603 41 0 65494 0
vsize: 262140
[startup+220.012 s]
Raw data (loadavg): 0.99 0.92 0.91 2/55 4483
Raw data (stat): 4428 (minisat+) R 4427 20838 20837 0 -1 0 55835 0 0 0 21863 139 0 0 25 0 1 0 547796183 268431360 54185 4294967295 134512640 134672761 3221224544 3221223668 134566034 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 65535 54185 603 41 0 65494 0
vsize: 262140
[startup+230.012 s]
Raw data (loadavg): 0.99 0.92 0.91 2/55 4483
Raw data (stat): 4428 (minisat+) R 4427 20838 20837 0 -1 0 55862 0 0 0 22863 139 0 0 25 0 1 0 547796183 268566528 54212 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 65568 54212 603 41 0 65527 0
vsize: 262272
[startup+240.013 s]
Raw data (loadavg): 0.99 0.92 0.91 2/55 4483
Raw data (stat): 4428 (minisat+) R 4427 20838 20837 0 -1 0 55879 0 0 0 23863 139 0 0 25 0 1 0 547796183 268701696 54229 4294967295 134512640 134672761 3221224544 3221223744 134557911 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 65601 54229 603 41 0 65560 0
vsize: 262404
[startup+250.013 s]
Raw data (loadavg): 0.99 0.92 0.91 2/55 4483
Raw data (stat): 4428 (minisat+) R 4427 20838 20837 0 -1 0 55914 0 0 0 24863 139 0 0 25 0 1 0 547796183 268836864 54264 4294967295 134512640 134672761 3221224544 3221223696 134565110 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 65634 54264 603 41 0 65593 0
vsize: 262536
[startup+260.013 s]
Raw data (loadavg): 0.99 0.93 0.91 2/55 4483
Raw data (stat): 4428 (minisat+) R 4427 20838 20837 0 -1 0 55935 0 0 0 25863 139 0 0 25 0 1 0 547796183 268836864 54285 4294967295 134512640 134672761 3221224544 3221223668 134566043 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 65634 54285 603 41 0 65593 0
vsize: 262536
[startup+270.013 s]
Raw data (loadavg): 0.99 0.93 0.91 2/55 4483
Raw data (stat): 4428 (minisat+) R 4427 20838 20837 0 -1 0 55950 0 0 0 26863 139 0 0 25 0 1 0 547796183 268967936 54300 4294967295 134512640 134672761 3221224544 3221223744 134561972 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 65666 54300 603 41 0 65625 0
vsize: 262664
[startup+280.013 s]
Raw data (loadavg): 0.99 0.93 0.91 2/55 4485
Raw data (stat): 4428 (minisat+) R 4427 20838 20837 0 -1 0 55966 0 0 0 27863 139 0 0 25 0 1 0 547796183 268967936 54316 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 65666 54316 603 41 0 65625 0
vsize: 262664
[startup+290.013 s]
Raw data (loadavg): 0.99 0.93 0.91 2/55 4485
Raw data (stat): 4428 (minisat+) R 4427 20838 20837 0 -1 0 55979 0 0 0 28863 140 0 0 25 0 1 0 547796183 269103104 54329 4294967295 134512640 134672761 3221224544 3221223668 134566128 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 65699 54329 603 41 0 65658 0
vsize: 262796
[startup+300.013 s]
Raw data (loadavg): 0.99 0.93 0.91 2/55 4485
Raw data (stat): 4428 (minisat+) R 4427 20838 20837 0 -1 0 56004 0 0 0 29863 140 0 0 25 0 1 0 547796183 269103104 54354 4294967295 134512640 134672761 3221224544 3221223716 134556643 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 65699 54354 603 41 0 65658 0
vsize: 262796
[startup+310.014 s]
Raw data (loadavg): 0.99 0.94 0.91 2/55 4485
Raw data (stat): 4428 (minisat+) R 4427 20838 20837 0 -1 0 56021 0 0 0 30864 140 0 0 25 0 1 0 547796183 269238272 54371 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 65732 54371 603 41 0 65691 0
vsize: 262928
[startup+320.013 s]
Raw data (loadavg): 0.99 0.94 0.91 2/55 4485
Raw data (stat): 4428 (minisat+) R 4427 20838 20837 0 -1 0 56036 0 0 0 31864 140 0 0 25 0 1 0 547796183 269238272 54386 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 65732 54386 603 41 0 65691 0
vsize: 262928
[startup+330.013 s]
Raw data (loadavg): 0.99 0.94 0.91 2/55 4485
Raw data (stat): 4428 (minisat+) R 4427 20838 20837 0 -1 0 56054 0 0 0 32864 140 0 0 25 0 1 0 547796183 269373440 54404 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 65765 54404 603 41 0 65724 0
vsize: 263060
[startup+340.014 s]
Raw data (loadavg): 0.99 0.94 0.91 2/55 4485
Raw data (stat): 4428 (minisat+) R 4427 20838 20837 0 -1 0 56066 0 0 0 33863 140 0 0 25 0 1 0 547796183 269373440 54416 4294967295 134512640 134672761 3221224544 3221223700 134561032 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 65765 54416 603 41 0 65724 0
vsize: 263060
[startup+350.013 s]
Raw data (loadavg): 0.99 0.94 0.91 2/55 4485
Raw data (stat): 4428 (minisat+) R 4427 20838 20837 0 -1 0 56100 0 0 0 34864 140 0 0 25 0 1 0 547796183 269635584 54450 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 65829 54450 603 41 0 65788 0
vsize: 263316
[startup+360.013 s]
Raw data (loadavg): 0.99 0.94 0.91 2/55 4487
Raw data (stat): 4428 (minisat+) R 4427 20838 20837 0 -1 0 56101 0 0 0 35864 140 0 0 25 0 1 0 547796183 269635584 54451 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 65829 54451 603 41 0 65788 0
vsize: 263316
[startup+370.012 s]
Raw data (loadavg): 0.99 0.94 0.91 2/55 4487
Raw data (stat): 4428 (minisat+) R 4427 20838 20837 0 -1 0 56109 0 0 0 36864 140 0 0 25 0 1 0 547796183 269635584 54459 4294967295 134512640 134672761 3221224544 3221223760 134561993 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 65829 54459 603 41 0 65788 0
vsize: 263316
[startup+380.013 s]
Raw data (loadavg): 0.99 0.95 0.91 2/55 4487
Raw data (stat): 4428 (minisat+) R 4427 20838 20837 0 -1 0 56472 0 0 0 37863 141 0 0 25 0 1 0 547796183 271110144 54822 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 66189 54822 603 41 0 66148 0
vsize: 264756
[startup+390.013 s]
Raw data (loadavg): 0.99 0.95 0.91 2/55 4487
Raw data (stat): 4428 (minisat+) R 4427 20838 20837 0 -1 0 56484 0 0 0 38863 141 0 0 25 0 1 0 547796183 271245312 54834 4294967295 134512640 134672761 3221224544 3221223716 134556627 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 66222 54834 603 41 0 66181 0
vsize: 264888
[startup+400.013 s]
Raw data (loadavg): 0.99 0.95 0.91 2/55 4487
Raw data (stat): 4428 (minisat+) R 4427 20838 20837 0 -1 0 56549 0 0 0 39863 142 0 0 25 0 1 0 547796183 271380480 54899 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 66255 54899 603 41 0 66214 0
vsize: 265020
[startup+410.013 s]
Raw data (loadavg): 0.99 0.95 0.91 2/55 4487
Raw data (stat): 4428 (minisat+) R 4427 20838 20837 0 -1 0 56622 0 0 0 40863 142 0 0 25 0 1 0 547796183 271650816 54972 4294967295 134512640 134672761 3221224544 3221223716 134556667 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 66321 54972 603 41 0 66280 0
vsize: 265284
[startup+420.013 s]
Raw data (loadavg): 0.99 0.95 0.91 2/55 4487
Raw data (stat): 4428 (minisat+) R 4427 20838 20837 0 -1 0 56637 0 0 0 41863 142 0 0 25 0 1 0 547796183 271781888 54987 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 66353 54987 603 41 0 66312 0
vsize: 265412
[startup+430.013 s]
Raw data (loadavg): 0.99 0.95 0.91 2/55 4487
Raw data (stat): 4428 (minisat+) R 4427 20838 20837 0 -1 0 56657 0 0 0 42863 142 0 0 25 0 1 0 547796183 271781888 55007 4294967295 134512640 134672761 3221224544 3221223680 134560673 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 66353 55007 603 41 0 66312 0
vsize: 265412
[startup+440.013 s]
Raw data (loadavg): 0.99 0.95 0.91 2/55 4487
Raw data (stat): 4428 (minisat+) R 4427 20838 20837 0 -1 0 56717 0 0 0 43863 142 0 0 25 0 1 0 547796183 271917056 55067 4294967295 134512640 134672761 3221224544 3221223760 134561997 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 66386 55067 603 41 0 66345 0
vsize: 265544
[startup+450.012 s]
Raw data (loadavg): 0.99 0.95 0.91 2/55 4487
Raw data (stat): 4428 (minisat+) R 4427 20838 20837 0 -1 0 56737 0 0 0 44863 142 0 0 25 0 1 0 547796183 272048128 55087 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 66418 55087 603 41 0 66377 0
vsize: 265672
[startup+460.012 s]
Raw data (loadavg): 0.99 0.95 0.91 2/55 4487
Raw data (stat): 4428 (minisat+) R 4427 20838 20837 0 -1 0 56749 0 0 0 45864 142 0 0 25 0 1 0 547796183 272048128 55099 4294967295 134512640 134672761 3221224544 3221223712 134560942 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 66418 55099 603 41 0 66377 0
vsize: 265672
[startup+470.012 s]
Raw data (loadavg): 0.99 0.95 0.91 2/55 4487
Raw data (stat): 4428 (minisat+) R 4427 20838 20837 0 -1 0 56769 0 0 0 46864 143 0 0 25 0 1 0 547796183 272179200 55119 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 66450 55119 603 41 0 66409 0
vsize: 265800
[startup+480.012 s]
Raw data (loadavg): 0.99 0.96 0.91 2/55 4487
Raw data (stat): 4428 (minisat+) R 4427 20838 20837 0 -1 0 56806 0 0 0 47864 143 0 0 25 0 1 0 547796183 272314368 55156 4294967295 134512640 134672761 3221224544 3221223716 134556667 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 66483 55156 603 41 0 66442 0
vsize: 265932
[startup+490.012 s]
Raw data (loadavg): 0.99 0.96 0.91 2/55 4487
Raw data (stat): 4428 (minisat+) R 4427 20838 20837 0 -1 0 56899 0 0 0 48863 143 0 0 25 0 1 0 547796183 272711680 55249 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 66580 55249 603 41 0 66539 0
vsize: 266320
[startup+500.011 s]
Raw data (loadavg): 0.99 0.96 0.91 2/55 4487
Raw data (stat): 4428 (minisat+) R 4427 20838 20837 0 -1 0 56920 0 0 0 49864 143 0 0 25 0 1 0 547796183 272711680 55270 4294967295 134512640 134672761 3221224544 3221223744 134557911 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 66580 55270 603 41 0 66539 0
vsize: 266320
[startup+510.012 s]
Raw data (loadavg): 0.99 0.96 0.91 2/55 4487
Raw data (stat): 4428 (minisat+) R 4427 20838 20837 0 -1 0 56952 0 0 0 50863 143 0 0 25 0 1 0 547796183 272846848 55302 4294967295 134512640 134672761 3221224544 3221223696 134561244 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 66613 55302 603 41 0 66572 0
vsize: 266452
[startup+520.011 s]
Raw data (loadavg): 0.99 0.96 0.91 2/55 4487
Raw data (stat): 4428 (minisat+) R 4427 20838 20837 0 -1 0 56967 0 0 0 51863 144 0 0 25 0 1 0 547796183 272982016 55317 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 66646 55317 603 41 0 66605 0
vsize: 266584
[startup+530.011 s]
Raw data (loadavg): 0.99 0.96 0.91 2/55 4487
Raw data (stat): 4428 (minisat+) R 4427 20838 20837 0 -1 0 57017 0 0 0 52862 144 0 0 25 0 1 0 547796183 273117184 55367 4294967295 134512640 134672761 3221224544 3221223744 134557911 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 66679 55367 603 41 0 66638 0
vsize: 266716
[startup+540.011 s]
Raw data (loadavg): 0.99 0.96 0.91 2/55 4487
Raw data (stat): 4428 (minisat+) R 4427 20838 20837 0 -1 0 57041 0 0 0 53862 144 0 0 25 0 1 0 547796183 273252352 55391 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 66712 55391 603 41 0 66671 0
vsize: 266848
[startup+550.013 s]
Raw data (loadavg): 0.99 0.96 0.91 2/55 4487
Raw data (stat): 4428 (minisat+) R 4427 20838 20837 0 -1 0 57055 0 0 0 54863 144 0 0 25 0 1 0 547796183 273252352 55405 4294967295 134512640 134672761 3221224544 3221223712 134564746 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 66712 55405 603 41 0 66671 0
vsize: 266848
[startup+560.013 s]
Raw data (loadavg): 0.99 0.96 0.91 2/55 4487
Raw data (stat): 4428 (minisat+) R 4427 20838 20837 0 -1 0 57066 0 0 0 55863 144 0 0 25 0 1 0 547796183 273252352 55416 4294967295 134512640 134672761 3221224544 3221223748 134561964 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 66712 55416 603 41 0 66671 0
vsize: 266848
[startup+570.012 s]
Raw data (loadavg): 0.99 0.96 0.91 2/55 4487
Raw data (stat): 4428 (minisat+) R 4427 20838 20837 0 -1 0 57081 0 0 0 56863 144 0 0 25 0 1 0 547796183 273383424 55431 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 66744 55431 603 41 0 66703 0
vsize: 266976
[startup+580.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 4489
Raw data (stat): 4428 (minisat+) R 4427 20838 20837 0 -1 0 57099 0 0 0 57863 144 0 0 25 0 1 0 547796183 273383424 55449 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 66744 55449 603 41 0 66703 0
vsize: 266976
[startup+590.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 4489
Raw data (stat): 4428 (minisat+) R 4427 20838 20837 0 -1 0 57121 0 0 0 58863 145 0 0 25 0 1 0 547796183 273780736 55471 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 66841 55471 603 41 0 66800 0
vsize: 267364
[startup+600.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 4489
Raw data (stat): 4428 (minisat+) R 4427 20838 20837 0 -1 0 57143 0 0 0 59863 145 0 0 25 0 1 0 547796183 273915904 55493 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 66874 55493 603 41 0 66833 0
vsize: 267496
[startup+610.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 4489
Raw data (stat): 4428 (minisat+) R 4427 20838 20837 0 -1 0 57164 0 0 0 60864 145 0 0 25 0 1 0 547796183 273915904 55514 4294967295 134512640 134672761 3221224544 3221223680 134560588 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 66874 55514 603 41 0 66833 0
vsize: 267496
[startup+620.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 4489
Raw data (stat): 4428 (minisat+) R 4427 20838 20837 0 -1 0 57215 0 0 0 61863 145 0 0 25 0 1 0 547796183 274186240 55565 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 66940 55565 603 41 0 66899 0
vsize: 267760
[startup+630.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 4489
Raw data (stat): 4428 (minisat+) R 4427 20838 20837 0 -1 0 57236 0 0 0 62863 145 0 0 25 0 1 0 547796183 274186240 55586 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 66940 55586 603 41 0 66899 0
vsize: 267760
[startup+640.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 4489
Raw data (stat): 4428 (minisat+) R 4427 20838 20837 0 -1 0 57259 0 0 0 63863 145 0 0 25 0 1 0 547796183 274321408 55609 4294967295 134512640 134672761 3221224544 3221223696 134565096 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 66973 55609 603 41 0 66932 0
vsize: 267892
[startup+650.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 4489
Raw data (stat): 4428 (minisat+) R 4427 20838 20837 0 -1 0 57288 0 0 0 64864 145 0 0 25 0 1 0 547796183 274456576 55638 4294967295 134512640 134672761 3221224544 3221223716 134556646 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 67006 55638 603 41 0 66965 0
vsize: 268024
[startup+660.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 4489
Raw data (stat): 4428 (minisat+) R 4427 20838 20837 0 -1 0 57316 0 0 0 65864 145 0 0 25 0 1 0 547796183 274591744 55666 4294967295 134512640 134672761 3221224544 3221223732 134556588 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 67039 55666 603 41 0 66998 0
vsize: 268156
[startup+670.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 4489
Raw data (stat): 4428 (minisat+) R 4427 20838 20837 0 -1 0 57338 0 0 0 66864 146 0 0 25 0 1 0 547796183 274591744 55688 4294967295 134512640 134672761 3221224544 3221223696 134565086 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 67039 55688 603 41 0 66998 0
vsize: 268156
[startup+680.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 4489
Raw data (stat): 4428 (minisat+) R 4427 20838 20837 0 -1 0 57363 0 0 0 67864 146 0 0 25 0 1 0 547796183 274726912 55713 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 67072 55713 603 41 0 67031 0
vsize: 268288
[startup+690.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 4489
Raw data (stat): 4428 (minisat+) R 4427 20838 20837 0 -1 0 57401 0 0 0 68864 146 0 0 25 0 1 0 547796183 274862080 55751 4294967295 134512640 134672761 3221224544 3221223668 134566049 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 67105 55751 603 41 0 67064 0
vsize: 268420
[startup+700.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 4489
Raw data (stat): 4428 (minisat+) R 4427 20838 20837 0 -1 0 57425 0 0 0 69864 146 0 0 25 0 1 0 547796183 274997248 55775 4294967295 134512640 134672761 3221224544 3221223712 134560871 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 67138 55775 603 41 0 67097 0
vsize: 268552
[startup+710.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 4489
Raw data (stat): 4428 (minisat+) R 4427 20838 20837 0 -1 0 57446 0 0 0 70864 146 0 0 25 0 1 0 547796183 274997248 55796 4294967295 134512640 134672761 3221224544 3221223712 134560858 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 67138 55796 603 41 0 67097 0
vsize: 268552
[startup+720.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 4489
Raw data (stat): 4428 (minisat+) R 4427 20838 20837 0 -1 0 57606 0 0 0 71864 147 0 0 25 0 1 0 547796183 275656704 55956 4294967295 134512640 134672761 3221224544 3221223680 134560677 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 67299 55956 603 41 0 67258 0
vsize: 269196
[startup+730.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 4489
Raw data (stat): 4428 (minisat+) R 4427 20838 20837 0 -1 0 57626 0 0 0 72863 147 0 0 25 0 1 0 547796183 275791872 55976 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 67332 55976 603 41 0 67291 0
vsize: 269328
[startup+740.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 4489
Raw data (stat): 4428 (minisat+) R 4427 20838 20837 0 -1 0 57645 0 0 0 73863 147 0 0 25 0 1 0 547796183 275791872 55995 4294967295 134512640 134672761 3221224544 3221223744 134557809 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 67332 55995 603 41 0 67291 0
vsize: 269328
[startup+750.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 4489
Raw data (stat): 4428 (minisat+) R 4427 20838 20837 0 -1 0 57664 0 0 0 74863 147 0 0 25 0 1 0 547796183 275927040 56014 4294967295 134512640 134672761 3221224544 3221223760 134561990 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 67365 56014 603 41 0 67324 0
vsize: 269460
[startup+760.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 4489
Raw data (stat): 4428 (minisat+) R 4427 20838 20837 0 -1 0 57686 0 0 0 75863 148 0 0 25 0 1 0 547796183 275927040 56036 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 67365 56036 603 41 0 67324 0
vsize: 269460
[startup+770.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 4489
Raw data (stat): 4428 (minisat+) R 4427 20838 20837 0 -1 0 57701 0 0 0 76863 148 0 0 25 0 1 0 547796183 276062208 56051 4294967295 134512640 134672761 3221224544 3221223732 134556676 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 67398 56051 603 41 0 67357 0
vsize: 269592
[startup+780.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 4489
Raw data (stat): 4428 (minisat+) R 4427 20838 20837 0 -1 0 57710 0 0 0 77863 148 0 0 25 0 1 0 547796183 276062208 56060 4294967295 134512640 134672761 3221224544 3221223668 134566037 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 67398 56060 603 41 0 67357 0
vsize: 269592
[startup+790.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 4489
Raw data (stat): 4428 (minisat+) R 4427 20838 20837 0 -1 0 57733 0 0 0 78864 148 0 0 25 0 1 0 547796183 276197376 56083 4294967295 134512640 134672761 3221224544 3221223716 134556653 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 67431 56083 603 41 0 67390 0
vsize: 269724
[startup+800.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 4489
Raw data (stat): 4428 (minisat+) R 4427 20838 20837 0 -1 0 57752 0 0 0 79864 148 0 0 25 0 1 0 547796183 276197376 56102 4294967295 134512640 134672761 3221224544 3221223712 134560785 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 67431 56102 603 41 0 67390 0
vsize: 269724
[startup+810.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 4489
Raw data (stat): 4428 (minisat+) R 4427 20838 20837 0 -1 0 57833 0 0 0 80863 149 0 0 25 0 1 0 547796183 276598784 56183 4294967295 134512640 134672761 3221224544 3221223716 134556649 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 67529 56183 603 41 0 67488 0
vsize: 270116
[startup+820.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 4489
Raw data (stat): 4428 (minisat+) R 4427 20838 20837 0 -1 0 58005 0 0 0 81863 149 0 0 25 0 1 0 547796183 277266432 56355 4294967295 134512640 134672761 3221224544 3221223712 134560979 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 67692 56355 603 41 0 67651 0
vsize: 270768
[startup+830.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 4489
Raw data (stat): 4428 (minisat+) R 4427 20838 20837 0 -1 0 58026 0 0 0 82863 149 0 0 25 0 1 0 547796183 277266432 56376 4294967295 134512640 134672761 3221224544 3221223712 134560855 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 67692 56376 603 41 0 67651 0
vsize: 270768
[startup+840.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 4489
Raw data (stat): 4428 (minisat+) R 4427 20838 20837 0 -1 0 58047 0 0 0 83863 149 0 0 25 0 1 0 547796183 277401600 56397 4294967295 134512640 134672761 3221224544 3221223696 134565092 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 67725 56397 603 41 0 67684 0
vsize: 270900
[startup+850.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 4489
Raw data (stat): 4428 (minisat+) R 4427 20838 20837 0 -1 0 58066 0 0 0 84863 150 0 0 25 0 1 0 547796183 277401600 56416 4294967295 134512640 134672761 3221224544 3221223680 134560588 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 67725 56416 603 41 0 67684 0
vsize: 270900
[startup+860.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 4489
Raw data (stat): 4428 (minisat+) R 4427 20838 20837 0 -1 0 58086 0 0 0 85864 150 0 0 25 0 1 0 547796183 277536768 56436 4294967295 134512640 134672761 3221224544 3221223744 134557800 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 67758 56436 603 41 0 67717 0
vsize: 271032
[startup+870.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 4489
Raw data (stat): 4428 (minisat+) R 4427 20838 20837 0 -1 0 58125 0 0 0 86864 150 0 0 25 0 1 0 547796183 277671936 56475 4294967295 134512640 134672761 3221224544 3221223728 134558662 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 67791 56475 603 41 0 67750 0
vsize: 271164
[startup+880.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 4491
Raw data (stat): 4428 (minisat+) R 4427 20838 20837 0 -1 0 58209 0 0 0 87864 150 0 0 25 0 1 0 547796183 278077440 56559 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 67890 56559 603 41 0 67849 0
vsize: 271560
[startup+890.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 4491
Raw data (stat): 4428 (minisat+) R 4427 20838 20837 0 -1 0 58248 0 0 0 88863 150 0 0 25 0 1 0 547796183 278212608 56598 4294967295 134512640 134672761 3221224544 3221223712 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 67923 56598 603 41 0 67882 0
vsize: 271692
[startup+900.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 4491
Raw data (stat): 4428 (minisat+) R 4427 20838 20837 0 -1 0 58267 0 0 0 89864 150 0 0 25 0 1 0 547796183 278212608 56617 4294967295 134512640 134672761 3221224544 3221223748 134561964 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 67923 56617 603 41 0 67882 0
vsize: 271692
[startup+910.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 4491
Raw data (stat): 4428 (minisat+) R 4427 20838 20837 0 -1 0 58286 0 0 0 90864 150 0 0 25 0 1 0 547796183 278347776 56636 4294967295 134512640 134672761 3221224544 3221223696 134561244 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 67956 56636 603 41 0 67915 0
vsize: 271824
[startup+920.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 4491
Raw data (stat): 4428 (minisat+) R 4427 20838 20837 0 -1 0 58310 0 0 0 91864 150 0 0 25 0 1 0 547796183 278347776 56660 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 67956 56660 603 41 0 67915 0
vsize: 271824
[startup+930.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 4491
Raw data (stat): 4428 (minisat+) R 4427 20838 20837 0 -1 0 58324 0 0 0 92864 151 0 0 25 0 1 0 547796183 278482944 56674 4294967295 134512640 134672761 3221224544 3221223668 134566037 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 67989 56674 603 41 0 67948 0
vsize: 271956
[startup+940.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 4491
Raw data (stat): 4428 (minisat+) R 4427 20838 20837 0 -1 0 58450 0 0 0 93864 151 0 0 25 0 1 0 547796183 279015424 56800 4294967295 134512640 134672761 3221224544 3221223648 134560059 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 68119 56800 603 41 0 68078 0
vsize: 272476
[startup+950.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 4491
Raw data (stat): 4428 (minisat+) R 4427 20838 20837 0 -1 0 58682 0 0 0 94863 152 0 0 25 0 1 0 547796183 279941120 57032 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 68345 57032 603 41 0 68304 0
vsize: 273380
[startup+960.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 4491
Raw data (stat): 4428 (minisat+) R 4427 20838 20837 0 -1 0 58718 0 0 0 95863 152 0 0 25 0 1 0 547796183 280076288 57068 4294967295 134512640 134672761 3221224544 3221223744 134557842 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 68378 57068 603 41 0 68337 0
vsize: 273512
[startup+970.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 4491
Raw data (stat): 4428 (minisat+) R 4427 20838 20837 0 -1 0 58883 0 0 0 96862 152 0 0 25 0 1 0 547796183 281276416 57233 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 68671 57233 603 41 0 68630 0
vsize: 274684
[startup+980.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 4491
Raw data (stat): 4428 (minisat+) R 4427 20838 20837 0 -1 0 58979 0 0 0 97861 153 0 0 25 0 1 0 547796183 281546752 57329 4294967295 134512640 134672761 3221224544 3221223712 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 68737 57329 603 41 0 68696 0
vsize: 274948
[startup+990.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 4491
Raw data (stat): 4428 (minisat+) R 4427 20838 20837 0 -1 0 58996 0 0 0 98862 153 0 0 25 0 1 0 547796183 281681920 57346 4294967295 134512640 134672761 3221224544 3221223732 134556588 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 68770 57346 603 41 0 68729 0
vsize: 275080
[startup+1000.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 4491
Raw data (stat): 4428 (minisat+) R 4427 20838 20837 0 -1 0 59016 0 0 0 99863 153 0 0 25 0 1 0 547796183 281681920 57366 4294967295 134512640 134672761 3221224544 3221223680 134560726 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 68770 57366 603 41 0 68729 0
vsize: 275080
[startup+1010.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 4491
Raw data (stat): 4428 (minisat+) R 4427 20838 20837 0 -1 0 59236 0 0 0 100865 154 0 0 25 0 1 0 547796183 282619904 57586 4294967295 134512640 134672761 3221224544 3221223680 134560575 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 68999 57586 603 41 0 68958 0
vsize: 275996
[startup+1020.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 4491
Raw data (stat): 4428 (minisat+) R 4427 20838 20837 0 -1 0 59423 0 0 0 101864 154 0 0 25 0 1 0 547796183 283426816 57773 4294967295 134512640 134672761 3221224544 3221223712 134561385 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 69196 57773 603 41 0 69155 0
vsize: 276784
[startup+1030.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 4491
Raw data (stat): 4428 (minisat+) R 4427 20838 20837 0 -1 0 59488 0 0 0 102864 154 0 0 25 0 1 0 547796183 283561984 57838 4294967295 134512640 134672761 3221224544 3221223744 134557830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 69229 57838 603 41 0 69188 0
vsize: 276916
[startup+1040.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 4491
Raw data (stat): 4428 (minisat+) R 4427 20838 20837 0 -1 0 59611 0 0 0 103864 155 0 0 25 0 1 0 547796183 284102656 57961 4294967295 134512640 134672761 3221224544 3221223680 134560694 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 69361 57961 603 41 0 69320 0
vsize: 277444
[startup+1050.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 4491
Raw data (stat): 4428 (minisat+) R 4427 20838 20837 0 -1 0 59662 0 0 0 104864 155 0 0 25 0 1 0 547796183 284368896 58012 4294967295 134512640 134672761 3221224544 3221223712 134560929 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 69426 58012 603 41 0 69385 0
vsize: 277704
[startup+1060.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 4491
Raw data (stat): 4428 (minisat+) R 4427 20838 20837 0 -1 0 59867 0 0 0 105864 155 0 0 25 0 1 0 547796183 285163520 58217 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 69620 58217 603 41 0 69579 0
vsize: 278480
[startup+1070.07 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 4491
Raw data (stat): 4428 (minisat+) R 4427 20838 20837 0 -1 0 60043 0 0 0 106865 156 0 0 25 0 1 0 547796183 285831168 58393 4294967295 134512640 134672761 3221224544 3221223716 134556688 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 69783 58393 603 41 0 69742 0
vsize: 279132
[startup+1080.07 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 4491
Raw data (stat): 4428 (minisat+) R 4427 20838 20837 0 -1 0 60067 0 0 0 107865 156 0 0 25 0 1 0 547796183 285966336 58417 4294967295 134512640 134672761 3221224544 3221223712 134561118 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 69816 58417 603 41 0 69775 0
vsize: 279264
[startup+1090.07 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 4491
Raw data (stat): 4428 (minisat+) R 4427 20838 20837 0 -1 0 60114 0 0 0 108865 156 0 0 25 0 1 0 547796183 286101504 58464 4294967295 134512640 134672761 3221224544 3221223744 134557922 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 69849 58464 603 41 0 69808 0
vsize: 279396
[startup+1100.07 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 4491
Raw data (stat): 4428 (minisat+) R 4427 20838 20837 0 -1 0 60129 0 0 0 109865 156 0 0 25 0 1 0 547796183 286236672 58479 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 69882 58479 603 41 0 69841 0
vsize: 279528
[startup+1110.07 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 4491
Raw data (stat): 4428 (minisat+) R 4427 20838 20837 0 -1 0 60147 0 0 0 110865 156 0 0 25 0 1 0 547796183 286236672 58497 4294967295 134512640 134672761 3221224544 3221223712 134560806 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 69882 58497 603 41 0 69841 0
vsize: 279528
[startup+1120.07 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 4491
Raw data (stat): 4428 (minisat+) R 4427 20838 20837 0 -1 0 60165 0 0 0 111865 156 0 0 25 0 1 0 547796183 286371840 58515 4294967295 134512640 134672761 3221224544 3221223752 134561960 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 69915 58515 603 41 0 69874 0
vsize: 279660
[startup+1130.07 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 4491
Raw data (stat): 4428 (minisat+) R 4427 20838 20837 0 -1 0 60182 0 0 0 112865 156 0 0 25 0 1 0 547796183 286371840 58532 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 69915 58532 603 41 0 69874 0
vsize: 279660
[startup+1140.07 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 4491
Raw data (stat): 4428 (minisat+) R 4427 20838 20837 0 -1 0 60224 0 0 0 113866 156 0 0 25 0 1 0 547796183 286502912 58574 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 69947 58574 603 41 0 69906 0
vsize: 279788
[startup+1150.07 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 4491
Raw data (stat): 4428 (minisat+) R 4427 20838 20837 0 -1 0 60242 0 0 0 114866 156 0 0 25 0 1 0 547796183 286638080 58592 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 69980 58592 603 41 0 69939 0
vsize: 279920
[startup+1160.07 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 4491
Raw data (stat): 4428 (minisat+) R 4427 20838 20837 0 -1 0 60256 0 0 0 115866 156 0 0 25 0 1 0 547796183 286638080 58606 4294967295 134512640 134672761 3221224544 3221223684 134560556 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 69980 58606 603 41 0 69939 0
vsize: 279920
[startup+1170.07 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 4491
Raw data (stat): 4428 (minisat+) R 4427 20838 20837 0 -1 0 60274 0 0 0 116866 156 0 0 25 0 1 0 547796183 286773248 58624 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 70013 58624 603 41 0 69972 0
vsize: 280052
[startup+1180.07 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 4493
Raw data (stat): 4428 (minisat+) R 4427 20838 20837 0 -1 0 60290 0 0 0 117866 157 0 0 25 0 1 0 547796183 286773248 58640 4294967295 134512640 134672761 3221224544 3221223668 134566071 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 70013 58640 603 41 0 69972 0
vsize: 280052
[startup+1190.07 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 4493
Raw data (stat): 4428 (minisat+) R 4427 20838 20837 0 -1 0 60318 0 0 0 118866 157 0 0 25 0 1 0 547796183 286908416 58668 4294967295 134512640 134672761 3221224544 3221223712 134560876 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 70046 58668 603 41 0 70005 0
vsize: 280184
[startup+1200.07 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 4493
Raw data (stat): 4428 (minisat+) R 4427 20838 20837 0 -1 0 60337 0 0 0 119867 157 0 0 25 0 1 0 547796183 287043584 58687 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 70079 58687 603 41 0 70038 0
vsize: 280316
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.19 s]
Raw data (loadavg): 0.99 0.97 0.91 1/55 4493
Raw data (stat): 4428 (minisat+) Z 4427 20838 20837 0 -1 12 60339 0 0 0 119867 168 0 0 25 0 1 0 547796183 0 0 4294967295 0 0 0 0 0 0 16384 5 16386 3222412051 0 0 17 0 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.19
CPU time (s): 1200.36
CPU user time (s): 1198.67
CPU system time (s): 1.68774
CPU usage (%): 100.014
Max. virtual memory (Kb): 280316
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####