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 18859

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

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.169
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:        812448 kB
Buffers:         24804 kB
Cached:         175636 kB
SwapCached:        364 kB
Active:          31688 kB
Inactive:       171280 kB
HighTotal:      131008 kB
HighFree:        91252 kB
LowTotal:       903652 kB
LowFree:        721196 kB
SwapTotal:     2097136 kB
SwapFree:      2096356 kB
Dirty:              40 kB
Writeback:           0 kB
Mapped:           6400 kB
Slab:            13432 kB
Committed_AS:    71712 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1388 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-21 17:05:53 (client local time) WITH STATUS 0 IN 1200.29 SECONDS
stats: 17418 7 1200.29 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 =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |         0 |  523731  1830049 |  157119       0        0     nan |  0.000 % |
c   -- subsuming                       
c   -- var.elim.:  1000/96963          
c   -- var.elim.:  2000/96963          
c   -- var.elim.:  3000/96963          
c   -- var.elim.:  4000/96963          
c   -- var.elim.:  5000/96963          
c   -- var.elim.:  6000/96963          
c   -- var.elim.:  7000/96963          
c   -- var.elim.:  8000/96963          
c   -- var.elim.:  9000/96963          
c   -- var.elim.:  10000/96963          
c   -- var.elim.:  11000/96963          
c   -- var.elim.:  12000/96963          
c   -- var.elim.:  13000/96963          
c   -- var.elim.:  14000/96963          
c   -- var.elim.:  15000/96963          
c   -- var.elim.:  16000/96963          
c   -- var.elim.:  17000/96963          
c   -- var.elim.:  18000/96963          
c   -- var.elim.:  19000/96963          
c   -- var.elim.:  20000/96963          
c   -- var.elim.:  21000/96963          
c   -- var.elim.:  22000/96963          
c   -- var.elim.:  23000/96963          
c   -- var.elim.:  24000/96963          
c   -- var.elim.:  25000/96963          
c   -- var.elim.:  26000/96963          
c   -- var.elim.:  27000/96963          
c   -- var.elim.:  28000/96963          
c   -- var.elim.:  29000/96963          
c   -- var.elim.:  30000/96963          
c   -- var.elim.:  31000/96963          
c   -- var.elim.:  32000/96963          
c   -- var.elim.:  33000/96963          
c   -- var.elim.:  34000/96963          
c   -- var.elim.:  35000/96963          
c   -- var.elim.:  36000/96963          
c   -- var.elim.:  37000/96963          
c   -- var.elim.:  38000/96963          
c   -- var.elim.:  39000/96963          
c   -- var.elim.:  40000/96963          
c   -- var.elim.:  41000/96963          
c   -- var.elim.:  42000/96963          
c   -- var.elim.:  43000/96963          
c   -- var.elim.:  44000/96963          
c   -- var.elim.:  45000/96963          
c   -- var.elim.:  46000/96963          
c   -- var.elim.:  47000/96963          
c   -- var.elim.:  48000/96963          
c   -- var.elim.:  49000/96963          
c   -- var.elim.:  50000/96963          
c   -- var.elim.:  51000/96963          
c   -- var.elim.:  52000/96963          
c   -- var.elim.:  53000/96963          
c   -- var.elim.:  54000/96963          
c   -- var.elim.:  55000/96963          
c   -- var.elim.:  56000/96963          
c   -- var.elim.:  57000/96963          
c   -- var.elim.:  58000/96963          
c   -- var.elim.:  59000/96963          
c   -- var.elim.:  60000/96963          
c   -- var.elim.:  61000/96963          
c   -- var.elim.:  62000/96963          
c   -- var.elim.:  63000/96963          
c   -- var.elim.:  64000/96963          
c   -- var.elim.:  65000/96963          
c   -- var.elim.:  66000/96963          
c   -- var.elim.:  67000/96963          
c   -- var.elim.:  68000/96963          
c   -- var.elim.:  69000/96963          
c   -- var.elim.:  70000/96963          
c   -- var.elim.:  71000/96963          
c   -- var.elim.:  72000/96963          
c   -- var.elim.:  73000/96963          
c   -- var.elim.:  74000/96963          
c   -- var.elim.:  75000/96963          
c   -- var.elim.:  76000/96963          
c   -- var.elim.:  77000/96963          
c   -- var.elim.:  78000/96963          
c   -- var.elim.:  79000/96963          
c   -- var.elim.:  80000/96963          
c   -- var.elim.:  81000/96963          
c   -- var.elim.:  82000/96963          
c   -- var.elim.:  83000/96963          
c   -- var.elim.:  84000/96963          
c   -- var.elim.:  85000/96963          
c   -- var.elim.:  86000/96963          
c   -- var.elim.:  87000/96963          
c   -- var.elim.:  88000/96963          
c   -- var.elim.:  89000/96963          
c   -- var.elim.:  90000/96963          
c   -- var.elim.:  91000/96963          
c   -- var.elim.:  92000/96963          
c   -- var.elim.:  93000/96963          
c   -- var.elim.:  94000/96963          
c   -- var.elim.:  95000/96963          
c   -- var.elim.:  96000/96963          
c   -- var.elim.:  96963/96963          
c   -- var.elim.:  1000/11288          
c   -- var.elim.:  2000/11288          
c   -- var.elim.:  3000/11288          
c   -- var.elim.:  4000/11288          
c   -- var.elim.:  5000/11288          
c   -- var.elim.:  6000/11288          
c   -- var.elim.:  7000/11288          
c   -- var.elim.:  8000/11288          
c   -- var.elim.:  9000/11288          
c   -- var.elim.:  10000/11288          
c   -- var.elim.:  11000/11288          
c   -- var.elim.:  11288/11288          
c   -- subsuming                       
c   -- var.elim.:  908/908          
c   -- var.elim.:  186/186          
c   -- subsuming                       
c   -- var.elim.:  117/117          
c |         0 |  510354  1781127 |      --       0       --      -- |     --   | -7772/-17902
c |         0 |  510354  1781127 |  204141       0        0     nan |  0.000 % |
c |       103 |  510354  1781127 |  224555     103      415     4.0 |  4.631 % |
c |       254 |  510354  1781127 |  247011     254     1837     7.2 |  4.631 % |
c |       481 |  510354  1781127 |  271712     481     2694    #### 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.93 0.98 0.99 2/54 10637
Raw data (stat): 10637 (runsolver) R 10636 5897 5896 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 488399878 1052672 99 4294967295 134512640 135381576 3221224448 3221219692 135158418 0 2147483391 7 90112 0 0 0 17 1 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0011 s]
Raw data (loadavg): 0.94 0.98 0.99 2/54 10637
Raw data (stat): 10637 (minisat+) R 10636 5897 5896 0 -1 0 18703 0 0 0 947 52 0 0 25 0 1 0 488399878 81567744 18250 4294967295 134512640 134672761 3221224544 3221223136 134621515 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19914 18250 603 41 0 19873 0
vsize: 79656
[startup+20.0016 s]
Raw data (loadavg): 0.95 0.98 0.99 2/54 10637
Raw data (stat): 10637 (minisat+) R 10636 5897 5896 0 -1 0 22284 0 0 0 1936 63 0 0 25 0 1 0 488399878 83185664 18774 4294967295 134512640 134672761 3221224544 3221223584 134614266 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20309 18774 603 41 0 20268 0
vsize: 81236
[startup+30.002 s]
Raw data (loadavg): 0.95 0.98 0.99 2/54 10637
Raw data (stat): 10637 (minisat+) R 10636 5897 5896 0 -1 0 23376 0 0 0 2933 65 0 0 25 0 1 0 488399878 87580672 19866 4294967295 134512640 134672761 3221224544 3221223728 134615804 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21382 19866 603 41 0 21341 0
vsize: 85528
[startup+40.003 s]
Raw data (loadavg): 0.96 0.98 0.99 2/54 10637
Raw data (stat): 10637 (minisat+) R 10636 5897 5896 0 -1 0 23949 0 0 0 3931 68 0 0 25 0 1 0 488399878 90091520 20439 4294967295 134512640 134672761 3221224544 3221223584 134612659 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21995 20439 603 41 0 21954 0
vsize: 87980
[startup+50.0031 s]
Raw data (loadavg): 0.97 0.98 0.99 2/54 10637
Raw data (stat): 10637 (minisat+) R 10636 5897 5896 0 -1 0 24647 0 0 0 4929 70 0 0 25 0 1 0 488399878 92889088 21137 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22678 21137 603 41 0 22637 0
vsize: 90712
[startup+60.0044 s]
Raw data (loadavg): 0.97 0.98 0.99 2/54 10637
Raw data (stat): 10637 (minisat+) R 10636 5897 5896 0 -1 0 25221 0 0 0 5927 72 0 0 25 0 1 0 488399878 95293440 21711 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23265 21711 603 41 0 23224 0
vsize: 93060
[startup+70.0054 s]
Raw data (loadavg): 0.97 0.98 0.99 2/54 10637
Raw data (stat): 10637 (minisat+) R 10636 5897 5896 0 -1 0 25663 0 0 0 6924 75 0 0 25 0 1 0 488399878 97140736 22153 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23716 22153 603 41 0 23675 0
vsize: 94864
[startup+80.0057 s]
Raw data (loadavg): 0.98 0.98 0.99 2/54 10637
Raw data (stat): 10637 (minisat+) R 10636 5897 5896 0 -1 0 26213 0 0 0 7922 77 0 0 25 0 1 0 488399878 99266560 22703 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24235 22703 603 41 0 24194 0
vsize: 96940
[startup+90.006 s]
Raw data (loadavg): 0.98 0.98 0.99 2/54 10637
Raw data (stat): 10637 (minisat+) R 10636 5897 5896 0 -1 0 27174 0 0 0 8919 80 0 0 25 0 1 0 488399878 103505920 23664 4294967295 134512640 134672761 3221224544 3221223696 134565101 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25270 23664 603 41 0 25229 0
vsize: 101080
[startup+100.006 s]
Raw data (loadavg): 0.98 0.98 0.99 2/54 10637
Raw data (stat): 10637 (minisat+) R 10636 5897 5896 0 -1 0 27835 0 0 0 9916 83 0 0 25 0 1 0 488399878 106143744 24325 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25914 24325 603 41 0 25873 0
vsize: 103656
[startup+110.007 s]
Raw data (loadavg): 0.99 0.98 0.99 2/54 10637
Raw data (stat): 10637 (minisat+) R 10636 5897 5896 0 -1 0 28434 0 0 0 10915 85 0 0 25 0 1 0 488399878 108650496 24924 4294967295 134512640 134672761 3221224544 3221223728 134615638 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26526 24924 603 41 0 26485 0
vsize: 106104
[startup+120.009 s]
Raw data (loadavg): 0.99 0.98 0.99 2/54 10637
Raw data (stat): 10637 (minisat+) R 10636 5897 5896 0 -1 0 28989 0 0 0 11913 87 0 0 25 0 1 0 488399878 110923776 25479 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27081 25479 603 41 0 27040 0
vsize: 108324
[startup+130.008 s]
Raw data (loadavg): 0.99 0.98 0.99 2/54 10637
Raw data (stat): 10637 (minisat+) R 10636 5897 5896 0 -1 0 29959 0 0 0 12910 90 0 0 25 0 1 0 488399878 114900992 26449 4294967295 134512640 134672761 3221224544 3221223728 134615671 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28052 26449 603 41 0 28011 0
vsize: 112208
[startup+140.009 s]
Raw data (loadavg): 0.99 0.98 0.99 2/54 10637
Raw data (stat): 10637 (minisat+) R 10636 5897 5896 0 -1 0 30793 0 0 0 13907 92 0 0 25 0 1 0 488399878 118235136 27283 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28866 27283 603 41 0 28825 0
vsize: 115464
[startup+150.01 s]
Raw data (loadavg): 0.99 0.98 0.99 2/54 10637
Raw data (stat): 10637 (minisat+) R 10636 5897 5896 0 -1 0 31388 0 0 0 14906 93 0 0 25 0 1 0 488399878 120750080 27878 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29480 27878 603 41 0 29439 0
vsize: 117920
[startup+160.011 s]
Raw data (loadavg): 0.99 0.98 0.99 2/54 10637
Raw data (stat): 10637 (minisat+) R 10636 5897 5896 0 -1 0 31890 0 0 0 15904 95 0 0 25 0 1 0 488399878 122740736 28380 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29966 28380 603 41 0 29925 0
vsize: 119864
[startup+170.011 s]
Raw data (loadavg): 0.99 0.98 0.99 2/54 10637
Raw data (stat): 10637 (minisat+) R 10636 5897 5896 0 -1 0 32272 0 0 0 16903 98 0 0 25 0 1 0 488399878 124334080 28762 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30355 28762 603 41 0 30314 0
vsize: 121420
[startup+180.012 s]
Raw data (loadavg): 0.99 0.98 0.99 2/54 10637
Raw data (stat): 10637 (minisat+) R 10636 5897 5896 0 -1 0 32699 0 0 0 17901 99 0 0 25 0 1 0 488399878 126058496 29189 4294967295 134512640 134672761 3221224544 3221223728 134615833 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30776 29189 603 41 0 30735 0
vsize: 123104
[startup+190.013 s]
Raw data (loadavg): 0.99 0.98 0.99 2/54 10637
Raw data (stat): 10637 (minisat+) R 10636 5897 5896 0 -1 0 33068 0 0 0 18899 101 0 0 25 0 1 0 488399878 127516672 29558 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31132 29558 603 41 0 31091 0
vsize: 124528
[startup+200.013 s]
Raw data (loadavg): 0.99 0.98 0.99 2/54 10637
Raw data (stat): 10637 (minisat+) R 10636 5897 5896 0 -1 0 33444 0 0 0 19898 103 0 0 25 0 1 0 488399878 129101824 29934 4294967295 134512640 134672761 3221224544 3221223728 134615833 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31519 29934 603 41 0 31478 0
vsize: 126076
[startup+210.014 s]
Raw data (loadavg): 0.99 0.98 0.99 2/54 10637
Raw data (stat): 10637 (minisat+) R 10636 5897 5896 0 -1 0 33841 0 0 0 20897 104 0 0 25 0 1 0 488399878 131293184 30331 4294967295 134512640 134672761 3221224544 3221223728 134615549 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32054 30331 603 41 0 32013 0
vsize: 128216
[startup+220.015 s]
Raw data (loadavg): 0.99 0.98 0.99 2/54 10637
Raw data (stat): 10637 (minisat+) R 10636 5897 5896 0 -1 0 34237 0 0 0 21895 106 0 0 25 0 1 0 488399878 132902912 30727 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32447 30727 603 41 0 32406 0
vsize: 129788
[startup+230.016 s]
Raw data (loadavg): 0.99 0.98 0.99 2/54 10637
Raw data (stat): 10637 (minisat+) R 10636 5897 5896 0 -1 0 34530 0 0 0 22894 107 0 0 25 0 1 0 488399878 134098944 31020 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32739 31020 603 41 0 32698 0
vsize: 130956
[startup+240.016 s]
Raw data (loadavg): 0.99 0.98 0.99 2/54 10637
Raw data (stat): 10637 (minisat+) R 10636 5897 5896 0 -1 0 34874 0 0 0 23893 108 0 0 25 0 1 0 488399878 135462912 31364 4294967295 134512640 134672761 3221224544 3221223728 134615571 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33072 31364 603 41 0 33031 0
vsize: 132288
[startup+250.017 s]
Raw data (loadavg): 0.99 0.98 0.99 2/54 10637
Raw data (stat): 10637 (minisat+) R 10636 5897 5896 0 -1 0 35171 0 0 0 24893 109 0 0 25 0 1 0 488399878 136650752 31661 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33362 31661 603 41 0 33321 0
vsize: 133448
[startup+260.018 s]
Raw data (loadavg): 0.99 0.98 0.99 2/54 10637
Raw data (stat): 10637 (minisat+) R 10636 5897 5896 0 -1 0 35440 0 0 0 25892 110 0 0 25 0 1 0 488399878 137773056 31930 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33636 31930 603 41 0 33595 0
vsize: 134544
[startup+270.019 s]
Raw data (loadavg): 0.99 0.98 0.99 2/54 10637
Raw data (stat): 10637 (minisat+) R 10636 5897 5896 0 -1 0 35717 0 0 0 26892 110 0 0 25 0 1 0 488399878 138883072 32207 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33907 32207 603 41 0 33866 0
vsize: 135628
[startup+280.019 s]
Raw data (loadavg): 0.99 0.98 0.99 2/54 10637
Raw data (stat): 10637 (minisat+) R 10636 5897 5896 0 -1 0 35975 0 0 0 27890 111 0 0 25 0 1 0 488399878 139960320 32465 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 34170 32465 603 41 0 34129 0
vsize: 136680
[startup+290.02 s]
Raw data (loadavg): 0.99 0.98 0.99 2/54 10637
Raw data (stat): 10637 (minisat+) R 10636 5897 5896 0 -1 0 36221 0 0 0 28890 112 0 0 25 0 1 0 488399878 141008896 32711 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 34426 32711 603 41 0 34385 0
vsize: 137704
[startup+300.02 s]
Raw data (loadavg): 0.99 0.98 0.99 2/54 10637
Raw data (stat): 10637 (minisat+) R 10636 5897 5896 0 -1 0 36453 0 0 0 29889 112 0 0 25 0 1 0 488399878 141996032 32943 4294967295 134512640 134672761 3221224544 3221223584 134614228 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 34667 32943 603 41 0 34626 0
vsize: 138668
[startup+310.021 s]
Raw data (loadavg): 0.99 0.98 0.99 2/54 10637
Raw data (stat): 10637 (minisat+) R 10636 5897 5896 0 -1 0 36700 0 0 0 30889 113 0 0 25 0 1 0 488399878 143056896 33190 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 34926 33190 603 41 0 34885 0
vsize: 139704
[startup+320.021 s]
Raw data (loadavg): 0.99 0.98 0.99 2/54 10637
Raw data (stat): 10637 (minisat+) R 10636 5897 5896 0 -1 0 36936 0 0 0 31888 114 0 0 25 0 1 0 488399878 143994880 33426 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 35155 33426 603 41 0 35114 0
vsize: 140620
[startup+330.021 s]
Raw data (loadavg): 0.99 0.98 0.99 2/54 10637
Raw data (stat): 10637 (minisat+) R 10636 5897 5896 0 -1 0 37125 0 0 0 32887 115 0 0 25 0 1 0 488399878 144789504 33615 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 35349 33615 603 41 0 35308 0
vsize: 141396
[startup+340.022 s]
Raw data (loadavg): 0.99 0.98 0.99 2/54 10637
Raw data (stat): 10637 (minisat+) R 10636 5897 5896 0 -1 0 37329 0 0 0 33887 116 0 0 25 0 1 0 488399878 145608704 33819 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 35549 33819 603 41 0 35508 0
vsize: 142196
[startup+350.022 s]
Raw data (loadavg): 0.99 0.98 0.99 2/54 10637
Raw data (stat): 10637 (minisat+) R 10636 5897 5896 0 -1 0 37521 0 0 0 34886 116 0 0 25 0 1 0 488399878 146395136 34011 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 35741 34011 603 41 0 35700 0
vsize: 142964
[startup+360.023 s]
Raw data (loadavg): 0.99 0.98 0.99 2/54 10637
Raw data (stat): 10637 (minisat+) R 10636 5897 5896 0 -1 0 37736 0 0 0 35886 117 0 0 25 0 1 0 488399878 147189760 34226 4294967295 134512640 134672761 3221224544 3221223728 134615830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 35935 34226 603 41 0 35894 0
vsize: 143740
[startup+370.023 s]
Raw data (loadavg): 0.99 0.98 0.99 2/54 10637
Raw data (stat): 10637 (minisat+) R 10636 5897 5896 0 -1 0 37910 0 0 0 36885 118 0 0 25 0 1 0 488399878 147992576 34400 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 36131 34400 603 41 0 36090 0
vsize: 144524
[startup+380.022 s]
Raw data (loadavg): 0.99 0.98 0.99 2/54 10637
Raw data (stat): 10637 (minisat+) R 10636 5897 5896 0 -1 0 38093 0 0 0 37884 119 0 0 25 0 1 0 488399878 148647936 34583 4294967295 134512640 134672761 3221224544 3221223728 134615833 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 36291 34583 603 41 0 36250 0
vsize: 145164
[startup+390.022 s]
Raw data (loadavg): 0.99 0.98 0.99 2/54 10637
Raw data (stat): 10637 (minisat+) R 10636 5897 5896 0 -1 0 38263 0 0 0 38883 120 0 0 25 0 1 0 488399878 149434368 34753 4294967295 134512640 134672761 3221224544 3221223728 134615663 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 36483 34753 603 41 0 36442 0
vsize: 145932
[startup+400.024 s]
Raw data (loadavg): 0.99 0.98 0.99 2/54 10637
Raw data (stat): 10637 (minisat+) R 10636 5897 5896 0 -1 0 38579 0 0 0 39883 120 0 0 25 0 1 0 488399878 150663168 35069 4294967295 134512640 134672761 3221224544 3221223728 134615705 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 36783 35069 603 41 0 36742 0
vsize: 147132
[startup+410.024 s]
Raw data (loadavg): 0.99 0.98 0.99 2/54 10637
Raw data (stat): 10637 (minisat+) R 10636 5897 5896 0 -1 0 39098 0 0 0 40881 122 0 0 25 0 1 0 488399878 152809472 35588 4294967295 134512640 134672761 3221224544 3221223728 134615652 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 37307 35588 603 41 0 37266 0
vsize: 149228
[startup+420.024 s]
Raw data (loadavg): 0.99 0.98 0.99 2/54 10637
Raw data (stat): 10637 (minisat+) R 10636 5897 5896 0 -1 0 39564 0 0 0 41880 124 0 0 25 0 1 0 488399878 154796032 36054 4294967295 134512640 134672761 3221224544 3221223728 134615791 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 37792 36054 603 41 0 37751 0
vsize: 151168
[startup+430.024 s]
Raw data (loadavg): 0.99 0.98 0.99 2/54 10637
Raw data (stat): 10637 (minisat+) R 10636 5897 5896 0 -1 0 40078 0 0 0 42878 125 0 0 25 0 1 0 488399878 156905472 36568 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 38307 36568 603 41 0 38266 0
vsize: 153228
[startup+440.025 s]
Raw data (loadavg): 0.99 0.98 0.99 2/54 10637
Raw data (stat): 10637 (minisat+) R 10636 5897 5896 0 -1 0 40561 0 0 0 43877 127 0 0 25 0 1 0 488399878 158883840 37051 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 38790 37051 603 41 0 38749 0
vsize: 155160
[startup+450.025 s]
Raw data (loadavg): 0.99 0.98 0.99 2/54 10637
Raw data (stat): 10637 (minisat+) R 10636 5897 5896 0 -1 0 40924 0 0 0 44875 129 0 0 25 0 1 0 488399878 160329728 37414 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39143 37414 603 41 0 39102 0
vsize: 156572
[startup+460.026 s]
Raw data (loadavg): 0.99 0.98 0.99 2/54 10637
Raw data (stat): 10637 (minisat+) R 10636 5897 5896 0 -1 0 41324 0 0 0 45874 130 0 0 25 0 1 0 488399878 161902592 37814 4294967295 134512640 134672761 3221224544 3221223584 134614205 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39527 37814 603 41 0 39486 0
vsize: 158108
[startup+470.026 s]
Raw data (loadavg): 0.99 0.98 0.99 2/54 10637
Raw data (stat): 10637 (minisat+) R 10636 5897 5896 0 -1 0 41724 0 0 0 46872 131 0 0 25 0 1 0 488399878 163610624 38214 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39944 38214 603 41 0 39903 0
vsize: 159776
[startup+480.026 s]
Raw data (loadavg): 0.99 0.98 0.99 2/54 10637
Raw data (stat): 10637 (minisat+) R 10636 5897 5896 0 -1 0 42077 0 0 0 47871 133 0 0 25 0 1 0 488399878 165089280 38567 4294967295 134512640 134672761 3221224544 3221223728 134615643 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 40305 38567 603 41 0 40264 0
vsize: 161220
[startup+490.027 s]
Raw data (loadavg): 0.99 0.98 0.99 2/54 10637
Raw data (stat): 10637 (minisat+) R 10636 5897 5896 0 -1 0 42364 0 0 0 48870 134 0 0 25 0 1 0 488399878 166154240 38854 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 40565 38854 603 41 0 40524 0
vsize: 162260
[startup+500.028 s]
Raw data (loadavg): 0.99 0.98 0.99 2/54 10637
Raw data (stat): 10637 (minisat+) R 10636 5897 5896 0 -1 0 42709 0 0 0 49869 135 0 0 25 0 1 0 488399878 167669760 39199 4294967295 134512640 134672761 3221224544 3221223728 134615676 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 40935 39199 603 41 0 40894 0
vsize: 163740
[startup+510.029 s]
Raw data (loadavg): 0.99 0.98 0.99 2/54 10637
Raw data (stat): 10637 (minisat+) R 10636 5897 5896 0 -1 0 43089 0 0 0 50868 136 0 0 25 0 1 0 488399878 169254912 39579 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 41322 39579 603 41 0 41281 0
vsize: 165288
[startup+520.029 s]
Raw data (loadavg): 0.99 0.98 0.99 2/54 10637
Raw data (stat): 10637 (minisat+) R 10636 5897 5896 0 -1 0 43454 0 0 0 51867 138 0 0 25 0 1 0 488399878 170717184 39944 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 41679 39944 603 41 0 41638 0
vsize: 166716
[startup+530.029 s]
Raw data (loadavg): 0.99 0.98 0.99 2/54 10637
Raw data (stat): 10637 (minisat+) R 10636 5897 5896 0 -1 0 43829 0 0 0 52866 139 0 0 25 0 1 0 488399878 172163072 40319 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 42032 40319 603 41 0 41991 0
vsize: 168128
[startup+540.03 s]
Raw data (loadavg): 0.99 0.98 0.99 2/54 10637
Raw data (stat): 10637 (minisat+) R 10636 5897 5896 0 -1 0 44124 0 0 0 53866 140 0 0 25 0 1 0 488399878 173342720 40614 4294967295 134512640 134672761 3221224544 3221223728 134615689 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 42320 40614 603 41 0 42279 0
vsize: 169280
[startup+550.031 s]
Raw data (loadavg): 0.99 0.98 0.99 2/54 10637
Raw data (stat): 10637 (minisat+) R 10636 5897 5896 0 -1 0 44447 0 0 0 54864 141 0 0 25 0 1 0 488399878 174653440 40937 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 42640 40937 603 41 0 42599 0
vsize: 170560
[startup+560.031 s]
Raw data (loadavg): 0.99 0.98 0.99 2/54 10637
Raw data (stat): 10637 (minisat+) R 10636 5897 5896 0 -1 0 44761 0 0 0 55863 143 0 0 25 0 1 0 488399878 176029696 41251 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 42976 41251 603 41 0 42935 0
vsize: 171904
[startup+570.032 s]
Raw data (loadavg): 0.99 0.98 0.99 2/54 10637
Raw data (stat): 10637 (minisat+) R 10636 5897 5896 0 -1 0 45034 0 0 0 56862 143 0 0 25 0 1 0 488399878 177233920 41524 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 43270 41524 603 41 0 43229 0
vsize: 173080
[startup+580.033 s]
Raw data (loadavg): 0.99 0.98 0.99 2/54 10637
Raw data (stat): 10637 (minisat+) R 10636 5897 5896 0 -1 0 45300 0 0 0 57861 144 0 0 25 0 1 0 488399878 178294784 41790 4294967295 134512640 134672761 3221224544 3221223728 134615741 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 43529 41790 603 41 0 43488 0
vsize: 174116
[startup+590.033 s]
Raw data (loadavg): 0.99 0.98 0.99 2/54 10637
Raw data (stat): 10637 (minisat+) R 10636 5897 5896 0 -1 0 45559 0 0 0 58861 145 0 0 25 0 1 0 488399878 179343360 42049 4294967295 134512640 134672761 3221224544 3221223728 134615833 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 43785 42049 603 41 0 43744 0
vsize: 175140
[startup+600.033 s]
Raw data (loadavg): 0.99 0.98 0.99 2/54 10637
Raw data (stat): 10637 (minisat+) R 10636 5897 5896 0 -1 0 45811 0 0 0 59860 146 0 0 25 0 1 0 488399878 180424704 42301 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 44049 42301 603 41 0 44008 0
vsize: 176196
[startup+610.035 s]
Raw data (loadavg): 0.99 0.98 0.99 2/54 10637
Raw data (stat): 10637 (minisat+) R 10636 5897 5896 0 -1 0 46072 0 0 0 60859 147 0 0 25 0 1 0 488399878 181477376 42562 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 44306 42562 603 41 0 44265 0
vsize: 177224
[startup+620.035 s]
Raw data (loadavg): 0.99 0.98 0.99 2/54 10637
Raw data (stat): 10637 (minisat+) R 10636 5897 5896 0 -1 0 46312 0 0 0 61858 148 0 0 25 0 1 0 488399878 182394880 42802 4294967295 134512640 134672761 3221224544 3221223728 134615676 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 44530 42802 603 41 0 44489 0
vsize: 178120
[startup+630.035 s]
Raw data (loadavg): 0.99 0.98 0.99 2/54 10637
Raw data (stat): 10637 (minisat+) R 10636 5897 5896 0 -1 0 46566 0 0 0 62857 149 0 0 25 0 1 0 488399878 183459840 43056 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 44790 43056 603 41 0 44749 0
vsize: 179160
[startup+640.037 s]
Raw data (loadavg): 0.99 0.98 0.99 2/54 10637
Raw data (stat): 10637 (minisat+) R 10636 5897 5896 0 -1 0 46835 0 0 0 63857 150 0 0 25 0 1 0 488399878 184512512 43325 4294967295 134512640 134672761 3221224544 3221223728 134615921 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 45047 43325 603 41 0 45006 0
vsize: 180188
[startup+650.037 s]
Raw data (loadavg): 0.99 0.98 0.99 2/54 10637
Raw data (stat): 10637 (minisat+) R 10636 5897 5896 0 -1 0 47105 0 0 0 64856 151 0 0 25 0 1 0 488399878 185696256 43595 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 45336 43595 603 41 0 45295 0
vsize: 181344
[startup+660.038 s]
Raw data (loadavg): 0.99 0.98 0.99 2/54 10637
Raw data (stat): 10637 (minisat+) R 10636 5897 5896 0 -1 0 47345 0 0 0 65855 152 0 0 25 0 1 0 488399878 186617856 43835 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 45561 43835 603 41 0 45520 0
vsize: 182244
[startup+670.039 s]
Raw data (loadavg): 0.99 0.98 0.99 2/54 10637
Raw data (stat): 10637 (minisat+) R 10636 5897 5896 0 -1 0 47613 0 0 0 66855 153 0 0 25 0 1 0 488399878 188723200 44103 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 46075 44103 603 41 0 46034 0
vsize: 184300
[startup+680.038 s]
Raw data (loadavg): 0.99 0.98 0.99 2/54 10637
Raw data (stat): 10637 (minisat+) R 10636 5897 5896 0 -1 0 47857 0 0 0 67854 154 0 0 25 0 1 0 488399878 189792256 44347 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 46336 44347 603 41 0 46295 0
vsize: 185344
[startup+690.038 s]
Raw data (loadavg): 0.99 0.98 0.99 2/54 10637
Raw data (stat): 10637 (minisat+) R 10636 5897 5896 0 -1 0 48096 0 0 0 68853 155 0 0 25 0 1 0 488399878 190713856 44586 4294967295 134512640 134672761 3221224544 3221223728 134615747 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 46561 44586 603 41 0 46520 0
vsize: 186244
[startup+700.04 s]
Raw data (loadavg): 0.99 0.98 0.99 2/54 10637
Raw data (stat): 10637 (minisat+) R 10636 5897 5896 0 -1 0 48349 0 0 0 69852 155 0 0 25 0 1 0 488399878 191762432 44839 4294967295 134512640 134672761 3221224544 3221223728 134615794 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 46817 44839 603 41 0 46776 0
vsize: 187268
[startup+710.04 s]
Raw data (loadavg): 0.99 0.98 0.99 2/54 10637
Raw data (stat): 10637 (minisat+) R 10636 5897 5896 0 -1 0 48604 0 0 0 70851 157 0 0 25 0 1 0 488399878 192741376 45094 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 47056 45094 603 41 0 47015 0
vsize: 188224
[startup+720.04 s]
Raw data (loadavg): 0.99 0.98 0.99 2/54 10637
Raw data (stat): 10637 (minisat+) R 10636 5897 5896 0 -1 0 48784 0 0 0 71850 158 0 0 25 0 1 0 488399878 193531904 45274 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 47249 45274 603 41 0 47208 0
vsize: 188996
[startup+730.04 s]
Raw data (loadavg): 0.99 0.98 0.99 2/54 10637
Raw data (stat): 10637 (minisat+) R 10636 5897 5896 0 -1 0 48980 0 0 0 72850 158 0 0 25 0 1 0 488399878 194441216 45470 4294967295 134512640 134672761 3221224544 3221223728 134615608 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 47471 45470 603 41 0 47430 0
vsize: 189884
[startup+740.04 s]
Raw data (loadavg): 0.99 0.98 0.99 2/54 10637
Raw data (stat): 10637 (minisat+) R 10636 5897 5896 0 -1 0 49159 0 0 0 73849 159 0 0 25 0 1 0 488399878 195125248 45649 4294967295 134512640 134672761 3221224544 3221223728 134615663 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 47638 45649 603 41 0 47597 0
vsize: 190552
[startup+750.04 s]
Raw data (loadavg): 0.99 0.98 0.99 2/54 10637
Raw data (stat): 10637 (minisat+) R 10636 5897 5896 0 -1 0 49319 0 0 0 74849 159 0 0 25 0 1 0 488399878 195784704 45809 4294967295 134512640 134672761 3221224544 3221223728 134615791 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 47799 45809 603 41 0 47758 0
vsize: 191196
[startup+760.042 s]
Raw data (loadavg): 0.99 0.98 0.99 2/54 10637
Raw data (stat): 10637 (minisat+) R 10636 5897 5896 0 -1 0 49500 0 0 0 75849 160 0 0 25 0 1 0 488399878 196571136 45990 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 47991 45990 603 41 0 47950 0
vsize: 191964
[startup+770.042 s]
Raw data (loadavg): 0.99 0.98 0.99 2/54 10637
Raw data (stat): 10637 (minisat+) R 10636 5897 5896 0 -1 0 49676 0 0 0 76848 161 0 0 25 0 1 0 488399878 197226496 46166 4294967295 134512640 134672761 3221224544 3221223728 134615627 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 48151 46166 603 41 0 48110 0
vsize: 192604
[startup+780.042 s]
Raw data (loadavg): 0.99 0.98 0.99 2/54 10637
Raw data (stat): 10637 (minisat+) R 10636 5897 5896 0 -1 0 49857 0 0 0 77847 162 0 0 25 0 1 0 488399878 198021120 46347 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 48345 46347 603 41 0 48304 0
vsize: 193380
[startup+790.043 s]
Raw data (loadavg): 0.99 0.98 0.99 2/54 10637
Raw data (stat): 10637 (minisat+) R 10636 5897 5896 0 -1 0 50070 0 0 0 78847 162 0 0 25 0 1 0 488399878 198823936 46560 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 48541 46560 603 41 0 48500 0
vsize: 194164
[startup+800.043 s]
Raw data (loadavg): 0.99 0.98 0.99 2/54 10637
Raw data (stat): 10637 (minisat+) R 10636 5897 5896 0 -1 0 50321 0 0 0 79846 163 0 0 25 0 1 0 488399878 199876608 46811 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 48798 46811 603 41 0 48757 0
vsize: 195192
[startup+810.043 s]
Raw data (loadavg): 0.99 0.98 0.99 2/54 10637
Raw data (stat): 10637 (minisat+) R 10636 5897 5896 0 -1 0 50551 0 0 0 80845 164 0 0 25 0 1 0 488399878 200794112 47041 4294967295 134512640 134672761 3221224544 3221223728 134615720 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 49022 47041 603 41 0 48981 0
vsize: 196088
[startup+820.045 s]
Raw data (loadavg): 0.99 0.98 0.99 2/54 10637
Raw data (stat): 10637 (minisat+) R 10636 5897 5896 0 -1 0 50767 0 0 0 81845 165 0 0 25 0 1 0 488399878 201715712 47257 4294967295 134512640 134672761 3221224544 3221223728 134615804 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 49247 47257 603 41 0 49206 0
vsize: 196988
[startup+830.044 s]
Raw data (loadavg): 0.99 0.98 0.99 2/54 10637
Raw data (stat): 10637 (minisat+) R 10636 5897 5896 0 -1 0 50953 0 0 0 82845 165 0 0 25 0 1 0 488399878 202506240 47443 4294967295 134512640 134672761 3221224544 3221223728 134615919 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 49440 47443 603 41 0 49399 0
vsize: 197760
[startup+840.044 s]
Raw data (loadavg): 0.99 0.98 0.99 2/54 10637
Raw data (stat): 10637 (minisat+) R 10636 5897 5896 0 -1 0 51123 0 0 0 83844 166 0 0 25 0 1 0 488399878 203177984 47613 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 49604 47613 603 41 0 49563 0
vsize: 198416
[startup+850.044 s]
Raw data (loadavg): 0.99 0.98 0.99 2/54 10637
Raw data (stat): 10637 (minisat+) R 10636 5897 5896 0 -1 0 51302 0 0 0 84844 167 0 0 25 0 1 0 488399878 203853824 47792 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 49769 47792 603 41 0 49728 0
vsize: 199076
[startup+860.045 s]
Raw data (loadavg): 1.07 1.00 0.99 2/54 10690
Raw data (stat): 10637 (minisat+) R 10636 5897 5896 0 -1 0 51508 0 0 0 85842 168 0 0 25 0 1 0 488399878 204877824 47998 4294967295 134512640 134672761 3221224544 3221223728 134615627 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 50019 47998 603 41 0 49978 0
vsize: 200076
[startup+870.045 s]
Raw data (loadavg): 1.06 1.00 0.99 2/54 10690
Raw data (stat): 10637 (minisat+) R 10636 5897 5896 0 -1 0 51703 0 0 0 86842 168 0 0 25 0 1 0 488399878 205602816 48193 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 50196 48193 603 41 0 50155 0
vsize: 200784
[startup+880.046 s]
Raw data (loadavg): 1.05 1.00 0.99 2/54 10690
Raw data (stat): 10637 (minisat+) R 10636 5897 5896 0 -1 0 51897 0 0 0 87841 169 0 0 25 0 1 0 488399878 206516224 48387 4294967295 134512640 134672761 3221224544 3221223728 134615591 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 50419 48387 603 41 0 50378 0
vsize: 201676
[startup+890.046 s]
Raw data (loadavg): 1.04 1.00 0.99 2/54 10690
Raw data (stat): 10637 (minisat+) R 10636 5897 5896 0 -1 0 52090 0 0 0 88841 169 0 0 25 0 1 0 488399878 207204352 48580 4294967295 134512640 134672761 3221224544 3221223728 134615732 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 50587 48580 603 41 0 50546 0
vsize: 202348
[startup+900.046 s]
Raw data (loadavg): 1.03 1.00 0.99 2/54 10690
Raw data (stat): 10637 (minisat+) R 10636 5897 5896 0 -1 0 52309 0 0 0 89841 170 0 0 25 0 1 0 488399878 208162816 48799 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 50821 48799 603 41 0 50780 0
vsize: 203284
[startup+910.047 s]
Raw data (loadavg): 1.03 1.00 0.99 2/54 10690
Raw data (stat): 10637 (minisat+) R 10636 5897 5896 0 -1 0 52512 0 0 0 90841 170 0 0 25 0 1 0 488399878 208957440 49002 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 51015 49002 603 41 0 50974 0
vsize: 204060
[startup+920.048 s]
Raw data (loadavg): 1.02 1.00 0.99 2/54 10690
Raw data (stat): 10637 (minisat+) R 10636 5897 5896 0 -1 0 52750 0 0 0 91841 171 0 0 25 0 1 0 488399878 210022400 49240 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 51275 49240 603 41 0 51234 0
vsize: 205100
[startup+930.048 s]
Raw data (loadavg): 1.02 1.00 0.99 2/54 10692
Raw data (stat): 10637 (minisat+) R 10636 5897 5896 0 -1 0 52885 0 0 0 92841 171 0 0 25 0 1 0 488399878 210952192 49375 4294967295 134512640 134672761 3221224544 3221223728 134615594 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 51502 49375 603 41 0 51461 0
vsize: 206008
[startup+940.049 s]
Raw data (loadavg): 1.02 1.00 0.99 2/54 10692
Raw data (stat): 10637 (minisat+) R 10636 5897 5896 0 -1 0 53082 0 0 0 93840 172 0 0 25 0 1 0 488399878 211742720 49572 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 51695 49572 603 41 0 51654 0
vsize: 206780
[startup+950.049 s]
Raw data (loadavg): 1.01 1.00 0.99 2/54 10692
Raw data (stat): 10637 (minisat+) R 10636 5897 5896 0 -1 0 53190 0 0 0 94840 172 0 0 25 0 1 0 488399878 212144128 49680 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 51793 49680 603 41 0 51752 0
vsize: 207172
[startup+960.051 s]
Raw data (loadavg): 1.01 1.00 0.99 2/54 10692
Raw data (stat): 10637 (minisat+) R 10636 5897 5896 0 -1 0 53362 0 0 0 95840 172 0 0 25 0 1 0 488399878 212934656 49852 4294967295 134512640 134672761 3221224544 3221223728 134615703 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 51986 49852 603 41 0 51945 0
vsize: 207944
[startup+970.051 s]
Raw data (loadavg): 1.01 1.00 0.99 2/54 10692
Raw data (stat): 10637 (minisat+) R 10636 5897 5896 0 -1 0 53512 0 0 0 96840 172 0 0 25 0 1 0 488399878 213463040 50002 4294967295 134512640 134672761 3221224544 3221223728 134615948 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 52115 50002 603 41 0 52074 0
vsize: 208460
[startup+980.051 s]
Raw data (loadavg): 1.01 1.00 0.99 2/54 10692
Raw data (stat): 10637 (minisat+) R 10636 5897 5896 0 -1 0 53645 0 0 0 97840 173 0 0 25 0 1 0 488399878 214118400 50135 4294967295 134512640 134672761 3221224544 3221223728 134615676 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 52275 50135 603 41 0 52234 0
vsize: 209100
[startup+990.052 s]
Raw data (loadavg): 1.00 1.00 0.99 2/54 10692
Raw data (stat): 10637 (minisat+) R 10636 5897 5896 0 -1 0 53789 0 0 0 98840 173 0 0 25 0 1 0 488399878 214650880 50279 4294967295 134512640 134672761 3221224544 3221223744 134610707 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 52405 50279 603 41 0 52364 0
vsize: 209620
[startup+1000.05 s]
Raw data (loadavg): 1.00 1.00 0.99 2/54 10692
Raw data (stat): 10637 (minisat+) R 10636 5897 5896 0 -1 0 53919 0 0 0 99840 173 0 0 25 0 1 0 488399878 215179264 50409 4294967295 134512640 134672761 3221224544 3221223584 134612987 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 52534 50409 603 41 0 52493 0
vsize: 210136
[startup+1010.05 s]
Raw data (loadavg): 1.00 1.00 0.99 2/54 10692
Raw data (stat): 10637 (minisat+) R 10636 5897 5896 0 -1 0 54066 0 0 0 100840 174 0 0 25 0 1 0 488399878 215711744 50556 4294967295 134512640 134672761 3221224544 3221223728 134615791 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 52664 50556 603 41 0 52623 0
vsize: 210656
[startup+1020.05 s]
Raw data (loadavg): 1.00 1.00 0.99 2/54 10692
Raw data (stat): 10637 (minisat+) R 10636 5897 5896 0 -1 0 54207 0 0 0 101840 174 0 0 25 0 1 0 488399878 216375296 50697 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 52826 50697 603 41 0 52785 0
vsize: 211304
[startup+1030.05 s]
Raw data (loadavg): 1.00 1.00 0.99 2/54 10692
Raw data (stat): 10637 (minisat+) R 10636 5897 5896 0 -1 0 54349 0 0 0 102839 174 0 0 25 0 1 0 488399878 216899584 50839 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 52954 50839 603 41 0 52913 0
vsize: 211816
[startup+1040.05 s]
Raw data (loadavg): 1.00 1.00 0.99 2/54 10692
Raw data (stat): 10637 (minisat+) R 10636 5897 5896 0 -1 0 54507 0 0 0 103839 174 0 0 25 0 1 0 488399878 217563136 50997 4294967295 134512640 134672761 3221224544 3221223728 134615681 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 53116 50997 603 41 0 53075 0
vsize: 212464
[startup+1050.05 s]
Raw data (loadavg): 1.00 1.00 0.99 2/54 10692
Raw data (stat): 10637 (minisat+) R 10636 5897 5896 0 -1 0 54679 0 0 0 104839 175 0 0 25 0 1 0 488399878 218218496 51169 4294967295 134512640 134672761 3221224544 3221223728 134615663 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 53276 51169 603 41 0 53235 0
vsize: 213104
[startup+1060.06 s]
Raw data (loadavg): 1.00 1.00 0.99 2/54 10692
Raw data (stat): 10637 (minisat+) R 10636 5897 5896 0 -1 0 54815 0 0 0 105839 176 0 0 25 0 1 0 488399878 218873856 51305 4294967295 134512640 134672761 3221224544 3221223744 134610707 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 53436 51305 603 41 0 53395 0
vsize: 213744
[startup+1070.06 s]
Raw data (loadavg): 1.00 1.00 0.99 2/54 10692
Raw data (stat): 10637 (minisat+) R 10636 5897 5896 0 -1 0 54996 0 0 0 106839 176 0 0 25 0 1 0 488399878 219537408 51486 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 53598 51486 603 41 0 53557 0
vsize: 214392
[startup+1080.07 s]
Raw data (loadavg): 1.00 1.00 0.99 2/54 10692
Raw data (stat): 10637 (minisat+) R 10636 5897 5896 0 -1 0 55143 0 0 0 107839 177 0 0 25 0 1 0 488399878 220192768 51633 4294967295 134512640 134672761 3221224544 3221223728 134615929 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 53758 51633 603 41 0 53717 0
vsize: 215032
[startup+1090.07 s]
Raw data (loadavg): 1.00 1.00 0.99 2/54 10692
Raw data (stat): 10637 (minisat+) R 10636 5897 5896 0 -1 0 55276 0 0 0 108838 177 0 0 25 0 1 0 488399878 220725248 51766 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 53888 51766 603 41 0 53847 0
vsize: 215552
[startup+1100.07 s]
Raw data (loadavg): 1.00 1.00 0.99 2/54 10692
Raw data (stat): 10637 (minisat+) R 10636 5897 5896 0 -1 0 55402 0 0 0 109838 178 0 0 25 0 1 0 488399878 221253632 51892 4294967295 134512640 134672761 3221224544 3221223744 134610707 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 54017 51892 603 41 0 53976 0
vsize: 216068
[startup+1110.07 s]
Raw data (loadavg): 1.00 1.00 0.99 2/54 10692
Raw data (stat): 10637 (minisat+) R 10636 5897 5896 0 -1 0 55527 0 0 0 110838 179 0 0 25 0 1 0 488399878 221646848 52017 4294967295 134512640 134672761 3221224544 3221223728 134615535 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 54113 52017 603 41 0 54072 0
vsize: 216452
[startup+1120.07 s]
Raw data (loadavg): 1.00 1.00 0.99 2/54 10692
Raw data (stat): 10637 (minisat+) R 10636 5897 5896 0 -1 0 55647 0 0 0 111837 179 0 0 25 0 1 0 488399878 222175232 52137 4294967295 134512640 134672761 3221224544 3221223680 134614690 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 54242 52137 603 41 0 54201 0
vsize: 216968
[startup+1130.07 s]
Raw data (loadavg): 1.00 1.00 0.99 2/54 10692
Raw data (stat): 10637 (minisat+) R 10636 5897 5896 0 -1 0 55769 0 0 0 112837 180 0 0 25 0 1 0 488399878 222711808 52259 4294967295 134512640 134672761 3221224544 3221223584 134612987 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 54373 52259 603 41 0 54332 0
vsize: 217492
[startup+1140.07 s]
Raw data (loadavg): 1.00 1.00 0.99 2/54 10692
Raw data (stat): 10637 (minisat+) R 10636 5897 5896 0 -1 0 55879 0 0 0 113836 181 0 0 25 0 1 0 488399878 223109120 52369 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 54470 52369 603 41 0 54429 0
vsize: 217880
[startup+1150.07 s]
Raw data (loadavg): 1.00 1.00 0.99 2/54 10692
Raw data (stat): 10637 (minisat+) R 10636 5897 5896 0 -1 0 55986 0 0 0 114836 181 0 0 25 0 1 0 488399878 223510528 52476 4294967295 134512640 134672761 3221224544 3221223728 134615747 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 54568 52476 603 41 0 54527 0
vsize: 218272
[startup+1160.07 s]
Raw data (loadavg): 1.00 1.00 0.99 2/54 10692
Raw data (stat): 10637 (minisat+) R 10636 5897 5896 0 -1 0 56101 0 0 0 115836 181 0 0 25 0 1 0 488399878 224047104 52591 4294967295 134512640 134672761 3221224544 3221223680 134614727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 54699 52591 603 41 0 54658 0
vsize: 218796
[startup+1170.07 s]
Raw data (loadavg): 1.00 1.00 0.99 2/54 10692
Raw data (stat): 10637 (minisat+) R 10636 5897 5896 0 -1 0 56205 0 0 0 116836 182 0 0 25 0 1 0 488399878 224444416 52695 4294967295 134512640 134672761 3221224544 3221223680 134614814 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 54796 52695 603 41 0 54755 0
vsize: 219184
[startup+1180.07 s]
Raw data (loadavg): 1.00 1.00 0.99 2/54 10692
Raw data (stat): 10637 (minisat+) R 10636 5897 5896 0 -1 0 56359 0 0 0 117836 182 0 0 25 0 1 0 488399878 225112064 52849 4294967295 134512640 134672761 3221224544 3221223744 134610707 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 54959 52849 603 41 0 54918 0
vsize: 219836
[startup+1190.07 s]
Raw data (loadavg): 1.00 1.00 0.99 2/54 10692
Raw data (stat): 10637 (minisat+) R 10636 5897 5896 0 -1 0 56494 0 0 0 118836 182 0 0 25 0 1 0 488399878 225648640 52984 4294967295 134512640 134672761 3221224544 3221223680 134614551 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 55090 52984 603 41 0 55049 0
vsize: 220360
[startup+1200.07 s]
Raw data (loadavg): 1.00 1.00 0.99 2/54 10692
Raw data (stat): 10637 (minisat+) R 10636 5897 5896 0 -1 0 56639 0 0 0 119835 183 0 0 25 0 1 0 488399878 226304000 53129 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 55250 53129 603 41 0 55209 0
vsize: 221000
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.17 s]
Raw data (loadavg): 1.00 1.00 0.99 1/54 10692
Raw data (stat): 10637 (minisat+) Z 10636 5897 5896 0 -1 12 56639 0 0 0 119835 193 0 0 25 0 1 0 488399878 0 0 4294967295 0 0 0 0 0 0 16384 5 16386 3222412051 0 0 17 0 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.17
CPU time (s): 1200.29
CPU user time (s): 1198.36
CPU system time (s): 1.93271
CPU usage (%): 100.01
Max. virtual memory (Kb): 221000
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####