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/submitted/manquinho/ttp/normalized-data6_3.opb
MD5SUM	3ce91e964f348d481da3f7741c5768eb
Bench Category	optimization, small integers (OPTSMALLINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	25102
Optimality of the best value was proved	NO
Number of terms in the objective function	180
Biggest coefficient in the objective function	1380
Number of bits for the biggest coefficient in the objective function	11
Sum of the numbers in the objective function	116904
Number of bits of the sum of numbers in the objective function	17
Biggest number in a constraint	1380
Number of bits of the biggest number in a constraint	11
Biggest sum of numbers in a constraint	116904
Number of bits of the biggest sum of numbers	17
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	1.03084
Number of variables	540
Total number of constraints	4476
Number of constraints which are clauses	2532
Number of constraints which are cardinality constraints (but not clauses)	264
Number of constraints which are nor clauses,nor cardinality constraints	1680
Minimum length of a constraint	2
Maximum length of a constraint	20
Trace number 5216

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

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

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        738208 kB
Buffers:         37272 kB
Cached:         218612 kB
SwapCached:          0 kB
Active:          79480 kB
Inactive:       179256 kB
HighTotal:      131008 kB
HighFree:          252 kB
LowTotal:       903652 kB
LowFree:        737956 kB
SwapTotal:     2097892 kB
SwapFree:      2097892 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6928 kB
Slab:            32100 kB
Committed_AS:    63492 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-13 22:55:03 (client local time) WITH STATUS 10 IN 1200.19 SECONDS
stats: 3646 7 1200.19 10
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 4626 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: ######################################################################################################################################################
c   -- Clauses(.)/Splits(s): ....................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................
c ---[4624]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[4622]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[4620]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[4618]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[4616]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[4614]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[4612]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[4610]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[4608]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[4606]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[4604]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[4602]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[4600]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[4598]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[4596]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[4594]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[4592]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[4590]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[4588]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[4586]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[4584]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[4582]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[4580]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[4578]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[4576]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[4574]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[4572]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[4570]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[4568]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[4566]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[4265]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[4264]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[4263]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[4262]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[4261]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[4260]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[4259]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[4258]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[4257]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[4256]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[4255]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[4254]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[4253]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[4252]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[4251]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[4250]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[4249]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[4248]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[4247]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[4246]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[4245]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[4244]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[4243]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[4242]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[4241]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[4240]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[4239]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[4238]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[4237]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[4236]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[4235]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[4234]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[4233]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[4232]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[4231]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[4230]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[4229]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[4228]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[4227]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[4226]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[4225]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[4224]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[4223]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[4222]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[4221]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[4220]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[4219]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[4218]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[4217]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[4216]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[4215]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[4214]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[4213]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[4212]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[4211]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[4210]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[4209]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[4208]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[4207]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[4206]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[4204]---> Adder-cost: 8   maxlim: 5   bits: 3/3
c ---[4202]---> Adder-cost: 8   maxlim: 5   bits: 3/3
c ---[4200]---> Adder-cost: 8   maxlim: 5   bits: 3/3
c ---[4198]---> Adder-cost: 8   maxlim: 5   bits: 3/3
c ---[4196]---> Adder-cost: 8   maxlim: 5   bits: 3/3
c ---[4194]---> Adder-cost: 8   maxlim: 5   bits: 3/3
c ---[4192]---> Adder-cost: 8   maxlim: 5   bits: 3/3
c ---[4190]---> Adder-cost: 8   maxlim: 5   bits: 3/3
c ---[4188]---> Adder-cost: 8   maxlim: 5   bits: 3/3
c ---[4186]---> Adder-cost: 8   maxlim: 5   bits: 3/3
c ---[4184]---> Adder-cost: 8   maxlim: 5   bits: 3/3
c ---[4182]---> Adder-cost: 8   maxlim: 5   bits: 3/3
c ---[4180]---> Adder-cost: 8   maxlim: 5   bits: 3/3
c ---[4178]---> Adder-cost: 8   maxlim: 5   bits: 3/3
c ---[4176]---> Adder-cost: 8   maxlim: 5   bits: 3/3
c ---[4174]---> Adder-cost: 8   maxlim: 5   bits: 3/3
c ---[4172]---> Adder-cost: 8   maxlim: 5   bits: 3/3
c ---[4170]---> Adder-cost: 8   maxlim: 5   bits: 3/3
c ---[4168]---> Adder-cost: 8   maxlim: 5   bits: 3/3
c ---[4166]---> Adder-cost: 8   maxlim: 5   bits: 3/3
c ---[4164]---> Adder-cost: 8   maxlim: 5   bits: 3/3
c ---[4162]---> Adder-cost: 8   maxlim: 5   bits: 3/3
c ---[4160]---> Adder-cost: 8   maxlim: 5   bits: 3/3
c ---[4158]---> Adder-cost: 8   maxlim: 5   bits: 3/3
c ---[4156]---> Adder-cost: 8   maxlim: 5   bits: 3/3
c ---[4154]---> Adder-cost: 8   maxlim: 5   bits: 3/3
c ---[4152]---> Adder-cost: 8   maxlim: 5   bits: 3/3
c ---[4150]---> Adder-cost: 8   maxlim: 5   bits: 3/3
c ---[4148]---> Adder-cost: 8   maxlim: 5   bits: 3/3
c ---[4146]---> Adder-cost: 8   maxlim: 5   bits: 3/3
c ---[4144]---> Adder-cost: 8   maxlim: 5   bits: 3/3
c ---[4142]---> Adder-cost: 8   maxlim: 5   bits: 3/3
c ---[4140]---> Adder-cost: 8   maxlim: 5   bits: 3/3
c ---[4138]---> Adder-cost: 8   maxlim: 5   bits: 3/3
c ---[4136]---> Adder-cost: 8   maxlim: 5   bits: 3/3
c ---[4134]---> Adder-cost: 8   maxlim: 5   bits: 3/3
c ---[4132]---> Adder-cost: 8   maxlim: 5   bits: 3/3
c ---[4130]---> Adder-cost: 8   maxlim: 5   bits: 3/3
c ---[4128]---> Adder-cost: 8   maxlim: 5   bits: 3/3
c ---[4126]---> Adder-cost: 8   maxlim: 5   bits: 3/3
c ---[4124]---> Adder-cost: 8   maxlim: 5   bits: 3/3
c ---[4122]---> Adder-cost: 8   maxlim: 5   bits: 3/3
c ---[4120]---> Adder-cost: 8   maxlim: 5   bits: 3/3
c ---[4118]---> Adder-cost: 8   maxlim: 5   bits: 3/3
c ---[4116]---> Adder-cost: 8   maxlim: 5   bits: 3/3
c ---[4114]---> Adder-cost: 8   maxlim: 5   bits: 3/3
c ---[4112]---> Adder-cost: 8   maxlim: 5   bits: 3/3
c ---[4110]---> Adder-cost: 8   maxlim: 5   bits: 3/3
c ---[4108]---> Adder-cost: 8   maxlim: 5   bits: 3/3
c ---[4106]---> Adder-cost: 8   maxlim: 5   bits: 3/3
c ---[4104]---> Adder-cost: 8   maxlim: 5   bits: 3/3
c ---[4102]---> Adder-cost: 8   maxlim: 5   bits: 3/3
c ---[4100]---> Adder-cost: 8   maxlim: 5   bits: 3/3
c ---[4098]---> Adder-cost: 8   maxlim: 5   bits: 3/3
c ---[4096]---> Adder-cost: 8   maxlim: 5   bits: 3/3
c ---[4094]---> Adder-cost: 8   maxlim: 5   bits: 3/3
c ---[4092]---> Adder-cost: 8   maxlim: 5   bits: 3/3
c ---[4090]---> Adder-cost: 8   maxlim: 5   bits: 3/3
c ---[4088]---> Adder-cost: 8   maxlim: 5   bits: 3/3
c ---[4086]---> Adder-cost: 8   maxlim: 5   bits: 3/3
c ---[4079]---> Adder-cost: 32   maxlim: 16   bits: 5/5
c ---[4078]---> Adder-cost: 32   maxlim: 16   bits: 5/5
c ---[4077]---> Adder-cost: 32   maxlim: 16   bits: 5/5
c ---[4076]---> Adder-cost: 32   maxlim: 16   bits: 5/5
c ---[4075]---> Adder-cost: 32   maxlim: 16   bits: 5/5
c ---[4074]---> Adder-cost: 32   maxlim: 16   bits: 5/5
c ---[4067]---> Adder-cost: 36   maxlim: 16   bits: 5/5
c ---[4066]---> Adder-cost: 36   maxlim: 16   bits: 5/5
c ---[4065]---> Adder-cost: 36   maxlim: 16   bits: 5/5
c ---[4064]---> Adder-cost: 36   maxlim: 16   bits: 5/5
c ---[4063]---> Adder-cost: 36   maxlim: 16   bits: 5/5
c ---[4062]---> Adder-cost: 36   maxlim: 16   bits: 5/5
c ---[4055]---> Adder-cost: 34   maxlim: 16   bits: 5/5
c ---[4054]---> Adder-cost: 34   maxlim: 16   bits: 5/5
c ---[4053]---> Adder-cost: 34   maxlim: 16   bits: 5/5
c ---[4052]---> Adder-cost: 34   maxlim: 16   bits: 5/5
c ---[4051]---> Adder-cost: 34   maxlim: 16   bits: 5/5
c ---[4050]---> Adder-cost: 34   maxlim: 16   bits: 5/5
c ---[4043]---> Adder-cost: 32   maxlim: 16   bits: 5/5
c ---[4042]---> Adder-cost: 32   maxlim: 16   bits: 5/5
c ---[4041]---> Adder-cost: 32   maxlim: 16   bits: 5/5
c ---[4040]---> Adder-cost: 32   maxlim: 16   bits: 5/5
c ---[4039]---> Adder-cost: 32   maxlim: 16   bits: 5/5
c ---[4038]---> Adder-cost: 32   maxlim: 16   bits: 5/5
c ---[4031]---> Adder-cost: 36   maxlim: 16   bits: 5/5
c ---[4030]---> Adder-cost: 36   maxlim: 16   bits: 5/5
c ---[4029]---> Adder-cost: 36   maxlim: 16   bits: 5/5
c ---[4028]---> Adder-cost: 36   maxlim: 16   bits: 5/5
c ---[4027]---> Adder-cost: 36   maxlim: 16   bits: 5/5
c ---[4026]---> Adder-cost: 36   maxlim: 16   bits: 5/5
c ---[4019]---> Adder-cost: 34   maxlim: 16   bits: 5/5
c ---[4018]---> Adder-cost: 34   maxlim: 16   bits: 5/5
c ---[4017]---> Adder-cost: 34   maxlim: 16   bits: 5/5
c ---[4016]---> Adder-cost: 34   maxlim: 16   bits: 5/5
c ---[4015]---> Adder-cost: 34   maxlim: 16   bits: 5/5
c ---[4014]---> Adder-cost: 34   maxlim: 16   bits: 5/5
c ---[4007]---> Adder-cost: 32   maxlim: 16   bits: 5/5
c ---[4006]---> Adder-cost: 32   maxlim: 16   bits: 5/5
c ---[4005]---> Adder-cost: 32   maxlim: 16   bits: 5/5
c ---[4004]---> Adder-cost: 32   maxlim: 16   bits: 5/5
c ---[4003]---> Adder-cost: 32   maxlim: 16   bits: 5/5
c ---[4002]---> Adder-cost: 32   maxlim: 16   bits: 5/5
c ---[2050]---> Adder-cost: 6   maxlim: 4   bits: 3/3
c ---[2048]---> Adder-cost: 6   maxlim: 4   bits: 3/3
c ---[2046]---> Adder-cost: 6   maxlim: 4   bits: 3/3
c ---[2044]---> Adder-cost: 6   maxlim: 4   bits: 3/3
c ---[2042]---> Adder-cost: 6   maxlim: 4   bits: 3/3
c ---[2040]---> Adder-cost: 6   maxlim: 4   bits: 3/3
c ---[2038]---> Adder-cost: 6   maxlim: 4   bits: 3/3
c ---[2036]---> Adder-cost: 6   maxlim: 4   bits: 3/3
c ---[2034]---> Adder-cost: 6   maxlim: 4   bits: 3/3
c ---[2032]---> Adder-cost: 6   maxlim: 4   bits: 3/3
c ---[2030]---> Adder-cost: 6   maxlim: 4   bits: 3/3
c ---[2028]---> Adder-cost: 6   maxlim: 4   bits: 3/3
c ---[2026]---> Adder-cost: 6   maxlim: 4   bits: 3/3
c ---[2024]---> Adder-cost: 6   maxlim: 4   bits: 3/3
c ---[2022]---> Adder-cost: 6   maxlim: 4   bits: 3/3
c ---[2020]---> Adder-cost: 6   maxlim: 4   bits: 3/3
c ---[2018]---> Adder-cost: 6   maxlim: 4   bits: 3/3
c ---[2016]---> Adder-cost: 6   maxlim: 4   bits: 3/3
c ---[2014]---> Adder-cost: 6   maxlim: 4   bits: 3/3
c ---[2012]---> Adder-cost: 6   maxlim: 4   bits: 3/3
c ---[2010]---> Adder-cost: 6   maxlim: 4   bits: 3/3
c ---[2008]---> Adder-cost: 6   maxlim: 4   bits: 3/3
c ---[2006]---> Adder-cost: 6   maxlim: 4   bits: 3/3
c ---[2004]---> Adder-cost: 6   maxlim: 4   bits: 3/3
c ---[2002]---> Adder-cost: 6   maxlim: 4   bits: 3/3
c ---[2000]---> Adder-cost: 6   maxlim: 4   bits: 3/3
c ---[1998]---> Adder-cost: 6   maxlim: 4   bits: 3/3
c ---[1996]---> Adder-cost: 6   maxlim: 4   bits: 3/3
c ---[1994]---> Adder-cost: 6   maxlim: 4   bits: 3/3
c ---[1992]---> Adder-cost: 6   maxlim: 4   bits: 3/3
c ---[1990]---> Adder-cost: 6   maxlim: 4   bits: 3/3
c ---[1988]---> Adder-cost: 6   maxlim: 4   bits: 3/3
c ---[1986]---> Adder-cost: 6   maxlim: 4   bits: 3/3
c ---[1984]---> Adder-cost: 6   maxlim: 4   bits: 3/3
c ---[1982]---> Adder-cost: 6   maxlim: 4   bits: 3/3
c ---[1980]---> Adder-cost: 6   maxlim: 4   bits: 3/3
c ---[1978]---> Adder-cost: 6   maxlim: 4   bits: 3/3
c ---[1976]---> Adder-cost: 6   maxlim: 4   bits: 3/3
c ---[1974]---> Adder-cost: 6   maxlim: 4   bits: 3/3
c ---[1972]---> Adder-cost: 6   maxlim: 4   bits: 3/3
c ---[1970]---> Adder-cost: 6   maxlim: 4   bits: 3/3
c ---[1968]---> Adder-cost: 6   maxlim: 4   bits: 3/3
c ---[1966]---> Adder-cost: 6   maxlim: 4   bits: 3/3
c ---[1964]---> Adder-cost: 6   maxlim: 4   bits: 3/3
c ---[1962]---> Adder-cost: 6   maxlim: 4   bits: 3/3
c ---[1960]---> Adder-cost: 6   maxlim: 4   bits: 3/3
c ---[1958]---> Adder-cost: 6   maxlim: 4   bits: 3/3
c ---[1956]---> Adder-cost: 6   maxlim: 4   bits: 3/3
c ---[1954]---> Adder-cost: 6   maxlim: 4   bits: 3/3
c ---[1952]---> Adder-cost: 6   maxlim: 4   bits: 3/3
c ---[1950]---> Adder-cost: 6   maxlim: 4   bits: 3/3
c ---[1948]---> Adder-cost: 6   maxlim: 4   bits: 3/3
c ---[1946]---> Adder-cost: 6   maxlim: 4   bits: 3/3
c ---[1944]---> Adder-cost: 6   maxlim: 4   bits: 3/3
c ---[1942]---> Adder-cost: 6   maxlim: 4   bits: 3/3
c ---[1940]---> Adder-cost: 6   maxlim: 4   bits: 3/3
c ---[1938]---> Adder-cost: 6   maxlim: 4   bits: 3/3
c ---[1936]---> Adder-cost: 6   maxlim: 4   bits: 3/3
c ---[1934]---> Adder-cost: 6   maxlim: 4   bits: 3/3
c ---[1932]---> Adder-cost: 6   maxlim: 4   bits: 3/3
c ---[1931]---> Adder-cost: 5   maxlim: 1   bits: 2/1
c ---[1930]---> Adder-cost: 5   maxlim: 1   bits: 2/1
c ---[1929]---> Adder-cost: 5   maxlim: 1   bits: 2/1
c ---[1928]---> Adder-cost: 5   maxlim: 1   bits: 2/1
c ---[1927]---> Adder-cost: 5   maxlim: 1   bits: 2/1
c ---[1926]---> Adder-cost: 5   maxlim: 1   bits: 2/1
c ---[1925]---> Adder-cost: 5   maxlim: 1   bits: 2/1
c ---[1924]---> Adder-cost: 5   maxlim: 1   bits: 2/1
c ---[1923]---> Adder-cost: 5   maxlim: 1   bits: 2/1
c ---[1922]---> Adder-cost: 5   maxlim: 1   bits: 2/1
c ---[1921]---> Adder-cost: 5   maxlim: 1   bits: 2/1
c ---[1920]---> Adder-cost: 5   maxlim: 1   bits: 2/1
c ---[1919]---> Adder-cost: 16   maxlim: 7   bits: 4/3
c ---[1918]---> Adder-cost: 2   maxlim: 7   bits: 4/3
c ---[1917]---> Adder-cost: 12   maxlim: 7   bits: 4/3
c ---[1916]---> Adder-cost: 2   maxlim: 7   bits: 4/3
c ---[1915]---> Adder-cost: 12   maxlim: 7   bits: 4/3
c ---[1914]---> Adder-cost: 2   maxlim: 7   bits: 4/3
c ---[1913]---> Adder-cost: 16   maxlim: 7   bits: 4/3
c ---[1912]---> Adder-cost: 2   maxlim: 7   bits: 4/3
c ---[1911]---> Adder-cost: 15   maxlim: 6   bits: 4/3
c ---[1910]---> Adder-cost: 15   maxlim: 6   bits: 4/3
c ---[1909]---> Adder-cost: 15   maxlim: 6   bits: 4/3
c ---[1908]---> Adder-cost: 15   maxlim: 6   bits: 4/3
c ---[1907]---> Adder-cost: 15   maxlim: 6   bits: 4/3
c ---[1906]---> Adder-cost: 15   maxlim: 6   bits: 4/3
c ---[1905]---> Adder-cost: 15   maxlim: 6   bits: 4/3
c ---[1904]---> Adder-cost: 15   maxlim: 6   bits: 4/3
c ---[1903]---> Adder-cost: 15   maxlim: 5   bits: 4/3
c ---[1902]---> Adder-cost: 9   maxlim: 5   bits: 4/3
c ---[1901]---> Adder-cost: 11   maxlim: 5   bits: 4/3
c ---[1900]---> Adder-cost: 9   maxlim: 5   bits: 4/3
c ---[1899]---> Adder-cost: 13   maxlim: 5   bits: 4/3
c ---[1898]---> Adder-cost: 9   maxlim: 5   bits: 4/3
c ---[1897]---> Adder-cost: 15   maxlim: 5   bits: 4/3
c ---[1896]---> Adder-cost: 9   maxlim: 5   bits: 4/3
c ---[1895]---> Adder-cost: 8   maxlim: 4   bits: 4/3
c ---[1894]---> Adder-cost: 8   maxlim: 4   bits: 4/3
c ---[1893]---> Adder-cost: 8   maxlim: 4   bits: 4/3
c ---[1892]---> Adder-cost: 8   maxlim: 4   bits: 4/3
c ---[1891]---> Adder-cost: 8   maxlim: 4   bits: 4/3
c ---[1890]---> Adder-cost: 8   maxlim: 4   bits: 4/3
c ---[1889]---> Adder-cost: 8   maxlim: 4   bits: 4/3
c ---[1888]---> Adder-cost: 8   maxlim: 4   bits: 4/3
c ---[1887]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[1886]---> Adder-cost: 2   maxlim: 3   bits: 3/2
c ---[1885]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[1884]---> Adder-cost: 2   maxlim: 3   bits: 3/2
c ---[1883]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[1882]---> Adder-cost: 2   maxlim: 3   bits: 3/2
c ---[1881]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[1880]---> Adder-cost: 2   maxlim: 3   bits: 3/2
c ---[1879]---> Adder-cost: 7   maxlim: 2   bits: 3/2
c ---[1878]---> Adder-cost: 7   maxlim: 2   bits: 3/2
c ---[1877]---> Adder-cost: 7   maxlim: 2   bits: 3/2
c ---[1876]---> Adder-cost: 7   maxlim: 2   bits: 3/2
c ---[1875]---> Adder-cost: 7   maxlim: 2   bits: 3/2
c ---[1874]---> Adder-cost: 7   maxlim: 2   bits: 3/2
c ---[1873]---> Adder-cost: 7   maxlim: 2   bits: 3/2
c ---[1872]---> Adder-cost: 7   maxlim: 2   bits: 3/2
c ---[1871]---> Adder-cost: 4   maxlim: 1   bits: 2/1
c ---[1870]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1869]---> Adder-cost: 4   maxlim: 1   bits: 2/1
c ---[1868]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1867]---> Adder-cost: 4   maxlim: 1   bits: 2/1
c ---[1866]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1865]---> Adder-cost: 4   maxlim: 1   bits: 2/1
c ---[1864]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1855]---> Adder-cost: 12   maxlim: 7   bits: 4/3
c ---[1854]---> Adder-cost: 2   maxlim: 7   bits: 4/3
c ---[1853]---> Adder-cost: 2   maxlim: 7   bits: 4/3
c ---[1852]---> Adder-cost: 2   maxlim: 7   bits: 4/3
c ---[1851]---> Adder-cost: 2   maxlim: 7   bits: 4/3
c ---[1850]---> Adder-cost: 2   maxlim: 7   bits: 4/3
c ---[1849]---> Adder-cost: 2   maxlim: 7   bits: 4/3
c ---[1848]---> Adder-cost: 2   maxlim: 7   bits: 4/3
c ---[1847]---> Adder-cost: 15   maxlim: 6   bits: 4/3
c ---[1846]---> Adder-cost: 15   maxlim: 6   bits: 4/3
c ---[1845]---> Adder-cost: 15   maxlim: 6   bits: 4/3
c ---[1844]---> Adder-cost: 15   maxlim: 6   bits: 4/3
c ---[1843]---> Adder-cost: 15   maxlim: 6   bits: 4/3
c ---[1842]---> Adder-cost: 15   maxlim: 6   bits: 4/3
c ---[1841]---> Adder-cost: 15   maxlim: 6   bits: 4/3
c ---[1840]---> Adder-cost: 15   maxlim: 6   bits: 4/3
c ---[1839]---> Adder-cost: 13   maxlim: 5   bits: 4/3
c ---[1838]---> Adder-cost: 9   maxlim: 5   bits: 4/3
c ---[1837]---> Adder-cost: 9   maxlim: 5   bits: 4/3
c ---[1836]---> Adder-cost: 9   maxlim: 5   bits: 4/3
c ---[1835]---> Adder-cost: 9   maxlim: 5   bits: 4/3
c ---[1834]---> Adder-cost: 9   maxlim: 5   bits: 4/3
c ---[1833]---> Adder-cost: 9   maxlim: 5   bits: 4/3
c ---[1832]---> Adder-cost: 9   maxlim: 5   bits: 4/3
c ---[1831]---> Adder-cost: 8   maxlim: 4   bits: 4/3
c ---[1830]---> Adder-cost: 8   maxlim: 4   bits: 4/3
c ---[1829]---> Adder-cost: 8   maxlim: 4   bits: 4/3
c ---[1828]---> Adder-cost: 8   maxlim: 4   bits: 4/3
c ---[1827]---> Adder-cost: 8   maxlim: 4   bits: 4/3
c ---[1826]---> Adder-cost: 8   maxlim: 4   bits: 4/3
c ---[1825]---> Adder-cost: 8   maxlim: 4   bits: 4/3
c ---[1824]---> Adder-cost: 8   maxlim: 4   bits: 4/3
c ---[1823]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[1822]---> Adder-cost: 2   maxlim: 3   bits: 3/2
c ---[1821]---> Adder-cost: 2   maxlim: 3   bits: 3/2
c ---[1820]---> Adder-cost: 2   maxlim: 3   bits: 3/2
c ---[1819]---> Adder-cost: 2   maxlim: 3   bits: 3/2
c ---[1818]---> Adder-cost: 2   maxlim: 3   bits: 3/2
c ---[1817]---> Adder-cost: 2   maxlim: 3   bits: 3/2
c ---[1816]---> Adder-cost: 2   maxlim: 3   bits: 3/2
c ---[1815]---> Adder-cost: 7   maxlim: 2   bits: 3/2
c ---[1814]---> Adder-cost: 7   maxlim: 2   bits: 3/2
c ---[1813]---> Adder-cost: 7   maxlim: 2   bits: 3/2
c ---[1812]---> Adder-cost: 7   maxlim: 2   bits: 3/2
c ---[1811]---> Adder-cost: 7   maxlim: 2   bits: 3/2
c ---[1810]---> Adder-cost: 7   maxlim: 2   bits: 3/2
c ---[1809]---> Adder-cost: 7   maxlim: 2   bits: 3/2
c ---[1808]---> Adder-cost: 7   maxlim: 2   bits: 3/2
c ---[1807]---> Adder-cost: 4   maxlim: 1   bits: 2/1
c ---[1806]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1805]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1804]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1803]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1802]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1801]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1800]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1791]---> Adder-cost: 2   maxlim: 7   bits: 4/3
c ---[1790]---> Adder-cost: 2   maxlim: 7   bits: 4/3
c ---[1789]---> Adder-cost: 2   maxlim: 7   bits: 4/3
c ---[1788]---> Adder-cost: 2   maxlim: 7   bits: 4/3
c ---[1787]---> Adder-cost: 2   maxlim: 7   bits: 4/3
c ---[1786]---> Adder-cost: 2   maxlim: 7   bits: 4/3
c ---[1785]---> Adder-cost: 2   maxlim: 7   bits: 4/3
c ---[1784]---> Adder-cost: 2   maxlim: 7   bits: 4/3
c ---[1783]---> Adder-cost: 15   maxlim: 6   bits: 4/3
c ---[1782]---> Adder-cost: 15   maxlim: 6   bits: 4/3
c ---[1781]---> Adder-cost: 15   maxlim: 6   bits: 4/3
c ---[1780]---> Adder-cost: 15   maxlim: 6   bits: 4/3
c ---[1779]---> Adder-cost: 15   maxlim: 6   bits: 4/3
c ---[1778]---> Adder-cost: 15   maxlim: 6   bits: 4/3
c ---[1777]---> Adder-cost: 15   maxlim: 6   bits: 4/3
c ---[1776]---> Adder-cost: 15   maxlim: 6   bits: 4/3
c ---[1775]---> Adder-cost: 9   maxlim: 5   bits: 4/3
c ---[1774]---> Adder-cost: 9   maxlim: 5   bits: 4/3
c ---[1773]---> Adder-cost: 9   maxlim: 5   bits: 4/3
c ---[1772]---> Adder-cost: 9   maxlim: 5   bits: 4/3
c ---[1771]---> Adder-cost: 9   maxlim: 5   bits: 4/3
c ---[1770]---> Adder-cost: 9   maxlim: 5   bits: 4/3
c ---[1769]---> Adder-cost: 9   maxlim: 5   bits: 4/3
c ---[1768]---> Adder-cost: 9   maxlim: 5   bits: 4/3
c ---[1767]---> Adder-cost: 8   maxlim: 4   bits: 4/3
c ---[1766]---> Adder-cost: 8   maxlim: 4   bits: 4/3
c ---[1765]---> Adder-cost: 8   maxlim: 4   bits: 4/3
c ---[1764]---> Adder-cost: 8   maxlim: 4   bits: 4/3
c ---[1763]---> Adder-cost: 8   maxlim: 4   bits: 4/3
c ---[1762]---> Adder-cost: 8   maxlim: 4   bits: 4/3
c ---[1761]---> Adder-cost: 8   maxlim: 4   bits: 4/3
c ---[1760]---> Adder-cost: 8   maxlim: 4   bits: 4/3
c ---[1759]---> Adder-cost: 2   maxlim: 3   bits: 3/2
c ---[1758]---> Adder-cost: 2   maxlim: 3   bits: 3/2
c ---[1757]---> Adder-cost: 2   maxlim: 3   bits: 3/2
c ---[1756]---> Adder-cost: 2   maxlim: 3   bits: 3/2
c ---[1755]---> Adder-cost: 2   maxlim: 3   bits: 3/2
c ---[1754]---> Adder-cost: 2   maxlim: 3   bits: 3/2
c ---[1753]---> Adder-cost: 2   maxlim: 3   bits: 3/2
c ---[1752]---> Adder-cost: 2   maxlim: 3   bits: 3/2
c ---[1751]---> Adder-cost: 7   maxlim: 2   bits: 3/2
c ---[1750]---> Adder-cost: 7   maxlim: 2   bits: 3/2
c ---[1749]---> Adder-cost: 7   maxlim: 2   bits: 3/2
c ---[1748]---> Adder-cost: 7   maxlim: 2   bits: 3/2
c ---[1747]---> Adder-cost: 7   maxlim: 2   bits: 3/2
c ---[1746]---> Adder-cost: 7   maxlim: 2   bits: 3/2
c ---[1745]---> Adder-cost: 7   maxlim: 2   bits: 3/2
c ---[1744]---> Adder-cost: 7   maxlim: 2   bits: 3/2
c ---[1743]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1742]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1741]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1740]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1739]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1738]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1737]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1736]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1727]---> Adder-cost: 2   maxlim: 7   bits: 4/3
c ---[1726]---> Adder-cost: 2   maxlim: 7   bits: 4/3
c ---[1725]---> Adder-cost: 2   maxlim: 7   bits: 4/3
c ---[1724]---> Adder-cost: 2   maxlim: 7   bits: 4/3
c ---[1723]---> Adder-cost: 2   maxlim: 7   bits: 4/3
c ---[1722]---> Adder-cost: 2   maxlim: 7   bits: 4/3
c ---[1721]---> Adder-cost: 2   maxlim: 7   bits: 4/3
c ---[1720]---> Adder-cost: 2   maxlim: 7   bits: 4/3
c ---[1719]---> Adder-cost: 15   maxlim: 6   bits: 4/3
c ---[1718]---> Adder-cost: 15   maxlim: 6   bits: 4/3
c ---[1717]---> Adder-cost: 15   maxlim: 6   bits: 4/3
c ---[1716]---> Adder-cost: 15   maxlim: 6   bits: 4/3
c ---[1715]---> Adder-cost: 15   maxlim: 6   bits: 4/3
c ---[1714]---> Adder-cost: 15   maxlim: 6   bits: 4/3
c ---[1713]---> Adder-cost: 15   maxlim: 6   bits: 4/3
c ---[1712]---> Adder-cost: 15   maxlim: 6   bits: 4/3
c ---[1711]---> Adder-cost: 9   maxlim: 5   bits: 4/3
c ---[1710]---> Adder-cost: 9   maxlim: 5   bits: 4/3
c ---[1709]---> Adder-cost: 9   maxlim: 5   bits: 4/3
c ---[1708]---> Adder-cost: 9   maxlim: 5   bits: 4/3
c ---[1707]---> Adder-cost: 9   maxlim: 5   bits: 4/3
c ---[1706]---> Adder-cost: 9   maxlim: 5   bits: 4/3
c ---[1705]---> Adder-cost: 9   maxlim: 5   bits: 4/3
c ---[1704]---> Adder-cost: 9   maxlim: 5   bits: 4/3
c ---[1703]---> Adder-cost: 8   maxlim: 4   bits: 4/3
c ---[1702]---> Adder-cost: 8   maxlim: 4   bits: 4/3
c ---[1701]---> Adder-cost: 8   maxlim: 4   bits: 4/3
c ---[1700]---> Adder-cost: 8   maxlim: 4   bits: 4/3
c ---[1699]---> Adder-cost: 8   maxlim: 4   bits: 4/3
c ---[1698]---> Adder-cost: 8   maxlim: 4   bits: 4/3
c ---[1697]---> Adder-cost: 8   maxlim: 4   bits: 4/3
c ---[1696]---> Adder-cost: 8   maxlim: 4   bits: 4/3
c ---[1695]---> Adder-cost: 2   maxlim: 3   bits: 3/2
c ---[1694]---> Adder-cost: 2   maxlim: 3   bits: 3/2
c ---[1693]---> Adder-cost: 2   maxlim: 3   bits: 3/2
c ---[1692]---> Adder-cost: 2   maxlim: 3   bits: 3/2
c ---[1691]---> Adder-cost: 2   maxlim: 3   bits: 3/2
c ---[1690]---> Adder-cost: 2   maxlim: 3   bits: 3/2
c ---[1689]---> Adder-cost: 2   maxlim: 3   bits: 3/2
c ---[1688]---> Adder-cost: 2   maxlim: 3   bits: 3/2
c ---[1687]---> Adder-cost: 7   maxlim: 2   bits: 3/2
c ---[1686]---> Adder-cost: 7   maxlim: 2   bits: 3/2
c ---[1685]---> Adder-cost: 7   maxlim: 2   bits: 3/2
c ---[1684]---> Adder-cost: 7   maxlim: 2   bits: 3/2
c ---[1683]---> Adder-cost: 7   maxlim: 2   bits: 3/2
c ---[1682]---> Adder-cost: 7   maxlim: 2   bits: 3/2
c ---[1681]---> Adder-cost: 7   maxlim: 2   bits: 3/2
c ---[1680]---> Adder-cost: 7   maxlim: 2   bits: 3/2
c ---[1679]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1678]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1677]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1676]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1675]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1674]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1673]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1672]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1663]---> Adder-cost: 2   maxlim: 7   bits: 4/3
c ---[1662]---> Adder-cost: 2   maxlim: 7   bits: 4/3
c ---[1661]---> Adder-cost: 2   maxlim: 7   bits: 4/3
c ---[1660]---> Adder-cost: 2   maxlim: 7   bits: 4/3
c ---[1659]---> Adder-cost: 2   maxlim: 7   bits: 4/3
c ---[1658]---> Adder-cost: 2   maxlim: 7   bits: 4/3
c ---[1657]---> Adder-cost: 2   maxlim: 7   bits: 4/3
c ---[1656]---> Adder-cost: 2   maxlim: 7   bits: 4/3
c ---[1655]---> Adder-cost: 15   maxlim: 6   bits: 4/3
c ---[1654]---> Adder-cost: 15   maxlim: 6   bits: 4/3
c ---[1653]---> Adder-cost: 15   maxlim: 6   bits: 4/3
c ---[1652]---> Adder-cost: 15   maxlim: 6   bits: 4/3
c ---[1651]---> Adder-cost: 15   maxlim: 6   bits: 4/3
c ---[1650]---> Adder-cost: 15   maxlim: 6   bits: 4/3
c ---[1649]---> Adder-cost: 15   maxlim: 6   bits: 4/3
c ---[1648]---> Adder-cost: 15   maxlim: 6   bits: 4/3
c ---[1647]---> Adder-cost: 9   maxlim: 5   bits: 4/3
c ---[1646]---> Adder-cost: 9   maxlim: 5   bits: 4/3
c ---[1645]---> Adder-cost: 9   maxlim: 5   bits: 4/3
c ---[1644]---> Adder-cost: 9   maxlim: 5   bits: 4/3
c ---[1643]---> Adder-cost: 9   maxlim: 5   bits: 4/3
c ---[1642]---> Adder-cost: 9   maxlim: 5   bits: 4/3
c ---[1641]---> Adder-cost: 9   maxlim: 5   bits: 4/3
c ---[1640]---> Adder-cost: 9   maxlim: 5   bits: 4/3
c ---[1639]---> Adder-cost: 8   maxlim: 4   bits: 4/3
c ---[1638]---> Adder-cost: 8   maxlim: 4   bits: 4/3
c ---[1637]---> Adder-cost: 8   maxlim: 4   bits: 4/3
c ---[1636]---> Adder-cost: 8   maxlim: 4   bits: 4/3
c ---[1635]---> Adder-cost: 8   maxlim: 4   bits: 4/3
c ---[1634]---> Adder-cost: 8   maxlim: 4   bits: 4/3
c ---[1633]---> Adder-cost: 8   maxlim: 4   bits: 4/3
c ---[1632]---> Adder-cost: 8   maxlim: 4   bits: 4/3
c ---[1631]---> Adder-cost: 2   maxlim: 3   bits: 3/2
c ---[1630]---> Adder-cost: 2   maxlim: 3   bits: 3/2
c ---[1629]---> Adder-cost: 2   maxlim: 3   bits: 3/2
c ---[1628]---> Adder-cost: 2   maxlim: 3   bits: 3/2
c ---[1627]---> Adder-cost: 2   maxlim: 3   bits: 3/2
c ---[1626]---> Adder-cost: 2   maxlim: 3   bits: 3/2
c ---[1625]---> Adder-cost: 2   maxlim: 3   bits: 3/2
c ---[1624]---> Adder-cost: 2   maxlim: 3   bits: 3/2
c ---[1623]---> Adder-cost: 7   maxlim: 2   bits: 3/2
c ---[1622]---> Adder-cost: 7   maxlim: 2   bits: 3/2
c ---[1621]---> Adder-cost: 7   maxlim: 2   bits: 3/2
c ---[1620]---> Adder-cost: 7   maxlim: 2   bits: 3/2
c ---[1619]---> Adder-cost: 7   maxlim: 2   bits: 3/2
c ---[1618]---> Adder-cost: 7   maxlim: 2   bits: 3/2
c ---[1617]---> Adder-cost: 7   maxlim: 2   bits: 3/2
c ---[1616]---> Adder-cost: 7   maxlim: 2   bits: 3/2
c ---[1615]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1614]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1613]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1612]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1611]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1610]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1609]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1608]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1599]---> Adder-cost: 16   maxlim: 7   bits: 4/3
c ---[1598]---> Adder-cost: 2   maxlim: 7   bits: 4/3
c ---[1597]---> Adder-cost: 12   maxlim: 7   bits: 4/3
c ---[1596]---> Adder-cost: 2   maxlim: 7   bits: 4/3
c ---[1595]---> Adder-cost: 12   maxlim: 7   bits: 4/3
c ---[1594]---> Adder-cost: 2   maxlim: 7   bits: 4/3
c ---[1593]---> Adder-cost: 16   maxlim: 7   bits: 4/3
c ---[1592]---> Adder-cost: 2   maxlim: 7   bits: 4/3
c ---[1591]---> Adder-cost: 15   maxlim: 6   bits: 4/3
c ---[1590]---> Adder-cost: 15   maxlim: 6   bits: 4/3
c ---[1589]---> Adder-cost: 15   maxlim: 6   bits: 4/3
c ---[1588]---> Adder-cost: 15   maxlim: 6   bits: 4/3
c ---[1587]---> Adder-cost: 15   maxlim: 6   bits: 4/3
c ---[1586]---> Adder-cost: 15   maxlim: 6   bits: 4/3
c ---[1585]---> Adder-cost: 15   maxlim: 6   bits: 4/3
c ---[1584]---> Adder-cost: 15   maxlim: 6   bits: 4/3
c ---[1583]---> Adder-cost: 15   maxlim: 5   bits: 4/3
c ---[1582]---> Adder-cost: 9   maxlim: 5   bits: 4/3
c ---[1581]---> Adder-cost: 11   maxlim: 5   bits: 4/3
c ---[1580]---> Adder-cost: 9   maxlim: 5   bits: 4/3
c ---[1579]---> Adder-cost: 13   maxlim: 5   bits: 4/3
c ---[1578]---> Adder-cost: 9   maxlim: 5   bits: 4/3
c ---[1577]---> Adder-cost: 15   maxlim: 5   bits: 4/3
c ---[1576]---> Adder-cost: 9   maxlim: 5   bits: 4/3
c ---[1575]---> Adder-cost: 8   maxlim: 4   bits: 4/3
c ---[1574]---> Adder-cost: 8   maxlim: 4   bits: 4/3
c ---[1573]---> Adder-cost: 8   maxlim: 4   bits: 4/3
c ---[1572]---> Adder-cost: 8   maxlim: 4   bits: 4/3
c ---[1571]---> Adder-cost: 8   maxlim: 4   bits: 4/3
c ---[1570]---> Adder-cost: 8   maxlim: 4   bits: 4/3
c ---[1569]---> Adder-cost: 8   maxlim: 4   bits: 4/3
c ---[1568]---> Adder-cost: 8   maxlim: 4   bits: 4/3
c ---[1567]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[1566]---> Adder-cost: 2   maxlim: 3   bits: 3/2
c ---[1565]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[1564]---> Adder-cost: 2   maxlim: 3   bits: 3/2
c ---[1563]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[1562]---> Adder-cost: 2   maxlim: 3   bits: 3/2
c ---[1561]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[1560]---> Adder-cost: 2   maxlim: 3   bits: 3/2
c ---[1559]---> Adder-cost: 7   maxlim: 2   bits: 3/2
c ---[1558]---> Adder-cost: 7   maxlim: 2   bits: 3/2
c ---[1557]---> Adder-cost: 7   maxlim: 2   bits: 3/2
c ---[1556]---> Adder-cost: 7   maxlim: 2   bits: 3/2
c ---[1555]---> Adder-cost: 7   maxlim: 2   bits: 3/2
c ---[1554]---> Adder-cost: 7   maxlim: 2   bits: 3/2
c ---[1553]---> Adder-cost: 7   maxlim: 2   bits: 3/2
c ---[1552]---> Adder-cost: 7   maxlim: 2   bits: 3/2
c ---[1551]---> Adder-cost: 4   maxlim: 1   bits: 2/1
c ---[1550]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1549]---> Adder-cost: 4   maxlim: 1   bits: 2/1
c ---[1548]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1547]---> Adder-cost: 4   maxlim: 1   bits: 2/1
c ---[1546]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1545]---> Adder-cost: 4   maxlim: 1   bits: 2/1
c ---[1544]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1535]---> Adder-cost: 12   maxlim: 7   bits: 4/3
c ---[1534]---> Adder-cost: 2   maxlim: 7   bits: 4/3
c ---[1533]---> Adder-cost: 2   maxlim: 7   bits: 4/3
c ---[1532]---> Adder-cost: 2   maxlim: 7   bits: 4/3
c ---[1531]---> Adder-cost: 2   maxlim: 7   bits: 4/3
c ---[1530]---> Adder-cost: 2   maxlim: 7   bits: 4/3
c ---[1529]---> Adder-cost: 2   maxlim: 7   bits: 4/3
c ---[1528]---> Adder-cost: 2   maxlim: 7   bits: 4/3
c ---[1527]---> Adder-cost: 15   maxlim: 6   bits: 4/3
c ---[1526]---> Adder-cost: 15   maxlim: 6   bits: 4/3
c ---[1525]---> Adder-cost: 15   maxlim: 6   bits: 4/3
c ---[1524]---> Adder-cost: 15   maxlim: 6   bits: 4/3
c ---[1523]---> Adder-cost: 15   maxlim: 6   bits: 4/3
c ---[1522]---> Adder-cost: 15   maxlim: 6   bits: 4/3
c ---[1521]---> Adder-cost: 15   maxlim: 6   bits: 4/3
c ---[1520]---> Adder-cost: 15   maxlim: 6   bits: 4/3
c ---[1519]---> Adder-cost: 13   maxlim: 5   bits: 4/3
c ---[1518]---> Adder-cost: 9   maxlim: 5   bits: 4/3
c ---[1517]---> Adder-cost: 9   maxlim: 5   bits: 4/3
c ---[1516]---> Adder-cost: 9   maxlim: 5   bits: 4/3
c ---[1515]---> Adder-cost: 9   maxlim: 5   bits: 4/3
c ---[1514]---> Adder-cost: 9   maxlim: 5   bits: 4/3
c ---[1513]---> Adder-cost: 9   maxlim: 5   bits: 4/3
c ---[1512]---> Adder-cost: 9   maxlim: 5   bits: 4/3
c ---[1511]---> Adder-cost: 8   maxlim: 4   bits: 4/3
c ---[1510]---> Adder-cost: 8   maxlim: 4   bits: 4/3
c ---[1509]---> Adder-cost: 8   maxlim: 4   bits: 4/3
c ---[1508]---> Adder-cost: 8   maxlim: 4   bits: 4/3
c ---[1507]---> Adder-cost: 8   maxlim: 4   bits: 4/3
c ---[1506]---> Adder-cost: 8   maxlim: 4   bits: 4/3
c ---[1505]---> Adder-cost: 8   maxlim: 4   bits: 4/3
c ---[1504]---> Adder-cost: 8   maxlim: 4   bits: 4/3
c ---[1503]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[1502]---> Adder-cost: 2   maxlim: 3   bits: 3/2
c ---[1501]---> Adder-cost: 2   maxlim: 3   bits: 3/2
c ---[1500]---> Adder-cost: 2   maxlim: 3   bits: 3/2
c ---[1499]---> Adder-cost: 2   maxlim: 3   bits: 3/2
c ---[1498]---> Adder-cost: 2   maxlim: 3   bits: 3/2
c ---[1497]---> Adder-cost: 2   maxlim: 3   bits: 3/2
c ---[1496]---> Adder-cost: 2   maxlim: 3   bits: 3/2
c ---[1495]---> Adder-cost: 7   maxlim: 2   bits: 3/2
c ---[1494]---> Adder-cost: 7   maxlim: 2   bits: 3/2
c ---[1493]---> Adder-cost: 7   maxlim: 2   bits: 3/2
c ---[1492]---> Adder-cost: 7   maxlim: 2   bits: 3/2
c ---[1491]---> Adder-cost: 7   maxlim: 2   bits: 3/2
c ---[1490]---> Adder-cost: 7   maxlim: 2   bits: 3/2
c ---[1489]---> Adder-cost: 7   maxlim: 2   bits: 3/2
c ---[1488]---> Adder-cost: 7   maxlim: 2   bits: 3/2
c ---[1487]---> Adder-cost: 4   maxlim: 1   bits: 2/1
c ---[1486]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1485]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1484]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1483]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1482]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1481]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1480]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1471]---> Adder-cost: 2   maxlim: 7   bits: 4/3
c ---[1470]---> Adder-cost: 2   maxlim: 7   bits: 4/3
c ---[1469]---> Adder-cost: 2   maxlim: 7   bits: 4/3
c ---[1468]---> Adder-cost: 2   maxlim: 7   bits: 4/3
c ---[1467]---> Adder-cost: 2   maxlim: 7   bits: 4/3
c ---[1466]---> Adder-cost: 2   maxlim: 7   bits: 4/3
c ---[1465]---> Adder-cost: 2   maxlim: 7   bits: 4/3
c ---[1464]---> Adder-cost: 2   maxlim: 7   bits: 4/3
c ---[1463]---> Adder-cost: 15   maxlim: 6   bits: 4/3
c ---[1462]---> Adder-cost: 15   maxlim: 6   bits: 4/3
c ---[1461]---> Adder-cost: 15   maxlim: 6   bits: 4/3
c ---[1460]---> Adder-cost: 15   maxlim: 6   bits: 4/3
c ---[1459]---> Adder-cost: 15   maxlim: 6   bits: 4/3
c ---[1458]---> Adder-cost: 15   maxlim: 6   bits: 4/3
c ---[1457]---> Adder-cost: 15   maxlim: 6   bits: 4/3
c ---[1456]---> Adder-cost: 15   maxlim: 6   bits: 4/3
c ---[1455]---> Adder-cost: 9   maxlim: 5   bits: 4/3
c ---[1454]---> Adder-cost: 9   maxlim: 5   bits: 4/3
c ---[1453]---> Adder-cost: 9   maxlim: 5   bits: 4/3
c ---[1452]---> Adder-cost: 9   maxlim: 5   bits: 4/3
c ---[1451]---> Adder-cost: 9   maxlim: 5   bits: 4/3
c ---[1450]---> Adder-cost: 9   maxlim: 5   bits: 4/3
c ---[1449]---> Adder-cost: 9   maxlim: 5   bits: 4/3
c ---[1448]---> Adder-cost: 9   maxlim: 5   bits: 4/3
c ---[1447]---> Adder-cost: 8   maxlim: 4   bits: 4/3
c ---[1446]---> Adder-cost: 8   maxlim: 4   bits: 4/3
c ---[1445]---> Adder-cost: 8   maxlim: 4   bits: 4/3
c ---[1444]---> Adder-cost: 8   maxlim: 4   bits: 4/3
c ---[1443]---> Adder-cost: 8   maxlim: 4   bits: 4/3
c ---[1442]---> Adder-cost: 8   maxlim: 4   bits: 4/3
c ---[1441]---> Adder-cost: 8   maxlim: 4   bits: 4/3
c ---[1440]---> Adder-cost: 8   maxlim: 4   bits: 4/3
c ---[1439]---> Adder-cost: 2   maxlim: 3   bits: 3/2
c ---[1438]---> Adder-cost: 2   maxlim: 3   bits: 3/2
c ---[1437]---> Adder-cost: 2   maxlim: 3   bits: 3/2
c ---[1436]---> Adder-cost: 2   maxlim: 3   bits: 3/2
c ---[1435]---> Adder-cost: 2   maxlim: 3   bits: 3/2
c ---[1434]---> Adder-cost: 2   maxlim: 3   bits: 3/2
c ---[1433]---> Adder-cost: 2   maxlim: 3   bits: 3/2
c ---[1432]---> Adder-cost: 2   maxlim: 3   bits: 3/2
c ---[1431]---> Adder-cost: 7   maxlim: 2   bits: 3/2
c ---[1430]---> Adder-cost: 7   maxlim: 2   bits: 3/2
c ---[1429]---> Adder-cost: 7   maxlim: 2   bits: 3/2
c ---[1428]---> Adder-cost: 7   maxlim: 2   bits: 3/2
c ---[1427]---> Adder-cost: 7   maxlim: 2   bits: 3/2
c ---[1426]---> Adder-cost: 7   maxlim: 2   bits: 3/2
c ---[1425]---> Adder-cost: 7   maxlim: 2   bits: 3/2
c ---[1424]---> Adder-cost: 7   maxlim: 2   bits: 3/2
c ---[1423]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1422]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1421]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1420]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1419]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1418]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1417]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1416]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1407]---> Adder-cost: 2   maxlim: 7   bits: 4/3
c ---[1406]---> Adder-cost: 2   maxlim: 7   bits: 4/3
c ---[1405]---> Adder-cost: 2   maxlim: 7   bits: 4/3
c ---[1404]---> Adder-cost: 2   maxlim: 7   bits: 4/3
c ---[1403]---> Adder-cost: 2   maxlim: 7   bits: 4/3
c ---[1402]---> Adder-cost: 2   maxlim: 7   bits: 4/3
c ---[1401]---> Adder-cost: 2   maxlim: 7   bits: 4/3
c ---[1400]---> Adder-cost: 2   maxlim: 7   bits: 4/3
c ---[1399]---> Adder-cost: 15   maxlim: 6   bits: 4/3
c ---[1398]---> Adder-cost: 15   maxlim: 6   bits: 4/3
c ---[1397]---> Adder-cost: 15   maxlim: 6   bits: 4/3
c ---[1396]---> Adder-cost: 15   maxlim: 6   bits: 4/3
c ---[1395]---> Adder-cost: 15   maxlim: 6   bits: 4/3
c ---[1394]---> Adder-cost: 15   maxlim: 6   bits: 4/3
c ---[1393]---> Adder-cost: 15   maxlim: 6   bits: 4/3
c ---[1392]---> Adder-cost: 15   maxlim: 6   bits: 4/3
c ---[1391]---> Adder-cost: 9   maxlim: 5   bits: 4/3
c ---[1390]---> Adder-cost: 9   maxlim: 5   bits: 4/3
c ---[1389]---> Adder-cost: 9   maxlim: 5   bits: 4/3
c ---[1388]---> Adder-cost: 9   maxlim: 5   bits: 4/3
c ---[1387]---> Adder-cost: 9   maxlim: 5   bits: 4/3
c ---[1386]---> Adder-cost: 9   maxlim: 5   bits: 4/3
c ---[1385]---> Adder-cost: 9   maxlim: 5   bits: 4/3
c ---[1384]---> Adder-cost: 9   maxlim: 5   bits: 4/3
c ---[1383]---> Adder-cost: 8   maxlim: 4   bits: 4/3
c ---[1382]---> Adder-cost: 8   maxlim: 4   bits: 4/3
c ---[1381]---> Adder-cost: 8   maxlim: 4   bits: 4/3
c ---[1380]---> Adder-cost: 8   maxlim: 4   bits: 4/3
c ---[1379]---> Adder-cost: 8   maxlim: 4   bits: 4/3
c ---[1378]---> Adder-cost: 8   maxlim: 4   bits: 4/3
c ---[1377]---> Adder-cost: 8   maxlim: 4   bits: 4/3
c ---[1376]---> Adder-cost: 8   maxlim: 4   bits: 4/3
c ---[1375]---> Adder-cost: 2   maxlim: 3   bits: 3/2
c ---[1374]---> Adder-cost: 2   maxlim: 3   bits: 3/2
c ---[1373]---> Adder-cost: 2   maxlim: 3   bits: 3/2
c ---[1372]---> Adder-cost: 2   maxlim: 3   bits: 3/2
c ---[1371]---> Adder-cost: 2   maxlim: 3   bits: 3/2
c ---[1370]---> Adder-cost: 2   maxlim: 3   bits: 3/2
c ---[1369]---> Adder-cost: 2   maxlim: 3   bits: 3/2
c ---[1368]---> Adder-cost: 2   maxlim: 3   bits: 3/2
c ---[1367]---> Adder-cost: 7   maxlim: 2   bits: 3/2
c ---[1366]---> Adder-cost: 7   maxlim: 2   bits: 3/2
c ---[1365]---> Adder-cost: 7   maxlim: 2   bits: 3/2
c ---[1364]---> Adder-cost: 7   maxlim: 2   bits: 3/2
c ---[1363]---> Adder-cost: 7   maxlim: 2   bits: 3/2
c ---[1362]---> Adder-cost: 7   maxlim: 2   bits: 3/2
c ---[1361]---> Adder-cost: 7   maxlim: 2   bits: 3/2
c ---[1360]---> Adder-cost: 7   maxlim: 2   bits: 3/2
c ---[1359]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1358]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1357]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1356]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1355]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1354]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1353]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1352]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1343]---> Adder-cost: 2   maxlim: 7   bits: 4/3
c ---[1342]---> Adder-cost: 2   maxlim: 7   bits: 4/3
c ---[1341]---> Adder-cost: 2   maxlim: 7   bits: 4/3
c ---[1340]---> Adder-cost: 2   maxlim: 7   bits: 4/3
c ---[1339]---> Adder-cost: 2   maxlim: 7   bits: 4/3
c ---[1338]---> Adder-cost: 2   maxlim: 7   bits: 4/3
c ---[1337]---> Adder-cost: 2   maxlim: 7   bits: 4/3
c ---[1336]---> Adder-cost: 2   maxlim: 7   bits: 4/3
c ---[1335]---> Adder-cost: 15   maxlim: 6   bits: 4/3
c ---[1334]---> Adder-cost: 15   maxlim: 6   bits: 4/3
c ---[1333]---> Adder-cost: 15   maxlim: 6   bits: 4/3
c ---[1332]---> Adder-cost: 15   maxlim: 6   bits: 4/3
c ---[1331]---> Adder-cost: 15   maxlim: 6   bits: 4/3
c ---[1330]---> Adder-cost: 15   maxlim: 6   bits: 4/3
c ---[1329]---> Adder-cost: 15   maxlim: 6   bits: 4/3
c ---[1328]---> Adder-cost: 15   maxlim: 6   bits: 4/3
c ---[1327]---> Adder-cost: 9   maxlim: 5   bits: 4/3
c ---[1326]---> Adder-cost: 9   maxlim: 5   bits: 4/3
c ---[1325]---> Adder-cost: 9   maxlim: 5   bits: 4/3
c ---[1324]---> Adder-cost: 9   maxlim: 5   bits: 4/3
c ---[1323]---> Adder-cost: 9   maxlim: 5   bits: 4/3
c ---[1322]---> Adder-cost: 9   maxlim: 5   bits: 4/3
c ---[1321]---> Adder-cost: 9   maxlim: 5   bits: 4/3
c ---[1320]---> Adder-cost: 9   maxlim: 5   bits: 4/3
c ---[1319]---> Adder-cost: 8   maxlim: 4   bits: 4/3
c ---[1318]---> Adder-cost: 8   maxlim: 4   bits: 4/3
c ---[1317]---> Adder-cost: 8   maxlim: 4   bits: 4/3
c ---[1316]---> Adder-cost: 8   maxlim: 4   bits: 4/3
c ---[1315]---> Adder-cost: 8   maxlim: 4   bits: 4/3
c ---[1314]---> Adder-cost: 8   maxlim: 4   bits: 4/3
c ---[1313]---> Adder-cost: 8   maxlim: 4   bits: 4/3
c ---[1312]---> Adder-cost: 8   maxlim: 4   bits: 4/3
c ---[1311]---> Adder-cost: 2   maxlim: 3   bits: 3/2
c ---[1310]---> Adder-cost: 2   maxlim: 3   bits: 3/2
c ---[1309]---> Adder-cost: 2   maxlim: 3   bits: 3/2
c ---[1308]---> Adder-cost: 2   maxlim: 3   bits: 3/2
c ---[1307]---> Adder-cost: 2   maxlim: 3   bits: 3/2
c ---[1306]---> Adder-cost: 2   maxlim: 3   bits: 3/2
c ---[1305]---> Adder-cost: 2   maxlim: 3   bits: 3/2
c ---[1304]---> Adder-cost: 2   maxlim: 3   bits: 3/2
c ---[1303]---> Adder-cost: 7   maxlim: 2   bits: 3/2
c ---[1302]---> Adder-cost: 7   maxlim: 2   bits: 3/2
c ---[1301]---> Adder-cost: 7   maxlim: 2   bits: 3/2
c ---[1300]---> Adder-cost: 7   maxlim: 2   bits: 3/2
c ---[1299]---> Adder-cost: 7   maxlim: 2   bits: 3/2
c ---[1298]---> Adder-cost: 7   maxlim: 2   bits: 3/2
c ---[1297]---> Adder-cost: 7   maxlim: 2   bits: 3/2
c ---[1296]---> Adder-cost: 7   maxlim: 2   bits: 3/2
c ---[1295]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1294]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1293]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1292]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1291]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1290]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1289]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1288]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1279]---> Adder-cost: 16   maxlim: 7   bits: 4/3
c ---[1278]---> Adder-cost: 2   maxlim: 7   bits: 4/3
c ---[1277]---> Adder-cost: 12   maxlim: 7   bits: 4/3
c ---[1276]---> Adder-cost: 2   maxlim: 7   bits: 4/3
c ---[1275]---> Adder-cost: 12   maxlim: 7   bits: 4/3
c ---[1274]---> Adder-cost: 2   maxlim: 7   bits: 4/3
c ---[1273]---> Adder-cost: 16   maxlim: 7   bits: 4/3
c ---[1272]---> Adder-cost: 2   maxlim: 7   bits: 4/3
c ---[1271]---> Adder-cost: 15   maxlim: 6   bits: 4/3
c ---[1270]---> Adder-cost: 15   maxlim: 6   bits: 4/3
c ---[1269]---> Adder-cost: 15   maxlim: 6   bits: 4/3
c ---[1268]---> Adder-cost: 15   maxlim: 6   bits: 4/3
c ---[1267]---> Adder-cost: 15   maxlim: 6   bits: 4/3
c ---[1266]---> Adder-cost: 15   maxlim: 6   bits: 4/3
c ---[1265]---> Adder-cost: 15   maxlim: 6   bits: 4/3
c ---[1264]---> Adder-cost: 15   maxlim: 6   bits: 4/3
c ---[1263]---> Adder-cost: 15   maxlim: 5   bits: 4/3
c ---[1262]---> Adder-cost: 9   maxlim: 5   bits: 4/3
c ---[1261]---> Adder-cost: 11   maxlim: 5   bits: 4/3
c ---[1260]---> Adder-cost: 9   maxlim: 5   bits: 4/3
c ---[1259]---> Adder-cost: 13   maxlim: 5   bits: 4/3
c ---[1258]---> Adder-cost: 9   maxlim: 5   bits: 4/3
c ---[1257]---> Adder-cost: 15   maxlim: 5   bits: 4/3
c ---[1256]---> Adder-cost: 9   maxlim: 5   bits: 4/3
c ---[1255]---> Adder-cost: 8   maxlim: 4   bits: 4/3
c ---[1254]---> Adder-cost: 8   maxlim: 4   bits: 4/3
c ---[1253]---> Adder-cost: 8   maxlim: 4   bits: 4/3
c ---[1252]---> Adder-cost: 8   maxlim: 4   bits: 4/3
c ---[1251]---> Adder-cost: 8   maxlim: 4   bits: 4/3
c ---[1250]---> Adder-cost: 8   maxlim: 4   bits: 4/3
c ---[1249]---> Adder-cost: 8   maxlim: 4   bits: 4/3
c ---[1248]---> Adder-cost: 8   maxlim: 4   bits: 4/3
c ---[1247]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[1246]---> Adder-cost: 2   maxlim: 3   bits: 3/2
c ---[1245]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[1244]---> Adder-cost: 2   maxlim: 3   bits: 3/2
c ---[1243]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[1242]---> Adder-cost: 2   maxlim: 3   bits: 3/2
c ---[1241]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[1240]---> Adder-cost: 2   maxlim: 3   bits: 3/2
c ---[1239]---> Adder-cost: 7   maxlim: 2   bits: 3/2
c ---[1238]---> Adder-cost: 7   maxlim: 2   bits: 3/2
c ---[1237]---> Adder-cost: 7   maxlim: 2   bits: 3/2
c ---[1236]---> Adder-cost: 7   maxlim: 2   bits: 3/2
c ---[1235]---> Adder-cost: 7   maxlim: 2   bits: 3/2
c ---[1234]---> Adder-cost: 7   maxlim: 2   bits: 3/2
c ---[1233]---> Adder-cost: 7   maxlim: 2   bits: 3/2
c ---[1232]---> Adder-cost: 7   maxlim: 2   bits: 3/2
c ---[1231]---> Adder-cost: 4   maxlim: 1   bits: 2/1
c ---[1230]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1229]---> Adder-cost: 4   maxlim: 1   bits: 2/1
c ---[1228]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1227]---> Adder-cost: 4   maxlim: 1   bits: 2/1
c ---[1226]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1225]---> Adder-cost: 4   maxlim: 1   bits: 2/1
c ---[1224]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1215]---> Adder-cost: 12   maxlim: 7   bits: 4/3
c ---[1214]---> Adder-cost: 2   maxlim: 7   bits: 4/3
c ---[1213]---> Adder-cost: 2   maxlim: 7   bits: 4/3
c ---[1212]---> Adder-cost: 2   maxlim: 7   bits: 4/3
c ---[1211]---> Adder-cost: 2   maxlim: 7   bits: 4/3
c ---[1210]---> Adder-cost: 2   maxlim: 7   bits: 4/3
c ---[1209]---> Adder-cost: 2   maxlim: 7   bits: 4/3
c ---[1208]---> Adder-cost: 2   maxlim: 7   bits: 4/3
c ---[1207]---> Adder-cost: 15   maxlim: 6   bits: 4/3
c ---[1206]---> Adder-cost: 15   maxlim: 6   bits: 4/3
c ---[1205]---> Adder-cost: 15   maxlim: 6   bits: 4/3
c ---[1204]---> Adder-cost: 15   maxlim: 6   bits: 4/3
c ---[1203]---> Adder-cost: 15   maxlim: 6   bits: 4/3
c ---[1202]---> Adder-cost: 15   maxlim: 6   bits: 4/3
c ---[1201]---> Adder-cost: 15   maxlim: 6   bits: 4/3
c ---[1200]---> Adder-cost: 15   maxlim: 6   bits: 4/3
c ---[1199]---> Adder-cost: 13   maxlim: 5   bits: 4/3
c ---[1198]---> Adder-cost: 9   maxlim: 5   bits: 4/3
c ---[1197]---> Adder-cost: 9   maxlim: 5   bits: 4/3
c ---[1196]---> Adder-cost: 9   maxlim: 5   bits: 4/3
c ---[1195]---> Adder-cost: 9   maxlim: 5   bits: 4/3
c ---[1194]---> Adder-cost: 9   maxlim: 5   bits: 4/3
c ---[1193]---> Adder-cost: 9   maxlim: 5   bits: 4/3
c ---[1192]---> Adder-cost: 9   maxlim: 5   bits: 4/3
c ---[1191]---> Adder-cost: 8   maxlim: 4   bits: 4/3
c ---[1190]---> Adder-cost: 8   maxlim: 4   bits: 4/3
c ---[1189]---> Adder-cost: 8   maxlim: 4   bits: 4/3
c ---[1188]---> Adder-cost: 8   maxlim: 4   bits: 4/3
c ---[1187]---> Adder-cost: 8   maxlim: 4   bits: 4/3
c ---[1186]---> Adder-cost: 8   maxlim: 4   bits: 4/3
c ---[1185]---> Adder-cost: 8   maxlim: 4   bits: 4/3
c ---[1184]---> Adder-cost: 8   maxlim: 4   bits: 4/3
c ---[1183]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[1182]---> Adder-cost: 2   maxlim: 3   bits: 3/2
c ---[1181]---> Adder-cost: 2   maxlim: 3   bits: 3/2
c ---[1180]---> Adder-cost: 2   maxlim: 3   bits: 3/2
c ---[1179]---> Adder-cost: 2   maxlim: 3   bits: 3/2
c ---[1178]---> Adder-cost: 2   maxlim: 3   bits: 3/2
c ---[1177]---> Adder-cost: 2   maxlim: 3   bits: 3/2
c ---[1176]---> Adder-cost: 2   maxlim: 3   bits: 3/2
c ---[1175]---> Adder-cost: 7   maxlim: 2   bits: 3/2
c ---[1174]---> Adder-cost: 7   maxlim: 2   bits: 3/2
c ---[1173]---> Adder-cost: 7   maxlim: 2   bits: 3/2
c ---[1172]---> Adder-cost: 7   maxlim: 2   bits: 3/2
c ---[1171]---> Adder-cost: 7   maxlim: 2   bits: 3/2
c ---[1170]---> Adder-cost: 7   maxlim: 2   bits: 3/2
c ---[1169]---> Adder-cost: 7   maxlim: 2   bits: 3/2
c ---[1168]---> Adder-cost: 7   maxlim: 2   bits: 3/2
c ---[1167]---> Adder-cost: 4   maxlim: 1   bits: 2/1
c ---[1166]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1165]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1164]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1163]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1162]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1161]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1160]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1151]---> Adder-cost: 2   maxlim: 7   bits: 4/3
c ---[1150]---> Adder-cost: 2   maxlim: 7   bits: 4/3
c ---[1149]---> Adder-cost: 2   maxlim: 7   bits: 4/3
c ---[1148]---> Adder-cost: 2   maxlim: 7   bits: 4/3
c ---[1147]---> Adder-cost: 2   maxlim: 7   bits: 4/3
c ---[1146]---> Adder-cost: 2   maxlim: 7   bits: 4/3
c ---[1145]---> Adder-cost: 2   maxlim: 7   bits: 4/3
c ---[1144]---> Adder-cost: 2   maxlim: 7   bits: 4/3
c ---[1143]---> Adder-cost: 15   maxlim: 6   bits: 4/3
c ---[1142]---> Adder-cost: 15   maxlim: 6   bits: 4/3
c ---[1141]---> Adder-cost: 15   maxlim: 6   bits: 4/3
c ---[1140]---> Adder-cost: 15   maxlim: 6   bits: 4/3
c ---[1139]---> Adder-cost: 15   maxlim: 6   bits: 4/3
c ---[1138]---> Adder-cost: 15   maxlim: 6   bits: 4/3
c ---[1137]---> Adder-cost: 15   maxlim: 6   bits: 4/3
c ---[1136]---> Adder-cost: 15   maxlim: 6   bits: 4/3
c ---[1135]---> Adder-cost: 9   maxlim: 5   bits: 4/3
c ---[1134]---> Adder-cost: 9   maxlim: 5   bits: 4/3
c ---[1133]---> Adder-cost: 9   maxlim: 5   bits: 4/3
c ---[1132]---> Adder-cost: 9   maxlim: 5   bits: 4/3
c ---[1131]---> Adder-cost: 9   maxlim: 5   bits: 4/3
c ---[1130]---> Adder-cost: 9   maxlim: 5   bits: 4/3
c ---[1129]---> Adder-cost: 9   maxlim: 5   bits: 4/3
c ---[1128]---> Adder-cost: 9   maxlim: 5   bits: 4/3
c ---[1127]---> Adder-cost: 8   maxlim: 4   bits: 4/3
c ---[1126]---> Adder-cost: 8   maxlim: 4   bits: 4/3
c ---[1125]---> Adder-cost: 8   maxlim: 4   bits: 4/3
c ---[1124]---> Adder-cost: 8   maxlim: 4   bits: 4/3
c ---[1123]---> Adder-cost: 8   maxlim: 4   bits: 4/3
c ---[1122]---> Adder-cost: 8   maxlim: 4   bits: 4/3
c ---[1121]---> Adder-cost: 8   maxlim: 4   bits: 4/3
c ---[1120]---> Adder-cost: 8   maxlim: 4   bits: 4/3
c ---[1119]---> Adder-cost: 2   maxlim: 3   bits: 3/2
c ---[1118]---> Adder-cost: 2   maxlim: 3   bits: 3/2
c ---[1117]---> Adder-cost: 2   maxlim: 3   bits: 3/2
c ---[1116]---> Adder-cost: 2   maxlim: 3   bits: 3/2
c ---[1115]---> Adder-cost: 2   maxlim: 3   bits: 3/2
c ---[1114]---> Adder-cost: 2   maxlim: 3   bits: 3/2
c ---[1113]---> Adder-cost: 2   maxlim: 3   bits: 3/2
c ---[1112]---> Adder-cost: 2   maxlim: 3   bits: 3/2
c ---[1111]---> Adder-cost: 7   maxlim: 2   bits: 3/2
c ---[1110]---> Adder-cost: 7   maxlim: 2   bits: 3/2
c ---[1109]---> Adder-cost: 7   maxlim: 2   bits: 3/2
c ---[1108]---> Adder-cost: 7   maxlim: 2   bits: 3/2
c ---[1107]---> Adder-cost: 7   maxlim: 2   bits: 3/2
c ---[1106]---> Adder-cost: 7   maxlim: 2   bits: 3/2
c ---[1105]---> Adder-cost: 7   maxlim: 2   bits: 3/2
c ---[1104]---> Adder-cost: 7   maxlim: 2   bits: 3/2
c ---[1103]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1102]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1101]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1100]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1099]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1098]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1097]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1096]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1087]---> Adder-cost: 2   maxlim: 7   bits: 4/3
c ---[1086]---> Adder-cost: 2   maxlim: 7   bits: 4/3
c ---[1085]---> Adder-cost: 2   maxlim: 7   bits: 4/3
c ---[1084]---> Adder-cost: 2   maxlim: 7   bits: 4/3
c ---[1083]---> Adder-cost: 2   maxlim: 7   bits: 4/3
c ---[1082]---> Adder-cost: 2   maxlim: 7   bits: 4/3
c ---[1081]---> Adder-cost: 2   maxlim: 7   bits: 4/3
c ---[1080]---> Adder-cost: 2   maxlim: 7   bits: 4/3
c ---[1079]---> Adder-cost: 15   maxlim: 6   bits: 4/3
c ---[1078]---> Adder-cost: 15   maxlim: 6   bits: 4/3
c ---[1077]---> Adder-cost: 15   maxlim: 6   bits: 4/3
c ---[1076]---> Adder-cost: 15   maxlim: 6   bits: 4/3
c ---[1075]---> Adder-cost: 15   maxlim: 6   bits: 4/3
c ---[1074]---> Adder-cost: 15   maxlim: 6   bits: 4/3
c ---[1073]---> Adder-cost: 15   maxlim: 6   bits: 4/3
c ---[1072]---> Adder-cost: 15   maxlim: 6   bits: 4/3
c ---[1071]---> Adder-cost: 9   maxlim: 5   bits: 4/3
c ---[1070]---> Adder-cost: 9   maxlim: 5   bits: 4/3
c ---[1069]---> Adder-cost: 9   maxlim: 5   bits: 4/3
c ---[1068]---> Adder-cost: 9   maxlim: 5   bits: 4/3
c ---[1067]---> Adder-cost: 9   maxlim: 5   bits: 4/3
c ---[1066]---> Adder-cost: 9   maxlim: 5   bits: 4/3
c ---[1065]---> Adder-cost: 9   maxlim: 5   bits: 4/3
c ---[1064]---> Adder-cost: 9   maxlim: 5   bits: 4/3
c ---[1063]---> Adder-cost: 8   maxlim: 4   bits: 4/3
c ---[1062]---> Adder-cost: 8   maxlim: 4   bits: 4/3
c ---[1061]---> Adder-cost: 8   maxlim: 4   bits: 4/3
c ---[1060]---> Adder-cost: 8   maxlim: 4   bits: 4/3
c ---[1059]---> Adder-cost: 8   maxlim: 4   bits: 4/3
c ---[1058]---> Adder-cost: 8   maxlim: 4   bits: 4/3
c ---[1057]---> Adder-cost: 8   maxlim: 4   bits: 4/3
c ---[1056]---> Adder-cost: 8   maxlim: 4   bits: 4/3
c ---[1055]---> Adder-cost: 2   maxlim: 3   bits: 3/2
c ---[1054]---> Adder-cost: 2   maxlim: 3   bits: 3/2
c ---[1053]---> Adder-cost: 2   maxlim: 3   bits: 3/2
c ---[1052]---> Adder-cost: 2   maxlim: 3   bits: 3/2
c ---[1051]---> Adder-cost: 2   maxlim: 3   bits: 3/2
c ---[1050]---> Adder-cost: 2   maxlim: 3   bits: 3/2
c ---[1049]---> Adder-cost: 2   maxlim: 3   bits: 3/2
c ---[1048]---> Adder-cost: 2   maxlim: 3   bits: 3/2
c ---[1047]---> Adder-cost: 7   maxlim: 2   bits: 3/2
c ---[1046]---> Adder-cost: 7   maxlim: 2   bits: 3/2
c ---[1045]---> Adder-cost: 7   maxlim: 2   bits: 3/2
c ---[1044]---> Adder-cost: 7   maxlim: 2   bits: 3/2
c ---[1043]---> Adder-cost: 7   maxlim: 2   bits: 3/2
c ---[1042]---> Adder-cost: 7   maxlim: 2   bits: 3/2
c ---[1041]---> Adder-cost: 7   maxlim: 2   bits: 3/2
c ---[1040]---> Adder-cost: 7   maxlim: 2   bits: 3/2
c ---[1039]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1038]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1037]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1036]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1035]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1034]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1033]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1032]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1023]---> Adder-cost: 2   maxlim: 7   bits: 4/3
c ---[1022]---> Adder-cost: 2   maxlim: 7   bits: 4/3
c ---[1021]---> Adder-cost: 2   maxlim: 7   bits: 4/3
c ---[1020]---> Adder-cost: 2   maxlim: 7   bits: 4/3
c ---[1019]---> Adder-cost: 2   maxlim: 7   bits: 4/3
c ---[1018]---> Adder-cost: 2   maxlim: 7   bits: 4/3
c ---[1017]---> Adder-cost: 2   maxlim: 7   bits: 4/3
c ---[1016]---> Adder-cost: 2   maxlim: 7   bits: 4/3
c ---[1015]---> Adder-cost: 15   maxlim: 6   bits: 4/3
c ---[1014]---> Adder-cost: 15   maxlim: 6   bits: 4/3
c ---[1013]---> Adder-cost: 15   maxlim: 6   bits: 4/3
c ---[1012]---> Adder-cost: 15   maxlim: 6   bits: 4/3
c ---[1011]---> Adder-cost: 15   maxlim: 6   bits: 4/3
c ---[1010]---> Adder-cost: 15   maxlim: 6   bits: 4/3
c ---[1009]---> Adder-cost: 15   maxlim: 6   bits: 4/3
c ---[1008]---> Adder-cost: 15   maxlim: 6   bits: 4/3
c ---[1007]---> Adder-cost: 9   maxlim: 5   bits: 4/3
c ---[1006]---> Adder-cost: 9   maxlim: 5   bits: 4/3
c ---[1005]---> Adder-cost: 9   maxlim: 5   bits: 4/3
c ---[1004]---> Adder-cost: 9   maxlim: 5   bits: 4/3
c ---[1003]---> Adder-cost: 9   maxlim: 5   bits: 4/3
c ---[1002]---> Adder-cost: 9   maxlim: 5   bits: 4/3
c ---[1001]---> Adder-cost: 9   maxlim: 5   bits: 4/3
c ---[1000]---> Adder-cost: 9   maxlim: 5   bits: 4/3
c ---[ 999]---> Adder-cost: 8   maxlim: 4   bits: 4/3
c ---[ 998]---> Adder-cost: 8   maxlim: 4   bits: 4/3
c ---[ 997]---> Adder-cost: 8   maxlim: 4   bits: 4/3
c ---[ 996]---> Adder-cost: 8   maxlim: 4   bits: 4/3
c ---[ 995]---> Adder-cost: 8   maxlim: 4   bits: 4/3
c ---[ 994]---> Adder-cost: 8   maxlim: 4   bits: 4/3
c ---[ 993]---> Adder-cost: 8   maxlim: 4   bits: 4/3
c ---[ 992]---> Adder-cost: 8   maxlim: 4   bits: 4/3
c ---[ 991]---> Adder-cost: 2   maxlim: 3   bits: 3/2
c ---[ 990]---> Adder-cost: 2   maxlim: 3   bits: 3/2
c ---[ 989]---> Adder-cost: 2   maxlim: 3   bits: 3/2
c ---[ 988]---> Adder-cost: 2   maxlim: 3   bits: 3/2
c ---[ 987]---> Adder-cost: 2   maxlim: 3   bits: 3/2
c ---[ 986]---> Adder-cost: 2   maxlim: 3   bits: 3/2
c ---[ 985]---> Adder-cost: 2   maxlim: 3   bits: 3/2
c ---[ 984]---> Adder-cost: 2   maxlim: 3   bits: 3/2
c ---[ 983]---> Adder-cost: 7   maxlim: 2   bits: 3/2
c ---[ 982]---> Adder-cost: 7   maxlim: 2   bits: 3/2
c ---[ 981]---> Adder-cost: 7   maxlim: 2   bits: 3/2
c ---[ 980]---> Adder-cost: 7   maxlim: 2   bits: 3/2
c ---[ 979]---> Adder-cost: 7   maxlim: 2   bits: 3/2
c ---[ 978]---> Adder-cost: 7   maxlim: 2   bits: 3/2
c ---[ 977]---> Adder-cost: 7   maxlim: 2   bits: 3/2
c ---[ 976]---> Adder-cost: 7   maxlim: 2   bits: 3/2
c ---[ 975]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 974]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 973]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 972]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 971]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 970]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 969]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 968]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 959]---> Adder-cost: 16   maxlim: 7   bits: 4/3
c ---[ 958]---> Adder-cost: 2   maxlim: 7   bits: 4/3
c ---[ 957]---> Adder-cost: 12   maxlim: 7   bits: 4/3
c ---[ 956]---> Adder-cost: 2   maxlim: 7   bits: 4/3
c ---[ 955]---> Adder-cost: 12   maxlim: 7   bits: 4/3
c ---[ 954]---> Adder-cost: 2   maxlim: 7   bits: 4/3
c ---[ 953]---> Adder-cost: 16   maxlim: 7   bits: 4/3
c ---[ 952]---> Adder-cost: 2   maxlim: 7   bits: 4/3
c ---[ 951]---> Adder-cost: 15   maxlim: 6   bits: 4/3
c ---[ 950]---> Adder-cost: 15   maxlim: 6   bits: 4/3
c ---[ 949]---> Adder-cost: 15   maxlim: 6   bits: 4/3
c ---[ 948]---> Adder-cost: 15   maxlim: 6   bits: 4/3
c ---[ 947]---> Adder-cost: 15   maxlim: 6   bits: 4/3
c ---[ 946]---> Adder-cost: 15   maxlim: 6   bits: 4/3
c ---[ 945]---> Adder-cost: 15   maxlim: 6   bits: 4/3
c ---[ 944]---> Adder-cost: 15   maxlim: 6   bits: 4/3
c ---[ 943]---> Adder-cost: 15   maxlim: 5   bits: 4/3
c ---[ 942]---> Adder-cost: 9   maxlim: 5   bits: 4/3
c ---[ 941]---> Adder-cost: 11   maxlim: 5   bits: 4/3
c ---[ 940]---> Adder-cost: 9   maxlim: 5   bits: 4/3
c ---[ 939]---> Adder-cost: 13   maxlim: 5   bits: 4/3
c ---[ 938]---> Adder-cost: 9   maxlim: 5   bits: 4/3
c ---[ 937]---> Adder-cost: 15   maxlim: 5   bits: 4/3
c ---[ 936]---> Adder-cost: 9   maxlim: 5   bits: 4/3
c ---[ 935]---> Adder-cost: 8   maxlim: 4   bits: 4/3
c ---[ 934]---> Adder-cost: 8   maxlim: 4   bits: 4/3
c ---[ 933]---> Adder-cost: 8   maxlim: 4   bits: 4/3
c ---[ 932]---> Adder-cost: 8   maxlim: 4   bits: 4/3
c ---[ 931]---> Adder-cost: 8   maxlim: 4   bits: 4/3
c ---[ 930]---> Adder-cost: 8   maxlim: 4   bits: 4/3
c ---[ 929]---> Adder-cost: 8   maxlim: 4   bits: 4/3
c ---[ 928]---> Adder-cost: 8   maxlim: 4   bits: 4/3
c ---[ 927]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[ 926]---> Adder-cost: 2   maxlim: 3   bits: 3/2
c ---[ 925]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[ 924]---> Adder-cost: 2   maxlim: 3   bits: 3/2
c ---[ 923]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[ 922]---> Adder-cost: 2   maxlim: 3   bits: 3/2
c ---[ 921]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[ 920]---> Adder-cost: 2   maxlim: 3   bits: 3/2
c ---[ 919]---> Adder-cost: 7   maxlim: 2   bits: 3/2
c ---[ 918]---> Adder-cost: 7   maxlim: 2   bits: 3/2
c ---[ 917]---> Adder-cost: 7   maxlim: 2   bits: 3/2
c ---[ 916]---> Adder-cost: 7   maxlim: 2   bits: 3/2
c ---[ 915]---> Adder-cost: 7   maxlim: 2   bits: 3/2
c ---[ 914]---> Adder-cost: 7   maxlim: 2   bits: 3/2
c ---[ 913]---> Adder-cost: 7   maxlim: 2   bits: 3/2
c ---[ 912]---> Adder-cost: 7   maxlim: 2   bits: 3/2
c ---[ 911]---> Adder-cost: 4   maxlim: 1   bits: 2/1
c ---[ 910]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 909]---> Adder-cost: 4   maxlim: 1   bits: 2/1
c ---[ 908]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 907]---> Adder-cost: 4   maxlim: 1   bits: 2/1
c ---[ 906]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 905]---> Adder-cost: 4   maxlim: 1   bits: 2/1
c ---[ 904]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 895]---> Adder-cost: 12   maxlim: 7   bits: 4/3
c ---[ 894]---> Adder-cost: 2   maxlim: 7   bits: 4/3
c ---[ 893]---> Adder-cost: 2   maxlim: 7   bits: 4/3
c ---[ 892]---> Adder-cost: 2   maxlim: 7   bits: 4/3
c ---[ 891]---> Adder-cost: 2   maxlim: 7   bits: 4/3
c ---[ 890]---> Adder-cost: 2   maxlim: 7   bits: 4/3
c ---[ 889]---> Adder-cost: 2   maxlim: 7   bits: 4/3
c ---[ 888]---> Adder-cost: 2   maxlim: 7   bits: 4/3
c ---[ 887]---> Adder-cost: 15   maxlim: 6   bits: 4/3
c ---[ 886]---> Adder-cost: 15   maxlim: 6   bits: 4/3
c ---[ 885]---> Adder-cost: 15   maxlim: 6   bits: 4/3
c ---[ 884]---> Adder-cost: 15   maxlim: 6   bits: 4/3
c ---[ 883]---> Adder-cost: 15   maxlim: 6   bits: 4/3
c ---[ 882]---> Adder-cost: 15   maxlim: 6   bits: 4/3
c ---[ 881]---> Adder-cost: 15   maxlim: 6   bits: 4/3
c ---[ 880]---> Adder-cost: 15   maxlim: 6   bits: 4/3
c ---[ 879]---> Adder-cost: 13   maxlim: 5   bits: 4/3
c ---[ 878]---> Adder-cost: 9   maxlim: 5   bits: 4/3
c ---[ 877]---> Adder-cost: 9   maxlim: 5   bits: 4/3
c ---[ 876]---> Adder-cost: 9   maxlim: 5   bits: 4/3
c ---[ 875]---> Adder-cost: 9   maxlim: 5   bits: 4/3
c ---[ 874]---> Adder-cost: 9   maxlim: 5   bits: 4/3
c ---[ 873]---> Adder-cost: 9   maxlim: 5   bits: 4/3
c ---[ 872]---> Adder-cost: 9   maxlim: 5   bits: 4/3
c ---[ 871]---> Adder-cost: 8   maxlim: 4   bits: 4/3
c ---[ 870]---> Adder-cost: 8   maxlim: 4   bits: 4/3
c ---[ 869]---> Adder-cost: 8   maxlim: 4   bits: 4/3
c ---[ 868]---> Adder-cost: 8   maxlim: 4   bits: 4/3
c ---[ 867]---> Adder-cost: 8   maxlim: 4   bits: 4/3
c ---[ 866]---> Adder-cost: 8   maxlim: 4   bits: 4/3
c ---[ 865]---> Adder-cost: 8   maxlim: 4   bits: 4/3
c ---[ 864]---> Adder-cost: 8   maxlim: 4   bits: 4/3
c ---[ 863]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[ 862]---> Adder-cost: 2   maxlim: 3   bits: 3/2
c ---[ 861]---> Adder-cost: 2   maxlim: 3   bits: 3/2
c ---[ 860]---> Adder-cost: 2   maxlim: 3   bits: 3/2
c ---[ 859]---> Adder-cost: 2   maxlim: 3   bits: 3/2
c ---[ 858]---> Adder-cost: 2   maxlim: 3   bits: 3/2
c ---[ 857]---> Adder-cost: 2   maxlim: 3   bits: 3/2
c ---[ 856]---> Adder-cost: 2   maxlim: 3   bits: 3/2
c ---[ 855]---> Adder-cost: 7   maxlim: 2   bits: 3/2
c ---[ 854]---> Adder-cost: 7   maxlim: 2   bits: 3/2
c ---[ 853]---> Adder-cost: 7   maxlim: 2   bits: 3/2
c ---[ 852]---> Adder-cost: 7   maxlim: 2   bits: 3/2
c ---[ 851]---> Adder-cost: 7   maxlim: 2   bits: 3/2
c ---[ 850]---> Adder-cost: 7   maxlim: 2   bits: 3/2
c ---[ 849]---> Adder-cost: 7   maxlim: 2   bits: 3/2
c ---[ 848]---> Adder-cost: 7   maxlim: 2   bits: 3/2
c ---[ 847]---> Adder-cost: 4   maxlim: 1   bits: 2/1
c ---[ 846]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 845]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 844]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 843]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 842]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 841]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 840]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 831]---> Adder-cost: 2   maxlim: 7   bits: 4/3
c ---[ 830]---> Adder-cost: 2   maxlim: 7   bits: 4/3
c ---[ 829]---> Adder-cost: 2   maxlim: 7   bits: 4/3
c ---[ 828]---> Adder-cost: 2   maxlim: 7   bits: 4/3
c ---[ 827]---> Adder-cost: 2   maxlim: 7   bits: 4/3
c ---[ 826]---> Adder-cost: 2   maxlim: 7   bits: 4/3
c ---[ 825]---> Adder-cost: 2   maxlim: 7   bits: 4/3
c ---[ 824]---> Adder-cost: 2   maxlim: 7   bits: 4/3
c ---[ 823]---> Adder-cost: 15   maxlim: 6   bits: 4/3
c ---[ 822]---> Adder-cost: 15   maxlim: 6   bits: 4/3
c ---[ 821]---> Adder-cost: 15   maxlim: 6   bits: 4/3
c ---[ 820]---> Adder-cost: 15   maxlim: 6   bits: 4/3
c ---[ 819]---> Adder-cost: 15   maxlim: 6   bits: 4/3
c ---[ 818]---> Adder-cost: 15   maxlim: 6   bits: 4/3
c ---[ 817]---> Adder-cost: 15   maxlim: 6   bits: 4/3
c ---[ 816]---> Adder-cost: 15   maxlim: 6   bits: 4/3
c ---[ 815]---> Adder-cost: 9   maxlim: 5   bits: 4/3
c ---[ 814]---> Adder-cost: 9   maxlim: 5   bits: 4/3
c ---[ 813]---> Adder-cost: 9   maxlim: 5   bits: 4/3
c ---[ 812]---> Adder-cost: 9   maxlim: 5   bits: 4/3
c ---[ 811]---> Adder-cost: 9   maxlim: 5   bits: 4/3
c ---[ 810]---> Adder-cost: 9   maxlim: 5   bits: 4/3
c ---[ 809]---> Adder-cost: 9   maxlim: 5   bits: 4/3
c ---[ 808]---> Adder-cost: 9   maxlim: 5   bits: 4/3
c ---[ 807]---> Adder-cost: 8   maxlim: 4   bits: 4/3
c ---[ 806]---> Adder-cost: 8   maxlim: 4   bits: 4/3
c ---[ 805]---> Adder-cost: 8   maxlim: 4   bits: 4/3
c ---[ 804]---> Adder-cost: 8   maxlim: 4   bits: 4/3
c ---[ 803]---> Adder-cost: 8   maxlim: 4   bits: 4/3
c ---[ 802]---> Adder-cost: 8   maxlim: 4   bits: 4/3
c ---[ 801]---> Adder-cost: 8   maxlim: 4   bits: 4/3
c ---[ 800]---> Adder-cost: 8   maxlim: 4   bits: 4/3
c ---[ 799]---> Adder-cost: 2   maxlim: 3   bits: 3/2
c ---[ 798]---> Adder-cost: 2   maxlim: 3   bits: 3/2
c ---[ 797]---> Adder-cost: 2   maxlim: 3   bits: 3/2
c ---[ 796]---> Adder-cost: 2   maxlim: 3   bits: 3/2
c ---[ 795]---> Adder-cost: 2   maxlim: 3   bits: 3/2
c ---[ 794]---> Adder-cost: 2   maxlim: 3   bits: 3/2
c ---[ 793]---> Adder-cost: 2   maxlim: 3   bits: 3/2
c ---[ 792]---> Adder-cost: 2   maxlim: 3   bits: 3/2
c ---[ 791]---> Adder-cost: 7   maxlim: 2   bits: 3/2
c ---[ 790]---> Adder-cost: 7   maxlim: 2   bits: 3/2
c ---[ 789]---> Adder-cost: 7   maxlim: 2   bits: 3/2
c ---[ 788]---> Adder-cost: 7   maxlim: 2   bits: 3/2
c ---[ 787]---> Adder-cost: 7   maxlim: 2   bits: 3/2
c ---[ 786]---> Adder-cost: 7   maxlim: 2   bits: 3/2
c ---[ 785]---> Adder-cost: 7   maxlim: 2   bits: 3/2
c ---[ 784]---> Adder-cost: 7   maxlim: 2   bits: 3/2
c ---[ 783]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 782]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 781]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 780]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 779]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 778]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 777]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 776]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 767]---> Adder-cost: 2   maxlim: 7   bits: 4/3
c ---[ 766]---> Adder-cost: 2   maxlim: 7   bits: 4/3
c ---[ 765]---> Adder-cost: 2   maxlim: 7   bits: 4/3
c ---[ 764]---> Adder-cost: 2   maxlim: 7   bits: 4/3
c ---[ 763]---> Adder-cost: 2   maxlim: 7   bits: 4/3
c ---[ 762]---> Adder-cost: 2   maxlim: 7   bits: 4/3
c ---[ 761]---> Adder-cost: 2   maxlim: 7   bits: 4/3
c ---[ 760]---> Adder-cost: 2   maxlim: 7   bits: 4/3
c ---[ 759]---> Adder-cost: 15   maxlim: 6   bits: 4/3
c ---[ 758]---> Adder-cost: 15   maxlim: 6   bits: 4/3
c ---[ 757]---> Adder-cost: 15   maxlim: 6   bits: 4/3
c ---[ 756]---> Adder-cost: 15   maxlim: 6   bits: 4/3
c ---[ 755]---> Adder-cost: 15   maxlim: 6   bits: 4/3
c ---[ 754]---> Adder-cost: 15   maxlim: 6   bits: 4/3
c ---[ 753]---> Adder-cost: 15   maxlim: 6   bits: 4/3
c ---[ 752]---> Adder-cost: 15   maxlim: 6   bits: 4/3
c ---[ 751]---> Adder-cost: 9   maxlim: 5   bits: 4/3
c ---[ 750]---> Adder-cost: 9   maxlim: 5   bits: 4/3
c ---[ 749]---> Adder-cost: 9   maxlim: 5   bits: 4/3
c ---[ 748]---> Adder-cost: 9   maxlim: 5   bits: 4/3
c ---[ 747]---> Adder-cost: 9   maxlim: 5   bits: 4/3
c ---[ 746]---> Adder-cost: 9   maxlim: 5   bits: 4/3
c ---[ 745]---> Adder-cost: 9   maxlim: 5   bits: 4/3
c ---[ 744]---> Adder-cost: 9   maxlim: 5   bits: 4/3
c ---[ 743]---> Adder-cost: 8   maxlim: 4   bits: 4/3
c ---[ 742]---> Adder-cost: 8   maxlim: 4   bits: 4/3
c ---[ 741]---> Adder-cost: 8   maxlim: 4   bits: 4/3
c ---[ 740]---> Adder-cost: 8   maxlim: 4   bits: 4/3
c ---[ 739]---> Adder-cost: 8   maxlim: 4   bits: 4/3
c ---[ 738]---> Adder-cost: 8   maxlim: 4   bits: 4/3
c ---[ 737]---> Adder-cost: 8   maxlim: 4   bits: 4/3
c ---[ 736]---> Adder-cost: 8   maxlim: 4   bits: 4/3
c ---[ 735]---> Adder-cost: 2   maxlim: 3   bits: 3/2
c ---[ 734]---> Adder-cost: 2   maxlim: 3   bits: 3/2
c ---[ 733]---> Adder-cost: 2   maxlim: 3   bits: 3/2
c ---[ 732]---> Adder-cost: 2   maxlim: 3   bits: 3/2
c ---[ 731]---> Adder-cost: 2   maxlim: 3   bits: 3/2
c ---[ 730]---> Adder-cost: 2   maxlim: 3   bits: 3/2
c ---[ 729]---> Adder-cost: 2   maxlim: 3   bits: 3/2
c ---[ 728]---> Adder-cost: 2   maxlim: 3   bits: 3/2
c ---[ 727]---> Adder-cost: 7   maxlim: 2   bits: 3/2
c ---[ 726]---> Adder-cost: 7   maxlim: 2   bits: 3/2
c ---[ 725]---> Adder-cost: 7   maxlim: 2   bits: 3/2
c ---[ 724]---> Adder-cost: 7   maxlim: 2   bits: 3/2
c ---[ 723]---> Adder-cost: 7   maxlim: 2   bits: 3/2
c ---[ 722]---> Adder-cost: 7   maxlim: 2   bits: 3/2
c ---[ 721]---> Adder-cost: 7   maxlim: 2   bits: 3/2
c ---[ 720]---> Adder-cost: 7   maxlim: 2   bits: 3/2
c ---[ 719]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 718]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 717]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 716]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 715]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 714]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 713]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 712]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 703]---> Adder-cost: 2   maxlim: 7   bits: 4/3
c ---[ 702]---> Adder-cost: 2   maxlim: 7   bits: 4/3
c ---[ 701]---> Adder-cost: 2   maxlim: 7   bits: 4/3
c ---[ 700]---> Adder-cost: 2   maxlim: 7   bits: 4/3
c ---[ 699]---> Adder-cost: 2   maxlim: 7   bits: 4/3
c ---[ 698]---> Adder-cost: 2   maxlim: 7   bits: 4/3
c ---[ 697]---> Adder-cost: 2   maxlim: 7   bits: 4/3
c ---[ 696]---> Adder-cost: 2   maxlim: 7   bits: 4/3
c ---[ 695]---> Adder-cost: 15   maxlim: 6   bits: 4/3
c ---[ 694]---> Adder-cost: 15   maxlim: 6   bits: 4/3
c ---[ 693]---> Adder-cost: 15   maxlim: 6   bits: 4/3
c ---[ 692]---> Adder-cost: 15   maxlim: 6   bits: 4/3
c ---[ 691]---> Adder-cost: 15   maxlim: 6   bits: 4/3
c ---[ 690]---> Adder-cost: 15   maxlim: 6   bits: 4/3
c ---[ 689]---> Adder-cost: 15   maxlim: 6   bits: 4/3
c ---[ 688]---> Adder-cost: 15   maxlim: 6   bits: 4/3
c ---[ 687]---> Adder-cost: 9   maxlim: 5   bits: 4/3
c ---[ 686]---> Adder-cost: 9   maxlim: 5   bits: 4/3
c ---[ 685]---> Adder-cost: 9   maxlim: 5   bits: 4/3
c ---[ 684]---> Adder-cost: 9   maxlim: 5   bits: 4/3
c ---[ 683]---> Adder-cost: 9   maxlim: 5   bits: 4/3
c ---[ 682]---> Adder-cost: 9   maxlim: 5   bits: 4/3
c ---[ 681]---> Adder-cost: 9   maxlim: 5   bits: 4/3
c ---[ 680]---> Adder-cost: 9   maxlim: 5   bits: 4/3
c ---[ 679]---> Adder-cost: 8   maxlim: 4   bits: 4/3
c ---[ 678]---> Adder-cost: 8   maxlim: 4   bits: 4/3
c ---[ 677]---> Adder-cost: 8   maxlim: 4   bits: 4/3
c ---[ 676]---> Adder-cost: 8   maxlim: 4   bits: 4/3
c ---[ 675]---> Adder-cost: 8   maxlim: 4   bits: 4/3
c ---[ 674]---> Adder-cost: 8   maxlim: 4   bits: 4/3
c ---[ 673]---> Adder-cost: 8   maxlim: 4   bits: 4/3
c ---[ 672]---> Adder-cost: 8   maxlim: 4   bits: 4/3
c ---[ 671]---> Adder-cost: 2   maxlim: 3   bits: 3/2
c ---[ 670]---> Adder-cost: 2   maxlim: 3   bits: 3/2
c ---[ 669]---> Adder-cost: 2   maxlim: 3   bits: 3/2
c ---[ 668]---> Adder-cost: 2   maxlim: 3   bits: 3/2
c ---[ 667]---> Adder-cost: 2   maxlim: 3   bits: 3/2
c ---[ 666]---> Adder-cost: 2   maxlim: 3   bits: 3/2
c ---[ 665]---> Adder-cost: 2   maxlim: 3   bits: 3/2
c ---[ 664]---> Adder-cost: 2   maxlim: 3   bits: 3/2
c ---[ 663]---> Adder-cost: 7   maxlim: 2   bits: 3/2
c ---[ 662]---> Adder-cost: 7   maxlim: 2   bits: 3/2
c ---[ 661]---> Adder-cost: 7   maxlim: 2   bits: 3/2
c ---[ 660]---> Adder-cost: 7   maxlim: 2   bits: 3/2
c ---[ 659]---> Adder-cost: 7   maxlim: 2   bits: 3/2
c ---[ 658]---> Adder-cost: 7   maxlim: 2   bits: 3/2
c ---[ 657]---> Adder-cost: 7   maxlim: 2   bits: 3/2
c ---[ 656]---> Adder-cost: 7   maxlim: 2   bits: 3/2
c ---[ 655]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 654]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 653]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 652]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 651]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 650]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 649]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 648]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 639]---> Adder-cost: 16   maxlim: 7   bits: 4/3
c ---[ 638]---> Adder-cost: 2   maxlim: 7   bits: 4/3
c ---[ 637]---> Adder-cost: 12   maxlim: 7   bits: 4/3
c ---[ 636]---> Adder-cost: 2   maxlim: 7   bits: 4/3
c ---[ 635]---> Adder-cost: 12   maxlim: 7   bits: 4/3
c ---[ 634]---> Adder-cost: 2   maxlim: 7   bits: 4/3
c ---[ 633]---> Adder-cost: 16   maxlim: 7   bits: 4/3
c ---[ 632]---> Adder-cost: 2   maxlim: 7   bits: 4/3
c ---[ 631]---> Adder-cost: 15   maxlim: 6   bits: 4/3
c ---[ 630]---> Adder-cost: 15   maxlim: 6   bits: 4/3
c ---[ 629]---> Adder-cost: 15   maxlim: 6   bits: 4/3
c ---[ 628]---> Adder-cost: 15   maxlim: 6   bits: 4/3
c ---[ 627]---> Adder-cost: 15   maxlim: 6   bits: 4/3
c ---[ 626]---> Adder-cost: 15   maxlim: 6   bits: 4/3
c ---[ 625]---> Adder-cost: 15   maxlim: 6   bits: 4/3
c ---[ 624]---> Adder-cost: 15   maxlim: 6   bits: 4/3
c ---[ 623]---> Adder-cost: 15   maxlim: 5   bits: 4/3
c ---[ 622]---> Adder-cost: 9   maxlim: 5   bits: 4/3
c ---[ 621]---> Adder-cost: 11   maxlim: 5   bits: 4/3
c ---[ 620]---> Adder-cost: 9   maxlim: 5   bits: 4/3
c ---[ 619]---> Adder-cost: 13   maxlim: 5   bits: 4/3
c ---[ 618]---> Adder-cost: 9   maxlim: 5   bits: 4/3
c ---[ 617]---> Adder-cost: 15   maxlim: 5   bits: 4/3
c ---[ 616]---> Adder-cost: 9   maxlim: 5   bits: 4/3
c ---[ 615]---> Adder-cost: 8   maxlim: 4   bits: 4/3
c ---[ 614]---> Adder-cost: 8   maxlim: 4   bits: 4/3
c ---[ 613]---> Adder-cost: 8   maxlim: 4   bits: 4/3
c ---[ 612]---> Adder-cost: 8   maxlim: 4   bits: 4/3
c ---[ 611]---> Adder-cost: 8   maxlim: 4   bits: 4/3
c ---[ 610]---> Adder-cost: 8   maxlim: 4   bits: 4/3
c ---[ 609]---> Adder-cost: 8   maxlim: 4   bits: 4/3
c ---[ 608]---> Adder-cost: 8   maxlim: 4   bits: 4/3
c ---[ 607]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[ 606]---> Adder-cost: 2   maxlim: 3   bits: 3/2
c ---[ 605]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[ 604]---> Adder-cost: 2   maxlim: 3   bits: 3/2
c ---[ 603]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[ 602]---> Adder-cost: 2   maxlim: 3   bits: 3/2
c ---[ 601]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[ 600]---> Adder-cost: 2   maxlim: 3   bits: 3/2
c ---[ 599]---> Adder-cost: 7   maxlim: 2   bits: 3/2
c ---[ 598]---> Adder-cost: 7   maxlim: 2   bits: 3/2
c ---[ 597]---> Adder-cost: 7   maxlim: 2   bits: 3/2
c ---[ 596]---> Adder-cost: 7   maxlim: 2   bits: 3/2
c ---[ 595]---> Adder-cost: 7   maxlim: 2   bits: 3/2
c ---[ 594]---> Adder-cost: 7   maxlim: 2   bits: 3/2
c ---[ 593]---> Adder-cost: 7   maxlim: 2   bits: 3/2
c ---[ 592]---> Adder-cost: 7   maxlim: 2   bits: 3/2
c ---[ 591]---> Adder-cost: 4   maxlim: 1   bits: 2/1
c ---[ 590]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 589]---> Adder-cost: 4   maxlim: 1   bits: 2/1
c ---[ 588]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 587]---> Adder-cost: 4   maxlim: 1   bits: 2/1
c ---[ 586]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 585]---> Adder-cost: 4   maxlim: 1   bits: 2/1
c ---[ 584]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 575]---> Adder-cost: 12   maxlim: 7   bits: 4/3
c ---[ 574]---> Adder-cost: 2   maxlim: 7   bits: 4/3
c ---[ 573]---> Adder-cost: 2   maxlim: 7   bits: 4/3
c ---[ 572]---> Adder-cost: 2   maxlim: 7   bits: 4/3
c ---[ 571]---> Adder-cost: 2   maxlim: 7   bits: 4/3
c ---[ 570]---> Adder-cost: 2   maxlim: 7   bits: 4/3
c ---[ 569]---> Adder-cost: 2   maxlim: 7   bits: 4/3
c ---[ 568]---> Adder-cost: 2   maxlim: 7   bits: 4/3
c ---[ 567]---> Adder-cost: 15   maxlim: 6   bits: 4/3
c ---[ 566]---> Adder-cost: 15   maxlim: 6   bits: 4/3
c ---[ 565]---> Adder-cost: 15   maxlim: 6   bits: 4/3
c ---[ 564]---> Adder-cost: 15   maxlim: 6   bits: 4/3
c ---[ 563]---> Adder-cost: 15   maxlim: 6   bits: 4/3
c ---[ 562]---> Adder-cost: 15   maxlim: 6   bits: 4/3
c ---[ 561]---> Adder-cost: 15   maxlim: 6   bits: 4/3
c ---[ 560]---> Adder-cost: 15   maxlim: 6   bits: 4/3
c ---[ 559]---> Adder-cost: 13   maxlim: 5   bits: 4/3
c ---[ 558]---> Adder-cost: 9   maxlim: 5   bits: 4/3
c ---[ 557]---> Adder-cost: 9   maxlim: 5   bits: 4/3
c ---[ 556]---> Adder-cost: 9   maxlim: 5   bits: 4/3
c ---[ 555]---> Adder-cost: 9   maxlim: 5   bits: 4/3
c ---[ 554]---> Adder-cost: 9   maxlim: 5   bits: 4/3
c ---[ 553]---> Adder-cost: 9   maxlim: 5   bits: 4/3
c ---[ 552]---> Adder-cost: 9   maxlim: 5   bits: 4/3
c ---[ 551]---> Adder-cost: 8   maxlim: 4   bits: 4/3
c ---[ 550]---> Adder-cost: 8   maxlim: 4   bits: 4/3
c ---[ 549]---> Adder-cost: 8   maxlim: 4   bits: 4/3
c ---[ 548]---> Adder-cost: 8   maxlim: 4   bits: 4/3
c ---[ 547]---> Adder-cost: 8   maxlim: 4   bits: 4/3
c ---[ 546]---> Adder-cost: 8   maxlim: 4   bits: 4/3
c ---[ 545]---> Adder-cost: 8   maxlim: 4   bits: 4/3
c ---[ 544]---> Adder-cost: 8   maxlim: 4   bits: 4/3
c ---[ 543]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[ 542]---> Adder-cost: 2   maxlim: 3   bits: 3/2
c ---[ 541]---> Adder-cost: 2   maxlim: 3   bits: 3/2
c ---[ 540]---> Adder-cost: 2   maxlim: 3   bits: 3/2
c ---[ 539]---> Adder-cost: 2   maxlim: 3   bits: 3/2
c ---[ 538]---> Adder-cost: 2   maxlim: 3   bits: 3/2
c ---[ 537]---> Adder-cost: 2   maxlim: 3   bits: 3/2
c ---[ 536]---> Adder-cost: 2   maxlim: 3   bits: 3/2
c ---[ 535]---> Adder-cost: 7   maxlim: 2   bits: 3/2
c ---[ 534]---> Adder-cost: 7   maxlim: 2   bits: 3/2
c ---[ 533]---> Adder-cost: 7   maxlim: 2   bits: 3/2
c ---[ 532]---> Adder-cost: 7   maxlim: 2   bits: 3/2
c ---[ 531]---> Adder-cost: 7   maxlim: 2   bits: 3/2
c ---[ 530]---> Adder-cost: 7   maxlim: 2   bits: 3/2
c ---[ 529]---> Adder-cost: 7   maxlim: 2   bits: 3/2
c ---[ 528]---> Adder-cost: 7   maxlim: 2   bits: 3/2
c ---[ 527]---> Adder-cost: 4   maxlim: 1   bits: 2/1
c ---[ 526]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 525]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 524]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 523]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 522]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 521]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 520]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 511]---> Adder-cost: 2   maxlim: 7   bits: 4/3
c ---[ 510]---> Adder-cost: 2   maxlim: 7   bits: 4/3
c ---[ 509]---> Adder-cost: 2   maxlim: 7   bits: 4/3
c ---[ 508]---> Adder-cost: 2   maxlim: 7   bits: 4/3
c ---[ 507]---> Adder-cost: 2   maxlim: 7   bits: 4/3
c ---[ 506]---> Adder-cost: 2   maxlim: 7   bits: 4/3
c ---[ 505]---> Adder-cost: 2   maxlim: 7   bits: 4/3
c ---[ 504]---> Adder-cost: 2   maxlim: 7   bits: 4/3
c ---[ 503]---> Adder-cost: 15   maxlim: 6   bits: 4/3
c ---[ 502]---> Adder-cost: 15   maxlim: 6   bits: 4/3
c ---[ 501]---> Adder-cost: 15   maxlim: 6   bits: 4/3
c ---[ 500]---> Adder-cost: 15   maxlim: 6   bits: 4/3
c ---[ 499]---> Adder-cost: 15   maxlim: 6   bits: 4/3
c ---[ 498]---> Adder-cost: 15   maxlim: 6   bits: 4/3
c ---[ 497]---> Adder-cost: 15   maxlim: 6   bits: 4/3
c ---[ 496]---> Adder-cost: 15   maxlim: 6   bits: 4/3
c ---[ 495]---> Adder-cost: 9   maxlim: 5   bits: 4/3
c ---[ 494]---> Adder-cost: 9   maxlim: 5   bits: 4/3
c ---[ 493]---> Adder-cost: 9   maxlim: 5   bits: 4/3
c ---[ 492]---> Adder-cost: 9   maxlim: 5   bits: 4/3
c ---[ 491]---> Adder-cost: 9   maxlim: 5   bits: 4/3
c ---[ 490]---> Adder-cost: 9   maxlim: 5   bits: 4/3
c ---[ 489]---> Adder-cost: 9   maxlim: 5   bits: 4/3
c ---[ 488]---> Adder-cost: 9   maxlim: 5   bits: 4/3
c ---[ 487]---> Adder-cost: 8   maxlim: 4   bits: 4/3
c ---[ 486]---> Adder-cost: 8   maxlim: 4   bits: 4/3
c ---[ 485]---> Adder-cost: 8   maxlim: 4   bits: 4/3
c ---[ 484]---> Adder-cost: 8   maxlim: 4   bits: 4/3
c ---[ 483]---> Adder-cost: 8   maxlim: 4   bits: 4/3
c ---[ 482]---> Adder-cost: 8   maxlim: 4   bits: 4/3
c ---[ 481]---> Adder-cost: 8   maxlim: 4   bits: 4/3
c ---[ 480]---> Adder-cost: 8   maxlim: 4   bits: 4/3
c ---[ 479]---> Adder-cost: 2   maxlim: 3   bits: 3/2
c ---[ 478]---> Adder-cost: 2   maxlim: 3   bits: 3/2
c ---[ 477]---> Adder-cost: 2   maxlim: 3   bits: 3/2
c ---[ 476]---> Adder-cost: 2   maxlim: 3   bits: 3/2
c ---[ 475]---> Adder-cost: 2   maxlim: 3   bits: 3/2
c ---[ 474]---> Adder-cost: 2   maxlim: 3   bits: 3/2
c ---[ 473]---> Adder-cost: 2   maxlim: 3   bits: 3/2
c ---[ 472]---> Adder-cost: 2   maxlim: 3   bits: 3/2
c ---[ 471]---> Adder-cost: 7   maxlim: 2   bits: 3/2
c ---[ 470]---> Adder-cost: 7   maxlim: 2   bits: 3/2
c ---[ 469]---> Adder-cost: 7   maxlim: 2   bits: 3/2
c ---[ 468]---> Adder-cost: 7   maxlim: 2   bits: 3/2
c ---[ 467]---> Adder-cost: 7   maxlim: 2   bits: 3/2
c ---[ 466]---> Adder-cost: 7   maxlim: 2   bits: 3/2
c ---[ 465]---> Adder-cost: 7   maxlim: 2   bits: 3/2
c ---[ 464]---> Adder-cost: 7   maxlim: 2   bits: 3/2
c ---[ 463]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 462]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 461]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 460]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 459]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 458]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 457]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 456]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 447]---> Adder-cost: 2   maxlim: 7   bits: 4/3
c ---[ 446]---> Adder-cost: 2   maxlim: 7   bits: 4/3
c ---[ 445]---> Adder-cost: 2   maxlim: 7   bits: 4/3
c ---[ 444]---> Adder-cost: 2   maxlim: 7   bits: 4/3
c ---[ 443]---> Adder-cost: 2   maxlim: 7   bits: 4/3
c ---[ 442]---> Adder-cost: 2   maxlim: 7   bits: 4/3
c ---[ 441]---> Adder-cost: 2   maxlim: 7   bits: 4/3
c ---[ 440]---> Adder-cost: 2   maxlim: 7   bits: 4/3
c ---[ 439]---> Adder-cost: 15   maxlim: 6   bits: 4/3
c ---[ 438]---> Adder-cost: 15   maxlim: 6   bits: 4/3
c ---[ 437]---> Adder-cost: 15   maxlim: 6   bits: 4/3
c ---[ 436]---> Adder-cost: 15   maxlim: 6   bits: 4/3
c ---[ 435]---> Adder-cost: 15   maxlim: 6   bits: 4/3
c ---[ 434]---> Adder-cost: 15   maxlim: 6   bits: 4/3
c ---[ 433]---> Adder-cost: 15   maxlim: 6   bits: 4/3
c ---[ 432]---> Adder-cost: 15   maxlim: 6   bits: 4/3
c ---[ 431]---> Adder-cost: 9   maxlim: 5   bits: 4/3
c ---[ 430]---> Adder-cost: 9   maxlim: 5   bits: 4/3
c ---[ 429]---> Adder-cost: 9   maxlim: 5   bits: 4/3
c ---[ 428]---> Adder-cost: 9   maxlim: 5   bits: 4/3
c ---[ 427]---> Adder-cost: 9   maxlim: 5   bits: 4/3
c ---[ 426]---> Adder-cost: 9   maxlim: 5   bits: 4/3
c ---[ 425]---> Adder-cost: 9   maxlim: 5   bits: 4/3
c ---[ 424]---> Adder-cost: 9   maxlim: 5   bits: 4/3
c ---[ 423]---> Adder-cost: 8   maxlim: 4   bits: 4/3
c ---[ 422]---> Adder-cost: 8   maxlim: 4   bits: 4/3
c ---[ 421]---> Adder-cost: 8   maxlim: 4   bits: 4/3
c ---[ 420]---> Adder-cost: 8   maxlim: 4   bits: 4/3
c ---[ 419]---> Adder-cost: 8   maxlim: 4   bits: 4/3
c ---[ 418]---> Adder-cost: 8   maxlim: 4   bits: 4/3
c ---[ 417]---> Adder-cost: 8   maxlim: 4   bits: 4/3
c ---[ 416]---> Adder-cost: 8   maxlim: 4   bits: 4/3
c ---[ 415]---> Adder-cost: 2   maxlim: 3   bits: 3/2
c ---[ 414]---> Adder-cost: 2   maxlim: 3   bits: 3/2
c ---[ 413]---> Adder-cost: 2   maxlim: 3   bits: 3/2
c ---[ 412]---> Adder-cost: 2   maxlim: 3   bits: 3/2
c ---[ 411]---> Adder-cost: 2   maxlim: 3   bits: 3/2
c ---[ 410]---> Adder-cost: 2   maxlim: 3   bits: 3/2
c ---[ 409]---> Adder-cost: 2   maxlim: 3   bits: 3/2
c ---[ 408]---> Adder-cost: 2   maxlim: 3   bits: 3/2
c ---[ 407]---> Adder-cost: 7   maxlim: 2   bits: 3/2
c ---[ 406]---> Adder-cost: 7   maxlim: 2   bits: 3/2
c ---[ 405]---> Adder-cost: 7   maxlim: 2   bits: 3/2
c ---[ 404]---> Adder-cost: 7   maxlim: 2   bits: 3/2
c ---[ 403]---> Adder-cost: 7   maxlim: 2   bits: 3/2
c ---[ 402]---> Adder-cost: 7   maxlim: 2   bits: 3/2
c ---[ 401]---> Adder-cost: 7   maxlim: 2   bits: 3/2
c ---[ 400]---> Adder-cost: 7   maxlim: 2   bits: 3/2
c ---[ 399]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 398]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 397]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 396]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 395]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 394]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 393]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 392]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 383]---> Adder-cost: 2   maxlim: 7   bits: 4/3
c ---[ 382]---> Adder-cost: 2   maxlim: 7   bits: 4/3
c ---[ 381]---> Adder-cost: 2   maxlim: 7   bits: 4/3
c ---[ 380]---> Adder-cost: 2   maxlim: 7   bits: 4/3
c ---[ 379]---> Adder-cost: 2   maxlim: 7   bits: 4/3
c ---[ 378]---> Adder-cost: 2   maxlim: 7   bits: 4/3
c ---[ 377]---> Adder-cost: 2   maxlim: 7   bits: 4/3
c ---[ 376]---> Adder-cost: 2   maxlim: 7   bits: 4/3
c ---[ 375]---> Adder-cost: 15   maxlim: 6   bits: 4/3
c ---[ 374]---> Adder-cost: 15   maxlim: 6   bits: 4/3
c ---[ 373]---> Adder-cost: 15   maxlim: 6   bits: 4/3
c ---[ 372]---> Adder-cost: 15   maxlim: 6   bits: 4/3
c ---[ 371]---> Adder-cost: 15   maxlim: 6   bits: 4/3
c ---[ 370]---> Adder-cost: 15   maxlim: 6   bits: 4/3
c ---[ 369]---> Adder-cost: 15   maxlim: 6   bits: 4/3
c ---[ 368]---> Adder-cost: 15   maxlim: 6   bits: 4/3
c ---[ 367]---> Adder-cost: 9   maxlim: 5   bits: 4/3
c ---[ 366]---> Adder-cost: 9   maxlim: 5   bits: 4/3
c ---[ 365]---> Adder-cost: 9   maxlim: 5   bits: 4/3
c ---[ 364]---> Adder-cost: 9   maxlim: 5   bits: 4/3
c ---[ 363]---> Adder-cost: 9   maxlim: 5   bits: 4/3
c ---[ 362]---> Adder-cost: 9   maxlim: 5   bits: 4/3
c ---[ 361]---> Adder-cost: 9   maxlim: 5   bits: 4/3
c ---[ 360]---> Adder-cost: 9   maxlim: 5   bits: 4/3
c ---[ 359]---> Adder-cost: 8   maxlim: 4   bits: 4/3
c ---[ 358]---> Adder-cost: 8   maxlim: 4   bits: 4/3
c ---[ 357]---> Adder-cost: 8   maxlim: 4   bits: 4/3
c ---[ 356]---> Adder-cost: 8   maxlim: 4   bits: 4/3
c ---[ 355]---> Adder-cost: 8   maxlim: 4   bits: 4/3
c ---[ 354]---> Adder-cost: 8   maxlim: 4   bits: 4/3
c ---[ 353]---> Adder-cost: 8   maxlim: 4   bits: 4/3
c ---[ 352]---> Adder-cost: 8   maxlim: 4   bits: 4/3
c ---[ 351]---> Adder-cost: 2   maxlim: 3   bits: 3/2
c ---[ 350]---> Adder-cost: 2   maxlim: 3   bits: 3/2
c ---[ 349]---> Adder-cost: 2   maxlim: 3   bits: 3/2
c ---[ 348]---> Adder-cost: 2   maxlim: 3   bits: 3/2
c ---[ 347]---> Adder-cost: 2   maxlim: 3   bits: 3/2
c ---[ 346]---> Adder-cost: 2   maxlim: 3   bits: 3/2
c ---[ 345]---> Adder-cost: 2   maxlim: 3   bits: 3/2
c ---[ 344]---> Adder-cost: 2   maxlim: 3   bits: 3/2
c ---[ 343]---> Adder-cost: 7   maxlim: 2   bits: 3/2
c ---[ 342]---> Adder-cost: 7   maxlim: 2   bits: 3/2
c ---[ 341]---> Adder-cost: 7   maxlim: 2   bits: 3/2
c ---[ 340]---> Adder-cost: 7   maxlim: 2   bits: 3/2
c ---[ 339]---> Adder-cost: 7   maxlim: 2   bits: 3/2
c ---[ 338]---> Adder-cost: 7   maxlim: 2   bits: 3/2
c ---[ 337]---> Adder-cost: 7   maxlim: 2   bits: 3/2
c ---[ 336]---> Adder-cost: 7   maxlim: 2   bits: 3/2
c ---[ 335]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 334]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 333]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 332]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 331]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 330]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 329]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 328]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 319]---> Adder-cost: 16   maxlim: 7   bits: 4/3
c ---[ 318]---> Adder-cost: 2   maxlim: 7   bits: 4/3
c ---[ 317]---> Adder-cost: 12   maxlim: 7   bits: 4/3
c ---[ 316]---> Adder-cost: 2   maxlim: 7   bits: 4/3
c ---[ 315]---> Adder-cost: 12   maxlim: 7   bits: 4/3
c ---[ 314]---> Adder-cost: 2   maxlim: 7   bits: 4/3
c ---[ 313]---> Adder-cost: 16   maxlim: 7   bits: 4/3
c ---[ 312]---> Adder-cost: 2   maxlim: 7   bits: 4/3
c ---[ 311]---> Adder-cost: 15   maxlim: 6   bits: 4/3
c ---[ 310]---> Adder-cost: 15   maxlim: 6   bits: 4/3
c ---[ 309]---> Adder-cost: 15   maxlim: 6   bits: 4/3
c ---[ 308]---> Adder-cost: 15   maxlim: 6   bits: 4/3
c ---[ 307]---> Adder-cost: 15   maxlim: 6   bits: 4/3
c ---[ 306]---> Adder-cost: 15   maxlim: 6   bits: 4/3
c ---[ 305]---> Adder-cost: 15   maxlim: 6   bits: 4/3
c ---[ 304]---> Adder-cost: 15   maxlim: 6   bits: 4/3
c ---[ 303]---> Adder-cost: 15   maxlim: 5   bits: 4/3
c ---[ 302]---> Adder-cost: 9   maxlim: 5   bits: 4/3
c ---[ 301]---> Adder-cost: 11   maxlim: 5   bits: 4/3
c ---[ 300]---> Adder-cost: 9   maxlim: 5   bits: 4/3
c ---[ 299]---> Adder-cost: 13   maxlim: 5   bits: 4/3
c ---[ 298]---> Adder-cost: 9   maxlim: 5   bits: 4/3
c ---[ 297]---> Adder-cost: 15   maxlim: 5   bits: 4/3
c ---[ 296]---> Adder-cost: 9   maxlim: 5   bits: 4/3
c ---[ 295]---> Adder-cost: 8   maxlim: 4   bits: 4/3
c ---[ 294]---> Adder-cost: 8   maxlim: 4   bits: 4/3
c ---[ 293]---> Adder-cost: 8   maxlim: 4   bits: 4/3
c ---[ 292]---> Adder-cost: 8   maxlim: 4   bits: 4/3
c ---[ 291]---> Adder-cost: 8   maxlim: 4   bits: 4/3
c ---[ 290]---> Adder-cost: 8   maxlim: 4   bits: 4/3
c ---[ 289]---> Adder-cost: 8   maxlim: 4   bits: 4/3
c ---[ 288]---> Adder-cost: 8   maxlim: 4   bits: 4/3
c ---[ 287]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[ 286]---> Adder-cost: 2   maxlim: 3   bits: 3/2
c ---[ 285]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[ 284]---> Adder-cost: 2   maxlim: 3   bits: 3/2
c ---[ 283]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[ 282]---> Adder-cost: 2   maxlim: 3   bits: 3/2
c ---[ 281]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[ 280]---> Adder-cost: 2   maxlim: 3   bits: 3/2
c ---[ 279]---> Adder-cost: 7   maxlim: 2   bits: 3/2
c ---[ 278]---> Adder-cost: 7   maxlim: 2   bits: 3/2
c ---[ 277]---> Adder-cost: 7   maxlim: 2   bits: 3/2
c ---[ 276]---> Adder-cost: 7   maxlim: 2   bits: 3/2
c ---[ 275]---> Adder-cost: 7   maxlim: 2   bits: 3/2
c ---[ 274]---> Adder-cost: 7   maxlim: 2   bits: 3/2
c ---[ 273]---> Adder-cost: 7   maxlim: 2   bits: 3/2
c ---[ 272]---> Adder-cost: 7   maxlim: 2   bits: 3/2
c ---[ 271]---> Adder-cost: 4   maxlim: 1   bits: 2/1
c ---[ 270]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 269]---> Adder-cost: 4   maxlim: 1   bits: 2/1
c ---[ 268]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 267]---> Adder-cost: 4   maxlim: 1   bits: 2/1
c ---[ 266]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 265]---> Adder-cost: 4   maxlim: 1   bits: 2/1
c ---[ 264]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 255]---> Adder-cost: 12   maxlim: 7   bits: 4/3
c ---[ 254]---> Adder-cost: 2   maxlim: 7   bits: 4/3
c ---[ 253]---> Adder-cost: 2   maxlim: 7   bits: 4/3
c ---[ 252]---> Adder-cost: 2   maxlim: 7   bits: 4/3
c ---[ 251]---> Adder-cost: 2   maxlim: 7   bits: 4/3
c ---[ 250]---> Adder-cost: 2   maxlim: 7   bits: 4/3
c ---[ 249]---> Adder-cost: 2   maxlim: 7   bits: 4/3
c ---[ 248]---> Adder-cost: 2   maxlim: 7   bits: 4/3
c ---[ 247]---> Adder-cost: 15   maxlim: 6   bits: 4/3
c ---[ 246]---> Adder-cost: 15   maxlim: 6   bits: 4/3
c ---[ 245]---> Adder-cost: 15   maxlim: 6   bits: 4/3
c ---[ 244]---> Adder-cost: 15   maxlim: 6   bits: 4/3
c ---[ 243]---> Adder-cost: 15   maxlim: 6   bits: 4/3
c ---[ 242]---> Adder-cost: 15   maxlim: 6   bits: 4/3
c ---[ 241]---> Adder-cost: 15   maxlim: 6   bits: 4/3
c ---[ 240]---> Adder-cost: 15   maxlim: 6   bits: 4/3
c ---[ 239]---> Adder-cost: 13   maxlim: 5   bits: 4/3
c ---[ 238]---> Adder-cost: 9   maxlim: 5   bits: 4/3
c ---[ 237]---> Adder-cost: 9   maxlim: 5   bits: 4/3
c ---[ 236]---> Adder-cost: 9   maxlim: 5   bits: 4/3
c ---[ 235]---> Adder-cost: 9   maxlim: 5   bits: 4/3
c ---[ 234]---> Adder-cost: 9   maxlim: 5   bits: 4/3
c ---[ 233]---> Adder-cost: 9   maxlim: 5   bits: 4/3
c ---[ 232]---> Adder-cost: 9   maxlim: 5   bits: 4/3
c ---[ 231]---> Adder-cost: 8   maxlim: 4   bits: 4/3
c ---[ 230]---> Adder-cost: 8   maxlim: 4   bits: 4/3
c ---[ 229]---> Adder-cost: 8   maxlim: 4   bits: 4/3
c ---[ 228]---> Adder-cost: 8   maxlim: 4   bits: 4/3
c ---[ 227]---> Adder-cost: 8   maxlim: 4   bits: 4/3
c ---[ 226]---> Adder-cost: 8   maxlim: 4   bits: 4/3
c ---[ 225]---> Adder-cost: 8   maxlim: 4   bits: 4/3
c ---[ 224]---> Adder-cost: 8   maxlim: 4   bits: 4/3
c ---[ 223]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[ 222]---> Adder-cost: 2   maxlim: 3   bits: 3/2
c ---[ 221]---> Adder-cost: 2   maxlim: 3   bits: 3/2
c ---[ 220]---> Adder-cost: 2   maxlim: 3   bits: 3/2
c ---[ 219]---> Adder-cost: 2   maxlim: 3   bits: 3/2
c ---[ 218]---> Adder-cost: 2   maxlim: 3   bits: 3/2
c ---[ 217]---> Adder-cost: 2   maxlim: 3   bits: 3/2
c ---[ 216]---> Adder-cost: 2   maxlim: 3   bits: 3/2
c ---[ 215]---> Adder-cost: 7   maxlim: 2   bits: 3/2
c ---[ 214]---> Adder-cost: 7   maxlim: 2   bits: 3/2
c ---[ 213]---> Adder-cost: 7   maxlim: 2   bits: 3/2
c ---[ 212]---> Adder-cost: 7   maxlim: 2   bits: 3/2
c ---[ 211]---> Adder-cost: 7   maxlim: 2   bits: 3/2
c ---[ 210]---> Adder-cost: 7   maxlim: 2   bits: 3/2
c ---[ 209]---> Adder-cost: 7   maxlim: 2   bits: 3/2
c ---[ 208]---> Adder-cost: 7   maxlim: 2   bits: 3/2
c ---[ 207]---> Adder-cost: 4   maxlim: 1   bits: 2/1
c ---[ 206]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 205]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 204]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 203]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 202]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 201]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 200]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 191]---> Adder-cost: 2   maxlim: 7   bits: 4/3
c ---[ 190]---> Adder-cost: 2   maxlim: 7   bits: 4/3
c ---[ 189]---> Adder-cost: 2   maxlim: 7   bits: 4/3
c ---[ 188]---> Adder-cost: 2   maxlim: 7   bits: 4/3
c ---[ 187]---> Adder-cost: 2   maxlim: 7   bits: 4/3
c ---[ 186]---> Adder-cost: 2   maxlim: 7   bits: 4/3
c ---[ 185]---> Adder-cost: 2   maxlim: 7   bits: 4/3
c ---[ 184]---> Adder-cost: 2   maxlim: 7   bits: 4/3
c ---[ 183]---> Adder-cost: 15   maxlim: 6   bits: 4/3
c ---[ 182]---> Adder-cost: 15   maxlim: 6   bits: 4/3
c ---[ 181]---> Adder-cost: 15   maxlim: 6   bits: 4/3
c ---[ 180]---> Adder-cost: 15   maxlim: 6   bits: 4/3
c ---[ 179]---> Adder-cost: 15   maxlim: 6   bits: 4/3
c ---[ 178]---> Adder-cost: 15   maxlim: 6   bits: 4/3
c ---[ 177]---> Adder-cost: 15   maxlim: 6   bits: 4/3
c ---[ 176]---> Adder-cost: 15   maxlim: 6   bits: 4/3
c ---[ 175]---> Adder-cost: 9   maxlim: 5   bits: 4/3
c ---[ 174]---> Adder-cost: 9   maxlim: 5   bits: 4/3
c ---[ 173]---> Adder-cost: 9   maxlim: 5   bits: 4/3
c ---[ 172]---> Adder-cost: 9   maxlim: 5   bits: 4/3
c ---[ 171]---> Adder-cost: 9   maxlim: 5   bits: 4/3
c ---[ 170]---> Adder-cost: 9   maxlim: 5   bits: 4/3
c ---[ 169]---> Adder-cost: 9   maxlim: 5   bits: 4/3
c ---[ 168]---> Adder-cost: 9   maxlim: 5   bits: 4/3
c ---[ 167]---> Adder-cost: 8   maxlim: 4   bits: 4/3
c ---[ 166]---> Adder-cost: 8   maxlim: 4   bits: 4/3
c ---[ 165]---> Adder-cost: 8   maxlim: 4   bits: 4/3
c ---[ 164]---> Adder-cost: 8   maxlim: 4   bits: 4/3
c ---[ 163]---> Adder-cost: 8   maxlim: 4   bits: 4/3
c ---[ 162]---> Adder-cost: 8   maxlim: 4   bits: 4/3
c ---[ 161]---> Adder-cost: 8   maxlim: 4   bits: 4/3
c ---[ 160]---> Adder-cost: 8   maxlim: 4   bits: 4/3
c ---[ 159]---> Adder-cost: 2   maxlim: 3   bits: 3/2
c ---[ 158]---> Adder-cost: 2   maxlim: 3   bits: 3/2
c ---[ 157]---> Adder-cost: 2   maxlim: 3   bits: 3/2
c ---[ 156]---> Adder-cost: 2   maxlim: 3   bits: 3/2
c ---[ 155]---> Adder-cost: 2   maxlim: 3   bits: 3/2
c ---[ 154]---> Adder-cost: 2   maxlim: 3   bits: 3/2
c ---[ 153]---> Adder-cost: 2   maxlim: 3   bits: 3/2
c ---[ 152]---> Adder-cost: 2   maxlim: 3   bits: 3/2
c ---[ 151]---> Adder-cost: 7   maxlim: 2   bits: 3/2
c ---[ 150]---> Adder-cost: 7   maxlim: 2   bits: 3/2
c ---[ 149]---> Adder-cost: 7   maxlim: 2   bits: 3/2
c ---[ 148]---> Adder-cost: 7   maxlim: 2   bits: 3/2
c ---[ 147]---> Adder-cost: 7   maxlim: 2   bits: 3/2
c ---[ 146]---> Adder-cost: 7   maxlim: 2   bits: 3/2
c ---[ 145]---> Adder-cost: 7   maxlim: 2   bits: 3/2
c ---[ 144]---> Adder-cost: 7   maxlim: 2   bits: 3/2
c ---[ 143]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 142]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 141]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 140]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 139]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 138]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 137]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 136]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 127]---> Adder-cost: 2   maxlim: 7   bits: 4/3
c ---[ 126]---> Adder-cost: 2   maxlim: 7   bits: 4/3
c ---[ 125]---> Adder-cost: 2   maxlim: 7   bits: 4/3
c ---[ 124]---> Adder-cost: 2   maxlim: 7   bits: 4/3
c ---[ 123]---> Adder-cost: 2   maxlim: 7   bits: 4/3
c ---[ 122]---> Adder-cost: 2   maxlim: 7   bits: 4/3
c ---[ 121]---> Adder-cost: 2   maxlim: 7   bits: 4/3
c ---[ 120]---> Adder-cost: 2   maxlim: 7   bits: 4/3
c ---[ 119]---> Adder-cost: 15   maxlim: 6   bits: 4/3
c ---[ 118]---> Adder-cost: 15   maxlim: 6   bits: 4/3
c ---[ 117]---> Adder-cost: 15   maxlim: 6   bits: 4/3
c ---[ 116]---> Adder-cost: 15   maxlim: 6   bits: 4/3
c ---[ 115]---> Adder-cost: 15   maxlim: 6   bits: 4/3
c ---[ 114]---> Adder-cost: 15   maxlim: 6   bits: 4/3
c ---[ 113]---> Adder-cost: 15   maxlim: 6   bits: 4/3
c ---[ 112]---> Adder-cost: 15   maxlim: 6   bits: 4/3
c ---[ 111]---> Adder-cost: 9   maxlim: 5   bits: 4/3
c ---[ 110]---> Adder-cost: 9   maxlim: 5   bits: 4/3
c ---[ 109]---> Adder-cost: 9   maxlim: 5   bits: 4/3
c ---[ 108]---> Adder-cost: 9   maxlim: 5   bits: 4/3
c ---[ 107]---> Adder-cost: 9   maxlim: 5   bits: 4/3
c ---[ 106]---> Adder-cost: 9   maxlim: 5   bits: 4/3
c ---[ 105]---> Adder-cost: 9   maxlim: 5   bits: 4/3
c ---[ 104]---> Adder-cost: 9   maxlim: 5   bits: 4/3
c ---[ 103]---> Adder-cost: 8   maxlim: 4   bits: 4/3
c ---[ 102]---> Adder-cost: 8   maxlim: 4   bits: 4/3
c ---[ 101]---> Adder-cost: 8   maxlim: 4   bits: 4/3
c ---[ 100]---> Adder-cost: 8   maxlim: 4   bits: 4/3
c ---[  99]---> Adder-cost: 8   maxlim: 4   bits: 4/3
c ---[  98]---> Adder-cost: 8   maxlim: 4   bits: 4/3
c ---[  97]---> Adder-cost: 8   maxlim: 4   bits: 4/3
c ---[  96]---> Adder-cost: 8   maxlim: 4   bits: 4/3
c ---[  95]---> Adder-cost: 2   maxlim: 3   bits: 3/2
c ---[  94]---> Adder-cost: 2   maxlim: 3   bits: 3/2
c ---[  93]---> Adder-cost: 2   maxlim: 3   bits: 3/2
c ---[  92]---> Adder-cost: 2   maxlim: 3   bits: 3/2
c ---[  91]---> Adder-cost: 2   maxlim: 3   bits: 3/2
c ---[  90]---> Adder-cost: 2   maxlim: 3   bits: 3/2
c ---[  89]---> Adder-cost: 2   maxlim: 3   bits: 3/2
c ---[  88]---> Adder-cost: 2   maxlim: 3   bits: 3/2
c ---[  87]---> Adder-cost: 7   maxlim: 2   bits: 3/2
c ---[  86]---> Adder-cost: 7   maxlim: 2   bits: 3/2
c ---[  85]---> Adder-cost: 7   maxlim: 2   bits: 3/2
c ---[  84]---> Adder-cost: 7   maxlim: 2   bits: 3/2
c ---[  83]---> Adder-cost: 7   maxlim: 2   bits: 3/2
c ---[  82]---> Adder-cost: 7   maxlim: 2   bits: 3/2
c ---[  81]---> Adder-cost: 7   maxlim: 2   bits: 3/2
c ---[  80]---> Adder-cost: 7   maxlim: 2   bits: 3/2
c ---[  79]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[  78]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[  77]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[  76]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[  75]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[  74]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[  73]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[  72]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[  63]---> Adder-cost: 2   maxlim: 7   bits: 4/3
c ---[  62]---> Adder-cost: 2   maxlim: 7   bits: 4/3
c ---[  61]---> Adder-cost: 2   maxlim: 7   bits: 4/3
c ---[  60]---> Adder-cost: 2   maxlim: 7   bits: 4/3
c ---[  59]---> Adder-cost: 2   maxlim: 7   bits: 4/3
c ---[  58]---> Adder-cost: 2   maxlim: 7   bits: 4/3
c ---[  57]---> Adder-cost: 2   maxlim: 7   bits: 4/3
c ---[  56]---> Adder-cost: 2   maxlim: 7   bits: 4/3
c ---[  55]---> Adder-cost: 15   maxlim: 6   bits: 4/3
c ---[  54]---> Adder-cost: 15   maxlim: 6   bits: 4/3
c ---[  53]---> Adder-cost: 15   maxlim: 6   bits: 4/3
c ---[  52]---> Adder-cost: 15   maxlim: 6   bits: 4/3
c ---[  51]---> Adder-cost: 15   maxlim: 6   bits: 4/3
c ---[  50]---> Adder-cost: 15   maxlim: 6   bits: 4/3
c ---[  49]---> Adder-cost: 15   maxlim: 6   bits: 4/3
c ---[  48]---> Adder-cost: 15   maxlim: 6   bits: 4/3
c ---[  47]---> Adder-cost: 9   maxlim: 5   bits: 4/3
c ---[  46]---> Adder-cost: 9   maxlim: 5   bits: 4/3
c ---[  45]---> Adder-cost: 9   maxlim: 5   bits: 4/3
c ---[  44]---> Adder-cost: 9   maxlim: 5   bits: 4/3
c ---[  43]---> Adder-cost: 9   maxlim: 5   bits: 4/3
c ---[  42]---> Adder-cost: 9   maxlim: 5   bits: 4/3
c ---[  41]---> Adder-cost: 9   maxlim: 5   bits: 4/3
c ---[  40]---> Adder-cost: 9   maxlim: 5   bits: 4/3
c ---[  39]---> Adder-cost: 8   maxlim: 4   bits: 4/3
c ---[  38]---> Adder-cost: 8   maxlim: 4   bits: 4/3
c ---[  37]---> Adder-cost: 8   maxlim: 4   bits: 4/3
c ---[  36]---> Adder-cost: 8   maxlim: 4   bits: 4/3
c ---[  35]---> Adder-cost: 8   maxlim: 4   bits: 4/3
c ---[  34]---> Adder-cost: 8   maxlim: 4   bits: 4/3
c ---[  33]---> Adder-cost: 8   maxlim: 4   bits: 4/3
c ---[  32]---> Adder-cost: 8   maxlim: 4   bits: 4/3
c ---[  31]---> Adder-cost: 2   maxlim: 3   bits: 3/2
c ---[  30]---> Adder-cost: 2   maxlim: 3   bits: 3/2
c ---[  29]---> Adder-cost: 2   maxlim: 3   bits: 3/2
c ---[  28]---> Adder-cost: 2   maxlim: 3   bits: 3/2
c ---[  27]---> Adder-cost: 2   maxlim: 3   bits: 3/2
c ---[  26]---> Adder-cost: 2   maxlim: 3   bits: 3/2
c ---[  25]---> Adder-cost: 2   maxlim: 3   bits: 3/2
c ---[  24]---> Adder-cost: 2   maxlim: 3   bits: 3/2
c ---[  23]---> Adder-cost: 7   maxlim: 2   bits: 3/2
c ---[  22]---> Adder-cost: 7   maxlim: 2   bits: 3/2
c ---[  21]---> Adder-cost: 7   maxlim: 2   bits: 3/2
c ---[  20]---> Adder-cost: 7   maxlim: 2   bits: 3/2
c ---[  19]---> Adder-cost: 7   maxlim: 2   bits: 3/2
c ---[  18]---> Adder-cost: 7   maxlim: 2   bits: 3/2
c ---[  17]---> Adder-cost: 7   maxlim: 2   bits: 3/2
c ---[  16]---> Adder-cost: 7   maxlim: 2   bits: 3/2
c ---[  15]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[  14]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[  13]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[  12]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[  11]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[  10]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[   9]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[   8]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |   69174   240078 |   23058       0        0     nan |  0.000 % |
c |       100 |   68870   239007 |   25363      89      774     8.7 | 25.986 % |
c ==============================================================================
c [1mFound solution: 31045[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 1084   maxlim: 85859   bits: 17/17
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       161 |   76273   265449 |   25424     147     1235     8.4 | 25.986 % |
c ==============================================================================
c [1mFound solution: 30484[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 86420   bits: 17/17
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       227 |   76277   265510 |   25425     212     3085    14.6 | 25.986 % |
c |       327 |   76073   264815 |   27967     303     4327    14.3 | 24.629 % |
c ==============================================================================
c [1mFound solution: 30468[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 86436   bits: 17/17
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       372 |   76031   264708 |   25343     345     4793    13.9 | 24.629 % |
c |       472 |   75806   263926 |   27877     437     6019    13.8 | 24.809 % |
c |       623 |   75558   263053 |   30665     581     8688    15.0 | 24.899 % |
c |       848 |   75469   262745 |   33731     803    11475    14.3 | 24.945 % |
c |      1185 |   75048   261303 |   37104    1122    17086    15.2 | 25.171 % |
c ==============================================================================
c [1mFound solution: 29797[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 87107   bits: 17/17
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      1523 |   74715   260157 |   24905    1449    27069    18.7 | 25.171 % |
c ==============================================================================
c [1mFound solution: 29655[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 87249   bits: 17/17
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      1563 |   74719   260207 |   24906    1489    29261    19.7 | 25.171 % |
c |      1663 |   74656   259980 |   27396    1588    30372    19.1 | 25.347 % |
c |      1815 |   74527   259520 |   30136    1735    35014    20.2 | 25.381 % |
c |      2040 |   74372   259002 |   33149    1952    40724    20.9 | 25.494 % |
c ==============================================================================
c [1mFound solution: 29512[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 87392   bits: 17/17
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      2244 |   74170   258313 |   24723    2148    45096    21.0 | 25.494 % |
c ==============================================================================
c [1mFound solution: 28800[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 88104   bits: 17/17
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      2280 |   74164   258333 |   24721    2183    45584    20.9 | 25.494 % |
c |      2381 |   74076   258032 |   27193    2281    47675    20.9 | 25.637 % |
c |      2532 |   74076   258032 |   29912    2432    50259    20.7 | 25.637 % |
c |      2757 |   73788   257013 |   32903    2648    56357    21.3 | 25.711 % |
c ==============================================================================
c [1mFound solution: 28616[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 88288   bits: 17/17
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      3028 |   73618   256448 |   24539    2914    68365    23.5 | 25.711 % |
c |      3128 |   73505   256042 |   26992    3011    71749    23.8 | 25.808 % |
c |      3278 |   73178   254885 |   29692    3152    74974    23.8 | 25.899 % |
c ==============================================================================
c [1mFound solution: 27497[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 89407   bits: 17/17
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      3336 |   73183   254915 |   24394    3210    76064    23.7 | 25.899 % |
c |      3436 |   73168   254868 |   26833    3309    80168    24.2 | 25.925 % |
c |      3586 |   73152   254814 |   29516    3458    90977    26.3 | 25.942 % |
c |      3811 |   73152   254814 |   32468    3683    98897    26.9 | 25.942 % |
c |      4149 |   73122   254720 |   35715    4019   117398    29.2 | 25.976 % |
c |      4655 |   72933   254041 |   39286    4520   145202    32.1 | 26.005 % |
c ==============================================================================
c [1mFound solution: 27377[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 89527   bits: 17/17
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      5330 |   72939   254094 |   24313    5195   187927    36.2 | 26.005 % |
c |      5431 |   72939   254094 |   26744    5296   190779    36.0 | 26.018 % |
c |      5587 |   72939   254094 |   29418    5452   199386    36.6 | 26.018 % |
c |      5812 |   72924   254047 |   32360    5676   209728    36.9 | 26.035 % |
c ==============================================================================
c [1mFound solution: 26759[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 90145   bits: 17/17
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      5968 |   72818   253683 |   24272    5830   215841    37.0 | 26.035 % |
c |      6069 |   72803   253636 |   26699    5930   220270    37.1 | 26.079 % |
c |      6219 |   72803   253636 |   29369    6080   227751    37.5 | 26.079 % |
c |      6445 |   72788   253589 |   32306    6305   236235    37.5 | 26.096 % |
c |      6784 |   72788   253589 |   35536    6644   254010    38.2 | 26.096 % |
c |      7290 |   72788   253589 |   39090    7150   296757    41.5 | 26.096 % |
c |      8049 |   72657   253117 |   42999    7905   347672    44.0 | 26.113 % |
c |      9189 |   72544   252711 |   47299    9041   436087    48.2 | 26.130 % |
c ==============================================================================
c [1mFound solution: 26386[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 90518   bits: 17/17
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     10667 |   72358   252100 |   24119   10513   531669    50.6 | 26.130 % |
c |     10767 |   72358   252100 |   26530   10613   534130    50.3 | 26.194 % |
c |     10917 |   72358   252100 |   29183   10763   543369    50.5 | 26.194 % |
c |     11144 |   72358   252100 |   32102   10990   560530    51.0 | 26.194 % |
c |     11483 |   72294   251871 |   35312   11328   571086    50.4 | 26.205 % |
c |     11991 |   72294   251871 |   38843   11836   601883    50.9 | 26.205 % |
c |     12750 |   72294   251871 |   42728   12595   659835    52.4 | 26.205 % |
c |     13889 |   72294   251871 |   47001   13734   733125    53.4 | 26.205 % |
c |     15602 |   72294   251871 |   51701   15447   865695    56.0 | 26.205 % |
c |     18167 |   72294   251871 |   56871   18012  1059450    58.8 | 26.205 % |
c |     22011 |   72119   251256 |   62558   21840  1312936    60.1 | 26.268 % |
c |     27778 |   72104   251209 |   68814   27606  1759607    63.7 | 26.285 % |
c |     36428 |   71928   250596 |   75695   36249  2283761    63.0 | 26.352 % |
c |     49404 |   71851   250321 |   83265   49222  3113408    63.3 | 26.375 % |
c |     68865 |   71851   250321 |   91591   68683  4666041    67.9 | 26.375 % |
c |     98058 |   71851   250321 |  100751   19890  1305622    65.6 | 26.375 % |
c |    141847 |   71781   250070 |  110826   63678  4699774    73.8 | 26.386 % |
#### 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.91 0.95 0.90 2/54 14938
Raw data (stat): 14938 (runsolver) R 14937 11931 11930 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 479589060 1052672 99 4294967295 134512640 135381576 3221224464 3221219708 135158418 0 2147483391 7 90112 0 0 0 17 0 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0009 s]
Raw data (loadavg): 0.93 0.95 0.90 2/54 14938
Raw data (stat): 14938 (minisat+) R 14937 11931 11930 0 -1 0 2320 0 0 0 992 5 0 0 25 0 1 0 479589060 11935744 2246 4294967295 134512640 134672761 3221224560 3221223760 134557895 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2914 2246 603 41 0 2873 0
vsize: 11656
[startup+20.0013 s]
Raw data (loadavg): 0.94 0.96 0.91 2/54 14938
Raw data (stat): 14938 (minisat+) R 14937 11931 11930 0 -1 0 2506 0 0 0 1990 7 0 0 25 0 1 0 479589060 12726272 2432 4294967295 134512640 134672761 3221224560 3221223728 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3107 2432 603 41 0 3066 0
vsize: 12428
[startup+30.0015 s]
Raw data (loadavg): 0.95 0.96 0.91 2/54 14938
Raw data (stat): 14938 (minisat+) R 14937 11931 11930 0 -1 0 2732 0 0 0 2989 8 0 0 25 0 1 0 479589060 13668352 2658 4294967295 134512640 134672761 3221224560 3221223728 134561201 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3337 2658 603 41 0 3296 0
vsize: 13348
[startup+40.0021 s]
Raw data (loadavg): 0.95 0.96 0.91 2/54 14938
Raw data (stat): 14938 (minisat+) R 14937 11931 11930 0 -1 0 2927 0 0 0 3986 9 0 0 25 0 1 0 479589060 14471168 2853 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3533 2853 603 41 0 3492 0
vsize: 14132
[startup+50.0026 s]
Raw data (loadavg): 0.96 0.96 0.91 2/54 14938
Raw data (stat): 14938 (minisat+) R 14937 11931 11930 0 -1 0 3123 0 0 0 4986 10 0 0 25 0 1 0 479589060 15273984 3049 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3729 3049 603 41 0 3688 0
vsize: 14916
[startup+60.0027 s]
Raw data (loadavg): 0.97 0.96 0.91 2/54 14938
Raw data (stat): 14938 (minisat+) R 14937 11931 11930 0 -1 0 3331 0 0 0 5985 11 0 0 25 0 1 0 479589060 16236544 3257 4294967295 134512640 134672761 3221224560 3221223728 134561218 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3964 3257 603 41 0 3923 0
vsize: 15856
[startup+70.0036 s]
Raw data (loadavg): 0.97 0.96 0.91 2/54 14938
Raw data (stat): 14938 (minisat+) R 14937 11931 11930 0 -1 0 3530 0 0 0 6984 12 0 0 25 0 1 0 479589060 17047552 3456 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4162 3456 603 41 0 4121 0
vsize: 16648
[startup+80.0031 s]
Raw data (loadavg): 0.98 0.96 0.91 2/54 14938
Raw data (stat): 14938 (minisat+) R 14937 11931 11930 0 -1 0 3703 0 0 0 7983 12 0 0 25 0 1 0 479589060 17715200 3629 4294967295 134512640 134672761 3221224560 3221223728 134561220 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4325 3629 603 41 0 4284 0
vsize: 17300
[startup+90.0032 s]
Raw data (loadavg): 0.98 0.96 0.91 2/54 14938
Raw data (stat): 14938 (minisat+) R 14937 11931 11930 0 -1 0 3875 0 0 0 8983 12 0 0 25 0 1 0 479589060 18391040 3801 4294967295 134512640 134672761 3221224560 3221223728 134561154 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4490 3801 603 41 0 4449 0
vsize: 17960
[startup+100.003 s]
Raw data (loadavg): 0.98 0.96 0.91 2/54 14938
Raw data (stat): 14938 (minisat+) R 14937 11931 11930 0 -1 0 4041 0 0 0 9983 13 0 0 25 0 1 0 479589060 19062784 3967 4294967295 134512640 134672761 3221224560 3221223728 134560874 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4654 3967 603 41 0 4613 0
vsize: 18616
[startup+110.004 s]
Raw data (loadavg): 0.98 0.96 0.91 2/54 14938
Raw data (stat): 14938 (minisat+) R 14937 11931 11930 0 -1 0 4234 0 0 0 10982 14 0 0 25 0 1 0 479589060 19865600 4160 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4850 4160 603 41 0 4809 0
vsize: 19400
[startup+120.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14938
Raw data (stat): 14938 (minisat+) R 14937 11931 11930 0 -1 0 4378 0 0 0 11982 14 0 0 25 0 1 0 479589060 20402176 4304 4294967295 134512640 134672761 3221224560 3221223728 134561164 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4981 4304 603 41 0 4940 0
vsize: 19924
[startup+130.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14938
Raw data (stat): 14938 (minisat+) R 14937 11931 11930 0 -1 0 4528 0 0 0 12982 15 0 0 25 0 1 0 479589060 21073920 4454 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5145 4454 603 41 0 5104 0
vsize: 20580
[startup+140.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14938
Raw data (stat): 14938 (minisat+) R 14937 11931 11930 0 -1 0 4717 0 0 0 13981 15 0 0 25 0 1 0 479589060 21876736 4643 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5341 4643 603 41 0 5300 0
vsize: 21364
[startup+150.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14938
Raw data (stat): 14938 (minisat+) R 14937 11931 11930 0 -1 0 4845 0 0 0 14981 16 0 0 25 0 1 0 479589060 22409216 4771 4294967295 134512640 134672761 3221224560 3221223728 134560852 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5471 4771 603 41 0 5430 0
vsize: 21884
[startup+160.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14938
Raw data (stat): 14938 (minisat+) R 14937 11931 11930 0 -1 0 5002 0 0 0 15980 17 0 0 25 0 1 0 479589060 23072768 4928 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5633 4928 603 41 0 5592 0
vsize: 22532
[startup+170.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14938
Raw data (stat): 14938 (minisat+) R 14937 11931 11930 0 -1 0 5133 0 0 0 16980 17 0 0 25 0 1 0 479589060 23605248 5059 4294967295 134512640 134672761 3221224560 3221223728 134561205 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5763 5059 603 41 0 5722 0
vsize: 23052
[startup+180.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14938
Raw data (stat): 14938 (minisat+) R 14937 11931 11930 0 -1 0 5272 0 0 0 17980 17 0 0 25 0 1 0 479589060 24137728 5198 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5893 5198 603 41 0 5852 0
vsize: 23572
[startup+190.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14938
Raw data (stat): 14938 (minisat+) R 14937 11931 11930 0 -1 0 5412 0 0 0 18980 18 0 0 25 0 1 0 479589060 24670208 5338 4294967295 134512640 134672761 3221224560 3221223760 134557809 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6023 5338 603 41 0 5982 0
vsize: 24092
[startup+200.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14938
Raw data (stat): 14938 (minisat+) R 14937 11931 11930 0 -1 0 5558 0 0 0 19979 18 0 0 25 0 1 0 479589060 25329664 5484 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6184 5484 603 41 0 6143 0
vsize: 24736
[startup+210.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14938
Raw data (stat): 14938 (minisat+) R 14937 11931 11930 0 -1 0 5696 0 0 0 20979 19 0 0 25 0 1 0 479589060 25870336 5622 4294967295 134512640 134672761 3221224560 3221223708 134560552 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6316 5622 603 41 0 6275 0
vsize: 25264
[startup+220.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14938
Raw data (stat): 14938 (minisat+) R 14937 11931 11930 0 -1 0 5845 0 0 0 21979 19 0 0 25 0 1 0 479589060 26542080 5771 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6480 5771 603 41 0 6439 0
vsize: 25920
[startup+230.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14938
Raw data (stat): 14938 (minisat+) R 14937 11931 11930 0 -1 0 5985 0 0 0 22978 20 0 0 25 0 1 0 479589060 27082752 5911 4294967295 134512640 134672761 3221224560 3221223728 134561190 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6612 5911 603 41 0 6571 0
vsize: 26448
[startup+240.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14938
Raw data (stat): 14938 (minisat+) R 14937 11931 11930 0 -1 0 6126 0 0 0 23978 20 0 0 25 0 1 0 479589060 27615232 6052 4294967295 134512640 134672761 3221224560 3221223728 134560903 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6742 6052 603 41 0 6701 0
vsize: 26968
[startup+250.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14938
Raw data (stat): 14938 (minisat+) R 14937 11931 11930 0 -1 0 6250 0 0 0 24978 21 0 0 25 0 1 0 479589060 28147712 6176 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6872 6176 603 41 0 6831 0
vsize: 27488
[startup+260.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14938
Raw data (stat): 14938 (minisat+) R 14937 11931 11930 0 -1 0 6383 0 0 0 25978 21 0 0 25 0 1 0 479589060 28684288 6309 4294967295 134512640 134672761 3221224560 3221223728 134560920 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7003 6309 603 41 0 6962 0
vsize: 28012
[startup+270.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14938
Raw data (stat): 14938 (minisat+) R 14937 11931 11930 0 -1 0 6508 0 0 0 26977 22 0 0 25 0 1 0 479589060 29220864 6434 4294967295 134512640 134672761 3221224560 3221223728 134560892 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7134 6434 603 41 0 7093 0
vsize: 28536
[startup+280.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14938
Raw data (stat): 14938 (minisat+) R 14937 11931 11930 0 -1 0 6644 0 0 0 27977 22 0 0 25 0 1 0 479589060 29749248 6570 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7263 6570 603 41 0 7222 0
vsize: 29052
[startup+290.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14938
Raw data (stat): 14938 (minisat+) R 14937 11931 11930 0 -1 0 6790 0 0 0 28977 22 0 0 25 0 1 0 479589060 30281728 6716 4294967295 134512640 134672761 3221224560 3221223728 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7393 6716 603 41 0 7352 0
vsize: 29572
[startup+300.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14938
Raw data (stat): 14938 (minisat+) R 14937 11931 11930 0 -1 0 6936 0 0 0 29977 23 0 0 25 0 1 0 479589060 30953472 6862 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7557 6862 603 41 0 7516 0
vsize: 30228
[startup+310.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14938
Raw data (stat): 14938 (minisat+) R 14937 11931 11930 0 -1 0 7080 0 0 0 30977 23 0 0 25 0 1 0 479589060 31494144 7006 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7689 7006 603 41 0 7648 0
vsize: 30756
[startup+320.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14938
Raw data (stat): 14938 (minisat+) R 14937 11931 11930 0 -1 0 7226 0 0 0 31977 23 0 0 25 0 1 0 479589060 32030720 7152 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7820 7152 603 41 0 7779 0
vsize: 31280
[startup+330.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14938
Raw data (stat): 14938 (minisat+) R 14937 11931 11930 0 -1 0 7367 0 0 0 32977 24 0 0 25 0 1 0 479589060 32960512 7293 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8047 7293 603 41 0 8006 0
vsize: 32188
[startup+340.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14938
Raw data (stat): 14938 (minisat+) R 14937 11931 11930 0 -1 0 7523 0 0 0 33977 24 0 0 25 0 1 0 479589060 33501184 7449 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8179 7449 603 41 0 8138 0
vsize: 32716
[startup+350.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14938
Raw data (stat): 14938 (minisat+) R 14937 11931 11930 0 -1 0 7674 0 0 0 34975 25 0 0 25 0 1 0 479589060 34168832 7600 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8342 7600 603 41 0 8301 0
vsize: 33368
[startup+360.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14938
Raw data (stat): 14938 (minisat+) R 14937 11931 11930 0 -1 0 7837 0 0 0 35975 25 0 0 25 0 1 0 479589060 34840576 7763 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8506 7763 603 41 0 8465 0
vsize: 34024
[startup+370.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14938
Raw data (stat): 14938 (minisat+) R 14937 11931 11930 0 -1 0 7976 0 0 0 36975 26 0 0 25 0 1 0 479589060 35381248 7902 4294967295 134512640 134672761 3221224560 3221223728 134560942 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8638 7902 603 41 0 8597 0
vsize: 34552
[startup+380.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14938
Raw data (stat): 14938 (minisat+) R 14937 11931 11930 0 -1 0 8129 0 0 0 37975 26 0 0 25 0 1 0 479589060 36048896 8055 4294967295 134512640 134672761 3221224560 3221223728 134560858 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8801 8055 603 41 0 8760 0
vsize: 35204
[startup+390.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14938
Raw data (stat): 14938 (minisat+) R 14937 11931 11930 0 -1 0 8273 0 0 0 38975 26 0 0 25 0 1 0 479589060 36585472 8199 4294967295 134512640 134672761 3221224560 3221223744 134559618 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8932 8199 603 41 0 8891 0
vsize: 35728
[startup+400.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14938
Raw data (stat): 14938 (minisat+) R 14937 11931 11930 0 -1 0 8406 0 0 0 39974 27 0 0 25 0 1 0 479589060 37122048 8332 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9063 8332 603 41 0 9022 0
vsize: 36252
[startup+410.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14938
Raw data (stat): 14938 (minisat+) R 14937 11931 11930 0 -1 0 8539 0 0 0 40973 28 0 0 25 0 1 0 479589060 37658624 8465 4294967295 134512640 134672761 3221224560 3221223728 134560956 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9194 8465 603 41 0 9153 0
vsize: 36776
[startup+420.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14938
Raw data (stat): 14938 (minisat+) R 14937 11931 11930 0 -1 0 8702 0 0 0 41973 29 0 0 25 0 1 0 479589060 38330368 8628 4294967295 134512640 134672761 3221224560 3221223728 134560871 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9358 8628 603 41 0 9317 0
vsize: 37432
[startup+430.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14938
Raw data (stat): 14938 (minisat+) R 14937 11931 11930 0 -1 0 8859 0 0 0 42973 29 0 0 25 0 1 0 479589060 39002112 8785 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9522 8785 603 41 0 9481 0
vsize: 38088
[startup+440.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14938
Raw data (stat): 14938 (minisat+) R 14937 11931 11930 0 -1 0 9024 0 0 0 43973 29 0 0 25 0 1 0 479589060 39673856 8950 4294967295 134512640 134672761 3221224560 3221223728 134560903 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9686 8950 603 41 0 9645 0
vsize: 38744
[startup+450.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14938
Raw data (stat): 14938 (minisat+) R 14937 11931 11930 0 -1 0 9147 0 0 0 44972 30 0 0 25 0 1 0 479589060 40210432 9073 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9817 9073 603 41 0 9776 0
vsize: 39268
[startup+460.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14938
Raw data (stat): 14938 (minisat+) R 14937 11931 11930 0 -1 0 9275 0 0 0 45973 30 0 0 25 0 1 0 479589060 40624128 9201 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9918 9201 603 41 0 9877 0
vsize: 39672
[startup+470.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14938
Raw data (stat): 14938 (minisat+) R 14937 11931 11930 0 -1 0 9409 0 0 0 46973 30 0 0 25 0 1 0 479589060 41160704 9335 4294967295 134512640 134672761 3221224560 3221223728 134561382 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10049 9335 603 41 0 10008 0
vsize: 40196
[startup+480.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14938
Raw data (stat): 14938 (minisat+) R 14937 11931 11930 0 -1 0 9544 0 0 0 47972 31 0 0 25 0 1 0 479589060 41832448 9470 4294967295 134512640 134672761 3221224560 3221223728 134560885 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10213 9470 603 41 0 10172 0
vsize: 40852
[startup+490.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14938
Raw data (stat): 14938 (minisat+) R 14937 11931 11930 0 -1 0 9685 0 0 0 48972 31 0 0 25 0 1 0 479589060 42364928 9611 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10343 9611 603 41 0 10302 0
vsize: 41372
[startup+500.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14938
Raw data (stat): 14938 (minisat+) R 14937 11931 11930 0 -1 0 9810 0 0 0 49972 31 0 0 25 0 1 0 479589060 42905600 9736 4294967295 134512640 134672761 3221224560 3221223760 134557828 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10475 9736 603 41 0 10434 0
vsize: 41900
[startup+510.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14938
Raw data (stat): 14938 (minisat+) R 14937 11931 11930 0 -1 0 9935 0 0 0 50971 32 0 0 25 0 1 0 479589060 43307008 9861 4294967295 134512640 134672761 3221224560 3221223728 134561118 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10573 9861 603 41 0 10532 0
vsize: 42292
[startup+520.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14938
Raw data (stat): 14938 (minisat+) R 14937 11931 11930 0 -1 0 10080 0 0 0 51971 33 0 0 25 0 1 0 479589060 43974656 10006 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10736 10006 603 41 0 10695 0
vsize: 42944
[startup+530.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14938
Raw data (stat): 14938 (minisat+) R 14937 11931 11930 0 -1 0 10219 0 0 0 52970 33 0 0 25 0 1 0 479589060 44527616 10145 4294967295 134512640 134672761 3221224560 3221223728 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10871 10145 603 41 0 10830 0
vsize: 43484
[startup+540.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14938
Raw data (stat): 14938 (minisat+) R 14937 11931 11930 0 -1 0 10351 0 0 0 53970 34 0 0 25 0 1 0 479589060 45064192 10277 4294967295 134512640 134672761 3221224560 3221223728 134560892 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11002 10277 603 41 0 10961 0
vsize: 44008
[startup+550.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14938
Raw data (stat): 14938 (minisat+) R 14937 11931 11930 0 -1 0 10483 0 0 0 54970 34 0 0 25 0 1 0 479589060 45600768 10409 4294967295 134512640 134672761 3221224560 3221223728 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11133 10409 603 41 0 11092 0
vsize: 44532
[startup+560.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14938
Raw data (stat): 14938 (minisat+) R 14937 11931 11930 0 -1 0 10589 0 0 0 55970 34 0 0 25 0 1 0 479589060 46145536 10515 4294967295 134512640 134672761 3221224560 3221223560 1075350790 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11266 10515 603 41 0 11225 0
vsize: 45064
[startup+570.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14938
Raw data (stat): 14938 (minisat+) R 14937 11931 11930 0 -1 0 10589 0 0 0 56969 34 0 0 25 0 1 0 479589060 46145536 10515 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11266 10515 603 41 0 11225 0
vsize: 45064
[startup+580.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14938
Raw data (stat): 14938 (minisat+) R 14937 11931 11930 0 -1 0 10589 0 0 0 57970 34 0 0 25 0 1 0 479589060 46145536 10515 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11266 10515 603 41 0 11225 0
vsize: 45064
[startup+590.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14938
Raw data (stat): 14938 (minisat+) R 14937 11931 11930 0 -1 0 10589 0 0 0 58970 34 0 0 25 0 1 0 479589060 46145536 10515 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11266 10515 603 41 0 11225 0
vsize: 45064
[startup+600.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14938
Raw data (stat): 14938 (minisat+) R 14937 11931 11930 0 -1 0 10589 0 0 0 59970 34 0 0 25 0 1 0 479589060 46145536 10515 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11266 10515 603 41 0 11225 0
vsize: 45064
[startup+610.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14938
Raw data (stat): 14938 (minisat+) R 14937 11931 11930 0 -1 0 10589 0 0 0 60970 34 0 0 25 0 1 0 479589060 46145536 10515 4294967295 134512640 134672761 3221224560 3221223696 134565092 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11266 10515 603 41 0 11225 0
vsize: 45064
[startup+620.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14938
Raw data (stat): 14938 (minisat+) R 14937 11931 11930 0 -1 0 10589 0 0 0 61970 34 0 0 25 0 1 0 479589060 46145536 10515 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11266 10515 603 41 0 11225 0
vsize: 45064
[startup+630.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14938
Raw data (stat): 14938 (minisat+) R 14937 11931 11930 0 -1 0 10589 0 0 0 62970 34 0 0 25 0 1 0 479589060 46145536 10515 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11266 10515 603 41 0 11225 0
vsize: 45064
[startup+640.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14938
Raw data (stat): 14938 (minisat+) R 14937 11931 11930 0 -1 0 10589 0 0 0 63971 34 0 0 25 0 1 0 479589060 46145536 10515 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11266 10515 603 41 0 11225 0
vsize: 45064
[startup+650.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14938
Raw data (stat): 14938 (minisat+) R 14937 11931 11930 0 -1 0 10589 0 0 0 64971 34 0 0 25 0 1 0 479589060 46145536 10515 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11266 10515 603 41 0 11225 0
vsize: 45064
[startup+660.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14938
Raw data (stat): 14938 (minisat+) R 14937 11931 11930 0 -1 0 10589 0 0 0 65971 34 0 0 25 0 1 0 479589060 46145536 10515 4294967295 134512640 134672761 3221224560 3221223696 134560677 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11266 10515 603 41 0 11225 0
vsize: 45064
[startup+670.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14938
Raw data (stat): 14938 (minisat+) R 14937 11931 11930 0 -1 0 10589 0 0 0 66971 35 0 0 25 0 1 0 479589060 46145536 10515 4294967295 134512640 134672761 3221224560 3221223728 134560855 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11266 10515 603 41 0 11225 0
vsize: 45064
[startup+680.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14938
Raw data (stat): 14938 (minisat+) R 14937 11931 11930 0 -1 0 10589 0 0 0 67971 35 0 0 25 0 1 0 479589060 46145536 10515 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11266 10515 603 41 0 11225 0
vsize: 45064
[startup+690.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14938
Raw data (stat): 14938 (minisat+) R 14937 11931 11930 0 -1 0 10589 0 0 0 68972 35 0 0 25 0 1 0 479589060 46145536 10515 4294967295 134512640 134672761 3221224560 3221223728 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11266 10515 603 41 0 11225 0
vsize: 45064
[startup+700.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14938
Raw data (stat): 14938 (minisat+) R 14937 11931 11930 0 -1 0 10589 0 0 0 69972 35 0 0 25 0 1 0 479589060 46145536 10515 4294967295 134512640 134672761 3221224560 3221223744 134558918 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11266 10515 603 41 0 11225 0
vsize: 45064
[startup+710.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14938
Raw data (stat): 14938 (minisat+) R 14937 11931 11930 0 -1 0 10589 0 0 0 70972 35 0 0 25 0 1 0 479589060 46145536 10515 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11266 10515 603 41 0 11225 0
vsize: 45064
[startup+720.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14938
Raw data (stat): 14938 (minisat+) R 14937 11931 11930 0 -1 0 10589 0 0 0 71972 35 0 0 25 0 1 0 479589060 46145536 10515 4294967295 134512640 134672761 3221224560 3221223728 134561198 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11266 10515 603 41 0 11225 0
vsize: 45064
[startup+730.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14938
Raw data (stat): 14938 (minisat+) R 14937 11931 11930 0 -1 0 10589 0 0 0 72972 35 0 0 25 0 1 0 479589060 46145536 10515 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11266 10515 603 41 0 11225 0
vsize: 45064
[startup+740.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14938
Raw data (stat): 14938 (minisat+) R 14937 11931 11930 0 -1 0 10589 0 0 0 73972 35 0 0 25 0 1 0 479589060 46145536 10515 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11266 10515 603 41 0 11225 0
vsize: 45064
[startup+750.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14938
Raw data (stat): 14938 (minisat+) R 14937 11931 11930 0 -1 0 10589 0 0 0 74973 35 0 0 25 0 1 0 479589060 46145536 10515 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11266 10515 603 41 0 11225 0
vsize: 45064
[startup+760.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14938
Raw data (stat): 14938 (minisat+) R 14937 11931 11930 0 -1 0 10589 0 0 0 75973 35 0 0 25 0 1 0 479589060 46145536 10515 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11266 10515 603 41 0 11225 0
vsize: 45064
[startup+770.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14938
Raw data (stat): 14938 (minisat+) R 14937 11931 11930 0 -1 0 10589 0 0 0 76973 35 0 0 25 0 1 0 479589060 46145536 10515 4294967295 134512640 134672761 3221224560 3221223728 134561005 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11266 10515 603 41 0 11225 0
vsize: 45064
[startup+780.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14938
Raw data (stat): 14938 (minisat+) R 14937 11931 11930 0 -1 0 10589 0 0 0 77973 35 0 0 25 0 1 0 479589060 46145536 10515 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11266 10515 603 41 0 11225 0
vsize: 45064
[startup+790.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14938
Raw data (stat): 14938 (minisat+) R 14937 11931 11930 0 -1 0 10590 0 0 0 78973 35 0 0 25 0 1 0 479589060 46145536 10516 4294967295 134512640 134672761 3221224560 3221223728 134560882 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11266 10516 603 41 0 11225 0
vsize: 45064
[startup+800.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14938
Raw data (stat): 14938 (minisat+) R 14937 11931 11930 0 -1 0 10590 0 0 0 79974 35 0 0 25 0 1 0 479589060 46145536 10516 4294967295 134512640 134672761 3221224560 3221223760 134557809 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11266 10516 603 41 0 11225 0
vsize: 45064
[startup+810.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14938
Raw data (stat): 14938 (minisat+) R 14937 11931 11930 0 -1 0 10590 0 0 0 80973 35 0 0 25 0 1 0 479589060 46145536 10516 4294967295 134512640 134672761 3221224560 3221223728 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11266 10516 603 41 0 11225 0
vsize: 45064
[startup+820.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14938
Raw data (stat): 14938 (minisat+) R 14937 11931 11930 0 -1 0 10590 0 0 0 81973 35 0 0 25 0 1 0 479589060 46145536 10516 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11266 10516 603 41 0 11225 0
vsize: 45064
[startup+830.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14938
Raw data (stat): 14938 (minisat+) R 14937 11931 11930 0 -1 0 10590 0 0 0 82974 35 0 0 25 0 1 0 479589060 46145536 10516 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11266 10516 603 41 0 11225 0
vsize: 45064
[startup+840.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14938
Raw data (stat): 14938 (minisat+) R 14937 11931 11930 0 -1 0 10590 0 0 0 83974 35 0 0 25 0 1 0 479589060 46145536 10516 4294967295 134512640 134672761 3221224560 3221223728 134560912 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11266 10516 603 41 0 11225 0
vsize: 45064
[startup+850.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14938
Raw data (stat): 14938 (minisat+) R 14937 11931 11930 0 -1 0 10590 0 0 0 84974 35 0 0 25 0 1 0 479589060 46145536 10516 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11266 10516 603 41 0 11225 0
vsize: 45064
[startup+860.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14938
Raw data (stat): 14938 (minisat+) R 14937 11931 11930 0 -1 0 10590 0 0 0 85974 35 0 0 25 0 1 0 479589060 46145536 10516 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11266 10516 603 41 0 11225 0
vsize: 45064
[startup+870.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14938
Raw data (stat): 14938 (minisat+) R 14937 11931 11930 0 -1 0 10591 0 0 0 86974 35 0 0 25 0 1 0 479589060 46145536 10517 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11266 10517 603 41 0 11225 0
vsize: 45064
[startup+880.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14938
Raw data (stat): 14938 (minisat+) R 14937 11931 11930 0 -1 0 10591 0 0 0 87975 35 0 0 25 0 1 0 479589060 46145536 10517 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11266 10517 603 41 0 11225 0
vsize: 45064
[startup+890.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14938
Raw data (stat): 14938 (minisat+) R 14937 11931 11930 0 -1 0 10591 0 0 0 88975 35 0 0 25 0 1 0 479589060 46145536 10517 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11266 10517 603 41 0 11225 0
vsize: 45064
[startup+900.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14938
Raw data (stat): 14938 (minisat+) R 14937 11931 11930 0 -1 0 10591 0 0 0 89975 35 0 0 25 0 1 0 479589060 46145536 10517 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11266 10517 603 41 0 11225 0
vsize: 45064
[startup+910.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14938
Raw data (stat): 14938 (minisat+) R 14937 11931 11930 0 -1 0 10591 0 0 0 90975 35 0 0 25 0 1 0 479589060 46145536 10517 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11266 10517 603 41 0 11225 0
vsize: 45064
[startup+920.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14938
Raw data (stat): 14938 (minisat+) R 14937 11931 11930 0 -1 0 10591 0 0 0 91975 35 0 0 25 0 1 0 479589060 46145536 10517 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11266 10517 603 41 0 11225 0
vsize: 45064
[startup+930.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14938
Raw data (stat): 14938 (minisat+) R 14937 11931 11930 0 -1 0 10591 0 0 0 92975 35 0 0 25 0 1 0 479589060 46145536 10517 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11266 10517 603 41 0 11225 0
vsize: 45064
[startup+940.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14938
Raw data (stat): 14938 (minisat+) R 14937 11931 11930 0 -1 0 10591 0 0 0 93976 35 0 0 25 0 1 0 479589060 46145536 10517 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11266 10517 603 41 0 11225 0
vsize: 45064
[startup+950.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14938
Raw data (stat): 14938 (minisat+) R 14937 11931 11930 0 -1 0 10591 0 0 0 94976 35 0 0 25 0 1 0 479589060 46145536 10517 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11266 10517 603 41 0 11225 0
vsize: 45064
[startup+960.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14938
Raw data (stat): 14938 (minisat+) R 14937 11931 11930 0 -1 0 10591 0 0 0 95976 35 0 0 25 0 1 0 479589060 46145536 10517 4294967295 134512640 134672761 3221224560 3221223728 134560980 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11266 10517 603 41 0 11225 0
vsize: 45064
[startup+970.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14938
Raw data (stat): 14938 (minisat+) R 14937 11931 11930 0 -1 0 10592 0 0 0 96976 35 0 0 25 0 1 0 479589060 46145536 10518 4294967295 134512640 134672761 3221224560 3221223728 134560964 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11266 10518 603 41 0 11225 0
vsize: 45064
[startup+980.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14938
Raw data (stat): 14938 (minisat+) R 14937 11931 11930 0 -1 0 10592 0 0 0 97977 35 0 0 25 0 1 0 479589060 46145536 10518 4294967295 134512640 134672761 3221224560 3221223728 134560903 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11266 10518 603 41 0 11225 0
vsize: 45064
[startup+990.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14938
Raw data (stat): 14938 (minisat+) R 14937 11931 11930 0 -1 0 10593 0 0 0 98977 35 0 0 25 0 1 0 479589060 46145536 10519 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11266 10519 603 41 0 11225 0
vsize: 45064
[startup+1000.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14938
Raw data (stat): 14938 (minisat+) R 14937 11931 11930 0 -1 0 10743 0 0 0 99977 35 0 0 25 0 1 0 479589060 46682112 10669 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11397 10669 603 41 0 11356 0
vsize: 45588
[startup+1010.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14938
Raw data (stat): 14938 (minisat+) R 14937 11931 11930 0 -1 0 10882 0 0 0 100976 35 0 0 25 0 1 0 479589060 47210496 10808 4294967295 134512640 134672761 3221224560 3221223728 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11526 10808 603 41 0 11485 0
vsize: 46104
[startup+1020.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14938
Raw data (stat): 14938 (minisat+) R 14937 11931 11930 0 -1 0 11031 0 0 0 101976 36 0 0 25 0 1 0 479589060 47882240 10957 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11690 10957 603 41 0 11649 0
vsize: 46760
[startup+1030.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14938
Raw data (stat): 14938 (minisat+) R 14937 11931 11930 0 -1 0 11166 0 0 0 102976 36 0 0 25 0 1 0 479589060 48414720 11092 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11820 11092 603 41 0 11779 0
vsize: 47280
[startup+1040.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14938
Raw data (stat): 14938 (minisat+) R 14937 11931 11930 0 -1 0 11308 0 0 0 103976 37 0 0 25 0 1 0 479589060 48951296 11234 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11951 11234 603 41 0 11910 0
vsize: 47804
[startup+1050.02 s]
Raw data (loadavg): 1.06 0.99 0.91 2/54 14938
Raw data (stat): 14938 (minisat+) R 14937 11931 11930 0 -1 0 11435 0 0 0 104975 37 0 0 25 0 1 0 479589060 49483776 11361 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12081 11361 603 41 0 12040 0
vsize: 48324
[startup+1060.02 s]
Raw data (loadavg): 1.05 0.99 0.91 2/54 14938
Raw data (stat): 14938 (minisat+) R 14937 11931 11930 0 -1 0 11556 0 0 0 105975 37 0 0 25 0 1 0 479589060 50020352 11482 4294967295 134512640 134672761 3221224560 3221223728 134561139 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12212 11482 603 41 0 12171 0
vsize: 48848
[startup+1070.02 s]
Raw data (loadavg): 1.04 0.99 0.91 2/54 14938
Raw data (stat): 14938 (minisat+) R 14937 11931 11930 0 -1 0 11672 0 0 0 106975 38 0 0 25 0 1 0 479589060 50429952 11598 4294967295 134512640 134672761 3221224560 3221223728 134561011 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12312 11598 603 41 0 12271 0
vsize: 49248
[startup+1080.02 s]
Raw data (loadavg): 1.04 0.99 0.91 2/54 14938
Raw data (stat): 14938 (minisat+) R 14937 11931 11930 0 -1 0 11793 0 0 0 107975 38 0 0 25 0 1 0 479589060 50966528 11719 4294967295 134512640 134672761 3221224560 3221223728 134561164 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12443 11719 603 41 0 12402 0
vsize: 49772
[startup+1090.02 s]
Raw data (loadavg): 1.03 0.99 0.91 2/54 14938
Raw data (stat): 14938 (minisat+) R 14937 11931 11930 0 -1 0 11903 0 0 0 108975 38 0 0 25 0 1 0 479589060 51507200 11829 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12575 11829 603 41 0 12534 0
vsize: 50300
[startup+1100.02 s]
Raw data (loadavg): 1.03 0.99 0.91 2/54 14938
Raw data (stat): 14938 (minisat+) R 14937 11931 11930 0 -1 0 12037 0 0 0 109974 39 0 0 25 0 1 0 479589060 52047872 11963 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12707 11963 603 41 0 12666 0
vsize: 50828
[startup+1110.02 s]
Raw data (loadavg): 1.02 0.99 0.91 2/54 14938
Raw data (stat): 14938 (minisat+) R 14937 11931 11930 0 -1 0 12167 0 0 0 110974 39 0 0 25 0 1 0 479589060 52613120 12093 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12845 12093 603 41 0 12804 0
vsize: 51380
[startup+1120.03 s]
Raw data (loadavg): 1.02 0.99 0.91 2/54 14938
Raw data (stat): 14938 (minisat+) R 14937 11931 11930 0 -1 0 12287 0 0 0 111974 40 0 0 25 0 1 0 479589060 53035008 12213 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12948 12213 603 41 0 12907 0
vsize: 51792
[startup+1130.02 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 14938
Raw data (stat): 14938 (minisat+) R 14937 11931 11930 0 -1 0 12416 0 0 0 112974 40 0 0 25 0 1 0 479589060 53571584 12342 4294967295 134512640 134672761 3221224560 3221223728 134560909 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13079 12342 603 41 0 13038 0
vsize: 52316
[startup+1140.02 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 14938
Raw data (stat): 14938 (minisat+) R 14937 11931 11930 0 -1 0 12531 0 0 0 113974 40 0 0 25 0 1 0 479589060 54108160 12457 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13210 12457 603 41 0 13169 0
vsize: 52840
[startup+1150.03 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 14938
Raw data (stat): 14938 (minisat+) R 14937 11931 11930 0 -1 0 12648 0 0 0 114974 40 0 0 25 0 1 0 479589060 54509568 12574 4294967295 134512640 134672761 3221224560 3221223728 134560874 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13308 12574 603 41 0 13267 0
vsize: 53232
[startup+1160.03 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 14938
Raw data (stat): 14938 (minisat+) R 14937 11931 11930 0 -1 0 12770 0 0 0 115974 40 0 0 25 0 1 0 479589060 55042048 12696 4294967295 134512640 134672761 3221224560 3221223664 134560215 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13438 12696 603 41 0 13397 0
vsize: 53752
[startup+1170.03 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 14938
Raw data (stat): 14938 (minisat+) R 14937 11931 11930 0 -1 0 12881 0 0 0 116974 41 0 0 25 0 1 0 479589060 55468032 12807 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13542 12807 603 41 0 13501 0
vsize: 54168
[startup+1180.03 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 14938
Raw data (stat): 14938 (minisat+) R 14937 11931 11930 0 -1 0 13000 0 0 0 117974 41 0 0 25 0 1 0 479589060 56000512 12926 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13672 12926 603 41 0 13631 0
vsize: 54688
[startup+1190.03 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 14938
Raw data (stat): 14938 (minisat+) R 14937 11931 11930 0 -1 0 13135 0 0 0 118974 41 0 0 25 0 1 0 479589060 56541184 13061 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13804 13061 603 41 0 13763 0
vsize: 55216
[startup+1200.03 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 14938
Raw data (stat): 14938 (minisat+) R 14937 11931 11930 0 -1 0 13237 0 0 0 119974 41 0 0 25 0 1 0 479589060 56942592 13163 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13902 13163 603 41 0 13861 0
vsize: 55608
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.05 s]
Raw data (loadavg): 1.00 0.99 0.91 1/54 14938
Raw data (stat): 14938 (minisat+) Z 14937 11931 11930 0 -1 12 13240 0 0 0 119974 44 0 0 25 0 1 0 479589060 0 0 4294967295 0 0 0 0 0 0 16384 5 16386 3222412051 0 0 17 0 0 0
Raw data (statm): 0 0 0 0 0 0 0
vsize: 0
Maximum CPU time exceeded: sending SIGTERM and SIGKILL

Child status: 10
Real time (s): 1200.05
CPU time (s): 1200.19
CPU user time (s): 1199.74
CPU system time (s): 0.444932
CPU usage (%): 100.011
Max. virtual memory (Kb): 55608
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####