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:
  1. 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.
  2. SOLVER DATA
    This is the output of the solver (stdout and stderr).
  3. 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.
  4. 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

Namenormalized-opb/mps-v2-13-7/ftp.netlib.org/lp/data/normalized-mps-v2-13-7-sctap3.opb
MD5SUM9acbf5c4d628ba2ce39f0b2ebe624ef2
Bench Categoryoptimization, medium integers (OPTMEDINT)
Has Objective FunctionYES
SatisfiableYES
(Un)Satisfiability was provedYES
Best value of the objective function 64629117
Optimality of the best value was proved NO
Number of terms in the objective function 37200
Biggest coefficient in the objective function 41943040
Number of bits for the biggest coefficient in the objective function 26
Sum of the numbers in the objective function 30639361500
Number of bits of the sum of numbers in the objective function 35
Biggest number in a constraint 41943040
Number of bits of the biggest number in a constraint 26
Biggest sum of numbers in a constraint 30639361500
Number of bits of the biggest sum of numbers35
Best result obtained on this benchmarkSAT
Best CPU time to get the best result obtained on this benchmark1189.14
Number of variables49600
Total number of constraints1480
Number of constraints which are clauses0
Number of constraints which are cardinality constraints (but not clauses)0
Number of constraints which are nor clauses,nor cardinality constraints1480
Minimum length of a constraint60
Maximum length of a constraint620

Trace number 16032 

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

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.091
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:        767584 kB
Buffers:         28936 kB
Cached:         215888 kB
SwapCached:        316 kB
Active:          55284 kB
Inactive:       191824 kB
HighTotal:      131008 kB
HighFree:          252 kB
LowTotal:       903652 kB
LowFree:        767332 kB
SwapTotal:     2097136 kB
SwapFree:      2096236 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           5748 kB
Slab:            14316 kB
Committed_AS:    63596 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-21 06:29:28 (client local time) WITH STATUS 0 IN 1200.4 SECONDS
stats: 16341 7 1200.4 0
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 2028 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: ############################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################
c   -- Clauses(.)/Splits(s): ssssssssssssss
c ---[2041]---> Sorter-cost: 1148     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[2040]---> Sorter-cost: 1148     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[2039]---> Sorter-cost: 1148     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[2038]---> Sorter-cost: 1148     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[2037]---> Sorter-cost: 1148     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[2036]---> Sorter-cost: 1148     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[2035]---> Sorter-cost: 1148     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[2034]---> Sorter-cost: 1148     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[2033]---> Sorter-cost: 1148     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[2032]---> Sorter-cost: 1148     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[2031]---> Sorter-cost: 1148     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[2030]---> Sorter-cost: 1148     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[2029]---> Sorter-cost: 1148     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[2028]---> Sorter-cost: 1148     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[2027]---> Sorter-cost: 1148     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[2026]---> Sorter-cost: 1148     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[2025]---> Sorter-cost: 1148     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[2024]---> Sorter-cost: 1148     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[2023]---> Sorter-cost: 1148     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[2022]---> Sorter-cost: 1148     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[2021]---> Sorter-cost: 1148     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[2020]---> Sorter-cost: 1148     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[2019]---> Sorter-cost: 1148     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[2018]---> Sorter-cost: 1148     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[2017]---> Sorter-cost: 1148     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[2016]---> Sorter-cost: 1148     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[2015]---> Sorter-cost: 1148     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[2014]---> Sorter-cost: 1148     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[2013]---> Sorter-cost: 1148     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[2012]---> Sorter-cost: 1148     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[2011]---> Sorter-cost: 1148     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[2010]---> Sorter-cost: 1148     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[2009]---> Sorter-cost: 1148     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[2008]---> Sorter-cost: 1148     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[2007]---> Sorter-cost: 1148     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[2006]---> Sorter-cost: 1148     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[2005]---> Sorter-cost: 1148     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[2004]---> Sorter-cost: 1148     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[2003]---> Sorter-cost: 1148     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[2002]---> Sorter-cost: 1148     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[2001]---> Sorter-cost: 1148     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[2000]---> Sorter-cost: 1148     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1999]---> Sorter-cost: 1148     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1998]---> Sorter-cost: 1148     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1997]---> Sorter-cost: 1148     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1996]---> Sorter-cost: 1148     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1995]---> Sorter-cost: 1148     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1994]---> Sorter-cost: 1148     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1993]---> Sorter-cost: 1148     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1992]---> Sorter-cost: 1148     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1991]---> Sorter-cost: 1148     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1990]---> Sorter-cost: 1148     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1989]---> Sorter-cost: 1148     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1988]---> Sorter-cost: 1148     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1987]---> Sorter-cost: 1148     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1986]---> Sorter-cost: 1148     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1985]---> Sorter-cost: 1148     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1984]---> Sorter-cost: 1148     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1983]---> Sorter-cost: 1148     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1982]---> Sorter-cost: 1148     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1981]---> Sorter-cost: 1148     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1980]---> Sorter-cost: 1148     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1979]---> Sorter-cost: 1148     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1978]---> Sorter-cost: 2134     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1977]---> Sorter-cost: 2134     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1976]---> Sorter-cost: 2134     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1975]---> Sorter-cost: 2134     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1974]---> Sorter-cost: 2134     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1973]---> Sorter-cost: 2134     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1972]---> Sorter-cost: 2134     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1971]---> Sorter-cost: 2134     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1970]---> Sorter-cost: 2134     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1969]---> Sorter-cost: 2134     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1968]---> Sorter-cost: 2134     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1967]---> Sorter-cost: 2134     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1966]---> Sorter-cost: 2134     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1965]---> Sorter-cost: 2134     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1964]---> Sorter-cost: 2134     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1963]---> Sorter-cost: 2134     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1962]---> Sorter-cost: 2134     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1961]---> Sorter-cost: 2134     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1960]---> Sorter-cost: 2134     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1959]---> Sorter-cost: 2134     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1958]---> Sorter-cost: 2134     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1957]---> Sorter-cost: 2134     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1956]---> Sorter-cost: 2134     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1955]---> Sorter-cost: 2134     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1954]---> Sorter-cost: 2134     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1953]---> Sorter-cost: 2134     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1952]---> Sorter-cost: 2134     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1951]---> Sorter-cost: 2134     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1950]---> Sorter-cost: 2134     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1949]---> Sorter-cost: 2134     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1948]---> Sorter-cost: 2134     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1947]---> Sorter-cost: 2134     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1946]---> Sorter-cost: 2134     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1945]---> Sorter-cost: 2134     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1944]---> Sorter-cost: 2134     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1943]---> Sorter-cost: 2134     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1942]---> Sorter-cost: 2134     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1941]---> Sorter-cost: 2134     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1940]---> Sorter-cost: 2134     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1939]---> Sorter-cost: 2134     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1938]---> Sorter-cost: 2134     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1937]---> Sorter-cost: 2134     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1936]---> Sorter-cost: 2134     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1935]---> Sorter-cost: 2134     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1934]---> Sorter-cost: 2134     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1933]---> Sorter-cost: 2134     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1932]---> Sorter-cost: 2134     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1931]---> Sorter-cost: 2134     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1930]---> Sorter-cost: 2134     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1929]---> Sorter-cost: 2134     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1928]---> Sorter-cost: 2134     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1927]---> Sorter-cost: 2134     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1926]---> Sorter-cost: 2134     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1925]---> Sorter-cost: 2134     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1924]---> Sorter-cost: 2134     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1923]---> Sorter-cost: 2134     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1922]---> Sorter-cost: 2134     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1921]---> Sorter-cost: 2134     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1920]---> Sorter-cost: 2134     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1919]---> Sorter-cost: 2134     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1918]---> Sorter-cost: 2134     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1917]---> Sorter-cost: 2134     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1916]---> Sorter-cost: 2134     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1915]---> Sorter-cost: 2134     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1914]---> Sorter-cost: 2134     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1913]---> Sorter-cost: 2134     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1912]---> Sorter-cost: 2134     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1911]---> Sorter-cost: 2134     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1910]---> Sorter-cost: 2134     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1909]---> Sorter-cost: 2134     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1908]---> Sorter-cost: 2134     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1907]---> Sorter-cost: 2134     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1906]---> Sorter-cost: 2134     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1905]---> Sorter-cost: 2134     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1904]---> Sorter-cost: 2134     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1903]---> Sorter-cost: 2134     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1902]---> Sorter-cost: 2134     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1901]---> Sorter-cost: 2134     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1900]---> Sorter-cost: 2134     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1899]---> Sorter-cost: 2134     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1898]---> Sorter-cost: 2134     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1897]---> Sorter-cost: 2134     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1896]---> Sorter-cost: 2134     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1895]---> Sorter-cost: 2134     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1894]---> Sorter-cost: 2134     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1893]---> Sorter-cost: 2134     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1892]---> Sorter-cost: 2134     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1891]---> Sorter-cost: 2134     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1890]---> Sorter-cost: 2134     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1889]---> Sorter-cost: 2134     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1888]---> Sorter-cost: 2134     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1887]---> Sorter-cost: 2134     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1886]---> Sorter-cost: 2134     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1885]---> Sorter-cost: 2134     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1884]---> Sorter-cost: 2134     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1883]---> Sorter-cost: 2134     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1882]---> Sorter-cost: 2134     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1881]---> Sorter-cost: 2134     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1880]---> Sorter-cost: 2134     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1879]---> Sorter-cost: 2134     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1878]---> Sorter-cost: 2134     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1877]---> Sorter-cost: 2134     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1876]---> Sorter-cost: 2134     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1875]---> Sorter-cost: 2134     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1874]---> Sorter-cost: 2134     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1873]---> Sorter-cost: 2134     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1872]---> Sorter-cost: 2134     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1871]---> Sorter-cost: 2134     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1870]---> Sorter-cost: 2134     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1869]---> Sorter-cost: 2134     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1868]---> Sorter-cost: 2134     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1867]---> Sorter-cost: 2134     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1866]---> Sorter-cost: 2134     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1865]---> Sorter-cost: 2134     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1864]---> Sorter-cost: 2134     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1863]---> Sorter-cost: 2134     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1862]---> Sorter-cost: 2134     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1861]---> Sorter-cost: 2134     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1860]---> Sorter-cost: 2134     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1859]---> Sorter-cost: 2134     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1858]---> Sorter-cost: 2134     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1857]---> Sorter-cost: 2134     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1856]---> Sorter-cost: 2134     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1855]---> Sorter-cost: 2134     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1854]---> Sorter-cost: 2134     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1853]---> Sorter-cost: 2134     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1852]---> Sorter-cost: 1913     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1851]---> Sorter-cost: 1913     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1850]---> Sorter-cost: 1913     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1849]---> Sorter-cost: 1913     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1848]---> Sorter-cost: 1913     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1847]---> Sorter-cost: 1913     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1846]---> Sorter-cost: 1913     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1845]---> Sorter-cost: 1913     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1844]---> Sorter-cost: 1913     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1843]---> Sorter-cost: 1913     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1842]---> Sorter-cost: 1913     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1841]---> Sorter-cost: 1913     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1840]---> Sorter-cost: 1913     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1839]---> Sorter-cost: 1913     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1838]---> Sorter-cost: 1913     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1837]---> Sorter-cost: 1913     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1836]---> Sorter-cost: 1913     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1835]---> Sorter-cost: 1913     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1834]---> Sorter-cost: 1913     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1833]---> Sorter-cost: 1913     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1832]---> Sorter-cost: 1913     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1831]---> Sorter-cost: 1913     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1830]---> Sorter-cost: 1913     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1829]---> Sorter-cost: 1913     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1828]---> Sorter-cost: 1913     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1827]---> Sorter-cost: 1913     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1826]---> Sorter-cost: 1913     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1825]---> Sorter-cost: 1913     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1824]---> Sorter-cost: 1913     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1823]---> Sorter-cost: 1913     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1822]---> Sorter-cost: 1913     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1821]---> Sorter-cost: 1913     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1820]---> Sorter-cost: 1913     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1819]---> Sorter-cost: 1913     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1818]---> Sorter-cost: 1913     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1817]---> Sorter-cost: 1913     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1816]---> Sorter-cost: 1913     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1815]---> Sorter-cost: 1913     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1814]---> Sorter-cost: 1913     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1813]---> Sorter-cost: 1913     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1812]---> Sorter-cost: 1913     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1811]---> Sorter-cost: 1913     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1810]---> Sorter-cost: 1913     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1809]---> Sorter-cost: 1913     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1808]---> Sorter-cost: 1913     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1807]---> Sorter-cost: 1913     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1806]---> Sorter-cost: 1913     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1805]---> Sorter-cost: 1913     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1804]---> Sorter-cost: 1913     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1803]---> Sorter-cost: 1913     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1802]---> Sorter-cost: 1913     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1801]---> Sorter-cost: 1913     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1800]---> Sorter-cost: 1913     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1799]---> Sorter-cost: 1913     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1798]---> Sorter-cost: 1913     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1797]---> Sorter-cost: 1913     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1796]---> Sorter-cost: 1913     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1795]---> Sorter-cost: 1913     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1794]---> Sorter-cost: 1913     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1793]---> Sorter-cost: 1913     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1792]---> Sorter-cost: 1913     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1791]---> Sorter-cost: 1913     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1790]---> Sorter-cost: 1913     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1789]---> Sorter-cost: 1913     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1788]---> Sorter-cost: 1913     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1787]---> Sorter-cost: 1913     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1786]---> Sorter-cost: 1913     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1785]---> Sorter-cost: 1913     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1784]---> Sorter-cost: 1913     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1783]---> Sorter-cost: 1913     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1782]---> Sorter-cost: 1913     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1781]---> Sorter-cost: 1913     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1780]---> Sorter-cost: 1913     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1779]---> Sorter-cost: 1913     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1778]---> Sorter-cost: 1913     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1777]---> Sorter-cost: 1913     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1776]---> Sorter-cost: 1913     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1775]---> Sorter-cost: 1913     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1774]---> Sorter-cost: 1913     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1773]---> Sorter-cost: 1913     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1772]---> Sorter-cost: 1913     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1771]---> Sorter-cost: 1913     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1770]---> Sorter-cost: 1913     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1769]---> Sorter-cost: 1913     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1768]---> Sorter-cost: 1913     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1767]---> Sorter-cost: 1913     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1766]---> Sorter-cost: 1913     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1765]---> Sorter-cost: 1913     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1764]---> Sorter-cost: 1913     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1763]---> Sorter-cost: 1913     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1762]---> Sorter-cost: 1913     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1761]---> Sorter-cost: 1913     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1760]---> Sorter-cost: 1913     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1759]---> Sorter-cost: 1913     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1758]---> Sorter-cost: 1913     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1757]---> Sorter-cost: 1913     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1756]---> Sorter-cost: 1913     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1755]---> Sorter-cost: 1913     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1754]---> Sorter-cost: 1913     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1753]---> Sorter-cost: 1913     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1752]---> Sorter-cost: 1913     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1751]---> Sorter-cost: 1913     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1750]---> Sorter-cost: 1913     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1749]---> Sorter-cost: 1913     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1748]---> Sorter-cost: 1913     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1747]---> Sorter-cost: 1913     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1746]---> Sorter-cost: 1913     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1745]---> Sorter-cost: 1913     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1744]---> Sorter-cost: 1913     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1743]---> Sorter-cost: 1913     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1742]---> Sorter-cost: 1913     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1741]---> Sorter-cost: 1913     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1740]---> Sorter-cost: 1913     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1739]---> Sorter-cost: 1913     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1738]---> Sorter-cost: 1913     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1737]---> Sorter-cost: 1913     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1736]---> Sorter-cost: 1913     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1735]---> Sorter-cost: 1913     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1734]---> Sorter-cost: 1913     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1733]---> Sorter-cost: 1913     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1732]---> Sorter-cost: 1913     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1731]---> Sorter-cost: 1913     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1730]---> Sorter-cost: 1913     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1729]---> Sorter-cost: 1913     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1728]---> Sorter-cost: 1913     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1727]---> Sorter-cost: 1913     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1726]---> Sorter-cost: 1864     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1725]---> Sorter-cost: 1864     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1724]---> Sorter-cost: 1864     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1723]---> Sorter-cost: 1864     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1722]---> Sorter-cost: 1864     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1721]---> Sorter-cost: 1864     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1720]---> Sorter-cost: 1864     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1719]---> Sorter-cost: 1864     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1718]---> Sorter-cost: 1864     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1717]---> Sorter-cost: 1864     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1716]---> Sorter-cost: 1864     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1715]---> Sorter-cost: 1864     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1714]---> Sorter-cost: 1864     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1713]---> Sorter-cost: 1864     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1712]---> Sorter-cost: 1864     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1711]---> Sorter-cost: 1864     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1710]---> Sorter-cost: 1864     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1709]---> Sorter-cost: 1864     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1708]---> Sorter-cost: 1864     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1707]---> Sorter-cost: 1864     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1706]---> Sorter-cost: 1864     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1705]---> Sorter-cost: 1864     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1704]---> Sorter-cost: 1864     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1703]---> Sorter-cost: 1864     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1702]---> Sorter-cost: 1864     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1701]---> Sorter-cost: 1864     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1700]---> Sorter-cost: 1864     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1699]---> Sorter-cost: 1148     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1698]---> Sorter-cost: 1148     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1697]---> Sorter-cost: 1148     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1696]---> Sorter-cost: 1148     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1695]---> Sorter-cost: 1148     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1694]---> Sorter-cost: 1148     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1693]---> Sorter-cost: 1148     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1692]---> Sorter-cost: 1148     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1691]---> Sorter-cost: 1148     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1690]---> Sorter-cost: 1148     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1689]---> Sorter-cost: 1148     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1688]---> Sorter-cost: 1148     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1687]---> Sorter-cost: 1148     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1686]---> Sorter-cost: 1148     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1685]---> Sorter-cost: 1148     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1684]---> Sorter-cost: 1148     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1683]---> Sorter-cost: 1148     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1682]---> Sorter-cost: 1148     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1681]---> Sorter-cost: 1148     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1680]---> Sorter-cost: 1148     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1679]---> Sorter-cost: 1148     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1678]---> Sorter-cost: 1148     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1677]---> Sorter-cost: 1148     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1676]---> Sorter-cost: 1148     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1675]---> Sorter-cost: 1148     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1674]---> Sorter-cost: 1148     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1673]---> Sorter-cost: 1148     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1672]---> Sorter-cost: 1148     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1671]---> Sorter-cost: 1148     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1670]---> Sorter-cost: 1148     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1669]---> Sorter-cost: 1148     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1668]---> Sorter-cost: 1148     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1667]---> Sorter-cost: 1148     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1666]---> Sorter-cost: 1148     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1665]---> Sorter-cost: 1148     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1664]---> Sorter-cost: 1148     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1663]---> Sorter-cost: 1148     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1662]---> Sorter-cost: 1148     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1661]---> Sorter-cost: 1148     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1660]---> Sorter-cost: 1148     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1659]---> Sorter-cost: 1148     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1658]---> Sorter-cost: 1148     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1657]---> Sorter-cost: 1148     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1656]---> Sorter-cost: 1148     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1655]---> Sorter-cost: 1148     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1654]---> Sorter-cost: 1148     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1653]---> Sorter-cost: 1148     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1652]---> Sorter-cost: 1148     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1651]---> Sorter-cost: 1148     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1650]---> Sorter-cost: 1148     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1649]---> Sorter-cost: 1148     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1648]---> Sorter-cost: 1148     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1647]---> Sorter-cost: 1148     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1646]---> Sorter-cost: 1148     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1645]---> Sorter-cost: 1148     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1644]---> Sorter-cost: 1148     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1643]---> Sorter-cost: 1148     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1642]---> Sorter-cost: 1148     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1641]---> Sorter-cost: 1148     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1640]---> Sorter-cost: 1148     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1639]---> Sorter-cost: 1148     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1638]---> Sorter-cost: 1148     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1637]---> Sorter-cost: 1148     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1636]---> Sorter-cost: 1148     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1635]---> Sorter-cost: 1148     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1634]---> Sorter-cost: 1148     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1633]---> Sorter-cost: 1148     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1632]---> Sorter-cost: 1148     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1631]---> Sorter-cost: 1148     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1630]---> Sorter-cost: 1148     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1629]---> Sorter-cost: 1148     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1628]---> Sorter-cost: 1148     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1627]---> Sorter-cost: 1148     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1626]---> Sorter-cost: 1148     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1625]---> Sorter-cost: 1148     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1624]---> Sorter-cost: 1148     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1623]---> Sorter-cost: 1148     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1622]---> Sorter-cost: 1148     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1621]---> Sorter-cost: 1148     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1620]---> Sorter-cost: 1148     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1619]---> Sorter-cost: 1148     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1618]---> Sorter-cost: 1148     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1617]---> Sorter-cost: 1148     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1616]---> Sorter-cost: 1148     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1615]---> Sorter-cost: 1148     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1614]---> Sorter-cost: 1148     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1613]---> Sorter-cost: 1148     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1612]---> Sorter-cost: 1148     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1611]---> Sorter-cost: 1148     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1610]---> Sorter-cost: 1148     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1609]---> Sorter-cost: 1148     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1608]---> Sorter-cost: 1148     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1607]---> Sorter-cost: 1148     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1606]---> Sorter-cost: 1148     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1605]---> Sorter-cost: 1148     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1604]---> Sorter-cost: 1148     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1603]---> Sorter-cost: 1148     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1602]---> Sorter-cost: 1148     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1601]---> Sorter-cost: 1148     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1600]---> Sorter-cost: 1148     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1599]---> Sorter-cost: 1148     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1598]---> Sorter-cost: 1148     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1597]---> Sorter-cost: 1148     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1596]---> Sorter-cost: 1148     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1595]---> Sorter-cost: 1148     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1594]---> Sorter-cost: 1148     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1593]---> Sorter-cost: 1148     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1592]---> Sorter-cost: 1148     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1591]---> Sorter-cost: 1148     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1590]---> Sorter-cost: 1148     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1589]---> Sorter-cost: 1148     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1588]---> Sorter-cost: 1148     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1587]---> Sorter-cost: 1148     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1586]---> Sorter-cost: 1148     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1585]---> Sorter-cost: 1148     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1584]---> Sorter-cost: 1148     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1583]---> Sorter-cost: 1148     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1582]---> Sorter-cost: 1148     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1581]---> Sorter-cost: 1148     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1580]---> Sorter-cost: 1148     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1579]---> Sorter-cost: 1148     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1578]---> Sorter-cost: 1148     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1577]---> Sorter-cost: 1148     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1576]---> Sorter-cost: 1148     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1575]---> Sorter-cost: 1148     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1574]---> Sorter-cost: 1148     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1573]---> Sorter-cost: 1148     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1572]---> Sorter-cost: 1148     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1571]---> Sorter-cost: 1148     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1570]---> Sorter-cost: 1148     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1569]---> Sorter-cost: 1148     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1568]---> Sorter-cost: 1148     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1567]---> Sorter-cost: 1148     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1566]---> Sorter-cost: 1148     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1565]---> Sorter-cost: 1148     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1564]---> Sorter-cost: 1148     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1563]---> Sorter-cost: 1148     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1562]---> Sorter-cost: 1148     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1561]---> Sorter-cost: 1148     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1560]---> Sorter-cost: 1148     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1559]---> Sorter-cost: 1148     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1558]---> Sorter-cost: 1148     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1557]---> Sorter-cost: 1148     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1556]---> Sorter-cost: 1148     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1555]---> Sorter-cost: 1148     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1554]---> Sorter-cost: 1148     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1553]---> Sorter-cost: 1148     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1552]---> Sorter-cost: 1148     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1551]---> Sorter-cost: 1148     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1550]---> Sorter-cost: 1148     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1549]---> Sorter-cost: 1148     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1548]---> Sorter-cost: 1148     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1547]---> Sorter-cost: 1148     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1546]---> Sorter-cost: 1148     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1545]---> Sorter-cost: 1148     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1544]---> Sorter-cost: 1148     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1543]---> Sorter-cost: 1148     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1542]---> Sorter-cost: 1148     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1541]---> Sorter-cost: 1148     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1540]---> Sorter-cost: 1148     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1539]---> Sorter-cost: 1148     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1538]---> Sorter-cost: 1148     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1537]---> Sorter-cost: 1148     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1536]---> Sorter-cost: 1148     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1535]---> Sorter-cost: 1148     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1534]---> Sorter-cost: 1148     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1533]---> Sorter-cost: 1148     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1532]---> Sorter-cost: 1148     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1531]---> Sorter-cost: 1148     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1530]---> Sorter-cost: 1148     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1529]---> Sorter-cost: 1148     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1528]---> Sorter-cost: 1148     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1527]---> Sorter-cost: 1148     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1526]---> Sorter-cost: 1148     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1525]---> Sorter-cost: 1148     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1524]---> Sorter-cost: 1148     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1523]---> Sorter-cost: 1148     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1522]---> Sorter-cost: 1148     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1521]---> Sorter-cost: 1148     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1520]---> Sorter-cost: 1148     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1519]---> Sorter-cost: 1148     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1518]---> Sorter-cost: 1148     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1517]---> Sorter-cost: 1148     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1516]---> Sorter-cost: 1148     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1515]---> Sorter-cost: 1148     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1514]---> Sorter-cost: 1148     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1513]---> Sorter-cost: 1148     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1512]---> Sorter-cost: 1148     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1511]---> Sorter-cost: 1148     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1510]---> Sorter-cost: 1148     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1509]---> Sorter-cost: 1148     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1508]---> Sorter-cost: 1148     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1507]---> Sorter-cost: 1148     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1506]---> Sorter-cost: 1148     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1505]---> Sorter-cost: 1148     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1504]---> Sorter-cost: 1148     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1503]---> Sorter-cost: 1148     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1502]---> Sorter-cost: 1148     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1501]---> Sorter-cost: 1148     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1500]---> Sorter-cost: 1148     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1499]---> Sorter-cost: 1148     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1498]---> Sorter-cost: 1148     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1497]---> Sorter-cost: 1148     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1496]---> Sorter-cost: 1148     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1495]---> Sorter-cost: 1148     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1494]---> Sorter-cost: 1148     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1493]---> Sorter-cost: 1148     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1492]---> Sorter-cost: 1148     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1491]---> Sorter-cost: 1148     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1490]---> Sorter-cost: 1148     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1489]---> Sorter-cost: 1148     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1488]---> Sorter-cost: 1148     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1487]---> Sorter-cost: 1148     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1486]---> Sorter-cost: 1148     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1485]---> Sorter-cost: 1148     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1484]---> Sorter-cost: 1148     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1482]---> BDD-cost:   76
c ---[1480]---> BDD-cost:   76
c ---[1478]---> BDD-cost:   76
c ---[1476]---> BDD-cost:   76
c ---[1474]---> BDD-cost:   76
c ---[1472]---> BDD-cost:   76
c ---[1470]---> BDD-cost:   76
c ---[1468]---> BDD-cost:   76
c ---[1466]---> BDD-cost:   76
c ---[1464]---> BDD-cost:   76
c ---[1462]---> BDD-cost:   76
c ---[1460]---> BDD-cost:   76
c ---[1458]---> BDD-cost:   76
c ---[1456]---> BDD-cost:   76
c ---[1454]---> BDD-cost:   76
c ---[1452]---> BDD-cost:   76
c ---[1450]---> BDD-cost:   76
c ---[1448]---> BDD-cost:   76
c ---[1446]---> BDD-cost:   76
c ---[1444]---> BDD-cost:   76
c ---[1442]---> BDD-cost:   76
c ---[1440]---> BDD-cost:   76
c ---[1438]---> BDD-cost:   76
c ---[1436]---> BDD-cost:   76
c ---[1434]---> BDD-cost:   76
c ---[1432]---> BDD-cost:   76
c ---[1430]---> BDD-cost:   76
c ---[1428]---> BDD-cost:   76
c ---[1426]---> BDD-cost:   76
c ---[1424]---> BDD-cost:   76
c ---[1422]---> BDD-cost:   76
c ---[1420]---> BDD-cost:   76
c ---[1418]---> BDD-cost:   76
c ---[1416]---> BDD-cost:   76
c ---[1414]---> BDD-cost:   76
c ---[1412]---> BDD-cost:   76
c ---[1410]---> BDD-cost:   76
c ---[1408]---> BDD-cost:   76
c ---[1406]---> BDD-cost:   76
c ---[1404]---> BDD-cost:   76
c ---[1402]---> BDD-cost:   76
c ---[1400]---> BDD-cost:   76
c ---[1398]---> BDD-cost:   76
c ---[1396]---> BDD-cost:   76
c ---[1394]---> BDD-cost:   76
c ---[1392]---> BDD-cost:   76
c ---[1390]---> BDD-cost:   76
c ---[1388]---> BDD-cost:   76
c ---[1386]---> BDD-cost:   76
c ---[1384]---> BDD-cost:   76
c ---[1382]---> BDD-cost:   76
c ---[1380]---> BDD-cost:   76
c ---[1378]---> BDD-cost:   76
c ---[1376]---> BDD-cost:   76
c ---[1374]---> BDD-cost:   76
c ---[1372]---> BDD-cost:   76
c ---[1370]---> BDD-cost:   76
c ---[1368]---> BDD-cost:   76
c ---[1366]---> BDD-cost:   76
c ---[1364]---> BDD-cost:   76
c ---[1362]---> BDD-cost:   76
c ---[1360]---> BDD-cost:   76
c ---[1358]---> BDD-cost:   76
c ---[1356]---> BDD-cost:   76
c ---[1354]---> BDD-cost:   76
c ---[1352]---> BDD-cost:   76
c ---[1350]---> BDD-cost:   76
c ---[1348]---> BDD-cost:   76
c ---[1346]---> BDD-cost:   76
c ---[1344]---> BDD-cost:   76
c ---[1342]---> BDD-cost:   76
c ---[1340]---> BDD-cost:   76
c ---[1338]---> BDD-cost:   76
c ---[1336]---> BDD-cost:   76
c ---[1334]---> BDD-cost:   76
c ---[1332]---> BDD-cost:   76
c ---[1330]---> BDD-cost:   76
c ---[1328]---> BDD-cost:   76
c ---[1326]---> BDD-cost:   76
c ---[1324]---> BDD-cost:   76
c ---[1322]---> BDD-cost:   76
c ---[1320]---> BDD-cost:   76
c ---[1318]---> BDD-cost:   76
c ---[1316]---> BDD-cost:   76
c ---[1314]---> BDD-cost:   76
c ---[1312]---> BDD-cost:   76
c ---[1310]---> BDD-cost:   76
c ---[1308]---> BDD-cost:   76
c ---[1306]---> BDD-cost:   76
c ---[1304]---> BDD-cost:   76
c ---[1302]---> BDD-cost:   76
c ---[1300]---> BDD-cost:   76
c ---[1298]---> BDD-cost:   76
c ---[1296]---> BDD-cost:   76
c ---[1294]---> BDD-cost:   76
c ---[1292]---> BDD-cost:   76
c ---[1290]---> BDD-cost:   76
c ---[1288]---> BDD-cost:   76
c ---[1286]---> BDD-cost:   76
c ---[1284]---> BDD-cost:   76
c ---[1282]---> BDD-cost:   76
c ---[1280]---> BDD-cost:   76
c ---[1278]---> BDD-cost:   76
c ---[1276]---> BDD-cost:   76
c ---[1274]---> BDD-cost:   76
c ---[1272]---> BDD-cost:   76
c ---[1270]---> BDD-cost:   76
c ---[1268]---> BDD-cost:   76
c ---[1266]---> BDD-cost:   76
c ---[1264]---> BDD-cost:   76
c ---[1262]---> BDD-cost:   76
c ---[1260]---> BDD-cost:   76
c ---[1258]---> BDD-cost:   76
c ---[1256]---> BDD-cost:   76
c ---[1254]---> BDD-cost:   76
c ---[1252]---> BDD-cost:   76
c ---[1250]---> BDD-cost:   76
c ---[1248]---> BDD-cost:   76
c ---[1246]---> BDD-cost:   76
c ---[1244]---> BDD-cost:   76
c ---[1242]---> BDD-cost:   76
c ---[1240]---> BDD-cost:   76
c ---[1238]---> BDD-cost:   76
c ---[1236]---> BDD-cost:   76
c ---[1234]---> BDD-cost:   76
c ---[1232]---> BDD-cost:   76
c ---[1230]---> BDD-cost:   76
c ---[1228]---> BDD-cost:   76
c ---[1226]---> BDD-cost:   76
c ---[1224]---> BDD-cost:   76
c ---[1222]---> BDD-cost:   76
c ---[1220]---> BDD-cost:   76
c ---[1218]---> BDD-cost:   76
c ---[1216]---> BDD-cost:   76
c ---[1214]---> BDD-cost:   76
c ---[1212]---> BDD-cost:   76
c ---[1210]---> BDD-cost:   76
c ---[1208]---> BDD-cost:   76
c ---[1206]---> BDD-cost:   76
c ---[1204]---> BDD-cost:   76
c ---[1202]---> BDD-cost:   76
c ---[1200]---> BDD-cost:   76
c ---[1198]---> BDD-cost:   76
c ---[1196]---> BDD-cost:   76
c ---[1194]---> BDD-cost:   76
c ---[1192]---> BDD-cost:   76
c ---[1190]---> BDD-cost:   76
c ---[1188]---> BDD-cost:   76
c ---[1186]---> BDD-cost:   76
c ---[1184]---> BDD-cost:   76
c ---[1182]---> BDD-cost:   76
c ---[1180]---> BDD-cost:   76
c ---[1178]---> BDD-cost:   76
c ---[1176]---> BDD-cost:   76
c ---[1174]---> BDD-cost:   76
c ---[1172]---> BDD-cost:   76
c ---[1170]---> BDD-cost:   76
c ---[1168]---> BDD-cost:   76
c ---[1166]---> BDD-cost:   76
c ---[1164]---> BDD-cost:   76
c ---[1162]---> BDD-cost:   76
c ---[1160]---> BDD-cost:   76
c ---[1158]---> BDD-cost:   76
c ---[1156]---> BDD-cost:   76
c ---[1154]---> BDD-cost:   76
c ---[1152]---> BDD-cost:   76
c ---[1150]---> BDD-cost:   76
c ---[1148]---> BDD-cost:   76
c ---[1146]---> BDD-cost:   76
c ---[1144]---> BDD-cost:   76
c ---[1142]---> BDD-cost:   76
c ---[1140]---> BDD-cost:   76
c ---[1138]---> BDD-cost:   76
c ---[1136]---> BDD-cost:   76
c ---[1134]---> BDD-cost:   76
c ---[1132]---> BDD-cost:   76
c ---[1130]---> BDD-cost:   76
c ---[1128]---> BDD-cost:   76
c ---[1126]---> BDD-cost:   76
c ---[1124]---> BDD-cost:   76
c ---[1122]---> BDD-cost:   76
c ---[1120]---> BDD-cost:   76
c ---[1118]---> BDD-cost:   76
c ---[1116]---> BDD-cost:   76
c ---[1114]---> BDD-cost:   76
c ---[1112]---> BDD-cost:   76
c ---[1110]---> BDD-cost:   76
c ---[1108]---> BDD-cost:   76
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:   74
c ---[1060]---> BDD-cost:   76
c ---[1058]---> BDD-cost:   74
c ---[1056]---> BDD-cost:   74
c ---[1054]---> BDD-cost:   74
c ---[1052]---> BDD-cost:   74
c ---[1050]---> BDD-cost:   74
c ---[1048]---> BDD-cost:   74
c ---[1046]---> BDD-cost:   74
c ---[1044]---> BDD-cost:   74
c ---[1042]---> BDD-cost:   74
c ---[1040]---> BDD-cost:   76
c ---[1038]---> BDD-cost:   74
c ---[1036]---> BDD-cost:   74
c ---[1034]---> BDD-cost:   74
c ---[1032]---> BDD-cost:   74
c ---[1030]---> BDD-cost:   74
c ---[1028]---> BDD-cost:   74
c ---[1026]---> BDD-cost:   74
c ---[1024]---> BDD-cost:   74
c ---[1022]---> BDD-cost:   74
c ---[1020]---> BDD-cost:   76
c ---[1018]---> BDD-cost:   74
c ---[1016]---> BDD-cost:   74
c ---[1014]---> BDD-cost:   74
c ---[1012]---> BDD-cost:   74
c ---[1010]---> BDD-cost:   74
c ---[1008]---> BDD-cost:   74
c ---[1006]---> BDD-cost:   74
c ---[1004]---> BDD-cost:   74
c ---[1002]---> BDD-cost:   74
c ---[1000]---> BDD-cost:   76
c ---[ 998]---> BDD-cost:   74
c ---[ 996]---> BDD-cost:   74
c ---[ 994]---> BDD-cost:   74
c ---[ 992]---> BDD-cost:   74
c ---[ 990]---> BDD-cost:   74
c ---[ 988]---> BDD-cost:   74
c ---[ 986]---> BDD-cost:   74
c ---[ 984]---> BDD-cost:   74
c ---[ 982]---> BDD-cost:   74
c ---[ 980]---> BDD-cost:   76
c ---[ 978]---> BDD-cost:   74
c ---[ 976]---> BDD-cost:   74
c ---[ 974]---> BDD-cost:   74
c ---[ 972]---> BDD-cost:   74
c ---[ 970]---> BDD-cost:   74
c ---[ 968]---> BDD-cost:   74
c ---[ 966]---> BDD-cost:   74
c ---[ 964]---> BDD-cost:   74
c ---[ 962]---> BDD-cost:   74
c ---[ 960]---> BDD-cost:   76
c ---[ 958]---> BDD-cost:   74
c ---[ 956]---> BDD-cost:   74
c ---[ 954]---> BDD-cost:   74
c ---[ 952]---> BDD-cost:   74
c ---[ 950]---> BDD-cost:   74
c ---[ 948]---> BDD-cost:   74
c ---[ 946]---> BDD-cost:   74
c ---[ 944]---> BDD-cost:   74
c ---[ 942]---> BDD-cost:   74
c ---[ 940]---> BDD-cost:   76
c ---[ 938]---> BDD-cost:   74
c ---[ 936]---> BDD-cost:   74
c ---[ 934]---> BDD-cost:   74
c ---[ 932]---> BDD-cost:   74
c ---[ 930]---> BDD-cost:   74
c ---[ 928]---> BDD-cost:   74
c ---[ 926]---> BDD-cost:   74
c ---[ 924]---> BDD-cost:   74
c ---[ 922]---> BDD-cost:   74
c ---[ 920]---> BDD-cost:   76
c ---[ 918]---> BDD-cost:   74
c ---[ 916]---> BDD-cost:   74
c ---[ 914]---> BDD-cost:   74
c ---[ 912]---> BDD-cost:   74
c ---[ 910]---> BDD-cost:   74
c ---[ 908]---> BDD-cost:   74
c ---[ 906]---> BDD-cost:   74
c ---[ 904]---> BDD-cost:   74
c ---[ 902]---> BDD-cost:   74
c ---[ 900]---> BDD-cost:   76
c ---[ 898]---> BDD-cost:   74
c ---[ 896]---> BDD-cost:   74
c ---[ 894]---> BDD-cost:   74
c ---[ 892]---> BDD-cost:   74
c ---[ 890]---> BDD-cost:   74
c ---[ 888]---> BDD-cost:   74
c ---[ 886]---> BDD-cost:   74
c ---[ 884]---> BDD-cost:   74
c ---[ 882]---> BDD-cost:   74
c ---[ 880]---> BDD-cost:   76
c ---[ 878]---> BDD-cost:   74
c ---[ 876]---> BDD-cost:   74
c ---[ 874]---> BDD-cost:   74
c ---[ 872]---> BDD-cost:   74
c ---[ 870]---> BDD-cost:   74
c ---[ 868]---> BDD-cost:   74
c ---[ 866]---> BDD-cost:   74
c ---[ 864]---> BDD-cost:   74
c ---[ 862]---> BDD-cost:   74
c ---[ 860]---> BDD-cost:   76
c ---[ 858]---> BDD-cost:   74
c ---[ 856]---> BDD-cost:   74
c ---[ 854]---> BDD-cost:   74
c ---[ 852]---> BDD-cost:   74
c ---[ 850]---> BDD-cost:   74
c ---[ 848]---> BDD-cost:   74
c ---[ 846]---> BDD-cost:   74
c ---[ 844]---> BDD-cost:   74
c ---[ 842]---> BDD-cost:   74
c ---[ 840]---> BDD-cost:   76
c ---[ 838]---> BDD-cost:   74
c ---[ 836]---> BDD-cost:   74
c ---[ 834]---> BDD-cost:   74
c ---[ 832]---> BDD-cost:   74
c ---[ 830]---> BDD-cost:   74
c ---[ 828]---> BDD-cost:   74
c ---[ 826]---> BDD-cost:   74
c ---[ 824]---> BDD-cost:   74
c ---[ 822]---> BDD-cost:   74
c ---[ 820]---> BDD-cost:   76
c ---[ 818]---> BDD-cost:   74
c ---[ 816]---> BDD-cost:   74
c ---[ 814]---> BDD-cost:   74
c ---[ 812]---> BDD-cost:   74
c ---[ 810]---> BDD-cost:   74
c ---[ 808]---> BDD-cost:   74
c ---[ 806]---> BDD-cost:   74
c ---[ 804]---> BDD-cost:   74
c ---[ 802]---> BDD-cost:   74
c ---[ 800]---> BDD-cost:   76
c ---[ 798]---> BDD-cost:   74
c ---[ 796]---> BDD-cost:   74
c ---[ 794]---> BDD-cost:   74
c ---[ 792]---> BDD-cost:   74
c ---[ 790]---> BDD-cost:   74
c ---[ 788]---> BDD-cost:   74
c ---[ 786]---> BDD-cost:   74
c ---[ 784]---> BDD-cost:   74
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:   76
c ---[ 470]---> BDD-cost:   76
c ---[ 468]---> BDD-cost:   76
c ---[ 466]---> BDD-cost:   76
c ---[ 464]---> BDD-cost:   76
c ---[ 462]---> BDD-cost:   76
c ---[ 460]---> BDD-cost:   76
c ---[ 458]---> BDD-cost:   76
c ---[ 456]---> BDD-cost:   76
c ---[ 454]---> BDD-cost:   76
c ---[ 452]---> BDD-cost:   76
c ---[ 450]---> BDD-cost:   76
c ---[ 448]---> BDD-cost:   76
c ---[ 446]---> BDD-cost:   76
c ---[ 444]---> BDD-cost:   76
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:   76
c ---[ 426]---> BDD-cost:   76
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:   76
c ---[ 400]---> BDD-cost:   76
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:   76
c ---[ 338]---> BDD-cost:   76
c ---[ 336]---> BDD-cost:   76
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:   76
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:   76
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 ---[ 243]---> Adder-cost: 972   maxlim: 3202079   bits: 23/22
c ---[ 242]---> Adder-cost: 972   maxlim: 3202079   bits: 23/22
c ---[ 241]---> Adder-cost: 932   maxlim: 3202079   bits: 23/22
c ---[ 240]---> Adder-cost: 932   maxlim: 3202079   bits: 23/22
c ---[ 239]---> Adder-cost: 932   maxlim: 3202079   bits: 23/22
c ---[ 238]---> Adder-cost: 932   maxlim: 3202079   bits: 23/22
c ---[ 237]---> Adder-cost: 932   maxlim: 3202079   bits: 23/22
c ---[ 236]---> Adder-cost: 932   maxlim: 3202079   bits: 23/22
c ---[ 235]---> Adder-cost: 892   maxlim: 3202079   bits: 23/22
c ---[ 234]---> Adder-cost: 778   maxlim: 2149679   bits: 23/22
c ---[ 233]---> Adder-cost: 778   maxlim: 2149679   bits: 23/22
c ---[ 232]---> Adder-cost: 778   maxlim: 2149679   bits: 23/22
c ---[ 231]---> Adder-cost: 778   maxlim: 2149679   bits: 23/22
c ---[ 230]---> Adder-cost: 778   maxlim: 2149679   bits: 23/22
c ---[ 229]---> Adder-cost: 778   maxlim: 2149679   bits: 23/22
c ---[ 228]---> Adder-cost: 778   maxlim: 2149679   bits: 23/22
c ---[ 227]---> Adder-cost: 778   maxlim: 2149679   bits: 23/22
c ---[ 226]---> Adder-cost: 778   maxlim: 2149679   bits: 23/22
c ---[ 225]---> Adder-cost: 972   maxlim: 3202079   bits: 23/22
c ---[ 224]---> Adder-cost: 972   maxlim: 3202079   bits: 23/22
c ---[ 223]---> Adder-cost: 932   maxlim: 3202079   bits: 23/22
c ---[ 222]---> Adder-cost: 932   maxlim: 3202079   bits: 23/22
c ---[ 221]---> Adder-cost: 932   maxlim: 3202079   bits: 23/22
c ---[ 220]---> Adder-cost: 932   maxlim: 3202079   bits: 23/22
c ---[ 219]---> Adder-cost: 932   maxlim: 3202079   bits: 23/22
c ---[ 218]---> Adder-cost: 932   maxlim: 3202079   bits: 23/22
c ---[ 217]---> Adder-cost: 892   maxlim: 3202079   bits: 23/22
c ---[ 216]---> Adder-cost: 1034   maxlim: 4219544   bits: 24/23
c ---[ 214]---> Adder-cost: 1034   maxlim: 4223384   bits: 24/23
c ---[ 213]---> Adder-cost: 1034   maxlim: 4224664   bits: 24/23
c ---[ 212]---> Adder-cost: 1034   maxlim: 4222104   bits: 24/23
c ---[ 211]---> Adder-cost: 1034   maxlim: 4220184   bits: 24/23
c ---[ 210]---> Adder-cost: 1034   maxlim: 4219544   bits: 24/23
c ---[ 209]---> Adder-cost: 1034   maxlim: 4219544   bits: 24/23
c ---[ 208]---> Adder-cost: 1034   maxlim: 4219544   bits: 24/23
c ---[ 207]---> Adder-cost: 1034   maxlim: 4219544   bits: 24/23
c ---[ 206]---> Adder-cost: 1194   maxlim: 5269394   bits: 24/23
c ---[ 205]---> Adder-cost: 1194   maxlim: 5269394   bits: 24/23
c ---[ 204]---> Adder-cost: 1192   maxlim: 5269394   bits: 24/23
c ---[ 203]---> Adder-cost: 1192   maxlim: 5269394   bits: 24/23
c ---[ 202]---> Adder-cost: 1192   maxlim: 5269394   bits: 24/23
c ---[ 201]---> Adder-cost: 1192   maxlim: 5269394   bits: 24/23
c ---[ 200]---> Adder-cost: 1192   maxlim: 5269394   bits: 24/23
c ---[ 199]---> Adder-cost: 1192   maxlim: 5269394   bits: 24/23
c ---[ 198]---> Adder-cost: 1190   maxlim: 5269394   bits: 24/23
c ---[ 197]---> Adder-cost: 1116   maxlim: 5263019   bits: 24/23
c ---[ 195]---> Adder-cost: 1116   maxlim: 5264299   bits: 24/23
c ---[ 194]---> Adder-cost: 1116   maxlim: 5264299   bits: 24/23
c ---[ 193]---> Adder-cost: 1116   maxlim: 5264299   bits: 24/23
c ---[ 192]---> Adder-cost: 1116   maxlim: 5264299   bits: 24/23
c ---[ 191]---> Adder-cost: 1116   maxlim: 5264299   bits: 24/23
c ---[ 190]---> Adder-cost: 1116   maxlim: 5265579   bits: 24/23
c ---[ 189]---> Adder-cost: 1116   maxlim: 5266859   bits: 24/23
c ---[ 188]---> Adder-cost: 1116   maxlim: 5263659   bits: 24/23
c ---[ 187]---> Sorter-cost: 2549     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 185]---> Sorter-cost: 2549     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 184]---> Sorter-cost: 2549     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 183]---> Sorter-cost: 2549     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 182]---> Sorter-cost: 2549     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 181]---> Sorter-cost: 2549     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 180]---> Sorter-cost: 2549     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 179]---> Sorter-cost: 2549     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 178]---> Sorter-cost: 2549     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 177]---> Sorter-cost: 2549     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 175]---> Sorter-cost: 2549     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 174]---> Sorter-cost: 2549     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 173]---> Sorter-cost: 2549     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 172]---> Sorter-cost: 2549     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 171]---> Sorter-cost: 2549     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 170]---> Sorter-cost: 2549     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 169]---> Sorter-cost: 2549     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 168]---> Sorter-cost: 2549     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 167]---> Sorter-cost: 2549     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 165]---> Sorter-cost: 2549     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 164]---> Sorter-cost: 2549     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 163]---> Sorter-cost: 2549     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 162]---> Sorter-cost: 2549     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 161]---> Sorter-cost: 2549     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 160]---> Sorter-cost: 2549     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 159]---> Sorter-cost: 2549     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 158]---> Sorter-cost: 2549     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 157]---> Sorter-cost: 2549     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 155]---> Sorter-cost: 2549     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 154]---> Sorter-cost: 2549     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 153]---> Sorter-cost: 2549     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 152]---> Sorter-cost: 2549     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 151]---> Sorter-cost: 2549     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 150]---> Sorter-cost: 2549     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 149]---> Sorter-cost: 2549     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 148]---> Sorter-cost: 2549     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 147]---> Sorter-cost: 2549     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 145]---> Sorter-cost: 2549     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 144]---> Sorter-cost: 2549     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 143]---> Sorter-cost: 2549     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 142]---> Sorter-cost: 2549     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 141]---> Sorter-cost: 2549     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 140]---> Sorter-cost: 2549     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 139]---> Sorter-cost: 2549     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 138]---> Sorter-cost: 2549     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 137]---> Sorter-cost: 2549     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 135]---> Sorter-cost: 2549     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 134]---> Sorter-cost: 2549     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 133]---> Sorter-cost: 2549     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 132]---> Sorter-cost: 2549     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 131]---> Sorter-cost: 2549     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 130]---> Sorter-cost: 2549     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 129]---> Sorter-cost: 2549     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 128]---> Sorter-cost: 2549     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 127]---> Adder-cost: 326   maxlim: 1062599   bits: 22/21
c ---[ 125]---> Adder-cost: 326   maxlim: 1062983   bits: 22/21
c ---[ 124]---> Adder-cost: 326   maxlim: 1062727   bits: 22/21
c ---[ 123]---> Adder-cost: 326   maxlim: 1062599   bits: 22/21
c ---[ 122]---> Adder-cost: 326   maxlim: 1062599   bits: 22/21
c ---[ 121]---> Adder-cost: 326   maxlim: 1062599   bits: 22/21
c ---[ 120]---> Adder-cost: 326   maxlim: 1062599   bits: 22/21
c ---[ 119]---> Adder-cost: 326   maxlim: 1062599   bits: 22/21
c ---[ 118]---> Adder-cost: 326   maxlim: 1062599   bits: 22/21
c ---[ 117]---> Adder-cost: 402   maxlim: 2106074   bits: 23/22
c ---[ 115]---> Adder-cost: 402   maxlim: 2106586   bits: 23/22
c ---[ 114]---> Adder-cost: 402   maxlim: 2106074   bits: 23/22
c ---[ 113]---> Adder-cost: 402   maxlim: 2106074   bits: 23/22
c ---[ 112]---> Adder-cost: 402   maxlim: 2106074   bits: 23/22
c ---[ 111]---> Adder-cost: 402   maxlim: 2106074   bits: 23/22
c ---[ 110]---> Adder-cost: 402   maxlim: 2106074   bits: 23/22
c ---[ 109]---> Adder-cost: 402   maxlim: 2106074   bits: 23/22
c ---[ 108]---> Adder-cost: 402   maxlim: 2106074   bits: 23/22
c ---[ 107]---> Adder-cost: 326   maxlim: 1062599   bits: 22/21
c ---[ 105]---> Adder-cost: 326   maxlim: 1062983   bits: 22/21
c ---[ 104]---> Adder-cost: 326   maxlim: 1062727   bits: 22/21
c ---[ 103]---> Adder-cost: 326   maxlim: 1062599   bits: 22/21
c ---[ 102]---> Adder-cost: 326   maxlim: 1062599   bits: 22/21
c ---[ 101]---> Adder-cost: 326   maxlim: 1062599   bits: 22/21
c ---[ 100]---> Adder-cost: 326   maxlim: 1062599   bits: 22/21
c ---[  99]---> Adder-cost: 326   maxlim: 1062599   bits: 22/21
c ---[  98]---> Adder-cost: 326   maxlim: 1062599   bits: 22/21
c ---[  97]---> Adder-cost: 778   maxlim: 3169184   bits: 23/22
c ---[  95]---> Adder-cost: 778   maxlim: 3169440   bits: 23/22
c ---[  94]---> Adder-cost: 738   maxlim: 3169696   bits: 23/22
c ---[  93]---> Adder-cost: 738   maxlim: 3169440   bits: 23/22
c ---[  92]---> Adder-cost: 738   maxlim: 3169184   bits: 23/22
c ---[  91]---> Adder-cost: 738   maxlim: 3169184   bits: 23/22
c ---[  90]---> Adder-cost: 738   maxlim: 3169184   bits: 23/22
c ---[  89]---> Adder-cost: 738   maxlim: 3169184   bits: 23/22
c ---[  88]---> Adder-cost: 698   maxlim: 3169184   bits: 23/22
c ---[  87]---> Adder-cost: 1116   maxlim: 5263019   bits: 24/23
c ---[  85]---> Adder-cost: 1116   maxlim: 5263659   bits: 24/23
c ---[  84]---> Adder-cost: 1116   maxlim: 5263403   bits: 24/23
c ---[  83]---> Adder-cost: 1116   maxlim: 5263147   bits: 24/23
c ---[  82]---> Adder-cost: 1116   maxlim: 5263019   bits: 24/23
c ---[  81]---> Adder-cost: 1116   maxlim: 5263019   bits: 24/23
c ---[  80]---> Adder-cost: 1116   maxlim: 5263019   bits: 24/23
c ---[  79]---> Adder-cost: 1116   maxlim: 5263019   bits: 24/23
c ---[  78]---> Adder-cost: 1116   maxlim: 5263019   bits: 24/23
c ---[  77]---> Adder-cost: 902   maxlim: 4212659   bits: 24/23
c ---[  76]---> Adder-cost: 902   maxlim: 4213043   bits: 24/23
c ---[  75]---> Adder-cost: 902   maxlim: 4213171   bits: 24/23
c ---[  74]---> Adder-cost: 902   maxlim: 4212659   bits: 24/23
c ---[  73]---> Adder-cost: 902   maxlim: 4212659   bits: 24/23
c ---[  72]---> Adder-cost: 902   maxlim: 4212659   bits: 24/23
c ---[  71]---> Adder-cost: 902   maxlim: 4212659   bits: 24/23
c ---[  70]---> Adder-cost: 902   maxlim: 4212659   bits: 24/23
c ---[  69]---> Adder-cost: 902   maxlim: 4212659   bits: 24/23
c ---[  68]---> Adder-cost: 972   maxlim: 3202079   bits: 23/22
c ---[  67]---> Adder-cost: 972   maxlim: 3202207   bits: 23/22
c ---[  66]---> Adder-cost: 932   maxlim: 3202463   bits: 23/22
c ---[  65]---> Adder-cost: 932   maxlim: 3202207   bits: 23/22
c ---[  64]---> Adder-cost: 932   maxlim: 3202079   bits: 23/22
c ---[  63]---> Adder-cost: 932   maxlim: 3202079   bits: 23/22
c ---[  62]---> Adder-cost: 932   maxlim: 3202079   bits: 23/22
c ---[  61]---> Adder-cost: 932   maxlim: 3202079   bits: 23/22
c ---[  60]---> Adder-cost: 892   maxlim: 3202079   bits: 23/22
c ---[  59]---> Adder-cost: 778   maxlim: 2149679   bits: 23/22
c ---[  58]---> Adder-cost: 778   maxlim: 2149679   bits: 23/22
c ---[  57]---> Adder-cost: 778   maxlim: 2149679   bits: 23/22
c ---[  56]---> Adder-cost: 778   maxlim: 2149679   bits: 23/22
c ---[  55]---> Adder-cost: 778   maxlim: 2149679   bits: 23/22
c ---[  54]---> Adder-cost: 778   maxlim: 2149679   bits: 23/22
c ---[  53]---> Adder-cost: 778   maxlim: 2149679   bits: 23/22
c ---[  52]---> Adder-cost: 778   maxlim: 2149679   bits: 23/22
c ---[  51]---> Adder-cost: 778   maxlim: 2149679   bits: 23/22
c ---[  50]---> Adder-cost: 1116   maxlim: 5263019   bits: 24/23
c ---[  49]---> Adder-cost: 1116   maxlim: 5264299   bits: 24/23
c ---[  48]---> Adder-cost: 1116   maxlim: 5265579   bits: 24/23
c ---[  47]---> Adder-cost: 1116   maxlim: 5266859   bits: 24/23
c ---[  46]---> Adder-cost: 1116   maxlim: 5269419   bits: 24/23
c ---[  45]---> Adder-cost: 1116   maxlim: 5265579   bits: 24/23
c ---[  44]---> Adder-cost: 1116   maxlim: 5266859   bits: 24/23
c ---[  43]---> Adder-cost: 1116   maxlim: 5264299   bits: 24/23
c ---[  42]---> Adder-cost: 1116   maxlim: 5263659   bits: 24/23
c ---[  41]---> Adder-cost: 778   maxlim: 2149679   bits: 23/22
c ---[  40]---> Adder-cost: 778   maxlim: 2149679   bits: 23/22
c ---[  39]---> Adder-cost: 778   maxlim: 2149679   bits: 23/22
c ---[  38]---> Adder-cost: 778   maxlim: 2149679   bits: 23/22
c ---[  37]---> Adder-cost: 778   maxlim: 2149679   bits: 23/22
c ---[  36]---> Adder-cost: 778   maxlim: 2149679   bits: 23/22
c ---[  35]---> Adder-cost: 778   maxlim: 2149679   bits: 23/22
c ---[  34]---> Adder-cost: 778   maxlim: 2149679   bits: 23/22
c ---[  33]---> Adder-cost: 778   maxlim: 2149679   bits: 23/22
c ---[  32]---> Adder-cost: 778   maxlim: 2149679   bits: 23/22
c ---[  31]---> Adder-cost: 778   maxlim: 2149679   bits: 23/22
c ---[  30]---> Adder-cost: 778   maxlim: 2149679   bits: 23/22
c ---[  29]---> Adder-cost: 778   maxlim: 2149679   bits: 23/22
c ---[  28]---> Adder-cost: 778   maxlim: 2149679   bits: 23/22
c ---[  27]---> Adder-cost: 778   maxlim: 2149679   bits: 23/22
c ---[  26]---> Adder-cost: 778   maxlim: 2149679   bits: 23/22
c ---[  25]---> Adder-cost: 778   maxlim: 2149679   bits: 23/22
c ---[  24]---> Adder-cost: 778   maxlim: 2149679   bits: 23/22
c ---[  23]---> Adder-cost: 1034   maxlim: 4219544   bits: 24/23
c ---[  21]---> Adder-cost: 1034   maxlim: 4220184   bits: 24/23
c ---[  20]---> Adder-cost: 1034   maxlim: 4220184   bits: 24/23
c ---[  19]---> Adder-cost: 1034   maxlim: 4220184   bits: 24/23
c ---[  18]---> Adder-cost: 1034   maxlim: 4220824   bits: 24/23
c ---[  17]---> Adder-cost: 1034   maxlim: 4220184   bits: 24/23
c ---[  16]---> Adder-cost: 1034   maxlim: 4220184   bits: 24/23
c ---[  15]---> Adder-cost: 1034   maxlim: 4219544   bits: 24/23
c ---[  14]---> Adder-cost: 1034   maxlim: 4219544   bits: 24/23
c ---[  13]---> Adder-cost: 333   maxlim: 1279   bits: 12/11
c ---[  12]---> Adder-cost: 401   maxlim: 1279   bits: 12/11
c ---[  11]---> Sorter-cost:  231     Base: 2 2 2 2 2 2 2
c ---[  10]---> Sorter-cost:  343     Base: 2 2 2 2 2 2 2
c ---[   9]---> Sorter-cost:  341     Base: 2 2 2 2 2 2 2 2
c ---[   8]---> Sorter-cost:  343     Base: 2 2 2 2 2 2 2
c ---[   7]---> Sorter-cost:  295     Base: 2 2 2 2 2 2 2 2
c ---[   6]---> Sorter-cost:  231     Base: 2 2 2 2 2 2 2
c ---[   5]---> Sorter-cost:  341     Base: 2 2 2 2 2 2 2 2
c ---[   4]---> Sorter-cost: 1036     Base: 2 2 2 2 2 2 2
c ---[   3]---> BDD-cost:   60
c ---[   2]---> Adder-cost: 186   maxlim: 639   bits: 11/10
c ---[   1]---> Adder-cost: 345   maxlim: 639   bits: 11/10
c ---[   0]---> Adder-cost: 287   maxlim: 639   bits: 11/10
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 | 3979974 10639655 | 1326658       0        0     nan |  0.000 % |
c |       100 | 3979974 10639655 | 1459323     100      304     3.0 |  2.192 % |
c |       250 | 3979916 10639526 | 1605256     245      876     3.6 |  2.193 % |
c |       475 | 3979908 10639508 | 1765781     469     1700     3.6 |  2.193 % |
c |       812 | 3979908 10639508 | 1942359     806     3183     3.9 |  2.193 % |
c |      1318 | 3979809 10639288 | 2136595    1309     5662     4.3 |  2.195 % |
c |      2077 | 3979809 10639288 | 2350255    2068    10507     5.1 |  2.195 % |
c |      3216 | 3979748 10639152 | 2585281    3206    16093     5.0 |  2.197 % |
c |      4924 | 3979748 10639152 | 2843809    4914    27429     5.6 |  2.197 % |
c |      7486 | 3979748 10639152 | 3128190    7476    49041     6.6 |  2.197 % |
c |     11331 | 3979649 10638932 | 3441009   11318    76414     6.8 |  2.199 % |
c |     17097 | 3979496 10638591 | 3785110   17079   132897     7.8 |  2.202 % |
c |     25746 | 3979100 10637703 | 4163621   25708   196833     7.7 |  2.212 % |
c |     38720 | 3978456 10636270 | 4579983   38662   296078     7.7 |  2.226 % |
c |     58181 | 3976749 10632455 | 5037981   58057   509372     8.8 |  2.265 % |
c |     87373 | 3975672 10630042 | 5541779   87210  1357565    15.6 |  2.289 % |
c |    131164 | 3974036 10626374 | 6095957  130931  2723843    20.8 |  2.327 % |
c |    196850 | 3971933 10621671 | 6705553  196512  4536749    23.1 |  2.375 % |
#### 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.55 0.88 0.93 2/54 22170
Raw data (stat): 22170 (runsolver) R 22169 25285 25284 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 484581760 1052672 99 4294967295 134512640 135381576 3221224448 3221219692 135158418 0 2147483391 7 90112 0 0 0 17 0 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0001 s]
Raw data (loadavg): 0.62 0.88 0.93 2/54 22170
Raw data (stat): 22170 (minisat+) R 22169 25285 25284 0 -1 0 17395 0 0 0 955 44 0 0 25 0 1 0 484581760 73904128 14448 4294967295 134512640 134672761 3221224544 3221221280 134522987 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18043 14448 603 41 0 18002 0
vsize: 72172
[startup+20.001 s]
Raw data (loadavg): 0.68 0.88 0.93 2/54 22170
Raw data (stat): 22170 (minisat+) R 22169 25285 25284 0 -1 0 41368 0 0 0 1900 99 0 0 25 0 1 0 484581760 188067840 38421 4294967295 134512640 134672761 3221224544 3221221232 134525037 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 45915 38421 603 41 0 45874 0
vsize: 183660
[startup+30.0008 s]
Raw data (loadavg): 0.73 0.89 0.93 2/54 22170
Raw data (stat): 22170 (minisat+) R 22169 25285 25284 0 -1 0 91488 0 0 0 2782 217 0 0 25 0 1 0 484581760 449228800 88541 4294967295 134512640 134672761 3221224544 3221221504 134553610 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 109675 88541 603 41 0 109634 0
vsize: 438700
[startup+40.0005 s]
Raw data (loadavg): 0.77 0.89 0.93 2/54 22170
Raw data (stat): 22170 (minisat+) R 22169 25285 25284 0 -1 0 96138 0 0 0 3769 230 0 0 25 0 1 0 484581760 463888384 93191 4294967295 134512640 134672761 3221224544 3221223716 134556651 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 113254 93191 603 41 0 113213 0
vsize: 453016
[startup+50.0013 s]
Raw data (loadavg): 0.80 0.89 0.93 2/54 22170
Raw data (stat): 22170 (minisat+) R 22169 25285 25284 0 -1 0 96362 0 0 0 4769 230 0 0 25 0 1 0 484581760 464711680 93415 4294967295 134512640 134672761 3221224544 3221223712 134560839 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 113455 93415 603 41 0 113414 0
vsize: 453820
[startup+60.0011 s]
Raw data (loadavg): 0.83 0.90 0.93 2/54 22170
Raw data (stat): 22170 (minisat+) R 22169 25285 25284 0 -1 0 96543 0 0 0 5769 230 0 0 25 0 1 0 484581760 465252352 93596 4294967295 134512640 134672761 3221224544 3221223680 134560588 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 113587 93596 603 41 0 113546 0
vsize: 454348
[startup+70.001 s]
Raw data (loadavg): 0.86 0.90 0.93 2/54 22170
Raw data (stat): 22170 (minisat+) R 22169 25285 25284 0 -1 0 96695 0 0 0 6769 231 0 0 25 0 1 0 484581760 465793024 93748 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 113719 93748 603 41 0 113678 0
vsize: 454876
[startup+80.0009 s]
Raw data (loadavg): 0.88 0.90 0.93 2/54 22170
Raw data (stat): 22170 (minisat+) R 22169 25285 25284 0 -1 0 96740 0 0 0 7769 231 0 0 25 0 1 0 484581760 465928192 93793 4294967295 134512640 134672761 3221224544 3221223744 134557820 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 113752 93793 603 41 0 113711 0
vsize: 455008
[startup+90.0007 s]
Raw data (loadavg): 0.90 0.90 0.93 2/54 22170
Raw data (stat): 22170 (minisat+) R 22169 25285 25284 0 -1 0 96806 0 0 0 8769 231 0 0 25 0 1 0 484581760 466198528 93859 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 113818 93859 603 41 0 113777 0
vsize: 455272
[startup+100.001 s]
Raw data (loadavg): 0.99 0.92 0.94 2/54 22170
Raw data (stat): 22170 (minisat+) R 22169 25285 25284 0 -1 0 96843 0 0 0 9769 231 0 0 25 0 1 0 484581760 466423808 93896 4294967295 134512640 134672761 3221224544 3221223712 134560852 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 113873 93896 603 41 0 113832 0
vsize: 455492
[startup+110.001 s]
Raw data (loadavg): 0.99 0.93 0.94 2/54 22170
Raw data (stat): 22170 (minisat+) R 22169 25285 25284 0 -1 0 96926 0 0 0 10768 232 0 0 25 0 1 0 484581760 466694144 93979 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 113939 93979 603 41 0 113898 0
vsize: 455756
[startup+120.002 s]
Raw data (loadavg): 0.99 0.93 0.94 2/54 22170
Raw data (stat): 22170 (minisat+) R 22169 25285 25284 0 -1 0 96988 0 0 0 11768 232 0 0 25 0 1 0 484581760 466829312 94041 4294967295 134512640 134672761 3221224544 3221223716 134556606 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 113972 94041 603 41 0 113931 0
vsize: 455888
[startup+130.001 s]
Raw data (loadavg): 0.99 0.93 0.94 2/54 22170
Raw data (stat): 22170 (minisat+) R 22169 25285 25284 0 -1 0 97035 0 0 0 12768 232 0 0 25 0 1 0 484581760 467099648 94088 4294967295 134512640 134672761 3221224544 3221223712 134564467 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 114038 94088 603 41 0 113997 0
vsize: 456152
[startup+140.001 s]
Raw data (loadavg): 0.99 0.93 0.94 2/54 22170
Raw data (stat): 22170 (minisat+) R 22169 25285 25284 0 -1 0 97057 0 0 0 13768 232 0 0 25 0 1 0 484581760 467234816 94110 4294967295 134512640 134672761 3221224544 3221223668 134566037 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 114071 94110 603 41 0 114030 0
vsize: 456284
[startup+150.01 s]
Raw data (loadavg): 0.99 0.93 0.94 2/54 22170
Raw data (stat): 22170 (minisat+) R 22169 25285 25284 0 -1 0 97091 0 0 0 14769 233 0 0 25 0 1 0 484581760 467369984 94144 4294967295 134512640 134672761 3221224544 3221223744 134557809 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 114104 94144 603 41 0 114063 0
vsize: 456416
[startup+160.01 s]
Raw data (loadavg): 0.99 0.94 0.94 2/54 22170
Raw data (stat): 22170 (minisat+) R 22169 25285 25284 0 -1 0 97129 0 0 0 15769 233 0 0 25 0 1 0 484581760 467505152 94182 4294967295 134512640 134672761 3221224544 3221223712 134560956 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 114137 94182 603 41 0 114096 0
vsize: 456548
[startup+170.01 s]
Raw data (loadavg): 0.99 0.94 0.94 2/54 22170
Raw data (stat): 22170 (minisat+) R 22169 25285 25284 0 -1 0 97203 0 0 0 16768 233 0 0 25 0 1 0 484581760 467640320 94256 4294967295 134512640 134672761 3221224544 3221223712 134560808 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 114170 94256 603 41 0 114129 0
vsize: 456680
[startup+180.01 s]
Raw data (loadavg): 0.99 0.94 0.94 2/54 22170
Raw data (stat): 22170 (minisat+) R 22169 25285 25284 0 -1 0 97247 0 0 0 17768 233 0 0 25 0 1 0 484581760 467910656 94300 4294967295 134512640 134672761 3221224544 3221223744 134557895 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 114236 94300 603 41 0 114195 0
vsize: 456944
[startup+190.009 s]
Raw data (loadavg): 0.99 0.94 0.94 2/54 22170
Raw data (stat): 22170 (minisat+) R 22169 25285 25284 0 -1 0 97278 0 0 0 18768 234 0 0 25 0 1 0 484581760 467910656 94331 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 114236 94331 603 41 0 114195 0
vsize: 456944
[startup+200.009 s]
Raw data (loadavg): 0.99 0.94 0.94 2/54 22170
Raw data (stat): 22170 (minisat+) R 22169 25285 25284 0 -1 0 97415 0 0 0 19768 234 0 0 25 0 1 0 484581760 468578304 94468 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 114399 94468 603 41 0 114358 0
vsize: 457596
[startup+210.009 s]
Raw data (loadavg): 0.99 0.94 0.94 2/54 22170
Raw data (stat): 22170 (minisat+) R 22169 25285 25284 0 -1 0 97416 0 0 0 20768 234 0 0 25 0 1 0 484581760 468578304 94469 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 114399 94469 603 41 0 114358 0
vsize: 457596
[startup+220.01 s]
Raw data (loadavg): 0.99 0.94 0.94 2/54 22170
Raw data (stat): 22170 (minisat+) R 22169 25285 25284 0 -1 0 97436 0 0 0 21768 234 0 0 25 0 1 0 484581760 468713472 94489 4294967295 134512640 134672761 3221224544 3221223744 134557911 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 114432 94489 603 41 0 114391 0
vsize: 457728
[startup+230.01 s]
Raw data (loadavg): 0.99 0.95 0.94 2/54 22170
Raw data (stat): 22170 (minisat+) R 22169 25285 25284 0 -1 0 97453 0 0 0 22768 234 0 0 25 0 1 0 484581760 468713472 94506 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 114432 94506 603 41 0 114391 0
vsize: 457728
[startup+240.01 s]
Raw data (loadavg): 0.99 0.95 0.94 2/54 22170
Raw data (stat): 22170 (minisat+) R 22169 25285 25284 0 -1 0 97492 0 0 0 23768 234 0 0 25 0 1 0 484581760 468848640 94545 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 114465 94545 603 41 0 114424 0
vsize: 457860
[startup+250.01 s]
Raw data (loadavg): 0.99 0.95 0.94 2/54 22170
Raw data (stat): 22170 (minisat+) R 22169 25285 25284 0 -1 0 97515 0 0 0 24768 234 0 0 25 0 1 0 484581760 468983808 94568 4294967295 134512640 134672761 3221224544 3221223748 134561964 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 114498 94568 603 41 0 114457 0
vsize: 457992
[startup+260.01 s]
Raw data (loadavg): 0.99 0.95 0.94 2/54 22170
Raw data (stat): 22170 (minisat+) R 22169 25285 25284 0 -1 0 97540 0 0 0 25769 234 0 0 25 0 1 0 484581760 468983808 94593 4294967295 134512640 134672761 3221224544 3221223744 134557830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 114498 94593 603 41 0 114457 0
vsize: 457992
[startup+270.01 s]
Raw data (loadavg): 0.99 0.95 0.94 2/54 22170
Raw data (stat): 22170 (minisat+) R 22169 25285 25284 0 -1 0 97582 0 0 0 26769 235 0 0 25 0 1 0 484581760 469250048 94635 4294967295 134512640 134672761 3221224544 3221223668 134566122 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 114563 94635 603 41 0 114522 0
vsize: 458252
[startup+280.01 s]
Raw data (loadavg): 0.99 0.95 0.94 2/54 22170
Raw data (stat): 22170 (minisat+) R 22169 25285 25284 0 -1 0 97598 0 0 0 27769 235 0 0 25 0 1 0 484581760 469250048 94651 4294967295 134512640 134672761 3221224544 3221223680 134560588 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 114563 94651 603 41 0 114522 0
vsize: 458252
[startup+290.01 s]
Raw data (loadavg): 0.99 0.95 0.94 2/54 22170
Raw data (stat): 22170 (minisat+) R 22169 25285 25284 0 -1 0 97635 0 0 0 28769 235 0 0 25 0 1 0 484581760 469385216 94688 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 114596 94688 603 41 0 114555 0
vsize: 458384
[startup+300.01 s]
Raw data (loadavg): 0.99 0.95 0.94 2/54 22170
Raw data (stat): 22170 (minisat+) R 22169 25285 25284 0 -1 0 97749 0 0 0 29769 235 0 0 25 0 1 0 484581760 469790720 94802 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 114695 94802 603 41 0 114654 0
vsize: 458780
[startup+310.01 s]
Raw data (loadavg): 0.99 0.95 0.94 2/54 22170
Raw data (stat): 22170 (minisat+) R 22169 25285 25284 0 -1 0 97765 0 0 0 30769 235 0 0 25 0 1 0 484581760 469925888 94818 4294967295 134512640 134672761 3221224544 3221223680 134560588 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 114728 94818 603 41 0 114687 0
vsize: 458912
[startup+320.01 s]
Raw data (loadavg): 0.99 0.95 0.94 2/54 22170
Raw data (stat): 22170 (minisat+) R 22169 25285 25284 0 -1 0 97794 0 0 0 31769 235 0 0 25 0 1 0 484581760 469925888 94847 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 114728 94847 603 41 0 114687 0
vsize: 458912
[startup+330.01 s]
Raw data (loadavg): 0.99 0.95 0.94 2/54 22170
Raw data (stat): 22170 (minisat+) R 22169 25285 25284 0 -1 0 97823 0 0 0 32769 235 0 0 25 0 1 0 484581760 470061056 94876 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 114761 94876 603 41 0 114720 0
vsize: 459044
[startup+340.01 s]
Raw data (loadavg): 0.99 0.96 0.94 2/54 22170
Raw data (stat): 22170 (minisat+) R 22169 25285 25284 0 -1 0 97869 0 0 0 33769 235 0 0 25 0 1 0 484581760 470331392 94922 4294967295 134512640 134672761 3221224544 3221223716 134556641 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 114827 94922 603 41 0 114786 0
vsize: 459308
[startup+350.01 s]
Raw data (loadavg): 0.99 0.96 0.94 2/54 22170
Raw data (stat): 22170 (minisat+) R 22169 25285 25284 0 -1 0 97905 0 0 0 34769 236 0 0 25 0 1 0 484581760 470466560 94958 4294967295 134512640 134672761 3221224544 3221223748 134561964 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 114860 94958 603 41 0 114819 0
vsize: 459440
[startup+360.01 s]
Raw data (loadavg): 0.99 0.96 0.94 2/54 22170
Raw data (stat): 22170 (minisat+) R 22169 25285 25284 0 -1 0 97933 0 0 0 35769 236 0 0 25 0 1 0 484581760 470466560 94986 4294967295 134512640 134672761 3221224544 3221223744 134561967 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 114860 94986 603 41 0 114819 0
vsize: 459440
[startup+370.01 s]
Raw data (loadavg): 0.99 0.96 0.94 2/54 22170
Raw data (stat): 22170 (minisat+) R 22169 25285 25284 0 -1 0 97961 0 0 0 36769 236 0 0 25 0 1 0 484581760 470597632 95014 4294967295 134512640 134672761 3221224544 3221223712 134560948 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 114892 95014 603 41 0 114851 0
vsize: 459568
[startup+380.01 s]
Raw data (loadavg): 0.99 0.96 0.94 2/54 22170
Raw data (stat): 22170 (minisat+) R 22169 25285 25284 0 -1 0 98061 0 0 0 37769 236 0 0 25 0 1 0 484581760 471003136 95114 4294967295 134512640 134672761 3221224544 3221223692 134560552 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 114991 95114 603 41 0 114950 0
vsize: 459964
[startup+390.01 s]
Raw data (loadavg): 0.99 0.96 0.94 2/54 22170
Raw data (stat): 22170 (minisat+) R 22169 25285 25284 0 -1 0 98116 0 0 0 38769 236 0 0 25 0 1 0 484581760 471273472 95169 4294967295 134512640 134672761 3221224544 3221223712 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 115057 95169 603 41 0 115016 0
vsize: 460228
[startup+400.011 s]
Raw data (loadavg): 0.99 0.96 0.94 2/54 22170
Raw data (stat): 22170 (minisat+) R 22169 25285 25284 0 -1 0 98147 0 0 0 39769 236 0 0 25 0 1 0 484581760 471408640 95200 4294967295 134512640 134672761 3221224544 3221223716 134556685 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 115090 95200 603 41 0 115049 0
vsize: 460360
[startup+410.011 s]
Raw data (loadavg): 0.99 0.96 0.94 2/54 22170
Raw data (stat): 22170 (minisat+) R 22169 25285 25284 0 -1 0 98176 0 0 0 40769 236 0 0 25 0 1 0 484581760 471408640 95229 4294967295 134512640 134672761 3221224544 3221223716 134556618 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 115090 95229 603 41 0 115049 0
vsize: 460360
[startup+420.012 s]
Raw data (loadavg): 0.99 0.96 0.94 2/54 22170
Raw data (stat): 22170 (minisat+) R 22169 25285 25284 0 -1 0 98197 0 0 0 41769 237 0 0 25 0 1 0 484581760 471543808 95250 4294967295 134512640 134672761 3221224544 3221223716 134556651 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 115123 95250 603 41 0 115082 0
vsize: 460492
[startup+430.011 s]
Raw data (loadavg): 0.99 0.96 0.94 2/54 22170
Raw data (stat): 22170 (minisat+) R 22169 25285 25284 0 -1 0 98230 0 0 0 42769 237 0 0 25 0 1 0 484581760 471678976 95283 4294967295 134512640 134672761 3221224544 3221223668 134566071 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 115156 95283 603 41 0 115115 0
vsize: 460624
[startup+440.011 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 22170
Raw data (stat): 22170 (minisat+) R 22169 25285 25284 0 -1 0 98244 0 0 0 43770 237 0 0 25 0 1 0 484581760 471678976 95297 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 115156 95297 603 41 0 115115 0
vsize: 460624
[startup+450.011 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 22170
Raw data (stat): 22170 (minisat+) R 22169 25285 25284 0 -1 0 98441 0 0 0 44769 237 0 0 25 0 1 0 484581760 472752128 95494 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 115418 95494 603 41 0 115377 0
vsize: 461672
[startup+460.011 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 22170
Raw data (stat): 22170 (minisat+) R 22169 25285 25284 0 -1 0 98538 0 0 0 45769 238 0 0 25 0 1 0 484581760 473157632 95591 4294967295 134512640 134672761 3221224544 3221223712 134561188 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 115517 95591 603 41 0 115476 0
vsize: 462068
[startup+470.02 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 22170
Raw data (stat): 22170 (minisat+) R 22169 25285 25284 0 -1 0 99087 0 0 0 46768 239 0 0 25 0 1 0 484581760 475312128 96140 4294967295 134512640 134672761 3221224544 3221223712 134560828 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 116043 96140 603 41 0 116002 0
vsize: 464172
[startup+480.021 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 22170
Raw data (stat): 22170 (minisat+) R 22169 25285 25284 0 -1 0 99352 0 0 0 47768 240 0 0 25 0 1 0 484581760 476393472 96405 4294967295 134512640 134672761 3221224544 3221223748 134561964 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 116307 96405 603 41 0 116266 0
vsize: 465228
[startup+490.02 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 22170
Raw data (stat): 22170 (minisat+) R 22169 25285 25284 0 -1 0 99449 0 0 0 48768 240 0 0 25 0 1 0 484581760 476794880 96502 4294967295 134512640 134672761 3221224544 3221223716 134556651 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 116405 96502 603 41 0 116364 0
vsize: 465620
[startup+500.021 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 22170
Raw data (stat): 22170 (minisat+) R 22169 25285 25284 0 -1 0 99476 0 0 0 49768 240 0 0 25 0 1 0 484581760 476930048 96529 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 116438 96529 603 41 0 116397 0
vsize: 465752
[startup+510.021 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 22170
Raw data (stat): 22170 (minisat+) R 22169 25285 25284 0 -1 0 99689 0 0 0 50768 240 0 0 25 0 1 0 484581760 477736960 96742 4294967295 134512640 134672761 3221224544 3221223712 134560999 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 116635 96742 603 41 0 116594 0
vsize: 466540
[startup+520.022 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 22170
Raw data (stat): 22170 (minisat+) R 22169 25285 25284 0 -1 0 100239 0 0 0 51766 243 0 0 25 0 1 0 484581760 480014336 97292 4294967295 134512640 134672761 3221224544 3221223744 134557842 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 117191 97292 603 41 0 117150 0
vsize: 468764
[startup+530.022 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 22170
Raw data (stat): 22170 (minisat+) R 22169 25285 25284 0 -1 0 100538 0 0 0 52765 244 0 0 25 0 1 0 484581760 481218560 97591 4294967295 134512640 134672761 3221224544 3221223668 134566071 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 117485 97591 603 41 0 117444 0
vsize: 469940
[startup+540.022 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 22170
Raw data (stat): 22170 (minisat+) R 22169 25285 25284 0 -1 0 100589 0 0 0 53765 244 0 0 25 0 1 0 484581760 481353728 97642 4294967295 134512640 134672761 3221224544 3221223716 134556643 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 117518 97642 603 41 0 117477 0
vsize: 470072
[startup+550.021 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 22170
Raw data (stat): 22170 (minisat+) R 22169 25285 25284 0 -1 0 100647 0 0 0 54765 244 0 0 25 0 1 0 484581760 481624064 97700 4294967295 134512640 134672761 3221224544 3221223680 134560677 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 117584 97700 603 41 0 117543 0
vsize: 470336
[startup+560.021 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 22170
Raw data (stat): 22170 (minisat+) R 22169 25285 25284 0 -1 0 100668 0 0 0 55765 244 0 0 25 0 1 0 484581760 481759232 97721 4294967295 134512640 134672761 3221224544 3221223544 1075350517 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 117617 97721 603 41 0 117576 0
vsize: 470468
[startup+570.022 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 22170
Raw data (stat): 22170 (minisat+) R 22169 25285 25284 0 -1 0 100699 0 0 0 56765 245 0 0 25 0 1 0 484581760 481894400 97752 4294967295 134512640 134672761 3221224544 3221223668 134566062 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 117650 97752 603 41 0 117609 0
vsize: 470600
[startup+580.022 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 22170
Raw data (stat): 22170 (minisat+) R 22169 25285 25284 0 -1 0 100720 0 0 0 57765 245 0 0 25 0 1 0 484581760 481894400 97773 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 117650 97773 603 41 0 117609 0
vsize: 470600
[startup+590.023 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 22170
Raw data (stat): 22170 (minisat+) R 22169 25285 25284 0 -1 0 100743 0 0 0 58765 245 0 0 25 0 1 0 484581760 482029568 97796 4294967295 134512640 134672761 3221224544 3221223744 134557852 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 117683 97796 603 41 0 117642 0
vsize: 470732
[startup+600.023 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 22170
Raw data (stat): 22170 (minisat+) R 22169 25285 25284 0 -1 0 100780 0 0 0 59765 245 0 0 25 0 1 0 484581760 482164736 97833 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 117716 97833 603 41 0 117675 0
vsize: 470864
[startup+610.023 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 22170
Raw data (stat): 22170 (minisat+) R 22169 25285 25284 0 -1 0 100806 0 0 0 60765 245 0 0 25 0 1 0 484581760 482299904 97859 4294967295 134512640 134672761 3221224544 3221223716 134556651 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 117749 97859 603 41 0 117708 0
vsize: 470996
[startup+620.023 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 22170
Raw data (stat): 22170 (minisat+) R 22169 25285 25284 0 -1 0 101214 0 0 0 61764 246 0 0 25 0 1 0 484581760 484438016 98267 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 118271 98267 603 41 0 118230 0
vsize: 473084
[startup+630.022 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 22170
Raw data (stat): 22170 (minisat+) R 22169 25285 25284 0 -1 0 101251 0 0 0 62763 246 0 0 25 0 1 0 484581760 484573184 98304 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 118304 98304 603 41 0 118263 0
vsize: 473216
[startup+640.022 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 22170
Raw data (stat): 22170 (minisat+) R 22169 25285 25284 0 -1 0 101288 0 0 0 63763 246 0 0 25 0 1 0 484581760 484708352 98341 4294967295 134512640 134672761 3221224544 3221223680 134560688 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 118337 98341 603 41 0 118296 0
vsize: 473348
[startup+650.022 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 22170
Raw data (stat): 22170 (minisat+) R 22169 25285 25284 0 -1 0 101407 0 0 0 64762 246 0 0 25 0 1 0 484581760 485113856 98460 4294967295 134512640 134672761 3221224544 3221223744 134557809 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 118436 98460 603 41 0 118395 0
vsize: 473744
[startup+660.022 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 22170
Raw data (stat): 22170 (minisat+) R 22169 25285 25284 0 -1 0 101432 0 0 0 65763 246 0 0 25 0 1 0 484581760 485244928 98485 4294967295 134512640 134672761 3221224544 3221223716 134556653 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 118468 98485 603 41 0 118427 0
vsize: 473872
[startup+670.022 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 22170
Raw data (stat): 22170 (minisat+) R 22169 25285 25284 0 -1 0 101459 0 0 0 66762 247 0 0 25 0 1 0 484581760 485380096 98512 4294967295 134512640 134672761 3221224544 3221223712 134561378 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 118501 98512 603 41 0 118460 0
vsize: 474004
[startup+680.021 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 22170
Raw data (stat): 22170 (minisat+) R 22169 25285 25284 0 -1 0 101490 0 0 0 67762 247 0 0 25 0 1 0 484581760 485515264 98543 4294967295 134512640 134672761 3221224544 3221223712 134560864 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 118534 98543 603 41 0 118493 0
vsize: 474136
[startup+690.022 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 22170
Raw data (stat): 22170 (minisat+) R 22169 25285 25284 0 -1 0 101881 0 0 0 68761 248 0 0 25 0 1 0 484581760 487124992 98934 4294967295 134512640 134672761 3221224544 3221223668 134566037 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 118927 98934 603 41 0 118886 0
vsize: 475708
[startup+700.022 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 22170
Raw data (stat): 22170 (minisat+) R 22169 25285 25284 0 -1 0 102034 0 0 0 69761 248 0 0 25 0 1 0 484581760 487661568 99087 4294967295 134512640 134672761 3221224544 3221223712 134560871 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 119058 99087 603 41 0 119017 0
vsize: 476232
[startup+710.022 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 22170
Raw data (stat): 22170 (minisat+) R 22169 25285 25284 0 -1 0 102475 0 0 0 70760 250 0 0 25 0 1 0 484581760 489422848 99528 4294967295 134512640 134672761 3221224544 3221223712 134560912 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 119488 99528 603 41 0 119447 0
vsize: 477952
[startup+720.023 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 22170
Raw data (stat): 22170 (minisat+) R 22169 25285 25284 0 -1 0 102840 0 0 0 71759 251 0 0 25 0 1 0 484581760 490917888 99893 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 119853 99893 603 41 0 119812 0
vsize: 479412
[startup+730.023 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 22170
Raw data (stat): 22170 (minisat+) R 22169 25285 25284 0 -1 0 103154 0 0 0 72758 252 0 0 25 0 1 0 484581760 492265472 100207 4294967295 134512640 134672761 3221224544 3221223728 134559161 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 120182 100207 603 41 0 120141 0
vsize: 480728
[startup+740.023 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 22170
Raw data (stat): 22170 (minisat+) R 22169 25285 25284 0 -1 0 103328 0 0 0 73758 252 0 0 25 0 1 0 484581760 492961792 100381 4294967295 134512640 134672761 3221224544 3221223716 134556643 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 120352 100381 603 41 0 120311 0
vsize: 481408
[startup+750.023 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 22170
Raw data (stat): 22170 (minisat+) R 22169 25285 25284 0 -1 0 103342 0 0 0 74758 252 0 0 25 0 1 0 484581760 492961792 100395 4294967295 134512640 134672761 3221224544 3221223716 134556667 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 120352 100395 603 41 0 120311 0
vsize: 481408
[startup+760.023 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 22170
Raw data (stat): 22170 (minisat+) R 22169 25285 25284 0 -1 0 103364 0 0 0 75758 252 0 0 25 0 1 0 484581760 493096960 100417 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 120385 100417 603 41 0 120344 0
vsize: 481540
[startup+770.023 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 22170
Raw data (stat): 22170 (minisat+) R 22169 25285 25284 0 -1 0 103388 0 0 0 76758 252 0 0 25 0 1 0 484581760 493232128 100441 4294967295 134512640 134672761 3221224544 3221223712 134560839 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 120418 100441 603 41 0 120377 0
vsize: 481672
[startup+780.024 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 22170
Raw data (stat): 22170 (minisat+) R 22169 25285 25284 0 -1 0 103409 0 0 0 77759 252 0 0 25 0 1 0 484581760 493232128 100462 4294967295 134512640 134672761 3221224544 3221223692 134560552 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 120418 100462 603 41 0 120377 0
vsize: 481672
[startup+790.024 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 22170
Raw data (stat): 22170 (minisat+) R 22169 25285 25284 0 -1 0 103416 0 0 0 78759 252 0 0 25 0 1 0 484581760 493232128 100469 4294967295 134512640 134672761 3221224544 3221223716 134556643 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 120418 100469 603 41 0 120377 0
vsize: 481672
[startup+800.024 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 22170
Raw data (stat): 22170 (minisat+) R 22169 25285 25284 0 -1 0 103436 0 0 0 79759 252 0 0 25 0 1 0 484581760 493367296 100489 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 120451 100489 603 41 0 120410 0
vsize: 481804
[startup+810.024 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 22170
Raw data (stat): 22170 (minisat+) R 22169 25285 25284 0 -1 0 103444 0 0 0 80759 252 0 0 25 0 1 0 484581760 493367296 100497 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 120451 100497 603 41 0 120410 0
vsize: 481804
[startup+820.024 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 22170
Raw data (stat): 22170 (minisat+) R 22169 25285 25284 0 -1 0 103522 0 0 0 81759 253 0 0 25 0 1 0 484581760 493637632 100575 4294967295 134512640 134672761 3221224544 3221223692 134560552 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 120517 100575 603 41 0 120476 0
vsize: 482068
[startup+830.025 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 22170
Raw data (stat): 22170 (minisat+) R 22169 25285 25284 0 -1 0 103544 0 0 0 82759 253 0 0 25 0 1 0 484581760 493772800 100597 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 120550 100597 603 41 0 120509 0
vsize: 482200
[startup+840.024 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 22170
Raw data (stat): 22170 (minisat+) R 22169 25285 25284 0 -1 0 103581 0 0 0 83759 253 0 0 25 0 1 0 484581760 493907968 100634 4294967295 134512640 134672761 3221224544 3221223680 134560667 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 120583 100634 603 41 0 120542 0
vsize: 482332
[startup+850.025 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 22170
Raw data (stat): 22170 (minisat+) R 22169 25285 25284 0 -1 0 103610 0 0 0 84760 253 0 0 25 0 1 0 484581760 494043136 100663 4294967295 134512640 134672761 3221224544 3221223680 134560588 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 120616 100663 603 41 0 120575 0
vsize: 482464
[startup+860.025 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 22170
Raw data (stat): 22170 (minisat+) R 22169 25285 25284 0 -1 0 103671 0 0 0 85759 253 0 0 25 0 1 0 484581760 494178304 100724 4294967295 134512640 134672761 3221224544 3221223744 134557842 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 120649 100724 603 41 0 120608 0
vsize: 482596
[startup+870.025 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 22170
Raw data (stat): 22170 (minisat+) R 22169 25285 25284 0 -1 0 103716 0 0 0 86759 253 0 0 25 0 1 0 484581760 494313472 100769 4294967295 134512640 134672761 3221224544 3221223716 134556682 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 120682 100769 603 41 0 120641 0
vsize: 482728
[startup+880.024 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 22170
Raw data (stat): 22170 (minisat+) R 22169 25285 25284 0 -1 0 103739 0 0 0 87759 253 0 0 25 0 1 0 484581760 494448640 100792 4294967295 134512640 134672761 3221224544 3221223668 134566037 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 120715 100792 603 41 0 120674 0
vsize: 482860
[startup+890.028 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 22170
Raw data (stat): 22170 (minisat+) R 22169 25285 25284 0 -1 0 103777 0 0 0 88760 253 0 0 25 0 1 0 484581760 494583808 100830 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 120748 100830 603 41 0 120707 0
vsize: 482992
[startup+900.028 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 22170
Raw data (stat): 22170 (minisat+) R 22169 25285 25284 0 -1 0 103790 0 0 0 89760 253 0 0 25 0 1 0 484581760 494583808 100843 4294967295 134512640 134672761 3221224544 3221223668 134566043 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 120748 100843 603 41 0 120707 0
vsize: 482992
[startup+910.028 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 22170
Raw data (stat): 22170 (minisat+) R 22169 25285 25284 0 -1 0 103813 0 0 0 90760 253 0 0 25 0 1 0 484581760 494747648 100866 4294967295 134512640 134672761 3221224544 3221223740 134556678 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 120788 100866 603 41 0 120747 0
vsize: 483152
[startup+920.029 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 22170
Raw data (stat): 22170 (minisat+) R 22169 25285 25284 0 -1 0 103833 0 0 0 91760 253 0 0 25 0 1 0 484581760 494747648 100886 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 120788 100886 603 41 0 120747 0
vsize: 483152
[startup+930.029 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 22170
Raw data (stat): 22170 (minisat+) R 22169 25285 25284 0 -1 0 103852 0 0 0 92760 253 0 0 25 0 1 0 484581760 494886912 100905 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 120822 100905 603 41 0 120781 0
vsize: 483288
[startup+940.029 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 22170
Raw data (stat): 22170 (minisat+) R 22169 25285 25284 0 -1 0 103863 0 0 0 93761 253 0 0 25 0 1 0 484581760 494886912 100916 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 120822 100916 603 41 0 120781 0
vsize: 483288
[startup+950.031 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 22170
Raw data (stat): 22170 (minisat+) R 22169 25285 25284 0 -1 0 103879 0 0 0 94760 254 0 0 25 0 1 0 484581760 495022080 100932 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 120855 100932 603 41 0 120814 0
vsize: 483420
[startup+960.036 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 22170
Raw data (stat): 22170 (minisat+) R 22169 25285 25284 0 -1 0 103892 0 0 0 95761 254 0 0 25 0 1 0 484581760 495022080 100945 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 120855 100945 603 41 0 120814 0
vsize: 483420
[startup+970.036 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 22170
Raw data (stat): 22170 (minisat+) R 22169 25285 25284 0 -1 0 103911 0 0 0 96760 254 0 0 25 0 1 0 484581760 495022080 100964 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 120855 100964 603 41 0 120814 0
vsize: 483420
[startup+980.036 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 22170
Raw data (stat): 22170 (minisat+) R 22169 25285 25284 0 -1 0 103946 0 0 0 97761 254 0 0 25 0 1 0 484581760 495157248 100999 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 120888 100999 603 41 0 120847 0
vsize: 483552
[startup+990.036 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 22170
Raw data (stat): 22170 (minisat+) R 22169 25285 25284 0 -1 0 103968 0 0 0 98761 254 0 0 25 0 1 0 484581760 495292416 101021 4294967295 134512640 134672761 3221224544 3221223712 134560855 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 120921 101021 603 41 0 120880 0
vsize: 483684
[startup+1000.04 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 22170
Raw data (stat): 22170 (minisat+) R 22169 25285 25284 0 -1 0 103980 0 0 0 99761 254 0 0 25 0 1 0 484581760 495292416 101033 4294967295 134512640 134672761 3221224544 3221223744 134557809 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 120921 101033 603 41 0 120880 0
vsize: 483684
[startup+1010.04 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 22170
Raw data (stat): 22170 (minisat+) R 22169 25285 25284 0 -1 0 103997 0 0 0 100761 254 0 0 25 0 1 0 484581760 495427584 101050 4294967295 134512640 134672761 3221224544 3221223744 134557842 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 120954 101050 603 41 0 120913 0
vsize: 483816
[startup+1020.04 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 22170
Raw data (stat): 22170 (minisat+) R 22169 25285 25284 0 -1 0 104011 0 0 0 101761 254 0 0 25 0 1 0 484581760 495427584 101064 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 120954 101064 603 41 0 120913 0
vsize: 483816
[startup+1030.04 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 22170
Raw data (stat): 22170 (minisat+) R 22169 25285 25284 0 -1 0 104022 0 0 0 102761 254 0 0 25 0 1 0 484581760 495562752 101075 4294967295 134512640 134672761 3221224544 3221223712 134560948 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 120987 101075 603 41 0 120946 0
vsize: 483948
[startup+1040.04 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 22170
Raw data (stat): 22170 (minisat+) R 22169 25285 25284 0 -1 0 104035 0 0 0 103762 254 0 0 25 0 1 0 484581760 495562752 101088 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 120987 101088 603 41 0 120946 0
vsize: 483948
[startup+1050.04 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 22170
Raw data (stat): 22170 (minisat+) R 22169 25285 25284 0 -1 0 104048 0 0 0 104762 254 0 0 25 0 1 0 484581760 495562752 101101 4294967295 134512640 134672761 3221224544 3221223744 134557895 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 120987 101101 603 41 0 120946 0
vsize: 483948
[startup+1060.04 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 22170
Raw data (stat): 22170 (minisat+) R 22169 25285 25284 0 -1 0 104066 0 0 0 105762 254 0 0 25 0 1 0 484581760 495697920 101119 4294967295 134512640 134672761 3221224544 3221223696 134565127 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 121020 101119 603 41 0 120979 0
vsize: 484080
[startup+1070.04 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 22170
Raw data (stat): 22170 (minisat+) R 22169 25285 25284 0 -1 0 104075 0 0 0 106762 254 0 0 25 0 1 0 484581760 495697920 101128 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 121020 101128 603 41 0 120979 0
vsize: 484080
[startup+1080.04 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 22170
Raw data (stat): 22170 (minisat+) R 22169 25285 25284 0 -1 0 104116 0 0 0 107762 254 0 0 25 0 1 0 484581760 495833088 101169 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 121053 101169 603 41 0 121012 0
vsize: 484212
[startup+1090.04 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 22170
Raw data (stat): 22170 (minisat+) R 22169 25285 25284 0 -1 0 104127 0 0 0 108762 254 0 0 25 0 1 0 484581760 495833088 101180 4294967295 134512640 134672761 3221224544 3221223716 134556653 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 121053 101180 603 41 0 121012 0
vsize: 484212
[startup+1100.04 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 22170
Raw data (stat): 22170 (minisat+) R 22169 25285 25284 0 -1 0 104132 0 0 0 109762 254 0 0 25 0 1 0 484581760 495833088 101185 4294967295 134512640 134672761 3221224544 3221223760 134561985 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 121053 101185 603 41 0 121012 0
vsize: 484212
[startup+1110.04 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 22170
Raw data (stat): 22170 (minisat+) R 22169 25285 25284 0 -1 0 104142 0 0 0 110762 254 0 0 25 0 1 0 484581760 495833088 101195 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 121053 101195 603 41 0 121012 0
vsize: 484212
[startup+1120.04 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 22170
Raw data (stat): 22170 (minisat+) R 22169 25285 25284 0 -1 0 104154 0 0 0 111762 255 0 0 25 0 1 0 484581760 495968256 101207 4294967295 134512640 134672761 3221224544 3221223748 134561964 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 121086 101207 603 41 0 121045 0
vsize: 484344
[startup+1130.04 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 22170
Raw data (stat): 22170 (minisat+) R 22169 25285 25284 0 -1 0 104164 0 0 0 112762 255 0 0 25 0 1 0 484581760 495968256 101217 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 121086 101217 603 41 0 121045 0
vsize: 484344
[startup+1140.04 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 22170
Raw data (stat): 22170 (minisat+) R 22169 25285 25284 0 -1 0 104212 0 0 0 113762 255 0 0 25 0 1 0 484581760 496103424 101265 4294967295 134512640 134672761 3221224544 3221223760 134561997 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 121119 101265 603 41 0 121078 0
vsize: 484476
[startup+1150.04 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 22170
Raw data (stat): 22170 (minisat+) R 22169 25285 25284 0 -1 0 104233 0 0 0 114762 255 0 0 25 0 1 0 484581760 496238592 101286 4294967295 134512640 134672761 3221224544 3221223712 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 121152 101286 603 41 0 121111 0
vsize: 484608
[startup+1160.04 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 22170
Raw data (stat): 22170 (minisat+) R 22169 25285 25284 0 -1 0 104250 0 0 0 115762 255 0 0 25 0 1 0 484581760 496238592 101303 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 121152 101303 603 41 0 121111 0
vsize: 484608
[startup+1170.04 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 22170
Raw data (stat): 22170 (minisat+) R 22169 25285 25284 0 -1 0 104263 0 0 0 116762 256 0 0 25 0 1 0 484581760 496238592 101316 4294967295 134512640 134672761 3221224544 3221223716 134556618 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 121152 101316 603 41 0 121111 0
vsize: 484608
[startup+1180.04 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 22170
Raw data (stat): 22170 (minisat+) R 22169 25285 25284 0 -1 0 104273 0 0 0 117762 256 0 0 25 0 1 0 484581760 496373760 101326 4294967295 134512640 134672761 3221224544 3221223716 134556688 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 121185 101326 603 41 0 121144 0
vsize: 484740
[startup+1190.04 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 22170
Raw data (stat): 22170 (minisat+) R 22169 25285 25284 0 -1 0 104289 0 0 0 118763 256 0 0 25 0 1 0 484581760 496373760 101342 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 121185 101342 603 41 0 121144 0
vsize: 484740
[startup+1200.04 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 22170
Raw data (stat): 22170 (minisat+) R 22169 25285 25284 0 -1 0 104296 0 0 0 119763 256 0 0 25 0 1 0 484581760 496373760 101349 4294967295 134512640 134672761 3221224544 3221223712 134560839 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 121185 101349 603 41 0 121144 0
vsize: 484740
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.25 s]
Raw data (loadavg): 0.99 0.97 0.94 1/54 22170
Raw data (stat): 22170 (minisat+) Z 22169 25285 25284 0 -1 12 104298 0 0 0 119763 276 0 0 25 0 1 0 484581760 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.24
CPU time (s): 1200.4
CPU user time (s): 1197.63
CPU system time (s): 2.76558
CPU usage (%): 100.013
Max. virtual memory (Kb): 484740
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####