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:
  1. 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.
  2. SOLVER DATA
    This is the output of the solver (stdout and stderr).
    Note that some very long lines in this section may be truncated by your web browser !
  3. 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.
  4. 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

Namemps-v2-20-10/plato.asu.edu/pub/milp/normalized-mps-v2-20-10-swath3.opb
MD5SUM2570fb3c524f5be873ba701d5990d98b
Bench Categoryoptimization, big integers (OPTBIGINT)
Has Objective FunctionYES
Satisfiable
(Un)Satisfiability was proved
Best value of the objective function
Optimality of the best value was proved
Number of terms in the objective function 31
Biggest coefficient in the objective function 1073741824
Number of bits for the biggest coefficient in the objective function 31
Sum of the numbers in the objective function 2147483647
Number of bits of the sum of numbers in the objective function 31
Biggest number in a constraint 1073741824000000
Number of bits of the biggest number in a constraint 50
Biggest sum of numbers in a constraint 4776342294353942
Number of bits of the biggest sum of numbers53
Best result obtained on this benchmark
Best CPU time to get the best result obtained on this benchmark
Number of variables49335
Total number of constraints7608
Number of constraints which are clauses0
Number of constraints which are cardinality constraints (but not clauses)2915
Number of constraints which are nor clauses,nor cardinality constraints4693
Minimum length of a constraint1
Maximum length of a constraint46934

Trace number 5896

Launcher Data

LAUNCH ON wulflinc20 THE 2005-09-20 01:46:17 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=3085 boxname=wulflinc20 idbench=741 idsolver=3 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  2570fb3c524f5be873ba701d5990d98b  /oldhome/oroussel/tmp/wulflinc20/normalized-mps-v2-20-10-swath3.opb
REAL COMMAND:  minisat+_script /oldhome/oroussel/tmp/wulflinc20/normalized-mps-v2-20-10-swath3.opb
IDLAUNCH: 3085
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.215
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.215
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:        897316 kB
Buffers:         11968 kB
Cached:          94944 kB
SwapCached:        800 kB
Active:          38880 kB
Inactive:        70736 kB
HighTotal:      131008 kB
HighFree:        32312 kB
LowTotal:       903652 kB
LowFree:        865004 kB
SwapTotal:     2097892 kB
SwapFree:      2096636 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           5736 kB
Slab:            21896 kB
Committed_AS:    64132 kB
PageTables:        328 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-09-20 01:56:13 (client local time) WITH STATUS 0 IN 574.454 SECONDS
stats: 3085 7 574.454 0

Solver Data

c Parsing PB file...
c PARSE ERROR! [line 13534] Integer overflow. Use BigNum-version.
c OK -- Running BigNum-version instead...
c Parsing PB file...
c Converting 4604 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: #######################################################################################################
c   -- Clauses(.)/Splits(s): (none)
c ---[4603]---> BDD-cost:   10
c ---[4602]---> BDD-cost:   10
c ---[4601]---> BDD-cost:   10
c ---[4600]---> BDD-cost:   10
c ---[4599]---> BDD-cost:   10
c ---[4598]---> BDD-cost:   10
c ---[4597]---> BDD-cost:   10
c ---[4596]---> BDD-cost:   10
c ---[4595]---> BDD-cost:   10
c ---[4594]---> BDD-cost:   10
c ---[4593]---> BDD-cost:   10
c ---[4592]---> BDD-cost:   10
c ---[4591]---> BDD-cost:   10
c ---[4590]---> BDD-cost:   10
c ---[4589]---> BDD-cost:   10
c ---[4588]---> BDD-cost:   10
c ---[4587]---> BDD-cost:   10
c ---[4586]---> BDD-cost:   10
c ---[4585]---> BDD-cost:   10
c ---[4584]---> BDD-cost:   10
c ---[4583]---> BDD-cost:   10
c ---[4582]---> BDD-cost:   10
c ---[4581]---> BDD-cost:   10
c ---[4580]---> BDD-cost:   10
c ---[4579]---> BDD-cost:   10
c ---[4578]---> BDD-cost:   10
c ---[4577]---> BDD-cost:   10
c ---[4576]---> BDD-cost:   10
c ---[4575]---> BDD-cost:   10
c ---[4574]---> BDD-cost:   10
c ---[4573]---> BDD-cost:   10
c ---[4572]---> BDD-cost:   10
c ---[4571]---> BDD-cost:   10
c ---[4570]---> BDD-cost:   10
c ---[4569]---> BDD-cost:   10
c ---[4568]---> BDD-cost:   10
c ---[4567]---> BDD-cost:   10
c ---[4566]---> BDD-cost:   10
c ---[4565]---> BDD-cost:   10
c ---[4564]---> BDD-cost:   10
c ---[4563]---> BDD-cost:   10
c ---[4562]---> BDD-cost:   10
c ---[4561]---> BDD-cost:   10
c ---[4560]---> BDD-cost:   10
c ---[4559]---> BDD-cost:   10
c ---[4558]---> BDD-cost:   10
c ---[4557]---> BDD-cost:   10
c ---[4556]---> BDD-cost:   10
c ---[4555]---> BDD-cost:   10
c ---[4554]---> BDD-cost:   10
c ---[4553]---> BDD-cost:   10
c ---[4552]---> BDD-cost:   10
c ---[4551]---> BDD-cost:   10
c ---[4550]---> BDD-cost:   10
c ---[4549]---> BDD-cost:   10
c ---[4548]---> BDD-cost:   10
c ---[4547]---> BDD-cost:   10
c ---[4546]---> BDD-cost:   10
c ---[4545]---> BDD-cost:   10
c ---[4544]---> BDD-cost:   10
c ---[4543]---> BDD-cost:   10
c ---[4542]---> BDD-cost:   10
c ---[4541]---> BDD-cost:   10
c ---[4540]---> BDD-cost:   10
c ---[4539]---> BDD-cost:   10
c ---[4538]---> BDD-cost:   10
c ---[4537]---> BDD-cost:   10
c ---[4536]---> BDD-cost:   10
c ---[4535]---> BDD-cost:   10
c ---[4534]---> BDD-cost:   10
c ---[4533]---> BDD-cost:   10
c ---[4532]---> BDD-cost:   10
c ---[4531]---> BDD-cost:   10
c ---[4530]---> BDD-cost:   10
c ---[4529]---> BDD-cost:   10
c ---[4528]---> BDD-cost:   10
c ---[4527]---> BDD-cost:   10
c ---[4526]---> BDD-cost:   10
c ---[4525]---> BDD-cost:   10
c ---[4524]---> BDD-cost:   10
c ---[4523]---> BDD-cost:   10
c ---[4522]---> BDD-cost:   10
c ---[4521]---> BDD-cost:   10
c ---[4516]---> BDD-cost:   10
c ---[4515]---> BDD-cost:   10
c ---[4514]---> BDD-cost:   10
c ---[4513]---> BDD-cost:   10
c ---[4512]---> BDD-cost:   10
c ---[4511]---> BDD-cost:   10
c ---[4510]---> BDD-cost:   10
c ---[4509]---> BDD-cost:   10
c ---[4508]---> BDD-cost:   10
c ---[4507]---> BDD-cost:   10
c ---[4506]---> BDD-cost:   10
c ---[4505]---> BDD-cost:   10
c ---[4504]---> BDD-cost:   10
c ---[4503]---> BDD-cost:   10
c ---[4502]---> BDD-cost:   10
c ---[4501]---> BDD-cost:   10
c ---[4500]---> BDD-cost:   10
c ---[4499]---> BDD-cost:   10
c ---[4498]---> BDD-cost:   10
c ---[4497]---> BDD-cost:   10
c ---[4496]---> BDD-cost:   10
c ---[4495]---> BDD-cost:   10
c ---[4494]---> BDD-cost:   10
c ---[4493]---> BDD-cost:   10
c ---[4492]---> BDD-cost:   10
c ---[4491]---> BDD-cost:   10
c ---[4490]---> BDD-cost:   10
c ---[4489]---> BDD-cost:   10
c ---[4488]---> BDD-cost:   10
c ---[4487]---> BDD-cost:   10
c ---[4486]---> BDD-cost:   10
c ---[4485]---> BDD-cost:   10
c ---[4484]---> BDD-cost:   10
c ---[4483]---> BDD-cost:   10
c ---[4482]---> BDD-cost:   10
c ---[4481]---> BDD-cost:   10
c ---[4480]---> BDD-cost:   10
c ---[4479]---> BDD-cost:   10
c ---[4478]---> BDD-cost:   10
c ---[4477]---> BDD-cost:   10
c ---[4476]---> BDD-cost:   10
c ---[4475]---> BDD-cost:   10
c ---[4474]---> BDD-cost:   10
c ---[4473]---> BDD-cost:   10
c ---[4472]---> BDD-cost:   10
c ---[4471]---> BDD-cost:   10
c ---[4470]---> BDD-cost:   10
c ---[4469]---> BDD-cost:   10
c ---[4468]---> BDD-cost:   10
c ---[4467]---> BDD-cost:   10
c ---[4466]---> BDD-cost:   10
c ---[4465]---> BDD-cost:   10
c ---[4464]---> BDD-cost:   10
c ---[4463]---> BDD-cost:   10
c ---[4462]---> BDD-cost:   10
c ---[4461]---> BDD-cost:   10
c ---[4460]---> BDD-cost:   10
c ---[4459]---> BDD-cost:   10
c ---[4458]---> BDD-cost:   10
c ---[4457]---> BDD-cost:   10
c ---[4456]---> BDD-cost:   10
c ---[4455]---> BDD-cost:   10
c ---[4454]---> BDD-cost:   10
c ---[4453]---> BDD-cost:   10
c ---[4452]---> BDD-cost:   10
c ---[4451]---> BDD-cost:   10
c ---[4450]---> BDD-cost:   10
c ---[4449]---> BDD-cost:   10
c ---[4448]---> BDD-cost:   10
c ---[4447]---> BDD-cost:   10
c ---[4446]---> BDD-cost:   10
c ---[4445]---> BDD-cost:   10
c ---[4444]---> BDD-cost:   10
c ---[4443]---> BDD-cost:   10
c ---[4442]---> BDD-cost:   10
c ---[4441]---> BDD-cost:   10
c ---[4440]---> BDD-cost:   10
c ---[4439]---> BDD-cost:   10
c ---[4434]---> BDD-cost:   10
c ---[4433]---> BDD-cost:   10
c ---[4432]---> BDD-cost:   10
c ---[4431]---> BDD-cost:   10
c ---[4430]---> BDD-cost:   10
c ---[4429]---> BDD-cost:   10
c ---[4428]---> BDD-cost:   10
c ---[4427]---> BDD-cost:   10
c ---[4426]---> BDD-cost:   10
c ---[4425]---> BDD-cost:   10
c ---[4424]---> BDD-cost:   10
c ---[4423]---> BDD-cost:   10
c ---[4422]---> BDD-cost:   10
c ---[4421]---> BDD-cost:   10
c ---[4420]---> BDD-cost:   10
c ---[4419]---> BDD-cost:   10
c ---[4418]---> BDD-cost:   10
c ---[4417]---> BDD-cost:   10
c ---[4416]---> BDD-cost:   10
c ---[4415]---> BDD-cost:   10
c ---[4414]---> BDD-cost:   10
c ---[4413]---> BDD-cost:   10
c ---[4412]---> BDD-cost:   10
c ---[4411]---> BDD-cost:   10
c ---[4410]---> BDD-cost:   10
c ---[4409]---> BDD-cost:   10
c ---[4408]---> BDD-cost:   10
c ---[4407]---> BDD-cost:   10
c ---[4406]---> BDD-cost:   10
c ---[4405]---> BDD-cost:   10
c ---[4404]---> BDD-cost:   10
c ---[4403]---> BDD-cost:   10
c ---[4402]---> BDD-cost:   10
c ---[4401]---> BDD-cost:   10
c ---[4400]---> BDD-cost:   10
c ---[4399]---> BDD-cost:   10
c ---[4398]---> BDD-cost:   10
c ---[4397]---> BDD-cost:   10
c ---[4396]---> BDD-cost:   10
c ---[4395]---> BDD-cost:   10
c ---[4394]---> BDD-cost:   10
c ---[4393]---> BDD-cost:   10
c ---[4392]---> BDD-cost:   10
c ---[4391]---> BDD-cost:   10
c ---[4390]---> BDD-cost:   10
c ---[4389]---> BDD-cost:   10
c ---[4388]---> BDD-cost:   10
c ---[4387]---> BDD-cost:   10
c ---[4386]---> BDD-cost:   10
c ---[4385]---> BDD-cost:   10
c ---[4384]---> BDD-cost:   10
c ---[4383]---> BDD-cost:   10
c ---[4382]---> BDD-cost:   10
c ---[4381]---> BDD-cost:   10
c ---[4380]---> BDD-cost:   10
c ---[4379]---> BDD-cost:   10
c ---[4378]---> BDD-cost:   10
c ---[4377]---> BDD-cost:   10
c ---[4376]---> BDD-cost:   10
c ---[4375]---> BDD-cost:   10
c ---[4374]---> BDD-cost:   10
c ---[4373]---> BDD-cost:   10
c ---[4372]---> BDD-cost:   10
c ---[4371]---> BDD-cost:   10
c ---[4370]---> BDD-cost:   10
c ---[4369]---> BDD-cost:   10
c ---[4368]---> BDD-cost:   10
c ---[4367]---> BDD-cost:   10
c ---[4366]---> BDD-cost:   10
c ---[4365]---> BDD-cost:   10
c ---[4364]---> BDD-cost:   10
c ---[4363]---> BDD-cost:   10
c ---[4362]---> BDD-cost:   10
c ---[4361]---> BDD-cost:   10
c ---[4360]---> BDD-cost:   10
c ---[4359]---> BDD-cost:   10
c ---[4358]---> BDD-cost:   10
c ---[4357]---> BDD-cost:   10
c ---[4352]---> BDD-cost:   10
c ---[4351]---> BDD-cost:   10
c ---[4350]---> BDD-cost:   10
c ---[4349]---> BDD-cost:   10
c ---[4348]---> BDD-cost:   10
c ---[4347]---> BDD-cost:   10
c ---[4346]---> BDD-cost:   10
c ---[4345]---> BDD-cost:   10
c ---[4344]---> BDD-cost:   10
c ---[4343]---> BDD-cost:   10
c ---[4342]---> BDD-cost:   10
c ---[4341]---> BDD-cost:   10
c ---[4340]---> BDD-cost:   10
c ---[4339]---> BDD-cost:   10
c ---[4338]---> BDD-cost:   10
c ---[4337]---> BDD-cost:   10
c ---[4336]---> BDD-cost:   10
c ---[4335]---> BDD-cost:   10
c ---[4334]---> BDD-cost:   10
c ---[4333]---> BDD-cost:   10
c ---[4332]---> BDD-cost:   10
c ---[4331]---> BDD-cost:   10
c ---[4330]---> BDD-cost:   10
c ---[4329]---> BDD-cost:   10
c ---[4328]---> BDD-cost:   10
c ---[4327]---> BDD-cost:   10
c ---[4326]---> BDD-cost:   10
c ---[4325]---> BDD-cost:   10
c ---[4324]---> BDD-cost:   10
c ---[4323]---> BDD-cost:   10
c ---[4322]---> BDD-cost:   10
c ---[4321]---> BDD-cost:   10
c ---[4320]---> BDD-cost:   10
c ---[4319]---> BDD-cost:   10
c ---[4318]---> BDD-cost:   10
c ---[4317]---> BDD-cost:   10
c ---[4316]---> BDD-cost:   10
c ---[4315]---> BDD-cost:   10
c ---[4314]---> BDD-cost:   10
c ---[4313]---> BDD-cost:   10
c ---[4312]---> BDD-cost:   10
c ---[4311]---> BDD-cost:   10
c ---[4310]---> BDD-cost:   10
c ---[4309]---> BDD-cost:   10
c ---[4308]---> BDD-cost:   10
c ---[4307]---> BDD-cost:   10
c ---[4306]---> BDD-cost:   10
c ---[4305]---> BDD-cost:   10
c ---[4304]---> BDD-cost:   10
c ---[4303]---> BDD-cost:   10
c ---[4302]---> BDD-cost:   10
c ---[4301]---> BDD-cost:   10
c ---[4300]---> BDD-cost:   10
c ---[4299]---> BDD-cost:   10
c ---[4298]---> BDD-cost:   10
c ---[4297]---> BDD-cost:   10
c ---[4296]---> BDD-cost:   10
c ---[4295]---> BDD-cost:   10
c ---[4294]---> BDD-cost:   10
c ---[4293]---> BDD-cost:   10
c ---[4292]---> BDD-cost:   10
c ---[4291]---> BDD-cost:   10
c ---[4290]---> BDD-cost:   10
c ---[4289]---> BDD-cost:   10
c ---[4288]---> BDD-cost:   10
c ---[4287]---> BDD-cost:   10
c ---[4286]---> BDD-cost:   10
c ---[4285]---> BDD-cost:   10
c ---[4284]---> BDD-cost:   10
c ---[4283]---> BDD-cost:   10
c ---[4282]---> BDD-cost:   10
c ---[4281]---> BDD-cost:   10
c ---[4280]---> BDD-cost:   10
c ---[4279]---> BDD-cost:   10
c ---[4278]---> BDD-cost:   10
c ---[4277]---> BDD-cost:   10
c ---[4276]---> BDD-cost:   10
c ---[4275]---> BDD-cost:   10
c ---[4270]---> BDD-cost:   10
c ---[4269]---> BDD-cost:   10
c ---[4268]---> BDD-cost:   10
c ---[4267]---> BDD-cost:   10
c ---[4266]---> BDD-cost:   10
c ---[4265]---> BDD-cost:   10
c ---[4264]---> BDD-cost:   10
c ---[4263]---> BDD-cost:   10
c ---[4262]---> BDD-cost:   10
c ---[4261]---> BDD-cost:   10
c ---[4260]---> BDD-cost:   10
c ---[4259]---> BDD-cost:   10
c ---[4258]---> BDD-cost:   10
c ---[4257]---> BDD-cost:   10
c ---[4256]---> BDD-cost:   10
c ---[4255]---> BDD-cost:   10
c ---[4254]---> BDD-cost:   10
c ---[4253]---> BDD-cost:   10
c ---[4252]---> BDD-cost:   10
c ---[4251]---> BDD-cost:   10
c ---[4250]---> BDD-cost:   10
c ---[4249]---> BDD-cost:   10
c ---[4248]---> BDD-cost:   10
c ---[4247]---> BDD-cost:   10
c ---[4246]---> BDD-cost:   10
c ---[4245]---> BDD-cost:   10
c ---[4244]---> BDD-cost:   10
c ---[4243]---> BDD-cost:   10
c ---[4242]---> BDD-cost:   10
c ---[4241]---> BDD-cost:   10
c ---[4240]---> BDD-cost:   10
c ---[4239]---> BDD-cost:   10
c ---[4238]---> BDD-cost:   10
c ---[4237]---> BDD-cost:   10
c ---[4236]---> BDD-cost:   10
c ---[4235]---> BDD-cost:   10
c ---[4234]---> BDD-cost:   10
c ---[4233]---> BDD-cost:   10
c ---[4232]---> BDD-cost:   10
c ---[4231]---> BDD-cost:   10
c ---[4230]---> BDD-cost:   10
c ---[4229]---> BDD-cost:   10
c ---[4228]---> BDD-cost:   10
c ---[4227]---> BDD-cost:   10
c ---[4226]---> BDD-cost:   10
c ---[4225]---> BDD-cost:   10
c ---[4224]---> BDD-cost:   10
c ---[4223]---> BDD-cost:   10
c ---[4222]---> BDD-cost:   10
c ---[4221]---> BDD-cost:   10
c ---[4220]---> BDD-cost:   10
c ---[4219]---> BDD-cost:   10
c ---[4218]---> BDD-cost:   10
c ---[4217]---> BDD-cost:   10
c ---[4216]---> BDD-cost:   10
c ---[4215]---> BDD-cost:   10
c ---[4214]---> BDD-cost:   10
c ---[4213]---> BDD-cost:   10
c ---[4212]---> BDD-cost:   10
c ---[4211]---> BDD-cost:   10
c ---[4210]---> BDD-cost:   10
c ---[4209]---> BDD-cost:   10
c ---[4208]---> BDD-cost:   10
c ---[4207]---> BDD-cost:   10
c ---[4206]---> BDD-cost:   10
c ---[4205]---> BDD-cost:   10
c ---[4204]---> BDD-cost:   10
c ---[4203]---> BDD-cost:   10
c ---[4202]---> BDD-cost:   10
c ---[4201]---> BDD-cost:   10
c ---[4200]---> BDD-cost:   10
c ---[4199]---> BDD-cost:   10
c ---[4198]---> BDD-cost:   10
c ---[4197]---> BDD-cost:   10
c ---[4196]---> BDD-cost:   10
c ---[4195]---> BDD-cost:   10
c ---[4194]---> BDD-cost:   10
c ---[4193]---> BDD-cost:   10
c ---[4192]---> BDD-cost:   10
c ---[4191]---> BDD-cost:   10
c ---[4190]---> BDD-cost:   10
c ---[4189]---> BDD-cost:   10
c ---[4184]---> BDD-cost:   10
c ---[4183]---> BDD-cost:   10
c ---[4182]---> BDD-cost:   10
c ---[4181]---> BDD-cost:   10
c ---[4180]---> BDD-cost:   10
c ---[4179]---> BDD-cost:   10
c ---[4178]---> BDD-cost:   10
c ---[4177]---> BDD-cost:   10
c ---[4176]---> BDD-cost:   10
c ---[4175]---> BDD-cost:   10
c ---[4174]---> BDD-cost:   10
c ---[4173]---> BDD-cost:   10
c ---[4172]---> BDD-cost:   10
c ---[4171]---> BDD-cost:   10
c ---[4170]---> BDD-cost:   10
c ---[4169]---> BDD-cost:   10
c ---[4168]---> BDD-cost:   10
c ---[4167]---> BDD-cost:   10
c ---[4166]---> BDD-cost:   10
c ---[4165]---> BDD-cost:   10
c ---[4164]---> BDD-cost:   10
c ---[4163]---> BDD-cost:   10
c ---[4162]---> BDD-cost:   10
c ---[4161]---> BDD-cost:   10
c ---[4160]---> BDD-cost:   10
c ---[4159]---> BDD-cost:   10
c ---[4158]---> BDD-cost:   10
c ---[4157]---> BDD-cost:   10
c ---[4156]---> BDD-cost:   10
c ---[4155]---> BDD-cost:   10
c ---[4154]---> BDD-cost:   10
c ---[4153]---> BDD-cost:   10
c ---[4152]---> BDD-cost:   10
c ---[4151]---> BDD-cost:   10
c ---[4150]---> BDD-cost:   10
c ---[4149]---> BDD-cost:   10
c ---[4148]---> BDD-cost:   10
c ---[4147]---> BDD-cost:   10
c ---[4146]---> BDD-cost:   10
c ---[4145]---> BDD-cost:   10
c ---[4144]---> BDD-cost:   10
c ---[4143]---> BDD-cost:   10
c ---[4142]---> BDD-cost:   10
c ---[4141]---> BDD-cost:   10
c ---[4140]---> BDD-cost:   10
c ---[4139]---> BDD-cost:   10
c ---[4138]---> BDD-cost:   10
c ---[4137]---> BDD-cost:   10
c ---[4136]---> BDD-cost:   10
c ---[4135]---> BDD-cost:   10
c ---[4134]---> BDD-cost:   10
c ---[4133]---> BDD-cost:   10
c ---[4132]---> BDD-cost:   10
c ---[4131]---> BDD-cost:   10
c ---[4130]---> BDD-cost:   10
c ---[4129]---> BDD-cost:   10
c ---[4128]---> BDD-cost:   10
c ---[4127]---> BDD-cost:   10
c ---[4126]---> BDD-cost:   10
c ---[4125]---> BDD-cost:   10
c ---[4124]---> BDD-cost:   10
c ---[4123]---> BDD-cost:   10
c ---[4122]---> BDD-cost:   10
c ---[4121]---> BDD-cost:   10
c ---[4120]---> BDD-cost:   10
c ---[4119]---> BDD-cost:   10
c ---[4118]---> BDD-cost:   10
c ---[4117]---> BDD-cost:   10
c ---[4116]---> BDD-cost:   10
c ---[4115]---> BDD-cost:   10
c ---[4114]---> BDD-cost:   10
c ---[4113]---> BDD-cost:   10
c ---[4112]---> BDD-cost:   10
c ---[4111]---> BDD-cost:   10
c ---[4110]---> BDD-cost:   10
c ---[4109]---> BDD-cost:   10
c ---[4108]---> BDD-cost:   10
c ---[4107]---> BDD-cost:   10
c ---[4102]---> BDD-cost:   10
c ---[4101]---> BDD-cost:   10
c ---[4100]---> BDD-cost:   10
c ---[4099]---> BDD-cost:   10
c ---[4098]---> BDD-cost:   10
c ---[4097]---> BDD-cost:   10
c ---[4096]---> BDD-cost:   10
c ---[4095]---> BDD-cost:   10
c ---[4094]---> BDD-cost:   10
c ---[4093]---> BDD-cost:   10
c ---[4092]---> BDD-cost:   10
c ---[4091]---> BDD-cost:   10
c ---[4090]---> BDD-cost:   10
c ---[4089]---> BDD-cost:   10
c ---[4088]---> BDD-cost:   10
c ---[4087]---> BDD-cost:   10
c ---[4086]---> BDD-cost:   10
c ---[4085]---> BDD-cost:   10
c ---[4084]---> BDD-cost:   10
c ---[4083]---> BDD-cost:   10
c ---[4082]---> BDD-cost:   10
c ---[4081]---> BDD-cost:   10
c ---[4080]---> BDD-cost:   10
c ---[4079]---> BDD-cost:   10
c ---[4078]---> BDD-cost:   10
c ---[4077]---> BDD-cost:   10
c ---[4076]---> BDD-cost:   10
c ---[4075]---> BDD-cost:   10
c ---[4074]---> BDD-cost:   10
c ---[4073]---> BDD-cost:   10
c ---[4072]---> BDD-cost:   10
c ---[4071]---> BDD-cost:   10
c ---[4070]---> BDD-cost:   10
c ---[4069]---> BDD-cost:   10
c ---[4068]---> BDD-cost:   10
c ---[4067]---> BDD-cost:   10
c ---[4066]---> BDD-cost:   10
c ---[4065]---> BDD-cost:   10
c ---[4064]---> BDD-cost:   10
c ---[4063]---> BDD-cost:   10
c ---[4062]---> BDD-cost:   10
c ---[4061]---> BDD-cost:   10
c ---[4060]---> BDD-cost:   10
c ---[4059]---> BDD-cost:   10
c ---[4058]---> BDD-cost:   10
c ---[4057]---> BDD-cost:   10
c ---[4056]---> BDD-cost:   10
c ---[4055]---> BDD-cost:   10
c ---[4054]---> BDD-cost:   10
c ---[4053]---> BDD-cost:   10
c ---[4052]---> BDD-cost:   10
c ---[4051]---> BDD-cost:   10
c ---[4050]---> BDD-cost:   10
c ---[4049]---> BDD-cost:   10
c ---[4048]---> BDD-cost:   10
c ---[4047]---> BDD-cost:   10
c ---[4046]---> BDD-cost:   10
c ---[4045]---> BDD-cost:   10
c ---[4044]---> BDD-cost:   10
c ---[4043]---> BDD-cost:   10
c ---[4042]---> BDD-cost:   10
c ---[4041]---> BDD-cost:   10
c ---[4040]---> BDD-cost:   10
c ---[4039]---> BDD-cost:   10
c ---[4038]---> BDD-cost:   10
c ---[4037]---> BDD-cost:   10
c ---[4036]---> BDD-cost:   10
c ---[4035]---> BDD-cost:   10
c ---[4034]---> BDD-cost:   10
c ---[4033]---> BDD-cost:   10
c ---[4032]---> BDD-cost:   10
c ---[4031]---> BDD-cost:   10
c ---[4030]---> BDD-cost:   10
c ---[4029]---> BDD-cost:   10
c ---[4028]---> BDD-cost:   10
c ---[4027]---> BDD-cost:   10
c ---[4026]---> BDD-cost:   10
c ---[4025]---> BDD-cost:   10
c ---[4020]---> BDD-cost:   10
c ---[4019]---> BDD-cost:   10
c ---[4018]---> BDD-cost:   10
c ---[4017]---> BDD-cost:   10
c ---[4016]---> BDD-cost:   10
c ---[4015]---> BDD-cost:   10
c ---[4014]---> BDD-cost:   10
c ---[4013]---> BDD-cost:   10
c ---[4012]---> BDD-cost:   10
c ---[4011]---> BDD-cost:   10
c ---[4010]---> BDD-cost:   10
c ---[4009]---> BDD-cost:   10
c ---[4008]---> BDD-cost:   10
c ---[4007]---> BDD-cost:   10
c ---[4006]---> BDD-cost:   10
c ---[4005]---> BDD-cost:   10
c ---[4004]---> BDD-cost:   10
c ---[4003]---> BDD-cost:   10
c ---[4002]---> BDD-cost:   10
c ---[4001]---> BDD-cost:   10
c ---[4000]---> BDD-cost:   10
c ---[3999]---> BDD-cost:   10
c ---[3998]---> BDD-cost:   10
c ---[3997]---> BDD-cost:   10
c ---[3996]---> BDD-cost:   10
c ---[3995]---> BDD-cost:   10
c ---[3994]---> BDD-cost:   10
c ---[3993]---> BDD-cost:   10
c ---[3992]---> BDD-cost:   10
c ---[3991]---> BDD-cost:   10
c ---[3990]---> BDD-cost:   10
c ---[3989]---> BDD-cost:   10
c ---[3988]---> BDD-cost:   10
c ---[3987]---> BDD-cost:   10
c ---[3986]---> BDD-cost:   10
c ---[3985]---> BDD-cost:   10
c ---[3984]---> BDD-cost:   10
c ---[3983]---> BDD-cost:   10
c ---[3982]---> BDD-cost:   10
c ---[3981]---> BDD-cost:   10
c ---[3980]---> BDD-cost:   10
c ---[3979]---> BDD-cost:   10
c ---[3978]---> BDD-cost:   10
c ---[3977]---> BDD-cost:   10
c ---[3976]---> BDD-cost:   10
c ---[3975]---> BDD-cost:   10
c ---[3974]---> BDD-cost:   10
c ---[3973]---> BDD-cost:   10
c ---[3972]---> BDD-cost:   10
c ---[3971]---> BDD-cost:   10
c ---[3970]---> BDD-cost:   10
c ---[3969]---> BDD-cost:   10
c ---[3968]---> BDD-cost:   10
c ---[3967]---> BDD-cost:   10
c ---[3966]---> BDD-cost:   10
c ---[3965]---> BDD-cost:   10
c ---[3964]---> BDD-cost:   10
c ---[3963]---> BDD-cost:   10
c ---[3962]---> BDD-cost:   10
c ---[3961]---> BDD-cost:   10
c ---[3960]---> BDD-cost:   10
c ---[3959]---> BDD-cost:   10
c ---[3958]---> BDD-cost:   10
c ---[3957]---> BDD-cost:   10
c ---[3956]---> BDD-cost:   10
c ---[3955]---> BDD-cost:   10
c ---[3954]---> BDD-cost:   10
c ---[3953]---> BDD-cost:   10
c ---[3952]---> BDD-cost:   10
c ---[3951]---> BDD-cost:   10
c ---[3950]---> BDD-cost:   10
c ---[3949]---> BDD-cost:   10
c ---[3948]---> BDD-cost:   10
c ---[3947]---> BDD-cost:   10
c ---[3946]---> BDD-cost:   10
c ---[3945]---> BDD-cost:   10
c ---[3944]---> BDD-cost:   10
c ---[3943]---> BDD-cost:   10
c ---[3938]---> BDD-cost:   10
c ---[3937]---> BDD-cost:   10
c ---[3936]---> BDD-cost:   10
c ---[3935]---> BDD-cost:   10
c ---[3934]---> BDD-cost:   10
c ---[3933]---> BDD-cost:   10
c ---[3932]---> BDD-cost:   10
c ---[3931]---> BDD-cost:   10
c ---[3930]---> BDD-cost:   10
c ---[3929]---> BDD-cost:   10
c ---[3928]---> BDD-cost:   10
c ---[3927]---> BDD-cost:   10
c ---[3926]---> BDD-cost:   10
c ---[3925]---> BDD-cost:   10
c ---[3924]---> BDD-cost:   10
c ---[3923]---> BDD-cost:   10
c ---[3922]---> BDD-cost:   10
c ---[3921]---> BDD-cost:   10
c ---[3920]---> BDD-cost:   10
c ---[3919]---> BDD-cost:   10
c ---[3918]---> BDD-cost:   10
c ---[3917]---> BDD-cost:   10
c ---[3916]---> BDD-cost:   10
c ---[3915]---> BDD-cost:   10
c ---[3914]---> BDD-cost:   10
c ---[3913]---> BDD-cost:   10
c ---[3912]---> BDD-cost:   10
c ---[3911]---> BDD-cost:   10
c ---[3910]---> BDD-cost:   10
c ---[3909]---> BDD-cost:   10
c ---[3908]---> BDD-cost:   10
c ---[3907]---> BDD-cost:   10
c ---[3906]---> BDD-cost:   10
c ---[3905]---> BDD-cost:   10
c ---[3904]---> BDD-cost:   10
c ---[3903]---> BDD-cost:   10
c ---[3902]---> BDD-cost:   10
c ---[3901]---> BDD-cost:   10
c ---[3900]---> BDD-cost:   10
c ---[3899]---> BDD-cost:   10
c ---[3898]---> BDD-cost:   10
c ---[3897]---> BDD-cost:   10
c ---[3896]---> BDD-cost:   10
c ---[3895]---> BDD-cost:   10
c ---[3894]---> BDD-cost:   10
c ---[3893]---> BDD-cost:   10
c ---[3892]---> BDD-cost:   10
c ---[3891]---> BDD-cost:   10
c ---[3890]---> BDD-cost:   10
c ---[3889]---> BDD-cost:   10
c ---[3888]---> BDD-cost:   10
c ---[3887]---> BDD-cost:   10
c ---[3886]---> BDD-cost:   10
c ---[3885]---> BDD-cost:   10
c ---[3884]---> BDD-cost:   10
c ---[3883]---> BDD-cost:   10
c ---[3882]---> BDD-cost:   10
c ---[3881]---> BDD-cost:   10
c ---[3880]---> BDD-cost:   10
c ---[3879]---> BDD-cost:   10
c ---[3878]---> BDD-cost:   10
c ---[3877]---> BDD-cost:   10
c ---[3876]---> BDD-cost:   10
c ---[3875]---> BDD-cost:   10
c ---[3874]---> BDD-cost:   10
c ---[3873]---> BDD-cost:   10
c ---[3872]---> BDD-cost:   10
c ---[3871]---> BDD-cost:   10
c ---[3870]---> BDD-cost:   10
c ---[3869]---> BDD-cost:   10
c ---[3868]---> BDD-cost:   10
c ---[3867]---> BDD-cost:   10
c ---[3866]---> BDD-cost:   10
c ---[3865]---> BDD-cost:   10
c ---[3864]---> BDD-cost:   10
c ---[3863]---> BDD-cost:   10
c ---[3862]---> BDD-cost:   10
c ---[3861]---> BDD-cost:   10
c ---[3860]---> BDD-cost:   10
c ---[3859]---> BDD-cost:   10
c ---[3858]---> BDD-cost:   10
c ---[3857]---> BDD-cost:   10
c ---[3852]---> BDD-cost:   10
c ---[3851]---> BDD-cost:   10
c ---[3850]---> BDD-cost:   10
c ---[3849]---> BDD-cost:   10
c ---[3848]---> BDD-cost:   10
c ---[3847]---> BDD-cost:   10
c ---[3846]---> BDD-cost:   10
c ---[3845]---> BDD-cost:   10
c ---[3844]---> BDD-cost:   10
c ---[3843]---> BDD-cost:   10
c ---[3842]---> BDD-cost:   10
c ---[3841]---> BDD-cost:   10
c ---[3840]---> BDD-cost:   10
c ---[3839]---> BDD-cost:   10
c ---[3838]---> BDD-cost:   10
c ---[3837]---> BDD-cost:   10
c ---[3836]---> BDD-cost:   10
c ---[3835]---> BDD-cost:   10
c ---[3834]---> BDD-cost:   10
c ---[3833]---> BDD-cost:   10
c ---[3832]---> BDD-cost:   10
c ---[3831]---> BDD-cost:   10
c ---[3830]---> BDD-cost:   10
c ---[3829]---> BDD-cost:   10
c ---[3828]---> BDD-cost:   10
c ---[3827]---> BDD-cost:   10
c ---[3826]---> BDD-cost:   10
c ---[3825]---> BDD-cost:   10
c ---[3824]---> BDD-cost:   10
c ---[3823]---> BDD-cost:   10
c ---[3822]---> BDD-cost:   10
c ---[3821]---> BDD-cost:   10
c ---[3820]---> BDD-cost:   10
c ---[3819]---> BDD-cost:   10
c ---[3818]---> BDD-cost:   10
c ---[3817]---> BDD-cost:   10
c ---[3816]---> BDD-cost:   10
c ---[3815]---> BDD-cost:   10
c ---[3814]---> BDD-cost:   10
c ---[3813]---> BDD-cost:   10
c ---[3812]---> BDD-cost:   10
c ---[3811]---> BDD-cost:   10
c ---[3810]---> BDD-cost:   10
c ---[3809]---> BDD-cost:   10
c ---[3808]---> BDD-cost:   10
c ---[3807]---> BDD-cost:   10
c ---[3806]---> BDD-cost:   10
c ---[3805]---> BDD-cost:   10
c ---[3804]---> BDD-cost:   10
c ---[3803]---> BDD-cost:   10
c ---[3802]---> BDD-cost:   10
c ---[3801]---> BDD-cost:   10
c ---[3800]---> BDD-cost:   10
c ---[3799]---> BDD-cost:   10
c ---[3798]---> BDD-cost:   10
c ---[3797]---> BDD-cost:   10
c ---[3796]---> BDD-cost:   10
c ---[3795]---> BDD-cost:   10
c ---[3794]---> BDD-cost:   10
c ---[3793]---> BDD-cost:   10
c ---[3792]---> BDD-cost:   10
c ---[3791]---> BDD-cost:   10
c ---[3790]---> BDD-cost:   10
c ---[3789]---> BDD-cost:   10
c ---[3788]---> BDD-cost:   10
c ---[3787]---> BDD-cost:   10
c ---[3786]---> BDD-cost:   10
c ---[3785]---> BDD-cost:   10
c ---[3784]---> BDD-cost:   10
c ---[3783]---> BDD-cost:   10
c ---[3782]---> BDD-cost:   10
c ---[3781]---> BDD-cost:   10
c ---[3780]---> BDD-cost:   10
c ---[3779]---> BDD-cost:   10
c ---[3778]---> BDD-cost:   10
c ---[3777]---> BDD-cost:   10
c ---[3776]---> BDD-cost:   10
c ---[3775]---> BDD-cost:   10
c ---[3770]---> BDD-cost:   10
c ---[3769]---> BDD-cost:   10
c ---[3768]---> BDD-cost:   10
c ---[3767]---> BDD-cost:   10
c ---[3766]---> BDD-cost:   10
c ---[3765]---> BDD-cost:   10
c ---[3764]---> BDD-cost:   10
c ---[3763]---> BDD-cost:   10
c ---[3762]---> BDD-cost:   10
c ---[3761]---> BDD-cost:   10
c ---[3760]---> BDD-cost:   10
c ---[3759]---> BDD-cost:   10
c ---[3758]---> BDD-cost:   10
c ---[3757]---> BDD-cost:   10
c ---[3756]---> BDD-cost:   10
c ---[3755]---> BDD-cost:   10
c ---[3754]---> BDD-cost:   10
c ---[3753]---> BDD-cost:   10
c ---[3752]---> BDD-cost:   10
c ---[3751]---> BDD-cost:   10
c ---[3750]---> BDD-cost:   10
c ---[3749]---> BDD-cost:   10
c ---[3748]---> BDD-cost:   10
c ---[3747]---> BDD-cost:   10
c ---[3746]---> BDD-cost:   10
c ---[3745]---> BDD-cost:   10
c ---[3744]---> BDD-cost:   10
c ---[3743]---> BDD-cost:   10
c ---[3742]---> BDD-cost:   10
c ---[3741]---> BDD-cost:   10
c ---[3740]---> BDD-cost:   10
c ---[3739]---> BDD-cost:   10
c ---[3738]---> BDD-cost:   10
c ---[3737]---> BDD-cost:   10
c ---[3736]---> BDD-cost:   10
c ---[3735]---> BDD-cost:   10
c ---[3734]---> BDD-cost:   10
c ---[3733]---> BDD-cost:   10
c ---[3732]---> BDD-cost:   10
c ---[3731]---> BDD-cost:   10
c ---[3730]---> BDD-cost:   10
c ---[3729]---> BDD-cost:   10
c ---[3728]---> BDD-cost:   10
c ---[3727]---> BDD-cost:   10
c ---[3726]---> BDD-cost:   10
c ---[3725]---> BDD-cost:   10
c ---[3724]---> BDD-cost:   10
c ---[3723]---> BDD-cost:   10
c ---[3722]---> BDD-cost:   10
c ---[3721]---> BDD-cost:   10
c ---[3720]---> BDD-cost:   10
c ---[3719]---> BDD-cost:   10
c ---[3718]---> BDD-cost:   10
c ---[3717]---> BDD-cost:   10
c ---[3716]---> BDD-cost:   10
c ---[3715]---> BDD-cost:   10
c ---[3714]---> BDD-cost:   10
c ---[3713]---> BDD-cost:   10
c ---[3712]---> BDD-cost:   10
c ---[3711]---> BDD-cost:   10
c ---[3710]---> BDD-cost:   10
c ---[3709]---> BDD-cost:   10
c ---[3708]---> BDD-cost:   10
c ---[3707]---> BDD-cost:   10
c ---[3706]---> BDD-cost:   10
c ---[3705]---> BDD-cost:   10
c ---[3704]---> BDD-cost:   10
c ---[3703]---> BDD-cost:   10
c ---[3702]---> BDD-cost:   10
c ---[3701]---> BDD-cost:   10
c ---[3700]---> BDD-cost:   10
c ---[3699]---> BDD-cost:   10
c ---[3698]---> BDD-cost:   10
c ---[3697]---> BDD-cost:   10
c ---[3696]---> BDD-cost:   10
c ---[3695]---> BDD-cost:   10
c ---[3694]---> BDD-cost:   10
c ---[3693]---> BDD-cost:   10
c ---[3688]---> BDD-cost:   10
c ---[3687]---> BDD-cost:   10
c ---[3686]---> BDD-cost:   10
c ---[3685]---> BDD-cost:   10
c ---[3684]---> BDD-cost:   10
c ---[3683]---> BDD-cost:   10
c ---[3682]---> BDD-cost:   10
c ---[3681]---> BDD-cost:   10
c ---[3680]---> BDD-cost:   10
c ---[3679]---> BDD-cost:   10
c ---[3678]---> BDD-cost:   10
c ---[3677]---> BDD-cost:   10
c ---[3676]---> BDD-cost:   10
c ---[3675]---> BDD-cost:   10
c ---[3674]---> BDD-cost:   10
c ---[3673]---> BDD-cost:   10
c ---[3672]---> BDD-cost:   10
c ---[3671]---> BDD-cost:   10
c ---[3670]---> BDD-cost:   10
c ---[3669]---> BDD-cost:   10
c ---[3668]---> BDD-cost:   10
c ---[3667]---> BDD-cost:   10
c ---[3666]---> BDD-cost:   10
c ---[3665]---> BDD-cost:   10
c ---[3664]---> BDD-cost:   10
c ---[3663]---> BDD-cost:   10
c ---[3662]---> BDD-cost:   10
c ---[3661]---> BDD-cost:   10
c ---[3660]---> BDD-cost:   10
c ---[3659]---> BDD-cost:   10
c ---[3658]---> BDD-cost:   10
c ---[3657]---> BDD-cost:   10
c ---[3656]---> BDD-cost:   10
c ---[3655]---> BDD-cost:   10
c ---[3654]---> BDD-cost:   10
c ---[3653]---> BDD-cost:   10
c ---[3652]---> BDD-cost:   10
c ---[3651]---> BDD-cost:   10
c ---[3650]---> BDD-cost:   10
c ---[3649]---> BDD-cost:   10
c ---[3648]---> BDD-cost:   10
c ---[3647]---> BDD-cost:   10
c ---[3646]---> BDD-cost:   10
c ---[3645]---> BDD-cost:   10
c ---[3644]---> BDD-cost:   10
c ---[3643]---> BDD-cost:   10
c ---[3642]---> BDD-cost:   10
c ---[3641]---> BDD-cost:   10
c ---[3640]---> BDD-cost:   10
c ---[3639]---> BDD-cost:   10
c ---[3638]---> BDD-cost:   10
c ---[3637]---> BDD-cost:   10
c ---[3636]---> BDD-cost:   10
c ---[3635]---> BDD-cost:   10
c ---[3634]---> BDD-cost:   10
c ---[3633]---> BDD-cost:   10
c ---[3632]---> BDD-cost:   10
c ---[3631]---> BDD-cost:   10
c ---[3630]---> BDD-cost:   10
c ---[3629]---> BDD-cost:   10
c ---[3628]---> BDD-cost:   10
c ---[3627]---> BDD-cost:   10
c ---[3626]---> BDD-cost:   10
c ---[3625]---> BDD-cost:   10
c ---[3624]---> BDD-cost:   10
c ---[3623]---> BDD-cost:   10
c ---[3622]---> BDD-cost:   10
c ---[3621]---> BDD-cost:   10
c ---[3620]---> BDD-cost:   10
c ---[3619]---> BDD-cost:   10
c ---[3618]---> BDD-cost:   10
c ---[3617]---> BDD-cost:   10
c ---[3616]---> BDD-cost:   10
c ---[3615]---> BDD-cost:   10
c ---[3614]---> BDD-cost:   10
c ---[3613]---> BDD-cost:   10
c ---[3612]---> BDD-cost:   10
c ---[3611]---> BDD-cost:   10
c ---[3606]---> BDD-cost:   10
c ---[3605]---> BDD-cost:   10
c ---[3604]---> BDD-cost:   10
c ---[3603]---> BDD-cost:   10
c ---[3602]---> BDD-cost:   10
c ---[3601]---> BDD-cost:   10
c ---[3600]---> BDD-cost:   10
c ---[3599]---> BDD-cost:   10
c ---[3598]---> BDD-cost:   10
c ---[3597]---> BDD-cost:   10
c ---[3596]---> BDD-cost:   10
c ---[3595]---> BDD-cost:   10
c ---[3594]---> BDD-cost:   10
c ---[3593]---> BDD-cost:   10
c ---[3592]---> BDD-cost:   10
c ---[3591]---> BDD-cost:   10
c ---[3590]---> BDD-cost:   10
c ---[3589]---> BDD-cost:   10
c ---[3588]---> BDD-cost:   10
c ---[3587]---> BDD-cost:   10
c ---[3586]---> BDD-cost:   10
c ---[3585]---> BDD-cost:   10
c ---[3584]---> BDD-cost:   10
c ---[3583]---> BDD-cost:   10
c ---[3582]---> BDD-cost:   10
c ---[3581]---> BDD-cost:   10
c ---[3580]---> BDD-cost:   10
c ---[3579]---> BDD-cost:   10
c ---[3578]---> BDD-cost:   10
c ---[3577]---> BDD-cost:   10
c ---[3576]---> BDD-cost:   10
c ---[3575]---> BDD-cost:   10
c ---[3574]---> BDD-cost:   10
c ---[3573]---> BDD-cost:   10
c ---[3572]---> BDD-cost:   10
c ---[3571]---> BDD-cost:   10
c ---[3570]---> BDD-cost:   10
c ---[3569]---> BDD-cost:   10
c ---[3568]---> BDD-cost:   10
c ---[3567]---> BDD-cost:   10
c ---[3566]---> BDD-cost:   10
c ---[3565]---> BDD-cost:   10
c ---[3564]---> BDD-cost:   10
c ---[3563]---> BDD-cost:   10
c ---[3562]---> BDD-cost:   10
c ---[3561]---> BDD-cost:   10
c ---[3560]---> BDD-cost:   10
c ---[3559]---> BDD-cost:   10
c ---[3558]---> BDD-cost:   10
c ---[3557]---> BDD-cost:   10
c ---[3556]---> BDD-cost:   10
c ---[3555]---> BDD-cost:   10
c ---[3554]---> BDD-cost:   10
c ---[3553]---> BDD-cost:   10
c ---[3552]---> BDD-cost:   10
c ---[3551]---> BDD-cost:   10
c ---[3550]---> BDD-cost:   10
c ---[3549]---> BDD-cost:   10
c ---[3548]---> BDD-cost:   10
c ---[3547]---> BDD-cost:   10
c ---[3546]---> BDD-cost:   10
c ---[3545]---> BDD-cost:   10
c ---[3544]---> BDD-cost:   10
c ---[3543]---> BDD-cost:   10
c ---[3542]---> BDD-cost:   10
c ---[3541]---> BDD-cost:   10
c ---[3540]---> BDD-cost:   10
c ---[3539]---> BDD-cost:   10
c ---[3538]---> BDD-cost:   10
c ---[3537]---> BDD-cost:   10
c ---[3536]---> BDD-cost:   10
c ---[3535]---> BDD-cost:   10
c ---[3534]---> BDD-cost:   10
c ---[3533]---> BDD-cost:   10
c ---[3532]---> BDD-cost:   10
c ---[3531]---> BDD-cost:   10
c ---[3530]---> BDD-cost:   10
c ---[3529]---> BDD-cost:   10
c ---[3528]---> BDD-cost:   10
c ---[3527]---> BDD-cost:   10
c ---[3526]---> BDD-cost:   10
c ---[3525]---> BDD-cost:   10
c ---[3520]---> BDD-cost:   10
c ---[3519]---> BDD-cost:   10
c ---[3518]---> BDD-cost:   10
c ---[3517]---> BDD-cost:   10
c ---[3516]---> BDD-cost:   10
c ---[3515]---> BDD-cost:   10
c ---[3514]---> BDD-cost:   10
c ---[3513]---> BDD-cost:   10
c ---[3512]---> BDD-cost:   10
c ---[3511]---> BDD-cost:   10
c ---[3510]---> BDD-cost:   10
c ---[3509]---> BDD-cost:   10
c ---[3508]---> BDD-cost:   10
c ---[3507]---> BDD-cost:   10
c ---[3506]---> BDD-cost:   10
c ---[3505]---> BDD-cost:   10
c ---[3504]---> BDD-cost:   10
c ---[3503]---> BDD-cost:   10
c ---[3502]---> BDD-cost:   10
c ---[3501]---> BDD-cost:   10
c ---[3500]---> BDD-cost:   10
c ---[3499]---> BDD-cost:   10
c ---[3498]---> BDD-cost:   10
c ---[3497]---> BDD-cost:   10
c ---[3496]---> BDD-cost:   10
c ---[3495]---> BDD-cost:   10
c ---[3494]---> BDD-cost:   10
c ---[3493]---> BDD-cost:   10
c ---[3492]---> BDD-cost:   10
c ---[3491]---> BDD-cost:   10
c ---[3490]---> BDD-cost:   10
c ---[3489]---> BDD-cost:   10
c ---[3488]---> BDD-cost:   10
c ---[3487]---> BDD-cost:   10
c ---[3486]---> BDD-cost:   10
c ---[3485]---> BDD-cost:   10
c ---[3484]---> BDD-cost:   10
c ---[3483]---> BDD-cost:   10
c ---[3482]---> BDD-cost:   10
c ---[3481]---> BDD-cost:   10
c ---[3480]---> BDD-cost:   10
c ---[3479]---> BDD-cost:   10
c ---[3478]---> BDD-cost:   10
c ---[3477]---> BDD-cost:   10
c ---[3476]---> BDD-cost:   10
c ---[3475]---> BDD-cost:   10
c ---[3474]---> BDD-cost:   10
c ---[3473]---> BDD-cost:   10
c ---[3472]---> BDD-cost:   10
c ---[3471]---> BDD-cost:   10
c ---[3470]---> BDD-cost:   10
c ---[3469]---> BDD-cost:   10
c ---[3468]---> BDD-cost:   10
c ---[3467]---> BDD-cost:   10
c ---[3466]---> BDD-cost:   10
c ---[3465]---> BDD-cost:   10
c ---[3464]---> BDD-cost:   10
c ---[3463]---> BDD-cost:   10
c ---[3462]---> BDD-cost:   10
c ---[3461]---> BDD-cost:   10
c ---[3460]---> BDD-cost:   10
c ---[3459]---> BDD-cost:   10
c ---[3458]---> BDD-cost:   10
c ---[3457]---> BDD-cost:   10
c ---[3456]---> BDD-cost:   10
c ---[3455]---> BDD-cost:   10
c ---[3454]---> BDD-cost:   10
c ---[3453]---> BDD-cost:   10
c ---[3452]---> BDD-cost:   10
c ---[3451]---> BDD-cost:   10
c ---[3450]---> BDD-cost:   10
c ---[3449]---> BDD-cost:   10
c ---[3448]---> BDD-cost:   10
c ---[3447]---> BDD-cost:   10
c ---[3446]---> BDD-cost:   10
c ---[3445]---> BDD-cost:   10
c ---[3444]---> BDD-cost:   10
c ---[3443]---> BDD-cost:   10
c ---[3438]---> BDD-cost:   10
c ---[3437]---> BDD-cost:   10
c ---[3436]---> BDD-cost:   10
c ---[3435]---> BDD-cost:   10
c ---[3434]---> BDD-cost:   10
c ---[3433]---> BDD-cost:   10
c ---[3432]---> BDD-cost:   10
c ---[3431]---> BDD-cost:   10
c ---[3430]---> BDD-cost:   10
c ---[3429]---> BDD-cost:   10
c ---[3428]---> BDD-cost:   10
c ---[3427]---> BDD-cost:   10
c ---[3426]---> BDD-cost:   10
c ---[3425]---> BDD-cost:   10
c ---[3424]---> BDD-cost:   10
c ---[3423]---> BDD-cost:   10
c ---[3422]---> BDD-cost:   10
c ---[3421]---> BDD-cost:   10
c ---[3420]---> BDD-cost:   10
c ---[3419]---> BDD-cost:   10
c ---[3418]---> BDD-cost:   10
c ---[3417]---> BDD-cost:   10
c ---[3416]---> BDD-cost:   10
c ---[3415]---> BDD-cost:   10
c ---[3414]---> BDD-cost:   10
c ---[3413]---> BDD-cost:   10
c ---[3412]---> BDD-cost:   10
c ---[3411]---> BDD-cost:   10
c ---[3410]---> BDD-cost:   10
c ---[3409]---> BDD-cost:   10
c ---[3408]---> BDD-cost:   10
c ---[3407]---> BDD-cost:   10
c ---[3406]---> BDD-cost:   10
c ---[3405]---> BDD-cost:   10
c ---[3404]---> BDD-cost:   10
c ---[3403]---> BDD-cost:   10
c ---[3402]---> BDD-cost:   10
c ---[3401]---> BDD-cost:   10
c ---[3400]---> BDD-cost:   10
c ---[3399]---> BDD-cost:   10
c ---[3398]---> BDD-cost:   10
c ---[3397]---> BDD-cost:   10
c ---[3396]---> BDD-cost:   10
c ---[3395]---> BDD-cost:   10
c ---[3394]---> BDD-cost:   10
c ---[3393]---> BDD-cost:   10
c ---[3392]---> BDD-cost:   10
c ---[3391]---> BDD-cost:   10
c ---[3390]---> BDD-cost:   10
c ---[3389]---> BDD-cost:   10
c ---[3388]---> BDD-cost:   10
c ---[3387]---> BDD-cost:   10
c ---[3386]---> BDD-cost:   10
c ---[3385]---> BDD-cost:   10
c ---[3384]---> BDD-cost:   10
c ---[3383]---> BDD-cost:   10
c ---[3382]---> BDD-cost:   10
c ---[3381]---> BDD-cost:   10
c ---[3380]---> BDD-cost:   10
c ---[3379]---> BDD-cost:   10
c ---[3378]---> BDD-cost:   10
c ---[3377]---> BDD-cost:   10
c ---[3376]---> BDD-cost:   10
c ---[3375]---> BDD-cost:   10
c ---[3374]---> BDD-cost:   10
c ---[3373]---> BDD-cost:   10
c ---[3372]---> BDD-cost:   10
c ---[3371]---> BDD-cost:   10
c ---[3370]---> BDD-cost:   10
c ---[3369]---> BDD-cost:   10
c ---[3368]---> BDD-cost:   10
c ---[3367]---> BDD-cost:   10
c ---[3366]---> BDD-cost:   10
c ---[3365]---> BDD-cost:   10
c ---[3364]---> BDD-cost:   10
c ---[3363]---> BDD-cost:   10
c ---[3362]---> BDD-cost:   10
c ---[3361]---> BDD-cost:   10
c ---[3356]---> BDD-cost:   10
c ---[3355]---> BDD-cost:   10
c ---[3354]---> BDD-cost:   10
c ---[3353]---> BDD-cost:   10
c ---[3352]---> BDD-cost:   10
c ---[3351]---> BDD-cost:   10
c ---[3350]---> BDD-cost:   10
c ---[3349]---> BDD-cost:   10
c ---[3348]---> BDD-cost:   10
c ---[3347]---> BDD-cost:   10
c ---[3346]---> BDD-cost:   10
c ---[3345]---> BDD-cost:   10
c ---[3344]---> BDD-cost:   10
c ---[3343]---> BDD-cost:   10
c ---[3342]---> BDD-cost:   10
c ---[3341]---> BDD-cost:   10
c ---[3340]---> BDD-cost:   10
c ---[3339]---> BDD-cost:   10
c ---[3338]---> BDD-cost:   10
c ---[3337]---> BDD-cost:   10
c ---[3336]---> BDD-cost:   10
c ---[3335]---> BDD-cost:   10
c ---[3334]---> BDD-cost:   10
c ---[3333]---> BDD-cost:   10
c ---[3332]---> BDD-cost:   10
c ---[3331]---> BDD-cost:   10
c ---[3330]---> BDD-cost:   10
c ---[3329]---> BDD-cost:   10
c ---[3328]---> BDD-cost:   10
c ---[3327]---> BDD-cost:   10
c ---[3326]---> BDD-cost:   10
c ---[3325]---> BDD-cost:   10
c ---[3324]---> BDD-cost:   10
c ---[3323]---> BDD-cost:   10
c ---[3322]---> BDD-cost:   10
c ---[3321]---> BDD-cost:   10
c ---[3320]---> BDD-cost:   10
c ---[3319]---> BDD-cost:   10
c ---[3318]---> BDD-cost:   10
c ---[3317]---> BDD-cost:   10
c ---[3316]---> BDD-cost:   10
c ---[3315]---> BDD-cost:   10
c ---[3314]---> BDD-cost:   10
c ---[3313]---> BDD-cost:   10
c ---[3312]---> BDD-cost:   10
c ---[3311]---> BDD-cost:   10
c ---[3310]---> BDD-cost:   10
c ---[3309]---> BDD-cost:   10
c ---[3308]---> BDD-cost:   10
c ---[3307]---> BDD-cost:   10
c ---[3306]---> BDD-cost:   10
c ---[3305]---> BDD-cost:   10
c ---[3304]---> BDD-cost:   10
c ---[3303]---> BDD-cost:   10
c ---[3302]---> BDD-cost:   10
c ---[3301]---> BDD-cost:   10
c ---[3300]---> BDD-cost:   10
c ---[3299]---> BDD-cost:   10
c ---[3298]---> BDD-cost:   10
c ---[3297]---> BDD-cost:   10
c ---[3296]---> BDD-cost:   10
c ---[3295]---> BDD-cost:   10
c ---[3294]---> BDD-cost:   10
c ---[3293]---> BDD-cost:   10
c ---[3292]---> BDD-cost:   10
c ---[3291]---> BDD-cost:   10
c ---[3290]---> BDD-cost:   10
c ---[3289]---> BDD-cost:   10
c ---[3288]---> BDD-cost:   10
c ---[3287]---> BDD-cost:   10
c ---[3286]---> BDD-cost:   10
c ---[3285]---> BDD-cost:   10
c ---[3284]---> BDD-cost:   10
c ---[3283]---> BDD-cost:   10
c ---[3282]---> BDD-cost:   10
c ---[3281]---> BDD-cost:   10
c ---[3280]---> BDD-cost:   10
c ---[3279]---> BDD-cost:   10
c ---[3274]---> BDD-cost:   10
c ---[3273]---> BDD-cost:   10
c ---[3272]---> BDD-cost:   10
c ---[3271]---> BDD-cost:   10
c ---[3270]---> BDD-cost:   10
c ---[3269]---> BDD-cost:   10
c ---[3268]---> BDD-cost:   10
c ---[3267]---> BDD-cost:   10
c ---[3266]---> BDD-cost:   10
c ---[3265]---> BDD-cost:   10
c ---[3264]---> BDD-cost:   10
c ---[3263]---> BDD-cost:   10
c ---[3262]---> BDD-cost:   10
c ---[3261]---> BDD-cost:   10
c ---[3260]---> BDD-cost:   10
c ---[3259]---> BDD-cost:   10
c ---[3258]---> BDD-cost:   10
c ---[3257]---> BDD-cost:   10
c ---[3256]---> BDD-cost:   10
c ---[3255]---> BDD-cost:   10
c ---[3254]---> BDD-cost:   10
c ---[3253]---> BDD-cost:   10
c ---[3252]---> BDD-cost:   10
c ---[3251]---> BDD-cost:   10
c ---[3250]---> BDD-cost:   10
c ---[3249]---> BDD-cost:   10
c ---[3248]---> BDD-cost:   10
c ---[3247]---> BDD-cost:   10
c ---[3246]---> BDD-cost:   10
c ---[3245]---> BDD-cost:   10
c ---[3244]---> BDD-cost:   10
c ---[3243]---> BDD-cost:   10
c ---[3242]---> BDD-cost:   10
c ---[3241]---> BDD-cost:   10
c ---[3240]---> BDD-cost:   10
c ---[3239]---> BDD-cost:   10
c ---[3238]---> BDD-cost:   10
c ---[3237]---> BDD-cost:   10
c ---[3236]---> BDD-cost:   10
c ---[3235]---> BDD-cost:   10
c ---[3234]---> BDD-cost:   10
c ---[3233]---> BDD-cost:   10
c ---[3232]---> BDD-cost:   10
c ---[3231]---> BDD-cost:   10
c ---[3230]---> BDD-cost:   10
c ---[3229]---> BDD-cost:   10
c ---[3228]---> BDD-cost:   10
c ---[3227]---> BDD-cost:   10
c ---[3226]---> BDD-cost:   10
c ---[3225]---> BDD-cost:   10
c ---[3224]---> BDD-cost:   10
c ---[3223]---> BDD-cost:   10
c ---[3222]---> BDD-cost:   10
c ---[3221]---> BDD-cost:   10
c ---[3220]---> BDD-cost:   10
c ---[3219]---> BDD-cost:   10
c ---[3218]---> BDD-cost:   10
c ---[3217]---> BDD-cost:   10
c ---[3216]---> BDD-cost:   10
c ---[3215]---> BDD-cost:   10
c ---[3214]---> BDD-cost:   10
c ---[3213]---> BDD-cost:   10
c ---[3212]---> BDD-cost:   10
c ---[3211]---> BDD-cost:   10
c ---[3210]---> BDD-cost:   10
c ---[3209]---> BDD-cost:   10
c ---[3208]---> BDD-cost:   10
c ---[3207]---> BDD-cost:   10
c ---[3206]---> BDD-cost:   10
c ---[3205]---> BDD-cost:   10
c ---[3204]---> BDD-cost:   10
c ---[3203]---> BDD-cost:   10
c ---[3202]---> BDD-cost:   10
c ---[3201]---> BDD-cost:   10
c ---[3200]---> BDD-cost:   10
c ---[3199]---> BDD-cost:   10
c ---[3198]---> BDD-cost:   10
c ---[3197]---> BDD-cost:   10
c ---[3196]---> BDD-cost:   10
c ---[3195]---> BDD-cost:   10
c ---[3194]---> BDD-cost:   10
c ---[3193]---> BDD-cost:   10
c ---[3188]---> BDD-cost:   10
c ---[3187]---> BDD-cost:   10
c ---[3186]---> BDD-cost:   10
c ---[3185]---> BDD-cost:   10
c ---[3184]---> BDD-cost:   10
c ---[3183]---> BDD-cost:   10
c ---[3182]---> BDD-cost:   10
c ---[3181]---> BDD-cost:   10
c ---[3180]---> BDD-cost:   10
c ---[3179]---> BDD-cost:   10
c ---[3178]---> BDD-cost:   10
c ---[3177]---> BDD-cost:   10
c ---[3176]---> BDD-cost:   10
c ---[3175]---> BDD-cost:   10
c ---[3174]---> BDD-cost:   10
c ---[3173]---> BDD-cost:   10
c ---[3172]---> BDD-cost:   10
c ---[3171]---> BDD-cost:   10
c ---[3170]---> BDD-cost:   10
c ---[3169]---> BDD-cost:   10
c ---[3168]---> BDD-cost:   10
c ---[3167]---> BDD-cost:   10
c ---[3166]---> BDD-cost:   10
c ---[3165]---> BDD-cost:   10
c ---[3164]---> BDD-cost:   10
c ---[3163]---> BDD-cost:   10
c ---[3162]---> BDD-cost:   10
c ---[3161]---> BDD-cost:   10
c ---[3160]---> BDD-cost:   10
c ---[3159]---> BDD-cost:   10
c ---[3158]---> BDD-cost:   10
c ---[3157]---> BDD-cost:   10
c ---[3156]---> BDD-cost:   10
c ---[3155]---> BDD-cost:   10
c ---[3154]---> BDD-cost:   10
c ---[3153]---> BDD-cost:   10
c ---[3152]---> BDD-cost:   10
c ---[3151]---> BDD-cost:   10
c ---[3150]---> BDD-cost:   10
c ---[3149]---> BDD-cost:   10
c ---[3148]---> BDD-cost:   10
c ---[3147]---> BDD-cost:   10
c ---[3146]---> BDD-cost:   10
c ---[3145]---> BDD-cost:   10
c ---[3144]---> BDD-cost:   10
c ---[3143]---> BDD-cost:   10
c ---[3142]---> BDD-cost:   10
c ---[3141]---> BDD-cost:   10
c ---[3140]---> BDD-cost:   10
c ---[3139]---> BDD-cost:   10
c ---[3138]---> BDD-cost:   10
c ---[3137]---> BDD-cost:   10
c ---[3136]---> BDD-cost:   10
c ---[3135]---> BDD-cost:   10
c ---[3134]---> BDD-cost:   10
c ---[3133]---> BDD-cost:   10
c ---[3132]---> BDD-cost:   10
c ---[3131]---> BDD-cost:   10
c ---[3130]---> BDD-cost:   10
c ---[3129]---> BDD-cost:   10
c ---[3128]---> BDD-cost:   10
c ---[3127]---> BDD-cost:   10
c ---[3126]---> BDD-cost:   10
c ---[3125]---> BDD-cost:   10
c ---[3124]---> BDD-cost:   10
c ---[3123]---> BDD-cost:   10
c ---[3122]---> BDD-cost:   10
c ---[3121]---> BDD-cost:   10
c ---[3120]---> BDD-cost:   10
c ---[3119]---> BDD-cost:   10
c ---[3118]---> BDD-cost:   10
c ---[3117]---> BDD-cost:   10
c ---[3116]---> BDD-cost:   10
c ---[3115]---> BDD-cost:   10
c ---[3114]---> BDD-cost:   10
c ---[3113]---> BDD-cost:   10
c ---[3112]---> BDD-cost:   10
c ---[3111]---> BDD-cost:   10
c ---[3106]---> BDD-cost:   10
c ---[3105]---> BDD-cost:   10
c ---[3104]---> BDD-cost:   10
c ---[3103]---> BDD-cost:   10
c ---[3102]---> BDD-cost:   10
c ---[3101]---> BDD-cost:   10
c ---[3100]---> BDD-cost:   10
c ---[3099]---> BDD-cost:   10
c ---[3098]---> BDD-cost:   10
c ---[3097]---> BDD-cost:   10
c ---[3096]---> BDD-cost:   10
c ---[3095]---> BDD-cost:   10
c ---[3094]---> BDD-cost:   10
c ---[3093]---> BDD-cost:   10
c ---[3092]---> BDD-cost:   10
c ---[3091]---> BDD-cost:   10
c ---[3090]---> BDD-cost:   10
c ---[3089]---> BDD-cost:   10
c ---[3088]---> BDD-cost:   10
c ---[3087]---> BDD-cost:   10
c ---[3086]---> BDD-cost:   10
c ---[3085]---> BDD-cost:   10
c ---[3084]---> BDD-cost:   10
c ---[3083]---> BDD-cost:   10
c ---[3082]---> BDD-cost:   10
c ---[3081]---> BDD-cost:   10
c ---[3080]---> BDD-cost:   10
c ---[3079]---> BDD-cost:   10
c ---[3078]---> BDD-cost:   10
c ---[3077]---> BDD-cost:   10
c ---[3076]---> BDD-cost:   10
c ---[3075]---> BDD-cost:   10
c ---[3074]---> BDD-cost:   10
c ---[3073]---> BDD-cost:   10
c ---[3072]---> BDD-cost:   10
c ---[3071]---> BDD-cost:   10
c ---[3070]---> BDD-cost:   10
c ---[3069]---> BDD-cost:   10
c ---[3068]---> BDD-cost:   10
c ---[3067]---> BDD-cost:   10
c ---[3066]---> BDD-cost:   10
c ---[3065]---> BDD-cost:   10
c ---[3064]---> BDD-cost:   10
c ---[3063]---> BDD-cost:   10
c ---[3062]---> BDD-cost:   10
c ---[3061]---> BDD-cost:   10
c ---[3060]---> BDD-cost:   10
c ---[3059]---> BDD-cost:   10
c ---[3058]---> BDD-cost:   10
c ---[3057]---> BDD-cost:   10
c ---[3056]---> BDD-cost:   10
c ---[3055]---> BDD-cost:   10
c ---[3054]---> BDD-cost:   10
c ---[3053]---> BDD-cost:   10
c ---[3052]---> BDD-cost:   10
c ---[3051]---> BDD-cost:   10
c ---[3050]---> BDD-cost:   10
c ---[3049]---> BDD-cost:   10
c ---[3048]---> BDD-cost:   10
c ---[3047]---> BDD-cost:   10
c ---[3046]---> BDD-cost:   10
c ---[3045]---> BDD-cost:   10
c ---[3044]---> BDD-cost:   10
c ---[3043]---> BDD-cost:   10
c ---[3042]---> BDD-cost:   10
c ---[3041]---> BDD-cost:   10
c ---[3040]---> BDD-cost:   10
c ---[3039]---> BDD-cost:   10
c ---[3038]---> BDD-cost:   10
c ---[3037]---> BDD-cost:   10
c ---[3036]---> BDD-cost:   10
c ---[3035]---> BDD-cost:   10
c ---[3034]---> BDD-cost:   10
c ---[3033]---> BDD-cost:   10
c ---[3032]---> BDD-cost:   10
c ---[3031]---> BDD-cost:   10
c ---[3030]---> BDD-cost:   10
c ---[3029]---> BDD-cost:   10
c ---[3024]---> BDD-cost:   10
c ---[3023]---> BDD-cost:   10
c ---[3022]---> BDD-cost:   10
c ---[3021]---> BDD-cost:   10
c ---[3020]---> BDD-cost:   10
c ---[3019]---> BDD-cost:   10
c ---[3018]---> BDD-cost:   10
c ---[3017]---> BDD-cost:   10
c ---[3016]---> BDD-cost:   10
c ---[3015]---> BDD-cost:   10
c ---[3014]---> BDD-cost:   10
c ---[3013]---> BDD-cost:   10
c ---[3012]---> BDD-cost:   10
c ---[3011]---> BDD-cost:   10
c ---[3010]---> BDD-cost:   10
c ---[3009]---> BDD-cost:   10
c ---[3008]---> BDD-cost:   10
c ---[3007]---> BDD-cost:   10
c ---[3006]---> BDD-cost:   10
c ---[3005]---> BDD-cost:   10
c ---[3004]---> BDD-cost:   10
c ---[3003]---> BDD-cost:   10
c ---[3002]---> BDD-cost:   10
c ---[3001]---> BDD-cost:   10
c ---[3000]---> BDD-cost:   10
c ---[2999]---> BDD-cost:   10
c ---[2998]---> BDD-cost:   10
c ---[2997]---> BDD-cost:   10
c ---[2996]---> BDD-cost:   10
c ---[2995]---> BDD-cost:   10
c ---[2994]---> BDD-cost:   10
c ---[2993]---> BDD-cost:   10
c ---[2992]---> BDD-cost:   10
c ---[2991]---> BDD-cost:   10
c ---[2990]---> BDD-cost:   10
c ---[2989]---> BDD-cost:   10
c ---[2988]---> BDD-cost:   10
c ---[2987]---> BDD-cost:   10
c ---[2986]---> BDD-cost:   10
c ---[2985]---> BDD-cost:   10
c ---[2984]---> BDD-cost:   10
c ---[2983]---> BDD-cost:   10
c ---[2982]---> BDD-cost:   10
c ---[2981]---> BDD-cost:   10
c ---[2980]---> BDD-cost:   10
c ---[2979]---> BDD-cost:   10
c ---[2978]---> BDD-cost:   10
c ---[2977]---> BDD-cost:   10
c ---[2976]---> BDD-cost:   10
c ---[2975]---> BDD-cost:   10
c ---[2974]---> BDD-cost:   10
c ---[2973]---> BDD-cost:   10
c ---[2972]---> BDD-cost:   10
c ---[2971]---> BDD-cost:   10
c ---[2970]---> BDD-cost:   10
c ---[2969]---> BDD-cost:   10
c ---[2968]---> BDD-cost:   10
c ---[2967]---> BDD-cost:   10
c ---[2966]---> BDD-cost:   10
c ---[2965]---> BDD-cost:   10
c ---[2964]---> BDD-cost:   10
c ---[2963]---> BDD-cost:   10
c ---[2962]---> BDD-cost:   10
c ---[2961]---> BDD-cost:   10
c ---[2960]---> BDD-cost:   10
c ---[2959]---> BDD-cost:   10
c ---[2958]---> BDD-cost:   10
c ---[2957]---> BDD-cost:   10
c ---[2956]---> BDD-cost:   10
c ---[2955]---> BDD-cost:   10
c ---[2954]---> BDD-cost:   10
c ---[2953]---> BDD-cost:   10
c ---[2952]---> BDD-cost:   10
c ---[2951]---> BDD-cost:   10
c ---[2950]---> BDD-cost:   10
c ---[2949]---> BDD-cost:   10
c ---[2948]---> BDD-cost:   10
c ---[2947]---> BDD-cost:   10
c ---[2942]---> BDD-cost:   10
c ---[2941]---> BDD-cost:   10
c ---[2940]---> BDD-cost:   10
c ---[2939]---> BDD-cost:   10
c ---[2938]---> BDD-cost:   10
c ---[2937]---> BDD-cost:   10
c ---[2936]---> BDD-cost:   10
c ---[2935]---> BDD-cost:   10
c ---[2934]---> BDD-cost:   10
c ---[2933]---> BDD-cost:   10
c ---[2932]---> BDD-cost:   10
c ---[2931]---> BDD-cost:   10
c ---[2930]---> BDD-cost:   10
c ---[2929]---> BDD-cost:   10
c ---[2928]---> BDD-cost:   10
c ---[2927]---> BDD-cost:   10
c ---[2926]---> BDD-cost:   10
c ---[2925]---> BDD-cost:   10
c ---[2924]---> BDD-cost:   10
c ---[2923]---> BDD-cost:   10
c ---[2922]---> BDD-cost:   10
c ---[2921]---> BDD-cost:   10
c ---[2920]---> BDD-cost:   10
c ---[2919]---> BDD-cost:   10
c ---[2918]---> BDD-cost:   10
c ---[2917]---> BDD-cost:   10
c ---[2916]---> BDD-cost:   10
c ---[2915]---> BDD-cost:   10
c ---[2914]---> BDD-cost:   10
c ---[2913]---> BDD-cost:   10
c ---[2912]---> BDD-cost:   10
c ---[2911]---> BDD-cost:   10
c ---[2910]---> BDD-cost:   10
c ---[2909]---> BDD-cost:   10
c ---[2908]---> BDD-cost:   10
c ---[2907]---> BDD-cost:   10
c ---[2906]---> BDD-cost:   10
c ---[2905]---> BDD-cost:   10
c ---[2904]---> BDD-cost:   10
c ---[2903]---> BDD-cost:   10
c ---[2902]---> BDD-cost:   10
c ---[2901]---> BDD-cost:   10
c ---[2900]---> BDD-cost:   10
c ---[2899]---> BDD-cost:   10
c ---[2898]---> BDD-cost:   10
c ---[2897]---> BDD-cost:   10
c ---[2896]---> BDD-cost:   10
c ---[2895]---> BDD-cost:   10
c ---[2894]---> BDD-cost:   10
c ---[2893]---> BDD-cost:   10
c ---[2892]---> BDD-cost:   10
c ---[2891]---> BDD-cost:   10
c ---[2890]---> BDD-cost:   10
c ---[2889]---> BDD-cost:   10
c ---[2888]---> BDD-cost:   10
c ---[2887]---> BDD-cost:   10
c ---[2886]---> BDD-cost:   10
c ---[2885]---> BDD-cost:   10
c ---[2884]---> BDD-cost:   10
c ---[2883]---> BDD-cost:   10
c ---[2882]---> BDD-cost:   10
c ---[2881]---> BDD-cost:   10
c ---[2880]---> BDD-cost:   10
c ---[2879]---> BDD-cost:   10
c ---[2878]---> BDD-cost:   10
c ---[2877]---> BDD-cost:   10
c ---[2876]---> BDD-cost:   10
c ---[2875]---> BDD-cost:   10
c ---[2874]---> BDD-cost:   10
c ---[2873]---> BDD-cost:   10
c ---[2872]---> BDD-cost:   10
c ---[2871]---> BDD-cost:   10
c ---[2870]---> BDD-cost:   10
c ---[2869]---> BDD-cost:   10
c ---[2868]---> BDD-cost:   10
c ---[2867]---> BDD-cost:   10
c ---[2866]---> BDD-cost:   10
c ---[2865]---> BDD-cost:   10
c ---[2864]---> BDD-cost:   10
c ---[2863]---> BDD-cost:   10
c ---[2862]---> BDD-cost:   10
c ---[2861]---> BDD-cost:   10
c ---[2856]---> BDD-cost:   10
c ---[2855]---> BDD-cost:   10
c ---[2854]---> BDD-cost:   10
c ---[2853]---> BDD-cost:   10
c ---[2852]---> BDD-cost:   10
c ---[2851]---> BDD-cost:   10
c ---[2850]---> BDD-cost:   10
c ---[2849]---> BDD-cost:   10
c ---[2848]---> BDD-cost:   10
c ---[2847]---> BDD-cost:   10
c ---[2846]---> BDD-cost:   10
c ---[2845]---> BDD-cost:   10
c ---[2844]---> BDD-cost:   10
c ---[2843]---> BDD-cost:   10
c ---[2842]---> BDD-cost:   10
c ---[2841]---> BDD-cost:   10
c ---[2840]---> BDD-cost:   10
c ---[2839]---> BDD-cost:   10
c ---[2838]---> BDD-cost:   10
c ---[2837]---> BDD-cost:   10
c ---[2836]---> BDD-cost:   10
c ---[2835]---> BDD-cost:   10
c ---[2834]---> BDD-cost:   10
c ---[2833]---> BDD-cost:   10
c ---[2832]---> BDD-cost:   10
c ---[2831]---> BDD-cost:   10
c ---[2830]---> BDD-cost:   10
c ---[2829]---> BDD-cost:   10
c ---[2828]---> BDD-cost:   10
c ---[2827]---> BDD-cost:   10
c ---[2826]---> BDD-cost:   10
c ---[2825]---> BDD-cost:   10
c ---[2824]---> BDD-cost:   10
c ---[2823]---> BDD-cost:   10
c ---[2822]---> BDD-cost:   10
c ---[2821]---> BDD-cost:   10
c ---[2820]---> BDD-cost:   10
c ---[2819]---> BDD-cost:   10
c ---[2818]---> BDD-cost:   10
c ---[2817]---> BDD-cost:   10
c ---[2816]---> BDD-cost:   10
c ---[2815]---> BDD-cost:   10
c ---[2814]---> BDD-cost:   10
c ---[2813]---> BDD-cost:   10
c ---[2812]---> BDD-cost:   10
c ---[2811]---> BDD-cost:   10
c ---[2810]---> BDD-cost:   10
c ---[2809]---> BDD-cost:   10
c ---[2808]---> BDD-cost:   10
c ---[2807]---> BDD-cost:   10
c ---[2806]---> BDD-cost:   10
c ---[2805]---> BDD-cost:   10
c ---[2804]---> BDD-cost:   10
c ---[2803]---> BDD-cost:   10
c ---[2802]---> BDD-cost:   10
c ---[2801]---> BDD-cost:   10
c ---[2800]---> BDD-cost:   10
c ---[2799]---> BDD-cost:   10
c ---[2798]---> BDD-cost:   10
c ---[2797]---> BDD-cost:   10
c ---[2796]---> BDD-cost:   10
c ---[2795]---> BDD-cost:   10
c ---[2794]---> BDD-cost:   10
c ---[2793]---> BDD-cost:   10
c ---[2792]---> BDD-cost:   10
c ---[2791]---> BDD-cost:   10
c ---[2790]---> BDD-cost:   10
c ---[2789]---> BDD-cost:   10
c ---[2788]---> BDD-cost:   10
c ---[2787]---> BDD-cost:   10
c ---[2786]---> BDD-cost:   10
c ---[2785]---> BDD-cost:   10
c ---[2784]---> BDD-cost:   10
c ---[2783]---> BDD-cost:   10
c ---[2782]---> BDD-cost:   10
c ---[2781]---> BDD-cost:   10
c ---[2780]---> BDD-cost:   10
c ---[2779]---> BDD-cost:   10
c ---[2774]---> BDD-cost:   10
c ---[2773]---> BDD-cost:   10
c ---[2772]---> BDD-cost:   10
c ---[2771]---> BDD-cost:   10
c ---[2770]---> BDD-cost:   10
c ---[2769]---> BDD-cost:   10
c ---[2768]---> BDD-cost:   10
c ---[2767]---> BDD-cost:   10
c ---[2766]---> BDD-cost:   10
c ---[2765]---> BDD-cost:   10
c ---[2764]---> BDD-cost:   10
c ---[2763]---> BDD-cost:   10
c ---[2762]---> BDD-cost:   10
c ---[2761]---> BDD-cost:   10
c ---[2760]---> BDD-cost:   10
c ---[2759]---> BDD-cost:   10
c ---[2758]---> BDD-cost:   10
c ---[2757]---> BDD-cost:   10
c ---[2756]---> BDD-cost:   10
c ---[2755]---> BDD-cost:   10
c ---[2754]---> BDD-cost:   10
c ---[2753]---> BDD-cost:   10
c ---[2752]---> BDD-cost:   10
c ---[2751]---> BDD-cost:   10
c ---[2750]---> BDD-cost:   10
c ---[2749]---> BDD-cost:   10
c ---[2748]---> BDD-cost:   10
c ---[2747]---> BDD-cost:   10
c ---[2746]---> BDD-cost:   10
c ---[2745]---> BDD-cost:   10
c ---[2744]---> BDD-cost:   10
c ---[2743]---> BDD-cost:   10
c ---[2742]---> BDD-cost:   10
c ---[2741]---> BDD-cost:   10
c ---[2740]---> BDD-cost:   10
c ---[2739]---> BDD-cost:   10
c ---[2738]---> BDD-cost:   10
c ---[2737]---> BDD-cost:   10
c ---[2736]---> BDD-cost:   10
c ---[2735]---> BDD-cost:   10
c ---[2734]---> BDD-cost:   10
c ---[2733]---> BDD-cost:   10
c ---[2732]---> BDD-cost:   10
c ---[2731]---> BDD-cost:   10
c ---[2730]---> BDD-cost:   10
c ---[2729]---> BDD-cost:   10
c ---[2728]---> BDD-cost:   10
c ---[2727]---> BDD-cost:   10
c ---[2726]---> BDD-cost:   10
c ---[2725]---> BDD-cost:   10
c ---[2724]---> BDD-cost:   10
c ---[2723]---> BDD-cost:   10
c ---[2722]---> BDD-cost:   10
c ---[2721]---> BDD-cost:   10
c ---[2720]---> BDD-cost:   10
c ---[2719]---> BDD-cost:   10
c ---[2718]---> BDD-cost:   10
c ---[2717]---> BDD-cost:   10
c ---[2716]---> BDD-cost:   10
c ---[2715]---> BDD-cost:   10
c ---[2714]---> BDD-cost:   10
c ---[2713]---> BDD-cost:   10
c ---[2712]---> BDD-cost:   10
c ---[2711]---> BDD-cost:   10
c ---[2710]---> BDD-cost:   10
c ---[2709]---> BDD-cost:   10
c ---[2708]---> BDD-cost:   10
c ---[2707]---> BDD-cost:   10
c ---[2706]---> BDD-cost:   10
c ---[2705]---> BDD-cost:   10
c ---[2704]---> BDD-cost:   10
c ---[2703]---> BDD-cost:   10
c ---[2702]---> BDD-cost:   10
c ---[2701]---> BDD-cost:   10
c ---[2700]---> BDD-cost:   10
c ---[2699]---> BDD-cost:   10
c ---[2698]---> BDD-cost:   10
c ---[2697]---> BDD-cost:   10
c ---[2692]---> BDD-cost:   10
c ---[2691]---> BDD-cost:   10
c ---[2690]---> BDD-cost:   10
c ---[2689]---> BDD-cost:   10
c ---[2688]---> BDD-cost:   10
c ---[2687]---> BDD-cost:   10
c ---[2686]---> BDD-cost:   10
c ---[2685]---> BDD-cost:   10
c ---[2684]---> BDD-cost:   10
c ---[2683]---> BDD-cost:   10
c ---[2682]---> BDD-cost:   10
c ---[2681]---> BDD-cost:   10
c ---[2680]---> BDD-cost:   10
c ---[2679]---> BDD-cost:   10
c ---[2678]---> BDD-cost:   10
c ---[2677]---> BDD-cost:   10
c ---[2676]---> BDD-cost:   10
c ---[2675]---> BDD-cost:   10
c ---[2674]---> BDD-cost:   10
c ---[2673]---> BDD-cost:   10
c ---[2672]---> BDD-cost:   10
c ---[2671]---> BDD-cost:   10
c ---[2670]---> BDD-cost:   10
c ---[2669]---> BDD-cost:   10
c ---[2668]---> BDD-cost:   10
c ---[2667]---> BDD-cost:   10
c ---[2666]---> BDD-cost:   10
c ---[2665]---> BDD-cost:   10
c ---[2664]---> BDD-cost:   10
c ---[2663]---> BDD-cost:   10
c ---[2662]---> BDD-cost:   10
c ---[2661]---> BDD-cost:   10
c ---[2660]---> BDD-cost:   10
c ---[2659]---> BDD-cost:   10
c ---[2658]---> BDD-cost:   10
c ---[2657]---> BDD-cost:   10
c ---[2656]---> BDD-cost:   10
c ---[2655]---> BDD-cost:   10
c ---[2654]---> BDD-cost:   10
c ---[2653]---> BDD-cost:   10
c ---[2652]---> BDD-cost:   10
c ---[2651]---> BDD-cost:   10
c ---[2650]---> BDD-cost:   10
c ---[2649]---> BDD-cost:   10
c ---[2648]---> BDD-cost:   10
c ---[2647]---> BDD-cost:   10
c ---[2646]---> BDD-cost:   10
c ---[2645]---> BDD-cost:   10
c ---[2644]---> BDD-cost:   10
c ---[2643]---> BDD-cost:   10
c ---[2642]---> BDD-cost:   10
c ---[2641]---> BDD-cost:   10
c ---[2640]---> BDD-cost:   10
c ---[2639]---> BDD-cost:   10
c ---[2638]---> BDD-cost:   10
c ---[2637]---> BDD-cost:   10
c ---[2636]---> BDD-cost:   10
c ---[2635]---> BDD-cost:   10
c ---[2634]---> BDD-cost:   10
c ---[2633]---> BDD-cost:   10
c ---[2632]---> BDD-cost:   10
c ---[2631]---> BDD-cost:   10
c ---[2630]---> BDD-cost:   10
c ---[2629]---> BDD-cost:   10
c ---[2628]---> BDD-cost:   10
c ---[2627]---> BDD-cost:   10
c ---[2626]---> BDD-cost:   10
c ---[2625]---> BDD-cost:   10
c ---[2624]---> BDD-cost:   10
c ---[2623]---> BDD-cost:   10
c ---[2622]---> BDD-cost:   10
c ---[2621]---> BDD-cost:   10
c ---[2620]---> BDD-cost:   10
c ---[2619]---> BDD-cost:   10
c ---[2618]---> BDD-cost:   10
c ---[2617]---> BDD-cost:   10
c ---[2616]---> BDD-cost:   10
c ---[2615]---> BDD-cost:   10
c ---[2610]---> BDD-cost:   10
c ---[2609]---> BDD-cost:   10
c ---[2608]---> BDD-cost:   10
c ---[2607]---> BDD-cost:   10
c ---[2606]---> BDD-cost:   10
c ---[2605]---> BDD-cost:   10
c ---[2604]---> BDD-cost:   10
c ---[2603]---> BDD-cost:   10
c ---[2602]---> BDD-cost:   10
c ---[2601]---> BDD-cost:   10
c ---[2600]---> BDD-cost:   10
c ---[2599]---> BDD-cost:   10
c ---[2598]---> BDD-cost:   10
c ---[2597]---> BDD-cost:   10
c ---[2596]---> BDD-cost:   10
c ---[2595]---> BDD-cost:   10
c ---[2594]---> BDD-cost:   10
c ---[2593]---> BDD-cost:   10
c ---[2592]---> BDD-cost:   10
c ---[2591]---> BDD-cost:   10
c ---[2590]---> BDD-cost:   10
c ---[2589]---> BDD-cost:   10
c ---[2588]---> BDD-cost:   10
c ---[2587]---> BDD-cost:   10
c ---[2586]---> BDD-cost:   10
c ---[2585]---> BDD-cost:   10
c ---[2584]---> BDD-cost:   10
c ---[2583]---> BDD-cost:   10
c ---[2582]---> BDD-cost:   10
c ---[2581]---> BDD-cost:   10
c ---[2580]---> BDD-cost:   10
c ---[2579]---> BDD-cost:   10
c ---[2578]---> BDD-cost:   10
c ---[2577]---> BDD-cost:   10
c ---[2576]---> BDD-cost:   10
c ---[2575]---> BDD-cost:   10
c ---[2574]---> BDD-cost:   10
c ---[2573]---> BDD-cost:   10
c ---[2572]---> BDD-cost:   10
c ---[2571]---> BDD-cost:   10
c ---[2570]---> BDD-cost:   10
c ---[2569]---> BDD-cost:   10
c ---[2568]---> BDD-cost:   10
c ---[2567]---> BDD-cost:   10
c ---[2566]---> BDD-cost:   10
c ---[2565]---> BDD-cost:   10
c ---[2564]---> BDD-cost:   10
c ---[2563]---> BDD-cost:   10
c ---[2562]---> BDD-cost:   10
c ---[2561]---> BDD-cost:   10
c ---[2560]---> BDD-cost:   10
c ---[2559]---> BDD-cost:   10
c ---[2558]---> BDD-cost:   10
c ---[2557]---> BDD-cost:   10
c ---[2556]---> BDD-cost:   10
c ---[2555]---> BDD-cost:   10
c ---[2554]---> BDD-cost:   10
c ---[2553]---> BDD-cost:   10
c ---[2552]---> BDD-cost:   10
c ---[2551]---> BDD-cost:   10
c ---[2550]---> BDD-cost:   10
c ---[2549]---> BDD-cost:   10
c ---[2548]---> BDD-cost:   10
c ---[2547]---> BDD-cost:   10
c ---[2546]---> BDD-cost:   10
c ---[2545]---> BDD-cost:   10
c ---[2544]---> BDD-cost:   10
c ---[2543]---> BDD-cost:   10
c ---[2542]---> BDD-cost:   10
c ---[2541]---> BDD-cost:   10
c ---[2540]---> BDD-cost:   10
c ---[2539]---> BDD-cost:   10
c ---[2538]---> BDD-cost:   10
c ---[2537]---> BDD-cost:   10
c ---[2536]---> BDD-cost:   10
c ---[2535]---> BDD-cost:   10
c ---[2534]---> BDD-cost:   10
c ---[2533]---> BDD-cost:   10
c ---[2532]---> BDD-cost:   10
c ---[2531]---> BDD-cost:   10
c ---[2530]---> BDD-cost:   10
c ---[2529]---> BDD-cost:   10
c ---[2524]---> BDD-cost:   10
c ---[2523]---> BDD-cost:   10
c ---[2522]---> BDD-cost:   10
c ---[2521]---> BDD-cost:   10
c ---[2520]---> BDD-cost:   10
c ---[2519]---> BDD-cost:   10
c ---[2518]---> BDD-cost:   10
c ---[2517]---> BDD-cost:   10
c ---[2516]---> BDD-cost:   10
c ---[2515]---> BDD-cost:   10
c ---[2514]---> BDD-cost:   10
c ---[2513]---> BDD-cost:   10
c ---[2512]---> BDD-cost:   10
c ---[2511]---> BDD-cost:   10
c ---[2510]---> BDD-cost:   10
c ---[2509]---> BDD-cost:   10
c ---[2508]---> BDD-cost:   10
c ---[2507]---> BDD-cost:   10
c ---[2506]---> BDD-cost:   10
c ---[2505]---> BDD-cost:   10
c ---[2504]---> BDD-cost:   10
c ---[2503]---> BDD-cost:   10
c ---[2502]---> BDD-cost:   10
c ---[2501]---> BDD-cost:   10
c ---[2500]---> BDD-cost:   10
c ---[2499]---> BDD-cost:   10
c ---[2498]---> BDD-cost:   10
c ---[2497]---> BDD-cost:   10
c ---[2496]---> BDD-cost:   10
c ---[2495]---> BDD-cost:   10
c ---[2494]---> BDD-cost:   10
c ---[2493]---> BDD-cost:   10
c ---[2492]---> BDD-cost:   10
c ---[2491]---> BDD-cost:   10
c ---[2490]---> BDD-cost:   10
c ---[2489]---> BDD-cost:   10
c ---[2488]---> BDD-cost:   10
c ---[2487]---> BDD-cost:   10
c ---[2486]---> BDD-cost:   10
c ---[2485]---> BDD-cost:   10
c ---[2484]---> BDD-cost:   10
c ---[2483]---> BDD-cost:   10
c ---[2482]---> BDD-cost:   10
c ---[2481]---> BDD-cost:   10
c ---[2480]---> BDD-cost:   10
c ---[2479]---> BDD-cost:   10
c ---[2478]---> BDD-cost:   10
c ---[2477]---> BDD-cost:   10
c ---[2476]---> BDD-cost:   10
c ---[2475]---> BDD-cost:   10
c ---[2474]---> BDD-cost:   10
c ---[2473]---> BDD-cost:   10
c ---[2472]---> BDD-cost:   10
c ---[2471]---> BDD-cost:   10
c ---[2470]---> BDD-cost:   10
c ---[2469]---> BDD-cost:   10
c ---[2468]---> BDD-cost:   10
c ---[2467]---> BDD-cost:   10
c ---[2466]---> BDD-cost:   10
c ---[2465]---> BDD-cost:   10
c ---[2464]---> BDD-cost:   10
c ---[2463]---> BDD-cost:   10
c ---[2462]---> BDD-cost:   10
c ---[2461]---> BDD-cost:   10
c ---[2460]---> BDD-cost:   10
c ---[2459]---> BDD-cost:   10
c ---[2458]---> BDD-cost:   10
c ---[2457]---> BDD-cost:   10
c ---[2456]---> BDD-cost:   10
c ---[2455]---> BDD-cost:   10
c ---[2454]---> BDD-cost:   10
c ---[2453]---> BDD-cost:   10
c ---[2452]---> BDD-cost:   10
c ---[2451]---> BDD-cost:   10
c ---[2450]---> BDD-cost:   10
c ---[2449]---> BDD-cost:   10
c ---[2448]---> BDD-cost:   10
c ---[2447]---> BDD-cost:   10
c ---[2442]---> BDD-cost:   10
c ---[2441]---> BDD-cost:   10
c ---[2440]---> BDD-cost:   10
c ---[2439]---> BDD-cost:   10
c ---[2438]---> BDD-cost:   10
c ---[2437]---> BDD-cost:   10
c ---[2436]---> BDD-cost:   10
c ---[2435]---> BDD-cost:   10
c ---[2434]---> BDD-cost:   10
c ---[2433]---> BDD-cost:   10
c ---[2432]---> BDD-cost:   10
c ---[2431]---> BDD-cost:   10
c ---[2430]---> BDD-cost:   10
c ---[2429]---> BDD-cost:   10
c ---[2428]---> BDD-cost:   10
c ---[2427]---> BDD-cost:   10
c ---[2426]---> BDD-cost:   10
c ---[2425]---> BDD-cost:   10
c ---[2424]---> BDD-cost:   10
c ---[2423]---> BDD-cost:   10
c ---[2422]---> BDD-cost:   10
c ---[2421]---> BDD-cost:   10
c ---[2420]---> BDD-cost:   10
c ---[2419]---> BDD-cost:   10
c ---[2418]---> BDD-cost:   10
c ---[2417]---> BDD-cost:   10
c ---[2416]---> BDD-cost:   10
c ---[2415]---> BDD-cost:   10
c ---[2414]---> BDD-cost:   10
c ---[2413]---> BDD-cost:   10
c ---[2412]---> BDD-cost:   10
c ---[2411]---> BDD-cost:   10
c ---[2410]---> BDD-cost:   10
c ---[2409]---> BDD-cost:   10
c ---[2408]---> BDD-cost:   10
c ---[2407]---> BDD-cost:   10
c ---[2406]---> BDD-cost:   10
c ---[2405]---> BDD-cost:   10
c ---[2404]---> BDD-cost:   10
c ---[2403]---> BDD-cost:   10
c ---[2402]---> BDD-cost:   10
c ---[2401]---> BDD-cost:   10
c ---[2400]---> BDD-cost:   10
c ---[2399]---> BDD-cost:   10
c ---[2398]---> BDD-cost:   10
c ---[2397]---> BDD-cost:   10
c ---[2396]---> BDD-cost:   10
c ---[2395]---> BDD-cost:   10
c ---[2394]---> BDD-cost:   10
c ---[2393]---> BDD-cost:   10
c ---[2392]---> BDD-cost:   10
c ---[2391]---> BDD-cost:   10
c ---[2390]---> BDD-cost:   10
c ---[2389]---> BDD-cost:   10
c ---[2388]---> BDD-cost:   10
c ---[2387]---> BDD-cost:   10
c ---[2386]---> BDD-cost:   10
c ---[2385]---> BDD-cost:   10
c ---[2384]---> BDD-cost:   10
c ---[2383]---> BDD-cost:   10
c ---[2382]---> BDD-cost:   10
c ---[2381]---> BDD-cost:   10
c ---[2380]---> BDD-cost:   10
c ---[2379]---> BDD-cost:   10
c ---[2378]---> BDD-cost:   10
c ---[2377]---> BDD-cost:   10
c ---[2376]---> BDD-cost:   10
c ---[2375]---> BDD-cost:   10
c ---[2374]---> BDD-cost:   10
c ---[2373]---> BDD-cost:   10
c ---[2372]---> BDD-cost:   10
c ---[2371]---> BDD-cost:   10
c ---[2370]---> BDD-cost:   10
c ---[2369]---> BDD-cost:   10
c ---[2368]---> BDD-cost:   10
c ---[2367]---> BDD-cost:   10
c ---[2366]---> BDD-cost:   10
c ---[2365]---> BDD-cost:   10
c ---[2360]---> BDD-cost:   10
c ---[2359]---> BDD-cost:   10
c ---[2358]---> BDD-cost:   10
c ---[2357]---> BDD-cost:   10
c ---[2356]---> BDD-cost:   10
c ---[2355]---> BDD-cost:   10
c ---[2354]---> BDD-cost:   10
c ---[2353]---> BDD-cost:   10
c ---[2352]---> BDD-cost:   10
c ---[2351]---> BDD-cost:   10
c ---[2350]---> BDD-cost:   10
c ---[2349]---> BDD-cost:   10
c ---[2348]---> BDD-cost:   10
c ---[2347]---> BDD-cost:   10
c ---[2346]---> BDD-cost:   10
c ---[2345]---> BDD-cost:   10
c ---[2344]---> BDD-cost:   10
c ---[2343]---> BDD-cost:   10
c ---[2342]---> BDD-cost:   10
c ---[2341]---> BDD-cost:   10
c ---[2340]---> BDD-cost:   10
c ---[2339]---> BDD-cost:   10
c ---[2338]---> BDD-cost:   10
c ---[2337]---> BDD-cost:   10
c ---[2336]---> BDD-cost:   10
c ---[2335]---> BDD-cost:   10
c ---[2334]---> BDD-cost:   10
c ---[2333]---> BDD-cost:   10
c ---[2332]---> BDD-cost:   10
c ---[2331]---> BDD-cost:   10
c ---[2330]---> BDD-cost:   10
c ---[2329]---> BDD-cost:   10
c ---[2328]---> BDD-cost:   10
c ---[2327]---> BDD-cost:   10
c ---[2326]---> BDD-cost:   10
c ---[2325]---> BDD-cost:   10
c ---[2324]---> BDD-cost:   10
c ---[2323]---> BDD-cost:   10
c ---[2322]---> BDD-cost:   10
c ---[2321]---> BDD-cost:   10
c ---[2320]---> BDD-cost:   10
c ---[2319]---> BDD-cost:   10
c ---[2318]---> BDD-cost:   10
c ---[2317]---> BDD-cost:   10
c ---[2316]---> BDD-cost:   10
c ---[2315]---> BDD-cost:   10
c ---[2314]---> BDD-cost:   10
c ---[2313]---> BDD-cost:   10
c ---[2312]---> BDD-cost:   10
c ---[2311]---> BDD-cost:   10
c ---[2310]---> BDD-cost:   10
c ---[2309]---> BDD-cost:   10
c ---[2308]---> BDD-cost:   10
c ---[2307]---> BDD-cost:   10
c ---[2306]---> BDD-cost:   10
c ---[2305]---> BDD-cost:   10
c ---[2304]---> BDD-cost:   10
c ---[2303]---> BDD-cost:   10
c ---[2302]---> BDD-cost:   10
c ---[2301]---> BDD-cost:   10
c ---[2300]---> BDD-cost:   10
c ---[2299]---> BDD-cost:   10
c ---[2298]---> BDD-cost:   10
c ---[2297]---> BDD-cost:   10
c ---[2296]---> BDD-cost:   10
c ---[2295]---> BDD-cost:   10
c ---[2294]---> BDD-cost:   10
c ---[2293]---> BDD-cost:   10
c ---[2292]---> BDD-cost:   10
c ---[2291]---> BDD-cost:   10
c ---[2290]---> BDD-cost:   10
c ---[2289]---> BDD-cost:   10
c ---[2288]---> BDD-cost:   10
c ---[2287]---> BDD-cost:   10
c ---[2286]---> BDD-cost:   10
c ---[2285]---> BDD-cost:   10
c ---[2284]---> BDD-cost:   10
c ---[2283]---> BDD-cost:   10
c ---[2278]---> BDD-cost:   10
c ---[2277]---> BDD-cost:   10
c ---[2276]---> BDD-cost:   10
c ---[2275]---> BDD-cost:   10
c ---[2274]---> BDD-cost:   10
c ---[2273]---> BDD-cost:   10
c ---[2272]---> BDD-cost:   10
c ---[2271]---> BDD-cost:   10
c ---[2270]---> BDD-cost:   10
c ---[2269]---> BDD-cost:   10
c ---[2268]---> BDD-cost:   10
c ---[2267]---> BDD-cost:   10
c ---[2266]---> BDD-cost:   10
c ---[2265]---> BDD-cost:   10
c ---[2264]---> BDD-cost:   10
c ---[2263]---> BDD-cost:   10
c ---[2262]---> BDD-cost:   10
c ---[2261]---> BDD-cost:   10
c ---[2260]---> BDD-cost:   10
c ---[2259]---> BDD-cost:   10
c ---[2258]---> BDD-cost:   10
c ---[2257]---> BDD-cost:   10
c ---[2256]---> BDD-cost:   10
c ---[2255]---> BDD-cost:   10
c ---[2254]---> BDD-cost:   10
c ---[2253]---> BDD-cost:   10
c ---[2252]---> BDD-cost:   10
c ---[2251]---> BDD-cost:   10
c ---[2250]---> BDD-cost:   10
c ---[2249]---> BDD-cost:   10
c ---[2248]---> BDD-cost:   10
c ---[2247]---> BDD-cost:   10
c ---[2246]---> BDD-cost:   10
c ---[2245]---> BDD-cost:   10
c ---[2244]---> BDD-cost:   10
c ---[2243]---> BDD-cost:   10
c ---[2242]---> BDD-cost:   10
c ---[2241]---> BDD-cost:   10
c ---[2240]---> BDD-cost:   10
c ---[2239]---> BDD-cost:   10
c ---[2238]---> BDD-cost:   10
c ---[2237]---> BDD-cost:   10
c ---[2236]---> BDD-cost:   10
c ---[2235]---> BDD-cost:   10
c ---[2234]---> BDD-cost:   10
c ---[2233]---> BDD-cost:   10
c ---[2232]---> BDD-cost:   10
c ---[2231]---> BDD-cost:   10
c ---[2230]---> BDD-cost:   10
c ---[2229]---> BDD-cost:   10
c ---[2228]---> BDD-cost:   10
c ---[2227]---> BDD-cost:   10
c ---[2226]---> BDD-cost:   10
c ---[2225]---> BDD-cost:   10
c ---[2224]---> BDD-cost:   10
c ---[2223]---> BDD-cost:   10
c ---[2222]---> BDD-cost:   10
c ---[2221]---> BDD-cost:   10
c ---[2220]---> BDD-cost:   10
c ---[2219]---> BDD-cost:   10
c ---[2218]---> BDD-cost:   10
c ---[2217]---> BDD-cost:   10
c ---[2216]---> BDD-cost:   10
c ---[2215]---> BDD-cost:   10
c ---[2214]---> BDD-cost:   10
c ---[2213]---> BDD-cost:   10
c ---[2212]---> BDD-cost:   10
c ---[2211]---> BDD-cost:   10
c ---[2210]---> BDD-cost:   10
c ---[2209]---> BDD-cost:   10
c ---[2208]---> BDD-cost:   10
c ---[2207]---> BDD-cost:   10
c ---[2206]---> BDD-cost:   10
c ---[2205]---> BDD-cost:   10
c ---[2204]---> BDD-cost:   10
c ---[2203]---> BDD-cost:   10
c ---[2202]---> BDD-cost:   10
c ---[2201]---> BDD-cost:   10
c ---[2200]---> BDD-cost:   10
c ---[2199]---> BDD-cost:   10
c ---[2198]---> BDD-cost:   10
c ---[2197]---> BDD-cost:   10
c ---[2192]---> BDD-cost:   10
c ---[2191]---> BDD-cost:   10
c ---[2190]---> BDD-cost:   10
c ---[2189]---> BDD-cost:   10
c ---[2188]---> BDD-cost:   10
c ---[2187]---> BDD-cost:   10
c ---[2186]---> BDD-cost:   10
c ---[2185]---> BDD-cost:   10
c ---[2184]---> BDD-cost:   10
c ---[2183]---> BDD-cost:   10
c ---[2182]---> BDD-cost:   10
c ---[2181]---> BDD-cost:   10
c ---[2180]---> BDD-cost:   10
c ---[2179]---> BDD-cost:   10
c ---[2178]---> BDD-cost:   10
c ---[2177]---> BDD-cost:   10
c ---[2176]---> BDD-cost:   10
c ---[2175]---> BDD-cost:   10
c ---[2174]---> BDD-cost:   10
c ---[2173]---> BDD-cost:   10
c ---[2172]---> BDD-cost:   10
c ---[2171]---> BDD-cost:   10
c ---[2170]---> BDD-cost:   10
c ---[2169]---> BDD-cost:   10
c ---[2168]---> BDD-cost:   10
c ---[2167]---> BDD-cost:   10
c ---[2166]---> BDD-cost:   10
c ---[2165]---> BDD-cost:   10
c ---[2164]---> BDD-cost:   10
c ---[2163]---> BDD-cost:   10
c ---[2162]---> BDD-cost:   10
c ---[2161]---> BDD-cost:   10
c ---[2160]---> BDD-cost:   10
c ---[2159]---> BDD-cost:   10
c ---[2158]---> BDD-cost:   10
c ---[2157]---> BDD-cost:   10
c ---[2156]---> BDD-cost:   10
c ---[2155]---> BDD-cost:   10
c ---[2154]---> BDD-cost:   10
c ---[2153]---> BDD-cost:   10
c ---[2152]---> BDD-cost:   10
c ---[2151]---> BDD-cost:   10
c ---[2150]---> BDD-cost:   10
c ---[2149]---> BDD-cost:   10
c ---[2148]---> BDD-cost:   10
c ---[2147]---> BDD-cost:   10
c ---[2146]---> BDD-cost:   10
c ---[2145]---> BDD-cost:   10
c ---[2144]---> BDD-cost:   10
c ---[2143]---> BDD-cost:   10
c ---[2142]---> BDD-cost:   10
c ---[2141]---> BDD-cost:   10
c ---[2140]---> BDD-cost:   10
c ---[2139]---> BDD-cost:   10
c ---[2138]---> BDD-cost:   10
c ---[2137]---> BDD-cost:   10
c ---[2136]---> BDD-cost:   10
c ---[2135]---> BDD-cost:   10
c ---[2134]---> BDD-cost:   10
c ---[2133]---> BDD-cost:   10
c ---[2132]---> BDD-cost:   10
c ---[2131]---> BDD-cost:   10
c ---[2130]---> BDD-cost:   10
c ---[2129]---> BDD-cost:   10
c ---[2128]---> BDD-cost:   10
c ---[2127]---> BDD-cost:   10
c ---[2126]---> BDD-cost:   10
c ---[2125]---> BDD-cost:   10
c ---[2124]---> BDD-cost:   10
c ---[2123]---> BDD-cost:   10
c ---[2122]---> BDD-cost:   10
c ---[2121]---> BDD-cost:   10
c ---[2120]---> BDD-cost:   10
c ---[2119]---> BDD-cost:   10
c ---[2118]---> BDD-cost:   10
c ---[2117]---> BDD-cost:   10
c ---[2116]---> BDD-cost:   10
c ---[2115]---> BDD-cost:   10
c ---[2110]---> BDD-cost:   10
c ---[2109]---> BDD-cost:   10
c ---[2108]---> BDD-cost:   10
c ---[2107]---> BDD-cost:   10
c ---[2106]---> BDD-cost:   10
c ---[2105]---> BDD-cost:   10
c ---[2104]---> BDD-cost:   10
c ---[2103]---> BDD-cost:   10
c ---[2102]---> BDD-cost:   10
c ---[2101]---> BDD-cost:   10
c ---[2100]---> BDD-cost:   10
c ---[2099]---> BDD-cost:   10
c ---[2098]---> BDD-cost:   10
c ---[2097]---> BDD-cost:   10
c ---[2096]---> BDD-cost:   10
c ---[2095]---> BDD-cost:   10
c ---[2094]---> BDD-cost:   10
c ---[2093]---> BDD-cost:   10
c ---[2092]---> BDD-cost:   10
c ---[2091]---> BDD-cost:   10
c ---[2090]---> BDD-cost:   10
c ---[2089]---> BDD-cost:   10
c ---[2088]---> BDD-cost:   10
c ---[2087]---> BDD-cost:   10
c ---[2086]---> BDD-cost:   10
c ---[2085]---> BDD-cost:   10
c ---[2084]---> BDD-cost:   10
c ---[2083]---> BDD-cost:   10
c ---[2082]---> BDD-cost:   10
c ---[2081]---> BDD-cost:   10
c ---[2080]---> BDD-cost:   10
c ---[2079]---> BDD-cost:   10
c ---[2078]---> BDD-cost:   10
c ---[2077]---> BDD-cost:   10
c ---[2076]---> BDD-cost:   10
c ---[2075]---> BDD-cost:   10
c ---[2074]---> BDD-cost:   10
c ---[2073]---> BDD-cost:   10
c ---[2072]---> BDD-cost:   10
c ---[2071]---> BDD-cost:   10
c ---[2070]---> BDD-cost:   10
c ---[2069]---> BDD-cost:   10
c ---[2068]---> BDD-cost:   10
c ---[2067]---> BDD-cost:   10
c ---[2066]---> BDD-cost:   10
c ---[2065]---> BDD-cost:   10
c ---[2064]---> BDD-cost:   10
c ---[2063]---> BDD-cost:   10
c ---[2062]---> BDD-cost:   10
c ---[2061]---> BDD-cost:   10
c ---[2060]---> BDD-cost:   10
c ---[2059]---> BDD-cost:   10
c ---[2058]---> BDD-cost:   10
c ---[2057]---> BDD-cost:   10
c ---[2056]---> BDD-cost:   10
c ---[2055]---> BDD-cost:   10
c ---[2054]---> BDD-cost:   10
c ---[2053]---> BDD-cost:   10
c ---[2052]---> BDD-cost:   10
c ---[2051]---> BDD-cost:   10
c ---[2050]---> BDD-cost:   10
c ---[2049]---> BDD-cost:   10
c ---[2048]---> BDD-cost:   10
c ---[2047]---> BDD-cost:   10
c ---[2046]---> BDD-cost:   10
c ---[2045]---> BDD-cost:   10
c ---[2044]---> BDD-cost:   10
c ---[2043]---> BDD-cost:   10
c ---[2042]---> BDD-cost:   10
c ---[2041]---> BDD-cost:   10
c ---[2040]---> BDD-cost:   10
c ---[2039]---> BDD-cost:   10
c ---[2038]---> BDD-cost:   10
c ---[2037]---> BDD-cost:   10
c ---[2036]---> BDD-cost:   10
c ---[2035]---> BDD-cost:   10
c ---[2034]---> BDD-cost:   10
c ---[2033]---> BDD-cost:   10
c ---[2028]---> BDD-cost:   10
c ---[2027]---> BDD-cost:   10
c ---[2026]---> BDD-cost:   10
c ---[2025]---> BDD-cost:   10
c ---[2024]---> BDD-cost:   10
c ---[2023]---> BDD-cost:   10
c ---[2022]---> BDD-cost:   10
c ---[2021]---> BDD-cost:   10
c ---[2020]---> BDD-cost:   10
c ---[2019]---> BDD-cost:   10
c ---[2018]---> BDD-cost:   10
c ---[2017]---> BDD-cost:   10
c ---[2016]---> BDD-cost:   10
c ---[2015]---> BDD-cost:   10
c ---[2014]---> BDD-cost:   10
c ---[2013]---> BDD-cost:   10
c ---[2012]---> BDD-cost:   10
c ---[2011]---> BDD-cost:   10
c ---[2010]---> BDD-cost:   10
c ---[2009]---> BDD-cost:   10
c ---[2008]---> BDD-cost:   10
c ---[2007]---> BDD-cost:   10
c ---[2006]---> BDD-cost:   10
c ---[2005]---> BDD-cost:   10
c ---[2004]---> BDD-cost:   10
c ---[2003]---> BDD-cost:   10
c ---[2002]---> BDD-cost:   10
c ---[2001]---> BDD-cost:   10
c ---[2000]---> BDD-cost:   10
c ---[1999]---> BDD-cost:   10
c ---[1998]---> BDD-cost:   10
c ---[1997]---> BDD-cost:   10
c ---[1996]---> BDD-cost:   10
c ---[1995]---> BDD-cost:   10
c ---[1994]---> BDD-cost:   10
c ---[1993]---> BDD-cost:   10
c ---[1992]---> BDD-cost:   10
c ---[1991]---> BDD-cost:   10
c ---[1990]---> BDD-cost:   10
c ---[1989]---> BDD-cost:   10
c ---[1988]---> BDD-cost:   10
c ---[1987]---> BDD-cost:   10
c ---[1986]---> BDD-cost:   10
c ---[1985]---> BDD-cost:   10
c ---[1984]---> BDD-cost:   10
c ---[1983]---> BDD-cost:   10
c ---[1982]---> BDD-cost:   10
c ---[1981]---> BDD-cost:   10
c ---[1980]---> BDD-cost:   10
c ---[1979]---> BDD-cost:   10
c ---[1978]---> BDD-cost:   10
c ---[1977]---> BDD-cost:   10
c ---[1976]---> BDD-cost:   10
c ---[1975]---> BDD-cost:   10
c ---[1974]---> BDD-cost:   10
c ---[1973]---> BDD-cost:   10
c ---[1972]---> BDD-cost:   10
c ---[1971]---> BDD-cost:   10
c ---[1970]---> BDD-cost:   10
c ---[1969]---> BDD-cost:   10
c ---[1968]---> BDD-cost:   10
c ---[1967]---> BDD-cost:   10
c ---[1966]---> BDD-cost:   10
c ---[1965]---> BDD-cost:   10
c ---[1964]---> BDD-cost:   10
c ---[1963]---> BDD-cost:   10
c ---[1962]---> BDD-cost:   10
c ---[1961]---> BDD-cost:   10
c ---[1960]---> BDD-cost:   10
c ---[1959]---> BDD-cost:   10
c ---[1958]---> BDD-cost:   10
c ---[1957]---> BDD-cost:   10
c ---[1956]---> BDD-cost:   10
c ---[1955]---> BDD-cost:   10
c ---[1954]---> BDD-cost:   10
c ---[1953]---> BDD-cost:   10
c ---[1952]---> BDD-cost:   10
c ---[1951]---> BDD-cost:   10
c ---[1946]---> BDD-cost:   10
c ---[1945]---> BDD-cost:   10
c ---[1944]---> BDD-cost:   10
c ---[1943]---> BDD-cost:   10
c ---[1942]---> BDD-cost:   10
c ---[1941]---> BDD-cost:   10
c ---[1940]---> BDD-cost:   10
c ---[1939]---> BDD-cost:   10
c ---[1938]---> BDD-cost:   10
c ---[1937]---> BDD-cost:   10
c ---[1936]---> BDD-cost:   10
c ---[1935]---> BDD-cost:   10
c ---[1934]---> BDD-cost:   10
c ---[1933]---> BDD-cost:   10
c ---[1932]---> BDD-cost:   10
c ---[1931]---> BDD-cost:   10
c ---[1930]---> BDD-cost:   10
c ---[1929]---> BDD-cost:   10
c ---[1928]---> BDD-cost:   10
c ---[1927]---> BDD-cost:   10
c ---[1926]---> BDD-cost:   10
c ---[1925]---> BDD-cost:   10
c ---[1924]---> BDD-cost:   10
c ---[1923]---> BDD-cost:   10
c ---[1922]---> BDD-cost:   10
c ---[1921]---> BDD-cost:   10
c ---[1920]---> BDD-cost:   10
c ---[1919]---> BDD-cost:   10
c ---[1918]---> BDD-cost:   10
c ---[1917]---> BDD-cost:   10
c ---[1916]---> BDD-cost:   10
c ---[1915]---> BDD-cost:   10
c ---[1914]---> BDD-cost:   10
c ---[1913]---> BDD-cost:   10
c ---[1912]---> BDD-cost:   10
c ---[1911]---> BDD-cost:   10
c ---[1910]---> BDD-cost:   10
c ---[1909]---> BDD-cost:   10
c ---[1908]---> BDD-cost:   10
c ---[1907]---> BDD-cost:   10
c ---[1906]---> BDD-cost:   10
c ---[1905]---> BDD-cost:   10
c ---[1904]---> BDD-cost:   10
c ---[1903]---> BDD-cost:   10
c ---[1902]---> BDD-cost:   10
c ---[1901]---> BDD-cost:   10
c ---[1900]---> BDD-cost:   10
c ---[1899]---> BDD-cost:   10
c ---[1898]---> BDD-cost:   10
c ---[1897]---> BDD-cost:   10
c ---[1896]---> BDD-cost:   10
c ---[1895]---> BDD-cost:   10
c ---[1894]---> BDD-cost:   10
c ---[1893]---> BDD-cost:   10
c ---[1892]---> BDD-cost:   10
c ---[1891]---> BDD-cost:   10
c ---[1890]---> BDD-cost:   10
c ---[1889]---> BDD-cost:   10
c ---[1888]---> BDD-cost:   10
c ---[1887]---> BDD-cost:   10
c ---[1886]---> BDD-cost:   10
c ---[1885]---> BDD-cost:   10
c ---[1884]---> BDD-cost:   10
c ---[1883]---> BDD-cost:   10
c ---[1882]---> BDD-cost:   10
c ---[1881]---> BDD-cost:   10
c ---[1880]---> BDD-cost:   10
c ---[1879]---> BDD-cost:   10
c ---[1878]---> BDD-cost:   10
c ---[1877]---> BDD-cost:   10
c ---[1876]---> BDD-cost:   10
c ---[1875]---> BDD-cost:   10
c ---[1874]---> BDD-cost:   10
c ---[1873]---> BDD-cost:   10
c ---[1872]---> BDD-cost:   10
c ---[1871]---> BDD-cost:   10
c ---[1870]---> BDD-cost:   10
c ---[1869]---> BDD-cost:   10
c ---[1868]---> BDD-cost:   10
c ---[1867]---> BDD-cost:   10
c ---[1866]---> BDD-cost:   10
c ---[1865]---> BDD-cost:   10
c ---[1860]---> BDD-cost:   10
c ---[1859]---> BDD-cost:   10
c ---[1858]---> BDD-cost:   10
c ---[1857]---> BDD-cost:   10
c ---[1856]---> BDD-cost:   10
c ---[1855]---> BDD-cost:   10
c ---[1854]---> BDD-cost:   10
c ---[1853]---> BDD-cost:   10
c ---[1852]---> BDD-cost:   10
c ---[1851]---> BDD-cost:   10
c ---[1850]---> BDD-cost:   10
c ---[1849]---> BDD-cost:   10
c ---[1848]---> BDD-cost:   10
c ---[1847]---> BDD-cost:   10
c ---[1846]---> BDD-cost:   10
c ---[1845]---> BDD-cost:   10
c ---[1844]---> BDD-cost:   10
c ---[1843]---> BDD-cost:   10
c ---[1842]---> BDD-cost:   10
c ---[1841]---> BDD-cost:   10
c ---[1840]---> BDD-cost:   10
c ---[1839]---> BDD-cost:   10
c ---[1838]---> BDD-cost:   10
c ---[1837]---> BDD-cost:   10
c ---[1836]---> BDD-cost:   10
c ---[1835]---> BDD-cost:   10
c ---[1834]---> BDD-cost:   10
c ---[1833]---> BDD-cost:   10
c ---[1832]---> BDD-cost:   10
c ---[1831]---> BDD-cost:   10
c ---[1830]---> BDD-cost:   10
c ---[1829]---> BDD-cost:   10
c ---[1828]---> BDD-cost:   10
c ---[1827]---> BDD-cost:   10
c ---[1826]---> BDD-cost:   10
c ---[1825]---> BDD-cost:   10
c ---[1824]---> BDD-cost:   10
c ---[1823]---> BDD-cost:   10
c ---[1822]---> BDD-cost:   10
c ---[1821]---> BDD-cost:   10
c ---[1820]---> BDD-cost:   10
c ---[1819]---> BDD-cost:   10
c ---[1818]---> BDD-cost:   10
c ---[1817]---> BDD-cost:   10
c ---[1816]---> BDD-cost:   10
c ---[1815]---> BDD-cost:   10
c ---[1814]---> BDD-cost:   10
c ---[1813]---> BDD-cost:   10
c ---[1812]---> BDD-cost:   10
c ---[1811]---> BDD-cost:   10
c ---[1810]---> BDD-cost:   10
c ---[1809]---> BDD-cost:   10
c ---[1808]---> BDD-cost:   10
c ---[1807]---> BDD-cost:   10
c ---[1806]---> BDD-cost:   10
c ---[1805]---> BDD-cost:   10
c ---[1804]---> BDD-cost:   10
c ---[1803]---> BDD-cost:   10
c ---[1802]---> BDD-cost:   10
c ---[1801]---> BDD-cost:   10
c ---[1800]---> BDD-cost:   10
c ---[1799]---> BDD-cost:   10
c ---[1798]---> BDD-cost:   10
c ---[1797]---> BDD-cost:   10
c ---[1796]---> BDD-cost:   10
c ---[1795]---> BDD-cost:   10
c ---[1794]---> BDD-cost:   10
c ---[1793]---> BDD-cost:   10
c ---[1792]---> BDD-cost:   10
c ---[1791]---> BDD-cost:   10
c ---[1790]---> BDD-cost:   10
c ---[1789]---> BDD-cost:   10
c ---[1788]---> BDD-cost:   10
c ---[1787]---> BDD-cost:   10
c ---[1786]---> BDD-cost:   10
c ---[1785]---> BDD-cost:   10
c ---[1784]---> BDD-cost:   10
c ---[1783]---> BDD-cost:   10
c ---[1778]---> BDD-cost:   10
c ---[1777]---> BDD-cost:   10
c ---[1776]---> BDD-cost:   10
c ---[1775]---> BDD-cost:   10
c ---[1774]---> BDD-cost:   10
c ---[1773]---> BDD-cost:   10
c ---[1772]---> BDD-cost:   10
c ---[1771]---> BDD-cost:   10
c ---[1770]---> BDD-cost:   10
c ---[1769]---> BDD-cost:   10
c ---[1768]---> BDD-cost:   10
c ---[1767]---> BDD-cost:   10
c ---[1766]---> BDD-cost:   10
c ---[1765]---> BDD-cost:   10
c ---[1764]---> BDD-cost:   10
c ---[1763]---> BDD-cost:   10
c ---[1762]---> BDD-cost:   10
c ---[1761]---> BDD-cost:   10
c ---[1760]---> BDD-cost:   10
c ---[1759]---> BDD-cost:   10
c ---[1758]---> BDD-cost:   10
c ---[1757]---> BDD-cost:   10
c ---[1756]---> BDD-cost:   10
c ---[1755]---> BDD-cost:   10
c ---[1754]---> BDD-cost:   10
c ---[1753]---> BDD-cost:   10
c ---[1752]---> BDD-cost:   10
c ---[1751]---> BDD-cost:   10
c ---[1750]---> BDD-cost:   10
c ---[1749]---> BDD-cost:   10
c ---[1748]---> BDD-cost:   10
c ---[1747]---> BDD-cost:   10
c ---[1746]---> BDD-cost:   10
c ---[1745]---> BDD-cost:   10
c ---[1744]---> BDD-cost:   10
c ---[1743]---> BDD-cost:   10
c ---[1742]---> BDD-cost:   10
c ---[1741]---> BDD-cost:   10
c ---[1740]---> BDD-cost:   10
c ---[1739]---> BDD-cost:   10
c ---[1738]---> BDD-cost:   10
c ---[1737]---> BDD-cost:   10
c ---[1736]---> BDD-cost:   10
c ---[1735]---> BDD-cost:   10
c ---[1734]---> BDD-cost:   10
c ---[1733]---> BDD-cost:   10
c ---[1732]---> BDD-cost:   10
c ---[1731]---> BDD-cost:   10
c ---[1730]---> BDD-cost:   10
c ---[1729]---> BDD-cost:   10
c ---[1728]---> BDD-cost:   10
c ---[1727]---> BDD-cost:   10
c ---[1726]---> BDD-cost:   10
c ---[1725]---> BDD-cost:   10
c ---[1724]---> BDD-cost:   10
c ---[1723]---> BDD-cost:   10
c ---[1722]---> BDD-cost:   10
c ---[1721]---> BDD-cost:   10
c ---[1720]---> BDD-cost:   10
c ---[1719]---> BDD-cost:   10
c ---[1718]---> BDD-cost:   10
c ---[1717]---> BDD-cost:   10
c ---[1716]---> BDD-cost:   10
c ---[1715]---> BDD-cost:   10
c ---[1714]---> BDD-cost:   10
c ---[1713]---> BDD-cost:   10
c ---[1712]---> BDD-cost:   10
c ---[1711]---> BDD-cost:   10
c ---[1710]---> BDD-cost:   10
c ---[1709]---> BDD-cost:   10
c ---[1708]---> BDD-cost:   10
c ---[1707]---> BDD-cost:   10
c ---[1706]---> BDD-cost:   10
c ---[1705]---> BDD-cost:   10
c ---[1704]---> BDD-cost:   10
c ---[1703]---> BDD-cost:   10
c ---[1702]---> BDD-cost:   10
c ---[1701]---> BDD-cost:   10
c ---[1696]---> BDD-cost:   10
c ---[1695]---> BDD-cost:   10
c ---[1694]---> BDD-cost:   10
c ---[1693]---> BDD-cost:   10
c ---[1692]---> BDD-cost:   10
c ---[1691]---> BDD-cost:   10
c ---[1690]---> BDD-cost:   10
c ---[1689]---> BDD-cost:   10
c ---[1688]---> BDD-cost:   10
c ---[1687]---> BDD-cost:   10
c ---[1686]---> BDD-cost:   10
c ---[1685]---> BDD-cost:   10
c ---[1684]---> BDD-cost:   10
c ---[1683]---> BDD-cost:   10
c ---[1682]---> BDD-cost:   10
c ---[1681]---> BDD-cost:   10
c ---[1680]---> BDD-cost:   10
c ---[1679]---> BDD-cost:   10
c ---[1678]---> BDD-cost:   10
c ---[1677]---> BDD-cost:   10
c ---[1676]---> BDD-cost:   10
c ---[1675]---> BDD-cost:   10
c ---[1674]---> BDD-cost:   10
c ---[1673]---> BDD-cost:   10
c ---[1672]---> BDD-cost:   10
c ---[1671]---> BDD-cost:   10
c ---[1670]---> BDD-cost:   10
c ---[1669]---> BDD-cost:   10
c ---[1668]---> BDD-cost:   10
c ---[1667]---> BDD-cost:   10
c ---[1666]---> BDD-cost:   10
c ---[1665]---> BDD-cost:   10
c ---[1664]---> BDD-cost:   10
c ---[1663]---> BDD-cost:   10
c ---[1662]---> BDD-cost:   10
c ---[1661]---> BDD-cost:   10
c ---[1660]---> BDD-cost:   10
c ---[1659]---> BDD-cost:   10
c ---[1658]---> BDD-cost:   10
c ---[1657]---> BDD-cost:   10
c ---[1656]---> BDD-cost:   10
c ---[1655]---> BDD-cost:   10
c ---[1654]---> BDD-cost:   10
c ---[1653]---> BDD-cost:   10
c ---[1652]---> BDD-cost:   10
c ---[1651]---> BDD-cost:   10
c ---[1650]---> BDD-cost:   10
c ---[1649]---> BDD-cost:   10
c ---[1648]---> BDD-cost:   10
c ---[1647]---> BDD-cost:   10
c ---[1646]---> BDD-cost:   10
c ---[1645]---> BDD-cost:   10
c ---[1644]---> BDD-cost:   10
c ---[1643]---> BDD-cost:   10
c ---[1642]---> BDD-cost:   10
c ---[1641]---> BDD-cost:   10
c ---[1640]---> BDD-cost:   10
c ---[1639]---> BDD-cost:   10
c ---[1638]---> BDD-cost:   10
c ---[1637]---> BDD-cost:   10
c ---[1636]---> BDD-cost:   10
c ---[1635]---> BDD-cost:   10
c ---[1634]---> BDD-cost:   10
c ---[1633]---> BDD-cost:   10
c ---[1632]---> BDD-cost:   10
c ---[1631]---> BDD-cost:   10
c ---[1630]---> BDD-cost:   10
c ---[1629]---> BDD-cost:   10
c ---[1628]---> BDD-cost:   10
c ---[1627]---> BDD-cost:   10
c ---[1626]---> BDD-cost:   10
c ---[1625]---> BDD-cost:   10
c ---[1624]---> BDD-cost:   10
c ---[1623]---> BDD-cost:   10
c ---[1622]---> BDD-cost:   10
c ---[1621]---> BDD-cost:   10
c ---[1620]---> BDD-cost:   10
c ---[1619]---> BDD-cost:   10
c ---[1614]---> BDD-cost:   10
c ---[1613]---> BDD-cost:   10
c ---[1612]---> BDD-cost:   10
c ---[1611]---> BDD-cost:   10
c ---[1610]---> BDD-cost:   10
c ---[1609]---> BDD-cost:   10
c ---[1608]---> BDD-cost:   10
c ---[1607]---> BDD-cost:   10
c ---[1606]---> BDD-cost:   10
c ---[1605]---> BDD-cost:   10
c ---[1604]---> BDD-cost:   10
c ---[1603]---> BDD-cost:   10
c ---[1602]---> BDD-cost:   10
c ---[1601]---> BDD-cost:   10
c ---[1600]---> BDD-cost:   10
c ---[1599]---> BDD-cost:   10
c ---[1598]---> BDD-cost:   10
c ---[1597]---> BDD-cost:   10
c ---[1596]---> BDD-cost:   10
c ---[1595]---> BDD-cost:   10
c ---[1594]---> BDD-cost:   10
c ---[1593]---> BDD-cost:   10
c ---[1592]---> BDD-cost:   10
c ---[1591]---> BDD-cost:   10
c ---[1590]---> BDD-cost:   10
c ---[1589]---> BDD-cost:   10
c ---[1588]---> BDD-cost:   10
c ---[1587]---> BDD-cost:   10
c ---[1586]---> BDD-cost:   10
c ---[1585]---> BDD-cost:   10
c ---[1584]---> BDD-cost:   10
c ---[1583]---> BDD-cost:   10
c ---[1582]---> BDD-cost:   10
c ---[1581]---> BDD-cost:   10
c ---[1580]---> BDD-cost:   10
c ---[1579]---> BDD-cost:   10
c ---[1578]---> BDD-cost:   10
c ---[1577]---> BDD-cost:   10
c ---[1576]---> BDD-cost:   10
c ---[1575]---> BDD-cost:   10
c ---[1574]---> BDD-cost:   10
c ---[1573]---> BDD-cost:   10
c ---[1572]---> BDD-cost:   10
c ---[1571]---> BDD-cost:   10
c ---[1570]---> BDD-cost:   10
c ---[1569]---> BDD-cost:   10
c ---[1568]---> BDD-cost:   10
c ---[1567]---> BDD-cost:   10
c ---[1566]---> BDD-cost:   10
c ---[1565]---> BDD-cost:   10
c ---[1564]---> BDD-cost:   10
c ---[1563]---> BDD-cost:   10
c ---[1562]---> BDD-cost:   10
c ---[1561]---> BDD-cost:   10
c ---[1560]---> BDD-cost:   10
c ---[1559]---> BDD-cost:   10
c ---[1558]---> BDD-cost:   10
c ---[1557]---> BDD-cost:   10
c ---[1556]---> BDD-cost:   10
c ---[1555]---> BDD-cost:   10
c ---[1554]---> BDD-cost:   10
c ---[1553]---> BDD-cost:   10
c ---[1552]---> BDD-cost:   10
c ---[1551]---> BDD-cost:   10
c ---[1550]---> BDD-cost:   10
c ---[1549]---> BDD-cost:   10
c ---[1548]---> BDD-cost:   10
c ---[1547]---> BDD-cost:   10
c ---[1546]---> BDD-cost:   10
c ---[1545]---> BDD-cost:   10
c ---[1544]---> BDD-cost:   10
c ---[1543]---> BDD-cost:   10
c ---[1542]---> BDD-cost:   10
c ---[1541]---> BDD-cost:   10
c ---[1540]---> BDD-cost:   10
c ---[1539]---> BDD-cost:   10
c ---[1538]---> BDD-cost:   10
c ---[1537]---> BDD-cost:   10
c ---[1536]---> BDD-cost:   10
c ---[1535]---> BDD-cost:   10
c ---[1534]---> BDD-cost:   10
c ---[1533]---> BDD-cost:   10
c ---[1528]---> BDD-cost:   10
c ---[1527]---> BDD-cost:   10
c ---[1526]---> BDD-cost:   10
c ---[1525]---> BDD-cost:   10
c ---[1524]---> BDD-cost:   10
c ---[1523]---> BDD-cost:   10
c ---[1522]---> BDD-cost:   10
c ---[1521]---> BDD-cost:   10
c ---[1520]---> BDD-cost:   10
c ---[1519]---> BDD-cost:   10
c ---[1518]---> BDD-cost:   10
c ---[1517]---> BDD-cost:   10
c ---[1516]---> BDD-cost:   10
c ---[1515]---> BDD-cost:   10
c ---[1514]---> BDD-cost:   10
c ---[1513]---> BDD-cost:   10
c ---[1512]---> BDD-cost:   10
c ---[1511]---> BDD-cost:   10
c ---[1510]---> BDD-cost:   10
c ---[1509]---> BDD-cost:   10
c ---[1508]---> BDD-cost:   10
c ---[1507]---> BDD-cost:   10
c ---[1506]---> BDD-cost:   10
c ---[1505]---> BDD-cost:   10
c ---[1504]---> BDD-cost:   10
c ---[1503]---> BDD-cost:   10
c ---[1502]---> BDD-cost:   10
c ---[1501]---> BDD-cost:   10
c ---[1500]---> BDD-cost:   10
c ---[1499]---> BDD-cost:   10
c ---[1498]---> BDD-cost:   10
c ---[1497]---> BDD-cost:   10
c ---[1496]---> BDD-cost:   10
c ---[1495]---> BDD-cost:   10
c ---[1494]---> BDD-cost:   10
c ---[1493]---> BDD-cost:   10
c ---[1492]---> BDD-cost:   10
c ---[1491]---> BDD-cost:   10
c ---[1490]---> BDD-cost:   10
c ---[1489]---> BDD-cost:   10
c ---[1488]---> BDD-cost:   10
c ---[1487]---> BDD-cost:   10
c ---[1486]---> BDD-cost:   10
c ---[1485]---> BDD-cost:   10
c ---[1484]---> BDD-cost:   10
c ---[1483]---> BDD-cost:   10
c ---[1482]---> BDD-cost:   10
c ---[1481]---> BDD-cost:   10
c ---[1480]---> BDD-cost:   10
c ---[1479]---> BDD-cost:   10
c ---[1478]---> BDD-cost:   10
c ---[1477]---> BDD-cost:   10
c ---[1476]---> BDD-cost:   10
c ---[1475]---> BDD-cost:   10
c ---[1474]---> BDD-cost:   10
c ---[1473]---> BDD-cost:   10
c ---[1472]---> BDD-cost:   10
c ---[1471]---> BDD-cost:   10
c ---[1470]---> BDD-cost:   10
c ---[1469]---> BDD-cost:   10
c ---[1468]---> BDD-cost:   10
c ---[1467]---> BDD-cost:   10
c ---[1466]---> BDD-cost:   10
c ---[1465]---> BDD-cost:   10
c ---[1464]---> BDD-cost:   10
c ---[1463]---> BDD-cost:   10
c ---[1462]---> BDD-cost:   10
c ---[1461]---> BDD-cost:   10
c ---[1460]---> BDD-cost:   10
c ---[1459]---> BDD-cost:   10
c ---[1458]---> BDD-cost:   10
c ---[1457]---> BDD-cost:   10
c ---[1456]---> BDD-cost:   10
c ---[1455]---> BDD-cost:   10
c ---[1454]---> BDD-cost:   10
c ---[1453]---> BDD-cost:   10
c ---[1452]---> BDD-cost:   10
c ---[1451]---> BDD-cost:   10
c ---[1446]---> BDD-cost:   10
c ---[1445]---> BDD-cost:   10
c ---[1444]---> BDD-cost:   10
c ---[1443]---> BDD-cost:   10
c ---[1442]---> BDD-cost:   10
c ---[1441]---> BDD-cost:   10
c ---[1440]---> BDD-cost:   10
c ---[1439]---> BDD-cost:   10
c ---[1438]---> BDD-cost:   10
c ---[1437]---> BDD-cost:   10
c ---[1436]---> BDD-cost:   10
c ---[1435]---> BDD-cost:   10
c ---[1434]---> BDD-cost:   10
c ---[1433]---> BDD-cost:   10
c ---[1432]---> BDD-cost:   10
c ---[1431]---> BDD-cost:   10
c ---[1430]---> BDD-cost:   10
c ---[1429]---> BDD-cost:   10
c ---[1428]---> BDD-cost:   10
c ---[1427]---> BDD-cost:   10
c ---[1426]---> BDD-cost:   10
c ---[1425]---> BDD-cost:   10
c ---[1424]---> BDD-cost:   10
c ---[1423]---> BDD-cost:   10
c ---[1422]---> BDD-cost:   10
c ---[1421]---> BDD-cost:   10
c ---[1420]---> BDD-cost:   10
c ---[1419]---> BDD-cost:   10
c ---[1418]---> BDD-cost:   10
c ---[1417]---> BDD-cost:   10
c ---[1416]---> BDD-cost:   10
c ---[1415]---> BDD-cost:   10
c ---[1414]---> BDD-cost:   10
c ---[1413]---> BDD-cost:   10
c ---[1412]---> BDD-cost:   10
c ---[1411]---> BDD-cost:   10
c ---[1410]---> BDD-cost:   10
c ---[1409]---> BDD-cost:   10
c ---[1408]---> BDD-cost:   10
c ---[1407]---> BDD-cost:   10
c ---[1406]---> BDD-cost:   10
c ---[1405]---> BDD-cost:   10
c ---[1404]---> BDD-cost:   10
c ---[1403]---> BDD-cost:   10
c ---[1402]---> BDD-cost:   10
c ---[1401]---> BDD-cost:   10
c ---[1400]---> BDD-cost:   10
c ---[1399]---> BDD-cost:   10
c ---[1398]---> BDD-cost:   10
c ---[1397]---> BDD-cost:   10
c ---[1396]---> BDD-cost:   10
c ---[1395]---> BDD-cost:   10
c ---[1394]---> BDD-cost:   10
c ---[1393]---> BDD-cost:   10
c ---[1392]---> BDD-cost:   10
c ---[1391]---> BDD-cost:   10
c ---[1390]---> BDD-cost:   10
c ---[1389]---> BDD-cost:   10
c ---[1388]---> BDD-cost:   10
c ---[1387]---> BDD-cost:   10
c ---[1386]---> BDD-cost:   10
c ---[1385]---> BDD-cost:   10
c ---[1384]---> BDD-cost:   10
c ---[1383]---> BDD-cost:   10
c ---[1382]---> BDD-cost:   10
c ---[1381]---> BDD-cost:   10
c ---[1380]---> BDD-cost:   10
c ---[1379]---> BDD-cost:   10
c ---[1378]---> BDD-cost:   10
c ---[1377]---> BDD-cost:   10
c ---[1376]---> BDD-cost:   10
c ---[1375]---> BDD-cost:   10
c ---[1374]---> BDD-cost:   10
c ---[1373]---> BDD-cost:   10
c ---[1372]---> BDD-cost:   10
c ---[1371]---> BDD-cost:   10
c ---[1370]---> BDD-cost:   10
c ---[1369]---> BDD-cost:   10
c ---[1364]---> BDD-cost:   10
c ---[1363]---> BDD-cost:   10
c ---[1362]---> BDD-cost:   10
c ---[1361]---> BDD-cost:   10
c ---[1360]---> BDD-cost:   10
c ---[1359]---> BDD-cost:   10
c ---[1358]---> BDD-cost:   10
c ---[1357]---> BDD-cost:   10
c ---[1356]---> BDD-cost:   10
c ---[1355]---> BDD-cost:   10
c ---[1354]---> BDD-cost:   10
c ---[1353]---> BDD-cost:   10
c ---[1352]---> BDD-cost:   10
c ---[1351]---> BDD-cost:   10
c ---[1350]---> BDD-cost:   10
c ---[1349]---> BDD-cost:   10
c ---[1348]---> BDD-cost:   10
c ---[1347]---> BDD-cost:   10
c ---[1346]---> BDD-cost:   10
c ---[1345]---> BDD-cost:   10
c ---[1344]---> BDD-cost:   10
c ---[1343]---> BDD-cost:   10
c ---[1342]---> BDD-cost:   10
c ---[1341]---> BDD-cost:   10
c ---[1340]---> BDD-cost:   10
c ---[1339]---> BDD-cost:   10
c ---[1338]---> BDD-cost:   10
c ---[1337]---> BDD-cost:   10
c ---[1336]---> BDD-cost:   10
c ---[1335]---> BDD-cost:   10
c ---[1334]---> BDD-cost:   10
c ---[1333]---> BDD-cost:   10
c ---[1332]---> BDD-cost:   10
c ---[1331]---> BDD-cost:   10
c ---[1330]---> BDD-cost:   10
c ---[1329]---> BDD-cost:   10
c ---[1328]---> BDD-cost:   10
c ---[1327]---> BDD-cost:   10
c ---[1326]---> BDD-cost:   10
c ---[1325]---> BDD-cost:   10
c ---[1324]---> BDD-cost:   10
c ---[1323]---> BDD-cost:   10
c ---[1322]---> BDD-cost:   10
c ---[1321]---> BDD-cost:   10
c ---[1320]---> BDD-cost:   10
c ---[1319]---> BDD-cost:   10
c ---[1318]---> BDD-cost:   10
c ---[1317]---> BDD-cost:   10
c ---[1316]---> BDD-cost:   10
c ---[1315]---> BDD-cost:   10
c ---[1314]---> BDD-cost:   10
c ---[1313]---> BDD-cost:   10
c ---[1312]---> BDD-cost:   10
c ---[1311]---> BDD-cost:   10
c ---[1310]---> BDD-cost:   10
c ---[1309]---> BDD-cost:   10
c ---[1308]---> BDD-cost:   10
c ---[1307]---> BDD-cost:   10
c ---[1306]---> BDD-cost:   10
c ---[1305]---> BDD-cost:   10
c ---[1304]---> BDD-cost:   10
c ---[1303]---> BDD-cost:   10
c ---[1302]---> BDD-cost:   10
c ---[1301]---> BDD-cost:   10
c ---[1300]---> BDD-cost:   10
c ---[1299]---> BDD-cost:   10
c ---[1298]---> BDD-cost:   10
c ---[1297]---> BDD-cost:   10
c ---[1296]---> BDD-cost:   10
c ---[1295]---> BDD-cost:   10
c ---[1294]---> BDD-cost:   10
c ---[1293]---> BDD-cost:   10
c ---[1292]---> BDD-cost:   10
c ---[1291]---> BDD-cost:   10
c ---[1290]---> BDD-cost:   10
c ---[1289]---> BDD-cost:   10
c ---[1288]---> BDD-cost:   10
c ---[1287]---> BDD-cost:   10
c ---[1282]---> BDD-cost:   10
c ---[1281]---> BDD-cost:   10
c ---[1280]---> BDD-cost:   10
c ---[1279]---> BDD-cost:   10
c ---[1278]---> BDD-cost:   10
c ---[1277]---> BDD-cost:   10
c ---[1276]---> BDD-cost:   10
c ---[1275]---> BDD-cost:   10
c ---[1274]---> BDD-cost:   10
c ---[1273]---> BDD-cost:   10
c ---[1272]---> BDD-cost:   10
c ---[1271]---> BDD-cost:   10
c ---[1270]---> BDD-cost:   10
c ---[1269]---> BDD-cost:   10
c ---[1268]---> BDD-cost:   10
c ---[1267]---> BDD-cost:   10
c ---[1266]---> BDD-cost:   10
c ---[1265]---> BDD-cost:   10
c ---[1264]---> BDD-cost:   10
c ---[1263]---> BDD-cost:   10
c ---[1262]---> BDD-cost:   10
c ---[1261]---> BDD-cost:   10
c ---[1260]---> BDD-cost:   10
c ---[1259]---> BDD-cost:   10
c ---[1258]---> BDD-cost:   10
c ---[1257]---> BDD-cost:   10
c ---[1256]---> BDD-cost:   10
c ---[1255]---> BDD-cost:   10
c ---[1254]---> BDD-cost:   10
c ---[1253]---> BDD-cost:   10
c ---[1252]---> BDD-cost:   10
c ---[1251]---> BDD-cost:   10
c ---[1250]---> BDD-cost:   10
c ---[1249]---> BDD-cost:   10
c ---[1248]---> BDD-cost:   10
c ---[1247]---> BDD-cost:   10
c ---[1246]---> BDD-cost:   10
c ---[1245]---> BDD-cost:   10
c ---[1244]---> BDD-cost:   10
c ---[1243]---> BDD-cost:   10
c ---[1242]---> BDD-cost:   10
c ---[1241]---> BDD-cost:   10
c ---[1240]---> BDD-cost:   10
c ---[1239]---> BDD-cost:   10
c ---[1238]---> BDD-cost:   10
c ---[1237]---> BDD-cost:   10
c ---[1236]---> BDD-cost:   10
c ---[1235]---> BDD-cost:   10
c ---[1234]---> BDD-cost:   10
c ---[1233]---> BDD-cost:   10
c ---[1232]---> BDD-cost:   10
c ---[1231]---> BDD-cost:   10
c ---[1230]---> BDD-cost:   10
c ---[1229]---> BDD-cost:   10
c ---[1228]---> BDD-cost:   10
c ---[1227]---> BDD-cost:   10
c ---[1226]---> BDD-cost:   10
c ---[1225]---> BDD-cost:   10
c ---[1224]---> BDD-cost:   10
c ---[1223]---> BDD-cost:   10
c ---[1222]---> BDD-cost:   10
c ---[1221]---> BDD-cost:   10
c ---[1220]---> BDD-cost:   10
c ---[1219]---> BDD-cost:   10
c ---[1218]---> BDD-cost:   10
c ---[1217]---> BDD-cost:   10
c ---[1216]---> BDD-cost:   10
c ---[1215]---> BDD-cost:   10
c ---[1214]---> BDD-cost:   10
c ---[1213]---> BDD-cost:   10
c ---[1212]---> BDD-cost:   10
c ---[1211]---> BDD-cost:   10
c ---[1210]---> BDD-cost:   10
c ---[1209]---> BDD-cost:   10
c ---[1208]---> BDD-cost:   10
c ---[1207]---> BDD-cost:   10
c ---[1206]---> BDD-cost:   10
c ---[1205]---> BDD-cost:   10
c ---[1204]---> BDD-cost:   10
c ---[1203]---> BDD-cost:   10
c ---[1202]---> BDD-cost:   10
c ---[1201]---> BDD-cost:   10
c ---[1196]---> BDD-cost:   10
c ---[1195]---> BDD-cost:   10
c ---[1194]---> BDD-cost:   10
c ---[1193]---> BDD-cost:   10
c ---[1192]---> BDD-cost:   10
c ---[1191]---> BDD-cost:   10
c ---[1190]---> BDD-cost:   10
c ---[1189]---> BDD-cost:   10
c ---[1188]---> BDD-cost:   10
c ---[1187]---> BDD-cost:   10
c ---[1186]---> BDD-cost:   10
c ---[1185]---> BDD-cost:   10
c ---[1184]---> BDD-cost:   10
c ---[1183]---> BDD-cost:   10
c ---[1182]---> BDD-cost:   10
c ---[1181]---> BDD-cost:   10
c ---[1180]---> BDD-cost:   10
c ---[1179]---> BDD-cost:   10
c ---[1178]---> BDD-cost:   10
c ---[1177]---> BDD-cost:   10
c ---[1176]---> BDD-cost:   10
c ---[1175]---> BDD-cost:   10
c ---[1174]---> BDD-cost:   10
c ---[1173]---> BDD-cost:   10
c ---[1172]---> BDD-cost:   10
c ---[1171]---> BDD-cost:   10
c ---[1170]---> BDD-cost:   10
c ---[1169]---> BDD-cost:   10
c ---[1168]---> BDD-cost:   10
c ---[1167]---> BDD-cost:   10
c ---[1166]---> BDD-cost:   10
c ---[1165]---> BDD-cost:   10
c ---[1164]---> BDD-cost:   10
c ---[1163]---> BDD-cost:   10
c ---[1162]---> BDD-cost:   10
c ---[1161]---> BDD-cost:   10
c ---[1160]---> BDD-cost:   10
c ---[1159]---> BDD-cost:   10
c ---[1158]---> BDD-cost:   10
c ---[1157]---> BDD-cost:   10
c ---[1156]---> BDD-cost:   10
c ---[1155]---> BDD-cost:   10
c ---[1154]---> BDD-cost:   10
c ---[1153]---> BDD-cost:   10
c ---[1152]---> BDD-cost:   10
c ---[1151]---> BDD-cost:   10
c ---[1150]---> BDD-cost:   10
c ---[1149]---> BDD-cost:   10
c ---[1148]---> BDD-cost:   10
c ---[1147]---> BDD-cost:   10
c ---[1146]---> BDD-cost:   10
c ---[1145]---> BDD-cost:   10
c ---[1144]---> BDD-cost:   10
c ---[1143]---> BDD-cost:   10
c ---[1142]---> BDD-cost:   10
c ---[1141]---> BDD-cost:   10
c ---[1140]---> BDD-cost:   10
c ---[1139]---> BDD-cost:   10
c ---[1138]---> BDD-cost:   10
c ---[1137]---> BDD-cost:   10
c ---[1136]---> BDD-cost:   10
c ---[1135]---> BDD-cost:   10
c ---[1134]---> BDD-cost:   10
c ---[1133]---> BDD-cost:   10
c ---[1132]---> BDD-cost:   10
c ---[1131]---> BDD-cost:   10
c ---[1130]---> BDD-cost:   10
c ---[1129]---> BDD-cost:   10
c ---[1128]---> BDD-cost:   10
c ---[1127]---> BDD-cost:   10
c ---[1126]---> BDD-cost:   10
c ---[1125]---> BDD-cost:   10
c ---[1124]---> BDD-cost:   10
c ---[1123]---> BDD-cost:   10
c ---[1122]---> BDD-cost:   10
c ---[1121]---> BDD-cost:   10
c ---[1120]---> BDD-cost:   10
c ---[1119]---> BDD-cost:   10
c ---[1114]---> BDD-cost:   10
c ---[1113]---> BDD-cost:   10
c ---[1112]---> BDD-cost:   10
c ---[1111]---> BDD-cost:   10
c ---[1110]---> BDD-cost:   10
c ---[1109]---> BDD-cost:   10
c ---[1108]---> BDD-cost:   10
c ---[1107]---> BDD-cost:   10
c ---[1106]---> BDD-cost:   10
c ---[1105]---> BDD-cost:   10
c ---[1104]---> BDD-cost:   10
c ---[1103]---> BDD-cost:   10
c ---[1102]---> BDD-cost:   10
c ---[1101]---> BDD-cost:   10
c ---[1100]---> BDD-cost:   10
c ---[1099]---> BDD-cost:   10
c ---[1098]---> BDD-cost:   10
c ---[1097]---> BDD-cost:   10
c ---[1096]---> BDD-cost:   10
c ---[1095]---> BDD-cost:   10
c ---[1094]---> BDD-cost:   10
c ---[1093]---> BDD-cost:   10
c ---[1092]---> BDD-cost:   10
c ---[1091]---> BDD-cost:   10
c ---[1090]---> BDD-cost:   10
c ---[1089]---> BDD-cost:   10
c ---[1088]---> BDD-cost:   10
c ---[1087]---> BDD-cost:   10
c ---[1086]---> BDD-cost:   10
c ---[1085]---> BDD-cost:   10
c ---[1084]---> BDD-cost:   10
c ---[1083]---> BDD-cost:   10
c ---[1082]---> BDD-cost:   10
c ---[1081]---> BDD-cost:   10
c ---[1080]---> BDD-cost:   10
c ---[1079]---> BDD-cost:   10
c ---[1078]---> BDD-cost:   10
c ---[1077]---> BDD-cost:   10
c ---[1076]---> BDD-cost:   10
c ---[1075]---> BDD-cost:   10
c ---[1074]---> BDD-cost:   10
c ---[1073]---> BDD-cost:   10
c ---[1072]---> BDD-cost:   10
c ---[1071]---> BDD-cost:   10
c ---[1070]---> BDD-cost:   10
c ---[1069]---> BDD-cost:   10
c ---[1068]---> BDD-cost:   10
c ---[1067]---> BDD-cost:   10
c ---[1066]---> BDD-cost:   10
c ---[1065]---> BDD-cost:   10
c ---[1064]---> BDD-cost:   10
c ---[1063]---> BDD-cost:   10
c ---[1062]---> BDD-cost:   10
c ---[1061]---> BDD-cost:   10
c ---[1060]---> BDD-cost:   10
c ---[1059]---> BDD-cost:   10
c ---[1058]---> BDD-cost:   10
c ---[1057]---> BDD-cost:   10
c ---[1056]---> BDD-cost:   10
c ---[1055]---> BDD-cost:   10
c ---[1054]---> BDD-cost:   10
c ---[1053]---> BDD-cost:   10
c ---[1052]---> BDD-cost:   10
c ---[1051]---> BDD-cost:   10
c ---[1050]---> BDD-cost:   10
c ---[1049]---> BDD-cost:   10
c ---[1048]---> BDD-cost:   10
c ---[1047]---> BDD-cost:   10
c ---[1046]---> BDD-cost:   10
c ---[1045]---> BDD-cost:   10
c ---[1044]---> BDD-cost:   10
c ---[1043]---> BDD-cost:   10
c ---[1042]---> BDD-cost:   10
c ---[1041]---> BDD-cost:   10
c ---[1040]---> BDD-cost:   10
c ---[1039]---> BDD-cost:   10
c ---[1038]---> BDD-cost:   10
c ---[1037]---> BDD-cost:   10
c ---[1032]---> BDD-cost:   10
c ---[1031]---> BDD-cost:   10
c ---[1030]---> BDD-cost:   10
c ---[1029]---> BDD-cost:   10
c ---[1028]---> BDD-cost:   10
c ---[1027]---> BDD-cost:   10
c ---[1026]---> BDD-cost:   10
c ---[1025]---> BDD-cost:   10
c ---[1024]---> BDD-cost:   10
c ---[1023]---> BDD-cost:   10
c ---[1022]---> BDD-cost:   10
c ---[1021]---> BDD-cost:   10
c ---[1020]---> BDD-cost:   10
c ---[1019]---> BDD-cost:   10
c ---[1018]---> BDD-cost:   10
c ---[1017]---> BDD-cost:   10
c ---[1016]---> BDD-cost:   10
c ---[1015]---> BDD-cost:   10
c ---[1014]---> BDD-cost:   10
c ---[1013]---> BDD-cost:   10
c ---[1012]---> BDD-cost:   10
c ---[1011]---> BDD-cost:   10
c ---[1010]---> BDD-cost:   10
c ---[1009]---> BDD-cost:   10
c ---[1008]---> BDD-cost:   10
c ---[1007]---> BDD-cost:   10
c ---[1006]---> BDD-cost:   10
c ---[1005]---> BDD-cost:   10
c ---[1004]---> BDD-cost:   10
c ---[1003]---> BDD-cost:   10
c ---[1002]---> BDD-cost:   10
c ---[1001]---> BDD-cost:   10
c ---[1000]---> BDD-cost:   10
c ---[ 999]---> BDD-cost:   10
c ---[ 998]---> BDD-cost:   10
c ---[ 997]---> BDD-cost:   10
c ---[ 996]---> BDD-cost:   10
c ---[ 995]---> BDD-cost:   10
c ---[ 994]---> BDD-cost:   10
c ---[ 993]---> BDD-cost:   10
c ---[ 992]---> BDD-cost:   10
c ---[ 991]---> BDD-cost:   10
c ---[ 990]---> BDD-cost:   10
c ---[ 989]---> BDD-cost:   10
c ---[ 988]---> BDD-cost:   10
c ---[ 987]---> BDD-cost:   10
c ---[ 986]---> BDD-cost:   10
c ---[ 985]---> BDD-cost:   10
c ---[ 984]---> BDD-cost:   10
c ---[ 983]---> BDD-cost:   10
c ---[ 982]---> BDD-cost:   10
c ---[ 981]---> BDD-cost:   10
c ---[ 980]---> BDD-cost:   10
c ---[ 979]---> BDD-cost:   10
c ---[ 978]---> BDD-cost:   10
c ---[ 977]---> BDD-cost:   10
c ---[ 976]---> BDD-cost:   10
c ---[ 975]---> BDD-cost:   10
c ---[ 974]---> BDD-cost:   10
c ---[ 973]---> BDD-cost:   10
c ---[ 972]---> BDD-cost:   10
c ---[ 971]---> BDD-cost:   10
c ---[ 970]---> BDD-cost:   10
c ---[ 969]---> BDD-cost:   10
c ---[ 968]---> BDD-cost:   10
c ---[ 967]---> BDD-cost:   10
c ---[ 966]---> BDD-cost:   10
c ---[ 965]---> BDD-cost:   10
c ---[ 964]---> BDD-cost:   10
c ---[ 963]---> BDD-cost:   10
c ---[ 962]---> BDD-cost:   10
c ---[ 961]---> BDD-cost:   10
c ---[ 960]---> BDD-cost:   10
c ---[ 959]---> BDD-cost:   10
c ---[ 958]---> BDD-cost:   10
c ---[ 957]---> BDD-cost:   10
c ---[ 956]---> BDD-cost:   10
c ---[ 955]---> BDD-cost:   10
c ---[ 950]---> BDD-cost:   10
c ---[ 949]---> BDD-cost:   10
c ---[ 948]---> BDD-cost:   10
c ---[ 947]---> BDD-cost:   10
c ---[ 946]---> BDD-cost:   10
c ---[ 945]---> BDD-cost:   10
c ---[ 944]---> BDD-cost:   10
c ---[ 943]---> BDD-cost:   10
c ---[ 942]---> BDD-cost:   10
c ---[ 941]---> BDD-cost:   10
c ---[ 940]---> BDD-cost:   10
c ---[ 939]---> BDD-cost:   10
c ---[ 938]---> BDD-cost:   10
c ---[ 937]---> BDD-cost:   10
c ---[ 936]---> BDD-cost:   10
c ---[ 935]---> BDD-cost:   10
c ---[ 934]---> BDD-cost:   10
c ---[ 933]---> BDD-cost:   10
c ---[ 932]---> BDD-cost:   10
c ---[ 931]---> BDD-cost:   10
c ---[ 930]---> BDD-cost:   10
c ---[ 929]---> BDD-cost:   10
c ---[ 928]---> BDD-cost:   10
c ---[ 927]---> BDD-cost:   10
c ---[ 926]---> BDD-cost:   10
c ---[ 925]---> BDD-cost:   10
c ---[ 924]---> BDD-cost:   10
c ---[ 923]---> BDD-cost:   10
c ---[ 922]---> BDD-cost:   10
c ---[ 921]---> BDD-cost:   10
c ---[ 920]---> BDD-cost:   10
c ---[ 919]---> BDD-cost:   10
c ---[ 918]---> BDD-cost:   10
c ---[ 917]---> BDD-cost:   10
c ---[ 916]---> BDD-cost:   10
c ---[ 915]---> BDD-cost:   10
c ---[ 914]---> BDD-cost:   10
c ---[ 913]---> BDD-cost:   10
c ---[ 912]---> BDD-cost:   10
c ---[ 911]---> BDD-cost:   10
c ---[ 910]---> BDD-cost:   10
c ---[ 909]---> BDD-cost:   10
c ---[ 908]---> BDD-cost:   10
c ---[ 907]---> BDD-cost:   10
c ---[ 906]---> BDD-cost:   10
c ---[ 905]---> BDD-cost:   10
c ---[ 904]---> BDD-cost:   10
c ---[ 903]---> BDD-cost:   10
c ---[ 902]---> BDD-cost:   10
c ---[ 901]---> BDD-cost:   10
c ---[ 900]---> BDD-cost:   10
c ---[ 899]---> BDD-cost:   10
c ---[ 898]---> BDD-cost:   10
c ---[ 897]---> BDD-cost:   10
c ---[ 896]---> BDD-cost:   10
c ---[ 895]---> BDD-cost:   10
c ---[ 894]---> BDD-cost:   10
c ---[ 893]---> BDD-cost:   10
c ---[ 892]---> BDD-cost:   10
c ---[ 891]---> BDD-cost:   10
c ---[ 890]---> BDD-cost:   10
c ---[ 889]---> BDD-cost:   10
c ---[ 888]---> BDD-cost:   10
c ---[ 887]---> BDD-cost:   10
c ---[ 886]---> BDD-cost:   10
c ---[ 885]---> BDD-cost:   10
c ---[ 884]---> BDD-cost:   10
c ---[ 883]---> BDD-cost:   10
c ---[ 882]---> BDD-cost:   10
c ---[ 881]---> BDD-cost:   10
c ---[ 880]---> BDD-cost:   10
c ---[ 879]---> BDD-cost:   10
c ---[ 878]---> BDD-cost:   10
c ---[ 877]---> BDD-cost:   10
c ---[ 876]---> BDD-cost:   10
c ---[ 875]---> BDD-cost:   10
c ---[ 874]---> BDD-cost:   10
c ---[ 873]---> BDD-cost:   10
c ---[ 872]---> BDD-cost:   10
c ---[ 871]---> BDD-cost:   10
c ---[ 870]---> BDD-cost:   10
c ---[ 869]---> BDD-cost:   10
c ---[ 864]---> BDD-cost:   10
c ---[ 863]---> BDD-cost:   10
c ---[ 862]---> BDD-cost:   10
c ---[ 861]---> BDD-cost:   10
c ---[ 860]---> BDD-cost:   10
c ---[ 859]---> BDD-cost:   10
c ---[ 858]---> BDD-cost:   10
c ---[ 857]---> BDD-cost:   10
c ---[ 856]---> BDD-cost:   10
c ---[ 855]---> BDD-cost:   10
c ---[ 854]---> BDD-cost:   10
c ---[ 853]---> BDD-cost:   10
c ---[ 852]---> BDD-cost:   10
c ---[ 851]---> BDD-cost:   10
c ---[ 850]---> BDD-cost:   10
c ---[ 849]---> BDD-cost:   10
c ---[ 848]---> BDD-cost:   10
c ---[ 847]---> BDD-cost:   10
c ---[ 846]---> BDD-cost:   10
c ---[ 845]---> BDD-cost:   10
c ---[ 844]---> BDD-cost:   10
c ---[ 843]---> BDD-cost:   10
c ---[ 842]---> BDD-cost:   10
c ---[ 841]---> BDD-cost:   10
c ---[ 840]---> BDD-cost:   10
c ---[ 839]---> BDD-cost:   10
c ---[ 838]---> BDD-cost:   10
c ---[ 837]---> BDD-cost:   10
c ---[ 836]---> BDD-cost:   10
c ---[ 835]---> BDD-cost:   10
c ---[ 834]---> BDD-cost:   10
c ---[ 833]---> BDD-cost:   10
c ---[ 832]---> BDD-cost:   10
c ---[ 831]---> BDD-cost:   10
c ---[ 830]---> BDD-cost:   10
c ---[ 829]---> BDD-cost:   10
c ---[ 828]---> BDD-cost:   10
c ---[ 827]---> BDD-cost:   10
c ---[ 826]---> BDD-cost:   10
c ---[ 825]---> BDD-cost:   10
c ---[ 824]---> BDD-cost:   10
c ---[ 823]---> BDD-cost:   10
c ---[ 822]---> BDD-cost:   10
c ---[ 821]---> BDD-cost:   10
c ---[ 820]---> BDD-cost:   10
c ---[ 819]---> BDD-cost:   10
c ---[ 818]---> BDD-cost:   10
c ---[ 817]---> BDD-cost:   10
c ---[ 816]---> BDD-cost:   10
c ---[ 815]---> BDD-cost:   10
c ---[ 814]---> BDD-cost:   10
c ---[ 813]---> BDD-cost:   10
c ---[ 812]---> BDD-cost:   10
c ---[ 811]---> BDD-cost:   10
c ---[ 810]---> BDD-cost:   10
c ---[ 809]---> BDD-cost:   10
c ---[ 808]---> BDD-cost:   10
c ---[ 807]---> BDD-cost:   10
c ---[ 806]---> BDD-cost:   10
c ---[ 805]---> BDD-cost:   10
c ---[ 804]---> BDD-cost:   10
c ---[ 803]---> BDD-cost:   10
c ---[ 802]---> BDD-cost:   10
c ---[ 801]---> BDD-cost:   10
c ---[ 800]---> BDD-cost:   10
c ---[ 799]---> BDD-cost:   10
c ---[ 798]---> BDD-cost:   10
c ---[ 797]---> BDD-cost:   10
c ---[ 796]---> BDD-cost:   10
c ---[ 795]---> BDD-cost:   10
c ---[ 794]---> BDD-cost:   10
c ---[ 793]---> BDD-cost:   10
c ---[ 792]---> BDD-cost:   10
c ---[ 791]---> BDD-cost:   10
c ---[ 790]---> BDD-cost:   10
c ---[ 789]---> BDD-cost:   10
c ---[ 788]---> BDD-cost:   10
c ---[ 787]---> BDD-cost:   10
c ---[ 782]---> BDD-cost:   10
c ---[ 781]---> BDD-cost:   10
c ---[ 780]---> BDD-cost:   10
c ---[ 779]---> BDD-cost:   10
c ---[ 778]---> BDD-cost:   10
c ---[ 777]---> BDD-cost:   10
c ---[ 776]---> BDD-cost:   10
c ---[ 775]---> BDD-cost:   10
c ---[ 774]---> BDD-cost:   10
c ---[ 773]---> BDD-cost:   10
c ---[ 772]---> BDD-cost:   10
c ---[ 771]---> BDD-cost:   10
c ---[ 770]---> BDD-cost:   10
c ---[ 769]---> BDD-cost:   10
c ---[ 768]---> BDD-cost:   10
c ---[ 767]---> BDD-cost:   10
c ---[ 766]---> BDD-cost:   10
c ---[ 765]---> BDD-cost:   10
c ---[ 764]---> BDD-cost:   10
c ---[ 763]---> BDD-cost:   10
c ---[ 762]---> BDD-cost:   10
c ---[ 761]---> BDD-cost:   10
c ---[ 760]---> BDD-cost:   10
c ---[ 759]---> BDD-cost:   10
c ---[ 758]---> BDD-cost:   10
c ---[ 757]---> BDD-cost:   10
c ---[ 756]---> BDD-cost:   10
c ---[ 755]---> BDD-cost:   10
c ---[ 754]---> BDD-cost:   10
c ---[ 753]---> BDD-cost:   10
c ---[ 752]---> BDD-cost:   10
c ---[ 751]---> BDD-cost:   10
c ---[ 750]---> BDD-cost:   10
c ---[ 749]---> BDD-cost:   10
c ---[ 748]---> BDD-cost:   10
c ---[ 747]---> BDD-cost:   10
c ---[ 746]---> BDD-cost:   10
c ---[ 745]---> BDD-cost:   10
c ---[ 744]---> BDD-cost:   10
c ---[ 743]---> BDD-cost:   10
c ---[ 742]---> BDD-cost:   10
c ---[ 741]---> BDD-cost:   10
c ---[ 740]---> BDD-cost:   10
c ---[ 739]---> BDD-cost:   10
c ---[ 738]---> BDD-cost:   10
c ---[ 737]---> BDD-cost:   10
c ---[ 736]---> BDD-cost:   10
c ---[ 735]---> BDD-cost:   10
c ---[ 734]---> BDD-cost:   10
c ---[ 733]---> BDD-cost:   10
c ---[ 732]---> BDD-cost:   10
c ---[ 731]---> BDD-cost:   10
c ---[ 730]---> BDD-cost:   10
c ---[ 729]---> BDD-cost:   10
c ---[ 728]---> BDD-cost:   10
c ---[ 727]---> BDD-cost:   10
c ---[ 726]---> BDD-cost:   10
c ---[ 725]---> BDD-cost:   10
c ---[ 724]---> BDD-cost:   10
c ---[ 723]---> BDD-cost:   10
c ---[ 722]---> BDD-cost:   10
c ---[ 721]---> BDD-cost:   10
c ---[ 720]---> BDD-cost:   10
c ---[ 719]---> BDD-cost:   10
c ---[ 718]---> BDD-cost:   10
c ---[ 717]---> BDD-cost:   10
c ---[ 716]---> BDD-cost:   10
c ---[ 715]---> BDD-cost:   10
c ---[ 714]---> BDD-cost:   10
c ---[ 713]---> BDD-cost:   10
c ---[ 712]---> BDD-cost:   10
c ---[ 711]---> BDD-cost:   10
c ---[ 710]---> BDD-cost:   10
c ---[ 709]---> BDD-cost:   10
c ---[ 708]---> BDD-cost:   10
c ---[ 707]---> BDD-cost:   10
c ---[ 706]---> BDD-cost:   10
c ---[ 705]---> BDD-cost:   10
c ---[ 700]---> BDD-cost:   10
c ---[ 699]---> BDD-cost:   10
c ---[ 698]---> BDD-cost:   10
c ---[ 697]---> BDD-cost:   10
c ---[ 696]---> BDD-cost:   10
c ---[ 695]---> BDD-cost:   10
c ---[ 694]---> BDD-cost:   10
c ---[ 693]---> BDD-cost:   10
c ---[ 692]---> BDD-cost:   10
c ---[ 691]---> BDD-cost:   10
c ---[ 690]---> BDD-cost:   10
c ---[ 689]---> BDD-cost:   10
c ---[ 688]---> BDD-cost:   10
c ---[ 687]---> BDD-cost:   10
c ---[ 686]---> BDD-cost:   10
c ---[ 685]---> BDD-cost:   10
c ---[ 684]---> BDD-cost:   10
c ---[ 683]---> BDD-cost:   10
c ---[ 682]---> BDD-cost:   10
c ---[ 681]---> BDD-cost:   10
c ---[ 680]---> BDD-cost:   10
c ---[ 679]---> BDD-cost:   10
c ---[ 678]---> BDD-cost:   10
c ---[ 677]---> BDD-cost:   10
c ---[ 676]---> BDD-cost:   10
c ---[ 675]---> BDD-cost:   10
c ---[ 674]---> BDD-cost:   10
c ---[ 673]---> BDD-cost:   10
c ---[ 672]---> BDD-cost:   10
c ---[ 671]---> BDD-cost:   10
c ---[ 670]---> BDD-cost:   10
c ---[ 669]---> BDD-cost:   10
c ---[ 668]---> BDD-cost:   10
c ---[ 667]---> BDD-cost:   10
c ---[ 666]---> BDD-cost:   10
c ---[ 665]---> BDD-cost:   10
c ---[ 664]---> BDD-cost:   10
c ---[ 663]---> BDD-cost:   10
c ---[ 662]---> BDD-cost:   10
c ---[ 661]---> BDD-cost:   10
c ---[ 660]---> BDD-cost:   10
c ---[ 659]---> BDD-cost:   10
c ---[ 658]---> BDD-cost:   10
c ---[ 657]---> BDD-cost:   10
c ---[ 656]---> BDD-cost:   10
c ---[ 655]---> BDD-cost:   10
c ---[ 654]---> BDD-cost:   10
c ---[ 653]---> BDD-cost:   10
c ---[ 652]---> BDD-cost:   10
c ---[ 651]---> BDD-cost:   10
c ---[ 650]---> BDD-cost:   10
c ---[ 649]---> BDD-cost:   10
c ---[ 648]---> BDD-cost:   10
c ---[ 647]---> BDD-cost:   10
c ---[ 646]---> BDD-cost:   10
c ---[ 645]---> BDD-cost:   10
c ---[ 644]---> BDD-cost:   10
c ---[ 643]---> BDD-cost:   10
c ---[ 642]---> BDD-cost:   10
c ---[ 641]---> BDD-cost:   10
c ---[ 640]---> BDD-cost:   10
c ---[ 639]---> BDD-cost:   10
c ---[ 638]---> BDD-cost:   10
c ---[ 637]---> BDD-cost:   10
c ---[ 636]---> BDD-cost:   10
c ---[ 635]---> BDD-cost:   10
c ---[ 634]---> BDD-cost:   10
c ---[ 633]---> BDD-cost:   10
c ---[ 632]---> BDD-cost:   10
c ---[ 631]---> BDD-cost:   10
c ---[ 630]---> BDD-cost:   10
c ---[ 629]---> BDD-cost:   10
c ---[ 628]---> BDD-cost:   10
c ---[ 627]---> BDD-cost:   10
c ---[ 626]---> BDD-cost:   10
c ---[ 625]---> BDD-cost:   10
c ---[ 624]---> BDD-cost:   10
c ---[ 623]---> BDD-cost:   10
c ---[ 618]---> BDD-cost:   10
c ---[ 617]---> BDD-cost:   10
c ---[ 616]---> BDD-cost:   10
c ---[ 615]---> BDD-cost:   10
c ---[ 614]---> BDD-cost:   10
c ---[ 613]---> BDD-cost:   10
c ---[ 612]---> BDD-cost:   10
c ---[ 611]---> BDD-cost:   10
c ---[ 610]---> BDD-cost:   10
c ---[ 609]---> BDD-cost:   10
c ---[ 608]---> BDD-cost:   10
c ---[ 607]---> BDD-cost:   10
c ---[ 606]---> BDD-cost:   10
c ---[ 605]---> BDD-cost:   10
c ---[ 604]---> BDD-cost:   10
c ---[ 603]---> BDD-cost:   10
c ---[ 602]---> BDD-cost:   10
c ---[ 601]---> BDD-cost:   10
c ---[ 600]---> BDD-cost:   10
c ---[ 599]---> BDD-cost:   10
c ---[ 598]---> BDD-cost:   10
c ---[ 597]---> BDD-cost:   10
c ---[ 596]---> BDD-cost:   10
c ---[ 595]---> BDD-cost:   10
c ---[ 594]---> BDD-cost:   10
c ---[ 593]---> BDD-cost:   10
c ---[ 592]---> BDD-cost:   10
c ---[ 591]---> BDD-cost:   10
c ---[ 590]---> BDD-cost:   10
c ---[

Watcher Data

Enforcing CPU limit (will send SIGTERM then SIGKILL): 1200 seconds
Enforcing CPUTime (will send SIGXCPU) limit: 1230 seconds
Enforcing Stack size limit: 67108864 bytes
Enforcing memory limit (will send SIGTERM then SIGKILL): 921600 Kb
Enforcing VSIZE limit: 994918400 bytes
Current StackSize limit: 67108864 bytes
Raw data (/proc/27399/stat): 27399 (minisat+_script) R 27398 27399 2660 0 -1 0 19 0 0 0 0 0 0 0 22 0 1 0 1854684993 712704 3 4294967295 134512640 135087896 3221224496 3221224496 1073744960 0 0 5 0 0 0 0 17 1 0 0
Raw data (/proc/27399/statm): 174 3 169 147 0 27 0
[pid=27399] vsize: 696
open syscall for file /etc/ld.so.preload
open syscall for file tls/i686/mmx/libtermcap.so.2
open syscall for file tls/i686/libtermcap.so.2
open syscall for file tls/mmx/libtermcap.so.2
open syscall for file tls/libtermcap.so.2
open syscall for file i686/mmx/libtermcap.so.2
open syscall for file i686/libtermcap.so.2
open syscall for file mmx/libtermcap.so.2
open syscall for file libtermcap.so.2
open syscall for file /oldhome/oroussel/lib/tls/i686/mmx/libtermcap.so.2
open syscall for file /oldhome/oroussel/lib/tls/i686/libtermcap.so.2
open syscall for file /oldhome/oroussel/lib/tls/mmx/libtermcap.so.2
open syscall for file /oldhome/oroussel/lib/tls/libtermcap.so.2
open syscall for file /oldhome/oroussel/lib/i686/mmx/libtermcap.so.2
open syscall for file /oldhome/oroussel/lib/i686/libtermcap.so.2
open syscall for file /oldhome/oroussel/lib/mmx/libtermcap.so.2
open syscall for file /oldhome/oroussel/lib/libtermcap.so.2
open syscall for file /etc/ld.so.cache
open syscall for file /lib/libtermcap.so.2
open syscall for file tls/i686/mmx/libdl.so.2
open syscall for file tls/i686/libdl.so.2
open syscall for file tls/mmx/libdl.so.2
open syscall for file tls/libdl.so.2
open syscall for file i686/mmx/libdl.so.2
open syscall for file i686/libdl.so.2
open syscall for file mmx/libdl.so.2
open syscall for file libdl.so.2
open syscall for file /oldhome/oroussel/lib/libdl.so.2
open syscall for file /lib/libdl.so.2
open syscall for file tls/i686/mmx/libc.so.6
open syscall for file tls/i686/libc.so.6
open syscall for file tls/mmx/libc.so.6
open syscall for file tls/libc.so.6
open syscall for file i686/mmx/libc.so.6
open syscall for file i686/libc.so.6
open syscall for file mmx/libc.so.6
open syscall for file libc.so.6
open syscall for file /oldhome/oroussel/lib/libc.so.6
open syscall for file /lib/tls/libc.so.6
open syscall for file /dev/tty
open syscall for file /etc/mtab
open syscall for file /proc/meminfo
open syscall for file /oldhome/oroussel/solvers/minisat+_script
New process pid=27400
New process pid=27401
New process pid=27402
execve syscall for /bin/sed executable
One traced child (pid=27401) exited with status: 0
open syscall for file /etc/ld.so.preload
open syscall for file tls/i686/mmx/libc.so.6
open syscall for file tls/i686/libc.so.6
open syscall for file tls/mmx/libc.so.6
open syscall for file tls/libc.so.6
open syscall for file i686/mmx/libc.so.6
open syscall for file i686/libc.so.6
open syscall for file mmx/libc.so.6
open syscall for file libc.so.6
open syscall for file /oldhome/oroussel/lib/tls/i686/mmx/libc.so.6
open syscall for file /oldhome/oroussel/lib/tls/i686/libc.so.6
open syscall for file /oldhome/oroussel/lib/tls/mmx/libc.so.6
open syscall for file /oldhome/oroussel/lib/tls/libc.so.6
open syscall for file /oldhome/oroussel/lib/i686/mmx/libc.so.6
open syscall for file /oldhome/oroussel/lib/i686/libc.so.6
open syscall for file /oldhome/oroussel/lib/mmx/libc.so.6
open syscall for file /oldhome/oroussel/lib/libc.so.6
open syscall for file /etc/ld.so.cache
open syscall for file /lib/tls/libc.so.6
One traced child (pid=27402) exited with status: 0
One traced child (pid=27400) exited with status: 0
New process pid=27403
execve syscall for /oldhome/oroussel/solvers/minisat+_64-bit_static executable
open syscall for file /dev/null
open syscall for file /oldhome/oroussel/tmp/wulflinc20/normalized-mps-v2-20-10-swath3.opb
One traced child (pid=27403) exited with status: 5
open syscall for file /oldhome/oroussel/solvers/
New process pid=27404
execve syscall for /oldhome/oroussel/solvers/minisat+_bignum_static executable
open syscall for file /dev/null
open syscall for file /oldhome/oroussel/tmp/wulflinc20/normalized-mps-v2-20-10-swath3.opb

[startup+10.0037 s]
Raw data (loadavg): 0.91 0.96 0.92 2/57 27404
Raw data (/proc/27399/stat): 27399 (minisat+_script) S 27398 27399 2660 0 -1 0 314 2516 0 0 0 1 46 10 17 0 1 0 1854684993 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27399/statm): 532 234 485 147 0 385 0
[pid=27399] vsize: 2128
Raw data (/proc/27404/stat): 27404 (minisat+_bignum) R 27399 27399 2660 0 -1 0 8139 0 0 0 794 37 0 0 17 0 1 0 1854685127 28180480 6352 4294967295 134512640 135167914 3221224448 3221222784 134845933 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27404/statm): 6880 6352 162 162 0 6718 0
[pid=27404] vsize: 27520
Current children cumulated CPU time (s) 8.88
Current children cumulated vsize (Kb) 29648

[startup+20.0054 s]
Raw data (loadavg): 0.92 0.96 0.92 2/57 27404
Raw data (/proc/27399/stat): 27399 (minisat+_script) S 27398 27399 2660 0 -1 0 314 2516 0 0 0 1 46 10 17 0 1 0 1854684993 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27399/statm): 532 234 485 147 0 385 0
[pid=27399] vsize: 2128
Raw data (/proc/27404/stat): 27404 (minisat+_bignum) R 27399 27399 2660 0 -1 0 10266 0 0 0 1765 50 0 0 25 0 1 0 1854685127 24805376 5657 4294967295 134512640 135167914 3221224448 3221222220 134843002 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27404/statm): 6056 5657 162 162 0 5894 0
[pid=27404] vsize: 24224
Current children cumulated CPU time (s) 18.72
Current children cumulated vsize (Kb) 26352

[startup+30.0061 s]
Raw data (loadavg): 0.93 0.96 0.92 2/57 27404
Raw data (/proc/27399/stat): 27399 (minisat+_script) S 27398 27399 2660 0 -1 0 314 2516 0 0 0 1 46 10 17 0 1 0 1854684993 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27399/statm): 532 234 485 147 0 385 0
[pid=27399] vsize: 2128
Raw data (/proc/27404/stat): 27404 (minisat+_bignum) R 27399 27399 2660 0 -1 0 12727 0 0 0 2726 68 0 0 25 0 1 0 1854685127 34889728 8118 4294967295 134512640 135167914 3221224448 3221222840 134516613 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27404/statm): 8518 8118 162 162 0 8356 0
[pid=27404] vsize: 34072
Current children cumulated CPU time (s) 28.51
Current children cumulated vsize (Kb) 36200

[startup+40.0069 s]
Raw data (loadavg): 0.94 0.96 0.92 2/57 27404
Raw data (/proc/27399/stat): 27399 (minisat+_script) S 27398 27399 2660 0 -1 0 314 2516 0 0 0 1 46 10 17 0 1 0 1854684993 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27399/statm): 532 234 485 147 0 385 0
[pid=27399] vsize: 2128
Raw data (/proc/27404/stat): 27404 (minisat+_bignum) R 27399 27399 2660 0 -1 0 15744 0 0 0 3695 83 0 0 25 0 1 0 1854685127 46698496 11043 4294967295 134512640 135167914 3221224448 3221223204 134697161 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27404/statm): 11401 11043 162 162 0 11239 0
[pid=27404] vsize: 45604
Current children cumulated CPU time (s) 38.35
Current children cumulated vsize (Kb) 47732

[startup+50.0086 s]
Raw data (loadavg): 0.95 0.96 0.92 2/57 27404
Raw data (/proc/27399/stat): 27399 (minisat+_script) S 27398 27399 2660 0 -1 0 314 2516 0 0 0 1 46 10 17 0 1 0 1854684993 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27399/statm): 532 234 485 147 0 385 0
[pid=27399] vsize: 2128
Raw data (/proc/27404/stat): 27404 (minisat+_bignum) R 27399 27399 2660 0 -1 0 15744 0 0 0 4695 84 0 0 25 0 1 0 1854685127 46698496 11043 4294967295 134512640 135167914 3221224448 3221223204 134697170 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27404/statm): 11401 11043 162 162 0 11239 0
[pid=27404] vsize: 45604
Current children cumulated CPU time (s) 48.36
Current children cumulated vsize (Kb) 47732

[startup+60.0093 s]
Raw data (loadavg): 0.96 0.96 0.92 2/57 27404
Raw data (/proc/27399/stat): 27399 (minisat+_script) S 27398 27399 2660 0 -1 0 314 2516 0 0 0 1 46 10 17 0 1 0 1854684993 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27399/statm): 532 234 485 147 0 385 0
[pid=27399] vsize: 2128
Raw data (/proc/27404/stat): 27404 (minisat+_bignum) R 27399 27399 2660 0 -1 0 15744 0 0 0 5695 84 0 0 25 0 1 0 1854685127 46698496 11043 4294967295 134512640 135167914 3221224448 3221223272 134522234 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27404/statm): 11401 11043 162 162 0 11239 0
[pid=27404] vsize: 45604
Current children cumulated CPU time (s) 58.36
Current children cumulated vsize (Kb) 47732

[startup+70.0111 s]
Raw data (loadavg): 0.96 0.96 0.92 2/57 27404
Raw data (/proc/27399/stat): 27399 (minisat+_script) S 27398 27399 2660 0 -1 0 314 2516 0 0 0 1 46 10 17 0 1 0 1854684993 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27399/statm): 532 234 485 147 0 385 0
[pid=27399] vsize: 2128
Raw data (/proc/27404/stat): 27404 (minisat+_bignum) R 27399 27399 2660 0 -1 0 15744 0 0 0 6694 85 0 0 25 0 1 0 1854685127 46698496 11043 4294967295 134512640 135167914 3221224448 3221223296 134596417 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27404/statm): 11401 11043 162 162 0 11239 0
[pid=27404] vsize: 45604
Current children cumulated CPU time (s) 68.36
Current children cumulated vsize (Kb) 47732

[startup+80.0128 s]
Raw data (loadavg): 0.97 0.96 0.92 2/57 27404
Raw data (/proc/27399/stat): 27399 (minisat+_script) S 27398 27399 2660 0 -1 0 314 2516 0 0 0 1 46 10 17 0 1 0 1854684993 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27399/statm): 532 234 485 147 0 385 0
[pid=27399] vsize: 2128
Raw data (/proc/27404/stat): 27404 (minisat+_bignum) R 27399 27399 2660 0 -1 0 15744 0 0 0 7694 85 0 0 25 0 1 0 1854685127 46698496 11043 4294967295 134512640 135167914 3221224448 3221223204 134697187 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27404/statm): 11401 11043 162 162 0 11239 0
[pid=27404] vsize: 45604
Current children cumulated CPU time (s) 78.36
Current children cumulated vsize (Kb) 47732

[startup+90.0135 s]
Raw data (loadavg): 0.97 0.96 0.92 2/57 27404
Raw data (/proc/27399/stat): 27399 (minisat+_script) S 27398 27399 2660 0 -1 0 314 2516 0 0 0 1 46 10 17 0 1 0 1854684993 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27399/statm): 532 234 485 147 0 385 0
[pid=27399] vsize: 2128
Raw data (/proc/27404/stat): 27404 (minisat+_bignum) R 27399 27399 2660 0 -1 0 15744 0 0 0 8694 86 0 0 25 0 1 0 1854685127 46698496 11043 4294967295 134512640 135167914 3221224448 3221223204 134697170 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27404/statm): 11401 11043 162 162 0 11239 0
[pid=27404] vsize: 45604
Current children cumulated CPU time (s) 88.37
Current children cumulated vsize (Kb) 47732

[startup+100.015 s]
Raw data (loadavg): 0.98 0.96 0.92 2/57 27404
Raw data (/proc/27399/stat): 27399 (minisat+_script) S 27398 27399 2660 0 -1 0 314 2516 0 0 0 1 46 10 17 0 1 0 1854684993 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27399/statm): 532 234 485 147 0 385 0
[pid=27399] vsize: 2128
Raw data (/proc/27404/stat): 27404 (minisat+_bignum) R 27399 27399 2660 0 -1 0 15744 0 0 0 9694 86 0 0 25 0 1 0 1854685127 46698496 11043 4294967295 134512640 135167914 3221224448 3221223296 134594169 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27404/statm): 11401 11043 162 162 0 11239 0
[pid=27404] vsize: 45604
Current children cumulated CPU time (s) 98.37
Current children cumulated vsize (Kb) 47732

[startup+110.016 s]
Raw data (loadavg): 0.98 0.97 0.92 2/57 27404
Raw data (/proc/27399/stat): 27399 (minisat+_script) S 27398 27399 2660 0 -1 0 314 2516 0 0 0 1 46 10 17 0 1 0 1854684993 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27399/statm): 532 234 485 147 0 385 0
[pid=27399] vsize: 2128
Raw data (/proc/27404/stat): 27404 (minisat+_bignum) R 27399 27399 2660 0 -1 0 15744 0 0 0 10693 86 0 0 25 0 1 0 1854685127 46698496 11043 4294967295 134512640 135167914 3221224448 3221223204 134697170 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27404/statm): 11401 11043 162 162 0 11239 0
[pid=27404] vsize: 45604
Current children cumulated CPU time (s) 108.36
Current children cumulated vsize (Kb) 47732

[startup+120.018 s]
Raw data (loadavg): 0.98 0.97 0.92 2/57 27404
Raw data (/proc/27399/stat): 27399 (minisat+_script) S 27398 27399 2660 0 -1 0 314 2516 0 0 0 1 46 10 17 0 1 0 1854684993 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27399/statm): 532 234 485 147 0 385 0
[pid=27399] vsize: 2128
Raw data (/proc/27404/stat): 27404 (minisat+_bignum) R 27399 27399 2660 0 -1 0 15744 0 0 0 11693 86 0 0 25 0 1 0 1854685127 46698496 11043 4294967295 134512640 135167914 3221224448 3221223204 134697170 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27404/statm): 11401 11043 162 162 0 11239 0
[pid=27404] vsize: 45604
Current children cumulated CPU time (s) 118.36
Current children cumulated vsize (Kb) 47732

[startup+130.018 s]
Raw data (loadavg): 0.98 0.97 0.92 2/57 27404
Raw data (/proc/27399/stat): 27399 (minisat+_script) S 27398 27399 2660 0 -1 0 314 2516 0 0 0 1 46 10 17 0 1 0 1854684993 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27399/statm): 532 234 485 147 0 385 0
[pid=27399] vsize: 2128
Raw data (/proc/27404/stat): 27404 (minisat+_bignum) R 27399 27399 2660 0 -1 0 15744 0 0 0 12692 87 0 0 25 0 1 0 1854685127 46698496 11043 4294967295 134512640 135167914 3221224448 3221223204 134697161 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27404/statm): 11401 11043 162 162 0 11239 0
[pid=27404] vsize: 45604
Current children cumulated CPU time (s) 128.36
Current children cumulated vsize (Kb) 47732

[startup+140.019 s]
Raw data (loadavg): 0.99 0.97 0.92 2/57 27404
Raw data (/proc/27399/stat): 27399 (minisat+_script) S 27398 27399 2660 0 -1 0 314 2516 0 0 0 1 46 10 17 0 1 0 1854684993 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27399/statm): 532 234 485 147 0 385 0
[pid=27399] vsize: 2128
Raw data (/proc/27404/stat): 27404 (minisat+_bignum) R 27399 27399 2660 0 -1 0 15744 0 0 0 13692 87 0 0 25 0 1 0 1854685127 46698496 11043 4294967295 134512640 135167914 3221224448 3221223216 134691240 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27404/statm): 11401 11043 162 162 0 11239 0
[pid=27404] vsize: 45604
Current children cumulated CPU time (s) 138.36
Current children cumulated vsize (Kb) 47732

[startup+150.021 s]
Raw data (loadavg): 0.99 0.97 0.92 2/57 27404
Raw data (/proc/27399/stat): 27399 (minisat+_script) S 27398 27399 2660 0 -1 0 314 2516 0 0 0 1 46 10 17 0 1 0 1854684993 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27399/statm): 532 234 485 147 0 385 0
[pid=27399] vsize: 2128
Raw data (/proc/27404/stat): 27404 (minisat+_bignum) R 27399 27399 2660 0 -1 0 15744 0 0 0 14692 88 0 0 25 0 1 0 1854685127 46698496 11043 4294967295 134512640 135167914 3221224448 3221223216 134691310 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27404/statm): 11401 11043 162 162 0 11239 0
[pid=27404] vsize: 45604
Current children cumulated CPU time (s) 148.37
Current children cumulated vsize (Kb) 47732

[startup+160.022 s]
Raw data (loadavg): 0.99 0.97 0.92 2/57 27404
Raw data (/proc/27399/stat): 27399 (minisat+_script) S 27398 27399 2660 0 -1 0 314 2516 0 0 0 1 46 10 17 0 1 0 1854684993 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27399/statm): 532 234 485 147 0 385 0
[pid=27399] vsize: 2128
Raw data (/proc/27404/stat): 27404 (minisat+_bignum) R 27399 27399 2660 0 -1 0 15942 0 0 0 15689 90 0 0 25 0 1 0 1854685127 46317568 10951 4294967295 134512640 135167914 3221224448 3221223232 134843130 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27404/statm): 11308 10951 162 162 0 11146 0
[pid=27404] vsize: 45232
Current children cumulated CPU time (s) 158.36
Current children cumulated vsize (Kb) 47360

[startup+170.023 s]
Raw data (loadavg): 0.99 0.97 0.92 2/57 27404
Raw data (/proc/27399/stat): 27399 (minisat+_script) S 27398 27399 2660 0 -1 0 314 2516 0 0 0 1 46 10 17 0 1 0 1854684993 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27399/statm): 532 234 485 147 0 385 0
[pid=27399] vsize: 2128
Raw data (/proc/27404/stat): 27404 (minisat+_bignum) R 27399 27399 2660 0 -1 0 27195 0 0 0 16604 131 0 0 25 0 1 0 1854685127 89063424 21387 4294967295 134512640 135167914 3221224448 3211232192 134625512 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27404/statm): 21744 21387 162 162 0 21582 0
[pid=27404] vsize: 86976
Current children cumulated CPU time (s) 167.92
Current children cumulated vsize (Kb) 89104

[startup+180.024 s]
Raw data (loadavg): 0.99 0.97 0.92 1/57 27404
Raw data (/proc/27399/stat): 27399 (minisat+_script) S 27398 27399 2660 0 -1 0 314 2516 0 0 0 1 46 10 17 0 1 0 1854684993 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27399/statm): 532 234 485 147 0 385 0
[pid=27399] vsize: 2128
Raw data (/proc/27404/stat): 27404 (minisat+_bignum) T 27399 27399 2660 0 -1 0 33808 0 0 0 17550 156 0 0 25 0 1 0 1854685127 108052480 26023 4294967295 134512640 135167914 3221224448 3211229932 134934490 0 0 5 16386 3222434794 0 0 17 1 0 0
Raw data (/proc/27404/statm): 26380 26023 162 162 0 26218 0
[pid=27404] vsize: 105520
Current children cumulated CPU time (s) 177.63
Current children cumulated vsize (Kb) 107648

[startup+190.026 s]
Raw data (loadavg): 0.99 0.97 0.92 2/57 27404
Raw data (/proc/27399/stat): 27399 (minisat+_script) S 27398 27399 2660 0 -1 0 314 2516 0 0 0 1 46 10 17 0 1 0 1854684993 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27399/statm): 532 234 485 147 0 385 0
[pid=27399] vsize: 2128
Raw data (/proc/27404/stat): 27404 (minisat+_bignum) R 27399 27399 2660 0 -1 0 38617 0 0 0 18497 180 0 0 25 0 1 0 1854685127 127750144 30832 4294967295 134512640 135167914 3221224448 3211231648 134845895 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27404/statm): 31189 30832 162 162 0 31027 0
[pid=27404] vsize: 124756
Current children cumulated CPU time (s) 187.34
Current children cumulated vsize (Kb) 126884

[startup+200.026 s]
Raw data (loadavg): 0.99 0.97 0.92 2/57 27404
Raw data (/proc/27399/stat): 27399 (minisat+_script) S 27398 27399 2660 0 -1 0 314 2516 0 0 0 1 46 10 17 0 1 0 1854684993 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27399/statm): 532 234 485 147 0 385 0
[pid=27399] vsize: 2128
Raw data (/proc/27404/stat): 27404 (minisat+_bignum) R 27399 27399 2660 0 -1 0 47477 0 0 0 19443 210 0 0 25 0 1 0 1854685127 153239552 37055 4294967295 134512640 135167914 3221224448 3211260412 134694320 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27404/statm): 37412 37055 162 162 0 37250 0
[pid=27404] vsize: 149648
Current children cumulated CPU time (s) 197.1
Current children cumulated vsize (Kb) 151776

[startup+210.027 s]
Raw data (loadavg): 0.99 0.97 0.92 2/57 27404
Raw data (/proc/27399/stat): 27399 (minisat+_script) S 27398 27399 2660 0 -1 0 314 2516 0 0 0 1 46 10 17 0 1 0 1854684993 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27399/statm): 532 234 485 147 0 385 0
[pid=27399] vsize: 2128
Raw data (/proc/27404/stat): 27404 (minisat+_bignum) R 27399 27399 2660 0 -1 0 52211 0 0 0 20390 232 0 0 25 0 1 0 1854685127 172630016 41789 4294967295 134512640 135167914 3221224448 3211230132 134845880 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27404/statm): 42146 41789 162 162 0 41984 0
[pid=27404] vsize: 168584
Current children cumulated CPU time (s) 206.79
Current children cumulated vsize (Kb) 170712

[startup+220.029 s]
Raw data (loadavg): 0.99 0.97 0.92 2/57 27404
Raw data (/proc/27399/stat): 27399 (minisat+_script) S 27398 27399 2660 0 -1 0 314 2516 0 0 0 1 46 10 17 0 1 0 1854684993 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27399/statm): 532 234 485 147 0 385 0
[pid=27399] vsize: 2128
Raw data (/proc/27404/stat): 27404 (minisat+_bignum) R 27399 27399 2660 0 -1 0 56842 0 0 0 21336 256 0 0 25 0 1 0 1854685127 191598592 46420 4294967295 134512640 135167914 3221224448 3211238592 134843118 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27404/statm): 46777 46420 162 162 0 46615 0
[pid=27404] vsize: 187108
Current children cumulated CPU time (s) 216.49
Current children cumulated vsize (Kb) 189236

[startup+230.03 s]
Raw data (loadavg): 0.99 0.97 0.92 2/57 27404
Raw data (/proc/27399/stat): 27399 (minisat+_script) S 27398 27399 2660 0 -1 0 314 2516 0 0 0 1 46 10 17 0 1 0 1854684993 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27399/statm): 532 234 485 147 0 385 0
[pid=27399] vsize: 2128
Raw data (/proc/27404/stat): 27404 (minisat+_bignum) R 27399 27399 2660 0 -1 0 61360 0 0 0 22283 277 0 0 25 0 1 0 1854685127 210104320 50938 4294967295 134512640 135167914 3221224448 3211232284 134722227 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27404/statm): 51295 50938 162 162 0 51133 0
[pid=27404] vsize: 205180
Current children cumulated CPU time (s) 226.17
Current children cumulated vsize (Kb) 207308

[startup+240.03 s]
Raw data (loadavg): 0.99 0.97 0.92 2/57 27404
Raw data (/proc/27399/stat): 27399 (minisat+_script) S 27398 27399 2660 0 -1 0 314 2516 0 0 0 1 46 10 17 0 1 0 1854684993 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27399/statm): 532 234 485 147 0 385 0
[pid=27399] vsize: 2128
Raw data (/proc/27404/stat): 27404 (minisat+_bignum) R 27399 27399 2660 0 -1 0 74258 0 0 0 23230 315 0 0 25 0 1 0 1854685127 241336320 58563 4294967295 134512640 135167914 3221224448 3211252048 134843001 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27404/statm): 58920 58563 162 162 0 58758 0
[pid=27404] vsize: 235680
Current children cumulated CPU time (s) 236.02
Current children cumulated vsize (Kb) 237808

[startup+250.031 s]
Raw data (loadavg): 0.99 0.97 0.92 2/57 27404
Raw data (/proc/27399/stat): 27399 (minisat+_script) S 27398 27399 2660 0 -1 0 314 2516 0 0 0 1 46 10 17 0 1 0 1854684993 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27399/statm): 532 234 485 147 0 385 0
[pid=27399] vsize: 2128
Raw data (/proc/27404/stat): 27404 (minisat+_bignum) R 27399 27399 2660 0 -1 0 78868 0 0 0 24181 337 0 0 19 0 1 0 1854685127 260218880 63173 4294967295 134512640 135167914 3221224448 3211230592 134849196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27404/statm): 63530 63173 162 162 0 63368 0
[pid=27404] vsize: 254120
Current children cumulated CPU time (s) 245.75
Current children cumulated vsize (Kb) 256248

[startup+260.032 s]
Raw data (loadavg): 0.99 0.97 0.92 2/57 27404
Raw data (/proc/27399/stat): 27399 (minisat+_script) S 27398 27399 2660 0 -1 0 314 2516 0 0 0 1 46 10 17 0 1 0 1854684993 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27399/statm): 532 234 485 147 0 385 0
[pid=27399] vsize: 2128
Raw data (/proc/27404/stat): 27404 (minisat+_bignum) R 27399 27399 2660 0 -1 0 83381 0 0 0 25130 358 0 0 25 0 1 0 1854685127 278704128 67686 4294967295 134512640 135167914 3221224448 3211235248 134623803 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27404/statm): 68043 67686 162 162 0 67881 0
[pid=27404] vsize: 272172
Current children cumulated CPU time (s) 255.45
Current children cumulated vsize (Kb) 274300

[startup+270.034 s]
Raw data (loadavg): 0.99 0.97 0.92 2/57 27404
Raw data (/proc/27399/stat): 27399 (minisat+_script) S 27398 27399 2660 0 -1 0 314 2516 0 0 0 1 46 10 17 0 1 0 1854684993 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27399/statm): 532 234 485 147 0 385 0
[pid=27399] vsize: 2128
Raw data (/proc/27404/stat): 27404 (minisat+_bignum) R 27399 27399 2660 0 -1 0 87838 0 0 0 26079 379 0 0 25 0 1 0 1854685127 296960000 72143 4294967295 134512640 135167914 3221224448 3211247360 134695961 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27404/statm): 72500 72143 162 162 0 72338 0
[pid=27404] vsize: 290000
Current children cumulated CPU time (s) 265.15
Current children cumulated vsize (Kb) 292128

[startup+280.034 s]
Raw data (loadavg): 0.99 0.97 0.92 2/57 27404
Raw data (/proc/27399/stat): 27399 (minisat+_script) S 27398 27399 2660 0 -1 0 314 2516 0 0 0 1 46 10 17 0 1 0 1854684993 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27399/statm): 532 234 485 147 0 385 0
[pid=27399] vsize: 2128
Raw data (/proc/27404/stat): 27404 (minisat+_bignum) T 27399 27399 2660 0 -1 0 92242 0 0 0 27027 402 0 0 25 0 1 0 1854685127 314998784 76547 4294967295 134512640 135167914 3221224448 3211230828 134934490 0 0 5 16386 3222434794 0 0 17 0 0 0
Raw data (/proc/27404/statm): 76904 76547 162 162 0 76742 0
[pid=27404] vsize: 307616
Current children cumulated CPU time (s) 274.86
Current children cumulated vsize (Kb) 309744

[startup+290.035 s]
Raw data (loadavg): 0.99 0.97 0.92 2/57 27404
Raw data (/proc/27399/stat): 27399 (minisat+_script) S 27398 27399 2660 0 -1 0 314 2516 0 0 0 1 46 10 17 0 1 0 1854684993 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27399/statm): 532 234 485 147 0 385 0
[pid=27399] vsize: 2128
Raw data (/proc/27404/stat): 27404 (minisat+_bignum) R 27399 27399 2660 0 -1 0 96606 0 0 0 27979 421 0 0 25 0 1 0 1854685127 332873728 80911 4294967295 134512640 135167914 3221224448 3211230976 134844676 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27404/statm): 81268 80911 162 162 0 81106 0
[pid=27404] vsize: 325072
Current children cumulated CPU time (s) 284.57
Current children cumulated vsize (Kb) 327200

[startup+300.036 s]
Raw data (loadavg): 0.99 0.97 0.92 2/57 27404
Raw data (/proc/27399/stat): 27399 (minisat+_script) S 27398 27399 2660 0 -1 0 314 2516 0 0 0 1 46 10 17 0 1 0 1854684993 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27399/statm): 532 234 485 147 0 385 0
[pid=27399] vsize: 2128
Raw data (/proc/27404/stat): 27404 (minisat+_bignum) R 27399 27399 2660 0 -1 0 100987 0 0 0 28930 443 0 0 25 0 1 0 1854685127 350818304 85292 4294967295 134512640 135167914 3221224448 3211252432 134844745 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27404/statm): 85649 85292 162 162 0 85487 0
[pid=27404] vsize: 342596
Current children cumulated CPU time (s) 294.3
Current children cumulated vsize (Kb) 344724

[startup+310.036 s]
Raw data (loadavg): 0.99 0.97 0.92 2/57 27404
Raw data (/proc/27399/stat): 27399 (minisat+_script) S 27398 27399 2660 0 -1 0 314 2516 0 0 0 1 46 10 17 0 1 0 1854684993 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27399/statm): 532 234 485 147 0 385 0
[pid=27399] vsize: 2128
Raw data (/proc/27404/stat): 27404 (minisat+_bignum) R 27399 27399 2660 0 -1 0 107856 0 0 0 29875 468 0 0 25 0 1 0 1854685127 454729728 92161 4294967295 134512640 135167914 3221224448 3211291776 134625368 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27404/statm): 111018 92161 162 162 0 110856 0
[pid=27404] vsize: 444072
Current children cumulated CPU time (s) 304
Current children cumulated vsize (Kb) 446200

[startup+320.038 s]
Raw data (loadavg): 0.99 0.97 0.92 2/57 27404
Raw data (/proc/27399/stat): 27399 (minisat+_script) S 27398 27399 2660 0 -1 0 314 2516 0 0 0 1 46 10 17 0 1 0 1854684993 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27399/statm): 532 234 485 147 0 385 0
[pid=27399] vsize: 2128
Raw data (/proc/27404/stat): 27404 (minisat+_bignum) R 27399 27399 2660 0 -1 0 126434 0 0 0 30830 511 0 0 25 0 1 0 1854685127 411852800 100193 4294967295 134512640 135167914 3221224448 3211290144 134845442 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27404/statm): 100550 100193 162 162 0 100388 0
[pid=27404] vsize: 402200
Current children cumulated CPU time (s) 313.98
Current children cumulated vsize (Kb) 404328

[startup+330.039 s]
Raw data (loadavg): 0.99 0.97 0.92 2/57 27404
Raw data (/proc/27399/stat): 27399 (minisat+_script) S 27398 27399 2660 0 -1 0 314 2516 0 0 0 1 46 10 17 0 1 0 1854684993 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27399/statm): 532 234 485 147 0 385 0
[pid=27399] vsize: 2128
Raw data (/proc/27404/stat): 27404 (minisat+_bignum) R 27399 27399 2660 0 -1 0 130901 0 0 0 31775 535 0 0 25 0 1 0 1854685127 430149632 104660 4294967295 134512640 135167914 3221224448 3211246816 134845760 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27404/statm): 105017 104660 162 162 0 104855 0
[pid=27404] vsize: 420068
Current children cumulated CPU time (s) 323.67
Current children cumulated vsize (Kb) 422196

[startup+340.04 s]
Raw data (loadavg): 0.99 0.97 0.92 2/57 27404
Raw data (/proc/27399/stat): 27399 (minisat+_script) S 27398 27399 2660 0 -1 0 314 2516 0 0 0 1 46 10 17 0 1 0 1854684993 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27399/statm): 532 234 485 147 0 385 0
[pid=27399] vsize: 2128
Raw data (/proc/27404/stat): 27404 (minisat+_bignum) R 27399 27399 2660 0 -1 0 135338 0 0 0 32723 554 0 0 25 0 1 0 1854685127 448323584 109097 4294967295 134512640 135167914 3221224448 3211229792 134722539 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27404/statm): 109454 109097 162 162 0 109292 0
[pid=27404] vsize: 437816
Current children cumulated CPU time (s) 333.34
Current children cumulated vsize (Kb) 439944

[startup+350.04 s]
Raw data (loadavg): 0.99 0.97 0.92 2/57 27404
Raw data (/proc/27399/stat): 27399 (minisat+_script) S 27398 27399 2660 0 -1 0 314 2516 0 0 0 1 46 10 17 0 1 0 1854684993 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27399/statm): 532 234 485 147 0 385 0
[pid=27399] vsize: 2128
Raw data (/proc/27404/stat): 27404 (minisat+_bignum) R 27399 27399 2660 0 -1 0 139766 0 0 0 33670 576 0 0 19 0 1 0 1854685127 466460672 113525 4294967295 134512640 135167914 3221224448 3211251872 134843400 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27404/statm): 113882 113525 162 162 0 113720 0
[pid=27404] vsize: 455528
Current children cumulated CPU time (s) 343.03
Current children cumulated vsize (Kb) 457656

[startup+360.042 s]
Raw data (loadavg): 0.99 0.97 0.92 2/57 27404
Raw data (/proc/27399/stat): 27399 (minisat+_script) S 27398 27399 2660 0 -1 0 314 2516 0 0 0 1 46 10 17 0 1 0 1854684993 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27399/statm): 532 234 485 147 0 385 0
[pid=27399] vsize: 2128
Raw data (/proc/27404/stat): 27404 (minisat+_bignum) R 27399 27399 2660 0 -1 0 144138 0 0 0 34623 596 0 0 25 0 1 0 1854685127 484368384 117897 4294967295 134512640 135167914 3221224448 3211246032 134845937 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27404/statm): 118254 117897 162 162 0 118092 0
[pid=27404] vsize: 473016
Current children cumulated CPU time (s) 352.76
Current children cumulated vsize (Kb) 475144

[startup+370.044 s]
Raw data (loadavg): 0.99 0.97 0.92 2/57 27404
Raw data (/proc/27399/stat): 27399 (minisat+_script) S 27398 27399 2660 0 -1 0 314 2516 0 0 0 1 46 10 17 0 1 0 1854684993 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27399/statm): 532 234 485 147 0 385 0
[pid=27399] vsize: 2128
Raw data (/proc/27404/stat): 27404 (minisat+_bignum) R 27399 27399 2660 0 -1 0 148505 0 0 0 35572 616 0 0 25 0 1 0 1854685127 502255616 122264 4294967295 134512640 135167914 3221224448 3211284440 134843032 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27404/statm): 122621 122264 162 162 0 122459 0
[pid=27404] vsize: 490484
Current children cumulated CPU time (s) 362.45
Current children cumulated vsize (Kb) 492612

[startup+380.045 s]
Raw data (loadavg): 0.99 0.97 0.92 2/57 27404
Raw data (/proc/27399/stat): 27399 (minisat+_script) S 27398 27399 2660 0 -1 0 314 2516 0 0 0 1 46 10 17 0 1 0 1854684993 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27399/statm): 532 234 485 147 0 385 0
[pid=27399] vsize: 2128
Raw data (/proc/27404/stat): 27404 (minisat+_bignum) R 27399 27399 2660 0 -1 0 152865 0 0 0 36522 639 0 0 25 0 1 0 1854685127 520114176 126624 4294967295 134512640 135167914 3221224448 3211284264 134846907 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27404/statm): 126981 126624 162 162 0 126819 0
[pid=27404] vsize: 507924
Current children cumulated CPU time (s) 372.18
Current children cumulated vsize (Kb) 510052

[startup+390.045 s]
Raw data (loadavg): 0.99 0.97 0.92 2/57 27404
Raw data (/proc/27399/stat): 27399 (minisat+_script) S 27398 27399 2660 0 -1 0 314 2516 0 0 0 1 46 10 17 0 1 0 1854684993 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27399/statm): 532 234 485 147 0 385 0
[pid=27399] vsize: 2128
Raw data (/proc/27404/stat): 27404 (minisat+_bignum) R 27399 27399 2660 0 -1 0 157211 0 0 0 37472 660 0 0 25 0 1 0 1854685127 537915392 130970 4294967295 134512640 135167914 3221224448 3211246716 134722225 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27404/statm): 131327 130970 162 162 0 131165 0
[pid=27404] vsize: 525308
Current children cumulated CPU time (s) 381.89
Current children cumulated vsize (Kb) 527436

[startup+400.047 s]
Raw data (loadavg): 0.99 0.97 0.92 2/57 27404
Raw data (/proc/27399/stat): 27399 (minisat+_script) S 27398 27399 2660 0 -1 0 314 2516 0 0 0 1 46 10 17 0 1 0 1854684993 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27399/statm): 532 234 485 147 0 385 0
[pid=27399] vsize: 2128
Raw data (/proc/27404/stat): 27404 (minisat+_bignum) R 27399 27399 2660 0 -1 0 161594 0 0 0 38422 681 0 0 25 0 1 0 1854685127 555868160 135353 4294967295 134512640 135167914 3221224448 3211242480 134845930 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27404/statm): 135710 135353 162 162 0 135548 0
[pid=27404] vsize: 542840
Current children cumulated CPU time (s) 391.6
Current children cumulated vsize (Kb) 544968

[startup+410.048 s]
Raw data (loadavg): 0.99 0.97 0.92 2/57 27404
Raw data (/proc/27399/stat): 27399 (minisat+_script) S 27398 27399 2660 0 -1 0 314 2516 0 0 0 1 46 10 17 0 1 0 1854684993 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27399/statm): 532 234 485 147 0 385 0
[pid=27399] vsize: 2128
Raw data (/proc/27404/stat): 27404 (minisat+_bignum) R 27399 27399 2660 0 -1 0 165931 0 0 0 39376 701 0 0 25 0 1 0 1854685127 573632512 139690 4294967295 134512640 135167914 3221224448 3211245552 134843113 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27404/statm): 140047 139690 162 162 0 139885 0
[pid=27404] vsize: 560188
Current children cumulated CPU time (s) 401.34
Current children cumulated vsize (Kb) 562316

[startup+420.048 s]
Raw data (loadavg): 0.99 0.97 0.92 2/57 27404
Raw data (/proc/27399/stat): 27399 (minisat+_script) S 27398 27399 2660 0 -1 0 314 2516 0 0 0 1 46 10 17 0 1 0 1854684993 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27399/statm): 532 234 485 147 0 385 0
[pid=27399] vsize: 2128
Raw data (/proc/27404/stat): 27404 (minisat+_bignum) R 27399 27399 2660 0 -1 0 170253 0 0 0 40322 726 0 0 25 0 1 0 1854685127 591335424 144012 4294967295 134512640 135167914 3221224448 3211253552 134849221 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27404/statm): 144369 144012 162 162 0 144207 0
[pid=27404] vsize: 577476
Current children cumulated CPU time (s) 411.05
Current children cumulated vsize (Kb) 579604

[startup+430.05 s]
Raw data (loadavg): 0.99 0.97 0.92 2/57 27404
Raw data (/proc/27399/stat): 27399 (minisat+_script) S 27398 27399 2660 0 -1 0 314 2516 0 0 0 1 46 10 17 0 1 0 1854684993 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27399/statm): 532 234 485 147 0 385 0
[pid=27399] vsize: 2128
Raw data (/proc/27404/stat): 27404 (minisat+_bignum) R 27399 27399 2660 0 -1 0 174579 0 0 0 41274 747 0 0 25 0 1 0 1854685127 609054720 148338 4294967295 134512640 135167914 3221224448 3211290992 134516638 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27404/statm): 148695 148338 162 162 0 148533 0
[pid=27404] vsize: 594780
Current children cumulated CPU time (s) 420.78
Current children cumulated vsize (Kb) 596908

[startup+440.051 s]
Raw data (loadavg): 0.99 0.97 0.92 2/57 27404
Raw data (/proc/27399/stat): 27399 (minisat+_script) S 27398 27399 2660 0 -1 0 314 2516 0 0 0 1 46 10 17 0 1 0 1854684993 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27399/statm): 532 234 485 147 0 385 0
[pid=27399] vsize: 2128
Raw data (/proc/27404/stat): 27404 (minisat+_bignum) R 27399 27399 2660 0 -1 0 178908 0 0 0 42224 769 0 0 25 0 1 0 1854685127 626786304 152667 4294967295 134512640 135167914 3221224448 3211263872 134694419 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27404/statm): 153024 152667 162 162 0 152862 0
[pid=27404] vsize: 612096
Current children cumulated CPU time (s) 430.5
Current children cumulated vsize (Kb) 614224

[startup+450.052 s]
Raw data (loadavg): 0.99 0.97 0.92 2/57 27404
Raw data (/proc/27399/stat): 27399 (minisat+_script) S 27398 27399 2660 0 -1 0 314 2516 0 0 0 1 46 10 17 0 1 0 1854684993 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27399/statm): 532 234 485 147 0 385 0
[pid=27399] vsize: 2128
Raw data (/proc/27404/stat): 27404 (minisat+_bignum) R 27399 27399 2660 0 -1 0 183224 0 0 0 43172 792 0 0 25 0 1 0 1854685127 644464640 156983 4294967295 134512640 135167914 3221224448 3211265196 134845882 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27404/statm): 157340 156983 162 162 0 157178 0
[pid=27404] vsize: 629360
Current children cumulated CPU time (s) 440.21
Current children cumulated vsize (Kb) 631488

[startup+460.052 s]
Raw data (loadavg): 0.99 0.97 0.92 2/57 27404
Raw data (/proc/27399/stat): 27399 (minisat+_script) S 27398 27399 2660 0 -1 0 314 2516 0 0 0 1 46 10 17 0 1 0 1854684993 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27399/statm): 532 234 485 147 0 385 0
[pid=27399] vsize: 2128
Raw data (/proc/27404/stat): 27404 (minisat+_bignum) R 27399 27399 2660 0 -1 0 187549 0 0 0 44121 814 0 0 25 0 1 0 1854685127 662179840 161308 4294967295 134512640 135167914 3221224448 3211229856 134695196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27404/statm): 161665 161308 162 162 0 161503 0
[pid=27404] vsize: 646660
Current children cumulated CPU time (s) 449.92
Current children cumulated vsize (Kb) 648788

[startup+470.054 s]
Raw data (loadavg): 0.99 0.97 0.92 2/57 27404
Raw data (/proc/27399/stat): 27399 (minisat+_script) S 27398 27399 2660 0 -1 0 314 2516 0 0 0 1 46 10 17 0 1 0 1854684993 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27399/statm): 532 234 485 147 0 385 0
[pid=27399] vsize: 2128
Raw data (/proc/27404/stat): 27404 (minisat+_bignum) R 27399 27399 2660 0 -1 0 232132 0 0 0 44998 923 0 0 25 0 1 0 1854685127 844791808 205891 4294967295 134512640 135167914 3221224448 3211265872 134845911 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27404/statm): 206248 205891 162 162 0 206086 0
[pid=27404] vsize: 824992
Current children cumulated CPU time (s) 459.78
Current children cumulated vsize (Kb) 827120

[startup+480.055 s]
Raw data (loadavg): 0.99 0.97 0.92 2/57 27404
Raw data (/proc/27399/stat): 27399 (minisat+_script) S 27398 27399 2660 0 -1 0 314 2516 0 0 0 1 46 10 17 0 1 0 1854684993 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27399/statm): 532 234 485 147 0 385 0
[pid=27399] vsize: 2128
Raw data (/proc/27404/stat): 27404 (minisat+_bignum) R 27399 27399 2660 0 -1 0 232132 0 0 0 45999 923 0 0 25 0 1 0 1854685127 844791808 205891 4294967295 134512640 135167914 3221224448 3211266016 134625423 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27404/statm): 206248 205891 162 162 0 206086 0
[pid=27404] vsize: 824992
Current children cumulated CPU time (s) 469.79
Current children cumulated vsize (Kb) 827120

[startup+490.055 s]
Raw data (loadavg): 0.99 0.97 0.92 2/57 27404
Raw data (/proc/27399/stat): 27399 (minisat+_script) S 27398 27399 2660 0 -1 0 314 2516 0 0 0 1 46 10 17 0 1 0 1854684993 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27399/statm): 532 234 485 147 0 385 0
[pid=27399] vsize: 2128
Raw data (/proc/27404/stat): 27404 (minisat+_bignum) T 27399 27399 2660 0 -1 0 234251 0 0 0 46971 935 0 0 17 0 1 0 1854685127 767082496 186919 4294967295 134512640 135167914 3221224448 3211231772 134934490 0 0 5 16386 3222434794 0 0 17 0 0 0
Raw data (/proc/27404/statm): 187276 186919 162 162 0 187114 0
[pid=27404] vsize: 749104
Current children cumulated CPU time (s) 479.63
Current children cumulated vsize (Kb) 751232

[startup+500.056 s]
Raw data (loadavg): 0.99 0.97 0.92 2/57 27404
Raw data (/proc/27399/stat): 27399 (minisat+_script) S 27398 27399 2660 0 -1 0 314 2516 0 0 0 1 46 10 17 0 1 0 1854684993 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27399/statm): 532 234 485 147 0 385 0
[pid=27399] vsize: 2128
Raw data (/proc/27404/stat): 27404 (minisat+_bignum) R 27399 27399 2660 0 -1 0 238754 0 0 0 47923 954 0 0 25 0 1 0 1854685127 785526784 191422 4294967295 134512640 135167914 3221224448 3211231164 134722512 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27404/statm): 191779 191422 162 162 0 191617 0
[pid=27404] vsize: 767116
Current children cumulated CPU time (s) 489.34
Current children cumulated vsize (Kb) 769244

[startup+510.057 s]
Raw data (loadavg): 0.99 0.97 0.92 2/57 27404
Raw data (/proc/27399/stat): 27399 (minisat+_script) S 27398 27399 2660 0 -1 0 314 2516 0 0 0 1 46 10 17 0 1 0 1854684993 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27399/statm): 532 234 485 147 0 385 0
[pid=27399] vsize: 2128
Raw data (/proc/27404/stat): 27404 (minisat+_bignum) R 27399 27399 2660 0 -1 0 243255 0 0 0 48873 976 0 0 25 0 1 0 1854685127 803962880 195923 4294967295 134512640 135167914 3221224448 3211249884 134843033 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27404/statm): 196280 195923 162 162 0 196118 0
[pid=27404] vsize: 785120
Current children cumulated CPU time (s) 499.06
Current children cumulated vsize (Kb) 787248

[startup+520.058 s]
Raw data (loadavg): 0.99 0.97 0.92 2/57 27404
Raw data (/proc/27399/stat): 27399 (minisat+_script) S 27398 27399 2660 0 -1 0 314 2516 0 0 0 1 46 10 17 0 1 0 1854684993 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27399/statm): 532 234 485 147 0 385 0
[pid=27399] vsize: 2128
Raw data (/proc/27404/stat): 27404 (minisat+_bignum) R 27399 27399 2660 0 -1 0 247748 0 0 0 49822 999 0 0 25 0 1 0 1854685127 822366208 200416 4294967295 134512640 135167914 3221224448 3211269340 134722227 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27404/statm): 200773 200416 162 162 0 200611 0
[pid=27404] vsize: 803092
Current children cumulated CPU time (s) 508.78
Current children cumulated vsize (Kb) 805220

[startup+530.058 s]
Raw data (loadavg): 0.99 0.97 0.92 2/57 27404
Raw data (/proc/27399/stat): 27399 (minisat+_script) S 27398 27399 2660 0 -1 0 314 2516 0 0 0 1 46 10 17 0 1 0 1854684993 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27399/statm): 532 234 485 147 0 385 0
[pid=27399] vsize: 2128
Raw data (/proc/27404/stat): 27404 (minisat+_bignum) R 27399 27399 2660 0 -1 0 252229 0 0 0 50769 1024 0 0 25 0 1 0 1854685127 840720384 204897 4294967295 134512640 135167914 3221224448 3211284448 134849538 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27404/statm): 205254 204897 162 162 0 205092 0
[pid=27404] vsize: 821016
Current children cumulated CPU time (s) 518.5
Current children cumulated vsize (Kb) 823144

[startup+540.059 s]
Raw data (loadavg): 0.99 0.97 0.92 2/57 27404
Raw data (/proc/27399/stat): 27399 (minisat+_script) S 27398 27399 2660 0 -1 0 314 2516 0 0 0 1 46 10 17 0 1 0 1854684993 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27399/statm): 532 234 485 147 0 385 0
[pid=27399] vsize: 2128
Raw data (/proc/27404/stat): 27404 (minisat+_bignum) R 27399 27399 2660 0 -1 0 256527 0 0 0 51718 1045 0 0 25 0 1 0 1854685127 858324992 209195 4294967295 134512640 135167914 3221224448 3211234160 134722527 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27404/statm): 209552 209195 162 162 0 209390 0
[pid=27404] vsize: 838208
Current children cumulated CPU time (s) 528.2
Current children cumulated vsize (Kb) 840336

[startup+550.061 s]
Raw data (loadavg): 0.99 0.97 0.92 2/57 27404
Raw data (/proc/27399/stat): 27399 (minisat+_script) S 27398 27399 2660 0 -1 0 314 2516 0 0 0 1 46 10 17 0 1 0 1854684993 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27399/statm): 532 234 485 147 0 385 0
[pid=27399] vsize: 2128
Raw data (/proc/27404/stat): 27404 (minisat+_bignum) R 27399 27399 2660 0 -1 0 260492 0 0 0 52669 1067 0 0 25 0 1 0 1854685127 874565632 213160 4294967295 134512640 135167914 3221224448 3211452936 134846971 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27404/statm): 213517 213160 162 162 0 213355 0
[pid=27404] vsize: 854068
Current children cumulated CPU time (s) 537.93
Current children cumulated vsize (Kb) 856196

[startup+560.062 s]
Raw data (loadavg): 0.99 0.97 0.92 2/57 27404
Raw data (/proc/27399/stat): 27399 (minisat+_script) S 27398 27399 2660 0 -1 0 314 2516 0 0 0 1 46 10 17 0 1 0 1854684993 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27399/statm): 532 234 485 147 0 385 0
[pid=27399] vsize: 2128
Raw data (/proc/27404/stat): 27404 (minisat+_bignum) R 27399 27399 2660 0 -1 0 264336 0 0 0 53624 1086 0 0 25 0 1 0 1854685127 890310656 217004 4294967295 134512640 135167914 3221224448 3211431772 134695741 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27404/statm): 217361 217004 162 162 0 217199 0
[pid=27404] vsize: 869444
Current children cumulated CPU time (s) 547.67
Current children cumulated vsize (Kb) 871572

[startup+570.063 s]
Raw data (loadavg): 0.99 0.97 0.92 2/57 27404
Raw data (/proc/27399/stat): 27399 (minisat+_script) S 27398 27399 2660 0 -1 0 314 2516 0 0 0 1 46 10 17 0 1 0 1854684993 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27399/statm): 532 234 485 147 0 385 0
[pid=27399] vsize: 2128
Raw data (/proc/27404/stat): 27404 (minisat+_bignum) R 27399 27399 2660 0 -1 0 268271 0 0 0 54577 1106 0 0 25 0 1 0 1854685127 906428416 220939 4294967295 134512640 135167914 3221224448 3211229916 134722225 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27404/statm): 221296 220939 162 162 0 221134 0
[pid=27404] vsize: 885184
Current children cumulated CPU time (s) 557.4
Current children cumulated vsize (Kb) 887312

[startup+580.064 s]
Raw data (loadavg): 0.99 0.97 0.92 2/57 27404
Raw data (/proc/27399/stat): 27399 (minisat+_script) S 27398 27399 2660 0 -1 0 314 2516 0 0 0 1 46 10 17 0 1 0 1854684993 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27399/statm): 532 234 485 147 0 385 0
[pid=27399] vsize: 2128
Raw data (/proc/27404/stat): 27404 (minisat+_bignum) T 27399 27399 2660 0 -1 0 272896 0 62 0 55432 1132 0 0 18 0 1 0 1854685127 924758016 224461 4294967295 134512640 135167914 3221224448 3211230012 134934490 0 0 5 16386 3222434794 0 0 17 0 0 0
Raw data (/proc/27404/statm): 225771 224461 162 162 0 225609 0
[pid=27404] vsize: 903084
Current children cumulated CPU time (s) 566.21
Current children cumulated vsize (Kb) 905212

[startup+590.065 s]
Raw data (loadavg): 1.07 0.99 0.93 2/57 27404
Raw data (/proc/27399/stat): 27399 (minisat+_script) S 27398 27399 2660 0 -1 0 314 2516 0 0 0 1 46 10 17 0 1 0 1854684993 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27399/statm): 532 234 485 147 0 385 0
[pid=27399] vsize: 2128
Raw data (/proc/27404/stat): 27404 (minisat+_bignum) T 27399 27399 2660 0 -1 0 276513 0 424 0 55960 1150 0 0 18 0 1 0 1854685127 935600128 226490 4294967295 134512640 135167914 3221224448 3211230684 134934490 0 0 5 16386 3222434794 0 0 17 0 0 0
Raw data (/proc/27404/statm): 228418 226490 162 162 0 228256 0
[pid=27404] vsize: 913672
Current children cumulated CPU time (s) 571.67
Current children cumulated vsize (Kb) 915800



Mem limit exceeded: sending SIGTERM then SIGKILL

[startup+595.037 s]
Raw data (loadavg): 1.06 0.99 0.93 1/57 27404
Raw data (/proc/27399/stat): 27399 (minisat+_script) S 27398 27399 2660 0 -1 0 314 2516 0 0 0 1 46 10 17 0 1 0 1854684993 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27399/statm): 532 234 485 147 0 385 0
[pid=27399] vsize: 2128
Raw data (/proc/27404/stat): 27404 (minisat+_bignum) T 27399 27399 2660 0 -1 0 278420 0 553 0 56244 1158 0 0 19 0 1 0 1854685127 941543424 226607 4294967295 134512640 135167914 3221224448 3211229260 134934490 0 0 5 16386 3222434794 0 0 17 0 0 0
Raw data (/proc/27404/statm): 229869 226607 162 162 0 229707 0
[pid=27404] vsize: 919476
Current children cumulated CPU time (s) 574.59
Current children cumulated vsize (Kb) 921604

Sending SIGTERM to -27399
Sleeping 2 seconds
One traced child (pid=27399) ended because it received signal 15 (SIGTERM)
One traced child (pid=27404) exited with status: 0
All traced children have exited ! Game is over.

Child status: 0
Real time (s): 595.482
CPU time (s): 574.454
CPU user time (s): 562.442
CPU system time (s): 12.0122
CPU usage (%): 96.4686
Max. virtual memory (cumulated for all children) (Kb): 921604

Verifier Data

ERROR: no interpretation found !