PB'05 competition: run trace

Some explanations

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

Name	normalized-opb/mps-v2-20-10/MIPLIB/miplib2003/normalized-mps-v2-20-10-aflow40b.opb
MD5SUM	64cd8dd71c00255f05a721f3d3f16ae5
Bench Category	optimization, medium integers (OPTMEDINT)
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	102400
Number of bits of the biggest number in a constraint	17
Biggest sum of numbers in a constraint	7037881
Number of bits of the biggest sum of numbers	23
Best result obtained on this benchmark
Best CPU time to get the best result obtained on this benchmark
Number of variables	23384
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	1202
Trace number 21901

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc13 THE 2005-04-22 01:22:48 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=12420 boxname=wulflinc13 idbench=956 idsolver=5 numberseed=0
MD5SUM SOLVER: 1d62365061f6d70b1a242542b016b2e4  /oldhome/oroussel/solvers/minisat+
MD5SUM BENCH:  64cd8dd71c00255f05a721f3d3f16ae5  /oldhome/oroussel/tmp/wulflinc13/normalized-mps-v2-20-10-aflow40b.opb
REAL COMMAND:  minisat+ /oldhome/oroussel/tmp/wulflinc13/normalized-mps-v2-20-10-aflow40b.opb
IDLAUNCH: 12420
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.242
cache size	: 512 KB
fdiv_bug	: no
hlt_bug		: no
f00f_bug	: no
coma_bug	: no
fpu		: yes
fpu_exception	: yes
cpuid level	: 2
wp		: yes
flags		: fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse
bogomips	: 888.83

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.242
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	: 901.12

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        361272 kB
Buffers:         20156 kB
Cached:         631708 kB
SwapCached:        392 kB
Active:          95796 kB
Inactive:       558200 kB
HighTotal:      131008 kB
HighFree:          252 kB
LowTotal:       903652 kB
LowFree:        361020 kB
SwapTotal:     2097136 kB
SwapFree:      2095968 kB
Dirty:              16 kB
Writeback:           0 kB
Mapped:           5748 kB
Slab:            13696 kB
Committed_AS:    63596 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-22 01:42:51 (client local time) WITH STATUS 0 IN 1200.26 SECONDS
stats: 12420 7 1200.26 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:   16
c ---[3066]---> BDD-cost:   16
c ---[3064]---> BDD-cost:   15
c ---[3063]---> BDD-cost:   16
c ---[3062]---> BDD-cost:   15
c ---[3061]---> BDD-cost:   14
c ---[3060]---> BDD-cost:   16
c ---[3059]---> BDD-cost:   16
c ---[3058]---> BDD-cost:   14
c ---[3056]---> BDD-cost:   14
c ---[3055]---> BDD-cost:   15
c ---[3053]---> BDD-cost:   16
c ---[3052]---> BDD-cost:   16
c ---[3051]---> BDD-cost:   13
c ---[3049]---> BDD-cost:   15
c ---[3048]---> BDD-cost:   16
c ---[3047]---> BDD-cost:   15
c ---[3046]---> BDD-cost:   16
c ---[3045]---> BDD-cost:   16
c ---[3044]---> BDD-cost:   16
c ---[3042]---> BDD-cost:   15
c ---[3040]---> BDD-cost:   14
c ---[3039]---> BDD-cost:   15
c ---[3038]---> BDD-cost:   15
c ---[3037]---> BDD-cost:   15
c ---[3036]---> BDD-cost:   15
c ---[3035]---> BDD-cost:   14
c ---[3034]---> BDD-cost:   14
c ---[3033]---> BDD-cost:   14
c ---[3032]---> BDD-cost:   16
c ---[3030]---> BDD-cost:   13
c ---[3028]---> BDD-cost:   14
c ---[3026]---> BDD-cost:   16
c ---[3025]---> BDD-cost:   16
c ---[3024]---> BDD-cost:   15
c ---[3023]---> BDD-cost:   16
c ---[3022]---> BDD-cost:   16
c ---[3021]---> BDD-cost:   16
c ---[3020]---> BDD-cost:   16
c ---[3019]---> BDD-cost:   15
c ---[3018]---> BDD-cost:   15
c ---[3017]---> BDD-cost:   14
c ---[3016]---> BDD-cost:   16
c ---[3015]---> BDD-cost:   16
c ---[3014]---> BDD-cost:   14
c ---[3013]---> BDD-cost:   16
c ---[3012]---> BDD-cost:   14
c ---[3011]---> BDD-cost:   14
c ---[3010]---> BDD-cost:   14
c ---[3009]---> BDD-cost:   16
c ---[3008]---> BDD-cost:   14
c ---[3007]---> BDD-cost:   16
c ---[3005]---> BDD-cost:   16
c ---[3004]---> BDD-cost:   16
c ---[3003]---> BDD-cost:   16
c ---[3002]---> BDD-cost:   15
c ---[3001]---> BDD-cost:   16
c ---[3000]---> BDD-cost:   15
c ---[2999]---> BDD-cost:   15
c ---[2998]---> BDD-cost:   15
c ---[2997]---> BDD-cost:   16
c ---[2996]---> BDD-cost:   15
c ---[2995]---> BDD-cost:   15
c ---[2994]---> BDD-cost:   16
c ---[2993]---> BDD-cost:   16
c ---[2992]---> BDD-cost:   16
c ---[2991]---> BDD-cost:   15
c ---[2990]---> BDD-cost:   16
c ---[2989]---> BDD-cost:   14
c ---[2988]---> BDD-cost:   13
c ---[2987]---> BDD-cost:   15
c ---[2986]---> BDD-cost:   15
c ---[2985]---> BDD-cost:   16
c ---[2984]---> BDD-cost:   14
c ---[2983]---> BDD-cost:   14
c ---[2982]---> BDD-cost:   16
c ---[2981]---> BDD-cost:   16
c ---[2980]---> BDD-cost:   16
c ---[2979]---> BDD-cost:   15
c ---[2978]---> BDD-cost:   15
c ---[2977]---> BDD-cost:   16
c ---[2976]---> BDD-cost:   15
c ---[2975]---> BDD-cost:   15
c ---[2974]---> BDD-cost:   16
c ---[2973]---> BDD-cost:   15
c ---[2972]---> BDD-cost:   15
c ---[2971]---> BDD-cost:   15
c ---[2969]---> BDD-cost:   16
c ---[2968]---> BDD-cost:   16
c ---[2967]---> BDD-cost:   15
c ---[2966]---> BDD-cost:   15
c ---[2965]---> BDD-cost:   15
c ---[2964]---> BDD-cost:   16
c ---[2963]---> BDD-cost:   16
c ---[2962]---> BDD-cost:   14
c ---[2961]---> BDD-cost:   16
c ---[2960]---> BDD-cost:   16
c ---[2959]---> BDD-cost:   14
c ---[2958]---> BDD-cost:   14
c ---[2955]---> BDD-cost:   16
c ---[2954]---> BDD-cost:   14
c ---[2953]---> BDD-cost:   16
c ---[2952]---> BDD-cost:   16
c ---[2951]---> BDD-cost:   15
c ---[2950]---> BDD-cost:   15
c ---[2949]---> BDD-cost:   15
c ---[2948]---> BDD-cost:   16
c ---[2947]---> BDD-cost:   15
c ---[2946]---> BDD-cost:   16
c ---[2945]---> BDD-cost:   15
c ---[2943]---> BDD-cost:   15
c ---[2942]---> BDD-cost:   16
c ---[2941]---> BDD-cost:   13
c ---[2940]---> BDD-cost:   16
c ---[2939]---> BDD-cost:   16
c ---[2938]---> BDD-cost:   16
c ---[2937]---> BDD-cost:   15
c ---[2935]---> BDD-cost:   15
c ---[2934]---> BDD-cost:   14
c ---[2933]---> BDD-cost:   16
c ---[2932]---> BDD-cost:   13
c ---[2930]---> BDD-cost:   15
c ---[2929]---> BDD-cost:   16
c ---[2928]---> BDD-cost:   16
c ---[2927]---> BDD-cost:   16
c ---[2926]---> BDD-cost:   16
c ---[2925]---> BDD-cost:   14
c ---[2924]---> BDD-cost:   16
c ---[2923]---> BDD-cost:   15
c ---[2922]---> BDD-cost:   16
c ---[2921]---> BDD-cost:   16
c ---[2919]---> BDD-cost:   15
c ---[2918]---> BDD-cost:   16
c ---[2917]---> BDD-cost:   15
c ---[2916]---> BDD-cost:   16
c ---[2915]---> BDD-cost:   13
c ---[2914]---> BDD-cost:   16
c ---[2913]---> BDD-cost:   15
c ---[2912]---> BDD-cost:   16
c ---[2911]---> BDD-cost:   14
c ---[2909]---> BDD-cost:   16
c ---[2907]---> BDD-cost:   16
c ---[2906]---> BDD-cost:   16
c ---[2905]---> BDD-cost:   14
c ---[2904]---> BDD-cost:   14
c ---[2902]---> BDD-cost:   16
c ---[2901]---> BDD-cost:   16
c ---[2900]---> BDD-cost:   16
c ---[2899]---> BDD-cost:   15
c ---[2898]---> BDD-cost:   16
c ---[2897]---> BDD-cost:   16
c ---[2896]---> BDD-cost:   15
c ---[2895]---> BDD-cost:   16
c ---[2894]---> BDD-cost:   14
c ---[2893]---> BDD-cost:   16
c ---[2892]---> BDD-cost:   16
c ---[2890]---> BDD-cost:   16
c ---[2889]---> BDD-cost:   15
c ---[2888]---> BDD-cost:   16
c ---[2887]---> BDD-cost:   13
c ---[2886]---> BDD-cost:   16
c ---[2884]---> BDD-cost:   16
c ---[2882]---> BDD-cost:   15
c ---[2881]---> BDD-cost:   16
c ---[2879]---> BDD-cost:   14
c ---[2877]---> BDD-cost:   15
c ---[2876]---> BDD-cost:   16
c ---[2875]---> BDD-cost:   16
c ---[2874]---> BDD-cost:   16
c ---[2873]---> BDD-cost:   16
c ---[2872]---> BDD-cost:   16
c ---[2871]---> BDD-cost:   16
c ---[2870]---> BDD-cost:   15
c ---[2869]---> BDD-cost:   16
c ---[2868]---> BDD-cost:   15
c ---[2866]---> BDD-cost:   16
c ---[2865]---> BDD-cost:   16
c ---[2864]---> BDD-cost:   14
c ---[2863]---> BDD-cost:   14
c ---[2862]---> BDD-cost:   14
c ---[2861]---> BDD-cost:   15
c ---[2860]---> BDD-cost:   15
c ---[2859]---> BDD-cost:   16
c ---[2858]---> BDD-cost:   16
c ---[2856]---> BDD-cost:   16
c ---[2855]---> BDD-cost:   15
c ---[2854]---> BDD-cost:   15
c ---[2853]---> BDD-cost:   15
c ---[2852]---> BDD-cost:   13
c ---[2851]---> BDD-cost:   14
c ---[2850]---> BDD-cost:   13
c ---[2849]---> BDD-cost:   15
c ---[2847]---> BDD-cost:   15
c ---[2846]---> BDD-cost:   13
c ---[2845]---> BDD-cost:   16
c ---[2844]---> BDD-cost:   16
c ---[2843]---> BDD-cost:   14
c ---[2842]---> BDD-cost:   16
c ---[2841]---> BDD-cost:   16
c ---[2840]---> BDD-cost:   16
c ---[2839]---> BDD-cost:   16
c ---[2838]---> BDD-cost:   15
c ---[2837]---> BDD-cost:   14
c ---[2836]---> BDD-cost:   14
c ---[2835]---> BDD-cost:   15
c ---[2834]---> BDD-cost:   16
c ---[2833]---> BDD-cost:   15
c ---[2832]---> BDD-cost:   14
c ---[2831]---> BDD-cost:   14
c ---[2830]---> BDD-cost:   15
c ---[2829]---> BDD-cost:   16
c ---[2828]---> BDD-cost:   14
c ---[2827]---> BDD-cost:   14
c ---[2826]---> BDD-cost:   16
c ---[2825]---> BDD-cost:   16
c ---[2824]---> BDD-cost:   14
c ---[2823]---> BDD-cost:   15
c ---[2822]---> BDD-cost:   16
c ---[2821]---> BDD-cost:   13
c ---[2820]---> BDD-cost:   16
c ---[2819]---> BDD-cost:   16
c ---[2817]---> BDD-cost:   16
c ---[2816]---> BDD-cost:   15
c ---[2815]---> BDD-cost:   13
c ---[2814]---> BDD-cost:   15
c ---[2813]---> BDD-cost:   15
c ---[2812]---> BDD-cost:   16
c ---[2811]---> BDD-cost:   14
c ---[2810]---> BDD-cost:   16
c ---[2808]---> BDD-cost:   16
c ---[2806]---> BDD-cost:   15
c ---[2805]---> BDD-cost:   14
c ---[2803]---> BDD-cost:   14
c ---[2802]---> BDD-cost:   16
c ---[2801]---> BDD-cost:   15
c ---[2800]---> BDD-cost:   16
c ---[2797]---> BDD-cost:   16
c ---[2796]---> BDD-cost:   15
c ---[2795]---> BDD-cost:   13
c ---[2794]---> BDD-cost:   16
c ---[2793]---> BDD-cost:   16
c ---[2792]---> BDD-cost:   16
c ---[2791]---> BDD-cost:   14
c ---[2790]---> BDD-cost:   16
c ---[2789]---> BDD-cost:   16
c ---[2788]---> BDD-cost:   16
c ---[2787]---> BDD-cost:   14
c ---[2786]---> BDD-cost:   16
c ---[2785]---> BDD-cost:   14
c ---[2784]---> BDD-cost:   15
c ---[2783]---> BDD-cost:   13
c ---[2781]---> BDD-cost:   16
c ---[2780]---> BDD-cost:   16
c ---[2779]---> BDD-cost:   15
c ---[2778]---> BDD-cost:   15
c ---[2777]---> BDD-cost:   16
c ---[2776]---> BDD-cost:   16
c ---[2775]---> BDD-cost:   16
c ---[2774]---> BDD-cost:   16
c ---[2773]---> BDD-cost:   16
c ---[2772]---> BDD-cost:   16
c ---[2771]---> BDD-cost:   16
c ---[2769]---> BDD-cost:   16
c ---[2768]---> BDD-cost:   16
c ---[2767]---> BDD-cost:   14
c ---[2766]---> BDD-cost:   15
c ---[2765]---> BDD-cost:   15
c ---[2764]---> BDD-cost:   16
c ---[2763]---> BDD-cost:   16
c ---[2762]---> BDD-cost:   16
c ---[2761]---> BDD-cost:   15
c ---[2760]---> BDD-cost:   15
c ---[2759]---> BDD-cost:   15
c ---[2758]---> BDD-cost:   16
c ---[2757]---> BDD-cost:   15
c ---[2756]---> BDD-cost:   16
c ---[2755]---> BDD-cost:   15
c ---[2754]---> BDD-cost:   16
c ---[2753]---> BDD-cost:   16
c ---[2752]---> BDD-cost:   13
c ---[2751]---> BDD-cost:   16
c ---[2750]---> BDD-cost:   14
c ---[2748]---> BDD-cost:   13
c ---[2747]---> BDD-cost:   16
c ---[2746]---> BDD-cost:   16
c ---[2744]---> BDD-cost:   13
c ---[2743]---> BDD-cost:   15
c ---[2742]---> BDD-cost:   16
c ---[2741]---> BDD-cost:   16
c ---[2740]---> BDD-cost:   16
c ---[2739]---> BDD-cost:   15
c ---[2737]---> BDD-cost:   16
c ---[2736]---> BDD-cost:   16
c ---[2735]---> BDD-cost:   15
c ---[2734]---> BDD-cost:   14
c ---[2733]---> BDD-cost:   16
c ---[2732]---> BDD-cost:   16
c ---[2731]---> BDD-cost:   16
c ---[2730]---> BDD-cost:   16
c ---[2728]---> BDD-cost:   16
c ---[2727]---> BDD-cost:   16
c ---[2726]---> BDD-cost:   16
c ---[2724]---> BDD-cost:   16
c ---[2723]---> BDD-cost:   15
c ---[2722]---> BDD-cost:   16
c ---[2721]---> BDD-cost:   16
c ---[2720]---> BDD-cost:   16
c ---[2719]---> BDD-cost:   15
c ---[2718]---> BDD-cost:   16
c ---[2717]---> BDD-cost:   14
c ---[2716]---> BDD-cost:   16
c ---[2715]---> BDD-cost:   15
c ---[2714]---> BDD-cost:   16
c ---[2712]---> BDD-cost:   16
c ---[2710]---> BDD-cost:   16
c ---[2709]---> BDD-cost:   16
c ---[2708]---> BDD-cost:   13
c ---[2706]---> BDD-cost:   16
c ---[2705]---> BDD-cost:   16
c ---[2704]---> BDD-cost:   15
c ---[2703]---> BDD-cost:   16
c ---[2701]---> BDD-cost:   16
c ---[2700]---> BDD-cost:   15
c ---[2699]---> BDD-cost:   15
c ---[2698]---> BDD-cost:   16
c ---[2697]---> BDD-cost:   16
c ---[2696]---> BDD-cost:   16
c ---[2695]---> BDD-cost:   16
c ---[2694]---> BDD-cost:   16
c ---[2693]---> BDD-cost:   16
c ---[2692]---> BDD-cost:   16
c ---[2691]---> BDD-cost:   14
c ---[2690]---> BDD-cost:   16
c ---[2689]---> BDD-cost:   15
c ---[2688]---> BDD-cost:   16
c ---[2687]---> BDD-cost:   16
c ---[2686]---> BDD-cost:   15
c ---[2685]---> BDD-cost:   15
c ---[2684]---> BDD-cost:   16
c ---[2683]---> BDD-cost:   16
c ---[2682]---> BDD-cost:   16
c ---[2681]---> BDD-cost:   14
c ---[2680]---> BDD-cost:   14
c ---[2679]---> BDD-cost:   16
c ---[2678]---> BDD-cost:   15
c ---[2677]---> BDD-cost:   15
c ---[2675]---> BDD-cost:   16
c ---[2674]---> BDD-cost:   16
c ---[2673]---> BDD-cost:   16
c ---[2672]---> BDD-cost:   15
c ---[2671]---> BDD-cost:   14
c ---[2670]---> BDD-cost:   15
c ---[2669]---> BDD-cost:   16
c ---[2668]---> BDD-cost:   13
c ---[2667]---> BDD-cost:   16
c ---[2665]---> BDD-cost:   15
c ---[2664]---> BDD-cost:   14
c ---[2662]---> BDD-cost:   16
c ---[2661]---> BDD-cost:   14
c ---[2660]---> BDD-cost:   14
c ---[2659]---> BDD-cost:   16
c ---[2658]---> BDD-cost:   15
c ---[2656]---> BDD-cost:   16
c ---[2654]---> BDD-cost:   16
c ---[2653]---> BDD-cost:   14
c ---[2652]---> BDD-cost:   15
c ---[2651]---> BDD-cost:   16
c ---[2650]---> BDD-cost:   15
c ---[2648]---> BDD-cost:   15
c ---[2647]---> BDD-cost:   14
c ---[2646]---> BDD-cost:   13
c ---[2645]---> BDD-cost:   15
c ---[2644]---> BDD-cost:   15
c ---[2643]---> BDD-cost:   15
c ---[2642]---> BDD-cost:   15
c ---[2641]---> BDD-cost:   16
c ---[2638]---> BDD-cost:   16
c ---[2637]---> BDD-cost:   15
c ---[2636]---> BDD-cost:   14
c ---[2635]---> BDD-cost:   14
c ---[2634]---> BDD-cost:   13
c ---[2633]---> BDD-cost:   16
c ---[2632]---> BDD-cost:   14
c ---[2631]---> BDD-cost:   15
c ---[2630]---> BDD-cost:   16
c ---[2629]---> BDD-cost:   14
c ---[2628]---> BDD-cost:   15
c ---[2627]---> BDD-cost:   16
c ---[2626]---> BDD-cost:   16
c ---[2625]---> BDD-cost:   15
c ---[2624]---> BDD-cost:   15
c ---[2623]---> BDD-cost:   16
c ---[2622]---> BDD-cost:   16
c ---[2621]---> BDD-cost:   16
c ---[2620]---> BDD-cost:   16
c ---[2619]---> BDD-cost:   14
c ---[2618]---> BDD-cost:   16
c ---[2617]---> BDD-cost:   15
c ---[2616]---> BDD-cost:   16
c ---[2615]---> BDD-cost:   16
c ---[2614]---> BDD-cost:   16
c ---[2613]---> BDD-cost:   15
c ---[2612]---> BDD-cost:   16
c ---[2611]---> BDD-cost:   16
c ---[2610]---> BDD-cost:   15
c ---[2609]---> BDD-cost:   15
c ---[2608]---> BDD-cost:   15
c ---[2606]---> BDD-cost:   15
c ---[2604]---> BDD-cost:   14
c ---[2603]---> BDD-cost:   15
c ---[2602]---> BDD-cost:   16
c ---[2601]---> BDD-cost:   16
c ---[2600]---> BDD-cost:   14
c ---[2599]---> BDD-cost:   16
c ---[2598]---> BDD-cost:   16
c ---[2597]---> BDD-cost:   14
c ---[2596]---> BDD-cost:   16
c ---[2595]---> BDD-cost:   16
c ---[2594]---> BDD-cost:   15
c ---[2593]---> BDD-cost:   16
c ---[2592]---> BDD-cost:   14
c ---[2591]---> BDD-cost:   16
c ---[2590]---> BDD-cost:   15
c ---[2589]---> BDD-cost:   16
c ---[2587]---> BDD-cost:   15
c ---[2586]---> BDD-cost:   16
c ---[2584]---> BDD-cost:   15
c ---[2583]---> BDD-cost:   16
c ---[2582]---> BDD-cost:   16
c ---[2581]---> BDD-cost:   16
c ---[2580]---> BDD-cost:   13
c ---[2579]---> BDD-cost:   14
c ---[2576]---> BDD-cost:   16
c ---[2575]---> BDD-cost:   16
c ---[2574]---> BDD-cost:   16
c ---[2572]---> BDD-cost:   14
c ---[2571]---> BDD-cost:   16
c ---[2570]---> BDD-cost:   16
c ---[2569]---> BDD-cost:   14
c ---[2568]---> BDD-cost:   16
c ---[2567]---> BDD-cost:   13
c ---[2566]---> BDD-cost:   15
c ---[2565]---> BDD-cost:   15
c ---[2564]---> BDD-cost:   16
c ---[2563]---> BDD-cost:   16
c ---[2562]---> BDD-cost:   16
c ---[2561]---> BDD-cost:   15
c ---[2559]---> BDD-cost:   15
c ---[2558]---> BDD-cost:   15
c ---[2557]---> BDD-cost:   16
c ---[2556]---> BDD-cost:   16
c ---[2554]---> BDD-cost:   14
c ---[2553]---> BDD-cost:   15
c ---[2550]---> BDD-cost:   15
c ---[2549]---> BDD-cost:   15
c ---[2548]---> BDD-cost:   14
c ---[2546]---> BDD-cost:   16
c ---[2545]---> BDD-cost:   13
c ---[2543]---> BDD-cost:   15
c ---[2541]---> BDD-cost:   16
c ---[2540]---> BDD-cost:   14
c ---[2539]---> BDD-cost:   16
c ---[2538]---> BDD-cost:   16
c ---[2537]---> BDD-cost:   16
c ---[2535]---> BDD-cost:   15
c ---[2533]---> BDD-cost:   15
c ---[2532]---> BDD-cost:   16
c ---[2531]---> BDD-cost:   14
c ---[2530]---> BDD-cost:   16
c ---[2529]---> BDD-cost:   15
c ---[2528]---> BDD-cost:   16
c ---[2527]---> BDD-cost:   16
c ---[2526]---> BDD-cost:   15
c ---[2524]---> BDD-cost:   16
c ---[2523]---> BDD-cost:   15
c ---[2522]---> BDD-cost:   16
c ---[2520]---> BDD-cost:   13
c ---[2519]---> BDD-cost:   15
c ---[2518]---> BDD-cost:   15
c ---[2517]---> BDD-cost:   16
c ---[2516]---> BDD-cost:   16
c ---[2515]---> BDD-cost:   15
c ---[2514]---> BDD-cost:   15
c ---[2513]---> BDD-cost:   15
c ---[2512]---> BDD-cost:   15
c ---[2511]---> BDD-cost:   16
c ---[2510]---> BDD-cost:   14
c ---[2509]---> BDD-cost:   16
c ---[2507]---> BDD-cost:   15
c ---[2506]---> BDD-cost:   15
c ---[2505]---> BDD-cost:   15
c ---[2504]---> BDD-cost:   16
c ---[2503]---> BDD-cost:   15
c ---[2502]---> BDD-cost:   16
c ---[2499]---> BDD-cost:   14
c ---[2498]---> BDD-cost:   16
c ---[2497]---> BDD-cost:   16
c ---[2495]---> BDD-cost:   16
c ---[2491]---> BDD-cost:   16
c ---[2489]---> BDD-cost:   15
c ---[2488]---> BDD-cost:   15
c ---[2484]---> BDD-cost:   15
c ---[2483]---> BDD-cost:   16
c ---[2482]---> BDD-cost:   16
c ---[2481]---> BDD-cost:   14
c ---[2479]---> BDD-cost:   13
c ---[2477]---> BDD-cost:   15
c ---[2476]---> BDD-cost:   16
c ---[2475]---> BDD-cost:   16
c ---[2474]---> BDD-cost:   16
c ---[2473]---> BDD-cost:   14
c ---[2472]---> BDD-cost:   16
c ---[2471]---> BDD-cost:   15
c ---[2470]---> BDD-cost:   16
c ---[2469]---> BDD-cost:   15
c ---[2468]---> BDD-cost:   15
c ---[2467]---> BDD-cost:   15
c ---[2466]---> BDD-cost:   16
c ---[2464]---> BDD-cost:   14
c ---[2463]---> BDD-cost:   15
c ---[2462]---> BDD-cost:   15
c ---[2460]---> BDD-cost:   14
c ---[2459]---> BDD-cost:   16
c ---[2457]---> BDD-cost:   14
c ---[2456]---> BDD-cost:   14
c ---[2454]---> BDD-cost:   16
c ---[2453]---> BDD-cost:   13
c ---[2451]---> BDD-cost:   16
c ---[2450]---> BDD-cost:   16
c ---[2449]---> BDD-cost:   16
c ---[2447]---> BDD-cost:   15
c ---[2446]---> BDD-cost:   16
c ---[2445]---> BDD-cost:   15
c ---[2444]---> BDD-cost:   13
c ---[2443]---> BDD-cost:   16
c ---[2442]---> BDD-cost:   16
c ---[2440]---> BDD-cost:   15
c ---[2439]---> BDD-cost:   16
c ---[2438]---> BDD-cost:   15
c ---[2437]---> BDD-cost:   15
c ---[2436]---> BDD-cost:   14
c ---[2435]---> BDD-cost:   16
c ---[2434]---> BDD-cost:   16
c ---[2433]---> BDD-cost:   16
c ---[2432]---> BDD-cost:   16
c ---[2431]---> BDD-cost:   16
c ---[2430]---> BDD-cost:   15
c ---[2429]---> BDD-cost:   16
c ---[2428]---> BDD-cost:   15
c ---[2427]---> BDD-cost:   16
c ---[2426]---> BDD-cost:   16
c ---[2425]---> BDD-cost:   15
c ---[2424]---> BDD-cost:   16
c ---[2423]---> BDD-cost:   14
c ---[2422]---> BDD-cost:   15
c ---[2421]---> BDD-cost:   13
c ---[2419]---> BDD-cost:   14
c ---[2418]---> BDD-cost:   14
c ---[2417]---> BDD-cost:   15
c ---[2416]---> BDD-cost:   16
c ---[2415]---> BDD-cost:   15
c ---[2413]---> BDD-cost:   15
c ---[2412]---> BDD-cost:   16
c ---[2410]---> BDD-cost:   16
c ---[2409]---> BDD-cost:   16
c ---[2408]---> BDD-cost:   14
c ---[2407]---> BDD-cost:   16
c ---[2406]---> BDD-cost:   14
c ---[2405]---> BDD-cost:   16
c ---[2404]---> BDD-cost:   15
c ---[2403]---> BDD-cost:   16
c ---[2402]---> BDD-cost:   14
c ---[2401]---> BDD-cost:   16
c ---[2400]---> BDD-cost:   15
c ---[2399]---> BDD-cost:   16
c ---[2398]---> BDD-cost:   13
c ---[2397]---> BDD-cost:   15
c ---[2396]---> BDD-cost:   15
c ---[2395]---> BDD-cost:   16
c ---[2394]---> BDD-cost:   15
c ---[2393]---> BDD-cost:   13
c ---[2392]---> BDD-cost:   16
c ---[2390]---> BDD-cost:   15
c ---[2389]---> BDD-cost:   14
c ---[2388]---> BDD-cost:   16
c ---[2387]---> BDD-cost:   14
c ---[2386]---> BDD-cost:   16
c ---[2385]---> BDD-cost:   15
c ---[2384]---> BDD-cost:   16
c ---[2383]---> BDD-cost:   16
c ---[2382]---> BDD-cost:   16
c ---[2381]---> BDD-cost:   13
c ---[2379]---> BDD-cost:   15
c ---[2378]---> BDD-cost:   15
c ---[2377]---> BDD-cost:   16
c ---[2376]---> BDD-cost:   16
c ---[2375]---> BDD-cost:   14
c ---[2374]---> BDD-cost:   15
c ---[2373]---> BDD-cost:   15
c ---[2372]---> BDD-cost:   15
c ---[2371]---> BDD-cost:   15
c ---[2370]---> BDD-cost:   13
c ---[2369]---> BDD-cost:   16
c ---[2367]---> BDD-cost:   15
c ---[2366]---> BDD-cost:   16
c ---[2365]---> BDD-cost:   16
c ---[2364]---> BDD-cost:   13
c ---[2363]---> BDD-cost:   16
c ---[2362]---> BDD-cost:   14
c ---[2361]---> BDD-cost:   16
c ---[2360]---> BDD-cost:   15
c ---[2359]---> BDD-cost:   15
c ---[2358]---> BDD-cost:   15
c ---[2357]---> BDD-cost:   16
c ---[2356]---> BDD-cost:   16
c ---[2354]---> BDD-cost:   14
c ---[2353]---> BDD-cost:   16
c ---[2352]---> BDD-cost:   16
c ---[2350]---> BDD-cost:   16
c ---[2348]---> BDD-cost:   13
c ---[2347]---> BDD-cost:   14
c ---[2346]---> BDD-cost:   16
c ---[2345]---> BDD-cost:   16
c ---[2344]---> BDD-cost:   16
c ---[2342]---> BDD-cost:   16
c ---[2341]---> BDD-cost:   16
c ---[2340]---> BDD-cost:   16
c ---[2338]---> BDD-cost:   16
c ---[2337]---> BDD-cost:   15
c ---[2336]---> BDD-cost:   16
c ---[2334]---> BDD-cost:   16
c ---[2333]---> BDD-cost:   16
c ---[2332]---> BDD-cost:   13
c ---[2331]---> BDD-cost:   15
c ---[2330]---> BDD-cost:   16
c ---[2329]---> BDD-cost:   16
c ---[2328]---> BDD-cost:   16
c ---[2327]---> BDD-cost:   16
c ---[2324]---> BDD-cost:   14
c ---[2321]---> BDD-cost:   16
c ---[2320]---> BDD-cost:   15
c ---[2319]---> BDD-cost:   16
c ---[2318]---> BDD-cost:   16
c ---[2317]---> BDD-cost:   16
c ---[2315]---> BDD-cost:   16
c ---[2314]---> BDD-cost:   14
c ---[2313]---> BDD-cost:   15
c ---[2312]---> BDD-cost:   16
c ---[2311]---> BDD-cost:   15
c ---[2310]---> BDD-cost:   15
c ---[2309]---> BDD-cost:   14
c ---[2307]---> BDD-cost:   16
c ---[2306]---> BDD-cost:   13
c ---[2305]---> BDD-cost:   13
c ---[2304]---> BDD-cost:   16
c ---[2303]---> BDD-cost:   16
c ---[2302]---> BDD-cost:   16
c ---[2301]---> BDD-cost:   16
c ---[2300]---> BDD-cost:   15
c ---[2299]---> BDD-cost:   15
c ---[2298]---> BDD-cost:   14
c ---[2297]---> BDD-cost:   13
c ---[2296]---> BDD-cost:   16
c ---[2294]---> BDD-cost:   15
c ---[2293]---> BDD-cost:   16
c ---[2292]---> BDD-cost:   15
c ---[2291]---> BDD-cost:   14
c ---[2290]---> BDD-cost:   15
c ---[2289]---> BDD-cost:   16
c ---[2288]---> BDD-cost:   14
c ---[2287]---> BDD-cost:   14
c ---[2286]---> BDD-cost:   15
c ---[2285]---> BDD-cost:   15
c ---[2284]---> BDD-cost:   16
c ---[2283]---> BDD-cost:   16
c ---[2282]---> BDD-cost:   14
c ---[2281]---> BDD-cost:   14
c ---[2280]---> BDD-cost:   15
c ---[2279]---> BDD-cost:   16
c ---[2277]---> BDD-cost:   15
c ---[2276]---> BDD-cost:   16
c ---[2275]---> BDD-cost:   16
c ---[2274]---> BDD-cost:   15
c ---[2273]---> BDD-cost:   16
c ---[2272]---> BDD-cost:   15
c ---[2271]---> BDD-cost:   15
c ---[2268]---> BDD-cost:   16
c ---[2267]---> BDD-cost:   14
c ---[2265]---> BDD-cost:   16
c ---[2264]---> BDD-cost:   15
c ---[2263]---> BDD-cost:   15
c ---[2262]---> BDD-cost:   13
c ---[2260]---> BDD-cost:   15
c ---[2259]---> BDD-cost:   15
c ---[2258]---> BDD-cost:   16
c ---[2257]---> BDD-cost:   15
c ---[2256]---> BDD-cost:   15
c ---[2255]---> BDD-cost:   16
c ---[2254]---> BDD-cost:   14
c ---[2253]---> BDD-cost:   16
c ---[2252]---> BDD-cost:   16
c ---[2251]---> BDD-cost:   15
c ---[2250]---> BDD-cost:   16
c ---[2249]---> BDD-cost:   16
c ---[2248]---> BDD-cost:   14
c ---[2247]---> BDD-cost:   15
c ---[2246]---> BDD-cost:   14
c ---[2245]---> BDD-cost:   15
c ---[2244]---> BDD-cost:   16
c ---[2243]---> BDD-cost:   16
c ---[2242]---> BDD-cost:   15
c ---[2241]---> BDD-cost:   16
c ---[2240]---> BDD-cost:   15
c ---[2239]---> BDD-cost:   16
c ---[2238]---> BDD-cost:   16
c ---[2237]---> BDD-cost:   15
c ---[2236]---> BDD-cost:   16
c ---[2235]---> BDD-cost:   14
c ---[2234]---> BDD-cost:   16
c ---[2233]---> BDD-cost:   16
c ---[2232]---> BDD-cost:   16
c ---[2231]---> BDD-cost:   15
c ---[2230]---> BDD-cost:   16
c ---[2229]---> BDD-cost:   14
c ---[2228]---> BDD-cost:   16
c ---[2226]---> BDD-cost:   15
c ---[2225]---> BDD-cost:   15
c ---[2224]---> BDD-cost:   15
c ---[2223]---> BDD-cost:   16
c ---[2222]---> BDD-cost:   16
c ---[2221]---> BDD-cost:   16
c ---[2220]---> BDD-cost:   15
c ---[2219]---> BDD-cost:   15
c ---[2218]---> BDD-cost:   13
c ---[2217]---> BDD-cost:   16
c ---[2216]---> BDD-cost:   16
c ---[2215]---> BDD-cost:   15
c ---[2214]---> BDD-cost:   15
c ---[2213]---> BDD-cost:   14
c ---[2212]---> BDD-cost:   13
c ---[2211]---> BDD-cost:   16
c ---[2210]---> BDD-cost:   16
c ---[2208]---> BDD-cost:   13
c ---[2207]---> BDD-cost:   15
c ---[2206]---> BDD-cost:   15
c ---[2205]---> BDD-cost:   16
c ---[2204]---> BDD-cost:   15
c ---[2203]---> BDD-cost:   16
c ---[2202]---> BDD-cost:   16
c ---[2200]---> BDD-cost:   16
c ---[2199]---> BDD-cost:   16
c ---[2198]---> BDD-cost:   14
c ---[2195]---> BDD-cost:   16
c ---[2194]---> BDD-cost:   13
c ---[2193]---> BDD-cost:   15
c ---[2192]---> BDD-cost:   14
c ---[2191]---> BDD-cost:   15
c ---[2190]---> BDD-cost:   16
c ---[2189]---> BDD-cost:   15
c ---[2188]---> BDD-cost:   16
c ---[2187]---> BDD-cost:   16
c ---[2186]---> BDD-cost:   16
c ---[2184]---> BDD-cost:   13
c ---[2182]---> BDD-cost:   16
c ---[2181]---> BDD-cost:   16
c ---[2180]---> BDD-cost:   14
c ---[2179]---> BDD-cost:   15
c ---[2178]---> BDD-cost:   16
c ---[2177]---> BDD-cost:   16
c ---[2175]---> BDD-cost:   16
c ---[2173]---> BDD-cost:   13
c ---[2172]---> BDD-cost:   15
c ---[2171]---> BDD-cost:   16
c ---[2170]---> BDD-cost:   14
c ---[2168]---> BDD-cost:   16
c ---[2167]---> BDD-cost:   15
c ---[2166]---> BDD-cost:   16
c ---[2165]---> BDD-cost:   16
c ---[2164]---> BDD-cost:   16
c ---[2163]---> BDD-cost:   16
c ---[2162]---> BDD-cost:   15
c ---[2161]---> BDD-cost:   15
c ---[2159]---> BDD-cost:   14
c ---[2158]---> BDD-cost:   15
c ---[2157]---> BDD-cost:   15
c ---[2155]---> BDD-cost:   15
c ---[2154]---> BDD-cost:   16
c ---[2153]---> BDD-cost:   16
c ---[2152]---> BDD-cost:   15
c ---[2151]---> BDD-cost:   16
c ---[2150]---> BDD-cost:   16
c ---[2149]---> BDD-cost:   16
c ---[2148]---> BDD-cost:   14
c ---[2147]---> BDD-cost:   14
c ---[2146]---> BDD-cost:   16
c ---[2145]---> BDD-cost:   16
c ---[2144]---> BDD-cost:   16
c ---[2143]---> BDD-cost:   16
c ---[2142]---> BDD-cost:   16
c ---[2141]---> BDD-cost:   13
c ---[2140]---> BDD-cost:   15
c ---[2139]---> BDD-cost:   13
c ---[2137]---> BDD-cost:   15
c ---[2136]---> BDD-cost:   16
c ---[2135]---> BDD-cost:   16
c ---[2134]---> BDD-cost:   16
c ---[2133]---> BDD-cost:   15
c ---[2132]---> BDD-cost:   15
c ---[2131]---> BDD-cost:   15
c ---[2130]---> BDD-cost:   15
c ---[2129]---> BDD-cost:   15
c ---[2128]---> BDD-cost:   16
c ---[2127]---> BDD-cost:   16
c ---[2126]---> BDD-cost:   15
c ---[2124]---> BDD-cost:   16
c ---[2123]---> BDD-cost:   15
c ---[2122]---> BDD-cost:   14
c ---[2121]---> BDD-cost:   13
c ---[2120]---> BDD-cost:   16
c ---[2119]---> BDD-cost:   15
c ---[2118]---> BDD-cost:   15
c ---[2117]---> BDD-cost:   14
c ---[2116]---> BDD-cost:   16
c ---[2115]---> BDD-cost:   16
c ---[2114]---> BDD-cost:   16
c ---[2113]---> BDD-cost:   15
c ---[2112]---> BDD-cost:   16
c ---[2111]---> BDD-cost:   16
c ---[2110]---> BDD-cost:   16
c ---[2109]---> BDD-cost:   16
c ---[2107]---> BDD-cost:   16
c ---[2106]---> BDD-cost:   13
c ---[2105]---> BDD-cost:   15
c ---[2104]---> BDD-cost:   16
c ---[2102]---> BDD-cost:   16
c ---[2101]---> BDD-cost:   15
c ---[2100]---> BDD-cost:   16
c ---[2099]---> BDD-cost:   16
c ---[2098]---> BDD-cost:   16
c ---[2097]---> BDD-cost:   16
c ---[2096]---> BDD-cost:   14
c ---[2095]---> BDD-cost:   16
c ---[2093]---> BDD-cost:   14
c ---[2092]---> BDD-cost:   14
c ---[2091]---> BDD-cost:   16
c ---[2090]---> BDD-cost:   16
c ---[2089]---> BDD-cost:   15
c ---[2088]---> BDD-cost:   15
c ---[2087]---> BDD-cost:   15
c ---[2086]---> BDD-cost:   16
c ---[2084]---> BDD-cost:   16
c ---[2083]---> BDD-cost:   16
c ---[2082]---> BDD-cost:   15
c ---[2081]---> BDD-cost:   15
c ---[2080]---> BDD-cost:   16
c ---[2079]---> BDD-cost:   16
c ---[2078]---> BDD-cost:   16
c ---[2077]---> BDD-cost:   15
c ---[2076]---> BDD-cost:   15
c ---[2075]---> BDD-cost:   14
c ---[2074]---> BDD-cost:   15
c ---[2073]---> BDD-cost:   15
c ---[2072]---> BDD-cost:   16
c ---[2071]---> BDD-cost:   16
c ---[2070]---> BDD-cost:   16
c ---[2069]---> BDD-cost:   16
c ---[2068]---> BDD-cost:   15
c ---[2067]---> BDD-cost:   14
c ---[2066]---> BDD-cost:   16
c ---[2065]---> BDD-cost:   16
c ---[2064]---> BDD-cost:   14
c ---[2063]---> BDD-cost:   15
c ---[2062]---> BDD-cost:   13
c ---[2061]---> BDD-cost:   16
c ---[2060]---> BDD-cost:   15
c ---[2059]---> BDD-cost:   14
c ---[2058]---> BDD-cost:   16
c ---[2057]---> BDD-cost:   15
c ---[2056]---> BDD-cost:   15
c ---[2055]---> BDD-cost:   14
c ---[2054]---> BDD-cost:   15
c ---[2052]---> BDD-cost:   16
c ---[2051]---> BDD-cost:   15
c ---[2050]---> BDD-cost:   16
c ---[2048]---> BDD-cost:   16
c ---[2047]---> BDD-cost:   15
c ---[2046]---> BDD-cost:   16
c ---[2045]---> BDD-cost:   16
c ---[2044]---> BDD-cost:   15
c ---[2042]---> BDD-cost:   15
c ---[2041]---> BDD-cost:   16
c ---[2040]---> BDD-cost:   16
c ---[2039]---> BDD-cost:   14
c ---[2038]---> BDD-cost:   15
c ---[2037]---> BDD-cost:   16
c ---[2036]---> BDD-cost:   16
c ---[2034]---> BDD-cost:   16
c ---[2033]---> BDD-cost:   15
c ---[2031]---> BDD-cost:   16
c ---[2030]---> BDD-cost:   13
c ---[2029]---> BDD-cost:   14
c ---[2028]---> BDD-cost:   15
c ---[2027]---> BDD-cost:   16
c ---[2026]---> BDD-cost:   16
c ---[2025]---> BDD-cost:   16
c ---[2024]---> BDD-cost:   16
c ---[2023]---> BDD-cost:   16
c ---[2022]---> BDD-cost:   15
c ---[2021]---> BDD-cost:   16
c ---[2020]---> BDD-cost:   15
c ---[2019]---> BDD-cost:   15
c ---[2018]---> BDD-cost:   14
c ---[2017]---> BDD-cost:   16
c ---[2015]---> BDD-cost:   16
c ---[2014]---> BDD-cost:   15
c ---[2013]---> BDD-cost:   15
c ---[2012]---> BDD-cost:   15
c ---[2011]---> BDD-cost:   16
c ---[2010]---> BDD-cost:   16
c ---[2009]---> BDD-cost:   16
c ---[2008]---> BDD-cost:   14
c ---[2007]---> BDD-cost:   16
c ---[2006]---> BDD-cost:   16
c ---[2005]---> BDD-cost:   16
c ---[2004]---> BDD-cost:   15
c ---[2003]---> BDD-cost:   16
c ---[2002]---> BDD-cost:   16
c ---[2001]---> BDD-cost:   16
c ---[2000]---> BDD-cost:   15
c ---[1999]---> BDD-cost:   15
c ---[1998]---> BDD-cost:   14
c ---[1997]---> BDD-cost:   16
c ---[1995]---> BDD-cost:   15
c ---[1994]---> BDD-cost:   14
c ---[1993]---> BDD-cost:   16
c ---[1992]---> BDD-cost:   15
c ---[1991]---> BDD-cost:   16
c ---[1990]---> BDD-cost:   15
c ---[1989]---> BDD-cost:   13
c ---[1988]---> BDD-cost:   15
c ---[1987]---> BDD-cost:   16
c ---[1986]---> BDD-cost:   14
c ---[1985]---> BDD-cost:   15
c ---[1984]---> BDD-cost:   15
c ---[1983]---> BDD-cost:   15
c ---[1982]---> BDD-cost:   15
c ---[1981]---> BDD-cost:   15
c ---[1980]---> BDD-cost:   14
c ---[1979]---> BDD-cost:   15
c ---[1978]---> BDD-cost:   16
c ---[1977]---> BDD-cost:   15
c ---[1975]---> BDD-cost:   15
c ---[1974]---> BDD-cost:   15
c ---[1973]---> BDD-cost:   14
c ---[1972]---> BDD-cost:   13
c ---[1971]---> BDD-cost:   16
c ---[1970]---> BDD-cost:   15
c ---[1969]---> BDD-cost:   15
c ---[1968]---> BDD-cost:   16
c ---[1967]---> BDD-cost:   15
c ---[1966]---> BDD-cost:   16
c ---[1965]---> BDD-cost:   14
c ---[1964]---> BDD-cost:   15
c ---[1963]---> BDD-cost:   15
c ---[1962]---> BDD-cost:   16
c ---[1960]---> BDD-cost:   16
c ---[1959]---> BDD-cost:   15
c ---[1958]---> BDD-cost:   14
c ---[1957]---> BDD-cost:   14
c ---[1956]---> BDD-cost:   16
c ---[1955]---> BDD-cost:   16
c ---[1954]---> BDD-cost:   16
c ---[1952]---> BDD-cost:   16
c ---[1951]---> BDD-cost:   16
c ---[1949]---> BDD-cost:   16
c ---[1948]---> BDD-cost:   15
c ---[1947]---> BDD-cost:   15
c ---[1946]---> BDD-cost:   16
c ---[1945]---> BDD-cost:   15
c ---[1944]---> BDD-cost:   16
c ---[1943]---> BDD-cost:   15
c ---[1942]---> BDD-cost:   15
c ---[1941]---> BDD-cost:   16
c ---[1940]---> BDD-cost:   15
c ---[1939]---> BDD-cost:   14
c ---[1935]---> BDD-cost:   16
c ---[1934]---> BDD-cost:   15
c ---[1931]---> BDD-cost:   16
c ---[1930]---> BDD-cost:   15
c ---[1929]---> BDD-cost:   15
c ---[1926]---> BDD-cost:   16
c ---[1924]---> BDD-cost:   16
c ---[1923]---> BDD-cost:   15
c ---[1922]---> BDD-cost:   16
c ---[1921]---> BDD-cost:   15
c ---[1920]---> BDD-cost:   16
c ---[1919]---> BDD-cost:   15
c ---[1918]---> BDD-cost:   15
c ---[1917]---> BDD-cost:   16
c ---[1916]---> BDD-cost:   16
c ---[1915]---> BDD-cost:   16
c ---[1914]---> BDD-cost:   16
c ---[1913]---> BDD-cost:   15
c ---[1912]---> BDD-cost:   15
c ---[1911]---> BDD-cost:   16
c ---[1910]---> BDD-cost:   16
c ---[1909]---> BDD-cost:   15
c ---[1908]---> BDD-cost:   16
c ---[1907]---> BDD-cost:   15
c ---[1906]---> BDD-cost:   16
c ---[1905]---> BDD-cost:   16
c ---[1904]---> BDD-cost:   15
c ---[1903]---> BDD-cost:   16
c ---[1902]---> BDD-cost:   16
c ---[1901]---> BDD-cost:   14
c ---[1900]---> BDD-cost:   14
c ---[1899]---> BDD-cost:   16
c ---[1898]---> BDD-cost:   16
c ---[1897]---> BDD-cost:   15
c ---[1896]---> BDD-cost:   15
c ---[1895]---> BDD-cost:   15
c ---[1893]---> BDD-cost:   13
c ---[1892]---> BDD-cost:   16
c ---[1891]---> BDD-cost:   13
c ---[1890]---> BDD-cost:   16
c ---[1889]---> BDD-cost:   16
c ---[1888]---> BDD-cost:   16
c ---[1887]---> BDD-cost:   14
c ---[1886]---> BDD-cost:   16
c ---[1885]---> BDD-cost:   16
c ---[1883]---> BDD-cost:   15
c ---[1882]---> BDD-cost:   14
c ---[1881]---> BDD-cost:   16
c ---[1879]---> BDD-cost:   15
c ---[1878]---> BDD-cost:   16
c ---[1877]---> BDD-cost:   16
c ---[1875]---> BDD-cost:   16
c ---[1874]---> BDD-cost:   16
c ---[1872]---> BDD-cost:   13
c ---[1871]---> BDD-cost:   16
c ---[1869]---> BDD-cost:   16
c ---[1868]---> BDD-cost:   16
c ---[1867]---> BDD-cost:   16
c ---[1865]---> BDD-cost:   16
c ---[1862]---> BDD-cost:   14
c ---[1861]---> BDD-cost:   15
c ---[1860]---> BDD-cost:   16
c ---[1859]---> BDD-cost:   15
c ---[1858]---> BDD-cost:   16
c ---[1857]---> BDD-cost:   15
c ---[1856]---> BDD-cost:   14
c ---[1855]---> BDD-cost:   16
c ---[1854]---> BDD-cost:   15
c ---[1853]---> BDD-cost:   15
c ---[1851]---> BDD-cost:   15
c ---[1850]---> BDD-cost:   16
c ---[1849]---> BDD-cost:   14
c ---[1848]---> BDD-cost:   14
c ---[1847]---> BDD-cost:   16
c ---[1846]---> BDD-cost:   15
c ---[1845]---> BDD-cost:   15
c ---[1844]---> BDD-cost:   15
c ---[1843]---> BDD-cost:   16
c ---[1842]---> BDD-cost:   14
c ---[1841]---> BDD-cost:   16
c ---[1840]---> BDD-cost:   14
c ---[1839]---> BDD-cost:   15
c ---[1838]---> BDD-cost:   15
c ---[1837]---> BDD-cost:   16
c ---[1836]---> BDD-cost:   16
c ---[1833]---> BDD-cost:   16
c ---[1832]---> BDD-cost:   14
c ---[1831]---> BDD-cost:   15
c ---[1830]---> BDD-cost:   16
c ---[1829]---> BDD-cost:   14
c ---[1828]---> BDD-cost:   14
c ---[1825]---> BDD-cost:   16
c ---[1824]---> BDD-cost:   16
c ---[1823]---> BDD-cost:   16
c ---[1822]---> BDD-cost:   14
c ---[1821]---> BDD-cost:   16
c ---[1820]---> BDD-cost:   16
c ---[1819]---> BDD-cost:   15
c ---[1818]---> BDD-cost:   16
c ---[1817]---> BDD-cost:   14
c ---[1816]---> BDD-cost:   16
c ---[1814]---> BDD-cost:   15
c ---[1813]---> BDD-cost:   16
c ---[1811]---> BDD-cost:   16
c ---[1810]---> BDD-cost:   15
c ---[1809]---> BDD-cost:   14
c ---[1807]---> BDD-cost:   16
c ---[1806]---> BDD-cost:   15
c ---[1805]---> BDD-cost:   13
c ---[1804]---> BDD-cost:   14
c ---[1803]---> BDD-cost:   16
c ---[1802]---> BDD-cost:   16
c ---[1800]---> BDD-cost:   14
c ---[1799]---> BDD-cost:   16
c ---[1798]---> BDD-cost:   15
c ---[1797]---> BDD-cost:   16
c ---[1796]---> BDD-cost:   15
c ---[1795]---> BDD-cost:   15
c ---[1794]---> BDD-cost:   16
c ---[1793]---> BDD-cost:   16
c ---[1792]---> BDD-cost:   16
c ---[1791]---> BDD-cost:   16
c ---[1788]---> BDD-cost:   16
c ---[1786]---> BDD-cost:   15
c ---[1785]---> BDD-cost:   16
c ---[1783]---> BDD-cost:   14
c ---[1782]---> BDD-cost:   15
c ---[1781]---> BDD-cost:   15
c ---[1780]---> BDD-cost:   16
c ---[1779]---> BDD-cost:   16
c ---[1778]---> BDD-cost:   14
c ---[1777]---> BDD-cost:   16
c ---[1776]---> BDD-cost:   13
c ---[1775]---> BDD-cost:   16
c ---[1774]---> BDD-cost:   16
c ---[1773]---> BDD-cost:   16
c ---[1772]---> BDD-cost:   14
c ---[1771]---> BDD-cost:   16
c ---[1769]---> BDD-cost:   15
c ---[1766]---> BDD-cost:   16
c ---[1765]---> BDD-cost:   15
c ---[1764]---> BDD-cost:   16
c ---[1763]---> BDD-cost:   16
c ---[1762]---> BDD-cost:   14
c ---[1761]---> BDD-cost:   15
c ---[1760]---> BDD-cost:   16
c ---[1759]---> BDD-cost:   14
c ---[1758]---> BDD-cost:   15
c ---[1757]---> BDD-cost:   16
c ---[1755]---> BDD-cost:   16
c ---[1753]---> BDD-cost:   15
c ---[1752]---> BDD-cost:   16
c ---[1751]---> BDD-cost:   16
c ---[1750]---> BDD-cost:   15
c ---[1749]---> BDD-cost:   16
c ---[1748]---> BDD-cost:   16
c ---[1747]---> BDD-cost:   14
c ---[1746]---> BDD-cost:   16
c ---[1745]---> BDD-cost:   16
c ---[1744]---> BDD-cost:   16
c ---[1743]---> BDD-cost:   15
c ---[1741]---> BDD-cost:   15
c ---[1740]---> BDD-cost:   15
c ---[1739]---> BDD-cost:   16
c ---[1738]---> BDD-cost:   15
c ---[1737]---> BDD-cost:   15
c ---[1736]---> BDD-cost:   16
c ---[1735]---> BDD-cost:   16
c ---[1734]---> BDD-cost:   15
c ---[1732]---> BDD-cost:   15
c ---[1731]---> BDD-cost:   16
c ---[1730]---> BDD-cost:   16
c ---[1729]---> BDD-cost:   16
c ---[1728]---> BDD-cost:   16
c ---[1727]---> BDD-cost:   14
c ---[1725]---> BDD-cost:   16
c ---[1724]---> BDD-cost:   14
c ---[1723]---> BDD-cost:   15
c ---[1722]---> BDD-cost:   15
c ---[1721]---> BDD-cost:   14
c ---[1719]---> BDD-cost:   15
c ---[1717]---> BDD-cost:   16
c ---[1716]---> BDD-cost:   15
c ---[1715]---> BDD-cost:   16
c ---[1714]---> BDD-cost:   14
c ---[1713]---> BDD-cost:   15
c ---[1712]---> BDD-cost:   16
c ---[1711]---> BDD-cost:   15
c ---[1710]---> BDD-cost:   15
c ---[1709]---> BDD-cost:   16
c ---[1708]---> BDD-cost:   16
c ---[1707]---> BDD-cost:   15
c ---[1706]---> BDD-cost:   15
c ---[1705]---> BDD-cost:   16
c ---[1704]---> BDD-cost:   15
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:   17
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:   22
c ---[1681]---> BDD-cost:    6
c ---[1680]---> BDD-cost:    6
c ---[1679]---> BDD-cost:   19
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:   19
c ---[1669]---> BDD-cost:   20
c ---[1668]---> BDD-cost:   20
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:   17
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:   19
c ---[1647]---> BDD-cost:    3
c ---[1646]---> BDD-cost:   17
c ---[1645]---> BDD-cost:    7
c ---[1644]---> BDD-cost:   22
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:   22
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:   17
c ---[1624]---> BDD-cost:    5
c ---[1623]---> BDD-cost:   17
c ---[1622]---> BDD-cost:    7
c ---[1621]---> BDD-cost:   22
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:   18
c ---[1609]---> BDD-cost:    6
c ---[1608]---> BDD-cost:    5
c ---[1607]---> BDD-cost:    6
c ---[1606]---> BDD-cost:    7
c ---[1605]---> BDD-cost:   20
c ---[1604]---> BDD-cost:   22
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:   18
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:   22
c ---[1574]---> BDD-cost:   22
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:   22
c ---[1543]---> BDD-cost:    8
c ---[1542]---> BDD-cost:    5
c ---[1541]---> BDD-cost:   22
c ---[1540]---> BDD-cost:   22
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:   18
c ---[1529]---> BDD-cost:    8
c ---[1528]---> BDD-cost:   20
c ---[1527]---> BDD-cost:    6
c ---[1526]---> BDD-cost:    4
c ---[1525]---> BDD-cost:    7
c ---[1524]---> BDD-cost:   22
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:   22
c ---[1513]---> BDD-cost:    4
c ---[1512]---> BDD-cost:    6
c ---[1511]---> BDD-cost:    4
c ---[1510]---> BDD-cost:   18
c ---[1509]---> BDD-cost:    4
c ---[1508]---> BDD-cost:    8
c ---[1507]---> BDD-cost:    5
c ---[1506]---> BDD-cost:   21
c ---[1505]---> BDD-cost:    7
c ---[1504]---> BDD-cost:    6
c ---[1503]---> BDD-cost:    3
c ---[1502]---> BDD-cost:   20
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:   21
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:   19
c ---[1487]---> BDD-cost:    7
c ---[1486]---> BDD-cost:    6
c ---[1485]---> BDD-cost:   22
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:   22
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:   18
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:   21
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:   22
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:   20
c ---[1418]---> BDD-cost:    7
c ---[1417]---> BDD-cost:    3
c ---[1416]---> BDD-cost:   20
c ---[1415]---> BDD-cost:    3
c ---[1414]---> BDD-cost:    7
c ---[1413]---> BDD-cost:   19
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:   22
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:   18
c ---[1390]---> BDD-cost:    7
c ---[1389]---> BDD-cost:    7
c ---[1388]---> BDD-cost:    6
c ---[1387]---> BDD-cost:    7
c ---[1386]---> BDD-cost:   21
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:   22
c ---[1372]---> BDD-cost:    6
c ---[1371]---> BDD-cost:    7
c ---[1370]---> BDD-cost:    6
c ---[1369]---> BDD-cost:    7
c ---[1368]---> BDD-cost:   19
c ---[1367]---> BDD-cost:   21
c ---[1366]---> BDD-cost:   22
c ---[1364]---> BDD-cost:   65
c ---[1363]---> BDD-cost:    8
c ---[1362]---> BDD-cost:    6
c ---[1361]---> BDD-cost:   21
c ---[1360]---> BDD-cost:    3
c ---[1359]---> BDD-cost:   20
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:   22
c ---[1352]---> BDD-cost:    3
c ---[1351]---> BDD-cost:    4
c ---[1350]---> BDD-cost:    8
c ---[1349]---> BDD-cost:   19
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:   18
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:   19
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:   20
c ---[1291]---> BDD-cost:    6
c ---[1290]---> BDD-cost:    8
c ---[1289]---> BDD-cost:   20
c ---[1288]---> BDD-cost:   20
c ---[1287]---> BDD-cost:   22
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:   22
c ---[1276]---> BDD-cost:   22
c ---[1275]---> BDD-cost:    5
c ---[1274]---> BDD-cost:   18
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:   20
c ---[1260]---> BDD-cost:    7
c ---[1259]---> BDD-cost:    7
c ---[1258]---> BDD-cost:    4
c ---[1257]---> BDD-cost:   20
c ---[1256]---> BDD-cost:    6
c ---[1255]---> BDD-cost:    7
c ---[1254]---> BDD-cost:    8
c ---[1252]---> BDD-cost:   73
c ---[1251]---> BDD-cost:   22
c ---[1250]---> BDD-cost:   22
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:   20
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:   22
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:   22
c ---[1225]---> BDD-cost:   18
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:   18
c ---[1210]---> BDD-cost:    5
c ---[1209]---> BDD-cost:    5
c ---[1208]---> BDD-cost:    8
c ---[1207]---> BDD-cost:    7
c ---[1206]---> BDD-cost:   20
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:   20
c ---[1191]---> BDD-cost:   19
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:   18
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:   18
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:   20
c ---[1159]---> BDD-cost:    7
c ---[1158]---> BDD-cost:    6
c ---[1157]---> BDD-cost:   22
c ---[1156]---> BDD-cost:    7
c ---[1155]---> BDD-cost:    3
c ---[1154]---> BDD-cost:    6
c ---[1153]---> BDD-cost:   22
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:   18
c ---[1144]---> BDD-cost:    7
c ---[1143]---> BDD-cost:   18
c ---[1142]---> BDD-cost:    5
c ---[1141]---> BDD-cost:    8
c ---[1140]---> BDD-cost:   17
c ---[1139]---> BDD-cost:    6
c ---[1137]---> BDD-cost:   71
c ---[1135]---> BDD-cost:   65
c ---[1134]---> BDD-cost:   18
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:   18
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:   21
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:   20
c ---[1082]---> BDD-cost:    8
c ---[1081]---> BDD-cost:   22
c ---[1080]---> BDD-cost:    5
c ---[1079]---> BDD-cost:    5
c ---[1078]---> BDD-cost:   20
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:   19
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:   21
c ---[1043]---> BDD-cost:    4
c ---[1042]---> BDD-cost:    8
c ---[1041]---> BDD-cost:    7
c ---[1039]---> BDD-cost:   63
c ---[1038]---> BDD-cost:   21
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:   19
c ---[1029]---> BDD-cost:   22
c ---[1027]---> BDD-cost:   71
c ---[1026]---> BDD-cost:    6
c ---[1025]---> BDD-cost:    7
c ---[1024]---> BDD-cost:    3
c ---[1023]---> BDD-cost:   22
c ---[1022]---> BDD-cost:    8
c ---[1021]---> BDD-cost:    8
c ---[1020]---> BDD-cost:    6
c ---[1019]---> BDD-cost:    3
c ---[1018]---> BDD-cost:   19
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:   20
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:   20
c ---[ 969]---> BDD-cost:   20
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:   22
c ---[ 935]---> BDD-cost:    7
c ---[ 934]---> BDD-cost:    5
c ---[ 933]---> BDD-cost:   18
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:   20
c ---[ 923]---> BDD-cost:   22
c ---[ 922]---> BDD-cost:    3
c ---[ 921]---> BDD-cost:    8
c ---[ 920]---> BDD-cost:    7
c ---[ 919]---> BDD-cost:   22
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:   20
c ---[ 897]---> BDD-cost:    7
c ---[ 896]---> BDD-cost:   17
c ---[ 895]---> BDD-cost:    7
c ---[ 893]---> BDD-cost:   57
c ---[ 891]---> Adder-cost: 2156   maxlim: 2895835   bits: 23/22
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:   21
c ---[ 882]---> BDD-cost:    8
c ---[ 881]---> BDD-cost:    7
c ---[ 879]---> Adder-cost: 2318   maxlim: 3144667   bits: 23/22
c ---[ 878]---> BDD-cost:    4
c ---[ 877]---> BDD-cost:   21
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: 2324   maxlim: 3258332   bits: 23/22
c ---[ 866]---> BDD-cost:    6
c ---[ 865]---> BDD-cost:    3
c ---[ 864]---> BDD-cost:    3
c ---[ 863]---> BDD-cost:    3
c ---[ 862]---> BDD-cost:   20
c ---[ 861]---> BDD-cost:    6
c ---[ 860]---> BDD-cost:    3
c ---[ 859]---> BDD-cost:    8
c ---[ 858]---> BDD-cost:   19
c ---[ 857]---> BDD-cost:   19
c ---[ 855]---> Adder-cost: 1992   maxlim: 2337762   bits: 23/22
c ---[ 854]---> BDD-cost:    7
c ---[ 853]---> BDD-cost:    8
c ---[ 852]---> BDD-cost:    8
c ---[ 851]---> BDD-cost:    5
c ---[ 850]---> BDD-cost:   18
c ---[ 849]---> BDD-cost:    5
c ---[ 848]---> BDD-cost:   22
c ---[ 847]---> BDD-cost:    7
c ---[ 846]---> BDD-cost:    8
c ---[ 845]---> BDD-cost:    6
c ---[ 843]---> Adder-cost: 2106   maxlim: 3205085   bits: 23/22
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:   21
c ---[ 831]---> Adder-cost: 2300   maxlim: 3529693   bits: 23/22
c ---[ 830]---> BDD-cost:    5
c ---[ 829]---> BDD-cost:    7
c ---[ 828]---> BDD-cost:    3
c ---[ 827]---> BDD-cost:   21
c ---[ 826]---> BDD-cost:    4
c ---[ 825]---> BDD-cost:    6
c ---[ 824]---> BDD-cost:   22
c ---[ 823]---> BDD-cost:    5
c ---[ 822]---> BDD-cost:   19
c ---[ 821]---> BDD-cost:    5
c ---[ 819]---> Adder-cost: 2034   maxlim: 2619359   bits: 23/22
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: 2372   maxlim: 3350491   bits: 23/22
c ---[ 806]---> BDD-cost:    5
c ---[ 805]---> BDD-cost:    7
c ---[ 804]---> BDD-cost:    3
c ---[ 803]---> BDD-cost:   18
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:   20
c ---[ 795]---> Adder-cost: 2032   maxlim: 2594782   bits: 23/22
c ---[ 794]---> BDD-cost:    7
c ---[ 793]---> BDD-cost:    8
c ---[ 792]---> BDD-cost:   18
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: 2312   maxlim: 2893788   bits: 23/22
c ---[ 782]---> BDD-cost:    8
c ---[ 781]---> BDD-cost:    7
c ---[ 780]---> BDD-cost:   18
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:   19
c ---[ 771]---> BDD-cost:   67
c ---[ 769]---> Adder-cost: 2158   maxlim: 3303386   bits: 23/22
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: 2220   maxlim: 3007452   bits: 23/22
c ---[ 756]---> BDD-cost:    6
c ---[ 755]---> BDD-cost:   21
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: 2192   maxlim: 3061726   bits: 23/22
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: 2162   maxlim: 2943962   bits: 23/22
c ---[ 732]---> BDD-cost:    3
c ---[ 731]---> BDD-cost:    6
c ---[ 730]---> BDD-cost:   18
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: 2194   maxlim: 2976733   bits: 23/22
c ---[ 720]---> BDD-cost:    8
c ---[ 719]---> BDD-cost:   20
c ---[ 718]---> BDD-cost:   22
c ---[ 717]---> BDD-cost:    6
c ---[ 716]---> BDD-cost:   18
c ---[ 715]---> BDD-cost:   18
c ---[ 714]---> BDD-cost:    8
c ---[ 713]---> BDD-cost:    3
c ---[ 712]---> BDD-cost:    7
c ---[ 711]---> BDD-cost:    6
c ---[ 709]---> Adder-cost: 2032   maxlim: 2712542   bits: 23/22
c ---[ 708]---> BDD-cost:    8
c ---[ 707]---> BDD-cost:   22
c ---[ 706]---> BDD-cost:    8
c ---[ 705]---> BDD-cost:    5
c ---[ 704]---> BDD-cost:    3
c ---[ 703]---> BDD-cost:   19
c ---[ 702]---> BDD-cost:    5
c ---[ 701]---> BDD-cost:    7
c ---[ 700]---> BDD-cost:    6
c ---[ 699]---> BDD-cost:    5
c ---[ 697]---> Adder-cost: 2150   maxlim: 2696158   bits: 23/22
c ---[ 696]---> BDD-cost:   19
c ---[ 695]---> BDD-cost:    8
c ---[ 694]---> BDD-cost:   17
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: 2294   maxlim: 2912221   bits: 23/22
c ---[ 684]---> BDD-cost:    4
c ---[ 683]---> BDD-cost:    7
c ---[ 682]---> BDD-cost:    4
c ---[ 681]---> BDD-cost:   22
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: 2282   maxlim: 3110877   bits: 23/22
c ---[ 672]---> BDD-cost:    6
c ---[ 671]---> BDD-cost:   22
c ---[ 670]---> BDD-cost:   18
c ---[ 669]---> BDD-cost:    5
c ---[ 668]---> BDD-cost:    6
c ---[ 667]---> BDD-cost:   22
c ---[ 666]---> BDD-cost:    5
c ---[ 665]---> BDD-cost:    7
c ---[ 664]---> BDD-cost:    7
c ---[ 663]---> BDD-cost:    6
c ---[ 661]---> Adder-cost: 2220   maxlim: 3010526   bits: 23/22
c ---[ 660]---> BDD-cost:    6
c ---[ 659]---> BDD-cost:    8
c ---[ 658]---> BDD-cost:    7
c ---[ 657]---> BDD-cost:   22
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: 2178   maxlim: 3334108   bits: 23/22
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: 2182   maxlim: 3058652   bits: 23/22
c ---[ 634]---> BDD-cost:    5
c ---[ 633]---> BDD-cost:    7
c ---[ 632]---> BDD-cost:   20
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: 2348   maxlim: 2894812   bits: 23/22
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: 2218   maxlim: 2889693   bits: 23/22
c ---[ 610]---> BDD-cost:    7
c ---[ 609]---> BDD-cost:    7
c ---[ 608]---> BDD-cost:    7
c ---[ 607]---> BDD-cost:    5
c ---[ 606]---> BDD-cost:   20
c ---[ 605]---> BDD-cost:   18
c ---[ 604]---> BDD-cost:    7
c ---[ 603]---> BDD-cost:    5
c ---[ 602]---> BDD-cost:    7
c ---[ 601]---> BDD-cost:    6
c ---[ 599]---> Adder-cost: 2072   maxlim: 2930655   bits: 23/22
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:   19
c ---[ 591]---> BDD-cost:    3
c ---[ 590]---> BDD-cost:   22
c ---[ 589]---> BDD-cost:    8
c ---[ 587]---> Adder-cost: 2184   maxlim: 2863070   bits: 23/22
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:   18
c ---[ 575]---> Adder-cost: 2030   maxlim: 2764767   bits: 23/22
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:   21
c ---[ 567]---> BDD-cost:    4
c ---[ 566]---> BDD-cost:    4
c ---[ 565]---> BDD-cost:    8
c ---[ 563]---> Adder-cost: 2096   maxlim: 2895839   bits: 23/22
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: 2270   maxlim: 3108827   bits: 23/22
c ---[ 550]---> BDD-cost:    5
c ---[ 549]---> BDD-cost:    3
c ---[ 548]---> BDD-cost:    4
c ---[ 547]---> BDD-cost:    5
c ---[ 546]---> BDD-cost:   22
c ---[ 545]---> BDD-cost:    6
c ---[ 544]---> BDD-cost:    7
c ---[ 543]---> BDD-cost:   19
c ---[ 542]---> BDD-cost:    3
c ---[ 541]---> BDD-cost:    8
c ---[ 539]---> Adder-cost: 2254   maxlim: 3202013   bits: 23/22
c ---[ 538]---> BDD-cost:    7
c ---[ 537]---> BDD-cost:    7
c ---[ 536]---> BDD-cost:    3
c ---[ 535]---> BDD-cost:    7
c ---[ 534]---> BDD-cost:   19
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: 2152   maxlim: 2366430   bits: 23/22
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: 2266   maxlim: 3364827   bits: 23/22
c ---[ 512]---> BDD-cost:    6
c ---[ 511]---> BDD-cost:    6
c ---[ 510]---> BDD-cost:   21
c ---[ 509]---> BDD-cost:    8
c ---[ 508]---> BDD-cost:    5
c ---[ 507]---> BDD-cost:    4
c ---[ 506]---> BDD-cost:    8
c ---[ 505]---> BDD-cost:   21
c ---[ 504]---> BDD-cost:    7
c ---[ 503]---> BDD-cost:    7
c ---[ 501]---> Adder-cost: 2314   maxlim: 2833370   bits: 23/22
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: 2288   maxlim: 3790811   bits: 23/22
c ---[ 488]---> BDD-cost:    5
c ---[ 487]---> BDD-cost:    8
c ---[ 486]---> BDD-cost:   22
c ---[ 485]---> BDD-cost:   22
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: 2324   maxlim: 2880476   bits: 23/22
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: 2124   maxlim: 2808797   bits: 23/22
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: 2224   maxlim: 2775007   bits: 23/22
c ---[ 452]---> BDD-cost:    3
c ---[ 451]---> BDD-cost:    5
c ---[ 450]---> BDD-cost:    7
c ---[ 449]---> BDD-cost:    6
c ---[ 448]---> BDD-cost:   20
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: 2096   maxlim: 2678751   bits: 23/22
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: 2134   maxlim: 2991074   bits: 23/22
c ---[ 428]---> BDD-cost:    3
c ---[ 427]---> BDD-cost:   19
c ---[ 426]---> BDD-cost:    8
c ---[ 425]---> BDD-cost:    6
c ---[ 424]---> BDD-cost:   21
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:   20
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:   21
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:   22
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:   21
c ---[ 375]---> BDD-cost:    8
c ---[ 374]---> BDD-cost:    3
c ---[ 373]---> BDD-cost:    7
c ---[ 372]---> BDD-cost:   20
c ---[ 371]---> BDD-cost:    8
c ---[ 370]---> BDD-cost:    7
c ---[ 369]---> BDD-cost:   22
c ---[ 368]---> BDD-cost:   18
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:   22
c ---[ 361]---> BDD-cost:    8
c ---[ 360]---> BDD-cost:    5
c ---[ 359]---> BDD-cost:    8
c ---[ 358]---> BDD-cost:    7
c ---[ 357]---> BDD-cost:   19
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:   22
c ---[ 332]---> BDD-cost:   20
c ---[ 331]---> BDD-cost:    7
c ---[ 330]---> BDD-cost:    4
c ---[ 329]---> BDD-cost:   17
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:   20
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:   22
c ---[ 307]---> BDD-cost:   20
c ---[ 306]---> BDD-cost:    7
c ---[ 305]---> BDD-cost:   17
c ---[ 304]---> BDD-cost:    7
c ---[ 303]---> BDD-cost:    3
c ---[ 302]---> BDD-cost:   22
c ---[ 301]---> BDD-cost:   22
c ---[ 300]---> BDD-cost:    5
c ---[ 299]---> BDD-cost:    7
c ---[ 298]---> BDD-cost:   20
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:   18
c ---[ 282]---> BDD-cost:    7
c ---[ 281]---> BDD-cost:    6
c ---[ 280]---> BDD-cost:   22
c ---[ 279]---> BDD-cost:    6
c ---[ 278]---> BDD-cost:    3
c ---[ 277]---> BDD-cost:    5
c ---[ 276]---> BDD-cost:   19
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:   19
c ---[ 255]---> BDD-cost:    8
c ---[ 254]---> BDD-cost:    8
c ---[ 253]---> BDD-cost:    6
c ---[ 252]---> BDD-cost:   20
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:   19
c ---[ 237]---> BDD-cost:    8
c ---[ 236]---> BDD-cost:    6
c ---[ 235]---> BDD-cost:    8
c ---[ 234]---> BDD-cost:    6
c ---[ 233]---> BDD-cost:   21
c ---[ 232]---> BDD-cost:    6
c ---[ 231]---> BDD-cost:    6
c ---[ 230]---> BDD-cost:    8
c ---[ 229]---> BDD-cost:   21
c ---[ 228]---> BDD-cost:    7
c ---[ 227]---> BDD-cost:    8
c ---[ 226]---> BDD-cost:    8
c ---[ 225]---> BDD-cost:    8
c ---[ 224]---> BDD-cost:   21
c ---[ 223]---> BDD-cost:    6
c ---[ 222]---> BDD-cost:    7
c ---[ 221]---> BDD-cost:    6
c ---[ 220]---> BDD-cost:    3
c ---[ 219]---> BDD-cost:   20
c ---[ 218]---> BDD-cost:   19
c ---[ 217]---> BDD-cost:   21
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:   21
c ---[ 196]---> BDD-cost:   21
c ---[ 195]---> BDD-cost:    3
c ---[ 194]---> BDD-cost:    8
c ---[ 193]---> BDD-cost:    6
c ---[ 192]---> BDD-cost:    8
c ---[ 191]---> BDD-cost:    6
c ---[ 190]---> BDD-cost:    8
c ---[ 189]---> BDD-cost:    6
c ---[ 188]---> BDD-cost:    3
c ---[ 187]---> BDD-cost:    6
c ---[ 186]---> BDD-cost:    6
c ---[ 185]---> BDD-cost:    7
c ---[ 184]---> BDD-cost:    7
c ---[ 183]---> BDD-cost:    1
c ---[ 182]---> BDD-cost:    1
c ---[ 181]---> BDD-cost:    1
c ---[ 180]---> BDD-cost:    1
c ---[ 179]---> BDD-cost:    1
c ---[ 178]---> BDD-cost:    1
c ---[ 177]---> BDD-cost:    1
c ---[ 176]---> BDD-cost:    1
c ---[ 175]---> BDD-cost:    1
c ---[ 174]---> BDD-cost:    1
c ---[ 173]---> BDD-cost:    1
c ---[ 172]---> BDD-cost:    1
c ---[ 171]---> BDD-cost:    1
c ---[ 170]---> BDD-cost:    1
c ---[ 169]---> BDD-cost:    1
c ---[ 168]---> BDD-cost:    1
c ---[ 167]---> BDD-cost:    1
c ---[ 166]---> BDD-cost:    1
c ---[ 165]---> BDD-cost:    1
c ---[ 164]---> BDD-cost:    1
c ---[ 163]---> BDD-cost:    1
c ---[ 162]---> BDD-cost:    1
c ---[ 161]---> BDD-cost:    1
c ---[ 160]---> BDD-cost:    1
c ---[ 159]---> BDD-cost:    1
c ---[ 158]---> BDD-cost:    1
c ---[ 157]---> BDD-cost:    1
c ---[ 156]---> BDD-cost:    1
c ---[ 155]---> BDD-cost:    1
c ---[ 154]---> BDD-cost:    1
c ---[ 153]---> BDD-cost:    1
c ---[ 152]---> BDD-cost:    1
c ---[ 151]---> BDD-cost:    1
c ---[ 150]---> BDD-cost:    1
c ---[ 149]---> BDD-cost:    1
c ---[ 148]---> BDD-cost:    1
c ---[ 147]---> BDD-cost:    1
c ---[ 146]---> BDD-cost:    1
c ---[ 145]---> BDD-cost:    1
c ---[ 144]---> BDD-cost:    1
c ---[ 143]---> BDD-cost:    1
c ---[ 142]---> BDD-cost:    1
c ---[ 141]---> BDD-cost:    1
c ---[ 140]---> BDD-cost:    1
c ---[ 139]---> BDD-cost:    1
c ---[ 138]---> BDD-cost:    1
c ---[ 137]---> BDD-cost:    1
c ---[ 136]---> BDD-cost:    1
c ---[ 135]---> BDD-cost:    1
c ---[ 134]---> BDD-cost:    1
c ---[ 133]---> BDD-cost:    1
c ---[ 132]---> BDD-cost:    1
c ---[ 131]---> BDD-cost:    1
c ---[ 130]---> BDD-cost:    1
c ---[ 129]---> BDD-cost:    1
c ---[ 128]---> BDD-cost:    1
c ---[ 127]---> BDD-cost:    1
c ---[ 126]---> BDD-cost:    1
c ---[ 125]---> BDD-cost:    1
c ---[ 124]---> BDD-cost:    1
c ---[ 123]---> BDD-cost:    1
c ---[ 122]---> BDD-cost:    1
c ---[ 121]---> BDD-cost:    1
c ---[ 120]---> BDD-cost:    1
c ---[ 119]---> BDD-cost:    1
c ---[ 118]---> BDD-cost:    1
c ---[ 117]---> BDD-cost:    1
c ---[ 116]---> BDD-cost:    1
c ---[ 115]---> BDD-cost:    1
c ---[ 114]---> BDD-cost:    1
c ---[ 113]---> BDD-cost:    1
c ---[ 112]---> BDD-cost:    1
c ---[ 111]---> BDD-cost:    1
c ---[ 110]---> BDD-cost:    1
c ---[ 109]---> BDD-cost:    1
c ---[ 108]---> BDD-cost:    1
c ---[ 107]---> BDD-cost:    1
c ---[ 106]---> BDD-cost:    1
c ---[ 105]---> BDD-cost:    1
c ---[ 104]---> BDD-cost:    1
c ---[ 103]---> BDD-cost:    1
c ---[ 102]---> BDD-cost:    1
c ---[ 101]---> BDD-cost:    1
c ---[ 100]---> BDD-cost:    1
c ---[  99]---> BDD-cost:    1
c ---[  98]---> BDD-cost:    1
c ---[  97]---> BDD-cost:    1
c ---[  96]---> BDD-cost:    1
c ---[  95]---> BDD-cost:    1
c ---[  94]---> BDD-cost:    1
c ---[  93]---> BDD-cost:    1
c ---[  92]---> BDD-cost:    1
c ---[  91]---> BDD-cost:    1
c ---[  90]---> BDD-cost:    1
c ---[  89]---> BDD-cost:    1
c ---[  88]---> BDD-cost:    1
c ---[  87]---> BDD-cost:    1
c ---[  86]---> BDD-cost:    1
c ---[  85]---> BDD-cost:    1
c ---[  84]---> BDD-cost:    1
c ---[  83]---> BDD-cost:    1
c ---[  82]---> BDD-cost:    1
c ---[  81]---> BDD-cost:    1
c ---[  80]---> BDD-cost:    1
c ---[  79]---> BDD-cost:    1
c ---[  78]---> BDD-cost:    1
c ---[  77]---> BDD-cost:    1
c ---[  76]---> BDD-cost:    1
c ---[  75]---> BDD-cost:    1
c ---[  74]---> BDD-cost:    1
c ---[  73]---> BDD-cost:    1
c ---[  72]---> BDD-cost:    1
c ---[  71]---> BDD-cost:    1
c ---[  70]---> BDD-cost:    1
c ---[  69]---> BDD-cost:    1
c ---[  68]---> BDD-cost:    1
c ---[  67]---> BDD-cost:    1
c ---[  66]---> BDD-cost:    1
c ---[  65]---> BDD-cost:    1
c ---[  64]---> BDD-cost:    1
c ---[  63]---> BDD-cost:    1
c ---[  62]---> BDD-cost:    1
c ---[  61]---> BDD-cost:    1
c ---[  60]---> BDD-cost:    1
c ---[  59]---> BDD-cost:    1
c ---[  58]---> BDD-cost:    1
c ---[  57]---> BDD-cost:    1
c ---[  56]---> BDD-cost:    1
c ---[  55]---> BDD-cost:    1
c ---[  54]---> BDD-cost:    1
c ---[  53]---> BDD-cost:    1
c ---[  52]---> BDD-cost:    1
c ---[  51]---> BDD-cost:    1
c ---[  50]---> BDD-cost:    1
c ---[  49]---> BDD-cost:    1
c ---[  48]---> BDD-cost:    1
c ---[  47]---> BDD-cost:    1
c ---[  46]---> BDD-cost:    1
c ---[  45]---> BDD-cost:    1
c ---[  44]---> BDD-cost:    1
c ---[  43]---> BDD-cost:    1
c ---[  42]---> BDD-cost:    1
c ---[  41]---> BDD-cost:    1
c ---[  40]---> BDD-cost:    1
c ---[  39]---> BDD-cost:    1
c ---[  38]---> BDD-cost:    1
c ---[  37]---> BDD-cost:    1
c ---[  36]---> BDD-cost:    1
c ---[  35]---> BDD-cost:    1
c ---[  34]---> BDD-cost:    1
c ---[  33]---> BDD-cost:    1
c ---[  32]---> BDD-cost:    1
c ---[  31]---> BDD-cost:    1
c ---[  30]---> BDD-cost:    1
c ---[  29]---> BDD-cost:    1
c ---[  28]---> BDD-cost:    1
c ---[  27]---> BDD-cost:    1
c ---[  26]---> BDD-cost:    1
c ---[  25]---> BDD-cost:    1
c ---[  24]---> BDD-cost:    1
c ---[  23]---> BDD-cost:    1
c ---[  22]---> BDD-cost:    1
c ---[  21]---> BDD-cost:    1
c ---[  20]---> BDD-cost:    1
c ---[  19]---> BDD-cost:    1
c ---[  18]---> BDD-cost:    1
c ---[  17]---> BDD-cost:    1
c ---[  16]---> BDD-cost:    1
c ---[  15]---> BDD-cost:    1
c ---[  14]---> BDD-cost:    1
c ---[  13]---> BDD-cost:    1
c ---[  12]---> BDD-cost:    1
c ---[  11]---> BDD-cost:    1
c ---[  10]---> BDD-cost:    1
c ---[   9]---> BDD-cost:    1
c ---[   8]---> BDD-cost:    1
c ---[   7]---> BDD-cost:    1
c ---[   6]---> BDD-cost:    1
c ---[   5]---> BDD-cost:    1
c ---[   4]---> BDD-cost:    1
c ---[   3]---> BDD-cost:    1
c ---[   2]---> BDD-cost:    1
c ---[   1]---> BDD-cost:    1
c ---[   0]---> BDD-cost:    1
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |  633343  2209544 |  211114       0        0     nan |  0.000 % |
c |       101 |  633343  2209544 |  232225     101    25727   254.7 |  3.726 % |
c |       251 |  633317  2209456 |  255447     246    26346   107.1 |  3.728 % |
c |       476 |  633317  2209456 |  280992     471    41882    88.9 |  3.728 % |
c |       813 |  633317  2209456 |  309092     808    58307    72.2 |  3.728 % |
c |      1319 |  633309  2209430 |  340001    1313    92254    70.3 |  3.729 % |
c |      2078 |  633300  2209399 |  374001    2069   134137    64.8 |  3.730 % |
c |      3220 |  633300  2209399 |  411401    3211   265417    82.7 |  3.730 % |
c |      4928 |  633275  2209316 |  452541    4915   375378    76.4 |  3.732 % |
c |      7490 |  633214  2209109 |  497795    7463   576859    77.3 |  3.738 % |
c |     11334 |  633137  2208846 |  547575   11281   867591    76.9 |  3.746 % |
c |     17103 |  633110  2208753 |  602332   17035  1834608   107.7 |  3.748 % |
c |     25753 |  633067  2208608 |  662566   25675  3316189   129.2 |  3.752 % |
c |     38727 |  633017  2208438 |  728822   38636  6777196   175.4 |  3.757 % |
c |     58188 |  632974  2208293 |  801705   58086 11786524   202.9 |  3.761 % |
#### 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.91 0.95 0.98 2/54 32745
Raw data (stat): 32745 (runsolver) R 32744 30701 30700 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 491510741 1052672 99 4294967295 134512640 135381576 3221224512 3221219756 135158418 0 2147483391 7 90112 0 0 0 17 0 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0009 s]
Raw data (loadavg): 0.93 0.95 0.98 2/54 32745
Raw data (stat): 32745 (minisat+) R 32744 30701 30700 0 -1 0 13249 0 0 0 970 29 0 0 25 0 1 0 491510741 57552896 12773 4294967295 134512640 134672761 3221224624 3221223808 134558947 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14051 12773 603 41 0 14010 0
vsize: 56204
[startup+20.0021 s]
Raw data (loadavg): 0.94 0.96 0.98 2/54 32745
Raw data (stat): 32745 (minisat+) R 32744 30701 30700 0 -1 0 13304 0 0 0 1969 30 0 0 25 0 1 0 491510741 57823232 12828 4294967295 134512640 134672761 3221224624 3221223824 134557806 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14117 12828 603 41 0 14076 0
vsize: 56468
[startup+30.0022 s]
Raw data (loadavg): 0.95 0.96 0.98 2/54 32745
Raw data (stat): 32745 (minisat+) R 32744 30701 30700 0 -1 0 13367 0 0 0 2969 30 0 0 25 0 1 0 491510741 58093568 12891 4294967295 134512640 134672761 3221224624 3221223792 134560871 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14183 12891 603 41 0 14142 0
vsize: 56732
[startup+40.0029 s]
Raw data (loadavg): 0.95 0.96 0.98 2/54 32745
Raw data (stat): 32745 (minisat+) R 32744 30701 30700 0 -1 0 13452 0 0 0 3969 30 0 0 25 0 1 0 491510741 58363904 12976 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14249 12976 603 41 0 14208 0
vsize: 56996
[startup+50.0041 s]
Raw data (loadavg): 0.96 0.96 0.98 2/54 32745
Raw data (stat): 32745 (minisat+) R 32744 30701 30700 0 -1 0 13511 0 0 0 4968 31 0 0 25 0 1 0 491510741 58634240 13035 4294967295 134512640 134672761 3221224624 3221223792 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14315 13035 603 41 0 14274 0
vsize: 57260
[startup+60.0047 s]
Raw data (loadavg): 0.97 0.96 0.98 2/54 32745
Raw data (stat): 32745 (minisat+) R 32744 30701 30700 0 -1 0 13558 0 0 0 5968 31 0 0 25 0 1 0 491510741 58769408 13082 4294967295 134512640 134672761 3221224624 3221223824 134557809 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14348 13082 603 41 0 14307 0
vsize: 57392
[startup+70.0049 s]
Raw data (loadavg): 0.97 0.96 0.98 2/54 32745
Raw data (stat): 32745 (minisat+) R 32744 30701 30700 0 -1 0 13631 0 0 0 6968 31 0 0 25 0 1 0 491510741 59174912 13155 4294967295 134512640 134672761 3221224624 3221223792 134560892 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14447 13155 603 41 0 14406 0
vsize: 57788
[startup+80.005 s]
Raw data (loadavg): 0.98 0.96 0.98 2/54 32745
Raw data (stat): 32745 (minisat+) R 32744 30701 30700 0 -1 0 13653 0 0 0 7968 31 0 0 25 0 1 0 491510741 59174912 13177 4294967295 134512640 134672761 3221224624 3221223776 134561040 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14447 13177 603 41 0 14406 0
vsize: 57788
[startup+90.0052 s]
Raw data (loadavg): 0.98 0.96 0.98 2/54 32745
Raw data (stat): 32745 (minisat+) R 32744 30701 30700 0 -1 0 13740 0 0 0 8967 32 0 0 25 0 1 0 491510741 59576320 13264 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14545 13264 603 41 0 14504 0
vsize: 58180
[startup+100.005 s]
Raw data (loadavg): 0.98 0.96 0.98 2/54 32745
Raw data (stat): 32745 (minisat+) R 32744 30701 30700 0 -1 0 13848 0 0 0 9967 33 0 0 25 0 1 0 491510741 59977728 13372 4294967295 134512640 134672761 3221224624 3221223728 134559851 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14643 13372 603 41 0 14602 0
vsize: 58572
[startup+110.006 s]
Raw data (loadavg): 0.98 0.96 0.98 2/54 32745
Raw data (stat): 32745 (minisat+) R 32744 30701 30700 0 -1 0 13895 0 0 0 10967 33 0 0 25 0 1 0 491510741 60248064 13419 4294967295 134512640 134672761 3221224624 3221223824 134557911 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14709 13419 603 41 0 14668 0
vsize: 58836
[startup+120.007 s]
Raw data (loadavg): 0.99 0.97 0.98 2/54 32745
Raw data (stat): 32745 (minisat+) R 32744 30701 30700 0 -1 0 13933 0 0 0 11967 33 0 0 25 0 1 0 491510741 60383232 13457 4294967295 134512640 134672761 3221224624 3221223808 134558662 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14742 13457 603 41 0 14701 0
vsize: 58968
[startup+130.006 s]
Raw data (loadavg): 0.99 0.97 0.98 2/54 32745
Raw data (stat): 32745 (minisat+) R 32744 30701 30700 0 -1 0 13968 0 0 0 12967 33 0 0 25 0 1 0 491510741 60518400 13492 4294967295 134512640 134672761 3221224624 3221223824 134557911 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14775 13492 603 41 0 14734 0
vsize: 59100
[startup+140.007 s]
Raw data (loadavg): 0.99 0.97 0.98 2/54 32745
Raw data (stat): 32745 (minisat+) R 32744 30701 30700 0 -1 0 14049 0 0 0 13966 34 0 0 25 0 1 0 491510741 60788736 13573 4294967295 134512640 134672761 3221224624 3221223824 134557885 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14841 13573 603 41 0 14800 0
vsize: 59364
[startup+150.007 s]
Raw data (loadavg): 0.99 0.97 0.98 2/54 32745
Raw data (stat): 32745 (minisat+) R 32744 30701 30700 0 -1 0 14130 0 0 0 14966 34 0 0 25 0 1 0 491510741 61194240 13654 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14940 13654 603 41 0 14899 0
vsize: 59760
[startup+160.008 s]
Raw data (loadavg): 0.99 0.97 0.98 2/54 32745
Raw data (stat): 32745 (minisat+) R 32744 30701 30700 0 -1 0 14197 0 0 0 15965 35 0 0 25 0 1 0 491510741 61464576 13721 4294967295 134512640 134672761 3221224624 3221223760 134560706 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15006 13721 603 41 0 14965 0
vsize: 60024
[startup+170.009 s]
Raw data (loadavg): 0.99 0.97 0.98 2/54 32745
Raw data (stat): 32745 (minisat+) R 32744 30701 30700 0 -1 0 14295 0 0 0 16965 35 0 0 25 0 1 0 491510741 61870080 13819 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15105 13819 603 41 0 15064 0
vsize: 60420
[startup+180.009 s]
Raw data (loadavg): 0.99 0.97 0.98 2/54 32745
Raw data (stat): 32745 (minisat+) R 32744 30701 30700 0 -1 0 14382 0 0 0 17964 36 0 0 25 0 1 0 491510741 62140416 13906 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15171 13906 603 41 0 15130 0
vsize: 60684
[startup+190.009 s]
Raw data (loadavg): 0.99 0.97 0.98 2/54 32745
Raw data (stat): 32745 (minisat+) R 32744 30701 30700 0 -1 0 14489 0 0 0 18964 36 0 0 25 0 1 0 491510741 62681088 14013 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15303 14013 603 41 0 15262 0
vsize: 61212
[startup+200.01 s]
Raw data (loadavg): 0.99 0.97 0.98 2/54 32745
Raw data (stat): 32745 (minisat+) R 32744 30701 30700 0 -1 0 14630 0 0 0 19964 37 0 0 25 0 1 0 491510741 63213568 14154 4294967295 134512640 134672761 3221224624 3221223792 134560926 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15433 14154 603 41 0 15392 0
vsize: 61732
[startup+210.01 s]
Raw data (loadavg): 0.99 0.97 0.98 2/54 32745
Raw data (stat): 32745 (minisat+) R 32744 30701 30700 0 -1 0 14747 0 0 0 20963 38 0 0 25 0 1 0 491510741 63754240 14271 4294967295 134512640 134672761 3221224624 3221223792 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15565 14271 603 41 0 15524 0
vsize: 62260
[startup+220.01 s]
Raw data (loadavg): 0.99 0.97 0.98 2/54 32745
Raw data (stat): 32745 (minisat+) R 32744 30701 30700 0 -1 0 14808 0 0 0 21963 38 0 0 25 0 1 0 491510741 63889408 14332 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15598 14332 603 41 0 15557 0
vsize: 62392
[startup+230.01 s]
Raw data (loadavg): 0.99 0.97 0.98 2/54 32745
Raw data (stat): 32745 (minisat+) R 32744 30701 30700 0 -1 0 14939 0 0 0 22962 39 0 0 25 0 1 0 491510741 64430080 14463 4294967295 134512640 134672761 3221224624 3221223824 134557849 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15730 14463 603 41 0 15689 0
vsize: 62920
[startup+240.011 s]
Raw data (loadavg): 0.99 0.97 0.98 2/54 32745
Raw data (stat): 32745 (minisat+) R 32744 30701 30700 0 -1 0 15070 0 0 0 23962 39 0 0 25 0 1 0 491510741 64970752 14594 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15862 14594 603 41 0 15821 0
vsize: 63448
[startup+250.011 s]
Raw data (loadavg): 0.99 0.97 0.98 2/54 32745
Raw data (stat): 32745 (minisat+) R 32744 30701 30700 0 -1 0 15219 0 0 0 24961 41 0 0 25 0 1 0 491510741 65675264 14743 4294967295 134512640 134672761 3221224624 3221223792 134560920 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16034 14743 603 41 0 15993 0
vsize: 64136
[startup+260.012 s]
Raw data (loadavg): 0.99 0.97 0.98 2/54 32745
Raw data (stat): 32745 (minisat+) R 32744 30701 30700 0 -1 0 15291 0 0 0 25961 41 0 0 25 0 1 0 491510741 65945600 14815 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16100 14815 603 41 0 16059 0
vsize: 64400
[startup+270.012 s]
Raw data (loadavg): 0.99 0.97 0.98 2/54 32745
Raw data (stat): 32745 (minisat+) R 32744 30701 30700 0 -1 0 15394 0 0 0 26960 42 0 0 25 0 1 0 491510741 66351104 14918 4294967295 134512640 134672761 3221224624 3221223792 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16199 14918 603 41 0 16158 0
vsize: 64796
[startup+280.012 s]
Raw data (loadavg): 0.99 0.97 0.98 2/54 32745
Raw data (stat): 32745 (minisat+) R 32744 30701 30700 0 -1 0 15456 0 0 0 27960 42 0 0 25 0 1 0 491510741 66621440 14980 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16265 14980 603 41 0 16224 0
vsize: 65060
[startup+290.013 s]
Raw data (loadavg): 0.99 0.97 0.98 2/54 32745
Raw data (stat): 32745 (minisat+) R 32744 30701 30700 0 -1 0 15600 0 0 0 28959 43 0 0 25 0 1 0 491510741 67297280 15124 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16430 15124 603 41 0 16389 0
vsize: 65720
[startup+300.014 s]
Raw data (loadavg): 0.99 0.97 0.98 2/54 32745
Raw data (stat): 32745 (minisat+) R 32744 30701 30700 0 -1 0 15676 0 0 0 29959 43 0 0 25 0 1 0 491510741 67563520 15200 4294967295 134512640 134672761 3221224624 3221223792 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16495 15200 603 41 0 16454 0
vsize: 65980
[startup+310.014 s]
Raw data (loadavg): 0.99 0.97 0.98 2/54 32745
Raw data (stat): 32745 (minisat+) R 32744 30701 30700 0 -1 0 15751 0 0 0 30959 44 0 0 25 0 1 0 491510741 67833856 15275 4294967295 134512640 134672761 3221224624 3221223792 134560852 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16561 15275 603 41 0 16520 0
vsize: 66244
[startup+320.015 s]
Raw data (loadavg): 0.99 0.97 0.98 2/54 32745
Raw data (stat): 32745 (minisat+) R 32744 30701 30700 0 -1 0 15826 0 0 0 31959 44 0 0 25 0 1 0 491510741 68104192 15350 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16627 15350 603 41 0 16586 0
vsize: 66508
[startup+330.014 s]
Raw data (loadavg): 0.99 0.97 0.98 2/54 32745
Raw data (stat): 32745 (minisat+) R 32744 30701 30700 0 -1 0 15905 0 0 0 32959 44 0 0 25 0 1 0 491510741 68509696 15429 4294967295 134512640 134672761 3221224624 3221223792 134560845 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16726 15429 603 41 0 16685 0
vsize: 66904
[startup+340.014 s]
Raw data (loadavg): 0.99 0.97 0.98 2/54 32745
Raw data (stat): 32745 (minisat+) R 32744 30701 30700 0 -1 0 16105 0 0 0 33958 45 0 0 25 0 1 0 491510741 69320704 15629 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16924 15629 603 41 0 16883 0
vsize: 67696
[startup+350.014 s]
Raw data (loadavg): 0.99 0.97 0.98 2/54 32745
Raw data (stat): 32745 (minisat+) R 32744 30701 30700 0 -1 0 16325 0 0 0 34958 45 0 0 25 0 1 0 491510741 70127616 15849 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17121 15849 603 41 0 17080 0
vsize: 68484
[startup+360.014 s]
Raw data (loadavg): 0.99 0.97 0.98 2/54 32745
Raw data (stat): 32745 (minisat+) R 32744 30701 30700 0 -1 0 16421 0 0 0 35958 46 0 0 25 0 1 0 491510741 70533120 15945 4294967295 134512640 134672761 3221224624 3221223728 134560031 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17220 15945 603 41 0 17179 0
vsize: 68880
[startup+370.014 s]
Raw data (loadavg): 0.99 0.97 0.98 2/54 32745
Raw data (stat): 32745 (minisat+) R 32744 30701 30700 0 -1 0 16563 0 0 0 36957 46 0 0 25 0 1 0 491510741 71208960 16087 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17385 16087 603 41 0 17344 0
vsize: 69540
[startup+380.014 s]
Raw data (loadavg): 0.99 0.97 0.98 2/54 32745
Raw data (stat): 32745 (minisat+) R 32744 30701 30700 0 -1 0 16792 0 0 0 37957 47 0 0 25 0 1 0 491510741 72146944 16316 4294967295 134512640 134672761 3221224624 3221223796 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17614 16316 603 41 0 17573 0
vsize: 70456
[startup+390.015 s]
Raw data (loadavg): 0.99 0.97 0.98 2/54 32745
Raw data (stat): 32745 (minisat+) R 32744 30701 30700 0 -1 0 16890 0 0 0 38956 47 0 0 25 0 1 0 491510741 72552448 16414 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17713 16414 603 41 0 17672 0
vsize: 70852
[startup+400.014 s]
Raw data (loadavg): 0.99 0.97 0.98 2/54 32745
Raw data (stat): 32745 (minisat+) R 32744 30701 30700 0 -1 0 17126 0 0 0 39956 48 0 0 25 0 1 0 491510741 73494528 16650 4294967295 134512640 134672761 3221224624 3221223792 134561382 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17943 16650 603 41 0 17902 0
vsize: 71772
[startup+410.015 s]
Raw data (loadavg): 0.99 0.97 0.98 2/54 32745
Raw data (stat): 32745 (minisat+) R 32744 30701 30700 0 -1 0 17414 0 0 0 40955 49 0 0 25 0 1 0 491510741 74571776 16938 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18206 16938 603 41 0 18165 0
vsize: 72824
[startup+420.015 s]
Raw data (loadavg): 0.99 0.97 0.98 2/54 32745
Raw data (stat): 32745 (minisat+) R 32744 30701 30700 0 -1 0 17679 0 0 0 41955 49 0 0 25 0 1 0 491510741 75653120 17203 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18470 17203 603 41 0 18429 0
vsize: 73880
[startup+430.014 s]
Raw data (loadavg): 0.99 0.97 0.98 2/54 32745
Raw data (stat): 32745 (minisat+) R 32744 30701 30700 0 -1 0 17975 0 0 0 42954 50 0 0 25 0 1 0 491510741 76869632 17499 4294967295 134512640 134672761 3221224624 3221223792 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18767 17499 603 41 0 18726 0
vsize: 75068
[startup+440.014 s]
Raw data (loadavg): 0.99 0.97 0.98 2/54 32745
Raw data (stat): 32745 (minisat+) R 32744 30701 30700 0 -1 0 18274 0 0 0 43953 51 0 0 25 0 1 0 491510741 78213120 17798 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19095 17798 603 41 0 19054 0
vsize: 76380
[startup+450.014 s]
Raw data (loadavg): 0.99 0.97 0.98 2/54 32745
Raw data (stat): 32745 (minisat+) R 32744 30701 30700 0 -1 0 18606 0 0 0 44953 52 0 0 25 0 1 0 491510741 79564800 18130 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19425 18130 603 41 0 19384 0
vsize: 77700
[startup+460.014 s]
Raw data (loadavg): 0.99 0.97 0.98 2/54 32745
Raw data (stat): 32745 (minisat+) R 32744 30701 30700 0 -1 0 18951 0 0 0 45951 53 0 0 25 0 1 0 491510741 80908288 18475 4294967295 134512640 134672761 3221224624 3221223748 134566018 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19753 18475 603 41 0 19712 0
vsize: 79012
[startup+470.014 s]
Raw data (loadavg): 0.99 0.97 0.98 2/54 32745
Raw data (stat): 32745 (minisat+) R 32744 30701 30700 0 -1 0 19086 0 0 0 46951 54 0 0 25 0 1 0 491510741 81457152 18610 4294967295 134512640 134672761 3221224624 3221223792 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19887 18610 603 41 0 19846 0
vsize: 79548
[startup+480.014 s]
Raw data (loadavg): 0.99 0.97 0.98 2/54 32745
Raw data (stat): 32745 (minisat+) R 32744 30701 30700 0 -1 0 19168 0 0 0 47951 54 0 0 25 0 1 0 491510741 81989632 18692 4294967295 134512640 134672761 3221224624 3221223824 134557830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20017 18692 603 41 0 19976 0
vsize: 80068
[startup+490.014 s]
Raw data (loadavg): 0.99 0.97 0.98 2/54 32745
Raw data (stat): 32745 (minisat+) R 32744 30701 30700 0 -1 0 19261 0 0 0 48951 54 0 0 25 0 1 0 491510741 82255872 18785 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20082 18785 603 41 0 20041 0
vsize: 80328
[startup+500.015 s]
Raw data (loadavg): 0.99 0.97 0.98 2/54 32745
Raw data (stat): 32745 (minisat+) R 32744 30701 30700 0 -1 0 19355 0 0 0 49951 54 0 0 25 0 1 0 491510741 82657280 18879 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20180 18879 603 41 0 20139 0
vsize: 80720
[startup+510.016 s]
Raw data (loadavg): 0.99 0.97 0.98 2/54 32745
Raw data (stat): 32745 (minisat+) R 32744 30701 30700 0 -1 0 19479 0 0 0 50951 55 0 0 25 0 1 0 491510741 83189760 19003 4294967295 134512640 134672761 3221224624 3221223824 134557887 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20310 19003 603 41 0 20269 0
vsize: 81240
[startup+520.015 s]
Raw data (loadavg): 0.99 0.97 0.98 2/54 32745
Raw data (stat): 32745 (minisat+) R 32744 30701 30700 0 -1 0 19598 0 0 0 51951 55 0 0 25 0 1 0 491510741 83726336 19122 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20441 19122 603 41 0 20400 0
vsize: 81764
[startup+530.015 s]
Raw data (loadavg): 0.99 0.97 0.98 2/54 32745
Raw data (stat): 32745 (minisat+) R 32744 30701 30700 0 -1 0 19728 0 0 0 52951 56 0 0 25 0 1 0 491510741 84267008 19252 4294967295 134512640 134672761 3221224624 3221223792 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20573 19252 603 41 0 20532 0
vsize: 82292
[startup+540.016 s]
Raw data (loadavg): 0.99 0.97 0.98 2/54 32745
Raw data (stat): 32745 (minisat+) R 32744 30701 30700 0 -1 0 19842 0 0 0 53950 56 0 0 25 0 1 0 491510741 84672512 19366 4294967295 134512640 134672761 3221224624 3221223760 134560677 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20672 19366 603 41 0 20631 0
vsize: 82688
[startup+550.015 s]
Raw data (loadavg): 0.99 0.97 0.98 2/54 32745
Raw data (stat): 32745 (minisat+) R 32744 30701 30700 0 -1 0 19932 0 0 0 54950 56 0 0 25 0 1 0 491510741 85078016 19456 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20771 19456 603 41 0 20730 0
vsize: 83084
[startup+560.016 s]
Raw data (loadavg): 0.99 0.97 0.98 2/54 32745
Raw data (stat): 32745 (minisat+) R 32744 30701 30700 0 -1 0 20016 0 0 0 55950 56 0 0 25 0 1 0 491510741 85344256 19540 4294967295 134512640 134672761 3221224624 3221223824 134557911 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20836 19540 603 41 0 20795 0
vsize: 83344
[startup+570.017 s]
Raw data (loadavg): 0.99 0.97 0.98 2/54 32745
Raw data (stat): 32745 (minisat+) R 32744 30701 30700 0 -1 0 20089 0 0 0 56950 57 0 0 25 0 1 0 491510741 85749760 19613 4294967295 134512640 134672761 3221224624 3221223792 134560852 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20935 19613 603 41 0 20894 0
vsize: 83740
[startup+580.016 s]
Raw data (loadavg): 0.99 0.97 0.98 2/54 32745
Raw data (stat): 32745 (minisat+) R 32744 30701 30700 0 -1 0 20177 0 0 0 57950 57 0 0 25 0 1 0 491510741 86020096 19701 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21001 19701 603 41 0 20960 0
vsize: 84004
[startup+590.016 s]
Raw data (loadavg): 0.99 0.97 0.98 2/54 32745
Raw data (stat): 32745 (minisat+) R 32744 30701 30700 0 -1 0 20265 0 0 0 58950 57 0 0 25 0 1 0 491510741 86425600 19789 4294967295 134512640 134672761 3221224624 3221223760 134560677 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21100 19789 603 41 0 21059 0
vsize: 84400
[startup+600.017 s]
Raw data (loadavg): 0.99 0.97 0.98 2/54 32745
Raw data (stat): 32745 (minisat+) R 32744 30701 30700 0 -1 0 20351 0 0 0 59950 57 0 0 25 0 1 0 491510741 86695936 19875 4294967295 134512640 134672761 3221224624 3221223808 134558771 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21166 19875 603 41 0 21125 0
vsize: 84664
[startup+610.017 s]
Raw data (loadavg): 0.99 0.97 0.98 2/54 32745
Raw data (stat): 32745 (minisat+) R 32744 30701 30700 0 -1 0 20429 0 0 0 60950 58 0 0 25 0 1 0 491510741 87101440 19953 4294967295 134512640 134672761 3221224624 3221223792 134561382 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21265 19953 603 41 0 21224 0
vsize: 85060
[startup+620.018 s]
Raw data (loadavg): 0.99 0.97 0.98 2/54 32745
Raw data (stat): 32745 (minisat+) R 32744 30701 30700 0 -1 0 20606 0 0 0 61949 58 0 0 25 0 1 0 491510741 87769088 20130 4294967295 134512640 134672761 3221224624 3221223824 134557830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21428 20130 603 41 0 21387 0
vsize: 85712
[startup+630.017 s]
Raw data (loadavg): 1.15 1.00 0.99 2/54 32745
Raw data (stat): 32745 (minisat+) R 32744 30701 30700 0 -1 0 20719 0 0 0 62948 59 0 0 25 0 1 0 491510741 88309760 20243 4294967295 134512640 134672761 3221224624 3221223824 134557911 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21560 20243 603 41 0 21519 0
vsize: 86240
[startup+640.017 s]
Raw data (loadavg): 1.12 1.00 0.99 2/54 32745
Raw data (stat): 32745 (minisat+) R 32744 30701 30700 0 -1 0 20855 0 0 0 63948 59 0 0 25 0 1 0 491510741 88846336 20379 4294967295 134512640 134672761 3221224624 3221223792 134561391 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21691 20379 603 41 0 21650 0
vsize: 86764
[startup+650.017 s]
Raw data (loadavg): 1.10 1.00 0.99 2/54 32745
Raw data (stat): 32745 (minisat+) R 32744 30701 30700 0 -1 0 21012 0 0 0 64947 60 0 0 25 0 1 0 491510741 89382912 20536 4294967295 134512640 134672761 3221224624 3221223792 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21822 20536 603 41 0 21781 0
vsize: 87288
[startup+660.018 s]
Raw data (loadavg): 1.09 1.00 0.99 2/54 32745
Raw data (stat): 32745 (minisat+) R 32744 30701 30700 0 -1 0 21127 0 0 0 65948 60 0 0 25 0 1 0 491510741 89923584 20651 4294967295 134512640 134672761 3221224624 3221223824 134557895 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21954 20651 603 41 0 21913 0
vsize: 87816
[startup+670.018 s]
Raw data (loadavg): 1.07 1.00 0.99 2/54 32745
Raw data (stat): 32745 (minisat+) R 32744 30701 30700 0 -1 0 21260 0 0 0 66948 60 0 0 25 0 1 0 491510741 90456064 20784 4294967295 134512640 134672761 3221224624 3221223792 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22084 20784 603 41 0 22043 0
vsize: 88336
[startup+680.018 s]
Raw data (loadavg): 1.06 1.00 0.99 2/54 32745
Raw data (stat): 32745 (minisat+) R 32744 30701 30700 0 -1 0 21383 0 0 0 67947 60 0 0 25 0 1 0 491510741 90996736 20907 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22216 20907 603 41 0 22175 0
vsize: 88864
[startup+690.019 s]
Raw data (loadavg): 1.05 1.00 0.99 2/54 32745
Raw data (stat): 32745 (minisat+) R 32744 30701 30700 0 -1 0 21525 0 0 0 68948 60 0 0 25 0 1 0 491510741 91537408 21049 4294967295 134512640 134672761 3221224624 3221223776 134561040 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22348 21049 603 41 0 22307 0
vsize: 89392
[startup+700.018 s]
Raw data (loadavg): 1.04 1.00 0.99 2/54 32745
Raw data (stat): 32745 (minisat+) R 32744 30701 30700 0 -1 0 21670 0 0 0 69947 61 0 0 25 0 1 0 491510741 92196864 21194 4294967295 134512640 134672761 3221224624 3221223824 134557836 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22509 21194 603 41 0 22468 0
vsize: 90036
[startup+710.019 s]
Raw data (loadavg): 1.04 1.00 0.99 2/54 32745
Raw data (stat): 32745 (minisat+) R 32744 30701 30700 0 -1 0 21816 0 0 0 70947 62 0 0 25 0 1 0 491510741 92741632 21340 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22642 21340 603 41 0 22601 0
vsize: 90568
[startup+720.02 s]
Raw data (loadavg): 1.03 1.00 0.99 2/54 32745
Raw data (stat): 32745 (minisat+) R 32744 30701 30700 0 -1 0 21979 0 0 0 71947 62 0 0 25 0 1 0 491510741 93417472 21503 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22807 21503 603 41 0 22766 0
vsize: 91228
[startup+730.019 s]
Raw data (loadavg): 1.03 1.00 0.99 2/54 32745
Raw data (stat): 32745 (minisat+) R 32744 30701 30700 0 -1 0 22134 0 0 0 72947 62 0 0 25 0 1 0 491510741 94093312 21658 4294967295 134512640 134672761 3221224624 3221223760 134560661 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22972 21658 603 41 0 22931 0
vsize: 91888
[startup+740.02 s]
Raw data (loadavg): 1.02 1.00 0.99 2/54 32745
Raw data (stat): 32745 (minisat+) R 32744 30701 30700 0 -1 0 22227 0 0 0 73947 62 0 0 25 0 1 0 491510741 94359552 21751 4294967295 134512640 134672761 3221224624 3221223824 134557828 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23037 21751 603 41 0 22996 0
vsize: 92148
[startup+750.02 s]
Raw data (loadavg): 1.02 1.00 0.99 2/54 32745
Raw data (stat): 32745 (minisat+) R 32744 30701 30700 0 -1 0 22330 0 0 0 74947 63 0 0 25 0 1 0 491510741 94896128 21854 4294967295 134512640 134672761 3221224624 3221223824 134557842 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23168 21854 603 41 0 23127 0
vsize: 92672
[startup+760.02 s]
Raw data (loadavg): 1.01 1.00 0.99 2/54 32745
Raw data (stat): 32745 (minisat+) R 32744 30701 30700 0 -1 0 22444 0 0 0 75946 63 0 0 25 0 1 0 491510741 95301632 21968 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23267 21968 603 41 0 23226 0
vsize: 93068
[startup+770.02 s]
Raw data (loadavg): 1.01 1.00 0.99 2/54 32745
Raw data (stat): 32745 (minisat+) R 32744 30701 30700 0 -1 0 22566 0 0 0 76946 64 0 0 25 0 1 0 491510741 95838208 22090 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23398 22090 603 41 0 23357 0
vsize: 93592
[startup+780.021 s]
Raw data (loadavg): 1.01 1.00 0.99 2/54 32745
Raw data (stat): 32745 (minisat+) R 32744 30701 30700 0 -1 0 22692 0 0 0 77946 64 0 0 25 0 1 0 491510741 96243712 22216 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23497 22216 603 41 0 23456 0
vsize: 93988
[startup+790.021 s]
Raw data (loadavg): 1.01 1.00 0.99 2/54 32745
Raw data (stat): 32745 (minisat+) R 32744 30701 30700 0 -1 0 22823 0 0 0 78946 65 0 0 25 0 1 0 491510741 96784384 22347 4294967295 134512640 134672761 3221224624 3221223792 134560976 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23629 22347 603 41 0 23588 0
vsize: 94516
[startup+800.021 s]
Raw data (loadavg): 1.01 1.00 0.99 2/54 32745
Raw data (stat): 32745 (minisat+) R 32744 30701 30700 0 -1 0 22931 0 0 0 79945 65 0 0 25 0 1 0 491510741 97320960 22455 4294967295 134512640 134672761 3221224624 3221223760 134560677 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23760 22455 603 41 0 23719 0
vsize: 95040
[startup+810.022 s]
Raw data (loadavg): 1.00 1.00 0.99 2/54 32745
Raw data (stat): 32745 (minisat+) R 32744 30701 30700 0 -1 0 23042 0 0 0 80945 65 0 0 25 0 1 0 491510741 97722368 22566 4294967295 134512640 134672761 3221224624 3221223824 134557836 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23858 22566 603 41 0 23817 0
vsize: 95432
[startup+820.021 s]
Raw data (loadavg): 1.00 1.00 0.99 2/54 32745
Raw data (stat): 32745 (minisat+) R 32744 30701 30700 0 -1 0 23144 0 0 0 81945 66 0 0 25 0 1 0 491510741 98123776 22668 4294967295 134512640 134672761 3221224624 3221223760 134560577 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23956 22668 603 41 0 23915 0
vsize: 95824
[startup+830.021 s]
Raw data (loadavg): 1.00 1.00 0.99 2/54 32745
Raw data (stat): 32745 (minisat+) R 32744 30701 30700 0 -1 0 23255 0 0 0 82945 66 0 0 25 0 1 0 491510741 98660352 22779 4294967295 134512640 134672761 3221224624 3221223792 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24087 22779 603 41 0 24046 0
vsize: 96348
[startup+840.022 s]
Raw data (loadavg): 1.00 1.00 0.99 2/54 32745
Raw data (stat): 32745 (minisat+) R 32744 30701 30700 0 -1 0 23358 0 0 0 83945 66 0 0 25 0 1 0 491510741 99065856 22882 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24186 22882 603 41 0 24145 0
vsize: 96744
[startup+850.022 s]
Raw data (loadavg): 1.00 1.00 0.99 2/54 32745
Raw data (stat): 32745 (minisat+) R 32744 30701 30700 0 -1 0 23483 0 0 0 84945 67 0 0 25 0 1 0 491510741 99602432 23007 4294967295 134512640 134672761 3221224624 3221223792 134561001 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24317 23007 603 41 0 24276 0
vsize: 97268
[startup+860.022 s]
Raw data (loadavg): 1.00 1.00 0.99 2/54 32745
Raw data (stat): 32745 (minisat+) R 32744 30701 30700 0 -1 0 23600 0 0 0 85944 67 0 0 25 0 1 0 491510741 100003840 23124 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24415 23124 603 41 0 24374 0
vsize: 97660
[startup+870.023 s]
Raw data (loadavg): 1.00 1.00 0.99 2/54 32745
Raw data (stat): 32745 (minisat+) R 32744 30701 30700 0 -1 0 23716 0 0 0 86945 67 0 0 25 0 1 0 491510741 100540416 23240 4294967295 134512640 134672761 3221224624 3221223760 134560590 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24546 23240 603 41 0 24505 0
vsize: 98184
[startup+880.022 s]
Raw data (loadavg): 1.00 1.00 0.99 2/54 32745
Raw data (stat): 32745 (minisat+) R 32744 30701 30700 0 -1 0 23833 0 0 0 87945 67 0 0 25 0 1 0 491510741 100945920 23357 4294967295 134512640 134672761 3221224624 3221223808 134558662 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24645 23357 603 41 0 24604 0
vsize: 98580
[startup+890.022 s]
Raw data (loadavg): 1.00 1.00 0.99 2/54 32745
Raw data (stat): 32745 (minisat+) R 32744 30701 30700 0 -1 0 23971 0 0 0 88944 68 0 0 25 0 1 0 491510741 101486592 23495 4294967295 134512640 134672761 3221224624 3221223728 134560235 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24777 23495 603 41 0 24736 0
vsize: 99108
[startup+900.022 s]
Raw data (loadavg): 1.00 1.00 0.99 2/54 32745
Raw data (stat): 32745 (minisat+) R 32744 30701 30700 0 -1 0 24127 0 0 0 89944 68 0 0 25 0 1 0 491510741 102162432 23651 4294967295 134512640 134672761 3221224624 3221223792 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24942 23651 603 41 0 24901 0
vsize: 99768
[startup+910.021 s]
Raw data (loadavg): 1.00 1.00 0.99 2/54 32745
Raw data (stat): 32745 (minisat+) R 32744 30701 30700 0 -1 0 24249 0 0 0 90944 69 0 0 25 0 1 0 491510741 102703104 23773 4294967295 134512640 134672761 3221224624 3221223792 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25074 23773 603 41 0 25033 0
vsize: 100296
[startup+920.022 s]
Raw data (loadavg): 1.00 1.00 0.99 2/54 32745
Raw data (stat): 32745 (minisat+) R 32744 30701 30700 0 -1 0 24383 0 0 0 91944 69 0 0 25 0 1 0 491510741 103239680 23907 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25205 23907 603 41 0 25164 0
vsize: 100820
[startup+930.021 s]
Raw data (loadavg): 1.07 1.02 1.00 2/54 32745
Raw data (stat): 32745 (minisat+) R 32744 30701 30700 0 -1 0 24560 0 0 0 92943 69 0 0 25 0 1 0 491510741 103915520 24084 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25370 24084 603 41 0 25329 0
vsize: 101480
[startup+940.021 s]
Raw data (loadavg): 1.06 1.02 1.00 2/54 32745
Raw data (stat): 32745 (minisat+) R 32744 30701 30700 0 -1 0 24706 0 0 0 93943 70 0 0 25 0 1 0 491510741 104583168 24230 4294967295 134512640 134672761 3221224624 3221223792 134560882 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25533 24230 603 41 0 25492 0
vsize: 102132
[startup+950.021 s]
Raw data (loadavg): 1.05 1.01 1.00 2/54 32745
Raw data (stat): 32745 (minisat+) R 32744 30701 30700 0 -1 0 24842 0 0 0 94943 70 0 0 25 0 1 0 491510741 105123840 24366 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25665 24366 603 41 0 25624 0
vsize: 102660
[startup+960.021 s]
Raw data (loadavg): 1.04 1.01 1.00 2/54 32745
Raw data (stat): 32745 (minisat+) R 32744 30701 30700 0 -1 0 24985 0 0 0 95942 71 0 0 25 0 1 0 491510741 105660416 24509 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25796 24509 603 41 0 25755 0
vsize: 103184
[startup+970.021 s]
Raw data (loadavg): 1.04 1.01 1.00 2/54 32745
Raw data (stat): 32745 (minisat+) R 32744 30701 30700 0 -1 0 25118 0 0 0 96942 71 0 0 25 0 1 0 491510741 106201088 24642 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25928 24642 603 41 0 25887 0
vsize: 103712
[startup+980.021 s]
Raw data (loadavg): 1.03 1.01 1.00 2/54 32745
Raw data (stat): 32745 (minisat+) R 32744 30701 30700 0 -1 0 25259 0 0 0 97942 72 0 0 25 0 1 0 491510741 106737664 24783 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26059 24783 603 41 0 26018 0
vsize: 104236
[startup+990.021 s]
Raw data (loadavg): 1.02 1.01 1.00 2/54 32745
Raw data (stat): 32745 (minisat+) R 32744 30701 30700 0 -1 0 25397 0 0 0 98942 72 0 0 25 0 1 0 491510741 107413504 24921 4294967295 134512640 134672761 3221224624 3221223792 134560839 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26224 24921 603 41 0 26183 0
vsize: 104896
[startup+1000.02 s]
Raw data (loadavg): 1.02 1.01 1.00 2/54 32745
Raw data (stat): 32745 (minisat+) R 32744 30701 30700 0 -1 0 25539 0 0 0 99942 72 0 0 25 0 1 0 491510741 107941888 25063 4294967295 134512640 134672761 3221224624 3221223808 134559354 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26353 25063 603 41 0 26312 0
vsize: 105412
[startup+1010.02 s]
Raw data (loadavg): 1.02 1.01 1.00 2/54 32745
Raw data (stat): 32745 (minisat+) R 32744 30701 30700 0 -1 0 25684 0 0 0 100941 72 0 0 25 0 1 0 491510741 108482560 25208 4294967295 134512640 134672761 3221224624 3221223824 134557842 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26485 25208 603 41 0 26444 0
vsize: 105940
[startup+1020.02 s]
Raw data (loadavg): 1.01 1.01 1.00 2/54 32745
Raw data (stat): 32745 (minisat+) R 32744 30701 30700 0 -1 0 25838 0 0 0 101940 73 0 0 25 0 1 0 491510741 109158400 25362 4294967295 134512640 134672761 3221224624 3221223792 134561375 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26650 25362 603 41 0 26609 0
vsize: 106600
[startup+1030.02 s]
Raw data (loadavg): 1.01 1.01 1.00 2/54 32745
Raw data (stat): 32745 (minisat+) R 32744 30701 30700 0 -1 0 26048 0 0 0 102940 74 0 0 25 0 1 0 491510741 109969408 25572 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26848 25572 603 41 0 26807 0
vsize: 107392
[startup+1040.02 s]
Raw data (loadavg): 1.01 1.01 1.00 2/54 32745
Raw data (stat): 32745 (minisat+) R 32744 30701 30700 0 -1 0 26198 0 0 0 103939 74 0 0 25 0 1 0 491510741 110645248 25722 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27013 25722 603 41 0 26972 0
vsize: 108052
[startup+1050.02 s]
Raw data (loadavg): 1.01 1.00 1.00 2/54 32745
Raw data (stat): 32745 (minisat+) R 32744 30701 30700 0 -1 0 26361 0 0 0 104939 75 0 0 25 0 1 0 491510741 111321088 25885 4294967295 134512640 134672761 3221224624 3221223728 134559872 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27178 25885 603 41 0 27137 0
vsize: 108712
[startup+1060.02 s]
Raw data (loadavg): 1.01 1.00 1.00 2/54 32745
Raw data (stat): 32745 (minisat+) R 32744 30701 30700 0 -1 0 26549 0 0 0 105939 75 0 0 25 0 1 0 491510741 112132096 26073 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27376 26073 603 41 0 27335 0
vsize: 109504
[startup+1070.02 s]
Raw data (loadavg): 1.00 1.00 1.00 2/54 32745
Raw data (stat): 32745 (minisat+) R 32744 30701 30700 0 -1 0 26821 0 0 0 106938 76 0 0 25 0 1 0 491510741 113213440 26345 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27640 26345 603 41 0 27599 0
vsize: 110560
[startup+1080.02 s]
Raw data (loadavg): 1.00 1.00 1.00 2/54 32745
Raw data (stat): 32745 (minisat+) R 32744 30701 30700 0 -1 0 27048 0 0 0 107938 77 0 0 25 0 1 0 491510741 114159616 26572 4294967295 134512640 134672761 3221224624 3221223760 134560677 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27871 26572 603 41 0 27830 0
vsize: 111484
[startup+1090.02 s]
Raw data (loadavg): 1.00 1.00 1.00 2/54 32745
Raw data (stat): 32745 (minisat+) R 32744 30701 30700 0 -1 0 27259 0 0 0 108937 77 0 0 25 0 1 0 491510741 114966528 26783 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28068 26783 603 41 0 28027 0
vsize: 112272
[startup+1100.02 s]
Raw data (loadavg): 1.00 1.00 1.00 2/54 32745
Raw data (stat): 32745 (minisat+) R 32744 30701 30700 0 -1 0 27454 0 0 0 109937 78 0 0 25 0 1 0 491510741 115777536 26978 4294967295 134512640 134672761 3221224624 3221223792 134560920 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28266 26978 603 41 0 28225 0
vsize: 113064
[startup+1110.02 s]
Raw data (loadavg): 1.00 1.00 1.00 2/54 32745
Raw data (stat): 32745 (minisat+) R 32744 30701 30700 0 -1 0 27608 0 0 0 110937 79 0 0 25 0 1 0 491510741 116457472 27132 4294967295 134512640 134672761 3221224624 3221223792 134561005 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28432 27132 603 41 0 28391 0
vsize: 113728
[startup+1120.03 s]
Raw data (loadavg): 1.00 1.00 1.00 2/54 32745
Raw data (stat): 32745 (minisat+) R 32744 30701 30700 0 -1 0 27798 0 0 0 111937 80 0 0 25 0 1 0 491510741 117129216 27322 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28596 27322 603 41 0 28555 0
vsize: 114384
[startup+1130.05 s]
Raw data (loadavg): 1.00 1.00 1.00 2/54 32745
Raw data (stat): 32745 (minisat+) R 32744 30701 30700 0 -1 0 28001 0 0 0 112938 80 0 0 25 0 1 0 491510741 118063104 27525 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28824 27525 603 41 0 28783 0
vsize: 115296
[startup+1140.05 s]
Raw data (loadavg): 1.00 1.00 1.00 2/54 32745
Raw data (stat): 32745 (minisat+) R 32744 30701 30700 0 -1 0 28175 0 0 0 113937 81 0 0 25 0 1 0 491510741 118996992 27699 4294967295 134512640 134672761 3221224624 3221223840 134561997 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29052 27699 603 41 0 29011 0
vsize: 116208
[startup+1150.05 s]
Raw data (loadavg): 1.00 1.00 1.00 2/54 32745
Raw data (stat): 32745 (minisat+) R 32744 30701 30700 0 -1 0 28278 0 0 0 114937 81 0 0 25 0 1 0 491510741 119398400 27802 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29150 27802 603 41 0 29109 0
vsize: 116600
[startup+1160.05 s]
Raw data (loadavg): 1.00 1.00 1.00 2/54 32745
Raw data (stat): 32745 (minisat+) R 32744 30701 30700 0 -1 0 28392 0 0 0 115937 81 0 0 25 0 1 0 491510741 119803904 27916 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29249 27916 603 41 0 29208 0
vsize: 116996
[startup+1170.05 s]
Raw data (loadavg): 1.00 1.00 1.00 2/54 32745
Raw data (stat): 32745 (minisat+) R 32744 30701 30700 0 -1 0 28477 0 0 0 116937 82 0 0 25 0 1 0 491510741 120205312 28001 4294967295 134512640 134672761 3221224624 3221223792 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29347 28001 603 41 0 29306 0
vsize: 117388
[startup+1180.05 s]
Raw data (loadavg): 1.00 1.00 1.00 2/54 32745
Raw data (stat): 32745 (minisat+) R 32744 30701 30700 0 -1 0 28546 0 0 0 117937 82 0 0 25 0 1 0 491510741 120471552 28070 4294967295 134512640 134672761 3221224624 3221223792 134560811 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29412 28070 603 41 0 29371 0
vsize: 117648
[startup+1190.05 s]
Raw data (loadavg): 1.00 1.00 1.00 2/54 32745
Raw data (stat): 32745 (minisat+) R 32744 30701 30700 0 -1 0 28779 0 0 0 118936 83 0 0 25 0 1 0 491510741 121409536 28303 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29641 28303 603 41 0 29600 0
vsize: 118564
[startup+1200.05 s]
Raw data (loadavg): 1.00 1.00 1.00 2/54 32745
Raw data (stat): 32745 (minisat+) R 32744 30701 30700 0 -1 0 29177 0 0 0 119935 85 0 0 25 0 1 0 491510741 123027456 28701 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30036 28701 603 41 0 29995 0
vsize: 120144
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.11 s]
Raw data (loadavg): 1.00 1.00 1.00 1/54 32745
Raw data (stat): 32745 (minisat+) Z 32744 30701 30700 0 -1 12 29179 0 0 0 119935 90 0 0 25 0 1 0 491510741 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.11
CPU time (s): 1200.26
CPU user time (s): 1199.35
CPU system time (s): 0.905862
CPU usage (%): 100.013
Max. virtual memory (Kb): 120144
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####