PB'05 competition: run trace

Some explanations

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

Name	normalized-opb/mps-v2-13-7/plato.asu.edu/pub/milp/normalized-mps-v2-13-7-neos20.opb
MD5SUM	7fb6e53cf6908940d4f4a33c8adba436
Bench Category	optimization, medium integers (OPTMEDINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	-58624
Optimality of the best value was proved	NO
Number of terms in the objective function	100
Biggest coefficient in the objective function	524288
Number of bits for the biggest coefficient in the objective function	20
Sum of the numbers in the objective function	5242875
Number of bits of the sum of numbers in the objective function	23
Biggest number in a constraint	167772160
Number of bits of the biggest number in a constraint	28
Biggest sum of numbers in a constraint	336554495
Number of bits of the biggest sum of numbers	29
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	7.82681
Number of variables	5948
Total number of constraints	3344
Number of constraints which are clauses	412
Number of constraints which are cardinality constraints (but not clauses)	1282
Number of constraints which are nor clauses,nor cardinality constraints	1650
Minimum length of a constraint	1
Maximum length of a constraint	180
Trace number 14541

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc6 THE 2005-04-21 00:31:15 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=19667 boxname=wulflinc6 idbench=1513 idsolver=11 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  7fb6e53cf6908940d4f4a33c8adba436  /oldhome/oroussel/tmp/wulflinc6/normalized-mps-v2-13-7-neos20.opb
REAL COMMAND:  minisat+ -S /oldhome/oroussel/tmp/wulflinc6/normalized-mps-v2-13-7-neos20.opb /oldhome/oroussel/tmp/wulflinc6/normalized-mps-v2-13-7-neos20.opb
IDLAUNCH: 19667
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.042
cache size	: 512 KB
fdiv_bug	: no
hlt_bug		: no
f00f_bug	: no
coma_bug	: no
fpu		: yes
fpu_exception	: yes
cpuid level	: 2
wp		: yes
flags		: fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse
bogomips	: 888.83

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.042
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:        796716 kB
Buffers:         30388 kB
Cached:         185440 kB
SwapCached:          4 kB
Active:          95124 kB
Inactive:       123200 kB
HighTotal:      131008 kB
HighFree:          252 kB
LowTotal:       903652 kB
LowFree:        796464 kB
SwapTotal:     2097136 kB
SwapFree:      2096768 kB
Dirty:              52 kB
Writeback:           0 kB
Mapped:           5924 kB
Slab:            13944 kB
Committed_AS:    63596 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-21 00:31:27 (client local time) WITH STATUS 30 IN 11.4393 SECONDS
stats: 19667 0 11.4393 30
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 3160 PB-constraints to clauses...
c   -- Unit propagations: pppppp
c   -- Detecting intervals from adjacent constraints: ########################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################
c   -- Clauses(.)/Splits(s): ...............................................................................................................................................................................................................................................................................................................................................................................................................................................................
c ---[3159]---> BDD-cost:    8
c ---[3158]---> BDD-cost:    8
c ---[3157]---> BDD-cost:    8
c ---[3156]---> BDD-cost:    8
c ---[3155]---> BDD-cost:    8
c ---[3154]---> BDD-cost:    8
c ---[3153]---> BDD-cost:    8
c ---[3152]---> BDD-cost:    8
c ---[3151]---> BDD-cost:    8
c ---[3150]---> BDD-cost:    8
c ---[3149]---> BDD-cost:    8
c ---[3148]---> BDD-cost:    8
c ---[3147]---> BDD-cost:    8
c ---[3146]---> BDD-cost:    8
c ---[3145]---> BDD-cost:    8
c ---[3144]---> BDD-cost:    8
c ---[3143]---> BDD-cost:    8
c ---[3142]---> BDD-cost:    8
c ---[3141]---> BDD-cost:    8
c ---[3140]---> BDD-cost:    8
c ---[3139]---> BDD-cost:    8
c ---[3138]---> BDD-cost:    8
c ---[3137]---> BDD-cost:    8
c ---[3136]---> BDD-cost:    8
c ---[3135]---> BDD-cost:    8
c ---[3129]---> BDD-cost:   33
c ---[3128]---> BDD-cost:   33
c ---[3127]---> BDD-cost:   33
c ---[3126]---> BDD-cost:   33
c ---[3124]---> BDD-cost:    4
c ---[3121]---> BDD-cost:    6
c ---[3119]---> BDD-cost:    1
c ---[3117]---> BDD-cost:    1
c ---[3115]---> BDD-cost:    1
c ---[3113]---> BDD-cost:    1
c ---[3112]---> BDD-cost:   33
c ---[3111]---> BDD-cost:    5
c ---[3110]---> BDD-cost:   33
c ---[3109]---> BDD-cost:   33
c ---[3108]---> BDD-cost:    5
c ---[3107]---> BDD-cost:   33
c ---[3106]---> BDD-cost:    5
c ---[3105]---> BDD-cost:   33
c ---[3104]---> BDD-cost:    5
c ---[3103]---> BDD-cost:    4
c ---[3101]---> BDD-cost:    4
c ---[3098]---> BDD-cost:    1
c ---[3096]---> BDD-cost:    6
c ---[3092]---> BDD-cost:   36
c ---[3091]---> BDD-cost:    2
c ---[3089]---> BDD-cost:   33
c ---[3087]---> BDD-cost:    9
c ---[3086]---> BDD-cost:    2
c ---[3083]---> BDD-cost:    9
c ---[3081]---> BDD-cost:   37
c ---[3079]---> BDD-cost:    1
c ---[3078]---> BDD-cost:   33
c ---[3077]---> BDD-cost:    5
c ---[3075]---> BDD-cost:    1
c ---[3073]---> BDD-cost:    1
c ---[3072]---> BDD-cost:   33
c ---[3070]---> BDD-cost:    1
c ---[3068]---> BDD-cost:    1
c ---[3067]---> BDD-cost:   33
c ---[3066]---> BDD-cost:    5
c ---[3065]---> BDD-cost:    5
c ---[3064]---> BDD-cost:    1
c ---[3063]---> BDD-cost:   33
c ---[3062]---> BDD-cost:    5
c ---[3061]---> BDD-cost:   33
c ---[3060]---> BDD-cost:    5
c ---[3058]---> BDD-cost:    1
c ---[3057]---> BDD-cost:    4
c ---[3055]---> BDD-cost:    4
c ---[3052]---> BDD-cost:    6
c ---[3050]---> BDD-cost:    1
c ---[3048]---> BDD-cost:    1
c ---[3046]---> BDD-cost:    1
c ---[3044]---> BDD-cost:    1
c ---[3043]---> BDD-cost:   33
c ---[3042]---> BDD-cost:   33
c ---[3041]---> BDD-cost:    5
c ---[3040]---> BDD-cost:    5
c ---[3039]---> BDD-cost:    1
c ---[3038]---> BDD-cost:   33
c ---[3037]---> BDD-cost:    5
c ---[3036]---> BDD-cost:   33
c ---[3035]---> BDD-cost:    5
c ---[3034]---> BDD-cost:    4
c ---[3032]---> BDD-cost:    4
c ---[3031]---> BDD-cost:   33
c ---[3028]---> BDD-cost:    6
c ---[3026]---> BDD-cost:    1
c ---[3024]---> BDD-cost:    1
c ---[3022]---> BDD-cost:    1
c ---[3020]---> BDD-cost:    1
c ---[3019]---> BDD-cost:   33
c ---[3018]---> BDD-cost:    5
c ---[3017]---> BDD-cost:    5
c ---[3016]---> BDD-cost:    1
c ---[3014]---> BDD-cost:    1
c ---[3013]---> BDD-cost:   33
c ---[3012]---> BDD-cost:    5
c ---[3011]---> BDD-cost:   33
c ---[3010]---> BDD-cost:    5
c ---[3009]---> BDD-cost:    4
c ---[3007]---> BDD-cost:    4
c ---[3004]---> BDD-cost:    6
c ---[3002]---> BDD-cost:   33
c ---[3001]---> BDD-cost:    3
c ---[2999]---> BDD-cost:    1
c ---[2996]---> BDD-cost:    9
c ---[2995]---> BDD-cost:    1
c ---[2992]---> BDD-cost:    9
c ---[2990]---> BDD-cost:   37
c ---[2988]---> BDD-cost:    1
c ---[2987]---> BDD-cost:   33
c ---[2985]---> BDD-cost:    1
c ---[2984]---> BDD-cost:   33
c ---[2983]---> BDD-cost:    5
c ---[2981]---> BDD-cost:    1
c ---[2979]---> BDD-cost:    1
c ---[2977]---> BDD-cost:    1
c ---[2975]---> BDD-cost:    1
c ---[2974]---> BDD-cost:   33
c ---[2973]---> BDD-cost:    5
c ---[2972]---> BDD-cost:   33
c ---[2970]---> BDD-cost:    1
c ---[2969]---> BDD-cost:    5
c ---[2968]---> BDD-cost:   33
c ---[2967]---> BDD-cost:    5
c ---[2966]---> BDD-cost:   33
c ---[2965]---> BDD-cost:    5
c ---[2964]---> BDD-cost:    4
c ---[2962]---> BDD-cost:    4
c ---[2959]---> BDD-cost:    6
c ---[2958]---> BDD-cost:    1
c ---[2956]---> BDD-cost:    1
c ---[2954]---> BDD-cost:    1
c ---[2952]---> BDD-cost:    1
c ---[2950]---> BDD-cost:    1
c ---[2949]---> BDD-cost:   33
c ---[2948]---> BDD-cost:    5
c ---[2947]---> BDD-cost:    5
c ---[2946]---> BDD-cost:    1
c ---[2945]---> BDD-cost:   33
c ---[2944]---> BDD-cost:    5
c ---[2943]---> BDD-cost:   33
c ---[2942]---> BDD-cost:   33
c ---[2941]---> BDD-cost:    5
c ---[2940]---> BDD-cost:    4
c ---[2938]---> BDD-cost:    4
c ---[2935]---> BDD-cost:    6
c ---[2933]---> BDD-cost:    1
c ---[2931]---> BDD-cost:    1
c ---[2929]---> BDD-cost:    1
c ---[2927]---> BDD-cost:    1
c ---[2925]---> BDD-cost:    1
c ---[2924]---> BDD-cost:   33
c ---[2923]---> BDD-cost:    5
c ---[2922]---> BDD-cost:    5
c ---[2921]---> BDD-cost:    1
c ---[2920]---> BDD-cost:   33
c ---[2919]---> BDD-cost:    5
c ---[2918]---> BDD-cost:   33
c ---[2917]---> BDD-cost:    5
c ---[2916]---> BDD-cost:    4
c ---[2915]---> BDD-cost:    2
c ---[2913]---> BDD-cost:    4
c ---[2910]---> BDD-cost:    6
c ---[2908]---> BDD-cost:    3
c ---[2906]---> BDD-cost:    2
c ---[2904]---> BDD-cost:    2
c ---[2903]---> BDD-cost:    2
c ---[2900]---> BDD-cost:    9
c ---[2899]---> BDD-cost:    2
c ---[2896]---> BDD-cost:    9
c ---[2894]---> BDD-cost:   37
c ---[2892]---> BDD-cost:    1
c ---[2891]---> BDD-cost:    2
c ---[2890]---> BDD-cost:    1
c ---[2889]---> BDD-cost:    1
c ---[2887]---> BDD-cost:    0
c ---[2885]---> BDD-cost:    0
c ---[2883]---> BDD-cost:    0
c ---[2881]---> BDD-cost:    1
c ---[2880]---> BDD-cost:    0
c ---[2879]---> BDD-cost:    0
c ---[2878]---> BDD-cost:    0
c ---[2877]---> BDD-cost:    0
c ---[2875]---> BDD-cost:   33
c ---[2874]---> BDD-cost:    5
c ---[2873]---> BDD-cost:   33
c ---[2872]---> BDD-cost:    5
c ---[2871]---> BDD-cost:    4
c ---[2869]---> BDD-cost:    4
c ---[2866]---> BDD-cost:    6
c ---[2864]---> BDD-cost:    1
c ---[2863]---> BDD-cost:    2
c ---[2861]---> BDD-cost:    1
c ---[2859]---> BDD-cost:    0
c ---[2857]---> BDD-cost:    0
c ---[2856]---> BDD-cost:    1
c ---[2855]---> BDD-cost:    1
c ---[2854]---> BDD-cost:   33
c ---[2853]---> BDD-cost:    5
c ---[2852]---> BDD-cost:   33
c ---[2851]---> BDD-cost:    5
c ---[2850]---> BDD-cost:    0
c ---[2849]---> BDD-cost:   33
c ---[2847]---> BDD-cost:    0
c ---[2846]---> BDD-cost:    4
c ---[2844]---> BDD-cost:    4
c ---[2841]---> BDD-cost:    6
c ---[2839]---> BDD-cost:    0
c ---[2837]---> BDD-cost:    0
c ---[2835]---> BDD-cost:    1
c ---[2833]---> BDD-cost:    0
c ---[2832]---> BDD-cost:    2
c ---[2831]---> BDD-cost:    0
c ---[2830]---> BDD-cost:    0
c ---[2829]---> BDD-cost:    0
c ---[2828]---> BDD-cost:    0
c ---[2827]---> BDD-cost:   33
c ---[2826]---> BDD-cost:    5
c ---[2825]---> BDD-cost:    0
c ---[2824]---> BDD-cost:    0
c ---[2823]---> BDD-cost:    4
c ---[2820]---> BDD-cost:    4
c ---[2817]---> BDD-cost:    6
c ---[2815]---> BDD-cost:    3
c ---[2813]---> BDD-cost:    1
c ---[2810]---> BDD-cost:    9
c ---[2809]---> BDD-cost:    2
c ---[2808]---> BDD-cost:    1
c ---[2805]---> BDD-cost:    9
c ---[2803]---> BDD-cost:   37
c ---[2801]---> BDD-cost:    1
c ---[2800]---> BDD-cost:    1
c ---[2799]---> BDD-cost:    1
c ---[2797]---> BDD-cost:    0
c ---[2795]---> BDD-cost:    1
c ---[2793]---> BDD-cost:    0
c ---[2790]---> BDD-cost:    0
c ---[2789]---> BDD-cost:    0
c ---[2788]---> BDD-cost:    0
c ---[2787]---> BDD-cost:   33
c ---[2786]---> BDD-cost:    5
c ---[2785]---> BDD-cost:    0
c ---[2784]---> BDD-cost:    0
c ---[2783]---> BDD-cost:    0
c ---[2782]---> BDD-cost:    0
c ---[2781]---> BDD-cost:    3
c ---[2780]---> BDD-cost:    2
c ---[2778]---> BDD-cost:    4
c ---[2775]---> BDD-cost:    6
c ---[2773]---> BDD-cost:    0
c ---[2771]---> BDD-cost:    0
c ---[2769]---> BDD-cost:    1
c ---[2767]---> BDD-cost:    1
c ---[2766]---> BDD-cost:    0
c ---[2765]---> BDD-cost:    0
c ---[2763]---> BDD-cost:    5
c ---[2762]---> BDD-cost:    1
c ---[2761]---> BDD-cost:   33
c ---[2760]---> BDD-cost:    5
c ---[2759]---> BDD-cost:    1
c ---[2758]---> BDD-cost:    1
c ---[2757]---> BDD-cost:    4
c ---[2755]---> BDD-cost:    4
c ---[2753]---> BDD-cost:    2
c ---[2751]---> BDD-cost:    6
c ---[2749]---> BDD-cost:    1
c ---[2747]---> BDD-cost:    0
c ---[2745]---> BDD-cost:    0
c ---[2743]---> BDD-cost:    0
c ---[2742]---> BDD-cost:   33
c ---[2741]---> BDD-cost:    5
c ---[2740]---> BDD-cost:    5
c ---[2739]---> BDD-cost:    1
c ---[2738]---> BDD-cost:    0
c ---[2736]---> BDD-cost:    0
c ---[2735]---> BDD-cost:    0
c ---[2734]---> BDD-cost:    0
c ---[2733]---> BDD-cost:    3
c ---[2731]---> BDD-cost:    4
c ---[2728]---> BDD-cost:    6
c ---[2726]---> BDD-cost:    2
c ---[2725]---> BDD-cost:    3
c ---[2723]---> BDD-cost:    2
c ---[2722]---> BDD-cost:    2
c ---[2721]---> BDD-cost:    2
c ---[2718]---> BDD-cost:    9
c ---[2717]---> BDD-cost:    2
c ---[2716]---> BDD-cost:    1
c ---[2712]---> BDD-cost:    9
c ---[2710]---> BDD-cost:   37
c ---[2708]---> BDD-cost:    1
c ---[2707]---> BDD-cost:    1
c ---[2706]---> BDD-cost:    1
c ---[2704]---> BDD-cost:    0
c ---[2702]---> BDD-cost:    0
c ---[2700]---> BDD-cost:    1
c ---[2698]---> BDD-cost:    1
c ---[2697]---> BDD-cost:    2
c ---[2696]---> BDD-cost:    0
c ---[2695]---> BDD-cost:    0
c ---[2694]---> BDD-cost:    0
c ---[2693]---> BDD-cost:    0
c ---[2692]---> BDD-cost:   33
c ---[2691]---> BDD-cost:    5
c ---[2690]---> BDD-cost:   33
c ---[2689]---> BDD-cost:    5
c ---[2688]---> BDD-cost:    4
c ---[2685]---> BDD-cost:    4
c ---[2682]---> BDD-cost:    6
c ---[2680]---> BDD-cost:    0
c ---[2678]---> BDD-cost:    0
c ---[2676]---> BDD-cost:    0
c ---[2674]---> BDD-cost:    0
c ---[2673]---> BDD-cost:    0
c ---[2672]---> BDD-cost:    0
c ---[2671]---> BDD-cost:    0
c ---[2670]---> BDD-cost:    2
c ---[2669]---> BDD-cost:    0
c ---[2668]---> BDD-cost:   33
c ---[2667]---> BDD-cost:    5
c ---[2666]---> BDD-cost:    0
c ---[2665]---> BDD-cost:    0
c ---[2664]---> BDD-cost:    4
c ---[2662]---> BDD-cost:    4
c ---[2659]---> BDD-cost:    6
c ---[2656]---> BDD-cost:    0
c ---[2654]---> BDD-cost:    0
c ---[2652]---> BDD-cost:    0
c ---[2650]---> BDD-cost:    0
c ---[2649]---> BDD-cost:    0
c ---[2648]---> BDD-cost:    0
c ---[2647]---> BDD-cost:    0
c ---[2646]---> BDD-cost:    0
c ---[2645]---> BDD-cost:   33
c ---[2644]---> BDD-cost:    5
c ---[2643]---> BDD-cost:    2
c ---[2642]---> BDD-cost:    0
c ---[2641]---> BDD-cost:    0
c ---[2640]---> BDD-cost:    4
c ---[2638]---> BDD-cost:    4
c ---[2635]---> BDD-cost:    6
c ---[2634]---> BDD-cost:    1
c ---[2630]---> BDD-cost:    9
c ---[2629]---> BDD-cost:    1
c ---[2626]---> BDD-cost:    9
c ---[2624]---> BDD-cost:   37
c ---[2622]---> BDD-cost:    1
c ---[2621]---> BDD-cost:    1
c ---[2620]---> BDD-cost:    1
c ---[2618]---> BDD-cost:    1
c ---[2617]---> BDD-cost:    2
c ---[2615]---> BDD-cost:    1
c ---[2613]---> BDD-cost:    0
c ---[2611]---> BDD-cost:    0
c ---[2610]---> BDD-cost:   33
c ---[2609]---> BDD-cost:    5
c ---[2608]---> BDD-cost:   33
c ---[2607]---> BDD-cost:    5
c ---[2606]---> BDD-cost:    0
c ---[2605]---> BDD-cost:    0
c ---[2604]---> BDD-cost:    0
c ---[2602]---> BDD-cost:    0
c ---[2601]---> BDD-cost:    3
c ---[2599]---> BDD-cost:    4
c ---[2596]---> BDD-cost:    6
c ---[2594]---> BDD-cost:    0
c ---[2592]---> BDD-cost:    0
c ---[2590]---> BDD-cost:    0
c ---[2588]---> BDD-cost:    0
c ---[2587]---> BDD-cost:    2
c ---[2586]---> BDD-cost:    0
c ---[2585]---> BDD-cost:    0
c ---[2584]---> BDD-cost:    5
c ---[2583]---> BDD-cost:    1
c ---[2582]---> BDD-cost:    0
c ---[2581]---> BDD-cost:    0
c ---[2580]---> BDD-cost:    0
c ---[2579]---> BDD-cost:    0
c ---[2578]---> BDD-cost:    3
c ---[2575]---> BDD-cost:    1
c ---[2573]---> BDD-cost:    4
c ---[2570]---> BDD-cost:    6
c ---[2568]---> BDD-cost:    0
c ---[2566]---> BDD-cost:    0
c ---[2564]---> BDD-cost:    0
c ---[2562]---> BDD-cost:    0
c ---[2561]---> BDD-cost:    0
c ---[2560]---> BDD-cost:    0
c ---[2559]---> BDD-cost:    0
c ---[2558]---> BDD-cost:    2
c ---[2557]---> BDD-cost:    0
c ---[2556]---> BDD-cost:    0
c ---[2555]---> BDD-cost:    0
c ---[2554]---> BDD-cost:    0
c ---[2553]---> BDD-cost:    0
c ---[2552]---> BDD-cost:    3
c ---[2550]---> BDD-cost:    4
c ---[2547]---> BDD-cost:    6
c ---[2543]---> BDD-cost:   36
c ---[2542]---> BDD-cost:    2
c ---[2539]---> BDD-cost:    9
c ---[2538]---> BDD-cost:    2
c ---[2537]---> BDD-cost:    2
c ---[2534]---> BDD-cost:    9
c ---[2532]---> BDD-cost:   37
c ---[2530]---> BDD-cost:    1
c ---[2529]---> BDD-cost:    1
c ---[2528]---> BDD-cost:    1
c ---[2526]---> BDD-cost:    0
c ---[2524]---> BDD-cost:    0
c ---[2522]---> BDD-cost:    0
c ---[2519]---> BDD-cost:    0
c ---[2518]---> BDD-cost:    0
c ---[2517]---> BDD-cost:    0
c ---[2516]---> BDD-cost:    0
c ---[2515]---> BDD-cost:    0
c ---[2514]---> BDD-cost:    0
c ---[2513]---> BDD-cost:    0
c ---[2512]---> BDD-cost:    0
c ---[2511]---> BDD-cost:    0
c ---[2510]---> BDD-cost:    4
c ---[2509]---> BDD-cost:    2
c ---[2507]---> BDD-cost:    4
c ---[2504]---> BDD-cost:    6
c ---[2502]---> BDD-cost:    0
c ---[2500]---> BDD-cost:    0
c ---[2498]---> BDD-cost:    0
c ---[2496]---> BDD-cost:    0
c ---[2495]---> BDD-cost:    0
c ---[2494]---> BDD-cost:    0
c ---[2492]---> BDD-cost:    5
c ---[2491]---> BDD-cost:    1
c ---[2490]---> BDD-cost:   33
c ---[2489]---> BDD-cost:    5
c ---[2488]---> BDD-cost:    0
c ---[2487]---> BDD-cost:    0
c ---[2486]---> BDD-cost:    4
c ---[2484]---> BDD-cost:    4
c ---[2482]---> BDD-cost:    2
c ---[2480]---> BDD-cost:    6
c ---[2478]---> BDD-cost:    0
c ---[2476]---> BDD-cost:    0
c ---[2474]---> BDD-cost:    0
c ---[2472]---> BDD-cost:    0
c ---[2471]---> BDD-cost:    0
c ---[2470]---> BDD-cost:    0
c ---[2469]---> BDD-cost:    0
c ---[2468]---> BDD-cost:    0
c ---[2467]---> BDD-cost:    0
c ---[2465]---> BDD-cost:    0
c ---[2464]---> BDD-cost:    0
c ---[2463]---> BDD-cost:    0
c ---[2462]---> BDD-cost:    4
c ---[2460]---> BDD-cost:    4
c ---[2457]---> BDD-cost:    6
c ---[2455]---> BDD-cost:    2
c ---[2454]---> BDD-cost:    3
c ---[2452]---> BDD-cost:    1
c ---[2449]---> BDD-cost:    9
c ---[2448]---> BDD-cost:    1
c ---[2445]---> BDD-cost:    9
c ---[2443]---> BDD-cost:   37
c ---[2441]---> BDD-cost:    1
c ---[2440]---> BDD-cost:    1
c ---[2438]---> BDD-cost:    1
c ---[2437]---> BDD-cost:    1
c ---[2435]---> BDD-cost:    0
c ---[2433]---> BDD-cost:    0
c ---[2431]---> BDD-cost:    0
c ---[2429]---> BDD-cost:    0
c ---[2428]---> BDD-cost:    0
c ---[2427]---> BDD-cost:    0
c ---[2426]---> BDD-cost:    0
c ---[2425]---> BDD-cost:    0
c ---[2424]---> BDD-cost:    2
c ---[2423]---> BDD-cost:    0
c ---[2422]---> BDD-cost:    0
c ---[2421]---> BDD-cost:    0
c ---[2420]---> BDD-cost:    0
c ---[2419]---> BDD-cost:    3
c ---[2417]---> BDD-cost:    4
c ---[2414]---> BDD-cost:    6
c ---[2412]---> BDD-cost:    0
c ---[2409]---> BDD-cost:    0
c ---[2407]---> BDD-cost:    0
c ---[2405]---> BDD-cost:    0
c ---[2404]---> BDD-cost:    0
c ---[2403]---> BDD-cost:    0
c ---[2402]---> BDD-cost:    5
c ---[2401]---> BDD-cost:    1
c ---[2400]---> BDD-cost:   33
c ---[2399]---> BDD-cost:    5
c ---[2398]---> BDD-cost:    0
c ---[2397]---> BDD-cost:    2
c ---[2396]---> BDD-cost:    0
c ---[2395]---> BDD-cost:    4
c ---[2393]---> BDD-cost:    4
c ---[2390]---> BDD-cost:    6
c ---[2388]---> BDD-cost:    0
c ---[2386]---> BDD-cost:    0
c ---[2384]---> BDD-cost:    0
c ---[2382]---> BDD-cost:    0
c ---[2380]---> BDD-cost:    0
c ---[2379]---> BDD-cost:    0
c ---[2378]---> BDD-cost:    0
c ---[2377]---> BDD-cost:    0
c ---[2376]---> BDD-cost:    0
c ---[2375]---> BDD-cost:    0
c ---[2374]---> BDD-cost:    0
c ---[2373]---> BDD-cost:    0
c ---[2372]---> BDD-cost:    3
c ---[2369]---> BDD-cost:   18
c ---[2368]---> BDD-cost:    4
c ---[2365]---> BDD-cost:    6
c ---[2363]---> BDD-cost:    3
c ---[2361]---> BDD-cost:    2
c ---[2360]---> BDD-cost:    2
c ---[2358]---> BDD-cost:    2
c ---[2355]---> BDD-cost:    9
c ---[2354]---> BDD-cost:    2
c ---[2351]---> BDD-cost:    9
c ---[2349]---> BDD-cost:   37
c ---[2347]---> BDD-cost:    1
c ---[2346]---> BDD-cost:    1
c ---[2345]---> BDD-cost:    3
c ---[2344]---> BDD-cost:    1
c ---[2342]---> BDD-cost:    0
c ---[2340]---> BDD-cost:    0
c ---[2338]---> BDD-cost:    0
c ---[2336]---> BDD-cost:    0
c ---[2335]---> BDD-cost:    0
c ---[2334]---> BDD-cost:    0
c ---[2333]---> BDD-cost:    0
c ---[2332]---> BDD-cost:    0
c ---[2331]---> BDD-cost:    0
c ---[2329]---> BDD-cost:   18
c ---[2328]---> BDD-cost:    0
c ---[2327]---> BDD-cost:    0
c ---[2326]---> BDD-cost:    0
c ---[2325]---> BDD-cost:    4
c ---[2323]---> BDD-cost:    4
c ---[2320]---> BDD-cost:    6
c ---[2318]---> BDD-cost:    0
c ---[2316]---> BDD-cost:    0
c ---[2313]---> BDD-cost:    0
c ---[2311]---> BDD-cost:    0
c ---[2310]---> BDD-cost:    0
c ---[2309]---> BDD-cost:    0
c ---[2308]---> BDD-cost:    0
c ---[2307]---> BDD-cost:    0
c ---[2306]---> BDD-cost:   33
c ---[2305]---> BDD-cost:    5
c ---[2304]---> BDD-cost:    0
c ---[2303]---> BDD-cost:    0
c ---[2302]---> BDD-cost:    1
c ---[2301]---> BDD-cost:    3
c ---[2300]---> BDD-cost:    4
c ---[2298]---> BDD-cost:    4
c ---[2295]---> BDD-cost:    6
c ---[2293]---> BDD-cost:    0
c ---[2291]---> BDD-cost:    0
c ---[2289]---> BDD-cost:    0
c ---[2287]---> BDD-cost:    0
c ---[2286]---> BDD-cost:    0
c ---[2284]---> BDD-cost:   18
c ---[2283]---> BDD-cost:    0
c ---[2282]---> BDD-cost:    0
c ---[2281]---> BDD-cost:    0
c ---[2280]---> BDD-cost:    0
c ---[2279]---> BDD-cost:    0
c ---[2278]---> BDD-cost:    0
c ---[2277]---> BDD-cost:    0
c ---[2276]---> BDD-cost:    4
c ---[2274]---> BDD-cost:    4
c ---[2270]---> BDD-cost:    6
c ---[2269]---> BDD-cost:    1
c ---[2266]---> BDD-cost:    9
c ---[2265]---> BDD-cost:    1
c ---[2262]---> BDD-cost:    9
c ---[2261]---> BDD-cost:    3
c ---[2259]---> BDD-cost:   37
c ---[2257]---> BDD-cost:    1
c ---[2256]---> BDD-cost:    1
c ---[2255]---> BDD-cost:    1
c ---[2253]---> BDD-cost:    0
c ---[2251]---> BDD-cost:    0
c ---[2249]---> BDD-cost:    0
c ---[2247]---> BDD-cost:    0
c ---[2246]---> BDD-cost:    0
c ---[2245]---> BDD-cost:    0
c ---[2243]---> BDD-cost:   18
c ---[2242]---> BDD-cost:    0
c ---[2241]---> BDD-cost:    0
c ---[2240]---> BDD-cost:    0
c ---[2239]---> BDD-cost:    0
c ---[2238]---> BDD-cost:    0
c ---[2237]---> BDD-cost:    0
c ---[2236]---> BDD-cost:    3
c ---[2234]---> BDD-cost:    4
c ---[2230]---> BDD-cost:    6
c ---[2228]---> BDD-cost:    0
c ---[2226]---> BDD-cost:    0
c ---[2224]---> BDD-cost:    0
c ---[2222]---> BDD-cost:    0
c ---[2221]---> BDD-cost:    0
c ---[2220]---> BDD-cost:    0
c ---[2219]---> BDD-cost:    5
c ---[2218]---> BDD-cost:    1
c ---[2217]---> BDD-cost:    0
c ---[2216]---> BDD-cost:    3
c ---[2215]---> BDD-cost:    0
c ---[2214]---> BDD-cost:    0
c ---[2213]---> BDD-cost:    0
c ---[2212]---> BDD-cost:    3
c ---[2210]---> BDD-cost:    4
c ---[2207]---> BDD-cost:    6
c ---[2205]---> BDD-cost:    0
c ---[2203]---> BDD-cost:    0
c ---[2201]---> BDD-cost:   18
c ---[2199]---> BDD-cost:    0
c ---[2197]---> BDD-cost:    0
c ---[2196]---> BDD-cost:    0
c ---[2195]---> BDD-cost:    0
c ---[2194]---> BDD-cost:    0
c ---[2193]---> BDD-cost:    0
c ---[2192]---> BDD-cost:    0
c ---[2191]---> BDD-cost:    0
c ---[2190]---> BDD-cost:    0
c ---[2189]---> BDD-cost:    0
c ---[2187]---> BDD-cost:    3
c ---[2185]---> BDD-cost:    4
c ---[2182]---> BDD-cost:    6
c ---[2180]---> BDD-cost:    3
c ---[2178]---> BDD-cost:   36
c ---[2177]---> BDD-cost:    2
c ---[2174]---> BDD-cost:    9
c ---[2173]---> BDD-cost:    2
c ---[2170]---> BDD-cost:    9
c ---[2168]---> BDD-cost:   37
c ---[2166]---> BDD-cost:    1
c ---[2164]---> BDD-cost:    1
c ---[2163]---> BDD-cost:    4
c ---[2162]---> BDD-cost:    1
c ---[2161]---> BDD-cost:    1
c ---[2159]---> BDD-cost:    0
c ---[2157]---> BDD-cost:    0
c ---[2155]---> BDD-cost:    0
c ---[2153]---> BDD-cost:    0
c ---[2152]---> BDD-cost:    0
c ---[2151]---> BDD-cost:    0
c ---[2150]---> BDD-cost:    0
c ---[2149]---> BDD-cost:    0
c ---[2147]---> BDD-cost:    0
c ---[2146]---> BDD-cost:    0
c ---[2145]---> BDD-cost:    0
c ---[2144]---> BDD-cost:    0
c ---[2143]---> BDD-cost:    4
c ---[2141]---> BDD-cost:    4
c ---[2138]---> BDD-cost:    6
c ---[2136]---> BDD-cost:    0
c ---[2135]---> BDD-cost:    4
c ---[2133]---> BDD-cost:    0
c ---[2131]---> BDD-cost:    0
c ---[2129]---> BDD-cost:    0
c ---[2128]---> BDD-cost:    0
c ---[2127]---> BDD-cost:    0
c ---[2126]---> BDD-cost:    0
c ---[2125]---> BDD-cost:    0
c ---[2124]---> BDD-cost:    0
c ---[2123]---> BDD-cost:    0
c ---[2122]---> BDD-cost:    0
c ---[2120]---> BDD-cost:    0
c ---[2119]---> BDD-cost:    4
c ---[2117]---> BDD-cost:    4
c ---[2114]---> BDD-cost:    6
c ---[2112]---> BDD-cost:    0
c ---[2110]---> BDD-cost:    0
c ---[2108]---> BDD-cost:    0
c ---[2106]---> BDD-cost:    0
c ---[2105]---> BDD-cost:    4
c ---[2104]---> BDD-cost:    0
c ---[2103]---> BDD-cost:    0
c ---[2102]---> BDD-cost:    0
c ---[2101]---> BDD-cost:    0
c ---[2100]---> BDD-cost:    0
c ---[2099]---> BDD-cost:    0
c ---[2098]---> BDD-cost:    0
c ---[2097]---> BDD-cost:    0
c ---[2096]---> BDD-cost:    4
c ---[2093]---> BDD-cost:    4
c ---[2090]---> BDD-cost:    6
c ---[2089]---> BDD-cost:    1
c ---[2086]---> BDD-cost:    9
c ---[2085]---> BDD-cost:    1
c ---[2083]---> BDD-cost:    4
c ---[2081]---> BDD-cost:    9
c ---[2079]---> BDD-cost:   37
c ---[2077]---> BDD-cost:    1
c ---[2076]---> BDD-cost:    1
c ---[2075]---> BDD-cost:    1
c ---[2073]---> BDD-cost:    0
c ---[2071]---> BDD-cost:    0
c ---[2069]---> BDD-cost:    0
c ---[2067]---> BDD-cost:    0
c ---[2066]---> BDD-cost:    0
c ---[2064]---> BDD-cost:    0
c ---[2063]---> BDD-cost:    0
c ---[2062]---> BDD-cost:    0
c ---[2061]---> BDD-cost:    0
c ---[2060]---> BDD-cost:    0
c ---[2059]---> BDD-cost:    0
c ---[2058]---> BDD-cost:    0
c ---[2057]---> BDD-cost:    3
c ---[2055]---> BDD-cost:    4
c ---[2053]---> BDD-cost:    7
c ---[2050]---> BDD-cost:    6
c ---[2048]---> BDD-cost:    0
c ---[2046]---> BDD-cost:    0
c ---[2044]---> BDD-cost:    0
c ---[2042]---> BDD-cost:    0
c ---[2041]---> BDD-cost:    0
c ---[2040]---> BDD-cost:    0
c ---[2039]---> BDD-cost:    0
c ---[2038]---> BDD-cost:    0
c ---[2037]---> BDD-cost:    4
c ---[2036]---> BDD-cost:    0
c ---[2035]---> BDD-cost:    0
c ---[2034]---> BDD-cost:    0
c ---[2033]---> BDD-cost:    0
c ---[2032]---> BDD-cost:    3
c ---[2030]---> BDD-cost:    4
c ---[2027]---> BDD-cost:    6
c ---[2025]---> BDD-cost:    0
c ---[2024]---> BDD-cost:    1
c ---[2021]---> BDD-cost:    0
c ---[2019]---> BDD-cost:    0
c ---[2017]---> BDD-cost:    0
c ---[2016]---> BDD-cost:    0
c ---[2015]---> BDD-cost:    0
c ---[2014]---> BDD-cost:    0
c ---[2013]---> BDD-cost:    0
c ---[2012]---> BDD-cost:    0
c ---[2011]---> BDD-cost:    0
c ---[2010]---> BDD-cost:    0
c ---[2009]---> BDD-cost:    4
c ---[2008]---> BDD-cost:    0
c ---[2007]---> BDD-cost:    4
c ---[2005]---> BDD-cost:    4
c ---[2002]---> BDD-cost:    6
c ---[1998]---> BDD-cost:   36
c ---[1996]---> BDD-cost:   48
c ---[1994]---> BDD-cost:    1
c ---[1992]---> BDD-cost:    1
c ---[1990]---> BDD-cost:    9
c ---[1988]---> BDD-cost:    9
c ---[1986]---> BDD-cost:    9
c ---[1984]---> BDD-cost:    5
c ---[1983]---> BDD-cost:    4
c ---[1981]---> BDD-cost:    5
c ---[1979]---> BDD-cost:    5
c ---[1977]---> BDD-cost:    5
c ---[1975]---> BDD-cost:   13
c ---[1974]---> BDD-cost:    2
c ---[1971]---> BDD-cost:   16
c ---[1970]---> BDD-cost:    2
c ---[1967]---> BDD-cost:   18
c ---[1965]---> BDD-cost:    2
c ---[1962]---> BDD-cost:   21
c ---[1961]---> BDD-cost:    2
c ---[1958]---> BDD-cost:   22
c ---[1957]---> BDD-cost:    2
c ---[1954]---> BDD-cost:   16
c ---[1953]---> BDD-cost:    2
c ---[1952]---> BDD-cost:    4
c ---[1949]---> BDD-cost:   18
c ---[1948]---> BDD-cost:    2
c ---[1945]---> BDD-cost:   21
c ---[1944]---> BDD-cost:    2
c ---[1941]---> BDD-cost:   22
c ---[1940]---> BDD-cost:    2
c ---[1936]---> BDD-cost:   20
c ---[1935]---> BDD-cost:    2
c ---[1932]---> BDD-cost:   21
c ---[1931]---> BDD-cost:    2
c ---[1928]---> BDD-cost:   19
c ---[1927]---> BDD-cost:    2
c ---[1924]---> BDD-cost:   21
c ---[1922]---> BDD-cost:    7
c ---[1921]---> BDD-cost:    2
c ---[1918]---> BDD-cost:   20
c ---[1917]---> BDD-cost:    2
c ---[1914]---> BDD-cost:   21
c ---[1913]---> BDD-cost:    2
c ---[1910]---> BDD-cost:   19
c ---[1909]---> BDD-cost:    2
c ---[1908]---> BDD-cost:    4
c ---[1905]---> BDD-cost:   21
c ---[1904]---> BDD-cost:    2
c ---[1901]---> BDD-cost:   21
c ---[1900]---> BDD-cost:    2
c ---[1897]---> BDD-cost:   21
c ---[1896]---> BDD-cost:    2
c ---[1892]---> BDD-cost:   21
c ---[1891]---> BDD-cost:    2
c ---[1888]---> BDD-cost:   21
c ---[1887]---> BDD-cost:    2
c ---[1884]---> BDD-cost:   21
c ---[1883]---> BDD-cost:    2
c ---[1880]---> BDD-cost:   21
c ---[1879]---> BDD-cost:    1
c ---[1878]---> BDD-cost:    4
c ---[1877]---> BDD-cost:    2
c ---[1874]---> BDD-cost:   21
c ---[1873]---> BDD-cost:    2
c ---[1870]---> BDD-cost:   21
c ---[1869]---> BDD-cost:    2
c ---[1866]---> BDD-cost:   20
c ---[1865]---> BDD-cost:    2
c ---[1861]---> BDD-cost:   20
c ---[1860]---> BDD-cost:    2
c ---[1857]---> BDD-cost:   23
c ---[1856]---> BDD-cost:    2
c ---[1853]---> BDD-cost:   19
c ---[1852]---> BDD-cost:    2
c ---[1850]---> BDD-cost:    4
c ---[1848]---> BDD-cost:   20
c ---[1847]---> BDD-cost:    2
c ---[1844]---> BDD-cost:   20
c ---[1843]---> BDD-cost:    2
c ---[1840]---> BDD-cost:   23
c ---[1839]---> BDD-cost:    2
c ---[1836]---> BDD-cost:   19
c ---[1834]---> BDD-cost:    2
c ---[1832]---> BDD-cost:    2
c ---[1830]---> BDD-cost:    2
c ---[1828]---> BDD-cost:    2
c ---[1827]---> BDD-cost:    4
c ---[1825]---> BDD-cost:    2
c ---[1823]---> BDD-cost:    2
c ---[1821]---> BDD-cost:    2
c ---[1818]---> BDD-cost:    2
c ---[1815]---> Sorter-cost: 2445     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1813]---> Sorter-cost: 2387     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1811]---> Sorter-cost: 2387     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1809]---> Sorter-cost: 2505     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1807]---> BDD-cost:   10
c ---[1805]---> BDD-cost:    7
c ---[1803]---> BDD-cost:   10
c ---[1801]---> BDD-cost:   10
c ---[1799]---> BDD-cost:   25
c ---[1797]---> BDD-cost:   25
c ---[1795]---> BDD-cost:   25
c ---[1793]---> BDD-cost:   11
c ---[1791]---> BDD-cost:   11
c ---[1789]---> BDD-cost:   11
c ---[1788]---> BDD-cost:    4
c ---[1786]---> BDD-cost:   28
c ---[1784]---> BDD-cost:   28
c ---[1782]---> BDD-cost:   28
c ---[1780]---> BDD-cost:   25
c ---[1778]---> BDD-cost:   81
c ---[1776]---> Sorter-cost:  364     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1774]---> Sorter-cost:  578     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1772]---> BDD-cost:   55
c ---[1769]---> Sorter-cost:  355     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1767]---> Sorter-cost:  460     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1765]---> Sorter-cost:  761     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1763]---> BDD-cost:   55
c ---[1761]---> Sorter-cost:  355     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1759]---> Sorter-cost:  460     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1757]---> Sorter-cost:  761     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1755]---> BDD-cost:   55
c ---[1753]---> Sorter-cost:  355     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1751]---> Sorter-cost:  280     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1750]---> BDD-cost:    4
c ---[1748]---> Sorter-cost:  559     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1746]---> BDD-cost:   25
c ---[1744]---> BDD-cost:   25
c ---[1742]---> BDD-cost:   25
c ---[1740]---> BDD-cost:   75
c ---[1738]---> BDD-cost:    0
c ---[1736]---> BDD-cost:    0
c ---[1734]---> BDD-cost:    0
c ---[1732]---> BDD-cost:    0
c ---[1731]---> BDD-cost:    0
c ---[1729]---> BDD-cost:    1
c ---[1727]---> BDD-cost:    1
c ---[1725]---> BDD-cost:    0
c ---[1724]---> BDD-cost:   33
c ---[1723]---> BDD-cost:    5
c ---[1722]---> BDD-cost:   33
c ---[1721]---> BDD-cost:    5
c ---[1720]---> BDD-cost:    0
c ---[1719]---> BDD-cost:    0
c ---[1718]---> BDD-cost:    4
c ---[1716]---> BDD-cost:    3
c ---[1715]---> BDD-cost:    4
c ---[1712]---> BDD-cost:    6
c ---[1709]---> BDD-cost:    0
c ---[1707]---> BDD-cost:    0
c ---[1705]---> BDD-cost:    0
c ---[1703]---> BDD-cost:    0
c ---[1702]---> BDD-cost:    0
c ---[1701]---> BDD-cost:    0
c ---[1700]---> BDD-cost:   33
c ---[1698]---> BDD-cost:    5
c ---[1697]---> BDD-cost:   33
c ---[1696]---> BDD-cost:    5
c ---[1695]---> BDD-cost:    0
c ---[1694]---> BDD-cost:    0
c ---[1693]---> BDD-cost:    4
c ---[1691]---> BDD-cost:    3
c ---[1688]---> BDD-cost:    6
c ---[1687]---> BDD-cost:    4
c ---[1684]---> BDD-cost:    0
c ---[1682]---> BDD-cost:    0
c ---[1680]---> BDD-cost:    0
c ---[1678]---> BDD-cost:    0
c ---[1677]---> BDD-cost:    0
c ---[1676]---> BDD-cost:    0
c ---[1675]---> BDD-cost:   33
c ---[1674]---> BDD-cost:    5
c ---[1673]---> BDD-cost:   33
c ---[1671]---> BDD-cost:    5
c ---[1670]---> BDD-cost:    0
c ---[1669]---> BDD-cost:    0
c ---[1668]---> BDD-cost:    3
c ---[1666]---> BDD-cost:    3
c ---[1663]---> BDD-cost:    6
c ---[1660]---> BDD-cost:    0
c ---[1658]---> BDD-cost:    7
c ---[1656]---> BDD-cost:    0
c ---[1654]---> BDD-cost:    0
c ---[1652]---> BDD-cost:    0
c ---[1651]---> BDD-cost:    0
c ---[1650]---> BDD-cost:    0
c ---[1649]---> BDD-cost:   33
c ---[1648]---> BDD-cost:    5
c ---[1647]---> BDD-cost:   33
c ---[1646]---> BDD-cost:    5
c ---[1645]---> BDD-cost:    0
c ---[1644]---> BDD-cost:    4
c ---[1643]---> BDD-cost:    0
c ---[1642]---> BDD-cost:    3
c ---[1640]---> BDD-cost:    3
c ---[1637]---> BDD-cost:    6
c ---[1634]---> BDD-cost:    0
c ---[1632]---> BDD-cost:    0
c ---[1630]---> BDD-cost:    0
c ---[1627]---> BDD-cost:    0
c ---[1626]---> BDD-cost:    0
c ---[1625]---> BDD-cost:    0
c ---[1624]---> BDD-cost:   33
c ---[1623]---> BDD-cost:    5
c ---[1622]---> BDD-cost:   33
c ---[1621]---> BDD-cost:    5
c ---[1620]---> BDD-cost:    0
c ---[1619]---> BDD-cost:    0
c ---[1618]---> BDD-cost:    3
c ---[1617]---> BDD-cost:    4
c ---[1615]---> BDD-cost:    3
c ---[1612]---> BDD-cost:    6
c ---[1609]---> BDD-cost:    0
c ---[1607]---> BDD-cost:    0
c ---[1605]---> BDD-cost:    0
c ---[1603]---> BDD-cost:    0
c ---[1602]---> BDD-cost:    0
c ---[1600]---> BDD-cost:    0
c ---[1599]---> BDD-cost:   33
c ---[1598]---> BDD-cost:    5
c ---[1597]---> BDD-cost:   33
c ---[1596]---> BDD-cost:    5
c ---[1595]---> BDD-cost:    0
c ---[1594]---> BDD-cost:    0
c ---[1593]---> BDD-cost:    3
c ---[1591]---> BDD-cost:    3
c ---[1590]---> BDD-cost:    1
c ---[1589]---> BDD-cost:    4
c ---[1586]---> BDD-cost:    6
c ---[1584]---> BDD-cost:   10
c ---[1582]---> BDD-cost:    3
c ---[1581]---> BDD-cost:   10
c ---[1578]---> BDD-cost:    3
c ---[1577]---> BDD-cost:   10
c ---[1575]---> BDD-cost:    3
c ---[1574]---> BDD-cost:   10
c ---[1573]---> BDD-cost:   10
c ---[1572]---> BDD-cost:    4
c ---[1569]---> BDD-cost:    7
c ---[1568]---> BDD-cost:    2
c ---[1565]---> BDD-cost:    9
c ---[1564]---> BDD-cost:    2
c ---[1562]---> BDD-cost:    1
c ---[1560]---> BDD-cost:    9
c ---[1559]---> BDD-cost:    2
c ---[1556]---> BDD-cost:    9
c ---[1555]---> BDD-cost:    2
c ---[1552]---> BDD-cost:    9
c ---[1550]---> Sorter-cost:  285     Base: 2 2 2 2 2 2 2
c ---[1548]---> BDD-cost:    1
c ---[1547]---> BDD-cost:    1
c ---[1545]---> BDD-cost:    1
c ---[1542]---> BDD-cost:    9
c ---[1541]---> BDD-cost:    1
c ---[1538]---> BDD-cost:    9
c ---[1537]---> BDD-cost:    1
c ---[1534]---> BDD-cost:    9
c ---[1533]---> BDD-cost:    1
c ---[1531]---> BDD-cost:    1
c ---[1529]---> BDD-cost:    9
c ---[1527]---> Sorter-cost:  285     Base: 2 2 2 2 2 2 2
c ---[1525]---> BDD-cost:    1
c ---[1524]---> BDD-cost:    2
c ---[1521]---> BDD-cost:    9
c ---[1520]---> BDD-cost:    2
c ---[1517]---> BDD-cost:    9
c ---[1516]---> BDD-cost:    2
c ---[1515]---> BDD-cost:    1
c ---[1512]---> BDD-cost:    9
c ---[1511]---> BDD-cost:    2
c ---[1508]---> BDD-cost:    9
c ---[1506]---> Sorter-cost:  285     Base: 2 2 2 2 2 2 2
c ---[1504]---> BDD-cost:    1
c ---[1503]---> BDD-cost:    1
c ---[1500]---> BDD-cost:    9
c ---[1498]---> BDD-cost:    1
c ---[1497]---> BDD-cost:    1
c ---[1494]---> BDD-cost:    9
c ---[1493]---> BDD-cost:    1
c ---[1490]---> BDD-cost:    9
c ---[1489]---> BDD-cost:    1
c ---[1486]---> BDD-cost:    9
c ---[1484]---> Sorter-cost:  285     Base: 2 2 2 2 2 2 2
c ---[1483]---> BDD-cost:    1
c ---[1481]---> BDD-cost:    1
c ---[1480]---> BDD-cost:    2
c ---[1477]---> BDD-cost:    9
c ---[1476]---> BDD-cost:    2
c ---[1473]---> BDD-cost:    9
c ---[1472]---> BDD-cost:    2
c ---[1469]---> BDD-cost:    9
c ---[1468]---> BDD-cost:    1
c ---[1467]---> BDD-cost:    2
c ---[1464]---> BDD-cost:    9
c ---[1462]---> Sorter-cost:  285     Base: 2 2 2 2 2 2 2
c ---[1460]---> BDD-cost:    1
c ---[1459]---> BDD-cost:    1
c ---[1456]---> BDD-cost:    9
c ---[1455]---> BDD-cost:    1
c ---[1452]---> BDD-cost:    1
c ---[1450]---> BDD-cost:    9
c ---[1449]---> BDD-cost:    1
c ---[1446]---> BDD-cost:    9
c ---[1445]---> BDD-cost:    1
c ---[1442]---> BDD-cost:    9
c ---[1440]---> Sorter-cost:  285     Base: 2 2 2 2 2 2 2
c ---[1438]---> BDD-cost:    1
c ---[1437]---> BDD-cost:    2
c ---[1436]---> BDD-cost:    1
c ---[1435]---> BDD-cost:    2
c ---[1432]---> BDD-cost:    9
c ---[1431]---> BDD-cost:    2
c ---[1428]---> BDD-cost:    9
c ---[1427]---> BDD-cost:    2
c ---[1424]---> BDD-cost:    9
c ---[1423]---> BDD-cost:    2
c ---[1419]---> BDD-cost:    9
c ---[1417]---> Sorter-cost:  285     Base: 2 2 2 2 2 2 2
c ---[1415]---> BDD-cost:    1
c ---[1414]---> BDD-cost:    1
c ---[1411]---> BDD-cost:    9
c ---[1410]---> BDD-cost:    1
c ---[1407]---> BDD-cost:    9
c ---[1406]---> BDD-cost:    1
c ---[1405]---> BDD-cost:    2
c ---[1402]---> BDD-cost:    9
c ---[1401]---> BDD-cost:    1
c ---[1398]---> BDD-cost:    9
c ---[1396]---> Sorter-cost:  285     Base: 2 2 2 2 2 2 2
c ---[1394]---> BDD-cost:    1
c ---[1393]---> BDD-cost:    2
c ---[1390]---> BDD-cost:    9
c ---[1388]---> BDD-cost:    2
c ---[1385]---> BDD-cost:    9
c ---[1384]---> BDD-cost:    2
c ---[1381]---> BDD-cost:    9
c ---[1380]---> BDD-cost:    2
c ---[1377]---> BDD-cost:    9
c ---[1375]---> Sorter-cost:  285     Base: 2 2 2 2 2 2 2
c ---[1374]---> BDD-cost:    2
c ---[1372]---> BDD-cost:    1
c ---[1371]---> BDD-cost:    1
c ---[1368]---> BDD-cost:    9
c ---[1367]---> BDD-cost:    1
c ---[1364]---> BDD-cost:    9
c ---[1363]---> BDD-cost:    1
c ---[1360]---> BDD-cost:    9
c ---[1358]---> BDD-cost:    1
c ---[1355]---> BDD-cost:    9
c ---[1353]---> Sorter-cost:  285     Base: 2 2 2 2 2 2 2
c ---[1351]---> BDD-cost:    1
c ---[1350]---> BDD-cost:    2
c ---[1347]---> BDD-cost:    9
c ---[1346]---> BDD-cost:    2
c ---[1344]---> BDD-cost:    2
c ---[1342]---> BDD-cost:    9
c ---[1341]---> BDD-cost:    2
c ---[1338]---> BDD-cost:    9
c ---[1337]---> BDD-cost:    2
c ---[1334]---> BDD-cost:    9
c ---[1332]---> Sorter-cost:  285     Base: 2 2 2 2 2 2 2
c ---[1330]---> BDD-cost:    1
c ---[1329]---> BDD-cost:    1
c ---[1325]---> BDD-cost:    9
c ---[1324]---> BDD-cost:    1
c ---[1321]---> BDD-cost:    9
c ---[1320]---> BDD-cost:    1
c ---[1317]---> BDD-cost:    9
c ---[1316]---> BDD-cost:    1
c ---[1314]---> BDD-cost:    2
c ---[1312]---> BDD-cost:    9
c ---[1310]---> Sorter-cost:  285     Base: 2 2 2 2 2 2 2
c ---[1308]---> BDD-cost:    1
c ---[1307]---> BDD-cost:    2
c ---[1304]---> BDD-cost:    9
c ---[1303]---> BDD-cost:    2
c ---[1300]---> BDD-cost:    9
c ---[1299]---> BDD-cost:    2
c ---[1295]---> BDD-cost:    9
c ---[1294]---> BDD-cost:    2
c ---[1291]---> BDD-cost:    9
c ---[1289]---> Sorter-cost:  285     Base: 2 2 2 2 2 2 2
c ---[1287]---> BDD-cost:    1
c ---[1286]---> BDD-cost:    1
c ---[1283]---> BDD-cost:    9
c ---[1282]---> BDD-cost:   33
c ---[1281]---> BDD-cost:    2
c ---[1280]---> BDD-cost:    1
c ---[1277]---> BDD-cost:    9
c ---[1276]---> BDD-cost:    1
c ---[1273]---> BDD-cost:    9
c ---[1272]---> BDD-cost:    1
c ---[1269]---> BDD-cost:    9
c ---[1267]---> Sorter-cost:  285     Base: 2 2 2 2 2 2 2
c ---[1264]---> BDD-cost:    1
c ---[1263]---> BDD-cost:    2
c ---[1260]---> BDD-cost:    9
c ---[1259]---> BDD-cost:    2
c ---[1256]---> BDD-cost:    9
c ---[1255]---> BDD-cost:    2
c ---[1252]---> BDD-cost:    9
c ---[1251]---> BDD-cost:    2
c ---[1250]---> BDD-cost:    2
c ---[1247]---> BDD-cost:    9
c ---[1245]---> Sorter-cost:  285     Base: 2 2 2 2 2 2 2
c ---[1243]---> BDD-cost:    1
c ---[1242]---> BDD-cost:    1
c ---[1239]---> BDD-cost:    9
c ---[1238]---> BDD-cost:    1
c ---[1234]---> BDD-cost:    9
c ---[1233]---> BDD-cost:    1
c ---[1230]---> BDD-cost:    9
c ---[1229]---> BDD-cost:    1
c ---[1226]---> BDD-cost:    9
c ---[1224]---> Sorter-cost:  285     Base: 2 2 2 2 2 2 2
c ---[1222]---> BDD-cost:    1
c ---[1221]---> BDD-cost:    2
c ---[1220]---> BDD-cost:    2
c ---[1217]---> BDD-cost:    9
c ---[1216]---> BDD-cost:    2
c ---[1213]---> BDD-cost:    9
c ---[1212]---> BDD-cost:    2
c ---[1209]---> BDD-cost:    9
c ---[1208]---> BDD-cost:    2
c ---[1204]---> BDD-cost:    9
c ---[1202]---> Sorter-cost:  285     Base: 2 2 2 2 2 2 2
c ---[1200]---> BDD-cost:    1
c ---[1199]---> BDD-cost:    1
c ---[1196]---> BDD-cost:    9
c ---[1195]---> BDD-cost:    1
c ---[1192]---> BDD-cost:    9
c ---[1191]---> BDD-cost:    1
c ---[1190]---> BDD-cost:    2
c ---[1187]---> BDD-cost:    9
c ---[1186]---> BDD-cost:    1
c ---[1183]---> BDD-cost:    9
c ---[1181]---> Sorter-cost:  285     Base: 2 2 2 2 2 2 2
c ---[1179]---> BDD-cost:    1
c ---[1178]---> BDD-cost:    2
c ---[1175]---> BDD-cost:    9
c ---[1173]---> BDD-cost:    2
c ---[1170]---> BDD-cost:    9
c ---[1169]---> BDD-cost:    2
c ---[1166]---> BDD-cost:    9
c ---[1165]---> BDD-cost:    2
c ---[1162]---> BDD-cost:    9
c ---[1160]---> Sorter-cost:  285     Base: 2 2 2 2 2 2 2
c ---[1159]---> BDD-cost:    2
c ---[1157]---> BDD-cost:    1
c ---[1156]---> BDD-cost:    1
c ---[1153]---> BDD-cost:    9
c ---[1152]---> BDD-cost:    1
c ---[1149]---> BDD-cost:    9
c ---[1148]---> BDD-cost:    1
c ---[1145]---> BDD-cost:    9
c ---[1143]---> BDD-cost:    1
c ---[1140]---> BDD-cost:    9
c ---[1138]---> Sorter-cost:  285     Base: 2 2 2 2 2 2 2
c ---[1136]---> BDD-cost:    1
c ---[1135]---> BDD-cost:    2
c ---[1132]---> BDD-cost:    9
c ---[1131]---> BDD-cost:    2
c ---[1128]---> BDD-cost:    1
c ---[1127]---> BDD-cost:    2
c ---[1125]---> BDD-cost:    9
c ---[1123]---> BDD-cost:   37
c ---[1121]---> BDD-cost:    1
c ---[1120]---> BDD-cost:    1
c ---[1119]---> BDD-cost:    1
c ---[1117]---> BDD-cost:    0
c ---[1115]---> BDD-cost:    0
c ---[1113]---> BDD-cost:    0
c ---[1111]---> BDD-cost:    0
c ---[1110]---> BDD-cost:    0
c ---[1108]---> BDD-cost:    0
c ---[1107]---> BDD-cost:    5
c ---[1106]---> BDD-cost:    1
c ---[1105]---> BDD-cost:    0
c ---[1104]---> BDD-cost:    0
c ---[1103]---> BDD-cost:    0
c ---[1102]---> BDD-cost:    0
c ---[1101]---> BDD-cost:    3
c ---[1099]---> BDD-cost:    4
c ---[1098]---> BDD-cost:    2
c ---[1095]---> BDD-cost:    6
c ---[1093]---> BDD-cost:    0
c ---[1091]---> BDD-cost:    0
c ---[1089]---> BDD-cost:    0
c ---[1087]---> BDD-cost:    0
c ---[1086]---> BDD-cost:    0
c ---[1085]---> BDD-cost:    0
c ---[1084]---> BDD-cost:   33
c ---[1083]---> BDD-cost:    5
c ---[1081]---> BDD-cost:    0
c ---[1080]---> BDD-cost:    0
c ---[1079]---> BDD-cost:    0
c ---[1078]---> BDD-cost:    0
c ---[1077]---> BDD-cost:    3
c ---[1075]---> BDD-cost:    4
c ---[1072]---> BDD-cost:    6
c ---[1070]---> BDD-cost:    0
c ---[1069]---> BDD-cost:    2
c ---[1067]---> BDD-cost:    0
c ---[1065]---> BDD-cost:    0
c ---[1063]---> BDD-cost:    0
c ---[1062]---> BDD-cost:    0
c ---[1061]---> BDD-cost:    0
c ---[1060]---> BDD-cost:    5
c ---[1059]---> BDD-cost:    1
c ---[1058]---> BDD-cost:    0
c ---[1057]---> BDD-cost:    0
c ---[1056]---> BDD-cost:    0
c ---[1054]---> BDD-cost:    0
c ---[1053]---> BDD-cost:    3
c ---[1051]---> BDD-cost:    4
c ---[1048]---> BDD-cost:    6
c ---[1046]---> BDD-cost:    3
c ---[1044]---> BDD-cost:    2
c ---[1043]---> BDD-cost:    1
c ---[1040]---> BDD-cost:    9
c ---[1039]---> BDD-cost:    1
c ---[1036]---> BDD-cost:    9
c ---[1034]---> BDD-cost:   37
c ---[1032]---> BDD-cost:    1
c ---[1031]---> BDD-cost:    1
c ---[1030]---> BDD-cost:    1
c ---[1027]---> BDD-cost:    0
c ---[1025]---> BDD-cost:    0
c ---[1023]---> BDD-cost:    0
c ---[1021]---> BDD-cost:    0
c ---[1020]---> BDD-cost:    0
c ---[1019]---> BDD-cost:    0
c ---[1018]---> BDD-cost:    0
c ---[1017]---> BDD-cost:    0
c ---[1016]---> BDD-cost:   33
c ---[1015]---> BDD-cost:    5
c ---[1014]---> BDD-cost:    2
c ---[1013]---> BDD-cost:    0
c ---[1012]---> BDD-cost:    0
c ---[1011]---> BDD-cost:    3
c ---[1009]---> BDD-cost:    4
c ---[1006]---> BDD-cost:    6
c ---[1004]---> BDD-cost:    0
c ---[1002]---> BDD-cost:    0
c ---[1000]---> BDD-cost:    0
c ---[ 997]---> BDD-cost:    0
c ---[ 996]---> BDD-cost:    0
c ---[ 995]---> BDD-cost:    0
c ---[ 994]---> BDD-cost:    0
c ---[ 993]---> BDD-cost:    0
c ---[ 992]---> BDD-cost:    0
c ---[ 991]---> BDD-cost:    0
c ---[ 990]---> BDD-cost:    0
c ---[ 989]---> BDD-cost:    0
c ---[ 988]---> BDD-cost:    3
c ---[ 987]---> BDD-cost:    1
c ---[ 986]---> BDD-cost:    2
c ---[ 984]---> BDD-cost:    4
c ---[ 981]---> BDD-cost:    6
c ---[ 979]---> BDD-cost:    0
c ---[ 977]---> BDD-cost:    0
c ---[ 975]---> BDD-cost:    0
c ---[ 973]---> BDD-cost:    0
c ---[ 972]---> BDD-cost:    0
c ---[ 971]---> BDD-cost:    0
c ---[ 969]---> BDD-cost:    0
c ---[ 968]---> BDD-cost:    0
c ---[ 967]---> BDD-cost:   33
c ---[ 966]---> BDD-cost:    5
c ---[ 965]---> BDD-cost:    0
c ---[ 964]---> BDD-cost:    0
c ---[ 963]---> BDD-cost:    4
c ---[ 961]---> BDD-cost:    4
c ---[ 959]---> BDD-cost:    2
c ---[ 957]---> BDD-cost:    6
c ---[ 955]---> BDD-cost:    3
c ---[ 953]---> BDD-cost:    2
c ---[ 952]---> BDD-cost:    2
c ---[ 951]---> BDD-cost:    2
c ---[ 947]---> BDD-cost:    9
c ---[ 946]---> BDD-cost:    2
c ---[ 943]---> BDD-cost:    9
c ---[ 941]---> BDD-cost:   37
c ---[ 939]---> BDD-cost:    1
c ---[ 938]---> BDD-cost:    1
c ---[ 937]---> BDD-cost:    1
c ---[ 935]---> BDD-cost:    0
c ---[ 934]---> BDD-cost:    2
c ---[ 932]---> BDD-cost:    0
c ---[ 930]---> BDD-cost:    0
c ---[ 928]---> BDD-cost:    0
c ---[ 927]---> BDD-cost:    0
c ---[ 926]---> BDD-cost:    0
c ---[ 925]---> BDD-cost:    5
c ---[ 924]---> BDD-cost:    1
c ---[ 923]---> BDD-cost:    0
c ---[ 922]---> BDD-cost:    0
c ---[ 921]---> BDD-cost:    0
c ---[ 919]---> BDD-cost:    0
c ---[ 918]---> BDD-cost:    4
c ---[ 916]---> BDD-cost:    4
c ---[ 913]---> BDD-cost:    6
c ---[ 911]---> BDD-cost:    0
c ---[ 909]---> BDD-cost:    0
c ---[ 907]---> BDD-cost:    0
c ---[ 905]---> BDD-cost:    0
c ---[ 904]---> BDD-cost:    2
c ---[ 903]---> BDD-cost:    0
c ---[ 902]---> BDD-cost:    0
c ---[ 901]---> BDD-cost:    0
c ---[ 900]---> BDD-cost:    0
c ---[ 899]---> BDD-cost:    0
c ---[ 898]---> BDD-cost:    0
c ---[ 897]---> BDD-cost:    0
c ---[ 896]---> BDD-cost:    0
c ---[ 895]---> BDD-cost:    4
c ---[ 892]---> BDD-cost:    4
c ---[ 889]---> BDD-cost:    6
c ---[ 887]---> BDD-cost:    0
c ---[ 885]---> BDD-cost:    0
c ---[ 883]---> BDD-cost:    0
c ---[ 881]---> BDD-cost:    0
c ---[ 880]---> BDD-cost:    0
c ---[ 879]---> BDD-cost:    0
c ---[ 878]---> BDD-cost:    0
c ---[ 877]---> BDD-cost:    2
c ---[ 876]---> BDD-cost:    0
c ---[ 875]---> BDD-cost:    0
c ---[ 874]---> BDD-cost:    0
c ---[ 873]---> BDD-cost:    0
c ---[ 872]---> BDD-cost:    0
c ---[ 871]---> BDD-cost:    4
c ---[ 869]---> BDD-cost:    4
c ---[ 866]---> BDD-cost:    6
c ---[ 863]---> BDD-cost:    3
c ---[ 861]---> BDD-cost:    1
c ---[ 858]---> BDD-cost:    9
c ---[ 857]---> BDD-cost:    1
c ---[ 854]---> BDD-cost:    9
c ---[ 853]---> BDD-cost:    1
c ---[ 851]---> BDD-cost:   18
c ---[ 849]---> BDD-cost:   37
c ---[ 847]---> BDD-cost:    1
c ---[ 846]---> BDD-cost:    1
c ---[ 845]---> BDD-cost:    1
c ---[ 843]---> BDD-cost:    0
c ---[ 841]---> BDD-cost:    0
c ---[ 839]---> BDD-cost:    0
c ---[ 837]---> BDD-cost:    0
c ---[ 836]---> BDD-cost:    0
c ---[ 835]---> BDD-cost:    0
c ---[ 833]---> BDD-cost:    0
c ---[ 832]---> BDD-cost:    0
c ---[ 831]---> BDD-cost:   33
c ---[ 830]---> BDD-cost:    5
c ---[ 829]---> BDD-cost:    0
c ---[ 828]---> BDD-cost:    0
c ---[ 827]---> BDD-cost:    3
c ---[ 825]---> BDD-cost:    4
c ---[ 823]---> BDD-cost:    3
c ---[ 821]---> BDD-cost:    6
c ---[ 819]---> BDD-cost:    0
c ---[ 817]---> BDD-cost:    0
c ---[ 815]---> BDD-cost:    0
c ---[ 813]---> BDD-cost:    0
c ---[ 812]---> BDD-cost:    0
c ---[ 811]---> BDD-cost:    0
c ---[ 810]---> BDD-cost:    0
c ---[ 809]---> BDD-cost:    0
c ---[ 808]---> BDD-cost:    0
c ---[ 806]---> BDD-cost:   18
c ---[ 805]---> BDD-cost:    0
c ---[ 804]---> BDD-cost:    0
c ---[ 803]---> BDD-cost:    0
c ---[ 802]---> BDD-cost:    3
c ---[ 800]---> BDD-cost:    4
c ---[ 797]---> BDD-cost:    6
c ---[ 795]---> BDD-cost:    0
c ---[ 793]---> BDD-cost:    0
c ---[ 790]---> BDD-cost:    0
c ---[ 788]---> BDD-cost:    0
c ---[ 787]---> BDD-cost:    0
c ---[ 786]---> BDD-cost:    0
c ---[ 785]---> BDD-cost:    0
c ---[ 784]---> BDD-cost:    0
c ---[ 783]---> BDD-cost:    0
c ---[ 782]---> BDD-cost:    0
c ---[ 781]---> BDD-cost:    0
c ---[ 780]---> BDD-cost:    0
c ---[ 779]---> BDD-cost:    3
c ---[ 778]---> BDD-cost:    3
c ---[ 776]---> BDD-cost:    4
c ---[ 773]---> BDD-cost:    6
c ---[ 771]---> BDD-cost:    3
c ---[ 769]---> BDD-cost:    2
c ---[ 767]---> BDD-cost:   18
c ---[ 766]---> BDD-cost:    2
c ---[ 765]---> BDD-cost:    2
c ---[ 762]---> BDD-cost:    9
c ---[ 761]---> BDD-cost:    2
c ---[ 758]---> BDD-cost:    9
c ---[ 756]---> BDD-cost:   37
c ---[ 753]---> BDD-cost:    1
c ---[ 752]---> BDD-cost:    1
c ---[ 751]---> BDD-cost:    1
c ---[ 749]---> BDD-cost:    0
c ---[ 747]---> BDD-cost:    0
c ---[ 745]---> BDD-cost:    0
c ---[ 743]---> BDD-cost:    0
c ---[ 742]---> BDD-cost:    0
c ---[ 741]---> BDD-cost:    0
c ---[ 740]---> BDD-cost:    0
c ---[ 739]---> BDD-cost:    3
c ---[ 738]---> BDD-cost:    0
c ---[ 737]---> BDD-cost:    0
c ---[ 736]---> BDD-cost:    0
c ---[ 735]---> BDD-cost:    0
c ---[ 734]---> BDD-cost:    0
c ---[ 733]---> BDD-cost:    4
c ---[ 731]---> BDD-cost:    4
c ---[ 728]---> BDD-cost:    6
c ---[ 726]---> BDD-cost:   18
c ---[ 724]---> BDD-cost:    0
c ---[ 722]---> BDD-cost:    0
c ---[ 720]---> BDD-cost:    0
c ---[ 718]---> BDD-cost:    0
c ---[ 717]---> BDD-cost:    0
c ---[ 716]---> BDD-cost:    0
c ---[ 715]---> BDD-cost:    0
c ---[ 714]---> BDD-cost:    0
c ---[ 713]---> BDD-cost:    0
c ---[ 712]---> BDD-cost:    0
c ---[ 710]---> BDD-cost:    1
c ---[ 708]---> BDD-cost:    0
c ---[ 707]---> BDD-cost:    0
c ---[ 706]---> BDD-cost:    4
c ---[ 704]---> BDD-cost:    4
c ---[ 701]---> BDD-cost:    6
c ---[ 699]---> BDD-cost:    0
c ---[ 697]---> BDD-cost:    0
c ---[ 695]---> BDD-cost:    0
c ---[ 694]---> BDD-cost:    3
c ---[ 692]---> BDD-cost:    0
c ---[ 691]---> BDD-cost:    0
c ---[ 690]---> BDD-cost:    0
c ---[ 689]---> BDD-cost:    0
c ---[ 688]---> BDD-cost:    0
c ---[ 687]---> BDD-cost:    0
c ---[ 686]---> BDD-cost:    0
c ---[ 685]---> BDD-cost:    0
c ---[ 684]---> BDD-cost:    0
c ---[ 683]---> BDD-cost:    4
c ---[ 681]---> BDD-cost:   18
c ---[ 679]---> BDD-cost:    4
c ---[ 676]---> BDD-cost:    6
c ---[ 674]---> BDD-cost:    3
c ---[ 672]---> BDD-cost:    1
c ---[ 668]---> BDD-cost:    9
c ---[ 667]---> BDD-cost:    1
c ---[ 664]---> BDD-cost:    9
c ---[ 662]---> BDD-cost:   37
c ---[ 660]---> BDD-cost:    1
c ---[ 659]---> BDD-cost:    1
c ---[ 658]---> BDD-cost:    1
c ---[ 656]---> BDD-cost:    0
c ---[ 654]---> BDD-cost:    0
c ---[ 653]---> BDD-cost:    3
c ---[ 651]---> BDD-cost:    0
c ---[ 649]---> BDD-cost:    0
c ---[ 648]---> BDD-cost:    0
c ---[ 647]---> BDD-cost:    0
c ---[ 646]---> BDD-cost:    0
c ---[ 645]---> BDD-cost:    0
c ---[ 644]---> BDD-cost:    0
c ---[ 643]---> BDD-cost:    0
c ---[ 642]---> BDD-cost:    0
c ---[ 641]---> BDD-cost:    0
c ---[ 640]---> BDD-cost:    1
c ---[ 639]---> BDD-cost:    3
c ---[ 637]---> BDD-cost:    4
c ---[ 634]---> BDD-cost:    6
c ---[ 632]---> BDD-cost:    0
c ---[ 630]---> BDD-cost:    0
c ---[ 628]---> BDD-cost:    0
c ---[ 626]---> BDD-cost:    0
c ---[ 625]---> BDD-cost:    0
c ---[ 624]---> BDD-cost:    1
c ---[ 623]---> BDD-cost:    0
c ---[ 622]---> BDD-cost:    0
c ---[ 621]---> BDD-cost:    0
c ---[ 620]---> BDD-cost:    0
c ---[ 619]---> BDD-cost:    0
c ---[ 618]---> BDD-cost:    0
c ---[ 617]---> BDD-cost:    0
c ---[ 616]---> BDD-cost:    3
c ---[ 614]---> BDD-cost:    4
c ---[ 612]---> BDD-cost:    1
c ---[ 609]---> BDD-cost:    6
c ---[ 607]---> BDD-cost:    0
c ---[ 605]---> BDD-cost:    0
c ---[ 603]---> BDD-cost:    0
c ---[ 601]---> BDD-cost:    0
c ---[ 600]---> BDD-cost:    0
c ---[ 599]---> BDD-cost:    0
c ---[ 598]---> BDD-cost:    0
c ---[ 597]---> BDD-cost:    0
c ---[ 596]---> BDD-cost:    1
c ---[ 595]---> BDD-cost:    0
c ---[ 594]---> BDD-cost:    0
c ---[ 593]---> BDD-cost:    0
c ---[ 592]---> BDD-cost:    0
c ---[ 591]---> BDD-cost:    3
c ---[ 589]---> BDD-cost:    4
c ---[ 586]---> BDD-cost:    6
c ---[ 584]---> BDD-cost:    1
c ---[ 583]---> BDD-cost:    3
c ---[ 581]---> BDD-cost:    2
c ---[ 580]---> BDD-cost:    2
c ---[ 579]---> BDD-cost:    2
c ---[ 576]---> BDD-cost:    9
c ---[ 575]---> BDD-cost:    1
c ---[ 573]---> BDD-cost:    1
c ---[ 572]---> BDD-cost:    2
c ---[ 569]---> BDD-cost:    9
c ---[ 567]---> BDD-cost:   37
c ---[ 565]---> BDD-cost:    1
c ---[ 564]---> BDD-cost:    1
c ---[ 563]---> BDD-cost:    1
c ---[ 561]---> BDD-cost:    0
c ---[ 559]---> BDD-cost:    0
c ---[ 557]---> BDD-cost:    0
c ---[ 556]---> BDD-cost:    1
c ---[ 554]---> BDD-cost:    0
c ---[ 553]---> BDD-cost:    0
c ---[ 552]---> BDD-cost:    0
c ---[ 551]---> BDD-cost:    0
c ---[ 550]---> BDD-cost:    0
c ---[ 549]---> BDD-cost:    0
c ---[ 548]---> BDD-cost:    0
c ---[ 547]---> BDD-cost:    0
c ---[ 546]---> BDD-cost:    0
c ---[ 545]---> BDD-cost:    3
c ---[ 544]---> BDD-cost:    1
c ---[ 542]---> BDD-cost:    4
c ---[ 539]---> BDD-cost:    6
c ---[ 537]---> BDD-cost:    0
c ---[ 535]---> BDD-cost:    0
c ---[ 533]---> BDD-cost:    0
c ---[ 531]---> BDD-cost:    0
c ---[ 530]---> BDD-cost:    0
c ---[ 529]---> BDD-cost:    0
c ---[ 527]---> BDD-cost:    1
c ---[ 526]---> BDD-cost:    0
c ---[ 525]---> BDD-cost:    0
c ---[ 524]---> BDD-cost:    0
c ---[ 523]---> BDD-cost:    0
c ---[ 522]---> BDD-cost:    0
c ---[ 521]---> BDD-cost:    0
c ---[ 520]---> BDD-cost:    3
c ---[ 518]---> BDD-cost:    4
c ---[ 516]---> BDD-cost:    1
c ---[ 514]---> BDD-cost:    6
c ---[ 512]---> BDD-cost:    0
c ---[ 510]---> BDD-cost:    0
c ---[ 508]---> BDD-cost:    0
c ---[ 506]---> BDD-cost:    0
c ---[ 505]---> BDD-cost:    0
c ---[ 504]---> BDD-cost:    0
c ---[ 503]---> BDD-cost:    0
c ---[ 502]---> BDD-cost:    0
c ---[ 501]---> BDD-cost:    0
c ---[ 500]---> BDD-cost:    1
c ---[ 499]---> BDD-cost:    0
c ---[ 498]---> BDD-cost:    0
c ---[ 497]---> BDD-cost:    0
c ---[ 496]---> BDD-cost:    4
c ---[ 494]---> BDD-cost:    4
c ---[ 491]---> BDD-cost:    6
c ---[ 489]---> BDD-cost:    1
c ---[ 488]---> BDD-cost:    1
c ---[ 485]---> BDD-cost:    9
c ---[ 484]---> BDD-cost:    1
c ---[ 481]---> BDD-cost:    9
c ---[ 479]---> BDD-cost:   37
c ---[ 477]---> BDD-cost:    1
c ---[ 476]---> BDD-cost:    1
c ---[ 475]---> BDD-cost:    1
c ---[ 474]---> BDD-cost:    1
c ---[ 472]---> BDD-cost:    0
c ---[ 470]---> BDD-cost:    0
c ---[ 468]---> BDD-cost:    0
c ---[ 466]---> BDD-cost:    0
c ---[ 465]---> BDD-cost:    0
c ---[ 464]---> BDD-cost:    0
c ---[ 463]---> BDD-cost:    0
c ---[ 462]---> BDD-cost:    0
c ---[ 461]---> BDD-cost:    0
c ---[ 460]---> BDD-cost:    0
c ---[ 459]---> BDD-cost:    1
c ---[ 458]---> BDD-cost:    0
c ---[ 457]---> BDD-cost:    0
c ---[ 456]---> BDD-cost:    3
c ---[ 454]---> BDD-cost:    4
c ---[ 451]---> BDD-cost:    6
c ---[ 449]---> BDD-cost:    0
c ---[ 447]---> BDD-cost:    0
c ---[ 445]---> BDD-cost:    0
c ---[ 443]---> BDD-cost:    1
c ---[ 441]---> BDD-cost:    0
c ---[ 440]---> BDD-cost:    0
c ---[ 439]---> BDD-cost:    0
c ---[ 438]---> BDD-cost:    0
c ---[ 437]---> BDD-cost:    0
c ---[ 436]---> BDD-cost:    0
c ---[ 435]---> BDD-cost:    0
c ---[ 434]---> BDD-cost:    0
c ---[ 433]---> BDD-cost:    0
c ---[ 432]---> BDD-cost:    3
c ---[ 431]---> BDD-cost:    1
c ---[ 430]---> BDD-cost:    1
c ---[ 428]---> BDD-cost:    1
c ---[ 427]---> BDD-cost:   26
c ---[ 426]---> BDD-cost:    1
c ---[ 424]---> BDD-cost:    1
c ---[ 423]---> BDD-cost:   26
c ---[ 422]---> BDD-cost:    1
c ---[ 420]---> BDD-cost:    1
c ---[ 419]---> BDD-cost:   26
c ---[ 418]---> BDD-cost:    1
c ---[ 416]---> BDD-cost:    1
c ---[ 415]---> BDD-cost:   26
c ---[ 414]---> BDD-cost:    1
c ---[ 412]---> BDD-cost:    1
c ---[ 411]---> BDD-cost:   26
c ---[ 410]---> BDD-cost:    1
c ---[ 408]---> BDD-cost:    1
c ---[ 407]---> BDD-cost:   26
c ---[ 406]---> BDD-cost:    1
c ---[ 404]---> BDD-cost:    1
c ---[ 403]---> BDD-cost:   26
c ---[ 402]---> BDD-cost:    1
c ---[ 400]---> BDD-cost:    1
c ---[ 395]---> BDD-cost:    1
c ---[ 394]---> BDD-cost:    1
c ---[ 392]---> BDD-cost:    1
c ---[ 391]---> BDD-cost:   26
c ---[ 390]---> BDD-cost:    1
c ---[ 388]---> BDD-cost:    1
c ---[ 387]---> BDD-cost:   26
c ---[ 386]---> BDD-cost:    1
c ---[ 384]---> BDD-cost:    1
c ---[ 383]---> BDD-cost:   26
c ---[ 382]---> BDD-cost:    1
c ---[ 380]---> BDD-cost:    1
c ---[ 379]---> BDD-cost:   26
c ---[ 378]---> BDD-cost:    1
c ---[ 376]---> BDD-cost:    1
c ---[ 375]---> BDD-cost:   26
c ---[ 374]---> BDD-cost:    1
c ---[ 372]---> BDD-cost:    1
c ---[ 371]---> BDD-cost:   26
c ---[ 370]---> BDD-cost:    1
c ---[ 368]---> BDD-cost:    1
c ---[ 367]---> BDD-cost:   26
c ---[ 366]---> BDD-cost:    1
c ---[ 364]---> BDD-cost:    1
c ---[ 359]---> BDD-cost:    1
c ---[ 358]---> BDD-cost:    1
c ---[ 356]---> BDD-cost:    1
c ---[ 355]---> BDD-cost:   26
c ---[ 354]---> BDD-cost:    1
c ---[ 352]---> BDD-cost:    1
c ---[ 351]---> BDD-cost:   26
c ---[ 350]---> BDD-cost:    1
c ---[ 348]---> BDD-cost:    1
c ---[ 347]---> BDD-cost:   26
c ---[ 346]---> BDD-cost:    1
c ---[ 344]---> BDD-cost:    1
c ---[ 343]---> BDD-cost:   26
c ---[ 342]---> BDD-cost:    1
c ---[ 340]---> BDD-cost:    1
c ---[ 339]---> BDD-cost:   26
c ---[ 338]---> BDD-cost:    1
c ---[ 336]---> BDD-cost:    1
c ---[ 335]---> BDD-cost:   26
c ---[ 334]---> BDD-cost:    1
c ---[ 332]---> BDD-cost:    1
c ---[ 331]---> BDD-cost:   26
c ---[ 330]---> BDD-cost:    1
c ---[ 328]---> BDD-cost:    1
c ---[ 323]---> BDD-cost:    1
c ---[ 322]---> BDD-cost:    1
c ---[ 320]---> BDD-cost:    1
c ---[ 319]---> BDD-cost:   26
c ---[ 318]---> BDD-cost:    1
c ---[ 316]---> BDD-cost:    1
c ---[ 315]---> BDD-cost:   26
c ---[ 314]---> BDD-cost:    1
c ---[ 312]---> BDD-cost:    1
c ---[ 311]---> BDD-cost:   26
c ---[ 310]---> BDD-cost:    1
c ---[ 308]---> BDD-cost:    1
c ---[ 307]---> BDD-cost:   26
c ---[ 306]---> BDD-cost:    1
c ---[ 304]---> BDD-cost:    1
c ---[ 303]---> BDD-cost:   26
c ---[ 302]---> BDD-cost:    1
c ---[ 300]---> BDD-cost:    1
c ---[ 299]---> BDD-cost:   26
c ---[ 298]---> BDD-cost:    1
c ---[ 296]---> BDD-cost:    1
c ---[ 295]---> BDD-cost:   26
c ---[ 294]---> BDD-cost:    1
c ---[ 292]---> BDD-cost:    1
c ---[ 287]---> BDD-cost:    1
c ---[ 286]---> BDD-cost:    1
c ---[ 284]---> BDD-cost:    1
c ---[ 283]---> BDD-cost:   26
c ---[ 282]---> BDD-cost:    1
c ---[ 280]---> BDD-cost:    1
c ---[ 279]---> BDD-cost:   26
c ---[ 278]---> BDD-cost:    1
c ---[ 276]---> BDD-cost:    1
c ---[ 275]---> BDD-cost:   26
c ---[ 274]---> BDD-cost:    1
c ---[ 272]---> BDD-cost:    1
c ---[ 271]---> BDD-cost:   26
c ---[ 270]---> BDD-cost:    1
c ---[ 268]---> BDD-cost:    1
c ---[ 267]---> BDD-cost:   26
c ---[ 266]---> BDD-cost:    1
c ---[ 264]---> BDD-cost:    1
c ---[ 263]---> BDD-cost:   26
c ---[ 262]---> BDD-cost:    1
c ---[ 260]---> BDD-cost:    1
c ---[ 259]---> BDD-cost:   26
c ---[ 258]---> BDD-cost:    1
c ---[ 256]---> BDD-cost:    1
c ---[ 251]---> BDD-cost:    1
c ---[ 250]---> BDD-cost:    1
c ---[ 248]---> BDD-cost:    1
c ---[ 247]---> BDD-cost:   26
c ---[ 246]---> BDD-cost:    1
c ---[ 244]---> BDD-cost:    1
c ---[ 243]---> BDD-cost:   26
c ---[ 242]---> BDD-cost:    1
c ---[ 240]---> BDD-cost:    1
c ---[ 239]---> BDD-cost:   26
c ---[ 238]---> BDD-cost:    1
c ---[ 236]---> BDD-cost:    1
c ---[ 235]---> BDD-cost:   26
c ---[ 234]---> BDD-cost:    1
c ---[ 232]---> BDD-cost:    1
c ---[ 231]---> BDD-cost:   26
c ---[ 230]---> BDD-cost:    1
c ---[ 228]---> BDD-cost:    1
c ---[ 227]---> BDD-cost:   26
c ---[ 226]---> BDD-cost:    1
c ---[ 224]---> BDD-cost:    1
c ---[ 223]---> BDD-cost:   26
c ---[ 222]---> BDD-cost:    1
c ---[ 220]---> BDD-cost:    1
c ---[ 215]---> BDD-cost:    1
c ---[ 214]---> BDD-cost:    1
c ---[ 212]---> BDD-cost:    1
c ---[ 211]---> BDD-cost:   26
c ---[ 210]---> BDD-cost:    1
c ---[ 208]---> BDD-cost:    1
c ---[ 207]---> BDD-cost:   26
c ---[ 206]---> BDD-cost:    1
c ---[ 204]---> BDD-cost:    1
c ---[ 203]---> BDD-cost:   26
c ---[ 202]---> BDD-cost:    1
c ---[ 200]---> BDD-cost:    1
c ---[ 199]---> BDD-cost:   26
c ---[ 198]---> BDD-cost:    1
c ---[ 196]---> BDD-cost:    1
c ---[ 195]---> BDD-cost:   26
c ---[ 194]---> BDD-cost:    1
c ---[ 192]---> BDD-cost:    1
c ---[ 191]---> BDD-cost:   26
c ---[ 190]---> BDD-cost:    1
c ---[ 188]---> BDD-cost:    1
c ---[ 187]---> BDD-cost:   26
c ---[ 186]---> BDD-cost:    1
c ---[ 184]---> BDD-cost:    1
c ---[ 179]---> BDD-cost:    1
c ---[ 178]---> BDD-cost:    1
c ---[ 176]---> BDD-cost:    1
c ---[ 175]---> BDD-cost:   26
c ---[ 174]---> BDD-cost:    1
c ---[ 172]---> BDD-cost:    1
c ---[ 171]---> BDD-cost:   26
c ---[ 170]---> BDD-cost:    1
c ---[ 168]---> BDD-cost:    1
c ---[ 167]---> BDD-cost:   26
c ---[ 166]---> BDD-cost:    1
c ---[ 164]---> BDD-cost:    1
c ---[ 163]---> BDD-cost:   26
c ---[ 162]---> BDD-cost:    1
c ---[ 160]---> BDD-cost:    1
c ---[ 159]---> BDD-cost:   26
c ---[ 158]---> BDD-cost:    1
c ---[ 156]---> BDD-cost:    1
c ---[ 155]---> BDD-cost:   26
c ---[ 154]---> BDD-cost:    1
c ---[ 152]---> BDD-cost:    1
c ---[ 151]---> BDD-cost:   26
c ---[ 150]---> BDD-cost:    1
c ---[ 148]---> BDD-cost:    1
c ---[ 143]---> BDD-cost:    1
c ---[ 142]---> BDD-cost:    1
c ---[ 140]---> BDD-cost:    1
c ---[ 139]---> BDD-cost:   26
c ---[ 138]---> BDD-cost:    1
c ---[ 136]---> BDD-cost:    1
c ---[ 135]---> BDD-cost:   26
c ---[ 134]---> BDD-cost:    1
c ---[ 132]---> BDD-cost:    1
c ---[ 131]---> BDD-cost:   26
c ---[ 130]---> BDD-cost:    1
c ---[ 128]---> BDD-cost:    1
c ---[ 127]---> BDD-cost:   26
c ---[ 126]---> BDD-cost:    1
c ---[ 124]---> BDD-cost:    1
c ---[ 123]---> BDD-cost:   26
c ---[ 122]---> BDD-cost:    1
c ---[ 120]---> BDD-cost:    1
c ---[ 119]---> BDD-cost:   26
c ---[ 118]---> BDD-cost:    1
c ---[ 116]---> BDD-cost:    1
c ---[ 115]---> BDD-cost:   26
c ---[ 114]---> BDD-cost:    1
c ---[ 112]---> BDD-cost:    1
c ---[ 107]---> BDD-cost:    1
c ---[ 106]---> BDD-cost:    1
c ---[ 104]---> BDD-cost:    1
c ---[ 103]---> BDD-cost:   26
c ---[ 102]---> BDD-cost:    1
c ---[ 100]---> BDD-cost:    1
c ---[  99]---> BDD-cost:   26
c ---[  98]---> BDD-cost:    1
c ---[  96]---> BDD-cost:    1
c ---[  95]---> BDD-cost:   26
c ---[  94]---> BDD-cost:    1
c ---[  92]---> BDD-cost:    1
c ---[  91]---> BDD-cost:   26
c ---[  90]---> BDD-cost:    1
c ---[  88]---> BDD-cost:    1
c ---[  87]---> BDD-cost:   26
c ---[  86]---> BDD-cost:    1
c ---[  84]---> BDD-cost:    1
c ---[  83]---> BDD-cost:   26
c ---[  82]---> BDD-cost:    1
c ---[  80]---> BDD-cost:    1
c ---[  79]---> BDD-cost:   26
c ---[  78]---> BDD-cost:    1
c ---[  76]---> BDD-cost:    1
c ---[  71]---> BDD-cost:    1
c ---[  70]---> BDD-cost:    1
c ---[  68]---> BDD-cost:    1
c ---[  67]---> BDD-cost:   26
c ---[  66]---> BDD-cost:    1
c ---[  64]---> BDD-cost:    1
c ---[  63]---> BDD-cost:   26
c ---[  62]---> BDD-cost:    1
c ---[  60]---> BDD-cost:    1
c ---[  59]---> BDD-cost:   26
c ---[  58]---> BDD-cost:    1
c ---[  56]---> BDD-cost:    1
c ---[  55]---> BDD-cost:   26
c ---[  54]---> BDD-cost:    1
c ---[  52]---> BDD-cost:    1
c ---[  51]---> BDD-cost:   26
c ---[  50]---> BDD-cost:    1
c ---[  48]---> BDD-cost:    1
c ---[  47]---> BDD-cost:   26
c ---[  46]---> BDD-cost:    1
c ---[  44]---> BDD-cost:    1
c ---[  43]---> BDD-cost:   26
c ---[  42]---> BDD-cost:    1
c ---[  40]---> BDD-cost:    1
c ---[  35]---> BDD-cost:    1
c ---[  34]---> BDD-cost:    1
c ---[  32]---> BDD-cost:    1
c ---[  31]---> BDD-cost:   26
c ---[  30]---> BDD-cost:    1
c ---[  28]---> BDD-cost:    1
c ---[  27]---> BDD-cost:   26
c ---[  26]---> BDD-cost:    1
c ---[  24]---> BDD-cost:    1
c ---[  23]---> BDD-cost:   26
c ---[  22]---> BDD-cost:    1
c ---[  20]---> BDD-cost:    1
c ---[  19]---> BDD-cost:   26
c ---[  18]---> BDD-cost:    1
c ---[  16]---> BDD-cost:    1
c ---[  15]---> BDD-cost:   26
c ---[  14]---> BDD-cost:    1
c ---[  12]---> BDD-cost:    1
c ---[  11]---> BDD-cost:   26
c ---[  10]---> BDD-cost:    1
c ---[   8]---> BDD-cost:    1
c ---[   7]---> BDD-cost:   26
c ---[   6]---> BDD-cost:    1
c ---[   4]---> BDD-cost:    1
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |         0 |   80286   196112 |   24085       0        0     nan |  0.000 % |
c   -- subsuming                       
c   -- var.elim.:  1000/26258          
c   -- var.elim.:  2000/26258          
c   -- var.elim.:  3000/26258          
c   -- var.elim.:  4000/26258          
c   -- var.elim.:  5000/26258          
c   -- var.elim.:  6000/26258          
c   -- var.elim.:  7000/26258          
c   -- var.elim.:  8000/26258          
c   -- var.elim.:  9000/26258          
c   -- var.elim.:  10000/26258          
c   -- var.elim.:  11000/26258          
c   -- var.elim.:  12000/26258          
c   -- var.elim.:  13000/26258          
c   -- var.elim.:  14000/26258          
c   -- var.elim.:  15000/26258          
c   -- var.elim.:  16000/26258          
c   -- var.elim.:  17000/26258          
c   -- var.elim.:  18000/26258          
c   -- var.elim.:  19000/26258          
c   -- var.elim.:  20000/26258          
c   -- var.elim.:  21000/26258          
c   -- var.elim.:  22000/26258          
c   -- var.elim.:  23000/26258          
c   -- var.elim.:  24000/26258          
c   -- var.elim.:  25000/26258          
c   -- var.elim.:  26000/26258          
c   -- var.elim.:  26258/26258          
c   -- var.elim.:  1000/12424          
c   -- var.elim.:  2000/12424          
c   -- var.elim.:  3000/12424          
c   -- var.elim.:  4000/12424          
c   -- var.elim.:  5000/12424          
c   -- var.elim.:  6000/12424          
c   -- var.elim.:  7000/12424          
c   -- var.elim.:  8000/12424          
c   -- var.elim.:  9000/12424          
c   -- var.elim.:  10000/12424          
c   -- var.elim.:  11000/12424          
c   -- var.elim.:  12000/12424          
c   -- var.elim.:  12424/12424          
c   -- var.elim.:  1000/1894          
c   -- var.elim.:  1894/1894          
c   -- var.elim.:  319/319          
c   -- subsuming                       
c   -- var.elim.:  1000/2709          
c   -- var.elim.:  2000/2709          
c   -- var.elim.:  2709/2709          
c   -- var.elim.:  1000/1485          
c   -- var.elim.:  1485/1485          
c   -- var.elim.:  118/118          
c   -- var.elim.:  31/31          
c   -- subsuming                       
c   -- var.elim.:  520/520          
c   -- var.elim.:  228/228          
c   -- subsuming                       
c   -- var.elim.:  92/92          
c   -- var.elim.:  36/36          
c |         0 |   18273    54913 |      --       0       --      -- |     --   | -58883/-130791
c |         0 |   18273    54913 |    7309       0        0     nan |  0.000 % |
c |       100 |   18273    54913 |    8040     100     1277    12.8 | 78.561 % |
c ==============================================================================
c (current CPU-time: 4.35234 s)
c ==============================================================================
c [1mFound solution: -13312[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): s
c ---[   0]---> BDD-cost:  107
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |       170 |   18523    55643 |    5556     170     2126    12.5 | 78.561 % |
c   -- subsuming                       
c   -- var.elim.:  168/168          
c   -- var.elim.:  95/95          
c |       170 |   18483    55812 |      --     170       --      -- |     --   | -40/170
c |       170 |   18483    55812 |    7393     170     2126    12.5 | 78.561 % |
c ==============================================================================
c (current CPU-time: 4.79427 s)
c ==============================================================================
c [1mFound solution: -23040[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): s
c ---[   0]---> BDD-cost:   83
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |       225 |   18547    55941 |    5564     223     2449    11.0 | 78.561 % |
c   -- subsuming                       
c   -- var.elim.:  262/262          
c   -- var.elim.:  161/161          
c   -- subsuming                       
c   -- var.elim.:  53/53          
c   -- var.elim.:  6/6          
c |       225 |   18468    55814 |      --     223       --      -- |     --   | -79/-126
c |       225 |   18468    55814 |    7387     215     2340    10.9 | 78.561 % |
c ==============================================================================
c (current CPU-time: 5.2752 s)
c ==============================================================================
c [1mFound solution: -37888[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> BDD-cost:   38
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |       296 |   18516    55932 |    5554     285     3194    11.2 | 78.561 % |
c   -- subsuming                       
c   -- var.elim.:  109/109          
c   -- var.elim.:  47/47          
c |       296 |   18497    55983 |      --     285       --      -- |     --   | -19/54
c |       296 |   18497    55983 |    7398     284     3168    11.2 | 78.561 % |
c ==============================================================================
c (current CPU-time: 5.71813 s)
c ==============================================================================
c [1mFound solution: -48256[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:  308     Base: 2 2 2 2 2 2 2 2
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |       323 |   19196    57621 |    5758     311     3337    10.7 | 78.561 % |
c   -- subsuming                       
c   -- var.elim.:  303/303          
c   -- var.elim.:  159/159          
c   -- var.elim.:  3/3          
c   -- subsuming                       
c   -- var.elim.:  72/72          
c   -- var.elim.:  53/53          
c   -- var.elim.:  8/8          
c |       323 |   19049    57838 |      --     311       --      -- |     --   | -147/218
c |       323 |   19049    57838 |    7619     311     3337    10.7 | 78.561 % |
c ==============================================================================
c (current CPU-time: 6.28504 s)
c ==============================================================================
c [1mFound solution: -50048[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    6     Base: 2 2 2 2 2 2 2 2
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |       419 |   19151    58097 |    5745     407     5329    13.1 | 78.561 % |
c   -- subsuming                       
c   -- var.elim.:  128/128          
c   -- var.elim.:  75/75          
c   -- var.elim.:  3/3          
c   -- var.elim.:  18/18          
c |       419 |   19091    57968 |      --     407       --      -- |     --   | -60/-128
c |       419 |   19091    57968 |    7636     407     5329    13.1 | 78.561 % |
c ==============================================================================
c (current CPU-time: 6.77297 s)
c ==============================================================================
c [1mFound solution: -51712[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> BDD-cost:   44
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |       489 |   18976    57435 |    5692     473     6380    13.5 | 78.561 % |
c   -- subsuming                       
c   -- var.elim.:  228/228          
c   -- var.elim.:  323/323          
c   -- var.elim.:  132/132          
c   -- subsuming                       
c   -- var.elim.:  63/63          
c   -- var.elim.:  41/41          
c |       489 |   18856    57348 |      --     473       --      -- |     --   | -120/-84
c |       489 |   18856    57348 |    7542     351     4059    11.6 | 78.561 % |
c ==============================================================================
c (current CPU-time: 7.2539 s)
c ==============================================================================
c [1mFound solution: -54528[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   60     Base: 2 2 2 2 2 2 2
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |       510 |   18952    57592 |    5685     372     4254    11.4 | 78.561 % |
c   -- subsuming                       
c   -- var.elim.:  136/136          
c   -- var.elim.:  82/82          
c |       510 |   18900    57581 |      --     372       --      -- |     --   | -52/-10
c |       510 |   18900    57581 |    7560     370     4201    11.4 | 78.561 % |
c ==============================================================================
c (current CPU-time: 7.69583 s)
c ==============================================================================
c [1mFound solution: -55552[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    6     Base: 2 2 2 2 2 2 2
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |       528 |   18936    57678 |    5680     387     4407    11.4 | 78.561 % |
c   -- subsuming                       
c   -- var.elim.:  106/106          
c   -- var.elim.:  101/101          
c   -- var.elim.:  23/23          
c |       528 |   18866    57568 |      --     387       --      -- |     --   | -70/-109
c |       528 |   18866    57568 |    7546     366     3962    10.8 | 78.561 % |
c |       630 |   18866    57568 |    8301     468     6355    13.6 | 77.766 % |
c |       780 |   18866    57568 |    9131     618    10957    17.7 | 77.766 % |
c |      1005 |   18696    56897 |    9953     813    17738    21.8 | 77.891 % |
c ==============================================================================
c (current CPU-time: 8.63069 s)
c ==============================================================================
c [1mFound solution: -56576[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   47     Base: 2 2 2 2 2 2 2
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |      1026 |   18761    57062 |    5628     834    18491    22.2 | 77.891 % |
c   -- subsuming                       
c   -- var.elim.:  205/205          
c   -- var.elim.:  244/244          
c   -- var.elim.:  130/130          
c   -- subsuming                       
c   -- var.elim.:  47/47          
c   -- var.elim.:  20/20          
c |      1026 |   18659    56945 |      --     834       --      -- |     --   | -102/-116
c |      1026 |   18659    56945 |    7463     601     9184    15.3 | 77.891 % |
c |      1128 |   18659    56945 |    8209     703    11678    16.6 | 77.990 % |
c ==============================================================================
c (current CPU-time: 9.26759 s)
c ==============================================================================
c [1mFound solution: -57600[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    5     Base: 2 2 2 2 2 2 2
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |      1200 |   18702    57065 |    5610     775    13854    17.9 | 77.990 % |
c   -- subsuming                       
c   -- var.elim.:  80/80          
c   -- var.elim.:  41/41          
c |      1200 |   18669    57049 |      --     775       --      -- |     --   | -33/-15
c |      1200 |   18669    57049 |    7467     775    13854    17.9 | 77.990 % |
c ==============================================================================
c (current CPU-time: 9.74552 s)
c ==============================================================================
c [1mFound solution: -57856[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> BDD-cost:   63
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |      1231 |   18838    57543 |    5651     806    15222    18.9 | 77.990 % |
c   -- subsuming                       
c   -- var.elim.:  109/109          
c   -- var.elim.:  47/47          
c |      1231 |   18818    57670 |      --     806       --      -- |     --   | -20/130
c |      1231 |   18818    57670 |    7527     806    15222    18.9 | 77.990 % |
c ==============================================================================
c (current CPU-time: 10.2324 s)
c ==============================================================================
c [1mFound solution: -58624[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    4     Base: 2 2 2 2 2 2 2
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |      1268 |   18865    57797 |    5659     843    16439    19.5 | 77.990 % |
c   -- subsuming                       
c   -- var.elim.:  71/71          
c   -- var.elim.:  41/41          
c |      1268 |   18836    57807 |      --     843       --      -- |     --   | -29/11
c |      1268 |   18836    57807 |    7534     843    16439    19.5 | 77.990 % |
c |      1368 |   18683    57121 |    8220     812    14588    18.0 | 77.839 % |
c ==============================================================================
c [1mOptimal solution: -58624[0m
s OPTIMUM FOUND
v -r0_bit_7 -r0_bit_6 -r0_bit_5 -r0_bit_4 -r0_bit_3 -r0_bit_2 -r0_bit_1 -r0_bit0 r0_bit1 r0_bit2 -r0_bit3 r0_bit4 -r0_bit5 -r0_bit6 r0_bit7 -r0_bit8 -r0_bit9 -r0_bit10 -r0_bit11 -r0_bit12 -r1_bit_7 -r1_bit_6 -r1_bit_5 -r1_bit_4 -r1_bit_3 -r1_bit_2 -r1_bit_1 -r1_bit0 -r1_bit1 -r1_bit2 r1_bit3 -r1_bit4 r1_bit5 -r1_bit6 r1_bit7 -r1_bit8 -r1_bit9 -r1_bit10 -r1_bit11 -r1_bit12 -r2_bit_7 -r2_bit_6 -r2_bit_5 -r2_bit_4 -r2_bit_3 -r2_bit_2 -r2_bit_1 -r2_bit0 -r2_bit1 r2_bit2 r2_bit3 -r2_bit4 -r2_bit5 -r2_bit6 r2_bit7 -r2_bit8 -r2_bit9 -r2_bit10 -r2_bit11 -r2_bit12 -r3_bit_7 -r3_bit_6 -r3_bit_5 -r3_bit_4 -r3_bit_3 -r3_bit_2 -r3_bit_1 -r3_bit0 -r3_bit1 -r3_bit2 -r3_bit3 -r3_bit4 -r3_bit5 -r3_bit6 -r3_bit7 -r3_bit8 -r3_bit9 -r3_bit10 -r3_bit11 -r3_bit12 -r4_bit_7 -r4_bit_6 -r4_bit_5 -r4_bit_4 -r4_bit_3 -r4_bit_2 -r4_bit_1 -r4_bit0 -r4_bit1 -r4_bit2 -r4_bit3 -r4_bit4 -r4_bit5 -r4_bit6 -r4_bit7 -r4_bit8 -r4_bit9 -r4_bit10 -r4_bit11 -r4_bit12 -o2b32_bit0 -f2a1a0f1_bit0 -f1a2a0f2_bit0 -p03p00_bit0 -s33p03_bit0 -p03p01_bit0 -p03p02_bit0 -p03p04_bit0 -s33p13_bit0 sp01_bit0 -sp02_bit0 -sp03_bit0 sp04_bit0 sp10_bit0 sp12_bit0 sp13_bit0 sp14_bit0 -o2c02_bit0 -sp20_bit0 sp21_bit0 sp23_bit0 -sp24_bit0 -o2c12_bit0 -sp30_bit0 sp31_bit0 sp32_bit0 -sp34_bit0 -s00_bit0 -s01_bit0 s02_bit0 o2c20_bit0 -s03_bit0 o2c21_bit0 -s04_bit0 o2c23_bit0 sp40_bit0 sp41_bit0 -sp42_bit0 -sp43_bit0 -s10_bit0 -s11_bit0 -s12_bit0 -s13_bit0 -s14_bit0 -o2c32_bit0 -f3a0a1f0_bit0 -s20_bit0 s21_bit0 s22_bit0 -s23_bit0 s24_bit0 s30_bit0 -s31_bit0 -s32_bit0 -s33_bit0 -s34_bit0 f0a3a1f3_bit0 -f4a2a3f2_bit0 -s02s00_bit0 -s02s01_bit0 -s02s03_bit0 -s02s04_bit0 f2a4a3f4_bit0 f4f1a0a1_bit0 -f3f2a0a2_bit0 f2f3a0a3_bit0 -f1f4a0a4_bit0 -o2d02_bit0 -o2d12_bit0 o2d20_bit0 o2d21_bit0 o2d23_bit0 -o2d32_bit0 -s22p02_bit0 -nta0f1_bit0 -nta0f2_bit0 -nta0f3_bit0 -nta0f4_bit0 s22p12_bit0 -f3f2a1a2_bit0 -f2f3a1a3_bit0 -a0a3f0f3_bit0 o2e02_bit0 -o2e12_bit0 -nt01_bit0 -nt02_bit0 -nt03_bit0 -nt04_bit0 -o2e20_bit0 o2e21_bit0 -nt10_bit0 o2e23_bit0 -nt12_bit0 -nt13_bit0 -nt14_bit0 -o2e32_bit0 -nt20_bit0 -nt21_bit0 -nt23_bit0 -nt24_bit0 nta1f0_bit0 -nt30_bit0 -nt31_bit0 nta1f2_bit0 -nt32_bit0 nta1f3_bit0 nta1f4_bit0 -nt34_bit0 -nt40_bit0 -nt41_bit0 -nt42_bit0 -nt43_bit0 a0a1_bit0 -ntf0a1_bit0 ntf0a2_bit0 a0a2_bit0 ntf0a3_bit0 a0a3_bit0 ntf0a4_bit0 a0a4_bit0 -s33s30_bit0 -s33s31_bit0 -s33s32_bit0 -s33s34_bit0 -s11p01_bit0 -ss01_bit0 -ss02_bit0 -ss03_bit0 -ss04_bit0 -s11p11_bit0 a1a2f1f2_bit0 -ss10_bit0 ss12_bit0 -ss13_bit0 ss14_bit0 o2f02_bit0 -f4a1a0f1_bit0 -ss20_bit0 ss21_bit0 -ss23_bit0 ss24_bit0 -f3a2a0f2_bit0 -o2f12_bit0 a0f1_bit0 -ss30_bit0 a0f2_bit0 -ss31_bit0 a0f3_bit0 -ss32_bit0 a0f4_bit0 -ss34_bit0 -f2a3a0f3_bit0 -o2f20_bit0 o2f21_bit0 o2f23_bit0 -f1a4a0f4_bit0 -ss40_bit0 ss41_bit0 ss42_bit0 -ss43_bit0 -o2f32_bit0 -nta2f0_bit0 -nta2f1_bit0 -nta2f3_bit0 -nta2f4_bit0 -a1a0_bit0 ntf1a0_bit0 ntf1a2_bit0 -a1a2_bit0 ntf1a3_bit0 -a1a3_bit0 ntf1a4_bit0 -a1a4_bit0 -o2g02_bit0 f3a2a1f2_bit0 -o2g12_bit0 -a1f0_bit0 -a1f2_bit0 -a1f3_bit0 -a1f4_bit0 -f2a3a1f3_bit0 o2g20_bit0 o2g21_bit0 o2g23_bit0 -lo01_bit0 -lo02_bit0 -lo03_bit0 -lo04_bit0 -o2g32_bit0 -lo10_bit0 -lo12_bit0 -lo13_bit0 -lo14_bit0 -nta3f0_bit0 -nta3f1_bit0 nta3f2_bit0 nta3f4_bit0 -lo20_bit0 -lo21_bit0 -lo23_bit0 -lo24_bit0 -lo30_bit0 -lo31_bit0 -s22s20_bit0 -lo32_bit0 s22s21_bit0 -lo34_bit0 -s22s23_bit0 s22s24_bit0 -lo40_bit0 -lo41_bit0 -lo42_bit0 -lo43_bit0 -s00p00_bit0 -s00p10_bit0 f4f3a0a3_bit0 f0a1_bit0 -f0a2_bit0 -f0a3_bit0 -f0a4_bit0 -f3f4a0a4_bit0 ntf2a0_bit0 -a2a0_bit0 -ntf2a1_bit0 a2a1_bit0 -ntf2a3_bit0 a2a3_bit0 ntf2a4_bit0 a2a4_bit0 f0f1_bit0 -f0f2_bit0 -f0f3_bit0 -f0f4_bit0 -o2h02_bit0 -o2h12_bit0 a2f0_bit0 a2f1_bit0 a2f3_bit0 a2f4_bit0 o0a01_bit0 o0a02_bit0 o0a03_bit0 o2h20_bit0 o2h21_bit0 -p12p10_bit0 o2h23_bit0 p12p11_bit0 p12p13_bit0 -p12p14_bit0 -o0a10_bit0 -o2h32_bit0 -f1f0a4a0_bit0 -o0a20_bit0 f0f1a4a1_bit0 -nta4f0_bit0 -nta4f1_bit0 -nta4f2_bit0 -nta4f3_bit0 -o0a30_bit0 dlt01_bit0 -dlt02_bit0 -dlt03_bit0 -dlt04_bit0 -dlt10_bit0 -dlt12_bit0 -dlt13_bit0 -dlt14_bit0 dlt20_bit0 dlt21_bit0 -a0_bit0 -a0_bit1 -a0_bit2 -a0_bit3 -a0_bit4 -a0_bit5 -a0_bit6 -a0_bit7 -a0_bit8 a1_bit0 a1_bit1 a1_bit2 -a1_bit3 a1_bit4 -a1_bit5 -a1_bit6 a1_bit7 -a1_bit8 dlt23_bit0 -a2_bit0 a2_bit1 -a2_bit2 -a2_bit3 -a2_bit4 -a2_bit5 -a2_bit6 -a2_bit7 -a2_bit8 -dlt24_bit0 a3_bit0 a3_bit1 a3_bit2 a3_bit3 -a3_bit4 -a3_bit5 -a3_bit6 a3_bit7 -a3_bit8 -a4_bit0 -a4_bit1 -a4_bit2 a4_bit3 a4_bit4 a4_bit5 a4_bit6 -a4_bit7 -a4_bit8 dlt30_bit0 dlt31_bit0 -dlt32_bit0 -dlt34_bit0 dlt40_bit0 dlt41_bit0 dlt42_bit0 dlt43_bit0 -c3_bit_7 -c3_bit_6 -c3_bit_5 -c3_bit_4 -c3_bit_3 -c3_bit_2 -c3_bit_1 -f1a0_bit0 -c4_bit_7 -c4_bit_6 -c4_bit_5 -c4_bit_4 -c4_bit_3 -c4_bit_2 -c4_bit_1 -f4f3a1a3_bit0 -f1a2_bit0 -f1a3_bit0 -f1a4_bit0 -f3f4a1a4_bit0 -d0_bit_7 -d0_bit_6 -d0_bit_5 -d0_bit_4 -d0_bit_3 -d0_bit_2 -d0_bit_1 -d4_bit_7 -d4_bit_6 -d4_bit_5 -d4_bit_4 -d4_bit_3 -d4_bit_2 -d4_bit_1 -f0_bit0 f0_bit1 f0_bit2 -f0_bit3 f0_bit4 -f0_bit5 -f0_bit6 f0_bit7 -f0_bit8 ntf3a0_bit0 -a3a0_bit0 f1_bit0 f1_bit1 f1_bit2 f1_bit3 f1_bit4 f1_bit5 -f1_bit6 -f1_bit7 f1_bit8 -ntf3a1_bit0 a3a1_bit0 -f2_bit0 f2_bit1 f2_bit2 f2_bit3 -f2_bit4 -f2_bit5 -f2_bit6 f2_bit7 -f2_bit8 ntf3a2_bit0 -a3a2_bit0 f3_bit0 f3_bit1 f3_bit2 f3_bit3 -f3_bit4 -f3_bit5 -f3_bit6 f3_bit7 -f3_bit8 -f4_bit0 f4_bit1 -f4_bit2 -f4_bit3 -f4_bit4 -f4_bit5 -f4_bit6 f4_bit7 -f4_bit8 ntf3a4_bit0 -a3a4_bit0 -f1f0_bit0 -f1f2_bit0 -f1f3_bit0 -f1f4_bit0 -s11s10_bit0 -s11s12_bit0 -s11s13_bit0 -s11s14_bit0 a3f0_bit0 a3f1_bit0 -a3f2_bit0 -a3f4_bit0 o0b01_bit0 o0b02_bit0 o0b03_bit0 -l0_bit0 l0_bit1 l0_bit2 -l0_bit3 l0_bit4 -l0_bit5 -l0_bit6 l0_bit7 -l0_bit8 l1_bit0 l1_bit1 l1_bit2 l1_bit3 l1_bit4 l1_bit5 -l1_bit6 -l1_bit7 l1_bit8 -l2_bit0 l2_bit1 l2_bit2 l2_bit3 -l2_bit4 -l2_bit5 -l2_bit6 l2_bit7 -l2_bit8 l3_bit0 l3_bit1 l3_bit2 l3_bit3 -l3_bit4 -l3_bit5 -l3_bit6 l3_bit7 -l3_bit8 -l4_bit0 -l4_bit1 -l4_bit2 l4_bit3 l4_bit4 l4_bit5 l4_bit6 -l4_bit7 -l4_bit8 -o0b10_bit0 -m0_bit0 -m0_bit1 -m0_bit2 -m0_bit3 -m0_bit4 -m0_bit5 -m0_bit6 -m0_bit7 -m0_bit8 m1_bit0 m1_bit1 m1_bit2 -m1_bit3 m1_bit4 -m1_bit5 -m1_bit6 m1_bit7 -m1_bit8 -m2_bit0 m2_bit1 -m2_bit2 -m2_bit3 -m2_bit4 -m2_bit5 -m2_bit6 -m2_bit7 -m2_bit8 m3_bit0 m3_bit1 m3_bit2 m3_bit3 -m3_bit4 -m3_bit5 -m3_bit6 m3_bit7 -m3_bit8 -m4_bit0 -m4_bit1 -m4_bit2 m4_bit3 m4_bit4 m4_bit5 m4_bit6 -m4_bit7 -m4_bit8 -o0b20_bit0 -n0_bit0 n0_bit1 n0_bit2 -n0_bit3 n0_bit4 -n0_bit5 -n0_bit6 n0_bit7 -n0_bit8 n1_bit0 n1_bit1 n1_bit2 n1_bit3 n1_bit4 n1_bit5 -n1_bit6 -n1_bit7 n1_bit8 -n2_bit0 n2_bit1 n2_bit2 n2_bit3 -n2_bit4 -n2_bit5 -n2_bit6 n2_bit7 -n2_bit8 n3_bit0 n3_bit1 n3_bit2 n3_bit3 -n3_bit4 -n3_bit5 -n3_bit6 n3_bit7 -n3_bit8 -n4_bit0 -n4_bit1 -n4_bit2 n4_bit3 n4_bit4 n4_bit5 n4_bit6 -n4_bit7 -n4_bit8 -o0b30_bit0 -f2a0_bit0 f2a1_bit0 f2a3_bit0 -f2a4_bit0 -s31p01_bit0 p01p00_bit0 -p01p02_bit0 -p01p03_bit0 p01p04_bit0 -s31p11_bit0 ntf4a0_bit0 -a4a0_bit0 -ntf4a1_bit0 a4a1_bit0 ntf4a2_bit0 -a4a2_bit0 -ntf4a3_bit0 a4a3_bit0 -f4a3a0f3_bit0 -f3a4a0f4_bit0 f2f0_bit0 f2f1_bit0 f2f3_bit0 -f2f4_bit0 a4f0_bit0 a4f1_bit0 a4f2_bit0 a4f3_bit0 o0c01_bit0 o0c02_bit0 o0c03_bit0 -o0c10_bit0 -f1f0a2a0_bit0 -o0c20_bit0 f0f1a2a1_bit0 -o0c30_bit0 -f1a0a4f0_bit0 -s00s01_bit0 -s00s02_bit0 -s00s03_bit0 -f0a1a4f1_bit0 -s00s04_bit0 -f3a0_bit0 f3a1_bit0 -f3a2_bit0 -f3a4_bit0 -f4a3a1f3_bit0 f3a4a1f4_bit0 f3f0_bit0 f3f1_bit0 -f3f2_bit0 -f3f4_bit0 o0d01_bit0 o0d02_bit0 o0d03_bit0 -o0d10_bit0 -spssnt01_bit0 -spssnt02_bit0 -spssnt03_bit0 -spssnt04_bit0 -f1f0a3a0_bit0 -o0d20_bit0 f0f1a3a1_bit0 -o0d30_bit0 -s20p00_bit0 -spssnt30_bit0 -spssnt31_bit0 -spssnt32_bit0 -spssnt34_bit0 -s20p10_bit0 spssnt40_bit0 -spssnt41_bit0 -spssnt42_bit0 spssnt43_bit0 -spssnt10_bit0 -spssnt12_bit0 -spssnt13_bit0 -spssnt14_bit0 -spssnt20_bit0 -spssnt21_bit0 -spssnt23_bit0 -spssnt24_bit0 -f4a0_bit0 f4a1_bit0 -f4a2_bit0 f4a3_bit0 f4f0_bit0 f4f1_bit0 f4f2_bit0 f4f3_bit0 -f3f0a4a0_bit0 f2f1a4a1_bit0 -f1f2a4a2_bit0 -f0f3a4a3_bit0 o0e01_bit0 -o0e02_bit0 -o0e03_bit0 flt01_bit0 -o0e10_bit0 -flt02_bit0 -flt03_bit0 -flt04_bit0 -flt10_bit0 o0e20_bit0 -flt12_bit0 -flt13_bit0 -flt14_bit0 flt20_bit0 flt21_bit0 o0e30_bit0 flt23_bit0 -flt24_bit0 flt30_bit0 flt31_bit0 -flt32_bit0 -flt34_bit0 flt40_bit0 flt41_bit0 flt42_bit0 flt43_bit0 -f1a0a2f0_bit0 -f0a1a2f1_bit0 -s31s30_bit0 -s31s32_bit0 -s31s33_bit0 -s31s34_bit0 o0f01_bit0 -o0f02_bit0 -o0f03_bit0 -o0f10_bit0 o0f20_bit0 o0f30_bit0 -f1a0a3f0_bit0 -f0a1a3f1_bit0 -f3f0a2a0_bit0 -f0f3a2a3_bit0 o0g01_bit0 -o0g02_bit0 -o0g03_bit0 -o0g10_bit0 o0g20_bit0 -f3a0a4f0_bit0 -f2a1a4f1_bit0 o0g30_bit0 -f1a2a4f2_bit0 -f0a3a4f3_bit0 -s20s21_bit0 -s20s22_bit0 -s20s23_bit0 -s20s24_bit0 -s14p04_bit0 -s14p14_bit0 f2f1a3a1_bit0 -f1f2a3a2_bit0 o0h01_bit0 -o0h02_bit0 -o0h03_bit0 -o0h10_bit0 o0h20_bit0 -p10p11_bit0 -p10p12_bit0 -p10p13_bit0 -p10p14_bit0 o0h30_bit0 -f3f2a4a2_bit0 f2f3a4a3_bit0 -f3a0a2f0_bit0 -f0a3a2f3_bit0 -s03p03_bit0 -s03p13_bit0 o3a03_bit0 -o3a13_bit0 o3a23_bit0 -o3a30_bit0 o3a31_bit0 -o3a32_bit0 -f2a1a3f1_bit0 f1a2a3f2_bit0 f4f1a2a1_bit0 -s14s10_bit0 -s14s11_bit0 -s14s12_bit0 -s14s13_bit0 -f1f4a2a4_bit0 o3b03_bit0 -f3a2a4f2_bit0 -o3b13_bit0 -f2a3a4f3_bit0 o3b23_bit0 -o3b30_bit0 o3b31_bit0 -o3b32_bit0 p04p00_bit0 p04p01_bit0 -s34p04_bit0 -p04p02_bit0 -f2f0a1a0_bit0 -p04p03_bit0 -s34p14_bit0 -f0f2a1a2_bit0 -a0f2f0a2_bit0 f4f1a3a1_bit0 a2f3f2a3_bit0 -f1f4a3a4_bit0 -o3c03_bit0 -o3c13_bit0 o3c23_bit0 o3c30_bit0 o3c31_bit0 -o3c32_bit0 -s03s00_bit0 -s03s01_bit0 -s03s02_bit0 -s03s04_bit0 -o3d03_bit0 -f4a1a2f1_bit0 -o3d13_bit0 o3d23_bit0 -f1a4a2f4_bit0 o3d30_bit0 o3d31_bit0 -o3d32_bit0 -s23p03_bit0 -s23p13_bit0 -f2a0a1f0_bit0 f0a2a1f2_bit0 o3e03_bit0 -f4a1a3f1_bit0 -o3e13_bit0 o3e23_bit0 f1a4a3f4_bit0 -o3e30_bit0 o3e31_bit0 -o3e32_bit0 f3f1a0a1_bit0 -f1f3a0a3_bit0 f4f3a2a3_bit0 -f3f4a2a4_bit0 -pipe0_bit0 -pipe0_bit1 -pipe1_bit0 -pipe1_bit1 pipe2_bit0 -pipe2_bit1 pipe3_bit0 -pipe3_bit1 -pipe4_bit0 -pipe4_bit1 -s34s30_bit0 -s34s31_bit0 -s34s32_bit0 -s34s33_bit0 -s12p02_bit0 -s12p12_bit0 o3f03_bit0 -o3f13_bit0 o3f23_bit0 -o3f30_bit0 o3f31_bit0 -o3f32_bit0 -f4f0a1a0_bit0 -f0f4a1a4_bit0 -a0a2f0f2_bit0 -a2a3f2f3_bit0 -o3g03_bit0 -o3g13_bit0 o3g23_bit0 o3g30_bit0 o3g31_bit0 -o3g32_bit0 -s23s20_bit0 -s23s21_bit0 -s23s22_bit0 -s23s24_bit0 -s01p01_bit0 -a1f3f1a3_bit0 -s01p11_bit0 -f3a1a0f1_bit0 -f1a3a0f3_bit0 -f4a3a2f3_bit0 -f3a4a2f4_bit0 -o3h03_bit0 -o3h13_bit0 o1a01_bit0 -p13p10_bit0 o3h23_bit0 p13p11_bit0 p13p12_bit0 -p13p14_bit0 -o1a10_bit0 -o1a12_bit0 -o1a13_bit0 o3h30_bit0 o3h31_bit0 -o3h32_bit0 o1a21_bit0 o1a31_bit0 -f4a0a1f0_bit0 f0a4a1f4_bit0 -s12s10_bit0 -s12s11_bit0 -s12s13_bit0 -s12s14_bit0 o1b01_bit0 -o1b10_bit0 -o1b12_bit0 -o1b13_bit0 -f4f2a0a2_bit0 o1b21_bit0 o1b31_bit0 -f2f4a0a4_bit0 -fl01_bit0 -fl02_bit0 -fl03_bit0 fl04_bit0 fl10_bit0 fl12_bit0 fl13_bit0 fl14_bit0 -fl20_bit0 -fl21_bit0 -fl23_bit0 -fl24_bit0 -fl30_bit0 -fl31_bit0 fl32_bit0 -fl34_bit0 -fl40_bit0 -fl41_bit0 -fl42_bit0 -fl43_bit0 -s32p02_bit0 -p02p00_bit0 -p02p01_bit0 -p02p03_bit0 -p02p04_bit0 -s32p12_bit0 o1c01_bit0 -o1c10_bit0 -o1c12_bit0 -o1c13_bit0 -f4f2a1a2_bit0 o1c21_bit0 o1c31_bit0 -f2f4a1a4_bit0 -s01s00_bit0 -s01s02_bit0 -s01s03_bit0 -s01s04_bit0 o1d01_bit0 -o1d10_bit0 -o1d12_bit0 -o1d13_bit0 o1d21_bit0 o1d31_bit0 s21p01_bit0 s21p11_bit0 a1a3f1f3_bit0 -f4a2a0f2_bit0 -f2a4a0f4_bit0 o1e01_bit0 -o1e10_bit0 -o1e12_bit0 -o1e13_bit0 o1e21_bit0 o1e31_bit0 -f4a2a1f2_bit0 f2a4a1f4_bit0 -s32s30_bit0 -s32s31_bit0 -s32s33_bit0 -s32s34_bit0 -s10p00_bit0 -s10p10_bit0 o1f01_bit0 -o1f10_bit0 -o1f12_bit0 -o1f13_bit0 o1f21_bit0 o1f31_bit0 -f2f0a4a0_bit0 -f0f2a4a2_bit0 o1g01_bit0 -o1g10_bit0 -o1g12_bit0 -o1g13_bit0 o1g21_bit0 o1g31_bit0 -s21s20_bit0 s21s22_bit0 -s21s23_bit0 s21s24_bit0 o1h01_bit0 -o1h10_bit0 -o1h12_bit0 -o1h13_bit0 o1h21_bit0 -p11p10_bit0 p11p12_bit0 p11p13_bit0 -p11p14_bit0 o1h31_bit0 -f2a0a4f0_bit0 -f0a2a4f2_bit0 -s10s11_bit0 -s10s12_bit0 -s10s13_bit0 -s10s14_bit0 -s04p04_bit0 -s04p14_bit0 dl01_bit0 -dl02_bit0 -dl03_bit0 -dl04_bit0 -dl10_bit0 -dl12_bit0 -dl13_bit0 -dl14_bit0 -f2f0a3a0_bit0 -dl20_bit0 dl21_bit0 dl23_bit0 -dl24_bit0 -f0f2a3a2_bit0 -dl30_bit0 dl31_bit0 -dl32_bit0 -dl34_bit0 dl40_bit0 dl41_bit0 -dl42_bit0 s30p00_bit0 -dl43_bit0 p00p01_bit0 -p00p02_bit0 -p00p03_bit0 p00p04_bit0 -s30p10_bit0 ssb01_bit0 ssb02_bit0 ssb03_bit0 ssb04_bit0 ssb10_bit0 -ssb12_bit0 ssb13_bit0 -ssb14_bit0 f3f1a4a1_bit0 ssb20_bit0 -ft0_bit0 -ssb21_bit0 -ft1_bit0 ft2_bit0 ssb23_bit0 -ft3_bit0 -ssb24_bit0 ft4_bit0 -f1f3a4a3_bit0 ssb30_bit0 ssb31_bit0 ssb32_bit0 ssb34_bit0 ssb40_bit0 -ssb41_bit0 -ssb42_bit0 ssb43_bit0 -f2a0a3f0_bit0 f0a2a3f2_bit0 -f4f0a2a0_bit0 -s04s00_bit0 -s04s01_bit0 -s04s02_bit0 -s04s03_bit0 f3f1a2a1_bit0 -f1f3a2a3_bit0 -f0f4a2a4_bit0 -f3a1a4f1_bit0 -f1a3a4f3_bit0 -s30s31_bit0 -s30s32_bit0 -s30s33_bit0 -s30s34_bit0 s24p04_bit0 -s24p14_bit0 a0f1f0a1_bit0 -f4f0a3a0_bit0 -f0f4a3a4_bit0 -f4a0a2f0_bit0 -f3a1a2f1_bit0 -f1a3a2f3_bit0 -f0a4a2f4_bit0 -s13p03_bit0 -s13p13_bit0 -ntt01_bit0 ntt02_bit0 -ntt03_bit0 -ntt04_bit_7 -ntt04_bit_6 -ntt04_bit_5 -ntt04_bit_4 -ntt04_bit_3 -ntt04_bit_2 -ntt04_bit_1 ntt10_bit0 ntt12_bit0 -ntt13_bit0 -ntt14_bit_7 -ntt14_bit_6 -ntt14_bit_5 -ntt14_bit_4 -ntt14_bit_3 -ntt14_bit_2 -ntt14_bit_1 ntt20_bit0 -ntt21_bit0 -ntt23_bit0 -ntt24_bit_7 -ntt24_bit_6 -ntt24_bit_5 -ntt24_bit_4 -ntt24_bit_3 -ntt24_bit_2 -ntt24_bit_1 ntt30_bit0 -ntt31_bit0 ntt32_bit0 -ntt34_bit_7 -ntt34_bit_6 -ntt34_bit_5 -ntt34_bit_4 -ntt34_bit_3 -ntt34_bit_2 -ntt34_bit_1 -ntt40_bit_7 -ntt40_bit_6 -ntt40_bit_5 -ntt40_bit_4 -ntt40_bit_3 -ntt40_bit_2 -ntt40_bit_1 -ntt41_bit_7 -ntt41_bit_6 -ntt41_bit_5 -ntt41_bit_4 -ntt41_bit_3 -ntt41_bit_2 -ntt41_bit_1 -ntt42_bit_7 -ntt42_bit_6 -ntt42_bit_5 -ntt42_bit_4 -ntt42_bit_3 -ntt42_bit_2 -ntt42_bit_1 -ntt43_bit_7 -ntt43_bit_6 -ntt43_bit_5 -ntt43_bit_4 -ntt43_bit_3 -ntt43_bit_2 -ntt43_bit_1 -f4a0a3f0_bit0 f0a4a3f4_bit0 f2f1a0a1_bit0 -f1f2a0a2_bit0 p00_bit0 p01_bit0 -p02_bit0 -p03_bit0 p04_bit0 -p10_bit0 p11_bit0 p12_bit0 p13_bit0 -p14_bit0 -s24s20_bit0 s24s21_bit0 s24s22_bit0 -s24s23_bit0 -lt0_bit0 lt1_bit0 -lt2_bit0 -lt3_bit0 -lt4_bit0 -s02p02_bit0 s02p12_bit0 -f3f0a1a0_bit0 o2a02_bit0 -p14p10_bit0 -p14p11_bit0 -p14p12_bit0 -p14p13_bit0 -o2a12_bit0 -f0f3a1a3_bit0 -a0f3f0a3_bit0 -f4f2a3a2_bit0 -o2a20_bit0 o2a21_bit0 o2a23_bit0 -a0a1f0f1_bit0 -o2a32_bit0 -f2f4a3a4_bit0 -s13s10_bit0 -s13s11_bit0 -s13s12_bit0 -s13s14_bit0 o2b02_bit0 -a1f2f1a2_bit0 -o2b12_bit0 -o2b20_bit0 o2b21_bit0 o2b23_bit0 -f4a0a2f2_bit0 -f4a0a2f2_bit1 -f4a0a2f2_bit2 -f4a0a2f2_bit3 -f4a0a2f2_bit4 -f4a0a2f2_bit5 -f4a0a2f2_bit6 -f4a0a2f2_bit7 -f4a0a2f2_bit8 -f4a0a2f2_bit9 -f4a0a2f2_bit10 -f4a0a2f2_bit11 -f4a0a2f2_bit12 f4a0a3f3_bit0 -f4a0a3f3_bit1 -f4a0a3f3_bit2 -f4a0a3f3_bit3 -f4a0a3f3_bit4 -f4a0a3f3_bit5 -f4a0a3f3_bit6 -f4a0a3f3_bit7 -f4a0a3f3_bit8 -f4a0a3f3_bit9 -f4a0a3f3_bit10 -f4a0a3f3_bit11 -f4a0a3f3_bit12 -b0_bit_7 -b0_bit_6 -b0_bit_5 -b0_bit_4 -b0_bit_3 -b0_bit_2 -b0_bit_1 -b0_bit0 -b0_bit1 -b0_bit2 -b0_bit3 -b0_bit4 -b0_bit5 -b0_bit6 -b0_bit7 -b0_bit8 -b0_bit9 -b0_bit10 -b0_bit11 -b0_bit12 -lot0_bit0 -lot0_bit1 -lot0_bit2 -lot0_bit3 -lot0_bit4 -lot0_bit5 -lot0_bit6 -lot0_bit7 -lot0_bit8 -lot0_bit9 -lot0_bit10 -lot0_bit11 -lot0_bit12 -sp120_bit_7 -sp120_bit_6 -sp120_bit_5 -sp120_bit_4 -sp120_bit_3 -sp120_bit_2 -sp120_bit_1 -sp120_bit0 -sp120_bit1 -sp120_bit2 -sp120_bit3 -sp120_bit4 -sp120_bit5 -sp120_bit6 -sp120_bit7 -sp120_bit8 -sp120_bit9 -sp120_bit10 -sp120_bit11 -sp120_bit12 -sp121_bit_7 -sp121_bit_6 -sp121_bit_5 -sp121_bit_4 -sp121_bit_3 -sp121_bit_2 -sp121_bit_1 sp121_bit0 -sp121_bit1 -sp121_bit2 -sp121_bit3 -sp121_bit4 -sp121_bit5 -sp121_bit6 -sp121_bit7 -sp121_bit8 -sp121_bit9 -sp121_bit10 -sp121_bit11 -sp121_bit12 -f1a2a0f0_bit0 -f1a2a0f0_bit1 -f1a2a0f0_bit2 -f1a2a0f0_bit3 -f1a2a0f0_bit4 -f1a2a0f0_bit5 -f1a2a0f0_bit6 -f1a2a0f0_bit7 -f1a2a0f0_bit8 -f1a2a0f0_bit9 -f1a2a0f0_bit10 -f1a2a0f0_bit11 -f1a2a0f0_bit12 -f1a2a3f3_bit0 -f1a2a3f3_bit1 -f1a2a3f3_bit2 -f1a2a3f3_bit3 -f1a2a3f3_bit4 -f1a2a3f3_bit5 -f1a2a3f3_bit6 -f1a2a3f3_bit7 -f1a2a3f3_bit8 -f1a2a3f3_bit9 -f1a2a3f3_bit10 -f1a2a3f3_bit11 -f1a2a3f3_bit12 -f1a2a4f4_bit0 -f1a2a4f4_bit1 -f1a2a4f4_bit2 -f1a2a4f4_bit3 -f1a2a4f4_bit4 -f1a2a4f4_bit5 -f1a2a4f4_bit6 -f1a2a4f4_bit7 -f1a2a4f4_bit8 -f1a2a4f4_bit9 -f1a2a4f4_bit10 -f1a2a4f4_bit11 -f1a2a4f4_bit12 -sp210_bit_7 -sp210_bit_6 -sp210_bit_5 -sp210_bit_4 -sp210_bit_3 -sp210_bit_2 -sp210_bit_1 -sp210_bit0 -sp210_bit1 -sp210_bit2 -sp210_bit3 -sp210_bit4 -sp210_bit5 -sp210_bit6 -sp210_bit7 -sp210_bit8 -sp210_bit9 -sp210_bit10 -sp210_bit11 -sp210_bit12 -sp211_bit_7 -sp211_bit_6 -sp211_bit_5 -sp211_bit_4 -sp211_bit_3 -sp211_bit_2 -sp211_bit_1 sp211_bit0 -sp211_bit1 -sp211_bit2 -sp211_bit3 -sp211_bit4 -sp211_bit5 -sp211_bit6 -sp211_bit7 -sp211_bit8 -sp211_bit9 -sp211_bit10 -sp211_bit11 -sp211_bit12 -f2a1a0f0_bit0 -f2a1a0f0_bit1 -f2a1a0f0_bit2 -f2a1a0f0_bit3 -f2a1a0f0_bit4 -f2a1a0f0_bit5 -f2a1a0f0_bit6 -f2a1a0f0_bit7 -f2a1a0f0_bit8 -f2a1a0f0_bit9 -f2a1a0f0_bit10 -f2a1a0f0_bit11 -f2a1a0f0_bit12 -f2a1a3f3_bit0 -f2a1a3f3_bit1 -f2a1a3f3_bit2 -f2a1a3f3_bit3 -f2a1a3f3_bit4 -f2a1a3f3_bit5 -f2a1a3f3_bit6 -f2a1a3f3_bit7 -f2a1a3f3_bit8 -f2a1a3f3_bit9 -f2a1a3f3_bit10 -f2a1a3f3_bit11 -f2a1a3f3_bit12 f2a1a4f4_bit0 -f2a1a4f4_bit1 -f2a1a4f4_bit2 -f2a1a4f4_bit3 -f2a1a4f4_bit4 -f2a1a4f4_bit5 -f2a1a4f4_bit6 -f2a1a4f4_bit7 -f2a1a4f4_bit8 -f2a1a4f4_bit9 -f2a1a4f4_bit10 -f2a1a4f4_bit11 -f2a1a4f4_bit12 -sp130_bit_7 -sp130_bit_6 -sp130_bit_5 -sp130_bit_4 -sp130_bit_3 -sp130_bit_2 -sp130_bit_1 -sp130_bit0 -sp130_bit1 -sp130_bit2 -sp130_bit3 -sp130_bit4 -sp130_bit5 -sp130_bit6 -sp130_bit7 -sp130_bit8 -sp130_bit9 -sp130_bit10 -sp130_bit11 -sp130_bit12 -sp131_bit_7 -sp131_bit_6 -sp131_bit_5 -sp131_bit_4 -sp131_bit_3 -sp131_bit_2 -sp131_bit_1 sp131_bit0 -sp131_bit1 -sp131_bit2 -sp131_bit3 -sp131_bit4 -sp131_bit5 -sp131_bit6 -sp131_bit7 -sp131_bit8 -sp131_bit9 -sp131_bit10 -sp131_bit11 -sp131_bit12 -f1a3a0f0_bit0 -f1a3a0f0_bit1 -f1a3a0f0_bit2 -f1a3a0f0_bit3 -f1a3a0f0_bit4 -f1a3a0f0_bit5 -f1a3a0f0_bit6 -f1a3a0f0_bit7 -f1a3a0f0_bit8 -f1a3a0f0_bit9 -f1a3a0f0_bit10 -f1a3a0f0_bit11 -f1a3a0f0_bit12 f1a3a2f2_bit0 -f1a3a2f2_bit1 -f1a3a2f2_bit2 -f1a3a2f2_bit3 -f1a3a2f2_bit4 -f1a3a2f2_bit5 -f1a3a2f2_bit6 -f1a3a2f2_bit7 -f1a3a2f2_bit8 -f1a3a2f2_bit9 -f1a3a2f2_bit10 -f1a3a2f2_bit11 -f1a3a2f2_bit12 f1a3a4f4_bit0 -f1a3a4f4_bit1 -f1a3a4f4_bit2 -f1a3a4f4_bit3 -f1a3a4f4_bit4 -f1a3a4f4_bit5 -f1a3a4f4_bit6 -f1a3a4f4_bit7 -f1a3a4f4_bit8 -f1a3a4f4_bit9 -f1a3a4f4_bit10 -f1a3a4f4_bit11 -f1a3a4f4_bit12 -sp310_bit_7 -sp310_bit_6 -sp310_bit_5 -sp310_bit_4 -sp310_bit_3 -sp310_bit_2 -sp310_bit_1 -sp310_bit0 -sp310_bit1 -sp310_bit2 -sp310_bit3 -sp310_bit4 -sp310_bit5 -sp310_bit6 -sp310_bit7 -sp310_bit8 -sp310_bit9 -sp310_bit10 -sp310_bit11 -sp310_bit12 -sp311_bit_7 -sp311_bit_6 -sp311_bit_5 -sp311_bit_4 -sp311_bit_3 -sp311_bit_2 -sp311_bit_1 sp311_bit0 -sp311_bit1 -sp311_bit2 -sp311_bit3 -sp311_bit4 -sp311_bit5 -sp311_bit6 -sp311_bit7 -sp311_bit8 -sp311_bit9 -sp311_bit10 -sp311_bit11 -sp311_bit12 -f3a1a0f0_bit0 -f3a1a0f0_bit1 -f3a1a0f0_bit2 -f3a1a0f0_bit3 -f3a1a0f0_bit4 -f3a1a0f0_bit5 -f3a1a0f0_bit6 -f3a1a0f0_bit7 -f3a1a0f0_bit8 -f3a1a0f0_bit9 -f3a1a0f0_bit10 -f3a1a0f0_bit11 -f3a1a0f0_bit12 f3a1a2f2_bit0 -f3a1a2f2_bit1 -f3a1a2f2_bit2 -f3a1a2f2_bit3 -f3a1a2f2_bit4 -f3a1a2f2_bit5 -f3a1a2f2_bit6 -f3a1a2f2_bit7 -f3a1a2f2_bit8 -f3a1a2f2_bit9 -f3a1a2f2_bit10 -f3a1a2f2_bit11 -f3a1a2f2_bit12 f3a1a4f4_bit0 -f3a1a4f4_bit1 -f3a1a4f4_bit2 -f3a1a4f4_bit3 -f3a1a4f4_bit4 -f3a1a4f4_bit5 -f3a1a4f4_bit6 -f3a1a4f4_bit7 -f3a1a4f4_bit8 -f3a1a4f4_bit9 -f3a1a4f4_bit10 -f3a1a4f4_bit11 -f3a1a4f4_bit12 -sp140_bit_7 -sp140_bit_6 -sp140_bit_5 -sp140_bit_4 -sp140_bit_3 -sp140_bit_2 -sp140_bit_1 sp140_bit0 -sp140_bit1 -sp140_bit2 -sp140_bit3 -sp140_bit4 -sp140_bit5 -sp140_bit6 -sp140_bit7 -sp140_bit8 -sp140_bit9 -sp140_bit10 -sp140_bit11 -sp140_bit12 -sp141_bit_7 -sp141_bit_6 -sp141_bit_5 -sp141_bit_4 -sp141_bit_3 -sp141_bit_2 -sp141_bit_1 -sp141_bit0 -sp141_bit1 -sp141_bit2 -sp141_bit3 -sp141_bit4 -sp141_bit5 -sp141_bit6 -sp141_bit7 -sp141_bit8 -sp141_bit9 -sp141_bit10 -sp141_bit11 -sp141_bit12 -f1a4a0f0_bit0 -f1a4a0f0_bit1 -f1a4a0f0_bit2 -f1a4a0f0_bit3 -f1a4a0f0_bit4 -f1a4a0f0_bit5 -f1a4a0f0_bit6 -f1a4a0f0_bit7 -f1a4a0f0_bit8 -f1a4a0f0_bit9 -f1a4a0f0_bit10 -f1a4a0f0_bit11 -f1a4a0f0_bit12 -f1a4a2f2_bit0 -f1a4a2f2_bit1 -f1a4a2f2_bit2 -f1a4a2f2_bit3 -f1a4a2f2_bit4 -f1a4a2f2_bit5 -f1a4a2f2_bit6 -f1a4a2f2_bit7 -f1a4a2f2_bit8 -f1a4a2f2_bit9 -f1a4a2f2_bit10 -f1a4a2f2_bit11 -f1a4a2f2_bit12 -f1a4a3f3_bit0 -f1a4a3f3_bit1 -f1a4a3f3_bit2 -f1a4a3f3_bit3 -f1a4a3f3_bit4 -f1a4a3f3_bit5 -f1a4a3f3_bit6 -f1a4a3f3_bit7 -f1a4a3f3_bit8 -f1a4a3f3_bit9 -f1a4a3f3_bit10 -f1a4a3f3_bit11 -f1a4a3f3_bit12 -sp410_bit_7 -sp410_bit_6 -sp410_bit_5 -sp410_bit_4 -sp410_bit_3 -sp410_bit_2 -sp410_bit_1 sp410_bit0 -sp410_bit1 -sp410_bit2 -sp410_bit3 -sp410_bit4 -sp410_bit5 -sp410_bit6 -sp410_bit7 -sp410_bit8 -sp410_bit9 -sp410_bit10 -sp410_bit11 -sp410_bit12 -sp411_bit_7 -sp411_bit_6 -sp411_bit_5 -sp411_bit_4 -sp411_bit_3 -sp411_bit_2 -sp411_bit_1 -sp411_bit0 -sp411_bit1 -sp411_bit2 -sp411_bit3 -sp411_bit4 -sp411_bit5 -sp411_bit6 -sp411_bit7 -sp411_bit8 -sp411_bit9 -sp411_bit10 -sp411_bit11 -sp411_bit12 -f4a1a0f0_bit0 -f4a1a0f0_bit1 -f4a1a0f0_bit2 -f4a1a0f0_bit3 -f4a1a0f0_bit4 -f4a1a0f0_bit5 -f4a1a0f0_bit6 -f4a1a0f0_bit7 -f4a1a0f0_bit8 -f4a1a0f0_bit9 -f4a1a0f0_bit10 -f4a1a0f0_bit11 -f4a1a0f0_bit12 -f4a1a2f2_bit0 -f4a1a2f2_bit1 -f4a1a2f2_bit2 -f4a1a2f2_bit3 -f4a1a2f2_bit4 -f4a1a2f2_bit5 -f4a1a2f2_bit6 -f4a1a2f2_bit7 -f4a1a2f2_bit8 -f4a1a2f2_bit9 -f4a1a2f2_bit10 -f4a1a2f2_bit11 -f4a1a2f2_bit12 -f4a1a3f3_bit0 -f4a1a3f3_bit1 -f4a1a3f3_bit2 -f4a1a3f3_bit3 -f4a1a3f3_bit4 -f4a1a3f3_bit5 -f4a1a3f3_bit6 -f4a1a3f3_bit7 -f4a1a3f3_bit8 -f4a1a3f3_bit9 -f4a1a3f3_bit10 -f4a1a3f3_bit11 -f4a1a3f3_bit12 -b1_bit_7 -b1_bit_6 -b1_bit_5 -b1_bit_4 -b1_bit_3 -b1_bit_2 -b1_bit_1 -b1_bit0 -b1_bit1 -b1_bit2 -b1_bit3 -b1_bit4 -b1_bit5 -b1_bit6 -b1_bit7 -b1_bit8 -b1_bit9 -b1_bit10 -b1_bit11 -b1_bit12 -lot1_bit0 -lot1_bit1 -lot1_bit2 -lot1_bit3 -lot1_bit4 -lot1_bit5 -lot1_bit6 -lot1_bit7 -lot1_bit8 -lot1_bit9 -lot1_bit10 -lot1_bit11 -lot1_bit12 -sp230_bit_7 -sp230_bit_6 -sp230_bit_5 -sp230_bit_4 -sp230_bit_3 -sp230_bit_2 -sp230_bit_1 -sp230_bit0 -sp230_bit1 -sp230_bit2 -sp230_bit3 -sp230_bit4 -sp230_bit5 -sp230_bit6 -sp230_bit7 -sp230_bit8 -sp230_bit9 -sp230_bit10 -sp230_bit11 -sp230_bit12 -sp231_bit_7 -sp231_bit_6 -sp231_bit_5 -sp231_bit_4 -sp231_bit_3 -sp231_bit_2 -sp231_bit_1 sp231_bit0 -sp231_bit1 -sp231_bit2 -sp231_bit3 -sp231_bit4 -sp231_bit5 -sp231_bit6 -sp231_bit7 -sp231_bit8 -sp231_bit9 -sp231_bit10 -sp231_bit11 -sp231_bit12 -f2a3a0f0_bit0 -f2a3a0f0_bit1 -f2a3a0f0_bit2 -f2a3a0f0_bit3 -f2a3a0f0_bit4 -f2a3a0f0_bit5 -f2a3a0f0_bit6 -f2a3a0f0_bit7 -f2a3a0f0_bit8 -f2a3a0f0_bit9 -f2a3a0f0_bit10 -f2a3a0f0_bit11 -f2a3a0f0_bit12 f2a3a1f1_bit0 -f2a3a1f1_bit1 -f2a3a1f1_bit2 -f2a3a1f1_bit3 -f2a3a1f1_bit4 -f2a3a1f1_bit5 -f2a3a1f1_bit6 -f2a3a1f1_bit7 -f2a3a1f1_bit8 -f2a3a1f1_bit9 -f2a3a1f1_bit10 -f2a3a1f1_bit11 -f2a3a1f1_bit12 f2a3a4f4_bit0 -f2a3a4f4_bit1 -f2a3a4f4_bit2 -f2a3a4f4_bit3 -f2a3a4f4_bit4 -f2a3a4f4_bit5 -f2a3a4f4_bit6 -f2a3a4f4_bit7 -f2a3a4f4_bit8 -f2a3a4f4_bit9 -f2a3a4f4_bit10 -f2a3a4f4_bit11 -f2a3a4f4_bit12 -sp320_bit_7 -sp320_bit_6 -sp320_bit_5 -sp320_bit_4 -sp320_bit_3 -sp320_bit_2 -sp320_bit_1 -sp320_bit0 -sp320_bit1 -sp320_bit2 -sp320_bit3 -sp320_bit4 -sp320_bit5 -sp320_bit6 -sp320_bit7 -sp320_bit8 -sp320_bit9 -sp320_bit10 -sp320_bit11 -sp320_bit12 -sp321_bit_7 -sp321_bit_6 -sp321_bit_5 -sp321_bit_4 -sp321_bit_3 -sp321_bit_2 -sp321_bit_1 sp321_bit0 -sp321_bit1 -sp321_bit2 -sp321_bit3 -sp321_bit4 -sp321_bit5 -sp321_bit6 -sp321_bit7 -sp321_bit8 -sp321_bit9 -sp321_bit10 -sp321_bit11 -sp321_bit12 -f3a2a0f0_bit0 -f3a2a0f0_bit1 -f3a2a0f0_bit2 -f3a2a0f0_bit3 -f3a2a0f0_bit4 -f3a2a0f0_bit5 -f3a2a0f0_bit6 -f3a2a0f0_bit7 -f3a2a0f0_bit8 -f3a2a0f0_bit9 -f3a2a0f0_bit10 -f3a2a0f0_bit11 -f3a2a0f0_bit12 f3a2a1f1_bit0 -f3a2a1f1_bit1 -f3a2a1f1_bit2 -f3a2a1f1_bit3 -f3a2a1f1_bit4 -f3a2a1f1_bit5 -f3a2a1f1_bit6 -f3a2a1f1_bit7 -f3a2a1f1_bit8 -f3a2a1f1_bit9 -f3a2a1f1_bit10 -f3a2a1f1_bit11 -f3a2a1f1_bit12 fl0_bit0 -fl0_bit1 -fl0_bit2 -fl0_bit3 -fl0_bit4 -fl0_bit5 -fl0_bit6 -fl0_bit7 -fl0_bit8 -fl0_bit9 -fl0_bit10 -fl0_bit11 -fl0_bit12 -f3a2a4f4_bit0 -f3a2a4f4_bit1 -f3a2a4f4_bit2 -f3a2a4f4_bit3 -f3a2a4f4_bit4 -f3a2a4f4_bit5 -f3a2a4f4_bit6 -f3a2a4f4_bit7 -f3a2a4f4_bit8 -f3a2a4f4_bit9 -f3a2a4f4_bit10 -f3a2a4f4_bit11 -f3a2a4f4_bit12 -sp240_bit_7 -sp240_bit_6 -sp240_bit_5 -sp240_bit_4 -sp240_bit_3 -sp240_bit_2 -sp240_bit_1 -sp240_bit0 -sp240_bit1 -sp240_bit2 -sp240_bit3 -sp240_bit4 -sp240_bit5 -sp240_bit6 -sp240_bit7 -sp240_bit8 -sp240_bit9 -sp240_bit10 -sp240_bit11 -sp240_bit12 -sp241_bit_7 -sp241_bit_6 -sp241_bit_5 -sp241_bit_4 -sp241_bit_3 -sp241_bit_2 -sp241_bit_1 -sp241_bit0 -sp241_bit1 -sp241_bit2 -sp241_bit3 -sp241_bit4 -sp241_bit5 -sp241_bit6 -sp241_bit7 -sp241_bit8 -sp241_bit9 -sp241_bit10 -sp241_bit11 -sp241_bit12 -fl1_bit0 -fl1_bit1 fl1_bit2 -fl1_bit3 -fl1_bit4 -fl1_bit5 -fl1_bit6 -fl1_bit7 -fl1_bit8 -fl1_bit9 -fl1_bit10 -fl1_bit11 -fl1_bit12 -f2a4a0f0_bit0 -f2a4a0f0_bit1 -f2a4a0f0_bit2 -f2a4a0f0_bit3 -f2a4a0f0_bit4 -f2a4a0f0_bit5 -f2a4a0f0_bit6 -f2a4a0f0_bit7 -f2a4a0f0_bit8 -f2a4a0f0_bit9 -f2a4a0f0_bit10 -f2a4a0f0_bit11 -f2a4a0f0_bit12 f2a4a1f1_bit0 -f2a4a1f1_bit1 -f2a4a1f1_bit2 -f2a4a1f1_bit3 -f2a4a1f1_bit4 -f2a4a1f1_bit5 -f2a4a1f1_bit6 -f2a4a1f1_bit7 -f2a4a1f1_bit8 -f2a4a1f1_bit9 -f2a4a1f1_bit10 -f2a4a1f1_bit11 -f2a4a1f1_bit12 -fl2_bit0 -fl2_bit1 -fl2_bit2 -fl2_bit3 -fl2_bit4 -fl2_bit5 -fl2_bit6 -fl2_bit7 -fl2_bit8 -fl2_bit9 -fl2_bit10 -fl2_bit11 -fl2_bit12 f2a4a3f3_bit0 -f2a4a3f3_bit1 -f2a4a3f3_bit2 -f2a4a3f3_bit3 -f2a4a3f3_bit4 -f2a4a3f3_bit5 -f2a4a3f3_bit6 -f2a4a3f3_bit7 -f2a4a3f3_bit8 -f2a4a3f3_bit9 -f2a4a3f3_bit10 -f2a4a3f3_bit11 -f2a4a3f3_bit12 -sp420_bit_7 -sp420_bit_6 -sp420_bit_5 -sp420_bit_4 -sp420_bit_3 -sp420_bit_2 -sp420_bit_1 -sp420_bit0 -sp420_bit1 -sp420_bit2 -sp420_bit3 -sp420_bit4 -sp420_bit5 -sp420_bit6 -sp420_bit7 -sp420_bit8 -sp420_bit9 -sp420_bit10 -sp420_bit11 -sp420_bit12 -sp421_bit_7 -sp421_bit_6 -sp421_bit_5 -sp421_bit_4 -sp421_bit_3 -sp421_bit_2 -sp421_bit_1 -sp421_bit0 -sp421_bit1 -sp421_bit2 -sp421_bit3 -sp421_bit4 -sp421_bit5 -sp421_bit6 -sp421_bit7 -sp421_bit8 -sp421_bit9 -sp421_bit10 -sp421_bit11 -sp421_bit12 fl3_bit0 -fl3_bit1 -fl3_bit2 -fl3_bit3 -fl3_bit4 -fl3_bit5 -fl3_bit6 -fl3_bit7 -fl3_bit8 -fl3_bit9 -fl3_bit10 -fl3_bit11 -fl3_bit12 -f4a2a0f0_bit0 -f4a2a0f0_bit1 -f4a2a0f0_bit2 -f4a2a0f0_bit3 -f4a2a0f0_bit4 -f4a2a0f0_bit5 -f4a2a0f0_bit6 -f4a2a0f0_bit7 -f4a2a0f0_bit8 -f4a2a0f0_bit9 -f4a2a0f0_bit10 -f4a2a0f0_bit11 -f4a2a0f0_bit12 f4a2a1f1_bit0 -f4a2a1f1_bit1 -f4a2a1f1_bit2 -f4a2a1f1_bit3 -f4a2a1f1_bit4 -f4a2a1f1_bit5 -f4a2a1f1_bit6 -f4a2a1f1_bit7 -f4a2a1f1_bit8 -f4a2a1f1_bit9 -f4a2a1f1_bit10 -f4a2a1f1_bit11 -f4a2a1f1_bit12 -fl4_bit0 -fl4_bit1 -fl4_bit2 -fl4_bit3 -fl4_bit4 -fl4_bit5 -fl4_bit6 -fl4_bit7 -fl4_bit8 -fl4_bit9 -fl4_bit10 -fl4_bit11 -fl4_bit12 f4a2a3f3_bit0 -f4a2a3f3_bit1 -f4a2a3f3_bit2 -f4a2a3f3_bit3 -f4a2a3f3_bit4 -f4a2a3f3_bit5 -f4a2a3f3_bit6 -f4a2a3f3_bit7 -f4a2a3f3_bit8 -f4a2a3f3_bit9 -f4a2a3f3_bit10 -f4a2a3f3_bit11 -f4a2a3f3_bit12 -b2_bit_7 -b2_bit_6 -b2_bit_5 -b2_bit_4 -b2_bit_3 -b2_bit_2 -b2_bit_1 -b2_bit0 -b2_bit1 -b2_bit2 -b2_bit3 -b2_bit4 -b2_bit5 -b2_bit6 -b2_bit7 -b2_bit8 -b2_bit9 -b2_bit10 -b2_bit11 -b2_bit12 -lot2_bit0 -lot2_bit1 -lot2_bit2 -lot2_bit3 -lot2_bit4 -lot2_bit5 -lot2_bit6 -lot2_bit7 -lot2_bit8 -lot2_bit9 -lot2_bit10 -lot2_bit11 -lot2_bit12 -sp340_bit_7 -sp340_bit_6 -sp340_bit_5 -sp340_bit_4 -sp340_bit_3 -sp340_bit_2 -sp340_bit_1 -sp340_bit0 -sp340_bit1 -sp340_bit2 -sp340_bit3 -sp340_bit4 -sp340_bit5 -sp340_bit6 -sp340_bit7 -sp340_bit8 -sp340_bit9 -sp340_bit10 -sp340_bit11 -sp340_bit12 -sp341_bit_7 -sp341_bit_6 -sp341_bit_5 -sp341_bit_4 -sp341_bit_3 -sp341_bit_2 -sp341_bit_1 -sp341_bit0 -sp341_bit1 -sp341_bit2 -sp341_bit3 -sp341_bit4 -sp341_bit5 -sp341_bit6 -sp341_bit7 -sp341_bit8 -sp341_bit9 -sp341_bit10 -sp341_bit11 -sp341_bit12 -f3a4a0f0_bit0 -f3a4a0f0_bit1 -f3a4a0f0_bit2 -f3a4a0f0_bit3 -f3a4a0f0_bit4 -f3a4a0f0_bit5 -f3a4a0f0_bit6 -f3a4a0f0_bit7 -f3a4a0f0_bit8 -f3a4a0f0_bit9 -f3a4a0f0_bit10 -f3a4a0f0_bit11 -f3a4a0f0_bit12 f3a4a1f1_bit0 -f3a4a1f1_bit1 -f3a4a1f1_bit2 -f3a4a1f1_bit3 -f3a4a1f1_bit4 -f3a4a1f1_bit5 -f3a4a1f1_bit6 -f3a4a1f1_bit7 -f3a4a1f1_bit8 -f3a4a1f1_bit9 -f3a4a1f1_bit10 -f3a4a1f1_bit11 -f3a4a1f1_bit12 -f3a4a2f2_bit0 -f3a4a2f2_bit1 -f3a4a2f2_bit2 -f3a4a2f2_bit3 -f3a4a2f2_bit4 -f3a4a2f2_bit5 -f3a4a2f2_bit6 -f3a4a2f2_bit7 -f3a4a2f2_bit8 -f3a4a2f2_bit9 -f3a4a2f2_bit10 -f3a4a2f2_bit11 -f3a4a2f2_bit12 -sp430_bit_7 -sp430_bit_6 -sp430_bit_5 -sp430_bit_4 -sp430_bit_3 -sp430_bit_2 -sp430_bit_1 -sp430_bit0 -sp430_bit1 -sp430_bit2 -sp430_bit3 -sp430_bit4 -sp430_bit5 -sp430_bit6 -sp430_bit7 -sp430_bit8 -sp430_bit9 -sp430_bit10 -sp430_bit11 -sp430_bit12 -sp431_bit_7 -sp431_bit_6 -sp431_bit_5 -sp431_bit_4 -sp431_bit_3 -sp431_bit_2 -sp431_bit_1 -sp431_bit0 -sp431_bit1 -sp431_bit2 -sp431_bit3 -sp431_bit4 -sp431_bit5 -sp431_bit6 -sp431_bit7 -sp431_bit8 -sp431_bit9 -sp431_bit10 -sp431_bit11 -sp431_bit12 -f4a3a0f0_bit0 -f4a3a0f0_bit1 -f4a3a0f0_bit2 -f4a3a0f0_bit3 -f4a3a0f0_bit4 -f4a3a0f0_bit5 -f4a3a0f0_bit6 -f4a3a0f0_bit7 -f4a3a0f0_bit8 -f4a3a0f0_bit9 -f4a3a0f0_bit10 -f4a3a0f0_bit11 -f4a3a0f0_bit12 f4a3a1f1_bit0 -f4a3a1f1_bit1 -f4a3a1f1_bit2 -f4a3a1f1_bit3 -f4a3a1f1_bit4 -f4a3a1f1_bit5 -f4a3a1f1_bit6 -f4a3a1f1_bit7 -f4a3a1f1_bit8 -f4a3a1f1_bit9 -f4a3a1f1_bit10 -f4a3a1f1_bit11 -f4a3a1f1_bit12 -f4a3a2f2_bit0 -f4a3a2f2_bit1 -f4a3a2f2_bit2 -f4a3a2f2_bit3 -f4a3a2f2_bit4 -f4a3a2f2_bit5 -f4a3a2f2_bit6 -f4a3a2f2_bit7 -f4a3a2f2_bit8 -f4a3a2f2_bit9 -f4a3a2f2_bit10 -f4a3a2f2_bit11 -f4a3a2f2_bit12 -b3_bit_7 -b3_bit_6 -b3_bit_5 -b3_bit_4 -b3_bit_3 -b3_bit_2 -b3_bit_1 -b3_bit0 -b3_bit1 -b3_bit2 -b3_bit3 -b3_bit4 -b3_bit5 -b3_bit6 -b3_bit7 -b3_bit8 -b3_bit9 -b3_bit10 -b3_bit11 -b3_bit12 -lot3_bit0 -lot3_bit1 -lot3_bit2 -lot3_bit3 -lot3_bit4 -lot3_bit5 -lot3_bit6 -lot3_bit7 -lot3_bit8 -lot3_bit9 -lot3_bit10 -lot3_bit11 -lot3_bit12 -b4_bit_7 -b4_bit_6 -b4_bit_5 -b4_bit_4 -b4_bit_3 -b4_bit_2 -b4_bit_1 -b4_bit0 b4_bit1 -b4_bit2 b4_bit3 -b4_bit4 -b4_bit5 -b4_bit6 -b4_bit7 -b4_bit8 -b4_bit9 -b4_bit10 -b4_bit11 -b4_bit12 -lot4_bit0 -lot4_bit1 -lot4_bit2 -lot4_bit3 -lot4_bit4 -lot4_bit5 -lot4_bit6 -lot4_bit7 -lot4_bit8 -lot4_bit9 -lot4_bit10 -lot4_bit11 -lot4_bit12 -p20_bit_7 -p20_bit_6 -p20_bit_5 -p20_bit_4 -p20_bit_3 -p20_bit_2 -p20_bit_1 -p20_bit0 -p20_bit1 -p20_bit2 -p20_bit3 -p20_bit4 -p20_bit5 -p20_bit6 -p20_bit7 -p20_bit8 -p20_bit9 -p20_bit10 -p20_bit11 -p20_bit12 -p30_bit_7 -p30_bit_6 -p30_bit_5 -p30_bit_4 -p30_bit_3 -p30_bit_2 -p30_bit_1 -p30_bit0 -p30_bit1 -p30_bit2 -p30_bit3 -p30_bit4 -p30_bit5 -p30_bit6 -p30_bit7 -p30_bit8 -p30_bit9 -p30_bit10 -p30_bit11 -p30_bit12 -p40_bit_7 -p40_bit_6 -p40_bit_5 -p40_bit_4 -p40_bit_3 -p40_bit_2 -p40_bit_1 p40_bit0 -p40_bit1 -p40_bit2 -p40_bit3 -p40_bit4 -p40_bit5 -p40_bit6 -p40_bit7 -p40_bit8 -p40_bit9 -p40_bit10 -p40_bit11 -p40_bit12 -s40_bit_7 -s40_bit_6 -s40_bit_5 -s40_bit_4 -s40_bit_3 -s40_bit_2 -s40_bit_1 -s40_bit0 -s40_bit1 -s40_bit2 -s40_bit3 -s40_bit4 -s40_bit5 -s40_bit6 -s40_bit7 -s40_bit8 -s40_bit9 -s40_bit10 -s40_bit11 -s40_bit12 -exec000_bit_7 -exec000_bit_6 -exec000_bit_5 -exec000_bit_4 -exec000_bit_3 -exec000_bit_2 -exec000_bit_1 -exec000_bit0 -exec000_bit1 -exec000_bit2 -exec000_bit3 -exec000_bit4 -exec000_bit5 -exec000_bit6 -exec000_bit7 -exec000_bit8 -exec000_bit9 -exec000_bit10 -exec000_bit11 -exec000_bit12 -exec001_bit_7 -exec001_bit_6 -exec001_bit_5 -exec001_bit_4 -exec001_bit_3 -exec001_bit_2 -exec001_bit_1 -exec001_bit0 -exec001_bit1 -exec001_bit2 -exec001_bit3 -exec001_bit4 -exec001_bit5 -exec001_bit6 -exec001_bit7 -exec001_bit8 -exec001_bit9 -exec001_bit10 -exec001_bit11 -exec001_bit12 -exec002_bit_7 -exec002_bit_6 -exec002_bit_5 -exec002_bit_4 -exec002_bit_3 -exec002_bit_2 -exec002_bit_1 -exec002_bit0 -exec002_bit1 -exec002_bit2 -exec002_bit3 -exec002_bit4 -exec002_bit5 -exec002_bit6 -exec002_bit7 -exec002_bit8 -exec002_bit9 -exec002_bit10 -exec002_bit11 -exec002_bit12 -exec003_bit_7 -exec003_bit_6 -exec003_bit_5 -exec003_bit_4 -exec003_bit_3 -exec003_bit_2 -exec003_bit_1 -exec003_bit0 exec003_bit1 exec003_bit2 -exec003_bit3 exec003_bit4 -exec003_bit5 -exec003_bit6 exec003_bit7 -exec003_bit8 -exec003_bit9 -exec003_bit10 -exec003_bit11 -exec003_bit12 -exec010_bit_7 -exec010_bit_6 -exec010_bit_5 -exec010_bit_4 -exec010_bit_3 -exec010_bit_2 -exec010_bit_1 -exec010_bit0 -exec010_bit1 -exec010_bit2 -exec010_bit3 -exec010_bit4 -exec010_bit5 -exec010_bit6 -exec010_bit7 -exec010_bit8 -exec010_bit9 -exec010_bit10 -exec010_bit11 -exec010_bit12 -exec011_bit_7 -exec011_bit_6 -exec011_bit_5 -exec011_bit_4 -exec011_bit_3 -exec011_bit_2 -exec011_bit_1 -exec011_bit0 -exec011_bit1 -exec011_bit2 -exec011_bit3 -exec011_bit4 -exec011_bit5 -exec011_bit6 -exec011_bit7 -exec011_bit8 -exec011_bit9 -exec011_bit10 -exec011_bit11 -exec011_bit12 -exec012_bit_7 -exec012_bit_6 -exec012_bit_5 -exec012_bit_4 -exec012_bit_3 -exec012_bit_2 -exec012_bit_1 -exec012_bit0 -exec012_bit1 -exec012_bit2 -exec012_bit3 -exec012_bit4 -exec012_bit5 -exec012_bit6 -exec012_bit7 -exec012_bit8 -exec012_bit9 -exec012_bit10 -exec012_bit11 -exec012_bit12 -exec013_bit_7 -exec013_bit_6 -exec013_bit_5 -exec013_bit_4 -exec013_bit_3 -exec013_bit_2 -exec013_bit_1 -exec013_bit0 -exec013_bit1 -exec013_bit2 -exec013_bit3 -exec013_bit4 -exec013_bit5 -exec013_bit6 -exec013_bit7 -exec013_bit8 -exec013_bit9 -exec013_bit10 -exec013_bit11 -exec013_bit12 -exec100_bit_7 -exec100_bit_6 -exec100_bit_5 -exec100_bit_4 -exec100_bit_3 -exec100_bit_2 -exec100_bit_1 -exec100_bit0 -exec100_bit1 -exec100_bit2 -exec100_bit3 -exec100_bit4 -exec100_bit5 -exec100_bit6 -exec100_bit7 -exec100_bit8 -exec100_bit9 -exec100_bit10 -exec100_bit11 -exec100_bit12 -exec101_bit_7 -exec101_bit_6 -exec101_bit_5 -exec101_bit_4 -exec101_bit_3 -exec101_bit_2 -exec101_bit_1 -exec101_bit0 -exec101_bit1 -exec101_bit2 -exec101_bit3 -exec101_bit4 -exec101_bit5 -exec101_bit6 -exec101_bit7 -exec101_bit8 -exec101_bit9 -exec101_bit10 -exec101_bit11 -exec101_bit12 -exec102_bit_7 -exec102_bit_6 -exec102_bit_5 -exec102_bit_4 -exec102_bit_3 -exec102_bit_2 -exec102_bit_1 -exec102_bit0 -exec102_bit1 exec102_bit2 -exec102_bit3 exec102_bit4 -exec102_bit5 exec102_bit6 -exec102_bit7 -exec102_bit8 -exec102_bit9 -exec102_bit10 -exec102_bit11 -exec102_bit12 -exec103_bit_7 -exec103_bit_6 -exec103_bit_5 -exec103_bit_4 -exec103_bit_3 -exec103_bit_2 -exec103_bit_1 -exec103_bit0 -exec103_bit1 -exec103_bit2 -exec103_bit3 -exec103_bit4 -exec103_bit5 -exec103_bit6 -exec103_bit7 -exec103_bit8 -exec103_bit9 -exec103_bit10 -exec103_bit11 -exec103_bit12 -exec110_bit_7 -exec110_bit_6 -exec110_bit_5 -exec110_bit_4 -exec110_bit_3 -exec110_bit_2 -exec110_bit_1 -exec110_bit0 -exec110_bit1 -exec110_bit2 -exec110_bit3 -exec110_bit4 -exec110_bit5 -exec110_bit6 -exec110_bit7 -exec110_bit8 -exec110_bit9 -exec110_bit10 -exec110_bit11 -exec110_bit12 -exec111_bit_7 -exec111_bit_6 -exec111_bit_5 -exec111_bit_4 -exec111_bit_3 -exec111_bit_2 -exec111_bit_1 -exec111_bit0 -exec111_bit1 -exec111_bit2 -exec111_bit3 -exec111_bit4 -exec111_bit5 -exec111_bit6 -exec111_bit7 -exec111_bit8 -exec111_bit9 -exec111_bit10 -exec111_bit11 -exec111_bit12 -exec112_bit_7 -exec112_bit_6 -exec112_bit_5 -exec112_bit_4 -exec112_bit_3 -exec112_bit_2 -exec112_bit_1 -exec112_bit0 -exec112_bit1 exec112_bit2 -exec112_bit3 exec112_bit4 -exec112_bit5 exec112_bit6 -exec112_bit7 -exec112_bit8 -exec112_bit9 -exec112_bit10 -exec112_bit11 -exec112_bit12 -exec113_bit_7 -exec113_bit_6 -exec113_bit_5 -exec113_bit_4 -exec113_bit_3 -exec113_bit_2 -exec113_bit_1 -exec113_bit0 -exec113_bit1 -exec113_bit2 -exec113_bit3 -exec113_bit4 -exec113_bit5 -exec113_bit6 -exec113_bit7 -exec113_bit8 -exec113_bit9 -exec113_bit10 -exec113_bit11 -exec113_bit12 -exec200_bit_7 -exec200_bit_6 -exec200_bit_5 -exec200_bit_4 -exec200_bit_3 -exec200_bit_2 -exec200_bit_1 -exec200_bit0 -exec200_bit1 -exec200_bit2 -exec200_bit3 -exec200_bit4 -exec200_bit5 -exec200_bit6 -exec200_bit7 -exec200_bit8 -exec200_bit9 -exec200_bit10 -exec200_bit11 -exec200_bit12 -exec201_bit_7 -exec201_bit_6 -exec201_bit_5 -exec201_bit_4 -exec201_bit_3 -exec201_bit_2 -exec201_bit_1 -exec201_bit0 -exec201_bit1 -exec201_bit2 -exec201_bit3 -exec201_bit4 -exec201_bit5 -exec201_bit6 -exec201_bit7 -exec201_bit8 -exec201_bit9 -exec201_bit10 -exec201_bit11 -exec201_bit12 -exec202_bit_7 -exec202_bit_6 -exec202_bit_5 -exec202_bit_4 -exec202_bit_3 -exec202_bit_2 -exec202_bit_1 -exec202_bit0 -exec202_bit1 -exec202_bit2 -exec202_bit3 -exec202_bit4 -exec202_bit5 -exec202_bit6 -exec202_bit7 -exec202_bit8 -exec202_bit9 -exec202_bit10 -exec202_bit11 -exec202_bit12 -exec203_bit_7 -exec203_bit_6 -exec203_bit_5 -exec203_bit_4 -exec203_bit_3 -exec203_bit_2 -exec203_bit_1 -exec203_bit0 -exec203_bit1 -exec203_bit2 -exec203_bit3 -exec203_bit4 -exec203_bit5 -exec203_bit6 -exec203_bit7 -exec203_bit8 -exec203_bit9 -exec203_bit10 -exec203_bit11 -exec203_bit12 -exec210_bit_7 -exec210_bit_6 -exec210_bit_5 -exec210_bit_4 -exec210_bit_3 -exec210_bit_2 -exec210_bit_1 exec210_bit0 -exec210_bit1 -exec210_bit2 -exec210_bit3 -exec210_bit4 -exec210_bit5 exec210_bit6 -exec210_bit7 -exec210_bit8 -exec210_bit9 -exec210_bit10 -exec210_bit11 -exec210_bit12 -exec211_bit_7 -exec211_bit_6 -exec211_bit_5 -exec211_bit_4 -exec211_bit_3 -exec211_bit_2 -exec211_bit_1 -exec211_bit0 -exec211_bit1 -exec211_bit2 -exec211_bit3 -exec211_bit4 -exec211_bit5 -exec211_bit6 -exec211_bit7 -exec211_bit8 -exec211_bit9 -exec211_bit10 -exec211_bit11 -exec211_bit12 -exec212_bit_7 -exec212_bit_6 -exec212_bit_5 -exec212_bit_4 -exec212_bit_3 -exec212_bit_2 -exec212_bit_1 exec212_bit0 exec212_bit1 -exec212_bit2 exec212_bit3 -exec212_bit4 -exec212_bit5 exec212_bit6 -exec212_bit7 -exec212_bit8 -exec212_bit9 -exec212_bit10 -exec212_bit11 -exec212_bit12 -exec213_bit_7 -exec213_bit_6 -exec213_bit_5 -exec213_bit_4 -exec213_bit_3 -exec213_bit_2 -exec213_bit_1 -exec213_bit0 -exec213_bit1 -exec213_bit2 -exec213_bit3 -exec213_bit4 -exec213_bit5 -exec213_bit6 -exec213_bit7 -exec213_bit8 -exec213_bit9 -exec213_bit10 -exec213_bit11 -exec213_bit12 -exec300_bit_7 -exec300_bit_6 -exec300_bit_5 -exec300_bit_4 -exec300_bit_3 -exec300_bit_2 -exec300_bit_1 -exec300_bit0 -exec300_bit1 -exec300_bit2 -exec300_bit3 -exec300_bit4 -exec300_bit5 -exec300_bit6 -exec300_bit7 -exec300_bit8 -exec300_bit9 -exec300_bit10 -exec300_bit11 -exec300_bit12 -exec301_bit_7 -exec301_bit_6 -exec301_bit_5 -exec301_bit_4 -exec301_bit_3 -exec301_bit_2 -exec301_bit_1 -exec301_bit0 -exec301_bit1 -exec301_bit2 -exec301_bit3 -exec301_bit4 -exec301_bit5 -exec301_bit6 -exec301_bit7 -exec301_bit8 -exec301_bit9 -exec301_bit10 -exec301_bit11 -exec301_bit12 -exec302_bit_7 -exec302_bit_6 -exec302_bit_5 -exec302_bit_4 -exec302_bit_3 -exec302_bit_2 -exec302_bit_1 -exec302_bit0 -exec302_bit1 -exec302_bit2 -exec302_bit3 -exec302_bit4 -exec302_bit5 -exec302_bit6 -exec302_bit7 -exec302_bit8 -exec302_bit9 -exec302_bit10 -exec302_bit11 -exec302_bit12 -exec303_bit_7 -exec303_bit_6 -exec303_bit_5 -exec303_bit_4 -exec303_bit_3 -exec303_bit_2 -exec303_bit_1 -exec303_bit0 -exec303_bit1 -exec303_bit2 -exec303_bit3 -exec303_bit4 -exec303_bit5 -exec303_bit6 -exec303_bit7 -exec303_bit8 -exec303_bit9 -exec303_bit10 -exec303_bit11 -exec303_bit12 -exec310_bit_7 -exec310_bit_6 -exec310_bit_5 -exec310_bit_4 -exec310_bit_3 -exec310_bit_2 -exec310_bit_1 -exec310_bit0 -exec310_bit1 -exec310_bit2 -exec310_bit3 -exec310_bit4 -exec310_bit5 -exec310_bit6 -exec310_bit7 -exec310_bit8 -exec310_bit9 -exec310_bit10 -exec310_bit11 -exec310_bit12 -exec311_bit_7 -exec311_bit_6 -exec311_bit_5 -exec311_bit_4 -exec311_bit_3 -exec311_bit_2 -exec311_bit_1 -exec311_bit0 -exec311_bit1 -exec311_bit2 -exec311_bit3 -exec311_bit4 -exec311_bit5 -exec311_bit6 -exec311_bit7 -exec311_bit8 -exec311_bit9 -exec311_bit10 -exec311_bit11 -exec311_bit12 -exec312_bit_7 -exec312_bit_6 -exec312_bit_5 -exec312_bit_4 -exec312_bit_3 -exec312_bit_2 -exec312_bit_1 -exec312_bit0 -exec312_bit1 -exec312_bit2 -exec312_bit3 -exec312_bit4 -exec312_bit5 -exec312_bit6 -exec312_bit7 -exec312_bit8 -exec312_bit9 -exec312_bit10 -exec312_bit11 -exec312_bit12 -exec313_bit_7 -exec313_bit_6 -exec313_bit_5 -exec313_bit_4 -exec313_bit_3 -exec313_bit_2 -exec313_bit_1 -exec313_bit0 -exec313_bit1 -exec313_bit2 -exec313_bit3 -exec313_bit4 -exec313_bit5 -exec313_bit6 -exec313_bit7 -exec313_bit8 -exec313_bit9 -exec313_bit10 -exec313_bit11 -exec313_bit12 -exec400_bit_7 -exec400_bit_6 -exec400_bit_5 -exec400_bit_4 -exec400_bit_3 -exec400_bit_2 -exec400_bit_1 -exec400_bit0 -exec400_bit1 -exec400_bit2 -exec400_bit3 -exec400_bit4 -exec400_bit5 -exec400_bit6 -exec400_bit7 -exec400_bit8 -exec400_bit9 -exec400_bit10 -exec400_bit11 -exec400_bit12 -exec401_bit_7 -exec401_bit_6 -exec401_bit_5 -exec401_bit_4 -exec401_bit_3 -exec401_bit_2 -exec401_bit_1 -exec401_bit0 -exec401_bit1 -exec401_bit2 -exec401_bit3 -exec401_bit4 -exec401_bit5 -exec401_bit6 -exec401_bit7 -exec401_bit8 -exec401_bit9 -exec401_bit10 -exec401_bit11 -exec401_bit12 -exec402_bit_7 -exec402_bit_6 -exec402_bit_5 -exec402_bit_4 -exec402_bit_3 -exec402_bit_2 -exec402_bit_1 -exec402_bit0 -exec402_bit1 -exec402_bit2 -exec402_bit3 -exec402_bit4 -exec402_bit5 -exec402_bit6 -exec402_bit7 -exec402_bit8 -exec402_bit9 -exec402_bit10 -exec402_bit11 -exec402_bit12 -exec403_bit_7 -exec403_bit_6 -exec403_bit_5 -exec403_bit_4 -exec403_bit_3 -exec403_bit_2 -exec403_bit_1 -exec403_bit0 -exec403_bit1 -exec403_bit2 -exec403_bit3 -exec403_bit4 -exec403_bit5 -exec403_bit6 -exec403_bit7 -exec403_bit8 -exec403_bit9 -exec403_bit10 -exec403_bit11 -exec403_bit12 -exec410_bit_7 -exec410_bit_6 -exec410_bit_5 -exec410_bit_4 -exec410_bit_3 -exec410_bit_2 -exec410_bit_1 -exec410_bit0 -exec410_bit1 -exec410_bit2 -exec410_bit3 -exec410_bit4 -exec410_bit5 -exec410_bit6 -exec410_bit7 -exec410_bit8 -exec410_bit9 -exec410_bit10 -exec410_bit11 -exec410_bit12 -exec411_bit_7 -exec411_bit_6 -exec411_bit_5 -exec411_bit_4 -exec411_bit_3 -exec411_bit_2 -exec411_bit_1 -exec411_bit0 -exec411_bit1 -exec411_bit2 -exec411_bit3 -exec411_bit4 -exec411_bit5 -exec411_bit6 -exec411_bit7 -exec411_bit8 -exec411_bit9 -exec411_bit10 -exec411_bit11 -exec411_bit12 -exec412_bit_7 -exec412_bit_6 -exec412_bit_5 -exec412_bit_4 -exec412_bit_3 -exec412_bit_2 -exec412_bit_1 -exec412_bit0 -exec412_bit1 -exec412_bit2 -exec412_bit3 -exec412_bit4 -exec412_bit5 -exec412_bit6 -exec412_bit7 -exec412_bit8 -exec412_bit9 -exec412_bit10 -exec412_bit11 -exec412_bit12 -exec413_bit_7 -exec413_bit_6 -exec413_bit_5 -exec413_bit_4 -exec413_bit_3 -exec413_bit_2 -exec413_bit_1 -exec413_bit0 -exec413_bit1 -exec413_bit2 -exec413_bit3 -exec413_bit4 -exec413_bit5 -exec413_bit6 -exec413_bit7 -exec413_bit8 -exec413_bit9 -exec413_bit10 -exec413_bit11 -exec413_bit12 -rd10_bit_7 -rd10_bit_6 -rd10_bit_5 -rd10_bit_4 -rd10_bit_3 -rd10_bit_2 -rd10_bit_1 -rd10_bit0 -rd10_bit1 -rd10_bit2 -rd10_bit3 -rd10_bit4 -rd10_bit5 -rd10_bit6 -rd10_bit7 -rd10_bit8 -rd10_bit9 -rd10_bit10 -rd10_bit11 -rd10_bit12 -rd20_bit_7 -rd20_bit_6 -rd20_bit_5 -rd20_bit_4 -rd20_bit_3 -rd20_bit_2 -rd20_bit_1 -rd20_bit0 -rd20_bit1 -rd20_bit2 -rd20_bit3 -rd20_bit4 -rd20_bit5 -rd20_bit6 -rd20_bit7 -rd20_bit8 -rd20_bit9 -rd20_bit10 -rd20_bit11 -rd20_bit12 -rd30_bit_7 -rd30_bit_6 -rd30_bit_5 -rd30_bit_4 -rd30_bit_3 -rd30_bit_2 -rd30_bit_1 -rd30_bit0 -rd30_bit1 -rd30_bit2 -rd30_bit3 -rd30_bit4 -rd30_bit5 -rd30_bit6 -rd30_bit7 -rd30_bit8 -rd30_bit9 -rd30_bit10 -rd30_bit11 -rd30_bit12 -d1_bit_7 -d1_bit_6 -d1_bit_5 -d1_bit_4 -d1_bit_3 -d1_bit_2 -d1_bit_1 -d1_bit0 -d1_bit1 -d1_bit2 -d1_bit3 -d1_bit4 -d1_bit5 -d1_bit6 -d1_bit7 -d1_bit8 -d1_bit9 -d1_bit10 -d1_bit11 -d1_bit12 -d2_bit_7 -d2_bit_6 -d2_bit_5 -d2_bit_4 -d2_bit_3 -d2_bit_2 -d2_bit_1 -d2_bit0 -d2_bit1 -d2_bit2 -d2_bit3 -d2_bit4 -d2_bit5 -d2_bit6 -d2_bit7 -d2_bit8 -d2_bit9 -d2_bit10 -d2_bit11 -d2_bit12 -d3_bit_7 -d3_bit_6 -d3_bit_5 -d3_bit_4 -d3_bit_3 -d3_bit_2 -d3_bit_1 -d3_bit0 -d3_bit1 -d3_bit2 -d3_bit3 -d3_bit4 -d3_bit5 -d3_bit6 -d3_bit7 -d3_bit8 -d3_bit9 -d3_bit10 -d3_bit11 -d3_bit12 -wt00_bit_7 -wt00_bit_6 -wt00_bit_5 -wt00_bit_4 -wt00_bit_3 -wt00_bit_2 -wt00_bit_1 -wt00_bit0 -wt00_bit1 -wt00_bit2 -wt00_bit3 -wt00_bit4 -wt00_bit5 -wt00_bit6 -wt00_bit7 -wt00_bit8 -wt00_bit9 -wt00_bit10 -wt00_bit11 -wt00_bit12 -wt10_bit_7 -wt10_bit_6 -wt10_bit_5 -wt10_bit_4 -wt10_bit_3 -wt10_bit_2 -wt10_bit_1 -wt10_bit0 -wt10_bit1 -wt10_bit2 -wt10_bit3 -wt10_bit4 -wt10_bit5 -wt10_bit6 -wt10_bit7 -wt10_bit8 -wt10_bit9 -wt10_bit10 -wt10_bit11 -wt10_bit12 -wt20_bit_7 -wt20_bit_6 -wt20_bit_5 -wt20_bit_4 -wt20_bit_3 -wt20_bit_2 -wt20_bit_1 -wt20_bit0 -wt20_bit1 -wt20_bit2 -wt20_bit3 -wt20_bit4 -wt20_bit5 -wt20_bit6 -wt20_bit7 -wt20_bit8 -wt20_bit9 -wt20_bit10 -wt20_bit11 -wt20_bit12 -c0_bit_7 -c0_bit_6 -c0_bit_5 -c0_bit_4 -c0_bit_3 -c0_bit_2 -c0_bit_1 -c0_bit0 -c0_bit1 -c0_bit2 -c0_bit3 -c0_bit4 -c0_bit5 -c0_bit6 -c0_bit7 -c0_bit8 -c0_bit9 -c0_bit10 -c0_bit11 -c0_bit12 -c1_bit_7 -c1_bit_6 -c1_bit_5 -c1_bit_4 -c1_bit_3 -c1_bit_2 -c1_bit_1 -c1_bit0 -c1_bit1 -c1_bit2 -c1_bit3 -c1_bit4 -c1_bit5 -c1_bit6 -c1_bit7 -c1_bit8 -c1_bit9 -c1_bit10 -c1_bit11 -c1_bit12 -c2_bit_7 -c2_bit_6 -c2_bit_5 -c2_bit_4 -c2_bit_3 -c2_bit_2 -c2_bit_1 -c2_bit0 -c2_bit1 -c2_bit2 -c2_bit3 -c2_bit4 -c2_bit5 -c2_bit6 -c2_bit7 -c2_bit8 -c2_bit9 -c2_bit10 -c2_bit11 -c2_bit12 a0f0a1f1_bit0 -a0f0a1f1_bit1 -a0f0a1f1_bit2 -a0f0a1f1_bit3 -a0f0a1f1_bit4 -a0f0a1f1_bit5 -a0f0a1f1_bit6 -a0f0a1f1_bit7 -a0f0a1f1_bit8 -a0f0a1f1_bit9 -a0f0a1f1_bit10 -a0f0a1f1_bit11 -a0f0a1f1_bit12 -a0f0a2f2_bit0 -a0f0a2f2_bit1 -a0f0a2f2_bit2 -a0f0a2f2_bit3 -a0f0a2f2_bit4 -a0f0a2f2_bit5 -a0f0a2f2_bit6 -a0f0a2f2_bit7 -a0f0a2f2_bit8 -a0f0a2f2_bit9 -a0f0a2f2_bit10 -a0f0a2f2_bit11 -a0f0a2f2_bit12 -a0f0a3f3_bit0 -a0f0a3f3_bit1 -a0f0a3f3_bit2 -a0f0a3f3_bit3 -a0f0a3f3_bit4 -a0f0a3f3_bit5 -a0f0a3f3_bit6 -a0f0a3f3_bit7 -a0f0a3f3_bit8 -a0f0a3f3_bit9 -a0f0a3f3_bit10 -a0f0a3f3_bit11 -a0f0a3f3_bit12 a1f1a2f2_bit0 -a1f1a2f2_bit1 -a1f1a2f2_bit2 -a1f1a2f2_bit3 -a1f1a2f2_bit4 -a1f1a2f2_bit5 -a1f1a2f2_bit6 -a1f1a2f2_bit7 -a1f1a2f2_bit8 -a1f1a2f2_bit9 -a1f1a2f2_bit10 -a1f1a2f2_bit11 -a1f1a2f2_bit12 a1f1a3f3_bit0 -a1f1a3f3_bit1 -a1f1a3f3_bit2 -a1f1a3f3_bit3 -a1f1a3f3_bit4 -a1f1a3f3_bit5 -a1f1a3f3_bit6 -a1f1a3f3_bit7 -a1f1a3f3_bit8 -a1f1a3f3_bit9 -a1f1a3f3_bit10 -a1f1a3f3_bit11 -a1f1a3f3_bit12 a2f2a3f3_bit0 -a2f2a3f3_bit1 -a2f2a3f3_bit2 -a2f2a3f3_bit3 -a2f2a3f3_bit4 -a2f2a3f3_bit5 -a2f2a3f3_bit6 -a2f2a3f3_bit7 -a2f2a3f3_bit8 -a2f2a3f3_bit9 -a2f2a3f3_bit10 -a2f2a3f3_bit11 -a2f2a3f3_bit12 -ss010_bit_7 -ss010_bit_6 -ss010_bit_5 -ss010_bit_4 -ss010_bit_3 -ss010_bit_2 -ss010_bit_1 -ss010_bit0 -ss010_bit1 -ss010_bit2 -ss010_bit3 -ss010_bit4 -ss010_bit5 -ss010_bit6 -ss010_bit7 -ss010_bit8 -ss010_bit9 -ss010_bit10 -ss010_bit11 -ss010_bit12 -ss011_bit_7 -ss011_bit_6 -ss011_bit_5 -ss011_bit_4 -ss011_bit_3 -ss011_bit_2 -ss011_bit_1 -ss011_bit0 -ss011_bit1 -ss011_bit2 -ss011_bit3 -ss011_bit4 -ss011_bit5 -ss011_bit6 -ss011_bit7 -ss011_bit8 -ss011_bit9 -ss011_bit10 -ss011_bit11 -ss011_bit12 -ss012_bit_7 -ss012_bit_6 -ss012_bit_5 -ss012_bit_4 -ss012_bit_3 -ss012_bit_2 -ss012_bit_1 -ss012_bit0 -ss012_bit1 -ss012_bit2 -ss012_bit3 -ss012_bit4 -ss012_bit5 -ss012_bit6 -ss012_bit7 -ss012_bit8 -ss012_bit9 -ss012_bit10 -ss012_bit11 -ss012_bit12 -ss013_bit_7 -ss013_bit_6 -ss013_bit_5 -ss013_bit_4 -ss013_bit_3 -ss013_bit_2 -ss013_bit_1 -ss013_bit0 -ss013_bit1 -ss013_bit2 -ss013_bit3 -ss013_bit4 -ss013_bit5 -ss013_bit6 -ss013_bit7 -ss013_bit8 -ss013_bit9 -ss013_bit10 -ss013_bit11 -ss013_bit12 -ss100_bit_7 -ss100_bit_6 -ss100_bit_5 -ss100_bit_4 -ss100_bit_3 -ss100_bit_2 -ss100_bit_1 -ss100_bit0 -ss100_bit1 -ss100_bit2 -ss100_bit3 -ss100_bit4 -ss100_bit5 -ss100_bit6 -ss100_bit7 -ss100_bit8 -ss100_bit9 -ss100_bit10 -ss100_bit11 -ss100_bit12 -ss101_bit_7 -ss101_bit_6 -ss101_bit_5 -ss101_bit_4 -ss101_bit_3 -ss101_bit_2 -ss101_bit_1 -ss101_bit0 -ss101_bit1 -ss101_bit2 -ss101_bit3 -ss101_bit4 -ss101_bit5 -ss101_bit6 -ss101_bit7 -ss101_bit8 -ss101_bit9 -ss101_bit10 -ss101_bit11 -ss101_bit12 -ss102_bit_7 -ss102_bit_6 -ss102_bit_5 -ss102_bit_4 -ss102_bit_3 -ss102_bit_2 -ss102_bit_1 -ss102_bit0 -ss102_bit1 -ss102_bit2 -ss102_bit3 -ss102_bit4 -ss102_bit5 -ss102_bit6 -ss102_bit7 -ss102_bit8 -ss102_bit9 -ss102_bit10 -ss102_bit11 -ss102_bit12 -ss103_bit_7 -ss103_bit_6 -ss103_bit_5 -ss103_bit_4 -ss103_bit_3 -ss103_bit_2 -ss103_bit_1 -ss103_bit0 -ss103_bit1 -ss103_bit2 -ss103_bit3 -ss103_bit4 -ss103_bit5 -ss103_bit6 -ss103_bit7 -ss103_bit8 -ss103_bit9 -ss103_bit10 -ss103_bit11 -ss103_bit12 -ss020_bit_7 -ss020_bit_6 -ss020_bit_5 -ss020_bit_4 -ss020_bit_3 -ss020_bit_2 -ss020_bit_1 -ss020_bit0 -ss020_bit1 -ss020_bit2 -ss020_bit3 -ss020_bit4 -ss020_bit5 -ss020_bit6 -ss020_bit7 -ss020_bit8 -ss020_bit9 -ss020_bit10 -ss020_bit11 -ss020_bit12 -ss021_bit_7 -ss021_bit_6 -ss021_bit_5 -ss021_bit_4 -ss021_bit_3 -ss021_bit_2 -ss021_bit_1 -ss021_bit0 -ss021_bit1 -ss021_bit2 -ss021_bit3 -ss021_bit4 -ss021_bit5 -ss021_bit6 -ss021_bit7 -ss021_bit8 -ss021_bit9 -ss021_bit10 -ss021_bit11 -ss021_bit12 -ss022_bit_7 -ss022_bit_6 -ss022_bit_5 -ss022_bit_4 -ss022_bit_3 -ss022_bit_2 -ss022_bit_1 -ss022_bit0 -ss022_bit1 -ss022_bit2 -ss022_bit3 -ss022_bit4 -ss022_bit5 -ss022_bit6 -ss022_bit7 -ss022_bit8 -ss022_bit9 -ss022_bit10 -ss022_bit11 -ss022_bit12 -ss023_bit_7 -ss023_bit_6 -ss023_bit_5 -ss023_bit_4 -ss023_bit_3 -ss023_bit_2 -ss023_bit_1 -ss023_bit0 -ss023_bit1 -ss023_bit2 -ss023_bit3 -ss023_bit4 -ss023_bit5 -ss023_bit6 -ss023_bit7 -ss023_bit8 -ss023_bit9 -ss023_bit10 -ss023_bit11 -ss023_bit12 -ss200_bit_7 -ss200_bit_6 -ss200_bit_5 -ss200_bit_4 -ss200_bit_3 -ss200_bit_2 -ss200_bit_1 -ss200_bit0 -ss200_bit1 -ss200_bit2 -ss200_bit3 -ss200_bit4 -ss200_bit5 -ss200_bit6 -ss200_bit7 -ss200_bit8 -ss200_bit9 -ss200_bit10 -ss200_bit11 -ss200_bit12 -ss201_bit_7 -ss201_bit_6 -ss201_bit_5 -ss201_bit_4 -ss201_bit_3 -ss201_bit_2 -ss201_bit_1 -ss201_bit0 -ss201_bit1 -ss201_bit2 -ss201_bit3 -ss201_bit4 -ss201_bit5 -ss201_bit6 -ss201_bit7 -ss201_bit8 -ss201_bit9 -ss201_bit10 -ss201_bit11 -ss201_bit12 -ss202_bit_7 -ss202_bit_6 -ss202_bit_5 -ss202_bit_4 -ss202_bit_3 -ss202_bit_2 -ss202_bit_1 -ss202_bit0 -ss202_bit1 -ss202_bit2 -ss202_bit3 -ss202_bit4 -ss202_bit5 -ss202_bit6 -ss202_bit7 -ss202_bit8 -ss202_bit9 -ss202_bit10 -ss202_bit11 -ss202_bit12 -ss203_bit_7 -ss203_bit_6 -ss203_bit_5 -ss203_bit_4 -ss203_bit_3 -ss203_bit_2 -ss203_bit_1 -ss203_bit0 -ss203_bit1 -ss203_bit2 -ss203_bit3 -ss203_bit4 -ss203_bit5 -ss203_bit6 -ss203_bit7 -ss203_bit8 -ss203_bit9 -ss203_bit10 -ss203_bit11 -ss203_bit12 -ss030_bit_7 -ss030_bit_6 -ss030_bit_5 -ss030_bit_4 -ss030_bit_3 -ss030_bit_2 -ss030_bit_1 -ss030_bit0 -ss030_bit1 -ss030_bit2 -ss030_bit3 -ss030_bit4 -ss030_bit5 -ss030_bit6 -ss030_bit7 -ss030_bit8 -ss030_bit9 -ss030_bit10 -ss030_bit11 -ss030_bit12 -ss031_bit_7 -ss031_bit_6 -ss031_bit_5 -ss031_bit_4 -ss031_bit_3 -ss031_bit_2 -ss031_bit_1 -ss031_bit0 -ss031_bit1 -ss031_bit2 -ss031_bit3 -ss031_bit4 -ss031_bit5 -ss031_bit6 -ss031_bit7 -ss031_bit8 -ss031_bit9 -ss031_bit10 -ss031_bit11 -ss031_bit12 -ss032_bit_7 -ss032_bit_6 -ss032_bit_5 -ss032_bit_4 -ss032_bit_3 -ss032_bit_2 -ss032_bit_1 -ss032_bit0 -ss032_bit1 -ss032_bit2 -ss032_bit3 -ss032_bit4 -ss032_bit5 -ss032_bit6 -ss032_bit7 -ss032_bit8 -ss032_bit9 -ss032_bit10 -ss032_bit11 -ss032_bit12 -ss033_bit_7 -ss033_bit_6 -ss033_bit_5 -ss033_bit_4 -ss033_bit_3 -ss033_bit_2 -ss033_bit_1 -ss033_bit0 -ss033_bit1 -ss033_bit2 -ss033_bit3 -ss033_bit4 -ss033_bit5 -ss033_bit6 -ss033_bit7 -ss033_bit8 -ss033_bit9 -ss033_bit10 -ss033_bit11 -ss033_bit12 -ss300_bit_7 -ss300_bit_6 -ss300_bit_5 -ss300_bit_4 -ss300_bit_3 -ss300_bit_2 -ss300_bit_1 -ss300_bit0 -ss300_bit1 -ss300_bit2 -ss300_bit3 -ss300_bit4 -ss300_bit5 -ss300_bit6 -ss300_bit7 -ss300_bit8 -ss300_bit9 -ss300_bit10 -ss300_bit11 -ss300_bit12 -ss301_bit_7 -ss301_bit_6 -ss301_bit_5 -ss301_bit_4 -ss301_bit_3 -ss301_bit_2 -ss301_bit_1 -ss301_bit0 -ss301_bit1 -ss301_bit2 -ss301_bit3 -ss301_bit4 -ss301_bit5 -ss301_bit6 -ss301_bit7 -ss301_bit8 -ss301_bit9 -ss301_bit10 -ss301_bit11 -ss301_bit12 -ss302_bit_7 -ss302_bit_6 -ss302_bit_5 -ss302_bit_4 -ss302_bit_3 -ss302_bit_2 -ss302_bit_1 -ss302_bit0 -ss302_bit1 -ss302_bit2 -ss302_bit3 -ss302_bit4 -ss302_bit5 -ss302_bit6 -ss302_bit7 -ss302_bit8 -ss302_bit9 -ss302_bit10 -ss302_bit11 -ss302_bit12 -ss303_bit_7 -ss303_bit_6 -ss303_bit_5 -ss303_bit_4 -ss303_bit_3 -ss303_bit_2 -ss303_bit_1 -ss303_bit0 -ss303_bit1 -ss303_bit2 -ss303_bit3 -ss303_bit4 -ss303_bit5 -ss303_bit6 -ss303_bit7 -ss303_bit8 -ss303_bit9 -ss303_bit10 -ss303_bit11 -ss303_bit12 -ss040_bit_7 -ss040_bit_6 -ss040_bit_5 -ss040_bit_4 -ss040_bit_3 -ss040_bit_2 -ss040_bit_1 -ss040_bit0 -ss040_bit1 -ss040_bit2 -ss040_bit3 -ss040_bit4 -ss040_bit5 -ss040_bit6 -ss040_bit7 -ss040_bit8 -ss040_bit9 -ss040_bit10 -ss040_bit11 -ss040_bit12 -ss041_bit_7 -ss041_bit_6 -ss041_bit_5 -ss041_bit_4 -ss041_bit_3 -ss041_bit_2 -ss041_bit_1 -ss041_bit0 -ss041_bit1 -ss041_bit2 -ss041_bit3 -ss041_bit4 -ss041_bit5 -ss041_bit6 -ss041_bit7 -ss041_bit8 -ss041_bit9 -ss041_bit10 -ss041_bit11 -ss041_bit12 -ss042_bit_7 -ss042_bit_6 -ss042_bit_5 -ss042_bit_4 -ss042_bit_3 -ss042_bit_2 -ss042_bit_1 -ss042_bit0 -ss042_bit1 -ss042_bit2 -ss042_bit3 -ss042_bit4 -ss042_bit5 -ss042_bit6 -ss042_bit7 -ss042_bit8 -ss042_bit9 -ss042_bit10 -ss042_bit11 -ss042_bit12 -ss043_bit_7 -ss043_bit_6 -ss043_bit_5 -ss043_bit_4 -ss043_bit_3 -ss043_bit_2 -ss043_bit_1 -ss043_bit0 -ss043_bit1 -ss043_bit2 -ss043_bit3 -ss043_bit4 -ss043_bit5 -ss043_bit6 -ss043_bit7 -ss043_bit8 -ss043_bit9 -ss043_bit10 -ss043_bit11 -ss043_bit12 -ss400_bit_7 -ss400_bit_6 -ss400_bit_5 -ss400_bit_4 -ss400_bit_3 -ss400_bit_2 -ss400_bit_1 -ss400_bit0 -ss400_bit1 -ss400_bit2 -ss400_bit3 -ss400_bit4 -ss400_bit5 -ss400_bit6 -ss400_bit7 -ss400_bit8 -ss400_bit9 -ss400_bit10 -ss400_bit11 -ss400_bit12 -ss401_bit_7 -ss401_bit_6 -ss401_bit_5 -ss401_bit_4 -ss401_bit_3 -ss401_bit_2 -ss401_bit_1 -ss401_bit0 -ss401_bit1 -ss401_bit2 -ss401_bit3 -ss401_bit4 -ss401_bit5 -ss401_bit6 -ss401_bit7 -ss401_bit8 -ss401_bit9 -ss401_bit10 -ss401_bit11 -ss401_bit12 -ss402_bit_7 -ss402_bit_6 -ss402_bit_5 -ss402_bit_4 -ss402_bit_3 -ss402_bit_2 -ss402_bit_1 -ss402_bit0 -ss402_bit1 -ss402_bit2 -ss402_bit3 -ss402_bit4 -ss402_bit5 -ss402_bit6 -ss402_bit7 -ss402_bit8 -ss402_bit9 -ss402_bit10 -ss402_bit11 -ss402_bit12 -ss403_bit_7 -ss403_bit_6 -ss403_bit_5 -ss403_bit_4 -ss403_bit_3 -ss403_bit_2 -ss403_bit_1 -ss403_bit0 -ss403_bit1 -ss403_bit2 -ss403_bit3 -ss403_bit4 -ss403_bit5 -ss403_bit6 -ss403_bit7 -ss403_bit8 -ss403_bit9 -ss403_bit10 -ss403_bit11 -ss403_bit12 -ss120_bit_7 -ss120_bit_6 -ss120_bit_5 -ss120_bit_4 -ss120_bit_3 -ss120_bit_2 -ss120_bit_1 -ss120_bit0 -ss120_bit1 -ss120_bit2 -ss120_bit3 -ss120_bit4 -ss120_bit5 -ss120_bit6 -ss120_bit7 -ss120_bit8 -ss120_bit9 -ss120_bit10 -ss120_bit11 -ss120_bit12 -ss121_bit_7 -ss121_bit_6 -ss121_bit_5 -ss121_bit_4 -ss121_bit_3 -ss121_bit_2 -ss121_bit_1 -ss121_bit0 -ss121_bit1 -ss121_bit2 -ss121_bit3 -ss121_bit4 -ss121_bit5 -ss121_bit6 -ss121_bit7 -ss121_bit8 -ss121_bit9 -ss121_bit10 -ss121_bit11 -ss121_bit12 -ss122_bit_7 -ss122_bit_6 -ss122_bit_5 -ss122_bit_4 -ss122_bit_3 -ss122_bit_2 -ss122_bit_1 ss122_bit0 -ss122_bit1 -ss122_bit2 -ss122_bit3 -ss122_bit4 -ss122_bit5 -ss122_bit6 -ss122_bit7 -ss122_bit8 -ss122_bit9 -ss122_bit10 -ss122_bit11 -ss122_bit12 -ss123_bit_7 -ss123_bit_6 -ss123_bit_5 -ss123_bit_4 -ss123_bit_3 -ss123_bit_2 -ss123_bit_1 -ss123_bit0 -ss123_bit1 -ss123_bit2 -ss123_bit3 -ss123_bit4 -ss123_bit5 -ss123_bit6 -ss123_bit7 -ss123_bit8 -ss123_bit9 -ss123_bit10 -ss123_bit11 -ss123_bit12 -ss210_bit_7 -ss210_bit_6 -ss210_bit_5 -ss210_bit_4 -ss210_bit_3 -ss210_bit_2 -ss210_bit_1 -ss210_bit0 -ss210_bit1 -ss210_bit2 -ss210_bit3 -ss210_bit4 -ss210_bit5 -ss210_bit6 -ss210_bit7 -ss210_bit8 -ss210_bit9 -ss210_bit10 -ss210_bit11 -ss210_bit12 -ss211_bit_7 -ss211_bit_6 -ss211_bit_5 -ss211_bit_4 -ss211_bit_3 -ss211_bit_2 -ss211_bit_1 -ss211_bit0 -ss211_bit1 -ss211_bit2 -ss211_bit3 -ss211_bit4 -ss211_bit5 -ss211_bit6 -ss211_bit7 -ss211_bit8 -ss211_bit9 -ss211_bit10 -ss211_bit11 -ss211_bit12 -ss212_bit_7 -ss212_bit_6 -ss212_bit_5 -ss212_bit_4 -ss212_bit_3 -ss212_bit_2 -ss212_bit_1 ss212_bit0 -ss212_bit1 -ss212_bit2 -ss212_bit3 -ss212_bit4 -ss212_bit5 -ss212_bit6 -ss212_bit7 -ss212_bit8 -ss212_bit9 -ss212_bit10 -ss212_bit11 -ss212_bit12 -ss213_bit_7 -ss213_bit_6 -ss213_bit_5 -ss213_bit_4 -ss213_bit_3 -ss213_bit_2 -ss213_bit_1 -ss213_bit0 -ss213_bit1 -ss213_bit2 -ss213_bit3 -ss213_bit4 -ss213_bit5 -ss213_bit6 -ss213_bit7 -ss213_bit8 -ss213_bit9 -ss213_bit10 -ss213_bit11 -ss213_bit12 -ss130_bit_7 -ss130_bit_6 -ss130_bit_5 -ss130_bit_4 -ss130_bit_3 -ss130_bit_2 -ss130_bit_1 -ss130_bit0 -ss130_bit1 -ss130_bit2 -ss130_bit3 -ss130_bit4 -ss130_bit5 -ss130_bit6 -ss130_bit7 -ss130_bit8 -ss130_bit9 -ss130_bit10 -ss130_bit11 -ss130_bit12 -ss131_bit_7 -ss131_bit_6 -ss131_bit_5 -ss131_bit_4 -ss131_bit_3 -ss131_bit_2 -ss131_bit_1 -ss131_bit0 -ss131_bit1 -ss131_bit2 -ss131_bit3 -ss131_bit4 -ss131_bit5 -ss131_bit6 -ss131_bit7 -ss131_bit8 -ss131_bit9 -ss131_bit10 -ss131_bit11 -ss131_bit12 -ss132_bit_7 -ss132_bit_6 -ss132_bit_5 -ss132_bit_4 -ss132_bit_3 -ss132_bit_2 -ss132_bit_1 -ss132_bit0 -ss132_bit1 -ss132_bit2 -ss132_bit3 -ss132_bit4 -ss132_bit5 -ss132_bit6 -ss132_bit7 -ss132_bit8 -ss132_bit9 -ss132_bit10 -ss132_bit11 -ss132_bit12 -ss133_bit_7 -ss133_bit_6 -ss133_bit_5 -ss133_bit_4 -ss133_bit_3 -ss133_bit_2 -ss133_bit_1 -ss133_bit0 -ss133_bit1 -ss133_bit2 -ss133_bit3 -ss133_bit4 -ss133_bit5 -ss133_bit6 -ss133_bit7 -ss133_bit8 -ss133_bit9 -ss133_bit10 -ss133_bit11 -ss133_bit12 -ss310_bit_7 -ss310_bit_6 -ss310_bit_5 -ss310_bit_4 -ss310_bit_3 -ss310_bit_2 -ss310_bit_1 -ss310_bit0 -ss310_bit1 -ss310_bit2 -ss310_bit3 -ss310_bit4 -ss310_bit5 -ss310_bit6 -ss310_bit7 -ss310_bit8 -ss310_bit9 -ss310_bit10 -ss310_bit11 -ss310_bit12 -ss311_bit_7 -ss311_bit_6 -ss311_bit_5 -ss311_bit_4 -ss311_bit_3 -ss311_bit_2 -ss311_bit_1 -ss311_bit0 -ss311_bit1 -ss311_bit2 -ss311_bit3 -ss311_bit4 -ss311_bit5 -ss311_bit6 -ss311_bit7 -ss311_bit8 -ss311_bit9 -ss311_bit10 -ss311_bit11 -ss311_bit12 -ss312_bit_7 -ss312_bit_6 -ss312_bit_5 -ss312_bit_4 -ss312_bit_3 -ss312_bit_2 -ss312_bit_1 -ss312_bit0 -ss312_bit1 -ss312_bit2 -ss312_bit3 -ss312_bit4 -ss312_bit5 -ss312_bit6 -ss312_bit7 -ss312_bit8 -ss312_bit9 -ss312_bit10 -ss312_bit11 -ss312_bit12 -ss313_bit_7 -ss313_bit_6 -ss313_bit_5 -ss313_bit_4 -ss313_bit_3 -ss313_bit_2 -ss313_bit_1 -ss313_bit0 -ss313_bit1 -ss313_bit2 -ss313_bit3 -ss313_bit4 -ss313_bit5 -ss313_bit6 -ss313_bit7 -ss313_bit8 -ss313_bit9 -ss313_bit10 -ss313_bit11 -ss313_bit12 -ss140_bit_7 -ss140_bit_6 -ss140_bit_5 -ss140_bit_4 -ss140_bit_3 -ss140_bit_2 -ss140_bit_1 -ss140_bit0 -ss140_bit1 -ss140_bit2 -ss140_bit3 -ss140_bit4 -ss140_bit5 -ss140_bit6 -ss140_bit7 -ss140_bit8 -ss140_bit9 -ss140_bit10 -ss140_bit11 -ss140_bit12 -ss141_bit_7 -ss141_bit_6 -ss141_bit_5 -ss141_bit_4 -ss141_bit_3 -ss141_bit_2 -ss141_bit_1 -ss141_bit0 -ss141_bit1 -ss141_bit2 -ss141_bit3 -ss141_bit4 -ss141_bit5 -ss141_bit6 -ss141_bit7 -ss141_bit8 -ss141_bit9 -ss141_bit10 -ss141_bit11 -ss141_bit12 -ss142_bit_7 -ss142_bit_6 -ss142_bit_5 -ss142_bit_4 -ss142_bit_3 -ss142_bit_2 -ss142_bit_1 ss142_bit0 -ss142_bit1 -ss142_bit2 -ss142_bit3 -ss142_bit4 -ss142_bit5 -ss142_bit6 -ss142_bit7 -ss142_bit8 -ss142_bit9 -ss142_bit10 -ss142_bit11 -ss142_bit12 -ss143_bit_7 -ss143_bit_6 -ss143_bit_5 -ss143_bit_4 -ss143_bit_3 -ss143_bit_2 -ss143_bit_1 -ss143_bit0 -ss143_bit1 -ss143_bit2 -ss143_bit3 -ss143_bit4 -ss143_bit5 -ss143_bit6 -ss143_bit7 -ss143_bit8 -ss143_bit9 -ss143_bit10 -ss143_bit11 -ss143_bit12 -ss410_bit_7 -ss410_bit_6 -ss410_bit_5 -ss410_bit_4 -ss410_bit_3 -ss410_bit_2 -ss410_bit_1 -ss410_bit0 -ss410_bit1 -ss410_bit2 -ss410_bit3 -ss410_bit4 -ss410_bit5 -ss410_bit6 -ss410_bit7 -ss410_bit8 -ss410_bit9 -ss410_bit10 -ss410_bit11 -ss410_bit12 -ss411_bit_7 -ss411_bit_6 -ss411_bit_5 -ss411_bit_4 -ss411_bit_3 -ss411_bit_2 -ss411_bit_1 -ss411_bit0 -ss411_bit1 -ss411_bit2 -ss411_bit3 -ss411_bit4 -ss411_bit5 -ss411_bit6 -ss411_bit7 -ss411_bit8 -ss411_bit9 -ss411_bit10 -ss411_bit11 -ss411_bit12 -ss412_bit_7 -ss412_bit_6 -ss412_bit_5 -ss412_bit_4 -ss412_bit_3 -ss412_bit_2 -ss412_bit_1 ss412_bit0 -ss412_bit1 -ss412_bit2 -ss412_bit3 -ss412_bit4 -ss412_bit5 -ss412_bit6 -ss412_bit7 -ss412_bit8 -ss412_bit9 -ss412_bit10 -ss412_bit11 -ss412_bit12 -ss413_bit_7 -ss413_bit_6 -ss413_bit_5 -ss413_bit_4 -ss413_bit_3 -ss413_bit_2 -ss413_bit_1 -ss413_bit0 -ss413_bit1 -ss413_bit2 -ss413_bit3 -ss413_bit4 -ss413_bit5 -ss413_bit6 -ss413_bit7 -ss413_bit8 -ss413_bit9 -ss413_bit10 -ss413_bit11 -ss413_bit12 -ss230_bit_7 -ss230_bit_6 -ss230_bit_5 -ss230_bit_4 -ss230_bit_3 -ss230_bit_2 -ss230_bit_1 -ss230_bit0 -ss230_bit1 -ss230_bit2 -ss230_bit3 -ss230_bit4 -ss230_bit5 -ss230_bit6 -ss230_bit7 -ss230_bit8 -ss230_bit9 -ss230_bit10 -ss230_bit11 -ss230_bit12 -ss231_bit_7 -ss231_bit_6 -ss231_bit_5 -ss231_bit_4 -ss231_bit_3 -ss231_bit_2 -ss231_bit_1 -ss231_bit0 -ss231_bit1 -ss231_bit2 -ss231_bit3 -ss231_bit4 -ss231_bit5 -ss231_bit6 -ss231_bit7 -ss231_bit8 -ss231_bit9 -ss231_bit10 -ss231_bit11 -ss231_bit12 -ss232_bit_7 -ss232_bit_6 -ss232_bit_5 -ss232_bit_4 -ss232_bit_3 -ss232_bit_2 -ss232_bit_1 -ss232_bit0 -ss232_bit1 -ss232_bit2 -ss232_bit3 -ss232_bit4 -ss232_bit5 -ss232_bit6 -ss232_bit7 -ss232_bit8 -ss232_bit9 -ss232_bit10 -ss232_bit11 -ss232_bit12 -ss233_bit_7 -ss233_bit_6 -ss233_bit_5 -ss233_bit_4 -ss233_bit_3 -ss233_bit_2 -ss233_bit_1 -ss233_bit0 -ss233_bit1 -ss233_bit2 -ss233_bit3 -ss233_bit4 -ss233_bit5 -ss233_bit6 -ss233_bit7 -ss233_bit8 -ss233_bit9 -ss233_bit10 -ss233_bit11 -ss233_bit12 -ss320_bit_7 -ss320_bit_6 -ss320_bit_5 -ss320_bit_4 -ss320_bit_3 -ss320_bit_2 -ss320_bit_1 -ss320_bit0 -ss320_bit1 -ss320_bit2 -ss320_bit3 -ss320_bit4 -ss320_bit5 -ss320_bit6 -ss320_bit7 -ss320_bit8 -ss320_bit9 -ss320_bit10 -ss320_bit11 -ss320_bit12 -ss321_bit_7 -ss321_bit_6 -ss321_bit_5 -ss321_bit_4 -ss321_bit_3 -ss321_bit_2 -ss321_bit_1 -ss321_bit0 -ss321_bit1 -ss321_bit2 -ss321_bit3 -ss321_bit4 -ss321_bit5 -ss321_bit6 -ss321_bit7 -ss321_bit8 -ss321_bit9 -ss321_bit10 -ss321_bit11 -ss321_bit12 -ss322_bit_7 -ss322_bit_6 -ss322_bit_5 -ss322_bit_4 -ss322_bit_3 -ss322_bit_2 -ss322_bit_1 -ss322_bit0 -ss322_bit1 -ss322_bit2 -ss322_bit3 -ss322_bit4 -ss322_bit5 -ss322_bit6 -ss322_bit7 -ss322_bit8 -ss322_bit9 -ss322_bit10 -ss322_bit11 -ss322_bit12 -ss323_bit_7 -ss323_bit_6 -ss323_bit_5 -ss323_bit_4 -ss323_bit_3 -ss323_bit_2 -ss323_bit_1 -ss323_bit0 -ss323_bit1 -ss323_bit2 -ss323_bit3 -ss323_bit4 -ss323_bit5 -ss323_bit6 -ss323_bit7 -ss323_bit8 -ss323_bit9 -ss323_bit10 -ss323_bit11 -ss323_bit12 -ss240_bit_7 -ss240_bit_6 -ss240_bit_5 -ss240_bit_4 -ss240_bit_3 -ss240_bit_2 -ss240_bit_1 -ss240_bit0 -ss240_bit1 -ss240_bit2 -ss240_bit3 -ss240_bit4 -ss240_bit5 -ss240_bit6 -ss240_bit7 -ss240_bit8 -ss240_bit9 -ss240_bit10 -ss240_bit11 -ss240_bit12 -ss241_bit_7 -ss241_bit_6 -ss241_bit_5 -ss241_bit_4 -ss241_bit_3 -ss241_bit_2 -ss241_bit_1 -ss241_bit0 -ss241_bit1 -ss241_bit2 -ss241_bit3 -ss241_bit4 -ss241_bit5 -ss241_bit6 -ss241_bit7 -ss241_bit8 -ss241_bit9 -ss241_bit10 -ss241_bit11 -ss241_bit12 -ss242_bit_7 -ss242_bit_6 -ss242_bit_5 -ss242_bit_4 -ss242_bit_3 -ss242_bit_2 -ss242_bit_1 ss242_bit0 -ss242_bit1 -ss242_bit2 -ss242_bit3 -ss242_bit4 -ss242_bit5 -ss242_bit6 -ss242_bit7 -ss242_bit8 -ss242_bit9 -ss242_bit10 -ss242_bit11 -ss242_bit12 -ss243_bit_7 -ss243_bit_6 -ss243_bit_5 -ss243_bit_4 -ss243_bit_3 -ss243_bit_2 -ss243_bit_1 -ss243_bit0 -ss243_bit1 -ss243_bit2 -ss243_bit3 -ss243_bit4 -ss243_bit5 -ss243_bit6 -ss243_bit7 -ss243_bit8 -ss243_bit9 -ss243_bit10 -ss243_bit11 -ss243_bit12 -ss420_bit_7 -ss420_bit_6 -ss420_bit_5 -ss420_bit_4 -ss420_bit_3 -ss420_bit_2 -ss420_bit_1 -ss420_bit0 -ss420_bit1 -ss420_bit2 -ss420_bit3 -ss420_bit4 -ss420_bit5 -ss420_bit6 -ss420_bit7 -ss420_bit8 -ss420_bit9 -ss420_bit10 -ss420_bit11 -ss420_bit12 -ss421_bit_7 -ss421_bit_6 -ss421_bit_5 -ss421_bit_4 -ss421_bit_3 -ss421_bit_2 -ss421_bit_1 -ss421_bit0 -ss421_bit1 -ss421_bit2 -ss421_bit3 -ss421_bit4 -ss421_bit5 -ss421_bit6 -ss421_bit7 -ss421_bit8 -ss421_bit9 -ss421_bit10 -ss421_bit11 -ss421_bit12 -ss422_bit_7 -ss422_bit_6 -ss422_bit_5 -ss422_bit_4 -ss422_bit_3 -ss422_bit_2 -ss422_bit_1 ss422_bit0 -ss422_bit1 -ss422_bit2 -ss422_bit3 -ss422_bit4 -ss422_bit5 -ss422_bit6 -ss422_bit7 -ss422_bit8 -ss422_bit9 -ss422_bit10 -ss422_bit11 -ss422_bit12 -ss423_bit_7 -ss423_bit_6 -ss423_bit_5 -ss423_bit_4 -ss423_bit_3 -ss423_bit_2 -ss423_bit_1 -ss423_bit0 -ss423_bit1 -ss423_bit2 -ss423_bit3 -ss423_bit4 -ss423_bit5 -ss423_bit6 -ss423_bit7 -ss423_bit8 -ss423_bit9 -ss423_bit10 -ss423_bit11 -ss423_bit12 -ss340_bit_7 -ss340_bit_6 -ss340_bit_5 -ss340_bit_4 -ss340_bit_3 -ss340_bit_2 -ss340_bit_1 -ss340_bit0 -ss340_bit1 -ss340_bit2 -ss340_bit3 -ss340_bit4 -ss340_bit5 -ss340_bit6 -ss340_bit7 -ss340_bit8 -ss340_bit9 -ss340_bit10 -ss340_bit11 -ss340_bit12 -ss341_bit_7 -ss341_bit_6 -ss341_bit_5 -ss341_bit_4 -ss341_bit_3 -ss341_bit_2 -ss341_bit_1 -ss341_bit0 -ss341_bit1 -ss341_bit2 -ss341_bit3 -ss341_bit4 -ss341_bit5 -ss341_bit6 -ss341_bit7 -ss341_bit8 -ss341_bit9 -ss341_bit10 -ss341_bit11 -ss341_bit12 -ss342_bit_7 -ss342_bit_6 -ss342_bit_5 -ss342_bit_4 -ss342_bit_3 -ss342_bit_2 -ss342_bit_1 -ss342_bit0 -ss342_bit1 -ss342_bit2 -ss342_bit3 -ss342_bit4 -ss342_bit5 -ss342_bit6 -ss342_bit7 -ss342_bit8 -ss342_bit9 -ss342_bit10 -ss342_bit11 -ss342_bit12 -ss343_bit_7 -ss343_bit_6 -ss343_bit_5 -ss343_bit_4 -ss343_bit_3 -ss343_bit_2 -ss343_bit_1 -ss343_bit0 -ss343_bit1 -ss343_bit2 -ss343_bit3 -ss343_bit4 -ss343_bit5 -ss343_bit6 -ss343_bit7 -ss343_bit8 -ss343_bit9 -ss343_bit10 -ss343_bit11 -ss343_bit12 -ss430_bit_7 -ss430_bit_6 -ss430_bit_5 -ss430_bit_4 -ss430_bit_3 -ss430_bit_2 -ss430_bit_1 -ss430_bit0 -ss430_bit1 -ss430_bit2 -ss430_bit3 -ss430_bit4 -ss430_bit5 -ss430_bit6 -ss430_bit7 -ss430_bit8 -ss430_bit9 -ss430_bit10 -ss430_bit11 -ss430_bit12 -ss431_bit_7 -ss431_bit_6 -ss431_bit_5 -ss431_bit_4 -ss431_bit_3 -ss431_bit_2 -ss431_bit_1 -ss431_bit0 -ss431_bit1 -ss431_bit2 -ss431_bit3 -ss431_bit4 -ss431_bit5 -ss431_bit6 -ss431_bit7 -ss431_bit8 -ss431_bit9 -ss431_bit10 -ss431_bit11 -ss431_bit12 -ss432_bit_7 -ss432_bit_6 -ss432_bit_5 -ss432_bit_4 -ss432_bit_3 -ss432_bit_2 -ss432_bit_1 -ss432_bit0 -ss432_bit1 -ss432_bit2 -ss432_bit3 -ss432_bit4 -ss432_bit5 -ss432_bit6 -ss432_bit7 -ss432_bit8 -ss432_bit9 -ss432_bit10 -ss432_bit11 -ss432_bit12 -ss433_bit_7 -ss433_bit_6 -ss433_bit_5 -ss433_bit_4 -ss433_bit_3 -ss433_bit_2 -ss433_bit_1 -ss433_bit0 -ss433_bit1 -ss433_bit2 -ss433_bit3 -ss433_bit4 -ss433_bit5 -ss433_bit6 -ss433_bit7 -ss433_bit8 -ss433_bit9 -ss433_bit10 -ss433_bit11 -ss433_bit12 -sp010_bit_7 -sp010_bit_6 -sp010_bit_5 -sp010_bit_4 -sp010_bit_3 -sp010_bit_2 -sp010_bit_1 sp010_bit0 -sp010_bit1 -sp010_bit2 -sp010_bit3 -sp010_bit4 -sp010_bit5 -sp010_bit6 -sp010_bit7 -sp010_bit8 -sp010_bit9 -sp010_bit10 -sp010_bit11 -sp010_bit12 -sp011_bit_7 -sp011_bit_6 -sp011_bit_5 -sp011_bit_4 -sp011_bit_3 -sp011_bit_2 -sp011_bit_1 -sp011_bit0 -sp011_bit1 -sp011_bit2 -sp011_bit3 -sp011_bit4 -sp011_bit5 -sp011_bit6 -sp011_bit7 -sp011_bit8 -sp011_bit9 -sp011_bit10 -sp011_bit11 -sp011_bit12 f0a1a2f2_bit0 -f0a1a2f2_bit1 -f0a1a2f2_bit2 -f0a1a2f2_bit3 -f0a1a2f2_bit4 -f0a1a2f2_bit5 -f0a1a2f2_bit6 -f0a1a2f2_bit7 -f0a1a2f2_bit8 -f0a1a2f2_bit9 -f0a1a2f2_bit10 -f0a1a2f2_bit11 -f0a1a2f2_bit12 f0a1a3f3_bit0 -f0a1a3f3_bit1 -f0a1a3f3_bit2 -f0a1a3f3_bit3 -f0a1a3f3_bit4 -f0a1a3f3_bit5 -f0a1a3f3_bit6 -f0a1a3f3_bit7 -f0a1a3f3_bit8 -f0a1a3f3_bit9 -f0a1a3f3_bit10 -f0a1a3f3_bit11 -f0a1a3f3_bit12 f0a1a4f4_bit0 -f0a1a4f4_bit1 -f0a1a4f4_bit2 -f0a1a4f4_bit3 -f0a1a4f4_bit4 -f0a1a4f4_bit5 -f0a1a4f4_bit6 -f0a1a4f4_bit7 -f0a1a4f4_bit8 -f0a1a4f4_bit9 -f0a1a4f4_bit10 -f0a1a4f4_bit11 -f0a1a4f4_bit12 -sp100_bit_7 -sp100_bit_6 -sp100_bit_5 -sp100_bit_4 -sp100_bit_3 -sp100_bit_2 -sp100_bit_1 sp100_bit0 -sp100_bit1 -sp100_bit2 -sp100_bit3 -sp100_bit4 -sp100_bit5 -sp100_bit6 -sp100_bit7 -sp100_bit8 -sp100_bit9 -sp100_bit10 -sp100_bit11 -sp100_bit12 -sp101_bit_7 -sp101_bit_6 -sp101_bit_5 -sp101_bit_4 -sp101_bit_3 -sp101_bit_2 -sp101_bit_1 -sp101_bit0 -sp101_bit1 -sp101_bit2 -sp101_bit3 -sp101_bit4 -sp101_bit5 -sp101_bit6 -sp101_bit7 -sp101_bit8 -sp101_bit9 -sp101_bit10 -sp101_bit11 -sp101_bit12 -f1a0a2f2_bit0 -f1a0a2f2_bit1 -f1a0a2f2_bit2 -f1a0a2f2_bit3 -f1a0a2f2_bit4 -f1a0a2f2_bit5 -f1a0a2f2_bit6 -f1a0a2f2_bit7 -f1a0a2f2_bit8 -f1a0a2f2_bit9 -f1a0a2f2_bit10 -f1a0a2f2_bit11 -f1a0a2f2_bit12 -f1a0a3f3_bit0 -f1a0a3f3_bit1 -f1a0a3f3_bit2 -f1a0a3f3_bit3 -f1a0a3f3_bit4 -f1a0a3f3_bit5 -f1a0a3f3_bit6 -f1a0a3f3_bit7 -f1a0a3f3_bit8 -f1a0a3f3_bit9 -f1a0a3f3_bit10 -f1a0a3f3_bit11 -f1a0a3f3_bit12 -f1a0a4f4_bit0 -f1a0a4f4_bit1 -f1a0a4f4_bit2 -f1a0a4f4_bit3 -f1a0a4f4_bit4 -f1a0a4f4_bit5 -f1a0a4f4_bit6 -f1a0a4f4_bit7 -f1a0a4f4_bit8 -f1a0a4f4_bit9 -f1a0a4f4_bit10 -f1a0a4f4_bit11 -f1a0a4f4_bit12 -sp020_bit_7 -sp020_bit_6 -sp020_bit_5 -sp020_bit_4 -sp020_bit_3 -sp020_bit_2 -sp020_bit_1 -sp020_bit0 -sp020_bit1 -sp020_bit2 -sp020_bit3 -sp020_bit4 -sp020_bit5 -sp020_bit6 -sp020_bit7 -sp020_bit8 -sp020_bit9 -sp020_bit10 -sp020_bit11 -sp020_bit12 -sp021_bit_7 -sp021_bit_6 -sp021_bit_5 -sp021_bit_4 -sp021_bit_3 -sp021_bit_2 -sp021_bit_1 -sp021_bit0 -sp021_bit1 -sp021_bit2 -sp021_bit3 -sp021_bit4 -sp021_bit5 -sp021_bit6 -sp021_bit7 -sp021_bit8 -sp021_bit9 -sp021_bit10 -sp021_bit11 -sp021_bit12 f0a2a1f1_bit0 -f0a2a1f1_bit1 -f0a2a1f1_bit2 -f0a2a1f1_bit3 -f0a2a1f1_bit4 -f0a2a1f1_bit5 -f0a2a1f1_bit6 -f0a2a1f1_bit7 -f0a2a1f1_bit8 -f0a2a1f1_bit9 -f0a2a1f1_bit10 -f0a2a1f1_bit11 -f0a2a1f1_bit12 -f0a2a3f3_bit0 -f0a2a3f3_bit1 -f0a2a3f3_bit2 -f0a2a3f3_bit3 -f0a2a3f3_bit4 -f0a2a3f3_bit5 -f0a2a3f3_bit6 -f0a2a3f3_bit7 -f0a2a3f3_bit8 -f0a2a3f3_bit9 -f0a2a3f3_bit10 -f0a2a3f3_bit11 -f0a2a3f3_bit12 -f0a2a4f4_bit0 -f0a2a4f4_bit1 -f0a2a4f4_bit2 -f0a2a4f4_bit3 -f0a2a4f4_bit4 -f0a2a4f4_bit5 -f0a2a4f4_bit6 -f0a2a4f4_bit7 -f0a2a4f4_bit8 -f0a2a4f4_bit9 -f0a2a4f4_bit10 -f0a2a4f4_bit11 -f0a2a4f4_bit12 -sp200_bit_7 -sp200_bit_6 -sp200_bit_5 -sp200_bit_4 -sp200_bit_3 -sp200_bit_2 -sp200_bit_1 -sp200_bit0 -sp200_bit1 -sp200_bit2 -sp200_bit3 -sp200_bit4 -sp200_bit5 -sp200_bit6 -sp200_bit7 -sp200_bit8 -sp200_bit9 -sp200_bit10 -sp200_bit11 -sp200_bit12 -sp201_bit_7 -sp201_bit_6 -sp201_bit_5 -sp201_bit_4 -sp201_bit_3 -sp201_bit_2 -sp201_bit_1 -sp201_bit0 -sp201_bit1 -sp201_bit2 -sp201_bit3 -sp201_bit4 -sp201_bit5 -sp201_bit6 -sp201_bit7 -sp201_bit8 -sp201_bit9 -sp201_bit10 -sp201_bit11 -sp201_bit12 dl0_bit0 -dl0_bit1 -dl0_bit2 -dl0_bit3 -dl0_bit4 -dl0_bit5 -dl0_bit6 -dl0_bit7 -dl0_bit8 -dl0_bit9 -dl0_bit10 -dl0_bit11 -dl0_bit12 f2a0a1f1_bit0 -f2a0a1f1_bit1 -f2a0a1f1_bit2 -f2a0a1f1_bit3 -f2a0a1f1_bit4 -f2a0a1f1_bit5 -f2a0a1f1_bit6 -f2a0a1f1_bit7 -f2a0a1f1_bit8 -f2a0a1f1_bit9 -f2a0a1f1_bit10 -f2a0a1f1_bit11 -f2a0a1f1_bit12 -dl1_bit0 -dl1_bit1 -dl1_bit2 -dl1_bit3 -dl1_bit4 -dl1_bit5 -dl1_bit6 -dl1_bit7 -dl1_bit8 -dl1_bit9 -dl1_bit10 -dl1_bit11 -dl1_bit12 f2a0a3f3_bit0 -f2a0a3f3_bit1 -f2a0a3f3_bit2 -f2a0a3f3_bit3 -f2a0a3f3_bit4 -f2a0a3f3_bit5 -f2a0a3f3_bit6 -f2a0a3f3_bit7 -f2a0a3f3_bit8 -f2a0a3f3_bit9 -f2a0a3f3_bit10 -f2a0a3f3_bit11 -f2a0a3f3_bit12 -f2a0a4f4_bit0 -f2a0a4f4_bit1 -f2a0a4f4_bit2 -f2a0a4f4_bit3 -f2a0a4f4_bit4 -f2a0a4f4_bit5 -f2a0a4f4_bit6 -f2a0a4f4_bit7 -f2a0a4f4_bit8 -f2a0a4f4_bit9 -f2a0a4f4_bit10 -f2a0a4f4_bit11 -f2a0a4f4_bit12 -dl2_bit0 dl2_bit1 -dl2_bit2 -dl2_bit3 -dl2_bit4 -dl2_bit5 -dl2_bit6 -dl2_bit7 -dl2_bit8 -dl2_bit9 -dl2_bit10 -dl2_bit11 -dl2_bit12 -sp030_bit_7 -sp030_bit_6 -sp030_bit_5 -sp030_bit_4 -sp030_bit_3 -sp030_bit_2 -sp030_bit_1 -sp030_bit0 -sp030_bit1 -sp030_bit2 -sp030_bit3 -sp030_bit4 -sp030_bit5 -sp030_bit6 -sp030_bit7 -sp030_bit8 -sp030_bit9 -sp030_bit10 -sp030_bit11 -sp030_bit12 -sp031_bit_7 -sp031_bit_6 -sp031_bit_5 -sp031_bit_4 -sp031_bit_3 -sp031_bit_2 -sp031_bit_1 -sp031_bit0 -sp031_bit1 -sp031_bit2 -sp031_bit3 -sp031_bit4 -sp031_bit5 -sp031_bit6 -sp031_bit7 -sp031_bit8 -sp031_bit9 -sp031_bit10 -sp031_bit11 -sp031_bit12 f0a3a1f1_bit0 -f0a3a1f1_bit1 -f0a3a1f1_bit2 -f0a3a1f1_bit3 -f0a3a1f1_bit4 -f0a3a1f1_bit5 -f0a3a1f1_bit6 -f0a3a1f1_bit7 -f0a3a1f1_bit8 -f0a3a1f1_bit9 -f0a3a1f1_bit10 -f0a3a1f1_bit11 -f0a3a1f1_bit12 dl3_bit0 -dl3_bit1 -dl3_bit2 -dl3_bit3 -dl3_bit4 -dl3_bit5 -dl3_bit6 -dl3_bit7 -dl3_bit8 -dl3_bit9 -dl3_bit10 -dl3_bit11 -dl3_bit12 f0a3a2f2_bit0 -f0a3a2f2_bit1 -f0a3a2f2_bit2 -f0a3a2f2_bit3 -f0a3a2f2_bit4 -f0a3a2f2_bit5 -f0a3a2f2_bit6 -f0a3a2f2_bit7 -f0a3a2f2_bit8 -f0a3a2f2_bit9 -f0a3a2f2_bit10 -f0a3a2f2_bit11 -f0a3a2f2_bit12 -dl4_bit0 dl4_bit1 -dl4_bit2 -dl4_bit3 -dl4_bit4 -dl4_bit5 -dl4_bit6 -dl4_bit7 -dl4_bit8 -dl4_bit9 -dl4_bit10 -dl4_bit11 -dl4_bit12 f0a3a4f4_bit0 -f0a3a4f4_bit1 -f0a3a4f4_bit2 -f0a3a4f4_bit3 -f0a3a4f4_bit4 -f0a3a4f4_bit5 -f0a3a4f4_bit6 -f0a3a4f4_bit7 -f0a3a4f4_bit8 -f0a3a4f4_bit9 -f0a3a4f4_bit10 -f0a3a4f4_bit11 -f0a3a4f4_bit12 -sp300_bit_7 -sp300_bit_6 -sp300_bit_5 -sp300_bit_4 -sp300_bit_3 -sp300_bit_2 -sp300_bit_1 -sp300_bit0 -sp300_bit1 -sp300_bit2 -sp300_bit3 -sp300_bit4 -sp300_bit5 -sp300_bit6 -sp300_bit7 -sp300_bit8 -sp300_bit9 -sp300_bit10 -sp300_bit11 -sp300_bit12 -sp301_bit_7 -sp301_bit_6 -sp301_bit_5 -sp301_bit_4 -sp301_bit_3 -sp301_bit_2 -sp301_bit_1 -sp301_bit0 -sp301_bit1 -sp301_bit2 -sp301_bit3 -sp301_bit4 -sp301_bit5 -sp301_bit6 -sp301_bit7 -sp301_bit8 -sp301_bit9 -sp301_bit10 -sp301_bit11 -sp301_bit12 f3a0a1f1_bit0 -f3a0a1f1_bit1 -f3a0a1f1_bit2 -f3a0a1f1_bit3 -f3a0a1f1_bit4 -f3a0a1f1_bit5 -f3a0a1f1_bit6 -f3a0a1f1_bit7 -f3a0a1f1_bit8 -f3a0a1f1_bit9 -f3a0a1f1_bit10 -f3a0a1f1_bit11 -f3a0a1f1_bit12 -f3a0a2f2_bit0 -f3a0a2f2_bit1 -f3a0a2f2_bit2 -f3a0a2f2_bit3 -f3a0a2f2_bit4 -f3a0a2f2_bit5 -f3a0a2f2_bit6 -f3a0a2f2_bit7 -f3a0a2f2_bit8 -f3a0a2f2_bit9 -f3a0a2f2_bit10 -f3a0a2f2_bit11 -f3a0a2f2_bit12 -f3a0a4f4_bit0 -f3a0a4f4_bit1 -f3a0a4f4_bit2 -f3a0a4f4_bit3 -f3a0a4f4_bit4 -f3a0a4f4_bit5 -f3a0a4f4_bit6 -f3a0a4f4_bit7 -f3a0a4f4_bit8 -f3a0a4f4_bit9 -f3a0a4f4_bit10 -f3a0a4f4_bit11 -f3a0a4f4_bit12 -sp040_bit_7 -sp040_bit_6 -sp040_bit_5 -sp040_bit_4 -sp040_bit_3 -sp040_bit_2 -sp040_bit_1 sp040_bit0 -sp040_bit1 -sp040_bit2 -sp040_bit3 -sp040_bit4 -sp040_bit5 -sp040_bit6 -sp040_bit7 -sp040_bit8 -sp040_bit9 -sp040_bit10 -sp040_bit11 -sp040_bit12 -sp041_bit_7 -sp041_bit_6 -sp041_bit_5 -sp041_bit_4 -sp041_bit_3 -sp041_bit_2 -sp041_bit_1 -sp041_bit0 -sp041_bit1 -sp041_bit2 -sp041_bit3 -sp041_bit4 -sp041_bit5 -sp041_bit6 -sp041_bit7 -sp041_bit8 -sp041_bit9 -sp041_bit10 -sp041_bit11 -sp041_bit12 f0a4a1f1_bit0 -f0a4a1f1_bit1 -f0a4a1f1_bit2 -f0a4a1f1_bit3 -f0a4a1f1_bit4 -f0a4a1f1_bit5 -f0a4a1f1_bit6 -f0a4a1f1_bit7 -f0a4a1f1_bit8 -f0a4a1f1_bit9 -f0a4a1f1_bit10 -f0a4a1f1_bit11 -f0a4a1f1_bit12 -f0a4a2f2_bit0 -f0a4a2f2_bit1 -f0a4a2f2_bit2 -f0a4a2f2_bit3 -f0a4a2f2_bit4 -f0a4a2f2_bit5 -f0a4a2f2_bit6 -f0a4a2f2_bit7 -f0a4a2f2_bit8 -f0a4a2f2_bit9 -f0a4a2f2_bit10 -f0a4a2f2_bit11 -f0a4a2f2_bit12 -f0a4a3f3_bit0 -f0a4a3f3_bit1 -f0a4a3f3_bit2 -f0a4a3f3_bit3 -f0a4a3f3_bit4 -f0a4a3f3_bit5 -f0a4a3f3_bit6 -f0a4a3f3_bit7 -f0a4a3f3_bit8 -f0a4a3f3_bit9 -f0a4a3f3_bit10 -f0a4a3f3_bit11 -f0a4a3f3_bit12 -sp400_bit_7 -sp400_bit_6 -sp400_bit_5 -sp400_bit_4 -sp400_bit_3 -sp400_bit_2 -sp400_bit_1 sp400_bit0 -sp400_bit1 -sp400_bit2 -sp400_bit3 -sp400_bit4 -sp400_bit5 -sp400_bit6 -sp400_bit7 -sp400_bit8 -sp400_bit9 -sp400_bit10 -sp400_bit11 -sp400_bit12 -sp401_bit_7 -sp401_bit_6 -sp401_bit_5 -sp401_bit_4 -sp401_bit_3 -sp401_bit_2 -sp401_bit_1 -sp401_bit0 -sp401_bit1 -sp401_bit2 -sp401_bit3 -sp401_bit4 -sp401_bit5 -sp401_bit6 -sp401_bit7 -sp401_bit8 -sp401_bit9 -sp401_bit10 -sp401_bit11 -sp401_bit12 f4a0a1f1_bit0 -f4a0a1f1_bit1 -f4a0a1f1_bit2 -f4a0a1f1_bit3 -f4a0a1f1_bit4 -f4a0a1f1_bit5 -f4a0a1f1_bit6 -f4a0a1f1_bit7 -f4a0a1f1_bit8 -f4a0a1f1_bit9 -f4a0a1f1_bit10 -f4a0a1f1_bit11 -f4a0a1f1_bit12
c _______________________________________________________________________________
c 
c restarts              : 19
c conflicts             : 1455           (133 /sec)
c decisions             : 4578           (420 /sec)
c propagations          : 542067         (49729 /sec)
c inspects              : 2175562        (199587 /sec)
c CPU time              : 10.9003 s
c _______________________________________________________________________________
#### 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.88 0.94 0.90 2/54 26947
Raw data (stat): 26947 (runsolver) R 26946 29653 29652 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 482555369 1052672 99 4294967295 134512640 135381576 3221224448 3221219692 135158418 0 0 7 90112 0 0 0 17 0 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+9.99951 s]
Raw data (loadavg): 0.90 0.94 0.90 2/54 26947
Raw data (stat): 26947 (minisat+) R 26946 29653 29652 0 -1 0 12674 0 0 0 952 47 0 0 25 0 1 0 482555369 25120768 5545 4294967295 134512640 134672761 3221224544 3221222920 1075384046 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6133 5545 603 41 0 6092 0
vsize: 24532
[startup+11.4605 s]
Raw data (loadavg): 0.90 0.94 0.90 1/53 26947
Raw data (stat): 26947 (minisat+) R 26946 29653 29652 0 -1 0 12674 0 0 0 952 47 0 0 25 0 1 0 482555369 25120768 5545 4294967295 134512640 134672761 3221224544 3221222920 1075384046 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6133 5545 603 41 0 6092 0
vsize: 0

Child status: 30
Real time (s): 11.4603
CPU time (s): 11.4393
CPU user time (s): 10.9113
CPU system time (s): 0.527919
CPU usage (%): 99.8167
Max. virtual memory (Kb): 24532
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
Verifier:	OK	-58624
#### END VERIFIER DATA ####