PB'05 competition: run trace

Some explanations

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

Name	normalized-opb/mps-v2-13-7/plato.asu.edu/pub/unibo/normalized-mps-v2-13-7-railway_8_1_0.opb
MD5SUM	9689869ef48b5a0c26d142f61d149c48
Bench Category	optimization, medium integers (OPTMEDINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	51200
Optimality of the best value was proved	NO
Number of terms in the objective function	123
Biggest coefficient in the objective function	524288
Number of bits for the biggest coefficient in the objective function	20
Sum of the numbers in the objective function	1061759
Number of bits of the sum of numbers in the objective function	21
Biggest number in a constraint	128000000
Number of bits of the biggest number in a constraint	27
Biggest sum of numbers in a constraint	268469758
Number of bits of the biggest sum of numbers	29
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	1189.08
Number of variables	17883
Total number of constraints	4322
Number of constraints which are clauses	426
Number of constraints which are cardinality constraints (but not clauses)	1177
Number of constraints which are nor clauses,nor cardinality constraints	2719
Minimum length of a constraint	1
Maximum length of a constraint	55
Trace number 32515

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc11 THE 2005-05-27 10:32:58 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=23910 boxname=wulflinc11 idbench=1554 idsolver=16 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  9689869ef48b5a0c26d142f61d149c48  /oldhome/oroussel/tmp/wulflinc11/normalized-mps-v2-13-7-railway_8_1_0.opb
REAL COMMAND:  minisat+_script -cb -gs /oldhome/oroussel/tmp/wulflinc11/normalized-mps-v2-13-7-railway_8_1_0.opb
IDLAUNCH: 23910
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.028
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.028
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:        903616 kB
Buffers:          1812 kB
Cached:         109752 kB
SwapCached:        772 kB
Active:          22776 kB
Inactive:        90776 kB
HighTotal:      131008 kB
HighFree:        17948 kB
LowTotal:       903652 kB
LowFree:        885668 kB
SwapTotal:     2097136 kB
SwapFree:      2095356 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           4924 kB
Slab:            11676 kB
Committed_AS:    63604 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-05-27 10:53:28 (client local time) WITH STATUS 152 IN 1229.87 SECONDS
stats: 23910 7 1229.87 152
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 3146 PB-constraints to clauses...
c   -- Unit propagations: pppp
c   -- Detecting intervals from adjacent constraints: ###################################################################################################################################################################
c   -- Clauses(.)/Splits(s): ssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssss..........................................................................................................................................................................................................................................................................................................................................................................................................................................
c ---[3140]---> BDD-cost:   79
c ---[3139]---> BDD-cost:   79
c ---[3138]---> BDD-cost:   79
c ---[3137]---> BDD-cost:  112
c ---[3136]---> BDD-cost:  110
c ---[3135]---> BDD-cost:   79
c ---[3134]---> BDD-cost:   79
c ---[3133]---> BDD-cost:   79
c ---[3132]---> BDD-cost:   79
c ---[3131]---> BDD-cost:  110
c ---[3129]---> BDD-cost:  110
c ---[3128]---> BDD-cost:   79
c ---[3127]---> BDD-cost:   79
c ---[3126]---> BDD-cost:   79
c ---[3125]---> BDD-cost:   79
c ---[3124]---> BDD-cost:  112
c ---[3123]---> BDD-cost:  110
c ---[3122]---> BDD-cost:   79
c ---[3121]---> BDD-cost:   79
c ---[3120]---> BDD-cost:   79
c ---[3118]---> BDD-cost:   79
c ---[3117]---> BDD-cost:  114
c ---[3116]---> BDD-cost:  110
c ---[3115]---> BDD-cost:   79
c ---[3114]---> BDD-cost:   79
c ---[3113]---> BDD-cost:   79
c ---[3112]---> BDD-cost:   79
c ---[3111]---> BDD-cost:  114
c ---[3110]---> BDD-cost:  110
c ---[3109]---> BDD-cost:   79
c ---[3107]---> BDD-cost:   79
c ---[3106]---> BDD-cost:   79
c ---[3105]---> BDD-cost:   79
c ---[3104]---> BDD-cost:  112
c ---[3103]---> BDD-cost:  110
c ---[3102]---> BDD-cost:   79
c ---[3101]---> BDD-cost:   79
c ---[3100]---> BDD-cost:   79
c ---[3099]---> BDD-cost:   79
c ---[3098]---> BDD-cost:  116
c ---[3096]---> BDD-cost:  110
c ---[3095]---> BDD-cost:   79
c ---[3094]---> BDD-cost:   79
c ---[3093]---> BDD-cost:   79
c ---[3092]---> BDD-cost:   79
c ---[3090]---> BDD-cost:  116
c ---[3088]---> BDD-cost:  114
c ---[3087]---> BDD-cost:  116
c ---[3085]---> BDD-cost:  116
c ---[3083]---> BDD-cost:  116
c ---[3081]---> BDD-cost:  114
c ---[3079]---> BDD-cost:  116
c ---[3077]---> BDD-cost:  116
c ---[3076]---> BDD-cost:  116
c ---[3074]---> BDD-cost:  116
c ---[3072]---> BDD-cost:  116
c ---[3070]---> BDD-cost:  114
c ---[3068]---> BDD-cost:  114
c ---[3066]---> BDD-cost:  116
c ---[3065]---> BDD-cost:  114
c ---[3063]---> BDD-cost:  114
c ---[3061]---> BDD-cost:   79
c ---[3059]---> BDD-cost:  116
c ---[3057]---> BDD-cost:  116
c ---[3055]---> BDD-cost:  116
c ---[3054]---> BDD-cost:  114
c ---[3052]---> BDD-cost:  114
c ---[3050]---> BDD-cost:  116
c ---[3048]---> BDD-cost:  114
c ---[3046]---> BDD-cost:  116
c ---[3044]---> BDD-cost:  116
c ---[3043]---> BDD-cost:  116
c ---[3041]---> BDD-cost:  116
c ---[3039]---> BDD-cost:   79
c ---[3037]---> BDD-cost:   79
c ---[3035]---> BDD-cost:  114
c ---[3033]---> BDD-cost:  112
c ---[3032]---> BDD-cost:  114
c ---[3029]---> BDD-cost:  114
c ---[3027]---> BDD-cost:  112
c ---[3025]---> BDD-cost:  116
c ---[3023]---> BDD-cost:  114
c ---[3021]---> BDD-cost:  116
c ---[3020]---> BDD-cost:  114
c ---[3018]---> BDD-cost:  114
c ---[3016]---> BDD-cost:  114
c ---[3014]---> BDD-cost:  116
c ---[3012]---> BDD-cost:  116
c ---[3010]---> BDD-cost:  112
c ---[3009]---> BDD-cost:  110
c ---[3007]---> BDD-cost:  110
c ---[3005]---> BDD-cost:  110
c ---[3003]---> BDD-cost:  110
c ---[3001]---> BDD-cost:  114
c ---[2999]---> BDD-cost:  116
c ---[2998]---> BDD-cost:  116
c ---[2996]---> BDD-cost:  116
c ---[2994]---> BDD-cost:   79
c ---[2992]---> BDD-cost:  116
c ---[2990]---> BDD-cost:  114
c ---[2988]---> BDD-cost:  116
c ---[2987]---> BDD-cost:  116
c ---[2985]---> BDD-cost:  116
c ---[2983]---> BDD-cost:  116
c ---[2981]---> BDD-cost:  114
c ---[2979]---> BDD-cost:  116
c ---[2977]---> BDD-cost:  112
c ---[2976]---> BDD-cost:  116
c ---[2974]---> BDD-cost:  116
c ---[2972]---> BDD-cost:  112
c ---[2970]---> BDD-cost:  116
c ---[2968]---> BDD-cost:  114
c ---[2966]---> BDD-cost:  116
c ---[2965]---> BDD-cost:  114
c ---[2963]---> BDD-cost:  114
c ---[2961]---> BDD-cost:  114
c ---[2959]---> BDD-cost:   79
c ---[2957]---> BDD-cost:  114
c ---[2955]---> BDD-cost:  114
c ---[2954]---> BDD-cost:  116
c ---[2952]---> BDD-cost:  116
c ---[2950]---> BDD-cost:   79
c ---[2948]---> BDD-cost:  114
c ---[2946]---> BDD-cost:  114
c ---[2944]---> BDD-cost:  116
c ---[2943]---> BDD-cost:  114
c ---[2941]---> BDD-cost:  114
c ---[2939]---> BDD-cost:  116
c ---[2937]---> BDD-cost:  116
c ---[2935]---> BDD-cost:  114
c ---[2933]---> BDD-cost:  114
c ---[2932]---> BDD-cost:  112
c ---[2930]---> BDD-cost:  112
c ---[2928]---> BDD-cost:  114
c ---[2926]---> BDD-cost:  116
c ---[2924]---> BDD-cost:  114
c ---[2922]---> BDD-cost:   79
c ---[2921]---> BDD-cost:  116
c ---[2918]---> BDD-cost:  116
c ---[2916]---> BDD-cost:  114
c ---[2914]---> BDD-cost:  116
c ---[2912]---> BDD-cost:   79
c ---[2910]---> BDD-cost:  116
c ---[2909]---> BDD-cost:  114
c ---[2907]---> BDD-cost:  114
c ---[2905]---> BDD-cost:  112
c ---[2903]---> BDD-cost:  114
c ---[2901]---> BDD-cost:   79
c ---[2899]---> BDD-cost:  112
c ---[2898]---> BDD-cost:  116
c ---[2896]---> BDD-cost:  116
c ---[2894]---> BDD-cost:  114
c ---[2892]---> BDD-cost:  116
c ---[2890]---> BDD-cost:  116
c ---[2888]---> BDD-cost:  114
c ---[2887]---> BDD-cost:  116
c ---[2885]---> BDD-cost:  116
c ---[2883]---> BDD-cost:   79
c ---[2881]---> BDD-cost:  116
c ---[2879]---> BDD-cost:  114
c ---[2877]---> BDD-cost:  116
c ---[2876]---> BDD-cost:  112
c ---[2874]---> BDD-cost:  112
c ---[2872]---> BDD-cost:  112
c ---[2870]---> BDD-cost:  110
c ---[2868]---> BDD-cost:  116
c ---[2866]---> BDD-cost:  114
c ---[2865]---> BDD-cost:  114
c ---[2863]---> BDD-cost:  114
c ---[2861]---> BDD-cost:  116
c ---[2859]---> BDD-cost:   79
c ---[2857]---> BDD-cost:  114
c ---[2855]---> BDD-cost:  116
c ---[2854]---> BDD-cost:   79
c ---[2852]---> BDD-cost:   79
c ---[2850]---> BDD-cost:  116
c ---[2848]---> BDD-cost:  116
c ---[2846]---> BDD-cost:  116
c ---[2844]---> BDD-cost:  116
c ---[2843]---> BDD-cost:  114
c ---[2841]---> BDD-cost:  114
c ---[2839]---> BDD-cost:  116
c ---[2837]---> BDD-cost:  114
c ---[2835]---> BDD-cost:  114
c ---[2833]---> BDD-cost:  114
c ---[2832]---> BDD-cost:   79
c ---[2830]---> BDD-cost:   79
c ---[2828]---> BDD-cost:  116
c ---[2826]---> BDD-cost:  116
c ---[2824]---> BDD-cost:  112
c ---[2822]---> BDD-cost:  116
c ---[2821]---> BDD-cost:  116
c ---[2819]---> BDD-cost:  116
c ---[2817]---> BDD-cost:   79
c ---[2815]---> BDD-cost:  116
c ---[2813]---> BDD-cost:  114
c ---[2811]---> BDD-cost:  116
c ---[2810]---> BDD-cost:  116
c ---[2807]---> BDD-cost:  116
c ---[2805]---> BDD-cost:  116
c ---[2803]---> BDD-cost:  116
c ---[2801]---> BDD-cost:   79
c ---[2799]---> BDD-cost:  116
c ---[2798]---> BDD-cost:  116
c ---[2796]---> BDD-cost:  116
c ---[2794]---> BDD-cost:   79
c ---[2792]---> BDD-cost:  116
c ---[2790]---> BDD-cost:  114
c ---[2788]---> BDD-cost:  116
c ---[2787]---> BDD-cost:  116
c ---[2785]---> BDD-cost:  116
c ---[2783]---> BDD-cost:  114
c ---[2781]---> BDD-cost:   79
c ---[2779]---> BDD-cost:   79
c ---[2777]---> BDD-cost:  116
c ---[2776]---> BDD-cost:  116
c ---[2774]---> BDD-cost:  116
c ---[2772]---> BDD-cost:  116
c ---[2770]---> BDD-cost:   79
c ---[2768]---> BDD-cost:  112
c ---[2766]---> BDD-cost:  114
c ---[2765]---> BDD-cost:   79
c ---[2763]---> BDD-cost:   79
c ---[2761]---> BDD-cost:  116
c ---[2759]---> BDD-cost:   79
c ---[2757]---> BDD-cost:  114
c ---[2755]---> BDD-cost:   79
c ---[2754]---> BDD-cost:   79
c ---[2752]---> BDD-cost:   79
c ---[2750]---> BDD-cost:  116
c ---[2748]---> BDD-cost:  116
c ---[2746]---> BDD-cost:   79
c ---[2744]---> BDD-cost:   79
c ---[2743]---> BDD-cost:  116
c ---[2741]---> BDD-cost:  116
c ---[2739]---> BDD-cost:  116
c ---[2737]---> BDD-cost:  116
c ---[2735]---> BDD-cost:  116
c ---[2733]---> BDD-cost:  116
c ---[2732]---> BDD-cost:  116
c ---[2730]---> BDD-cost:  116
c ---[2728]---> BDD-cost:   79
c ---[2726]---> BDD-cost:  116
c ---[2724]---> BDD-cost:  116
c ---[2722]---> BDD-cost:   79
c ---[2721]---> BDD-cost:  116
c ---[2719]---> BDD-cost:  116
c ---[2717]---> BDD-cost:   79
c ---[2715]---> BDD-cost:   79
c ---[2713]---> BDD-cost:  116
c ---[2711]---> BDD-cost:   79
c ---[2710]---> BDD-cost:   79
c ---[2708]---> BDD-cost:   79
c ---[2706]---> BDD-cost:   79
c ---[2704]---> BDD-cost:  116
c ---[2702]---> BDD-cost:  116
c ---[2700]---> BDD-cost:   79
c ---[2699]---> BDD-cost:  116
c ---[2696]---> BDD-cost:  116
c ---[2694]---> BDD-cost:   79
c ---[2692]---> BDD-cost:  116
c ---[2690]---> BDD-cost:  114
c ---[2688]---> BDD-cost:   79
c ---[2687]---> BDD-cost:  116
c ---[2685]---> BDD-cost:  116
c ---[2683]---> BDD-cost:  116
c ---[2681]---> BDD-cost:  116
c ---[2679]---> BDD-cost:  112
c ---[2677]---> BDD-cost:  116
c ---[2676]---> BDD-cost:  114
c ---[2674]---> BDD-cost:  114
c ---[2672]---> BDD-cost:  114
c ---[2670]---> BDD-cost:   79
c ---[2668]---> BDD-cost:  116
c ---[2666]---> BDD-cost:  112
c ---[2665]---> BDD-cost:  116
c ---[2663]---> BDD-cost:  116
c ---[2661]---> BDD-cost:  116
c ---[2659]---> BDD-cost:  114
c ---[2657]---> BDD-cost:  114
c ---[2655]---> BDD-cost:   79
c ---[2654]---> BDD-cost:  116
c ---[2652]---> BDD-cost:  116
c ---[2650]---> BDD-cost:  116
c ---[2648]---> BDD-cost:  116
c ---[2646]---> BDD-cost:   79
c ---[2644]---> BDD-cost:  114
c ---[2643]---> BDD-cost:  112
c ---[2641]---> BDD-cost:  112
c ---[2639]---> BDD-cost:  110
c ---[2638]---> BDD-cost:  119
c ---[2637]---> BDD-cost:  119
c ---[2636]---> BDD-cost:  128
c ---[2635]---> BDD-cost:  128
c ---[2634]---> BDD-cost:  131
c ---[2633]---> BDD-cost:  131
c ---[2632]---> BDD-cost:  128
c ---[2630]---> BDD-cost:  128
c ---[2629]---> BDD-cost:  126
c ---[2628]---> BDD-cost:  126
c ---[2627]---> BDD-cost:  128
c ---[2626]---> BDD-cost:  128
c ---[2625]---> BDD-cost:  134
c ---[2624]---> BDD-cost:  134
c ---[2623]---> BDD-cost:  128
c ---[2622]---> BDD-cost:  128
c ---[2621]---> BDD-cost:  126
c ---[2619]---> BDD-cost:  126
c ---[2618]---> BDD-cost:  128
c ---[2617]---> BDD-cost:  128
c ---[2616]---> BDD-cost:  131
c ---[2615]---> BDD-cost:  131
c ---[2614]---> BDD-cost:  128
c ---[2613]---> BDD-cost:  128
c ---[2612]---> BDD-cost:  129
c ---[2611]---> BDD-cost:  129
c ---[2610]---> BDD-cost:  128
c ---[2608]---> BDD-cost:  128
c ---[2607]---> BDD-cost:  134
c ---[2606]---> BDD-cost:  134
c ---[2605]---> BDD-cost:  128
c ---[2604]---> BDD-cost:  128
c ---[2603]---> BDD-cost:  131
c ---[2602]---> BDD-cost:  131
c ---[2601]---> BDD-cost:  128
c ---[2600]---> BDD-cost:  128
c ---[2599]---> BDD-cost:  121
c ---[2597]---> BDD-cost:  121
c ---[2596]---> BDD-cost:  128
c ---[2595]---> BDD-cost:  128
c ---[2594]---> BDD-cost:  137
c ---[2593]---> BDD-cost:  137
c ---[2592]---> BDD-cost:  128
c ---[2591]---> BDD-cost:  128
c ---[2590]---> BDD-cost:  124
c ---[2589]---> BDD-cost:  124
c ---[2588]---> BDD-cost:  128
c ---[2585]---> BDD-cost:  128
c ---[2584]---> BDD-cost:  129
c ---[2583]---> BDD-cost:  129
c ---[2582]---> BDD-cost:  128
c ---[2581]---> BDD-cost:  128
c ---[2580]---> BDD-cost:  137
c ---[2579]---> BDD-cost:  137
c ---[2578]---> BDD-cost:  128
c ---[2577]---> BDD-cost:  128
c ---[2576]---> BDD-cost:  134
c ---[2574]---> BDD-cost:  134
c ---[2573]---> BDD-cost:  128
c ---[2572]---> BDD-cost:  128
c ---[2571]---> BDD-cost:  134
c ---[2570]---> BDD-cost:  134
c ---[2569]---> BDD-cost:  128
c ---[2568]---> BDD-cost:  128
c ---[2567]---> BDD-cost:  134
c ---[2566]---> BDD-cost:  134
c ---[2565]---> BDD-cost:  128
c ---[2563]---> BDD-cost:  128
c ---[2562]---> BDD-cost:  129
c ---[2561]---> BDD-cost:  129
c ---[2560]---> BDD-cost:  128
c ---[2559]---> BDD-cost:  128
c ---[2558]---> BDD-cost:  131
c ---[2557]---> BDD-cost:  131
c ---[2556]---> BDD-cost:  128
c ---[2555]---> BDD-cost:  128
c ---[2554]---> BDD-cost:  134
c ---[2552]---> BDD-cost:  134
c ---[2551]---> BDD-cost:  128
c ---[2550]---> BDD-cost:  128
c ---[2549]---> BDD-cost:  132
c ---[2548]---> BDD-cost:  132
c ---[2547]---> BDD-cost:  128
c ---[2546]---> BDD-cost:  128
c ---[2545]---> BDD-cost:  131
c ---[2544]---> BDD-cost:  131
c ---[2543]---> BDD-cost:  128
c ---[2541]---> BDD-cost:  128
c ---[2540]---> BDD-cost:  131
c ---[2539]---> BDD-cost:  131
c ---[2538]---> BDD-cost:  128
c ---[2537]---> BDD-cost:  128
c ---[2536]---> BDD-cost:  134
c ---[2535]---> BDD-cost:  134
c ---[2534]---> BDD-cost:  128
c ---[2533]---> BDD-cost:  128
c ---[2532]---> BDD-cost:  131
c ---[2530]---> BDD-cost:  131
c ---[2529]---> BDD-cost:  128
c ---[2528]---> BDD-cost:  128
c ---[2527]---> BDD-cost:  131
c ---[2526]---> BDD-cost:  131
c ---[2525]---> BDD-cost:  128
c ---[2524]---> BDD-cost:  128
c ---[2523]---> BDD-cost:  131
c ---[2522]---> BDD-cost:  131
c ---[2521]---> BDD-cost:  128
c ---[2519]---> BDD-cost:  128
c ---[2518]---> BDD-cost:  134
c ---[2517]---> BDD-cost:  134
c ---[2516]---> BDD-cost:  128
c ---[2515]---> BDD-cost:  128
c ---[2514]---> BDD-cost:  131
c ---[2513]---> BDD-cost:  131
c ---[2512]---> BDD-cost:  128
c ---[2511]---> BDD-cost:  128
c ---[2510]---> BDD-cost:  131
c ---[2508]---> BDD-cost:  131
c ---[2507]---> BDD-cost:  128
c ---[2506]---> BDD-cost:  128
c ---[2505]---> BDD-cost:  134
c ---[2504]---> BDD-cost:  134
c ---[2503]---> BDD-cost:  128
c ---[2502]---> BDD-cost:  128
c ---[2501]---> BDD-cost:  134
c ---[2500]---> BDD-cost:  134
c ---[2499]---> BDD-cost:  128
c ---[2497]---> BDD-cost:  128
c ---[2496]---> BDD-cost:  134
c ---[2495]---> BDD-cost:  134
c ---[2494]---> BDD-cost:  128
c ---[2493]---> BDD-cost:  128
c ---[2492]---> BDD-cost:  131
c ---[2491]---> BDD-cost:  131
c ---[2490]---> BDD-cost:  128
c ---[2489]---> BDD-cost:  128
c ---[2488]---> BDD-cost:  134
c ---[2486]---> BDD-cost:  134
c ---[2485]---> BDD-cost:  128
c ---[2484]---> BDD-cost:  128
c ---[2483]---> BDD-cost:  131
c ---[2482]---> BDD-cost:  131
c ---[2481]---> BDD-cost:  128
c ---[2480]---> BDD-cost:  128
c ---[2479]---> BDD-cost:  119
c ---[2478]---> BDD-cost:  119
c ---[2477]---> BDD-cost:  128
c ---[2474]---> BDD-cost:  128
c ---[2473]---> BDD-cost:  129
c ---[2472]---> BDD-cost:  129
c ---[2471]---> BDD-cost:  128
c ---[2470]---> BDD-cost:  128
c ---[2469]---> BDD-cost:  124
c ---[2468]---> BDD-cost:  124
c ---[2467]---> BDD-cost:  128
c ---[2466]---> BDD-cost:  128
c ---[2465]---> BDD-cost:  131
c ---[2463]---> BDD-cost:  131
c ---[2462]---> BDD-cost:  128
c ---[2461]---> BDD-cost:  128
c ---[2460]---> BDD-cost:  131
c ---[2459]---> BDD-cost:  131
c ---[2458]---> BDD-cost:  128
c ---[2457]---> BDD-cost:  128
c ---[2456]---> BDD-cost:  131
c ---[2455]---> BDD-cost:  131
c ---[2454]---> BDD-cost:  128
c ---[2452]---> BDD-cost:  128
c ---[2451]---> BDD-cost:  131
c ---[2450]---> BDD-cost:  131
c ---[2449]---> BDD-cost:  128
c ---[2448]---> BDD-cost:  128
c ---[2447]---> BDD-cost:  128
c ---[2446]---> BDD-cost:  128
c ---[2445]---> BDD-cost:  128
c ---[2444]---> BDD-cost:  128
c ---[2443]---> BDD-cost:  134
c ---[2441]---> BDD-cost:  134
c ---[2440]---> BDD-cost:  128
c ---[2439]---> BDD-cost:  128
c ---[2438]---> BDD-cost:  134
c ---[2437]---> BDD-cost:  134
c ---[2436]---> BDD-cost:  128
c ---[2435]---> BDD-cost:  128
c ---[2434]---> BDD-cost:  132
c ---[2433]---> BDD-cost:  132
c ---[2432]---> BDD-cost:  128
c ---[2430]---> BDD-cost:  128
c ---[2429]---> BDD-cost:  131
c ---[2428]---> BDD-cost:  131
c ---[2427]---> BDD-cost:  128
c ---[2426]---> BDD-cost:  128
c ---[2425]---> BDD-cost:  117
c ---[2424]---> BDD-cost:  117
c ---[2423]---> BDD-cost:  128
c ---[2422]---> BDD-cost:  128
c ---[2421]---> BDD-cost:  126
c ---[2419]---> BDD-cost:  126
c ---[2418]---> BDD-cost:  128
c ---[2417]---> BDD-cost:  128
c ---[2416]---> BDD-cost:  131
c ---[2415]---> BDD-cost:  131
c ---[2414]---> BDD-cost:  128
c ---[2413]---> BDD-cost:  128
c ---[2412]---> BDD-cost:  126
c ---[2411]---> BDD-cost:  126
c ---[2410]---> BDD-cost:  128
c ---[2408]---> BDD-cost:  128
c ---[2407]---> BDD-cost:  126
c ---[2406]---> BDD-cost:  126
c ---[2405]---> BDD-cost:  128
c ---[2404]---> BDD-cost:  128
c ---[2403]---> BDD-cost:  134
c ---[2402]---> BDD-cost:  134
c ---[2401]---> BDD-cost:  128
c ---[2400]---> BDD-cost:  128
c ---[2399]---> BDD-cost:  129
c ---[2397]---> BDD-cost:  129
c ---[2396]---> BDD-cost:  128
c ---[2395]---> BDD-cost:  128
c ---[2394]---> BDD-cost:  126
c ---[2393]---> BDD-cost:  126
c ---[2392]---> BDD-cost:  128
c ---[2391]---> BDD-cost:  128
c ---[2390]---> BDD-cost:  127
c ---[2389]---> BDD-cost:  127
c ---[2388]---> BDD-cost:  128
c ---[2386]---> BDD-cost:  128
c ---[2385]---> BDD-cost:  137
c ---[2384]---> BDD-cost:  137
c ---[2383]---> BDD-cost:  128
c ---[2382]---> BDD-cost:  128
c ---[2381]---> BDD-cost:  129
c ---[2380]---> BDD-cost:  129
c ---[2379]---> BDD-cost:  128
c ---[2378]---> BDD-cost:  128
c ---[2377]---> BDD-cost:  134
c ---[2375]---> BDD-cost:  134
c ---[2374]---> BDD-cost:  128
c ---[2373]---> BDD-cost:  128
c ---[2372]---> BDD-cost:  114
c ---[2371]---> BDD-cost:  114
c ---[2370]---> BDD-cost:  128
c ---[2369]---> BDD-cost:  128
c ---[2368]---> BDD-cost:  137
c ---[2367]---> BDD-cost:  137
c ---[2366]---> BDD-cost:  128
c ---[2363]---> BDD-cost:  128
c ---[2362]---> BDD-cost:  134
c ---[2361]---> BDD-cost:  134
c ---[2360]---> BDD-cost:  128
c ---[2359]---> BDD-cost:  128
c ---[2358]---> BDD-cost:  131
c ---[2357]---> BDD-cost:  131
c ---[2356]---> BDD-cost:  128
c ---[2355]---> BDD-cost:  128
c ---[2354]---> BDD-cost:  119
c ---[2352]---> BDD-cost:  119
c ---[2351]---> BDD-cost:  128
c ---[2350]---> BDD-cost:  128
c ---[2349]---> BDD-cost:  134
c ---[2348]---> BDD-cost:  134
c ---[2347]---> BDD-cost:  128
c ---[2346]---> BDD-cost:  128
c ---[2345]---> BDD-cost:  124
c ---[2344]---> BDD-cost:  124
c ---[2343]---> BDD-cost:  128
c ---[2341]---> BDD-cost:  128
c ---[2340]---> BDD-cost:  132
c ---[2339]---> BDD-cost:  132
c ---[2338]---> BDD-cost:  128
c ---[2337]---> BDD-cost:  128
c ---[2336]---> BDD-cost:  129
c ---[2335]---> BDD-cost:  129
c ---[2334]---> BDD-cost:  128
c ---[2333]---> BDD-cost:  128
c ---[2332]---> BDD-cost:  116
c ---[2330]---> BDD-cost:  116
c ---[2329]---> BDD-cost:  128
c ---[2328]---> BDD-cost:  128
c ---[2327]---> BDD-cost:  134
c ---[2326]---> BDD-cost:  134
c ---[2325]---> BDD-cost:  128
c ---[2324]---> BDD-cost:  128
c ---[2323]---> BDD-cost:  134
c ---[2322]---> BDD-cost:  134
c ---[2321]---> BDD-cost:  128
c ---[2319]---> BDD-cost:  128
c ---[2318]---> BDD-cost:  134
c ---[2317]---> BDD-cost:  134
c ---[2316]---> BDD-cost:  128
c ---[2315]---> BDD-cost:  128
c ---[2314]---> BDD-cost:  126
c ---[2313]---> BDD-cost:  126
c ---[2312]---> BDD-cost:  128
c ---[2311]---> BDD-cost:  128
c ---[2310]---> BDD-cost:  131
c ---[2308]---> BDD-cost:  131
c ---[2307]---> BDD-cost:  128
c ---[2306]---> BDD-cost:  128
c ---[2305]---> BDD-cost:  119
c ---[2304]---> BDD-cost:  119
c ---[2303]---> BDD-cost:  128
c ---[2302]---> BDD-cost:  128
c ---[2301]---> BDD-cost:  134
c ---[2300]---> BDD-cost:  134
c ---[2299]---> BDD-cost:  128
c ---[2297]---> BDD-cost:  128
c ---[2296]---> BDD-cost:  129
c ---[2295]---> BDD-cost:  129
c ---[2294]---> BDD-cost:  128
c ---[2293]---> BDD-cost:  128
c ---[2292]---> BDD-cost:  114
c ---[2291]---> BDD-cost:  114
c ---[2290]---> BDD-cost:  128
c ---[2289]---> BDD-cost:  128
c ---[2288]---> BDD-cost:  131
c ---[2286]---> BDD-cost:  131
c ---[2285]---> BDD-cost:  128
c ---[2284]---> BDD-cost:  128
c ---[2283]---> BDD-cost:  131
c ---[2282]---> BDD-cost:  131
c ---[2281]---> BDD-cost:  128
c ---[2280]---> BDD-cost:  128
c ---[2279]---> BDD-cost:  131
c ---[2278]---> BDD-cost:  131
c ---[2277]---> BDD-cost:  128
c ---[2275]---> BDD-cost:  128
c ---[2274]---> BDD-cost:  126
c ---[2273]---> BDD-cost:  126
c ---[2272]---> BDD-cost:  128
c ---[2271]---> BDD-cost:  128
c ---[2270]---> BDD-cost:  129
c ---[2269]---> BDD-cost:  129
c ---[2268]---> BDD-cost:  128
c ---[2267]---> BDD-cost:  128
c ---[2266]---> BDD-cost:  134
c ---[2264]---> BDD-cost:  134
c ---[2263]---> BDD-cost:  128
c ---[2262]---> BDD-cost:  128
c ---[2261]---> BDD-cost:  129
c ---[2260]---> BDD-cost:  129
c ---[2259]---> BDD-cost:  128
c ---[2258]---> BDD-cost:  128
c ---[2257]---> BDD-cost:  134
c ---[2256]---> BDD-cost:  134
c ---[2255]---> BDD-cost:  128
c ---[2252]---> BDD-cost:  128
c ---[2251]---> BDD-cost:  134
c ---[2250]---> BDD-cost:  134
c ---[2249]---> BDD-cost:  128
c ---[2248]---> BDD-cost:  128
c ---[2247]---> BDD-cost:  119
c ---[2246]---> BDD-cost:  119
c ---[2245]---> BDD-cost:  128
c ---[2244]---> BDD-cost:  128
c ---[2243]---> BDD-cost:  134
c ---[2241]---> BDD-cost:  134
c ---[2240]---> BDD-cost:  128
c ---[2239]---> BDD-cost:  128
c ---[2238]---> BDD-cost:  124
c ---[2237]---> BDD-cost:  124
c ---[2236]---> BDD-cost:  128
c ---[2235]---> BDD-cost:  128
c ---[2234]---> BDD-cost:  131
c ---[2233]---> BDD-cost:  131
c ---[2232]---> BDD-cost:  128
c ---[2230]---> BDD-cost:  128
c ---[2229]---> BDD-cost:  121
c ---[2228]---> BDD-cost:  121
c ---[2227]---> BDD-cost:  128
c ---[2226]---> BDD-cost:  128
c ---[2225]---> BDD-cost:  131
c ---[2224]---> BDD-cost:  131
c ---[2223]---> BDD-cost:  128
c ---[2222]---> BDD-cost:  128
c ---[2221]---> BDD-cost:  124
c ---[2219]---> BDD-cost:  124
c ---[2218]---> BDD-cost:  128
c ---[2217]---> BDD-cost:  128
c ---[2216]---> BDD-cost:  109
c ---[2215]---> BDD-cost:  109
c ---[2214]---> BDD-cost:  128
c ---[2213]---> BDD-cost:  128
c ---[2212]---> BDD-cost:  131
c ---[2211]---> BDD-cost:  131
c ---[2210]---> BDD-cost:  128
c ---[2208]---> BDD-cost:  128
c ---[2207]---> BDD-cost:  134
c ---[2206]---> BDD-cost:  134
c ---[2205]---> BDD-cost:  128
c ---[2204]---> BDD-cost:  128
c ---[2203]---> BDD-cost:  131
c ---[2202]---> BDD-cost:  131
c ---[2201]---> BDD-cost:  128
c ---[2200]---> BDD-cost:  128
c ---[2199]---> BDD-cost:  131
c ---[2197]---> BDD-cost:  131
c ---[2196]---> BDD-cost:  128
c ---[2195]---> BDD-cost:  128
c ---[2194]---> BDD-cost:  134
c ---[2193]---> BDD-cost:  134
c ---[2192]---> BDD-cost:  128
c ---[2191]---> BDD-cost:  128
c ---[2190]---> BDD-cost:  134
c ---[2189]---> BDD-cost:  134
c ---[2188]---> BDD-cost:  128
c ---[2186]---> BDD-cost:  128
c ---[2185]---> BDD-cost:  126
c ---[2184]---> BDD-cost:  126
c ---[2183]---> BDD-cost:  128
c ---[2182]---> BDD-cost:  128
c ---[2181]---> BDD-cost:  125
c ---[2180]---> BDD-cost:  134
c ---[2179]---> BDD-cost:  120
c ---[2178]---> BDD-cost:  127
c ---[2177]---> BDD-cost:  115
c ---[2175]---> BDD-cost:  132
c ---[2174]---> BDD-cost:  117
c ---[2173]---> BDD-cost:  129
c ---[2172]---> BDD-cost:  115
c ---[2171]---> BDD-cost:  134
c ---[2170]---> BDD-cost:  128
c ---[2169]---> BDD-cost:  116
c ---[2168]---> BDD-cost:  120
c ---[2167]---> BDD-cost:  131
c ---[2166]---> BDD-cost:  125
c ---[2164]---> BDD-cost:  131
c ---[2163]---> BDD-cost:  123
c ---[2162]---> BDD-cost:  131
c ---[2161]---> BDD-cost:  123
c ---[2160]---> BDD-cost:  134
c ---[2159]---> BDD-cost:  123
c ---[2158]---> BDD-cost:  126
c ---[2157]---> BDD-cost:  123
c ---[2156]---> BDD-cost:  128
c ---[2155]---> BDD-cost:  117
c ---[2153]---> BDD-cost:  134
c ---[2152]---> BDD-cost:  123
c ---[2151]---> BDD-cost:  126
c ---[2150]---> BDD-cost:  118
c ---[2149]---> BDD-cost:  134
c ---[2148]---> BDD-cost:  128
c ---[2147]---> BDD-cost:  134
c ---[2146]---> BDD-cost:  111
c ---[2145]---> BDD-cost:  137
c ---[2144]---> BDD-cost:  123
c ---[2141]---> BDD-cost:  127
c ---[2140]---> BDD-cost:  123
c ---[2139]---> BDD-cost:  126
c ---[2138]---> BDD-cost:  128
c ---[2137]---> BDD-cost:  134
c ---[2136]---> BDD-cost:  115
c ---[2135]---> BDD-cost:  134
c ---[2134]---> BDD-cost:  122
c ---[2133]---> BDD-cost:  123
c ---[2132]---> BDD-cost:  115
c ---[2130]---> BDD-cost:  124
c ---[2129]---> BDD-cost:  117
c ---[2128]---> BDD-cost:  131
c ---[2127]---> BDD-cost:  111
c ---[2126]---> BDD-cost:  114
c ---[2125]---> BDD-cost:  117
c ---[2124]---> BDD-cost:  132
c ---[2123]---> BDD-cost:  128
c ---[2122]---> BDD-cost:  119
c ---[2121]---> BDD-cost:  128
c ---[2119]---> BDD-cost:  137
c ---[2118]---> BDD-cost:  123
c ---[2117]---> BDD-cost:  137
c ---[2116]---> BDD-cost:  111
c ---[2115]---> BDD-cost:  131
c ---[2114]---> BDD-cost:  128
c ---[2113]---> BDD-cost:  134
c ---[2112]---> BDD-cost:  128
c ---[2111]---> BDD-cost:  129
c ---[2110]---> BDD-cost:  128
c ---[2108]---> BDD-cost:  129
c ---[2107]---> BDD-cost:  123
c ---[2106]---> BDD-cost:  134
c ---[2105]---> BDD-cost:  125
c ---[2104]---> BDD-cost:  128
c ---[2103]---> BDD-cost:  128
c ---[2102]---> BDD-cost:  107
c ---[2101]---> BDD-cost:  125
c ---[2100]---> BDD-cost:  132
c ---[2099]---> BDD-cost:  113
c ---[2097]---> BDD-cost:  126
c ---[2096]---> BDD-cost:  111
c ---[2095]---> BDD-cost:  134
c ---[2094]---> BDD-cost:  128
c ---[2093]---> BDD-cost:  134
c ---[2092]---> BDD-cost:  117
c ---[2091]---> BDD-cost:  116
c ---[2090]---> BDD-cost:  115
c ---[2089]---> BDD-cost:  131
c ---[2088]---> BDD-cost:  122
c ---[2086]---> BDD-cost:  124
c ---[2085]---> BDD-cost:  118
c ---[2084]---> BDD-cost:  117
c ---[2083]---> BDD-cost:  118
c ---[2082]---> BDD-cost:  134
c ---[2081]---> BDD-cost:  113
c ---[2080]---> BDD-cost:  134
c ---[2079]---> BDD-cost:  123
c ---[2078]---> BDD-cost:  128
c ---[2077]---> BDD-cost:  125
c ---[2075]---> BDD-cost:  125
c ---[2074]---> BDD-cost:  117
c ---[2073]---> BDD-cost:  134
c ---[2072]---> BDD-cost:  115
c ---[2071]---> BDD-cost:  111
c ---[2070]---> BDD-cost:  118
c ---[2069]---> BDD-cost:  134
c ---[2068]---> BDD-cost:  111
c ---[2067]---> BDD-cost:  129
c ---[2066]---> BDD-cost:  128
c ---[2064]---> BDD-cost:  131
c ---[2063]---> BDD-cost:  120
c ---[2062]---> BDD-cost:  129
c ---[2061]---> BDD-cost:  117
c ---[2060]---> BDD-cost:  134
c ---[2059]---> BDD-cost:  122
c ---[2058]---> BDD-cost:  134
c ---[2057]---> BDD-cost:  120
c ---[2056]---> BDD-cost:  131
c ---[2055]---> BDD-cost:  122
c ---[2053]---> BDD-cost:  134
c ---[2052]---> BDD-cost:  122
c ---[2051]---> BDD-cost:  114
c ---[2050]---> BDD-cost:  131
c ---[2049]---> BDD-cost:  131
c ---[2048]---> BDD-cost:  126
c ---[2047]---> BDD-cost:  120
c ---[2046]---> BDD-cost:  134
c ---[2045]---> BDD-cost:  113
c ---[2044]---> BDD-cost:  124
c ---[2042]---> BDD-cost:  128
c ---[2041]---> BDD-cost:  132
c ---[2040]---> BDD-cost:  125
c ---[2039]---> BDD-cost:  134
c ---[2038]---> BDD-cost:  111
c ---[2037]---> BDD-cost:  116
c ---[2036]---> BDD-cost:  128
c ---[2035]---> BDD-cost:  124
c ---[2034]---> BDD-cost:  128
c ---[2033]---> BDD-cost:  122
c ---[2029]---> BDD-cost:  122
c ---[2028]---> BDD-cost:  128
c ---[2027]---> BDD-cost:  115
c ---[2026]---> BDD-cost:  127
c ---[2025]---> BDD-cost:  118
c ---[2024]---> BDD-cost:  124
c ---[2023]---> BDD-cost:  118
c ---[2022]---> BDD-cost:  137
c ---[2021]---> BDD-cost:  123
c ---[2020]---> BDD-cost:  132
c ---[2018]---> BDD-cost:  123
c ---[2017]---> BDD-cost:  121
c ---[2016]---> BDD-cost:  128
c ---[2015]---> BDD-cost:  131
c ---[2014]---> BDD-cost:  120
c ---[2013]---> BDD-cost:  134
c ---[2012]---> BDD-cost:  123
c ---[2011]---> BDD-cost:  129
c ---[2010]---> BDD-cost:  120
c ---[2009]---> BDD-cost:  127
c ---[2007]---> BDD-cost:  128
c ---[2006]---> BDD-cost:  129
c ---[2005]---> BDD-cost:  128
c ---[2004]---> BDD-cost:  137
c ---[2003]---> BDD-cost:  123
c ---[2002]---> BDD-cost:  137
c ---[2001]---> BDD-cost:  128
c ---[2000]---> BDD-cost:  132
c ---[1999]---> BDD-cost:  128
c ---[1998]---> BDD-cost:  114
c ---[1996]---> BDD-cost:  111
c ---[1995]---> BDD-cost:  134
c ---[1994]---> BDD-cost:  125
c ---[1993]---> BDD-cost:  137
c ---[1992]---> BDD-cost:  115
c ---[1991]---> BDD-cost:  121
c ---[1990]---> BDD-cost:  125
c ---[1989]---> BDD-cost:  132
c ---[1988]---> BDD-cost:  128
c ---[1987]---> BDD-cost:  132
c ---[1985]---> BDD-cost:  123
c ---[1984]---> BDD-cost:  132
c ---[1983]---> BDD-cost:  123
c ---[1982]---> BDD-cost:  137
c ---[1981]---> BDD-cost:  128
c ---[1980]---> BDD-cost:  137
c ---[1979]---> BDD-cost:  131
c ---[1978]---> BDD-cost:  131
c ---[1977]---> BDD-cost:  134
c ---[1976]---> BDD-cost:  111
c ---[1974]---> BDD-cost:  129
c ---[1973]---> BDD-cost:  125
c ---[1972]---> BDD-cost:  122
c ---[1971]---> BDD-cost:  120
c ---[1970]---> BDD-cost:  134
c ---[1969]---> BDD-cost:  125
c ---[1968]---> BDD-cost:  137
c ---[1967]---> BDD-cost:  128
c ---[1966]---> BDD-cost:  137
c ---[1965]---> BDD-cost:  111
c ---[1963]---> BDD-cost:  137
c ---[1962]---> BDD-cost:  113
c ---[1961]---> BDD-cost:  132
c ---[1960]---> BDD-cost:  131
c ---[1959]---> BDD-cost:  131
c ---[1958]---> BDD-cost:  132
c ---[1957]---> BDD-cost:  111
c ---[1956]---> BDD-cost:  129
c ---[1955]---> BDD-cost:  125
c ---[1954]---> BDD-cost:  123
c ---[1952]---> BDD-cost:  120
c ---[1951]---> BDD-cost:  134
c ---[1950]---> BDD-cost:  125
c ---[1949]---> BDD-cost:  125
c ---[1948]---> BDD-cost:  128
c ---[1947]---> BDD-cost:  137
c ---[1946]---> BDD-cost:  111
c ---[1945]---> BDD-cost:  128
c ---[1944]---> BDD-cost:  113
c ---[1943]---> BDD-cost:  119
c ---[1941]---> BDD-cost:  131
c ---[1940]---> BDD-cost:  131
c ---[1939]---> BDD-cost:  129
c ---[1938]---> BDD-cost:  122
c ---[1937]---> BDD-cost:  131
c ---[1936]---> BDD-cost:  115
c ---[1935]---> BDD-cost:  129
c ---[1934]---> BDD-cost:  122
c ---[1933]---> BDD-cost:  123
c ---[1932]---> BDD-cost:  111
c ---[1930]---> BDD-cost:  117
c ---[1929]---> BDD-cost:  111
c ---[1928]---> BDD-cost:  129
c ---[1927]---> BDD-cost:  123
c ---[1926]---> BDD-cost:  137
c ---[1925]---> BDD-cost:  128
c ---[1924]---> BDD-cost:  134
c ---[1923]---> BDD-cost:  128
c ---[1922]---> BDD-cost:  129
c ---[1921]---> BDD-cost:  117
c ---[1918]---> BDD-cost:  137
c ---[1917]---> BDD-cost:  128
c ---[1916]---> BDD-cost:  134
c ---[1915]---> BDD-cost:  128
c ---[1914]---> BDD-cost:  122
c ---[1913]---> BDD-cost:  123
c ---[1912]---> BDD-cost:  129
c ---[1911]---> BDD-cost:  117
c ---[1910]---> BDD-cost:  116
c ---[1909]---> BDD-cost:  122
c ---[1907]---> BDD-cost:  121
c ---[1906]---> BDD-cost:  128
c ---[1905]---> BDD-cost:  125
c ---[1904]---> BDD-cost:  131
c ---[1903]---> BDD-cost:  131
c ---[1902]---> BDD-cost:  134
c ---[1901]---> BDD-cost:  128
c ---[1900]---> BDD-cost:  121
c ---[1899]---> BDD-cost:  115
c ---[1898]---> BDD-cost:  129
c ---[1896]---> BDD-cost:  113
c ---[1895]---> BDD-cost:  129
c ---[1894]---> BDD-cost:  120
c ---[1893]---> BDD-cost:  109
c ---[1892]---> BDD-cost:  128
c ---[1891]---> BDD-cost:  134
c ---[1890]---> BDD-cost:  111
c ---[1889]---> BDD-cost:  137
c ---[1888]---> BDD-cost:  117
c ---[1887]---> BDD-cost:  134
c ---[1885]---> BDD-cost:  115
c ---[1884]---> BDD-cost:  134
c ---[1883]---> BDD-cost:  111
c ---[1882]---> BDD-cost:  129
c ---[1881]---> BDD-cost:  128
c ---[1880]---> BDD-cost:  134
c ---[1879]---> BDD-cost:  122
c ---[1878]---> BDD-cost:  137
c ---[1877]---> BDD-cost:  115
c ---[1876]---> BDD-cost:  131
c ---[1874]---> BDD-cost:  122
c ---[1873]---> BDD-cost:  134
c ---[1872]---> BDD-cost:  131
c ---[1871]---> BDD-cost:  131
c ---[1870]---> BDD-cost:  127
c ---[1869]---> BDD-cost:  123
c ---[1868]---> BDD-cost:  137
c ---[1867]---> BDD-cost:  117
c ---[1866]---> BDD-cost:  134
c ---[1865]---> BDD-cost:  128
c ---[1863]---> BDD-cost:  126
c ---[1862]---> BDD-cost:  120
c ---[1861]---> BDD-cost:  131
c ---[1860]---> BDD-cost:  128
c ---[1859]---> BDD-cost:  111
c ---[1858]---> BDD-cost:  118
c ---[1857]---> BDD-cost:  121
c ---[1856]---> BDD-cost:  128
c ---[1855]---> BDD-cost:  126
c ---[1854]---> BDD-cost:  120
c ---[1852]---> BDD-cost:  131
c ---[1851]---> BDD-cost:  125
c ---[1850]---> BDD-cost:  126
c ---[1849]---> BDD-cost:  120
c ---[1848]---> BDD-cost:  123
c ---[1847]---> BDD-cost:  123
c ---[1846]---> BDD-cost:  119
c ---[1845]---> BDD-cost:  128
c ---[1844]---> BDD-cost:  126
c ---[1843]---> BDD-cost:  128
c ---[1841]---> BDD-cost:  134
c ---[1840]---> BDD-cost:  111
c ---[1839]---> BDD-cost:  134
c ---[1838]---> BDD-cost:  122
c ---[1837]---> BDD-cost:  126
c ---[1836]---> BDD-cost:  123
c ---[1835]---> BDD-cost:  131
c ---[1834]---> BDD-cost:  113
c ---[1833]---> BDD-cost:  115
c ---[1832]---> BDD-cost:  122
c ---[1830]---> BDD-cost:  118
c ---[1829]---> BDD-cost:  128
c ---[1828]---> BDD-cost:  126
c ---[1827]---> BDD-cost:  111
c ---[1826]---> BDD-cost:  125
c ---[1825]---> BDD-cost:  128
c ---[1824]---> BDD-cost:  123
c ---[1823]---> BDD-cost:  120
c ---[1822]---> BDD-cost:  120
c ---[1821]---> BDD-cost:  111
c ---[1819]---> BDD-cost:  113
c ---[1818]---> BDD-cost:  128
c ---[1817]---> BDD-cost:  123
c ---[1816]---> BDD-cost:  118
c ---[1815]---> BDD-cost:  131
c ---[1814]---> BDD-cost:  111
c ---[1813]---> BDD-cost:  121
c ---[1812]---> BDD-cost:  128
c ---[1811]---> BDD-cost:  126
c ---[1810]---> BDD-cost:  128
c ---[1807]---> BDD-cost:  131
c ---[1806]---> BDD-cost:  123
c ---[1805]---> BDD-cost:  131
c ---[1804]---> BDD-cost:  123
c ---[1803]---> BDD-cost:  131
c ---[1802]---> BDD-cost:  117
c ---[1801]---> BDD-cost:  126
c ---[1800]---> BDD-cost:  113
c ---[1799]---> BDD-cost:  124
c ---[1798]---> BDD-cost:  123
c ---[1796]---> BDD-cost:  121
c ---[1795]---> BDD-cost:  128
c ---[1794]---> BDD-cost:  121
c ---[1793]---> BDD-cost:  115
c ---[1792]---> BDD-cost:  126
c ---[1791]---> BDD-cost:  128
c ---[1790]---> BDD-cost:  115
c ---[1789]---> BDD-cost:  123
c ---[1788]---> BDD-cost:  119
c ---[1787]---> BDD-cost:  115
c ---[1785]---> BDD-cost:  125
c ---[1784]---> BDD-cost:  125
c ---[1783]---> BDD-cost:  125
c ---[1782]---> BDD-cost:  125
c ---[1781]---> BDD-cost:  134
c ---[1780]---> BDD-cost:  122
c ---[1779]---> BDD-cost:  132
c ---[1778]---> BDD-cost:  115
c ---[1777]---> BDD-cost:  124
c ---[1776]---> BDD-cost:  125
c ---[1774]---> BDD-cost:  124
c ---[1773]---> BDD-cost:  115
c ---[1772]---> BDD-cost:  124
c ---[1771]---> BDD-cost:  128
c ---[1770]---> BDD-cost:  125
c ---[1769]---> BDD-cost:  128
c ---[1768]---> BDD-cost:  131
c ---[1767]---> BDD-cost:  128
c ---[1766]---> BDD-cost:  131
c ---[1765]---> BDD-cost:  125
c ---[1763]---> BDD-cost:  118
c ---[1762]---> BDD-cost:  128
c ---[1761]---> BDD-cost:  134
c ---[1760]---> BDD-cost:  122
c ---[1759]---> BDD-cost:  123
c ---[1758]---> BDD-cost:  113
c ---[1757]---> BDD-cost:  137
c ---[1756]---> BDD-cost:  113
c ---[1755]---> BDD-cost:  135
c ---[1754]---> BDD-cost:  118
c ---[1752]---> BDD-cost:  129
c ---[1751]---> BDD-cost:  122
c ---[1750]---> BDD-cost:  137
c ---[1749]---> BDD-cost:  111
c ---[1748]---> BDD-cost:  125
c ---[1747]---> BDD-cost:  123
c ---[1746]---> BDD-cost:  122
c ---[1745]---> BDD-cost:  128
c ---[1744]---> BDD-cost:  127
c ---[1743]---> BDD-cost:  127
c ---[1741]---> BDD-cost:  128
c ---[1740]---> BDD-cost:  113
c ---[1739]---> BDD-cost:  115
c ---[1738]---> BDD-cost:  129
c ---[1737]---> BDD-cost:  117
c ---[1736]---> BDD-cost:  134
c ---[1735]---> BDD-cost:  123
c ---[1734]---> BDD-cost:  131
c ---[1733]---> BDD-cost:  128
c ---[1732]---> BDD-cost:  128
c ---[1730]---> BDD-cost:  128
c ---[1729]---> BDD-cost:  120
c ---[1728]---> BDD-cost:  118
c ---[1727]---> BDD-cost:  120
c ---[1726]---> BDD-cost:  118
c ---[1725]---> BDD-cost:  124
c ---[1724]---> BDD-cost:  131
c ---[1723]---> BDD-cost:  131
c ---[1722]---> BDD-cost:  129
c ---[1721]---> BDD-cost:  117
c ---[1719]---> BDD-cost:  121
c ---[1718]---> BDD-cost:  122
c ---[1717]---> BDD-cost:  121
c ---[1716]---> BDD-cost:  113
c ---[1715]---> BDD-cost:  129
c ---[1714]---> BDD-cost:  125
c ---[1713]---> BDD-cost:  137
c ---[1712]---> BDD-cost:  125
c ---[1711]---> BDD-cost:  119
c ---[1710]---> BDD-cost:  125
c ---[1708]---> BDD-cost:  111
c ---[1707]---> BDD-cost:  115
c ---[1706]---> BDD-cost:  129
c ---[1705]---> BDD-cost:  128
c ---[1704]---> BDD-cost:  126
c ---[1703]---> BDD-cost:  128
c ---[1702]---> BDD-cost:  131
c ---[1701]---> BDD-cost:  128
c ---[1700]---> BDD-cost:  119
c ---[1699]---> BDD-cost:  117
c ---[1696]---> BDD-cost:  131
c ---[1695]---> BDD-cost:  125
c ---[1694]---> BDD-cost:  131
c ---[1693]---> BDD-cost:  117
c ---[1692]---> BDD-cost:  126
c ---[1691]---> BDD-cost:  111
c ---[1690]---> BDD-cost:  137
c ---[1689]---> BDD-cost:  111
c ---[1688]---> BDD-cost:  128
c ---[1687]---> BDD-cost:  128
c ---[1685]---> BDD-cost:  134
c ---[1684]---> BDD-cost:  131
c ---[1683]---> BDD-cost:  131
c ---[1682]---> BDD-cost:  128
c ---[1681]---> BDD-cost:  123
c ---[1680]---> BDD-cost:  134
c ---[1679]---> BDD-cost:  128
c ---[1678]---> BDD-cost:  131
c ---[1677]---> BDD-cost:  122
c ---[1676]---> BDD-cost:  132
c ---[1674]---> BDD-cost:  118
c ---[1673]---> BDD-cost:  129
c ---[1672]---> BDD-cost:  125
c ---[1671]---> BDD-cost:  131
c ---[1670]---> BDD-cost:  123
c ---[1669]---> BDD-cost:  115
c ---[1668]---> BDD-cost:  131
c ---[1667]---> BDD-cost:  131
c ---[1666]---> BDD-cost:  127
c ---[1665]---> BDD-cost:  128
c ---[1663]---> BDD-cost:  118
c ---[1662]---> BDD-cost:  113
c ---[1661]---> BDD-cost:  120
c ---[1660]---> BDD-cost:  128
c ---[1659]---> BDD-cost:  137
c ---[1658]---> BDD-cost:  113
c ---[1657]---> BDD-cost:  134
c ---[1656]---> BDD-cost:  111
c ---[1655]---> BDD-cost:  124
c ---[1654]---> BDD-cost:  123
c ---[1652]---> BDD-cost:  132
c ---[1651]---> BDD-cost:  132
c ---[1650]---> BDD-cost:  122
c ---[1649]---> BDD-cost:  137
c ---[1648]---> BDD-cost:  122
c ---[1647]---> BDD-cost:  134
c ---[1646]---> BDD-cost:  117
c ---[1645]---> BDD-cost:  134
c ---[1644]---> BDD-cost:  123
c ---[1643]---> BDD-cost:  119
c ---[1641]---> BDD-cost:  120
c ---[1640]---> BDD-cost:  126
c ---[1639]---> BDD-cost:  120
c ---[1638]---> BDD-cost:  131
c ---[1637]---> BDD-cost:  115
c ---[1636]---> BDD-cost:  134
c ---[1635]---> BDD-cost:  125
c ---[1634]---> BDD-cost:  125
c ---[1633]---> BDD-cost:  117
c ---[1632]---> BDD-cost:  134
c ---[1630]---> BDD-cost:  128
c ---[1629]---> BDD-cost:  114
c ---[1628]---> BDD-cost:  125
c ---[1627]---> BDD-cost:  134
c ---[1626]---> BDD-cost:  113
c ---[1625]---> BDD-cost:  126
c ---[1624]---> BDD-cost:  128
c ---[1623]---> BDD-cost:  137
c ---[1622]---> BDD-cost:  111
c ---[1621]---> BDD-cost:  137
c ---[1619]---> BDD-cost:  123
c ---[1618]---> BDD-cost:  140
c ---[1617]---> BDD-cost:  122
c ---[1616]---> BDD-cost:  132
c ---[1615]---> BDD-cost:  128
c ---[1614]---> BDD-cost:  121
c ---[1613]---> BDD-cost:  123
c ---[1612]---> BDD-cost:  116
c ---[1611]---> BDD-cost:  113
c ---[1610]---> BDD-cost:  117
c ---[1608]---> BDD-cost:  113
c ---[1607]---> BDD-cost:  109
c ---[1606]---> BDD-cost:  128
c ---[1605]---> BDD-cost:  121
c ---[1604]---> BDD-cost:  117
c ---[1603]---> BDD-cost:  134
c ---[1602]---> BDD-cost:  117
c ---[1601]---> BDD-cost:  131
c ---[1600]---> BDD-cost:  122
c ---[1599]---> BDD-cost:  131
c ---[1597]---> BDD-cost:  113
c ---[1596]---> BDD-cost:  134
c ---[1595]---> BDD-cost:  125
c ---[1594]---> BDD-cost:  132
c ---[1593]---> BDD-cost:  125
c ---[1592]---> BDD-cost:  134
c ---[1591]---> BDD-cost:  117
c ---[1590]---> BDD-cost:  124
c ---[1589]---> BDD-cost:  125
c ---[1588]---> BDD-cost:  137
c ---[1585]---> BDD-cost:  111
c ---[1584]---> BDD-cost:  137
c ---[1583]---> BDD-cost:  128
c ---[1582]---> BDD-cost:  137
c ---[1581]---> BDD-cost:  111
c ---[1580]---> BDD-cost:  137
c ---[1579]---> BDD-cost:  128
c ---[1578]---> BDD-cost:  129
c ---[1577]---> BDD-cost:  123
c ---[1576]---> BDD-cost:  121
c ---[1574]---> BDD-cost:  128
c ---[1573]---> BDD-cost:  137
c ---[1572]---> BDD-cost:  120
c ---[1571]---> BDD-cost:  131
c ---[1570]---> BDD-cost:  117
c ---[1569]---> BDD-cost:  122
c ---[1568]---> BDD-cost:  125
c ---[1567]---> BDD-cost:  128
c ---[1566]---> BDD-cost:  131
c ---[1565]---> BDD-cost:  131
c ---[1563]---> BDD-cost:  128
c ---[1562]---> BDD-cost:  128
c ---[1561]---> BDD-cost:  132
c ---[1560]---> BDD-cost:  123
c ---[1559]---> BDD-cost:  137
c ---[1558]---> BDD-cost:  137
c ---[1557]---> BDD-cost:  128
c ---[1556]---> BDD-cost:  137
c ---[1555]---> BDD-cost:  122
c ---[1554]---> BDD-cost:  121
c ---[1552]---> BDD-cost:  131
c ---[1551]---> BDD-cost:  131
c ---[1550]---> BDD-cost:  129
c ---[1549]---> BDD-cost:  113
c ---[1548]---> BDD-cost:  134
c ---[1547]---> BDD-cost:  128
c ---[1546]---> BDD-cost:  137
c ---[1545]---> BDD-cost:  113
c ---[1544]---> BDD-cost:  134
c ---[1543]---> BDD-cost:  128
c ---[1541]---> BDD-cost:  129
c ---[1540]---> BDD-cost:  118
c ---[1539]---> BDD-cost:  132
c ---[1538]---> BDD-cost:  125
c ---[1537]---> BDD-cost:  131
c ---[1536]---> BDD-cost:  113
c ---[1535]---> BDD-cost:  124
c ---[1534]---> BDD-cost:  128
c ---[1533]---> BDD-cost:  124
c ---[1532]---> BDD-cost:  131
c ---[1530]---> BDD-cost:  131
c ---[1529]---> BDD-cost:  137
c ---[1528]---> BDD-cost:  128
c ---[1527]---> BDD-cost:  132
c ---[1526]---> BDD-cost:  123
c ---[1525]---> BDD-cost:  132
c ---[1524]---> BDD-cost:  123
c ---[1523]---> BDD-cost:  134
c ---[1522]---> BDD-cost:  118
c ---[1521]---> BDD-cost:  137
c ---[1519]---> BDD-cost:  128
c ---[1518]---> BDD-cost:  124
c ---[1517]---> BDD-cost:  123
c ---[1516]---> BDD-cost:  109
c ---[1515]---> BDD-cost:  123
c ---[1514]---> BDD-cost:  131
c ---[1513]---> BDD-cost:  123
c ---[1512]---> BDD-cost:  129
c ---[1511]---> BDD-cost:  122
c ---[1510]---> BDD-cost:  137
c ---[1508]---> BDD-cost:  118
c ---[1507]---> BDD-cost:  131
c ---[1506]---> BDD-cost:  118
c ---[1505]---> BDD-cost:  132
c ---[1504]---> BDD-cost:  128
c ---[1503]---> BDD-cost:  127
c ---[1502]---> BDD-cost:  118
c ---[1501]---> BDD-cost:  118
c ---[1500]---> BDD-cost:  122
c ---[1499]---> BDD-cost:  129
c ---[1497]---> BDD-cost:  118
c ---[1496]---> BDD-cost:  131
c ---[1495]---> BDD-cost:  118
c ---[1494]---> BDD-cost:  134
c ---[1493]---> BDD-cost:  113
c ---[1492]---> BDD-cost:  131
c ---[1491]---> BDD-cost:  122
c ---[1490]---> BDD-cost:  127
c ---[1489]---> BDD-cost:  125
c ---[1488]---> BDD-cost:  128
c ---[1486]---> BDD-cost:  113
c ---[1485]---> BDD-cost:  132
c ---[1484]---> BDD-cost:  123
c ---[1483]---> BDD-cost:  119
c ---[1482]---> BDD-cost:  118
c ---[1481]---> BDD-cost:  123
c ---[1480]---> BDD-cost:  120
c ---[1479]---> BDD-cost:  137
c ---[1478]---> BDD-cost:  122
c ---[1477]---> BDD-cost:  137
c ---[1474]---> BDD-cost:  120
c ---[1473]---> BDD-cost:  137
c ---[1472]---> BDD-cost:  123
c ---[1471]---> BDD-cost:  132
c ---[1470]---> BDD-cost:  117
c ---[1469]---> BDD-cost:  129
c ---[1468]---> BDD-cost:  125
c ---[1467]---> BDD-cost:  129
c ---[1466]---> BDD-cost:  111
c ---[1465]---> BDD-cost:  132
c ---[1463]---> BDD-cost:  128
c ---[1462]---> BDD-cost:  134
c ---[1461]---> BDD-cost:  115
c ---[1460]---> BDD-cost:  134
c ---[1459]---> BDD-cost:  113
c ---[1458]---> BDD-cost:  127
c ---[1457]---> BDD-cost:  123
c ---[1456]---> BDD-cost:  134
c ---[1455]---> BDD-cost:  131
c ---[1454]---> BDD-cost:  131
c ---[1452]---> BDD-cost:  134
c ---[1451]---> BDD-cost:  128
c ---[1450]---> BDD-cost:  118
c ---[1449]---> BDD-cost:  113
c ---[1448]---> BDD-cost:  137
c ---[1447]---> BDD-cost:  123
c ---[1446]---> BDD-cost:  134
c ---[1252]---> BDD-cost:  116
c ---[1251]---> BDD-cost:  110
c ---[1250]---> BDD-cost:   79
c ---[1248]---> BDD-cost:   79
c ---[1247]---> BDD-cost:   79
c ---[1246]---> BDD-cost:   79
c ---[1245]---> BDD-cost:  114
c ---[1244]---> BDD-cost:  110
c ---[1243]---> BDD-cost:   79
c ---[1242]---> BDD-cost:   79
c ---[1241]---> BDD-cost:   79
c ---[1240]---> BDD-cost:   79
c ---[1239]---> BDD-cost:  116
c ---[1237]---> BDD-cost:  110
c ---[1236]---> BDD-cost:   79
c ---[1235]---> BDD-cost:   79
c ---[1234]---> BDD-cost:   79
c ---[1233]---> BDD-cost:   79
c ---[1232]---> BDD-cost:  106
c ---[1231]---> BDD-cost:  110
c ---[1230]---> BDD-cost:   79
c ---[1229]---> BDD-cost:   79
c ---[1228]---> BDD-cost:   79
c ---[1226]---> BDD-cost:   79
c ---[1225]---> BDD-cost:  116
c ---[1224]---> BDD-cost:  110
c ---[1223]---> BDD-cost:   79
c ---[1222]---> BDD-cost:   79
c ---[1221]---> BDD-cost:   79
c ---[1220]---> BDD-cost:   79
c ---[1219]---> BDD-cost:  114
c ---[1218]---> BDD-cost:  110
c ---[1217]---> BDD-cost:   79
c ---[1215]---> BDD-cost:   79
c ---[1214]---> BDD-cost:   79
c ---[1213]---> BDD-cost:   79
c ---[1212]---> BDD-cost:  116
c ---[1211]---> BDD-cost:  110
c ---[1210]---> BDD-cost:   79
c ---[1209]---> BDD-cost:   79
c ---[1208]---> BDD-cost:   79
c ---[1207]---> BDD-cost:   79
c ---[1206]---> BDD-cost:  114
c ---[1204]---> BDD-cost:  110
c ---[1203]---> BDD-cost:   79
c ---[1202]---> BDD-cost:   79
c ---[1201]---> BDD-cost:   79
c ---[1200]---> BDD-cost:   79
c ---[1199]---> BDD-cost:  112
c ---[1198]---> BDD-cost:  110
c ---[1197]---> BDD-cost:   79
c ---[1196]---> BDD-cost:   79
c ---[1195]---> BDD-cost:   79
c ---[1193]---> BDD-cost:   79
c ---[1192]---> BDD-cost:  116
c ---[1191]---> BDD-cost:  110
c ---[1190]---> BDD-cost:   79
c ---[1189]---> BDD-cost:   79
c ---[1188]---> BDD-cost:   79
c ---[1187]---> BDD-cost:   79
c ---[1186]---> BDD-cost:  114
c ---[1185]---> BDD-cost:  110
c ---[1184]---> BDD-cost:   79
c ---[1182]---> BDD-cost:   79
c ---[1181]---> BDD-cost:   79
c ---[1180]---> BDD-cost:   79
c ---[1179]---> BDD-cost:  116
c ---[1178]---> BDD-cost:  110
c ---[1177]---> BDD-cost:   79
c ---[1176]---> BDD-cost:   79
c ---[1175]---> BDD-cost:   79
c ---[1174]---> BDD-cost:   79
c ---[1173]---> BDD-cost:  116
c ---[1170]---> BDD-cost:  110
c ---[1169]---> BDD-cost:   79
c ---[1168]---> BDD-cost:   79
c ---[1167]---> BDD-cost:   79
c ---[1166]---> BDD-cost:   79
c ---[1165]---> BDD-cost:  114
c ---[1164]---> BDD-cost:  110
c ---[1163]---> BDD-cost:   79
c ---[1162]---> BDD-cost:   79
c ---[1161]---> BDD-cost:   79
c ---[1159]---> BDD-cost:   79
c ---[1158]---> BDD-cost:  106
c ---[1157]---> BDD-cost:  110
c ---[1156]---> BDD-cost:   79
c ---[1155]---> BDD-cost:   79
c ---[1154]---> BDD-cost:   79
c ---[1153]---> BDD-cost:   79
c ---[1152]---> BDD-cost:  114
c ---[1151]---> BDD-cost:  110
c ---[1150]---> BDD-cost:   79
c ---[1148]---> BDD-cost:   79
c ---[1147]---> BDD-cost:   79
c ---[1146]---> BDD-cost:   79
c ---[1145]---> BDD-cost:  110
c ---[1144]---> BDD-cost:  110
c ---[1143]---> BDD-cost:   79
c ---[1142]---> BDD-cost:   79
c ---[1141]---> BDD-cost:   79
c ---[1140]---> BDD-cost:   79
c ---[1139]---> BDD-cost:  116
c ---[1137]---> BDD-cost:  110
c ---[1136]---> BDD-cost:   79
c ---[1135]---> BDD-cost:   79
c ---[1134]---> BDD-cost:   79
c ---[1133]---> BDD-cost:   79
c ---[1132]---> BDD-cost:  110
c ---[1131]---> BDD-cost:  110
c ---[1130]---> BDD-cost:   79
c ---[1129]---> BDD-cost:   79
c ---[1128]---> BDD-cost:   79
c ---[1126]---> BDD-cost:   79
c ---[1125]---> BDD-cost:  114
c ---[1124]---> BDD-cost:  110
c ---[1123]---> BDD-cost:   79
c ---[1122]---> BDD-cost:   79
c ---[1121]---> BDD-cost:   79
c ---[1120]---> BDD-cost:   79
c ---[1119]---> BDD-cost:  116
c ---[1118]---> BDD-cost:  110
c ---[1117]---> BDD-cost:   79
c ---[1115]---> BDD-cost:   79
c ---[1114]---> BDD-cost:   79
c ---[1113]---> BDD-cost:   79
c ---[1112]---> BDD-cost:  112
c ---[1111]---> BDD-cost:  110
c ---[1110]---> BDD-cost:   79
c ---[1109]---> BDD-cost:   79
c ---[1108]---> BDD-cost:   79
c ---[1107]---> BDD-cost:   79
c ---[1106]---> BDD-cost:  114
c ---[1104]---> BDD-cost:  110
c ---[1103]---> BDD-cost:   79
c ---[1102]---> BDD-cost:   79
c ---[1101]---> BDD-cost:   79
c ---[1100]---> BDD-cost:   79
c ---[1099]---> BDD-cost:  110
c ---[1098]---> BDD-cost:  110
c ---[1097]---> BDD-cost:   79
c ---[1096]---> BDD-cost:   79
c ---[1095]---> BDD-cost:   79
c ---[1093]---> BDD-cost:   79
c ---[1092]---> BDD-cost:  114
c ---[1091]---> BDD-cost:  110
c ---[1090]---> BDD-cost:   79
c ---[1089]---> BDD-cost:   79
c ---[1088]---> BDD-cost:   79
c ---[1087]---> BDD-cost:   79
c ---[1086]---> BDD-cost:  112
c ---[1085]---> BDD-cost:  110
c ---[1084]---> BDD-cost:   79
c ---[1082]---> BDD-cost:   79
c ---[1081]---> BDD-cost:   79
c ---[1080]---> BDD-cost:   79
c ---[1079]---> BDD-cost:  114
c ---[1078]---> BDD-cost:  110
c ---[1077]---> BDD-cost:   79
c ---[1076]---> BDD-cost:   79
c ---[1075]---> BDD-cost:   79
c ---[1074]---> BDD-cost:   79
c ---[1073]---> BDD-cost:  114
c ---[1071]---> BDD-cost:  110
c ---[1070]---> BDD-cost:   79
c ---[1069]---> BDD-cost:   79
c ---[1068]---> BDD-cost:   79
c ---[1067]---> BDD-cost:   79
c ---[1066]---> BDD-cost:  112
c ---[1065]---> BDD-cost:  110
c ---[1064]---> BDD-cost:   79
c ---[1063]---> BDD-cost:   79
c ---[1062]---> BDD-cost:   79
c ---[1059]---> BDD-cost:   79
c ---[1058]---> BDD-cost:  114
c ---[1057]---> BDD-cost:  110
c ---[1056]---> BDD-cost:   79
c ---[1055]---> BDD-cost:   79
c ---[1054]---> BDD-cost:   79
c ---[1053]---> BDD-cost:   79
c ---[1052]---> BDD-cost:  112
c ---[1051]---> BDD-cost:  110
c ---[1050]---> BDD-cost:   79
c ---[1048]---> BDD-cost:   79
c ---[1047]---> BDD-cost:   79
c ---[1046]---> BDD-cost:   79
c ---[1045]---> BDD-cost:  114
c ---[1044]---> BDD-cost:  110
c ---[1043]---> BDD-cost:   79
c ---[1042]---> BDD-cost:   79
c ---[1041]---> BDD-cost:   79
c ---[1040]---> BDD-cost:   79
c ---[1039]---> BDD-cost:  114
c ---[1037]---> BDD-cost:  110
c ---[1036]---> BDD-cost:   79
c ---[1035]---> BDD-cost:   79
c ---[1034]---> BDD-cost:   79
c ---[1033]---> BDD-cost:   79
c ---[1032]---> BDD-cost:  114
c ---[1031]---> BDD-cost:  110
c ---[1030]---> BDD-cost:   79
c ---[1029]---> BDD-cost:   79
c ---[1028]---> BDD-cost:   79
c ---[1026]---> BDD-cost:   79
c ---[1025]---> BDD-cost:  114
c ---[1024]---> BDD-cost:  110
c ---[1023]---> BDD-cost:   79
c ---[1022]---> BDD-cost:   79
c ---[1021]---> BDD-cost:   79
c ---[1020]---> BDD-cost:   79
c ---[1019]---> BDD-cost:  110
c ---[1018]---> BDD-cost:  110
c ---[1017]---> BDD-cost:   79
c ---[1015]---> BDD-cost:   79
c ---[1014]---> BDD-cost:   79
c ---[1013]---> BDD-cost:   79
c ---[1012]---> BDD-cost:  116
c ---[1011]---> BDD-cost:  110
c ---[1010]---> BDD-cost:   79
c ---[1009]---> BDD-cost:   79
c ---[1008]---> BDD-cost:   79
c ---[1007]---> BDD-cost:   79
c ---[1006]---> BDD-cost:  116
c ---[1004]---> BDD-cost:  110
c ---[1003]---> BDD-cost:   79
c ---[1002]---> BDD-cost:   79
c ---[1001]---> BDD-cost:   79
c ---[1000]---> BDD-cost:   79
c ---[ 999]---> BDD-cost:  116
c ---[ 998]---> BDD-cost:  110
c ---[ 997]---> BDD-cost:   79
c ---[ 996]---> BDD-cost:   79
c ---[ 995]---> BDD-cost:   79
c ---[ 993]---> BDD-cost:   79
c ---[ 992]---> BDD-cost:  112
c ---[ 991]---> BDD-cost:  110
c ---[ 990]---> BDD-cost:   79
c ---[ 989]---> BDD-cost:   79
c ---[ 988]---> BDD-cost:   79
c ---[ 987]---> BDD-cost:   79
c ---[ 986]---> BDD-cost:  110
c ---[ 985]---> BDD-cost:  110
c ---[ 984]---> BDD-cost:   79
c ---[ 982]---> BDD-cost:   79
c ---[ 981]---> BDD-cost:   79
c ---[ 980]---> BDD-cost:   79
c ---[ 979]---> BDD-cost:  114
c ---[ 978]---> BDD-cost:  110
c ---[ 977]---> BDD-cost:   79
c ---[ 976]---> BDD-cost:   79
c ---[ 975]---> BDD-cost:   79
c ---[ 974]---> BDD-cost:   79
c ---[ 973]---> BDD-cost:  110
c ---[ 971]---> BDD-cost:  110
c ---[ 970]---> BDD-cost:   79
c ---[ 969]---> BDD-cost:   79
c ---[ 968]---> BDD-cost:   79
c ---[ 967]---> BDD-cost:   79
c ---[ 966]---> BDD-cost:  112
c ---[ 965]---> BDD-cost:  110
c ---[ 964]---> BDD-cost:   79
c ---[ 963]---> BDD-cost:   79
c ---[ 962]---> BDD-cost:   79
c ---[ 960]---> BDD-cost:   79
c ---[ 959]---> BDD-cost:  112
c ---[ 958]---> BDD-cost:  110
c ---[ 957]---> BDD-cost:   79
c ---[ 956]---> BDD-cost:   79
c ---[ 955]---> BDD-cost:   79
c ---[ 954]---> BDD-cost:   79
c ---[ 953]---> BDD-cost:  114
c ---[ 952]---> BDD-cost:  110
c ---[ 951]---> BDD-cost:   79
c ---[ 948]---> BDD-cost:   79
c ---[ 947]---> BDD-cost:   79
c ---[ 946]---> BDD-cost:   79
c ---[ 945]---> BDD-cost:  116
c ---[ 944]---> BDD-cost:  110
c ---[ 943]---> BDD-cost:   79
c ---[ 942]---> BDD-cost:   79
c ---[ 941]---> BDD-cost:   79
c ---[ 940]---> BDD-cost:   79
c ---[ 939]---> BDD-cost:  110
c ---[ 937]---> BDD-cost:  110
c ---[ 936]---> BDD-cost:   79
c ---[ 935]---> BDD-cost:   79
c ---[ 934]---> BDD-cost:   79
c ---[ 933]---> BDD-cost:   79
c ---[ 932]---> BDD-cost:  116
c ---[ 931]---> BDD-cost:  110
c ---[ 930]---> BDD-cost:   79
c ---[ 929]---> BDD-cost:   79
c ---[ 928]---> BDD-cost:   79
c ---[ 926]---> BDD-cost:   79
c ---[ 925]---> BDD-cost:  116
c ---[ 924]---> BDD-cost:  110
c ---[ 923]---> BDD-cost:   79
c ---[ 922]---> BDD-cost:   79
c ---[ 921]---> BDD-cost:   79
c ---[ 920]---> BDD-cost:   79
c ---[ 919]---> BDD-cost:  114
c ---[ 918]---> BDD-cost:  110
c ---[ 917]---> BDD-cost:   79
c ---[ 915]---> BDD-cost:   79
c ---[ 914]---> BDD-cost:   79
c ---[ 913]---> BDD-cost:   79
c ---[ 912]---> BDD-cost:  116
c ---[ 911]---> BDD-cost:  110
c ---[ 910]---> BDD-cost:   79
c ---[ 909]---> BDD-cost:   79
c ---[ 908]---> BDD-cost:   79
c ---[ 907]---> BDD-cost:   79
c ---[ 906]---> BDD-cost:  116
c ---[ 904]---> BDD-cost:  110
c ---[ 903]---> BDD-cost:   79
c ---[ 902]---> BDD-cost:   79
c ---[ 901]---> BDD-cost:   79
c ---[ 900]---> BDD-cost:   79
c ---[ 899]---> BDD-cost:  106
c ---[ 898]---> BDD-cost:  110
c ---[ 897]---> BDD-cost:   79
c ---[ 896]---> BDD-cost:   79
c ---[ 895]---> BDD-cost:   79
c ---[ 893]---> BDD-cost:   79
c ---[ 892]---> BDD-cost:  116
c ---[ 891]---> BDD-cost:  110
c ---[ 890]---> BDD-cost:   79
c ---[ 889]---> BDD-cost:   79
c ---[ 888]---> BDD-cost:   79
c ---[ 887]---> BDD-cost:   79
c ---[ 886]---> BDD-cost:  116
c ---[ 885]---> BDD-cost:  110
c ---[ 884]---> BDD-cost:   79
c ---[ 882]---> BDD-cost:   79
c ---[ 881]---> BDD-cost:   79
c ---[ 880]---> BDD-cost:   79
c ---[ 879]---> BDD-cost:  116
c ---[ 878]---> BDD-cost:  110
c ---[ 877]---> BDD-cost:   79
c ---[ 876]---> BDD-cost:   79
c ---[ 875]---> BDD-cost:   79
c ---[ 874]---> BDD-cost:   79
c ---[ 873]---> BDD-cost:  114
c ---[ 871]---> BDD-cost:  110
c ---[ 870]---> BDD-cost:   79
c ---[ 869]---> BDD-cost:   79
c ---[ 868]---> BDD-cost:   79
c ---[ 867]---> BDD-cost:   79
c ---[ 866]---> BDD-cost:  116
c ---[ 865]---> BDD-cost:  110
c ---[ 864]---> BDD-cost:   79
c ---[ 863]---> BDD-cost:   79
c ---[ 862]---> BDD-cost:   79
c ---[ 860]---> BDD-cost:   79
c ---[ 859]---> BDD-cost:  114
c ---[ 858]---> BDD-cost:  110
c ---[ 857]---> BDD-cost:   79
c ---[ 856]---> BDD-cost:   79
c ---[ 855]---> BDD-cost:   79
c ---[ 854]---> BDD-cost:   79
c ---[ 853]---> BDD-cost:  116
c ---[ 852]---> BDD-cost:  110
c ---[ 851]---> BDD-cost:   79
c ---[ 849]---> BDD-cost:   79
c ---[ 848]---> BDD-cost:   79
c ---[ 847]---> BDD-cost:   79
c ---[ 846]---> BDD-cost:  114
c ---[ 845]---> BDD-cost:  110
c ---[ 844]---> BDD-cost:   79
c ---[ 843]---> BDD-cost:   79
c ---[ 842]---> BDD-cost:   79
c ---[ 841]---> BDD-cost:   79
c ---[ 840]---> BDD-cost:  112
c ---[ 837]---> BDD-cost:  110
c ---[ 836]---> BDD-cost:   79
c ---[ 835]---> BDD-cost:   79
c ---[ 834]---> BDD-cost:   79
c ---[ 833]---> BDD-cost:   79
c ---[ 832]---> BDD-cost:  114
c ---[ 831]---> BDD-cost:  110
c ---[ 830]---> BDD-cost:   79
c ---[ 829]---> BDD-cost:   79
c ---[ 828]---> BDD-cost:   79
c ---[ 826]---> BDD-cost:   79
c ---[ 825]---> BDD-cost:  116
c ---[ 824]---> BDD-cost:  110
c ---[ 823]---> BDD-cost:   79
c ---[ 822]---> BDD-cost:   79
c ---[ 821]---> BDD-cost:   79
c ---[ 820]---> BDD-cost:   79
c ---[ 819]---> BDD-cost:  110
c ---[ 818]---> BDD-cost:  110
c ---[ 817]---> BDD-cost:   79
c ---[ 815]---> BDD-cost:   79
c ---[ 814]---> BDD-cost:   79
c ---[ 813]---> BDD-cost:   79
c ---[ 812]---> BDD-cost:  116
c ---[ 811]---> BDD-cost:  110
c ---[ 810]---> BDD-cost:   79
c ---[ 809]---> BDD-cost:   79
c ---[ 808]---> BDD-cost:   79
c ---[ 807]---> BDD-cost:   79
c ---[ 806]---> BDD-cost:  116
c ---[ 804]---> BDD-cost:  110
c ---[ 803]---> BDD-cost:   79
c ---[ 802]---> BDD-cost:   79
c ---[ 801]---> BDD-cost:   79
c ---[ 800]---> BDD-cost:   79
c ---[ 799]---> BDD-cost:  116
c ---[ 798]---> BDD-cost:  110
c ---[ 797]---> BDD-cost:   79
c ---[ 796]---> BDD-cost:   79
c ---[ 795]---> BDD-cost:   79
c ---[ 793]---> BDD-cost:   79
c ---[ 792]---> BDD-cost:  116
c ---[ 791]---> BDD-cost:  110
c ---[ 790]---> BDD-cost:   79
c ---[ 789]---> BDD-cost:   79
c ---[ 788]---> BDD-cost:   79
c ---[ 787]---> BDD-cost:   79
c ---[ 786]---> BDD-cost:  110
c ---[ 785]---> BDD-cost:  110
c ---[ 784]---> BDD-cost:   79
c ---[ 782]---> BDD-cost:   79
c ---[ 781]---> BDD-cost:   79
c ---[ 780]---> BDD-cost:   79
c ---[ 779]---> BDD-cost:  112
c ---[ 778]---> BDD-cost:  110
c ---[ 777]---> BDD-cost:   79
c ---[ 776]---> BDD-cost:   79
c ---[ 775]---> BDD-cost:   79
c ---[ 774]---> BDD-cost:   79
c ---[ 773]---> BDD-cost:  112
c ---[ 771]---> BDD-cost:  110
c ---[ 770]---> BDD-cost:   79
c ---[ 769]---> BDD-cost:   79
c ---[ 768]---> BDD-cost:   79
c ---[ 767]---> BDD-cost:   79
c ---[ 766]---> BDD-cost:  116
c ---[ 765]---> BDD-cost:  110
c ---[ 764]---> BDD-cost:   79
c ---[ 763]---> BDD-cost:   79
c ---[ 762]---> BDD-cost:   79
c ---[ 760]---> BDD-cost:   79
c ---[ 759]---> BDD-cost:  110
c ---[ 758]---> BDD-cost:  110
c ---[ 757]---> BDD-cost:   79
c ---[ 756]---> BDD-cost:   79
c ---[ 755]---> BDD-cost:   79
c ---[ 754]---> BDD-cost:   79
c ---[ 753]---> BDD-cost:  116
c ---[ 752]---> BDD-cost:  110
c ---[ 751]---> BDD-cost:   79
c ---[ 749]---> BDD-cost:   79
c ---[ 748]---> BDD-cost:   79
c ---[ 747]---> BDD-cost:   79
c ---[ 746]---> BDD-cost:  110
c ---[ 745]---> BDD-cost:  110
c ---[ 744]---> BDD-cost:   79
c ---[ 743]---> BDD-cost:   79
c ---[ 742]---> BDD-cost:   79
c ---[ 741]---> BDD-cost:   79
c ---[ 740]---> BDD-cost:  116
c ---[ 738]---> BDD-cost:  110
c ---[ 737]---> BDD-cost:   79
c ---[ 736]---> BDD-cost:   79
c ---[ 735]---> BDD-cost:   79
c ---[ 734]---> BDD-cost:   79
c ---[ 733]---> BDD-cost:  116
c ---[ 732]---> BDD-cost:  110
c ---[ 731]---> BDD-cost:   79
c ---[ 730]---> BDD-cost:   79
c ---[ 729]---> BDD-cost:   79
c ---[ 726]---> BDD-cost:   79
c ---[ 725]---> BDD-cost:  112
c ---[ 724]---> BDD-cost:  110
c ---[ 723]---> BDD-cost:   79
c ---[ 722]---> BDD-cost:   79
c ---[ 721]---> BDD-cost:   79
c ---[ 720]---> BDD-cost:   79
c ---[ 719]---> BDD-cost:  114
c ---[ 718]---> BDD-cost:  110
c ---[ 717]---> BDD-cost:   79
c ---[ 715]---> BDD-cost:   79
c ---[ 714]---> BDD-cost:   79
c ---[ 713]---> BDD-cost:   79
c ---[ 712]---> BDD-cost:  114
c ---[ 711]---> BDD-cost:  110
c ---[ 710]---> BDD-cost:   79
c ---[ 709]---> BDD-cost:   79
c ---[ 708]---> BDD-cost:   79
c ---[ 707]---> BDD-cost:   79
c ---[ 706]---> BDD-cost:  116
c ---[ 704]---> BDD-cost:  110
c ---[ 703]---> BDD-cost:   79
c ---[ 702]---> BDD-cost:   79
c ---[ 701]---> BDD-cost:   79
c ---[ 700]---> BDD-cost:   79
c ---[ 699]---> BDD-cost:  116
c ---[ 698]---> BDD-cost:  110
c ---[ 697]---> BDD-cost:   79
c ---[ 696]---> BDD-cost:   79
c ---[ 695]---> BDD-cost:   79
c ---[ 693]---> BDD-cost:   79
c ---[ 692]---> BDD-cost:  112
c ---[ 691]---> BDD-cost:  110
c ---[ 690]---> BDD-cost:   79
c ---[ 689]---> BDD-cost:   79
c ---[ 688]---> BDD-cost:   79
c ---[ 687]---> BDD-cost:   79
c ---[ 686]---> BDD-cost:  116
c ---[ 685]---> BDD-cost:  110
c ---[ 684]---> BDD-cost:   79
c ---[ 682]---> BDD-cost:   79
c ---[ 681]---> BDD-cost:   79
c ---[ 680]---> BDD-cost:   79
c ---[ 679]---> BDD-cost:  112
c ---[ 678]---> BDD-cost:  110
c ---[ 677]---> BDD-cost:   79
c ---[ 676]---> BDD-cost:   79
c ---[ 675]---> BDD-cost:   79
c ---[ 674]---> BDD-cost:   79
c ---[ 673]---> BDD-cost:  114
c ---[ 671]---> BDD-cost:  110
c ---[ 670]---> BDD-cost:   79
c ---[ 669]---> BDD-cost:   79
c ---[ 668]---> BDD-cost:   79
c ---[ 667]---> BDD-cost:   79
c ---[ 666]---> BDD-cost:  116
c ---[ 665]---> BDD-cost:  110
c ---[ 664]---> BDD-cost:   79
c ---[ 663]---> BDD-cost:   79
c ---[ 662]---> BDD-cost:   79
c ---[ 660]---> BDD-cost:   79
c ---[ 659]---> BDD-cost:  110
c ---[ 658]---> BDD-cost:  110
c ---[ 657]---> BDD-cost:   79
c ---[ 656]---> BDD-cost:   79
c ---[ 655]---> BDD-cost:   79
c ---[ 654]---> BDD-cost:   79
c ---[ 653]---> BDD-cost:  116
c ---[ 652]---> BDD-cost:  110
c ---[ 651]---> BDD-cost:   79
c ---[ 649]---> BDD-cost:   79
c ---[ 648]---> BDD-cost:   79
c ---[ 647]---> BDD-cost:   79
c ---[ 646]---> BDD-cost:  108
c ---[ 645]---> BDD-cost:  110
c ---[ 644]---> BDD-cost:   79
c ---[ 643]---> BDD-cost:   79
c ---[ 642]---> BDD-cost:   79
c ---[ 641]---> BDD-cost:   79
c ---[ 640]---> BDD-cost:  116
c ---[ 638]---> BDD-cost:  110
c ---[ 637]---> BDD-cost:   79
c ---[ 636]---> BDD-cost:   79
c ---[ 635]---> BDD-cost:   79
c ---[ 634]---> BDD-cost:   79
c ---[ 633]---> BDD-cost:  112
c ---[ 632]---> BDD-cost:  110
c ---[ 631]---> BDD-cost:   79
c ---[ 630]---> BDD-cost:   79
c ---[ 629]---> BDD-cost:   79
c ---[ 627]---> BDD-cost:   79
c ---[ 626]---> BDD-cost:  116
c ---[ 625]---> BDD-cost:  110
c ---[ 624]---> BDD-cost:   79
c ---[ 623]---> BDD-cost:   79
c ---[ 622]---> BDD-cost:   79
c ---[ 621]---> BDD-cost:   79
c ---[ 620]---> BDD-cost:  116
c ---[ 619]---> BDD-cost:  110
c ---[ 618]---> BDD-cost:   79
c ---[ 617]---> BDD-cost:   23
c ---[ 616]---> BDD-cost:   23
c ---[ 615]---> BDD-cost:   23
c ---[ 614]---> BDD-cost:   23
c ---[ 613]---> BDD-cost:   23
c ---[ 612]---> BDD-cost:   23
c ---[ 611]---> BDD-cost:   23
c ---[ 610]---> BDD-cost:   23
c ---[ 609]---> BDD-cost:   23
c ---[ 608]---> BDD-cost:   23
c ---[ 607]---> BDD-cost:   23
c ---[ 606]---> BDD-cost:   23
c ---[ 605]---> BDD-cost:   23
c ---[ 604]---> BDD-cost:   23
c ---[ 603]---> BDD-cost:   23
c ---[ 602]---> BDD-cost:   23
c ---[ 601]---> BDD-cost:   23
c ---[ 600]---> BDD-cost:   23
c ---[ 599]---> BDD-cost:   23
c ---[ 598]---> BDD-cost:   23
c ---[ 597]---> BDD-cost:   23
c ---[ 596]---> BDD-cost:   23
c ---[ 595]---> BDD-cost:   23
c ---[ 594]---> BDD-cost:   23
c ---[ 593]---> BDD-cost:   23
c ---[ 592]---> BDD-cost:   23
c ---[ 591]---> BDD-cost:   23
c ---[ 590]---> BDD-cost:   23
c ---[ 589]---> BDD-cost:   23
c ---[ 588]---> BDD-cost:   23
c ---[ 587]---> BDD-cost:   23
c ---[ 586]---> BDD-cost:   23
c ---[ 585]---> BDD-cost:   23
c ---[ 584]---> BDD-cost:   23
c ---[ 583]---> BDD-cost:   23
c ---[ 582]---> BDD-cost:   23
c ---[ 581]---> BDD-cost:   23
c ---[ 580]---> BDD-cost:   23
c ---[ 579]---> BDD-cost:   23
c ---[ 578]---> BDD-cost:   23
c ---[ 577]---> BDD-cost:   23
c ---[ 576]---> BDD-cost:   23
c ---[ 575]---> BDD-cost:   23
c ---[ 574]---> BDD-cost:   23
c ---[ 573]---> BDD-cost:   23
c ---[ 572]---> BDD-cost:   23
c ---[ 571]---> BDD-cost:   23
c ---[ 570]---> BDD-cost:   23
c ---[ 569]---> BDD-cost:   23
c ---[ 568]---> BDD-cost:   23
c ---[ 567]---> BDD-cost:   23
c ---[ 566]---> BDD-cost:   23
c ---[ 565]---> BDD-cost:   23
c ---[ 564]---> BDD-cost:   23
c ---[ 563]---> BDD-cost:   23
c ---[ 562]---> BDD-cost:   23
c ---[ 561]---> BDD-cost:   23
c ---[ 560]---> BDD-cost:   23
c ---[ 559]---> BDD-cost:   23
c ---[ 558]---> BDD-cost:   23
c ---[ 557]---> BDD-cost:   23
c ---[ 556]---> BDD-cost:   23
c ---[ 555]---> BDD-cost:   23
c ---[ 554]---> BDD-cost:   23
c ---[ 553]---> BDD-cost:   23
c ---[ 552]---> BDD-cost:   23
c ---[ 551]---> BDD-cost:   23
c ---[ 550]---> BDD-cost:   23
c ---[ 549]---> BDD-cost:   23
c ---[ 548]---> BDD-cost:   23
c ---[ 547]---> BDD-cost:   23
c ---[ 546]---> BDD-cost:   23
c ---[ 545]---> BDD-cost:   23
c ---[ 544]---> BDD-cost:   23
c ---[ 543]---> BDD-cost:   23
c ---[ 542]---> BDD-cost:   23
c ---[ 541]---> BDD-cost:   23
c ---[ 540]---> BDD-cost:   23
c ---[ 539]---> BDD-cost:   23
c ---[ 538]---> BDD-cost:   23
c ---[ 537]---> BDD-cost:   23
c ---[ 536]---> BDD-cost:   23
c ---[ 535]---> BDD-cost:   23
c ---[ 534]---> BDD-cost:   23
c ---[ 533]---> BDD-cost:   23
c ---[ 532]---> BDD-cost:   23
c ---[ 531]---> BDD-cost:   23
c ---[ 530]---> BDD-cost:   23
c ---[ 529]---> BDD-cost:   23
c ---[ 528]---> BDD-cost:   23
c ---[ 527]---> BDD-cost:   23
c ---[ 526]---> BDD-cost:   23
c ---[ 525]---> BDD-cost:   23
c ---[ 524]---> BDD-cost:   23
c ---[ 523]---> BDD-cost:   23
c ---[ 522]---> BDD-cost:   23
c ---[ 521]---> BDD-cost:   23
c ---[ 520]---> BDD-cost:   23
c ---[ 519]---> BDD-cost:   23
c ---[ 518]---> BDD-cost:   23
c ---[ 517]---> BDD-cost:   23
c ---[ 516]---> BDD-cost:   23
c ---[ 515]---> BDD-cost:   23
c ---[ 514]---> BDD-cost:   23
c ---[ 513]---> BDD-cost:   23
c ---[ 512]---> BDD-cost:   23
c ---[ 511]---> BDD-cost:   23
c ---[ 510]---> BDD-cost:   23
c ---[ 509]---> BDD-cost:   23
c ---[ 508]---> BDD-cost:   23
c ---[ 507]---> BDD-cost:   23
c ---[ 506]---> BDD-cost:   23
c ---[ 505]---> BDD-cost:   23
c ---[ 504]---> BDD-cost:   23
c ---[ 503]---> BDD-cost:   23
c ---[ 502]---> BDD-cost:   23
c ---[ 501]---> BDD-cost:   23
c ---[ 500]---> BDD-cost:   23
c ---[ 499]---> BDD-cost:   23
c ---[ 498]---> BDD-cost:   23
c ---[ 497]---> BDD-cost:   23
c ---[ 496]---> BDD-cost:   23
c ---[ 495]---> BDD-cost:   23
c ---[ 494]---> BDD-cost:   23
c ---[ 493]---> BDD-cost:   23
c ---[ 492]---> BDD-cost:   23
c ---[ 491]---> BDD-cost:   23
c ---[ 490]---> BDD-cost:   23
c ---[ 489]---> BDD-cost:   23
c ---[ 488]---> BDD-cost:   23
c ---[ 487]---> BDD-cost:   23
c ---[ 486]---> BDD-cost:   23
c ---[ 485]---> BDD-cost:   23
c ---[ 484]---> BDD-cost:   23
c ---[ 483]---> BDD-cost:   23
c ---[ 482]---> BDD-cost:   23
c ---[ 481]---> BDD-cost:   23
c ---[ 480]---> BDD-cost:   23
c ---[ 479]---> BDD-cost:   23
c ---[ 478]---> BDD-cost:   23
c ---[ 477]---> BDD-cost:   23
c ---[ 476]---> BDD-cost:   23
c ---[ 475]---> BDD-cost:   23
c ---[ 474]---> BDD-cost:   23
c ---[ 473]---> BDD-cost:   23
c ---[ 472]---> BDD-cost:   23
c ---[ 471]---> BDD-cost:   23
c ---[ 470]---> BDD-cost:   23
c ---[ 469]---> BDD-cost:   23
c ---[ 468]---> BDD-cost:   23
c ---[ 467]---> BDD-cost:   23
c ---[ 466]---> BDD-cost:   23
c ---[ 465]---> BDD-cost:   23
c ---[ 464]---> BDD-cost:   23
c ---[ 463]---> BDD-cost:   23
c ---[ 462]---> BDD-cost:   23
c ---[ 461]---> BDD-cost:   23
c ---[ 460]---> BDD-cost:   23
c ---[ 459]---> BDD-cost:   23
c ---[ 458]---> BDD-cost:   23
c ---[ 457]---> BDD-cost:   23
c ---[ 456]---> BDD-cost:   23
c ---[ 455]---> BDD-cost:   23
c ---[ 454]---> BDD-cost:   23
c ---[ 453]---> BDD-cost:   23
c ---[ 452]---> BDD-cost:   23
c ---[ 451]---> BDD-cost:   23
c ---[ 450]---> BDD-cost:   23
c ---[ 449]---> BDD-cost:   23
c ---[ 448]---> BDD-cost:   23
c ---[ 447]---> BDD-cost:   23
c ---[ 446]---> BDD-cost:   23
c ---[ 445]---> BDD-cost:   23
c ---[ 444]---> BDD-cost:   23
c ---[ 443]---> BDD-cost:   23
c ---[ 442]---> BDD-cost:   23
c ---[ 441]---> BDD-cost:   23
c ---[ 440]---> BDD-cost:   23
c ---[ 439]---> BDD-cost:   23
c ---[ 438]---> BDD-cost:   23
c ---[ 437]---> BDD-cost:   23
c ---[ 436]---> BDD-cost:   23
c ---[ 435]---> BDD-cost:   23
c ---[ 434]---> BDD-cost:   23
c ---[ 433]---> BDD-cost:   23
c ---[ 432]---> BDD-cost:   23
c ---[ 431]---> BDD-cost:   23
c ---[ 430]---> BDD-cost:   23
c ---[ 429]---> BDD-cost:   23
c ---[ 428]---> BDD-cost:   23
c ---[ 427]---> BDD-cost:   23
c ---[ 426]---> BDD-cost:   23
c ---[ 425]---> BDD-cost:   23
c ---[ 424]---> BDD-cost:   23
c ---[ 423]---> BDD-cost:   23
c ---[ 422]---> BDD-cost:   23
c ---[ 421]---> BDD-cost:   23
c ---[ 420]---> BDD-cost:   23
c ---[ 419]---> BDD-cost:   23
c ---[ 418]---> BDD-cost:   23
c ---[ 417]---> BDD-cost:   23
c ---[ 416]---> BDD-cost:   23
c ---[ 415]---> BDD-cost:   23
c ---[ 414]---> BDD-cost:   23
c ---[ 413]---> BDD-cost:   23
c ---[ 412]---> BDD-cost:   23
c ---[ 411]---> BDD-cost:   23
c ---[ 410]---> BDD-cost:   23
c ---[ 409]---> BDD-cost:   23
c ---[ 408]---> BDD-cost:   23
c ---[ 407]---> BDD-cost:   23
c ---[ 406]---> BDD-cost:   23
c ---[ 405]---> BDD-cost:   23
c ---[ 404]---> BDD-cost:   23
c ---[ 403]---> BDD-cost:   23
c ---[ 402]---> BDD-cost:   23
c ---[ 401]---> BDD-cost:   23
c ---[ 400]---> BDD-cost:   23
c ---[ 399]---> BDD-cost:   23
c ---[ 398]---> BDD-cost:   23
c ---[ 397]---> BDD-cost:   23
c ---[ 396]---> BDD-cost:   23
c ---[ 395]---> BDD-cost:   23
c ---[ 394]---> BDD-cost:   23
c ---[ 393]---> BDD-cost:   23
c ---[ 392]---> BDD-cost:   23
c ---[ 391]---> BDD-cost:   23
c ---[ 390]---> BDD-cost:   23
c ---[ 389]---> BDD-cost:   23
c ---[ 388]---> BDD-cost:   23
c ---[ 387]---> BDD-cost:   23
c ---[ 386]---> BDD-cost:   23
c ---[ 385]---> BDD-cost:   23
c ---[ 384]---> BDD-cost:   23
c ---[ 383]---> BDD-cost:   23
c ---[ 382]---> BDD-cost:   23
c ---[ 381]---> BDD-cost:   23
c ---[ 380]---> BDD-cost:   23
c ---[ 379]---> BDD-cost:   23
c ---[ 378]---> BDD-cost:   23
c ---[ 377]---> BDD-cost:   23
c ---[ 376]---> BDD-cost:   23
c ---[ 375]---> BDD-cost:   23
c ---[ 374]---> BDD-cost:   23
c ---[ 373]---> BDD-cost:   23
c ---[ 372]---> BDD-cost:   23
c ---[ 371]---> BDD-cost:   23
c ---[ 370]---> BDD-cost:   23
c ---[ 369]---> BDD-cost:   23
c ---[ 368]---> BDD-cost:   23
c ---[ 367]---> BDD-cost:   23
c ---[ 366]---> BDD-cost:   23
c ---[ 365]---> BDD-cost:   23
c ---[ 364]---> BDD-cost:   23
c ---[ 363]---> BDD-cost:   23
c ---[ 362]---> BDD-cost:   23
c ---[ 361]---> BDD-cost:   23
c ---[ 360]---> BDD-cost:   23
c ---[ 359]---> BDD-cost:   23
c ---[ 358]---> BDD-cost:   23
c ---[ 357]---> BDD-cost:   23
c ---[ 356]---> BDD-cost:   23
c ---[ 355]---> BDD-cost:   23
c ---[ 354]---> BDD-cost:   23
c ---[ 353]---> BDD-cost:   23
c ---[ 352]---> BDD-cost:   23
c ---[ 351]---> BDD-cost:   23
c ---[ 350]---> BDD-cost:   23
c ---[ 349]---> BDD-cost:   23
c ---[ 348]---> BDD-cost:   23
c ---[ 347]---> BDD-cost:   23
c ---[ 346]---> BDD-cost:   23
c ---[ 345]---> BDD-cost:   23
c ---[ 344]---> BDD-cost:   23
c ---[ 343]---> BDD-cost:   23
c ---[ 342]---> BDD-cost:   23
c ---[ 341]---> BDD-cost:   23
c ---[ 340]---> BDD-cost:   23
c ---[ 339]---> BDD-cost:   23
c ---[ 338]---> BDD-cost:   23
c ---[ 337]---> BDD-cost:   23
c ---[ 336]---> BDD-cost:   23
c ---[ 335]---> BDD-cost:   23
c ---[ 334]---> BDD-cost:   23
c ---[ 333]---> BDD-cost:   23
c ---[ 332]---> BDD-cost:   23
c ---[ 331]---> BDD-cost:   23
c ---[ 330]---> BDD-cost:   23
c ---[ 329]---> BDD-cost:   23
c ---[ 328]---> BDD-cost:   23
c ---[ 327]---> BDD-cost:   23
c ---[ 326]---> BDD-cost:   23
c ---[ 325]---> BDD-cost:   23
c ---[ 324]---> BDD-cost:   23
c ---[ 323]---> BDD-cost:   23
c ---[ 322]---> BDD-cost:   23
c ---[ 321]---> BDD-cost:   23
c ---[ 320]---> BDD-cost:   23
c ---[ 319]---> BDD-cost:   23
c ---[ 318]---> BDD-cost:   23
c ---[ 317]---> BDD-cost:   23
c ---[ 316]---> BDD-cost:   23
c ---[ 315]---> BDD-cost:   23
c ---[ 314]---> BDD-cost:   23
c ---[ 313]---> BDD-cost:   23
c ---[ 312]---> BDD-cost:   23
c ---[ 311]---> BDD-cost:   23
c ---[ 310]---> BDD-cost:   23
c ---[ 309]---> BDD-cost:   23
c ---[ 308]---> BDD-cost:   23
c ---[ 307]---> BDD-cost:   23
c ---[ 306]---> BDD-cost:   23
c ---[ 305]---> BDD-cost:   23
c ---[ 304]---> BDD-cost:   23
c ---[ 303]---> BDD-cost:   23
c ---[ 302]---> BDD-cost:   23
c ---[ 301]---> BDD-cost:   23
c ---[ 300]---> BDD-cost:   23
c ---[ 299]---> BDD-cost:   23
c ---[ 298]---> BDD-cost:   23
c ---[ 297]---> BDD-cost:   23
c ---[ 296]---> BDD-cost:   23
c ---[ 295]---> BDD-cost:   23
c ---[ 294]---> BDD-cost:   23
c ---[ 293]---> BDD-cost:   23
c ---[ 292]---> BDD-cost:   23
c ---[ 291]---> BDD-cost:   23
c ---[ 290]---> BDD-cost:   23
c ---[ 289]---> BDD-cost:   23
c ---[ 288]---> BDD-cost:   23
c ---[ 287]---> BDD-cost:   23
c ---[ 286]---> BDD-cost:   23
c ---[ 285]---> BDD-cost:   23
c ---[ 284]---> BDD-cost:   23
c ---[ 283]---> BDD-cost:   23
c ---[ 282]---> BDD-cost:   23
c ---[ 281]---> BDD-cost:   23
c ---[ 280]---> BDD-cost:   23
c ---[ 279]---> BDD-cost:   23
c ---[ 278]---> BDD-cost:   23
c ---[ 277]---> BDD-cost:   23
c ---[ 276]---> BDD-cost:   23
c ---[ 275]---> BDD-cost:   23
c ---[ 274]---> BDD-cost:   23
c ---[ 273]---> BDD-cost:   23
c ---[ 272]---> BDD-cost:   23
c ---[ 271]---> BDD-cost:   23
c ---[ 270]---> BDD-cost:   23
c ---[ 269]---> BDD-cost:   23
c ---[ 268]---> BDD-cost:   23
c ---[ 267]---> BDD-cost:   23
c ---[ 266]---> BDD-cost:   23
c ---[ 265]---> BDD-cost:   23
c ---[ 264]---> BDD-cost:   23
c ---[ 263]---> BDD-cost:   23
c ---[ 262]---> BDD-cost:   23
c ---[ 261]---> BDD-cost:   23
c ---[ 260]---> BDD-cost:   23
c ---[ 259]---> BDD-cost:   23
c ---[ 258]---> BDD-cost:   23
c ---[ 257]---> BDD-cost:   23
c ---[ 256]---> BDD-cost:   23
c ---[ 255]---> BDD-cost:   23
c ---[ 254]---> BDD-cost:   23
c ---[ 253]---> BDD-cost:   23
c ---[ 252]---> BDD-cost:   23
c ---[ 251]---> BDD-cost:   23
c ---[ 250]---> BDD-cost:   23
c ---[ 249]---> BDD-cost:   23
c ---[ 248]---> BDD-cost:   23
c ---[ 247]---> BDD-cost:   23
c ---[ 246]---> BDD-cost:   23
c ---[ 245]---> BDD-cost:   23
c ---[ 244]---> BDD-cost:   23
c ---[ 243]---> BDD-cost:   23
c ---[ 242]---> BDD-cost:   23
c ---[ 241]---> BDD-cost:   23
c ---[ 240]---> BDD-cost:   23
c ---[ 239]---> BDD-cost:   23
c ---[ 238]---> BDD-cost:   23
c ---[ 237]---> BDD-cost:   23
c ---[ 236]---> BDD-cost:   23
c ---[ 235]---> BDD-cost:   23
c ---[ 234]---> BDD-cost:   23
c ---[ 233]---> BDD-cost:   23
c ---[ 232]---> BDD-cost:   23
c ---[ 231]---> BDD-cost:   23
c ---[ 230]---> BDD-cost:   23
c ---[ 229]---> BDD-cost:   23
c ---[ 228]---> BDD-cost:   23
c ---[ 227]---> BDD-cost:   23
c ---[ 226]---> BDD-cost:   23
c ---[ 225]---> BDD-cost:   23
c ---[ 224]---> BDD-cost:   23
c ---[ 223]---> BDD-cost:   23
c ---[ 222]---> BDD-cost:   23
c ---[ 221]---> BDD-cost:   23
c ---[ 220]---> BDD-cost:   23
c ---[ 219]---> BDD-cost:   23
c ---[ 218]---> BDD-cost:   23
c ---[ 217]---> BDD-cost:   23
c ---[ 216]---> BDD-cost:   23
c ---[ 215]---> BDD-cost:   23
c ---[ 214]---> BDD-cost:   23
c ---[ 213]---> BDD-cost:   23
c ---[ 212]---> BDD-cost:   23
c ---[ 211]---> BDD-cost:   23
c ---[ 210]---> BDD-cost:   23
c ---[ 209]---> BDD-cost:   23
c ---[ 208]---> BDD-cost:   23
c ---[ 207]---> BDD-cost:   23
c ---[ 206]---> BDD-cost:   23
c ---[ 205]---> BDD-cost:   23
c ---[ 204]---> BDD-cost:   23
c ---[ 203]---> BDD-cost:   23
c ---[ 202]---> BDD-cost:   23
c ---[ 201]---> BDD-cost:   23
c ---[ 200]---> BDD-cost:   23
c ---[ 199]---> BDD-cost:   23
c ---[ 198]---> BDD-cost:   23
c ---[ 197]---> BDD-cost:   23
c ---[ 196]---> BDD-cost:   23
c ---[ 195]---> BDD-cost:   23
c ---[ 194]---> BDD-cost:   23
c ---[ 193]---> BDD-cost:   23
c ---[ 192]---> BDD-cost:   23
c ---[ 191]---> BDD-cost:   23
c ---[ 190]---> BDD-cost:   23
c ---[ 189]---> BDD-cost:   23
c ---[ 188]---> BDD-cost:   23
c ---[ 187]---> BDD-cost:   23
c ---[ 186]---> BDD-cost:   23
c ---[ 185]---> BDD-cost:   23
c ---[ 184]---> BDD-cost:   23
c ---[ 183]---> BDD-cost:   23
c ---[ 182]---> BDD-cost:   23
c ---[ 181]---> BDD-cost:   23
c ---[ 180]---> BDD-cost:   23
c ---[ 179]---> BDD-cost:   23
c ---[ 178]---> BDD-cost:   23
c ---[ 177]---> BDD-cost:   23
c ---[ 176]---> BDD-cost:   23
c ---[ 175]---> BDD-cost:   23
c ---[ 174]---> BDD-cost:   23
c ---[ 173]---> BDD-cost:   23
c ---[ 172]---> BDD-cost:   23
c ---[ 171]---> BDD-cost:   23
c ---[ 170]---> BDD-cost:   23
c ---[ 169]---> BDD-cost:   23
c ---[ 168]---> BDD-cost:   23
c ---[ 167]---> BDD-cost:   23
c ---[ 166]---> BDD-cost:   23
c ---[ 165]---> BDD-cost:   23
c ---[ 164]---> BDD-cost:   23
c ---[ 163]---> BDD-cost:   23
c ---[ 162]---> BDD-cost:   23
c ---[ 161]---> BDD-cost:   23
c ---[ 160]---> BDD-cost:   23
c ---[ 159]---> BDD-cost:   23
c ---[ 158]---> BDD-cost:   23
c ---[ 157]---> BDD-cost:   23
c ---[ 156]---> BDD-cost:   23
c ---[ 155]---> BDD-cost:   23
c ---[ 154]---> BDD-cost:   23
c ---[ 153]---> BDD-cost:   23
c ---[ 152]---> BDD-cost:   23
c ---[ 151]---> BDD-cost:   23
c ---[ 150]---> BDD-cost:   23
c ---[ 149]---> BDD-cost:   23
c ---[ 148]---> BDD-cost:   23
c ---[ 147]---> BDD-cost:   23
c ---[ 146]---> BDD-cost:   23
c ---[ 145]---> BDD-cost:   23
c ---[ 144]---> BDD-cost:   23
c ---[ 143]---> BDD-cost:   23
c ---[ 142]---> BDD-cost:   23
c ---[ 141]---> BDD-cost:   23
c ---[ 140]---> BDD-cost:   23
c ---[ 139]---> BDD-cost:   23
c ---[ 138]---> BDD-cost:   23
c ---[ 137]---> BDD-cost:   23
c ---[ 136]---> BDD-cost:   23
c ---[ 135]---> BDD-cost:   23
c ---[ 134]---> BDD-cost:   23
c ---[ 133]---> BDD-cost:   23
c ---[ 132]---> BDD-cost:   23
c ---[ 131]---> BDD-cost:   23
c ---[ 130]---> BDD-cost:   23
c ---[ 129]---> BDD-cost:   23
c ---[ 128]---> BDD-cost:   23
c ---[ 127]---> BDD-cost:   23
c ---[ 126]---> BDD-cost:   23
c ---[ 125]---> BDD-cost:   23
c ---[ 124]---> BDD-cost:   23
c ---[ 123]---> BDD-cost:   23
c ---[ 122]---> BDD-cost:   23
c ---[ 121]---> BDD-cost:   23
c ---[ 120]---> BDD-cost:   23
c ---[ 119]---> BDD-cost:   23
c ---[ 118]---> BDD-cost:   23
c ---[ 117]---> BDD-cost:   23
c ---[ 116]---> BDD-cost:   23
c ---[ 115]---> BDD-cost:   23
c ---[ 114]---> BDD-cost:   23
c ---[ 113]---> BDD-cost:   23
c ---[ 112]---> BDD-cost:   23
c ---[ 111]---> BDD-cost:   23
c ---[ 110]---> BDD-cost:   23
c ---[ 109]---> BDD-cost:   23
c ---[ 108]---> BDD-cost:   23
c ---[ 107]---> BDD-cost:   23
c ---[ 106]---> BDD-cost:   23
c ---[ 105]---> BDD-cost:   23
c ---[ 104]---> BDD-cost:   23
c ---[ 103]---> BDD-cost:   23
c ---[ 102]---> BDD-cost:   23
c ---[ 101]---> BDD-cost:   23
c ---[ 100]---> BDD-cost:   23
c ---[  99]---> BDD-cost:   23
c ---[  98]---> BDD-cost:   23
c ---[  97]---> BDD-cost:   23
c ---[  96]---> BDD-cost:   23
c ---[  95]---> BDD-cost:   23
c ---[  94]---> BDD-cost:   23
c ---[  93]---> BDD-cost:   23
c ---[  92]---> BDD-cost:   23
c ---[  91]---> BDD-cost:   23
c ---[  90]---> BDD-cost:   23
c ---[  89]---> BDD-cost:   23
c ---[  88]---> BDD-cost:   23
c ---[  87]---> BDD-cost:   23
c ---[  86]---> BDD-cost:   23
c ---[  85]---> BDD-cost:   23
c ---[  84]---> BDD-cost:   23
c ---[  83]---> BDD-cost:   23
c ---[  82]---> BDD-cost:   23
c ---[  81]---> BDD-cost:   23
c ---[  80]---> BDD-cost:   23
c ---[  79]---> BDD-cost:   23
c ---[  78]---> BDD-cost:   23
c ---[  77]---> BDD-cost:   23
c ---[  76]---> BDD-cost:   23
c ---[  75]---> BDD-cost:   23
c ---[  74]---> BDD-cost:   23
c ---[  73]---> BDD-cost:   23
c ---[  72]---> BDD-cost:   23
c ---[  71]---> BDD-cost:   23
c ---[  70]---> BDD-cost:   23
c ---[  69]---> BDD-cost:   23
c ---[  68]---> BDD-cost:   23
c ---[  67]---> BDD-cost:   23
c ---[  66]---> BDD-cost:   23
c ---[  65]---> BDD-cost:   23
c ---[  64]---> BDD-cost:   23
c ---[  63]---> BDD-cost:   23
c ---[  62]---> BDD-cost:   23
c ---[  61]---> BDD-cost:   23
c ---[  60]---> BDD-cost:   23
c ---[  59]---> BDD-cost:   23
c ---[  58]---> BDD-cost:   23
c ---[  57]---> BDD-cost:   23
c ---[  56]---> BDD-cost:   23
c ---[  55]---> BDD-cost:   23
c ---[  54]---> BDD-cost:   23
c ---[  53]---> BDD-cost:   23
c ---[  52]---> BDD-cost:   23
c ---[  51]---> BDD-cost:   23
c ---[  50]---> BDD-cost:   23
c ---[  49]---> BDD-cost:   23
c ---[  48]---> BDD-cost:   23
c ---[  47]---> BDD-cost:   23
c ---[  46]---> BDD-cost:   23
c ---[  45]---> BDD-cost:   23
c ---[  44]---> BDD-cost:   23
c ---[  43]---> BDD-cost:   23
c ---[  42]---> BDD-cost:   23
c ---[  41]---> BDD-cost:   23
c ---[  40]---> BDD-cost:   23
c ---[  39]---> BDD-cost:   23
c ---[  38]---> BDD-cost:   23
c ---[  37]---> BDD-cost:   23
c ---[  36]---> BDD-cost:   23
c ---[  35]---> BDD-cost:   23
c ---[  34]---> BDD-cost:   23
c ---[  33]---> BDD-cost:   23
c ---[  32]---> BDD-cost:   23
c ---[  31]---> BDD-cost:   23
c ---[  30]---> BDD-cost:   23
c ---[  29]---> BDD-cost:   23
c ---[  28]---> BDD-cost:   23
c ---[  27]---> BDD-cost:   23
c ---[  26]---> BDD-cost:   23
c ---[  25]---> BDD-cost:   23
c ---[  24]---> BDD-cost:   23
c ---[  23]---> BDD-cost:   23
c ---[  22]---> BDD-cost:   23
c ---[  21]---> BDD-cost:   23
c ---[  20]---> BDD-cost:   23
c ---[  19]---> BDD-cost:   23
c ---[  18]---> BDD-cost:   23
c ---[  17]---> BDD-cost:   23
c ---[  16]---> BDD-cost:   23
c ---[  15]---> BDD-cost:   23
c ---[  14]---> BDD-cost:   23
c ---[  13]---> BDD-cost:   23
c ---[  12]---> BDD-cost:   23
c ---[  11]---> BDD-cost:   23
c ---[  10]---> BDD-cost:   23
c ---[   9]---> BDD-cost:   23
c ---[   8]---> BDD-cost:   23
c ---[   7]---> BDD-cost:   23
c ---[   6]---> BDD-cost:   23
c ---[   5]---> BDD-cost:   23
c ---[   4]---> BDD-cost:   23
c ---[   3]---> BDD-cost:   23
c ---[   2]---> BDD-cost:   23
c ---[   1]---> BDD-cost:   23
c ---[   0]---> BDD-cost:   23
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |  450978  1208466 |  150326       0        0     nan |  0.000 % |
c |       101 |  450978  1208466 |  165358     101     1328    13.1 |  1.196 % |
c |       251 |  450922  1208354 |  181894     223     1956     8.8 |  1.209 % |
c ==============================================================================
c [1mFound solution: 63488[0m
c ---[   0]---> Sorter-cost: 2296     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       383 |  452957  1213181 |  150985     343     2614     7.6 |  1.209 % |
c |       483 |  452955  1213177 |  166083     442     3169     7.2 |  1.210 % |
c |       633 |  452773  1212813 |  182691     500     3581     7.2 |  1.252 % |
c |       858 |  452605  1212477 |  200961     642     4736     7.4 |  1.290 % |
c |      1195 |  452571  1212409 |  221057     962     6658     6.9 |  1.298 % |
c |      1701 |  452443  1212153 |  243162    1404    11182     8.0 |  1.328 % |
c |      2460 |  452361  1211988 |  267479    2122    16780     7.9 |  1.347 % |
c |      3600 |  452241  1211748 |  294227    3201    30312     9.5 |  1.374 % |
c |      5309 |  452143  1211540 |  323649    4855    54953    11.3 |  1.397 % |
c ==============================================================================
c [1mFound solution: 59520[0m
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      6292 |  452552  1212570 |  150850    5808    61715    10.6 |  1.397 % |
c |      6394 |  452522  1212510 |  165935    5895    63109    10.7 |  1.416 % |
c |      6545 |  452520  1212506 |  182528    6045    64190    10.6 |  1.417 % |
c |      6770 |  452516  1212498 |  200781    6268    66557    10.6 |  1.418 % |
c |      7107 |  452516  1212498 |  220859    6605    69746    10.6 |  1.418 % |
c |      7613 |  452468  1212402 |  242945    7087    74848    10.6 |  1.429 % |
c |      8372 |  452406  1212265 |  267239    7803    80586    10.3 |  1.443 % |
c |      9511 |  452266  1211969 |  293963    8868    89412    10.1 |  1.475 % |
c ==============================================================================
c [1mFound solution: 57984[0m
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     10719 |  452272  1212049 |  150757   10019   102147    10.2 |  1.475 % |
c |     10821 |  452270  1212045 |  165832   10120   102804    10.2 |  1.502 % |
c |     10971 |  452270  1212045 |  182415   10270   104048    10.1 |  1.502 % |
c |     11196 |  452236  1211977 |  200657   10475   105856    10.1 |  1.509 % |
c |     11534 |  452224  1211953 |  220723   10807   108417    10.0 |  1.512 % |
c |     12041 |  452206  1211914 |  242795   11305   115954    10.3 |  1.516 % |
c |     12801 |  452158  1211818 |  267075   12038   123882    10.3 |  1.527 % |
c ==============================================================================
c [1mFound solution: 56832[0m
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     13748 |  452183  1211910 |  150727   12963   131206    10.1 |  1.527 % |
c |     13848 |  452155  1211854 |  165799   13049   131832    10.1 |  1.547 % |
c |     13998 |  452137  1211818 |  182379   13190   132563    10.1 |  1.551 % |
c |     14224 |  452137  1211818 |  200617   13416   135825    10.1 |  1.551 % |
c |     14561 |  452117  1211778 |  220679   13743   138295    10.1 |  1.556 % |
c |     15067 |  452001  1211534 |  242747   14183   144165    10.2 |  1.582 % |
c |     15826 |  451987  1211499 |  267022   14921   152864    10.2 |  1.586 % |
c |     16965 |  451967  1211457 |  293724   16050   163305    10.2 |  1.590 % |
c |     18673 |  451965  1211453 |  323096   17757   191826    10.8 |  1.591 % |
c |     21235 |  451923  1211358 |  355406   20284   236400    11.7 |  1.600 % |
c |     25079 |  451857  1211215 |  390947   24086   301458    12.5 |  1.615 % |
c |     30845 |  451597  1210686 |  430041   29634   378382    12.8 |  1.675 % |
c |     39494 |  451533  1210554 |  473045   38248   539657    14.1 |  1.690 % |
c ==============================================================================
c [1mFound solution: 56192[0m
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     49725 |  451479  1210458 |  150493   48384   796151    16.5 |  1.690 % |
c |     49828 |  451479  1210458 |  165542   48487   796971    16.4 |  1.714 % |
c |     49978 |  451479  1210458 |  182096   48637   799062    16.4 |  1.714 % |
c |     50203 |  451479  1210458 |  200306   48862   802553    16.4 |  1.714 % |
c |     50541 |  451477  1210454 |  220336   49199   805305    16.4 |  1.715 % |
c |     51047 |  451469  1210438 |  242370   49701   813331    16.4 |  1.717 % |
c |     51807 |  451407  1210311 |  266607   50419   822741    16.3 |  1.731 % |
c |     52946 |  451403  1210303 |  293268   51556   838881    16.3 |  1.732 % |
c ==============================================================================
c [1mFound solution: 55552[0m
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     54523 |  451397  1210256 |  150465   53120   857536    16.1 |  1.732 % |
c |     54624 |  451397  1210256 |  165511   53221   858625    16.1 |  1.743 % |
c |     54775 |  451387  1210231 |  182062   53367   861657    16.1 |  1.745 % |
c |     55000 |  451387  1210231 |  200268   53592   864883    16.1 |  1.745 % |
c |     55337 |  451387  1210231 |  220295   53929   871684    16.2 |  1.745 % |
c |     55843 |  451385  1210227 |  242325   54434   878554    16.1 |  1.746 % |
c |     56602 |  451383  1210223 |  266557   55192   888884    16.1 |  1.746 % |
c |     57741 |  451377  1210210 |  293213   56327   903447    16.0 |  1.748 % |
c |     59449 |  451365  1210186 |  322535   58029   929055    16.0 |  1.751 % |
c |     62011 |  451343  1210141 |  354788   60568   964224    15.9 |  1.756 % |
c |     65855 |  451195  1209841 |  390267   64293  1015337    15.8 |  1.790 % |
c ==============================================================================
c [1mFound solution: 54400[0m
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     70309 |  451109  1209703 |  150369   68672  1093294    15.9 |  1.790 % |
c |     70410 |  451109  1209703 |  165405   68773  1095291    15.9 |  1.824 % |
c |     70560 |  451109  1209703 |  181946   68923  1096731    15.9 |  1.824 % |
c |     70785 |  451107  1209699 |  200141   69147  1103123    16.0 |  1.824 % |
c |     71122 |  451107  1209699 |  220155   69484  1106561    15.9 |  1.824 % |
c |     71628 |  451095  1209675 |  242170   69984  1114109    15.9 |  1.827 % |
c |     72387 |  451089  1209663 |  266387   70740  1126155    15.9 |  1.828 % |
c |     73528 |  451085  1209655 |  293026   71879  1146622    16.0 |  1.829 % |
c |     75236 |  451063  1209609 |  322329   73507  1169681    15.9 |  1.834 % |
c |     77798 |  451043  1209568 |  354562   76054  1204707    15.8 |  1.840 % |
c |     81643 |  451021  1209524 |  390018   79889  1311394    16.4 |  1.844 % |
c |     87409 |  450909  1209281 |  429020   85559  1396867    16.3 |  1.870 % |
c |     96058 |  450731  1208913 |  471922   94071  1539171    16.4 |  1.911 % |
c ==============================================================================
c [1mFound solution: 53888[0m
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    101791 |  450735  1208934 |  150245   99791  1637659    16.4 |  1.911 % |
c |    101891 |  450735  1208934 |  165269   99891  1639065    16.4 |  1.917 % |
c |    102041 |  450733  1208930 |  181796  100040  1640864    16.4 |  1.917 % |
c |    102267 |  450727  1208918 |  199976  100263  1644211    16.4 |  1.919 % |
c |    102604 |  450727  1208918 |  219973  100600  1651405    16.4 |  1.919 % |
c ==============================================================================
c [1mFound solution: 53248[0m
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    102955 |  450698  1208835 |  150232  100942  1656454    16.4 |  1.919 % |
c |    103057 |  450698  1208835 |  165255  101044  1657455    16.4 |  1.935 % |
c |    103208 |  450698  1208835 |  181780  101195  1659892    16.4 |  1.935 % |
c |    103433 |  450696  1208831 |  199958  101419  1662859    16.4 |  1.935 % |
c |    103770 |  450696  1208831 |  219954  101756  1668015    16.4 |  1.935 % |
c |    104277 |  450688  1208814 |  241950  102221  1674755    16.4 |  1.937 % |
c ==============================================================================
c [1mFound solution: 52864[0m
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    104466 |  450711  1208870 |  150237  102410  1677178    16.4 |  1.937 % |
c |    104567 |  450707  1208862 |  165260  102509  1678011    16.4 |  1.938 % |
c |    104717 |  450707  1208862 |  181786  102659  1682614    16.4 |  1.938 % |
c |    104942 |  450707  1208862 |  199965  102884  1689821    16.4 |  1.938 % |
c |    105280 |  450707  1208862 |  219961  103222  1696537    16.4 |  1.938 % |
c |    105786 |  450707  1208862 |  241958  103728  1738330    16.8 |  1.938 % |
c |    106545 |  450703  1208854 |  266154  104485  1750932    16.8 |  1.939 % |
c |    107684 |  450703  1208854 |  292769  105624  1789119    16.9 |  1.939 % |
c |    109392 |  450701  1208850 |  322046  107331  1820403    17.0 |  1.940 % |
c |    111955 |  450689  1208826 |  354250  109888  1867471    17.0 |  1.942 % |
c ==============================================================================
c [1mFound solution: 52736[0m
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    112284 |  450622  1208646 |  150207  110190  1871916    17.0 |  1.942 % |
c |    112385 |  450622  1208646 |  165227  110291  1872827    17.0 |  1.963 % |
c |    112537 |  450622  1208646 |  181750  110443  1875025    17.0 |  1.963 % |
c |    112763 |  450618  1208636 |  199925  110661  1878513    17.0 |  1.963 % |
c |    113101 |  450618  1208636 |  219918  110999  1883889    17.0 |  1.963 % |
c |    113607 |  450616  1208632 |  241909  111504  1895973    17.0 |  1.964 % |
c |    114366 |  450612  1208624 |  266100  112261  1922064    17.1 |  1.965 % |
c |    115505 |  450608  1208616 |  292710  113398  1949320    17.2 |  1.966 % |
c |    117214 |  450596  1208592 |  321982  115101  1982618    17.2 |  1.969 % |
c ==============================================================================
c [1mFound solution: 52608[0m
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    118347 |  450605  1208617 |  150201  116232  2002698    17.2 |  1.969 % |
c |    118447 |  450605  1208617 |  165221  116332  2004315    17.2 |  1.970 % |
c |    118597 |  450603  1208613 |  181743  116481  2006770    17.2 |  1.970 % |
c |    118822 |  450603  1208613 |  199917  116706  2012190    17.2 |  1.970 % |
c |    119159 |  450603  1208613 |  219909  117043  2017985    17.2 |  1.970 % |
c |    119668 |  450601  1208609 |  241900  117551  2028378    17.3 |  1.971 % |
c |    120427 |  450593  1208593 |  266090  118306  2064160    17.4 |  1.973 % |
c |    121566 |  450575  1208549 |  292699  119350  2101987    17.6 |  1.977 % |
c |    123276 |  450557  1208509 |  321969  121042  2129500    17.6 |  1.981 % |
c |    125838 |  450531  1208448 |  354166  123577  2232019    18.1 |  1.987 % |
c ==============================================================================
c [1mFound solution: 52480[0m
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    126634 |  450508  1208376 |  150169  124319  2245024    18.1 |  1.987 % |
c |    126734 |  450504  1208367 |  165185  124415  2246050    18.1 |  1.996 % |
c |    126884 |  450504  1208367 |  181704  124565  2247277    18.0 |  1.996 % |
c |    127109 |  450474  1208305 |  199874  124764  2253231    18.1 |  2.002 % |
c |    127447 |  450472  1208301 |  219862  125101  2259488    18.1 |  2.003 % |
c |    127953 |  450472  1208301 |  241848  125607  2278182    18.1 |  2.003 % |
c ==============================================================================
c [1mFound solution: 52352[0m
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    128408 |  450486  1208337 |  150162  126062  2296100    18.2 |  2.003 % |
c |    128509 |  450484  1208333 |  165178  126162  2297487    18.2 |  2.004 % |
c |    128660 |  450484  1208333 |  181696  126313  2299650    18.2 |  2.004 % |
c |    128885 |  450484  1208333 |  199865  126538  2303330    18.2 |  2.004 % |
c |    129222 |  450482  1208328 |  219852  126874  2306571    18.2 |  2.004 % |
c |    129730 |  450478  1208320 |  241837  127380  2312729    18.2 |  2.005 % |
c ==============================================================================
c [1mFound solution: 52224[0m
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    130369 |  450423  1208165 |  150141  127940  2315501    18.1 |  2.005 % |
c |    130469 |  450423  1208165 |  165155  128040  2316664    18.1 |  2.022 % |
c |    130621 |  450423  1208165 |  181670  128192  2319917    18.1 |  2.022 % |
c |    130846 |  450421  1208161 |  199837  128416  2323874    18.1 |  2.023 % |
c |    131185 |  450421  1208161 |  219821  128755  2331385    18.1 |  2.023 % |
c |    131692 |  450421  1208161 |  241803  129262  2344242    18.1 |  2.023 % |
c ==============================================================================
c [1mFound solution: 52096[0m
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    132043 |  450434  1208194 |  150144  129613  2352343    18.1 |  2.023 % |
c |    132144 |  450434  1208194 |  165158  129714  2353668    18.1 |  2.023 % |
c |    132294 |  450434  1208194 |  181674  129864  2360225    18.2 |  2.023 % |
c |    132519 |  450434  1208194 |  199841  130089  2363243    18.2 |  2.023 % |
c |    132857 |  450428  1208182 |  219825  130424  2370772    18.2 |  2.024 % |
c |    133363 |  450428  1208182 |  241808  130930  2378908    18.2 |  2.024 % |
c |    134124 |  450422  1208168 |  265989  131667  2415766    18.3 |  2.026 % |
c |    135263 |  450416  1208156 |  292588  132803  2441577    18.4 |  2.027 % |
c |    136973 |  450412  1208146 |  321846  134511  2495546    18.6 |  2.028 % |
c ==============================================================================
c [1mFound solution: 51968[0m
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    138024 |  450377  1208034 |  150125  135463  2522404    18.6 |  2.028 % |
c |    138124 |  450377  1208034 |  165137  135563  2523417    18.6 |  2.039 % |
c |    138274 |  450377  1208034 |  181651  135713  2533126    18.7 |  2.039 % |
c |    138499 |  450377  1208034 |  199816  135938  2537337    18.7 |  2.039 % |
c |    138836 |  450375  1208030 |  219798  136274  2544218    18.7 |  2.039 % |
c |    139342 |  450373  1208026 |  241777  136779  2554707    18.7 |  2.040 % |
c |    140102 |  450371  1208022 |  265955  137538  2579337    18.8 |  2.040 % |
c |    141242 |  450363  1208006 |  292551  138674  2612583    18.8 |  2.042 % |
/oldhome/oroussel/solvers/minisat+_script: line 9: 21035 CPU time limit exceeded $XDIR/minisat+_64-bit_static -try "$@"
#### END SOLVER DATA ####
#### BEGIN WATCHER DATA ####
Enforcing CPU limit (will send SIGTERM then SIGKILL): 1200 seconds
Enforcing CPUTime (will send SIGXCPU) limit: 1230 seconds
Enforcing VSIZE limit: 943718400 bytes
Raw data (loadavg): 0.93 0.98 0.92 2/54 21031
Raw data (stat): 21031 (runsolver) R 21030 25830 25829 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 797244539 1052672 99 4294967295 134512640 135381576 3221224464 3221219672 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.0007 s]
Raw data (loadavg): 0.94 0.98 0.92 2/55 21035
Raw data (stat): 21031 (minisat+_script) S 21030 25830 25829 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 797244539 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+20.0012 s]
Raw data (loadavg): 0.95 0.98 0.92 2/55 21035
Raw data (stat): 21031 (minisat+_script) S 21030 25830 25829 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 797244539 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+30.0019 s]
Raw data (loadavg): 0.95 0.98 0.92 2/55 21035
Raw data (stat): 21031 (minisat+_script) S 21030 25830 25829 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 797244539 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+40.0021 s]
Raw data (loadavg): 0.96 0.98 0.92 2/55 21035
Raw data (stat): 21031 (minisat+_script) S 21030 25830 25829 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 797244539 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+50.0024 s]
Raw data (loadavg): 0.97 0.98 0.92 2/55 21035
Raw data (stat): 21031 (minisat+_script) S 21030 25830 25829 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 797244539 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+60.0022 s]
Raw data (loadavg): 0.97 0.98 0.92 2/55 21035
Raw data (stat): 21031 (minisat+_script) S 21030 25830 25829 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 797244539 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+70.0084 s]
Raw data (loadavg): 0.97 0.98 0.92 2/55 21035
Raw data (stat): 21031 (minisat+_script) S 21030 25830 25829 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 797244539 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+80.0088 s]
Raw data (loadavg): 0.98 0.98 0.92 2/55 21035
Raw data (stat): 21031 (minisat+_script) S 21030 25830 25829 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 797244539 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+90.0086 s]
Raw data (loadavg): 0.98 0.98 0.92 2/55 21035
Raw data (stat): 21031 (minisat+_script) S 21030 25830 25829 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 797244539 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+100.009 s]
Raw data (loadavg): 0.98 0.98 0.92 2/55 21035
Raw data (stat): 21031 (minisat+_script) S 21030 25830 25829 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 797244539 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+110.01 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 21035
Raw data (stat): 21031 (minisat+_script) S 21030 25830 25829 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 797244539 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+120.01 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 21035
Raw data (stat): 21031 (minisat+_script) S 21030 25830 25829 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 797244539 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+130.011 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 21035
Raw data (stat): 21031 (minisat+_script) S 21030 25830 25829 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 797244539 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+140.011 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 21035
Raw data (stat): 21031 (minisat+_script) S 21030 25830 25829 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 797244539 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+150.01 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 21035
Raw data (stat): 21031 (minisat+_script) S 21030 25830 25829 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 797244539 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+160.01 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 21035
Raw data (stat): 21031 (minisat+_script) S 21030 25830 25829 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 797244539 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+170.01 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 21035
Raw data (stat): 21031 (minisat+_script) S 21030 25830 25829 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 797244539 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+180.011 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 21035
Raw data (stat): 21031 (minisat+_script) S 21030 25830 25829 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 797244539 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+190.012 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 21035
Raw data (stat): 21031 (minisat+_script) S 21030 25830 25829 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 797244539 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+200.011 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 21035
Raw data (stat): 21031 (minisat+_script) S 21030 25830 25829 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 797244539 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+210.011 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 21035
Raw data (stat): 21031 (minisat+_script) S 21030 25830 25829 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 797244539 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+220.011 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 21035
Raw data (stat): 21031 (minisat+_script) S 21030 25830 25829 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 797244539 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+230.012 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 21035
Raw data (stat): 21031 (minisat+_script) S 21030 25830 25829 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 797244539 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+240.012 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 21035
Raw data (stat): 21031 (minisat+_script) S 21030 25830 25829 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 797244539 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+250.013 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 21035
Raw data (stat): 21031 (minisat+_script) S 21030 25830 25829 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 797244539 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+260.013 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 21035
Raw data (stat): 21031 (minisat+_script) S 21030 25830 25829 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 797244539 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+270.013 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 21035
Raw data (stat): 21031 (minisat+_script) S 21030 25830 25829 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 797244539 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+280.013 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 21035
Raw data (stat): 21031 (minisat+_script) S 21030 25830 25829 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 797244539 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+290.014 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 21035
Raw data (stat): 21031 (minisat+_script) S 21030 25830 25829 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 797244539 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+300.013 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 21035
Raw data (stat): 21031 (minisat+_script) S 21030 25830 25829 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 797244539 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+310.013 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 21035
Raw data (stat): 21031 (minisat+_script) S 21030 25830 25829 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 797244539 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+320.013 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 21035
Raw data (stat): 21031 (minisat+_script) S 21030 25830 25829 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 797244539 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+330.014 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 21035
Raw data (stat): 21031 (minisat+_script) S 21030 25830 25829 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 797244539 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+340.014 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 21035
Raw data (stat): 21031 (minisat+_script) S 21030 25830 25829 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 797244539 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+350.013 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 21035
Raw data (stat): 21031 (minisat+_script) S 21030 25830 25829 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 797244539 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+360.014 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 21035
Raw data (stat): 21031 (minisat+_script) S 21030 25830 25829 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 797244539 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+370.014 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 21035
Raw data (stat): 21031 (minisat+_script) S 21030 25830 25829 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 797244539 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+380.014 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 21035
Raw data (stat): 21031 (minisat+_script) S 21030 25830 25829 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 797244539 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+390.014 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 21035
Raw data (stat): 21031 (minisat+_script) S 21030 25830 25829 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 797244539 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+400.014 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 21035
Raw data (stat): 21031 (minisat+_script) S 21030 25830 25829 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 797244539 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+410.015 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 21035
Raw data (stat): 21031 (minisat+_script) S 21030 25830 25829 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 797244539 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+420.015 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 21035
Raw data (stat): 21031 (minisat+_script) S 21030 25830 25829 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 797244539 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+430.021 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 21035
Raw data (stat): 21031 (minisat+_script) S 21030 25830 25829 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 797244539 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+440.02 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 21035
Raw data (stat): 21031 (minisat+_script) S 21030 25830 25829 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 797244539 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+450.02 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 21035
Raw data (stat): 21031 (minisat+_script) S 21030 25830 25829 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 797244539 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+460.02 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 21035
Raw data (stat): 21031 (minisat+_script) S 21030 25830 25829 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 797244539 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+470.021 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 21035
Raw data (stat): 21031 (minisat+_script) S 21030 25830 25829 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 797244539 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+480.021 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 21035
Raw data (stat): 21031 (minisat+_script) S 21030 25830 25829 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 797244539 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+490.021 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 21035
Raw data (stat): 21031 (minisat+_script) S 21030 25830 25829 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 797244539 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+500.021 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 21035
Raw data (stat): 21031 (minisat+_script) S 21030 25830 25829 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 797244539 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+510.021 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 21035
Raw data (stat): 21031 (minisat+_script) S 21030 25830 25829 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 797244539 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+520.021 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 21035
Raw data (stat): 21031 (minisat+_script) S 21030 25830 25829 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 797244539 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+530.022 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 21035
Raw data (stat): 21031 (minisat+_script) S 21030 25830 25829 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 797244539 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+540.022 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 21035
Raw data (stat): 21031 (minisat+_script) S 21030 25830 25829 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 797244539 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+550.022 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 21035
Raw data (stat): 21031 (minisat+_script) S 21030 25830 25829 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 797244539 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+560.023 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 21035
Raw data (stat): 21031 (minisat+_script) S 21030 25830 25829 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 797244539 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+570.022 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 21035
Raw data (stat): 21031 (minisat+_script) S 21030 25830 25829 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 797244539 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+580.024 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 21035
Raw data (stat): 21031 (minisat+_script) S 21030 25830 25829 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 797244539 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+590.024 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 21035
Raw data (stat): 21031 (minisat+_script) S 21030 25830 25829 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 797244539 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+600.024 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 21035
Raw data (stat): 21031 (minisat+_script) S 21030 25830 25829 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 797244539 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+610.025 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 21035
Raw data (stat): 21031 (minisat+_script) S 21030 25830 25829 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 797244539 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+620.024 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 21035
Raw data (stat): 21031 (minisat+_script) S 21030 25830 25829 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 797244539 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+630.025 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 21035
Raw data (stat): 21031 (minisat+_script) S 21030 25830 25829 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 797244539 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+640.026 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 21035
Raw data (stat): 21031 (minisat+_script) S 21030 25830 25829 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 797244539 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+650.026 s]
Raw data (loadavg): 1.07 1.00 0.93 2/55 21035
Raw data (stat): 21031 (minisat+_script) S 21030 25830 25829 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 797244539 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+660.027 s]
Raw data (loadavg): 1.06 1.00 0.93 2/55 21035
Raw data (stat): 21031 (minisat+_script) S 21030 25830 25829 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 797244539 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+670.027 s]
Raw data (loadavg): 1.05 1.00 0.93 2/55 21035
Raw data (stat): 21031 (minisat+_script) S 21030 25830 25829 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 797244539 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+680.027 s]
Raw data (loadavg): 1.04 1.00 0.93 2/55 21035
Raw data (stat): 21031 (minisat+_script) S 21030 25830 25829 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 797244539 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+690.027 s]
Raw data (loadavg): 1.04 1.00 0.93 2/55 21035
Raw data (stat): 21031 (minisat+_script) S 21030 25830 25829 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 797244539 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+700.027 s]
Raw data (loadavg): 1.03 1.00 0.93 2/55 21035
Raw data (stat): 21031 (minisat+_script) S 21030 25830 25829 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 797244539 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+710.028 s]
Raw data (loadavg): 1.03 1.00 0.93 2/55 21035
Raw data (stat): 21031 (minisat+_script) S 21030 25830 25829 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 797244539 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+720.027 s]
Raw data (loadavg): 1.02 1.00 0.93 2/55 21035
Raw data (stat): 21031 (minisat+_script) S 21030 25830 25829 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 797244539 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+730.029 s]
Raw data (loadavg): 1.02 1.00 0.93 2/55 21035
Raw data (stat): 21031 (minisat+_script) S 21030 25830 25829 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 797244539 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+740.029 s]
Raw data (loadavg): 1.01 1.00 0.93 2/55 21035
Raw data (stat): 21031 (minisat+_script) S 21030 25830 25829 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 797244539 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+750.029 s]
Raw data (loadavg): 1.01 1.00 0.93 2/55 21035
Raw data (stat): 21031 (minisat+_script) S 21030 25830 25829 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 797244539 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+760.029 s]
Raw data (loadavg): 1.01 1.00 0.93 2/55 21035
Raw data (stat): 21031 (minisat+_script) S 21030 25830 25829 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 797244539 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+770.029 s]
Raw data (loadavg): 1.01 1.00 0.93 2/55 21035
Raw data (stat): 21031 (minisat+_script) S 21030 25830 25829 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 797244539 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+780.029 s]
Raw data (loadavg): 1.01 1.00 0.93 2/55 21035
Raw data (stat): 21031 (minisat+_script) S 21030 25830 25829 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 797244539 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+790.029 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 21035
Raw data (stat): 21031 (minisat+_script) S 21030 25830 25829 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 797244539 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+800.029 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 21035
Raw data (stat): 21031 (minisat+_script) S 21030 25830 25829 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 797244539 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+810.029 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 21035
Raw data (stat): 21031 (minisat+_script) S 21030 25830 25829 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 797244539 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+820.03 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 21035
Raw data (stat): 21031 (minisat+_script) S 21030 25830 25829 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 797244539 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+830.03 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 21035
Raw data (stat): 21031 (minisat+_script) S 21030 25830 25829 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 797244539 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+840.031 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 21035
Raw data (stat): 21031 (minisat+_script) S 21030 25830 25829 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 797244539 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+850.031 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 21035
Raw data (stat): 21031 (minisat+_script) S 21030 25830 25829 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 797244539 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+860.031 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 21035
Raw data (stat): 21031 (minisat+_script) S 21030 25830 25829 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 797244539 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+870.031 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 21035
Raw data (stat): 21031 (minisat+_script) S 21030 25830 25829 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 797244539 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+880.032 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 21035
Raw data (stat): 21031 (minisat+_script) S 21030 25830 25829 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 797244539 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+890.033 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 21035
Raw data (stat): 21031 (minisat+_script) S 21030 25830 25829 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 797244539 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+900.033 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 21035
Raw data (stat): 21031 (minisat+_script) S 21030 25830 25829 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 797244539 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+910.033 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 21035
Raw data (stat): 21031 (minisat+_script) S 21030 25830 25829 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 797244539 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+920.033 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 21035
Raw data (stat): 21031 (minisat+_script) S 21030 25830 25829 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 797244539 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+930.034 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 21035
Raw data (stat): 21031 (minisat+_script) S 21030 25830 25829 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 797244539 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+940.034 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 21035
Raw data (stat): 21031 (minisat+_script) S 21030 25830 25829 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 797244539 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+950.035 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 21035
Raw data (stat): 21031 (minisat+_script) S 21030 25830 25829 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 797244539 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+960.035 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 21035
Raw data (stat): 21031 (minisat+_script) S 21030 25830 25829 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 797244539 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+970.035 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 21035
Raw data (stat): 21031 (minisat+_script) S 21030 25830 25829 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 797244539 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+980.036 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 21035
Raw data (stat): 21031 (minisat+_script) S 21030 25830 25829 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 797244539 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+990.037 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 21035
Raw data (stat): 21031 (minisat+_script) S 21030 25830 25829 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 797244539 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1000.04 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 21035
Raw data (stat): 21031 (minisat+_script) S 21030 25830 25829 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 797244539 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1010.04 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 21035
Raw data (stat): 21031 (minisat+_script) S 21030 25830 25829 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 797244539 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1020.04 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 21035
Raw data (stat): 21031 (minisat+_script) S 21030 25830 25829 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 797244539 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1030.04 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 21035
Raw data (stat): 21031 (minisat+_script) S 21030 25830 25829 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 797244539 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1040.04 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 21035
Raw data (stat): 21031 (minisat+_script) S 21030 25830 25829 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 797244539 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1050.04 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 21035
Raw data (stat): 21031 (minisat+_script) S 21030 25830 25829 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 797244539 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1060.04 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 21035
Raw data (stat): 21031 (minisat+_script) S 21030 25830 25829 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 797244539 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1070.04 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 21035
Raw data (stat): 21031 (minisat+_script) S 21030 25830 25829 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 797244539 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1080.04 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 21035
Raw data (stat): 21031 (minisat+_script) S 21030 25830 25829 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 797244539 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1090.04 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 21035
Raw data (stat): 21031 (minisat+_script) S 21030 25830 25829 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 797244539 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1100.04 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 21035
Raw data (stat): 21031 (minisat+_script) S 21030 25830 25829 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 797244539 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1110.04 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 21035
Raw data (stat): 21031 (minisat+_script) S 21030 25830 25829 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 797244539 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1120.04 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 21035
Raw data (stat): 21031 (minisat+_script) S 21030 25830 25829 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 797244539 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1130.04 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 21035
Raw data (stat): 21031 (minisat+_script) S 21030 25830 25829 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 797244539 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1140.04 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 21035
Raw data (stat): 21031 (minisat+_script) S 21030 25830 25829 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 797244539 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1150.04 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 21035
Raw data (stat): 21031 (minisat+_script) S 21030 25830 25829 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 797244539 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1160.04 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 21035
Raw data (stat): 21031 (minisat+_script) S 21030 25830 25829 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 797244539 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1170.04 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 21035
Raw data (stat): 21031 (minisat+_script) S 21030 25830 25829 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 797244539 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1180.04 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 21035
Raw data (stat): 21031 (minisat+_script) S 21030 25830 25829 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 797244539 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1190.04 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 21035
Raw data (stat): 21031 (minisat+_script) S 21030 25830 25829 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 797244539 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1200.04 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 21035
Raw data (stat): 21031 (minisat+_script) S 21030 25830 25829 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 797244539 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1210.04 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 21035
Raw data (stat): 21031 (minisat+_script) S 21030 25830 25829 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 797244539 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1220.04 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 21035
Raw data (stat): 21031 (minisat+_script) S 21030 25830 25829 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 797244539 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1229.72 s]
Raw data (loadavg): 1.00 1.00 0.93 1/53 21035
Raw data (stat): 21031 (minisat+_script) S 21030 25830 25829 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 797244539 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 0

Child status: 152
Real time (s): 1229.72
CPU time (s): 1229.87
CPU user time (s): 1229.15
CPU system time (s): 0.724889
CPU usage (%): 100.013
Max. virtual memory (Kb): 2124
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####