PB'05 competition: run trace

Some explanations

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

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

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

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 450.999
cache size	: 512 KB
fdiv_bug	: no
hlt_bug		: no
f00f_bug	: no
coma_bug	: no
fpu		: yes
fpu_exception	: yes
cpuid level	: 2
wp		: yes
flags		: fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse
bogomips	: 899.07

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        585248 kB
Buffers:         31360 kB
Cached:         396124 kB
SwapCached:        440 kB
Active:          64120 kB
Inactive:       365548 kB
HighTotal:      131008 kB
HighFree:         1148 kB
LowTotal:       903652 kB
LowFree:        584100 kB
SwapTotal:     2097136 kB
SwapFree:      2095984 kB
Dirty:              40 kB
Writeback:           0 kB
Mapped:           5360 kB
Slab:            14192 kB
Committed_AS:    63484 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-21 17:02:56 (client local time) WITH STATUS 0 IN 1200.23 SECONDS
stats: 17420 7 1200.23 0
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 2884 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: ##############################################################################
c   -- Clauses(.)/Splits(s): ssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssss
c ---[3067]---> BDD-cost:   13
c ---[3066]---> BDD-cost:   13
c ---[3064]---> BDD-cost:   12
c ---[3063]---> BDD-cost:   13
c ---[3062]---> BDD-cost:   12
c ---[3061]---> BDD-cost:   11
c ---[3060]---> BDD-cost:   13
c ---[3059]---> BDD-cost:   13
c ---[3058]---> BDD-cost:   11
c ---[3056]---> BDD-cost:   11
c ---[3055]---> BDD-cost:   12
c ---[3053]---> BDD-cost:   13
c ---[3052]---> BDD-cost:   13
c ---[3051]---> BDD-cost:   10
c ---[3049]---> BDD-cost:   12
c ---[3048]---> BDD-cost:   13
c ---[3047]---> BDD-cost:   12
c ---[3046]---> BDD-cost:   13
c ---[3045]---> BDD-cost:   13
c ---[3044]---> BDD-cost:   13
c ---[3042]---> BDD-cost:   12
c ---[3040]---> BDD-cost:   11
c ---[3039]---> BDD-cost:   12
c ---[3038]---> BDD-cost:   12
c ---[3037]---> BDD-cost:   12
c ---[3036]---> BDD-cost:   12
c ---[3035]---> BDD-cost:   11
c ---[3034]---> BDD-cost:   11
c ---[3033]---> BDD-cost:   11
c ---[3032]---> BDD-cost:   13
c ---[3030]---> BDD-cost:   10
c ---[3028]---> BDD-cost:   11
c ---[3026]---> BDD-cost:   13
c ---[3025]---> BDD-cost:   13
c ---[3024]---> BDD-cost:   12
c ---[3023]---> BDD-cost:   13
c ---[3022]---> BDD-cost:   13
c ---[3021]---> BDD-cost:   13
c ---[3020]---> BDD-cost:   13
c ---[3019]---> BDD-cost:   12
c ---[3018]---> BDD-cost:   12
c ---[3017]---> BDD-cost:   11
c ---[3016]---> BDD-cost:   13
c ---[3015]---> BDD-cost:   13
c ---[3014]---> BDD-cost:   11
c ---[3013]---> BDD-cost:   13
c ---[3012]---> BDD-cost:   11
c ---[3011]---> BDD-cost:   11
c ---[3010]---> BDD-cost:   11
c ---[3009]---> BDD-cost:   13
c ---[3008]---> BDD-cost:   11
c ---[3007]---> BDD-cost:   13
c ---[3005]---> BDD-cost:   13
c ---[3004]---> BDD-cost:   13
c ---[3003]---> BDD-cost:   13
c ---[3002]---> BDD-cost:   12
c ---[3001]---> BDD-cost:   13
c ---[3000]---> BDD-cost:   12
c ---[2999]---> BDD-cost:   12
c ---[2998]---> BDD-cost:   12
c ---[2997]---> BDD-cost:   13
c ---[2996]---> BDD-cost:   12
c ---[2995]---> BDD-cost:   12
c ---[2994]---> BDD-cost:   13
c ---[2993]---> BDD-cost:   13
c ---[2992]---> BDD-cost:   13
c ---[2991]---> BDD-cost:   12
c ---[2990]---> BDD-cost:   13
c ---[2989]---> BDD-cost:   11
c ---[2988]---> BDD-cost:   10
c ---[2987]---> BDD-cost:   12
c ---[2986]---> BDD-cost:   12
c ---[2985]---> BDD-cost:   13
c ---[2984]---> BDD-cost:   11
c ---[2983]---> BDD-cost:   11
c ---[2982]---> BDD-cost:   13
c ---[2981]---> BDD-cost:   13
c ---[2980]---> BDD-cost:   13
c ---[2979]---> BDD-cost:   12
c ---[2978]---> BDD-cost:   12
c ---[2977]---> BDD-cost:   13
c ---[2976]---> BDD-cost:   12
c ---[2975]---> BDD-cost:   12
c ---[2974]---> BDD-cost:   13
c ---[2973]---> BDD-cost:   12
c ---[2972]---> BDD-cost:   12
c ---[2971]---> BDD-cost:   12
c ---[2969]---> BDD-cost:   13
c ---[2968]---> BDD-cost:   13
c ---[2967]---> BDD-cost:   12
c ---[2966]---> BDD-cost:   12
c ---[2965]---> BDD-cost:   12
c ---[2964]---> BDD-cost:   13
c ---[2963]---> BDD-cost:   13
c ---[2962]---> BDD-cost:   11
c ---[2961]---> BDD-cost:   13
c ---[2960]---> BDD-cost:   13
c ---[2959]---> BDD-cost:   11
c ---[2958]---> BDD-cost:   11
c ---[2955]---> BDD-cost:   13
c ---[2954]---> BDD-cost:   11
c ---[2953]---> BDD-cost:   13
c ---[2952]---> BDD-cost:   13
c ---[2951]---> BDD-cost:   12
c ---[2950]---> BDD-cost:   12
c ---[2949]---> BDD-cost:   12
c ---[2948]---> BDD-cost:   13
c ---[2947]---> BDD-cost:   12
c ---[2946]---> BDD-cost:   13
c ---[2945]---> BDD-cost:   12
c ---[2943]---> BDD-cost:   12
c ---[2942]---> BDD-cost:   13
c ---[2941]---> BDD-cost:   10
c ---[2940]---> BDD-cost:   13
c ---[2939]---> BDD-cost:   13
c ---[2938]---> BDD-cost:   13
c ---[2937]---> BDD-cost:   12
c ---[2935]---> BDD-cost:   12
c ---[2934]---> BDD-cost:   11
c ---[2933]---> BDD-cost:   13
c ---[2932]---> BDD-cost:   10
c ---[2930]---> BDD-cost:   12
c ---[2929]---> BDD-cost:   13
c ---[2928]---> BDD-cost:   13
c ---[2927]---> BDD-cost:   13
c ---[2926]---> BDD-cost:   13
c ---[2925]---> BDD-cost:   11
c ---[2924]---> BDD-cost:   13
c ---[2923]---> BDD-cost:   12
c ---[2922]---> BDD-cost:   13
c ---[2921]---> BDD-cost:   13
c ---[2919]---> BDD-cost:   12
c ---[2918]---> BDD-cost:   13
c ---[2917]---> BDD-cost:   12
c ---[2916]---> BDD-cost:   13
c ---[2915]---> BDD-cost:   10
c ---[2914]---> BDD-cost:   13
c ---[2913]---> BDD-cost:   12
c ---[2912]---> BDD-cost:   13
c ---[2911]---> BDD-cost:   11
c ---[2909]---> BDD-cost:   13
c ---[2907]---> BDD-cost:   13
c ---[2906]---> BDD-cost:   13
c ---[2905]---> BDD-cost:   11
c ---[2904]---> BDD-cost:   11
c ---[2902]---> BDD-cost:   13
c ---[2901]---> BDD-cost:   13
c ---[2900]---> BDD-cost:   13
c ---[2899]---> BDD-cost:   12
c ---[2898]---> BDD-cost:   13
c ---[2897]---> BDD-cost:   13
c ---[2896]---> BDD-cost:   12
c ---[2895]---> BDD-cost:   13
c ---[2894]---> BDD-cost:   11
c ---[2893]---> BDD-cost:   13
c ---[2892]---> BDD-cost:   13
c ---[2890]---> BDD-cost:   13
c ---[2889]---> BDD-cost:   12
c ---[2888]---> BDD-cost:   13
c ---[2887]---> BDD-cost:   10
c ---[2886]---> BDD-cost:   13
c ---[2884]---> BDD-cost:   13
c ---[2882]---> BDD-cost:   12
c ---[2881]---> BDD-cost:   13
c ---[2879]---> BDD-cost:   11
c ---[2877]---> BDD-cost:   12
c ---[2876]---> BDD-cost:   13
c ---[2875]---> BDD-cost:   13
c ---[2874]---> BDD-cost:   13
c ---[2873]---> BDD-cost:   13
c ---[2872]---> BDD-cost:   13
c ---[2871]---> BDD-cost:   13
c ---[2870]---> BDD-cost:   12
c ---[2869]---> BDD-cost:   13
c ---[2868]---> BDD-cost:   12
c ---[2866]---> BDD-cost:   13
c ---[2865]---> BDD-cost:   13
c ---[2864]---> BDD-cost:   11
c ---[2863]---> BDD-cost:   11
c ---[2862]---> BDD-cost:   11
c ---[2861]---> BDD-cost:   12
c ---[2860]---> BDD-cost:   12
c ---[2859]---> BDD-cost:   13
c ---[2858]---> BDD-cost:   13
c ---[2856]---> BDD-cost:   13
c ---[2855]---> BDD-cost:   12
c ---[2854]---> BDD-cost:   12
c ---[2853]---> BDD-cost:   12
c ---[2852]---> BDD-cost:   10
c ---[2851]---> BDD-cost:   11
c ---[2850]---> BDD-cost:   10
c ---[2849]---> BDD-cost:   12
c ---[2847]---> BDD-cost:   12
c ---[2846]---> BDD-cost:   10
c ---[2845]---> BDD-cost:   13
c ---[2844]---> BDD-cost:   13
c ---[2843]---> BDD-cost:   11
c ---[2842]---> BDD-cost:   13
c ---[2841]---> BDD-cost:   13
c ---[2840]---> BDD-cost:   13
c ---[2839]---> BDD-cost:   13
c ---[2838]---> BDD-cost:   12
c ---[2837]---> BDD-cost:   11
c ---[2836]---> BDD-cost:   11
c ---[2835]---> BDD-cost:   12
c ---[2834]---> BDD-cost:   13
c ---[2833]---> BDD-cost:   12
c ---[2832]---> BDD-cost:   11
c ---[2831]---> BDD-cost:   11
c ---[2830]---> BDD-cost:   12
c ---[2829]---> BDD-cost:   13
c ---[2828]---> BDD-cost:   11
c ---[2827]---> BDD-cost:   11
c ---[2826]---> BDD-cost:   13
c ---[2825]---> BDD-cost:   13
c ---[2824]---> BDD-cost:   11
c ---[2823]---> BDD-cost:   12
c ---[2822]---> BDD-cost:   13
c ---[2821]---> BDD-cost:   10
c ---[2820]---> BDD-cost:   13
c ---[2819]---> BDD-cost:   13
c ---[2817]---> BDD-cost:   13
c ---[2816]---> BDD-cost:   12
c ---[2815]---> BDD-cost:   10
c ---[2814]---> BDD-cost:   12
c ---[2813]---> BDD-cost:   12
c ---[2812]---> BDD-cost:   13
c ---[2811]---> BDD-cost:   11
c ---[2810]---> BDD-cost:   13
c ---[2808]---> BDD-cost:   13
c ---[2806]---> BDD-cost:   12
c ---[2805]---> BDD-cost:   11
c ---[2803]---> BDD-cost:   11
c ---[2802]---> BDD-cost:   13
c ---[2801]---> BDD-cost:   12
c ---[2800]---> BDD-cost:   13
c ---[2797]---> BDD-cost:   13
c ---[2796]---> BDD-cost:   12
c ---[2795]---> BDD-cost:   10
c ---[2794]---> BDD-cost:   13
c ---[2793]---> BDD-cost:   13
c ---[2792]---> BDD-cost:   13
c ---[2791]---> BDD-cost:   11
c ---[2790]---> BDD-cost:   13
c ---[2789]---> BDD-cost:   13
c ---[2788]---> BDD-cost:   13
c ---[2787]---> BDD-cost:   11
c ---[2786]---> BDD-cost:   13
c ---[2785]---> BDD-cost:   11
c ---[2784]---> BDD-cost:   12
c ---[2783]---> BDD-cost:   10
c ---[2781]---> BDD-cost:   13
c ---[2780]---> BDD-cost:   13
c ---[2779]---> BDD-cost:   12
c ---[2778]---> BDD-cost:   12
c ---[2777]---> BDD-cost:   13
c ---[2776]---> BDD-cost:   13
c ---[2775]---> BDD-cost:   13
c ---[2774]---> BDD-cost:   13
c ---[2773]---> BDD-cost:   13
c ---[2772]---> BDD-cost:   13
c ---[2771]---> BDD-cost:   13
c ---[2769]---> BDD-cost:   13
c ---[2768]---> BDD-cost:   13
c ---[2767]---> BDD-cost:   11
c ---[2766]---> BDD-cost:   12
c ---[2765]---> BDD-cost:   12
c ---[2764]---> BDD-cost:   13
c ---[2763]---> BDD-cost:   13
c ---[2762]---> BDD-cost:   13
c ---[2761]---> BDD-cost:   12
c ---[2760]---> BDD-cost:   12
c ---[2759]---> BDD-cost:   12
c ---[2758]---> BDD-cost:   13
c ---[2757]---> BDD-cost:   12
c ---[2756]---> BDD-cost:   13
c ---[2755]---> BDD-cost:   12
c ---[2754]---> BDD-cost:   13
c ---[2753]---> BDD-cost:   13
c ---[2752]---> BDD-cost:   10
c ---[2751]---> BDD-cost:   13
c ---[2750]---> BDD-cost:   11
c ---[2748]---> BDD-cost:   10
c ---[2747]---> BDD-cost:   13
c ---[2746]---> BDD-cost:   13
c ---[2744]---> BDD-cost:   10
c ---[2743]---> BDD-cost:   12
c ---[2742]---> BDD-cost:   13
c ---[2741]---> BDD-cost:   13
c ---[2740]---> BDD-cost:   13
c ---[2739]---> BDD-cost:   12
c ---[2737]---> BDD-cost:   13
c ---[2736]---> BDD-cost:   13
c ---[2735]---> BDD-cost:   12
c ---[2734]---> BDD-cost:   11
c ---[2733]---> BDD-cost:   13
c ---[2732]---> BDD-cost:   13
c ---[2731]---> BDD-cost:   13
c ---[2730]---> BDD-cost:   13
c ---[2728]---> BDD-cost:   13
c ---[2727]---> BDD-cost:   13
c ---[2726]---> BDD-cost:   13
c ---[2724]---> BDD-cost:   13
c ---[2723]---> BDD-cost:   12
c ---[2722]---> BDD-cost:   13
c ---[2721]---> BDD-cost:   13
c ---[2720]---> BDD-cost:   13
c ---[2719]---> BDD-cost:   12
c ---[2718]---> BDD-cost:   13
c ---[2717]---> BDD-cost:   11
c ---[2716]---> BDD-cost:   13
c ---[2715]---> BDD-cost:   12
c ---[2714]---> BDD-cost:   13
c ---[2712]---> BDD-cost:   13
c ---[2710]---> BDD-cost:   13
c ---[2709]---> BDD-cost:   13
c ---[2708]---> BDD-cost:   10
c ---[2706]---> BDD-cost:   13
c ---[2705]---> BDD-cost:   13
c ---[2704]---> BDD-cost:   12
c ---[2703]---> BDD-cost:   13
c ---[2701]---> BDD-cost:   13
c ---[2700]---> BDD-cost:   12
c ---[2699]---> BDD-cost:   12
c ---[2698]---> BDD-cost:   13
c ---[2697]---> BDD-cost:   13
c ---[2696]---> BDD-cost:   13
c ---[2695]---> BDD-cost:   13
c ---[2694]---> BDD-cost:   13
c ---[2693]---> BDD-cost:   13
c ---[2692]---> BDD-cost:   13
c ---[2691]---> BDD-cost:   11
c ---[2690]---> BDD-cost:   13
c ---[2689]---> BDD-cost:   12
c ---[2688]---> BDD-cost:   13
c ---[2687]---> BDD-cost:   13
c ---[2686]---> BDD-cost:   12
c ---[2685]---> BDD-cost:   12
c ---[2684]---> BDD-cost:   13
c ---[2683]---> BDD-cost:   13
c ---[2682]---> BDD-cost:   13
c ---[2681]---> BDD-cost:   11
c ---[2680]---> BDD-cost:   11
c ---[2679]---> BDD-cost:   13
c ---[2678]---> BDD-cost:   12
c ---[2677]---> BDD-cost:   12
c ---[2675]---> BDD-cost:   13
c ---[2674]---> BDD-cost:   13
c ---[2673]---> BDD-cost:   13
c ---[2672]---> BDD-cost:   12
c ---[2671]---> BDD-cost:   11
c ---[2670]---> BDD-cost:   12
c ---[2669]---> BDD-cost:   13
c ---[2668]---> BDD-cost:   10
c ---[2667]---> BDD-cost:   13
c ---[2665]---> BDD-cost:   12
c ---[2664]---> BDD-cost:   11
c ---[2662]---> BDD-cost:   13
c ---[2661]---> BDD-cost:   11
c ---[2660]---> BDD-cost:   11
c ---[2659]---> BDD-cost:   13
c ---[2658]---> BDD-cost:   12
c ---[2656]---> BDD-cost:   13
c ---[2654]---> BDD-cost:   13
c ---[2653]---> BDD-cost:   11
c ---[2652]---> BDD-cost:   12
c ---[2651]---> BDD-cost:   13
c ---[2650]---> BDD-cost:   12
c ---[2648]---> BDD-cost:   12
c ---[2647]---> BDD-cost:   11
c ---[2646]---> BDD-cost:   10
c ---[2645]---> BDD-cost:   12
c ---[2644]---> BDD-cost:   12
c ---[2643]---> BDD-cost:   12
c ---[2642]---> BDD-cost:   12
c ---[2641]---> BDD-cost:   13
c ---[2638]---> BDD-cost:   13
c ---[2637]---> BDD-cost:   12
c ---[2636]---> BDD-cost:   11
c ---[2635]---> BDD-cost:   11
c ---[2634]---> BDD-cost:   10
c ---[2633]---> BDD-cost:   13
c ---[2632]---> BDD-cost:   11
c ---[2631]---> BDD-cost:   12
c ---[2630]---> BDD-cost:   13
c ---[2629]---> BDD-cost:   11
c ---[2628]---> BDD-cost:   12
c ---[2627]---> BDD-cost:   13
c ---[2626]---> BDD-cost:   13
c ---[2625]---> BDD-cost:   12
c ---[2624]---> BDD-cost:   12
c ---[2623]---> BDD-cost:   13
c ---[2622]---> BDD-cost:   13
c ---[2621]---> BDD-cost:   13
c ---[2620]---> BDD-cost:   13
c ---[2619]---> BDD-cost:   11
c ---[2618]---> BDD-cost:   13
c ---[2617]---> BDD-cost:   12
c ---[2616]---> BDD-cost:   13
c ---[2615]---> BDD-cost:   13
c ---[2614]---> BDD-cost:   13
c ---[2613]---> BDD-cost:   12
c ---[2612]---> BDD-cost:   13
c ---[2611]---> BDD-cost:   13
c ---[2610]---> BDD-cost:   12
c ---[2609]---> BDD-cost:   12
c ---[2608]---> BDD-cost:   12
c ---[2606]---> BDD-cost:   12
c ---[2604]---> BDD-cost:   11
c ---[2603]---> BDD-cost:   12
c ---[2602]---> BDD-cost:   13
c ---[2601]---> BDD-cost:   13
c ---[2600]---> BDD-cost:   11
c ---[2599]---> BDD-cost:   13
c ---[2598]---> BDD-cost:   13
c ---[2597]---> BDD-cost:   11
c ---[2596]---> BDD-cost:   13
c ---[2595]---> BDD-cost:   13
c ---[2594]---> BDD-cost:   12
c ---[2593]---> BDD-cost:   13
c ---[2592]---> BDD-cost:   11
c ---[2591]---> BDD-cost:   13
c ---[2590]---> BDD-cost:   12
c ---[2589]---> BDD-cost:   13
c ---[2587]---> BDD-cost:   12
c ---[2586]---> BDD-cost:   13
c ---[2584]---> BDD-cost:   12
c ---[2583]---> BDD-cost:   13
c ---[2582]---> BDD-cost:   13
c ---[2581]---> BDD-cost:   13
c ---[2580]---> BDD-cost:   10
c ---[2579]---> BDD-cost:   11
c ---[2576]---> BDD-cost:   13
c ---[2575]---> BDD-cost:   13
c ---[2574]---> BDD-cost:   13
c ---[2572]---> BDD-cost:   11
c ---[2571]---> BDD-cost:   13
c ---[2570]---> BDD-cost:   13
c ---[2569]---> BDD-cost:   11
c ---[2568]---> BDD-cost:   13
c ---[2567]---> BDD-cost:   10
c ---[2566]---> BDD-cost:   12
c ---[2565]---> BDD-cost:   12
c ---[2564]---> BDD-cost:   13
c ---[2563]---> BDD-cost:   13
c ---[2562]---> BDD-cost:   13
c ---[2561]---> BDD-cost:   12
c ---[2559]---> BDD-cost:   12
c ---[2558]---> BDD-cost:   12
c ---[2557]---> BDD-cost:   13
c ---[2556]---> BDD-cost:   13
c ---[2554]---> BDD-cost:   11
c ---[2553]---> BDD-cost:   12
c ---[2550]---> BDD-cost:   12
c ---[2549]---> BDD-cost:   12
c ---[2548]---> BDD-cost:   11
c ---[2546]---> BDD-cost:   13
c ---[2545]---> BDD-cost:   10
c ---[2543]---> BDD-cost:   12
c ---[2541]---> BDD-cost:   13
c ---[2540]---> BDD-cost:   11
c ---[2539]---> BDD-cost:   13
c ---[2538]---> BDD-cost:   13
c ---[2537]---> BDD-cost:   13
c ---[2535]---> BDD-cost:   12
c ---[2533]---> BDD-cost:   12
c ---[2532]---> BDD-cost:   13
c ---[2531]---> BDD-cost:   11
c ---[2530]---> BDD-cost:   13
c ---[2529]---> BDD-cost:   12
c ---[2528]---> BDD-cost:   13
c ---[2527]---> BDD-cost:   13
c ---[2526]---> BDD-cost:   12
c ---[2524]---> BDD-cost:   13
c ---[2523]---> BDD-cost:   12
c ---[2522]---> BDD-cost:   13
c ---[2520]---> BDD-cost:   10
c ---[2519]---> BDD-cost:   12
c ---[2518]---> BDD-cost:   12
c ---[2517]---> BDD-cost:   13
c ---[2516]---> BDD-cost:   13
c ---[2515]---> BDD-cost:   12
c ---[2514]---> BDD-cost:   12
c ---[2513]---> BDD-cost:   12
c ---[2512]---> BDD-cost:   12
c ---[2511]---> BDD-cost:   13
c ---[2510]---> BDD-cost:   11
c ---[2509]---> BDD-cost:   13
c ---[2507]---> BDD-cost:   12
c ---[2506]---> BDD-cost:   12
c ---[2505]---> BDD-cost:   12
c ---[2504]---> BDD-cost:   13
c ---[2503]---> BDD-cost:   12
c ---[2502]---> BDD-cost:   13
c ---[2499]---> BDD-cost:   11
c ---[2498]---> BDD-cost:   13
c ---[2497]---> BDD-cost:   13
c ---[2495]---> BDD-cost:   13
c ---[2491]---> BDD-cost:   13
c ---[2489]---> BDD-cost:   12
c ---[2488]---> BDD-cost:   12
c ---[2484]---> BDD-cost:   12
c ---[2483]---> BDD-cost:   13
c ---[2482]---> BDD-cost:   13
c ---[2481]---> BDD-cost:   11
c ---[2479]---> BDD-cost:   10
c ---[2477]---> BDD-cost:   12
c ---[2476]---> BDD-cost:   13
c ---[2475]---> BDD-cost:   13
c ---[2474]---> BDD-cost:   13
c ---[2473]---> BDD-cost:   11
c ---[2472]---> BDD-cost:   13
c ---[2471]---> BDD-cost:   12
c ---[2470]---> BDD-cost:   13
c ---[2469]---> BDD-cost:   12
c ---[2468]---> BDD-cost:   12
c ---[2467]---> BDD-cost:   12
c ---[2466]---> BDD-cost:   13
c ---[2464]---> BDD-cost:   11
c ---[2463]---> BDD-cost:   12
c ---[2462]---> BDD-cost:   12
c ---[2460]---> BDD-cost:   11
c ---[2459]---> BDD-cost:   13
c ---[2457]---> BDD-cost:   11
c ---[2456]---> BDD-cost:   11
c ---[2454]---> BDD-cost:   13
c ---[2453]---> BDD-cost:   10
c ---[2451]---> BDD-cost:   13
c ---[2450]---> BDD-cost:   13
c ---[2449]---> BDD-cost:   13
c ---[2447]---> BDD-cost:   12
c ---[2446]---> BDD-cost:   13
c ---[2445]---> BDD-cost:   12
c ---[2444]---> BDD-cost:   10
c ---[2443]---> BDD-cost:   13
c ---[2442]---> BDD-cost:   13
c ---[2440]---> BDD-cost:   12
c ---[2439]---> BDD-cost:   13
c ---[2438]---> BDD-cost:   12
c ---[2437]---> BDD-cost:   12
c ---[2436]---> BDD-cost:   11
c ---[2435]---> BDD-cost:   13
c ---[2434]---> BDD-cost:   13
c ---[2433]---> BDD-cost:   13
c ---[2432]---> BDD-cost:   13
c ---[2431]---> BDD-cost:   13
c ---[2430]---> BDD-cost:   12
c ---[2429]---> BDD-cost:   13
c ---[2428]---> BDD-cost:   12
c ---[2427]---> BDD-cost:   13
c ---[2426]---> BDD-cost:   13
c ---[2425]---> BDD-cost:   12
c ---[2424]---> BDD-cost:   13
c ---[2423]---> BDD-cost:   11
c ---[2422]---> BDD-cost:   12
c ---[2421]---> BDD-cost:   10
c ---[2419]---> BDD-cost:   11
c ---[2418]---> BDD-cost:   11
c ---[2417]---> BDD-cost:   12
c ---[2416]---> BDD-cost:   13
c ---[2415]---> BDD-cost:   12
c ---[2413]---> BDD-cost:   12
c ---[2412]---> BDD-cost:   13
c ---[2410]---> BDD-cost:   13
c ---[2409]---> BDD-cost:   13
c ---[2408]---> BDD-cost:   11
c ---[2407]---> BDD-cost:   13
c ---[2406]---> BDD-cost:   11
c ---[2405]---> BDD-cost:   13
c ---[2404]---> BDD-cost:   12
c ---[2403]---> BDD-cost:   13
c ---[2402]---> BDD-cost:   11
c ---[2401]---> BDD-cost:   13
c ---[2400]---> BDD-cost:   12
c ---[2399]---> BDD-cost:   13
c ---[2398]---> BDD-cost:   10
c ---[2397]---> BDD-cost:   12
c ---[2396]---> BDD-cost:   12
c ---[2395]---> BDD-cost:   13
c ---[2394]---> BDD-cost:   12
c ---[2393]---> BDD-cost:   10
c ---[2392]---> BDD-cost:   13
c ---[2390]---> BDD-cost:   12
c ---[2389]---> BDD-cost:   11
c ---[2388]---> BDD-cost:   13
c ---[2387]---> BDD-cost:   11
c ---[2386]---> BDD-cost:   13
c ---[2385]---> BDD-cost:   12
c ---[2384]---> BDD-cost:   13
c ---[2383]---> BDD-cost:   13
c ---[2382]---> BDD-cost:   13
c ---[2381]---> BDD-cost:   10
c ---[2379]---> BDD-cost:   12
c ---[2378]---> BDD-cost:   12
c ---[2377]---> BDD-cost:   13
c ---[2376]---> BDD-cost:   13
c ---[2375]---> BDD-cost:   11
c ---[2374]---> BDD-cost:   12
c ---[2373]---> BDD-cost:   12
c ---[2372]---> BDD-cost:   12
c ---[2371]---> BDD-cost:   12
c ---[2370]---> BDD-cost:   10
c ---[2369]---> BDD-cost:   13
c ---[2367]---> BDD-cost:   12
c ---[2366]---> BDD-cost:   13
c ---[2365]---> BDD-cost:   13
c ---[2364]---> BDD-cost:   10
c ---[2363]---> BDD-cost:   13
c ---[2362]---> BDD-cost:   11
c ---[2361]---> BDD-cost:   13
c ---[2360]---> BDD-cost:   12
c ---[2359]---> BDD-cost:   12
c ---[2358]---> BDD-cost:   12
c ---[2357]---> BDD-cost:   13
c ---[2356]---> BDD-cost:   13
c ---[2354]---> BDD-cost:   11
c ---[2353]---> BDD-cost:   13
c ---[2352]---> BDD-cost:   13
c ---[2350]---> BDD-cost:   13
c ---[2348]---> BDD-cost:   10
c ---[2347]---> BDD-cost:   11
c ---[2346]---> BDD-cost:   13
c ---[2345]---> BDD-cost:   13
c ---[2344]---> BDD-cost:   13
c ---[2342]---> BDD-cost:   13
c ---[2341]---> BDD-cost:   13
c ---[2340]---> BDD-cost:   13
c ---[2338]---> BDD-cost:   13
c ---[2337]---> BDD-cost:   12
c ---[2336]---> BDD-cost:   13
c ---[2334]---> BDD-cost:   13
c ---[2333]---> BDD-cost:   13
c ---[2332]---> BDD-cost:   10
c ---[2331]---> BDD-cost:   12
c ---[2330]---> BDD-cost:   13
c ---[2329]---> BDD-cost:   13
c ---[2328]---> BDD-cost:   13
c ---[2327]---> BDD-cost:   13
c ---[2324]---> BDD-cost:   11
c ---[2321]---> BDD-cost:   13
c ---[2320]---> BDD-cost:   12
c ---[2319]---> BDD-cost:   13
c ---[2318]---> BDD-cost:   13
c ---[2317]---> BDD-cost:   13
c ---[2315]---> BDD-cost:   13
c ---[2314]---> BDD-cost:   11
c ---[2313]---> BDD-cost:   12
c ---[2312]---> BDD-cost:   13
c ---[2311]---> BDD-cost:   12
c ---[2310]---> BDD-cost:   12
c ---[2309]---> BDD-cost:   11
c ---[2307]---> BDD-cost:   13
c ---[2306]---> BDD-cost:   10
c ---[2305]---> BDD-cost:   10
c ---[2304]---> BDD-cost:   13
c ---[2303]---> BDD-cost:   13
c ---[2302]---> BDD-cost:   13
c ---[2301]---> BDD-cost:   13
c ---[2300]---> BDD-cost:   12
c ---[2299]---> BDD-cost:   12
c ---[2298]---> BDD-cost:   11
c ---[2297]---> BDD-cost:   10
c ---[2296]---> BDD-cost:   13
c ---[2294]---> BDD-cost:   12
c ---[2293]---> BDD-cost:   13
c ---[2292]---> BDD-cost:   12
c ---[2291]---> BDD-cost:   11
c ---[2290]---> BDD-cost:   12
c ---[2289]---> BDD-cost:   13
c ---[2288]---> BDD-cost:   11
c ---[2287]---> BDD-cost:   11
c ---[2286]---> BDD-cost:   12
c ---[2285]---> BDD-cost:   12
c ---[2284]---> BDD-cost:   13
c ---[2283]---> BDD-cost:   13
c ---[2282]---> BDD-cost:   11
c ---[2281]---> BDD-cost:   11
c ---[2280]---> BDD-cost:   12
c ---[2279]---> BDD-cost:   13
c ---[2277]---> BDD-cost:   12
c ---[2276]---> BDD-cost:   13
c ---[2275]---> BDD-cost:   13
c ---[2274]---> BDD-cost:   12
c ---[2273]---> BDD-cost:   13
c ---[2272]---> BDD-cost:   12
c ---[2271]---> BDD-cost:   12
c ---[2268]---> BDD-cost:   13
c ---[2267]---> BDD-cost:   11
c ---[2265]---> BDD-cost:   13
c ---[2264]---> BDD-cost:   12
c ---[2263]---> BDD-cost:   12
c ---[2262]---> BDD-cost:   10
c ---[2260]---> BDD-cost:   12
c ---[2259]---> BDD-cost:   12
c ---[2258]---> BDD-cost:   13
c ---[2257]---> BDD-cost:   12
c ---[2256]---> BDD-cost:   12
c ---[2255]---> BDD-cost:   13
c ---[2254]---> BDD-cost:   11
c ---[2253]---> BDD-cost:   13
c ---[2252]---> BDD-cost:   13
c ---[2251]---> BDD-cost:   12
c ---[2250]---> BDD-cost:   13
c ---[2249]---> BDD-cost:   13
c ---[2248]---> BDD-cost:   11
c ---[2247]---> BDD-cost:   12
c ---[2246]---> BDD-cost:   11
c ---[2245]---> BDD-cost:   12
c ---[2244]---> BDD-cost:   13
c ---[2243]---> BDD-cost:   13
c ---[2242]---> BDD-cost:   12
c ---[2241]---> BDD-cost:   13
c ---[2240]---> BDD-cost:   12
c ---[2239]---> BDD-cost:   13
c ---[2238]---> BDD-cost:   13
c ---[2237]---> BDD-cost:   12
c ---[2236]---> BDD-cost:   13
c ---[2235]---> BDD-cost:   11
c ---[2234]---> BDD-cost:   13
c ---[2233]---> BDD-cost:   13
c ---[2232]---> BDD-cost:   13
c ---[2231]---> BDD-cost:   12
c ---[2230]---> BDD-cost:   13
c ---[2229]---> BDD-cost:   11
c ---[2228]---> BDD-cost:   13
c ---[2226]---> BDD-cost:   12
c ---[2225]---> BDD-cost:   12
c ---[2224]---> BDD-cost:   12
c ---[2223]---> BDD-cost:   13
c ---[2222]---> BDD-cost:   13
c ---[2221]---> BDD-cost:   13
c ---[2220]---> BDD-cost:   12
c ---[2219]---> BDD-cost:   12
c ---[2218]---> BDD-cost:   10
c ---[2217]---> BDD-cost:   13
c ---[2216]---> BDD-cost:   13
c ---[2215]---> BDD-cost:   12
c ---[2214]---> BDD-cost:   12
c ---[2213]---> BDD-cost:   11
c ---[2212]---> BDD-cost:   10
c ---[2211]---> BDD-cost:   13
c ---[2210]---> BDD-cost:   13
c ---[2208]---> BDD-cost:   10
c ---[2207]---> BDD-cost:   12
c ---[2206]---> BDD-cost:   12
c ---[2205]---> BDD-cost:   13
c ---[2204]---> BDD-cost:   12
c ---[2203]---> BDD-cost:   13
c ---[2202]---> BDD-cost:   13
c ---[2200]---> BDD-cost:   13
c ---[2199]---> BDD-cost:   13
c ---[2198]---> BDD-cost:   11
c ---[2195]---> BDD-cost:   13
c ---[2194]---> BDD-cost:   10
c ---[2193]---> BDD-cost:   12
c ---[2192]---> BDD-cost:   11
c ---[2191]---> BDD-cost:   12
c ---[2190]---> BDD-cost:   13
c ---[2189]---> BDD-cost:   12
c ---[2188]---> BDD-cost:   13
c ---[2187]---> BDD-cost:   13
c ---[2186]---> BDD-cost:   13
c ---[2184]---> BDD-cost:   10
c ---[2182]---> BDD-cost:   13
c ---[2181]---> BDD-cost:   13
c ---[2180]---> BDD-cost:   11
c ---[2179]---> BDD-cost:   12
c ---[2178]---> BDD-cost:   13
c ---[2177]---> BDD-cost:   13
c ---[2175]---> BDD-cost:   13
c ---[2173]---> BDD-cost:   10
c ---[2172]---> BDD-cost:   12
c ---[2171]---> BDD-cost:   13
c ---[2170]---> BDD-cost:   11
c ---[2168]---> BDD-cost:   13
c ---[2167]---> BDD-cost:   12
c ---[2166]---> BDD-cost:   13
c ---[2165]---> BDD-cost:   13
c ---[2164]---> BDD-cost:   13
c ---[2163]---> BDD-cost:   13
c ---[2162]---> BDD-cost:   12
c ---[2161]---> BDD-cost:   12
c ---[2159]---> BDD-cost:   11
c ---[2158]---> BDD-cost:   12
c ---[2157]---> BDD-cost:   12
c ---[2155]---> BDD-cost:   12
c ---[2154]---> BDD-cost:   13
c ---[2153]---> BDD-cost:   13
c ---[2152]---> BDD-cost:   12
c ---[2151]---> BDD-cost:   13
c ---[2150]---> BDD-cost:   13
c ---[2149]---> BDD-cost:   13
c ---[2148]---> BDD-cost:   11
c ---[2147]---> BDD-cost:   11
c ---[2146]---> BDD-cost:   13
c ---[2145]---> BDD-cost:   13
c ---[2144]---> BDD-cost:   13
c ---[2143]---> BDD-cost:   13
c ---[2142]---> BDD-cost:   13
c ---[2141]---> BDD-cost:   10
c ---[2140]---> BDD-cost:   12
c ---[2139]---> BDD-cost:   10
c ---[2137]---> BDD-cost:   12
c ---[2136]---> BDD-cost:   13
c ---[2135]---> BDD-cost:   13
c ---[2134]---> BDD-cost:   13
c ---[2133]---> BDD-cost:   12
c ---[2132]---> BDD-cost:   12
c ---[2131]---> BDD-cost:   12
c ---[2130]---> BDD-cost:   12
c ---[2129]---> BDD-cost:   12
c ---[2128]---> BDD-cost:   13
c ---[2127]---> BDD-cost:   13
c ---[2126]---> BDD-cost:   12
c ---[2124]---> BDD-cost:   13
c ---[2123]---> BDD-cost:   12
c ---[2122]---> BDD-cost:   11
c ---[2121]---> BDD-cost:   10
c ---[2120]---> BDD-cost:   13
c ---[2119]---> BDD-cost:   12
c ---[2118]---> BDD-cost:   12
c ---[2117]---> BDD-cost:   11
c ---[2116]---> BDD-cost:   13
c ---[2115]---> BDD-cost:   13
c ---[2114]---> BDD-cost:   13
c ---[2113]---> BDD-cost:   12
c ---[2112]---> BDD-cost:   13
c ---[2111]---> BDD-cost:   13
c ---[2110]---> BDD-cost:   13
c ---[2109]---> BDD-cost:   13
c ---[2107]---> BDD-cost:   13
c ---[2106]---> BDD-cost:   10
c ---[2105]---> BDD-cost:   12
c ---[2104]---> BDD-cost:   13
c ---[2102]---> BDD-cost:   13
c ---[2101]---> BDD-cost:   12
c ---[2100]---> BDD-cost:   13
c ---[2099]---> BDD-cost:   13
c ---[2098]---> BDD-cost:   13
c ---[2097]---> BDD-cost:   13
c ---[2096]---> BDD-cost:   11
c ---[2095]---> BDD-cost:   13
c ---[2093]---> BDD-cost:   11
c ---[2092]---> BDD-cost:   11
c ---[2091]---> BDD-cost:   13
c ---[2090]---> BDD-cost:   13
c ---[2089]---> BDD-cost:   12
c ---[2088]---> BDD-cost:   12
c ---[2087]---> BDD-cost:   12
c ---[2086]---> BDD-cost:   13
c ---[2084]---> BDD-cost:   13
c ---[2083]---> BDD-cost:   13
c ---[2082]---> BDD-cost:   12
c ---[2081]---> BDD-cost:   12
c ---[2080]---> BDD-cost:   13
c ---[2079]---> BDD-cost:   13
c ---[2078]---> BDD-cost:   13
c ---[2077]---> BDD-cost:   12
c ---[2076]---> BDD-cost:   12
c ---[2075]---> BDD-cost:   11
c ---[2074]---> BDD-cost:   12
c ---[2073]---> BDD-cost:   12
c ---[2072]---> BDD-cost:   13
c ---[2071]---> BDD-cost:   13
c ---[2070]---> BDD-cost:   13
c ---[2069]---> BDD-cost:   13
c ---[2068]---> BDD-cost:   12
c ---[2067]---> BDD-cost:   11
c ---[2066]---> BDD-cost:   13
c ---[2065]---> BDD-cost:   13
c ---[2064]---> BDD-cost:   11
c ---[2063]---> BDD-cost:   12
c ---[2062]---> BDD-cost:   10
c ---[2061]---> BDD-cost:   13
c ---[2060]---> BDD-cost:   12
c ---[2059]---> BDD-cost:   11
c ---[2058]---> BDD-cost:   13
c ---[2057]---> BDD-cost:   12
c ---[2056]---> BDD-cost:   12
c ---[2055]---> BDD-cost:   11
c ---[2054]---> BDD-cost:   12
c ---[2052]---> BDD-cost:   13
c ---[2051]---> BDD-cost:   12
c ---[2050]---> BDD-cost:   13
c ---[2048]---> BDD-cost:   13
c ---[2047]---> BDD-cost:   12
c ---[2046]---> BDD-cost:   13
c ---[2045]---> BDD-cost:   13
c ---[2044]---> BDD-cost:   12
c ---[2042]---> BDD-cost:   12
c ---[2041]---> BDD-cost:   13
c ---[2040]---> BDD-cost:   13
c ---[2039]---> BDD-cost:   11
c ---[2038]---> BDD-cost:   12
c ---[2037]---> BDD-cost:   13
c ---[2036]---> BDD-cost:   13
c ---[2034]---> BDD-cost:   13
c ---[2033]---> BDD-cost:   12
c ---[2031]---> BDD-cost:   13
c ---[2030]---> BDD-cost:   10
c ---[2029]---> BDD-cost:   11
c ---[2028]---> BDD-cost:   12
c ---[2027]---> BDD-cost:   13
c ---[2026]---> BDD-cost:   13
c ---[2025]---> BDD-cost:   13
c ---[2024]---> BDD-cost:   13
c ---[2023]---> BDD-cost:   13
c ---[2022]---> BDD-cost:   12
c ---[2021]---> BDD-cost:   13
c ---[2020]---> BDD-cost:   12
c ---[2019]---> BDD-cost:   12
c ---[2018]---> BDD-cost:   11
c ---[2017]---> BDD-cost:   13
c ---[2015]---> BDD-cost:   13
c ---[2014]---> BDD-cost:   12
c ---[2013]---> BDD-cost:   12
c ---[2012]---> BDD-cost:   12
c ---[2011]---> BDD-cost:   13
c ---[2010]---> BDD-cost:   13
c ---[2009]---> BDD-cost:   13
c ---[2008]---> BDD-cost:   11
c ---[2007]---> BDD-cost:   13
c ---[2006]---> BDD-cost:   13
c ---[2005]---> BDD-cost:   13
c ---[2004]---> BDD-cost:   12
c ---[2003]---> BDD-cost:   13
c ---[2002]---> BDD-cost:   13
c ---[2001]---> BDD-cost:   13
c ---[2000]---> BDD-cost:   12
c ---[1999]---> BDD-cost:   12
c ---[1998]---> BDD-cost:   11
c ---[1997]---> BDD-cost:   13
c ---[1995]---> BDD-cost:   12
c ---[1994]---> BDD-cost:   11
c ---[1993]---> BDD-cost:   13
c ---[1992]---> BDD-cost:   12
c ---[1991]---> BDD-cost:   13
c ---[1990]---> BDD-cost:   12
c ---[1989]---> BDD-cost:   10
c ---[1988]---> BDD-cost:   12
c ---[1987]---> BDD-cost:   13
c ---[1986]---> BDD-cost:   11
c ---[1985]---> BDD-cost:   12
c ---[1984]---> BDD-cost:   12
c ---[1983]---> BDD-cost:   12
c ---[1982]---> BDD-cost:   12
c ---[1981]---> BDD-cost:   12
c ---[1980]---> BDD-cost:   11
c ---[1979]---> BDD-cost:   12
c ---[1978]---> BDD-cost:   13
c ---[1977]---> BDD-cost:   12
c ---[1975]---> BDD-cost:   12
c ---[1974]---> BDD-cost:   12
c ---[1973]---> BDD-cost:   11
c ---[1972]---> BDD-cost:   10
c ---[1971]---> BDD-cost:   13
c ---[1970]---> BDD-cost:   12
c ---[1969]---> BDD-cost:   12
c ---[1968]---> BDD-cost:   13
c ---[1967]---> BDD-cost:   12
c ---[1966]---> BDD-cost:   13
c ---[1965]---> BDD-cost:   11
c ---[1964]---> BDD-cost:   12
c ---[1963]---> BDD-cost:   12
c ---[1962]---> BDD-cost:   13
c ---[1960]---> BDD-cost:   13
c ---[1959]---> BDD-cost:   12
c ---[1958]---> BDD-cost:   11
c ---[1957]---> BDD-cost:   11
c ---[1956]---> BDD-cost:   13
c ---[1955]---> BDD-cost:   13
c ---[1954]---> BDD-cost:   13
c ---[1952]---> BDD-cost:   13
c ---[1951]---> BDD-cost:   13
c ---[1949]---> BDD-cost:   13
c ---[1948]---> BDD-cost:   12
c ---[1947]---> BDD-cost:   12
c ---[1946]---> BDD-cost:   13
c ---[1945]---> BDD-cost:   12
c ---[1944]---> BDD-cost:   13
c ---[1943]---> BDD-cost:   12
c ---[1942]---> BDD-cost:   12
c ---[1941]---> BDD-cost:   13
c ---[1940]---> BDD-cost:   12
c ---[1939]---> BDD-cost:   11
c ---[1935]---> BDD-cost:   13
c ---[1934]---> BDD-cost:   12
c ---[1931]---> BDD-cost:   13
c ---[1930]---> BDD-cost:   12
c ---[1929]---> BDD-cost:   12
c ---[1926]---> BDD-cost:   13
c ---[1924]---> BDD-cost:   13
c ---[1923]---> BDD-cost:   12
c ---[1922]---> BDD-cost:   13
c ---[1921]---> BDD-cost:   12
c ---[1920]---> BDD-cost:   13
c ---[1919]---> BDD-cost:   12
c ---[1918]---> BDD-cost:   12
c ---[1917]---> BDD-cost:   13
c ---[1916]---> BDD-cost:   13
c ---[1915]---> BDD-cost:   13
c ---[1914]---> BDD-cost:   13
c ---[1913]---> BDD-cost:   12
c ---[1912]---> BDD-cost:   12
c ---[1911]---> BDD-cost:   13
c ---[1910]---> BDD-cost:   13
c ---[1909]---> BDD-cost:   12
c ---[1908]---> BDD-cost:   13
c ---[1907]---> BDD-cost:   12
c ---[1906]---> BDD-cost:   13
c ---[1905]---> BDD-cost:   13
c ---[1904]---> BDD-cost:   12
c ---[1903]---> BDD-cost:   13
c ---[1902]---> BDD-cost:   13
c ---[1901]---> BDD-cost:   11
c ---[1900]---> BDD-cost:   11
c ---[1899]---> BDD-cost:   13
c ---[1898]---> BDD-cost:   13
c ---[1897]---> BDD-cost:   12
c ---[1896]---> BDD-cost:   12
c ---[1895]---> BDD-cost:   12
c ---[1893]---> BDD-cost:   10
c ---[1892]---> BDD-cost:   13
c ---[1891]---> BDD-cost:   10
c ---[1890]---> BDD-cost:   13
c ---[1889]---> BDD-cost:   13
c ---[1888]---> BDD-cost:   13
c ---[1887]---> BDD-cost:   11
c ---[1886]---> BDD-cost:   13
c ---[1885]---> BDD-cost:   13
c ---[1883]---> BDD-cost:   12
c ---[1882]---> BDD-cost:   11
c ---[1881]---> BDD-cost:   13
c ---[1879]---> BDD-cost:   12
c ---[1878]---> BDD-cost:   13
c ---[1877]---> BDD-cost:   13
c ---[1875]---> BDD-cost:   13
c ---[1874]---> BDD-cost:   13
c ---[1872]---> BDD-cost:   10
c ---[1871]---> BDD-cost:   13
c ---[1869]---> BDD-cost:   13
c ---[1868]---> BDD-cost:   13
c ---[1867]---> BDD-cost:   13
c ---[1865]---> BDD-cost:   13
c ---[1862]---> BDD-cost:   11
c ---[1861]---> BDD-cost:   12
c ---[1860]---> BDD-cost:   13
c ---[1859]---> BDD-cost:   12
c ---[1858]---> BDD-cost:   13
c ---[1857]---> BDD-cost:   12
c ---[1856]---> BDD-cost:   11
c ---[1855]---> BDD-cost:   13
c ---[1854]---> BDD-cost:   12
c ---[1853]---> BDD-cost:   12
c ---[1851]---> BDD-cost:   12
c ---[1850]---> BDD-cost:   13
c ---[1849]---> BDD-cost:   11
c ---[1848]---> BDD-cost:   11
c ---[1847]---> BDD-cost:   13
c ---[1846]---> BDD-cost:   12
c ---[1845]---> BDD-cost:   12
c ---[1844]---> BDD-cost:   12
c ---[1843]---> BDD-cost:   13
c ---[1842]---> BDD-cost:   11
c ---[1841]---> BDD-cost:   13
c ---[1840]---> BDD-cost:   11
c ---[1839]---> BDD-cost:   12
c ---[1838]---> BDD-cost:   12
c ---[1837]---> BDD-cost:   13
c ---[1836]---> BDD-cost:   13
c ---[1833]---> BDD-cost:   13
c ---[1832]---> BDD-cost:   11
c ---[1831]---> BDD-cost:   12
c ---[1830]---> BDD-cost:   13
c ---[1829]---> BDD-cost:   11
c ---[1828]---> BDD-cost:   11
c ---[1825]---> BDD-cost:   13
c ---[1824]---> BDD-cost:   13
c ---[1823]---> BDD-cost:   13
c ---[1822]---> BDD-cost:   11
c ---[1821]---> BDD-cost:   13
c ---[1820]---> BDD-cost:   13
c ---[1819]---> BDD-cost:   12
c ---[1818]---> BDD-cost:   13
c ---[1817]---> BDD-cost:   11
c ---[1816]---> BDD-cost:   13
c ---[1814]---> BDD-cost:   12
c ---[1813]---> BDD-cost:   13
c ---[1811]---> BDD-cost:   13
c ---[1810]---> BDD-cost:   12
c ---[1809]---> BDD-cost:   11
c ---[1807]---> BDD-cost:   13
c ---[1806]---> BDD-cost:   12
c ---[1805]---> BDD-cost:   10
c ---[1804]---> BDD-cost:   11
c ---[1803]---> BDD-cost:   13
c ---[1802]---> BDD-cost:   13
c ---[1800]---> BDD-cost:   11
c ---[1799]---> BDD-cost:   13
c ---[1798]---> BDD-cost:   12
c ---[1797]---> BDD-cost:   13
c ---[1796]---> BDD-cost:   12
c ---[1795]---> BDD-cost:   12
c ---[1794]---> BDD-cost:   13
c ---[1793]---> BDD-cost:   13
c ---[1792]---> BDD-cost:   13
c ---[1791]---> BDD-cost:   13
c ---[1788]---> BDD-cost:   13
c ---[1786]---> BDD-cost:   12
c ---[1785]---> BDD-cost:   13
c ---[1783]---> BDD-cost:   11
c ---[1782]---> BDD-cost:   12
c ---[1781]---> BDD-cost:   12
c ---[1780]---> BDD-cost:   13
c ---[1779]---> BDD-cost:   13
c ---[1778]---> BDD-cost:   11
c ---[1777]---> BDD-cost:   13
c ---[1776]---> BDD-cost:   10
c ---[1775]---> BDD-cost:   13
c ---[1774]---> BDD-cost:   13
c ---[1773]---> BDD-cost:   13
c ---[1772]---> BDD-cost:   11
c ---[1771]---> BDD-cost:   13
c ---[1769]---> BDD-cost:   12
c ---[1766]---> BDD-cost:   13
c ---[1765]---> BDD-cost:   12
c ---[1764]---> BDD-cost:   13
c ---[1763]---> BDD-cost:   13
c ---[1762]---> BDD-cost:   11
c ---[1761]---> BDD-cost:   12
c ---[1760]---> BDD-cost:   13
c ---[1759]---> BDD-cost:   11
c ---[1758]---> BDD-cost:   12
c ---[1757]---> BDD-cost:   13
c ---[1755]---> BDD-cost:   13
c ---[1753]---> BDD-cost:   12
c ---[1752]---> BDD-cost:   13
c ---[1751]---> BDD-cost:   13
c ---[1750]---> BDD-cost:   12
c ---[1749]---> BDD-cost:   13
c ---[1748]---> BDD-cost:   13
c ---[1747]---> BDD-cost:   11
c ---[1746]---> BDD-cost:   13
c ---[1745]---> BDD-cost:   13
c ---[1744]---> BDD-cost:   13
c ---[1743]---> BDD-cost:   12
c ---[1741]---> BDD-cost:   12
c ---[1740]---> BDD-cost:   12
c ---[1739]---> BDD-cost:   13
c ---[1738]---> BDD-cost:   12
c ---[1737]---> BDD-cost:   12
c ---[1736]---> BDD-cost:   13
c ---[1735]---> BDD-cost:   13
c ---[1734]---> BDD-cost:   12
c ---[1732]---> BDD-cost:   12
c ---[1731]---> BDD-cost:   13
c ---[1730]---> BDD-cost:   13
c ---[1729]---> BDD-cost:   13
c ---[1728]---> BDD-cost:   13
c ---[1727]---> BDD-cost:   11
c ---[1725]---> BDD-cost:   13
c ---[1724]---> BDD-cost:   11
c ---[1723]---> BDD-cost:   12
c ---[1722]---> BDD-cost:   12
c ---[1721]---> BDD-cost:   11
c ---[1719]---> BDD-cost:   12
c ---[1717]---> BDD-cost:   13
c ---[1716]---> BDD-cost:   12
c ---[1715]---> BDD-cost:   13
c ---[1714]---> BDD-cost:   11
c ---[1713]---> BDD-cost:   12
c ---[1712]---> BDD-cost:   13
c ---[1711]---> BDD-cost:   12
c ---[1710]---> BDD-cost:   12
c ---[1709]---> BDD-cost:   13
c ---[1708]---> BDD-cost:   13
c ---[1707]---> BDD-cost:   12
c ---[1706]---> BDD-cost:   12
c ---[1705]---> BDD-cost:   13
c ---[1704]---> BDD-cost:   12
c ---[1702]---> BDD-cost:   71
c ---[1700]---> BDD-cost:   69
c ---[1699]---> BDD-cost:    7
c ---[1698]---> BDD-cost:    5
c ---[1697]---> BDD-cost:    8
c ---[1696]---> BDD-cost:    5
c ---[1695]---> BDD-cost:    6
c ---[1694]---> BDD-cost:    7
c ---[1693]---> BDD-cost:   14
c ---[1692]---> BDD-cost:    8
c ---[1691]---> BDD-cost:    7
c ---[1690]---> BDD-cost:    4
c ---[1689]---> BDD-cost:    7
c ---[1688]---> BDD-cost:    8
c ---[1687]---> BDD-cost:    6
c ---[1686]---> BDD-cost:    3
c ---[1685]---> BDD-cost:    7
c ---[1684]---> BDD-cost:    5
c ---[1683]---> BDD-cost:    7
c ---[1682]---> BDD-cost:   19
c ---[1681]---> BDD-cost:    6
c ---[1680]---> BDD-cost:    6
c ---[1679]---> BDD-cost:   16
c ---[1678]---> BDD-cost:    6
c ---[1677]---> BDD-cost:    8
c ---[1676]---> BDD-cost:    8
c ---[1675]---> BDD-cost:    6
c ---[1674]---> BDD-cost:    6
c ---[1673]---> BDD-cost:    5
c ---[1672]---> BDD-cost:    8
c ---[1671]---> BDD-cost:    7
c ---[1670]---> BDD-cost:   16
c ---[1669]---> BDD-cost:   17
c ---[1668]---> BDD-cost:   17
c ---[1667]---> BDD-cost:    7
c ---[1666]---> BDD-cost:    5
c ---[1665]---> BDD-cost:    5
c ---[1664]---> BDD-cost:    7
c ---[1663]---> BDD-cost:    5
c ---[1662]---> BDD-cost:    6
c ---[1661]---> BDD-cost:   14
c ---[1660]---> BDD-cost:    5
c ---[1659]---> BDD-cost:    8
c ---[1658]---> BDD-cost:    8
c ---[1657]---> BDD-cost:    4
c ---[1656]---> BDD-cost:    3
c ---[1655]---> BDD-cost:    8
c ---[1654]---> BDD-cost:    5
c ---[1653]---> BDD-cost:    6
c ---[1652]---> BDD-cost:    7
c ---[1651]---> BDD-cost:    6
c ---[1650]---> BDD-cost:    8
c ---[1649]---> BDD-cost:    4
c ---[1648]---> BDD-cost:   16
c ---[1647]---> BDD-cost:    3
c ---[1646]---> BDD-cost:   14
c ---[1645]---> BDD-cost:    7
c ---[1644]---> BDD-cost:   19
c ---[1643]---> BDD-cost:    8
c ---[1642]---> BDD-cost:    3
c ---[1641]---> BDD-cost:    5
c ---[1640]---> BDD-cost:    8
c ---[1639]---> BDD-cost:    7
c ---[1638]---> BDD-cost:    7
c ---[1637]---> BDD-cost:    5
c ---[1636]---> BDD-cost:    8
c ---[1635]---> BDD-cost:   19
c ---[1634]---> BDD-cost:    7
c ---[1633]---> BDD-cost:    8
c ---[1632]---> BDD-cost:    8
c ---[1631]---> BDD-cost:    6
c ---[1630]---> BDD-cost:    7
c ---[1629]---> BDD-cost:    5
c ---[1628]---> BDD-cost:    7
c ---[1627]---> BDD-cost:    6
c ---[1626]---> BDD-cost:    7
c ---[1625]---> BDD-cost:   14
c ---[1624]---> BDD-cost:    5
c ---[1623]---> BDD-cost:   14
c ---[1622]---> BDD-cost:    7
c ---[1621]---> BDD-cost:   19
c ---[1620]---> BDD-cost:    5
c ---[1619]---> BDD-cost:    8
c ---[1618]---> BDD-cost:    3
c ---[1617]---> BDD-cost:    8
c ---[1616]---> BDD-cost:    8
c ---[1615]---> BDD-cost:    6
c ---[1614]---> BDD-cost:    7
c ---[1613]---> BDD-cost:    6
c ---[1612]---> BDD-cost:    5
c ---[1611]---> BDD-cost:    4
c ---[1610]---> BDD-cost:   15
c ---[1609]---> BDD-cost:    6
c ---[1608]---> BDD-cost:    5
c ---[1607]---> BDD-cost:    6
c ---[1606]---> BDD-cost:    7
c ---[1605]---> BDD-cost:   17
c ---[1604]---> BDD-cost:   19
c ---[1603]---> BDD-cost:    6
c ---[1602]---> BDD-cost:    8
c ---[1601]---> BDD-cost:    6
c ---[1600]---> BDD-cost:    8
c ---[1599]---> BDD-cost:    7
c ---[1598]---> BDD-cost:    6
c ---[1597]---> BDD-cost:    7
c ---[1596]---> BDD-cost:    5
c ---[1595]---> BDD-cost:    8
c ---[1594]---> BDD-cost:    8
c ---[1593]---> BDD-cost:    7
c ---[1592]---> BDD-cost:    6
c ---[1591]---> BDD-cost:   15
c ---[1590]---> BDD-cost:    7
c ---[1588]---> BDD-cost:   73
c ---[1587]---> BDD-cost:    6
c ---[1586]---> BDD-cost:    8
c ---[1585]---> BDD-cost:    8
c ---[1584]---> BDD-cost:    7
c ---[1583]---> BDD-cost:    5
c ---[1582]---> BDD-cost:    8
c ---[1581]---> BDD-cost:    8
c ---[1580]---> BDD-cost:    6
c ---[1579]---> BDD-cost:    8
c ---[1578]---> BDD-cost:    4
c ---[1577]---> BDD-cost:    6
c ---[1576]---> BDD-cost:    6
c ---[1575]---> BDD-cost:   19
c ---[1574]---> BDD-cost:   19
c ---[1573]---> BDD-cost:    7
c ---[1572]---> BDD-cost:    6
c ---[1571]---> BDD-cost:    6
c ---[1570]---> BDD-cost:    8
c ---[1569]---> BDD-cost:    5
c ---[1568]---> BDD-cost:    7
c ---[1567]---> BDD-cost:    8
c ---[1566]---> BDD-cost:    7
c ---[1565]---> BDD-cost:    4
c ---[1564]---> BDD-cost:    8
c ---[1563]---> BDD-cost:    8
c ---[1562]---> BDD-cost:    5
c ---[1561]---> BDD-cost:    7
c ---[1560]---> BDD-cost:    3
c ---[1559]---> BDD-cost:    3
c ---[1558]---> BDD-cost:    8
c ---[1557]---> BDD-cost:    5
c ---[1556]---> BDD-cost:    8
c ---[1555]---> BDD-cost:    4
c ---[1554]---> BDD-cost:    4
c ---[1553]---> BDD-cost:    5
c ---[1552]---> BDD-cost:    6
c ---[1551]---> BDD-cost:    6
c ---[1550]---> BDD-cost:    8
c ---[1549]---> BDD-cost:    6
c ---[1548]---> BDD-cost:    6
c ---[1547]---> BDD-cost:    8
c ---[1546]---> BDD-cost:    5
c ---[1545]---> BDD-cost:    3
c ---[1544]---> BDD-cost:   19
c ---[1543]---> BDD-cost:    8
c ---[1542]---> BDD-cost:    5
c ---[1541]---> BDD-cost:   19
c ---[1540]---> BDD-cost:   19
c ---[1539]---> BDD-cost:    8
c ---[1538]---> BDD-cost:    8
c ---[1537]---> BDD-cost:    3
c ---[1536]---> BDD-cost:    8
c ---[1535]---> BDD-cost:    7
c ---[1534]---> BDD-cost:    6
c ---[1533]---> BDD-cost:    4
c ---[1532]---> BDD-cost:    7
c ---[1531]---> BDD-cost:    8
c ---[1530]---> BDD-cost:   15
c ---[1529]---> BDD-cost:    8
c ---[1528]---> BDD-cost:   17
c ---[1527]---> BDD-cost:    6
c ---[1526]---> BDD-cost:    4
c ---[1525]---> BDD-cost:    7
c ---[1524]---> BDD-cost:   19
c ---[1523]---> BDD-cost:    7
c ---[1522]---> BDD-cost:    7
c ---[1521]---> BDD-cost:    5
c ---[1520]---> BDD-cost:    8
c ---[1519]---> BDD-cost:    8
c ---[1518]---> BDD-cost:    6
c ---[1517]---> BDD-cost:    6
c ---[1516]---> BDD-cost:    8
c ---[1515]---> BDD-cost:    7
c ---[1514]---> BDD-cost:   19
c ---[1513]---> BDD-cost:    4
c ---[1512]---> BDD-cost:    6
c ---[1511]---> BDD-cost:    4
c ---[1510]---> BDD-cost:   15
c ---[1509]---> BDD-cost:    4
c ---[1508]---> BDD-cost:    8
c ---[1507]---> BDD-cost:    5
c ---[1506]---> BDD-cost:   18
c ---[1505]---> BDD-cost:    7
c ---[1504]---> BDD-cost:    6
c ---[1503]---> BDD-cost:    3
c ---[1502]---> BDD-cost:   17
c ---[1501]---> BDD-cost:    7
c ---[1500]---> BDD-cost:    3
c ---[1499]---> BDD-cost:    5
c ---[1498]---> BDD-cost:    7
c ---[1497]---> BDD-cost:    7
c ---[1496]---> BDD-cost:    8
c ---[1495]---> BDD-cost:   18
c ---[1494]---> BDD-cost:    7
c ---[1493]---> BDD-cost:    4
c ---[1492]---> BDD-cost:    8
c ---[1491]---> BDD-cost:    6
c ---[1490]---> BDD-cost:    5
c ---[1489]---> BDD-cost:    7
c ---[1488]---> BDD-cost:   16
c ---[1487]---> BDD-cost:    7
c ---[1486]---> BDD-cost:    6
c ---[1485]---> BDD-cost:   19
c ---[1484]---> BDD-cost:    6
c ---[1483]---> BDD-cost:    7
c ---[1482]---> BDD-cost:    7
c ---[1481]---> BDD-cost:    6
c ---[1480]---> BDD-cost:    5
c ---[1479]---> BDD-cost:    6
c ---[1478]---> BDD-cost:    3
c ---[1476]---> BDD-cost:   69
c ---[1475]---> BDD-cost:    5
c ---[1474]---> BDD-cost:    8
c ---[1473]---> BDD-cost:    6
c ---[1472]---> BDD-cost:    3
c ---[1471]---> BDD-cost:    5
c ---[1470]---> BDD-cost:    8
c ---[1469]---> BDD-cost:    6
c ---[1468]---> BDD-cost:   19
c ---[1467]---> BDD-cost:    5
c ---[1466]---> BDD-cost:    5
c ---[1465]---> BDD-cost:    8
c ---[1464]---> BDD-cost:    3
c ---[1463]---> BDD-cost:    7
c ---[1462]---> BDD-cost:    6
c ---[1461]---> BDD-cost:    7
c ---[1460]---> BDD-cost:    8
c ---[1459]---> BDD-cost:    7
c ---[1458]---> BDD-cost:   15
c ---[1457]---> BDD-cost:    6
c ---[1456]---> BDD-cost:    7
c ---[1455]---> BDD-cost:    4
c ---[1454]---> BDD-cost:    8
c ---[1453]---> BDD-cost:    7
c ---[1452]---> BDD-cost:    3
c ---[1451]---> BDD-cost:    5
c ---[1450]---> BDD-cost:    6
c ---[1449]---> BDD-cost:    6
c ---[1448]---> BDD-cost:    7
c ---[1447]---> BDD-cost:   18
c ---[1446]---> BDD-cost:    7
c ---[1445]---> BDD-cost:    6
c ---[1444]---> BDD-cost:    7
c ---[1443]---> BDD-cost:    8
c ---[1442]---> BDD-cost:    7
c ---[1441]---> BDD-cost:    3
c ---[1440]---> BDD-cost:    4
c ---[1439]---> BDD-cost:    8
c ---[1438]---> BDD-cost:    7
c ---[1437]---> BDD-cost:    5
c ---[1436]---> BDD-cost:    7
c ---[1435]---> BDD-cost:    6
c ---[1434]---> BDD-cost:    6
c ---[1433]---> BDD-cost:    5
c ---[1432]---> BDD-cost:    6
c ---[1431]---> BDD-cost:    7
c ---[1430]---> BDD-cost:    7
c ---[1429]---> BDD-cost:    7
c ---[1428]---> BDD-cost:   19
c ---[1427]---> BDD-cost:    6
c ---[1426]---> BDD-cost:    6
c ---[1425]---> BDD-cost:    4
c ---[1424]---> BDD-cost:    8
c ---[1423]---> BDD-cost:    6
c ---[1422]---> BDD-cost:    8
c ---[1421]---> BDD-cost:    8
c ---[1420]---> BDD-cost:    8
c ---[1419]---> BDD-cost:   17
c ---[1418]---> BDD-cost:    7
c ---[1417]---> BDD-cost:    3
c ---[1416]---> BDD-cost:   17
c ---[1415]---> BDD-cost:    3
c ---[1414]---> BDD-cost:    7
c ---[1413]---> BDD-cost:   16
c ---[1412]---> BDD-cost:    5
c ---[1411]---> BDD-cost:    5
c ---[1410]---> BDD-cost:    7
c ---[1409]---> BDD-cost:    7
c ---[1408]---> BDD-cost:    8
c ---[1407]---> BDD-cost:    8
c ---[1406]---> BDD-cost:    8
c ---[1405]---> BDD-cost:    5
c ---[1404]---> BDD-cost:    3
c ---[1403]---> BDD-cost:   19
c ---[1402]---> BDD-cost:    7
c ---[1401]---> BDD-cost:    6
c ---[1400]---> BDD-cost:    3
c ---[1399]---> BDD-cost:    6
c ---[1398]---> BDD-cost:    7
c ---[1397]---> BDD-cost:    8
c ---[1396]---> BDD-cost:    7
c ---[1395]---> BDD-cost:    7
c ---[1394]---> BDD-cost:    7
c ---[1393]---> BDD-cost:    6
c ---[1392]---> BDD-cost:    8
c ---[1391]---> BDD-cost:   15
c ---[1390]---> BDD-cost:    7
c ---[1389]---> BDD-cost:    7
c ---[1388]---> BDD-cost:    6
c ---[1387]---> BDD-cost:    7
c ---[1386]---> BDD-cost:   18
c ---[1385]---> BDD-cost:    7
c ---[1384]---> BDD-cost:    5
c ---[1383]---> BDD-cost:    7
c ---[1382]---> BDD-cost:    8
c ---[1381]---> BDD-cost:    7
c ---[1380]---> BDD-cost:    7
c ---[1379]---> BDD-cost:    8
c ---[1378]---> BDD-cost:    5
c ---[1377]---> BDD-cost:    7
c ---[1376]---> BDD-cost:    6
c ---[1375]---> BDD-cost:    6
c ---[1374]---> BDD-cost:    6
c ---[1373]---> BDD-cost:   19
c ---[1372]---> BDD-cost:    6
c ---[1371]---> BDD-cost:    7
c ---[1370]---> BDD-cost:    6
c ---[1369]---> BDD-cost:    7
c ---[1368]---> BDD-cost:   16
c ---[1367]---> BDD-cost:   18
c ---[1366]---> BDD-cost:   19
c ---[1364]---> BDD-cost:   65
c ---[1363]---> BDD-cost:    8
c ---[1362]---> BDD-cost:    6
c ---[1361]---> BDD-cost:   18
c ---[1360]---> BDD-cost:    3
c ---[1359]---> BDD-cost:   17
c ---[1358]---> BDD-cost:    7
c ---[1357]---> BDD-cost:    8
c ---[1356]---> BDD-cost:    8
c ---[1355]---> BDD-cost:    7
c ---[1354]---> BDD-cost:    7
c ---[1353]---> BDD-cost:   19
c ---[1352]---> BDD-cost:    3
c ---[1351]---> BDD-cost:    4
c ---[1350]---> BDD-cost:    8
c ---[1349]---> BDD-cost:   16
c ---[1348]---> BDD-cost:    8
c ---[1347]---> BDD-cost:    7
c ---[1346]---> BDD-cost:    8
c ---[1345]---> BDD-cost:    6
c ---[1344]---> BDD-cost:    5
c ---[1343]---> BDD-cost:    6
c ---[1342]---> BDD-cost:    8
c ---[1341]---> BDD-cost:    6
c ---[1340]---> BDD-cost:    8
c ---[1339]---> BDD-cost:    6
c ---[1338]---> BDD-cost:    8
c ---[1337]---> BDD-cost:    8
c ---[1336]---> BDD-cost:    5
c ---[1335]---> BDD-cost:    6
c ---[1334]---> BDD-cost:    6
c ---[1333]---> BDD-cost:   15
c ---[1332]---> BDD-cost:    4
c ---[1331]---> BDD-cost:    7
c ---[1330]---> BDD-cost:    8
c ---[1329]---> BDD-cost:    6
c ---[1328]---> BDD-cost:    7
c ---[1327]---> BDD-cost:    6
c ---[1326]---> BDD-cost:    3
c ---[1325]---> BDD-cost:    6
c ---[1324]---> BDD-cost:    3
c ---[1323]---> BDD-cost:    5
c ---[1322]---> BDD-cost:    3
c ---[1321]---> BDD-cost:    7
c ---[1320]---> BDD-cost:    3
c ---[1319]---> BDD-cost:    6
c ---[1318]---> BDD-cost:    7
c ---[1317]---> BDD-cost:    3
c ---[1316]---> BDD-cost:    3
c ---[1315]---> BDD-cost:    6
c ---[1314]---> BDD-cost:    6
c ---[1313]---> BDD-cost:    6
c ---[1312]---> BDD-cost:    6
c ---[1311]---> BDD-cost:    8
c ---[1310]---> BDD-cost:    7
c ---[1309]---> BDD-cost:    7
c ---[1308]---> BDD-cost:    6
c ---[1307]---> BDD-cost:    7
c ---[1306]---> BDD-cost:    7
c ---[1305]---> BDD-cost:    8
c ---[1304]---> BDD-cost:    6
c ---[1303]---> BDD-cost:    3
c ---[1302]---> BDD-cost:    7
c ---[1301]---> BDD-cost:    7
c ---[1300]---> BDD-cost:    5
c ---[1299]---> BDD-cost:    6
c ---[1298]---> BDD-cost:   16
c ---[1297]---> BDD-cost:    5
c ---[1296]---> BDD-cost:    5
c ---[1295]---> BDD-cost:    5
c ---[1294]---> BDD-cost:    8
c ---[1293]---> BDD-cost:    7
c ---[1292]---> BDD-cost:   17
c ---[1291]---> BDD-cost:    6
c ---[1290]---> BDD-cost:    8
c ---[1289]---> BDD-cost:   17
c ---[1288]---> BDD-cost:   17
c ---[1287]---> BDD-cost:   19
c ---[1286]---> BDD-cost:    8
c ---[1285]---> BDD-cost:    8
c ---[1284]---> BDD-cost:    6
c ---[1283]---> BDD-cost:    5
c ---[1282]---> BDD-cost:    5
c ---[1281]---> BDD-cost:    8
c ---[1280]---> BDD-cost:    6
c ---[1279]---> BDD-cost:    8
c ---[1278]---> BDD-cost:    5
c ---[1277]---> BDD-cost:   19
c ---[1276]---> BDD-cost:   19
c ---[1275]---> BDD-cost:    5
c ---[1274]---> BDD-cost:   15
c ---[1273]---> BDD-cost:    8
c ---[1272]---> BDD-cost:    8
c ---[1271]---> BDD-cost:    7
c ---[1270]---> BDD-cost:    6
c ---[1269]---> BDD-cost:    3
c ---[1268]---> BDD-cost:    8
c ---[1267]---> BDD-cost:    7
c ---[1266]---> BDD-cost:    7
c ---[1265]---> BDD-cost:    5
c ---[1264]---> BDD-cost:    6
c ---[1263]---> BDD-cost:    4
c ---[1262]---> BDD-cost:    7
c ---[1261]---> BDD-cost:   17
c ---[1260]---> BDD-cost:    7
c ---[1259]---> BDD-cost:    7
c ---[1258]---> BDD-cost:    4
c ---[1257]---> BDD-cost:   17
c ---[1256]---> BDD-cost:    6
c ---[1255]---> BDD-cost:    7
c ---[1254]---> BDD-cost:    8
c ---[1252]---> BDD-cost:   73
c ---[1251]---> BDD-cost:   19
c ---[1250]---> BDD-cost:   19
c ---[1249]---> BDD-cost:    3
c ---[1248]---> BDD-cost:    6
c ---[1247]---> BDD-cost:    8
c ---[1246]---> BDD-cost:    3
c ---[1245]---> BDD-cost:    6
c ---[1244]---> BDD-cost:    7
c ---[1243]---> BDD-cost:   17
c ---[1242]---> BDD-cost:    7
c ---[1241]---> BDD-cost:    5
c ---[1240]---> BDD-cost:    8
c ---[1239]---> BDD-cost:    3
c ---[1238]---> BDD-cost:    8
c ---[1237]---> BDD-cost:    8
c ---[1236]---> BDD-cost:    7
c ---[1235]---> BDD-cost:    6
c ---[1234]---> BDD-cost:    6
c ---[1233]---> BDD-cost:   19
c ---[1232]---> BDD-cost:    7
c ---[1231]---> BDD-cost:    8
c ---[1230]---> BDD-cost:    7
c ---[1229]---> BDD-cost:    5
c ---[1228]---> BDD-cost:    6
c ---[1227]---> BDD-cost:    8
c ---[1226]---> BDD-cost:   19
c ---[1225]---> BDD-cost:   15
c ---[1224]---> BDD-cost:    8
c ---[1223]---> BDD-cost:    6
c ---[1222]---> BDD-cost:    6
c ---[1221]---> BDD-cost:    8
c ---[1220]---> BDD-cost:    3
c ---[1219]---> BDD-cost:    6
c ---[1218]---> BDD-cost:    6
c ---[1217]---> BDD-cost:    6
c ---[1216]---> BDD-cost:    7
c ---[1215]---> BDD-cost:    8
c ---[1214]---> BDD-cost:    6
c ---[1213]---> BDD-cost:    6
c ---[1212]---> BDD-cost:    8
c ---[1211]---> BDD-cost:   15
c ---[1210]---> BDD-cost:    5
c ---[1209]---> BDD-cost:    5
c ---[1208]---> BDD-cost:    8
c ---[1207]---> BDD-cost:    7
c ---[1206]---> BDD-cost:   17
c ---[1205]---> BDD-cost:    6
c ---[1204]---> BDD-cost:    7
c ---[1203]---> BDD-cost:    8
c ---[1202]---> BDD-cost:    7
c ---[1201]---> BDD-cost:    8
c ---[1200]---> BDD-cost:    8
c ---[1199]---> BDD-cost:    6
c ---[1197]---> BDD-cost:   67
c ---[1196]---> BDD-cost:    6
c ---[1195]---> BDD-cost:    6
c ---[1194]---> BDD-cost:    5
c ---[1193]---> BDD-cost:    6
c ---[1192]---> BDD-cost:   17
c ---[1191]---> BDD-cost:   16
c ---[1190]---> BDD-cost:    8
c ---[1189]---> BDD-cost:    5
c ---[1188]---> BDD-cost:    3
c ---[1187]---> BDD-cost:    8
c ---[1185]---> BDD-cost:   65
c ---[1184]---> BDD-cost:    6
c ---[1183]---> BDD-cost:    7
c ---[1182]---> BDD-cost:    7
c ---[1181]---> BDD-cost:    5
c ---[1180]---> BDD-cost:    6
c ---[1179]---> BDD-cost:    6
c ---[1178]---> BDD-cost:    7
c ---[1177]---> BDD-cost:   15
c ---[1176]---> BDD-cost:    6
c ---[1175]---> BDD-cost:    6
c ---[1173]---> BDD-cost:   65
c ---[1172]---> BDD-cost:    4
c ---[1171]---> BDD-cost:    8
c ---[1170]---> BDD-cost:    3
c ---[1169]---> BDD-cost:    8
c ---[1168]---> BDD-cost:    7
c ---[1167]---> BDD-cost:   15
c ---[1166]---> BDD-cost:    5
c ---[1165]---> BDD-cost:    6
c ---[1164]---> BDD-cost:    7
c ---[1163]---> BDD-cost:    4
c ---[1161]---> BDD-cost:   67
c ---[1160]---> BDD-cost:   17
c ---[1159]---> BDD-cost:    7
c ---[1158]---> BDD-cost:    6
c ---[1157]---> BDD-cost:   19
c ---[1156]---> BDD-cost:    7
c ---[1155]---> BDD-cost:    3
c ---[1154]---> BDD-cost:    6
c ---[1153]---> BDD-cost:   19
c ---[1152]---> BDD-cost:    3
c ---[1151]---> BDD-cost:    7
c ---[1149]---> BDD-cost:   67
c ---[1148]---> BDD-cost:    7
c ---[1147]---> BDD-cost:    3
c ---[1146]---> BDD-cost:    3
c ---[1145]---> BDD-cost:   15
c ---[1144]---> BDD-cost:    7
c ---[1143]---> BDD-cost:   15
c ---[1142]---> BDD-cost:    5
c ---[1141]---> BDD-cost:    8
c ---[1140]---> BDD-cost:   14
c ---[1139]---> BDD-cost:    6
c ---[1137]---> BDD-cost:   71
c ---[1135]---> BDD-cost:   65
c ---[1134]---> BDD-cost:   15
c ---[1133]---> BDD-cost:    7
c ---[1132]---> BDD-cost:    8
c ---[1131]---> BDD-cost:    8
c ---[1130]---> BDD-cost:    5
c ---[1129]---> BDD-cost:    7
c ---[1128]---> BDD-cost:    7
c ---[1127]---> BDD-cost:    7
c ---[1126]---> BDD-cost:    5
c ---[1125]---> BDD-cost:    3
c ---[1123]---> BDD-cost:   69
c ---[1122]---> BDD-cost:    7
c ---[1121]---> BDD-cost:   15
c ---[1120]---> BDD-cost:    8
c ---[1119]---> BDD-cost:    5
c ---[1118]---> BDD-cost:    3
c ---[1117]---> BDD-cost:    6
c ---[1116]---> BDD-cost:    3
c ---[1115]---> BDD-cost:    4
c ---[1114]---> BDD-cost:    6
c ---[1113]---> BDD-cost:    5
c ---[1111]---> BDD-cost:   69
c ---[1110]---> BDD-cost:    7
c ---[1109]---> BDD-cost:    5
c ---[1108]---> BDD-cost:    7
c ---[1107]---> BDD-cost:    8
c ---[1106]---> BDD-cost:    5
c ---[1105]---> BDD-cost:    5
c ---[1104]---> BDD-cost:    6
c ---[1103]---> BDD-cost:    7
c ---[1102]---> BDD-cost:    6
c ---[1101]---> BDD-cost:    7
c ---[1099]---> BDD-cost:   69
c ---[1098]---> BDD-cost:    7
c ---[1097]---> BDD-cost:    4
c ---[1096]---> BDD-cost:    7
c ---[1095]---> BDD-cost:    3
c ---[1094]---> BDD-cost:   18
c ---[1093]---> BDD-cost:    8
c ---[1092]---> BDD-cost:    5
c ---[1091]---> BDD-cost:    4
c ---[1090]---> BDD-cost:    6
c ---[1089]---> BDD-cost:    4
c ---[1087]---> BDD-cost:   67
c ---[1086]---> BDD-cost:    7
c ---[1085]---> BDD-cost:    6
c ---[1084]---> BDD-cost:    6
c ---[1083]---> BDD-cost:   17
c ---[1082]---> BDD-cost:    8
c ---[1081]---> BDD-cost:   19
c ---[1080]---> BDD-cost:    5
c ---[1079]---> BDD-cost:    5
c ---[1078]---> BDD-cost:   17
c ---[1077]---> BDD-cost:    3
c ---[1075]---> BDD-cost:   63
c ---[1074]---> BDD-cost:    8
c ---[1073]---> BDD-cost:    5
c ---[1072]---> BDD-cost:    7
c ---[1071]---> BDD-cost:    6
c ---[1070]---> BDD-cost:    7
c ---[1069]---> BDD-cost:    8
c ---[1068]---> BDD-cost:   16
c ---[1067]---> BDD-cost:    7
c ---[1066]---> BDD-cost:    6
c ---[1065]---> BDD-cost:    7
c ---[1063]---> BDD-cost:   65
c ---[1062]---> BDD-cost:    7
c ---[1061]---> BDD-cost:    7
c ---[1060]---> BDD-cost:    6
c ---[1059]---> BDD-cost:    7
c ---[1058]---> BDD-cost:    7
c ---[1057]---> BDD-cost:    7
c ---[1056]---> BDD-cost:    6
c ---[1055]---> BDD-cost:    7
c ---[1054]---> BDD-cost:    7
c ---[1053]---> BDD-cost:    7
c ---[1051]---> BDD-cost:   63
c ---[1050]---> BDD-cost:    7
c ---[1049]---> BDD-cost:    7
c ---[1048]---> BDD-cost:    7
c ---[1047]---> BDD-cost:    3
c ---[1046]---> BDD-cost:    8
c ---[1045]---> BDD-cost:    4
c ---[1044]---> BDD-cost:   18
c ---[1043]---> BDD-cost:    4
c ---[1042]---> BDD-cost:    8
c ---[1041]---> BDD-cost:    7
c ---[1039]---> BDD-cost:   63
c ---[1038]---> BDD-cost:   18
c ---[1037]---> BDD-cost:    4
c ---[1036]---> BDD-cost:    7
c ---[1035]---> BDD-cost:    7
c ---[1034]---> BDD-cost:    5
c ---[1033]---> BDD-cost:    5
c ---[1032]---> BDD-cost:    6
c ---[1031]---> BDD-cost:    8
c ---[1030]---> BDD-cost:   16
c ---[1029]---> BDD-cost:   19
c ---[1027]---> BDD-cost:   71
c ---[1026]---> BDD-cost:    6
c ---[1025]---> BDD-cost:    7
c ---[1024]---> BDD-cost:    3
c ---[1023]---> BDD-cost:   19
c ---[1022]---> BDD-cost:    8
c ---[1021]---> BDD-cost:    8
c ---[1020]---> BDD-cost:    6
c ---[1019]---> BDD-cost:    3
c ---[1018]---> BDD-cost:   16
c ---[1017]---> BDD-cost:    8
c ---[1015]---> BDD-cost:   69
c ---[1013]---> BDD-cost:   67
c ---[1012]---> BDD-cost:    4
c ---[1011]---> BDD-cost:    6
c ---[1010]---> BDD-cost:    8
c ---[1009]---> BDD-cost:    8
c ---[1008]---> BDD-cost:    8
c ---[1007]---> BDD-cost:    7
c ---[1006]---> BDD-cost:    7
c ---[1005]---> BDD-cost:    7
c ---[1004]---> BDD-cost:    8
c ---[1003]---> BDD-cost:    4
c ---[1001]---> BDD-cost:   65
c ---[1000]---> BDD-cost:    8
c ---[ 999]---> BDD-cost:    7
c ---[ 998]---> BDD-cost:    7
c ---[ 997]---> BDD-cost:    8
c ---[ 996]---> BDD-cost:    7
c ---[ 995]---> BDD-cost:    7
c ---[ 994]---> BDD-cost:    7
c ---[ 993]---> BDD-cost:    3
c ---[ 992]---> BDD-cost:    7
c ---[ 991]---> BDD-cost:    6
c ---[ 989]---> BDD-cost:   71
c ---[ 988]---> BDD-cost:    3
c ---[ 987]---> BDD-cost:    6
c ---[ 986]---> BDD-cost:    8
c ---[ 985]---> BDD-cost:    6
c ---[ 984]---> BDD-cost:    7
c ---[ 983]---> BDD-cost:    7
c ---[ 982]---> BDD-cost:    6
c ---[ 981]---> BDD-cost:   17
c ---[ 980]---> BDD-cost:    7
c ---[ 979]---> BDD-cost:    6
c ---[ 977]---> BDD-cost:   73
c ---[ 976]---> BDD-cost:    3
c ---[ 975]---> BDD-cost:    5
c ---[ 974]---> BDD-cost:    5
c ---[ 973]---> BDD-cost:    6
c ---[ 972]---> BDD-cost:    5
c ---[ 971]---> BDD-cost:    8
c ---[ 970]---> BDD-cost:   17
c ---[ 969]---> BDD-cost:   17
c ---[ 968]---> BDD-cost:    8
c ---[ 967]---> BDD-cost:    5
c ---[ 965]---> BDD-cost:   71
c ---[ 964]---> BDD-cost:    6
c ---[ 963]---> BDD-cost:    6
c ---[ 962]---> BDD-cost:    5
c ---[ 961]---> BDD-cost:    8
c ---[ 960]---> BDD-cost:    6
c ---[ 959]---> BDD-cost:    6
c ---[ 958]---> BDD-cost:    3
c ---[ 957]---> BDD-cost:    6
c ---[ 956]---> BDD-cost:    6
c ---[ 955]---> BDD-cost:    7
c ---[ 953]---> BDD-cost:   69
c ---[ 952]---> BDD-cost:    7
c ---[ 951]---> BDD-cost:    5
c ---[ 950]---> BDD-cost:    7
c ---[ 949]---> BDD-cost:    8
c ---[ 948]---> BDD-cost:    6
c ---[ 947]---> BDD-cost:    5
c ---[ 946]---> BDD-cost:    8
c ---[ 945]---> BDD-cost:    8
c ---[ 944]---> BDD-cost:    3
c ---[ 943]---> BDD-cost:    6
c ---[ 941]---> BDD-cost:   67
c ---[ 940]---> BDD-cost:    6
c ---[ 939]---> BDD-cost:    8
c ---[ 938]---> BDD-cost:    7
c ---[ 937]---> BDD-cost:    8
c ---[ 936]---> BDD-cost:   19
c ---[ 935]---> BDD-cost:    7
c ---[ 934]---> BDD-cost:    5
c ---[ 933]---> BDD-cost:   15
c ---[ 932]---> BDD-cost:    7
c ---[ 931]---> BDD-cost:    8
c ---[ 929]---> BDD-cost:   63
c ---[ 928]---> BDD-cost:    8
c ---[ 927]---> BDD-cost:    8
c ---[ 926]---> BDD-cost:    5
c ---[ 925]---> BDD-cost:    3
c ---[ 924]---> BDD-cost:   17
c ---[ 923]---> BDD-cost:   19
c ---[ 922]---> BDD-cost:    3
c ---[ 921]---> BDD-cost:    8
c ---[ 920]---> BDD-cost:    7
c ---[ 919]---> BDD-cost:   19
c ---[ 917]---> BDD-cost:   63
c ---[ 916]---> BDD-cost:    3
c ---[ 915]---> BDD-cost:    7
c ---[ 914]---> BDD-cost:    6
c ---[ 913]---> BDD-cost:    6
c ---[ 912]---> BDD-cost:    8
c ---[ 911]---> BDD-cost:    3
c ---[ 910]---> BDD-cost:    7
c ---[ 909]---> BDD-cost:    7
c ---[ 908]---> BDD-cost:    8
c ---[ 907]---> BDD-cost:    7
c ---[ 905]---> BDD-cost:   57
c ---[ 904]---> BDD-cost:    4
c ---[ 903]---> BDD-cost:    4
c ---[ 902]---> BDD-cost:    7
c ---[ 901]---> BDD-cost:    6
c ---[ 900]---> BDD-cost:    6
c ---[ 899]---> BDD-cost:    5
c ---[ 898]---> BDD-cost:   17
c ---[ 897]---> BDD-cost:    7
c ---[ 896]---> BDD-cost:   14
c ---[ 895]---> BDD-cost:    7
c ---[ 893]---> BDD-cost:   57
c ---[ 891]---> Adder-cost: 1754   maxlim: 361947   bits: 20/19
c ---[ 890]---> BDD-cost:    8
c ---[ 889]---> BDD-cost:    6
c ---[ 888]---> BDD-cost:    7
c ---[ 887]---> BDD-cost:    7
c ---[ 886]---> BDD-cost:    8
c ---[ 885]---> BDD-cost:    8
c ---[ 884]---> BDD-cost:    3
c ---[ 883]---> BDD-cost:   18
c ---[ 882]---> BDD-cost:    8
c ---[ 881]---> BDD-cost:    7
c ---[ 879]---> Adder-cost: 1886   maxlim: 393051   bits: 20/19
c ---[ 878]---> BDD-cost:    4
c ---[ 877]---> BDD-cost:   18
c ---[ 876]---> BDD-cost:    5
c ---[ 875]---> BDD-cost:    3
c ---[ 874]---> BDD-cost:    5
c ---[ 873]---> BDD-cost:    7
c ---[ 872]---> BDD-cost:    8
c ---[ 871]---> BDD-cost:    7
c ---[ 870]---> BDD-cost:    6
c ---[ 869]---> BDD-cost:    5
c ---[ 867]---> Adder-cost: 1892   maxlim: 407260   bits: 20/19
c ---[ 866]---> BDD-cost:    6
c ---[ 865]---> BDD-cost:    3
c ---[ 864]---> BDD-cost:    3
c ---[ 863]---> BDD-cost:    3
c ---[ 862]---> BDD-cost:   17
c ---[ 861]---> BDD-cost:    6
c ---[ 860]---> BDD-cost:    3
c ---[ 859]---> BDD-cost:    8
c ---[ 858]---> BDD-cost:   16
c ---[ 857]---> BDD-cost:   16
c ---[ 855]---> Adder-cost: 1620   maxlim: 292194   bits: 20/19
c ---[ 854]---> BDD-cost:    7
c ---[ 853]---> BDD-cost:    8
c ---[ 852]---> BDD-cost:    8
c ---[ 851]---> BDD-cost:    5
c ---[ 850]---> BDD-cost:   15
c ---[ 849]---> BDD-cost:    5
c ---[ 848]---> BDD-cost:   19
c ---[ 847]---> BDD-cost:    7
c ---[ 846]---> BDD-cost:    8
c ---[ 845]---> BDD-cost:    6
c ---[ 843]---> Adder-cost: 1716   maxlim: 400605   bits: 20/19
c ---[ 842]---> BDD-cost:    8
c ---[ 841]---> BDD-cost:    6
c ---[ 840]---> BDD-cost:    8
c ---[ 839]---> BDD-cost:    6
c ---[ 838]---> BDD-cost:    7
c ---[ 837]---> BDD-cost:    3
c ---[ 836]---> BDD-cost:    7
c ---[ 835]---> BDD-cost:    5
c ---[ 834]---> BDD-cost:    7
c ---[ 833]---> BDD-cost:   18
c ---[ 831]---> Adder-cost: 1880   maxlim: 441181   bits: 20/19
c ---[ 830]---> BDD-cost:    5
c ---[ 829]---> BDD-cost:    7
c ---[ 828]---> BDD-cost:    3
c ---[ 827]---> BDD-cost:   18
c ---[ 826]---> BDD-cost:    4
c ---[ 825]---> BDD-cost:    6
c ---[ 824]---> BDD-cost:   19
c ---[ 823]---> BDD-cost:    5
c ---[ 822]---> BDD-cost:   16
c ---[ 821]---> BDD-cost:    5
c ---[ 819]---> Adder-cost: 1650   maxlim: 327391   bits: 20/19
c ---[ 818]---> BDD-cost:    7
c ---[ 817]---> BDD-cost:    8
c ---[ 816]---> BDD-cost:    7
c ---[ 815]---> BDD-cost:    5
c ---[ 814]---> BDD-cost:    7
c ---[ 813]---> BDD-cost:    7
c ---[ 812]---> BDD-cost:    7
c ---[ 811]---> BDD-cost:    8
c ---[ 810]---> BDD-cost:    6
c ---[ 809]---> BDD-cost:    3
c ---[ 807]---> Adder-cost: 1934   maxlim: 418779   bits: 20/19
c ---[ 806]---> BDD-cost:    5
c ---[ 805]---> BDD-cost:    7
c ---[ 804]---> BDD-cost:    3
c ---[ 803]---> BDD-cost:   15
c ---[ 802]---> BDD-cost:    5
c ---[ 801]---> BDD-cost:    4
c ---[ 800]---> BDD-cost:    7
c ---[ 799]---> BDD-cost:    7
c ---[ 798]---> BDD-cost:    7
c ---[ 797]---> BDD-cost:   17
c ---[ 795]---> Adder-cost: 1654   maxlim: 324318   bits: 20/19
c ---[ 794]---> BDD-cost:    7
c ---[ 793]---> BDD-cost:    8
c ---[ 792]---> BDD-cost:   15
c ---[ 791]---> BDD-cost:    7
c ---[ 790]---> BDD-cost:    7
c ---[ 789]---> BDD-cost:    6
c ---[ 788]---> BDD-cost:    3
c ---[ 787]---> BDD-cost:    8
c ---[ 786]---> BDD-cost:    5
c ---[ 785]---> BDD-cost:    5
c ---[ 783]---> Adder-cost: 1880   maxlim: 361692   bits: 20/19
c ---[ 782]---> BDD-cost:    8
c ---[ 781]---> BDD-cost:    7
c ---[ 780]---> BDD-cost:   15
c ---[ 779]---> BDD-cost:    7
c ---[ 778]---> BDD-cost:    3
c ---[ 777]---> BDD-cost:    7
c ---[ 776]---> BDD-cost:    6
c ---[ 775]---> BDD-cost:    7
c ---[ 774]---> BDD-cost:    5
c ---[ 773]---> BDD-cost:   16
c ---[ 771]---> BDD-cost:   67
c ---[ 769]---> Adder-cost: 1756   maxlim: 412890   bits: 20/19
c ---[ 768]---> BDD-cost:    7
c ---[ 767]---> BDD-cost:    7
c ---[ 766]---> BDD-cost:    8
c ---[ 765]---> BDD-cost:    7
c ---[ 764]---> BDD-cost:    4
c ---[ 763]---> BDD-cost:    6
c ---[ 762]---> BDD-cost:    6
c ---[ 761]---> BDD-cost:    5
c ---[ 760]---> BDD-cost:    7
c ---[ 759]---> BDD-cost:    3
c ---[ 757]---> Adder-cost: 1806   maxlim: 375900   bits: 20/19
c ---[ 756]---> BDD-cost:    6
c ---[ 755]---> BDD-cost:   18
c ---[ 754]---> BDD-cost:    6
c ---[ 753]---> BDD-cost:    7
c ---[ 752]---> BDD-cost:    6
c ---[ 751]---> BDD-cost:    5
c ---[ 750]---> BDD-cost:    7
c ---[ 749]---> BDD-cost:    5
c ---[ 748]---> BDD-cost:    8
c ---[ 747]---> BDD-cost:    4
c ---[ 745]---> Adder-cost: 1784   maxlim: 382686   bits: 20/19
c ---[ 744]---> BDD-cost:    7
c ---[ 743]---> BDD-cost:    5
c ---[ 742]---> BDD-cost:    4
c ---[ 741]---> BDD-cost:    6
c ---[ 740]---> BDD-cost:    8
c ---[ 739]---> BDD-cost:    5
c ---[ 738]---> BDD-cost:    5
c ---[ 737]---> BDD-cost:    8
c ---[ 736]---> BDD-cost:    7
c ---[ 735]---> BDD-cost:    6
c ---[ 733]---> Adder-cost: 1754   maxlim: 367962   bits: 20/19
c ---[ 732]---> BDD-cost:    3
c ---[ 731]---> BDD-cost:    6
c ---[ 730]---> BDD-cost:   15
c ---[ 729]---> BDD-cost:    8
c ---[ 728]---> BDD-cost:    8
c ---[ 727]---> BDD-cost:    5
c ---[ 726]---> BDD-cost:    7
c ---[ 725]---> BDD-cost:    6
c ---[ 724]---> BDD-cost:    8
c ---[ 723]---> BDD-cost:    8
c ---[ 721]---> Adder-cost: 1792   maxlim: 372061   bits: 20/19
c ---[ 720]---> BDD-cost:    8
c ---[ 719]---> BDD-cost:   17
c ---[ 718]---> BDD-cost:   19
c ---[ 717]---> BDD-cost:    6
c ---[ 716]---> BDD-cost:   15
c ---[ 715]---> BDD-cost:   15
c ---[ 714]---> BDD-cost:    8
c ---[ 713]---> BDD-cost:    3
c ---[ 712]---> BDD-cost:    7
c ---[ 711]---> BDD-cost:    6
c ---[ 709]---> Adder-cost: 1648   maxlim: 339038   bits: 20/19
c ---[ 708]---> BDD-cost:    8
c ---[ 707]---> BDD-cost:   19
c ---[ 706]---> BDD-cost:    8
c ---[ 705]---> BDD-cost:    5
c ---[ 704]---> BDD-cost:    3
c ---[ 703]---> BDD-cost:   16
c ---[ 702]---> BDD-cost:    5
c ---[ 701]---> BDD-cost:    7
c ---[ 700]---> BDD-cost:    6
c ---[ 699]---> BDD-cost:    5
c ---[ 697]---> Adder-cost: 1748   maxlim: 336990   bits: 20/19
c ---[ 696]---> BDD-cost:   16
c ---[ 695]---> BDD-cost:    8
c ---[ 694]---> BDD-cost:   14
c ---[ 693]---> BDD-cost:    7
c ---[ 692]---> BDD-cost:    4
c ---[ 691]---> BDD-cost:    6
c ---[ 690]---> BDD-cost:    7
c ---[ 689]---> BDD-cost:    8
c ---[ 688]---> BDD-cost:    7
c ---[ 687]---> BDD-cost:    5
c ---[ 685]---> Adder-cost: 1868   maxlim: 363997   bits: 20/19
c ---[ 684]---> BDD-cost:    4
c ---[ 683]---> BDD-cost:    7
c ---[ 682]---> BDD-cost:    4
c ---[ 681]---> BDD-cost:   19
c ---[ 680]---> BDD-cost:    6
c ---[ 679]---> BDD-cost:    6
c ---[ 678]---> BDD-cost:    8
c ---[ 677]---> BDD-cost:    7
c ---[ 676]---> BDD-cost:    4
c ---[ 675]---> BDD-cost:    6
c ---[ 673]---> Adder-cost: 1862   maxlim: 388829   bits: 20/19
c ---[ 672]---> BDD-cost:    6
c ---[ 671]---> BDD-cost:   19
c ---[ 670]---> BDD-cost:   15
c ---[ 669]---> BDD-cost:    5
c ---[ 668]---> BDD-cost:    6
c ---[ 667]---> BDD-cost:   19
c ---[ 666]---> BDD-cost:    5
c ---[ 665]---> BDD-cost:    7
c ---[ 664]---> BDD-cost:    7
c ---[ 663]---> BDD-cost:    6
c ---[ 661]---> Adder-cost: 1812   maxlim: 376286   bits: 20/19
c ---[ 660]---> BDD-cost:    6
c ---[ 659]---> BDD-cost:    8
c ---[ 658]---> BDD-cost:    7
c ---[ 657]---> BDD-cost:   19
c ---[ 656]---> BDD-cost:    5
c ---[ 655]---> BDD-cost:    8
c ---[ 654]---> BDD-cost:    7
c ---[ 653]---> BDD-cost:    4
c ---[ 652]---> BDD-cost:    8
c ---[ 651]---> BDD-cost:    7
c ---[ 649]---> BDD-cost:   67
c ---[ 647]---> Adder-cost: 1776   maxlim: 416732   bits: 20/19
c ---[ 646]---> BDD-cost:    7
c ---[ 645]---> BDD-cost:    4
c ---[ 644]---> BDD-cost:    6
c ---[ 643]---> BDD-cost:    8
c ---[ 642]---> BDD-cost:    6
c ---[ 641]---> BDD-cost:    8
c ---[ 640]---> BDD-cost:    7
c ---[ 639]---> BDD-cost:    4
c ---[ 638]---> BDD-cost:    7
c ---[ 637]---> BDD-cost:    7
c ---[ 635]---> Adder-cost: 1774   maxlim: 382300   bits: 20/19
c ---[ 634]---> BDD-cost:    5
c ---[ 633]---> BDD-cost:    7
c ---[ 632]---> BDD-cost:   17
c ---[ 631]---> BDD-cost:    7
c ---[ 630]---> BDD-cost:    6
c ---[ 629]---> BDD-cost:    7
c ---[ 628]---> BDD-cost:    8
c ---[ 627]---> BDD-cost:    3
c ---[ 626]---> BDD-cost:    8
c ---[ 625]---> BDD-cost:    8
c ---[ 623]---> Adder-cost: 1910   maxlim: 361820   bits: 20/19
c ---[ 622]---> BDD-cost:    5
c ---[ 621]---> BDD-cost:    5
c ---[ 620]---> BDD-cost:    3
c ---[ 619]---> BDD-cost:    5
c ---[ 618]---> BDD-cost:    4
c ---[ 617]---> BDD-cost:    4
c ---[ 616]---> BDD-cost:    5
c ---[ 615]---> BDD-cost:    7
c ---[ 614]---> BDD-cost:    6
c ---[ 613]---> BDD-cost:    6
c ---[ 611]---> Adder-cost: 1804   maxlim: 361181   bits: 20/19
c ---[ 610]---> BDD-cost:    7
c ---[ 609]---> BDD-cost:    7
c ---[ 608]---> BDD-cost:    7
c ---[ 607]---> BDD-cost:    5
c ---[ 606]---> BDD-cost:   17
c ---[ 605]---> BDD-cost:   15
c ---[ 604]---> BDD-cost:    7
c ---[ 603]---> BDD-cost:    5
c ---[ 602]---> BDD-cost:    7
c ---[ 601]---> BDD-cost:    6
c ---[ 599]---> Adder-cost: 1688   maxlim: 366303   bits: 20/19
c ---[ 598]---> BDD-cost:    6
c ---[ 597]---> BDD-cost:    7
c ---[ 596]---> BDD-cost:    7
c ---[ 595]---> BDD-cost:    7
c ---[ 594]---> BDD-cost:    8
c ---[ 593]---> BDD-cost:    7
c ---[ 592]---> BDD-cost:   16
c ---[ 591]---> BDD-cost:    3
c ---[ 590]---> BDD-cost:   19
c ---[ 589]---> BDD-cost:    8
c ---[ 587]---> Adder-cost: 1776   maxlim: 357854   bits: 20/19
c ---[ 586]---> BDD-cost:    4
c ---[ 585]---> BDD-cost:    6
c ---[ 584]---> BDD-cost:    8
c ---[ 583]---> BDD-cost:    6
c ---[ 582]---> BDD-cost:    5
c ---[ 581]---> BDD-cost:    8
c ---[ 580]---> BDD-cost:    8
c ---[ 579]---> BDD-cost:    6
c ---[ 578]---> BDD-cost:    7
c ---[ 577]---> BDD-cost:   15
c ---[ 575]---> Adder-cost: 1652   maxlim: 345567   bits: 20/19
c ---[ 574]---> BDD-cost:    5
c ---[ 573]---> BDD-cost:    7
c ---[ 572]---> BDD-cost:    6
c ---[ 571]---> BDD-cost:    5
c ---[ 570]---> BDD-cost:    6
c ---[ 569]---> BDD-cost:    7
c ---[ 568]---> BDD-cost:   18
c ---[ 567]---> BDD-cost:    4
c ---[ 566]---> BDD-cost:    4
c ---[ 565]---> BDD-cost:    8
c ---[ 563]---> Adder-cost: 1706   maxlim: 361951   bits: 20/19
c ---[ 562]---> BDD-cost:    7
c ---[ 561]---> BDD-cost:    6
c ---[ 560]---> BDD-cost:    8
c ---[ 559]---> BDD-cost:    5
c ---[ 558]---> BDD-cost:    5
c ---[ 557]---> BDD-cost:    6
c ---[ 556]---> BDD-cost:    7
c ---[ 555]---> BDD-cost:    8
c ---[ 554]---> BDD-cost:    8
c ---[ 553]---> BDD-cost:    7
c ---[ 551]---> Adder-cost: 1844   maxlim: 388571   bits: 20/19
c ---[ 550]---> BDD-cost:    5
c ---[ 549]---> BDD-cost:    3
c ---[ 548]---> BDD-cost:    4
c ---[ 547]---> BDD-cost:    5
c ---[ 546]---> BDD-cost:   19
c ---[ 545]---> BDD-cost:    6
c ---[ 544]---> BDD-cost:    7
c ---[ 543]---> BDD-cost:   16
c ---[ 542]---> BDD-cost:    3
c ---[ 541]---> BDD-cost:    8
c ---[ 539]---> Adder-cost: 1840   maxlim: 400221   bits: 20/19
c ---[ 538]---> BDD-cost:    7
c ---[ 537]---> BDD-cost:    7
c ---[ 536]---> BDD-cost:    3
c ---[ 535]---> BDD-cost:    7
c ---[ 534]---> BDD-cost:   16
c ---[ 533]---> BDD-cost:    7
c ---[ 532]---> BDD-cost:    6
c ---[ 531]---> BDD-cost:    3
c ---[ 530]---> BDD-cost:    4
c ---[ 529]---> BDD-cost:    4
c ---[ 527]---> BDD-cost:   63
c ---[ 525]---> Adder-cost: 1750   maxlim: 295774   bits: 20/19
c ---[ 524]---> BDD-cost:    3
c ---[ 523]---> BDD-cost:    6
c ---[ 522]---> BDD-cost:    7
c ---[ 521]---> BDD-cost:    5
c ---[ 520]---> BDD-cost:    8
c ---[ 519]---> BDD-cost:    8
c ---[ 518]---> BDD-cost:    8
c ---[ 517]---> BDD-cost:    7
c ---[ 516]---> BDD-cost:    7
c ---[ 515]---> BDD-cost:    8
c ---[ 513]---> Adder-cost: 1846   maxlim: 420571   bits: 20/19
c ---[ 512]---> BDD-cost:    6
c ---[ 511]---> BDD-cost:    6
c ---[ 510]---> BDD-cost:   18
c ---[ 509]---> BDD-cost:    8
c ---[ 508]---> BDD-cost:    5
c ---[ 507]---> BDD-cost:    4
c ---[ 506]---> BDD-cost:    8
c ---[ 505]---> BDD-cost:   18
c ---[ 504]---> BDD-cost:    7
c ---[ 503]---> BDD-cost:    7
c ---[ 501]---> Adder-cost: 1882   maxlim: 354138   bits: 20/19
c ---[ 500]---> BDD-cost:    8
c ---[ 499]---> BDD-cost:    3
c ---[ 498]---> BDD-cost:    8
c ---[ 497]---> BDD-cost:    7
c ---[ 496]---> BDD-cost:    7
c ---[ 495]---> BDD-cost:    8
c ---[ 494]---> BDD-cost:    8
c ---[ 493]---> BDD-cost:    8
c ---[ 492]---> BDD-cost:    6
c ---[ 491]---> BDD-cost:    7
c ---[ 489]---> Adder-cost: 1868   maxlim: 473819   bits: 20/19
c ---[ 488]---> BDD-cost:    5
c ---[ 487]---> BDD-cost:    8
c ---[ 486]---> BDD-cost:   19
c ---[ 485]---> BDD-cost:   19
c ---[ 484]---> BDD-cost:    8
c ---[ 483]---> BDD-cost:    7
c ---[ 482]---> BDD-cost:    5
c ---[ 481]---> BDD-cost:    8
c ---[ 480]---> BDD-cost:    7
c ---[ 479]---> BDD-cost:    8
c ---[ 477]---> Adder-cost: 1892   maxlim: 360028   bits: 20/19
c ---[ 476]---> BDD-cost:    7
c ---[ 475]---> BDD-cost:    4
c ---[ 474]---> BDD-cost:    5
c ---[ 473]---> BDD-cost:    6
c ---[ 472]---> BDD-cost:    7
c ---[ 471]---> BDD-cost:    8
c ---[ 470]---> BDD-cost:    8
c ---[ 469]---> BDD-cost:    6
c ---[ 468]---> BDD-cost:    8
c ---[ 467]---> BDD-cost:    5
c ---[ 465]---> Adder-cost: 1728   maxlim: 351069   bits: 20/19
c ---[ 464]---> BDD-cost:    6
c ---[ 463]---> BDD-cost:    8
c ---[ 462]---> BDD-cost:    7
c ---[ 461]---> BDD-cost:    5
c ---[ 460]---> BDD-cost:    3
c ---[ 459]---> BDD-cost:    4
c ---[ 458]---> BDD-cost:    7
c ---[ 457]---> BDD-cost:    7
c ---[ 456]---> BDD-cost:    6
c ---[ 455]---> BDD-cost:    5
c ---[ 453]---> Adder-cost: 1810   maxlim: 346847   bits: 20/19
c ---[ 452]---> BDD-cost:    3
c ---[ 451]---> BDD-cost:    5
c ---[ 450]---> BDD-cost:    7
c ---[ 449]---> BDD-cost:    6
c ---[ 448]---> BDD-cost:   17
c ---[ 447]---> BDD-cost:    5
c ---[ 446]---> BDD-cost:    6
c ---[ 445]---> BDD-cost:    6
c ---[ 444]---> BDD-cost:    8
c ---[ 443]---> BDD-cost:    6
c ---[ 441]---> Adder-cost: 1706   maxlim: 334815   bits: 20/19
c ---[ 440]---> BDD-cost:    6
c ---[ 439]---> BDD-cost:    6
c ---[ 438]---> BDD-cost:    8
c ---[ 437]---> BDD-cost:    7
c ---[ 436]---> BDD-cost:    5
c ---[ 435]---> BDD-cost:    8
c ---[ 434]---> BDD-cost:    5
c ---[ 433]---> BDD-cost:    6
c ---[ 432]---> BDD-cost:    7
c ---[ 431]---> BDD-cost:    8
c ---[ 429]---> Adder-cost: 1744   maxlim: 373858   bits: 20/19
c ---[ 428]---> BDD-cost:    3
c ---[ 427]---> BDD-cost:   16
c ---[ 426]---> BDD-cost:    8
c ---[ 425]---> BDD-cost:    6
c ---[ 424]---> BDD-cost:   18
c ---[ 423]---> BDD-cost:    6
c ---[ 422]---> BDD-cost:    4
c ---[ 421]---> BDD-cost:    3
c ---[ 420]---> BDD-cost:    7
c ---[ 419]---> BDD-cost:    7
c ---[ 418]---> BDD-cost:    8
c ---[ 417]---> BDD-cost:    7
c ---[ 416]---> BDD-cost:    3
c ---[ 415]---> BDD-cost:    7
c ---[ 414]---> BDD-cost:    7
c ---[ 413]---> BDD-cost:    4
c ---[ 412]---> BDD-cost:    8
c ---[ 411]---> BDD-cost:   17
c ---[ 410]---> BDD-cost:    5
c ---[ 409]---> BDD-cost:    8
c ---[ 408]---> BDD-cost:    3
c ---[ 406]---> BDD-cost:   71
c ---[ 405]---> BDD-cost:    6
c ---[ 404]---> BDD-cost:    7
c ---[ 403]---> BDD-cost:    8
c ---[ 402]---> BDD-cost:    5
c ---[ 401]---> BDD-cost:   18
c ---[ 400]---> BDD-cost:    5
c ---[ 399]---> BDD-cost:    5
c ---[ 398]---> BDD-cost:    8
c ---[ 397]---> BDD-cost:    7
c ---[ 396]---> BDD-cost:    5
c ---[ 395]---> BDD-cost:    8
c ---[ 394]---> BDD-cost:    8
c ---[ 393]---> BDD-cost:    6
c ---[ 392]---> BDD-cost:    6
c ---[ 391]---> BDD-cost:    8
c ---[ 390]---> BDD-cost:    8
c ---[ 389]---> BDD-cost:    7
c ---[ 388]---> BDD-cost:    7
c ---[ 387]---> BDD-cost:    3
c ---[ 386]---> BDD-cost:    6
c ---[ 385]---> BDD-cost:    7
c ---[ 384]---> BDD-cost:   19
c ---[ 383]---> BDD-cost:    8
c ---[ 382]---> BDD-cost:    6
c ---[ 381]---> BDD-cost:    3
c ---[ 380]---> BDD-cost:    8
c ---[ 379]---> BDD-cost:    7
c ---[ 378]---> BDD-cost:    6
c ---[ 377]---> BDD-cost:    3
c ---[ 376]---> BDD-cost:   18
c ---[ 375]---> BDD-cost:    8
c ---[ 374]---> BDD-cost:    3
c ---[ 373]---> BDD-cost:    7
c ---[ 372]---> BDD-cost:   17
c ---[ 371]---> BDD-cost:    8
c ---[ 370]---> BDD-cost:    7
c ---[ 369]---> BDD-cost:   19
c ---[ 368]---> BDD-cost:   15
c ---[ 367]---> BDD-cost:    8
c ---[ 366]---> BDD-cost:    8
c ---[ 365]---> BDD-cost:    4
c ---[ 364]---> BDD-cost:    7
c ---[ 363]---> BDD-cost:    7
c ---[ 362]---> BDD-cost:   19
c ---[ 361]---> BDD-cost:    8
c ---[ 360]---> BDD-cost:    5
c ---[ 359]---> BDD-cost:    8
c ---[ 358]---> BDD-cost:    7
c ---[ 357]---> BDD-cost:   16
c ---[ 356]---> BDD-cost:    6
c ---[ 355]---> BDD-cost:    7
c ---[ 354]---> BDD-cost:    5
c ---[ 353]---> BDD-cost:    5
c ---[ 352]---> BDD-cost:    8
c ---[ 351]---> BDD-cost:    4
c ---[ 350]---> BDD-cost:    6
c ---[ 349]---> BDD-cost:    6
c ---[ 348]---> BDD-cost:    8
c ---[ 347]---> BDD-cost:    3
c ---[ 346]---> BDD-cost:    8
c ---[ 345]---> BDD-cost:    6
c ---[ 344]---> BDD-cost:    7
c ---[ 343]---> BDD-cost:    6
c ---[ 342]---> BDD-cost:    7
c ---[ 341]---> BDD-cost:    7
c ---[ 340]---> BDD-cost:    8
c ---[ 339]---> BDD-cost:    5
c ---[ 338]---> BDD-cost:    8
c ---[ 337]---> BDD-cost:    7
c ---[ 336]---> BDD-cost:    8
c ---[ 335]---> BDD-cost:    5
c ---[ 334]---> BDD-cost:    6
c ---[ 333]---> BDD-cost:   19
c ---[ 332]---> BDD-cost:   17
c ---[ 331]---> BDD-cost:    7
c ---[ 330]---> BDD-cost:    4
c ---[ 329]---> BDD-cost:   14
c ---[ 328]---> BDD-cost:    6
c ---[ 327]---> BDD-cost:    8
c ---[ 326]---> BDD-cost:    8
c ---[ 325]---> BDD-cost:    6
c ---[ 324]---> BDD-cost:    4
c ---[ 323]---> BDD-cost:    6
c ---[ 322]---> BDD-cost:    3
c ---[ 321]---> BDD-cost:    7
c ---[ 320]---> BDD-cost:    7
c ---[ 319]---> BDD-cost:    7
c ---[ 318]---> BDD-cost:    6
c ---[ 317]---> BDD-cost:   17
c ---[ 316]---> BDD-cost:    8
c ---[ 315]---> BDD-cost:    6
c ---[ 314]---> BDD-cost:    8
c ---[ 313]---> BDD-cost:    3
c ---[ 312]---> BDD-cost:    6
c ---[ 311]---> BDD-cost:    7
c ---[ 310]---> BDD-cost:    5
c ---[ 309]---> BDD-cost:    6
c ---[ 308]---> BDD-cost:   19
c ---[ 307]---> BDD-cost:   17
c ---[ 306]---> BDD-cost:    7
c ---[ 305]---> BDD-cost:   14
c ---[ 304]---> BDD-cost:    7
c ---[ 303]---> BDD-cost:    3
c ---[ 302]---> BDD-cost:   19
c ---[ 301]---> BDD-cost:   19
c ---[ 300]---> BDD-cost:    5
c ---[ 299]---> BDD-cost:    7
c ---[ 298]---> BDD-cost:   17
c ---[ 297]---> BDD-cost:    5
c ---[ 296]---> BDD-cost:    5
c ---[ 294]---> BDD-cost:   65
c ---[ 293]---> BDD-cost:    5
c ---[ 292]---> BDD-cost:    8
c ---[ 291]---> BDD-cost:    3
c ---[ 290]---> BDD-cost:    7
c ---[ 289]---> BDD-cost:    3
c ---[ 288]---> BDD-cost:    8
c ---[ 287]---> BDD-cost:    7
c ---[ 286]---> BDD-cost:    5
c ---[ 285]---> BDD-cost:    7
c ---[ 284]---> BDD-cost:    7
c ---[ 283]---> BDD-cost:   15
c ---[ 282]---> BDD-cost:    7
c ---[ 281]---> BDD-cost:    6
c ---[ 280]---> BDD-cost:   19
c ---[ 279]---> BDD-cost:    6
c ---[ 278]---> BDD-cost:    3
c ---[ 277]---> BDD-cost:    5
c ---[ 276]---> BDD-cost:   16
c ---[ 275]---> BDD-cost:    8
c ---[ 274]---> BDD-cost:    8
c ---[ 273]---> BDD-cost:    3
c ---[ 272]---> BDD-cost:    8
c ---[ 271]---> BDD-cost:    8
c ---[ 270]---> BDD-cost:    7
c ---[ 269]---> BDD-cost:    6
c ---[ 268]---> BDD-cost:    8
c ---[ 267]---> BDD-cost:    6
c ---[ 266]---> BDD-cost:    7
c ---[ 265]---> BDD-cost:    8
c ---[ 264]---> BDD-cost:    5
c ---[ 263]---> BDD-cost:    7
c ---[ 262]---> BDD-cost:    3
c ---[ 261]---> BDD-cost:    6
c ---[ 260]---> BDD-cost:    5
c ---[ 259]---> BDD-cost:    8
c ---[ 258]---> BDD-cost:    8
c ---[ 257]---> BDD-cost:    7
c ---[ 256]---> BDD-cost:   16
c ---[ 255]---> BDD-cost:    8
c ---[ 254]---> BDD-cost:    8
c ---[ 253]---> BDD-cost:    6
c ---[ 252]---> BDD-cost:   17
c ---[ 251]---> BDD-cost:    8
c ---[ 250]---> BDD-cost:    7
c ---[ 249]---> BDD-cost:    8
c ---[ 248]---> BDD-cost:    3
c ---[ 247]---> BDD-cost:    8
c ---[ 246]---> BDD-cost:    7
c ---[ 245]---> BDD-cost:    4
c ---[ 244]---> BDD-cost:    3
c ---[ 243]---> BDD-cost:    3
c ---[ 242]---> BDD-cost:    7
c ---[ 241]---> BDD-cost:    7
c ---[ 240]---> BDD-cost:    4
c ---[ 239]---> BDD-cost:    3
c ---[ 238]---> BDD-cost:   16
c ---[ 237]---> BDD-cost:    8
c ---[ 236]---> BDD-cost:    6
c ---[ 235]---> BDD-cost:    8
c ---[ 234]---> BDD-cost:    6
c ---[ 233]---> BDD-cost:   18
c ---[ 232]---> BDD-cost:    6
c ---[ 231]---> BDD-cost:    6
c ---[ 230]---> BDD-cost:    8
c ---[ 229]---> BDD-cost:   18
c ---[ 228]---> BDD-cost:    7
c ---[ 227]---> BDD-cost:    8
c ---[ 226]---> BDD-cost:    8
c ---[ 225]---> BDD-cost:    8
c ---[ 224]---> BDD-cost:   18
c ---[ 223]---> BDD-cost:    6
c ---[ 222]---> BDD-cost:    7
c ---[ 221]---> BDD-cost:    6
c ---[ 220]---> BDD-cost:    3
c ---[ 219]---> BDD-cost:   17
c ---[ 218]---> BDD-cost:   16
c ---[ 217]---> BDD-cost:   18
c ---[ 216]---> BDD-cost:    7
c ---[ 215]---> BDD-cost:    3
c ---[ 214]---> BDD-cost:    3
c ---[ 213]---> BDD-cost:    4
c ---[ 212]---> BDD-cost:    8
c ---[ 211]---> BDD-cost:    6
c ---[ 210]---> BDD-cost:    6
c ---[ 209]---> BDD-cost:    8
c ---[ 208]---> BDD-cost:    3
c ---[ 207]---> BDD-cost:    7
c ---[ 206]---> BDD-cost:    7
c ---[ 205]---> BDD-cost:    8
c ---[ 204]---> BDD-cost:    6
c ---[ 203]---> BDD-cost:    5
c ---[ 202]---> BDD-cost:    7
c ---[ 201]---> BDD-cost:    4
c ---[ 200]---> BDD-cost:    6
c ---[ 199]---> BDD-cost:    7
c ---[ 198]---> BDD-cost:    7
c ---[ 197]---> BDD-cost:   18
c ---[ 196]---> BDD-cost:   18
c ---[ 195]---> BDD-cost:    3
c ---[ 194]---> BDD-cost:    8
c ---[ 193]---> BDD-cost:    6
c ---[ 192]---> BDD-cost:    8
c ---[ 191]---> BDD-cost:    6
c ---[ 190]---> BDD-cost:    8
c ---[ 189]---> BDD-cost:    6
c ---[ 188]---> BDD-cost:    3
c ---[ 187]---> BDD-cost:    6
c ---[ 186]---> BDD-cost:    6
c ---[ 185]---> BDD-cost:    7
c ---[ 184]---> BDD-cost:    7
c ---[ 183]---> BDD-cost:    1
c ---[ 182]---> BDD-cost:    1
c ---[ 181]---> BDD-cost:    1
c ---[ 180]---> BDD-cost:    1
c ---[ 179]---> BDD-cost:    1
c ---[ 178]---> BDD-cost:    1
c ---[ 177]---> BDD-cost:    1
c ---[ 176]---> BDD-cost:    1
c ---[ 175]---> BDD-cost:    1
c ---[ 174]---> BDD-cost:    1
c ---[ 173]---> BDD-cost:    1
c ---[ 172]---> BDD-cost:    1
c ---[ 171]---> BDD-cost:    1
c ---[ 170]---> BDD-cost:    1
c ---[ 169]---> BDD-cost:    1
c ---[ 168]---> BDD-cost:    1
c ---[ 167]---> BDD-cost:    1
c ---[ 166]---> BDD-cost:    1
c ---[ 165]---> BDD-cost:    1
c ---[ 164]---> BDD-cost:    1
c ---[ 163]---> BDD-cost:    1
c ---[ 162]---> BDD-cost:    1
c ---[ 161]---> BDD-cost:    1
c ---[ 160]---> BDD-cost:    1
c ---[ 159]---> BDD-cost:    1
c ---[ 158]---> BDD-cost:    1
c ---[ 157]---> BDD-cost:    1
c ---[ 156]---> BDD-cost:    1
c ---[ 155]---> BDD-cost:    1
c ---[ 154]---> BDD-cost:    1
c ---[ 153]---> BDD-cost:    1
c ---[ 152]---> BDD-cost:    1
c ---[ 151]---> BDD-cost:    1
c ---[ 150]---> BDD-cost:    1
c ---[ 149]---> BDD-cost:    1
c ---[ 148]---> BDD-cost:    1
c ---[ 147]---> BDD-cost:    1
c ---[ 146]---> BDD-cost:    1
c ---[ 145]---> BDD-cost:    1
c ---[ 144]---> BDD-cost:    1
c ---[ 143]---> BDD-cost:    1
c ---[ 142]---> BDD-cost:    1
c ---[ 141]---> BDD-cost:    1
c ---[ 140]---> BDD-cost:    1
c ---[ 139]---> BDD-cost:    1
c ---[ 138]---> BDD-cost:    1
c ---[ 137]---> BDD-cost:    1
c ---[ 136]---> BDD-cost:    1
c ---[ 135]---> BDD-cost:    1
c ---[ 134]---> BDD-cost:    1
c ---[ 133]---> BDD-cost:    1
c ---[ 132]---> BDD-cost:    1
c ---[ 131]---> BDD-cost:    1
c ---[ 130]---> BDD-cost:    1
c ---[ 129]---> BDD-cost:    1
c ---[ 128]---> BDD-cost:    1
c ---[ 127]---> BDD-cost:    1
c ---[ 126]---> BDD-cost:    1
c ---[ 125]---> BDD-cost:    1
c ---[ 124]---> BDD-cost:    1
c ---[ 123]---> BDD-cost:    1
c ---[ 122]---> BDD-cost:    1
c ---[ 121]---> BDD-cost:    1
c ---[ 120]---> BDD-cost:    1
c ---[ 119]---> BDD-cost:    1
c ---[ 118]---> BDD-cost:    1
c ---[ 117]---> BDD-cost:    1
c ---[ 116]---> BDD-cost:    1
c ---[ 115]---> BDD-cost:    1
c ---[ 114]---> BDD-cost:    1
c ---[ 113]---> BDD-cost:    1
c ---[ 112]---> BDD-cost:    1
c ---[ 111]---> BDD-cost:    1
c ---[ 110]---> BDD-cost:    1
c ---[ 109]---> BDD-cost:    1
c ---[ 108]---> BDD-cost:    1
c ---[ 107]---> BDD-cost:    1
c ---[ 106]---> BDD-cost:    1
c ---[ 105]---> BDD-cost:    1
c ---[ 104]---> BDD-cost:    1
c ---[ 103]---> BDD-cost:    1
c ---[ 102]---> BDD-cost:    1
c ---[ 101]---> BDD-cost:    1
c ---[ 100]---> BDD-cost:    1
c ---[  99]---> BDD-cost:    1
c ---[  98]---> BDD-cost:    1
c ---[  97]---> BDD-cost:    1
c ---[  96]---> BDD-cost:    1
c ---[  95]---> BDD-cost:    1
c ---[  94]---> BDD-cost:    1
c ---[  93]---> BDD-cost:    1
c ---[  92]---> BDD-cost:    1
c ---[  91]---> BDD-cost:    1
c ---[  90]---> BDD-cost:    1
c ---[  89]---> BDD-cost:    1
c ---[  88]---> BDD-cost:    1
c ---[  87]---> BDD-cost:    1
c ---[  86]---> BDD-cost:    1
c ---[  85]---> BDD-cost:    1
c ---[  84]---> BDD-cost:    1
c ---[  83]---> BDD-cost:    1
c ---[  82]---> BDD-cost:    1
c ---[  81]---> BDD-cost:    1
c ---[  80]---> BDD-cost:    1
c ---[  79]---> BDD-cost:    1
c ---[  78]---> BDD-cost:    1
c ---[  77]---> BDD-cost:    1
c ---[  76]---> BDD-cost:    1
c ---[  75]---> BDD-cost:    1
c ---[  74]---> BDD-cost:    1
c ---[  73]---> BDD-cost:    1
c ---[  72]---> BDD-cost:    1
c ---[  71]---> BDD-cost:    1
c ---[  70]---> BDD-cost:    1
c ---[  69]---> BDD-cost:    1
c ---[  68]---> BDD-cost:    1
c ---[  67]---> BDD-cost:    1
c ---[  66]---> BDD-cost:    1
c ---[  65]---> BDD-cost:    1
c ---[  64]---> BDD-cost:    1
c ---[  63]---> BDD-cost:    1
c ---[  62]---> BDD-cost:    1
c ---[  61]---> BDD-cost:    1
c ---[  60]---> BDD-cost:    1
c ---[  59]---> BDD-cost:    1
c ---[  58]---> BDD-cost:    1
c ---[  57]---> BDD-cost:    1
c ---[  56]---> BDD-cost:    1
c ---[  55]---> BDD-cost:    1
c ---[  54]---> BDD-cost:    1
c ---[  53]---> BDD-cost:    1
c ---[  52]---> BDD-cost:    1
c ---[  51]---> BDD-cost:    1
c ---[  50]---> BDD-cost:    1
c ---[  49]---> BDD-cost:    1
c ---[  48]---> BDD-cost:    1
c ---[  47]---> BDD-cost:    1
c ---[  46]---> BDD-cost:    1
c ---[  45]---> BDD-cost:    1
c ---[  44]---> BDD-cost:    1
c ---[  43]---> BDD-cost:    1
c ---[  42]---> BDD-cost:    1
c ---[  41]---> BDD-cost:    1
c ---[  40]---> BDD-cost:    1
c ---[  39]---> BDD-cost:    1
c ---[  38]---> BDD-cost:    1
c ---[  37]---> BDD-cost:    1
c ---[  36]---> BDD-cost:    1
c ---[  35]---> BDD-cost:    1
c ---[  34]---> BDD-cost:    1
c ---[  33]---> BDD-cost:    1
c ---[  32]---> BDD-cost:    1
c ---[  31]---> BDD-cost:    1
c ---[  30]---> BDD-cost:    1
c ---[  29]---> BDD-cost:    1
c ---[  28]---> BDD-cost:    1
c ---[  27]---> BDD-cost:    1
c ---[  26]---> BDD-cost:    1
c ---[  25]---> BDD-cost:    1
c ---[  24]---> BDD-cost:    1
c ---[  23]---> BDD-cost:    1
c ---[  22]---> BDD-cost:    1
c ---[  21]---> BDD-cost:    1
c ---[  20]---> BDD-cost:    1
c ---[  19]---> BDD-cost:    1
c ---[  18]---> BDD-cost:    1
c ---[  17]---> BDD-cost:    1
c ---[  16]---> BDD-cost:    1
c ---[  15]---> BDD-cost:    1
c ---[  14]---> BDD-cost:    1
c ---[  13]---> BDD-cost:    1
c ---[  12]---> BDD-cost:    1
c ---[  11]---> BDD-cost:    1
c ---[  10]---> BDD-cost:    1
c ---[   9]---> BDD-cost:    1
c ---[   8]---> BDD-cost:    1
c ---[   7]---> BDD-cost:    1
c ---[   6]---> BDD-cost:    1
c ---[   5]---> BDD-cost:    1
c ---[   4]---> BDD-cost:    1
c ---[   3]---> BDD-cost:    1
c ---[   2]---> BDD-cost:    1
c ---[   1]---> BDD-cost:    1
c ---[   0]---> BDD-cost:    1
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |  532570  1857987 |  177523       0        0     nan |  0.000 % |
c |       101 |  532570  1857987 |  195275     101    37586   372.1 |  4.235 % |
c |       253 |  532561  1857956 |  214802     251    42380   168.8 |  4.236 % |
c |       478 |  532524  1857833 |  236283     459    43284    94.3 |  4.241 % |
c |       815 |  532508  1857781 |  259911     794    85927   108.2 |  4.243 % |
c |      1325 |  532499  1857750 |  285902    1301   121399    93.3 |  4.244 % |
c |      2084 |  532465  1857636 |  314492    2051   182853    89.2 |  4.248 % |
c |      3224 |  532422  1857491 |  345942    3182   244996    77.0 |  4.253 % |
c |      4933 |  532404  1857429 |  380536    4886   756179   154.8 |  4.255 % |
c |      7495 |  532404  1857429 |  418589    7448  1081555   145.2 |  4.255 % |
c |     11342 |  532369  1857306 |  460448   11282  1731938   153.5 |  4.259 % |
c |     17108 |  532334  1857187 |  506493   17039  2731363   160.3 |  4.263 % |
c |     25758 |  532325  1857156 |  557143   25687  4730832   184.2 |  4.264 % |
c |     38732 |  532236  1856857 |  612857   38644  7750605   200.6 |  4.275 % |
c |     58193 |  532168  1856625 |  674143   58082 11726103   201.9 |  4.282 % |
c |     87385 |  532116  1856449 |  741557   87262 23166830   265.5 |  4.288 % |
#### 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.85 0.97 0.93 2/54 10783
Raw data (stat): 10783 (runsolver) R 10782 29151 29150 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 488383162 1052672 99 4294967295 134512640 135381576 3221224432 3221219676 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.87 0.97 0.93 2/54 10783
Raw data (stat): 10783 (minisat+) R 10782 29151 29150 0 -1 0 11237 0 0 0 968 30 0 0 25 0 1 0 488383162 49766400 10785 4294967295 134512640 134672761 3221224544 3221223712 134561201 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12150 10785 603 41 0 12109 0
vsize: 48600
[startup+20.0007 s]
Raw data (loadavg): 0.89 0.97 0.93 2/54 10783
Raw data (stat): 10783 (minisat+) R 10782 29151 29150 0 -1 0 11328 0 0 0 1968 30 0 0 25 0 1 0 488383162 50171904 10876 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12249 10876 603 41 0 12208 0
vsize: 48996
[startup+30.0015 s]
Raw data (loadavg): 0.91 0.97 0.93 2/54 10783
Raw data (stat): 10783 (minisat+) R 10782 29151 29150 0 -1 0 11404 0 0 0 2968 30 0 0 25 0 1 0 488383162 50577408 10952 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12348 10952 603 41 0 12307 0
vsize: 49392
[startup+40.0017 s]
Raw data (loadavg): 0.92 0.97 0.93 2/54 10783
Raw data (stat): 10783 (minisat+) R 10782 29151 29150 0 -1 0 11452 0 0 0 3968 31 0 0 25 0 1 0 488383162 50712576 11000 4294967295 134512640 134672761 3221224544 3221223732 134556676 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12381 11000 603 41 0 12340 0
vsize: 49524
[startup+50.0031 s]
Raw data (loadavg): 0.93 0.97 0.93 2/54 10783
Raw data (stat): 10783 (minisat+) R 10782 29151 29150 0 -1 0 11577 0 0 0 4967 32 0 0 25 0 1 0 488383162 51253248 11125 4294967295 134512640 134672761 3221224544 3221223712 134560842 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12513 11125 603 41 0 12472 0
vsize: 50052
[startup+60.003 s]
Raw data (loadavg): 0.94 0.97 0.93 2/54 10783
Raw data (stat): 10783 (minisat+) R 10782 29151 29150 0 -1 0 11800 0 0 0 5966 33 0 0 25 0 1 0 488383162 52199424 11348 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12744 11348 603 41 0 12703 0
vsize: 50976
[startup+70.0028 s]
Raw data (loadavg): 0.95 0.97 0.93 2/54 10783
Raw data (stat): 10783 (minisat+) R 10782 29151 29150 0 -1 0 11991 0 0 0 6965 33 0 0 25 0 1 0 488383162 52871168 11539 4294967295 134512640 134672761 3221224544 3221223712 134561164 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12908 11539 603 41 0 12867 0
vsize: 51632
[startup+80.0036 s]
Raw data (loadavg): 0.96 0.97 0.93 2/54 10783
Raw data (stat): 10783 (minisat+) R 10782 29151 29150 0 -1 0 12087 0 0 0 7964 34 0 0 25 0 1 0 488383162 53276672 11635 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13007 11635 603 41 0 12966 0
vsize: 52028
[startup+90.0034 s]
Raw data (loadavg): 0.96 0.97 0.93 2/54 10783
Raw data (stat): 10783 (minisat+) R 10782 29151 29150 0 -1 0 12257 0 0 0 8963 36 0 0 25 0 1 0 488383162 53952512 11805 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13172 11805 603 41 0 13131 0
vsize: 52688
[startup+100.005 s]
Raw data (loadavg): 0.97 0.97 0.93 2/54 10783
Raw data (stat): 10783 (minisat+) R 10782 29151 29150 0 -1 0 12405 0 0 0 9962 37 0 0 25 0 1 0 488383162 54624256 11953 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13336 11953 603 41 0 13295 0
vsize: 53344
[startup+110.005 s]
Raw data (loadavg): 0.97 0.97 0.93 2/54 10783
Raw data (stat): 10783 (minisat+) R 10782 29151 29150 0 -1 0 12531 0 0 0 10962 37 0 0 25 0 1 0 488383162 55201792 12079 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13477 12079 603 41 0 13436 0
vsize: 53908
[startup+120.006 s]
Raw data (loadavg): 0.98 0.97 0.93 2/54 10783
Raw data (stat): 10783 (minisat+) R 10782 29151 29150 0 -1 0 12603 0 0 0 11961 38 0 0 25 0 1 0 488383162 55472128 12151 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13543 12151 603 41 0 13502 0
vsize: 54172
[startup+130.007 s]
Raw data (loadavg): 0.98 0.97 0.93 2/54 10783
Raw data (stat): 10783 (minisat+) R 10782 29151 29150 0 -1 0 12763 0 0 0 12962 38 0 0 25 0 1 0 488383162 56143872 12311 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13707 12311 603 41 0 13666 0
vsize: 54828
[startup+140.007 s]
Raw data (loadavg): 0.98 0.97 0.93 2/54 10783
Raw data (stat): 10783 (minisat+) R 10782 29151 29150 0 -1 0 12911 0 0 0 13961 39 0 0 25 0 1 0 488383162 56684544 12459 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13839 12459 603 41 0 13798 0
vsize: 55356
[startup+150.007 s]
Raw data (loadavg): 0.98 0.97 0.93 2/54 10783
Raw data (stat): 10783 (minisat+) R 10782 29151 29150 0 -1 0 13030 0 0 0 14960 39 0 0 25 0 1 0 488383162 57225216 12578 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13971 12578 603 41 0 13930 0
vsize: 55884
[startup+160.008 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 10783
Raw data (stat): 10783 (minisat+) R 10782 29151 29150 0 -1 0 13125 0 0 0 15960 40 0 0 25 0 1 0 488383162 57630720 12673 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14070 12673 603 41 0 14029 0
vsize: 56280
[startup+170.007 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 10783
Raw data (stat): 10783 (minisat+) R 10782 29151 29150 0 -1 0 13270 0 0 0 16959 40 0 0 25 0 1 0 488383162 58167296 12818 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14201 12818 603 41 0 14160 0
vsize: 56804
[startup+180.008 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 10783
Raw data (stat): 10783 (minisat+) R 10782 29151 29150 0 -1 0 13389 0 0 0 17959 41 0 0 25 0 1 0 488383162 58707968 12937 4294967295 134512640 134672761 3221224544 3221223712 134560871 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14333 12937 603 41 0 14292 0
vsize: 57332
[startup+190.009 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 10783
Raw data (stat): 10783 (minisat+) R 10782 29151 29150 0 -1 0 13482 0 0 0 18958 42 0 0 25 0 1 0 488383162 58978304 13030 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14399 13030 603 41 0 14358 0
vsize: 57596
[startup+200.009 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 10783
Raw data (stat): 10783 (minisat+) R 10782 29151 29150 0 -1 0 13620 0 0 0 19957 43 0 0 25 0 1 0 488383162 59654144 13168 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14564 13168 603 41 0 14523 0
vsize: 58256
[startup+210.009 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 10783
Raw data (stat): 10783 (minisat+) R 10782 29151 29150 0 -1 0 13777 0 0 0 20956 44 0 0 25 0 1 0 488383162 60194816 13325 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14696 13325 603 41 0 14655 0
vsize: 58784
[startup+220.01 s]
Raw data (loadavg): 1.07 0.99 0.93 2/54 10783
Raw data (stat): 10783 (minisat+) R 10782 29151 29150 0 -1 0 13928 0 0 0 21955 45 0 0 25 0 1 0 488383162 60981248 13476 4294967295 134512640 134672761 3221224544 3221223648 134555373 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14888 13476 603 41 0 14847 0
vsize: 59552
[startup+230.01 s]
Raw data (loadavg): 1.06 0.99 0.93 2/54 10783
Raw data (stat): 10783 (minisat+) R 10782 29151 29150 0 -1 0 14107 0 0 0 22955 46 0 0 25 0 1 0 488383162 61652992 13655 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15052 13655 603 41 0 15011 0
vsize: 60208
[startup+240.01 s]
Raw data (loadavg): 1.05 0.99 0.93 2/54 10783
Raw data (stat): 10783 (minisat+) R 10782 29151 29150 0 -1 0 14172 0 0 0 23954 46 0 0 25 0 1 0 488383162 61923328 13720 4294967295 134512640 134672761 3221224544 3221223712 134560882 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15118 13720 603 41 0 15077 0
vsize: 60472
[startup+250.011 s]
Raw data (loadavg): 1.04 0.99 0.93 2/54 10783
Raw data (stat): 10783 (minisat+) R 10782 29151 29150 0 -1 0 14261 0 0 0 24954 46 0 0 25 0 1 0 488383162 62328832 13809 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15217 13809 603 41 0 15176 0
vsize: 60868
[startup+260.011 s]
Raw data (loadavg): 1.03 0.99 0.93 2/54 10783
Raw data (stat): 10783 (minisat+) R 10782 29151 29150 0 -1 0 14400 0 0 0 25953 47 0 0 25 0 1 0 488383162 62869504 13948 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15349 13948 603 41 0 15308 0
vsize: 61396
[startup+270.011 s]
Raw data (loadavg): 1.03 0.99 0.93 2/54 10783
Raw data (stat): 10783 (minisat+) R 10782 29151 29150 0 -1 0 14608 0 0 0 26953 48 0 0 25 0 1 0 488383162 63676416 14156 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15546 14156 603 41 0 15505 0
vsize: 62184
[startup+280.012 s]
Raw data (loadavg): 1.02 0.99 0.93 2/54 10783
Raw data (stat): 10783 (minisat+) R 10782 29151 29150 0 -1 0 14711 0 0 0 27952 49 0 0 25 0 1 0 488383162 64077824 14259 4294967295 134512640 134672761 3221224544 3221223744 134557842 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15644 14259 603 41 0 15603 0
vsize: 62576
[startup+290.013 s]
Raw data (loadavg): 1.02 0.99 0.93 2/54 10783
Raw data (stat): 10783 (minisat+) R 10782 29151 29150 0 -1 0 15011 0 0 0 28951 50 0 0 25 0 1 0 488383162 65290240 14559 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15940 14559 603 41 0 15899 0
vsize: 63760
[startup+300.013 s]
Raw data (loadavg): 1.02 0.99 0.93 2/54 10783
Raw data (stat): 10783 (minisat+) R 10782 29151 29150 0 -1 0 15257 0 0 0 29950 51 0 0 25 0 1 0 488383162 66367488 14805 4294967295 134512640 134672761 3221224544 3221223680 134560557 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16203 14805 603 41 0 16162 0
vsize: 64812
[startup+310.013 s]
Raw data (loadavg): 1.01 0.99 0.93 2/54 10783
Raw data (stat): 10783 (minisat+) R 10782 29151 29150 0 -1 0 15521 0 0 0 30949 52 0 0 25 0 1 0 488383162 67440640 15069 4294967295 134512640 134672761 3221224544 3221223616 134553544 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16465 15069 603 41 0 16424 0
vsize: 65860
[startup+320.012 s]
Raw data (loadavg): 1.01 0.99 0.93 2/54 10783
Raw data (stat): 10783 (minisat+) R 10782 29151 29150 0 -1 0 15801 0 0 0 31948 53 0 0 25 0 1 0 488383162 68513792 15349 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16727 15349 603 41 0 16686 0
vsize: 66908
[startup+330.013 s]
Raw data (loadavg): 1.01 0.99 0.93 2/54 10783
Raw data (stat): 10783 (minisat+) R 10782 29151 29150 0 -1 0 16040 0 0 0 32946 55 0 0 25 0 1 0 488383162 69591040 15588 4294967295 134512640 134672761 3221224544 3221223712 134560888 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16990 15588 603 41 0 16949 0
vsize: 67960
[startup+340.023 s]
Raw data (loadavg): 1.01 0.99 0.93 2/54 10783
Raw data (stat): 10783 (minisat+) R 10782 29151 29150 0 -1 0 16213 0 0 0 33947 55 0 0 25 0 1 0 488383162 70262784 15761 4294967295 134512640 134672761 3221224544 3221223712 134560839 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17154 15761 603 41 0 17113 0
vsize: 68616
[startup+350.022 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 10783
Raw data (stat): 10783 (minisat+) R 10782 29151 29150 0 -1 0 16341 0 0 0 34946 56 0 0 25 0 1 0 488383162 70803456 15889 4294967295 134512640 134672761 3221224544 3221223680 134560706 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17286 15889 603 41 0 17245 0
vsize: 69144
[startup+360.023 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 10783
Raw data (stat): 10783 (minisat+) R 10782 29151 29150 0 -1 0 16466 0 0 0 35945 57 0 0 25 0 1 0 488383162 71204864 16014 4294967295 134512640 134672761 3221224544 3221223712 134560895 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17384 16014 603 41 0 17343 0
vsize: 69536
[startup+370.022 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 10783
Raw data (stat): 10783 (minisat+) R 10782 29151 29150 0 -1 0 16543 0 0 0 36945 57 0 0 25 0 1 0 488383162 71610368 16091 4294967295 134512640 134672761 3221224544 3221223680 134560688 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17483 16091 603 41 0 17442 0
vsize: 69932
[startup+380.023 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 10783
Raw data (stat): 10783 (minisat+) R 10782 29151 29150 0 -1 0 16630 0 0 0 37945 58 0 0 25 0 1 0 488383162 71880704 16178 4294967295 134512640 134672761 3221224544 3221223648 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17549 16178 603 41 0 17508 0
vsize: 70196
[startup+390.023 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 10783
Raw data (stat): 10783 (minisat+) R 10782 29151 29150 0 -1 0 16719 0 0 0 38944 58 0 0 25 0 1 0 488383162 72282112 16267 4294967295 134512640 134672761 3221224544 3221223712 134560956 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17647 16267 603 41 0 17606 0
vsize: 70588
[startup+400.023 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 10783
Raw data (stat): 10783 (minisat+) R 10782 29151 29150 0 -1 0 16834 0 0 0 39944 59 0 0 25 0 1 0 488383162 72814592 16382 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17777 16382 603 41 0 17736 0
vsize: 71108
[startup+410.024 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 10783
Raw data (stat): 10783 (minisat+) R 10782 29151 29150 0 -1 0 16956 0 0 0 40944 59 0 0 25 0 1 0 488383162 73220096 16504 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17876 16504 603 41 0 17835 0
vsize: 71504
[startup+420.023 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 10783
Raw data (stat): 10783 (minisat+) R 10782 29151 29150 0 -1 0 17069 0 0 0 41944 59 0 0 25 0 1 0 488383162 73760768 16617 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18008 16617 603 41 0 17967 0
vsize: 72032
[startup+430.024 s]
Raw data (loadavg): 1.00 0.99 0.93 3/54 10783
Raw data (stat): 10783 (minisat+) R 10782 29151 29150 0 -1 0 17283 0 0 0 42944 60 0 0 25 0 1 0 488383162 74567680 16831 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18205 16831 603 41 0 18164 0
vsize: 72820
[startup+440.024 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 10783
Raw data (stat): 10783 (minisat+) R 10782 29151 29150 0 -1 0 17626 0 0 0 43943 60 0 0 25 0 1 0 488383162 76173312 17174 4294967295 134512640 134672761 3221224544 3221223728 134558662 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18597 17174 603 41 0 18556 0
vsize: 74388
[startup+450.024 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 10783
Raw data (stat): 10783 (minisat+) R 10782 29151 29150 0 -1 0 17907 0 0 0 44942 61 0 0 25 0 1 0 488383162 77250560 17455 4294967295 134512640 134672761 3221224544 3221223712 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18860 17455 603 41 0 18819 0
vsize: 75440
[startup+460.024 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 10783
Raw data (stat): 10783 (minisat+) R 10782 29151 29150 0 -1 0 18188 0 0 0 45941 62 0 0 25 0 1 0 488383162 78458880 17736 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19155 17736 603 41 0 19114 0
vsize: 76620
[startup+470.025 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 10783
Raw data (stat): 10783 (minisat+) R 10782 29151 29150 0 -1 0 18471 0 0 0 46941 63 0 0 25 0 1 0 488383162 79540224 18019 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19419 18019 603 41 0 19378 0
vsize: 77676
[startup+480.024 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 10783
Raw data (stat): 10783 (minisat+) R 10782 29151 29150 0 -1 0 18785 0 0 0 47940 64 0 0 25 0 1 0 488383162 80883712 18333 4294967295 134512640 134672761 3221224544 3221223712 134560842 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19747 18333 603 41 0 19706 0
vsize: 78988
[startup+490.024 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 10783
Raw data (stat): 10783 (minisat+) R 10782 29151 29150 0 -1 0 18893 0 0 0 48940 64 0 0 25 0 1 0 488383162 81289216 18441 4294967295 134512640 134672761 3221224544 3221223744 134557911 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19846 18441 603 41 0 19805 0
vsize: 79384
[startup+500.024 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 10783
Raw data (stat): 10783 (minisat+) R 10782 29151 29150 0 -1 0 19028 0 0 0 49940 65 0 0 25 0 1 0 488383162 81829888 18576 4294967295 134512640 134672761 3221224544 3221223728 134558899 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19978 18576 603 41 0 19937 0
vsize: 79912
[startup+510.024 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 10783
Raw data (stat): 10783 (minisat+) R 10782 29151 29150 0 -1 0 19190 0 0 0 50940 65 0 0 25 0 1 0 488383162 82505728 18738 4294967295 134512640 134672761 3221224544 3221223712 134560855 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20143 18738 603 41 0 20102 0
vsize: 80572
[startup+520.024 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 10783
Raw data (stat): 10783 (minisat+) R 10782 29151 29150 0 -1 0 19353 0 0 0 51939 66 0 0 25 0 1 0 488383162 83173376 18901 4294967295 134512640 134672761 3221224544 3221223712 134560871 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20306 18901 603 41 0 20265 0
vsize: 81224
[startup+530.025 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 10783
Raw data (stat): 10783 (minisat+) R 10782 29151 29150 0 -1 0 19447 0 0 0 52938 66 0 0 25 0 1 0 488383162 83578880 18995 4294967295 134512640 134672761 3221224544 3221223712 134560839 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20405 18995 603 41 0 20364 0
vsize: 81620
[startup+540.026 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 10783
Raw data (stat): 10783 (minisat+) R 10782 29151 29150 0 -1 0 19589 0 0 0 53938 66 0 0 25 0 1 0 488383162 84115456 19137 4294967295 134512640 134672761 3221224544 3221223712 134561391 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20536 19137 603 41 0 20495 0
vsize: 82144
[startup+550.025 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 10783
Raw data (stat): 10783 (minisat+) R 10782 29151 29150 0 -1 0 19819 0 0 0 54938 67 0 0 25 0 1 0 488383162 85061632 19367 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20767 19367 603 41 0 20726 0
vsize: 83068
[startup+560.025 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 10783
Raw data (stat): 10783 (minisat+) R 10782 29151 29150 0 -1 0 20016 0 0 0 55937 67 0 0 25 0 1 0 488383162 85864448 19564 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20963 19564 603 41 0 20922 0
vsize: 83852
[startup+570.025 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 10783
Raw data (stat): 10783 (minisat+) R 10782 29151 29150 0 -1 0 20175 0 0 0 56936 68 0 0 25 0 1 0 488383162 86536192 19723 4294967295 134512640 134672761 3221224544 3221223712 134560858 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21127 19723 603 41 0 21086 0
vsize: 84508
[startup+580.026 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 10783
Raw data (stat): 10783 (minisat+) R 10782 29151 29150 0 -1 0 20299 0 0 0 57936 69 0 0 25 0 1 0 488383162 87076864 19847 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21259 19847 603 41 0 21218 0
vsize: 85036
[startup+590.025 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 10783
Raw data (stat): 10783 (minisat+) R 10782 29151 29150 0 -1 0 20457 0 0 0 58935 70 0 0 25 0 1 0 488383162 87617536 20005 4294967295 134512640 134672761 3221224544 3221223648 134559862 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21391 20005 603 41 0 21350 0
vsize: 85564
[startup+600.026 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 10783
Raw data (stat): 10783 (minisat+) R 10782 29151 29150 0 -1 0 20619 0 0 0 59935 70 0 0 25 0 1 0 488383162 88289280 20167 4294967295 134512640 134672761 3221224544 3221223712 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21555 20167 603 41 0 21514 0
vsize: 86220
[startup+610.026 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 10783
Raw data (stat): 10783 (minisat+) R 10782 29151 29150 0 -1 0 20770 0 0 0 60935 70 0 0 25 0 1 0 488383162 88965120 20318 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21720 20318 603 41 0 21679 0
vsize: 86880
[startup+620.026 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 10783
Raw data (stat): 10783 (minisat+) R 10782 29151 29150 0 -1 0 20939 0 0 0 61935 70 0 0 25 0 1 0 488383162 89636864 20487 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21884 20487 603 41 0 21843 0
vsize: 87536
[startup+630.026 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 10783
Raw data (stat): 10783 (minisat+) R 10782 29151 29150 0 -1 0 21125 0 0 0 62935 71 0 0 25 0 1 0 488383162 90447872 20673 4294967295 134512640 134672761 3221224544 3221223680 134560729 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22082 20673 603 41 0 22041 0
vsize: 88328
[startup+640.027 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 10783
Raw data (stat): 10783 (minisat+) R 10782 29151 29150 0 -1 0 21307 0 0 0 63935 71 0 0 25 0 1 0 488383162 91123712 20855 4294967295 134512640 134672761 3221224544 3221223648 134559872 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22247 20855 603 41 0 22206 0
vsize: 88988
[startup+650.026 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 10783
Raw data (stat): 10783 (minisat+) R 10782 29151 29150 0 -1 0 21513 0 0 0 64934 72 0 0 25 0 1 0 488383162 91926528 21061 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22443 21061 603 41 0 22402 0
vsize: 89772
[startup+660.027 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 10783
Raw data (stat): 10783 (minisat+) R 10782 29151 29150 0 -1 0 21655 0 0 0 65933 73 0 0 25 0 1 0 488383162 92610560 21203 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22610 21203 603 41 0 22569 0
vsize: 90440
[startup+670.027 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 10783
Raw data (stat): 10783 (minisat+) R 10782 29151 29150 0 -1 0 21801 0 0 0 66933 74 0 0 25 0 1 0 488383162 93151232 21349 4294967295 134512640 134672761 3221224544 3221223680 134560590 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22742 21349 603 41 0 22701 0
vsize: 90968
[startup+680.027 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 10783
Raw data (stat): 10783 (minisat+) R 10782 29151 29150 0 -1 0 21955 0 0 0 67932 74 0 0 25 0 1 0 488383162 93827072 21503 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22907 21503 603 41 0 22866 0
vsize: 91628
[startup+690.027 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 10783
Raw data (stat): 10783 (minisat+) R 10782 29151 29150 0 -1 0 22149 0 0 0 68932 75 0 0 25 0 1 0 488383162 94642176 21697 4294967295 134512640 134672761 3221224544 3221223728 134559538 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23106 21697 603 41 0 23065 0
vsize: 92424
[startup+700.027 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 10783
Raw data (stat): 10783 (minisat+) R 10782 29151 29150 0 -1 0 22297 0 0 0 69932 75 0 0 25 0 1 0 488383162 95182848 21845 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23238 21845 603 41 0 23197 0
vsize: 92952
[startup+710.027 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 10783
Raw data (stat): 10783 (minisat+) R 10782 29151 29150 0 -1 0 22448 0 0 0 70931 76 0 0 25 0 1 0 488383162 95850496 21996 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23401 21996 603 41 0 23360 0
vsize: 93604
[startup+720.027 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 10783
Raw data (stat): 10783 (minisat+) R 10782 29151 29150 0 -1 0 22587 0 0 0 71931 77 0 0 25 0 1 0 488383162 96391168 22135 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23533 22135 603 41 0 23492 0
vsize: 94132
[startup+730.028 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 10783
Raw data (stat): 10783 (minisat+) R 10782 29151 29150 0 -1 0 22770 0 0 0 72931 77 0 0 25 0 1 0 488383162 97058816 22318 4294967295 134512640 134672761 3221224544 3221223712 134560839 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23696 22318 603 41 0 23655 0
vsize: 94784
[startup+740.029 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 10783
Raw data (stat): 10783 (minisat+) R 10782 29151 29150 0 -1 0 22985 0 0 0 73930 78 0 0 25 0 1 0 488383162 98004992 22533 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23927 22533 603 41 0 23886 0
vsize: 95708
[startup+750.029 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 10783
Raw data (stat): 10783 (minisat+) R 10782 29151 29150 0 -1 0 23193 0 0 0 74930 78 0 0 25 0 1 0 488383162 98807808 22741 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24123 22741 603 41 0 24082 0
vsize: 96492
[startup+760.03 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 10783
Raw data (stat): 10783 (minisat+) R 10782 29151 29150 0 -1 0 23417 0 0 0 75929 79 0 0 25 0 1 0 488383162 99758080 22965 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24355 22965 603 41 0 24314 0
vsize: 97420
[startup+770.03 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 10783
Raw data (stat): 10783 (minisat+) R 10782 29151 29150 0 -1 0 23656 0 0 0 76928 80 0 0 25 0 1 0 488383162 100700160 23204 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24585 23204 603 41 0 24544 0
vsize: 98340
[startup+780.031 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 10783
Raw data (stat): 10783 (minisat+) R 10782 29151 29150 0 -1 0 23864 0 0 0 77928 80 0 0 25 0 1 0 488383162 101646336 23412 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24816 23412 603 41 0 24775 0
vsize: 99264
[startup+790.031 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 10783
Raw data (stat): 10783 (minisat+) R 10782 29151 29150 0 -1 0 23929 0 0 0 78928 80 0 0 25 0 1 0 488383162 101916672 23477 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24882 23477 603 41 0 24841 0
vsize: 99528
[startup+800.031 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 10783
Raw data (stat): 10783 (minisat+) R 10782 29151 29150 0 -1 0 24090 0 0 0 79928 81 0 0 25 0 1 0 488383162 102453248 23638 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25013 23638 603 41 0 24972 0
vsize: 100052
[startup+810.032 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 10783
Raw data (stat): 10783 (minisat+) R 10782 29151 29150 0 -1 0 24294 0 0 0 80928 81 0 0 25 0 1 0 488383162 103391232 23842 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25242 23842 603 41 0 25201 0
vsize: 100968
[startup+820.032 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 10783
Raw data (stat): 10783 (minisat+) R 10782 29151 29150 0 -1 0 24381 0 0 0 81928 81 0 0 25 0 1 0 488383162 103657472 23929 4294967295 134512640 134672761 3221224544 3221223716 134556643 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25307 23929 603 41 0 25266 0
vsize: 101228
[startup+830.032 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 10783
Raw data (stat): 10783 (minisat+) R 10782 29151 29150 0 -1 0 24482 0 0 0 82927 82 0 0 25 0 1 0 488383162 104062976 24030 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25406 24030 603 41 0 25365 0
vsize: 101624
[startup+840.032 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 10783
Raw data (stat): 10783 (minisat+) R 10782 29151 29150 0 -1 0 24627 0 0 0 83927 82 0 0 25 0 1 0 488383162 104734720 24175 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25570 24175 603 41 0 25529 0
vsize: 102280
[startup+850.032 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 10783
Raw data (stat): 10783 (minisat+) R 10782 29151 29150 0 -1 0 24804 0 0 0 84927 83 0 0 25 0 1 0 488383162 105410560 24352 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25735 24352 603 41 0 25694 0
vsize: 102940
[startup+860.032 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 10783
Raw data (stat): 10783 (minisat+) R 10782 29151 29150 0 -1 0 25037 0 0 0 85926 83 0 0 25 0 1 0 488383162 106352640 24585 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25965 24585 603 41 0 25924 0
vsize: 103860
[startup+870.032 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 10783
Raw data (stat): 10783 (minisat+) R 10782 29151 29150 0 -1 0 25251 0 0 0 86926 84 0 0 25 0 1 0 488383162 107556864 24799 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26259 24799 603 41 0 26218 0
vsize: 105036
[startup+880.033 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 10783
Raw data (stat): 10783 (minisat+) R 10782 29151 29150 0 -1 0 25495 0 0 0 87925 85 0 0 25 0 1 0 488383162 108503040 25043 4294967295 134512640 134672761 3221224544 3221223712 134560895 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26490 25043 603 41 0 26449 0
vsize: 105960
[startup+890.032 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 10783
Raw data (stat): 10783 (minisat+) R 10782 29151 29150 0 -1 0 25684 0 0 0 88925 85 0 0 25 0 1 0 488383162 109314048 25232 4294967295 134512640 134672761 3221224544 3221223744 134557887 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26688 25232 603 41 0 26647 0
vsize: 106752
[startup+900.032 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 10783
Raw data (stat): 10783 (minisat+) R 10782 29151 29150 0 -1 0 25871 0 0 0 89925 86 0 0 25 0 1 0 488383162 109985792 25419 4294967295 134512640 134672761 3221224544 3221223712 134561027 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26852 25419 603 41 0 26811 0
vsize: 107408
[startup+910.033 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 10783
Raw data (stat): 10783 (minisat+) R 10782 29151 29150 0 -1 0 26062 0 0 0 90924 86 0 0 25 0 1 0 488383162 110796800 25610 4294967295 134512640 134672761 3221224544 3221223696 134560074 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27050 25610 603 41 0 27009 0
vsize: 108200
[startup+920.033 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 10783
Raw data (stat): 10783 (minisat+) R 10782 29151 29150 0 -1 0 26319 0 0 0 91924 87 0 0 25 0 1 0 488383162 111878144 25867 4294967295 134512640 134672761 3221224544 3221223712 134560956 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27314 25867 603 41 0 27273 0
vsize: 109256
[startup+930.033 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 10783
Raw data (stat): 10783 (minisat+) R 10782 29151 29150 0 -1 0 26736 0 0 0 92923 88 0 0 25 0 1 0 488383162 113623040 26284 4294967295 134512640 134672761 3221224544 3221223712 134560864 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27740 26284 603 41 0 27699 0
vsize: 110960
[startup+940.034 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 10783
Raw data (stat): 10783 (minisat+) R 10782 29151 29150 0 -1 0 27077 0 0 0 93922 89 0 0 25 0 1 0 488383162 114974720 26625 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28070 26625 603 41 0 28029 0
vsize: 112280
[startup+950.033 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 10783
Raw data (stat): 10783 (minisat+) R 10782 29151 29150 0 -1 0 27377 0 0 0 94922 90 0 0 25 0 1 0 488383162 116183040 26925 4294967295 134512640 134672761 3221224544 3221223692 134560631 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28365 26925 603 41 0 28324 0
vsize: 113460
[startup+960.033 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 10783
Raw data (stat): 10783 (minisat+) R 10782 29151 29150 0 -1 0 27846 0 0 0 95921 91 0 0 25 0 1 0 488383162 118071296 27394 4294967295 134512640 134672761 3221224544 3221223712 134560980 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28826 27394 603 41 0 28785 0
vsize: 115304
[startup+970.034 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 10783
Raw data (stat): 10783 (minisat+) R 10782 29151 29150 0 -1 0 28302 0 0 0 96920 92 0 0 25 0 1 0 488383162 119934976 27850 4294967295 134512640 134672761 3221224544 3221223648 134559949 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29281 27850 603 41 0 29240 0
vsize: 117124
[startup+980.035 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 10783
Raw data (stat): 10783 (minisat+) R 10782 29151 29150 0 -1 0 28663 0 0 0 97919 92 0 0 25 0 1 0 488383162 121417728 28211 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29643 28211 603 41 0 29602 0
vsize: 118572
[startup+990.035 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 10783
Raw data (stat): 10783 (minisat+) R 10782 29151 29150 0 -1 0 29070 0 0 0 98917 94 0 0 25 0 1 0 488383162 123174912 28618 4294967295 134512640 134672761 3221224544 3221223744 134557895 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30072 28618 603 41 0 30031 0
vsize: 120288
[startup+1000.04 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 10783
Raw data (stat): 10783 (minisat+) R 10782 29151 29150 0 -1 0 29529 0 0 0 99917 95 0 0 25 0 1 0 488383162 125063168 29077 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30533 29077 603 41 0 30492 0
vsize: 122132
[startup+1010.04 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 10783
Raw data (stat): 10783 (minisat+) R 10782 29151 29150 0 -1 0 29931 0 0 0 100916 96 0 0 25 0 1 0 488383162 126676992 29479 4294967295 134512640 134672761 3221224544 3221223712 134560895 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30927 29479 603 41 0 30886 0
vsize: 123708
[startup+1020.04 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 10783
Raw data (stat): 10783 (minisat+) R 10782 29151 29150 0 -1 0 30319 0 0 0 101914 98 0 0 25 0 1 0 488383162 128290816 29867 4294967295 134512640 134672761 3221224544 3221223712 134560888 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31321 29867 603 41 0 31280 0
vsize: 125284
[startup+1030.04 s]
Raw data (loadavg): 1.00 0.99 0.93 2/55 10784
Raw data (stat): 10783 (minisat+) R 10782 29151 29150 0 -1 0 30684 0 0 0 102914 98 0 0 25 0 1 0 488383162 129765376 30232 4294967295 134512640 134672761 3221224544 3221223712 134561220 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31681 30232 603 41 0 31640 0
vsize: 126724
[startup+1040.04 s]
Raw data (loadavg): 1.07 1.00 0.94 2/54 10836
Raw data (stat): 10783 (minisat+) R 10782 29151 29150 0 -1 0 31107 0 0 0 103913 99 0 0 25 0 1 0 488383162 131518464 30655 4294967295 134512640 134672761 3221224544 3221223544 1075350517 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32109 30655 603 41 0 32068 0
vsize: 128436
[startup+1050.04 s]
Raw data (loadavg): 1.06 1.00 0.94 2/54 10836
Raw data (stat): 10783 (minisat+) R 10782 29151 29150 0 -1 0 31495 0 0 0 104911 101 0 0 25 0 1 0 488383162 133005312 31043 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32472 31043 603 41 0 32431 0
vsize: 129888
[startup+1060.04 s]
Raw data (loadavg): 1.05 1.00 0.94 2/54 10836
Raw data (stat): 10783 (minisat+) R 10782 29151 29150 0 -1 0 31891 0 0 0 105910 103 0 0 25 0 1 0 488383162 134619136 31439 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32866 31439 603 41 0 32825 0
vsize: 131464
[startup+1070.04 s]
Raw data (loadavg): 1.04 1.00 0.94 2/54 10836
Raw data (stat): 10783 (minisat+) R 10782 29151 29150 0 -1 0 32299 0 0 0 106910 103 0 0 25 0 1 0 488383162 136376320 31847 4294967295 134512640 134672761 3221224544 3221223684 134560556 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33295 31847 603 41 0 33254 0
vsize: 133180
[startup+1080.04 s]
Raw data (loadavg): 1.04 1.00 0.94 2/54 10836
Raw data (stat): 10783 (minisat+) R 10782 29151 29150 0 -1 0 32663 0 0 0 107908 104 0 0 25 0 1 0 488383162 137863168 32211 4294967295 134512640 134672761 3221224544 3221223648 134560048 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33658 32211 603 41 0 33617 0
vsize: 134632
[startup+1090.04 s]
Raw data (loadavg): 1.03 1.00 0.94 2/54 10836
Raw data (stat): 10783 (minisat+) R 10782 29151 29150 0 -1 0 33058 0 0 0 108908 106 0 0 25 0 1 0 488383162 139485184 32606 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 34054 32606 603 41 0 34013 0
vsize: 136216
[startup+1100.04 s]
Raw data (loadavg): 1.02 1.00 0.94 2/54 10836
Raw data (stat): 10783 (minisat+) R 10782 29151 29150 0 -1 0 33469 0 0 0 109907 107 0 0 25 0 1 0 488383162 141103104 33017 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 34449 33017 603 41 0 34408 0
vsize: 137796
[startup+1110.04 s]
Raw data (loadavg): 1.02 1.00 0.94 2/54 10838
Raw data (stat): 10783 (minisat+) R 10782 29151 29150 0 -1 0 33823 0 0 0 110906 107 0 0 25 0 1 0 488383162 142581760 33371 4294967295 134512640 134672761 3221224544 3221223712 134561164 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 34810 33371 603 41 0 34769 0
vsize: 139240
[startup+1120.04 s]
Raw data (loadavg): 1.02 1.00 0.94 2/54 10838
Raw data (stat): 10783 (minisat+) R 10782 29151 29150 0 -1 0 34258 0 0 0 111905 109 0 0 25 0 1 0 488383162 144338944 33806 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 35239 33806 603 41 0 35198 0
vsize: 140956
[startup+1130.04 s]
Raw data (loadavg): 1.01 1.00 0.94 2/54 10838
Raw data (stat): 10783 (minisat+) R 10782 29151 29150 0 -1 0 34698 0 0 0 112904 110 0 0 25 0 1 0 488383162 146219008 34246 4294967295 134512640 134672761 3221224544 3221223712 134560988 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 35698 34247 603 41 0 35657 0
vsize: 142792
[startup+1140.04 s]
Raw data (loadavg): 1.01 1.00 0.94 2/54 10838
Raw data (stat): 10783 (minisat+) R 10782 29151 29150 0 -1 0 35036 0 0 0 113904 110 0 0 25 0 1 0 488383162 147570688 34584 4294967295 134512640 134672761 3221224544 3221223712 134561161 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 36028 34584 603 41 0 35987 0
vsize: 144112
[startup+1150.04 s]
Raw data (loadavg): 1.01 1.00 0.94 2/54 10838
Raw data (stat): 10783 (minisat+) R 10782 29151 29150 0 -1 0 35329 0 0 0 114903 111 0 0 25 0 1 0 488383162 148783104 34877 4294967295 134512640 134672761 3221224544 3221223728 134559332 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 36324 34877 603 41 0 36283 0
vsize: 145296
[startup+1160.04 s]
Raw data (loadavg): 1.01 1.00 0.94 2/54 10838
Raw data (stat): 10783 (minisat+) R 10782 29151 29150 0 -1 0 35580 0 0 0 115902 112 0 0 25 0 1 0 488383162 149725184 35128 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 36554 35128 603 41 0 36513 0
vsize: 146216
[startup+1170.04 s]
Raw data (loadavg): 1.01 1.00 0.94 2/54 10838
Raw data (stat): 10783 (minisat+) R 10782 29151 29150 0 -1 0 35860 0 0 0 116901 113 0 0 25 0 1 0 488383162 150929408 35408 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 36848 35408 603 41 0 36807 0
vsize: 147392
[startup+1180.04 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 10838
Raw data (stat): 10783 (minisat+) R 10782 29151 29150 0 -1 0 36137 0 0 0 117901 114 0 0 25 0 1 0 488383162 152006656 35685 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 37111 35685 603 41 0 37070 0
vsize: 148444
[startup+1190.05 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 10838
Raw data (stat): 10783 (minisat+) R 10782 29151 29150 0 -1 0 36435 0 0 0 118901 114 0 0 25 0 1 0 488383162 153214976 35983 4294967295 134512640 134672761 3221224544 3221223728 134558662 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 37406 35983 603 41 0 37365 0
vsize: 149624
[startup+1200.04 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 10838
Raw data (stat): 10783 (minisat+) R 10782 29151 29150 0 -1 0 36742 0 0 0 119900 115 0 0 25 0 1 0 488383162 154558464 36290 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 37734 36290 603 41 0 37693 0
vsize: 150936
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.12 s]
Raw data (loadavg): 1.00 1.00 0.94 1/54 10838
Raw data (stat): 10783 (minisat+) Z 10782 29151 29150 0 -1 12 36744 0 0 0 119900 122 0 0 25 0 1 0 488383162 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.23
CPU user time (s): 1199
CPU system time (s): 1.22181
CPU usage (%): 100.009
Max. virtual memory (Kb): 150936
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####