PB'05 competition: run trace

Some explanations

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

Name	normalized-opb/mps-v2-20-10/plato.asu.edu/pub/unibo/normalized-mps-v2-20-10-usAbbrv.8.25_70.opb
MD5SUM	7f148daab2a076d0407e04408057198b
Bench Category	optimization, big integers (OPTBIGINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	204800
Optimality of the best value was proved	NO
Number of terms in the objective function	135
Biggest coefficient in the objective function	536870912
Number of bits for the biggest coefficient in the objective function	30
Sum of the numbers in the objective function	1073849343
Number of bits of the sum of numbers in the objective function	31
Biggest number in a constraint	1024000000
Number of bits of the biggest number in a constraint	30
Biggest sum of numbers in a constraint	2147557374
Number of bits of the biggest sum of numbers	32
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	1201.26
Number of variables	20611
Total number of constraints	5602
Number of constraints which are clauses	563
Number of constraints which are cardinality constraints (but not clauses)	1681
Number of constraints which are nor clauses,nor cardinality constraints	3358
Minimum length of a constraint	1
Maximum length of a constraint	61
Trace number 31004

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

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

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        890980 kB
Buffers:          7332 kB
Cached:         116136 kB
SwapCached:        768 kB
Active:          42640 kB
Inactive:        82888 kB
HighTotal:      131008 kB
HighFree:        12460 kB
LowTotal:       903652 kB
LowFree:        878520 kB
SwapTotal:     2097136 kB
SwapFree:      2095468 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           5036 kB
Slab:            12380 kB
Committed_AS:    63604 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-05-25 21:38:02 (client local time) WITH STATUS 152 IN 1229.88 SECONDS
stats: 22363 7 1229.88 152
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 3922 PB-constraints to clauses...
c   -- Unit propagations: pppp
c   -- Detecting intervals from adjacent constraints: ######################################################################################################################################################################
c   -- Clauses(.)/Splits(s): ssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssss...................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................
c ---[3916]---> BDD-cost:  119
c ---[3915]---> BDD-cost:   88
c ---[3914]---> BDD-cost:   88
c ---[3913]---> BDD-cost:   88
c ---[3912]---> BDD-cost:   88
c ---[3911]---> BDD-cost:  117
c ---[3910]---> BDD-cost:  119
c ---[3909]---> BDD-cost:   88
c ---[3908]---> BDD-cost:   88
c ---[3907]---> BDD-cost:   88
c ---[3905]---> BDD-cost:   88
c ---[3904]---> BDD-cost:  125
c ---[3903]---> BDD-cost:  119
c ---[3902]---> BDD-cost:   88
c ---[3901]---> BDD-cost:   88
c ---[3900]---> BDD-cost:   88
c ---[3899]---> BDD-cost:   88
c ---[3898]---> BDD-cost:  123
c ---[3897]---> BDD-cost:  119
c ---[3896]---> BDD-cost:   88
c ---[3894]---> BDD-cost:   88
c ---[3893]---> BDD-cost:   88
c ---[3892]---> BDD-cost:   88
c ---[3891]---> BDD-cost:  117
c ---[3890]---> BDD-cost:  119
c ---[3889]---> BDD-cost:   88
c ---[3888]---> BDD-cost:   88
c ---[3887]---> BDD-cost:   88
c ---[3886]---> BDD-cost:   88
c ---[3885]---> BDD-cost:  125
c ---[3883]---> BDD-cost:  119
c ---[3882]---> BDD-cost:   88
c ---[3881]---> BDD-cost:   88
c ---[3880]---> BDD-cost:   88
c ---[3879]---> BDD-cost:   88
c ---[3878]---> BDD-cost:  125
c ---[3877]---> BDD-cost:  119
c ---[3876]---> BDD-cost:   88
c ---[3875]---> BDD-cost:   88
c ---[3874]---> BDD-cost:   88
c ---[3872]---> BDD-cost:   88
c ---[3871]---> BDD-cost:  117
c ---[3870]---> BDD-cost:  119
c ---[3869]---> BDD-cost:   88
c ---[3868]---> BDD-cost:   88
c ---[3867]---> BDD-cost:   88
c ---[3866]---> BDD-cost:   88
c ---[3865]---> BDD-cost:  121
c ---[3864]---> BDD-cost:  119
c ---[3863]---> BDD-cost:   88
c ---[3861]---> BDD-cost:   88
c ---[3860]---> BDD-cost:   88
c ---[3859]---> BDD-cost:   88
c ---[3858]---> BDD-cost:  117
c ---[3857]---> BDD-cost:  119
c ---[3856]---> BDD-cost:   88
c ---[3855]---> BDD-cost:   88
c ---[3854]---> BDD-cost:   88
c ---[3853]---> BDD-cost:   88
c ---[3852]---> BDD-cost:  125
c ---[3850]---> BDD-cost:  119
c ---[3849]---> BDD-cost:   88
c ---[3848]---> BDD-cost:   88
c ---[3847]---> BDD-cost:   88
c ---[3846]---> BDD-cost:   88
c ---[3845]---> BDD-cost:  117
c ---[3844]---> BDD-cost:  119
c ---[3843]---> BDD-cost:   88
c ---[3842]---> BDD-cost:   88
c ---[3841]---> BDD-cost:   88
c ---[3839]---> BDD-cost:   88
c ---[3838]---> BDD-cost:  125
c ---[3837]---> BDD-cost:  119
c ---[3836]---> BDD-cost:   88
c ---[3835]---> BDD-cost:   88
c ---[3834]---> BDD-cost:   88
c ---[3833]---> BDD-cost:   88
c ---[3832]---> BDD-cost:  125
c ---[3831]---> BDD-cost:  119
c ---[3830]---> BDD-cost:   88
c ---[3828]---> BDD-cost:   88
c ---[3827]---> BDD-cost:   88
c ---[3826]---> BDD-cost:   88
c ---[3825]---> BDD-cost:  125
c ---[3824]---> BDD-cost:  119
c ---[3823]---> BDD-cost:   88
c ---[3822]---> BDD-cost:   88
c ---[3821]---> BDD-cost:   88
c ---[3820]---> BDD-cost:   88
c ---[3819]---> BDD-cost:  117
c ---[3817]---> BDD-cost:  119
c ---[3816]---> BDD-cost:   88
c ---[3815]---> BDD-cost:   88
c ---[3814]---> BDD-cost:   88
c ---[3813]---> BDD-cost:   88
c ---[3812]---> BDD-cost:  125
c ---[3811]---> BDD-cost:  119
c ---[3810]---> BDD-cost:   88
c ---[3809]---> BDD-cost:   88
c ---[3808]---> BDD-cost:   88
c ---[3805]---> BDD-cost:   88
c ---[3804]---> BDD-cost:  125
c ---[3803]---> BDD-cost:  119
c ---[3802]---> BDD-cost:   88
c ---[3801]---> BDD-cost:   88
c ---[3800]---> BDD-cost:   88
c ---[3799]---> BDD-cost:   88
c ---[3798]---> BDD-cost:  125
c ---[3797]---> BDD-cost:  119
c ---[3796]---> BDD-cost:   88
c ---[3794]---> BDD-cost:   88
c ---[3793]---> BDD-cost:   88
c ---[3792]---> BDD-cost:   88
c ---[3791]---> BDD-cost:  117
c ---[3790]---> BDD-cost:  119
c ---[3789]---> BDD-cost:   88
c ---[3788]---> BDD-cost:   88
c ---[3787]---> BDD-cost:   88
c ---[3786]---> BDD-cost:   88
c ---[3785]---> BDD-cost:  117
c ---[3783]---> BDD-cost:  119
c ---[3782]---> BDD-cost:   88
c ---[3781]---> BDD-cost:   88
c ---[3780]---> BDD-cost:   88
c ---[3779]---> BDD-cost:   88
c ---[3778]---> BDD-cost:  117
c ---[3777]---> BDD-cost:  119
c ---[3776]---> BDD-cost:   88
c ---[3775]---> BDD-cost:   88
c ---[3774]---> BDD-cost:   88
c ---[3772]---> BDD-cost:   88
c ---[3771]---> BDD-cost:  123
c ---[3770]---> BDD-cost:  119
c ---[3769]---> BDD-cost:   88
c ---[3768]---> BDD-cost:   88
c ---[3767]---> BDD-cost:   88
c ---[3766]---> BDD-cost:   88
c ---[3765]---> BDD-cost:  125
c ---[3764]---> BDD-cost:  119
c ---[3763]---> BDD-cost:   88
c ---[3761]---> BDD-cost:   88
c ---[3760]---> BDD-cost:   88
c ---[3759]---> BDD-cost:   88
c ---[3758]---> BDD-cost:  125
c ---[3757]---> BDD-cost:  119
c ---[3756]---> BDD-cost:   88
c ---[3755]---> BDD-cost:   88
c ---[3754]---> BDD-cost:   88
c ---[3753]---> BDD-cost:   88
c ---[3752]---> BDD-cost:  117
c ---[3750]---> BDD-cost:  119
c ---[3749]---> BDD-cost:   88
c ---[3748]---> BDD-cost:   88
c ---[3747]---> BDD-cost:   88
c ---[3746]---> BDD-cost:   88
c ---[3745]---> BDD-cost:  117
c ---[3744]---> BDD-cost:  119
c ---[3743]---> BDD-cost:   88
c ---[3742]---> BDD-cost:   88
c ---[3741]---> BDD-cost:   88
c ---[3739]---> BDD-cost:   88
c ---[3738]---> BDD-cost:  125
c ---[3737]---> BDD-cost:  119
c ---[3736]---> BDD-cost:   88
c ---[3735]---> BDD-cost:   88
c ---[3734]---> BDD-cost:   88
c ---[3733]---> BDD-cost:   88
c ---[3732]---> BDD-cost:  117
c ---[3731]---> BDD-cost:  119
c ---[3730]---> BDD-cost:   88
c ---[3728]---> BDD-cost:   88
c ---[3727]---> BDD-cost:   88
c ---[3726]---> BDD-cost:   88
c ---[3725]---> BDD-cost:  125
c ---[3724]---> BDD-cost:  119
c ---[3723]---> BDD-cost:   88
c ---[3722]---> BDD-cost:   88
c ---[3721]---> BDD-cost:   88
c ---[3720]---> BDD-cost:   88
c ---[3719]---> BDD-cost:  117
c ---[3717]---> BDD-cost:  119
c ---[3716]---> BDD-cost:   88
c ---[3715]---> BDD-cost:   88
c ---[3714]---> BDD-cost:   88
c ---[3713]---> BDD-cost:   88
c ---[3712]---> BDD-cost:  117
c ---[3711]---> BDD-cost:  119
c ---[3710]---> BDD-cost:   88
c ---[3709]---> BDD-cost:   88
c ---[3708]---> BDD-cost:   88
c ---[3706]---> BDD-cost:   88
c ---[3705]---> BDD-cost:  125
c ---[3704]---> BDD-cost:  119
c ---[3703]---> BDD-cost:   88
c ---[3702]---> BDD-cost:   88
c ---[3701]---> BDD-cost:   88
c ---[3700]---> BDD-cost:   88
c ---[3699]---> BDD-cost:  123
c ---[3698]---> BDD-cost:  119
c ---[3697]---> BDD-cost:   88
c ---[3694]---> BDD-cost:   88
c ---[3693]---> BDD-cost:   88
c ---[3692]---> BDD-cost:   88
c ---[3691]---> BDD-cost:  123
c ---[3690]---> BDD-cost:  119
c ---[3689]---> BDD-cost:   88
c ---[3688]---> BDD-cost:   88
c ---[3687]---> BDD-cost:   88
c ---[3686]---> BDD-cost:   88
c ---[3685]---> BDD-cost:  117
c ---[3683]---> BDD-cost:  119
c ---[3682]---> BDD-cost:   88
c ---[3681]---> BDD-cost:   88
c ---[3680]---> BDD-cost:   88
c ---[3679]---> BDD-cost:   88
c ---[3678]---> BDD-cost:  123
c ---[3677]---> BDD-cost:  119
c ---[3676]---> BDD-cost:   88
c ---[3675]---> BDD-cost:   88
c ---[3674]---> BDD-cost:   88
c ---[3672]---> BDD-cost:   88
c ---[3671]---> BDD-cost:  125
c ---[3670]---> BDD-cost:  119
c ---[3669]---> BDD-cost:   88
c ---[3668]---> BDD-cost:   88
c ---[3667]---> BDD-cost:   88
c ---[3666]---> BDD-cost:   88
c ---[3665]---> BDD-cost:  117
c ---[3664]---> BDD-cost:  119
c ---[3663]---> BDD-cost:   88
c ---[3661]---> BDD-cost:   88
c ---[3660]---> BDD-cost:   88
c ---[3659]---> BDD-cost:   88
c ---[3658]---> BDD-cost:  125
c ---[3657]---> BDD-cost:  119
c ---[3656]---> BDD-cost:   88
c ---[3655]---> BDD-cost:   88
c ---[3654]---> BDD-cost:   88
c ---[3653]---> BDD-cost:   88
c ---[3652]---> BDD-cost:  125
c ---[3650]---> BDD-cost:  119
c ---[3649]---> BDD-cost:   88
c ---[3648]---> BDD-cost:   88
c ---[3647]---> BDD-cost:   88
c ---[3646]---> BDD-cost:   88
c ---[3645]---> BDD-cost:  117
c ---[3644]---> BDD-cost:  119
c ---[3643]---> BDD-cost:   88
c ---[3642]---> BDD-cost:   88
c ---[3641]---> BDD-cost:   88
c ---[3639]---> BDD-cost:   88
c ---[3638]---> BDD-cost:  125
c ---[3637]---> BDD-cost:  119
c ---[3636]---> BDD-cost:   88
c ---[3635]---> BDD-cost:   88
c ---[3634]---> BDD-cost:   88
c ---[3633]---> BDD-cost:   88
c ---[3632]---> BDD-cost:  125
c ---[3631]---> BDD-cost:  119
c ---[3630]---> BDD-cost:   88
c ---[3628]---> BDD-cost:   88
c ---[3627]---> BDD-cost:   88
c ---[3626]---> BDD-cost:   88
c ---[3625]---> BDD-cost:  117
c ---[3624]---> BDD-cost:  119
c ---[3623]---> BDD-cost:   88
c ---[3622]---> BDD-cost:   88
c ---[3621]---> BDD-cost:   88
c ---[3620]---> BDD-cost:   88
c ---[3619]---> BDD-cost:  125
c ---[3617]---> BDD-cost:  119
c ---[3616]---> BDD-cost:   88
c ---[3615]---> BDD-cost:   88
c ---[3614]---> BDD-cost:   88
c ---[3613]---> BDD-cost:   88
c ---[3612]---> BDD-cost:  125
c ---[3611]---> BDD-cost:  119
c ---[3610]---> BDD-cost:   88
c ---[3609]---> BDD-cost:   88
c ---[3608]---> BDD-cost:   88
c ---[3606]---> BDD-cost:   88
c ---[3605]---> BDD-cost:  125
c ---[3604]---> BDD-cost:  119
c ---[3603]---> BDD-cost:   88
c ---[3602]---> BDD-cost:   88
c ---[3601]---> BDD-cost:   88
c ---[3600]---> BDD-cost:   88
c ---[3599]---> BDD-cost:  125
c ---[3598]---> BDD-cost:  119
c ---[3597]---> BDD-cost:   88
c ---[3595]---> BDD-cost:   88
c ---[3594]---> BDD-cost:   88
c ---[3593]---> BDD-cost:   88
c ---[3592]---> BDD-cost:  125
c ---[3591]---> BDD-cost:  119
c ---[3590]---> BDD-cost:   88
c ---[3589]---> BDD-cost:   88
c ---[3588]---> BDD-cost:   88
c ---[3587]---> BDD-cost:   88
c ---[3586]---> BDD-cost:  121
c ---[3583]---> BDD-cost:  121
c ---[3581]---> BDD-cost:  125
c ---[3579]---> BDD-cost:  123
c ---[3577]---> BDD-cost:   88
c ---[3575]---> BDD-cost:  125
c ---[3574]---> BDD-cost:  125
c ---[3572]---> BDD-cost:  125
c ---[3570]---> BDD-cost:  125
c ---[3568]---> BDD-cost:   88
c ---[3566]---> BDD-cost:  125
c ---[3564]---> BDD-cost:   88
c ---[3563]---> BDD-cost:  125
c ---[3561]---> BDD-cost:  125
c ---[3559]---> BDD-cost:  123
c ---[3557]---> BDD-cost:   88
c ---[3555]---> BDD-cost:  123
c ---[3553]---> BDD-cost:   88
c ---[3552]---> BDD-cost:  125
c ---[3550]---> BDD-cost:  125
c ---[3548]---> BDD-cost:   88
c ---[3546]---> BDD-cost:  123
c ---[3544]---> BDD-cost:   88
c ---[3542]---> BDD-cost:  125
c ---[3541]---> BDD-cost:   88
c ---[3539]---> BDD-cost:   88
c ---[3537]---> BDD-cost:  125
c ---[3535]---> BDD-cost:  121
c ---[3533]---> BDD-cost:   88
c ---[3531]---> BDD-cost:  125
c ---[3530]---> BDD-cost:  125
c ---[3528]---> BDD-cost:  125
c ---[3526]---> BDD-cost:  125
c ---[3524]---> BDD-cost:  123
c ---[3522]---> BDD-cost:  125
c ---[3520]---> BDD-cost:   88
c ---[3519]---> BDD-cost:  125
c ---[3517]---> BDD-cost:  125
c ---[3515]---> BDD-cost:  125
c ---[3513]---> BDD-cost:  125
c ---[3511]---> BDD-cost:   88
c ---[3509]---> BDD-cost:  123
c ---[3508]---> BDD-cost:  125
c ---[3506]---> BDD-cost:  125
c ---[3504]---> BDD-cost:  125
c ---[3502]---> BDD-cost:  125
c ---[3500]---> BDD-cost:  125
c ---[3498]---> BDD-cost:  123
c ---[3497]---> BDD-cost:  125
c ---[3495]---> BDD-cost:  125
c ---[3493]---> BDD-cost:  125
c ---[3491]---> BDD-cost:  125
c ---[3489]---> BDD-cost:  123
c ---[3487]---> BDD-cost:  125
c ---[3486]---> BDD-cost:  125
c ---[3484]---> BDD-cost:  125
c ---[3482]---> BDD-cost:  125
c ---[3480]---> BDD-cost:  125
c ---[3478]---> BDD-cost:  125
c ---[3476]---> BDD-cost:  125
c ---[3475]---> BDD-cost:  123
c ---[3472]---> BDD-cost:  123
c ---[3470]---> BDD-cost:  123
c ---[3468]---> BDD-cost:  125
c ---[3466]---> BDD-cost:  125
c ---[3464]---> BDD-cost:  125
c ---[3463]---> BDD-cost:  125
c ---[3461]---> BDD-cost:  125
c ---[3459]---> BDD-cost:  125
c ---[3457]---> BDD-cost:  125
c ---[3455]---> BDD-cost:  125
c ---[3453]---> BDD-cost:  125
c ---[3452]---> BDD-cost:   88
c ---[3450]---> BDD-cost:   88
c ---[3448]---> BDD-cost:  125
c ---[3446]---> BDD-cost:  123
c ---[3444]---> BDD-cost:   88
c ---[3442]---> BDD-cost:   88
c ---[3441]---> BDD-cost:  123
c ---[3439]---> BDD-cost:  123
c ---[3437]---> BDD-cost:   88
c ---[3435]---> BDD-cost:  125
c ---[3433]---> BDD-cost:  125
c ---[3431]---> BDD-cost:  123
c ---[3430]---> BDD-cost:   88
c ---[3428]---> BDD-cost:   88
c ---[3426]---> BDD-cost:  123
c ---[3424]---> BDD-cost:  125
c ---[3422]---> BDD-cost:  125
c ---[3420]---> BDD-cost:  125
c ---[3419]---> BDD-cost:  123
c ---[3417]---> BDD-cost:  123
c ---[3415]---> BDD-cost:   88
c ---[3413]---> BDD-cost:   88
c ---[3411]---> BDD-cost:  125
c ---[3409]---> BDD-cost:  125
c ---[3408]---> BDD-cost:  123
c ---[3406]---> BDD-cost:  123
c ---[3404]---> BDD-cost:  125
c ---[3402]---> BDD-cost:  125
c ---[3400]---> BDD-cost:  125
c ---[3398]---> BDD-cost:  125
c ---[3397]---> BDD-cost:   88
c ---[3395]---> BDD-cost:   88
c ---[3393]---> BDD-cost:  123
c ---[3391]---> BDD-cost:   88
c ---[3389]---> BDD-cost:  125
c ---[3387]---> BDD-cost:  125
c ---[3386]---> BDD-cost:  125
c ---[3384]---> BDD-cost:  125
c ---[3382]---> BDD-cost:  121
c ---[3380]---> BDD-cost:  123
c ---[3378]---> BDD-cost:  123
c ---[3376]---> BDD-cost:  125
c ---[3375]---> BDD-cost:  125
c ---[3373]---> BDD-cost:  125
c ---[3371]---> BDD-cost:  125
c ---[3369]---> BDD-cost:  125
c ---[3367]---> BDD-cost:  125
c ---[3365]---> BDD-cost:  125
c ---[3364]---> BDD-cost:  123
c ---[3361]---> BDD-cost:  123
c ---[3359]---> BDD-cost:  125
c ---[3357]---> BDD-cost:  125
c ---[3355]---> BDD-cost:  125
c ---[3353]---> BDD-cost:  125
c ---[3352]---> BDD-cost:  125
c ---[3350]---> BDD-cost:  125
c ---[3348]---> BDD-cost:  125
c ---[3346]---> BDD-cost:  125
c ---[3344]---> BDD-cost:   88
c ---[3342]---> BDD-cost:   88
c ---[3341]---> BDD-cost:  125
c ---[3339]---> BDD-cost:  125
c ---[3337]---> BDD-cost:   88
c ---[3335]---> BDD-cost:  123
c ---[3333]---> BDD-cost:  125
c ---[3331]---> BDD-cost:  125
c ---[3330]---> BDD-cost:  125
c ---[3328]---> BDD-cost:  125
c ---[3326]---> BDD-cost:  123
c ---[3324]---> BDD-cost:  125
c ---[3322]---> BDD-cost:  125
c ---[3320]---> BDD-cost:   88
c ---[3319]---> BDD-cost:  125
c ---[3317]---> BDD-cost:  125
c ---[3315]---> BDD-cost:   88
c ---[3313]---> BDD-cost:  125
c ---[3311]---> BDD-cost:  123
c ---[3309]---> BDD-cost:  125
c ---[3308]---> BDD-cost:   88
c ---[3306]---> BDD-cost:   88
c ---[3304]---> BDD-cost:   88
c ---[3302]---> BDD-cost:  125
c ---[3300]---> BDD-cost:  125
c ---[3298]---> BDD-cost:  125
c ---[3297]---> BDD-cost:   88
c ---[3295]---> BDD-cost:   88
c ---[3293]---> BDD-cost:   88
c ---[3291]---> BDD-cost:   88
c ---[3289]---> BDD-cost:  125
c ---[3287]---> BDD-cost:  125
c ---[3286]---> BDD-cost:   88
c ---[3284]---> BDD-cost:   88
c ---[3282]---> BDD-cost:  125
c ---[3280]---> BDD-cost:  125
c ---[3278]---> BDD-cost:   88
c ---[3276]---> BDD-cost:   88
c ---[3275]---> BDD-cost:  125
c ---[3273]---> BDD-cost:  125
c ---[3271]---> BDD-cost:  123
c ---[3269]---> BDD-cost:   88
c ---[3267]---> BDD-cost:   88
c ---[3265]---> BDD-cost:   88
c ---[3264]---> BDD-cost:  125
c ---[3262]---> BDD-cost:  125
c ---[3260]---> BDD-cost:  125
c ---[3258]---> BDD-cost:  125
c ---[3256]---> BDD-cost:  121
c ---[3254]---> BDD-cost:  121
c ---[3253]---> BDD-cost:   88
c ---[3250]---> BDD-cost:   88
c ---[3248]---> BDD-cost:  125
c ---[3246]---> BDD-cost:  125
c ---[3244]---> BDD-cost:   88
c ---[3242]---> BDD-cost:  125
c ---[3241]---> BDD-cost:  125
c ---[3239]---> BDD-cost:  125
c ---[3237]---> BDD-cost:   88
c ---[3235]---> BDD-cost:  121
c ---[3233]---> BDD-cost:   88
c ---[3231]---> BDD-cost:  123
c ---[3230]---> BDD-cost:  125
c ---[3228]---> BDD-cost:  125
c ---[3226]---> BDD-cost:  123
c ---[3224]---> BDD-cost:  123
c ---[3222]---> BDD-cost:   88
c ---[3220]---> BDD-cost:  125
c ---[3219]---> BDD-cost:  119
c ---[3217]---> BDD-cost:  119
c ---[3215]---> BDD-cost:  119
c ---[3213]---> BDD-cost:   88
c ---[3211]---> BDD-cost:  123
c ---[3209]---> BDD-cost:  123
c ---[3208]---> BDD-cost:  125
c ---[3206]---> BDD-cost:  125
c ---[3204]---> BDD-cost:  123
c ---[3202]---> BDD-cost:  125
c ---[3200]---> BDD-cost:  125
c ---[3198]---> BDD-cost:  125
c ---[3197]---> BDD-cost:   88
c ---[3195]---> BDD-cost:   88
c ---[3193]---> BDD-cost:  125
c ---[3191]---> BDD-cost:  125
c ---[3189]---> BDD-cost:  123
c ---[3187]---> BDD-cost:  123
c ---[3186]---> BDD-cost:   88
c ---[3184]---> BDD-cost:   88
c ---[3182]---> BDD-cost:  125
c ---[3180]---> BDD-cost:  125
c ---[3178]---> BDD-cost:  125
c ---[3176]---> BDD-cost:  125
c ---[3175]---> BDD-cost:  125
c ---[3173]---> BDD-cost:  125
c ---[3171]---> BDD-cost:  123
c ---[3169]---> BDD-cost:  123
c ---[3167]---> BDD-cost:  123
c ---[3165]---> BDD-cost:  125
c ---[3164]---> BDD-cost:  125
c ---[3162]---> BDD-cost:  125
c ---[3160]---> BDD-cost:  125
c ---[3158]---> BDD-cost:  123
c ---[3156]---> BDD-cost:  125
c ---[3154]---> BDD-cost:  125
c ---[3153]---> BDD-cost:  125
c ---[3151]---> BDD-cost:  125
c ---[3149]---> BDD-cost:  125
c ---[3147]---> BDD-cost:   88
c ---[3145]---> BDD-cost:  121
c ---[3143]---> BDD-cost:  125
c ---[3142]---> BDD-cost:  123
c ---[3139]---> BDD-cost:  123
c ---[3137]---> BDD-cost:  123
c ---[3135]---> BDD-cost:  123
c ---[3133]---> BDD-cost:  125
c ---[3131]---> BDD-cost:  123
c ---[3130]---> BDD-cost:  123
c ---[3128]---> BDD-cost:  123
c ---[3126]---> BDD-cost:  125
c ---[3124]---> BDD-cost:  125
c ---[3123]---> BDD-cost:  140
c ---[3122]---> BDD-cost:  140
c ---[3121]---> BDD-cost:  137
c ---[3120]---> BDD-cost:  137
c ---[3119]---> BDD-cost:  120
c ---[3117]---> BDD-cost:  120
c ---[3116]---> BDD-cost:  137
c ---[3115]---> BDD-cost:  137
c ---[3114]---> BDD-cost:  120
c ---[3113]---> BDD-cost:  120
c ---[3112]---> BDD-cost:  137
c ---[3111]---> BDD-cost:  137
c ---[3110]---> BDD-cost:  140
c ---[3109]---> BDD-cost:  140
c ---[3108]---> BDD-cost:  137
c ---[3106]---> BDD-cost:  137
c ---[3105]---> BDD-cost:  120
c ---[3104]---> BDD-cost:  120
c ---[3103]---> BDD-cost:  137
c ---[3102]---> BDD-cost:  137
c ---[3101]---> BDD-cost:  140
c ---[3100]---> BDD-cost:  140
c ---[3099]---> BDD-cost:  137
c ---[3098]---> BDD-cost:  137
c ---[3097]---> BDD-cost:  137
c ---[3095]---> BDD-cost:  137
c ---[3094]---> BDD-cost:  137
c ---[3093]---> BDD-cost:  137
c ---[3092]---> BDD-cost:  137
c ---[3091]---> BDD-cost:  137
c ---[3090]---> BDD-cost:  137
c ---[3089]---> BDD-cost:  137
c ---[3088]---> BDD-cost:  140
c ---[3087]---> BDD-cost:  140
c ---[3086]---> BDD-cost:  137
c ---[3084]---> BDD-cost:  137
c ---[3083]---> BDD-cost:  135
c ---[3082]---> BDD-cost:  135
c ---[3081]---> BDD-cost:  137
c ---[3080]---> BDD-cost:  137
c ---[3079]---> BDD-cost:  135
c ---[3078]---> BDD-cost:  135
c ---[3077]---> BDD-cost:  137
c ---[3076]---> BDD-cost:  137
c ---[3075]---> BDD-cost:  132
c ---[3073]---> BDD-cost:  132
c ---[3072]---> BDD-cost:  137
c ---[3071]---> BDD-cost:  137
c ---[3070]---> BDD-cost:  140
c ---[3069]---> BDD-cost:  140
c ---[3068]---> BDD-cost:  137
c ---[3067]---> BDD-cost:  137
c ---[3066]---> BDD-cost:  132
c ---[3065]---> BDD-cost:  132
c ---[3064]---> BDD-cost:  137
c ---[3062]---> BDD-cost:  137
c ---[3061]---> BDD-cost:  132
c ---[3060]---> BDD-cost:  132
c ---[3059]---> BDD-cost:  137
c ---[3058]---> BDD-cost:  137
c ---[3057]---> BDD-cost:  120
c ---[3056]---> BDD-cost:  120
c ---[3055]---> BDD-cost:  137
c ---[3054]---> BDD-cost:  137
c ---[3053]---> BDD-cost:  135
c ---[3051]---> BDD-cost:  135
c ---[3050]---> BDD-cost:  137
c ---[3049]---> BDD-cost:  137
c ---[3048]---> BDD-cost:  137
c ---[3047]---> BDD-cost:  137
c ---[3046]---> BDD-cost:  137
c ---[3045]---> BDD-cost:  137
c ---[3044]---> BDD-cost:  140
c ---[3043]---> BDD-cost:  140
c ---[3042]---> BDD-cost:  137
c ---[3040]---> BDD-cost:  137
c ---[3039]---> BDD-cost:  140
c ---[3038]---> BDD-cost:  140
c ---[3037]---> BDD-cost:  137
c ---[3036]---> BDD-cost:  137
c ---[3035]---> BDD-cost:  137
c ---[3034]---> BDD-cost:  137
c ---[3033]---> BDD-cost:  137
c ---[3032]---> BDD-cost:  137
c ---[3031]---> BDD-cost:  140
c ---[3028]---> BDD-cost:  140
c ---[3027]---> BDD-cost:  137
c ---[3026]---> BDD-cost:  137
c ---[3025]---> BDD-cost:  140
c ---[3024]---> BDD-cost:  140
c ---[3023]---> BDD-cost:  137
c ---[3022]---> BDD-cost:  137
c ---[3021]---> BDD-cost:  140
c ---[3020]---> BDD-cost:  140
c ---[3019]---> BDD-cost:  137
c ---[3017]---> BDD-cost:  137
c ---[3016]---> BDD-cost:  120
c ---[3015]---> BDD-cost:  120
c ---[3014]---> BDD-cost:  137
c ---[3013]---> BDD-cost:  137
c ---[3012]---> BDD-cost:  132
c ---[3011]---> BDD-cost:  132
c ---[3010]---> BDD-cost:  137
c ---[3009]---> BDD-cost:  137
c ---[3008]---> BDD-cost:  135
c ---[3006]---> BDD-cost:  135
c ---[3005]---> BDD-cost:  137
c ---[3004]---> BDD-cost:  137
c ---[3003]---> BDD-cost:  135
c ---[3002]---> BDD-cost:  135
c ---[3001]---> BDD-cost:  137
c ---[3000]---> BDD-cost:  137
c ---[2999]---> BDD-cost:  120
c ---[2998]---> BDD-cost:  120
c ---[2997]---> BDD-cost:  137
c ---[2995]---> BDD-cost:  137
c ---[2994]---> BDD-cost:  120
c ---[2993]---> BDD-cost:  120
c ---[2992]---> BDD-cost:  137
c ---[2991]---> BDD-cost:  137
c ---[2990]---> BDD-cost:  135
c ---[2989]---> BDD-cost:  135
c ---[2988]---> BDD-cost:  137
c ---[2987]---> BDD-cost:  137
c ---[2986]---> BDD-cost:  140
c ---[2984]---> BDD-cost:  140
c ---[2983]---> BDD-cost:  137
c ---[2982]---> BDD-cost:  137
c ---[2981]---> BDD-cost:  140
c ---[2980]---> BDD-cost:  140
c ---[2979]---> BDD-cost:  137
c ---[2978]---> BDD-cost:  137
c ---[2977]---> BDD-cost:  140
c ---[2976]---> BDD-cost:  140
c ---[2975]---> BDD-cost:  137
c ---[2973]---> BDD-cost:  137
c ---[2972]---> BDD-cost:  140
c ---[2971]---> BDD-cost:  140
c ---[2970]---> BDD-cost:  137
c ---[2969]---> BDD-cost:  137
c ---[2968]---> BDD-cost:  135
c ---[2967]---> BDD-cost:  135
c ---[2966]---> BDD-cost:  137
c ---[2965]---> BDD-cost:  137
c ---[2964]---> BDD-cost:  140
c ---[2962]---> BDD-cost:  140
c ---[2961]---> BDD-cost:  137
c ---[2960]---> BDD-cost:  137
c ---[2959]---> BDD-cost:  140
c ---[2958]---> BDD-cost:  140
c ---[2957]---> BDD-cost:  137
c ---[2956]---> BDD-cost:  137
c ---[2955]---> BDD-cost:  140
c ---[2954]---> BDD-cost:  140
c ---[2953]---> BDD-cost:  137
c ---[2951]---> BDD-cost:  137
c ---[2950]---> BDD-cost:  135
c ---[2949]---> BDD-cost:  135
c ---[2948]---> BDD-cost:  137
c ---[2947]---> BDD-cost:  137
c ---[2946]---> BDD-cost:  140
c ---[2945]---> BDD-cost:  140
c ---[2944]---> BDD-cost:  137
c ---[2943]---> BDD-cost:  137
c ---[2942]---> BDD-cost:  130
c ---[2940]---> BDD-cost:  130
c ---[2939]---> BDD-cost:  137
c ---[2938]---> BDD-cost:  137
c ---[2937]---> BDD-cost:  132
c ---[2936]---> BDD-cost:  132
c ---[2935]---> BDD-cost:  137
c ---[2934]---> BDD-cost:  137
c ---[2933]---> BDD-cost:  140
c ---[2932]---> BDD-cost:  140
c ---[2931]---> BDD-cost:  137
c ---[2929]---> BDD-cost:  137
c ---[2928]---> BDD-cost:  140
c ---[2927]---> BDD-cost:  140
c ---[2926]---> BDD-cost:  137
c ---[2925]---> BDD-cost:  137
c ---[2924]---> BDD-cost:  140
c ---[2923]---> BDD-cost:  140
c ---[2922]---> BDD-cost:  137
c ---[2921]---> BDD-cost:  137
c ---[2920]---> BDD-cost:  140
c ---[2917]---> BDD-cost:  140
c ---[2916]---> BDD-cost:  137
c ---[2915]---> BDD-cost:  137
c ---[2914]---> BDD-cost:  140
c ---[2913]---> BDD-cost:  140
c ---[2912]---> BDD-cost:  137
c ---[2911]---> BDD-cost:  137
c ---[2910]---> BDD-cost:  135
c ---[2909]---> BDD-cost:  135
c ---[2908]---> BDD-cost:  137
c ---[2906]---> BDD-cost:  137
c ---[2905]---> BDD-cost:  135
c ---[2904]---> BDD-cost:  135
c ---[2903]---> BDD-cost:  137
c ---[2902]---> BDD-cost:  137
c ---[2901]---> BDD-cost:  140
c ---[2900]---> BDD-cost:  140
c ---[2899]---> BDD-cost:  137
c ---[2898]---> BDD-cost:  137
c ---[2897]---> BDD-cost:  135
c ---[2895]---> BDD-cost:  135
c ---[2894]---> BDD-cost:  137
c ---[2893]---> BDD-cost:  137
c ---[2892]---> BDD-cost:  135
c ---[2891]---> BDD-cost:  135
c ---[2890]---> BDD-cost:  137
c ---[2889]---> BDD-cost:  137
c ---[2888]---> BDD-cost:  135
c ---[2887]---> BDD-cost:  135
c ---[2886]---> BDD-cost:  137
c ---[2884]---> BDD-cost:  137
c ---[2883]---> BDD-cost:  140
c ---[2882]---> BDD-cost:  140
c ---[2881]---> BDD-cost:  137
c ---[2880]---> BDD-cost:  137
c ---[2879]---> BDD-cost:  140
c ---[2878]---> BDD-cost:  140
c ---[2877]---> BDD-cost:  137
c ---[2876]---> BDD-cost:  137
c ---[2875]---> BDD-cost:  140
c ---[2873]---> BDD-cost:  140
c ---[2872]---> BDD-cost:  137
c ---[2871]---> BDD-cost:  137
c ---[2870]---> BDD-cost:  120
c ---[2869]---> BDD-cost:  120
c ---[2868]---> BDD-cost:  137
c ---[2867]---> BDD-cost:  137
c ---[2866]---> BDD-cost:  137
c ---[2865]---> BDD-cost:  137
c ---[2864]---> BDD-cost:  137
c ---[2862]---> BDD-cost:  137
c ---[2861]---> BDD-cost:  140
c ---[2860]---> BDD-cost:  140
c ---[2859]---> BDD-cost:  137
c ---[2858]---> BDD-cost:  137
c ---[2857]---> BDD-cost:  120
c ---[2856]---> BDD-cost:  120
c ---[2855]---> BDD-cost:  137
c ---[2854]---> BDD-cost:  137
c ---[2853]---> BDD-cost:  132
c ---[2851]---> BDD-cost:  132
c ---[2850]---> BDD-cost:  137
c ---[2849]---> BDD-cost:  137
c ---[2848]---> BDD-cost:  140
c ---[2847]---> BDD-cost:  140
c ---[2846]---> BDD-cost:  137
c ---[2845]---> BDD-cost:  137
c ---[2844]---> BDD-cost:  137
c ---[2843]---> BDD-cost:  137
c ---[2842]---> BDD-cost:  137
c ---[2840]---> BDD-cost:  137
c ---[2839]---> BDD-cost:  140
c ---[2838]---> BDD-cost:  140
c ---[2837]---> BDD-cost:  137
c ---[2836]---> BDD-cost:  137
c ---[2835]---> BDD-cost:  135
c ---[2834]---> BDD-cost:  135
c ---[2833]---> BDD-cost:  137
c ---[2832]---> BDD-cost:  137
c ---[2831]---> BDD-cost:  140
c ---[2829]---> BDD-cost:  140
c ---[2828]---> BDD-cost:  137
c ---[2827]---> BDD-cost:  137
c ---[2826]---> BDD-cost:  135
c ---[2825]---> BDD-cost:  135
c ---[2824]---> BDD-cost:  137
c ---[2823]---> BDD-cost:  137
c ---[2822]---> BDD-cost:  120
c ---[2821]---> BDD-cost:  120
c ---[2820]---> BDD-cost:  137
c ---[2818]---> BDD-cost:  137
c ---[2817]---> BDD-cost:  135
c ---[2816]---> BDD-cost:  135
c ---[2815]---> BDD-cost:  137
c ---[2814]---> BDD-cost:  137
c ---[2813]---> BDD-cost:  140
c ---[2812]---> BDD-cost:  140
c ---[2811]---> BDD-cost:  137
c ---[2810]---> BDD-cost:  137
c ---[2809]---> BDD-cost:  120
c ---[2805]---> BDD-cost:  120
c ---[2804]---> BDD-cost:  137
c ---[2803]---> BDD-cost:  137
c ---[2802]---> BDD-cost:  135
c ---[2801]---> BDD-cost:  135
c ---[2800]---> BDD-cost:  137
c ---[2799]---> BDD-cost:  137
c ---[2798]---> BDD-cost:  135
c ---[2797]---> BDD-cost:  135
c ---[2796]---> BDD-cost:  137
c ---[2794]---> BDD-cost:  137
c ---[2793]---> BDD-cost:  140
c ---[2792]---> BDD-cost:  140
c ---[2791]---> BDD-cost:  137
c ---[2790]---> BDD-cost:  137
c ---[2789]---> BDD-cost:  140
c ---[2788]---> BDD-cost:  140
c ---[2787]---> BDD-cost:  137
c ---[2786]---> BDD-cost:  137
c ---[2785]---> BDD-cost:  140
c ---[2783]---> BDD-cost:  140
c ---[2782]---> BDD-cost:  137
c ---[2781]---> BDD-cost:  137
c ---[2780]---> BDD-cost:  140
c ---[2779]---> BDD-cost:  140
c ---[2778]---> BDD-cost:  137
c ---[2777]---> BDD-cost:  137
c ---[2776]---> BDD-cost:  130
c ---[2775]---> BDD-cost:  130
c ---[2774]---> BDD-cost:  137
c ---[2772]---> BDD-cost:  137
c ---[2771]---> BDD-cost:  120
c ---[2770]---> BDD-cost:  120
c ---[2769]---> BDD-cost:  137
c ---[2768]---> BDD-cost:  137
c ---[2767]---> BDD-cost:  140
c ---[2766]---> BDD-cost:  140
c ---[2765]---> BDD-cost:  137
c ---[2764]---> BDD-cost:  137
c ---[2763]---> BDD-cost:  140
c ---[2761]---> BDD-cost:  140
c ---[2760]---> BDD-cost:  137
c ---[2759]---> BDD-cost:  137
c ---[2758]---> BDD-cost:  120
c ---[2757]---> BDD-cost:  120
c ---[2756]---> BDD-cost:  137
c ---[2755]---> BDD-cost:  137
c ---[2754]---> BDD-cost:  140
c ---[2753]---> BDD-cost:  140
c ---[2752]---> BDD-cost:  137
c ---[2750]---> BDD-cost:  137
c ---[2749]---> BDD-cost:  135
c ---[2748]---> BDD-cost:  135
c ---[2747]---> BDD-cost:  137
c ---[2746]---> BDD-cost:  137
c ---[2745]---> BDD-cost:  140
c ---[2744]---> BDD-cost:  140
c ---[2743]---> BDD-cost:  137
c ---[2742]---> BDD-cost:  137
c ---[2741]---> BDD-cost:  140
c ---[2739]---> BDD-cost:  140
c ---[2738]---> BDD-cost:  137
c ---[2737]---> BDD-cost:  137
c ---[2736]---> BDD-cost:  120
c ---[2735]---> BDD-cost:  120
c ---[2734]---> BDD-cost:  137
c ---[2733]---> BDD-cost:  137
c ---[2732]---> BDD-cost:  140
c ---[2731]---> BDD-cost:  140
c ---[2730]---> BDD-cost:  137
c ---[2728]---> BDD-cost:  137
c ---[2727]---> BDD-cost:  140
c ---[2726]---> BDD-cost:  140
c ---[2725]---> BDD-cost:  137
c ---[2724]---> BDD-cost:  137
c ---[2723]---> BDD-cost:  140
c ---[2722]---> BDD-cost:  140
c ---[2721]---> BDD-cost:  137
c ---[2720]---> BDD-cost:  137
c ---[2719]---> BDD-cost:  137
c ---[2717]---> BDD-cost:  137
c ---[2716]---> BDD-cost:  137
c ---[2715]---> BDD-cost:  137
c ---[2714]---> BDD-cost:  135
c ---[2713]---> BDD-cost:  135
c ---[2712]---> BDD-cost:  137
c ---[2711]---> BDD-cost:  137
c ---[2710]---> BDD-cost:  140
c ---[2709]---> BDD-cost:  140
c ---[2708]---> BDD-cost:  137
c ---[2706]---> BDD-cost:  137
c ---[2705]---> BDD-cost:  132
c ---[2704]---> BDD-cost:  132
c ---[2703]---> BDD-cost:  137
c ---[2702]---> BDD-cost:  137
c ---[2701]---> BDD-cost:  120
c ---[2700]---> BDD-cost:  120
c ---[2699]---> BDD-cost:  137
c ---[2698]---> BDD-cost:  137
c ---[2697]---> BDD-cost:  140
c ---[2694]---> BDD-cost:  140
c ---[2693]---> BDD-cost:  137
c ---[2692]---> BDD-cost:  137
c ---[2691]---> BDD-cost:  120
c ---[2690]---> BDD-cost:  120
c ---[2689]---> BDD-cost:  137
c ---[2688]---> BDD-cost:  137
c ---[2687]---> BDD-cost:  135
c ---[2686]---> BDD-cost:  135
c ---[2685]---> BDD-cost:  137
c ---[2683]---> BDD-cost:  137
c ---[2682]---> BDD-cost:  140
c ---[2681]---> BDD-cost:  140
c ---[2680]---> BDD-cost:  137
c ---[2679]---> BDD-cost:  137
c ---[2678]---> BDD-cost:  132
c ---[2677]---> BDD-cost:  132
c ---[2676]---> BDD-cost:  137
c ---[2675]---> BDD-cost:  137
c ---[2674]---> BDD-cost:  120
c ---[2672]---> BDD-cost:  120
c ---[2671]---> BDD-cost:  137
c ---[2670]---> BDD-cost:  137
c ---[2669]---> BDD-cost:  120
c ---[2668]---> BDD-cost:  120
c ---[2667]---> BDD-cost:  137
c ---[2666]---> BDD-cost:  137
c ---[2665]---> BDD-cost:  120
c ---[2664]---> BDD-cost:  120
c ---[2663]---> BDD-cost:  137
c ---[2661]---> BDD-cost:  137
c ---[2660]---> BDD-cost:  135
c ---[2659]---> BDD-cost:  135
c ---[2658]---> BDD-cost:  137
c ---[2657]---> BDD-cost:  137
c ---[2656]---> BDD-cost:  120
c ---[2655]---> BDD-cost:  137
c ---[2654]---> BDD-cost:  132
c ---[2653]---> BDD-cost:  140
c ---[2652]---> BDD-cost:  137
c ---[2650]---> BDD-cost:  140
c ---[2649]---> BDD-cost:  132
c ---[2648]---> BDD-cost:  143
c ---[2647]---> BDD-cost:  143
c ---[2646]---> BDD-cost:  131
c ---[2645]---> BDD-cost:  135
c ---[2644]---> BDD-cost:  137
c ---[2643]---> BDD-cost:  137
c ---[2642]---> BDD-cost:  127
c ---[2641]---> BDD-cost:  127
c ---[2639]---> BDD-cost:  127
c ---[2638]---> BDD-cost:  140
c ---[2637]---> BDD-cost:  127
c ---[2636]---> BDD-cost:  129
c ---[2635]---> BDD-cost:  137
c ---[2634]---> BDD-cost:  137
c ---[2633]---> BDD-cost:  124
c ---[2632]---> BDD-cost:  127
c ---[2631]---> BDD-cost:  137
c ---[2630]---> BDD-cost:  124
c ---[2628]---> BDD-cost:  137
c ---[2627]---> BDD-cost:  124
c ---[2626]---> BDD-cost:  127
c ---[2625]---> BDD-cost:  140
c ---[2624]---> BDD-cost:  129
c ---[2623]---> BDD-cost:  140
c ---[2622]---> BDD-cost:  132
c ---[2621]---> BDD-cost:  140
c ---[2620]---> BDD-cost:  137
c ---[2619]---> BDD-cost:  140
c ---[2617]---> BDD-cost:  129
c ---[2616]---> BDD-cost:  118
c ---[2615]---> BDD-cost:  126
c ---[2614]---> BDD-cost:  135
c ---[2613]---> BDD-cost:  140
c ---[2612]---> BDD-cost:  140
c ---[2611]---> BDD-cost:  140
c ---[2610]---> BDD-cost:  132
c ---[2609]---> BDD-cost:  120
c ---[2608]---> BDD-cost:  120
c ---[2606]---> BDD-cost:  140
c ---[2605]---> BDD-cost:  137
c ---[2604]---> BDD-cost:  135
c ---[2603]---> BDD-cost:  134
c ---[2602]---> BDD-cost:  125
c ---[2601]---> BDD-cost:  131
c ---[2600]---> BDD-cost:  137
c ---[2599]---> BDD-cost:  126
c ---[2598]---> BDD-cost:  132
c ---[2597]---> BDD-cost:  132
c ---[2595]---> BDD-cost:  120
c ---[2594]---> BDD-cost:  137
c ---[2593]---> BDD-cost:  140
c ---[2592]---> BDD-cost:  132
c ---[2591]---> BDD-cost:  135
c ---[2590]---> BDD-cost:  129
c ---[2589]---> BDD-cost:  130
c ---[2588]---> BDD-cost:  124
c ---[2587]---> BDD-cost:  140
c ---[2586]---> BDD-cost:  131
c ---[2583]---> BDD-cost:  135
c ---[2582]---> BDD-cost:  124
c ---[2581]---> BDD-cost:  135
c ---[2580]---> BDD-cost:  124
c ---[2579]---> BDD-cost:  129
c ---[2578]---> BDD-cost:  137
c ---[2577]---> BDD-cost:  143
c ---[2576]---> BDD-cost:  137
c ---[2575]---> BDD-cost:  125
c ---[2574]---> BDD-cost:  132
c ---[2572]---> BDD-cost:  140
c ---[2571]---> BDD-cost:  134
c ---[2570]---> BDD-cost:  134
c ---[2569]---> BDD-cost:  124
c ---[2568]---> BDD-cost:  140
c ---[2567]---> BDD-cost:  124
c ---[2566]---> BDD-cost:  140
c ---[2565]---> BDD-cost:  131
c ---[2564]---> BDD-cost:  140
c ---[2563]---> BDD-cost:  131
c ---[2561]---> BDD-cost:  126
c ---[2560]---> BDD-cost:  137
c ---[2559]---> BDD-cost:  125
c ---[2558]---> BDD-cost:  132
c ---[2557]---> BDD-cost:  140
c ---[2556]---> BDD-cost:  137
c ---[2555]---> BDD-cost:  134
c ---[2554]---> BDD-cost:  122
c ---[2553]---> BDD-cost:  140
c ---[2552]---> BDD-cost:  122
c ---[2550]---> BDD-cost:  140
c ---[2549]---> BDD-cost:  134
c ---[2548]---> BDD-cost:  140
c ---[2547]---> BDD-cost:  134
c ---[2546]---> BDD-cost:  137
c ---[2545]---> BDD-cost:  124
c ---[2544]---> BDD-cost:  122
c ---[2543]---> BDD-cost:  124
c ---[2542]---> BDD-cost:  137
c ---[2541]---> BDD-cost:  124
c ---[2539]---> BDD-cost:  127
c ---[2538]---> BDD-cost:  131
c ---[2537]---> BDD-cost:  120
c ---[2536]---> BDD-cost:  126
c ---[2535]---> BDD-cost:  130
c ---[2534]---> BDD-cost:  120
c ---[2533]---> BDD-cost:  135
c ---[2532]---> BDD-cost:  132
c ---[2531]---> BDD-cost:  125
c ---[2530]---> BDD-cost:  132
c ---[2528]---> BDD-cost:  135
c ---[2527]---> BDD-cost:  137
c ---[2526]---> BDD-cost:  125
c ---[2525]---> BDD-cost:  134
c ---[2524]---> BDD-cost:  132
c ---[2523]---> BDD-cost:  129
c ---[2522]---> BDD-cost:  137
c ---[2521]---> BDD-cost:  129
c ---[2520]---> BDD-cost:  120
c ---[2519]---> BDD-cost:  129
c ---[2517]---> BDD-cost:  131
c ---[2516]---> BDD-cost:  134
c ---[2515]---> BDD-cost:  140
c ---[2514]---> BDD-cost:  124
c ---[2513]---> BDD-cost:  140
c ---[2512]---> BDD-cost:  131
c ---[2511]---> BDD-cost:  127
c ---[2510]---> BDD-cost:  131
c ---[2509]---> BDD-cost:  137
c ---[2508]---> BDD-cost:  131
c ---[2506]---> BDD-cost:  122
c ---[2505]---> BDD-cost:  131
c ---[2504]---> BDD-cost:  135
c ---[2503]---> BDD-cost:  126
c ---[2502]---> BDD-cost:  135
c ---[2501]---> BDD-cost:  137
c ---[2500]---> BDD-cost:  140
c ---[2499]---> BDD-cost:  137
c ---[2498]---> BDD-cost:  140
c ---[2497]---> BDD-cost:  132
c ---[2495]---> BDD-cost:  140
c ---[2494]---> BDD-cost:  122
c ---[2493]---> BDD-cost:  137
c ---[2492]---> BDD-cost:  134
c ---[2491]---> BDD-cost:  127
c ---[2490]---> BDD-cost:  134
c ---[2489]---> BDD-cost:  140
c ---[2488]---> BDD-cost:  134
c ---[2487]---> BDD-cost:  126
c ---[2486]---> BDD-cost:  129
c ---[2484]---> BDD-cost:  130
c ---[2483]---> BDD-cost:  134
c ---[2482]---> BDD-cost:  135
c ---[2481]---> BDD-cost:  124
c ---[2480]---> BDD-cost:  137
c ---[2479]---> BDD-cost:  124
c ---[2478]---> BDD-cost:  132
c ---[2477]---> BDD-cost:  124
c ---[2476]---> BDD-cost:  137
c ---[2475]---> BDD-cost:  124
c ---[2472]---> BDD-cost:  140
c ---[2471]---> BDD-cost:  131
c ---[2470]---> BDD-cost:  140
c ---[2469]---> BDD-cost:  140
c ---[2468]---> BDD-cost:  126
c ---[2467]---> BDD-cost:  137
c ---[2466]---> BDD-cost:  127
c ---[2465]---> BDD-cost:  135
c ---[2464]---> BDD-cost:  132
c ---[2463]---> BDD-cost:  124
c ---[2461]---> BDD-cost:  137
c ---[2460]---> BDD-cost:  120
c ---[2459]---> BDD-cost:  134
c ---[2458]---> BDD-cost:  122
c ---[2457]---> BDD-cost:  140
c ---[2456]---> BDD-cost:  140
c ---[2455]---> BDD-cost:  140
c ---[2454]---> BDD-cost:  120
c ---[2453]---> BDD-cost:  140
c ---[2452]---> BDD-cost:  132
c ---[2450]---> BDD-cost:  140
c ---[2449]---> BDD-cost:  137
c ---[2448]---> BDD-cost:  120
c ---[2447]---> BDD-cost:  137
c ---[2446]---> BDD-cost:  140
c ---[2445]---> BDD-cost:  127
c ---[2444]---> BDD-cost:  125
c ---[2443]---> BDD-cost:  137
c ---[2442]---> BDD-cost:  120
c ---[2441]---> BDD-cost:  132
c ---[2439]---> BDD-cost:  140
c ---[2438]---> BDD-cost:  132
c ---[2437]---> BDD-cost:  127
c ---[2436]---> BDD-cost:  132
c ---[2435]---> BDD-cost:  137
c ---[2434]---> BDD-cost:  132
c ---[2433]---> BDD-cost:  140
c ---[2432]---> BDD-cost:  137
c ---[2431]---> BDD-cost:  140
c ---[2430]---> BDD-cost:  122
c ---[2428]---> BDD-cost:  137
c ---[2427]---> BDD-cost:  134
c ---[2426]---> BDD-cost:  130
c ---[2425]---> BDD-cost:  129
c ---[2424]---> BDD-cost:  125
c ---[2423]---> BDD-cost:  129
c ---[2422]---> BDD-cost:  140
c ---[2421]---> BDD-cost:  129
c ---[2420]---> BDD-cost:  135
c ---[2419]---> BDD-cost:  131
c ---[2417]---> BDD-cost:  137
c ---[2416]---> BDD-cost:  131
c ---[2415]---> BDD-cost:  127
c ---[2414]---> BDD-cost:  131
c ---[2413]---> BDD-cost:  135
c ---[2412]---> BDD-cost:  126
c ---[2411]---> BDD-cost:  126
c ---[2410]---> BDD-cost:  120
c ---[2409]---> BDD-cost:  140
c ---[2408]---> BDD-cost:  132
c ---[2406]---> BDD-cost:  140
c ---[2405]---> BDD-cost:  137
c ---[2404]---> BDD-cost:  135
c ---[2403]---> BDD-cost:  137
c ---[2402]---> BDD-cost:  140
c ---[2401]---> BDD-cost:  127
c ---[2400]---> BDD-cost:  135
c ---[2399]---> BDD-cost:  137
c ---[2398]---> BDD-cost:  132
c ---[2397]---> BDD-cost:  132
c ---[2395]---> BDD-cost:  140
c ---[2394]---> BDD-cost:  132
c ---[2393]---> BDD-cost:  132
c ---[2392]---> BDD-cost:  132
c ---[2391]---> BDD-cost:  140
c ---[2390]---> BDD-cost:  132
c ---[2389]---> BDD-cost:  140
c ---[2388]---> BDD-cost:  137
c ---[2387]---> BDD-cost:  140
c ---[2386]---> BDD-cost:  122
c ---[2384]---> BDD-cost:  140
c ---[2383]---> BDD-cost:  134
c ---[2382]---> BDD-cost:  135
c ---[2381]---> BDD-cost:  129
c ---[2380]---> BDD-cost:  135
c ---[2379]---> BDD-cost:  129
c ---[2378]---> BDD-cost:  140
c ---[2377]---> BDD-cost:  129
c ---[2376]---> BDD-cost:  120
c ---[2375]---> BDD-cost:  134
c ---[2373]---> BDD-cost:  126
c ---[2372]---> BDD-cost:  131
c ---[2371]---> BDD-cost:  140
c ---[2370]---> BDD-cost:  131
c ---[2369]---> BDD-cost:  135
c ---[2368]---> BDD-cost:  131
c ---[2367]---> BDD-cost:  118
c ---[2366]---> BDD-cost:  137
c ---[2365]---> BDD-cost:  140
c ---[2364]---> BDD-cost:  132
c ---[2361]---> BDD-cost:  130
c ---[2360]---> BDD-cost:  132
c ---[2359]---> BDD-cost:  140
c ---[2358]---> BDD-cost:  137
c ---[2357]---> BDD-cost:  130
c ---[2356]---> BDD-cost:  127
c ---[2355]---> BDD-cost:  120
c ---[2354]---> BDD-cost:  137
c ---[2353]---> BDD-cost:  140
c ---[2352]---> BDD-cost:  137
c ---[2350]---> BDD-cost:  127
c ---[2349]---> BDD-cost:  137
c ---[2348]---> BDD-cost:  140
c ---[2347]---> BDD-cost:  137
c ---[2346]---> BDD-cost:  140
c ---[2345]---> BDD-cost:  132
c ---[2344]---> BDD-cost:  140
c ---[2343]---> BDD-cost:  137
c ---[2342]---> BDD-cost:  140
c ---[2341]---> BDD-cost:  122
c ---[2339]---> BDD-cost:  130
c ---[2338]---> BDD-cost:  134
c ---[2337]---> BDD-cost:  130
c ---[2336]---> BDD-cost:  134
c ---[2335]---> BDD-cost:  143
c ---[2334]---> BDD-cost:  134
c ---[2333]---> BDD-cost:  135
c ---[2332]---> BDD-cost:  124
c ---[2331]---> BDD-cost:  140
c ---[2330]---> BDD-cost:  124
c ---[2328]---> BDD-cost:  120
c ---[2327]---> BDD-cost:  124
c ---[2326]---> BDD-cost:  135
c ---[2325]---> BDD-cost:  131
c ---[2324]---> BDD-cost:  126
c ---[2323]---> BDD-cost:  120
c ---[2322]---> BDD-cost:  135
c ---[2321]---> BDD-cost:  120
c ---[2320]---> BDD-cost:  140
c ---[2319]---> BDD-cost:  137
c ---[2317]---> BDD-cost:  135
c ---[2316]---> BDD-cost:  132
c ---[2315]---> BDD-cost:  129
c ---[2314]---> BDD-cost:  137
c ---[2313]---> BDD-cost:  140
c ---[2312]---> BDD-cost:  137
c ---[2311]---> BDD-cost:  126
c ---[2310]---> BDD-cost:  137
c ---[2309]---> BDD-cost:  140
c ---[2308]---> BDD-cost:  137
c ---[2306]---> BDD-cost:  137
c ---[2305]---> BDD-cost:  127
c ---[2304]---> BDD-cost:  140
c ---[2303]---> BDD-cost:  137
c ---[2302]---> BDD-cost:  140
c ---[2301]---> BDD-cost:  132
c ---[2300]---> BDD-cost:  135
c ---[2299]---> BDD-cost:  137
c ---[2298]---> BDD-cost:  130
c ---[2297]---> BDD-cost:  137
c ---[2295]---> BDD-cost:  140
c ---[2294]---> BDD-cost:  137
c ---[2293]---> BDD-cost:  122
c ---[2292]---> BDD-cost:  122
c ---[2291]---> BDD-cost:  126
c ---[2290]---> BDD-cost:  129
c ---[2289]---> BDD-cost:  140
c ---[2288]---> BDD-cost:  129
c ---[2287]---> BDD-cost:  135
c ---[2286]---> BDD-cost:  129
c ---[2284]---> BDD-cost:  118
c ---[2283]---> BDD-cost:  118
c ---[2282]---> BDD-cost:  140
c ---[2281]---> BDD-cost:  140
c ---[2280]---> BDD-cost:  130
c ---[2279]---> BDD-cost:  120
c ---[2278]---> BDD-cost:  140
c ---[2277]---> BDD-cost:  137
c ---[2276]---> BDD-cost:  131
c ---[2275]---> BDD-cost:  132
c ---[2273]---> BDD-cost:  138
c ---[2272]---> BDD-cost:  138
c ---[2271]---> BDD-cost:  132
c ---[2270]---> BDD-cost:  135
c ---[2269]---> BDD-cost:  132
c ---[2268]---> BDD-cost:  132
c ---[2267]---> BDD-cost:  137
c ---[2266]---> BDD-cost:  120
c ---[2265]---> BDD-cost:  127
c ---[2264]---> BDD-cost:  118
c ---[2262]---> BDD-cost:  137
c ---[2261]---> BDD-cost:  137
c ---[2260]---> BDD-cost:  132
c ---[2259]---> BDD-cost:  140
c ---[2258]---> BDD-cost:  132
c ---[2257]---> BDD-cost:  130
c ---[2256]---> BDD-cost:  132
c ---[2255]---> BDD-cost:  134
c ---[2254]---> BDD-cost:  137
c ---[2253]---> BDD-cost:  137
c ---[2250]---> BDD-cost:  134
c ---[2249]---> BDD-cost:  118
c ---[2248]---> BDD-cost:  134
c ---[2247]---> BDD-cost:  127
c ---[2246]---> BDD-cost:  134
c ---[2245]---> BDD-cost:  140
c ---[2244]---> BDD-cost:  134
c ---[2243]---> BDD-cost:  140
c ---[2242]---> BDD-cost:  120
c ---[2241]---> BDD-cost:  130
c ---[2239]---> BDD-cost:  137
c ---[2238]---> BDD-cost:  122
c ---[2237]---> BDD-cost:  132
c ---[2236]---> BDD-cost:  140
c ---[2235]---> BDD-cost:  132
c ---[2234]---> BDD-cost:  124
c ---[2233]---> BDD-cost:  132
c ---[2232]---> BDD-cost:  140
c ---[2231]---> BDD-cost:  132
c ---[2230]---> BDD-cost:  137
c ---[2228]---> BDD-cost:  137
c ---[2227]---> BDD-cost:  140
c ---[2226]---> BDD-cost:  127
c ---[2225]---> BDD-cost:  140
c ---[2224]---> BDD-cost:  137
c ---[2223]---> BDD-cost:  130
c ---[2222]---> BDD-cost:  132
c ---[2221]---> BDD-cost:  135
c ---[2220]---> BDD-cost:  132
c ---[2219]---> BDD-cost:  140
c ---[2217]---> BDD-cost:  132
c ---[2216]---> BDD-cost:  132
c ---[2215]---> BDD-cost:  137
c ---[2214]---> BDD-cost:  122
c ---[2213]---> BDD-cost:  134
c ---[2212]---> BDD-cost:  140
c ---[2211]---> BDD-cost:  134
c ---[2210]---> BDD-cost:  134
c ---[2209]---> BDD-cost:  134
c ---[2208]---> BDD-cost:  125
c ---[2206]---> BDD-cost:  134
c ---[2205]---> BDD-cost:  138
c ---[2204]---> BDD-cost:  137
c ---[2203]---> BDD-cost:  137
c ---[2202]---> BDD-cost:  132
c ---[2201]---> BDD-cost:  140
c ---[2200]---> BDD-cost:  132
c ---[2199]---> BDD-cost:  122
c ---[2198]---> BDD-cost:  137
c ---[2197]---> BDD-cost:  129
c ---[2195]---> BDD-cost:  137
c ---[2194]---> BDD-cost:  134
c ---[2193]---> BDD-cost:  132
c ---[2192]---> BDD-cost:  126
c ---[2191]---> BDD-cost:  132
c ---[2190]---> BDD-cost:  137
c ---[2189]---> BDD-cost:  129
c ---[2188]---> BDD-cost:  140
c ---[2187]---> BDD-cost:  134
c ---[2186]---> BDD-cost:  125
c ---[2184]---> BDD-cost:  120
c ---[2183]---> BDD-cost:  137
c ---[2182]---> BDD-cost:  137
c ---[2181]---> BDD-cost:  125
c ---[2180]---> BDD-cost:  137
c ---[2179]---> BDD-cost:  134
c ---[2178]---> BDD-cost:  137
c ---[2177]---> BDD-cost:  130
c ---[2176]---> BDD-cost:  137
c ---[2175]---> BDD-cost:  135
c ---[2173]---> BDD-cost:  132
c ---[2172]---> BDD-cost:  125
c ---[2171]---> BDD-cost:  137
c ---[2170]---> BDD-cost:  135
c ---[2169]---> BDD-cost:  127
c ---[2168]---> BDD-cost:  140
c ---[2167]---> BDD-cost:  137
c ---[2166]---> BDD-cost:  140
c ---[2165]---> BDD-cost:  137
c ---[2164]---> BDD-cost:  130
c ---[2162]---> BDD-cost:  137
c ---[2161]---> BDD-cost:  137
c ---[2160]---> BDD-cost:  132
c ---[2159]---> BDD-cost:  131
c ---[2158]---> BDD-cost:  122
c ---[2157]---> BDD-cost:  135
c ---[2156]---> BDD-cost:  122
c ---[2155]---> BDD-cost:  126
c ---[2154]---> BDD-cost:  122
c ---[2153]---> BDD-cost:  140
c ---[2151]---> BDD-cost:  122
c ---[2150]---> BDD-cost:  143
c ---[2149]---> BDD-cost:  120
c ---[2148]---> BDD-cost:  124
c ---[2147]---> BDD-cost:  120
c ---[2146]---> BDD-cost:  140
c ---[2145]---> BDD-cost:  120
c ---[2144]---> BDD-cost:  125
c ---[2143]---> BDD-cost:  137
c ---[2142]---> BDD-cost:  135
c ---[2139]---> BDD-cost:  132
c ---[2138]---> BDD-cost:  126
c ---[2137]---> BDD-cost:  137
c ---[2136]---> BDD-cost:  140
c ---[2135]---> BDD-cost:  127
c ---[2134]---> BDD-cost:  137
c ---[2133]---> BDD-cost:  127
c ---[2132]---> BDD-cost:  135
c ---[2131]---> BDD-cost:  127
c ---[2130]---> BDD-cost:  140
c ---[2128]---> BDD-cost:  137
c ---[2127]---> BDD-cost:  126
c ---[2126]---> BDD-cost:  137
c ---[2125]---> BDD-cost:  137
c ---[2124]---> BDD-cost:  122
c ---[2123]---> BDD-cost:  137
c ---[2122]---> BDD-cost:  134
c ---[2121]---> BDD-cost:  126
c ---[2120]---> BDD-cost:  140
c ---[2119]---> BDD-cost:  140
c ---[2117]---> BDD-cost:  140
c ---[2116]---> BDD-cost:  140
c ---[2115]---> BDD-cost:  140
c ---[2114]---> BDD-cost:  137
c ---[2113]---> BDD-cost:  120
c ---[2112]---> BDD-cost:  140
c ---[2111]---> BDD-cost:  137
c ---[2110]---> BDD-cost:  143
c ---[2109]---> BDD-cost:  132
c ---[2108]---> BDD-cost:  120
c ---[2106]---> BDD-cost:  137
c ---[2105]---> BDD-cost:  135
c ---[2104]---> BDD-cost:  137
c ---[2103]---> BDD-cost:  140
c ---[2102]---> BDD-cost:  137
c ---[2101]---> BDD-cost:  129
c ---[2100]---> BDD-cost:  127
c ---[2099]---> BDD-cost:  132
c ---[2098]---> BDD-cost:  132
c ---[2097]---> BDD-cost:  143
c ---[2095]---> BDD-cost:  132
c ---[2094]---> BDD-cost:  137
c ---[2093]---> BDD-cost:  132
c ---[2092]---> BDD-cost:  135
c ---[2091]---> BDD-cost:  132
c ---[2090]---> BDD-cost:  135
c ---[2089]---> BDD-cost:  140
c ---[2088]---> BDD-cost:  140
c ---[2087]---> BDD-cost:  130
c ---[2086]---> BDD-cost:  120
c ---[2084]---> BDD-cost:  135
c ---[2083]---> BDD-cost:  132
c ---[2082]---> BDD-cost:  140
c ---[2081]---> BDD-cost:  137
c ---[2080]---> BDD-cost:  134
c ---[2079]---> BDD-cost:  137
c ---[2078]---> BDD-cost:  132
c ---[2077]---> BDD-cost:  137
c ---[2076]---> BDD-cost:  140
c ---[2075]---> BDD-cost:  132
c ---[2073]---> BDD-cost:  137
c ---[2072]---> BDD-cost:  137
c ---[2071]---> BDD-cost:  140
c ---[2070]---> BDD-cost:  122
c ---[2069]---> BDD-cost:  132
c ---[2068]---> BDD-cost:  140
c ---[2067]---> BDD-cost:  140
c ---[2066]---> BDD-cost:  134
c ---[2065]---> BDD-cost:  120
c ---[2064]---> BDD-cost:  137
c ---[2062]---> BDD-cost:  137
c ---[2061]---> BDD-cost:  143
c ---[2060]---> BDD-cost:  132
c ---[2059]---> BDD-cost:  127
c ---[2058]---> BDD-cost:  137
c ---[2057]---> BDD-cost:  135
c ---[2056]---> BDD-cost:  137
c ---[2055]---> BDD-cost:  140
c ---[2054]---> BDD-cost:  137
c ---[2053]---> BDD-cost:  126
c ---[2051]---> BDD-cost:  127
c ---[2050]---> BDD-cost:  132
c ---[2049]---> BDD-cost:  132
c ---[2048]---> BDD-cost:  140
c ---[2047]---> BDD-cost:  132
c ---[2046]---> BDD-cost:  137
c ---[2045]---> BDD-cost:  132
c ---[2044]---> BDD-cost:  135
c ---[2043]---> BDD-cost:  132
c ---[2042]---> BDD-cost:  135
c ---[2040]---> BDD-cost:  120
c ---[2039]---> BDD-cost:  140
c ---[2038]---> BDD-cost:  137
c ---[2037]---> BDD-cost:  137
c ---[2036]---> BDD-cost:  132
c ---[2035]---> BDD-cost:  130
c ---[2034]---> BDD-cost:  137
c ---[2033]---> BDD-cost:  135
c ---[2032]---> BDD-cost:  137
c ---[2031]---> BDD-cost:  140
c ---[2028]---> BDD-cost:  137
c ---[2027]---> BDD-cost:  135
c ---[2026]---> BDD-cost:  132
c ---[2025]---> BDD-cost:  137
c ---[2024]---> BDD-cost:  132
c ---[2023]---> BDD-cost:  129
c ---[2022]---> BDD-cost:  132
c ---[2021]---> BDD-cost:  130
c ---[2020]---> BDD-cost:  137
c ---[2019]---> BDD-cost:  132
c ---[2017]---> BDD-cost:  120
c ---[2016]---> BDD-cost:  137
c ---[2015]---> BDD-cost:  137
c ---[2014]---> BDD-cost:  138
c ---[2013]---> BDD-cost:  138
c ---[2012]---> BDD-cost:  132
c ---[2011]---> BDD-cost:  125
c ---[2010]---> BDD-cost:  132
c ---[2009]---> BDD-cost:  140
c ---[2008]---> BDD-cost:  132
c ---[2006]---> BDD-cost:  125
c ---[2005]---> BDD-cost:  137
c ---[2004]---> BDD-cost:  137
c ---[2003]---> BDD-cost:  137
c ---[2002]---> BDD-cost:  127
c ---[2001]---> BDD-cost:  137
c ---[2000]---> BDD-cost:  135
c ---[1999]---> BDD-cost:  132
c ---[1998]---> BDD-cost:  122
c ---[1997]---> BDD-cost:  126
c ---[1995]---> BDD-cost:  130
c ---[1994]---> BDD-cost:  120
c ---[1993]---> BDD-cost:  132
c ---[1992]---> BDD-cost:  137
c ---[1991]---> BDD-cost:  125
c ---[1990]---> BDD-cost:  137
c ---[1989]---> BDD-cost:  140
c ---[1988]---> BDD-cost:  137
c ---[1987]---> BDD-cost:  124
c ---[1986]---> BDD-cost:  132
c ---[1984]---> BDD-cost:  135
c ---[1983]---> BDD-cost:  127
c ---[1982]---> BDD-cost:  143
c ---[1981]---> BDD-cost:  127
c ---[1980]---> BDD-cost:  140
c ---[1979]---> BDD-cost:  127
c ---[1978]---> BDD-cost:  138
c ---[1977]---> BDD-cost:  127
c ---[1976]---> BDD-cost:  130
c ---[1975]---> BDD-cost:  131
c ---[1973]---> BDD-cost:  122
c ---[1972]---> BDD-cost:  127
c ---[1971]---> BDD-cost:  124
c ---[1970]---> BDD-cost:  134
c ---[1969]---> BDD-cost:  135
c ---[1968]---> BDD-cost:  120
c ---[1967]---> BDD-cost:  140
c ---[1966]---> BDD-cost:  120
c ---[1965]---> BDD-cost:  135
c ---[1964]---> BDD-cost:  120
c ---[1962]---> BDD-cost:  140
c ---[1961]---> BDD-cost:  137
c ---[1960]---> BDD-cost:  132
c ---[1959]---> BDD-cost:  137
c ---[1958]---> BDD-cost:  137
c ---[1957]---> BDD-cost:  137
c ---[1956]---> BDD-cost:  140
c ---[1955]---> BDD-cost:  127
c ---[1954]---> BDD-cost:  134
c ---[1953]---> BDD-cost:  124
c ---[1951]---> BDD-cost:  140
c ---[1950]---> BDD-cost:  140
c ---[1949]---> BDD-cost:  140
c ---[1948]---> BDD-cost:  130
c ---[1947]---> BDD-cost:  140
c ---[1946]---> BDD-cost:  140
c ---[1945]---> BDD-cost:  137
c ---[1944]---> BDD-cost:  120
c ---[1943]---> BDD-cost:  134
c ---[1942]---> BDD-cost:  132
c ---[1940]---> BDD-cost:  125
c ---[1939]---> BDD-cost:  132
c ---[1938]---> BDD-cost:  124
c ---[1937]---> BDD-cost:  132
c ---[1936]---> BDD-cost:  140
c ---[1935]---> BDD-cost:  132
c ---[1934]---> BDD-cost:  143
c ---[1933]---> BDD-cost:  134
c ---[1932]---> BDD-cost:  140
c ---[1931]---> BDD-cost:  140
c ---[1929]---> BDD-cost:  140
c ---[1928]---> BDD-cost:  130
c ---[1927]---> BDD-cost:  132
c ---[1926]---> BDD-cost:  140
c ---[1925]---> BDD-cost:  132
c ---[1924]---> BDD-cost:  120
c ---[1923]---> BDD-cost:  132
c ---[1922]---> BDD-cost:  135
c ---[1921]---> BDD-cost:  137
c ---[1920]---> BDD-cost:  124
c ---[1917]---> BDD-cost:  134
c ---[1916]---> BDD-cost:  125
c ---[1915]---> BDD-cost:  132
c ---[1914]---> BDD-cost:  124
c ---[1913]---> BDD-cost:  132
c ---[1912]---> BDD-cost:  137
c ---[1911]---> BDD-cost:  137
c ---[1910]---> BDD-cost:  140
c ---[1909]---> BDD-cost:  127
c ---[1908]---> BDD-cost:  129
c ---[1906]---> BDD-cost:  134
c ---[1905]---> BDD-cost:  140
c ---[1904]---> BDD-cost:  137
c ---[1903]---> BDD-cost:  132
c ---[1902]---> BDD-cost:  137
c ---[1901]---> BDD-cost:  118
c ---[1900]---> BDD-cost:  137
c ---[1899]---> BDD-cost:  140
c ---[1898]---> BDD-cost:  137
c ---[1897]---> BDD-cost:  137
c ---[1895]---> BDD-cost:  132
c ---[1894]---> BDD-cost:  120
c ---[1893]---> BDD-cost:  126
c ---[1892]---> BDD-cost:  132
c ---[1891]---> BDD-cost:  126
c ---[1890]---> BDD-cost:  140
c ---[1889]---> BDD-cost:  140
c ---[1888]---> BDD-cost:  140
c ---[1887]---> BDD-cost:  137
c ---[1886]---> BDD-cost:  140
c ---[1884]---> BDD-cost:  140
c ---[1883]---> BDD-cost:  135
c ---[1882]---> BDD-cost:  140
c ---[1881]---> BDD-cost:  140
c ---[1880]---> BDD-cost:  130
c ---[1879]---> BDD-cost:  122
c ---[1878]---> BDD-cost:  122
c ---[1877]---> BDD-cost:  124
c ---[1876]---> BDD-cost:  140
c ---[1875]---> BDD-cost:  124
c ---[1873]---> BDD-cost:  125
c ---[1872]---> BDD-cost:  140
c ---[1871]---> BDD-cost:  140
c ---[1870]---> BDD-cost:  120
c ---[1869]---> BDD-cost:  140
c ---[1868]---> BDD-cost:  140
c ---[1867]---> BDD-cost:  122
c ---[1866]---> BDD-cost:  127
c ---[1865]---> BDD-cost:  140
c ---[1864]---> BDD-cost:  124
c ---[1862]---> BDD-cost:  137
c ---[1861]---> BDD-cost:  124
c ---[1860]---> BDD-cost:  135
c ---[1859]---> BDD-cost:  140
c ---[1858]---> BDD-cost:  140
c ---[1857]---> BDD-cost:  140
c ---[1856]---> BDD-cost:  122
c ---[1855]---> BDD-cost:  134
c ---[1854]---> BDD-cost:  124
c ---[1853]---> BDD-cost:  135
c ---[1851]---> BDD-cost:  124
c ---[1850]---> BDD-cost:  140
c ---[1849]---> BDD-cost:  122
c ---[1848]---> BDD-cost:  140
c ---[1847]---> BDD-cost:  124
c ---[1846]---> BDD-cost:  118
c ---[1845]---> BDD-cost:  124
c ---[1844]---> BDD-cost:  140
c ---[1843]---> BDD-cost:  120
c ---[1842]---> BDD-cost:  120
c ---[1840]---> BDD-cost:  137
c ---[1839]---> BDD-cost:  137
c ---[1838]---> BDD-cost:  126
c ---[1837]---> BDD-cost:  140
c ---[1836]---> BDD-cost:  132
c ---[1835]---> BDD-cost:  126
c ---[1834]---> BDD-cost:  131
c ---[1833]---> BDD-cost:  135
c ---[1832]---> BDD-cost:  137
c ---[1831]---> BDD-cost:  129
c ---[1829]---> BDD-cost:  134
c ---[1828]---> BDD-cost:  135
c ---[1827]---> BDD-cost:  137
c ---[1826]---> BDD-cost:  127
c ---[1825]---> BDD-cost:  132
c ---[1824]---> BDD-cost:  140
c ---[1823]---> BDD-cost:  137
c ---[1822]---> BDD-cost:  135
c ---[1821]---> BDD-cost:  134
c ---[1820]---> BDD-cost:  137
c ---[1818]---> BDD-cost:  134
c ---[1817]---> BDD-cost:  137
c ---[1816]---> BDD-cost:  140
c ---[1815]---> BDD-cost:  140
c ---[1814]---> BDD-cost:  130
c ---[1813]---> BDD-cost:  137
c ---[1812]---> BDD-cost:  140
c ---[1811]---> BDD-cost:  137
c ---[1810]---> BDD-cost:  118
c ---[1809]---> BDD-cost:  137
c ---[1806]---> BDD-cost:  118
c ---[1805]---> BDD-cost:  126
c ---[1804]---> BDD-cost:  124
c ---[1803]---> BDD-cost:  137
c ---[1802]---> BDD-cost:  132
c ---[1801]---> BDD-cost:  137
c ---[1800]---> BDD-cost:  140
c ---[1799]---> BDD-cost:  137
c ---[1798]---> BDD-cost:  140
c ---[1797]---> BDD-cost:  120
c ---[1795]---> BDD-cost:  122
c ---[1794]---> BDD-cost:  129
c ---[1793]---> BDD-cost:  135
c ---[1792]---> BDD-cost:  134
c ---[1791]---> BDD-cost:  140
c ---[1790]---> BDD-cost:  120
c ---[1789]---> BDD-cost:  135
c ---[1788]---> BDD-cost:  137
c ---[1787]---> BDD-cost:  135
c ---[1786]---> BDD-cost:  137
c ---[1784]---> BDD-cost:  140
c ---[1783]---> BDD-cost:  137
c ---[1782]---> BDD-cost:  135
c ---[1781]---> BDD-cost:  137
c ---[1780]---> BDD-cost:  135
c ---[1779]---> BDD-cost:  134
c ---[1778]---> BDD-cost:  131
c ---[1777]---> BDD-cost:  129
c ---[1776]---> BDD-cost:  132
c ---[1775]---> BDD-cost:  124
c ---[1773]---> BDD-cost:  124
c ---[1772]---> BDD-cost:  132
c ---[1771]---> BDD-cost:  140
c ---[1770]---> BDD-cost:  132
c ---[1769]---> BDD-cost:  135
c ---[1768]---> BDD-cost:  140
c ---[1767]---> BDD-cost:  140
c ---[1766]---> BDD-cost:  143
c ---[1765]---> BDD-cost:  143
c ---[1764]---> BDD-cost:  132
c ---[1762]---> BDD-cost:  134
c ---[1761]---> BDD-cost:  122
c ---[1760]---> BDD-cost:  137
c ---[1759]---> BDD-cost:  132
c ---[1758]---> BDD-cost:  134
c ---[1757]---> BDD-cost:  122
c ---[1756]---> BDD-cost:  137
c ---[1755]---> BDD-cost:  140
c ---[1754]---> BDD-cost:  140
c ---[1753]---> BDD-cost:  135
c ---[1751]---> BDD-cost:  129
c ---[1750]---> BDD-cost:  140
c ---[1749]---> BDD-cost:  129
c ---[1748]---> BDD-cost:  140
c ---[1747]---> BDD-cost:  129
c ---[1746]---> BDD-cost:  118
c ---[1745]---> BDD-cost:  129
c ---[1744]---> BDD-cost:  120
c ---[1743]---> BDD-cost:  120
c ---[1742]---> BDD-cost:  130
c ---[1740]---> BDD-cost:  134
c ---[1739]---> BDD-cost:  131
c ---[1738]---> BDD-cost:  122
c ---[1737]---> BDD-cost:  132
c ---[1736]---> BDD-cost:  140
c ---[1735]---> BDD-cost:  140
c ---[1734]---> BDD-cost:  137
c ---[1733]---> BDD-cost:  122
c ---[1732]---> BDD-cost:  137
c ---[1731]---> BDD-cost:  122
c ---[1729]---> BDD-cost:  140
c ---[1728]---> BDD-cost:  131
c ---[1727]---> BDD-cost:  140
c ---[1726]---> BDD-cost:  140
c ---[1725]---> BDD-cost:  140
c ---[1724]---> BDD-cost:  120
c ---[1723]---> BDD-cost:  129
c ---[1722]---> BDD-cost:  130
c ---[1721]---> BDD-cost:  129
c ---[1720]---> BDD-cost:  140
c ---[1718]---> BDD-cost:  137
c ---[1717]---> BDD-cost:  130
c ---[1716]---> BDD-cost:  132
c ---[1715]---> BDD-cost:  143
c ---[1714]---> BDD-cost:  120
c ---[1713]---> BDD-cost:  135
c ---[1712]---> BDD-cost:  126
c ---[1711]---> BDD-cost:  124
c ---[1710]---> BDD-cost:  124
c ---[1709]---> BDD-cost:  137
c ---[1707]---> BDD-cost:  126
c ---[1706]---> BDD-cost:  127
c ---[1705]---> BDD-cost:  120
c ---[1704]---> BDD-cost:  126
c ---[1703]---> BDD-cost:  137
c ---[1702]---> BDD-cost:  138
c ---[1701]---> BDD-cost:  137
c ---[1700]---> BDD-cost:  135
c ---[1699]---> BDD-cost:  126
c ---[1698]---> BDD-cost:  120
c ---[1694]---> BDD-cost:  120
c ---[1693]---> BDD-cost:  140
c ---[1692]---> BDD-cost:  120
c ---[1691]---> BDD-cost:  131
c ---[1690]---> BDD-cost:  137
c ---[1689]---> BDD-cost:  130
c ---[1688]---> BDD-cost:  132
c ---[1687]---> BDD-cost:  140
c ---[1686]---> BDD-cost:  127
c ---[1685]---> BDD-cost:  135
c ---[1683]---> BDD-cost:  132
c ---[1682]---> BDD-cost:  140
c ---[1681]---> BDD-cost:  132
c ---[1680]---> BDD-cost:  137
c ---[1679]---> BDD-cost:  137
c ---[1678]---> BDD-cost:  130
c ---[1677]---> BDD-cost:  122
c ---[1676]---> BDD-cost:  118
c ---[1675]---> BDD-cost:  118
c ---[1674]---> BDD-cost:  134
c ---[1672]---> BDD-cost:  140
c ---[1671]---> BDD-cost:  129
c ---[1670]---> BDD-cost:  130
c ---[1669]---> BDD-cost:  134
c ---[1668]---> BDD-cost:  134
c ---[1667]---> BDD-cost:  131
c ---[1666]---> BDD-cost:  140
c ---[1665]---> BDD-cost:  120
c ---[1664]---> BDD-cost:  135
c ---[1663]---> BDD-cost:  137
c ---[1661]---> BDD-cost:  140
c ---[1660]---> BDD-cost:  137
c ---[1659]---> BDD-cost:  125
c ---[1658]---> BDD-cost:  137
c ---[1657]---> BDD-cost:  140
c ---[1656]---> BDD-cost:  137
c ---[1655]---> BDD-cost:  137
c ---[1654]---> BDD-cost:  132
c ---[1653]---> BDD-cost:  135
c ---[1652]---> BDD-cost:  137
c ---[1650]---> BDD-cost:  130
c ---[1649]---> BDD-cost:  122
c ---[1648]---> BDD-cost:  140
c ---[1647]---> BDD-cost:  134
c ---[1646]---> BDD-cost:  135
c ---[1645]---> BDD-cost:  129
c ---[1644]---> BDD-cost:  137
c ---[1643]---> BDD-cost:  124
c ---[1642]---> BDD-cost:  137
c ---[1641]---> BDD-cost:  126
c ---[1639]---> BDD-cost:  135
c ---[1638]---> BDD-cost:  137
c ---[1637]---> BDD-cost:  140
c ---[1636]---> BDD-cost:  137
c ---[1635]---> BDD-cost:  126
c ---[1634]---> BDD-cost:  124
c ---[1633]---> BDD-cost:  140
c ---[1632]---> BDD-cost:  120
c ---[1631]---> BDD-cost:  118
c ---[1630]---> BDD-cost:  132
c ---[1628]---> BDD-cost:  140
c ---[1627]---> BDD-cost:  127
c ---[1626]---> BDD-cost:  135
c ---[1625]---> BDD-cost:  127
c ---[1624]---> BDD-cost:  122
c ---[1623]---> BDD-cost:  137
c ---[1622]---> BDD-cost:  143
c ---[1621]---> BDD-cost:  132
c ---[1620]---> BDD-cost:  140
c ---[1619]---> BDD-cost:  137
c ---[1617]---> BDD-cost:  135
c ---[1616]---> BDD-cost:  122
c ---[1615]---> BDD-cost:  140
c ---[1614]---> BDD-cost:  134
c ---[1613]---> BDD-cost:  132
c ---[1612]---> BDD-cost:  134
c ---[1611]---> BDD-cost:  132
c ---[1610]---> BDD-cost:  131
c ---[1609]---> BDD-cost:  143
c ---[1608]---> BDD-cost:  143
c ---[1606]---> BDD-cost:  137
c ---[1605]---> BDD-cost:  135
c ---[1604]---> BDD-cost:  137
c ---[1603]---> BDD-cost:  140
c ---[1602]---> BDD-cost:  137
c ---[1601]---> BDD-cost:  134
c ---[1600]---> BDD-cost:  127
c ---[1599]---> BDD-cost:  133
c ---[1598]---> BDD-cost:  133
c ---[1597]---> BDD-cost:  137
c ---[1595]---> BDD-cost:  125
c ---[1594]---> BDD-cost:  132
c ---[1593]---> BDD-cost:  140
c ---[1592]---> BDD-cost:  137
c ---[1591]---> BDD-cost:  130
c ---[1590]---> BDD-cost:  122
c ---[1589]---> BDD-cost:  137
c ---[1588]---> BDD-cost:  129
c ---[1587]---> BDD-cost:  137
c ---[1586]---> BDD-cost:  124
c ---[1583]---> BDD-cost:  118
c ---[1582]---> BDD-cost:  137
c ---[1581]---> BDD-cost:  135
c ---[1580]---> BDD-cost:  137
c ---[1579]---> BDD-cost:  126
c ---[1578]---> BDD-cost:  132
c ---[1577]---> BDD-cost:  143
c ---[1576]---> BDD-cost:  137
c ---[1575]---> BDD-cost:  140
c ---[1574]---> BDD-cost:  127
c ---[1572]---> BDD-cost:  118
c ---[1571]---> BDD-cost:  137
c ---[1570]---> BDD-cost:  140
c ---[1569]---> BDD-cost:  132
c ---[1568]---> BDD-cost:  135
c ---[1567]---> BDD-cost:  122
c ---[1566]---> BDD-cost:  122
c ---[1565]---> BDD-cost:  129
c ---[1564]---> BDD-cost:  140
c ---[1563]---> BDD-cost:  120
c ---[1561]---> BDD-cost:  135
c ---[1560]---> BDD-cost:  137
c ---[1559]---> BDD-cost:  135
c ---[1558]---> BDD-cost:  132
c ---[1557]---> BDD-cost:  140
c ---[1556]---> BDD-cost:  137
c ---[1555]---> BDD-cost:  118
c ---[1554]---> BDD-cost:  127
c ---[1553]---> BDD-cost:  140
c ---[1552]---> BDD-cost:  132
c ---[1550]---> BDD-cost:  134
c ---[1549]---> BDD-cost:  122
c ---[1548]---> BDD-cost:  135
c ---[1547]---> BDD-cost:  126
c ---[1546]---> BDD-cost:  140
c ---[1545]---> BDD-cost:  120
c ---[1544]---> BDD-cost:  122
c ---[1543]---> BDD-cost:  137
c ---[1542]---> BDD-cost:  127
c ---[1541]---> BDD-cost:  132
c ---[1539]---> BDD-cost:  131
c ---[1538]---> BDD-cost:  132
c ---[1537]---> BDD-cost:  140
c ---[1536]---> BDD-cost:  122
c ---[1535]---> BDD-cost:  122
c ---[1534]---> BDD-cost:  120
c ---[1533]---> BDD-cost:  140
c ---[1532]---> BDD-cost:  137
c ---[1531]---> BDD-cost:  138
c ---[1530]---> BDD-cost:  132
c ---[1528]---> BDD-cost:  140
c ---[1527]---> BDD-cost:  137
c ---[1526]---> BDD-cost:  135
c ---[1525]---> BDD-cost:  137
c ---[1524]---> BDD-cost:  132
c ---[1523]---> BDD-cost:  137
c ---[1522]---> BDD-cost:  143
c ---[1521]---> BDD-cost:  131
c ---[1520]---> BDD-cost:  118
c ---[1519]---> BDD-cost:  126
c ---[1517]---> BDD-cost:  140
c ---[1516]---> BDD-cost:  120
c ---[1515]---> BDD-cost:  135
c ---[1514]---> BDD-cost:  137
c ---[1513]---> BDD-cost:  140
c ---[1512]---> BDD-cost:  132
c ---[1511]---> BDD-cost:  129
c ---[1510]---> BDD-cost:  127
c ---[1509]---> BDD-cost:  135
c ---[1508]---> BDD-cost:  132
c ---[1506]---> BDD-cost:  140
c ---[1505]---> BDD-cost:  124
c ---[1504]---> BDD-cost:  130
c ---[1503]---> BDD-cost:  131
c ---[1502]---> BDD-cost:  140
c ---[1501]---> BDD-cost:  120
c ---[1500]---> BDD-cost:  135
c ---[1499]---> BDD-cost:  137
c ---[1498]---> BDD-cost:  140
c ---[1497]---> BDD-cost:  137
c ---[1495]---> BDD-cost:  137
c ---[1494]---> BDD-cost:  137
c ---[1493]---> BDD-cost:  135
c ---[1492]---> BDD-cost:  134
c ---[1491]---> BDD-cost:  140
c ---[1490]---> BDD-cost:  124
c ---[1489]---> BDD-cost:  135
c ---[1488]---> BDD-cost:  120
c ---[1487]---> BDD-cost:  130
c ---[1486]---> BDD-cost:  132
c ---[1484]---> BDD-cost:  129
c ---[1483]---> BDD-cost:  127
c ---[1482]---> BDD-cost:  140
c ---[1481]---> BDD-cost:  129
c ---[1480]---> BDD-cost:  118
c ---[1479]---> BDD-cost:  134
c ---[1478]---> BDD-cost:  140
c ---[1477]---> BDD-cost:  137
c ---[1476]---> BDD-cost:  132
c ---[1475]---> BDD-cost:  134
c ---[1472]---> BDD-cost:  140
c ---[1471]---> BDD-cost:  129
c ---[1470]---> BDD-cost:  132
c ---[1469]---> BDD-cost:  137
c ---[1468]---> BDD-cost:  132
c ---[1467]---> BDD-cost:  137
c ---[1466]---> BDD-cost:  134
c ---[1465]---> BDD-cost:  122
c ---[1464]---> BDD-cost:  120
c ---[1463]---> BDD-cost:  137
c ---[1461]---> BDD-cost:  130
c ---[1460]---> BDD-cost:  132
c ---[1459]---> BDD-cost:  140
c ---[1458]---> BDD-cost:  131
c ---[1457]---> BDD-cost:  132
c ---[1456]---> BDD-cost:  126
c ---[1455]---> BDD-cost:  140
c ---[1454]---> BDD-cost:  120
c ---[1453]---> BDD-cost:  125
c ---[1452]---> BDD-cost:  137
c ---[1450]---> BDD-cost:  140
c ---[1449]---> BDD-cost:  122
c ---[1448]---> BDD-cost:  132
c ---[1447]---> BDD-cost:  129
c ---[1446]---> BDD-cost:  137
c ---[1445]---> BDD-cost:  134
c ---[1444]---> BDD-cost:  120
c ---[1443]---> BDD-cost:  132
c ---[1442]---> BDD-cost:  132
c ---[1441]---> BDD-cost:  137
c ---[1439]---> BDD-cost:  140
c ---[1438]---> BDD-cost:  134
c ---[1437]---> BDD-cost:  135
c ---[1436]---> BDD-cost:  129
c ---[1435]---> BDD-cost:  140
c ---[1434]---> BDD-cost:  137
c ---[1433]---> BDD-cost:  126
c ---[1432]---> BDD-cost:  131
c ---[1431]---> BDD-cost:  126
c ---[1430]---> BDD-cost:  126
c ---[1428]---> BDD-cost:  140
c ---[1427]---> BDD-cost:  137
c ---[1426]---> BDD-cost:  138
c ---[1425]---> BDD-cost:  132
c ---[1424]---> BDD-cost:  140
c ---[1423]---> BDD-cost:  124
c ---[1422]---> BDD-cost:  140
c ---[1421]---> BDD-cost:  131
c ---[1420]---> BDD-cost:  140
c ---[1419]---> BDD-cost:  120
c ---[1417]---> BDD-cost:  135
c ---[1416]---> BDD-cost:  129
c ---[1415]---> BDD-cost:  118
c ---[1414]---> BDD-cost:  134
c ---[1413]---> BDD-cost:  138
c ---[1412]---> BDD-cost:  134
c ---[1411]---> BDD-cost:  143
c ---[1410]---> BDD-cost:  129
c ---[1409]---> BDD-cost:  140
c ---[1408]---> BDD-cost:  126
c ---[1406]---> BDD-cost:  137
c ---[1405]---> BDD-cost:  134
c ---[1404]---> BDD-cost:  137
c ---[1403]---> BDD-cost:  129
c ---[1402]---> BDD-cost:  130
c ---[1401]---> BDD-cost:  126
c ---[1400]---> BDD-cost:  135
c ---[1399]---> BDD-cost:  120
c ---[1398]---> BDD-cost:  140
c ---[1397]---> BDD-cost:  127
c ---[1395]---> BDD-cost:  137
c ---[1394]---> BDD-cost:  137
c ---[1393]---> BDD-cost:  137
c ---[1392]---> BDD-cost:  129
c ---[1391]---> BDD-cost:  134
c ---[1390]---> BDD-cost:  120
c ---[1389]---> BDD-cost:  135
c ---[1388]---> BDD-cost:  127
c ---[1387]---> BDD-cost:  132
c ---[1386]---> BDD-cost:  137
c ---[1384]---> BDD-cost:  140
c ---[1383]---> BDD-cost:  137
c ---[1382]---> BDD-cost:  129
c ---[1381]---> BDD-cost:  126
c ---[1380]---> BDD-cost:  127
c ---[1379]---> BDD-cost:  129
c ---[1378]---> BDD-cost:  130
c ---[1377]---> BDD-cost:  122
c ---[1376]---> BDD-cost:  140
c ---[1375]---> BDD-cost:  122
c ---[1373]---> BDD-cost:  118
c ---[1112]---> BDD-cost:    6
c ---[1111]---> BDD-cost:    6
c ---[1110]---> BDD-cost:    6
c ---[1109]---> BDD-cost:    6
c ---[1108]---> BDD-cost:    6
c ---[1107]---> BDD-cost:    6
c ---[1105]---> BDD-cost:    6
c ---[1104]---> BDD-cost:    6
c ---[1103]---> BDD-cost:    6
c ---[1102]---> BDD-cost:    6
c ---[1101]---> BDD-cost:    6
c ---[1100]---> BDD-cost:    6
c ---[1099]---> BDD-cost:    6
c ---[1098]---> BDD-cost:    6
c ---[1097]---> BDD-cost:    6
c ---[1096]---> BDD-cost:    6
c ---[1094]---> BDD-cost:    6
c ---[1093]---> BDD-cost:    6
c ---[1092]---> BDD-cost:    6
c ---[1091]---> BDD-cost:    6
c ---[1090]---> BDD-cost:    6
c ---[1089]---> BDD-cost:    6
c ---[1088]---> BDD-cost:    6
c ---[1087]---> BDD-cost:    6
c ---[1086]---> BDD-cost:    6
c ---[1085]---> BDD-cost:    6
c ---[1083]---> BDD-cost:    6
c ---[1082]---> BDD-cost:    6
c ---[1081]---> BDD-cost:    6
c ---[1080]---> BDD-cost:    6
c ---[1079]---> BDD-cost:    6
c ---[1078]---> BDD-cost:    6
c ---[1077]---> BDD-cost:    6
c ---[1076]---> BDD-cost:    6
c ---[1075]---> BDD-cost:    6
c ---[1074]---> BDD-cost:    6
c ---[1071]---> BDD-cost:    6
c ---[1070]---> BDD-cost:    6
c ---[1069]---> BDD-cost:    6
c ---[1068]---> BDD-cost:    6
c ---[1067]---> BDD-cost:    6
c ---[1066]---> BDD-cost:    6
c ---[1065]---> BDD-cost:    6
c ---[1064]---> BDD-cost:    6
c ---[1063]---> BDD-cost:    6
c ---[1062]---> BDD-cost:    6
c ---[1060]---> BDD-cost:    6
c ---[1059]---> BDD-cost:    6
c ---[1058]---> BDD-cost:    6
c ---[1057]---> BDD-cost:    6
c ---[1056]---> BDD-cost:    6
c ---[1055]---> BDD-cost:    6
c ---[1054]---> BDD-cost:    6
c ---[1053]---> BDD-cost:    6
c ---[1052]---> BDD-cost:    6
c ---[1051]---> BDD-cost:    6
c ---[1049]---> BDD-cost:    6
c ---[1048]---> BDD-cost:    6
c ---[1047]---> BDD-cost:    6
c ---[1046]---> BDD-cost:    6
c ---[1045]---> BDD-cost:    6
c ---[1044]---> BDD-cost:    6
c ---[1043]---> BDD-cost:    6
c ---[1042]---> BDD-cost:    6
c ---[1041]---> BDD-cost:    6
c ---[1040]---> BDD-cost:    6
c ---[1038]---> BDD-cost:    6
c ---[1037]---> BDD-cost:    6
c ---[1036]---> BDD-cost:    6
c ---[1035]---> BDD-cost:    6
c ---[1034]---> BDD-cost:    6
c ---[1033]---> BDD-cost:    6
c ---[1032]---> BDD-cost:    6
c ---[1031]---> BDD-cost:    6
c ---[1030]---> BDD-cost:    6
c ---[1029]---> BDD-cost:    6
c ---[1027]---> BDD-cost:    6
c ---[1026]---> BDD-cost:    6
c ---[1025]---> BDD-cost:    6
c ---[1024]---> BDD-cost:    6
c ---[1023]---> BDD-cost:    6
c ---[1022]---> BDD-cost:    6
c ---[1021]---> BDD-cost:    6
c ---[1020]---> BDD-cost:    6
c ---[1019]---> BDD-cost:    6
c ---[1018]---> BDD-cost:    6
c ---[1016]---> BDD-cost:    6
c ---[1015]---> BDD-cost:    6
c ---[1014]---> BDD-cost:    6
c ---[1013]---> BDD-cost:    6
c ---[1012]---> BDD-cost:    6
c ---[1011]---> BDD-cost:    6
c ---[1010]---> BDD-cost:    6
c ---[1009]---> BDD-cost:    6
c ---[1008]---> BDD-cost:    6
c ---[1007]---> BDD-cost:    6
c ---[1005]---> BDD-cost:    6
c ---[1004]---> BDD-cost:    6
c ---[1003]---> BDD-cost:    6
c ---[1002]---> BDD-cost:    6
c ---[1001]---> BDD-cost:    6
c ---[1000]---> BDD-cost:    6
c ---[ 999]---> BDD-cost:    6
c ---[ 998]---> BDD-cost:    6
c ---[ 997]---> BDD-cost:    6
c ---[ 996]---> BDD-cost:  117
c ---[ 994]---> BDD-cost:  119
c ---[ 993]---> BDD-cost:   88
c ---[ 992]---> BDD-cost:   88
c ---[ 991]---> BDD-cost:   88
c ---[ 990]---> BDD-cost:   88
c ---[ 989]---> BDD-cost:  125
c ---[ 988]---> BDD-cost:  119
c ---[ 987]---> BDD-cost:   88
c ---[ 986]---> BDD-cost:   88
c ---[ 985]---> BDD-cost:   88
c ---[ 983]---> BDD-cost:   88
c ---[ 982]---> BDD-cost:  125
c ---[ 981]---> BDD-cost:  119
c ---[ 980]---> BDD-cost:   88
c ---[ 979]---> BDD-cost:   88
c ---[ 978]---> BDD-cost:   88
c ---[ 977]---> BDD-cost:   88
c ---[ 976]---> BDD-cost:  117
c ---[ 975]---> BDD-cost:  119
c ---[ 974]---> BDD-cost:   88
c ---[ 972]---> BDD-cost:   88
c ---[ 971]---> BDD-cost:   88
c ---[ 970]---> BDD-cost:   88
c ---[ 969]---> BDD-cost:  125
c ---[ 968]---> BDD-cost:  119
c ---[ 967]---> BDD-cost:   88
c ---[ 966]---> BDD-cost:   88
c ---[ 965]---> BDD-cost:   88
c ---[ 964]---> BDD-cost:   88
c ---[ 963]---> BDD-cost:  117
c ---[ 960]---> BDD-cost:  119
c ---[ 959]---> BDD-cost:   88
c ---[ 958]---> BDD-cost:   88
c ---[ 957]---> BDD-cost:   88
c ---[ 956]---> BDD-cost:   88
c ---[ 955]---> BDD-cost:  121
c ---[ 954]---> BDD-cost:  119
c ---[ 953]---> BDD-cost:   88
c ---[ 952]---> BDD-cost:   88
c ---[ 951]---> BDD-cost:   88
c ---[ 949]---> BDD-cost:   88
c ---[ 948]---> BDD-cost:  123
c ---[ 947]---> BDD-cost:  119
c ---[ 946]---> BDD-cost:   88
c ---[ 945]---> BDD-cost:   88
c ---[ 944]---> BDD-cost:   88
c ---[ 943]---> BDD-cost:   88
c ---[ 942]---> BDD-cost:  117
c ---[ 941]---> BDD-cost:  119
c ---[ 940]---> BDD-cost:   88
c ---[ 938]---> BDD-cost:   88
c ---[ 937]---> BDD-cost:   88
c ---[ 936]---> BDD-cost:   88
c ---[ 935]---> BDD-cost:  125
c ---[ 934]---> BDD-cost:  119
c ---[ 933]---> BDD-cost:   88
c ---[ 932]---> BDD-cost:   88
c ---[ 931]---> BDD-cost:   88
c ---[ 930]---> BDD-cost:   88
c ---[ 929]---> BDD-cost:  125
c ---[ 927]---> BDD-cost:  119
c ---[ 926]---> BDD-cost:   88
c ---[ 925]---> BDD-cost:   88
c ---[ 924]---> BDD-cost:   88
c ---[ 923]---> BDD-cost:   88
c ---[ 922]---> BDD-cost:  125
c ---[ 921]---> BDD-cost:  119
c ---[ 920]---> BDD-cost:   88
c ---[ 919]---> BDD-cost:   88
c ---[ 918]---> BDD-cost:   88
c ---[ 916]---> BDD-cost:   88
c ---[ 915]---> BDD-cost:  117
c ---[ 914]---> BDD-cost:  119
c ---[ 913]---> BDD-cost:   88
c ---[ 912]---> BDD-cost:   88
c ---[ 911]---> BDD-cost:   88
c ---[ 910]---> BDD-cost:   88
c ---[ 909]---> BDD-cost:  125
c ---[ 908]---> BDD-cost:  119
c ---[ 907]---> BDD-cost:   88
c ---[ 905]---> BDD-cost:   88
c ---[ 904]---> BDD-cost:   88
c ---[ 903]---> BDD-cost:   88
c ---[ 902]---> BDD-cost:  125
c ---[ 901]---> BDD-cost:  119
c ---[ 900]---> BDD-cost:   88
c ---[ 899]---> BDD-cost:   88
c ---[ 898]---> BDD-cost:   88
c ---[ 897]---> BDD-cost:   88
c ---[ 896]---> BDD-cost:  125
c ---[ 894]---> BDD-cost:  119
c ---[ 893]---> BDD-cost:   88
c ---[ 892]---> BDD-cost:   88
c ---[ 891]---> BDD-cost:   88
c ---[ 890]---> BDD-cost:   88
c ---[ 889]---> BDD-cost:  125
c ---[ 888]---> BDD-cost:  119
c ---[ 887]---> BDD-cost:   88
c ---[ 886]---> BDD-cost:   88
c ---[ 885]---> BDD-cost:   88
c ---[ 883]---> BDD-cost:   88
c ---[ 882]---> BDD-cost:  123
c ---[ 881]---> BDD-cost:  119
c ---[ 880]---> BDD-cost:   88
c ---[ 879]---> BDD-cost:   88
c ---[ 878]---> BDD-cost:   88
c ---[ 877]---> BDD-cost:   88
c ---[ 876]---> BDD-cost:  117
c ---[ 875]---> BDD-cost:  119
c ---[ 874]---> BDD-cost:   88
c ---[ 872]---> BDD-cost:   88
c ---[ 871]---> BDD-cost:   88
c ---[ 870]---> BDD-cost:   88
c ---[ 869]---> BDD-cost:  117
c ---[ 868]---> BDD-cost:  119
c ---[ 867]---> BDD-cost:   88
c ---[ 866]---> BDD-cost:   88
c ---[ 865]---> BDD-cost:   88
c ---[ 864]---> BDD-cost:   88
c ---[ 863]---> BDD-cost:  121
c ---[ 861]---> BDD-cost:  119
c ---[ 860]---> BDD-cost:   88
c ---[ 859]---> BDD-cost:   88
c ---[ 858]---> BDD-cost:   88
c ---[ 857]---> BDD-cost:   88
c ---[ 856]---> BDD-cost:  117
c ---[ 855]---> BDD-cost:  119
c ---[ 854]---> BDD-cost:   88
c ---[ 853]---> BDD-cost:   88
c ---[ 852]---> BDD-cost:   88
c ---[ 849]---> BDD-cost:   88
c ---[ 848]---> BDD-cost:  117
c ---[ 847]---> BDD-cost:  119
c ---[ 846]---> BDD-cost:   88
c ---[ 845]---> BDD-cost:   88
c ---[ 844]---> BDD-cost:   88
c ---[ 843]---> BDD-cost:   88
c ---[ 842]---> BDD-cost:  117
c ---[ 841]---> BDD-cost:  119
c ---[ 840]---> BDD-cost:   88
c ---[ 838]---> BDD-cost:   88
c ---[ 837]---> BDD-cost:   88
c ---[ 836]---> BDD-cost:   88
c ---[ 835]---> BDD-cost:  125
c ---[ 834]---> BDD-cost:  119
c ---[ 833]---> BDD-cost:   88
c ---[ 832]---> BDD-cost:   88
c ---[ 831]---> BDD-cost:   88
c ---[ 830]---> BDD-cost:   88
c ---[ 829]---> BDD-cost:  125
c ---[ 827]---> BDD-cost:  119
c ---[ 826]---> BDD-cost:   88
c ---[ 825]---> BDD-cost:   88
c ---[ 824]---> BDD-cost:   88
c ---[ 823]---> BDD-cost:   88
c ---[ 822]---> BDD-cost:  125
c ---[ 821]---> BDD-cost:  119
c ---[ 820]---> BDD-cost:   88
c ---[ 819]---> BDD-cost:   88
c ---[ 818]---> BDD-cost:   88
c ---[ 816]---> BDD-cost:   88
c ---[ 815]---> BDD-cost:  125
c ---[ 814]---> BDD-cost:  119
c ---[ 813]---> BDD-cost:   88
c ---[ 812]---> BDD-cost:   88
c ---[ 811]---> BDD-cost:   88
c ---[ 810]---> BDD-cost:   88
c ---[ 809]---> BDD-cost:  125
c ---[ 808]---> BDD-cost:  119
c ---[ 807]---> BDD-cost:   88
c ---[ 805]---> BDD-cost:   88
c ---[ 804]---> BDD-cost:   88
c ---[ 803]---> BDD-cost:   88
c ---[ 802]---> BDD-cost:  125
c ---[ 801]---> BDD-cost:  119
c ---[ 800]---> BDD-cost:   88
c ---[ 799]---> BDD-cost:   88
c ---[ 798]---> BDD-cost:   88
c ---[ 797]---> BDD-cost:   88
c ---[ 796]---> BDD-cost:  125
c ---[ 794]---> BDD-cost:  119
c ---[ 793]---> BDD-cost:   88
c ---[ 792]---> BDD-cost:   88
c ---[ 791]---> BDD-cost:   88
c ---[ 790]---> BDD-cost:   88
c ---[ 789]---> BDD-cost:  123
c ---[ 788]---> BDD-cost:  119
c ---[ 787]---> BDD-cost:   88
c ---[ 786]---> BDD-cost:   88
c ---[ 785]---> BDD-cost:   88
c ---[ 783]---> BDD-cost:   88
c ---[ 782]---> BDD-cost:  117
c ---[ 781]---> BDD-cost:  119
c ---[ 780]---> BDD-cost:   88
c ---[ 779]---> BDD-cost:   88
c ---[ 778]---> BDD-cost:   88
c ---[ 777]---> BDD-cost:   88
c ---[ 776]---> BDD-cost:  117
c ---[ 775]---> BDD-cost:  119
c ---[ 774]---> BDD-cost:   88
c ---[ 772]---> BDD-cost:   88
c ---[ 771]---> BDD-cost:   88
c ---[ 770]---> BDD-cost:   88
c ---[ 769]---> BDD-cost:  117
c ---[ 768]---> BDD-cost:  119
c ---[ 767]---> BDD-cost:   88
c ---[ 766]---> BDD-cost:   88
c ---[ 765]---> BDD-cost:   88
c ---[ 764]---> BDD-cost:   88
c ---[ 763]---> BDD-cost:  125
c ---[ 761]---> BDD-cost:  119
c ---[ 760]---> BDD-cost:   88
c ---[ 759]---> BDD-cost:   88
c ---[ 758]---> BDD-cost:   88
c ---[ 757]---> BDD-cost:   88
c ---[ 756]---> BDD-cost:  117
c ---[ 755]---> BDD-cost:  119
c ---[ 754]---> BDD-cost:   88
c ---[ 753]---> BDD-cost:   88
c ---[ 752]---> BDD-cost:   88
c ---[ 750]---> BDD-cost:   88
c ---[ 749]---> BDD-cost:  117
c ---[ 748]---> BDD-cost:  119
c ---[ 747]---> BDD-cost:   88
c ---[ 746]---> BDD-cost:   88
c ---[ 745]---> BDD-cost:   88
c ---[ 744]---> BDD-cost:   88
c ---[ 743]---> BDD-cost:  117
c ---[ 742]---> BDD-cost:  119
c ---[ 741]---> BDD-cost:   88
c ---[ 738]---> BDD-cost:   88
c ---[ 737]---> BDD-cost:   88
c ---[ 736]---> BDD-cost:   88
c ---[ 735]---> BDD-cost:  125
c ---[ 734]---> BDD-cost:  119
c ---[ 733]---> BDD-cost:   88
c ---[ 732]---> BDD-cost:   88
c ---[ 731]---> BDD-cost:   88
c ---[ 730]---> BDD-cost:   88
c ---[ 729]---> BDD-cost:  117
c ---[ 727]---> BDD-cost:  119
c ---[ 726]---> BDD-cost:   88
c ---[ 725]---> BDD-cost:   88
c ---[ 724]---> BDD-cost:   88
c ---[ 723]---> BDD-cost:   88
c ---[ 722]---> BDD-cost:  125
c ---[ 721]---> BDD-cost:  119
c ---[ 720]---> BDD-cost:   88
c ---[ 719]---> BDD-cost:   88
c ---[ 718]---> BDD-cost:   88
c ---[ 716]---> BDD-cost:   88
c ---[ 715]---> BDD-cost:  125
c ---[ 714]---> BDD-cost:  119
c ---[ 713]---> BDD-cost:   88
c ---[ 712]---> BDD-cost:   88
c ---[ 711]---> BDD-cost:   88
c ---[ 710]---> BDD-cost:   88
c ---[ 709]---> BDD-cost:  117
c ---[ 708]---> BDD-cost:  119
c ---[ 707]---> BDD-cost:   88
c ---[ 705]---> BDD-cost:   88
c ---[ 704]---> BDD-cost:   88
c ---[ 703]---> BDD-cost:   88
c ---[ 702]---> BDD-cost:  117
c ---[ 701]---> BDD-cost:  119
c ---[ 700]---> BDD-cost:   88
c ---[ 699]---> BDD-cost:   88
c ---[ 698]---> BDD-cost:   88
c ---[ 697]---> BDD-cost:   88
c ---[ 696]---> BDD-cost:  117
c ---[ 694]---> BDD-cost:  119
c ---[ 693]---> BDD-cost:   88
c ---[ 692]---> BDD-cost:   88
c ---[ 691]---> BDD-cost:   88
c ---[ 690]---> BDD-cost:   88
c ---[ 689]---> BDD-cost:  117
c ---[ 688]---> BDD-cost:  119
c ---[ 687]---> BDD-cost:   88
c ---[ 686]---> BDD-cost:   88
c ---[ 685]---> BDD-cost:   88
c ---[ 683]---> BDD-cost:   88
c ---[ 682]---> BDD-cost:  117
c ---[ 681]---> BDD-cost:  119
c ---[ 680]---> BDD-cost:   88
c ---[ 679]---> BDD-cost:   88
c ---[ 678]---> BDD-cost:   88
c ---[ 677]---> BDD-cost:   88
c ---[ 676]---> BDD-cost:  125
c ---[ 675]---> BDD-cost:  119
c ---[ 674]---> BDD-cost:   88
c ---[ 672]---> BDD-cost:   88
c ---[ 671]---> BDD-cost:   88
c ---[ 670]---> BDD-cost:   88
c ---[ 669]---> BDD-cost:  125
c ---[ 668]---> BDD-cost:  119
c ---[ 667]---> BDD-cost:   88
c ---[ 666]---> BDD-cost:   88
c ---[ 665]---> BDD-cost:   88
c ---[ 664]---> BDD-cost:   88
c ---[ 663]---> BDD-cost:  123
c ---[ 661]---> BDD-cost:  119
c ---[ 660]---> BDD-cost:   88
c ---[ 659]---> BDD-cost:   88
c ---[ 658]---> BDD-cost:   88
c ---[ 657]---> BDD-cost:   88
c ---[ 656]---> BDD-cost:  125
c ---[ 655]---> BDD-cost:  119
c ---[ 654]---> BDD-cost:   88
c ---[ 653]---> BDD-cost:   88
c ---[ 652]---> BDD-cost:   88
c ---[ 650]---> BDD-cost:   88
c ---[ 649]---> BDD-cost:  125
c ---[ 648]---> BDD-cost:  119
c ---[ 647]---> BDD-cost:   88
c ---[ 646]---> BDD-cost:   88
c ---[ 645]---> BDD-cost:   88
c ---[ 644]---> BDD-cost:   88
c ---[ 643]---> BDD-cost:  125
c ---[ 642]---> BDD-cost:  119
c ---[ 641]---> BDD-cost:   88
c ---[ 639]---> BDD-cost:   88
c ---[ 638]---> BDD-cost:   88
c ---[ 637]---> BDD-cost:   88
c ---[ 636]---> BDD-cost:  117
c ---[ 635]---> BDD-cost:  119
c ---[ 634]---> BDD-cost:   88
c ---[ 633]---> BDD-cost:   88
c ---[ 632]---> BDD-cost:   88
c ---[ 631]---> BDD-cost:   88
c ---[ 630]---> BDD-cost:  117
c ---[ 629]---> BDD-cost:   26
c ---[ 628]---> BDD-cost:   26
c ---[ 627]---> BDD-cost:   26
c ---[ 626]---> BDD-cost:   26
c ---[ 625]---> BDD-cost:   26
c ---[ 624]---> BDD-cost:   26
c ---[ 623]---> BDD-cost:   26
c ---[ 622]---> BDD-cost:   26
c ---[ 621]---> BDD-cost:   26
c ---[ 620]---> BDD-cost:   26
c ---[ 619]---> BDD-cost:   26
c ---[ 618]---> BDD-cost:   26
c ---[ 617]---> BDD-cost:   26
c ---[ 616]---> BDD-cost:   26
c ---[ 615]---> BDD-cost:   26
c ---[ 614]---> BDD-cost:   26
c ---[ 613]---> BDD-cost:   26
c ---[ 612]---> BDD-cost:   26
c ---[ 611]---> BDD-cost:   26
c ---[ 610]---> BDD-cost:   26
c ---[ 609]---> BDD-cost:   26
c ---[ 608]---> BDD-cost:   26
c ---[ 607]---> BDD-cost:   26
c ---[ 606]---> BDD-cost:   26
c ---[ 605]---> BDD-cost:   26
c ---[ 604]---> BDD-cost:   26
c ---[ 603]---> BDD-cost:   26
c ---[ 602]---> BDD-cost:   26
c ---[ 601]---> BDD-cost:   26
c ---[ 600]---> BDD-cost:   26
c ---[ 599]---> BDD-cost:   26
c ---[ 598]---> BDD-cost:   26
c ---[ 597]---> BDD-cost:   26
c ---[ 596]---> BDD-cost:   26
c ---[ 595]---> BDD-cost:   26
c ---[ 594]---> BDD-cost:   26
c ---[ 593]---> BDD-cost:   26
c ---[ 592]---> BDD-cost:   26
c ---[ 591]---> BDD-cost:   26
c ---[ 590]---> BDD-cost:   26
c ---[ 589]---> BDD-cost:   26
c ---[ 588]---> BDD-cost:   26
c ---[ 587]---> BDD-cost:   26
c ---[ 586]---> BDD-cost:   26
c ---[ 585]---> BDD-cost:   26
c ---[ 584]---> BDD-cost:   26
c ---[ 583]---> BDD-cost:   26
c ---[ 582]---> BDD-cost:   26
c ---[ 581]---> BDD-cost:   26
c ---[ 580]---> BDD-cost:   26
c ---[ 579]---> BDD-cost:   26
c ---[ 578]---> BDD-cost:   26
c ---[ 577]---> BDD-cost:   26
c ---[ 576]---> BDD-cost:   26
c ---[ 575]---> BDD-cost:   26
c ---[ 574]---> BDD-cost:   26
c ---[ 573]---> BDD-cost:   26
c ---[ 572]---> BDD-cost:   26
c ---[ 571]---> BDD-cost:   26
c ---[ 570]---> BDD-cost:   26
c ---[ 569]---> BDD-cost:   26
c ---[ 568]---> BDD-cost:   26
c ---[ 567]---> BDD-cost:   26
c ---[ 566]---> BDD-cost:   26
c ---[ 565]---> BDD-cost:   26
c ---[ 564]---> BDD-cost:   26
c ---[ 563]---> BDD-cost:   26
c ---[ 562]---> BDD-cost:   26
c ---[ 561]---> BDD-cost:   26
c ---[ 560]---> BDD-cost:   26
c ---[ 559]---> BDD-cost:   26
c ---[ 558]---> BDD-cost:   26
c ---[ 557]---> BDD-cost:   26
c ---[ 556]---> BDD-cost:   26
c ---[ 555]---> BDD-cost:   26
c ---[ 554]---> BDD-cost:   26
c ---[ 553]---> BDD-cost:   26
c ---[ 552]---> BDD-cost:   26
c ---[ 551]---> BDD-cost:   26
c ---[ 550]---> BDD-cost:   26
c ---[ 549]---> BDD-cost:   26
c ---[ 548]---> BDD-cost:   26
c ---[ 547]---> BDD-cost:   26
c ---[ 546]---> BDD-cost:   26
c ---[ 545]---> BDD-cost:   26
c ---[ 544]---> BDD-cost:   26
c ---[ 543]---> BDD-cost:   26
c ---[ 542]---> BDD-cost:   26
c ---[ 541]---> BDD-cost:   26
c ---[ 540]---> BDD-cost:   26
c ---[ 539]---> BDD-cost:   26
c ---[ 538]---> BDD-cost:   26
c ---[ 537]---> BDD-cost:   26
c ---[ 536]---> BDD-cost:   26
c ---[ 535]---> BDD-cost:   26
c ---[ 534]---> BDD-cost:   26
c ---[ 533]---> BDD-cost:   26
c ---[ 532]---> BDD-cost:   26
c ---[ 531]---> BDD-cost:   26
c ---[ 530]---> BDD-cost:   26
c ---[ 529]---> BDD-cost:   26
c ---[ 528]---> BDD-cost:   26
c ---[ 527]---> BDD-cost:   26
c ---[ 526]---> BDD-cost:   26
c ---[ 525]---> BDD-cost:   26
c ---[ 524]---> BDD-cost:   26
c ---[ 523]---> BDD-cost:   26
c ---[ 522]---> BDD-cost:   26
c ---[ 521]---> BDD-cost:   26
c ---[ 520]---> BDD-cost:   26
c ---[ 519]---> BDD-cost:   26
c ---[ 518]---> BDD-cost:   26
c ---[ 517]---> BDD-cost:   26
c ---[ 516]---> BDD-cost:   26
c ---[ 515]---> BDD-cost:   26
c ---[ 514]---> BDD-cost:   26
c ---[ 513]---> BDD-cost:   26
c ---[ 512]---> BDD-cost:   26
c ---[ 511]---> BDD-cost:   26
c ---[ 510]---> BDD-cost:   26
c ---[ 509]---> BDD-cost:   26
c ---[ 508]---> BDD-cost:   26
c ---[ 507]---> BDD-cost:   26
c ---[ 506]---> BDD-cost:   26
c ---[ 505]---> BDD-cost:   26
c ---[ 504]---> BDD-cost:   26
c ---[ 503]---> BDD-cost:   26
c ---[ 502]---> BDD-cost:   26
c ---[ 501]---> BDD-cost:   26
c ---[ 500]---> BDD-cost:   26
c ---[ 499]---> BDD-cost:   26
c ---[ 498]---> BDD-cost:   26
c ---[ 497]---> BDD-cost:   26
c ---[ 496]---> BDD-cost:   26
c ---[ 495]---> BDD-cost:   26
c ---[ 494]---> BDD-cost:   26
c ---[ 493]---> BDD-cost:   26
c ---[ 492]---> BDD-cost:   26
c ---[ 491]---> BDD-cost:   26
c ---[ 490]---> BDD-cost:   26
c ---[ 489]---> BDD-cost:   26
c ---[ 488]---> BDD-cost:   26
c ---[ 487]---> BDD-cost:   26
c ---[ 486]---> BDD-cost:   26
c ---[ 485]---> BDD-cost:   26
c ---[ 484]---> BDD-cost:   26
c ---[ 483]---> BDD-cost:   26
c ---[ 482]---> BDD-cost:   26
c ---[ 481]---> BDD-cost:   26
c ---[ 480]---> BDD-cost:   26
c ---[ 479]---> BDD-cost:   26
c ---[ 478]---> BDD-cost:   26
c ---[ 477]---> BDD-cost:   26
c ---[ 476]---> BDD-cost:   26
c ---[ 475]---> BDD-cost:   26
c ---[ 474]---> BDD-cost:   26
c ---[ 473]---> BDD-cost:   26
c ---[ 472]---> BDD-cost:   26
c ---[ 471]---> BDD-cost:   26
c ---[ 470]---> BDD-cost:   26
c ---[ 469]---> BDD-cost:   26
c ---[ 468]---> BDD-cost:   26
c ---[ 467]---> BDD-cost:   26
c ---[ 466]---> BDD-cost:   26
c ---[ 465]---> BDD-cost:   26
c ---[ 464]---> BDD-cost:   26
c ---[ 463]---> BDD-cost:   26
c ---[ 462]---> BDD-cost:   26
c ---[ 461]---> BDD-cost:   26
c ---[ 460]---> BDD-cost:   26
c ---[ 459]---> BDD-cost:   26
c ---[ 458]---> BDD-cost:   26
c ---[ 457]---> BDD-cost:   26
c ---[ 456]---> BDD-cost:   26
c ---[ 455]---> BDD-cost:   26
c ---[ 454]---> BDD-cost:   26
c ---[ 453]---> BDD-cost:   26
c ---[ 452]---> BDD-cost:   26
c ---[ 451]---> BDD-cost:   26
c ---[ 450]---> BDD-cost:   26
c ---[ 449]---> BDD-cost:   26
c ---[ 448]---> BDD-cost:   26
c ---[ 447]---> BDD-cost:   26
c ---[ 446]---> BDD-cost:   26
c ---[ 445]---> BDD-cost:   26
c ---[ 444]---> BDD-cost:   26
c ---[ 443]---> BDD-cost:   26
c ---[ 442]---> BDD-cost:   26
c ---[ 441]---> BDD-cost:   26
c ---[ 440]---> BDD-cost:   26
c ---[ 439]---> BDD-cost:   26
c ---[ 438]---> BDD-cost:   26
c ---[ 437]---> BDD-cost:   26
c ---[ 436]---> BDD-cost:   26
c ---[ 435]---> BDD-cost:   26
c ---[ 434]---> BDD-cost:   26
c ---[ 433]---> BDD-cost:   26
c ---[ 432]---> BDD-cost:   26
c ---[ 431]---> BDD-cost:   26
c ---[ 430]---> BDD-cost:   26
c ---[ 429]---> BDD-cost:   26
c ---[ 428]---> BDD-cost:   26
c ---[ 427]---> BDD-cost:   26
c ---[ 426]---> BDD-cost:   26
c ---[ 425]---> BDD-cost:   26
c ---[ 424]---> BDD-cost:   26
c ---[ 423]---> BDD-cost:   26
c ---[ 422]---> BDD-cost:   26
c ---[ 421]---> BDD-cost:   26
c ---[ 420]---> BDD-cost:   26
c ---[ 419]---> BDD-cost:   26
c ---[ 418]---> BDD-cost:   26
c ---[ 417]---> BDD-cost:   26
c ---[ 416]---> BDD-cost:   26
c ---[ 415]---> BDD-cost:   26
c ---[ 414]---> BDD-cost:   26
c ---[ 413]---> BDD-cost:   26
c ---[ 412]---> BDD-cost:   26
c ---[ 411]---> BDD-cost:   26
c ---[ 410]---> BDD-cost:   26
c ---[ 409]---> BDD-cost:   26
c ---[ 408]---> BDD-cost:   26
c ---[ 407]---> BDD-cost:   26
c ---[ 406]---> BDD-cost:   26
c ---[ 405]---> BDD-cost:   26
c ---[ 404]---> BDD-cost:   26
c ---[ 403]---> BDD-cost:   26
c ---[ 402]---> BDD-cost:   26
c ---[ 401]---> BDD-cost:   26
c ---[ 400]---> BDD-cost:   26
c ---[ 399]---> BDD-cost:   26
c ---[ 398]---> BDD-cost:   26
c ---[ 397]---> BDD-cost:   26
c ---[ 396]---> BDD-cost:   26
c ---[ 395]---> BDD-cost:   26
c ---[ 394]---> BDD-cost:   26
c ---[ 393]---> BDD-cost:   26
c ---[ 392]---> BDD-cost:   26
c ---[ 391]---> BDD-cost:   26
c ---[ 390]---> BDD-cost:   26
c ---[ 389]---> BDD-cost:   26
c ---[ 388]---> BDD-cost:   26
c ---[ 387]---> BDD-cost:   26
c ---[ 386]---> BDD-cost:   26
c ---[ 385]---> BDD-cost:   26
c ---[ 384]---> BDD-cost:   26
c ---[ 383]---> BDD-cost:   26
c ---[ 382]---> BDD-cost:   26
c ---[ 381]---> BDD-cost:   26
c ---[ 380]---> BDD-cost:   26
c ---[ 379]---> BDD-cost:   26
c ---[ 378]---> BDD-cost:   26
c ---[ 377]---> BDD-cost:   26
c ---[ 376]---> BDD-cost:   26
c ---[ 375]---> BDD-cost:   26
c ---[ 374]---> BDD-cost:   26
c ---[ 373]---> BDD-cost:   26
c ---[ 372]---> BDD-cost:   26
c ---[ 371]---> BDD-cost:   26
c ---[ 370]---> BDD-cost:   26
c ---[ 369]---> BDD-cost:   26
c ---[ 368]---> BDD-cost:   26
c ---[ 367]---> BDD-cost:   26
c ---[ 366]---> BDD-cost:   26
c ---[ 365]---> BDD-cost:   26
c ---[ 364]---> BDD-cost:   26
c ---[ 363]---> BDD-cost:   26
c ---[ 362]---> BDD-cost:   26
c ---[ 361]---> BDD-cost:   26
c ---[ 360]---> BDD-cost:   26
c ---[ 359]---> BDD-cost:   26
c ---[ 358]---> BDD-cost:   26
c ---[ 357]---> BDD-cost:   26
c ---[ 356]---> BDD-cost:   26
c ---[ 355]---> BDD-cost:   26
c ---[ 354]---> BDD-cost:   26
c ---[ 353]---> BDD-cost:   26
c ---[ 352]---> BDD-cost:   26
c ---[ 351]---> BDD-cost:   26
c ---[ 350]---> BDD-cost:   26
c ---[ 349]---> BDD-cost:   26
c ---[ 348]---> BDD-cost:   26
c ---[ 347]---> BDD-cost:   26
c ---[ 346]---> BDD-cost:   26
c ---[ 345]---> BDD-cost:   26
c ---[ 344]---> BDD-cost:   26
c ---[ 343]---> BDD-cost:   26
c ---[ 342]---> BDD-cost:   26
c ---[ 341]---> BDD-cost:   26
c ---[ 340]---> BDD-cost:   26
c ---[ 339]---> BDD-cost:   26
c ---[ 338]---> BDD-cost:   26
c ---[ 337]---> BDD-cost:   26
c ---[ 336]---> BDD-cost:   26
c ---[ 335]---> BDD-cost:   26
c ---[ 334]---> BDD-cost:   26
c ---[ 333]---> BDD-cost:   26
c ---[ 332]---> BDD-cost:   26
c ---[ 331]---> BDD-cost:   26
c ---[ 330]---> BDD-cost:   26
c ---[ 329]---> BDD-cost:   26
c ---[ 328]---> BDD-cost:   26
c ---[ 327]---> BDD-cost:   26
c ---[ 326]---> BDD-cost:   26
c ---[ 325]---> BDD-cost:   26
c ---[ 324]---> BDD-cost:   26
c ---[ 323]---> BDD-cost:   26
c ---[ 322]---> BDD-cost:   26
c ---[ 321]---> BDD-cost:   26
c ---[ 320]---> BDD-cost:   26
c ---[ 319]---> BDD-cost:   26
c ---[ 318]---> BDD-cost:   26
c ---[ 317]---> BDD-cost:   26
c ---[ 316]---> BDD-cost:   26
c ---[ 315]---> BDD-cost:   26
c ---[ 314]---> BDD-cost:   26
c ---[ 313]---> BDD-cost:   26
c ---[ 312]---> BDD-cost:   26
c ---[ 311]---> BDD-cost:   26
c ---[ 310]---> BDD-cost:   26
c ---[ 309]---> BDD-cost:   26
c ---[ 308]---> BDD-cost:   26
c ---[ 307]---> BDD-cost:   26
c ---[ 306]---> BDD-cost:   26
c ---[ 305]---> BDD-cost:   26
c ---[ 304]---> BDD-cost:   26
c ---[ 303]---> BDD-cost:   26
c ---[ 302]---> BDD-cost:   26
c ---[ 301]---> BDD-cost:   26
c ---[ 300]---> BDD-cost:   26
c ---[ 299]---> BDD-cost:   26
c ---[ 298]---> BDD-cost:   26
c ---[ 297]---> BDD-cost:   26
c ---[ 296]---> BDD-cost:   26
c ---[ 295]---> BDD-cost:   26
c ---[ 294]---> BDD-cost:   26
c ---[ 293]---> BDD-cost:   26
c ---[ 292]---> BDD-cost:   26
c ---[ 291]---> BDD-cost:   26
c ---[ 290]---> BDD-cost:   26
c ---[ 289]---> BDD-cost:   26
c ---[ 288]---> BDD-cost:   26
c ---[ 287]---> BDD-cost:   26
c ---[ 286]---> BDD-cost:   26
c ---[ 285]---> BDD-cost:   26
c ---[ 284]---> BDD-cost:   26
c ---[ 283]---> BDD-cost:   26
c ---[ 282]---> BDD-cost:   26
c ---[ 281]---> BDD-cost:   26
c ---[ 280]---> BDD-cost:   26
c ---[ 279]---> BDD-cost:   26
c ---[ 278]---> BDD-cost:   26
c ---[ 277]---> BDD-cost:   26
c ---[ 276]---> BDD-cost:   26
c ---[ 275]---> BDD-cost:   26
c ---[ 274]---> BDD-cost:   26
c ---[ 273]---> BDD-cost:   26
c ---[ 272]---> BDD-cost:   26
c ---[ 271]---> BDD-cost:   26
c ---[ 270]---> BDD-cost:   26
c ---[ 269]---> BDD-cost:   26
c ---[ 268]---> BDD-cost:   26
c ---[ 267]---> BDD-cost:   26
c ---[ 266]---> BDD-cost:   26
c ---[ 265]---> BDD-cost:   26
c ---[ 264]---> BDD-cost:   26
c ---[ 263]---> BDD-cost:   26
c ---[ 262]---> BDD-cost:   26
c ---[ 261]---> BDD-cost:   26
c ---[ 260]---> BDD-cost:   26
c ---[ 259]---> BDD-cost:   26
c ---[ 258]---> BDD-cost:   26
c ---[ 257]---> BDD-cost:   26
c ---[ 256]---> BDD-cost:   26
c ---[ 255]---> BDD-cost:   26
c ---[ 254]---> BDD-cost:   26
c ---[ 253]---> BDD-cost:   26
c ---[ 252]---> BDD-cost:   26
c ---[ 251]---> BDD-cost:   26
c ---[ 250]---> BDD-cost:   26
c ---[ 249]---> BDD-cost:   26
c ---[ 248]---> BDD-cost:   26
c ---[ 247]---> BDD-cost:   26
c ---[ 246]---> BDD-cost:   26
c ---[ 245]---> BDD-cost:   26
c ---[ 244]---> BDD-cost:   26
c ---[ 243]---> BDD-cost:   26
c ---[ 242]---> BDD-cost:   26
c ---[ 241]---> BDD-cost:   26
c ---[ 240]---> BDD-cost:   26
c ---[ 239]---> BDD-cost:   26
c ---[ 238]---> BDD-cost:   26
c ---[ 237]---> BDD-cost:   26
c ---[ 236]---> BDD-cost:   26
c ---[ 235]---> BDD-cost:   26
c ---[ 234]---> BDD-cost:   26
c ---[ 233]---> BDD-cost:   26
c ---[ 232]---> BDD-cost:   26
c ---[ 231]---> BDD-cost:   26
c ---[ 230]---> BDD-cost:   26
c ---[ 229]---> BDD-cost:   26
c ---[ 228]---> BDD-cost:   26
c ---[ 227]---> BDD-cost:   26
c ---[ 226]---> BDD-cost:   26
c ---[ 225]---> BDD-cost:   26
c ---[ 224]---> BDD-cost:   26
c ---[ 223]---> BDD-cost:   26
c ---[ 222]---> BDD-cost:   26
c ---[ 221]---> BDD-cost:   26
c ---[ 220]---> BDD-cost:   26
c ---[ 219]---> BDD-cost:   26
c ---[ 218]---> BDD-cost:   26
c ---[ 217]---> BDD-cost:   26
c ---[ 216]---> BDD-cost:   26
c ---[ 215]---> BDD-cost:   26
c ---[ 214]---> BDD-cost:   26
c ---[ 213]---> BDD-cost:   26
c ---[ 212]---> BDD-cost:   26
c ---[ 211]---> BDD-cost:   26
c ---[ 210]---> BDD-cost:   26
c ---[ 209]---> BDD-cost:   26
c ---[ 208]---> BDD-cost:   26
c ---[ 207]---> BDD-cost:   26
c ---[ 206]---> BDD-cost:   26
c ---[ 205]---> BDD-cost:   26
c ---[ 204]---> BDD-cost:   26
c ---[ 203]---> BDD-cost:   26
c ---[ 202]---> BDD-cost:   26
c ---[ 201]---> BDD-cost:   26
c ---[ 200]---> BDD-cost:   26
c ---[ 199]---> BDD-cost:   26
c ---[ 198]---> BDD-cost:   26
c ---[ 197]---> BDD-cost:   26
c ---[ 196]---> BDD-cost:   26
c ---[ 195]---> BDD-cost:   26
c ---[ 194]---> BDD-cost:   26
c ---[ 193]---> BDD-cost:   26
c ---[ 192]---> BDD-cost:   26
c ---[ 191]---> BDD-cost:   26
c ---[ 190]---> BDD-cost:   26
c ---[ 189]---> BDD-cost:   26
c ---[ 188]---> BDD-cost:   26
c ---[ 187]---> BDD-cost:   26
c ---[ 186]---> BDD-cost:   26
c ---[ 185]---> BDD-cost:   26
c ---[ 184]---> BDD-cost:   26
c ---[ 183]---> BDD-cost:   26
c ---[ 182]---> BDD-cost:   26
c ---[ 181]---> BDD-cost:   26
c ---[ 180]---> BDD-cost:   26
c ---[ 179]---> BDD-cost:   26
c ---[ 178]---> BDD-cost:   26
c ---[ 177]---> BDD-cost:   26
c ---[ 176]---> BDD-cost:   26
c ---[ 175]---> BDD-cost:   26
c ---[ 174]---> BDD-cost:   26
c ---[ 173]---> BDD-cost:   26
c ---[ 172]---> BDD-cost:   26
c ---[ 171]---> BDD-cost:   26
c ---[ 170]---> BDD-cost:   26
c ---[ 169]---> BDD-cost:   26
c ---[ 168]---> BDD-cost:   26
c ---[ 167]---> BDD-cost:   26
c ---[ 166]---> BDD-cost:   26
c ---[ 165]---> BDD-cost:   26
c ---[ 164]---> BDD-cost:   26
c ---[ 163]---> BDD-cost:   26
c ---[ 162]---> BDD-cost:   26
c ---[ 161]---> BDD-cost:   26
c ---[ 160]---> BDD-cost:   26
c ---[ 159]---> BDD-cost:   26
c ---[ 158]---> BDD-cost:   26
c ---[ 157]---> BDD-cost:   26
c ---[ 156]---> BDD-cost:   26
c ---[ 155]---> BDD-cost:   26
c ---[ 154]---> BDD-cost:   26
c ---[ 153]---> BDD-cost:   26
c ---[ 152]---> BDD-cost:   26
c ---[ 151]---> BDD-cost:   26
c ---[ 150]---> BDD-cost:   26
c ---[ 149]---> BDD-cost:   26
c ---[ 148]---> BDD-cost:   26
c ---[ 147]---> BDD-cost:   26
c ---[ 146]---> BDD-cost:   26
c ---[ 145]---> BDD-cost:   26
c ---[ 144]---> BDD-cost:   26
c ---[ 143]---> BDD-cost:   26
c ---[ 142]---> BDD-cost:   26
c ---[ 141]---> BDD-cost:   26
c ---[ 140]---> BDD-cost:   26
c ---[ 139]---> BDD-cost:   26
c ---[ 138]---> BDD-cost:   26
c ---[ 137]---> BDD-cost:   26
c ---[ 136]---> BDD-cost:   26
c ---[ 135]---> BDD-cost:   26
c ---[ 134]---> BDD-cost:   26
c ---[ 133]---> BDD-cost:   26
c ---[ 132]---> BDD-cost:   26
c ---[ 131]---> BDD-cost:   26
c ---[ 130]---> BDD-cost:   26
c ---[ 129]---> BDD-cost:   26
c ---[ 128]---> BDD-cost:   26
c ---[ 127]---> BDD-cost:   26
c ---[ 126]---> BDD-cost:   26
c ---[ 125]---> BDD-cost:   26
c ---[ 124]---> BDD-cost:   26
c ---[ 123]---> BDD-cost:   26
c ---[ 122]---> BDD-cost:   26
c ---[ 121]---> BDD-cost:   26
c ---[ 120]---> BDD-cost:   26
c ---[ 119]---> BDD-cost:   26
c ---[ 118]---> BDD-cost:   26
c ---[ 117]---> BDD-cost:   26
c ---[ 116]---> BDD-cost:   26
c ---[ 115]---> BDD-cost:   26
c ---[ 114]---> BDD-cost:   26
c ---[ 113]---> BDD-cost:   26
c ---[ 112]---> BDD-cost:   26
c ---[ 111]---> BDD-cost:   26
c ---[ 110]---> BDD-cost:   26
c ---[ 109]---> BDD-cost:   26
c ---[ 108]---> BDD-cost:   26
c ---[ 107]---> BDD-cost:   26
c ---[ 106]---> BDD-cost:   26
c ---[ 105]---> BDD-cost:   26
c ---[ 104]---> BDD-cost:   26
c ---[ 103]---> BDD-cost:   26
c ---[ 102]---> BDD-cost:   26
c ---[ 101]---> BDD-cost:   26
c ---[ 100]---> BDD-cost:   26
c ---[  99]---> BDD-cost:   26
c ---[  98]---> BDD-cost:   26
c ---[  97]---> BDD-cost:   26
c ---[  96]---> BDD-cost:   26
c ---[  95]---> BDD-cost:   26
c ---[  94]---> BDD-cost:   26
c ---[  93]---> BDD-cost:   26
c ---[  92]---> BDD-cost:   26
c ---[  91]---> BDD-cost:   26
c ---[  90]---> BDD-cost:   26
c ---[  89]---> BDD-cost:   26
c ---[  88]---> BDD-cost:   26
c ---[  87]---> BDD-cost:   26
c ---[  86]---> BDD-cost:   26
c ---[  85]---> BDD-cost:   26
c ---[  84]---> BDD-cost:   26
c ---[  83]---> BDD-cost:   26
c ---[  82]---> BDD-cost:   26
c ---[  81]---> BDD-cost:   26
c ---[  80]---> BDD-cost:   26
c ---[  79]---> BDD-cost:   26
c ---[  78]---> BDD-cost:   26
c ---[  77]---> BDD-cost:   26
c ---[  76]---> BDD-cost:   26
c ---[  75]---> BDD-cost:   26
c ---[  74]---> BDD-cost:   26
c ---[  73]---> BDD-cost:   26
c ---[  72]---> BDD-cost:   26
c ---[  71]---> BDD-cost:   26
c ---[  70]---> BDD-cost:   26
c ---[  69]---> BDD-cost:   26
c ---[  68]---> BDD-cost:   26
c ---[  67]---> BDD-cost:   26
c ---[  66]---> BDD-cost:   26
c ---[  65]---> BDD-cost:   26
c ---[  64]---> BDD-cost:   26
c ---[  63]---> BDD-cost:   26
c ---[  62]---> BDD-cost:   26
c ---[  61]---> BDD-cost:   26
c ---[  60]---> BDD-cost:   26
c ---[  59]---> BDD-cost:   26
c ---[  58]---> BDD-cost:   26
c ---[  57]---> BDD-cost:   26
c ---[  56]---> BDD-cost:   26
c ---[  55]---> BDD-cost:   26
c ---[  54]---> BDD-cost:   26
c ---[  53]---> BDD-cost:   26
c ---[  52]---> BDD-cost:   26
c ---[  51]---> BDD-cost:   26
c ---[  50]---> BDD-cost:   26
c ---[  49]---> BDD-cost:   26
c ---[  48]---> BDD-cost:   26
c ---[  47]---> BDD-cost:   26
c ---[  46]---> BDD-cost:   26
c ---[  45]---> BDD-cost:   26
c ---[  44]---> BDD-cost:   26
c ---[  43]---> BDD-cost:   26
c ---[  42]---> BDD-cost:   26
c ---[  41]---> BDD-cost:   26
c ---[  40]---> BDD-cost:   26
c ---[  39]---> BDD-cost:   26
c ---[  38]---> BDD-cost:   26
c ---[  37]---> BDD-cost:   26
c ---[  36]---> BDD-cost:   26
c ---[  35]---> BDD-cost:   26
c ---[  34]---> BDD-cost:   26
c ---[  33]---> BDD-cost:   26
c ---[  32]---> BDD-cost:   26
c ---[  31]---> BDD-cost:   26
c ---[  30]---> BDD-cost:   26
c ---[  29]---> BDD-cost:   26
c ---[  28]---> BDD-cost:   26
c ---[  27]---> BDD-cost:   26
c ---[  26]---> BDD-cost:   26
c ---[  25]---> BDD-cost:   26
c ---[  24]---> BDD-cost:   26
c ---[  23]---> BDD-cost:   26
c ---[  22]---> BDD-cost:   26
c ---[  21]---> BDD-cost:   26
c ---[  20]---> BDD-cost:   26
c ---[  19]---> BDD-cost:   26
c ---[  18]---> BDD-cost:   26
c ---[  17]---> BDD-cost:   26
c ---[  16]---> BDD-cost:   26
c ---[  15]---> BDD-cost:   26
c ---[  14]---> BDD-cost:   26
c ---[  13]---> BDD-cost:   26
c ---[  12]---> BDD-cost:   26
c ---[  11]---> BDD-cost:   26
c ---[  10]---> BDD-cost:   26
c ---[   9]---> BDD-cost:   26
c ---[   8]---> BDD-cost:   26
c ---[   7]---> BDD-cost:   26
c ---[   6]---> BDD-cost:   26
c ---[   5]---> BDD-cost:   26
c ---[   4]---> BDD-cost:   26
c ---[   3]---> BDD-cost:   26
c ---[   2]---> BDD-cost:   26
c ---[   1]---> BDD-cost:   26
c ---[   0]---> BDD-cost:   26
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |  621352  1664855 |  207117       0        0     nan |  0.000 % |
c |       101 |  621346  1664843 |  227828      98      828     8.4 |  1.098 % |
c |       251 |  621346  1664843 |  250611     248     2369     9.6 |  1.098 % |
c |       476 |  621308  1664767 |  275672     454     3431     7.6 |  1.105 % |
c |       813 |  621230  1664611 |  303239     752     8173    10.9 |  1.118 % |
c |      1319 |  621220  1664591 |  333563    1253    12914    10.3 |  1.120 % |
c |      2078 |  620924  1663995 |  366920    1862    17350     9.3 |  1.170 % |
c |      3217 |  620796  1663725 |  403612    2927    29867    10.2 |  1.192 % |
c |      4926 |  620666  1663433 |  443973    4560    46431    10.2 |  1.214 % |
c |      7489 |  620158  1662391 |  488371    6845    72575    10.6 |  1.300 % |
c ==============================================================================
c [1mFound solution: 203776[0m
c ---[   0]---> BDD-cost:  207
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      8054 |  620500  1663485 |  206833    7373    76734    10.4 |  1.300 % |
c |      8154 |  620498  1663481 |  227516    7472    77492    10.4 |  1.312 % |
c |      8304 |  620476  1663437 |  250267    7611    78481    10.3 |  1.316 % |
c |      8529 |  620398  1663267 |  275294    7789    80196    10.3 |  1.329 % |
c |      8866 |  620310  1663069 |  302824    8007    83711    10.5 |  1.345 % |
c |      9372 |  620198  1662841 |  333106    8458    87791    10.4 |  1.364 % |
c ==============================================================================
c [1mFound solution: 202752[0m
c ---[   0]---> BDD-cost:  103
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      9841 |  620366  1663483 |  206788    8857    92002    10.4 |  1.364 % |
c |      9941 |  620362  1663473 |  227466    8954    92583    10.3 |  1.388 % |
c |     10091 |  620342  1663424 |  250213    9078    94194    10.4 |  1.391 % |
c |     10316 |  620320  1663372 |  275234    9290    96147    10.3 |  1.395 % |
c |     10653 |  620300  1663332 |  302758    9617    99315    10.3 |  1.398 % |
c |     11159 |  620138  1663001 |  333034   10039   105280    10.5 |  1.426 % |
c |     11918 |  619938  1662585 |  366337   10687   113029    10.6 |  1.460 % |
c |     13058 |  619872  1662444 |  402971   11791   132049    11.2 |  1.471 % |
c ==============================================================================
c [1mFound solution: 197632[0m
c ---[   0]---> Sorter-cost: 2346     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     14217 |  622037  1667565 |  207345   12911   144853    11.2 |  1.471 % |
c |     14318 |  622037  1667565 |  228079   13012   145675    11.2 |  1.470 % |
c |     14468 |  622029  1667545 |  250887   13157   147560    11.2 |  1.471 % |
c |     14693 |  622029  1667545 |  275976   13382   149845    11.2 |  1.471 % |
c ==============================================================================
c [1mFound solution: 196608[0m
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     14808 |  622026  1667538 |  207342   13497   150735    11.2 |  1.471 % |
c |     14908 |  621984  1667454 |  228076   13576   151402    11.2 |  1.481 % |
c |     15058 |  621984  1667454 |  250883   13726   152322    11.1 |  1.481 % |
c |     15284 |  621922  1667324 |  275972   13899   154822    11.1 |  1.491 % |
c |     15622 |  621922  1667324 |  303569   14237   161431    11.3 |  1.491 % |
c |     16128 |  621922  1667324 |  333926   14743   167758    11.4 |  1.491 % |
c |     16887 |  621900  1667276 |  367319   15486   177030    11.4 |  1.495 % |
c |     18026 |  621844  1667136 |  404050   16565   189581    11.4 |  1.504 % |
c |     19734 |  621676  1666776 |  444455   18141   207200    11.4 |  1.533 % |
c |     22297 |  621452  1666320 |  488901   20566   240319    11.7 |  1.571 % |
c |     26141 |  621202  1665788 |  537791   24205   299462    12.4 |  1.613 % |
c ==============================================================================
c [1mFound solution: 179200[0m
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     27177 |  621425  1666381 |  207141   25158   308374    12.3 |  1.613 % |
c |     27277 |  621423  1666376 |  227855   25257   310842    12.3 |  1.624 % |
c |     27427 |  621423  1666376 |  250640   25407   312776    12.3 |  1.624 % |
c |     27652 |  621423  1666376 |  275704   25632   314571    12.3 |  1.624 % |
c |     27990 |  621405  1666337 |  303275   25961   318864    12.3 |  1.628 % |
c |     28497 |  621403  1666333 |  333602   26467   329817    12.5 |  1.628 % |
c |     29256 |  621373  1666272 |  366962   27211   342313    12.6 |  1.633 % |
c |     30395 |  621337  1666188 |  403659   28292   356805    12.6 |  1.639 % |
c |     32103 |  621269  1666051 |  444025   29966   379121    12.7 |  1.651 % |
c |     34665 |  621165  1665826 |  488427   32327   408380    12.6 |  1.668 % |
c |     38509 |  621107  1665701 |  537270   36131   501718    13.9 |  1.678 % |
c ==============================================================================
c [1mFound solution: 176128[0m
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     42482 |  621004  1665515 |  207001   40013   558436    14.0 |  1.678 % |
c |     42582 |  621004  1665515 |  227701   40113   560448    14.0 |  1.703 % |
c |     42732 |  621004  1665515 |  250471   40263   568524    14.1 |  1.703 % |
c |     42960 |  621004  1665515 |  275518   40491   572186    14.1 |  1.703 % |
c |     43297 |  621004  1665515 |  303070   40828   581031    14.2 |  1.703 % |
c |     43803 |  620956  1665412 |  333377   41258   593141    14.4 |  1.712 % |
c |     44562 |  620930  1665353 |  366714   41987   606944    14.5 |  1.716 % |
c |     45701 |  620928  1665348 |  403386   43125   638954    14.8 |  1.716 % |
c |     47409 |  620916  1665323 |  443725   44736   664582    14.9 |  1.718 % |
c |     49972 |  620742  1664964 |  488097   47181   699493    14.8 |  1.748 % |
c |     53816 |  620670  1664809 |  536907   50954   756310    14.8 |  1.760 % |
c ==============================================================================
c [1mFound solution: 171008[0m
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     58286 |  620523  1664556 |  206841   55069   818052    14.9 |  1.760 % |
c |     58386 |  620523  1664556 |  227525   55169   819229    14.8 |  1.797 % |
c |     58536 |  620523  1664556 |  250277   55319   820547    14.8 |  1.797 % |
c |     58762 |  620523  1664556 |  275305   55545   824680    14.8 |  1.797 % |
c |     59101 |  620519  1664547 |  302835   55881   828710    14.8 |  1.798 % |
c |     59607 |  620519  1664547 |  333119   56387   837713    14.9 |  1.798 % |
c |     60370 |  620491  1664488 |  366431   57127   850096    14.9 |  1.802 % |
c |     61510 |  620447  1664387 |  403074   58208   861028    14.8 |  1.810 % |
c |     63218 |  620437  1664366 |  443382   59892   886163    14.8 |  1.811 % |
c |     65781 |  620431  1664352 |  487720   62451   950876    15.2 |  1.812 % |
c |     69625 |  620359  1664194 |  536492   66231  1006910    15.2 |  1.825 % |
c |     75391 |  620317  1664097 |  590141   71967  1106946    15.4 |  1.832 % |
c |     84040 |  620287  1664035 |  649155   80557  1285498    16.0 |  1.837 % |
/oldhome/oroussel/solvers/minisat+_script: line 9: 11222 CPU time limit exceeded $XDIR/minisat+_64-bit_static -try "$@"
#### END SOLVER DATA ####
#### BEGIN WATCHER DATA ####
Enforcing CPU limit (will send SIGTERM then SIGKILL): 1200 seconds
Enforcing CPUTime (will send SIGXCPU) limit: 1230 seconds
Enforcing VSIZE limit: 943718400 bytes
Raw data (loadavg): 0.92 0.97 0.91 2/54 11218
Raw data (stat): 11218 (runsolver) R 11217 25830 25829 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 783830229 1052672 99 4294967295 134512640 135381576 3221224480 3221219688 135158418 0 2147483391 7 90112 0 0 0 17 0 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0002 s]
Raw data (loadavg): 0.93 0.97 0.91 2/55 11222
Raw data (stat): 11218 (minisat+_script) S 11217 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783830229 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+20.0009 s]
Raw data (loadavg): 0.94 0.97 0.91 2/55 11222
Raw data (stat): 11218 (minisat+_script) S 11217 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783830229 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+30.013 s]
Raw data (loadavg): 0.95 0.97 0.91 2/55 11222
Raw data (stat): 11218 (minisat+_script) S 11217 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783830229 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+40.0136 s]
Raw data (loadavg): 0.96 0.97 0.91 2/55 11222
Raw data (stat): 11218 (minisat+_script) S 11217 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783830229 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+50.0143 s]
Raw data (loadavg): 0.96 0.97 0.91 2/55 11222
Raw data (stat): 11218 (minisat+_script) S 11217 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783830229 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+60.0145 s]
Raw data (loadavg): 0.97 0.97 0.91 2/55 11222
Raw data (stat): 11218 (minisat+_script) S 11217 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783830229 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+70.0149 s]
Raw data (loadavg): 0.97 0.97 0.91 2/55 11222
Raw data (stat): 11218 (minisat+_script) S 11217 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783830229 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+80.016 s]
Raw data (loadavg): 0.98 0.97 0.91 2/55 11222
Raw data (stat): 11218 (minisat+_script) S 11217 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783830229 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+90.0168 s]
Raw data (loadavg): 0.98 0.97 0.91 2/55 11222
Raw data (stat): 11218 (minisat+_script) S 11217 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783830229 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+100.016 s]
Raw data (loadavg): 0.98 0.97 0.91 2/55 11222
Raw data (stat): 11218 (minisat+_script) S 11217 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783830229 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+110.016 s]
Raw data (loadavg): 0.98 0.97 0.91 2/55 11222
Raw data (stat): 11218 (minisat+_script) S 11217 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783830229 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+120.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11222
Raw data (stat): 11218 (minisat+_script) S 11217 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783830229 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+130.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11222
Raw data (stat): 11218 (minisat+_script) S 11217 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783830229 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+140.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11222
Raw data (stat): 11218 (minisat+_script) S 11217 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783830229 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+150.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11222
Raw data (stat): 11218 (minisat+_script) S 11217 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783830229 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+160.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11222
Raw data (stat): 11218 (minisat+_script) S 11217 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783830229 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+170.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11222
Raw data (stat): 11218 (minisat+_script) S 11217 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783830229 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+180.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11222
Raw data (stat): 11218 (minisat+_script) S 11217 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783830229 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+190.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11222
Raw data (stat): 11218 (minisat+_script) S 11217 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783830229 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+200.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11222
Raw data (stat): 11218 (minisat+_script) S 11217 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783830229 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+210.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11222
Raw data (stat): 11218 (minisat+_script) S 11217 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783830229 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+220.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11222
Raw data (stat): 11218 (minisat+_script) S 11217 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783830229 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+230.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11222
Raw data (stat): 11218 (minisat+_script) S 11217 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783830229 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+240.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11222
Raw data (stat): 11218 (minisat+_script) S 11217 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783830229 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+250.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11222
Raw data (stat): 11218 (minisat+_script) S 11217 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783830229 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+260.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11222
Raw data (stat): 11218 (minisat+_script) S 11217 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783830229 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+270.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11222
Raw data (stat): 11218 (minisat+_script) S 11217 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783830229 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+280.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11222
Raw data (stat): 11218 (minisat+_script) S 11217 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783830229 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+290.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11222
Raw data (stat): 11218 (minisat+_script) S 11217 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783830229 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+300.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11222
Raw data (stat): 11218 (minisat+_script) S 11217 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783830229 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+310.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11222
Raw data (stat): 11218 (minisat+_script) S 11217 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783830229 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+320.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11222
Raw data (stat): 11218 (minisat+_script) S 11217 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783830229 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+330.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11222
Raw data (stat): 11218 (minisat+_script) S 11217 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783830229 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+340.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11222
Raw data (stat): 11218 (minisat+_script) S 11217 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783830229 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+350.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11222
Raw data (stat): 11218 (minisat+_script) S 11217 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783830229 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+360.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11222
Raw data (stat): 11218 (minisat+_script) S 11217 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783830229 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+370.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11222
Raw data (stat): 11218 (minisat+_script) S 11217 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783830229 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+380.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11222
Raw data (stat): 11218 (minisat+_script) S 11217 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783830229 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+390.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11222
Raw data (stat): 11218 (minisat+_script) S 11217 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783830229 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+400.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11222
Raw data (stat): 11218 (minisat+_script) S 11217 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783830229 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+410.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11222
Raw data (stat): 11218 (minisat+_script) S 11217 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783830229 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+420.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11222
Raw data (stat): 11218 (minisat+_script) S 11217 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783830229 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+430.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11222
Raw data (stat): 11218 (minisat+_script) S 11217 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783830229 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+440.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11222
Raw data (stat): 11218 (minisat+_script) S 11217 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783830229 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+450.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11222
Raw data (stat): 11218 (minisat+_script) S 11217 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783830229 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+460.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11222
Raw data (stat): 11218 (minisat+_script) S 11217 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783830229 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+470.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11222
Raw data (stat): 11218 (minisat+_script) S 11217 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783830229 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+480.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11222
Raw data (stat): 11218 (minisat+_script) S 11217 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783830229 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+490.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11222
Raw data (stat): 11218 (minisat+_script) S 11217 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783830229 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+500.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11222
Raw data (stat): 11218 (minisat+_script) S 11217 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783830229 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+510.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11222
Raw data (stat): 11218 (minisat+_script) S 11217 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783830229 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+520.031 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11222
Raw data (stat): 11218 (minisat+_script) S 11217 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783830229 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+530.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11222
Raw data (stat): 11218 (minisat+_script) S 11217 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783830229 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+540.032 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11222
Raw data (stat): 11218 (minisat+_script) S 11217 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783830229 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+550.032 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11222
Raw data (stat): 11218 (minisat+_script) S 11217 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783830229 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+560.031 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11222
Raw data (stat): 11218 (minisat+_script) S 11217 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783830229 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+570.033 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11222
Raw data (stat): 11218 (minisat+_script) S 11217 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783830229 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+580.032 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11222
Raw data (stat): 11218 (minisat+_script) S 11217 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783830229 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+590.033 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11222
Raw data (stat): 11218 (minisat+_script) S 11217 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783830229 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+600.033 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11222
Raw data (stat): 11218 (minisat+_script) S 11217 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783830229 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+610.033 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11222
Raw data (stat): 11218 (minisat+_script) S 11217 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783830229 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+620.033 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11222
Raw data (stat): 11218 (minisat+_script) S 11217 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783830229 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+630.033 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11222
Raw data (stat): 11218 (minisat+_script) S 11217 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783830229 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+640.034 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11222
Raw data (stat): 11218 (minisat+_script) S 11217 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783830229 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+650.033 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11222
Raw data (stat): 11218 (minisat+_script) S 11217 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783830229 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+660.034 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11222
Raw data (stat): 11218 (minisat+_script) S 11217 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783830229 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+670.034 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11222
Raw data (stat): 11218 (minisat+_script) S 11217 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783830229 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+680.035 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11222
Raw data (stat): 11218 (minisat+_script) S 11217 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783830229 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+690.036 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11222
Raw data (stat): 11218 (minisat+_script) S 11217 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783830229 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+700.035 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11222
Raw data (stat): 11218 (minisat+_script) S 11217 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783830229 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+710.035 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11222
Raw data (stat): 11218 (minisat+_script) S 11217 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783830229 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+720.036 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11222
Raw data (stat): 11218 (minisat+_script) S 11217 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783830229 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+730.036 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11222
Raw data (stat): 11218 (minisat+_script) S 11217 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783830229 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+740.037 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11222
Raw data (stat): 11218 (minisat+_script) S 11217 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783830229 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+750.038 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11222
Raw data (stat): 11218 (minisat+_script) S 11217 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783830229 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+760.037 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11222
Raw data (stat): 11218 (minisat+_script) S 11217 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783830229 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+770.037 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11222
Raw data (stat): 11218 (minisat+_script) S 11217 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783830229 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+780.037 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11222
Raw data (stat): 11218 (minisat+_script) S 11217 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783830229 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+790.038 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11222
Raw data (stat): 11218 (minisat+_script) S 11217 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783830229 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+800.037 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11222
Raw data (stat): 11218 (minisat+_script) S 11217 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783830229 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+810.037 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11222
Raw data (stat): 11218 (minisat+_script) S 11217 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783830229 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+820.038 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11222
Raw data (stat): 11218 (minisat+_script) S 11217 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783830229 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+830.038 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11222
Raw data (stat): 11218 (minisat+_script) S 11217 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783830229 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+840.039 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11222
Raw data (stat): 11218 (minisat+_script) S 11217 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783830229 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+850.039 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11222
Raw data (stat): 11218 (minisat+_script) S 11217 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783830229 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+860.039 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11222
Raw data (stat): 11218 (minisat+_script) S 11217 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783830229 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+870.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11222
Raw data (stat): 11218 (minisat+_script) S 11217 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783830229 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+880.041 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11222
Raw data (stat): 11218 (minisat+_script) S 11217 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783830229 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+890.041 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11222
Raw data (stat): 11218 (minisat+_script) S 11217 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783830229 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+900.043 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11222
Raw data (stat): 11218 (minisat+_script) S 11217 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783830229 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+910.042 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11222
Raw data (stat): 11218 (minisat+_script) S 11217 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783830229 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+920.042 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11222
Raw data (stat): 11218 (minisat+_script) S 11217 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783830229 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+930.042 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11222
Raw data (stat): 11218 (minisat+_script) S 11217 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783830229 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+940.042 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11222
Raw data (stat): 11218 (minisat+_script) S 11217 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783830229 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+950.042 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11222
Raw data (stat): 11218 (minisat+_script) S 11217 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783830229 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+960.043 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11222
Raw data (stat): 11218 (minisat+_script) S 11217 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783830229 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+970.043 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11222
Raw data (stat): 11218 (minisat+_script) S 11217 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783830229 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+980.042 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11222
Raw data (stat): 11218 (minisat+_script) S 11217 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783830229 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+990.043 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11222
Raw data (stat): 11218 (minisat+_script) S 11217 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783830229 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1000.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11222
Raw data (stat): 11218 (minisat+_script) S 11217 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783830229 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1010.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11222
Raw data (stat): 11218 (minisat+_script) S 11217 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783830229 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1020.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11222
Raw data (stat): 11218 (minisat+_script) S 11217 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783830229 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1030.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11222
Raw data (stat): 11218 (minisat+_script) S 11217 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783830229 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1040.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11222
Raw data (stat): 11218 (minisat+_script) S 11217 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783830229 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1050.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11222
Raw data (stat): 11218 (minisat+_script) S 11217 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783830229 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1060.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11222
Raw data (stat): 11218 (minisat+_script) S 11217 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783830229 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1070.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11222
Raw data (stat): 11218 (minisat+_script) S 11217 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783830229 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1080.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11222
Raw data (stat): 11218 (minisat+_script) S 11217 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783830229 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1090.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11222
Raw data (stat): 11218 (minisat+_script) S 11217 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783830229 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1100.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11222
Raw data (stat): 11218 (minisat+_script) S 11217 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783830229 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1110.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11222
Raw data (stat): 11218 (minisat+_script) S 11217 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783830229 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1120.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11222
Raw data (stat): 11218 (minisat+_script) S 11217 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783830229 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1130.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11222
Raw data (stat): 11218 (minisat+_script) S 11217 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783830229 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1140.07 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11222
Raw data (stat): 11218 (minisat+_script) S 11217 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783830229 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1150.07 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11222
Raw data (stat): 11218 (minisat+_script) S 11217 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783830229 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1160.07 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11222
Raw data (stat): 11218 (minisat+_script) S 11217 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783830229 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1170.07 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11222
Raw data (stat): 11218 (minisat+_script) S 11217 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783830229 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1180.07 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11222
Raw data (stat): 11218 (minisat+_script) S 11217 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783830229 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1190.07 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11222
Raw data (stat): 11218 (minisat+_script) S 11217 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783830229 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1200.07 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11222
Raw data (stat): 11218 (minisat+_script) S 11217 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783830229 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1210.07 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11222
Raw data (stat): 11218 (minisat+_script) S 11217 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783830229 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1220.07 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11222
Raw data (stat): 11218 (minisat+_script) S 11217 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783830229 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1229.76 s]
Raw data (loadavg): 0.99 0.97 0.91 1/53 11222
Raw data (stat): 11218 (minisat+_script) S 11217 25830 25829 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783830229 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 0

Child status: 152
Real time (s): 1229.76
CPU time (s): 1229.88
CPU user time (s): 1229.07
CPU system time (s): 0.814876
CPU usage (%): 100.01
Max. virtual memory (Kb): 2124
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####