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 16853

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

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.053
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:        486012 kB
Buffers:          1004 kB
Cached:         521984 kB
SwapCached:          0 kB
Active:          19984 kB
Inactive:       506128 kB
HighTotal:      131008 kB
HighFree:        15428 kB
LowTotal:       903652 kB
LowFree:        470584 kB
SwapTotal:     2097136 kB
SwapFree:      2096968 kB
Dirty:              60 kB
Writeback:           0 kB
Mapped:           7220 kB
Slab:            16728 kB
Committed_AS:    92820 kB
PageTables:        344 kB
VmallocTotal:   114680 kB
VmallocUsed:      1388 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-21 09:03:35 (client local time) WITH STATUS 0 IN 1200.31 SECONDS
stats: 12426 7 1200.31 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 =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |         0 |  639324  2238724 |  191797       0        0     nan |  0.000 % |
c   -- subsuming                       
c   -- var.elim.:  1000/116850          
c   -- var.elim.:  2000/116850          
c   -- var.elim.:  3000/116850          
c   -- var.elim.:  4000/116850          
c   -- var.elim.:  5000/116850          
c   -- var.elim.:  6000/116850          
c   -- var.elim.:  7000/116850          
c   -- var.elim.:  8000/116850          
c   -- var.elim.:  9000/116850          
c   -- var.elim.:  10000/116850          
c   -- var.elim.:  11000/116850          
c   -- var.elim.:  12000/116850          
c   -- var.elim.:  13000/116850          
c   -- var.elim.:  14000/116850          
c   -- var.elim.:  15000/116850          
c   -- var.elim.:  16000/116850          
c   -- var.elim.:  17000/116850          
c   -- var.elim.:  18000/116850          
c   -- var.elim.:  19000/116850          
c   -- var.elim.:  20000/116850          
c   -- var.elim.:  21000/116850          
c   -- var.elim.:  22000/116850          
c   -- var.elim.:  23000/116850          
c   -- var.elim.:  24000/116850          
c   -- var.elim.:  25000/116850          
c   -- var.elim.:  26000/116850          
c   -- var.elim.:  27000/116850          
c   -- var.elim.:  28000/116850          
c   -- var.elim.:  29000/116850          
c   -- var.elim.:  30000/116850          
c   -- var.elim.:  31000/116850          
c   -- var.elim.:  32000/116850          
c   -- var.elim.:  33000/116850          
c   -- var.elim.:  34000/116850          
c   -- var.elim.:  35000/116850          
c   -- var.elim.:  36000/116850          
c   -- var.elim.:  37000/116850          
c   -- var.elim.:  38000/116850          
c   -- var.elim.:  39000/116850          
c   -- var.elim.:  40000/116850          
c   -- var.elim.:  41000/116850          
c   -- var.elim.:  42000/116850          
c   -- var.elim.:  43000/116850          
c   -- var.elim.:  44000/116850          
c   -- var.elim.:  45000/116850          
c   -- var.elim.:  46000/116850          
c   -- var.elim.:  47000/116850          
c   -- var.elim.:  48000/116850          
c   -- var.elim.:  49000/116850          
c   -- var.elim.:  50000/116850          
c   -- var.elim.:  51000/116850          
c   -- var.elim.:  52000/116850          
c   -- var.elim.:  53000/116850          
c   -- var.elim.:  54000/116850          
c   -- var.elim.:  55000/116850          
c   -- var.elim.:  56000/116850          
c   -- var.elim.:  57000/116850          
c   -- var.elim.:  58000/116850          
c   -- var.elim.:  59000/116850          
c   -- var.elim.:  60000/116850          
c   -- var.elim.:  61000/116850          
c   -- var.elim.:  62000/116850          
c   -- var.elim.:  63000/116850          
c   -- var.elim.:  64000/116850          
c   -- var.elim.:  65000/116850          
c   -- var.elim.:  66000/116850          
c   -- var.elim.:  67000/116850          
c   -- var.elim.:  68000/116850          
c   -- var.elim.:  69000/116850          
c   -- var.elim.:  70000/116850          
c   -- var.elim.:  71000/116850          
c   -- var.elim.:  72000/116850          
c   -- var.elim.:  73000/116850          
c   -- var.elim.:  74000/116850          
c   -- var.elim.:  75000/116850          
c   -- var.elim.:  76000/116850          
c   -- var.elim.:  77000/116850          
c   -- var.elim.:  78000/116850          
c   -- var.elim.:  79000/116850          
c   -- var.elim.:  80000/116850          
c   -- var.elim.:  81000/116850          
c   -- var.elim.:  82000/116850          
c   -- var.elim.:  83000/116850          
c   -- var.elim.:  84000/116850          
c   -- var.elim.:  85000/116850          
c   -- var.elim.:  86000/116850          
c   -- var.elim.:  87000/116850          
c   -- var.elim.:  88000/116850          
c   -- var.elim.:  89000/116850          
c   -- var.elim.:  90000/116850          
c   -- var.elim.:  91000/116850          
c   -- var.elim.:  92000/116850          
c   -- var.elim.:  93000/116850          
c   -- var.elim.:  94000/116850          
c   -- var.elim.:  95000/116850          
c   -- var.elim.:  96000/116850          
c   -- var.elim.:  97000/116850          
c   -- var.elim.:  98000/116850          
c   -- var.elim.:  99000/116850          
c   -- var.elim.:  100000/116850          
c   -- var.elim.:  101000/116850          
c   -- var.elim.:  102000/116850          
c   -- var.elim.:  103000/116850          
c   -- var.elim.:  104000/116850          
c   -- var.elim.:  105000/116850          
c   -- var.elim.:  106000/116850          
c   -- var.elim.:  107000/116850          
c   -- var.elim.:  108000/116850          
c   -- var.elim.:  109000/116850          
c   -- var.elim.:  110000/116850          
c   -- var.elim.:  111000/116850          
c   -- var.elim.:  112000/116850          
c   -- var.elim.:  113000/116850          
c   -- var.elim.:  114000/116850          
c   -- var.elim.:  115000/116850          
c   -- var.elim.:  116000/116850          
c   -- var.elim.:  116850/116850          
c   -- var.elim.:  1000/11288          
c   -- var.elim.:  2000/11288          
#### 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.84 0.94 0.90 2/56 25538
Raw data (stat): 25538 (runsolver) R 25537 12452 12451 0 -1 64 4 0 0 0 0 0 0 0 20 0 1 0 428655124 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.0008 s]
Raw data (loadavg): 0.87 0.94 0.90 2/56 25538
Raw data (stat): 25538 (minisat+) R 25537 12452 12451 0 -1 0 21845 0 0 0 945 54 0 0 25 0 1 0 428655124 97255424 21325 4294967295 134512640 134672761 3221224544 3221223088 134621401 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23744 21325 603 41 0 23703 0
vsize: 94976
[startup+20.0017 s]
Raw data (loadavg): 0.89 0.94 0.90 2/56 25538
Raw data (stat): 25538 (minisat+) R 25537 12452 12451 0 -1 0 26182 0 0 0 1932 66 0 0 25 0 1 0 428655124 99708928 21935 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24343 21935 603 41 0 24302 0
vsize: 97372
[startup+30.0014 s]
Raw data (loadavg): 0.90 0.94 0.90 2/56 25538
Raw data (stat): 25538 (minisat+) R 25537 12452 12451 0 -1 0 27426 0 0 0 2928 70 0 0 25 0 1 0 428655124 104865792 23179 4294967295 134512640 134672761 3221224544 3221223744 134610697 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25602 23179 603 41 0 25561 0
vsize: 102408
[startup+40.0017 s]
Raw data (loadavg): 0.92 0.94 0.90 2/56 25538
Raw data (stat): 25538 (minisat+) R 25537 12452 12451 0 -1 0 28442 0 0 0 3925 74 0 0 25 0 1 0 428655124 109105152 24195 4294967295 134512640 134672761 3221224544 3221223728 134615652 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26637 24195 603 41 0 26596 0
vsize: 106548
[startup+50.002 s]
Raw data (loadavg): 0.93 0.94 0.90 2/56 25538
Raw data (stat): 25538 (minisat+) R 25537 12452 12451 0 -1 0 29214 0 0 0 4923 76 0 0 25 0 1 0 428655124 112279552 24967 4294967295 134512640 134672761 3221224544 3221223728 134615652 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27412 24967 603 41 0 27371 0
vsize: 109648
[startup+60.0028 s]
Raw data (loadavg): 0.94 0.95 0.90 2/56 25538
Raw data (stat): 25538 (minisat+) R 25537 12452 12451 0 -1 0 30032 0 0 0 5921 78 0 0 25 0 1 0 428655124 115605504 25785 4294967295 134512640 134672761 3221224544 3221223728 134615833 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28224 25785 603 41 0 28183 0
vsize: 112896
[startup+70.0036 s]
Raw data (loadavg): 0.95 0.95 0.91 2/56 25538
Raw data (stat): 25538 (minisat+) R 25537 12452 12451 0 -1 0 30755 0 0 0 6918 81 0 0 25 0 1 0 428655124 118525952 26508 4294967295 134512640 134672761 3221224544 3221223728 134615693 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28937 26508 603 41 0 28896 0
vsize: 115748
[startup+80.0033 s]
Raw data (loadavg): 0.96 0.95 0.91 2/56 25538
Raw data (stat): 25538 (minisat+) R 25537 12452 12451 0 -1 0 31621 0 0 0 7916 83 0 0 25 0 1 0 428655124 122253312 27374 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29847 27374 603 41 0 29806 0
vsize: 119388
[startup+90.0032 s]
Raw data (loadavg): 0.96 0.95 0.91 2/56 25540
Raw data (stat): 25538 (minisat+) R 25537 12452 12451 0 -1 0 32226 0 0 0 8913 86 0 0 25 0 1 0 428655124 124768256 27979 4294967295 134512640 134672761 3221224544 3221223728 134615627 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30461 27979 603 41 0 30420 0
vsize: 121844
[startup+100.003 s]
Raw data (loadavg): 0.97 0.95 0.91 2/56 25540
Raw data (stat): 25538 (minisat+) R 25537 12452 12451 0 -1 0 32770 0 0 0 9912 88 0 0 25 0 1 0 428655124 127021056 28523 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31011 28523 603 41 0 30970 0
vsize: 124044
[startup+110.004 s]
Raw data (loadavg): 0.97 0.95 0.91 2/56 25540
Raw data (stat): 25538 (minisat+) R 25537 12452 12451 0 -1 0 33376 0 0 0 10910 89 0 0 25 0 1 0 428655124 129413120 29129 4294967295 134512640 134672761 3221224544 3221223728 134615940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31595 29129 603 41 0 31554 0
vsize: 126380
[startup+120.005 s]
Raw data (loadavg): 0.98 0.95 0.91 2/56 25540
Raw data (stat): 25538 (minisat+) R 25537 12452 12451 0 -1 0 34131 0 0 0 11907 93 0 0 25 0 1 0 428655124 132493312 29884 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32347 29884 603 41 0 32306 0
vsize: 129388
[startup+130.004 s]
Raw data (loadavg): 0.98 0.95 0.91 2/56 25540
Raw data (stat): 25538 (minisat+) R 25537 12452 12451 0 -1 0 34506 0 0 0 12906 94 0 0 25 0 1 0 428655124 134082560 30259 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32735 30259 603 41 0 32694 0
vsize: 130940
[startup+140.004 s]
Raw data (loadavg): 0.98 0.95 0.91 2/56 25540
Raw data (stat): 25538 (minisat+) R 25537 12452 12451 0 -1 0 34889 0 0 0 13905 95 0 0 25 0 1 0 428655124 135675904 30642 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33124 30642 603 41 0 33083 0
vsize: 132496
[startup+150.004 s]
Raw data (loadavg): 0.98 0.95 0.91 2/56 25540
Raw data (stat): 25538 (minisat+) R 25537 12452 12451 0 -1 0 35252 0 0 0 14905 96 0 0 25 0 1 0 428655124 137142272 31005 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33482 31005 603 41 0 33441 0
vsize: 133928
[startup+160.004 s]
Raw data (loadavg): 0.99 0.96 0.91 2/56 25540
Raw data (stat): 25538 (minisat+) R 25537 12452 12451 0 -1 0 35569 0 0 0 15904 97 0 0 25 0 1 0 428655124 138350592 31322 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33777 31322 603 41 0 33736 0
vsize: 135108
[startup+170.003 s]
Raw data (loadavg): 0.99 0.96 0.91 2/56 25540
Raw data (stat): 25538 (minisat+) R 25537 12452 12451 0 -1 0 35846 0 0 0 16903 98 0 0 25 0 1 0 428655124 139550720 31599 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 34070 31599 603 41 0 34029 0
vsize: 136280
[startup+180.003 s]
Raw data (loadavg): 0.99 0.96 0.91 2/56 25540
Raw data (stat): 25538 (minisat+) R 25537 12452 12451 0 -1 0 36144 0 0 0 17901 99 0 0 25 0 1 0 428655124 140746752 31897 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 34362 31897 603 41 0 34321 0
vsize: 137448
[startup+190.004 s]
Raw data (loadavg): 0.99 0.96 0.91 2/56 25540
Raw data (stat): 25538 (minisat+) R 25537 12452 12451 0 -1 0 36435 0 0 0 18901 100 0 0 25 0 1 0 428655124 141930496 32188 4294967295 134512640 134672761 3221224544 3221223728 134615919 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 34651 32188 603 41 0 34610 0
vsize: 138604
[startup+200.004 s]
Raw data (loadavg): 0.99 0.96 0.91 2/56 25540
Raw data (stat): 25538 (minisat+) R 25537 12452 12451 0 -1 0 36745 0 0 0 19900 102 0 0 25 0 1 0 428655124 143257600 32498 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 34975 32498 603 41 0 34934 0
vsize: 139900
[startup+210.003 s]
Raw data (loadavg): 0.99 0.96 0.91 2/56 25540
Raw data (stat): 25538 (minisat+) R 25537 12452 12451 0 -1 0 36993 0 0 0 20899 102 0 0 25 0 1 0 428655124 144211968 32746 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 35208 32746 603 41 0 35167 0
vsize: 140832
[startup+220.004 s]
Raw data (loadavg): 0.99 0.96 0.91 2/56 25540
Raw data (stat): 25538 (minisat+) R 25537 12452 12451 0 -1 0 37247 0 0 0 21898 103 0 0 25 0 1 0 428655124 145264640 33000 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 35465 33000 603 41 0 35424 0
vsize: 141860
[startup+230.003 s]
Raw data (loadavg): 0.99 0.96 0.91 2/56 25540
Raw data (stat): 25538 (minisat+) R 25537 12452 12451 0 -1 0 37509 0 0 0 22897 104 0 0 25 0 1 0 428655124 146313216 33262 4294967295 134512640 134672761 3221224544 3221223728 134615758 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 35721 33262 603 41 0 35680 0
vsize: 142884
[startup+240.003 s]
Raw data (loadavg): 0.99 0.96 0.91 2/56 25540
Raw data (stat): 25538 (minisat+) R 25537 12452 12451 0 -1 0 37741 0 0 0 23897 105 0 0 25 0 1 0 428655124 147234816 33494 4294967295 134512640 134672761 3221224544 3221223728 134615755 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 35946 33494 603 41 0 35905 0
vsize: 143784
[startup+250.003 s]
Raw data (loadavg): 0.99 0.96 0.91 2/56 25540
Raw data (stat): 25538 (minisat+) R 25537 12452 12451 0 -1 0 38575 0 0 0 24896 106 0 0 25 0 1 0 428655124 151220224 34328 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 36919 34328 603 41 0 36878 0
vsize: 147676
[startup+260.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 25540
Raw data (stat): 25538 (minisat+) R 25537 12452 12451 0 -1 0 39460 0 0 0 25893 109 0 0 25 0 1 0 428655124 154791936 35213 4294967295 134512640 134672761 3221224544 3221223728 134615916 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 37791 35213 603 41 0 37750 0
vsize: 151164
[startup+270.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 25540
Raw data (stat): 25538 (minisat+) R 25537 12452 12451 0 -1 0 40172 0 0 0 26891 111 0 0 25 0 1 0 428655124 157708288 35925 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 38503 35925 603 41 0 38462 0
vsize: 154012
[startup+280.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 25540
Raw data (stat): 25538 (minisat+) R 25537 12452 12451 0 -1 0 40720 0 0 0 27890 112 0 0 25 0 1 0 428655124 159981568 36473 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 39058 36473 603 41 0 39017 0
vsize: 156232
[startup+290.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 25540
Raw data (stat): 25538 (minisat+) R 25537 12452 12451 0 -1 0 41241 0 0 0 28890 113 0 0 25 0 1 0 428655124 162103296 36994 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 39576 36994 603 41 0 39535 0
vsize: 158304
[startup+300.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 25540
Raw data (stat): 25538 (minisat+) R 25537 12452 12451 0 -1 0 41643 0 0 0 29889 114 0 0 25 0 1 0 428655124 163758080 37396 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 39980 37396 603 41 0 39939 0
vsize: 159920
[startup+310.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 25540
Raw data (stat): 25538 (minisat+) R 25537 12452 12451 0 -1 0 42130 0 0 0 30888 115 0 0 25 0 1 0 428655124 165658624 37883 4294967295 134512640 134672761 3221224544 3221223728 134615747 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 40444 37883 603 41 0 40403 0
vsize: 161776
[startup+320.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 25540
Raw data (stat): 25538 (minisat+) R 25537 12452 12451 0 -1 0 42583 0 0 0 31887 116 0 0 25 0 1 0 428655124 167518208 38336 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 40898 38336 603 41 0 40857 0
vsize: 163592
[startup+330.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 25540
Raw data (stat): 25538 (minisat+) R 25537 12452 12451 0 -1 0 42968 0 0 0 32886 117 0 0 25 0 1 0 428655124 169222144 38721 4294967295 134512640 134672761 3221224544 3221223584 134603490 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 41314 38721 603 41 0 41273 0
vsize: 165256
[startup+340.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 25540
Raw data (stat): 25538 (minisat+) R 25537 12452 12451 0 -1 0 43267 0 0 0 33885 118 0 0 25 0 1 0 428655124 170430464 39020 4294967295 134512640 134672761 3221224544 3221223728 134615720 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 41609 39020 603 41 0 41568 0
vsize: 166436
[startup+350.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 25540
Raw data (stat): 25538 (minisat+) R 25537 12452 12451 0 -1 0 43546 0 0 0 34885 118 0 0 25 0 1 0 428655124 171495424 39299 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 41869 39299 603 41 0 41828 0
vsize: 167476
[startup+360.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 25540
Raw data (stat): 25538 (minisat+) R 25537 12452 12451 0 -1 0 44005 0 0 0 35884 119 0 0 25 0 1 0 428655124 173367296 39758 4294967295 134512640 134672761 3221224544 3221223584 134612783 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 42326 39758 603 41 0 42285 0
vsize: 169304
[startup+370.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 25540
Raw data (stat): 25538 (minisat+) R 25537 12452 12451 0 -1 0 44321 0 0 0 36883 121 0 0 25 0 1 0 428655124 174706688 40074 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 42653 40074 603 41 0 42612 0
vsize: 170612
[startup+380.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 25540
Raw data (stat): 25538 (minisat+) R 25537 12452 12451 0 -1 0 44580 0 0 0 37882 122 0 0 25 0 1 0 428655124 175763456 40333 4294967295 134512640 134672761 3221224544 3221223728 134615830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 42911 40333 603 41 0 42870 0
vsize: 171644
[startup+390.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 25542
Raw data (stat): 25538 (minisat+) R 25537 12452 12451 0 -1 0 44803 0 0 0 38882 122 0 0 25 0 1 0 428655124 176697344 40556 4294967295 134512640 134672761 3221224544 3221223728 134615579 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 43139 40556 603 41 0 43098 0
vsize: 172556
[startup+400.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 25542
Raw data (stat): 25538 (minisat+) R 25537 12452 12451 0 -1 0 45254 0 0 0 39881 124 0 0 25 0 1 0 428655124 178552832 41007 4294967295 134512640 134672761 3221224544 3221223356 1075350517 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 43592 41007 603 41 0 43551 0
vsize: 174368
[startup+410.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 25542
Raw data (stat): 25538 (minisat+) R 25537 12452 12451 0 -1 0 45820 0 0 0 40879 125 0 0 25 0 1 0 428655124 180805632 41573 4294967295 134512640 134672761 3221224544 3221223584 134612587 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 44142 41573 603 41 0 44101 0
vsize: 176568
[startup+420.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 25542
Raw data (stat): 25538 (minisat+) R 25537 12452 12451 0 -1 0 46261 0 0 0 41878 127 0 0 25 0 1 0 428655124 182657024 42014 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 44594 42014 603 41 0 44553 0
vsize: 178376
[startup+430.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 25542
Raw data (stat): 25538 (minisat+) R 25537 12452 12451 0 -1 0 46702 0 0 0 42877 128 0 0 25 0 1 0 428655124 184385536 42455 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 45016 42455 603 41 0 44975 0
vsize: 180064
[startup+440.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 25542
Raw data (stat): 25538 (minisat+) R 25537 12452 12451 0 -1 0 47156 0 0 0 43876 129 0 0 25 0 1 0 428655124 186241024 42909 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 45469 42909 603 41 0 45428 0
vsize: 181876
[startup+450.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 25542
Raw data (stat): 25538 (minisat+) R 25537 12452 12451 0 -1 0 47455 0 0 0 44874 131 0 0 25 0 1 0 428655124 187555840 43208 4294967295 134512640 134672761 3221224544 3221223696 134565103 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 45790 43208 603 41 0 45749 0
vsize: 183160
[startup+460.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 25542
Raw data (stat): 25538 (minisat+) R 25537 12452 12451 0 -1 0 47872 0 0 0 45873 132 0 0 25 0 1 0 428655124 189411328 43625 4294967295 134512640 134672761 3221224544 3221223680 134614736 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 46243 43625 603 41 0 46202 0
vsize: 184972
[startup+470.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 25542
Raw data (stat): 25538 (minisat+) R 25537 12452 12451 0 -1 0 48222 0 0 0 46873 133 0 0 25 0 1 0 428655124 190836736 43975 4294967295 134512640 134672761 3221224544 3221223728 134615549 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 46591 43975 603 41 0 46550 0
vsize: 186364
[startup+480.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 25542
Raw data (stat): 25538 (minisat+) R 25537 12452 12451 0 -1 0 48917 0 0 0 47870 135 0 0 25 0 1 0 428655124 193589248 44670 4294967295 134512640 134672761 3221224544 3221223728 134615916 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 47263 44670 603 41 0 47222 0
vsize: 189052
[startup+490.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 25542
Raw data (stat): 25538 (minisat+) R 25537 12452 12451 0 -1 0 49442 0 0 0 48869 137 0 0 25 0 1 0 428655124 195788800 45195 4294967295 134512640 134672761 3221224544 3221223688 134616156 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 47800 45195 603 41 0 47759 0
vsize: 191200
[startup+500.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 25542
Raw data (stat): 25538 (minisat+) R 25537 12452 12451 0 -1 0 49566 0 0 0 49869 137 0 0 25 0 1 0 428655124 196321280 45319 4294967295 134512640 134672761 3221224544 3221223728 134615703 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 47930 45319 603 41 0 47889 0
vsize: 191720
[startup+510.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 25542
Raw data (stat): 25538 (minisat+) R 25537 12452 12451 0 -1 0 49769 0 0 0 50869 137 0 0 25 0 1 0 428655124 197107712 45522 4294967295 134512640 134672761 3221224544 3221223728 134615571 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 48122 45522 603 41 0 48081 0
vsize: 192488
[startup+520.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 25542
Raw data (stat): 25538 (minisat+) R 25537 12452 12451 0 -1 0 50097 0 0 0 51868 139 0 0 25 0 1 0 428655124 198414336 45850 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 48441 45850 603 41 0 48400 0
vsize: 193764
[startup+530.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 25542
Raw data (stat): 25538 (minisat+) R 25537 12452 12451 0 -1 0 50335 0 0 0 52867 139 0 0 25 0 1 0 428655124 199471104 46088 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 48699 46088 603 41 0 48658 0
vsize: 194796
[startup+540.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 25542
Raw data (stat): 25538 (minisat+) R 25537 12452 12451 0 -1 0 50547 0 0 0 53867 140 0 0 25 0 1 0 428655124 200261632 46300 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 48892 46300 603 41 0 48851 0
vsize: 195568
[startup+550.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 25542
Raw data (stat): 25538 (minisat+) R 25537 12452 12451 0 -1 0 50751 0 0 0 54866 140 0 0 25 0 1 0 428655124 201195520 46504 4294967295 134512640 134672761 3221224544 3221223744 134610707 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 49120 46504 603 41 0 49079 0
vsize: 196480
[startup+560.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 25542
Raw data (stat): 25538 (minisat+) R 25537 12452 12451 0 -1 0 51169 0 0 0 55866 141 0 0 25 0 1 0 428655124 202792960 46922 4294967295 134512640 134672761 3221224544 3221223744 134610652 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 49510 46922 603 41 0 49469 0
vsize: 198040
[startup+570.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 25542
Raw data (stat): 25538 (minisat+) R 25537 12452 12451 0 -1 0 51678 0 0 0 56864 143 0 0 25 0 1 0 428655124 204902400 47431 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 50025 47431 603 41 0 49984 0
vsize: 200100
[startup+580.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 25542
Raw data (stat): 25538 (minisat+) R 25537 12452 12451 0 -1 0 52168 0 0 0 57864 144 0 0 25 0 1 0 428655124 206880768 47921 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 50508 47921 603 41 0 50467 0
vsize: 202032
[startup+590.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 25542
Raw data (stat): 25538 (minisat+) R 25537 12452 12451 0 -1 0 52657 0 0 0 58862 145 0 0 25 0 1 0 428655124 208986112 48410 4294967295 134512640 134672761 3221224544 3221223680 134614701 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 51022 48410 603 41 0 50981 0
vsize: 204088
[startup+600.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 25542
Raw data (stat): 25538 (minisat+) R 25537 12452 12451 0 -1 0 53026 0 0 0 59862 146 0 0 25 0 1 0 428655124 210448384 48779 4294967295 134512640 134672761 3221224544 3221223680 134614685 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 51379 48779 603 41 0 51338 0
vsize: 205516
[startup+610.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 25542
Raw data (stat): 25538 (minisat+) R 25537 12452 12451 0 -1 0 53559 0 0 0 60861 147 0 0 25 0 1 0 428655124 212692992 49312 4294967295 134512640 134672761 3221224544 3221223728 134615833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 51927 49312 603 41 0 51886 0
vsize: 207708
[startup+620.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 25542
Raw data (stat): 25538 (minisat+) R 25537 12452 12451 0 -1 0 54009 0 0 0 61860 148 0 0 25 0 1 0 428655124 214425600 49762 4294967295 134512640 134672761 3221224544 3221223728 134615549 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 52350 49762 603 41 0 52309 0
vsize: 209400
[startup+630.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 25542
Raw data (stat): 25538 (minisat+) R 25537 12452 12451 0 -1 0 54444 0 0 0 62859 149 0 0 25 0 1 0 428655124 216264704 50197 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 52799 50197 603 41 0 52758 0
vsize: 211196
[startup+640.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 25542
Raw data (stat): 25538 (minisat+) R 25537 12452 12451 0 -1 0 54897 0 0 0 63858 150 0 0 25 0 1 0 428655124 218112000 50650 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 53250 50650 603 41 0 53209 0
vsize: 213000
[startup+650.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 25542
Raw data (stat): 25538 (minisat+) R 25537 12452 12451 0 -1 0 55409 0 0 0 64858 151 0 0 25 0 1 0 428655124 220205056 51162 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 53761 51162 603 41 0 53720 0
vsize: 215044
[startup+660.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 25542
Raw data (stat): 25538 (minisat+) R 25537 12452 12451 0 -1 0 55912 0 0 0 65856 153 0 0 25 0 1 0 428655124 222322688 51665 4294967295 134512640 134672761 3221224544 3221223584 134612987 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 54278 51666 603 41 0 54237 0
vsize: 217112
[startup+670.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 25542
Raw data (stat): 25538 (minisat+) R 25537 12452 12451 0 -1 0 56420 0 0 0 66856 153 0 0 25 0 1 0 428655124 224305152 52173 4294967295 134512640 134672761 3221224544 3221223744 134610707 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 54762 52173 603 41 0 54721 0
vsize: 219048
[startup+680.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 25542
Raw data (stat): 25538 (minisat+) R 25537 12452 12451 0 -1 0 56858 0 0 0 67855 155 0 0 25 0 1 0 428655124 226119680 52611 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 55205 52611 603 41 0 55164 0
vsize: 220820
[startup+690.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 25544
Raw data (stat): 25538 (minisat+) R 25537 12452 12451 0 -1 0 57017 0 0 0 68854 155 0 0 25 0 1 0 428655124 226775040 52770 4294967295 134512640 134672761 3221224544 3221223728 134615828 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 55365 52770 603 41 0 55324 0
vsize: 221460
[startup+700.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 25544
Raw data (stat): 25538 (minisat+) R 25537 12452 12451 0 -1 0 57275 0 0 0 69854 156 0 0 25 0 1 0 428655124 227844096 53028 4294967295 134512640 134672761 3221224544 3221223728 134615549 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 55626 53028 603 41 0 55585 0
vsize: 222504
[startup+710.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 25544
Raw data (stat): 25538 (minisat+) R 25537 12452 12451 0 -1 0 57522 0 0 0 70853 157 0 0 25 0 1 0 428655124 228900864 53275 4294967295 134512640 134672761 3221224544 3221223744 134610686 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 55884 53275 603 41 0 55843 0
vsize: 223536
[startup+720.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 25544
Raw data (stat): 25538 (minisat+) R 25537 12452 12451 0 -1 0 57849 0 0 0 71852 158 0 0 25 0 1 0 428655124 230227968 53602 4294967295 134512640 134672761 3221224544 3221223584 134613791 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 56208 53602 603 41 0 56167 0
vsize: 224832
[startup+730.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 25544
Raw data (stat): 25538 (minisat+) R 25537 12452 12451 0 -1 0 58334 0 0 0 72852 159 0 0 25 0 1 0 428655124 232206336 54087 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 56691 54087 603 41 0 56650 0
vsize: 226764
[startup+740.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 25544
Raw data (stat): 25538 (minisat+) R 25537 12452 12451 0 -1 0 58864 0 0 0 73850 160 0 0 25 0 1 0 428655124 234328064 54617 4294967295 134512640 134672761 3221224544 3221223744 134610686 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 57209 54617 603 41 0 57168 0
vsize: 228836
[startup+750.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 25544
Raw data (stat): 25538 (minisat+) R 25537 12452 12451 0 -1 0 59394 0 0 0 74849 161 0 0 25 0 1 0 428655124 236437504 55147 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 57724 55147 603 41 0 57683 0
vsize: 230896
[startup+760.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 25544
Raw data (stat): 25538 (minisat+) R 25537 12452 12451 0 -1 0 59897 0 0 0 75848 163 0 0 25 0 1 0 428655124 238534656 55650 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 58236 55650 603 41 0 58195 0
vsize: 232944
[startup+770.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 25544
Raw data (stat): 25538 (minisat+) R 25537 12452 12451 0 -1 0 60378 0 0 0 76847 164 0 0 25 0 1 0 428655124 240533504 56131 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 58724 56131 603 41 0 58683 0
vsize: 234896
[startup+780.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 25544
Raw data (stat): 25538 (minisat+) R 25537 12452 12451 0 -1 0 60885 0 0 0 77846 165 0 0 25 0 1 0 428655124 242651136 56638 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 59241 56638 603 41 0 59200 0
vsize: 236964
[startup+790.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 25544
Raw data (stat): 25538 (minisat+) R 25537 12452 12451 0 -1 0 61423 0 0 0 78845 167 0 0 25 0 1 0 428655124 244789248 57176 4294967295 134512640 134672761 3221224544 3221223728 134615736 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 59763 57176 603 41 0 59722 0
vsize: 239052
[startup+800.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 25544
Raw data (stat): 25538 (minisat+) R 25537 12452 12451 0 -1 0 62000 0 0 0 79843 168 0 0 25 0 1 0 428655124 247132160 57753 4294967295 134512640 134672761 3221224544 3221223744 134610707 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 60335 57753 603 41 0 60294 0
vsize: 241340
[startup+810.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 25544
Raw data (stat): 25538 (minisat+) R 25537 12452 12451 0 -1 0 62412 0 0 0 80842 169 0 0 25 0 1 0 428655124 248864768 58165 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 60758 58165 603 41 0 60717 0
vsize: 243032
[startup+820.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 25544
Raw data (stat): 25538 (minisat+) R 25537 12452 12451 0 -1 0 62898 0 0 0 81841 170 0 0 25 0 1 0 428655124 250822656 58651 4294967295 134512640 134672761 3221224544 3221223728 134615720 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 61236 58651 603 41 0 61195 0
vsize: 244944
[startup+830.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 25544
Raw data (stat): 25538 (minisat+) R 25537 12452 12451 0 -1 0 63482 0 0 0 82840 171 0 0 25 0 1 0 428655124 253198336 59235 4294967295 134512640 134672761 3221224544 3221223744 134610707 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 61816 59235 603 41 0 61775 0
vsize: 247264
[startup+840.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 25544
Raw data (stat): 25538 (minisat+) R 25537 12452 12451 0 -1 0 64047 0 0 0 83839 173 0 0 25 0 1 0 428655124 255590400 59800 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 62400 59800 603 41 0 62359 0
vsize: 249600
[startup+850.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 25544
Raw data (stat): 25538 (minisat+) R 25537 12452 12451 0 -1 0 64501 0 0 0 84839 174 0 0 25 0 1 0 428655124 257417216 60254 4294967295 134512640 134672761 3221224544 3221223728 134615665 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 62846 60254 603 41 0 62805 0
vsize: 251384
[startup+860.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 25544
Raw data (stat): 25538 (minisat+) R 25537 12452 12451 0 -1 0 64951 0 0 0 85838 175 0 0 25 0 1 0 428655124 259248128 60704 4294967295 134512640 134672761 3221224544 3221223728 134615549 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 63293 60704 603 41 0 63252 0
vsize: 253172
[startup+870.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 25544
Raw data (stat): 25538 (minisat+) R 25537 12452 12451 0 -1 0 65411 0 0 0 86836 176 0 0 25 0 1 0 428655124 261095424 61164 4294967295 134512640 134672761 3221224544 3221223744 134610707 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 63744 61164 603 41 0 63703 0
vsize: 254976
[startup+880.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 25544
Raw data (stat): 25538 (minisat+) R 25537 12452 12451 0 -1 0 65985 0 0 0 87836 177 0 0 25 0 1 0 428655124 263467008 61738 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 64323 61738 603 41 0 64282 0
vsize: 257292
[startup+890.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 25544
Raw data (stat): 25538 (minisat+) R 25537 12452 12451 0 -1 0 66548 0 0 0 88834 178 0 0 25 0 1 0 428655124 265846784 62301 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 64904 62301 603 41 0 64863 0
vsize: 259616
[startup+900.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 25544
Raw data (stat): 25538 (minisat+) R 25537 12452 12451 0 -1 0 66948 0 0 0 89834 179 0 0 25 0 1 0 428655124 267427840 62701 4294967295 134512640 134672761 3221224544 3221223744 134610707 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 65290 62701 603 41 0 65249 0
vsize: 261160
[startup+910.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 25544
Raw data (stat): 25538 (minisat+) R 25537 12452 12451 0 -1 0 67283 0 0 0 90833 180 0 0 25 0 1 0 428655124 268750848 63036 4294967295 134512640 134672761 3221224544 3221223728 134615703 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 65613 63036 603 41 0 65572 0
vsize: 262452
[startup+920.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 25544
Raw data (stat): 25538 (minisat+) R 25537 12452 12451 0 -1 0 67465 0 0 0 91832 181 0 0 25 0 1 0 428655124 269549568 63218 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 65808 63218 603 41 0 65767 0
vsize: 263232
[startup+930.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 25544
Raw data (stat): 25538 (minisat+) R 25537 12452 12451 0 -1 0 67749 0 0 0 92832 182 0 0 25 0 1 0 428655124 270733312 63502 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 66097 63502 603 41 0 66056 0
vsize: 264388
[startup+940.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 25544
Raw data (stat): 25538 (minisat+) R 25537 12452 12451 0 -1 0 68194 0 0 0 93831 183 0 0 25 0 1 0 428655124 272572416 63947 4294967295 134512640 134672761 3221224544 3221223728 134615835 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 66546 63947 603 41 0 66505 0
vsize: 266184
[startup+950.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 25544
Raw data (stat): 25538 (minisat+) R 25537 12452 12451 0 -1 0 68458 0 0 0 94830 184 0 0 25 0 1 0 428655124 273629184 64211 4294967295 134512640 134672761 3221224544 3221223728 134615549 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 66804 64211 603 41 0 66763 0
vsize: 267216
[startup+960.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 25544
Raw data (stat): 25538 (minisat+) R 25537 12452 12451 0 -1 0 68792 0 0 0 95829 185 0 0 25 0 1 0 428655124 276004864 64545 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 67384 64545 603 41 0 67343 0
vsize: 269536
[startup+970.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 25544
Raw data (stat): 25538 (minisat+) R 25537 12452 12451 0 -1 0 69097 0 0 0 96829 185 0 0 25 0 1 0 428655124 277323776 64850 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 67706 64850 603 41 0 67665 0
vsize: 270824
[startup+980.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 25544
Raw data (stat): 25538 (minisat+) R 25537 12452 12451 0 -1 0 69452 0 0 0 97829 186 0 0 25 0 1 0 428655124 278654976 65205 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 68031 65205 603 41 0 67990 0
vsize: 272124
[startup+990.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 25546
Raw data (stat): 25538 (minisat+) R 25537 12452 12451 0 -1 0 69763 0 0 0 98828 187 0 0 25 0 1 0 428655124 279965696 65516 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 68351 65516 603 41 0 68310 0
vsize: 273404
[startup+1000.01 s]
Raw data (loadavg): 1.07 0.99 0.91 2/56 25599
Raw data (stat): 25538 (minisat+) R 25537 12452 12451 0 -1 0 70107 0 0 0 99825 188 0 0 25 0 1 0 428655124 281436160 65860 4294967295 134512640 134672761 3221224544 3221223680 134614696 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 68710 65860 603 41 0 68669 0
vsize: 274840
[startup+1010.01 s]
Raw data (loadavg): 1.06 0.99 0.91 2/56 25599
Raw data (stat): 25538 (minisat+) R 25537 12452 12451 0 -1 0 70401 0 0 0 100825 189 0 0 25 0 1 0 428655124 282615808 66154 4294967295 134512640 134672761 3221224544 3221223568 134612944 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 68998 66154 603 41 0 68957 0
vsize: 275992
[startup+1020.01 s]
Raw data (loadavg): 1.05 0.99 0.91 2/56 25599
Raw data (stat): 25538 (minisat+) R 25537 12452 12451 0 -1 0 70729 0 0 0 101824 190 0 0 25 0 1 0 428655124 283934720 66482 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 69320 66482 603 41 0 69279 0
vsize: 277280
[startup+1030.01 s]
Raw data (loadavg): 1.04 0.99 0.91 2/56 25599
Raw data (stat): 25538 (minisat+) R 25537 12452 12451 0 -1 0 71048 0 0 0 102823 191 0 0 25 0 1 0 428655124 285265920 66801 4294967295 134512640 134672761 3221224544 3221223728 134615665 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 69645 66801 603 41 0 69604 0
vsize: 278580
[startup+1040.01 s]
Raw data (loadavg): 1.03 0.99 0.91 2/56 25599
Raw data (stat): 25538 (minisat+) R 25537 12452 12451 0 -1 0 71322 0 0 0 103822 191 0 0 25 0 1 0 428655124 286322688 67075 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 69903 67075 603 41 0 69862 0
vsize: 279612
[startup+1050.01 s]
Raw data (loadavg): 1.03 0.99 0.91 2/56 25601
Raw data (stat): 25538 (minisat+) R 25537 12452 12451 0 -1 0 71597 0 0 0 104821 193 0 0 25 0 1 0 428655124 287522816 67350 4294967295 134512640 134672761 3221224544 3221223552 134522549 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 70196 67350 603 41 0 70155 0
vsize: 280784
[startup+1060.01 s]
Raw data (loadavg): 1.02 0.99 0.91 2/56 25601
Raw data (stat): 25538 (minisat+) R 25537 12452 12451 0 -1 0 71977 0 0 0 105820 194 0 0 25 0 1 0 428655124 288985088 67730 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 70553 67730 603 41 0 70512 0
vsize: 282212
[startup+1070.01 s]
Raw data (loadavg): 1.02 0.99 0.91 2/56 25603
Raw data (stat): 25538 (minisat+) R 25537 12452 12451 0 -1 0 72278 0 0 0 106820 195 0 0 25 0 1 0 428655124 290304000 68031 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 70875 68031 603 41 0 70834 0
vsize: 283500
[startup+1080.01 s]
Raw data (loadavg): 1.02 0.99 0.91 2/56 25603
Raw data (stat): 25538 (minisat+) R 25537 12452 12451 0 -1 0 72527 0 0 0 107819 195 0 0 25 0 1 0 428655124 291348480 68280 4294967295 134512640 134672761 3221224544 3221223728 134615916 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 71130 68280 603 41 0 71089 0
vsize: 284520
[startup+1090.01 s]
Raw data (loadavg): 1.01 0.99 0.91 2/56 25603
Raw data (stat): 25538 (minisat+) R 25537 12452 12451 0 -1 0 72878 0 0 0 108818 196 0 0 25 0 1 0 428655124 292786176 68631 4294967295 134512640 134672761 3221224544 3221223728 134615916 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 71481 68631 603 41 0 71440 0
vsize: 285924
[startup+1100.01 s]
Raw data (loadavg): 1.01 0.99 0.91 2/56 25603
Raw data (stat): 25538 (minisat+) R 25537 12452 12451 0 -1 0 73254 0 0 0 109817 198 0 0 25 0 1 0 428655124 294232064 69007 4294967295 134512640 134672761 3221224544 3221223728 134615665 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 71834 69007 603 41 0 71793 0
vsize: 287336
[startup+1110.01 s]
Raw data (loadavg): 1.01 0.99 0.91 2/56 25603
Raw data (stat): 25538 (minisat+) R 25537 12452 12451 0 -1 0 73619 0 0 0 110816 199 0 0 25 0 1 0 428655124 295800832 69372 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 72217 69372 603 41 0 72176 0
vsize: 288868
[startup+1120.01 s]
Raw data (loadavg): 1.01 0.99 0.91 2/56 25603
Raw data (stat): 25538 (minisat+) R 25537 12452 12451 0 -1 0 73951 0 0 0 111815 200 0 0 25 0 1 0 428655124 297136128 69704 4294967295 134512640 134672761 3221224544 3221223728 134615663 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 72543 69704 603 41 0 72502 0
vsize: 290172
[startup+1130.01 s]
Raw data (loadavg): 1.00 0.99 0.91 2/56 25603
Raw data (stat): 25538 (minisat+) R 25537 12452 12451 0 -1 0 74316 0 0 0 112815 200 0 0 25 0 1 0 428655124 298586112 70069 4294967295 134512640 134672761 3221224544 3221223744 134610707 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 72897 70069 603 41 0 72856 0
vsize: 291588
[startup+1140.01 s]
Raw data (loadavg): 1.00 0.99 0.91 2/56 25603
Raw data (stat): 25538 (minisat+) R 25537 12452 12451 0 -1 0 74620 0 0 0 113815 201 0 0 25 0 1 0 428655124 299909120 70373 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 73220 70373 603 41 0 73179 0
vsize: 292880
[startup+1150.01 s]
Raw data (loadavg): 1.00 0.99 0.91 2/56 25603
Raw data (stat): 25538 (minisat+) R 25537 12452 12451 0 -1 0 74958 0 0 0 114814 201 0 0 25 0 1 0 428655124 301228032 70711 4294967295 134512640 134672761 3221224544 3221223744 134610614 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 73542 70711 603 41 0 73501 0
vsize: 294168
[startup+1160.01 s]
Raw data (loadavg): 1.00 0.99 0.91 2/56 25603
Raw data (stat): 25538 (minisat+) R 25537 12452 12451 0 -1 0 75318 0 0 0 115813 202 0 0 25 0 1 0 428655124 302669824 71071 4294967295 134512640 134672761 3221224544 3221223728 134615649 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 73894 71071 603 41 0 73853 0
vsize: 295576
[startup+1170.01 s]
Raw data (loadavg): 1.00 0.99 0.91 2/56 25603
Raw data (stat): 25538 (minisat+) R 25537 12452 12451 0 -1 0 75714 0 0 0 116813 203 0 0 25 0 1 0 428655124 304369664 71467 4294967295 134512640 134672761 3221224544 3221223584 134613822 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 74309 71467 603 41 0 74268 0
vsize: 297236
[startup+1180.01 s]
Raw data (loadavg): 1.00 0.99 0.91 2/56 25603
Raw data (stat): 25538 (minisat+) R 25537 12452 12451 0 -1 0 76060 0 0 0 117812 204 0 0 25 0 1 0 428655124 305700864 71813 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 74634 71813 603 41 0 74593 0
vsize: 298536
[startup+1190.01 s]
Raw data (loadavg): 1.00 0.99 0.91 2/56 25603
Raw data (stat): 25538 (minisat+) R 25537 12452 12451 0 -1 0 76413 0 0 0 118812 205 0 0 25 0 1 0 428655124 307154944 72166 4294967295 134512640 134672761 3221224544 3221223728 134615663 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 74989 72166 603 41 0 74948 0
vsize: 299956
[startup+1200.01 s]
Raw data (loadavg): 1.00 0.99 0.91 2/56 25603
Raw data (stat): 25538 (minisat+) R 25537 12452 12451 0 -1 0 76742 0 0 0 119811 205 0 0 25 0 1 0 428655124 308477952 72495 4294967295 134512640 134672761 3221224544 3221223728 134615627 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 75312 72495 603 41 0 75271 0
vsize: 301248
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.15 s]
Raw data (loadavg): 1.00 0.99 0.91 1/56 25603
Raw data (stat): 25538 (minisat+) Z 25537 12452 12451 0 -1 12 76742 0 0 0 119811 219 0 0 25 0 1 0 428655124 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.15
CPU time (s): 1200.31
CPU user time (s): 1198.12
CPU system time (s): 2.19567
CPU usage (%): 100.014
Max. virtual memory (Kb): 301248
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####