PB'05 competition: run trace

Some explanations

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

Name	normalized-opb/mps-v2-20-10/MIPLIB/miplib2003/normalized-mps-v2-20-10-aflow40b.opb
MD5SUM	64cd8dd71c00255f05a721f3d3f16ae5
Bench Category	optimization, medium integers (OPTMEDINT)
Has Objective Function	YES
Satisfiable
(Un)Satisfiability was proved
Best value of the objective function
Optimality of the best value was proved
Number of terms in the objective function	1364
Biggest coefficient in the objective function	500
Number of bits for the biggest coefficient in the objective function	9
Sum of the numbers in the objective function	230637
Number of bits of the sum of numbers in the objective function	18
Biggest number in a constraint	102400
Number of bits of the biggest number in a constraint	17
Biggest sum of numbers in a constraint	7037881
Number of bits of the biggest sum of numbers	23
Best result obtained on this benchmark
Best CPU time to get the best result obtained on this benchmark
Number of variables	23384
Total number of constraints	4170
Number of constraints which are clauses	0
Number of constraints which are cardinality constraints (but not clauses)	1403
Number of constraints which are nor clauses,nor cardinality constraints	2767
Minimum length of a constraint	1
Maximum length of a constraint	1202
Trace number 21889

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

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.050
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:        309832 kB
Buffers:         22088 kB
Cached:         680364 kB
SwapCached:        328 kB
Active:          50536 kB
Inactive:       654496 kB
HighTotal:      131008 kB
HighFree:        35644 kB
LowTotal:       903652 kB
LowFree:        274188 kB
SwapTotal:     2097136 kB
SwapFree:      2096520 kB
Dirty:              40 kB
Writeback:           0 kB
Mapped:           6460 kB
Slab:            14036 kB
Committed_AS:    63596 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-22 01:41:59 (client local time) WITH STATUS 0 IN 1200.25 SECONDS
stats: 12428 7 1200.25 0
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 2884 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: ##############################################################################
c   -- Clauses(.)/Splits(s): ssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssss
c ---[3067]---> BDD-cost:   16
c ---[3066]---> BDD-cost:   16
c ---[3064]---> BDD-cost:   15
c ---[3063]---> BDD-cost:   16
c ---[3062]---> BDD-cost:   15
c ---[3061]---> BDD-cost:   14
c ---[3060]---> BDD-cost:   16
c ---[3059]---> BDD-cost:   16
c ---[3058]---> BDD-cost:   14
c ---[3056]---> BDD-cost:   14
c ---[3055]---> BDD-cost:   15
c ---[3053]---> BDD-cost:   16
c ---[3052]---> BDD-cost:   16
c ---[3051]---> BDD-cost:   13
c ---[3049]---> BDD-cost:   15
c ---[3048]---> BDD-cost:   16
c ---[3047]---> BDD-cost:   15
c ---[3046]---> BDD-cost:   16
c ---[3045]---> BDD-cost:   16
c ---[3044]---> BDD-cost:   16
c ---[3042]---> BDD-cost:   15
c ---[3040]---> BDD-cost:   14
c ---[3039]---> BDD-cost:   15
c ---[3038]---> BDD-cost:   15
c ---[3037]---> BDD-cost:   15
c ---[3036]---> BDD-cost:   15
c ---[3035]---> BDD-cost:   14
c ---[3034]---> BDD-cost:   14
c ---[3033]---> BDD-cost:   14
c ---[3032]---> BDD-cost:   16
c ---[3030]---> BDD-cost:   13
c ---[3028]---> BDD-cost:   14
c ---[3026]---> BDD-cost:   16
c ---[3025]---> BDD-cost:   16
c ---[3024]---> BDD-cost:   15
c ---[3023]---> BDD-cost:   16
c ---[3022]---> BDD-cost:   16
c ---[3021]---> BDD-cost:   16
c ---[3020]---> BDD-cost:   16
c ---[3019]---> BDD-cost:   15
c ---[3018]---> BDD-cost:   15
c ---[3017]---> BDD-cost:   14
c ---[3016]---> BDD-cost:   16
c ---[3015]---> BDD-cost:   16
c ---[3014]---> BDD-cost:   14
c ---[3013]---> BDD-cost:   16
c ---[3012]---> BDD-cost:   14
c ---[3011]---> BDD-cost:   14
c ---[3010]---> BDD-cost:   14
c ---[3009]---> BDD-cost:   16
c ---[3008]---> BDD-cost:   14
c ---[3007]---> BDD-cost:   16
c ---[3005]---> BDD-cost:   16
c ---[3004]---> BDD-cost:   16
c ---[3003]---> BDD-cost:   16
c ---[3002]---> BDD-cost:   15
c ---[3001]---> BDD-cost:   16
c ---[3000]---> BDD-cost:   15
c ---[2999]---> BDD-cost:   15
c ---[2998]---> BDD-cost:   15
c ---[2997]---> BDD-cost:   16
c ---[2996]---> BDD-cost:   15
c ---[2995]---> BDD-cost:   15
c ---[2994]---> BDD-cost:   16
c ---[2993]---> BDD-cost:   16
c ---[2992]---> BDD-cost:   16
c ---[2991]---> BDD-cost:   15
c ---[2990]---> BDD-cost:   16
c ---[2989]---> BDD-cost:   14
c ---[2988]---> BDD-cost:   13
c ---[2987]---> BDD-cost:   15
c ---[2986]---> BDD-cost:   15
c ---[2985]---> BDD-cost:   16
c ---[2984]---> BDD-cost:   14
c ---[2983]---> BDD-cost:   14
c ---[2982]---> BDD-cost:   16
c ---[2981]---> BDD-cost:   16
c ---[2980]---> BDD-cost:   16
c ---[2979]---> BDD-cost:   15
c ---[2978]---> BDD-cost:   15
c ---[2977]---> BDD-cost:   16
c ---[2976]---> BDD-cost:   15
c ---[2975]---> BDD-cost:   15
c ---[2974]---> BDD-cost:   16
c ---[2973]---> BDD-cost:   15
c ---[2972]---> BDD-cost:   15
c ---[2971]---> BDD-cost:   15
c ---[2969]---> BDD-cost:   16
c ---[2968]---> BDD-cost:   16
c ---[2967]---> BDD-cost:   15
c ---[2966]---> BDD-cost:   15
c ---[2965]---> BDD-cost:   15
c ---[2964]---> BDD-cost:   16
c ---[2963]---> BDD-cost:   16
c ---[2962]---> BDD-cost:   14
c ---[2961]---> BDD-cost:   16
c ---[2960]---> BDD-cost:   16
c ---[2959]---> BDD-cost:   14
c ---[2958]---> BDD-cost:   14
c ---[2955]---> BDD-cost:   16
c ---[2954]---> BDD-cost:   14
c ---[2953]---> BDD-cost:   16
c ---[2952]---> BDD-cost:   16
c ---[2951]---> BDD-cost:   15
c ---[2950]---> BDD-cost:   15
c ---[2949]---> BDD-cost:   15
c ---[2948]---> BDD-cost:   16
c ---[2947]---> BDD-cost:   15
c ---[2946]---> BDD-cost:   16
c ---[2945]---> BDD-cost:   15
c ---[2943]---> BDD-cost:   15
c ---[2942]---> BDD-cost:   16
c ---[2941]---> BDD-cost:   13
c ---[2940]---> BDD-cost:   16
c ---[2939]---> BDD-cost:   16
c ---[2938]---> BDD-cost:   16
c ---[2937]---> BDD-cost:   15
c ---[2935]---> BDD-cost:   15
c ---[2934]---> BDD-cost:   14
c ---[2933]---> BDD-cost:   16
c ---[2932]---> BDD-cost:   13
c ---[2930]---> BDD-cost:   15
c ---[2929]---> BDD-cost:   16
c ---[2928]---> BDD-cost:   16
c ---[2927]---> BDD-cost:   16
c ---[2926]---> BDD-cost:   16
c ---[2925]---> BDD-cost:   14
c ---[2924]---> BDD-cost:   16
c ---[2923]---> BDD-cost:   15
c ---[2922]---> BDD-cost:   16
c ---[2921]---> BDD-cost:   16
c ---[2919]---> BDD-cost:   15
c ---[2918]---> BDD-cost:   16
c ---[2917]---> BDD-cost:   15
c ---[2916]---> BDD-cost:   16
c ---[2915]---> BDD-cost:   13
c ---[2914]---> BDD-cost:   16
c ---[2913]---> BDD-cost:   15
c ---[2912]---> BDD-cost:   16
c ---[2911]---> BDD-cost:   14
c ---[2909]---> BDD-cost:   16
c ---[2907]---> BDD-cost:   16
c ---[2906]---> BDD-cost:   16
c ---[2905]---> BDD-cost:   14
c ---[2904]---> BDD-cost:   14
c ---[2902]---> BDD-cost:   16
c ---[2901]---> BDD-cost:   16
c ---[2900]---> BDD-cost:   16
c ---[2899]---> BDD-cost:   15
c ---[2898]---> BDD-cost:   16
c ---[2897]---> BDD-cost:   16
c ---[2896]---> BDD-cost:   15
c ---[2895]---> BDD-cost:   16
c ---[2894]---> BDD-cost:   14
c ---[2893]---> BDD-cost:   16
c ---[2892]---> BDD-cost:   16
c ---[2890]---> BDD-cost:   16
c ---[2889]---> BDD-cost:   15
c ---[2888]---> BDD-cost:   16
c ---[2887]---> BDD-cost:   13
c ---[2886]---> BDD-cost:   16
c ---[2884]---> BDD-cost:   16
c ---[2882]---> BDD-cost:   15
c ---[2881]---> BDD-cost:   16
c ---[2879]---> BDD-cost:   14
c ---[2877]---> BDD-cost:   15
c ---[2876]---> BDD-cost:   16
c ---[2875]---> BDD-cost:   16
c ---[2874]---> BDD-cost:   16
c ---[2873]---> BDD-cost:   16
c ---[2872]---> BDD-cost:   16
c ---[2871]---> BDD-cost:   16
c ---[2870]---> BDD-cost:   15
c ---[2869]---> BDD-cost:   16
c ---[2868]---> BDD-cost:   15
c ---[2866]---> BDD-cost:   16
c ---[2865]---> BDD-cost:   16
c ---[2864]---> BDD-cost:   14
c ---[2863]---> BDD-cost:   14
c ---[2862]---> BDD-cost:   14
c ---[2861]---> BDD-cost:   15
c ---[2860]---> BDD-cost:   15
c ---[2859]---> BDD-cost:   16
c ---[2858]---> BDD-cost:   16
c ---[2856]---> BDD-cost:   16
c ---[2855]---> BDD-cost:   15
c ---[2854]---> BDD-cost:   15
c ---[2853]---> BDD-cost:   15
c ---[2852]---> BDD-cost:   13
c ---[2851]---> BDD-cost:   14
c ---[2850]---> BDD-cost:   13
c ---[2849]---> BDD-cost:   15
c ---[2847]---> BDD-cost:   15
c ---[2846]---> BDD-cost:   13
c ---[2845]---> BDD-cost:   16
c ---[2844]---> BDD-cost:   16
c ---[2843]---> BDD-cost:   14
c ---[2842]---> BDD-cost:   16
c ---[2841]---> BDD-cost:   16
c ---[2840]---> BDD-cost:   16
c ---[2839]---> BDD-cost:   16
c ---[2838]---> BDD-cost:   15
c ---[2837]---> BDD-cost:   14
c ---[2836]---> BDD-cost:   14
c ---[2835]---> BDD-cost:   15
c ---[2834]---> BDD-cost:   16
c ---[2833]---> BDD-cost:   15
c ---[2832]---> BDD-cost:   14
c ---[2831]---> BDD-cost:   14
c ---[2830]---> BDD-cost:   15
c ---[2829]---> BDD-cost:   16
c ---[2828]---> BDD-cost:   14
c ---[2827]---> BDD-cost:   14
c ---[2826]---> BDD-cost:   16
c ---[2825]---> BDD-cost:   16
c ---[2824]---> BDD-cost:   14
c ---[2823]---> BDD-cost:   15
c ---[2822]---> BDD-cost:   16
c ---[2821]---> BDD-cost:   13
c ---[2820]---> BDD-cost:   16
c ---[2819]---> BDD-cost:   16
c ---[2817]---> BDD-cost:   16
c ---[2816]---> BDD-cost:   15
c ---[2815]---> BDD-cost:   13
c ---[2814]---> BDD-cost:   15
c ---[2813]---> BDD-cost:   15
c ---[2812]---> BDD-cost:   16
c ---[2811]---> BDD-cost:   14
c ---[2810]---> BDD-cost:   16
c ---[2808]---> BDD-cost:   16
c ---[2806]---> BDD-cost:   15
c ---[2805]---> BDD-cost:   14
c ---[2803]---> BDD-cost:   14
c ---[2802]---> BDD-cost:   16
c ---[2801]---> BDD-cost:   15
c ---[2800]---> BDD-cost:   16
c ---[2797]---> BDD-cost:   16
c ---[2796]---> BDD-cost:   15
c ---[2795]---> BDD-cost:   13
c ---[2794]---> BDD-cost:   16
c ---[2793]---> BDD-cost:   16
c ---[2792]---> BDD-cost:   16
c ---[2791]---> BDD-cost:   14
c ---[2790]---> BDD-cost:   16
c ---[2789]---> BDD-cost:   16
c ---[2788]---> BDD-cost:   16
c ---[2787]---> BDD-cost:   14
c ---[2786]---> BDD-cost:   16
c ---[2785]---> BDD-cost:   14
c ---[2784]---> BDD-cost:   15
c ---[2783]---> BDD-cost:   13
c ---[2781]---> BDD-cost:   16
c ---[2780]---> BDD-cost:   16
c ---[2779]---> BDD-cost:   15
c ---[2778]---> BDD-cost:   15
c ---[2777]---> BDD-cost:   16
c ---[2776]---> BDD-cost:   16
c ---[2775]---> BDD-cost:   16
c ---[2774]---> BDD-cost:   16
c ---[2773]---> BDD-cost:   16
c ---[2772]---> BDD-cost:   16
c ---[2771]---> BDD-cost:   16
c ---[2769]---> BDD-cost:   16
c ---[2768]---> BDD-cost:   16
c ---[2767]---> BDD-cost:   14
c ---[2766]---> BDD-cost:   15
c ---[2765]---> BDD-cost:   15
c ---[2764]---> BDD-cost:   16
c ---[2763]---> BDD-cost:   16
c ---[2762]---> BDD-cost:   16
c ---[2761]---> BDD-cost:   15
c ---[2760]---> BDD-cost:   15
c ---[2759]---> BDD-cost:   15
c ---[2758]---> BDD-cost:   16
c ---[2757]---> BDD-cost:   15
c ---[2756]---> BDD-cost:   16
c ---[2755]---> BDD-cost:   15
c ---[2754]---> BDD-cost:   16
c ---[2753]---> BDD-cost:   16
c ---[2752]---> BDD-cost:   13
c ---[2751]---> BDD-cost:   16
c ---[2750]---> BDD-cost:   14
c ---[2748]---> BDD-cost:   13
c ---[2747]---> BDD-cost:   16
c ---[2746]---> BDD-cost:   16
c ---[2744]---> BDD-cost:   13
c ---[2743]---> BDD-cost:   15
c ---[2742]---> BDD-cost:   16
c ---[2741]---> BDD-cost:   16
c ---[2740]---> BDD-cost:   16
c ---[2739]---> BDD-cost:   15
c ---[2737]---> BDD-cost:   16
c ---[2736]---> BDD-cost:   16
c ---[2735]---> BDD-cost:   15
c ---[2734]---> BDD-cost:   14
c ---[2733]---> BDD-cost:   16
c ---[2732]---> BDD-cost:   16
c ---[2731]---> BDD-cost:   16
c ---[2730]---> BDD-cost:   16
c ---[2728]---> BDD-cost:   16
c ---[2727]---> BDD-cost:   16
c ---[2726]---> BDD-cost:   16
c ---[2724]---> BDD-cost:   16
c ---[2723]---> BDD-cost:   15
c ---[2722]---> BDD-cost:   16
c ---[2721]---> BDD-cost:   16
c ---[2720]---> BDD-cost:   16
c ---[2719]---> BDD-cost:   15
c ---[2718]---> BDD-cost:   16
c ---[2717]---> BDD-cost:   14
c ---[2716]---> BDD-cost:   16
c ---[2715]---> BDD-cost:   15
c ---[2714]---> BDD-cost:   16
c ---[2712]---> BDD-cost:   16
c ---[2710]---> BDD-cost:   16
c ---[2709]---> BDD-cost:   16
c ---[2708]---> BDD-cost:   13
c ---[2706]---> BDD-cost:   16
c ---[2705]---> BDD-cost:   16
c ---[2704]---> BDD-cost:   15
c ---[2703]---> BDD-cost:   16
c ---[2701]---> BDD-cost:   16
c ---[2700]---> BDD-cost:   15
c ---[2699]---> BDD-cost:   15
c ---[2698]---> BDD-cost:   16
c ---[2697]---> BDD-cost:   16
c ---[2696]---> BDD-cost:   16
c ---[2695]---> BDD-cost:   16
c ---[2694]---> BDD-cost:   16
c ---[2693]---> BDD-cost:   16
c ---[2692]---> BDD-cost:   16
c ---[2691]---> BDD-cost:   14
c ---[2690]---> BDD-cost:   16
c ---[2689]---> BDD-cost:   15
c ---[2688]---> BDD-cost:   16
c ---[2687]---> BDD-cost:   16
c ---[2686]---> BDD-cost:   15
c ---[2685]---> BDD-cost:   15
c ---[2684]---> BDD-cost:   16
c ---[2683]---> BDD-cost:   16
c ---[2682]---> BDD-cost:   16
c ---[2681]---> BDD-cost:   14
c ---[2680]---> BDD-cost:   14
c ---[2679]---> BDD-cost:   16
c ---[2678]---> BDD-cost:   15
c ---[2677]---> BDD-cost:   15
c ---[2675]---> BDD-cost:   16
c ---[2674]---> BDD-cost:   16
c ---[2673]---> BDD-cost:   16
c ---[2672]---> BDD-cost:   15
c ---[2671]---> BDD-cost:   14
c ---[2670]---> BDD-cost:   15
c ---[2669]---> BDD-cost:   16
c ---[2668]---> BDD-cost:   13
c ---[2667]---> BDD-cost:   16
c ---[2665]---> BDD-cost:   15
c ---[2664]---> BDD-cost:   14
c ---[2662]---> BDD-cost:   16
c ---[2661]---> BDD-cost:   14
c ---[2660]---> BDD-cost:   14
c ---[2659]---> BDD-cost:   16
c ---[2658]---> BDD-cost:   15
c ---[2656]---> BDD-cost:   16
c ---[2654]---> BDD-cost:   16
c ---[2653]---> BDD-cost:   14
c ---[2652]---> BDD-cost:   15
c ---[2651]---> BDD-cost:   16
c ---[2650]---> BDD-cost:   15
c ---[2648]---> BDD-cost:   15
c ---[2647]---> BDD-cost:   14
c ---[2646]---> BDD-cost:   13
c ---[2645]---> BDD-cost:   15
c ---[2644]---> BDD-cost:   15
c ---[2643]---> BDD-cost:   15
c ---[2642]---> BDD-cost:   15
c ---[2641]---> BDD-cost:   16
c ---[2638]---> BDD-cost:   16
c ---[2637]---> BDD-cost:   15
c ---[2636]---> BDD-cost:   14
c ---[2635]---> BDD-cost:   14
c ---[2634]---> BDD-cost:   13
c ---[2633]---> BDD-cost:   16
c ---[2632]---> BDD-cost:   14
c ---[2631]---> BDD-cost:   15
c ---[2630]---> BDD-cost:   16
c ---[2629]---> BDD-cost:   14
c ---[2628]---> BDD-cost:   15
c ---[2627]---> BDD-cost:   16
c ---[2626]---> BDD-cost:   16
c ---[2625]---> BDD-cost:   15
c ---[2624]---> BDD-cost:   15
c ---[2623]---> BDD-cost:   16
c ---[2622]---> BDD-cost:   16
c ---[2621]---> BDD-cost:   16
c ---[2620]---> BDD-cost:   16
c ---[2619]---> BDD-cost:   14
c ---[2618]---> BDD-cost:   16
c ---[2617]---> BDD-cost:   15
c ---[2616]---> BDD-cost:   16
c ---[2615]---> BDD-cost:   16
c ---[2614]---> BDD-cost:   16
c ---[2613]---> BDD-cost:   15
c ---[2612]---> BDD-cost:   16
c ---[2611]---> BDD-cost:   16
c ---[2610]---> BDD-cost:   15
c ---[2609]---> BDD-cost:   15
c ---[2608]---> BDD-cost:   15
c ---[2606]---> BDD-cost:   15
c ---[2604]---> BDD-cost:   14
c ---[2603]---> BDD-cost:   15
c ---[2602]---> BDD-cost:   16
c ---[2601]---> BDD-cost:   16
c ---[2600]---> BDD-cost:   14
c ---[2599]---> BDD-cost:   16
c ---[2598]---> BDD-cost:   16
c ---[2597]---> BDD-cost:   14
c ---[2596]---> BDD-cost:   16
c ---[2595]---> BDD-cost:   16
c ---[2594]---> BDD-cost:   15
c ---[2593]---> BDD-cost:   16
c ---[2592]---> BDD-cost:   14
c ---[2591]---> BDD-cost:   16
c ---[2590]---> BDD-cost:   15
c ---[2589]---> BDD-cost:   16
c ---[2587]---> BDD-cost:   15
c ---[2586]---> BDD-cost:   16
c ---[2584]---> BDD-cost:   15
c ---[2583]---> BDD-cost:   16
c ---[2582]---> BDD-cost:   16
c ---[2581]---> BDD-cost:   16
c ---[2580]---> BDD-cost:   13
c ---[2579]---> BDD-cost:   14
c ---[2576]---> BDD-cost:   16
c ---[2575]---> BDD-cost:   16
c ---[2574]---> BDD-cost:   16
c ---[2572]---> BDD-cost:   14
c ---[2571]---> BDD-cost:   16
c ---[2570]---> BDD-cost:   16
c ---[2569]---> BDD-cost:   14
c ---[2568]---> BDD-cost:   16
c ---[2567]---> BDD-cost:   13
c ---[2566]---> BDD-cost:   15
c ---[2565]---> BDD-cost:   15
c ---[2564]---> BDD-cost:   16
c ---[2563]---> BDD-cost:   16
c ---[2562]---> BDD-cost:   16
c ---[2561]---> BDD-cost:   15
c ---[2559]---> BDD-cost:   15
c ---[2558]---> BDD-cost:   15
c ---[2557]---> BDD-cost:   16
c ---[2556]---> BDD-cost:   16
c ---[2554]---> BDD-cost:   14
c ---[2553]---> BDD-cost:   15
c ---[2550]---> BDD-cost:   15
c ---[2549]---> BDD-cost:   15
c ---[2548]---> BDD-cost:   14
c ---[2546]---> BDD-cost:   16
c ---[2545]---> BDD-cost:   13
c ---[2543]---> BDD-cost:   15
c ---[2541]---> BDD-cost:   16
c ---[2540]---> BDD-cost:   14
c ---[2539]---> BDD-cost:   16
c ---[2538]---> BDD-cost:   16
c ---[2537]---> BDD-cost:   16
c ---[2535]---> BDD-cost:   15
c ---[2533]---> BDD-cost:   15
c ---[2532]---> BDD-cost:   16
c ---[2531]---> BDD-cost:   14
c ---[2530]---> BDD-cost:   16
c ---[2529]---> BDD-cost:   15
c ---[2528]---> BDD-cost:   16
c ---[2527]---> BDD-cost:   16
c ---[2526]---> BDD-cost:   15
c ---[2524]---> BDD-cost:   16
c ---[2523]---> BDD-cost:   15
c ---[2522]---> BDD-cost:   16
c ---[2520]---> BDD-cost:   13
c ---[2519]---> BDD-cost:   15
c ---[2518]---> BDD-cost:   15
c ---[2517]---> BDD-cost:   16
c ---[2516]---> BDD-cost:   16
c ---[2515]---> BDD-cost:   15
c ---[2514]---> BDD-cost:   15
c ---[2513]---> BDD-cost:   15
c ---[2512]---> BDD-cost:   15
c ---[2511]---> BDD-cost:   16
c ---[2510]---> BDD-cost:   14
c ---[2509]---> BDD-cost:   16
c ---[2507]---> BDD-cost:   15
c ---[2506]---> BDD-cost:   15
c ---[2505]---> BDD-cost:   15
c ---[2504]---> BDD-cost:   16
c ---[2503]---> BDD-cost:   15
c ---[2502]---> BDD-cost:   16
c ---[2499]---> BDD-cost:   14
c ---[2498]---> BDD-cost:   16
c ---[2497]---> BDD-cost:   16
c ---[2495]---> BDD-cost:   16
c ---[2491]---> BDD-cost:   16
c ---[2489]---> BDD-cost:   15
c ---[2488]---> BDD-cost:   15
c ---[2484]---> BDD-cost:   15
c ---[2483]---> BDD-cost:   16
c ---[2482]---> BDD-cost:   16
c ---[2481]---> BDD-cost:   14
c ---[2479]---> BDD-cost:   13
c ---[2477]---> BDD-cost:   15
c ---[2476]---> BDD-cost:   16
c ---[2475]---> BDD-cost:   16
c ---[2474]---> BDD-cost:   16
c ---[2473]---> BDD-cost:   14
c ---[2472]---> BDD-cost:   16
c ---[2471]---> BDD-cost:   15
c ---[2470]---> BDD-cost:   16
c ---[2469]---> BDD-cost:   15
c ---[2468]---> BDD-cost:   15
c ---[2467]---> BDD-cost:   15
c ---[2466]---> BDD-cost:   16
c ---[2464]---> BDD-cost:   14
c ---[2463]---> BDD-cost:   15
c ---[2462]---> BDD-cost:   15
c ---[2460]---> BDD-cost:   14
c ---[2459]---> BDD-cost:   16
c ---[2457]---> BDD-cost:   14
c ---[2456]---> BDD-cost:   14
c ---[2454]---> BDD-cost:   16
c ---[2453]---> BDD-cost:   13
c ---[2451]---> BDD-cost:   16
c ---[2450]---> BDD-cost:   16
c ---[2449]---> BDD-cost:   16
c ---[2447]---> BDD-cost:   15
c ---[2446]---> BDD-cost:   16
c ---[2445]---> BDD-cost:   15
c ---[2444]---> BDD-cost:   13
c ---[2443]---> BDD-cost:   16
c ---[2442]---> BDD-cost:   16
c ---[2440]---> BDD-cost:   15
c ---[2439]---> BDD-cost:   16
c ---[2438]---> BDD-cost:   15
c ---[2437]---> BDD-cost:   15
c ---[2436]---> BDD-cost:   14
c ---[2435]---> BDD-cost:   16
c ---[2434]---> BDD-cost:   16
c ---[2433]---> BDD-cost:   16
c ---[2432]---> BDD-cost:   16
c ---[2431]---> BDD-cost:   16
c ---[2430]---> BDD-cost:   15
c ---[2429]---> BDD-cost:   16
c ---[2428]---> BDD-cost:   15
c ---[2427]---> BDD-cost:   16
c ---[2426]---> BDD-cost:   16
c ---[2425]---> BDD-cost:   15
c ---[2424]---> BDD-cost:   16
c ---[2423]---> BDD-cost:   14
c ---[2422]---> BDD-cost:   15
c ---[2421]---> BDD-cost:   13
c ---[2419]---> BDD-cost:   14
c ---[2418]---> BDD-cost:   14
c ---[2417]---> BDD-cost:   15
c ---[2416]---> BDD-cost:   16
c ---[2415]---> BDD-cost:   15
c ---[2413]---> BDD-cost:   15
c ---[2412]---> BDD-cost:   16
c ---[2410]---> BDD-cost:   16
c ---[2409]---> BDD-cost:   16
c ---[2408]---> BDD-cost:   14
c ---[2407]---> BDD-cost:   16
c ---[2406]---> BDD-cost:   14
c ---[2405]---> BDD-cost:   16
c ---[2404]---> BDD-cost:   15
c ---[2403]---> BDD-cost:   16
c ---[2402]---> BDD-cost:   14
c ---[2401]---> BDD-cost:   16
c ---[2400]---> BDD-cost:   15
c ---[2399]---> BDD-cost:   16
c ---[2398]---> BDD-cost:   13
c ---[2397]---> BDD-cost:   15
c ---[2396]---> BDD-cost:   15
c ---[2395]---> BDD-cost:   16
c ---[2394]---> BDD-cost:   15
c ---[2393]---> BDD-cost:   13
c ---[2392]---> BDD-cost:   16
c ---[2390]---> BDD-cost:   15
c ---[2389]---> BDD-cost:   14
c ---[2388]---> BDD-cost:   16
c ---[2387]---> BDD-cost:   14
c ---[2386]---> BDD-cost:   16
c ---[2385]---> BDD-cost:   15
c ---[2384]---> BDD-cost:   16
c ---[2383]---> BDD-cost:   16
c ---[2382]---> BDD-cost:   16
c ---[2381]---> BDD-cost:   13
c ---[2379]---> BDD-cost:   15
c ---[2378]---> BDD-cost:   15
c ---[2377]---> BDD-cost:   16
c ---[2376]---> BDD-cost:   16
c ---[2375]---> BDD-cost:   14
c ---[2374]---> BDD-cost:   15
c ---[2373]---> BDD-cost:   15
c ---[2372]---> BDD-cost:   15
c ---[2371]---> BDD-cost:   15
c ---[2370]---> BDD-cost:   13
c ---[2369]---> BDD-cost:   16
c ---[2367]---> BDD-cost:   15
c ---[2366]---> BDD-cost:   16
c ---[2365]---> BDD-cost:   16
c ---[2364]---> BDD-cost:   13
c ---[2363]---> BDD-cost:   16
c ---[2362]---> BDD-cost:   14
c ---[2361]---> BDD-cost:   16
c ---[2360]---> BDD-cost:   15
c ---[2359]---> BDD-cost:   15
c ---[2358]---> BDD-cost:   15
c ---[2357]---> BDD-cost:   16
c ---[2356]---> BDD-cost:   16
c ---[2354]---> BDD-cost:   14
c ---[2353]---> BDD-cost:   16
c ---[2352]---> BDD-cost:   16
c ---[2350]---> BDD-cost:   16
c ---[2348]---> BDD-cost:   13
c ---[2347]---> BDD-cost:   14
c ---[2346]---> BDD-cost:   16
c ---[2345]---> BDD-cost:   16
c ---[2344]---> BDD-cost:   16
c ---[2342]---> BDD-cost:   16
c ---[2341]---> BDD-cost:   16
c ---[2340]---> BDD-cost:   16
c ---[2338]---> BDD-cost:   16
c ---[2337]---> BDD-cost:   15
c ---[2336]---> BDD-cost:   16
c ---[2334]---> BDD-cost:   16
c ---[2333]---> BDD-cost:   16
c ---[2332]---> BDD-cost:   13
c ---[2331]---> BDD-cost:   15
c ---[2330]---> BDD-cost:   16
c ---[2329]---> BDD-cost:   16
c ---[2328]---> BDD-cost:   16
c ---[2327]---> BDD-cost:   16
c ---[2324]---> BDD-cost:   14
c ---[2321]---> BDD-cost:   16
c ---[2320]---> BDD-cost:   15
c ---[2319]---> BDD-cost:   16
c ---[2318]---> BDD-cost:   16
c ---[2317]---> BDD-cost:   16
c ---[2315]---> BDD-cost:   16
c ---[2314]---> BDD-cost:   14
c ---[2313]---> BDD-cost:   15
c ---[2312]---> BDD-cost:   16
c ---[2311]---> BDD-cost:   15
c ---[2310]---> BDD-cost:   15
c ---[2309]---> BDD-cost:   14
c ---[2307]---> BDD-cost:   16
c ---[2306]---> BDD-cost:   13
c ---[2305]---> BDD-cost:   13
c ---[2304]---> BDD-cost:   16
c ---[2303]---> BDD-cost:   16
c ---[2302]---> BDD-cost:   16
c ---[2301]---> BDD-cost:   16
c ---[2300]---> BDD-cost:   15
c ---[2299]---> BDD-cost:   15
c ---[2298]---> BDD-cost:   14
c ---[2297]---> BDD-cost:   13
c ---[2296]---> BDD-cost:   16
c ---[2294]---> BDD-cost:   15
c ---[2293]---> BDD-cost:   16
c ---[2292]---> BDD-cost:   15
c ---[2291]---> BDD-cost:   14
c ---[2290]---> BDD-cost:   15
c ---[2289]---> BDD-cost:   16
c ---[2288]---> BDD-cost:   14
c ---[2287]---> BDD-cost:   14
c ---[2286]---> BDD-cost:   15
c ---[2285]---> BDD-cost:   15
c ---[2284]---> BDD-cost:   16
c ---[2283]---> BDD-cost:   16
c ---[2282]---> BDD-cost:   14
c ---[2281]---> BDD-cost:   14
c ---[2280]---> BDD-cost:   15
c ---[2279]---> BDD-cost:   16
c ---[2277]---> BDD-cost:   15
c ---[2276]---> BDD-cost:   16
c ---[2275]---> BDD-cost:   16
c ---[2274]---> BDD-cost:   15
c ---[2273]---> BDD-cost:   16
c ---[2272]---> BDD-cost:   15
c ---[2271]---> BDD-cost:   15
c ---[2268]---> BDD-cost:   16
c ---[2267]---> BDD-cost:   14
c ---[2265]---> BDD-cost:   16
c ---[2264]---> BDD-cost:   15
c ---[2263]---> BDD-cost:   15
c ---[2262]---> BDD-cost:   13
c ---[2260]---> BDD-cost:   15
c ---[2259]---> BDD-cost:   15
c ---[2258]---> BDD-cost:   16
c ---[2257]---> BDD-cost:   15
c ---[2256]---> BDD-cost:   15
c ---[2255]---> BDD-cost:   16
c ---[2254]---> BDD-cost:   14
c ---[2253]---> BDD-cost:   16
c ---[2252]---> BDD-cost:   16
c ---[2251]---> BDD-cost:   15
c ---[2250]---> BDD-cost:   16
c ---[2249]---> BDD-cost:   16
c ---[2248]---> BDD-cost:   14
c ---[2247]---> BDD-cost:   15
c ---[2246]---> BDD-cost:   14
c ---[2245]---> BDD-cost:   15
c ---[2244]---> BDD-cost:   16
c ---[2243]---> BDD-cost:   16
c ---[2242]---> BDD-cost:   15
c ---[2241]---> BDD-cost:   16
c ---[2240]---> BDD-cost:   15
c ---[2239]---> BDD-cost:   16
c ---[2238]---> BDD-cost:   16
c ---[2237]---> BDD-cost:   15
c ---[2236]---> BDD-cost:   16
c ---[2235]---> BDD-cost:   14
c ---[2234]---> BDD-cost:   16
c ---[2233]---> BDD-cost:   16
c ---[2232]---> BDD-cost:   16
c ---[2231]---> BDD-cost:   15
c ---[2230]---> BDD-cost:   16
c ---[2229]---> BDD-cost:   14
c ---[2228]---> BDD-cost:   16
c ---[2226]---> BDD-cost:   15
c ---[2225]---> BDD-cost:   15
c ---[2224]---> BDD-cost:   15
c ---[2223]---> BDD-cost:   16
c ---[2222]---> BDD-cost:   16
c ---[2221]---> BDD-cost:   16
c ---[2220]---> BDD-cost:   15
c ---[2219]---> BDD-cost:   15
c ---[2218]---> BDD-cost:   13
c ---[2217]---> BDD-cost:   16
c ---[2216]---> BDD-cost:   16
c ---[2215]---> BDD-cost:   15
c ---[2214]---> BDD-cost:   15
c ---[2213]---> BDD-cost:   14
c ---[2212]---> BDD-cost:   13
c ---[2211]---> BDD-cost:   16
c ---[2210]---> BDD-cost:   16
c ---[2208]---> BDD-cost:   13
c ---[2207]---> BDD-cost:   15
c ---[2206]---> BDD-cost:   15
c ---[2205]---> BDD-cost:   16
c ---[2204]---> BDD-cost:   15
c ---[2203]---> BDD-cost:   16
c ---[2202]---> BDD-cost:   16
c ---[2200]---> BDD-cost:   16
c ---[2199]---> BDD-cost:   16
c ---[2198]---> BDD-cost:   14
c ---[2195]---> BDD-cost:   16
c ---[2194]---> BDD-cost:   13
c ---[2193]---> BDD-cost:   15
c ---[2192]---> BDD-cost:   14
c ---[2191]---> BDD-cost:   15
c ---[2190]---> BDD-cost:   16
c ---[2189]---> BDD-cost:   15
c ---[2188]---> BDD-cost:   16
c ---[2187]---> BDD-cost:   16
c ---[2186]---> BDD-cost:   16
c ---[2184]---> BDD-cost:   13
c ---[2182]---> BDD-cost:   16
c ---[2181]---> BDD-cost:   16
c ---[2180]---> BDD-cost:   14
c ---[2179]---> BDD-cost:   15
c ---[2178]---> BDD-cost:   16
c ---[2177]---> BDD-cost:   16
c ---[2175]---> BDD-cost:   16
c ---[2173]---> BDD-cost:   13
c ---[2172]---> BDD-cost:   15
c ---[2171]---> BDD-cost:   16
c ---[2170]---> BDD-cost:   14
c ---[2168]---> BDD-cost:   16
c ---[2167]---> BDD-cost:   15
c ---[2166]---> BDD-cost:   16
c ---[2165]---> BDD-cost:   16
c ---[2164]---> BDD-cost:   16
c ---[2163]---> BDD-cost:   16
c ---[2162]---> BDD-cost:   15
c ---[2161]---> BDD-cost:   15
c ---[2159]---> BDD-cost:   14
c ---[2158]---> BDD-cost:   15
c ---[2157]---> BDD-cost:   15
c ---[2155]---> BDD-cost:   15
c ---[2154]---> BDD-cost:   16
c ---[2153]---> BDD-cost:   16
c ---[2152]---> BDD-cost:   15
c ---[2151]---> BDD-cost:   16
c ---[2150]---> BDD-cost:   16
c ---[2149]---> BDD-cost:   16
c ---[2148]---> BDD-cost:   14
c ---[2147]---> BDD-cost:   14
c ---[2146]---> BDD-cost:   16
c ---[2145]---> BDD-cost:   16
c ---[2144]---> BDD-cost:   16
c ---[2143]---> BDD-cost:   16
c ---[2142]---> BDD-cost:   16
c ---[2141]---> BDD-cost:   13
c ---[2140]---> BDD-cost:   15
c ---[2139]---> BDD-cost:   13
c ---[2137]---> BDD-cost:   15
c ---[2136]---> BDD-cost:   16
c ---[2135]---> BDD-cost:   16
c ---[2134]---> BDD-cost:   16
c ---[2133]---> BDD-cost:   15
c ---[2132]---> BDD-cost:   15
c ---[2131]---> BDD-cost:   15
c ---[2130]---> BDD-cost:   15
c ---[2129]---> BDD-cost:   15
c ---[2128]---> BDD-cost:   16
c ---[2127]---> BDD-cost:   16
c ---[2126]---> BDD-cost:   15
c ---[2124]---> BDD-cost:   16
c ---[2123]---> BDD-cost:   15
c ---[2122]---> BDD-cost:   14
c ---[2121]---> BDD-cost:   13
c ---[2120]---> BDD-cost:   16
c ---[2119]---> BDD-cost:   15
c ---[2118]---> BDD-cost:   15
c ---[2117]---> BDD-cost:   14
c ---[2116]---> BDD-cost:   16
c ---[2115]---> BDD-cost:   16
c ---[2114]---> BDD-cost:   16
c ---[2113]---> BDD-cost:   15
c ---[2112]---> BDD-cost:   16
c ---[2111]---> BDD-cost:   16
c ---[2110]---> BDD-cost:   16
c ---[2109]---> BDD-cost:   16
c ---[2107]---> BDD-cost:   16
c ---[2106]---> BDD-cost:   13
c ---[2105]---> BDD-cost:   15
c ---[2104]---> BDD-cost:   16
c ---[2102]---> BDD-cost:   16
c ---[2101]---> BDD-cost:   15
c ---[2100]---> BDD-cost:   16
c ---[2099]---> BDD-cost:   16
c ---[2098]---> BDD-cost:   16
c ---[2097]---> BDD-cost:   16
c ---[2096]---> BDD-cost:   14
c ---[2095]---> BDD-cost:   16
c ---[2093]---> BDD-cost:   14
c ---[2092]---> BDD-cost:   14
c ---[2091]---> BDD-cost:   16
c ---[2090]---> BDD-cost:   16
c ---[2089]---> BDD-cost:   15
c ---[2088]---> BDD-cost:   15
c ---[2087]---> BDD-cost:   15
c ---[2086]---> BDD-cost:   16
c ---[2084]---> BDD-cost:   16
c ---[2083]---> BDD-cost:   16
c ---[2082]---> BDD-cost:   15
c ---[2081]---> BDD-cost:   15
c ---[2080]---> BDD-cost:   16
c ---[2079]---> BDD-cost:   16
c ---[2078]---> BDD-cost:   16
c ---[2077]---> BDD-cost:   15
c ---[2076]---> BDD-cost:   15
c ---[2075]---> BDD-cost:   14
c ---[2074]---> BDD-cost:   15
c ---[2073]---> BDD-cost:   15
c ---[2072]---> BDD-cost:   16
c ---[2071]---> BDD-cost:   16
c ---[2070]---> BDD-cost:   16
c ---[2069]---> BDD-cost:   16
c ---[2068]---> BDD-cost:   15
c ---[2067]---> BDD-cost:   14
c ---[2066]---> BDD-cost:   16
c ---[2065]---> BDD-cost:   16
c ---[2064]---> BDD-cost:   14
c ---[2063]---> BDD-cost:   15
c ---[2062]---> BDD-cost:   13
c ---[2061]---> BDD-cost:   16
c ---[2060]---> BDD-cost:   15
c ---[2059]---> BDD-cost:   14
c ---[2058]---> BDD-cost:   16
c ---[2057]---> BDD-cost:   15
c ---[2056]---> BDD-cost:   15
c ---[2055]---> BDD-cost:   14
c ---[2054]---> BDD-cost:   15
c ---[2052]---> BDD-cost:   16
c ---[2051]---> BDD-cost:   15
c ---[2050]---> BDD-cost:   16
c ---[2048]---> BDD-cost:   16
c ---[2047]---> BDD-cost:   15
c ---[2046]---> BDD-cost:   16
c ---[2045]---> BDD-cost:   16
c ---[2044]---> BDD-cost:   15
c ---[2042]---> BDD-cost:   15
c ---[2041]---> BDD-cost:   16
c ---[2040]---> BDD-cost:   16
c ---[2039]---> BDD-cost:   14
c ---[2038]---> BDD-cost:   15
c ---[2037]---> BDD-cost:   16
c ---[2036]---> BDD-cost:   16
c ---[2034]---> BDD-cost:   16
c ---[2033]---> BDD-cost:   15
c ---[2031]---> BDD-cost:   16
c ---[2030]---> BDD-cost:   13
c ---[2029]---> BDD-cost:   14
c ---[2028]---> BDD-cost:   15
c ---[2027]---> BDD-cost:   16
c ---[2026]---> BDD-cost:   16
c ---[2025]---> BDD-cost:   16
c ---[2024]---> BDD-cost:   16
c ---[2023]---> BDD-cost:   16
c ---[2022]---> BDD-cost:   15
c ---[2021]---> BDD-cost:   16
c ---[2020]---> BDD-cost:   15
c ---[2019]---> BDD-cost:   15
c ---[2018]---> BDD-cost:   14
c ---[2017]---> BDD-cost:   16
c ---[2015]---> BDD-cost:   16
c ---[2014]---> BDD-cost:   15
c ---[2013]---> BDD-cost:   15
c ---[2012]---> BDD-cost:   15
c ---[2011]---> BDD-cost:   16
c ---[2010]---> BDD-cost:   16
c ---[2009]---> BDD-cost:   16
c ---[2008]---> BDD-cost:   14
c ---[2007]---> BDD-cost:   16
c ---[2006]---> BDD-cost:   16
c ---[2005]---> BDD-cost:   16
c ---[2004]---> BDD-cost:   15
c ---[2003]---> BDD-cost:   16
c ---[2002]---> BDD-cost:   16
c ---[2001]---> BDD-cost:   16
c ---[2000]---> BDD-cost:   15
c ---[1999]---> BDD-cost:   15
c ---[1998]---> BDD-cost:   14
c ---[1997]---> BDD-cost:   16
c ---[1995]---> BDD-cost:   15
c ---[1994]---> BDD-cost:   14
c ---[1993]---> BDD-cost:   16
c ---[1992]---> BDD-cost:   15
c ---[1991]---> BDD-cost:   16
c ---[1990]---> BDD-cost:   15
c ---[1989]---> BDD-cost:   13
c ---[1988]---> BDD-cost:   15
c ---[1987]---> BDD-cost:   16
c ---[1986]---> BDD-cost:   14
c ---[1985]---> BDD-cost:   15
c ---[1984]---> BDD-cost:   15
c ---[1983]---> BDD-cost:   15
c ---[1982]---> BDD-cost:   15
c ---[1981]---> BDD-cost:   15
c ---[1980]---> BDD-cost:   14
c ---[1979]---> BDD-cost:   15
c ---[1978]---> BDD-cost:   16
c ---[1977]---> BDD-cost:   15
c ---[1975]---> BDD-cost:   15
c ---[1974]---> BDD-cost:   15
c ---[1973]---> BDD-cost:   14
c ---[1972]---> BDD-cost:   13
c ---[1971]---> BDD-cost:   16
c ---[1970]---> BDD-cost:   15
c ---[1969]---> BDD-cost:   15
c ---[1968]---> BDD-cost:   16
c ---[1967]---> BDD-cost:   15
c ---[1966]---> BDD-cost:   16
c ---[1965]---> BDD-cost:   14
c ---[1964]---> BDD-cost:   15
c ---[1963]---> BDD-cost:   15
c ---[1962]---> BDD-cost:   16
c ---[1960]---> BDD-cost:   16
c ---[1959]---> BDD-cost:   15
c ---[1958]---> BDD-cost:   14
c ---[1957]---> BDD-cost:   14
c ---[1956]---> BDD-cost:   16
c ---[1955]---> BDD-cost:   16
c ---[1954]---> BDD-cost:   16
c ---[1952]---> BDD-cost:   16
c ---[1951]---> BDD-cost:   16
c ---[1949]---> BDD-cost:   16
c ---[1948]---> BDD-cost:   15
c ---[1947]---> BDD-cost:   15
c ---[1946]---> BDD-cost:   16
c ---[1945]---> BDD-cost:   15
c ---[1944]---> BDD-cost:   16
c ---[1943]---> BDD-cost:   15
c ---[1942]---> BDD-cost:   15
c ---[1941]---> BDD-cost:   16
c ---[1940]---> BDD-cost:   15
c ---[1939]---> BDD-cost:   14
c ---[1935]---> BDD-cost:   16
c ---[1934]---> BDD-cost:   15
c ---[1931]---> BDD-cost:   16
c ---[1930]---> BDD-cost:   15
c ---[1929]---> BDD-cost:   15
c ---[1926]---> BDD-cost:   16
c ---[1924]---> BDD-cost:   16
c ---[1923]---> BDD-cost:   15
c ---[1922]---> BDD-cost:   16
c ---[1921]---> BDD-cost:   15
c ---[1920]---> BDD-cost:   16
c ---[1919]---> BDD-cost:   15
c ---[1918]---> BDD-cost:   15
c ---[1917]---> BDD-cost:   16
c ---[1916]---> BDD-cost:   16
c ---[1915]---> BDD-cost:   16
c ---[1914]---> BDD-cost:   16
c ---[1913]---> BDD-cost:   15
c ---[1912]---> BDD-cost:   15
c ---[1911]---> BDD-cost:   16
c ---[1910]---> BDD-cost:   16
c ---[1909]---> BDD-cost:   15
c ---[1908]---> BDD-cost:   16
c ---[1907]---> BDD-cost:   15
c ---[1906]---> BDD-cost:   16
c ---[1905]---> BDD-cost:   16
c ---[1904]---> BDD-cost:   15
c ---[1903]---> BDD-cost:   16
c ---[1902]---> BDD-cost:   16
c ---[1901]---> BDD-cost:   14
c ---[1900]---> BDD-cost:   14
c ---[1899]---> BDD-cost:   16
c ---[1898]---> BDD-cost:   16
c ---[1897]---> BDD-cost:   15
c ---[1896]---> BDD-cost:   15
c ---[1895]---> BDD-cost:   15
c ---[1893]---> BDD-cost:   13
c ---[1892]---> BDD-cost:   16
c ---[1891]---> BDD-cost:   13
c ---[1890]---> BDD-cost:   16
c ---[1889]---> BDD-cost:   16
c ---[1888]---> BDD-cost:   16
c ---[1887]---> BDD-cost:   14
c ---[1886]---> BDD-cost:   16
c ---[1885]---> BDD-cost:   16
c ---[1883]---> BDD-cost:   15
c ---[1882]---> BDD-cost:   14
c ---[1881]---> BDD-cost:   16
c ---[1879]---> BDD-cost:   15
c ---[1878]---> BDD-cost:   16
c ---[1877]---> BDD-cost:   16
c ---[1875]---> BDD-cost:   16
c ---[1874]---> BDD-cost:   16
c ---[1872]---> BDD-cost:   13
c ---[1871]---> BDD-cost:   16
c ---[1869]---> BDD-cost:   16
c ---[1868]---> BDD-cost:   16
c ---[1867]---> BDD-cost:   16
c ---[1865]---> BDD-cost:   16
c ---[1862]---> BDD-cost:   14
c ---[1861]---> BDD-cost:   15
c ---[1860]---> BDD-cost:   16
c ---[1859]---> BDD-cost:   15
c ---[1858]---> BDD-cost:   16
c ---[1857]---> BDD-cost:   15
c ---[1856]---> BDD-cost:   14
c ---[1855]---> BDD-cost:   16
c ---[1854]---> BDD-cost:   15
c ---[1853]---> BDD-cost:   15
c ---[1851]---> BDD-cost:   15
c ---[1850]---> BDD-cost:   16
c ---[1849]---> BDD-cost:   14
c ---[1848]---> BDD-cost:   14
c ---[1847]---> BDD-cost:   16
c ---[1846]---> BDD-cost:   15
c ---[1845]---> BDD-cost:   15
c ---[1844]---> BDD-cost:   15
c ---[1843]---> BDD-cost:   16
c ---[1842]---> BDD-cost:   14
c ---[1841]---> BDD-cost:   16
c ---[1840]---> BDD-cost:   14
c ---[1839]---> BDD-cost:   15
c ---[1838]---> BDD-cost:   15
c ---[1837]---> BDD-cost:   16
c ---[1836]---> BDD-cost:   16
c ---[1833]---> BDD-cost:   16
c ---[1832]---> BDD-cost:   14
c ---[1831]---> BDD-cost:   15
c ---[1830]---> BDD-cost:   16
c ---[1829]---> BDD-cost:   14
c ---[1828]---> BDD-cost:   14
c ---[1825]---> BDD-cost:   16
c ---[1824]---> BDD-cost:   16
c ---[1823]---> BDD-cost:   16
c ---[1822]---> BDD-cost:   14
c ---[1821]---> BDD-cost:   16
c ---[1820]---> BDD-cost:   16
c ---[1819]---> BDD-cost:   15
c ---[1818]---> BDD-cost:   16
c ---[1817]---> BDD-cost:   14
c ---[1816]---> BDD-cost:   16
c ---[1814]---> BDD-cost:   15
c ---[1813]---> BDD-cost:   16
c ---[1811]---> BDD-cost:   16
c ---[1810]---> BDD-cost:   15
c ---[1809]---> BDD-cost:   14
c ---[1807]---> BDD-cost:   16
c ---[1806]---> BDD-cost:   15
c ---[1805]---> BDD-cost:   13
c ---[1804]---> BDD-cost:   14
c ---[1803]---> BDD-cost:   16
c ---[1802]---> BDD-cost:   16
c ---[1800]---> BDD-cost:   14
c ---[1799]---> BDD-cost:   16
c ---[1798]---> BDD-cost:   15
c ---[1797]---> BDD-cost:   16
c ---[1796]---> BDD-cost:   15
c ---[1795]---> BDD-cost:   15
c ---[1794]---> BDD-cost:   16
c ---[1793]---> BDD-cost:   16
c ---[1792]---> BDD-cost:   16
c ---[1791]---> BDD-cost:   16
c ---[1788]---> BDD-cost:   16
c ---[1786]---> BDD-cost:   15
c ---[1785]---> BDD-cost:   16
c ---[1783]---> BDD-cost:   14
c ---[1782]---> BDD-cost:   15
c ---[1781]---> BDD-cost:   15
c ---[1780]---> BDD-cost:   16
c ---[1779]---> BDD-cost:   16
c ---[1778]---> BDD-cost:   14
c ---[1777]---> BDD-cost:   16
c ---[1776]---> BDD-cost:   13
c ---[1775]---> BDD-cost:   16
c ---[1774]---> BDD-cost:   16
c ---[1773]---> BDD-cost:   16
c ---[1772]---> BDD-cost:   14
c ---[1771]---> BDD-cost:   16
c ---[1769]---> BDD-cost:   15
c ---[1766]---> BDD-cost:   16
c ---[1765]---> BDD-cost:   15
c ---[1764]---> BDD-cost:   16
c ---[1763]---> BDD-cost:   16
c ---[1762]---> BDD-cost:   14
c ---[1761]---> BDD-cost:   15
c ---[1760]---> BDD-cost:   16
c ---[1759]---> BDD-cost:   14
c ---[1758]---> BDD-cost:   15
c ---[1757]---> BDD-cost:   16
c ---[1755]---> BDD-cost:   16
c ---[1753]---> BDD-cost:   15
c ---[1752]---> BDD-cost:   16
c ---[1751]---> BDD-cost:   16
c ---[1750]---> BDD-cost:   15
c ---[1749]---> BDD-cost:   16
c ---[1748]---> BDD-cost:   16
c ---[1747]---> BDD-cost:   14
c ---[1746]---> BDD-cost:   16
c ---[1745]---> BDD-cost:   16
c ---[1744]---> BDD-cost:   16
c ---[1743]---> BDD-cost:   15
c ---[1741]---> BDD-cost:   15
c ---[1740]---> BDD-cost:   15
c ---[1739]---> BDD-cost:   16
c ---[1738]---> BDD-cost:   15
c ---[1737]---> BDD-cost:   15
c ---[1736]---> BDD-cost:   16
c ---[1735]---> BDD-cost:   16
c ---[1734]---> BDD-cost:   15
c ---[1732]---> BDD-cost:   15
c ---[1731]---> BDD-cost:   16
c ---[1730]---> BDD-cost:   16
c ---[1729]---> BDD-cost:   16
c ---[1728]---> BDD-cost:   16
c ---[1727]---> BDD-cost:   14
c ---[1725]---> BDD-cost:   16
c ---[1724]---> BDD-cost:   14
c ---[1723]---> BDD-cost:   15
c ---[1722]---> BDD-cost:   15
c ---[1721]---> BDD-cost:   14
c ---[1719]---> BDD-cost:   15
c ---[1717]---> BDD-cost:   16
c ---[1716]---> BDD-cost:   15
c ---[1715]---> BDD-cost:   16
c ---[1714]---> BDD-cost:   14
c ---[1713]---> BDD-cost:   15
c ---[1712]---> BDD-cost:   16
c ---[1711]---> BDD-cost:   15
c ---[1710]---> BDD-cost:   15
c ---[1709]---> BDD-cost:   16
c ---[1708]---> BDD-cost:   16
c ---[1707]---> BDD-cost:   15
c ---[1706]---> BDD-cost:   15
c ---[1705]---> BDD-cost:   16
c ---[1704]---> BDD-cost:   15
c ---[1702]---> BDD-cost:   71
c ---[1700]---> BDD-cost:   69
c ---[1699]---> BDD-cost:    7
c ---[1698]---> BDD-cost:    5
c ---[1697]---> BDD-cost:    8
c ---[1696]---> BDD-cost:    5
c ---[1695]---> BDD-cost:    6
c ---[1694]---> BDD-cost:    7
c ---[1693]---> BDD-cost:   17
c ---[1692]---> BDD-cost:    8
c ---[1691]---> BDD-cost:    7
c ---[1690]---> BDD-cost:    4
c ---[1689]---> BDD-cost:    7
c ---[1688]---> BDD-cost:    8
c ---[1687]---> BDD-cost:    6
c ---[1686]---> BDD-cost:    3
c ---[1685]---> BDD-cost:    7
c ---[1684]---> BDD-cost:    5
c ---[1683]---> BDD-cost:    7
c ---[1682]---> BDD-cost:   22
c ---[1681]---> BDD-cost:    6
c ---[1680]---> BDD-cost:    6
c ---[1679]---> BDD-cost:   19
c ---[1678]---> BDD-cost:    6
c ---[1677]---> BDD-cost:    8
c ---[1676]---> BDD-cost:    8
c ---[1675]---> BDD-cost:    6
c ---[1674]---> BDD-cost:    6
c ---[1673]---> BDD-cost:    5
c ---[1672]---> BDD-cost:    8
c ---[1671]---> BDD-cost:    7
c ---[1670]---> BDD-cost:   19
c ---[1669]---> BDD-cost:   20
c ---[1668]---> BDD-cost:   20
c ---[1667]---> BDD-cost:    7
c ---[1666]---> BDD-cost:    5
c ---[1665]---> BDD-cost:    5
c ---[1664]---> BDD-cost:    7
c ---[1663]---> BDD-cost:    5
c ---[1662]---> BDD-cost:    6
c ---[1661]---> BDD-cost:   17
c ---[1660]---> BDD-cost:    5
c ---[1659]---> BDD-cost:    8
c ---[1658]---> BDD-cost:    8
c ---[1657]---> BDD-cost:    4
c ---[1656]---> BDD-cost:    3
c ---[1655]---> BDD-cost:    8
c ---[1654]---> BDD-cost:    5
c ---[1653]---> BDD-cost:    6
c ---[1652]---> BDD-cost:    7
c ---[1651]---> BDD-cost:    6
c ---[1650]---> BDD-cost:    8
c ---[1649]---> BDD-cost:    4
c ---[1648]---> BDD-cost:   19
c ---[1647]---> BDD-cost:    3
c ---[1646]---> BDD-cost:   17
c ---[1645]---> BDD-cost:    7
c ---[1644]---> BDD-cost:   22
c ---[1643]---> BDD-cost:    8
c ---[1642]---> BDD-cost:    3
c ---[1641]---> BDD-cost:    5
c ---[1640]---> BDD-cost:    8
c ---[1639]---> BDD-cost:    7
c ---[1638]---> BDD-cost:    7
c ---[1637]---> BDD-cost:    5
c ---[1636]---> BDD-cost:    8
c ---[1635]---> BDD-cost:   22
c ---[1634]---> BDD-cost:    7
c ---[1633]---> BDD-cost:    8
c ---[1632]---> BDD-cost:    8
c ---[1631]---> BDD-cost:    6
c ---[1630]---> BDD-cost:    7
c ---[1629]---> BDD-cost:    5
c ---[1628]---> BDD-cost:    7
c ---[1627]---> BDD-cost:    6
c ---[1626]---> BDD-cost:    7
c ---[1625]---> BDD-cost:   17
c ---[1624]---> BDD-cost:    5
c ---[1623]---> BDD-cost:   17
c ---[1622]---> BDD-cost:    7
c ---[1621]---> BDD-cost:   22
c ---[1620]---> BDD-cost:    5
c ---[1619]---> BDD-cost:    8
c ---[1618]---> BDD-cost:    3
c ---[1617]---> BDD-cost:    8
c ---[1616]---> BDD-cost:    8
c ---[1615]---> BDD-cost:    6
c ---[1614]---> BDD-cost:    7
c ---[1613]---> BDD-cost:    6
c ---[1612]---> BDD-cost:    5
c ---[1611]---> BDD-cost:    4
c ---[1610]---> BDD-cost:   18
c ---[1609]---> BDD-cost:    6
c ---[1608]---> BDD-cost:    5
c ---[1607]---> BDD-cost:    6
c ---[1606]---> BDD-cost:    7
c ---[1605]---> BDD-cost:   20
c ---[1604]---> BDD-cost:   22
c ---[1603]---> BDD-cost:    6
c ---[1602]---> BDD-cost:    8
c ---[1601]---> BDD-cost:    6
c ---[1600]---> BDD-cost:    8
c ---[1599]---> BDD-cost:    7
c ---[1598]---> BDD-cost:    6
c ---[1597]---> BDD-cost:    7
c ---[1596]---> BDD-cost:    5
c ---[1595]---> BDD-cost:    8
c ---[1594]---> BDD-cost:    8
c ---[1593]---> BDD-cost:    7
c ---[1592]---> BDD-cost:    6
c ---[1591]---> BDD-cost:   18
c ---[1590]---> BDD-cost:    7
c ---[1588]---> BDD-cost:   73
c ---[1587]---> BDD-cost:    6
c ---[1586]---> BDD-cost:    8
c ---[1585]---> BDD-cost:    8
c ---[1584]---> BDD-cost:    7
c ---[1583]---> BDD-cost:    5
c ---[1582]---> BDD-cost:    8
c ---[1581]---> BDD-cost:    8
c ---[1580]---> BDD-cost:    6
c ---[1579]---> BDD-cost:    8
c ---[1578]---> BDD-cost:    4
c ---[1577]---> BDD-cost:    6
c ---[1576]---> BDD-cost:    6
c ---[1575]---> BDD-cost:   22
c ---[1574]---> BDD-cost:   22
c ---[1573]---> BDD-cost:    7
c ---[1572]---> BDD-cost:    6
c ---[1571]---> BDD-cost:    6
c ---[1570]---> BDD-cost:    8
c ---[1569]---> BDD-cost:    5
c ---[1568]---> BDD-cost:    7
c ---[1567]---> BDD-cost:    8
c ---[1566]---> BDD-cost:    7
c ---[1565]---> BDD-cost:    4
c ---[1564]---> BDD-cost:    8
c ---[1563]---> BDD-cost:    8
c ---[1562]---> BDD-cost:    5
c ---[1561]---> BDD-cost:    7
c ---[1560]---> BDD-cost:    3
c ---[1559]---> BDD-cost:    3
c ---[1558]---> BDD-cost:    8
c ---[1557]---> BDD-cost:    5
c ---[1556]---> BDD-cost:    8
c ---[1555]---> BDD-cost:    4
c ---[1554]---> BDD-cost:    4
c ---[1553]---> BDD-cost:    5
c ---[1552]---> BDD-cost:    6
c ---[1551]---> BDD-cost:    6
c ---[1550]---> BDD-cost:    8
c ---[1549]---> BDD-cost:    6
c ---[1548]---> BDD-cost:    6
c ---[1547]---> BDD-cost:    8
c ---[1546]---> BDD-cost:    5
c ---[1545]---> BDD-cost:    3
c ---[1544]---> BDD-cost:   22
c ---[1543]---> BDD-cost:    8
c ---[1542]---> BDD-cost:    5
c ---[1541]---> BDD-cost:   22
c ---[1540]---> BDD-cost:   22
c ---[1539]---> BDD-cost:    8
c ---[1538]---> BDD-cost:    8
c ---[1537]---> BDD-cost:    3
c ---[1536]---> BDD-cost:    8
c ---[1535]---> BDD-cost:    7
c ---[1534]---> BDD-cost:    6
c ---[1533]---> BDD-cost:    4
c ---[1532]---> BDD-cost:    7
c ---[1531]---> BDD-cost:    8
c ---[1530]---> BDD-cost:   18
c ---[1529]---> BDD-cost:    8
c ---[1528]---> BDD-cost:   20
c ---[1527]---> BDD-cost:    6
c ---[1526]---> BDD-cost:    4
c ---[1525]---> BDD-cost:    7
c ---[1524]---> BDD-cost:   22
c ---[1523]---> BDD-cost:    7
c ---[1522]---> BDD-cost:    7
c ---[1521]---> BDD-cost:    5
c ---[1520]---> BDD-cost:    8
c ---[1519]---> BDD-cost:    8
c ---[1518]---> BDD-cost:    6
c ---[1517]---> BDD-cost:    6
c ---[1516]---> BDD-cost:    8
c ---[1515]---> BDD-cost:    7
c ---[1514]---> BDD-cost:   22
c ---[1513]---> BDD-cost:    4
c ---[1512]---> BDD-cost:    6
c ---[1511]---> BDD-cost:    4
c ---[1510]---> BDD-cost:   18
c ---[1509]---> BDD-cost:    4
c ---[1508]---> BDD-cost:    8
c ---[1507]---> BDD-cost:    5
c ---[1506]---> BDD-cost:   21
c ---[1505]---> BDD-cost:    7
c ---[1504]---> BDD-cost:    6
c ---[1503]---> BDD-cost:    3
c ---[1502]---> BDD-cost:   20
c ---[1501]---> BDD-cost:    7
c ---[1500]---> BDD-cost:    3
c ---[1499]---> BDD-cost:    5
c ---[1498]---> BDD-cost:    7
c ---[1497]---> BDD-cost:    7
c ---[1496]---> BDD-cost:    8
c ---[1495]---> BDD-cost:   21
c ---[1494]---> BDD-cost:    7
c ---[1493]---> BDD-cost:    4
c ---[1492]---> BDD-cost:    8
c ---[1491]---> BDD-cost:    6
c ---[1490]---> BDD-cost:    5
c ---[1489]---> BDD-cost:    7
c ---[1488]---> BDD-cost:   19
c ---[1487]---> BDD-cost:    7
c ---[1486]---> BDD-cost:    6
c ---[1485]---> BDD-cost:   22
c ---[1484]---> BDD-cost:    6
c ---[1483]---> BDD-cost:    7
c ---[1482]---> BDD-cost:    7
c ---[1481]---> BDD-cost:    6
c ---[1480]---> BDD-cost:    5
c ---[1479]---> BDD-cost:    6
c ---[1478]---> BDD-cost:    3
c ---[1476]---> BDD-cost:   69
c ---[1475]---> BDD-cost:    5
c ---[1474]---> BDD-cost:    8
c ---[1473]---> BDD-cost:    6
c ---[1472]---> BDD-cost:    3
c ---[1471]---> BDD-cost:    5
c ---[1470]---> BDD-cost:    8
c ---[1469]---> BDD-cost:    6
c ---[1468]---> BDD-cost:   22
c ---[1467]---> BDD-cost:    5
c ---[1466]---> BDD-cost:    5
c ---[1465]---> BDD-cost:    8
c ---[1464]---> BDD-cost:    3
c ---[1463]---> BDD-cost:    7
c ---[1462]---> BDD-cost:    6
c ---[1461]---> BDD-cost:    7
c ---[1460]---> BDD-cost:    8
c ---[1459]---> BDD-cost:    7
c ---[1458]---> BDD-cost:   18
c ---[1457]---> BDD-cost:    6
c ---[1456]---> BDD-cost:    7
c ---[1455]---> BDD-cost:    4
c ---[1454]---> BDD-cost:    8
c ---[1453]---> BDD-cost:    7
c ---[1452]---> BDD-cost:    3
c ---[1451]---> BDD-cost:    5
c ---[1450]---> BDD-cost:    6
c ---[1449]---> BDD-cost:    6
c ---[1448]---> BDD-cost:    7
c ---[1447]---> BDD-cost:   21
c ---[1446]---> BDD-cost:    7
c ---[1445]---> BDD-cost:    6
c ---[1444]---> BDD-cost:    7
c ---[1443]---> BDD-cost:    8
c ---[1442]---> BDD-cost:    7
c ---[1441]---> BDD-cost:    3
c ---[1440]---> BDD-cost:    4
c ---[1439]---> BDD-cost:    8
c ---[1438]---> BDD-cost:    7
c ---[1437]---> BDD-cost:    5
c ---[1436]---> BDD-cost:    7
c ---[1435]---> BDD-cost:    6
c ---[1434]---> BDD-cost:    6
c ---[1433]---> BDD-cost:    5
c ---[1432]---> BDD-cost:    6
c ---[1431]---> BDD-cost:    7
c ---[1430]---> BDD-cost:    7
c ---[1429]---> BDD-cost:    7
c ---[1428]---> BDD-cost:   22
c ---[1427]---> BDD-cost:    6
c ---[1426]---> BDD-cost:    6
c ---[1425]---> BDD-cost:    4
c ---[1424]---> BDD-cost:    8
c ---[1423]---> BDD-cost:    6
c ---[1422]---> BDD-cost:    8
c ---[1421]---> BDD-cost:    8
c ---[1420]---> BDD-cost:    8
c ---[1419]---> BDD-cost:   20
c ---[1418]---> BDD-cost:    7
c ---[1417]---> BDD-cost:    3
c ---[1416]---> BDD-cost:   20
c ---[1415]---> BDD-cost:    3
c ---[1414]---> BDD-cost:    7
c ---[1413]---> BDD-cost:   19
c ---[1412]---> BDD-cost:    5
c ---[1411]---> BDD-cost:    5
c ---[1410]---> BDD-cost:    7
c ---[1409]---> BDD-cost:    7
c ---[1408]---> BDD-cost:    8
c ---[1407]---> BDD-cost:    8
c ---[1406]---> BDD-cost:    8
c ---[1405]---> BDD-cost:    5
c ---[1404]---> BDD-cost:    3
c ---[1403]---> BDD-cost:   22
c ---[1402]---> BDD-cost:    7
c ---[1401]---> BDD-cost:    6
c ---[1400]---> BDD-cost:    3
c ---[1399]---> BDD-cost:    6
c ---[1398]---> BDD-cost:    7
c ---[1397]---> BDD-cost:    8
c ---[1396]---> BDD-cost:    7
c ---[1395]---> BDD-cost:    7
c ---[1394]---> BDD-cost:    7
c ---[1393]---> BDD-cost:    6
c ---[1392]---> BDD-cost:    8
c ---[1391]---> BDD-cost:   18
c ---[1390]---> BDD-cost:    7
c ---[1389]---> BDD-cost:    7
c ---[1388]---> BDD-cost:    6
c ---[1387]---> BDD-cost:    7
c ---[1386]---> BDD-cost:   21
c ---[1385]---> BDD-cost:    7
c ---[1384]---> BDD-cost:    5
c ---[1383]---> BDD-cost:    7
c ---[1382]---> BDD-cost:    8
c ---[1381]---> BDD-cost:    7
c ---[1380]---> BDD-cost:    7
c ---[1379]---> BDD-cost:    8
c ---[1378]---> BDD-cost:    5
c ---[1377]---> BDD-cost:    7
c ---[1376]---> BDD-cost:    6
c ---[1375]---> BDD-cost:    6
c ---[1374]---> BDD-cost:    6
c ---[1373]---> BDD-cost:   22
c ---[1372]---> BDD-cost:    6
c ---[1371]---> BDD-cost:    7
c ---[1370]---> BDD-cost:    6
c ---[1369]---> BDD-cost:    7
c ---[1368]---> BDD-cost:   19
c ---[1367]---> BDD-cost:   21
c ---[1366]---> BDD-cost:   22
c ---[1364]---> BDD-cost:   65
c ---[1363]---> BDD-cost:    8
c ---[1362]---> BDD-cost:    6
c ---[1361]---> BDD-cost:   21
c ---[1360]---> BDD-cost:    3
c ---[1359]---> BDD-cost:   20
c ---[1358]---> BDD-cost:    7
c ---[1357]---> BDD-cost:    8
c ---[1356]---> BDD-cost:    8
c ---[1355]---> BDD-cost:    7
c ---[1354]---> BDD-cost:    7
c ---[1353]---> BDD-cost:   22
c ---[1352]---> BDD-cost:    3
c ---[1351]---> BDD-cost:    4
c ---[1350]---> BDD-cost:    8
c ---[1349]---> BDD-cost:   19
c ---[1348]---> BDD-cost:    8
c ---[1347]---> BDD-cost:    7
c ---[1346]---> BDD-cost:    8
c ---[1345]---> BDD-cost:    6
c ---[1344]---> BDD-cost:    5
c ---[1343]---> BDD-cost:    6
c ---[1342]---> BDD-cost:    8
c ---[1341]---> BDD-cost:    6
c ---[1340]---> BDD-cost:    8
c ---[1339]---> BDD-cost:    6
c ---[1338]---> BDD-cost:    8
c ---[1337]---> BDD-cost:    8
c ---[1336]---> BDD-cost:    5
c ---[1335]---> BDD-cost:    6
c ---[1334]---> BDD-cost:    6
c ---[1333]---> BDD-cost:   18
c ---[1332]---> BDD-cost:    4
c ---[1331]---> BDD-cost:    7
c ---[1330]---> BDD-cost:    8
c ---[1329]---> BDD-cost:    6
c ---[1328]---> BDD-cost:    7
c ---[1327]---> BDD-cost:    6
c ---[1326]---> BDD-cost:    3
c ---[1325]---> BDD-cost:    6
c ---[1324]---> BDD-cost:    3
c ---[1323]---> BDD-cost:    5
c ---[1322]---> BDD-cost:    3
c ---[1321]---> BDD-cost:    7
c ---[1320]---> BDD-cost:    3
c ---[1319]---> BDD-cost:    6
c ---[1318]---> BDD-cost:    7
c ---[1317]---> BDD-cost:    3
c ---[1316]---> BDD-cost:    3
c ---[1315]---> BDD-cost:    6
c ---[1314]---> BDD-cost:    6
c ---[1313]---> BDD-cost:    6
c ---[1312]---> BDD-cost:    6
c ---[1311]---> BDD-cost:    8
c ---[1310]---> BDD-cost:    7
c ---[1309]---> BDD-cost:    7
c ---[1308]---> BDD-cost:    6
c ---[1307]---> BDD-cost:    7
c ---[1306]---> BDD-cost:    7
c ---[1305]---> BDD-cost:    8
c ---[1304]---> BDD-cost:    6
c ---[1303]---> BDD-cost:    3
c ---[1302]---> BDD-cost:    7
c ---[1301]---> BDD-cost:    7
c ---[1300]---> BDD-cost:    5
c ---[1299]---> BDD-cost:    6
c ---[1298]---> BDD-cost:   19
c ---[1297]---> BDD-cost:    5
c ---[1296]---> BDD-cost:    5
c ---[1295]---> BDD-cost:    5
c ---[1294]---> BDD-cost:    8
c ---[1293]---> BDD-cost:    7
c ---[1292]---> BDD-cost:   20
c ---[1291]---> BDD-cost:    6
c ---[1290]---> BDD-cost:    8
c ---[1289]---> BDD-cost:   20
c ---[1288]---> BDD-cost:   20
c ---[1287]---> BDD-cost:   22
c ---[1286]---> BDD-cost:    8
c ---[1285]---> BDD-cost:    8
c ---[1284]---> BDD-cost:    6
c ---[1283]---> BDD-cost:    5
c ---[1282]---> BDD-cost:    5
c ---[1281]---> BDD-cost:    8
c ---[1280]---> BDD-cost:    6
c ---[1279]---> BDD-cost:    8
c ---[1278]---> BDD-cost:    5
c ---[1277]---> BDD-cost:   22
c ---[1276]---> BDD-cost:   22
c ---[1275]---> BDD-cost:    5
c ---[1274]---> BDD-cost:   18
c ---[1273]---> BDD-cost:    8
c ---[1272]---> BDD-cost:    8
c ---[1271]---> BDD-cost:    7
c ---[1270]---> BDD-cost:    6
c ---[1269]---> BDD-cost:    3
c ---[1268]---> BDD-cost:    8
c ---[1267]---> BDD-cost:    7
c ---[1266]---> BDD-cost:    7
c ---[1265]---> BDD-cost:    5
c ---[1264]---> BDD-cost:    6
c ---[1263]---> BDD-cost:    4
c ---[1262]---> BDD-cost:    7
c ---[1261]---> BDD-cost:   20
c ---[1260]---> BDD-cost:    7
c ---[1259]---> BDD-cost:    7
c ---[1258]---> BDD-cost:    4
c ---[1257]---> BDD-cost:   20
c ---[1256]---> BDD-cost:    6
c ---[1255]---> BDD-cost:    7
c ---[1254]---> BDD-cost:    8
c ---[1252]---> BDD-cost:   73
c ---[1251]---> BDD-cost:   22
c ---[1250]---> BDD-cost:   22
c ---[1249]---> BDD-cost:    3
c ---[1248]---> BDD-cost:    6
c ---[1247]---> BDD-cost:    8
c ---[1246]---> BDD-cost:    3
c ---[1245]---> BDD-cost:    6
c ---[1244]---> BDD-cost:    7
c ---[1243]---> BDD-cost:   20
c ---[1242]---> BDD-cost:    7
c ---[1241]---> BDD-cost:    5
c ---[1240]---> BDD-cost:    8
c ---[1239]---> BDD-cost:    3
c ---[1238]---> BDD-cost:    8
c ---[1237]---> BDD-cost:    8
c ---[1236]---> BDD-cost:    7
c ---[1235]---> BDD-cost:    6
c ---[1234]---> BDD-cost:    6
c ---[1233]---> BDD-cost:   22
c ---[1232]---> BDD-cost:    7
c ---[1231]---> BDD-cost:    8
c ---[1230]---> BDD-cost:    7
c ---[1229]---> BDD-cost:    5
c ---[1228]---> BDD-cost:    6
c ---[1227]---> BDD-cost:    8
c ---[1226]---> BDD-cost:   22
c ---[1225]---> BDD-cost:   18
c ---[1224]---> BDD-cost:    8
c ---[1223]---> BDD-cost:    6
c ---[1222]---> BDD-cost:    6
c ---[1221]---> BDD-cost:    8
c ---[1220]---> BDD-cost:    3
c ---[1219]---> BDD-cost:    6
c ---[1218]---> BDD-cost:    6
c ---[1217]---> BDD-cost:    6
c ---[1216]---> BDD-cost:    7
c ---[1215]---> BDD-cost:    8
c ---[1214]---> BDD-cost:    6
c ---[1213]---> BDD-cost:    6
c ---[1212]---> BDD-cost:    8
c ---[1211]---> BDD-cost:   18
c ---[1210]---> BDD-cost:    5
c ---[1209]---> BDD-cost:    5
c ---[1208]---> BDD-cost:    8
c ---[1207]---> BDD-cost:    7
c ---[1206]---> BDD-cost:   20
c ---[1205]---> BDD-cost:    6
c ---[1204]---> BDD-cost:    7
c ---[1203]---> BDD-cost:    8
c ---[1202]---> BDD-cost:    7
c ---[1201]---> BDD-cost:    8
c ---[1200]---> BDD-cost:    8
c ---[1199]---> BDD-cost:    6
c ---[1197]---> BDD-cost:   67
c ---[1196]---> BDD-cost:    6
c ---[1195]---> BDD-cost:    6
c ---[1194]---> BDD-cost:    5
c ---[1193]---> BDD-cost:    6
c ---[1192]---> BDD-cost:   20
c ---[1191]---> BDD-cost:   19
c ---[1190]---> BDD-cost:    8
c ---[1189]---> BDD-cost:    5
c ---[1188]---> BDD-cost:    3
c ---[1187]---> BDD-cost:    8
c ---[1185]---> BDD-cost:   65
c ---[1184]---> BDD-cost:    6
c ---[1183]---> BDD-cost:    7
c ---[1182]---> BDD-cost:    7
c ---[1181]---> BDD-cost:    5
c ---[1180]---> BDD-cost:    6
c ---[1179]---> BDD-cost:    6
c ---[1178]---> BDD-cost:    7
c ---[1177]---> BDD-cost:   18
c ---[1176]---> BDD-cost:    6
c ---[1175]---> BDD-cost:    6
c ---[1173]---> BDD-cost:   65
c ---[1172]---> BDD-cost:    4
c ---[1171]---> BDD-cost:    8
c ---[1170]---> BDD-cost:    3
c ---[1169]---> BDD-cost:    8
c ---[1168]---> BDD-cost:    7
c ---[1167]---> BDD-cost:   18
c ---[1166]---> BDD-cost:    5
c ---[1165]---> BDD-cost:    6
c ---[1164]---> BDD-cost:    7
c ---[1163]---> BDD-cost:    4
c ---[1161]---> BDD-cost:   67
c ---[1160]---> BDD-cost:   20
c ---[1159]---> BDD-cost:    7
c ---[1158]---> BDD-cost:    6
c ---[1157]---> BDD-cost:   22
c ---[1156]---> BDD-cost:    7
c ---[1155]---> BDD-cost:    3
c ---[1154]---> BDD-cost:    6
c ---[1153]---> BDD-cost:   22
c ---[1152]---> BDD-cost:    3
c ---[1151]---> BDD-cost:    7
c ---[1149]---> BDD-cost:   67
c ---[1148]---> BDD-cost:    7
c ---[1147]---> BDD-cost:    3
c ---[1146]---> BDD-cost:    3
c ---[1145]---> BDD-cost:   18
c ---[1144]---> BDD-cost:    7
c ---[1143]---> BDD-cost:   18
c ---[1142]---> BDD-cost:    5
c ---[1141]---> BDD-cost:    8
c ---[1140]---> BDD-cost:   17
c ---[1139]---> BDD-cost:    6
c ---[1137]---> BDD-cost:   71
c ---[1135]---> BDD-cost:   65
c ---[1134]---> BDD-cost:   18
c ---[1133]---> BDD-cost:    7
c ---[1132]---> BDD-cost:    8
c ---[1131]---> BDD-cost:    8
c ---[1130]---> BDD-cost:    5
c ---[1129]---> BDD-cost:    7
c ---[1128]---> BDD-cost:    7
c ---[1127]---> BDD-cost:    7
c ---[1126]---> BDD-cost:    5
c ---[1125]---> BDD-cost:    3
c ---[1123]---> BDD-cost:   69
c ---[1122]---> BDD-cost:    7
c ---[1121]---> BDD-cost:   18
c ---[1120]---> BDD-cost:    8
c ---[1119]---> BDD-cost:    5
c ---[1118]---> BDD-cost:    3
c ---[1117]---> BDD-cost:    6
c ---[1116]---> BDD-cost:    3
c ---[1115]---> BDD-cost:    4
c ---[1114]---> BDD-cost:    6
c ---[1113]---> BDD-cost:    5
c ---[1111]---> BDD-cost:   69
c ---[1110]---> BDD-cost:    7
c ---[1109]---> BDD-cost:    5
c ---[1108]---> BDD-cost:    7
c ---[1107]---> BDD-cost:    8
c ---[1106]---> BDD-cost:    5
c ---[1105]---> BDD-cost:    5
c ---[1104]---> BDD-cost:    6
c ---[1103]---> BDD-cost:    7
c ---[1102]---> BDD-cost:    6
c ---[1101]---> BDD-cost:    7
c ---[1099]---> BDD-cost:   69
c ---[1098]---> BDD-cost:    7
c ---[1097]---> BDD-cost:    4
c ---[1096]---> BDD-cost:    7
c ---[1095]---> BDD-cost:    3
c ---[1094]---> BDD-cost:   21
c ---[1093]---> BDD-cost:    8
c ---[1092]---> BDD-cost:    5
c ---[1091]---> BDD-cost:    4
c ---[1090]---> BDD-cost:    6
c ---[1089]---> BDD-cost:    4
c ---[1087]---> BDD-cost:   67
c ---[1086]---> BDD-cost:    7
c ---[1085]---> BDD-cost:    6
c ---[1084]---> BDD-cost:    6
c ---[1083]---> BDD-cost:   20
c ---[1082]---> BDD-cost:    8
c ---[1081]---> BDD-cost:   22
c ---[1080]---> BDD-cost:    5
c ---[1079]---> BDD-cost:    5
c ---[1078]---> BDD-cost:   20
c ---[1077]---> BDD-cost:    3
c ---[1075]---> BDD-cost:   63
c ---[1074]---> BDD-cost:    8
c ---[1073]---> BDD-cost:    5
c ---[1072]---> BDD-cost:    7
c ---[1071]---> BDD-cost:    6
c ---[1070]---> BDD-cost:    7
c ---[1069]---> BDD-cost:    8
c ---[1068]---> BDD-cost:   19
c ---[1067]---> BDD-cost:    7
c ---[1066]---> BDD-cost:    6
c ---[1065]---> BDD-cost:    7
c ---[1063]---> BDD-cost:   65
c ---[1062]---> BDD-cost:    7
c ---[1061]---> BDD-cost:    7
c ---[1060]---> BDD-cost:    6
c ---[1059]---> BDD-cost:    7
c ---[1058]---> BDD-cost:    7
c ---[1057]---> BDD-cost:    7
c ---[1056]---> BDD-cost:    6
c ---[1055]---> BDD-cost:    7
c ---[1054]---> BDD-cost:    7
c ---[1053]---> BDD-cost:    7
c ---[1051]---> BDD-cost:   63
c ---[1050]---> BDD-cost:    7
c ---[1049]---> BDD-cost:    7
c ---[1048]---> BDD-cost:    7
c ---[1047]---> BDD-cost:    3
c ---[1046]---> BDD-cost:    8
c ---[1045]---> BDD-cost:    4
c ---[1044]---> BDD-cost:   21
c ---[1043]---> BDD-cost:    4
c ---[1042]---> BDD-cost:    8
c ---[1041]---> BDD-cost:    7
c ---[1039]---> BDD-cost:   63
c ---[1038]---> BDD-cost:   21
c ---[1037]---> BDD-cost:    4
c ---[1036]---> BDD-cost:    7
c ---[1035]---> BDD-cost:    7
c ---[1034]---> BDD-cost:    5
c ---[1033]---> BDD-cost:    5
c ---[1032]---> BDD-cost:    6
c ---[1031]---> BDD-cost:    8
c ---[1030]---> BDD-cost:   19
c ---[1029]---> BDD-cost:   22
c ---[1027]---> BDD-cost:   71
c ---[1026]---> BDD-cost:    6
c ---[1025]---> BDD-cost:    7
c ---[1024]---> BDD-cost:    3
c ---[1023]---> BDD-cost:   22
c ---[1022]---> BDD-cost:    8
c ---[1021]---> BDD-cost:    8
c ---[1020]---> BDD-cost:    6
c ---[1019]---> BDD-cost:    3
c ---[1018]---> BDD-cost:   19
c ---[1017]---> BDD-cost:    8
c ---[1015]---> BDD-cost:   69
c ---[1013]---> BDD-cost:   67
c ---[1012]---> BDD-cost:    4
c ---[1011]---> BDD-cost:    6
c ---[1010]---> BDD-cost:    8
c ---[1009]---> BDD-cost:    8
c ---[1008]---> BDD-cost:    8
c ---[1007]---> BDD-cost:    7
c ---[1006]---> BDD-cost:    7
c ---[1005]---> BDD-cost:    7
c ---[1004]---> BDD-cost:    8
c ---[1003]---> BDD-cost:    4
c ---[1001]---> BDD-cost:   65
c ---[1000]---> BDD-cost:    8
c ---[ 999]---> BDD-cost:    7
c ---[ 998]---> BDD-cost:    7
c ---[ 997]---> BDD-cost:    8
c ---[ 996]---> BDD-cost:    7
c ---[ 995]---> BDD-cost:    7
c ---[ 994]---> BDD-cost:    7
c ---[ 993]---> BDD-cost:    3
c ---[ 992]---> BDD-cost:    7
c ---[ 991]---> BDD-cost:    6
c ---[ 989]---> BDD-cost:   71
c ---[ 988]---> BDD-cost:    3
c ---[ 987]---> BDD-cost:    6
c ---[ 986]---> BDD-cost:    8
c ---[ 985]---> BDD-cost:    6
c ---[ 984]---> BDD-cost:    7
c ---[ 983]---> BDD-cost:    7
c ---[ 982]---> BDD-cost:    6
c ---[ 981]---> BDD-cost:   20
c ---[ 980]---> BDD-cost:    7
c ---[ 979]---> BDD-cost:    6
c ---[ 977]---> BDD-cost:   73
c ---[ 976]---> BDD-cost:    3
c ---[ 975]---> BDD-cost:    5
c ---[ 974]---> BDD-cost:    5
c ---[ 973]---> BDD-cost:    6
c ---[ 972]---> BDD-cost:    5
c ---[ 971]---> BDD-cost:    8
c ---[ 970]---> BDD-cost:   20
c ---[ 969]---> BDD-cost:   20
c ---[ 968]---> BDD-cost:    8
c ---[ 967]---> BDD-cost:    5
c ---[ 965]---> BDD-cost:   71
c ---[ 964]---> BDD-cost:    6
c ---[ 963]---> BDD-cost:    6
c ---[ 962]---> BDD-cost:    5
c ---[ 961]---> BDD-cost:    8
c ---[ 960]---> BDD-cost:    6
c ---[ 959]---> BDD-cost:    6
c ---[ 958]---> BDD-cost:    3
c ---[ 957]---> BDD-cost:    6
c ---[ 956]---> BDD-cost:    6
c ---[ 955]---> BDD-cost:    7
c ---[ 953]---> BDD-cost:   69
c ---[ 952]---> BDD-cost:    7
c ---[ 951]---> BDD-cost:    5
c ---[ 950]---> BDD-cost:    7
c ---[ 949]---> BDD-cost:    8
c ---[ 948]---> BDD-cost:    6
c ---[ 947]---> BDD-cost:    5
c ---[ 946]---> BDD-cost:    8
c ---[ 945]---> BDD-cost:    8
c ---[ 944]---> BDD-cost:    3
c ---[ 943]---> BDD-cost:    6
c ---[ 941]---> BDD-cost:   67
c ---[ 940]---> BDD-cost:    6
c ---[ 939]---> BDD-cost:    8
c ---[ 938]---> BDD-cost:    7
c ---[ 937]---> BDD-cost:    8
c ---[ 936]---> BDD-cost:   22
c ---[ 935]---> BDD-cost:    7
c ---[ 934]---> BDD-cost:    5
c ---[ 933]---> BDD-cost:   18
c ---[ 932]---> BDD-cost:    7
c ---[ 931]---> BDD-cost:    8
c ---[ 929]---> BDD-cost:   63
c ---[ 928]---> BDD-cost:    8
c ---[ 927]---> BDD-cost:    8
c ---[ 926]---> BDD-cost:    5
c ---[ 925]---> BDD-cost:    3
c ---[ 924]---> BDD-cost:   20
c ---[ 923]---> BDD-cost:   22
c ---[ 922]---> BDD-cost:    3
c ---[ 921]---> BDD-cost:    8
c ---[ 920]---> BDD-cost:    7
c ---[ 919]---> BDD-cost:   22
c ---[ 917]---> BDD-cost:   63
c ---[ 916]---> BDD-cost:    3
c ---[ 915]---> BDD-cost:    7
c ---[ 914]---> BDD-cost:    6
c ---[ 913]---> BDD-cost:    6
c ---[ 912]---> BDD-cost:    8
c ---[ 911]---> BDD-cost:    3
c ---[ 910]---> BDD-cost:    7
c ---[ 909]---> BDD-cost:    7
c ---[ 908]---> BDD-cost:    8
c ---[ 907]---> BDD-cost:    7
c ---[ 905]---> BDD-cost:   57
c ---[ 904]---> BDD-cost:    4
c ---[ 903]---> BDD-cost:    4
c ---[ 902]---> BDD-cost:    7
c ---[ 901]---> BDD-cost:    6
c ---[ 900]---> BDD-cost:    6
c ---[ 899]---> BDD-cost:    5
c ---[ 898]---> BDD-cost:   20
c ---[ 897]---> BDD-cost:    7
c ---[ 896]---> BDD-cost:   17
c ---[ 895]---> BDD-cost:    7
c ---[ 893]---> BDD-cost:   57
c ---[ 891]---> Adder-cost: 2156   maxlim: 2895835   bits: 23/22
c ---[ 890]---> BDD-cost:    8
c ---[ 889]---> BDD-cost:    6
c ---[ 888]---> BDD-cost:    7
c ---[ 887]---> BDD-cost:    7
c ---[ 886]---> BDD-cost:    8
c ---[ 885]---> BDD-cost:    8
c ---[ 884]---> BDD-cost:    3
c ---[ 883]---> BDD-cost:   21
c ---[ 882]---> BDD-cost:    8
c ---[ 881]---> BDD-cost:    7
c ---[ 879]---> Adder-cost: 2318   maxlim: 3144667   bits: 23/22
c ---[ 878]---> BDD-cost:    4
c ---[ 877]---> BDD-cost:   21
c ---[ 876]---> BDD-cost:    5
c ---[ 875]---> BDD-cost:    3
c ---[ 874]---> BDD-cost:    5
c ---[ 873]---> BDD-cost:    7
c ---[ 872]---> BDD-cost:    8
c ---[ 871]---> BDD-cost:    7
c ---[ 870]---> BDD-cost:    6
c ---[ 869]---> BDD-cost:    5
c ---[ 867]---> Adder-cost: 2324   maxlim: 3258332   bits: 23/22
c ---[ 866]---> BDD-cost:    6
c ---[ 865]---> BDD-cost:    3
c ---[ 864]---> BDD-cost:    3
c ---[ 863]---> BDD-cost:    3
c ---[ 862]---> BDD-cost:   20
c ---[ 861]---> BDD-cost:    6
c ---[ 860]---> BDD-cost:    3
c ---[ 859]---> BDD-cost:    8
c ---[ 858]---> BDD-cost:   19
c ---[ 857]---> BDD-cost:   19
c ---[ 855]---> Adder-cost: 1992   maxlim: 2337762   bits: 23/22
c ---[ 854]---> BDD-cost:    7
c ---[ 853]---> BDD-cost:    8
c ---[ 852]---> BDD-cost:    8
c ---[ 851]---> BDD-cost:    5
c ---[ 850]---> BDD-cost:   18
c ---[ 849]---> BDD-cost:    5
c ---[ 848]---> BDD-cost:   22
c ---[ 847]---> BDD-cost:    7
c ---[ 846]---> BDD-cost:    8
c ---[ 845]---> BDD-cost:    6
c ---[ 843]---> Adder-cost: 2106   maxlim: 3205085   bits: 23/22
c ---[ 842]---> BDD-cost:    8
c ---[ 841]---> BDD-cost:    6
c ---[ 840]---> BDD-cost:    8
c ---[ 839]---> BDD-cost:    6
c ---[ 838]---> BDD-cost:    7
c ---[ 837]---> BDD-cost:    3
c ---[ 836]---> BDD-cost:    7
c ---[ 835]---> BDD-cost:    5
c ---[ 834]---> BDD-cost:    7
c ---[ 833]---> BDD-cost:   21
c ---[ 831]---> Adder-cost: 2300   maxlim: 3529693   bits: 23/22
c ---[ 830]---> BDD-cost:    5
c ---[ 829]---> BDD-cost:    7
c ---[ 828]---> BDD-cost:    3
c ---[ 827]---> BDD-cost:   21
c ---[ 826]---> BDD-cost:    4
c ---[ 825]---> BDD-cost:    6
c ---[ 824]---> BDD-cost:   22
c ---[ 823]---> BDD-cost:    5
c ---[ 822]---> BDD-cost:   19
c ---[ 821]---> BDD-cost:    5
c ---[ 819]---> Adder-cost: 2034   maxlim: 2619359   bits: 23/22
c ---[ 818]---> BDD-cost:    7
c ---[ 817]---> BDD-cost:    8
c ---[ 816]---> BDD-cost:    7
c ---[ 815]---> BDD-cost:    5
c ---[ 814]---> BDD-cost:    7
c ---[ 813]---> BDD-cost:    7
c ---[ 812]---> BDD-cost:    7
c ---[ 811]---> BDD-cost:    8
c ---[ 810]---> BDD-cost:    6
c ---[ 809]---> BDD-cost:    3
c ---[ 807]---> Adder-cost: 2372   maxlim: 3350491   bits: 23/22
c ---[ 806]---> BDD-cost:    5
c ---[ 805]---> BDD-cost:    7
c ---[ 804]---> BDD-cost:    3
c ---[ 803]---> BDD-cost:   18
c ---[ 802]---> BDD-cost:    5
c ---[ 801]---> BDD-cost:    4
c ---[ 800]---> BDD-cost:    7
c ---[ 799]---> BDD-cost:    7
c ---[ 798]---> BDD-cost:    7
c ---[ 797]---> BDD-cost:   20
c ---[ 795]---> Adder-cost: 2032   maxlim: 2594782   bits: 23/22
c ---[ 794]---> BDD-cost:    7
c ---[ 793]---> BDD-cost:    8
c ---[ 792]---> BDD-cost:   18
c ---[ 791]---> BDD-cost:    7
c ---[ 790]---> BDD-cost:    7
c ---[ 789]---> BDD-cost:    6
c ---[ 788]---> BDD-cost:    3
c ---[ 787]---> BDD-cost:    8
c ---[ 786]---> BDD-cost:    5
c ---[ 785]---> BDD-cost:    5
c ---[ 783]---> Adder-cost: 2312   maxlim: 2893788   bits: 23/22
c ---[ 782]---> BDD-cost:    8
c ---[ 781]---> BDD-cost:    7
c ---[ 780]---> BDD-cost:   18
c ---[ 779]---> BDD-cost:    7
c ---[ 778]---> BDD-cost:    3
c ---[ 777]---> BDD-cost:    7
c ---[ 776]---> BDD-cost:    6
c ---[ 775]---> BDD-cost:    7
c ---[ 774]---> BDD-cost:    5
c ---[ 773]---> BDD-cost:   19
c ---[ 771]---> BDD-cost:   67
c ---[ 769]---> Adder-cost: 2158   maxlim: 3303386   bits: 23/22
c ---[ 768]---> BDD-cost:    7
c ---[ 767]---> BDD-cost:    7
c ---[ 766]---> BDD-cost:    8
c ---[ 765]---> BDD-cost:    7
c ---[ 764]---> BDD-cost:    4
c ---[ 763]---> BDD-cost:    6
c ---[ 762]---> BDD-cost:    6
c ---[ 761]---> BDD-cost:    5
c ---[ 760]---> BDD-cost:    7
c ---[ 759]---> BDD-cost:    3
c ---[ 757]---> Adder-cost: 2220   maxlim: 3007452   bits: 23/22
c ---[ 756]---> BDD-cost:    6
c ---[ 755]---> BDD-cost:   21
c ---[ 754]---> BDD-cost:    6
c ---[ 753]---> BDD-cost:    7
c ---[ 752]---> BDD-cost:    6
c ---[ 751]---> BDD-cost:    5
c ---[ 750]---> BDD-cost:    7
c ---[ 749]---> BDD-cost:    5
c ---[ 748]---> BDD-cost:    8
c ---[ 747]---> BDD-cost:    4
c ---[ 745]---> Adder-cost: 2192   maxlim: 3061726   bits: 23/22
c ---[ 744]---> BDD-cost:    7
c ---[ 743]---> BDD-cost:    5
c ---[ 742]---> BDD-cost:    4
c ---[ 741]---> BDD-cost:    6
c ---[ 740]---> BDD-cost:    8
c ---[ 739]---> BDD-cost:    5
c ---[ 738]---> BDD-cost:    5
c ---[ 737]---> BDD-cost:    8
c ---[ 736]---> BDD-cost:    7
c ---[ 735]---> BDD-cost:    6
c ---[ 733]---> Adder-cost: 2162   maxlim: 2943962   bits: 23/22
c ---[ 732]---> BDD-cost:    3
c ---[ 731]---> BDD-cost:    6
c ---[ 730]---> BDD-cost:   18
c ---[ 729]---> BDD-cost:    8
c ---[ 728]---> BDD-cost:    8
c ---[ 727]---> BDD-cost:    5
c ---[ 726]---> BDD-cost:    7
c ---[ 725]---> BDD-cost:    6
c ---[ 724]---> BDD-cost:    8
c ---[ 723]---> BDD-cost:    8
c ---[ 721]---> Adder-cost: 2194   maxlim: 2976733   bits: 23/22
c ---[ 720]---> BDD-cost:    8
c ---[ 719]---> BDD-cost:   20
c ---[ 718]---> BDD-cost:   22
c ---[ 717]---> BDD-cost:    6
c ---[ 716]---> BDD-cost:   18
c ---[ 715]---> BDD-cost:   18
c ---[ 714]---> BDD-cost:    8
c ---[ 713]---> BDD-cost:    3
c ---[ 712]---> BDD-cost:    7
c ---[ 711]---> BDD-cost:    6
c ---[ 709]---> Adder-cost: 2032   maxlim: 2712542   bits: 23/22
c ---[ 708]---> BDD-cost:    8
c ---[ 707]---> BDD-cost:   22
c ---[ 706]---> BDD-cost:    8
c ---[ 705]---> BDD-cost:    5
c ---[ 704]---> BDD-cost:    3
c ---[ 703]---> BDD-cost:   19
c ---[ 702]---> BDD-cost:    5
c ---[ 701]---> BDD-cost:    7
c ---[ 700]---> BDD-cost:    6
c ---[ 699]---> BDD-cost:    5
c ---[ 697]---> Adder-cost: 2150   maxlim: 2696158   bits: 23/22
c ---[ 696]---> BDD-cost:   19
c ---[ 695]---> BDD-cost:    8
c ---[ 694]---> BDD-cost:   17
c ---[ 693]---> BDD-cost:    7
c ---[ 692]---> BDD-cost:    4
c ---[ 691]---> BDD-cost:    6
c ---[ 690]---> BDD-cost:    7
c ---[ 689]---> BDD-cost:    8
c ---[ 688]---> BDD-cost:    7
c ---[ 687]---> BDD-cost:    5
c ---[ 685]---> Adder-cost: 2294   maxlim: 2912221   bits: 23/22
c ---[ 684]---> BDD-cost:    4
c ---[ 683]---> BDD-cost:    7
c ---[ 682]---> BDD-cost:    4
c ---[ 681]---> BDD-cost:   22
c ---[ 680]---> BDD-cost:    6
c ---[ 679]---> BDD-cost:    6
c ---[ 678]---> BDD-cost:    8
c ---[ 677]---> BDD-cost:    7
c ---[ 676]---> BDD-cost:    4
c ---[ 675]---> BDD-cost:    6
c ---[ 673]---> Adder-cost: 2282   maxlim: 3110877   bits: 23/22
c ---[ 672]---> BDD-cost:    6
c ---[ 671]---> BDD-cost:   22
c ---[ 670]---> BDD-cost:   18
c ---[ 669]---> BDD-cost:    5
c ---[ 668]---> BDD-cost:    6
c ---[ 667]---> BDD-cost:   22
c ---[ 666]---> BDD-cost:    5
c ---[ 665]---> BDD-cost:    7
c ---[ 664]---> BDD-cost:    7
c ---[ 663]---> BDD-cost:    6
c ---[ 661]---> Adder-cost: 2220   maxlim: 3010526   bits: 23/22
c ---[ 660]---> BDD-cost:    6
c ---[ 659]---> BDD-cost:    8
c ---[ 658]---> BDD-cost:    7
c ---[ 657]---> BDD-cost:   22
c ---[ 656]---> BDD-cost:    5
c ---[ 655]---> BDD-cost:    8
c ---[ 654]---> BDD-cost:    7
c ---[ 653]---> BDD-cost:    4
c ---[ 652]---> BDD-cost:    8
c ---[ 651]---> BDD-cost:    7
c ---[ 649]---> BDD-cost:   67
c ---[ 647]---> Adder-cost: 2178   maxlim: 3334108   bits: 23/22
c ---[ 646]---> BDD-cost:    7
c ---[ 645]---> BDD-cost:    4
c ---[ 644]---> BDD-cost:    6
c ---[ 643]---> BDD-cost:    8
c ---[ 642]---> BDD-cost:    6
c ---[ 641]---> BDD-cost:    8
c ---[ 640]---> BDD-cost:    7
c ---[ 639]---> BDD-cost:    4
c ---[ 638]---> BDD-cost:    7
c ---[ 637]---> BDD-cost:    7
c ---[ 635]---> Adder-cost: 2182   maxlim: 3058652   bits: 23/22
c ---[ 634]---> BDD-cost:    5
c ---[ 633]---> BDD-cost:    7
c ---[ 632]---> BDD-cost:   20
c ---[ 631]---> BDD-cost:    7
c ---[ 630]---> BDD-cost:    6
c ---[ 629]---> BDD-cost:    7
c ---[ 628]---> BDD-cost:    8
c ---[ 627]---> BDD-cost:    3
c ---[ 626]---> BDD-cost:    8
c ---[ 625]---> BDD-cost:    8
c ---[ 623]---> Adder-cost: 2348   maxlim: 2894812   bits: 23/22
c ---[ 622]---> BDD-cost:    5
c ---[ 621]---> BDD-cost:    5
c ---[ 620]---> BDD-cost:    3
c ---[ 619]---> BDD-cost:    5
c ---[ 618]---> BDD-cost:    4
c ---[ 617]---> BDD-cost:    4
c ---[ 616]---> BDD-cost:    5
c ---[ 615]---> BDD-cost:    7
c ---[ 614]---> BDD-cost:    6
c ---[ 613]---> BDD-cost:    6
c ---[ 611]---> Adder-cost: 2218   maxlim: 2889693   bits: 23/22
c ---[ 610]---> BDD-cost:    7
c ---[ 609]---> BDD-cost:    7
c ---[ 608]---> BDD-cost:    7
c ---[ 607]---> BDD-cost:    5
c ---[ 606]---> BDD-cost:   20
c ---[ 605]---> BDD-cost:   18
c ---[ 604]---> BDD-cost:    7
c ---[ 603]---> BDD-cost:    5
c ---[ 602]---> BDD-cost:    7
c ---[ 601]---> BDD-cost:    6
c ---[ 599]---> Adder-cost: 2072   maxlim: 2930655   bits: 23/22
c ---[ 598]---> BDD-cost:    6
c ---[ 597]---> BDD-cost:    7
c ---[ 596]---> BDD-cost:    7
c ---[ 595]---> BDD-cost:    7
c ---[ 594]---> BDD-cost:    8
c ---[ 593]---> BDD-cost:    7
c ---[ 592]---> BDD-cost:   19
c ---[ 591]---> BDD-cost:    3
c ---[ 590]---> BDD-cost:   22
c ---[ 589]---> BDD-cost:    8
c ---[ 587]---> Adder-cost: 2184   maxlim: 2863070   bits: 23/22
c ---[ 586]---> BDD-cost:    4
c ---[ 585]---> BDD-cost:    6
c ---[ 584]---> BDD-cost:    8
c ---[ 583]---> BDD-cost:    6
c ---[ 582]---> BDD-cost:    5
c ---[ 581]---> BDD-cost:    8
c ---[ 580]---> BDD-cost:    8
c ---[ 579]---> BDD-cost:    6
c ---[ 578]---> BDD-cost:    7
c ---[ 577]---> BDD-cost:   18
c ---[ 575]---> Adder-cost: 2030   maxlim: 2764767   bits: 23/22
c ---[ 574]---> BDD-cost:    5
c ---[ 573]---> BDD-cost:    7
c ---[ 572]---> BDD-cost:    6
c ---[ 571]---> BDD-cost:    5
c ---[ 570]---> BDD-cost:    6
c ---[ 569]---> BDD-cost:    7
c ---[ 568]---> BDD-cost:   21
c ---[ 567]---> BDD-cost:    4
c ---[ 566]---> BDD-cost:    4
c ---[ 565]---> BDD-cost:    8
c ---[ 563]---> Adder-cost: 2096   maxlim: 2895839   bits: 23/22
c ---[ 562]---> BDD-cost:    7
c ---[ 561]---> BDD-cost:    6
c ---[ 560]---> BDD-cost:    8
c ---[ 559]---> BDD-cost:    5
c ---[ 558]---> BDD-cost:    5
c ---[ 557]---> BDD-cost:    6
c ---[ 556]---> BDD-cost:    7
c ---[ 555]---> BDD-cost:    8
c ---[ 554]---> BDD-cost:    8
c ---[ 553]---> BDD-cost:    7
c ---[ 551]---> Adder-cost: 2270   maxlim: 3108827   bits: 23/22
c ---[ 550]---> BDD-cost:    5
c ---[ 549]---> BDD-cost:    3
c ---[ 548]---> BDD-cost:    4
c ---[ 547]---> BDD-cost:    5
c ---[ 546]---> BDD-cost:   22
c ---[ 545]---> BDD-cost:    6
c ---[ 544]---> BDD-cost:    7
c ---[ 543]---> BDD-cost:   19
c ---[ 542]---> BDD-cost:    3
c ---[ 541]---> BDD-cost:    8
c ---[ 539]---> Adder-cost: 2254   maxlim: 3202013   bits: 23/22
c ---[ 538]---> BDD-cost:    7
c ---[ 537]---> BDD-cost:    7
c ---[ 536]---> BDD-cost:    3
c ---[ 535]---> BDD-cost:    7
c ---[ 534]---> BDD-cost:   19
c ---[ 533]---> BDD-cost:    7
c ---[ 532]---> BDD-cost:    6
c ---[ 531]---> BDD-cost:    3
c ---[ 530]---> BDD-cost:    4
c ---[ 529]---> BDD-cost:    4
c ---[ 527]---> BDD-cost:   63
c ---[ 525]---> Adder-cost: 2152   maxlim: 2366430   bits: 23/22
c ---[ 524]---> BDD-cost:    3
c ---[ 523]---> BDD-cost:    6
c ---[ 522]---> BDD-cost:    7
c ---[ 521]---> BDD-cost:    5
c ---[ 520]---> BDD-cost:    8
c ---[ 519]---> BDD-cost:    8
c ---[ 518]---> BDD-cost:    8
c ---[ 517]---> BDD-cost:    7
c ---[ 516]---> BDD-cost:    7
c ---[ 515]---> BDD-cost:    8
c ---[ 513]---> Adder-cost: 2266   maxlim: 3364827   bits: 23/22
c ---[ 512]---> BDD-cost:    6
c ---[ 511]---> BDD-cost:    6
c ---[ 510]---> BDD-cost:   21
c ---[ 509]---> BDD-cost:    8
c ---[ 508]---> BDD-cost:    5
c ---[ 507]---> BDD-cost:    4
c ---[ 506]---> BDD-cost:    8
c ---[ 505]---> BDD-cost:   21
c ---[ 504]---> BDD-cost:    7
c ---[ 503]---> BDD-cost:    7
c ---[ 501]---> Adder-cost: 2314   maxlim: 2833370   bits: 23/22
c ---[ 500]---> BDD-cost:    8
c ---[ 499]---> BDD-cost:    3
c ---[ 498]---> BDD-cost:    8
c ---[ 497]---> BDD-cost:    7
c ---[ 496]---> BDD-cost:    7
c ---[ 495]---> BDD-cost:    8
c ---[ 494]---> BDD-cost:    8
c ---[ 493]---> BDD-cost:    8
c ---[ 492]---> BDD-cost:    6
c ---[ 491]---> BDD-cost:    7
c ---[ 489]---> Adder-cost: 2288   maxlim: 3790811   bits: 23/22
c ---[ 488]---> BDD-cost:    5
c ---[ 487]---> BDD-cost:    8
c ---[ 486]---> BDD-cost:   22
c ---[ 485]---> BDD-cost:   22
c ---[ 484]---> BDD-cost:    8
c ---[ 483]---> BDD-cost:    7
c ---[ 482]---> BDD-cost:    5
c ---[ 481]---> BDD-cost:    8
c ---[ 480]---> BDD-cost:    7
c ---[ 479]---> BDD-cost:    8
c ---[ 477]---> Adder-cost: 2324   maxlim: 2880476   bits: 23/22
c ---[ 476]---> BDD-cost:    7
c ---[ 475]---> BDD-cost:    4
c ---[ 474]---> BDD-cost:    5
c ---[ 473]---> BDD-cost:    6
c ---[ 472]---> BDD-cost:    7
c ---[ 471]---> BDD-cost:    8
c ---[ 470]---> BDD-cost:    8
c ---[ 469]---> BDD-cost:    6
c ---[ 468]---> BDD-cost:    8
c ---[ 467]---> BDD-cost:    5
c ---[ 465]---> Adder-cost: 2124   maxlim: 2808797   bits: 23/22
c ---[ 464]---> BDD-cost:    6
c ---[ 463]---> BDD-cost:    8
c ---[ 462]---> BDD-cost:    7
c ---[ 461]---> BDD-cost:    5
c ---[ 460]---> BDD-cost:    3
c ---[ 459]---> BDD-cost:    4
c ---[ 458]---> BDD-cost:    7
c ---[ 457]---> BDD-cost:    7
c ---[ 456]---> BDD-cost:    6
c ---[ 455]---> BDD-cost:    5
c ---[ 453]---> Adder-cost: 2224   maxlim: 2775007   bits: 23/22
c ---[ 452]---> BDD-cost:    3
c ---[ 451]---> BDD-cost:    5
c ---[ 450]---> BDD-cost:    7
c ---[ 449]---> BDD-cost:    6
c ---[ 448]---> BDD-cost:   20
c ---[ 447]---> BDD-cost:    5
c ---[ 446]---> BDD-cost:    6
c ---[ 445]---> BDD-cost:    6
c ---[ 444]---> BDD-cost:    8
c ---[ 443]---> BDD-cost:    6
c ---[ 441]---> Adder-cost: 2096   maxlim: 2678751   bits: 23/22
c ---[ 440]---> BDD-cost:    6
c ---[ 439]---> BDD-cost:    6
c ---[ 438]---> BDD-cost:    8
c ---[ 437]---> BDD-cost:    7
c ---[ 436]---> BDD-cost:    5
c ---[ 435]---> BDD-cost:    8
c ---[ 434]---> BDD-cost:    5
c ---[ 433]---> BDD-cost:    6
c ---[ 432]---> BDD-cost:    7
c ---[ 431]---> BDD-cost:    8
c ---[ 429]---> Adder-cost: 2134   maxlim: 2991074   bits: 23/22
c ---[ 428]---> BDD-cost:    3
c ---[ 427]---> BDD-cost:   19
c ---[ 426]---> BDD-cost:    8
c ---[ 425]---> BDD-cost:    6
c ---[ 424]---> BDD-cost:   21
c ---[ 423]---> BDD-cost:    6
c ---[ 422]---> BDD-cost:    4
c ---[ 421]---> BDD-cost:    3
c ---[ 420]---> BDD-cost:    7
c ---[ 419]---> BDD-cost:    7
c ---[ 418]---> BDD-cost:    8
c ---[ 417]---> BDD-cost:    7
c ---[ 416]---> BDD-cost:    3
c ---[ 415]---> BDD-cost:    7
c ---[ 414]---> BDD-cost:    7
c ---[ 413]---> BDD-cost:    4
c ---[ 412]---> BDD-cost:    8
c ---[ 411]---> BDD-cost:   20
c ---[ 410]---> BDD-cost:    5
c ---[ 409]---> BDD-cost:    8
c ---[ 408]---> BDD-cost:    3
c ---[ 406]---> BDD-cost:   71
c ---[ 405]---> BDD-cost:    6
c ---[ 404]---> BDD-cost:    7
c ---[ 403]---> BDD-cost:    8
c ---[ 402]---> BDD-cost:    5
c ---[ 401]---> BDD-cost:   21
c ---[ 400]---> BDD-cost:    5
c ---[ 399]---> BDD-cost:    5
c ---[ 398]---> BDD-cost:    8
c ---[ 397]---> BDD-cost:    7
c ---[ 396]---> BDD-cost:    5
c ---[ 395]---> BDD-cost:    8
c ---[ 394]---> BDD-cost:    8
c ---[ 393]---> BDD-cost:    6
c ---[ 392]---> BDD-cost:    6
c ---[ 391]---> BDD-cost:    8
c ---[ 390]---> BDD-cost:    8
c ---[ 389]---> BDD-cost:    7
c ---[ 388]---> BDD-cost:    7
c ---[ 387]---> BDD-cost:    3
c ---[ 386]---> BDD-cost:    6
c ---[ 385]---> BDD-cost:    7
c ---[ 384]---> BDD-cost:   22
c ---[ 383]---> BDD-cost:    8
c ---[ 382]---> BDD-cost:    6
c ---[ 381]---> BDD-cost:    3
c ---[ 380]---> BDD-cost:    8
c ---[ 379]---> BDD-cost:    7
c ---[ 378]---> BDD-cost:    6
c ---[ 377]---> BDD-cost:    3
c ---[ 376]---> BDD-cost:   21
c ---[ 375]---> BDD-cost:    8
c ---[ 374]---> BDD-cost:    3
c ---[ 373]---> BDD-cost:    7
c ---[ 372]---> BDD-cost:   20
c ---[ 371]---> BDD-cost:    8
c ---[ 370]---> BDD-cost:    7
c ---[ 369]---> BDD-cost:   22
c ---[ 368]---> BDD-cost:   18
c ---[ 367]---> BDD-cost:    8
c ---[ 366]---> BDD-cost:    8
c ---[ 365]---> BDD-cost:    4
c ---[ 364]---> BDD-cost:    7
c ---[ 363]---> BDD-cost:    7
c ---[ 362]---> BDD-cost:   22
c ---[ 361]---> BDD-cost:    8
c ---[ 360]---> BDD-cost:    5
c ---[ 359]---> BDD-cost:    8
c ---[ 358]---> BDD-cost:    7
c ---[ 357]---> BDD-cost:   19
c ---[ 356]---> BDD-cost:    6
c ---[ 355]---> BDD-cost:    7
c ---[ 354]---> BDD-cost:    5
c ---[ 353]---> BDD-cost:    5
c ---[ 352]---> BDD-cost:    8
c ---[ 351]---> BDD-cost:    4
c ---[ 350]---> BDD-cost:    6
c ---[ 349]---> BDD-cost:    6
c ---[ 348]---> BDD-cost:    8
c ---[ 347]---> BDD-cost:    3
c ---[ 346]---> BDD-cost:    8
c ---[ 345]---> BDD-cost:    6
c ---[ 344]---> BDD-cost:    7
c ---[ 343]---> BDD-cost:    6
c ---[ 342]---> BDD-cost:    7
c ---[ 341]---> BDD-cost:    7
c ---[ 340]---> BDD-cost:    8
c ---[ 339]---> BDD-cost:    5
c ---[ 338]---> BDD-cost:    8
c ---[ 337]---> BDD-cost:    7
c ---[ 336]---> BDD-cost:    8
c ---[ 335]---> BDD-cost:    5
c ---[ 334]---> BDD-cost:    6
c ---[ 333]---> BDD-cost:   22
c ---[ 332]---> BDD-cost:   20
c ---[ 331]---> BDD-cost:    7
c ---[ 330]---> BDD-cost:    4
c ---[ 329]---> BDD-cost:   17
c ---[ 328]---> BDD-cost:    6
c ---[ 327]---> BDD-cost:    8
c ---[ 326]---> BDD-cost:    8
c ---[ 325]---> BDD-cost:    6
c ---[ 324]---> BDD-cost:    4
c ---[ 323]---> BDD-cost:    6
c ---[ 322]---> BDD-cost:    3
c ---[ 321]---> BDD-cost:    7
c ---[ 320]---> BDD-cost:    7
c ---[ 319]---> BDD-cost:    7
c ---[ 318]---> BDD-cost:    6
c ---[ 317]---> BDD-cost:   20
c ---[ 316]---> BDD-cost:    8
c ---[ 315]---> BDD-cost:    6
c ---[ 314]---> BDD-cost:    8
c ---[ 313]---> BDD-cost:    3
c ---[ 312]---> BDD-cost:    6
c ---[ 311]---> BDD-cost:    7
c ---[ 310]---> BDD-cost:    5
c ---[ 309]---> BDD-cost:    6
c ---[ 308]---> BDD-cost:   22
c ---[ 307]---> BDD-cost:   20
c ---[ 306]---> BDD-cost:    7
c ---[ 305]---> BDD-cost:   17
c ---[ 304]---> BDD-cost:    7
c ---[ 303]---> BDD-cost:    3
c ---[ 302]---> BDD-cost:   22
c ---[ 301]---> BDD-cost:   22
c ---[ 300]---> BDD-cost:    5
c ---[ 299]---> BDD-cost:    7
c ---[ 298]---> BDD-cost:   20
c ---[ 297]---> BDD-cost:    5
c ---[ 296]---> BDD-cost:    5
c ---[ 294]---> BDD-cost:   65
c ---[ 293]---> BDD-cost:    5
c ---[ 292]---> BDD-cost:    8
c ---[ 291]---> BDD-cost:    3
c ---[ 290]---> BDD-cost:    7
c ---[ 289]---> BDD-cost:    3
c ---[ 288]---> BDD-cost:    8
c ---[ 287]---> BDD-cost:    7
c ---[ 286]---> BDD-cost:    5
c ---[ 285]---> BDD-cost:    7
c ---[ 284]---> BDD-cost:    7
c ---[ 283]---> BDD-cost:   18
c ---[ 282]---> BDD-cost:    7
c ---[ 281]---> BDD-cost:    6
c ---[ 280]---> BDD-cost:   22
c ---[ 279]---> BDD-cost:    6
c ---[ 278]---> BDD-cost:    3
c ---[ 277]---> BDD-cost:    5
c ---[ 276]---> BDD-cost:   19
c ---[ 275]---> BDD-cost:    8
c ---[ 274]---> BDD-cost:    8
c ---[ 273]---> BDD-cost:    3
c ---[ 272]---> BDD-cost:    8
c ---[ 271]---> BDD-cost:    8
c ---[ 270]---> BDD-cost:    7
c ---[ 269]---> BDD-cost:    6
c ---[ 268]---> BDD-cost:    8
c ---[ 267]---> BDD-cost:    6
c ---[ 266]---> BDD-cost:    7
c ---[ 265]---> BDD-cost:    8
c ---[ 264]---> BDD-cost:    5
c ---[ 263]---> BDD-cost:    7
c ---[ 262]---> BDD-cost:    3
c ---[ 261]---> BDD-cost:    6
c ---[ 260]---> BDD-cost:    5
c ---[ 259]---> BDD-cost:    8
c ---[ 258]---> BDD-cost:    8
c ---[ 257]---> BDD-cost:    7
c ---[ 256]---> BDD-cost:   19
c ---[ 255]---> BDD-cost:    8
c ---[ 254]---> BDD-cost:    8
c ---[ 253]---> BDD-cost:    6
c ---[ 252]---> BDD-cost:   20
c ---[ 251]---> BDD-cost:    8
c ---[ 250]---> BDD-cost:    7
c ---[ 249]---> BDD-cost:    8
c ---[ 248]---> BDD-cost:    3
c ---[ 247]---> BDD-cost:    8
c ---[ 246]---> BDD-cost:    7
c ---[ 245]---> BDD-cost:    4
c ---[ 244]---> BDD-cost:    3
c ---[ 243]---> BDD-cost:    3
c ---[ 242]---> BDD-cost:    7
c ---[ 241]---> BDD-cost:    7
c ---[ 240]---> BDD-cost:    4
c ---[ 239]---> BDD-cost:    3
c ---[ 238]---> BDD-cost:   19
c ---[ 237]---> BDD-cost:    8
c ---[ 236]---> BDD-cost:    6
c ---[ 235]---> BDD-cost:    8
c ---[ 234]---> BDD-cost:    6
c ---[ 233]---> BDD-cost:   21
c ---[ 232]---> BDD-cost:    6
c ---[ 231]---> BDD-cost:    6
c ---[ 230]---> BDD-cost:    8
c ---[ 229]---> BDD-cost:   21
c ---[ 228]---> BDD-cost:    7
c ---[ 227]---> BDD-cost:    8
c ---[ 226]---> BDD-cost:    8
c ---[ 225]---> BDD-cost:    8
c ---[ 224]---> BDD-cost:   21
c ---[ 223]---> BDD-cost:    6
c ---[ 222]---> BDD-cost:    7
c ---[ 221]---> BDD-cost:    6
c ---[ 220]---> BDD-cost:    3
c ---[ 219]---> BDD-cost:   20
c ---[ 218]---> BDD-cost:   19
c ---[ 217]---> BDD-cost:   21
c ---[ 216]---> BDD-cost:    7
c ---[ 215]---> BDD-cost:    3
c ---[ 214]---> BDD-cost:    3
c ---[ 213]---> BDD-cost:    4
c ---[ 212]---> BDD-cost:    8
c ---[ 211]---> BDD-cost:    6
c ---[ 210]---> BDD-cost:    6
c ---[ 209]---> BDD-cost:    8
c ---[ 208]---> BDD-cost:    3
c ---[ 207]---> BDD-cost:    7
c ---[ 206]---> BDD-cost:    7
c ---[ 205]---> BDD-cost:    8
c ---[ 204]---> BDD-cost:    6
c ---[ 203]---> BDD-cost:    5
c ---[ 202]---> BDD-cost:    7
c ---[ 201]---> BDD-cost:    4
c ---[ 200]---> BDD-cost:    6
c ---[ 199]---> BDD-cost:    7
c ---[ 198]---> BDD-cost:    7
c ---[ 197]---> BDD-cost:   21
c ---[ 196]---> BDD-cost:   21
c ---[ 195]---> BDD-cost:    3
c ---[ 194]---> BDD-cost:    8
c ---[ 193]---> BDD-cost:    6
c ---[ 192]---> BDD-cost:    8
c ---[ 191]---> BDD-cost:    6
c ---[ 190]---> BDD-cost:    8
c ---[ 189]---> BDD-cost:    6
c ---[ 188]---> BDD-cost:    3
c ---[ 187]---> BDD-cost:    6
c ---[ 186]---> BDD-cost:    6
c ---[ 185]---> BDD-cost:    7
c ---[ 184]---> BDD-cost:    7
c ---[ 183]---> BDD-cost:    1
c ---[ 182]---> BDD-cost:    1
c ---[ 181]---> BDD-cost:    1
c ---[ 180]---> BDD-cost:    1
c ---[ 179]---> BDD-cost:    1
c ---[ 178]---> BDD-cost:    1
c ---[ 177]---> BDD-cost:    1
c ---[ 176]---> BDD-cost:    1
c ---[ 175]---> BDD-cost:    1
c ---[ 174]---> BDD-cost:    1
c ---[ 173]---> BDD-cost:    1
c ---[ 172]---> BDD-cost:    1
c ---[ 171]---> BDD-cost:    1
c ---[ 170]---> BDD-cost:    1
c ---[ 169]---> BDD-cost:    1
c ---[ 168]---> BDD-cost:    1
c ---[ 167]---> BDD-cost:    1
c ---[ 166]---> BDD-cost:    1
c ---[ 165]---> BDD-cost:    1
c ---[ 164]---> BDD-cost:    1
c ---[ 163]---> BDD-cost:    1
c ---[ 162]---> BDD-cost:    1
c ---[ 161]---> BDD-cost:    1
c ---[ 160]---> BDD-cost:    1
c ---[ 159]---> BDD-cost:    1
c ---[ 158]---> BDD-cost:    1
c ---[ 157]---> BDD-cost:    1
c ---[ 156]---> BDD-cost:    1
c ---[ 155]---> BDD-cost:    1
c ---[ 154]---> BDD-cost:    1
c ---[ 153]---> BDD-cost:    1
c ---[ 152]---> BDD-cost:    1
c ---[ 151]---> BDD-cost:    1
c ---[ 150]---> BDD-cost:    1
c ---[ 149]---> BDD-cost:    1
c ---[ 148]---> BDD-cost:    1
c ---[ 147]---> BDD-cost:    1
c ---[ 146]---> BDD-cost:    1
c ---[ 145]---> BDD-cost:    1
c ---[ 144]---> BDD-cost:    1
c ---[ 143]---> BDD-cost:    1
c ---[ 142]---> BDD-cost:    1
c ---[ 141]---> BDD-cost:    1
c ---[ 140]---> BDD-cost:    1
c ---[ 139]---> BDD-cost:    1
c ---[ 138]---> BDD-cost:    1
c ---[ 137]---> BDD-cost:    1
c ---[ 136]---> BDD-cost:    1
c ---[ 135]---> BDD-cost:    1
c ---[ 134]---> BDD-cost:    1
c ---[ 133]---> BDD-cost:    1
c ---[ 132]---> BDD-cost:    1
c ---[ 131]---> BDD-cost:    1
c ---[ 130]---> BDD-cost:    1
c ---[ 129]---> BDD-cost:    1
c ---[ 128]---> BDD-cost:    1
c ---[ 127]---> BDD-cost:    1
c ---[ 126]---> BDD-cost:    1
c ---[ 125]---> BDD-cost:    1
c ---[ 124]---> BDD-cost:    1
c ---[ 123]---> BDD-cost:    1
c ---[ 122]---> BDD-cost:    1
c ---[ 121]---> BDD-cost:    1
c ---[ 120]---> BDD-cost:    1
c ---[ 119]---> BDD-cost:    1
c ---[ 118]---> BDD-cost:    1
c ---[ 117]---> BDD-cost:    1
c ---[ 116]---> BDD-cost:    1
c ---[ 115]---> BDD-cost:    1
c ---[ 114]---> BDD-cost:    1
c ---[ 113]---> BDD-cost:    1
c ---[ 112]---> BDD-cost:    1
c ---[ 111]---> BDD-cost:    1
c ---[ 110]---> BDD-cost:    1
c ---[ 109]---> BDD-cost:    1
c ---[ 108]---> BDD-cost:    1
c ---[ 107]---> BDD-cost:    1
c ---[ 106]---> BDD-cost:    1
c ---[ 105]---> BDD-cost:    1
c ---[ 104]---> BDD-cost:    1
c ---[ 103]---> BDD-cost:    1
c ---[ 102]---> BDD-cost:    1
c ---[ 101]---> BDD-cost:    1
c ---[ 100]---> BDD-cost:    1
c ---[  99]---> BDD-cost:    1
c ---[  98]---> BDD-cost:    1
c ---[  97]---> BDD-cost:    1
c ---[  96]---> BDD-cost:    1
c ---[  95]---> BDD-cost:    1
c ---[  94]---> BDD-cost:    1
c ---[  93]---> BDD-cost:    1
c ---[  92]---> BDD-cost:    1
c ---[  91]---> BDD-cost:    1
c ---[  90]---> BDD-cost:    1
c ---[  89]---> BDD-cost:    1
c ---[  88]---> BDD-cost:    1
c ---[  87]---> BDD-cost:    1
c ---[  86]---> BDD-cost:    1
c ---[  85]---> BDD-cost:    1
c ---[  84]---> BDD-cost:    1
c ---[  83]---> BDD-cost:    1
c ---[  82]---> BDD-cost:    1
c ---[  81]---> BDD-cost:    1
c ---[  80]---> BDD-cost:    1
c ---[  79]---> BDD-cost:    1
c ---[  78]---> BDD-cost:    1
c ---[  77]---> BDD-cost:    1
c ---[  76]---> BDD-cost:    1
c ---[  75]---> BDD-cost:    1
c ---[  74]---> BDD-cost:    1
c ---[  73]---> BDD-cost:    1
c ---[  72]---> BDD-cost:    1
c ---[  71]---> BDD-cost:    1
c ---[  70]---> BDD-cost:    1
c ---[  69]---> BDD-cost:    1
c ---[  68]---> BDD-cost:    1
c ---[  67]---> BDD-cost:    1
c ---[  66]---> BDD-cost:    1
c ---[  65]---> BDD-cost:    1
c ---[  64]---> BDD-cost:    1
c ---[  63]---> BDD-cost:    1
c ---[  62]---> BDD-cost:    1
c ---[  61]---> BDD-cost:    1
c ---[  60]---> BDD-cost:    1
c ---[  59]---> BDD-cost:    1
c ---[  58]---> BDD-cost:    1
c ---[  57]---> BDD-cost:    1
c ---[  56]---> BDD-cost:    1
c ---[  55]---> BDD-cost:    1
c ---[  54]---> BDD-cost:    1
c ---[  53]---> BDD-cost:    1
c ---[  52]---> BDD-cost:    1
c ---[  51]---> BDD-cost:    1
c ---[  50]---> BDD-cost:    1
c ---[  49]---> BDD-cost:    1
c ---[  48]---> BDD-cost:    1
c ---[  47]---> BDD-cost:    1
c ---[  46]---> BDD-cost:    1
c ---[  45]---> BDD-cost:    1
c ---[  44]---> BDD-cost:    1
c ---[  43]---> BDD-cost:    1
c ---[  42]---> BDD-cost:    1
c ---[  41]---> BDD-cost:    1
c ---[  40]---> BDD-cost:    1
c ---[  39]---> BDD-cost:    1
c ---[  38]---> BDD-cost:    1
c ---[  37]---> BDD-cost:    1
c ---[  36]---> BDD-cost:    1
c ---[  35]---> BDD-cost:    1
c ---[  34]---> BDD-cost:    1
c ---[  33]---> BDD-cost:    1
c ---[  32]---> BDD-cost:    1
c ---[  31]---> BDD-cost:    1
c ---[  30]---> BDD-cost:    1
c ---[  29]---> BDD-cost:    1
c ---[  28]---> BDD-cost:    1
c ---[  27]---> BDD-cost:    1
c ---[  26]---> BDD-cost:    1
c ---[  25]---> BDD-cost:    1
c ---[  24]---> BDD-cost:    1
c ---[  23]---> BDD-cost:    1
c ---[  22]---> BDD-cost:    1
c ---[  21]---> BDD-cost:    1
c ---[  20]---> BDD-cost:    1
c ---[  19]---> BDD-cost:    1
c ---[  18]---> BDD-cost:    1
c ---[  17]---> BDD-cost:    1
c ---[  16]---> BDD-cost:    1
c ---[  15]---> BDD-cost:    1
c ---[  14]---> BDD-cost:    1
c ---[  13]---> BDD-cost:    1
c ---[  12]---> BDD-cost:    1
c ---[  11]---> BDD-cost:    1
c ---[  10]---> BDD-cost:    1
c ---[   9]---> BDD-cost:    1
c ---[   8]---> BDD-cost:    1
c ---[   7]---> BDD-cost:    1
c ---[   6]---> BDD-cost:    1
c ---[   5]---> BDD-cost:    1
c ---[   4]---> BDD-cost:    1
c ---[   3]---> BDD-cost:    1
c ---[   2]---> BDD-cost:    1
c ---[   1]---> BDD-cost:    1
c ---[   0]---> BDD-cost:    1
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |  647578  2266191 |  215859       0        0     nan |  0.000 % |
c |       100 |  647578  2266191 |  237444     100   102245  1022.5 |  3.726 % |
c |       250 |  647578  2266191 |  261189     250   106836   427.3 |  3.726 % |
c |       476 |  647562  2266139 |  287308     474   107969   227.8 |  3.727 % |
c |       813 |  647554  2266113 |  316039     810   109650   135.4 |  3.728 % |
c |      1319 |  647546  2266087 |  347643    1315   112045    85.2 |  3.729 % |
c |      2081 |  647546  2266087 |  382407    2077   295446   142.2 |  3.729 % |
c |      3223 |  647510  2265963 |  420648    3210   393131   122.5 |  3.732 % |
c |      4931 |  647501  2265932 |  462712    4915   586315   119.3 |  3.733 % |
c |      7493 |  647483  2265870 |  508984    7473   962893   128.8 |  3.735 % |
c |     11337 |  647425  2265674 |  559882   11306  1383585   122.4 |  3.741 % |
c |     17103 |  647408  2265617 |  615870   17065  2533779   148.5 |  3.742 % |
c |     25756 |  647373  2265498 |  677458   25710  4024336   156.5 |  3.746 % |
c |     38730 |  647210  2264941 |  745203   38641  7815121   202.2 |  3.761 % |
c |     58191 |  647124  2264647 |  819724   58078 13671715   235.4 |  3.769 % |
#### 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.81 0.95 0.93 2/54 24059
Raw data (stat): 24059 (runsolver) R 24058 22932 22931 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 491506352 1052672 99 4294967295 134512640 135381576 3221224432 3221219676 135158418 0 2147483391 7 90112 0 0 0 17 1 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0011 s]
Raw data (loadavg): 0.84 0.95 0.93 2/54 24059
Raw data (stat): 24059 (minisat+) R 24058 22932 22931 0 -1 0 13418 0 0 0 963 35 0 0 25 0 1 0 491506352 58093568 12942 4294967295 134512640 134672761 3221224544 3221223668 134566065 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14183 12942 603 41 0 14142 0
vsize: 56732
[startup+20.0013 s]
Raw data (loadavg): 0.86 0.95 0.93 2/54 24059
Raw data (stat): 24059 (minisat+) R 24058 22932 22931 0 -1 0 13461 0 0 0 1962 36 0 0 25 0 1 0 491506352 58228736 12985 4294967295 134512640 134672761 3221224544 3221223744 134557836 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14216 12985 603 41 0 14175 0
vsize: 56864
[startup+30.0025 s]
Raw data (loadavg): 0.88 0.95 0.93 2/54 24059
Raw data (stat): 24059 (minisat+) R 24058 22932 22931 0 -1 0 13639 0 0 0 2960 37 0 0 25 0 1 0 491506352 59039744 13163 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14414 13163 603 41 0 14373 0
vsize: 57656
[startup+40.0028 s]
Raw data (loadavg): 0.90 0.96 0.93 2/54 24059
Raw data (stat): 24059 (minisat+) R 24058 22932 22931 0 -1 0 13679 0 0 0 3959 37 0 0 25 0 1 0 491506352 59174912 13203 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14447 13203 603 41 0 14406 0
vsize: 57788
[startup+50.0021 s]
Raw data (loadavg): 0.91 0.96 0.93 2/54 24059
Raw data (stat): 24059 (minisat+) R 24058 22932 22931 0 -1 0 13774 0 0 0 4959 38 0 0 25 0 1 0 491506352 59580416 13298 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14546 13298 603 41 0 14505 0
vsize: 58184
[startup+60.0024 s]
Raw data (loadavg): 0.93 0.96 0.93 2/54 24059
Raw data (stat): 24059 (minisat+) R 24058 22932 22931 0 -1 0 13856 0 0 0 5959 38 0 0 25 0 1 0 491506352 59850752 13380 4294967295 134512640 134672761 3221224544 3221223744 134557809 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14612 13380 603 41 0 14571 0
vsize: 58448
[startup+70.0027 s]
Raw data (loadavg): 0.94 0.96 0.93 2/54 24059
Raw data (stat): 24059 (minisat+) R 24058 22932 22931 0 -1 0 13954 0 0 0 6958 39 0 0 25 0 1 0 491506352 60252160 13478 4294967295 134512640 134672761 3221224544 3221223712 134560895 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14710 13478 603 41 0 14669 0
vsize: 58840
[startup+80.0029 s]
Raw data (loadavg): 0.95 0.96 0.93 2/54 24059
Raw data (stat): 24059 (minisat+) R 24058 22932 22931 0 -1 0 14017 0 0 0 7957 39 0 0 25 0 1 0 491506352 60518400 13541 4294967295 134512640 134672761 3221224544 3221223700 134561032 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14775 13541 603 41 0 14734 0
vsize: 59100
[startup+90.0029 s]
Raw data (loadavg): 0.95 0.96 0.93 2/54 24059
Raw data (stat): 24059 (minisat+) R 24058 22932 22931 0 -1 0 14124 0 0 0 8957 39 0 0 25 0 1 0 491506352 61050880 13648 4294967295 134512640 134672761 3221224544 3221223712 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14905 13648 603 41 0 14864 0
vsize: 59620
[startup+100.003 s]
Raw data (loadavg): 0.96 0.96 0.93 2/54 24059
Raw data (stat): 24059 (minisat+) R 24058 22932 22931 0 -1 0 14212 0 0 0 9957 40 0 0 25 0 1 0 491506352 61321216 13736 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14971 13736 603 41 0 14930 0
vsize: 59884
[startup+110.003 s]
Raw data (loadavg): 0.97 0.96 0.93 2/54 24059
Raw data (stat): 24059 (minisat+) R 24058 22932 22931 0 -1 0 14328 0 0 0 10957 40 0 0 25 0 1 0 491506352 61853696 13852 4294967295 134512640 134672761 3221224544 3221223648 134560510 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15101 13852 603 41 0 15060 0
vsize: 60404
[startup+120.003 s]
Raw data (loadavg): 0.97 0.96 0.93 2/54 24059
Raw data (stat): 24059 (minisat+) R 24058 22932 22931 0 -1 0 14416 0 0 0 11956 41 0 0 25 0 1 0 491506352 62255104 13940 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15199 13940 603 41 0 15158 0
vsize: 60796
[startup+130.003 s]
Raw data (loadavg): 0.98 0.96 0.93 2/54 24059
Raw data (stat): 24059 (minisat+) R 24058 22932 22931 0 -1 0 14497 0 0 0 12956 41 0 0 25 0 1 0 491506352 62558208 14021 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15273 14021 603 41 0 15232 0
vsize: 61092
[startup+140.003 s]
Raw data (loadavg): 0.98 0.97 0.93 2/54 24059
Raw data (stat): 24059 (minisat+) R 24058 22932 22931 0 -1 0 14567 0 0 0 13956 41 0 0 25 0 1 0 491506352 62828544 14091 4294967295 134512640 134672761 3221224544 3221223748 134561964 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15339 14091 603 41 0 15298 0
vsize: 61356
[startup+150.003 s]
Raw data (loadavg): 0.98 0.97 0.93 2/54 24059
Raw data (stat): 24059 (minisat+) R 24058 22932 22931 0 -1 0 14671 0 0 0 14956 41 0 0 25 0 1 0 491506352 63229952 14195 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15437 14195 603 41 0 15396 0
vsize: 61748
[startup+160.003 s]
Raw data (loadavg): 0.98 0.97 0.93 2/54 24059
Raw data (stat): 24059 (minisat+) R 24058 22932 22931 0 -1 0 14799 0 0 0 15956 42 0 0 25 0 1 0 491506352 63770624 14323 4294967295 134512640 134672761 3221224544 3221223712 134561201 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15569 14323 603 41 0 15528 0
vsize: 62276
[startup+170.003 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 24059
Raw data (stat): 24059 (minisat+) R 24058 22932 22931 0 -1 0 14967 0 0 0 16955 43 0 0 25 0 1 0 491506352 64438272 14491 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15732 14491 603 41 0 15691 0
vsize: 62928
[startup+180.004 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 24059
Raw data (stat): 24059 (minisat+) R 24058 22932 22931 0 -1 0 15185 0 0 0 17954 44 0 0 25 0 1 0 491506352 65372160 14709 4294967295 134512640 134672761 3221224544 3221223648 134559869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15960 14709 603 41 0 15919 0
vsize: 63840
[startup+190.004 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 24059
Raw data (stat): 24059 (minisat+) R 24058 22932 22931 0 -1 0 15293 0 0 0 18954 44 0 0 25 0 1 0 491506352 65777664 14817 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16059 14817 603 41 0 16018 0
vsize: 64236
[startup+200.004 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 24059
Raw data (stat): 24059 (minisat+) R 24058 22932 22931 0 -1 0 15396 0 0 0 19954 44 0 0 25 0 1 0 491506352 66179072 14920 4294967295 134512640 134672761 3221224544 3221223712 134560871 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16157 14920 603 41 0 16116 0
vsize: 64628
[startup+210.004 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 24059
Raw data (stat): 24059 (minisat+) R 24058 22932 22931 0 -1 0 15497 0 0 0 20954 44 0 0 25 0 1 0 491506352 66584576 15021 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16256 15021 603 41 0 16215 0
vsize: 65024
[startup+220.005 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 24059
Raw data (stat): 24059 (minisat+) R 24058 22932 22931 0 -1 0 15629 0 0 0 21954 45 0 0 25 0 1 0 491506352 67125248 15153 4294967295 134512640 134672761 3221224544 3221223744 134557911 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16388 15153 603 41 0 16347 0
vsize: 65552
[startup+230.005 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 24059
Raw data (stat): 24059 (minisat+) R 24058 22932 22931 0 -1 0 15772 0 0 0 22953 46 0 0 25 0 1 0 491506352 67796992 15296 4294967295 134512640 134672761 3221224544 3221223648 134560506 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16552 15296 603 41 0 16511 0
vsize: 66208
[startup+240.006 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 24059
Raw data (stat): 24059 (minisat+) R 24058 22932 22931 0 -1 0 15884 0 0 0 23953 46 0 0 25 0 1 0 491506352 68198400 15408 4294967295 134512640 134672761 3221224544 3221223744 134557830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16650 15408 603 41 0 16609 0
vsize: 66600
[startup+250.005 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 24059
Raw data (stat): 24059 (minisat+) R 24058 22932 22931 0 -1 0 16018 0 0 0 24953 46 0 0 25 0 1 0 491506352 68849664 15542 4294967295 134512640 134672761 3221224544 3221223712 134560892 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16809 15542 603 41 0 16768 0
vsize: 67236
[startup+260.005 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 24059
Raw data (stat): 24059 (minisat+) R 24058 22932 22931 0 -1 0 16139 0 0 0 25952 47 0 0 25 0 1 0 491506352 69255168 15663 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16908 15663 603 41 0 16867 0
vsize: 67632
[startup+270.006 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 24059
Raw data (stat): 24059 (minisat+) R 24058 22932 22931 0 -1 0 16198 0 0 0 26952 47 0 0 25 0 1 0 491506352 69525504 15722 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16974 15722 603 41 0 16933 0
vsize: 67896
[startup+280.006 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 24059
Raw data (stat): 24059 (minisat+) R 24058 22932 22931 0 -1 0 16257 0 0 0 27951 48 0 0 25 0 1 0 491506352 69795840 15781 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17040 15781 603 41 0 16999 0
vsize: 68160
[startup+290.006 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 24059
Raw data (stat): 24059 (minisat+) R 24058 22932 22931 0 -1 0 16401 0 0 0 28950 48 0 0 25 0 1 0 491506352 70336512 15925 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17172 15925 603 41 0 17131 0
vsize: 68688
[startup+300.007 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 24059
Raw data (stat): 24059 (minisat+) R 24058 22932 22931 0 -1 0 16561 0 0 0 29950 49 0 0 25 0 1 0 491506352 71012352 16085 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17337 16085 603 41 0 17296 0
vsize: 69348
[startup+310.007 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 24059
Raw data (stat): 24059 (minisat+) R 24058 22932 22931 0 -1 0 16698 0 0 0 30949 49 0 0 25 0 1 0 491506352 71553024 16222 4294967295 134512640 134672761 3221224544 3221223712 134560980 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17469 16222 603 41 0 17428 0
vsize: 69876
[startup+320.006 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 24059
Raw data (stat): 24059 (minisat+) R 24058 22932 22931 0 -1 0 16909 0 0 0 31949 50 0 0 25 0 1 0 491506352 72491008 16433 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17698 16433 603 41 0 17657 0
vsize: 70792
[startup+330.007 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 24059
Raw data (stat): 24059 (minisat+) R 24058 22932 22931 0 -1 0 17142 0 0 0 32948 51 0 0 25 0 1 0 491506352 73437184 16666 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17929 16666 603 41 0 17888 0
vsize: 71716
[startup+340.007 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 24059
Raw data (stat): 24059 (minisat+) R 24058 22932 22931 0 -1 0 17337 0 0 0 33948 51 0 0 25 0 1 0 491506352 74244096 16861 4294967295 134512640 134672761 3221224544 3221223648 134560184 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18126 16861 603 41 0 18085 0
vsize: 72504
[startup+350.006 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 24059
Raw data (stat): 24059 (minisat+) R 24058 22932 22931 0 -1 0 17563 0 0 0 34947 52 0 0 25 0 1 0 491506352 75051008 17087 4294967295 134512640 134672761 3221224544 3221223712 134561400 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18323 17087 603 41 0 18282 0
vsize: 73292
[startup+360.007 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 24059
Raw data (stat): 24059 (minisat+) R 24058 22932 22931 0 -1 0 17668 0 0 0 35947 52 0 0 25 0 1 0 491506352 75587584 17192 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18454 17192 603 41 0 18413 0
vsize: 73816
[startup+370.008 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 24059
Raw data (stat): 24059 (minisat+) R 24058 22932 22931 0 -1 0 17713 0 0 0 36947 53 0 0 25 0 1 0 491506352 75718656 17237 4294967295 134512640 134672761 3221224544 3221223680 134560688 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18486 17237 603 41 0 18445 0
vsize: 73944
[startup+380.008 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 24059
Raw data (stat): 24059 (minisat+) R 24058 22932 22931 0 -1 0 17978 0 0 0 37947 54 0 0 25 0 1 0 491506352 76795904 17502 4294967295 134512640 134672761 3221224544 3221223680 134560688 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18749 17502 603 41 0 18708 0
vsize: 74996
[startup+390.008 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 24059
Raw data (stat): 24059 (minisat+) R 24058 22932 22931 0 -1 0 18286 0 0 0 38945 55 0 0 25 0 1 0 491506352 78012416 17810 4294967295 134512640 134672761 3221224544 3221223648 134560048 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19046 17810 603 41 0 19005 0
vsize: 76184
[startup+400.009 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 24059
Raw data (stat): 24059 (minisat+) R 24058 22932 22931 0 -1 0 18548 0 0 0 39944 56 0 0 25 0 1 0 491506352 79093760 18072 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19310 18072 603 41 0 19269 0
vsize: 77240
[startup+410.009 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 24059
Raw data (stat): 24059 (minisat+) R 24058 22932 22931 0 -1 0 18838 0 0 0 40943 57 0 0 25 0 1 0 491506352 80306176 18362 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19606 18362 603 41 0 19565 0
vsize: 78424
[startup+420.009 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 24059
Raw data (stat): 24059 (minisat+) R 24058 22932 22931 0 -1 0 19096 0 0 0 41943 58 0 0 25 0 1 0 491506352 81379328 18620 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19868 18620 603 41 0 19827 0
vsize: 79472
[startup+430.01 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 24059
Raw data (stat): 24059 (minisat+) R 24058 22932 22931 0 -1 0 19434 0 0 0 42943 59 0 0 25 0 1 0 491506352 82731008 18958 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20198 18958 603 41 0 20157 0
vsize: 80792
[startup+440.011 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 24059
Raw data (stat): 24059 (minisat+) R 24058 22932 22931 0 -1 0 19740 0 0 0 43942 60 0 0 25 0 1 0 491506352 83943424 19264 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20494 19264 603 41 0 20453 0
vsize: 81976
[startup+450.011 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 24059
Raw data (stat): 24059 (minisat+) R 24058 22932 22931 0 -1 0 20028 0 0 0 44942 60 0 0 25 0 1 0 491506352 85155840 19552 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20790 19552 603 41 0 20749 0
vsize: 83160
[startup+460.011 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 24059
Raw data (stat): 24059 (minisat+) R 24058 22932 22931 0 -1 0 20267 0 0 0 45941 61 0 0 25 0 1 0 491506352 86228992 19791 4294967295 134512640 134672761 3221224544 3221223744 134557828 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21052 19791 603 41 0 21011 0
vsize: 84208
[startup+470.012 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 24059
Raw data (stat): 24059 (minisat+) R 24058 22932 22931 0 -1 0 20530 0 0 0 46941 61 0 0 25 0 1 0 491506352 87306240 20054 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21315 20054 603 41 0 21274 0
vsize: 85260
[startup+480.013 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 24059
Raw data (stat): 24059 (minisat+) R 24058 22932 22931 0 -1 0 20795 0 0 0 47940 62 0 0 25 0 1 0 491506352 88387584 20319 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21579 20319 603 41 0 21538 0
vsize: 86316
[startup+490.013 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 24059
Raw data (stat): 24059 (minisat+) R 24058 22932 22931 0 -1 0 21036 0 0 0 48939 63 0 0 25 0 1 0 491506352 89468928 20560 4294967295 134512640 134672761 3221224544 3221223728 134558662 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21843 20560 603 41 0 21802 0
vsize: 87372
[startup+500.012 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 24059
Raw data (stat): 24059 (minisat+) R 24058 22932 22931 0 -1 0 21276 0 0 0 49939 64 0 0 25 0 1 0 491506352 90415104 20800 4294967295 134512640 134672761 3221224544 3221223716 134556651 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22074 20800 603 41 0 22033 0
vsize: 88296
[startup+510.012 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 24059
Raw data (stat): 24059 (minisat+) R 24058 22932 22931 0 -1 0 21309 0 0 0 50939 64 0 0 25 0 1 0 491506352 90550272 20833 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22107 20833 603 41 0 22066 0
vsize: 88428
[startup+520.012 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 24059
Raw data (stat): 24059 (minisat+) R 24058 22932 22931 0 -1 0 21412 0 0 0 51939 64 0 0 25 0 1 0 491506352 90955776 20936 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22206 20936 603 41 0 22165 0
vsize: 88824
[startup+530.012 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 24059
Raw data (stat): 24059 (minisat+) R 24058 22932 22931 0 -1 0 21480 0 0 0 52939 64 0 0 25 0 1 0 491506352 91226112 21004 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22272 21004 603 41 0 22231 0
vsize: 89088
[startup+540.014 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 24059
Raw data (stat): 24059 (minisat+) R 24058 22932 22931 0 -1 0 21562 0 0 0 53939 64 0 0 25 0 1 0 491506352 91631616 21086 4294967295 134512640 134672761 3221224544 3221223744 134557836 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22371 21086 603 41 0 22330 0
vsize: 89484
[startup+550.013 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 24059
Raw data (stat): 24059 (minisat+) R 24058 22932 22931 0 -1 0 21714 0 0 0 54938 65 0 0 25 0 1 0 491506352 92168192 21238 4294967295 134512640 134672761 3221224544 3221223712 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22502 21238 603 41 0 22461 0
vsize: 90008
[startup+560.013 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 24059
Raw data (stat): 24059 (minisat+) R 24058 22932 22931 0 -1 0 22196 0 0 0 55936 67 0 0 25 0 1 0 491506352 94191616 21720 4294967295 134512640 134672761 3221224544 3221223680 134560688 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22996 21720 603 41 0 22955 0
vsize: 91984
[startup+570.013 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 24059
Raw data (stat): 24059 (minisat+) R 24058 22932 22931 0 -1 0 22698 0 0 0 56936 68 0 0 25 0 1 0 491506352 96210944 22222 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23489 22222 603 41 0 23448 0
vsize: 93956
[startup+580.014 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 24059
Raw data (stat): 24059 (minisat+) R 24058 22932 22931 0 -1 0 23183 0 0 0 57935 69 0 0 25 0 1 0 491506352 98250752 22707 4294967295 134512640 134672761 3221224544 3221223648 134560367 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23987 22707 603 41 0 23946 0
vsize: 95948
[startup+590.013 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 24059
Raw data (stat): 24059 (minisat+) R 24058 22932 22931 0 -1 0 23819 0 0 0 58934 70 0 0 25 0 1 0 491506352 100859904 23343 4294967295 134512640 134672761 3221224544 3221223648 134559914 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24624 23343 603 41 0 24583 0
vsize: 98496
[startup+600.013 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 24059
Raw data (stat): 24059 (minisat+) R 24058 22932 22931 0 -1 0 23972 0 0 0 59933 71 0 0 25 0 1 0 491506352 101404672 23496 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24757 23496 603 41 0 24716 0
vsize: 99028
[startup+610.014 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 24059
Raw data (stat): 24059 (minisat+) R 24058 22932 22931 0 -1 0 24035 0 0 0 60933 71 0 0 25 0 1 0 491506352 101670912 23559 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24822 23559 603 41 0 24781 0
vsize: 99288
[startup+620.013 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 24059
Raw data (stat): 24059 (minisat+) R 24058 22932 22931 0 -1 0 24133 0 0 0 61932 72 0 0 25 0 1 0 491506352 102076416 23657 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24921 23657 603 41 0 24880 0
vsize: 99684
[startup+630.014 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 24059
Raw data (stat): 24059 (minisat+) R 24058 22932 22931 0 -1 0 24225 0 0 0 62932 72 0 0 25 0 1 0 491506352 102477824 23749 4294967295 134512640 134672761 3221224544 3221223712 134560903 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25019 23749 603 41 0 24978 0
vsize: 100076
[startup+640.015 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 24059
Raw data (stat): 24059 (minisat+) R 24058 22932 22931 0 -1 0 24334 0 0 0 63932 73 0 0 25 0 1 0 491506352 102883328 23858 4294967295 134512640 134672761 3221224544 3221223744 134557830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25118 23858 603 41 0 25077 0
vsize: 100472
[startup+650.014 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 24059
Raw data (stat): 24059 (minisat+) R 24058 22932 22931 0 -1 0 24452 0 0 0 64932 73 0 0 25 0 1 0 491506352 103424000 23976 4294967295 134512640 134672761 3221224544 3221223712 134560882 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25250 23976 603 41 0 25209 0
vsize: 101000
[startup+660.014 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 24059
Raw data (stat): 24059 (minisat+) R 24058 22932 22931 0 -1 0 24565 0 0 0 65931 74 0 0 25 0 1 0 491506352 103821312 24089 4294967295 134512640 134672761 3221224544 3221223648 134560235 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25347 24089 603 41 0 25306 0
vsize: 101388
[startup+670.015 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 24059
Raw data (stat): 24059 (minisat+) R 24058 22932 22931 0 -1 0 24689 0 0 0 66930 75 0 0 25 0 1 0 491506352 104357888 24213 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25478 24213 603 41 0 25437 0
vsize: 101912
[startup+680.015 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 24059
Raw data (stat): 24059 (minisat+) R 24058 22932 22931 0 -1 0 24840 0 0 0 67930 75 0 0 25 0 1 0 491506352 105029632 24364 4294967295 134512640 134672761 3221224544 3221223712 134560839 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25642 24364 603 41 0 25601 0
vsize: 102568
[startup+690.014 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 24059
Raw data (stat): 24059 (minisat+) R 24058 22932 22931 0 -1 0 24973 0 0 0 68930 76 0 0 25 0 1 0 491506352 105562112 24497 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25772 24497 603 41 0 25731 0
vsize: 103088
[startup+700.014 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 24059
Raw data (stat): 24059 (minisat+) R 24058 22932 22931 0 -1 0 25094 0 0 0 69930 76 0 0 25 0 1 0 491506352 105967616 24618 4294967295 134512640 134672761 3221224544 3221223728 134558687 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25871 24618 603 41 0 25830 0
vsize: 103484
[startup+710.015 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 24059
Raw data (stat): 24059 (minisat+) R 24058 22932 22931 0 -1 0 25256 0 0 0 70929 77 0 0 25 0 1 0 491506352 106639360 24780 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26035 24780 603 41 0 25994 0
vsize: 104140
[startup+720.015 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 24059
Raw data (stat): 24059 (minisat+) R 24058 22932 22931 0 -1 0 25394 0 0 0 71929 77 0 0 25 0 1 0 491506352 107171840 24918 4294967295 134512640 134672761 3221224544 3221223648 134560350 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26165 24918 603 41 0 26124 0
vsize: 104660
[startup+730.015 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 24059
Raw data (stat): 24059 (minisat+) R 24058 22932 22931 0 -1 0 25560 0 0 0 72929 78 0 0 25 0 1 0 491506352 107847680 25084 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26330 25084 603 41 0 26289 0
vsize: 105320
[startup+740.016 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 24059
Raw data (stat): 24059 (minisat+) R 24058 22932 22931 0 -1 0 25727 0 0 0 73928 79 0 0 25 0 1 0 491506352 108523520 25251 4294967295 134512640 134672761 3221224544 3221223648 134559925 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26495 25251 603 41 0 26454 0
vsize: 105980
[startup+750.015 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 24059
Raw data (stat): 24059 (minisat+) R 24058 22932 22931 0 -1 0 25896 0 0 0 74928 79 0 0 25 0 1 0 491506352 109334528 25420 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26693 25420 603 41 0 26652 0
vsize: 106772
[startup+760.015 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 24059
Raw data (stat): 24059 (minisat+) R 24058 22932 22931 0 -1 0 26051 0 0 0 75928 79 0 0 25 0 1 0 491506352 109875200 25575 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26825 25575 603 41 0 26784 0
vsize: 107300
[startup+770.015 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 24059
Raw data (stat): 24059 (minisat+) R 24058 22932 22931 0 -1 0 26173 0 0 0 76928 79 0 0 25 0 1 0 491506352 110415872 25697 4294967295 134512640 134672761 3221224544 3221223728 134558341 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26957 25697 603 41 0 26916 0
vsize: 107828
[startup+780.016 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 24059
Raw data (stat): 24059 (minisat+) R 24058 22932 22931 0 -1 0 26306 0 0 0 77928 80 0 0 25 0 1 0 491506352 110956544 25830 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27089 25830 603 41 0 27048 0
vsize: 108356
[startup+790.016 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 24059
Raw data (stat): 24059 (minisat+) R 24058 22932 22931 0 -1 0 26468 0 0 0 78928 80 0 0 25 0 1 0 491506352 111628288 25992 4294967295 134512640 134672761 3221224544 3221223712 134560871 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27253 25992 603 41 0 27212 0
vsize: 109012
[startup+800.015 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 24059
Raw data (stat): 24059 (minisat+) R 24058 22932 22931 0 -1 0 26598 0 0 0 79927 81 0 0 25 0 1 0 491506352 112164864 26122 4294967295 134512640 134672761 3221224544 3221223744 134557842 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27384 26122 603 41 0 27343 0
vsize: 109536
[startup+810.016 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 24059
Raw data (stat): 24059 (minisat+) R 24058 22932 22931 0 -1 0 26755 0 0 0 80927 81 0 0 25 0 1 0 491506352 112836608 26279 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27548 26279 603 41 0 27507 0
vsize: 110192
[startup+820.016 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 24059
Raw data (stat): 24059 (minisat+) R 24058 22932 22931 0 -1 0 26921 0 0 0 81926 82 0 0 25 0 1 0 491506352 113508352 26445 4294967295 134512640 134672761 3221224544 3221223728 134558899 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27712 26445 603 41 0 27671 0
vsize: 110848
[startup+830.016 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 24059
Raw data (stat): 24059 (minisat+) R 24058 22932 22931 0 -1 0 27084 0 0 0 82926 82 0 0 25 0 1 0 491506352 114184192 26608 4294967295 134512640 134672761 3221224544 3221223712 134560929 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27877 26608 603 41 0 27836 0
vsize: 111508
[startup+840.017 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 24059
Raw data (stat): 24059 (minisat+) R 24058 22932 22931 0 -1 0 27258 0 0 0 83926 83 0 0 25 0 1 0 491506352 114860032 26782 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28042 26782 603 41 0 28001 0
vsize: 112168
[startup+850.017 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 24059
Raw data (stat): 24059 (minisat+) R 24058 22932 22931 0 -1 0 27436 0 0 0 84926 83 0 0 25 0 1 0 491506352 115531776 26960 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28206 26960 603 41 0 28165 0
vsize: 112824
[startup+860.017 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 24059
Raw data (stat): 24059 (minisat+) R 24058 22932 22931 0 -1 0 27604 0 0 0 85926 83 0 0 25 0 1 0 491506352 116203520 27128 4294967295 134512640 134672761 3221224544 3221223744 134557836 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28370 27128 603 41 0 28329 0
vsize: 113480
[startup+870.017 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 24059
Raw data (stat): 24059 (minisat+) R 24058 22932 22931 0 -1 0 27822 0 0 0 86924 85 0 0 25 0 1 0 491506352 117149696 27346 4294967295 134512640 134672761 3221224544 3221223728 134559622 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28601 27348 603 41 0 28560 0
vsize: 114404
[startup+880.018 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 24059
Raw data (stat): 24059 (minisat+) R 24058 22932 22931 0 -1 0 27956 0 0 0 87924 85 0 0 25 0 1 0 491506352 117694464 27480 4294967295 134512640 134672761 3221224544 3221223648 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28734 27480 603 41 0 28693 0
vsize: 114936
[startup+890.017 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 24059
Raw data (stat): 24059 (minisat+) R 24058 22932 22931 0 -1 0 28104 0 0 0 88924 85 0 0 25 0 1 0 491506352 118231040 27628 4294967295 134512640 134672761 3221224544 3221223744 134557806 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28865 27628 603 41 0 28824 0
vsize: 115460
[startup+900.017 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 24059
Raw data (stat): 24059 (minisat+) R 24058 22932 22931 0 -1 0 28261 0 0 0 89924 86 0 0 25 0 1 0 491506352 118906880 27785 4294967295 134512640 134672761 3221224544 3221223680 134560673 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29030 27785 603 41 0 28989 0
vsize: 116120
[startup+910.018 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 24059
Raw data (stat): 24059 (minisat+) R 24058 22932 22931 0 -1 0 28445 0 0 0 90923 86 0 0 25 0 1 0 491506352 119713792 27969 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29227 27969 603 41 0 29186 0
vsize: 116908
[startup+920.017 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 24059
Raw data (stat): 24059 (minisat+) R 24058 22932 22931 0 -1 0 28654 0 0 0 91923 87 0 0 25 0 1 0 491506352 120524800 28178 4294967295 134512640 134672761 3221224544 3221223712 134560937 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29425 28178 603 41 0 29384 0
vsize: 117700
[startup+930.018 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 24059
Raw data (stat): 24059 (minisat+) R 24058 22932 22931 0 -1 0 28803 0 0 0 92923 88 0 0 25 0 1 0 491506352 121196544 28327 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29589 28327 603 41 0 29548 0
vsize: 118356
[startup+940.019 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 24059
Raw data (stat): 24059 (minisat+) R 24058 22932 22931 0 -1 0 29452 0 0 0 93922 89 0 0 25 0 1 0 491506352 124026880 28976 4294967295 134512640 134672761 3221224544 3221223680 134560716 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30280 28976 603 41 0 30239 0
vsize: 121120
[startup+950.018 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 24059
Raw data (stat): 24059 (minisat+) R 24058 22932 22931 0 -1 0 30113 0 0 0 94920 90 0 0 25 0 1 0 491506352 126726144 29637 4294967295 134512640 134672761 3221224544 3221223668 134566034 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30939 29637 603 41 0 30898 0
vsize: 123756
[startup+960.018 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 24059
Raw data (stat): 24059 (minisat+) R 24058 22932 22931 0 -1 0 30179 0 0 0 95920 91 0 0 25 0 1 0 491506352 127004672 29703 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31007 29703 603 41 0 30966 0
vsize: 124028
[startup+970.019 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 24059
Raw data (stat): 24059 (minisat+) R 24058 22932 22931 0 -1 0 30263 0 0 0 96920 91 0 0 25 0 1 0 491506352 127406080 29787 4294967295 134512640 134672761 3221224544 3221223680 134560688 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31105 29787 603 41 0 31064 0
vsize: 124420
[startup+980.019 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 24059
Raw data (stat): 24059 (minisat+) R 24058 22932 22931 0 -1 0 30377 0 0 0 97920 91 0 0 25 0 1 0 491506352 127803392 29901 4294967295 134512640 134672761 3221224544 3221223712 134560988 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31202 29901 603 41 0 31161 0
vsize: 124808
[startup+990.019 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 24059
Raw data (stat): 24059 (minisat+) R 24058 22932 22931 0 -1 0 30481 0 0 0 98920 91 0 0 25 0 1 0 491506352 128208896 30005 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31301 30005 603 41 0 31260 0
vsize: 125204
[startup+1000.02 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 24059
Raw data (stat): 24059 (minisat+) R 24058 22932 22931 0 -1 0 30579 0 0 0 99920 92 0 0 25 0 1 0 491506352 128610304 30103 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31399 30103 603 41 0 31358 0
vsize: 125596
[startup+1010.02 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 24059
Raw data (stat): 24059 (minisat+) R 24058 22932 22931 0 -1 0 30681 0 0 0 100920 92 0 0 25 0 1 0 491506352 129011712 30205 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31497 30205 603 41 0 31456 0
vsize: 125988
[startup+1020.02 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 24059
Raw data (stat): 24059 (minisat+) R 24058 22932 22931 0 -1 0 30795 0 0 0 101920 92 0 0 25 0 1 0 491506352 129544192 30319 4294967295 134512640 134672761 3221224544 3221223716 134556688 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31627 30319 603 41 0 31586 0
vsize: 126508
[startup+1030.02 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 24059
Raw data (stat): 24059 (minisat+) R 24058 22932 22931 0 -1 0 30887 0 0 0 102919 93 0 0 25 0 1 0 491506352 129937408 30411 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31723 30411 603 41 0 31682 0
vsize: 126892
[startup+1040.02 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 24059
Raw data (stat): 24059 (minisat+) R 24058 22932 22931 0 -1 0 30975 0 0 0 103919 93 0 0 25 0 1 0 491506352 130207744 30499 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31789 30499 603 41 0 31748 0
vsize: 127156
[startup+1050.02 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 24059
Raw data (stat): 24059 (minisat+) R 24058 22932 22931 0 -1 0 31081 0 0 0 104920 93 0 0 25 0 1 0 491506352 130744320 30605 4294967295 134512640 134672761 3221224544 3221223712 134560888 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31920 30605 603 41 0 31879 0
vsize: 127680
[startup+1060.02 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 24059
Raw data (stat): 24059 (minisat+) R 24058 22932 22931 0 -1 0 31215 0 0 0 105919 93 0 0 25 0 1 0 491506352 131276800 30739 4294967295 134512640 134672761 3221224544 3221223648 134559887 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32050 30739 603 41 0 32009 0
vsize: 128200
[startup+1070.02 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 24059
Raw data (stat): 24059 (minisat+) R 24058 22932 22931 0 -1 0 31388 0 0 0 106919 94 0 0 25 0 1 0 491506352 131948544 30912 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32214 30912 603 41 0 32173 0
vsize: 128856
[startup+1080.02 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 24059
Raw data (stat): 24059 (minisat+) R 24058 22932 22931 0 -1 0 31615 0 0 0 107919 94 0 0 25 0 1 0 491506352 132894720 31139 4294967295 134512640 134672761 3221224544 3221223648 134559966 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32445 31139 603 41 0 32404 0
vsize: 129780
[startup+1090.02 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 24059
Raw data (stat): 24059 (minisat+) R 24058 22932 22931 0 -1 0 31845 0 0 0 108918 95 0 0 25 0 1 0 491506352 133828608 31369 4294967295 134512640 134672761 3221224544 3221223712 134560833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32673 31369 603 41 0 32632 0
vsize: 130692
[startup+1100.02 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 24059
Raw data (stat): 24059 (minisat+) R 24058 22932 22931 0 -1 0 32027 0 0 0 109918 96 0 0 25 0 1 0 491506352 134504448 31551 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32838 31551 603 41 0 32797 0
vsize: 131352
[startup+1110.02 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 24059
Raw data (stat): 24059 (minisat+) R 24058 22932 22931 0 -1 0 32193 0 0 0 110918 96 0 0 25 0 1 0 491506352 135180288 31717 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33003 31717 603 41 0 32962 0
vsize: 132012
[startup+1120.02 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 24059
Raw data (stat): 24059 (minisat+) R 24058 22932 22931 0 -1 0 32375 0 0 0 111918 96 0 0 25 0 1 0 491506352 135991296 31899 4294967295 134512640 134672761 3221224544 3221223712 134561385 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33201 31899 603 41 0 33160 0
vsize: 132804
[startup+1130.02 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 24059
Raw data (stat): 24059 (minisat+) R 24058 22932 22931 0 -1 0 32580 0 0 0 112918 97 0 0 25 0 1 0 491506352 136802304 32104 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33399 32104 603 41 0 33358 0
vsize: 133596
[startup+1140.03 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 24059
Raw data (stat): 24059 (minisat+) R 24058 22932 22931 0 -1 0 32765 0 0 0 113918 97 0 0 25 0 1 0 491506352 137613312 32289 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33597 32289 603 41 0 33556 0
vsize: 134388
[startup+1150.03 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 24059
Raw data (stat): 24059 (minisat+) R 24058 22932 22931 0 -1 0 32949 0 0 0 114918 98 0 0 25 0 1 0 491506352 138285056 32473 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33761 32473 603 41 0 33720 0
vsize: 135044
[startup+1160.03 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 24059
Raw data (stat): 24059 (minisat+) R 24058 22932 22931 0 -1 0 33146 0 0 0 115916 99 0 0 25 0 1 0 491506352 139091968 32670 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33958 32670 603 41 0 33917 0
vsize: 135832
[startup+1170.04 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 24059
Raw data (stat): 24059 (minisat+) R 24058 22932 22931 0 -1 0 33336 0 0 0 116917 100 0 0 25 0 1 0 491506352 139902976 32860 4294967295 134512640 134672761 3221224544 3221223680 134560706 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 34156 32860 603 41 0 34115 0
vsize: 136624
[startup+1180.04 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 24059
Raw data (stat): 24059 (minisat+) R 24058 22932 22931 0 -1 0 33555 0 0 0 117915 101 0 0 25 0 1 0 491506352 140849152 33079 4294967295 134512640 134672761 3221224544 3221223712 134561207 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 34387 33079 603 41 0 34346 0
vsize: 137548
[startup+1190.04 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 24059
Raw data (stat): 24059 (minisat+) R 24058 22932 22931 0 -1 0 33760 0 0 0 118915 102 0 0 25 0 1 0 491506352 141656064 33284 4294967295 134512640 134672761 3221224544 3221223744 134557895 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 34584 33284 603 41 0 34543 0
vsize: 138336
[startup+1200.04 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 24059
Raw data (stat): 24059 (minisat+) R 24058 22932 22931 0 -1 0 34027 0 0 0 119915 102 0 0 25 0 1 0 491506352 142737408 33551 4294967295 134512640 134672761 3221224544 3221223728 134558662 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 34848 33551 603 41 0 34807 0
vsize: 139392
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.1 s]
Raw data (loadavg): 0.99 0.97 0.93 1/54 24059
Raw data (stat): 24059 (minisat+) Z 24058 22932 22931 0 -1 12 34029 0 0 0 119915 109 0 0 25 0 1 0 491506352 0 0 4294967295 0 0 0 0 0 0 16384 5 16386 3222412051 0 0 17 1 0 0
Raw data (statm): 0 0 0 0 0 0 0
vsize: 0
Maximum CPU time exceeded: sending SIGTERM and SIGKILL

Child status: 0
Real time (s): 1200.1
CPU time (s): 1200.25
CPU user time (s): 1199.15
CPU system time (s): 1.09183
CPU usage (%): 100.012
Max. virtual memory (Kb): 139392
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####