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/miplib2003/normalized-mps-v2-13-7-dano3mip.opb
MD5SUM	b6a39917c8daf46435ad718b26e9c6f0
Bench Category	optimization, medium integers (OPTMEDINT)
Has Objective Function	YES
Satisfiable
(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
Best CPU time to get the best result obtained on this benchmark
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 18724

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

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

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        776288 kB
Buffers:          4068 kB
Cached:         231484 kB
SwapCached:          0 kB
Active:          63600 kB
Inactive:       174896 kB
HighTotal:      131008 kB
HighFree:          252 kB
LowTotal:       903652 kB
LowFree:        776036 kB
SwapTotal:     2097892 kB
SwapFree:      2097804 kB
Dirty:              48 kB
Writeback:           0 kB
Mapped:           6952 kB
Slab:            14196 kB
Committed_AS:    63796 kB
PageTables:        332 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-21 16:33:18 (client local time) WITH STATUS 0 IN 185.556 SECONDS
stats: 17498 7 185.556 0
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 4450 PB-constraints to clauses...
c   -- Unit propagations: pppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppp
c   -- Detecting intervals from adjacent constraints: #####################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################=====#=====#=====#################################################################################################################################################################################################################################################################################################################################################################################################################################################################################
c   -- Clauses(.)/Splits(s): sssssssssssssssssssssssssssssssssssssssssssssssss
c ---[4498]---> BDD-cost:   17
c ---[4497]---> BDD-cost:   17
c ---[4496]---> BDD-cost:   17
c ---[4495]---> BDD-cost:   17
c ---[4494]---> BDD-cost:   17
c ---[4493]---> BDD-cost:   17
c ---[4492]---> BDD-cost:   17
c ---[4491]---> BDD-cost:   17
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 ---[4473]---> BDD-cost:   63
c ---[4471]---> BDD-cost:   63
c ---[4469]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[4468]---> Adder-cost: 744   maxlim: 131070   bits: 18/17
c ---[4467]---> Adder-cost: 728   maxlim: 65534   bits: 17/16
c ---[4466]---> Adder-cost: 750   maxlim: 131070   bits: 18/17
c ---[4465]---> Adder-cost: 752   maxlim: 131070   bits: 18/17
c ---[4464]---> Adder-cost: 752   maxlim: 131070   bits: 18/17
c ---[4463]---> Adder-cost: 744   maxlim: 131070   bits: 18/17
c ---[4462]---> Adder-cost: 752   maxlim: 131070   bits: 18/17
c ---[4461]---> Adder-cost: 752   maxlim: 131070   bits: 18/17
c ---[4460]---> Adder-cost: 752   maxlim: 131070   bits: 18/17
c ---[4459]---> Adder-cost: 752   maxlim: 131070   bits: 18/17
c ---[4457]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[4456]---> Adder-cost: 748   maxlim: 131070   bits: 18/17
c ---[4455]---> Adder-cost: 752   maxlim: 131070   bits: 18/17
c ---[4454]---> Adder-cost: 750   maxlim: 131070   bits: 18/17
c ---[4453]---> Adder-cost: 752   maxlim: 131070   bits: 18/17
c ---[4452]---> Adder-cost: 748   maxlim: 131070   bits: 18/17
c ---[4451]---> Adder-cost: 752   maxlim: 131070   bits: 18/17
c ---[4450]---> Adder-cost: 746   maxlim: 131070   bits: 18/17
c ---[4449]---> Adder-cost: 752   maxlim: 131070   bits: 18/17
c ---[4448]---> Adder-cost: 726   maxlim: 65534   bits: 17/16
c ---[4447]---> Adder-cost: 750   maxlim: 131070   bits: 18/17
c ---[4445]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[4444]---> Adder-cost: 752   maxlim: 131070   bits: 18/17
c ---[4443]---> Adder-cost: 750   maxlim: 131070   bits: 18/17
c ---[4442]---> Adder-cost: 746   maxlim: 131070   bits: 18/17
c ---[4441]---> Adder-cost: 750   maxlim: 131070   bits: 18/17
c ---[4440]---> Adder-cost: 744   maxlim: 131070   bits: 18/17
c ---[4439]---> Adder-cost: 752   maxlim: 131070   bits: 18/17
c ---[4438]---> Adder-cost: 746   maxlim: 131070   bits: 18/17
c ---[4437]---> Adder-cost: 748   maxlim: 131070   bits: 18/17
c ---[4436]---> Adder-cost: 744   maxlim: 131070   bits: 18/17
c ---[4435]---> Adder-cost: 746   maxlim: 131070   bits: 18/17
c ---[4433]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[4432]---> Adder-cost: 752   maxlim: 131070   bits: 18/17
c ---[4431]---> Adder-cost: 752   maxlim: 131070   bits: 18/17
c ---[4430]---> Adder-cost: 746   maxlim: 131070   bits: 18/17
c ---[4429]---> Adder-cost: 743   maxlim: 131070   bits: 18/17
c ---[4428]---> Adder-cost: 750   maxlim: 131070   bits: 18/17
c ---[4427]---> Adder-cost: 752   maxlim: 131070   bits: 18/17
c ---[4426]---> Adder-cost: 752   maxlim: 131070   bits: 18/17
c ---[4425]---> Adder-cost: 752   maxlim: 131070   bits: 18/17
c ---[4424]---> Adder-cost: 752   maxlim: 131070   bits: 18/17
c ---[4423]---> Adder-cost: 752   maxlim: 131070   bits: 18/17
c ---[4421]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[4420]---> Adder-cost: 750   maxlim: 131070   bits: 18/17
c ---[4419]---> Adder-cost: 744   maxlim: 131070   bits: 18/17
c ---[4418]---> Adder-cost: 752   maxlim: 131070   bits: 18/17
c ---[4417]---> Adder-cost: 748   maxlim: 131070   bits: 18/17
c ---[4416]---> Adder-cost: 752   maxlim: 131070   bits: 18/17
c ---[4415]---> Adder-cost: 746   maxlim: 131070   bits: 18/17
c ---[4414]---> Adder-cost: 748   maxlim: 131070   bits: 18/17
c ---[4413]---> Adder-cost: 752   maxlim: 131070   bits: 18/17
c ---[4412]---> Adder-cost: 748   maxlim: 131070   bits: 18/17
c ---[4411]---> Adder-cost: 746   maxlim: 131070   bits: 18/17
c ---[4409]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[4408]---> Adder-cost: 746   maxlim: 131070   bits: 18/17
c ---[4407]---> Adder-cost: 752   maxlim: 131070   bits: 18/17
c ---[4406]---> Adder-cost: 752   maxlim: 131070   bits: 18/17
c ---[4405]---> Adder-cost: 748   maxlim: 131070   bits: 18/17
c ---[4404]---> Adder-cost: 752   maxlim: 131070   bits: 18/17
c ---[4403]---> Adder-cost: 748   maxlim: 131070   bits: 18/17
c ---[4402]---> Adder-cost: 752   maxlim: 131070   bits: 18/17
c ---[4401]---> Adder-cost: 752   maxlim: 131070   bits: 18/17
c ---[4400]---> Adder-cost: 748   maxlim: 131070   bits: 18/17
c ---[4399]---> Adder-cost: 752   maxlim: 131070   bits: 18/17
c ---[4397]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[4396]---> Adder-cost: 744   maxlim: 131070   bits: 18/17
c ---[4395]---> Adder-cost: 746   maxlim: 131070   bits: 18/17
c ---[4394]---> Adder-cost: 746   maxlim: 131070   bits: 18/17
c ---[4393]---> Adder-cost: 744   maxlim: 131070   bits: 18/17
c ---[4392]---> Adder-cost: 752   maxlim: 131070   bits: 18/17
c ---[4391]---> Adder-cost: 750   maxlim: 131070   bits: 18/17
c ---[4390]---> Adder-cost: 752   maxlim: 131070   bits: 18/17
c ---[4389]---> Adder-cost: 750   maxlim: 131070   bits: 18/17
c ---[4388]---> Adder-cost: 748   maxlim: 131070   bits: 18/17
c ---[4387]---> Adder-cost: 748   maxlim: 131070   bits: 18/17
c ---[4385]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[4384]---> Adder-cost: 722   maxlim: 65534   bits: 17/16
c ---[4383]---> Adder-cost: 752   maxlim: 131070   bits: 18/17
c ---[4382]---> Adder-cost: 750   maxlim: 131070   bits: 18/17
c ---[4381]---> Adder-cost: 748   maxlim: 131070   bits: 18/17
c ---[4380]---> Adder-cost: 744   maxlim: 131070   bits: 18/17
c ---[4379]---> Adder-cost: 746   maxlim: 131070   bits: 18/17
c ---[4378]---> Adder-cost: 752   maxlim: 131070   bits: 18/17
c ---[4377]---> Adder-cost: 750   maxlim: 131070   bits: 18/17
c ---[4376]---> Adder-cost: 752   maxlim: 131070   bits: 18/17
c ---[4375]---> Adder-cost: 752   maxlim: 131070   bits: 18/17
c ---[4373]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[4372]---> Adder-cost: 752   maxlim: 131070   bits: 18/17
c ---[4371]---> Adder-cost: 748   maxlim: 131070   bits: 18/17
c ---[4370]---> Adder-cost: 750   maxlim: 131070   bits: 18/17
c ---[4369]---> Adder-cost: 748   maxlim: 131070   bits: 18/17
c ---[4368]---> Adder-cost: 750   maxlim: 131070   bits: 18/17
c ---[4367]---> Adder-cost: 752   maxlim: 131070   bits: 18/17
c ---[4366]---> Adder-cost: 752   maxlim: 131070   bits: 18/17
c ---[4365]---> Adder-cost: 728   maxlim: 65534   bits: 17/16
c ---[4364]---> Adder-cost: 752   maxlim: 131070   bits: 18/17
c ---[4363]---> Adder-cost: 750   maxlim: 131070   bits: 18/17
c ---[4361]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[4360]---> Adder-cost: 748   maxlim: 131070   bits: 18/17
c ---[4359]---> Adder-cost: 752   maxlim: 131070   bits: 18/17
c ---[4358]---> Adder-cost: 749   maxlim: 131070   bits: 18/17
c ---[4357]---> Adder-cost: 750   maxlim: 131070   bits: 18/17
c ---[4356]---> Adder-cost: 750   maxlim: 131070   bits: 18/17
c ---[4354]---> Adder-cost: 1496   maxlim: 3011561   bits: 23/22
c ---[4352]---> Adder-cost: 1496   maxlim: 3009129   bits: 23/22
c ---[4350]---> Adder-cost: 1496   maxlim: 3011689   bits: 23/22
c ---[4348]---> Adder-cost: 1496   maxlim: 3011945   bits: 23/22
c ---[4346]---> Adder-cost: 1496   maxlim: 3009385   bits: 23/22
c ---[4344]---> BDD-cost:   63
c ---[4342]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[4340]---> Adder-cost: 1496   maxlim: 3006825   bits: 23/22
c ---[4338]---> Adder-cost: 1496   maxlim: 3011945   bits: 23/22
c ---[4336]---> Adder-cost: 1496   maxlim: 3012073   bits: 23/22
c ---[4334]---> Adder-cost: 1496   maxlim: 3014633   bits: 23/22
c ---[4332]---> Adder-cost: 1496   maxlim: 3014633   bits: 23/22
c ---[4330]---> Adder-cost: 1496   maxlim: 3014633   bits: 23/22
c ---[4328]---> Adder-cost: 1496   maxlim: 3014633   bits: 23/22
c ---[4326]---> Adder-cost: 1496   maxlim: 3014633   bits: 23/22
c ---[4324]---> Adder-cost: 1496   maxlim: 2943977   bits: 23/22
c ---[4322]---> Adder-cost: 1496   maxlim: 3014633   bits: 23/22
c ---[4320]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[4318]---> Adder-cost: 1496   maxlim: 3014633   bits: 23/22
c ---[4316]---> Adder-cost: 1496   maxlim: 3014633   bits: 23/22
c ---[4314]---> Adder-cost: 1496   maxlim: 3014633   bits: 23/22
c ---[4312]---> Adder-cost: 1496   maxlim: 3014633   bits: 23/22
c ---[4310]---> Adder-cost: 1496   maxlim: 3011561   bits: 23/22
c ---[4308]---> Adder-cost: 1496   maxlim: 3012201   bits: 23/22
c ---[4306]---> Adder-cost: 1496   maxlim: 3011689   bits: 23/22
c ---[4304]---> Adder-cost: 1496   maxlim: 3014633   bits: 23/22
c ---[4302]---> Adder-cost: 1496   maxlim: 3014633   bits: 23/22
c ---[4300]---> Adder-cost: 1496   maxlim: 3014633   bits: 23/22
c ---[4298]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[4296]---> Adder-cost: 1496   maxlim: 3014633   bits: 23/22
c ---[4294]---> Adder-cost: 1496   maxlim: 3011945   bits: 23/22
c ---[4292]---> Adder-cost: 1496   maxlim: 3012329   bits: 23/22
c ---[4290]---> Adder-cost: 1496   maxlim: 3009641   bits: 23/22
c ---[4288]---> Adder-cost: 1496   maxlim: 3011689   bits: 23/22
c ---[4286]---> Adder-cost: 1496   maxlim: 3014633   bits: 23/22
c ---[4284]---> Adder-cost: 1496   maxlim: 3014633   bits: 23/22
c ---[4282]---> Adder-cost: 1496   maxlim: 3009513   bits: 23/22
c ---[4280]---> Adder-cost: 1496   maxlim: 3012201   bits: 23/22
c ---[4278]---> Adder-cost: 1496   maxlim: 3006441   bits: 23/22
c ---[4276]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[4274]---> Adder-cost: 1496   maxlim: 3012201   bits: 23/22
c ---[4272]---> Adder-cost: 1496   maxlim: 3012457   bits: 23/22
c ---[4270]---> Adder-cost: 1496   maxlim: 2940905   bits: 23/22
c ---[4268]---> Adder-cost: 1496   maxlim: 3004393   bits: 23/22
c ---[4266]---> Adder-cost: 1496   maxlim: 3014633   bits: 23/22
c ---[4264]---> Adder-cost: 1496   maxlim: 3014633   bits: 23/22
c ---[4262]---> Adder-cost: 1496   maxlim: 3011817   bits: 23/22
c ---[4260]---> Adder-cost: 1496   maxlim: 2946025   bits: 23/22
c ---[4258]---> Adder-cost: 1496   maxlim: 3012329   bits: 23/22
c ---[4256]---> Adder-cost: 1496   maxlim: 3012201   bits: 23/22
c ---[4254]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[4252]---> Adder-cost: 1496   maxlim: 3014633   bits: 23/22
c ---[4250]---> Adder-cost: 1496   maxlim: 3012585   bits: 23/22
c ---[4248]---> Adder-cost: 1496   maxlim: 3014633   bits: 23/22
c ---[4246]---> Adder-cost: 1496   maxlim: 3012073   bits: 23/22
c ---[4244]---> Adder-cost: 1496   maxlim: 3009001   bits: 23/22
c ---[4242]---> Adder-cost: 1496   maxlim: 3014633   bits: 23/22
c ---[4240]---> Adder-cost: 1496   maxlim: 3009257   bits: 23/22
c ---[4238]---> Adder-cost: 1496   maxlim: 3011817   bits: 23/22
c ---[4236]---> Adder-cost: 1496   maxlim: 3012073   bits: 23/22
c ---[4234]---> Adder-cost: 1496   maxlim: 3014633   bits: 23/22
c ---[4232]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[4230]---> Adder-cost: 1496   maxlim: 3014633   bits: 23/22
c ---[4228]---> Adder-cost: 1496   maxlim: 3011689   bits: 23/22
c ---[4226]---> Adder-cost: 1496   maxlim: 3011945   bits: 23/22
c ---[4224]---> Adder-cost: 1496   maxlim: 3014633   bits: 23/22
c ---[4222]---> Adder-cost: 1496   maxlim: 3009513   bits: 23/22
c ---[4220]---> Adder-cost: 1496   maxlim: 3011945   bits: 23/22
c ---[4218]---> Adder-cost: 1496   maxlim: 3009769   bits: 23/22
c ---[4216]---> Adder-cost: 1496   maxlim: 3002217   bits: 23/22
c ---[4214]---> Adder-cost: 1496   maxlim: 3011817   bits: 23/22
c ---[4212]---> Adder-cost: 1496   maxlim: 3012457   bits: 23/22
c ---[4210]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[4208]---> Adder-cost: 1496   maxlim: 3012073   bits: 23/22
c ---[4206]---> Adder-cost: 1496   maxlim: 3009897   bits: 23/22
c ---[4204]---> Adder-cost: 1496   maxlim: 3012457   bits: 23/22
c ---[4202]---> Adder-cost: 1496   maxlim: 3012073   bits: 23/22
c ---[4200]---> Adder-cost: 1496   maxlim: 3009257   bits: 23/22
c ---[4198]---> Adder-cost: 1496   maxlim: 3012073   bits: 23/22
c ---[4196]---> Adder-cost: 1496   maxlim: 3012329   bits: 23/22
c ---[4194]---> Adder-cost: 1496   maxlim: 3009513   bits: 23/22
c ---[4192]---> Adder-cost: 1496   maxlim: 3007337   bits: 23/22
c ---[4190]---> Adder-cost: 1496   maxlim: 3009129   bits: 23/22
c ---[4188]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[4186]---> Adder-cost: 1496   maxlim: 3009257   bits: 23/22
c ---[4184]---> Adder-cost: 1496   maxlim: 3014633   bits: 23/22
c ---[4182]---> Adder-cost: 1496   maxlim: 2949097   bits: 23/22
c ---[4180]---> Adder-cost: 1496   maxlim: 3012201   bits: 23/22
c ---[4178]---> Adder-cost: 1496   maxlim: 3012457   bits: 23/22
c ---[4176]---> Adder-cost: 1496   maxlim: 3014633   bits: 23/22
c ---[4174]---> Adder-cost: 1496   maxlim: 3009641   bits: 23/22
c ---[4172]---> Adder-cost: 1496   maxlim: 3014633   bits: 23/22
c ---[4170]---> Adder-cost: 1496   maxlim: 3014633   bits: 23/22
c ---[4168]---> Adder-cost: 1496   maxlim: 3011817   bits: 23/22
c ---[4166]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[4164]---> Adder-cost: 1496   maxlim: 3009385   bits: 23/22
c ---[4162]---> Adder-cost: 1496   maxlim: 3014633   bits: 23/22
c ---[4160]---> Adder-cost: 1496   maxlim: 3014633   bits: 23/22
c ---[4158]---> Adder-cost: 1496   maxlim: 3012457   bits: 23/22
c ---[4156]---> Adder-cost: 1496   maxlim: 3009257   bits: 23/22
c ---[4154]---> Adder-cost: 1496   maxlim: 2943977   bits: 23/22
c ---[4152]---> Adder-cost: 1496   maxlim: 3009129   bits: 23/22
c ---[4150]---> Adder-cost: 1496   maxlim: 3014633   bits: 23/22
c ---[4148]---> Adder-cost: 1496   maxlim: 3014633   bits: 23/22
c ---[4146]---> Adder-cost: 1496   maxlim: 3014633   bits: 23/22
c ---[4144]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[4142]---> Adder-cost: 1496   maxlim: 2943977   bits: 23/22
c ---[4140]---> Adder-cost: 1490   maxlim: 3004009   bits: 23/22
c ---[4138]---> Adder-cost: 1496   maxlim: 3006953   bits: 23/22
c ---[4136]---> Adder-cost: 1496   maxlim: 3014633   bits: 23/22
c ---[4134]---> Adder-cost: 1496   maxlim: 3009001   bits: 23/22
c ---[4132]---> Adder-cost: 1496   maxlim: 3014633   bits: 23/22
c ---[4130]---> Adder-cost: 1496   maxlim: 3009897   bits: 23/22
c ---[4128]---> Adder-cost: 1496   maxlim: 3006953   bits: 23/22
c ---[4126]---> Adder-cost: 1496   maxlim: 3014633   bits: 23/22
c ---[4124]---> Adder-cost: 1496   maxlim: 2943977   bits: 23/22
c ---[4122]---> BDD-cost:   63
c ---[4120]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[4118]---> Adder-cost: 1496   maxlim: 3014633   bits: 23/22
c ---[4116]---> Adder-cost: 1496   maxlim: 3014633   bits: 23/22
c ---[4114]---> Adder-cost: 1496   maxlim: 3009513   bits: 23/22
c ---[4112]---> Adder-cost: 1496   maxlim: 3012201   bits: 23/22
c ---[4110]---> Adder-cost: 1496   maxlim: 3014633   bits: 23/22
c ---[4108]---> Adder-cost: 1496   maxlim: 3009641   bits: 23/22
c ---[4106]---> Adder-cost: 1496   maxlim: 3009385   bits: 23/22
c ---[4104]---> Adder-cost: 1496   maxlim: 3012457   bits: 23/22
c ---[4102]---> Adder-cost: 1496   maxlim: 3014633   bits: 23/22
c ---[4100]---> Adder-cost: 1496   maxlim: 3014633   bits: 23/22
c ---[4098]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[4096]---> Adder-cost: 1496   maxlim: 3006953   bits: 23/22
c ---[4094]---> Adder-cost: 1496   maxlim: 3012329   bits: 23/22
c ---[4092]---> Adder-cost: 1496   maxlim: 3014633   bits: 23/22
c ---[4090]---> Adder-cost: 1496   maxlim: 3009897   bits: 23/22
c ---[4088]---> Adder-cost: 1496   maxlim: 3012329   bits: 23/22
c ---[4086]---> Adder-cost: 1496   maxlim: 3011945   bits: 23/22
c ---[4084]---> Adder-cost: 1496   maxlim: 3009385   bits: 23/22
c ---[4082]---> Adder-cost: 1496   maxlim: 3011689   bits: 23/22
c ---[4080]---> Adder-cost: 1496   maxlim: 3009641   bits: 23/22
c ---[4078]---> Adder-cost: 1496   maxlim: 3014633   bits: 23/22
c ---[4076]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[4074]---> Adder-cost: 1496   maxlim: 3006569   bits: 23/22
c ---[4072]---> Adder-cost: 1496   maxlim: 3006953   bits: 23/22
c ---[4070]---> Adder-cost: 1496   maxlim: 3009641   bits: 23/22
c ---[4068]---> Adder-cost: 1496   maxlim: 3014633   bits: 23/22
c ---[4066]---> Adder-cost: 1496   maxlim: 3012201   bits: 23/22
c ---[4064]---> Adder-cost: 1496   maxlim: 3014633   bits: 23/22
c ---[4062]---> Adder-cost: 1496   maxlim: 3012585   bits: 23/22
c ---[4060]---> Adder-cost: 1496   maxlim: 3012585   bits: 23/22
c ---[4058]---> Adder-cost: 1496   maxlim: 3014633   bits: 23/22
c ---[4056]---> Adder-cost: 1496   maxlim: 3014633   bits: 23/22
c ---[4054]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[4052]---> Adder-cost: 1496   maxlim: 3009513   bits: 23/22
c ---[4050]---> Adder-cost: 1496   maxlim: 3014633   bits: 23/22
c ---[4048]---> Adder-cost: 1496   maxlim: 3012585   bits: 23/22
c ---[4046]---> Adder-cost: 1496   maxlim: 3011817   bits: 23/22
c ---[4044]---> Adder-cost: 1496   maxlim: 3014633   bits: 23/22
c ---[4042]---> Adder-cost: 1496   maxlim: 3014633   bits: 23/22
c ---[4040]---> Adder-cost: 1496   maxlim: 2949097   bits: 23/22
c ---[4038]---> Adder-cost: 1496   maxlim: 3014633   bits: 23/22
c ---[4036]---> Adder-cost: 1496   maxlim: 3014633   bits: 23/22
c ---[4034]---> Adder-cost: 1496   maxlim: 2941289   bits: 23/22
c ---[4032]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[4030]---> Adder-cost: 1496   maxlim: 3010025   bits: 23/22
c ---[4028]---> Adder-cost: 1488   maxlim: 3004393   bits: 23/22
c ---[4026]---> Adder-cost: 1496   maxlim: 3002345   bits: 23/22
c ---[4024]---> Adder-cost: 1496   maxlim: 3012201   bits: 23/22
c ---[4022]---> Adder-cost: 1496   maxlim: 3012201   bits: 23/22
c ---[4020]---> Adder-cost: 1496   maxlim: 3009385   bits: 23/22
c ---[4018]---> Adder-cost: 1496   maxlim: 3012585   bits: 23/22
c ---[4016]---> Adder-cost: 1496   maxlim: 3014633   bits: 23/22
c ---[4014]---> Adder-cost: 1496   maxlim: 3014633   bits: 23/22
c ---[4012]---> Adder-cost: 1496   maxlim: 3014633   bits: 23/22
c ---[4010]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[4008]---> Adder-cost: 1496   maxlim: 2946281   bits: 23/22
c ---[4006]---> Adder-cost: 1496   maxlim: 3014633   bits: 23/22
c ---[4004]---> Adder-cost: 1496   maxlim: 3009129   bits: 23/22
c ---[4002]---> Adder-cost: 1496   maxlim: 3014633   bits: 23/22
c ---[4000]---> Adder-cost: 1496   maxlim: 2943465   bits: 23/22
c ---[3998]---> Adder-cost: 1496   maxlim: 3011817   bits: 23/22
c ---[3996]---> Adder-cost: 1496   maxlim: 3014633   bits: 23/22
c ---[3994]---> Adder-cost: 1496   maxlim: 3014633   bits: 23/22
c ---[3992]---> Adder-cost: 1496   maxlim: 3012073   bits: 23/22
c ---[3990]---> Adder-cost: 1496   maxlim: 3012201   bits: 23/22
c ---[3988]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[3986]---> Adder-cost: 1496   maxlim: 3012457   bits: 23/22
c ---[3984]---> Adder-cost: 1496   maxlim: 3012073   bits: 23/22
c ---[3982]---> Adder-cost: 1496   maxlim: 3009513   bits: 23/22
c ---[3980]---> Adder-cost: 1496   maxlim: 3014633   bits: 23/22
c ---[3978]---> Adder-cost: 1496   maxlim: 3006953   bits: 23/22
c ---[3976]---> Adder-cost: 1496   maxlim: 3006825   bits: 23/22
c ---[3974]---> Adder-cost: 1496   maxlim: 3014633   bits: 23/22
c ---[3972]---> Adder-cost: 1496   maxlim: 3012073   bits: 23/22
c ---[3970]---> Adder-cost: 1496   maxlim: 3006697   bits: 23/22
c ---[3968]---> Adder-cost: 1496   maxlim: 3012073   bits: 23/22
c ---[3966]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[3964]---> Adder-cost: 1496   maxlim: 3014633   bits: 23/22
c ---[3962]---> Adder-cost: 1496   maxlim: 3014633   bits: 23/22
c ---[3960]---> Adder-cost: 1496   maxlim: 3009769   bits: 23/22
c ---[3958]---> Adder-cost: 1496   maxlim: 3014633   bits: 23/22
c ---[3956]---> Adder-cost: 1496   maxlim: 3014633   bits: 23/22
c ---[3954]---> Adder-cost: 1496   maxlim: 3014633   bits: 23/22
c ---[3952]---> Adder-cost: 1496   maxlim: 3014633   bits: 23/22
c ---[3950]---> Adder-cost: 1496   maxlim: 3011561   bits: 23/22
c ---[3948]---> Adder-cost: 1496   maxlim: 3011817   bits: 23/22
c ---[3946]---> Adder-cost: 1496   maxlim: 3011945   bits: 23/22
c ---[3944]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[3942]---> Adder-cost: 1496   maxlim: 3011817   bits: 23/22
c ---[3940]---> Adder-cost: 1496   maxlim: 3009769   bits: 23/22
c ---[3938]---> Adder-cost: 1496   maxlim: 3014633   bits: 23/22
c ---[3936]---> Adder-cost: 1496   maxlim: 3009001   bits: 23/22
c ---[3934]---> Adder-cost: 1496   maxlim: 3012073   bits: 23/22
c ---[3932]---> Adder-cost: 1496   maxlim: 3009513   bits: 23/22
c ---[3930]---> Adder-cost: 1496   maxlim: 3009641   bits: 23/22
c ---[3928]---> Adder-cost: 1496   maxlim: 3010025   bits: 23/22
c ---[3926]---> Adder-cost: 1496   maxlim: 3011817   bits: 23/22
c ---[3924]---> Adder-cost: 1496   maxlim: 3011945   bits: 23/22
c ---[3922]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[3920]---> Adder-cost: 1496   maxlim: 3012201   bits: 23/22
c ---[3918]---> Adder-cost: 1496   maxlim: 3009641   bits: 23/22
c ---[3916]---> Adder-cost: 1496   maxlim: 3012201   bits: 23/22
c ---[3914]---> Adder-cost: 1496   maxlim: 3014633   bits: 23/22
c ---[3912]---> Adder-cost: 1496   maxlim: 3014633   bits: 23/22
c ---[3910]---> Adder-cost: 1496   maxlim: 3011945   bits: 23/22
c ---[3908]---> Adder-cost: 1496   maxlim: 3011561   bits: 23/22
c ---[3906]---> Adder-cost: 1496   maxlim: 3012585   bits: 23/22
c ---[3904]---> Adder-cost: 1496   maxlim: 3011689   bits: 23/22
c ---[3902]---> Adder-cost: 1496   maxlim: 3011945   bits: 23/22
c ---[3900]---> BDD-cost:   63
c ---[3898]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[3896]---> Adder-cost: 1496   maxlim: 3009897   bits: 23/22
c ---[3894]---> Adder-cost: 1496   maxlim: 3014633   bits: 23/22
c ---[3892]---> Adder-cost: 1496   maxlim: 3014633   bits: 23/22
c ---[3890]---> Adder-cost: 1496   maxlim: 3011561   bits: 23/22
c ---[3888]---> Adder-cost: 1496   maxlim: 2946153   bits: 23/22
c ---[3886]---> Adder-cost: 1496   maxlim: 3009641   bits: 23/22
c ---[3884]---> Adder-cost: 1496   maxlim: 3012073   bits: 23/22
c ---[3882]---> Adder-cost: 1496   maxlim: 3014633   bits: 23/22
c ---[3880]---> Adder-cost: 1496   maxlim: 3014633   bits: 23/22
c ---[3878]---> Adder-cost: 1496   maxlim: 3009385   bits: 23/22
c ---[3876]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[3874]---> Adder-cost: 1496   maxlim: 3014633   bits: 23/22
c ---[3872]---> Adder-cost: 1496   maxlim: 2949097   bits: 23/22
c ---[3870]---> Adder-cost: 1496   maxlim: 3011817   bits: 23/22
c ---[3868]---> Adder-cost: 1496   maxlim: 3014633   bits: 23/22
c ---[3866]---> Adder-cost: 1496   maxlim: 3014633   bits: 23/22
c ---[3864]---> Adder-cost: 1496   maxlim: 3009001   bits: 23/22
c ---[3862]---> Adder-cost: 1496   maxlim: 3009257   bits: 23/22
c ---[3860]---> Adder-cost: 1496   maxlim: 3011817   bits: 23/22
c ---[3858]---> Adder-cost: 1490   maxlim: 3009257   bits: 23/22
c ---[3856]---> Adder-cost: 1496   maxlim: 2946281   bits: 23/22
c ---[3854]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[3852]---> Adder-cost: 1496   maxlim: 3012201   bits: 23/22
c ---[3850]---> Adder-cost: 1496   maxlim: 3012073   bits: 23/22
c ---[3848]---> Adder-cost: 1496   maxlim: 3007209   bits: 23/22
c ---[3846]---> Adder-cost: 1496   maxlim: 3012329   bits: 23/22
c ---[3844]---> Adder-cost: 1496   maxlim: 3014633   bits: 23/22
c ---[3842]---> Adder-cost: 1490   maxlim: 3006953   bits: 23/22
c ---[3840]---> Adder-cost: 1496   maxlim: 2941801   bits: 23/22
c ---[3838]---> Adder-cost: 1496   maxlim: 3014633   bits: 23/22
c ---[3836]---> Adder-cost: 1496   maxlim: 3014633   bits: 23/22
c ---[3834]---> Adder-cost: 1496   maxlim: 3012585   bits: 23/22
c ---[3832]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[3830]---> Adder-cost: 1496   maxlim: 3014633   bits: 23/22
c ---[3828]---> Adder-cost: 1496   maxlim: 3012585   bits: 23/22
c ---[3826]---> Adder-cost: 1496   maxlim: 2944361   bits: 23/22
c ---[3824]---> Adder-cost: 1496   maxlim: 3014633   bits: 23/22
c ---[3822]---> Adder-cost: 1496   maxlim: 3014633   bits: 23/22
c ---[3820]---> Adder-cost: 1496   maxlim: 3009001   bits: 23/22
c ---[3818]---> Adder-cost: 1496   maxlim: 2941033   bits: 23/22
c ---[3816]---> Adder-cost: 1496   maxlim: 3014633   bits: 23/22
c ---[3814]---> Adder-cost: 1496   maxlim: 3012329   bits: 23/22
c ---[3812]---> Adder-cost: 1496   maxlim: 3014633   bits: 23/22
c ---[3810]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[3808]---> Adder-cost: 1496   maxlim: 3012457   bits: 23/22
c ---[3806]---> Adder-cost: 1496   maxlim: 3012329   bits: 23/22
c ---[3804]---> Adder-cost: 1496   maxlim: 3014633   bits: 23/22
c ---[3802]---> Adder-cost: 1496   maxlim: 3014633   bits: 23/22
c ---[3800]---> Adder-cost: 1496   maxlim: 3014633   bits: 23/22
c ---[3798]---> Adder-cost: 1496   maxlim: 3001833   bits: 23/22
c ---[3796]---> Adder-cost: 1496   maxlim: 2946025   bits: 23/22
c ---[3794]---> Adder-cost: 1496   maxlim: 3011689   bits: 23/22
c ---[3792]---> Adder-cost: 1496   maxlim: 3014633   bits: 23/22
c ---[3790]---> Adder-cost: 1496   maxlim: 3009001   bits: 23/22
c ---[3788]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[3786]---> Adder-cost: 1496   maxlim: 3009001   bits: 23/22
c ---[3784]---> Adder-cost: 1496   maxlim: 3014633   bits: 23/22
c ---[3782]---> Adder-cost: 1496   maxlim: 3011689   bits: 23/22
c ---[3780]---> Adder-cost: 1496   maxlim: 3012457   bits: 23/22
c ---[3778]---> Adder-cost: 1496   maxlim: 3009641   bits: 23/22
c ---[3776]---> Adder-cost: 1496   maxlim: 3011945   bits: 23/22
c ---[3774]---> Adder-cost: 1496   maxlim: 3014633   bits: 23/22
c ---[3772]---> Adder-cost: 1496   maxlim: 3012457   bits: 23/22
c ---[3770]---> Adder-cost: 1496   maxlim: 2943977   bits: 23/22
c ---[3768]---> Adder-cost: 1496   maxlim: 3011561   bits: 23/22
c ---[3766]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[3764]---> Adder-cost: 1496   maxlim: 3004649   bits: 23/22
c ---[3762]---> Adder-cost: 1496   maxlim: 3012457   bits: 23/22
c ---[3760]---> Adder-cost: 1496   maxlim: 3011561   bits: 23/22
c ---[3758]---> Adder-cost: 1496   maxlim: 3012073   bits: 23/22
c ---[3756]---> Adder-cost: 1496   maxlim: 3012329   bits: 23/22
c ---[3754]---> Adder-cost: 1496   maxlim: 3014633   bits: 23/22
c ---[3752]---> Adder-cost: 1496   maxlim: 3011561   bits: 23/22
c ---[3750]---> Adder-cost: 1496   maxlim: 3011561   bits: 23/22
c ---[3748]---> Adder-cost: 1496   maxlim: 3014633   bits: 23/22
c ---[3746]---> Adder-cost: 1496   maxlim: 3012073   bits: 23/22
c ---[3744]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[3742]---> Adder-cost: 1496   maxlim: 3014633   bits: 23/22
c ---[3740]---> Adder-cost: 1496   maxlim: 3011689   bits: 23/22
c ---[3738]---> Adder-cost: 1496   maxlim: 3012585   bits: 23/22
c ---[3736]---> Adder-cost: 1496   maxlim: 3014633   bits: 23/22
c ---[3734]---> Adder-cost: 1496   maxlim: 3014633   bits: 23/22
c ---[3732]---> Adder-cost: 1496   maxlim: 3014633   bits: 23/22
c ---[3730]---> Adder-cost: 1496   maxlim: 2946153   bits: 23/22
c ---[3728]---> Adder-cost: 1496   maxlim: 3014633   bits: 23/22
c ---[3726]---> Adder-cost: 1496   maxlim: 3014633   bits: 23/22
c ---[3724]---> Adder-cost: 1496   maxlim: 3014633   bits: 23/22
c ---[3722]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[3720]---> Adder-cost: 1496   maxlim: 3014633   bits: 23/22
c ---[3718]---> Adder-cost: 1490   maxlim: 2910825   bits: 23/22
c ---[3716]---> Adder-cost: 1490   maxlim: 2941673   bits: 23/22
c ---[3714]---> Adder-cost: 1496   maxlim: 2916329   bits: 23/22
c ---[3712]---> Adder-cost: 1496   maxlim: 3011561   bits: 23/22
c ---[3710]---> Adder-cost: 1486   maxlim: 3006953   bits: 23/22
c ---[3708]---> Adder-cost: 1496   maxlim: 3014633   bits: 23/22
c ---[3706]---> Adder-cost: 1496   maxlim: 3014633   bits: 23/22
c ---[3704]---> Adder-cost: 1496   maxlim: 2913897   bits: 23/22
c ---[3702]---> Adder-cost: 1496   maxlim: 3014633   bits: 23/22
c ---[3700]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[3698]---> Adder-cost: 1496   maxlim: 2913641   bits: 23/22
c ---[3696]---> Adder-cost: 1496   maxlim: 3014633   bits: 23/22
c ---[3694]---> Adder-cost: 1496   maxlim: 3012073   bits: 23/22
c ---[3692]---> Adder-cost: 1496   maxlim: 3014633   bits: 23/22
c ---[3690]---> Adder-cost: 1496   maxlim: 2943465   bits: 23/22
c ---[3688]---> Adder-cost: 1496   maxlim: 3012073   bits: 23/22
c ---[3686]---> Adder-cost: 1496   maxlim: 3014633   bits: 23/22
c ---[3684]---> Adder-cost: 1496   maxlim: 3012201   bits: 23/22
c ---[3682]---> Adder-cost: 1496   maxlim: 3011945   bits: 23/22
c ---[3680]---> Adder-cost: 1496   maxlim: 3014633   bits: 23/22
c ---[3678]---> BDD-cost:   63
c ---[3676]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[3674]---> Adder-cost: 1496   maxlim: 3009641   bits: 23/22
c ---[3672]---> Adder-cost: 1496   maxlim: 3012201   bits: 23/22
c ---[3670]---> Adder-cost: 1496   maxlim: 3014633   bits: 23/22
c ---[3668]---> Adder-cost: 1496   maxlim: 3014633   bits: 23/22
c ---[3666]---> Adder-cost: 1496   maxlim: 3014633   bits: 23/22
c ---[3664]---> Adder-cost: 1496   maxlim: 2944105   bits: 23/22
c ---[3662]---> Adder-cost: 1496   maxlim: 3011817   bits: 23/22
c ---[3660]---> Adder-cost: 1496   maxlim: 3014633   bits: 23/22
c ---[3658]---> Adder-cost: 1496   maxlim: 3006441   bits: 23/22
c ---[3656]---> Adder-cost: 1496   maxlim: 3011561   bits: 23/22
c ---[3654]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[3652]---> Adder-cost: 1496   maxlim: 3011817   bits: 23/22
c ---[3650]---> Adder-cost: 1496   maxlim: 3014633   bits: 23/22
c ---[3648]---> Adder-cost: 1496   maxlim: 3009641   bits: 23/22
c ---[3646]---> Adder-cost: 1496   maxlim: 3014633   bits: 23/22
c ---[3644]---> Adder-cost: 1496   maxlim: 3009129   bits: 23/22
c ---[3642]---> Adder-cost: 1496   maxlim: 3009257   bits: 23/22
c ---[3640]---> Adder-cost: 1496   maxlim: 3012585   bits: 23/22
c ---[3638]---> Adder-cost: 1496   maxlim: 3014633   bits: 23/22
c ---[3636]---> Adder-cost: 1496   maxlim: 3006953   bits: 23/22
c ---[3634]---> Adder-cost: 1496   maxlim: 3009897   bits: 23/22
c ---[3632]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[3630]---> Adder-cost: 1496   maxlim: 3012329   bits: 23/22
c ---[3628]---> Adder-cost: 1496   maxlim: 3014633   bits: 23/22
c ---[3626]---> Adder-cost: 1496   maxlim: 3014633   bits: 23/22
c ---[3624]---> Adder-cost: 1496   maxlim: 3014633   bits: 23/22
c ---[3622]---> Adder-cost: 1496   maxlim: 3012073   bits: 23/22
c ---[3620]---> Adder-cost: 1496   maxlim: 3014633   bits: 23/22
c ---[3618]---> Adder-cost: 1496   maxlim: 3009385   bits: 23/22
c ---[3616]---> Adder-cost: 1496   maxlim: 2943593   bits: 23/22
c ---[3614]---> Adder-cost: 1496   maxlim: 3012585   bits: 23/22
c ---[3612]---> Adder-cost: 1496   maxlim: 3009129   bits: 23/22
c ---[3610]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[3608]---> Adder-cost: 1496   maxlim: 3011561   bits: 23/22
c ---[3606]---> Adder-cost: 1496   maxlim: 3014633   bits: 23/22
c ---[3604]---> Adder-cost: 1496   maxlim: 3012329   bits: 23/22
c ---[3602]---> Adder-cost: 1496   maxlim: 3012329   bits: 23/22
c ---[3600]---> Adder-cost: 1496   maxlim: 3014633   bits: 23/22
c ---[3598]---> Adder-cost: 1496   maxlim: 3009001   bits: 23/22
c ---[3596]---> Adder-cost: 1496   maxlim: 3012073   bits: 23/22
c ---[3594]---> Adder-cost: 1496   maxlim: 3014633   bits: 23/22
c ---[3592]---> Adder-cost: 1496   maxlim: 3011945   bits: 23/22
c ---[3590]---> Adder-cost: 1496   maxlim: 3009897   bits: 23/22
c ---[3588]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[3586]---> Adder-cost: 1496   maxlim: 3014633   bits: 23/22
c ---[3584]---> Adder-cost: 1496   maxlim: 3014633   bits: 23/22
c ---[3582]---> Adder-cost: 1496   maxlim: 3011689   bits: 23/22
c ---[3580]---> Adder-cost: 1496   maxlim: 3009641   bits: 23/22
c ---[3578]---> Adder-cost: 1496   maxlim: 3014633   bits: 23/22
c ---[3576]---> Adder-cost: 1496   maxlim: 3011561   bits: 23/22
c ---[3574]---> Adder-cost: 1496   maxlim: 2943977   bits: 23/22
c ---[3572]---> Adder-cost: 1496   maxlim: 3014633   bits: 23/22
c ---[3570]---> Adder-cost: 1496   maxlim: 3009897   bits: 23/22
c ---[3568]---> Adder-cost: 1496   maxlim: 3014633   bits: 23/22
c ---[3566]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[3564]---> Adder-cost: 1496   maxlim: 3009513   bits: 23/22
c ---[3562]---> Adder-cost: 1496   maxlim: 3012073   bits: 23/22
c ---[3560]---> Adder-cost: 1496   maxlim: 3009001   bits: 23/22
c ---[3558]---> Adder-cost: 1490   maxlim: 2878057   bits: 23/22
c ---[3556]---> Adder-cost: 1496   maxlim: 3014633   bits: 23/22
c ---[3554]---> Adder-cost: 1496   maxlim: 3014633   bits: 23/22
c ---[3552]---> Adder-cost: 1496   maxlim: 3014633   bits: 23/22
c ---[3550]---> Adder-cost: 1496   maxlim: 3014633   bits: 23/22
c ---[3548]---> Adder-cost: 1496   maxlim: 3012585   bits: 23/22
c ---[3546]---> Adder-cost: 1496   maxlim: 3014633   bits: 23/22
c ---[3544]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[3542]---> Adder-cost: 1496   maxlim: 3007081   bits: 23/22
c ---[3540]---> Adder-cost: 1496   maxlim: 3014633   bits: 23/22
c ---[3538]---> Adder-cost: 1496   maxlim: 3014633   bits: 23/22
c ---[3536]---> Adder-cost: 1496   maxlim: 3014633   bits: 23/22
c ---[3534]---> Adder-cost: 1496   maxlim: 3009257   bits: 23/22
c ---[3532]---> Adder-cost: 1496   maxlim: 3014633   bits: 23/22
c ---[3530]---> Adder-cost: 1496   maxlim: 3014633   bits: 23/22
c ---[3528]---> Adder-cost: 1496   maxlim: 3011689   bits: 23/22
c ---[3526]---> Adder-cost: 1496   maxlim: 3011561   bits: 23/22
c ---[3524]---> Adder-cost: 1496   maxlim: 2944233   bits: 23/22
c ---[3522]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[3520]---> Adder-cost: 1496   maxlim: 3012201   bits: 23/22
c ---[3518]---> Adder-cost: 1496   maxlim: 3010025   bits: 23/22
c ---[3516]---> Adder-cost: 1496   maxlim: 3014633   bits: 23/22
c ---[3514]---> Adder-cost: 1496   maxlim: 3012073   bits: 23/22
c ---[3512]---> Adder-cost: 1496   maxlim: 3006953   bits: 23/22
c ---[3510]---> Adder-cost: 1496   maxlim: 3007337   bits: 23/22
c ---[3508]---> Adder-cost: 1496   maxlim: 3014633   bits: 23/22
c ---[3506]---> Adder-cost: 1496   maxlim: 3011689   bits: 23/22
c ---[3504]---> Adder-cost: 1496   maxlim: 3009513   bits: 23/22
c ---[3502]---> Adder-cost: 1496   maxlim: 3014633   bits: 23/22
c ---[3500]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[3498]---> Adder-cost: 1496   maxlim: 3014633   bits: 23/22
c ---[3496]---> Adder-cost: 1496   maxlim: 3012585   bits: 23/22
c ---[3494]---> Adder-cost: 1496   maxlim: 3009257   bits: 23/22
c ---[3492]---> Adder-cost: 1496   maxlim: 3014633   bits: 23/22
c ---[3490]---> Adder-cost: 1496   maxlim: 3011689   bits: 23/22
c ---[3488]---> Adder-cost: 1496   maxlim: 3014633   bits: 23/22
c ---[3486]---> Adder-cost: 1496   maxlim: 3014633   bits: 23/22
c ---[3484]---> Adder-cost: 1496   maxlim: 2943849   bits: 23/22
c ---[3482]---> Adder-cost: 1496   maxlim: 2944489   bits: 23/22
c ---[3480]---> Adder-cost: 1496   maxlim: 3009129   bits: 23/22
c ---[3478]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[3476]---> Adder-cost: 1496   maxlim: 3011689   bits: 23/22
c ---[3474]---> Adder-cost: 1496   maxlim: 3009385   bits: 23/22
c ---[3472]---> Adder-cost: 1496   maxlim: 3012457   bits: 23/22
c ---[3470]---> Adder-cost: 1496   maxlim: 3014633   bits: 23/22
c ---[3468]---> Adder-cost: 1496   maxlim: 3009769   bits: 23/22
c ---[3466]---> Adder-cost: 1496   maxlim: 3014633   bits: 23/22
c ---[3464]---> Adder-cost: 1496   maxlim: 3014633   bits: 23/22
c ---[3462]---> Adder-cost: 1496   maxlim: 3011945   bits: 23/22
c ---[3460]---> Adder-cost: 1496   maxlim: 3011945   bits: 23/22
c ---[3458]---> Adder-cost: 1496   maxlim: 3012457   bits: 23/22
c ---[3456]---> BDD-cost:   63
c ---[3454]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[3452]---> Adder-cost: 1496   maxlim: 3012585   bits: 23/22
c ---[3450]---> Adder-cost: 1266   maxlim: 3012585   bits: 23/22
c ---[3448]---> Adder-cost: 1496   maxlim: 2944105   bits: 23/22
c ---[3446]---> Adder-cost: 1496   maxlim: 3011817   bits: 23/22
c ---[3444]---> Adder-cost: 1496   maxlim: 3014633   bits: 23/22
c ---[3442]---> Adder-cost: 1250   maxlim: 3011945   bits: 23/22
c ---[3440]---> Adder-cost: 1496   maxlim: 3011689   bits: 23/22
c ---[3438]---> Adder-cost: 1496   maxlim: 3012585   bits: 23/22
c ---[3436]---> Adder-cost: 1184   maxlim: 3011689   bits: 23/22
c ---[3434]---> Adder-cost: 1244   maxlim: 3012457   bits: 23/22
c ---[3432]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[3430]---> Adder-cost: 1496   maxlim: 3014633   bits: 23/22
c ---[3428]---> Adder-cost: 1496   maxlim: 3011689   bits: 23/22
c ---[3426]---> Adder-cost: 1496   maxlim: 3011689   bits: 23/22
c ---[3424]---> Adder-cost: 1242   maxlim: 3012073   bits: 23/22
c ---[3422]---> Adder-cost: 1496   maxlim: 3014633   bits: 23/22
c ---[3420]---> Adder-cost: 1496   maxlim: 3012457   bits: 23/22
c ---[3418]---> Adder-cost: 1496   maxlim: 3007209   bits: 23/22
c ---[3416]---> Adder-cost: 1172   maxlim: 3012457   bits: 23/22
c ---[3414]---> Adder-cost: 1496   maxlim: 3014633   bits: 23/22
c ---[3412]---> Adder-cost: 1496   maxlim: 3012073   bits: 23/22
c ---[3410]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[3408]---> Adder-cost: 1496   maxlim: 3014633   bits: 23/22
c ---[3406]---> Adder-cost: 1496   maxlim: 3012457   bits: 23/22
c ---[3404]---> Adder-cost: 1244   maxlim: 3011561   bits: 23/22
c ---[3402]---> Adder-cost: 1496   maxlim: 3014633   bits: 23/22
c ---[3400]---> Adder-cost: 1496   maxlim: 3014633   bits: 23/22
c ---[3398]---> Adder-cost: 1496   maxlim: 3012457   bits: 23/22
c ---[3396]---> Adder-cost: 1496   maxlim: 2943721   bits: 23/22
c ---[3394]---> Adder-cost: 1246   maxlim: 3007209   bits: 23/22
c ---[3392]---> Adder-cost: 1496   maxlim: 3012201   bits: 23/22
c ---[3390]---> Adder-cost: 1496   maxlim: 3011817   bits: 23/22
c ---[3388]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[3386]---> Adder-cost: 1496   maxlim: 3014633   bits: 23/22
c ---[3384]---> Adder-cost: 1178   maxlim: 3011561   bits: 23/22
c ---[3382]---> Adder-cost: 1230   maxlim: 2943721   bits: 23/22
c ---[3380]---> Adder-cost: 1496   maxlim: 3014633   bits: 23/22
c ---[3378]---> Adder-cost: 1452   maxlim: 3012585   bits: 23/22
c ---[3376]---> Adder-cost: 1496   maxlim: 3014633   bits: 23/22
c ---[3374]---> Adder-cost: 1496   maxlim: 3009129   bits: 23/22
c ---[3372]---> Adder-cost: 1496   maxlim: 3014633   bits: 23/22
c ---[3370]---> Adder-cost: 1238   maxlim: 3011561   bits: 23/22
c ---[3368]---> Adder-cost: 1496   maxlim: 3010025   bits: 23/22
c ---[3366]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[3364]---> Adder-cost: 1496   maxlim: 3014633   bits: 23/22
c ---[3362]---> Adder-cost: 1496   maxlim: 3012585   bits: 23/22
c ---[3360]---> Adder-cost: 1178   maxlim: 3011561   bits: 23/22
c ---[3358]---> Adder-cost: 1496   maxlim: 3009385   bits: 23/22
c ---[3356]---> Adder-cost: 1496   maxlim: 3009385   bits: 23/22
c ---[3354]---> Adder-cost: 1496   maxlim: 3014633   bits: 23/22
c ---[3352]---> Adder-cost: 1244   maxlim: 3011561   bits: 23/22
c ---[3350]---> Adder-cost: 1496   maxlim: 3014633   bits: 23/22
c ---[3348]---> Adder-cost: 1496   maxlim: 3014633   bits: 23/22
c ---[3346]---> Adder-cost: 1496   maxlim: 3014633   bits: 23/22
c ---[3344]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[3342]---> Adder-cost: 1496   maxlim: 3014633   bits: 23/22
c ---[3340]---> Adder-cost: 1496   maxlim: 3007465   bits: 23/22
c ---[3338]---> Adder-cost: 1496   maxlim: 3009769   bits: 23/22
c ---[3336]---> Adder-cost: 1250   maxlim: 3006569   bits: 23/22
c ---[3334]---> Adder-cost: 1496   maxlim: 3012201   bits: 23/22
c ---[3332]---> Adder-cost: 1236   maxlim: 3009897   bits: 23/22
c ---[3330]---> Adder-cost: 1496   maxlim: 3011689   bits: 23/22
c ---[3328]---> Adder-cost: 1462   maxlim: 3011689   bits: 23/22
c ---[3326]---> Adder-cost: 1496   maxlim: 3014633   bits: 23/22
c ---[3324]---> Adder-cost: 1246   maxlim: 3009257   bits: 23/22
c ---[3322]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[3320]---> Adder-cost: 1482   maxlim: 3012585   bits: 23/22
c ---[3318]---> Adder-cost: 1496   maxlim: 3011689   bits: 23/22
c ---[3316]---> Adder-cost: 1182   maxlim: 3004905   bits: 23/22
c ---[3314]---> Adder-cost: 1496   maxlim: 3011689   bits: 23/22
c ---[3312]---> Adder-cost: 1496   maxlim: 3014633   bits: 23/22
c ---[3310]---> Adder-cost: 1496   maxlim: 3014633   bits: 23/22
c ---[3308]---> Adder-cost: 1496   maxlim: 3011561   bits: 23/22
c ---[3306]---> Adder-cost: 1244   maxlim: 3012073   bits: 23/22
c ---[3304]---> Adder-cost: 1496   maxlim: 3009385   bits: 23/22
c ---[3302]---> Adder-cost: 1496   maxlim: 3012073   bits: 23/22
c ---[3300]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[3298]---> Adder-cost: 1238   maxlim: 3011561   bits: 23/22
c ---[3296]---> Adder-cost: 1496   maxlim: 3009513   bits: 23/22
c ---[3294]---> Adder-cost: 1496   maxlim: 3011689   bits: 23/22
c ---[3292]---> Adder-cost: 1496   maxlim: 3014633   bits: 23/22
c ---[3290]---> Adder-cost: 1496   maxlim: 3014633   bits: 23/22
c ---[3288]---> Adder-cost: 1184   maxlim: 3009641   bits: 23/22
c ---[3286]---> Adder-cost: 1496   maxlim: 3012073   bits: 23/22
c ---[3284]---> Adder-cost: 1496   maxlim: 3014633   bits: 23/22
c ---[3282]---> Adder-cost: 1228   maxlim: 3009129   bits: 23/22
c ---[3280]---> Adder-cost: 1496   maxlim: 3012073   bits: 23/22
c ---[3278]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[3276]---> Adder-cost: 1428   maxlim: 3012457   bits: 23/22
c ---[3274]---> Adder-cost: 1250   maxlim: 3012457   bits: 23/22
c ---[3272]---> Adder-cost: 1496   maxlim: 3014633   bits: 23/22
c ---[3270]---> Adder-cost: 1496   maxlim: 3012073   bits: 23/22
c ---[3268]---> Adder-cost: 1496   maxlim: 3012201   bits: 23/22
c ---[3266]---> Adder-cost: 1496   maxlim: 3014633   bits: 23/22
c ---[3264]---> Adder-cost: 1180   maxlim: 3004393   bits: 23/22
c ---[3262]---> Adder-cost: 1496   maxlim: 3014633   bits: 23/22
c ---[3260]---> Adder-cost: 1496   maxlim: 3014633   bits: 23/22
c ---[3258]---> Adder-cost: 1496   maxlim: 3014633   bits: 23/22
c ---[3256]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[3254]---> Adder-cost: 1496   maxlim: 3009513   bits: 23/22
c ---[3252]---> Adder-cost: 1496   maxlim: 3014633   bits: 23/22
c ---[3250]---> Adder-cost: 1496   maxlim: 3009513   bits: 23/22
c ---[3248]---> Adder-cost: 1266   maxlim: 3012585   bits: 23/22
c ---[3246]---> Adder-cost: 1496   maxlim: 3012201   bits: 23/22
c ---[3244]---> Adder-cost: 1496   maxlim: 3014633   bits: 23/22
c ---[3242]---> Adder-cost: 1496   maxlim: 3014633   bits: 23/22
c ---[3240]---> Adder-cost: 1496   maxlim: 3014633   bits: 23/22
c ---[3238]---> Adder-cost: 1496   maxlim: 3012329   bits: 23/22
c ---[3236]---> Adder-cost: 1250   maxlim: 3012457   bits: 23/22
c ---[3234]---> BDD-cost:   63
c ---[3232]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[3230]---> Adder-cost: 1496   maxlim: 3014633   bits: 23/22
c ---[3228]---> Adder-cost: 1244   maxlim: 3012329   bits: 23/22
c ---[3226]---> Adder-cost: 1496   maxlim: 3012073   bits: 23/22
c ---[3224]---> Adder-cost: 1428   maxlim: 3009001   bits: 23/22
c ---[3222]---> Adder-cost: 1252   maxlim: 2943977   bits: 23/22
c ---[3220]---> Adder-cost: 1496   maxlim: 3011945   bits: 23/22
c ---[3218]---> Adder-cost: 1496   maxlim: 3012329   bits: 23/22
c ---[3216]---> Adder-cost: 1496   maxlim: 3014633   bits: 23/22
c ---[3214]---> Adder-cost: 1176   maxlim: 3012073   bits: 23/22
c ---[3212]---> Adder-cost: 1496   maxlim: 3014633   bits: 23/22
c ---[3210]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[3208]---> Adder-cost: 1496   maxlim: 3014633   bits: 23/22
c ---[3206]---> Adder-cost: 1474   maxlim: 3012585   bits: 23/22
c ---[3204]---> Adder-cost: 1496   maxlim: 3011561   bits: 23/22
c ---[3202]---> Adder-cost: 1496   maxlim: 3014633   bits: 23/22
c ---[3200]---> Adder-cost: 1496   maxlim: 3014633   bits: 23/22
c ---[3198]---> Adder-cost: 1236   maxlim: 3012201   bits: 23/22
c ---[3196]---> Adder-cost: 1496   maxlim: 3012329   bits: 23/22
c ---[3194]---> Adder-cost: 1496   maxlim: 3014633   bits: 23/22
c ---[3192]---> Adder-cost: 1496   maxlim: 3012457   bits: 23/22
c ---[3190]---> Adder-cost: 1250   maxlim: 3011689   bits: 23/22
c ---[3188]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[3186]---> Adder-cost: 1496   maxlim: 3014633   bits: 23/22
c ---[3184]---> Adder-cost: 1496   maxlim: 3011689   bits: 23/22
c ---[3182]---> Adder-cost: 1496   maxlim: 3009001   bits: 23/22
c ---[3180]---> Adder-cost: 1180   maxlim: 3009257   bits: 23/22
c ---[3178]---> Adder-cost: 1236   maxlim: 3009001   bits: 23/22
c ---[3176]---> Adder-cost: 1496   maxlim: 3014633   bits: 23/22
c ---[3174]---> Adder-cost: 1496   maxlim: 3014633   bits: 23/22
c ---[3172]---> Adder-cost: 1496   maxlim: 3014633   bits: 23/22
c ---[3170]---> Adder-cost: 1496   maxlim: 3006697   bits: 23/22
c ---[3168]---> Adder-cost: 1496   maxlim: 3014633   bits: 23/22
c ---[3166]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[3164]---> Adder-cost: 1250   maxlim: 3012457   bits: 23/22
c ---[3162]---> Adder-cost: 1496   maxlim: 3009385   bits: 23/22
c ---[3160]---> Adder-cost: 1496   maxlim: 3014633   bits: 23/22
c ---[3158]---> Adder-cost: 1496   maxlim: 3014633   bits: 23/22
c ---[3156]---> Adder-cost: 1496   maxlim: 3014633   bits: 23/22
c ---[3154]---> Adder-cost: 1496   maxlim: 2941033   bits: 23/22
c ---[3152]---> Adder-cost: 1496   maxlim: 3014633   bits: 23/22
c ---[3150]---> Adder-cost: 1184   maxlim: 2944361   bits: 23/22
c ---[3148]---> Adder-cost: 1496   maxlim: 3011817   bits: 23/22
c ---[3146]---> Adder-cost: 1496   maxlim: 3014633   bits: 23/22
c ---[3144]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[3142]---> Adder-cost: 1496   maxlim: 3012073   bits: 23/22
c ---[3140]---> Adder-cost: 1496   maxlim: 3014633   bits: 23/22
c ---[3138]---> Adder-cost: 1496   maxlim: 3014633   bits: 23/22
c ---[3136]---> Adder-cost: 1496   maxlim: 3012201   bits: 23/22
c ---[3134]---> Adder-cost: 1228   maxlim: 3007337   bits: 23/22
c ---[3132]---> Adder-cost: 1496   maxlim: 3012329   bits: 23/22
c ---[3130]---> Adder-cost: 1496   maxlim: 3009769   bits: 23/22
c ---[3129]---> BDD-cost:  131
c ---[3128]---> BDD-cost:   24
c ---[3127]---> BDD-cost:  131
c ---[3125]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[3124]---> BDD-cost:   24
c ---[3123]---> BDD-cost:  131
c ---[3122]---> BDD-cost:   24
c ---[3121]---> BDD-cost:  131
c ---[3120]---> BDD-cost:   24
c ---[3119]---> BDD-cost:  131
c ---[3118]---> BDD-cost:   24
c ---[3117]---> BDD-cost:  131
c ---[3116]---> BDD-cost:   24
c ---[3115]---> BDD-cost:  131
c ---[3113]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[3112]---> BDD-cost:   24
c ---[3111]---> BDD-cost:  131
c ---[3110]---> BDD-cost:   24
c ---[3109]---> BDD-cost:  131
c ---[3108]---> BDD-cost:   24
c ---[3107]---> BDD-cost:  131
c ---[3106]---> BDD-cost:   24
c ---[3105]---> BDD-cost:  131
c ---[3104]---> BDD-cost:   24
c ---[3103]---> BDD-cost:  131
c ---[3101]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[3100]---> BDD-cost:   24
c ---[3099]---> BDD-cost:  131
c ---[3098]---> BDD-cost:   24
c ---[3097]---> BDD-cost:  131
c ---[3096]---> BDD-cost:   24
c ---[3095]---> BDD-cost:  131
c ---[3094]---> BDD-cost:   24
c ---[3093]---> BDD-cost:  131
c ---[3092]---> BDD-cost:   24
c ---[3091]---> BDD-cost:  131
c ---[3089]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[3088]---> BDD-cost:   24
c ---[3087]---> BDD-cost:  131
c ---[3086]---> BDD-cost:   24
c ---[3085]---> BDD-cost:  131
c ---[3084]---> BDD-cost:   24
c ---[3083]---> BDD-cost:  131
c ---[3082]---> BDD-cost:   24
c ---[3081]---> BDD-cost:  131
c ---[3080]---> BDD-cost:   24
c ---[3079]---> BDD-cost:  131
c ---[3077]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[3076]---> BDD-cost:   24
c ---[3075]---> BDD-cost:  131
c ---[3074]---> BDD-cost:   24
c ---[3073]---> BDD-cost:  131
c ---[3072]---> BDD-cost:   24
c ---[3071]---> BDD-cost:  131
c ---[3070]---> BDD-cost:   24
c ---[3069]---> BDD-cost:  131
c ---[3068]---> BDD-cost:   24
c ---[3067]---> BDD-cost:  131
c ---[3065]---> BDD-cost:   63
c ---[3063]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[3062]---> BDD-cost:   24
c ---[3061]---> BDD-cost:  131
c ---[3060]---> BDD-cost:   24
c ---[3059]---> BDD-cost:  131
c ---[3058]---> BDD-cost:   24
c ---[3057]---> BDD-cost:  131
c ---[3056]---> BDD-cost:   24
c ---[3055]---> BDD-cost:  131
c ---[3054]---> BDD-cost:   24
c ---[3053]---> BDD-cost:  131
c ---[3051]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[3050]---> BDD-cost:   24
c ---[3049]---> BDD-cost:  131
c ---[3048]---> BDD-cost:   24
c ---[3047]---> BDD-cost:  131
c ---[3046]---> BDD-cost:   24
c ---[3045]---> BDD-cost:  131
c ---[3044]---> BDD-cost:   24
c ---[3043]---> BDD-cost:  131
c ---[3042]---> BDD-cost:   24
c ---[3041]---> BDD-cost:  131
c ---[3039]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[3038]---> BDD-cost:   24
c ---[3037]---> BDD-cost:  131
c ---[3036]---> BDD-cost:   24
c ---[3035]---> BDD-cost:  131
c ---[3034]---> BDD-cost:   24
c ---[3033]---> BDD-cost:  131
c ---[3032]---> BDD-cost:   24
c ---[3031]---> BDD-cost:  131
c ---[3030]---> BDD-cost:   24
c ---[3029]---> BDD-cost:  131
c ---[3027]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[3026]---> BDD-cost:   24
c ---[3025]---> BDD-cost:  131
c ---[3024]---> BDD-cost:   24
c ---[3023]---> BDD-cost:  131
c ---[3022]---> BDD-cost:   24
c ---[3021]---> BDD-cost:  131
c ---[3020]---> BDD-cost:   24
c ---[3019]---> BDD-cost:  131
c ---[3018]---> BDD-cost:   24
c ---[3017]---> BDD-cost:  131
c ---[3015]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[3014]---> BDD-cost:   24
c ---[3013]---> BDD-cost:  131
c ---[3012]---> BDD-cost:   24
c ---[3011]---> BDD-cost:  131
c ---[3010]---> BDD-cost:   24
c ---[3009]---> BDD-cost:  131
c ---[3008]---> BDD-cost:   24
c ---[3007]---> BDD-cost:  131
c ---[3006]---> BDD-cost:   24
c ---[3005]---> BDD-cost:  131
c ---[3003]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[3002]---> BDD-cost:   24
c ---[3001]---> BDD-cost:  131
c ---[3000]---> BDD-cost:   24
c ---[2999]---> BDD-cost:  131
c ---[2998]---> BDD-cost:   24
c ---[2997]---> BDD-cost:  131
c ---[2996]---> BDD-cost:   24
c ---[2995]---> BDD-cost:  131
c ---[2994]---> BDD-cost:   24
c ---[2993]---> BDD-cost:  131
c ---[2991]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[2990]---> BDD-cost:   24
c ---[2989]---> BDD-cost:  131
c ---[2988]---> BDD-cost:   24
c ---[2987]---> BDD-cost:  131
c ---[2986]---> BDD-cost:   24
c ---[2985]---> BDD-cost:  131
c ---[2984]---> BDD-cost:   24
c ---[2983]---> BDD-cost:  131
c ---[2982]---> BDD-cost:   24
c ---[2981]---> BDD-cost:  131
c ---[2979]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[2978]---> BDD-cost:   24
c ---[2977]---> BDD-cost:  131
c ---[2976]---> BDD-cost:   24
c ---[2975]---> BDD-cost:  131
c ---[2974]---> BDD-cost:   24
c ---[2973]---> BDD-cost:  131
c ---[2972]---> BDD-cost:   24
c ---[2971]---> BDD-cost:  131
c ---[2970]---> BDD-cost:   24
c ---[2969]---> BDD-cost:  131
c ---[2967]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[2966]---> BDD-cost:   24
c ---[2965]---> BDD-cost:  131
c ---[2964]---> BDD-cost:   24
c ---[2963]---> BDD-cost:  131
c ---[2962]---> BDD-cost:   24
c ---[2961]---> BDD-cost:  131
c ---[2960]---> BDD-cost:   24
c ---[2959]---> BDD-cost:  131
c ---[2958]---> BDD-cost:   24
c ---[2957]---> BDD-cost:  131
c ---[2955]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[2954]---> BDD-cost:   24
c ---[2953]---> BDD-cost:  131
c ---[2952]---> BDD-cost:   24
c ---[2951]---> BDD-cost:  131
c ---[2950]---> BDD-cost:   24
c ---[2949]---> BDD-cost:  131
c ---[2948]---> BDD-cost:   24
c ---[2947]---> BDD-cost:  131
c ---[2946]---> BDD-cost:   24
c ---[2945]---> BDD-cost:  131
c ---[2943]---> BDD-cost:   63
c ---[2941]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[2940]---> BDD-cost:   24
c ---[2939]---> BDD-cost:  131
c ---[2938]---> BDD-cost:   24
c ---[2937]---> BDD-cost:  131
c ---[2936]---> BDD-cost:   24
c ---[2935]---> BDD-cost:  131
c ---[2934]---> BDD-cost:   24
c ---[2933]---> BDD-cost:  131
c ---[2932]---> BDD-cost:   24
c ---[2931]---> BDD-cost:  131
c ---[2929]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[2928]---> BDD-cost:   24
c ---[2927]---> BDD-cost:  131
c ---[2926]---> BDD-cost:   24
c ---[2925]---> BDD-cost:  131
c ---[2924]---> BDD-cost:   24
c ---[2923]---> BDD-cost:  131
c ---[2922]---> BDD-cost:   24
c ---[2921]---> BDD-cost:  131
c ---[2920]---> BDD-cost:   24
c ---[2919]---> BDD-cost:  131
c ---[2917]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[2916]---> BDD-cost:   24
c ---[2915]---> BDD-cost:  131
c ---[2914]---> BDD-cost:   24
c ---[2913]---> BDD-cost:  131
c ---[2912]---> BDD-cost:   24
c ---[2911]---> BDD-cost:  131
c ---[2910]---> BDD-cost:   24
c ---[2909]---> BDD-cost:  131
c ---[2908]---> BDD-cost:   24
c ---[2907]---> BDD-cost:  131
c ---[2905]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[2904]---> BDD-cost:   24
c ---[2903]---> BDD-cost:  131
c ---[2902]---> BDD-cost:   24
c ---[2901]---> BDD-cost:  131
c ---[2900]---> BDD-cost:   24
c ---[2899]---> BDD-cost:  131
c ---[2898]---> BDD-cost:   24
c ---[2897]---> BDD-cost:  131
c ---[2896]---> BDD-cost:   24
c ---[2895]---> BDD-cost:  131
c ---[2893]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[2892]---> BDD-cost:   24
c ---[2891]---> BDD-cost:  131
c ---[2890]---> BDD-cost:   24
c ---[2889]---> BDD-cost:  131
c ---[2888]---> BDD-cost:   24
c ---[2887]---> BDD-cost:  131
c ---[2886]---> BDD-cost:   24
c ---[2885]---> BDD-cost:  131
c ---[2884]---> BDD-cost:   24
c ---[2883]---> BDD-cost:  131
c ---[2881]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[2880]---> BDD-cost:   24
c ---[2879]---> BDD-cost:  131
c ---[2878]---> BDD-cost:   24
c ---[2877]---> BDD-cost:  131
c ---[2876]---> BDD-cost:   24
c ---[2875]---> BDD-cost:  131
c ---[2874]---> BDD-cost:   24
c ---[2873]---> BDD-cost:  131
c ---[2872]---> BDD-cost:   24
c ---[2871]---> BDD-cost:  131
c ---[2869]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[2868]---> BDD-cost:   24
c ---[2867]---> BDD-cost:  131
c ---[2866]---> BDD-cost:   24
c ---[2865]---> BDD-cost:  131
c ---[2864]---> BDD-cost:   24
c ---[2863]---> BDD-cost:  131
c ---[2862]---> BDD-cost:   24
c ---[2861]---> BDD-cost:  131
c ---[2860]---> BDD-cost:   24
c ---[2859]---> BDD-cost:  131
c ---[2857]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[2856]---> BDD-cost:   24
c ---[2855]---> BDD-cost:  131
c ---[2854]---> BDD-cost:   24
c ---[2853]---> BDD-cost:  131
c ---[2852]---> BDD-cost:   24
c ---[2851]---> BDD-cost:  131
c ---[2850]---> BDD-cost:   24
c ---[2849]---> BDD-cost:  131
c ---[2848]---> BDD-cost:   24
c ---[2847]---> BDD-cost:  131
c ---[2845]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[2844]---> BDD-cost:   24
c ---[2843]---> BDD-cost:  131
c ---[2842]---> BDD-cost:   24
c ---[2841]---> BDD-cost:  131
c ---[2840]---> BDD-cost:   24
c ---[2839]---> BDD-cost:  131
c ---[2838]---> BDD-cost:   24
c ---[2837]---> BDD-cost:  131
c ---[2836]---> BDD-cost:   24
c ---[2835]---> BDD-cost:  131
c ---[2833]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[2832]---> BDD-cost:   24
c ---[2831]---> BDD-cost:  131
c ---[2830]---> BDD-cost:   24
c ---[2829]---> BDD-cost:  131
c ---[2828]---> BDD-cost:   24
c ---[2827]---> BDD-cost:  131
c ---[2826]---> BDD-cost:   24
c ---[2825]---> BDD-cost:  131
c ---[2824]---> BDD-cost:   24
c ---[2823]---> BDD-cost:  131
c ---[2821]---> BDD-cost:   63
c ---[2819]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[2818]---> BDD-cost:   24
c ---[2817]---> BDD-cost:  131
c ---[2816]---> BDD-cost:   24
c ---[2815]---> BDD-cost:  131
c ---[2814]---> BDD-cost:   24
c ---[2813]---> BDD-cost:  131
c ---[2812]---> BDD-cost:   24
c ---[2811]---> BDD-cost:  131
c ---[2810]---> BDD-cost:   24
c ---[2809]---> BDD-cost:  131
c ---[2807]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[2806]---> BDD-cost:   24
c ---[2805]---> BDD-cost:  131
c ---[2804]---> BDD-cost:   24
c ---[2803]---> BDD-cost:  131
c ---[2802]---> BDD-cost:   24
c ---[2801]---> BDD-cost:  131
c ---[2800]---> BDD-cost:   24
c ---[2799]---> BDD-cost:  131
c ---[2798]---> BDD-cost:   24
c ---[2797]---> BDD-cost:  131
c ---[2795]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[2794]---> BDD-cost:   24
c ---[2793]---> BDD-cost:  131
c ---[2792]---> BDD-cost:   24
c ---[2791]---> BDD-cost:  131
c ---[2790]---> BDD-cost:   24
c ---[2789]---> BDD-cost:  131
c ---[2788]---> BDD-cost:   24
c ---[2787]---> BDD-cost:  131
c ---[2786]---> BDD-cost:   24
c ---[2785]---> BDD-cost:  131
c ---[2783]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[2782]---> BDD-cost:   24
c ---[2781]---> BDD-cost:  131
c ---[2780]---> BDD-cost:   24
c ---[2779]---> BDD-cost:  131
c ---[2778]---> BDD-cost:   24
c ---[2777]---> BDD-cost:  131
c ---[2776]---> BDD-cost:   24
c ---[2775]---> BDD-cost:  131
c ---[2774]---> BDD-cost:   24
c ---[2773]---> BDD-cost:  131
c ---[2771]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[2770]---> BDD-cost:   24
c ---[2769]---> BDD-cost:  131
c ---[2768]---> BDD-cost:   24
c ---[2767]---> BDD-cost:  131
c ---[2766]---> BDD-cost:   24
c ---[2765]---> BDD-cost:  131
c ---[2764]---> BDD-cost:   24
c ---[2763]---> BDD-cost:  131
c ---[2762]---> BDD-cost:   24
c ---[2761]---> BDD-cost:  131
c ---[2759]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[2758]---> BDD-cost:   24
c ---[2757]---> BDD-cost:  131
c ---[2756]---> BDD-cost:   24
c ---[2755]---> BDD-cost:  131
c ---[2754]---> BDD-cost:   24
c ---[2753]---> BDD-cost:  131
c ---[2752]---> BDD-cost:   24
c ---[2751]---> BDD-cost:  131
c ---[2750]---> BDD-cost:   24
c ---[2749]---> BDD-cost:  131
c ---[2747]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[2746]---> BDD-cost:   24
c ---[2745]---> BDD-cost:  131
c ---[2744]---> BDD-cost:   24
c ---[2743]---> BDD-cost:  131
c ---[2742]---> BDD-cost:   24
c ---[2741]---> BDD-cost:  131
c ---[2740]---> BDD-cost:   24
c ---[2739]---> BDD-cost:  131
c ---[2738]---> BDD-cost:   24
c ---[2737]---> BDD-cost:  131
c ---[2735]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[2734]---> BDD-cost:   24
c ---[2733]---> BDD-cost:  131
c ---[2732]---> BDD-cost:   24
c ---[2731]---> BDD-cost:  131
c ---[2730]---> BDD-cost:   24
c ---[2729]---> BDD-cost:  131
c ---[2728]---> BDD-cost:   24
c ---[2727]---> BDD-cost:  131
c ---[2726]---> BDD-cost:   24
c ---[2725]---> BDD-cost:  131
c ---[2723]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[2722]---> BDD-cost:   24
c ---[2721]---> BDD-cost:  131
c ---[2720]---> BDD-cost:   24
c ---[2719]---> BDD-cost:  131
c ---[2718]---> BDD-cost:   24
c ---[2717]---> BDD-cost:  131
c ---[2716]---> BDD-cost:   24
c ---[2715]---> BDD-cost:  131
c ---[2714]---> BDD-cost:   24
c ---[2713]---> BDD-cost:  131
c ---[2711]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[2710]---> BDD-cost:   24
c ---[2709]---> BDD-cost:  131
c ---[2708]---> BDD-cost:   24
c ---[2707]---> BDD-cost:  131
c ---[2706]---> BDD-cost:   24
c ---[2705]---> BDD-cost:  131
c ---[2704]---> BDD-cost:   24
c ---[2703]---> BDD-cost:  131
c ---[2702]---> BDD-cost:   24
c ---[2701]---> BDD-cost:  131
c ---[2699]---> BDD-cost:   63
c ---[2697]---> BDD-cost:   63
c ---[2695]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[2694]---> BDD-cost:   24
c ---[2693]---> BDD-cost:  131
c ---[2692]---> BDD-cost:   24
c ---[2691]---> BDD-cost:  131
c ---[2690]---> BDD-cost:   24
c ---[2689]---> BDD-cost:  131
c ---[2688]---> BDD-cost:   24
c ---[2687]---> BDD-cost:  131
c ---[2686]---> BDD-cost:   24
c ---[2685]---> BDD-cost:  131
c ---[2683]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[2682]---> BDD-cost:   24
c ---[2681]---> BDD-cost:  131
c ---[2680]---> BDD-cost:   24
c ---[2679]---> BDD-cost:  131
c ---[2678]---> BDD-cost:   24
c ---[2677]---> BDD-cost:  131
c ---[2676]---> BDD-cost:   24
c ---[2675]---> BDD-cost:  131
c ---[2674]---> BDD-cost:   24
c ---[2673]---> BDD-cost:  131
c ---[2671]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[2670]---> BDD-cost:   24
c ---[2669]---> BDD-cost:  131
c ---[2668]---> BDD-cost:   24
c ---[2667]---> BDD-cost:  131
c ---[2666]---> BDD-cost:   24
c ---[2665]---> BDD-cost:  131
c ---[2664]---> BDD-cost:   24
c ---[2663]---> BDD-cost:  131
c ---[2662]---> BDD-cost:   24
c ---[2661]---> BDD-cost:  131
c ---[2659]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[2658]---> BDD-cost:   24
c ---[2657]---> BDD-cost:  131
c ---[2656]---> BDD-cost:   24
c ---[2655]---> BDD-cost:  131
c ---[2654]---> BDD-cost:   24
c ---[2653]---> BDD-cost:  131
c ---[2652]---> BDD-cost:   24
c ---[2651]---> BDD-cost:  131
c ---[2650]---> BDD-cost:   24
c ---[2649]---> BDD-cost:  131
c ---[2647]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[2646]---> BDD-cost:   24
c ---[2645]---> BDD-cost:  131
c ---[2644]---> BDD-cost:   24
c ---[2643]---> BDD-cost:  131
c ---[2642]---> BDD-cost:   24
c ---[2641]---> BDD-cost:  131
c ---[2640]---> BDD-cost:   24
c ---[2639]---> BDD-cost:  131
c ---[2638]---> BDD-cost:   24
c ---[2637]---> BDD-cost:  131
c ---[2635]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[2634]---> BDD-cost:   24
c ---[2633]---> BDD-cost:  131
c ---[2632]---> BDD-cost:   24
c ---[2631]---> BDD-cost:  131
c ---[2630]---> BDD-cost:   24
c ---[2629]---> BDD-cost:  131
c ---[2628]---> BDD-cost:   24
c ---[2627]---> BDD-cost:  131
c ---[2626]---> BDD-cost:   24
c ---[2625]---> BDD-cost:  131
c ---[2623]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[2622]---> BDD-cost:   24
c ---[2621]---> BDD-cost:  131
c ---[2620]---> BDD-cost:   24
c ---[2619]---> BDD-cost:  131
c ---[2618]---> BDD-cost:   24
c ---[2617]---> BDD-cost:  131
c ---[2616]---> BDD-cost:   24
c ---[2615]---> BDD-cost:  131
c ---[2614]---> BDD-cost:   24
c ---[2613]---> BDD-cost:  131
c ---[2611]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[2610]---> BDD-cost:   24
c ---[2609]---> BDD-cost:  131
c ---[2608]---> BDD-cost:   24
c ---[2607]---> BDD-cost:  131
c ---[2606]---> BDD-cost:   24
c ---[2605]---> BDD-cost:  131
c ---[2604]---> BDD-cost:   24
c ---[2603]---> BDD-cost:  131
c ---[2602]---> BDD-cost:   24
c ---[2601]---> BDD-cost:  131
c ---[2599]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[2598]---> BDD-cost:   24
c ---[2597]---> BDD-cost:  131
c ---[2596]---> BDD-cost:   24
c ---[2595]---> BDD-cost:  131
c ---[2594]---> BDD-cost:   24
c ---[2593]---> BDD-cost:  131
c ---[2592]---> BDD-cost:   24
c ---[2591]---> BDD-cost:  131
c ---[2590]---> BDD-cost:   24
c ---[2589]---> BDD-cost:  131
c ---[2587]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[2586]---> BDD-cost:   24
c ---[2585]---> BDD-cost:  131
c ---[2584]---> BDD-cost:   24
c ---[2583]---> BDD-cost:  131
c ---[2582]---> BDD-cost:   24
c ---[2581]---> BDD-cost:  131
c ---[2580]---> BDD-cost:   24
c ---[2579]---> BDD-cost:  131
c ---[2578]---> BDD-cost:   24
c ---[2577]---> BDD-cost:  131
c ---[2575]---> BDD-cost:   63
c ---[2573]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[2572]---> BDD-cost:   24
c ---[2571]---> BDD-cost:  131
c ---[2570]---> BDD-cost:   24
c ---[2569]---> BDD-cost:  131
c ---[2568]---> BDD-cost:   24
c ---[2567]---> BDD-cost:  131
c ---[2566]---> BDD-cost:   24
c ---[2565]---> BDD-cost:  131
c ---[2564]---> BDD-cost:   24
c ---[2563]---> BDD-cost:  131
c ---[2561]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[2560]---> BDD-cost:   24
c ---[2559]---> BDD-cost:  131
c ---[2558]---> BDD-cost:   24
c ---[2557]---> BDD-cost:  131
c ---[2556]---> BDD-cost:   24
c ---[2555]---> BDD-cost:  131
c ---[2554]---> BDD-cost:   24
c ---[2553]---> BDD-cost:  131
c ---[2552]---> BDD-cost:   24
c ---[2551]---> BDD-cost:  131
c ---[2549]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[2548]---> BDD-cost:   24
c ---[2547]---> BDD-cost:  131
c ---[2546]---> BDD-cost:   24
c ---[2545]---> BDD-cost:  131
c ---[2544]---> BDD-cost:   24
c ---[2543]---> BDD-cost:  131
c ---[2542]---> BDD-cost:   24
c ---[2541]---> BDD-cost:  131
c ---[2540]---> BDD-cost:   24
c ---[2539]---> BDD-cost:  131
c ---[2537]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[2536]---> BDD-cost:   24
c ---[2535]---> BDD-cost:  131
c ---[2534]---> BDD-cost:   24
c ---[2533]---> BDD-cost:  131
c ---[2532]---> BDD-cost:   24
c ---[2531]---> BDD-cost:  131
c ---[2530]---> BDD-cost:   24
c ---[2529]---> BDD-cost:  131
c ---[2528]---> BDD-cost:   24
c ---[2527]---> BDD-cost:  131
c ---[2525]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[2524]---> BDD-cost:   24
c ---[2523]---> BDD-cost:  131
c ---[2522]---> BDD-cost:   24
c ---[2521]---> BDD-cost:  131
c ---[2520]---> BDD-cost:   24
c ---[2519]---> BDD-cost:  131
c ---[2518]---> BDD-cost:   24
c ---[2517]---> BDD-cost:  131
c ---[2516]---> BDD-cost:   24
c ---[2515]---> BDD-cost:  131
c ---[2513]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[2512]---> BDD-cost:   24
c ---[2511]---> BDD-cost:  131
c ---[2510]---> BDD-cost:   24
c ---[2509]---> BDD-cost:  131
c ---[2508]---> BDD-cost:   24
c ---[2507]---> BDD-cost:  131
c ---[2506]---> BDD-cost:   24
c ---[2505]---> BDD-cost:  131
c ---[2504]---> BDD-cost:   24
c ---[2503]---> BDD-cost:  131
c ---[2501]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[2500]---> BDD-cost:   24
c ---[2499]---> BDD-cost:  131
c ---[2498]---> BDD-cost:   24
c ---[2497]---> BDD-cost:  131
c ---[2496]---> BDD-cost:   24
c ---[2495]---> BDD-cost:  131
c ---[2494]---> BDD-cost:   24
c ---[2493]---> BDD-cost:  131
c ---[2492]---> BDD-cost:   24
c ---[2491]---> BDD-cost:  131
c ---[2489]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[2488]---> BDD-cost:   24
c ---[2487]---> BDD-cost:  131
c ---[2486]---> BDD-cost:   24
c ---[2485]---> BDD-cost:  131
c ---[2484]---> BDD-cost:   24
c ---[2483]---> BDD-cost:  131
c ---[2482]---> BDD-cost:   24
c ---[2481]---> BDD-cost:  131
c ---[2480]---> BDD-cost:   24
c ---[2479]---> BDD-cost:  131
c ---[2477]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[2476]---> BDD-cost:   24
c ---[2475]---> BDD-cost:  131
c ---[2474]---> BDD-cost:   24
c ---[2473]---> BDD-cost:  131
c ---[2472]---> BDD-cost:   24
c ---[2471]---> BDD-cost:  131
c ---[2470]---> BDD-cost:   24
c ---[2469]---> BDD-cost:  131
c ---[2468]---> BDD-cost:   24
c ---[2467]---> BDD-cost:  131
c ---[2465]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[2464]---> BDD-cost:   24
c ---[2463]---> BDD-cost:  131
c ---[2462]---> BDD-cost:   24
c ---[2461]---> BDD-cost:  131
c ---[2460]---> BDD-cost:   24
c ---[2459]---> BDD-cost:  131
c ---[2458]---> BDD-cost:   24
c ---[2457]---> BDD-cost:  131
c ---[2456]---> BDD-cost:   24
c ---[2455]---> BDD-cost:  131
c ---[2453]---> BDD-cost:   63
c ---[2451]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[2450]---> BDD-cost:   24
c ---[2449]---> BDD-cost:  131
c ---[2448]---> BDD-cost:   24
c ---[2447]---> BDD-cost:  131
c ---[2446]---> BDD-cost:   24
c ---[2445]---> BDD-cost:  131
c ---[2444]---> BDD-cost:   24
c ---[2443]---> BDD-cost:  131
c ---[2442]---> BDD-cost:   24
c ---[2441]---> BDD-cost:  131
c ---[2439]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[2438]---> BDD-cost:   24
c ---[2437]---> BDD-cost:  131
c ---[2436]---> BDD-cost:   24
c ---[2435]---> BDD-cost:  131
c ---[2434]---> BDD-cost:   24
c ---[2433]---> BDD-cost:  131
c ---[2432]---> BDD-cost:   24
c ---[2431]---> BDD-cost:  131
c ---[2430]---> BDD-cost:   24
c ---[2429]---> BDD-cost:  131
c ---[2427]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[2426]---> BDD-cost:   24
c ---[2425]---> BDD-cost:  131
c ---[2424]---> BDD-cost:   24
c ---[2423]---> BDD-cost:  131
c ---[2422]---> BDD-cost:   24
c ---[2421]---> BDD-cost:  131
c ---[2420]---> BDD-cost:   24
c ---[2419]---> BDD-cost:  131
c ---[2418]---> BDD-cost:   24
c ---[2417]---> BDD-cost:  131
c ---[2415]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[2414]---> BDD-cost:   24
c ---[2413]---> BDD-cost:  131
c ---[2412]---> BDD-cost:   24
c ---[2411]---> BDD-cost:  131
c ---[2410]---> BDD-cost:   24
c ---[2409]---> BDD-cost:  131
c ---[2408]---> BDD-cost:   24
c ---[2407]---> BDD-cost:  131
c ---[2406]---> BDD-cost:   24
c ---[2405]---> BDD-cost:  131
c ---[2403]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[2402]---> BDD-cost:   24
c ---[2401]---> BDD-cost:  131
c ---[2400]---> BDD-cost:   24
c ---[2399]---> BDD-cost:  131
c ---[2398]---> BDD-cost:   24
c ---[2397]---> BDD-cost:  131
c ---[2396]---> BDD-cost:   24
c ---[2395]---> BDD-cost:  131
c ---[2394]---> BDD-cost:   24
c ---[2393]---> BDD-cost:  131
c ---[2391]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[2390]---> BDD-cost:   24
c ---[2389]---> BDD-cost:  131
c ---[2388]---> BDD-cost:   24
c ---[2387]---> BDD-cost:  131
c ---[2386]---> BDD-cost:   24
c ---[2385]---> BDD-cost:  131
c ---[2384]---> BDD-cost:   24
c ---[2383]---> BDD-cost:  131
c ---[2382]---> BDD-cost:   24
c ---[2381]---> BDD-cost:  131
c ---[2379]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[2378]---> BDD-cost:   24
c ---[2377]---> BDD-cost:  131
c ---[2376]---> BDD-cost:   24
c ---[2375]---> BDD-cost:  131
c ---[2374]---> BDD-cost:   24
c ---[2373]---> BDD-cost:  131
c ---[2372]---> BDD-cost:   24
c ---[2371]---> BDD-cost:  131
c ---[2370]---> BDD-cost:   24
c ---[2369]---> BDD-cost:  131
c ---[2367]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[2366]---> BDD-cost:   24
c ---[2365]---> BDD-cost:  131
c ---[2364]---> BDD-cost:   24
c ---[2363]---> BDD-cost:  131
c ---[2362]---> BDD-cost:   24
c ---[2361]---> BDD-cost:  131
c ---[2360]---> BDD-cost:   24
c ---[2359]---> BDD-cost:  131
c ---[2358]---> BDD-cost:   24
c ---[2357]---> BDD-cost:  131
c ---[2355]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[2354]---> BDD-cost:   24
c ---[2353]---> BDD-cost:  131
c ---[2352]---> BDD-cost:   24
c ---[2351]---> BDD-cost:  131
c ---[2350]---> BDD-cost:   24
c ---[2349]---> BDD-cost:  131
c ---[2348]---> BDD-cost:   24
c ---[2347]---> BDD-cost:  131
c ---[2346]---> BDD-cost:   24
c ---[2345]---> BDD-cost:  131
c ---[2343]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[2342]---> BDD-cost:   24
c ---[2341]---> BDD-cost:  131
c ---[2340]---> BDD-cost:   24
c ---[2339]---> BDD-cost:  131
c ---[2338]---> BDD-cost:   24
c ---[2337]---> BDD-cost:  131
c ---[2336]---> BDD-cost:   24
c ---[2335]---> BDD-cost:  131
c ---[2334]---> BDD-cost:   24
c ---[2333]---> BDD-cost:  131
c ---[2331]---> BDD-cost:   63
c ---[2329]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[2328]---> BDD-cost:   24
c ---[2327]---> BDD-cost:  131
c ---[2326]---> BDD-cost:   24
c ---[2325]---> BDD-cost:  131
c ---[2324]---> BDD-cost:   24
c ---[2323]---> BDD-cost:  131
c ---[2322]---> BDD-cost:   24
c ---[2321]---> BDD-cost:  131
c ---[2320]---> BDD-cost:   24
c ---[2319]---> BDD-cost:  131
c ---[2317]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[2316]---> BDD-cost:   24
c ---[2315]---> BDD-cost:  131
c ---[2314]---> BDD-cost:   24
c ---[2313]---> BDD-cost:  131
c ---[2312]---> BDD-cost:   24
c ---[2311]---> BDD-cost:  131
c ---[2310]---> BDD-cost:   24
c ---[2309]---> BDD-cost:  131
c ---[2308]---> BDD-cost:   24
c ---[2307]---> BDD-cost:  131
c ---[2305]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[2304]---> BDD-cost:   24
c ---[2303]---> BDD-cost:  131
c ---[2302]---> BDD-cost:   24
c ---[2301]---> BDD-cost:  131
c ---[2300]---> BDD-cost:   24
c ---[2299]---> BDD-cost:  131
c ---[2298]---> BDD-cost:   24
c ---[2297]---> BDD-cost:  131
c ---[2296]---> BDD-cost:   24
c ---[2295]---> BDD-cost:  131
c ---[2293]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[2292]---> BDD-cost:   24
c ---[2291]---> BDD-cost:  131
c ---[2290]---> BDD-cost:   24
c ---[2289]---> BDD-cost:  131
c ---[2288]---> BDD-cost:   24
c ---[2287]---> BDD-cost:  131
c ---[2286]---> BDD-cost:   24
c ---[2285]---> BDD-cost:  131
c ---[2284]---> BDD-cost:   24
c ---[2283]---> BDD-cost:  131
c ---[2281]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[2280]---> BDD-cost:   24
c ---[2279]---> BDD-cost:  131
c ---[2278]---> BDD-cost:   24
c ---[2277]---> BDD-cost:  131
c ---[2276]---> BDD-cost:   24
c ---[2275]---> BDD-cost:  131
c ---[2274]---> BDD-cost:   24
c ---[2273]---> BDD-cost:  131
c ---[2272]---> BDD-cost:   24
c ---[2271]---> BDD-cost:  131
c ---[2269]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[2268]---> BDD-cost:   24
c ---[2267]---> BDD-cost:  131
c ---[2266]---> BDD-cost:   24
c ---[2265]---> BDD-cost:  131
c ---[2264]---> BDD-cost:   24
c ---[2263]---> BDD-cost:  131
c ---[2262]---> BDD-cost:   24
c ---[2261]---> BDD-cost:  131
c ---[2260]---> BDD-cost:   24
c ---[2259]---> BDD-cost:  131
c ---[2257]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[2256]---> BDD-cost:   24
c ---[2255]---> BDD-cost:  131
c ---[2254]---> BDD-cost:   24
c ---[2253]---> BDD-cost:  131
c ---[2252]---> BDD-cost:   24
c ---[2251]---> BDD-cost:  131
c ---[2250]---> BDD-cost:   24
c ---[2249]---> BDD-cost:  131
c ---[2248]---> BDD-cost:   24
c ---[2247]---> BDD-cost:  131
c ---[2245]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[2244]---> BDD-cost:   24
c ---[2243]---> BDD-cost:  131
c ---[2242]---> BDD-cost:   24
c ---[2241]---> BDD-cost:  131
c ---[2240]---> BDD-cost:   24
c ---[2239]---> BDD-cost:  131
c ---[2238]---> BDD-cost:   24
c ---[2237]---> BDD-cost:  131
c ---[2236]---> BDD-cost:   24
c ---[2235]---> BDD-cost:  131
c ---[2233]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[2232]---> BDD-cost:   24
c ---[2231]---> BDD-cost:  131
c ---[2230]---> BDD-cost:   24
c ---[2229]---> BDD-cost:  131
c ---[2228]---> BDD-cost:   24
c ---[2227]---> BDD-cost:  131
c ---[2226]---> BDD-cost:   24
c ---[2225]---> BDD-cost:  131
c ---[2224]---> BDD-cost:   24
c ---[2223]---> BDD-cost:  131
c ---[2221]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[2220]---> BDD-cost:   24
c ---[2219]---> BDD-cost:  131
c ---[2218]---> BDD-cost:   24
c ---[2217]---> BDD-cost:  131
c ---[2216]---> BDD-cost:   24
c ---[2215]---> BDD-cost:  131
c ---[2214]---> BDD-cost:   24
c ---[2213]---> BDD-cost:  131
c ---[2212]---> BDD-cost:   24
c ---[2211]---> BDD-cost:  131
c ---[2209]---> BDD-cost:   63
c ---[2207]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[2206]---> BDD-cost:   24
c ---[2205]---> BDD-cost:  131
c ---[2204]---> BDD-cost:   24
c ---[2203]---> BDD-cost:  131
c ---[2202]---> BDD-cost:   24
c ---[2201]---> BDD-cost:  131
c ---[2200]---> BDD-cost:   24
c ---[2199]---> BDD-cost:  131
c ---[2198]---> BDD-cost:   24
c ---[2197]---> BDD-cost:  131
c ---[2195]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[2194]---> BDD-cost:   24
c ---[2193]---> BDD-cost:  131
c ---[2192]---> BDD-cost:   24
c ---[2191]---> BDD-cost:  131
c ---[2190]---> BDD-cost:   24
c ---[2189]---> BDD-cost:  131
c ---[2188]---> BDD-cost:   24
c ---[2187]---> BDD-cost:  131
c ---[2186]---> BDD-cost:   24
c ---[2185]---> BDD-cost:  131
c ---[2183]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[2182]---> BDD-cost:   24
c ---[2181]---> BDD-cost:  131
c ---[2180]---> BDD-cost:   24
c ---[2179]---> BDD-cost:  131
c ---[2178]---> BDD-cost:   24
c ---[2177]---> BDD-cost:  131
c ---[2176]---> BDD-cost:   24
c ---[2175]---> BDD-cost:  131
c ---[2174]---> BDD-cost:   24
c ---[2173]---> BDD-cost:  131
c ---[2171]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[2170]---> BDD-cost:   24
c ---[2169]---> BDD-cost:  131
c ---[2168]---> BDD-cost:   24
c ---[2167]---> BDD-cost:  131
c ---[2166]---> BDD-cost:   24
c ---[2165]---> BDD-cost:  131
c ---[2164]---> BDD-cost:   24
c ---[2163]---> BDD-cost:  131
c ---[2162]---> BDD-cost:   24
c ---[2161]---> BDD-cost:  131
c ---[2159]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[2158]---> BDD-cost:   24
c ---[2157]---> BDD-cost:  131
c ---[2156]---> BDD-cost:   24
c ---[2155]---> BDD-cost:  131
c ---[2154]---> BDD-cost:   24
c ---[2153]---> BDD-cost:  131
c ---[2152]---> BDD-cost:   24
c ---[2151]---> BDD-cost:  131
c ---[2150]---> BDD-cost:   24
c ---[2149]---> BDD-cost:  131
c ---[2147]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[2146]---> BDD-cost:   24
c ---[2145]---> BDD-cost:  131
c ---[2144]---> BDD-cost:   24
c ---[2143]---> BDD-cost:  131
c ---[2142]---> BDD-cost:   24
c ---[2141]---> BDD-cost:  131
c ---[2140]---> BDD-cost:   24
c ---[2139]---> BDD-cost:  131
c ---[2138]---> BDD-cost:   24
c ---[2137]---> BDD-cost:  131
c ---[2135]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[2134]---> BDD-cost:   24
c ---[2133]---> BDD-cost:  131
c ---[2132]---> BDD-cost:   24
c ---[2131]---> BDD-cost:  131
c ---[2130]---> BDD-cost:   24
c ---[2129]---> BDD-cost:  131
c ---[2128]---> BDD-cost:   24
c ---[2127]---> BDD-cost:  131
c ---[2126]---> BDD-cost:   24
c ---[2125]---> BDD-cost:  131
c ---[2123]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[2122]---> BDD-cost:   24
c ---[2121]---> BDD-cost:  131
c ---[2120]---> BDD-cost:   24
c ---[2119]---> BDD-cost:  131
c ---[2118]---> BDD-cost:   24
c ---[2117]---> BDD-cost:  131
c ---[2116]---> BDD-cost:   24
c ---[2115]---> BDD-cost:  131
c ---[2114]---> BDD-cost:   24
c ---[2113]---> BDD-cost:  131
c ---[2111]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[2110]---> BDD-cost:   24
c ---[2109]---> BDD-cost:  131
c ---[2108]---> BDD-cost:   24
c ---[2107]---> BDD-cost:  131
c ---[2106]---> BDD-cost:   24
c ---[2105]---> BDD-cost:  131
c ---[2104]---> BDD-cost:   24
c ---[2103]---> BDD-cost:  131
c ---[2102]---> BDD-cost:   24
c ---[2101]---> BDD-cost:  131
c ---[2099]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[2098]---> BDD-cost:   24
c ---[2097]---> BDD-cost:  131
c ---[2096]---> BDD-cost:   24
c ---[2095]---> BDD-cost:  131
c ---[2094]---> BDD-cost:   24
c ---[2093]---> BDD-cost:  131
c ---[2092]---> BDD-cost:   24
c ---[2091]---> BDD-cost:  131
c ---[2090]---> BDD-cost:   24
c ---[2089]---> BDD-cost:  131
c ---[2087]---> BDD-cost:   63
c ---[2085]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[2084]---> BDD-cost:   24
c ---[2083]---> BDD-cost:  131
c ---[2082]---> BDD-cost:   24
c ---[2081]---> BDD-cost:  131
c ---[2080]---> BDD-cost:   24
c ---[2079]---> BDD-cost:  131
c ---[2078]---> BDD-cost:   24
c ---[2077]---> BDD-cost:  131
c ---[2076]---> BDD-cost:   24
c ---[2075]---> BDD-cost:  131
c ---[2073]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[2072]---> BDD-cost:   24
c ---[2071]---> BDD-cost:  131
c ---[2070]---> BDD-cost:   24
c ---[2069]---> BDD-cost:  131
c ---[2068]---> BDD-cost:   24
c ---[2067]---> BDD-cost:  131
c ---[2066]---> BDD-cost:   24
c ---[2065]---> BDD-cost:  131
c ---[2064]---> BDD-cost:   24
c ---[2063]---> BDD-cost:  131
c ---[2061]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[2060]---> BDD-cost:   24
c ---[2059]---> BDD-cost:  131
c ---[2058]---> BDD-cost:   24
c ---[2057]---> BDD-cost:  131
c ---[2056]---> BDD-cost:   24
c ---[2055]---> BDD-cost:  131
c ---[2054]---> BDD-cost:   24
c ---[2053]---> BDD-cost:  131
c ---[2052]---> BDD-cost:   24
c ---[2051]---> BDD-cost:  131
c ---[2049]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[2048]---> BDD-cost:   24
c ---[2047]---> BDD-cost:  131
c ---[2046]---> BDD-cost:   24
c ---[2045]---> BDD-cost:  131
c ---[2044]---> BDD-cost:   24
c ---[2043]---> BDD-cost:  131
c ---[2042]---> BDD-cost:   24
c ---[2041]---> BDD-cost:  131
c ---[2040]---> BDD-cost:   24
c ---[2039]---> BDD-cost:  131
c ---[2037]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[2036]---> BDD-cost:   24
c ---[2035]---> BDD-cost:  131
c ---[2034]---> BDD-cost:   24
c ---[2033]---> BDD-cost:  131
c ---[2032]---> BDD-cost:   24
c ---[2031]---> BDD-cost:  131
c ---[2030]---> BDD-cost:   24
c ---[2029]---> BDD-cost:  131
c ---[2028]---> BDD-cost:   24
c ---[2027]---> BDD-cost:  131
c ---[2025]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[2024]---> BDD-cost:   24
c ---[2023]---> BDD-cost:  131
c ---[2022]---> BDD-cost:   24
c ---[2021]---> BDD-cost:  131
c ---[2020]---> BDD-cost:   24
c ---[2019]---> BDD-cost:  131
c ---[2018]---> BDD-cost:   24
c ---[2017]---> BDD-cost:  131
c ---[2016]---> BDD-cost:   24
c ---[2015]---> BDD-cost:  131
c ---[2013]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[2012]---> BDD-cost:   24
c ---[2011]---> BDD-cost:  131
c ---[2010]---> BDD-cost:   24
c ---[2009]---> BDD-cost:  131
c ---[2008]---> BDD-cost:   24
c ---[2007]---> BDD-cost:  131
c ---[2006]---> BDD-cost:   24
c ---[2005]---> BDD-cost:  131
c ---[2004]---> BDD-cost:   24
c ---[2003]---> BDD-cost:  131
c ---[2001]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[2000]---> BDD-cost:   24
c ---[1999]---> BDD-cost:  131
c ---[1998]---> BDD-cost:   24
c ---[1997]---> BDD-cost:  131
c ---[1996]---> BDD-cost:   24
c ---[1995]---> BDD-cost:  131
c ---[1994]---> BDD-cost:   24
c ---[1993]---> BDD-cost:  131
c ---[1992]---> BDD-cost:   24
c ---[1991]---> BDD-cost:  131
c ---[1989]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[1988]---> BDD-cost:   24
c ---[1987]---> BDD-cost:  131
c ---[1986]---> BDD-cost:   24
c ---[1985]---> BDD-cost:  131
c ---[1984]---> BDD-cost:   24
c ---[1983]---> BDD-cost:  131
c ---[1982]---> BDD-cost:   24
c ---[1981]---> BDD-cost:  131
c ---[1980]---> BDD-cost:   24
c ---[1979]---> BDD-cost:  131
c ---[1977]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[1976]---> BDD-cost:   24
c ---[1975]---> BDD-cost:  131
c ---[1974]---> BDD-cost:   24
c ---[1973]---> BDD-cost:  131
c ---[1972]---> BDD-cost:   24
c ---[1971]---> BDD-cost:  131
c ---[1970]---> BDD-cost:   24
c ---[1969]---> BDD-cost:  131
c ---[1968]---> BDD-cost:   24
c ---[1967]---> BDD-cost:  131
c ---[1965]---> BDD-cost:   63
c ---[1963]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[1962]---> BDD-cost:   24
c ---[1961]---> BDD-cost:  131
c ---[1960]---> BDD-cost:   24
c ---[1959]---> BDD-cost:  131
c ---[1958]---> BDD-cost:   24
c ---[1957]---> BDD-cost:  131
c ---[1956]---> BDD-cost:   24
c ---[1955]---> BDD-cost:  131
c ---[1954]---> BDD-cost:   24
c ---[1953]---> BDD-cost:  131
c ---[1951]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[1950]---> BDD-cost:   24
c ---[1949]---> BDD-cost:  131
c ---[1948]---> BDD-cost:   24
c ---[1947]---> BDD-cost:  131
c ---[1946]---> BDD-cost:   24
c ---[1945]---> BDD-cost:  131
c ---[1944]---> BDD-cost:   24
c ---[1943]---> BDD-cost:  131
c ---[1942]---> BDD-cost:   24
c ---[1941]---> BDD-cost:  131
c ---[1939]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[1938]---> BDD-cost:   24
c ---[1937]---> BDD-cost:  131
c ---[1936]---> BDD-cost:   24
c ---[1935]---> BDD-cost:  131
c ---[1934]---> BDD-cost:   24
c ---[1933]---> BDD-cost:  131
c ---[1932]---> BDD-cost:   24
c ---[1931]---> BDD-cost:  131
c ---[1930]---> BDD-cost:   24
c ---[1929]---> BDD-cost:  131
c ---[1927]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[1926]---> BDD-cost:   24
c ---[1925]---> BDD-cost:  131
c ---[1924]---> BDD-cost:   24
c ---[1923]---> BDD-cost:  131
c ---[1922]---> BDD-cost:   24
c ---[1921]---> BDD-cost:  131
c ---[1920]---> BDD-cost:   24
c ---[1919]---> BDD-cost:  131
c ---[1918]---> BDD-cost:   24
c ---[1917]---> BDD-cost:  131
c ---[1915]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[1914]---> BDD-cost:   24
c ---[1913]---> BDD-cost:  131
c ---[1912]---> BDD-cost:   24
c ---[1911]---> BDD-cost:  131
c ---[1910]---> BDD-cost:   24
c ---[1909]---> BDD-cost:  131
c ---[1908]---> BDD-cost:   24
c ---[1907]---> BDD-cost:  131
c ---[1906]---> BDD-cost:   24
c ---[1905]---> BDD-cost:  131
c ---[1903]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[1902]---> BDD-cost:   24
c ---[1901]---> BDD-cost:  131
c ---[1900]---> BDD-cost:   24
c ---[1899]---> BDD-cost:  131
c ---[1898]---> BDD-cost:   24
c ---[1897]---> BDD-cost:  131
c ---[1896]---> BDD-cost:   24
c ---[1895]---> BDD-cost:  131
c ---[1894]---> BDD-cost:   24
c ---[1893]---> BDD-cost:  131
c ---[1891]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[1890]---> BDD-cost:   24
c ---[1889]---> BDD-cost:  131
c ---[1888]---> BDD-cost:   24
c ---[1887]---> BDD-cost:  131
c ---[1886]---> BDD-cost:   24
c ---[1885]---> BDD-cost:  131
c ---[1884]---> BDD-cost:   24
c ---[1883]---> BDD-cost:  131
c ---[1882]---> BDD-cost:   24
c ---[1881]---> BDD-cost:  131
c ---[1879]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[1878]---> BDD-cost:   24
c ---[1877]---> BDD-cost:  131
c ---[1876]---> BDD-cost:   24
c ---[1875]---> BDD-cost:  131
c ---[1874]---> BDD-cost:   24
c ---[1873]---> BDD-cost:  131
c ---[1872]---> BDD-cost:   24
c ---[1871]---> BDD-cost:  131
c ---[1870]---> BDD-cost:   24
c ---[1869]---> BDD-cost:  131
c ---[1867]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[1866]---> BDD-cost:   24
c ---[1865]---> BDD-cost:  131
c ---[1864]---> BDD-cost:   24
c ---[1863]---> BDD-cost:  131
c ---[1862]---> BDD-cost:   24
c ---[1861]---> BDD-cost:  131
c ---[1860]---> BDD-cost:   24
c ---[1859]---> BDD-cost:  131
c ---[1858]---> BDD-cost:   24
c ---[1857]---> BDD-cost:  131
c ---[1855]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[1854]---> BDD-cost:   24
c ---[1853]---> BDD-cost:  131
c ---[1852]---> BDD-cost:   24
c ---[1851]---> BDD-cost:  131
c ---[1850]---> BDD-cost:   24
c ---[1849]---> BDD-cost:  131
c ---[1848]---> BDD-cost:   24
c ---[1847]---> BDD-cost:  131
c ---[1846]---> BDD-cost:   24
c ---[1845]---> BDD-cost:  131
c ---[1843]---> BDD-cost:   63
c ---[1841]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[1840]---> BDD-cost:   24
c ---[1839]---> BDD-cost:  131
c ---[1838]---> BDD-cost:   24
c ---[1837]---> BDD-cost:  131
c ---[1836]---> BDD-cost:   24
c ---[1835]---> BDD-cost:  131
c ---[1834]---> BDD-cost:   24
c ---[1833]---> BDD-cost:  131
c ---[1832]---> BDD-cost:   24
c ---[1831]---> BDD-cost:  131
c ---[1829]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[1828]---> BDD-cost:   24
c ---[1827]---> BDD-cost:  131
c ---[1826]---> BDD-cost:   24
c ---[1825]---> BDD-cost:  131
c ---[1824]---> BDD-cost:   24
c ---[1823]---> BDD-cost:  131
c ---[1822]---> BDD-cost:   24
c ---[1821]---> BDD-cost:  131
c ---[1820]---> BDD-cost:   24
c ---[1819]---> BDD-cost:  131
c ---[1817]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[1816]---> BDD-cost:   24
c ---[1815]---> BDD-cost:  131
c ---[1814]---> BDD-cost:   24
c ---[1813]---> BDD-cost:  131
c ---[1812]---> BDD-cost:   24
c ---[1811]---> BDD-cost:  131
c ---[1810]---> BDD-cost:   24
c ---[1809]---> BDD-cost:  131
c ---[1808]---> BDD-cost:   24
c ---[1807]---> BDD-cost:  131
c ---[1805]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[1804]---> BDD-cost:   24
c ---[1803]---> BDD-cost:  131
c ---[1802]---> BDD-cost:   24
c ---[1801]---> BDD-cost:  131
c ---[1800]---> BDD-cost:   24
c ---[1799]---> BDD-cost:  131
c ---[1798]---> BDD-cost:   24
c ---[1797]---> BDD-cost:  131
c ---[1796]---> BDD-cost:   24
c ---[1795]---> BDD-cost:  131
c ---[1793]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[1792]---> BDD-cost:   24
c ---[1791]---> BDD-cost:  131
c ---[1790]---> BDD-cost:   24
c ---[1789]---> BDD-cost:  131
c ---[1788]---> BDD-cost:   24
c ---[1787]---> BDD-cost:  131
c ---[1786]---> BDD-cost:   24
c ---[1785]---> BDD-cost:  131
c ---[1784]---> BDD-cost:   24
c ---[1783]---> BDD-cost:  131
c ---[1781]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[1780]---> BDD-cost:   24
c ---[1779]---> BDD-cost:   22
c ---[1778]---> BDD-cost:   25
c ---[1777]---> BDD-cost:   25
c ---[1776]---> BDD-cost:   27
c ---[1775]---> BDD-cost:   27
c ---[1774]---> BDD-cost:   26
c ---[1773]---> BDD-cost:   26
c ---[1772]---> BDD-cost:   25
c ---[1771]---> BDD-cost:   26
c ---[1769]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[1768]---> BDD-cost:   25
c ---[1767]---> BDD-cost:   24
c ---[1766]---> BDD-cost:   24
c ---[1765]---> BDD-cost:   24
c ---[1764]---> BDD-cost:   24
c ---[1763]---> BDD-cost:   25
c ---[1762]---> BDD-cost:   25
c ---[1761]---> BDD-cost:   26
c ---[1760]---> BDD-cost:   23
c ---[1759]---> BDD-cost:   23
c ---[1757]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[1756]---> BDD-cost:   20
c ---[1755]---> BDD-cost:   20
c ---[1754]---> BDD-cost:   20
c ---[1753]---> BDD-cost:   20
c ---[1752]---> BDD-cost:   26
c ---[1751]---> BDD-cost:   24
c ---[1750]---> BDD-cost:   21
c ---[1749]---> BDD-cost:   21
c ---[1748]---> BDD-cost:   25
c ---[1747]---> BDD-cost:   25
c ---[1745]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[1744]---> BDD-cost:   25
c ---[1743]---> BDD-cost:   25
c ---[1742]---> BDD-cost:   24
c ---[1741]---> BDD-cost:   22
c ---[1740]---> BDD-cost:   23
c ---[1739]---> BDD-cost:   25
c ---[1738]---> BDD-cost:   23
c ---[1737]---> BDD-cost:   23
c ---[1736]---> BDD-cost:   23
c ---[1735]---> BDD-cost:   25
c ---[1733]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[1732]---> BDD-cost:   25
c ---[1731]---> BDD-cost:   25
c ---[1730]---> BDD-cost:   23
c ---[1729]---> BDD-cost:   25
c ---[1728]---> BDD-cost:   25
c ---[1727]---> BDD-cost:   25
c ---[1726]---> BDD-cost:   23
c ---[1725]---> BDD-cost:   24
c ---[1724]---> BDD-cost:   24
c ---[1723]---> BDD-cost:   24
c ---[1721]---> BDD-cost:   63
c ---[1719]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[1718]---> BDD-cost:   23
c ---[1717]---> BDD-cost:   26
c ---[1716]---> BDD-cost:   25
c ---[1715]---> BDD-cost:   23
c ---[1714]---> BDD-cost:   24
c ---[1713]---> Sorter-cost:  797     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1712]---> Sorter-cost:  701     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1711]---> Sorter-cost:  749     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1710]---> Sorter-cost:  688     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1709]---> Sorter-cost:  695     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1707]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[1706]---> Sorter-cost:  686     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1705]---> Sorter-cost:  778     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1704]---> Sorter-cost:  750     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1703]---> Sorter-cost:  755     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1702]---> Sorter-cost:  778     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1701]---> Sorter-cost:  769     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1700]---> Sorter-cost:  679     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1699]---> Sorter-cost:  787     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1698]---> Sorter-cost:  778     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1697]---> Sorter-cost:  520     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1695]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[1694]---> Sorter-cost:  520     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1693]---> Sorter-cost:  520     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1692]---> Sorter-cost:  520     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1691]---> Sorter-cost:  520     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1690]---> Sorter-cost:  520     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1689]---> Sorter-cost:  520     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1688]---> Sorter-cost:  520     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1687]---> Sorter-cost:  520     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1686]---> Sorter-cost:  520     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1685]---> Sorter-cost:  520     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1683]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[1671]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[1659]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[1647]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[1646]---> Sorter-cost:  657     Base: 2 2 2 2 2 2 2 2 2 2 2 2 7 7
c ---[1645]---> Adder-cost: 719   maxlim: 131070   bits: 18/17
c ---[1644]---> Adder-cost: 647   maxlim: 131070   bits: 18/17
c ---[1643]---> Adder-cost: 719   maxlim: 131070   bits: 18/17
c ---[1642]---> Adder-cost: 717   maxlim: 131070   bits: 18/17
c ---[1641]---> Adder-cost: 719   maxlim: 131070   bits: 18/17
c ---[1640]---> Adder-cost: 713   maxlim: 131070   bits: 18/17
c ---[1639]---> Adder-cost: 719   maxlim: 131070   bits: 18/17
c ---[1638]---> Adder-cost: 717   maxlim: 131070   bits: 18/17
c ---[1635]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[1634]---> Adder-cost: 719   maxlim: 131070   bits: 18/17
c ---[1633]---> Adder-cost: 715   maxlim: 131070   bits: 18/17
c ---[1632]---> Adder-cost: 651   maxlim: 131070   bits: 18/17
c ---[1631]---> Adder-cost: 664   maxlim: 131070   bits: 18/17
c ---[1630]---> Adder-cost: 719   maxlim: 131070   bits: 18/17
c ---[1629]---> Adder-cost: 647   maxlim: 131070   bits: 18/17
c ---[1628]---> Adder-cost: 717   maxlim: 131070   bits: 18/17
c ---[1627]---> Adder-cost: 715   maxlim: 131070   bits: 18/17
c ---[1626]---> Adder-cost: 491   maxlim: 131070   bits: 18/17
c ---[1625]---> Adder-cost: 719   maxlim: 131070   bits: 18/17
c ---[1623]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[1622]---> Adder-cost: 717   maxlim: 131070   bits: 18/17
c ---[1621]---> Adder-cost: 715   maxlim: 131070   bits: 18/17
c ---[1620]---> Adder-cost: 717   maxlim: 131070   bits: 18/17
c ---[1619]---> Adder-cost: 719   maxlim: 131070   bits: 18/17
c ---[1615]---> Adder-cost: 719   maxlim: 131070   bits: 18/17
c ---[1614]---> Adder-cost: 717   maxlim: 131070   bits: 18/17
c ---[1613]---> Adder-cost: 711   maxlim: 131070   bits: 18/17
c ---[1611]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[1610]---> Adder-cost: 579   maxlim: 131070   bits: 18/17
c ---[1609]---> Adder-cost: 651   maxlim: 131070   bits: 18/17
c ---[1608]---> Adder-cost: 651   maxlim: 131070   bits: 18/17
c ---[1607]---> Adder-cost: 713   maxlim: 131070   bits: 18/17
c ---[1606]---> Adder-cost: 719   maxlim: 131070   bits: 18/17
c ---[1605]---> Adder-cost: 719   maxlim: 131070   bits: 18/17
c ---[1604]---> Adder-cost: 715   maxlim: 131070   bits: 18/17
c ---[1602]---> Adder-cost: 711   maxlim: 131070   bits: 18/17
c ---[1599]---> BDD-cost:   63
c ---[1597]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[1595]---> Adder-cost: 717   maxlim: 131070   bits: 18/17
c ---[1594]---> Adder-cost: 617   maxlim: 131070   bits: 18/17
c ---[1593]---> Adder-cost: 717   maxlim: 131070   bits: 18/17
c ---[1592]---> Adder-cost: 493   maxlim: 131070   bits: 18/17
c ---[1591]---> Adder-cost: 613   maxlim: 131070   bits: 18/17
c ---[1590]---> Adder-cost: 715   maxlim: 131070   bits: 18/17
c ---[1589]---> Adder-cost: 715   maxlim: 131070   bits: 18/17
c ---[1588]---> Adder-cost: 717   maxlim: 131070   bits: 18/17
c ---[1587]---> Adder-cost: 630   maxlim: 131070   bits: 18/17
c ---[1585]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[1584]---> Adder-cost: 713   maxlim: 131070   bits: 18/17
c ---[1583]---> Adder-cost: 717   maxlim: 131070   bits: 18/17
c ---[1582]---> Adder-cost: 719   maxlim: 131070   bits: 18/17
c ---[1581]---> Adder-cost: 617   maxlim: 131070   bits: 18/17
c ---[1580]---> Adder-cost: 719   maxlim: 131070   bits: 18/17
c ---[1579]---> Adder-cost: 719   maxlim: 131070   bits: 18/17
c ---[1578]---> Adder-cost: 649   maxlim: 131070   bits: 18/17
c ---[1577]---> Adder-cost: 719   maxlim: 131070   bits: 18/17
c ---[1576]---> Adder-cost: 685   maxlim: 131070   bits: 18/17
c ---[1575]---> Adder-cost: 529   maxlim: 131070   bits: 18/17
c ---[1573]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[1572]---> Adder-cost: 649   maxlim: 131070   bits: 18/17
c ---[1571]---> Adder-cost: 715   maxlim: 131070   bits: 18/17
c ---[1570]---> Adder-cost: 719   maxlim: 131070   bits: 18/17
c ---[1567]---> Adder-cost: 719   maxlim: 131070   bits: 18/17
c ---[1565]---> Adder-cost: 709   maxlim: 131070   bits: 18/17
c ---[1563]---> Adder-cost: 613   maxlim: 131070   bits: 18/17
c ---[1561]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[1560]---> Adder-cost: 719   maxlim: 131070   bits: 18/17
c ---[1559]---> Adder-cost: 717   maxlim: 131070   bits: 18/17
c ---[1558]---> Adder-cost: 611   maxlim: 131070   bits: 18/17
c ---[1557]---> Adder-cost: 715   maxlim: 131070   bits: 18/17
c ---[1556]---> Adder-cost: 719   maxlim: 131070   bits: 18/17
c ---[1555]---> Adder-cost: 533   maxlim: 131070   bits: 18/17
c ---[1554]---> Adder-cost: 719   maxlim: 131070   bits: 18/17
c ---[1553]---> Adder-cost: 642   maxlim: 131070   bits: 18/17
c ---[1552]---> Adder-cost: 715   maxlim: 131070   bits: 18/17
c ---[1551]---> Adder-cost: 685   maxlim: 131070   bits: 18/17
c ---[1549]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[1547]---> Adder-cost: 719   maxlim: 131070   bits: 18/17
c ---[1546]---> Adder-cost: 719   maxlim: 131070   bits: 18/17
c ---[1545]---> Adder-cost: 713   maxlim: 131070   bits: 18/17
c ---[1544]---> Adder-cost: 719   maxlim: 131070   bits: 18/17
c ---[1543]---> Adder-cost: 615   maxlim: 131070   bits: 18/17
c ---[1541]---> Adder-cost: 715   maxlim: 131070   bits: 18/17
c ---[1537]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[1536]---> Adder-cost: 713   maxlim: 131070   bits: 18/17
c ---[1535]---> Adder-cost: 713   maxlim: 131070   bits: 18/17
c ---[1534]---> Adder-cost: 565   maxlim: 131070   bits: 18/17
c ---[1533]---> Adder-cost: 719   maxlim: 131070   bits: 18/17
c ---[1532]---> Adder-cost: 719   maxlim: 131070   bits: 18/17
c ---[1529]---> Adder-cost: 617   maxlim: 131070   bits: 18/17
c ---[1528]---> Adder-cost: 717   maxlim: 131070   bits: 18/17
c ---[1527]---> Adder-cost: 713   maxlim: 131070   bits: 18/17
c ---[1525]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[1524]---> Adder-cost: 529   maxlim: 131070   bits: 18/17
c ---[1523]---> Adder-cost: 491   maxlim: 131070   bits: 18/17
c ---[1522]---> Adder-cost: 713   maxlim: 131070   bits: 18/17
c ---[1521]---> Adder-cost: 715   maxlim: 131070   bits: 18/17
c ---[1520]---> Adder-cost: 613   maxlim: 131070   bits: 18/17
c ---[1518]---> Adder-cost: 711   maxlim: 131070   bits: 18/17
c ---[1517]---> Adder-cost: 531   maxlim: 131070   bits: 18/17
c ---[1516]---> Adder-cost: 529   maxlim: 131070   bits: 18/17
c ---[1515]---> Adder-cost: 719   maxlim: 131070   bits: 18/17
c ---[1513]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[1512]---> Adder-cost: 719   maxlim: 131070   bits: 18/17
c ---[1510]---> Adder-cost: 715   maxlim: 131070   bits: 18/17
c ---[1509]---> Adder-cost: 645   maxlim: 131070   bits: 18/17
c ---[1508]---> Adder-cost: 719   maxlim: 131070   bits: 18/17
c ---[1507]---> Adder-cost: 517   maxlim: 131070   bits: 18/17
c ---[1506]---> Adder-cost: 719   maxlim: 131070   bits: 18/17
c ---[1505]---> Adder-cost: 719   maxlim: 131070   bits: 18/17
c ---[1503]---> Adder-cost: 719   maxlim: 131070   bits: 18/17
c ---[1501]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[1500]---> Adder-cost: 639   maxlim: 131070   bits: 18/17
c ---[1499]---> Adder-cost: 647   maxlim: 131070   bits: 18/17
c ---[1498]---> Adder-cost: 558   maxlim: 131070   bits: 18/17
c ---[1497]---> Adder-cost: 685   maxlim: 131070   bits: 18/17
c ---[1496]---> Adder-cost: 719   maxlim: 131070   bits: 18/17
c ---[1495]---> Adder-cost: 545   maxlim: 131070   bits: 18/17
c ---[1494]---> Adder-cost: 563   maxlim: 131070   bits: 18/17
c ---[1493]---> Adder-cost: 613   maxlim: 131070   bits: 18/17
c ---[1492]---> Adder-cost: 477   maxlim: 131070   bits: 18/17
c ---[1491]---> Adder-cost: 533   maxlim: 131070   bits: 18/17
c ---[1489]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[1488]---> Adder-cost: 510   maxlim: 131070   bits: 18/17
c ---[1487]---> Adder-cost: 510   maxlim: 131070   bits: 18/17
c ---[1486]---> Adder-cost: 477   maxlim: 131070   bits: 18/17
c ---[1485]---> Adder-cost: 481   maxlim: 131070   bits: 18/17
c ---[1484]---> Adder-cost: 571   maxlim: 131070   bits: 18/17
c ---[1483]---> Adder-cost: 567   maxlim: 131070   bits: 18/17
c ---[1482]---> Adder-cost: 477   maxlim: 131070   bits: 18/17
c ---[1480]---> Adder-cost: 500   maxlim: 131070   bits: 18/17
c ---[1479]---> Adder-cost: 515   maxlim: 131070   bits: 18/17
c ---[1477]---> BDD-cost:   63
c ---[1475]---> BDD-cost:   63
c ---[1473]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[1472]---> Adder-cost: 549   maxlim: 131070   bits: 18/17
c ---[1471]---> Adder-cost: 473   maxlim: 131070   bits: 18/17
c ---[1470]---> Adder-cost: 465   maxlim: 131070   bits: 18/17
c ---[1469]---> Adder-cost: 613   maxlim: 131070   bits: 18/17
c ---[1468]---> Adder-cost: 545   maxlim: 131070   bits: 18/17
c ---[1467]---> Adder-cost: 523   maxlim: 131070   bits: 18/17
c ---[1466]---> Adder-cost: 545   maxlim: 131070   bits: 18/17
c ---[1465]---> Adder-cost: 514   maxlim: 131070   bits: 18/17
c ---[1464]---> Adder-cost: 509   maxlim: 131070   bits: 18/17
c ---[1463]---> Adder-cost: 651   maxlim: 131070   bits: 18/17
c ---[1461]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[1460]---> Adder-cost: 476   maxlim: 131070   bits: 18/17
c ---[1459]---> Adder-cost: 479   maxlim: 131070   bits: 18/17
c ---[1458]---> Adder-cost: 547   maxlim: 131070   bits: 18/17
c ---[1457]---> Adder-cost: 578   maxlim: 131070   bits: 18/17
c ---[1456]---> Adder-cost: 525   maxlim: 131070   bits: 18/17
c ---[1455]---> Adder-cost: 475   maxlim: 131070   bits: 18/17
c ---[1454]---> Adder-cost: 513   maxlim: 131070   bits: 18/17
c ---[1453]---> Adder-cost: 517   maxlim: 131070   bits: 18/17
c ---[1452]---> Adder-cost: 651   maxlim: 131070   bits: 18/17
c ---[1451]---> Adder-cost: 649   maxlim: 131070   bits: 18/17
c ---[1449]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[1447]---> Adder-cost: 506   maxlim: 131070   bits: 18/17
c ---[1446]---> Adder-cost: 1072   maxlim: 2621419   bits: 23/22
c ---[1445]---> Adder-cost: 1038   maxlim: 2621419   bits: 23/22
c ---[1444]---> Adder-cost: 1324   maxlim: 2490348   bits: 23/22
c ---[1443]---> Adder-cost: 1454   maxlim: 2621419   bits: 23/22
c ---[1442]---> Adder-cost: 1434   maxlim: 2752490   bits: 23/22
c ---[1441]---> Adder-cost: 1210   maxlim: 2490348   bits: 23/22
c ---[1440]---> Adder-cost: 1146   maxlim: 2621419   bits: 23/22
c ---[1439]---> Adder-cost: 1174   maxlim: 2555883   bits: 23/22
c ---[1437]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[1436]---> Adder-cost: 1324   maxlim: 2752490   bits: 23/22
c ---[1435]---> Adder-cost: 1382   maxlim: 2228206   bits: 23/22
c ---[1434]---> Adder-cost: 1380   maxlim: 2490348   bits: 23/22
c ---[1433]---> Adder-cost: 1006   maxlim: 2621419   bits: 23/22
c ---[1432]---> Adder-cost: 1304   maxlim: 2490348   bits: 23/22
c ---[1431]---> Adder-cost: 1162   maxlim: 2621419   bits: 23/22
c ---[1430]---> Adder-cost: 1498   maxlim: 2752490   bits: 23/22
c ---[1429]---> Adder-cost: 1052   maxlim: 2621419   bits: 23/22
c ---[1428]---> Adder-cost: 1208   maxlim: 2752490   bits: 23/22
c ---[1427]---> Adder-cost: 1186   maxlim: 2359277   bits: 23/22
c ---[1425]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[1424]---> Adder-cost: 1048   maxlim: 2490348   bits: 23/22
c ---[1423]---> Adder-cost: 1396   maxlim: 2490348   bits: 23/22
c ---[1422]---> Adder-cost: 1228   maxlim: 2359277   bits: 23/22
c ---[1421]---> Adder-cost: 1120   maxlim: 2490348   bits: 23/22
c ---[1420]---> Adder-cost: 1092   maxlim: 2621419   bits: 23/22
c ---[1419]---> Adder-cost: 1302   maxlim: 2752490   bits: 23/22
c ---[1418]---> Adder-cost: 1328   maxlim: 2293741   bits: 23/22
c ---[1417]---> Adder-cost: 1024   maxlim: 2424812   bits: 23/22
c ---[1416]---> Adder-cost: 902   maxlim: 2621419   bits: 23/22
c ---[1415]---> Adder-cost: 1212   maxlim: 2490348   bits: 23/22
c ---[1413]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[1412]---> Adder-cost: 1218   maxlim: 2162670   bits: 23/22
c ---[1411]---> Adder-cost: 1424   maxlim: 2621419   bits: 23/22
c ---[1410]---> Adder-cost: 1394   maxlim: 2359277   bits: 23/22
c ---[1409]---> Adder-cost: 1008   maxlim: 2621419   bits: 23/22
c ---[1408]---> Adder-cost: 1004   maxlim: 2621419   bits: 23/22
c ---[1407]---> Adder-cost: 1010   maxlim: 2621419   bits: 23/22
c ---[1406]---> Adder-cost: 1358   maxlim: 2490348   bits: 23/22
c ---[1405]---> Adder-cost: 1408   maxlim: 2490348   bits: 23/22
c ---[1404]---> Adder-cost: 1490   maxlim: 2752490   bits: 23/22
c ---[1403]---> Adder-cost: 1118   maxlim: 2228206   bits: 23/22
c ---[1401]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[1400]---> Adder-cost: 1306   maxlim: 2752490   bits: 23/22
c ---[1399]---> Adder-cost: 1184   maxlim: 2752490   bits: 23/22
c ---[1398]---> Adder-cost: 1154   maxlim: 2490348   bits: 23/22
c ---[1397]---> Adder-cost: 1088   maxlim: 2555883   bits: 23/22
c ---[1396]---> Adder-cost: 1384   maxlim: 2621419   bits: 23/22
c ---[1395]---> Adder-cost: 1046   maxlim: 2228206   bits: 23/22
c ---[1394]---> Adder-cost: 1340   maxlim: 2621419   bits: 23/22
c ---[1393]---> Adder-cost: 1157   maxlim: 2031599   bits: 22/21
c ---[1392]---> Adder-cost: 1276   maxlim: 2293741   bits: 23/22
c ---[1391]---> Adder-cost: 1452   maxlim: 2752490   bits: 23/22
c ---[1389]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[1388]---> Adder-cost: 1036   maxlim: 2490348   bits: 23/22
c ---[1387]---> Adder-cost: 1420   maxlim: 2752490   bits: 23/22
c ---[1386]---> Adder-cost: 1244   maxlim: 2621419   bits: 23/22
c ---[1385]---> Adder-cost: 1364   maxlim: 2359277   bits: 23/22
c ---[1384]---> Adder-cost: 1388   maxlim: 2621419   bits: 23/22
c ---[1383]---> Adder-cost: 1400   maxlim: 2621419   bits: 23/22
c ---[1382]---> Adder-cost: 1338   maxlim: 2228206   bits: 23/22
c ---[1381]---> Adder-cost: 1440   maxlim: 2752490   bits: 23/22
c ---[1380]---> Adder-cost: 1408   maxlim: 2359277   bits: 23/22
c ---[1379]---> Adder-cost: 1086   maxlim: 2621419   bits: 23/22
c ---[1377]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[1376]---> Adder-cost: 966   maxlim: 2490348   bits: 23/22
c ---[1375]---> Adder-cost: 1158   maxlim: 2752490   bits: 23/22
c ---[1374]---> Adder-cost: 1218   maxlim: 2621419   bits: 23/22
c ---[1373]---> Adder-cost: 1232   maxlim: 2359277   bits: 23/22
c ---[1372]---> Adder-cost: 1378   maxlim: 2621419   bits: 23/22
c ---[1371]---> Adder-cost: 1154   maxlim: 2359277   bits: 23/22
c ---[1370]---> Adder-cost: 1404   maxlim: 2621419   bits: 23/22
c ---[1369]---> Adder-cost: 1154   maxlim: 2621419   bits: 23/22
c ---[1368]---> Adder-cost: 1130   maxlim: 2424812   bits: 23/22
c ---[1367]---> Adder-cost: 1380   maxlim: 2621419   bits: 23/22
c ---[1365]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[1364]---> Adder-cost: 1182   maxlim: 2752490   bits: 23/22
c ---[1363]---> Adder-cost: 1266   maxlim: 2752490   bits: 23/22
c ---[1362]---> Adder-cost: 1528   maxlim: 2752490   bits: 23/22
c ---[1361]---> Adder-cost: 1340   maxlim: 2162670   bits: 23/22
c ---[1360]---> Adder-cost: 1320   maxlim: 2621419   bits: 23/22
c ---[1359]---> Adder-cost: 1116   maxlim: 2621419   bits: 23/22
c ---[1358]---> Adder-cost: 1074   maxlim: 2424812   bits: 23/22
c ---[1357]---> Adder-cost: 1362   maxlim: 2621419   bits: 23/22
c ---[1356]---> Adder-cost: 964   maxlim: 2555883   bits: 23/22
c ---[1355]---> Adder-cost: 1342   maxlim: 2490348   bits: 23/22
c ---[1353]---> BDD-cost:   63
c ---[1351]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[1350]---> Adder-cost: 1500   maxlim: 2686954   bits: 23/22
c ---[1349]---> Adder-cost: 1162   maxlim: 2621419   bits: 23/22
c ---[1348]---> Adder-cost: 1250   maxlim: 2162670   bits: 23/22
c ---[1347]---> Adder-cost: 1472   maxlim: 2752490   bits: 23/22
c ---[1346]---> Adder-cost: 1452   maxlim: 2490348   bits: 23/22
c ---[1345]---> Adder-cost: 1068   maxlim: 2621419   bits: 23/22
c ---[1344]---> Adder-cost: 1424   maxlim: 2752490   bits: 23/22
c ---[1343]---> Adder-cost: 1146   maxlim: 2359277   bits: 23/22
c ---[1342]---> Adder-cost: 1016   maxlim: 2621419   bits: 23/22
c ---[1341]---> Adder-cost: 1214   maxlim: 2490348   bits: 23/22
c ---[1339]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[1338]---> Adder-cost: 1116   maxlim: 2293741   bits: 23/22
c ---[1337]---> Adder-cost: 1234   maxlim: 2621419   bits: 23/22
c ---[1336]---> Adder-cost: 1162   maxlim: 2621419   bits: 23/22
c ---[1335]---> Adder-cost: 1412   maxlim: 2752490   bits: 23/22
c ---[1334]---> Adder-cost: 1124   maxlim: 2752490   bits: 23/22
c ---[1333]---> Adder-cost: 1342   maxlim: 2228206   bits: 23/22
c ---[1332]---> Adder-cost: 1138   maxlim: 2490348   bits: 23/22
c ---[1331]---> Adder-cost: 1360   maxlim: 2359277   bits: 23/22
c ---[1330]---> Adder-cost: 1222   maxlim: 2392044   bits: 23/22
c ---[1329]---> Adder-cost: 1342   maxlim: 2424812   bits: 23/22
c ---[1327]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[1326]---> Adder-cost: 1164   maxlim: 2621419   bits: 23/22
c ---[1325]---> Adder-cost: 1374   maxlim: 2129902   bits: 23/22
c ---[1324]---> Adder-cost: 1026   maxlim: 2523115   bits: 23/22
c ---[1323]---> Adder-cost: 1340   maxlim: 2228206   bits: 23/22
c ---[1322]---> Adder-cost: 1086   maxlim: 2555883   bits: 23/22
c ---[1321]---> Adder-cost: 1106   maxlim: 2490348   bits: 23/22
c ---[1320]---> Adder-cost: 992   maxlim: 2621419   bits: 23/22
c ---[1319]---> Adder-cost: 1216   maxlim: 2293741   bits: 23/22
c ---[1318]---> Adder-cost: 1394   maxlim: 2490348   bits: 23/22
c ---[1317]---> Adder-cost: 1320   maxlim: 2752490   bits: 23/22
c ---[1315]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[1314]---> Adder-cost: 1138   maxlim: 2490348   bits: 23/22
c ---[1313]---> Adder-cost: 1114   maxlim: 2490348   bits: 23/22
c ---[1312]---> Adder-cost: 1266   maxlim: 2555883   bits: 23/22
c ---[1311]---> Adder-cost: 1288   maxlim: 2621419   bits: 23/22
c ---[1310]---> Adder-cost: 1246   maxlim: 2228206   bits: 23/22
c ---[1309]---> Adder-cost: 1378   maxlim: 2621419   bits: 23/22
c ---[1308]---> Adder-cost: 1182   maxlim: 2490348   bits: 23/22
c ---[1307]---> Adder-cost: 1084   maxlim: 2621419   bits: 23/22
c ---[1306]---> Adder-cost: 1412   maxlim: 2752490   bits: 23/22
c ---[1305]---> Adder-cost: 1172   maxlim: 2359277   bits: 23/22
c ---[1303]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[1302]---> Adder-cost: 1334   maxlim: 2621419   bits: 23/22
c ---[1301]---> Adder-cost: 1360   maxlim: 2228205   bits: 23/22
c ---[1300]---> Adder-cost: 1228   maxlim: 2621419   bits: 23/22
c ---[1299]---> Adder-cost: 1428   maxlim: 2490348   bits: 23/22
c ---[1298]---> Adder-cost: 1360   maxlim: 2621419   bits: 23/22
c ---[1297]---> Adder-cost: 1050   maxlim: 2424812   bits: 23/22
c ---[1296]---> Adder-cost: 1388   maxlim: 2621419   bits: 23/22
c ---[1295]---> Adder-cost: 1078   maxlim: 2359277   bits: 23/22
c ---[1294]---> Adder-cost: 1438   maxlim: 2621419   bits: 23/22
c ---[1293]---> Adder-cost: 1418   maxlim: 2752490   bits: 23/22
c ---[1291]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[1290]---> Adder-cost: 1382   maxlim: 2228206   bits: 23/22
c ---[1289]---> Adder-cost: 1402   maxlim: 2424812   bits: 23/22
c ---[1288]---> Adder-cost: 1344   maxlim: 2555883   bits: 23/22
c ---[1287]---> Adder-cost: 1444   maxlim: 2752490   bits: 23/22
c ---[1286]---> Adder-cost: 1176   maxlim: 2359277   bits: 23/22
c ---[1285]---> Adder-cost: 1144   maxlim: 2621419   bits: 23/22
c ---[1284]---> Adder-cost: 1098   maxlim: 2228206   bits: 23/22
c ---[1283]---> Adder-cost: 1020   maxlim: 2621419   bits: 23/22
c ---[1282]---> Adder-cost: 1090   maxlim: 2752490   bits: 23/22
c ---[1281]---> Adder-cost: 1188   maxlim: 2621419   bits: 23/22
c ---[1279]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[1278]---> Adder-cost: 848   maxlim: 2228206   bits: 23/22
c ---[1277]---> Adder-cost: 1476   maxlim: 2752490   bits: 23/22
c ---[1276]---> Adder-cost: 954   maxlim: 2490348   bits: 23/22
c ---[1275]---> Adder-cost: 1082   maxlim: 2490348   bits: 23/22
c ---[1274]---> Adder-cost: 1312   maxlim: 2490348   bits: 23/22
c ---[1273]---> Adder-cost: 1056   maxlim: 2359277   bits: 23/22
c ---[1272]---> Adder-cost: 1348   maxlim: 2621419   bits: 23/22
c ---[1271]---> Adder-cost: 1276   maxlim: 2228206   bits: 23/22
c ---[1270]---> Adder-cost: 1380   maxlim: 2490348   bits: 23/22
c ---[1269]---> Adder-cost: 1032   maxlim: 2424812   bits: 23/22
c ---[1267]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[1266]---> Adder-cost: 1048   maxlim: 2490348   bits: 23/22
c ---[1265]---> Adder-cost: 1346   maxlim: 2359277   bits: 23/22
c ---[1264]---> Adder-cost: 1286   maxlim: 2490348   bits: 23/22
c ---[1263]---> Adder-cost: 1312   maxlim: 2359277   bits: 23/22
c ---[1262]---> Adder-cost: 1332   maxlim: 2621419   bits: 23/22
c ---[1261]---> Adder-cost: 1340   maxlim: 2621419   bits: 23/22
c ---[1260]---> Adder-cost: 1116   maxlim: 2490348   bits: 23/22
c ---[1259]---> Adder-cost: 1092   maxlim: 2490348   bits: 23/22
c ---[1258]---> Adder-cost: 1528   maxlim: 2752490   bits: 23/22
c ---[1257]---> Adder-cost: 1128   maxlim: 2490348   bits: 23/22
c ---[1255]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[1254]---> Adder-cost: 1414   maxlim: 2621419   bits: 23/22
c ---[1253]---> Adder-cost: 1026   maxlim: 2359277   bits: 23/22
c ---[1252]---> Adder-cost: 1130   maxlim: 2621419   bits: 23/22
c ---[1251]---> Adder-cost: 1492   maxlim: 2621419   bits: 23/22
c ---[1250]---> Adder-cost: 1272   maxlim: 2228206   bits: 23/22
c ---[1249]---> Adder-cost: 1072   maxlim: 2490348   bits: 23/22
c ---[1248]---> Adder-cost: 1092   maxlim: 2490348   bits: 23/22
c ---[1247]---> Adder-cost: 1006   maxlim: 2621419   bits: 23/22
c ---[1246]---> Adder-cost: 1502   maxlim: 2752490   bits: 23/22
c ---[1245]---> Adder-cost: 1350   maxlim: 2228206   bits: 23/22
c ---[1243]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[1242]---> Adder-cost: 1418   maxlim: 2752490   bits: 23/22
c ---[1241]---> Adder-cost: 888   maxlim: 2621419   bits: 23/22
c ---[1240]---> Adder-cost: 1436   maxlim: 2621419   bits: 23/22
c ---[1239]---> Adder-cost: 1224   maxlim: 2752490   bits: 23/22
c ---[1238]---> Adder-cost: 978   maxlim: 2228206   bits: 23/22
c ---[1237]---> Adder-cost: 1104   maxlim: 2621419   bits: 23/22
c ---[1236]---> Adder-cost: 1352   maxlim: 2359277   bits: 23/22
c ---[1235]---> Adder-cost: 1326   maxlim: 2162670   bits: 23/22
c ---[1234]---> Adder-cost: 1114   maxlim: 2621419   bits: 23/22
c ---[1233]---> Adder-cost: 1076   maxlim: 2490348   bits: 23/22
c ---[1231]---> BDD-cost:   63
c ---[1229]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[1228]---> Adder-cost: 1168   maxlim: 2621419   bits: 23/22
c ---[1227]---> Adder-cost: 1510   maxlim: 2752490   bits: 23/22
c ---[1226]---> Adder-cost: 1154   maxlim: 2359277   bits: 23/22
c ---[1224]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[1222]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[1220]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[1218]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[1216]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[1214]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[1212]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[1210]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[1208]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[1206]---> BDD-cost:   63
c ---[1204]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[1202]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[1200]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[1198]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[1196]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[1194]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[1192]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[1190]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[1188]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[1186]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[1184]---> BDD-cost:   63
c ---[1182]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[1180]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[1178]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[1176]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[1174]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[1172]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[1170]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[1168]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[1166]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[1164]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[1162]---> BDD-cost:   63
c ---[1160]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[1158]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[1156]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[1154]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[1152]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[1150]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[1148]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[1146]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[1144]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[1142]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[1140]---> BDD-cost:   63
c ---[1138]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[1136]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[1134]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[1132]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[1130]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[1128]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[1126]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[1124]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[1122]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[1120]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[1118]---> BDD-cost:   63
c ---[1116]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[1114]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[1112]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[1110]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[1108]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[1106]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[1104]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[1102]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[1100]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[1098]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[1096]---> BDD-cost:   63
c ---[1094]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[1092]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[1090]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[1088]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[1086]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[1084]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[1082]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[1080]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[1078]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[1076]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[1074]---> BDD-cost:   63
c ---[1072]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[1070]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[1068]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[1066]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[1064]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[1062]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[1060]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[1058]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[1056]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[1054]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[1052]---> BDD-cost:   63
c ---[1050]---> BDD-cost:   63
c ---[1048]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[1046]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[1044]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[1042]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[1040]---> Adder-cost: 763   maxlim: 131071   bits: 18/17
c ---[1038]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[1036]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[1034]---> Adder-cost: 763   maxlim: 131071   bits: 18/17
c ---[1032]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[1030]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[1028]---> BDD-cost:   63
c ---[1026]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[1024]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[1022]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[1020]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[1018]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[1016]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[1014]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[1012]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[1010]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[1008]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[1006]---> BDD-cost:   63
c ---[1004]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[1002]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[1000]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[ 998]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[ 996]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[ 994]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[ 992]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[ 990]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[ 988]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[ 986]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[ 984]---> BDD-cost:   63
c ---[ 982]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[ 980]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[ 978]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[ 976]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[ 974]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[ 972]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[ 970]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[ 968]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[ 966]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[ 964]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[ 962]---> BDD-cost:   63
c ---[ 960]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[ 958]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[ 956]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[ 954]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[ 952]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[ 950]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[ 948]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[ 946]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[ 944]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[ 942]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[ 940]---> BDD-cost:   63
c ---[ 938]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[ 936]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[ 934]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[ 932]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[ 930]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[ 928]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[ 926]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[ 924]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[ 922]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[ 920]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[ 918]---> BDD-cost:   63
c ---[ 916]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[ 914]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[ 912]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[ 910]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[ 908]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[ 906]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[ 904]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[ 902]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[ 900]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[ 898]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[ 896]---> BDD-cost:   63
c ---[ 894]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[ 892]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[ 890]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[ 888]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[ 886]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[ 884]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[ 882]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[ 880]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[ 878]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[ 876]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[ 874]---> BDD-cost:   63
c ---[ 872]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[ 870]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[ 868]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[ 866]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[ 864]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[ 862]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[ 860]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[ 858]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[ 856]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[ 854]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[ 852]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[ 850]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[ 848]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[ 846]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[ 844]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[ 842]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[ 840]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[ 838]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[ 836]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[ 834]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[ 832]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[ 830]---> BDD-cost:   63
c ---[ 828]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[ 826]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[ 824]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[ 822]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[ 820]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[ 818]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[ 816]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[ 814]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[ 812]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[ 810]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[ 808]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[ 806]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[ 804]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[ 802]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[ 800]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[ 798]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[ 796]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[ 794]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[ 792]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[ 790]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[ 788]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[ 786]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[ 784]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[ 782]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[ 780]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[ 778]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[ 776]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[ 774]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[ 772]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[ 770]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[ 768]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[ 766]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[ 764]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[ 762]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[ 760]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[ 758]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[ 756]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[ 754]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[ 752]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[ 750]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[ 748]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[ 746]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[ 744]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[ 742]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[ 740]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[ 738]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[ 736]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[ 734]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[ 732]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[ 730]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[ 728]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[ 726]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[ 724]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[ 722]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[ 720]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[ 718]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[ 716]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[ 714]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[ 712]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[ 710]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[ 708]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[ 706]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[ 704]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[ 702]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[ 700]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[ 698]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[ 696]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[ 694]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[ 692]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[ 690]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[ 688]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[ 686]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[ 684]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[ 682]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[ 680]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[ 678]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[ 676]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[ 674]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[ 672]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[ 670]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[ 668]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[ 666]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[ 664]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[ 662]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[ 660]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[ 658]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[ 656]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[ 654]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[ 652]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[ 650]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[ 648]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[ 646]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[ 644]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[ 642]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[ 640]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[ 638]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[ 636]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[ 634]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[ 632]---> Adder-cost: 763   maxlim: 131071   bits: 18/17
c ---[ 630]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[ 628]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[ 626]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[ 624]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[ 622]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[ 620]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[ 618]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[ 616]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[ 614]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[ 612]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[ 610]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[ 608]---> BDD-cost:   63
c ---[ 606]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[ 604]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[ 602]---> Adder-cost: 14339   maxlim: 1048575   bits: 21/20
c ---[ 600]---> Adder-cost: 13378   maxlim: 1048575   bits: 21/20
c ---[ 598]---> Adder-cost: 15412   maxlim: 1048575   bits: 21/20
c ---[ 596]---> Adder-cost: 13871   maxlim: 1048575   bits: 21/20
c ---[ 594]---> Adder-cost: 14012   maxlim: 1048575   bits: 21/20
c ---[ 592]---> Adder-cost: 13510   maxlim: 1048575   bits: 21/20
c ---[ 590]---> Adder-cost: 13642   maxlim: 1048575   bits: 21/20
c ---[ 588]---> Adder-cost: 14594   maxlim: 1048575   bits: 21/20
c ---[ 586]---> Adder-cost: 14189   maxlim: 1048575   bits: 21/20
c ---[ 584]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[ 582]---> Adder-cost: 14405   maxlim: 1048575   bits: 21/20
c ---[ 580]---> Adder-cost: 13496   maxlim: 1048575   bits: 21/20
c ---[ 578]---> Adder-cost: 14335   maxlim: 1048575   bits: 21/20
c ---[ 576]---> Adder-cost: 14486   maxlim: 1048575   bits: 21/20
c ---[ 574]---> Adder-cost: 14455   maxlim: 1048575   bits: 21/20
c ---[ 572]---> Adder-cost: 14653   maxlim: 1048575   bits: 21/20
c ---[ 570]---> Adder-cost: 14882   maxlim: 1048575   bits: 21/20
c ---[ 568]---> Adder-cost: 14268   maxlim: 1048575   bits: 21/20
c ---[ 566]---> Adder-cost: 15851   maxlim: 1048575   bits: 21/20
c ---[ 564]---> Adder-cost: 15172   maxlim: 1048575   bits: 21/20
c ---[ 562]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[ 560]---> Adder-cost: 15055   maxlim: 1048575   bits: 21/20
c ---[ 558]---> Adder-cost: 15162   maxlim: 1048575   bits: 21/20
c ---[ 556]---> Adder-cost: 15557   maxlim: 1048575   bits: 21/20
c ---[ 554]---> Adder-cost: 15167   maxlim: 1048575   bits: 21/20
c ---[ 552]---> Adder-cost: 14654   maxlim: 1048575   bits: 21/20
c ---[ 550]---> Sorter-cost:  937     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 549]---> Sorter-cost: 1154     Base: 2 2 2 2 2 2 2 2 2 2 2 2 3 5 3
c ---[ 548]---> Sorter-cost: 1375     Base: 2 2 2 2 2 2 2 2 2 2 2 2 7 2 3
c ---[ 547]---> Sorter-cost:  736     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 545]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[ 544]---> Sorter-cost: 1181     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 5
c ---[ 543]---> Sorter-cost:  812     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 5
c ---[ 542]---> Sorter-cost:  785     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 541]---> Sorter-cost: 1343     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 7 3
c ---[ 540]---> Sorter-cost: 1217     Base: 2 2 2 2 2 2 2 2 2 2 2 2 7 5
c ---[ 539]---> Sorter-cost: 1031     Base: 2 2 2 2 2 2 2 2 2 2 2 3 5 2 2
c ---[ 538]---> Sorter-cost: 1056     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 7 3
c ---[ 536]---> Sorter-cost:  893     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 535]---> Sorter-cost: 1239     Base: 2 2 2 2 2 2 2 2 2 2 2 2 7 5
c ---[ 533]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[ 531]---> Sorter-cost: 1177     Base: 2 2 2 2 2 2 2 2 2 2 2 2 7 5
c ---[ 530]---> Sorter-cost: 1453     Base: 2 2 2 2 2 2 2 2 2 2 2 2 13 3
c ---[ 529]---> Sorter-cost: 1287     Base: 2 2 2 2 2 2 2 2 2 2 2 7 3 3
c ---[ 528]---> Sorter-cost: 1187     Base: 2 2 2 2 2 2 2 2 2 3 3 7 5
c ---[ 527]---> Sorter-cost: 1356     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 7 3
c ---[ 525]---> Sorter-cost:  801     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 524]---> Sorter-cost:  926     Base: 2 2 2 2 2 2 2 2 2 2 2 2 5 3 2
c ---[ 522]---> Adder-cost: 785   maxlim: 315391   bits: 20/19
c ---[ 520]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[ 519]---> BDD-cost:   65
c ---[ 517]---> Adder-cost: 785   maxlim: 327039   bits: 20/19
c ---[ 516]---> BDD-cost:   73
c ---[ 514]---> Adder-cost: 785   maxlim: 335999   bits: 20/19
c ---[ 513]---> BDD-cost:   73
c ---[ 511]---> Adder-cost: 785   maxlim: 331519   bits: 20/19
c ---[ 510]---> BDD-cost:   71
c ---[ 508]---> Adder-cost: 785   maxlim: 328703   bits: 20/19
c ---[ 507]---> BDD-cost:   67
c ---[ 505]---> Adder-cost: 785   maxlim: 329471   bits: 20/19
c ---[ 503]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[ 502]---> BDD-cost:   71
c ---[ 500]---> Adder-cost: 785   maxlim: 333823   bits: 20/19
c ---[ 499]---> BDD-cost:   67
c ---[ 497]---> Adder-cost: 785   maxlim: 326783   bits: 20/19
c ---[ 496]---> BDD-cost:   75
c ---[ 494]---> Adder-cost: 785   maxlim: 328959   bits: 20/19
c ---[ 493]---> BDD-cost:   71
c ---[ 491]---> Adder-cost: 785   maxlim: 322815   bits: 20/19
c ---[ 490]---> BDD-cost:   71
c ---[ 488]---> Adder-cost: 785   maxlim: 325247   bits: 20/19
c ---[ 486]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[ 485]---> BDD-cost:   75
c ---[ 483]---> Adder-cost: 785   maxlim: 328447   bits: 20/19
c ---[ 482]---> BDD-cost:   73
c ---[ 480]---> Adder-cost: 785   maxlim: 301439   bits: 20/19
c ---[ 479]---> BDD-cost:   75
c ---[ 477]---> Adder-cost: 785   maxlim: 327551   bits: 20/19
c ---[ 476]---> BDD-cost:   75
c ---[ 474]---> Adder-cost: 785   maxlim: 323455   bits: 20/19
c ---[ 473]---> BDD-cost:   75
c ---[ 471]---> Adder-cost: 785   maxlim: 314495   bits: 20/19
c ---[ 469]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[ 468]---> BDD-cost:   73
c ---[ 466]---> Adder-cost: 785   maxlim: 323967   bits: 20/19
c ---[ 465]---> BDD-cost:   73
c ---[ 463]---> Adder-cost: 785   maxlim: 322815   bits: 20/19
c ---[ 462]---> BDD-cost:   71
c ---[ 460]---> Adder-cost: 785   maxlim: 318591   bits: 20/19
c ---[ 459]---> BDD-cost:   73
c ---[ 457]---> Adder-cost: 785   maxlim: 331263   bits: 20/19
c ---[ 456]---> BDD-cost:   71
c ---[ 454]---> Adder-cost: 785   maxlim: 330367   bits: 20/19
c ---[ 452]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[ 451]---> BDD-cost:   73
c ---[ 449]---> Adder-cost: 785   maxlim: 314623   bits: 20/19
c ---[ 448]---> BDD-cost:   73
c ---[ 446]---> Adder-cost: 785   maxlim: 319231   bits: 20/19
c ---[ 445]---> BDD-cost:   71
c ---[ 443]---> Adder-cost: 785   maxlim: 323199   bits: 20/19
c ---[ 442]---> BDD-cost:   73
c ---[ 440]---> Adder-cost: 788   maxlim: 1048575   bits: 21/20
c ---[ 439]---> BDD-cost:   58
c ---[ 437]---> Adder-cost: 788   maxlim: 1048575   bits: 21/20
c ---[ 435]---> BDD-cost:   63
c ---[ 433]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[ 432]---> BDD-cost:   58
c ---[ 430]---> Adder-cost: 788   maxlim: 1048575   bits: 21/20
c ---[ 429]---> BDD-cost:   58
c ---[ 427]---> Adder-cost: 788   maxlim: 1048575   bits: 21/20
c ---[ 426]---> BDD-cost:   58
c ---[ 424]---> Adder-cost: 788   maxlim: 1048575   bits: 21/20
c ---[ 423]---> BDD-cost:   58
c ---[ 421]---> Adder-cost: 788   maxlim: 1048575   bits: 21/20
c ---[ 420]---> BDD-cost:   58
c ---[ 418]---> Adder-cost: 788   maxlim: 1048575   bits: 21/20
c ---[ 416]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[ 415]---> BDD-cost:   58
c ---[ 413]---> Adder-cost: 788   maxlim: 1048575   bits: 21/20
c ---[ 412]---> BDD-cost:   58
c ---[ 410]---> Adder-cost: 788   maxlim: 1048575   bits: 21/20
c ---[ 409]---> BDD-cost:   58
c ---[ 407]---> Adder-cost: 788   maxlim: 1048575   bits: 21/20
c ---[ 406]---> BDD-cost:   58
c ---[ 404]---> Adder-cost: 788   maxlim: 1048575   bits: 21/20
c ---[ 403]---> BDD-cost:   58
c ---[ 401]---> Adder-cost: 788   maxlim: 1048575   bits: 21/20
c ---[ 399]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[ 398]---> BDD-cost:   58
c ---[ 396]---> Adder-cost: 788   maxlim: 1048575   bits: 21/20
c ---[ 395]---> BDD-cost:   58
c ---[ 393]---> Adder-cost: 788   maxlim: 1048575   bits: 21/20
c ---[ 392]---> BDD-cost:   58
c ---[ 390]---> Adder-cost: 788   maxlim: 1048575   bits: 21/20
c ---[ 389]---> BDD-cost:   58
c ---[ 387]---> Adder-cost: 788   maxlim: 1048575   bits: 21/20
c ---[ 386]---> BDD-cost:   58
c ---[ 384]---> Adder-cost: 788   maxlim: 1048575   bits: 21/20
c ---[ 382]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[ 381]---> BDD-cost:   58
c ---[ 379]---> Adder-cost: 788   maxlim: 1048575   bits: 21/20
c ---[ 378]---> BDD-cost:   58
c ---[ 376]---> Adder-cost: 788   maxlim: 1048575   bits: 21/20
c ---[ 375]---> BDD-cost:   58
c ---[ 373]---> Adder-cost: 788   maxlim: 1048575   bits: 21/20
c ---[ 372]---> BDD-cost:   58
c ---[ 370]---> Adder-cost: 788   maxlim: 1048575   bits: 21/20
c ---[ 369]---> BDD-cost:   58
c ---[ 367]---> Adder-cost: 788   maxlim: 1048575   bits: 21/20
c ---[ 365]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[ 364]---> BDD-cost:   58
c ---[ 362]---> Adder-cost: 788   maxlim: 1048575   bits: 21/20
c ---[ 361]---> BDD-cost:   58
c ---[ 359]---> Adder-cost: 788   maxlim: 1048575   bits: 21/20
c ---[ 358]---> BDD-cost:   58
c ---[ 357]---> Adder-cost: 494   maxlim: 131070   bits: 18/17
c ---[ 356]---> Adder-cost: 642   maxlim: 131070   bits: 18/17
c ---[ 355]---> Adder-cost: 752   maxlim: 131070   bits: 18/17
c ---[ 354]---> Adder-cost: 494   maxlim: 131070   bits: 18/17
c ---[ 353]---> Adder-cost: 752   maxlim: 131070   bits: 18/17
c ---[ 351]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[ 350]---> Adder-cost: 752   maxlim: 131070   bits: 18/17
c ---[ 349]---> Adder-cost: 463   maxlim: 131070   bits: 18/17
c ---[ 348]---> Adder-cost: 503   maxlim: 131070   bits: 18/17
c ---[ 346]---> Adder-cost: 746   maxlim: 131070   bits: 18/17
c ---[ 345]---> Adder-cost: 752   maxlim: 131070   bits: 18/17
c ---[ 344]---> Adder-cost: 752   maxlim: 131070   bits: 18/17
c ---[ 343]---> Adder-cost: 474   maxlim: 131070   bits: 18/17
c ---[ 342]---> Adder-cost: 476   maxlim: 131070   bits: 18/17
c ---[ 341]---> Adder-cost: 752   maxlim: 131070   bits: 18/17
c ---[ 339]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[ 338]---> Adder-cost: 536   maxlim: 131070   bits: 18/17
c ---[ 337]---> Adder-cost: 472   maxlim: 131070   bits: 18/17
c ---[ 336]---> Adder-cost: 752   maxlim: 131070   bits: 18/17
c ---[ 335]---> Adder-cost: 740   maxlim: 131070   bits: 18/17
c ---[ 334]---> Adder-cost: 649   maxlim: 131070   bits: 18/17
c ---[ 333]---> Adder-cost: 613   maxlim: 131070   bits: 18/17
c ---[ 331]---> Adder-cost: 673   maxlim: 131070   bits: 18/17
c ---[ 330]---> Adder-cost: 716   maxlim: 131070   bits: 18/17
c ---[ 329]---> Adder-cost: 744   maxlim: 131070   bits: 18/17
c ---[ 327]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[ 326]---> Adder-cost: 577   maxlim: 131070   bits: 18/17
c ---[ 325]---> Adder-cost: 545   maxlim: 131070   bits: 18/17
c ---[ 324]---> Adder-cost: 502   maxlim: 131070   bits: 18/17
c ---[ 323]---> Adder-cost: 748   maxlim: 131070   bits: 18/17
c ---[ 322]---> Adder-cost: 523   maxlim: 131070   bits: 18/17
c ---[ 321]---> Adder-cost: 572   maxlim: 131070   bits: 18/17
c ---[ 320]---> Adder-cost: 532   maxlim: 131070   bits: 18/17
c ---[ 319]---> Adder-cost: 610   maxlim: 131070   bits: 18/17
c ---[ 318]---> Adder-cost: 622   maxlim: 131070   bits: 18/17
c ---[ 317]---> Adder-cost: 752   maxlim: 131070   bits: 18/17
c ---[ 315]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[ 314]---> Adder-cost: 678   maxlim: 131070   bits: 18/17
c ---[ 313]---> Adder-cost: 684   maxlim: 131070   bits: 18/17
c ---[ 312]---> Adder-cost: 682   maxlim: 131070   bits: 18/17
c ---[ 311]---> Adder-cost: 718   maxlim: 131070   bits: 18/17
c ---[ 310]---> Adder-cost: 750   maxlim: 131070   bits: 18/17
c ---[ 309]---> Adder-cost: 718   maxlim: 131070   bits: 18/17
c ---[ 308]---> Adder-cost: 748   maxlim: 131070   bits: 18/17
c ---[ 307]---> Adder-cost: 752   maxlim: 131070   bits: 18/17
c ---[ 306]---> Adder-cost: 752   maxlim: 131070   bits: 18/17
c ---[ 305]---> Adder-cost: 544   maxlim: 131070   bits: 18/17
c ---[ 303]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[ 302]---> Adder-cost: 490   maxlim: 131070   bits: 18/17
c ---[ 301]---> Adder-cost: 486   maxlim: 131070   bits: 18/17
c ---[ 300]---> Adder-cost: 492   maxlim: 131070   bits: 18/17
c ---[ 299]---> Adder-cost: 499   maxlim: 131070   bits: 18/17
c ---[ 298]---> Adder-cost: 749   maxlim: 131070   bits: 18/17
c ---[ 297]---> Adder-cost: 576   maxlim: 131070   bits: 18/17
c ---[ 296]---> Adder-cost: 534   maxlim: 131070   bits: 18/17
c ---[ 295]---> Adder-cost: 580   maxlim: 131070   bits: 18/17
c ---[ 294]---> Adder-cost: 684   maxlim: 131070   bits: 18/17
c ---[ 293]---> Adder-cost: 648   maxlim: 131070   bits: 18/17
c ---[ 291]---> BDD-cost:   63
c ---[ 289]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[ 288]---> Adder-cost: 508   maxlim: 131070   bits: 18/17
c ---[ 287]---> Adder-cost: 752   maxlim: 131070   bits: 18/17
c ---[ 286]---> Adder-cost: 543   maxlim: 131070   bits: 18/17
c ---[ 285]---> Adder-cost: 579   maxlim: 131070   bits: 18/17
c ---[ 284]---> Adder-cost: 712   maxlim: 131070   bits: 18/17
c ---[ 283]---> Adder-cost: 749   maxlim: 131070   bits: 18/17
c ---[ 282]---> Adder-cost: 456   maxlim: 131070   bits: 18/17
c ---[ 281]---> Adder-cost: 749   maxlim: 131070   bits: 18/17
c ---[ 280]---> Adder-cost: 736   maxlim: 131070   bits: 18/17
c ---[ 279]---> Adder-cost: 740   maxlim: 131070   bits: 18/17
c ---[ 277]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[ 276]---> Adder-cost: 580   maxlim: 131070   bits: 18/17
c ---[ 275]---> Adder-cost: 570   maxlim: 131070   bits: 18/17
c ---[ 274]---> Adder-cost: 649   maxlim: 131070   bits: 18/17
c ---[ 273]---> Adder-cost: 678   maxlim: 131070   bits: 18/17
c ---[ 272]---> Adder-cost: 613   maxlim: 131070   bits: 18/17
c ---[ 271]---> Adder-cost: 718   maxlim: 131070   bits: 18/17
c ---[ 270]---> Adder-cost: 752   maxlim: 131070   bits: 18/17
c ---[ 269]---> Adder-cost: 752   maxlim: 131070   bits: 18/17
c ---[ 268]---> Adder-cost: 748   maxlim: 131070   bits: 18/17
c ---[ 267]---> Adder-cost: 646   maxlim: 131070   bits: 18/17
c ---[ 265]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[ 264]---> Adder-cost: 498   maxlim: 131070   bits: 18/17
c ---[ 263]---> Adder-cost: 546   maxlim: 131070   bits: 18/17
c ---[ 262]---> Adder-cost: 752   maxlim: 131070   bits: 18/17
c ---[ 261]---> Adder-cost: 465   maxlim: 131070   bits: 18/17
c ---[ 260]---> Adder-cost: 505   maxlim: 131070   bits: 18/17
c ---[ 259]---> Adder-cost: 752   maxlim: 131070   bits: 18/17
c ---[ 258]---> Adder-cost: 752   maxlim: 131070   bits: 18/17
c ---[ 257]---> Adder-cost: 748   maxlim: 131070   bits: 18/17
c ---[ 256]---> Adder-cost: 648   maxlim: 131070   bits: 18/17
c ---[ 255]---> Adder-cost: 580   maxlim: 131070   bits: 18/17
c ---[ 253]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[ 252]---> Adder-cost: 740   maxlim: 131070   bits: 18/17
c ---[ 251]---> Adder-cost: 680   maxlim: 131070   bits: 18/17
c ---[ 250]---> Adder-cost: 573   maxlim: 131070   bits: 18/17
c ---[ 249]---> Adder-cost: 542   maxlim: 131070   bits: 18/17
c ---[ 248]---> Adder-cost: 681   maxlim: 131070   bits: 18/17
c ---[ 247]---> Adder-cost: 542   maxlim: 131070   bits: 18/17
c ---[ 246]---> Adder-cost: 740   maxlim: 131070   bits: 18/17
c ---[ 245]---> Adder-cost: 738   maxlim: 131070   bits: 18/17
c ---[ 244]---> Adder-cost: 570   maxlim: 131070   bits: 18/17
c ---[ 243]---> Adder-cost: 752   maxlim: 131070   bits: 18/17
c ---[ 241]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[ 240]---> Adder-cost: 542   maxlim: 131070   bits: 18/17
c ---[ 239]---> Adder-cost: 547   maxlim: 131070   bits: 18/17
c ---[ 238]---> Adder-cost: 637   maxlim: 131070   bits: 18/17
c ---[ 237]---> Adder-cost: 750   maxlim: 131070   bits: 18/17
c ---[ 236]---> Adder-cost: 752   maxlim: 131070   bits: 18/17
c ---[ 235]---> Adder-cost: 544   maxlim: 131070   bits: 18/17
c ---[ 234]---> Adder-cost: 543   maxlim: 131070   bits: 18/17
c ---[ 233]---> Adder-cost: 488   maxlim: 131070   bits: 18/17
c ---[ 232]---> Adder-cost: 518   maxlim: 131070   bits: 18/17
c ---[ 231]---> Adder-cost: 752   maxlim: 131070   bits: 18/17
c ---[ 229]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[ 228]---> Adder-cost: 578   maxlim: 131070   bits: 18/17
c ---[ 227]---> Adder-cost: 530   maxlim: 131070   bits: 18/17
c ---[ 226]---> Adder-cost: 748   maxlim: 131070   bits: 18/17
c ---[ 225]---> Adder-cost: 574   maxlim: 131070   bits: 18/17
c ---[ 224]---> Adder-cost: 578   maxlim: 131070   bits: 18/17
c ---[ 223]---> Adder-cost: 646   maxlim: 131070   bits: 18/17
c ---[ 222]---> Adder-cost: 645   maxlim: 131070   bits: 18/17
c ---[ 221]---> Adder-cost: 613   maxlim: 131070   bits: 18/17
c ---[ 220]---> Adder-cost: 539   maxlim: 131070   bits: 18/17
c ---[ 219]---> Adder-cost: 543   maxlim: 131070   bits: 18/17
c ---[ 217]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[ 216]---> Adder-cost: 752   maxlim: 131070   bits: 18/17
c ---[ 215]---> Adder-cost: 576   maxlim: 131070   bits: 18/17
c ---[ 214]---> Adder-cost: 494   maxlim: 131070   bits: 18/17
c ---[ 213]---> Adder-cost: 748   maxlim: 131070   bits: 18/17
c ---[ 212]---> Adder-cost: 748   maxlim: 131070   bits: 18/17
c ---[ 211]---> Adder-cost: 530   maxlim: 131070   bits: 18/17
c ---[ 210]---> Adder-cost: 578   maxlim: 131070   bits: 18/17
c ---[ 209]---> Adder-cost: 578   maxlim: 131070   bits: 18/17
c ---[ 208]---> Adder-cost: 576   maxlim: 131070   bits: 18/17
c ---[ 207]---> Adder-cost: 684   maxlim: 131070   bits: 18/17
c ---[ 205]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[ 204]---> Adder-cost: 578   maxlim: 131070   bits: 18/17
c ---[ 203]---> Adder-cost: 541   maxlim: 131070   bits: 18/17
c ---[ 202]---> Adder-cost: 649   maxlim: 131070   bits: 18/17
c ---[ 201]---> Adder-cost: 578   maxlim: 131070   bits: 18/17
c ---[ 200]---> Adder-cost: 746   maxlim: 131070   bits: 18/17
c ---[ 199]---> Adder-cost: 712   maxlim: 131070   bits: 18/17
c ---[ 198]---> Adder-cost: 752   maxlim: 131070   bits: 18/17
c ---[ 197]---> Adder-cost: 752   maxlim: 131070   bits: 18/17
c ---[ 196]---> Adder-cost: 752   maxlim: 131070   bits: 18/17
c ---[ 195]---> Adder-cost: 482   maxlim: 131070   bits: 18/17
c ---[ 193]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[ 192]---> Adder-cost: 494   maxlim: 131070   bits: 18/17
c ---[ 191]---> Adder-cost: 472   maxlim: 131070   bits: 18/17
c ---[ 190]---> Adder-cost: 485   maxlim: 131070   bits: 18/17
c ---[ 189]---> Adder-cost: 578   maxlim: 131070   bits: 18/17
c ---[ 188]---> Adder-cost: 744   maxlim: 131070   bits: 18/17
c ---[ 187]---> Adder-cost: 745   maxlim: 131070   bits: 18/17
c ---[ 186]---> Adder-cost: 580   maxlim: 131070   bits: 18/17
c ---[ 185]---> Adder-cost: 682   maxlim: 131070   bits: 18/17
c ---[ 184]---> Adder-cost: 747   maxlim: 131070   bits: 18/17
c ---[ 183]---> Adder-cost: 718   maxlim: 131070   bits: 18/17
c ---[ 181]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[ 180]---> Adder-cost: 545   maxlim: 131070   bits: 18/17
c ---[ 179]---> Adder-cost: 748   maxlim: 131070   bits: 18/17
c ---[ 178]---> Adder-cost: 750   maxlim: 131070   bits: 18/17
c ---[ 177]---> Adder-cost: 750   maxlim: 131070   bits: 18/17
c ---[ 176]---> Adder-cost: 745   maxlim: 131070   bits: 18/17
c ---[ 175]---> Adder-cost: 740   maxlim: 131070   bits: 18/17
c ---[ 174]---> Adder-cost: 487   maxlim: 131070   bits: 18/17
c ---[ 173]---> Adder-cost: 538   maxlim: 131070   bits: 18/17
c ---[ 172]---> Adder-cost: 744   maxlim: 131070   bits: 18/17
c ---[ 171]---> Adder-cost: 644   maxlim: 131070   bits: 18/17
c ---[ 169]---> BDD-cost:   63
c ---[ 167]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[ 165]---> Adder-cost: 611   maxlim: 131070   bits: 18/17
c ---[ 164]---> Adder-cost: 684   maxlim: 131070   bits: 18/17
c ---[ 163]---> Adder-cost: 750   maxlim: 131070   bits: 18/17
c ---[ 162]---> Adder-cost: 748   maxlim: 131070   bits: 18/17
c ---[ 161]---> Adder-cost: 746   maxlim: 131070   bits: 18/17
c ---[ 160]---> Adder-cost: 545   maxlim: 131070   bits: 18/17
c ---[ 159]---> Adder-cost: 748   maxlim: 131070   bits: 18/17
c ---[ 158]---> Adder-cost: 506   maxlim: 131070   bits: 18/17
c ---[ 157]---> Adder-cost: 548   maxlim: 131070   bits: 18/17
c ---[ 155]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[ 154]---> Adder-cost: 582   maxlim: 131070   bits: 18/17
c ---[ 153]---> Adder-cost: 496   maxlim: 131070   bits: 18/17
c ---[ 152]---> Adder-cost: 578   maxlim: 131070   bits: 18/17
c ---[ 151]---> Adder-cost: 477   maxlim: 131070   bits: 18/17
c ---[ 150]---> Adder-cost: 712   maxlim: 131070   bits: 18/17
c ---[ 149]---> Adder-cost: 540   maxlim: 131070   bits: 18/17
c ---[ 148]---> Adder-cost: 646   maxlim: 131070   bits: 18/17
c ---[ 147]---> Adder-cost: 613   maxlim: 131070   bits: 18/17
c ---[ 146]---> Adder-cost: 537   maxlim: 131070   bits: 18/17
c ---[ 145]---> Adder-cost: 544   maxlim: 131070   bits: 18/17
c ---[ 143]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[ 142]---> Adder-cost: 750   maxlim: 131070   bits: 18/17
c ---[ 141]---> Adder-cost: 712   maxlim: 131070   bits: 18/17
c ---[ 140]---> Adder-cost: 537   maxlim: 131070   bits: 18/17
c ---[ 139]---> Adder-cost: 541   maxlim: 131070   bits: 18/17
c ---[ 138]---> Adder-cost: 458   maxlim: 131070   bits: 18/17
c ---[ 137]---> Adder-cost: 632   maxlim: 131070   bits: 18/17
c ---[ 135]---> Adder-cost: 715   maxlim: 131070   bits: 18/17
c ---[ 134]---> Adder-cost: 625   maxlim: 131070   bits: 18/17
c ---[ 133]---> Adder-cost: 603   maxlim: 131070   bits: 18/17
c ---[ 131]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[ 130]---> Adder-cost: 735   maxlim: 131070   bits: 18/17
c ---[ 129]---> Adder-cost: 692   maxlim: 131070   bits: 18/17
c ---[ 128]---> Adder-cost: 748   maxlim: 131070   bits: 18/17
c ---[ 127]---> Adder-cost: 541   maxlim: 131070   bits: 18/17
c ---[ 125]---> Adder-cost: 500   maxlim: 131070   bits: 18/17
c ---[ 124]---> Adder-cost: 423   maxlim: 131070   bits: 18/17
c ---[ 123]---> Adder-cost: 752   maxlim: 131070   bits: 18/17
c ---[ 122]---> Adder-cost: 536   maxlim: 131070   bits: 18/17
c ---[ 121]---> Adder-cost: 578   maxlim: 131070   bits: 18/17
c ---[ 119]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[ 118]---> Adder-cost: 752   maxlim: 131070   bits: 18/17
c ---[ 117]---> Adder-cost: 620   maxlim: 131070   bits: 18/17
c ---[ 116]---> Adder-cost: 736   maxlim: 131070   bits: 18/17
c ---[ 115]---> Adder-cost: 508   maxlim: 131070   bits: 18/17
c ---[ 114]---> Adder-cost: 748   maxlim: 131070   bits: 18/17
c ---[ 113]---> Adder-cost: 718   maxlim: 131070   bits: 18/17
c ---[ 112]---> Adder-cost: 579   maxlim: 131070   bits: 18/17
c ---[ 111]---> Adder-cost: 750   maxlim: 131070   bits: 18/17
c ---[ 110]---> Adder-cost: 741   maxlim: 131070   bits: 18/17
c ---[ 109]---> Adder-cost: 745   maxlim: 131070   bits: 18/17
c ---[ 107]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[ 106]---> Adder-cost: 496   maxlim: 131070   bits: 18/17
c ---[ 105]---> Adder-cost: 417   maxlim: 131070   bits: 18/17
c ---[ 104]---> Adder-cost: 748   maxlim: 131070   bits: 18/17
c ---[ 103]---> Adder-cost: 580   maxlim: 131070   bits: 18/17
c ---[ 102]---> Adder-cost: 742   maxlim: 131070   bits: 18/17
c ---[ 101]---> Adder-cost: 744   maxlim: 131070   bits: 18/17
c ---[ 100]---> Adder-cost: 524   maxlim: 131070   bits: 18/17
c ---[  99]---> Adder-cost: 537   maxlim: 131070   bits: 18/17
c ---[  98]---> Adder-cost: 682   maxlim: 131070   bits: 18/17
c ---[  97]---> Adder-cost: 612   maxlim: 131070   bits: 18/17
c ---[  95]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[  94]---> Adder-cost: 714   maxlim: 131070   bits: 18/17
c ---[  93]---> Adder-cost: 748   maxlim: 131070   bits: 18/17
c ---[  92]---> Adder-cost: 752   maxlim: 131070   bits: 18/17
c ---[  91]---> Adder-cost: 752   maxlim: 131070   bits: 18/17
c ---[  90]---> Adder-cost: 490   maxlim: 131070   bits: 18/17
c ---[  89]---> Adder-cost: 478   maxlim: 131070   bits: 18/17
c ---[  88]---> Adder-cost: 576   maxlim: 131070   bits: 18/17
c ---[  86]---> Adder-cost: 749   maxlim: 131070   bits: 18/17
c ---[  85]---> Adder-cost: 740   maxlim: 131070   bits: 18/17
c ---[  83]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[  82]---> Adder-cost: 540   maxlim: 131070   bits: 18/17
c ---[  81]---> Adder-cost: 516   maxlim: 131070   bits: 18/17
c ---[  79]---> Adder-cost: 541   maxlim: 131070   bits: 18/17
c ---[  78]---> Adder-cost: 752   maxlim: 131070   bits: 18/17
c ---[  77]---> Adder-cost: 484   maxlim: 131070   bits: 18/17
c ---[  76]---> Adder-cost: 491   maxlim: 131070   bits: 18/17
c ---[  75]---> Adder-cost: 746   maxlim: 131070   bits: 18/17
c ---[  74]---> Adder-cost: 500   maxlim: 131070   bits: 18/17
c ---[  73]---> Adder-cost: 752   maxlim: 131070   bits: 18/17
c ---[  71]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[  70]---> Adder-cost: 745   maxlim: 131070   bits: 18/17
c ---[  69]---> Adder-cost: 644   maxlim: 131070   bits: 18/17
c ---[  68]---> Adder-cost: 748   maxlim: 131070   bits: 18/17
c ---[  67]---> Adder-cost: 626   maxlim: 131070   bits: 18/17
c ---[  66]---> Adder-cost: 548   maxlim: 131070   bits: 18/17
c ---[  65]---> Adder-cost: 539   maxlim: 131070   bits: 18/17
c ---[  64]---> Adder-cost: 712   maxlim: 131070   bits: 18/17
c ---[  63]---> Adder-cost: 750   maxlim: 131070   bits: 18/17
c ---[  62]---> Adder-cost: 545   maxlim: 131070   bits: 18/17
c ---[  59]---> Adder-cost: 766   maxlim: 131071   bits: 18/17
c ---[  58]---> Adder-cost: 542   maxlim: 131070   bits: 18/17
c ---[  57]---> Adder-cost: 738   maxlim: 131070   bits: 18/17
c ---[  56]---> Adder-cost: 588   maxlim: 131070   bits: 18/17
c ---[  55]---> Adder-cost: 542   maxlim: 131070   bits: 18/17
c ---[  54]---> Adder-cost: 568   maxlim: 131070   bits: 18/17
c ---[  53]---> Adder-cost: 577   maxlim: 131070   bits: 18/17
c ---[  52]---> Adder-cost: 646   maxlim: 131070   bits: 18/17
c ---[  51]---> Adder-cost: 718   maxlim: 131070   bits: 18/17
c ---[  50]---> Adder-cost: 547   maxlim: 131070   bits: 18/17
c ---[  49]---> Adder-cost: 540   maxlim: 131070   bits: 18/17
c ---[  48]---> BDD-cost:    2
c ---[  47]---> BDD-cost:    5
c ---[  46]---> BDD-cost:    3
c ---[  45]---> BDD-cost:    6
c ---[  44]---> BDD-cost:    6
c ---[  43]---> BDD-cost:    6
c ---[  42]---> BDD-cost:    6
c ---[  41]---> BDD-cost:    6
c ---[  40]---> BDD-cost:    4
c ---[  39]---> BDD-cost:    4
c ---[  38]---> BDD-cost:    4
c ---[  37]---> BDD-cost:    2
c ---[  36]---> BDD-cost:    4
c ---[  35]---> BDD-cost:    6
c ---[  34]---> BDD-cost:    5
c ---[  33]---> Adder-cost: 478   maxlim: 65534   bits: 17/16
c ---[  32]---> Adder-cost: 368   maxlim: 65534   bits: 17/16
c ---[  31]---> Adder-cost: 668   maxlim: 65534   bits: 17/16
c ---[  30]---> Adder-cost: 508   maxlim: 65534   bits: 17/16
c ---[  29]---> Adder-cost: 642   maxlim: 65534   bits: 17/16
c ---[  28]---> Adder-cost: 544   maxlim: 65534   bits: 17/16
c ---[  27]---> Adder-cost: 432   maxlim: 65534   bits: 17/16
c ---[  26]---> Adder-cost: 566   maxlim: 65534   bits: 17/16
c ---[  25]---> Adder-cost: 450   maxlim: 65534   bits: 17/16
c ---[  24]---> Adder-cost: 414   maxlim: 65534   bits: 17/16
c ---[  23]---> Adder-cost: 508   maxlim: 65534   bits: 17/16
c ---[  22]---> Adder-cost: 462   maxlim: 65534   bits: 17/16
c ---[  21]---> Adder-cost: 500   maxlim: 32766   bits: 16/15
c ---[  20]---> Adder-cost: 643   maxlim: 32766   bits: 16/15
c ---[  19]---> Adder-cost: 470   maxlim: 32766   bits: 16/15
c ---[  18]---> Adder-cost: 376   maxlim: 65534   bits: 17/16
c ---[  17]---> Adder-cost: 420   maxlim: 65534   bits: 17/16
c ---[  16]---> Adder-cost: 604   maxlim: 65534   bits: 17/16
c ---[  15]---> Adder-cost: 640   maxlim: 65534   bits: 17/16
c ---[  14]---> Adder-cost: 514   maxlim: 65534   bits: 17/16
c ---[  13]---> Adder-cost: 438   maxlim: 65534   bits: 17/16
c ---[  12]---#### END SOLVER DATA ####
#### BEGIN WATCHER DATA ####
Enforcing CPU limit (will send SIGTERM then SIGKILL): 1200 seconds
Enforcing CPUTime (will send SIGXCPU) limit: 1230 seconds
Enforcing VSIZE limit: 943718400 bytes
Raw data (loadavg): 0.81 0.92 0.90 2/55 14156
Raw data (stat): 14156 (runsolver) R 14155 30927 30926 0 -1 64 4 0 0 0 0 0 0 0 20 0 1 0 423795433 1052672 99 4294967295 134512640 135381576 3221224432 3221219676 135158418 0 2147483391 7 90112 0 0 0 17 1 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0009 s]
Raw data (loadavg): 0.84 0.93 0.90 2/55 14156
Raw data (stat): 14156 (minisat+) R 14155 30927 30926 0 -1 0 26685 0 0 0 919 79 0 0 25 0 1 0 423795433 123490304 22279 4294967295 134512640 134672761 3221224544 3221223896 1075730078 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30149 22280 603 41 0 30108 0
vsize: 120596
[startup+20.0014 s]
Raw data (loadavg): 0.87 0.93 0.90 2/55 14156
Raw data (stat): 14156 (minisat+) R 14155 30927 30926 0 -1 0 32069 0 0 0 1907 92 0 0 25 0 1 0 423795433 145498112 27663 4294967295 134512640 134672761 3221224544 3221223936 134580837 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 35522 27663 603 41 0 35481 0
vsize: 142088
[startup+30.0011 s]
Raw data (loadavg): 0.89 0.93 0.90 2/55 14156
Raw data (stat): 14156 (minisat+) R 14155 30927 30926 0 -1 0 32069 0 0 0 2907 92 0 0 25 0 1 0 423795433 145498112 27663 4294967295 134512640 134672761 3221224544 3221223936 134580795 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 35522 27663 603 41 0 35481 0
vsize: 142088
[startup+40.0022 s]
Raw data (loadavg): 0.90 0.93 0.90 2/55 14156
Raw data (stat): 14156 (minisat+) R 14155 30927 30926 0 -1 0 32069 0 0 0 3907 92 0 0 25 0 1 0 423795433 145498112 27663 4294967295 134512640 134672761 3221224544 3221223936 134581428 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 35522 27663 603 41 0 35481 0
vsize: 142088
[startup+50.0024 s]
Raw data (loadavg): 0.92 0.93 0.90 2/55 14156
Raw data (stat): 14156 (minisat+) R 14155 30927 30926 0 -1 0 32097 0 0 0 4907 93 0 0 25 0 1 0 423795433 139124736 26126 4294967295 134512640 134672761 3221224544 3221222736 134544467 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33966 26126 603 41 0 33925 0
vsize: 135864
[startup+60.0021 s]
Raw data (loadavg): 0.93 0.94 0.90 2/55 14156
Raw data (stat): 14156 (minisat+) R 14155 30927 30926 0 -1 0 34540 0 0 0 5901 99 0 0 25 0 1 0 423795433 150847488 28569 4294967295 134512640 134672761 3221224544 3221222736 134522994 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 36828 28569 603 41 0 36787 0
vsize: 147312
[startup+70.0018 s]
Raw data (loadavg): 0.94 0.94 0.90 2/55 14156
Raw data (stat): 14156 (minisat+) R 14155 30927 30926 0 -1 0 38404 0 0 0 6889 110 0 0 25 0 1 0 423795433 169439232 32433 4294967295 134512640 134672761 3221224544 3221220992 134523714 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 41367 32433 603 41 0 41326 0
vsize: 165468
[startup+80.0018 s]
Raw data (loadavg): 0.95 0.94 0.90 2/55 14156
Raw data (stat): 14156 (minisat+) R 14155 30927 30926 0 -1 0 40753 0 0 0 7883 116 0 0 25 0 1 0 423795433 170086400 33464 4294967295 134512640 134672761 3221224544 3221221760 134545085 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 41525 33464 603 41 0 41484 0
vsize: 166100
[startup+90.0024 s]
Raw data (loadavg): 0.96 0.94 0.90 2/55 14156
Raw data (stat): 14156 (minisat+) R 14155 30927 30926 0 -1 0 43728 0 0 0 8874 125 0 0 25 0 1 0 423795433 190435328 36439 4294967295 134512640 134672761 3221224544 3221221216 1075349701 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 46493 36439 603 41 0 46452 0
vsize: 185972
[startup+100.002 s]
Raw data (loadavg): 0.96 0.94 0.91 2/55 14156
Raw data (stat): 14156 (minisat+) R 14155 30927 30926 0 -1 0 50992 0 0 0 9857 143 0 0 25 0 1 0 423795433 206274560 41066 4294967295 134512640 134672761 3221224544 3221223536 134597188 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 50360 41066 603 41 0 50319 0
vsize: 201440
[startup+110.003 s]
Raw data (loadavg): 0.97 0.94 0.91 2/55 14156
Raw data (stat): 14156 (minisat+) R 14155 30927 30926 0 -1 0 53036 0 0 0 10851 149 0 0 25 0 1 0 423795433 211587072 43110 4294967295 134512640 134672761 3221224544 3221222896 134599063 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 51657 43110 603 41 0 51616 0
vsize: 206628
[startup+120.002 s]
Raw data (loadavg): 0.97 0.94 0.91 2/55 14156
Raw data (stat): 14156 (minisat+) R 14155 30927 30926 0 -1 0 57509 0 0 0 11840 160 0 0 25 0 1 0 423795433 247431168 47002 4294967295 134512640 134672761 3221224544 3221223440 134522369 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 60408 47002 603 41 0 60367 0
vsize: 241632
[startup+130.002 s]
Raw data (loadavg): 0.98 0.95 0.91 2/55 14156
Raw data (stat): 14156 (minisat+) R 14155 30927 30926 0 -1 0 59967 0 0 0 12834 166 0 0 25 0 1 0 423795433 250912768 48381 4294967295 134512640 134672761 3221224544 3221221968 134523222 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 61258 48381 603 41 0 61217 0
vsize: 245032
[startup+140.003 s]
Raw data (loadavg): 0.98 0.95 0.91 2/55 14156
Raw data (stat): 14156 (minisat+) R 14155 30927 30926 0 -1 0 61126 0 0 0 13832 168 0 0 25 0 1 0 423795433 252792832 49125 4294967295 134512640 134672761 3221224544 3221222544 134544288 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 61717 49125 603 41 0 61676 0
vsize: 246868
[startup+150.004 s]
Raw data (loadavg): 0.98 0.95 0.91 2/55 14156
Raw data (stat): 14156 (minisat+) R 14155 30927 30926 0 -1 0 76115 0 0 0 14799 201 0 0 25 0 1 0 423795433 279519232 57929 4294967295 134512640 134672761 3221224544 3221220456 1075350918 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 68242 57929 603 41 0 68201 0
vsize: 272968
[startup+160.005 s]
Raw data (loadavg): 0.98 0.95 0.91 2/55 14156
Raw data (stat): 14156 (minisat+) R 14155 30927 30926 0 -1 0 116195 0 0 0 15705 295 0 0 25 0 1 0 423795433 449884160 98009 4294967295 134512640 134672761 3221224544 3221218368 134565478 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 109835 98009 603 41 0 109794 0
vsize: 439340
[startup+170.005 s]
Raw data (loadavg): 0.99 0.95 0.91 2/55 14156
Raw data (stat): 14156 (minisat+) R 14155 30927 30926 0 -1 0 163233 0 0 0 16596 405 0 0 25 0 1 0 423795433 682774528 145047 4294967295 134512640 134672761 3221224544 3221222968 134553579 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 166693 145047 603 41 0 166652 0
vsize: 666772
[startup+180.006 s]
Raw data (loadavg): 0.99 0.95 0.91 2/55 14156
Raw data (stat): 14156 (minisat+) R 14155 30927 30926 0 -1 0 209978 0 0 0 17478 522 0 0 25 0 1 0 423795433 865693696 191792 4294967295 134512640 134672761 3221224544 3221222200 134542305 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 211351 191792 603 41 0 211310 0
vsize: 845404
[startup+186.361 s]
Raw data (loadavg): 0.99 0.95 0.91 1/54 14156
Raw data (stat): 14156 (minisat+) R 14155 30927 30926 0 -1 0 209978 0 0 0 17478 522 0 0 25 0 1 0 423795433 865693696 191792 4294967295 134512640 134672761 3221224544 3221222200 134542305 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 211351 191792 603 41 0 211310 0
vsize: 0

Child ended because it received signal 11 (SIGSEGV)
Real time (s): 186.361
CPU time (s): 185.556
CPU user time (s): 179.264
CPU system time (s): 6.29204
CPU usage (%): 99.568
Max. virtual memory (Kb): 845404
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####