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/MIPLIB/miplib2003/normalized-mps-v2-13-7-aflow40b.opb
MD5SUM	7872170cf5be0e3f0e6be125266c16ee
Bench Category	optimization, small integers (OPTSMALLINT)
Has Objective Function	YES
Satisfiable
(Un)Satisfiability was proved
Best value of the objective function
Optimality of the best value was proved
Number of terms in the objective function	1364
Biggest coefficient in the objective function	500
Number of bits for the biggest coefficient in the objective function	9
Sum of the numbers in the objective function	230637
Number of bits of the sum of numbers in the objective function	18
Biggest number in a constraint	12800
Number of bits of the biggest number in a constraint	14
Biggest sum of numbers in a constraint	879673
Number of bits of the biggest sum of numbers	20
Best result obtained on this benchmark
Best CPU time to get the best result obtained on this benchmark
Number of variables	19292
Total number of constraints	4170
Number of constraints which are clauses	0
Number of constraints which are cardinality constraints (but not clauses)	1403
Number of constraints which are nor clauses,nor cardinality constraints	2767
Minimum length of a constraint	1
Maximum length of a constraint	980
Trace number 18860

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc12 THE 2005-04-21 16:47:54 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=17412 boxname=wulflinc12 idbench=1340 idsolver=5 numberseed=0
MD5SUM SOLVER: 1d62365061f6d70b1a242542b016b2e4  /oldhome/oroussel/solvers/minisat+
MD5SUM BENCH:  7872170cf5be0e3f0e6be125266c16ee  /oldhome/oroussel/tmp/wulflinc12/normalized-mps-v2-13-7-aflow40b.opb
REAL COMMAND:  minisat+ /oldhome/oroussel/tmp/wulflinc12/normalized-mps-v2-13-7-aflow40b.opb
IDLAUNCH: 17412
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.091
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.091
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:        758208 kB
Buffers:         27556 kB
Cached:         227004 kB
SwapCached:        508 kB
Active:          56628 kB
Inactive:       200020 kB
HighTotal:      131008 kB
HighFree:        15708 kB
LowTotal:       903652 kB
LowFree:        742500 kB
SwapTotal:     2097136 kB
SwapFree:      2095888 kB
Dirty:              40 kB
Writeback:           0 kB
Mapped:           5276 kB
Slab:            14116 kB
Committed_AS:    63560 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-21 17:07:56 (client local time) WITH STATUS 0 IN 1200.22 SECONDS
stats: 17412 7 1200.22 0
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 2884 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: ##############################################################################
c   -- Clauses(.)/Splits(s): ssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssss
c ---[3067]---> BDD-cost:   13
c ---[3066]---> BDD-cost:   13
c ---[3064]---> BDD-cost:   12
c ---[3063]---> BDD-cost:   13
c ---[3062]---> BDD-cost:   12
c ---[3061]---> BDD-cost:   11
c ---[3060]---> BDD-cost:   13
c ---[3059]---> BDD-cost:   13
c ---[3058]---> BDD-cost:   11
c ---[3056]---> BDD-cost:   11
c ---[3055]---> BDD-cost:   12
c ---[3053]---> BDD-cost:   13
c ---[3052]---> BDD-cost:   13
c ---[3051]---> BDD-cost:   10
c ---[3049]---> BDD-cost:   12
c ---[3048]---> BDD-cost:   13
c ---[3047]---> BDD-cost:   12
c ---[3046]---> BDD-cost:   13
c ---[3045]---> BDD-cost:   13
c ---[3044]---> BDD-cost:   13
c ---[3042]---> BDD-cost:   12
c ---[3040]---> BDD-cost:   11
c ---[3039]---> BDD-cost:   12
c ---[3038]---> BDD-cost:   12
c ---[3037]---> BDD-cost:   12
c ---[3036]---> BDD-cost:   12
c ---[3035]---> BDD-cost:   11
c ---[3034]---> BDD-cost:   11
c ---[3033]---> BDD-cost:   11
c ---[3032]---> BDD-cost:   13
c ---[3030]---> BDD-cost:   10
c ---[3028]---> BDD-cost:   11
c ---[3026]---> BDD-cost:   13
c ---[3025]---> BDD-cost:   13
c ---[3024]---> BDD-cost:   12
c ---[3023]---> BDD-cost:   13
c ---[3022]---> BDD-cost:   13
c ---[3021]---> BDD-cost:   13
c ---[3020]---> BDD-cost:   13
c ---[3019]---> BDD-cost:   12
c ---[3018]---> BDD-cost:   12
c ---[3017]---> BDD-cost:   11
c ---[3016]---> BDD-cost:   13
c ---[3015]---> BDD-cost:   13
c ---[3014]---> BDD-cost:   11
c ---[3013]---> BDD-cost:   13
c ---[3012]---> BDD-cost:   11
c ---[3011]---> BDD-cost:   11
c ---[3010]---> BDD-cost:   11
c ---[3009]---> BDD-cost:   13
c ---[3008]---> BDD-cost:   11
c ---[3007]---> BDD-cost:   13
c ---[3005]---> BDD-cost:   13
c ---[3004]---> BDD-cost:   13
c ---[3003]---> BDD-cost:   13
c ---[3002]---> BDD-cost:   12
c ---[3001]---> BDD-cost:   13
c ---[3000]---> BDD-cost:   12
c ---[2999]---> BDD-cost:   12
c ---[2998]---> BDD-cost:   12
c ---[2997]---> BDD-cost:   13
c ---[2996]---> BDD-cost:   12
c ---[2995]---> BDD-cost:   12
c ---[2994]---> BDD-cost:   13
c ---[2993]---> BDD-cost:   13
c ---[2992]---> BDD-cost:   13
c ---[2991]---> BDD-cost:   12
c ---[2990]---> BDD-cost:   13
c ---[2989]---> BDD-cost:   11
c ---[2988]---> BDD-cost:   10
c ---[2987]---> BDD-cost:   12
c ---[2986]---> BDD-cost:   12
c ---[2985]---> BDD-cost:   13
c ---[2984]---> BDD-cost:   11
c ---[2983]---> BDD-cost:   11
c ---[2982]---> BDD-cost:   13
c ---[2981]---> BDD-cost:   13
c ---[2980]---> BDD-cost:   13
c ---[2979]---> BDD-cost:   12
c ---[2978]---> BDD-cost:   12
c ---[2977]---> BDD-cost:   13
c ---[2976]---> BDD-cost:   12
c ---[2975]---> BDD-cost:   12
c ---[2974]---> BDD-cost:   13
c ---[2973]---> BDD-cost:   12
c ---[2972]---> BDD-cost:   12
c ---[2971]---> BDD-cost:   12
c ---[2969]---> BDD-cost:   13
c ---[2968]---> BDD-cost:   13
c ---[2967]---> BDD-cost:   12
c ---[2966]---> BDD-cost:   12
c ---[2965]---> BDD-cost:   12
c ---[2964]---> BDD-cost:   13
c ---[2963]---> BDD-cost:   13
c ---[2962]---> BDD-cost:   11
c ---[2961]---> BDD-cost:   13
c ---[2960]---> BDD-cost:   13
c ---[2959]---> BDD-cost:   11
c ---[2958]---> BDD-cost:   11
c ---[2955]---> BDD-cost:   13
c ---[2954]---> BDD-cost:   11
c ---[2953]---> BDD-cost:   13
c ---[2952]---> BDD-cost:   13
c ---[2951]---> BDD-cost:   12
c ---[2950]---> BDD-cost:   12
c ---[2949]---> BDD-cost:   12
c ---[2948]---> BDD-cost:   13
c ---[2947]---> BDD-cost:   12
c ---[2946]---> BDD-cost:   13
c ---[2945]---> BDD-cost:   12
c ---[2943]---> BDD-cost:   12
c ---[2942]---> BDD-cost:   13
c ---[2941]---> BDD-cost:   10
c ---[2940]---> BDD-cost:   13
c ---[2939]---> BDD-cost:   13
c ---[2938]---> BDD-cost:   13
c ---[2937]---> BDD-cost:   12
c ---[2935]---> BDD-cost:   12
c ---[2934]---> BDD-cost:   11
c ---[2933]---> BDD-cost:   13
c ---[2932]---> BDD-cost:   10
c ---[2930]---> BDD-cost:   12
c ---[2929]---> BDD-cost:   13
c ---[2928]---> BDD-cost:   13
c ---[2927]---> BDD-cost:   13
c ---[2926]---> BDD-cost:   13
c ---[2925]---> BDD-cost:   11
c ---[2924]---> BDD-cost:   13
c ---[2923]---> BDD-cost:   12
c ---[2922]---> BDD-cost:   13
c ---[2921]---> BDD-cost:   13
c ---[2919]---> BDD-cost:   12
c ---[2918]---> BDD-cost:   13
c ---[2917]---> BDD-cost:   12
c ---[2916]---> BDD-cost:   13
c ---[2915]---> BDD-cost:   10
c ---[2914]---> BDD-cost:   13
c ---[2913]---> BDD-cost:   12
c ---[2912]---> BDD-cost:   13
c ---[2911]---> BDD-cost:   11
c ---[2909]---> BDD-cost:   13
c ---[2907]---> BDD-cost:   13
c ---[2906]---> BDD-cost:   13
c ---[2905]---> BDD-cost:   11
c ---[2904]---> BDD-cost:   11
c ---[2902]---> BDD-cost:   13
c ---[2901]---> BDD-cost:   13
c ---[2900]---> BDD-cost:   13
c ---[2899]---> BDD-cost:   12
c ---[2898]---> BDD-cost:   13
c ---[2897]---> BDD-cost:   13
c ---[2896]---> BDD-cost:   12
c ---[2895]---> BDD-cost:   13
c ---[2894]---> BDD-cost:   11
c ---[2893]---> BDD-cost:   13
c ---[2892]---> BDD-cost:   13
c ---[2890]---> BDD-cost:   13
c ---[2889]---> BDD-cost:   12
c ---[2888]---> BDD-cost:   13
c ---[2887]---> BDD-cost:   10
c ---[2886]---> BDD-cost:   13
c ---[2884]---> BDD-cost:   13
c ---[2882]---> BDD-cost:   12
c ---[2881]---> BDD-cost:   13
c ---[2879]---> BDD-cost:   11
c ---[2877]---> BDD-cost:   12
c ---[2876]---> BDD-cost:   13
c ---[2875]---> BDD-cost:   13
c ---[2874]---> BDD-cost:   13
c ---[2873]---> BDD-cost:   13
c ---[2872]---> BDD-cost:   13
c ---[2871]---> BDD-cost:   13
c ---[2870]---> BDD-cost:   12
c ---[2869]---> BDD-cost:   13
c ---[2868]---> BDD-cost:   12
c ---[2866]---> BDD-cost:   13
c ---[2865]---> BDD-cost:   13
c ---[2864]---> BDD-cost:   11
c ---[2863]---> BDD-cost:   11
c ---[2862]---> BDD-cost:   11
c ---[2861]---> BDD-cost:   12
c ---[2860]---> BDD-cost:   12
c ---[2859]---> BDD-cost:   13
c ---[2858]---> BDD-cost:   13
c ---[2856]---> BDD-cost:   13
c ---[2855]---> BDD-cost:   12
c ---[2854]---> BDD-cost:   12
c ---[2853]---> BDD-cost:   12
c ---[2852]---> BDD-cost:   10
c ---[2851]---> BDD-cost:   11
c ---[2850]---> BDD-cost:   10
c ---[2849]---> BDD-cost:   12
c ---[2847]---> BDD-cost:   12
c ---[2846]---> BDD-cost:   10
c ---[2845]---> BDD-cost:   13
c ---[2844]---> BDD-cost:   13
c ---[2843]---> BDD-cost:   11
c ---[2842]---> BDD-cost:   13
c ---[2841]---> BDD-cost:   13
c ---[2840]---> BDD-cost:   13
c ---[2839]---> BDD-cost:   13
c ---[2838]---> BDD-cost:   12
c ---[2837]---> BDD-cost:   11
c ---[2836]---> BDD-cost:   11
c ---[2835]---> BDD-cost:   12
c ---[2834]---> BDD-cost:   13
c ---[2833]---> BDD-cost:   12
c ---[2832]---> BDD-cost:   11
c ---[2831]---> BDD-cost:   11
c ---[2830]---> BDD-cost:   12
c ---[2829]---> BDD-cost:   13
c ---[2828]---> BDD-cost:   11
c ---[2827]---> BDD-cost:   11
c ---[2826]---> BDD-cost:   13
c ---[2825]---> BDD-cost:   13
c ---[2824]---> BDD-cost:   11
c ---[2823]---> BDD-cost:   12
c ---[2822]---> BDD-cost:   13
c ---[2821]---> BDD-cost:   10
c ---[2820]---> BDD-cost:   13
c ---[2819]---> BDD-cost:   13
c ---[2817]---> BDD-cost:   13
c ---[2816]---> BDD-cost:   12
c ---[2815]---> BDD-cost:   10
c ---[2814]---> BDD-cost:   12
c ---[2813]---> BDD-cost:   12
c ---[2812]---> BDD-cost:   13
c ---[2811]---> BDD-cost:   11
c ---[2810]---> BDD-cost:   13
c ---[2808]---> BDD-cost:   13
c ---[2806]---> BDD-cost:   12
c ---[2805]---> BDD-cost:   11
c ---[2803]---> BDD-cost:   11
c ---[2802]---> BDD-cost:   13
c ---[2801]---> BDD-cost:   12
c ---[2800]---> BDD-cost:   13
c ---[2797]---> BDD-cost:   13
c ---[2796]---> BDD-cost:   12
c ---[2795]---> BDD-cost:   10
c ---[2794]---> BDD-cost:   13
c ---[2793]---> BDD-cost:   13
c ---[2792]---> BDD-cost:   13
c ---[2791]---> BDD-cost:   11
c ---[2790]---> BDD-cost:   13
c ---[2789]---> BDD-cost:   13
c ---[2788]---> BDD-cost:   13
c ---[2787]---> BDD-cost:   11
c ---[2786]---> BDD-cost:   13
c ---[2785]---> BDD-cost:   11
c ---[2784]---> BDD-cost:   12
c ---[2783]---> BDD-cost:   10
c ---[2781]---> BDD-cost:   13
c ---[2780]---> BDD-cost:   13
c ---[2779]---> BDD-cost:   12
c ---[2778]---> BDD-cost:   12
c ---[2777]---> BDD-cost:   13
c ---[2776]---> BDD-cost:   13
c ---[2775]---> BDD-cost:   13
c ---[2774]---> BDD-cost:   13
c ---[2773]---> BDD-cost:   13
c ---[2772]---> BDD-cost:   13
c ---[2771]---> BDD-cost:   13
c ---[2769]---> BDD-cost:   13
c ---[2768]---> BDD-cost:   13
c ---[2767]---> BDD-cost:   11
c ---[2766]---> BDD-cost:   12
c ---[2765]---> BDD-cost:   12
c ---[2764]---> BDD-cost:   13
c ---[2763]---> BDD-cost:   13
c ---[2762]---> BDD-cost:   13
c ---[2761]---> BDD-cost:   12
c ---[2760]---> BDD-cost:   12
c ---[2759]---> BDD-cost:   12
c ---[2758]---> BDD-cost:   13
c ---[2757]---> BDD-cost:   12
c ---[2756]---> BDD-cost:   13
c ---[2755]---> BDD-cost:   12
c ---[2754]---> BDD-cost:   13
c ---[2753]---> BDD-cost:   13
c ---[2752]---> BDD-cost:   10
c ---[2751]---> BDD-cost:   13
c ---[2750]---> BDD-cost:   11
c ---[2748]---> BDD-cost:   10
c ---[2747]---> BDD-cost:   13
c ---[2746]---> BDD-cost:   13
c ---[2744]---> BDD-cost:   10
c ---[2743]---> BDD-cost:   12
c ---[2742]---> BDD-cost:   13
c ---[2741]---> BDD-cost:   13
c ---[2740]---> BDD-cost:   13
c ---[2739]---> BDD-cost:   12
c ---[2737]---> BDD-cost:   13
c ---[2736]---> BDD-cost:   13
c ---[2735]---> BDD-cost:   12
c ---[2734]---> BDD-cost:   11
c ---[2733]---> BDD-cost:   13
c ---[2732]---> BDD-cost:   13
c ---[2731]---> BDD-cost:   13
c ---[2730]---> BDD-cost:   13
c ---[2728]---> BDD-cost:   13
c ---[2727]---> BDD-cost:   13
c ---[2726]---> BDD-cost:   13
c ---[2724]---> BDD-cost:   13
c ---[2723]---> BDD-cost:   12
c ---[2722]---> BDD-cost:   13
c ---[2721]---> BDD-cost:   13
c ---[2720]---> BDD-cost:   13
c ---[2719]---> BDD-cost:   12
c ---[2718]---> BDD-cost:   13
c ---[2717]---> BDD-cost:   11
c ---[2716]---> BDD-cost:   13
c ---[2715]---> BDD-cost:   12
c ---[2714]---> BDD-cost:   13
c ---[2712]---> BDD-cost:   13
c ---[2710]---> BDD-cost:   13
c ---[2709]---> BDD-cost:   13
c ---[2708]---> BDD-cost:   10
c ---[2706]---> BDD-cost:   13
c ---[2705]---> BDD-cost:   13
c ---[2704]---> BDD-cost:   12
c ---[2703]---> BDD-cost:   13
c ---[2701]---> BDD-cost:   13
c ---[2700]---> BDD-cost:   12
c ---[2699]---> BDD-cost:   12
c ---[2698]---> BDD-cost:   13
c ---[2697]---> BDD-cost:   13
c ---[2696]---> BDD-cost:   13
c ---[2695]---> BDD-cost:   13
c ---[2694]---> BDD-cost:   13
c ---[2693]---> BDD-cost:   13
c ---[2692]---> BDD-cost:   13
c ---[2691]---> BDD-cost:   11
c ---[2690]---> BDD-cost:   13
c ---[2689]---> BDD-cost:   12
c ---[2688]---> BDD-cost:   13
c ---[2687]---> BDD-cost:   13
c ---[2686]---> BDD-cost:   12
c ---[2685]---> BDD-cost:   12
c ---[2684]---> BDD-cost:   13
c ---[2683]---> BDD-cost:   13
c ---[2682]---> BDD-cost:   13
c ---[2681]---> BDD-cost:   11
c ---[2680]---> BDD-cost:   11
c ---[2679]---> BDD-cost:   13
c ---[2678]---> BDD-cost:   12
c ---[2677]---> BDD-cost:   12
c ---[2675]---> BDD-cost:   13
c ---[2674]---> BDD-cost:   13
c ---[2673]---> BDD-cost:   13
c ---[2672]---> BDD-cost:   12
c ---[2671]---> BDD-cost:   11
c ---[2670]---> BDD-cost:   12
c ---[2669]---> BDD-cost:   13
c ---[2668]---> BDD-cost:   10
c ---[2667]---> BDD-cost:   13
c ---[2665]---> BDD-cost:   12
c ---[2664]---> BDD-cost:   11
c ---[2662]---> BDD-cost:   13
c ---[2661]---> BDD-cost:   11
c ---[2660]---> BDD-cost:   11
c ---[2659]---> BDD-cost:   13
c ---[2658]---> BDD-cost:   12
c ---[2656]---> BDD-cost:   13
c ---[2654]---> BDD-cost:   13
c ---[2653]---> BDD-cost:   11
c ---[2652]---> BDD-cost:   12
c ---[2651]---> BDD-cost:   13
c ---[2650]---> BDD-cost:   12
c ---[2648]---> BDD-cost:   12
c ---[2647]---> BDD-cost:   11
c ---[2646]---> BDD-cost:   10
c ---[2645]---> BDD-cost:   12
c ---[2644]---> BDD-cost:   12
c ---[2643]---> BDD-cost:   12
c ---[2642]---> BDD-cost:   12
c ---[2641]---> BDD-cost:   13
c ---[2638]---> BDD-cost:   13
c ---[2637]---> BDD-cost:   12
c ---[2636]---> BDD-cost:   11
c ---[2635]---> BDD-cost:   11
c ---[2634]---> BDD-cost:   10
c ---[2633]---> BDD-cost:   13
c ---[2632]---> BDD-cost:   11
c ---[2631]---> BDD-cost:   12
c ---[2630]---> BDD-cost:   13
c ---[2629]---> BDD-cost:   11
c ---[2628]---> BDD-cost:   12
c ---[2627]---> BDD-cost:   13
c ---[2626]---> BDD-cost:   13
c ---[2625]---> BDD-cost:   12
c ---[2624]---> BDD-cost:   12
c ---[2623]---> BDD-cost:   13
c ---[2622]---> BDD-cost:   13
c ---[2621]---> BDD-cost:   13
c ---[2620]---> BDD-cost:   13
c ---[2619]---> BDD-cost:   11
c ---[2618]---> BDD-cost:   13
c ---[2617]---> BDD-cost:   12
c ---[2616]---> BDD-cost:   13
c ---[2615]---> BDD-cost:   13
c ---[2614]---> BDD-cost:   13
c ---[2613]---> BDD-cost:   12
c ---[2612]---> BDD-cost:   13
c ---[2611]---> BDD-cost:   13
c ---[2610]---> BDD-cost:   12
c ---[2609]---> BDD-cost:   12
c ---[2608]---> BDD-cost:   12
c ---[2606]---> BDD-cost:   12
c ---[2604]---> BDD-cost:   11
c ---[2603]---> BDD-cost:   12
c ---[2602]---> BDD-cost:   13
c ---[2601]---> BDD-cost:   13
c ---[2600]---> BDD-cost:   11
c ---[2599]---> BDD-cost:   13
c ---[2598]---> BDD-cost:   13
c ---[2597]---> BDD-cost:   11
c ---[2596]---> BDD-cost:   13
c ---[2595]---> BDD-cost:   13
c ---[2594]---> BDD-cost:   12
c ---[2593]---> BDD-cost:   13
c ---[2592]---> BDD-cost:   11
c ---[2591]---> BDD-cost:   13
c ---[2590]---> BDD-cost:   12
c ---[2589]---> BDD-cost:   13
c ---[2587]---> BDD-cost:   12
c ---[2586]---> BDD-cost:   13
c ---[2584]---> BDD-cost:   12
c ---[2583]---> BDD-cost:   13
c ---[2582]---> BDD-cost:   13
c ---[2581]---> BDD-cost:   13
c ---[2580]---> BDD-cost:   10
c ---[2579]---> BDD-cost:   11
c ---[2576]---> BDD-cost:   13
c ---[2575]---> BDD-cost:   13
c ---[2574]---> BDD-cost:   13
c ---[2572]---> BDD-cost:   11
c ---[2571]---> BDD-cost:   13
c ---[2570]---> BDD-cost:   13
c ---[2569]---> BDD-cost:   11
c ---[2568]---> BDD-cost:   13
c ---[2567]---> BDD-cost:   10
c ---[2566]---> BDD-cost:   12
c ---[2565]---> BDD-cost:   12
c ---[2564]---> BDD-cost:   13
c ---[2563]---> BDD-cost:   13
c ---[2562]---> BDD-cost:   13
c ---[2561]---> BDD-cost:   12
c ---[2559]---> BDD-cost:   12
c ---[2558]---> BDD-cost:   12
c ---[2557]---> BDD-cost:   13
c ---[2556]---> BDD-cost:   13
c ---[2554]---> BDD-cost:   11
c ---[2553]---> BDD-cost:   12
c ---[2550]---> BDD-cost:   12
c ---[2549]---> BDD-cost:   12
c ---[2548]---> BDD-cost:   11
c ---[2546]---> BDD-cost:   13
c ---[2545]---> BDD-cost:   10
c ---[2543]---> BDD-cost:   12
c ---[2541]---> BDD-cost:   13
c ---[2540]---> BDD-cost:   11
c ---[2539]---> BDD-cost:   13
c ---[2538]---> BDD-cost:   13
c ---[2537]---> BDD-cost:   13
c ---[2535]---> BDD-cost:   12
c ---[2533]---> BDD-cost:   12
c ---[2532]---> BDD-cost:   13
c ---[2531]---> BDD-cost:   11
c ---[2530]---> BDD-cost:   13
c ---[2529]---> BDD-cost:   12
c ---[2528]---> BDD-cost:   13
c ---[2527]---> BDD-cost:   13
c ---[2526]---> BDD-cost:   12
c ---[2524]---> BDD-cost:   13
c ---[2523]---> BDD-cost:   12
c ---[2522]---> BDD-cost:   13
c ---[2520]---> BDD-cost:   10
c ---[2519]---> BDD-cost:   12
c ---[2518]---> BDD-cost:   12
c ---[2517]---> BDD-cost:   13
c ---[2516]---> BDD-cost:   13
c ---[2515]---> BDD-cost:   12
c ---[2514]---> BDD-cost:   12
c ---[2513]---> BDD-cost:   12
c ---[2512]---> BDD-cost:   12
c ---[2511]---> BDD-cost:   13
c ---[2510]---> BDD-cost:   11
c ---[2509]---> BDD-cost:   13
c ---[2507]---> BDD-cost:   12
c ---[2506]---> BDD-cost:   12
c ---[2505]---> BDD-cost:   12
c ---[2504]---> BDD-cost:   13
c ---[2503]---> BDD-cost:   12
c ---[2502]---> BDD-cost:   13
c ---[2499]---> BDD-cost:   11
c ---[2498]---> BDD-cost:   13
c ---[2497]---> BDD-cost:   13
c ---[2495]---> BDD-cost:   13
c ---[2491]---> BDD-cost:   13
c ---[2489]---> BDD-cost:   12
c ---[2488]---> BDD-cost:   12
c ---[2484]---> BDD-cost:   12
c ---[2483]---> BDD-cost:   13
c ---[2482]---> BDD-cost:   13
c ---[2481]---> BDD-cost:   11
c ---[2479]---> BDD-cost:   10
c ---[2477]---> BDD-cost:   12
c ---[2476]---> BDD-cost:   13
c ---[2475]---> BDD-cost:   13
c ---[2474]---> BDD-cost:   13
c ---[2473]---> BDD-cost:   11
c ---[2472]---> BDD-cost:   13
c ---[2471]---> BDD-cost:   12
c ---[2470]---> BDD-cost:   13
c ---[2469]---> BDD-cost:   12
c ---[2468]---> BDD-cost:   12
c ---[2467]---> BDD-cost:   12
c ---[2466]---> BDD-cost:   13
c ---[2464]---> BDD-cost:   11
c ---[2463]---> BDD-cost:   12
c ---[2462]---> BDD-cost:   12
c ---[2460]---> BDD-cost:   11
c ---[2459]---> BDD-cost:   13
c ---[2457]---> BDD-cost:   11
c ---[2456]---> BDD-cost:   11
c ---[2454]---> BDD-cost:   13
c ---[2453]---> BDD-cost:   10
c ---[2451]---> BDD-cost:   13
c ---[2450]---> BDD-cost:   13
c ---[2449]---> BDD-cost:   13
c ---[2447]---> BDD-cost:   12
c ---[2446]---> BDD-cost:   13
c ---[2445]---> BDD-cost:   12
c ---[2444]---> BDD-cost:   10
c ---[2443]---> BDD-cost:   13
c ---[2442]---> BDD-cost:   13
c ---[2440]---> BDD-cost:   12
c ---[2439]---> BDD-cost:   13
c ---[2438]---> BDD-cost:   12
c ---[2437]---> BDD-cost:   12
c ---[2436]---> BDD-cost:   11
c ---[2435]---> BDD-cost:   13
c ---[2434]---> BDD-cost:   13
c ---[2433]---> BDD-cost:   13
c ---[2432]---> BDD-cost:   13
c ---[2431]---> BDD-cost:   13
c ---[2430]---> BDD-cost:   12
c ---[2429]---> BDD-cost:   13
c ---[2428]---> BDD-cost:   12
c ---[2427]---> BDD-cost:   13
c ---[2426]---> BDD-cost:   13
c ---[2425]---> BDD-cost:   12
c ---[2424]---> BDD-cost:   13
c ---[2423]---> BDD-cost:   11
c ---[2422]---> BDD-cost:   12
c ---[2421]---> BDD-cost:   10
c ---[2419]---> BDD-cost:   11
c ---[2418]---> BDD-cost:   11
c ---[2417]---> BDD-cost:   12
c ---[2416]---> BDD-cost:   13
c ---[2415]---> BDD-cost:   12
c ---[2413]---> BDD-cost:   12
c ---[2412]---> BDD-cost:   13
c ---[2410]---> BDD-cost:   13
c ---[2409]---> BDD-cost:   13
c ---[2408]---> BDD-cost:   11
c ---[2407]---> BDD-cost:   13
c ---[2406]---> BDD-cost:   11
c ---[2405]---> BDD-cost:   13
c ---[2404]---> BDD-cost:   12
c ---[2403]---> BDD-cost:   13
c ---[2402]---> BDD-cost:   11
c ---[2401]---> BDD-cost:   13
c ---[2400]---> BDD-cost:   12
c ---[2399]---> BDD-cost:   13
c ---[2398]---> BDD-cost:   10
c ---[2397]---> BDD-cost:   12
c ---[2396]---> BDD-cost:   12
c ---[2395]---> BDD-cost:   13
c ---[2394]---> BDD-cost:   12
c ---[2393]---> BDD-cost:   10
c ---[2392]---> BDD-cost:   13
c ---[2390]---> BDD-cost:   12
c ---[2389]---> BDD-cost:   11
c ---[2388]---> BDD-cost:   13
c ---[2387]---> BDD-cost:   11
c ---[2386]---> BDD-cost:   13
c ---[2385]---> BDD-cost:   12
c ---[2384]---> BDD-cost:   13
c ---[2383]---> BDD-cost:   13
c ---[2382]---> BDD-cost:   13
c ---[2381]---> BDD-cost:   10
c ---[2379]---> BDD-cost:   12
c ---[2378]---> BDD-cost:   12
c ---[2377]---> BDD-cost:   13
c ---[2376]---> BDD-cost:   13
c ---[2375]---> BDD-cost:   11
c ---[2374]---> BDD-cost:   12
c ---[2373]---> BDD-cost:   12
c ---[2372]---> BDD-cost:   12
c ---[2371]---> BDD-cost:   12
c ---[2370]---> BDD-cost:   10
c ---[2369]---> BDD-cost:   13
c ---[2367]---> BDD-cost:   12
c ---[2366]---> BDD-cost:   13
c ---[2365]---> BDD-cost:   13
c ---[2364]---> BDD-cost:   10
c ---[2363]---> BDD-cost:   13
c ---[2362]---> BDD-cost:   11
c ---[2361]---> BDD-cost:   13
c ---[2360]---> BDD-cost:   12
c ---[2359]---> BDD-cost:   12
c ---[2358]---> BDD-cost:   12
c ---[2357]---> BDD-cost:   13
c ---[2356]---> BDD-cost:   13
c ---[2354]---> BDD-cost:   11
c ---[2353]---> BDD-cost:   13
c ---[2352]---> BDD-cost:   13
c ---[2350]---> BDD-cost:   13
c ---[2348]---> BDD-cost:   10
c ---[2347]---> BDD-cost:   11
c ---[2346]---> BDD-cost:   13
c ---[2345]---> BDD-cost:   13
c ---[2344]---> BDD-cost:   13
c ---[2342]---> BDD-cost:   13
c ---[2341]---> BDD-cost:   13
c ---[2340]---> BDD-cost:   13
c ---[2338]---> BDD-cost:   13
c ---[2337]---> BDD-cost:   12
c ---[2336]---> BDD-cost:   13
c ---[2334]---> BDD-cost:   13
c ---[2333]---> BDD-cost:   13
c ---[2332]---> BDD-cost:   10
c ---[2331]---> BDD-cost:   12
c ---[2330]---> BDD-cost:   13
c ---[2329]---> BDD-cost:   13
c ---[2328]---> BDD-cost:   13
c ---[2327]---> BDD-cost:   13
c ---[2324]---> BDD-cost:   11
c ---[2321]---> BDD-cost:   13
c ---[2320]---> BDD-cost:   12
c ---[2319]---> BDD-cost:   13
c ---[2318]---> BDD-cost:   13
c ---[2317]---> BDD-cost:   13
c ---[2315]---> BDD-cost:   13
c ---[2314]---> BDD-cost:   11
c ---[2313]---> BDD-cost:   12
c ---[2312]---> BDD-cost:   13
c ---[2311]---> BDD-cost:   12
c ---[2310]---> BDD-cost:   12
c ---[2309]---> BDD-cost:   11
c ---[2307]---> BDD-cost:   13
c ---[2306]---> BDD-cost:   10
c ---[2305]---> BDD-cost:   10
c ---[2304]---> BDD-cost:   13
c ---[2303]---> BDD-cost:   13
c ---[2302]---> BDD-cost:   13
c ---[2301]---> BDD-cost:   13
c ---[2300]---> BDD-cost:   12
c ---[2299]---> BDD-cost:   12
c ---[2298]---> BDD-cost:   11
c ---[2297]---> BDD-cost:   10
c ---[2296]---> BDD-cost:   13
c ---[2294]---> BDD-cost:   12
c ---[2293]---> BDD-cost:   13
c ---[2292]---> BDD-cost:   12
c ---[2291]---> BDD-cost:   11
c ---[2290]---> BDD-cost:   12
c ---[2289]---> BDD-cost:   13
c ---[2288]---> BDD-cost:   11
c ---[2287]---> BDD-cost:   11
c ---[2286]---> BDD-cost:   12
c ---[2285]---> BDD-cost:   12
c ---[2284]---> BDD-cost:   13
c ---[2283]---> BDD-cost:   13
c ---[2282]---> BDD-cost:   11
c ---[2281]---> BDD-cost:   11
c ---[2280]---> BDD-cost:   12
c ---[2279]---> BDD-cost:   13
c ---[2277]---> BDD-cost:   12
c ---[2276]---> BDD-cost:   13
c ---[2275]---> BDD-cost:   13
c ---[2274]---> BDD-cost:   12
c ---[2273]---> BDD-cost:   13
c ---[2272]---> BDD-cost:   12
c ---[2271]---> BDD-cost:   12
c ---[2268]---> BDD-cost:   13
c ---[2267]---> BDD-cost:   11
c ---[2265]---> BDD-cost:   13
c ---[2264]---> BDD-cost:   12
c ---[2263]---> BDD-cost:   12
c ---[2262]---> BDD-cost:   10
c ---[2260]---> BDD-cost:   12
c ---[2259]---> BDD-cost:   12
c ---[2258]---> BDD-cost:   13
c ---[2257]---> BDD-cost:   12
c ---[2256]---> BDD-cost:   12
c ---[2255]---> BDD-cost:   13
c ---[2254]---> BDD-cost:   11
c ---[2253]---> BDD-cost:   13
c ---[2252]---> BDD-cost:   13
c ---[2251]---> BDD-cost:   12
c ---[2250]---> BDD-cost:   13
c ---[2249]---> BDD-cost:   13
c ---[2248]---> BDD-cost:   11
c ---[2247]---> BDD-cost:   12
c ---[2246]---> BDD-cost:   11
c ---[2245]---> BDD-cost:   12
c ---[2244]---> BDD-cost:   13
c ---[2243]---> BDD-cost:   13
c ---[2242]---> BDD-cost:   12
c ---[2241]---> BDD-cost:   13
c ---[2240]---> BDD-cost:   12
c ---[2239]---> BDD-cost:   13
c ---[2238]---> BDD-cost:   13
c ---[2237]---> BDD-cost:   12
c ---[2236]---> BDD-cost:   13
c ---[2235]---> BDD-cost:   11
c ---[2234]---> BDD-cost:   13
c ---[2233]---> BDD-cost:   13
c ---[2232]---> BDD-cost:   13
c ---[2231]---> BDD-cost:   12
c ---[2230]---> BDD-cost:   13
c ---[2229]---> BDD-cost:   11
c ---[2228]---> BDD-cost:   13
c ---[2226]---> BDD-cost:   12
c ---[2225]---> BDD-cost:   12
c ---[2224]---> BDD-cost:   12
c ---[2223]---> BDD-cost:   13
c ---[2222]---> BDD-cost:   13
c ---[2221]---> BDD-cost:   13
c ---[2220]---> BDD-cost:   12
c ---[2219]---> BDD-cost:   12
c ---[2218]---> BDD-cost:   10
c ---[2217]---> BDD-cost:   13
c ---[2216]---> BDD-cost:   13
c ---[2215]---> BDD-cost:   12
c ---[2214]---> BDD-cost:   12
c ---[2213]---> BDD-cost:   11
c ---[2212]---> BDD-cost:   10
c ---[2211]---> BDD-cost:   13
c ---[2210]---> BDD-cost:   13
c ---[2208]---> BDD-cost:   10
c ---[2207]---> BDD-cost:   12
c ---[2206]---> BDD-cost:   12
c ---[2205]---> BDD-cost:   13
c ---[2204]---> BDD-cost:   12
c ---[2203]---> BDD-cost:   13
c ---[2202]---> BDD-cost:   13
c ---[2200]---> BDD-cost:   13
c ---[2199]---> BDD-cost:   13
c ---[2198]---> BDD-cost:   11
c ---[2195]---> BDD-cost:   13
c ---[2194]---> BDD-cost:   10
c ---[2193]---> BDD-cost:   12
c ---[2192]---> BDD-cost:   11
c ---[2191]---> BDD-cost:   12
c ---[2190]---> BDD-cost:   13
c ---[2189]---> BDD-cost:   12
c ---[2188]---> BDD-cost:   13
c ---[2187]---> BDD-cost:   13
c ---[2186]---> BDD-cost:   13
c ---[2184]---> BDD-cost:   10
c ---[2182]---> BDD-cost:   13
c ---[2181]---> BDD-cost:   13
c ---[2180]---> BDD-cost:   11
c ---[2179]---> BDD-cost:   12
c ---[2178]---> BDD-cost:   13
c ---[2177]---> BDD-cost:   13
c ---[2175]---> BDD-cost:   13
c ---[2173]---> BDD-cost:   10
c ---[2172]---> BDD-cost:   12
c ---[2171]---> BDD-cost:   13
c ---[2170]---> BDD-cost:   11
c ---[2168]---> BDD-cost:   13
c ---[2167]---> BDD-cost:   12
c ---[2166]---> BDD-cost:   13
c ---[2165]---> BDD-cost:   13
c ---[2164]---> BDD-cost:   13
c ---[2163]---> BDD-cost:   13
c ---[2162]---> BDD-cost:   12
c ---[2161]---> BDD-cost:   12
c ---[2159]---> BDD-cost:   11
c ---[2158]---> BDD-cost:   12
c ---[2157]---> BDD-cost:   12
c ---[2155]---> BDD-cost:   12
c ---[2154]---> BDD-cost:   13
c ---[2153]---> BDD-cost:   13
c ---[2152]---> BDD-cost:   12
c ---[2151]---> BDD-cost:   13
c ---[2150]---> BDD-cost:   13
c ---[2149]---> BDD-cost:   13
c ---[2148]---> BDD-cost:   11
c ---[2147]---> BDD-cost:   11
c ---[2146]---> BDD-cost:   13
c ---[2145]---> BDD-cost:   13
c ---[2144]---> BDD-cost:   13
c ---[2143]---> BDD-cost:   13
c ---[2142]---> BDD-cost:   13
c ---[2141]---> BDD-cost:   10
c ---[2140]---> BDD-cost:   12
c ---[2139]---> BDD-cost:   10
c ---[2137]---> BDD-cost:   12
c ---[2136]---> BDD-cost:   13
c ---[2135]---> BDD-cost:   13
c ---[2134]---> BDD-cost:   13
c ---[2133]---> BDD-cost:   12
c ---[2132]---> BDD-cost:   12
c ---[2131]---> BDD-cost:   12
c ---[2130]---> BDD-cost:   12
c ---[2129]---> BDD-cost:   12
c ---[2128]---> BDD-cost:   13
c ---[2127]---> BDD-cost:   13
c ---[2126]---> BDD-cost:   12
c ---[2124]---> BDD-cost:   13
c ---[2123]---> BDD-cost:   12
c ---[2122]---> BDD-cost:   11
c ---[2121]---> BDD-cost:   10
c ---[2120]---> BDD-cost:   13
c ---[2119]---> BDD-cost:   12
c ---[2118]---> BDD-cost:   12
c ---[2117]---> BDD-cost:   11
c ---[2116]---> BDD-cost:   13
c ---[2115]---> BDD-cost:   13
c ---[2114]---> BDD-cost:   13
c ---[2113]---> BDD-cost:   12
c ---[2112]---> BDD-cost:   13
c ---[2111]---> BDD-cost:   13
c ---[2110]---> BDD-cost:   13
c ---[2109]---> BDD-cost:   13
c ---[2107]---> BDD-cost:   13
c ---[2106]---> BDD-cost:   10
c ---[2105]---> BDD-cost:   12
c ---[2104]---> BDD-cost:   13
c ---[2102]---> BDD-cost:   13
c ---[2101]---> BDD-cost:   12
c ---[2100]---> BDD-cost:   13
c ---[2099]---> BDD-cost:   13
c ---[2098]---> BDD-cost:   13
c ---[2097]---> BDD-cost:   13
c ---[2096]---> BDD-cost:   11
c ---[2095]---> BDD-cost:   13
c ---[2093]---> BDD-cost:   11
c ---[2092]---> BDD-cost:   11
c ---[2091]---> BDD-cost:   13
c ---[2090]---> BDD-cost:   13
c ---[2089]---> BDD-cost:   12
c ---[2088]---> BDD-cost:   12
c ---[2087]---> BDD-cost:   12
c ---[2086]---> BDD-cost:   13
c ---[2084]---> BDD-cost:   13
c ---[2083]---> BDD-cost:   13
c ---[2082]---> BDD-cost:   12
c ---[2081]---> BDD-cost:   12
c ---[2080]---> BDD-cost:   13
c ---[2079]---> BDD-cost:   13
c ---[2078]---> BDD-cost:   13
c ---[2077]---> BDD-cost:   12
c ---[2076]---> BDD-cost:   12
c ---[2075]---> BDD-cost:   11
c ---[2074]---> BDD-cost:   12
c ---[2073]---> BDD-cost:   12
c ---[2072]---> BDD-cost:   13
c ---[2071]---> BDD-cost:   13
c ---[2070]---> BDD-cost:   13
c ---[2069]---> BDD-cost:   13
c ---[2068]---> BDD-cost:   12
c ---[2067]---> BDD-cost:   11
c ---[2066]---> BDD-cost:   13
c ---[2065]---> BDD-cost:   13
c ---[2064]---> BDD-cost:   11
c ---[2063]---> BDD-cost:   12
c ---[2062]---> BDD-cost:   10
c ---[2061]---> BDD-cost:   13
c ---[2060]---> BDD-cost:   12
c ---[2059]---> BDD-cost:   11
c ---[2058]---> BDD-cost:   13
c ---[2057]---> BDD-cost:   12
c ---[2056]---> BDD-cost:   12
c ---[2055]---> BDD-cost:   11
c ---[2054]---> BDD-cost:   12
c ---[2052]---> BDD-cost:   13
c ---[2051]---> BDD-cost:   12
c ---[2050]---> BDD-cost:   13
c ---[2048]---> BDD-cost:   13
c ---[2047]---> BDD-cost:   12
c ---[2046]---> BDD-cost:   13
c ---[2045]---> BDD-cost:   13
c ---[2044]---> BDD-cost:   12
c ---[2042]---> BDD-cost:   12
c ---[2041]---> BDD-cost:   13
c ---[2040]---> BDD-cost:   13
c ---[2039]---> BDD-cost:   11
c ---[2038]---> BDD-cost:   12
c ---[2037]---> BDD-cost:   13
c ---[2036]---> BDD-cost:   13
c ---[2034]---> BDD-cost:   13
c ---[2033]---> BDD-cost:   12
c ---[2031]---> BDD-cost:   13
c ---[2030]---> BDD-cost:   10
c ---[2029]---> BDD-cost:   11
c ---[2028]---> BDD-cost:   12
c ---[2027]---> BDD-cost:   13
c ---[2026]---> BDD-cost:   13
c ---[2025]---> BDD-cost:   13
c ---[2024]---> BDD-cost:   13
c ---[2023]---> BDD-cost:   13
c ---[2022]---> BDD-cost:   12
c ---[2021]---> BDD-cost:   13
c ---[2020]---> BDD-cost:   12
c ---[2019]---> BDD-cost:   12
c ---[2018]---> BDD-cost:   11
c ---[2017]---> BDD-cost:   13
c ---[2015]---> BDD-cost:   13
c ---[2014]---> BDD-cost:   12
c ---[2013]---> BDD-cost:   12
c ---[2012]---> BDD-cost:   12
c ---[2011]---> BDD-cost:   13
c ---[2010]---> BDD-cost:   13
c ---[2009]---> BDD-cost:   13
c ---[2008]---> BDD-cost:   11
c ---[2007]---> BDD-cost:   13
c ---[2006]---> BDD-cost:   13
c ---[2005]---> BDD-cost:   13
c ---[2004]---> BDD-cost:   12
c ---[2003]---> BDD-cost:   13
c ---[2002]---> BDD-cost:   13
c ---[2001]---> BDD-cost:   13
c ---[2000]---> BDD-cost:   12
c ---[1999]---> BDD-cost:   12
c ---[1998]---> BDD-cost:   11
c ---[1997]---> BDD-cost:   13
c ---[1995]---> BDD-cost:   12
c ---[1994]---> BDD-cost:   11
c ---[1993]---> BDD-cost:   13
c ---[1992]---> BDD-cost:   12
c ---[1991]---> BDD-cost:   13
c ---[1990]---> BDD-cost:   12
c ---[1989]---> BDD-cost:   10
c ---[1988]---> BDD-cost:   12
c ---[1987]---> BDD-cost:   13
c ---[1986]---> BDD-cost:   11
c ---[1985]---> BDD-cost:   12
c ---[1984]---> BDD-cost:   12
c ---[1983]---> BDD-cost:   12
c ---[1982]---> BDD-cost:   12
c ---[1981]---> BDD-cost:   12
c ---[1980]---> BDD-cost:   11
c ---[1979]---> BDD-cost:   12
c ---[1978]---> BDD-cost:   13
c ---[1977]---> BDD-cost:   12
c ---[1975]---> BDD-cost:   12
c ---[1974]---> BDD-cost:   12
c ---[1973]---> BDD-cost:   11
c ---[1972]---> BDD-cost:   10
c ---[1971]---> BDD-cost:   13
c ---[1970]---> BDD-cost:   12
c ---[1969]---> BDD-cost:   12
c ---[1968]---> BDD-cost:   13
c ---[1967]---> BDD-cost:   12
c ---[1966]---> BDD-cost:   13
c ---[1965]---> BDD-cost:   11
c ---[1964]---> BDD-cost:   12
c ---[1963]---> BDD-cost:   12
c ---[1962]---> BDD-cost:   13
c ---[1960]---> BDD-cost:   13
c ---[1959]---> BDD-cost:   12
c ---[1958]---> BDD-cost:   11
c ---[1957]---> BDD-cost:   11
c ---[1956]---> BDD-cost:   13
c ---[1955]---> BDD-cost:   13
c ---[1954]---> BDD-cost:   13
c ---[1952]---> BDD-cost:   13
c ---[1951]---> BDD-cost:   13
c ---[1949]---> BDD-cost:   13
c ---[1948]---> BDD-cost:   12
c ---[1947]---> BDD-cost:   12
c ---[1946]---> BDD-cost:   13
c ---[1945]---> BDD-cost:   12
c ---[1944]---> BDD-cost:   13
c ---[1943]---> BDD-cost:   12
c ---[1942]---> BDD-cost:   12
c ---[1941]---> BDD-cost:   13
c ---[1940]---> BDD-cost:   12
c ---[1939]---> BDD-cost:   11
c ---[1935]---> BDD-cost:   13
c ---[1934]---> BDD-cost:   12
c ---[1931]---> BDD-cost:   13
c ---[1930]---> BDD-cost:   12
c ---[1929]---> BDD-cost:   12
c ---[1926]---> BDD-cost:   13
c ---[1924]---> BDD-cost:   13
c ---[1923]---> BDD-cost:   12
c ---[1922]---> BDD-cost:   13
c ---[1921]---> BDD-cost:   12
c ---[1920]---> BDD-cost:   13
c ---[1919]---> BDD-cost:   12
c ---[1918]---> BDD-cost:   12
c ---[1917]---> BDD-cost:   13
c ---[1916]---> BDD-cost:   13
c ---[1915]---> BDD-cost:   13
c ---[1914]---> BDD-cost:   13
c ---[1913]---> BDD-cost:   12
c ---[1912]---> BDD-cost:   12
c ---[1911]---> BDD-cost:   13
c ---[1910]---> BDD-cost:   13
c ---[1909]---> BDD-cost:   12
c ---[1908]---> BDD-cost:   13
c ---[1907]---> BDD-cost:   12
c ---[1906]---> BDD-cost:   13
c ---[1905]---> BDD-cost:   13
c ---[1904]---> BDD-cost:   12
c ---[1903]---> BDD-cost:   13
c ---[1902]---> BDD-cost:   13
c ---[1901]---> BDD-cost:   11
c ---[1900]---> BDD-cost:   11
c ---[1899]---> BDD-cost:   13
c ---[1898]---> BDD-cost:   13
c ---[1897]---> BDD-cost:   12
c ---[1896]---> BDD-cost:   12
c ---[1895]---> BDD-cost:   12
c ---[1893]---> BDD-cost:   10
c ---[1892]---> BDD-cost:   13
c ---[1891]---> BDD-cost:   10
c ---[1890]---> BDD-cost:   13
c ---[1889]---> BDD-cost:   13
c ---[1888]---> BDD-cost:   13
c ---[1887]---> BDD-cost:   11
c ---[1886]---> BDD-cost:   13
c ---[1885]---> BDD-cost:   13
c ---[1883]---> BDD-cost:   12
c ---[1882]---> BDD-cost:   11
c ---[1881]---> BDD-cost:   13
c ---[1879]---> BDD-cost:   12
c ---[1878]---> BDD-cost:   13
c ---[1877]---> BDD-cost:   13
c ---[1875]---> BDD-cost:   13
c ---[1874]---> BDD-cost:   13
c ---[1872]---> BDD-cost:   10
c ---[1871]---> BDD-cost:   13
c ---[1869]---> BDD-cost:   13
c ---[1868]---> BDD-cost:   13
c ---[1867]---> BDD-cost:   13
c ---[1865]---> BDD-cost:   13
c ---[1862]---> BDD-cost:   11
c ---[1861]---> BDD-cost:   12
c ---[1860]---> BDD-cost:   13
c ---[1859]---> BDD-cost:   12
c ---[1858]---> BDD-cost:   13
c ---[1857]---> BDD-cost:   12
c ---[1856]---> BDD-cost:   11
c ---[1855]---> BDD-cost:   13
c ---[1854]---> BDD-cost:   12
c ---[1853]---> BDD-cost:   12
c ---[1851]---> BDD-cost:   12
c ---[1850]---> BDD-cost:   13
c ---[1849]---> BDD-cost:   11
c ---[1848]---> BDD-cost:   11
c ---[1847]---> BDD-cost:   13
c ---[1846]---> BDD-cost:   12
c ---[1845]---> BDD-cost:   12
c ---[1844]---> BDD-cost:   12
c ---[1843]---> BDD-cost:   13
c ---[1842]---> BDD-cost:   11
c ---[1841]---> BDD-cost:   13
c ---[1840]---> BDD-cost:   11
c ---[1839]---> BDD-cost:   12
c ---[1838]---> BDD-cost:   12
c ---[1837]---> BDD-cost:   13
c ---[1836]---> BDD-cost:   13
c ---[1833]---> BDD-cost:   13
c ---[1832]---> BDD-cost:   11
c ---[1831]---> BDD-cost:   12
c ---[1830]---> BDD-cost:   13
c ---[1829]---> BDD-cost:   11
c ---[1828]---> BDD-cost:   11
c ---[1825]---> BDD-cost:   13
c ---[1824]---> BDD-cost:   13
c ---[1823]---> BDD-cost:   13
c ---[1822]---> BDD-cost:   11
c ---[1821]---> BDD-cost:   13
c ---[1820]---> BDD-cost:   13
c ---[1819]---> BDD-cost:   12
c ---[1818]---> BDD-cost:   13
c ---[1817]---> BDD-cost:   11
c ---[1816]---> BDD-cost:   13
c ---[1814]---> BDD-cost:   12
c ---[1813]---> BDD-cost:   13
c ---[1811]---> BDD-cost:   13
c ---[1810]---> BDD-cost:   12
c ---[1809]---> BDD-cost:   11
c ---[1807]---> BDD-cost:   13
c ---[1806]---> BDD-cost:   12
c ---[1805]---> BDD-cost:   10
c ---[1804]---> BDD-cost:   11
c ---[1803]---> BDD-cost:   13
c ---[1802]---> BDD-cost:   13
c ---[1800]---> BDD-cost:   11
c ---[1799]---> BDD-cost:   13
c ---[1798]---> BDD-cost:   12
c ---[1797]---> BDD-cost:   13
c ---[1796]---> BDD-cost:   12
c ---[1795]---> BDD-cost:   12
c ---[1794]---> BDD-cost:   13
c ---[1793]---> BDD-cost:   13
c ---[1792]---> BDD-cost:   13
c ---[1791]---> BDD-cost:   13
c ---[1788]---> BDD-cost:   13
c ---[1786]---> BDD-cost:   12
c ---[1785]---> BDD-cost:   13
c ---[1783]---> BDD-cost:   11
c ---[1782]---> BDD-cost:   12
c ---[1781]---> BDD-cost:   12
c ---[1780]---> BDD-cost:   13
c ---[1779]---> BDD-cost:   13
c ---[1778]---> BDD-cost:   11
c ---[1777]---> BDD-cost:   13
c ---[1776]---> BDD-cost:   10
c ---[1775]---> BDD-cost:   13
c ---[1774]---> BDD-cost:   13
c ---[1773]---> BDD-cost:   13
c ---[1772]---> BDD-cost:   11
c ---[1771]---> BDD-cost:   13
c ---[1769]---> BDD-cost:   12
c ---[1766]---> BDD-cost:   13
c ---[1765]---> BDD-cost:   12
c ---[1764]---> BDD-cost:   13
c ---[1763]---> BDD-cost:   13
c ---[1762]---> BDD-cost:   11
c ---[1761]---> BDD-cost:   12
c ---[1760]---> BDD-cost:   13
c ---[1759]---> BDD-cost:   11
c ---[1758]---> BDD-cost:   12
c ---[1757]---> BDD-cost:   13
c ---[1755]---> BDD-cost:   13
c ---[1753]---> BDD-cost:   12
c ---[1752]---> BDD-cost:   13
c ---[1751]---> BDD-cost:   13
c ---[1750]---> BDD-cost:   12
c ---[1749]---> BDD-cost:   13
c ---[1748]---> BDD-cost:   13
c ---[1747]---> BDD-cost:   11
c ---[1746]---> BDD-cost:   13
c ---[1745]---> BDD-cost:   13
c ---[1744]---> BDD-cost:   13
c ---[1743]---> BDD-cost:   12
c ---[1741]---> BDD-cost:   12
c ---[1740]---> BDD-cost:   12
c ---[1739]---> BDD-cost:   13
c ---[1738]---> BDD-cost:   12
c ---[1737]---> BDD-cost:   12
c ---[1736]---> BDD-cost:   13
c ---[1735]---> BDD-cost:   13
c ---[1734]---> BDD-cost:   12
c ---[1732]---> BDD-cost:   12
c ---[1731]---> BDD-cost:   13
c ---[1730]---> BDD-cost:   13
c ---[1729]---> BDD-cost:   13
c ---[1728]---> BDD-cost:   13
c ---[1727]---> BDD-cost:   11
c ---[1725]---> BDD-cost:   13
c ---[1724]---> BDD-cost:   11
c ---[1723]---> BDD-cost:   12
c ---[1722]---> BDD-cost:   12
c ---[1721]---> BDD-cost:   11
c ---[1719]---> BDD-cost:   12
c ---[1717]---> BDD-cost:   13
c ---[1716]---> BDD-cost:   12
c ---[1715]---> BDD-cost:   13
c ---[1714]---> BDD-cost:   11
c ---[1713]---> BDD-cost:   12
c ---[1712]---> BDD-cost:   13
c ---[1711]---> BDD-cost:   12
c ---[1710]---> BDD-cost:   12
c ---[1709]---> BDD-cost:   13
c ---[1708]---> BDD-cost:   13
c ---[1707]---> BDD-cost:   12
c ---[1706]---> BDD-cost:   12
c ---[1705]---> BDD-cost:   13
c ---[1704]---> BDD-cost:   12
c ---[1702]---> BDD-cost:   71
c ---[1700]---> BDD-cost:   69
c ---[1699]---> BDD-cost:    7
c ---[1698]---> BDD-cost:    5
c ---[1697]---> BDD-cost:    8
c ---[1696]---> BDD-cost:    5
c ---[1695]---> BDD-cost:    6
c ---[1694]---> BDD-cost:    7
c ---[1693]---> BDD-cost:   14
c ---[1692]---> BDD-cost:    8
c ---[1691]---> BDD-cost:    7
c ---[1690]---> BDD-cost:    4
c ---[1689]---> BDD-cost:    7
c ---[1688]---> BDD-cost:    8
c ---[1687]---> BDD-cost:    6
c ---[1686]---> BDD-cost:    3
c ---[1685]---> BDD-cost:    7
c ---[1684]---> BDD-cost:    5
c ---[1683]---> BDD-cost:    7
c ---[1682]---> BDD-cost:   19
c ---[1681]---> BDD-cost:    6
c ---[1680]---> BDD-cost:    6
c ---[1679]---> BDD-cost:   16
c ---[1678]---> BDD-cost:    6
c ---[1677]---> BDD-cost:    8
c ---[1676]---> BDD-cost:    8
c ---[1675]---> BDD-cost:    6
c ---[1674]---> BDD-cost:    6
c ---[1673]---> BDD-cost:    5
c ---[1672]---> BDD-cost:    8
c ---[1671]---> BDD-cost:    7
c ---[1670]---> BDD-cost:   16
c ---[1669]---> BDD-cost:   17
c ---[1668]---> BDD-cost:   17
c ---[1667]---> BDD-cost:    7
c ---[1666]---> BDD-cost:    5
c ---[1665]---> BDD-cost:    5
c ---[1664]---> BDD-cost:    7
c ---[1663]---> BDD-cost:    5
c ---[1662]---> BDD-cost:    6
c ---[1661]---> BDD-cost:   14
c ---[1660]---> BDD-cost:    5
c ---[1659]---> BDD-cost:    8
c ---[1658]---> BDD-cost:    8
c ---[1657]---> BDD-cost:    4
c ---[1656]---> BDD-cost:    3
c ---[1655]---> BDD-cost:    8
c ---[1654]---> BDD-cost:    5
c ---[1653]---> BDD-cost:    6
c ---[1652]---> BDD-cost:    7
c ---[1651]---> BDD-cost:    6
c ---[1650]---> BDD-cost:    8
c ---[1649]---> BDD-cost:    4
c ---[1648]---> BDD-cost:   16
c ---[1647]---> BDD-cost:    3
c ---[1646]---> BDD-cost:   14
c ---[1645]---> BDD-cost:    7
c ---[1644]---> BDD-cost:   19
c ---[1643]---> BDD-cost:    8
c ---[1642]---> BDD-cost:    3
c ---[1641]---> BDD-cost:    5
c ---[1640]---> BDD-cost:    8
c ---[1639]---> BDD-cost:    7
c ---[1638]---> BDD-cost:    7
c ---[1637]---> BDD-cost:    5
c ---[1636]---> BDD-cost:    8
c ---[1635]---> BDD-cost:   19
c ---[1634]---> BDD-cost:    7
c ---[1633]---> BDD-cost:    8
c ---[1632]---> BDD-cost:    8
c ---[1631]---> BDD-cost:    6
c ---[1630]---> BDD-cost:    7
c ---[1629]---> BDD-cost:    5
c ---[1628]---> BDD-cost:    7
c ---[1627]---> BDD-cost:    6
c ---[1626]---> BDD-cost:    7
c ---[1625]---> BDD-cost:   14
c ---[1624]---> BDD-cost:    5
c ---[1623]---> BDD-cost:   14
c ---[1622]---> BDD-cost:    7
c ---[1621]---> BDD-cost:   19
c ---[1620]---> BDD-cost:    5
c ---[1619]---> BDD-cost:    8
c ---[1618]---> BDD-cost:    3
c ---[1617]---> BDD-cost:    8
c ---[1616]---> BDD-cost:    8
c ---[1615]---> BDD-cost:    6
c ---[1614]---> BDD-cost:    7
c ---[1613]---> BDD-cost:    6
c ---[1612]---> BDD-cost:    5
c ---[1611]---> BDD-cost:    4
c ---[1610]---> BDD-cost:   15
c ---[1609]---> BDD-cost:    6
c ---[1608]---> BDD-cost:    5
c ---[1607]---> BDD-cost:    6
c ---[1606]---> BDD-cost:    7
c ---[1605]---> BDD-cost:   17
c ---[1604]---> BDD-cost:   19
c ---[1603]---> BDD-cost:    6
c ---[1602]---> BDD-cost:    8
c ---[1601]---> BDD-cost:    6
c ---[1600]---> BDD-cost:    8
c ---[1599]---> BDD-cost:    7
c ---[1598]---> BDD-cost:    6
c ---[1597]---> BDD-cost:    7
c ---[1596]---> BDD-cost:    5
c ---[1595]---> BDD-cost:    8
c ---[1594]---> BDD-cost:    8
c ---[1593]---> BDD-cost:    7
c ---[1592]---> BDD-cost:    6
c ---[1591]---> BDD-cost:   15
c ---[1590]---> BDD-cost:    7
c ---[1588]---> BDD-cost:   73
c ---[1587]---> BDD-cost:    6
c ---[1586]---> BDD-cost:    8
c ---[1585]---> BDD-cost:    8
c ---[1584]---> BDD-cost:    7
c ---[1583]---> BDD-cost:    5
c ---[1582]---> BDD-cost:    8
c ---[1581]---> BDD-cost:    8
c ---[1580]---> BDD-cost:    6
c ---[1579]---> BDD-cost:    8
c ---[1578]---> BDD-cost:    4
c ---[1577]---> BDD-cost:    6
c ---[1576]---> BDD-cost:    6
c ---[1575]---> BDD-cost:   19
c ---[1574]---> BDD-cost:   19
c ---[1573]---> BDD-cost:    7
c ---[1572]---> BDD-cost:    6
c ---[1571]---> BDD-cost:    6
c ---[1570]---> BDD-cost:    8
c ---[1569]---> BDD-cost:    5
c ---[1568]---> BDD-cost:    7
c ---[1567]---> BDD-cost:    8
c ---[1566]---> BDD-cost:    7
c ---[1565]---> BDD-cost:    4
c ---[1564]---> BDD-cost:    8
c ---[1563]---> BDD-cost:    8
c ---[1562]---> BDD-cost:    5
c ---[1561]---> BDD-cost:    7
c ---[1560]---> BDD-cost:    3
c ---[1559]---> BDD-cost:    3
c ---[1558]---> BDD-cost:    8
c ---[1557]---> BDD-cost:    5
c ---[1556]---> BDD-cost:    8
c ---[1555]---> BDD-cost:    4
c ---[1554]---> BDD-cost:    4
c ---[1553]---> BDD-cost:    5
c ---[1552]---> BDD-cost:    6
c ---[1551]---> BDD-cost:    6
c ---[1550]---> BDD-cost:    8
c ---[1549]---> BDD-cost:    6
c ---[1548]---> BDD-cost:    6
c ---[1547]---> BDD-cost:    8
c ---[1546]---> BDD-cost:    5
c ---[1545]---> BDD-cost:    3
c ---[1544]---> BDD-cost:   19
c ---[1543]---> BDD-cost:    8
c ---[1542]---> BDD-cost:    5
c ---[1541]---> BDD-cost:   19
c ---[1540]---> BDD-cost:   19
c ---[1539]---> BDD-cost:    8
c ---[1538]---> BDD-cost:    8
c ---[1537]---> BDD-cost:    3
c ---[1536]---> BDD-cost:    8
c ---[1535]---> BDD-cost:    7
c ---[1534]---> BDD-cost:    6
c ---[1533]---> BDD-cost:    4
c ---[1532]---> BDD-cost:    7
c ---[1531]---> BDD-cost:    8
c ---[1530]---> BDD-cost:   15
c ---[1529]---> BDD-cost:    8
c ---[1528]---> BDD-cost:   17
c ---[1527]---> BDD-cost:    6
c ---[1526]---> BDD-cost:    4
c ---[1525]---> BDD-cost:    7
c ---[1524]---> BDD-cost:   19
c ---[1523]---> BDD-cost:    7
c ---[1522]---> BDD-cost:    7
c ---[1521]---> BDD-cost:    5
c ---[1520]---> BDD-cost:    8
c ---[1519]---> BDD-cost:    8
c ---[1518]---> BDD-cost:    6
c ---[1517]---> BDD-cost:    6
c ---[1516]---> BDD-cost:    8
c ---[1515]---> BDD-cost:    7
c ---[1514]---> BDD-cost:   19
c ---[1513]---> BDD-cost:    4
c ---[1512]---> BDD-cost:    6
c ---[1511]---> BDD-cost:    4
c ---[1510]---> BDD-cost:   15
c ---[1509]---> BDD-cost:    4
c ---[1508]---> BDD-cost:    8
c ---[1507]---> BDD-cost:    5
c ---[1506]---> BDD-cost:   18
c ---[1505]---> BDD-cost:    7
c ---[1504]---> BDD-cost:    6
c ---[1503]---> BDD-cost:    3
c ---[1502]---> BDD-cost:   17
c ---[1501]---> BDD-cost:    7
c ---[1500]---> BDD-cost:    3
c ---[1499]---> BDD-cost:    5
c ---[1498]---> BDD-cost:    7
c ---[1497]---> BDD-cost:    7
c ---[1496]---> BDD-cost:    8
c ---[1495]---> BDD-cost:   18
c ---[1494]---> BDD-cost:    7
c ---[1493]---> BDD-cost:    4
c ---[1492]---> BDD-cost:    8
c ---[1491]---> BDD-cost:    6
c ---[1490]---> BDD-cost:    5
c ---[1489]---> BDD-cost:    7
c ---[1488]---> BDD-cost:   16
c ---[1487]---> BDD-cost:    7
c ---[1486]---> BDD-cost:    6
c ---[1485]---> BDD-cost:   19
c ---[1484]---> BDD-cost:    6
c ---[1483]---> BDD-cost:    7
c ---[1482]---> BDD-cost:    7
c ---[1481]---> BDD-cost:    6
c ---[1480]---> BDD-cost:    5
c ---[1479]---> BDD-cost:    6
c ---[1478]---> BDD-cost:    3
c ---[1476]---> BDD-cost:   69
c ---[1475]---> BDD-cost:    5
c ---[1474]---> BDD-cost:    8
c ---[1473]---> BDD-cost:    6
c ---[1472]---> BDD-cost:    3
c ---[1471]---> BDD-cost:    5
c ---[1470]---> BDD-cost:    8
c ---[1469]---> BDD-cost:    6
c ---[1468]---> BDD-cost:   19
c ---[1467]---> BDD-cost:    5
c ---[1466]---> BDD-cost:    5
c ---[1465]---> BDD-cost:    8
c ---[1464]---> BDD-cost:    3
c ---[1463]---> BDD-cost:    7
c ---[1462]---> BDD-cost:    6
c ---[1461]---> BDD-cost:    7
c ---[1460]---> BDD-cost:    8
c ---[1459]---> BDD-cost:    7
c ---[1458]---> BDD-cost:   15
c ---[1457]---> BDD-cost:    6
c ---[1456]---> BDD-cost:    7
c ---[1455]---> BDD-cost:    4
c ---[1454]---> BDD-cost:    8
c ---[1453]---> BDD-cost:    7
c ---[1452]---> BDD-cost:    3
c ---[1451]---> BDD-cost:    5
c ---[1450]---> BDD-cost:    6
c ---[1449]---> BDD-cost:    6
c ---[1448]---> BDD-cost:    7
c ---[1447]---> BDD-cost:   18
c ---[1446]---> BDD-cost:    7
c ---[1445]---> BDD-cost:    6
c ---[1444]---> BDD-cost:    7
c ---[1443]---> BDD-cost:    8
c ---[1442]---> BDD-cost:    7
c ---[1441]---> BDD-cost:    3
c ---[1440]---> BDD-cost:    4
c ---[1439]---> BDD-cost:    8
c ---[1438]---> BDD-cost:    7
c ---[1437]---> BDD-cost:    5
c ---[1436]---> BDD-cost:    7
c ---[1435]---> BDD-cost:    6
c ---[1434]---> BDD-cost:    6
c ---[1433]---> BDD-cost:    5
c ---[1432]---> BDD-cost:    6
c ---[1431]---> BDD-cost:    7
c ---[1430]---> BDD-cost:    7
c ---[1429]---> BDD-cost:    7
c ---[1428]---> BDD-cost:   19
c ---[1427]---> BDD-cost:    6
c ---[1426]---> BDD-cost:    6
c ---[1425]---> BDD-cost:    4
c ---[1424]---> BDD-cost:    8
c ---[1423]---> BDD-cost:    6
c ---[1422]---> BDD-cost:    8
c ---[1421]---> BDD-cost:    8
c ---[1420]---> BDD-cost:    8
c ---[1419]---> BDD-cost:   17
c ---[1418]---> BDD-cost:    7
c ---[1417]---> BDD-cost:    3
c ---[1416]---> BDD-cost:   17
c ---[1415]---> BDD-cost:    3
c ---[1414]---> BDD-cost:    7
c ---[1413]---> BDD-cost:   16
c ---[1412]---> BDD-cost:    5
c ---[1411]---> BDD-cost:    5
c ---[1410]---> BDD-cost:    7
c ---[1409]---> BDD-cost:    7
c ---[1408]---> BDD-cost:    8
c ---[1407]---> BDD-cost:    8
c ---[1406]---> BDD-cost:    8
c ---[1405]---> BDD-cost:    5
c ---[1404]---> BDD-cost:    3
c ---[1403]---> BDD-cost:   19
c ---[1402]---> BDD-cost:    7
c ---[1401]---> BDD-cost:    6
c ---[1400]---> BDD-cost:    3
c ---[1399]---> BDD-cost:    6
c ---[1398]---> BDD-cost:    7
c ---[1397]---> BDD-cost:    8
c ---[1396]---> BDD-cost:    7
c ---[1395]---> BDD-cost:    7
c ---[1394]---> BDD-cost:    7
c ---[1393]---> BDD-cost:    6
c ---[1392]---> BDD-cost:    8
c ---[1391]---> BDD-cost:   15
c ---[1390]---> BDD-cost:    7
c ---[1389]---> BDD-cost:    7
c ---[1388]---> BDD-cost:    6
c ---[1387]---> BDD-cost:    7
c ---[1386]---> BDD-cost:   18
c ---[1385]---> BDD-cost:    7
c ---[1384]---> BDD-cost:    5
c ---[1383]---> BDD-cost:    7
c ---[1382]---> BDD-cost:    8
c ---[1381]---> BDD-cost:    7
c ---[1380]---> BDD-cost:    7
c ---[1379]---> BDD-cost:    8
c ---[1378]---> BDD-cost:    5
c ---[1377]---> BDD-cost:    7
c ---[1376]---> BDD-cost:    6
c ---[1375]---> BDD-cost:    6
c ---[1374]---> BDD-cost:    6
c ---[1373]---> BDD-cost:   19
c ---[1372]---> BDD-cost:    6
c ---[1371]---> BDD-cost:    7
c ---[1370]---> BDD-cost:    6
c ---[1369]---> BDD-cost:    7
c ---[1368]---> BDD-cost:   16
c ---[1367]---> BDD-cost:   18
c ---[1366]---> BDD-cost:   19
c ---[1364]---> BDD-cost:   65
c ---[1363]---> BDD-cost:    8
c ---[1362]---> BDD-cost:    6
c ---[1361]---> BDD-cost:   18
c ---[1360]---> BDD-cost:    3
c ---[1359]---> BDD-cost:   17
c ---[1358]---> BDD-cost:    7
c ---[1357]---> BDD-cost:    8
c ---[1356]---> BDD-cost:    8
c ---[1355]---> BDD-cost:    7
c ---[1354]---> BDD-cost:    7
c ---[1353]---> BDD-cost:   19
c ---[1352]---> BDD-cost:    3
c ---[1351]---> BDD-cost:    4
c ---[1350]---> BDD-cost:    8
c ---[1349]---> BDD-cost:   16
c ---[1348]---> BDD-cost:    8
c ---[1347]---> BDD-cost:    7
c ---[1346]---> BDD-cost:    8
c ---[1345]---> BDD-cost:    6
c ---[1344]---> BDD-cost:    5
c ---[1343]---> BDD-cost:    6
c ---[1342]---> BDD-cost:    8
c ---[1341]---> BDD-cost:    6
c ---[1340]---> BDD-cost:    8
c ---[1339]---> BDD-cost:    6
c ---[1338]---> BDD-cost:    8
c ---[1337]---> BDD-cost:    8
c ---[1336]---> BDD-cost:    5
c ---[1335]---> BDD-cost:    6
c ---[1334]---> BDD-cost:    6
c ---[1333]---> BDD-cost:   15
c ---[1332]---> BDD-cost:    4
c ---[1331]---> BDD-cost:    7
c ---[1330]---> BDD-cost:    8
c ---[1329]---> BDD-cost:    6
c ---[1328]---> BDD-cost:    7
c ---[1327]---> BDD-cost:    6
c ---[1326]---> BDD-cost:    3
c ---[1325]---> BDD-cost:    6
c ---[1324]---> BDD-cost:    3
c ---[1323]---> BDD-cost:    5
c ---[1322]---> BDD-cost:    3
c ---[1321]---> BDD-cost:    7
c ---[1320]---> BDD-cost:    3
c ---[1319]---> BDD-cost:    6
c ---[1318]---> BDD-cost:    7
c ---[1317]---> BDD-cost:    3
c ---[1316]---> BDD-cost:    3
c ---[1315]---> BDD-cost:    6
c ---[1314]---> BDD-cost:    6
c ---[1313]---> BDD-cost:    6
c ---[1312]---> BDD-cost:    6
c ---[1311]---> BDD-cost:    8
c ---[1310]---> BDD-cost:    7
c ---[1309]---> BDD-cost:    7
c ---[1308]---> BDD-cost:    6
c ---[1307]---> BDD-cost:    7
c ---[1306]---> BDD-cost:    7
c ---[1305]---> BDD-cost:    8
c ---[1304]---> BDD-cost:    6
c ---[1303]---> BDD-cost:    3
c ---[1302]---> BDD-cost:    7
c ---[1301]---> BDD-cost:    7
c ---[1300]---> BDD-cost:    5
c ---[1299]---> BDD-cost:    6
c ---[1298]---> BDD-cost:   16
c ---[1297]---> BDD-cost:    5
c ---[1296]---> BDD-cost:    5
c ---[1295]---> BDD-cost:    5
c ---[1294]---> BDD-cost:    8
c ---[1293]---> BDD-cost:    7
c ---[1292]---> BDD-cost:   17
c ---[1291]---> BDD-cost:    6
c ---[1290]---> BDD-cost:    8
c ---[1289]---> BDD-cost:   17
c ---[1288]---> BDD-cost:   17
c ---[1287]---> BDD-cost:   19
c ---[1286]---> BDD-cost:    8
c ---[1285]---> BDD-cost:    8
c ---[1284]---> BDD-cost:    6
c ---[1283]---> BDD-cost:    5
c ---[1282]---> BDD-cost:    5
c ---[1281]---> BDD-cost:    8
c ---[1280]---> BDD-cost:    6
c ---[1279]---> BDD-cost:    8
c ---[1278]---> BDD-cost:    5
c ---[1277]---> BDD-cost:   19
c ---[1276]---> BDD-cost:   19
c ---[1275]---> BDD-cost:    5
c ---[1274]---> BDD-cost:   15
c ---[1273]---> BDD-cost:    8
c ---[1272]---> BDD-cost:    8
c ---[1271]---> BDD-cost:    7
c ---[1270]---> BDD-cost:    6
c ---[1269]---> BDD-cost:    3
c ---[1268]---> BDD-cost:    8
c ---[1267]---> BDD-cost:    7
c ---[1266]---> BDD-cost:    7
c ---[1265]---> BDD-cost:    5
c ---[1264]---> BDD-cost:    6
c ---[1263]---> BDD-cost:    4
c ---[1262]---> BDD-cost:    7
c ---[1261]---> BDD-cost:   17
c ---[1260]---> BDD-cost:    7
c ---[1259]---> BDD-cost:    7
c ---[1258]---> BDD-cost:    4
c ---[1257]---> BDD-cost:   17
c ---[1256]---> BDD-cost:    6
c ---[1255]---> BDD-cost:    7
c ---[1254]---> BDD-cost:    8
c ---[1252]---> BDD-cost:   73
c ---[1251]---> BDD-cost:   19
c ---[1250]---> BDD-cost:   19
c ---[1249]---> BDD-cost:    3
c ---[1248]---> BDD-cost:    6
c ---[1247]---> BDD-cost:    8
c ---[1246]---> BDD-cost:    3
c ---[1245]---> BDD-cost:    6
c ---[1244]---> BDD-cost:    7
c ---[1243]---> BDD-cost:   17
c ---[1242]---> BDD-cost:    7
c ---[1241]---> BDD-cost:    5
c ---[1240]---> BDD-cost:    8
c ---[1239]---> BDD-cost:    3
c ---[1238]---> BDD-cost:    8
c ---[1237]---> BDD-cost:    8
c ---[1236]---> BDD-cost:    7
c ---[1235]---> BDD-cost:    6
c ---[1234]---> BDD-cost:    6
c ---[1233]---> BDD-cost:   19
c ---[1232]---> BDD-cost:    7
c ---[1231]---> BDD-cost:    8
c ---[1230]---> BDD-cost:    7
c ---[1229]---> BDD-cost:    5
c ---[1228]---> BDD-cost:    6
c ---[1227]---> BDD-cost:    8
c ---[1226]---> BDD-cost:   19
c ---[1225]---> BDD-cost:   15
c ---[1224]---> BDD-cost:    8
c ---[1223]---> BDD-cost:    6
c ---[1222]---> BDD-cost:    6
c ---[1221]---> BDD-cost:    8
c ---[1220]---> BDD-cost:    3
c ---[1219]---> BDD-cost:    6
c ---[1218]---> BDD-cost:    6
c ---[1217]---> BDD-cost:    6
c ---[1216]---> BDD-cost:    7
c ---[1215]---> BDD-cost:    8
c ---[1214]---> BDD-cost:    6
c ---[1213]---> BDD-cost:    6
c ---[1212]---> BDD-cost:    8
c ---[1211]---> BDD-cost:   15
c ---[1210]---> BDD-cost:    5
c ---[1209]---> BDD-cost:    5
c ---[1208]---> BDD-cost:    8
c ---[1207]---> BDD-cost:    7
c ---[1206]---> BDD-cost:   17
c ---[1205]---> BDD-cost:    6
c ---[1204]---> BDD-cost:    7
c ---[1203]---> BDD-cost:    8
c ---[1202]---> BDD-cost:    7
c ---[1201]---> BDD-cost:    8
c ---[1200]---> BDD-cost:    8
c ---[1199]---> BDD-cost:    6
c ---[1197]---> BDD-cost:   67
c ---[1196]---> BDD-cost:    6
c ---[1195]---> BDD-cost:    6
c ---[1194]---> BDD-cost:    5
c ---[1193]---> BDD-cost:    6
c ---[1192]---> BDD-cost:   17
c ---[1191]---> BDD-cost:   16
c ---[1190]---> BDD-cost:    8
c ---[1189]---> BDD-cost:    5
c ---[1188]---> BDD-cost:    3
c ---[1187]---> BDD-cost:    8
c ---[1185]---> BDD-cost:   65
c ---[1184]---> BDD-cost:    6
c ---[1183]---> BDD-cost:    7
c ---[1182]---> BDD-cost:    7
c ---[1181]---> BDD-cost:    5
c ---[1180]---> BDD-cost:    6
c ---[1179]---> BDD-cost:    6
c ---[1178]---> BDD-cost:    7
c ---[1177]---> BDD-cost:   15
c ---[1176]---> BDD-cost:    6
c ---[1175]---> BDD-cost:    6
c ---[1173]---> BDD-cost:   65
c ---[1172]---> BDD-cost:    4
c ---[1171]---> BDD-cost:    8
c ---[1170]---> BDD-cost:    3
c ---[1169]---> BDD-cost:    8
c ---[1168]---> BDD-cost:    7
c ---[1167]---> BDD-cost:   15
c ---[1166]---> BDD-cost:    5
c ---[1165]---> BDD-cost:    6
c ---[1164]---> BDD-cost:    7
c ---[1163]---> BDD-cost:    4
c ---[1161]---> BDD-cost:   67
c ---[1160]---> BDD-cost:   17
c ---[1159]---> BDD-cost:    7
c ---[1158]---> BDD-cost:    6
c ---[1157]---> BDD-cost:   19
c ---[1156]---> BDD-cost:    7
c ---[1155]---> BDD-cost:    3
c ---[1154]---> BDD-cost:    6
c ---[1153]---> BDD-cost:   19
c ---[1152]---> BDD-cost:    3
c ---[1151]---> BDD-cost:    7
c ---[1149]---> BDD-cost:   67
c ---[1148]---> BDD-cost:    7
c ---[1147]---> BDD-cost:    3
c ---[1146]---> BDD-cost:    3
c ---[1145]---> BDD-cost:   15
c ---[1144]---> BDD-cost:    7
c ---[1143]---> BDD-cost:   15
c ---[1142]---> BDD-cost:    5
c ---[1141]---> BDD-cost:    8
c ---[1140]---> BDD-cost:   14
c ---[1139]---> BDD-cost:    6
c ---[1137]---> BDD-cost:   71
c ---[1135]---> BDD-cost:   65
c ---[1134]---> BDD-cost:   15
c ---[1133]---> BDD-cost:    7
c ---[1132]---> BDD-cost:    8
c ---[1131]---> BDD-cost:    8
c ---[1130]---> BDD-cost:    5
c ---[1129]---> BDD-cost:    7
c ---[1128]---> BDD-cost:    7
c ---[1127]---> BDD-cost:    7
c ---[1126]---> BDD-cost:    5
c ---[1125]---> BDD-cost:    3
c ---[1123]---> BDD-cost:   69
c ---[1122]---> BDD-cost:    7
c ---[1121]---> BDD-cost:   15
c ---[1120]---> BDD-cost:    8
c ---[1119]---> BDD-cost:    5
c ---[1118]---> BDD-cost:    3
c ---[1117]---> BDD-cost:    6
c ---[1116]---> BDD-cost:    3
c ---[1115]---> BDD-cost:    4
c ---[1114]---> BDD-cost:    6
c ---[1113]---> BDD-cost:    5
c ---[1111]---> BDD-cost:   69
c ---[1110]---> BDD-cost:    7
c ---[1109]---> BDD-cost:    5
c ---[1108]---> BDD-cost:    7
c ---[1107]---> BDD-cost:    8
c ---[1106]---> BDD-cost:    5
c ---[1105]---> BDD-cost:    5
c ---[1104]---> BDD-cost:    6
c ---[1103]---> BDD-cost:    7
c ---[1102]---> BDD-cost:    6
c ---[1101]---> BDD-cost:    7
c ---[1099]---> BDD-cost:   69
c ---[1098]---> BDD-cost:    7
c ---[1097]---> BDD-cost:    4
c ---[1096]---> BDD-cost:    7
c ---[1095]---> BDD-cost:    3
c ---[1094]---> BDD-cost:   18
c ---[1093]---> BDD-cost:    8
c ---[1092]---> BDD-cost:    5
c ---[1091]---> BDD-cost:    4
c ---[1090]---> BDD-cost:    6
c ---[1089]---> BDD-cost:    4
c ---[1087]---> BDD-cost:   67
c ---[1086]---> BDD-cost:    7
c ---[1085]---> BDD-cost:    6
c ---[1084]---> BDD-cost:    6
c ---[1083]---> BDD-cost:   17
c ---[1082]---> BDD-cost:    8
c ---[1081]---> BDD-cost:   19
c ---[1080]---> BDD-cost:    5
c ---[1079]---> BDD-cost:    5
c ---[1078]---> BDD-cost:   17
c ---[1077]---> BDD-cost:    3
c ---[1075]---> BDD-cost:   63
c ---[1074]---> BDD-cost:    8
c ---[1073]---> BDD-cost:    5
c ---[1072]---> BDD-cost:    7
c ---[1071]---> BDD-cost:    6
c ---[1070]---> BDD-cost:    7
c ---[1069]---> BDD-cost:    8
c ---[1068]---> BDD-cost:   16
c ---[1067]---> BDD-cost:    7
c ---[1066]---> BDD-cost:    6
c ---[1065]---> BDD-cost:    7
c ---[1063]---> BDD-cost:   65
c ---[1062]---> BDD-cost:    7
c ---[1061]---> BDD-cost:    7
c ---[1060]---> BDD-cost:    6
c ---[1059]---> BDD-cost:    7
c ---[1058]---> BDD-cost:    7
c ---[1057]---> BDD-cost:    7
c ---[1056]---> BDD-cost:    6
c ---[1055]---> BDD-cost:    7
c ---[1054]---> BDD-cost:    7
c ---[1053]---> BDD-cost:    7
c ---[1051]---> BDD-cost:   63
c ---[1050]---> BDD-cost:    7
c ---[1049]---> BDD-cost:    7
c ---[1048]---> BDD-cost:    7
c ---[1047]---> BDD-cost:    3
c ---[1046]---> BDD-cost:    8
c ---[1045]---> BDD-cost:    4
c ---[1044]---> BDD-cost:   18
c ---[1043]---> BDD-cost:    4
c ---[1042]---> BDD-cost:    8
c ---[1041]---> BDD-cost:    7
c ---[1039]---> BDD-cost:   63
c ---[1038]---> BDD-cost:   18
c ---[1037]---> BDD-cost:    4
c ---[1036]---> BDD-cost:    7
c ---[1035]---> BDD-cost:    7
c ---[1034]---> BDD-cost:    5
c ---[1033]---> BDD-cost:    5
c ---[1032]---> BDD-cost:    6
c ---[1031]---> BDD-cost:    8
c ---[1030]---> BDD-cost:   16
c ---[1029]---> BDD-cost:   19
c ---[1027]---> BDD-cost:   71
c ---[1026]---> BDD-cost:    6
c ---[1025]---> BDD-cost:    7
c ---[1024]---> BDD-cost:    3
c ---[1023]---> BDD-cost:   19
c ---[1022]---> BDD-cost:    8
c ---[1021]---> BDD-cost:    8
c ---[1020]---> BDD-cost:    6
c ---[1019]---> BDD-cost:    3
c ---[1018]---> BDD-cost:   16
c ---[1017]---> BDD-cost:    8
c ---[1015]---> BDD-cost:   69
c ---[1013]---> BDD-cost:   67
c ---[1012]---> BDD-cost:    4
c ---[1011]---> BDD-cost:    6
c ---[1010]---> BDD-cost:    8
c ---[1009]---> BDD-cost:    8
c ---[1008]---> BDD-cost:    8
c ---[1007]---> BDD-cost:    7
c ---[1006]---> BDD-cost:    7
c ---[1005]---> BDD-cost:    7
c ---[1004]---> BDD-cost:    8
c ---[1003]---> BDD-cost:    4
c ---[1001]---> BDD-cost:   65
c ---[1000]---> BDD-cost:    8
c ---[ 999]---> BDD-cost:    7
c ---[ 998]---> BDD-cost:    7
c ---[ 997]---> BDD-cost:    8
c ---[ 996]---> BDD-cost:    7
c ---[ 995]---> BDD-cost:    7
c ---[ 994]---> BDD-cost:    7
c ---[ 993]---> BDD-cost:    3
c ---[ 992]---> BDD-cost:    7
c ---[ 991]---> BDD-cost:    6
c ---[ 989]---> BDD-cost:   71
c ---[ 988]---> BDD-cost:    3
c ---[ 987]---> BDD-cost:    6
c ---[ 986]---> BDD-cost:    8
c ---[ 985]---> BDD-cost:    6
c ---[ 984]---> BDD-cost:    7
c ---[ 983]---> BDD-cost:    7
c ---[ 982]---> BDD-cost:    6
c ---[ 981]---> BDD-cost:   17
c ---[ 980]---> BDD-cost:    7
c ---[ 979]---> BDD-cost:    6
c ---[ 977]---> BDD-cost:   73
c ---[ 976]---> BDD-cost:    3
c ---[ 975]---> BDD-cost:    5
c ---[ 974]---> BDD-cost:    5
c ---[ 973]---> BDD-cost:    6
c ---[ 972]---> BDD-cost:    5
c ---[ 971]---> BDD-cost:    8
c ---[ 970]---> BDD-cost:   17
c ---[ 969]---> BDD-cost:   17
c ---[ 968]---> BDD-cost:    8
c ---[ 967]---> BDD-cost:    5
c ---[ 965]---> BDD-cost:   71
c ---[ 964]---> BDD-cost:    6
c ---[ 963]---> BDD-cost:    6
c ---[ 962]---> BDD-cost:    5
c ---[ 961]---> BDD-cost:    8
c ---[ 960]---> BDD-cost:    6
c ---[ 959]---> BDD-cost:    6
c ---[ 958]---> BDD-cost:    3
c ---[ 957]---> BDD-cost:    6
c ---[ 956]---> BDD-cost:    6
c ---[ 955]---> BDD-cost:    7
c ---[ 953]---> BDD-cost:   69
c ---[ 952]---> BDD-cost:    7
c ---[ 951]---> BDD-cost:    5
c ---[ 950]---> BDD-cost:    7
c ---[ 949]---> BDD-cost:    8
c ---[ 948]---> BDD-cost:    6
c ---[ 947]---> BDD-cost:    5
c ---[ 946]---> BDD-cost:    8
c ---[ 945]---> BDD-cost:    8
c ---[ 944]---> BDD-cost:    3
c ---[ 943]---> BDD-cost:    6
c ---[ 941]---> BDD-cost:   67
c ---[ 940]---> BDD-cost:    6
c ---[ 939]---> BDD-cost:    8
c ---[ 938]---> BDD-cost:    7
c ---[ 937]---> BDD-cost:    8
c ---[ 936]---> BDD-cost:   19
c ---[ 935]---> BDD-cost:    7
c ---[ 934]---> BDD-cost:    5
c ---[ 933]---> BDD-cost:   15
c ---[ 932]---> BDD-cost:    7
c ---[ 931]---> BDD-cost:    8
c ---[ 929]---> BDD-cost:   63
c ---[ 928]---> BDD-cost:    8
c ---[ 927]---> BDD-cost:    8
c ---[ 926]---> BDD-cost:    5
c ---[ 925]---> BDD-cost:    3
c ---[ 924]---> BDD-cost:   17
c ---[ 923]---> BDD-cost:   19
c ---[ 922]---> BDD-cost:    3
c ---[ 921]---> BDD-cost:    8
c ---[ 920]---> BDD-cost:    7
c ---[ 919]---> BDD-cost:   19
c ---[ 917]---> BDD-cost:   63
c ---[ 916]---> BDD-cost:    3
c ---[ 915]---> BDD-cost:    7
c ---[ 914]---> BDD-cost:    6
c ---[ 913]---> BDD-cost:    6
c ---[ 912]---> BDD-cost:    8
c ---[ 911]---> BDD-cost:    3
c ---[ 910]---> BDD-cost:    7
c ---[ 909]---> BDD-cost:    7
c ---[ 908]---> BDD-cost:    8
c ---[ 907]---> BDD-cost:    7
c ---[ 905]---> BDD-cost:   57
c ---[ 904]---> BDD-cost:    4
c ---[ 903]---> BDD-cost:    4
c ---[ 902]---> BDD-cost:    7
c ---[ 901]---> BDD-cost:    6
c ---[ 900]---> BDD-cost:    6
c ---[ 899]---> BDD-cost:    5
c ---[ 898]---> BDD-cost:   17
c ---[ 897]---> BDD-cost:    7
c ---[ 896]---> BDD-cost:   14
c ---[ 895]---> BDD-cost:    7
c ---[ 893]---> BDD-cost:   57
c ---[ 891]---> Adder-cost: 1754   maxlim: 361947   bits: 20/19
c ---[ 890]---> BDD-cost:    8
c ---[ 889]---> BDD-cost:    6
c ---[ 888]---> BDD-cost:    7
c ---[ 887]---> BDD-cost:    7
c ---[ 886]---> BDD-cost:    8
c ---[ 885]---> BDD-cost:    8
c ---[ 884]---> BDD-cost:    3
c ---[ 883]---> BDD-cost:   18
c ---[ 882]---> BDD-cost:    8
c ---[ 881]---> BDD-cost:    7
c ---[ 879]---> Adder-cost: 1886   maxlim: 393051   bits: 20/19
c ---[ 878]---> BDD-cost:    4
c ---[ 877]---> BDD-cost:   18
c ---[ 876]---> BDD-cost:    5
c ---[ 875]---> BDD-cost:    3
c ---[ 874]---> BDD-cost:    5
c ---[ 873]---> BDD-cost:    7
c ---[ 872]---> BDD-cost:    8
c ---[ 871]---> BDD-cost:    7
c ---[ 870]---> BDD-cost:    6
c ---[ 869]---> BDD-cost:    5
c ---[ 867]---> Adder-cost: 1892   maxlim: 407260   bits: 20/19
c ---[ 866]---> BDD-cost:    6
c ---[ 865]---> BDD-cost:    3
c ---[ 864]---> BDD-cost:    3
c ---[ 863]---> BDD-cost:    3
c ---[ 862]---> BDD-cost:   17
c ---[ 861]---> BDD-cost:    6
c ---[ 860]---> BDD-cost:    3
c ---[ 859]---> BDD-cost:    8
c ---[ 858]---> BDD-cost:   16
c ---[ 857]---> BDD-cost:   16
c ---[ 855]---> Adder-cost: 1620   maxlim: 292194   bits: 20/19
c ---[ 854]---> BDD-cost:    7
c ---[ 853]---> BDD-cost:    8
c ---[ 852]---> BDD-cost:    8
c ---[ 851]---> BDD-cost:    5
c ---[ 850]---> BDD-cost:   15
c ---[ 849]---> BDD-cost:    5
c ---[ 848]---> BDD-cost:   19
c ---[ 847]---> BDD-cost:    7
c ---[ 846]---> BDD-cost:    8
c ---[ 845]---> BDD-cost:    6
c ---[ 843]---> Adder-cost: 1716   maxlim: 400605   bits: 20/19
c ---[ 842]---> BDD-cost:    8
c ---[ 841]---> BDD-cost:    6
c ---[ 840]---> BDD-cost:    8
c ---[ 839]---> BDD-cost:    6
c ---[ 838]---> BDD-cost:    7
c ---[ 837]---> BDD-cost:    3
c ---[ 836]---> BDD-cost:    7
c ---[ 835]---> BDD-cost:    5
c ---[ 834]---> BDD-cost:    7
c ---[ 833]---> BDD-cost:   18
c ---[ 831]---> Adder-cost: 1880   maxlim: 441181   bits: 20/19
c ---[ 830]---> BDD-cost:    5
c ---[ 829]---> BDD-cost:    7
c ---[ 828]---> BDD-cost:    3
c ---[ 827]---> BDD-cost:   18
c ---[ 826]---> BDD-cost:    4
c ---[ 825]---> BDD-cost:    6
c ---[ 824]---> BDD-cost:   19
c ---[ 823]---> BDD-cost:    5
c ---[ 822]---> BDD-cost:   16
c ---[ 821]---> BDD-cost:    5
c ---[ 819]---> Adder-cost: 1650   maxlim: 327391   bits: 20/19
c ---[ 818]---> BDD-cost:    7
c ---[ 817]---> BDD-cost:    8
c ---[ 816]---> BDD-cost:    7
c ---[ 815]---> BDD-cost:    5
c ---[ 814]---> BDD-cost:    7
c ---[ 813]---> BDD-cost:    7
c ---[ 812]---> BDD-cost:    7
c ---[ 811]---> BDD-cost:    8
c ---[ 810]---> BDD-cost:    6
c ---[ 809]---> BDD-cost:    3
c ---[ 807]---> Adder-cost: 1934   maxlim: 418779   bits: 20/19
c ---[ 806]---> BDD-cost:    5
c ---[ 805]---> BDD-cost:    7
c ---[ 804]---> BDD-cost:    3
c ---[ 803]---> BDD-cost:   15
c ---[ 802]---> BDD-cost:    5
c ---[ 801]---> BDD-cost:    4
c ---[ 800]---> BDD-cost:    7
c ---[ 799]---> BDD-cost:    7
c ---[ 798]---> BDD-cost:    7
c ---[ 797]---> BDD-cost:   17
c ---[ 795]---> Adder-cost: 1654   maxlim: 324318   bits: 20/19
c ---[ 794]---> BDD-cost:    7
c ---[ 793]---> BDD-cost:    8
c ---[ 792]---> BDD-cost:   15
c ---[ 791]---> BDD-cost:    7
c ---[ 790]---> BDD-cost:    7
c ---[ 789]---> BDD-cost:    6
c ---[ 788]---> BDD-cost:    3
c ---[ 787]---> BDD-cost:    8
c ---[ 786]---> BDD-cost:    5
c ---[ 785]---> BDD-cost:    5
c ---[ 783]---> Adder-cost: 1880   maxlim: 361692   bits: 20/19
c ---[ 782]---> BDD-cost:    8
c ---[ 781]---> BDD-cost:    7
c ---[ 780]---> BDD-cost:   15
c ---[ 779]---> BDD-cost:    7
c ---[ 778]---> BDD-cost:    3
c ---[ 777]---> BDD-cost:    7
c ---[ 776]---> BDD-cost:    6
c ---[ 775]---> BDD-cost:    7
c ---[ 774]---> BDD-cost:    5
c ---[ 773]---> BDD-cost:   16
c ---[ 771]---> BDD-cost:   67
c ---[ 769]---> Adder-cost: 1756   maxlim: 412890   bits: 20/19
c ---[ 768]---> BDD-cost:    7
c ---[ 767]---> BDD-cost:    7
c ---[ 766]---> BDD-cost:    8
c ---[ 765]---> BDD-cost:    7
c ---[ 764]---> BDD-cost:    4
c ---[ 763]---> BDD-cost:    6
c ---[ 762]---> BDD-cost:    6
c ---[ 761]---> BDD-cost:    5
c ---[ 760]---> BDD-cost:    7
c ---[ 759]---> BDD-cost:    3
c ---[ 757]---> Adder-cost: 1806   maxlim: 375900   bits: 20/19
c ---[ 756]---> BDD-cost:    6
c ---[ 755]---> BDD-cost:   18
c ---[ 754]---> BDD-cost:    6
c ---[ 753]---> BDD-cost:    7
c ---[ 752]---> BDD-cost:    6
c ---[ 751]---> BDD-cost:    5
c ---[ 750]---> BDD-cost:    7
c ---[ 749]---> BDD-cost:    5
c ---[ 748]---> BDD-cost:    8
c ---[ 747]---> BDD-cost:    4
c ---[ 745]---> Adder-cost: 1784   maxlim: 382686   bits: 20/19
c ---[ 744]---> BDD-cost:    7
c ---[ 743]---> BDD-cost:    5
c ---[ 742]---> BDD-cost:    4
c ---[ 741]---> BDD-cost:    6
c ---[ 740]---> BDD-cost:    8
c ---[ 739]---> BDD-cost:    5
c ---[ 738]---> BDD-cost:    5
c ---[ 737]---> BDD-cost:    8
c ---[ 736]---> BDD-cost:    7
c ---[ 735]---> BDD-cost:    6
c ---[ 733]---> Adder-cost: 1754   maxlim: 367962   bits: 20/19
c ---[ 732]---> BDD-cost:    3
c ---[ 731]---> BDD-cost:    6
c ---[ 730]---> BDD-cost:   15
c ---[ 729]---> BDD-cost:    8
c ---[ 728]---> BDD-cost:    8
c ---[ 727]---> BDD-cost:    5
c ---[ 726]---> BDD-cost:    7
c ---[ 725]---> BDD-cost:    6
c ---[ 724]---> BDD-cost:    8
c ---[ 723]---> BDD-cost:    8
c ---[ 721]---> Adder-cost: 1792   maxlim: 372061   bits: 20/19
c ---[ 720]---> BDD-cost:    8
c ---[ 719]---> BDD-cost:   17
c ---[ 718]---> BDD-cost:   19
c ---[ 717]---> BDD-cost:    6
c ---[ 716]---> BDD-cost:   15
c ---[ 715]---> BDD-cost:   15
c ---[ 714]---> BDD-cost:    8
c ---[ 713]---> BDD-cost:    3
c ---[ 712]---> BDD-cost:    7
c ---[ 711]---> BDD-cost:    6
c ---[ 709]---> Adder-cost: 1648   maxlim: 339038   bits: 20/19
c ---[ 708]---> BDD-cost:    8
c ---[ 707]---> BDD-cost:   19
c ---[ 706]---> BDD-cost:    8
c ---[ 705]---> BDD-cost:    5
c ---[ 704]---> BDD-cost:    3
c ---[ 703]---> BDD-cost:   16
c ---[ 702]---> BDD-cost:    5
c ---[ 701]---> BDD-cost:    7
c ---[ 700]---> BDD-cost:    6
c ---[ 699]---> BDD-cost:    5
c ---[ 697]---> Adder-cost: 1748   maxlim: 336990   bits: 20/19
c ---[ 696]---> BDD-cost:   16
c ---[ 695]---> BDD-cost:    8
c ---[ 694]---> BDD-cost:   14
c ---[ 693]---> BDD-cost:    7
c ---[ 692]---> BDD-cost:    4
c ---[ 691]---> BDD-cost:    6
c ---[ 690]---> BDD-cost:    7
c ---[ 689]---> BDD-cost:    8
c ---[ 688]---> BDD-cost:    7
c ---[ 687]---> BDD-cost:    5
c ---[ 685]---> Adder-cost: 1868   maxlim: 363997   bits: 20/19
c ---[ 684]---> BDD-cost:    4
c ---[ 683]---> BDD-cost:    7
c ---[ 682]---> BDD-cost:    4
c ---[ 681]---> BDD-cost:   19
c ---[ 680]---> BDD-cost:    6
c ---[ 679]---> BDD-cost:    6
c ---[ 678]---> BDD-cost:    8
c ---[ 677]---> BDD-cost:    7
c ---[ 676]---> BDD-cost:    4
c ---[ 675]---> BDD-cost:    6
c ---[ 673]---> Adder-cost: 1862   maxlim: 388829   bits: 20/19
c ---[ 672]---> BDD-cost:    6
c ---[ 671]---> BDD-cost:   19
c ---[ 670]---> BDD-cost:   15
c ---[ 669]---> BDD-cost:    5
c ---[ 668]---> BDD-cost:    6
c ---[ 667]---> BDD-cost:   19
c ---[ 666]---> BDD-cost:    5
c ---[ 665]---> BDD-cost:    7
c ---[ 664]---> BDD-cost:    7
c ---[ 663]---> BDD-cost:    6
c ---[ 661]---> Adder-cost: 1812   maxlim: 376286   bits: 20/19
c ---[ 660]---> BDD-cost:    6
c ---[ 659]---> BDD-cost:    8
c ---[ 658]---> BDD-cost:    7
c ---[ 657]---> BDD-cost:   19
c ---[ 656]---> BDD-cost:    5
c ---[ 655]---> BDD-cost:    8
c ---[ 654]---> BDD-cost:    7
c ---[ 653]---> BDD-cost:    4
c ---[ 652]---> BDD-cost:    8
c ---[ 651]---> BDD-cost:    7
c ---[ 649]---> BDD-cost:   67
c ---[ 647]---> Adder-cost: 1776   maxlim: 416732   bits: 20/19
c ---[ 646]---> BDD-cost:    7
c ---[ 645]---> BDD-cost:    4
c ---[ 644]---> BDD-cost:    6
c ---[ 643]---> BDD-cost:    8
c ---[ 642]---> BDD-cost:    6
c ---[ 641]---> BDD-cost:    8
c ---[ 640]---> BDD-cost:    7
c ---[ 639]---> BDD-cost:    4
c ---[ 638]---> BDD-cost:    7
c ---[ 637]---> BDD-cost:    7
c ---[ 635]---> Adder-cost: 1774   maxlim: 382300   bits: 20/19
c ---[ 634]---> BDD-cost:    5
c ---[ 633]---> BDD-cost:    7
c ---[ 632]---> BDD-cost:   17
c ---[ 631]---> BDD-cost:    7
c ---[ 630]---> BDD-cost:    6
c ---[ 629]---> BDD-cost:    7
c ---[ 628]---> BDD-cost:    8
c ---[ 627]---> BDD-cost:    3
c ---[ 626]---> BDD-cost:    8
c ---[ 625]---> BDD-cost:    8
c ---[ 623]---> Adder-cost: 1910   maxlim: 361820   bits: 20/19
c ---[ 622]---> BDD-cost:    5
c ---[ 621]---> BDD-cost:    5
c ---[ 620]---> BDD-cost:    3
c ---[ 619]---> BDD-cost:    5
c ---[ 618]---> BDD-cost:    4
c ---[ 617]---> BDD-cost:    4
c ---[ 616]---> BDD-cost:    5
c ---[ 615]---> BDD-cost:    7
c ---[ 614]---> BDD-cost:    6
c ---[ 613]---> BDD-cost:    6
c ---[ 611]---> Adder-cost: 1804   maxlim: 361181   bits: 20/19
c ---[ 610]---> BDD-cost:    7
c ---[ 609]---> BDD-cost:    7
c ---[ 608]---> BDD-cost:    7
c ---[ 607]---> BDD-cost:    5
c ---[ 606]---> BDD-cost:   17
c ---[ 605]---> BDD-cost:   15
c ---[ 604]---> BDD-cost:    7
c ---[ 603]---> BDD-cost:    5
c ---[ 602]---> BDD-cost:    7
c ---[ 601]---> BDD-cost:    6
c ---[ 599]---> Adder-cost: 1688   maxlim: 366303   bits: 20/19
c ---[ 598]---> BDD-cost:    6
c ---[ 597]---> BDD-cost:    7
c ---[ 596]---> BDD-cost:    7
c ---[ 595]---> BDD-cost:    7
c ---[ 594]---> BDD-cost:    8
c ---[ 593]---> BDD-cost:    7
c ---[ 592]---> BDD-cost:   16
c ---[ 591]---> BDD-cost:    3
c ---[ 590]---> BDD-cost:   19
c ---[ 589]---> BDD-cost:    8
c ---[ 587]---> Adder-cost: 1776   maxlim: 357854   bits: 20/19
c ---[ 586]---> BDD-cost:    4
c ---[ 585]---> BDD-cost:    6
c ---[ 584]---> BDD-cost:    8
c ---[ 583]---> BDD-cost:    6
c ---[ 582]---> BDD-cost:    5
c ---[ 581]---> BDD-cost:    8
c ---[ 580]---> BDD-cost:    8
c ---[ 579]---> BDD-cost:    6
c ---[ 578]---> BDD-cost:    7
c ---[ 577]---> BDD-cost:   15
c ---[ 575]---> Adder-cost: 1652   maxlim: 345567   bits: 20/19
c ---[ 574]---> BDD-cost:    5
c ---[ 573]---> BDD-cost:    7
c ---[ 572]---> BDD-cost:    6
c ---[ 571]---> BDD-cost:    5
c ---[ 570]---> BDD-cost:    6
c ---[ 569]---> BDD-cost:    7
c ---[ 568]---> BDD-cost:   18
c ---[ 567]---> BDD-cost:    4
c ---[ 566]---> BDD-cost:    4
c ---[ 565]---> BDD-cost:    8
c ---[ 563]---> Adder-cost: 1706   maxlim: 361951   bits: 20/19
c ---[ 562]---> BDD-cost:    7
c ---[ 561]---> BDD-cost:    6
c ---[ 560]---> BDD-cost:    8
c ---[ 559]---> BDD-cost:    5
c ---[ 558]---> BDD-cost:    5
c ---[ 557]---> BDD-cost:    6
c ---[ 556]---> BDD-cost:    7
c ---[ 555]---> BDD-cost:    8
c ---[ 554]---> BDD-cost:    8
c ---[ 553]---> BDD-cost:    7
c ---[ 551]---> Adder-cost: 1844   maxlim: 388571   bits: 20/19
c ---[ 550]---> BDD-cost:    5
c ---[ 549]---> BDD-cost:    3
c ---[ 548]---> BDD-cost:    4
c ---[ 547]---> BDD-cost:    5
c ---[ 546]---> BDD-cost:   19
c ---[ 545]---> BDD-cost:    6
c ---[ 544]---> BDD-cost:    7
c ---[ 543]---> BDD-cost:   16
c ---[ 542]---> BDD-cost:    3
c ---[ 541]---> BDD-cost:    8
c ---[ 539]---> Adder-cost: 1840   maxlim: 400221   bits: 20/19
c ---[ 538]---> BDD-cost:    7
c ---[ 537]---> BDD-cost:    7
c ---[ 536]---> BDD-cost:    3
c ---[ 535]---> BDD-cost:    7
c ---[ 534]---> BDD-cost:   16
c ---[ 533]---> BDD-cost:    7
c ---[ 532]---> BDD-cost:    6
c ---[ 531]---> BDD-cost:    3
c ---[ 530]---> BDD-cost:    4
c ---[ 529]---> BDD-cost:    4
c ---[ 527]---> BDD-cost:   63
c ---[ 525]---> Adder-cost: 1750   maxlim: 295774   bits: 20/19
c ---[ 524]---> BDD-cost:    3
c ---[ 523]---> BDD-cost:    6
c ---[ 522]---> BDD-cost:    7
c ---[ 521]---> BDD-cost:    5
c ---[ 520]---> BDD-cost:    8
c ---[ 519]---> BDD-cost:    8
c ---[ 518]---> BDD-cost:    8
c ---[ 517]---> BDD-cost:    7
c ---[ 516]---> BDD-cost:    7
c ---[ 515]---> BDD-cost:    8
c ---[ 513]---> Adder-cost: 1846   maxlim: 420571   bits: 20/19
c ---[ 512]---> BDD-cost:    6
c ---[ 511]---> BDD-cost:    6
c ---[ 510]---> BDD-cost:   18
c ---[ 509]---> BDD-cost:    8
c ---[ 508]---> BDD-cost:    5
c ---[ 507]---> BDD-cost:    4
c ---[ 506]---> BDD-cost:    8
c ---[ 505]---> BDD-cost:   18
c ---[ 504]---> BDD-cost:    7
c ---[ 503]---> BDD-cost:    7
c ---[ 501]---> Adder-cost: 1882   maxlim: 354138   bits: 20/19
c ---[ 500]---> BDD-cost:    8
c ---[ 499]---> BDD-cost:    3
c ---[ 498]---> BDD-cost:    8
c ---[ 497]---> BDD-cost:    7
c ---[ 496]---> BDD-cost:    7
c ---[ 495]---> BDD-cost:    8
c ---[ 494]---> BDD-cost:    8
c ---[ 493]---> BDD-cost:    8
c ---[ 492]---> BDD-cost:    6
c ---[ 491]---> BDD-cost:    7
c ---[ 489]---> Adder-cost: 1868   maxlim: 473819   bits: 20/19
c ---[ 488]---> BDD-cost:    5
c ---[ 487]---> BDD-cost:    8
c ---[ 486]---> BDD-cost:   19
c ---[ 485]---> BDD-cost:   19
c ---[ 484]---> BDD-cost:    8
c ---[ 483]---> BDD-cost:    7
c ---[ 482]---> BDD-cost:    5
c ---[ 481]---> BDD-cost:    8
c ---[ 480]---> BDD-cost:    7
c ---[ 479]---> BDD-cost:    8
c ---[ 477]---> Adder-cost: 1892   maxlim: 360028   bits: 20/19
c ---[ 476]---> BDD-cost:    7
c ---[ 475]---> BDD-cost:    4
c ---[ 474]---> BDD-cost:    5
c ---[ 473]---> BDD-cost:    6
c ---[ 472]---> BDD-cost:    7
c ---[ 471]---> BDD-cost:    8
c ---[ 470]---> BDD-cost:    8
c ---[ 469]---> BDD-cost:    6
c ---[ 468]---> BDD-cost:    8
c ---[ 467]---> BDD-cost:    5
c ---[ 465]---> Adder-cost: 1728   maxlim: 351069   bits: 20/19
c ---[ 464]---> BDD-cost:    6
c ---[ 463]---> BDD-cost:    8
c ---[ 462]---> BDD-cost:    7
c ---[ 461]---> BDD-cost:    5
c ---[ 460]---> BDD-cost:    3
c ---[ 459]---> BDD-cost:    4
c ---[ 458]---> BDD-cost:    7
c ---[ 457]---> BDD-cost:    7
c ---[ 456]---> BDD-cost:    6
c ---[ 455]---> BDD-cost:    5
c ---[ 453]---> Adder-cost: 1810   maxlim: 346847   bits: 20/19
c ---[ 452]---> BDD-cost:    3
c ---[ 451]---> BDD-cost:    5
c ---[ 450]---> BDD-cost:    7
c ---[ 449]---> BDD-cost:    6
c ---[ 448]---> BDD-cost:   17
c ---[ 447]---> BDD-cost:    5
c ---[ 446]---> BDD-cost:    6
c ---[ 445]---> BDD-cost:    6
c ---[ 444]---> BDD-cost:    8
c ---[ 443]---> BDD-cost:    6
c ---[ 441]---> Adder-cost: 1706   maxlim: 334815   bits: 20/19
c ---[ 440]---> BDD-cost:    6
c ---[ 439]---> BDD-cost:    6
c ---[ 438]---> BDD-cost:    8
c ---[ 437]---> BDD-cost:    7
c ---[ 436]---> BDD-cost:    5
c ---[ 435]---> BDD-cost:    8
c ---[ 434]---> BDD-cost:    5
c ---[ 433]---> BDD-cost:    6
c ---[ 432]---> BDD-cost:    7
c ---[ 431]---> BDD-cost:    8
c ---[ 429]---> Adder-cost: 1744   maxlim: 373858   bits: 20/19
c ---[ 428]---> BDD-cost:    3
c ---[ 427]---> BDD-cost:   16
c ---[ 426]---> BDD-cost:    8
c ---[ 425]---> BDD-cost:    6
c ---[ 424]---> BDD-cost:   18
c ---[ 423]---> BDD-cost:    6
c ---[ 422]---> BDD-cost:    4
c ---[ 421]---> BDD-cost:    3
c ---[ 420]---> BDD-cost:    7
c ---[ 419]---> BDD-cost:    7
c ---[ 418]---> BDD-cost:    8
c ---[ 417]---> BDD-cost:    7
c ---[ 416]---> BDD-cost:    3
c ---[ 415]---> BDD-cost:    7
c ---[ 414]---> BDD-cost:    7
c ---[ 413]---> BDD-cost:    4
c ---[ 412]---> BDD-cost:    8
c ---[ 411]---> BDD-cost:   17
c ---[ 410]---> BDD-cost:    5
c ---[ 409]---> BDD-cost:    8
c ---[ 408]---> BDD-cost:    3
c ---[ 406]---> BDD-cost:   71
c ---[ 405]---> BDD-cost:    6
c ---[ 404]---> BDD-cost:    7
c ---[ 403]---> BDD-cost:    8
c ---[ 402]---> BDD-cost:    5
c ---[ 401]---> BDD-cost:   18
c ---[ 400]---> BDD-cost:    5
c ---[ 399]---> BDD-cost:    5
c ---[ 398]---> BDD-cost:    8
c ---[ 397]---> BDD-cost:    7
c ---[ 396]---> BDD-cost:    5
c ---[ 395]---> BDD-cost:    8
c ---[ 394]---> BDD-cost:    8
c ---[ 393]---> BDD-cost:    6
c ---[ 392]---> BDD-cost:    6
c ---[ 391]---> BDD-cost:    8
c ---[ 390]---> BDD-cost:    8
c ---[ 389]---> BDD-cost:    7
c ---[ 388]---> BDD-cost:    7
c ---[ 387]---> BDD-cost:    3
c ---[ 386]---> BDD-cost:    6
c ---[ 385]---> BDD-cost:    7
c ---[ 384]---> BDD-cost:   19
c ---[ 383]---> BDD-cost:    8
c ---[ 382]---> BDD-cost:    6
c ---[ 381]---> BDD-cost:    3
c ---[ 380]---> BDD-cost:    8
c ---[ 379]---> BDD-cost:    7
c ---[ 378]---> BDD-cost:    6
c ---[ 377]---> BDD-cost:    3
c ---[ 376]---> BDD-cost:   18
c ---[ 375]---> BDD-cost:    8
c ---[ 374]---> BDD-cost:    3
c ---[ 373]---> BDD-cost:    7
c ---[ 372]---> BDD-cost:   17
c ---[ 371]---> BDD-cost:    8
c ---[ 370]---> BDD-cost:    7
c ---[ 369]---> BDD-cost:   19
c ---[ 368]---> BDD-cost:   15
c ---[ 367]---> BDD-cost:    8
c ---[ 366]---> BDD-cost:    8
c ---[ 365]---> BDD-cost:    4
c ---[ 364]---> BDD-cost:    7
c ---[ 363]---> BDD-cost:    7
c ---[ 362]---> BDD-cost:   19
c ---[ 361]---> BDD-cost:    8
c ---[ 360]---> BDD-cost:    5
c ---[ 359]---> BDD-cost:    8
c ---[ 358]---> BDD-cost:    7
c ---[ 357]---> BDD-cost:   16
c ---[ 356]---> BDD-cost:    6
c ---[ 355]---> BDD-cost:    7
c ---[ 354]---> BDD-cost:    5
c ---[ 353]---> BDD-cost:    5
c ---[ 352]---> BDD-cost:    8
c ---[ 351]---> BDD-cost:    4
c ---[ 350]---> BDD-cost:    6
c ---[ 349]---> BDD-cost:    6
c ---[ 348]---> BDD-cost:    8
c ---[ 347]---> BDD-cost:    3
c ---[ 346]---> BDD-cost:    8
c ---[ 345]---> BDD-cost:    6
c ---[ 344]---> BDD-cost:    7
c ---[ 343]---> BDD-cost:    6
c ---[ 342]---> BDD-cost:    7
c ---[ 341]---> BDD-cost:    7
c ---[ 340]---> BDD-cost:    8
c ---[ 339]---> BDD-cost:    5
c ---[ 338]---> BDD-cost:    8
c ---[ 337]---> BDD-cost:    7
c ---[ 336]---> BDD-cost:    8
c ---[ 335]---> BDD-cost:    5
c ---[ 334]---> BDD-cost:    6
c ---[ 333]---> BDD-cost:   19
c ---[ 332]---> BDD-cost:   17
c ---[ 331]---> BDD-cost:    7
c ---[ 330]---> BDD-cost:    4
c ---[ 329]---> BDD-cost:   14
c ---[ 328]---> BDD-cost:    6
c ---[ 327]---> BDD-cost:    8
c ---[ 326]---> BDD-cost:    8
c ---[ 325]---> BDD-cost:    6
c ---[ 324]---> BDD-cost:    4
c ---[ 323]---> BDD-cost:    6
c ---[ 322]---> BDD-cost:    3
c ---[ 321]---> BDD-cost:    7
c ---[ 320]---> BDD-cost:    7
c ---[ 319]---> BDD-cost:    7
c ---[ 318]---> BDD-cost:    6
c ---[ 317]---> BDD-cost:   17
c ---[ 316]---> BDD-cost:    8
c ---[ 315]---> BDD-cost:    6
c ---[ 314]---> BDD-cost:    8
c ---[ 313]---> BDD-cost:    3
c ---[ 312]---> BDD-cost:    6
c ---[ 311]---> BDD-cost:    7
c ---[ 310]---> BDD-cost:    5
c ---[ 309]---> BDD-cost:    6
c ---[ 308]---> BDD-cost:   19
c ---[ 307]---> BDD-cost:   17
c ---[ 306]---> BDD-cost:    7
c ---[ 305]---> BDD-cost:   14
c ---[ 304]---> BDD-cost:    7
c ---[ 303]---> BDD-cost:    3
c ---[ 302]---> BDD-cost:   19
c ---[ 301]---> BDD-cost:   19
c ---[ 300]---> BDD-cost:    5
c ---[ 299]---> BDD-cost:    7
c ---[ 298]---> BDD-cost:   17
c ---[ 297]---> BDD-cost:    5
c ---[ 296]---> BDD-cost:    5
c ---[ 294]---> BDD-cost:   65
c ---[ 293]---> BDD-cost:    5
c ---[ 292]---> BDD-cost:    8
c ---[ 291]---> BDD-cost:    3
c ---[ 290]---> BDD-cost:    7
c ---[ 289]---> BDD-cost:    3
c ---[ 288]---> BDD-cost:    8
c ---[ 287]---> BDD-cost:    7
c ---[ 286]---> BDD-cost:    5
c ---[ 285]---> BDD-cost:    7
c ---[ 284]---> BDD-cost:    7
c ---[ 283]---> BDD-cost:   15
c ---[ 282]---> BDD-cost:    7
c ---[ 281]---> BDD-cost:    6
c ---[ 280]---> BDD-cost:   19
c ---[ 279]---> BDD-cost:    6
c ---[ 278]---> BDD-cost:    3
c ---[ 277]---> BDD-cost:    5
c ---[ 276]---> BDD-cost:   16
c ---[ 275]---> BDD-cost:    8
c ---[ 274]---> BDD-cost:    8
c ---[ 273]---> BDD-cost:    3
c ---[ 272]---> BDD-cost:    8
c ---[ 271]---> BDD-cost:    8
c ---[ 270]---> BDD-cost:    7
c ---[ 269]---> BDD-cost:    6
c ---[ 268]---> BDD-cost:    8
c ---[ 267]---> BDD-cost:    6
c ---[ 266]---> BDD-cost:    7
c ---[ 265]---> BDD-cost:    8
c ---[ 264]---> BDD-cost:    5
c ---[ 263]---> BDD-cost:    7
c ---[ 262]---> BDD-cost:    3
c ---[ 261]---> BDD-cost:    6
c ---[ 260]---> BDD-cost:    5
c ---[ 259]---> BDD-cost:    8
c ---[ 258]---> BDD-cost:    8
c ---[ 257]---> BDD-cost:    7
c ---[ 256]---> BDD-cost:   16
c ---[ 255]---> BDD-cost:    8
c ---[ 254]---> BDD-cost:    8
c ---[ 253]---> BDD-cost:    6
c ---[ 252]---> BDD-cost:   17
c ---[ 251]---> BDD-cost:    8
c ---[ 250]---> BDD-cost:    7
c ---[ 249]---> BDD-cost:    8
c ---[ 248]---> BDD-cost:    3
c ---[ 247]---> BDD-cost:    8
c ---[ 246]---> BDD-cost:    7
c ---[ 245]---> BDD-cost:    4
c ---[ 244]---> BDD-cost:    3
c ---[ 243]---> BDD-cost:    3
c ---[ 242]---> BDD-cost:    7
c ---[ 241]---> BDD-cost:    7
c ---[ 240]---> BDD-cost:    4
c ---[ 239]---> BDD-cost:    3
c ---[ 238]---> BDD-cost:   16
c ---[ 237]---> BDD-cost:    8
c ---[ 236]---> BDD-cost:    6
c ---[ 235]---> BDD-cost:    8
c ---[ 234]---> BDD-cost:    6
c ---[ 233]---> BDD-cost:   18
c ---[ 232]---> BDD-cost:    6
c ---[ 231]---> BDD-cost:    6
c ---[ 230]---> BDD-cost:    8
c ---[ 229]---> BDD-cost:   18
c ---[ 228]---> BDD-cost:    7
c ---[ 227]---> BDD-cost:    8
c ---[ 226]---> BDD-cost:    8
c ---[ 225]---> BDD-cost:    8
c ---[ 224]---> BDD-cost:   18
c ---[ 223]---> BDD-cost:    6
c ---[ 222]---> BDD-cost:    7
c ---[ 221]---> BDD-cost:    6
c ---[ 220]---> BDD-cost:    3
c ---[ 219]---> BDD-cost:   17
c ---[ 218]---> BDD-cost:   16
c ---[ 217]---> BDD-cost:   18
c ---[ 216]---> BDD-cost:    7
c ---[ 215]---> BDD-cost:    3
c ---[ 214]---> BDD-cost:    3
c ---[ 213]---> BDD-cost:    4
c ---[ 212]---> BDD-cost:    8
c ---[ 211]---> BDD-cost:    6
c ---[ 210]---> BDD-cost:    6
c ---[ 209]---> BDD-cost:    8
c ---[ 208]---> BDD-cost:    3
c ---[ 207]---> BDD-cost:    7
c ---[ 206]---> BDD-cost:    7
c ---[ 205]---> BDD-cost:    8
c ---[ 204]---> BDD-cost:    6
c ---[ 203]---> BDD-cost:    5
c ---[ 202]---> BDD-cost:    7
c ---[ 201]---> BDD-cost:    4
c ---[ 200]---> BDD-cost:    6
c ---[ 199]---> BDD-cost:    7
c ---[ 198]---> BDD-cost:    7
c ---[ 197]---> BDD-cost:   18
c ---[ 196]---> BDD-cost:   18
c ---[ 195]---> BDD-cost:    3
c ---[ 194]---> BDD-cost:    8
c ---[ 193]---> BDD-cost:    6
c ---[ 192]---> BDD-cost:    8
c ---[ 191]---> BDD-cost:    6
c ---[ 190]---> BDD-cost:    8
c ---[ 189]---> BDD-cost:    6
c ---[ 188]---> BDD-cost:    3
c ---[ 187]---> BDD-cost:    6
c ---[ 186]---> BDD-cost:    6
c ---[ 185]---> BDD-cost:    7
c ---[ 184]---> BDD-cost:    7
c ---[ 183]---> BDD-cost:    1
c ---[ 182]---> BDD-cost:    1
c ---[ 181]---> BDD-cost:    1
c ---[ 180]---> BDD-cost:    1
c ---[ 179]---> BDD-cost:    1
c ---[ 178]---> BDD-cost:    1
c ---[ 177]---> BDD-cost:    1
c ---[ 176]---> BDD-cost:    1
c ---[ 175]---> BDD-cost:    1
c ---[ 174]---> BDD-cost:    1
c ---[ 173]---> BDD-cost:    1
c ---[ 172]---> BDD-cost:    1
c ---[ 171]---> BDD-cost:    1
c ---[ 170]---> BDD-cost:    1
c ---[ 169]---> BDD-cost:    1
c ---[ 168]---> BDD-cost:    1
c ---[ 167]---> BDD-cost:    1
c ---[ 166]---> BDD-cost:    1
c ---[ 165]---> BDD-cost:    1
c ---[ 164]---> BDD-cost:    1
c ---[ 163]---> BDD-cost:    1
c ---[ 162]---> BDD-cost:    1
c ---[ 161]---> BDD-cost:    1
c ---[ 160]---> BDD-cost:    1
c ---[ 159]---> BDD-cost:    1
c ---[ 158]---> BDD-cost:    1
c ---[ 157]---> BDD-cost:    1
c ---[ 156]---> BDD-cost:    1
c ---[ 155]---> BDD-cost:    1
c ---[ 154]---> BDD-cost:    1
c ---[ 153]---> BDD-cost:    1
c ---[ 152]---> BDD-cost:    1
c ---[ 151]---> BDD-cost:    1
c ---[ 150]---> BDD-cost:    1
c ---[ 149]---> BDD-cost:    1
c ---[ 148]---> BDD-cost:    1
c ---[ 147]---> BDD-cost:    1
c ---[ 146]---> BDD-cost:    1
c ---[ 145]---> BDD-cost:    1
c ---[ 144]---> BDD-cost:    1
c ---[ 143]---> BDD-cost:    1
c ---[ 142]---> BDD-cost:    1
c ---[ 141]---> BDD-cost:    1
c ---[ 140]---> BDD-cost:    1
c ---[ 139]---> BDD-cost:    1
c ---[ 138]---> BDD-cost:    1
c ---[ 137]---> BDD-cost:    1
c ---[ 136]---> BDD-cost:    1
c ---[ 135]---> BDD-cost:    1
c ---[ 134]---> BDD-cost:    1
c ---[ 133]---> BDD-cost:    1
c ---[ 132]---> BDD-cost:    1
c ---[ 131]---> BDD-cost:    1
c ---[ 130]---> BDD-cost:    1
c ---[ 129]---> BDD-cost:    1
c ---[ 128]---> BDD-cost:    1
c ---[ 127]---> BDD-cost:    1
c ---[ 126]---> BDD-cost:    1
c ---[ 125]---> BDD-cost:    1
c ---[ 124]---> BDD-cost:    1
c ---[ 123]---> BDD-cost:    1
c ---[ 122]---> BDD-cost:    1
c ---[ 121]---> BDD-cost:    1
c ---[ 120]---> BDD-cost:    1
c ---[ 119]---> BDD-cost:    1
c ---[ 118]---> BDD-cost:    1
c ---[ 117]---> BDD-cost:    1
c ---[ 116]---> BDD-cost:    1
c ---[ 115]---> BDD-cost:    1
c ---[ 114]---> BDD-cost:    1
c ---[ 113]---> BDD-cost:    1
c ---[ 112]---> BDD-cost:    1
c ---[ 111]---> BDD-cost:    1
c ---[ 110]---> BDD-cost:    1
c ---[ 109]---> BDD-cost:    1
c ---[ 108]---> BDD-cost:    1
c ---[ 107]---> BDD-cost:    1
c ---[ 106]---> BDD-cost:    1
c ---[ 105]---> BDD-cost:    1
c ---[ 104]---> BDD-cost:    1
c ---[ 103]---> BDD-cost:    1
c ---[ 102]---> BDD-cost:    1
c ---[ 101]---> BDD-cost:    1
c ---[ 100]---> BDD-cost:    1
c ---[  99]---> BDD-cost:    1
c ---[  98]---> BDD-cost:    1
c ---[  97]---> BDD-cost:    1
c ---[  96]---> BDD-cost:    1
c ---[  95]---> BDD-cost:    1
c ---[  94]---> BDD-cost:    1
c ---[  93]---> BDD-cost:    1
c ---[  92]---> BDD-cost:    1
c ---[  91]---> BDD-cost:    1
c ---[  90]---> BDD-cost:    1
c ---[  89]---> BDD-cost:    1
c ---[  88]---> BDD-cost:    1
c ---[  87]---> BDD-cost:    1
c ---[  86]---> BDD-cost:    1
c ---[  85]---> BDD-cost:    1
c ---[  84]---> BDD-cost:    1
c ---[  83]---> BDD-cost:    1
c ---[  82]---> BDD-cost:    1
c ---[  81]---> BDD-cost:    1
c ---[  80]---> BDD-cost:    1
c ---[  79]---> BDD-cost:    1
c ---[  78]---> BDD-cost:    1
c ---[  77]---> BDD-cost:    1
c ---[  76]---> BDD-cost:    1
c ---[  75]---> BDD-cost:    1
c ---[  74]---> BDD-cost:    1
c ---[  73]---> BDD-cost:    1
c ---[  72]---> BDD-cost:    1
c ---[  71]---> BDD-cost:    1
c ---[  70]---> BDD-cost:    1
c ---[  69]---> BDD-cost:    1
c ---[  68]---> BDD-cost:    1
c ---[  67]---> BDD-cost:    1
c ---[  66]---> BDD-cost:    1
c ---[  65]---> BDD-cost:    1
c ---[  64]---> BDD-cost:    1
c ---[  63]---> BDD-cost:    1
c ---[  62]---> BDD-cost:    1
c ---[  61]---> BDD-cost:    1
c ---[  60]---> BDD-cost:    1
c ---[  59]---> BDD-cost:    1
c ---[  58]---> BDD-cost:    1
c ---[  57]---> BDD-cost:    1
c ---[  56]---> BDD-cost:    1
c ---[  55]---> BDD-cost:    1
c ---[  54]---> BDD-cost:    1
c ---[  53]---> BDD-cost:    1
c ---[  52]---> BDD-cost:    1
c ---[  51]---> BDD-cost:    1
c ---[  50]---> BDD-cost:    1
c ---[  49]---> BDD-cost:    1
c ---[  48]---> BDD-cost:    1
c ---[  47]---> BDD-cost:    1
c ---[  46]---> BDD-cost:    1
c ---[  45]---> BDD-cost:    1
c ---[  44]---> BDD-cost:    1
c ---[  43]---> BDD-cost:    1
c ---[  42]---> BDD-cost:    1
c ---[  41]---> BDD-cost:    1
c ---[  40]---> BDD-cost:    1
c ---[  39]---> BDD-cost:    1
c ---[  38]---> BDD-cost:    1
c ---[  37]---> BDD-cost:    1
c ---[  36]---> BDD-cost:    1
c ---[  35]---> BDD-cost:    1
c ---[  34]---> BDD-cost:    1
c ---[  33]---> BDD-cost:    1
c ---[  32]---> BDD-cost:    1
c ---[  31]---> BDD-cost:    1
c ---[  30]---> BDD-cost:    1
c ---[  29]---> BDD-cost:    1
c ---[  28]---> BDD-cost:    1
c ---[  27]---> BDD-cost:    1
c ---[  26]---> BDD-cost:    1
c ---[  25]---> BDD-cost:    1
c ---[  24]---> BDD-cost:    1
c ---[  23]---> BDD-cost:    1
c ---[  22]---> BDD-cost:    1
c ---[  21]---> BDD-cost:    1
c ---[  20]---> BDD-cost:    1
c ---[  19]---> BDD-cost:    1
c ---[  18]---> BDD-cost:    1
c ---[  17]---> BDD-cost:    1
c ---[  16]---> BDD-cost:    1
c ---[  15]---> BDD-cost:    1
c ---[  14]---> BDD-cost:    1
c ---[  13]---> BDD-cost:    1
c ---[  12]---> BDD-cost:    1
c ---[  11]---> BDD-cost:    1
c ---[  10]---> BDD-cost:    1
c ---[   9]---> BDD-cost:    1
c ---[   8]---> BDD-cost:    1
c ---[   7]---> BDD-cost:    1
c ---[   6]---> BDD-cost:    1
c ---[   5]---> BDD-cost:    1
c ---[   4]---> BDD-cost:    1
c ---[   3]---> BDD-cost:    1
c ---[   2]---> BDD-cost:    1
c ---[   1]---> BDD-cost:    1
c ---[   0]---> BDD-cost:    1
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |  518335  1805432 |  172778       0        0     nan |  0.000 % |
c |       100 |  518335  1805432 |  190055     100    28924   289.2 |  4.235 % |
c |       250 |  518327  1805406 |  209061     249    29627   119.0 |  4.236 % |
c |       478 |  518327  1805406 |  229967     477    37431    78.5 |  4.236 % |
c |       816 |  518286  1805263 |  252964     797    54200    68.0 |  4.241 % |
c |      1323 |  518269  1805206 |  278260    1301   110528    85.0 |  4.243 % |
c |      2082 |  518236  1805097 |  306086    2053   123909    60.4 |  4.247 % |
c |      3223 |  518236  1805097 |  336695    3194   187040    58.6 |  4.247 % |
c |      4931 |  518176  1804895 |  370364    4889   318013    65.0 |  4.254 % |
c |      7493 |  518160  1804843 |  407401    7449   584975    78.5 |  4.256 % |
c |     11340 |  518101  1804642 |  448141   11281  1581751   140.2 |  4.263 % |
c |     17106 |  518006  1804321 |  492955   17019  2128414   125.1 |  4.274 % |
c |     25757 |  517936  1804083 |  542251   25650  3752157   146.3 |  4.281 % |
c |     38731 |  517840  1803757 |  596476   38597  8459867   219.2 |  4.292 % |
c |     58194 |  517700  1803277 |  656124   58008 12617149   217.5 |  4.308 % |
#### 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.79 0.92 0.89 2/54 32223
Raw data (stat): 32223 (runsolver) R 32222 25285 25284 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 488413023 1052672 99 4294967295 134512640 135381576 3221224512 3221219756 135158418 0 2147483391 7 90112 0 0 0 17 0 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+9.99996 s]
Raw data (loadavg): 0.82 0.93 0.90 2/54 32223
Raw data (stat): 32223 (minisat+) R 32222 25285 25284 0 -1 0 11116 0 0 0 974 24 0 0 25 0 1 0 488413023 47386624 10664 4294967295 134512640 134672761 3221224624 3221223792 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11569 10664 603 41 0 11528 0
vsize: 46276
[startup+19.9998 s]
Raw data (loadavg): 0.85 0.93 0.90 2/54 32223
Raw data (stat): 32223 (minisat+) R 32222 25285 25284 0 -1 0 11197 0 0 0 1973 24 0 0 25 0 1 0 488413023 47792128 10745 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11668 10745 603 41 0 11627 0
vsize: 46672
[startup+30.0007 s]
Raw data (loadavg): 0.87 0.93 0.90 2/54 32223
Raw data (stat): 32223 (minisat+) R 32222 25285 25284 0 -1 0 11233 0 0 0 2973 24 0 0 25 0 1 0 488413023 47927296 10781 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11701 10781 603 41 0 11660 0
vsize: 46804
[startup+40.0005 s]
Raw data (loadavg): 0.89 0.93 0.90 2/54 32223
Raw data (stat): 32223 (minisat+) R 32222 25285 25284 0 -1 0 11289 0 0 0 3972 25 0 0 25 0 1 0 488413023 48197632 10837 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11767 10837 603 41 0 11726 0
vsize: 47068
[startup+50.0003 s]
Raw data (loadavg): 0.91 0.93 0.90 2/54 32223
Raw data (stat): 32223 (minisat+) R 32222 25285 25284 0 -1 0 11351 0 0 0 4972 25 0 0 25 0 1 0 488413023 48467968 10899 4294967295 134512640 134672761 3221224624 3221223760 134560673 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11833 10899 603 41 0 11792 0
vsize: 47332
[startup+60.0001 s]
Raw data (loadavg): 0.92 0.94 0.90 2/54 32223
Raw data (stat): 32223 (minisat+) R 32222 25285 25284 0 -1 0 11462 0 0 0 5971 25 0 0 25 0 1 0 488413023 48898048 11010 4294967295 134512640 134672761 3221224624 3221223728 134559964 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11938 11010 603 41 0 11897 0
vsize: 47752
[startup+69.9999 s]
Raw data (loadavg): 0.93 0.94 0.90 2/54 32223
Raw data (stat): 32223 (minisat+) R 32222 25285 25284 0 -1 0 11533 0 0 0 6971 26 0 0 25 0 1 0 488413023 49168384 11081 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12004 11081 603 41 0 11963 0
vsize: 48016
[startup+80.0008 s]
Raw data (loadavg): 0.94 0.94 0.90 2/54 32223
Raw data (stat): 32223 (minisat+) R 32222 25285 25284 0 -1 0 11625 0 0 0 7971 27 0 0 25 0 1 0 488413023 49573888 11173 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12103 11173 603 41 0 12062 0
vsize: 48412
[startup+90.0006 s]
Raw data (loadavg): 0.95 0.94 0.90 2/54 32223
Raw data (stat): 32223 (minisat+) R 32222 25285 25284 0 -1 0 11725 0 0 0 8970 27 0 0 25 0 1 0 488413023 49975296 11273 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12201 11273 603 41 0 12160 0
vsize: 48804
[startup+100 s]
Raw data (loadavg): 0.96 0.94 0.90 2/54 32223
Raw data (stat): 32223 (minisat+) R 32222 25285 25284 0 -1 0 11795 0 0 0 9970 27 0 0 25 0 1 0 488413023 50245632 11343 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12267 11343 603 41 0 12226 0
vsize: 49068
[startup+110.002 s]
Raw data (loadavg): 0.96 0.94 0.91 2/54 32223
Raw data (stat): 32223 (minisat+) R 32222 25285 25284 0 -1 0 11940 0 0 0 10970 27 0 0 25 0 1 0 488413023 50786304 11488 4294967295 134512640 134672761 3221224624 3221223792 134561161 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12399 11488 603 41 0 12358 0
vsize: 49596
[startup+120.001 s]
Raw data (loadavg): 0.97 0.94 0.91 2/54 32223
Raw data (stat): 32223 (minisat+) R 32222 25285 25284 0 -1 0 12251 0 0 0 11969 29 0 0 25 0 1 0 488413023 52129792 11799 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12727 11799 603 41 0 12686 0
vsize: 50908
[startup+130.001 s]
Raw data (loadavg): 0.97 0.95 0.91 2/54 32223
Raw data (stat): 32223 (minisat+) R 32222 25285 25284 0 -1 0 12519 0 0 0 12969 29 0 0 25 0 1 0 488413023 53211136 12067 4294967295 134512640 134672761 3221224624 3221223760 134560718 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12991 12067 603 41 0 12950 0
vsize: 51964
[startup+140.001 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 32223
Raw data (stat): 32223 (minisat+) R 32222 25285 25284 0 -1 0 12757 0 0 0 13969 30 0 0 25 0 1 0 488413023 54153216 12305 4294967295 134512640 134672761 3221224624 3221223824 134557911 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13221 12305 603 41 0 13180 0
vsize: 52884
[startup+150.001 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 32223
Raw data (stat): 32223 (minisat+) R 32222 25285 25284 0 -1 0 12816 0 0 0 14968 30 0 0 25 0 1 0 488413023 54423552 12364 4294967295 134512640 134672761 3221224624 3221223824 134557911 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13287 12364 603 41 0 13246 0
vsize: 53148
[startup+160 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 32223
Raw data (stat): 32223 (minisat+) R 32222 25285 25284 0 -1 0 12893 0 0 0 15968 30 0 0 25 0 1 0 488413023 54693888 12441 4294967295 134512640 134672761 3221224624 3221223824 134557830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13353 12441 603 41 0 13312 0
vsize: 53412
[startup+170.001 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 32223
Raw data (stat): 32223 (minisat+) R 32222 25285 25284 0 -1 0 12944 0 0 0 16969 30 0 0 25 0 1 0 488413023 54960128 12492 4294967295 134512640 134672761 3221224624 3221223760 134560640 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13418 12492 603 41 0 13377 0
vsize: 53672
[startup+180.001 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 32223
Raw data (stat): 32223 (minisat+) R 32222 25285 25284 0 -1 0 13073 0 0 0 17968 30 0 0 25 0 1 0 488413023 55500800 12621 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13550 12621 603 41 0 13509 0
vsize: 54200
[startup+190.001 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 32223
Raw data (stat): 32223 (minisat+) R 32222 25285 25284 0 -1 0 13158 0 0 0 18968 31 0 0 25 0 1 0 488413023 55771136 12706 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13616 12706 603 41 0 13575 0
vsize: 54464
[startup+200.001 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 32223
Raw data (stat): 32223 (minisat+) R 32222 25285 25284 0 -1 0 13233 0 0 0 19968 31 0 0 25 0 1 0 488413023 56176640 12781 4294967295 134512640 134672761 3221224624 3221223792 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13715 12781 603 41 0 13674 0
vsize: 54860
[startup+210.002 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 32223
Raw data (stat): 32223 (minisat+) R 32222 25285 25284 0 -1 0 13311 0 0 0 20969 31 0 0 25 0 1 0 488413023 56537088 12859 4294967295 134512640 134672761 3221224624 3221223808 134558662 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13803 12859 603 41 0 13762 0
vsize: 55212
[startup+220.002 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 32223
Raw data (stat): 32223 (minisat+) R 32222 25285 25284 0 -1 0 13411 0 0 0 21968 31 0 0 25 0 1 0 488413023 56942592 12959 4294967295 134512640 134672761 3221224624 3221223808 134559498 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13902 12959 603 41 0 13861 0
vsize: 55608
[startup+230.002 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 32223
Raw data (stat): 32223 (minisat+) R 32222 25285 25284 0 -1 0 13502 0 0 0 22968 31 0 0 25 0 1 0 488413023 57212928 13050 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13968 13050 603 41 0 13927 0
vsize: 55872
[startup+240.001 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 32223
Raw data (stat): 32223 (minisat+) R 32222 25285 25284 0 -1 0 13579 0 0 0 23968 32 0 0 25 0 1 0 488413023 57618432 13127 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14067 13127 603 41 0 14026 0
vsize: 56268
[startup+250.001 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 32223
Raw data (stat): 32223 (minisat+) R 32222 25285 25284 0 -1 0 13620 0 0 0 24968 32 0 0 25 0 1 0 488413023 57757696 13168 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14101 13168 603 41 0 14060 0
vsize: 56404
[startup+260.001 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 32223
Raw data (stat): 32223 (minisat+) R 32222 25285 25284 0 -1 0 13678 0 0 0 25968 32 0 0 25 0 1 0 488413023 58028032 13226 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14167 13226 603 41 0 14126 0
vsize: 56668
[startup+270.001 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 32223
Raw data (stat): 32223 (minisat+) R 32222 25285 25284 0 -1 0 13793 0 0 0 26968 33 0 0 25 0 1 0 488413023 58425344 13341 4294967295 134512640 134672761 3221224624 3221223792 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14264 13341 603 41 0 14223 0
vsize: 57056
[startup+280.002 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 32223
Raw data (stat): 32223 (minisat+) R 32222 25285 25284 0 -1 0 13949 0 0 0 27968 33 0 0 25 0 1 0 488413023 59092992 13497 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14427 13497 603 41 0 14386 0
vsize: 57708
[startup+290.002 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 32223
Raw data (stat): 32223 (minisat+) R 32222 25285 25284 0 -1 0 14100 0 0 0 28968 33 0 0 25 0 1 0 488413023 59633664 13648 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14559 13648 603 41 0 14518 0
vsize: 58236
[startup+300.002 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 32223
Raw data (stat): 32223 (minisat+) R 32222 25285 25284 0 -1 0 14282 0 0 0 29967 33 0 0 25 0 1 0 488413023 60444672 13830 4294967295 134512640 134672761 3221224624 3221223824 134557895 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14757 13830 603 41 0 14716 0
vsize: 59028
[startup+310.002 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 32223
Raw data (stat): 32223 (minisat+) R 32222 25285 25284 0 -1 0 14430 0 0 0 30967 34 0 0 25 0 1 0 488413023 60985344 13978 4294967295 134512640 134672761 3221224624 3221223792 134561375 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14889 13978 603 41 0 14848 0
vsize: 59556
[startup+320.002 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 32223
Raw data (stat): 32223 (minisat+) R 32222 25285 25284 0 -1 0 14620 0 0 0 31967 34 0 0 25 0 1 0 488413023 61796352 14168 4294967295 134512640 134672761 3221224624 3221223760 134560718 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15087 14168 603 41 0 15046 0
vsize: 60348
[startup+330.002 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 32223
Raw data (stat): 32223 (minisat+) R 32222 25285 25284 0 -1 0 14787 0 0 0 32966 35 0 0 25 0 1 0 488413023 62468096 14335 4294967295 134512640 134672761 3221224624 3221223728 134560235 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15251 14335 603 41 0 15210 0
vsize: 61004
[startup+340.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32223
Raw data (stat): 32223 (minisat+) R 32222 25285 25284 0 -1 0 15008 0 0 0 33965 36 0 0 25 0 1 0 488413023 63410176 14556 4294967295 134512640 134672761 3221224624 3221223792 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15481 14556 603 41 0 15440 0
vsize: 61924
[startup+350.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32223
Raw data (stat): 32223 (minisat+) R 32222 25285 25284 0 -1 0 15102 0 0 0 34964 37 0 0 25 0 1 0 488413023 63815680 14650 4294967295 134512640 134672761 3221224624 3221223796 134556639 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15580 14650 603 41 0 15539 0
vsize: 62320
[startup+360.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32223
Raw data (stat): 32223 (minisat+) R 32222 25285 25284 0 -1 0 15162 0 0 0 35963 37 0 0 25 0 1 0 488413023 64086016 14710 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15646 14710 603 41 0 15605 0
vsize: 62584
[startup+370.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32223
Raw data (stat): 32223 (minisat+) R 32222 25285 25284 0 -1 0 15290 0 0 0 36963 37 0 0 25 0 1 0 488413023 64491520 14838 4294967295 134512640 134672761 3221224624 3221223792 134560839 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15745 14838 603 41 0 15704 0
vsize: 62980
[startup+380.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32223
Raw data (stat): 32223 (minisat+) R 32222 25285 25284 0 -1 0 15637 0 0 0 37962 38 0 0 25 0 1 0 488413023 65986560 15185 4294967295 134512640 134672761 3221224624 3221223728 134560293 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16110 15185 603 41 0 16069 0
vsize: 64440
[startup+390.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32223
Raw data (stat): 32223 (minisat+) R 32222 25285 25284 0 -1 0 15963 0 0 0 38962 39 0 0 25 0 1 0 488413023 67325952 15511 4294967295 134512640 134672761 3221224624 3221223776 134541816 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16437 15511 603 41 0 16396 0
vsize: 65748
[startup+400.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32223
Raw data (stat): 32223 (minisat+) R 32222 25285 25284 0 -1 0 16231 0 0 0 39961 40 0 0 25 0 1 0 488413023 68399104 15779 4294967295 134512640 134672761 3221224624 3221223824 134557828 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16699 15779 603 41 0 16658 0
vsize: 66796
[startup+410.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32223
Raw data (stat): 32223 (minisat+) R 32222 25285 25284 0 -1 0 16553 0 0 0 40960 40 0 0 25 0 1 0 488413023 69742592 16101 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17027 16101 603 41 0 16986 0
vsize: 68108
[startup+420.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32223
Raw data (stat): 32223 (minisat+) R 32222 25285 25284 0 -1 0 16955 0 0 0 41959 42 0 0 25 0 1 0 488413023 71340032 16503 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17417 16503 603 41 0 17376 0
vsize: 69668
[startup+430.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32223
Raw data (stat): 32223 (minisat+) R 32222 25285 25284 0 -1 0 17345 0 0 0 42958 43 0 0 25 0 1 0 488413023 73080832 16893 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17842 16893 603 41 0 17801 0
vsize: 71368
[startup+440.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32223
Raw data (stat): 32223 (minisat+) R 32222 25285 25284 0 -1 0 17753 0 0 0 43957 44 0 0 25 0 1 0 488413023 74690560 17301 4294967295 134512640 134672761 3221224624 3221223792 134560999 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18235 17301 603 41 0 18194 0
vsize: 72940
[startup+450.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32223
Raw data (stat): 32223 (minisat+) R 32222 25285 25284 0 -1 0 18135 0 0 0 44956 45 0 0 25 0 1 0 488413023 76304384 17683 4294967295 134512640 134672761 3221224624 3221223728 134560246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18629 17683 603 41 0 18588 0
vsize: 74516
[startup+460.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32223
Raw data (stat): 32223 (minisat+) R 32222 25285 25284 0 -1 0 18519 0 0 0 45955 47 0 0 25 0 1 0 488413023 77918208 18067 4294967295 134512640 134672761 3221224624 3221223792 134560988 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19023 18067 603 41 0 18982 0
vsize: 76092
[startup+470.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32223
Raw data (stat): 32223 (minisat+) R 32222 25285 25284 0 -1 0 18944 0 0 0 46954 48 0 0 25 0 1 0 488413023 79671296 18492 4294967295 134512640 134672761 3221224624 3221223824 134557809 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19451 18492 603 41 0 19410 0
vsize: 77804
[startup+480.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32223
Raw data (stat): 32223 (minisat+) R 32222 25285 25284 0 -1 0 19360 0 0 0 47952 50 0 0 25 0 1 0 488413023 81285120 18908 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19845 18908 603 41 0 19804 0
vsize: 79380
[startup+490.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32223
Raw data (stat): 32223 (minisat+) R 32222 25285 25284 0 -1 0 19671 0 0 0 48952 50 0 0 25 0 1 0 488413023 82644992 19219 4294967295 134512640 134672761 3221224624 3221223728 134559862 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20177 19219 603 41 0 20136 0
vsize: 80708
[startup+500.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32223
Raw data (stat): 32223 (minisat+) R 32222 25285 25284 0 -1 0 19909 0 0 0 49951 51 0 0 25 0 1 0 488413023 83574784 19457 4294967295 134512640 134672761 3221224624 3221223824 134557828 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20404 19457 603 41 0 20363 0
vsize: 81616
[startup+510.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32223
Raw data (stat): 32223 (minisat+) R 32222 25285 25284 0 -1 0 20120 0 0 0 50950 52 0 0 25 0 1 0 488413023 84381696 19668 4294967295 134512640 134672761 3221224624 3221223808 134558671 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20601 19668 603 41 0 20560 0
vsize: 82404
[startup+520.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32223
Raw data (stat): 32223 (minisat+) R 32222 25285 25284 0 -1 0 20317 0 0 0 51950 52 0 0 25 0 1 0 488413023 85188608 19865 4294967295 134512640 134672761 3221224624 3221223728 134559787 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20798 19865 603 41 0 20757 0
vsize: 83192
[startup+530.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32223
Raw data (stat): 32223 (minisat+) R 32222 25285 25284 0 -1 0 20520 0 0 0 52950 53 0 0 25 0 1 0 488413023 85995520 20068 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20995 20068 603 41 0 20954 0
vsize: 83980
[startup+540.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32223
Raw data (stat): 32223 (minisat+) R 32222 25285 25284 0 -1 0 20678 0 0 0 53949 53 0 0 25 0 1 0 488413023 86671360 20226 4294967295 134512640 134672761 3221224624 3221223808 134558656 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21160 20226 603 41 0 21119 0
vsize: 84640
[startup+550.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32223
Raw data (stat): 32223 (minisat+) R 32222 25285 25284 0 -1 0 20770 0 0 0 54949 54 0 0 25 0 1 0 488413023 87076864 20318 4294967295 134512640 134672761 3221224624 3221223792 134560892 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21259 20318 603 41 0 21218 0
vsize: 85036
[startup+560.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32223
Raw data (stat): 32223 (minisat+) R 32222 25285 25284 0 -1 0 20825 0 0 0 55950 54 0 0 25 0 1 0 488413023 87347200 20373 4294967295 134512640 134672761 3221224624 3221223792 134560895 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21325 20373 603 41 0 21284 0
vsize: 85300
[startup+570.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32223
Raw data (stat): 32223 (minisat+) R 32222 25285 25284 0 -1 0 21164 0 0 0 56949 55 0 0 25 0 1 0 488413023 88690688 20712 4294967295 134512640 134672761 3221224624 3221223728 134560048 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21653 20712 603 41 0 21612 0
vsize: 86612
[startup+580.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32223
Raw data (stat): 32223 (minisat+) R 32222 25285 25284 0 -1 0 21351 0 0 0 57948 56 0 0 25 0 1 0 488413023 89489408 20899 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21848 20899 603 41 0 21807 0
vsize: 87392
[startup+590.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32223
Raw data (stat): 32223 (minisat+) R 32222 25285 25284 0 -1 0 21463 0 0 0 58948 56 0 0 25 0 1 0 488413023 89894912 21011 4294967295 134512640 134672761 3221224624 3221223792 134561118 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21947 21011 603 41 0 21906 0
vsize: 87788
[startup+600.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32223
Raw data (stat): 32223 (minisat+) R 32222 25285 25284 0 -1 0 21558 0 0 0 59947 57 0 0 25 0 1 0 488413023 90300416 21106 4294967295 134512640 134672761 3221224624 3221223760 134560677 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22046 21106 603 41 0 22005 0
vsize: 88184
[startup+610.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32223
Raw data (stat): 32223 (minisat+) R 32222 25285 25284 0 -1 0 21638 0 0 0 60947 57 0 0 25 0 1 0 488413023 90570752 21186 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22112 21186 603 41 0 22071 0
vsize: 88448
[startup+620.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32223
Raw data (stat): 32223 (minisat+) R 32222 25285 25284 0 -1 0 21794 0 0 0 61946 58 0 0 25 0 1 0 488413023 91246592 21342 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22277 21342 603 41 0 22236 0
vsize: 89108
[startup+630.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32223
Raw data (stat): 32223 (minisat+) R 32222 25285 25284 0 -1 0 22087 0 0 0 62946 59 0 0 25 0 1 0 488413023 92459008 21635 4294967295 134512640 134672761 3221224624 3221223792 134560920 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22573 21635 603 41 0 22532 0
vsize: 90292
[startup+640.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32223
Raw data (stat): 32223 (minisat+) R 32222 25285 25284 0 -1 0 22331 0 0 0 63945 60 0 0 25 0 1 0 488413023 93396992 21879 4294967295 134512640 134672761 3221224624 3221223792 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22802 21879 603 41 0 22761 0
vsize: 91208
[startup+650.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32223
Raw data (stat): 32223 (minisat+) R 32222 25285 25284 0 -1 0 22365 0 0 0 64945 60 0 0 25 0 1 0 488413023 93528064 21913 4294967295 134512640 134672761 3221224624 3221223796 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22834 21913 603 41 0 22793 0
vsize: 91336
[startup+660.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32223
Raw data (stat): 32223 (minisat+) R 32222 25285 25284 0 -1 0 22453 0 0 0 65945 60 0 0 25 0 1 0 488413023 93933568 22001 4294967295 134512640 134672761 3221224624 3221223792 134561269 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22933 22001 603 41 0 22892 0
vsize: 91732
[startup+670.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32223
Raw data (stat): 32223 (minisat+) R 32222 25285 25284 0 -1 0 22581 0 0 0 66945 60 0 0 25 0 1 0 488413023 94474240 22129 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23065 22129 603 41 0 23024 0
vsize: 92260
[startup+680.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32223
Raw data (stat): 32223 (minisat+) R 32222 25285 25284 0 -1 0 22755 0 0 0 67945 61 0 0 25 0 1 0 488413023 95145984 22303 4294967295 134512640 134672761 3221224624 3221223824 134557895 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23229 22303 603 41 0 23188 0
vsize: 92916
[startup+690.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32223
Raw data (stat): 32223 (minisat+) R 32222 25285 25284 0 -1 0 22958 0 0 0 68944 61 0 0 25 0 1 0 488413023 95956992 22506 4294967295 134512640 134672761 3221224624 3221223808 134558656 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23427 22506 603 41 0 23386 0
vsize: 93708
[startup+700.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32223
Raw data (stat): 32223 (minisat+) R 32222 25285 25284 0 -1 0 23128 0 0 0 69944 62 0 0 25 0 1 0 488413023 96624640 22676 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23590 22676 603 41 0 23549 0
vsize: 94360
[startup+710.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32223
Raw data (stat): 32223 (minisat+) R 32222 25285 25284 0 -1 0 23339 0 0 0 70943 63 0 0 25 0 1 0 488413023 97562624 22887 4294967295 134512640 134672761 3221224624 3221223728 134559877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23819 22887 603 41 0 23778 0
vsize: 95276
[startup+720.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32223
Raw data (stat): 32223 (minisat+) R 32222 25285 25284 0 -1 0 23529 0 0 0 71943 63 0 0 25 0 1 0 488413023 98373632 23077 4294967295 134512640 134672761 3221224624 3221223728 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24017 23077 603 41 0 23976 0
vsize: 96068
[startup+730.015 s]
Raw data (loadavg): 0.99 0.97 0.91 3/55 32224
Raw data (stat): 32223 (minisat+) R 32222 25285 25284 0 -1 0 23721 0 0 0 72942 65 0 0 25 0 1 0 488413023 99049472 23269 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24182 23269 603 41 0 24141 0
vsize: 96728
[startup+740.016 s]
Raw data (loadavg): 1.07 0.99 0.91 2/54 32276
Raw data (stat): 32223 (minisat+) R 32222 25285 25284 0 -1 0 23955 0 0 0 73941 66 0 0 25 0 1 0 488413023 100122624 23503 4294967295 134512640 134672761 3221224624 3221223728 134559914 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24444 23503 603 41 0 24403 0
vsize: 97776
[startup+750.016 s]
Raw data (loadavg): 1.06 0.99 0.91 2/54 32276
Raw data (stat): 32223 (minisat+) R 32222 25285 25284 0 -1 0 24073 0 0 0 74941 66 0 0 25 0 1 0 488413023 100528128 23621 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24543 23621 603 41 0 24502 0
vsize: 98172
[startup+760.016 s]
Raw data (loadavg): 1.05 0.99 0.91 2/54 32276
Raw data (stat): 32223 (minisat+) R 32222 25285 25284 0 -1 0 24181 0 0 0 75940 67 0 0 25 0 1 0 488413023 100933632 23729 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24642 23729 603 41 0 24601 0
vsize: 98568
[startup+770.016 s]
Raw data (loadavg): 1.04 0.99 0.91 2/54 32276
Raw data (stat): 32223 (minisat+) R 32222 25285 25284 0 -1 0 24280 0 0 0 76940 68 0 0 25 0 1 0 488413023 101335040 23828 4294967295 134512640 134672761 3221224624 3221223792 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24740 23828 603 41 0 24699 0
vsize: 98960
[startup+780.016 s]
Raw data (loadavg): 1.03 0.99 0.91 2/54 32276
Raw data (stat): 32223 (minisat+) R 32222 25285 25284 0 -1 0 24377 0 0 0 77939 68 0 0 25 0 1 0 488413023 101732352 23925 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24837 23925 603 41 0 24796 0
vsize: 99348
[startup+790.016 s]
Raw data (loadavg): 1.03 0.99 0.91 2/54 32276
Raw data (stat): 32223 (minisat+) R 32222 25285 25284 0 -1 0 24472 0 0 0 78939 69 0 0 25 0 1 0 488413023 102133760 24020 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24935 24020 603 41 0 24894 0
vsize: 99740
[startup+800.016 s]
Raw data (loadavg): 1.02 0.99 0.91 2/54 32276
Raw data (stat): 32223 (minisat+) R 32222 25285 25284 0 -1 0 24569 0 0 0 79938 70 0 0 25 0 1 0 488413023 102539264 24117 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25034 24117 603 41 0 24993 0
vsize: 100136
[startup+810.017 s]
Raw data (loadavg): 1.02 0.99 0.91 2/54 32278
Raw data (stat): 32223 (minisat+) R 32222 25285 25284 0 -1 0 24774 0 0 0 80937 71 0 0 25 0 1 0 488413023 103350272 24322 4294967295 134512640 134672761 3221224624 3221223760 134560647 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25232 24322 603 41 0 25191 0
vsize: 100928
[startup+820.017 s]
Raw data (loadavg): 1.02 0.99 0.91 2/54 32278
Raw data (stat): 32223 (minisat+) R 32222 25285 25284 0 -1 0 24904 0 0 0 81936 72 0 0 25 0 1 0 488413023 103890944 24452 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25364 24452 603 41 0 25323 0
vsize: 101456
[startup+830.018 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 32278
Raw data (stat): 32223 (minisat+) R 32222 25285 25284 0 -1 0 25170 0 0 0 82935 73 0 0 25 0 1 0 488413023 104968192 24718 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25627 24718 603 41 0 25586 0
vsize: 102508
[startup+840.019 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 32278
Raw data (stat): 32223 (minisat+) R 32222 25285 25284 0 -1 0 25286 0 0 0 83934 74 0 0 25 0 1 0 488413023 105504768 24834 4294967295 134512640 134672761 3221224624 3221223768 134560630 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25758 24834 603 41 0 25717 0
vsize: 103032
[startup+850.018 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 32278
Raw data (stat): 32223 (minisat+) R 32222 25285 25284 0 -1 0 25365 0 0 0 84934 75 0 0 25 0 1 0 488413023 105775104 24913 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25824 24913 603 41 0 25783 0
vsize: 103296
[startup+860.019 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 32278
Raw data (stat): 32223 (minisat+) R 32222 25285 25284 0 -1 0 25526 0 0 0 85933 76 0 0 25 0 1 0 488413023 106442752 25074 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25987 25074 603 41 0 25946 0
vsize: 103948
[startup+870.018 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 32278
Raw data (stat): 32223 (minisat+) R 32222 25285 25284 0 -1 0 25963 0 0 0 86932 77 0 0 25 0 1 0 488413023 108462080 25511 4294967295 134512640 134672761 3221224624 3221223824 134557852 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26480 25511 603 41 0 26439 0
vsize: 105920
[startup+880.019 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 32278
Raw data (stat): 32223 (minisat+) R 32222 25285 25284 0 -1 0 26122 0 0 0 87931 78 0 0 25 0 1 0 488413023 109129728 25670 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26643 25670 603 41 0 26602 0
vsize: 106572
[startup+890.019 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 32278
Raw data (stat): 32223 (minisat+) R 32222 25285 25284 0 -1 0 26278 0 0 0 88930 79 0 0 25 0 1 0 488413023 109801472 25826 4294967295 134512640 134672761 3221224624 3221223728 134559925 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26807 25826 603 41 0 26766 0
vsize: 107228
[startup+900.019 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 32278
Raw data (stat): 32223 (minisat+) R 32222 25285 25284 0 -1 0 26448 0 0 0 89930 79 0 0 25 0 1 0 488413023 110477312 25996 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26972 25996 603 41 0 26931 0
vsize: 107888
[startup+910.019 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 32278
Raw data (stat): 32223 (minisat+) R 32222 25285 25284 0 -1 0 26649 0 0 0 90929 81 0 0 25 0 1 0 488413023 111288320 26197 4294967295 134512640 134672761 3221224624 3221223728 134560510 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27170 26197 603 41 0 27129 0
vsize: 108680
[startup+920.02 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 32278
Raw data (stat): 32223 (minisat+) R 32222 25285 25284 0 -1 0 26761 0 0 0 91929 81 0 0 25 0 1 0 488413023 111828992 26309 4294967295 134512640 134672761 3221224624 3221223792 134560909 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27302 26309 603 41 0 27261 0
vsize: 109208
[startup+930.02 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 32278
Raw data (stat): 32223 (minisat+) R 32222 25285 25284 0 -1 0 26900 0 0 0 92928 82 0 0 25 0 1 0 488413023 112369664 26448 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27434 26448 603 41 0 27393 0
vsize: 109736
[startup+940.02 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 32278
Raw data (stat): 32223 (minisat+) R 32222 25285 25284 0 -1 0 27053 0 0 0 93928 83 0 0 25 0 1 0 488413023 112910336 26601 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27566 26601 603 41 0 27525 0
vsize: 110264
[startup+950.02 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 32278
Raw data (stat): 32223 (minisat+) R 32222 25285 25284 0 -1 0 27223 0 0 0 94927 83 0 0 25 0 1 0 488413023 113709056 26771 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27761 26771 603 41 0 27720 0
vsize: 111044
[startup+960.021 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 32278
Raw data (stat): 32223 (minisat+) R 32222 25285 25284 0 -1 0 27327 0 0 0 95927 84 0 0 25 0 1 0 488413023 114114560 26875 4294967295 134512640 134672761 3221224624 3221223792 134560871 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27860 26875 603 41 0 27819 0
vsize: 111440
[startup+970.02 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 32278
Raw data (stat): 32223 (minisat+) R 32222 25285 25284 0 -1 0 27487 0 0 0 96927 84 0 0 25 0 1 0 488413023 114786304 27035 4294967295 134512640 134672761 3221224624 3221223824 134557842 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28024 27035 603 41 0 27983 0
vsize: 112096
[startup+980.022 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 32278
Raw data (stat): 32223 (minisat+) R 32222 25285 25284 0 -1 0 27621 0 0 0 97926 86 0 0 25 0 1 0 488413023 115322880 27169 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28155 27169 603 41 0 28114 0
vsize: 112620
[startup+990.021 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 32278
Raw data (stat): 32223 (minisat+) R 32222 25285 25284 0 -1 0 27742 0 0 0 98925 86 0 0 25 0 1 0 488413023 115728384 27290 4294967295 134512640 134672761 3221224624 3221223792 134560968 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28254 27290 603 41 0 28213 0
vsize: 113016
[startup+1000.02 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 32278
Raw data (stat): 32223 (minisat+) R 32222 25285 25284 0 -1 0 27956 0 0 0 99924 88 0 0 25 0 1 0 488413023 116662272 27504 4294967295 134512640 134672761 3221224624 3221223760 134560588 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28482 27504 603 41 0 28441 0
vsize: 113928
[startup+1010.02 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 32278
Raw data (stat): 32223 (minisat+) R 32222 25285 25284 0 -1 0 28225 0 0 0 100923 89 0 0 25 0 1 0 488413023 117739520 27773 4294967295 134512640 134672761 3221224624 3221223728 134560529 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28745 27773 603 41 0 28704 0
vsize: 114980
[startup+1020.02 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 32278
Raw data (stat): 32223 (minisat+) R 32222 25285 25284 0 -1 0 28494 0 0 0 101923 89 0 0 25 0 1 0 488413023 118816768 28042 4294967295 134512640 134672761 3221224624 3221223760 134565092 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29008 28042 603 41 0 28967 0
vsize: 116032
[startup+1030.02 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 32278
Raw data (stat): 32223 (minisat+) R 32222 25285 25284 0 -1 0 28748 0 0 0 102921 91 0 0 25 0 1 0 488413023 119885824 28296 4294967295 134512640 134672761 3221224624 3221223792 134560926 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29269 28296 603 41 0 29228 0
vsize: 117076
[startup+1040.02 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 32278
Raw data (stat): 32223 (minisat+) R 32222 25285 25284 0 -1 0 29057 0 0 0 103920 92 0 0 25 0 1 0 488413023 121085952 28605 4294967295 134512640 134672761 3221224624 3221223824 134557836 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29562 28605 603 41 0 29521 0
vsize: 118248
[startup+1050.02 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 32278
Raw data (stat): 32223 (minisat+) R 32222 25285 25284 0 -1 0 29422 0 0 0 104920 93 0 0 25 0 1 0 488413023 122691584 28970 4294967295 134512640 134672761 3221224624 3221223764 134560556 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29954 28970 603 41 0 29913 0
vsize: 119816
[startup+1060.02 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 32278
Raw data (stat): 32223 (minisat+) R 32222 25285 25284 0 -1 0 29779 0 0 0 105919 94 0 0 25 0 1 0 488413023 124047360 29327 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30285 29327 603 41 0 30244 0
vsize: 121140
[startup+1070.02 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 32280
Raw data (stat): 32223 (minisat+) R 32222 25285 25284 0 -1 0 30099 0 0 0 106918 95 0 0 25 0 1 0 488413023 125394944 29647 4294967295 134512640 134672761 3221224624 3221223760 134560697 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30614 29647 603 41 0 30573 0
vsize: 122456
[startup+1080.02 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 32280
Raw data (stat): 32223 (minisat+) R 32222 25285 25284 0 -1 0 30287 0 0 0 107917 96 0 0 25 0 1 0 488413023 126205952 29835 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30812 29835 603 41 0 30771 0
vsize: 123248
[startup+1090.02 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 32280
Raw data (stat): 32223 (minisat+) R 32222 25285 25284 0 -1 0 30388 0 0 0 108916 97 0 0 25 0 1 0 488413023 126611456 29936 4294967295 134512640 134672761 3221224624 3221223792 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30911 29936 603 41 0 30870 0
vsize: 123644
[startup+1100.02 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 32280
Raw data (stat): 32223 (minisat+) R 32222 25285 25284 0 -1 0 30497 0 0 0 109916 98 0 0 25 0 1 0 488413023 127012864 30045 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31009 30045 603 41 0 30968 0
vsize: 124036
[startup+1110.02 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 32280
Raw data (stat): 32223 (minisat+) R 32222 25285 25284 0 -1 0 30613 0 0 0 110915 98 0 0 25 0 1 0 488413023 127545344 30161 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31139 30161 603 41 0 31098 0
vsize: 124556
[startup+1120.02 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 32280
Raw data (stat): 32223 (minisat+) R 32222 25285 25284 0 -1 0 30770 0 0 0 111915 99 0 0 25 0 1 0 488413023 128077824 30318 4294967295 134512640 134672761 3221224624 3221223824 134557895 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31269 30318 603 41 0 31228 0
vsize: 125076
[startup+1130.03 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 32280
Raw data (stat): 32223 (minisat+) R 32222 25285 25284 0 -1 0 30915 0 0 0 112914 100 0 0 25 0 1 0 488413023 128749568 30463 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31433 30463 603 41 0 31392 0
vsize: 125732
[startup+1140.03 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 32280
Raw data (stat): 32223 (minisat+) R 32222 25285 25284 0 -1 0 31038 0 0 0 113914 100 0 0 25 0 1 0 488413023 129286144 30586 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31564 30586 603 41 0 31523 0
vsize: 126256
[startup+1150.03 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 32280
Raw data (stat): 32223 (minisat+) R 32222 25285 25284 0 -1 0 31169 0 0 0 114913 101 0 0 25 0 1 0 488413023 129818624 30717 4294967295 134512640 134672761 3221224624 3221223792 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31694 30717 603 41 0 31653 0
vsize: 126776
[startup+1160.03 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 32280
Raw data (stat): 32223 (minisat+) R 32222 25285 25284 0 -1 0 31344 0 0 0 115912 102 0 0 25 0 1 0 488413023 130494464 30892 4294967295 134512640 134672761 3221224624 3221223760 134560688 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31859 30892 603 41 0 31818 0
vsize: 127436
[startup+1170.03 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 32280
Raw data (stat): 32223 (minisat+) R 32222 25285 25284 0 -1 0 31505 0 0 0 116912 102 0 0 25 0 1 0 488413023 131166208 31053 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32023 31053 603 41 0 31982 0
vsize: 128092
[startup+1180.03 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 32280
Raw data (stat): 32223 (minisat+) R 32222 25285 25284 0 -1 0 31638 0 0 0 117912 103 0 0 25 0 1 0 488413023 131702784 31186 4294967295 134512640 134672761 3221224624 3221223792 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32154 31186 603 41 0 32113 0
vsize: 128616
[startup+1190.03 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 32280
Raw data (stat): 32223 (minisat+) R 32222 25285 25284 0 -1 0 31811 0 0 0 118912 104 0 0 25 0 1 0 488413023 132370432 31359 4294967295 134512640 134672761 3221224624 3221223728 134559862 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32317 31359 603 41 0 32276 0
vsize: 129268
[startup+1200.03 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 32280
Raw data (stat): 32223 (minisat+) R 32222 25285 25284 0 -1 0 32011 0 0 0 119911 104 0 0 25 0 1 0 488413023 133173248 31559 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32513 31559 603 41 0 32472 0
vsize: 130052
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.09 s]
Raw data (loadavg): 1.00 0.99 0.91 1/54 32280
Raw data (stat): 32223 (minisat+) Z 32222 25285 25284 0 -1 12 32013 0 0 0 119911 110 0 0 25 0 1 0 488413023 0 0 4294967295 0 0 0 0 0 0 16384 5 16386 3222412051 0 0 17 1 0 0
Raw data (statm): 0 0 0 0 0 0 0
vsize: 0
Maximum CPU time exceeded: sending SIGTERM and SIGKILL

Child status: 0
Real time (s): 1200.09
CPU time (s): 1200.22
CPU user time (s): 1199.12
CPU system time (s): 1.10683
CPU usage (%): 100.011
Max. virtual memory (Kb): 130052
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####