PB'05 competition: run trace

Some explanations

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

Name	normalized-opb/mps-v2-13-7/MIPLIB/miplib3/normalized-mps-v2-13-7-dano3mip.opb
MD5SUM	a9d7b9b5569d1dec981f274df34ef66e
Bench Category	optimization, medium integers (OPTMEDINT)
Has Objective Function	YES
Satisfiable	NO
(Un)Satisfiability was proved
Best value of the objective function
Optimality of the best value was proved
Number of terms in the objective function	20
Biggest coefficient in the objective function	524288
Number of bits for the biggest coefficient in the objective function	20
Sum of the numbers in the objective function	1048575
Number of bits of the sum of numbers in the objective function	20
Biggest number in a constraint	65536000
Number of bits of the biggest number in a constraint	26
Biggest sum of numbers in a constraint	555744750
Number of bits of the biggest sum of numbers	30
Best result obtained on this benchmark	UNSAT
Best CPU time to get the best result obtained on this benchmark	35.1067
Number of variables	266924
Total number of constraints	3778
Number of constraints which are clauses	0
Number of constraints which are cardinality constraints (but not clauses)	600
Number of constraints which are nor clauses,nor cardinality constraints	3178
Minimum length of a constraint	1
Maximum length of a constraint	10600
Trace number 15154

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

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.220
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	: 901.12

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        764480 kB
Buffers:         12768 kB
Cached:         236652 kB
SwapCached:        820 kB
Active:          58768 kB
Inactive:       192772 kB
HighTotal:      131008 kB
HighFree:          252 kB
LowTotal:       903652 kB
LowFree:        764228 kB
SwapTotal:     2097892 kB
SwapFree:      2096248 kB
Dirty:              32 kB
Writeback:           0 kB
Mapped:           5024 kB
Slab:            12932 kB
Committed_AS:    63596 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-21 03:22:06 (client local time) WITH STATUS 0 IN 161.492 SECONDS
stats: 18265 7 161.492 0
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 4450 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: ########################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################===============
c   -- Clauses(.)/Splits(s): sssssssssssssssssssssssssssssssssssssssss
c ---[4490]---> BDD-cost:   17
c ---[4489]---> BDD-cost:   17
c ---[4488]---> BDD-cost:   17
c ---[4487]---> BDD-cost:   17
c ---[4486]---> BDD-cost:   17
c ---[4485]---> BDD-cost:   17
c ---[4484]---> BDD-cost:   17
c ---[4483]---> BDD-cost:   17
c ---[4482]---> BDD-cost:   17
c ---[4481]---> BDD-cost:   17
c ---[4480]---> BDD-cost:   17
c ---[4479]---> BDD-cost:   17
c ---[4478]---> BDD-cost:   17
c ---[4477]---> BDD-cost:   17
c ---[4476]---> BDD-cost:   17
c ---[4475]---> BDD-cost:   17
c ---[4474]---> BDD-cost:   17
c ---[4473]---> BDD-cost:   17
c ---[4472]---> BDD-cost:   17
c ---[4471]---> BDD-cost:   17
c ---[4470]---> BDD-cost:   17
c ---[4469]---> BDD-cost:   17
c ---[4468]---> BDD-cost:   17
c ---[4467]---> BDD-cost:   17
c ---[4465]---> Adder-cost: 1496   maxlim: 3011561   bits: 23/22
c ---[4463]---> Adder-cost: 1496   maxlim: 3009129   bits: 23/22
c ---[4461]---> Adder-cost: 1496   maxlim: 3011689   bits: 23/22
c ---[4459]---> Adder-cost: 1496   maxlim: 3011945   bits: 23/22
c ---[4457]---> Adder-cost: 1496   maxlim: 3009385   bits: 23/22
c ---[4455]---> Adder-cost: 1496   maxlim: 3006825   bits: 23/22
c ---[4453]---> Adder-cost: 1496   maxlim: 3011945   bits: 23/22
c ---[4451]---> Adder-cost: 1496   maxlim: 3012073   bits: 23/22
c ---[4449]---> Adder-cost: 1496   maxlim: 3014633   bits: 23/22
c ---[4447]---> Adder-cost: 1496   maxlim: 3014633   bits: 23/22
c ---[4445]---> Adder-cost: 1496   maxlim: 3014633   bits: 23/22
c ---[4443]---> Adder-cost: 1496   maxlim: 3014633   bits: 23/22
c ---[4441]---> Adder-cost: 1496   maxlim: 3014633   bits: 23/22
c ---[4439]---> Adder-cost: 1496   maxlim: 2943977   bits: 23/22
c ---[4437]---> Adder-cost: 1496   maxlim: 3014633   bits: 23/22
c ---[4435]---> Adder-cost: 1496   maxlim: 3014633   bits: 23/22
c ---[4433]---> Adder-cost: 1496   maxlim: 3014633   bits: 23/22
c ---[4431]---> Adder-cost: 1496   maxlim: 3014633   bits: 23/22
c ---[4429]---> Adder-cost: 1496   maxlim: 3014633   bits: 23/22
c ---[4427]---> Adder-cost: 1496   maxlim: 3011561   bits: 23/22
c ---[4425]---> Adder-cost: 1496   maxlim: 3012201   bits: 23/22
c ---[4423]---> Adder-cost: 1496   maxlim: 3011689   bits: 23/22
c ---[4421]---> Adder-cost: 1496   maxlim: 3014633   bits: 23/22
c ---[4419]---> Adder-cost: 1496   maxlim: 3014633   bits: 23/22
c ---[4417]---> Adder-cost: 1496   maxlim: 3014633   bits: 23/22
c ---[4415]---> Adder-cost: 1496   maxlim: 3014633   bits: 23/22
c ---[4413]---> Adder-cost: 1496   maxlim: 3011945   bits: 23/22
c ---[4411]---> Adder-cost: 1496   maxlim: 3012329   bits: 23/22
c ---[4409]---> Adder-cost: 1496   maxlim: 3009641   bits: 23/22
c ---[4407]---> Adder-cost: 1496   maxlim: 3011689   bits: 23/22
c ---[4405]---> Adder-cost: 1496   maxlim: 3014633   bits: 23/22
c ---[4403]---> Adder-cost: 1496   maxlim: 3014633   bits: 23/22
c ---[4401]---> Adder-cost: 1496   maxlim: 3009513   bits: 23/22
c ---[4399]---> Adder-cost: 1496   maxlim: 3012201   bits: 23/22
c ---[4397]---> Adder-cost: 1496   maxlim: 3006441   bits: 23/22
c ---[4395]---> Adder-cost: 1496   maxlim: 3012201   bits: 23/22
c ---[4393]---> Adder-cost: 1496   maxlim: 3012457   bits: 23/22
c ---[4391]---> Adder-cost: 1496   maxlim: 2940905   bits: 23/22
c ---[4389]---> Adder-cost: 1496   maxlim: 3004393   bits: 23/22
c ---[4387]---> Adder-cost: 1496   maxlim: 3014633   bits: 23/22
c ---[4385]---> Adder-cost: 1496   maxlim: 3014633   bits: 23/22
c ---[4383]---> Adder-cost: 1496   maxlim: 3011817   bits: 23/22
c ---[4381]---> Adder-cost: 1496   maxlim: 2946025   bits: 23/22
c ---[4379]---> Adder-cost: 1496   maxlim: 3012329   bits: 23/22
c ---[4377]---> Adder-cost: 1496   maxlim: 3012201   bits: 23/22
c ---[4375]---> Adder-cost: 1496   maxlim: 3014633   bits: 23/22
c ---[4373]---> Adder-cost: 1496   maxlim: 3012585   bits: 23/22
c ---[4371]---> Adder-cost: 1496   maxlim: 3014633   bits: 23/22
c ---[4369]---> Adder-cost: 1496   maxlim: 3012073   bits: 23/22
c ---[4367]---> Adder-cost: 1496   maxlim: 3009001   bits: 23/22
c ---[4365]---> Adder-cost: 1496   maxlim: 3014633   bits: 23/22
c ---[4363]---> Adder-cost: 1496   maxlim: 3009257   bits: 23/22
c ---[4361]---> Adder-cost: 1496   maxlim: 3011817   bits: 23/22
c ---[4359]---> Adder-cost: 1496   maxlim: 3012073   bits: 23/22
c ---[4357]---> Adder-cost: 1496   maxlim: 3014633   bits: 23/22
c ---[4355]---> Adder-cost: 1496   maxlim: 3014633   bits: 23/22
c ---[4353]---> Adder-cost: 1496   maxlim: 3011689   bits: 23/22
c ---[4351]---> Adder-cost: 1496   maxlim: 3011945   bits: 23/22
c ---[4349]---> Adder-cost: 1496   maxlim: 3014633   bits: 23/22
c ---[4347]---> Adder-cost: 1496   maxlim: 3009513   bits: 23/22
c ---[4345]---> Adder-cost: 1496   maxlim: 3011945   bits: 23/22
c ---[4343]---> Adder-cost: 1496   maxlim: 3009769   bits: 23/22
c ---[4341]---> Adder-cost: 1496   maxlim: 3002217   bits: 23/22
c ---[4339]---> Adder-cost: 1496   maxlim: 3011817   bits: 23/22
c ---[4337]---> Adder-cost: 1496   maxlim: 3012457   bits: 23/22
c ---[4335]---> Adder-cost: 1496   maxlim: 3012073   bits: 23/22
c ---[4333]---> Adder-cost: 1496   maxlim: 3009897   bits: 23/22
c ---[4331]---> Adder-cost: 1496   maxlim: 3012457   bits: 23/22
c ---[4329]---> Adder-cost: 1496   maxlim: 3012073   bits: 23/22
c ---[4327]---> Adder-cost: 1496   maxlim: 3009257   bits: 23/22
c ---[4325]---> Adder-cost: 1496   maxlim: 3012073   bits: 23/22
c ---[4323]---> Adder-cost: 1496   maxlim: 3012329   bits: 23/22
c ---[4321]---> Adder-cost: 1496   maxlim: 3009513   bits: 23/22
c ---[4319]---> Adder-cost: 1496   maxlim: 3007337   bits: 23/22
c ---[4317]---> Adder-cost: 1496   maxlim: 3009129   bits: 23/22
c ---[4315]---> Adder-cost: 1496   maxlim: 3009257   bits: 23/22
c ---[4313]---> Adder-cost: 1496   maxlim: 3014633   bits: 23/22
c ---[4311]---> Adder-cost: 1496   maxlim: 2949097   bits: 23/22
c ---[4309]---> Adder-cost: 1496   maxlim: 3012201   bits: 23/22
c ---[4307]---> Adder-cost: 1496   maxlim: 3012457   bits: 23/22
c ---[4305]---> Adder-cost: 1496   maxlim: 3014633   bits: 23/22
c ---[4303]---> Adder-cost: 1496   maxlim: 3009641   bits: 23/22
c ---[4301]---> Adder-cost: 1496   maxlim: 3014633   bits: 23/22
c ---[4299]---> Adder-cost: 1496   maxlim: 3014633   bits: 23/22
c ---[4297]---> Adder-cost: 1496   maxlim: 3011817   bits: 23/22
c ---[4295]---> Adder-cost: 1496   maxlim: 3009385   bits: 23/22
c ---[4293]---> Adder-cost: 1496   maxlim: 3014633   bits: 23/22
c ---[4291]---> Adder-cost: 1496   maxlim: 3014633   bits: 23/22
c ---[4289]---> Adder-cost: 1496   maxlim: 3012457   bits: 23/22
c ---[4287]---> Adder-cost: 1496   maxlim: 3009257   bits: 23/22
c ---[4285]---> Adder-cost: 1496   maxlim: 2943977   bits: 23/22
c ---[4283]---> Adder-cost: 1496   maxlim: 3009129   bits: 23/22
c ---[4281]---> Adder-cost: 1496   maxlim: 3014633   bits: 23/22
c ---[4279]---> Adder-cost: 1496   maxlim: 3014633   bits: 23/22
c ---[4277]---> Adder-cost: 1496   maxlim: 3014633   bits: 23/22
c ---[4275]---> Adder-cost: 1496   maxlim: 2943977   bits: 23/22
c ---[4273]---> Adder-cost: 1490   maxlim: 3004009   bits: 23/22
c ---[4271]---> Adder-cost: 1496   maxlim: 3006953   bits: 23/22
c ---[4269]---> Adder-cost: 1496   maxlim: 3014633   bits: 23/22
c ---[4267]---> Adder-cost: 1496   maxlim: 3009001   bits: 23/22
c ---[4265]---> Adder-cost: 1496   maxlim: 3014633   bits: 23/22
c ---[4263]---> Adder-cost: 1496   maxlim: 3009897   bits: 23/22
c ---[4261]---> Adder-cost: 1496   maxlim: 3006953   bits: 23/22
c ---[4259]---> Adder-cost: 1496   maxlim: 3014633   bits: 23/22
c ---[4257]---> Adder-cost: 1496   maxlim: 2943977   bits: 23/22
c ---[4255]---> Adder-cost: 1496   maxlim: 3014633   bits: 23/22
c ---[4253]---> Adder-cost: 1496   maxlim: 3014633   bits: 23/22
c ---[4251]---> Adder-cost: 1496   maxlim: 3009513   bits: 23/22
c ---[4249]---> Adder-cost: 1496   maxlim: 3012201   bits: 23/22
c ---[4247]---> Adder-cost: 1496   maxlim: 3014633   bits: 23/22
c ---[4245]---> Adder-cost: 1496   maxlim: 3009641   bits: 23/22
c ---[4243]---> Adder-cost: 1496   maxlim: 3009385   bits: 23/22
c ---[4241]---> Adder-cost: 1496   maxlim: 3012457   bits: 23/22
c ---[4239]---> Adder-cost: 1496   maxlim: 3014633   bits: 23/22
c ---[4237]---> Adder-cost: 1496   maxlim: 3014633   bits: 23/22
c ---[4235]---> Adder-cost: 1496   maxlim: 3006953   bits: 23/22
c ---[4233]---> Adder-cost: 1496   maxlim: 3012329   bits: 23/22
c ---[4231]---> Adder-cost: 1496   maxlim: 3014633   bits: 23/22
c ---[4229]---> Adder-cost: 1496   maxlim: 3009897   bits: 23/22
c ---[4227]---> Adder-cost: 1496   maxlim: 3012329   bits: 23/22
c ---[4225]---> Adder-cost: 1496   maxlim: 3011945   bits: 23/22
c ---[4223]---> Adder-cost: 1496   maxlim: 3009385   bits: 23/22
c ---[4221]---> Adder-cost: 1496   maxlim: 3011689   bits: 23/22
c ---[4219]---> Adder-cost: 1496   maxlim: 3009641   bits: 23/22
c ---[4217]---> Adder-cost: 1496   maxlim: 3014633   bits: 23/22
c ---[4215]---> Adder-cost: 1496   maxlim: 3006569   bits: 23/22
c ---[4213]---> Adder-cost: 1496   maxlim: 3006953   bits: 23/22
c ---[4211]---> Adder-cost: 1496   maxlim: 3009641   bits: 23/22
c ---[4209]---> Adder-cost: 1496   maxlim: 3014633   bits: 23/22
c ---[4207]---> Adder-cost: 1496   maxlim: 3012201   bits: 23/22
c ---[4205]---> Adder-cost: 1496   maxlim: 3014633   bits: 23/22
c ---[4203]---> Adder-cost: 1496   maxlim: 3012585   bits: 23/22
c ---[4201]---> Adder-cost: 1496   maxlim: 3012585   bits: 23/22
c ---[4199]---> Adder-cost: 1496   maxlim: 3014633   bits: 23/22
c ---[4197]---> Adder-cost: 1496   maxlim: 3014633   bits: 23/22
c ---[4195]---> Adder-cost: 1496   maxlim: 3009513   bits: 23/22
c ---[4193]---> Adder-cost: 1496   maxlim: 3014633   bits: 23/22
c ---[4191]---> Adder-cost: 1496   maxlim: 3012585   bits: 23/22
c ---[4189]---> Adder-cost: 1496   maxlim: 3011817   bits: 23/22
c ---[4187]---> Adder-cost: 1496   maxlim: 3014633   bits: 23/22
c ---[4185]---> Adder-cost: 1496   maxlim: 3014633   bits: 23/22
c ---[4183]---> Adder-cost: 1496   maxlim: 2949097   bits: 23/22
c ---[4181]---> Adder-cost: 1496   maxlim: 3014633   bits: 23/22
c ---[4179]---> Adder-cost: 1496   maxlim: 3014633   bits: 23/22
c ---[4177]---> Adder-cost: 1496   maxlim: 2941289   bits: 23/22
c ---[4175]---> Adder-cost: 1496   maxlim: 3010025   bits: 23/22
c ---[4173]---> Adder-cost: 1488   maxlim: 3004393   bits: 23/22
c ---[4171]---> Adder-cost: 1496   maxlim: 3002345   bits: 23/22
c ---[4169]---> Adder-cost: 1496   maxlim: 3012201   bits: 23/22
c ---[4167]---> Adder-cost: 1496   maxlim: 3012201   bits: 23/22
c ---[4165]---> Adder-cost: 1496   maxlim: 3009385   bits: 23/22
c ---[4163]---> Adder-cost: 1496   maxlim: 3012585   bits: 23/22
c ---[4161]---> Adder-cost: 1496   maxlim: 3014633   bits: 23/22
c ---[4159]---> Adder-cost: 1496   maxlim: 3014633   bits: 23/22
c ---[4157]---> Adder-cost: 1496   maxlim: 3014633   bits: 23/22
c ---[4155]---> Adder-cost: 1496   maxlim: 2946281   bits: 23/22
c ---[4153]---> Adder-cost: 1496   maxlim: 3014633   bits: 23/22
c ---[4151]---> Adder-cost: 1496   maxlim: 3009129   bits: 23/22
c ---[4149]---> Adder-cost: 1496   maxlim: 3014633   bits: 23/22
c ---[4147]---> Adder-cost: 1496   maxlim: 2943465   bits: 23/22
c ---[4145]---> Adder-cost: 1496   maxlim: 3011817   bits: 23/22
c ---[4143]---> Adder-cost: 1496   maxlim: 3014633   bits: 23/22
c ---[4141]---> Adder-cost: 1496   maxlim: 3014633   bits: 23/22
c ---[4139]---> Adder-cost: 1496   maxlim: 3012073   bits: 23/22
c ---[4137]---> Adder-cost: 1496   maxlim: 3012201   bits: 23/22
c ---[4135]---> Adder-cost: 1496   maxlim: 3012457   bits: 23/22
c ---[4133]---> Adder-cost: 1496   maxlim: 3012073   bits: 23/22
c ---[4131]---> Adder-cost: 1496   maxlim: 3009513   bits: 23/22
c ---[4129]---> Adder-cost: 1496   maxlim: 3014633   bits: 23/22
c ---[4127]---> Adder-cost: 1496   maxlim: 3006953   bits: 23/22
c ---[4125]---> Adder-cost: 1496   maxlim: 3006825   bits: 23/22
c ---[4123]---> Adder-cost: 1496   maxlim: 3014633   bits: 23/22
c ---[4121]---> Adder-cost: 1496   maxlim: 3012073   bits: 23/22
c ---[4119]---> Adder-cost: 1496   maxlim: 3006697   bits: 23/22
c ---[4117]---> Adder-cost: 1496   maxlim: 3012073   bits: 23/22
c ---[4115]---> Adder-cost: 1496   maxlim: 3014633   bits: 23/22
c ---[4113]---> Adder-cost: 1496   maxlim: 3014633   bits: 23/22
c ---[4111]---> Adder-cost: 1496   maxlim: 3009769   bits: 23/22
c ---[4109]---> Adder-cost: 1496   maxlim: 3014633   bits: 23/22
c ---[4107]---> Adder-cost: 1496   maxlim: 3014633   bits: 23/22
c ---[4105]---> Adder-cost: 1496   maxlim: 3014633   bits: 23/22
c ---[4103]---> Adder-cost: 1496   maxlim: 3014633   bits: 23/22
c ---[4101]---> Adder-cost: 1496   maxlim: 3011561   bits: 23/22
c ---[4099]---> Adder-cost: 1496   maxlim: 3011817   bits: 23/22
c ---[4097]---> Adder-cost: 1496   maxlim: 3011945   bits: 23/22
c ---[4095]---> Adder-cost: 1496   maxlim: 3011817   bits: 23/22
c ---[4093]---> Adder-cost: 1496   maxlim: 3009769   bits: 23/22
c ---[4091]---> Adder-cost: 1496   maxlim: 3014633   bits: 23/22
c ---[4089]---> Adder-cost: 1496   maxlim: 3009001   bits: 23/22
c ---[4087]---> Adder-cost: 1496   maxlim: 3012073   bits: 23/22
c ---[4085]---> Adder-cost: 1496   maxlim: 3009513   bits: 23/22
c ---[4083]---> Adder-cost: 1496   maxlim: 3009641   bits: 23/22
c ---[4081]---> Adder-cost: 1496   maxlim: 3010025   bits: 23/22
c ---[4079]---> Adder-cost: 1496   maxlim: 3011817   bits: 23/22
c ---[4077]---> Adder-cost: 1496   maxlim: 3011945   bits: 23/22
c ---[4075]---> Adder-cost: 1496   maxlim: 3012201   bits: 23/22
c ---[4073]---> Adder-cost: 1496   maxlim: 3009641   bits: 23/22
c ---[4071]---> Adder-cost: 1496   maxlim: 3012201   bits: 23/22
c ---[4069]---> Adder-cost: 1496   maxlim: 3014633   bits: 23/22
c ---[4067]---> Adder-cost: 1496   maxlim: 3014633   bits: 23/22
c ---[4065]---> Adder-cost: 1496   maxlim: 3011945   bits: 23/22
c ---[4063]---> Adder-cost: 1496   maxlim: 3011561   bits: 23/22
c ---[4061]---> Adder-cost: 1496   maxlim: 3012585   bits: 23/22
c ---[4059]---> Adder-cost: 1496   maxlim: 3011689   bits: 23/22
c ---[4057]---> Adder-cost: 1496   maxlim: 3011945   bits: 23/22
c ---[4055]---> Adder-cost: 1496   maxlim: 3009897   bits: 23/22
c ---[4053]---> Adder-cost: 1496   maxlim: 3014633   bits: 23/22
c ---[4051]---> Adder-cost: 1496   maxlim: 3014633   bits: 23/22
c ---[4049]---> Adder-cost: 1496   maxlim: 3011561   bits: 23/22
c ---[4047]---> Adder-cost: 1496   maxlim: 2946153   bits: 23/22
c ---[4045]---> Adder-cost: 1496   maxlim: 3009641   bits: 23/22
c ---[4043]---> Adder-cost: 1496   maxlim: 3012073   bits: 23/22
c ---[4041]---> Adder-cost: 1496   maxlim: 3014633   bits: 23/22
c ---[4039]---> Adder-cost: 1496   maxlim: 3014633   bits: 23/22
c ---[4037]---> Adder-cost: 1496   maxlim: 3009385   bits: 23/22
c ---[4035]---> Adder-cost: 1496   maxlim: 3014633   bits: 23/22
c ---[4033]---> Adder-cost: 1496   maxlim: 2949097   bits: 23/22
c ---[4031]---> Adder-cost: 1496   maxlim: 3011817   bits: 23/22
c ---[4029]---> Adder-cost: 1496   maxlim: 3014633   bits: 23/22
c ---[4027]---> Adder-cost: 1496   maxlim: 3014633   bits: 23/22
c ---[4025]---> Adder-cost: 1496   maxlim: 3009001   bits: 23/22
c ---[4023]---> Adder-cost: 1496   maxlim: 3009257   bits: 23/22
c ---[4021]---> Adder-cost: 1496   maxlim: 3011817   bits: 23/22
c ---[4019]---> Adder-cost: 1490   maxlim: 3009257   bits: 23/22
c ---[4017]---> Adder-cost: 1496   maxlim: 2946281   bits: 23/22
c ---[4015]---> Adder-cost: 1496   maxlim: 3012201   bits: 23/22
c ---[4013]---> Adder-cost: 1496   maxlim: 3012073   bits: 23/22
c ---[4011]---> Adder-cost: 1496   maxlim: 3007209   bits: 23/22
c ---[4009]---> Adder-cost: 1496   maxlim: 3012329   bits: 23/22
c ---[4007]---> Adder-cost: 1496   maxlim: 3014633   bits: 23/22
c ---[4005]---> Adder-cost: 1490   maxlim: 3006953   bits: 23/22
c ---[4003]---> Adder-cost: 1496   maxlim: 2941801   bits: 23/22
c ---[4001]---> Adder-cost: 1496   maxlim: 3014633   bits: 23/22
c ---[3999]---> Adder-cost: 1496   maxlim: 3014633   bits: 23/22
c ---[3997]---> Adder-cost: 1496   maxlim: 3012585   bits: 23/22
c ---[3995]---> Adder-cost: 1496   maxlim: 3014633   bits: 23/22
c ---[3993]---> Adder-cost: 1496   maxlim: 3012585   bits: 23/22
c ---[3991]---> Adder-cost: 1496   maxlim: 2944361   bits: 23/22
c ---[3989]---> Adder-cost: 1496   maxlim: 3014633   bits: 23/22
c ---[3987]---> Adder-cost: 1496   maxlim: 3014633   bits: 23/22
c ---[3985]---> Adder-cost: 1496   maxlim: 3009001   bits: 23/22
c ---[3983]---> Adder-cost: 1496   maxlim: 2941033   bits: 23/22
c ---[3981]---> Adder-cost: 1496   maxlim: 3014633   bits: 23/22
c ---[3979]---> Adder-cost: 1496   maxlim: 3012329   bits: 23/22
c ---[3977]---> Adder-cost: 1496   maxlim: 3014633   bits: 23/22
c ---[3975]---> Adder-cost: 1496   maxlim: 3012457   bits: 23/22
c ---[3973]---> Adder-cost: 1496   maxlim: 3012329   bits: 23/22
c ---[3971]---> Adder-cost: 1496   maxlim: 3014633   bits: 23/22
c ---[3969]---> Adder-cost: 1496   maxlim: 3014633   bits: 23/22
c ---[3967]---> Adder-cost: 1496   maxlim: 3014633   bits: 23/22
c ---[3965]---> Adder-cost: 1496   maxlim: 3001833   bits: 23/22
c ---[3963]---> Adder-cost: 1496   maxlim: 2946025   bits: 23/22
c ---[3961]---> Adder-cost: 1496   maxlim: 3011689   bits: 23/22
c ---[3959]---> Adder-cost: 1496   maxlim: 3014633   bits: 23/22
c ---[3957]---> Adder-cost: 1496   maxlim: 3009001   bits: 23/22
c ---[3955]---> Adder-cost: 1496   maxlim: 3009001   bits: 23/22
c ---[3953]---> Adder-cost: 1496   maxlim: 3014633   bits: 23/22
c ---[3951]---> Adder-cost: 1496   maxlim: 3011689   bits: 23/22
c ---[3949]---> Adder-cost: 1496   maxlim: 3012457   bits: 23/22
c ---[3947]---> Adder-cost: 1496   maxlim: 3009641   bits: 23/22
c ---[3945]---> Adder-cost: 1496   maxlim: 3011945   bits: 23/22
c ---[3943]---> Adder-cost: 1496   maxlim: 3014633   bits: 23/22
c ---[3941]---> Adder-cost: 1496   maxlim: 3012457   bits: 23/22
c ---[3939]---> Adder-cost: 1496   maxlim: 2943977   bits: 23/22
c ---[3937]---> Adder-cost: 1496   maxlim: 3011561   bits: 23/22
c ---[3935]---> Adder-cost: 1496   maxlim: 3004649   bits: 23/22
c ---[3933]---> Adder-cost: 1496   maxlim: 3012457   bits: 23/22
c ---[3931]---> Adder-cost: 1496   maxlim: 3011561   bits: 23/22
c ---[3929]---> Adder-cost: 1496   maxlim: 3012073   bits: 23/22
c ---[3927]---> Adder-cost: 1496   maxlim: 3012329   bits: 23/22
c ---[3925]---> Adder-cost: 1496   maxlim: 3014633   bits: 23/22
c ---[3923]---> Adder-cost: 1496   maxlim: 3011561   bits: 23/22
c ---[3921]---> Adder-cost: 1496   maxlim: 3011561   bits: 23/22
c ---[3919]---> Adder-cost: 1496   maxlim: 3014633   bits: 23/22
c ---[3917]---> Adder-cost: 1496   maxlim: 3012073   bits: 23/22
c ---[3915]---> Adder-cost: 1496   maxlim: 3014633   bits: 23/22
c ---[3913]---> Adder-cost: 1496   maxlim: 3011689   bits: 23/22
c ---[3911]---> Adder-cost: 1496   maxlim: 3012585   bits: 23/22
c ---[3909]---> Adder-cost: 1496   maxlim: 3014633   bits: 23/22
c ---[3907]---> Adder-cost: 1496   maxlim: 3014633   bits: 23/22
c ---[3905]---> Adder-cost: 1496   maxlim: 3014633   bits: 23/22
c ---[3903]---> Adder-cost: 1496   maxlim: 2946153   bits: 23/22
c ---[3901]---> Adder-cost: 1496   maxlim: 3014633   bits: 23/22
c ---[3899]---> Adder-cost: 1496   maxlim: 3014633   bits: 23/22
c ---[3897]---> Adder-cost: 1496   maxlim: 3014633   bits: 23/22
c ---[3895]---> Adder-cost: 1496   maxlim: 3014633   bits: 23/22
c ---[3893]---> Adder-cost: 1490   maxlim: 2910825   bits: 23/22
c ---[3891]---> Adder-cost: 1490   maxlim: 2941673   bits: 23/22
c ---[3889]---> Adder-cost: 1496   maxlim: 2916329   bits: 23/22
c ---[3887]---> Adder-cost: 1496   maxlim: 3011561   bits: 23/22
c ---[3885]---> Adder-cost: 1486   maxlim: 3006953   bits: 23/22
c ---[3883]---> Adder-cost: 1496   maxlim: 3014633   bits: 23/22
c ---[3881]---> Adder-cost: 1496   maxlim: 3014633   bits: 23/22
c ---[3879]---> Adder-cost: 1496   maxlim: 2913897   bits: 23/22
c ---[3877]---> Adder-cost: 1496   maxlim: 3014633   bits: 23/22
c ---[3875]---> Adder-cost: 1496   maxlim: 2913641   bits: 23/22
c ---[3873]---> Adder-cost: 1496   maxlim: 3014633   bits: 23/22
c ---[3871]---> Adder-cost: 1496   maxlim: 3012073   bits: 23/22
c ---[3869]---> Adder-cost: 1496   maxlim: 3014633   bits: 23/22
c ---[3867]---> Adder-cost: 1496   maxlim: 2943465   bits: 23/22
c ---[3865]---> Adder-cost: 1496   maxlim: 3012073   bits: 23/22
c ---[3863]---> Adder-cost: 1496   maxlim: 3014633   bits: 23/22
c ---[3861]---> Adder-cost: 1496   maxlim: 3012201   bits: 23/22
c ---[3859]---> Adder-cost: 1496   maxlim: 3011945   bits: 23/22
c ---[3857]---> Adder-cost: 1496   maxlim: 3014633   bits: 23/22
c ---[3855]---> Adder-cost: 1496   maxlim: 3009641   bits: 23/22
c ---[3853]---> Adder-cost: 1496   maxlim: 3012201   bits: 23/22
c ---[3851]---> Adder-cost: 1496   maxlim: 3014633   bits: 23/22
c ---[3849]---> Adder-cost: 1496   maxlim: 3014633   bits: 23/22
c ---[3847]---> Adder-cost: 1496   maxlim: 3014633   bits: 23/22
c ---[3845]---> Adder-cost: 1496   maxlim: 2944105   bits: 23/22
c ---[3843]---> Adder-cost: 1496   maxlim: 3011817   bits: 23/22
c ---[3841]---> Adder-cost: 1496   maxlim: 3014633   bits: 23/22
c ---[3839]---> Adder-cost: 1496   maxlim: 3006441   bits: 23/22
c ---[3837]---> Adder-cost: 1496   maxlim: 3011561   bits: 23/22
c ---[3835]---> Adder-cost: 1496   maxlim: 3011817   bits: 23/22
c ---[3833]---> Adder-cost: 1496   maxlim: 3014633   bits: 23/22
c ---[3831]---> Adder-cost: 1496   maxlim: 3009641   bits: 23/22
c ---[3829]---> Adder-cost: 1496   maxlim: 3014633   bits: 23/22
c ---[3827]---> Adder-cost: 1496   maxlim: 3009129   bits: 23/22
c ---[3825]---> Adder-cost: 1496   maxlim: 3009257   bits: 23/22
c ---[3823]---> Adder-cost: 1496   maxlim: 3012585   bits: 23/22
c ---[3821]---> Adder-cost: 1496   maxlim: 3014633   bits: 23/22
c ---[3819]---> Adder-cost: 1496   maxlim: 3006953   bits: 23/22
c ---[3817]---> Adder-cost: 1496   maxlim: 3009897   bits: 23/22
c ---[3815]---> Adder-cost: 1496   maxlim: 3012329   bits: 23/22
c ---[3813]---> Adder-cost: 1496   maxlim: 3014633   bits: 23/22
c ---[3811]---> Adder-cost: 1496   maxlim: 3014633   bits: 23/22
c ---[3809]---> Adder-cost: 1496   maxlim: 3014633   bits: 23/22
c ---[3807]---> Adder-cost: 1496   maxlim: 3012073   bits: 23/22
c ---[3805]---> Adder-cost: 1496   maxlim: 3014633   bits: 23/22
c ---[3803]---> Adder-cost: 1496   maxlim: 3009385   bits: 23/22
c ---[3801]---> Adder-cost: 1496   maxlim: 2943593   bits: 23/22
c ---[3799]---> Adder-cost: 1496   maxlim: 3012585   bits: 23/22
c ---[3797]---> Adder-cost: 1496   maxlim: 3009129   bits: 23/22
c ---[3795]---> Adder-cost: 1496   maxlim: 3011561   bits: 23/22
c ---[3793]---> Adder-cost: 1496   maxlim: 3014633   bits: 23/22
c ---[3791]---> Adder-cost: 1496   maxlim: 3012329   bits: 23/22
c ---[3789]---> Adder-cost: 1496   maxlim: 3012329   bits: 23/22
c ---[3787]---> Adder-cost: 1496   maxlim: 3014633   bits: 23/22
c ---[3785]---> Adder-cost: 1496   maxlim: 3009001   bits: 23/22
c ---[3783]---> Adder-cost: 1496   maxlim: 3012073   bits: 23/22
c ---[3781]---> Adder-cost: 1496   maxlim: 3014633   bits: 23/22
c ---[3779]---> Adder-cost: 1496   maxlim: 3011945   bits: 23/22
c ---[3777]---> Adder-cost: 1496   maxlim: 3009897   bits: 23/22
c ---[3775]---> Adder-cost: 1496   maxlim: 3014633   bits: 23/22
c ---[3773]---> Adder-cost: 1496   maxlim: 3014633   bits: 23/22
c ---[3771]---> Adder-cost: 1496   maxlim: 3011689   bits: 23/22
c ---[3769]---> Adder-cost: 1496   maxlim: 3009641   bits: 23/22
c ---[3767]---> Adder-cost: 1496   maxlim: 3014633   bits: 23/22
c ---[3765]---> Adder-cost: 1496   maxlim: 3011561   bits: 23/22
c ---[3763]---> Adder-cost: 1496   maxlim: 2943977   bits: 23/22
c ---[3761]---> Adder-cost: 1496   maxlim: 3014633   bits: 23/22
c ---[3759]---> Adder-cost: 1496   maxlim: 3009897   bits: 23/22
c ---[3757]---> Adder-cost: 1496   maxlim: 3014633   bits: 23/22
c ---[3755]---> Adder-cost: 1496   maxlim: 3009513   bits: 23/22
c ---[3753]---> Adder-cost: 1496   maxlim: 3012073   bits: 23/22
c ---[3751]---> Adder-cost: 1496   maxlim: 3009001   bits: 23/22
c ---[3749]---> Adder-cost: 1490   maxlim: 2878057   bits: 23/22
c ---[3747]---> Adder-cost: 1496   maxlim: 3014633   bits: 23/22
c ---[3745]---> Adder-cost: 1496   maxlim: 3014633   bits: 23/22
c ---[3743]---> Adder-cost: 1496   maxlim: 3014633   bits: 23/22
c ---[3741]---> Adder-cost: 1496   maxlim: 3014633   bits: 23/22
c ---[3739]---> Adder-cost: 1496   maxlim: 3012585   bits: 23/22
c ---[3737]---> Adder-cost: 1496   maxlim: 3014633   bits: 23/22
c ---[3735]---> Adder-cost: 1496   maxlim: 3007081   bits: 23/22
c ---[3733]---> Adder-cost: 1496   maxlim: 3014633   bits: 23/22
c ---[3731]---> Adder-cost: 1496   maxlim: 3014633   bits: 23/22
c ---[3729]---> Adder-cost: 1496   maxlim: 3014633   bits: 23/22
c ---[3727]---> Adder-cost: 1496   maxlim: 3009257   bits: 23/22
c ---[3725]---> Adder-cost: 1496   maxlim: 3014633   bits: 23/22
c ---[3723]---> Adder-cost: 1496   maxlim: 3014633   bits: 23/22
c ---[3721]---> Adder-cost: 1496   maxlim: 3011689   bits: 23/22
c ---[3719]---> Adder-cost: 1496   maxlim: 3011561   bits: 23/22
c ---[3717]---> Adder-cost: 1496   maxlim: 2944233   bits: 23/22
c ---[3715]---> Adder-cost: 1496   maxlim: 3012201   bits: 23/22
c ---[3713]---> Adder-cost: 1496   maxlim: 3010025   bits: 23/22
c ---[3711]---> Adder-cost: 1496   maxlim: 3014633   bits: 23/22
c ---[3709]---> Adder-cost: 1496   maxlim: 3012073   bits: 23/22
c ---[3707]---> Adder-cost: 1496   maxlim: 3006953   bits: 23/22
c ---[3705]---> Adder-cost: 1496   maxlim: 3007337   bits: 23/22
c ---[3703]---> Adder-cost: 1496   maxlim: 3014633   bits: 23/22
c ---[3701]---> Adder-cost: 1496   maxlim: 3011689   bits: 23/22
c ---[3699]---> Adder-cost: 1496   maxlim: 3009513   bits: 23/22
c ---[3697]---> Adder-cost: 1496   maxlim: 3014633   bits: 23/22
c ---[3695]---> Adder-cost: 1496   maxlim: 3014633   bits: 23/22
c ---[3693]---> Adder-cost: 1496   maxlim: 3012585   bits: 23/22
c ---[3691]---> Adder-cost: 1496   maxlim: 3009257   bits: 23/22
c ---[3689]---> Adder-cost: 1496   maxlim: 3014633   bits: 23/22
c ---[3687]---> Adder-cost: 1496   maxlim: 3011689   bits: 23/22
c ---[3685]---> Adder-cost: 1496   maxlim: 3014633   bits: 23/22
c ---[3683]---> Adder-cost: 1496   maxlim: 3014633   bits: 23/22
c ---[3681]---> Adder-cost: 1496   maxlim: 2943849   bits: 23/22
c ---[3679]---> Adder-cost: 1496   maxlim: 2944489   bits: 23/22
c ---[3677]---> Adder-cost: 1496   maxlim: 3009129   bits: 23/22
c ---[3675]---> Adder-cost: 1496   maxlim: 3011689   bits: 23/22
c ---[3673]---> Adder-cost: 1496   maxlim: 3009385   bits: 23/22
c ---[3671]---> Adder-cost: 1496   maxlim: 3012457   bits: 23/22
c ---[3669]---> Adder-cost: 1496   maxlim: 3014633   bits: 23/22
c ---[3667]---> Adder-cost: 1496   maxlim: 3009769   bits: 23/22
c ---[3665]---> Adder-cost: 1496   maxlim: 3014633   bits: 23/22
c ---[3663]---> Adder-cost: 1496   maxlim: 3014633   bits: 23/22
c ---[3661]---> Adder-cost: 1496   maxlim: 3011945   bits: 23/22
c ---[3659]---> Adder-cost: 1496   maxlim: 3011945   bits: 23/22
c ---[3657]---> Adder-cost: 1496   maxlim: 3012457   bits: 23/22
c ---[3655]---> Adder-cost: 1496   maxlim: 3012585   bits: 23/22
c ---[3653]---> Adder-cost: 1496   maxlim: 3012585   bits: 23/22
c ---[3651]---> Adder-cost: 1496   maxlim: 2944105   bits: 23/22
c ---[3649]---> Adder-cost: 1496   maxlim: 3011817   bits: 23/22
c ---[3647]---> Adder-cost: 1496   maxlim: 3014633   bits: 23/22
c ---[3645]---> Adder-cost: 1496   maxlim: 3011945   bits: 23/22
c ---[3643]---> Adder-cost: 1496   maxlim: 3011689   bits: 23/22
c ---[3641]---> Adder-cost: 1496   maxlim: 3012585   bits: 23/22
c ---[3639]---> Adder-cost: 1496   maxlim: 3011689   bits: 23/22
c ---[3637]---> Adder-cost: 1496   maxlim: 3012457   bits: 23/22
c ---[3635]---> Adder-cost: 1496   maxlim: 3014633   bits: 23/22
c ---[3633]---> Adder-cost: 1496   maxlim: 3011689   bits: 23/22
c ---[3631]---> Adder-cost: 1496   maxlim: 3011689   bits: 23/22
c ---[3629]---> Adder-cost: 1496   maxlim: 3012073   bits: 23/22
c ---[3627]---> Adder-cost: 1496   maxlim: 3014633   bits: 23/22
c ---[3625]---> Adder-cost: 1496   maxlim: 3012457   bits: 23/22
c ---[3623]---> Adder-cost: 1496   maxlim: 3007209   bits: 23/22
c ---[3621]---> Adder-cost: 1496   maxlim: 3012457   bits: 23/22
c ---[3619]---> Adder-cost: 1496   maxlim: 3014633   bits: 23/22
c ---[3617]---> Adder-cost: 1496   maxlim: 3012073   bits: 23/22
c ---[3615]---> Adder-cost: 1496   maxlim: 3014633   bits: 23/22
c ---[3613]---> Adder-cost: 1496   maxlim: 3012457   bits: 23/22
c ---[3611]---> Adder-cost: 1496   maxlim: 3011561   bits: 23/22
c ---[3609]---> Adder-cost: 1496   maxlim: 3014633   bits: 23/22
c ---[3607]---> Adder-cost: 1496   maxlim: 3014633   bits: 23/22
c ---[3605]---> Adder-cost: 1496   maxlim: 3012457   bits: 23/22
c ---[3603]---> Adder-cost: 1496   maxlim: 2943721   bits: 23/22
c ---[3601]---> Adder-cost: 1496   maxlim: 3007209   bits: 23/22
c ---[3599]---> Adder-cost: 1496   maxlim: 3012201   bits: 23/22
c ---[3597]---> Adder-cost: 1496   maxlim: 3011817   bits: 23/22
c ---[3595]---> Adder-cost: 1496   maxlim: 3014633   bits: 23/22
c ---[3593]---> Adder-cost: 1496   maxlim: 3011561   bits: 23/22
c ---[3591]---> Adder-cost: 1496   maxlim: 2943721   bits: 23/22
c ---[3589]---> Adder-cost: 1496   maxlim: 3014633   bits: 23/22
c ---[3587]---> Adder-cost: 1496   maxlim: 3012585   bits: 23/22
c ---[3585]---> Adder-cost: 1496   maxlim: 3014633   bits: 23/22
c ---[3583]---> Adder-cost: 1496   maxlim: 3009129   bits: 23/22
c ---[3581]---> Adder-cost: 1496   maxlim: 3014633   bits: 23/22
c ---[3579]---> Adder-cost: 1496   maxlim: 3011561   bits: 23/22
c ---[3577]---> Adder-cost: 1496   maxlim: 3010025   bits: 23/22
c ---[3575]---> Adder-cost: 1496   maxlim: 3014633   bits: 23/22
c ---[3573]---> Adder-cost: 1496   maxlim: 3012585   bits: 23/22
c ---[3571]---> Adder-cost: 1496   maxlim: 3011561   bits: 23/22
c ---[3569]---> Adder-cost: 1496   maxlim: 3009385   bits: 23/22
c ---[3567]---> Adder-cost: 1496   maxlim: 3009385   bits: 23/22
c ---[3565]---> Adder-cost: 1496   maxlim: 3014633   bits: 23/22
c ---[3563]---> Adder-cost: 1496   maxlim: 3011561   bits: 23/22
c ---[3561]---> Adder-cost: 1496   maxlim: 3014633   bits: 23/22
c ---[3559]---> Adder-cost: 1496   maxlim: 3014633   bits: 23/22
c ---[3557]---> Adder-cost: 1496   maxlim: 3014633   bits: 23/22
c ---[3555]---> Adder-cost: 1496   maxlim: 3014633   bits: 23/22
c ---[3553]---> Adder-cost: 1496   maxlim: 3007465   bits: 23/22
c ---[3551]---> Adder-cost: 1496   maxlim: 3009769   bits: 23/22
c ---[3549]---> Adder-cost: 1496   maxlim: 3006569   bits: 23/22
c ---[3547]---> Adder-cost: 1496   maxlim: 3012201   bits: 23/22
c ---[3545]---> Adder-cost: 1496   maxlim: 3009897   bits: 23/22
c ---[3543]---> Adder-cost: 1496   maxlim: 3011689   bits: 23/22
c ---[3541]---> Adder-cost: 1496   maxlim: 3011689   bits: 23/22
c ---[3539]---> Adder-cost: 1496   maxlim: 3014633   bits: 23/22
c ---[3537]---> Adder-cost: 1496   maxlim: 3009257   bits: 23/22
c ---[3535]---> Adder-cost: 1496   maxlim: 3012585   bits: 23/22
c ---[3533]---> Adder-cost: 1496   maxlim: 3011689   bits: 23/22
c ---[3531]---> Adder-cost: 1496   maxlim: 3004905   bits: 23/22
c ---[3529]---> Adder-cost: 1496   maxlim: 3011689   bits: 23/22
c ---[3527]---> Adder-cost: 1496   maxlim: 3014633   bits: 23/22
c ---[3525]---> Adder-cost: 1496   maxlim: 3014633   bits: 23/22
c ---[3523]---> Adder-cost: 1496   maxlim: 3011561   bits: 23/22
c ---[3521]---> Adder-cost: 1496   maxlim: 3012073   bits: 23/22
c ---[3519]---> Adder-cost: 1496   maxlim: 3009385   bits: 23/22
c ---[3517]---> Adder-cost: 1496   maxlim: 3012073   bits: 23/22
c ---[3515]---> Adder-cost: 1496   maxlim: 3011561   bits: 23/22
c ---[3513]---> Adder-cost: 1496   maxlim: 3009513   bits: 23/22
c ---[3511]---> Adder-cost: 1496   maxlim: 3011689   bits: 23/22
c ---[3509]---> Adder-cost: 1496   maxlim: 3014633   bits: 23/22
c ---[3507]---> Adder-cost: 1496   maxlim: 3014633   bits: 23/22
c ---[3505]---> Adder-cost: 1496   maxlim: 3009641   bits: 23/22
c ---[3503]---> Adder-cost: 1496   maxlim: 3012073   bits: 23/22
c ---[3501]---> Adder-cost: 1496   maxlim: 3014633   bits: 23/22
c ---[3499]---> Adder-cost: 1496   maxlim: 3009129   bits: 23/22
c ---[3497]---> Adder-cost: 1496   maxlim: 3012073   bits: 23/22
c ---[3495]---> Adder-cost: 1496   maxlim: 3012457   bits: 23/22
c ---[3493]---> Adder-cost: 1496   maxlim: 3012457   bits: 23/22
c ---[3491]---> Adder-cost: 1496   maxlim: 3014633   bits: 23/22
c ---[3489]---> Adder-cost: 1496   maxlim: 3012073   bits: 23/22
c ---[3487]---> Adder-cost: 1496   maxlim: 3012201   bits: 23/22
c ---[3485]---> Adder-cost: 1496   maxlim: 3014633   bits: 23/22
c ---[3483]---> Adder-cost: 1496   maxlim: 3004393   bits: 23/22
c ---[3481]---> Adder-cost: 1496   maxlim: 3014633   bits: 23/22
c ---[3479]---> Adder-cost: 1496   maxlim: 3014633   bits: 23/22
c ---[3477]---> Adder-cost: 1496   maxlim: 3014633   bits: 23/22
c ---[3475]---> Adder-cost: 1496   maxlim: 3009513   bits: 23/22
c ---[3473]---> Adder-cost: 1496   maxlim: 3014633   bits: 23/22
c ---[3471]---> Adder-cost: 1496   maxlim: 3009513   bits: 23/22
c ---[3469]---> Adder-cost: 1496   maxlim: 3012585   bits: 23/22
c ---[3467]---> Adder-cost: 1496   maxlim: 3012201   bits: 23/22
c ---[3465]---> Adder-cost: 1496   maxlim: 3014633   bits: 23/22
c ---[3463]---> Adder-cost: 1496   maxlim: 3014633   bits: 23/22
c ---[3461]---> Adder-cost: 1496   maxlim: 3014633   bits: 23/22
c ---[3459]---> Adder-cost: 1496   maxlim: 3012329   bits: 23/22
c ---[3457]---> Adder-cost: 1496   maxlim: 3012457   bits: 23/22
c ---[3455]---> Adder-cost: 1496   maxlim: 3014633   bits: 23/22
c ---[3453]---> Adder-cost: 1496   maxlim: 3012329   bits: 23/22
c ---[3451]---> Adder-cost: 1496   maxlim: 3012073   bits: 23/22
c ---[3449]---> Adder-cost: 1496   maxlim: 3009001   bits: 23/22
c ---[3447]---> Adder-cost: 1496   maxlim: 2943977   bits: 23/22
c ---[3445]---> Adder-cost: 1496   maxlim: 3011945   bits: 23/22
c ---[3443]---> Adder-cost: 1496   maxlim: 3012329   bits: 23/22
c ---[3441]---> Adder-cost: 1496   maxlim: 3014633   bits: 23/22
c ---[3439]---> Adder-cost: 1496   maxlim: 3012073   bits: 23/22
c ---[3437]---> Adder-cost: 1496   maxlim: 3014633   bits: 23/22
c ---[3435]---> Adder-cost: 1496   maxlim: 3014633   bits: 23/22
c ---[3433]---> Adder-cost: 1496   maxlim: 3012585   bits: 23/22
c ---[3431]---> Adder-cost: 1496   maxlim: 3011561   bits: 23/22
c ---[3429]---> Adder-cost: 1496   maxlim: 3014633   bits: 23/22
c ---[3427]---> Adder-cost: 1496   maxlim: 3014633   bits: 23/22
c ---[3425]---> Adder-cost: 1496   maxlim: 3012201   bits: 23/22
c ---[3423]---> Adder-cost: 1496   maxlim: 3012329   bits: 23/22
c ---[3421]---> Adder-cost: 1496   maxlim: 3014633   bits: 23/22
c ---[3419]---> Adder-cost: 1496   maxlim: 3012457   bits: 23/22
c ---[3417]---> Adder-cost: 1496   maxlim: 3011689   bits: 23/22
c ---[3415]---> Adder-cost: 1496   maxlim: 3014633   bits: 23/22
c ---[3413]---> Adder-cost: 1496   maxlim: 3011689   bits: 23/22
c ---[3411]---> Adder-cost: 1496   maxlim: 3009001   bits: 23/22
c ---[3409]---> Adder-cost: 1496   maxlim: 3009257   bits: 23/22
c ---[3407]---> Adder-cost: 1496   maxlim: 3009001   bits: 23/22
c ---[3405]---> Adder-cost: 1496   maxlim: 3014633   bits: 23/22
c ---[3403]---> Adder-cost: 1496   maxlim: 3014633   bits: 23/22
c ---[3401]---> Adder-cost: 1496   maxlim: 3014633   bits: 23/22
c ---[3399]---> Adder-cost: 1496   maxlim: 3006697   bits: 23/22
c ---[3397]---> Adder-cost: 1496   maxlim: 3014633   bits: 23/22
c ---[3395]---> Adder-cost: 1496   maxlim: 3012457   bits: 23/22
c ---[3393]---> Adder-cost: 1496   maxlim: 3009385   bits: 23/22
c ---[3391]---> Adder-cost: 1496   maxlim: 3014633   bits: 23/22
c ---[3389]---> Adder-cost: 1496   maxlim: 3014633   bits: 23/22
c ---[3387]---> Adder-cost: 1496   maxlim: 3014633   bits: 23/22
c ---[3385]---> Adder-cost: 1496   maxlim: 2941033   bits: 23/22
c ---[3383]---> Adder-cost: 1496   maxlim: 3014633   bits: 23/22
c ---[3381]---> Adder-cost: 1496   maxlim: 2944361   bits: 23/22
c ---[3379]---> Adder-cost: 1496   maxlim: 3011817   bits: 23/22
c ---[3377]---> Adder-cost: 1496   maxlim: 3014633   bits: 23/22
c ---[3375]---> Adder-cost: 1496   maxlim: 3012073   bits: 23/22
c ---[3373]---> Adder-cost: 1496   maxlim: 3014633   bits: 23/22
c ---[3371]---> Adder-cost: 1496   maxlim: 3014633   bits: 23/22
c ---[3369]---> Adder-cost: 1496   maxlim: 3012201   bits: 23/22
c ---[3367]---> Adder-cost: 1496   maxlim: 3007337   bits: 23/22
c ---[3365]---> Adder-cost: 1496   maxlim: 3012329   bits: 23/22
c ---[3363]---> Adder-cost: 1496   maxlim: 3009769   bits: 23/22
c ---[3362]---> BDD-cost:   24
c ---[3361]---> BDD-cost:   24
c ---[3360]---> BDD-cost:   24
c ---[3359]---> BDD-cost:   24
c ---[3358]---> BDD-cost:   24
c ---[3357]---> BDD-cost:   24
c ---[3356]---> BDD-cost:   24
c ---[3355]---> BDD-cost:   24
c ---[3354]---> BDD-cost:   24
c ---[3353]---> BDD-cost:   24
c ---[3352]---> BDD-cost:   24
c ---[3351]---> BDD-cost:   24
c ---[3350]---> BDD-cost:   24
c ---[3349]---> BDD-cost:   24
c ---[3348]---> BDD-cost:   24
c ---[3347]---> BDD-cost:   24
c ---[3346]---> BDD-cost:   24
c ---[3345]---> BDD-cost:   24
c ---[3344]---> BDD-cost:   24
c ---[3343]---> BDD-cost:   24
c ---[3342]---> BDD-cost:   24
c ---[3341]---> BDD-cost:   24
c ---[3340]---> BDD-cost:   24
c ---[3339]---> BDD-cost:   24
c ---[3338]---> BDD-cost:   24
c ---[3337]---> BDD-cost:   24
c ---[3336]---> BDD-cost:   24
c ---[3335]---> BDD-cost:   24
c ---[3334]---> BDD-cost:   24
c ---[3333]---> BDD-cost:   24
c ---[3332]---> BDD-cost:   24
c ---[3331]---> BDD-cost:   24
c ---[3330]---> BDD-cost:   24
c ---[3329]---> BDD-cost:   24
c ---[3328]---> BDD-cost:   24
c ---[3327]---> BDD-cost:   24
c ---[3326]---> BDD-cost:   24
c ---[3325]---> BDD-cost:   24
c ---[3324]---> BDD-cost:   24
c ---[3323]---> BDD-cost:   24
c ---[3322]---> BDD-cost:   24
c ---[3321]---> BDD-cost:   24
c ---[3320]---> BDD-cost:   24
c ---[3319]---> BDD-cost:   24
c ---[3318]---> BDD-cost:   24
c ---[3317]---> BDD-cost:   24
c ---[3316]---> BDD-cost:   24
c ---[3315]---> BDD-cost:   24
c ---[3314]---> BDD-cost:   24
c ---[3313]---> BDD-cost:   24
c ---[3312]---> BDD-cost:   24
c ---[3311]---> BDD-cost:   24
c ---[3310]---> BDD-cost:   24
c ---[3309]---> BDD-cost:   24
c ---[3308]---> BDD-cost:   24
c ---[3307]---> BDD-cost:   24
c ---[3306]---> BDD-cost:   24
c ---[3305]---> BDD-cost:   24
c ---[3304]---> BDD-cost:   24
c ---[3303]---> BDD-cost:   24
c ---[3302]---> BDD-cost:   24
c ---[3301]---> BDD-cost:   24
c ---[3300]---> BDD-cost:   24
c ---[3299]---> BDD-cost:   24
c ---[3298]---> BDD-cost:   24
c ---[3297]---> BDD-cost:   24
c ---[3296]---> BDD-cost:   24
c ---[3295]---> BDD-cost:   24
c ---[3294]---> BDD-cost:   24
c ---[3293]---> BDD-cost:   24
c ---[3292]---> BDD-cost:   24
c ---[3291]---> BDD-cost:   24
c ---[3290]---> BDD-cost:   24
c ---[3289]---> BDD-cost:   24
c ---[3288]---> BDD-cost:   24
c ---[3287]---> BDD-cost:   24
c ---[3286]---> BDD-cost:   24
c ---[3285]---> BDD-cost:   24
c ---[3284]---> BDD-cost:   24
c ---[3283]---> BDD-cost:   24
c ---[3282]---> BDD-cost:   24
c ---[3281]---> BDD-cost:   24
c ---[3280]---> BDD-cost:   24
c ---[3279]---> BDD-cost:   24
c ---[3278]---> BDD-cost:   24
c ---[3277]---> BDD-cost:   24
c ---[3276]---> BDD-cost:   24
c ---[3275]---> BDD-cost:   24
c ---[3274]---> BDD-cost:   24
c ---[3273]---> BDD-cost:   24
c ---[3272]---> BDD-cost:   24
c ---[3271]---> BDD-cost:   24
c ---[3270]---> BDD-cost:   24
c ---[3269]---> BDD-cost:   24
c ---[3268]---> BDD-cost:   24
c ---[3267]---> BDD-cost:   24
c ---[3266]---> BDD-cost:   24
c ---[3265]---> BDD-cost:   24
c ---[3264]---> BDD-cost:   24
c ---[3263]---> BDD-cost:   24
c ---[3262]---> BDD-cost:   24
c ---[3261]---> BDD-cost:   24
c ---[3260]---> BDD-cost:   24
c ---[3259]---> BDD-cost:   24
c ---[3258]---> BDD-cost:   24
c ---[3257]---> BDD-cost:   24
c ---[3256]---> BDD-cost:   24
c ---[3255]---> BDD-cost:   24
c ---[3254]---> BDD-cost:   24
c ---[3253]---> BDD-cost:   24
c ---[3252]---> BDD-cost:   24
c ---[3251]---> BDD-cost:   24
c ---[3250]---> BDD-cost:   24
c ---[3249]---> BDD-cost:   24
c ---[3248]---> BDD-cost:   24
c ---[3247]---> BDD-cost:   24
c ---[3246]---> BDD-cost:   24
c ---[3245]---> BDD-cost:   24
c ---[3244]---> BDD-cost:   24
c ---[3243]---> BDD-cost:   24
c ---[3242]---> BDD-cost:   24
c ---[3241]---> BDD-cost:   24
c ---[3240]---> BDD-cost:   24
c ---[3239]---> BDD-cost:   24
c ---[3238]---> BDD-cost:   24
c ---[3237]---> BDD-cost:   24
c ---[3236]---> BDD-cost:   24
c ---[3235]---> BDD-cost:   24
c ---[3234]---> BDD-cost:   24
c ---[3233]---> BDD-cost:   24
c ---[3232]---> BDD-cost:   24
c ---[3231]---> BDD-cost:   24
c ---[3230]---> BDD-cost:   24
c ---[3229]---> BDD-cost:   24
c ---[3228]---> BDD-cost:   24
c ---[3227]---> BDD-cost:   24
c ---[3226]---> BDD-cost:   24
c ---[3225]---> BDD-cost:   24
c ---[3224]---> BDD-cost:   24
c ---[3223]---> BDD-cost:   24
c ---[3222]---> BDD-cost:   24
c ---[3221]---> BDD-cost:   24
c ---[3220]---> BDD-cost:   24
c ---[3219]---> BDD-cost:   24
c ---[3218]---> BDD-cost:   24
c ---[3217]---> BDD-cost:   24
c ---[3216]---> BDD-cost:   24
c ---[3215]---> BDD-cost:   24
c ---[3214]---> BDD-cost:   24
c ---[3213]---> BDD-cost:   24
c ---[3212]---> BDD-cost:   24
c ---[3211]---> BDD-cost:   24
c ---[3210]---> BDD-cost:   24
c ---[3209]---> BDD-cost:   24
c ---[3208]---> BDD-cost:   24
c ---[3207]---> BDD-cost:   24
c ---[3206]---> BDD-cost:   24
c ---[3205]---> BDD-cost:   24
c ---[3204]---> BDD-cost:   24
c ---[3203]---> BDD-cost:   24
c ---[3202]---> BDD-cost:   24
c ---[3201]---> BDD-cost:   24
c ---[3200]---> BDD-cost:   24
c ---[3199]---> BDD-cost:   24
c ---[3198]---> BDD-cost:   24
c ---[3197]---> BDD-cost:   24
c ---[3196]---> BDD-cost:   24
c ---[3195]---> BDD-cost:   24
c ---[3194]---> BDD-cost:   24
c ---[3193]---> BDD-cost:   24
c ---[3192]---> BDD-cost:   24
c ---[3191]---> BDD-cost:   24
c ---[3190]---> BDD-cost:   24
c ---[3189]---> BDD-cost:   24
c ---[3188]---> BDD-cost:   24
c ---[3187]---> BDD-cost:   24
c ---[3186]---> BDD-cost:   24
c ---[3185]---> BDD-cost:   24
c ---[3184]---> BDD-cost:   24
c ---[3183]---> BDD-cost:   24
c ---[3182]---> BDD-cost:   24
c ---[3181]---> BDD-cost:   24
c ---[3180]---> BDD-cost:   24
c ---[3179]---> BDD-cost:   24
c ---[3178]---> BDD-cost:   24
c ---[3177]---> BDD-cost:   24
c ---[3176]---> BDD-cost:   24
c ---[3175]---> BDD-cost:   24
c ---[3174]---> BDD-cost:   24
c ---[3173]---> BDD-cost:   24
c ---[3172]---> BDD-cost:   24
c ---[3171]---> BDD-cost:   24
c ---[3170]---> BDD-cost:   24
c ---[3169]---> BDD-cost:   24
c ---[3168]---> BDD-cost:   24
c ---[3167]---> BDD-cost:   24
c ---[3166]---> BDD-cost:   24
c ---[3165]---> BDD-cost:   24
c ---[3164]---> BDD-cost:   24
c ---[3163]---> BDD-cost:   24
c ---[3162]---> BDD-cost:   24
c ---[3161]---> BDD-cost:   24
c ---[3160]---> BDD-cost:   24
c ---[3159]---> BDD-cost:   24
c ---[3158]---> BDD-cost:   24
c ---[3157]---> BDD-cost:   24
c ---[3156]---> BDD-cost:   24
c ---[3155]---> BDD-cost:   24
c ---[3154]---> BDD-cost:   24
c ---[3153]---> BDD-cost:   24
c ---[3152]---> BDD-cost:   24
c ---[3151]---> BDD-cost:   24
c ---[3150]---> BDD-cost:   24
c ---[3149]---> BDD-cost:   24
c ---[3148]---> BDD-cost:   24
c ---[3147]---> BDD-cost:   24
c ---[3146]---> BDD-cost:   24
c ---[3145]---> BDD-cost:   24
c ---[3144]---> BDD-cost:   24
c ---[3143]---> BDD-cost:   24
c ---[3142]---> BDD-cost:   24
c ---[3141]---> BDD-cost:   24
c ---[3140]---> BDD-cost:   24
c ---[3139]---> BDD-cost:   24
c ---[3138]---> BDD-cost:   24
c ---[3137]---> BDD-cost:   24
c ---[3136]---> BDD-cost:   24
c ---[3135]---> BDD-cost:   24
c ---[3134]---> BDD-cost:   24
c ---[3133]---> BDD-cost:   24
c ---[3132]---> BDD-cost:   24
c ---[3131]---> BDD-cost:   24
c ---[3130]---> BDD-cost:   24
c ---[3129]---> BDD-cost:   24
c ---[3128]---> BDD-cost:   24
c ---[3127]---> BDD-cost:   24
c ---[3126]---> BDD-cost:   24
c ---[3125]---> BDD-cost:   24
c ---[3124]---> BDD-cost:   24
c ---[3123]---> BDD-cost:   24
c ---[3122]---> BDD-cost:   24
c ---[3121]---> BDD-cost:   24
c ---[3120]---> BDD-cost:   24
c ---[3119]---> BDD-cost:   24
c ---[3118]---> BDD-cost:   24
c ---[3117]---> BDD-cost:   24
c ---[3116]---> BDD-cost:   24
c ---[3115]---> BDD-cost:   24
c ---[3114]---> BDD-cost:   24
c ---[3113]---> BDD-cost:   24
c ---[3112]---> BDD-cost:   24
c ---[3111]---> BDD-cost:   24
c ---[3110]---> BDD-cost:   24
c ---[3109]---> BDD-cost:   24
c ---[3108]---> BDD-cost:   24
c ---[3107]---> BDD-cost:   24
c ---[3106]---> BDD-cost:   24
c ---[3105]---> BDD-cost:   24
c ---[3104]---> BDD-cost:   24
c ---[3103]---> BDD-cost:   24
c ---[3102]---> BDD-cost:   24
c ---[3101]---> BDD-cost:   24
c ---[3100]---> BDD-cost:   24
c ---[3099]---> BDD-cost:   24
c ---[3098]---> BDD-cost:   24
c ---[3097]---> BDD-cost:   24
c ---[3096]---> BDD-cost:   24
c ---[3095]---> BDD-cost:   24
c ---[3094]---> BDD-cost:   24
c ---[3093]---> BDD-cost:   24
c ---[3092]---> BDD-cost:   24
c ---[3091]---> BDD-cost:   24
c ---[3090]---> BDD-cost:   24
c ---[3089]---> BDD-cost:   24
c ---[3088]---> BDD-cost:   24
c ---[3087]---> BDD-cost:   24
c ---[3086]---> BDD-cost:   24
c ---[3085]---> BDD-cost:   24
c ---[3084]---> BDD-cost:   24
c ---[3083]---> BDD-cost:   24
c ---[3082]---> BDD-cost:   24
c ---[3081]---> BDD-cost:   24
c ---[3080]---> BDD-cost:   24
c ---[3079]---> BDD-cost:   24
c ---[3078]---> BDD-cost:   24
c ---[3077]---> BDD-cost:   24
c ---[3076]---> BDD-cost:   24
c ---[3075]---> BDD-cost:   24
c ---[3074]---> BDD-cost:   24
c ---[3073]---> BDD-cost:   24
c ---[3072]---> BDD-cost:   24
c ---[3071]---> BDD-cost:   24
c ---[3070]---> BDD-cost:   24
c ---[3069]---> BDD-cost:   24
c ---[3068]---> BDD-cost:   24
c ---[3067]---> BDD-cost:   24
c ---[3066]---> BDD-cost:   24
c ---[3065]---> BDD-cost:   24
c ---[3064]---> BDD-cost:   24
c ---[3063]---> BDD-cost:   24
c ---[3062]---> BDD-cost:   24
c ---[3061]---> BDD-cost:   24
c ---[3060]---> BDD-cost:   24
c ---[3059]---> BDD-cost:   24
c ---[3058]---> BDD-cost:   24
c ---[3057]---> BDD-cost:   24
c ---[3056]---> BDD-cost:   24
c ---[3055]---> BDD-cost:   24
c ---[3054]---> BDD-cost:   24
c ---[3053]---> BDD-cost:   24
c ---[3052]---> BDD-cost:   24
c ---[3051]---> BDD-cost:   24
c ---[3050]---> BDD-cost:   24
c ---[3049]---> BDD-cost:   24
c ---[3048]---> BDD-cost:   24
c ---[3047]---> BDD-cost:   24
c ---[3046]---> BDD-cost:   24
c ---[3045]---> BDD-cost:   24
c ---[3044]---> BDD-cost:   24
c ---[3043]---> BDD-cost:   24
c ---[3042]---> BDD-cost:   24
c ---[3041]---> BDD-cost:   24
c ---[3040]---> BDD-cost:   24
c ---[3039]---> BDD-cost:   24
c ---[3038]---> BDD-cost:   24
c ---[3037]---> BDD-cost:   24
c ---[3036]---> BDD-cost:   24
c ---[3035]---> BDD-cost:   24
c ---[3034]---> BDD-cost:   24
c ---[3033]---> BDD-cost:   24
c ---[3032]---> BDD-cost:   24
c ---[3031]---> BDD-cost:   24
c ---[3030]---> BDD-cost:   24
c ---[3029]---> BDD-cost:   24
c ---[3028]---> BDD-cost:   24
c ---[3027]---> BDD-cost:   24
c ---[3026]---> BDD-cost:   24
c ---[3025]---> BDD-cost:   24
c ---[3024]---> BDD-cost:   24
c ---[3023]---> BDD-cost:   24
c ---[3022]---> BDD-cost:   24
c ---[3021]---> BDD-cost:   24
c ---[3020]---> BDD-cost:   24
c ---[3019]---> BDD-cost:   24
c ---[3018]---> BDD-cost:   24
c ---[3017]---> BDD-cost:   24
c ---[3016]---> BDD-cost:   24
c ---[3015]---> BDD-cost:   24
c ---[3014]---> BDD-cost:   24
c ---[3013]---> BDD-cost:   24
c ---[3012]---> BDD-cost:   24
c ---[3011]---> BDD-cost:   24
c ---[3010]---> BDD-cost:   24
c ---[3009]---> BDD-cost:   24
c ---[3008]---> BDD-cost:   24
c ---[3007]---> BDD-cost:   24
c ---[3006]---> BDD-cost:   24
c ---[3005]---> BDD-cost:   24
c ---[3004]---> BDD-cost:   24
c ---[3003]---> BDD-cost:   24
c ---[3002]---> BDD-cost:   24
c ---[3001]---> BDD-cost:   24
c ---[3000]---> BDD-cost:   24
c ---[2999]---> BDD-cost:   24
c ---[2998]---> BDD-cost:   24
c ---[2997]---> BDD-cost:   24
c ---[2996]---> BDD-cost:   24
c ---[2995]---> BDD-cost:   24
c ---[2994]---> BDD-cost:   24
c ---[2993]---> BDD-cost:   24
c ---[2992]---> BDD-cost:   24
c ---[2991]---> BDD-cost:   24
c ---[2990]---> BDD-cost:   24
c ---[2989]---> BDD-cost:   24
c ---[2988]---> BDD-cost:   24
c ---[2987]---> BDD-cost:   24
c ---[2986]---> BDD-cost:   24
c ---[2985]---> BDD-cost:   24
c ---[2984]---> BDD-cost:   24
c ---[2983]---> BDD-cost:   24
c ---[2982]---> BDD-cost:   24
c ---[2981]---> BDD-cost:   24
c ---[2980]---> BDD-cost:   24
c ---[2979]---> BDD-cost:   24
c ---[2978]---> BDD-cost:   24
c ---[2977]---> BDD-cost:   24
c ---[2976]---> BDD-cost:   24
c ---[2975]---> BDD-cost:   24
c ---[2974]---> BDD-cost:   24
c ---[2973]---> BDD-cost:   24
c ---[2972]---> BDD-cost:   24
c ---[2971]---> BDD-cost:   24
c ---[2970]---> BDD-cost:   24
c ---[2969]---> BDD-cost:   24
c ---[2968]---> BDD-cost:   24
c ---[2967]---> BDD-cost:   24
c ---[2966]---> BDD-cost:   24
c ---[2965]---> BDD-cost:   24
c ---[2964]---> BDD-cost:   24
c ---[2963]---> BDD-cost:   24
c ---[2962]---> BDD-cost:   24
c ---[2961]---> BDD-cost:   24
c ---[2960]---> BDD-cost:   24
c ---[2959]---> BDD-cost:   24
c ---[2958]---> BDD-cost:   24
c ---[2957]---> BDD-cost:   24
c ---[2956]---> BDD-cost:   24
c ---[2955]---> BDD-cost:   24
c ---[2954]---> BDD-cost:   24
c ---[2953]---> BDD-cost:   24
c ---[2952]---> BDD-cost:   24
c ---[2951]---> BDD-cost:   24
c ---[2950]---> BDD-cost:   24
c ---[2949]---> BDD-cost:   24
c ---[2948]---> BDD-cost:   24
c ---[2947]---> BDD-cost:   24
c ---[2946]---> BDD-cost:   24
c ---[2945]---> BDD-cost:   24
c ---[2944]---> BDD-cost:   24
c ---[2943]---> BDD-cost:   24
c ---[2942]---> BDD-cost:   24
c ---[2941]---> BDD-cost:   24
c ---[2940]---> BDD-cost:   24
c ---[2939]---> BDD-cost:   24
c ---[2938]---> BDD-cost:   24
c ---[2937]---> BDD-cost:   24
c ---[2936]---> BDD-cost:   24
c ---[2935]---> BDD-cost:   24
c ---[2934]---> BDD-cost:   24
c ---[2933]---> BDD-cost:   24
c ---[2932]---> BDD-cost:   24
c ---[2931]---> BDD-cost:   24
c ---[2930]---> BDD-cost:   24
c ---[2929]---> BDD-cost:   24
c ---[2928]---> BDD-cost:   24
c ---[2927]---> BDD-cost:   24
c ---[2926]---> BDD-cost:   24
c ---[2925]---> BDD-cost:   24
c ---[2924]---> BDD-cost:   24
c ---[2923]---> BDD-cost:   24
c ---[2922]---> BDD-cost:   24
c ---[2921]---> BDD-cost:   24
c ---[2920]---> BDD-cost:   24
c ---[2919]---> BDD-cost:   24
c ---[2918]---> BDD-cost:   24
c ---[2917]---> BDD-cost:   24
c ---[2916]---> BDD-cost:   24
c ---[2915]---> BDD-cost:   24
c ---[2914]---> BDD-cost:   24
c ---[2913]---> BDD-cost:   24
c ---[2912]---> BDD-cost:   24
c ---[2911]---> BDD-cost:   24
c ---[2910]---> BDD-cost:   24
c ---[2909]---> BDD-cost:   24
c ---[2908]---> BDD-cost:   24
c ---[2907]---> BDD-cost:   24
c ---[2906]---> BDD-cost:   24
c ---[2905]---> BDD-cost:   24
c ---[2904]---> BDD-cost:   24
c ---[2903]---> BDD-cost:   24
c ---[2902]---> BDD-cost:   24
c ---[2901]---> BDD-cost:   24
c ---[2900]---> BDD-cost:   24
c ---[2899]---> BDD-cost:   24
c ---[2898]---> BDD-cost:   24
c ---[2897]---> BDD-cost:   24
c ---[2896]---> BDD-cost:   24
c ---[2895]---> BDD-cost:   24
c ---[2894]---> BDD-cost:   24
c ---[2893]---> BDD-cost:   24
c ---[2892]---> BDD-cost:   24
c ---[2891]---> BDD-cost:   24
c ---[2890]---> BDD-cost:   24
c ---[2889]---> BDD-cost:   24
c ---[2888]---> BDD-cost:   24
c ---[2887]---> BDD-cost:   24
c ---[2886]---> BDD-cost:   24
c ---[2885]---> BDD-cost:   24
c ---[2884]---> BDD-cost:   24
c ---[2883]---> BDD-cost:   24
c ---[2882]---> BDD-cost:   24
c ---[2881]---> BDD-cost:   24
c ---[2880]---> BDD-cost:   24
c ---[2879]---> BDD-cost:   24
c ---[2878]---> BDD-cost:   24
c ---[2877]---> BDD-cost:   24
c ---[2876]---> BDD-cost:   24
c ---[2875]---> BDD-cost:   24
c ---[2874]---> BDD-cost:   24
c ---[2873]---> BDD-cost:   24
c ---[2872]---> BDD-cost:   24
c ---[2871]---> BDD-cost:   24
c ---[2870]---> BDD-cost:   24
c ---[2869]---> BDD-cost:   24
c ---[2868]---> BDD-cost:   24
c ---[2867]---> BDD-cost:   24
c ---[2866]---> BDD-cost:   24
c ---[2865]---> BDD-cost:   24
c ---[2864]---> BDD-cost:   24
c ---[2863]---> BDD-cost:   24
c ---[2862]---> BDD-cost:   24
c ---[2861]---> BDD-cost:   24
c ---[2860]---> BDD-cost:   24
c ---[2859]---> BDD-cost:   24
c ---[2858]---> BDD-cost:   24
c ---[2857]---> BDD-cost:   24
c ---[2856]---> BDD-cost:   24
c ---[2855]---> BDD-cost:   24
c ---[2854]---> BDD-cost:   24
c ---[2853]---> BDD-cost:   24
c ---[2852]---> BDD-cost:   24
c ---[2851]---> BDD-cost:   24
c ---[2850]---> BDD-cost:   24
c ---[2849]---> BDD-cost:   24
c ---[2848]---> BDD-cost:   24
c ---[2847]---> BDD-cost:   24
c ---[2846]---> BDD-cost:   24
c ---[2845]---> BDD-cost:   24
c ---[2844]---> BDD-cost:   24
c ---[2843]---> BDD-cost:   24
c ---[2842]---> BDD-cost:   24
c ---[2841]---> BDD-cost:   24
c ---[2840]---> BDD-cost:   24
c ---[2839]---> BDD-cost:   24
c ---[2838]---> BDD-cost:   24
c ---[2837]---> BDD-cost:   24
c ---[2836]---> BDD-cost:   24
c ---[2835]---> BDD-cost:   24
c ---[2834]---> BDD-cost:   24
c ---[2833]---> BDD-cost:   24
c ---[2832]---> BDD-cost:   24
c ---[2831]---> BDD-cost:   24
c ---[2830]---> BDD-cost:   24
c ---[2829]---> BDD-cost:   24
c ---[2828]---> BDD-cost:   24
c ---[2827]---> BDD-cost:   24
c ---[2826]---> BDD-cost:   24
c ---[2825]---> BDD-cost:   24
c ---[2824]---> BDD-cost:   24
c ---[2823]---> BDD-cost:   24
c ---[2822]---> BDD-cost:   24
c ---[2821]---> BDD-cost:   24
c ---[2820]---> BDD-cost:   24
c ---[2819]---> BDD-cost:   24
c ---[2818]---> BDD-cost:   24
c ---[2817]---> BDD-cost:   24
c ---[2816]---> BDD-cost:   24
c ---[2815]---> BDD-cost:   24
c ---[2814]---> BDD-cost:   24
c ---[2813]---> BDD-cost:   24
c ---[2812]---> BDD-cost:   24
c ---[2811]---> BDD-cost:   24
c ---[2810]---> BDD-cost:  131
c ---[2809]---> BDD-cost:  131
c ---[2808]---> BDD-cost:  131
c ---[2807]---> BDD-cost:  131
c ---[2806]---> BDD-cost:  131
c ---[2805]---> BDD-cost:  131
c ---[2804]---> BDD-cost:  131
c ---[2803]---> BDD-cost:  131
c ---[2802]---> BDD-cost:  131
c ---[2801]---> BDD-cost:  131
c ---[2800]---> BDD-cost:  131
c ---[2799]---> BDD-cost:  131
c ---[2798]---> BDD-cost:  131
c ---[2797]---> BDD-cost:  131
c ---[2796]---> BDD-cost:  131
c ---[2795]---> BDD-cost:  131
c ---[2794]---> BDD-cost:  131
c ---[2793]---> BDD-cost:  131
c ---[2792]---> BDD-cost:  131
c ---[2791]---> BDD-cost:  131
c ---[2790]---> BDD-cost:  131
c ---[2789]---> BDD-cost:  131
c ---[2788]---> BDD-cost:  131
c ---[2787]---> BDD-cost:  131
c ---[2786]---> BDD-cost:  131
c ---[2785]---> BDD-cost:  131
c ---[2784]---> BDD-cost:  131
c ---[2783]---> BDD-cost:  131
c ---[2782]---> BDD-cost:  131
c ---[2781]---> BDD-cost:  131
c ---[2780]---> BDD-cost:  131
c ---[2779]---> BDD-cost:  131
c ---[2778]---> BDD-cost:  131
c ---[2777]---> BDD-cost:  131
c ---[2776]---> BDD-cost:  131
c ---[2775]---> BDD-cost:  131
c ---[2774]---> BDD-cost:  131
c ---[2773]---> BDD-cost:  131
c ---[2772]---> BDD-cost:  131
c ---[2771]---> BDD-cost:  131
c ---[2770]---> BDD-cost:  131
c ---[2769]---> BDD-cost:  131
c ---[2768]---> BDD-cost:  131
c ---[2767]---> BDD-cost:  131
c ---[2766]---> BDD-cost:  131
c ---[2765]---> BDD-cost:  131
c ---[2764]---> BDD-cost:  131
c ---[2763]---> BDD-cost:  131
c ---[2762]---> BDD-cost:  131
c ---[2761]---> BDD-cost:  131
c ---[2760]---> BDD-cost:  131
c ---[2759]---> BDD-cost:  131
c ---[2758]---> BDD-cost:  131
c ---[2757]---> BDD-cost:  131
c ---[2756]---> BDD-cost:  131
c ---[2755]---> BDD-cost:  131
c ---[2754]---> BDD-cost:  131
c ---[2753]---> BDD-cost:  131
c ---[2752]---> BDD-cost:  131
c ---[2751]---> BDD-cost:  131
c ---[2750]---> BDD-cost:  131
c ---[2749]---> BDD-cost:  131
c ---[2748]---> BDD-cost:  131
c ---[2747]---> BDD-cost:  131
c ---[2746]---> BDD-cost:  131
c ---[2745]---> BDD-cost:  131
c ---[2744]---> BDD-cost:  131
c ---[2743]---> BDD-cost:  131
c ---[2742]---> BDD-cost:  131
c ---[2741]---> BDD-cost:  131
c ---[2740]---> BDD-cost:  131
c ---[2739]---> BDD-cost:  131
c ---[2738]---> BDD-cost:  131
c ---[2737]---> BDD-cost:  131
c ---[2736]---> BDD-cost:  131
c ---[2735]---> BDD-cost:  131
c ---[2734]---> BDD-cost:  131
c ---[2733]---> BDD-cost:  131
c ---[2732]---> BDD-cost:  131
c ---[2731]---> BDD-cost:  131
c ---[2730]---> BDD-cost:  131
c ---[2729]---> BDD-cost:  131
c ---[2728]---> BDD-cost:  131
c ---[2727]---> BDD-cost:  131
c ---[2726]---> BDD-cost:  131
c ---[2725]---> BDD-cost:  131
c ---[2724]---> BDD-cost:  131
c ---[2723]---> BDD-cost:  131
c ---[2722]---> BDD-cost:  131
c ---[2721]---> BDD-cost:  131
c ---[2720]---> BDD-cost:  131
c ---[2719]---> BDD-cost:  131
c ---[2718]---> BDD-cost:  131
c ---[2717]---> BDD-cost:  131
c ---[2716]---> BDD-cost:  131
c ---[2715]---> BDD-cost:  131
c ---[2714]---> BDD-cost:  131
c ---[2713]---> BDD-cost:  131
c ---[2712]---> BDD-cost:  131
c ---[2711]---> BDD-cost:  131
c ---[2710]---> BDD-cost:  131
c ---[2709]---> BDD-cost:  131
c ---[2708]---> BDD-cost:  131
c ---[2707]---> BDD-cost:  131
c ---[2706]---> BDD-cost:  131
c ---[2705]---> BDD-cost:  131
c ---[2704]---> BDD-cost:  131
c ---[2703]---> BDD-cost:  131
c ---[2702]---> BDD-cost:  131
c ---[2701]---> BDD-cost:  131
c ---[2700]---> BDD-cost:  131
c ---[2699]---> BDD-cost:  131
c ---[2698]---> BDD-cost:  131
c ---[2697]---> BDD-cost:  131
c ---[2696]---> BDD-cost:  131
c ---[2695]---> BDD-cost:  131
c ---[2694]---> BDD-cost:  131
c ---[2693]---> BDD-cost:  131
c ---[2692]---> BDD-cost:  131
c ---[2691]---> BDD-cost:  131
c ---[2690]---> BDD-cost:  131
c ---[2689]---> BDD-cost:  131
c ---[2688]---> BDD-cost:  131
c ---[2687]---> BDD-cost:  131
c ---[2686]---> BDD-cost:  131
c ---[2685]---> BDD-cost:  131
c ---[2684]---> BDD-cost:  131
c ---[2683]---> BDD-cost:  131
c ---[2682]---> BDD-cost:  131
c ---[2681]---> BDD-cost:  131
c ---[2680]---> BDD-cost:  131
c ---[2679]---> BDD-cost:  131
c ---[2678]---> BDD-cost:  131
c ---[2677]---> BDD-cost:  131
c ---[2676]---> BDD-cost:  131
c ---[2675]---> BDD-cost:  131
c ---[2674]---> BDD-cost:  131
c ---[2673]---> BDD-cost:  131
c ---[2672]---> BDD-cost:  131
c ---[2671]---> BDD-cost:  131
c ---[2670]---> BDD-cost:  131
c ---[2669]---> BDD-cost:  131
c ---[2668]---> BDD-cost:  131
c ---[2667]---> BDD-cost:  131
c ---[2666]---> BDD-cost:  131
c ---[2665]---> BDD-cost:  131
c ---[2664]---> BDD-cost:  131
c ---[2663]---> BDD-cost:  131
c ---[2662]---> BDD-cost:  131
c ---[2661]---> BDD-cost:  131
c ---[2660]---> BDD-cost:  131
c ---[2659]---> BDD-cost:  131
c ---[2658]---> BDD-cost:  131
c ---[2657]---> BDD-cost:  131
c ---[2656]---> BDD-cost:  131
c ---[2655]---> BDD-cost:  131
c ---[2654]---> BDD-cost:  131
c ---[2653]---> BDD-cost:  131
c ---[2652]---> BDD-cost:  131
c ---[2651]---> BDD-cost:  131
c ---[2650]---> BDD-cost:  131
c ---[2649]---> BDD-cost:  131
c ---[2648]---> BDD-cost:  131
c ---[2647]---> BDD-cost:  131
c ---[2646]---> BDD-cost:  131
c ---[2645]---> BDD-cost:  131
c ---[2644]---> BDD-cost:  131
c ---[2643]---> BDD-cost:  131
c ---[2642]---> BDD-cost:  131
c ---[2641]---> BDD-cost:  131
c ---[2640]---> BDD-cost:  131
c ---[2639]---> BDD-cost:  131
c ---[2638]---> BDD-cost:  131
c ---[2637]---> BDD-cost:  131
c ---[2636]---> BDD-cost:  131
c ---[2635]---> BDD-cost:  131
c ---[2634]---> BDD-cost:  131
c ---[2633]---> BDD-cost:  131
c ---[2632]---> BDD-cost:  131
c ---[2631]---> BDD-cost:  131
c ---[2630]---> BDD-cost:  131
c ---[2629]---> BDD-cost:  131
c ---[2628]---> BDD-cost:  131
c ---[2627]---> BDD-cost:  131
c ---[2626]---> BDD-cost:  131
c ---[2625]---> BDD-cost:  131
c ---[2624]---> BDD-cost:  131
c ---[2623]---> BDD-cost:  131
c ---[2622]---> BDD-cost:  131
c ---[2621]---> BDD-cost:  131
c ---[2620]---> BDD-cost:  131
c ---[2619]---> BDD-cost:  131
c ---[2618]---> BDD-cost:  131
c ---[2617]---> BDD-cost:  131
c ---[2616]---> BDD-cost:  131
c ---[2615]---> BDD-cost:  131
c ---[2614]---> BDD-cost:  131
c ---[2613]---> BDD-cost:  131
c ---[2612]---> BDD-cost:  131
c ---[2611]---> BDD-cost:  131
c ---[2610]---> BDD-cost:  131
c ---[2609]---> BDD-cost:  131
c ---[2608]---> BDD-cost:  131
c ---[2607]---> BDD-cost:  131
c ---[2606]---> BDD-cost:  131
c ---[2605]---> BDD-cost:  131
c ---[2604]---> BDD-cost:  131
c ---[2603]---> BDD-cost:  131
c ---[2602]---> BDD-cost:  131
c ---[2601]---> BDD-cost:  131
c ---[2600]---> BDD-cost:  131
c ---[2599]---> BDD-cost:  131
c ---[2598]---> BDD-cost:  131
c ---[2597]---> BDD-cost:  131
c ---[2596]---> BDD-cost:  131
c ---[2595]---> BDD-cost:  131
c ---[2594]---> BDD-cost:  131
c ---[2593]---> BDD-cost:  131
c ---[2592]---> BDD-cost:  131
c ---[2591]---> BDD-cost:  131
c ---[2590]---> BDD-cost:  131
c ---[2589]---> BDD-cost:  131
c ---[2588]---> BDD-cost:  131
c ---[2587]---> BDD-cost:  131
c ---[2586]---> BDD-cost:  131
c ---[2585]---> BDD-cost:  131
c ---[2584]---> BDD-cost:  131
c ---[2583]---> BDD-cost:  131
c ---[2582]---> BDD-cost:  131
c ---[2581]---> BDD-cost:  131
c ---[2580]---> BDD-cost:  131
c ---[2579]---> BDD-cost:  131
c ---[2578]---> BDD-cost:  131
c ---[2577]---> BDD-cost:  131
c ---[2576]---> BDD-cost:  131
c ---[2575]---> BDD-cost:  131
c ---[2574]---> BDD-cost:  131
c ---[2573]---> BDD-cost:  131
c ---[2572]---> BDD-cost:  131
c ---[2571]---> BDD-cost:  131
c ---[2570]---> BDD-cost:  131
c ---[2569]---> BDD-cost:  131
c ---[2568]---> BDD-cost:  131
c ---[2567]---> BDD-cost:  131
c ---[2566]---> BDD-cost:  131
c ---[2565]---> BDD-cost:  131
c ---[2564]---> BDD-cost:  131
c ---[2563]---> BDD-cost:  131
c ---[2562]---> BDD-cost:  131
c ---[2561]---> BDD-cost:  131
c ---[2560]---> BDD-cost:  131
c ---[2559]---> BDD-cost:  131
c ---[2558]---> BDD-cost:  131
c ---[2557]---> BDD-cost:  131
c ---[2556]---> BDD-cost:  131
c ---[2555]---> BDD-cost:  131
c ---[2554]---> BDD-cost:  131
c ---[2553]---> BDD-cost:  131
c ---[2552]---> BDD-cost:  131
c ---[2551]---> BDD-cost:  131
c ---[2550]---> BDD-cost:  131
c ---[2549]---> BDD-cost:  131
c ---[2548]---> BDD-cost:  131
c ---[2547]---> BDD-cost:  131
c ---[2546]---> BDD-cost:  131
c ---[2545]---> BDD-cost:  131
c ---[2544]---> BDD-cost:  131
c ---[2543]---> BDD-cost:  131
c ---[2542]---> BDD-cost:  131
c ---[2541]---> BDD-cost:  131
c ---[2540]---> BDD-cost:  131
c ---[2539]---> BDD-cost:  131
c ---[2538]---> BDD-cost:  131
c ---[2537]---> BDD-cost:  131
c ---[2536]---> BDD-cost:  131
c ---[2535]---> BDD-cost:  131
c ---[2534]---> BDD-cost:  131
c ---[2533]---> BDD-cost:  131
c ---[2532]---> BDD-cost:  131
c ---[2531]---> BDD-cost:  131
c ---[2530]---> BDD-cost:  131
c ---[2529]---> BDD-cost:  131
c ---[2528]---> BDD-cost:  131
c ---[2527]---> BDD-cost:  131
c ---[2526]---> BDD-cost:  131
c ---[2525]---> BDD-cost:  131
c ---[2524]---> BDD-cost:  131
c ---[2523]---> BDD-cost:  131
c ---[2522]---> BDD-cost:  131
c ---[2521]---> BDD-cost:  131
c ---[2520]---> BDD-cost:  131
c ---[2519]---> BDD-cost:  131
c ---[2518]---> BDD-cost:  131
c ---[2517]---> BDD-cost:  131
c ---[2516]---> BDD-cost:  131
c ---[2515]---> BDD-cost:  131
c ---[2514]---> BDD-cost:  131
c ---[2513]---> BDD-cost:  131
c ---[2512]---> BDD-cost:  131
c ---[2511]---> BDD-cost:  131
c ---[2510]---> BDD-cost:  131
c ---[2509]---> BDD-cost:  131
c ---[2508]---> BDD-cost:  131
c ---[2507]---> BDD-cost:  131
c ---[2506]---> BDD-cost:  131
c ---[2505]---> BDD-cost:  131
c ---[2504]---> BDD-cost:  131
c ---[2503]---> BDD-cost:  131
c ---[2502]---> BDD-cost:  131
c ---[2501]---> BDD-cost:  131
c ---[2500]---> BDD-cost:  131
c ---[2499]---> BDD-cost:  131
c ---[2498]---> BDD-cost:  131
c ---[2497]---> BDD-cost:  131
c ---[2496]---> BDD-cost:  131
c ---[2495]---> BDD-cost:  131
c ---[2494]---> BDD-cost:  131
c ---[2493]---> BDD-cost:  131
c ---[2492]---> BDD-cost:  131
c ---[2491]---> BDD-cost:  131
c ---[2490]---> BDD-cost:  131
c ---[2489]---> BDD-cost:  131
c ---[2488]---> BDD-cost:  131
c ---[2487]---> BDD-cost:  131
c ---[2486]---> BDD-cost:  131
c ---[2485]---> BDD-cost:  131
c ---[2484]---> BDD-cost:  131
c ---[2483]---> BDD-cost:  131
c ---[2482]---> BDD-cost:  131
c ---[2481]---> BDD-cost:  131
c ---[2480]---> BDD-cost:  131
c ---[2479]---> BDD-cost:  131
c ---[2478]---> BDD-cost:  131
c ---[2477]---> BDD-cost:  131
c ---[2476]---> BDD-cost:  131
c ---[2475]---> BDD-cost:  131
c ---[2474]---> BDD-cost:  131
c ---[2473]---> BDD-cost:  131
c ---[2472]---> BDD-cost:  131
c ---[2471]---> BDD-cost:  131
c ---[2470]---> BDD-cost:  131
c ---[2469]---> BDD-cost:  131
c ---[2468]---> BDD-cost:  131
c ---[2467]---> BDD-cost:  131
c ---[2466]---> BDD-cost:  131
c ---[2465]---> BDD-cost:  131
c ---[2464]---> BDD-cost:  131
c ---[2463]---> BDD-cost:  131
c ---[2462]---> BDD-cost:  131
c ---[2461]---> BDD-cost:  131
c ---[2460]---> BDD-cost:  131
c ---[2459]---> BDD-cost:  131
c ---[2458]---> BDD-cost:  131
c ---[2457]---> BDD-cost:  131
c ---[2456]---> BDD-cost:  131
c ---[2455]---> BDD-cost:  131
c ---[2454]---> BDD-cost:  131
c ---[2453]---> BDD-cost:  131
c ---[2452]---> BDD-cost:  131
c ---[2451]---> BDD-cost:  131
c ---[2450]---> BDD-cost:  131
c ---[2449]---> BDD-cost:  131
c ---[2448]---> BDD-cost:  131
c ---[2447]---> BDD-cost:  131
c ---[2446]---> BDD-cost:  131
c ---[2445]---> BDD-cost:  131
c ---[2444]---> BDD-cost:  131
c ---[2443]---> BDD-cost:  131
c ---[2442]---> BDD-cost:  131
c ---[2441]---> BDD-cost:  131
c ---[2440]---> BDD-cost:  131
c ---[2439]---> BDD-cost:  131
c ---[2438]---> BDD-cost:  131
c ---[2437]---> BDD-cost:  131
c ---[2436]---> BDD-cost:  131
c ---[2435]---> BDD-cost:  131
c ---[2434]---> BDD-cost:  131
c ---[2433]---> BDD-cost:  131
c ---[2432]---> BDD-cost:  131
c ---[2431]---> BDD-cost:  131
c ---[2430]---> BDD-cost:  131
c ---[2429]---> BDD-cost:  131
c ---[2428]---> BDD-cost:  131
c ---[2427]---> BDD-cost:  131
c ---[2426]---> BDD-cost:  131
c ---[2425]---> BDD-cost:  131
c ---[2424]---> BDD-cost:  131
c ---[2423]---> BDD-cost:  131
c ---[2422]---> BDD-cost:  131
c ---[2421]---> BDD-cost:  131
c ---[2420]---> BDD-cost:  131
c ---[2419]---> BDD-cost:  131
c ---[2418]---> BDD-cost:  131
c ---[2417]---> BDD-cost:  131
c ---[2416]---> BDD-cost:  131
c ---[2415]---> BDD-cost:  131
c ---[2414]---> BDD-cost:  131
c ---[2413]---> BDD-cost:  131
c ---[2412]---> BDD-cost:  131
c ---[2411]---> BDD-cost:  131
c ---[2410]---> BDD-cost:  131
c ---[2409]---> BDD-cost:  131
c ---[2408]---> BDD-cost:  131
c ---[2407]---> BDD-cost:  131
c ---[2406]---> BDD-cost:  131
c ---[2405]---> BDD-cost:  131
c ---[2404]---> BDD-cost:  131
c ---[2403]---> BDD-cost:  131
c ---[2402]---> BDD-cost:  131
c ---[2401]---> BDD-cost:  131
c ---[2400]---> BDD-cost:  131
c ---[2399]---> BDD-cost:  131
c ---[2398]---> BDD-cost:  131
c ---[2397]---> BDD-cost:  131
c ---[2396]---> BDD-cost:  131
c ---[2395]---> BDD-cost:  131
c ---[2394]---> BDD-cost:  131
c ---[2393]---> BDD-cost:  131
c ---[2392]---> BDD-cost:  131
c ---[2391]---> BDD-cost:  131
c ---[2390]---> BDD-cost:  131
c ---[2389]---> BDD-cost:  131
c ---[2388]---> BDD-cost:  131
c ---[2387]---> BDD-cost:  131
c ---[2386]---> BDD-cost:  131
c ---[2385]---> BDD-cost:  131
c ---[2384]---> BDD-cost:  131
c ---[2383]---> BDD-cost:  131
c ---[2382]---> BDD-cost:  131
c ---[2381]---> BDD-cost:  131
c ---[2380]---> BDD-cost:  131
c ---[2379]---> BDD-cost:  131
c ---[2378]---> BDD-cost:  131
c ---[2377]---> BDD-cost:  131
c ---[2376]---> BDD-cost:  131
c ---[2375]---> BDD-cost:  131
c ---[2374]---> BDD-cost:  131
c ---[2373]---> BDD-cost:  131
c ---[2372]---> BDD-cost:  131
c ---[2371]---> BDD-cost:  131
c ---[2370]---> BDD-cost:  131
c ---[2369]---> BDD-cost:  131
c ---[2368]---> BDD-cost:  131
c ---[2367]---> BDD-cost:  131
c ---[2366]---> BDD-cost:  131
c ---[2365]---> BDD-cost:  131
c ---[2364]---> BDD-cost:  131
c ---[2363]---> BDD-cost:  131
c ---[2362]---> BDD-cost:  131
c ---[2361]---> BDD-cost:  131
c ---[2360]---> BDD-cost:  131
c ---[2359]---> BDD-cost:  131
c ---[2358]---> BDD-cost:  131
c ---[2357]---> BDD-cost:  131
c ---[2356]---> BDD-cost:  131
c ---[2355]---> BDD-cost:  131
c ---[2354]---> BDD-cost:  131
c ---[2353]---> BDD-cost:  131
c ---[2352]---> BDD-cost:  131
c ---[2351]---> BDD-cost:  131
c ---[2350]---> BDD-cost:  131
c ---[2349]---> BDD-cost:  131
c ---[2348]---> BDD-cost:  131
c ---[2347]---> BDD-cost:  131
c ---[2346]---> BDD-cost:  131
c ---[2345]---> BDD-cost:  131
c ---[2344]---> BDD-cost:  131
c ---[2343]---> BDD-cost:  131
c ---[2342]---> BDD-cost:  131
c ---[2341]---> BDD-cost:  131
c ---[2340]---> BDD-cost:  131
c ---[2339]---> BDD-cost:  131
c ---[2338]---> BDD-cost:  131
c ---[2337]---> BDD-cost:  131
c ---[2336]---> BDD-cost:  131
c ---[2335]---> BDD-cost:  131
c ---[2334]---> BDD-cost:  131
c ---[2333]---> BDD-cost:  131
c ---[2332]---> BDD-cost:  131
c ---[2331]---> BDD-cost:  131
c ---[2330]---> BDD-cost:  131
c ---[2329]---> BDD-cost:  131
c ---[2328]---> BDD-cost:  131
c ---[2327]---> BDD-cost:  131
c ---[2326]---> BDD-cost:  131
c ---[2325]---> BDD-cost:  131
c ---[2324]---> BDD-cost:  131
c ---[2323]---> BDD-cost:  131
c ---[2322]---> BDD-cost:  131
c ---[2321]---> BDD-cost:  131
c ---[2320]---> BDD-cost:  131
c ---[2319]---> BDD-cost:  131
c ---[2318]---> BDD-cost:  131
c ---[2317]---> BDD-cost:  131
c ---[2316]---> BDD-cost:  131
c ---[2315]---> BDD-cost:  131
c ---[2314]---> BDD-cost:  131
c ---[2313]---> BDD-cost:  131
c ---[2312]---> BDD-cost:  131
c ---[2311]---> BDD-cost:  131
c ---[2310]---> BDD-cost:  131
c ---[2309]---> BDD-cost:  131
c ---[2308]---> BDD-cost:  131
c ---[2307]---> BDD-cost:  131
c ---[2306]---> BDD-cost:  131
c ---[2305]---> BDD-cost:  131
c ---[2304]---> BDD-cost:  131
c ---[2303]---> BDD-cost:  131
c ---[2302]---> BDD-cost:  131
c ---[2301]---> BDD-cost:  131
c ---[2300]---> BDD-cost:  131
c ---[2299]---> BDD-cost:  131
c ---[2298]---> BDD-cost:  131
c ---[2297]---> BDD-cost:  131
c ---[2296]---> BDD-cost:  131
c ---[2295]---> BDD-cost:  131
c ---[2294]---> BDD-cost:  131
c ---[2293]---> BDD-cost:  131
c ---[2292]---> BDD-cost:  131
c ---[2291]---> BDD-cost:  131
c ---[2290]---> BDD-cost:  131
c ---[2289]---> BDD-cost:  131
c ---[2288]---> BDD-cost:  131
c ---[2287]---> BDD-cost:  131
c ---[2286]---> BDD-cost:  131
c ---[2285]---> BDD-cost:  131
c ---[2284]---> BDD-cost:  131
c ---[2283]---> BDD-cost:  131
c ---[2282]---> BDD-cost:  131
c ---[2281]---> BDD-cost:  131
c ---[2280]---> BDD-cost:  131
c ---[2279]---> BDD-cost:  131
c ---[2278]---> BDD-cost:  131
c ---[2277]---> BDD-cost:  131
c ---[2276]---> BDD-cost:  131
c ---[2275]---> BDD-cost:  131
c ---[2274]---> BDD-cost:  131
c ---[2273]---> BDD-cost:  131
c ---[2272]---> BDD-cost:  131
c ---[2271]---> BDD-cost:  131
c ---[2270]---> BDD-cost:  131
c ---[2269]---> BDD-cost:  131
c ---[2268]---> BDD-cost:  131
c ---[2267]---> BDD-cost:  131
c ---[2266]---> BDD-cost:  131
c ---[2265]---> BDD-cost:  131
c ---[2264]---> BDD-cost:  131
c ---[2263]---> BDD-cost:  131
c ---[2262]---> BDD-cost:  131
c ---[2261]---> BDD-cost:  131
c ---[2260]---> BDD-cost:  131
c ---[2259]---> BDD-cost:  131
c ---[2257]---> Adder-cost: 788   maxlim: 1048575   bits: 21/20
c ---[2255]---> Adder-cost: 788   maxlim: 1048575   bits: 21/20
c ---[2253]---> Adder-cost: 788   maxlim: 1048575   bits: 21/20
c ---[2251]---> Adder-cost: 788   maxlim: 1048575   bits: 21/20
c ---[2249]---> Adder-cost: 788   maxlim: 1048575   bits: 21/20
c ---[2247]---> Adder-cost: 788   maxlim: 1048575   bits: 21/20
c ---[2245]---> Adder-cost: 788   maxlim: 1048575   bits: 21/20
c ---[2243]---> Adder-cost: 788   maxlim: 1048575   bits: 21/20
c ---[2241]---> Adder-cost: 788   maxlim: 1048575   bits: 21/20
c ---[2239]---> Adder-cost: 788   maxlim: 1048575   bits: 21/20
c ---[2237]---> Adder-cost: 788   maxlim: 1048575   bits: 21/20
c ---[2235]---> Adder-cost: 788   maxlim: 1048575   bits: 21/20
c ---[2233]---> Adder-cost: 788   maxlim: 1048575   bits: 21/20
c ---[2231]---> Adder-cost: 788   maxlim: 1048575   bits: 21/20
c ---[2229]---> Adder-cost: 788   maxlim: 1048575   bits: 21/20
c ---[2227]---> Adder-cost: 788   maxlim: 1048575   bits: 21/20
c ---[2225]---> Adder-cost: 788   maxlim: 1048575   bits: 21/20
c ---[2223]---> Adder-cost: 788   maxlim: 1048575   bits: 21/20
c ---[2221]---> Adder-cost: 788   maxlim: 1048575   bits: 21/20
c ---[2219]---> Adder-cost: 788   maxlim: 1048575   bits: 21/20
c ---[2217]---> Adder-cost: 788   maxlim: 1048575   bits: 21/20
c ---[2215]---> Adder-cost: 788   maxlim: 1048575   bits: 21/20
c ---[2213]---> Adder-cost: 788   maxlim: 1048575   bits: 21/20
c ---[2211]---> Adder-cost: 788   maxlim: 1048575   bits: 21/20
c ---[2209]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[2207]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[2205]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[2203]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[2201]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[2199]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[2197]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[2195]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[2193]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[2191]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[2189]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[2187]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[2185]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[2183]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[2181]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[2179]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[2177]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[2175]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[2173]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[2171]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[2169]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[2167]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[2165]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[2163]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[2161]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[2159]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[2157]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[2155]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[2153]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[2151]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[2149]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[2147]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[2145]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[2143]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[2141]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[2139]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[2137]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[2135]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[2133]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[2131]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[2129]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[2127]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[2125]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[2123]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[2121]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[2119]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[2117]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[2115]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[2113]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[2111]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[2109]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[2107]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[2105]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[2103]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[2101]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[2099]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[2097]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[2095]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[2093]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[2091]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[2089]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[2087]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[2085]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[2083]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[2081]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[2079]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[2077]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[2075]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[2073]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[2071]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[2069]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[2067]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[2065]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[2063]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[2061]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[2059]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[2057]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[2055]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[2053]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[2051]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[2049]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[2047]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[2045]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[2043]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[2041]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[2039]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[2037]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[2035]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[2033]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[2031]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[2029]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[2027]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[2025]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[2023]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[2021]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[2019]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[2017]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[2015]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[2013]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[2011]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[2009]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[2007]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[2005]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[2003]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[2001]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[1999]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[1997]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[1995]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[1993]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[1991]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[1989]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[1987]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[1985]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[1983]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[1981]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[1979]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[1977]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[1975]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[1973]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[1971]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[1969]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[1967]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[1965]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[1963]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[1961]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[1959]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[1957]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[1955]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[1953]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[1951]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[1949]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[1947]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[1945]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[1943]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[1941]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[1939]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[1937]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[1935]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[1933]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[1931]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[1929]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[1927]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[1925]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[1923]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[1921]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[1919]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[1917]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[1915]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[1913]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[1911]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[1909]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[1907]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[1905]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[1903]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[1901]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[1899]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[1897]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[1895]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[1893]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[1891]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[1889]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[1887]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[1885]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[1883]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[1881]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[1879]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[1877]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[1875]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[1873]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[1871]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[1869]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[1867]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[1865]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[1863]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[1861]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[1859]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[1857]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[1855]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[1853]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[1851]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[1849]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[1847]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[1845]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[1843]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[1841]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[1839]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[1837]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[1835]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[1833]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[1831]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[1829]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[1827]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[1825]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[1823]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[1821]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[1819]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[1817]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[1815]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[1813]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[1811]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[1809]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[1807]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[1805]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[1803]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[1801]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[1799]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[1797]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[1795]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[1793]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[1791]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[1789]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[1787]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[1785]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[1783]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[1781]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[1779]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[1777]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[1775]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[1773]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[1771]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[1769]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[1767]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[1765]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[1763]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[1761]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[1759]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[1757]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[1755]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[1753]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[1751]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[1749]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[1747]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[1745]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[1743]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[1741]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[1739]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[1737]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[1735]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[1733]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[1731]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[1729]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[1727]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[1725]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[1723]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[1721]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[1719]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[1717]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[1715]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[1713]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[1711]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[1709]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[1707]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[1705]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[1703]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[1701]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[1699]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[1697]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[1695]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[1693]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[1691]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[1689]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[1687]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[1685]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[1683]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[1681]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[1679]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[1677]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[1675]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[1673]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[1671]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[1669]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[1667]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[1665]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[1663]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[1661]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[1659]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[1657]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[1655]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[1653]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[1651]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[1649]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[1647]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[1645]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[1643]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[1641]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[1639]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[1637]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[1635]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[1633]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[1631]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[1629]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[1627]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[1625]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[1623]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[1621]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[1619]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[1617]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[1615]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[1613]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[1611]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[1609]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[1607]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[1605]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[1603]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[1601]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[1599]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[1597]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[1595]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[1593]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[1591]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[1589]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[1587]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[1585]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[1583]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[1581]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[1579]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[1577]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[1575]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[1573]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[1571]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[1569]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[1567]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[1565]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[1563]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[1561]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[1559]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[1557]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[1555]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[1553]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[1551]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[1549]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[1547]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[1545]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[1543]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[1541]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[1539]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[1537]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[1535]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[1533]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[1531]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[1529]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[1527]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[1525]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[1523]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[1521]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[1519]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[1517]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[1515]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[1513]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[1511]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[1509]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[1507]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[1505]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[1503]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[1501]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[1499]---> Adder-cost: 763   maxlim: 131071   bits: 18/17
c ---[1497]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[1495]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[1493]---> Adder-cost: 763   maxlim: 131071   bits: 18/17
c ---[1491]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[1489]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[1487]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[1485]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[1483]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[1481]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[1479]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[1477]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[1475]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[1473]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[1471]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[1469]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[1467]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[1465]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[1463]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[1461]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[1459]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[1457]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[1455]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[1453]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[1451]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[1449]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[1447]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[1445]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[1443]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[1441]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[1439]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[1437]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[1435]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[1433]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[1431]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[1429]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[1427]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[1425]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[1423]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[1421]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[1419]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[1417]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[1415]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[1413]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[1411]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[1409]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[1407]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[1405]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[1403]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[1401]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[1399]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[1397]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[1395]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[1393]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[1391]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[1389]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[1387]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[1385]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[1383]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[1381]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[1379]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[1377]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[1375]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[1373]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[1371]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[1369]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[1367]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[1365]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[1363]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[1361]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[1359]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[1357]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[1355]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[1353]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[1351]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[1349]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[1347]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[1345]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[1343]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[1341]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[1339]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[1337]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[1335]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[1333]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[1331]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[1329]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[1327]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[1325]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[1323]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[1321]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[1319]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[1317]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[1315]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[1313]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[1311]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[1309]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[1307]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[1305]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[1303]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[1301]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[1299]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[1297]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[1295]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[1293]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[1291]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[1289]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[1287]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[1285]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[1283]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[1281]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[1279]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[1277]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[1275]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[1273]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[1271]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[1269]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[1267]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[1265]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[1263]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[1261]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[1259]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[1257]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[1255]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[1253]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[1251]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[1249]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[1247]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[1245]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[1243]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[1241]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[1239]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[1237]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[1235]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[1233]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[1231]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[1229]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[1227]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[1225]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[1223]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[1221]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[1219]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[1217]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[1215]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[1213]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[1211]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[1209]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[1207]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[1205]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[1203]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[1201]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[1199]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[1197]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[1195]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[1193]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[1191]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[1189]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[1187]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[1185]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[1183]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[1181]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[1179]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[1177]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[1175]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[1173]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[1171]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[1169]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[1167]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[1165]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[1163]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[1161]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[1159]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[1157]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[1155]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[1153]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[1151]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[1149]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[1147]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[1145]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[1143]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[1141]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[1139]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[1137]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[1135]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[1133]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[1131]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[1129]---> Adder-cost: 763   maxlim: 131071   bits: 18/17
c ---[1127]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[1125]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[1123]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[1121]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[1119]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[1117]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[1115]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[1113]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[1111]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[1109]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[1107]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[1105]---> Adder-cost: 14004   maxlim: 1048575   bits: 21/20
c ---[1103]---> Adder-cost: 13986   maxlim: 1048575   bits: 21/20
c ---[1101]---> Adder-cost: 13974   maxlim: 1048575   bits: 21/20
c ---[1099]---> Adder-cost: 13981   maxlim: 1048575   bits: 21/20
c ---[1097]---> Adder-cost: 14054   maxlim: 1048575   bits: 21/20
c ---[1095]---> Adder-cost: 13922   maxlim: 1048575   bits: 21/20
c ---[1093]---> Adder-cost: 13949   maxlim: 1048575   bits: 21/20
c ---[1091]---> Adder-cost: 13891   maxlim: 1048575   bits: 21/20
c ---[1089]---> Adder-cost: 13891   maxlim: 1048575   bits: 21/20
c ---[1087]---> Adder-cost: 13963   maxlim: 1048575   bits: 21/20
c ---[1085]---> Adder-cost: 13952   maxlim: 1048575   bits: 21/20
c ---[1083]---> Adder-cost: 13867   maxlim: 1048575   bits: 21/20
c ---[1081]---> Adder-cost: 13904   maxlim: 1048575   bits: 21/20
c ---[1079]---> Adder-cost: 13902   maxlim: 1048575   bits: 21/20
c ---[1077]---> Adder-cost: 13929   maxlim: 1048575   bits: 21/20
c ---[1075]---> Adder-cost: 13811   maxlim: 1048575   bits: 21/20
c ---[1073]---> Adder-cost: 13787   maxlim: 1048575   bits: 21/20
c ---[1071]---> Adder-cost: 13971   maxlim: 1048575   bits: 21/20
c ---[1069]---> Adder-cost: 13756   maxlim: 1048575   bits: 21/20
c ---[1067]---> Adder-cost: 13836   maxlim: 1048575   bits: 21/20
c ---[1065]---> Adder-cost: 13743   maxlim: 1048575   bits: 21/20
c ---[1063]---> Adder-cost: 13726   maxlim: 1048575   bits: 21/20
c ---[1061]---> Adder-cost: 13788   maxlim: 1048575   bits: 21/20
c ---[1059]---> Adder-cost: 13757   maxlim: 1048575   bits: 21/20
c ---[1057]---> BDD-cost:   63
c ---[1055]---> BDD-cost:   63
c ---[1053]---> BDD-cost:   63
c ---[1051]---> BDD-cost:   63
c ---[1049]---> BDD-cost:   63
c ---[1047]---> BDD-cost:   63
c ---[1045]---> BDD-cost:   63
c ---[1043]---> BDD-cost:   63
c ---[1041]---> BDD-cost:   63
c ---[1039]---> BDD-cost:   63
c ---[1037]---> BDD-cost:   63
c ---[1035]---> BDD-cost:   63
c ---[1033]---> BDD-cost:   63
c ---[1031]---> BDD-cost:   63
c ---[1029]---> BDD-cost:   63
c ---[1027]---> BDD-cost:   63
c ---[1025]---> BDD-cost:   63
c ---[1023]---> BDD-cost:   63
c ---[1021]---> BDD-cost:   63
c ---[1019]---> BDD-cost:   63
c ---[1017]---> BDD-cost:   63
c ---[1015]---> BDD-cost:   63
c ---[1013]---> BDD-cost:   63
c ---[1011]---> BDD-cost:   63
c ---[1009]---> BDD-cost:   63
c ---[1007]---> BDD-cost:   63
c ---[1005]---> BDD-cost:   63
c ---[1003]---> BDD-cost:   63
c ---[1001]---> BDD-cost:   63
c ---[ 999]---> BDD-cost:   63
c ---[ 997]---> BDD-cost:   63
c ---[ 995]---> BDD-cost:   63
c ---[ 993]---> BDD-cost:   63
c ---[ 991]---> BDD-cost:   63
c ---[ 989]---> BDD-cost:   63
c ---[ 987]---> BDD-cost:   63
c ---[ 985]---> BDD-cost:   63
c ---[ 983]---> BDD-cost:   63
c ---[ 981]---> BDD-cost:   63
c ---[ 979]---> BDD-cost:   63
c ---[ 977]---> BDD-cost:   63
c ---[ 975]---> BDD-cost:   63
c ---[ 973]---> BDD-cost:   63
c ---[ 971]---> BDD-cost:   63
c ---[ 969]---> BDD-cost:   63
c ---[ 967]---> BDD-cost:   63
c ---[ 965]---> BDD-cost:   63
c ---[ 963]---> BDD-cost:   63
c ---[ 962]---> Adder-cost: 438   maxlim: 131070   bits: 18/17
c ---[ 961]---> Adder-cost: 752   maxlim: 131070   bits: 18/17
c ---[ 960]---> Adder-cost: 752   maxlim: 131070   bits: 18/17
c ---[ 959]---> Adder-cost: 510   maxlim: 131070   bits: 18/17
c ---[ 958]---> Adder-cost: 752   maxlim: 131070   bits: 18/17
c ---[ 957]---> Adder-cost: 752   maxlim: 131070   bits: 18/17
c ---[ 956]---> Adder-cost: 532   maxlim: 131070   bits: 18/17
c ---[ 955]---> Adder-cost: 748   maxlim: 131070   bits: 18/17
c ---[ 954]---> Adder-cost: 722   maxlim: 65534   bits: 17/16
c ---[ 953]---> Adder-cost: 746   maxlim: 131070   bits: 18/17
c ---[ 952]---> Adder-cost: 752   maxlim: 131070   bits: 18/17
c ---[ 951]---> Adder-cost: 752   maxlim: 131070   bits: 18/17
c ---[ 950]---> Adder-cost: 508   maxlim: 131070   bits: 18/17
c ---[ 949]---> Adder-cost: 750   maxlim: 131070   bits: 18/17
c ---[ 948]---> Adder-cost: 752   maxlim: 131070   bits: 18/17
c ---[ 947]---> Adder-cost: 536   maxlim: 131070   bits: 18/17
c ---[ 946]---> Adder-cost: 576   maxlim: 131070   bits: 18/17
c ---[ 945]---> Adder-cost: 752   maxlim: 131070   bits: 18/17
c ---[ 944]---> Adder-cost: 740   maxlim: 131070   bits: 18/17
c ---[ 943]---> Adder-cost: 649   maxlim: 131070   bits: 18/17
c ---[ 942]---> Adder-cost: 752   maxlim: 131070   bits: 18/17
c ---[ 941]---> Adder-cost: 716   maxlim: 65534   bits: 17/16
c ---[ 940]---> Adder-cost: 673   maxlim: 131070   bits: 18/17
c ---[ 939]---> Adder-cost: 716   maxlim: 131070   bits: 18/17
c ---[ 938]---> Adder-cost: 744   maxlim: 131070   bits: 18/17
c ---[ 937]---> Adder-cost: 750   maxlim: 131070   bits: 18/17
c ---[ 936]---> Adder-cost: 752   maxlim: 131070   bits: 18/17
c ---[ 935]---> Adder-cost: 450   maxlim: 131070   bits: 18/17
c ---[ 934]---> Adder-cost: 748   maxlim: 131070   bits: 18/17
c ---[ 933]---> Adder-cost: 505   maxlim: 131070   bits: 18/17
c ---[ 932]---> Adder-cost: 750   maxlim: 131070   bits: 18/17
c ---[ 931]---> Adder-cost: 532   maxlim: 131070   bits: 18/17
c ---[ 930]---> Adder-cost: 748   maxlim: 131070   bits: 18/17
c ---[ 929]---> Adder-cost: 752   maxlim: 131070   bits: 18/17
c ---[ 928]---> Adder-cost: 752   maxlim: 131070   bits: 18/17
c ---[ 927]---> Adder-cost: 746   maxlim: 131070   bits: 18/17
c ---[ 926]---> Adder-cost: 752   maxlim: 131070   bits: 18/17
c ---[ 925]---> Adder-cost: 682   maxlim: 131070   bits: 18/17
c ---[ 924]---> Adder-cost: 752   maxlim: 131070   bits: 18/17
c ---[ 923]---> Adder-cost: 750   maxlim: 131070   bits: 18/17
c ---[ 922]---> Adder-cost: 718   maxlim: 131070   bits: 18/17
c ---[ 921]---> Adder-cost: 748   maxlim: 131070   bits: 18/17
c ---[ 920]---> Adder-cost: 752   maxlim: 131070   bits: 18/17
c ---[ 919]---> Adder-cost: 752   maxlim: 131070   bits: 18/17
c ---[ 918]---> Adder-cost: 748   maxlim: 131070   bits: 18/17
c ---[ 917]---> Adder-cost: 434   maxlim: 131070   bits: 18/17
c ---[ 916]---> Adder-cost: 748   maxlim: 131070   bits: 18/17
c ---[ 915]---> Adder-cost: 750   maxlim: 131070   bits: 18/17
c ---[ 914]---> Adder-cost: 499   maxlim: 131070   bits: 18/17
c ---[ 913]---> Adder-cost: 749   maxlim: 131070   bits: 18/17
c ---[ 912]---> Adder-cost: 752   maxlim: 131070   bits: 18/17
c ---[ 911]---> Adder-cost: 534   maxlim: 131070   bits: 18/17
c ---[ 910]---> Adder-cost: 580   maxlim: 131070   bits: 18/17
c ---[ 909]---> Adder-cost: 752   maxlim: 131070   bits: 18/17
c ---[ 908]---> Adder-cost: 648   maxlim: 131070   bits: 18/17
c ---[ 907]---> Adder-cost: 682   maxlim: 131070   bits: 18/17
c ---[ 906]---> Adder-cost: 752   maxlim: 131070   bits: 18/17
c ---[ 905]---> Adder-cost: 752   maxlim: 131070   bits: 18/17
c ---[ 904]---> Adder-cost: 750   maxlim: 131070   bits: 18/17
c ---[ 903]---> Adder-cost: 746   maxlim: 131070   bits: 18/17
c ---[ 902]---> Adder-cost: 749   maxlim: 131070   bits: 18/17
c ---[ 901]---> Adder-cost: 472   maxlim: 131070   bits: 18/17
c ---[ 900]---> Adder-cost: 749   maxlim: 131070   bits: 18/17
c ---[ 899]---> Adder-cost: 736   maxlim: 131070   bits: 18/17
c ---[ 898]---> Adder-cost: 740   maxlim: 131070   bits: 18/17
c ---[ 897]---> Adder-cost: 580   maxlim: 131070   bits: 18/17
c ---[ 896]---> Adder-cost: 742   maxlim: 131070   bits: 18/17
c ---[ 895]---> Adder-cost: 649   maxlim: 131070   bits: 18/17
c ---[ 894]---> Adder-cost: 678   maxlim: 131070   bits: 18/17
c ---[ 893]---> Adder-cost: 750   maxlim: 131070   bits: 18/17
c ---[ 892]---> Adder-cost: 718   maxlim: 131070   bits: 18/17
c ---[ 891]---> Adder-cost: 752   maxlim: 131070   bits: 18/17
c ---[ 890]---> Adder-cost: 752   maxlim: 131070   bits: 18/17
c ---[ 889]---> Adder-cost: 428   maxlim: 131070   bits: 18/17
c ---[ 888]---> Adder-cost: 750   maxlim: 131070   bits: 18/17
c ---[ 887]---> Adder-cost: 480   maxlim: 131070   bits: 18/17
c ---[ 886]---> Adder-cost: 750   maxlim: 131070   bits: 18/17
c ---[ 885]---> Adder-cost: 752   maxlim: 131070   bits: 18/17
c ---[ 884]---> Adder-cost: 534   maxlim: 131070   bits: 18/17
c ---[ 883]---> Adder-cost: 752   maxlim: 131070   bits: 18/17
c ---[ 882]---> Adder-cost: 752   maxlim: 131070   bits: 18/17
c ---[ 881]---> Adder-cost: 752   maxlim: 131070   bits: 18/17
c ---[ 880]---> Adder-cost: 748   maxlim: 131070   bits: 18/17
c ---[ 879]---> Adder-cost: 648   maxlim: 131070   bits: 18/17
c ---[ 878]---> Adder-cost: 752   maxlim: 131070   bits: 18/17
c ---[ 877]---> Adder-cost: 740   maxlim: 131070   bits: 18/17
c ---[ 876]---> Adder-cost: 744   maxlim: 131070   bits: 18/17
c ---[ 875]---> Adder-cost: 746   maxlim: 131070   bits: 18/17
c ---[ 874]---> Adder-cost: 744   maxlim: 131070   bits: 18/17
c ---[ 873]---> Adder-cost: 436   maxlim: 131070   bits: 18/17
c ---[ 872]---> Adder-cost: 544   maxlim: 131070   bits: 18/17
c ---[ 871]---> Adder-cost: 740   maxlim: 131070   bits: 18/17
c ---[ 870]---> Adder-cost: 738   maxlim: 131070   bits: 18/17
c ---[ 869]---> Adder-cost: 570   maxlim: 131070   bits: 18/17
c ---[ 868]---> Adder-cost: 752   maxlim: 131070   bits: 18/17
c ---[ 867]---> Adder-cost: 752   maxlim: 131070   bits: 18/17
c ---[ 866]---> Adder-cost: 649   maxlim: 131070   bits: 18/17
c ---[ 865]---> Adder-cost: 738   maxlim: 131070   bits: 18/17
c ---[ 864]---> Adder-cost: 750   maxlim: 131070   bits: 18/17
c ---[ 863]---> Adder-cost: 752   maxlim: 131070   bits: 18/17
c ---[ 862]---> Adder-cost: 748   maxlim: 131070   bits: 18/17
c ---[ 861]---> Adder-cost: 750   maxlim: 131070   bits: 18/17
c ---[ 860]---> Adder-cost: 748   maxlim: 131070   bits: 18/17
c ---[ 859]---> Adder-cost: 486   maxlim: 131070   bits: 18/17
c ---[ 858]---> Adder-cost: 752   maxlim: 131070   bits: 18/17
c ---[ 857]---> Adder-cost: 748   maxlim: 131070   bits: 18/17
c ---[ 856]---> Adder-cost: 530   maxlim: 131070   bits: 18/17
c ---[ 855]---> Adder-cost: 748   maxlim: 131070   bits: 18/17
c ---[ 854]---> Adder-cost: 574   maxlim: 131070   bits: 18/17
c ---[ 853]---> Adder-cost: 748   maxlim: 131070   bits: 18/17
c ---[ 852]---> Adder-cost: 646   maxlim: 131070   bits: 18/17
c ---[ 851]---> Adder-cost: 748   maxlim: 131070   bits: 18/17
c ---[ 850]---> Adder-cost: 750   maxlim: 131070   bits: 18/17
c ---[ 849]---> Adder-cost: 746   maxlim: 131070   bits: 18/17
c ---[ 848]---> Adder-cost: 750   maxlim: 131070   bits: 18/17
c ---[ 847]---> Adder-cost: 434   maxlim: 131070   bits: 18/17
c ---[ 846]---> Adder-cost: 750   maxlim: 131070   bits: 18/17
c ---[ 845]---> Adder-cost: 750   maxlim: 131070   bits: 18/17
c ---[ 844]---> Adder-cost: 748   maxlim: 131070   bits: 18/17
c ---[ 843]---> Adder-cost: 748   maxlim: 131070   bits: 18/17
c ---[ 842]---> Adder-cost: 530   maxlim: 131070   bits: 18/17
c ---[ 841]---> Adder-cost: 752   maxlim: 131070   bits: 18/17
c ---[ 840]---> Adder-cost: 748   maxlim: 131070   bits: 18/17
c ---[ 839]---> Adder-cost: 576   maxlim: 131070   bits: 18/17
c ---[ 838]---> Adder-cost: 752   maxlim: 131070   bits: 18/17
c ---[ 837]---> Adder-cost: 752   maxlim: 131070   bits: 18/17
c ---[ 836]---> Adder-cost: 648   maxlim: 131070   bits: 18/17
c ---[ 835]---> Adder-cost: 752   maxlim: 131070   bits: 18/17
c ---[ 834]---> Adder-cost: 752   maxlim: 131070   bits: 18/17
c ---[ 833]---> Adder-cost: 746   maxlim: 131070   bits: 18/17
c ---[ 832]---> Adder-cost: 712   maxlim: 131070   bits: 18/17
c ---[ 831]---> Adder-cost: 752   maxlim: 131070   bits: 18/17
c ---[ 830]---> Adder-cost: 752   maxlim: 131070   bits: 18/17
c ---[ 829]---> Adder-cost: 752   maxlim: 131070   bits: 18/17
c ---[ 828]---> Adder-cost: 746   maxlim: 131070   bits: 18/17
c ---[ 827]---> Adder-cost: 752   maxlim: 131070   bits: 18/17
c ---[ 826]---> Adder-cost: 486   maxlim: 131070   bits: 18/17
c ---[ 825]---> Adder-cost: 748   maxlim: 131070   bits: 18/17
c ---[ 824]---> Adder-cost: 752   maxlim: 131070   bits: 18/17
c ---[ 823]---> Adder-cost: 744   maxlim: 131070   bits: 18/17
c ---[ 822]---> Adder-cost: 745   maxlim: 131070   bits: 18/17
c ---[ 821]---> Adder-cost: 746   maxlim: 131070   bits: 18/17
c ---[ 820]---> Adder-cost: 682   maxlim: 131070   bits: 18/17
c ---[ 819]---> Adder-cost: 747   maxlim: 131070   bits: 18/17
c ---[ 818]---> Adder-cost: 750   maxlim: 131070   bits: 18/17
c ---[ 817]---> Adder-cost: 718   maxlim: 131070   bits: 18/17
c ---[ 816]---> Adder-cost: 748   maxlim: 131070   bits: 18/17
c ---[ 815]---> Adder-cost: 750   maxlim: 131070   bits: 18/17
c ---[ 814]---> Adder-cost: 750   maxlim: 131070   bits: 18/17
c ---[ 813]---> Adder-cost: 429   maxlim: 131070   bits: 18/17
c ---[ 812]---> Adder-cost: 736   maxlim: 131070   bits: 18/17
c ---[ 811]---> Adder-cost: 724   maxlim: 131070   bits: 18/17
c ---[ 810]---> Adder-cost: 538   maxlim: 131070   bits: 18/17
c ---[ 809]---> Adder-cost: 744   maxlim: 131070   bits: 18/17
c ---[ 808]---> Adder-cost: 748   maxlim: 131070   bits: 18/17
c ---[ 807]---> Adder-cost: 728   maxlim: 65534   bits: 17/16
c ---[ 806]---> Adder-cost: 750   maxlim: 131070   bits: 18/17
c ---[ 805]---> Adder-cost: 684   maxlim: 131070   bits: 18/17
c ---[ 804]---> Adder-cost: 750   maxlim: 131070   bits: 18/17
c ---[ 803]---> Adder-cost: 748   maxlim: 131070   bits: 18/17
c ---[ 802]---> Adder-cost: 746   maxlim: 131070   bits: 18/17
c ---[ 801]---> Adder-cost: 752   maxlim: 131070   bits: 18/17
c ---[ 800]---> Adder-cost: 748   maxlim: 131070   bits: 18/17
c ---[ 799]---> Adder-cost: 748   maxlim: 131070   bits: 18/17
c ---[ 798]---> Adder-cost: 752   maxlim: 131070   bits: 18/17
c ---[ 797]---> Adder-cost: 752   maxlim: 131070   bits: 18/17
c ---[ 796]---> Adder-cost: 536   maxlim: 131070   bits: 18/17
c ---[ 795]---> Adder-cost: 752   maxlim: 131070   bits: 18/17
c ---[ 794]---> Adder-cost: 582   maxlim: 131070   bits: 18/17
c ---[ 793]---> Adder-cost: 746   maxlim: 131070   bits: 18/17
c ---[ 792]---> Adder-cost: 746   maxlim: 131070   bits: 18/17
c ---[ 791]---> Adder-cost: 646   maxlim: 131070   bits: 18/17
c ---[ 790]---> Adder-cost: 752   maxlim: 131070   bits: 18/17
c ---[ 789]---> Adder-cost: 743   maxlim: 131070   bits: 18/17
c ---[ 788]---> Adder-cost: 680   maxlim: 131070   bits: 18/17
c ---[ 787]---> Adder-cost: 750   maxlim: 131070   bits: 18/17
c ---[ 786]---> Adder-cost: 712   maxlim: 131070   bits: 18/17
c ---[ 785]---> Adder-cost: 746   maxlim: 131070   bits: 18/17
c ---[ 784]---> Adder-cost: 748   maxlim: 131070   bits: 18/17
c ---[ 783]---> Adder-cost: 434   maxlim: 131070   bits: 18/17
c ---[ 782]---> Adder-cost: 732   maxlim: 131070   bits: 18/17
c ---[ 781]---> Adder-cost: 728   maxlim: 65534   bits: 17/16
c ---[ 780]---> Adder-cost: 749   maxlim: 131070   bits: 18/17
c ---[ 779]---> Adder-cost: 745   maxlim: 131070   bits: 18/17
c ---[ 778]---> Adder-cost: 742   maxlim: 131070   bits: 18/17
c ---[ 777]---> Adder-cost: 735   maxlim: 131070   bits: 18/17
c ---[ 776]---> Adder-cost: 752   maxlim: 131070   bits: 18/17
c ---[ 775]---> Adder-cost: 748   maxlim: 131070   bits: 18/17
c ---[ 774]---> Adder-cost: 748   maxlim: 131070   bits: 18/17
c ---[ 773]---> Adder-cost: 426   maxlim: 65534   bits: 17/16
c ---[ 772]---> Adder-cost: 748   maxlim: 131070   bits: 18/17
c ---[ 771]---> Adder-cost: 490   maxlim: 131070   bits: 18/17
c ---[ 770]---> Adder-cost: 752   maxlim: 131070   bits: 18/17
c ---[ 769]---> Adder-cost: 536   maxlim: 131070   bits: 18/17
c ---[ 768]---> Adder-cost: 752   maxlim: 131070   bits: 18/17
c ---[ 767]---> Adder-cost: 752   maxlim: 131070   bits: 18/17
c ---[ 766]---> Adder-cost: 620   maxlim: 131070   bits: 18/17
c ---[ 765]---> Adder-cost: 736   maxlim: 131070   bits: 18/17
c ---[ 764]---> Adder-cost: 678   maxlim: 131070   bits: 18/17
c ---[ 763]---> Adder-cost: 748   maxlim: 131070   bits: 18/17
c ---[ 762]---> Adder-cost: 718   maxlim: 131070   bits: 18/17
c ---[ 761]---> Adder-cost: 752   maxlim: 131070   bits: 18/17
c ---[ 760]---> Adder-cost: 750   maxlim: 131070   bits: 18/17
c ---[ 759]---> Adder-cost: 741   maxlim: 131070   bits: 18/17
c ---[ 758]---> Adder-cost: 745   maxlim: 131070   bits: 18/17
c ---[ 757]---> Adder-cost: 752   maxlim: 131070   bits: 18/17
c ---[ 756]---> Adder-cost: 480   maxlim: 131070   bits: 18/17
c ---[ 755]---> Adder-cost: 748   maxlim: 131070   bits: 18/17
c ---[ 754]---> Adder-cost: 580   maxlim: 131070   bits: 18/17
c ---[ 753]---> Adder-cost: 744   maxlim: 131070   bits: 18/17
c ---[ 752]---> Adder-cost: 744   maxlim: 131070   bits: 18/17
c ---[ 751]---> Adder-cost: 626   maxlim: 131070   bits: 18/17
c ---[ 750]---> Adder-cost: 746   maxlim: 131070   bits: 18/17
c ---[ 749]---> Adder-cost: 682   maxlim: 131070   bits: 18/17
c ---[ 748]---> Adder-cost: 750   maxlim: 131070   bits: 18/17
c ---[ 747]---> Adder-cost: 714   maxlim: 131070   bits: 18/17
c ---[ 746]---> Adder-cost: 748   maxlim: 131070   bits: 18/17
c ---[ 745]---> Adder-cost: 752   maxlim: 131070   bits: 18/17
c ---[ 744]---> Adder-cost: 752   maxlim: 131070   bits: 18/17
c ---[ 743]---> Adder-cost: 752   maxlim: 131070   bits: 18/17
c ---[ 742]---> Adder-cost: 486   maxlim: 131070   bits: 18/17
c ---[ 741]---> Adder-cost: 746   maxlim: 131070   bits: 18/17
c ---[ 740]---> Adder-cost: 520   maxlim: 65534   bits: 17/16
c ---[ 739]---> Adder-cost: 749   maxlim: 131070   bits: 18/17
c ---[ 738]---> Adder-cost: 740   maxlim: 131070   bits: 18/17
c ---[ 737]---> Adder-cost: 742   maxlim: 131070   bits: 18/17
c ---[ 736]---> Adder-cost: 618   maxlim: 131070   bits: 18/17
c ---[ 735]---> Adder-cost: 728   maxlim: 65534   bits: 17/16
c ---[ 734]---> Adder-cost: 712   maxlim: 131070   bits: 18/17
c ---[ 733]---> Adder-cost: 752   maxlim: 131070   bits: 18/17
c ---[ 732]---> Adder-cost: 750   maxlim: 131070   bits: 18/17
c ---[ 731]---> Adder-cost: 752   maxlim: 131070   bits: 18/17
c ---[ 730]---> Adder-cost: 746   maxlim: 131070   bits: 18/17
c ---[ 729]---> Adder-cost: 536   maxlim: 131070   bits: 18/17
c ---[ 728]---> Adder-cost: 752   maxlim: 131070   bits: 18/17
c ---[ 727]---> Adder-cost: 745   maxlim: 131070   bits: 18/17
c ---[ 726]---> Adder-cost: 748   maxlim: 131070   bits: 18/17
c ---[ 725]---> Adder-cost: 748   maxlim: 131070   bits: 18/17
c ---[ 724]---> Adder-cost: 626   maxlim: 131070   bits: 18/17
c ---[ 723]---> Adder-cost: 752   maxlim: 131070   bits: 18/17
c ---[ 722]---> Adder-cost: 678   maxlim: 131070   bits: 18/17
c ---[ 721]---> Adder-cost: 712   maxlim: 131070   bits: 18/17
c ---[ 720]---> Adder-cost: 750   maxlim: 131070   bits: 18/17
c ---[ 719]---> Adder-cost: 752   maxlim: 131070   bits: 18/17
c ---[ 718]---> Adder-cost: 728   maxlim: 65534   bits: 17/16
c ---[ 717]---> Adder-cost: 748   maxlim: 131070   bits: 18/17
c ---[ 716]---> Adder-cost: 490   maxlim: 131070   bits: 18/17
c ---[ 715]---> Adder-cost: 742   maxlim: 131070   bits: 18/17
c ---[ 714]---> Adder-cost: 742   maxlim: 131070   bits: 18/17
c ---[ 713]---> Adder-cost: 530   maxlim: 131070   bits: 18/17
c ---[ 712]---> Adder-cost: 747   maxlim: 131070   bits: 18/17
c ---[ 711]---> Adder-cost: 746   maxlim: 131070   bits: 18/17
c ---[ 710]---> Adder-cost: 620   maxlim: 131070   bits: 18/17
c ---[ 709]---> Adder-cost: 748   maxlim: 131070   bits: 18/17
c ---[ 708]---> Adder-cost: 740   maxlim: 131070   bits: 18/17
c ---[ 707]---> Adder-cost: 680   maxlim: 131070   bits: 18/17
c ---[ 706]---> Adder-cost: 728   maxlim: 65534   bits: 17/16
c ---[ 705]---> Adder-cost: 750   maxlim: 131070   bits: 18/17
c ---[ 704]---> Adder-cost: 752   maxlim: 131070   bits: 18/17
c ---[ 703]---> Adder-cost: 752   maxlim: 131070   bits: 18/17
c ---[ 702]---> Adder-cost: 744   maxlim: 131070   bits: 18/17
c ---[ 701]---> Adder-cost: 752   maxlim: 131070   bits: 18/17
c ---[ 700]---> Adder-cost: 442   maxlim: 131070   bits: 18/17
c ---[ 699]---> Adder-cost: 752   maxlim: 131070   bits: 18/17
c ---[ 698]---> Adder-cost: 490   maxlim: 131070   bits: 18/17
c ---[ 697]---> Adder-cost: 748   maxlim: 131070   bits: 18/17
c ---[ 696]---> Adder-cost: 530   maxlim: 131070   bits: 18/17
c ---[ 695]---> Adder-cost: 750   maxlim: 131070   bits: 18/17
c ---[ 694]---> Adder-cost: 752   maxlim: 131070   bits: 18/17
c ---[ 693]---> Adder-cost: 748   maxlim: 131070   bits: 18/17
c ---[ 692]---> Adder-cost: 622   maxlim: 131070   bits: 18/17
c ---[ 691]---> Adder-cost: 746   maxlim: 131070   bits: 18/17
c ---[ 690]---> Adder-cost: 752   maxlim: 131070   bits: 18/17
c ---[ 689]---> Adder-cost: 726   maxlim: 65534   bits: 17/16
c ---[ 688]---> Adder-cost: 716   maxlim: 131070   bits: 18/17
c ---[ 687]---> Adder-cost: 752   maxlim: 131070   bits: 18/17
c ---[ 686]---> Adder-cost: 750   maxlim: 131070   bits: 18/17
c ---[ 685]---> Adder-cost: 746   maxlim: 131070   bits: 18/17
c ---[ 684]---> Adder-cost: 430   maxlim: 131070   bits: 18/17
c ---[ 683]---> Adder-cost: 744   maxlim: 131070   bits: 18/17
c ---[ 682]---> Adder-cost: 752   maxlim: 131070   bits: 18/17
c ---[ 681]---> Adder-cost: 530   maxlim: 131070   bits: 18/17
c ---[ 680]---> Adder-cost: 748   maxlim: 131070   bits: 18/17
c ---[ 679]---> Adder-cost: 584   maxlim: 131070   bits: 18/17
c ---[ 678]---> Adder-cost: 746   maxlim: 131070   bits: 18/17
c ---[ 677]---> Adder-cost: 752   maxlim: 131070   bits: 18/17
c ---[ 676]---> Adder-cost: 624   maxlim: 131070   bits: 18/17
c ---[ 675]---> Adder-cost: 746   maxlim: 131070   bits: 18/17
c ---[ 674]---> Adder-cost: 743   maxlim: 131070   bits: 18/17
c ---[ 673]---> Adder-cost: 750   maxlim: 131070   bits: 18/17
c ---[ 672]---> Adder-cost: 752   maxlim: 131070   bits: 18/17
c ---[ 671]---> Adder-cost: 752   maxlim: 131070   bits: 18/17
c ---[ 670]---> Adder-cost: 434   maxlim: 131070   bits: 18/17
c ---[ 669]---> Adder-cost: 752   maxlim: 131070   bits: 18/17
c ---[ 668]---> Adder-cost: 752   maxlim: 131070   bits: 18/17
c ---[ 667]---> Adder-cost: 750   maxlim: 131070   bits: 18/17
c ---[ 666]---> Adder-cost: 744   maxlim: 131070   bits: 18/17
c ---[ 665]---> Adder-cost: 536   maxlim: 131070   bits: 18/17
c ---[ 664]---> Adder-cost: 748   maxlim: 131070   bits: 18/17
c ---[ 663]---> Adder-cost: 752   maxlim: 131070   bits: 18/17
c ---[ 662]---> Adder-cost: 746   maxlim: 131070   bits: 18/17
c ---[ 661]---> Adder-cost: 616   maxlim: 131070   bits: 18/17
c ---[ 660]---> Adder-cost: 752   maxlim: 131070   bits: 18/17
c ---[ 659]---> Adder-cost: 748   maxlim: 131070   bits: 18/17
c ---[ 658]---> Adder-cost: 678   maxlim: 131070   bits: 18/17
c ---[ 657]---> Adder-cost: 746   maxlim: 131070   bits: 18/17
c ---[ 656]---> Adder-cost: 752   maxlim: 131070   bits: 18/17
c ---[ 655]---> Adder-cost: 752   maxlim: 131070   bits: 18/17
c ---[ 654]---> Adder-cost: 748   maxlim: 131070   bits: 18/17
c ---[ 653]---> Adder-cost: 432   maxlim: 131070   bits: 18/17
c ---[ 652]---> Adder-cost: 748   maxlim: 131070   bits: 18/17
c ---[ 651]---> Adder-cost: 752   maxlim: 131070   bits: 18/17
c ---[ 650]---> Adder-cost: 480   maxlim: 131070   bits: 18/17
c ---[ 649]---> Adder-cost: 748   maxlim: 131070   bits: 18/17
c ---[ 648]---> Adder-cost: 534   maxlim: 131070   bits: 18/17
c ---[ 647]---> Adder-cost: 744   maxlim: 131070   bits: 18/17
c ---[ 646]---> Adder-cost: 614   maxlim: 131070   bits: 18/17
c ---[ 645]---> Adder-cost: 746   maxlim: 131070   bits: 18/17
c ---[ 644]---> Adder-cost: 680   maxlim: 131070   bits: 18/17
c ---[ 643]---> Adder-cost: 752   maxlim: 131070   bits: 18/17
c ---[ 642]---> Adder-cost: 750   maxlim: 131070   bits: 18/17
c ---[ 641]---> Adder-cost: 752   maxlim: 131070   bits: 18/17
c ---[ 640]---> Adder-cost: 440   maxlim: 131070   bits: 18/17
c ---[ 639]---> Adder-cost: 748   maxlim: 131070   bits: 18/17
c ---[ 638]---> Adder-cost: 748   maxlim: 131070   bits: 18/17
c ---[ 637]---> Adder-cost: 462   maxlim: 65534   bits: 17/16
c ---[ 636]---> Adder-cost: 752   maxlim: 131070   bits: 18/17
c ---[ 635]---> Adder-cost: 750   maxlim: 131070   bits: 18/17
c ---[ 634]---> Adder-cost: 748   maxlim: 131070   bits: 18/17
c ---[ 633]---> Adder-cost: 738   maxlim: 131070   bits: 18/17
c ---[ 632]---> Adder-cost: 746   maxlim: 131070   bits: 18/17
c ---[ 631]---> Adder-cost: 752   maxlim: 131070   bits: 18/17
c ---[ 630]---> Adder-cost: 682   maxlim: 131070   bits: 18/17
c ---[ 629]---> Adder-cost: 752   maxlim: 131070   bits: 18/17
c ---[ 628]---> Adder-cost: 718   maxlim: 131070   bits: 18/17
c ---[ 627]---> Adder-cost: 752   maxlim: 131070   bits: 18/17
c ---[ 626]---> Adder-cost: 748   maxlim: 131070   bits: 18/17
c ---[ 625]---> Adder-cost: 750   maxlim: 131070   bits: 18/17
c ---[ 624]---> Adder-cost: 434   maxlim: 131070   bits: 18/17
c ---[ 623]---> Adder-cost: 750   maxlim: 131070   bits: 18/17
c ---[ 622]---> Adder-cost: 530   maxlim: 131070   bits: 18/17
c ---[ 621]---> Adder-cost: 752   maxlim: 131070   bits: 18/17
c ---[ 620]---> Adder-cost: 728   maxlim: 65534   bits: 17/16
c ---[ 619]---> Adder-cost: 752   maxlim: 131070   bits: 18/17
c ---[ 618]---> Adder-cost: 746   maxlim: 131070   bits: 18/17
c ---[ 617]---> Adder-cost: 746   maxlim: 131070   bits: 18/17
c ---[ 616]---> Adder-cost: 752   maxlim: 131070   bits: 18/17
c ---[ 615]---> Adder-cost: 749   maxlim: 131070   bits: 18/17
c ---[ 614]---> Adder-cost: 750   maxlim: 131070   bits: 18/17
c ---[ 613]---> Adder-cost: 750   maxlim: 131070   bits: 18/17
c ---[ 611]---> Adder-cost: 785   maxlim: 315391   bits: 20/19
c ---[ 609]---> Adder-cost: 785   maxlim: 327039   bits: 20/19
c ---[ 607]---> Adder-cost: 785   maxlim: 335999   bits: 20/19
c ---[ 605]---> Adder-cost: 785   maxlim: 331519   bits: 20/19
c ---[ 603]---> Adder-cost: 785   maxlim: 328703   bits: 20/19
c ---[ 601]---> Adder-cost: 785   maxlim: 329471   bits: 20/19
c ---[ 599]---> Adder-cost: 785   maxlim: 333823   bits: 20/19
c ---[ 597]---> Adder-cost: 785   maxlim: 326783   bits: 20/19
c ---[ 595]---> Adder-cost: 785   maxlim: 328959   bits: 20/19
c ---[ 593]---> Adder-cost: 785   maxlim: 322815   bits: 20/19
c ---[ 591]---> Adder-cost: 785   maxlim: 325247   bits: 20/19
c ---[ 589]---> Adder-cost: 785   maxlim: 328447   bits: 20/19
c ---[ 587]---> Adder-cost: 785   maxlim: 301439   bits: 20/19
c ---[ 585]---> Adder-cost: 785   maxlim: 327551   bits: 20/19
c ---[ 583]---> Adder-cost: 785   maxlim: 323455   bits: 20/19
c ---[ 581]---> Adder-cost: 785   maxlim: 314495   bits: 20/19
c ---[ 579]---> Adder-cost: 785   maxlim: 323967   bits: 20/19
c ---[ 577]---> Adder-cost: 785   maxlim: 322815   bits: 20/19
c ---[ 575]---> Adder-cost: 785   maxlim: 318591   bits: 20/19
c ---[ 573]---> Adder-cost: 785   maxlim: 331263   bits: 20/19
c ---[ 571]---> Adder-cost: 785   maxlim: 330367   bits: 20/19
c ---[ 569]---> Adder-cost: 785   maxlim: 314623   bits: 20/19
c ---[ 567]---> Adder-cost: 785   maxlim: 319231   bits: 20/19
c ---[ 565]---> Adder-cost: 785   maxlim: 323199   bits: 20/19
c ---[ 564]---> BDD-cost:   65
c ---[ 563]---> BDD-cost:   75
c ---[ 562]---> BDD-cost:   75
c ---[ 561]---> BDD-cost:   73
c ---[ 560]---> BDD-cost:   69
c ---[ 559]---> BDD-cost:   73
c ---[ 558]---> BDD-cost:   67
c ---[ 557]---> BDD-cost:   75
c ---[ 556]---> BDD-cost:   73
c ---[ 555]---> BDD-cost:   73
c ---[ 554]---> BDD-cost:   75
c ---[ 553]---> BDD-cost:   73
c ---[ 552]---> BDD-cost:   75
c ---[ 551]---> BDD-cost:   75
c ---[ 550]---> BDD-cost:   75
c ---[ 549]---> BDD-cost:   75
c ---[ 548]---> BDD-cost:   75
c ---[ 547]---> BDD-cost:   73
c ---[ 546]---> BDD-cost:   75
c ---[ 545]---> BDD-cost:   71
c ---[ 544]---> BDD-cost:   75
c ---[ 543]---> BDD-cost:   73
c ---[ 542]---> BDD-cost:   73
c ---[ 541]---> BDD-cost:   75
c ---[ 540]---> BDD-cost:   58
c ---[ 539]---> BDD-cost:   58
c ---[ 538]---> BDD-cost:   58
c ---[ 537]---> BDD-cost:   58
c ---[ 536]---> BDD-cost:   58
c ---[ 535]---> BDD-cost:   58
c ---[ 534]---> BDD-cost:   58
c ---[ 533]---> BDD-cost:   58
c ---[ 532]---> BDD-cost:   58
c ---[ 531]---> BDD-cost:   58
c ---[ 530]---> BDD-cost:   58
c ---[ 529]---> BDD-cost:   58
c ---[ 528]---> BDD-cost:   58
c ---[ 527]---> BDD-cost:   58
c ---[ 526]---> BDD-cost:   58
c ---[ 525]---> BDD-cost:   58
c ---[ 524]---> BDD-cost:   58
c ---[ 523]---> BDD-cost:   58
c ---[ 522]---> BDD-cost:   58
c ---[ 521]---> BDD-cost:   58
c ---[ 520]---> BDD-cost:   58
c ---[ 519]---> BDD-cost:   58
c ---[ 518]---> BDD-cost:   58
c ---[ 517]---> BDD-cost:   58
c ---[ 515]---> Sorter-cost:  937     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 514]---> Sorter-cost: 1154     Base: 2 2 2 2 2 2 2 2 2 2 2 2 3 5 3
c ---[ 513]---> Sorter-cost: 1375     Base: 2 2 2 2 2 2 2 2 2 2 2 2 7 2 3
c ---[ 512]---> Sorter-cost:  736     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 511]---> Sorter-cost: 1181     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 5
c ---[ 510]---> Sorter-cost:  812     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 5
c ---[ 509]---> Sorter-cost:  785     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 508]---> Sorter-cost: 1353     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 7 3
c ---[ 507]---> Sorter-cost: 1217     Base: 2 2 2 2 2 2 2 2 2 2 2 2 7 5
c ---[ 506]---> Sorter-cost: 1031     Base: 2 2 2 2 2 2 2 2 2 2 2 3 5 2 2
c ---[ 505]---> Sorter-cost: 1056     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 7 3
c ---[ 503]---> Sorter-cost:  893     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 502]---> Sorter-cost: 1239     Base: 2 2 2 2 2 2 2 2 2 2 2 2 7 5
c ---[ 500]---> Sorter-cost: 1177     Base: 2 2 2 2 2 2 2 2 2 2 2 2 7 5
c ---[ 499]---> Sorter-cost: 1453     Base: 2 2 2 2 2 2 2 2 2 2 2 2 13 3
c ---[ 498]---> Sorter-cost: 1287     Base: 2 2 2 2 2 2 2 2 2 2 2 7 3 3
c ---[ 497]---> Sorter-cost: 1187     Base: 2 2 2 2 2 2 2 2 2 3 3 7 5
c ---[ 496]---> Sorter-cost: 1356     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 7 3
c ---[ 494]---> Sorter-cost:  801     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 493]---> Sorter-cost:  926     Base: 2 2 2 2 2 2 2 2 2 2 2 2 5 3 2
c ---[ 492]---> BDD-cost:   22
c ---[ 491]---> BDD-cost:   25
c ---[ 490]---> BDD-cost:   25
c ---[ 489]---> BDD-cost:   27
c ---[ 488]---> BDD-cost:   27
c ---[ 487]---> BDD-cost:   26
c ---[ 486]---> BDD-cost:   26
c ---[ 485]---> BDD-cost:   25
c ---[ 484]---> BDD-cost:   26
c ---[ 483]---> BDD-cost:   25
c ---[ 482]---> BDD-cost:   24
c ---[ 481]---> BDD-cost:   24
c ---[ 480]---> BDD-cost:   24
c ---[ 479]---> BDD-cost:   24
c ---[ 478]---> BDD-cost:   25
c ---[ 477]---> BDD-cost:   25
c ---[ 476]---> BDD-cost:   26
c ---[ 475]---> BDD-cost:   23
c ---[ 474]---> BDD-cost:   23
c ---[ 473]---> BDD-cost:   20
c ---[ 472]---> BDD-cost:   20
c ---[ 471]---> BDD-cost:   20
c ---[ 470]---> BDD-cost:   20
c ---[ 469]---> BDD-cost:   26
c ---[ 468]---> BDD-cost:   24
c ---[ 467]---> BDD-cost:   21
c ---[ 466]---> BDD-cost:   21
c ---[ 465]---> BDD-cost:   25
c ---[ 464]---> BDD-cost:   25
c ---[ 463]---> BDD-cost:   25
c ---[ 462]---> BDD-cost:   25
c ---[ 461]---> BDD-cost:   24
c ---[ 460]---> BDD-cost:   22
c ---[ 459]---> BDD-cost:   23
c ---[ 458]---> BDD-cost:   25
c ---[ 457]---> BDD-cost:   23
c ---[ 456]---> BDD-cost:   23
c ---[ 455]---> BDD-cost:   23
c ---[ 454]---> BDD-cost:   25
c ---[ 453]---> BDD-cost:   25
c ---[ 452]---> BDD-cost:   25
c ---[ 451]---> BDD-cost:   23
c ---[ 450]---> BDD-cost:   25
c ---[ 449]---> BDD-cost:   25
c ---[ 448]---> BDD-cost:   25
c ---[ 447]---> BDD-cost:   23
c ---[ 446]---> BDD-cost:   24
c ---[ 445]---> BDD-cost:   24
c ---[ 444]---> BDD-cost:   24
c ---[ 443]---> BDD-cost:   23
c ---[ 442]---> BDD-cost:   26
c ---[ 441]---> BDD-cost:   25
c ---[ 440]---> BDD-cost:   23
c ---[ 439]---> BDD-cost:   24
c ---[ 438]---> Sorter-cost:  795     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 437]---> Sorter-cost:  699     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 436]---> Sorter-cost:  747     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 435]---> Sorter-cost:  686     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 434]---> Sorter-cost:  693     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 433]---> Sorter-cost:  684     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 432]---> Sorter-cost:  776     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 431]---> Sorter-cost:  748     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 430]---> Sorter-cost:  753     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 429]---> Sorter-cost:  776     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 428]---> Sorter-cost:  767     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 427]---> Sorter-cost:  677     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 426]---> Sorter-cost:  785     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 425]---> Sorter-cost:  776     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 424]---> Sorter-cost:  520     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 423]---> Sorter-cost:  520     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 422]---> Sorter-cost:  520     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 421]---> Sorter-cost:  520     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 420]---> Sorter-cost:  520     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 419]---> Sorter-cost:  520     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 418]---> Sorter-cost:  520     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 417]---> Sorter-cost:  520     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 416]---> Sorter-cost:  520     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 415]---> Sorter-cost:  520     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 414]---> Sorter-cost:  520     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 383]---> Sorter-cost:  647     Base: 2 2 2 2 2 2 2 2 2 2 2 2 7 7
c ---[ 382]---> Adder-cost: 719   maxlim: 131070   bits: 18/17
c ---[ 381]---> Adder-cost: 510   maxlim: 131070   bits: 18/17
c ---[ 380]---> Adder-cost: 650   maxlim: 131070   bits: 18/17
c ---[ 379]---> Adder-cost: 541   maxlim: 131070   bits: 18/17
c ---[ 378]---> Adder-cost: 685   maxlim: 131070   bits: 18/17
c ---[ 377]---> Adder-cost: 609   maxlim: 131070   bits: 18/17
c ---[ 376]---> Adder-cost: 512   maxlim: 131070   bits: 18/17
c ---[ 375]---> Adder-cost: 544   maxlim: 131070   bits: 18/17
c ---[ 373]---> Adder-cost: 546   maxlim: 131070   bits: 18/17
c ---[ 372]---> Adder-cost: 511   maxlim: 131070   bits: 18/17
c ---[ 371]---> Adder-cost: 512   maxlim: 131070   bits: 18/17
c ---[ 370]---> Adder-cost: 664   maxlim: 131070   bits: 18/17
c ---[ 369]---> Adder-cost: 615   maxlim: 131070   bits: 18/17
c ---[ 368]---> Adder-cost: 510   maxlim: 131070   bits: 18/17
c ---[ 367]---> Adder-cost: 648   maxlim: 131070   bits: 18/17
c ---[ 366]---> Adder-cost: 506   maxlim: 131070   bits: 18/17
c ---[ 365]---> Adder-cost: 513   maxlim: 131070   bits: 18/17
c ---[ 364]---> Adder-cost: 547   maxlim: 131070   bits: 18/17
c ---[ 363]---> Adder-cost: 546   maxlim: 131070   bits: 18/17
c ---[ 362]---> Adder-cost: 473   maxlim: 131070   bits: 18/17
c ---[ 361]---> Adder-cost: 541   maxlim: 131070   bits: 18/17
c ---[ 360]---> Adder-cost: 510   maxlim: 131070   bits: 18/17
c ---[ 356]---> Adder-cost: 550   maxlim: 131070   bits: 18/17
c ---[ 355]---> Adder-cost: 513   maxlim: 131070   bits: 18/17
c ---[ 354]---> Adder-cost: 509   maxlim: 131070   bits: 18/17
c ---[ 353]---> Adder-cost: 465   maxlim: 131070   bits: 18/17
c ---[ 352]---> Adder-cost: 547   maxlim: 131070   bits: 18/17
c ---[ 351]---> Adder-cost: 548   maxlim: 131070   bits: 18/17
c ---[ 350]---> Adder-cost: 540   maxlim: 131070   bits: 18/17
c ---[ 349]---> Adder-cost: 650   maxlim: 131070   bits: 18/17
c ---[ 348]---> Adder-cost: 611   maxlim: 131070   bits: 18/17
c ---[ 347]---> Adder-cost: 511   maxlim: 131070   bits: 18/17
c ---[ 345]---> Adder-cost: 550   maxlim: 131070   bits: 18/17
c ---[ 342]---> Adder-cost: 648   maxlim: 131070   bits: 18/17
c ---[ 341]---> Adder-cost: 499   maxlim: 131070   bits: 18/17
c ---[ 340]---> Adder-cost: 510   maxlim: 131070   bits: 18/17
c ---[ 339]---> Adder-cost: 511   maxlim: 131070   bits: 18/17
c ---[ 338]---> Adder-cost: 529   maxlim: 131070   bits: 18/17
c ---[ 337]---> Adder-cost: 511   maxlim: 131070   bits: 18/17
c ---[ 336]---> Adder-cost: 544   maxlim: 131070   bits: 18/17
c ---[ 335]---> Adder-cost: 546   maxlim: 131070   bits: 18/17
c ---[ 334]---> Adder-cost: 630   maxlim: 131070   bits: 18/17
c ---[ 333]---> Adder-cost: 506   maxlim: 131070   bits: 18/17
c ---[ 332]---> Adder-cost: 510   maxlim: 131070   bits: 18/17
c ---[ 331]---> Adder-cost: 541   maxlim: 131070   bits: 18/17
c ---[ 330]---> Adder-cost: 533   maxlim: 131070   bits: 18/17
c ---[ 329]---> Adder-cost: 616   maxlim: 131070   bits: 18/17
c ---[ 328]---> Adder-cost: 548   maxlim: 131070   bits: 18/17
c ---[ 327]---> Adder-cost: 475   maxlim: 131070   bits: 18/17
c ---[ 326]---> Adder-cost: 511   maxlim: 131070   bits: 18/17
c ---[ 325]---> Adder-cost: 511   maxlim: 131070   bits: 18/17
c ---[ 324]---> Adder-cost: 508   maxlim: 131070   bits: 18/17
c ---[ 323]---> Adder-cost: 547   maxlim: 131070   bits: 18/17
c ---[ 322]---> Adder-cost: 518   maxlim: 131070   bits: 18/17
c ---[ 321]---> Adder-cost: 546   maxlim: 131070   bits: 18/17
c ---[ 318]---> Adder-cost: 513   maxlim: 131070   bits: 18/17
c ---[ 316]---> Adder-cost: 524   maxlim: 131070   bits: 18/17
c ---[ 314]---> Adder-cost: 509   maxlim: 131070   bits: 18/17
c ---[ 313]---> Adder-cost: 512   maxlim: 131070   bits: 18/17
c ---[ 312]---> Adder-cost: 546   maxlim: 131070   bits: 18/17
c ---[ 311]---> Adder-cost: 529   maxlim: 131070   bits: 18/17
c ---[ 310]---> Adder-cost: 575   maxlim: 131070   bits: 18/17
c ---[ 309]---> Adder-cost: 515   maxlim: 131070   bits: 18/17
c ---[ 308]---> Adder-cost: 489   maxlim: 131070   bits: 18/17
c ---[ 307]---> Adder-cost: 515   maxlim: 131070   bits: 18/17
c ---[ 306]---> Adder-cost: 506   maxlim: 131070   bits: 18/17
c ---[ 305]---> Adder-cost: 508   maxlim: 131070   bits: 18/17
c ---[ 304]---> Adder-cost: 580   maxlim: 131070   bits: 18/17
c ---[ 302]---> Adder-cost: 511   maxlim: 131070   bits: 18/17
c ---[ 301]---> Adder-cost: 548   maxlim: 131070   bits: 18/17
c ---[ 300]---> Adder-cost: 504   maxlim: 131070   bits: 18/17
c ---[ 299]---> Adder-cost: 609   maxlim: 131070   bits: 18/17
c ---[ 298]---> Adder-cost: 509   maxlim: 131070   bits: 18/17
c ---[ 296]---> Adder-cost: 508   maxlim: 131070   bits: 18/17
c ---[ 293]---> Adder-cost: 542   maxlim: 131070   bits: 18/17
c ---[ 292]---> Adder-cost: 577   maxlim: 131070   bits: 18/17
c ---[ 291]---> Adder-cost: 566   maxlim: 131070   bits: 18/17
c ---[ 290]---> Adder-cost: 546   maxlim: 131070   bits: 18/17
c ---[ 289]---> Adder-cost: 513   maxlim: 131070   bits: 18/17
c ---[ 286]---> Adder-cost: 503   maxlim: 131070   bits: 18/17
c ---[ 285]---> Adder-cost: 547   maxlim: 131070   bits: 18/17
c ---[ 284]---> Adder-cost: 472   maxlim: 131070   bits: 18/17
c ---[ 283]---> Adder-cost: 510   maxlim: 131070   bits: 18/17
c ---[ 282]---> Adder-cost: 464   maxlim: 131070   bits: 18/17
c ---[ 281]---> Adder-cost: 509   maxlim: 131070   bits: 18/17
c ---[ 280]---> Adder-cost: 511   maxlim: 131070   bits: 18/17
c ---[ 279]---> Adder-cost: 503   maxlim: 131070   bits: 18/17
c ---[ 277]---> Adder-cost: 540   maxlim: 131070   bits: 18/17
c ---[ 276]---> Adder-cost: 510   maxlim: 131070   bits: 18/17
c ---[ 275]---> Adder-cost: 489   maxlim: 131070   bits: 18/17
c ---[ 274]---> Adder-cost: 515   maxlim: 131070   bits: 18/17
c ---[ 273]---> Adder-cost: 512   maxlim: 131070   bits: 18/17
c ---[ 271]---> Adder-cost: 509   maxlim: 131070   bits: 18/17
c ---[ 270]---> Adder-cost: 506   maxlim: 131070   bits: 18/17
c ---[ 269]---> Adder-cost: 512   maxlim: 131070   bits: 18/17
c ---[ 268]---> Adder-cost: 515   maxlim: 131070   bits: 18/17
c ---[ 267]---> Adder-cost: 515   maxlim: 131070   bits: 18/17
c ---[ 266]---> Adder-cost: 495   maxlim: 131070   bits: 18/17
c ---[ 264]---> Adder-cost: 514   maxlim: 131070   bits: 18/17
c ---[ 263]---> Adder-cost: 508   maxlim: 131070   bits: 18/17
c ---[ 262]---> Adder-cost: 507   maxlim: 131070   bits: 18/17
c ---[ 261]---> Adder-cost: 506   maxlim: 131070   bits: 18/17
c ---[ 260]---> Adder-cost: 545   maxlim: 131070   bits: 18/17
c ---[ 259]---> Adder-cost: 510   maxlim: 131070   bits: 18/17
c ---[ 258]---> Adder-cost: 510   maxlim: 131070   bits: 18/17
c ---[ 257]---> Adder-cost: 508   maxlim: 131070   bits: 18/17
c ---[ 256]---> Adder-cost: 609   maxlim: 131070   bits: 18/17
c ---[ 255]---> Adder-cost: 545   maxlim: 131070   bits: 18/17
c ---[ 254]---> Adder-cost: 511   maxlim: 131070   bits: 18/17
c ---[ 253]---> Adder-cost: 476   maxlim: 131070   bits: 18/17
c ---[ 252]---> Adder-cost: 510   maxlim: 131070   bits: 18/17
c ---[ 251]---> Adder-cost: 485   maxlim: 131070   bits: 18/17
c ---[ 250]---> Adder-cost: 509   maxlim: 131070   bits: 18/17
c ---[ 249]---> Adder-cost: 492   maxlim: 131070   bits: 18/17
c ---[ 248]---> Adder-cost: 508   maxlim: 131070   bits: 18/17
c ---[ 247]---> Adder-cost: 541   maxlim: 131070   bits: 18/17
c ---[ 245]---> Adder-cost: 502   maxlim: 131070   bits: 18/17
c ---[ 244]---> Adder-cost: 515   maxlim: 131070   bits: 18/17
c ---[ 243]---> Adder-cost: 514   maxlim: 131070   bits: 18/17
c ---[ 242]---> Adder-cost: 509   maxlim: 131070   bits: 18/17
c ---[ 241]---> Adder-cost: 513   maxlim: 131070   bits: 18/17
c ---[ 240]---> Adder-cost: 508   maxlim: 131070   bits: 18/17
c ---[ 239]---> Adder-cost: 477   maxlim: 131070   bits: 18/17
c ---[ 238]---> Adder-cost: 541   maxlim: 131070   bits: 18/17
c ---[ 237]---> Adder-cost: 511   maxlim: 131070   bits: 18/17
c ---[ 236]---> Adder-cost: 515   maxlim: 131070   bits: 18/17
c ---[ 235]---> Adder-cost: 505   maxlim: 131070   bits: 18/17
c ---[ 234]---> Adder-cost: 514   maxlim: 131070   bits: 18/17
c ---[ 233]---> Adder-cost: 464   maxlim: 131070   bits: 18/17
c ---[ 232]---> Adder-cost: 515   maxlim: 131070   bits: 18/17
c ---[ 231]---> Adder-cost: 513   maxlim: 131070   bits: 18/17
c ---[ 230]---> Adder-cost: 510   maxlim: 131070   bits: 18/17
c ---[ 229]---> Adder-cost: 509   maxlim: 131070   bits: 18/17
c ---[ 228]---> Adder-cost: 475   maxlim: 131070   bits: 18/17
c ---[ 227]---> Adder-cost: 513   maxlim: 131070   bits: 18/17
c ---[ 226]---> Adder-cost: 495   maxlim: 131070   bits: 18/17
c ---[ 225]---> Adder-cost: 512   maxlim: 131070   bits: 18/17
c ---[ 224]---> Adder-cost: 510   maxlim: 131070   bits: 18/17
c ---[ 222]---> Adder-cost: 506   maxlim: 131070   bits: 18/17
c ---[ 221]---> Adder-cost: 1050   maxlim: 2621419   bits: 23/22
c ---[ 220]---> Adder-cost: 1028   maxlim: 2621419   bits: 23/22
c ---[ 219]---> Adder-cost: 1148   maxlim: 2490348   bits: 23/22
c ---[ 218]---> Adder-cost: 1454   maxlim: 2621419   bits: 23/22
c ---[ 217]---> Adder-cost: 1054   maxlim: 2752490   bits: 23/22
c ---[ 216]---> Adder-cost: 1210   maxlim: 2490348   bits: 23/22
c ---[ 215]---> Adder-cost: 1146   maxlim: 2621419   bits: 23/22
c ---[ 214]---> Adder-cost: 1142   maxlim: 2555883   bits: 23/22
c ---[ 213]---> Adder-cost: 1323   maxlim: 2752490   bits: 23/22
c ---[ 212]---> Adder-cost: 1382   maxlim: 2228206   bits: 23/22
c ---[ 211]---> Adder-cost: 1202   maxlim: 2490348   bits: 23/22
c ---[ 210]---> Adder-cost: 998   maxlim: 2621419   bits: 23/22
c ---[ 209]---> Adder-cost: 1128   maxlim: 2490348   bits: 23/22
c ---[ 208]---> Adder-cost: 1185   maxlim: 2621419   bits: 23/22
c ---[ 207]---> Adder-cost: 1464   maxlim: 2752490   bits: 23/22
c ---[ 206]---> Adder-cost: 1092   maxlim: 2621419   bits: 23/22
c ---[ 205]---> Adder-cost: 1208   maxlim: 2752490   bits: 23/22
c ---[ 204]---> Adder-cost: 1030   maxlim: 2359277   bits: 23/22
c ---[ 203]---> Adder-cost: 1035   maxlim: 2490348   bits: 23/22
c ---[ 202]---> Adder-cost: 1216   maxlim: 2490348   bits: 23/22
c ---[ 201]---> Adder-cost: 1207   maxlim: 2359277   bits: 23/22
c ---[ 200]---> Adder-cost: 1118   maxlim: 2490348   bits: 23/22
c ---[ 199]---> Adder-cost: 1092   maxlim: 2621419   bits: 23/22
c ---[ 198]---> Adder-cost: 1302   maxlim: 2752490   bits: 23/22
c ---[ 197]---> Adder-cost: 1294   maxlim: 2293741   bits: 23/22
c ---[ 196]---> Adder-cost: 997   maxlim: 2424812   bits: 23/22
c ---[ 195]---> Adder-cost: 870   maxlim: 2621419   bits: 23/22
c ---[ 194]---> Adder-cost: 1034   maxlim: 2490348   bits: 23/22
c ---[ 193]---> Adder-cost: 1212   maxlim: 2162670   bits: 23/22
c ---[ 192]---> Adder-cost: 1374   maxlim: 2621419   bits: 23/22
c ---[ 191]---> Adder-cost: 1068   maxlim: 2359277   bits: 23/22
c ---[ 190]---> Adder-cost: 988   maxlim: 2621419   bits: 23/22
c ---[ 189]---> Adder-cost: 1004   maxlim: 2621419   bits: 23/22
c ---[ 188]---> Adder-cost: 1002   maxlim: 2621419   bits: 23/22
c ---[ 187]---> Adder-cost: 1180   maxlim: 2490348   bits: 23/22
c ---[ 186]---> Adder-cost: 1246   maxlim: 2490348   bits: 23/22
c ---[ 185]---> Adder-cost: 1456   maxlim: 2752490   bits: 23/22
c ---[ 184]---> Adder-cost: 1054   maxlim: 2228206   bits: 23/22
c ---[ 183]---> Adder-cost: 1306   maxlim: 2752490   bits: 23/22
c ---[ 182]---> Adder-cost: 1184   maxlim: 2752490   bits: 23/22
c ---[ 181]---> Adder-cost: 1066   maxlim: 2490348   bits: 23/22
c ---[ 180]---> Adder-cost: 1074   maxlim: 2555883   bits: 23/22
c ---[ 179]---> Adder-cost: 1312   maxlim: 2621419   bits: 23/22
c ---[ 178]---> Adder-cost: 1046   maxlim: 2228206   bits: 23/22
c ---[ 177]---> Adder-cost: 1272   maxlim: 2621419   bits: 23/22
c ---[ 176]---> Adder-cost: 1123   maxlim: 2031599   bits: 22/21
c ---[ 175]---> Adder-cost: 1276   maxlim: 2293741   bits: 23/22
c ---[ 174]---> Adder-cost: 1452   maxlim: 2752490   bits: 23/22
c ---[ 173]---> Adder-cost: 1021   maxlim: 2490348   bits: 23/22
c ---[ 172]---> Adder-cost: 1420   maxlim: 2752490   bits: 23/22
c ---[ 171]---> Adder-cost: 1142   maxlim: 2621419   bits: 23/22
c ---[ 170]---> Adder-cost: 1364   maxlim: 2359277   bits: 23/22
c ---[ 169]---> Adder-cost: 1301   maxlim: 2621419   bits: 23/22
c ---[ 168]---> Adder-cost: 1349   maxlim: 2621419   bits: 23/22
c ---[ 167]---> Adder-cost: 1338   maxlim: 2228206   bits: 23/22
c ---[ 166]---> Adder-cost: 1440   maxlim: 2752490   bits: 23/22
c ---[ 165]---> Adder-cost: 1044   maxlim: 2359277   bits: 23/22
c ---[ 164]---> Adder-cost: 1418   maxlim: 2621419   bits: 23/22
c ---[ 163]---> Adder-cost: 1050   maxlim: 2490348   bits: 23/22
c ---[ 162]---> Adder-cost: 1158   maxlim: 2752490   bits: 23/22
c ---[ 161]---> Adder-cost: 1042   maxlim: 2621419   bits: 23/22
c ---[ 160]---> Adder-cost: 1212   maxlim: 2359277   bits: 23/22
c ---[ 159]---> Adder-cost: 1306   maxlim: 2621419   bits: 23/22
c ---[ 158]---> Adder-cost: 1148   maxlim: 2359277   bits: 23/22
c ---[ 157]---> Adder-cost: 1327   maxlim: 2621419   bits: 23/22
c ---[ 156]---> Adder-cost: 1120   maxlim: 2621419   bits: 23/22
c ---[ 155]---> Adder-cost: 1356   maxlim: 2424812   bits: 23/22
c ---[ 154]---> Adder-cost: 1186   maxlim: 2621419   bits: 23/22
c ---[ 153]---> Adder-cost: 1182   maxlim: 2752490   bits: 23/22
c ---[ 152]---> Adder-cost: 1193   maxlim: 2752490   bits: 23/22
c ---[ 151]---> Adder-cost: 1396   maxlim: 2752490   bits: 23/22
c ---[ 150]---> Adder-cost: 1271   maxlim: 2162670   bits: 23/22
c ---[ 149]---> Adder-cost: 1316   maxlim: 2621419   bits: 23/22
c ---[ 148]---> Adder-cost: 1082   maxlim: 2621419   bits: 23/22
c ---[ 147]---> Adder-cost: 1074   maxlim: 2424812   bits: 23/22
c ---[ 146]---> Adder-cost: 1147   maxlim: 2621419   bits: 23/22
c ---[ 145]---> Adder-cost: 960   maxlim: 2555883   bits: 23/22
c ---[ 144]---> Adder-cost: 1176   maxlim: 2490348   bits: 23/22
c ---[ 143]---> Adder-cost: 1500   maxlim: 2686954   bits: 23/22
c ---[ 142]---> Adder-cost: 1161   maxlim: 2621419   bits: 23/22
c ---[ 141]---> Adder-cost: 1250   maxlim: 2162670   bits: 23/22
c ---[ 140]---> Adder-cost: 1472   maxlim: 2752490   bits: 23/22
c ---[ 139]---> Adder-cost: 1086   maxlim: 2490348   bits: 23/22
c ---[ 138]---> Adder-cost: 1068   maxlim: 2621419   bits: 23/22
c ---[ 137]---> Adder-cost: 1424   maxlim: 2752490   bits: 23/22
c ---[ 136]---> Adder-cost: 1136   maxlim: 2359277   bits: 23/22
c ---[ 135]---> Adder-cost: 908   maxlim: 2621419   bits: 23/22
c ---[ 134]---> Adder-cost: 1214   maxlim: 2490348   bits: 23/22
c ---[ 133]---> Adder-cost: 1082   maxlim: 2293741   bits: 23/22
c ---[ 132]---> Adder-cost: 1096   maxlim: 2621419   bits: 23/22
c ---[ 131]---> Adder-cost: 1162   maxlim: 2621419   bits: 23/22
c ---[ 130]---> Adder-cost: 1410   maxlim: 2752490   bits: 23/22
c ---[ 129]---> Adder-cost: 1092   maxlim: 2752490   bits: 23/22
c ---[ 128]---> Adder-cost: 1342   maxlim: 2228206   bits: 23/22
c ---[ 127]---> Adder-cost: 1066   maxlim: 2490348   bits: 23/22
c ---[ 126]---> Adder-cost: 1050   maxlim: 2359277   bits: 23/22
c ---[ 125]---> Adder-cost: 1256   maxlim: 2392044   bits: 23/22
c ---[ 124]---> Adder-cost: 1215   maxlim: 2424812   bits: 23/22
c ---[ 123]---> Adder-cost: 1164   maxlim: 2621419   bits: 23/22
c ---[ 122]---> Adder-cost: 1277   maxlim: 2129902   bits: 23/22
c ---[ 121]---> Adder-cost: 994   maxlim: 2523115   bits: 23/22
c ---[ 120]---> Adder-cost: 1340   maxlim: 2228206   bits: 23/22
c ---[ 119]---> Adder-cost: 1052   maxlim: 2555883   bits: 23/22
c ---[ 118]---> Adder-cost: 1080   maxlim: 2490348   bits: 23/22
c ---[ 117]---> Adder-cost: 886   maxlim: 2621419   bits: 23/22
c ---[ 116]---> Adder-cost: 1208   maxlim: 2293741   bits: 23/22
c ---[ 115]---> Adder-cost: 1424   maxlim: 2490348   bits: 23/22
c ---[ 114]---> Adder-cost: 1319   maxlim: 2752490   bits: 23/22
c ---[ 113]---> Adder-cost: 1385   maxlim: 2490348   bits: 23/22
c ---[ 112]---> Adder-cost: 1084   maxlim: 2490348   bits: 23/22
c ---[ 111]---> Adder-cost: 1075   maxlim: 2555883   bits: 23/22
c ---[ 110]---> Adder-cost: 1288   maxlim: 2621419   bits: 23/22
c ---[ 109]---> Adder-cost: 1110   maxlim: 2228206   bits: 23/22
c ---[ 108]---> Adder-cost: 1328   maxlim: 2621419   bits: 23/22
c ---[ 107]---> Adder-cost: 1418   maxlim: 2490348   bits: 23/22
c ---[ 106]---> Adder-cost: 1060   maxlim: 2621419   bits: 23/22
c ---[ 105]---> Adder-cost: 1412   maxlim: 2752490   bits: 23/22
c ---[ 104]---> Adder-cost: 1168   maxlim: 2359277   bits: 23/22
c ---[ 103]---> Adder-cost: 1397   maxlim: 2621419   bits: 23/22
c ---[ 102]---> Adder-cost: 1190   maxlim: 2228205   bits: 23/22
c ---[ 101]---> Adder-cost: 1224   maxlim: 2621419   bits: 23/22
c ---[ 100]---> Adder-cost: 1066   maxlim: 2490348   bits: 23/22
c ---[  99]---> Adder-cost: 1230   maxlim: 2621419   bits: 23/22
c ---[  98]---> Adder-cost: 1075   maxlim: 2424812   bits: 23/22
c ---[  97]---> Adder-cost: 1388   maxlim: 2621419   bits: 23/22
c ---[  96]---> Adder-cost: 1081   maxlim: 2359277   bits: 23/22
c ---[  95]---> Adder-cost: 1438   maxlim: 2621419   bits: 23/22
c ---[  94]---> Adder-cost: 1486   maxlim: 2752490   bits: 23/22
c ---[  93]---> Adder-cost: 1382   maxlim: 2228206   bits: 23/22
c ---[  92]---> Adder-cost: 1096   maxlim: 2424812   bits: 23/22
c ---[  91]---> Adder-cost: 1431   maxlim: 2555883   bits: 23/22
c ---[  90]---> Adder-cost: 1438   maxlim: 2752490   bits: 23/22
c ---[  89]---> Adder-cost: 1080   maxlim: 2359277   bits: 23/22
c ---[  88]---> Adder-cost: 1163   maxlim: 2621419   bits: 23/22
c ---[  87]---> Adder-cost: 1034   maxlim: 2228206   bits: 23/22
c ---[  86]---> Adder-cost: 1325   maxlim: 2621419   bits: 23/22
c ---[  85]---> Adder-cost: 1465   maxlim: 2752490   bits: 23/22
c ---[  84]---> Adder-cost: 1080   maxlim: 2621419   bits: 23/22
c ---[  83]---> Adder-cost: 1286   maxlim: 2228206   bits: 23/22
c ---[  82]---> Adder-cost: 1196   maxlim: 2752490   bits: 23/22
c ---[  81]---> Adder-cost: 1020   maxlim: 2490348   bits: 23/22
c ---[  80]---> Adder-cost: 1416   maxlim: 2490348   bits: 23/22
c ---[  79]---> Adder-cost: 1312   maxlim: 2490348   bits: 23/22
c ---[  78]---> Adder-cost: 1178   maxlim: 2359277   bits: 23/22
c ---[  77]---> Adder-cost: 1155   maxlim: 2621419   bits: 23/22
c ---[  76]---> Adder-cost: 1066   maxlim: 2228206   bits: 23/22
c ---[  75]---> Adder-cost: 1072   maxlim: 2490348   bits: 23/22
c ---[  74]---> Adder-cost: 994   maxlim: 2424812   bits: 23/22
c ---[  73]---> Adder-cost: 1321   maxlim: 2490348   bits: 23/22
c ---[  72]---> Adder-cost: 1078   maxlim: 2359277   bits: 23/22
c ---[  71]---> Adder-cost: 1096   maxlim: 2490348   bits: 23/22
c ---[  70]---> Adder-cost: 1180   maxlim: 2359277   bits: 23/22
c ---[  69]---> Adder-cost: 1167   maxlim: 2621419   bits: 23/22
c ---[  68]---> Adder-cost: 1376   maxlim: 2621419   bits: 23/22
c ---[  67]---> Adder-cost: 1082   maxlim: 2490348   bits: 23/22
c ---[  66]---> Adder-cost: 1034   maxlim: 2490348   bits: 23/22
c ---[  65]---> Adder-cost: 1220   maxlim: 2752490   bits: 23/22
c ---[  64]---> Adder-cost: 1350   maxlim: 2490348   bits: 23/22
c ---[  63]---> Adder-cost: 1138   maxlim: 2621419   bits: 23/22
c ---[  62]---> Adder-cost: 1142   maxlim: 2359277   bits: 23/22
c ---[  61]---> Adder-cost: 1380   maxlim: 2621419   bits: 23/22
c ---[  60]---> Adder-cost: 1390   maxlim: 2621419   bits: 23/22
c ---[  59]---> Adder-cost: 1340   maxlim: 2228206   bits: 23/22
c ---[  58]---> Adder-cost: 1026   maxlim: 2490348   bits: 23/22
c ---[  57]---> Adder-cost: 1090   maxlim: 2490348   bits: 23/22
c ---[  56]---> Adder-cost: 1232   maxlim: 2621419   bits: 23/22
c ---[  55]---> Adder-cost: 1400   maxlim: 2752490   bits: 23/22
c ---[  54]---> Adder-cost: 1316   maxlim: 2228206   bits: 23/22
c ---[  53]---> Adder-cost: 1403   maxlim: 2752490   bits: 23/22
c ---[  52]---> Adder-cost: 878   maxlim: 2621419   bits: 23/22
c ---[  51]---> Adder-cost: 1402   maxlim: 2621419   bits: 23/22
c ---[  50]---> Adder-cost: 1486   maxlim: 2752490   bits: 23/22
c ---[  49]---> Adder-cost: 1117   maxlim: 2228206   bits: 23/22
c ---[  48]---> Adder-cost: 1100   maxlim: 2621419   bits: 23/22
c ---[  47]---> Adder-cost: 1082   maxlim: 2359277   bits: 23/22
c ---[  46]---> Adder-cost: 1126   maxlim: 2162670   bits: 23/22
c ---[  45]---> Adder-cost: 1369   maxlim: 2621419   bits: 23/22
c ---[  44]---> Adder-cost: 1054   maxlim: 2490348   bits: 23/22
c ---[  43]---> Adder-cost: 1342   maxlim: 2621419   bits: 23/22
c ---[  42]---> Adder-cost: 1254   maxlim: 2752490   bits: 23/22
c ---[  41]---> Adder-cost: 1412   maxlim: 2359277   bits: 23/22
c ---[  40]---> Sorter-cost:  932     Base: 2 2 2 2 2 2 2 2 2 5 3 2 2 2
c ---[  39]---> Sorter-cost:  698     Base: 2 2 2 2 2 2 2 2 2 2 2 2 7
c ---[  38]---> Sorter-cost:  663     Base: 2 2 2 2 2 2 2 2 2 2 2 2 3 5
c ---[  37]---> Sorter-cost:  572     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 7
c ---[  36]---> BDD-cost:    2
c ---[  35]---> BDD-cost:    5
c ---[  34]---> BDD-cost:    3
c ---[  33]---> BDD-cost:    6
c ---[  32]---> BDD-cost:    6
c ---[  31]---> BDD-cost:    6
c ---[  30]---> BDD-cost:    6
c ---[  29]---> BDD-cost:    6
c ---[  28]---> BDD-cost:    4
c ---[  27]---> BDD-cost:    4
c ---[  26]---> BDD-cost:    4
c ---[  25]---> BDD-cost:    2
c ---[  24]---> BDD-cost:    4
c ---[  23]---> BDD-cost:    6
c ---[  22]---> BDD-cost:    5
c ---[  21]---> Adder-cost: 478   maxlim: 65534   bits: 17/16
c ---[  20]---> Adder-cost: 368   maxlim: 65534   bits: 17/16
c ---[  19]---> Adder-cost: 668   maxlim: 65534   bits: 17/16
c ---[  18]---> Adder-cost: 508   maxlim: 65534   bits: 17/16
c ---[  17]---> Adder-cost: 642   maxlim: 65534   bits: 17/16
c ---[  16]---> Adder-cost: 544   maxlim: 65534   bits: 17/16
c ---[  15]---> Adder-cost: 432   maxlim: 65534   bits: 17/16
c ---[  14]---> Adder-cost: 420   maxlim: 65534   bits: 17/16
c ---[  13]---> Adder-cost: 450   maxlim: 65534   bits: 17/16
c ---[  12]---> Adder-cost: 414   maxlim: 65534   bits: 17/16
c ---[  11]-#### END SOLVER DATA ####
#### BEGIN WATCHER DATA ####
Enforcing CPU limit (will send SIGTERM then SIGKILL): 1200 seconds
Enforcing CPUTime (will send SIGXCPU) limit: 1230 seconds
Enforcing VSIZE limit: 943718400 bytes
Raw data (loadavg): 1.03 0.97 0.92 2/54 28249
Raw data (stat): 28249 (runsolver) R 28248 28099 28098 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 541796878 1052672 99 4294967295 134512640 135381576 3221224432 3221219676 135158418 0 2147483391 7 90112 0 0 0 17 0 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+9.99994 s]
Raw data (loadavg): 1.02 0.97 0.92 2/54 28249
Raw data (stat): 28249 (minisat+) R 28248 28099 28098 0 -1 0 26178 0 0 0 920 79 0 0 25 0 1 0 541796878 121028608 21902 4294967295 134512640 134672761 3221224544 3221223920 134567516 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29548 21902 603 41 0 29507 0
vsize: 118192
[startup+20 s]
Raw data (loadavg): 1.02 0.97 0.92 2/54 28249
Raw data (stat): 28249 (minisat+) R 28248 28099 28098 0 -1 0 31469 0 0 0 1907 92 0 0 25 0 1 0 541796878 142630912 27193 4294967295 134512640 134672761 3221224544 3221223936 134580781 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 34822 27193 603 41 0 34781 0
vsize: 139288
[startup+30.0007 s]
Raw data (loadavg): 1.02 0.97 0.92 2/54 28249
Raw data (stat): 28249 (minisat+) R 28248 28099 28098 0 -1 0 31505 0 0 0 2906 93 0 0 25 0 1 0 541796878 136290304 25664 4294967295 134512640 134672761 3221224544 3221223488 134522981 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33274 25664 603 41 0 33233 0
vsize: 133096
[startup+40.0009 s]
Raw data (loadavg): 1.01 0.97 0.92 2/54 28249
Raw data (stat): 28249 (minisat+) R 28248 28099 28098 0 -1 0 34287 0 0 0 3899 100 0 0 25 0 1 0 541796878 147980288 28446 4294967295 134512640 134672761 3221224544 3221153420 134594266 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 36128 28446 603 41 0 36087 0
vsize: 144512
[startup+50.0016 s]
Raw data (loadavg): 1.01 0.97 0.92 2/54 28249
Raw data (stat): 28249 (minisat+) R 28248 28099 28098 0 -1 0 38693 0 0 0 4889 110 0 0 25 0 1 0 541796878 163586048 31534 4294967295 134512640 134672761 3221224544 3221223248 134522445 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 39938 31534 603 41 0 39897 0
vsize: 159752
[startup+60.0022 s]
Raw data (loadavg): 1.01 0.97 0.92 2/54 28249
Raw data (stat): 28249 (minisat+) R 28248 28099 28098 0 -1 0 41633 0 0 0 5879 120 0 0 25 0 1 0 541796878 183713792 34474 4294967295 134512640 134672761 3221224544 3221220980 1075346935 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 44852 34474 603 41 0 44811 0
vsize: 179408
[startup+70.0015 s]
Raw data (loadavg): 1.01 0.97 0.92 2/54 28249
Raw data (stat): 28249 (minisat+) R 28248 28099 28098 0 -1 0 49025 0 0 0 6862 137 0 0 25 0 1 0 541796878 200040448 39229 4294967295 134512640 134672761 3221224544 3221222240 134597188 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 48838 39229 603 41 0 48797 0
vsize: 195352
[startup+80.0025 s]
Raw data (loadavg): 1.00 0.97 0.92 2/54 28249
Raw data (stat): 28249 (minisat+) R 28248 28099 28098 0 -1 0 53610 0 0 0 7850 150 0 0 25 0 1 0 541796878 210849792 43177 4294967295 134512640 134672761 3221224544 3220381744 134592917 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 51477 43177 603 41 0 51436 0
vsize: 205908
[startup+90.0017 s]
Raw data (loadavg): 1.00 0.97 0.92 2/54 28249
Raw data (stat): 28249 (minisat+) R 28248 28099 28098 0 -1 0 56768 0 0 0 8843 156 0 0 25 0 1 0 541796878 214929408 44710 4294967295 134512640 134672761 3221224544 3220416128 134594571 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 52473 44710 603 41 0 52432 0
vsize: 209892
[startup+100.002 s]
Raw data (loadavg): 1.00 0.97 0.92 2/54 28249
Raw data (stat): 28249 (minisat+) R 28248 28099 28098 0 -1 0 58061 0 0 0 9839 161 0 0 25 0 1 0 541796878 241295360 45253 4294967295 134512640 134672761 3221224544 3221220300 1074866809 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 58910 45253 603 41 0 58869 0
vsize: 235640
[startup+110.003 s]
Raw data (loadavg): 1.00 0.97 0.92 2/54 28249
Raw data (stat): 28249 (minisat+) R 28248 28099 28098 0 -1 0 59995 0 0 0 10832 167 0 0 25 0 1 0 541796878 246185984 47187 4294967295 134512640 134672761 3221224544 3221223008 134523156 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 60104 47187 603 41 0 60063 0
vsize: 240416
[startup+120.004 s]
Raw data (loadavg): 1.00 0.97 0.92 2/54 28249
Raw data (stat): 28249 (minisat+) R 28248 28099 28098 0 -1 0 61962 0 0 0 11827 173 0 0 25 0 1 0 541796878 251256832 49154 4294967295 134512640 134672761 3221224544 3221221848 1075347105 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 61342 49154 603 41 0 61301 0
vsize: 245368
[startup+130.005 s]
Raw data (loadavg): 1.00 0.97 0.92 2/54 28249
Raw data (stat): 28249 (minisat+) R 28248 28099 28098 0 -1 0 82633 0 0 0 12779 221 0 0 25 0 1 0 541796878 349233152 68961 4294967295 134512640 134672761 3221224544 3221220928 134556762 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 85262 68962 603 41 0 85221 0
vsize: 341048
[startup+140.005 s]
Raw data (loadavg): 1.00 0.97 0.92 2/54 28249
Raw data (stat): 28249 (minisat+) R 28248 28099 28098 0 -1 0 130559 0 0 0 13663 337 0 0 25 0 1 0 541796878 583794688 116887 4294967295 134512640 134672761 3221224544 3221221408 134565545 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 142561 116888 603 41 0 142520 0
vsize: 570112
[startup+150.006 s]
Raw data (loadavg): 1.00 0.97 0.92 2/54 28249
Raw data (stat): 28249 (minisat+) R 28248 28099 28098 0 -1 0 177600 0 0 0 14550 451 0 0 25 0 1 0 541796878 772169728 163928 4294967295 134512640 134672761 3221224544 3221220896 134553607 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 188518 163935 603 41 0 188477 0
vsize: 754072
[startup+160.005 s]
Raw data (loadavg): 1.00 0.97 0.92 2/54 28249
Raw data (stat): 28249 (minisat+) R 28248 28099 28098 0 -1 0 223622 0 0 0 15429 568 0 0 25 0 1 0 541796878 919502848 208544 4294967295 134512640 134672761 3221224544 3221217216 134556276 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 224488 208544 603 41 0 224447 0
vsize: 897952
[startup+161.512 s]
Raw data (loadavg): 1.00 0.97 0.92 1/53 28249
Raw data (stat): 28249 (minisat+) R 28248 28099 28098 0 -1 0 223622 0 0 0 15429 568 0 0 25 0 1 0 541796878 919502848 208544 4294967295 134512640 134672761 3221224544 3221217216 134556276 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 224488 208544 603 41 0 224447 0
vsize: 0

Child ended because it received signal 11 (SIGSEGV)
Real time (s): 161.511
CPU time (s): 161.492
CPU user time (s): 155.218
CPU system time (s): 6.27405
CPU usage (%): 99.9884
Max. virtual memory (Kb): 897952
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####