PB'05 competition: run trace

Some explanations

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

Name	normalized-opb/mps-v2-20-10/plato.asu.edu/pub/unibo/normalized-mps-v2-20-10-railway_8_1_0.opb
MD5SUM	7bc553fee464cd071c8e3d02b13f4c95
Bench Category	optimization, big integers (OPTBIGINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	499712
Optimality of the best value was proved	NO
Number of terms in the objective function	133
Biggest coefficient in the objective function	536870912
Number of bits for the biggest coefficient in the objective function	30
Sum of the numbers in the objective function	1073847295
Number of bits of the sum of numbers in the objective function	31
Biggest number in a constraint	1024000000
Number of bits of the biggest number in a constraint	30
Biggest sum of numbers in a constraint	2147758078
Number of bits of the biggest sum of numbers	32
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	1201.13
Number of variables	19747
Total number of constraints	4322
Number of constraints which are clauses	426
Number of constraints which are cardinality constraints (but not clauses)	1177
Number of constraints which are nor clauses,nor cardinality constraints	2719
Minimum length of a constraint	1
Maximum length of a constraint	61
Trace number 32211

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc19 THE 2005-05-27 08:24:55 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=23525 boxname=wulflinc19 idbench=1169 idsolver=16 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  7bc553fee464cd071c8e3d02b13f4c95  /oldhome/oroussel/tmp/wulflinc19/normalized-mps-v2-20-10-railway_8_1_0.opb
REAL COMMAND:  minisat+_script -cb -gs /oldhome/oroussel/tmp/wulflinc19/normalized-mps-v2-20-10-railway_8_1_0.opb
IDLAUNCH: 23525
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.037
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	: 890.88

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.037
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:        894344 kB
Buffers:           140 kB
Cached:         118992 kB
SwapCached:        684 kB
Active:          17044 kB
Inactive:       104240 kB
HighTotal:      131008 kB
HighFree:         9100 kB
LowTotal:       903652 kB
LowFree:        885244 kB
SwapTotal:     2097892 kB
SwapFree:      2096396 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           5192 kB
Slab:            13304 kB
Committed_AS:    63600 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-05-27 08:45:25 (client local time) WITH STATUS 152 IN 1229.88 SECONDS
stats: 23525 7 1229.88 152
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 3146 PB-constraints to clauses...
c   -- Unit propagations: pppp
c   -- Detecting intervals from adjacent constraints: ###################################################################################################################################################################
c   -- Clauses(.)/Splits(s): ssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssss..........................................................................................................................................................................................................................................................................................................................................................................................................................................
c ---[3140]---> BDD-cost:   88
c ---[3139]---> BDD-cost:   88
c ---[3138]---> BDD-cost:   88
c ---[3137]---> BDD-cost:  121
c ---[3136]---> BDD-cost:  119
c ---[3135]---> BDD-cost:   88
c ---[3134]---> BDD-cost:   88
c ---[3133]---> BDD-cost:   88
c ---[3132]---> BDD-cost:   88
c ---[3131]---> BDD-cost:  119
c ---[3129]---> BDD-cost:  119
c ---[3128]---> BDD-cost:   88
c ---[3127]---> BDD-cost:   88
c ---[3126]---> BDD-cost:   88
c ---[3125]---> BDD-cost:   88
c ---[3124]---> BDD-cost:  121
c ---[3123]---> BDD-cost:  119
c ---[3122]---> BDD-cost:   88
c ---[3121]---> BDD-cost:   88
c ---[3120]---> BDD-cost:   88
c ---[3118]---> BDD-cost:   88
c ---[3117]---> BDD-cost:  123
c ---[3116]---> BDD-cost:  119
c ---[3115]---> BDD-cost:   88
c ---[3114]---> BDD-cost:   88
c ---[3113]---> BDD-cost:   88
c ---[3112]---> BDD-cost:   88
c ---[3111]---> BDD-cost:  123
c ---[3110]---> BDD-cost:  119
c ---[3109]---> BDD-cost:   88
c ---[3107]---> BDD-cost:   88
c ---[3106]---> BDD-cost:   88
c ---[3105]---> BDD-cost:   88
c ---[3104]---> BDD-cost:  121
c ---[3103]---> BDD-cost:  119
c ---[3102]---> BDD-cost:   88
c ---[3101]---> BDD-cost:   88
c ---[3100]---> BDD-cost:   88
c ---[3099]---> BDD-cost:   88
c ---[3098]---> BDD-cost:  125
c ---[3096]---> BDD-cost:  119
c ---[3095]---> BDD-cost:   88
c ---[3094]---> BDD-cost:   88
c ---[3093]---> BDD-cost:   88
c ---[3092]---> BDD-cost:   88
c ---[3090]---> BDD-cost:  125
c ---[3088]---> BDD-cost:  123
c ---[3087]---> BDD-cost:  125
c ---[3085]---> BDD-cost:  125
c ---[3083]---> BDD-cost:  125
c ---[3081]---> BDD-cost:  123
c ---[3079]---> BDD-cost:  125
c ---[3077]---> BDD-cost:  125
c ---[3076]---> BDD-cost:  125
c ---[3074]---> BDD-cost:  125
c ---[3072]---> BDD-cost:  125
c ---[3070]---> BDD-cost:  123
c ---[3068]---> BDD-cost:  123
c ---[3066]---> BDD-cost:  125
c ---[3065]---> BDD-cost:  123
c ---[3063]---> BDD-cost:  123
c ---[3061]---> BDD-cost:   88
c ---[3059]---> BDD-cost:  125
c ---[3057]---> BDD-cost:  125
c ---[3055]---> BDD-cost:  125
c ---[3054]---> BDD-cost:  123
c ---[3052]---> BDD-cost:  123
c ---[3050]---> BDD-cost:  125
c ---[3048]---> BDD-cost:  123
c ---[3046]---> BDD-cost:  125
c ---[3044]---> BDD-cost:  125
c ---[3043]---> BDD-cost:  125
c ---[3041]---> BDD-cost:  125
c ---[3039]---> BDD-cost:   88
c ---[3037]---> BDD-cost:   88
c ---[3035]---> BDD-cost:  123
c ---[3033]---> BDD-cost:  121
c ---[3032]---> BDD-cost:  123
c ---[3029]---> BDD-cost:  123
c ---[3027]---> BDD-cost:  121
c ---[3025]---> BDD-cost:  125
c ---[3023]---> BDD-cost:  123
c ---[3021]---> BDD-cost:  125
c ---[3020]---> BDD-cost:  123
c ---[3018]---> BDD-cost:  123
c ---[3016]---> BDD-cost:  123
c ---[3014]---> BDD-cost:  125
c ---[3012]---> BDD-cost:  125
c ---[3010]---> BDD-cost:  121
c ---[3009]---> BDD-cost:  119
c ---[3007]---> BDD-cost:  119
c ---[3005]---> BDD-cost:  119
c ---[3003]---> BDD-cost:  119
c ---[3001]---> BDD-cost:  123
c ---[2999]---> BDD-cost:  125
c ---[2998]---> BDD-cost:  125
c ---[2996]---> BDD-cost:  125
c ---[2994]---> BDD-cost:   88
c ---[2992]---> BDD-cost:  125
c ---[2990]---> BDD-cost:  123
c ---[2988]---> BDD-cost:  125
c ---[2987]---> BDD-cost:  125
c ---[2985]---> BDD-cost:  125
c ---[2983]---> BDD-cost:  125
c ---[2981]---> BDD-cost:  123
c ---[2979]---> BDD-cost:  125
c ---[2977]---> BDD-cost:  121
c ---[2976]---> BDD-cost:  125
c ---[2974]---> BDD-cost:  125
c ---[2972]---> BDD-cost:  121
c ---[2970]---> BDD-cost:  125
c ---[2968]---> BDD-cost:  123
c ---[2966]---> BDD-cost:  125
c ---[2965]---> BDD-cost:  123
c ---[2963]---> BDD-cost:  123
c ---[2961]---> BDD-cost:  123
c ---[2959]---> BDD-cost:   88
c ---[2957]---> BDD-cost:  123
c ---[2955]---> BDD-cost:  123
c ---[2954]---> BDD-cost:  125
c ---[2952]---> BDD-cost:  125
c ---[2950]---> BDD-cost:   88
c ---[2948]---> BDD-cost:  123
c ---[2946]---> BDD-cost:  123
c ---[2944]---> BDD-cost:  125
c ---[2943]---> BDD-cost:  123
c ---[2941]---> BDD-cost:  123
c ---[2939]---> BDD-cost:  125
c ---[2937]---> BDD-cost:  125
c ---[2935]---> BDD-cost:  123
c ---[2933]---> BDD-cost:  123
c ---[2932]---> BDD-cost:  121
c ---[2930]---> BDD-cost:  121
c ---[2928]---> BDD-cost:  123
c ---[2926]---> BDD-cost:  125
c ---[2924]---> BDD-cost:  123
c ---[2922]---> BDD-cost:   88
c ---[2921]---> BDD-cost:  125
c ---[2918]---> BDD-cost:  125
c ---[2916]---> BDD-cost:  123
c ---[2914]---> BDD-cost:  125
c ---[2912]---> BDD-cost:   88
c ---[2910]---> BDD-cost:  125
c ---[2909]---> BDD-cost:  123
c ---[2907]---> BDD-cost:  123
c ---[2905]---> BDD-cost:  121
c ---[2903]---> BDD-cost:  123
c ---[2901]---> BDD-cost:   88
c ---[2899]---> BDD-cost:  121
c ---[2898]---> BDD-cost:  125
c ---[2896]---> BDD-cost:  125
c ---[2894]---> BDD-cost:  123
c ---[2892]---> BDD-cost:  125
c ---[2890]---> BDD-cost:  125
c ---[2888]---> BDD-cost:  123
c ---[2887]---> BDD-cost:  125
c ---[2885]---> BDD-cost:  125
c ---[2883]---> BDD-cost:   88
c ---[2881]---> BDD-cost:  125
c ---[2879]---> BDD-cost:  123
c ---[2877]---> BDD-cost:  125
c ---[2876]---> BDD-cost:  121
c ---[2874]---> BDD-cost:  121
c ---[2872]---> BDD-cost:  121
c ---[2870]---> BDD-cost:  119
c ---[2868]---> BDD-cost:  125
c ---[2866]---> BDD-cost:  123
c ---[2865]---> BDD-cost:  123
c ---[2863]---> BDD-cost:  123
c ---[2861]---> BDD-cost:  125
c ---[2859]---> BDD-cost:   88
c ---[2857]---> BDD-cost:  123
c ---[2855]---> BDD-cost:  125
c ---[2854]---> BDD-cost:   88
c ---[2852]---> BDD-cost:   88
c ---[2850]---> BDD-cost:  125
c ---[2848]---> BDD-cost:  125
c ---[2846]---> BDD-cost:  125
c ---[2844]---> BDD-cost:  125
c ---[2843]---> BDD-cost:  123
c ---[2841]---> BDD-cost:  123
c ---[2839]---> BDD-cost:  125
c ---[2837]---> BDD-cost:  123
c ---[2835]---> BDD-cost:  123
c ---[2833]---> BDD-cost:  123
c ---[2832]---> BDD-cost:   88
c ---[2830]---> BDD-cost:   88
c ---[2828]---> BDD-cost:  125
c ---[2826]---> BDD-cost:  125
c ---[2824]---> BDD-cost:  121
c ---[2822]---> BDD-cost:  125
c ---[2821]---> BDD-cost:  125
c ---[2819]---> BDD-cost:  125
c ---[2817]---> BDD-cost:   88
c ---[2815]---> BDD-cost:  125
c ---[2813]---> BDD-cost:  123
c ---[2811]---> BDD-cost:  125
c ---[2810]---> BDD-cost:  125
c ---[2807]---> BDD-cost:  125
c ---[2805]---> BDD-cost:  125
c ---[2803]---> BDD-cost:  125
c ---[2801]---> BDD-cost:   88
c ---[2799]---> BDD-cost:  125
c ---[2798]---> BDD-cost:  125
c ---[2796]---> BDD-cost:  125
c ---[2794]---> BDD-cost:   88
c ---[2792]---> BDD-cost:  125
c ---[2790]---> BDD-cost:  123
c ---[2788]---> BDD-cost:  125
c ---[2787]---> BDD-cost:  125
c ---[2785]---> BDD-cost:  125
c ---[2783]---> BDD-cost:  123
c ---[2781]---> BDD-cost:   88
c ---[2779]---> BDD-cost:   88
c ---[2777]---> BDD-cost:  125
c ---[2776]---> BDD-cost:  125
c ---[2774]---> BDD-cost:  125
c ---[2772]---> BDD-cost:  125
c ---[2770]---> BDD-cost:   88
c ---[2768]---> BDD-cost:  121
c ---[2766]---> BDD-cost:  123
c ---[2765]---> BDD-cost:   88
c ---[2763]---> BDD-cost:   88
c ---[2761]---> BDD-cost:  125
c ---[2759]---> BDD-cost:   88
c ---[2757]---> BDD-cost:  123
c ---[2755]---> BDD-cost:   88
c ---[2754]---> BDD-cost:   88
c ---[2752]---> BDD-cost:   88
c ---[2750]---> BDD-cost:  125
c ---[2748]---> BDD-cost:  125
c ---[2746]---> BDD-cost:   88
c ---[2744]---> BDD-cost:   88
c ---[2743]---> BDD-cost:  125
c ---[2741]---> BDD-cost:  125
c ---[2739]---> BDD-cost:  125
c ---[2737]---> BDD-cost:  125
c ---[2735]---> BDD-cost:  125
c ---[2733]---> BDD-cost:  125
c ---[2732]---> BDD-cost:  125
c ---[2730]---> BDD-cost:  125
c ---[2728]---> BDD-cost:   88
c ---[2726]---> BDD-cost:  125
c ---[2724]---> BDD-cost:  125
c ---[2722]---> BDD-cost:   88
c ---[2721]---> BDD-cost:  125
c ---[2719]---> BDD-cost:  125
c ---[2717]---> BDD-cost:   88
c ---[2715]---> BDD-cost:   88
c ---[2713]---> BDD-cost:  125
c ---[2711]---> BDD-cost:   88
c ---[2710]---> BDD-cost:   88
c ---[2708]---> BDD-cost:   88
c ---[2706]---> BDD-cost:   88
c ---[2704]---> BDD-cost:  125
c ---[2702]---> BDD-cost:  125
c ---[2700]---> BDD-cost:   88
c ---[2699]---> BDD-cost:  125
c ---[2696]---> BDD-cost:  125
c ---[2694]---> BDD-cost:   88
c ---[2692]---> BDD-cost:  125
c ---[2690]---> BDD-cost:  123
c ---[2688]---> BDD-cost:   88
c ---[2687]---> BDD-cost:  125
c ---[2685]---> BDD-cost:  125
c ---[2683]---> BDD-cost:  125
c ---[2681]---> BDD-cost:  125
c ---[2679]---> BDD-cost:  121
c ---[2677]---> BDD-cost:  125
c ---[2676]---> BDD-cost:  123
c ---[2674]---> BDD-cost:  123
c ---[2672]---> BDD-cost:  123
c ---[2670]---> BDD-cost:   88
c ---[2668]---> BDD-cost:  125
c ---[2666]---> BDD-cost:  121
c ---[2665]---> BDD-cost:  125
c ---[2663]---> BDD-cost:  125
c ---[2661]---> BDD-cost:  125
c ---[2659]---> BDD-cost:  123
c ---[2657]---> BDD-cost:  123
c ---[2655]---> BDD-cost:   88
c ---[2654]---> BDD-cost:  125
c ---[2652]---> BDD-cost:  125
c ---[2650]---> BDD-cost:  125
c ---[2648]---> BDD-cost:  125
c ---[2646]---> BDD-cost:   88
c ---[2644]---> BDD-cost:  123
c ---[2643]---> BDD-cost:  121
c ---[2641]---> BDD-cost:  121
c ---[2639]---> BDD-cost:  119
c ---[2638]---> BDD-cost:  128
c ---[2637]---> BDD-cost:  128
c ---[2636]---> BDD-cost:  137
c ---[2635]---> BDD-cost:  137
c ---[2634]---> BDD-cost:  140
c ---[2633]---> BDD-cost:  140
c ---[2632]---> BDD-cost:  137
c ---[2630]---> BDD-cost:  137
c ---[2629]---> BDD-cost:  135
c ---[2628]---> BDD-cost:  135
c ---[2627]---> BDD-cost:  137
c ---[2626]---> BDD-cost:  137
c ---[2625]---> BDD-cost:  143
c ---[2624]---> BDD-cost:  143
c ---[2623]---> BDD-cost:  137
c ---[2622]---> BDD-cost:  137
c ---[2621]---> BDD-cost:  135
c ---[2619]---> BDD-cost:  135
c ---[2618]---> BDD-cost:  137
c ---[2617]---> BDD-cost:  137
c ---[2616]---> BDD-cost:  140
c ---[2615]---> BDD-cost:  140
c ---[2614]---> BDD-cost:  137
c ---[2613]---> BDD-cost:  137
c ---[2612]---> BDD-cost:  138
c ---[2611]---> BDD-cost:  138
c ---[2610]---> BDD-cost:  137
c ---[2608]---> BDD-cost:  137
c ---[2607]---> BDD-cost:  143
c ---[2606]---> BDD-cost:  143
c ---[2605]---> BDD-cost:  137
c ---[2604]---> BDD-cost:  137
c ---[2603]---> BDD-cost:  140
c ---[2602]---> BDD-cost:  140
c ---[2601]---> BDD-cost:  137
c ---[2600]---> BDD-cost:  137
c ---[2599]---> BDD-cost:  130
c ---[2597]---> BDD-cost:  130
c ---[2596]---> BDD-cost:  137
c ---[2595]---> BDD-cost:  137
c ---[2594]---> BDD-cost:  146
c ---[2593]---> BDD-cost:  146
c ---[2592]---> BDD-cost:  137
c ---[2591]---> BDD-cost:  137
c ---[2590]---> BDD-cost:  133
c ---[2589]---> BDD-cost:  133
c ---[2588]---> BDD-cost:  137
c ---[2585]---> BDD-cost:  137
c ---[2584]---> BDD-cost:  138
c ---[2583]---> BDD-cost:  138
c ---[2582]---> BDD-cost:  137
c ---[2581]---> BDD-cost:  137
c ---[2580]---> BDD-cost:  146
c ---[2579]---> BDD-cost:  146
c ---[2578]---> BDD-cost:  137
c ---[2577]---> BDD-cost:  137
c ---[2576]---> BDD-cost:  143
c ---[2574]---> BDD-cost:  143
c ---[2573]---> BDD-cost:  137
c ---[2572]---> BDD-cost:  137
c ---[2571]---> BDD-cost:  143
c ---[2570]---> BDD-cost:  143
c ---[2569]---> BDD-cost:  137
c ---[2568]---> BDD-cost:  137
c ---[2567]---> BDD-cost:  143
c ---[2566]---> BDD-cost:  143
c ---[2565]---> BDD-cost:  137
c ---[2563]---> BDD-cost:  137
c ---[2562]---> BDD-cost:  138
c ---[2561]---> BDD-cost:  138
c ---[2560]---> BDD-cost:  137
c ---[2559]---> BDD-cost:  137
c ---[2558]---> BDD-cost:  140
c ---[2557]---> BDD-cost:  140
c ---[2556]---> BDD-cost:  137
c ---[2555]---> BDD-cost:  137
c ---[2554]---> BDD-cost:  143
c ---[2552]---> BDD-cost:  143
c ---[2551]---> BDD-cost:  137
c ---[2550]---> BDD-cost:  137
c ---[2549]---> BDD-cost:  141
c ---[2548]---> BDD-cost:  141
c ---[2547]---> BDD-cost:  137
c ---[2546]---> BDD-cost:  137
c ---[2545]---> BDD-cost:  140
c ---[2544]---> BDD-cost:  140
c ---[2543]---> BDD-cost:  137
c ---[2541]---> BDD-cost:  137
c ---[2540]---> BDD-cost:  140
c ---[2539]---> BDD-cost:  140
c ---[2538]---> BDD-cost:  137
c ---[2537]---> BDD-cost:  137
c ---[2536]---> BDD-cost:  143
c ---[2535]---> BDD-cost:  143
c ---[2534]---> BDD-cost:  137
c ---[2533]---> BDD-cost:  137
c ---[2532]---> BDD-cost:  140
c ---[2530]---> BDD-cost:  140
c ---[2529]---> BDD-cost:  137
c ---[2528]---> BDD-cost:  137
c ---[2527]---> BDD-cost:  140
c ---[2526]---> BDD-cost:  140
c ---[2525]---> BDD-cost:  137
c ---[2524]---> BDD-cost:  137
c ---[2523]---> BDD-cost:  140
c ---[2522]---> BDD-cost:  140
c ---[2521]---> BDD-cost:  137
c ---[2519]---> BDD-cost:  137
c ---[2518]---> BDD-cost:  143
c ---[2517]---> BDD-cost:  143
c ---[2516]---> BDD-cost:  137
c ---[2515]---> BDD-cost:  137
c ---[2514]---> BDD-cost:  140
c ---[2513]---> BDD-cost:  140
c ---[2512]---> BDD-cost:  137
c ---[2511]---> BDD-cost:  137
c ---[2510]---> BDD-cost:  140
c ---[2508]---> BDD-cost:  140
c ---[2507]---> BDD-cost:  137
c ---[2506]---> BDD-cost:  137
c ---[2505]---> BDD-cost:  143
c ---[2504]---> BDD-cost:  143
c ---[2503]---> BDD-cost:  137
c ---[2502]---> BDD-cost:  137
c ---[2501]---> BDD-cost:  143
c ---[2500]---> BDD-cost:  143
c ---[2499]---> BDD-cost:  137
c ---[2497]---> BDD-cost:  137
c ---[2496]---> BDD-cost:  143
c ---[2495]---> BDD-cost:  143
c ---[2494]---> BDD-cost:  137
c ---[2493]---> BDD-cost:  137
c ---[2492]---> BDD-cost:  140
c ---[2491]---> BDD-cost:  140
c ---[2490]---> BDD-cost:  137
c ---[2489]---> BDD-cost:  137
c ---[2488]---> BDD-cost:  143
c ---[2486]---> BDD-cost:  143
c ---[2485]---> BDD-cost:  137
c ---[2484]---> BDD-cost:  137
c ---[2483]---> BDD-cost:  140
c ---[2482]---> BDD-cost:  140
c ---[2481]---> BDD-cost:  137
c ---[2480]---> BDD-cost:  137
c ---[2479]---> BDD-cost:  128
c ---[2478]---> BDD-cost:  128
c ---[2477]---> BDD-cost:  137
c ---[2474]---> BDD-cost:  137
c ---[2473]---> BDD-cost:  138
c ---[2472]---> BDD-cost:  138
c ---[2471]---> BDD-cost:  137
c ---[2470]---> BDD-cost:  137
c ---[2469]---> BDD-cost:  133
c ---[2468]---> BDD-cost:  133
c ---[2467]---> BDD-cost:  137
c ---[2466]---> BDD-cost:  137
c ---[2465]---> BDD-cost:  140
c ---[2463]---> BDD-cost:  140
c ---[2462]---> BDD-cost:  137
c ---[2461]---> BDD-cost:  137
c ---[2460]---> BDD-cost:  140
c ---[2459]---> BDD-cost:  140
c ---[2458]---> BDD-cost:  137
c ---[2457]---> BDD-cost:  137
c ---[2456]---> BDD-cost:  140
c ---[2455]---> BDD-cost:  140
c ---[2454]---> BDD-cost:  137
c ---[2452]---> BDD-cost:  137
c ---[2451]---> BDD-cost:  140
c ---[2450]---> BDD-cost:  140
c ---[2449]---> BDD-cost:  137
c ---[2448]---> BDD-cost:  137
c ---[2447]---> BDD-cost:  137
c ---[2446]---> BDD-cost:  137
c ---[2445]---> BDD-cost:  137
c ---[2444]---> BDD-cost:  137
c ---[2443]---> BDD-cost:  143
c ---[2441]---> BDD-cost:  143
c ---[2440]---> BDD-cost:  137
c ---[2439]---> BDD-cost:  137
c ---[2438]---> BDD-cost:  143
c ---[2437]---> BDD-cost:  143
c ---[2436]---> BDD-cost:  137
c ---[2435]---> BDD-cost:  137
c ---[2434]---> BDD-cost:  141
c ---[2433]---> BDD-cost:  141
c ---[2432]---> BDD-cost:  137
c ---[2430]---> BDD-cost:  137
c ---[2429]---> BDD-cost:  140
c ---[2428]---> BDD-cost:  140
c ---[2427]---> BDD-cost:  137
c ---[2426]---> BDD-cost:  137
c ---[2425]---> BDD-cost:  126
c ---[2424]---> BDD-cost:  126
c ---[2423]---> BDD-cost:  137
c ---[2422]---> BDD-cost:  137
c ---[2421]---> BDD-cost:  135
c ---[2419]---> BDD-cost:  135
c ---[2418]---> BDD-cost:  137
c ---[2417]---> BDD-cost:  137
c ---[2416]---> BDD-cost:  140
c ---[2415]---> BDD-cost:  140
c ---[2414]---> BDD-cost:  137
c ---[2413]---> BDD-cost:  137
c ---[2412]---> BDD-cost:  135
c ---[2411]---> BDD-cost:  135
c ---[2410]---> BDD-cost:  137
c ---[2408]---> BDD-cost:  137
c ---[2407]---> BDD-cost:  135
c ---[2406]---> BDD-cost:  135
c ---[2405]---> BDD-cost:  137
c ---[2404]---> BDD-cost:  137
c ---[2403]---> BDD-cost:  143
c ---[2402]---> BDD-cost:  143
c ---[2401]---> BDD-cost:  137
c ---[2400]---> BDD-cost:  137
c ---[2399]---> BDD-cost:  138
c ---[2397]---> BDD-cost:  138
c ---[2396]---> BDD-cost:  137
c ---[2395]---> BDD-cost:  137
c ---[2394]---> BDD-cost:  135
c ---[2393]---> BDD-cost:  135
c ---[2392]---> BDD-cost:  137
c ---[2391]---> BDD-cost:  137
c ---[2390]---> BDD-cost:  136
c ---[2389]---> BDD-cost:  136
c ---[2388]---> BDD-cost:  137
c ---[2386]---> BDD-cost:  137
c ---[2385]---> BDD-cost:  146
c ---[2384]---> BDD-cost:  146
c ---[2383]---> BDD-cost:  137
c ---[2382]---> BDD-cost:  137
c ---[2381]---> BDD-cost:  138
c ---[2380]---> BDD-cost:  138
c ---[2379]---> BDD-cost:  137
c ---[2378]---> BDD-cost:  137
c ---[2377]---> BDD-cost:  143
c ---[2375]---> BDD-cost:  143
c ---[2374]---> BDD-cost:  137
c ---[2373]---> BDD-cost:  137
c ---[2372]---> BDD-cost:  123
c ---[2371]---> BDD-cost:  123
c ---[2370]---> BDD-cost:  137
c ---[2369]---> BDD-cost:  137
c ---[2368]---> BDD-cost:  146
c ---[2367]---> BDD-cost:  146
c ---[2366]---> BDD-cost:  137
c ---[2363]---> BDD-cost:  137
c ---[2362]---> BDD-cost:  143
c ---[2361]---> BDD-cost:  143
c ---[2360]---> BDD-cost:  137
c ---[2359]---> BDD-cost:  137
c ---[2358]---> BDD-cost:  140
c ---[2357]---> BDD-cost:  140
c ---[2356]---> BDD-cost:  137
c ---[2355]---> BDD-cost:  137
c ---[2354]---> BDD-cost:  128
c ---[2352]---> BDD-cost:  128
c ---[2351]---> BDD-cost:  137
c ---[2350]---> BDD-cost:  137
c ---[2349]---> BDD-cost:  143
c ---[2348]---> BDD-cost:  143
c ---[2347]---> BDD-cost:  137
c ---[2346]---> BDD-cost:  137
c ---[2345]---> BDD-cost:  133
c ---[2344]---> BDD-cost:  133
c ---[2343]---> BDD-cost:  137
c ---[2341]---> BDD-cost:  137
c ---[2340]---> BDD-cost:  141
c ---[2339]---> BDD-cost:  141
c ---[2338]---> BDD-cost:  137
c ---[2337]---> BDD-cost:  137
c ---[2336]---> BDD-cost:  138
c ---[2335]---> BDD-cost:  138
c ---[2334]---> BDD-cost:  137
c ---[2333]---> BDD-cost:  137
c ---[2332]---> BDD-cost:  125
c ---[2330]---> BDD-cost:  125
c ---[2329]---> BDD-cost:  137
c ---[2328]---> BDD-cost:  137
c ---[2327]---> BDD-cost:  143
c ---[2326]---> BDD-cost:  143
c ---[2325]---> BDD-cost:  137
c ---[2324]---> BDD-cost:  137
c ---[2323]---> BDD-cost:  143
c ---[2322]---> BDD-cost:  143
c ---[2321]---> BDD-cost:  137
c ---[2319]---> BDD-cost:  137
c ---[2318]---> BDD-cost:  143
c ---[2317]---> BDD-cost:  143
c ---[2316]---> BDD-cost:  137
c ---[2315]---> BDD-cost:  137
c ---[2314]---> BDD-cost:  135
c ---[2313]---> BDD-cost:  135
c ---[2312]---> BDD-cost:  137
c ---[2311]---> BDD-cost:  137
c ---[2310]---> BDD-cost:  140
c ---[2308]---> BDD-cost:  140
c ---[2307]---> BDD-cost:  137
c ---[2306]---> BDD-cost:  137
c ---[2305]---> BDD-cost:  128
c ---[2304]---> BDD-cost:  128
c ---[2303]---> BDD-cost:  137
c ---[2302]---> BDD-cost:  137
c ---[2301]---> BDD-cost:  143
c ---[2300]---> BDD-cost:  143
c ---[2299]---> BDD-cost:  137
c ---[2297]---> BDD-cost:  137
c ---[2296]---> BDD-cost:  138
c ---[2295]---> BDD-cost:  138
c ---[2294]---> BDD-cost:  137
c ---[2293]---> BDD-cost:  137
c ---[2292]---> BDD-cost:  123
c ---[2291]---> BDD-cost:  123
c ---[2290]---> BDD-cost:  137
c ---[2289]---> BDD-cost:  137
c ---[2288]---> BDD-cost:  140
c ---[2286]---> BDD-cost:  140
c ---[2285]---> BDD-cost:  137
c ---[2284]---> BDD-cost:  137
c ---[2283]---> BDD-cost:  140
c ---[2282]---> BDD-cost:  140
c ---[2281]---> BDD-cost:  137
c ---[2280]---> BDD-cost:  137
c ---[2279]---> BDD-cost:  140
c ---[2278]---> BDD-cost:  140
c ---[2277]---> BDD-cost:  137
c ---[2275]---> BDD-cost:  137
c ---[2274]---> BDD-cost:  135
c ---[2273]---> BDD-cost:  135
c ---[2272]---> BDD-cost:  137
c ---[2271]---> BDD-cost:  137
c ---[2270]---> BDD-cost:  138
c ---[2269]---> BDD-cost:  138
c ---[2268]---> BDD-cost:  137
c ---[2267]---> BDD-cost:  137
c ---[2266]---> BDD-cost:  143
c ---[2264]---> BDD-cost:  143
c ---[2263]---> BDD-cost:  137
c ---[2262]---> BDD-cost:  137
c ---[2261]---> BDD-cost:  138
c ---[2260]---> BDD-cost:  138
c ---[2259]---> BDD-cost:  137
c ---[2258]---> BDD-cost:  137
c ---[2257]---> BDD-cost:  143
c ---[2256]---> BDD-cost:  143
c ---[2255]---> BDD-cost:  137
c ---[2252]---> BDD-cost:  137
c ---[2251]---> BDD-cost:  143
c ---[2250]---> BDD-cost:  143
c ---[2249]---> BDD-cost:  137
c ---[2248]---> BDD-cost:  137
c ---[2247]---> BDD-cost:  128
c ---[2246]---> BDD-cost:  128
c ---[2245]---> BDD-cost:  137
c ---[2244]---> BDD-cost:  137
c ---[2243]---> BDD-cost:  143
c ---[2241]---> BDD-cost:  143
c ---[2240]---> BDD-cost:  137
c ---[2239]---> BDD-cost:  137
c ---[2238]---> BDD-cost:  133
c ---[2237]---> BDD-cost:  133
c ---[2236]---> BDD-cost:  137
c ---[2235]---> BDD-cost:  137
c ---[2234]---> BDD-cost:  140
c ---[2233]---> BDD-cost:  140
c ---[2232]---> BDD-cost:  137
c ---[2230]---> BDD-cost:  137
c ---[2229]---> BDD-cost:  130
c ---[2228]---> BDD-cost:  130
c ---[2227]---> BDD-cost:  137
c ---[2226]---> BDD-cost:  137
c ---[2225]---> BDD-cost:  140
c ---[2224]---> BDD-cost:  140
c ---[2223]---> BDD-cost:  137
c ---[2222]---> BDD-cost:  137
c ---[2221]---> BDD-cost:  133
c ---[2219]---> BDD-cost:  133
c ---[2218]---> BDD-cost:  137
c ---[2217]---> BDD-cost:  137
c ---[2216]---> BDD-cost:  118
c ---[2215]---> BDD-cost:  118
c ---[2214]---> BDD-cost:  137
c ---[2213]---> BDD-cost:  137
c ---[2212]---> BDD-cost:  140
c ---[2211]---> BDD-cost:  140
c ---[2210]---> BDD-cost:  137
c ---[2208]---> BDD-cost:  137
c ---[2207]---> BDD-cost:  143
c ---[2206]---> BDD-cost:  143
c ---[2205]---> BDD-cost:  137
c ---[2204]---> BDD-cost:  137
c ---[2203]---> BDD-cost:  140
c ---[2202]---> BDD-cost:  140
c ---[2201]---> BDD-cost:  137
c ---[2200]---> BDD-cost:  137
c ---[2199]---> BDD-cost:  140
c ---[2197]---> BDD-cost:  140
c ---[2196]---> BDD-cost:  137
c ---[2195]---> BDD-cost:  137
c ---[2194]---> BDD-cost:  143
c ---[2193]---> BDD-cost:  143
c ---[2192]---> BDD-cost:  137
c ---[2191]---> BDD-cost:  137
c ---[2190]---> BDD-cost:  143
c ---[2189]---> BDD-cost:  143
c ---[2188]---> BDD-cost:  137
c ---[2186]---> BDD-cost:  137
c ---[2185]---> BDD-cost:  135
c ---[2184]---> BDD-cost:  135
c ---[2183]---> BDD-cost:  137
c ---[2182]---> BDD-cost:  137
c ---[2181]---> BDD-cost:  134
c ---[2180]---> BDD-cost:  143
c ---[2179]---> BDD-cost:  129
c ---[2178]---> BDD-cost:  136
c ---[2177]---> BDD-cost:  124
c ---[2175]---> BDD-cost:  141
c ---[2174]---> BDD-cost:  126
c ---[2173]---> BDD-cost:  138
c ---[2172]---> BDD-cost:  124
c ---[2171]---> BDD-cost:  143
c ---[2170]---> BDD-cost:  137
c ---[2169]---> BDD-cost:  125
c ---[2168]---> BDD-cost:  129
c ---[2167]---> BDD-cost:  140
c ---[2166]---> BDD-cost:  134
c ---[2164]---> BDD-cost:  140
c ---[2163]---> BDD-cost:  132
c ---[2162]---> BDD-cost:  140
c ---[2161]---> BDD-cost:  132
c ---[2160]---> BDD-cost:  143
c ---[2159]---> BDD-cost:  132
c ---[2158]---> BDD-cost:  135
c ---[2157]---> BDD-cost:  132
c ---[2156]---> BDD-cost:  137
c ---[2155]---> BDD-cost:  126
c ---[2153]---> BDD-cost:  143
c ---[2152]---> BDD-cost:  132
c ---[2151]---> BDD-cost:  135
c ---[2150]---> BDD-cost:  127
c ---[2149]---> BDD-cost:  143
c ---[2148]---> BDD-cost:  137
c ---[2147]---> BDD-cost:  143
c ---[2146]---> BDD-cost:  120
c ---[2145]---> BDD-cost:  146
c ---[2144]---> BDD-cost:  132
c ---[2141]---> BDD-cost:  136
c ---[2140]---> BDD-cost:  132
c ---[2139]---> BDD-cost:  135
c ---[2138]---> BDD-cost:  137
c ---[2137]---> BDD-cost:  143
c ---[2136]---> BDD-cost:  124
c ---[2135]---> BDD-cost:  143
c ---[2134]---> BDD-cost:  131
c ---[2133]---> BDD-cost:  132
c ---[2132]---> BDD-cost:  124
c ---[2130]---> BDD-cost:  133
c ---[2129]---> BDD-cost:  126
c ---[2128]---> BDD-cost:  140
c ---[2127]---> BDD-cost:  120
c ---[2126]---> BDD-cost:  123
c ---[2125]---> BDD-cost:  126
c ---[2124]---> BDD-cost:  141
c ---[2123]---> BDD-cost:  137
c ---[2122]---> BDD-cost:  128
c ---[2121]---> BDD-cost:  137
c ---[2119]---> BDD-cost:  146
c ---[2118]---> BDD-cost:  132
c ---[2117]---> BDD-cost:  146
c ---[2116]---> BDD-cost:  120
c ---[2115]---> BDD-cost:  140
c ---[2114]---> BDD-cost:  137
c ---[2113]---> BDD-cost:  143
c ---[2112]---> BDD-cost:  137
c ---[2111]---> BDD-cost:  138
c ---[2110]---> BDD-cost:  137
c ---[2108]---> BDD-cost:  138
c ---[2107]---> BDD-cost:  132
c ---[2106]---> BDD-cost:  143
c ---[2105]---> BDD-cost:  134
c ---[2104]---> BDD-cost:  137
c ---[2103]---> BDD-cost:  137
c ---[2102]---> BDD-cost:  116
c ---[2101]---> BDD-cost:  134
c ---[2100]---> BDD-cost:  141
c ---[2099]---> BDD-cost:  122
c ---[2097]---> BDD-cost:  135
c ---[2096]---> BDD-cost:  120
c ---[2095]---> BDD-cost:  143
c ---[2094]---> BDD-cost:  137
c ---[2093]---> BDD-cost:  143
c ---[2092]---> BDD-cost:  126
c ---[2091]---> BDD-cost:  125
c ---[2090]---> BDD-cost:  124
c ---[2089]---> BDD-cost:  140
c ---[2088]---> BDD-cost:  131
c ---[2086]---> BDD-cost:  133
c ---[2085]---> BDD-cost:  127
c ---[2084]---> BDD-cost:  126
c ---[2083]---> BDD-cost:  127
c ---[2082]---> BDD-cost:  143
c ---[2081]---> BDD-cost:  122
c ---[2080]---> BDD-cost:  143
c ---[2079]---> BDD-cost:  132
c ---[2078]---> BDD-cost:  137
c ---[2077]---> BDD-cost:  134
c ---[2075]---> BDD-cost:  134
c ---[2074]---> BDD-cost:  126
c ---[2073]---> BDD-cost:  143
c ---[2072]---> BDD-cost:  124
c ---[2071]---> BDD-cost:  120
c ---[2070]---> BDD-cost:  127
c ---[2069]---> BDD-cost:  143
c ---[2068]---> BDD-cost:  120
c ---[2067]---> BDD-cost:  138
c ---[2066]---> BDD-cost:  137
c ---[2064]---> BDD-cost:  140
c ---[2063]---> BDD-cost:  129
c ---[2062]---> BDD-cost:  138
c ---[2061]---> BDD-cost:  126
c ---[2060]---> BDD-cost:  143
c ---[2059]---> BDD-cost:  131
c ---[2058]---> BDD-cost:  143
c ---[2057]---> BDD-cost:  129
c ---[2056]---> BDD-cost:  140
c ---[2055]---> BDD-cost:  131
c ---[2053]---> BDD-cost:  143
c ---[2052]---> BDD-cost:  131
c ---[2051]---> BDD-cost:  123
c ---[2050]---> BDD-cost:  140
c ---[2049]---> BDD-cost:  140
c ---[2048]---> BDD-cost:  135
c ---[2047]---> BDD-cost:  129
c ---[2046]---> BDD-cost:  143
c ---[2045]---> BDD-cost:  122
c ---[2044]---> BDD-cost:  133
c ---[2042]---> BDD-cost:  137
c ---[2041]---> BDD-cost:  141
c ---[2040]---> BDD-cost:  134
c ---[2039]---> BDD-cost:  143
c ---[2038]---> BDD-cost:  120
c ---[2037]---> BDD-cost:  125
c ---[2036]---> BDD-cost:  137
c ---[2035]---> BDD-cost:  133
c ---[2034]---> BDD-cost:  137
c ---[2033]---> BDD-cost:  131
c ---[2029]---> BDD-cost:  131
c ---[2028]---> BDD-cost:  137
c ---[2027]---> BDD-cost:  124
c ---[2026]---> BDD-cost:  136
c ---[2025]---> BDD-cost:  127
c ---[2024]---> BDD-cost:  133
c ---[2023]---> BDD-cost:  127
c ---[2022]---> BDD-cost:  146
c ---[2021]---> BDD-cost:  132
c ---[2020]---> BDD-cost:  141
c ---[2018]---> BDD-cost:  132
c ---[2017]---> BDD-cost:  130
c ---[2016]---> BDD-cost:  137
c ---[2015]---> BDD-cost:  140
c ---[2014]---> BDD-cost:  129
c ---[2013]---> BDD-cost:  143
c ---[2012]---> BDD-cost:  132
c ---[2011]---> BDD-cost:  138
c ---[2010]---> BDD-cost:  129
c ---[2009]---> BDD-cost:  136
c ---[2007]---> BDD-cost:  137
c ---[2006]---> BDD-cost:  138
c ---[2005]---> BDD-cost:  137
c ---[2004]---> BDD-cost:  146
c ---[2003]---> BDD-cost:  132
c ---[2002]---> BDD-cost:  146
c ---[2001]---> BDD-cost:  137
c ---[2000]---> BDD-cost:  141
c ---[1999]---> BDD-cost:  137
c ---[1998]---> BDD-cost:  123
c ---[1996]---> BDD-cost:  120
c ---[1995]---> BDD-cost:  143
c ---[1994]---> BDD-cost:  134
c ---[1993]---> BDD-cost:  146
c ---[1992]---> BDD-cost:  124
c ---[1991]---> BDD-cost:  130
c ---[1990]---> BDD-cost:  134
c ---[1989]---> BDD-cost:  141
c ---[1988]---> BDD-cost:  137
c ---[1987]---> BDD-cost:  141
c ---[1985]---> BDD-cost:  132
c ---[1984]---> BDD-cost:  141
c ---[1983]---> BDD-cost:  132
c ---[1982]---> BDD-cost:  146
c ---[1981]---> BDD-cost:  137
c ---[1980]---> BDD-cost:  146
c ---[1979]---> BDD-cost:  140
c ---[1978]---> BDD-cost:  140
c ---[1977]---> BDD-cost:  143
c ---[1976]---> BDD-cost:  120
c ---[1974]---> BDD-cost:  138
c ---[1973]---> BDD-cost:  134
c ---[1972]---> BDD-cost:  131
c ---[1971]---> BDD-cost:  129
c ---[1970]---> BDD-cost:  143
c ---[1969]---> BDD-cost:  134
c ---[1968]---> BDD-cost:  146
c ---[1967]---> BDD-cost:  137
c ---[1966]---> BDD-cost:  146
c ---[1965]---> BDD-cost:  120
c ---[1963]---> BDD-cost:  146
c ---[1962]---> BDD-cost:  122
c ---[1961]---> BDD-cost:  141
c ---[1960]---> BDD-cost:  140
c ---[1959]---> BDD-cost:  140
c ---[1958]---> BDD-cost:  141
c ---[1957]---> BDD-cost:  120
c ---[1956]---> BDD-cost:  138
c ---[1955]---> BDD-cost:  134
c ---[1954]---> BDD-cost:  132
c ---[1952]---> BDD-cost:  129
c ---[1951]---> BDD-cost:  143
c ---[1950]---> BDD-cost:  134
c ---[1949]---> BDD-cost:  134
c ---[1948]---> BDD-cost:  137
c ---[1947]---> BDD-cost:  146
c ---[1946]---> BDD-cost:  120
c ---[1945]---> BDD-cost:  137
c ---[1944]---> BDD-cost:  122
c ---[1943]---> BDD-cost:  128
c ---[1941]---> BDD-cost:  140
c ---[1940]---> BDD-cost:  140
c ---[1939]---> BDD-cost:  138
c ---[1938]---> BDD-cost:  131
c ---[1937]---> BDD-cost:  140
c ---[1936]---> BDD-cost:  124
c ---[1935]---> BDD-cost:  138
c ---[1934]---> BDD-cost:  131
c ---[1933]---> BDD-cost:  132
c ---[1932]---> BDD-cost:  120
c ---[1930]---> BDD-cost:  126
c ---[1929]---> BDD-cost:  120
c ---[1928]---> BDD-cost:  138
c ---[1927]---> BDD-cost:  132
c ---[1926]---> BDD-cost:  146
c ---[1925]---> BDD-cost:  137
c ---[1924]---> BDD-cost:  143
c ---[1923]---> BDD-cost:  137
c ---[1922]---> BDD-cost:  138
c ---[1921]---> BDD-cost:  126
c ---[1918]---> BDD-cost:  146
c ---[1917]---> BDD-cost:  137
c ---[1916]---> BDD-cost:  143
c ---[1915]---> BDD-cost:  137
c ---[1914]---> BDD-cost:  131
c ---[1913]---> BDD-cost:  132
c ---[1912]---> BDD-cost:  138
c ---[1911]---> BDD-cost:  126
c ---[1910]---> BDD-cost:  125
c ---[1909]---> BDD-cost:  131
c ---[1907]---> BDD-cost:  130
c ---[1906]---> BDD-cost:  137
c ---[1905]---> BDD-cost:  134
c ---[1904]---> BDD-cost:  140
c ---[1903]---> BDD-cost:  140
c ---[1902]---> BDD-cost:  143
c ---[1901]---> BDD-cost:  137
c ---[1900]---> BDD-cost:  130
c ---[1899]---> BDD-cost:  124
c ---[1898]---> BDD-cost:  138
c ---[1896]---> BDD-cost:  122
c ---[1895]---> BDD-cost:  138
c ---[1894]---> BDD-cost:  129
c ---[1893]---> BDD-cost:  118
c ---[1892]---> BDD-cost:  137
c ---[1891]---> BDD-cost:  143
c ---[1890]---> BDD-cost:  120
c ---[1889]---> BDD-cost:  146
c ---[1888]---> BDD-cost:  126
c ---[1887]---> BDD-cost:  143
c ---[1885]---> BDD-cost:  124
c ---[1884]---> BDD-cost:  143
c ---[1883]---> BDD-cost:  120
c ---[1882]---> BDD-cost:  138
c ---[1881]---> BDD-cost:  137
c ---[1880]---> BDD-cost:  143
c ---[1879]---> BDD-cost:  131
c ---[1878]---> BDD-cost:  146
c ---[1877]---> BDD-cost:  124
c ---[1876]---> BDD-cost:  140
c ---[1874]---> BDD-cost:  131
c ---[1873]---> BDD-cost:  143
c ---[1872]---> BDD-cost:  140
c ---[1871]---> BDD-cost:  140
c ---[1870]---> BDD-cost:  136
c ---[1869]---> BDD-cost:  132
c ---[1868]---> BDD-cost:  146
c ---[1867]---> BDD-cost:  126
c ---[1866]---> BDD-cost:  143
c ---[1865]---> BDD-cost:  137
c ---[1863]---> BDD-cost:  135
c ---[1862]---> BDD-cost:  129
c ---[1861]---> BDD-cost:  140
c ---[1860]---> BDD-cost:  137
c ---[1859]---> BDD-cost:  120
c ---[1858]---> BDD-cost:  127
c ---[1857]---> BDD-cost:  130
c ---[1856]---> BDD-cost:  137
c ---[1855]---> BDD-cost:  135
c ---[1854]---> BDD-cost:  129
c ---[1852]---> BDD-cost:  140
c ---[1851]---> BDD-cost:  134
c ---[1850]---> BDD-cost:  135
c ---[1849]---> BDD-cost:  129
c ---[1848]---> BDD-cost:  132
c ---[1847]---> BDD-cost:  132
c ---[1846]---> BDD-cost:  128
c ---[1845]---> BDD-cost:  137
c ---[1844]---> BDD-cost:  135
c ---[1843]---> BDD-cost:  137
c ---[1841]---> BDD-cost:  143
c ---[1840]---> BDD-cost:  120
c ---[1839]---> BDD-cost:  143
c ---[1838]---> BDD-cost:  131
c ---[1837]---> BDD-cost:  135
c ---[1836]---> BDD-cost:  132
c ---[1835]---> BDD-cost:  140
c ---[1834]---> BDD-cost:  122
c ---[1833]---> BDD-cost:  124
c ---[1832]---> BDD-cost:  131
c ---[1830]---> BDD-cost:  127
c ---[1829]---> BDD-cost:  137
c ---[1828]---> BDD-cost:  135
c ---[1827]---> BDD-cost:  120
c ---[1826]---> BDD-cost:  134
c ---[1825]---> BDD-cost:  137
c ---[1824]---> BDD-cost:  132
c ---[1823]---> BDD-cost:  129
c ---[1822]---> BDD-cost:  129
c ---[1821]---> BDD-cost:  120
c ---[1819]---> BDD-cost:  122
c ---[1818]---> BDD-cost:  137
c ---[1817]---> BDD-cost:  132
c ---[1816]---> BDD-cost:  127
c ---[1815]---> BDD-cost:  140
c ---[1814]---> BDD-cost:  120
c ---[1813]---> BDD-cost:  130
c ---[1812]---> BDD-cost:  137
c ---[1811]---> BDD-cost:  135
c ---[1810]---> BDD-cost:  137
c ---[1807]---> BDD-cost:  140
c ---[1806]---> BDD-cost:  132
c ---[1805]---> BDD-cost:  140
c ---[1804]---> BDD-cost:  132
c ---[1803]---> BDD-cost:  140
c ---[1802]---> BDD-cost:  126
c ---[1801]---> BDD-cost:  135
c ---[1800]---> BDD-cost:  122
c ---[1799]---> BDD-cost:  133
c ---[1798]---> BDD-cost:  132
c ---[1796]---> BDD-cost:  130
c ---[1795]---> BDD-cost:  137
c ---[1794]---> BDD-cost:  130
c ---[1793]---> BDD-cost:  124
c ---[1792]---> BDD-cost:  135
c ---[1791]---> BDD-cost:  137
c ---[1790]---> BDD-cost:  124
c ---[1789]---> BDD-cost:  132
c ---[1788]---> BDD-cost:  128
c ---[1787]---> BDD-cost:  124
c ---[1785]---> BDD-cost:  134
c ---[1784]---> BDD-cost:  134
c ---[1783]---> BDD-cost:  134
c ---[1782]---> BDD-cost:  134
c ---[1781]---> BDD-cost:  143
c ---[1780]---> BDD-cost:  131
c ---[1779]---> BDD-cost:  141
c ---[1778]---> BDD-cost:  124
c ---[1777]---> BDD-cost:  133
c ---[1776]---> BDD-cost:  134
c ---[1774]---> BDD-cost:  133
c ---[1773]---> BDD-cost:  124
c ---[1772]---> BDD-cost:  133
c ---[1771]---> BDD-cost:  137
c ---[1770]---> BDD-cost:  134
c ---[1769]---> BDD-cost:  137
c ---[1768]---> BDD-cost:  140
c ---[1767]---> BDD-cost:  137
c ---[1766]---> BDD-cost:  140
c ---[1765]---> BDD-cost:  134
c ---[1763]---> BDD-cost:  127
c ---[1762]---> BDD-cost:  137
c ---[1761]---> BDD-cost:  143
c ---[1760]---> BDD-cost:  131
c ---[1759]---> BDD-cost:  132
c ---[1758]---> BDD-cost:  122
c ---[1757]---> BDD-cost:  146
c ---[1756]---> BDD-cost:  122
c ---[1755]---> BDD-cost:  144
c ---[1754]---> BDD-cost:  127
c ---[1752]---> BDD-cost:  138
c ---[1751]---> BDD-cost:  131
c ---[1750]---> BDD-cost:  146
c ---[1749]---> BDD-cost:  120
c ---[1748]---> BDD-cost:  134
c ---[1747]---> BDD-cost:  132
c ---[1746]---> BDD-cost:  131
c ---[1745]---> BDD-cost:  137
c ---[1744]---> BDD-cost:  136
c ---[1743]---> BDD-cost:  136
c ---[1741]---> BDD-cost:  137
c ---[1740]---> BDD-cost:  122
c ---[1739]---> BDD-cost:  124
c ---[1738]---> BDD-cost:  138
c ---[1737]---> BDD-cost:  126
c ---[1736]---> BDD-cost:  143
c ---[1735]---> BDD-cost:  132
c ---[1734]---> BDD-cost:  140
c ---[1733]---> BDD-cost:  137
c ---[1732]---> BDD-cost:  137
c ---[1730]---> BDD-cost:  137
c ---[1729]---> BDD-cost:  129
c ---[1728]---> BDD-cost:  127
c ---[1727]---> BDD-cost:  129
c ---[1726]---> BDD-cost:  127
c ---[1725]---> BDD-cost:  133
c ---[1724]---> BDD-cost:  140
c ---[1723]---> BDD-cost:  140
c ---[1722]---> BDD-cost:  138
c ---[1721]---> BDD-cost:  126
c ---[1719]---> BDD-cost:  130
c ---[1718]---> BDD-cost:  131
c ---[1717]---> BDD-cost:  130
c ---[1716]---> BDD-cost:  122
c ---[1715]---> BDD-cost:  138
c ---[1714]---> BDD-cost:  134
c ---[1713]---> BDD-cost:  146
c ---[1712]---> BDD-cost:  134
c ---[1711]---> BDD-cost:  128
c ---[1710]---> BDD-cost:  134
c ---[1708]---> BDD-cost:  120
c ---[1707]---> BDD-cost:  124
c ---[1706]---> BDD-cost:  138
c ---[1705]---> BDD-cost:  137
c ---[1704]---> BDD-cost:  135
c ---[1703]---> BDD-cost:  137
c ---[1702]---> BDD-cost:  140
c ---[1701]---> BDD-cost:  137
c ---[1700]---> BDD-cost:  128
c ---[1699]---> BDD-cost:  126
c ---[1696]---> BDD-cost:  140
c ---[1695]---> BDD-cost:  134
c ---[1694]---> BDD-cost:  140
c ---[1693]---> BDD-cost:  126
c ---[1692]---> BDD-cost:  135
c ---[1691]---> BDD-cost:  120
c ---[1690]---> BDD-cost:  146
c ---[1689]---> BDD-cost:  120
c ---[1688]---> BDD-cost:  137
c ---[1687]---> BDD-cost:  137
c ---[1685]---> BDD-cost:  143
c ---[1684]---> BDD-cost:  140
c ---[1683]---> BDD-cost:  140
c ---[1682]---> BDD-cost:  137
c ---[1681]---> BDD-cost:  132
c ---[1680]---> BDD-cost:  143
c ---[1679]---> BDD-cost:  137
c ---[1678]---> BDD-cost:  140
c ---[1677]---> BDD-cost:  131
c ---[1676]---> BDD-cost:  141
c ---[1674]---> BDD-cost:  127
c ---[1673]---> BDD-cost:  138
c ---[1672]---> BDD-cost:  134
c ---[1671]---> BDD-cost:  140
c ---[1670]---> BDD-cost:  132
c ---[1669]---> BDD-cost:  124
c ---[1668]---> BDD-cost:  140
c ---[1667]---> BDD-cost:  140
c ---[1666]---> BDD-cost:  136
c ---[1665]---> BDD-cost:  137
c ---[1663]---> BDD-cost:  127
c ---[1662]---> BDD-cost:  122
c ---[1661]---> BDD-cost:  129
c ---[1660]---> BDD-cost:  137
c ---[1659]---> BDD-cost:  146
c ---[1658]---> BDD-cost:  122
c ---[1657]---> BDD-cost:  143
c ---[1656]---> BDD-cost:  120
c ---[1655]---> BDD-cost:  133
c ---[1654]---> BDD-cost:  132
c ---[1652]---> BDD-cost:  141
c ---[1651]---> BDD-cost:  141
c ---[1650]---> BDD-cost:  131
c ---[1649]---> BDD-cost:  146
c ---[1648]---> BDD-cost:  131
c ---[1647]---> BDD-cost:  143
c ---[1646]---> BDD-cost:  126
c ---[1645]---> BDD-cost:  143
c ---[1644]---> BDD-cost:  132
c ---[1643]---> BDD-cost:  128
c ---[1641]---> BDD-cost:  129
c ---[1640]---> BDD-cost:  135
c ---[1639]---> BDD-cost:  129
c ---[1638]---> BDD-cost:  140
c ---[1637]---> BDD-cost:  124
c ---[1636]---> BDD-cost:  143
c ---[1635]---> BDD-cost:  134
c ---[1634]---> BDD-cost:  134
c ---[1633]---> BDD-cost:  126
c ---[1632]---> BDD-cost:  143
c ---[1630]---> BDD-cost:  137
c ---[1629]---> BDD-cost:  123
c ---[1628]---> BDD-cost:  134
c ---[1627]---> BDD-cost:  143
c ---[1626]---> BDD-cost:  122
c ---[1625]---> BDD-cost:  135
c ---[1624]---> BDD-cost:  137
c ---[1623]---> BDD-cost:  146
c ---[1622]---> BDD-cost:  120
c ---[1621]---> BDD-cost:  146
c ---[1619]---> BDD-cost:  132
c ---[1618]---> BDD-cost:  149
c ---[1617]---> BDD-cost:  131
c ---[1616]---> BDD-cost:  141
c ---[1615]---> BDD-cost:  137
c ---[1614]---> BDD-cost:  130
c ---[1613]---> BDD-cost:  132
c ---[1612]---> BDD-cost:  125
c ---[1611]---> BDD-cost:  122
c ---[1610]---> BDD-cost:  126
c ---[1608]---> BDD-cost:  122
c ---[1607]---> BDD-cost:  118
c ---[1606]---> BDD-cost:  137
c ---[1605]---> BDD-cost:  130
c ---[1604]---> BDD-cost:  126
c ---[1603]---> BDD-cost:  143
c ---[1602]---> BDD-cost:  126
c ---[1601]---> BDD-cost:  140
c ---[1600]---> BDD-cost:  131
c ---[1599]---> BDD-cost:  140
c ---[1597]---> BDD-cost:  122
c ---[1596]---> BDD-cost:  143
c ---[1595]---> BDD-cost:  134
c ---[1594]---> BDD-cost:  141
c ---[1593]---> BDD-cost:  134
c ---[1592]---> BDD-cost:  143
c ---[1591]---> BDD-cost:  126
c ---[1590]---> BDD-cost:  133
c ---[1589]---> BDD-cost:  134
c ---[1588]---> BDD-cost:  146
c ---[1585]---> BDD-cost:  120
c ---[1584]---> BDD-cost:  146
c ---[1583]---> BDD-cost:  137
c ---[1582]---> BDD-cost:  146
c ---[1581]---> BDD-cost:  120
c ---[1580]---> BDD-cost:  146
c ---[1579]---> BDD-cost:  137
c ---[1578]---> BDD-cost:  138
c ---[1577]---> BDD-cost:  132
c ---[1576]---> BDD-cost:  130
c ---[1574]---> BDD-cost:  137
c ---[1573]---> BDD-cost:  146
c ---[1572]---> BDD-cost:  129
c ---[1571]---> BDD-cost:  140
c ---[1570]---> BDD-cost:  126
c ---[1569]---> BDD-cost:  131
c ---[1568]---> BDD-cost:  134
c ---[1567]---> BDD-cost:  137
c ---[1566]---> BDD-cost:  140
c ---[1565]---> BDD-cost:  140
c ---[1563]---> BDD-cost:  137
c ---[1562]---> BDD-cost:  137
c ---[1561]---> BDD-cost:  141
c ---[1560]---> BDD-cost:  132
c ---[1559]---> BDD-cost:  146
c ---[1558]---> BDD-cost:  146
c ---[1557]---> BDD-cost:  137
c ---[1556]---> BDD-cost:  146
c ---[1555]---> BDD-cost:  131
c ---[1554]---> BDD-cost:  130
c ---[1552]---> BDD-cost:  140
c ---[1551]---> BDD-cost:  140
c ---[1550]---> BDD-cost:  138
c ---[1549]---> BDD-cost:  122
c ---[1548]---> BDD-cost:  143
c ---[1547]---> BDD-cost:  137
c ---[1546]---> BDD-cost:  146
c ---[1545]---> BDD-cost:  122
c ---[1544]---> BDD-cost:  143
c ---[1543]---> BDD-cost:  137
c ---[1541]---> BDD-cost:  138
c ---[1540]---> BDD-cost:  127
c ---[1539]---> BDD-cost:  141
c ---[1538]---> BDD-cost:  134
c ---[1537]---> BDD-cost:  140
c ---[1536]---> BDD-cost:  122
c ---[1535]---> BDD-cost:  133
c ---[1534]---> BDD-cost:  137
c ---[1533]---> BDD-cost:  133
c ---[1532]---> BDD-cost:  140
c ---[1530]---> BDD-cost:  140
c ---[1529]---> BDD-cost:  146
c ---[1528]---> BDD-cost:  137
c ---[1527]---> BDD-cost:  141
c ---[1526]---> BDD-cost:  132
c ---[1525]---> BDD-cost:  141
c ---[1524]---> BDD-cost:  132
c ---[1523]---> BDD-cost:  143
c ---[1522]---> BDD-cost:  127
c ---[1521]---> BDD-cost:  146
c ---[1519]---> BDD-cost:  137
c ---[1518]---> BDD-cost:  133
c ---[1517]---> BDD-cost:  132
c ---[1516]---> BDD-cost:  118
c ---[1515]---> BDD-cost:  132
c ---[1514]---> BDD-cost:  140
c ---[1513]---> BDD-cost:  132
c ---[1512]---> BDD-cost:  138
c ---[1511]---> BDD-cost:  131
c ---[1510]---> BDD-cost:  146
c ---[1508]---> BDD-cost:  127
c ---[1507]---> BDD-cost:  140
c ---[1506]---> BDD-cost:  127
c ---[1505]---> BDD-cost:  141
c ---[1504]---> BDD-cost:  137
c ---[1503]---> BDD-cost:  136
c ---[1502]---> BDD-cost:  127
c ---[1501]---> BDD-cost:  127
c ---[1500]---> BDD-cost:  131
c ---[1499]---> BDD-cost:  138
c ---[1497]---> BDD-cost:  127
c ---[1496]---> BDD-cost:  140
c ---[1495]---> BDD-cost:  127
c ---[1494]---> BDD-cost:  143
c ---[1493]---> BDD-cost:  122
c ---[1492]---> BDD-cost:  140
c ---[1491]---> BDD-cost:  131
c ---[1490]---> BDD-cost:  136
c ---[1489]---> BDD-cost:  134
c ---[1488]---> BDD-cost:  137
c ---[1486]---> BDD-cost:  122
c ---[1485]---> BDD-cost:  141
c ---[1484]---> BDD-cost:  132
c ---[1483]---> BDD-cost:  128
c ---[1482]---> BDD-cost:  127
c ---[1481]---> BDD-cost:  132
c ---[1480]---> BDD-cost:  129
c ---[1479]---> BDD-cost:  146
c ---[1478]---> BDD-cost:  131
c ---[1477]---> BDD-cost:  146
c ---[1474]---> BDD-cost:  129
c ---[1473]---> BDD-cost:  146
c ---[1472]---> BDD-cost:  132
c ---[1471]---> BDD-cost:  141
c ---[1470]---> BDD-cost:  126
c ---[1469]---> BDD-cost:  138
c ---[1468]---> BDD-cost:  134
c ---[1467]---> BDD-cost:  138
c ---[1466]---> BDD-cost:  120
c ---[1465]---> BDD-cost:  141
c ---[1463]---> BDD-cost:  137
c ---[1462]---> BDD-cost:  143
c ---[1461]---> BDD-cost:  124
c ---[1460]---> BDD-cost:  143
c ---[1459]---> BDD-cost:  122
c ---[1458]---> BDD-cost:  136
c ---[1457]---> BDD-cost:  132
c ---[1456]---> BDD-cost:  143
c ---[1455]---> BDD-cost:  140
c ---[1454]---> BDD-cost:  140
c ---[1452]---> BDD-cost:  143
c ---[1451]---> BDD-cost:  137
c ---[1450]---> BDD-cost:  127
c ---[1449]---> BDD-cost:  122
c ---[1448]---> BDD-cost:  146
c ---[1447]---> BDD-cost:  132
c ---[1446]---> BDD-cost:  143
c ---[1252]---> BDD-cost:  125
c ---[1251]---> BDD-cost:  119
c ---[1250]---> BDD-cost:   88
c ---[1248]---> BDD-cost:   88
c ---[1247]---> BDD-cost:   88
c ---[1246]---> BDD-cost:   88
c ---[1245]---> BDD-cost:  123
c ---[1244]---> BDD-cost:  119
c ---[1243]---> BDD-cost:   88
c ---[1242]---> BDD-cost:   88
c ---[1241]---> BDD-cost:   88
c ---[1240]---> BDD-cost:   88
c ---[1239]---> BDD-cost:  125
c ---[1237]---> BDD-cost:  119
c ---[1236]---> BDD-cost:   88
c ---[1235]---> BDD-cost:   88
c ---[1234]---> BDD-cost:   88
c ---[1233]---> BDD-cost:   88
c ---[1232]---> BDD-cost:  115
c ---[1231]---> BDD-cost:  119
c ---[1230]---> BDD-cost:   88
c ---[1229]---> BDD-cost:   88
c ---[1228]---> BDD-cost:   88
c ---[1226]---> BDD-cost:   88
c ---[1225]---> BDD-cost:  125
c ---[1224]---> BDD-cost:  119
c ---[1223]---> BDD-cost:   88
c ---[1222]---> BDD-cost:   88
c ---[1221]---> BDD-cost:   88
c ---[1220]---> BDD-cost:   88
c ---[1219]---> BDD-cost:  123
c ---[1218]---> BDD-cost:  119
c ---[1217]---> BDD-cost:   88
c ---[1215]---> BDD-cost:   88
c ---[1214]---> BDD-cost:   88
c ---[1213]---> BDD-cost:   88
c ---[1212]---> BDD-cost:  125
c ---[1211]---> BDD-cost:  119
c ---[1210]---> BDD-cost:   88
c ---[1209]---> BDD-cost:   88
c ---[1208]---> BDD-cost:   88
c ---[1207]---> BDD-cost:   88
c ---[1206]---> BDD-cost:  123
c ---[1204]---> BDD-cost:  119
c ---[1203]---> BDD-cost:   88
c ---[1202]---> BDD-cost:   88
c ---[1201]---> BDD-cost:   88
c ---[1200]---> BDD-cost:   88
c ---[1199]---> BDD-cost:  121
c ---[1198]---> BDD-cost:  119
c ---[1197]---> BDD-cost:   88
c ---[1196]---> BDD-cost:   88
c ---[1195]---> BDD-cost:   88
c ---[1193]---> BDD-cost:   88
c ---[1192]---> BDD-cost:  125
c ---[1191]---> BDD-cost:  119
c ---[1190]---> BDD-cost:   88
c ---[1189]---> BDD-cost:   88
c ---[1188]---> BDD-cost:   88
c ---[1187]---> BDD-cost:   88
c ---[1186]---> BDD-cost:  123
c ---[1185]---> BDD-cost:  119
c ---[1184]---> BDD-cost:   88
c ---[1182]---> BDD-cost:   88
c ---[1181]---> BDD-cost:   88
c ---[1180]---> BDD-cost:   88
c ---[1179]---> BDD-cost:  125
c ---[1178]---> BDD-cost:  119
c ---[1177]---> BDD-cost:   88
c ---[1176]---> BDD-cost:   88
c ---[1175]---> BDD-cost:   88
c ---[1174]---> BDD-cost:   88
c ---[1173]---> BDD-cost:  125
c ---[1170]---> BDD-cost:  119
c ---[1169]---> BDD-cost:   88
c ---[1168]---> BDD-cost:   88
c ---[1167]---> BDD-cost:   88
c ---[1166]---> BDD-cost:   88
c ---[1165]---> BDD-cost:  123
c ---[1164]---> BDD-cost:  119
c ---[1163]---> BDD-cost:   88
c ---[1162]---> BDD-cost:   88
c ---[1161]---> BDD-cost:   88
c ---[1159]---> BDD-cost:   88
c ---[1158]---> BDD-cost:  115
c ---[1157]---> BDD-cost:  119
c ---[1156]---> BDD-cost:   88
c ---[1155]---> BDD-cost:   88
c ---[1154]---> BDD-cost:   88
c ---[1153]---> BDD-cost:   88
c ---[1152]---> BDD-cost:  123
c ---[1151]---> BDD-cost:  119
c ---[1150]---> BDD-cost:   88
c ---[1148]---> BDD-cost:   88
c ---[1147]---> BDD-cost:   88
c ---[1146]---> BDD-cost:   88
c ---[1145]---> BDD-cost:  119
c ---[1144]---> BDD-cost:  119
c ---[1143]---> BDD-cost:   88
c ---[1142]---> BDD-cost:   88
c ---[1141]---> BDD-cost:   88
c ---[1140]---> BDD-cost:   88
c ---[1139]---> BDD-cost:  125
c ---[1137]---> BDD-cost:  119
c ---[1136]---> BDD-cost:   88
c ---[1135]---> BDD-cost:   88
c ---[1134]---> BDD-cost:   88
c ---[1133]---> BDD-cost:   88
c ---[1132]---> BDD-cost:  119
c ---[1131]---> BDD-cost:  119
c ---[1130]---> BDD-cost:   88
c ---[1129]---> BDD-cost:   88
c ---[1128]---> BDD-cost:   88
c ---[1126]---> BDD-cost:   88
c ---[1125]---> BDD-cost:  123
c ---[1124]---> BDD-cost:  119
c ---[1123]---> BDD-cost:   88
c ---[1122]---> BDD-cost:   88
c ---[1121]---> BDD-cost:   88
c ---[1120]---> BDD-cost:   88
c ---[1119]---> BDD-cost:  125
c ---[1118]---> BDD-cost:  119
c ---[1117]---> BDD-cost:   88
c ---[1115]---> BDD-cost:   88
c ---[1114]---> BDD-cost:   88
c ---[1113]---> BDD-cost:   88
c ---[1112]---> BDD-cost:  121
c ---[1111]---> BDD-cost:  119
c ---[1110]---> BDD-cost:   88
c ---[1109]---> BDD-cost:   88
c ---[1108]---> BDD-cost:   88
c ---[1107]---> BDD-cost:   88
c ---[1106]---> BDD-cost:  123
c ---[1104]---> BDD-cost:  119
c ---[1103]---> BDD-cost:   88
c ---[1102]---> BDD-cost:   88
c ---[1101]---> BDD-cost:   88
c ---[1100]---> BDD-cost:   88
c ---[1099]---> BDD-cost:  119
c ---[1098]---> BDD-cost:  119
c ---[1097]---> BDD-cost:   88
c ---[1096]---> BDD-cost:   88
c ---[1095]---> BDD-cost:   88
c ---[1093]---> BDD-cost:   88
c ---[1092]---> BDD-cost:  123
c ---[1091]---> BDD-cost:  119
c ---[1090]---> BDD-cost:   88
c ---[1089]---> BDD-cost:   88
c ---[1088]---> BDD-cost:   88
c ---[1087]---> BDD-cost:   88
c ---[1086]---> BDD-cost:  121
c ---[1085]---> BDD-cost:  119
c ---[1084]---> BDD-cost:   88
c ---[1082]---> BDD-cost:   88
c ---[1081]---> BDD-cost:   88
c ---[1080]---> BDD-cost:   88
c ---[1079]---> BDD-cost:  123
c ---[1078]---> BDD-cost:  119
c ---[1077]---> BDD-cost:   88
c ---[1076]---> BDD-cost:   88
c ---[1075]---> BDD-cost:   88
c ---[1074]---> BDD-cost:   88
c ---[1073]---> BDD-cost:  123
c ---[1071]---> BDD-cost:  119
c ---[1070]---> BDD-cost:   88
c ---[1069]---> BDD-cost:   88
c ---[1068]---> BDD-cost:   88
c ---[1067]---> BDD-cost:   88
c ---[1066]---> BDD-cost:  121
c ---[1065]---> BDD-cost:  119
c ---[1064]---> BDD-cost:   88
c ---[1063]---> BDD-cost:   88
c ---[1062]---> BDD-cost:   88
c ---[1059]---> BDD-cost:   88
c ---[1058]---> BDD-cost:  123
c ---[1057]---> BDD-cost:  119
c ---[1056]---> BDD-cost:   88
c ---[1055]---> BDD-cost:   88
c ---[1054]---> BDD-cost:   88
c ---[1053]---> BDD-cost:   88
c ---[1052]---> BDD-cost:  121
c ---[1051]---> BDD-cost:  119
c ---[1050]---> BDD-cost:   88
c ---[1048]---> BDD-cost:   88
c ---[1047]---> BDD-cost:   88
c ---[1046]---> BDD-cost:   88
c ---[1045]---> BDD-cost:  123
c ---[1044]---> BDD-cost:  119
c ---[1043]---> BDD-cost:   88
c ---[1042]---> BDD-cost:   88
c ---[1041]---> BDD-cost:   88
c ---[1040]---> BDD-cost:   88
c ---[1039]---> BDD-cost:  123
c ---[1037]---> BDD-cost:  119
c ---[1036]---> BDD-cost:   88
c ---[1035]---> BDD-cost:   88
c ---[1034]---> BDD-cost:   88
c ---[1033]---> BDD-cost:   88
c ---[1032]---> BDD-cost:  123
c ---[1031]---> BDD-cost:  119
c ---[1030]---> BDD-cost:   88
c ---[1029]---> BDD-cost:   88
c ---[1028]---> BDD-cost:   88
c ---[1026]---> BDD-cost:   88
c ---[1025]---> BDD-cost:  123
c ---[1024]---> BDD-cost:  119
c ---[1023]---> BDD-cost:   88
c ---[1022]---> BDD-cost:   88
c ---[1021]---> BDD-cost:   88
c ---[1020]---> BDD-cost:   88
c ---[1019]---> BDD-cost:  119
c ---[1018]---> BDD-cost:  119
c ---[1017]---> BDD-cost:   88
c ---[1015]---> BDD-cost:   88
c ---[1014]---> BDD-cost:   88
c ---[1013]---> BDD-cost:   88
c ---[1012]---> BDD-cost:  125
c ---[1011]---> BDD-cost:  119
c ---[1010]---> BDD-cost:   88
c ---[1009]---> BDD-cost:   88
c ---[1008]---> BDD-cost:   88
c ---[1007]---> BDD-cost:   88
c ---[1006]---> BDD-cost:  125
c ---[1004]---> BDD-cost:  119
c ---[1003]---> BDD-cost:   88
c ---[1002]---> BDD-cost:   88
c ---[1001]---> BDD-cost:   88
c ---[1000]---> BDD-cost:   88
c ---[ 999]---> BDD-cost:  125
c ---[ 998]---> BDD-cost:  119
c ---[ 997]---> BDD-cost:   88
c ---[ 996]---> BDD-cost:   88
c ---[ 995]---> BDD-cost:   88
c ---[ 993]---> BDD-cost:   88
c ---[ 992]---> BDD-cost:  121
c ---[ 991]---> BDD-cost:  119
c ---[ 990]---> BDD-cost:   88
c ---[ 989]---> BDD-cost:   88
c ---[ 988]---> BDD-cost:   88
c ---[ 987]---> BDD-cost:   88
c ---[ 986]---> BDD-cost:  119
c ---[ 985]---> BDD-cost:  119
c ---[ 984]---> BDD-cost:   88
c ---[ 982]---> BDD-cost:   88
c ---[ 981]---> BDD-cost:   88
c ---[ 980]---> BDD-cost:   88
c ---[ 979]---> BDD-cost:  123
c ---[ 978]---> BDD-cost:  119
c ---[ 977]---> BDD-cost:   88
c ---[ 976]---> BDD-cost:   88
c ---[ 975]---> BDD-cost:   88
c ---[ 974]---> BDD-cost:   88
c ---[ 973]---> BDD-cost:  119
c ---[ 971]---> BDD-cost:  119
c ---[ 970]---> BDD-cost:   88
c ---[ 969]---> BDD-cost:   88
c ---[ 968]---> BDD-cost:   88
c ---[ 967]---> BDD-cost:   88
c ---[ 966]---> BDD-cost:  121
c ---[ 965]---> BDD-cost:  119
c ---[ 964]---> BDD-cost:   88
c ---[ 963]---> BDD-cost:   88
c ---[ 962]---> BDD-cost:   88
c ---[ 960]---> BDD-cost:   88
c ---[ 959]---> BDD-cost:  121
c ---[ 958]---> BDD-cost:  119
c ---[ 957]---> BDD-cost:   88
c ---[ 956]---> BDD-cost:   88
c ---[ 955]---> BDD-cost:   88
c ---[ 954]---> BDD-cost:   88
c ---[ 953]---> BDD-cost:  123
c ---[ 952]---> BDD-cost:  119
c ---[ 951]---> BDD-cost:   88
c ---[ 948]---> BDD-cost:   88
c ---[ 947]---> BDD-cost:   88
c ---[ 946]---> BDD-cost:   88
c ---[ 945]---> BDD-cost:  125
c ---[ 944]---> BDD-cost:  119
c ---[ 943]---> BDD-cost:   88
c ---[ 942]---> BDD-cost:   88
c ---[ 941]---> BDD-cost:   88
c ---[ 940]---> BDD-cost:   88
c ---[ 939]---> BDD-cost:  119
c ---[ 937]---> BDD-cost:  119
c ---[ 936]---> BDD-cost:   88
c ---[ 935]---> BDD-cost:   88
c ---[ 934]---> BDD-cost:   88
c ---[ 933]---> BDD-cost:   88
c ---[ 932]---> BDD-cost:  125
c ---[ 931]---> BDD-cost:  119
c ---[ 930]---> BDD-cost:   88
c ---[ 929]---> BDD-cost:   88
c ---[ 928]---> BDD-cost:   88
c ---[ 926]---> BDD-cost:   88
c ---[ 925]---> BDD-cost:  125
c ---[ 924]---> BDD-cost:  119
c ---[ 923]---> BDD-cost:   88
c ---[ 922]---> BDD-cost:   88
c ---[ 921]---> BDD-cost:   88
c ---[ 920]---> BDD-cost:   88
c ---[ 919]---> BDD-cost:  123
c ---[ 918]---> BDD-cost:  119
c ---[ 917]---> BDD-cost:   88
c ---[ 915]---> BDD-cost:   88
c ---[ 914]---> BDD-cost:   88
c ---[ 913]---> BDD-cost:   88
c ---[ 912]---> BDD-cost:  125
c ---[ 911]---> BDD-cost:  119
c ---[ 910]---> BDD-cost:   88
c ---[ 909]---> BDD-cost:   88
c ---[ 908]---> BDD-cost:   88
c ---[ 907]---> BDD-cost:   88
c ---[ 906]---> BDD-cost:  125
c ---[ 904]---> BDD-cost:  119
c ---[ 903]---> BDD-cost:   88
c ---[ 902]---> BDD-cost:   88
c ---[ 901]---> BDD-cost:   88
c ---[ 900]---> BDD-cost:   88
c ---[ 899]---> BDD-cost:  115
c ---[ 898]---> BDD-cost:  119
c ---[ 897]---> BDD-cost:   88
c ---[ 896]---> BDD-cost:   88
c ---[ 895]---> BDD-cost:   88
c ---[ 893]---> BDD-cost:   88
c ---[ 892]---> BDD-cost:  125
c ---[ 891]---> BDD-cost:  119
c ---[ 890]---> BDD-cost:   88
c ---[ 889]---> BDD-cost:   88
c ---[ 888]---> BDD-cost:   88
c ---[ 887]---> BDD-cost:   88
c ---[ 886]---> BDD-cost:  125
c ---[ 885]---> BDD-cost:  119
c ---[ 884]---> BDD-cost:   88
c ---[ 882]---> BDD-cost:   88
c ---[ 881]---> BDD-cost:   88
c ---[ 880]---> BDD-cost:   88
c ---[ 879]---> BDD-cost:  125
c ---[ 878]---> BDD-cost:  119
c ---[ 877]---> BDD-cost:   88
c ---[ 876]---> BDD-cost:   88
c ---[ 875]---> BDD-cost:   88
c ---[ 874]---> BDD-cost:   88
c ---[ 873]---> BDD-cost:  123
c ---[ 871]---> BDD-cost:  119
c ---[ 870]---> BDD-cost:   88
c ---[ 869]---> BDD-cost:   88
c ---[ 868]---> BDD-cost:   88
c ---[ 867]---> BDD-cost:   88
c ---[ 866]---> BDD-cost:  125
c ---[ 865]---> BDD-cost:  119
c ---[ 864]---> BDD-cost:   88
c ---[ 863]---> BDD-cost:   88
c ---[ 862]---> BDD-cost:   88
c ---[ 860]---> BDD-cost:   88
c ---[ 859]---> BDD-cost:  123
c ---[ 858]---> BDD-cost:  119
c ---[ 857]---> BDD-cost:   88
c ---[ 856]---> BDD-cost:   88
c ---[ 855]---> BDD-cost:   88
c ---[ 854]---> BDD-cost:   88
c ---[ 853]---> BDD-cost:  125
c ---[ 852]---> BDD-cost:  119
c ---[ 851]---> BDD-cost:   88
c ---[ 849]---> BDD-cost:   88
c ---[ 848]---> BDD-cost:   88
c ---[ 847]---> BDD-cost:   88
c ---[ 846]---> BDD-cost:  123
c ---[ 845]---> BDD-cost:  119
c ---[ 844]---> BDD-cost:   88
c ---[ 843]---> BDD-cost:   88
c ---[ 842]---> BDD-cost:   88
c ---[ 841]---> BDD-cost:   88
c ---[ 840]---> BDD-cost:  121
c ---[ 837]---> BDD-cost:  119
c ---[ 836]---> BDD-cost:   88
c ---[ 835]---> BDD-cost:   88
c ---[ 834]---> BDD-cost:   88
c ---[ 833]---> BDD-cost:   88
c ---[ 832]---> BDD-cost:  123
c ---[ 831]---> BDD-cost:  119
c ---[ 830]---> BDD-cost:   88
c ---[ 829]---> BDD-cost:   88
c ---[ 828]---> BDD-cost:   88
c ---[ 826]---> BDD-cost:   88
c ---[ 825]---> BDD-cost:  125
c ---[ 824]---> BDD-cost:  119
c ---[ 823]---> BDD-cost:   88
c ---[ 822]---> BDD-cost:   88
c ---[ 821]---> BDD-cost:   88
c ---[ 820]---> BDD-cost:   88
c ---[ 819]---> BDD-cost:  119
c ---[ 818]---> BDD-cost:  119
c ---[ 817]---> BDD-cost:   88
c ---[ 815]---> BDD-cost:   88
c ---[ 814]---> BDD-cost:   88
c ---[ 813]---> BDD-cost:   88
c ---[ 812]---> BDD-cost:  125
c ---[ 811]---> BDD-cost:  119
c ---[ 810]---> BDD-cost:   88
c ---[ 809]---> BDD-cost:   88
c ---[ 808]---> BDD-cost:   88
c ---[ 807]---> BDD-cost:   88
c ---[ 806]---> BDD-cost:  125
c ---[ 804]---> BDD-cost:  119
c ---[ 803]---> BDD-cost:   88
c ---[ 802]---> BDD-cost:   88
c ---[ 801]---> BDD-cost:   88
c ---[ 800]---> BDD-cost:   88
c ---[ 799]---> BDD-cost:  125
c ---[ 798]---> BDD-cost:  119
c ---[ 797]---> BDD-cost:   88
c ---[ 796]---> BDD-cost:   88
c ---[ 795]---> BDD-cost:   88
c ---[ 793]---> BDD-cost:   88
c ---[ 792]---> BDD-cost:  125
c ---[ 791]---> BDD-cost:  119
c ---[ 790]---> BDD-cost:   88
c ---[ 789]---> BDD-cost:   88
c ---[ 788]---> BDD-cost:   88
c ---[ 787]---> BDD-cost:   88
c ---[ 786]---> BDD-cost:  119
c ---[ 785]---> BDD-cost:  119
c ---[ 784]---> BDD-cost:   88
c ---[ 782]---> BDD-cost:   88
c ---[ 781]---> BDD-cost:   88
c ---[ 780]---> BDD-cost:   88
c ---[ 779]---> BDD-cost:  121
c ---[ 778]---> BDD-cost:  119
c ---[ 777]---> BDD-cost:   88
c ---[ 776]---> BDD-cost:   88
c ---[ 775]---> BDD-cost:   88
c ---[ 774]---> BDD-cost:   88
c ---[ 773]---> BDD-cost:  121
c ---[ 771]---> BDD-cost:  119
c ---[ 770]---> BDD-cost:   88
c ---[ 769]---> BDD-cost:   88
c ---[ 768]---> BDD-cost:   88
c ---[ 767]---> BDD-cost:   88
c ---[ 766]---> BDD-cost:  125
c ---[ 765]---> BDD-cost:  119
c ---[ 764]---> BDD-cost:   88
c ---[ 763]---> BDD-cost:   88
c ---[ 762]---> BDD-cost:   88
c ---[ 760]---> BDD-cost:   88
c ---[ 759]---> BDD-cost:  119
c ---[ 758]---> BDD-cost:  119
c ---[ 757]---> BDD-cost:   88
c ---[ 756]---> BDD-cost:   88
c ---[ 755]---> BDD-cost:   88
c ---[ 754]---> BDD-cost:   88
c ---[ 753]---> BDD-cost:  125
c ---[ 752]---> BDD-cost:  119
c ---[ 751]---> BDD-cost:   88
c ---[ 749]---> BDD-cost:   88
c ---[ 748]---> BDD-cost:   88
c ---[ 747]---> BDD-cost:   88
c ---[ 746]---> BDD-cost:  119
c ---[ 745]---> BDD-cost:  119
c ---[ 744]---> BDD-cost:   88
c ---[ 743]---> BDD-cost:   88
c ---[ 742]---> BDD-cost:   88
c ---[ 741]---> BDD-cost:   88
c ---[ 740]---> BDD-cost:  125
c ---[ 738]---> BDD-cost:  119
c ---[ 737]---> BDD-cost:   88
c ---[ 736]---> BDD-cost:   88
c ---[ 735]---> BDD-cost:   88
c ---[ 734]---> BDD-cost:   88
c ---[ 733]---> BDD-cost:  125
c ---[ 732]---> BDD-cost:  119
c ---[ 731]---> BDD-cost:   88
c ---[ 730]---> BDD-cost:   88
c ---[ 729]---> BDD-cost:   88
c ---[ 726]---> BDD-cost:   88
c ---[ 725]---> BDD-cost:  121
c ---[ 724]---> BDD-cost:  119
c ---[ 723]---> BDD-cost:   88
c ---[ 722]---> BDD-cost:   88
c ---[ 721]---> BDD-cost:   88
c ---[ 720]---> BDD-cost:   88
c ---[ 719]---> BDD-cost:  123
c ---[ 718]---> BDD-cost:  119
c ---[ 717]---> BDD-cost:   88
c ---[ 715]---> BDD-cost:   88
c ---[ 714]---> BDD-cost:   88
c ---[ 713]---> BDD-cost:   88
c ---[ 712]---> BDD-cost:  123
c ---[ 711]---> BDD-cost:  119
c ---[ 710]---> BDD-cost:   88
c ---[ 709]---> BDD-cost:   88
c ---[ 708]---> BDD-cost:   88
c ---[ 707]---> BDD-cost:   88
c ---[ 706]---> BDD-cost:  125
c ---[ 704]---> BDD-cost:  119
c ---[ 703]---> BDD-cost:   88
c ---[ 702]---> BDD-cost:   88
c ---[ 701]---> BDD-cost:   88
c ---[ 700]---> BDD-cost:   88
c ---[ 699]---> BDD-cost:  125
c ---[ 698]---> BDD-cost:  119
c ---[ 697]---> BDD-cost:   88
c ---[ 696]---> BDD-cost:   88
c ---[ 695]---> BDD-cost:   88
c ---[ 693]---> BDD-cost:   88
c ---[ 692]---> BDD-cost:  121
c ---[ 691]---> BDD-cost:  119
c ---[ 690]---> BDD-cost:   88
c ---[ 689]---> BDD-cost:   88
c ---[ 688]---> BDD-cost:   88
c ---[ 687]---> BDD-cost:   88
c ---[ 686]---> BDD-cost:  125
c ---[ 685]---> BDD-cost:  119
c ---[ 684]---> BDD-cost:   88
c ---[ 682]---> BDD-cost:   88
c ---[ 681]---> BDD-cost:   88
c ---[ 680]---> BDD-cost:   88
c ---[ 679]---> BDD-cost:  121
c ---[ 678]---> BDD-cost:  119
c ---[ 677]---> BDD-cost:   88
c ---[ 676]---> BDD-cost:   88
c ---[ 675]---> BDD-cost:   88
c ---[ 674]---> BDD-cost:   88
c ---[ 673]---> BDD-cost:  123
c ---[ 671]---> BDD-cost:  119
c ---[ 670]---> BDD-cost:   88
c ---[ 669]---> BDD-cost:   88
c ---[ 668]---> BDD-cost:   88
c ---[ 667]---> BDD-cost:   88
c ---[ 666]---> BDD-cost:  125
c ---[ 665]---> BDD-cost:  119
c ---[ 664]---> BDD-cost:   88
c ---[ 663]---> BDD-cost:   88
c ---[ 662]---> BDD-cost:   88
c ---[ 660]---> BDD-cost:   88
c ---[ 659]---> BDD-cost:  119
c ---[ 658]---> BDD-cost:  119
c ---[ 657]---> BDD-cost:   88
c ---[ 656]---> BDD-cost:   88
c ---[ 655]---> BDD-cost:   88
c ---[ 654]---> BDD-cost:   88
c ---[ 653]---> BDD-cost:  125
c ---[ 652]---> BDD-cost:  119
c ---[ 651]---> BDD-cost:   88
c ---[ 649]---> BDD-cost:   88
c ---[ 648]---> BDD-cost:   88
c ---[ 647]---> BDD-cost:   88
c ---[ 646]---> BDD-cost:  117
c ---[ 645]---> BDD-cost:  119
c ---[ 644]---> BDD-cost:   88
c ---[ 643]---> BDD-cost:   88
c ---[ 642]---> BDD-cost:   88
c ---[ 641]---> BDD-cost:   88
c ---[ 640]---> BDD-cost:  125
c ---[ 638]---> BDD-cost:  119
c ---[ 637]---> BDD-cost:   88
c ---[ 636]---> BDD-cost:   88
c ---[ 635]---> BDD-cost:   88
c ---[ 634]---> BDD-cost:   88
c ---[ 633]---> BDD-cost:  121
c ---[ 632]---> BDD-cost:  119
c ---[ 631]---> BDD-cost:   88
c ---[ 630]---> BDD-cost:   88
c ---[ 629]---> BDD-cost:   88
c ---[ 627]---> BDD-cost:   88
c ---[ 626]---> BDD-cost:  125
c ---[ 625]---> BDD-cost:  119
c ---[ 624]---> BDD-cost:   88
c ---[ 623]---> BDD-cost:   88
c ---[ 622]---> BDD-cost:   88
c ---[ 621]---> BDD-cost:   88
c ---[ 620]---> BDD-cost:  125
c ---[ 619]---> BDD-cost:  119
c ---[ 618]---> BDD-cost:   88
c ---[ 617]---> BDD-cost:   26
c ---[ 616]---> BDD-cost:   26
c ---[ 615]---> BDD-cost:   26
c ---[ 614]---> BDD-cost:   26
c ---[ 613]---> BDD-cost:   26
c ---[ 612]---> BDD-cost:   26
c ---[ 611]---> BDD-cost:   26
c ---[ 610]---> BDD-cost:   26
c ---[ 609]---> BDD-cost:   26
c ---[ 608]---> BDD-cost:   26
c ---[ 607]---> BDD-cost:   26
c ---[ 606]---> BDD-cost:   26
c ---[ 605]---> BDD-cost:   26
c ---[ 604]---> BDD-cost:   26
c ---[ 603]---> BDD-cost:   26
c ---[ 602]---> BDD-cost:   26
c ---[ 601]---> BDD-cost:   26
c ---[ 600]---> BDD-cost:   26
c ---[ 599]---> BDD-cost:   26
c ---[ 598]---> BDD-cost:   26
c ---[ 597]---> BDD-cost:   26
c ---[ 596]---> BDD-cost:   26
c ---[ 595]---> BDD-cost:   26
c ---[ 594]---> BDD-cost:   26
c ---[ 593]---> BDD-cost:   26
c ---[ 592]---> BDD-cost:   26
c ---[ 591]---> BDD-cost:   26
c ---[ 590]---> BDD-cost:   26
c ---[ 589]---> BDD-cost:   26
c ---[ 588]---> BDD-cost:   26
c ---[ 587]---> BDD-cost:   26
c ---[ 586]---> BDD-cost:   26
c ---[ 585]---> BDD-cost:   26
c ---[ 584]---> BDD-cost:   26
c ---[ 583]---> BDD-cost:   26
c ---[ 582]---> BDD-cost:   26
c ---[ 581]---> BDD-cost:   26
c ---[ 580]---> BDD-cost:   26
c ---[ 579]---> BDD-cost:   26
c ---[ 578]---> BDD-cost:   26
c ---[ 577]---> BDD-cost:   26
c ---[ 576]---> BDD-cost:   26
c ---[ 575]---> BDD-cost:   26
c ---[ 574]---> BDD-cost:   26
c ---[ 573]---> BDD-cost:   26
c ---[ 572]---> BDD-cost:   26
c ---[ 571]---> BDD-cost:   26
c ---[ 570]---> BDD-cost:   26
c ---[ 569]---> BDD-cost:   26
c ---[ 568]---> BDD-cost:   26
c ---[ 567]---> BDD-cost:   26
c ---[ 566]---> BDD-cost:   26
c ---[ 565]---> BDD-cost:   26
c ---[ 564]---> BDD-cost:   26
c ---[ 563]---> BDD-cost:   26
c ---[ 562]---> BDD-cost:   26
c ---[ 561]---> BDD-cost:   26
c ---[ 560]---> BDD-cost:   26
c ---[ 559]---> BDD-cost:   26
c ---[ 558]---> BDD-cost:   26
c ---[ 557]---> BDD-cost:   26
c ---[ 556]---> BDD-cost:   26
c ---[ 555]---> BDD-cost:   26
c ---[ 554]---> BDD-cost:   26
c ---[ 553]---> BDD-cost:   26
c ---[ 552]---> BDD-cost:   26
c ---[ 551]---> BDD-cost:   26
c ---[ 550]---> BDD-cost:   26
c ---[ 549]---> BDD-cost:   26
c ---[ 548]---> BDD-cost:   26
c ---[ 547]---> BDD-cost:   26
c ---[ 546]---> BDD-cost:   26
c ---[ 545]---> BDD-cost:   26
c ---[ 544]---> BDD-cost:   26
c ---[ 543]---> BDD-cost:   26
c ---[ 542]---> BDD-cost:   26
c ---[ 541]---> BDD-cost:   26
c ---[ 540]---> BDD-cost:   26
c ---[ 539]---> BDD-cost:   26
c ---[ 538]---> BDD-cost:   26
c ---[ 537]---> BDD-cost:   26
c ---[ 536]---> BDD-cost:   26
c ---[ 535]---> BDD-cost:   26
c ---[ 534]---> BDD-cost:   26
c ---[ 533]---> BDD-cost:   26
c ---[ 532]---> BDD-cost:   26
c ---[ 531]---> BDD-cost:   26
c ---[ 530]---> BDD-cost:   26
c ---[ 529]---> BDD-cost:   26
c ---[ 528]---> BDD-cost:   26
c ---[ 527]---> BDD-cost:   26
c ---[ 526]---> BDD-cost:   26
c ---[ 525]---> BDD-cost:   26
c ---[ 524]---> BDD-cost:   26
c ---[ 523]---> BDD-cost:   26
c ---[ 522]---> BDD-cost:   26
c ---[ 521]---> BDD-cost:   26
c ---[ 520]---> BDD-cost:   26
c ---[ 519]---> BDD-cost:   26
c ---[ 518]---> BDD-cost:   26
c ---[ 517]---> BDD-cost:   26
c ---[ 516]---> BDD-cost:   26
c ---[ 515]---> BDD-cost:   26
c ---[ 514]---> BDD-cost:   26
c ---[ 513]---> BDD-cost:   26
c ---[ 512]---> BDD-cost:   26
c ---[ 511]---> BDD-cost:   26
c ---[ 510]---> BDD-cost:   26
c ---[ 509]---> BDD-cost:   26
c ---[ 508]---> BDD-cost:   26
c ---[ 507]---> BDD-cost:   26
c ---[ 506]---> BDD-cost:   26
c ---[ 505]---> BDD-cost:   26
c ---[ 504]---> BDD-cost:   26
c ---[ 503]---> BDD-cost:   26
c ---[ 502]---> BDD-cost:   26
c ---[ 501]---> BDD-cost:   26
c ---[ 500]---> BDD-cost:   26
c ---[ 499]---> BDD-cost:   26
c ---[ 498]---> BDD-cost:   26
c ---[ 497]---> BDD-cost:   26
c ---[ 496]---> BDD-cost:   26
c ---[ 495]---> BDD-cost:   26
c ---[ 494]---> BDD-cost:   26
c ---[ 493]---> BDD-cost:   26
c ---[ 492]---> BDD-cost:   26
c ---[ 491]---> BDD-cost:   26
c ---[ 490]---> BDD-cost:   26
c ---[ 489]---> BDD-cost:   26
c ---[ 488]---> BDD-cost:   26
c ---[ 487]---> BDD-cost:   26
c ---[ 486]---> BDD-cost:   26
c ---[ 485]---> BDD-cost:   26
c ---[ 484]---> BDD-cost:   26
c ---[ 483]---> BDD-cost:   26
c ---[ 482]---> BDD-cost:   26
c ---[ 481]---> BDD-cost:   26
c ---[ 480]---> BDD-cost:   26
c ---[ 479]---> BDD-cost:   26
c ---[ 478]---> BDD-cost:   26
c ---[ 477]---> BDD-cost:   26
c ---[ 476]---> BDD-cost:   26
c ---[ 475]---> BDD-cost:   26
c ---[ 474]---> BDD-cost:   26
c ---[ 473]---> BDD-cost:   26
c ---[ 472]---> BDD-cost:   26
c ---[ 471]---> BDD-cost:   26
c ---[ 470]---> BDD-cost:   26
c ---[ 469]---> BDD-cost:   26
c ---[ 468]---> BDD-cost:   26
c ---[ 467]---> BDD-cost:   26
c ---[ 466]---> BDD-cost:   26
c ---[ 465]---> BDD-cost:   26
c ---[ 464]---> BDD-cost:   26
c ---[ 463]---> BDD-cost:   26
c ---[ 462]---> BDD-cost:   26
c ---[ 461]---> BDD-cost:   26
c ---[ 460]---> BDD-cost:   26
c ---[ 459]---> BDD-cost:   26
c ---[ 458]---> BDD-cost:   26
c ---[ 457]---> BDD-cost:   26
c ---[ 456]---> BDD-cost:   26
c ---[ 455]---> BDD-cost:   26
c ---[ 454]---> BDD-cost:   26
c ---[ 453]---> BDD-cost:   26
c ---[ 452]---> BDD-cost:   26
c ---[ 451]---> BDD-cost:   26
c ---[ 450]---> BDD-cost:   26
c ---[ 449]---> BDD-cost:   26
c ---[ 448]---> BDD-cost:   26
c ---[ 447]---> BDD-cost:   26
c ---[ 446]---> BDD-cost:   26
c ---[ 445]---> BDD-cost:   26
c ---[ 444]---> BDD-cost:   26
c ---[ 443]---> BDD-cost:   26
c ---[ 442]---> BDD-cost:   26
c ---[ 441]---> BDD-cost:   26
c ---[ 440]---> BDD-cost:   26
c ---[ 439]---> BDD-cost:   26
c ---[ 438]---> BDD-cost:   26
c ---[ 437]---> BDD-cost:   26
c ---[ 436]---> BDD-cost:   26
c ---[ 435]---> BDD-cost:   26
c ---[ 434]---> BDD-cost:   26
c ---[ 433]---> BDD-cost:   26
c ---[ 432]---> BDD-cost:   26
c ---[ 431]---> BDD-cost:   26
c ---[ 430]---> BDD-cost:   26
c ---[ 429]---> BDD-cost:   26
c ---[ 428]---> BDD-cost:   26
c ---[ 427]---> BDD-cost:   26
c ---[ 426]---> BDD-cost:   26
c ---[ 425]---> BDD-cost:   26
c ---[ 424]---> BDD-cost:   26
c ---[ 423]---> BDD-cost:   26
c ---[ 422]---> BDD-cost:   26
c ---[ 421]---> BDD-cost:   26
c ---[ 420]---> BDD-cost:   26
c ---[ 419]---> BDD-cost:   26
c ---[ 418]---> BDD-cost:   26
c ---[ 417]---> BDD-cost:   26
c ---[ 416]---> BDD-cost:   26
c ---[ 415]---> BDD-cost:   26
c ---[ 414]---> BDD-cost:   26
c ---[ 413]---> BDD-cost:   26
c ---[ 412]---> BDD-cost:   26
c ---[ 411]---> BDD-cost:   26
c ---[ 410]---> BDD-cost:   26
c ---[ 409]---> BDD-cost:   26
c ---[ 408]---> BDD-cost:   26
c ---[ 407]---> BDD-cost:   26
c ---[ 406]---> BDD-cost:   26
c ---[ 405]---> BDD-cost:   26
c ---[ 404]---> BDD-cost:   26
c ---[ 403]---> BDD-cost:   26
c ---[ 402]---> BDD-cost:   26
c ---[ 401]---> BDD-cost:   26
c ---[ 400]---> BDD-cost:   26
c ---[ 399]---> BDD-cost:   26
c ---[ 398]---> BDD-cost:   26
c ---[ 397]---> BDD-cost:   26
c ---[ 396]---> BDD-cost:   26
c ---[ 395]---> BDD-cost:   26
c ---[ 394]---> BDD-cost:   26
c ---[ 393]---> BDD-cost:   26
c ---[ 392]---> BDD-cost:   26
c ---[ 391]---> BDD-cost:   26
c ---[ 390]---> BDD-cost:   26
c ---[ 389]---> BDD-cost:   26
c ---[ 388]---> BDD-cost:   26
c ---[ 387]---> BDD-cost:   26
c ---[ 386]---> BDD-cost:   26
c ---[ 385]---> BDD-cost:   26
c ---[ 384]---> BDD-cost:   26
c ---[ 383]---> BDD-cost:   26
c ---[ 382]---> BDD-cost:   26
c ---[ 381]---> BDD-cost:   26
c ---[ 380]---> BDD-cost:   26
c ---[ 379]---> BDD-cost:   26
c ---[ 378]---> BDD-cost:   26
c ---[ 377]---> BDD-cost:   26
c ---[ 376]---> BDD-cost:   26
c ---[ 375]---> BDD-cost:   26
c ---[ 374]---> BDD-cost:   26
c ---[ 373]---> BDD-cost:   26
c ---[ 372]---> BDD-cost:   26
c ---[ 371]---> BDD-cost:   26
c ---[ 370]---> BDD-cost:   26
c ---[ 369]---> BDD-cost:   26
c ---[ 368]---> BDD-cost:   26
c ---[ 367]---> BDD-cost:   26
c ---[ 366]---> BDD-cost:   26
c ---[ 365]---> BDD-cost:   26
c ---[ 364]---> BDD-cost:   26
c ---[ 363]---> BDD-cost:   26
c ---[ 362]---> BDD-cost:   26
c ---[ 361]---> BDD-cost:   26
c ---[ 360]---> BDD-cost:   26
c ---[ 359]---> BDD-cost:   26
c ---[ 358]---> BDD-cost:   26
c ---[ 357]---> BDD-cost:   26
c ---[ 356]---> BDD-cost:   26
c ---[ 355]---> BDD-cost:   26
c ---[ 354]---> BDD-cost:   26
c ---[ 353]---> BDD-cost:   26
c ---[ 352]---> BDD-cost:   26
c ---[ 351]---> BDD-cost:   26
c ---[ 350]---> BDD-cost:   26
c ---[ 349]---> BDD-cost:   26
c ---[ 348]---> BDD-cost:   26
c ---[ 347]---> BDD-cost:   26
c ---[ 346]---> BDD-cost:   26
c ---[ 345]---> BDD-cost:   26
c ---[ 344]---> BDD-cost:   26
c ---[ 343]---> BDD-cost:   26
c ---[ 342]---> BDD-cost:   26
c ---[ 341]---> BDD-cost:   26
c ---[ 340]---> BDD-cost:   26
c ---[ 339]---> BDD-cost:   26
c ---[ 338]---> BDD-cost:   26
c ---[ 337]---> BDD-cost:   26
c ---[ 336]---> BDD-cost:   26
c ---[ 335]---> BDD-cost:   26
c ---[ 334]---> BDD-cost:   26
c ---[ 333]---> BDD-cost:   26
c ---[ 332]---> BDD-cost:   26
c ---[ 331]---> BDD-cost:   26
c ---[ 330]---> BDD-cost:   26
c ---[ 329]---> BDD-cost:   26
c ---[ 328]---> BDD-cost:   26
c ---[ 327]---> BDD-cost:   26
c ---[ 326]---> BDD-cost:   26
c ---[ 325]---> BDD-cost:   26
c ---[ 324]---> BDD-cost:   26
c ---[ 323]---> BDD-cost:   26
c ---[ 322]---> BDD-cost:   26
c ---[ 321]---> BDD-cost:   26
c ---[ 320]---> BDD-cost:   26
c ---[ 319]---> BDD-cost:   26
c ---[ 318]---> BDD-cost:   26
c ---[ 317]---> BDD-cost:   26
c ---[ 316]---> BDD-cost:   26
c ---[ 315]---> BDD-cost:   26
c ---[ 314]---> BDD-cost:   26
c ---[ 313]---> BDD-cost:   26
c ---[ 312]---> BDD-cost:   26
c ---[ 311]---> BDD-cost:   26
c ---[ 310]---> BDD-cost:   26
c ---[ 309]---> BDD-cost:   26
c ---[ 308]---> BDD-cost:   26
c ---[ 307]---> BDD-cost:   26
c ---[ 306]---> BDD-cost:   26
c ---[ 305]---> BDD-cost:   26
c ---[ 304]---> BDD-cost:   26
c ---[ 303]---> BDD-cost:   26
c ---[ 302]---> BDD-cost:   26
c ---[ 301]---> BDD-cost:   26
c ---[ 300]---> BDD-cost:   26
c ---[ 299]---> BDD-cost:   26
c ---[ 298]---> BDD-cost:   26
c ---[ 297]---> BDD-cost:   26
c ---[ 296]---> BDD-cost:   26
c ---[ 295]---> BDD-cost:   26
c ---[ 294]---> BDD-cost:   26
c ---[ 293]---> BDD-cost:   26
c ---[ 292]---> BDD-cost:   26
c ---[ 291]---> BDD-cost:   26
c ---[ 290]---> BDD-cost:   26
c ---[ 289]---> BDD-cost:   26
c ---[ 288]---> BDD-cost:   26
c ---[ 287]---> BDD-cost:   26
c ---[ 286]---> BDD-cost:   26
c ---[ 285]---> BDD-cost:   26
c ---[ 284]---> BDD-cost:   26
c ---[ 283]---> BDD-cost:   26
c ---[ 282]---> BDD-cost:   26
c ---[ 281]---> BDD-cost:   26
c ---[ 280]---> BDD-cost:   26
c ---[ 279]---> BDD-cost:   26
c ---[ 278]---> BDD-cost:   26
c ---[ 277]---> BDD-cost:   26
c ---[ 276]---> BDD-cost:   26
c ---[ 275]---> BDD-cost:   26
c ---[ 274]---> BDD-cost:   26
c ---[ 273]---> BDD-cost:   26
c ---[ 272]---> BDD-cost:   26
c ---[ 271]---> BDD-cost:   26
c ---[ 270]---> BDD-cost:   26
c ---[ 269]---> BDD-cost:   26
c ---[ 268]---> BDD-cost:   26
c ---[ 267]---> BDD-cost:   26
c ---[ 266]---> BDD-cost:   26
c ---[ 265]---> BDD-cost:   26
c ---[ 264]---> BDD-cost:   26
c ---[ 263]---> BDD-cost:   26
c ---[ 262]---> BDD-cost:   26
c ---[ 261]---> BDD-cost:   26
c ---[ 260]---> BDD-cost:   26
c ---[ 259]---> BDD-cost:   26
c ---[ 258]---> BDD-cost:   26
c ---[ 257]---> BDD-cost:   26
c ---[ 256]---> BDD-cost:   26
c ---[ 255]---> BDD-cost:   26
c ---[ 254]---> BDD-cost:   26
c ---[ 253]---> BDD-cost:   26
c ---[ 252]---> BDD-cost:   26
c ---[ 251]---> BDD-cost:   26
c ---[ 250]---> BDD-cost:   26
c ---[ 249]---> BDD-cost:   26
c ---[ 248]---> BDD-cost:   26
c ---[ 247]---> BDD-cost:   26
c ---[ 246]---> BDD-cost:   26
c ---[ 245]---> BDD-cost:   26
c ---[ 244]---> BDD-cost:   26
c ---[ 243]---> BDD-cost:   26
c ---[ 242]---> BDD-cost:   26
c ---[ 241]---> BDD-cost:   26
c ---[ 240]---> BDD-cost:   26
c ---[ 239]---> BDD-cost:   26
c ---[ 238]---> BDD-cost:   26
c ---[ 237]---> BDD-cost:   26
c ---[ 236]---> BDD-cost:   26
c ---[ 235]---> BDD-cost:   26
c ---[ 234]---> BDD-cost:   26
c ---[ 233]---> BDD-cost:   26
c ---[ 232]---> BDD-cost:   26
c ---[ 231]---> BDD-cost:   26
c ---[ 230]---> BDD-cost:   26
c ---[ 229]---> BDD-cost:   26
c ---[ 228]---> BDD-cost:   26
c ---[ 227]---> BDD-cost:   26
c ---[ 226]---> BDD-cost:   26
c ---[ 225]---> BDD-cost:   26
c ---[ 224]---> BDD-cost:   26
c ---[ 223]---> BDD-cost:   26
c ---[ 222]---> BDD-cost:   26
c ---[ 221]---> BDD-cost:   26
c ---[ 220]---> BDD-cost:   26
c ---[ 219]---> BDD-cost:   26
c ---[ 218]---> BDD-cost:   26
c ---[ 217]---> BDD-cost:   26
c ---[ 216]---> BDD-cost:   26
c ---[ 215]---> BDD-cost:   26
c ---[ 214]---> BDD-cost:   26
c ---[ 213]---> BDD-cost:   26
c ---[ 212]---> BDD-cost:   26
c ---[ 211]---> BDD-cost:   26
c ---[ 210]---> BDD-cost:   26
c ---[ 209]---> BDD-cost:   26
c ---[ 208]---> BDD-cost:   26
c ---[ 207]---> BDD-cost:   26
c ---[ 206]---> BDD-cost:   26
c ---[ 205]---> BDD-cost:   26
c ---[ 204]---> BDD-cost:   26
c ---[ 203]---> BDD-cost:   26
c ---[ 202]---> BDD-cost:   26
c ---[ 201]---> BDD-cost:   26
c ---[ 200]---> BDD-cost:   26
c ---[ 199]---> BDD-cost:   26
c ---[ 198]---> BDD-cost:   26
c ---[ 197]---> BDD-cost:   26
c ---[ 196]---> BDD-cost:   26
c ---[ 195]---> BDD-cost:   26
c ---[ 194]---> BDD-cost:   26
c ---[ 193]---> BDD-cost:   26
c ---[ 192]---> BDD-cost:   26
c ---[ 191]---> BDD-cost:   26
c ---[ 190]---> BDD-cost:   26
c ---[ 189]---> BDD-cost:   26
c ---[ 188]---> BDD-cost:   26
c ---[ 187]---> BDD-cost:   26
c ---[ 186]---> BDD-cost:   26
c ---[ 185]---> BDD-cost:   26
c ---[ 184]---> BDD-cost:   26
c ---[ 183]---> BDD-cost:   26
c ---[ 182]---> BDD-cost:   26
c ---[ 181]---> BDD-cost:   26
c ---[ 180]---> BDD-cost:   26
c ---[ 179]---> BDD-cost:   26
c ---[ 178]---> BDD-cost:   26
c ---[ 177]---> BDD-cost:   26
c ---[ 176]---> BDD-cost:   26
c ---[ 175]---> BDD-cost:   26
c ---[ 174]---> BDD-cost:   26
c ---[ 173]---> BDD-cost:   26
c ---[ 172]---> BDD-cost:   26
c ---[ 171]---> BDD-cost:   26
c ---[ 170]---> BDD-cost:   26
c ---[ 169]---> BDD-cost:   26
c ---[ 168]---> BDD-cost:   26
c ---[ 167]---> BDD-cost:   26
c ---[ 166]---> BDD-cost:   26
c ---[ 165]---> BDD-cost:   26
c ---[ 164]---> BDD-cost:   26
c ---[ 163]---> BDD-cost:   26
c ---[ 162]---> BDD-cost:   26
c ---[ 161]---> BDD-cost:   26
c ---[ 160]---> BDD-cost:   26
c ---[ 159]---> BDD-cost:   26
c ---[ 158]---> BDD-cost:   26
c ---[ 157]---> BDD-cost:   26
c ---[ 156]---> BDD-cost:   26
c ---[ 155]---> BDD-cost:   26
c ---[ 154]---> BDD-cost:   26
c ---[ 153]---> BDD-cost:   26
c ---[ 152]---> BDD-cost:   26
c ---[ 151]---> BDD-cost:   26
c ---[ 150]---> BDD-cost:   26
c ---[ 149]---> BDD-cost:   26
c ---[ 148]---> BDD-cost:   26
c ---[ 147]---> BDD-cost:   26
c ---[ 146]---> BDD-cost:   26
c ---[ 145]---> BDD-cost:   26
c ---[ 144]---> BDD-cost:   26
c ---[ 143]---> BDD-cost:   26
c ---[ 142]---> BDD-cost:   26
c ---[ 141]---> BDD-cost:   26
c ---[ 140]---> BDD-cost:   26
c ---[ 139]---> BDD-cost:   26
c ---[ 138]---> BDD-cost:   26
c ---[ 137]---> BDD-cost:   26
c ---[ 136]---> BDD-cost:   26
c ---[ 135]---> BDD-cost:   26
c ---[ 134]---> BDD-cost:   26
c ---[ 133]---> BDD-cost:   26
c ---[ 132]---> BDD-cost:   26
c ---[ 131]---> BDD-cost:   26
c ---[ 130]---> BDD-cost:   26
c ---[ 129]---> BDD-cost:   26
c ---[ 128]---> BDD-cost:   26
c ---[ 127]---> BDD-cost:   26
c ---[ 126]---> BDD-cost:   26
c ---[ 125]---> BDD-cost:   26
c ---[ 124]---> BDD-cost:   26
c ---[ 123]---> BDD-cost:   26
c ---[ 122]---> BDD-cost:   26
c ---[ 121]---> BDD-cost:   26
c ---[ 120]---> BDD-cost:   26
c ---[ 119]---> BDD-cost:   26
c ---[ 118]---> BDD-cost:   26
c ---[ 117]---> BDD-cost:   26
c ---[ 116]---> BDD-cost:   26
c ---[ 115]---> BDD-cost:   26
c ---[ 114]---> BDD-cost:   26
c ---[ 113]---> BDD-cost:   26
c ---[ 112]---> BDD-cost:   26
c ---[ 111]---> BDD-cost:   26
c ---[ 110]---> BDD-cost:   26
c ---[ 109]---> BDD-cost:   26
c ---[ 108]---> BDD-cost:   26
c ---[ 107]---> BDD-cost:   26
c ---[ 106]---> BDD-cost:   26
c ---[ 105]---> BDD-cost:   26
c ---[ 104]---> BDD-cost:   26
c ---[ 103]---> BDD-cost:   26
c ---[ 102]---> BDD-cost:   26
c ---[ 101]---> BDD-cost:   26
c ---[ 100]---> BDD-cost:   26
c ---[  99]---> BDD-cost:   26
c ---[  98]---> BDD-cost:   26
c ---[  97]---> BDD-cost:   26
c ---[  96]---> BDD-cost:   26
c ---[  95]---> BDD-cost:   26
c ---[  94]---> BDD-cost:   26
c ---[  93]---> BDD-cost:   26
c ---[  92]---> BDD-cost:   26
c ---[  91]---> BDD-cost:   26
c ---[  90]---> BDD-cost:   26
c ---[  89]---> BDD-cost:   26
c ---[  88]---> BDD-cost:   26
c ---[  87]---> BDD-cost:   26
c ---[  86]---> BDD-cost:   26
c ---[  85]---> BDD-cost:   26
c ---[  84]---> BDD-cost:   26
c ---[  83]---> BDD-cost:   26
c ---[  82]---> BDD-cost:   26
c ---[  81]---> BDD-cost:   26
c ---[  80]---> BDD-cost:   26
c ---[  79]---> BDD-cost:   26
c ---[  78]---> BDD-cost:   26
c ---[  77]---> BDD-cost:   26
c ---[  76]---> BDD-cost:   26
c ---[  75]---> BDD-cost:   26
c ---[  74]---> BDD-cost:   26
c ---[  73]---> BDD-cost:   26
c ---[  72]---> BDD-cost:   26
c ---[  71]---> BDD-cost:   26
c ---[  70]---> BDD-cost:   26
c ---[  69]---> BDD-cost:   26
c ---[  68]---> BDD-cost:   26
c ---[  67]---> BDD-cost:   26
c ---[  66]---> BDD-cost:   26
c ---[  65]---> BDD-cost:   26
c ---[  64]---> BDD-cost:   26
c ---[  63]---> BDD-cost:   26
c ---[  62]---> BDD-cost:   26
c ---[  61]---> BDD-cost:   26
c ---[  60]---> BDD-cost:   26
c ---[  59]---> BDD-cost:   26
c ---[  58]---> BDD-cost:   26
c ---[  57]---> BDD-cost:   26
c ---[  56]---> BDD-cost:   26
c ---[  55]---> BDD-cost:   26
c ---[  54]---> BDD-cost:   26
c ---[  53]---> BDD-cost:   26
c ---[  52]---> BDD-cost:   26
c ---[  51]---> BDD-cost:   26
c ---[  50]---> BDD-cost:   26
c ---[  49]---> BDD-cost:   26
c ---[  48]---> BDD-cost:   26
c ---[  47]---> BDD-cost:   26
c ---[  46]---> BDD-cost:   26
c ---[  45]---> BDD-cost:   26
c ---[  44]---> BDD-cost:   26
c ---[  43]---> BDD-cost:   26
c ---[  42]---> BDD-cost:   26
c ---[  41]---> BDD-cost:   26
c ---[  40]---> BDD-cost:   26
c ---[  39]---> BDD-cost:   26
c ---[  38]---> BDD-cost:   26
c ---[  37]---> BDD-cost:   26
c ---[  36]---> BDD-cost:   26
c ---[  35]---> BDD-cost:   26
c ---[  34]---> BDD-cost:   26
c ---[  33]---> BDD-cost:   26
c ---[  32]---> BDD-cost:   26
c ---[  31]---> BDD-cost:   26
c ---[  30]---> BDD-cost:   26
c ---[  29]---> BDD-cost:   26
c ---[  28]---> BDD-cost:   26
c ---[  27]---> BDD-cost:   26
c ---[  26]---> BDD-cost:   26
c ---[  25]---> BDD-cost:   26
c ---[  24]---> BDD-cost:   26
c ---[  23]---> BDD-cost:   26
c ---[  22]---> BDD-cost:   26
c ---[  21]---> BDD-cost:   26
c ---[  20]---> BDD-cost:   26
c ---[  19]---> BDD-cost:   26
c ---[  18]---> BDD-cost:   26
c ---[  17]---> BDD-cost:   26
c ---[  16]---> BDD-cost:   26
c ---[  15]---> BDD-cost:   26
c ---[  14]---> BDD-cost:   26
c ---[  13]---> BDD-cost:   26
c ---[  12]---> BDD-cost:   26
c ---[  11]---> BDD-cost:   26
c ---[  10]---> BDD-cost:   26
c ---[   9]---> BDD-cost:   26
c ---[   8]---> BDD-cost:   26
c ---[   7]---> BDD-cost:   26
c ---[   6]---> BDD-cost:   26
c ---[   5]---> BDD-cost:   26
c ---[   4]---> BDD-cost:   26
c ---[   3]---> BDD-cost:   26
c ---[   2]---> BDD-cost:   26
c ---[   1]---> BDD-cost:   26
c ---[   0]---> BDD-cost:   26
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |  488187  1305639 |  162729       0        0     nan |  0.000 % |
c |       100 |  488185  1305635 |  179001      99      789     8.0 |  1.103 % |
c |       250 |  488063  1305391 |  196902     188     1628     8.7 |  1.129 % |
c |       475 |  488063  1305391 |  216592     413     4167    10.1 |  1.129 % |
c |       815 |  488041  1305347 |  238251     742     6934     9.3 |  1.133 % |
c |      1322 |  488029  1305323 |  262076    1243    10742     8.6 |  1.136 % |
c |      2081 |  487977  1305219 |  288284    1975    17960     9.1 |  1.147 % |
c ==============================================================================
c [1mFound solution: 509952[0m
c ---[   0]---> Sorter-cost: 2296     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      2403 |  489875  1309738 |  163291    2256    20043     8.9 |  1.147 % |
c |      2503 |  489871  1309730 |  179620    2354    20839     8.9 |  1.161 % |
c |      2653 |  489765  1309518 |  197582    2451    22245     9.1 |  1.183 % |
c |      2878 |  489761  1309510 |  217340    2674    24056     9.0 |  1.184 % |
c |      3215 |  489727  1309442 |  239074    2994    29969    10.0 |  1.191 % |
c |      3721 |  489605  1309198 |  262981    3438    34480    10.0 |  1.217 % |
c |      4480 |  489421  1308830 |  289279    4105    39449     9.6 |  1.256 % |
c |      5621 |  489417  1308822 |  318207    5244    54142    10.3 |  1.257 % |
c |      7331 |  489241  1308452 |  350028    6852    70008    10.2 |  1.294 % |
c |      9893 |  488691  1307341 |  385031    9108   110895    12.2 |  1.411 % |
c ==============================================================================
c [1mFound solution: 487424[0m
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     12225 |  488910  1307977 |  162970   11135   128836    11.6 |  1.411 % |
c |     12325 |  488896  1307949 |  179267   11228   129298    11.5 |  1.463 % |
c |     12475 |  488896  1307949 |  197193   11378   130814    11.5 |  1.463 % |
c |     12700 |  488896  1307949 |  216913   11603   133598    11.5 |  1.463 % |
c |     13038 |  488890  1307935 |  238604   11938   137204    11.5 |  1.464 % |
c |     13544 |  488886  1307925 |  262464   12436   141519    11.4 |  1.465 % |
c |     14304 |  488850  1307853 |  288711   13178   151098    11.5 |  1.473 % |
c |     15444 |  488800  1307751 |  317582   14255   162856    11.4 |  1.483 % |
c |     17153 |  488786  1307723 |  349340   15957   200361    12.6 |  1.486 % |
c |     19715 |  488778  1307707 |  384274   18515   233337    12.6 |  1.488 % |
c ==============================================================================
c [1mFound solution: 463872[0m
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     20411 |  488905  1308055 |  162968   19108   239844    12.6 |  1.488 % |
c |     20511 |  488905  1308055 |  179264   19208   240709    12.5 |  1.508 % |
c |     20661 |  488873  1307988 |  197191   19341   241559    12.5 |  1.514 % |
c |     20886 |  488867  1307973 |  216910   19563   243724    12.5 |  1.516 % |
c |     21225 |  488863  1307963 |  238601   19893   247663    12.4 |  1.516 % |
c |     21731 |  488815  1307867 |  262461   20375   253023    12.4 |  1.527 % |
c |     22490 |  488749  1307735 |  288707   21100   261693    12.4 |  1.542 % |
c |     23629 |  488549  1307311 |  317578   21974   269475    12.3 |  1.583 % |
c |     25337 |  488453  1307094 |  349336   23562   294111    12.5 |  1.603 % |
c |     27900 |  488249  1306677 |  384270   26010   344268    13.2 |  1.646 % |
c |     31745 |  488233  1306640 |  422697   29846   429312    14.4 |  1.650 % |
c |     37513 |  488001  1306159 |  464966   35413   496230    14.0 |  1.699 % |
c |     46163 |  487791  1305728 |  511463   43878   733527    16.7 |  1.743 % |
c ==============================================================================
c [1mFound solution: 457728[0m
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     51947 |  487475  1305105 |  162491   49182   801329    16.3 |  1.743 % |
c |     52047 |  487475  1305105 |  178740   49282   802466    16.3 |  1.822 % |
c |     52198 |  487459  1305073 |  196614   49425   804069    16.3 |  1.825 % |
c |     52423 |  487455  1305065 |  216275   49648   806920    16.3 |  1.826 % |
c |     52761 |  487437  1305025 |  237903   49952   812002    16.3 |  1.830 % |
c |     53267 |  487415  1304969 |  261693   50389   819533    16.3 |  1.834 % |
c |     54027 |  487405  1304947 |  287862   51139   830854    16.2 |  1.837 % |
c |     55166 |  487395  1304926 |  316648   52273   850324    16.3 |  1.839 % |
c |     56874 |  487329  1304785 |  348313   53871   873828    16.2 |  1.853 % |
c |     59437 |  487227  1304570 |  383145   56329   915354    16.3 |  1.874 % |
c |     63281 |  487099  1304296 |  421459   60071   969467    16.1 |  1.901 % |
c |     69047 |  486847  1303750 |  463605   65643  1059313    16.1 |  1.955 % |
c ==============================================================================
c [1mFound solution: 453632[0m
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     75281 |  486840  1303766 |  162280   71850  1168327    16.3 |  1.955 % |
c |     75381 |  486840  1303766 |  178508   71950  1168918    16.2 |  1.965 % |
c |     75531 |  486840  1303766 |  196358   72100  1170693    16.2 |  1.965 % |
c |     75756 |  486840  1303766 |  215994   72325  1173705    16.2 |  1.965 % |
c |     76095 |  486840  1303766 |  237594   72664  1180056    16.2 |  1.965 % |
c |     76601 |  486834  1303754 |  261353   73167  1187797    16.2 |  1.967 % |
c |     77360 |  486832  1303750 |  287488   73925  1199875    16.2 |  1.967 % |
c |     78499 |  486832  1303750 |  316237   75063  1218061    16.2 |  1.967 % |
c |     80208 |  486804  1303688 |  347861   76544  1244242    16.3 |  1.973 % |
c |     82770 |  486772  1303616 |  382647   79061  1289433    16.3 |  1.980 % |
c |     86614 |  486704  1303456 |  420912   82751  1347469    16.3 |  1.994 % |
c |     92381 |  486640  1303308 |  463003   88416  1455213    16.5 |  2.008 % |
c |    101030 |  486596  1303202 |  509304   96977  1682591    17.4 |  2.017 % |
c |    114004 |  486486  1302963 |  560234  109673  1950536    17.8 |  2.040 % |
/oldhome/oroussel/solvers/minisat+_script: line 9:  3257 CPU time limit exceeded $XDIR/minisat+_64-bit_static -try "$@"
#### END SOLVER DATA ####
#### BEGIN WATCHER DATA ####
Enforcing CPU limit (will send SIGTERM then SIGKILL): 1200 seconds
Enforcing CPUTime (will send SIGXCPU) limit: 1230 seconds
Enforcing VSIZE limit: 943718400 bytes
Raw data (loadavg): 0.92 0.95 0.92 2/54 3253
Raw data (stat): 3253 (runsolver) R 3252 10795 10794 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 854694103 1052672 99 4294967295 134512640 135381576 3221224464 3221219672 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+9.99943 s]
Raw data (loadavg): 0.93 0.96 0.92 2/55 3257
Raw data (stat): 3253 (minisat+_script) S 3252 10795 10794 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854694103 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 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.0002 s]
Raw data (loadavg): 0.94 0.96 0.92 2/55 3257
Raw data (stat): 3253 (minisat+_script) S 3252 10795 10794 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854694103 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 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+29.9999 s]
Raw data (loadavg): 0.95 0.96 0.92 2/55 3257
Raw data (stat): 3253 (minisat+_script) S 3252 10795 10794 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854694103 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 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+39.9998 s]
Raw data (loadavg): 0.96 0.96 0.92 2/55 3257
Raw data (stat): 3253 (minisat+_script) S 3252 10795 10794 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854694103 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 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.0006 s]
Raw data (loadavg): 0.96 0.96 0.92 2/55 3257
Raw data (stat): 3253 (minisat+_script) S 3252 10795 10794 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854694103 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 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.0007 s]
Raw data (loadavg): 0.97 0.96 0.92 2/55 3257
Raw data (stat): 3253 (minisat+_script) S 3252 10795 10794 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854694103 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 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.0012 s]
Raw data (loadavg): 0.97 0.96 0.92 2/55 3257
Raw data (stat): 3253 (minisat+_script) S 3252 10795 10794 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854694103 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 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.001 s]
Raw data (loadavg): 0.98 0.96 0.92 2/55 3257
Raw data (stat): 3253 (minisat+_script) S 3252 10795 10794 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854694103 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 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.0018 s]
Raw data (loadavg): 0.98 0.96 0.92 2/55 3257
Raw data (stat): 3253 (minisat+_script) S 3252 10795 10794 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854694103 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 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.002 s]
Raw data (loadavg): 0.98 0.96 0.92 2/55 3257
Raw data (stat): 3253 (minisat+_script) S 3252 10795 10794 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854694103 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 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.001 s]
Raw data (loadavg): 0.98 0.97 0.92 2/55 3257
Raw data (stat): 3253 (minisat+_script) S 3252 10795 10794 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854694103 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+120.003 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 3257
Raw data (stat): 3253 (minisat+_script) S 3252 10795 10794 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854694103 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 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.002 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 3257
Raw data (stat): 3253 (minisat+_script) S 3252 10795 10794 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854694103 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 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.003 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 3257
Raw data (stat): 3253 (minisat+_script) S 3252 10795 10794 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854694103 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 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.004 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 3257
Raw data (stat): 3253 (minisat+_script) S 3252 10795 10794 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854694103 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 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.003 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 3257
Raw data (stat): 3253 (minisat+_script) S 3252 10795 10794 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854694103 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 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.004 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 3257
Raw data (stat): 3253 (minisat+_script) S 3252 10795 10794 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854694103 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 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.004 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 3257
Raw data (stat): 3253 (minisat+_script) S 3252 10795 10794 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854694103 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 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.004 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 3257
Raw data (stat): 3253 (minisat+_script) S 3252 10795 10794 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854694103 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 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.004 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 3257
Raw data (stat): 3253 (minisat+_script) S 3252 10795 10794 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854694103 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 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.004 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 3257
Raw data (stat): 3253 (minisat+_script) S 3252 10795 10794 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854694103 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 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.004 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 3257
Raw data (stat): 3253 (minisat+_script) S 3252 10795 10794 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854694103 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 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.004 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 3257
Raw data (stat): 3253 (minisat+_script) S 3252 10795 10794 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854694103 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 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.005 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 3257
Raw data (stat): 3253 (minisat+_script) S 3252 10795 10794 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854694103 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 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.006 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 3257
Raw data (stat): 3253 (minisat+_script) S 3252 10795 10794 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854694103 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 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.01 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 3257
Raw data (stat): 3253 (minisat+_script) S 3252 10795 10794 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854694103 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 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.012 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 3257
Raw data (stat): 3253 (minisat+_script) S 3252 10795 10794 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854694103 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 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.012 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 3257
Raw data (stat): 3253 (minisat+_script) S 3252 10795 10794 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854694103 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 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.043 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 3257
Raw data (stat): 3253 (minisat+_script) S 3252 10795 10794 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854694103 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 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.043 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 3257
Raw data (stat): 3253 (minisat+_script) S 3252 10795 10794 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854694103 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 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.042 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 3257
Raw data (stat): 3253 (minisat+_script) S 3252 10795 10794 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854694103 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 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.043 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 3257
Raw data (stat): 3253 (minisat+_script) S 3252 10795 10794 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854694103 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 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.043 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 3257
Raw data (stat): 3253 (minisat+_script) S 3252 10795 10794 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854694103 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 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.044 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 3257
Raw data (stat): 3253 (minisat+_script) S 3252 10795 10794 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854694103 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 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.044 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 3257
Raw data (stat): 3253 (minisat+_script) S 3252 10795 10794 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854694103 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 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.045 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 3257
Raw data (stat): 3253 (minisat+_script) S 3252 10795 10794 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854694103 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 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.045 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 3257
Raw data (stat): 3253 (minisat+_script) S 3252 10795 10794 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854694103 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 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.045 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 3257
Raw data (stat): 3253 (minisat+_script) S 3252 10795 10794 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854694103 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 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.046 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 3257
Raw data (stat): 3253 (minisat+_script) S 3252 10795 10794 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854694103 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 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.047 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 3257
Raw data (stat): 3253 (minisat+_script) S 3252 10795 10794 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854694103 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 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.047 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 3257
Raw data (stat): 3253 (minisat+_script) S 3252 10795 10794 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854694103 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 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.048 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 3257
Raw data (stat): 3253 (minisat+_script) S 3252 10795 10794 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854694103 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 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.048 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 3257
Raw data (stat): 3253 (minisat+_script) S 3252 10795 10794 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854694103 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 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.049 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 3257
Raw data (stat): 3253 (minisat+_script) S 3252 10795 10794 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854694103 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 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.05 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 3257
Raw data (stat): 3253 (minisat+_script) S 3252 10795 10794 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854694103 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 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.05 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 3257
Raw data (stat): 3253 (minisat+_script) S 3252 10795 10794 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854694103 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 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.051 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 3257
Raw data (stat): 3253 (minisat+_script) S 3252 10795 10794 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854694103 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 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.051 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 3257
Raw data (stat): 3253 (minisat+_script) S 3252 10795 10794 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854694103 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 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.051 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 3257
Raw data (stat): 3253 (minisat+_script) S 3252 10795 10794 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854694103 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 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.052 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 3257
Raw data (stat): 3253 (minisat+_script) S 3252 10795 10794 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854694103 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 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.052 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 3257
Raw data (stat): 3253 (minisat+_script) S 3252 10795 10794 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854694103 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 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.052 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 3257
Raw data (stat): 3253 (minisat+_script) S 3252 10795 10794 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854694103 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 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.052 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 3257
Raw data (stat): 3253 (minisat+_script) S 3252 10795 10794 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854694103 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 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.054 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 3257
Raw data (stat): 3253 (minisat+_script) S 3252 10795 10794 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854694103 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 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.054 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 3257
Raw data (stat): 3253 (minisat+_script) S 3252 10795 10794 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854694103 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 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.054 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 3257
Raw data (stat): 3253 (minisat+_script) S 3252 10795 10794 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854694103 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 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.062 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 3257
Raw data (stat): 3253 (minisat+_script) S 3252 10795 10794 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854694103 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 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.061 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 3257
Raw data (stat): 3253 (minisat+_script) S 3252 10795 10794 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854694103 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 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.062 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 3257
Raw data (stat): 3253 (minisat+_script) S 3252 10795 10794 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854694103 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 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.062 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 3257
Raw data (stat): 3253 (minisat+_script) S 3252 10795 10794 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854694103 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 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.063 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 3257
Raw data (stat): 3253 (minisat+_script) S 3252 10795 10794 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854694103 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 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.062 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 3257
Raw data (stat): 3253 (minisat+_script) S 3252 10795 10794 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854694103 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 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.062 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 3257
Raw data (stat): 3253 (minisat+_script) S 3252 10795 10794 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854694103 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 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.063 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 3257
Raw data (stat): 3253 (minisat+_script) S 3252 10795 10794 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854694103 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 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.063 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 3257
Raw data (stat): 3253 (minisat+_script) S 3252 10795 10794 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854694103 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 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.083 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 3257
Raw data (stat): 3253 (minisat+_script) S 3252 10795 10794 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854694103 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 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.083 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 3257
Raw data (stat): 3253 (minisat+_script) S 3252 10795 10794 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854694103 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 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.084 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 3257
Raw data (stat): 3253 (minisat+_script) S 3252 10795 10794 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854694103 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 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.084 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 3257
Raw data (stat): 3253 (minisat+_script) S 3252 10795 10794 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854694103 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 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.084 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 3257
Raw data (stat): 3253 (minisat+_script) S 3252 10795 10794 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854694103 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 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.084 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 3257
Raw data (stat): 3253 (minisat+_script) S 3252 10795 10794 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854694103 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 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.085 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 3257
Raw data (stat): 3253 (minisat+_script) S 3252 10795 10794 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854694103 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 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.085 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 3257
Raw data (stat): 3253 (minisat+_script) S 3252 10795 10794 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854694103 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 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.086 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 3257
Raw data (stat): 3253 (minisat+_script) S 3252 10795 10794 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854694103 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 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.086 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 3257
Raw data (stat): 3253 (minisat+_script) S 3252 10795 10794 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854694103 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 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.086 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 3257
Raw data (stat): 3253 (minisat+_script) S 3252 10795 10794 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854694103 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 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.086 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 3257
Raw data (stat): 3253 (minisat+_script) S 3252 10795 10794 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854694103 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 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.086 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 3257
Raw data (stat): 3253 (minisat+_script) S 3252 10795 10794 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854694103 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 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.086 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 3257
Raw data (stat): 3253 (minisat+_script) S 3252 10795 10794 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854694103 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 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.086 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 3257
Raw data (stat): 3253 (minisat+_script) S 3252 10795 10794 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854694103 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 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.086 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 3257
Raw data (stat): 3253 (minisat+_script) S 3252 10795 10794 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854694103 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 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.086 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 3257
Raw data (stat): 3253 (minisat+_script) S 3252 10795 10794 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854694103 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 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.086 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 3257
Raw data (stat): 3253 (minisat+_script) S 3252 10795 10794 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854694103 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 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.086 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 3257
Raw data (stat): 3253 (minisat+_script) S 3252 10795 10794 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854694103 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 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.087 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 3257
Raw data (stat): 3253 (minisat+_script) S 3252 10795 10794 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854694103 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 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.087 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 3257
Raw data (stat): 3253 (minisat+_script) S 3252 10795 10794 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854694103 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 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.088 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 3257
Raw data (stat): 3253 (minisat+_script) S 3252 10795 10794 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854694103 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 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.088 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 3257
Raw data (stat): 3253 (minisat+_script) S 3252 10795 10794 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854694103 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 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.09 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 3257
Raw data (stat): 3253 (minisat+_script) S 3252 10795 10794 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854694103 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 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.09 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 3257
Raw data (stat): 3253 (minisat+_script) S 3252 10795 10794 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854694103 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 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.09 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 3257
Raw data (stat): 3253 (minisat+_script) S 3252 10795 10794 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854694103 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 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.091 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 3257
Raw data (stat): 3253 (minisat+_script) S 3252 10795 10794 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854694103 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 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.09 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 3257
Raw data (stat): 3253 (minisat+_script) S 3252 10795 10794 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854694103 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 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.091 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 3257
Raw data (stat): 3253 (minisat+_script) S 3252 10795 10794 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854694103 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 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.092 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 3257
Raw data (stat): 3253 (minisat+_script) S 3252 10795 10794 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854694103 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 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.092 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 3257
Raw data (stat): 3253 (minisat+_script) S 3252 10795 10794 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854694103 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 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.093 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 3257
Raw data (stat): 3253 (minisat+_script) S 3252 10795 10794 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854694103 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 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.093 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 3257
Raw data (stat): 3253 (minisat+_script) S 3252 10795 10794 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854694103 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 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.093 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 3257
Raw data (stat): 3253 (minisat+_script) S 3252 10795 10794 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854694103 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 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.09 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 3257
Raw data (stat): 3253 (minisat+_script) S 3252 10795 10794 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854694103 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 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.09 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 3257
Raw data (stat): 3253 (minisat+_script) S 3252 10795 10794 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854694103 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 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.09 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 3257
Raw data (stat): 3253 (minisat+_script) S 3252 10795 10794 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854694103 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 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.09 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 3257
Raw data (stat): 3253 (minisat+_script) S 3252 10795 10794 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854694103 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 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.09 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 3257
Raw data (stat): 3253 (minisat+_script) S 3252 10795 10794 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854694103 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 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.1 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 3257
Raw data (stat): 3253 (minisat+_script) S 3252 10795 10794 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854694103 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 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.1 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 3257
Raw data (stat): 3253 (minisat+_script) S 3252 10795 10794 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854694103 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 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.1 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 3257
Raw data (stat): 3253 (minisat+_script) S 3252 10795 10794 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854694103 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 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.1 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 3257
Raw data (stat): 3253 (minisat+_script) S 3252 10795 10794 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854694103 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 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.1 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 3257
Raw data (stat): 3253 (minisat+_script) S 3252 10795 10794 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854694103 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 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.1 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 3257
Raw data (stat): 3253 (minisat+_script) S 3252 10795 10794 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854694103 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 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.1 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 3257
Raw data (stat): 3253 (minisat+_script) S 3252 10795 10794 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854694103 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 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.1 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 3257
Raw data (stat): 3253 (minisat+_script) S 3252 10795 10794 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854694103 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 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.1 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 3257
Raw data (stat): 3253 (minisat+_script) S 3252 10795 10794 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854694103 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 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.1 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 3257
Raw data (stat): 3253 (minisat+_script) S 3252 10795 10794 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854694103 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 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.1 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 3257
Raw data (stat): 3253 (minisat+_script) S 3252 10795 10794 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854694103 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 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.1 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 3257
Raw data (stat): 3253 (minisat+_script) S 3252 10795 10794 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854694103 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 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.1 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 3257
Raw data (stat): 3253 (minisat+_script) S 3252 10795 10794 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854694103 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 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.1 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 3257
Raw data (stat): 3253 (minisat+_script) S 3252 10795 10794 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854694103 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 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.1 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 3257
Raw data (stat): 3253 (minisat+_script) S 3252 10795 10794 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854694103 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 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.1 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 3257
Raw data (stat): 3253 (minisat+_script) S 3252 10795 10794 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854694103 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 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.1 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 3257
Raw data (stat): 3253 (minisat+_script) S 3252 10795 10794 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854694103 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 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.1 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 3257
Raw data (stat): 3253 (minisat+_script) S 3252 10795 10794 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854694103 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 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.73 s]
Raw data (loadavg): 0.99 0.97 0.92 1/53 3257
Raw data (stat): 3253 (minisat+_script) S 3252 10795 10794 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854694103 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 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.73
CPU time (s): 1229.88
CPU user time (s): 1229.11
CPU system time (s): 0.766883
CPU usage (%): 100.011
Max. virtual memory (Kb): 2124
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####