PB'05 competition: run trace

Some explanations

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

Name	normalized-opb/web/uclid_pb_benchmarks/normalized-ooo.tag12.ucl.opb
MD5SUM	04162d5197113d66489e9d95b6572385
Bench Category	no optimization function (SAT)
Has Objective Function	NO
Satisfiable	NO
(Un)Satisfiability was proved
Best value of the objective function
Optimality of the best value was proved
Number of terms in the objective function	0
Biggest coefficient in the objective function	0
Number of bits for the biggest coefficient in the objective function	0
Sum of the numbers in the objective function	0
Number of bits of the sum of numbers in the objective function	0
Biggest number in a constraint	41
Number of bits of the biggest number in a constraint	6
Biggest sum of numbers in a constraint	134
Number of bits of the biggest sum of numbers	8
Best result obtained on this benchmark	UNSAT
Best CPU time to get the best result obtained on this benchmark	20.7588
Number of variables	20605
Total number of constraints	59851
Number of constraints which are clauses	58675
Number of constraints which are cardinality constraints (but not clauses)	0
Number of constraints which are nor clauses,nor cardinality constraints	1176
Minimum length of a constraint	1
Maximum length of a constraint	11
Trace number 5228

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc10 THE 2005-04-13 22:42:07 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=3695 boxname=wulflinc10 idbench=311 idsolver=10 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  04162d5197113d66489e9d95b6572385  /oldhome/oroussel/tmp/wulflinc10/normalized-ooo.tag12.ucl.opb
REAL COMMAND:  minisat+ -ca /oldhome/oroussel/tmp/wulflinc10/normalized-ooo.tag12.ucl.opb /oldhome/oroussel/tmp/wulflinc10/normalized-ooo.tag12.ucl.opb
IDLAUNCH: 3695
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 450.999
cache size	: 512 KB
fdiv_bug	: no
hlt_bug		: no
f00f_bug	: no
coma_bug	: no
fpu		: yes
fpu_exception	: yes
cpuid level	: 2
wp		: yes
flags		: fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse
bogomips	: 890.88

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

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        883268 kB
Buffers:         34448 kB
Cached:          97036 kB
SwapCached:        164 kB
Active:          52920 kB
Inactive:        81592 kB
HighTotal:      131008 kB
HighFree:        30324 kB
LowTotal:       903652 kB
LowFree:        852944 kB
SwapTotal:     2097136 kB
SwapFree:      2096972 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6916 kB
Slab:            11320 kB
Committed_AS:    63484 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-13 23:02:09 (client local time) WITH STATUS 0 IN 1200.18 SECONDS
stats: 3695 7 1200.18 0
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 59850 PB-constraints to clauses...
c   -- Unit propagations: pppppppppppp
c   -- Detecting intervals from adjacent constraints: #################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################
c   -- Clauses(.)/Splits(s): ...................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................
c ---[59843]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[59832]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[59827]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[59819]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[59811]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[59803]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[59795]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[59787]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[59779]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[59771]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[59763]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[59752]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[59741]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[59736]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[59734]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[59729]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[59718]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[59692]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[59687]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[59685]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[59680]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[59678]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[59673]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[59671]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[59666]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[59664]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[59659]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[59657]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[59652]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[59650]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[59645]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[59643]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[59638]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[59606]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[59592]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[59587]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[59582]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[59541]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[59512]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[59498]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[59451]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[59434]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[59294]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[59280]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[59224]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[59186]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[59151]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[59134]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[59129]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[59109]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[59089]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[59084]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[59046]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[59035]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[58961]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[58935]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[58894]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[58823]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[58812]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[58795]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[58784]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[58731]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[58714]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[58631]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[58602]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[58579]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[58556]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[58533]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[58510]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[58487]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[58446]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[58420]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[58400]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[58287]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[58285]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[58055]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[57993]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[57925]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[57920]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[57870]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[57859]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[57836]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[57813]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[57796]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[57791]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[57771]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[57751]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[57710]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[57693]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[57688]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[57668]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[57639]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[57598]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[57587]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[57570]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[57559]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[57443]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[57306]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[57262]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[57194]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[57189]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[57139]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[57128]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[57096]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[57076]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[56948]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[56937]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[56920]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[56909]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[56892]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[56872]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[56804]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[56787]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[56674]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[56633]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[56601]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[56569]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[56537]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[56505]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[56446]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[56411]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[56385]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[56200]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[56186]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[55791]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[55666]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[55427]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[55332]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[55315]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[55310]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[55290]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[55261]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[55184]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[55173]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[55156]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[55145]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[55122]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[55093]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[55070]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[55053]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[55048]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[55028]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[55008]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[54973]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[54905]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[54882]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[54865]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[54860]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[54840]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[54820]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[54773]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[54753]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[54688]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[54677]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[54660]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[54649]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[54632]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[54612]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[54442]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[54218]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[54129]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[53962]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[53867]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[53850]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[53845]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[53825]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[53796]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[53719]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[53708]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[53691]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[53680]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[53645]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[53625]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[53590]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[53387]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[53376]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[53359]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[53348]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[53331]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[53311]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[53294]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[53268]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[53185]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[53168]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[53028]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[52978]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[52937]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[52896]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[52855]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[52778]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[52734]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[52702]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[52427]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[52407]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[51799]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[51599]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[51438]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[50899]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[50777]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[50754]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[50737]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[50732]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[50712]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[50692]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[50645]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[50625]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[50488]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[50477]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[50460]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[50449]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[50432]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[50412]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[50389]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[50354]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[50325]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[50302]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[50285]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[50280]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[50260]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[50240]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[50205]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[50149]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[50060]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[50031]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[50008]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[49991]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[49986]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[49966]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[49946]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[49911]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[49840]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[49820]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[49785]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[49690]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[49679]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[49662]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[49651]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[49634]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[49614]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[49597]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[49571]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[49335]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[48997]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[48857]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[48741]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[48367]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[48245]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[48222]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[48205]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[48200]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[48180]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[48160]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[48113]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[48093]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[47956]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[47945]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[47928]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[47917]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[47900]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[47880]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[47842]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[47822]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[47787]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[47731]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[47447]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[47436]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[47419]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[47408]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[47391]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[47371]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[47354]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[47328]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[47311]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[47279]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[47181]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[47164]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[46997]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[46938]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[46888]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[46838]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[46743]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[46690]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[46652]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[46269]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[46243]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[45377]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[45087]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[44842]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[44645]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[43656]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[43507]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[43478]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[43455]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[43438]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[43433]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[43413]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[43393]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[43358]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[43287]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[43267]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[43232]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[43017]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[43006]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[42989]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[42978]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[42961]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[42941]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[42924]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[42898]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[42875]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[42834]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[42799]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[42770]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[42747]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[42730]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[42725]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[42705]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[42685]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[42650]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[42594]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[42523]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[42413]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[42378]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[42349]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[42326]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[42309]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[42304]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[42284]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[42264]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[42229]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[42173]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[42084]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[42064]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[42029]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[41973]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[41854]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[41843]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[41826]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[41815]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[41798]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[41778]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[41761]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[41735]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[41718]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[41686]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[41372]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[40896]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[40696]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[40523]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[40380]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[39697]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[39548]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[39519]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[39496]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[39479]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[39474]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[39454]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[39434]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[39399]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[39328]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[39308]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[39273]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[39058]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[39047]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[39030]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[39019]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[39002]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[38982]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[38965]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[38939]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[38898]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[38878]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[38843]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[38787]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[38716]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[38339]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[38328]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[38311]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[38300]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[38283]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[38263]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[38246]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[38220]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[38203]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[38171]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[38154]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[38116]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[38003]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[37986]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[37792]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[37724]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[37665]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[37552]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[37490]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[37446]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[36937]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[36905]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[35736]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[35338]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[34994]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[34704]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[34471]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[32855]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[32679]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[32644]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[32615]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[32592]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[32575]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[32570]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[32550]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[32530]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[32495]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[32439]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[32350]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[32330]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[32295]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[32239]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[31940]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[31929]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[31912]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[31901]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[31884]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[31864]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[31847]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[31821]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[31804]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[31772]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[31749]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[31702]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[31661]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[31626]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[31597]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[31574]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[31557]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[31552]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[31532]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[31512]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[31477]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[31421]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[31350]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[31264]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[31133]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[31092]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[31057]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[31028]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[31005]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[30988]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[30983]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[30963]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[30943]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[30908]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[30852]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[30781]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[30674]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[30654]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[30619]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[30563]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[30492]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[30349]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[30338]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[30321]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[30310]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[30293]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[30273]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[30256]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[30230]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[30213]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[30181]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[30164]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[30126]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[29722]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[29084]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[28812]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[28573]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[28367]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[28197]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[27085]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[26909]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[26874]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[26845]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[26822]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[26805]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[26800]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[26780]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[26760]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[26725]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[26669]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[26580]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[26560]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[26525]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[26469]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[26170]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[26159]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[26142]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[26131]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[26114]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[26094]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[26077]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[26051]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[26034]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[26002]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[25958]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[25938]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[25903]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[25847]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[25776]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[25690]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[25208]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[25197]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[25180]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[25169]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[25152]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[25132]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[25115]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[25089]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[25072]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[25040]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[25023]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[24985]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[24968]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[24924]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[24796]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[24779]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[24558]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[24481]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[24350]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[24279]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[24229]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[23576]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[23538]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[22021]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[21497]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[21036]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[20638]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[20303]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[20034]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[17587]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[17384]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[17343]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[17308]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[17279]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[17256]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[17239]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[17234]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[17214]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[17194]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[17159]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[17103]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[17032]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[16925]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[16905]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[16870]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[16814]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[16743]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[16348]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[16337]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[16320]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[16309]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[16292]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[16272]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[16255]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[16229]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[16212]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[16180]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[16163]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[16125]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[16102]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[16049]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[16002]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[15961]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[15926]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[15897]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[15874]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[15857]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[15852]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[15832]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[15812]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[15777]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[15721]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[15650]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[15564]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[15463]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[15311]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[15264]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[15223]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[15188]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[15159]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[15136]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[15119]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[15114]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[15094]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[15074]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[15039]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[14983]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[14912]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[14826]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[14701]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[14681]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[14646]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[14590]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[14519]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[14433]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[14266]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[14255]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[14238]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[14227]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[14210]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[14190]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[14173]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[14147]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[14130]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[14098]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[14081]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[14043]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[14026]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[13982]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[13476]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[12652]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[12296]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[11979]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[11701]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[11462]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[11265]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[9586]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[9383]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[9342]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[9307]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[9278]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[9255]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[9238]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[9233]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[9213]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[9193]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[9158]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[9102]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[9031]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[8924]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[8904]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[8869]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[8813]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[8742]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[8347]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[8336]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[8319]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[8308]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[8291]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[8271]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[8254]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[8228]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[8211]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[8179]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[8162]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[8124]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[8077]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[8057]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[8022]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[7966]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[7895]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[7809]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[7708]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[7109]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[7098]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[7081]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[7070]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[7053]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[7033]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[7016]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[6990]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[6973]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[6941]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[6924]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[6886]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[6869]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[6825]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[6808]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[6758]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[6675]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[6544]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[6386]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[6261]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[6226]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[6188]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[5532]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[5446]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[5363]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[5277]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[5188]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[5096]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[5001]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[4903]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[4805]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[4674]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[4057]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[3221]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[3151]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[2981]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[2895]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[2812]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[2726]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[2637]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[2545]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[2450]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[2352]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[2254]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1580]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1175]---> Adder-cost: 19   maxlim: 30   bits: 6/5
c ---[1174]---> Adder-cost: 19   maxlim: 30   bits: 6/5
c ---[1173]---> Adder-cost: 11   maxlim: 31   bits: 6/5
c ---[1172]---> Adder-cost: 10   maxlim: 31   bits: 6/5
c ---[1171]---> Adder-cost: 19   maxlim: 30   bits: 6/5
c ---[1170]---> Adder-cost: 19   maxlim: 30   bits: 6/5
c ---[1169]---> Adder-cost: 11   maxlim: 31   bits: 6/5
c ---[1168]---> Adder-cost: 10   maxlim: 31   bits: 6/5
c ---[1167]---> Adder-cost: 19   maxlim: 30   bits: 6/5
c ---[1166]---> Adder-cost: 19   maxlim: 30   bits: 6/5
c ---[1165]---> Adder-cost: 11   maxlim: 31   bits: 6/5
c ---[1164]---> Adder-cost: 10   maxlim: 31   bits: 6/5
c ---[1163]---> Adder-cost: 19   maxlim: 29   bits: 6/5
c ---[1162]---> Adder-cost: 10   maxlim: 31   bits: 6/5
c ---[1161]---> Adder-cost: 12   maxlim: 32   bits: 7/6
c ---[1160]---> Adder-cost: 19   maxlim: 30   bits: 6/5
c ---[1159]---> Adder-cost: 19   maxlim: 30   bits: 6/5
c ---[1158]---> Adder-cost: 19   maxlim: 30   bits: 6/5
c ---[1157]---> Adder-cost: 1   maxlim: 31   bits: 6/5
c ---[1156]---> Adder-cost: 9   maxlim: 31   bits: 6/5
c ---[1155]---> Adder-cost: 19   maxlim: 30   bits: 6/5
c ---[1154]---> Adder-cost: 19   maxlim: 30   bits: 6/5
c ---[1153]---> Adder-cost: 11   maxlim: 31   bits: 6/5
c ---[1152]---> Adder-cost: 10   maxlim: 31   bits: 6/5
c ---[1151]---> Adder-cost: 19   maxlim: 30   bits: 6/5
c ---[1150]---> Adder-cost: 19   maxlim: 30   bits: 6/5
c ---[1149]---> Adder-cost: 11   maxlim: 31   bits: 6/5
c ---[1148]---> Adder-cost: 10   maxlim: 31   bits: 6/5
c ---[1147]---> Adder-cost: 19   maxlim: 30   bits: 6/5
c ---[1146]---> Adder-cost: 19   maxlim: 30   bits: 6/5
c ---[1145]---> Adder-cost: 11   maxlim: 31   bits: 6/5
c ---[1144]---> Adder-cost: 10   maxlim: 31   bits: 6/5
c ---[1143]---> Adder-cost: 19   maxlim: 30   bits: 6/5
c ---[1142]---> Adder-cost: 19   maxlim: 30   bits: 6/5
c ---[1141]---> Adder-cost: 11   maxlim: 31   bits: 6/5
c ---[1140]---> Adder-cost: 10   maxlim: 31   bits: 6/5
c ---[1139]---> Adder-cost: 17   maxlim: 29   bits: 6/5
c ---[1138]---> Adder-cost: 1   maxlim: 31   bits: 6/5
c ---[1137]---> Adder-cost: 12   maxlim: 32   bits: 7/6
c ---[1136]---> Adder-cost: 19   maxlim: 30   bits: 6/5
c ---[1135]---> Adder-cost: 17   maxlim: 28   bits: 6/5
c ---[1134]---> Adder-cost: 12   maxlim: 32   bits: 7/6
c ---[1133]---> Adder-cost: 20   maxlim: 33   bits: 7/6
c ---[1132]---> Adder-cost: 18   maxlim: 29   bits: 6/5
c ---[1131]---> Adder-cost: 17   maxlim: 29   bits: 6/5
c ---[1130]---> Adder-cost: 9   maxlim: 31   bits: 6/5
c ---[1129]---> Adder-cost: 12   maxlim: 32   bits: 7/6
c ---[1128]---> Adder-cost: 19   maxlim: 30   bits: 6/5
c ---[1127]---> Adder-cost: 19   maxlim: 30   bits: 6/5
c ---[1126]---> Adder-cost: 19   maxlim: 30   bits: 6/5
c ---[1125]---> Adder-cost: 1   maxlim: 31   bits: 6/5
c ---[1124]---> Adder-cost: 9   maxlim: 31   bits: 6/5
c ---[1123]---> Adder-cost: 19   maxlim: 30   bits: 6/5
c ---[1122]---> Adder-cost: 19   maxlim: 30   bits: 6/5
c ---[1121]---> Adder-cost: 11   maxlim: 31   bits: 6/5
c ---[1120]---> Adder-cost: 10   maxlim: 31   bits: 6/5
c ---[1119]---> Adder-cost: 19   maxlim: 30   bits: 6/5
c ---[1118]---> Adder-cost: 19   maxlim: 30   bits: 6/5
c ---[1117]---> Adder-cost: 11   maxlim: 31   bits: 6/5
c ---[1116]---> Adder-cost: 10   maxlim: 31   bits: 6/5
c ---[1115]---> Adder-cost: 19   maxlim: 30   bits: 6/5
c ---[1114]---> Adder-cost: 19   maxlim: 30   bits: 6/5
c ---[1113]---> Adder-cost: 11   maxlim: 31   bits: 6/5
c ---[1112]---> Adder-cost: 10   maxlim: 31   bits: 6/5
c ---[1111]---> Adder-cost: 19   maxlim: 30   bits: 6/5
c ---[1110]---> Adder-cost: 19   maxlim: 30   bits: 6/5
c ---[1109]---> Adder-cost: 11   maxlim: 31   bits: 6/5
c ---[1108]---> Adder-cost: 10   maxlim: 31   bits: 6/5
c ---[1107]---> Adder-cost: 19   maxlim: 30   bits: 6/5
c ---[1106]---> Adder-cost: 19   maxlim: 30   bits: 6/5
c ---[1105]---> Adder-cost: 11   maxlim: 31   bits: 6/5
c ---[1104]---> Adder-cost: 10   maxlim: 31   bits: 6/5
c ---[1103]---> Adder-cost: 19   maxlim: 30   bits: 6/5
c ---[1102]---> Adder-cost: 19   maxlim: 30   bits: 6/5
c ---[1101]---> Adder-cost: 11   maxlim: 31   bits: 6/5
c ---[1100]---> Adder-cost: 10   maxlim: 31   bits: 6/5
c ---[1099]---> Adder-cost: 19   maxlim: 30   bits: 6/5
c ---[1098]---> Adder-cost: 19   maxlim: 30   bits: 6/5
c ---[1097]---> Adder-cost: 11   maxlim: 31   bits: 6/5
c ---[1096]---> Adder-cost: 10   maxlim: 31   bits: 6/5
c ---[1095]---> Adder-cost: 19   maxlim: 30   bits: 6/5
c ---[1094]---> Adder-cost: 19   maxlim: 30   bits: 6/5
c ---[1093]---> Adder-cost: 11   maxlim: 31   bits: 6/5
c ---[1092]---> Adder-cost: 10   maxlim: 31   bits: 6/5
c ---[1091]---> Adder-cost: 19   maxlim: 30   bits: 6/5
c ---[1090]---> Adder-cost: 19   maxlim: 30   bits: 6/5
c ---[1089]---> Adder-cost: 11   maxlim: 31   bits: 6/5
c ---[1088]---> Adder-cost: 10   maxlim: 31   bits: 6/5
c ---[1087]---> Adder-cost: 17   maxlim: 28   bits: 6/5
c ---[1086]---> Adder-cost: 12   maxlim: 32   bits: 7/6
c ---[1085]---> Adder-cost: 18   maxlim: 33   bits: 7/6
c ---[1084]---> Adder-cost: 17   maxlim: 29   bits: 6/5
c ---[1083]---> Adder-cost: 17   maxlim: 28   bits: 6/5
c ---[1082]---> Adder-cost: 12   maxlim: 32   bits: 7/6
c ---[1081]---> Adder-cost: 18   maxlim: 33   bits: 7/6
c ---[1080]---> Adder-cost: 17   maxlim: 29   bits: 6/5
c ---[1079]---> Adder-cost: 17   maxlim: 27   bits: 6/5
c ---[1078]---> Adder-cost: 19   maxlim: 33   bits: 7/6
c ---[1077]---> Adder-cost: 20   maxlim: 34   bits: 7/6
c ---[1076]---> Adder-cost: 17   maxlim: 28   bits: 6/5
c ---[1075]---> Adder-cost: 17   maxlim: 28   bits: 6/5
c ---[1074]---> Adder-cost: 12   maxlim: 32   bits: 7/6
c ---[1073]---> Adder-cost: 18   maxlim: 33   bits: 7/6
c ---[1072]---> Adder-cost: 17   maxlim: 29   bits: 6/5
c ---[1071]---> Adder-cost: 17   maxlim: 29   bits: 6/5
c ---[1070]---> Adder-cost: 9   maxlim: 31   bits: 6/5
c ---[1069]---> Adder-cost: 12   maxlim: 32   bits: 7/6
c ---[1068]---> Adder-cost: 19   maxlim: 30   bits: 6/5
c ---[1067]---> Adder-cost: 19   maxlim: 30   bits: 6/5
c ---[1066]---> Adder-cost: 19   maxlim: 30   bits: 6/5
c ---[1065]---> Adder-cost: 1   maxlim: 31   bits: 6/5
c ---[1064]---> Adder-cost: 7   maxlim: 31   bits: 6/5
c ---[1063]---> Adder-cost: 19   maxlim: 30   bits: 6/5
c ---[1062]---> Adder-cost: 19   maxlim: 30   bits: 6/5
c ---[1061]---> Adder-cost: 11   maxlim: 31   bits: 6/5
c ---[1060]---> Adder-cost: 10   maxlim: 31   bits: 6/5
c ---[1059]---> Adder-cost: 19   maxlim: 30   bits: 6/5
c ---[1058]---> Adder-cost: 19   maxlim: 30   bits: 6/5
c ---[1057]---> Adder-cost: 11   maxlim: 31   bits: 6/5
c ---[1056]---> Adder-cost: 10   maxlim: 31   bits: 6/5
c ---[1055]---> Adder-cost: 19   maxlim: 30   bits: 6/5
c ---[1054]---> Adder-cost: 19   maxlim: 30   bits: 6/5
c ---[1053]---> Adder-cost: 11   maxlim: 31   bits: 6/5
c ---[1052]---> Adder-cost: 10   maxlim: 31   bits: 6/5
c ---[1051]---> Adder-cost: 19   maxlim: 30   bits: 6/5
c ---[1050]---> Adder-cost: 19   maxlim: 30   bits: 6/5
c ---[1049]---> Adder-cost: 11   maxlim: 31   bits: 6/5
c ---[1048]---> Adder-cost: 10   maxlim: 31   bits: 6/5
c ---[1047]---> Adder-cost: 19   maxlim: 30   bits: 6/5
c ---[1046]---> Adder-cost: 19   maxlim: 30   bits: 6/5
c ---[1045]---> Adder-cost: 11   maxlim: 31   bits: 6/5
c ---[1044]---> Adder-cost: 10   maxlim: 31   bits: 6/5
c ---[1043]---> Adder-cost: 19   maxlim: 30   bits: 6/5
c ---[1042]---> Adder-cost: 19   maxlim: 30   bits: 6/5
c ---[1041]---> Adder-cost: 11   maxlim: 31   bits: 6/5
c ---[1040]---> Adder-cost: 10   maxlim: 31   bits: 6/5
c ---[1039]---> Adder-cost: 19   maxlim: 30   bits: 6/5
c ---[1038]---> Adder-cost: 19   maxlim: 30   bits: 6/5
c ---[1037]---> Adder-cost: 11   maxlim: 31   bits: 6/5
c ---[1036]---> Adder-cost: 10   maxlim: 31   bits: 6/5
c ---[1035]---> Adder-cost: 19   maxlim: 30   bits: 6/5
c ---[1034]---> Adder-cost: 19   maxlim: 30   bits: 6/5
c ---[1033]---> Adder-cost: 11   maxlim: 31   bits: 6/5
c ---[1032]---> Adder-cost: 10   maxlim: 31   bits: 6/5
c ---[1031]---> Adder-cost: 19   maxlim: 30   bits: 6/5
c ---[1030]---> Adder-cost: 19   maxlim: 30   bits: 6/5
c ---[1029]---> Adder-cost: 11   maxlim: 31   bits: 6/5
c ---[1028]---> Adder-cost: 10   maxlim: 31   bits: 6/5
c ---[1027]---> Adder-cost: 19   maxlim: 30   bits: 6/5
c ---[1026]---> Adder-cost: 19   maxlim: 30   bits: 6/5
c ---[1025]---> Adder-cost: 11   maxlim: 31   bits: 6/5
c ---[1024]---> Adder-cost: 10   maxlim: 31   bits: 6/5
c ---[1023]---> Adder-cost: 19   maxlim: 30   bits: 6/5
c ---[1022]---> Adder-cost: 19   maxlim: 30   bits: 6/5
c ---[1021]---> Adder-cost: 11   maxlim: 31   bits: 6/5
c ---[1020]---> Adder-cost: 10   maxlim: 31   bits: 6/5
c ---[1019]---> Adder-cost: 19   maxlim: 30   bits: 6/5
c ---[1018]---> Adder-cost: 19   maxlim: 30   bits: 6/5
c ---[1017]---> Adder-cost: 11   maxlim: 31   bits: 6/5
c ---[1016]---> Adder-cost: 10   maxlim: 31   bits: 6/5
c ---[1015]---> Adder-cost: 19   maxlim: 30   bits: 6/5
c ---[1014]---> Adder-cost: 19   maxlim: 30   bits: 6/5
c ---[1013]---> Adder-cost: 11   maxlim: 31   bits: 6/5
c ---[1012]---> Adder-cost: 10   maxlim: 31   bits: 6/5
c ---[1011]---> Adder-cost: 19   maxlim: 30   bits: 6/5
c ---[1010]---> Adder-cost: 19   maxlim: 30   bits: 6/5
c ---[1009]---> Adder-cost: 11   maxlim: 31   bits: 6/5
c ---[1008]---> Adder-cost: 10   maxlim: 31   bits: 6/5
c ---[1007]---> Adder-cost: 19   maxlim: 30   bits: 6/5
c ---[1006]---> Adder-cost: 19   maxlim: 30   bits: 6/5
c ---[1005]---> Adder-cost: 11   maxlim: 31   bits: 6/5
c ---[1004]---> Adder-cost: 10   maxlim: 31   bits: 6/5
c ---[1003]---> Adder-cost: 19   maxlim: 30   bits: 6/5
c ---[1002]---> Adder-cost: 19   maxlim: 30   bits: 6/5
c ---[1001]---> Adder-cost: 11   maxlim: 31   bits: 6/5
c ---[1000]---> Adder-cost: 10   maxlim: 31   bits: 6/5
c ---[ 999]---> Adder-cost: 19   maxlim: 30   bits: 6/5
c ---[ 998]---> Adder-cost: 19   maxlim: 30   bits: 6/5
c ---[ 997]---> Adder-cost: 11   maxlim: 31   bits: 6/5
c ---[ 996]---> Adder-cost: 10   maxlim: 31   bits: 6/5
c ---[ 995]---> Adder-cost: 19   maxlim: 30   bits: 6/5
c ---[ 994]---> Adder-cost: 19   maxlim: 30   bits: 6/5
c ---[ 993]---> Adder-cost: 11   maxlim: 31   bits: 6/5
c ---[ 992]---> Adder-cost: 10   maxlim: 31   bits: 6/5
c ---[ 991]---> Adder-cost: 19   maxlim: 30   bits: 6/5
c ---[ 990]---> Adder-cost: 19   maxlim: 30   bits: 6/5
c ---[ 989]---> Adder-cost: 11   maxlim: 31   bits: 6/5
c ---[ 988]---> Adder-cost: 10   maxlim: 31   bits: 6/5
c ---[ 987]---> Adder-cost: 19   maxlim: 30   bits: 6/5
c ---[ 986]---> Adder-cost: 19   maxlim: 30   bits: 6/5
c ---[ 985]---> Adder-cost: 11   maxlim: 31   bits: 6/5
c ---[ 984]---> Adder-cost: 10   maxlim: 31   bits: 6/5
c ---[ 983]---> Adder-cost: 13   maxlim: 27   bits: 6/5
c ---[ 982]---> Adder-cost: 18   maxlim: 33   bits: 7/6
c ---[ 981]---> Adder-cost: 20   maxlim: 34   bits: 7/6
c ---[ 980]---> Adder-cost: 17   maxlim: 28   bits: 6/5
c ---[ 979]---> Adder-cost: 13   maxlim: 27   bits: 6/5
c ---[ 978]---> Adder-cost: 18   maxlim: 33   bits: 7/6
c ---[ 977]---> Adder-cost: 20   maxlim: 34   bits: 7/6
c ---[ 976]---> Adder-cost: 17   maxlim: 28   bits: 6/5
c ---[ 975]---> Adder-cost: 13   maxlim: 27   bits: 6/5
c ---[ 974]---> Adder-cost: 18   maxlim: 33   bits: 7/6
c ---[ 973]---> Adder-cost: 20   maxlim: 34   bits: 7/6
c ---[ 972]---> Adder-cost: 17   maxlim: 28   bits: 6/5
c ---[ 971]---> Adder-cost: 19   maxlim: 26   bits: 6/5
c ---[ 970]---> Adder-cost: 20   maxlim: 34   bits: 7/6
c ---[ 969]---> Adder-cost: 18   maxlim: 35   bits: 7/6
c ---[ 968]---> Adder-cost: 16   maxlim: 27   bits: 6/5
c ---[ 967]---> Adder-cost: 13   maxlim: 27   bits: 6/5
c ---[ 966]---> Adder-cost: 18   maxlim: 33   bits: 7/6
c ---[ 965]---> Adder-cost: 20   maxlim: 34   bits: 7/6
c ---[ 964]---> Adder-cost: 17   maxlim: 28   bits: 6/5
c ---[ 963]---> Adder-cost: 17   maxlim: 28   bits: 6/5
c ---[ 962]---> Adder-cost: 12   maxlim: 32   bits: 7/6
c ---[ 961]---> Adder-cost: 18   maxlim: 33   bits: 7/6
c ---[ 960]---> Adder-cost: 17   maxlim: 29   bits: 6/5
c ---[ 959]---> Adder-cost: 17   maxlim: 29   bits: 6/5
c ---[ 958]---> Adder-cost: 7   maxlim: 31   bits: 6/5
c ---[ 957]---> Adder-cost: 12   maxlim: 32   bits: 7/6
c ---[ 956]---> Adder-cost: 19   maxlim: 30   bits: 6/5
c ---[ 955]---> Adder-cost: 19   maxlim: 30   bits: 6/5
c ---[ 954]---> Adder-cost: 19   maxlim: 30   bits: 6/5
c ---[ 953]---> Adder-cost: 1   maxlim: 31   bits: 6/5
c ---[ 952]---> Adder-cost: 7   maxlim: 31   bits: 6/5
c ---[ 951]---> Adder-cost: 19   maxlim: 30   bits: 6/5
c ---[ 950]---> Adder-cost: 19   maxlim: 30   bits: 6/5
c ---[ 949]---> Adder-cost: 11   maxlim: 31   bits: 6/5
c ---[ 948]---> Adder-cost: 10   maxlim: 31   bits: 6/5
c ---[ 947]---> Adder-cost: 19   maxlim: 30   bits: 6/5
c ---[ 946]---> Adder-cost: 19   maxlim: 30   bits: 6/5
c ---[ 945]---> Adder-cost: 11   maxlim: 31   bits: 6/5
c ---[ 944]---> Adder-cost: 10   maxlim: 31   bits: 6/5
c ---[ 943]---> Adder-cost: 19   maxlim: 30   bits: 6/5
c ---[ 942]---> Adder-cost: 19   maxlim: 30   bits: 6/5
c ---[ 941]---> Adder-cost: 11   maxlim: 31   bits: 6/5
c ---[ 940]---> Adder-cost: 10   maxlim: 31   bits: 6/5
c ---[ 939]---> Adder-cost: 19   maxlim: 30   bits: 6/5
c ---[ 938]---> Adder-cost: 19   maxlim: 30   bits: 6/5
c ---[ 937]---> Adder-cost: 11   maxlim: 31   bits: 6/5
c ---[ 936]---> Adder-cost: 10   maxlim: 31   bits: 6/5
c ---[ 935]---> Adder-cost: 19   maxlim: 30   bits: 6/5
c ---[ 934]---> Adder-cost: 19   maxlim: 30   bits: 6/5
c ---[ 933]---> Adder-cost: 11   maxlim: 31   bits: 6/5
c ---[ 932]---> Adder-cost: 10   maxlim: 31   bits: 6/5
c ---[ 931]---> Adder-cost: 19   maxlim: 30   bits: 6/5
c ---[ 930]---> Adder-cost: 19   maxlim: 30   bits: 6/5
c ---[ 929]---> Adder-cost: 11   maxlim: 31   bits: 6/5
c ---[ 928]---> Adder-cost: 10   maxlim: 31   bits: 6/5
c ---[ 927]---> Adder-cost: 19   maxlim: 30   bits: 6/5
c ---[ 926]---> Adder-cost: 19   maxlim: 30   bits: 6/5
c ---[ 925]---> Adder-cost: 11   maxlim: 31   bits: 6/5
c ---[ 924]---> Adder-cost: 10   maxlim: 31   bits: 6/5
c ---[ 923]---> Adder-cost: 19   maxlim: 30   bits: 6/5
c ---[ 922]---> Adder-cost: 19   maxlim: 30   bits: 6/5
c ---[ 921]---> Adder-cost: 11   maxlim: 31   bits: 6/5
c ---[ 920]---> Adder-cost: 10   maxlim: 31   bits: 6/5
c ---[ 919]---> Adder-cost: 19   maxlim: 30   bits: 6/5
c ---[ 918]---> Adder-cost: 19   maxlim: 30   bits: 6/5
c ---[ 917]---> Adder-cost: 11   maxlim: 31   bits: 6/5
c ---[ 916]---> Adder-cost: 10   maxlim: 31   bits: 6/5
c ---[ 915]---> Adder-cost: 19   maxlim: 30   bits: 6/5
c ---[ 914]---> Adder-cost: 19   maxlim: 30   bits: 6/5
c ---[ 913]---> Adder-cost: 11   maxlim: 31   bits: 6/5
c ---[ 912]---> Adder-cost: 10   maxlim: 31   bits: 6/5
c ---[ 911]---> Adder-cost: 19   maxlim: 30   bits: 6/5
c ---[ 910]---> Adder-cost: 19   maxlim: 30   bits: 6/5
c ---[ 909]---> Adder-cost: 11   maxlim: 31   bits: 6/5
c ---[ 908]---> Adder-cost: 10   maxlim: 31   bits: 6/5
c ---[ 907]---> Adder-cost: 19   maxlim: 30   bits: 6/5
c ---[ 906]---> Adder-cost: 19   maxlim: 30   bits: 6/5
c ---[ 905]---> Adder-cost: 11   maxlim: 31   bits: 6/5
c ---[ 904]---> Adder-cost: 10   maxlim: 31   bits: 6/5
c ---[ 903]---> Adder-cost: 19   maxlim: 30   bits: 6/5
c ---[ 902]---> Adder-cost: 19   maxlim: 30   bits: 6/5
c ---[ 901]---> Adder-cost: 11   maxlim: 31   bits: 6/5
c ---[ 900]---> Adder-cost: 10   maxlim: 31   bits: 6/5
c ---[ 899]---> Adder-cost: 19   maxlim: 30   bits: 6/5
c ---[ 898]---> Adder-cost: 19   maxlim: 30   bits: 6/5
c ---[ 897]---> Adder-cost: 11   maxlim: 31   bits: 6/5
c ---[ 896]---> Adder-cost: 10   maxlim: 31   bits: 6/5
c ---[ 895]---> Adder-cost: 19   maxlim: 30   bits: 6/5
c ---[ 894]---> Adder-cost: 19   maxlim: 30   bits: 6/5
c ---[ 893]---> Adder-cost: 11   maxlim: 31   bits: 6/5
c ---[ 892]---> Adder-cost: 10   maxlim: 31   bits: 6/5
c ---[ 891]---> Adder-cost: 19   maxlim: 30   bits: 6/5
c ---[ 890]---> Adder-cost: 19   maxlim: 30   bits: 6/5
c ---[ 889]---> Adder-cost: 11   maxlim: 31   bits: 6/5
c ---[ 888]---> Adder-cost: 10   maxlim: 31   bits: 6/5
c ---[ 887]---> Adder-cost: 19   maxlim: 30   bits: 6/5
c ---[ 886]---> Adder-cost: 19   maxlim: 30   bits: 6/5
c ---[ 885]---> Adder-cost: 11   maxlim: 31   bits: 6/5
c ---[ 884]---> Adder-cost: 10   maxlim: 31   bits: 6/5
c ---[ 883]---> Adder-cost: 19   maxlim: 30   bits: 6/5
c ---[ 882]---> Adder-cost: 19   maxlim: 30   bits: 6/5
c ---[ 881]---> Adder-cost: 11   maxlim: 31   bits: 6/5
c ---[ 880]---> Adder-cost: 10   maxlim: 31   bits: 6/5
c ---[ 879]---> Adder-cost: 19   maxlim: 30   bits: 6/5
c ---[ 878]---> Adder-cost: 19   maxlim: 30   bits: 6/5
c ---[ 877]---> Adder-cost: 11   maxlim: 31   bits: 6/5
c ---[ 876]---> Adder-cost: 10   maxlim: 31   bits: 6/5
c ---[ 875]---> Adder-cost: 19   maxlim: 30   bits: 6/5
c ---[ 874]---> Adder-cost: 19   maxlim: 30   bits: 6/5
c ---[ 873]---> Adder-cost: 11   maxlim: 31   bits: 6/5
c ---[ 872]---> Adder-cost: 10   maxlim: 31   bits: 6/5
c ---[ 871]---> Adder-cost: 19   maxlim: 30   bits: 6/5
c ---[ 870]---> Adder-cost: 19   maxlim: 30   bits: 6/5
c ---[ 869]---> Adder-cost: 11   maxlim: 31   bits: 6/5
c ---[ 868]---> Adder-cost: 10   maxlim: 31   bits: 6/5
c ---[ 867]---> Adder-cost: 19   maxlim: 26   bits: 6/5
c ---[ 866]---> Adder-cost: 20   maxlim: 34   bits: 7/6
c ---[ 865]---> Adder-cost: 14   maxlim: 35   bits: 7/6
c ---[ 864]---> Adder-cost: 13   maxlim: 27   bits: 6/5
c ---[ 863]---> Adder-cost: 19   maxlim: 26   bits: 6/5
c ---[ 862]---> Adder-cost: 20   maxlim: 34   bits: 7/6
c ---[ 861]---> Adder-cost: 14   maxlim: 35   bits: 7/6
c ---[ 860]---> Adder-cost: 13   maxlim: 27   bits: 6/5
c ---[ 859]---> Adder-cost: 19   maxlim: 26   bits: 6/5
c ---[ 858]---> Adder-cost: 20   maxlim: 34   bits: 7/6
c ---[ 857]---> Adder-cost: 14   maxlim: 35   bits: 7/6
c ---[ 856]---> Adder-cost: 13   maxlim: 27   bits: 6/5
c ---[ 855]---> Adder-cost: 19   maxlim: 26   bits: 6/5
c ---[ 854]---> Adder-cost: 20   maxlim: 34   bits: 7/6
c ---[ 853]---> Adder-cost: 14   maxlim: 35   bits: 7/6
c ---[ 852]---> Adder-cost: 13   maxlim: 27   bits: 6/5
c ---[ 851]---> Adder-cost: 19   maxlim: 25   bits: 6/5
c ---[ 850]---> Adder-cost: 17   maxlim: 35   bits: 7/6
c ---[ 849]---> Adder-cost: 18   maxlim: 36   bits: 7/6
c ---[ 848]---> Adder-cost: 19   maxlim: 26   bits: 6/5
c ---[ 847]---> Adder-cost: 19   maxlim: 26   bits: 6/5
c ---[ 846]---> Adder-cost: 20   maxlim: 34   bits: 7/6
c ---[ 845]---> Adder-cost: 14   maxlim: 35   bits: 7/6
c ---[ 844]---> Adder-cost: 15   maxlim: 27   bits: 6/5
c ---[ 843]---> Adder-cost: 13   maxlim: 27   bits: 6/5
c ---[ 842]---> Adder-cost: 18   maxlim: 33   bits: 7/6
c ---[ 841]---> Adder-cost: 20   maxlim: 34   bits: 7/6
c ---[ 840]---> Adder-cost: 17   maxlim: 28   bits: 6/5
c ---[ 839]---> Adder-cost: 17   maxlim: 28   bits: 6/5
c ---[ 838]---> Adder-cost: 12   maxlim: 32   bits: 7/6
c ---[ 837]---> Adder-cost: 18   maxlim: 33   bits: 7/6
c ---[ 836]---> Adder-cost: 17   maxlim: 29   bits: 6/5
c ---[ 835]---> Adder-cost: 17   maxlim: 29   bits: 6/5
c ---[ 834]---> Adder-cost: 7   maxlim: 31   bits: 6/5
c ---[ 833]---> Adder-cost: 12   maxlim: 32   bits: 7/6
c ---[ 832]---> Adder-cost: 19   maxlim: 30   bits: 6/5
c ---[ 831]---> Adder-cost: 19   maxlim: 30   bits: 6/5
c ---[ 830]---> Adder-cost: 19   maxlim: 30   bits: 6/5
c ---[ 829]---> Adder-cost: 1   maxlim: 31   bits: 6/5
c ---[ 828]---> Adder-cost: 7   maxlim: 31   bits: 6/5
c ---[ 827]---> Adder-cost: 19   maxlim: 30   bits: 6/5
c ---[ 826]---> Adder-cost: 19   maxlim: 30   bits: 6/5
c ---[ 825]---> Adder-cost: 11   maxlim: 31   bits: 6/5
c ---[ 824]---> Adder-cost: 10   maxlim: 31   bits: 6/5
c ---[ 823]---> Adder-cost: 19   maxlim: 30   bits: 6/5
c ---[ 822]---> Adder-cost: 19   maxlim: 30   bits: 6/5
c ---[ 821]---> Adder-cost: 11   maxlim: 31   bits: 6/5
c ---[ 820]---> Adder-cost: 10   maxlim: 31   bits: 6/5
c ---[ 819]---> Adder-cost: 19   maxlim: 30   bits: 6/5
c ---[ 818]---> Adder-cost: 19   maxlim: 30   bits: 6/5
c ---[ 817]---> Adder-cost: 11   maxlim: 31   bits: 6/5
c ---[ 816]---> Adder-cost: 10   maxlim: 31   bits: 6/5
c ---[ 815]---> Adder-cost: 19   maxlim: 30   bits: 6/5
c ---[ 814]---> Adder-cost: 19   maxlim: 30   bits: 6/5
c ---[ 813]---> Adder-cost: 11   maxlim: 31   bits: 6/5
c ---[ 812]---> Adder-cost: 10   maxlim: 31   bits: 6/5
c ---[ 811]---> Adder-cost: 19   maxlim: 30   bits: 6/5
c ---[ 810]---> Adder-cost: 19   maxlim: 30   bits: 6/5
c ---[ 809]---> Adder-cost: 11   maxlim: 31   bits: 6/5
c ---[ 808]---> Adder-cost: 10   maxlim: 31   bits: 6/5
c ---[ 807]---> Adder-cost: 19   maxlim: 30   bits: 6/5
c ---[ 806]---> Adder-cost: 19   maxlim: 30   bits: 6/5
c ---[ 805]---> Adder-cost: 11   maxlim: 31   bits: 6/5
c ---[ 804]---> Adder-cost: 10   maxlim: 31   bits: 6/5
c ---[ 803]---> Adder-cost: 19   maxlim: 30   bits: 6/5
c ---[ 802]---> Adder-cost: 19   maxlim: 30   bits: 6/5
c ---[ 801]---> Adder-cost: 11   maxlim: 31   bits: 6/5
c ---[ 800]---> Adder-cost: 10   maxlim: 31   bits: 6/5
c ---[ 799]---> Adder-cost: 19   maxlim: 30   bits: 6/5
c ---[ 798]---> Adder-cost: 19   maxlim: 30   bits: 6/5
c ---[ 797]---> Adder-cost: 11   maxlim: 31   bits: 6/5
c ---[ 796]---> Adder-cost: 10   maxlim: 31   bits: 6/5
c ---[ 795]---> Adder-cost: 19   maxlim: 30   bits: 6/5
c ---[ 794]---> Adder-cost: 19   maxlim: 30   bits: 6/5
c ---[ 793]---> Adder-cost: 11   maxlim: 31   bits: 6/5
c ---[ 792]---> Adder-cost: 10   maxlim: 31   bits: 6/5
c ---[ 791]---> Adder-cost: 19   maxlim: 30   bits: 6/5
c ---[ 790]---> Adder-cost: 19   maxlim: 30   bits: 6/5
c ---[ 789]---> Adder-cost: 11   maxlim: 31   bits: 6/5
c ---[ 788]---> Adder-cost: 10   maxlim: 31   bits: 6/5
c ---[ 787]---> Adder-cost: 19   maxlim: 30   bits: 6/5
c ---[ 786]---> Adder-cost: 19   maxlim: 30   bits: 6/5
c ---[ 785]---> Adder-cost: 11   maxlim: 31   bits: 6/5
c ---[ 784]---> Adder-cost: 10   maxlim: 31   bits: 6/5
c ---[ 783]---> Adder-cost: 19   maxlim: 30   bits: 6/5
c ---[ 782]---> Adder-cost: 19   maxlim: 30   bits: 6/5
c ---[ 781]---> Adder-cost: 11   maxlim: 31   bits: 6/5
c ---[ 780]---> Adder-cost: 10   maxlim: 31   bits: 6/5
c ---[ 779]---> Adder-cost: 19   maxlim: 30   bits: 6/5
c ---[ 778]---> Adder-cost: 19   maxlim: 30   bits: 6/5
c ---[ 777]---> Adder-cost: 11   maxlim: 31   bits: 6/5
c ---[ 776]---> Adder-cost: 10   maxlim: 31   bits: 6/5
c ---[ 775]---> Adder-cost: 19   maxlim: 30   bits: 6/5
c ---[ 774]---> Adder-cost: 19   maxlim: 30   bits: 6/5
c ---[ 773]---> Adder-cost: 11   maxlim: 31   bits: 6/5
c ---[ 772]---> Adder-cost: 10   maxlim: 31   bits: 6/5
c ---[ 771]---> Adder-cost: 19   maxlim: 30   bits: 6/5
c ---[ 770]---> Adder-cost: 19   maxlim: 30   bits: 6/5
c ---[ 769]---> Adder-cost: 11   maxlim: 31   bits: 6/5
c ---[ 768]---> Adder-cost: 10   maxlim: 31   bits: 6/5
c ---[ 767]---> Adder-cost: 19   maxlim: 30   bits: 6/5
c ---[ 766]---> Adder-cost: 19   maxlim: 30   bits: 6/5
c ---[ 765]---> Adder-cost: 11   maxlim: 31   bits: 6/5
c ---[ 764]---> Adder-cost: 10   maxlim: 31   bits: 6/5
c ---[ 763]---> Adder-cost: 19   maxlim: 30   bits: 6/5
c ---[ 762]---> Adder-cost: 19   maxlim: 30   bits: 6/5
c ---[ 761]---> Adder-cost: 11   maxlim: 31   bits: 6/5
c ---[ 760]---> Adder-cost: 10   maxlim: 31   bits: 6/5
c ---[ 759]---> Adder-cost: 19   maxlim: 30   bits: 6/5
c ---[ 758]---> Adder-cost: 19   maxlim: 30   bits: 6/5
c ---[ 757]---> Adder-cost: 11   maxlim: 31   bits: 6/5
c ---[ 756]---> Adder-cost: 10   maxlim: 31   bits: 6/5
c ---[ 755]---> Adder-cost: 19   maxlim: 30   bits: 6/5
c ---[ 754]---> Adder-cost: 19   maxlim: 30   bits: 6/5
c ---[ 753]---> Adder-cost: 11   maxlim: 31   bits: 6/5
c ---[ 752]---> Adder-cost: 10   maxlim: 31   bits: 6/5
c ---[ 751]---> Adder-cost: 19   maxlim: 30   bits: 6/5
c ---[ 750]---> Adder-cost: 19   maxlim: 30   bits: 6/5
c ---[ 749]---> Adder-cost: 11   maxlim: 31   bits: 6/5
c ---[ 748]---> Adder-cost: 10   maxlim: 31   bits: 6/5
c ---[ 747]---> Adder-cost: 19   maxlim: 30   bits: 6/5
c ---[ 746]---> Adder-cost: 19   maxlim: 30   bits: 6/5
c ---[ 745]---> Adder-cost: 11   maxlim: 31   bits: 6/5
c ---[ 744]---> Adder-cost: 10   maxlim: 31   bits: 6/5
c ---[ 743]---> Adder-cost: 19   maxlim: 30   bits: 6/5
c ---[ 742]---> Adder-cost: 19   maxlim: 30   bits: 6/5
c ---[ 741]---> Adder-cost: 11   maxlim: 31   bits: 6/5
c ---[ 740]---> Adder-cost: 10   maxlim: 31   bits: 6/5
c ---[ 739]---> Adder-cost: 19   maxlim: 30   bits: 6/5
c ---[ 738]---> Adder-cost: 19   maxlim: 30   bits: 6/5
c ---[ 737]---> Adder-cost: 11   maxlim: 31   bits: 6/5
c ---[ 736]---> Adder-cost: 10   maxlim: 31   bits: 6/5
c ---[ 735]---> Adder-cost: 19   maxlim: 30   bits: 6/5
c ---[ 734]---> Adder-cost: 19   maxlim: 30   bits: 6/5
c ---[ 733]---> Adder-cost: 11   maxlim: 31   bits: 6/5
c ---[ 732]---> Adder-cost: 10   maxlim: 31   bits: 6/5
c ---[ 731]---> Adder-cost: 19   maxlim: 30   bits: 6/5
c ---[ 730]---> Adder-cost: 19   maxlim: 30   bits: 6/5
c ---[ 729]---> Adder-cost: 11   maxlim: 31   bits: 6/5
c ---[ 728]---> Adder-cost: 10   maxlim: 31   bits: 6/5
c ---[ 727]---> Adder-cost: 19   maxlim: 30   bits: 6/5
c ---[ 726]---> Adder-cost: 19   maxlim: 30   bits: 6/5
c ---[ 725]---> Adder-cost: 11   maxlim: 31   bits: 6/5
c ---[ 724]---> Adder-cost: 10   maxlim: 31   bits: 6/5
c ---[ 723]---> Adder-cost: 17   maxlim: 25   bits: 6/5
c ---[ 722]---> Adder-cost: 14   maxlim: 35   bits: 7/6
c ---[ 721]---> Adder-cost: 18   maxlim: 36   bits: 7/6
c ---[ 720]---> Adder-cost: 19   maxlim: 26   bits: 6/5
c ---[ 719]---> Adder-cost: 17   maxlim: 25   bits: 6/5
c ---[ 718]---> Adder-cost: 14   maxlim: 35   bits: 7/6
c ---[ 717]---> Adder-cost: 18   maxlim: 36   bits: 7/6
c ---[ 716]---> Adder-cost: 19   maxlim: 26   bits: 6/5
c ---[ 715]---> Adder-cost: 17   maxlim: 25   bits: 6/5
c ---[ 714]---> Adder-cost: 14   maxlim: 35   bits: 7/6
c ---[ 713]---> Adder-cost: 18   maxlim: 36   bits: 7/6
c ---[ 712]---> Adder-cost: 19   maxlim: 26   bits: 6/5
c ---[ 711]---> Adder-cost: 17   maxlim: 25   bits: 6/5
c ---[ 710]---> Adder-cost: 14   maxlim: 35   bits: 7/6
c ---[ 709]---> Adder-cost: 18   maxlim: 36   bits: 7/6
c ---[ 708]---> Adder-cost: 19   maxlim: 26   bits: 6/5
c ---[ 707]---> Adder-cost: 17   maxlim: 25   bits: 6/5
c ---[ 706]---> Adder-cost: 14   maxlim: 35   bits: 7/6
c ---[ 705]---> Adder-cost: 18   maxlim: 36   bits: 7/6
c ---[ 704]---> Adder-cost: 19   maxlim: 26   bits: 6/5
c ---[ 703]---> Adder-cost: 15   maxlim: 24   bits: 6/5
c ---[ 702]---> Adder-cost: 18   maxlim: 36   bits: 7/6
c ---[ 701]---> Adder-cost: 20   maxlim: 37   bits: 7/6
c ---[ 700]---> Adder-cost: 18   maxlim: 25   bits: 6/5
c ---[ 699]---> Adder-cost: 17   maxlim: 25   bits: 6/5
c ---[ 698]---> Adder-cost: 16   maxlim: 35   bits: 7/6
c ---[ 697]---> Adder-cost: 18   maxlim: 36   bits: 7/6
c ---[ 696]---> Adder-cost: 19   maxlim: 26   bits: 6/5
c ---[ 695]---> Adder-cost: 19   maxlim: 26   bits: 6/5
c ---[ 694]---> Adder-cost: 20   maxlim: 34   bits: 7/6
c ---[ 693]---> Adder-cost: 14   maxlim: 35   bits: 7/6
c ---[ 692]---> Adder-cost: 15   maxlim: 27   bits: 6/5
c ---[ 691]---> Adder-cost: 13   maxlim: 27   bits: 6/5
c ---[ 690]---> Adder-cost: 18   maxlim: 33   bits: 7/6
c ---[ 689]---> Adder-cost: 20   maxlim: 34   bits: 7/6
c ---[ 688]---> Adder-cost: 17   maxlim: 28   bits: 6/5
c ---[ 687]---> Adder-cost: 17   maxlim: 28   bits: 6/5
c ---[ 686]---> Adder-cost: 12   maxlim: 32   bits: 7/6
c ---[ 685]---> Adder-cost: 18   maxlim: 33   bits: 7/6
c ---[ 684]---> Adder-cost: 17   maxlim: 29   bits: 6/5
c ---[ 683]---> Adder-cost: 17   maxlim: 29   bits: 6/5
c ---[ 682]---> Adder-cost: 7   maxlim: 31   bits: 6/5
c ---[ 681]---> Adder-cost: 12   maxlim: 32   bits: 7/6
c ---[ 680]---> Adder-cost: 19   maxlim: 30   bits: 6/5
c ---[ 679]---> Adder-cost: 19   maxlim: 30   bits: 6/5
c ---[ 678]---> Adder-cost: 19   maxlim: 30   bits: 6/5
c ---[ 677]---> Adder-cost: 1   maxlim: 31   bits: 6/5
c ---[ 676]---> Adder-cost: 7   maxlim: 31   bits: 6/5
c ---[ 675]---> Adder-cost: 19   maxlim: 30   bits: 6/5
c ---[ 674]---> Adder-cost: 19   maxlim: 30   bits: 6/5
c ---[ 673]---> Adder-cost: 11   maxlim: 31   bits: 6/5
c ---[ 672]---> Adder-cost: 10   maxlim: 31   bits: 6/5
c ---[ 671]---> Adder-cost: 19   maxlim: 30   bits: 6/5
c ---[ 670]---> Adder-cost: 19   maxlim: 30   bits: 6/5
c ---[ 669]---> Adder-cost: 11   maxlim: 31   bits: 6/5
c ---[ 668]---> Adder-cost: 10   maxlim: 31   bits: 6/5
c ---[ 667]---> Adder-cost: 19   maxlim: 30   bits: 6/5
c ---[ 666]---> Adder-cost: 19   maxlim: 30   bits: 6/5
c ---[ 665]---> Adder-cost: 11   maxlim: 31   bits: 6/5
c ---[ 664]---> Adder-cost: 10   maxlim: 31   bits: 6/5
c ---[ 663]---> Adder-cost: 19   maxlim: 30   bits: 6/5
c ---[ 662]---> Adder-cost: 19   maxlim: 30   bits: 6/5
c ---[ 661]---> Adder-cost: 11   maxlim: 31   bits: 6/5
c ---[ 660]---> Adder-cost: 10   maxlim: 31   bits: 6/5
c ---[ 659]---> Adder-cost: 19   maxlim: 30   bits: 6/5
c ---[ 658]---> Adder-cost: 19   maxlim: 30   bits: 6/5
c ---[ 657]---> Adder-cost: 11   maxlim: 31   bits: 6/5
c ---[ 656]---> Adder-cost: 10   maxlim: 31   bits: 6/5
c ---[ 655]---> Adder-cost: 19   maxlim: 30   bits: 6/5
c ---[ 654]---> Adder-cost: 19   maxlim: 30   bits: 6/5
c ---[ 653]---> Adder-cost: 11   maxlim: 31   bits: 6/5
c ---[ 652]---> Adder-cost: 10   maxlim: 31   bits: 6/5
c ---[ 651]---> Adder-cost: 19   maxlim: 30   bits: 6/5
c ---[ 650]---> Adder-cost: 19   maxlim: 30   bits: 6/5
c ---[ 649]---> Adder-cost: 11   maxlim: 31   bits: 6/5
c ---[ 648]---> Adder-cost: 10   maxlim: 31   bits: 6/5
c ---[ 647]---> Adder-cost: 19   maxlim: 30   bits: 6/5
c ---[ 646]---> Adder-cost: 19   maxlim: 30   bits: 6/5
c ---[ 645]---> Adder-cost: 11   maxlim: 31   bits: 6/5
c ---[ 644]---> Adder-cost: 10   maxlim: 31   bits: 6/5
c ---[ 643]---> Adder-cost: 19   maxlim: 30   bits: 6/5
c ---[ 642]---> Adder-cost: 19   maxlim: 30   bits: 6/5
c ---[ 641]---> Adder-cost: 11   maxlim: 31   bits: 6/5
c ---[ 640]---> Adder-cost: 10   maxlim: 31   bits: 6/5
c ---[ 639]---> Adder-cost: 19   maxlim: 30   bits: 6/5
c ---[ 638]---> Adder-cost: 19   maxlim: 30   bits: 6/5
c ---[ 637]---> Adder-cost: 11   maxlim: 31   bits: 6/5
c ---[ 636]---> Adder-cost: 10   maxlim: 31   bits: 6/5
c ---[ 635]---> Adder-cost: 19   maxlim: 30   bits: 6/5
c ---[ 634]---> Adder-cost: 19   maxlim: 30   bits: 6/5
c ---[ 633]---> Adder-cost: 11   maxlim: 31   bits: 6/5
c ---[ 632]---> Adder-cost: 10   maxlim: 31   bits: 6/5
c ---[ 631]---> Adder-cost: 19   maxlim: 30   bits: 6/5
c ---[ 630]---> Adder-cost: 19   maxlim: 30   bits: 6/5
c ---[ 629]---> Adder-cost: 11   maxlim: 31   bits: 6/5
c ---[ 628]---> Adder-cost: 10   maxlim: 31   bits: 6/5
c ---[ 627]---> Adder-cost: 19   maxlim: 30   bits: 6/5
c ---[ 626]---> Adder-cost: 19   maxlim: 30   bits: 6/5
c ---[ 625]---> Adder-cost: 11   maxlim: 31   bits: 6/5
c ---[ 624]---> Adder-cost: 10   maxlim: 31   bits: 6/5
c ---[ 623]---> Adder-cost: 19   maxlim: 30   bits: 6/5
c ---[ 622]---> Adder-cost: 19   maxlim: 30   bits: 6/5
c ---[ 621]---> Adder-cost: 11   maxlim: 31   bits: 6/5
c ---[ 620]---> Adder-cost: 10   maxlim: 31   bits: 6/5
c ---[ 619]---> Adder-cost: 19   maxlim: 30   bits: 6/5
c ---[ 618]---> Adder-cost: 19   maxlim: 30   bits: 6/5
c ---[ 617]---> Adder-cost: 11   maxlim: 31   bits: 6/5
c ---[ 616]---> Adder-cost: 10   maxlim: 31   bits: 6/5
c ---[ 615]---> Adder-cost: 19   maxlim: 30   bits: 6/5
c ---[ 614]---> Adder-cost: 19   maxlim: 30   bits: 6/5
c ---[ 613]---> Adder-cost: 11   maxlim: 31   bits: 6/5
c ---[ 612]---> Adder-cost: 10   maxlim: 31   bits: 6/5
c ---[ 611]---> Adder-cost: 19   maxlim: 30   bits: 6/5
c ---[ 610]---> Adder-cost: 19   maxlim: 30   bits: 6/5
c ---[ 609]---> Adder-cost: 11   maxlim: 31   bits: 6/5
c ---[ 608]---> Adder-cost: 10   maxlim: 31   bits: 6/5
c ---[ 607]---> Adder-cost: 19   maxlim: 30   bits: 6/5
c ---[ 606]---> Adder-cost: 19   maxlim: 30   bits: 6/5
c ---[ 605]---> Adder-cost: 11   maxlim: 31   bits: 6/5
c ---[ 604]---> Adder-cost: 10   maxlim: 31   bits: 6/5
c ---[ 603]---> Adder-cost: 19   maxlim: 30   bits: 6/5
c ---[ 602]---> Adder-cost: 19   maxlim: 30   bits: 6/5
c ---[ 601]---> Adder-cost: 11   maxlim: 31   bits: 6/5
c ---[ 600]---> Adder-cost: 10   maxlim: 31   bits: 6/5
c ---[ 599]---> Adder-cost: 19   maxlim: 30   bits: 6/5
c ---[ 598]---> Adder-cost: 19   maxlim: 30   bits: 6/5
c ---[ 597]---> Adder-cost: 11   maxlim: 31   bits: 6/5
c ---[ 596]---> Adder-cost: 10   maxlim: 31   bits: 6/5
c ---[ 595]---> Adder-cost: 19   maxlim: 30   bits: 6/5
c ---[ 594]---> Adder-cost: 19   maxlim: 30   bits: 6/5
c ---[ 593]---> Adder-cost: 11   maxlim: 31   bits: 6/5
c ---[ 592]---> Adder-cost: 10   maxlim: 31   bits: 6/5
c ---[ 591]---> Adder-cost: 19   maxlim: 30   bits: 6/5
c ---[ 590]---> Adder-cost: 19   maxlim: 30   bits: 6/5
c ---[ 589]---> Adder-cost: 11   maxlim: 31   bits: 6/5
c ---[ 588]---> Adder-cost: 10   maxlim: 31   bits: 6/5
c ---[ 587]---> Adder-cost: 19   maxlim: 30   bits: 6/5
c ---[ 586]---> Adder-cost: 19   maxlim: 30   bits: 6/5
c ---[ 585]---> Adder-cost: 11   maxlim: 31   bits: 6/5
c ---[ 584]---> Adder-cost: 10   maxlim: 31   bits: 6/5
c ---[ 583]---> Adder-cost: 19   maxlim: 30   bits: 6/5
c ---[ 582]---> Adder-cost: 19   maxlim: 30   bits: 6/5
c ---[ 581]---> Adder-cost: 11   maxlim: 31   bits: 6/5
c ---[ 580]---> Adder-cost: 10   maxlim: 31   bits: 6/5
c ---[ 579]---> Adder-cost: 19   maxlim: 30   bits: 6/5
c ---[ 578]---> Adder-cost: 19   maxlim: 30   bits: 6/5
c ---[ 577]---> Adder-cost: 11   maxlim: 31   bits: 6/5
c ---[ 576]---> Adder-cost: 10   maxlim: 31   bits: 6/5
c ---[ 575]---> Adder-cost: 19   maxlim: 30   bits: 6/5
c ---[ 574]---> Adder-cost: 19   maxlim: 30   bits: 6/5
c ---[ 573]---> Adder-cost: 11   maxlim: 31   bits: 6/5
c ---[ 572]---> Adder-cost: 10   maxlim: 31   bits: 6/5
c ---[ 571]---> Adder-cost: 19   maxlim: 30   bits: 6/5
c ---[ 570]---> Adder-cost: 19   maxlim: 30   bits: 6/5
c ---[ 569]---> Adder-cost: 11   maxlim: 31   bits: 6/5
c ---[ 568]---> Adder-cost: 10   maxlim: 31   bits: 6/5
c ---[ 567]---> Adder-cost: 19   maxlim: 30   bits: 6/5
c ---[ 566]---> Adder-cost: 19   maxlim: 30   bits: 6/5
c ---[ 565]---> Adder-cost: 11   maxlim: 31   bits: 6/5
c ---[ 564]---> Adder-cost: 10   maxlim: 31   bits: 6/5
c ---[ 563]---> Adder-cost: 19   maxlim: 30   bits: 6/5
c ---[ 562]---> Adder-cost: 19   maxlim: 30   bits: 6/5
c ---[ 561]---> Adder-cost: 11   maxlim: 31   bits: 6/5
c ---[ 560]---> Adder-cost: 10   maxlim: 31   bits: 6/5
c ---[ 559]---> Adder-cost: 19   maxlim: 30   bits: 6/5
c ---[ 558]---> Adder-cost: 19   maxlim: 30   bits: 6/5
c ---[ 557]---> Adder-cost: 11   maxlim: 31   bits: 6/5
c ---[ 556]---> Adder-cost: 10   maxlim: 31   bits: 6/5
c ---[ 555]---> Adder-cost: 19   maxlim: 30   bits: 6/5
c ---[ 554]---> Adder-cost: 19   maxlim: 30   bits: 6/5
c ---[ 553]---> Adder-cost: 11   maxlim: 31   bits: 6/5
c ---[ 552]---> Adder-cost: 10   maxlim: 31   bits: 6/5
c ---[ 551]---> Adder-cost: 15   maxlim: 24   bits: 6/5
c ---[ 550]---> Adder-cost: 18   maxlim: 36   bits: 7/6
c ---[ 549]---> Adder-cost: 18   maxlim: 37   bits: 7/6
c ---[ 548]---> Adder-cost: 17   maxlim: 25   bits: 6/5
c ---[ 547]---> Adder-cost: 15   maxlim: 24   bits: 6/5
c ---[ 546]---> Adder-cost: 18   maxlim: 36   bits: 7/6
c ---[ 545]---> Adder-cost: 18   maxlim: 37   bits: 7/6
c ---[ 544]---> Adder-cost: 17   maxlim: 25   bits: 6/5
c ---[ 543]---> Adder-cost: 15   maxlim: 24   bits: 6/5
c ---[ 542]---> Adder-cost: 18   maxlim: 36   bits: 7/6
c ---[ 541]---> Adder-cost: 18   maxlim: 37   bits: 7/6
c ---[ 540]---> Adder-cost: 17   maxlim: 25   bits: 6/5
c ---[ 539]---> Adder-cost: 15   maxlim: 24   bits: 6/5
c ---[ 538]---> Adder-cost: 18   maxlim: 36   bits: 7/6
c ---[ 537]---> Adder-cost: 18   maxlim: 37   bits: 7/6
c ---[ 536]---> Adder-cost: 17   maxlim: 25   bits: 6/5
c ---[ 535]---> Adder-cost: 15   maxlim: 24   bits: 6/5
c ---[ 534]---> Adder-cost: 18   maxlim: 36   bits: 7/6
c ---[ 533]---> Adder-cost: 18   maxlim: 37   bits: 7/6
c ---[ 532]---> Adder-cost: 17   maxlim: 25   bits: 6/5
c ---[ 531]---> Adder-cost: 15   maxlim: 24   bits: 6/5
c ---[ 530]---> Adder-cost: 18   maxlim: 36   bits: 7/6
c ---[ 529]---> Adder-cost: 18   maxlim: 37   bits: 7/6
c ---[ 528]---> Adder-cost: 17   maxlim: 25   bits: 6/5
c ---[ 527]---> Adder-cost: 15   maxlim: 23   bits: 6/5
c ---[ 526]---> Adder-cost: 19   maxlim: 37   bits: 7/6
c ---[ 525]---> Adder-cost: 20   maxlim: 38   bits: 7/6
c ---[ 524]---> Adder-cost: 15   maxlim: 24   bits: 6/5
c ---[ 523]---> Adder-cost: 15   maxlim: 24   bits: 6/5
c ---[ 522]---> Adder-cost: 18   maxlim: 36   bits: 7/6
c ---[ 521]---> Adder-cost: 18   maxlim: 37   bits: 7/6
c ---[ 520]---> Adder-cost: 17   maxlim: 25   bits: 6/5
c ---[ 519]---> Adder-cost: 17   maxlim: 25   bits: 6/5
c ---[ 518]---> Adder-cost: 16   maxlim: 35   bits: 7/6
c ---[ 517]---> Adder-cost: 18   maxlim: 36   bits: 7/6
c ---[ 516]---> Adder-cost: 19   maxlim: 26   bits: 6/5
c ---[ 515]---> Adder-cost: 19   maxlim: 26   bits: 6/5
c ---[ 514]---> Adder-cost: 20   maxlim: 34   bits: 7/6
c ---[ 513]---> Adder-cost: 14   maxlim: 35   bits: 7/6
c ---[ 512]---> Adder-cost: 13   maxlim: 27   bits: 6/5
c ---[ 511]---> Adder-cost: 13   maxlim: 27   bits: 6/5
c ---[ 510]---> Adder-cost: 18   maxlim: 33   bits: 7/6
c ---[ 509]---> Adder-cost: 20   maxlim: 34   bits: 7/6
c ---[ 508]---> Adder-cost: 17   maxlim: 28   bits: 6/5
c ---[ 507]---> Adder-cost: 17   maxlim: 28   bits: 6/5
c ---[ 506]---> Adder-cost: 12   maxlim: 32   bits: 7/6
c ---[ 505]---> Adder-cost: 18   maxlim: 33   bits: 7/6
c ---[ 504]---> Adder-cost: 17   maxlim: 29   bits: 6/5
c ---[ 503]---> Adder-cost: 17   maxlim: 29   bits: 6/5
c ---[ 502]---> Adder-cost: 7   maxlim: 31   bits: 6/5
c ---[ 501]---> Adder-cost: 12   maxlim: 32   bits: 7/6
c ---[ 500]---> Adder-cost: 19   maxlim: 30   bits: 6/5
c ---[ 499]---> Adder-cost: 19   maxlim: 30   bits: 6/5
c ---[ 498]---> Adder-cost: 19   maxlim: 30   bits: 6/5
c ---[ 497]---> Adder-cost: 1   maxlim: 31   bits: 6/5
c ---[ 496]---> Adder-cost: 5   maxlim: 31   bits: 6/5
c ---[ 495]---> Adder-cost: 19   maxlim: 30   bits: 6/5
c ---[ 494]---> Adder-cost: 19   maxlim: 30   bits: 6/5
c ---[ 493]---> Adder-cost: 11   maxlim: 31   bits: 6/5
c ---[ 492]---> Adder-cost: 10   maxlim: 31   bits: 6/5
c ---[ 491]---> Adder-cost: 19   maxlim: 30   bits: 6/5
c ---[ 490]---> Adder-cost: 19   maxlim: 30   bits: 6/5
c ---[ 489]---> Adder-cost: 11   maxlim: 31   bits: 6/5
c ---[ 488]---> Adder-cost: 10   maxlim: 31   bits: 6/5
c ---[ 487]---> Adder-cost: 19   maxlim: 30   bits: 6/5
c ---[ 486]---> Adder-cost: 19   maxlim: 30   bits: 6/5
c ---[ 485]---> Adder-cost: 11   maxlim: 31   bits: 6/5
c ---[ 484]---> Adder-cost: 10   maxlim: 31   bits: 6/5
c ---[ 483]---> Adder-cost: 19   maxlim: 30   bits: 6/5
c ---[ 482]---> Adder-cost: 19   maxlim: 30   bits: 6/5
c ---[ 481]---> Adder-cost: 11   maxlim: 31   bits: 6/5
c ---[ 480]---> Adder-cost: 10   maxlim: 31   bits: 6/5
c ---[ 479]---> Adder-cost: 19   maxlim: 30   bits: 6/5
c ---[ 478]---> Adder-cost: 19   maxlim: 30   bits: 6/5
c ---[ 477]---> Adder-cost: 11   maxlim: 31   bits: 6/5
c ---[ 476]---> Adder-cost: 10   maxlim: 31   bits: 6/5
c ---[ 475]---> Adder-cost: 19   maxlim: 30   bits: 6/5
c ---[ 474]---> Adder-cost: 19   maxlim: 30   bits: 6/5
c ---[ 473]---> Adder-cost: 11   maxlim: 31   bits: 6/5
c ---[ 472]---> Adder-cost: 10   maxlim: 31   bits: 6/5
c ---[ 471]---> Adder-cost: 19   maxlim: 30   bits: 6/5
c ---[ 470]---> Adder-cost: 19   maxlim: 30   bits: 6/5
c ---[ 469]---> Adder-cost: 11   maxlim: 31   bits: 6/5
c ---[ 468]---> Adder-cost: 10   maxlim: 31   bits: 6/5
c ---[ 467]---> Adder-cost: 19   maxlim: 30   bits: 6/5
c ---[ 466]---> Adder-cost: 19   maxlim: 30   bits: 6/5
c ---[ 465]---> Adder-cost: 11   maxlim: 31   bits: 6/5
c ---[ 464]---> Adder-cost: 10   maxlim: 31   bits: 6/5
c ---[ 463]---> Adder-cost: 19   maxlim: 30   bits: 6/5
c ---[ 462]---> Adder-cost: 19   maxlim: 30   bits: 6/5
c ---[ 461]---> Adder-cost: 11   maxlim: 31   bits: 6/5
c ---[ 460]---> Adder-cost: 10   maxlim: 31   bits: 6/5
c ---[ 459]---> Adder-cost: 19   maxlim: 30   bits: 6/5
c ---[ 458]---> Adder-cost: 19   maxlim: 30   bits: 6/5
c ---[ 457]---> Adder-cost: 11   maxlim: 31   bits: 6/5
c ---[ 456]---> Adder-cost: 10   maxlim: 31   bits: 6/5
c ---[ 455]---> Adder-cost: 19   maxlim: 30   bits: 6/5
c ---[ 454]---> Adder-cost: 19   maxlim: 30   bits: 6/5
c ---[ 453]---> Adder-cost: 11   maxlim: 31   bits: 6/5
c ---[ 452]---> Adder-cost: 10   maxlim: 31   bits: 6/5
c ---[ 451]---> Adder-cost: 19   maxlim: 30   bits: 6/5
c ---[ 450]---> Adder-cost: 19   maxlim: 30   bits: 6/5
c ---[ 449]---> Adder-cost: 11   maxlim: 31   bits: 6/5
c ---[ 448]---> Adder-cost: 10   maxlim: 31   bits: 6/5
c ---[ 447]---> Adder-cost: 19   maxlim: 30   bits: 6/5
c ---[ 446]---> Adder-cost: 19   maxlim: 30   bits: 6/5
c ---[ 445]---> Adder-cost: 11   maxlim: 31   bits: 6/5
c ---[ 444]---> Adder-cost: 10   maxlim: 31   bits: 6/5
c ---[ 443]---> Adder-cost: 19   maxlim: 30   bits: 6/5
c ---[ 442]---> Adder-cost: 19   maxlim: 30   bits: 6/5
c ---[ 441]---> Adder-cost: 11   maxlim: 31   bits: 6/5
c ---[ 440]---> Adder-cost: 10   maxlim: 31   bits: 6/5
c ---[ 439]---> Adder-cost: 19   maxlim: 30   bits: 6/5
c ---[ 438]---> Adder-cost: 19   maxlim: 30   bits: 6/5
c ---[ 437]---> Adder-cost: 11   maxlim: 31   bits: 6/5
c ---[ 436]---> Adder-cost: 10   maxlim: 31   bits: 6/5
c ---[ 435]---> Adder-cost: 19   maxlim: 30   bits: 6/5
c ---[ 434]---> Adder-cost: 19   maxlim: 30   bits: 6/5
c ---[ 433]---> Adder-cost: 11   maxlim: 31   bits: 6/5
c ---[ 432]---> Adder-cost: 10   maxlim: 31   bits: 6/5
c ---[ 431]---> Adder-cost: 19   maxlim: 30   bits: 6/5
c ---[ 430]---> Adder-cost: 19   maxlim: 30   bits: 6/5
c ---[ 429]---> Adder-cost: 11   maxlim: 31   bits: 6/5
c ---[ 428]---> Adder-cost: 10   maxlim: 31   bits: 6/5
c ---[ 427]---> Adder-cost: 19   maxlim: 30   bits: 6/5
c ---[ 426]---> Adder-cost: 19   maxlim: 30   bits: 6/5
c ---[ 425]---> Adder-cost: 11   maxlim: 31   bits: 6/5
c ---[ 424]---> Adder-cost: 10   maxlim: 31   bits: 6/5
c ---[ 423]---> Adder-cost: 19   maxlim: 30   bits: 6/5
c ---[ 422]---> Adder-cost: 19   maxlim: 30   bits: 6/5
c ---[ 421]---> Adder-cost: 11   maxlim: 31   bits: 6/5
c ---[ 420]---> Adder-cost: 10   maxlim: 31   bits: 6/5
c ---[ 419]---> Adder-cost: 19   maxlim: 30   bits: 6/5
c ---[ 418]---> Adder-cost: 19   maxlim: 30   bits: 6/5
c ---[ 417]---> Adder-cost: 11   maxlim: 31   bits: 6/5
c ---[ 416]---> Adder-cost: 10   maxlim: 31   bits: 6/5
c ---[ 415]---> Adder-cost: 19   maxlim: 30   bits: 6/5
c ---[ 414]---> Adder-cost: 19   maxlim: 30   bits: 6/5
c ---[ 413]---> Adder-cost: 11   maxlim: 31   bits: 6/5
c ---[ 412]---> Adder-cost: 10   maxlim: 31   bits: 6/5
c ---[ 411]---> Adder-cost: 19   maxlim: 30   bits: 6/5
c ---[ 410]---> Adder-cost: 19   maxlim: 30   bits: 6/5
c ---[ 409]---> Adder-cost: 11   maxlim: 31   bits: 6/5
c ---[ 408]---> Adder-cost: 10   maxlim: 31   bits: 6/5
c ---[ 407]---> Adder-cost: 19   maxlim: 30   bits: 6/5
c ---[ 406]---> Adder-cost: 19   maxlim: 30   bits: 6/5
c ---[ 405]---> Adder-cost: 11   maxlim: 31   bits: 6/5
c ---[ 404]---> Adder-cost: 10   maxlim: 31   bits: 6/5
c ---[ 403]---> Adder-cost: 19   maxlim: 30   bits: 6/5
c ---[ 402]---> Adder-cost: 19   maxlim: 30   bits: 6/5
c ---[ 401]---> Adder-cost: 11   maxlim: 31   bits: 6/5
c ---[ 400]---> Adder-cost: 10   maxlim: 31   bits: 6/5
c ---[ 399]---> Adder-cost: 19   maxlim: 30   bits: 6/5
c ---[ 398]---> Adder-cost: 19   maxlim: 30   bits: 6/5
c ---[ 397]---> Adder-cost: 11   maxlim: 31   bits: 6/5
c ---[ 396]---> Adder-cost: 10   maxlim: 31   bits: 6/5
c ---[ 395]---> Adder-cost: 19   maxlim: 30   bits: 6/5
c ---[ 394]---> Adder-cost: 19   maxlim: 30   bits: 6/5
c ---[ 393]---> Adder-cost: 11   maxlim: 31   bits: 6/5
c ---[ 392]---> Adder-cost: 10   maxlim: 31   bits: 6/5
c ---[ 391]---> Adder-cost: 19   maxlim: 30   bits: 6/5
c ---[ 390]---> Adder-cost: 19   maxlim: 30   bits: 6/5
c ---[ 389]---> Adder-cost: 11   maxlim: 31   bits: 6/5
c ---[ 388]---> Adder-cost: 10   maxlim: 31   bits: 6/5
c ---[ 387]---> Adder-cost: 19   maxlim: 30   bits: 6/5
c ---[ 386]---> Adder-cost: 19   maxlim: 30   bits: 6/5
c ---[ 385]---> Adder-cost: 11   maxlim: 31   bits: 6/5
c ---[ 384]---> Adder-cost: 10   maxlim: 31   bits: 6/5
c ---[ 383]---> Adder-cost: 19   maxlim: 30   bits: 6/5
c ---[ 382]---> Adder-cost: 19   maxlim: 30   bits: 6/5
c ---[ 381]---> Adder-cost: 11   maxlim: 31   bits: 6/5
c ---[ 380]---> Adder-cost: 10   maxlim: 31   bits: 6/5
c ---[ 379]---> Adder-cost: 19   maxlim: 30   bits: 6/5
c ---[ 378]---> Adder-cost: 19   maxlim: 30   bits: 6/5
c ---[ 377]---> Adder-cost: 11   maxlim: 31   bits: 6/5
c ---[ 376]---> Adder-cost: 10   maxlim: 31   bits: 6/5
c ---[ 375]---> Adder-cost: 19   maxlim: 30   bits: 6/5
c ---[ 374]---> Adder-cost: 19   maxlim: 30   bits: 6/5
c ---[ 373]---> Adder-cost: 11   maxlim: 31   bits: 6/5
c ---[ 372]---> Adder-cost: 10   maxlim: 31   bits: 6/5
c ---[ 371]---> Adder-cost: 19   maxlim: 30   bits: 6/5
c ---[ 370]---> Adder-cost: 19   maxlim: 30   bits: 6/5
c ---[ 369]---> Adder-cost: 11   maxlim: 31   bits: 6/5
c ---[ 368]---> Adder-cost: 10   maxlim: 31   bits: 6/5
c ---[ 367]---> Adder-cost: 19   maxlim: 30   bits: 6/5
c ---[ 366]---> Adder-cost: 19   maxlim: 30   bits: 6/5
c ---[ 365]---> Adder-cost: 11   maxlim: 31   bits: 6/5
c ---[ 364]---> Adder-cost: 10   maxlim: 31   bits: 6/5
c ---[ 363]---> Adder-cost: 19   maxlim: 30   bits: 6/5
c ---[ 362]---> Adder-cost: 19   maxlim: 30   bits: 6/5
c ---[ 361]---> Adder-cost: 11   maxlim: 31   bits: 6/5
c ---[ 360]---> Adder-cost: 10   maxlim: 31   bits: 6/5
c ---[ 359]---> Adder-cost: 19   maxlim: 30   bits: 6/5
c ---[ 358]---> Adder-cost: 19   maxlim: 30   bits: 6/5
c ---[ 357]---> Adder-cost: 11   maxlim: 31   bits: 6/5
c ---[ 356]---> Adder-cost: 10   maxlim: 31   bits: 6/5
c ---[ 355]---> Adder-cost: 19   maxlim: 30   bits: 6/5
c ---[ 354]---> Adder-cost: 19   maxlim: 30   bits: 6/5
c ---[ 353]---> Adder-cost: 11   maxlim: 31   bits: 6/5
c ---[ 352]---> Adder-cost: 10   maxlim: 31   bits: 6/5
c ---[ 351]---> Adder-cost: 9   maxlim: 23   bits: 6/5
c ---[ 350]---> Adder-cost: 18   maxlim: 37   bits: 7/6
c ---[ 349]---> Adder-cost: 20   maxlim: 38   bits: 7/6
c ---[ 348]---> Adder-cost: 15   maxlim: 24   bits: 6/5
c ---[ 347]---> Adder-cost: 9   maxlim: 23   bits: 6/5
c ---[ 346]---> Adder-cost: 18   maxlim: 37   bits: 7/6
c ---[ 345]---> Adder-cost: 20   maxlim: 38   bits: 7/6
c ---[ 344]---> Adder-cost: 15   maxlim: 24   bits: 6/5
c ---[ 343]---> Adder-cost: 9   maxlim: 23   bits: 6/5
c ---[ 342]---> Adder-cost: 18   maxlim: 37   bits: 7/6
c ---[ 341]---> Adder-cost: 20   maxlim: 38   bits: 7/6
c ---[ 340]---> Adder-cost: 15   maxlim: 24   bits: 6/5
c ---[ 339]---> Adder-cost: 9   maxlim: 23   bits: 6/5
c ---[ 338]---> Adder-cost: 18   maxlim: 37   bits: 7/6
c ---[ 337]---> Adder-cost: 20   maxlim: 38   bits: 7/6
c ---[ 336]---> Adder-cost: 15   maxlim: 24   bits: 6/5
c ---[ 335]---> Adder-cost: 9   maxlim: 23   bits: 6/5
c ---[ 334]---> Adder-cost: 18   maxlim: 37   bits: 7/6
c ---[ 333]---> Adder-cost: 20   maxlim: 38   bits: 7/6
c ---[ 332]---> Adder-cost: 15   maxlim: 24   bits: 6/5
c ---[ 331]---> Adder-cost: 9   maxlim: 23   bits: 6/5
c ---[ 330]---> Adder-cost: 18   maxlim: 37   bits: 7/6
c ---[ 329]---> Adder-cost: 20   maxlim: 38   bits: 7/6
c ---[ 328]---> Adder-cost: 15   maxlim: 24   bits: 6/5
c ---[ 327]---> Adder-cost: 9   maxlim: 23   bits: 6/5
c ---[ 326]---> Adder-cost: 18   maxlim: 37   bits: 7/6
c ---[ 325]---> Adder-cost: 20   maxlim: 38   bits: 7/6
c ---[ 324]---> Adder-cost: 15   maxlim: 24   bits: 6/5
c ---[ 323]---> Adder-cost: 19   maxlim: 22   bits: 6/5
c ---[ 322]---> Adder-cost: 20   maxlim: 38   bits: 7/6
c ---[ 321]---> Adder-cost: 16   maxlim: 39   bits: 7/6
c ---[ 320]---> Adder-cost: 14   maxlim: 23   bits: 6/5
c ---[ 319]---> Adder-cost: 9   maxlim: 23   bits: 6/5
c ---[ 318]---> Adder-cost: 18   maxlim: 37   bits: 7/6
c ---[ 317]---> Adder-cost: 20   maxlim: 38   bits: 7/6
c ---[ 316]---> Adder-cost: 15   maxlim: 24   bits: 6/5
c ---[ 315]---> Adder-cost: 15   maxlim: 24   bits: 6/5
c ---[ 314]---> Adder-cost: 18   maxlim: 36   bits: 7/6
c ---[ 313]---> Adder-cost: 18   maxlim: 37   bits: 7/6
c ---[ 312]---> Adder-cost: 17   maxlim: 25   bits: 6/5
c ---[ 311]---> Adder-cost: 17   maxlim: 25   bits: 6/5
c ---[ 310]---> Adder-cost: 14   maxlim: 35   bits: 7/6
c ---[ 309]---> Adder-cost: 18   maxlim: 36   bits: 7/6
c ---[ 308]---> Adder-cost: 19   maxlim: 26   bits: 6/5
c ---[ 307]---> Adder-cost: 19   maxlim: 26   bits: 6/5
c ---[ 306]---> Adder-cost: 20   maxlim: 34   bits: 7/6
c ---[ 305]---> Adder-cost: 14   maxlim: 35   bits: 7/6
c ---[ 304]---> Adder-cost: 13   maxlim: 27   bits: 6/5
c ---[ 303]---> Adder-cost: 13   maxlim: 27   bits: 6/5
c ---[ 302]---> Adder-cost: 18   maxlim: 33   bits: 7/6
c ---[ 301]---> Adder-cost: 20   maxlim: 34   bits: 7/6
c ---[ 300]---> Adder-cost: 17   maxlim: 28   bits: 6/5
c ---[ 299]---> Adder-cost: 17   maxlim: 28   bits: 6/5
c ---[ 298]---> Adder-cost: 12   maxlim: 32   bits: 7/6
c ---[ 297]---> Adder-cost: 18   maxlim: 33   bits: 7/6
c ---[ 296]---> Adder-cost: 17   maxlim: 29   bits: 6/5
c ---[ 295]---> Adder-cost: 17   maxlim: 29   bits: 6/5
c ---[ 294]---> Adder-cost: 5   maxlim: 31   bits: 6/5
c ---[ 293]---> Adder-cost: 12   maxlim: 32   bits: 7/6
c ---[ 292]---> Adder-cost: 19   maxlim: 30   bits: 6/5
c ---[ 291]---> Adder-cost: 19   maxlim: 30   bits: 6/5
c ---[ 290]---> Adder-cost: 19   maxlim: 30   bits: 6/5
c ---[ 289]---> Adder-cost: 1   maxlim: 31   bits: 6/5
c ---[ 288]---> Adder-cost: 5   maxlim: 31   bits: 6/5
c ---[ 287]---> Adder-cost: 19   maxlim: 30   bits: 6/5
c ---[ 286]---> Adder-cost: 19   maxlim: 30   bits: 6/5
c ---[ 285]---> Adder-cost: 11   maxlim: 31   bits: 6/5
c ---[ 284]---> Adder-cost: 10   maxlim: 31   bits: 6/5
c ---[ 283]---> Adder-cost: 19   maxlim: 30   bits: 6/5
c ---[ 282]---> Adder-cost: 19   maxlim: 30   bits: 6/5
c ---[ 281]---> Adder-cost: 11   maxlim: 31   bits: 6/5
c ---[ 280]---> Adder-cost: 10   maxlim: 31   bits: 6/5
c ---[ 279]---> Adder-cost: 19   maxlim: 30   bits: 6/5
c ---[ 278]---> Adder-cost: 19   maxlim: 30   bits: 6/5
c ---[ 277]---> Adder-cost: 11   maxlim: 31   bits: 6/5
c ---[ 276]---> Adder-cost: 10   maxlim: 31   bits: 6/5
c ---[ 275]---> Adder-cost: 19   maxlim: 30   bits: 6/5
c ---[ 274]---> Adder-cost: 19   maxlim: 30   bits: 6/5
c ---[ 273]---> Adder-cost: 11   maxlim: 31   bits: 6/5
c ---[ 272]---> Adder-cost: 10   maxlim: 31   bits: 6/5
c ---[ 271]---> Adder-cost: 19   maxlim: 30   bits: 6/5
c ---[ 270]---> Adder-cost: 19   maxlim: 30   bits: 6/5
c ---[ 269]---> Adder-cost: 11   maxlim: 31   bits: 6/5
c ---[ 268]---> Adder-cost: 10   maxlim: 31   bits: 6/5
c ---[ 267]---> Adder-cost: 19   maxlim: 30   bits: 6/5
c ---[ 266]---> Adder-cost: 19   maxlim: 30   bits: 6/5
c ---[ 265]---> Adder-cost: 11   maxlim: 31   bits: 6/5
c ---[ 264]---> Adder-cost: 10   maxlim: 31   bits: 6/5
c ---[ 263]---> Adder-cost: 19   maxlim: 30   bits: 6/5
c ---[ 262]---> Adder-cost: 19   maxlim: 30   bits: 6/5
c ---[ 261]---> Adder-cost: 11   maxlim: 31   bits: 6/5
c ---[ 260]---> Adder-cost: 10   maxlim: 31   bits: 6/5
c ---[ 259]---> Adder-cost: 19   maxlim: 30   bits: 6/5
c ---[ 258]---> Adder-cost: 19   maxlim: 30   bits: 6/5
c ---[ 257]---> Adder-cost: 11   maxlim: 31   bits: 6/5
c ---[ 256]---> Adder-cost: 10   maxlim: 31   bits: 6/5
c ---[ 255]---> Adder-cost: 19   maxlim: 30   bits: 6/5
c ---[ 254]---> Adder-cost: 19   maxlim: 30   bits: 6/5
c ---[ 253]---> Adder-cost: 11   maxlim: 31   bits: 6/5
c ---[ 252]---> Adder-cost: 10   maxlim: 31   bits: 6/5
c ---[ 251]---> Adder-cost: 19   maxlim: 30   bits: 6/5
c ---[ 250]---> Adder-cost: 19   maxlim: 30   bits: 6/5
c ---[ 249]---> Adder-cost: 11   maxlim: 31   bits: 6/5
c ---[ 248]---> Adder-cost: 10   maxlim: 31   bits: 6/5
c ---[ 247]---> Adder-cost: 19   maxlim: 30   bits: 6/5
c ---[ 246]---> Adder-cost: 19   maxlim: 30   bits: 6/5
c ---[ 245]---> Adder-cost: 11   maxlim: 31   bits: 6/5
c ---[ 244]---> Adder-cost: 10   maxlim: 31   bits: 6/5
c ---[ 243]---> Adder-cost: 19   maxlim: 30   bits: 6/5
c ---[ 242]---> Adder-cost: 19   maxlim: 30   bits: 6/5
c ---[ 241]---> Adder-cost: 11   maxlim: 31   bits: 6/5
c ---[ 240]---> Adder-cost: 10   maxlim: 31   bits: 6/5
c ---[ 239]---> Adder-cost: 19   maxlim: 30   bits: 6/5
c ---[ 238]---> Adder-cost: 19   maxlim: 30   bits: 6/5
c ---[ 237]---> Adder-cost: 11   maxlim: 31   bits: 6/5
c ---[ 236]---> Adder-cost: 10   maxlim: 31   bits: 6/5
c ---[ 235]---> Adder-cost: 19   maxlim: 30   bits: 6/5
c ---[ 234]---> Adder-cost: 19   maxlim: 30   bits: 6/5
c ---[ 233]---> Adder-cost: 11   maxlim: 31   bits: 6/5
c ---[ 232]---> Adder-cost: 10   maxlim: 31   bits: 6/5
c ---[ 231]---> Adder-cost: 19   maxlim: 30   bits: 6/5
c ---[ 230]---> Adder-cost: 19   maxlim: 30   bits: 6/5
c ---[ 229]---> Adder-cost: 11   maxlim: 31   bits: 6/5
c ---[ 228]---> Adder-cost: 10   maxlim: 31   bits: 6/5
c ---[ 227]---> Adder-cost: 19   maxlim: 30   bits: 6/5
c ---[ 226]---> Adder-cost: 19   maxlim: 30   bits: 6/5
c ---[ 225]---> Adder-cost: 11   maxlim: 31   bits: 6/5
c ---[ 224]---> Adder-cost: 10   maxlim: 31   bits: 6/5
c ---[ 223]---> Adder-cost: 19   maxlim: 30   bits: 6/5
c ---[ 222]---> Adder-cost: 19   maxlim: 30   bits: 6/5
c ---[ 221]---> Adder-cost: 11   maxlim: 31   bits: 6/5
c ---[ 220]---> Adder-cost: 10   maxlim: 31   bits: 6/5
c ---[ 219]---> Adder-cost: 19   maxlim: 30   bits: 6/5
c ---[ 218]---> Adder-cost: 19   maxlim: 30   bits: 6/5
c ---[ 217]---> Adder-cost: 11   maxlim: 31   bits: 6/5
c ---[ 216]---> Adder-cost: 10   maxlim: 31   bits: 6/5
c ---[ 215]---> Adder-cost: 19   maxlim: 30   bits: 6/5
c ---[ 214]---> Adder-cost: 19   maxlim: 30   bits: 6/5
c ---[ 213]---> Adder-cost: 11   maxlim: 31   bits: 6/5
c ---[ 212]---> Adder-cost: 10   maxlim: 31   bits: 6/5
c ---[ 211]---> Adder-cost: 19   maxlim: 30   bits: 6/5
c ---[ 210]---> Adder-cost: 19   maxlim: 30   bits: 6/5
c ---[ 209]---> Adder-cost: 11   maxlim: 31   bits: 6/5
c ---[ 208]---> Adder-cost: 10   maxlim: 31   bits: 6/5
c ---[ 207]---> Adder-cost: 19   maxlim: 30   bits: 6/5
c ---[ 206]---> Adder-cost: 19   maxlim: 30   bits: 6/5
c ---[ 205]---> Adder-cost: 11   maxlim: 31   bits: 6/5
c ---[ 204]---> Adder-cost: 10   maxlim: 31   bits: 6/5
c ---[ 203]---> Adder-cost: 19   maxlim: 30   bits: 6/5
c ---[ 202]---> Adder-cost: 19   maxlim: 30   bits: 6/5
c ---[ 201]---> Adder-cost: 11   maxlim: 31   bits: 6/5
c ---[ 200]---> Adder-cost: 10   maxlim: 31   bits: 6/5
c ---[ 199]---> Adder-cost: 19   maxlim: 30   bits: 6/5
c ---[ 198]---> Adder-cost: 19   maxlim: 30   bits: 6/5
c ---[ 197]---> Adder-cost: 11   maxlim: 31   bits: 6/5
c ---[ 196]---> Adder-cost: 10   maxlim: 31   bits: 6/5
c ---[ 195]---> Adder-cost: 19   maxlim: 30   bits: 6/5
c ---[ 194]---> Adder-cost: 19   maxlim: 30   bits: 6/5
c ---[ 193]---> Adder-cost: 11   maxlim: 31   bits: 6/5
c ---[ 192]---> Adder-cost: 10   maxlim: 31   bits: 6/5
c ---[ 191]---> Adder-cost: 19   maxlim: 30   bits: 6/5
c ---[ 190]---> Adder-cost: 19   maxlim: 30   bits: 6/5
c ---[ 189]---> Adder-cost: 11   maxlim: 31   bits: 6/5
c ---[ 188]---> Adder-cost: 10   maxlim: 31   bits: 6/5
c ---[ 187]---> Adder-cost: 19   maxlim: 30   bits: 6/5
c ---[ 186]---> Adder-cost: 19   maxlim: 30   bits: 6/5
c ---[ 185]---> Adder-cost: 11   maxlim: 31   bits: 6/5
c ---[ 184]---> Adder-cost: 10   maxlim: 31   bits: 6/5
c ---[ 183]---> Adder-cost: 19   maxlim: 30   bits: 6/5
c ---[ 182]---> Adder-cost: 19   maxlim: 30   bits: 6/5
c ---[ 181]---> Adder-cost: 11   maxlim: 31   bits: 6/5
c ---[ 180]---> Adder-cost: 10   maxlim: 31   bits: 6/5
c ---[ 179]---> Adder-cost: 19   maxlim: 30   bits: 6/5
c ---[ 178]---> Adder-cost: 19   maxlim: 30   bits: 6/5
c ---[ 177]---> Adder-cost: 11   maxlim: 31   bits: 6/5
c ---[ 176]---> Adder-cost: 10   maxlim: 31   bits: 6/5
c ---[ 175]---> Adder-cost: 19   maxlim: 30   bits: 6/5
c ---[ 174]---> Adder-cost: 19   maxlim: 30   bits: 6/5
c ---[ 173]---> Adder-cost: 11   maxlim: 31   bits: 6/5
c ---[ 172]---> Adder-cost: 10   maxlim: 31   bits: 6/5
c ---[ 171]---> Adder-cost: 19   maxlim: 30   bits: 6/5
c ---[ 170]---> Adder-cost: 19   maxlim: 30   bits: 6/5
c ---[ 169]---> Adder-cost: 11   maxlim: 31   bits: 6/5
c ---[ 168]---> Adder-cost: 10   maxlim: 31   bits: 6/5
c ---[ 167]---> Adder-cost: 19   maxlim: 30   bits: 6/5
c ---[ 166]---> Adder-cost: 19   maxlim: 30   bits: 6/5
c ---[ 165]---> Adder-cost: 11   maxlim: 31   bits: 6/5
c ---[ 164]---> Adder-cost: 10   maxlim: 31   bits: 6/5
c ---[ 163]---> Adder-cost: 19   maxlim: 30   bits: 6/5
c ---[ 162]---> Adder-cost: 19   maxlim: 30   bits: 6/5
c ---[ 161]---> Adder-cost: 11   maxlim: 31   bits: 6/5
c ---[ 160]---> Adder-cost: 10   maxlim: 31   bits: 6/5
c ---[ 159]---> Adder-cost: 19   maxlim: 30   bits: 6/5
c ---[ 158]---> Adder-cost: 19   maxlim: 30   bits: 6/5
c ---[ 157]---> Adder-cost: 11   maxlim: 31   bits: 6/5
c ---[ 156]---> Adder-cost: 10   maxlim: 31   bits: 6/5
c ---[ 155]---> Adder-cost: 19   maxlim: 30   bits: 6/5
c ---[ 154]---> Adder-cost: 19   maxlim: 30   bits: 6/5
c ---[ 153]---> Adder-cost: 11   maxlim: 31   bits: 6/5
c ---[ 152]---> Adder-cost: 10   maxlim: 31   bits: 6/5
c ---[ 151]---> Adder-cost: 19   maxlim: 30   bits: 6/5
c ---[ 150]---> Adder-cost: 19   maxlim: 30   bits: 6/5
c ---[ 149]---> Adder-cost: 11   maxlim: 31   bits: 6/5
c ---[ 148]---> Adder-cost: 10   maxlim: 31   bits: 6/5
c ---[ 147]---> Adder-cost: 19   maxlim: 30   bits: 6/5
c ---[ 146]---> Adder-cost: 19   maxlim: 30   bits: 6/5
c ---[ 145]---> Adder-cost: 11   maxlim: 31   bits: 6/5
c ---[ 144]---> Adder-cost: 10   maxlim: 31   bits: 6/5
c ---[ 143]---> Adder-cost: 19   maxlim: 30   bits: 6/5
c ---[ 142]---> Adder-cost: 19   maxlim: 30   bits: 6/5
c ---[ 141]---> Adder-cost: 11   maxlim: 31   bits: 6/5
c ---[ 140]---> Adder-cost: 10   maxlim: 31   bits: 6/5
c ---[ 139]---> Adder-cost: 19   maxlim: 30   bits: 6/5
c ---[ 138]---> Adder-cost: 19   maxlim: 30   bits: 6/5
c ---[ 137]---> Adder-cost: 11   maxlim: 31   bits: 6/5
c ---[ 136]---> Adder-cost: 10   maxlim: 31   bits: 6/5
c ---[ 135]---> Adder-cost: 19   maxlim: 30   bits: 6/5
c ---[ 134]---> Adder-cost: 19   maxlim: 30   bits: 6/5
c ---[ 133]---> Adder-cost: 11   maxlim: 31   bits: 6/5
c ---[ 132]---> Adder-cost: 10   maxlim: 31   bits: 6/5
c ---[ 131]---> Adder-cost: 19   maxlim: 30   bits: 6/5
c ---[ 130]---> Adder-cost: 19   maxlim: 30   bits: 6/5
c ---[ 129]---> Adder-cost: 11   maxlim: 31   bits: 6/5
c ---[ 128]---> Adder-cost: 10   maxlim: 31   bits: 6/5
c ---[ 127]---> Adder-cost: 19   maxlim: 30   bits: 6/5
c ---[ 126]---> Adder-cost: 19   maxlim: 30   bits: 6/5
c ---[ 125]---> Adder-cost: 11   maxlim: 31   bits: 6/5
c ---[ 124]---> Adder-cost: 10   maxlim: 31   bits: 6/5
c ---[ 123]---> Adder-cost: 19   maxlim: 22   bits: 6/5
c ---[ 122]---> Adder-cost: 20   maxlim: 38   bits: 7/6
c ---[ 121]---> Adder-cost: 10   maxlim: 39   bits: 7/6
c ---[ 120]---> Adder-cost: 9   maxlim: 23   bits: 6/5
c ---[ 119]---> Adder-cost: 19   maxlim: 22   bits: 6/5
c ---[ 118]---> Adder-cost: 20   maxlim: 38   bits: 7/6
c ---[ 117]---> Adder-cost: 10   maxlim: 39   bits: 7/6
c ---[ 116]---> Adder-cost: 9   maxlim: 23   bits: 6/5
c ---[ 115]---> Adder-cost: 19   maxlim: 22   bits: 6/5
c ---[ 114]---> Adder-cost: 20   maxlim: 38   bits: 7/6
c ---[ 113]---> Adder-cost: 10   maxlim: 39   bits: 7/6
c ---[ 112]---> Adder-cost: 9   maxlim: 23   bits: 6/5
c ---[ 111]---> Adder-cost: 19   maxlim: 22   bits: 6/5
c ---[ 110]---> Adder-cost: 20   maxlim: 38   bits: 7/6
c ---[ 109]---> Adder-cost: 10   maxlim: 39   bits: 7/6
c ---[ 108]---> Adder-cost: 9   maxlim: 23   bits: 6/5
c ---[ 107]---> Adder-cost: 19   maxlim: 22   bits: 6/5
c ---[ 106]---> Adder-cost: 20   maxlim: 38   bits: 7/6
c ---[ 105]---> Adder-cost: 10   maxlim: 39   bits: 7/6
c ---[ 104]---> Adder-cost: 9   maxlim: 23   bits: 6/5
c ---[ 103]---> Adder-cost: 19   maxlim: 22   bits: 6/5
c ---[ 102]---> Adder-cost: 20   maxlim: 38   bits: 7/6
c ---[ 101]---> Adder-cost: 10   maxlim: 39   bits: 7/6
c ---[ 100]---> Adder-cost: 9   maxlim: 23   bits: 6/5
c ---[  99]---> Adder-cost: 19   maxlim: 22   bits: 6/5
c ---[  98]---> Adder-cost: 20   maxlim: 38   bits: 7/6
c ---[  97]---> Adder-cost: 10   maxlim: 39   bits: 7/6
c ---[  96]---> Adder-cost: 9   maxlim: 23   bits: 6/5
c ---[  95]---> Adder-cost: 19   maxlim: 22   bits: 6/5
c ---[  94]---> Adder-cost: 20   maxlim: 38   bits: 7/6
c ---[  93]---> Adder-cost: 10   maxlim: 39   bits: 7/6
c ---[  92]---> Adder-cost: 9   maxlim: 23   bits: 6/5
c ---[  91]---> Adder-cost: 19   maxlim: 30   bits: 6/5
c ---[  90]---> Adder-cost: 19   maxlim: 30   bits: 6/5
c ---[  89]---> Adder-cost: 11   maxlim: 31   bits: 6/5
c ---[  88]---> Adder-cost: 10   maxlim: 31   bits: 6/5
c ---[  87]---> Adder-cost: 19   maxlim: 30   bits: 6/5
c ---[  86]---> Adder-cost: 19   maxlim: 30   bits: 6/5
c ---[  85]---> Adder-cost: 11   maxlim: 31   bits: 6/5
c ---[  84]---> Adder-cost: 10   maxlim: 31   bits: 6/5
c ---[  83]---> Adder-cost: 19   maxlim: 30   bits: 6/5
c ---[  82]---> Adder-cost: 19   maxlim: 30   bits: 6/5
c ---[  81]---> Adder-cost: 11   maxlim: 31   bits: 6/5
c ---[  80]---> Adder-cost: 10   maxlim: 31   bits: 6/5
c ---[  79]---> Adder-cost: 19   maxlim: 30   bits: 6/5
c ---[  78]---> Adder-cost: 19   maxlim: 30   bits: 6/5
c ---[  77]---> Adder-cost: 11   maxlim: 31   bits: 6/5
c ---[  76]---> Adder-cost: 10   maxlim: 31   bits: 6/5
c ---[  75]---> Adder-cost: 19   maxlim: 30   bits: 6/5
c ---[  74]---> Adder-cost: 19   maxlim: 30   bits: 6/5
c ---[  73]---> Adder-cost: 11   maxlim: 31   bits: 6/5
c ---[  72]---> Adder-cost: 10   maxlim: 31   bits: 6/5
c ---[  71]---> Adder-cost: 19   maxlim: 30   bits: 6/5
c ---[  70]---> Adder-cost: 19   maxlim: 30   bits: 6/5
c ---[  69]---> Adder-cost: 11   maxlim: 31   bits: 6/5
c ---[  68]---> Adder-cost: 10   maxlim: 31   bits: 6/5
c ---[  67]---> Adder-cost: 19   maxlim: 30   bits: 6/5
c ---[  66]---> Adder-cost: 19   maxlim: 30   bits: 6/5
c ---[  65]---> Adder-cost: 11   maxlim: 31   bits: 6/5
c ---[  64]---> Adder-cost: 10   maxlim: 31   bits: 6/5
c ---[  63]---> Adder-cost: 19   maxlim: 30   bits: 6/5
c ---[  62]---> Adder-cost: 19   maxlim: 30   bits: 6/5
c ---[  61]---> Adder-cost: 11   maxlim: 31   bits: 6/5
c ---[  60]---> Adder-cost: 10   maxlim: 31   bits: 6/5
c ---[  59]---> Adder-cost: 19   maxlim: 30   bits: 6/5
c ---[  58]---> Adder-cost: 19   maxlim: 30   bits: 6/5
c ---[  57]---> Adder-cost: 11   maxlim: 31   bits: 6/5
c ---[  56]---> Adder-cost: 10   maxlim: 31   bits: 6/5
c ---[  55]---> Adder-cost: 19   maxlim: 30   bits: 6/5
c ---[  54]---> Adder-cost: 19   maxlim: 30   bits: 6/5
c ---[  53]---> Adder-cost: 11   maxlim: 31   bits: 6/5
c ---[  52]---> Adder-cost: 10   maxlim: 31   bits: 6/5
c ---[  51]---> Adder-cost: 19   maxlim: 30   bits: 6/5
c ---[  50]---> Adder-cost: 19   maxlim: 30   bits: 6/5
c ---[  49]---> Adder-cost: 11   maxlim: 31   bits: 6/5
c ---[  48]---> Adder-cost: 10   maxlim: 31   bits: 6/5
c ---[  47]---> Adder-cost: 19   maxlim: 30   bits: 6/5
c ---[  46]---> Adder-cost: 19   maxlim: 30   bits: 6/5
c ---[  45]---> Adder-cost: 11   maxlim: 31   bits: 6/5
c ---[  44]---> Adder-cost: 10   maxlim: 31   bits: 6/5
c ---[  43]---> Adder-cost: 19   maxlim: 30   bits: 6/5
c ---[  42]---> Adder-cost: 19   maxlim: 30   bits: 6/5
c ---[  41]---> Adder-cost: 11   maxlim: 31   bits: 6/5
c ---[  40]---> Adder-cost: 10   maxlim: 31   bits: 6/5
c ---[  39]---> Adder-cost: 19   maxlim: 30   bits: 6/5
c ---[  38]---> Adder-cost: 19   maxlim: 30   bits: 6/5
c ---[  37]---> Adder-cost: 11   maxlim: 31   bits: 6/5
c ---[  36]---> Adder-cost: 10   maxlim: 31   bits: 6/5
c ---[  35]---> Adder-cost: 19   maxlim: 30   bits: 6/5
c ---[  34]---> Adder-cost: 19   maxlim: 30   bits: 6/5
c ---[  33]---> Adder-cost: 11   maxlim: 31   bits: 6/5
c ---[  32]---> Adder-cost: 10   maxlim: 31   bits: 6/5
c ---[  31]---> Adder-cost: 19   maxlim: 30   bits: 6/5
c ---[  30]---> Adder-cost: 19   maxlim: 30   bits: 6/5
c ---[  29]---> Adder-cost: 11   maxlim: 31   bits: 6/5
c ---[  28]---> Adder-cost: 10   maxlim: 31   bits: 6/5
c ---[  27]---> Adder-cost: 19   maxlim: 30   bits: 6/5
c ---[  26]---> Adder-cost: 19   maxlim: 30   bits: 6/5
c ---[  25]---> Adder-cost: 11   maxlim: 31   bits: 6/5
c ---[  24]---> Adder-cost: 10   maxlim: 31   bits: 6/5
c ---[  23]---> Adder-cost: 19   maxlim: 30   bits: 6/5
c ---[  22]---> Adder-cost: 19   maxlim: 30   bits: 6/5
c ---[  21]---> Adder-cost: 11   maxlim: 31   bits: 6/5
c ---[  20]---> Adder-cost: 10   maxlim: 31   bits: 6/5
c ---[  19]---> Adder-cost: 19   maxlim: 30   bits: 6/5
c ---[  18]---> Adder-cost: 19   maxlim: 30   bits: 6/5
c ---[  17]---> Adder-cost: 11   maxlim: 31   bits: 6/5
c ---[  16]---> Adder-cost: 10   maxlim: 31   bits: 6/5
c ---[  15]---> Adder-cost: 19   maxlim: 30   bits: 6/5
c ---[  14]---> Adder-cost: 19   maxlim: 30   bits: 6/5
c ---[  13]---> Adder-cost: 11   maxlim: 31   bits: 6/5
c ---[  12]---> Adder-cost: 10   maxlim: 31   bits: 6/5
c ---[  11]---> Adder-cost: 19   maxlim: 30   bits: 6/5
c ---[  10]---> Adder-cost: 19   maxlim: 30   bits: 6/5
c ---[   9]---> Adder-cost: 11   maxlim: 31   bits: 6/5
c ---[   8]---> Adder-cost: 10   maxlim: 31   bits: 6/5
c ---[   7]---> Adder-cost: 19   maxlim: 30   bits: 6/5
c ---[   6]---> Adder-cost: 19   maxlim: 30   bits: 6/5
c ---[   5]---> Adder-cost: 11   maxlim: 31   bits: 6/5
c ---[   4]---> Adder-cost: 10   maxlim: 31   bits: 6/5
c ---[   3]---> Adder-cost: 19   maxlim: 30   bits: 6/5
c ---[   2]---> Adder-cost: 19   maxlim: 30   bits: 6/5
c ---[   1]---> Adder-cost: 11   maxlim: 31   bits: 6/5
c ---[   0]---> Adder-cost: 10   maxlim: 31   bits: 6/5
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |  141460   427685 |   47153       0        0     nan |  0.000 % |
c |       100 |  141460   427685 |   51868     100     1086    10.9 | 13.655 % |
c |       250 |  141460   427685 |   57055     250     3851    15.4 | 13.655 % |
c |       475 |  141460   427685 |   62760     475     6971    14.7 | 13.655 % |
c |       813 |  141460   427685 |   69036     813    24709    30.4 | 13.655 % |
c |      1321 |  141460   427685 |   75940    1321    40424    30.6 | 13.655 % |
c |      2080 |  141460   427685 |   83534    2080    64901    31.2 | 13.655 % |
c |      3221 |  141460   427685 |   91887    3221    99056    30.8 | 13.655 % |
c |      4931 |  141460   427685 |  101076    4931   166996    33.9 | 13.655 % |
c |      7496 |  141460   427685 |  111184    7496   293767    39.2 | 13.655 % |
c |     11341 |  141460   427685 |  122302   11341   387360    34.2 | 13.655 % |
c |     17110 |  141460   427685 |  134533   17110   651401    38.1 | 13.655 % |
c |     25759 |  141460   427685 |  147986   25759   974546    37.8 | 13.655 % |
c |     38733 |  141460   427685 |  162784   38733  1486586    38.4 | 13.655 % |
c |     58194 |  141460   427685 |  179063   58194  2263996    38.9 | 13.655 % |
c |     87386 |  141460   427685 |  196969   87386  3311103    37.9 | 13.655 % |
c |    131175 |  141460   427685 |  216666  131175  4734056    36.1 | 13.655 % |
c |    196860 |  141278   427035 |  238333   41348  1358515    32.9 | 13.657 % |
#### 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.75 0.92 0.89 2/54 29174
Raw data (stat): 29174 (runsolver) R 29173 25347 25346 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 421419875 1052672 99 4294967295 134512640 135381576 3221224448 3221219692 135158418 0 2147483391 7 90112 0 0 0 17 1 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0005 s]
Raw data (loadavg): 0.79 0.93 0.90 2/54 29174
Raw data (stat): 29174 (minisat+) R 29173 25347 25346 0 -1 0 5179 0 0 0 984 14 0 0 25 0 1 0 421419875 23781376 4968 4294967295 134512640 134672761 3221224560 3221223744 134558656 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5806 4968 603 41 0 5765 0
vsize: 23224
[startup+20.0015 s]
Raw data (loadavg): 0.82 0.93 0.90 2/54 29174
Raw data (stat): 29174 (minisat+) R 29173 25347 25346 0 -1 0 5179 0 0 0 1984 14 0 0 25 0 1 0 421419875 23781376 4968 4294967295 134512640 134672761 3221224560 3221223696 134560590 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5806 4968 603 41 0 5765 0
vsize: 23224
[startup+30.0016 s]
Raw data (loadavg): 0.85 0.93 0.90 2/54 29174
Raw data (stat): 29174 (minisat+) R 29173 25347 25346 0 -1 0 5179 0 0 0 2983 14 0 0 25 0 1 0 421419875 23781376 4968 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5806 4968 603 41 0 5765 0
vsize: 23224
[startup+40.001 s]
Raw data (loadavg): 0.87 0.93 0.90 2/54 29174
Raw data (stat): 29174 (minisat+) R 29173 25347 25346 0 -1 0 5179 0 0 0 3983 14 0 0 25 0 1 0 421419875 23781376 4968 4294967295 134512640 134672761 3221224560 3221223696 134560588 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5806 4968 603 41 0 5765 0
vsize: 23224
[startup+50.0019 s]
Raw data (loadavg): 0.89 0.93 0.90 2/54 29174
Raw data (stat): 29174 (minisat+) R 29173 25347 25346 0 -1 0 5179 0 0 0 4983 14 0 0 25 0 1 0 421419875 23781376 4968 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5806 4968 603 41 0 5765 0
vsize: 23224
[startup+60.0011 s]
Raw data (loadavg): 0.90 0.94 0.90 2/54 29174
Raw data (stat): 29174 (minisat+) R 29173 25347 25346 0 -1 0 5281 0 0 0 5983 14 0 0 25 0 1 0 421419875 24043520 5070 4294967295 134512640 134672761 3221224560 3221223696 134565073 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5870 5070 603 41 0 5829 0
vsize: 23480
[startup+70.0017 s]
Raw data (loadavg): 0.92 0.94 0.90 2/54 29174
Raw data (stat): 29174 (minisat+) R 29173 25347 25346 0 -1 0 5461 0 0 0 6983 15 0 0 25 0 1 0 421419875 24858624 5250 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6069 5250 603 41 0 6028 0
vsize: 24276
[startup+80.0029 s]
Raw data (loadavg): 0.93 0.94 0.90 2/54 29174
Raw data (stat): 29174 (minisat+) R 29173 25347 25346 0 -1 0 5576 0 0 0 7982 15 0 0 25 0 1 0 421419875 25395200 5365 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6200 5365 603 41 0 6159 0
vsize: 24800
[startup+90.0018 s]
Raw data (loadavg): 0.94 0.94 0.90 2/54 29174
Raw data (stat): 29174 (minisat+) R 29173 25347 25346 0 -1 0 5666 0 0 0 8983 15 0 0 25 0 1 0 421419875 25792512 5455 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6297 5455 603 41 0 6256 0
vsize: 25188
[startup+100.001 s]
Raw data (loadavg): 0.95 0.94 0.90 2/54 29174
Raw data (stat): 29174 (minisat+) R 29173 25347 25346 0 -1 0 5768 0 0 0 9982 16 0 0 25 0 1 0 421419875 26193920 5557 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6395 5557 603 41 0 6354 0
vsize: 25580
[startup+110.001 s]
Raw data (loadavg): 0.96 0.94 0.91 2/54 29174
Raw data (stat): 29174 (minisat+) R 29173 25347 25346 0 -1 0 5874 0 0 0 10982 16 0 0 25 0 1 0 421419875 26595328 5663 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6493 5663 603 41 0 6452 0
vsize: 25972
[startup+120.002 s]
Raw data (loadavg): 0.96 0.94 0.91 2/54 29174
Raw data (stat): 29174 (minisat+) R 29173 25347 25346 0 -1 0 5992 0 0 0 11982 17 0 0 25 0 1 0 421419875 26992640 5781 4294967295 134512640 134672761 3221224560 3221223728 134560858 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6590 5781 603 41 0 6549 0
vsize: 26360
[startup+130.001 s]
Raw data (loadavg): 0.97 0.95 0.91 2/54 29174
Raw data (stat): 29174 (minisat+) R 29173 25347 25346 0 -1 0 6101 0 0 0 12981 17 0 0 25 0 1 0 421419875 27525120 5890 4294967295 134512640 134672761 3221224560 3221223712 134565029 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6720 5890 603 41 0 6679 0
vsize: 26880
[startup+140.001 s]
Raw data (loadavg): 0.97 0.95 0.91 2/54 29174
Raw data (stat): 29174 (minisat+) R 29173 25347 25346 0 -1 0 6240 0 0 0 13981 18 0 0 25 0 1 0 421419875 28307456 6029 4294967295 134512640 134672761 3221224560 3221223728 134561269 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6911 6029 603 41 0 6870 0
vsize: 27644
[startup+150.001 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 29174
Raw data (stat): 29174 (minisat+) R 29173 25347 25346 0 -1 0 6337 0 0 0 14981 18 0 0 25 0 1 0 421419875 28704768 6126 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7008 6126 603 41 0 6967 0
vsize: 28032
[startup+160.001 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 29174
Raw data (stat): 29174 (minisat+) R 29173 25347 25346 0 -1 0 6420 0 0 0 15980 19 0 0 25 0 1 0 421419875 28971008 6209 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7073 6209 603 41 0 7032 0
vsize: 28292
[startup+170.002 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 29174
Raw data (stat): 29174 (minisat+) R 29173 25347 25346 0 -1 0 6518 0 0 0 16980 19 0 0 25 0 1 0 421419875 29380608 6307 4294967295 134512640 134672761 3221224560 3221223728 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7173 6307 603 41 0 7132 0
vsize: 28692
[startup+180.002 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 29174
Raw data (stat): 29174 (minisat+) R 29173 25347 25346 0 -1 0 6605 0 0 0 17979 19 0 0 25 0 1 0 421419875 29786112 6394 4294967295 134512640 134672761 3221224560 3221223696 134560590 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7272 6394 603 41 0 7231 0
vsize: 29088
[startup+190.001 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 29174
Raw data (stat): 29174 (minisat+) R 29173 25347 25346 0 -1 0 6679 0 0 0 18979 20 0 0 25 0 1 0 421419875 30052352 6468 4294967295 134512640 134672761 3221224560 3221223760 134557836 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7337 6468 603 41 0 7296 0
vsize: 29348
[startup+200.002 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 29174
Raw data (stat): 29174 (minisat+) R 29173 25347 25346 0 -1 0 6762 0 0 0 19979 20 0 0 25 0 1 0 421419875 30322688 6551 4294967295 134512640 134672761 3221224560 3221223728 134561215 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7403 6551 603 41 0 7362 0
vsize: 29612
[startup+210.002 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 29174
Raw data (stat): 29174 (minisat+) R 29173 25347 25346 0 -1 0 6882 0 0 0 20979 20 0 0 25 0 1 0 421419875 30928896 6671 4294967295 134512640 134672761 3221224560 3221223696 134560557 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7551 6671 603 41 0 7510 0
vsize: 30204
[startup+220.002 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 29174
Raw data (stat): 29174 (minisat+) R 29173 25347 25346 0 -1 0 6987 0 0 0 21978 21 0 0 25 0 1 0 421419875 31330304 6776 4294967295 134512640 134672761 3221224560 3221223728 134561201 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7649 6776 603 41 0 7608 0
vsize: 30596
[startup+230.002 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 29174
Raw data (stat): 29174 (minisat+) R 29173 25347 25346 0 -1 0 7078 0 0 0 22978 21 0 0 25 0 1 0 421419875 31592448 6867 4294967295 134512640 134672761 3221224560 3221223696 134560622 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7713 6867 603 41 0 7672 0
vsize: 30852
[startup+240.001 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 29174
Raw data (stat): 29174 (minisat+) R 29173 25347 25346 0 -1 0 7177 0 0 0 23978 22 0 0 25 0 1 0 421419875 32137216 6966 4294967295 134512640 134672761 3221224560 3221223712 134561249 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7846 6966 603 41 0 7805 0
vsize: 31384
[startup+250.001 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 29174
Raw data (stat): 29174 (minisat+) R 29173 25347 25346 0 -1 0 7340 0 0 0 24978 22 0 0 25 0 1 0 421419875 32686080 7129 4294967295 134512640 134672761 3221224560 3221223760 134557836 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7980 7129 603 41 0 7939 0
vsize: 31920
[startup+260.001 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 29174
Raw data (stat): 29174 (minisat+) R 29173 25347 25346 0 -1 0 7449 0 0 0 25978 22 0 0 25 0 1 0 421419875 33214464 7238 4294967295 134512640 134672761 3221224560 3221223696 134560588 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8109 7238 603 41 0 8068 0
vsize: 32436
[startup+270.001 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 29174
Raw data (stat): 29174 (minisat+) R 29173 25347 25346 0 -1 0 7540 0 0 0 26977 23 0 0 25 0 1 0 421419875 33476608 7329 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8173 7329 603 41 0 8132 0
vsize: 32692
[startup+280.001 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 29174
Raw data (stat): 29174 (minisat+) R 29173 25347 25346 0 -1 0 7619 0 0 0 27977 23 0 0 25 0 1 0 421419875 33873920 7408 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8270 7408 603 41 0 8229 0
vsize: 33080
[startup+290 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 29174
Raw data (stat): 29174 (minisat+) R 29173 25347 25346 0 -1 0 7722 0 0 0 28977 23 0 0 25 0 1 0 421419875 34279424 7511 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8369 7511 603 41 0 8328 0
vsize: 33476
[startup+300.001 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 29174
Raw data (stat): 29174 (minisat+) R 29173 25347 25346 0 -1 0 7823 0 0 0 29977 24 0 0 25 0 1 0 421419875 35069952 7612 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8562 7612 603 41 0 8521 0
vsize: 34248
[startup+310 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 29174
Raw data (stat): 29174 (minisat+) R 29173 25347 25346 0 -1 0 7925 0 0 0 30976 25 0 0 25 0 1 0 421419875 35471360 7714 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8660 7714 603 41 0 8619 0
vsize: 34640
[startup+320.001 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 29174
Raw data (stat): 29174 (minisat+) R 29173 25347 25346 0 -1 0 8011 0 0 0 31976 25 0 0 25 0 1 0 421419875 35733504 7800 4294967295 134512640 134672761 3221224560 3221223760 134557809 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8724 7800 603 41 0 8683 0
vsize: 34896
[startup+330.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29174
Raw data (stat): 29174 (minisat+) R 29173 25347 25346 0 -1 0 8088 0 0 0 32976 25 0 0 25 0 1 0 421419875 36130816 7877 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8821 7877 603 41 0 8780 0
vsize: 35284
[startup+340.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29174
Raw data (stat): 29174 (minisat+) R 29173 25347 25346 0 -1 0 8146 0 0 0 33976 25 0 0 25 0 1 0 421419875 36261888 7935 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8853 7935 603 41 0 8812 0
vsize: 35412
[startup+350.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29174
Raw data (stat): 29174 (minisat+) R 29173 25347 25346 0 -1 0 8229 0 0 0 34976 26 0 0 25 0 1 0 421419875 36655104 8018 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8949 8018 603 41 0 8908 0
vsize: 35796
[startup+360.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29174
Raw data (stat): 29174 (minisat+) R 29173 25347 25346 0 -1 0 8323 0 0 0 35976 26 0 0 25 0 1 0 421419875 37052416 8112 4294967295 134512640 134672761 3221224560 3221223728 134560833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9046 8112 603 41 0 9005 0
vsize: 36184
[startup+370.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29174
Raw data (stat): 29174 (minisat+) R 29173 25347 25346 0 -1 0 8394 0 0 0 36976 26 0 0 25 0 1 0 421419875 37318656 8183 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9111 8183 603 41 0 9070 0
vsize: 36444
[startup+380.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29174
Raw data (stat): 29174 (minisat+) R 29173 25347 25346 0 -1 0 8455 0 0 0 37976 26 0 0 25 0 1 0 421419875 37580800 8244 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9175 8244 603 41 0 9134 0
vsize: 36700
[startup+390.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29174
Raw data (stat): 29174 (minisat+) R 29173 25347 25346 0 -1 0 8563 0 0 0 38976 26 0 0 25 0 1 0 421419875 37969920 8352 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9270 8352 603 41 0 9229 0
vsize: 37080
[startup+400.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29174
Raw data (stat): 29174 (minisat+) R 29173 25347 25346 0 -1 0 8616 0 0 0 39976 27 0 0 25 0 1 0 421419875 38232064 8405 4294967295 134512640 134672761 3221224560 3221223728 134561167 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9334 8405 603 41 0 9293 0
vsize: 37336
[startup+410.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29174
Raw data (stat): 29174 (minisat+) R 29173 25347 25346 0 -1 0 8688 0 0 0 40976 27 0 0 25 0 1 0 421419875 38617088 8477 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9428 8477 603 41 0 9387 0
vsize: 37712
[startup+420.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29174
Raw data (stat): 29174 (minisat+) R 29173 25347 25346 0 -1 0 8757 0 0 0 41974 28 0 0 25 0 1 0 421419875 38887424 8546 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9494 8546 603 41 0 9453 0
vsize: 37976
[startup+430.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29174
Raw data (stat): 29174 (minisat+) R 29173 25347 25346 0 -1 0 8877 0 0 0 42974 28 0 0 25 0 1 0 421419875 39272448 8666 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9588 8666 603 41 0 9547 0
vsize: 38352
[startup+440.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29174
Raw data (stat): 29174 (minisat+) R 29173 25347 25346 0 -1 0 8948 0 0 0 43974 28 0 0 25 0 1 0 421419875 39665664 8737 4294967295 134512640 134672761 3221224560 3221223696 134560588 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9684 8737 603 41 0 9643 0
vsize: 38736
[startup+450.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29174
Raw data (stat): 29174 (minisat+) R 29173 25347 25346 0 -1 0 9036 0 0 0 44974 28 0 0 25 0 1 0 421419875 39927808 8825 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9748 8825 603 41 0 9707 0
vsize: 38992
[startup+460.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29174
Raw data (stat): 29174 (minisat+) R 29173 25347 25346 0 -1 0 9112 0 0 0 45974 29 0 0 25 0 1 0 421419875 40189952 8901 4294967295 134512640 134672761 3221224560 3221223760 134557895 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9812 8901 603 41 0 9771 0
vsize: 39248
[startup+470.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29174
Raw data (stat): 29174 (minisat+) R 29173 25347 25346 0 -1 0 9186 0 0 0 46974 29 0 0 25 0 1 0 421419875 40587264 8975 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9909 8975 603 41 0 9868 0
vsize: 39636
[startup+480.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29174
Raw data (stat): 29174 (minisat+) R 29173 25347 25346 0 -1 0 9255 0 0 0 47974 29 0 0 25 0 1 0 421419875 40853504 9044 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9974 9044 603 41 0 9933 0
vsize: 39896
[startup+490.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29174
Raw data (stat): 29174 (minisat+) R 29173 25347 25346 0 -1 0 9328 0 0 0 48974 29 0 0 25 0 1 0 421419875 41119744 9117 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10039 9117 603 41 0 9998 0
vsize: 40156
[startup+500.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29174
Raw data (stat): 29174 (minisat+) R 29173 25347 25346 0 -1 0 9397 0 0 0 49974 29 0 0 25 0 1 0 421419875 41447424 9186 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10119 9186 603 41 0 10078 0
vsize: 40476
[startup+510.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29174
Raw data (stat): 29174 (minisat+) R 29173 25347 25346 0 -1 0 9483 0 0 0 50974 30 0 0 25 0 1 0 421419875 41762816 9272 4294967295 134512640 134672761 3221224560 3221223708 134560552 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10196 9272 603 41 0 10155 0
vsize: 40784
[startup+520.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29174
Raw data (stat): 29174 (minisat+) R 29173 25347 25346 0 -1 0 9555 0 0 0 51974 30 0 0 25 0 1 0 421419875 42291200 9344 4294967295 134512640 134672761 3221224560 3221223696 134560588 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10325 9344 603 41 0 10284 0
vsize: 41300
[startup+530.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29174
Raw data (stat): 29174 (minisat+) R 29173 25347 25346 0 -1 0 9627 0 0 0 52974 31 0 0 25 0 1 0 421419875 42557440 9416 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10390 9416 603 41 0 10349 0
vsize: 41560
[startup+540.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29174
Raw data (stat): 29174 (minisat+) R 29173 25347 25346 0 -1 0 9700 0 0 0 53974 31 0 0 25 0 1 0 421419875 42819584 9489 4294967295 134512640 134672761 3221224560 3221223728 134560968 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10454 9489 603 41 0 10413 0
vsize: 41816
[startup+550.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29174
Raw data (stat): 29174 (minisat+) R 29173 25347 25346 0 -1 0 9771 0 0 0 54974 31 0 0 25 0 1 0 421419875 43081728 9560 4294967295 134512640 134672761 3221224560 3221223728 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10518 9560 603 41 0 10477 0
vsize: 42072
[startup+560.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29174
Raw data (stat): 29174 (minisat+) R 29173 25347 25346 0 -1 0 9840 0 0 0 55974 31 0 0 25 0 1 0 421419875 43474944 9629 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10614 9629 603 41 0 10573 0
vsize: 42456
[startup+570.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29174
Raw data (stat): 29174 (minisat+) R 29173 25347 25346 0 -1 0 9892 0 0 0 56974 31 0 0 25 0 1 0 421419875 43610112 9681 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10647 9681 603 41 0 10606 0
vsize: 42588
[startup+580.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29174
Raw data (stat): 29174 (minisat+) R 29173 25347 25346 0 -1 0 9945 0 0 0 57974 31 0 0 25 0 1 0 421419875 43876352 9734 4294967295 134512640 134672761 3221224560 3221223696 134560566 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10712 9734 603 41 0 10671 0
vsize: 42848
[startup+590.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29174
Raw data (stat): 29174 (minisat+) R 29173 25347 25346 0 -1 0 10072 0 0 0 58974 32 0 0 25 0 1 0 421419875 44400640 9861 4294967295 134512640 134672761 3221224560 3221223696 134560598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10840 9861 603 41 0 10799 0
vsize: 43360
[startup+600.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29174
Raw data (stat): 29174 (minisat+) R 29173 25347 25346 0 -1 0 10141 0 0 0 59973 32 0 0 25 0 1 0 421419875 44662784 9930 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10904 9930 603 41 0 10863 0
vsize: 43616
[startup+610.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29174
Raw data (stat): 29174 (minisat+) R 29173 25347 25346 0 -1 0 10201 0 0 0 60973 33 0 0 25 0 1 0 421419875 44793856 9990 4294967295 134512640 134672761 3221224560 3221223708 134560631 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10936 9990 603 41 0 10895 0
vsize: 43744
[startup+620.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29174
Raw data (stat): 29174 (minisat+) R 29173 25347 25346 0 -1 0 10250 0 0 0 61973 33 0 0 25 0 1 0 421419875 45056000 10039 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11000 10039 603 41 0 10959 0
vsize: 44000
[startup+630.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29174
Raw data (stat): 29174 (minisat+) R 29173 25347 25346 0 -1 0 10296 0 0 0 62973 33 0 0 25 0 1 0 421419875 45187072 10085 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11032 10085 603 41 0 10991 0
vsize: 44128
[startup+640.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29174
Raw data (stat): 29174 (minisat+) R 29173 25347 25346 0 -1 0 10339 0 0 0 63973 33 0 0 25 0 1 0 421419875 45449216 10128 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11096 10128 603 41 0 11055 0
vsize: 44384
[startup+650.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29174
Raw data (stat): 29174 (minisat+) R 29173 25347 25346 0 -1 0 10383 0 0 0 64973 33 0 0 25 0 1 0 421419875 45580288 10172 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11128 10172 603 41 0 11087 0
vsize: 44512
[startup+660.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29174
Raw data (stat): 29174 (minisat+) R 29173 25347 25346 0 -1 0 10412 0 0 0 65973 33 0 0 25 0 1 0 421419875 45715456 10201 4294967295 134512640 134672761 3221224560 3221223728 134560822 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11161 10201 603 41 0 11120 0
vsize: 44644
[startup+670.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29174
Raw data (stat): 29174 (minisat+) R 29173 25347 25346 0 -1 0 10451 0 0 0 66974 33 0 0 25 0 1 0 421419875 46370816 10240 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11321 10240 603 41 0 11280 0
vsize: 45284
[startup+680.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29174
Raw data (stat): 29174 (minisat+) R 29173 25347 25346 0 -1 0 10559 0 0 0 67973 33 0 0 25 0 1 0 421419875 46796800 10348 4294967295 134512640 134672761 3221224560 3221223728 134561127 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11425 10348 603 41 0 11384 0
vsize: 45700
[startup+690.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29174
Raw data (stat): 29174 (minisat+) R 29173 25347 25346 0 -1 0 10619 0 0 0 68973 34 0 0 25 0 1 0 421419875 47087616 10408 4294967295 134512640 134672761 3221224560 3221223760 134557849 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11496 10408 603 41 0 11455 0
vsize: 45984
[startup+700 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29174
Raw data (stat): 29174 (minisat+) R 29173 25347 25346 0 -1 0 10683 0 0 0 69973 34 0 0 25 0 1 0 421419875 47505408 10472 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11598 10472 603 41 0 11557 0
vsize: 46392
[startup+710 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29174
Raw data (stat): 29174 (minisat+) R 29173 25347 25346 0 -1 0 10750 0 0 0 70973 34 0 0 25 0 1 0 421419875 47767552 10539 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11662 10539 603 41 0 11621 0
vsize: 46648
[startup+719.999 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29174
Raw data (stat): 29174 (minisat+) R 29173 25347 25346 0 -1 0 10813 0 0 0 71972 34 0 0 25 0 1 0 421419875 48029696 10602 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11726 10602 603 41 0 11685 0
vsize: 46904
[startup+729.999 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29174
Raw data (stat): 29174 (minisat+) R 29173 25347 25346 0 -1 0 10868 0 0 0 72972 34 0 0 25 0 1 0 421419875 48291840 10657 4294967295 134512640 134672761 3221224560 3221223728 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11790 10657 603 41 0 11749 0
vsize: 47160
[startup+739.999 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29174
Raw data (stat): 29174 (minisat+) R 29173 25347 25346 0 -1 0 10915 0 0 0 73972 35 0 0 25 0 1 0 421419875 48427008 10704 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11823 10704 603 41 0 11782 0
vsize: 47292
[startup+749.999 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29174
Raw data (stat): 29174 (minisat+) R 29173 25347 25346 0 -1 0 10967 0 0 0 74972 35 0 0 25 0 1 0 421419875 48689152 10756 4294967295 134512640 134672761 3221224560 3221223728 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11887 10756 603 41 0 11846 0
vsize: 47548
[startup+759.999 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29174
Raw data (stat): 29174 (minisat+) R 29173 25347 25346 0 -1 0 11016 0 0 0 75972 35 0 0 25 0 1 0 421419875 48824320 10805 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11920 10805 603 41 0 11879 0
vsize: 47680
[startup+769.998 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29174
Raw data (stat): 29174 (minisat+) R 29173 25347 25346 0 -1 0 11064 0 0 0 76972 35 0 0 25 0 1 0 421419875 49086464 10853 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11984 10853 603 41 0 11943 0
vsize: 47936
[startup+779.999 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29174
Raw data (stat): 29174 (minisat+) R 29173 25347 25346 0 -1 0 11112 0 0 0 77972 35 0 0 25 0 1 0 421419875 49221632 10901 4294967295 134512640 134672761 3221224560 3221223696 134560588 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12017 10901 603 41 0 11976 0
vsize: 48068
[startup+789.998 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29174
Raw data (stat): 29174 (minisat+) R 29173 25347 25346 0 -1 0 11156 0 0 0 78972 35 0 0 25 0 1 0 421419875 49356800 10945 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12050 10945 603 41 0 12009 0
vsize: 48200
[startup+799.998 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29174
Raw data (stat): 29174 (minisat+) R 29173 25347 25346 0 -1 0 11207 0 0 0 79972 36 0 0 25 0 1 0 421419875 49623040 10996 4294967295 134512640 134672761 3221224560 3221223728 134560895 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12115 10996 603 41 0 12074 0
vsize: 48460
[startup+809.999 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29174
Raw data (stat): 29174 (minisat+) R 29173 25347 25346 0 -1 0 11296 0 0 0 80972 36 0 0 25 0 1 0 421419875 50016256 11085 4294967295 134512640 134672761 3221224560 3221223728 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12211 11085 603 41 0 12170 0
vsize: 48844
[startup+819.998 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29174
Raw data (stat): 29174 (minisat+) R 29173 25347 25346 0 -1 0 11376 0 0 0 81972 36 0 0 25 0 1 0 421419875 50409472 11165 4294967295 134512640 134672761 3221224560 3221223696 134560588 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12307 11165 603 41 0 12266 0
vsize: 49228
[startup+829.998 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29174
Raw data (stat): 29174 (minisat+) R 29173 25347 25346 0 -1 0 11451 0 0 0 82972 37 0 0 25 0 1 0 421419875 50671616 11240 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12371 11240 603 41 0 12330 0
vsize: 49484
[startup+839.997 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29174
Raw data (stat): 29174 (minisat+) R 29173 25347 25346 0 -1 0 11521 0 0 0 83972 37 0 0 25 0 1 0 421419875 50941952 11310 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12437 11310 603 41 0 12396 0
vsize: 49748
[startup+849.998 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29174
Raw data (stat): 29174 (minisat+) R 29173 25347 25346 0 -1 0 11568 0 0 0 84972 37 0 0 25 0 1 0 421419875 51073024 11357 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12469 11357 603 41 0 12428 0
vsize: 49876
[startup+859.998 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29174
Raw data (stat): 29174 (minisat+) R 29173 25347 25346 0 -1 0 11622 0 0 0 85972 37 0 0 25 0 1 0 421419875 51335168 11411 4294967295 134512640 134672761 3221224560 3221223728 134560867 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12533 11411 603 41 0 12492 0
vsize: 50132
[startup+869.997 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29174
Raw data (stat): 29174 (minisat+) R 29173 25347 25346 0 -1 0 11660 0 0 0 86973 37 0 0 25 0 1 0 421419875 51466240 11449 4294967295 134512640 134672761 3221224560 3221223728 134561167 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12565 11449 603 41 0 12524 0
vsize: 50260
[startup+879.997 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29174
Raw data (stat): 29174 (minisat+) R 29173 25347 25346 0 -1 0 11706 0 0 0 87973 37 0 0 25 0 1 0 421419875 51728384 11495 4294967295 134512640 134672761 3221224560 3221223728 134561018 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12629 11495 603 41 0 12588 0
vsize: 50516
[startup+889.997 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29174
Raw data (stat): 29174 (minisat+) R 29173 25347 25346 0 -1 0 11760 0 0 0 88973 37 0 0 25 0 1 0 421419875 51863552 11549 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12662 11549 603 41 0 12621 0
vsize: 50648
[startup+899.997 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29174
Raw data (stat): 29174 (minisat+) R 29173 25347 25346 0 -1 0 11829 0 0 0 89973 37 0 0 25 0 1 0 421419875 52133888 11618 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12728 11618 603 41 0 12687 0
vsize: 50912
[startup+909.996 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29174
Raw data (stat): 29174 (minisat+) R 29173 25347 25346 0 -1 0 11889 0 0 0 90973 37 0 0 25 0 1 0 421419875 52396032 11678 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12792 11678 603 41 0 12751 0
vsize: 51168
[startup+919.996 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29174
Raw data (stat): 29174 (minisat+) R 29173 25347 25346 0 -1 0 11942 0 0 0 91972 38 0 0 25 0 1 0 421419875 52658176 11731 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12856 11731 603 41 0 12815 0
vsize: 51424
[startup+929.996 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29174
Raw data (stat): 29174 (minisat+) R 29173 25347 25346 0 -1 0 11988 0 0 0 92972 38 0 0 25 0 1 0 421419875 52789248 11777 4294967295 134512640 134672761 3221224560 3221223708 134560552 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12888 11777 603 41 0 12847 0
vsize: 51552
[startup+939.996 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29174
Raw data (stat): 29174 (minisat+) R 29173 25347 25346 0 -1 0 12047 0 0 0 93972 38 0 0 25 0 1 0 421419875 53051392 11836 4294967295 134512640 134672761 3221224560 3221223760 134557830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12952 11836 603 41 0 12911 0
vsize: 51808
[startup+949.996 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29174
Raw data (stat): 29174 (minisat+) R 29173 25347 25346 0 -1 0 12101 0 0 0 94972 39 0 0 25 0 1 0 421419875 53313536 11890 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13016 11890 603 41 0 12975 0
vsize: 52064
[startup+959.996 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29174
Raw data (stat): 29174 (minisat+) R 29173 25347 25346 0 -1 0 12151 0 0 0 95972 39 0 0 25 0 1 0 421419875 53444608 11940 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13048 11940 603 41 0 13007 0
vsize: 52192
[startup+969.996 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29174
Raw data (stat): 29174 (minisat+) R 29173 25347 25346 0 -1 0 12204 0 0 0 96972 39 0 0 25 0 1 0 421419875 53706752 11993 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13112 11993 603 41 0 13071 0
vsize: 52448
[startup+979.996 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29174
Raw data (stat): 29174 (minisat+) R 29173 25347 25346 0 -1 0 12253 0 0 0 97972 39 0 0 25 0 1 0 421419875 53837824 12042 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13144 12042 603 41 0 13103 0
vsize: 52576
[startup+989.996 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29174
Raw data (stat): 29174 (minisat+) R 29173 25347 25346 0 -1 0 12303 0 0 0 98972 39 0 0 25 0 1 0 421419875 54104064 12092 4294967295 134512640 134672761 3221224560 3221223696 134560661 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13209 12092 603 41 0 13168 0
vsize: 52836
[startup+999.995 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29174
Raw data (stat): 29174 (minisat+) R 29173 25347 25346 0 -1 0 12340 0 0 0 99972 39 0 0 25 0 1 0 421419875 54235136 12129 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13241 12129 603 41 0 13200 0
vsize: 52964
[startup+1009.99 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29174
Raw data (stat): 29174 (minisat+) R 29173 25347 25346 0 -1 0 12392 0 0 0 100972 39 0 0 25 0 1 0 421419875 54366208 12181 4294967295 134512640 134672761 3221224560 3221223760 134557836 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13273 12181 603 41 0 13232 0
vsize: 53092
[startup+1019.99 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29174
Raw data (stat): 29174 (minisat+) R 29173 25347 25346 0 -1 0 12486 0 0 0 101972 40 0 0 25 0 1 0 421419875 54890496 12275 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13401 12275 603 41 0 13360 0
vsize: 53604
[startup+1029.99 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29174
Raw data (stat): 29174 (minisat+) R 29173 25347 25346 0 -1 0 12524 0 0 0 102972 40 0 0 25 0 1 0 421419875 55140352 12313 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13462 12313 603 41 0 13421 0
vsize: 53848
[startup+1039.99 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29174
Raw data (stat): 29174 (minisat+) R 29173 25347 25346 0 -1 0 12525 0 0 0 103972 40 0 0 25 0 1 0 421419875 55140352 12314 4294967295 134512640 134672761 3221224560 3221223712 134554662 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13462 12314 603 41 0 13421 0
vsize: 53848
[startup+1049.99 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29174
Raw data (stat): 29174 (minisat+) R 29173 25347 25346 0 -1 0 12525 0 0 0 104972 40 0 0 25 0 1 0 421419875 55140352 12314 4294967295 134512640 134672761 3221224560 3221223712 134554662 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13462 12314 603 41 0 13421 0
vsize: 53848
[startup+1059.99 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29174
Raw data (stat): 29174 (minisat+) R 29173 25347 25346 0 -1 0 12525 0 0 0 105972 40 0 0 25 0 1 0 421419875 55140352 12314 4294967295 134512640 134672761 3221224560 3221223712 134554642 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13462 12314 603 41 0 13421 0
vsize: 53848
[startup+1069.99 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29174
Raw data (stat): 29174 (minisat+) R 29173 25347 25346 0 -1 0 12525 0 0 0 106973 40 0 0 25 0 1 0 421419875 55140352 12314 4294967295 134512640 134672761 3221224560 3221223712 134554677 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13462 12314 603 41 0 13421 0
vsize: 53848
[startup+1079.99 s]
Raw data (loadavg): 0.99 0.97 0.91 3/57 29211
Raw data (stat): 29174 (minisat+) R 29173 25347 25346 0 -1 0 12525 0 0 0 107973 40 0 0 25 0 1 0 421419875 55140352 12314 4294967295 134512640 134672761 3221224560 3221223712 134554656 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13462 12314 603 41 0 13421 0
vsize: 53848
[startup+1089.99 s]
Raw data (loadavg): 1.07 0.99 0.91 2/54 29227
Raw data (stat): 29174 (minisat+) R 29173 25347 25346 0 -1 0 12525 0 0 0 108973 40 0 0 25 0 1 0 421419875 55140352 12314 4294967295 134512640 134672761 3221224560 3221223712 134554636 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13462 12314 603 41 0 13421 0
vsize: 53848
[startup+1099.99 s]
Raw data (loadavg): 1.06 0.99 0.91 2/54 29227
Raw data (stat): 29174 (minisat+) R 29173 25347 25346 0 -1 0 12525 0 0 0 109973 40 0 0 25 0 1 0 421419875 55140352 12314 4294967295 134512640 134672761 3221224560 3221223712 134554642 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13462 12314 603 41 0 13421 0
vsize: 53848
[startup+1109.99 s]
Raw data (loadavg): 1.05 0.99 0.91 2/54 29227
Raw data (stat): 29174 (minisat+) R 29173 25347 25346 0 -1 0 12525 0 0 0 110973 40 0 0 25 0 1 0 421419875 55140352 12314 4294967295 134512640 134672761 3221224560 3221223712 134554662 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13462 12314 603 41 0 13421 0
vsize: 53848
[startup+1119.99 s]
Raw data (loadavg): 1.04 0.99 0.91 2/54 29227
Raw data (stat): 29174 (minisat+) R 29173 25347 25346 0 -1 0 12525 0 0 0 111973 40 0 0 25 0 1 0 421419875 55140352 12314 4294967295 134512640 134672761 3221224560 3221223732 134556632 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13462 12314 603 41 0 13421 0
vsize: 53848
[startup+1129.99 s]
Raw data (loadavg): 1.03 0.99 0.91 2/54 29227
Raw data (stat): 29174 (minisat+) R 29173 25347 25346 0 -1 0 12525 0 0 0 112974 40 0 0 25 0 1 0 421419875 55140352 12314 4294967295 134512640 134672761 3221224560 3221223696 134560588 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13462 12314 603 41 0 13421 0
vsize: 53848
[startup+1139.99 s]
Raw data (loadavg): 1.03 0.99 0.91 2/54 29227
Raw data (stat): 29174 (minisat+) R 29173 25347 25346 0 -1 0 12525 0 0 0 113974 40 0 0 25 0 1 0 421419875 55140352 12314 4294967295 134512640 134672761 3221224560 3221223696 134560729 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13462 12314 603 41 0 13421 0
vsize: 53848
[startup+1149.99 s]
Raw data (loadavg): 1.02 0.99 0.91 2/54 29227
Raw data (stat): 29174 (minisat+) R 29173 25347 25346 0 -1 0 12525 0 0 0 114974 40 0 0 25 0 1 0 421419875 55140352 12314 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13462 12314 603 41 0 13421 0
vsize: 53848
[startup+1159.99 s]
Raw data (loadavg): 1.02 0.99 0.91 2/54 29229
Raw data (stat): 29174 (minisat+) R 29173 25347 25346 0 -1 0 12525 0 0 0 115974 40 0 0 25 0 1 0 421419875 55140352 12314 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13462 12314 603 41 0 13421 0
vsize: 53848
[startup+1169.99 s]
Raw data (loadavg): 1.02 0.99 0.91 2/54 29229
Raw data (stat): 29174 (minisat+) R 29173 25347 25346 0 -1 0 12525 0 0 0 116974 40 0 0 25 0 1 0 421419875 55140352 12314 4294967295 134512640 134672761 3221224560 3221223760 134557913 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13462 12314 603 41 0 13421 0
vsize: 53848
[startup+1179.99 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 29229
Raw data (stat): 29174 (minisat+) R 29173 25347 25346 0 -1 0 12525 0 0 0 117974 40 0 0 25 0 1 0 421419875 55140352 12314 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13462 12314 603 41 0 13421 0
vsize: 53848
[startup+1189.99 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 29229
Raw data (stat): 29174 (minisat+) R 29173 25347 25346 0 -1 0 12525 0 0 0 118974 40 0 0 25 0 1 0 421419875 55140352 12314 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13462 12314 603 41 0 13421 0
vsize: 53848
[startup+1199.99 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 29229
Raw data (stat): 29174 (minisat+) R 29173 25347 25346 0 -1 0 12525 0 0 0 119974 40 0 0 25 0 1 0 421419875 55140352 12314 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13462 12314 603 41 0 13421 0
vsize: 53848
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.02 s]
Raw data (loadavg): 1.01 0.99 0.91 1/54 29229
Raw data (stat): 29174 (minisat+) Z 29173 25347 25346 0 -1 12 12527 0 0 0 119974 43 0 0 25 0 1 0 421419875 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.02
CPU time (s): 1200.18
CPU user time (s): 1199.74
CPU system time (s): 0.432934
CPU usage (%): 100.013
Max. virtual memory (Kb): 53848
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####