PB'05 competition: run trace

Some explanations

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

Name	normalized-opb/mps-v2-13-7/plato.asu.edu/pub/unibo/normalized-mps-v2-13-7-usAbbrv.8.25_70.opb
MD5SUM	0b6e5fd99af8bfe5c5be00124c8da261
Bench Category	optimization, medium integers (OPTMEDINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	20736
Optimality of the best value was proved	NO
Number of terms in the objective function	125
Biggest coefficient in the objective function	524288
Number of bits for the biggest coefficient in the objective function	20
Sum of the numbers in the objective function	1062015
Number of bits of the sum of numbers in the objective function	21
Biggest number in a constraint	128000000
Number of bits of the biggest number in a constraint	27
Biggest sum of numbers in a constraint	268444670
Number of bits of the biggest sum of numbers	29
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	1201.16
Number of variables	18711
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	55
Trace number 31348

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

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.077
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:        797908 kB
Buffers:         31844 kB
Cached:         183444 kB
SwapCached:        748 kB
Active:          30216 kB
Inactive:       187308 kB
HighTotal:      131008 kB
HighFree:          252 kB
LowTotal:       903652 kB
LowFree:        797656 kB
SwapTotal:     2097640 kB
SwapFree:      2096192 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           5444 kB
Slab:            13616 kB
Committed_AS:    63604 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-05-26 00:45:53 (client local time) WITH STATUS 152 IN 1229.88 SECONDS
stats: 22748 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:  110
c ---[3915]---> BDD-cost:   79
c ---[3914]---> BDD-cost:   79
c ---[3913]---> BDD-cost:   79
c ---[3912]---> BDD-cost:   79
c ---[3911]---> BDD-cost:  108
c ---[3910]---> BDD-cost:  110
c ---[3909]---> BDD-cost:   79
c ---[3908]---> BDD-cost:   79
c ---[3907]---> BDD-cost:   79
c ---[3905]---> BDD-cost:   79
c ---[3904]---> BDD-cost:  116
c ---[3903]---> BDD-cost:  110
c ---[3902]---> BDD-cost:   79
c ---[3901]---> BDD-cost:   79
c ---[3900]---> BDD-cost:   79
c ---[3899]---> BDD-cost:   79
c ---[3898]---> BDD-cost:  114
c ---[3897]---> BDD-cost:  110
c ---[3896]---> BDD-cost:   79
c ---[3894]---> BDD-cost:   79
c ---[3893]---> BDD-cost:   79
c ---[3892]---> BDD-cost:   79
c ---[3891]---> BDD-cost:  108
c ---[3890]---> BDD-cost:  110
c ---[3889]---> BDD-cost:   79
c ---[3888]---> BDD-cost:   79
c ---[3887]---> BDD-cost:   79
c ---[3886]---> BDD-cost:   79
c ---[3885]---> BDD-cost:  116
c ---[3883]---> BDD-cost:  110
c ---[3882]---> BDD-cost:   79
c ---[3881]---> BDD-cost:   79
c ---[3880]---> BDD-cost:   79
c ---[3879]---> BDD-cost:   79
c ---[3878]---> BDD-cost:  116
c ---[3877]---> BDD-cost:  110
c ---[3876]---> BDD-cost:   79
c ---[3875]---> BDD-cost:   79
c ---[3874]---> BDD-cost:   79
c ---[3872]---> BDD-cost:   79
c ---[3871]---> BDD-cost:  108
c ---[3870]---> BDD-cost:  110
c ---[3869]---> BDD-cost:   79
c ---[3868]---> BDD-cost:   79
c ---[3867]---> BDD-cost:   79
c ---[3866]---> BDD-cost:   79
c ---[3865]---> BDD-cost:  112
c ---[3864]---> BDD-cost:  110
c ---[3863]---> BDD-cost:   79
c ---[3861]---> BDD-cost:   79
c ---[3860]---> BDD-cost:   79
c ---[3859]---> BDD-cost:   79
c ---[3858]---> BDD-cost:  108
c ---[3857]---> BDD-cost:  110
c ---[3856]---> BDD-cost:   79
c ---[3855]---> BDD-cost:   79
c ---[3854]---> BDD-cost:   79
c ---[3853]---> BDD-cost:   79
c ---[3852]---> BDD-cost:  116
c ---[3850]---> BDD-cost:  110
c ---[3849]---> BDD-cost:   79
c ---[3848]---> BDD-cost:   79
c ---[3847]---> BDD-cost:   79
c ---[3846]---> BDD-cost:   79
c ---[3845]---> BDD-cost:  108
c ---[3844]---> BDD-cost:  110
c ---[3843]---> BDD-cost:   79
c ---[3842]---> BDD-cost:   79
c ---[3841]---> BDD-cost:   79
c ---[3839]---> BDD-cost:   79
c ---[3838]---> BDD-cost:  116
c ---[3837]---> BDD-cost:  110
c ---[3836]---> BDD-cost:   79
c ---[3835]---> BDD-cost:   79
c ---[3834]---> BDD-cost:   79
c ---[3833]---> BDD-cost:   79
c ---[3832]---> BDD-cost:  116
c ---[3831]---> BDD-cost:  110
c ---[3830]---> BDD-cost:   79
c ---[3828]---> BDD-cost:   79
c ---[3827]---> BDD-cost:   79
c ---[3826]---> BDD-cost:   79
c ---[3825]---> BDD-cost:  116
c ---[3824]---> BDD-cost:  110
c ---[3823]---> BDD-cost:   79
c ---[3822]---> BDD-cost:   79
c ---[3821]---> BDD-cost:   79
c ---[3820]---> BDD-cost:   79
c ---[3819]---> BDD-cost:  108
c ---[3817]---> BDD-cost:  110
c ---[3816]---> BDD-cost:   79
c ---[3815]---> BDD-cost:   79
c ---[3814]---> BDD-cost:   79
c ---[3813]---> BDD-cost:   79
c ---[3812]---> BDD-cost:  116
c ---[3811]---> BDD-cost:  110
c ---[3810]---> BDD-cost:   79
c ---[3809]---> BDD-cost:   79
c ---[3808]---> BDD-cost:   79
c ---[3805]---> BDD-cost:   79
c ---[3804]---> BDD-cost:  116
c ---[3803]---> BDD-cost:  110
c ---[3802]---> BDD-cost:   79
c ---[3801]---> BDD-cost:   79
c ---[3800]---> BDD-cost:   79
c ---[3799]---> BDD-cost:   79
c ---[3798]---> BDD-cost:  116
c ---[3797]---> BDD-cost:  110
c ---[3796]---> BDD-cost:   79
c ---[3794]---> BDD-cost:   79
c ---[3793]---> BDD-cost:   79
c ---[3792]---> BDD-cost:   79
c ---[3791]---> BDD-cost:  108
c ---[3790]---> BDD-cost:  110
c ---[3789]---> BDD-cost:   79
c ---[3788]---> BDD-cost:   79
c ---[3787]---> BDD-cost:   79
c ---[3786]---> BDD-cost:   79
c ---[3785]---> BDD-cost:  108
c ---[3783]---> BDD-cost:  110
c ---[3782]---> BDD-cost:   79
c ---[3781]---> BDD-cost:   79
c ---[3780]---> BDD-cost:   79
c ---[3779]---> BDD-cost:   79
c ---[3778]---> BDD-cost:  108
c ---[3777]---> BDD-cost:  110
c ---[3776]---> BDD-cost:   79
c ---[3775]---> BDD-cost:   79
c ---[3774]---> BDD-cost:   79
c ---[3772]---> BDD-cost:   79
c ---[3771]---> BDD-cost:  114
c ---[3770]---> BDD-cost:  110
c ---[3769]---> BDD-cost:   79
c ---[3768]---> BDD-cost:   79
c ---[3767]---> BDD-cost:   79
c ---[3766]---> BDD-cost:   79
c ---[3765]---> BDD-cost:  116
c ---[3764]---> BDD-cost:  110
c ---[3763]---> BDD-cost:   79
c ---[3761]---> BDD-cost:   79
c ---[3760]---> BDD-cost:   79
c ---[3759]---> BDD-cost:   79
c ---[3758]---> BDD-cost:  116
c ---[3757]---> BDD-cost:  110
c ---[3756]---> BDD-cost:   79
c ---[3755]---> BDD-cost:   79
c ---[3754]---> BDD-cost:   79
c ---[3753]---> BDD-cost:   79
c ---[3752]---> BDD-cost:  108
c ---[3750]---> BDD-cost:  110
c ---[3749]---> BDD-cost:   79
c ---[3748]---> BDD-cost:   79
c ---[3747]---> BDD-cost:   79
c ---[3746]---> BDD-cost:   79
c ---[3745]---> BDD-cost:  108
c ---[3744]---> BDD-cost:  110
c ---[3743]---> BDD-cost:   79
c ---[3742]---> BDD-cost:   79
c ---[3741]---> BDD-cost:   79
c ---[3739]---> BDD-cost:   79
c ---[3738]---> BDD-cost:  116
c ---[3737]---> BDD-cost:  110
c ---[3736]---> BDD-cost:   79
c ---[3735]---> BDD-cost:   79
c ---[3734]---> BDD-cost:   79
c ---[3733]---> BDD-cost:   79
c ---[3732]---> BDD-cost:  108
c ---[3731]---> BDD-cost:  110
c ---[3730]---> BDD-cost:   79
c ---[3728]---> BDD-cost:   79
c ---[3727]---> BDD-cost:   79
c ---[3726]---> BDD-cost:   79
c ---[3725]---> BDD-cost:  116
c ---[3724]---> BDD-cost:  110
c ---[3723]---> BDD-cost:   79
c ---[3722]---> BDD-cost:   79
c ---[3721]---> BDD-cost:   79
c ---[3720]---> BDD-cost:   79
c ---[3719]---> BDD-cost:  108
c ---[3717]---> BDD-cost:  110
c ---[3716]---> BDD-cost:   79
c ---[3715]---> BDD-cost:   79
c ---[3714]---> BDD-cost:   79
c ---[3713]---> BDD-cost:   79
c ---[3712]---> BDD-cost:  108
c ---[3711]---> BDD-cost:  110
c ---[3710]---> BDD-cost:   79
c ---[3709]---> BDD-cost:   79
c ---[3708]---> BDD-cost:   79
c ---[3706]---> BDD-cost:   79
c ---[3705]---> BDD-cost:  116
c ---[3704]---> BDD-cost:  110
c ---[3703]---> BDD-cost:   79
c ---[3702]---> BDD-cost:   79
c ---[3701]---> BDD-cost:   79
c ---[3700]---> BDD-cost:   79
c ---[3699]---> BDD-cost:  114
c ---[3698]---> BDD-cost:  110
c ---[3697]---> BDD-cost:   79
c ---[3694]---> BDD-cost:   79
c ---[3693]---> BDD-cost:   79
c ---[3692]---> BDD-cost:   79
c ---[3691]---> BDD-cost:  114
c ---[3690]---> BDD-cost:  110
c ---[3689]---> BDD-cost:   79
c ---[3688]---> BDD-cost:   79
c ---[3687]---> BDD-cost:   79
c ---[3686]---> BDD-cost:   79
c ---[3685]---> BDD-cost:  108
c ---[3683]---> BDD-cost:  110
c ---[3682]---> BDD-cost:   79
c ---[3681]---> BDD-cost:   79
c ---[3680]---> BDD-cost:   79
c ---[3679]---> BDD-cost:   79
c ---[3678]---> BDD-cost:  114
c ---[3677]---> BDD-cost:  110
c ---[3676]---> BDD-cost:   79
c ---[3675]---> BDD-cost:   79
c ---[3674]---> BDD-cost:   79
c ---[3672]---> BDD-cost:   79
c ---[3671]---> BDD-cost:  116
c ---[3670]---> BDD-cost:  110
c ---[3669]---> BDD-cost:   79
c ---[3668]---> BDD-cost:   79
c ---[3667]---> BDD-cost:   79
c ---[3666]---> BDD-cost:   79
c ---[3665]---> BDD-cost:  108
c ---[3664]---> BDD-cost:  110
c ---[3663]---> BDD-cost:   79
c ---[3661]---> BDD-cost:   79
c ---[3660]---> BDD-cost:   79
c ---[3659]---> BDD-cost:   79
c ---[3658]---> BDD-cost:  116
c ---[3657]---> BDD-cost:  110
c ---[3656]---> BDD-cost:   79
c ---[3655]---> BDD-cost:   79
c ---[3654]---> BDD-cost:   79
c ---[3653]---> BDD-cost:   79
c ---[3652]---> BDD-cost:  116
c ---[3650]---> BDD-cost:  110
c ---[3649]---> BDD-cost:   79
c ---[3648]---> BDD-cost:   79
c ---[3647]---> BDD-cost:   79
c ---[3646]---> BDD-cost:   79
c ---[3645]---> BDD-cost:  108
c ---[3644]---> BDD-cost:  110
c ---[3643]---> BDD-cost:   79
c ---[3642]---> BDD-cost:   79
c ---[3641]---> BDD-cost:   79
c ---[3639]---> BDD-cost:   79
c ---[3638]---> BDD-cost:  116
c ---[3637]---> BDD-cost:  110
c ---[3636]---> BDD-cost:   79
c ---[3635]---> BDD-cost:   79
c ---[3634]---> BDD-cost:   79
c ---[3633]---> BDD-cost:   79
c ---[3632]---> BDD-cost:  116
c ---[3631]---> BDD-cost:  110
c ---[3630]---> BDD-cost:   79
c ---[3628]---> BDD-cost:   79
c ---[3627]---> BDD-cost:   79
c ---[3626]---> BDD-cost:   79
c ---[3625]---> BDD-cost:  108
c ---[3624]---> BDD-cost:  110
c ---[3623]---> BDD-cost:   79
c ---[3622]---> BDD-cost:   79
c ---[3621]---> BDD-cost:   79
c ---[3620]---> BDD-cost:   79
c ---[3619]---> BDD-cost:  116
c ---[3617]---> BDD-cost:  110
c ---[3616]---> BDD-cost:   79
c ---[3615]---> BDD-cost:   79
c ---[3614]---> BDD-cost:   79
c ---[3613]---> BDD-cost:   79
c ---[3612]---> BDD-cost:  116
c ---[3611]---> BDD-cost:  110
c ---[3610]---> BDD-cost:   79
c ---[3609]---> BDD-cost:   79
c ---[3608]---> BDD-cost:   79
c ---[3606]---> BDD-cost:   79
c ---[3605]---> BDD-cost:  116
c ---[3604]---> BDD-cost:  110
c ---[3603]---> BDD-cost:   79
c ---[3602]---> BDD-cost:   79
c ---[3601]---> BDD-cost:   79
c ---[3600]---> BDD-cost:   79
c ---[3599]---> BDD-cost:  116
c ---[3598]---> BDD-cost:  110
c ---[3597]---> BDD-cost:   79
c ---[3595]---> BDD-cost:   79
c ---[3594]---> BDD-cost:   79
c ---[3593]---> BDD-cost:   79
c ---[3592]---> BDD-cost:  116
c ---[3591]---> BDD-cost:  110
c ---[3590]---> BDD-cost:   79
c ---[3589]---> BDD-cost:   79
c ---[3588]---> BDD-cost:   79
c ---[3587]---> BDD-cost:   79
c ---[3586]---> BDD-cost:  112
c ---[3583]---> BDD-cost:  112
c ---[3581]---> BDD-cost:  116
c ---[3579]---> BDD-cost:  114
c ---[3577]---> BDD-cost:   79
c ---[3575]---> BDD-cost:  116
c ---[3574]---> BDD-cost:  116
c ---[3572]---> BDD-cost:  116
c ---[3570]---> BDD-cost:  116
c ---[3568]---> BDD-cost:   79
c ---[3566]---> BDD-cost:  116
c ---[3564]---> BDD-cost:   79
c ---[3563]---> BDD-cost:  116
c ---[3561]---> BDD-cost:  116
c ---[3559]---> BDD-cost:  114
c ---[3557]---> BDD-cost:   79
c ---[3555]---> BDD-cost:  114
c ---[3553]---> BDD-cost:   79
c ---[3552]---> BDD-cost:  116
c ---[3550]---> BDD-cost:  116
c ---[3548]---> BDD-cost:   79
c ---[3546]---> BDD-cost:  114
c ---[3544]---> BDD-cost:   79
c ---[3542]---> BDD-cost:  116
c ---[3541]---> BDD-cost:   79
c ---[3539]---> BDD-cost:   79
c ---[3537]---> BDD-cost:  116
c ---[3535]---> BDD-cost:  112
c ---[3533]---> BDD-cost:   79
c ---[3531]---> BDD-cost:  116
c ---[3530]---> BDD-cost:  116
c ---[3528]---> BDD-cost:  116
c ---[3526]---> BDD-cost:  116
c ---[3524]---> BDD-cost:  114
c ---[3522]---> BDD-cost:  116
c ---[3520]---> BDD-cost:   79
c ---[3519]---> BDD-cost:  116
c ---[3517]---> BDD-cost:  116
c ---[3515]---> BDD-cost:  116
c ---[3513]---> BDD-cost:  116
c ---[3511]---> BDD-cost:   79
c ---[3509]---> BDD-cost:  114
c ---[3508]---> BDD-cost:  116
c ---[3506]---> BDD-cost:  116
c ---[3504]---> BDD-cost:  116
c ---[3502]---> BDD-cost:  116
c ---[3500]---> BDD-cost:  116
c ---[3498]---> BDD-cost:  114
c ---[3497]---> BDD-cost:  116
c ---[3495]---> BDD-cost:  116
c ---[3493]---> BDD-cost:  116
c ---[3491]---> BDD-cost:  116
c ---[3489]---> BDD-cost:  114
c ---[3487]---> BDD-cost:  116
c ---[3486]---> BDD-cost:  116
c ---[3484]---> BDD-cost:  116
c ---[3482]---> BDD-cost:  116
c ---[3480]---> BDD-cost:  116
c ---[3478]---> BDD-cost:  116
c ---[3476]---> BDD-cost:  116
c ---[3475]---> BDD-cost:  114
c ---[3472]---> BDD-cost:  114
c ---[3470]---> BDD-cost:  114
c ---[3468]---> BDD-cost:  116
c ---[3466]---> BDD-cost:  116
c ---[3464]---> BDD-cost:  116
c ---[3463]---> BDD-cost:  116
c ---[3461]---> BDD-cost:  116
c ---[3459]---> BDD-cost:  116
c ---[3457]---> BDD-cost:  116
c ---[3455]---> BDD-cost:  116
c ---[3453]---> BDD-cost:  116
c ---[3452]---> BDD-cost:   79
c ---[3450]---> BDD-cost:   79
c ---[3448]---> BDD-cost:  116
c ---[3446]---> BDD-cost:  114
c ---[3444]---> BDD-cost:   79
c ---[3442]---> BDD-cost:   79
c ---[3441]---> BDD-cost:  114
c ---[3439]---> BDD-cost:  114
c ---[3437]---> BDD-cost:   79
c ---[3435]---> BDD-cost:  116
c ---[3433]---> BDD-cost:  116
c ---[3431]---> BDD-cost:  114
c ---[3430]---> BDD-cost:   79
c ---[3428]---> BDD-cost:   79
c ---[3426]---> BDD-cost:  114
c ---[3424]---> BDD-cost:  116
c ---[3422]---> BDD-cost:  116
c ---[3420]---> BDD-cost:  116
c ---[3419]---> BDD-cost:  114
c ---[3417]---> BDD-cost:  114
c ---[3415]---> BDD-cost:   79
c ---[3413]---> BDD-cost:   79
c ---[3411]---> BDD-cost:  116
c ---[3409]---> BDD-cost:  116
c ---[3408]---> BDD-cost:  114
c ---[3406]---> BDD-cost:  114
c ---[3404]---> BDD-cost:  116
c ---[3402]---> BDD-cost:  116
c ---[3400]---> BDD-cost:  116
c ---[3398]---> BDD-cost:  116
c ---[3397]---> BDD-cost:   79
c ---[3395]---> BDD-cost:   79
c ---[3393]---> BDD-cost:  114
c ---[3391]---> BDD-cost:   79
c ---[3389]---> BDD-cost:  116
c ---[3387]---> BDD-cost:  116
c ---[3386]---> BDD-cost:  116
c ---[3384]---> BDD-cost:  116
c ---[3382]---> BDD-cost:  112
c ---[3380]---> BDD-cost:  114
c ---[3378]---> BDD-cost:  114
c ---[3376]---> BDD-cost:  116
c ---[3375]---> BDD-cost:  116
c ---[3373]---> BDD-cost:  116
c ---[3371]---> BDD-cost:  116
c ---[3369]---> BDD-cost:  116
c ---[3367]---> BDD-cost:  116
c ---[3365]---> BDD-cost:  116
c ---[3364]---> BDD-cost:  114
c ---[3361]---> BDD-cost:  114
c ---[3359]---> BDD-cost:  116
c ---[3357]---> BDD-cost:  116
c ---[3355]---> BDD-cost:  116
c ---[3353]---> BDD-cost:  116
c ---[3352]---> BDD-cost:  116
c ---[3350]---> BDD-cost:  116
c ---[3348]---> BDD-cost:  116
c ---[3346]---> BDD-cost:  116
c ---[3344]---> BDD-cost:   79
c ---[3342]---> BDD-cost:   79
c ---[3341]---> BDD-cost:  116
c ---[3339]---> BDD-cost:  116
c ---[3337]---> BDD-cost:   79
c ---[3335]---> BDD-cost:  114
c ---[3333]---> BDD-cost:  116
c ---[3331]---> BDD-cost:  116
c ---[3330]---> BDD-cost:  116
c ---[3328]---> BDD-cost:  116
c ---[3326]---> BDD-cost:  114
c ---[3324]---> BDD-cost:  116
c ---[3322]---> BDD-cost:  116
c ---[3320]---> BDD-cost:   79
c ---[3319]---> BDD-cost:  116
c ---[3317]---> BDD-cost:  116
c ---[3315]---> BDD-cost:   79
c ---[3313]---> BDD-cost:  116
c ---[3311]---> BDD-cost:  114
c ---[3309]---> BDD-cost:  116
c ---[3308]---> BDD-cost:   79
c ---[3306]---> BDD-cost:   79
c ---[3304]---> BDD-cost:   79
c ---[3302]---> BDD-cost:  116
c ---[3300]---> BDD-cost:  116
c ---[3298]---> BDD-cost:  116
c ---[3297]---> BDD-cost:   79
c ---[3295]---> BDD-cost:   79
c ---[3293]---> BDD-cost:   79
c ---[3291]---> BDD-cost:   79
c ---[3289]---> BDD-cost:  116
c ---[3287]---> BDD-cost:  116
c ---[3286]---> BDD-cost:   79
c ---[3284]---> BDD-cost:   79
c ---[3282]---> BDD-cost:  116
c ---[3280]---> BDD-cost:  116
c ---[3278]---> BDD-cost:   79
c ---[3276]---> BDD-cost:   79
c ---[3275]---> BDD-cost:  116
c ---[3273]---> BDD-cost:  116
c ---[3271]---> BDD-cost:  114
c ---[3269]---> BDD-cost:   79
c ---[3267]---> BDD-cost:   79
c ---[3265]---> BDD-cost:   79
c ---[3264]---> BDD-cost:  116
c ---[3262]---> BDD-cost:  116
c ---[3260]---> BDD-cost:  116
c ---[3258]---> BDD-cost:  116
c ---[3256]---> BDD-cost:  112
c ---[3254]---> BDD-cost:  112
c ---[3253]---> BDD-cost:   79
c ---[3250]---> BDD-cost:   79
c ---[3248]---> BDD-cost:  116
c ---[3246]---> BDD-cost:  116
c ---[3244]---> BDD-cost:   79
c ---[3242]---> BDD-cost:  116
c ---[3241]---> BDD-cost:  116
c ---[3239]---> BDD-cost:  116
c ---[3237]---> BDD-cost:   79
c ---[3235]---> BDD-cost:  112
c ---[3233]---> BDD-cost:   79
c ---[3231]---> BDD-cost:  114
c ---[3230]---> BDD-cost:  116
c ---[3228]---> BDD-cost:  116
c ---[3226]---> BDD-cost:  114
c ---[3224]---> BDD-cost:  114
c ---[3222]---> BDD-cost:   79
c ---[3220]---> BDD-cost:  116
c ---[3219]---> BDD-cost:  110
c ---[3217]---> BDD-cost:  110
c ---[3215]---> BDD-cost:  110
c ---[3213]---> BDD-cost:   79
c ---[3211]---> BDD-cost:  114
c ---[3209]---> BDD-cost:  114
c ---[3208]---> BDD-cost:  116
c ---[3206]---> BDD-cost:  116
c ---[3204]---> BDD-cost:  114
c ---[3202]---> BDD-cost:  116
c ---[3200]---> BDD-cost:  116
c ---[3198]---> BDD-cost:  116
c ---[3197]---> BDD-cost:   79
c ---[3195]---> BDD-cost:   79
c ---[3193]---> BDD-cost:  116
c ---[3191]---> BDD-cost:  116
c ---[3189]---> BDD-cost:  114
c ---[3187]---> BDD-cost:  114
c ---[3186]---> BDD-cost:   79
c ---[3184]---> BDD-cost:   79
c ---[3182]---> BDD-cost:  116
c ---[3180]---> BDD-cost:  116
c ---[3178]---> BDD-cost:  116
c ---[3176]---> BDD-cost:  116
c ---[3175]---> BDD-cost:  116
c ---[3173]---> BDD-cost:  116
c ---[3171]---> BDD-cost:  114
c ---[3169]---> BDD-cost:  114
c ---[3167]---> BDD-cost:  114
c ---[3165]---> BDD-cost:  116
c ---[3164]---> BDD-cost:  116
c ---[3162]---> BDD-cost:  116
c ---[3160]---> BDD-cost:  116
c ---[3158]---> BDD-cost:  114
c ---[3156]---> BDD-cost:  116
c ---[3154]---> BDD-cost:  116
c ---[3153]---> BDD-cost:  116
c ---[3151]---> BDD-cost:  116
c ---[3149]---> BDD-cost:  116
c ---[3147]---> BDD-cost:   79
c ---[3145]---> BDD-cost:  112
c ---[3143]---> BDD-cost:  116
c ---[3142]---> BDD-cost:  114
c ---[3139]---> BDD-cost:  114
c ---[3137]---> BDD-cost:  114
c ---[3135]---> BDD-cost:  114
c ---[3133]---> BDD-cost:  116
c ---[3131]---> BDD-cost:  114
c ---[3130]---> BDD-cost:  114
c ---[3128]---> BDD-cost:  114
c ---[3126]---> BDD-cost:  116
c ---[3124]---> BDD-cost:  116
c ---[3123]---> BDD-cost:  131
c ---[3122]---> BDD-cost:  131
c ---[3121]---> BDD-cost:  128
c ---[3120]---> BDD-cost:  128
c ---[3119]---> BDD-cost:  111
c ---[3117]---> BDD-cost:  111
c ---[3116]---> BDD-cost:  128
c ---[3115]---> BDD-cost:  128
c ---[3114]---> BDD-cost:  111
c ---[3113]---> BDD-cost:  111
c ---[3112]---> BDD-cost:  128
c ---[3111]---> BDD-cost:  128
c ---[3110]---> BDD-cost:  131
c ---[3109]---> BDD-cost:  131
c ---[3108]---> BDD-cost:  128
c ---[3106]---> BDD-cost:  128
c ---[3105]---> BDD-cost:  111
c ---[3104]---> BDD-cost:  111
c ---[3103]---> BDD-cost:  128
c ---[3102]---> BDD-cost:  128
c ---[3101]---> BDD-cost:  131
c ---[3100]---> BDD-cost:  131
c ---[3099]---> BDD-cost:  128
c ---[3098]---> BDD-cost:  128
c ---[3097]---> BDD-cost:  128
c ---[3095]---> BDD-cost:  128
c ---[3094]---> BDD-cost:  128
c ---[3093]---> BDD-cost:  128
c ---[3092]---> BDD-cost:  128
c ---[3091]---> BDD-cost:  128
c ---[3090]---> BDD-cost:  128
c ---[3089]---> BDD-cost:  128
c ---[3088]---> BDD-cost:  131
c ---[3087]---> BDD-cost:  131
c ---[3086]---> BDD-cost:  128
c ---[3084]---> BDD-cost:  128
c ---[3083]---> BDD-cost:  126
c ---[3082]---> BDD-cost:  126
c ---[3081]---> BDD-cost:  128
c ---[3080]---> BDD-cost:  128
c ---[3079]---> BDD-cost:  126
c ---[3078]---> BDD-cost:  126
c ---[3077]---> BDD-cost:  128
c ---[3076]---> BDD-cost:  128
c ---[3075]---> BDD-cost:  123
c ---[3073]---> BDD-cost:  123
c ---[3072]---> BDD-cost:  128
c ---[3071]---> BDD-cost:  128
c ---[3070]---> BDD-cost:  131
c ---[3069]---> BDD-cost:  131
c ---[3068]---> BDD-cost:  128
c ---[3067]---> BDD-cost:  128
c ---[3066]---> BDD-cost:  123
c ---[3065]---> BDD-cost:  123
c ---[3064]---> BDD-cost:  128
c ---[3062]---> BDD-cost:  128
c ---[3061]---> BDD-cost:  123
c ---[3060]---> BDD-cost:  123
c ---[3059]---> BDD-cost:  128
c ---[3058]---> BDD-cost:  128
c ---[3057]---> BDD-cost:  111
c ---[3056]---> BDD-cost:  111
c ---[3055]---> BDD-cost:  128
c ---[3054]---> BDD-cost:  128
c ---[3053]---> BDD-cost:  126
c ---[3051]---> BDD-cost:  126
c ---[3050]---> BDD-cost:  128
c ---[3049]---> BDD-cost:  128
c ---[3048]---> BDD-cost:  128
c ---[3047]---> BDD-cost:  128
c ---[3046]---> BDD-cost:  128
c ---[3045]---> BDD-cost:  128
c ---[3044]---> BDD-cost:  131
c ---[3043]---> BDD-cost:  131
c ---[3042]---> BDD-cost:  128
c ---[3040]---> BDD-cost:  128
c ---[3039]---> BDD-cost:  131
c ---[3038]---> BDD-cost:  131
c ---[3037]---> BDD-cost:  128
c ---[3036]---> BDD-cost:  128
c ---[3035]---> BDD-cost:  128
c ---[3034]---> BDD-cost:  128
c ---[3033]---> BDD-cost:  128
c ---[3032]---> BDD-cost:  128
c ---[3031]---> BDD-cost:  131
c ---[3028]---> BDD-cost:  131
c ---[3027]---> BDD-cost:  128
c ---[3026]---> BDD-cost:  128
c ---[3025]---> BDD-cost:  131
c ---[3024]---> BDD-cost:  131
c ---[3023]---> BDD-cost:  128
c ---[3022]---> BDD-cost:  128
c ---[3021]---> BDD-cost:  131
c ---[3020]---> BDD-cost:  131
c ---[3019]---> BDD-cost:  128
c ---[3017]---> BDD-cost:  128
c ---[3016]---> BDD-cost:  111
c ---[3015]---> BDD-cost:  111
c ---[3014]---> BDD-cost:  128
c ---[3013]---> BDD-cost:  128
c ---[3012]---> BDD-cost:  123
c ---[3011]---> BDD-cost:  123
c ---[3010]---> BDD-cost:  128
c ---[3009]---> BDD-cost:  128
c ---[3008]---> BDD-cost:  126
c ---[3006]---> BDD-cost:  126
c ---[3005]---> BDD-cost:  128
c ---[3004]---> BDD-cost:  128
c ---[3003]---> BDD-cost:  126
c ---[3002]---> BDD-cost:  126
c ---[3001]---> BDD-cost:  128
c ---[3000]---> BDD-cost:  128
c ---[2999]---> BDD-cost:  111
c ---[2998]---> BDD-cost:  111
c ---[2997]---> BDD-cost:  128
c ---[2995]---> BDD-cost:  128
c ---[2994]---> BDD-cost:  111
c ---[2993]---> BDD-cost:  111
c ---[2992]---> BDD-cost:  128
c ---[2991]---> BDD-cost:  128
c ---[2990]---> BDD-cost:  126
c ---[2989]---> BDD-cost:  126
c ---[2988]---> BDD-cost:  128
c ---[2987]---> BDD-cost:  128
c ---[2986]---> BDD-cost:  131
c ---[2984]---> BDD-cost:  131
c ---[2983]---> BDD-cost:  128
c ---[2982]---> BDD-cost:  128
c ---[2981]---> BDD-cost:  131
c ---[2980]---> BDD-cost:  131
c ---[2979]---> BDD-cost:  128
c ---[2978]---> BDD-cost:  128
c ---[2977]---> BDD-cost:  131
c ---[2976]---> BDD-cost:  131
c ---[2975]---> BDD-cost:  128
c ---[2973]---> BDD-cost:  128
c ---[2972]---> BDD-cost:  131
c ---[2971]---> BDD-cost:  131
c ---[2970]---> BDD-cost:  128
c ---[2969]---> BDD-cost:  128
c ---[2968]---> BDD-cost:  126
c ---[2967]---> BDD-cost:  126
c ---[2966]---> BDD-cost:  128
c ---[2965]---> BDD-cost:  128
c ---[2964]---> BDD-cost:  131
c ---[2962]---> BDD-cost:  131
c ---[2961]---> BDD-cost:  128
c ---[2960]---> BDD-cost:  128
c ---[2959]---> BDD-cost:  131
c ---[2958]---> BDD-cost:  131
c ---[2957]---> BDD-cost:  128
c ---[2956]---> BDD-cost:  128
c ---[2955]---> BDD-cost:  131
c ---[2954]---> BDD-cost:  131
c ---[2953]---> BDD-cost:  128
c ---[2951]---> BDD-cost:  128
c ---[2950]---> BDD-cost:  126
c ---[2949]---> BDD-cost:  126
c ---[2948]---> BDD-cost:  128
c ---[2947]---> BDD-cost:  128
c ---[2946]---> BDD-cost:  131
c ---[2945]---> BDD-cost:  131
c ---[2944]---> BDD-cost:  128
c ---[2943]---> BDD-cost:  128
c ---[2942]---> BDD-cost:  121
c ---[2940]---> BDD-cost:  121
c ---[2939]---> BDD-cost:  128
c ---[2938]---> BDD-cost:  128
c ---[2937]---> BDD-cost:  123
c ---[2936]---> BDD-cost:  123
c ---[2935]---> BDD-cost:  128
c ---[2934]---> BDD-cost:  128
c ---[2933]---> BDD-cost:  131
c ---[2932]---> BDD-cost:  131
c ---[2931]---> BDD-cost:  128
c ---[2929]---> BDD-cost:  128
c ---[2928]---> BDD-cost:  131
c ---[2927]---> BDD-cost:  131
c ---[2926]---> BDD-cost:  128
c ---[2925]---> BDD-cost:  128
c ---[2924]---> BDD-cost:  131
c ---[2923]---> BDD-cost:  131
c ---[2922]---> BDD-cost:  128
c ---[2921]---> BDD-cost:  128
c ---[2920]---> BDD-cost:  131
c ---[2917]---> BDD-cost:  131
c ---[2916]---> BDD-cost:  128
c ---[2915]---> BDD-cost:  128
c ---[2914]---> BDD-cost:  131
c ---[2913]---> BDD-cost:  131
c ---[2912]---> BDD-cost:  128
c ---[2911]---> BDD-cost:  128
c ---[2910]---> BDD-cost:  126
c ---[2909]---> BDD-cost:  126
c ---[2908]---> BDD-cost:  128
c ---[2906]---> BDD-cost:  128
c ---[2905]---> BDD-cost:  126
c ---[2904]---> BDD-cost:  126
c ---[2903]---> BDD-cost:  128
c ---[2902]---> BDD-cost:  128
c ---[2901]---> BDD-cost:  131
c ---[2900]---> BDD-cost:  131
c ---[2899]---> BDD-cost:  128
c ---[2898]---> BDD-cost:  128
c ---[2897]---> BDD-cost:  126
c ---[2895]---> BDD-cost:  126
c ---[2894]---> BDD-cost:  128
c ---[2893]---> BDD-cost:  128
c ---[2892]---> BDD-cost:  126
c ---[2891]---> BDD-cost:  126
c ---[2890]---> BDD-cost:  128
c ---[2889]---> BDD-cost:  128
c ---[2888]---> BDD-cost:  126
c ---[2887]---> BDD-cost:  126
c ---[2886]---> BDD-cost:  128
c ---[2884]---> BDD-cost:  128
c ---[2883]---> BDD-cost:  131
c ---[2882]---> BDD-cost:  131
c ---[2881]---> BDD-cost:  128
c ---[2880]---> BDD-cost:  128
c ---[2879]---> BDD-cost:  131
c ---[2878]---> BDD-cost:  131
c ---[2877]---> BDD-cost:  128
c ---[2876]---> BDD-cost:  128
c ---[2875]---> BDD-cost:  131
c ---[2873]---> BDD-cost:  131
c ---[2872]---> BDD-cost:  128
c ---[2871]---> BDD-cost:  128
c ---[2870]---> BDD-cost:  111
c ---[2869]---> BDD-cost:  111
c ---[2868]---> BDD-cost:  128
c ---[2867]---> BDD-cost:  128
c ---[2866]---> BDD-cost:  128
c ---[2865]---> BDD-cost:  128
c ---[2864]---> BDD-cost:  128
c ---[2862]---> BDD-cost:  128
c ---[2861]---> BDD-cost:  131
c ---[2860]---> BDD-cost:  131
c ---[2859]---> BDD-cost:  128
c ---[2858]---> BDD-cost:  128
c ---[2857]---> BDD-cost:  111
c ---[2856]---> BDD-cost:  111
c ---[2855]---> BDD-cost:  128
c ---[2854]---> BDD-cost:  128
c ---[2853]---> BDD-cost:  123
c ---[2851]---> BDD-cost:  123
c ---[2850]---> BDD-cost:  128
c ---[2849]---> BDD-cost:  128
c ---[2848]---> BDD-cost:  131
c ---[2847]---> BDD-cost:  131
c ---[2846]---> BDD-cost:  128
c ---[2845]---> BDD-cost:  128
c ---[2844]---> BDD-cost:  128
c ---[2843]---> BDD-cost:  128
c ---[2842]---> BDD-cost:  128
c ---[2840]---> BDD-cost:  128
c ---[2839]---> BDD-cost:  131
c ---[2838]---> BDD-cost:  131
c ---[2837]---> BDD-cost:  128
c ---[2836]---> BDD-cost:  128
c ---[2835]---> BDD-cost:  126
c ---[2834]---> BDD-cost:  126
c ---[2833]---> BDD-cost:  128
c ---[2832]---> BDD-cost:  128
c ---[2831]---> BDD-cost:  131
c ---[2829]---> BDD-cost:  131
c ---[2828]---> BDD-cost:  128
c ---[2827]---> BDD-cost:  128
c ---[2826]---> BDD-cost:  126
c ---[2825]---> BDD-cost:  126
c ---[2824]---> BDD-cost:  128
c ---[2823]---> BDD-cost:  128
c ---[2822]---> BDD-cost:  111
c ---[2821]---> BDD-cost:  111
c ---[2820]---> BDD-cost:  128
c ---[2818]---> BDD-cost:  128
c ---[2817]---> BDD-cost:  126
c ---[2816]---> BDD-cost:  126
c ---[2815]---> BDD-cost:  128
c ---[2814]---> BDD-cost:  128
c ---[2813]---> BDD-cost:  131
c ---[2812]---> BDD-cost:  131
c ---[2811]---> BDD-cost:  128
c ---[2810]---> BDD-cost:  128
c ---[2809]---> BDD-cost:  111
c ---[2805]---> BDD-cost:  111
c ---[2804]---> BDD-cost:  128
c ---[2803]---> BDD-cost:  128
c ---[2802]---> BDD-cost:  126
c ---[2801]---> BDD-cost:  126
c ---[2800]---> BDD-cost:  128
c ---[2799]---> BDD-cost:  128
c ---[2798]---> BDD-cost:  126
c ---[2797]---> BDD-cost:  126
c ---[2796]---> BDD-cost:  128
c ---[2794]---> BDD-cost:  128
c ---[2793]---> BDD-cost:  131
c ---[2792]---> BDD-cost:  131
c ---[2791]---> BDD-cost:  128
c ---[2790]---> BDD-cost:  128
c ---[2789]---> BDD-cost:  131
c ---[2788]---> BDD-cost:  131
c ---[2787]---> BDD-cost:  128
c ---[2786]---> BDD-cost:  128
c ---[2785]---> BDD-cost:  131
c ---[2783]---> BDD-cost:  131
c ---[2782]---> BDD-cost:  128
c ---[2781]---> BDD-cost:  128
c ---[2780]---> BDD-cost:  131
c ---[2779]---> BDD-cost:  131
c ---[2778]---> BDD-cost:  128
c ---[2777]---> BDD-cost:  128
c ---[2776]---> BDD-cost:  121
c ---[2775]---> BDD-cost:  121
c ---[2774]---> BDD-cost:  128
c ---[2772]---> BDD-cost:  128
c ---[2771]---> BDD-cost:  111
c ---[2770]---> BDD-cost:  111
c ---[2769]---> BDD-cost:  128
c ---[2768]---> BDD-cost:  128
c ---[2767]---> BDD-cost:  131
c ---[2766]---> BDD-cost:  131
c ---[2765]---> BDD-cost:  128
c ---[2764]---> BDD-cost:  128
c ---[2763]---> BDD-cost:  131
c ---[2761]---> BDD-cost:  131
c ---[2760]---> BDD-cost:  128
c ---[2759]---> BDD-cost:  128
c ---[2758]---> BDD-cost:  111
c ---[2757]---> BDD-cost:  111
c ---[2756]---> BDD-cost:  128
c ---[2755]---> BDD-cost:  128
c ---[2754]---> BDD-cost:  131
c ---[2753]---> BDD-cost:  131
c ---[2752]---> BDD-cost:  128
c ---[2750]---> BDD-cost:  128
c ---[2749]---> BDD-cost:  126
c ---[2748]---> BDD-cost:  126
c ---[2747]---> BDD-cost:  128
c ---[2746]---> BDD-cost:  128
c ---[2745]---> BDD-cost:  131
c ---[2744]---> BDD-cost:  131
c ---[2743]---> BDD-cost:  128
c ---[2742]---> BDD-cost:  128
c ---[2741]---> BDD-cost:  131
c ---[2739]---> BDD-cost:  131
c ---[2738]---> BDD-cost:  128
c ---[2737]---> BDD-cost:  128
c ---[2736]---> BDD-cost:  111
c ---[2735]---> BDD-cost:  111
c ---[2734]---> BDD-cost:  128
c ---[2733]---> BDD-cost:  128
c ---[2732]---> BDD-cost:  131
c ---[2731]---> BDD-cost:  131
c ---[2730]---> BDD-cost:  128
c ---[2728]---> BDD-cost:  128
c ---[2727]---> BDD-cost:  131
c ---[2726]---> BDD-cost:  131
c ---[2725]---> BDD-cost:  128
c ---[2724]---> BDD-cost:  128
c ---[2723]---> BDD-cost:  131
c ---[2722]---> BDD-cost:  131
c ---[2721]---> BDD-cost:  128
c ---[2720]---> BDD-cost:  128
c ---[2719]---> BDD-cost:  128
c ---[2717]---> BDD-cost:  128
c ---[2716]---> BDD-cost:  128
c ---[2715]---> BDD-cost:  128
c ---[2714]---> BDD-cost:  126
c ---[2713]---> BDD-cost:  126
c ---[2712]---> BDD-cost:  128
c ---[2711]---> BDD-cost:  128
c ---[2710]---> BDD-cost:  131
c ---[2709]---> BDD-cost:  131
c ---[2708]---> BDD-cost:  128
c ---[2706]---> BDD-cost:  128
c ---[2705]---> BDD-cost:  123
c ---[2704]---> BDD-cost:  123
c ---[2703]---> BDD-cost:  128
c ---[2702]---> BDD-cost:  128
c ---[2701]---> BDD-cost:  111
c ---[2700]---> BDD-cost:  111
c ---[2699]---> BDD-cost:  128
c ---[2698]---> BDD-cost:  128
c ---[2697]---> BDD-cost:  131
c ---[2694]---> BDD-cost:  131
c ---[2693]---> BDD-cost:  128
c ---[2692]---> BDD-cost:  128
c ---[2691]---> BDD-cost:  111
c ---[2690]---> BDD-cost:  111
c ---[2689]---> BDD-cost:  128
c ---[2688]---> BDD-cost:  128
c ---[2687]---> BDD-cost:  126
c ---[2686]---> BDD-cost:  126
c ---[2685]---> BDD-cost:  128
c ---[2683]---> BDD-cost:  128
c ---[2682]---> BDD-cost:  131
c ---[2681]---> BDD-cost:  131
c ---[2680]---> BDD-cost:  128
c ---[2679]---> BDD-cost:  128
c ---[2678]---> BDD-cost:  123
c ---[2677]---> BDD-cost:  123
c ---[2676]---> BDD-cost:  128
c ---[2675]---> BDD-cost:  128
c ---[2674]---> BDD-cost:  111
c ---[2672]---> BDD-cost:  111
c ---[2671]---> BDD-cost:  128
c ---[2670]---> BDD-cost:  128
c ---[2669]---> BDD-cost:  111
c ---[2668]---> BDD-cost:  111
c ---[2667]---> BDD-cost:  128
c ---[2666]---> BDD-cost:  128
c ---[2665]---> BDD-cost:  111
c ---[2664]---> BDD-cost:  111
c ---[2663]---> BDD-cost:  128
c ---[2661]---> BDD-cost:  128
c ---[2660]---> BDD-cost:  126
c ---[2659]---> BDD-cost:  126
c ---[2658]---> BDD-cost:  128
c ---[2657]---> BDD-cost:  128
c ---[2656]---> BDD-cost:  111
c ---[2655]---> BDD-cost:  128
c ---[2654]---> BDD-cost:  123
c ---[2653]---> BDD-cost:  131
c ---[2652]---> BDD-cost:  128
c ---[2650]---> BDD-cost:  131
c ---[2649]---> BDD-cost:  123
c ---[2648]---> BDD-cost:  134
c ---[2647]---> BDD-cost:  134
c ---[2646]---> BDD-cost:  122
c ---[2645]---> BDD-cost:  126
c ---[2644]---> BDD-cost:  128
c ---[2643]---> BDD-cost:  128
c ---[2642]---> BDD-cost:  118
c ---[2641]---> BDD-cost:  118
c ---[2639]---> BDD-cost:  118
c ---[2638]---> BDD-cost:  131
c ---[2637]---> BDD-cost:  118
c ---[2636]---> BDD-cost:  120
c ---[2635]---> BDD-cost:  128
c ---[2634]---> BDD-cost:  128
c ---[2633]---> BDD-cost:  115
c ---[2632]---> BDD-cost:  118
c ---[2631]---> BDD-cost:  128
c ---[2630]---> BDD-cost:  115
c ---[2628]---> BDD-cost:  128
c ---[2627]---> BDD-cost:  115
c ---[2626]---> BDD-cost:  118
c ---[2625]---> BDD-cost:  131
c ---[2624]---> BDD-cost:  120
c ---[2623]---> BDD-cost:  131
c ---[2622]---> BDD-cost:  123
c ---[2621]---> BDD-cost:  131
c ---[2620]---> BDD-cost:  128
c ---[2619]---> BDD-cost:  131
c ---[2617]---> BDD-cost:  120
c ---[2616]---> BDD-cost:  109
c ---[2615]---> BDD-cost:  117
c ---[2614]---> BDD-cost:  126
c ---[2613]---> BDD-cost:  131
c ---[2612]---> BDD-cost:  131
c ---[2611]---> BDD-cost:  131
c ---[2610]---> BDD-cost:  123
c ---[2609]---> BDD-cost:  111
c ---[2608]---> BDD-cost:  111
c ---[2606]---> BDD-cost:  131
c ---[2605]---> BDD-cost:  128
c ---[2604]---> BDD-cost:  126
c ---[2603]---> BDD-cost:  125
c ---[2602]---> BDD-cost:  116
c ---[2601]---> BDD-cost:  122
c ---[2600]---> BDD-cost:  128
c ---[2599]---> BDD-cost:  117
c ---[2598]---> BDD-cost:  123
c ---[2597]---> BDD-cost:  123
c ---[2595]---> BDD-cost:  111
c ---[2594]---> BDD-cost:  128
c ---[2593]---> BDD-cost:  131
c ---[2592]---> BDD-cost:  123
c ---[2591]---> BDD-cost:  126
c ---[2590]---> BDD-cost:  120
c ---[2589]---> BDD-cost:  121
c ---[2588]---> BDD-cost:  115
c ---[2587]---> BDD-cost:  131
c ---[2586]---> BDD-cost:  122
c ---[2583]---> BDD-cost:  126
c ---[2582]---> BDD-cost:  115
c ---[2581]---> BDD-cost:  126
c ---[2580]---> BDD-cost:  115
c ---[2579]---> BDD-cost:  120
c ---[2578]---> BDD-cost:  128
c ---[2577]---> BDD-cost:  134
c ---[2576]---> BDD-cost:  128
c ---[2575]---> BDD-cost:  116
c ---[2574]---> BDD-cost:  123
c ---[2572]---> BDD-cost:  131
c ---[2571]---> BDD-cost:  125
c ---[2570]---> BDD-cost:  125
c ---[2569]---> BDD-cost:  115
c ---[2568]---> BDD-cost:  131
c ---[2567]---> BDD-cost:  115
c ---[2566]---> BDD-cost:  131
c ---[2565]---> BDD-cost:  122
c ---[2564]---> BDD-cost:  131
c ---[2563]---> BDD-cost:  122
c ---[2561]---> BDD-cost:  117
c ---[2560]---> BDD-cost:  128
c ---[2559]---> BDD-cost:  116
c ---[2558]---> BDD-cost:  123
c ---[2557]---> BDD-cost:  131
c ---[2556]---> BDD-cost:  128
c ---[2555]---> BDD-cost:  125
c ---[2554]---> BDD-cost:  113
c ---[2553]---> BDD-cost:  131
c ---[2552]---> BDD-cost:  113
c ---[2550]---> BDD-cost:  131
c ---[2549]---> BDD-cost:  125
c ---[2548]---> BDD-cost:  131
c ---[2547]---> BDD-cost:  125
c ---[2546]---> BDD-cost:  128
c ---[2545]---> BDD-cost:  115
c ---[2544]---> BDD-cost:  113
c ---[2543]---> BDD-cost:  115
c ---[2542]---> BDD-cost:  128
c ---[2541]---> BDD-cost:  115
c ---[2539]---> BDD-cost:  118
c ---[2538]---> BDD-cost:  122
c ---[2537]---> BDD-cost:  111
c ---[2536]---> BDD-cost:  117
c ---[2535]---> BDD-cost:  121
c ---[2534]---> BDD-cost:  111
c ---[2533]---> BDD-cost:  126
c ---[2532]---> BDD-cost:  123
c ---[2531]---> BDD-cost:  116
c ---[2530]---> BDD-cost:  123
c ---[2528]---> BDD-cost:  126
c ---[2527]---> BDD-cost:  128
c ---[2526]---> BDD-cost:  116
c ---[2525]---> BDD-cost:  125
c ---[2524]---> BDD-cost:  123
c ---[2523]---> BDD-cost:  120
c ---[2522]---> BDD-cost:  128
c ---[2521]---> BDD-cost:  120
c ---[2520]---> BDD-cost:  111
c ---[2519]---> BDD-cost:  120
c ---[2517]---> BDD-cost:  122
c ---[2516]---> BDD-cost:  125
c ---[2515]---> BDD-cost:  131
c ---[2514]---> BDD-cost:  115
c ---[2513]---> BDD-cost:  131
c ---[2512]---> BDD-cost:  122
c ---[2511]---> BDD-cost:  118
c ---[2510]---> BDD-cost:  122
c ---[2509]---> BDD-cost:  128
c ---[2508]---> BDD-cost:  122
c ---[2506]---> BDD-cost:  113
c ---[2505]---> BDD-cost:  122
c ---[2504]---> BDD-cost:  126
c ---[2503]---> BDD-cost:  117
c ---[2502]---> BDD-cost:  126
c ---[2501]---> BDD-cost:  128
c ---[2500]---> BDD-cost:  131
c ---[2499]---> BDD-cost:  128
c ---[2498]---> BDD-cost:  131
c ---[2497]---> BDD-cost:  123
c ---[2495]---> BDD-cost:  131
c ---[2494]---> BDD-cost:  113
c ---[2493]---> BDD-cost:  128
c ---[2492]---> BDD-cost:  125
c ---[2491]---> BDD-cost:  118
c ---[2490]---> BDD-cost:  125
c ---[2489]---> BDD-cost:  131
c ---[2488]---> BDD-cost:  125
c ---[2487]---> BDD-cost:  117
c ---[2486]---> BDD-cost:  120
c ---[2484]---> BDD-cost:  121
c ---[2483]---> BDD-cost:  125
c ---[2482]---> BDD-cost:  126
c ---[2481]---> BDD-cost:  115
c ---[2480]---> BDD-cost:  128
c ---[2479]---> BDD-cost:  115
c ---[2478]---> BDD-cost:  123
c ---[2477]---> BDD-cost:  115
c ---[2476]---> BDD-cost:  128
c ---[2475]---> BDD-cost:  115
c ---[2472]---> BDD-cost:  131
c ---[2471]---> BDD-cost:  122
c ---[2470]---> BDD-cost:  131
c ---[2469]---> BDD-cost:  131
c ---[2468]---> BDD-cost:  117
c ---[2467]---> BDD-cost:  128
c ---[2466]---> BDD-cost:  118
c ---[2465]---> BDD-cost:  126
c ---[2464]---> BDD-cost:  123
c ---[2463]---> BDD-cost:  115
c ---[2461]---> BDD-cost:  128
c ---[2460]---> BDD-cost:  111
c ---[2459]---> BDD-cost:  125
c ---[2458]---> BDD-cost:  113
c ---[2457]---> BDD-cost:  131
c ---[2456]---> BDD-cost:  131
c ---[2455]---> BDD-cost:  131
c ---[2454]---> BDD-cost:  111
c ---[2453]---> BDD-cost:  131
c ---[2452]---> BDD-cost:  123
c ---[2450]---> BDD-cost:  131
c ---[2449]---> BDD-cost:  128
c ---[2448]---> BDD-cost:  111
c ---[2447]---> BDD-cost:  128
c ---[2446]---> BDD-cost:  131
c ---[2445]---> BDD-cost:  118
c ---[2444]---> BDD-cost:  116
c ---[2443]---> BDD-cost:  128
c ---[2442]---> BDD-cost:  111
c ---[2441]---> BDD-cost:  123
c ---[2439]---> BDD-cost:  131
c ---[2438]---> BDD-cost:  123
c ---[2437]---> BDD-cost:  118
c ---[2436]---> BDD-cost:  123
c ---[2435]---> BDD-cost:  128
c ---[2434]---> BDD-cost:  123
c ---[2433]---> BDD-cost:  131
c ---[2432]---> BDD-cost:  128
c ---[2431]---> BDD-cost:  131
c ---[2430]---> BDD-cost:  113
c ---[2428]---> BDD-cost:  128
c ---[2427]---> BDD-cost:  125
c ---[2426]---> BDD-cost:  121
c ---[2425]---> BDD-cost:  120
c ---[2424]---> BDD-cost:  116
c ---[2423]---> BDD-cost:  120
c ---[2422]---> BDD-cost:  131
c ---[2421]---> BDD-cost:  120
c ---[2420]---> BDD-cost:  126
c ---[2419]---> BDD-cost:  122
c ---[2417]---> BDD-cost:  128
c ---[2416]---> BDD-cost:  122
c ---[2415]---> BDD-cost:  118
c ---[2414]---> BDD-cost:  122
c ---[2413]---> BDD-cost:  126
c ---[2412]---> BDD-cost:  117
c ---[2411]---> BDD-cost:  117
c ---[2410]---> BDD-cost:  111
c ---[2409]---> BDD-cost:  131
c ---[2408]---> BDD-cost:  123
c ---[2406]---> BDD-cost:  131
c ---[2405]---> BDD-cost:  128
c ---[2404]---> BDD-cost:  126
c ---[2403]---> BDD-cost:  128
c ---[2402]---> BDD-cost:  131
c ---[2401]---> BDD-cost:  118
c ---[2400]---> BDD-cost:  126
c ---[2399]---> BDD-cost:  128
c ---[2398]---> BDD-cost:  123
c ---[2397]---> BDD-cost:  123
c ---[2395]---> BDD-cost:  131
c ---[2394]---> BDD-cost:  123
c ---[2393]---> BDD-cost:  123
c ---[2392]---> BDD-cost:  123
c ---[2391]---> BDD-cost:  131
c ---[2390]---> BDD-cost:  123
c ---[2389]---> BDD-cost:  131
c ---[2388]---> BDD-cost:  128
c ---[2387]---> BDD-cost:  131
c ---[2386]---> BDD-cost:  113
c ---[2384]---> BDD-cost:  131
c ---[2383]---> BDD-cost:  125
c ---[2382]---> BDD-cost:  126
c ---[2381]---> BDD-cost:  120
c ---[2380]---> BDD-cost:  126
c ---[2379]---> BDD-cost:  120
c ---[2378]---> BDD-cost:  131
c ---[2377]---> BDD-cost:  120
c ---[2376]---> BDD-cost:  111
c ---[2375]---> BDD-cost:  125
c ---[2373]---> BDD-cost:  117
c ---[2372]---> BDD-cost:  122
c ---[2371]---> BDD-cost:  131
c ---[2370]---> BDD-cost:  122
c ---[2369]---> BDD-cost:  126
c ---[2368]---> BDD-cost:  122
c ---[2367]---> BDD-cost:  109
c ---[2366]---> BDD-cost:  128
c ---[2365]---> BDD-cost:  131
c ---[2364]---> BDD-cost:  123
c ---[2361]---> BDD-cost:  121
c ---[2360]---> BDD-cost:  123
c ---[2359]---> BDD-cost:  131
c ---[2358]---> BDD-cost:  128
c ---[2357]---> BDD-cost:  121
c ---[2356]---> BDD-cost:  118
c ---[2355]---> BDD-cost:  111
c ---[2354]---> BDD-cost:  128
c ---[2353]---> BDD-cost:  131
c ---[2352]---> BDD-cost:  128
c ---[2350]---> BDD-cost:  118
c ---[2349]---> BDD-cost:  128
c ---[2348]---> BDD-cost:  131
c ---[2347]---> BDD-cost:  128
c ---[2346]---> BDD-cost:  131
c ---[2345]---> BDD-cost:  123
c ---[2344]---> BDD-cost:  131
c ---[2343]---> BDD-cost:  128
c ---[2342]---> BDD-cost:  131
c ---[2341]---> BDD-cost:  113
c ---[2339]---> BDD-cost:  121
c ---[2338]---> BDD-cost:  125
c ---[2337]---> BDD-cost:  121
c ---[2336]---> BDD-cost:  125
c ---[2335]---> BDD-cost:  134
c ---[2334]---> BDD-cost:  125
c ---[2333]---> BDD-cost:  126
c ---[2332]---> BDD-cost:  115
c ---[2331]---> BDD-cost:  131
c ---[2330]---> BDD-cost:  115
c ---[2328]---> BDD-cost:  111
c ---[2327]---> BDD-cost:  115
c ---[2326]---> BDD-cost:  126
c ---[2325]---> BDD-cost:  122
c ---[2324]---> BDD-cost:  117
c ---[2323]---> BDD-cost:  111
c ---[2322]---> BDD-cost:  126
c ---[2321]---> BDD-cost:  111
c ---[2320]---> BDD-cost:  131
c ---[2319]---> BDD-cost:  128
c ---[2317]---> BDD-cost:  126
c ---[2316]---> BDD-cost:  123
c ---[2315]---> BDD-cost:  120
c ---[2314]---> BDD-cost:  128
c ---[2313]---> BDD-cost:  131
c ---[2312]---> BDD-cost:  128
c ---[2311]---> BDD-cost:  117
c ---[2310]---> BDD-cost:  128
c ---[2309]---> BDD-cost:  131
c ---[2308]---> BDD-cost:  128
c ---[2306]---> BDD-cost:  128
c ---[2305]---> BDD-cost:  118
c ---[2304]---> BDD-cost:  131
c ---[2303]---> BDD-cost:  128
c ---[2302]---> BDD-cost:  131
c ---[2301]---> BDD-cost:  123
c ---[2300]---> BDD-cost:  126
c ---[2299]---> BDD-cost:  128
c ---[2298]---> BDD-cost:  121
c ---[2297]---> BDD-cost:  128
c ---[2295]---> BDD-cost:  131
c ---[2294]---> BDD-cost:  128
c ---[2293]---> BDD-cost:  113
c ---[2292]---> BDD-cost:  113
c ---[2291]---> BDD-cost:  117
c ---[2290]---> BDD-cost:  120
c ---[2289]---> BDD-cost:  131
c ---[2288]---> BDD-cost:  120
c ---[2287]---> BDD-cost:  126
c ---[2286]---> BDD-cost:  120
c ---[2284]---> BDD-cost:  109
c ---[2283]---> BDD-cost:  109
c ---[2282]---> BDD-cost:  131
c ---[2281]---> BDD-cost:  131
c ---[2280]---> BDD-cost:  121
c ---[2279]---> BDD-cost:  111
c ---[2278]---> BDD-cost:  131
c ---[2277]---> BDD-cost:  128
c ---[2276]---> BDD-cost:  122
c ---[2275]---> BDD-cost:  123
c ---[2273]---> BDD-cost:  129
c ---[2272]---> BDD-cost:  129
c ---[2271]---> BDD-cost:  123
c ---[2270]---> BDD-cost:  126
c ---[2269]---> BDD-cost:  123
c ---[2268]---> BDD-cost:  123
c ---[2267]---> BDD-cost:  128
c ---[2266]---> BDD-cost:  111
c ---[2265]---> BDD-cost:  118
c ---[2264]---> BDD-cost:  109
c ---[2262]---> BDD-cost:  128
c ---[2261]---> BDD-cost:  128
c ---[2260]---> BDD-cost:  123
c ---[2259]---> BDD-cost:  131
c ---[2258]---> BDD-cost:  123
c ---[2257]---> BDD-cost:  121
c ---[2256]---> BDD-cost:  123
c ---[2255]---> BDD-cost:  125
c ---[2254]---> BDD-cost:  128
c ---[2253]---> BDD-cost:  128
c ---[2250]---> BDD-cost:  125
c ---[2249]---> BDD-cost:  109
c ---[2248]---> BDD-cost:  125
c ---[2247]---> BDD-cost:  118
c ---[2246]---> BDD-cost:  125
c ---[2245]---> BDD-cost:  131
c ---[2244]---> BDD-cost:  125
c ---[2243]---> BDD-cost:  131
c ---[2242]---> BDD-cost:  111
c ---[2241]---> BDD-cost:  121
c ---[2239]---> BDD-cost:  128
c ---[2238]---> BDD-cost:  113
c ---[2237]---> BDD-cost:  123
c ---[2236]---> BDD-cost:  131
c ---[2235]---> BDD-cost:  123
c ---[2234]---> BDD-cost:  115
c ---[2233]---> BDD-cost:  123
c ---[2232]---> BDD-cost:  131
c ---[2231]---> BDD-cost:  123
c ---[2230]---> BDD-cost:  128
c ---[2228]---> BDD-cost:  128
c ---[2227]---> BDD-cost:  131
c ---[2226]---> BDD-cost:  118
c ---[2225]---> BDD-cost:  131
c ---[2224]---> BDD-cost:  128
c ---[2223]---> BDD-cost:  121
c ---[2222]---> BDD-cost:  123
c ---[2221]---> BDD-cost:  126
c ---[2220]---> BDD-cost:  123
c ---[2219]---> BDD-cost:  131
c ---[2217]---> BDD-cost:  123
c ---[2216]---> BDD-cost:  123
c ---[2215]---> BDD-cost:  128
c ---[2214]---> BDD-cost:  113
c ---[2213]---> BDD-cost:  125
c ---[2212]---> BDD-cost:  131
c ---[2211]---> BDD-cost:  125
c ---[2210]---> BDD-cost:  125
c ---[2209]---> BDD-cost:  125
c ---[2208]---> BDD-cost:  116
c ---[2206]---> BDD-cost:  125
c ---[2205]---> BDD-cost:  129
c ---[2204]---> BDD-cost:  128
c ---[2203]---> BDD-cost:  128
c ---[2202]---> BDD-cost:  123
c ---[2201]---> BDD-cost:  131
c ---[2200]---> BDD-cost:  123
c ---[2199]---> BDD-cost:  113
c ---[2198]---> BDD-cost:  128
c ---[2197]---> BDD-cost:  120
c ---[2195]---> BDD-cost:  128
c ---[2194]---> BDD-cost:  125
c ---[2193]---> BDD-cost:  123
c ---[2192]---> BDD-cost:  117
c ---[2191]---> BDD-cost:  123
c ---[2190]---> BDD-cost:  128
c ---[2189]---> BDD-cost:  120
c ---[2188]---> BDD-cost:  131
c ---[2187]---> BDD-cost:  125
c ---[2186]---> BDD-cost:  116
c ---[2184]---> BDD-cost:  111
c ---[2183]---> BDD-cost:  128
c ---[2182]---> BDD-cost:  128
c ---[2181]---> BDD-cost:  116
c ---[2180]---> BDD-cost:  128
c ---[2179]---> BDD-cost:  125
c ---[2178]---> BDD-cost:  128
c ---[2177]---> BDD-cost:  121
c ---[2176]---> BDD-cost:  128
c ---[2175]---> BDD-cost:  126
c ---[2173]---> BDD-cost:  123
c ---[2172]---> BDD-cost:  116
c ---[2171]---> BDD-cost:  128
c ---[2170]---> BDD-cost:  126
c ---[2169]---> BDD-cost:  118
c ---[2168]---> BDD-cost:  131
c ---[2167]---> BDD-cost:  128
c ---[2166]---> BDD-cost:  131
c ---[2165]---> BDD-cost:  128
c ---[2164]---> BDD-cost:  121
c ---[2162]---> BDD-cost:  128
c ---[2161]---> BDD-cost:  128
c ---[2160]---> BDD-cost:  123
c ---[2159]---> BDD-cost:  122
c ---[2158]---> BDD-cost:  113
c ---[2157]---> BDD-cost:  126
c ---[2156]---> BDD-cost:  113
c ---[2155]---> BDD-cost:  117
c ---[2154]---> BDD-cost:  113
c ---[2153]---> BDD-cost:  131
c ---[2151]---> BDD-cost:  113
c ---[2150]---> BDD-cost:  134
c ---[2149]---> BDD-cost:  111
c ---[2148]---> BDD-cost:  115
c ---[2147]---> BDD-cost:  111
c ---[2146]---> BDD-cost:  131
c ---[2145]---> BDD-cost:  111
c ---[2144]---> BDD-cost:  116
c ---[2143]---> BDD-cost:  128
c ---[2142]---> BDD-cost:  126
c ---[2139]---> BDD-cost:  123
c ---[2138]---> BDD-cost:  117
c ---[2137]---> BDD-cost:  128
c ---[2136]---> BDD-cost:  131
c ---[2135]---> BDD-cost:  118
c ---[2134]---> BDD-cost:  128
c ---[2133]---> BDD-cost:  118
c ---[2132]---> BDD-cost:  126
c ---[2131]---> BDD-cost:  118
c ---[2130]---> BDD-cost:  131
c ---[2128]---> BDD-cost:  128
c ---[2127]---> BDD-cost:  117
c ---[2126]---> BDD-cost:  128
c ---[2125]---> BDD-cost:  128
c ---[2124]---> BDD-cost:  113
c ---[2123]---> BDD-cost:  128
c ---[2122]---> BDD-cost:  125
c ---[2121]---> BDD-cost:  117
c ---[2120]---> BDD-cost:  131
c ---[2119]---> BDD-cost:  131
c ---[2117]---> BDD-cost:  131
c ---[2116]---> BDD-cost:  131
c ---[2115]---> BDD-cost:  131
c ---[2114]---> BDD-cost:  128
c ---[2113]---> BDD-cost:  111
c ---[2112]---> BDD-cost:  131
c ---[2111]---> BDD-cost:  128
c ---[2110]---> BDD-cost:  134
c ---[2109]---> BDD-cost:  123
c ---[2108]---> BDD-cost:  111
c ---[2106]---> BDD-cost:  128
c ---[2105]---> BDD-cost:  126
c ---[2104]---> BDD-cost:  128
c ---[2103]---> BDD-cost:  131
c ---[2102]---> BDD-cost:  128
c ---[2101]---> BDD-cost:  120
c ---[2100]---> BDD-cost:  118
c ---[2099]---> BDD-cost:  123
c ---[2098]---> BDD-cost:  123
c ---[2097]---> BDD-cost:  134
c ---[2095]---> BDD-cost:  123
c ---[2094]---> BDD-cost:  128
c ---[2093]---> BDD-cost:  123
c ---[2092]---> BDD-cost:  126
c ---[2091]---> BDD-cost:  123
c ---[2090]---> BDD-cost:  126
c ---[2089]---> BDD-cost:  131
c ---[2088]---> BDD-cost:  131
c ---[2087]---> BDD-cost:  121
c ---[2086]---> BDD-cost:  111
c ---[2084]---> BDD-cost:  126
c ---[2083]---> BDD-cost:  123
c ---[2082]---> BDD-cost:  131
c ---[2081]---> BDD-cost:  128
c ---[2080]---> BDD-cost:  125
c ---[2079]---> BDD-cost:  128
c ---[2078]---> BDD-cost:  123
c ---[2077]---> BDD-cost:  128
c ---[2076]---> BDD-cost:  131
c ---[2075]---> BDD-cost:  123
c ---[2073]---> BDD-cost:  128
c ---[2072]---> BDD-cost:  128
c ---[2071]---> BDD-cost:  131
c ---[2070]---> BDD-cost:  113
c ---[2069]---> BDD-cost:  123
c ---[2068]---> BDD-cost:  131
c ---[2067]---> BDD-cost:  131
c ---[2066]---> BDD-cost:  125
c ---[2065]---> BDD-cost:  111
c ---[2064]---> BDD-cost:  128
c ---[2062]---> BDD-cost:  128
c ---[2061]---> BDD-cost:  134
c ---[2060]---> BDD-cost:  123
c ---[2059]---> BDD-cost:  118
c ---[2058]---> BDD-cost:  128
c ---[2057]---> BDD-cost:  126
c ---[2056]---> BDD-cost:  128
c ---[2055]---> BDD-cost:  131
c ---[2054]---> BDD-cost:  128
c ---[2053]---> BDD-cost:  117
c ---[2051]---> BDD-cost:  118
c ---[2050]---> BDD-cost:  123
c ---[2049]---> BDD-cost:  123
c ---[2048]---> BDD-cost:  131
c ---[2047]---> BDD-cost:  123
c ---[2046]---> BDD-cost:  128
c ---[2045]---> BDD-cost:  123
c ---[2044]---> BDD-cost:  126
c ---[2043]---> BDD-cost:  123
c ---[2042]---> BDD-cost:  126
c ---[2040]---> BDD-cost:  111
c ---[2039]---> BDD-cost:  131
c ---[2038]---> BDD-cost:  128
c ---[2037]---> BDD-cost:  128
c ---[2036]---> BDD-cost:  123
c ---[2035]---> BDD-cost:  121
c ---[2034]---> BDD-cost:  128
c ---[2033]---> BDD-cost:  126
c ---[2032]---> BDD-cost:  128
c ---[2031]---> BDD-cost:  131
c ---[2028]---> BDD-cost:  128
c ---[2027]---> BDD-cost:  126
c ---[2026]---> BDD-cost:  123
c ---[2025]---> BDD-cost:  128
c ---[2024]---> BDD-cost:  123
c ---[2023]---> BDD-cost:  120
c ---[2022]---> BDD-cost:  123
c ---[2021]---> BDD-cost:  121
c ---[2020]---> BDD-cost:  128
c ---[2019]---> BDD-cost:  123
c ---[2017]---> BDD-cost:  111
c ---[2016]---> BDD-cost:  128
c ---[2015]---> BDD-cost:  128
c ---[2014]---> BDD-cost:  129
c ---[2013]---> BDD-cost:  129
c ---[2012]---> BDD-cost:  123
c ---[2011]---> BDD-cost:  116
c ---[2010]---> BDD-cost:  123
c ---[2009]---> BDD-cost:  131
c ---[2008]---> BDD-cost:  123
c ---[2006]---> BDD-cost:  116
c ---[2005]---> BDD-cost:  128
c ---[2004]---> BDD-cost:  128
c ---[2003]---> BDD-cost:  128
c ---[2002]---> BDD-cost:  118
c ---[2001]---> BDD-cost:  128
c ---[2000]---> BDD-cost:  126
c ---[1999]---> BDD-cost:  123
c ---[1998]---> BDD-cost:  113
c ---[1997]---> BDD-cost:  117
c ---[1995]---> BDD-cost:  121
c ---[1994]---> BDD-cost:  111
c ---[1993]---> BDD-cost:  123
c ---[1992]---> BDD-cost:  128
c ---[1991]---> BDD-cost:  116
c ---[1990]---> BDD-cost:  128
c ---[1989]---> BDD-cost:  131
c ---[1988]---> BDD-cost:  128
c ---[1987]---> BDD-cost:  115
c ---[1986]---> BDD-cost:  123
c ---[1984]---> BDD-cost:  126
c ---[1983]---> BDD-cost:  118
c ---[1982]---> BDD-cost:  134
c ---[1981]---> BDD-cost:  118
c ---[1980]---> BDD-cost:  131
c ---[1979]---> BDD-cost:  118
c ---[1978]---> BDD-cost:  129
c ---[1977]---> BDD-cost:  118
c ---[1976]---> BDD-cost:  121
c ---[1975]---> BDD-cost:  122
c ---[1973]---> BDD-cost:  113
c ---[1972]---> BDD-cost:  118
c ---[1971]---> BDD-cost:  115
c ---[1970]---> BDD-cost:  125
c ---[1969]---> BDD-cost:  126
c ---[1968]---> BDD-cost:  111
c ---[1967]---> BDD-cost:  131
c ---[1966]---> BDD-cost:  111
c ---[1965]---> BDD-cost:  126
c ---[1964]---> BDD-cost:  111
c ---[1962]---> BDD-cost:  131
c ---[1961]---> BDD-cost:  128
c ---[1960]---> BDD-cost:  123
c ---[1959]---> BDD-cost:  128
c ---[1958]---> BDD-cost:  128
c ---[1957]---> BDD-cost:  128
c ---[1956]---> BDD-cost:  131
c ---[1955]---> BDD-cost:  118
c ---[1954]---> BDD-cost:  125
c ---[1953]---> BDD-cost:  115
c ---[1951]---> BDD-cost:  131
c ---[1950]---> BDD-cost:  131
c ---[1949]---> BDD-cost:  131
c ---[1948]---> BDD-cost:  121
c ---[1947]---> BDD-cost:  131
c ---[1946]---> BDD-cost:  131
c ---[1945]---> BDD-cost:  128
c ---[1944]---> BDD-cost:  111
c ---[1943]---> BDD-cost:  125
c ---[1942]---> BDD-cost:  123
c ---[1940]---> BDD-cost:  116
c ---[1939]---> BDD-cost:  123
c ---[1938]---> BDD-cost:  115
c ---[1937]---> BDD-cost:  123
c ---[1936]---> BDD-cost:  131
c ---[1935]---> BDD-cost:  123
c ---[1934]---> BDD-cost:  134
c ---[1933]---> BDD-cost:  125
c ---[1932]---> BDD-cost:  131
c ---[1931]---> BDD-cost:  131
c ---[1929]---> BDD-cost:  131
c ---[1928]---> BDD-cost:  121
c ---[1927]---> BDD-cost:  123
c ---[1926]---> BDD-cost:  131
c ---[1925]---> BDD-cost:  123
c ---[1924]---> BDD-cost:  111
c ---[1923]---> BDD-cost:  123
c ---[1922]---> BDD-cost:  126
c ---[1921]---> BDD-cost:  128
c ---[1920]---> BDD-cost:  115
c ---[1917]---> BDD-cost:  125
c ---[1916]---> BDD-cost:  116
c ---[1915]---> BDD-cost:  123
c ---[1914]---> BDD-cost:  115
c ---[1913]---> BDD-cost:  123
c ---[1912]---> BDD-cost:  128
c ---[1911]---> BDD-cost:  128
c ---[1910]---> BDD-cost:  131
c ---[1909]---> BDD-cost:  118
c ---[1908]---> BDD-cost:  120
c ---[1906]---> BDD-cost:  125
c ---[1905]---> BDD-cost:  131
c ---[1904]---> BDD-cost:  128
c ---[1903]---> BDD-cost:  123
c ---[1902]---> BDD-cost:  128
c ---[1901]---> BDD-cost:  109
c ---[1900]---> BDD-cost:  128
c ---[1899]---> BDD-cost:  131
c ---[1898]---> BDD-cost:  128
c ---[1897]---> BDD-cost:  128
c ---[1895]---> BDD-cost:  123
c ---[1894]---> BDD-cost:  111
c ---[1893]---> BDD-cost:  117
c ---[1892]---> BDD-cost:  123
c ---[1891]---> BDD-cost:  117
c ---[1890]---> BDD-cost:  131
c ---[1889]---> BDD-cost:  131
c ---[1888]---> BDD-cost:  131
c ---[1887]---> BDD-cost:  128
c ---[1886]---> BDD-cost:  131
c ---[1884]---> BDD-cost:  131
c ---[1883]---> BDD-cost:  126
c ---[1882]---> BDD-cost:  131
c ---[1881]---> BDD-cost:  131
c ---[1880]---> BDD-cost:  121
c ---[1879]---> BDD-cost:  113
c ---[1878]---> BDD-cost:  113
c ---[1877]---> BDD-cost:  115
c ---[1876]---> BDD-cost:  131
c ---[1875]---> BDD-cost:  115
c ---[1873]---> BDD-cost:  116
c ---[1872]---> BDD-cost:  131
c ---[1871]---> BDD-cost:  131
c ---[1870]---> BDD-cost:  111
c ---[1869]---> BDD-cost:  131
c ---[1868]---> BDD-cost:  131
c ---[1867]---> BDD-cost:  113
c ---[1866]---> BDD-cost:  118
c ---[1865]---> BDD-cost:  131
c ---[1864]---> BDD-cost:  115
c ---[1862]---> BDD-cost:  128
c ---[1861]---> BDD-cost:  115
c ---[1860]---> BDD-cost:  126
c ---[1859]---> BDD-cost:  131
c ---[1858]---> BDD-cost:  131
c ---[1857]---> BDD-cost:  131
c ---[1856]---> BDD-cost:  113
c ---[1855]---> BDD-cost:  125
c ---[1854]---> BDD-cost:  115
c ---[1853]---> BDD-cost:  126
c ---[1851]---> BDD-cost:  115
c ---[1850]---> BDD-cost:  131
c ---[1849]---> BDD-cost:  113
c ---[1848]---> BDD-cost:  131
c ---[1847]---> BDD-cost:  115
c ---[1846]---> BDD-cost:  109
c ---[1845]---> BDD-cost:  115
c ---[1844]---> BDD-cost:  131
c ---[1843]---> BDD-cost:  111
c ---[1842]---> BDD-cost:  111
c ---[1840]---> BDD-cost:  128
c ---[1839]---> BDD-cost:  128
c ---[1838]---> BDD-cost:  117
c ---[1837]---> BDD-cost:  131
c ---[1836]---> BDD-cost:  123
c ---[1835]---> BDD-cost:  117
c ---[1834]---> BDD-cost:  122
c ---[1833]---> BDD-cost:  126
c ---[1832]---> BDD-cost:  128
c ---[1831]---> BDD-cost:  120
c ---[1829]---> BDD-cost:  125
c ---[1828]---> BDD-cost:  126
c ---[1827]---> BDD-cost:  128
c ---[1826]---> BDD-cost:  118
c ---[1825]---> BDD-cost:  123
c ---[1824]---> BDD-cost:  131
c ---[1823]---> BDD-cost:  128
c ---[1822]---> BDD-cost:  126
c ---[1821]---> BDD-cost:  125
c ---[1820]---> BDD-cost:  128
c ---[1818]---> BDD-cost:  125
c ---[1817]---> BDD-cost:  128
c ---[1816]---> BDD-cost:  131
c ---[1815]---> BDD-cost:  131
c ---[1814]---> BDD-cost:  121
c ---[1813]---> BDD-cost:  128
c ---[1812]---> BDD-cost:  131
c ---[1811]---> BDD-cost:  128
c ---[1810]---> BDD-cost:  109
c ---[1809]---> BDD-cost:  128
c ---[1806]---> BDD-cost:  109
c ---[1805]---> BDD-cost:  117
c ---[1804]---> BDD-cost:  115
c ---[1803]---> BDD-cost:  128
c ---[1802]---> BDD-cost:  123
c ---[1801]---> BDD-cost:  128
c ---[1800]---> BDD-cost:  131
c ---[1799]---> BDD-cost:  128
c ---[1798]---> BDD-cost:  131
c ---[1797]---> BDD-cost:  111
c ---[1795]---> BDD-cost:  113
c ---[1794]---> BDD-cost:  120
c ---[1793]---> BDD-cost:  126
c ---[1792]---> BDD-cost:  125
c ---[1791]---> BDD-cost:  131
c ---[1790]---> BDD-cost:  111
c ---[1789]---> BDD-cost:  126
c ---[1788]---> BDD-cost:  128
c ---[1787]---> BDD-cost:  126
c ---[1786]---> BDD-cost:  128
c ---[1784]---> BDD-cost:  131
c ---[1783]---> BDD-cost:  128
c ---[1782]---> BDD-cost:  126
c ---[1781]---> BDD-cost:  128
c ---[1780]---> BDD-cost:  126
c ---[1779]---> BDD-cost:  125
c ---[1778]---> BDD-cost:  122
c ---[1777]---> BDD-cost:  120
c ---[1776]---> BDD-cost:  123
c ---[1775]---> BDD-cost:  115
c ---[1773]---> BDD-cost:  115
c ---[1772]---> BDD-cost:  123
c ---[1771]---> BDD-cost:  131
c ---[1770]---> BDD-cost:  123
c ---[1769]---> BDD-cost:  126
c ---[1768]---> BDD-cost:  131
c ---[1767]---> BDD-cost:  131
c ---[1766]---> BDD-cost:  134
c ---[1765]---> BDD-cost:  134
c ---[1764]---> BDD-cost:  123
c ---[1762]---> BDD-cost:  125
c ---[1761]---> BDD-cost:  113
c ---[1760]---> BDD-cost:  128
c ---[1759]---> BDD-cost:  123
c ---[1758]---> BDD-cost:  125
c ---[1757]---> BDD-cost:  113
c ---[1756]---> BDD-cost:  128
c ---[1755]---> BDD-cost:  131
c ---[1754]---> BDD-cost:  131
c ---[1753]---> BDD-cost:  126
c ---[1751]---> BDD-cost:  120
c ---[1750]---> BDD-cost:  131
c ---[1749]---> BDD-cost:  120
c ---[1748]---> BDD-cost:  131
c ---[1747]---> BDD-cost:  120
c ---[1746]---> BDD-cost:  109
c ---[1745]---> BDD-cost:  120
c ---[1744]---> BDD-cost:  111
c ---[1743]---> BDD-cost:  111
c ---[1742]---> BDD-cost:  121
c ---[1740]---> BDD-cost:  125
c ---[1739]---> BDD-cost:  122
c ---[1738]---> BDD-cost:  113
c ---[1737]---> BDD-cost:  123
c ---[1736]---> BDD-cost:  131
c ---[1735]---> BDD-cost:  131
c ---[1734]---> BDD-cost:  128
c ---[1733]---> BDD-cost:  113
c ---[1732]---> BDD-cost:  128
c ---[1731]---> BDD-cost:  113
c ---[1729]---> BDD-cost:  131
c ---[1728]---> BDD-cost:  122
c ---[1727]---> BDD-cost:  131
c ---[1726]---> BDD-cost:  131
c ---[1725]---> BDD-cost:  131
c ---[1724]---> BDD-cost:  111
c ---[1723]---> BDD-cost:  120
c ---[1722]---> BDD-cost:  121
c ---[1721]---> BDD-cost:  120
c ---[1720]---> BDD-cost:  131
c ---[1718]---> BDD-cost:  128
c ---[1717]---> BDD-cost:  121
c ---[1716]---> BDD-cost:  123
c ---[1715]---> BDD-cost:  134
c ---[1714]---> BDD-cost:  111
c ---[1713]---> BDD-cost:  126
c ---[1712]---> BDD-cost:  117
c ---[1711]---> BDD-cost:  115
c ---[1710]---> BDD-cost:  115
c ---[1709]---> BDD-cost:  128
c ---[1707]---> BDD-cost:  117
c ---[1706]---> BDD-cost:  118
c ---[1705]---> BDD-cost:  111
c ---[1704]---> BDD-cost:  117
c ---[1703]---> BDD-cost:  128
c ---[1702]---> BDD-cost:  129
c ---[1701]---> BDD-cost:  128
c ---[1700]---> BDD-cost:  126
c ---[1699]---> BDD-cost:  117
c ---[1698]---> BDD-cost:  111
c ---[1694]---> BDD-cost:  111
c ---[1693]---> BDD-cost:  131
c ---[1692]---> BDD-cost:  111
c ---[1691]---> BDD-cost:  122
c ---[1690]---> BDD-cost:  128
c ---[1689]---> BDD-cost:  121
c ---[1688]---> BDD-cost:  123
c ---[1687]---> BDD-cost:  131
c ---[1686]---> BDD-cost:  118
c ---[1685]---> BDD-cost:  126
c ---[1683]---> BDD-cost:  123
c ---[1682]---> BDD-cost:  131
c ---[1681]---> BDD-cost:  123
c ---[1680]---> BDD-cost:  128
c ---[1679]---> BDD-cost:  128
c ---[1678]---> BDD-cost:  121
c ---[1677]---> BDD-cost:  113
c ---[1676]---> BDD-cost:  109
c ---[1675]---> BDD-cost:  109
c ---[1674]---> BDD-cost:  125
c ---[1672]---> BDD-cost:  131
c ---[1671]---> BDD-cost:  120
c ---[1670]---> BDD-cost:  121
c ---[1669]---> BDD-cost:  125
c ---[1668]---> BDD-cost:  125
c ---[1667]---> BDD-cost:  122
c ---[1666]---> BDD-cost:  131
c ---[1665]---> BDD-cost:  111
c ---[1664]---> BDD-cost:  126
c ---[1663]---> BDD-cost:  128
c ---[1661]---> BDD-cost:  131
c ---[1660]---> BDD-cost:  128
c ---[1659]---> BDD-cost:  116
c ---[1658]---> BDD-cost:  128
c ---[1657]---> BDD-cost:  131
c ---[1656]---> BDD-cost:  128
c ---[1655]---> BDD-cost:  128
c ---[1654]---> BDD-cost:  123
c ---[1653]---> BDD-cost:  126
c ---[1652]---> BDD-cost:  128
c ---[1650]---> BDD-cost:  121
c ---[1649]---> BDD-cost:  113
c ---[1648]---> BDD-cost:  131
c ---[1647]---> BDD-cost:  125
c ---[1646]---> BDD-cost:  126
c ---[1645]---> BDD-cost:  120
c ---[1644]---> BDD-cost:  128
c ---[1643]---> BDD-cost:  115
c ---[1642]---> BDD-cost:  128
c ---[1641]---> BDD-cost:  117
c ---[1639]---> BDD-cost:  126
c ---[1638]---> BDD-cost:  128
c ---[1637]---> BDD-cost:  131
c ---[1636]---> BDD-cost:  128
c ---[1635]---> BDD-cost:  117
c ---[1634]---> BDD-cost:  115
c ---[1633]---> BDD-cost:  131
c ---[1632]---> BDD-cost:  111
c ---[1631]---> BDD-cost:  109
c ---[1630]---> BDD-cost:  123
c ---[1628]---> BDD-cost:  131
c ---[1627]---> BDD-cost:  118
c ---[1626]---> BDD-cost:  126
c ---[1625]---> BDD-cost:  118
c ---[1624]---> BDD-cost:  113
c ---[1623]---> BDD-cost:  128
c ---[1622]---> BDD-cost:  134
c ---[1621]---> BDD-cost:  123
c ---[1620]---> BDD-cost:  131
c ---[1619]---> BDD-cost:  128
c ---[1617]---> BDD-cost:  126
c ---[1616]---> BDD-cost:  113
c ---[1615]---> BDD-cost:  131
c ---[1614]---> BDD-cost:  125
c ---[1613]---> BDD-cost:  123
c ---[1612]---> BDD-cost:  125
c ---[1611]---> BDD-cost:  123
c ---[1610]---> BDD-cost:  122
c ---[1609]---> BDD-cost:  134
c ---[1608]---> BDD-cost:  134
c ---[1606]---> BDD-cost:  128
c ---[1605]---> BDD-cost:  126
c ---[1604]---> BDD-cost:  128
c ---[1603]---> BDD-cost:  131
c ---[1602]---> BDD-cost:  128
c ---[1601]---> BDD-cost:  125
c ---[1600]---> BDD-cost:  118
c ---[1599]---> BDD-cost:  124
c ---[1598]---> BDD-cost:  124
c ---[1597]---> BDD-cost:  128
c ---[1595]---> BDD-cost:  116
c ---[1594]---> BDD-cost:  123
c ---[1593]---> BDD-cost:  131
c ---[1592]---> BDD-cost:  128
c ---[1591]---> BDD-cost:  121
c ---[1590]---> BDD-cost:  113
c ---[1589]---> BDD-cost:  128
c ---[1588]---> BDD-cost:  120
c ---[1587]---> BDD-cost:  128
c ---[1586]---> BDD-cost:  115
c ---[1583]---> BDD-cost:  109
c ---[1582]---> BDD-cost:  128
c ---[1581]---> BDD-cost:  126
c ---[1580]---> BDD-cost:  128
c ---[1579]---> BDD-cost:  117
c ---[1578]---> BDD-cost:  123
c ---[1577]---> BDD-cost:  134
c ---[1576]---> BDD-cost:  128
c ---[1575]---> BDD-cost:  131
c ---[1574]---> BDD-cost:  118
c ---[1572]---> BDD-cost:  109
c ---[1571]---> BDD-cost:  128
c ---[1570]---> BDD-cost:  131
c ---[1569]---> BDD-cost:  123
c ---[1568]---> BDD-cost:  126
c ---[1567]---> BDD-cost:  113
c ---[1566]---> BDD-cost:  113
c ---[1565]---> BDD-cost:  120
c ---[1564]---> BDD-cost:  131
c ---[1563]---> BDD-cost:  111
c ---[1561]---> BDD-cost:  126
c ---[1560]---> BDD-cost:  128
c ---[1559]---> BDD-cost:  126
c ---[1558]---> BDD-cost:  123
c ---[1557]---> BDD-cost:  131
c ---[1556]---> BDD-cost:  128
c ---[1555]---> BDD-cost:  109
c ---[1554]---> BDD-cost:  118
c ---[1553]---> BDD-cost:  131
c ---[1552]---> BDD-cost:  123
c ---[1550]---> BDD-cost:  125
c ---[1549]---> BDD-cost:  113
c ---[1548]---> BDD-cost:  126
c ---[1547]---> BDD-cost:  117
c ---[1546]---> BDD-cost:  131
c ---[1545]---> BDD-cost:  111
c ---[1544]---> BDD-cost:  113
c ---[1543]---> BDD-cost:  128
c ---[1542]---> BDD-cost:  118
c ---[1541]---> BDD-cost:  123
c ---[1539]---> BDD-cost:  122
c ---[1538]---> BDD-cost:  123
c ---[1537]---> BDD-cost:  131
c ---[1536]---> BDD-cost:  113
c ---[1535]---> BDD-cost:  113
c ---[1534]---> BDD-cost:  111
c ---[1533]---> BDD-cost:  131
c ---[1532]---> BDD-cost:  128
c ---[1531]---> BDD-cost:  129
c ---[1530]---> BDD-cost:  123
c ---[1528]---> BDD-cost:  131
c ---[1527]---> BDD-cost:  128
c ---[1526]---> BDD-cost:  126
c ---[1525]---> BDD-cost:  128
c ---[1524]---> BDD-cost:  123
c ---[1523]---> BDD-cost:  128
c ---[1522]---> BDD-cost:  134
c ---[1521]---> BDD-cost:  122
c ---[1520]---> BDD-cost:  109
c ---[1519]---> BDD-cost:  117
c ---[1517]---> BDD-cost:  131
c ---[1516]---> BDD-cost:  111
c ---[1515]---> BDD-cost:  126
c ---[1514]---> BDD-cost:  128
c ---[1513]---> BDD-cost:  131
c ---[1512]---> BDD-cost:  123
c ---[1511]---> BDD-cost:  120
c ---[1510]---> BDD-cost:  118
c ---[1509]---> BDD-cost:  126
c ---[1508]---> BDD-cost:  123
c ---[1506]---> BDD-cost:  131
c ---[1505]---> BDD-cost:  115
c ---[1504]---> BDD-cost:  121
c ---[1503]---> BDD-cost:  122
c ---[1502]---> BDD-cost:  131
c ---[1501]---> BDD-cost:  111
c ---[1500]---> BDD-cost:  126
c ---[1499]---> BDD-cost:  128
c ---[1498]---> BDD-cost:  131
c ---[1497]---> BDD-cost:  128
c ---[1495]---> BDD-cost:  128
c ---[1494]---> BDD-cost:  128
c ---[1493]---> BDD-cost:  126
c ---[1492]---> BDD-cost:  125
c ---[1491]---> BDD-cost:  131
c ---[1490]---> BDD-cost:  115
c ---[1489]---> BDD-cost:  126
c ---[1488]---> BDD-cost:  111
c ---[1487]---> BDD-cost:  121
c ---[1486]---> BDD-cost:  123
c ---[1484]---> BDD-cost:  120
c ---[1483]---> BDD-cost:  118
c ---[1482]---> BDD-cost:  131
c ---[1481]---> BDD-cost:  120
c ---[1480]---> BDD-cost:  109
c ---[1479]---> BDD-cost:  125
c ---[1478]---> BDD-cost:  131
c ---[1477]---> BDD-cost:  128
c ---[1476]---> BDD-cost:  123
c ---[1475]---> BDD-cost:  125
c ---[1472]---> BDD-cost:  131
c ---[1471]---> BDD-cost:  120
c ---[1470]---> BDD-cost:  123
c ---[1469]---> BDD-cost:  128
c ---[1468]---> BDD-cost:  123
c ---[1467]---> BDD-cost:  128
c ---[1466]---> BDD-cost:  125
c ---[1465]---> BDD-cost:  113
c ---[1464]---> BDD-cost:  111
c ---[1463]---> BDD-cost:  128
c ---[1461]---> BDD-cost:  121
c ---[1460]---> BDD-cost:  123
c ---[1459]---> BDD-cost:  131
c ---[1458]---> BDD-cost:  122
c ---[1457]---> BDD-cost:  123
c ---[1456]---> BDD-cost:  117
c ---[1455]---> BDD-cost:  131
c ---[1454]---> BDD-cost:  111
c ---[1453]---> BDD-cost:  116
c ---[1452]---> BDD-cost:  128
c ---[1450]---> BDD-cost:  131
c ---[1449]---> BDD-cost:  113
c ---[1448]---> BDD-cost:  123
c ---[1447]---> BDD-cost:  120
c ---[1446]---> BDD-cost:  128
c ---[1445]---> BDD-cost:  125
c ---[1444]---> BDD-cost:  111
c ---[1443]---> BDD-cost:  123
c ---[1442]---> BDD-cost:  123
c ---[1441]---> BDD-cost:  128
c ---[1439]---> BDD-cost:  131
c ---[1438]---> BDD-cost:  125
c ---[1437]---> BDD-cost:  126
c ---[1436]---> BDD-cost:  120
c ---[1435]---> BDD-cost:  131
c ---[1434]---> BDD-cost:  128
c ---[1433]---> BDD-cost:  117
c ---[1432]---> BDD-cost:  122
c ---[1431]---> BDD-cost:  117
c ---[1430]---> BDD-cost:  117
c ---[1428]---> BDD-cost:  131
c ---[1427]---> BDD-cost:  128
c ---[1426]---> BDD-cost:  129
c ---[1425]---> BDD-cost:  123
c ---[1424]---> BDD-cost:  131
c ---[1423]---> BDD-cost:  115
c ---[1422]---> BDD-cost:  131
c ---[1421]---> BDD-cost:  122
c ---[1420]---> BDD-cost:  131
c ---[1419]---> BDD-cost:  111
c ---[1417]---> BDD-cost:  126
c ---[1416]---> BDD-cost:  120
c ---[1415]---> BDD-cost:  109
c ---[1414]---> BDD-cost:  125
c ---[1413]---> BDD-cost:  129
c ---[1412]---> BDD-cost:  125
c ---[1411]---> BDD-cost:  134
c ---[1410]---> BDD-cost:  120
c ---[1409]---> BDD-cost:  131
c ---[1408]---> BDD-cost:  117
c ---[1406]---> BDD-cost:  128
c ---[1405]---> BDD-cost:  125
c ---[1404]---> BDD-cost:  128
c ---[1403]---> BDD-cost:  120
c ---[1402]---> BDD-cost:  121
c ---[1401]---> BDD-cost:  117
c ---[1400]---> BDD-cost:  126
c ---[1399]---> BDD-cost:  111
c ---[1398]---> BDD-cost:  131
c ---[1397]---> BDD-cost:  118
c ---[1395]---> BDD-cost:  128
c ---[1394]---> BDD-cost:  128
c ---[1393]---> BDD-cost:  128
c ---[1392]---> BDD-cost:  120
c ---[1391]---> BDD-cost:  125
c ---[1390]---> BDD-cost:  111
c ---[1389]---> BDD-cost:  126
c ---[1388]---> BDD-cost:  118
c ---[1387]---> BDD-cost:  123
c ---[1386]---> BDD-cost:  128
c ---[1384]---> BDD-cost:  131
c ---[1383]---> BDD-cost:  128
c ---[1382]---> BDD-cost:  120
c ---[1381]---> BDD-cost:  117
c ---[1380]---> BDD-cost:  118
c ---[1379]---> BDD-cost:  120
c ---[1378]---> BDD-cost:  121
c ---[1377]---> BDD-cost:  113
c ---[1376]---> BDD-cost:  131
c ---[1375]---> BDD-cost:  113
c ---[1373]---> BDD-cost:  109
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:  108
c ---[ 994]---> BDD-cost:  110
c ---[ 993]---> BDD-cost:   79
c ---[ 992]---> BDD-cost:   79
c ---[ 991]---> BDD-cost:   79
c ---[ 990]---> BDD-cost:   79
c ---[ 989]---> BDD-cost:  116
c ---[ 988]---> BDD-cost:  110
c ---[ 987]---> BDD-cost:   79
c ---[ 986]---> BDD-cost:   79
c ---[ 985]---> BDD-cost:   79
c ---[ 983]---> BDD-cost:   79
c ---[ 982]---> BDD-cost:  116
c ---[ 981]---> BDD-cost:  110
c ---[ 980]---> BDD-cost:   79
c ---[ 979]---> BDD-cost:   79
c ---[ 978]---> BDD-cost:   79
c ---[ 977]---> BDD-cost:   79
c ---[ 976]---> BDD-cost:  108
c ---[ 975]---> BDD-cost:  110
c ---[ 974]---> BDD-cost:   79
c ---[ 972]---> BDD-cost:   79
c ---[ 971]---> BDD-cost:   79
c ---[ 970]---> BDD-cost:   79
c ---[ 969]---> BDD-cost:  116
c ---[ 968]---> BDD-cost:  110
c ---[ 967]---> BDD-cost:   79
c ---[ 966]---> BDD-cost:   79
c ---[ 965]---> BDD-cost:   79
c ---[ 964]---> BDD-cost:   79
c ---[ 963]---> BDD-cost:  108
c ---[ 960]---> BDD-cost:  110
c ---[ 959]---> BDD-cost:   79
c ---[ 958]---> BDD-cost:   79
c ---[ 957]---> BDD-cost:   79
c ---[ 956]---> BDD-cost:   79
c ---[ 955]---> BDD-cost:  112
c ---[ 954]---> BDD-cost:  110
c ---[ 953]---> BDD-cost:   79
c ---[ 952]---> BDD-cost:   79
c ---[ 951]---> BDD-cost:   79
c ---[ 949]---> BDD-cost:   79
c ---[ 948]---> BDD-cost:  114
c ---[ 947]---> BDD-cost:  110
c ---[ 946]---> BDD-cost:   79
c ---[ 945]---> BDD-cost:   79
c ---[ 944]---> BDD-cost:   79
c ---[ 943]---> BDD-cost:   79
c ---[ 942]---> BDD-cost:  108
c ---[ 941]---> BDD-cost:  110
c ---[ 940]---> BDD-cost:   79
c ---[ 938]---> BDD-cost:   79
c ---[ 937]---> BDD-cost:   79
c ---[ 936]---> BDD-cost:   79
c ---[ 935]---> BDD-cost:  116
c ---[ 934]---> BDD-cost:  110
c ---[ 933]---> BDD-cost:   79
c ---[ 932]---> BDD-cost:   79
c ---[ 931]---> BDD-cost:   79
c ---[ 930]---> BDD-cost:   79
c ---[ 929]---> BDD-cost:  116
c ---[ 927]---> BDD-cost:  110
c ---[ 926]---> BDD-cost:   79
c ---[ 925]---> BDD-cost:   79
c ---[ 924]---> BDD-cost:   79
c ---[ 923]---> BDD-cost:   79
c ---[ 922]---> BDD-cost:  116
c ---[ 921]---> BDD-cost:  110
c ---[ 920]---> BDD-cost:   79
c ---[ 919]---> BDD-cost:   79
c ---[ 918]---> BDD-cost:   79
c ---[ 916]---> BDD-cost:   79
c ---[ 915]---> BDD-cost:  108
c ---[ 914]---> BDD-cost:  110
c ---[ 913]---> BDD-cost:   79
c ---[ 912]---> BDD-cost:   79
c ---[ 911]---> BDD-cost:   79
c ---[ 910]---> BDD-cost:   79
c ---[ 909]---> BDD-cost:  116
c ---[ 908]---> BDD-cost:  110
c ---[ 907]---> BDD-cost:   79
c ---[ 905]---> BDD-cost:   79
c ---[ 904]---> BDD-cost:   79
c ---[ 903]---> BDD-cost:   79
c ---[ 902]---> BDD-cost:  116
c ---[ 901]---> BDD-cost:  110
c ---[ 900]---> BDD-cost:   79
c ---[ 899]---> BDD-cost:   79
c ---[ 898]---> BDD-cost:   79
c ---[ 897]---> BDD-cost:   79
c ---[ 896]---> BDD-cost:  116
c ---[ 894]---> BDD-cost:  110
c ---[ 893]---> BDD-cost:   79
c ---[ 892]---> BDD-cost:   79
c ---[ 891]---> BDD-cost:   79
c ---[ 890]---> BDD-cost:   79
c ---[ 889]---> BDD-cost:  116
c ---[ 888]---> BDD-cost:  110
c ---[ 887]---> BDD-cost:   79
c ---[ 886]---> BDD-cost:   79
c ---[ 885]---> BDD-cost:   79
c ---[ 883]---> BDD-cost:   79
c ---[ 882]---> BDD-cost:  114
c ---[ 881]---> BDD-cost:  110
c ---[ 880]---> BDD-cost:   79
c ---[ 879]---> BDD-cost:   79
c ---[ 878]---> BDD-cost:   79
c ---[ 877]---> BDD-cost:   79
c ---[ 876]---> BDD-cost:  108
c ---[ 875]---> BDD-cost:  110
c ---[ 874]---> BDD-cost:   79
c ---[ 872]---> BDD-cost:   79
c ---[ 871]---> BDD-cost:   79
c ---[ 870]---> BDD-cost:   79
c ---[ 869]---> BDD-cost:  108
c ---[ 868]---> BDD-cost:  110
c ---[ 867]---> BDD-cost:   79
c ---[ 866]---> BDD-cost:   79
c ---[ 865]---> BDD-cost:   79
c ---[ 864]---> BDD-cost:   79
c ---[ 863]---> BDD-cost:  112
c ---[ 861]---> BDD-cost:  110
c ---[ 860]---> BDD-cost:   79
c ---[ 859]---> BDD-cost:   79
c ---[ 858]---> BDD-cost:   79
c ---[ 857]---> BDD-cost:   79
c ---[ 856]---> BDD-cost:  108
c ---[ 855]---> BDD-cost:  110
c ---[ 854]---> BDD-cost:   79
c ---[ 853]---> BDD-cost:   79
c ---[ 852]---> BDD-cost:   79
c ---[ 849]---> BDD-cost:   79
c ---[ 848]---> BDD-cost:  108
c ---[ 847]---> BDD-cost:  110
c ---[ 846]---> BDD-cost:   79
c ---[ 845]---> BDD-cost:   79
c ---[ 844]---> BDD-cost:   79
c ---[ 843]---> BDD-cost:   79
c ---[ 842]---> BDD-cost:  108
c ---[ 841]---> BDD-cost:  110
c ---[ 840]---> BDD-cost:   79
c ---[ 838]---> BDD-cost:   79
c ---[ 837]---> BDD-cost:   79
c ---[ 836]---> BDD-cost:   79
c ---[ 835]---> BDD-cost:  116
c ---[ 834]---> BDD-cost:  110
c ---[ 833]---> BDD-cost:   79
c ---[ 832]---> BDD-cost:   79
c ---[ 831]---> BDD-cost:   79
c ---[ 830]---> BDD-cost:   79
c ---[ 829]---> BDD-cost:  116
c ---[ 827]---> BDD-cost:  110
c ---[ 826]---> BDD-cost:   79
c ---[ 825]---> BDD-cost:   79
c ---[ 824]---> BDD-cost:   79
c ---[ 823]---> BDD-cost:   79
c ---[ 822]---> BDD-cost:  116
c ---[ 821]---> BDD-cost:  110
c ---[ 820]---> BDD-cost:   79
c ---[ 819]---> BDD-cost:   79
c ---[ 818]---> BDD-cost:   79
c ---[ 816]---> BDD-cost:   79
c ---[ 815]---> BDD-cost:  116
c ---[ 814]---> BDD-cost:  110
c ---[ 813]---> BDD-cost:   79
c ---[ 812]---> BDD-cost:   79
c ---[ 811]---> BDD-cost:   79
c ---[ 810]---> BDD-cost:   79
c ---[ 809]---> BDD-cost:  116
c ---[ 808]---> BDD-cost:  110
c ---[ 807]---> BDD-cost:   79
c ---[ 805]---> BDD-cost:   79
c ---[ 804]---> BDD-cost:   79
c ---[ 803]---> BDD-cost:   79
c ---[ 802]---> BDD-cost:  116
c ---[ 801]---> BDD-cost:  110
c ---[ 800]---> BDD-cost:   79
c ---[ 799]---> BDD-cost:   79
c ---[ 798]---> BDD-cost:   79
c ---[ 797]---> BDD-cost:   79
c ---[ 796]---> BDD-cost:  116
c ---[ 794]---> BDD-cost:  110
c ---[ 793]---> BDD-cost:   79
c ---[ 792]---> BDD-cost:   79
c ---[ 791]---> BDD-cost:   79
c ---[ 790]---> BDD-cost:   79
c ---[ 789]---> BDD-cost:  114
c ---[ 788]---> BDD-cost:  110
c ---[ 787]---> BDD-cost:   79
c ---[ 786]---> BDD-cost:   79
c ---[ 785]---> BDD-cost:   79
c ---[ 783]---> BDD-cost:   79
c ---[ 782]---> BDD-cost:  108
c ---[ 781]---> BDD-cost:  110
c ---[ 780]---> BDD-cost:   79
c ---[ 779]---> BDD-cost:   79
c ---[ 778]---> BDD-cost:   79
c ---[ 777]---> BDD-cost:   79
c ---[ 776]---> BDD-cost:  108
c ---[ 775]---> BDD-cost:  110
c ---[ 774]---> BDD-cost:   79
c ---[ 772]---> BDD-cost:   79
c ---[ 771]---> BDD-cost:   79
c ---[ 770]---> BDD-cost:   79
c ---[ 769]---> BDD-cost:  108
c ---[ 768]---> BDD-cost:  110
c ---[ 767]---> BDD-cost:   79
c ---[ 766]---> BDD-cost:   79
c ---[ 765]---> BDD-cost:   79
c ---[ 764]---> BDD-cost:   79
c ---[ 763]---> BDD-cost:  116
c ---[ 761]---> BDD-cost:  110
c ---[ 760]---> BDD-cost:   79
c ---[ 759]---> BDD-cost:   79
c ---[ 758]---> BDD-cost:   79
c ---[ 757]---> BDD-cost:   79
c ---[ 756]---> BDD-cost:  108
c ---[ 755]---> BDD-cost:  110
c ---[ 754]---> BDD-cost:   79
c ---[ 753]---> BDD-cost:   79
c ---[ 752]---> BDD-cost:   79
c ---[ 750]---> BDD-cost:   79
c ---[ 749]---> BDD-cost:  108
c ---[ 748]---> BDD-cost:  110
c ---[ 747]---> BDD-cost:   79
c ---[ 746]---> BDD-cost:   79
c ---[ 745]---> BDD-cost:   79
c ---[ 744]---> BDD-cost:   79
c ---[ 743]---> BDD-cost:  108
c ---[ 742]---> BDD-cost:  110
c ---[ 741]---> BDD-cost:   79
c ---[ 738]---> BDD-cost:   79
c ---[ 737]---> BDD-cost:   79
c ---[ 736]---> BDD-cost:   79
c ---[ 735]---> BDD-cost:  116
c ---[ 734]---> BDD-cost:  110
c ---[ 733]---> BDD-cost:   79
c ---[ 732]---> BDD-cost:   79
c ---[ 731]---> BDD-cost:   79
c ---[ 730]---> BDD-cost:   79
c ---[ 729]---> BDD-cost:  108
c ---[ 727]---> BDD-cost:  110
c ---[ 726]---> BDD-cost:   79
c ---[ 725]---> BDD-cost:   79
c ---[ 724]---> BDD-cost:   79
c ---[ 723]---> BDD-cost:   79
c ---[ 722]---> BDD-cost:  116
c ---[ 721]---> BDD-cost:  110
c ---[ 720]---> BDD-cost:   79
c ---[ 719]---> BDD-cost:   79
c ---[ 718]---> BDD-cost:   79
c ---[ 716]---> BDD-cost:   79
c ---[ 715]---> BDD-cost:  116
c ---[ 714]---> BDD-cost:  110
c ---[ 713]---> BDD-cost:   79
c ---[ 712]---> BDD-cost:   79
c ---[ 711]---> BDD-cost:   79
c ---[ 710]---> BDD-cost:   79
c ---[ 709]---> BDD-cost:  108
c ---[ 708]---> BDD-cost:  110
c ---[ 707]---> BDD-cost:   79
c ---[ 705]---> BDD-cost:   79
c ---[ 704]---> BDD-cost:   79
c ---[ 703]---> BDD-cost:   79
c ---[ 702]---> BDD-cost:  108
c ---[ 701]---> BDD-cost:  110
c ---[ 700]---> BDD-cost:   79
c ---[ 699]---> BDD-cost:   79
c ---[ 698]---> BDD-cost:   79
c ---[ 697]---> BDD-cost:   79
c ---[ 696]---> BDD-cost:  108
c ---[ 694]---> BDD-cost:  110
c ---[ 693]---> BDD-cost:   79
c ---[ 692]---> BDD-cost:   79
c ---[ 691]---> BDD-cost:   79
c ---[ 690]---> BDD-cost:   79
c ---[ 689]---> BDD-cost:  108
c ---[ 688]---> BDD-cost:  110
c ---[ 687]---> BDD-cost:   79
c ---[ 686]---> BDD-cost:   79
c ---[ 685]---> BDD-cost:   79
c ---[ 683]---> BDD-cost:   79
c ---[ 682]---> BDD-cost:  108
c ---[ 681]---> BDD-cost:  110
c ---[ 680]---> BDD-cost:   79
c ---[ 679]---> BDD-cost:   79
c ---[ 678]---> BDD-cost:   79
c ---[ 677]---> BDD-cost:   79
c ---[ 676]---> BDD-cost:  116
c ---[ 675]---> BDD-cost:  110
c ---[ 674]---> BDD-cost:   79
c ---[ 672]---> BDD-cost:   79
c ---[ 671]---> BDD-cost:   79
c ---[ 670]---> BDD-cost:   79
c ---[ 669]---> BDD-cost:  116
c ---[ 668]---> BDD-cost:  110
c ---[ 667]---> BDD-cost:   79
c ---[ 666]---> BDD-cost:   79
c ---[ 665]---> BDD-cost:   79
c ---[ 664]---> BDD-cost:   79
c ---[ 663]---> BDD-cost:  114
c ---[ 661]---> BDD-cost:  110
c ---[ 660]---> BDD-cost:   79
c ---[ 659]---> BDD-cost:   79
c ---[ 658]---> BDD-cost:   79
c ---[ 657]---> BDD-cost:   79
c ---[ 656]---> BDD-cost:  116
c ---[ 655]---> BDD-cost:  110
c ---[ 654]---> BDD-cost:   79
c ---[ 653]---> BDD-cost:   79
c ---[ 652]---> BDD-cost:   79
c ---[ 650]---> BDD-cost:   79
c ---[ 649]---> BDD-cost:  116
c ---[ 648]---> BDD-cost:  110
c ---[ 647]---> BDD-cost:   79
c ---[ 646]---> BDD-cost:   79
c ---[ 645]---> BDD-cost:   79
c ---[ 644]---> BDD-cost:   79
c ---[ 643]---> BDD-cost:  116
c ---[ 642]---> BDD-cost:  110
c ---[ 641]---> BDD-cost:   79
c ---[ 639]---> BDD-cost:   79
c ---[ 638]---> BDD-cost:   79
c ---[ 637]---> BDD-cost:   79
c ---[ 636]---> BDD-cost:  108
c ---[ 635]---> BDD-cost:  110
c ---[ 634]---> BDD-cost:   79
c ---[ 633]---> BDD-cost:   79
c ---[ 632]---> BDD-cost:   79
c ---[ 631]---> BDD-cost:   79
c ---[ 630]---> BDD-cost:  108
c ---[ 629]---> BDD-cost:   23
c ---[ 628]---> BDD-cost:   23
c ---[ 627]---> BDD-cost:   23
c ---[ 626]---> BDD-cost:   23
c ---[ 625]---> BDD-cost:   23
c ---[ 624]---> BDD-cost:   23
c ---[ 623]---> BDD-cost:   23
c ---[ 622]---> BDD-cost:   23
c ---[ 621]---> BDD-cost:   23
c ---[ 620]---> BDD-cost:   23
c ---[ 619]---> BDD-cost:   23
c ---[ 618]---> BDD-cost:   23
c ---[ 617]---> BDD-cost:   23
c ---[ 616]---> BDD-cost:   23
c ---[ 615]---> BDD-cost:   23
c ---[ 614]---> BDD-cost:   23
c ---[ 613]---> BDD-cost:   23
c ---[ 612]---> BDD-cost:   23
c ---[ 611]---> BDD-cost:   23
c ---[ 610]---> BDD-cost:   23
c ---[ 609]---> BDD-cost:   23
c ---[ 608]---> BDD-cost:   23
c ---[ 607]---> BDD-cost:   23
c ---[ 606]---> BDD-cost:   23
c ---[ 605]---> BDD-cost:   23
c ---[ 604]---> BDD-cost:   23
c ---[ 603]---> BDD-cost:   23
c ---[ 602]---> BDD-cost:   23
c ---[ 601]---> BDD-cost:   23
c ---[ 600]---> BDD-cost:   23
c ---[ 599]---> BDD-cost:   23
c ---[ 598]---> BDD-cost:   23
c ---[ 597]---> BDD-cost:   23
c ---[ 596]---> BDD-cost:   23
c ---[ 595]---> BDD-cost:   23
c ---[ 594]---> BDD-cost:   23
c ---[ 593]---> BDD-cost:   23
c ---[ 592]---> BDD-cost:   23
c ---[ 591]---> BDD-cost:   23
c ---[ 590]---> BDD-cost:   23
c ---[ 589]---> BDD-cost:   23
c ---[ 588]---> BDD-cost:   23
c ---[ 587]---> BDD-cost:   23
c ---[ 586]---> BDD-cost:   23
c ---[ 585]---> BDD-cost:   23
c ---[ 584]---> BDD-cost:   23
c ---[ 583]---> BDD-cost:   23
c ---[ 582]---> BDD-cost:   23
c ---[ 581]---> BDD-cost:   23
c ---[ 580]---> BDD-cost:   23
c ---[ 579]---> BDD-cost:   23
c ---[ 578]---> BDD-cost:   23
c ---[ 577]---> BDD-cost:   23
c ---[ 576]---> BDD-cost:   23
c ---[ 575]---> BDD-cost:   23
c ---[ 574]---> BDD-cost:   23
c ---[ 573]---> BDD-cost:   23
c ---[ 572]---> BDD-cost:   23
c ---[ 571]---> BDD-cost:   23
c ---[ 570]---> BDD-cost:   23
c ---[ 569]---> BDD-cost:   23
c ---[ 568]---> BDD-cost:   23
c ---[ 567]---> BDD-cost:   23
c ---[ 566]---> BDD-cost:   23
c ---[ 565]---> BDD-cost:   23
c ---[ 564]---> BDD-cost:   23
c ---[ 563]---> BDD-cost:   23
c ---[ 562]---> BDD-cost:   23
c ---[ 561]---> BDD-cost:   23
c ---[ 560]---> BDD-cost:   23
c ---[ 559]---> BDD-cost:   23
c ---[ 558]---> BDD-cost:   23
c ---[ 557]---> BDD-cost:   23
c ---[ 556]---> BDD-cost:   23
c ---[ 555]---> BDD-cost:   23
c ---[ 554]---> BDD-cost:   23
c ---[ 553]---> BDD-cost:   23
c ---[ 552]---> BDD-cost:   23
c ---[ 551]---> BDD-cost:   23
c ---[ 550]---> BDD-cost:   23
c ---[ 549]---> BDD-cost:   23
c ---[ 548]---> BDD-cost:   23
c ---[ 547]---> BDD-cost:   23
c ---[ 546]---> BDD-cost:   23
c ---[ 545]---> BDD-cost:   23
c ---[ 544]---> BDD-cost:   23
c ---[ 543]---> BDD-cost:   23
c ---[ 542]---> BDD-cost:   23
c ---[ 541]---> BDD-cost:   23
c ---[ 540]---> BDD-cost:   23
c ---[ 539]---> BDD-cost:   23
c ---[ 538]---> BDD-cost:   23
c ---[ 537]---> BDD-cost:   23
c ---[ 536]---> BDD-cost:   23
c ---[ 535]---> BDD-cost:   23
c ---[ 534]---> BDD-cost:   23
c ---[ 533]---> BDD-cost:   23
c ---[ 532]---> BDD-cost:   23
c ---[ 531]---> BDD-cost:   23
c ---[ 530]---> BDD-cost:   23
c ---[ 529]---> BDD-cost:   23
c ---[ 528]---> BDD-cost:   23
c ---[ 527]---> BDD-cost:   23
c ---[ 526]---> BDD-cost:   23
c ---[ 525]---> BDD-cost:   23
c ---[ 524]---> BDD-cost:   23
c ---[ 523]---> BDD-cost:   23
c ---[ 522]---> BDD-cost:   23
c ---[ 521]---> BDD-cost:   23
c ---[ 520]---> BDD-cost:   23
c ---[ 519]---> BDD-cost:   23
c ---[ 518]---> BDD-cost:   23
c ---[ 517]---> BDD-cost:   23
c ---[ 516]---> BDD-cost:   23
c ---[ 515]---> BDD-cost:   23
c ---[ 514]---> BDD-cost:   23
c ---[ 513]---> BDD-cost:   23
c ---[ 512]---> BDD-cost:   23
c ---[ 511]---> BDD-cost:   23
c ---[ 510]---> BDD-cost:   23
c ---[ 509]---> BDD-cost:   23
c ---[ 508]---> BDD-cost:   23
c ---[ 507]---> BDD-cost:   23
c ---[ 506]---> BDD-cost:   23
c ---[ 505]---> BDD-cost:   23
c ---[ 504]---> BDD-cost:   23
c ---[ 503]---> BDD-cost:   23
c ---[ 502]---> BDD-cost:   23
c ---[ 501]---> BDD-cost:   23
c ---[ 500]---> BDD-cost:   23
c ---[ 499]---> BDD-cost:   23
c ---[ 498]---> BDD-cost:   23
c ---[ 497]---> BDD-cost:   23
c ---[ 496]---> BDD-cost:   23
c ---[ 495]---> BDD-cost:   23
c ---[ 494]---> BDD-cost:   23
c ---[ 493]---> BDD-cost:   23
c ---[ 492]---> BDD-cost:   23
c ---[ 491]---> BDD-cost:   23
c ---[ 490]---> BDD-cost:   23
c ---[ 489]---> BDD-cost:   23
c ---[ 488]---> BDD-cost:   23
c ---[ 487]---> BDD-cost:   23
c ---[ 486]---> BDD-cost:   23
c ---[ 485]---> BDD-cost:   23
c ---[ 484]---> BDD-cost:   23
c ---[ 483]---> BDD-cost:   23
c ---[ 482]---> BDD-cost:   23
c ---[ 481]---> BDD-cost:   23
c ---[ 480]---> BDD-cost:   23
c ---[ 479]---> BDD-cost:   23
c ---[ 478]---> BDD-cost:   23
c ---[ 477]---> BDD-cost:   23
c ---[ 476]---> BDD-cost:   23
c ---[ 475]---> BDD-cost:   23
c ---[ 474]---> BDD-cost:   23
c ---[ 473]---> BDD-cost:   23
c ---[ 472]---> BDD-cost:   23
c ---[ 471]---> BDD-cost:   23
c ---[ 470]---> BDD-cost:   23
c ---[ 469]---> BDD-cost:   23
c ---[ 468]---> BDD-cost:   23
c ---[ 467]---> BDD-cost:   23
c ---[ 466]---> BDD-cost:   23
c ---[ 465]---> BDD-cost:   23
c ---[ 464]---> BDD-cost:   23
c ---[ 463]---> BDD-cost:   23
c ---[ 462]---> BDD-cost:   23
c ---[ 461]---> BDD-cost:   23
c ---[ 460]---> BDD-cost:   23
c ---[ 459]---> BDD-cost:   23
c ---[ 458]---> BDD-cost:   23
c ---[ 457]---> BDD-cost:   23
c ---[ 456]---> BDD-cost:   23
c ---[ 455]---> BDD-cost:   23
c ---[ 454]---> BDD-cost:   23
c ---[ 453]---> BDD-cost:   23
c ---[ 452]---> BDD-cost:   23
c ---[ 451]---> BDD-cost:   23
c ---[ 450]---> BDD-cost:   23
c ---[ 449]---> BDD-cost:   23
c ---[ 448]---> BDD-cost:   23
c ---[ 447]---> BDD-cost:   23
c ---[ 446]---> BDD-cost:   23
c ---[ 445]---> BDD-cost:   23
c ---[ 444]---> BDD-cost:   23
c ---[ 443]---> BDD-cost:   23
c ---[ 442]---> BDD-cost:   23
c ---[ 441]---> BDD-cost:   23
c ---[ 440]---> BDD-cost:   23
c ---[ 439]---> BDD-cost:   23
c ---[ 438]---> BDD-cost:   23
c ---[ 437]---> BDD-cost:   23
c ---[ 436]---> BDD-cost:   23
c ---[ 435]---> BDD-cost:   23
c ---[ 434]---> BDD-cost:   23
c ---[ 433]---> BDD-cost:   23
c ---[ 432]---> BDD-cost:   23
c ---[ 431]---> BDD-cost:   23
c ---[ 430]---> BDD-cost:   23
c ---[ 429]---> BDD-cost:   23
c ---[ 428]---> BDD-cost:   23
c ---[ 427]---> BDD-cost:   23
c ---[ 426]---> BDD-cost:   23
c ---[ 425]---> BDD-cost:   23
c ---[ 424]---> BDD-cost:   23
c ---[ 423]---> BDD-cost:   23
c ---[ 422]---> BDD-cost:   23
c ---[ 421]---> BDD-cost:   23
c ---[ 420]---> BDD-cost:   23
c ---[ 419]---> BDD-cost:   23
c ---[ 418]---> BDD-cost:   23
c ---[ 417]---> BDD-cost:   23
c ---[ 416]---> BDD-cost:   23
c ---[ 415]---> BDD-cost:   23
c ---[ 414]---> BDD-cost:   23
c ---[ 413]---> BDD-cost:   23
c ---[ 412]---> BDD-cost:   23
c ---[ 411]---> BDD-cost:   23
c ---[ 410]---> BDD-cost:   23
c ---[ 409]---> BDD-cost:   23
c ---[ 408]---> BDD-cost:   23
c ---[ 407]---> BDD-cost:   23
c ---[ 406]---> BDD-cost:   23
c ---[ 405]---> BDD-cost:   23
c ---[ 404]---> BDD-cost:   23
c ---[ 403]---> BDD-cost:   23
c ---[ 402]---> BDD-cost:   23
c ---[ 401]---> BDD-cost:   23
c ---[ 400]---> BDD-cost:   23
c ---[ 399]---> BDD-cost:   23
c ---[ 398]---> BDD-cost:   23
c ---[ 397]---> BDD-cost:   23
c ---[ 396]---> BDD-cost:   23
c ---[ 395]---> BDD-cost:   23
c ---[ 394]---> BDD-cost:   23
c ---[ 393]---> BDD-cost:   23
c ---[ 392]---> BDD-cost:   23
c ---[ 391]---> BDD-cost:   23
c ---[ 390]---> BDD-cost:   23
c ---[ 389]---> BDD-cost:   23
c ---[ 388]---> BDD-cost:   23
c ---[ 387]---> BDD-cost:   23
c ---[ 386]---> BDD-cost:   23
c ---[ 385]---> BDD-cost:   23
c ---[ 384]---> BDD-cost:   23
c ---[ 383]---> BDD-cost:   23
c ---[ 382]---> BDD-cost:   23
c ---[ 381]---> BDD-cost:   23
c ---[ 380]---> BDD-cost:   23
c ---[ 379]---> BDD-cost:   23
c ---[ 378]---> BDD-cost:   23
c ---[ 377]---> BDD-cost:   23
c ---[ 376]---> BDD-cost:   23
c ---[ 375]---> BDD-cost:   23
c ---[ 374]---> BDD-cost:   23
c ---[ 373]---> BDD-cost:   23
c ---[ 372]---> BDD-cost:   23
c ---[ 371]---> BDD-cost:   23
c ---[ 370]---> BDD-cost:   23
c ---[ 369]---> BDD-cost:   23
c ---[ 368]---> BDD-cost:   23
c ---[ 367]---> BDD-cost:   23
c ---[ 366]---> BDD-cost:   23
c ---[ 365]---> BDD-cost:   23
c ---[ 364]---> BDD-cost:   23
c ---[ 363]---> BDD-cost:   23
c ---[ 362]---> BDD-cost:   23
c ---[ 361]---> BDD-cost:   23
c ---[ 360]---> BDD-cost:   23
c ---[ 359]---> BDD-cost:   23
c ---[ 358]---> BDD-cost:   23
c ---[ 357]---> BDD-cost:   23
c ---[ 356]---> BDD-cost:   23
c ---[ 355]---> BDD-cost:   23
c ---[ 354]---> BDD-cost:   23
c ---[ 353]---> BDD-cost:   23
c ---[ 352]---> BDD-cost:   23
c ---[ 351]---> BDD-cost:   23
c ---[ 350]---> BDD-cost:   23
c ---[ 349]---> BDD-cost:   23
c ---[ 348]---> BDD-cost:   23
c ---[ 347]---> BDD-cost:   23
c ---[ 346]---> BDD-cost:   23
c ---[ 345]---> BDD-cost:   23
c ---[ 344]---> BDD-cost:   23
c ---[ 343]---> BDD-cost:   23
c ---[ 342]---> BDD-cost:   23
c ---[ 341]---> BDD-cost:   23
c ---[ 340]---> BDD-cost:   23
c ---[ 339]---> BDD-cost:   23
c ---[ 338]---> BDD-cost:   23
c ---[ 337]---> BDD-cost:   23
c ---[ 336]---> BDD-cost:   23
c ---[ 335]---> BDD-cost:   23
c ---[ 334]---> BDD-cost:   23
c ---[ 333]---> BDD-cost:   23
c ---[ 332]---> BDD-cost:   23
c ---[ 331]---> BDD-cost:   23
c ---[ 330]---> BDD-cost:   23
c ---[ 329]---> BDD-cost:   23
c ---[ 328]---> BDD-cost:   23
c ---[ 327]---> BDD-cost:   23
c ---[ 326]---> BDD-cost:   23
c ---[ 325]---> BDD-cost:   23
c ---[ 324]---> BDD-cost:   23
c ---[ 323]---> BDD-cost:   23
c ---[ 322]---> BDD-cost:   23
c ---[ 321]---> BDD-cost:   23
c ---[ 320]---> BDD-cost:   23
c ---[ 319]---> BDD-cost:   23
c ---[ 318]---> BDD-cost:   23
c ---[ 317]---> BDD-cost:   23
c ---[ 316]---> BDD-cost:   23
c ---[ 315]---> BDD-cost:   23
c ---[ 314]---> BDD-cost:   23
c ---[ 313]---> BDD-cost:   23
c ---[ 312]---> BDD-cost:   23
c ---[ 311]---> BDD-cost:   23
c ---[ 310]---> BDD-cost:   23
c ---[ 309]---> BDD-cost:   23
c ---[ 308]---> BDD-cost:   23
c ---[ 307]---> BDD-cost:   23
c ---[ 306]---> BDD-cost:   23
c ---[ 305]---> BDD-cost:   23
c ---[ 304]---> BDD-cost:   23
c ---[ 303]---> BDD-cost:   23
c ---[ 302]---> BDD-cost:   23
c ---[ 301]---> BDD-cost:   23
c ---[ 300]---> BDD-cost:   23
c ---[ 299]---> BDD-cost:   23
c ---[ 298]---> BDD-cost:   23
c ---[ 297]---> BDD-cost:   23
c ---[ 296]---> BDD-cost:   23
c ---[ 295]---> BDD-cost:   23
c ---[ 294]---> BDD-cost:   23
c ---[ 293]---> BDD-cost:   23
c ---[ 292]---> BDD-cost:   23
c ---[ 291]---> BDD-cost:   23
c ---[ 290]---> BDD-cost:   23
c ---[ 289]---> BDD-cost:   23
c ---[ 288]---> BDD-cost:   23
c ---[ 287]---> BDD-cost:   23
c ---[ 286]---> BDD-cost:   23
c ---[ 285]---> BDD-cost:   23
c ---[ 284]---> BDD-cost:   23
c ---[ 283]---> BDD-cost:   23
c ---[ 282]---> BDD-cost:   23
c ---[ 281]---> BDD-cost:   23
c ---[ 280]---> BDD-cost:   23
c ---[ 279]---> BDD-cost:   23
c ---[ 278]---> BDD-cost:   23
c ---[ 277]---> BDD-cost:   23
c ---[ 276]---> BDD-cost:   23
c ---[ 275]---> BDD-cost:   23
c ---[ 274]---> BDD-cost:   23
c ---[ 273]---> BDD-cost:   23
c ---[ 272]---> BDD-cost:   23
c ---[ 271]---> BDD-cost:   23
c ---[ 270]---> BDD-cost:   23
c ---[ 269]---> BDD-cost:   23
c ---[ 268]---> BDD-cost:   23
c ---[ 267]---> BDD-cost:   23
c ---[ 266]---> BDD-cost:   23
c ---[ 265]---> BDD-cost:   23
c ---[ 264]---> BDD-cost:   23
c ---[ 263]---> BDD-cost:   23
c ---[ 262]---> BDD-cost:   23
c ---[ 261]---> BDD-cost:   23
c ---[ 260]---> BDD-cost:   23
c ---[ 259]---> BDD-cost:   23
c ---[ 258]---> BDD-cost:   23
c ---[ 257]---> BDD-cost:   23
c ---[ 256]---> BDD-cost:   23
c ---[ 255]---> BDD-cost:   23
c ---[ 254]---> BDD-cost:   23
c ---[ 253]---> BDD-cost:   23
c ---[ 252]---> BDD-cost:   23
c ---[ 251]---> BDD-cost:   23
c ---[ 250]---> BDD-cost:   23
c ---[ 249]---> BDD-cost:   23
c ---[ 248]---> BDD-cost:   23
c ---[ 247]---> BDD-cost:   23
c ---[ 246]---> BDD-cost:   23
c ---[ 245]---> BDD-cost:   23
c ---[ 244]---> BDD-cost:   23
c ---[ 243]---> BDD-cost:   23
c ---[ 242]---> BDD-cost:   23
c ---[ 241]---> BDD-cost:   23
c ---[ 240]---> BDD-cost:   23
c ---[ 239]---> BDD-cost:   23
c ---[ 238]---> BDD-cost:   23
c ---[ 237]---> BDD-cost:   23
c ---[ 236]---> BDD-cost:   23
c ---[ 235]---> BDD-cost:   23
c ---[ 234]---> BDD-cost:   23
c ---[ 233]---> BDD-cost:   23
c ---[ 232]---> BDD-cost:   23
c ---[ 231]---> BDD-cost:   23
c ---[ 230]---> BDD-cost:   23
c ---[ 229]---> BDD-cost:   23
c ---[ 228]---> BDD-cost:   23
c ---[ 227]---> BDD-cost:   23
c ---[ 226]---> BDD-cost:   23
c ---[ 225]---> BDD-cost:   23
c ---[ 224]---> BDD-cost:   23
c ---[ 223]---> BDD-cost:   23
c ---[ 222]---> BDD-cost:   23
c ---[ 221]---> BDD-cost:   23
c ---[ 220]---> BDD-cost:   23
c ---[ 219]---> BDD-cost:   23
c ---[ 218]---> BDD-cost:   23
c ---[ 217]---> BDD-cost:   23
c ---[ 216]---> BDD-cost:   23
c ---[ 215]---> BDD-cost:   23
c ---[ 214]---> BDD-cost:   23
c ---[ 213]---> BDD-cost:   23
c ---[ 212]---> BDD-cost:   23
c ---[ 211]---> BDD-cost:   23
c ---[ 210]---> BDD-cost:   23
c ---[ 209]---> BDD-cost:   23
c ---[ 208]---> BDD-cost:   23
c ---[ 207]---> BDD-cost:   23
c ---[ 206]---> BDD-cost:   23
c ---[ 205]---> BDD-cost:   23
c ---[ 204]---> BDD-cost:   23
c ---[ 203]---> BDD-cost:   23
c ---[ 202]---> BDD-cost:   23
c ---[ 201]---> BDD-cost:   23
c ---[ 200]---> BDD-cost:   23
c ---[ 199]---> BDD-cost:   23
c ---[ 198]---> BDD-cost:   23
c ---[ 197]---> BDD-cost:   23
c ---[ 196]---> BDD-cost:   23
c ---[ 195]---> BDD-cost:   23
c ---[ 194]---> BDD-cost:   23
c ---[ 193]---> BDD-cost:   23
c ---[ 192]---> BDD-cost:   23
c ---[ 191]---> BDD-cost:   23
c ---[ 190]---> BDD-cost:   23
c ---[ 189]---> BDD-cost:   23
c ---[ 188]---> BDD-cost:   23
c ---[ 187]---> BDD-cost:   23
c ---[ 186]---> BDD-cost:   23
c ---[ 185]---> BDD-cost:   23
c ---[ 184]---> BDD-cost:   23
c ---[ 183]---> BDD-cost:   23
c ---[ 182]---> BDD-cost:   23
c ---[ 181]---> BDD-cost:   23
c ---[ 180]---> BDD-cost:   23
c ---[ 179]---> BDD-cost:   23
c ---[ 178]---> BDD-cost:   23
c ---[ 177]---> BDD-cost:   23
c ---[ 176]---> BDD-cost:   23
c ---[ 175]---> BDD-cost:   23
c ---[ 174]---> BDD-cost:   23
c ---[ 173]---> BDD-cost:   23
c ---[ 172]---> BDD-cost:   23
c ---[ 171]---> BDD-cost:   23
c ---[ 170]---> BDD-cost:   23
c ---[ 169]---> BDD-cost:   23
c ---[ 168]---> BDD-cost:   23
c ---[ 167]---> BDD-cost:   23
c ---[ 166]---> BDD-cost:   23
c ---[ 165]---> BDD-cost:   23
c ---[ 164]---> BDD-cost:   23
c ---[ 163]---> BDD-cost:   23
c ---[ 162]---> BDD-cost:   23
c ---[ 161]---> BDD-cost:   23
c ---[ 160]---> BDD-cost:   23
c ---[ 159]---> BDD-cost:   23
c ---[ 158]---> BDD-cost:   23
c ---[ 157]---> BDD-cost:   23
c ---[ 156]---> BDD-cost:   23
c ---[ 155]---> BDD-cost:   23
c ---[ 154]---> BDD-cost:   23
c ---[ 153]---> BDD-cost:   23
c ---[ 152]---> BDD-cost:   23
c ---[ 151]---> BDD-cost:   23
c ---[ 150]---> BDD-cost:   23
c ---[ 149]---> BDD-cost:   23
c ---[ 148]---> BDD-cost:   23
c ---[ 147]---> BDD-cost:   23
c ---[ 146]---> BDD-cost:   23
c ---[ 145]---> BDD-cost:   23
c ---[ 144]---> BDD-cost:   23
c ---[ 143]---> BDD-cost:   23
c ---[ 142]---> BDD-cost:   23
c ---[ 141]---> BDD-cost:   23
c ---[ 140]---> BDD-cost:   23
c ---[ 139]---> BDD-cost:   23
c ---[ 138]---> BDD-cost:   23
c ---[ 137]---> BDD-cost:   23
c ---[ 136]---> BDD-cost:   23
c ---[ 135]---> BDD-cost:   23
c ---[ 134]---> BDD-cost:   23
c ---[ 133]---> BDD-cost:   23
c ---[ 132]---> BDD-cost:   23
c ---[ 131]---> BDD-cost:   23
c ---[ 130]---> BDD-cost:   23
c ---[ 129]---> BDD-cost:   23
c ---[ 128]---> BDD-cost:   23
c ---[ 127]---> BDD-cost:   23
c ---[ 126]---> BDD-cost:   23
c ---[ 125]---> BDD-cost:   23
c ---[ 124]---> BDD-cost:   23
c ---[ 123]---> BDD-cost:   23
c ---[ 122]---> BDD-cost:   23
c ---[ 121]---> BDD-cost:   23
c ---[ 120]---> BDD-cost:   23
c ---[ 119]---> BDD-cost:   23
c ---[ 118]---> BDD-cost:   23
c ---[ 117]---> BDD-cost:   23
c ---[ 116]---> BDD-cost:   23
c ---[ 115]---> BDD-cost:   23
c ---[ 114]---> BDD-cost:   23
c ---[ 113]---> BDD-cost:   23
c ---[ 112]---> BDD-cost:   23
c ---[ 111]---> BDD-cost:   23
c ---[ 110]---> BDD-cost:   23
c ---[ 109]---> BDD-cost:   23
c ---[ 108]---> BDD-cost:   23
c ---[ 107]---> BDD-cost:   23
c ---[ 106]---> BDD-cost:   23
c ---[ 105]---> BDD-cost:   23
c ---[ 104]---> BDD-cost:   23
c ---[ 103]---> BDD-cost:   23
c ---[ 102]---> BDD-cost:   23
c ---[ 101]---> BDD-cost:   23
c ---[ 100]---> BDD-cost:   23
c ---[  99]---> BDD-cost:   23
c ---[  98]---> BDD-cost:   23
c ---[  97]---> BDD-cost:   23
c ---[  96]---> BDD-cost:   23
c ---[  95]---> BDD-cost:   23
c ---[  94]---> BDD-cost:   23
c ---[  93]---> BDD-cost:   23
c ---[  92]---> BDD-cost:   23
c ---[  91]---> BDD-cost:   23
c ---[  90]---> BDD-cost:   23
c ---[  89]---> BDD-cost:   23
c ---[  88]---> BDD-cost:   23
c ---[  87]---> BDD-cost:   23
c ---[  86]---> BDD-cost:   23
c ---[  85]---> BDD-cost:   23
c ---[  84]---> BDD-cost:   23
c ---[  83]---> BDD-cost:   23
c ---[  82]---> BDD-cost:   23
c ---[  81]---> BDD-cost:   23
c ---[  80]---> BDD-cost:   23
c ---[  79]---> BDD-cost:   23
c ---[  78]---> BDD-cost:   23
c ---[  77]---> BDD-cost:   23
c ---[  76]---> BDD-cost:   23
c ---[  75]---> BDD-cost:   23
c ---[  74]---> BDD-cost:   23
c ---[  73]---> BDD-cost:   23
c ---[  72]---> BDD-cost:   23
c ---[  71]---> BDD-cost:   23
c ---[  70]---> BDD-cost:   23
c ---[  69]---> BDD-cost:   23
c ---[  68]---> BDD-cost:   23
c ---[  67]---> BDD-cost:   23
c ---[  66]---> BDD-cost:   23
c ---[  65]---> BDD-cost:   23
c ---[  64]---> BDD-cost:   23
c ---[  63]---> BDD-cost:   23
c ---[  62]---> BDD-cost:   23
c ---[  61]---> BDD-cost:   23
c ---[  60]---> BDD-cost:   23
c ---[  59]---> BDD-cost:   23
c ---[  58]---> BDD-cost:   23
c ---[  57]---> BDD-cost:   23
c ---[  56]---> BDD-cost:   23
c ---[  55]---> BDD-cost:   23
c ---[  54]---> BDD-cost:   23
c ---[  53]---> BDD-cost:   23
c ---[  52]---> BDD-cost:   23
c ---[  51]---> BDD-cost:   23
c ---[  50]---> BDD-cost:   23
c ---[  49]---> BDD-cost:   23
c ---[  48]---> BDD-cost:   23
c ---[  47]---> BDD-cost:   23
c ---[  46]---> BDD-cost:   23
c ---[  45]---> BDD-cost:   23
c ---[  44]---> BDD-cost:   23
c ---[  43]---> BDD-cost:   23
c ---[  42]---> BDD-cost:   23
c ---[  41]---> BDD-cost:   23
c ---[  40]---> BDD-cost:   23
c ---[  39]---> BDD-cost:   23
c ---[  38]---> BDD-cost:   23
c ---[  37]---> BDD-cost:   23
c ---[  36]---> BDD-cost:   23
c ---[  35]---> BDD-cost:   23
c ---[  34]---> BDD-cost:   23
c ---[  33]---> BDD-cost:   23
c ---[  32]---> BDD-cost:   23
c ---[  31]---> BDD-cost:   23
c ---[  30]---> BDD-cost:   23
c ---[  29]---> BDD-cost:   23
c ---[  28]---> BDD-cost:   23
c ---[  27]---> BDD-cost:   23
c ---[  26]---> BDD-cost:   23
c ---[  25]---> BDD-cost:   23
c ---[  24]---> BDD-cost:   23
c ---[  23]---> BDD-cost:   23
c ---[  22]---> BDD-cost:   23
c ---[  21]---> BDD-cost:   23
c ---[  20]---> BDD-cost:   23
c ---[  19]---> BDD-cost:   23
c ---[  18]---> BDD-cost:   23
c ---[  17]---> BDD-cost:   23
c ---[  16]---> BDD-cost:   23
c ---[  15]---> BDD-cost:   23
c ---[  14]---> BDD-cost:   23
c ---[  13]---> BDD-cost:   23
c ---[  12]---> BDD-cost:   23
c ---[  11]---> BDD-cost:   23
c ---[  10]---> BDD-cost:   23
c ---[   9]---> BDD-cost:   23
c ---[   8]---> BDD-cost:   23
c ---[   7]---> BDD-cost:   23
c ---[   6]---> BDD-cost:   23
c ---[   5]---> BDD-cost:   23
c ---[   4]---> BDD-cost:   23
c ---[   3]---> BDD-cost:   23
c ---[   2]---> BDD-cost:   23
c ---[   1]---> BDD-cost:   23
c ---[   0]---> BDD-cost:   23
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |  574756  1542689 |  191585       0        0     nan |  0.000 % |
c |       100 |  574740  1542654 |  210743      89     1016    11.4 |  1.194 % |
c |       250 |  574694  1542562 |  231817     216     1798     8.3 |  1.203 % |
c |       475 |  574694  1542562 |  254999     441     2892     6.6 |  1.203 % |
c |       812 |  574688  1542550 |  280499     775     6604     8.5 |  1.204 % |
c |      1318 |  574456  1542086 |  308549    1165    11078     9.5 |  1.247 % |
c |      2078 |  574328  1541828 |  339404    1861    17802     9.6 |  1.270 % |
c |      3217 |  574206  1541579 |  373344    2938    26758     9.1 |  1.293 % |
c |      4925 |  573852  1540840 |  410679    4455    41259     9.3 |  1.359 % |
c |      7487 |  573686  1540472 |  451747    6900    65187     9.4 |  1.390 % |
c ==============================================================================
c [1mFound solution: 25472[0m
c ---[   0]---> BDD-cost:  207
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      9564 |  573984  1541464 |  191328    8866    83602     9.4 |  1.390 % |
c |      9664 |  573972  1541438 |  210460    8960    84619     9.4 |  1.413 % |
c |      9814 |  573916  1541319 |  231506    9081    86061     9.5 |  1.423 % |
c |     10039 |  573914  1541315 |  254657    9305    87744     9.4 |  1.423 % |
c |     10376 |  573874  1541232 |  280123    9622    91021     9.5 |  1.431 % |
c ==============================================================================
c [1mFound solution: 25344[0m
c ---[   0]---> BDD-cost:  103
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     10641 |  574150  1542090 |  191383    9871    92759     9.4 |  1.431 % |
c |     10744 |  574112  1542008 |  210521    9954    93477     9.4 |  1.444 % |
c ==============================================================================
c [1mFound solution: 25216[0m
c ---[   0]---> BDD-cost:  102
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     10855 |  574405  1542893 |  191468   10059    94163     9.4 |  1.444 % |
c |     10955 |  574405  1542893 |  210614   10159    95084     9.4 |  1.446 % |
c |     11107 |  574401  1542883 |  231676   10300    96743     9.4 |  1.446 % |
c |     11332 |  574391  1542858 |  254843   10519    99042     9.4 |  1.448 % |
c |     11669 |  574331  1542710 |  280328   10788   100928     9.4 |  1.459 % |
c ==============================================================================
c [1mFound solution: 25088[0m
c ---[   0]---> BDD-cost:  101
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     11799 |  574627  1543599 |  191542   10899   101711     9.3 |  1.459 % |
c |     11899 |  574623  1543591 |  210696   10997   102702     9.3 |  1.461 % |
c |     12049 |  574613  1543566 |  231765   11142   103965     9.3 |  1.463 % |
c |     12274 |  574607  1543554 |  254942   11364   105869     9.3 |  1.464 % |
c ==============================================================================
c [1mFound solution: 24960[0m
c ---[   0]---> BDD-cost:  100
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     12352 |  574906  1544449 |  191635   11442   106758     9.3 |  1.464 % |
c |     12452 |  574906  1544449 |  210798   11542   107715     9.3 |  1.464 % |
c |     12602 |  574866  1544365 |  231878   11663   108469     9.3 |  1.471 % |
c |     12828 |  574866  1544365 |  255066   11889   110564     9.3 |  1.471 % |
c |     13165 |  574856  1544345 |  280572   12221   114599     9.4 |  1.473 % |
c |     13671 |  574792  1544207 |  308630   12686   119435     9.4 |  1.485 % |
c |     14430 |  574720  1544049 |  339493   13380   125902     9.4 |  1.498 % |
c ==============================================================================
c [1mFound solution: 24448[0m
c ---[   0]---> BDD-cost:  384
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     15450 |  575828  1547394 |  191942   14372   144822    10.1 |  1.498 % |
c |     15551 |  575820  1547375 |  211136   14468   145958    10.1 |  1.505 % |
c |     15701 |  575816  1547366 |  232249   14613   147897    10.1 |  1.506 % |
c |     15926 |  575816  1547366 |  255474   14838   150001    10.1 |  1.506 % |
c |     16266 |  575802  1547332 |  281022   15168   157123    10.4 |  1.509 % |
c |     16774 |  575774  1547267 |  309124   15661   161875    10.3 |  1.514 % |
c ==============================================================================
c [1mFound solution: 24320[0m
c ---[   0]---> BDD-cost:   95
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     17152 |  576042  1548079 |  192014   15987   165321    10.3 |  1.514 % |
c |     17254 |  576042  1548079 |  211215   16089   166488    10.3 |  1.517 % |
c |     17404 |  576042  1548079 |  232336   16239   168794    10.4 |  1.517 % |
c |     17629 |  575956  1547904 |  255570   16413   171017    10.4 |  1.533 % |
c |     17966 |  575934  1547860 |  281127   16740   177234    10.6 |  1.537 % |
c ==============================================================================
c [1mFound solution: 24192[0m
c ---[   0]---> BDD-cost:   94
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     18317 |  576211  1548691 |  192070   17089   180047    10.5 |  1.537 % |
c |     18417 |  576211  1548691 |  211277   17189   180876    10.5 |  1.537 % |
c |     18567 |  576211  1548691 |  232404   17339   182263    10.5 |  1.537 % |
c |     18793 |  576207  1548681 |  255645   17562   185709    10.6 |  1.538 % |
c |     19131 |  576203  1548673 |  281209   17898   190343    10.6 |  1.539 % |
c |     19637 |  576195  1548657 |  309330   18400   197728    10.7 |  1.540 % |
c |     20398 |  576165  1548583 |  340263   19135   208722    10.9 |  1.546 % |
c |     21538 |  576101  1548446 |  374290   20217   227599    11.3 |  1.557 % |
c |     23248 |  576037  1548304 |  411719   21887   251314    11.5 |  1.569 % |
c ==============================================================================
c [1mFound solution: 22528[0m
c ---[   0]---> Sorter-cost: 2346     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     24790 |  578472  1554051 |  192824   23417   269791    11.5 |  1.569 % |
c |     24891 |  578456  1554019 |  212106   23510   270449    11.5 |  1.567 % |
c |     25042 |  578354  1553814 |  233317   23609   271870    11.5 |  1.586 % |
c |     25267 |  578354  1553814 |  256648   23834   274291    11.5 |  1.586 % |
c |     25605 |  578352  1553809 |  282313   24166   278362    11.5 |  1.586 % |
c |     26112 |  578340  1553782 |  310544   24666   284563    11.5 |  1.588 % |
c |     26871 |  578198  1553496 |  341599   25352   290714    11.5 |  1.614 % |
c |     28011 |  578182  1553459 |  375759   26484   306935    11.6 |  1.617 % |
c |     29719 |  578170  1553431 |  413335   28186   344091    12.2 |  1.619 % |
c |     32281 |  578054  1553197 |  454668   30685   373546    12.2 |  1.641 % |
c |     36126 |  578046  1553181 |  500135   34526   443582    12.8 |  1.642 % |
c |     41893 |  578004  1553090 |  550149   40263   578148    14.4 |  1.650 % |
c |     50544 |  577982  1553043 |  605164   48878   816471    16.7 |  1.654 % |
c ==============================================================================
c [1mFound solution: 22016[0m
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     63460 |  577823  1552746 |  192607   61516  1054370    17.1 |  1.654 % |
c |     63560 |  577823  1552746 |  211867   61616  1055490    17.1 |  1.695 % |
c |     63710 |  577823  1552746 |  233054   61766  1056717    17.1 |  1.695 % |
c |     63935 |  577823  1552746 |  256359   61991  1059495    17.1 |  1.695 % |
c |     64273 |  577819  1552737 |  281995   62327  1063809    17.1 |  1.696 % |
c |     64779 |  577791  1552677 |  310195   62816  1070858    17.0 |  1.701 % |
c |     65538 |  577779  1552653 |  341215   63569  1080835    17.0 |  1.704 % |
c |     66678 |  577779  1552653 |  375336   64709  1117860    17.3 |  1.704 % |
c ==============================================================================
c [1mFound solution: 20608[0m
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     67917 |  577826  1552838 |  192608   65874  1143553    17.4 |  1.704 % |
c |     68019 |  577822  1552829 |  211868   65974  1144292    17.3 |  1.719 % |
c |     68169 |  577822  1552829 |  233055   66124  1145901    17.3 |  1.719 % |
c |     68395 |  577818  1552819 |  256361   66342  1149168    17.3 |  1.720 % |
c |     68733 |  577792  1552766 |  281997   66658  1154966    17.3 |  1.724 % |
c |     69239 |  577790  1552762 |  310197   67163  1166434    17.4 |  1.725 % |
c |     69999 |  577788  1552758 |  341216   67922  1176005    17.3 |  1.725 % |
c |     71138 |  577788  1552758 |  375338   69061  1192642    17.3 |  1.725 % |
c |     72846 |  577770  1552721 |  412872   70760  1217586    17.2 |  1.728 % |
c |     75409 |  577764  1552707 |  454159   73320  1272837    17.4 |  1.729 % |
c |     79253 |  577710  1552598 |  499575   77137  1331370    17.3 |  1.739 % |
c |     85020 |  577632  1552435 |  549533   82830  1420825    17.2 |  1.754 % |
/oldhome/oroussel/solvers/minisat+_script: line 9: 11898 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): 1.06 0.99 0.91 2/54 11894
Raw data (stat): 11894 (runsolver) R 11893 24821 24820 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 843189101 1052672 99 4294967295 134512640 135381576 3221224480 3221219688 135158418 0 2147483391 7 90112 0 0 0 17 1 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0001 s]
Raw data (loadavg): 1.05 0.99 0.91 2/55 11898
Raw data (stat): 11894 (minisat+_script) S 11893 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 843189101 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+20 s]
Raw data (loadavg): 1.04 0.99 0.91 2/55 11898
Raw data (stat): 11894 (minisat+_script) S 11893 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 843189101 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+30.0004 s]
Raw data (loadavg): 1.04 0.99 0.91 2/55 11898
Raw data (stat): 11894 (minisat+_script) S 11893 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 843189101 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+40.0002 s]
Raw data (loadavg): 1.03 0.99 0.91 2/55 11898
Raw data (stat): 11894 (minisat+_script) S 11893 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 843189101 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+50.0002 s]
Raw data (loadavg): 1.02 0.99 0.91 2/55 11898
Raw data (stat): 11894 (minisat+_script) S 11893 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 843189101 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+60.0008 s]
Raw data (loadavg): 1.02 0.99 0.91 2/55 11898
Raw data (stat): 11894 (minisat+_script) S 11893 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 843189101 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+70.0004 s]
Raw data (loadavg): 1.02 0.99 0.91 2/55 11898
Raw data (stat): 11894 (minisat+_script) S 11893 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 843189101 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+80.1023 s]
Raw data (loadavg): 1.01 0.99 0.91 2/55 11898
Raw data (stat): 11894 (minisat+_script) S 11893 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 843189101 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+90.1017 s]
Raw data (loadavg): 1.01 0.99 0.91 2/55 11898
Raw data (stat): 11894 (minisat+_script) S 11893 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 843189101 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+100.101 s]
Raw data (loadavg): 1.01 0.99 0.91 2/55 11898
Raw data (stat): 11894 (minisat+_script) S 11893 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 843189101 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+110.105 s]
Raw data (loadavg): 1.01 0.99 0.91 2/55 11898
Raw data (stat): 11894 (minisat+_script) S 11893 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 843189101 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+120.105 s]
Raw data (loadavg): 1.01 0.99 0.91 2/55 11898
Raw data (stat): 11894 (minisat+_script) S 11893 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 843189101 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+130.106 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 11898
Raw data (stat): 11894 (minisat+_script) S 11893 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 843189101 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+140.106 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 11898
Raw data (stat): 11894 (minisat+_script) S 11893 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 843189101 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+150.106 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 11898
Raw data (stat): 11894 (minisat+_script) S 11893 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 843189101 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+160.106 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 11898
Raw data (stat): 11894 (minisat+_script) S 11893 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 843189101 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+170.105 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 11898
Raw data (stat): 11894 (minisat+_script) S 11893 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 843189101 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+180.106 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 11898
Raw data (stat): 11894 (minisat+_script) S 11893 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 843189101 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+190.106 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 11898
Raw data (stat): 11894 (minisat+_script) S 11893 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 843189101 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+200.106 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 11898
Raw data (stat): 11894 (minisat+_script) S 11893 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 843189101 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+210.105 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 11898
Raw data (stat): 11894 (minisat+_script) S 11893 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 843189101 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+220.105 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 11898
Raw data (stat): 11894 (minisat+_script) S 11893 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 843189101 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+230.105 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 11898
Raw data (stat): 11894 (minisat+_script) S 11893 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 843189101 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+240.105 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 11898
Raw data (stat): 11894 (minisat+_script) S 11893 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 843189101 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+250.104 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 11898
Raw data (stat): 11894 (minisat+_script) S 11893 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 843189101 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+260.104 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 11898
Raw data (stat): 11894 (minisat+_script) S 11893 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 843189101 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+270.104 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 11898
Raw data (stat): 11894 (minisat+_script) S 11893 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 843189101 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+280.103 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 11898
Raw data (stat): 11894 (minisat+_script) S 11893 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 843189101 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+290.104 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 11898
Raw data (stat): 11894 (minisat+_script) S 11893 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 843189101 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+300.104 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 11898
Raw data (stat): 11894 (minisat+_script) S 11893 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 843189101 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+310.104 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 11898
Raw data (stat): 11894 (minisat+_script) S 11893 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 843189101 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+320.13 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 11898
Raw data (stat): 11894 (minisat+_script) S 11893 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 843189101 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+330.13 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 11898
Raw data (stat): 11894 (minisat+_script) S 11893 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 843189101 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+340.13 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 11898
Raw data (stat): 11894 (minisat+_script) S 11893 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 843189101 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+350.13 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 11898
Raw data (stat): 11894 (minisat+_script) S 11893 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 843189101 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+360.13 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 11898
Raw data (stat): 11894 (minisat+_script) S 11893 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 843189101 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+370.13 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 11898
Raw data (stat): 11894 (minisat+_script) S 11893 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 843189101 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+380.129 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 11898
Raw data (stat): 11894 (minisat+_script) S 11893 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 843189101 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+390.129 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 11898
Raw data (stat): 11894 (minisat+_script) S 11893 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 843189101 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+400.129 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 11898
Raw data (stat): 11894 (minisat+_script) S 11893 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 843189101 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+410.208 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 11898
Raw data (stat): 11894 (minisat+_script) S 11893 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 843189101 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+420.209 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 11898
Raw data (stat): 11894 (minisat+_script) S 11893 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 843189101 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+430.209 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 11898
Raw data (stat): 11894 (minisat+_script) S 11893 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 843189101 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+440.209 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 11898
Raw data (stat): 11894 (minisat+_script) S 11893 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 843189101 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+450.209 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 11898
Raw data (stat): 11894 (minisat+_script) S 11893 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 843189101 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+460.209 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 11898
Raw data (stat): 11894 (minisat+_script) S 11893 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 843189101 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+470.209 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 11898
Raw data (stat): 11894 (minisat+_script) S 11893 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 843189101 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+480.21 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 11898
Raw data (stat): 11894 (minisat+_script) S 11893 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 843189101 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+490.21 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 11898
Raw data (stat): 11894 (minisat+_script) S 11893 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 843189101 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+500.21 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 11898
Raw data (stat): 11894 (minisat+_script) S 11893 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 843189101 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+510.21 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 11898
Raw data (stat): 11894 (minisat+_script) S 11893 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 843189101 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+520.21 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 11898
Raw data (stat): 11894 (minisat+_script) S 11893 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 843189101 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+530.211 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 11898
Raw data (stat): 11894 (minisat+_script) S 11893 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 843189101 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+540.21 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 11898
Raw data (stat): 11894 (minisat+_script) S 11893 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 843189101 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+550.21 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 11898
Raw data (stat): 11894 (minisat+_script) S 11893 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 843189101 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+560.21 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 11898
Raw data (stat): 11894 (minisat+_script) S 11893 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 843189101 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+570.21 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 11898
Raw data (stat): 11894 (minisat+_script) S 11893 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 843189101 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+580.21 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 11898
Raw data (stat): 11894 (minisat+_script) S 11893 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 843189101 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+590.21 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 11898
Raw data (stat): 11894 (minisat+_script) S 11893 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 843189101 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+600.21 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 11898
Raw data (stat): 11894 (minisat+_script) S 11893 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 843189101 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+610.21 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 11898
Raw data (stat): 11894 (minisat+_script) S 11893 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 843189101 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+620.21 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 11898
Raw data (stat): 11894 (minisat+_script) S 11893 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 843189101 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+630.21 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 11898
Raw data (stat): 11894 (minisat+_script) S 11893 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 843189101 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+640.211 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 11898
Raw data (stat): 11894 (minisat+_script) S 11893 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 843189101 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+650.211 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 11898
Raw data (stat): 11894 (minisat+_script) S 11893 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 843189101 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+660.211 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 11898
Raw data (stat): 11894 (minisat+_script) S 11893 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 843189101 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+670.212 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 11898
Raw data (stat): 11894 (minisat+_script) S 11893 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 843189101 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+680.212 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 11898
Raw data (stat): 11894 (minisat+_script) S 11893 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 843189101 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+690.212 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 11898
Raw data (stat): 11894 (minisat+_script) S 11893 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 843189101 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+700.212 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 11898
Raw data (stat): 11894 (minisat+_script) S 11893 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 843189101 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+710.224 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 11898
Raw data (stat): 11894 (minisat+_script) S 11893 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 843189101 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+720.223 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 11898
Raw data (stat): 11894 (minisat+_script) S 11893 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 843189101 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+730.224 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 11898
Raw data (stat): 11894 (minisat+_script) S 11893 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 843189101 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+740.225 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 11898
Raw data (stat): 11894 (minisat+_script) S 11893 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 843189101 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+750.224 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 11898
Raw data (stat): 11894 (minisat+_script) S 11893 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 843189101 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+760.224 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 11898
Raw data (stat): 11894 (minisat+_script) S 11893 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 843189101 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+770.225 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 11898
Raw data (stat): 11894 (minisat+_script) S 11893 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 843189101 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+780.226 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 11898
Raw data (stat): 11894 (minisat+_script) S 11893 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 843189101 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+790.225 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 11898
Raw data (stat): 11894 (minisat+_script) S 11893 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 843189101 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+800.225 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 11898
Raw data (stat): 11894 (minisat+_script) S 11893 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 843189101 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+810.226 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 11898
Raw data (stat): 11894 (minisat+_script) S 11893 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 843189101 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+820.226 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 11898
Raw data (stat): 11894 (minisat+_script) S 11893 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 843189101 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+830.227 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 11898
Raw data (stat): 11894 (minisat+_script) S 11893 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 843189101 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+840.227 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 11898
Raw data (stat): 11894 (minisat+_script) S 11893 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 843189101 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+850.227 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 11898
Raw data (stat): 11894 (minisat+_script) S 11893 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 843189101 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+860.226 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 11898
Raw data (stat): 11894 (minisat+_script) S 11893 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 843189101 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+870.226 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 11898
Raw data (stat): 11894 (minisat+_script) S 11893 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 843189101 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+880.227 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 11898
Raw data (stat): 11894 (minisat+_script) S 11893 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 843189101 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+890.227 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 11898
Raw data (stat): 11894 (minisat+_script) S 11893 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 843189101 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+900.226 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 11898
Raw data (stat): 11894 (minisat+_script) S 11893 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 843189101 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+910.226 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 11898
Raw data (stat): 11894 (minisat+_script) S 11893 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 843189101 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+920.227 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 11898
Raw data (stat): 11894 (minisat+_script) S 11893 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 843189101 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+930.226 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 11898
Raw data (stat): 11894 (minisat+_script) S 11893 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 843189101 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+940.226 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 11898
Raw data (stat): 11894 (minisat+_script) S 11893 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 843189101 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+950.226 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 11898
Raw data (stat): 11894 (minisat+_script) S 11893 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 843189101 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+960.226 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 11898
Raw data (stat): 11894 (minisat+_script) S 11893 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 843189101 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+970.226 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 11898
Raw data (stat): 11894 (minisat+_script) S 11893 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 843189101 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+980.226 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 11898
Raw data (stat): 11894 (minisat+_script) S 11893 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 843189101 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+990.226 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 11898
Raw data (stat): 11894 (minisat+_script) S 11893 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 843189101 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1000.23 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 11898
Raw data (stat): 11894 (minisat+_script) S 11893 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 843189101 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1010.23 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 11898
Raw data (stat): 11894 (minisat+_script) S 11893 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 843189101 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1020.22 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 11898
Raw data (stat): 11894 (minisat+_script) S 11893 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 843189101 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1030.23 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 11898
Raw data (stat): 11894 (minisat+_script) S 11893 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 843189101 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1040.23 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 11898
Raw data (stat): 11894 (minisat+_script) S 11893 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 843189101 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1050.22 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 11898
Raw data (stat): 11894 (minisat+_script) S 11893 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 843189101 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1060.23 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 11898
Raw data (stat): 11894 (minisat+_script) S 11893 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 843189101 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1070.23 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 11898
Raw data (stat): 11894 (minisat+_script) S 11893 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 843189101 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1080.23 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 11898
Raw data (stat): 11894 (minisat+_script) S 11893 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 843189101 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1090.23 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 11898
Raw data (stat): 11894 (minisat+_script) S 11893 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 843189101 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1100.23 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 11898
Raw data (stat): 11894 (minisat+_script) S 11893 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 843189101 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1110.23 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 11898
Raw data (stat): 11894 (minisat+_script) S 11893 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 843189101 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1120.23 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 11898
Raw data (stat): 11894 (minisat+_script) S 11893 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 843189101 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1130.23 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 11898
Raw data (stat): 11894 (minisat+_script) S 11893 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 843189101 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1140.23 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 11898
Raw data (stat): 11894 (minisat+_script) S 11893 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 843189101 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1150.23 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 11898
Raw data (stat): 11894 (minisat+_script) S 11893 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 843189101 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1160.23 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 11898
Raw data (stat): 11894 (minisat+_script) S 11893 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 843189101 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1170.23 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 11898
Raw data (stat): 11894 (minisat+_script) S 11893 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 843189101 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1180.23 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 11898
Raw data (stat): 11894 (minisat+_script) S 11893 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 843189101 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1190.23 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 11898
Raw data (stat): 11894 (minisat+_script) S 11893 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 843189101 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1200.23 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 11898
Raw data (stat): 11894 (minisat+_script) S 11893 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 843189101 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1210.23 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 11898
Raw data (stat): 11894 (minisat+_script) S 11893 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 843189101 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1220.22 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 11898
Raw data (stat): 11894 (minisat+_script) S 11893 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 843189101 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1229.72 s]
Raw data (loadavg): 1.00 0.99 0.91 1/53 11898
Raw data (stat): 11894 (minisat+_script) S 11893 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 843189101 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 0

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