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 19604 

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

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

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        645292 kB
Buffers:         21052 kB
Cached:         342136 kB
SwapCached:        408 kB
Active:          63200 kB
Inactive:       302564 kB
HighTotal:      131008 kB
HighFree:         8064 kB
LowTotal:       903652 kB
LowFree:        637228 kB
SwapTotal:     2097892 kB
SwapFree:      2097056 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           5856 kB
Slab:            18004 kB
Committed_AS:    63820 kB
PageTables:        328 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-21 19:44:33 (client local time) WITH STATUS 0 IN 1200.37 SECONDS
stats: 16333 7 1200.37 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 | 3723988  9911362 | 1241329       0        0     nan |  0.000 % |
c |       100 | 3723988  9911362 | 1365461     100      304     3.0 |  2.192 % |
c |       251 | 3723955  9911289 | 1502008     249      769     3.1 |  2.192 % |
c |       476 | 3723942  9911261 | 1652208     473     1592     3.4 |  2.193 % |
c |       813 | 3723942  9911261 | 1817429     810     3151     3.9 |  2.193 % |
c |      1319 | 3723942  9911261 | 1999172    1316     5714     4.3 |  2.193 % |
c |      2079 | 3723942  9911261 | 2199090    2076    10533     5.1 |  2.193 % |
c |      3218 | 3723780  9910901 | 2418999    3211    18144     5.7 |  2.197 % |
c |      4928 | 3723776  9910892 | 2660898    4920    27709     5.6 |  2.197 % |
c |      7490 | 3723776  9910892 | 2926988    7482    55573     7.4 |  2.197 % |
c |     11335 | 3723751  9910837 | 3219687   11326    81472     7.2 |  2.197 % |
c |     17101 | 3723627  9910561 | 3541656   17086   133008     7.8 |  2.200 % |
c |     25750 | 3723106  9909408 | 3895822   25717   228074     8.9 |  2.213 % |
c |     38724 | 3721879  9906693 | 4285404   38621   338855     8.8 |  2.242 % |
c |     58187 | 3720460  9903547 | 4713944   58020   795231    13.7 |  2.277 % |
c |     87379 | 3718655  9899545 | 5185339   87106  1784185    20.5 |  2.321 % |
c |    131169 | 3715498  9892544 | 5703873  130720  2573442    19.7 |  2.398 % |
#### 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.92 0.97 0.99 2/55 2395
Raw data (stat): 2395 (runsolver) R 2394 20838 20837 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 547585996 1052672 99 4294967295 134512640 135381576 3221224528 3221219772 135158418 0 2147483391 7 90112 0 0 0 17 1 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0002 s]
Raw data (loadavg): 0.93 0.97 0.99 2/55 2395
Raw data (stat): 2395 (minisat+) R 2394 20838 20837 0 -1 0 17150 0 0 0 953 46 0 0 25 0 1 0 547585996 73244672 14203 4294967295 134512640 134672761 3221224624 3221221280 134523047 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17882 14203 603 41 0 17841 0
vsize: 71528
[startup+20.0013 s]
Raw data (loadavg): 0.94 0.97 0.99 2/55 2395
Raw data (stat): 2395 (minisat+) R 2394 20838 20837 0 -1 0 37187 0 0 0 1905 93 0 0 25 0 1 0 547585996 172339200 34240 4294967295 134512640 134672761 3221224624 3221184192 134556959 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 42075 34240 603 41 0 42034 0
vsize: 168300
[startup+30.0019 s]
Raw data (loadavg): 0.95 0.97 0.99 2/55 2395
Raw data (stat): 2395 (minisat+) R 2394 20838 20837 0 -1 0 81326 0 0 0 2795 204 0 0 25 0 1 0 547585996 351756288 78379 4294967295 134512640 134672761 3221224624 3221197480 1075347139 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 85878 78379 603 41 0 85837 0
vsize: 343512
[startup+40.001 s]
Raw data (loadavg): 0.96 0.97 0.99 2/55 2395
Raw data (stat): 2395 (minisat+) R 2394 20838 20837 0 -1 0 95087 0 0 0 3756 242 0 0 25 0 1 0 547585996 464773120 92140 4294967295 134512640 134672761 3221224624 3221223792 134561375 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 113470 92140 603 41 0 113429 0
vsize: 453880
[startup+50.0019 s]
Raw data (loadavg): 0.96 0.97 0.99 2/55 2395
Raw data (stat): 2395 (minisat+) R 2394 20838 20837 0 -1 0 95246 0 0 0 4755 243 0 0 25 0 1 0 547585996 465330176 92299 4294967295 134512640 134672761 3221224624 3221223796 134556688 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 113606 92299 603 41 0 113565 0
vsize: 454424
[startup+60.0017 s]
Raw data (loadavg): 0.97 0.97 0.99 2/55 2395
Raw data (stat): 2395 (minisat+) R 2394 20838 20837 0 -1 0 95481 0 0 0 5754 244 0 0 25 0 1 0 547585996 466051072 92534 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 113782 92534 603 41 0 113741 0
vsize: 455128
[startup+70.0028 s]
Raw data (loadavg): 0.97 0.97 0.99 2/55 2395
Raw data (stat): 2395 (minisat+) R 2394 20838 20837 0 -1 0 95525 0 0 0 6754 244 0 0 25 0 1 0 547585996 466321408 92578 4294967295 134512640 134672761 3221224624 3221223792 134561218 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 113848 92578 603 41 0 113807 0
vsize: 455392
[startup+80.0039 s]
Raw data (loadavg): 0.98 0.97 0.99 2/55 2395
Raw data (stat): 2395 (minisat+) R 2394 20838 20837 0 -1 0 95657 0 0 0 7753 245 0 0 25 0 1 0 547585996 466722816 92710 4294967295 134512640 134672761 3221224624 3221223760 134560588 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 113946 92710 603 41 0 113905 0
vsize: 455784
[startup+90.0035 s]
Raw data (loadavg): 0.98 0.97 0.99 2/55 2395
Raw data (stat): 2395 (minisat+) R 2394 20838 20837 0 -1 0 95871 0 0 0 8753 246 0 0 25 0 1 0 547585996 467386368 92924 4294967295 134512640 134672761 3221224624 3221223748 134566118 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 114108 92924 603 41 0 114067 0
vsize: 456432
[startup+100.004 s]
Raw data (loadavg): 0.98 0.97 0.99 2/55 2395
Raw data (stat): 2395 (minisat+) R 2394 20838 20837 0 -1 0 95961 0 0 0 9752 246 0 0 25 0 1 0 547585996 467791872 93014 4294967295 134512640 134672761 3221224624 3221223840 134561993 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 114207 93014 603 41 0 114166 0
vsize: 456828
[startup+110.005 s]
Raw data (loadavg): 0.98 0.97 0.99 2/55 2395
Raw data (stat): 2395 (minisat+) R 2394 20838 20837 0 -1 0 96008 0 0 0 10752 246 0 0 25 0 1 0 547585996 467927040 93061 4294967295 134512640 134672761 3221224624 3221223828 134561964 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 114240 93061 603 41 0 114199 0
vsize: 456960
[startup+120.004 s]
Raw data (loadavg): 0.99 0.97 0.99 2/55 2395
Raw data (stat): 2395 (minisat+) R 2394 20838 20837 0 -1 0 96050 0 0 0 11752 247 0 0 25 0 1 0 547585996 468193280 93103 4294967295 134512640 134672761 3221224624 3221223760 134560588 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 114305 93103 603 41 0 114264 0
vsize: 457220
[startup+130.004 s]
Raw data (loadavg): 0.99 0.97 0.99 2/55 2395
Raw data (stat): 2395 (minisat+) R 2394 20838 20837 0 -1 0 96125 0 0 0 12752 247 0 0 25 0 1 0 547585996 468463616 93178 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 114371 93178 603 41 0 114330 0
vsize: 457484
[startup+140.004 s]
Raw data (loadavg): 0.99 0.97 0.99 2/55 2395
Raw data (stat): 2395 (minisat+) R 2394 20838 20837 0 -1 0 96230 0 0 0 13751 248 0 0 25 0 1 0 547585996 468869120 93283 4294967295 134512640 134672761 3221224624 3221223828 134561964 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 114470 93283 603 41 0 114429 0
vsize: 457880
[startup+150.005 s]
Raw data (loadavg): 0.99 0.97 0.99 2/55 2395
Raw data (stat): 2395 (minisat+) R 2394 20838 20837 0 -1 0 96297 0 0 0 14751 248 0 0 25 0 1 0 547585996 469139456 93350 4294967295 134512640 134672761 3221224624 3221223796 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 114536 93350 603 41 0 114495 0
vsize: 458144
[startup+160.004 s]
Raw data (loadavg): 0.99 0.97 0.99 2/55 2395
Raw data (stat): 2395 (minisat+) R 2394 20838 20837 0 -1 0 96339 0 0 0 15750 249 0 0 25 0 1 0 547585996 469401600 93392 4294967295 134512640 134672761 3221224624 3221223796 134556643 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 114600 93392 603 41 0 114559 0
vsize: 458400
[startup+170.004 s]
Raw data (loadavg): 0.99 0.97 0.99 2/55 2395
Raw data (stat): 2395 (minisat+) R 2394 20838 20837 0 -1 0 96348 0 0 0 16750 249 0 0 25 0 1 0 547585996 469401600 93401 4294967295 134512640 134672761 3221224624 3221223840 134561990 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 114600 93401 603 41 0 114559 0
vsize: 458400
[startup+180.005 s]
Raw data (loadavg): 0.99 0.97 0.99 2/55 2395
Raw data (stat): 2395 (minisat+) R 2394 20838 20837 0 -1 0 96356 0 0 0 17749 250 0 0 25 0 1 0 547585996 469401600 93409 4294967295 134512640 134672761 3221224624 3221223776 134565101 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 114600 93409 603 41 0 114559 0
vsize: 458400
[startup+190.005 s]
Raw data (loadavg): 0.99 0.97 0.99 2/55 2395
Raw data (stat): 2395 (minisat+) R 2394 20838 20837 0 -1 0 96372 0 0 0 18749 250 0 0 25 0 1 0 547585996 469536768 93425 4294967295 134512640 134672761 3221224624 3221223772 134560552 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 114633 93425 603 41 0 114592 0
vsize: 458532
[startup+200.006 s]
Raw data (loadavg): 0.99 0.97 0.99 2/55 2395
Raw data (stat): 2395 (minisat+) R 2394 20838 20837 0 -1 0 96456 0 0 0 19749 251 0 0 25 0 1 0 547585996 469807104 93509 4294967295 134512640 134672761 3221224624 3221223760 134560683 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 114699 93509 603 41 0 114658 0
vsize: 458796
[startup+210.007 s]
Raw data (loadavg): 0.99 0.97 0.99 2/55 2395
Raw data (stat): 2395 (minisat+) R 2394 20838 20837 0 -1 0 96503 0 0 0 20748 252 0 0 25 0 1 0 547585996 469942272 93556 4294967295 134512640 134672761 3221224624 3221223748 134566075 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 114732 93556 603 41 0 114691 0
vsize: 458928
[startup+220.007 s]
Raw data (loadavg): 0.99 0.97 0.99 2/55 2395
Raw data (stat): 2395 (minisat+) R 2394 20838 20837 0 -1 0 96518 0 0 0 21748 252 0 0 25 0 1 0 547585996 470077440 93571 4294967295 134512640 134672761 3221224624 3221223824 134557842 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 114765 93571 603 41 0 114724 0
vsize: 459060
[startup+230.007 s]
Raw data (loadavg): 0.99 0.97 0.99 2/55 2395
Raw data (stat): 2395 (minisat+) R 2394 20838 20837 0 -1 0 96554 0 0 0 22747 253 0 0 25 0 1 0 547585996 470212608 93607 4294967295 134512640 134672761 3221224624 3221223788 134561028 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 114798 93607 603 41 0 114757 0
vsize: 459192
[startup+240.007 s]
Raw data (loadavg): 0.99 0.97 0.99 2/55 2395
Raw data (stat): 2395 (minisat+) R 2394 20838 20837 0 -1 0 96590 0 0 0 23747 253 0 0 25 0 1 0 547585996 470347776 93643 4294967295 134512640 134672761 3221224624 3221223808 134556675 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 114831 93643 603 41 0 114790 0
vsize: 459324
[startup+250.008 s]
Raw data (loadavg): 0.99 0.97 0.99 2/55 2395
Raw data (stat): 2395 (minisat+) R 2394 20838 20837 0 -1 0 96625 0 0 0 24747 254 0 0 25 0 1 0 547585996 470482944 93678 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 114864 93678 603 41 0 114823 0
vsize: 459456
[startup+260.009 s]
Raw data (loadavg): 0.99 0.97 0.99 2/55 2395
Raw data (stat): 2395 (minisat+) R 2394 20838 20837 0 -1 0 96828 0 0 0 25746 255 0 0 25 0 1 0 547585996 471293952 93881 4294967295 134512640 134672761 3221224624 3221223792 134564448 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 115062 93881 603 41 0 115021 0
vsize: 460248
[startup+270.008 s]
Raw data (loadavg): 0.99 0.97 0.99 2/55 2395
Raw data (stat): 2395 (minisat+) R 2394 20838 20837 0 -1 0 96871 0 0 0 26745 255 0 0 25 0 1 0 547585996 471429120 93924 4294967295 134512640 134672761 3221224624 3221223796 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 115095 93924 603 41 0 115054 0
vsize: 460380
[startup+280.009 s]
Raw data (loadavg): 0.99 0.97 0.99 2/55 2397
Raw data (stat): 2395 (minisat+) R 2394 20838 20837 0 -1 0 96891 0 0 0 27745 256 0 0 25 0 1 0 547585996 471429120 93944 4294967295 134512640 134672761 3221224624 3221223824 134557852 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 115095 93944 603 41 0 115054 0
vsize: 460380
[startup+290.019 s]
Raw data (loadavg): 0.99 0.97 0.99 2/55 2397
Raw data (stat): 2395 (minisat+) R 2394 20838 20837 0 -1 0 96913 0 0 0 28745 257 0 0 25 0 1 0 547585996 471564288 93966 4294967295 134512640 134672761 3221224624 3221223796 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 115128 93966 603 41 0 115087 0
vsize: 460512
[startup+300.019 s]
Raw data (loadavg): 1.07 0.99 0.99 2/55 2397
Raw data (stat): 2395 (minisat+) R 2394 20838 20837 0 -1 0 96963 0 0 0 29744 257 0 0 25 0 1 0 547585996 471834624 94016 4294967295 134512640 134672761 3221224624 3221223796 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 115194 94016 603 41 0 115153 0
vsize: 460776
[startup+310.019 s]
Raw data (loadavg): 1.06 0.99 0.99 2/55 2397
Raw data (stat): 2395 (minisat+) R 2394 20838 20837 0 -1 0 97236 0 0 0 30743 260 0 0 25 0 1 0 547585996 472915968 94289 4294967295 134512640 134672761 3221224624 3221223796 134556667 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 115458 94289 603 41 0 115417 0
vsize: 461832
[startup+320.019 s]
Raw data (loadavg): 1.05 0.99 0.99 2/55 2397
Raw data (stat): 2395 (minisat+) R 2394 20838 20837 0 -1 0 97268 0 0 0 31742 260 0 0 25 0 1 0 547585996 473051136 94321 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 115491 94321 603 41 0 115450 0
vsize: 461964
[startup+330.02 s]
Raw data (loadavg): 1.04 0.99 0.99 2/55 2397
Raw data (stat): 2395 (minisat+) R 2394 20838 20837 0 -1 0 97779 0 0 0 32741 262 0 0 25 0 1 0 547585996 475348992 94832 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 116052 94832 603 41 0 116011 0
vsize: 464208
[startup+340.019 s]
Raw data (loadavg): 1.03 0.99 0.99 2/55 2397
Raw data (stat): 2395 (minisat+) R 2394 20838 20837 0 -1 0 98137 0 0 0 33739 263 0 0 25 0 1 0 547585996 476823552 95190 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 116412 95190 603 41 0 116371 0
vsize: 465648
[startup+350.02 s]
Raw data (loadavg): 1.03 0.99 0.99 2/55 2397
Raw data (stat): 2395 (minisat+) R 2394 20838 20837 0 -1 0 98203 0 0 0 34739 263 0 0 25 0 1 0 547585996 477097984 95256 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 116479 95256 603 41 0 116438 0
vsize: 465916
[startup+360.021 s]
Raw data (loadavg): 1.02 0.99 0.99 2/55 2397
Raw data (stat): 2395 (minisat+) R 2394 20838 20837 0 -1 0 98223 0 0 0 35739 264 0 0 25 0 1 0 547585996 477097984 95276 4294967295 134512640 134672761 3221224624 3221223796 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 116479 95276 603 41 0 116438 0
vsize: 465916
[startup+370.02 s]
Raw data (loadavg): 1.02 0.99 0.99 2/55 2397
Raw data (stat): 2395 (minisat+) R 2394 20838 20837 0 -1 0 98281 0 0 0 36738 265 0 0 25 0 1 0 547585996 477368320 95334 4294967295 134512640 134672761 3221224624 3221223796 134556649 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 116545 95334 603 41 0 116504 0
vsize: 466180
[startup+380.02 s]
Raw data (loadavg): 1.02 0.99 0.99 2/55 2397
Raw data (stat): 2395 (minisat+) R 2394 20838 20837 0 -1 0 98303 0 0 0 37738 265 0 0 25 0 1 0 547585996 477368320 95356 4294967295 134512640 134672761 3221224624 3221223796 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 116545 95356 603 41 0 116504 0
vsize: 466180
[startup+390.019 s]
Raw data (loadavg): 1.01 0.99 0.99 2/55 2397
Raw data (stat): 2395 (minisat+) R 2394 20838 20837 0 -1 0 98319 0 0 0 38737 265 0 0 25 0 1 0 547585996 477499392 95372 4294967295 134512640 134672761 3221224624 3221223840 134561999 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 116577 95372 603 41 0 116536 0
vsize: 466308
[startup+400.02 s]
Raw data (loadavg): 1.01 0.99 0.99 2/55 2397
Raw data (stat): 2395 (minisat+) R 2394 20838 20837 0 -1 0 98337 0 0 0 39737 266 0 0 25 0 1 0 547585996 477634560 95390 4294967295 134512640 134672761 3221224624 3221223828 134561964 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 116610 95390 603 41 0 116569 0
vsize: 466440
[startup+410.02 s]
Raw data (loadavg): 1.01 0.99 0.99 3/55 2397
Raw data (stat): 2395 (minisat+) R 2394 20838 20837 0 -1 0 98481 0 0 0 40736 267 0 0 25 0 1 0 547585996 478167040 95534 4294967295 134512640 134672761 3221224624 3221223792 134560920 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 116740 95534 603 41 0 116699 0
vsize: 466960
[startup+420.02 s]
Raw data (loadavg): 1.01 0.99 0.99 2/55 2397
Raw data (stat): 2395 (minisat+) R 2394 20838 20837 0 -1 0 98586 0 0 0 41735 268 0 0 25 0 1 0 547585996 478568448 95639 4294967295 134512640 134672761 3221224624 3221223796 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 116838 95639 603 41 0 116797 0
vsize: 467352
[startup+430.021 s]
Raw data (loadavg): 1.00 0.99 0.99 2/55 2397
Raw data (stat): 2395 (minisat+) R 2394 20838 20837 0 -1 0 98597 0 0 0 42735 268 0 0 25 0 1 0 547585996 478568448 95650 4294967295 134512640 134672761 3221224624 3221223796 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 116838 95650 603 41 0 116797 0
vsize: 467352
[startup+440.02 s]
Raw data (loadavg): 1.00 0.99 0.99 2/55 2397
Raw data (stat): 2395 (minisat+) R 2394 20838 20837 0 -1 0 98622 0 0 0 43735 269 0 0 25 0 1 0 547585996 478703616 95675 4294967295 134512640 134672761 3221224624 3221223796 134556653 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 116871 95675 603 41 0 116830 0
vsize: 467484
[startup+450.021 s]
Raw data (loadavg): 1.00 0.99 0.99 2/55 2397
Raw data (stat): 2395 (minisat+) R 2394 20838 20837 0 -1 0 98650 0 0 0 44735 269 0 0 25 0 1 0 547585996 478838784 95703 4294967295 134512640 134672761 3221224624 3221223796 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 116904 95703 603 41 0 116863 0
vsize: 467616
[startup+460.021 s]
Raw data (loadavg): 1.00 0.99 0.99 2/55 2397
Raw data (stat): 2395 (minisat+) R 2394 20838 20837 0 -1 0 98690 0 0 0 45735 269 0 0 25 0 1 0 547585996 478973952 95743 4294967295 134512640 134672761 3221224624 3221223804 134556590 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 116937 95743 603 41 0 116896 0
vsize: 467748
[startup+470.021 s]
Raw data (loadavg): 1.00 0.99 0.99 2/55 2397
Raw data (stat): 2395 (minisat+) R 2394 20838 20837 0 -1 0 98702 0 0 0 46734 270 0 0 25 0 1 0 547585996 478973952 95755 4294967295 134512640 134672761 3221224624 3221223792 134561215 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 116937 95755 603 41 0 116896 0
vsize: 467748
[startup+480.022 s]
Raw data (loadavg): 1.00 0.99 0.99 2/55 2397
Raw data (stat): 2395 (minisat+) R 2394 20838 20837 0 -1 0 98725 0 0 0 47734 270 0 0 25 0 1 0 547585996 479109120 95778 4294967295 134512640 134672761 3221224624 3221223776 134565116 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 116970 95778 603 41 0 116929 0
vsize: 467880
[startup+490.021 s]
Raw data (loadavg): 1.00 0.99 0.99 2/55 2397
Raw data (stat): 2395 (minisat+) R 2394 20838 20837 0 -1 0 98736 0 0 0 48734 270 0 0 25 0 1 0 547585996 479109120 95789 4294967295 134512640 134672761 3221224624 3221223760 134560588 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 116970 95789 603 41 0 116929 0
vsize: 467880
[startup+500.022 s]
Raw data (loadavg): 1.00 0.99 0.99 2/55 2397
Raw data (stat): 2395 (minisat+) R 2394 20838 20837 0 -1 0 98772 0 0 0 49734 271 0 0 25 0 1 0 547585996 479244288 95825 4294967295 134512640 134672761 3221224624 3221223792 134561275 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 117003 95825 603 41 0 116962 0
vsize: 468012
[startup+510.022 s]
Raw data (loadavg): 1.00 0.99 0.99 2/55 2397
Raw data (stat): 2395 (minisat+) R 2394 20838 20837 0 -1 0 98883 0 0 0 50733 272 0 0 25 0 1 0 547585996 479649792 95936 4294967295 134512640 134672761 3221224624 3221223804 134556674 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 117102 95936 603 41 0 117061 0
vsize: 468408
[startup+520.021 s]
Raw data (loadavg): 1.00 0.99 0.99 2/55 2397
Raw data (stat): 2395 (minisat+) R 2394 20838 20837 0 -1 0 98911 0 0 0 51733 272 0 0 25 0 1 0 547585996 479784960 95964 4294967295 134512640 134672761 3221224624 3221223796 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 117135 95964 603 41 0 117094 0
vsize: 468540
[startup+530.022 s]
Raw data (loadavg): 1.00 0.99 0.99 2/55 2397
Raw data (stat): 2395 (minisat+) R 2394 20838 20837 0 -1 0 98926 0 0 0 52733 272 0 0 25 0 1 0 547585996 479784960 95979 4294967295 134512640 134672761 3221224624 3221223828 134561964 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 117135 95979 603 41 0 117094 0
vsize: 468540
[startup+540.023 s]
Raw data (loadavg): 1.00 0.99 0.99 2/55 2397
Raw data (stat): 2395 (minisat+) R 2394 20838 20837 0 -1 0 98938 0 0 0 53732 273 0 0 25 0 1 0 547585996 479920128 95991 4294967295 134512640 134672761 3221224624 3221223796 134556682 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 117168 95991 603 41 0 117127 0
vsize: 468672
[startup+550.023 s]
Raw data (loadavg): 1.00 0.99 0.99 2/55 2397
Raw data (stat): 2395 (minisat+) R 2394 20838 20837 0 -1 0 98955 0 0 0 54731 274 0 0 25 0 1 0 547585996 479920128 96008 4294967295 134512640 134672761 3221224624 3221223760 134565092 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 117168 96008 603 41 0 117127 0
vsize: 468672
[startup+560.023 s]
Raw data (loadavg): 1.00 0.99 0.99 2/55 2397
Raw data (stat): 2395 (minisat+) R 2394 20838 20837 0 -1 0 98962 0 0 0 55731 274 0 0 25 0 1 0 547585996 479920128 96015 4294967295 134512640 134672761 3221224624 3221223792 134560842 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 117168 96015 603 41 0 117127 0
vsize: 468672
[startup+570.023 s]
Raw data (loadavg): 1.00 0.99 0.99 2/55 2397
Raw data (stat): 2395 (minisat+) R 2394 20838 20837 0 -1 0 98973 0 0 0 56731 274 0 0 25 0 1 0 547585996 480055296 96026 4294967295 134512640 134672761 3221224624 3221223796 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 117201 96026 603 41 0 117160 0
vsize: 468804
[startup+580.024 s]
Raw data (loadavg): 1.00 0.99 0.99 2/55 2399
Raw data (stat): 2395 (minisat+) R 2394 20838 20837 0 -1 0 99013 0 0 0 57730 275 0 0 25 0 1 0 547585996 480186368 96066 4294967295 134512640 134672761 3221224624 3221223796 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 117233 96066 603 41 0 117192 0
vsize: 468932
[startup+590.024 s]
Raw data (loadavg): 1.00 0.99 0.99 2/55 2399
Raw data (stat): 2395 (minisat+) R 2394 20838 20837 0 -1 0 99027 0 0 0 58730 275 0 0 25 0 1 0 547585996 480186368 96080 4294967295 134512640 134672761 3221224624 3221223748 134566034 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 117233 96080 603 41 0 117192 0
vsize: 468932
[startup+600.025 s]
Raw data (loadavg): 1.00 0.99 0.99 2/55 2399
Raw data (stat): 2395 (minisat+) R 2394 20838 20837 0 -1 0 99038 0 0 0 59730 276 0 0 25 0 1 0 547585996 480186368 96091 4294967295 134512640 134672761 3221224624 3221223776 134564780 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 117233 96091 603 41 0 117192 0
vsize: 468932
[startup+610.025 s]
Raw data (loadavg): 1.00 0.99 0.99 2/55 2399
Raw data (stat): 2395 (minisat+) R 2394 20838 20837 0 -1 0 99058 0 0 0 60730 276 0 0 25 0 1 0 547585996 480321536 96111 4294967295 134512640 134672761 3221224624 3221223824 134557852 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 117266 96111 603 41 0 117225 0
vsize: 469064
[startup+620.025 s]
Raw data (loadavg): 1.00 0.99 0.99 2/55 2399
Raw data (stat): 2395 (minisat+) R 2394 20838 20837 0 -1 0 99110 0 0 0 61729 277 0 0 25 0 1 0 547585996 480591872 96163 4294967295 134512640 134672761 3221224624 3221223748 134566018 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 117332 96163 603 41 0 117291 0
vsize: 469328
[startup+630.026 s]
Raw data (loadavg): 1.00 0.99 0.99 2/55 2399
Raw data (stat): 2395 (minisat+) R 2394 20838 20837 0 -1 0 99134 0 0 0 62729 277 0 0 25 0 1 0 547585996 480591872 96187 4294967295 134512640 134672761 3221224624 3221223748 134566068 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 117332 96187 603 41 0 117291 0
vsize: 469328
[startup+640.026 s]
Raw data (loadavg): 1.00 0.99 0.99 2/55 2399
Raw data (stat): 2395 (minisat+) R 2394 20838 20837 0 -1 0 99401 0 0 0 63728 279 0 0 25 0 1 0 547585996 481673216 96454 4294967295 134512640 134672761 3221224624 3221223796 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 117596 96454 603 41 0 117555 0
vsize: 470384
[startup+650.027 s]
Raw data (loadavg): 1.00 0.99 0.99 2/55 2399
Raw data (stat): 2395 (minisat+) R 2394 20838 20837 0 -1 0 99447 0 0 0 64728 279 0 0 25 0 1 0 547585996 481808384 96500 4294967295 134512640 134672761 3221224624 3221223772 134560552 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 117629 96500 603 41 0 117588 0
vsize: 470516
[startup+660.027 s]
Raw data (loadavg): 1.00 0.99 0.99 2/55 2399
Raw data (stat): 2395 (minisat+) R 2394 20838 20837 0 -1 0 99473 0 0 0 65727 280 0 0 25 0 1 0 547585996 481939456 96526 4294967295 134512640 134672761 3221224624 3221223748 134566045 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 117661 96526 603 41 0 117620 0
vsize: 470644
[startup+670.027 s]
Raw data (loadavg): 1.00 0.99 0.99 2/55 2399
Raw data (stat): 2395 (minisat+) R 2394 20838 20837 0 -1 0 99821 0 0 0 66726 281 0 0 25 0 1 0 547585996 483426304 96874 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 118024 96874 603 41 0 117983 0
vsize: 472096
[startup+680.027 s]
Raw data (loadavg): 1.00 0.99 0.99 2/55 2399
Raw data (stat): 2395 (minisat+) R 2394 20838 20837 0 -1 0 99864 0 0 0 67725 282 0 0 25 0 1 0 547585996 483561472 96917 4294967295 134512640 134672761 3221224624 3221223796 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 118057 96917 603 41 0 118016 0
vsize: 472228
[startup+690.027 s]
Raw data (loadavg): 1.00 0.99 0.99 2/55 2399
Raw data (stat): 2395 (minisat+) R 2394 20838 20837 0 -1 0 99896 0 0 0 68725 282 0 0 25 0 1 0 547585996 483696640 96949 4294967295 134512640 134672761 3221224624 3221223840 134561950 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 118090 96949 603 41 0 118049 0
vsize: 472360
[startup+700.027 s]
Raw data (loadavg): 1.00 0.99 0.99 2/55 2399
Raw data (stat): 2395 (minisat+) R 2394 20838 20837 0 -1 0 99922 0 0 0 69725 282 0 0 25 0 1 0 547585996 483696640 96975 4294967295 134512640 134672761 3221224624 3221223840 134561948 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 118090 96975 603 41 0 118049 0
vsize: 472360
[startup+710.027 s]
Raw data (loadavg): 1.00 0.99 0.99 2/55 2399
Raw data (stat): 2395 (minisat+) R 2394 20838 20837 0 -1 0 99940 0 0 0 70725 283 0 0 25 0 1 0 547585996 483831808 96993 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 118123 96993 603 41 0 118082 0
vsize: 472492
[startup+720.026 s]
Raw data (loadavg): 1.00 0.99 0.99 2/55 2399
Raw data (stat): 2395 (minisat+) R 2394 20838 20837 0 -1 0 99974 0 0 0 71725 283 0 0 25 0 1 0 547585996 483966976 97027 4294967295 134512640 134672761 3221224624 3221223796 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 118156 97027 603 41 0 118115 0
vsize: 472624
[startup+730.027 s]
Raw data (loadavg): 1.00 0.99 0.99 2/55 2399
Raw data (stat): 2395 (minisat+) R 2394 20838 20837 0 -1 0 100025 0 0 0 72724 284 0 0 25 0 1 0 547585996 484102144 97078 4294967295 134512640 134672761 3221224624 3221223796 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 118189 97078 603 41 0 118148 0
vsize: 472756
[startup+740.026 s]
Raw data (loadavg): 1.00 0.99 0.99 2/55 2399
Raw data (stat): 2395 (minisat+) R 2394 20838 20837 0 -1 0 100061 0 0 0 73724 284 0 0 25 0 1 0 547585996 484372480 97114 4294967295 134512640 134672761 3221224624 3221223796 134556596 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 118255 97114 603 41 0 118214 0
vsize: 473020
[startup+750.027 s]
Raw data (loadavg): 1.00 0.99 0.99 2/55 2399
Raw data (stat): 2395 (minisat+) R 2394 20838 20837 0 -1 0 100101 0 0 0 74724 284 0 0 25 0 1 0 547585996 484503552 97154 4294967295 134512640 134672761 3221224624 3221223792 134560839 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 118287 97154 603 41 0 118246 0
vsize: 473148
[startup+760.028 s]
Raw data (loadavg): 1.00 0.99 0.99 2/55 2399
Raw data (stat): 2395 (minisat+) R 2394 20838 20837 0 -1 0 100123 0 0 0 75723 285 0 0 25 0 1 0 547585996 484503552 97176 4294967295 134512640 134672761 3221224624 3221223748 134566031 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 118287 97176 603 41 0 118246 0
vsize: 473148
[startup+770.028 s]
Raw data (loadavg): 1.00 0.99 0.99 2/55 2399
Raw data (stat): 2395 (minisat+) R 2394 20838 20837 0 -1 0 100147 0 0 0 76723 285 0 0 25 0 1 0 547585996 485163008 97200 4294967295 134512640 134672761 3221224624 3221223796 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 118448 97200 603 41 0 118407 0
vsize: 473792
[startup+780.028 s]
Raw data (loadavg): 1.00 0.99 0.99 2/55 2399
Raw data (stat): 2395 (minisat+) R 2394 20838 20837 0 -1 0 100202 0 0 0 77723 286 0 0 25 0 1 0 547585996 485298176 97255 4294967295 134512640 134672761 3221224624 3221223748 134566109 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 118481 97255 603 41 0 118440 0
vsize: 473924
[startup+790.027 s]
Raw data (loadavg): 1.00 0.99 0.99 2/55 2399
Raw data (stat): 2395 (minisat+) R 2394 20838 20837 0 -1 0 100231 0 0 0 78722 286 0 0 25 0 1 0 547585996 485433344 97284 4294967295 134512640 134672761 3221224624 3221223796 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 118514 97284 603 41 0 118473 0
vsize: 474056
[startup+800.028 s]
Raw data (loadavg): 1.00 0.99 0.99 2/55 2399
Raw data (stat): 2395 (minisat+) R 2394 20838 20837 0 -1 0 100257 0 0 0 79722 287 0 0 25 0 1 0 547585996 485568512 97310 4294967295 134512640 134672761 3221224624 3221223748 134566043 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 118547 97310 603 41 0 118506 0
vsize: 474188
[startup+810.029 s]
Raw data (loadavg): 1.00 0.99 0.99 2/55 2399
Raw data (stat): 2395 (minisat+) R 2394 20838 20837 0 -1 0 100328 0 0 0 80722 287 0 0 25 0 1 0 547585996 485703680 97381 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 118580 97381 603 41 0 118539 0
vsize: 474320
[startup+820.028 s]
Raw data (loadavg): 1.00 0.99 0.99 2/55 2399
Raw data (stat): 2395 (minisat+) R 2394 20838 20837 0 -1 0 100341 0 0 0 81721 288 0 0 25 0 1 0 547585996 485703680 97394 4294967295 134512640 134672761 3221224624 3221223748 134566047 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 118580 97394 603 41 0 118539 0
vsize: 474320
[startup+830.028 s]
Raw data (loadavg): 1.00 0.99 0.99 2/55 2399
Raw data (stat): 2395 (minisat+) R 2394 20838 20837 0 -1 0 100364 0 0 0 82721 288 0 0 25 0 1 0 547585996 485838848 97417 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 118613 97417 603 41 0 118572 0
vsize: 474452
[startup+840.029 s]
Raw data (loadavg): 1.00 0.99 0.99 2/55 2399
Raw data (stat): 2395 (minisat+) R 2394 20838 20837 0 -1 0 100390 0 0 0 83721 288 0 0 25 0 1 0 547585996 485974016 97443 4294967295 134512640 134672761 3221224624 3221223796 134556643 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 118646 97443 603 41 0 118605 0
vsize: 474584
[startup+850.029 s]
Raw data (loadavg): 1.00 0.99 0.99 2/55 2399
Raw data (stat): 2395 (minisat+) R 2394 20838 20837 0 -1 0 100416 0 0 0 84721 288 0 0 25 0 1 0 547585996 486109184 97469 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 118679 97469 603 41 0 118638 0
vsize: 474716
[startup+860.029 s]
Raw data (loadavg): 1.00 0.99 0.99 3/55 2399
Raw data (stat): 2395 (minisat+) R 2394 20838 20837 0 -1 0 100430 0 0 0 85722 288 0 0 25 0 1 0 547585996 486109184 97483 4294967295 134512640 134672761 3221224624 3221223772 134560552 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 118679 97483 603 41 0 118638 0
vsize: 474716
[startup+870.028 s]
Raw data (loadavg): 1.00 0.99 0.99 2/55 2399
Raw data (stat): 2395 (minisat+) R 2394 20838 20837 0 -1 0 100765 0 0 0 86721 289 0 0 25 0 1 0 547585996 487452672 97818 4294967295 134512640 134672761 3221224624 3221223824 134557849 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 119007 97818 603 41 0 118966 0
vsize: 476028
[startup+880.029 s]
Raw data (loadavg): 1.00 0.99 0.99 2/55 2401
Raw data (stat): 2395 (minisat+) R 2394 20838 20837 0 -1 0 101013 0 0 0 87720 290 0 0 25 0 1 0 547585996 488398848 98066 4294967295 134512640 134672761 3221224624 3221223824 134557895 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 119238 98066 603 41 0 119197 0
vsize: 476952
[startup+890.029 s]
Raw data (loadavg): 1.00 0.99 0.99 2/55 2401
Raw data (stat): 2395 (minisat+) R 2394 20838 20837 0 -1 0 101053 0 0 0 88720 290 0 0 25 0 1 0 547585996 488529920 98106 4294967295 134512640 134672761 3221224624 3221223796 134556667 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 119270 98106 603 41 0 119229 0
vsize: 477080
[startup+900.029 s]
Raw data (loadavg): 1.00 0.99 0.99 2/55 2401
Raw data (stat): 2395 (minisat+) R 2394 20838 20837 0 -1 0 101070 0 0 0 89720 290 0 0 25 0 1 0 547585996 488665088 98123 4294967295 134512640 134672761 3221224624 3221223796 134556641 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 119303 98123 603 41 0 119262 0
vsize: 477212
[startup+910.029 s]
Raw data (loadavg): 1.00 0.99 0.99 2/55 2401
Raw data (stat): 2395 (minisat+) R 2394 20838 20837 0 -1 0 101089 0 0 0 90721 290 0 0 25 0 1 0 547585996 488665088 98142 4294967295 134512640 134672761 3221224624 3221223796 134556685 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 119303 98142 603 41 0 119262 0
vsize: 477212
[startup+920.029 s]
Raw data (loadavg): 1.00 0.99 0.99 2/55 2401
Raw data (stat): 2395 (minisat+) R 2394 20838 20837 0 -1 0 101102 0 0 0 91720 290 0 0 25 0 1 0 547585996 488800256 98155 4294967295 134512640 134672761 3221224624 3221223824 134557915 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 119336 98155 603 41 0 119295 0
vsize: 477344
[startup+930.029 s]
Raw data (loadavg): 1.00 0.99 0.99 2/55 2401
Raw data (stat): 2395 (minisat+) R 2394 20838 20837 0 -1 0 101114 0 0 0 92720 290 0 0 25 0 1 0 547585996 488800256 98167 4294967295 134512640 134672761 3221224624 3221223792 134560885 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 119336 98167 603 41 0 119295 0
vsize: 477344
[startup+940.028 s]
Raw data (loadavg): 1.00 0.99 0.99 2/55 2401
Raw data (stat): 2395 (minisat+) R 2394 20838 20837 0 -1 0 101131 0 0 0 93720 290 0 0 25 0 1 0 547585996 488931328 98184 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 119368 98184 603 41 0 119327 0
vsize: 477472
[startup+950.029 s]
Raw data (loadavg): 1.00 0.99 0.99 2/55 2401
Raw data (stat): 2395 (minisat+) R 2394 20838 20837 0 -1 0 101151 0 0 0 94721 290 0 0 25 0 1 0 547585996 488931328 98204 4294967295 134512640 134672761 3221224624 3221223748 134566057 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 119368 98204 603 41 0 119327 0
vsize: 477472
[startup+960.029 s]
Raw data (loadavg): 1.00 0.99 0.99 2/55 2401
Raw data (stat): 2395 (minisat+) R 2394 20838 20837 0 -1 0 101166 0 0 0 95721 290 0 0 25 0 1 0 547585996 489066496 98219 4294967295 134512640 134672761 3221224624 3221223796 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 119401 98219 603 41 0 119360 0
vsize: 477604
[startup+970.028 s]
Raw data (loadavg): 1.00 0.99 0.99 2/55 2401
Raw data (stat): 2395 (minisat+) R 2394 20838 20837 0 -1 0 101184 0 0 0 96721 291 0 0 25 0 1 0 547585996 489066496 98237 4294967295 134512640 134672761 3221224624 3221223824 134557885 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 119401 98237 603 41 0 119360 0
vsize: 477604
[startup+980.029 s]
Raw data (loadavg): 1.00 0.99 0.99 3/55 2401
Raw data (stat): 2395 (minisat+) R 2394 20838 20837 0 -1 0 101205 0 0 0 97721 291 0 0 25 0 1 0 547585996 489197568 98258 4294967295 134512640 134672761 3221224624 3221223796 134556688 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 119433 98258 603 41 0 119392 0
vsize: 477732
[startup+990.029 s]
Raw data (loadavg): 1.00 0.99 0.99 2/55 2401
Raw data (stat): 2395 (minisat+) R 2394 20838 20837 0 -1 0 101224 0 0 0 98721 291 0 0 25 0 1 0 547585996 489197568 98277 4294967295 134512640 134672761 3221224624 3221223792 134561011 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 119433 98277 603 41 0 119392 0
vsize: 477732
[startup+1000.03 s]
Raw data (loadavg): 1.00 0.99 0.99 2/55 2401
Raw data (stat): 2395 (minisat+) R 2394 20838 20837 0 -1 0 101275 0 0 0 99721 291 0 0 25 0 1 0 547585996 489332736 98328 4294967295 134512640 134672761 3221224624 3221223796 134556643 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 119466 98328 603 41 0 119425 0
vsize: 477864
[startup+1010.03 s]
Raw data (loadavg): 1.00 0.99 0.99 2/55 2401
Raw data (stat): 2395 (minisat+) R 2394 20838 20837 0 -1 0 101280 0 0 0 100721 291 0 0 25 0 1 0 547585996 489332736 98333 4294967295 134512640 134672761 3221224624 3221223780 134561032 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 119466 98333 603 41 0 119425 0
vsize: 477864
[startup+1020.03 s]
Raw data (loadavg): 1.00 0.99 0.99 2/55 2401
Raw data (stat): 2395 (minisat+) R 2394 20838 20837 0 -1 0 101297 0 0 0 101721 291 0 0 25 0 1 0 547585996 489467904 98350 4294967295 134512640 134672761 3221224624 3221223796 134556682 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 119499 98350 603 41 0 119458 0
vsize: 477996
[startup+1030.03 s]
Raw data (loadavg): 1.00 0.99 0.99 2/55 2401
Raw data (stat): 2395 (minisat+) R 2394 20838 20837 0 -1 0 101298 0 0 0 102722 291 0 0 25 0 1 0 547585996 489467904 98351 4294967295 134512640 134672761 3221224624 3221223796 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 119499 98351 603 41 0 119458 0
vsize: 477996
[startup+1040.03 s]
Raw data (loadavg): 1.00 0.99 0.99 2/55 2401
Raw data (stat): 2395 (minisat+) R 2394 20838 20837 0 -1 0 101300 0 0 0 103722 291 0 0 25 0 1 0 547585996 489467904 98353 4294967295 134512640 134672761 3221224624 3221223796 134556667 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 119499 98353 603 41 0 119458 0
vsize: 477996
[startup+1050.03 s]
Raw data (loadavg): 1.00 0.99 0.99 2/55 2401
Raw data (stat): 2395 (minisat+) R 2394 20838 20837 0 -1 0 101571 0 0 0 104721 292 0 0 25 0 1 0 547585996 490549248 98624 4294967295 134512640 134672761 3221224624 3221223820 134556678 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 119763 98624 603 41 0 119722 0
vsize: 479052
[startup+1060.03 s]
Raw data (loadavg): 1.00 0.99 0.99 2/55 2401
Raw data (stat): 2395 (minisat+) R 2394 20838 20837 0 -1 0 101598 0 0 0 105721 292 0 0 25 0 1 0 547585996 490684416 98651 4294967295 134512640 134672761 3221224624 3221223760 134560697 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 119796 98651 603 41 0 119755 0
vsize: 479184
[startup+1070.03 s]
Raw data (loadavg): 1.00 0.99 0.99 2/55 2401
Raw data (stat): 2395 (minisat+) R 2394 20838 20837 0 -1 0 101623 0 0 0 106721 292 0 0 25 0 1 0 547585996 490819584 98676 4294967295 134512640 134672761 3221224624 3221223796 134556643 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 119829 98676 603 41 0 119788 0
vsize: 479316
[startup+1080.03 s]
Raw data (loadavg): 1.00 0.99 0.99 2/55 2401
Raw data (stat): 2395 (minisat+) R 2394 20838 20837 0 -1 0 101634 0 0 0 107721 292 0 0 25 0 1 0 547585996 490819584 98687 4294967295 134512640 134672761 3221224624 3221223828 134561964 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 119829 98687 603 41 0 119788 0
vsize: 479316
[startup+1090.03 s]
Raw data (loadavg): 1.00 0.99 0.99 2/55 2401
Raw data (stat): 2395 (minisat+) R 2394 20838 20837 0 -1 0 101648 0 0 0 108722 292 0 0 25 0 1 0 547585996 490819584 98701 4294967295 134512640 134672761 3221224624 3221223796 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 119829 98701 603 41 0 119788 0
vsize: 479316
[startup+1100.03 s]
Raw data (loadavg): 1.00 0.99 0.99 2/55 2401
Raw data (stat): 2395 (minisat+) R 2394 20838 20837 0 -1 0 101673 0 0 0 109722 292 0 0 25 0 1 0 547585996 490954752 98726 4294967295 134512640 134672761 3221224624 3221223812 134556588 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 119862 98726 603 41 0 119821 0
vsize: 479448
[startup+1110.03 s]
Raw data (loadavg): 1.00 0.99 0.99 2/55 2401
Raw data (stat): 2395 (minisat+) R 2394 20838 20837 0 -1 0 101715 0 0 0 110722 292 0 0 25 0 1 0 547585996 491089920 98768 4294967295 134512640 134672761 3221224624 3221223760 134560729 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 119895 98768 603 41 0 119854 0
vsize: 479580
[startup+1120.03 s]
Raw data (loadavg): 1.00 0.99 0.99 2/55 2401
Raw data (stat): 2395 (minisat+) R 2394 20838 20837 0 -1 0 101727 0 0 0 111722 292 0 0 25 0 1 0 547585996 491225088 98780 4294967295 134512640 134672761 3221224624 3221223748 134566109 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 119928 98780 603 41 0 119887 0
vsize: 479712
[startup+1130.04 s]
Raw data (loadavg): 1.00 0.99 0.99 2/55 2401
Raw data (stat): 2395 (minisat+) R 2394 20838 20837 0 -1 0 101745 0 0 0 112723 292 0 0 25 0 1 0 547585996 491225088 98798 4294967295 134512640 134672761 3221224624 3221223788 134561235 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 119928 98798 603 41 0 119887 0
vsize: 479712
[startup+1140.04 s]
Raw data (loadavg): 1.00 0.99 0.99 2/55 2401
Raw data (stat): 2395 (minisat+) R 2394 20838 20837 0 -1 0 101753 0 0 0 113723 292 0 0 25 0 1 0 547585996 491225088 98806 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 119928 98806 603 41 0 119887 0
vsize: 479712
[startup+1150.04 s]
Raw data (loadavg): 1.00 0.99 0.99 2/55 2401
Raw data (stat): 2395 (minisat+) R 2394 20838 20837 0 -1 0 101793 0 0 0 114723 293 0 0 25 0 1 0 547585996 491495424 98846 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 119994 98846 603 41 0 119953 0
vsize: 479976
[startup+1160.04 s]
Raw data (loadavg): 1.00 0.99 0.99 2/55 2401
Raw data (stat): 2395 (minisat+) R 2394 20838 20837 0 -1 0 101815 0 0 0 115723 293 0 0 25 0 1 0 547585996 491495424 98868 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 119994 98868 603 41 0 119953 0
vsize: 479976
[startup+1170.04 s]
Raw data (loadavg): 1.00 0.99 0.99 2/55 2401
Raw data (stat): 2395 (minisat+) R 2394 20838 20837 0 -1 0 101840 0 0 0 116723 293 0 0 25 0 1 0 547585996 491626496 98893 4294967295 134512640 134672761 3221224624 3221223824 134557828 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 120026 98893 603 41 0 119985 0
vsize: 480104
[startup+1180.04 s]
Raw data (loadavg): 1.00 0.99 0.99 2/55 2403
Raw data (stat): 2395 (minisat+) R 2394 20838 20837 0 -1 0 101867 0 0 0 117723 293 0 0 25 0 1 0 547585996 491761664 98920 4294967295 134512640 134672761 3221224624 3221223748 134566057 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 120059 98920 603 41 0 120018 0
vsize: 480236
[startup+1190.04 s]
Raw data (loadavg): 1.00 0.99 0.99 2/55 2403
Raw data (stat): 2395 (minisat+) R 2394 20838 20837 0 -1 0 101887 0 0 0 118723 293 0 0 25 0 1 0 547585996 491761664 98940 4294967295 134512640 134672761 3221224624 3221223824 134557911 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 120059 98940 603 41 0 120018 0
vsize: 480236
[startup+1200.04 s]
Raw data (loadavg): 1.00 0.99 0.99 2/55 2403
Raw data (stat): 2395 (minisat+) R 2394 20838 20837 0 -1 0 101901 0 0 0 119723 293 0 0 25 0 1 0 547585996 491896832 98954 4294967295 134512640 134672761 3221224624 3221223748 134566049 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 120092 98954 603 41 0 120051 0
vsize: 480368
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.25 s]
Raw data (loadavg): 1.00 0.99 0.99 1/55 2403
Raw data (stat): 2395 (minisat+) Z 2394 20838 20837 0 -1 12 101903 0 0 0 119723 313 0 0 24 0 1 0 547585996 0 0 4294967295 0 0 0 0 0 0 16384 5 16386 3222412051 0 0 17 1 0 0
Raw data (statm): 0 0 0 0 0 0 0
vsize: 0
Maximum CPU time exceeded: sending SIGTERM and SIGKILL

Child status: 0
Real time (s): 1200.25
CPU time (s): 1200.37
CPU user time (s): 1197.24
CPU system time (s): 3.13252
CPU usage (%): 100.01
Max. virtual memory (Kb): 480368
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####