PB'05 competition: run trace

Some explanations

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

Name	normalized-opb/mps-v2-13-7/ftp.netlib.org/lp/data/normalized-mps-v2-13-7-sierra.opb
MD5SUM	0c242afd458949841d3ea7014466f311
Bench Category	optimization, big integers (OPTBIGINT)
Has Objective Function	YES
Satisfiable	NO
(Un)Satisfiability was proved
Best value of the objective function
Optimality of the best value was proved
Number of terms in the objective function	31139
Biggest coefficient in the objective function	5007894118400
Number of bits for the biggest coefficient in the objective function	43
Sum of the numbers in the objective function	89107300928876
Number of bits of the sum of numbers in the objective function	47
Biggest number in a constraint	5007894118400
Number of bits of the biggest number in a constraint	43
Biggest sum of numbers in a constraint	89107300928876
Number of bits of the biggest sum of numbers	47
Best result obtained on this benchmark	UNSAT
Best CPU time to get the best result obtained on this benchmark	0.282956
Number of variables	32607
Total number of constraints	3263
Number of constraints which are clauses	0
Number of constraints which are cardinality constraints (but not clauses)	0
Number of constraints which are nor clauses,nor cardinality constraints	3263
Minimum length of a constraint	7
Maximum length of a constraint	426
Trace number 31062

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc30 THE 2005-05-25 21:41:23 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=22452 boxname=wulflinc30 idbench=1268 idsolver=15 numberseed=0
MD5SUM SOLVER: 34d34154b8ad81f02ee98439942e0814  /oldhome/oroussel/solvers/minisat+_script
MD5SUM BENCH:  0c242afd458949841d3ea7014466f311  /oldhome/oroussel/tmp/wulflinc30/normalized-mps-v2-13-7-sierra.opb
REAL COMMAND:  minisat+_script /oldhome/oroussel/tmp/wulflinc30/normalized-mps-v2-13-7-sierra.opb
IDLAUNCH: 22452
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.072
cache size	: 512 KB
fdiv_bug	: no
hlt_bug		: no
f00f_bug	: no
coma_bug	: no
fpu		: yes
fpu_exception	: yes
cpuid level	: 2
wp		: yes
flags		: fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse
bogomips	: 888.83

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

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        888840 kB
Buffers:          1832 kB
Cached:         123616 kB
SwapCached:        624 kB
Active:          18592 kB
Inactive:       108808 kB
HighTotal:      131008 kB
HighFree:         4172 kB
LowTotal:       903652 kB
LowFree:        884668 kB
SwapTotal:     2097892 kB
SwapFree:      2096256 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           4948 kB
Slab:            12680 kB
Committed_AS:    63596 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-05-25 22:01:53 (client local time) WITH STATUS 152 IN 1229.93 SECONDS
stats: 22452 7 1229.93 152
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 3761 PB-constraints to clauses...
c   -- Unit propagations: ppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppp
c   -- Detecting intervals from adjacent constraints: ###########################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################
c   -- Clauses(.)/Splits(s): ssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssss
c ---[4574]---> BDD-cost:   20
c ---[4573]---> BDD-cost:   20
c ---[4572]---> BDD-cost:   20
c ---[4564]---> BDD-cost:   20
c ---[4563]---> BDD-cost:   20
c ---[4562]---> BDD-cost:   20
c ---[4555]---> BDD-cost:   18
c ---[4554]---> BDD-cost:   18
c ---[4553]---> BDD-cost:   18
c ---[4552]---> BDD-cost:   18
c ---[4550]---> BDD-cost:   18
c ---[4549]---> BDD-cost:   18
c ---[4548]---> BDD-cost:   18
c ---[4547]---> BDD-cost:   18
c ---[4545]---> BDD-cost:   20
c ---[4544]---> BDD-cost:   20
c ---[4543]---> BDD-cost:   20
c ---[4542]---> BDD-cost:   20
c ---[4536]---> BDD-cost:   18
c ---[4535]---> BDD-cost:   18
c ---[4534]---> BDD-cost:   18
c ---[4533]---> BDD-cost:   18
c ---[4532]---> BDD-cost:   18
c ---[4526]---> BDD-cost:   18
c ---[4525]---> BDD-cost:   18
c ---[4524]---> BDD-cost:   18
c ---[4523]---> BDD-cost:   18
c ---[4522]---> BDD-cost:   18
c ---[4516]---> BDD-cost:   18
c ---[4515]---> BDD-cost:   18
c ---[4514]---> BDD-cost:   18
c ---[4513]---> BDD-cost:   18
c ---[4512]---> BDD-cost:   18
c ---[4505]---> BDD-cost:   20
c ---[4504]---> BDD-cost:   20
c ---[4503]---> BDD-cost:   20
c ---[4502]---> BDD-cost:   20
c ---[4495]---> BDD-cost:   20
c ---[4494]---> BDD-cost:   20
c ---[4493]---> BDD-cost:   20
c ---[4492]---> BDD-cost:   20
c ---[4486]---> BDD-cost:   20
c ---[4485]---> BDD-cost:   20
c ---[4484]---> BDD-cost:   20
c ---[4483]---> BDD-cost:   20
c ---[4482]---> BDD-cost:   20
c ---[4481]---> BDD-cost:   20
c ---[4480]---> BDD-cost:   20
c ---[4479]---> BDD-cost:   20
c ---[4478]---> BDD-cost:   20
c ---[4477]---> BDD-cost:   20
c ---[4471]---> BDD-cost:   20
c ---[4470]---> BDD-cost:   20
c ---[4469]---> BDD-cost:   20
c ---[4468]---> BDD-cost:   20
c ---[4467]---> BDD-cost:   20
c ---[4466]---> BDD-cost:   20
c ---[4465]---> BDD-cost:   20
c ---[4464]---> BDD-cost:   20
c ---[4463]---> BDD-cost:   20
c ---[4462]---> BDD-cost:   20
c ---[4356]---> BDD-cost:   18
c ---[4355]---> BDD-cost:   18
c ---[4354]---> BDD-cost:   18
c ---[4353]---> BDD-cost:   18
c ---[4352]---> BDD-cost:   18
c ---[4351]---> BDD-cost:   18
c ---[4350]---> BDD-cost:   18
c ---[4349]---> BDD-cost:   18
c ---[4348]---> BDD-cost:   18
c ---[4347]---> BDD-cost:   18
c ---[4346]---> BDD-cost:   18
c ---[4345]---> BDD-cost:   18
c ---[4344]---> BDD-cost:   18
c ---[4343]---> BDD-cost:   18
c ---[4342]---> BDD-cost:   18
c ---[4341]---> BDD-cost:   18
c ---[4340]---> BDD-cost:   18
c ---[4339]---> BDD-cost:   18
c ---[4338]---> BDD-cost:   18
c ---[4337]---> BDD-cost:   18
c ---[4336]---> BDD-cost:   18
c ---[4335]---> BDD-cost:   18
c ---[4334]---> BDD-cost:   18
c ---[4333]---> BDD-cost:   18
c ---[4332]---> BDD-cost:   18
c ---[4331]---> BDD-cost:   18
c ---[4330]---> BDD-cost:   18
c ---[4329]---> BDD-cost:   18
c ---[4328]---> BDD-cost:   18
c ---[4327]---> BDD-cost:   18
c ---[4326]---> BDD-cost:   18
c ---[4325]---> BDD-cost:   18
c ---[4324]---> BDD-cost:   18
c ---[4323]---> BDD-cost:   18
c ---[4322]---> BDD-cost:   18
c ---[4321]---> BDD-cost:   18
c ---[4320]---> BDD-cost:   18
c ---[4319]---> BDD-cost:   18
c ---[4318]---> BDD-cost:   18
c ---[4317]---> BDD-cost:   18
c ---[4306]---> BDD-cost:   18
c ---[4305]---> BDD-cost:   18
c ---[4304]---> BDD-cost:   18
c ---[4303]---> BDD-cost:   18
c ---[4302]---> BDD-cost:   18
c ---[4236]---> BDD-cost:   18
c ---[4235]---> BDD-cost:   18
c ---[4234]---> BDD-cost:   18
c ---[4233]---> BDD-cost:   18
c ---[4232]---> BDD-cost:   18
c ---[4226]---> BDD-cost:   18
c ---[4225]---> BDD-cost:   18
c ---[4224]---> BDD-cost:   18
c ---[4223]---> BDD-cost:   18
c ---[4222]---> BDD-cost:   18
c ---[4221]---> BDD-cost:   18
c ---[4220]---> BDD-cost:   18
c ---[4219]---> BDD-cost:   18
c ---[4218]---> BDD-cost:   18
c ---[4217]---> BDD-cost:   18
c ---[4216]---> BDD-cost:   18
c ---[4215]---> BDD-cost:   18
c ---[4214]---> BDD-cost:   18
c ---[4213]---> BDD-cost:   18
c ---[4212]---> BDD-cost:   18
c ---[4211]---> BDD-cost:   18
c ---[4210]---> BDD-cost:   18
c ---[4209]---> BDD-cost:   18
c ---[4208]---> BDD-cost:   18
c ---[4207]---> BDD-cost:   18
c ---[4176]---> BDD-cost:   18
c ---[4175]---> BDD-cost:   18
c ---[4174]---> BDD-cost:   18
c ---[4173]---> BDD-cost:   18
c ---[4172]---> BDD-cost:   18
c ---[4171]---> BDD-cost:   18
c ---[4170]---> BDD-cost:   18
c ---[4169]---> BDD-cost:   18
c ---[4168]---> BDD-cost:   18
c ---[4167]---> BDD-cost:   18
c ---[4166]---> BDD-cost:   18
c ---[4165]---> BDD-cost:   18
c ---[4164]---> BDD-cost:   18
c ---[4163]---> BDD-cost:   18
c ---[4162]---> BDD-cost:   18
c ---[4161]---> BDD-cost:   18
c ---[4160]---> BDD-cost:   18
c ---[4159]---> BDD-cost:   18
c ---[4158]---> BDD-cost:   18
c ---[4157]---> BDD-cost:   18
c ---[4156]---> BDD-cost:   18
c ---[4155]---> BDD-cost:   18
c ---[4154]---> BDD-cost:   18
c ---[4153]---> BDD-cost:   18
c ---[4152]---> BDD-cost:   18
c ---[4151]---> BDD-cost:   18
c ---[4150]---> BDD-cost:   18
c ---[4149]---> BDD-cost:   18
c ---[4148]---> BDD-cost:   18
c ---[4147]---> BDD-cost:   18
c ---[4146]---> BDD-cost:   18
c ---[4145]---> BDD-cost:   18
c ---[4144]---> BDD-cost:   18
c ---[4143]---> BDD-cost:   18
c ---[4142]---> BDD-cost:   18
c ---[4141]---> BDD-cost:   18
c ---[4140]---> BDD-cost:   18
c ---[4139]---> BDD-cost:   18
c ---[4138]---> BDD-cost:   18
c ---[4137]---> BDD-cost:   18
c ---[4136]---> BDD-cost:   18
c ---[4135]---> BDD-cost:   18
c ---[4134]---> BDD-cost:   18
c ---[4133]---> BDD-cost:   18
c ---[4132]---> BDD-cost:   18
c ---[4116]---> BDD-cost:   18
c ---[4115]---> BDD-cost:   18
c ---[4114]---> BDD-cost:   18
c ---[4113]---> BDD-cost:   18
c ---[4112]---> BDD-cost:   18
c ---[4111]---> BDD-cost:   18
c ---[4110]---> BDD-cost:   18
c ---[4109]---> BDD-cost:   18
c ---[4108]---> BDD-cost:   18
c ---[4107]---> BDD-cost:   18
c ---[4066]---> BDD-cost:   18
c ---[4065]---> BDD-cost:   18
c ---[4064]---> BDD-cost:   18
c ---[4063]---> BDD-cost:   18
c ---[4062]---> BDD-cost:   18
c ---[4061]---> BDD-cost:   18
c ---[4060]---> BDD-cost:   18
c ---[4059]---> BDD-cost:   18
c ---[4058]---> BDD-cost:   18
c ---[4057]---> BDD-cost:   18
c ---[4044]---> BDD-cost:   18
c ---[4043]---> BDD-cost:   18
c ---[4042]---> BDD-cost:   18
c ---[3996]---> BDD-cost:    7
c ---[3991]---> BDD-cost:   18
c ---[3990]---> BDD-cost:   18
c ---[3989]---> BDD-cost:   18
c ---[3988]---> BDD-cost:   18
c ---[3987]---> BDD-cost:   18
c ---[3986]---> BDD-cost:   18
c ---[3985]---> BDD-cost:   18
c ---[3984]---> BDD-cost:   18
c ---[3983]---> BDD-cost:   18
c ---[3982]---> BDD-cost:   18
c ---[3981]---> BDD-cost:   18
c ---[3980]---> BDD-cost:   18
c ---[3979]---> BDD-cost:   18
c ---[3978]---> BDD-cost:   18
c ---[3977]---> BDD-cost:   18
c ---[3976]---> BDD-cost:   18
c ---[3975]---> BDD-cost:    7
c ---[3966]---> BDD-cost:   18
c ---[3965]---> BDD-cost:   18
c ---[3964]---> BDD-cost:   18
c ---[3963]---> BDD-cost:   18
c ---[3962]---> BDD-cost:   18
c ---[3961]---> BDD-cost:   18
c ---[3960]---> BDD-cost:   18
c ---[3959]---> BDD-cost:   18
c ---[3958]---> BDD-cost:   18
c ---[3957]---> BDD-cost:   18
c ---[3956]---> BDD-cost:   18
c ---[3955]---> BDD-cost:   18
c ---[3954]---> BDD-cost:    7
c ---[3953]---> BDD-cost:   12
c ---[3952]---> BDD-cost:   12
c ---[3951]---> BDD-cost:   12
c ---[3950]---> BDD-cost:   12
c ---[3933]---> BDD-cost:    7
c ---[3932]---> BDD-cost:   12
c ---[3931]---> BDD-cost:   12
c ---[3930]---> BDD-cost:   12
c ---[3929]---> BDD-cost:   12
c ---[3928]---> BDD-cost:   12
c ---[3927]---> BDD-cost:   12
c ---[3926]---> BDD-cost:   12
c ---[3925]---> BDD-cost:   12
c ---[3912]---> BDD-cost:    7
c ---[3911]---> BDD-cost:   12
c ---[3910]---> BDD-cost:   12
c ---[3909]---> BDD-cost:   12
c ---[3908]---> BDD-cost:   12
c ---[3907]---> BDD-cost:   12
c ---[3906]---> BDD-cost:   12
c ---[3905]---> BDD-cost:   12
c ---[3904]---> BDD-cost:   12
c ---[3903]---> BDD-cost:   12
c ---[3902]---> BDD-cost:   12
c ---[3901]---> BDD-cost:   12
c ---[3900]---> BDD-cost:   12
c ---[3899]---> BDD-cost:   12
c ---[3898]---> BDD-cost:   12
c ---[3897]---> BDD-cost:   12
c ---[3896]---> BDD-cost:   12
c ---[3895]---> BDD-cost:   12
c ---[3894]---> BDD-cost:   12
c ---[3893]---> BDD-cost:   12
c ---[3892]---> BDD-cost:   12
c ---[3891]---> BDD-cost:    7
c ---[3886]---> BDD-cost:   18
c ---[3885]---> BDD-cost:   18
c ---[3884]---> BDD-cost:   18
c ---[3883]---> BDD-cost:   18
c ---[3882]---> BDD-cost:   18
c ---[3881]---> BDD-cost:   18
c ---[3880]---> BDD-cost:   18
c ---[3879]---> BDD-cost:   18
c ---[3878]---> BDD-cost:   18
c ---[3877]---> BDD-cost:   18
c ---[3876]---> BDD-cost:   18
c ---[3875]---> BDD-cost:   18
c ---[3874]---> BDD-cost:   18
c ---[3873]---> BDD-cost:   18
c ---[3872]---> BDD-cost:   18
c ---[3871]---> BDD-cost:   18
c ---[3870]---> BDD-cost:    7
c ---[3861]---> BDD-cost:   18
c ---[3860]---> BDD-cost:   18
c ---[3859]---> BDD-cost:   18
c ---[3858]---> BDD-cost:   18
c ---[3857]---> BDD-cost:   18
c ---[3856]---> BDD-cost:   18
c ---[3855]---> BDD-cost:   18
c ---[3854]---> BDD-cost:   18
c ---[3853]---> BDD-cost:   18
c ---[3852]---> BDD-cost:   18
c ---[3851]---> BDD-cost:   18
c ---[3850]---> BDD-cost:   18
c ---[3849]---> BDD-cost:    7
c ---[3848]---> BDD-cost:   12
c ---[3847]---> BDD-cost:   12
c ---[3846]---> BDD-cost:   12
c ---[3845]---> BDD-cost:   12
c ---[3828]---> BDD-cost:    7
c ---[3827]---> BDD-cost:   12
c ---[3826]---> BDD-cost:   12
c ---[3825]---> BDD-cost:   12
c ---[3824]---> BDD-cost:   12
c ---[3823]---> BDD-cost:   12
c ---[3822]---> BDD-cost:   12
c ---[3821]---> BDD-cost:   12
c ---[3820]---> BDD-cost:   12
c ---[3807]---> BDD-cost:    7
c ---[3806]---> BDD-cost:   12
c ---[3805]---> BDD-cost:   12
c ---[3804]---> BDD-cost:   12
c ---[3803]---> BDD-cost:   12
c ---[3802]---> BDD-cost:   12
c ---[3801]---> BDD-cost:   12
c ---[3800]---> BDD-cost:   12
c ---[3799]---> BDD-cost:   12
c ---[3798]---> BDD-cost:   12
c ---[3797]---> BDD-cost:   12
c ---[3796]---> BDD-cost:   12
c ---[3795]---> BDD-cost:   12
c ---[3794]---> BDD-cost:   12
c ---[3793]---> BDD-cost:   12
c ---[3792]---> BDD-cost:   12
c ---[3791]---> BDD-cost:   12
c ---[3790]---> BDD-cost:   12
c ---[3789]---> BDD-cost:   12
c ---[3788]---> BDD-cost:   12
c ---[3787]---> BDD-cost:   12
c ---[3786]---> BDD-cost:    7
c ---[3765]---> BDD-cost:    7
c ---[3764]---> BDD-cost:   12
c ---[3763]---> BDD-cost:   12
c ---[3762]---> BDD-cost:   12
c ---[3761]---> BDD-cost:   12
c ---[3744]---> BDD-cost:    7
c ---[3743]---> BDD-cost:   12
c ---[3742]---> BDD-cost:   12
c ---[3741]---> BDD-cost:   12
c ---[3740]---> BDD-cost:   12
c ---[3739]---> BDD-cost:   12
c ---[3738]---> BDD-cost:   12
c ---[3737]---> BDD-cost:   12
c ---[3736]---> BDD-cost:   12
c ---[3723]---> BDD-cost:    7
c ---[3722]---> BDD-cost:   12
c ---[3721]---> BDD-cost:   12
c ---[3720]---> BDD-cost:   12
c ---[3719]---> BDD-cost:   12
c ---[3718]---> BDD-cost:   12
c ---[3717]---> BDD-cost:   12
c ---[3716]---> BDD-cost:   12
c ---[3715]---> BDD-cost:   12
c ---[3714]---> BDD-cost:   12
c ---[3713]---> BDD-cost:   12
c ---[3712]---> BDD-cost:   12
c ---[3711]---> BDD-cost:   12
c ---[3710]---> BDD-cost:   12
c ---[3709]---> BDD-cost:   12
c ---[3708]---> BDD-cost:   12
c ---[3707]---> BDD-cost:   12
c ---[3706]---> BDD-cost:   12
c ---[3705]---> BDD-cost:   12
c ---[3704]---> BDD-cost:   12
c ---[3703]---> BDD-cost:   12
c ---[3702]---> BDD-cost:    7
c ---[3681]---> BDD-cost:    7
c ---[3680]---> BDD-cost:   12
c ---[3679]---> BDD-cost:   12
c ---[3678]---> BDD-cost:   12
c ---[3677]---> BDD-cost:   12
c ---[3660]---> BDD-cost:    7
c ---[3659]---> BDD-cost:   12
c ---[3658]---> BDD-cost:   12
c ---[3657]---> BDD-cost:   12
c ---[3656]---> BDD-cost:   12
c ---[3655]---> BDD-cost:   12
c ---[3654]---> BDD-cost:   12
c ---[3653]---> BDD-cost:   12
c ---[3652]---> BDD-cost:   12
c ---[3639]---> BDD-cost:    7
c ---[3638]---> BDD-cost:   12
c ---[3637]---> BDD-cost:   12
c ---[3636]---> BDD-cost:   12
c ---[3635]---> BDD-cost:   12
c ---[3634]---> BDD-cost:   12
c ---[3633]---> BDD-cost:   12
c ---[3632]---> BDD-cost:   12
c ---[3631]---> BDD-cost:   12
c ---[3630]---> BDD-cost:   12
c ---[3629]---> BDD-cost:   12
c ---[3628]---> BDD-cost:   12
c ---[3627]---> BDD-cost:   12
c ---[3626]---> BDD-cost:   12
c ---[3625]---> BDD-cost:   12
c ---[3624]---> BDD-cost:   12
c ---[3623]---> BDD-cost:   12
c ---[3622]---> BDD-cost:   12
c ---[3621]---> BDD-cost:   12
c ---[3620]---> BDD-cost:   12
c ---[3619]---> BDD-cost:   12
c ---[3618]---> BDD-cost:    7
c ---[3597]---> BDD-cost:    7
c ---[3596]---> BDD-cost:   12
c ---[3595]---> BDD-cost:   12
c ---[3594]---> BDD-cost:   12
c ---[3593]---> BDD-cost:   12
c ---[3576]---> BDD-cost:    7
c ---[3575]---> BDD-cost:   12
c ---[3574]---> BDD-cost:   12
c ---[3573]---> BDD-cost:   12
c ---[3572]---> BDD-cost:   12
c ---[3571]---> BDD-cost:   12
c ---[3570]---> BDD-cost:   12
c ---[3569]---> BDD-cost:   12
c ---[3568]---> BDD-cost:   12
c ---[3555]---> BDD-cost:    7
c ---[3554]---> BDD-cost:   12
c ---[3553]---> BDD-cost:   12
c ---[3552]---> BDD-cost:   12
c ---[3551]---> BDD-cost:   12
c ---[3550]---> BDD-cost:   12
c ---[3549]---> BDD-cost:   12
c ---[3548]---> BDD-cost:   12
c ---[3547]---> BDD-cost:   12
c ---[3546]---> BDD-cost:   12
c ---[3545]---> BDD-cost:   12
c ---[3544]---> BDD-cost:   12
c ---[3543]---> BDD-cost:   12
c ---[3542]---> BDD-cost:   12
c ---[3541]---> BDD-cost:   12
c ---[3540]---> BDD-cost:   12
c ---[3539]---> BDD-cost:   12
c ---[3538]---> BDD-cost:   12
c ---[3537]---> BDD-cost:   12
c ---[3536]---> BDD-cost:   12
c ---[3535]---> BDD-cost:   12
c ---[3534]---> BDD-cost:    7
c ---[3533]---> BDD-cost:   18
c ---[3532]---> BDD-cost:   18
c ---[3531]---> BDD-cost:   18
c ---[3530]---> BDD-cost:   18
c ---[3529]---> BDD-cost:   18
c ---[3528]---> BDD-cost:   18
c ---[3527]---> BDD-cost:   18
c ---[3526]---> BDD-cost:   18
c ---[3525]---> BDD-cost:   18
c ---[3524]---> BDD-cost:   18
c ---[3523]---> BDD-cost:   18
c ---[3522]---> BDD-cost:   18
c ---[3521]---> BDD-cost:   18
c ---[3520]---> BDD-cost:   18
c ---[3519]---> BDD-cost:   18
c ---[3518]---> BDD-cost:   18
c ---[3517]---> BDD-cost:   18
c ---[3516]---> BDD-cost:   18
c ---[3515]---> BDD-cost:   18
c ---[3514]---> BDD-cost:   18
c ---[3513]---> BDD-cost:    7
c ---[3508]---> BDD-cost:   18
c ---[3507]---> BDD-cost:   18
c ---[3506]---> BDD-cost:   18
c ---[3505]---> BDD-cost:   18
c ---[3504]---> BDD-cost:   18
c ---[3503]---> BDD-cost:   18
c ---[3502]---> BDD-cost:   18
c ---[3501]---> BDD-cost:   18
c ---[3500]---> BDD-cost:   18
c ---[3499]---> BDD-cost:   18
c ---[3498]---> BDD-cost:   18
c ---[3497]---> BDD-cost:   18
c ---[3496]---> BDD-cost:   18
c ---[3495]---> BDD-cost:   18
c ---[3494]---> BDD-cost:   18
c ---[3493]---> BDD-cost:   18
c ---[3492]---> BDD-cost:    7
c ---[3483]---> BDD-cost:   18
c ---[3482]---> BDD-cost:   18
c ---[3481]---> BDD-cost:   18
c ---[3480]---> BDD-cost:   18
c ---[3479]---> BDD-cost:   18
c ---[3478]---> BDD-cost:   18
c ---[3477]---> BDD-cost:   18
c ---[3476]---> BDD-cost:   18
c ---[3475]---> BDD-cost:   18
c ---[3474]---> BDD-cost:   18
c ---[3473]---> BDD-cost:   18
c ---[3472]---> BDD-cost:   18
c ---[3471]---> BDD-cost:    7
c ---[3450]---> BDD-cost:    7
c ---[3449]---> BDD-cost:   18
c ---[3448]---> BDD-cost:   18
c ---[3447]---> BDD-cost:   18
c ---[3446]---> BDD-cost:   18
c ---[3445]---> BDD-cost:   18
c ---[3444]---> BDD-cost:   18
c ---[3443]---> BDD-cost:   18
c ---[3442]---> BDD-cost:   18
c ---[3441]---> BDD-cost:   18
c ---[3440]---> BDD-cost:   18
c ---[3439]---> BDD-cost:   18
c ---[3438]---> BDD-cost:   18
c ---[3437]---> BDD-cost:   18
c ---[3436]---> BDD-cost:   18
c ---[3435]---> BDD-cost:   18
c ---[3434]---> BDD-cost:   18
c ---[3433]---> BDD-cost:   18
c ---[3432]---> BDD-cost:   18
c ---[3431]---> BDD-cost:   18
c ---[3430]---> BDD-cost:   18
c ---[3429]---> BDD-cost:    7
c ---[3424]---> BDD-cost:   18
c ---[3423]---> BDD-cost:   18
c ---[3422]---> BDD-cost:   18
c ---[3421]---> BDD-cost:   18
c ---[3420]---> BDD-cost:   18
c ---[3419]---> BDD-cost:   18
c ---[3418]---> BDD-cost:   18
c ---[3417]---> BDD-cost:   18
c ---[3416]---> BDD-cost:   18
c ---[3415]---> BDD-cost:   18
c ---[3414]---> BDD-cost:   18
c ---[3413]---> BDD-cost:   18
c ---[3412]---> BDD-cost:   18
c ---[3411]---> BDD-cost:   18
c ---[3410]---> BDD-cost:   18
c ---[3409]---> BDD-cost:   18
c ---[3408]---> BDD-cost:    7
c ---[3399]---> BDD-cost:   18
c ---[3398]---> BDD-cost:   18
c ---[3397]---> BDD-cost:   18
c ---[3396]---> BDD-cost:   18
c ---[3395]---> BDD-cost:   18
c ---[3394]---> BDD-cost:   18
c ---[3393]---> BDD-cost:   18
c ---[3392]---> BDD-cost:   18
c ---[3391]---> BDD-cost:   18
c ---[3390]---> BDD-cost:   18
c ---[3389]---> BDD-cost:   18
c ---[3388]---> BDD-cost:   18
c ---[3387]---> BDD-cost:    7
c ---[3366]---> BDD-cost:    7
c ---[3365]---> BDD-cost:   18
c ---[3364]---> BDD-cost:   18
c ---[3363]---> BDD-cost:   18
c ---[3362]---> BDD-cost:   18
c ---[3361]---> BDD-cost:   18
c ---[3360]---> BDD-cost:   18
c ---[3359]---> BDD-cost:   18
c ---[3358]---> BDD-cost:   18
c ---[3357]---> BDD-cost:   18
c ---[3356]---> BDD-cost:   18
c ---[3355]---> BDD-cost:   18
c ---[3354]---> BDD-cost:   18
c ---[3353]---> BDD-cost:   18
c ---[3352]---> BDD-cost:   18
c ---[3351]---> BDD-cost:   18
c ---[3350]---> BDD-cost:   18
c ---[3349]---> BDD-cost:   18
c ---[3348]---> BDD-cost:   18
c ---[3347]---> BDD-cost:   18
c ---[3346]---> BDD-cost:   18
c ---[3345]---> BDD-cost:    7
c ---[3340]---> BDD-cost:   18
c ---[3339]---> BDD-cost:   18
c ---[3338]---> BDD-cost:   18
c ---[3337]---> BDD-cost:   18
c ---[3336]---> BDD-cost:   18
c ---[3335]---> BDD-cost:   18
c ---[3334]---> BDD-cost:   18
c ---[3333]---> BDD-cost:   18
c ---[3332]---> BDD-cost:   18
c ---[3331]---> BDD-cost:   18
c ---[3330]---> BDD-cost:   18
c ---[3329]---> BDD-cost:   18
c ---[3328]---> BDD-cost:   18
c ---[3327]---> BDD-cost:   18
c ---[3326]---> BDD-cost:   18
c ---[3325]---> BDD-cost:   18
c ---[3324]---> BDD-cost:    7
c ---[3315]---> BDD-cost:   18
c ---[3314]---> BDD-cost:   18
c ---[3313]---> BDD-cost:   18
c ---[3312]---> BDD-cost:   18
c ---[3311]---> BDD-cost:   18
c ---[3310]---> BDD-cost:   18
c ---[3309]---> BDD-cost:   18
c ---[3308]---> BDD-cost:   18
c ---[3307]---> BDD-cost:   18
c ---[3306]---> BDD-cost:   18
c ---[3305]---> BDD-cost:   18
c ---[3304]---> BDD-cost:   18
c ---[3303]---> BDD-cost:    7
c ---[3282]---> BDD-cost:    7
c ---[3281]---> BDD-cost:   18
c ---[3280]---> BDD-cost:   18
c ---[3279]---> BDD-cost:   18
c ---[3278]---> BDD-cost:   18
c ---[3277]---> BDD-cost:   18
c ---[3276]---> BDD-cost:   18
c ---[3275]---> BDD-cost:   18
c ---[3274]---> BDD-cost:   18
c ---[3273]---> BDD-cost:   18
c ---[3272]---> BDD-cost:   18
c ---[3271]---> BDD-cost:   18
c ---[3270]---> BDD-cost:   18
c ---[3269]---> BDD-cost:   18
c ---[3268]---> BDD-cost:   18
c ---[3267]---> BDD-cost:   18
c ---[3266]---> BDD-cost:   18
c ---[3265]---> BDD-cost:   18
c ---[3264]---> BDD-cost:   18
c ---[3263]---> BDD-cost:   18
c ---[3262]---> BDD-cost:   18
c ---[3261]---> BDD-cost:    7
c ---[3256]---> BDD-cost:   18
c ---[3255]---> BDD-cost:   18
c ---[3254]---> BDD-cost:   18
c ---[3253]---> BDD-cost:   18
c ---[3252]---> BDD-cost:   18
c ---[3251]---> BDD-cost:   18
c ---[3250]---> BDD-cost:   18
c ---[3249]---> BDD-cost:   18
c ---[3248]---> BDD-cost:   18
c ---[3247]---> BDD-cost:   18
c ---[3246]---> BDD-cost:   18
c ---[3245]---> BDD-cost:   18
c ---[3244]---> BDD-cost:   18
c ---[3243]---> BDD-cost:   18
c ---[3242]---> BDD-cost:   18
c ---[3241]---> BDD-cost:   18
c ---[3240]---> BDD-cost:    7
c ---[3231]---> BDD-cost:   18
c ---[3230]---> BDD-cost:   18
c ---[3229]---> BDD-cost:   18
c ---[3228]---> BDD-cost:   18
c ---[3227]---> BDD-cost:   18
c ---[3226]---> BDD-cost:   18
c ---[3225]---> BDD-cost:   18
c ---[3224]---> BDD-cost:   18
c ---[3223]---> BDD-cost:   18
c ---[3222]---> BDD-cost:   18
c ---[3221]---> BDD-cost:   18
c ---[3220]---> BDD-cost:   18
c ---[3219]---> BDD-cost:    7
c ---[3198]---> BDD-cost:    7
c ---[3197]---> BDD-cost:   18
c ---[3196]---> BDD-cost:   18
c ---[3195]---> BDD-cost:   18
c ---[3194]---> BDD-cost:   18
c ---[3193]---> BDD-cost:   18
c ---[3192]---> BDD-cost:   18
c ---[3191]---> BDD-cost:   18
c ---[3190]---> BDD-cost:   18
c ---[3189]---> BDD-cost:   18
c ---[3188]---> BDD-cost:   18
c ---[3187]---> BDD-cost:   18
c ---[3186]---> BDD-cost:   18
c ---[3185]---> BDD-cost:   18
c ---[3184]---> BDD-cost:   18
c ---[3183]---> BDD-cost:   18
c ---[3182]---> BDD-cost:   18
c ---[3181]---> BDD-cost:   18
c ---[3180]---> BDD-cost:   18
c ---[3179]---> BDD-cost:   18
c ---[3178]---> BDD-cost:   18
c ---[3177]---> BDD-cost:    7
c ---[3172]---> BDD-cost:   18
c ---[3171]---> BDD-cost:   18
c ---[3170]---> BDD-cost:   18
c ---[3169]---> BDD-cost:   18
c ---[3168]---> BDD-cost:   18
c ---[3167]---> BDD-cost:   18
c ---[3166]---> BDD-cost:   18
c ---[3165]---> BDD-cost:   18
c ---[3164]---> BDD-cost:   18
c ---[3163]---> BDD-cost:   18
c ---[3162]---> BDD-cost:   18
c ---[3161]---> BDD-cost:   18
c ---[3160]---> BDD-cost:   18
c ---[3159]---> BDD-cost:   18
c ---[3158]---> BDD-cost:   18
c ---[3157]---> BDD-cost:   18
c ---[3156]---> BDD-cost:    7
c ---[3147]---> BDD-cost:   18
c ---[3146]---> BDD-cost:   18
c ---[3145]---> BDD-cost:   18
c ---[3144]---> BDD-cost:   18
c ---[3143]---> BDD-cost:   18
c ---[3142]---> BDD-cost:   18
c ---[3141]---> BDD-cost:   18
c ---[3140]---> BDD-cost:   18
c ---[3139]---> BDD-cost:   18
c ---[3138]---> BDD-cost:   18
c ---[3137]---> BDD-cost:   18
c ---[3136]---> BDD-cost:   18
c ---[3135]---> BDD-cost:    7
c ---[3114]---> BDD-cost:    7
c ---[3113]---> BDD-cost:   18
c ---[3112]---> BDD-cost:   18
c ---[3111]---> BDD-cost:   18
c ---[3110]---> BDD-cost:   18
c ---[3109]---> BDD-cost:   18
c ---[3108]---> BDD-cost:   18
c ---[3107]---> BDD-cost:   18
c ---[3106]---> BDD-cost:   18
c ---[3105]---> BDD-cost:   18
c ---[3104]---> BDD-cost:   18
c ---[3103]---> BDD-cost:   18
c ---[3102]---> BDD-cost:   18
c ---[3101]---> BDD-cost:   18
c ---[3100]---> BDD-cost:   18
c ---[3099]---> BDD-cost:   18
c ---[3098]---> BDD-cost:   18
c ---[3097]---> BDD-cost:   18
c ---[3096]---> BDD-cost:   18
c ---[3095]---> BDD-cost:   18
c ---[3094]---> BDD-cost:   18
c ---[3093]---> BDD-cost:    7
c ---[3088]---> BDD-cost:   18
c ---[3087]---> BDD-cost:   18
c ---[3086]---> BDD-cost:   18
c ---[3085]---> BDD-cost:   18
c ---[3084]---> BDD-cost:   18
c ---[3083]---> BDD-cost:   18
c ---[3082]---> BDD-cost:   18
c ---[3081]---> BDD-cost:   18
c ---[3080]---> BDD-cost:   18
c ---[3079]---> BDD-cost:   18
c ---[3078]---> BDD-cost:   18
c ---[3077]---> BDD-cost:   18
c ---[3076]---> BDD-cost:   18
c ---[3075]---> BDD-cost:   18
c ---[3074]---> BDD-cost:   18
c ---[3073]---> BDD-cost:   18
c ---[3072]---> BDD-cost:    7
c ---[3063]---> BDD-cost:   18
c ---[3062]---> BDD-cost:   18
c ---[3061]---> BDD-cost:   18
c ---[3060]---> BDD-cost:   18
c ---[3059]---> BDD-cost:   18
c ---[3058]---> BDD-cost:   18
c ---[3057]---> BDD-cost:   18
c ---[3056]---> BDD-cost:   18
c ---[3055]---> BDD-cost:   18
c ---[3054]---> BDD-cost:   18
c ---[3053]---> BDD-cost:   18
c ---[3052]---> BDD-cost:   18
c ---[3051]---> BDD-cost:    7
c ---[3030]---> BDD-cost:    7
c ---[3009]---> BDD-cost:    7
c ---[3008]---> BDD-cost:   12
c ---[3007]---> BDD-cost:   12
c ---[3006]---> BDD-cost:   12
c ---[3005]---> BDD-cost:   12
c ---[2988]---> BDD-cost:    7
c ---[2987]---> BDD-cost:   12
c ---[2986]---> BDD-cost:   12
c ---[2985]---> BDD-cost:   12
c ---[2984]---> BDD-cost:   12
c ---[2983]---> BDD-cost:   12
c ---[2982]---> BDD-cost:   12
c ---[2981]---> BDD-cost:   12
c ---[2980]---> BDD-cost:   12
c ---[2967]---> BDD-cost:    7
c ---[2966]---> BDD-cost:   12
c ---[2965]---> BDD-cost:   12
c ---[2964]---> BDD-cost:   12
c ---[2963]---> BDD-cost:   12
c ---[2962]---> BDD-cost:   12
c ---[2961]---> BDD-cost:   12
c ---[2960]---> BDD-cost:   12
c ---[2959]---> BDD-cost:   12
c ---[2958]---> BDD-cost:   12
c ---[2957]---> BDD-cost:   12
c ---[2956]---> BDD-cost:   12
c ---[2955]---> BDD-cost:   12
c ---[2954]---> BDD-cost:   12
c ---[2953]---> BDD-cost:   12
c ---[2952]---> BDD-cost:   12
c ---[2951]---> BDD-cost:   12
c ---[2950]---> BDD-cost:   12
c ---[2949]---> BDD-cost:   12
c ---[2948]---> BDD-cost:   12
c ---[2947]---> BDD-cost:   12
c ---[2946]---> BDD-cost:    7
c ---[2945]---> BDD-cost:   18
c ---[2944]---> BDD-cost:   18
c ---[2943]---> BDD-cost:   18
c ---[2942]---> BDD-cost:   18
c ---[2941]---> BDD-cost:   18
c ---[2940]---> BDD-cost:   18
c ---[2939]---> BDD-cost:   18
c ---[2938]---> BDD-cost:   18
c ---[2937]---> BDD-cost:   18
c ---[2936]---> BDD-cost:   18
c ---[2935]---> BDD-cost:   18
c ---[2934]---> BDD-cost:   18
c ---[2933]---> BDD-cost:   18
c ---[2932]---> BDD-cost:   18
c ---[2931]---> BDD-cost:   18
c ---[2930]---> BDD-cost:   18
c ---[2929]---> BDD-cost:   18
c ---[2928]---> BDD-cost:   18
c ---[2927]---> BDD-cost:   18
c ---[2926]---> BDD-cost:   18
c ---[2925]---> BDD-cost:    7
c ---[2920]---> BDD-cost:   18
c ---[2919]---> BDD-cost:   18
c ---[2918]---> BDD-cost:   18
c ---[2917]---> BDD-cost:   18
c ---[2916]---> BDD-cost:   18
c ---[2915]---> BDD-cost:   18
c ---[2914]---> BDD-cost:   18
c ---[2913]---> BDD-cost:   18
c ---[2912]---> BDD-cost:   18
c ---[2911]---> BDD-cost:   18
c ---[2910]---> BDD-cost:   18
c ---[2909]---> BDD-cost:   18
c ---[2908]---> BDD-cost:   18
c ---[2907]---> BDD-cost:   18
c ---[2906]---> BDD-cost:   18
c ---[2905]---> BDD-cost:   18
c ---[2904]---> BDD-cost:    7
c ---[2895]---> BDD-cost:   18
c ---[2894]---> BDD-cost:   18
c ---[2893]---> BDD-cost:   18
c ---[2892]---> BDD-cost:   18
c ---[2891]---> BDD-cost:   18
c ---[2890]---> BDD-cost:   18
c ---[2889]---> BDD-cost:   18
c ---[2888]---> BDD-cost:   18
c ---[2887]---> BDD-cost:   18
c ---[2886]---> BDD-cost:   18
c ---[2885]---> BDD-cost:   18
c ---[2884]---> BDD-cost:   18
c ---[2883]---> BDD-cost:    7
c ---[2862]---> BDD-cost:    7
c ---[2861]---> BDD-cost:   18
c ---[2860]---> BDD-cost:   18
c ---[2859]---> BDD-cost:   18
c ---[2858]---> BDD-cost:   18
c ---[2857]---> BDD-cost:   18
c ---[2856]---> BDD-cost:   18
c ---[2855]---> BDD-cost:   18
c ---[2854]---> BDD-cost:   18
c ---[2853]---> BDD-cost:   18
c ---[2852]---> BDD-cost:   18
c ---[2851]---> BDD-cost:   18
c ---[2850]---> BDD-cost:   18
c ---[2849]---> BDD-cost:   18
c ---[2848]---> BDD-cost:   18
c ---[2847]---> BDD-cost:   18
c ---[2846]---> BDD-cost:   18
c ---[2845]---> BDD-cost:   18
c ---[2844]---> BDD-cost:   18
c ---[2843]---> BDD-cost:   18
c ---[2842]---> BDD-cost:   18
c ---[2841]---> BDD-cost:    7
c ---[2836]---> BDD-cost:   18
c ---[2835]---> BDD-cost:   18
c ---[2834]---> BDD-cost:   18
c ---[2833]---> BDD-cost:   18
c ---[2832]---> BDD-cost:   18
c ---[2831]---> BDD-cost:   18
c ---[2830]---> BDD-cost:   18
c ---[2829]---> BDD-cost:   18
c ---[2828]---> BDD-cost:   18
c ---[2827]---> BDD-cost:   18
c ---[2826]---> BDD-cost:   18
c ---[2825]---> BDD-cost:   18
c ---[2824]---> BDD-cost:   18
c ---[2823]---> BDD-cost:   18
c ---[2822]---> BDD-cost:   18
c ---[2821]---> BDD-cost:   18
c ---[2820]---> BDD-cost:    7
c ---[2811]---> BDD-cost:   18
c ---[2810]---> BDD-cost:   18
c ---[2809]---> BDD-cost:   18
c ---[2808]---> BDD-cost:   18
c ---[2807]---> BDD-cost:   18
c ---[2806]---> BDD-cost:   18
c ---[2805]---> BDD-cost:   18
c ---[2804]---> BDD-cost:   18
c ---[2803]---> BDD-cost:   18
c ---[2802]---> BDD-cost:   18
c ---[2801]---> BDD-cost:   18
c ---[2800]---> BDD-cost:   18
c ---[2799]---> BDD-cost:    7
c ---[2778]---> BDD-cost:    7
c ---[2757]---> BDD-cost:    7
c ---[2756]---> BDD-cost:   12
c ---[2755]---> BDD-cost:   12
c ---[2754]---> BDD-cost:   12
c ---[2753]---> BDD-cost:   12
c ---[2736]---> BDD-cost:    7
c ---[2735]---> BDD-cost:   12
c ---[2734]---> BDD-cost:   12
c ---[2733]---> BDD-cost:   12
c ---[2732]---> BDD-cost:   12
c ---[2731]---> BDD-cost:   12
c ---[2730]---> BDD-cost:   12
c ---[2729]---> BDD-cost:   12
c ---[2728]---> BDD-cost:   12
c ---[2715]---> BDD-cost:    7
c ---[2714]---> BDD-cost:   12
c ---[2713]---> BDD-cost:   12
c ---[2712]---> BDD-cost:   12
c ---[2711]---> BDD-cost:   12
c ---[2710]---> BDD-cost:   12
c ---[2709]---> BDD-cost:   12
c ---[2708]---> BDD-cost:   12
c ---[2707]---> BDD-cost:   12
c ---[2706]---> BDD-cost:   12
c ---[2705]---> BDD-cost:   12
c ---[2704]---> BDD-cost:   12
c ---[2703]---> BDD-cost:   12
c ---[2702]---> BDD-cost:   12
c ---[2701]---> BDD-cost:   12
c ---[2700]---> BDD-cost:   12
c ---[2699]---> BDD-cost:   12
c ---[2698]---> BDD-cost:   12
c ---[2697]---> BDD-cost:   12
c ---[2696]---> BDD-cost:   12
c ---[2695]---> BDD-cost:   12
c ---[2694]---> BDD-cost:    7
c ---[2673]---> BDD-cost:    7
c ---[2672]---> BDD-cost:   12
c ---[2671]---> BDD-cost:   12
c ---[2670]---> BDD-cost:   12
c ---[2669]---> BDD-cost:   12
c ---[2652]---> BDD-cost:    7
c ---[2651]---> BDD-cost:   12
c ---[2650]---> BDD-cost:   12
c ---[2649]---> BDD-cost:   12
c ---[2648]---> BDD-cost:   12
c ---[2647]---> BDD-cost:   12
c ---[2646]---> BDD-cost:   12
c ---[2645]---> BDD-cost:   12
c ---[2644]---> BDD-cost:   12
c ---[2631]---> BDD-cost:    7
c ---[2630]---> BDD-cost:   12
c ---[2629]---> BDD-cost:   12
c ---[2628]---> BDD-cost:   12
c ---[2627]---> BDD-cost:   12
c ---[2626]---> BDD-cost:   12
c ---[2625]---> BDD-cost:   12
c ---[2624]---> BDD-cost:   12
c ---[2623]---> BDD-cost:   12
c ---[2622]---> BDD-cost:   12
c ---[2621]---> BDD-cost:   12
c ---[2620]---> BDD-cost:   12
c ---[2619]---> BDD-cost:   12
c ---[2618]---> BDD-cost:   12
c ---[2617]---> BDD-cost:   12
c ---[2616]---> BDD-cost:   12
c ---[2615]---> BDD-cost:   12
c ---[2614]---> BDD-cost:   12
c ---[2613]---> BDD-cost:   12
c ---[2612]---> BDD-cost:   12
c ---[2611]---> BDD-cost:   12
c ---[2609]---> BDD-cost:   76
c ---[2608]---> BDD-cost:   90
c ---[2607]---> BDD-cost:   90
c ---[2606]---> BDD-cost:   90
c ---[2604]---> BDD-cost:   76
c ---[2603]---> BDD-cost:   90
c ---[2602]---> BDD-cost:   90
c ---[2601]---> BDD-cost:   90
c ---[2599]---> BDD-cost:   88
c ---[2598]---> BDD-cost:   88
c ---[2597]---> BDD-cost:   88
c ---[2596]---> BDD-cost:   88
c ---[2594]---> BDD-cost:   84
c ---[2593]---> BDD-cost:   84
c ---[2592]---> BDD-cost:   84
c ---[2591]---> BDD-cost:   84
c ---[2590]---> BDD-cost:   83
c ---[2589]---> BDD-cost:   83
c ---[2588]---> BDD-cost:   83
c ---[2587]---> BDD-cost:   83
c ---[2586]---> BDD-cost:   83
c ---[2585]---> BDD-cost:   86
c ---[2584]---> BDD-cost:   86
c ---[2583]---> BDD-cost:   86
c ---[2582]---> BDD-cost:   86
c ---[2581]---> BDD-cost:   86
c ---[2580]---> BDD-cost:   83
c ---[2579]---> BDD-cost:   83
c ---[2578]---> BDD-cost:   83
c ---[2577]---> BDD-cost:   83
c ---[2576]---> BDD-cost:   83
c ---[2574]---> BDD-cost:   84
c ---[2573]---> BDD-cost:   84
c ---[2572]---> BDD-cost:   84
c ---[2571]---> BDD-cost:   84
c ---[2569]---> BDD-cost:   84
c ---[2568]---> BDD-cost:   84
c ---[2567]---> BDD-cost:   84
c ---[2566]---> BDD-cost:   84
c ---[2565]---> BDD-cost:   98
c ---[2564]---> BDD-cost:   98
c ---[2563]---> BDD-cost:   98
c ---[2562]---> BDD-cost:   98
c ---[2561]---> BDD-cost:   98
c ---[2555]---> BDD-cost:   98
c ---[2554]---> BDD-cost:   98
c ---[2553]---> BDD-cost:   98
c ---[2552]---> BDD-cost:   98
c ---[2551]---> BDD-cost:   98
c ---[2520]---> BDD-cost:   63
c ---[2519]---> BDD-cost:   63
c ---[2518]---> BDD-cost:   63
c ---[2517]---> BDD-cost:   63
c ---[2516]---> BDD-cost:   63
c ---[2515]---> BDD-cost:   63
c ---[2514]---> BDD-cost:   63
c ---[2513]---> BDD-cost:   63
c ---[2512]---> BDD-cost:   63
c ---[2511]---> BDD-cost:   63
c ---[2510]---> BDD-cost:   63
c ---[2509]---> BDD-cost:   63
c ---[2508]---> BDD-cost:   63
c ---[2507]---> BDD-cost:   63
c ---[2506]---> BDD-cost:   63
c ---[2505]---> BDD-cost:   63
c ---[2504]---> BDD-cost:   63
c ---[2503]---> BDD-cost:   63
c ---[2502]---> BDD-cost:   63
c ---[2501]---> BDD-cost:   63
c ---[2500]---> BDD-cost:   63
c ---[2499]---> BDD-cost:   63
c ---[2498]---> BDD-cost:   63
c ---[2497]---> BDD-cost:   63
c ---[2496]---> BDD-cost:   63
c ---[2495]---> BDD-cost:   88
c ---[2494]---> BDD-cost:   88
c ---[2493]---> BDD-cost:   88
c ---[2492]---> BDD-cost:   88
c ---[2491]---> BDD-cost:   88
c ---[2490]---> BDD-cost:   88
c ---[2489]---> BDD-cost:   88
c ---[2488]---> BDD-cost:   88
c ---[2487]---> BDD-cost:   88
c ---[2486]---> BDD-cost:   88
c ---[2485]---> BDD-cost:   88
c ---[2484]---> BDD-cost:   88
c ---[2483]---> BDD-cost:   88
c ---[2482]---> BDD-cost:   88
c ---[2481]---> BDD-cost:   88
c ---[2480]---> BDD-cost:   88
c ---[2479]---> BDD-cost:   88
c ---[2478]---> BDD-cost:   88
c ---[2477]---> BDD-cost:   88
c ---[2476]---> BDD-cost:   88
c ---[2475]---> BDD-cost:   63
c ---[2474]---> BDD-cost:   63
c ---[2473]---> BDD-cost:   63
c ---[2470]---> BDD-cost:   78
c ---[2469]---> BDD-cost:   78
c ---[2468]---> BDD-cost:   78
c ---[2467]---> BDD-cost:   78
c ---[2466]---> BDD-cost:   78
c ---[2460]---> BDD-cost:   63
c ---[2459]---> BDD-cost:   63
c ---[2458]---> BDD-cost:   63
c ---[2457]---> BDD-cost:   63
c ---[2456]---> BDD-cost:   63
c ---[2455]---> BDD-cost:   63
c ---[2454]---> BDD-cost:   63
c ---[2453]---> BDD-cost:   63
c ---[2452]---> BDD-cost:   63
c ---[2451]---> BDD-cost:   63
c ---[2450]---> BDD-cost:   63
c ---[2449]---> BDD-cost:   63
c ---[2448]---> BDD-cost:   63
c ---[2447]---> BDD-cost:   63
c ---[2446]---> BDD-cost:   63
c ---[2445]---> BDD-cost:   63
c ---[2444]---> BDD-cost:   63
c ---[2443]---> BDD-cost:   63
c ---[2442]---> BDD-cost:   63
c ---[2441]---> BDD-cost:   63
c ---[2440]---> BDD-cost:   63
c ---[2439]---> BDD-cost:   63
c ---[2438]---> BDD-cost:   63
c ---[2437]---> BDD-cost:   63
c ---[2436]---> BDD-cost:   63
c ---[2435]---> BDD-cost:   83
c ---[2434]---> BDD-cost:   83
c ---[2433]---> BDD-cost:   83
c ---[2432]---> BDD-cost:   83
c ---[2431]---> BDD-cost:   83
c ---[2430]---> BDD-cost:   88
c ---[2429]---> BDD-cost:   88
c ---[2428]---> BDD-cost:   88
c ---[2427]---> BDD-cost:   88
c ---[2426]---> BDD-cost:   88
c ---[2425]---> BDD-cost:   88
c ---[2424]---> BDD-cost:   88
c ---[2423]---> BDD-cost:   88
c ---[2422]---> BDD-cost:   88
c ---[2421]---> BDD-cost:   88
c ---[2420]---> BDD-cost:   63
c ---[2419]---> BDD-cost:   63
c ---[2418]---> BDD-cost:   63
c ---[2417]---> BDD-cost:   63
c ---[2416]---> BDD-cost:   63
c ---[2415]---> BDD-cost:   63
c ---[2414]---> BDD-cost:   63
c ---[2413]---> BDD-cost:   63
c ---[2412]---> BDD-cost:   63
c ---[2411]---> BDD-cost:   63
c ---[2410]---> BDD-cost:   63
c ---[2409]---> BDD-cost:   63
c ---[2408]---> BDD-cost:   63
c ---[2407]---> BDD-cost:   63
c ---[2406]---> BDD-cost:   63
c ---[2405]---> BDD-cost:   88
c ---[2404]---> BDD-cost:   88
c ---[2403]---> BDD-cost:   88
c ---[2402]---> BDD-cost:   88
c ---[2401]---> BDD-cost:   88
c ---[2400]---> BDD-cost:   88
c ---[2399]---> BDD-cost:   88
c ---[2398]---> BDD-cost:   88
c ---[2397]---> BDD-cost:   88
c ---[2396]---> BDD-cost:   88
c ---[2395]---> BDD-cost:   88
c ---[2394]---> BDD-cost:   88
c ---[2393]---> BDD-cost:   88
c ---[2392]---> BDD-cost:   88
c ---[2391]---> BDD-cost:   88
c ---[2390]---> BDD-cost:   88
c ---[2389]---> BDD-cost:   88
c ---[2388]---> BDD-cost:   88
c ---[2387]---> BDD-cost:   88
c ---[2386]---> BDD-cost:   88
c ---[2385]---> BDD-cost:   83
c ---[2384]---> BDD-cost:   83
c ---[2383]---> BDD-cost:   83
c ---[2382]---> BDD-cost:   83
c ---[2381]---> BDD-cost:   83
c ---[2380]---> BDD-cost:   63
c ---[2379]---> BDD-cost:   63
c ---[2378]---> BDD-cost:   63
c ---[2377]---> BDD-cost:   63
c ---[2376]---> BDD-cost:   63
c ---[2375]---> BDD-cost:   88
c ---[2374]---> BDD-cost:   88
c ---[2373]---> BDD-cost:   88
c ---[2372]---> BDD-cost:   88
c ---[2371]---> BDD-cost:   88
c ---[2370]---> BDD-cost:   63
c ---[2369]---> BDD-cost:   63
c ---[2368]---> BDD-cost:   63
c ---[2367]---> BDD-cost:   63
c ---[2366]---> BDD-cost:   63
c ---[2365]---> BDD-cost:   63
c ---[2364]---> BDD-cost:   63
c ---[2363]---> BDD-cost:   63
c ---[2362]---> BDD-cost:   63
c ---[2361]---> BDD-cost:   63
c ---[2360]---> BDD-cost:   63
c ---[2359]---> BDD-cost:   63
c ---[2358]---> BDD-cost:   63
c ---[2357]---> BDD-cost:   63
c ---[2356]---> BDD-cost:   63
c ---[2355]---> BDD-cost:   63
c ---[2354]---> BDD-cost:   63
c ---[2353]---> BDD-cost:   63
c ---[2352]---> BDD-cost:   63
c ---[2351]---> BDD-cost:   63
c ---[2350]---> BDD-cost:   88
c ---[2349]---> BDD-cost:   88
c ---[2348]---> BDD-cost:   88
c ---[2347]---> BDD-cost:   88
c ---[2346]---> BDD-cost:   88
c ---[2338]---> BDD-cost:   83
c ---[2337]---> BDD-cost:   83
c ---[2336]---> BDD-cost:   83
c ---[2330]---> BDD-cost:   63
c ---[2329]---> BDD-cost:   63
c ---[2328]---> BDD-cost:   63
c ---[2327]---> BDD-cost:   53
c ---[2326]---> BDD-cost:   53
c ---[2315]---> Sorter-cost:  504     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[2314]---> Sorter-cost:  699     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[2313]---> Sorter-cost:  699     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[2312]---> Sorter-cost:  699     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[2311]---> Sorter-cost:  699     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[2310]---> Sorter-cost:  504     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[2309]---> Sorter-cost:  699     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[2308]---> Sorter-cost:  699     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[2307]---> Sorter-cost:  699     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[2306]---> Sorter-cost:  699     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[2305]---> Sorter-cost:  504     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[2304]---> Sorter-cost:  504     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[2303]---> Sorter-cost:  504     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[2302]---> Sorter-cost:  504     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[2301]---> Sorter-cost:  504     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[2300]---> Sorter-cost:  504     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[2299]---> Sorter-cost:  504     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[2298]---> Sorter-cost:  504     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[2297]---> Sorter-cost:  504     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[2296]---> Sorter-cost:  504     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[2295]---> Sorter-cost:  504     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[2294]---> Sorter-cost:  504     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[2293]---> Sorter-cost:  504     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[2292]---> Sorter-cost:  504     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[2291]---> Sorter-cost:  504     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[2290]---> Sorter-cost:  699     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[2289]---> Sorter-cost:  699     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[2288]---> Sorter-cost:  699     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[2287]---> Sorter-cost:  699     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[2286]---> Sorter-cost:  699     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[2285]---> Sorter-cost:  699     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[2284]---> Sorter-cost:  699     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[2283]---> Sorter-cost:  699     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[2282]---> Sorter-cost:  699     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[2281]---> Sorter-cost:  699     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[2280]---> Sorter-cost:  699     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[2279]---> Sorter-cost:  699     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[2278]---> Sorter-cost:  699     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[2277]---> Sorter-cost:  699     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[2276]---> Sorter-cost:  699     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[2275]---> Sorter-cost:  699     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[2274]---> Sorter-cost:  699     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[2273]---> Sorter-cost:  699     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[2272]---> Sorter-cost:  699     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[2271]---> Sorter-cost:  699     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[2270]---> Sorter-cost:  699     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[2269]---> Sorter-cost:  699     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[2268]---> Sorter-cost:  699     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[2267]---> Sorter-cost:  699     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[2266]---> Sorter-cost:  699     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[2265]---> Sorter-cost:  699     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[2264]---> Sorter-cost:  699     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[2263]---> Sorter-cost:  699     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[2262]---> Sorter-cost:  699     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[2261]---> Sorter-cost:  699     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[2260]---> Sorter-cost:  699     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[2259]---> Sorter-cost:  699     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[2258]---> Sorter-cost:  699     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[2257]---> Sorter-cost:  699     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[2256]---> Sorter-cost:  699     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[2255]---> Sorter-cost:  699     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[2254]---> Sorter-cost:  699     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[2253]---> Sorter-cost:  699     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[2252]---> Sorter-cost:  699     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[2251]---> Sorter-cost:  699     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[2250]---> Sorter-cost:  504     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[2249]---> Sorter-cost:  504     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[2248]---> Sorter-cost:  504     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[2247]---> Sorter-cost:  504     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[2246]---> Sorter-cost:  504     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[2245]---> Sorter-cost:  504     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[2244]---> Sorter-cost:  504     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[2243]---> Sorter-cost:  504     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[2242]---> Sorter-cost:  504     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[2241]---> Sorter-cost:  504     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[2240]---> Sorter-cost:  504     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[2239]---> Sorter-cost:  504     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[2238]---> Sorter-cost:  504     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[2237]---> Sorter-cost:  504     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[2236]---> Sorter-cost:  504     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[2235]---> Sorter-cost:  504     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[2234]---> Sorter-cost:  504     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[2233]---> Sorter-cost:  699     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[2232]---> Sorter-cost:  699     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[2231]---> Sorter-cost:  699     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[2230]---> Sorter-cost:  504     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[2229]---> Sorter-cost:  504     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[2228]---> Sorter-cost:  699     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[2227]---> Sorter-cost:  699     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[2226]---> Sorter-cost:  699     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[2225]---> Sorter-cost:  465     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[2224]---> Sorter-cost:  504     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[2223]---> Sorter-cost:  504     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[2222]---> Sorter-cost:  504     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[2221]---> Sorter-cost:  504     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[2220]---> Sorter-cost:  465     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[2219]---> Sorter-cost:  504     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[2218]---> Sorter-cost:  504     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[2217]---> Sorter-cost:  504     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[2216]---> Sorter-cost:  504     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[2215]---> Sorter-cost:  465     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[2214]---> Sorter-cost:  504     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[2213]---> Sorter-cost:  504     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[2212]---> Sorter-cost:  504     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[2211]---> Sorter-cost:  504     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[2210]---> Sorter-cost:  504     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[2209]---> Sorter-cost:  699     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[2208]---> Sorter-cost:  699     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[2207]---> Sorter-cost:  699     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[2206]---> Sorter-cost:  699     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[2205]---> Sorter-cost:  504     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[2204]---> Sorter-cost:  699     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[2203]---> Sorter-cost:  699     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[2202]---> Sorter-cost:  699     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[2201]---> Sorter-cost:  699     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[2200]---> Sorter-cost:  504     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[2199]---> Sorter-cost:  699     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[2198]---> Sorter-cost:  699     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[2197]---> Sorter-cost:  699     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[2196]---> Sorter-cost:  699     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[2195]---> Sorter-cost:  504     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[2194]---> Sorter-cost:  699     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[2193]---> Sorter-cost:  699     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[2192]---> Sorter-cost:  699     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[2191]---> Sorter-cost:  699     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[2190]---> Sorter-cost:  504     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[2189]---> Sorter-cost:  699     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[2188]---> Sorter-cost:  699     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[2187]---> Sorter-cost:  699     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[2186]---> Sorter-cost:  699     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[2185]---> Sorter-cost:  504     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[2184]---> Sorter-cost:  699     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[2183]---> Sorter-cost:  699     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[2182]---> Sorter-cost:  699     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[2181]---> Sorter-cost:  699     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[2180]---> Sorter-cost:  504     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[2179]---> Sorter-cost:  699     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[2178]---> Sorter-cost:  699     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[2177]---> Sorter-cost:  699     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[2176]---> Sorter-cost:  699     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[2175]---> Sorter-cost:  504     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[2174]---> Sorter-cost:  699     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[2173]---> Sorter-cost:  699     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[2172]---> Sorter-cost:  699     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[2171]---> Sorter-cost:  699     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[2170]---> Sorter-cost:  465     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[2169]---> Sorter-cost:  504     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[2168]---> Sorter-cost:  504     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[2167]---> Sorter-cost:  504     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[2166]---> Sorter-cost:  504     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[2165]---> Sorter-cost:  465     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[2164]---> Sorter-cost:  504     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[2163]---> Sorter-cost:  504     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[2162]---> Sorter-cost:  504     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[2161]---> Sorter-cost:  504     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[2160]---> Sorter-cost:  465     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[2159]---> Sorter-cost:  504     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[2158]---> Sorter-cost:  504     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[2157]---> Sorter-cost:  504     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[2156]---> Sorter-cost:  504     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[2155]---> Sorter-cost:  465     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[2154]---> Sorter-cost:  504     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[2153]---> Sorter-cost:  504     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[2152]---> Sorter-cost:  504     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[2151]---> Sorter-cost:  504     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[2150]---> Sorter-cost:  465     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[2149]---> Sorter-cost:  504     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[2148]---> Sorter-cost:  504     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[2147]---> Sorter-cost:  504     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[2146]---> Sorter-cost:  504     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[2145]---> Sorter-cost:  465     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[2144]---> Sorter-cost:  465     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[2143]---> Sorter-cost:  504     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[2142]---> Sorter-cost:  504     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[2141]---> Sorter-cost:  504     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[2140]---> Sorter-cost:  465     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[2139]---> Sorter-cost:  465     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[2138]---> Sorter-cost:  504     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[2137]---> Sorter-cost:  504     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[2136]---> Sorter-cost:  504     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[2135]---> Sorter-cost:  465     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[2134]---> Sorter-cost:  465     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[2133]---> Sorter-cost:  504     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[2132]---> Sorter-cost:  504     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[2131]---> Sorter-cost:  504     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[2130]---> Sorter-cost:  504     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[2129]---> Sorter-cost:  504     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[2128]---> Sorter-cost:  699     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[2127]---> Sorter-cost:  699     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[2126]---> Sorter-cost:  699     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[2125]---> Sorter-cost:  504     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[2124]---> Sorter-cost:  504     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[2123]---> Sorter-cost:  699     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[2122]---> Sorter-cost:  699     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[2121]---> Sorter-cost:  699     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[2120]---> Sorter-cost:  504     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[2119]---> Sorter-cost:  504     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[2118]---> Sorter-cost:  699     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[2117]---> Sorter-cost:  699     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[2116]---> Sorter-cost:  699     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[2115]---> Sorter-cost:  504     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[2114]---> Sorter-cost:  504     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[2113]---> Sorter-cost:  699     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[2112]---> Sorter-cost:  699     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[2111]---> Sorter-cost:  699     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[2110]---> Sorter-cost:  504     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[2109]---> Sorter-cost:  504     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[2108]---> Sorter-cost:  699     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[2107]---> Sorter-cost:  699     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[2106]---> Sorter-cost:  699     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[2105]---> Sorter-cost:  504     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[2104]---> Sorter-cost:  504     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[2103]---> Sorter-cost:  699     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[2102]---> Sorter-cost:  699     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[2101]---> Sorter-cost:  699     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[2100]---> Sorter-cost:  504     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[2099]---> Sorter-cost:  504     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[2098]---> Sorter-cost:  699     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[2097]---> Sorter-cost:  699     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[2096]---> Sorter-cost:  699     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[2095]---> Sorter-cost:  504     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[2094]---> Sorter-cost:  504     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[2093]---> Sorter-cost:  699     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[2092]---> Sorter-cost:  699     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[2091]---> Sorter-cost:  699     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[2090]---> Sorter-cost:  465     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[2089]---> Sorter-cost:  465     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[2088]---> Sorter-cost:  504     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[2087]---> Sorter-cost:  504     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[2086]---> Sorter-cost:  504     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[2085]---> Sorter-cost:  465     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[2084]---> Sorter-cost:  465     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[2083]---> Sorter-cost:  504     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[2082]---> Sorter-cost:  504     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[2081]---> Sorter-cost:  504     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[2080]---> Sorter-cost:  465     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[2079]---> Sorter-cost:  465     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[2078]---> Sorter-cost:  504     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[2077]---> Sorter-cost:  504     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[2076]---> Sorter-cost:  504     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[2075]---> Sorter-cost:  465     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[2074]---> Sorter-cost:  465     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[2073]---> Sorter-cost:  504     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[2072]---> Sorter-cost:  504     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[2071]---> Sorter-cost:  504     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[2070]---> Sorter-cost:  465     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[2069]---> Sorter-cost:  465     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[2068]---> Sorter-cost:  504     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[2067]---> Sorter-cost:  504     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[2066]---> Sorter-cost:  504     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[2065]---> Sorter-cost:  465     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[2064]---> Sorter-cost:  465     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[2063]---> Sorter-cost:  465     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[2062]---> Sorter-cost:  465     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[2061]---> Sorter-cost:  465     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[2060]---> Sorter-cost:  465     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[2059]---> Sorter-cost:  465     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[2058]---> Sorter-cost:  465     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[2057]---> Sorter-cost:  465     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[2056]---> Sorter-cost:  465     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[2055]---> Sorter-cost:  465     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[2054]---> Sorter-cost:  465     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[2053]---> Sorter-cost:  465     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[2052]---> Sorter-cost:  465     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[2051]---> Sorter-cost:  465     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[2050]---> Sorter-cost:  504     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[2049]---> Sorter-cost:  504     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[2048]---> Sorter-cost:  504     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[2047]---> Sorter-cost:  504     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[2046]---> Sorter-cost:  504     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[2045]---> Sorter-cost:  504     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[2044]---> Sorter-cost:  504     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[2043]---> Sorter-cost:  504     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[2042]---> Sorter-cost:  504     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[2041]---> Sorter-cost:  504     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[2040]---> Sorter-cost:  504     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[2039]---> Sorter-cost:  504     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[2038]---> Sorter-cost:  504     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[2037]---> Sorter-cost:  504     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[2036]---> Sorter-cost:  504     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[2035]---> Sorter-cost:  504     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[2034]---> Sorter-cost:  504     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[2033]---> Sorter-cost:  504     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[2032]---> Sorter-cost:  504     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[2031]---> Sorter-cost:  504     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[2030]---> Sorter-cost:  504     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[2029]---> Sorter-cost:  504     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[2028]---> Sorter-cost:  504     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[2027]---> Sorter-cost:  504     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[2026]---> Sorter-cost:  504     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[2025]---> Sorter-cost:  504     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[2024]---> Sorter-cost:  504     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[2023]---> Sorter-cost:  504     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[2022]---> Sorter-cost:  504     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[2021]---> Sorter-cost:  504     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[2020]---> Sorter-cost:  504     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[2019]---> Sorter-cost:  504     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[2018]---> Sorter-cost:  504     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[2017]---> Sorter-cost:  504     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[2016]---> Sorter-cost:  504     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[2015]---> Sorter-cost:  504     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[2014]---> Sorter-cost:  504     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[2013]---> Sorter-cost:  504     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[2012]---> Sorter-cost:  504     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[2011]---> Sorter-cost:  504     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[2010]---> Sorter-cost:  465     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[2009]---> Sorter-cost:  465     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[2008]---> Sorter-cost:  465     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[2007]---> Sorter-cost:  465     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[2006]---> Sorter-cost:  465     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[2005]---> Sorter-cost:  465     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[2004]---> Sorter-cost:  465     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[2003]---> Sorter-cost:  465     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[2002]---> Sorter-cost:  465     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[2001]---> Sorter-cost:  465     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[2000]---> Sorter-cost:  465     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1999]---> Sorter-cost:  465     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1998]---> Sorter-cost:  465     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1997]---> Sorter-cost:  465     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1996]---> Sorter-cost:  465     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1995]---> Sorter-cost:  465     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1994]---> Sorter-cost:  465     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1993]---> Sorter-cost:  465     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1992]---> Sorter-cost:  465     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1991]---> Sorter-cost:  465     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1990]---> Sorter-cost:  465     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1989]---> Sorter-cost:  465     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1988]---> Sorter-cost:  465     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1987]---> Sorter-cost:  465     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1986]---> Sorter-cost:  465     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1984]---> BDD-cost:    0
c ---[1982]---> Adder-cost: 272   maxlim: 120186   bits: 18/17
c ---[1980]---> BDD-cost:    0
c ---[1978]---> Adder-cost: 296   maxlim: 832890   bits: 21/20
c ---[1976]---> BDD-cost:    0
c ---[1974]---> Adder-cost: 322   maxlim: 1348986   bits: 22/21
c ---[1972]---> BDD-cost:    0
c ---[1970]---> Adder-cost: 322   maxlim: 1348986   bits: 22/21
c ---[1968]---> BDD-cost:    0
c ---[1966]---> Adder-cost: 322   maxlim: 1348986   bits: 22/21
c ---[1964]---> BDD-cost:   49
c ---[1962]---> BDD-cost:   46
c ---[1960]---> BDD-cost:   58
c ---[1958]---> BDD-cost:   52
c ---[1956]---> BDD-cost:   61
c ---[1954]---> BDD-cost:   52
c ---[1952]---> BDD-cost:   61
c ---[1950]---> BDD-cost:   52
c ---[1948]---> BDD-cost:   61
c ---[1946]---> BDD-cost:   52
c ---[1944]---> Adder-cost: 508   maxlim: 114678   bits: 18/17
c ---[1942]---> Adder-cost: 508   maxlim: 114678   bits: 18/17
c ---[1940]---> Adder-cost: 554   maxlim: 1146870   bits: 22/21
c ---[1938]---> Adder-cost: 554   maxlim: 1146870   bits: 22/21
c ---[1936]---> Adder-cost: 604   maxlim: 2179062   bits: 23/22
c ---[1934]---> Adder-cost: 602   maxlim: 2179062   bits: 23/22
c ---[1932]---> Adder-cost: 604   maxlim: 2179062   bits: 23/22
c ---[1930]---> Adder-cost: 602   maxlim: 2179062   bits: 23/22
c ---[1928]---> Adder-cost: 604   maxlim: 2179062   bits: 23/22
c ---[1926]---> Adder-cost: 602   maxlim: 2179062   bits: 23/22
c ---[1924]---> BDD-cost:    0
c ---[1922]---> BDD-cost:    0
c ---[1920]---> BDD-cost:    0
c ---[1918]---> BDD-cost:    0
c ---[1916]---> BDD-cost:    0
c ---[1914]---> BDD-cost:    0
c ---[1912]---> BDD-cost:    0
c ---[1910]---> BDD-cost:    0
c ---[1908]---> BDD-cost:    0
c ---[1906]---> BDD-cost:    0
c ---[1904]---> Sorter-cost: 2794     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1902]---> Sorter-cost: 2767     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1900]---> Sorter-cost: 2848     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1898]---> Sorter-cost: 2837     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1896]---> Sorter-cost: 2932     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1894]---> Adder-cost: 258   maxlim: 188411   bits: 19/18
c ---[1892]---> Sorter-cost: 2932     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1890]---> Adder-cost: 258   maxlim: 188411   bits: 19/18
c ---[1888]---> Sorter-cost: 2932     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1886]---> Adder-cost: 258   maxlim: 188411   bits: 19/18
c ---[1884]---> Adder-cost: 400   maxlim: 81912   bits: 18/17
c ---[1882]---> Adder-cost: 400   maxlim: 81912   bits: 18/17
c ---[1880]---> Adder-cost: 406   maxlim: 98296   bits: 18/17
c ---[1878]---> Adder-cost: 406   maxlim: 98296   bits: 18/17
c ---[1876]---> Adder-cost: 414   maxlim: 114680   bits: 18/17
c ---[1874]---> Adder-cost: 414   maxlim: 114680   bits: 18/17
c ---[1872]---> Adder-cost: 414   maxlim: 114680   bits: 18/17
c ---[1870]---> Adder-cost: 414   maxlim: 114680   bits: 18/17
c ---[1868]---> Adder-cost: 414   maxlim: 114680   bits: 18/17
c ---[1866]---> Adder-cost: 414   maxlim: 114680   bits: 18/17
c ---[1864]---> Adder-cost: 418   maxlim: 606199   bits: 21/20
c ---[1862]---> Adder-cost: 413   maxlim: 212983   bits: 19/18
c ---[1860]---> Adder-cost: 424   maxlim: 622583   bits: 21/20
c ---[1858]---> Adder-cost: 419   maxlim: 229367   bits: 19/18
c ---[1856]---> Adder-cost: 432   maxlim: 638967   bits: 21/20
c ---[1854]---> Adder-cost: 427   maxlim: 245751   bits: 19/18
c ---[1852]---> Adder-cost: 432   maxlim: 638967   bits: 21/20
c ---[1850]---> Adder-cost: 427   maxlim: 245751   bits: 19/18
c ---[1848]---> Adder-cost: 432   maxlim: 638967   bits: 21/20
c ---[1846]---> Adder-cost: 427   maxlim: 245751   bits: 19/18
c ---[1844]---> Sorter-cost: 3104     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1842]---> Sorter-cost: 3065     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1840]---> Sorter-cost: 3346     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1838]---> Sorter-cost: 3322     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1836]---> Sorter-cost: 3589     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1834]---> Sorter-cost: 3567     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1832]---> Sorter-cost: 3589     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1830]---> Sorter-cost: 3567     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1828]---> Sorter-cost: 3589     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1826]---> Sorter-cost: 3567     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1824]---> BDD-cost:    0
c ---[1822]---> BDD-cost:    0
c ---[1820]---> BDD-cost:    0
c ---[1818]---> BDD-cost:    0
c ---[1816]---> BDD-cost:    0
c ---[1814]---> BDD-cost:    0
c ---[1812]---> BDD-cost:    0
c ---[1810]---> BDD-cost:    0
c ---[1808]---> BDD-cost:    0
c ---[1806]---> BDD-cost:    0
c ---[1804]---> BDD-cost:   55
c ---[1802]---> BDD-cost:   49
c ---[1800]---> BDD-cost:   55
c ---[1798]---> BDD-cost:   49
c ---[1796]---> BDD-cost:   55
c ---[1794]---> BDD-cost:   49
c ---[1792]---> BDD-cost:   55
c ---[1790]---> BDD-cost:   49
c ---[1788]---> BDD-cost:   55
c ---[1786]---> BDD-cost:   49
c ---[1784]---> Sorter-cost:  735     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1782]---> Sorter-cost:  625     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1780]---> Sorter-cost:  794     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1778]---> Sorter-cost:  625     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1776]---> Sorter-cost:  794     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1774]---> Sorter-cost:  625     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1772]---> Sorter-cost:  794     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1770]---> Sorter-cost:  625     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1768]---> Sorter-cost:  794     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1766]---> Sorter-cost:  625     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1764]---> Sorter-cost:  747     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1762]---> BDD-cost:  167
c ---[1760]---> Sorter-cost:  767     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1758]---> BDD-cost:  167
c ---[1756]---> Sorter-cost:  767     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1754]---> BDD-cost:  167
c ---[1752]---> Sorter-cost:  767     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1750]---> BDD-cost:  167
c ---[1748]---> Sorter-cost:  767     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1746]---> BDD-cost:  167
c ---[1744]---> BDD-cost:    0
c ---[1742]---> BDD-cost:    0
c ---[1740]---> BDD-cost:    0
c ---[1738]---> BDD-cost:    0
c ---[1736]---> BDD-cost:    0
c ---[1734]---> BDD-cost:    0
c ---[1732]---> BDD-cost:    0
c ---[1730]---> BDD-cost:    0
c ---[1728]---> BDD-cost:    0
c ---[1726]---> BDD-cost:    0
c ---[1724]---> BDD-cost:  164
c ---[1722]---> BDD-cost:  137
c ---[1720]---> BDD-cost:  173
c ---[1718]---> BDD-cost:  137
c ---[1716]---> BDD-cost:  173
c ---[1714]---> BDD-cost:  137
c ---[1712]---> BDD-cost:  173
c ---[1710]---> BDD-cost:  137
c ---[1708]---> BDD-cost:  173
c ---[1706]---> BDD-cost:  137
c ---[1704]---> BDD-cost:   40
c ---[1702]---> BDD-cost:   40
c ---[1700]---> BDD-cost:   40
c ---[1698]---> BDD-cost:   40
c ---[1696]---> BDD-cost:   40
c ---[1694]---> BDD-cost:  163
c ---[1692]---> BDD-cost:  136
c ---[1690]---> BDD-cost:  172
c ---[1688]---> BDD-cost:  136
c ---[1686]---> BDD-cost:  172
c ---[1684]---> BDD-cost:  136
c ---[1682]---> BDD-cost:  172
c ---[1680]---> BDD-cost:  136
c ---[1678]---> BDD-cost:  172
c ---[1676]---> BDD-cost:  136
c ---[1674]---> Sorter-cost:  685     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1672]---> BDD-cost:   46
c ---[1670]---> Sorter-cost:  690     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1668]---> BDD-cost:   46
c ---[1666]---> Sorter-cost:  690     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1664]---> BDD-cost:   46
c ---[1662]---> Sorter-cost:  690     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1660]---> BDD-cost:   46
c ---[1658]---> Sorter-cost:  690     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1656]---> BDD-cost:   46
c ---[1654]---> Sorter-cost:  388     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1652]---> BDD-cost:  135
c ---[1650]---> Sorter-cost:  388     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1648]---> BDD-cost:  135
c ---[1646]---> Sorter-cost:  388     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1644]---> BDD-cost:  135
c ---[1642]---> Sorter-cost:  388     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1640]---> BDD-cost:  135
c ---[1638]---> Sorter-cost:  388     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1636]---> BDD-cost:  135
c ---[1634]---> Sorter-cost:  829     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1632]---> Sorter-cost:  829     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1630]---> Sorter-cost:  829     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1628]---> Sorter-cost:  829     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1626]---> Sorter-cost:  829     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1624]---> Sorter-cost:  829     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1622]---> Sorter-cost:  829     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1620]---> Sorter-cost:  829     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1618]---> Sorter-cost:  829     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1616]---> Sorter-cost:  829     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1614]---> BDD-cost:  118
c ---[1612]---> BDD-cost:  118
c ---[1610]---> BDD-cost:  118
c ---[1608]---> BDD-cost:  118
c ---[1606]---> BDD-cost:  118
c ---[1604]---> BDD-cost:  118
c ---[1602]---> BDD-cost:  118
c ---[1600]---> BDD-cost:  118
c ---[1598]---> BDD-cost:  118
c ---[1596]---> BDD-cost:  118
c ---[1594]---> Adder-cost: 484   maxlim: 1146872   bits: 22/21
c ---[1592]---> Adder-cost: 484   maxlim: 1146872   bits: 22/21
c ---[1590]---> Adder-cost: 526   maxlim: 2162680   bits: 23/22
c ---[1588]---> Adder-cost: 526   maxlim: 2162680   bits: 23/22
c ---[1586]---> Adder-cost: 564   maxlim: 3178488   bits: 23/22
c ---[1584]---> Adder-cost: 564   maxlim: 3178488   bits: 23/22
c ---[1582]---> Adder-cost: 564   maxlim: 3178488   bits: 23/22
c ---[1580]---> Adder-cost: 564   maxlim: 3178488   bits: 23/22
c ---[1578]---> Adder-cost: 564   maxlim: 3178488   bits: 23/22
c ---[1576]---> Adder-cost: 564   maxlim: 3178488   bits: 23/22
c ---[1574]---> BDD-cost:    0
c ---[1572]---> BDD-cost:    0
c ---[1570]---> BDD-cost:    0
c ---[1568]---> BDD-cost:    0
c ---[1566]---> BDD-cost:    0
c ---[1564]---> BDD-cost:    0
c ---[1562]---> BDD-cost:    0
c ---[1560]---> BDD-cost:    0
c ---[1558]---> BDD-cost:    0
c ---[1556]---> BDD-cost:    0
c ---[1554]---> BDD-cost:    0
c ---[1552]---> BDD-cost:    0
c ---[1550]---> BDD-cost:    0
c ---[1548]---> BDD-cost:    0
c ---[1546]---> BDD-cost:    0
c ---[1544]---> BDD-cost:    0
c ---[1542]---> BDD-cost:    0
c ---[1540]---> BDD-cost:    0
c ---[1538]---> BDD-cost:    0
c ---[1536]---> BDD-cost:    0
c ---[1534]---> Sorter-cost: 2593     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1532]---> Sorter-cost: 2593     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1530]---> Sorter-cost: 2813     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1528]---> Sorter-cost: 2813     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1526]---> Sorter-cost: 3034     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1524]---> Sorter-cost: 3034     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1522]---> Sorter-cost: 3034     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1520]---> Sorter-cost: 3034     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1518]---> Sorter-cost: 3034     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1516]---> Sorter-cost: 3034     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1514]---> Adder-cost: 326   maxlim: 1609210   bits: 22/21
c ---[1512]---> BDD-cost:    0
c ---[1510]---> Adder-cost: 344   maxlim: 2104314   bits: 22/22
c ---[1508]---> BDD-cost:    0
c ---[1506]---> Adder-cost: 368   maxlim: 2599418   bits: 23/22
c ---[1504]---> BDD-cost:    0
c ---[1502]---> Adder-cost: 368   maxlim: 2586618   bits: 23/22
c ---[1500]---> BDD-cost:    0
c ---[1498]---> Adder-cost: 368   maxlim: 2573818   bits: 23/22
c ---[1496]---> BDD-cost:    0
c ---[1494]---> Sorter-cost:  616     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1492]---> Sorter-cost:  616     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1490]---> Sorter-cost:  616     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1488]---> Sorter-cost:  616     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1486]---> Sorter-cost:  616     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1484]---> Sorter-cost:  616     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1482]---> Sorter-cost:  566     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1480]---> Sorter-cost:  566     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1478]---> Sorter-cost:  566     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1476]---> Sorter-cost:  566     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1474]---> Sorter-cost: 1078     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1472]---> Sorter-cost: 1327     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1470]---> Sorter-cost: 1078     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1468]---> Sorter-cost: 1327     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1466]---> Sorter-cost: 1078     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1464]---> Sorter-cost: 1327     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1462]---> Sorter-cost: 1078     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1460]---> Sorter-cost: 1327     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1458]---> Sorter-cost: 1078     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1456]---> Sorter-cost: 1327     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1454]---> BDD-cost:  118
c ---[1452]---> BDD-cost:  118
c ---[1450]---> BDD-cost:  118
c ---[1448]---> BDD-cost:  118
c ---[1446]---> BDD-cost:  118
c ---[1444]---> BDD-cost:  118
c ---[1442]---> BDD-cost:  118
c ---[1440]---> BDD-cost:  118
c ---[1438]---> BDD-cost:  118
c ---[1436]---> BDD-cost:  118
c ---[1434]---> Sorter-cost:  520     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1432]---> Sorter-cost:  520     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1430]---> Sorter-cost:  520     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1428]---> Sorter-cost:  520     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1426]---> Sorter-cost:  520     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1424]---> Sorter-cost:  520     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1422]---> Sorter-cost:  520     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1420]---> Sorter-cost:  520     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1418]---> Sorter-cost:  520     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1416]---> Sorter-cost:  520     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1414]---> Sorter-cost:  520     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1412]---> Sorter-cost:  520     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1410]---> Sorter-cost:  520     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1408]---> Sorter-cost:  520     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1406]---> Sorter-cost:  520     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1404]---> Sorter-cost:  520     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1402]---> Sorter-cost:  520     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1400]---> Sorter-cost:  520     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1398]---> Sorter-cost:  520     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1396]---> Sorter-cost:  520     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1394]---> BDD-cost:    0
c ---[1392]---> Sorter-cost: 3104     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1390]---> BDD-cost:    0
c ---[1388]---> Sorter-cost: 3322     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1386]---> BDD-cost:    0
c ---[1384]---> Adder-cost: 322   maxlim: 1720315   bits: 22/21
c ---[1382]---> BDD-cost:    0
c ---[1380]---> Adder-cost: 322   maxlim: 1720315   bits: 22/21
c ---[1378]---> BDD-cost:    0
c ---[1376]---> Adder-cost: 322   maxlim: 1720315   bits: 22/21
c ---[1374]---> BDD-cost:    0
c ---[1372]---> Adder-cost: 286   maxlim: 565243   bits: 21/20
c ---[1370]---> BDD-cost:    0
c ---[1368]---> Adder-cost: 290   maxlim: 573435   bits: 21/20
c ---[1366]---> BDD-cost:    0
c ---[1364]---> Adder-cost: 292   maxlim: 581627   bits: 21/20
c ---[1362]---> BDD-cost:    0
c ---[1360]---> Adder-cost: 292   maxlim: 581627   bits: 21/20
c ---[1358]---> BDD-cost:    0
c ---[1356]---> Adder-cost: 292   maxlim: 581627   bits: 21/20
c ---[1354]---> Sorter-cost: 1662     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1352]---> Sorter-cost: 1662     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1350]---> Sorter-cost: 1714     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1348]---> Sorter-cost: 1714     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1346]---> Sorter-cost: 1766     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1344]---> Sorter-cost: 1766     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1342]---> Sorter-cost: 1766     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1340]---> Sorter-cost: 1766     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1338]---> Sorter-cost: 1766     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1336]---> Sorter-cost: 1766     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1334]---> BDD-cost:   55
c ---[1332]---> BDD-cost:   55
c ---[1330]---> BDD-cost:   55
c ---[1328]---> BDD-cost:   55
c ---[1326]---> BDD-cost:   55
c ---[1324]---> BDD-cost:   55
c ---[1322]---> BDD-cost:   55
c ---[1320]---> BDD-cost:   55
c ---[1318]---> BDD-cost:   55
c ---[1316]---> BDD-cost:   55
c ---[1314]---> Sorter-cost:  829     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1312]---> Sorter-cost:  829     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1310]---> Sorter-cost:  829     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1308]---> Sorter-cost:  829     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1306]---> Sorter-cost:  829     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1304]---> Sorter-cost:  829     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1302]---> Sorter-cost:  829     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1300]---> Sorter-cost:  829     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1298]---> Sorter-cost:  829     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1296]---> Sorter-cost:  829     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1294]---> BDD-cost:  145
c ---[1292]---> BDD-cost:  145
c ---[1290]---> BDD-cost:  145
c ---[1288]---> BDD-cost:  145
c ---[1286]---> BDD-cost:  145
c ---[1284]---> BDD-cost:  145
c ---[1282]---> BDD-cost:  145
c ---[1280]---> BDD-cost:  145
c ---[1278]---> BDD-cost:  145
c ---[1276]---> BDD-cost:  145
c ---[1274]---> BDD-cost:    0
c ---[1272]---> BDD-cost:    0
c ---[1270]---> BDD-cost:    0
c ---[1268]---> BDD-cost:    0
c ---[1266]---> BDD-cost:    0
c ---[1264]---> BDD-cost:    0
c ---[1262]---> BDD-cost:    0
c ---[1260]---> BDD-cost:    0
c ---[1258]---> BDD-cost:    0
c ---[1256]---> BDD-cost:    0
c ---[1254]---> BDD-cost:   55
c ---[1252]---> BDD-cost:   55
c ---[1250]---> BDD-cost:   55
c ---[1248]---> BDD-cost:   55
c ---[1246]---> BDD-cost:   55
c ---[1244]---> BDD-cost:   55
c ---[1242]---> BDD-cost:   55
c ---[1240]---> BDD-cost:   55
c ---[1238]---> BDD-cost:   55
c ---[1236]---> BDD-cost:   55
c ---[1234]---> BDD-cost:   55
c ---[1232]---> BDD-cost:   55
c ---[1230]---> BDD-cost:   55
c ---[1228]---> BDD-cost:   55
c ---[1226]---> BDD-cost:   55
c ---[1224]---> BDD-cost:   55
c ---[1222]---> BDD-cost:   55
c ---[1220]---> BDD-cost:   55
c ---[1218]---> BDD-cost:   55
c ---[1216]---> BDD-cost:   55
c ---[1214]---> BDD-cost:    0
c ---[1212]---> Sorter-cost:  993     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1210]---> BDD-cost:    0
c ---[1208]---> Sorter-cost:  993     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1206]---> BDD-cost:    0
c ---[1204]---> Sorter-cost:  993     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1202]---> BDD-cost:    0
c ---[1200]---> Sorter-cost:  993     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1198]---> BDD-cost:    0
c ---[1196]---> Sorter-cost:  993     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1194]---> Adder-cost: 482   maxlim: 630775   bits: 21/20
c ---[1192]---> Adder-cost: 482   maxlim: 630775   bits: 21/20
c ---[1190]---> Adder-cost: 504   maxlim: 1146871   bits: 22/21
c ---[1188]---> Adder-cost: 504   maxlim: 1146871   bits: 22/21
c ---[1186]---> Adder-cost: 528   maxlim: 1662967   bits: 22/21
c ---[1184]---> Adder-cost: 472   maxlim: 1662967   bits: 22/21
c ---[1182]---> Adder-cost: 528   maxlim: 1662967   bits: 22/21
c ---[1180]---> Adder-cost: 472   maxlim: 1662967   bits: 22/21
c ---[1178]---> Adder-cost: 528   maxlim: 1662967   bits: 22/21
c ---[1176]---> Adder-cost: 472   maxlim: 1662967   bits: 22/21
c ---[1174]---> Adder-cost: 460   maxlim: 1146872   bits: 22/21
c ---[1172]---> Adder-cost: 460   maxlim: 1146872   bits: 22/21
c ---[1170]---> Adder-cost: 500   maxlim: 2162680   bits: 23/22
c ---[1168]---> Adder-cost: 500   maxlim: 2162680   bits: 23/22
c ---[1166]---> Adder-cost: 520   maxlim: 3178488   bits: 23/22
c ---[1164]---> Adder-cost: 540   maxlim: 3178488   bits: 23/22
c ---[1162]---> Adder-cost: 520   maxlim: 3178488   bits: 23/22
c ---[1160]---> Adder-cost: 540   maxlim: 3178488   bits: 23/22
c ---[1158]---> Adder-cost: 520   maxlim: 3178488   bits: 23/22
c ---[1156]---> Adder-cost: 540   maxlim: 3178488   bits: 23/22
c ---[1154]---> BDD-cost:    0
c ---[1152]---> BDD-cost:    0
c ---[1150]---> BDD-cost:    0
c ---[1148]---> BDD-cost:    0
c ---[1146]---> BDD-cost:    0
c ---[1144]---> BDD-cost:    0
c ---[1142]---> BDD-cost:    0
c ---[1140]---> BDD-cost:    0
c ---[1138]---> BDD-cost:    0
c ---[1136]---> BDD-cost:    0
c ---[1134]---> Sorter-cost:  717     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1132]---> Sorter-cost:  683     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1130]---> Sorter-cost:  726     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1128]---> Sorter-cost:  683     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1126]---> Sorter-cost:  742     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1124]---> Sorter-cost:  692     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1122]---> Sorter-cost:  742     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1120]---> Sorter-cost:  692     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1118]---> Sorter-cost:  742     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1116]---> Sorter-cost:  692     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1114]---> Sorter-cost: 2390     Base: 2 2 2 2 2 2 2 2 2 2 2 2 7
c ---[1112]---> BDD-cost:    0
c ---[1110]---> Sorter-cost: 2439     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 7
c ---[1108]---> BDD-cost:    0
c ---[1106]---> Sorter-cost: 2371     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1104]---> BDD-cost:    0
c ---[1102]---> Sorter-cost: 2371     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1100]---> BDD-cost:    0
c ---[1098]---> Sorter-cost: 2371     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1096]---> BDD-cost:    0
c ---[1094]---> Adder-cost: 400   maxlim: 81912   bits: 18/17
c ---[1092]---> Adder-cost: 400   maxlim: 81912   bits: 18/17
c ---[1090]---> Adder-cost: 406   maxlim: 98296   bits: 18/17
c ---[1088]---> Adder-cost: 406   maxlim: 98296   bits: 18/17
c ---[1086]---> Adder-cost: 414   maxlim: 114680   bits: 18/17
c ---[1084]---> Adder-cost: 414   maxlim: 114680   bits: 18/17
c ---[1082]---> Adder-cost: 414   maxlim: 114680   bits: 18/17
c ---[1080]---> Adder-cost: 414   maxlim: 114680   bits: 18/17
c ---[1078]---> Adder-cost: 414   maxlim: 114680   bits: 18/17
c ---[1076]---> Adder-cost: 414   maxlim: 114680   bits: 18/17
c ---[1074]---> BDD-cost:  164
c ---[1072]---> BDD-cost:  137
c ---[1070]---> BDD-cost:  170
c ---[1068]---> BDD-cost:  137
c ---[1066]---> BDD-cost:  170
c ---[1064]---> BDD-cost:  137
c ---[1062]---> BDD-cost:  170
c ---[1060]---> BDD-cost:  137
c ---[1058]---> BDD-cost:  170
c ---[1056]---> BDD-cost:  137
c ---[1054]---> BDD-cost:   49
c ---[1052]---> BDD-cost:    0
c ---[1050]---> BDD-cost:   47
c ---[1048]---> BDD-cost:    0
c ---[1046]---> BDD-cost:   49
c ---[1044]---> BDD-cost:    0
c ---[1042]---> BDD-cost:   37
c ---[1040]---> BDD-cost:    0
c ---[1038]---> BDD-cost:   37
c ---[1036]---> BDD-cost:    0
c ---[1034]---> Sorter-cost:  432     Base: 2 2 2 2 2 2 2
c ---[1033]---> Sorter-cost:  425     Base: 2 2 2 2 2 2 2
c ---[1031]---> Sorter-cost:  279     Base: 2 2 2 2 2 2 2
c ---[1030]---> Sorter-cost:  270     Base: 2 2 2 2 2 2 2
c ---[1028]---> Sorter-cost:  279     Base: 2 2 2 2 2 2 2
c ---[1027]---> Sorter-cost:  270     Base: 2 2 2 2 2 2 2
c ---[1025]---> Sorter-cost:  279     Base: 2 2 2 2 2 2 2
c ---[1024]---> Sorter-cost:  270     Base: 2 2 2 2 2 2 2
c ---[1022]---> Sorter-cost:  279     Base: 2 2 2 2 2 2 2
c ---[1021]---> Sorter-cost:  270     Base: 2 2 2 2 2 2 2
c ---[1019]---> Sorter-cost:  279     Base: 2 2 2 2 2 2 2
c ---[1018]---> Sorter-cost:  270     Base: 2 2 2 2 2 2 2
c ---[1016]---> Sorter-cost:  279     Base: 2 2 2 2 2 2 2
c ---[1015]---> Sorter-cost:  270     Base: 2 2 2 2 2 2 2
c ---[1013]---> Sorter-cost:  279     Base: 2 2 2 2 2 2 2
c ---[1012]---> Sorter-cost:  270     Base: 2 2 2 2 2 2 2
c ---[1011]---> Adder-cost: 808   maxlim: 8454123   bits: 25/24
c ---[1010]---> Adder-cost: 774   maxlim: 6422507   bits: 24/23
c ---[1006]---> Adder-cost: 808   maxlim: 8454123   bits: 25/24
c ---[1005]---> Adder-cost: 774   maxlim: 6422507   bits: 24/23
c ---[ 989]---> Adder-cost: 863   maxlim: 10485739   bits: 25/24
c ---[ 988]---> Adder-cost: 808   maxlim: 8454123   bits: 25/24
c ---[ 987]---> Adder-cost: 774   maxlim: 6422507   bits: 24/23
c ---[ 985]---> Adder-cost: 863   maxlim: 10485739   bits: 25/24
c ---[ 984]---> Adder-cost: 808   maxlim: 8454123   bits: 25/24
c ---[ 983]---> Adder-cost: 774   maxlim: 6422507   bits: 24/23
c ---[ 981]---> Adder-cost: 863   maxlim: 10485739   bits: 25/24
c ---[ 980]---> Adder-cost: 808   maxlim: 8454123   bits: 25/24
c ---[ 979]---> Adder-cost: 774   maxlim: 6422507   bits: 24/23
c ---[ 977]---> Adder-cost: 863   maxlim: 10485739   bits: 25/24
c ---[ 976]---> Adder-cost: 808   maxlim: 8454123   bits: 25/24
c ---[ 975]---> Adder-cost: 774   maxlim: 6422507   bits: 24/23
c ---[ 973]---> Adder-cost: 863   maxlim: 10485739   bits: 25/24
c ---[ 972]---> Adder-cost: 808   maxlim: 8454123   bits: 25/24
c ---[ 971]---> Adder-cost: 774   maxlim: 6422507   bits: 24/23
c ---[ 969]---> Adder-cost: 863   maxlim: 10485739   bits: 25/24
c ---[ 968]---> Adder-cost: 808   maxlim: 8454123   bits: 25/24
c ---[ 967]---> Adder-cost: 774   maxlim: 6422507   bits: 24/23
c ---[ 965]---> Adder-cost: 863   maxlim: 10485739   bits: 25/24
c ---[ 964]---> Adder-cost: 808   maxlim: 8454123   bits: 25/24
c ---[ 963]---> Adder-cost: 774   maxlim: 6422507   bits: 24/23
c ---[ 961]---> Adder-cost: 863   maxlim: 10485739   bits: 25/24
c ---[ 960]---> Adder-cost: 808   maxlim: 8454123   bits: 25/24
c ---[ 959]---> Adder-cost: 774   maxlim: 6422507   bits: 24/23
c ---[ 944]---> Sorter-cost:  718     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 942]---> Sorter-cost:  598     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 940]---> Sorter-cost:  758     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 938]---> Sorter-cost:  598     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 936]---> Sorter-cost:  758     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 934]---> Sorter-cost:  598     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 932]---> Sorter-cost:  758     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 930]---> Sorter-cost:  598     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 928]---> Sorter-cost:  758     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 926]---> Sorter-cost:  598     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 924]---> BDD-cost:    0
c ---[ 922]---> BDD-cost:    0
c ---[ 920]---> BDD-cost:    0
c ---[ 918]---> BDD-cost:    0
c ---[ 916]---> BDD-cost:    0
c ---[ 914]---> BDD-cost:    0
c ---[ 912]---> BDD-cost:    0
c ---[ 910]---> BDD-cost:    0
c ---[ 908]---> BDD-cost:    0
c ---[ 906]---> BDD-cost:    0
c ---[ 904]---> BDD-cost:   52
c ---[ 902]---> BDD-cost:   43
c ---[ 900]---> BDD-cost:   55
c ---[ 898]---> BDD-cost:   43
c ---[ 896]---> BDD-cost:   55
c ---[ 894]---> BDD-cost:   43
c ---[ 892]---> BDD-cost:   55
c ---[ 890]---> BDD-cost:   43
c ---[ 888]---> BDD-cost:   55
c ---[ 886]---> BDD-cost:   43
c ---[ 884]---> BDD-cost:   52
c ---[ 882]---> BDD-cost:   43
c ---[ 880]---> BDD-cost:   55
c ---[ 878]---> BDD-cost:   43
c ---[ 876]---> BDD-cost:   55
c ---[ 874]---> BDD-cost:   43
c ---[ 872]---> BDD-cost:   55
c ---[ 870]---> BDD-cost:   43
c ---[ 868]---> BDD-cost:   55
c ---[ 866]---> BDD-cost:   43
c ---[ 865]---> BDD-cost:    9
c ---[ 864]---> BDD-cost:    9
c ---[ 863]---> BDD-cost:    9
c ---[ 862]---> BDD-cost:    9
c ---[ 861]---> BDD-cost:    9
c ---[ 860]---> BDD-cost:    9
c ---[ 859]---> BDD-cost:    9
c ---[ 858]---> BDD-cost:    9
c ---[ 857]---> BDD-cost:    9
c ---[ 856]---> BDD-cost:    9
c ---[ 855]---> BDD-cost:    9
c ---[ 854]---> BDD-cost:    9
c ---[ 853]---> BDD-cost:    9
c ---[ 852]---> BDD-cost:    9
c ---[ 851]---> BDD-cost:    9
c ---[ 850]---> BDD-cost:    9
c ---[ 849]---> BDD-cost:    9
c ---[ 848]---> BDD-cost:    9
c ---[ 847]---> BDD-cost:    9
c ---[ 846]---> BDD-cost:    9
c ---[ 845]---> BDD-cost:    9
c ---[ 844]---> BDD-cost:    9
c ---[ 843]---> BDD-cost:    9
c ---[ 842]---> BDD-cost:    9
c ---[ 841]---> BDD-cost:    9
c ---[ 840]---> BDD-cost:    9
c ---[ 839]---> BDD-cost:    9
c ---[ 838]---> BDD-cost:    9
c ---[ 837]---> BDD-cost:    9
c ---[ 836]---> BDD-cost:    9
c ---[ 835]---> BDD-cost:    9
c ---[ 834]---> BDD-cost:    9
c ---[ 833]---> BDD-cost:    9
c ---[ 832]---> BDD-cost:    9
c ---[ 831]---> BDD-cost:    9
c ---[ 830]---> BDD-cost:    9
c ---[ 829]---> BDD-cost:    9
c ---[ 828]---> BDD-cost:    9
c ---[ 827]---> BDD-cost:    9
c ---[ 826]---> BDD-cost:    9
c ---[ 825]---> BDD-cost:    9
c ---[ 824]---> BDD-cost:    9
c ---[ 823]---> BDD-cost:    9
c ---[ 822]---> BDD-cost:    9
c ---[ 821]---> BDD-cost:    9
c ---[ 820]---> BDD-cost:    9
c ---[ 819]---> BDD-cost:    9
c ---[ 818]---> BDD-cost:    9
c ---[ 817]---> BDD-cost:    9
c ---[ 816]---> BDD-cost:    9
c ---[ 815]---> BDD-cost:    9
c ---[ 814]---> BDD-cost:    9
c ---[ 813]---> BDD-cost:    9
c ---[ 812]---> BDD-cost:    9
c ---[ 811]---> BDD-cost:    9
c ---[ 810]---> BDD-cost:    9
c ---[ 809]---> BDD-cost:    9
c ---[ 808]---> BDD-cost:    9
c ---[ 807]---> BDD-cost:    9
c ---[ 806]---> BDD-cost:    9
c ---[ 805]---> BDD-cost:    9
c ---[ 804]---> BDD-cost:    9
c ---[ 803]---> BDD-cost:    9
c ---[ 802]---> BDD-cost:    9
c ---[ 801]---> BDD-cost:    9
c ---[ 800]---> BDD-cost:    9
c ---[ 799]---> BDD-cost:    9
c ---[ 798]---> BDD-cost:    9
c ---[ 797]---> BDD-cost:    9
c ---[ 796]---> BDD-cost:    9
c ---[ 795]---> BDD-cost:    9
c ---[ 794]---> BDD-cost:    9
c ---[ 793]---> BDD-cost:    9
c ---[ 792]---> BDD-cost:    9
c ---[ 791]---> BDD-cost:    9
c ---[ 790]---> BDD-cost:    9
c ---[ 789]---> BDD-cost:    9
c ---[ 788]---> BDD-cost:    9
c ---[ 787]---> BDD-cost:    9
c ---[ 786]---> BDD-cost:    9
c ---[ 785]---> BDD-cost:    9
c ---[ 784]---> BDD-cost:    9
c ---[ 783]---> BDD-cost:    9
c ---[ 782]---> BDD-cost:    9
c ---[ 781]---> BDD-cost:    9
c ---[ 780]---> BDD-cost:    9
c ---[ 779]---> BDD-cost:    9
c ---[ 778]---> BDD-cost:    9
c ---[ 777]---> BDD-cost:    9
c ---[ 776]---> BDD-cost:    9
c ---[ 775]---> BDD-cost:    9
c ---[ 774]---> BDD-cost:    9
c ---[ 773]---> BDD-cost:    9
c ---[ 772]---> BDD-cost:    9
c ---[ 771]---> BDD-cost:    9
c ---[ 770]---> BDD-cost:    9
c ---[ 769]---> BDD-cost:    9
c ---[ 768]---> BDD-cost:    9
c ---[ 767]---> BDD-cost:    9
c ---[ 766]---> BDD-cost:    9
c ---[ 765]---> BDD-cost:    9
c ---[ 764]---> BDD-cost:    9
c ---[ 763]---> BDD-cost:    9
c ---[ 762]---> BDD-cost:    9
c ---[ 761]---> BDD-cost:    9
c ---[ 760]---> BDD-cost:    9
c ---[ 759]---> BDD-cost:    9
c ---[ 758]---> BDD-cost:    9
c ---[ 757]---> BDD-cost:    9
c ---[ 756]---> BDD-cost:    9
c ---[ 755]---> BDD-cost:    9
c ---[ 754]---> BDD-cost:    9
c ---[ 753]---> BDD-cost:    9
c ---[ 752]---> BDD-cost:    9
c ---[ 751]---> BDD-cost:    9
c ---[ 750]---> BDD-cost:    9
c ---[ 749]---> BDD-cost:    9
c ---[ 748]---> BDD-cost:    9
c ---[ 747]---> BDD-cost:    9
c ---[ 746]---> BDD-cost:    9
c ---[ 745]---> BDD-cost:    9
c ---[ 744]---> BDD-cost:    9
c ---[ 743]---> BDD-cost:    9
c ---[ 742]---> BDD-cost:    9
c ---[ 741]---> BDD-cost:    9
c ---[ 740]---> BDD-cost:    9
c ---[ 739]---> BDD-cost:    9
c ---[ 738]---> BDD-cost:    9
c ---[ 737]---> BDD-cost:    9
c ---[ 736]---> BDD-cost:    9
c ---[ 735]---> BDD-cost:    9
c ---[ 734]---> BDD-cost:    9
c ---[ 733]---> BDD-cost:    9
c ---[ 732]---> BDD-cost:    9
c ---[ 731]---> BDD-cost:    9
c ---[ 730]---> BDD-cost:    9
c ---[ 729]---> BDD-cost:    9
c ---[ 728]---> BDD-cost:    9
c ---[ 727]---> BDD-cost:    9
c ---[ 726]---> BDD-cost:    9
c ---[ 725]---> BDD-cost:    9
c ---[ 724]---> BDD-cost:    9
c ---[ 723]---> BDD-cost:    9
c ---[ 722]---> BDD-cost:    9
c ---[ 721]---> BDD-cost:    9
c ---[ 720]---> BDD-cost:    9
c ---[ 719]---> BDD-cost:    9
c ---[ 718]---> BDD-cost:    9
c ---[ 717]---> BDD-cost:    9
c ---[ 716]---> BDD-cost:    9
c ---[ 715]---> BDD-cost:    9
c ---[ 714]---> BDD-cost:    9
c ---[ 713]---> BDD-cost:    9
c ---[ 712]---> BDD-cost:    9
c ---[ 711]---> BDD-cost:    9
c ---[ 710]---> BDD-cost:    9
c ---[ 709]---> BDD-cost:    9
c ---[ 708]---> BDD-cost:    9
c ---[ 707]---> BDD-cost:    9
c ---[ 706]---> BDD-cost:    9
c ---[ 705]---> BDD-cost:    9
c ---[ 704]---> BDD-cost:    9
c ---[ 703]---> BDD-cost:    9
c ---[ 702]---> BDD-cost:    9
c ---[ 701]---> BDD-cost:    9
c ---[ 700]---> BDD-cost:    9
c ---[ 699]---> BDD-cost:    9
c ---[ 698]---> BDD-cost:    9
c ---[ 697]---> BDD-cost:    9
c ---[ 696]---> BDD-cost:    9
c ---[ 695]---> BDD-cost:    9
c ---[ 694]---> BDD-cost:    9
c ---[ 693]---> BDD-cost:    9
c ---[ 692]---> BDD-cost:    9
c ---[ 691]---> BDD-cost:    9
c ---[ 690]---> BDD-cost:    9
c ---[ 689]---> BDD-cost:    9
c ---[ 688]---> BDD-cost:    9
c ---[ 687]---> BDD-cost:    9
c ---[ 686]---> BDD-cost:    9
c ---[ 685]---> BDD-cost:    9
c ---[ 684]---> BDD-cost:    9
c ---[ 683]---> BDD-cost:    9
c ---[ 682]---> BDD-cost:    9
c ---[ 681]---> BDD-cost:    9
c ---[ 680]---> BDD-cost:    9
c ---[ 679]---> BDD-cost:    9
c ---[ 678]---> BDD-cost:    9
c ---[ 677]---> BDD-cost:    9
c ---[ 676]---> BDD-cost:    9
c ---[ 675]---> BDD-cost:    9
c ---[ 674]---> BDD-cost:    9
c ---[ 673]---> BDD-cost:    9
c ---[ 672]---> BDD-cost:    9
c ---[ 671]---> BDD-cost:    9
c ---[ 670]---> BDD-cost:    9
c ---[ 669]---> BDD-cost:    9
c ---[ 668]---> BDD-cost:    9
c ---[ 667]---> BDD-cost:    9
c ---[ 666]---> BDD-cost:    9
c ---[ 665]---> BDD-cost:    9
c ---[ 664]---> BDD-cost:    9
c ---[ 663]---> BDD-cost:    9
c ---[ 662]---> BDD-cost:    9
c ---[ 661]---> BDD-cost:    9
c ---[ 660]---> BDD-cost:    9
c ---[ 659]---> BDD-cost:    9
c ---[ 658]---> BDD-cost:    9
c ---[ 657]---> BDD-cost:    9
c ---[ 656]---> BDD-cost:    9
c ---[ 655]---> BDD-cost:    9
c ---[ 654]---> BDD-cost:    9
c ---[ 653]---> BDD-cost:    9
c ---[ 652]---> BDD-cost:    9
c ---[ 651]---> BDD-cost:    9
c ---[ 650]---> BDD-cost:    9
c ---[ 649]---> BDD-cost:    9
c ---[ 648]---> BDD-cost:    9
c ---[ 647]---> BDD-cost:    9
c ---[ 646]---> BDD-cost:    9
c ---[ 645]---> BDD-cost:    9
c ---[ 644]---> BDD-cost:    9
c ---[ 643]---> BDD-cost:    9
c ---[ 642]---> BDD-cost:    9
c ---[ 641]---> BDD-cost:    9
c ---[ 640]---> BDD-cost:    9
c ---[ 639]---> BDD-cost:    9
c ---[ 638]---> BDD-cost:    9
c ---[ 637]---> BDD-cost:    9
c ---[ 636]---> BDD-cost:    9
c ---[ 635]---> BDD-cost:    9
c ---[ 634]---> BDD-cost:    9
c ---[ 633]---> BDD-cost:    9
c ---[ 632]---> BDD-cost:    9
c ---[ 631]---> BDD-cost:    9
c ---[ 630]---> BDD-cost:    9
c ---[ 629]---> BDD-cost:    9
c ---[ 628]---> BDD-cost:    9
c ---[ 627]---> BDD-cost:    9
c ---[ 626]---> BDD-cost:    9
c ---[ 625]---> BDD-cost:    9
c ---[ 624]---> BDD-cost:    9
c ---[ 623]---> BDD-cost:    9
c ---[ 622]---> BDD-cost:    9
c ---[ 621]---> BDD-cost:    9
c ---[ 620]---> BDD-cost:    9
c ---[ 619]---> BDD-cost:    9
c ---[ 618]---> BDD-cost:    9
c ---[ 617]---> BDD-cost:    9
c ---[ 616]---> BDD-cost:    9
c ---[ 615]---> BDD-cost:    9
c ---[ 614]---> BDD-cost:    9
c ---[ 613]---> BDD-cost:    9
c ---[ 612]---> BDD-cost:    9
c ---[ 611]---> BDD-cost:    9
c ---[ 610]---> BDD-cost:    9
c ---[ 609]---> BDD-cost:    9
c ---[ 608]---> BDD-cost:    9
c ---[ 607]---> BDD-cost:    9
c ---[ 606]---> BDD-cost:    9
c ---[ 605]---> BDD-cost:    9
c ---[ 604]---> BDD-cost:    9
c ---[ 603]---> BDD-cost:    9
c ---[ 602]---> BDD-cost:    9
c ---[ 601]---> BDD-cost:    9
c ---[ 600]---> BDD-cost:    9
c ---[ 599]---> BDD-cost:    9
c ---[ 598]---> BDD-cost:    9
c ---[ 597]---> BDD-cost:    9
c ---[ 596]---> BDD-cost:    9
c ---[ 595]---> BDD-cost:    9
c ---[ 594]---> BDD-cost:    9
c ---[ 593]---> BDD-cost:    9
c ---[ 592]---> BDD-cost:    9
c ---[ 591]---> BDD-cost:    9
c ---[ 590]---> BDD-cost:    9
c ---[ 589]---> BDD-cost:    9
c ---[ 588]---> BDD-cost:    9
c ---[ 587]---> BDD-cost:    9
c ---[ 586]---> BDD-cost:    9
c ---[ 585]---> BDD-cost:    9
c ---[ 584]---> BDD-cost:    9
c ---[ 583]---> BDD-cost:    9
c ---[ 582]---> BDD-cost:    9
c ---[ 581]---> BDD-cost:    9
c ---[ 580]---> BDD-cost:    9
c ---[ 579]---> BDD-cost:    9
c ---[ 578]---> BDD-cost:    9
c ---[ 577]---> BDD-cost:    9
c ---[ 576]---> BDD-cost:    9
c ---[ 575]---> BDD-cost:    9
c ---[ 574]---> BDD-cost:    9
c ---[ 573]---> BDD-cost:    9
c ---[ 572]---> BDD-cost:    9
c ---[ 571]---> BDD-cost:    9
c ---[ 570]---> BDD-cost:    9
c ---[ 569]---> BDD-cost:    9
c ---[ 568]---> BDD-cost:    9
c ---[ 567]---> BDD-cost:    9
c ---[ 566]---> BDD-cost:    9
c ---[ 565]---> BDD-cost:    9
c ---[ 564]---> BDD-cost:    9
c ---[ 563]---> BDD-cost:    9
c ---[ 562]---> BDD-cost:    9
c ---[ 561]---> BDD-cost:    9
c ---[ 560]---> BDD-cost:    9
c ---[ 559]---> BDD-cost:    9
c ---[ 558]---> BDD-cost:    9
c ---[ 557]---> BDD-cost:    9
c ---[ 556]---> BDD-cost:    9
c ---[ 555]---> BDD-cost:    9
c ---[ 554]---> BDD-cost:    9
c ---[ 553]---> BDD-cost:    9
c ---[ 552]---> BDD-cost:    9
c ---[ 551]---> BDD-cost:    9
c ---[ 550]---> BDD-cost:    9
c ---[ 549]---> BDD-cost:    9
c ---[ 548]---> BDD-cost:    9
c ---[ 547]---> BDD-cost:    9
c ---[ 546]---> BDD-cost:    9
c ---[ 545]---> BDD-cost:    9
c ---[ 544]---> BDD-cost:    9
c ---[ 543]---> BDD-cost:    9
c ---[ 542]---> BDD-cost:    9
c ---[ 541]---> BDD-cost:    9
c ---[ 540]---> BDD-cost:    9
c ---[ 539]---> BDD-cost:    9
c ---[ 538]---> BDD-cost:    9
c ---[ 537]---> BDD-cost:    9
c ---[ 536]---> BDD-cost:    9
c ---[ 535]---> BDD-cost:    9
c ---[ 534]---> BDD-cost:    9
c ---[ 533]---> BDD-cost:    9
c ---[ 532]---> BDD-cost:    9
c ---[ 531]---> BDD-cost:    9
c ---[ 530]---> BDD-cost:    9
c ---[ 529]---> BDD-cost:    9
c ---[ 528]---> BDD-cost:    9
c ---[ 527]---> BDD-cost:    9
c ---[ 526]---> BDD-cost:    9
c ---[ 525]---> BDD-cost:    9
c ---[ 524]---> BDD-cost:    9
c ---[ 523]---> BDD-cost:    9
c ---[ 522]---> BDD-cost:    9
c ---[ 521]---> BDD-cost:    9
c ---[ 520]---> BDD-cost:    9
c ---[ 519]---> BDD-cost:    9
c ---[ 518]---> BDD-cost:    9
c ---[ 517]---> BDD-cost:    9
c ---[ 516]---> BDD-cost:    9
c ---[ 515]---> BDD-cost:    9
c ---[ 514]---> BDD-cost:    9
c ---[ 513]---> BDD-cost:    9
c ---[ 512]---> BDD-cost:    9
c ---[ 511]---> BDD-cost:    9
c ---[ 510]---> BDD-cost:    9
c ---[ 509]---> BDD-cost:    9
c ---[ 508]---> BDD-cost:    9
c ---[ 507]---> BDD-cost:    9
c ---[ 506]---> BDD-cost:    9
c ---[ 505]---> BDD-cost:    9
c ---[ 504]---> BDD-cost:    9
c ---[ 503]---> BDD-cost:    9
c ---[ 502]---> BDD-cost:    9
c ---[ 501]---> BDD-cost:    9
c ---[ 500]---> BDD-cost:    9
c ---[ 499]---> BDD-cost:    9
c ---[ 498]---> BDD-cost:    9
c ---[ 497]---> BDD-cost:    9
c ---[ 496]---> BDD-cost:    9
c ---[ 495]---> BDD-cost:    9
c ---[ 494]---> BDD-cost:    9
c ---[ 493]---> BDD-cost:    9
c ---[ 492]---> BDD-cost:    9
c ---[ 491]---> BDD-cost:    9
c ---[ 490]---> BDD-cost:    9
c ---[ 489]---> BDD-cost:    9
c ---[ 488]---> BDD-cost:    9
c ---[ 487]---> BDD-cost:    9
c ---[ 486]---> BDD-cost:    9
c ---[ 485]---> BDD-cost:    9
c ---[ 484]---> BDD-cost:    9
c ---[ 483]---> BDD-cost:    9
c ---[ 482]---> BDD-cost:    9
c ---[ 481]---> BDD-cost:    9
c ---[ 480]---> BDD-cost:    9
c ---[ 479]---> BDD-cost:    9
c ---[ 478]---> BDD-cost:    9
c ---[ 477]---> BDD-cost:    9
c ---[ 476]---> BDD-cost:    9
c ---[ 475]---> BDD-cost:    9
c ---[ 474]---> BDD-cost:    9
c ---[ 473]---> BDD-cost:    9
c ---[ 472]---> BDD-cost:    9
c ---[ 471]---> BDD-cost:    9
c ---[ 470]---> BDD-cost:    9
c ---[ 469]---> BDD-cost:    9
c ---[ 468]---> BDD-cost:    9
c ---[ 467]---> BDD-cost:    9
c ---[ 466]---> BDD-cost:    9
c ---[ 465]---> BDD-cost:    9
c ---[ 464]---> BDD-cost:    9
c ---[ 463]---> BDD-cost:    9
c ---[ 462]---> BDD-cost:    9
c ---[ 461]---> BDD-cost:    9
c ---[ 460]---> BDD-cost:    9
c ---[ 459]---> BDD-cost:    9
c ---[ 458]---> BDD-cost:    9
c ---[ 457]---> BDD-cost:    9
c ---[ 456]---> BDD-cost:    9
c ---[ 455]---> BDD-cost:    9
c ---[ 454]---> BDD-cost:    9
c ---[ 453]---> BDD-cost:    9
c ---[ 452]---> BDD-cost:    9
c ---[ 451]---> BDD-cost:    9
c ---[ 450]---> BDD-cost:    9
c ---[ 449]---> BDD-cost:    9
c ---[ 448]---> BDD-cost:    9
c ---[ 447]---> BDD-cost:    9
c ---[ 446]---> BDD-cost:    9
c ---[ 445]---> BDD-cost:    9
c ---[ 444]---> BDD-cost:    9
c ---[ 443]---> BDD-cost:    9
c ---[ 442]---> BDD-cost:    9
c ---[ 441]---> BDD-cost:    9
c ---[ 440]---> BDD-cost:    9
c ---[ 439]---> BDD-cost:    9
c ---[ 438]---> BDD-cost:    9
c ---[ 437]---> BDD-cost:    9
c ---[ 436]---> BDD-cost:    9
c ---[ 435]---> BDD-cost:    9
c ---[ 434]---> BDD-cost:    9
c ---[ 433]---> BDD-cost:    9
c ---[ 432]---> BDD-cost:    9
c ---[ 431]---> BDD-cost:    9
c ---[ 430]---> BDD-cost:    9
c ---[ 429]---> BDD-cost:    9
c ---[ 428]---> BDD-cost:    9
c ---[ 427]---> BDD-cost:    9
c ---[ 426]---> BDD-cost:    9
c ---[ 425]---> BDD-cost:    9
c ---[ 424]---> BDD-cost:    9
c ---[ 423]---> BDD-cost:    9
c ---[ 422]---> BDD-cost:    9
c ---[ 421]---> BDD-cost:    9
c ---[ 420]---> BDD-cost:    9
c ---[ 419]---> BDD-cost:    9
c ---[ 418]---> BDD-cost:    9
c ---[ 417]---> BDD-cost:    9
c ---[ 416]---> BDD-cost:    9
c ---[ 415]---> BDD-cost:    9
c ---[ 414]---> BDD-cost:    9
c ---[ 413]---> BDD-cost:    9
c ---[ 412]---> BDD-cost:    9
c ---[ 411]---> BDD-cost:    9
c ---[ 410]---> BDD-cost:    9
c ---[ 409]---> BDD-cost:    9
c ---[ 408]---> BDD-cost:    9
c ---[ 407]---> BDD-cost:    9
c ---[ 406]---> BDD-cost:    9
c ---[ 405]---> BDD-cost:    9
c ---[ 404]---> BDD-cost:    9
c ---[ 403]---> BDD-cost:    9
c ---[ 402]---> BDD-cost:    9
c ---[ 401]---> BDD-cost:    9
c ---[ 400]---> BDD-cost:    9
c ---[ 399]---> BDD-cost:    9
c ---[ 398]---> BDD-cost:    9
c ---[ 397]---> BDD-cost:    9
c ---[ 396]---> BDD-cost:    9
c ---[ 395]---> BDD-cost:    9
c ---[ 394]---> BDD-cost:    9
c ---[ 393]---> BDD-cost:    9
c ---[ 392]---> BDD-cost:    9
c ---[ 391]---> BDD-cost:    9
c ---[ 390]---> BDD-cost:    9
c ---[ 389]---> BDD-cost:    9
c ---[ 388]---> BDD-cost:    9
c ---[ 387]---> BDD-cost:    9
c ---[ 386]---> BDD-cost:    9
c ---[ 385]---> BDD-cost:    9
c ---[ 384]---> BDD-cost:    9
c ---[ 383]---> BDD-cost:    9
c ---[ 382]---> BDD-cost:    9
c ---[ 381]---> BDD-cost:    9
c ---[ 380]---> BDD-cost:    9
c ---[ 379]---> BDD-cost:    9
c ---[ 378]---> BDD-cost:    9
c ---[ 377]---> BDD-cost:    9
c ---[ 376]---> BDD-cost:    9
c ---[ 375]---> BDD-cost:    9
c ---[ 374]---> BDD-cost:    9
c ---[ 373]---> BDD-cost:    9
c ---[ 372]---> BDD-cost:    9
c ---[ 371]---> BDD-cost:    9
c ---[ 370]---> BDD-cost:    9
c ---[ 369]---> BDD-cost:    9
c ---[ 368]---> BDD-cost:    9
c ---[ 367]---> BDD-cost:    9
c ---[ 366]---> BDD-cost:    9
c ---[ 365]---> BDD-cost:    9
c ---[ 364]---> BDD-cost:    9
c ---[ 363]---> BDD-cost:    9
c ---[ 362]---> BDD-cost:    9
c ---[ 361]---> BDD-cost:    9
c ---[ 360]---> BDD-cost:    9
c ---[ 359]---> BDD-cost:    9
c ---[ 358]---> BDD-cost:    9
c ---[ 357]---> BDD-cost:    9
c ---[ 356]---> BDD-cost:    9
c ---[ 355]---> BDD-cost:    9
c ---[ 354]---> BDD-cost:    9
c ---[ 353]---> BDD-cost:    9
c ---[ 352]---> BDD-cost:    9
c ---[ 351]---> BDD-cost:    9
c ---[ 350]---> BDD-cost:    9
c ---[ 349]---> BDD-cost:    9
c ---[ 348]---> BDD-cost:    9
c ---[ 347]---> BDD-cost:    9
c ---[ 346]---> BDD-cost:    9
c ---[ 345]---> BDD-cost:    9
c ---[ 344]---> BDD-cost:    9
c ---[ 343]---> BDD-cost:    9
c ---[ 342]---> BDD-cost:    9
c ---[ 341]---> BDD-cost:    9
c ---[ 340]---> BDD-cost:    9
c ---[ 339]---> BDD-cost:    9
c ---[ 338]---> BDD-cost:    9
c ---[ 337]---> BDD-cost:    9
c ---[ 336]---> BDD-cost:    9
c ---[ 335]---> BDD-cost:    9
c ---[ 334]---> BDD-cost:    9
c ---[ 333]---> BDD-cost:    9
c ---[ 332]---> BDD-cost:    9
c ---[ 331]---> BDD-cost:    9
c ---[ 330]---> BDD-cost:    9
c ---[ 329]---> BDD-cost:    9
c ---[ 328]---> BDD-cost:    9
c ---[ 327]---> BDD-cost:    9
c ---[ 326]---> BDD-cost:    9
c ---[ 325]---> BDD-cost:    9
c ---[ 324]---> BDD-cost:    9
c ---[ 323]---> BDD-cost:    9
c ---[ 322]---> BDD-cost:    9
c ---[ 321]---> BDD-cost:    9
c ---[ 320]---> BDD-cost:    9
c ---[ 319]---> BDD-cost:    9
c ---[ 318]---> BDD-cost:    9
c ---[ 317]---> BDD-cost:    9
c ---[ 316]---> BDD-cost:    9
c ---[ 315]---> BDD-cost:    9
c ---[ 314]---> BDD-cost:    9
c ---[ 313]---> BDD-cost:    9
c ---[ 312]---> BDD-cost:    9
c ---[ 311]---> BDD-cost:    9
c ---[ 310]---> BDD-cost:    9
c ---[ 309]---> BDD-cost:    9
c ---[ 308]---> BDD-cost:    9
c ---[ 307]---> BDD-cost:    9
c ---[ 306]---> BDD-cost:    9
c ---[ 305]---> BDD-cost:    9
c ---[ 304]---> BDD-cost:    9
c ---[ 303]---> BDD-cost:    9
c ---[ 302]---> BDD-cost:    9
c ---[ 301]---> BDD-cost:    9
c ---[ 300]---> BDD-cost:    9
c ---[ 299]---> BDD-cost:    9
c ---[ 298]---> BDD-cost:    9
c ---[ 297]---> BDD-cost:    9
c ---[ 296]---> BDD-cost:    9
c ---[ 295]---> BDD-cost:    9
c ---[ 294]---> BDD-cost:    9
c ---[ 293]---> BDD-cost:    9
c ---[ 292]---> BDD-cost:    9
c ---[ 291]---> BDD-cost:    9
c ---[ 290]---> BDD-cost:    9
c ---[ 289]---> BDD-cost:    9
c ---[ 288]---> BDD-cost:    9
c ---[ 287]---> BDD-cost:    9
c ---[ 286]---> BDD-cost:    9
c ---[ 285]---> BDD-cost:    9
c ---[ 284]---> BDD-cost:    9
c ---[ 283]---> BDD-cost:    9
c ---[ 282]---> BDD-cost:    9
c ---[ 281]---> BDD-cost:    9
c ---[ 280]---> BDD-cost:    9
c ---[ 279]---> BDD-cost:    9
c ---[ 278]---> BDD-cost:    9
c ---[ 277]---> BDD-cost:    9
c ---[ 276]---> BDD-cost:    9
c ---[ 275]---> BDD-cost:    9
c ---[ 274]---> BDD-cost:    9
c ---[ 273]---> BDD-cost:    9
c ---[ 272]---> BDD-cost:    9
c ---[ 271]---> BDD-cost:    9
c ---[ 270]---> BDD-cost:    9
c ---[ 269]---> BDD-cost:    9
c ---[ 268]---> BDD-cost:    9
c ---[ 267]---> BDD-cost:    9
c ---[ 266]---> BDD-cost:    9
c ---[ 265]---> BDD-cost:    9
c ---[ 264]---> BDD-cost:    9
c ---[ 263]---> BDD-cost:    9
c ---[ 262]---> BDD-cost:    9
c ---[ 261]---> BDD-cost:    9
c ---[ 260]---> BDD-cost:    9
c ---[ 259]---> BDD-cost:    9
c ---[ 258]---> BDD-cost:    9
c ---[ 257]---> BDD-cost:    9
c ---[ 256]---> BDD-cost:    9
c ---[ 255]---> BDD-cost:    9
c ---[ 254]---> BDD-cost:    9
c ---[ 253]---> BDD-cost:    9
c ---[ 252]---> BDD-cost:    9
c ---[ 251]---> BDD-cost:    9
c ---[ 250]---> BDD-cost:    9
c ---[ 249]---> BDD-cost:    9
c ---[ 248]---> BDD-cost:    9
c ---[ 247]---> BDD-cost:    9
c ---[ 246]---> BDD-cost:    9
c ---[ 245]---> BDD-cost:    9
c ---[ 244]---> BDD-cost:    9
c ---[ 243]---> BDD-cost:    9
c ---[ 242]---> BDD-cost:    9
c ---[ 241]---> BDD-cost:    9
c ---[ 240]---> BDD-cost:    9
c ---[ 239]---> BDD-cost:    9
c ---[ 238]---> BDD-cost:    9
c ---[ 237]---> BDD-cost:    9
c ---[ 236]---> BDD-cost:    9
c ---[ 235]---> BDD-cost:    9
c ---[ 234]---> BDD-cost:    9
c ---[ 233]---> BDD-cost:    9
c ---[ 232]---> BDD-cost:    9
c ---[ 231]---> BDD-cost:    9
c ---[ 230]---> BDD-cost:    9
c ---[ 229]---> BDD-cost:    9
c ---[ 228]---> BDD-cost:    9
c ---[ 227]---> BDD-cost:    9
c ---[ 226]---> BDD-cost:    9
c ---[ 225]---> BDD-cost:    9
c ---[ 224]---> BDD-cost:    9
c ---[ 223]---> BDD-cost:    9
c ---[ 222]---> BDD-cost:    9
c ---[ 221]---> BDD-cost:    9
c ---[ 220]---> BDD-cost:    9
c ---[ 219]---> BDD-cost:    9
c ---[ 218]---> BDD-cost:    9
c ---[ 217]---> BDD-cost:    9
c ---[ 216]---> BDD-cost:    9
c ---[ 215]---> BDD-cost:    9
c ---[ 214]---> BDD-cost:    9
c ---[ 213]---> BDD-cost:    9
c ---[ 212]---> BDD-cost:    9
c ---[ 211]---> BDD-cost:    9
c ---[ 210]---> BDD-cost:    9
c ---[ 209]---> BDD-cost:    9
c ---[ 208]---> BDD-cost:    9
c ---[ 207]---> BDD-cost:    9
c ---[ 206]---> BDD-cost:    9
c ---[ 205]---> BDD-cost:    9
c ---[ 204]---> BDD-cost:    9
c ---[ 203]---> BDD-cost:    9
c ---[ 202]---> BDD-cost:    9
c ---[ 201]---> BDD-cost:    9
c ---[ 200]---> BDD-cost:    9
c ---[ 199]---> BDD-cost:    9
c ---[ 198]---> BDD-cost:    9
c ---[ 197]---> BDD-cost:    9
c ---[ 196]---> BDD-cost:    9
c ---[ 195]---> BDD-cost:    9
c ---[ 194]---> BDD-cost:    9
c ---[ 193]---> BDD-cost:    9
c ---[ 192]---> BDD-cost:    9
c ---[ 191]---> BDD-cost:    9
c ---[ 190]---> BDD-cost:    9
c ---[ 189]---> BDD-cost:    9
c ---[ 188]---> BDD-cost:    9
c ---[ 187]---> BDD-cost:    9
c ---[ 186]---> BDD-cost:    9
c ---[ 185]---> BDD-cost:    9
c ---[ 184]---> BDD-cost:    9
c ---[ 183]---> BDD-cost:    9
c ---[ 182]---> BDD-cost:    9
c ---[ 181]---> BDD-cost:    9
c ---[ 180]---> BDD-cost:    9
c ---[ 179]---> BDD-cost:    9
c ---[ 178]---> BDD-cost:    9
c ---[ 177]---> BDD-cost:    9
c ---[ 176]---> BDD-cost:    9
c ---[ 175]---> BDD-cost:    9
c ---[ 174]---> BDD-cost:    9
c ---[ 173]---> BDD-cost:    9
c ---[ 172]---> BDD-cost:    9
c ---[ 171]---> BDD-cost:    9
c ---[ 170]---> BDD-cost:    9
c ---[ 169]---> BDD-cost:    9
c ---[ 168]---> BDD-cost:    9
c ---[ 167]---> BDD-cost:    9
c ---[ 166]---> BDD-cost:    9
c ---[ 165]---> BDD-cost:    9
c ---[ 164]---> BDD-cost:    9
c ---[ 163]---> BDD-cost:    9
c ---[ 162]---> BDD-cost:    9
c ---[ 161]---> BDD-cost:    9
c ---[ 160]---> BDD-cost:    9
c ---[ 159]---> BDD-cost:    9
c ---[ 158]---> BDD-cost:    9
c ---[ 157]---> BDD-cost:    9
c ---[ 156]---> BDD-cost:    9
c ---[ 155]---> BDD-cost:    9
c ---[ 154]---> BDD-cost:    9
c ---[ 153]---> BDD-cost:    9
c ---[ 152]---> BDD-cost:    9
c ---[ 151]---> BDD-cost:    9
c ---[ 150]---> BDD-cost:    9
c ---[ 149]---> BDD-cost:    9
c ---[ 148]---> BDD-cost:    9
c ---[ 147]---> BDD-cost:    9
c ---[ 146]---> BDD-cost:    9
c ---[ 145]---> BDD-cost:    9
c ---[ 144]---> BDD-cost:    9
c ---[ 143]---> BDD-cost:    9
c ---[ 142]---> BDD-cost:    9
c ---[ 141]---> BDD-cost:    9
c ---[ 140]---> BDD-cost:    9
c ---[ 139]---> BDD-cost:    9
c ---[ 138]---> BDD-cost:    9
c ---[ 137]---> BDD-cost:    9
c ---[ 136]---> BDD-cost:    9
c ---[ 135]---> BDD-cost:    9
c ---[ 134]---> BDD-cost:    9
c ---[ 133]---> BDD-cost:    9
c ---[ 132]---> BDD-cost:    9
c ---[ 131]---> BDD-cost:    9
c ---[ 130]---> BDD-cost:    9
c ---[ 129]---> BDD-cost:    9
c ---[ 128]---> BDD-cost:    9
c ---[ 127]---> BDD-cost:    9
c ---[ 126]---> BDD-cost:    9
c ---[ 125]---> BDD-cost:    9
c ---[ 124]---> BDD-cost:    9
c ---[ 123]---> BDD-cost:    9
c ---[ 122]---> BDD-cost:    9
c ---[ 121]---> BDD-cost:    9
c ---[ 120]---> BDD-cost:    9
c ---[ 119]---> BDD-cost:    9
c ---[ 118]---> BDD-cost:    9
c ---[ 117]---> BDD-cost:    9
c ---[ 116]---> BDD-cost:    9
c ---[ 115]---> BDD-cost:    9
c ---[ 114]---> BDD-cost:    9
c ---[ 113]---> BDD-cost:    9
c ---[ 112]---> BDD-cost:    9
c ---[ 111]---> BDD-cost:    9
c ---[ 110]---> BDD-cost:    9
c ---[ 109]---> BDD-cost:    9
c ---[ 108]---> BDD-cost:    9
c ---[ 107]---> BDD-cost:    9
c ---[ 106]---> BDD-cost:    9
c ---[ 105]---> BDD-cost:    9
c ---[ 104]---> BDD-cost:    9
c ---[ 103]---> BDD-cost:    9
c ---[ 102]---> BDD-cost:    9
c ---[ 101]---> BDD-cost:    9
c ---[ 100]---> BDD-cost:    9
c ---[  99]---> BDD-cost:    9
c ---[  98]---> BDD-cost:    9
c ---[  97]---> BDD-cost:    9
c ---[  96]---> BDD-cost:    9
c ---[  95]---> BDD-cost:    9
c ---[  94]---> BDD-cost:    9
c ---[  93]---> BDD-cost:    9
c ---[  92]---> BDD-cost:    9
c ---[  91]---> BDD-cost:    9
c ---[  90]---> BDD-cost:    9
c ---[  89]---> BDD-cost:    9
c ---[  88]---> BDD-cost:    9
c ---[  87]---> BDD-cost:    9
c ---[  86]---> BDD-cost:    9
c ---[  85]---> BDD-cost:    9
c ---[  84]---> BDD-cost:    9
c ---[  83]---> BDD-cost:    9
c ---[  82]---> BDD-cost:    9
c ---[  81]---> BDD-cost:    9
c ---[  80]---> BDD-cost:    9
c ---[  79]---> BDD-cost:    9
c ---[  78]---> BDD-cost:    9
c ---[  77]---> BDD-cost:    9
c ---[  76]---> BDD-cost:    9
c ---[  75]---> BDD-cost:    9
c ---[  74]---> BDD-cost:    9
c ---[  73]---> BDD-cost:    9
c ---[  72]---> BDD-cost:    9
c ---[  71]---> BDD-cost:    9
c ---[  70]---> BDD-cost:    9
c ---[  69]---> BDD-cost:    9
c ---[  68]---> BDD-cost:    9
c ---[  67]---> BDD-cost:    9
c ---[  66]---> BDD-cost:    9
c ---[  65]---> BDD-cost:    9
c ---[  64]---> BDD-cost:    9
c ---[  63]---> BDD-cost:    9
c ---[  62]---> BDD-cost:    9
c ---[  61]---> BDD-cost:    9
c ---[  60]---> BDD-cost:    9
c ---[  59]---> BDD-cost:    9
c ---[  58]---> BDD-cost:    9
c ---[  57]---> BDD-cost:    9
c ---[  56]---> BDD-cost:    9
c ---[  55]---> BDD-cost:    9
c ---[  54]---> BDD-cost:    9
c ---[  53]---> BDD-cost:    9
c ---[  52]---> BDD-cost:    9
c ---[  51]---> BDD-cost:    9
c ---[  50]---> BDD-cost:    9
c ---[  49]---> BDD-cost:    9
c ---[  48]---> BDD-cost:    9
c ---[  47]---> BDD-cost:    9
c ---[  46]---> BDD-cost:    9
c ---[  45]---> BDD-cost:    9
c ---[  44]---> BDD-cost:    9
c ---[  43]---> BDD-cost:    9
c ---[  42]---> BDD-cost:    1
c ---[  41]---> BDD-cost:    1
c ---[  40]---> BDD-cost:    1
c ---[  39]---> BDD-cost:    1
c ---[  38]---> BDD-cost:    1
c ---[  37]---> Adder-cost: 580   maxlim: 294891   bits: 20/19
c ---[  36]---> Adder-cost: 578   maxlim: 262123   bits: 19/18
c ---[  35]---> Adder-cost: 540   maxlim: 163819   bits: 19/18
c ---[  34]---> Adder-cost: 580   maxlim: 294891   bits: 20/19
c ---[  33]---> Adder-cost: 578   maxlim: 262123   bits: 19/18
c ---[  32]---> Adder-cost: 540   maxlim: 163819   bits: 19/18
c ---[  31]---> Adder-cost: 590   maxlim: 327659   bits: 20/19
c ---[  30]---> Adder-cost: 580   maxlim: 294891   bits: 20/19
c ---[  29]---> Adder-cost: 578   maxlim: 262123   bits: 19/18
c ---[  28]---> Adder-cost: 540   maxlim: 163819   bits: 19/18
c ---[  27]---> Adder-cost: 590   maxlim: 327659   bits: 20/19
c ---[  26]---> Adder-cost: 580   maxlim: 294891   bits: 20/19
c ---[  25]---> Adder-cost: 578   maxlim: 262123   bits: 19/18
c ---[  24]---> Adder-cost: 540   maxlim: 163819   bits: 19/18
c ---[  23]---> Adder-cost: 590   maxlim: 327659   bits: 20/19
c ---[  22]---> Adder-cost: 580   maxlim: 294891   bits: 20/19
c ---[  21]---> Adder-cost: 578   maxlim: 262123   bits: 19/18
c ---[  20]---> Adder-cost: 540   maxlim: 163819   bits: 19/18
c ---[  19]---> Adder-cost: 590   maxlim: 327659   bits: 20/19
c ---[  18]---> Adder-cost: 590   maxlim: 327659   bits: 20/19
c ---[  17]---> Adder-cost: 590   maxlim: 327659   bits: 20/19
c ---[  16]---> Adder-cost: 590   maxlim: 327659   bits: 20/19
c ---[  15]---> Adder-cost: 590   maxlim: 327659   bits: 20/19
c ---[  14]---> Adder-cost: 590   maxlim: 327659   bits: 20/19
c ---[  13]---> Adder-cost: 590   maxlim: 327659   bits: 20/19
c ---[  12]---> Adder-cost: 590   maxlim: 327659   bits: 20/19
c ---[  11]---> Adder-cost: 590   maxlim: 327659   bits: 20/19
c ---[  10]---> Adder-cost: 580   maxlim: 294891   bits: 20/19
c ---[   9]---> Adder-cost: 578   maxlim: 262123   bits: 19/18
c ---[   8]---> Adder-cost: 540   maxlim: 163819   bits: 19/18
c ---[   7]---> Adder-cost: 590   maxlim: 327659   bits: 20/19
c ---[   6]---> Adder-cost: 580   maxlim: 294891   bits: 20/19
c ---[   5]---> Adder-cost: 578   maxlim: 262123   bits: 19/18
c ---[   4]---> Adder-cost: 540   maxlim: 163819   bits: 19/18
c ---[   3]---> Adder-cost: 590   maxlim: 327659   bits: 20/19
c ---[   2]---> Adder-cost: 580   maxlim: 294891   bits: 20/19
c ---[   1]---> Adder-cost: 578   maxlim: 262123   bits: 19/18
c ---[   0]---> Adder-cost: 540   maxlim: 163819   bits: 19/18
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 | 1627409  4551349 |  542469       0        0     nan |  0.000 % |
c |       101 | 1627409  4551349 |  596715     101      313     3.1 |  2.961 % |
c |       251 | 1627409  4551349 |  656387     251      801     3.2 |  2.961 % |
c |       477 | 1627358  4551237 |  722026     461     1674     3.6 |  2.964 % |
c |       814 | 1627332  4551179 |  794228     795     3061     3.9 |  2.966 % |
c |      1320 | 1627323  4551148 |  873651    1298     4959     3.8 |  2.966 % |
c |      2079 | 1627241  4550965 |  961016    2043     7619     3.7 |  2.970 % |
c |      3218 | 1627196  4550858 | 1057118    3174    12375     3.9 |  2.973 % |
c |      4926 | 1627046  4550513 | 1162830    4853    18854     3.9 |  2.982 % |
c |      7488 | 1626793  4549949 | 1279113    7375    29565     4.0 |  2.998 % |
c |     11332 | 1625955  4548093 | 1407024   11101    46362     4.2 |  3.049 % |
c |     17098 | 1624802  4545541 | 1547727   16693    75096     4.5 |  3.118 % |
c |     25747 | 1624063  4543864 | 1702500   25211   136926     5.4 |  3.159 % |
c |     38721 | 1623456  4542497 | 1872750   38067   352392     9.3 |  3.194 % |
c |     58183 | 1621866  4538984 | 2060025   57245   555330     9.7 |  3.293 % |
c |     87376 | 1620677  4536321 | 2266027   86236  1178227    13.7 |  3.367 % |
c |    131165 | 1618765  4532127 | 2492630  129665  2934673    22.6 |  3.492 % |
c |    196852 | 1616277  4526616 | 2741893  194915  5734949    29.4 |  3.647 % |
/oldhome/oroussel/solvers/minisat+_script: line 9: 11014 CPU time limit exceeded $XDIR/minisat+_64-bit_static -try "$@"
#### 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.86 0.94 0.95 2/54 11010
Raw data (stat): 11010 (runsolver) R 11009 22056 22055 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 842193646 1052672 99 4294967295 134512640 135381576 3221224480 3221219688 135158418 0 2147483391 7 90112 0 0 0 17 0 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0004 s]
Raw data (loadavg): 0.88 0.94 0.95 2/55 11014
Raw data (stat): 11010 (minisat+_script) S 11009 22056 22055 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842193646 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+20.001 s]
Raw data (loadavg): 0.90 0.94 0.95 2/55 11014
Raw data (stat): 11010 (minisat+_script) S 11009 22056 22055 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842193646 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+30.0018 s]
Raw data (loadavg): 0.92 0.94 0.95 3/55 11014
Raw data (stat): 11010 (minisat+_script) S 11009 22056 22055 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842193646 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+40.0017 s]
Raw data (loadavg): 0.93 0.94 0.95 2/55 11014
Raw data (stat): 11010 (minisat+_script) S 11009 22056 22055 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842193646 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+50.0024 s]
Raw data (loadavg): 0.94 0.95 0.95 2/55 11014
Raw data (stat): 11010 (minisat+_script) S 11009 22056 22055 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842193646 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+60.0021 s]
Raw data (loadavg): 0.95 0.95 0.95 2/55 11014
Raw data (stat): 11010 (minisat+_script) S 11009 22056 22055 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842193646 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+70.0029 s]
Raw data (loadavg): 0.96 0.95 0.95 2/55 11014
Raw data (stat): 11010 (minisat+_script) S 11009 22056 22055 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842193646 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+80.0027 s]
Raw data (loadavg): 0.96 0.95 0.95 2/55 11014
Raw data (stat): 11010 (minisat+_script) S 11009 22056 22055 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842193646 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+90.0025 s]
Raw data (loadavg): 0.97 0.95 0.95 2/55 11014
Raw data (stat): 11010 (minisat+_script) S 11009 22056 22055 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842193646 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+100.003 s]
Raw data (loadavg): 0.97 0.95 0.95 2/55 11014
Raw data (stat): 11010 (minisat+_script) S 11009 22056 22055 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842193646 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+110.002 s]
Raw data (loadavg): 0.98 0.95 0.95 2/55 11014
Raw data (stat): 11010 (minisat+_script) S 11009 22056 22055 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842193646 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+120.003 s]
Raw data (loadavg): 0.98 0.95 0.95 2/55 11014
Raw data (stat): 11010 (minisat+_script) S 11009 22056 22055 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842193646 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+130.003 s]
Raw data (loadavg): 0.98 0.95 0.95 2/55 11014
Raw data (stat): 11010 (minisat+_script) S 11009 22056 22055 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842193646 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+140.002 s]
Raw data (loadavg): 0.98 0.95 0.95 2/55 11014
Raw data (stat): 11010 (minisat+_script) S 11009 22056 22055 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842193646 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+150.002 s]
Raw data (loadavg): 0.99 0.96 0.95 2/55 11014
Raw data (stat): 11010 (minisat+_script) S 11009 22056 22055 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842193646 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+160.002 s]
Raw data (loadavg): 0.99 0.96 0.95 2/55 11014
Raw data (stat): 11010 (minisat+_script) S 11009 22056 22055 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842193646 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+170.002 s]
Raw data (loadavg): 0.99 0.96 0.95 2/55 11014
Raw data (stat): 11010 (minisat+_script) S 11009 22056 22055 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842193646 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+180.002 s]
Raw data (loadavg): 0.99 0.96 0.95 2/55 11014
Raw data (stat): 11010 (minisat+_script) S 11009 22056 22055 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842193646 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+190.002 s]
Raw data (loadavg): 0.99 0.96 0.95 2/55 11014
Raw data (stat): 11010 (minisat+_script) S 11009 22056 22055 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842193646 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+200.002 s]
Raw data (loadavg): 0.99 0.96 0.95 2/55 11014
Raw data (stat): 11010 (minisat+_script) S 11009 22056 22055 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842193646 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+210.002 s]
Raw data (loadavg): 0.99 0.96 0.95 2/55 11014
Raw data (stat): 11010 (minisat+_script) S 11009 22056 22055 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842193646 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+220.003 s]
Raw data (loadavg): 0.99 0.96 0.95 2/55 11014
Raw data (stat): 11010 (minisat+_script) S 11009 22056 22055 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842193646 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+230.003 s]
Raw data (loadavg): 0.99 0.96 0.95 2/55 11014
Raw data (stat): 11010 (minisat+_script) S 11009 22056 22055 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842193646 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+240.002 s]
Raw data (loadavg): 0.99 0.96 0.95 2/55 11014
Raw data (stat): 11010 (minisat+_script) S 11009 22056 22055 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842193646 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+250.003 s]
Raw data (loadavg): 0.99 0.97 0.95 2/55 11014
Raw data (stat): 11010 (minisat+_script) S 11009 22056 22055 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842193646 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+260.002 s]
Raw data (loadavg): 0.99 0.97 0.95 2/55 11014
Raw data (stat): 11010 (minisat+_script) S 11009 22056 22055 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842193646 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+270.002 s]
Raw data (loadavg): 0.99 0.97 0.95 2/55 11014
Raw data (stat): 11010 (minisat+_script) S 11009 22056 22055 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842193646 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+280.002 s]
Raw data (loadavg): 0.99 0.97 0.95 2/55 11014
Raw data (stat): 11010 (minisat+_script) S 11009 22056 22055 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842193646 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+290.002 s]
Raw data (loadavg): 0.99 0.97 0.95 2/55 11014
Raw data (stat): 11010 (minisat+_script) S 11009 22056 22055 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842193646 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+300.002 s]
Raw data (loadavg): 0.99 0.97 0.95 2/55 11014
Raw data (stat): 11010 (minisat+_script) S 11009 22056 22055 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842193646 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+310.002 s]
Raw data (loadavg): 0.99 0.97 0.95 2/55 11014
Raw data (stat): 11010 (minisat+_script) S 11009 22056 22055 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842193646 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+320.003 s]
Raw data (loadavg): 0.99 0.97 0.95 2/55 11014
Raw data (stat): 11010 (minisat+_script) S 11009 22056 22055 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842193646 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+330.003 s]
Raw data (loadavg): 0.99 0.97 0.95 2/55 11014
Raw data (stat): 11010 (minisat+_script) S 11009 22056 22055 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842193646 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+340.002 s]
Raw data (loadavg): 0.99 0.97 0.95 2/55 11014
Raw data (stat): 11010 (minisat+_script) S 11009 22056 22055 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842193646 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+350.002 s]
Raw data (loadavg): 0.99 0.97 0.95 2/55 11014
Raw data (stat): 11010 (minisat+_script) S 11009 22056 22055 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842193646 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+360.002 s]
Raw data (loadavg): 0.99 0.97 0.95 2/55 11014
Raw data (stat): 11010 (minisat+_script) S 11009 22056 22055 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842193646 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+370.002 s]
Raw data (loadavg): 0.99 0.97 0.95 2/55 11014
Raw data (stat): 11010 (minisat+_script) S 11009 22056 22055 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842193646 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+380.002 s]
Raw data (loadavg): 0.99 0.97 0.95 2/55 11014
Raw data (stat): 11010 (minisat+_script) S 11009 22056 22055 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842193646 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+390.002 s]
Raw data (loadavg): 0.99 0.97 0.95 2/55 11014
Raw data (stat): 11010 (minisat+_script) S 11009 22056 22055 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842193646 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+400.003 s]
Raw data (loadavg): 0.99 0.97 0.95 2/55 11014
Raw data (stat): 11010 (minisat+_script) S 11009 22056 22055 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842193646 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+410.003 s]
Raw data (loadavg): 0.99 0.97 0.95 2/55 11014
Raw data (stat): 11010 (minisat+_script) S 11009 22056 22055 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842193646 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+420.003 s]
Raw data (loadavg): 0.99 0.97 0.95 2/55 11014
Raw data (stat): 11010 (minisat+_script) S 11009 22056 22055 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842193646 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+430.003 s]
Raw data (loadavg): 0.99 0.97 0.95 2/55 11014
Raw data (stat): 11010 (minisat+_script) S 11009 22056 22055 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842193646 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+440.003 s]
Raw data (loadavg): 0.99 0.97 0.95 2/55 11014
Raw data (stat): 11010 (minisat+_script) S 11009 22056 22055 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842193646 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+450.003 s]
Raw data (loadavg): 0.99 0.97 0.95 2/55 11014
Raw data (stat): 11010 (minisat+_script) S 11009 22056 22055 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842193646 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+460.003 s]
Raw data (loadavg): 0.99 0.97 0.95 2/55 11014
Raw data (stat): 11010 (minisat+_script) S 11009 22056 22055 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842193646 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+470.004 s]
Raw data (loadavg): 0.99 0.97 0.95 2/55 11014
Raw data (stat): 11010 (minisat+_script) S 11009 22056 22055 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842193646 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+480.003 s]
Raw data (loadavg): 0.99 0.97 0.95 2/55 11014
Raw data (stat): 11010 (minisat+_script) S 11009 22056 22055 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842193646 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+490.004 s]
Raw data (loadavg): 0.99 0.97 0.95 2/55 11014
Raw data (stat): 11010 (minisat+_script) S 11009 22056 22055 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842193646 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+500.005 s]
Raw data (loadavg): 0.99 0.97 0.95 2/55 11014
Raw data (stat): 11010 (minisat+_script) S 11009 22056 22055 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842193646 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+510.005 s]
Raw data (loadavg): 0.99 0.97 0.95 2/55 11014
Raw data (stat): 11010 (minisat+_script) S 11009 22056 22055 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842193646 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+520.005 s]
Raw data (loadavg): 0.99 0.97 0.95 2/55 11014
Raw data (stat): 11010 (minisat+_script) S 11009 22056 22055 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842193646 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+530.005 s]
Raw data (loadavg): 0.99 0.97 0.95 2/55 11014
Raw data (stat): 11010 (minisat+_script) S 11009 22056 22055 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842193646 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+540.005 s]
Raw data (loadavg): 0.99 0.97 0.95 2/55 11014
Raw data (stat): 11010 (minisat+_script) S 11009 22056 22055 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842193646 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+550.006 s]
Raw data (loadavg): 0.99 0.97 0.95 2/55 11014
Raw data (stat): 11010 (minisat+_script) S 11009 22056 22055 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842193646 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+560.005 s]
Raw data (loadavg): 0.99 0.97 0.95 2/55 11014
Raw data (stat): 11010 (minisat+_script) S 11009 22056 22055 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842193646 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+570.006 s]
Raw data (loadavg): 0.99 0.97 0.95 2/55 11014
Raw data (stat): 11010 (minisat+_script) S 11009 22056 22055 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842193646 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+580.006 s]
Raw data (loadavg): 0.99 0.97 0.95 2/55 11014
Raw data (stat): 11010 (minisat+_script) S 11009 22056 22055 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842193646 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+590.006 s]
Raw data (loadavg): 0.99 0.97 0.95 2/55 11014
Raw data (stat): 11010 (minisat+_script) S 11009 22056 22055 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842193646 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+600.006 s]
Raw data (loadavg): 0.99 0.97 0.95 2/55 11014
Raw data (stat): 11010 (minisat+_script) S 11009 22056 22055 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842193646 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+610.006 s]
Raw data (loadavg): 0.99 0.97 0.95 2/55 11014
Raw data (stat): 11010 (minisat+_script) S 11009 22056 22055 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842193646 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+620.007 s]
Raw data (loadavg): 0.99 0.97 0.95 2/55 11014
Raw data (stat): 11010 (minisat+_script) S 11009 22056 22055 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842193646 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+630.006 s]
Raw data (loadavg): 0.99 0.97 0.95 2/55 11014
Raw data (stat): 11010 (minisat+_script) S 11009 22056 22055 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842193646 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+640.008 s]
Raw data (loadavg): 0.99 0.97 0.95 2/55 11014
Raw data (stat): 11010 (minisat+_script) S 11009 22056 22055 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842193646 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+650.007 s]
Raw data (loadavg): 0.99 0.97 0.95 2/55 11014
Raw data (stat): 11010 (minisat+_script) S 11009 22056 22055 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842193646 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+660.007 s]
Raw data (loadavg): 0.99 0.97 0.95 2/55 11014
Raw data (stat): 11010 (minisat+_script) S 11009 22056 22055 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842193646 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+670.007 s]
Raw data (loadavg): 0.99 0.97 0.95 2/55 11014
Raw data (stat): 11010 (minisat+_script) S 11009 22056 22055 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842193646 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+680.008 s]
Raw data (loadavg): 0.99 0.97 0.95 2/55 11014
Raw data (stat): 11010 (minisat+_script) S 11009 22056 22055 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842193646 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+690.008 s]
Raw data (loadavg): 0.99 0.97 0.95 2/55 11014
Raw data (stat): 11010 (minisat+_script) S 11009 22056 22055 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842193646 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+700.008 s]
Raw data (loadavg): 0.99 0.97 0.95 2/55 11014
Raw data (stat): 11010 (minisat+_script) S 11009 22056 22055 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842193646 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+710.008 s]
Raw data (loadavg): 0.99 0.97 0.95 2/55 11014
Raw data (stat): 11010 (minisat+_script) S 11009 22056 22055 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842193646 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+720.008 s]
Raw data (loadavg): 0.99 0.97 0.95 2/55 11014
Raw data (stat): 11010 (minisat+_script) S 11009 22056 22055 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842193646 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+730.009 s]
Raw data (loadavg): 0.99 0.97 0.95 2/55 11014
Raw data (stat): 11010 (minisat+_script) S 11009 22056 22055 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842193646 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+740.01 s]
Raw data (loadavg): 0.99 0.97 0.95 2/55 11014
Raw data (stat): 11010 (minisat+_script) S 11009 22056 22055 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842193646 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+750.01 s]
Raw data (loadavg): 0.99 0.97 0.95 2/55 11014
Raw data (stat): 11010 (minisat+_script) S 11009 22056 22055 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842193646 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+760.01 s]
Raw data (loadavg): 0.99 0.97 0.95 2/55 11014
Raw data (stat): 11010 (minisat+_script) S 11009 22056 22055 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842193646 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+770.01 s]
Raw data (loadavg): 0.99 0.97 0.95 2/55 11014
Raw data (stat): 11010 (minisat+_script) S 11009 22056 22055 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842193646 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+780.01 s]
Raw data (loadavg): 0.99 0.97 0.95 2/55 11014
Raw data (stat): 11010 (minisat+_script) S 11009 22056 22055 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842193646 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+790.011 s]
Raw data (loadavg): 0.99 0.97 0.95 2/55 11014
Raw data (stat): 11010 (minisat+_script) S 11009 22056 22055 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842193646 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+800.011 s]
Raw data (loadavg): 0.99 0.97 0.95 2/55 11014
Raw data (stat): 11010 (minisat+_script) S 11009 22056 22055 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842193646 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+810.01 s]
Raw data (loadavg): 0.99 0.97 0.95 2/55 11014
Raw data (stat): 11010 (minisat+_script) S 11009 22056 22055 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842193646 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+820.011 s]
Raw data (loadavg): 1.07 0.99 0.96 2/55 11014
Raw data (stat): 11010 (minisat+_script) S 11009 22056 22055 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842193646 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+830.011 s]
Raw data (loadavg): 1.06 0.99 0.96 2/55 11014
Raw data (stat): 11010 (minisat+_script) S 11009 22056 22055 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842193646 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+840.012 s]
Raw data (loadavg): 1.05 0.99 0.96 2/55 11014
Raw data (stat): 11010 (minisat+_script) S 11009 22056 22055 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842193646 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+850.012 s]
Raw data (loadavg): 1.04 0.99 0.96 2/55 11014
Raw data (stat): 11010 (minisat+_script) S 11009 22056 22055 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842193646 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+860.012 s]
Raw data (loadavg): 1.04 0.99 0.96 2/55 11014
Raw data (stat): 11010 (minisat+_script) S 11009 22056 22055 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842193646 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+870.012 s]
Raw data (loadavg): 1.03 0.99 0.96 2/55 11014
Raw data (stat): 11010 (minisat+_script) S 11009 22056 22055 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842193646 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+880.012 s]
Raw data (loadavg): 1.03 0.99 0.96 2/55 11014
Raw data (stat): 11010 (minisat+_script) S 11009 22056 22055 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842193646 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+890.013 s]
Raw data (loadavg): 1.02 0.99 0.96 2/55 11014
Raw data (stat): 11010 (minisat+_script) S 11009 22056 22055 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842193646 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+900.012 s]
Raw data (loadavg): 1.02 0.99 0.96 2/55 11014
Raw data (stat): 11010 (minisat+_script) S 11009 22056 22055 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842193646 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+910.013 s]
Raw data (loadavg): 1.09 1.00 0.96 2/55 11014
Raw data (stat): 11010 (minisat+_script) S 11009 22056 22055 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842193646 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+920.013 s]
Raw data (loadavg): 1.07 1.00 0.96 2/55 11014
Raw data (stat): 11010 (minisat+_script) S 11009 22056 22055 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842193646 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+930.013 s]
Raw data (loadavg): 1.06 1.00 0.96 2/55 11014
Raw data (stat): 11010 (minisat+_script) S 11009 22056 22055 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842193646 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+940.013 s]
Raw data (loadavg): 1.05 1.00 0.96 2/55 11014
Raw data (stat): 11010 (minisat+_script) S 11009 22056 22055 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842193646 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+950.013 s]
Raw data (loadavg): 1.04 1.00 0.96 2/55 11014
Raw data (stat): 11010 (minisat+_script) S 11009 22056 22055 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842193646 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+960.012 s]
Raw data (loadavg): 1.04 1.00 0.96 2/55 11014
Raw data (stat): 11010 (minisat+_script) S 11009 22056 22055 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842193646 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+970.012 s]
Raw data (loadavg): 1.03 1.00 0.96 2/55 11014
Raw data (stat): 11010 (minisat+_script) S 11009 22056 22055 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842193646 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+980.012 s]
Raw data (loadavg): 1.02 1.00 0.96 2/55 11014
Raw data (stat): 11010 (minisat+_script) S 11009 22056 22055 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842193646 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+990.012 s]
Raw data (loadavg): 1.02 1.00 0.96 2/55 11014
Raw data (stat): 11010 (minisat+_script) S 11009 22056 22055 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842193646 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1000.01 s]
Raw data (loadavg): 1.02 1.00 0.96 2/55 11014
Raw data (stat): 11010 (minisat+_script) S 11009 22056 22055 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842193646 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1010.01 s]
Raw data (loadavg): 1.01 1.00 0.96 2/55 11014
Raw data (stat): 11010 (minisat+_script) S 11009 22056 22055 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842193646 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1020.01 s]
Raw data (loadavg): 1.01 1.00 0.96 2/55 11014
Raw data (stat): 11010 (minisat+_script) S 11009 22056 22055 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842193646 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1030.01 s]
Raw data (loadavg): 1.01 1.00 0.96 2/55 11014
Raw data (stat): 11010 (minisat+_script) S 11009 22056 22055 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842193646 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1040.01 s]
Raw data (loadavg): 1.01 1.00 0.96 2/55 11014
Raw data (stat): 11010 (minisat+_script) S 11009 22056 22055 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842193646 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1050.01 s]
Raw data (loadavg): 1.01 1.00 0.96 2/55 11014
Raw data (stat): 11010 (minisat+_script) S 11009 22056 22055 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842193646 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1060.01 s]
Raw data (loadavg): 1.00 1.00 0.96 2/55 11014
Raw data (stat): 11010 (minisat+_script) S 11009 22056 22055 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842193646 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1070.01 s]
Raw data (loadavg): 1.00 1.00 0.96 2/55 11014
Raw data (stat): 11010 (minisat+_script) S 11009 22056 22055 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842193646 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1080.01 s]
Raw data (loadavg): 1.00 1.00 0.96 2/55 11014
Raw data (stat): 11010 (minisat+_script) S 11009 22056 22055 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842193646 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1090.01 s]
Raw data (loadavg): 1.00 1.00 0.96 2/55 11014
Raw data (stat): 11010 (minisat+_script) S 11009 22056 22055 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842193646 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1100.01 s]
Raw data (loadavg): 1.00 1.00 0.96 2/55 11014
Raw data (stat): 11010 (minisat+_script) S 11009 22056 22055 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842193646 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1110.01 s]
Raw data (loadavg): 1.00 1.00 0.96 2/55 11014
Raw data (stat): 11010 (minisat+_script) S 11009 22056 22055 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842193646 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1120.01 s]
Raw data (loadavg): 1.00 1.00 0.96 2/55 11014
Raw data (stat): 11010 (minisat+_script) S 11009 22056 22055 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842193646 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1130.01 s]
Raw data (loadavg): 1.22 1.05 0.98 2/55 11067
Raw data (stat): 11010 (minisat+_script) S 11009 22056 22055 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842193646 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1140.02 s]
Raw data (loadavg): 1.19 1.05 0.98 2/55 11067
Raw data (stat): 11010 (minisat+_script) S 11009 22056 22055 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842193646 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1150.02 s]
Raw data (loadavg): 1.16 1.04 0.98 2/55 11067
Raw data (stat): 11010 (minisat+_script) S 11009 22056 22055 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842193646 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1160.02 s]
Raw data (loadavg): 1.13 1.04 0.98 2/55 11067
Raw data (stat): 11010 (minisat+_script) S 11009 22056 22055 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842193646 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1170.02 s]
Raw data (loadavg): 1.11 1.04 0.98 2/55 11067
Raw data (stat): 11010 (minisat+_script) S 11009 22056 22055 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842193646 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1180.02 s]
Raw data (loadavg): 1.09 1.04 0.98 2/55 11067
Raw data (stat): 11010 (minisat+_script) S 11009 22056 22055 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842193646 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1190.02 s]
Raw data (loadavg): 1.08 1.04 0.98 2/55 11067
Raw data (stat): 11010 (minisat+_script) S 11009 22056 22055 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842193646 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1200.02 s]
Raw data (loadavg): 1.07 1.04 0.98 2/55 11069
Raw data (stat): 11010 (minisat+_script) S 11009 22056 22055 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842193646 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1210.02 s]
Raw data (loadavg): 1.06 1.03 0.98 2/55 11069
Raw data (stat): 11010 (minisat+_script) S 11009 22056 22055 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842193646 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1220.02 s]
Raw data (loadavg): 1.05 1.03 0.98 2/55 11069
Raw data (stat): 11010 (minisat+_script) S 11009 22056 22055 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842193646 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1229.79 s]
Raw data (loadavg): 1.04 1.03 0.98 1/53 11069
Raw data (stat): 11010 (minisat+_script) S 11009 22056 22055 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842193646 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 0

Child status: 152
Real time (s): 1229.79
CPU time (s): 1229.93
CPU user time (s): 1228.44
CPU system time (s): 1.48777
CPU usage (%): 100.011
Max. virtual memory (Kb): 2124
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####