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-circ6_3.opb
MD5SUM	509cfdb6810b13d9963718243e9046cd
Bench Category	optimization, small integers (OPTSMALLINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	66
Optimality of the best value was proved	NO
Number of terms in the objective function	180
Biggest coefficient in the objective function	3
Number of bits for the biggest coefficient in the objective function	2
Sum of the numbers in the objective function	324
Number of bits of the sum of numbers in the objective function	9
Biggest number in a constraint	16
Number of bits of the biggest number in a constraint	5
Biggest sum of numbers in a constraint	324
Number of bits of the biggest sum of numbers	9
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	1175.98
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 5213

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc11 THE 2005-04-13 22:34:20 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=3642 boxname=wulflinc11 idbench=258 idsolver=10 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  509cfdb6810b13d9963718243e9046cd  /oldhome/oroussel/tmp/wulflinc11/normalized-circ6_3.opb
REAL COMMAND:  minisat+ -ca /oldhome/oroussel/tmp/wulflinc11/normalized-circ6_3.opb /oldhome/oroussel/tmp/wulflinc11/normalized-circ6_3.opb
IDLAUNCH: 3642
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.028
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	: 2
cpu MHz		: 451.028
cache size	: 512 KB
fdiv_bug	: no
hlt_bug		: no
f00f_bug	: no
coma_bug	: no
fpu		: yes
fpu_exception	: yes
cpuid level	: 2
wp		: yes
flags		: fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse
bogomips	: 899.07

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        915932 kB
Buffers:         34656 kB
Cached:          59828 kB
SwapCached:       4932 kB
Active:          54192 kB
Inactive:        48108 kB
HighTotal:      131008 kB
HighFree:        67396 kB
LowTotal:       903652 kB
LowFree:        848536 kB
SwapTotal:     2097136 kB
SwapFree:      2092204 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6924 kB
Slab:            10844 kB
Committed_AS:    63488 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-13 22:54:23 (client local time) WITH STATUS 10 IN 1200.1 SECONDS
stats: 3642 7 1200.1 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: 80[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 378   maxlim: 244   bits: 9/8
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       161 |   71381   247964 |   23793     147     1235     8.4 | 25.986 % |
c |       261 |   71288   247661 |   26172     241     2438    10.1 | 25.579 % |
c |       411 |   71272   247607 |   28789     390     5426    13.9 | 25.597 % |
c |       636 |   71149   247189 |   31668     610     8110    13.3 | 25.674 % |
c |       973 |   70895   246319 |   34835     934    14531    15.6 | 25.833 % |
c |      1480 |   70047   243334 |   38318    1418    23462    16.5 | 26.117 % |
c ==============================================================================
c [1mFound solution: 78[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 246   bits: 9/8
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      1550 |   70051   243359 |   23350    1488    24616    16.5 | 26.117 % |
c |      1650 |   69818   242564 |   25685    1577    25924    16.4 | 26.279 % |
c ==============================================================================
c [1mFound solution: 76[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 248   bits: 9/8
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      1709 |   69709   242181 |   23236    1632    26790    16.4 | 26.279 % |
c |      1809 |   69709   242181 |   25559    1732    29407    17.0 | 26.306 % |
c |      1960 |   69709   242181 |   28115    1883    33915    18.0 | 26.306 % |
c |      2186 |   69405   241110 |   30927    2099    37477    17.9 | 26.412 % |
c |      2523 |   69375   241016 |   34019    2434    50277    20.7 | 26.448 % |
c |      3029 |   69005   239713 |   37421    2925    65411    22.4 | 26.572 % |
c |      3789 |   68774   238906 |   41163    3678    89708    24.4 | 26.666 % |
c |      4929 |   68469   237833 |   45280    4809   131035    27.2 | 26.773 % |
c |      6641 |   68200   236903 |   49808    6511   216743    33.3 | 26.897 % |
c ==============================================================================
c [1mFound solution: 72[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 252   bits: 9/8
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      6937 |   68203   236923 |   22734    6807   230291    33.8 | 26.897 % |
c |      7038 |   68203   236923 |   25007    6908   235192    34.0 | 26.904 % |
c |      7189 |   68139   236694 |   27508    7058   241232    34.2 | 26.916 % |
c |      7416 |   68139   236694 |   30258    7285   253171    34.8 | 26.916 % |
c |      7753 |   67748   235290 |   33284    7612   270134    35.5 | 26.986 % |
c |      8259 |   67733   235243 |   36613    8117   296686    36.6 | 27.004 % |
c |      9018 |   67733   235243 |   40274    8876   334793    37.7 | 27.004 % |
c |     10159 |   67733   235243 |   44302   10017   409089    40.8 | 27.004 % |
c |     11867 |   67402   234058 |   48732   11714   492580    42.1 | 27.081 % |
c |     14429 |   67313   233750 |   53605   14272   617629    43.3 | 27.128 % |
c |     18273 |   67225   233449 |   58966   18111   863605    47.7 | 27.176 % |
c |     24040 |   67155   233198 |   64862   23876  1258964    52.7 | 27.187 % |
c |     32689 |   67140   233151 |   71349   32524  1817275    55.9 | 27.205 % |
c |     45663 |   67140   233151 |   78483   45498  2510483    55.2 | 27.205 % |
c |     65125 |   67009   232679 |   86332   64956  3819066    58.8 | 27.223 % |
c |     94317 |   66858   232149 |   94965   20575  1025976    49.9 | 27.282 % |
c ==============================================================================
c [1mFound solution: 70[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 254   bits: 9/8
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    125712 |   66861   232170 |   22287   51970  3311508    63.7 | 27.282 % |
c |    125813 |   66861   232170 |   24515   18033   921812    51.1 | 27.289 % |
c |    125963 |   66861   232170 |   26967   18183   929997    51.1 | 27.289 % |
c |    126189 |   66861   232170 |   29663   18409   940717    51.1 | 27.289 % |
c |    126526 |   66861   232170 |   32630   18746   962492    51.3 | 27.289 % |
c |    127032 |   66861   232170 |   35893   19252   970761    50.4 | 27.289 % |
c |    127793 |   66861   232170 |   39482   20013  1032761    51.6 | 27.289 % |
c |    128933 |   66861   232170 |   43431   21153  1108266    52.4 | 27.289 % |
c |    130643 |   66861   232170 |   47774   22863  1214626    53.1 | 27.289 % |
c |    133205 |   66861   232170 |   52551   25425  1384194    54.4 | 27.289 % |
c |    137050 |   66861   232170 |   57806   29270  1666558    56.9 | 27.289 % |
c |    142818 |   66861   232170 |   63587   35038  2080496    59.4 | 27.289 % |
c |    151467 |   66861   232170 |   69946   43687  2739866    62.7 | 27.289 % |
c |    164441 |   66861   232170 |   76940   56661  3713096    65.5 | 27.289 % |
c |    183904 |   66861   232170 |   84634   76124  5141403    67.5 | 27.289 % |
#### 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 5204
Raw data (stat): 5204 (runsolver) R 5203 32461 32460 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 421364083 1052672 99 4294967295 134512640 135381576 3221224464 3221219708 135158418 0 2147483391 7 90112 0 0 0 17 1 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0007 s]
Raw data (loadavg): 0.93 0.95 0.90 2/54 5204
Raw data (stat): 5204 (minisat+) R 5203 32461 32460 0 -1 0 2232 0 0 0 991 6 0 0 25 0 1 0 421364083 11653120 2158 4294967295 134512640 134672761 3221224560 3221223728 134560876 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2845 2158 603 41 0 2804 0
vsize: 11380
[startup+20.0009 s]
Raw data (loadavg): 0.94 0.96 0.91 2/54 5204
Raw data (stat): 5204 (minisat+) R 5203 32461 32460 0 -1 0 2396 0 0 0 1990 7 0 0 25 0 1 0 421364083 12328960 2322 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3010 2322 603 41 0 2969 0
vsize: 12040
[startup+30.0023 s]
Raw data (loadavg): 0.95 0.96 0.91 2/54 5204
Raw data (stat): 5204 (minisat+) R 5203 32461 32460 0 -1 0 2578 0 0 0 2990 7 0 0 25 0 1 0 421364083 13135872 2504 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3207 2504 603 41 0 3166 0
vsize: 12828
[startup+40.0031 s]
Raw data (loadavg): 0.95 0.96 0.91 2/54 5204
Raw data (stat): 5204 (minisat+) R 5203 32461 32460 0 -1 0 2746 0 0 0 3988 8 0 0 25 0 1 0 421364083 13811712 2672 4294967295 134512640 134672761 3221224560 3221223728 134560903 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3372 2672 603 41 0 3331 0
vsize: 13488
[startup+50.0033 s]
Raw data (loadavg): 0.96 0.96 0.91 2/54 5204
Raw data (stat): 5204 (minisat+) R 5203 32461 32460 0 -1 0 2876 0 0 0 4987 9 0 0 25 0 1 0 421364083 14344192 2802 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3502 2802 603 41 0 3461 0
vsize: 14008
[startup+60.0034 s]
Raw data (loadavg): 0.97 0.96 0.91 2/54 5204
Raw data (stat): 5204 (minisat+) R 5203 32461 32460 0 -1 0 3090 0 0 0 5987 9 0 0 25 0 1 0 421364083 15302656 3016 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3736 3016 603 41 0 3695 0
vsize: 14944
[startup+70.0045 s]
Raw data (loadavg): 0.97 0.96 0.91 2/54 5204
Raw data (stat): 5204 (minisat+) R 5203 32461 32460 0 -1 0 3286 0 0 0 6986 10 0 0 25 0 1 0 421364083 16105472 3212 4294967295 134512640 134672761 3221224560 3221223516 1075349698 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3932 3212 603 41 0 3891 0
vsize: 15728
[startup+80.0047 s]
Raw data (loadavg): 0.98 0.96 0.91 2/54 5204
Raw data (stat): 5204 (minisat+) R 5203 32461 32460 0 -1 0 3491 0 0 0 7985 11 0 0 25 0 1 0 421364083 16900096 3417 4294967295 134512640 134672761 3221224560 3221223728 134561167 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4126 3417 603 41 0 4085 0
vsize: 16504
[startup+90.0048 s]
Raw data (loadavg): 0.98 0.96 0.91 2/54 5204
Raw data (stat): 5204 (minisat+) R 5203 32461 32460 0 -1 0 3668 0 0 0 8984 12 0 0 25 0 1 0 421364083 17563648 3594 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4288 3594 603 41 0 4247 0
vsize: 17152
[startup+100.005 s]
Raw data (loadavg): 0.98 0.96 0.91 2/54 5204
Raw data (stat): 5204 (minisat+) R 5203 32461 32460 0 -1 0 3852 0 0 0 9984 12 0 0 25 0 1 0 421364083 18366464 3778 4294967295 134512640 134672761 3221224560 3221223728 134560906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4484 3778 603 41 0 4443 0
vsize: 17936
[startup+110.005 s]
Raw data (loadavg): 0.98 0.96 0.91 2/54 5204
Raw data (stat): 5204 (minisat+) R 5203 32461 32460 0 -1 0 4012 0 0 0 10983 13 0 0 25 0 1 0 421364083 19025920 3938 4294967295 134512640 134672761 3221224560 3221223728 134560903 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4645 3938 603 41 0 4604 0
vsize: 18580
[startup+120.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5204
Raw data (stat): 5204 (minisat+) R 5203 32461 32460 0 -1 0 4180 0 0 0 11984 13 0 0 25 0 1 0 421364083 19693568 4106 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4808 4106 603 41 0 4767 0
vsize: 19232
[startup+130.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5204
Raw data (stat): 5204 (minisat+) R 5203 32461 32460 0 -1 0 4330 0 0 0 12983 14 0 0 25 0 1 0 421364083 20357120 4256 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4970 4256 603 41 0 4929 0
vsize: 19880
[startup+140.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5204
Raw data (stat): 5204 (minisat+) R 5203 32461 32460 0 -1 0 4444 0 0 0 13982 15 0 0 25 0 1 0 421364083 20897792 4370 4294967295 134512640 134672761 3221224560 3221223728 134561215 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5102 4370 603 41 0 5061 0
vsize: 20408
[startup+150.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5204
Raw data (stat): 5204 (minisat+) R 5203 32461 32460 0 -1 0 4560 0 0 0 14983 15 0 0 25 0 1 0 421364083 21303296 4486 4294967295 134512640 134672761 3221224560 3221223696 134560688 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5201 4486 603 41 0 5160 0
vsize: 20804
[startup+160.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5204
Raw data (stat): 5204 (minisat+) R 5203 32461 32460 0 -1 0 4672 0 0 0 15982 15 0 0 25 0 1 0 421364083 21835776 4598 4294967295 134512640 134672761 3221224560 3221223728 134561201 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5331 4598 603 41 0 5290 0
vsize: 21324
[startup+170.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5204
Raw data (stat): 5204 (minisat+) R 5203 32461 32460 0 -1 0 4783 0 0 0 16982 15 0 0 25 0 1 0 421364083 22237184 4709 4294967295 134512640 134672761 3221224560 3221223728 134560892 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5429 4709 603 41 0 5388 0
vsize: 21716
[startup+180.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5204
Raw data (stat): 5204 (minisat+) R 5203 32461 32460 0 -1 0 4891 0 0 0 17982 16 0 0 25 0 1 0 421364083 22642688 4817 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5528 4817 603 41 0 5487 0
vsize: 22112
[startup+190.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5204
Raw data (stat): 5204 (minisat+) R 5203 32461 32460 0 -1 0 5001 0 0 0 18982 16 0 0 25 0 1 0 421364083 23179264 4927 4294967295 134512640 134672761 3221224560 3221223728 134560871 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5659 4927 603 41 0 5618 0
vsize: 22636
[startup+200.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5204
Raw data (stat): 5204 (minisat+) R 5203 32461 32460 0 -1 0 5118 0 0 0 19982 16 0 0 25 0 1 0 421364083 23584768 5044 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5758 5044 603 41 0 5717 0
vsize: 23032
[startup+210.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5204
Raw data (stat): 5204 (minisat+) R 5203 32461 32460 0 -1 0 5260 0 0 0 20982 17 0 0 25 0 1 0 421364083 24121344 5186 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5889 5186 603 41 0 5848 0
vsize: 23556
[startup+220.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5204
Raw data (stat): 5204 (minisat+) R 5203 32461 32460 0 -1 0 5404 0 0 0 21981 18 0 0 25 0 1 0 421364083 24784896 5330 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6051 5330 603 41 0 6010 0
vsize: 24204
[startup+230.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5204
Raw data (stat): 5204 (minisat+) R 5203 32461 32460 0 -1 0 5536 0 0 0 22981 18 0 0 25 0 1 0 421364083 25329664 5462 4294967295 134512640 134672761 3221224560 3221223728 134560929 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6184 5462 603 41 0 6143 0
vsize: 24736
[startup+240.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5204
Raw data (stat): 5204 (minisat+) R 5203 32461 32460 0 -1 0 5649 0 0 0 23980 18 0 0 25 0 1 0 421364083 25726976 5575 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6281 5575 603 41 0 6240 0
vsize: 25124
[startup+250.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5204
Raw data (stat): 5204 (minisat+) R 5203 32461 32460 0 -1 0 5769 0 0 0 24981 19 0 0 25 0 1 0 421364083 26267648 5695 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6413 5695 603 41 0 6372 0
vsize: 25652
[startup+260.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5204
Raw data (stat): 5204 (minisat+) R 5203 32461 32460 0 -1 0 5891 0 0 0 25980 19 0 0 25 0 1 0 421364083 26800128 5817 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6543 5817 603 41 0 6502 0
vsize: 26172
[startup+270.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5204
Raw data (stat): 5204 (minisat+) R 5203 32461 32460 0 -1 0 6016 0 0 0 26980 19 0 0 25 0 1 0 421364083 27201536 5942 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6641 5942 603 41 0 6600 0
vsize: 26564
[startup+280.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5204
Raw data (stat): 5204 (minisat+) R 5203 32461 32460 0 -1 0 6151 0 0 0 27980 20 0 0 25 0 1 0 421364083 27734016 6077 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6771 6077 603 41 0 6730 0
vsize: 27084
[startup+290.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5204
Raw data (stat): 5204 (minisat+) R 5203 32461 32460 0 -1 0 6280 0 0 0 28980 20 0 0 25 0 1 0 421364083 28266496 6206 4294967295 134512640 134672761 3221224560 3221223728 134561205 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6901 6206 603 41 0 6860 0
vsize: 27604
[startup+300.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5204
Raw data (stat): 5204 (minisat+) R 5203 32461 32460 0 -1 0 6414 0 0 0 29979 21 0 0 25 0 1 0 421364083 28921856 6340 4294967295 134512640 134672761 3221224560 3221223696 134560661 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7061 6340 603 41 0 7020 0
vsize: 28244
[startup+310.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5204
Raw data (stat): 5204 (minisat+) R 5203 32461 32460 0 -1 0 6545 0 0 0 30979 22 0 0 25 0 1 0 421364083 29454336 6471 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7191 6471 603 41 0 7150 0
vsize: 28764
[startup+320.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5204
Raw data (stat): 5204 (minisat+) R 5203 32461 32460 0 -1 0 6688 0 0 0 31979 22 0 0 25 0 1 0 421364083 30261248 6614 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7388 6614 603 41 0 7347 0
vsize: 29552
[startup+330.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5204
Raw data (stat): 5204 (minisat+) R 5203 32461 32460 0 -1 0 6816 0 0 0 32979 22 0 0 25 0 1 0 421364083 30797824 6742 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7519 6742 603 41 0 7478 0
vsize: 30076
[startup+340.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5204
Raw data (stat): 5204 (minisat+) R 5203 32461 32460 0 -1 0 6934 0 0 0 33978 23 0 0 25 0 1 0 421364083 31191040 6860 4294967295 134512640 134672761 3221224560 3221223728 134561205 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7615 6860 603 41 0 7574 0
vsize: 30460
[startup+350.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5204
Raw data (stat): 5204 (minisat+) R 5203 32461 32460 0 -1 0 7061 0 0 0 34978 23 0 0 25 0 1 0 421364083 31715328 6987 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7743 6987 603 41 0 7702 0
vsize: 30972
[startup+360.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5204
Raw data (stat): 5204 (minisat+) R 5203 32461 32460 0 -1 0 7196 0 0 0 35978 23 0 0 25 0 1 0 421364083 32251904 7122 4294967295 134512640 134672761 3221224560 3221223728 134561215 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7874 7122 603 41 0 7833 0
vsize: 31496
[startup+370.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5204
Raw data (stat): 5204 (minisat+) R 5203 32461 32460 0 -1 0 7319 0 0 0 36978 24 0 0 25 0 1 0 421364083 32784384 7245 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8004 7245 603 41 0 7963 0
vsize: 32016
[startup+380.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5204
Raw data (stat): 5204 (minisat+) R 5203 32461 32460 0 -1 0 7431 0 0 0 37978 24 0 0 25 0 1 0 421364083 33185792 7357 4294967295 134512640 134672761 3221224560 3221223728 134560855 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8102 7357 603 41 0 8061 0
vsize: 32408
[startup+390.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5204
Raw data (stat): 5204 (minisat+) R 5203 32461 32460 0 -1 0 7550 0 0 0 38978 24 0 0 25 0 1 0 421364083 33730560 7476 4294967295 134512640 134672761 3221224560 3221223728 134560888 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8235 7476 603 41 0 8194 0
vsize: 32940
[startup+400.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5204
Raw data (stat): 5204 (minisat+) R 5203 32461 32460 0 -1 0 7673 0 0 0 39977 25 0 0 25 0 1 0 421364083 34267136 7599 4294967295 134512640 134672761 3221224560 3221223728 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8366 7599 603 41 0 8325 0
vsize: 33464
[startup+410.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5204
Raw data (stat): 5204 (minisat+) R 5203 32461 32460 0 -1 0 7780 0 0 0 40977 26 0 0 25 0 1 0 421364083 34664448 7706 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8463 7706 603 41 0 8422 0
vsize: 33852
[startup+420.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5204
Raw data (stat): 5204 (minisat+) R 5203 32461 32460 0 -1 0 7895 0 0 0 41976 26 0 0 25 0 1 0 421364083 35069952 7821 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8562 7821 603 41 0 8521 0
vsize: 34248
[startup+430.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5204
Raw data (stat): 5204 (minisat+) R 5203 32461 32460 0 -1 0 8002 0 0 0 42976 27 0 0 25 0 1 0 421364083 35606528 7928 4294967295 134512640 134672761 3221224560 3221223728 134560929 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8693 7928 603 41 0 8652 0
vsize: 34772
[startup+440.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5204
Raw data (stat): 5204 (minisat+) R 5203 32461 32460 0 -1 0 8134 0 0 0 43976 27 0 0 25 0 1 0 421364083 36143104 8060 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8824 8060 603 41 0 8783 0
vsize: 35296
[startup+450.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5204
Raw data (stat): 5204 (minisat+) R 5203 32461 32460 0 -1 0 8241 0 0 0 44976 27 0 0 25 0 1 0 421364083 36536320 8167 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8920 8167 603 41 0 8879 0
vsize: 35680
[startup+460.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5204
Raw data (stat): 5204 (minisat+) R 5203 32461 32460 0 -1 0 8375 0 0 0 45976 27 0 0 25 0 1 0 421364083 37072896 8301 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9051 8301 603 41 0 9010 0
vsize: 36204
[startup+470.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5204
Raw data (stat): 5204 (minisat+) R 5203 32461 32460 0 -1 0 8481 0 0 0 46976 28 0 0 25 0 1 0 421364083 37470208 8407 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9148 8407 603 41 0 9107 0
vsize: 36592
[startup+480.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5204
Raw data (stat): 5204 (minisat+) R 5203 32461 32460 0 -1 0 8588 0 0 0 47976 28 0 0 25 0 1 0 421364083 37998592 8514 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9277 8514 603 41 0 9236 0
vsize: 37108
[startup+490.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5204
Raw data (stat): 5204 (minisat+) R 5203 32461 32460 0 -1 0 8697 0 0 0 48976 28 0 0 25 0 1 0 421364083 38400000 8623 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9375 8623 603 41 0 9334 0
vsize: 37500
[startup+500.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5204
Raw data (stat): 5204 (minisat+) R 5203 32461 32460 0 -1 0 8802 0 0 0 49976 28 0 0 25 0 1 0 421364083 38801408 8728 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9473 8728 603 41 0 9432 0
vsize: 37892
[startup+510.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5204
Raw data (stat): 5204 (minisat+) R 5203 32461 32460 0 -1 0 8924 0 0 0 50975 29 0 0 25 0 1 0 421364083 39329792 8850 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9602 8850 603 41 0 9561 0
vsize: 38408
[startup+520.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5204
Raw data (stat): 5204 (minisat+) R 5203 32461 32460 0 -1 0 8935 0 0 0 51974 29 0 0 25 0 1 0 421364083 39329792 8861 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9602 8861 603 41 0 9561 0
vsize: 38408
[startup+530.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5204
Raw data (stat): 5204 (minisat+) R 5203 32461 32460 0 -1 0 8935 0 0 0 52975 29 0 0 25 0 1 0 421364083 39329792 8861 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9602 8861 603 41 0 9561 0
vsize: 38408
[startup+540.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5204
Raw data (stat): 5204 (minisat+) R 5203 32461 32460 0 -1 0 8935 0 0 0 53975 29 0 0 25 0 1 0 421364083 39329792 8861 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9602 8861 603 41 0 9561 0
vsize: 38408
[startup+550.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5204
Raw data (stat): 5204 (minisat+) R 5203 32461 32460 0 -1 0 8935 0 0 0 54975 29 0 0 25 0 1 0 421364083 39329792 8861 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9602 8861 603 41 0 9561 0
vsize: 38408
[startup+560.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5204
Raw data (stat): 5204 (minisat+) R 5203 32461 32460 0 -1 0 8935 0 0 0 55975 29 0 0 25 0 1 0 421364083 39329792 8861 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9602 8861 603 41 0 9561 0
vsize: 38408
[startup+570.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5204
Raw data (stat): 5204 (minisat+) R 5203 32461 32460 0 -1 0 8935 0 0 0 56976 29 0 0 25 0 1 0 421364083 39329792 8861 4294967295 134512640 134672761 3221224560 3221223728 134561188 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9602 8861 603 41 0 9561 0
vsize: 38408
[startup+580.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5204
Raw data (stat): 5204 (minisat+) R 5203 32461 32460 0 -1 0 8936 0 0 0 57976 29 0 0 25 0 1 0 421364083 39329792 8862 4294967295 134512640 134672761 3221224560 3221223728 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9602 8862 603 41 0 9561 0
vsize: 38408
[startup+590.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5204
Raw data (stat): 5204 (minisat+) R 5203 32461 32460 0 -1 0 8936 0 0 0 58976 29 0 0 25 0 1 0 421364083 39329792 8862 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9602 8862 603 41 0 9561 0
vsize: 38408
[startup+600.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5204
Raw data (stat): 5204 (minisat+) R 5203 32461 32460 0 -1 0 8936 0 0 0 59976 29 0 0 25 0 1 0 421364083 39329792 8862 4294967295 134512640 134672761 3221224560 3221223728 134560942 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9602 8862 603 41 0 9561 0
vsize: 38408
[startup+610.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5204
Raw data (stat): 5204 (minisat+) R 5203 32461 32460 0 -1 0 8936 0 0 0 60976 29 0 0 25 0 1 0 421364083 39329792 8862 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9602 8862 603 41 0 9561 0
vsize: 38408
[startup+620.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5204
Raw data (stat): 5204 (minisat+) R 5203 32461 32460 0 -1 0 8936 0 0 0 61976 29 0 0 25 0 1 0 421364083 39329792 8862 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9602 8862 603 41 0 9561 0
vsize: 38408
[startup+630.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5204
Raw data (stat): 5204 (minisat+) R 5203 32461 32460 0 -1 0 8936 0 0 0 62977 29 0 0 25 0 1 0 421364083 39329792 8862 4294967295 134512640 134672761 3221224560 3221223728 134560954 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9602 8862 603 41 0 9561 0
vsize: 38408
[startup+640.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5204
Raw data (stat): 5204 (minisat+) R 5203 32461 32460 0 -1 0 8936 0 0 0 63977 29 0 0 25 0 1 0 421364083 39329792 8862 4294967295 134512640 134672761 3221224560 3221223700 134560556 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9602 8862 603 41 0 9561 0
vsize: 38408
[startup+650.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5204
Raw data (stat): 5204 (minisat+) R 5203 32461 32460 0 -1 0 8936 0 0 0 64977 29 0 0 25 0 1 0 421364083 39329792 8862 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9602 8862 603 41 0 9561 0
vsize: 38408
[startup+660.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5204
Raw data (stat): 5204 (minisat+) R 5203 32461 32460 0 -1 0 8936 0 0 0 65977 29 0 0 25 0 1 0 421364083 39329792 8862 4294967295 134512640 134672761 3221224560 3221223760 134557828 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9602 8862 603 41 0 9561 0
vsize: 38408
[startup+670.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5204
Raw data (stat): 5204 (minisat+) R 5203 32461 32460 0 -1 0 8936 0 0 0 66977 29 0 0 25 0 1 0 421364083 39329792 8862 4294967295 134512640 134672761 3221224560 3221223728 134561188 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9602 8862 603 41 0 9561 0
vsize: 38408
[startup+680.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5204
Raw data (stat): 5204 (minisat+) R 5203 32461 32460 0 -1 0 8936 0 0 0 67978 29 0 0 25 0 1 0 421364083 39329792 8862 4294967295 134512640 134672761 3221224560 3221223728 134560903 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9602 8862 603 41 0 9561 0
vsize: 38408
[startup+690.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5204
Raw data (stat): 5204 (minisat+) R 5203 32461 32460 0 -1 0 8936 0 0 0 68978 29 0 0 25 0 1 0 421364083 39329792 8862 4294967295 134512640 134672761 3221224560 3221223664 134554642 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9602 8862 603 41 0 9561 0
vsize: 38408
[startup+700.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5204
Raw data (stat): 5204 (minisat+) R 5203 32461 32460 0 -1 0 8936 0 0 0 69977 30 0 0 25 0 1 0 421364083 39329792 8862 4294967295 134512640 134672761 3221224560 3221223728 134560864 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9602 8862 603 41 0 9561 0
vsize: 38408
[startup+710.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5204
Raw data (stat): 5204 (minisat+) R 5203 32461 32460 0 -1 0 8936 0 0 0 70977 30 0 0 25 0 1 0 421364083 39329792 8862 4294967295 134512640 134672761 3221224560 3221223728 134561167 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9602 8862 603 41 0 9561 0
vsize: 38408
[startup+720.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5204
Raw data (stat): 5204 (minisat+) R 5203 32461 32460 0 -1 0 8936 0 0 0 71977 30 0 0 25 0 1 0 421364083 39329792 8862 4294967295 134512640 134672761 3221224560 3221223744 134558662 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9602 8862 603 41 0 9561 0
vsize: 38408
[startup+730.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5204
Raw data (stat): 5204 (minisat+) R 5203 32461 32460 0 -1 0 8936 0 0 0 72978 30 0 0 25 0 1 0 421364083 39329792 8862 4294967295 134512640 134672761 3221224560 3221223728 134560920 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9602 8862 603 41 0 9561 0
vsize: 38408
[startup+740.031 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5204
Raw data (stat): 5204 (minisat+) R 5203 32461 32460 0 -1 0 8936 0 0 0 73978 30 0 0 25 0 1 0 421364083 39329792 8862 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9602 8862 603 41 0 9561 0
vsize: 38408
[startup+750.031 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5204
Raw data (stat): 5204 (minisat+) R 5203 32461 32460 0 -1 0 8936 0 0 0 74978 30 0 0 25 0 1 0 421364083 39329792 8862 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9602 8862 603 41 0 9561 0
vsize: 38408
[startup+760.032 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5204
Raw data (stat): 5204 (minisat+) R 5203 32461 32460 0 -1 0 8936 0 0 0 75978 30 0 0 25 0 1 0 421364083 39329792 8862 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9602 8862 603 41 0 9561 0
vsize: 38408
[startup+770.031 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5204
Raw data (stat): 5204 (minisat+) R 5203 32461 32460 0 -1 0 8936 0 0 0 76978 30 0 0 25 0 1 0 421364083 39329792 8862 4294967295 134512640 134672761 3221224560 3221223708 134560552 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9602 8862 603 41 0 9561 0
vsize: 38408
[startup+780.032 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5204
Raw data (stat): 5204 (minisat+) R 5203 32461 32460 0 -1 0 8936 0 0 0 77979 30 0 0 25 0 1 0 421364083 39329792 8862 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9602 8862 603 41 0 9561 0
vsize: 38408
[startup+790.032 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5204
Raw data (stat): 5204 (minisat+) R 5203 32461 32460 0 -1 0 8936 0 0 0 78979 30 0 0 25 0 1 0 421364083 39329792 8862 4294967295 134512640 134672761 3221224560 3221223728 134560888 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9602 8862 603 41 0 9561 0
vsize: 38408
[startup+800.032 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5204
Raw data (stat): 5204 (minisat+) R 5203 32461 32460 0 -1 0 8936 0 0 0 79978 30 0 0 25 0 1 0 421364083 39329792 8862 4294967295 134512640 134672761 3221224560 3221223728 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9602 8862 603 41 0 9561 0
vsize: 38408
[startup+810.032 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5204
Raw data (stat): 5204 (minisat+) R 5203 32461 32460 0 -1 0 8936 0 0 0 80978 30 0 0 25 0 1 0 421364083 39329792 8862 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9602 8862 603 41 0 9561 0
vsize: 38408
[startup+820.033 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5204
Raw data (stat): 5204 (minisat+) R 5203 32461 32460 0 -1 0 8936 0 0 0 81978 30 0 0 25 0 1 0 421364083 39329792 8862 4294967295 134512640 134672761 3221224560 3221223728 134560909 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9602 8862 603 41 0 9561 0
vsize: 38408
[startup+830.033 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5204
Raw data (stat): 5204 (minisat+) R 5203 32461 32460 0 -1 0 8936 0 0 0 82977 31 0 0 25 0 1 0 421364083 39329792 8862 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9602 8862 603 41 0 9561 0
vsize: 38408
[startup+840.033 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5204
Raw data (stat): 5204 (minisat+) R 5203 32461 32460 0 -1 0 8936 0 0 0 83977 31 0 0 25 0 1 0 421364083 39329792 8862 4294967295 134512640 134672761 3221224560 3221223656 1075347325 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9602 8862 603 41 0 9561 0
vsize: 38408
[startup+850.034 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5204
Raw data (stat): 5204 (minisat+) R 5203 32461 32460 0 -1 0 8936 0 0 0 84976 32 0 0 25 0 1 0 421364083 39329792 8862 4294967295 134512640 134672761 3221224560 3221223728 134560876 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9602 8862 603 41 0 9561 0
vsize: 38408
[startup+860.034 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5204
Raw data (stat): 5204 (minisat+) R 5203 32461 32460 0 -1 0 8936 0 0 0 85976 32 0 0 25 0 1 0 421364083 39329792 8862 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9602 8862 603 41 0 9561 0
vsize: 38408
[startup+870.035 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5204
Raw data (stat): 5204 (minisat+) R 5203 32461 32460 0 -1 0 8937 0 0 0 86976 32 0 0 25 0 1 0 421364083 39329792 8863 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9602 8863 603 41 0 9561 0
vsize: 38408
[startup+880.035 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5204
Raw data (stat): 5204 (minisat+) R 5203 32461 32460 0 -1 0 8937 0 0 0 87976 32 0 0 25 0 1 0 421364083 39329792 8863 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9602 8863 603 41 0 9561 0
vsize: 38408
[startup+890.036 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5204
Raw data (stat): 5204 (minisat+) R 5203 32461 32460 0 -1 0 8937 0 0 0 88975 32 0 0 25 0 1 0 421364083 39329792 8863 4294967295 134512640 134672761 3221224560 3221223728 134560874 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9602 8863 603 41 0 9561 0
vsize: 38408
[startup+900.036 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5204
Raw data (stat): 5204 (minisat+) R 5203 32461 32460 0 -1 0 8937 0 0 0 89975 33 0 0 25 0 1 0 421364083 39329792 8863 4294967295 134512640 134672761 3221224560 3221223696 134565073 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9602 8863 603 41 0 9561 0
vsize: 38408
[startup+910.037 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5204
Raw data (stat): 5204 (minisat+) R 5203 32461 32460 0 -1 0 8937 0 0 0 90974 33 0 0 25 0 1 0 421364083 39329792 8863 4294967295 134512640 134672761 3221224560 3221223728 134561164 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9602 8863 603 41 0 9561 0
vsize: 38408
[startup+920.037 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5204
Raw data (stat): 5204 (minisat+) R 5203 32461 32460 0 -1 0 8937 0 0 0 91974 33 0 0 25 0 1 0 421364083 39329792 8863 4294967295 134512640 134672761 3221224560 3221223728 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9602 8863 603 41 0 9561 0
vsize: 38408
[startup+930.038 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5204
Raw data (stat): 5204 (minisat+) R 5203 32461 32460 0 -1 0 8937 0 0 0 92974 33 0 0 25 0 1 0 421364083 39329792 8863 4294967295 134512640 134672761 3221224560 3221223760 134557852 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9602 8863 603 41 0 9561 0
vsize: 38408
[startup+940.039 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5204
Raw data (stat): 5204 (minisat+) R 5203 32461 32460 0 -1 0 8937 0 0 0 93974 34 0 0 25 0 1 0 421364083 39329792 8863 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9602 8863 603 41 0 9561 0
vsize: 38408
[startup+950.038 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5204
Raw data (stat): 5204 (minisat+) R 5203 32461 32460 0 -1 0 8937 0 0 0 94973 34 0 0 25 0 1 0 421364083 39329792 8863 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9602 8863 603 41 0 9561 0
vsize: 38408
[startup+960.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5204
Raw data (stat): 5204 (minisat+) R 5203 32461 32460 0 -1 0 8937 0 0 0 95973 34 0 0 25 0 1 0 421364083 39329792 8863 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9602 8863 603 41 0 9561 0
vsize: 38408
[startup+970.041 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5204
Raw data (stat): 5204 (minisat+) R 5203 32461 32460 0 -1 0 8937 0 0 0 96973 34 0 0 25 0 1 0 421364083 39329792 8863 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9602 8863 603 41 0 9561 0
vsize: 38408
[startup+980.041 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5204
Raw data (stat): 5204 (minisat+) R 5203 32461 32460 0 -1 0 8937 0 0 0 97973 35 0 0 25 0 1 0 421364083 39329792 8863 4294967295 134512640 134672761 3221224560 3221223728 134560988 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9602 8863 603 41 0 9561 0
vsize: 38408
[startup+990.042 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5204
Raw data (stat): 5204 (minisat+) R 5203 32461 32460 0 -1 0 8937 0 0 0 98972 35 0 0 25 0 1 0 421364083 39329792 8863 4294967295 134512640 134672761 3221224560 3221223728 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9602 8863 603 41 0 9561 0
vsize: 38408
[startup+1000.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5204
Raw data (stat): 5204 (minisat+) R 5203 32461 32460 0 -1 0 8937 0 0 0 99972 35 0 0 25 0 1 0 421364083 39329792 8863 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9602 8863 603 41 0 9561 0
vsize: 38408
[startup+1010.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5204
Raw data (stat): 5204 (minisat+) R 5203 32461 32460 0 -1 0 8937 0 0 0 100971 35 0 0 25 0 1 0 421364083 39329792 8863 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9602 8863 603 41 0 9561 0
vsize: 38408
[startup+1020.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5204
Raw data (stat): 5204 (minisat+) R 5203 32461 32460 0 -1 0 8937 0 0 0 101971 35 0 0 25 0 1 0 421364083 39329792 8863 4294967295 134512640 134672761 3221224560 3221223760 134557911 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9602 8863 603 41 0 9561 0
vsize: 38408
[startup+1030.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5204
Raw data (stat): 5204 (minisat+) R 5203 32461 32460 0 -1 0 8937 0 0 0 102970 36 0 0 25 0 1 0 421364083 39329792 8863 4294967295 134512640 134672761 3221224560 3221223760 134557830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9602 8863 603 41 0 9561 0
vsize: 38408
[startup+1040.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5204
Raw data (stat): 5204 (minisat+) R 5203 32461 32460 0 -1 0 8937 0 0 0 103970 36 0 0 25 0 1 0 421364083 39329792 8863 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9602 8863 603 41 0 9561 0
vsize: 38408
[startup+1050.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5204
Raw data (stat): 5204 (minisat+) R 5203 32461 32460 0 -1 0 8937 0 0 0 104970 36 0 0 25 0 1 0 421364083 39329792 8863 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9602 8863 603 41 0 9561 0
vsize: 38408
[startup+1060.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5204
Raw data (stat): 5204 (minisat+) R 5203 32461 32460 0 -1 0 8937 0 0 0 105969 36 0 0 25 0 1 0 421364083 39329792 8863 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9602 8863 603 41 0 9561 0
vsize: 38408
[startup+1070.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5204
Raw data (stat): 5204 (minisat+) R 5203 32461 32460 0 -1 0 9029 0 0 0 106969 37 0 0 25 0 1 0 421364083 39735296 8955 4294967295 134512640 134672761 3221224560 3221223696 134560729 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9701 8955 603 41 0 9660 0
vsize: 38804
[startup+1080.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5204
Raw data (stat): 5204 (minisat+) R 5203 32461 32460 0 -1 0 9129 0 0 0 107969 37 0 0 25 0 1 0 421364083 40140800 9055 4294967295 134512640 134672761 3221224560 3221223728 134561115 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9800 9055 603 41 0 9759 0
vsize: 39200
[startup+1090.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5204
Raw data (stat): 5204 (minisat+) R 5203 32461 32460 0 -1 0 9232 0 0 0 108968 38 0 0 25 0 1 0 421364083 40542208 9158 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9898 9158 603 41 0 9857 0
vsize: 39592
[startup+1100.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5204
Raw data (stat): 5204 (minisat+) R 5203 32461 32460 0 -1 0 9341 0 0 0 109966 40 0 0 25 0 1 0 421364083 41074688 9267 4294967295 134512640 134672761 3221224560 3221223728 134560903 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10028 9267 603 41 0 9987 0
vsize: 40112
[startup+1110.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5204
Raw data (stat): 5204 (minisat+) R 5203 32461 32460 0 -1 0 9447 0 0 0 110966 40 0 0 25 0 1 0 421364083 41476096 9373 4294967295 134512640 134672761 3221224560 3221223728 134560964 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10126 9373 603 41 0 10085 0
vsize: 40504
[startup+1120.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5204
Raw data (stat): 5204 (minisat+) R 5203 32461 32460 0 -1 0 9544 0 0 0 111966 40 0 0 25 0 1 0 421364083 41877504 9470 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10224 9470 603 41 0 10183 0
vsize: 40896
[startup+1130.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5204
Raw data (stat): 5204 (minisat+) R 5203 32461 32460 0 -1 0 9575 0 0 0 112966 40 0 0 25 0 1 0 421364083 42012672 9501 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10257 9501 603 41 0 10216 0
vsize: 41028
[startup+1140.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5204
Raw data (stat): 5204 (minisat+) R 5203 32461 32460 0 -1 0 9575 0 0 0 113966 40 0 0 25 0 1 0 421364083 42012672 9501 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10257 9501 603 41 0 10216 0
vsize: 41028
[startup+1150.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5204
Raw data (stat): 5204 (minisat+) R 5203 32461 32460 0 -1 0 9575 0 0 0 114966 40 0 0 25 0 1 0 421364083 42012672 9501 4294967295 134512640 134672761 3221224560 3221223760 134557828 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10257 9501 603 41 0 10216 0
vsize: 41028
[startup+1160.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5204
Raw data (stat): 5204 (minisat+) R 5203 32461 32460 0 -1 0 9575 0 0 0 115966 40 0 0 25 0 1 0 421364083 42012672 9501 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10257 9501 603 41 0 10216 0
vsize: 41028
[startup+1170.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5204
Raw data (stat): 5204 (minisat+) R 5203 32461 32460 0 -1 0 9575 0 0 0 116967 40 0 0 25 0 1 0 421364083 42012672 9501 4294967295 134512640 134672761 3221224560 3221223728 134561190 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10257 9501 603 41 0 10216 0
vsize: 41028
[startup+1180.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5204
Raw data (stat): 5204 (minisat+) R 5203 32461 32460 0 -1 0 9575 0 0 0 117967 40 0 0 25 0 1 0 421364083 42012672 9501 4294967295 134512640 134672761 3221224560 3221223664 134560379 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10257 9501 603 41 0 10216 0
vsize: 41028
[startup+1190.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5204
Raw data (stat): 5204 (minisat+) R 5203 32461 32460 0 -1 0 9575 0 0 0 118967 40 0 0 25 0 1 0 421364083 42012672 9501 4294967295 134512640 134672761 3221224560 3221223728 134561215 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10257 9501 603 41 0 10216 0
vsize: 41028
[startup+1200.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5204
Raw data (stat): 5204 (minisat+) R 5203 32461 32460 0 -1 0 9580 0 0 0 119967 40 0 0 25 0 1 0 421364083 42012672 9506 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10257 9506 603 41 0 10216 0
vsize: 41028
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.07 s]
Raw data (loadavg): 0.99 0.97 0.91 1/54 5204
Raw data (stat): 5204 (minisat+) Z 5203 32461 32460 0 -1 12 9583 0 0 0 119967 42 0 0 25 0 1 0 421364083 0 0 4294967295 0 0 0 0 0 0 16384 5 16386 3222412051 0 0 17 1 0 0
Raw data (statm): 0 0 0 0 0 0 0
vsize: 0
Maximum CPU time exceeded: sending SIGTERM and SIGKILL

Child status: 10
Real time (s): 1200.07
CPU time (s): 1200.1
CPU user time (s): 1199.68
CPU system time (s): 0.423935
CPU usage (%): 100.003
Max. virtual memory (Kb): 41028
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####