PB'05 competition: run trace

Some explanations

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

Name	normalized-opb/mps-v2-20-10/plato.asu.edu/pub/unibo/normalized-mps-v2-20-10-railway_8_1_0.opb
MD5SUM	7bc553fee464cd071c8e3d02b13f4c95
Bench Category	optimization, big integers (OPTBIGINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	499712
Optimality of the best value was proved	NO
Number of terms in the objective function	133
Biggest coefficient in the objective function	536870912
Number of bits for the biggest coefficient in the objective function	30
Sum of the numbers in the objective function	1073847295
Number of bits of the sum of numbers in the objective function	31
Biggest number in a constraint	1024000000
Number of bits of the biggest number in a constraint	30
Biggest sum of numbers in a constraint	2147758078
Number of bits of the biggest sum of numbers	32
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	1201.13
Number of variables	19747
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	61
Trace number 30972

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc4 THE 2005-05-25 21:10:36 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=22353 boxname=wulflinc4 idbench=1169 idsolver=15 numberseed=0
MD5SUM SOLVER: 34d34154b8ad81f02ee98439942e0814  /oldhome/oroussel/solvers/minisat+_script
MD5SUM BENCH:  7bc553fee464cd071c8e3d02b13f4c95  /oldhome/oroussel/tmp/wulflinc4/normalized-mps-v2-20-10-railway_8_1_0.opb
REAL COMMAND:  minisat+_script /oldhome/oroussel/tmp/wulflinc4/normalized-mps-v2-20-10-railway_8_1_0.opb
IDLAUNCH: 22353
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.169
cache size	: 512 KB
fdiv_bug	: no
hlt_bug		: no
f00f_bug	: no
coma_bug	: no
fpu		: yes
fpu_exception	: yes
cpuid level	: 2
wp		: yes
flags		: fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse
bogomips	: 890.88

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.169
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:        865728 kB
Buffers:         28652 kB
Cached:         119836 kB
SwapCached:        500 kB
Active:          32936 kB
Inactive:       117940 kB
HighTotal:      131008 kB
HighFree:        18256 kB
LowTotal:       903652 kB
LowFree:        847472 kB
SwapTotal:     2097136 kB
SwapFree:      2096004 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           5784 kB
Slab:            12428 kB
Committed_AS:    71796 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1388 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-05-25 21:31:06 (client local time) WITH STATUS 152 IN 1229.88 SECONDS
stats: 22353 7 1229.88 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:   88
c ---[3139]---> BDD-cost:   88
c ---[3138]---> BDD-cost:   88
c ---[3137]---> BDD-cost:  121
c ---[3136]---> BDD-cost:  119
c ---[3135]---> BDD-cost:   88
c ---[3134]---> BDD-cost:   88
c ---[3133]---> BDD-cost:   88
c ---[3132]---> BDD-cost:   88
c ---[3131]---> BDD-cost:  119
c ---[3129]---> BDD-cost:  119
c ---[3128]---> BDD-cost:   88
c ---[3127]---> BDD-cost:   88
c ---[3126]---> BDD-cost:   88
c ---[3125]---> BDD-cost:   88
c ---[3124]---> BDD-cost:  121
c ---[3123]---> BDD-cost:  119
c ---[3122]---> BDD-cost:   88
c ---[3121]---> BDD-cost:   88
c ---[3120]---> BDD-cost:   88
c ---[3118]---> BDD-cost:   88
c ---[3117]---> BDD-cost:  123
c ---[3116]---> BDD-cost:  119
c ---[3115]---> BDD-cost:   88
c ---[3114]---> BDD-cost:   88
c ---[3113]---> BDD-cost:   88
c ---[3112]---> BDD-cost:   88
c ---[3111]---> BDD-cost:  123
c ---[3110]---> BDD-cost:  119
c ---[3109]---> BDD-cost:   88
c ---[3107]---> BDD-cost:   88
c ---[3106]---> BDD-cost:   88
c ---[3105]---> BDD-cost:   88
c ---[3104]---> BDD-cost:  121
c ---[3103]---> BDD-cost:  119
c ---[3102]---> BDD-cost:   88
c ---[3101]---> BDD-cost:   88
c ---[3100]---> BDD-cost:   88
c ---[3099]---> BDD-cost:   88
c ---[3098]---> BDD-cost:  125
c ---[3096]---> BDD-cost:  119
c ---[3095]---> BDD-cost:   88
c ---[3094]---> BDD-cost:   88
c ---[3093]---> BDD-cost:   88
c ---[3092]---> BDD-cost:   88
c ---[3090]---> BDD-cost:  125
c ---[3088]---> BDD-cost:  123
c ---[3087]---> BDD-cost:  125
c ---[3085]---> BDD-cost:  125
c ---[3083]---> BDD-cost:  125
c ---[3081]---> BDD-cost:  123
c ---[3079]---> BDD-cost:  125
c ---[3077]---> BDD-cost:  125
c ---[3076]---> BDD-cost:  125
c ---[3074]---> BDD-cost:  125
c ---[3072]---> BDD-cost:  125
c ---[3070]---> BDD-cost:  123
c ---[3068]---> BDD-cost:  123
c ---[3066]---> BDD-cost:  125
c ---[3065]---> BDD-cost:  123
c ---[3063]---> BDD-cost:  123
c ---[3061]---> BDD-cost:   88
c ---[3059]---> BDD-cost:  125
c ---[3057]---> BDD-cost:  125
c ---[3055]---> BDD-cost:  125
c ---[3054]---> BDD-cost:  123
c ---[3052]---> BDD-cost:  123
c ---[3050]---> BDD-cost:  125
c ---[3048]---> BDD-cost:  123
c ---[3046]---> BDD-cost:  125
c ---[3044]---> BDD-cost:  125
c ---[3043]---> BDD-cost:  125
c ---[3041]---> BDD-cost:  125
c ---[3039]---> BDD-cost:   88
c ---[3037]---> BDD-cost:   88
c ---[3035]---> BDD-cost:  123
c ---[3033]---> BDD-cost:  121
c ---[3032]---> BDD-cost:  123
c ---[3029]---> BDD-cost:  123
c ---[3027]---> BDD-cost:  121
c ---[3025]---> BDD-cost:  125
c ---[3023]---> BDD-cost:  123
c ---[3021]---> BDD-cost:  125
c ---[3020]---> BDD-cost:  123
c ---[3018]---> BDD-cost:  123
c ---[3016]---> BDD-cost:  123
c ---[3014]---> BDD-cost:  125
c ---[3012]---> BDD-cost:  125
c ---[3010]---> BDD-cost:  121
c ---[3009]---> BDD-cost:  119
c ---[3007]---> BDD-cost:  119
c ---[3005]---> BDD-cost:  119
c ---[3003]---> BDD-cost:  119
c ---[3001]---> BDD-cost:  123
c ---[2999]---> BDD-cost:  125
c ---[2998]---> BDD-cost:  125
c ---[2996]---> BDD-cost:  125
c ---[2994]---> BDD-cost:   88
c ---[2992]---> BDD-cost:  125
c ---[2990]---> BDD-cost:  123
c ---[2988]---> BDD-cost:  125
c ---[2987]---> BDD-cost:  125
c ---[2985]---> BDD-cost:  125
c ---[2983]---> BDD-cost:  125
c ---[2981]---> BDD-cost:  123
c ---[2979]---> BDD-cost:  125
c ---[2977]---> BDD-cost:  121
c ---[2976]---> BDD-cost:  125
c ---[2974]---> BDD-cost:  125
c ---[2972]---> BDD-cost:  121
c ---[2970]---> BDD-cost:  125
c ---[2968]---> BDD-cost:  123
c ---[2966]---> BDD-cost:  125
c ---[2965]---> BDD-cost:  123
c ---[2963]---> BDD-cost:  123
c ---[2961]---> BDD-cost:  123
c ---[2959]---> BDD-cost:   88
c ---[2957]---> BDD-cost:  123
c ---[2955]---> BDD-cost:  123
c ---[2954]---> BDD-cost:  125
c ---[2952]---> BDD-cost:  125
c ---[2950]---> BDD-cost:   88
c ---[2948]---> BDD-cost:  123
c ---[2946]---> BDD-cost:  123
c ---[2944]---> BDD-cost:  125
c ---[2943]---> BDD-cost:  123
c ---[2941]---> BDD-cost:  123
c ---[2939]---> BDD-cost:  125
c ---[2937]---> BDD-cost:  125
c ---[2935]---> BDD-cost:  123
c ---[2933]---> BDD-cost:  123
c ---[2932]---> BDD-cost:  121
c ---[2930]---> BDD-cost:  121
c ---[2928]---> BDD-cost:  123
c ---[2926]---> BDD-cost:  125
c ---[2924]---> BDD-cost:  123
c ---[2922]---> BDD-cost:   88
c ---[2921]---> BDD-cost:  125
c ---[2918]---> BDD-cost:  125
c ---[2916]---> BDD-cost:  123
c ---[2914]---> BDD-cost:  125
c ---[2912]---> BDD-cost:   88
c ---[2910]---> BDD-cost:  125
c ---[2909]---> BDD-cost:  123
c ---[2907]---> BDD-cost:  123
c ---[2905]---> BDD-cost:  121
c ---[2903]---> BDD-cost:  123
c ---[2901]---> BDD-cost:   88
c ---[2899]---> BDD-cost:  121
c ---[2898]---> BDD-cost:  125
c ---[2896]---> BDD-cost:  125
c ---[2894]---> BDD-cost:  123
c ---[2892]---> BDD-cost:  125
c ---[2890]---> BDD-cost:  125
c ---[2888]---> BDD-cost:  123
c ---[2887]---> BDD-cost:  125
c ---[2885]---> BDD-cost:  125
c ---[2883]---> BDD-cost:   88
c ---[2881]---> BDD-cost:  125
c ---[2879]---> BDD-cost:  123
c ---[2877]---> BDD-cost:  125
c ---[2876]---> BDD-cost:  121
c ---[2874]---> BDD-cost:  121
c ---[2872]---> BDD-cost:  121
c ---[2870]---> BDD-cost:  119
c ---[2868]---> BDD-cost:  125
c ---[2866]---> BDD-cost:  123
c ---[2865]---> BDD-cost:  123
c ---[2863]---> BDD-cost:  123
c ---[2861]---> BDD-cost:  125
c ---[2859]---> BDD-cost:   88
c ---[2857]---> BDD-cost:  123
c ---[2855]---> BDD-cost:  125
c ---[2854]---> BDD-cost:   88
c ---[2852]---> BDD-cost:   88
c ---[2850]---> BDD-cost:  125
c ---[2848]---> BDD-cost:  125
c ---[2846]---> BDD-cost:  125
c ---[2844]---> BDD-cost:  125
c ---[2843]---> BDD-cost:  123
c ---[2841]---> BDD-cost:  123
c ---[2839]---> BDD-cost:  125
c ---[2837]---> BDD-cost:  123
c ---[2835]---> BDD-cost:  123
c ---[2833]---> BDD-cost:  123
c ---[2832]---> BDD-cost:   88
c ---[2830]---> BDD-cost:   88
c ---[2828]---> BDD-cost:  125
c ---[2826]---> BDD-cost:  125
c ---[2824]---> BDD-cost:  121
c ---[2822]---> BDD-cost:  125
c ---[2821]---> BDD-cost:  125
c ---[2819]---> BDD-cost:  125
c ---[2817]---> BDD-cost:   88
c ---[2815]---> BDD-cost:  125
c ---[2813]---> BDD-cost:  123
c ---[2811]---> BDD-cost:  125
c ---[2810]---> BDD-cost:  125
c ---[2807]---> BDD-cost:  125
c ---[2805]---> BDD-cost:  125
c ---[2803]---> BDD-cost:  125
c ---[2801]---> BDD-cost:   88
c ---[2799]---> BDD-cost:  125
c ---[2798]---> BDD-cost:  125
c ---[2796]---> BDD-cost:  125
c ---[2794]---> BDD-cost:   88
c ---[2792]---> BDD-cost:  125
c ---[2790]---> BDD-cost:  123
c ---[2788]---> BDD-cost:  125
c ---[2787]---> BDD-cost:  125
c ---[2785]---> BDD-cost:  125
c ---[2783]---> BDD-cost:  123
c ---[2781]---> BDD-cost:   88
c ---[2779]---> BDD-cost:   88
c ---[2777]---> BDD-cost:  125
c ---[2776]---> BDD-cost:  125
c ---[2774]---> BDD-cost:  125
c ---[2772]---> BDD-cost:  125
c ---[2770]---> BDD-cost:   88
c ---[2768]---> BDD-cost:  121
c ---[2766]---> BDD-cost:  123
c ---[2765]---> BDD-cost:   88
c ---[2763]---> BDD-cost:   88
c ---[2761]---> BDD-cost:  125
c ---[2759]---> BDD-cost:   88
c ---[2757]---> BDD-cost:  123
c ---[2755]---> BDD-cost:   88
c ---[2754]---> BDD-cost:   88
c ---[2752]---> BDD-cost:   88
c ---[2750]---> BDD-cost:  125
c ---[2748]---> BDD-cost:  125
c ---[2746]---> BDD-cost:   88
c ---[2744]---> BDD-cost:   88
c ---[2743]---> BDD-cost:  125
c ---[2741]---> BDD-cost:  125
c ---[2739]---> BDD-cost:  125
c ---[2737]---> BDD-cost:  125
c ---[2735]---> BDD-cost:  125
c ---[2733]---> BDD-cost:  125
c ---[2732]---> BDD-cost:  125
c ---[2730]---> BDD-cost:  125
c ---[2728]---> BDD-cost:   88
c ---[2726]---> BDD-cost:  125
c ---[2724]---> BDD-cost:  125
c ---[2722]---> BDD-cost:   88
c ---[2721]---> BDD-cost:  125
c ---[2719]---> BDD-cost:  125
c ---[2717]---> BDD-cost:   88
c ---[2715]---> BDD-cost:   88
c ---[2713]---> BDD-cost:  125
c ---[2711]---> BDD-cost:   88
c ---[2710]---> BDD-cost:   88
c ---[2708]---> BDD-cost:   88
c ---[2706]---> BDD-cost:   88
c ---[2704]---> BDD-cost:  125
c ---[2702]---> BDD-cost:  125
c ---[2700]---> BDD-cost:   88
c ---[2699]---> BDD-cost:  125
c ---[2696]---> BDD-cost:  125
c ---[2694]---> BDD-cost:   88
c ---[2692]---> BDD-cost:  125
c ---[2690]---> BDD-cost:  123
c ---[2688]---> BDD-cost:   88
c ---[2687]---> BDD-cost:  125
c ---[2685]---> BDD-cost:  125
c ---[2683]---> BDD-cost:  125
c ---[2681]---> BDD-cost:  125
c ---[2679]---> BDD-cost:  121
c ---[2677]---> BDD-cost:  125
c ---[2676]---> BDD-cost:  123
c ---[2674]---> BDD-cost:  123
c ---[2672]---> BDD-cost:  123
c ---[2670]---> BDD-cost:   88
c ---[2668]---> BDD-cost:  125
c ---[2666]---> BDD-cost:  121
c ---[2665]---> BDD-cost:  125
c ---[2663]---> BDD-cost:  125
c ---[2661]---> BDD-cost:  125
c ---[2659]---> BDD-cost:  123
c ---[2657]---> BDD-cost:  123
c ---[2655]---> BDD-cost:   88
c ---[2654]---> BDD-cost:  125
c ---[2652]---> BDD-cost:  125
c ---[2650]---> BDD-cost:  125
c ---[2648]---> BDD-cost:  125
c ---[2646]---> BDD-cost:   88
c ---[2644]---> BDD-cost:  123
c ---[2643]---> BDD-cost:  121
c ---[2641]---> BDD-cost:  121
c ---[2639]---> BDD-cost:  119
c ---[2638]---> BDD-cost:  128
c ---[2637]---> BDD-cost:  128
c ---[2636]---> BDD-cost:  137
c ---[2635]---> BDD-cost:  137
c ---[2634]---> BDD-cost:  140
c ---[2633]---> BDD-cost:  140
c ---[2632]---> BDD-cost:  137
c ---[2630]---> BDD-cost:  137
c ---[2629]---> BDD-cost:  135
c ---[2628]---> BDD-cost:  135
c ---[2627]---> BDD-cost:  137
c ---[2626]---> BDD-cost:  137
c ---[2625]---> BDD-cost:  143
c ---[2624]---> BDD-cost:  143
c ---[2623]---> BDD-cost:  137
c ---[2622]---> BDD-cost:  137
c ---[2621]---> BDD-cost:  135
c ---[2619]---> BDD-cost:  135
c ---[2618]---> BDD-cost:  137
c ---[2617]---> BDD-cost:  137
c ---[2616]---> BDD-cost:  140
c ---[2615]---> BDD-cost:  140
c ---[2614]---> BDD-cost:  137
c ---[2613]---> BDD-cost:  137
c ---[2612]---> BDD-cost:  138
c ---[2611]---> BDD-cost:  138
c ---[2610]---> BDD-cost:  137
c ---[2608]---> BDD-cost:  137
c ---[2607]---> BDD-cost:  143
c ---[2606]---> BDD-cost:  143
c ---[2605]---> BDD-cost:  137
c ---[2604]---> BDD-cost:  137
c ---[2603]---> BDD-cost:  140
c ---[2602]---> BDD-cost:  140
c ---[2601]---> BDD-cost:  137
c ---[2600]---> BDD-cost:  137
c ---[2599]---> BDD-cost:  130
c ---[2597]---> BDD-cost:  130
c ---[2596]---> BDD-cost:  137
c ---[2595]---> BDD-cost:  137
c ---[2594]---> BDD-cost:  146
c ---[2593]---> BDD-cost:  146
c ---[2592]---> BDD-cost:  137
c ---[2591]---> BDD-cost:  137
c ---[2590]---> BDD-cost:  133
c ---[2589]---> BDD-cost:  133
c ---[2588]---> BDD-cost:  137
c ---[2585]---> BDD-cost:  137
c ---[2584]---> BDD-cost:  138
c ---[2583]---> BDD-cost:  138
c ---[2582]---> BDD-cost:  137
c ---[2581]---> BDD-cost:  137
c ---[2580]---> BDD-cost:  146
c ---[2579]---> BDD-cost:  146
c ---[2578]---> BDD-cost:  137
c ---[2577]---> BDD-cost:  137
c ---[2576]---> BDD-cost:  143
c ---[2574]---> BDD-cost:  143
c ---[2573]---> BDD-cost:  137
c ---[2572]---> BDD-cost:  137
c ---[2571]---> BDD-cost:  143
c ---[2570]---> BDD-cost:  143
c ---[2569]---> BDD-cost:  137
c ---[2568]---> BDD-cost:  137
c ---[2567]---> BDD-cost:  143
c ---[2566]---> BDD-cost:  143
c ---[2565]---> BDD-cost:  137
c ---[2563]---> BDD-cost:  137
c ---[2562]---> BDD-cost:  138
c ---[2561]---> BDD-cost:  138
c ---[2560]---> BDD-cost:  137
c ---[2559]---> BDD-cost:  137
c ---[2558]---> BDD-cost:  140
c ---[2557]---> BDD-cost:  140
c ---[2556]---> BDD-cost:  137
c ---[2555]---> BDD-cost:  137
c ---[2554]---> BDD-cost:  143
c ---[2552]---> BDD-cost:  143
c ---[2551]---> BDD-cost:  137
c ---[2550]---> BDD-cost:  137
c ---[2549]---> BDD-cost:  141
c ---[2548]---> BDD-cost:  141
c ---[2547]---> BDD-cost:  137
c ---[2546]---> BDD-cost:  137
c ---[2545]---> BDD-cost:  140
c ---[2544]---> BDD-cost:  140
c ---[2543]---> BDD-cost:  137
c ---[2541]---> BDD-cost:  137
c ---[2540]---> BDD-cost:  140
c ---[2539]---> BDD-cost:  140
c ---[2538]---> BDD-cost:  137
c ---[2537]---> BDD-cost:  137
c ---[2536]---> BDD-cost:  143
c ---[2535]---> BDD-cost:  143
c ---[2534]---> BDD-cost:  137
c ---[2533]---> BDD-cost:  137
c ---[2532]---> BDD-cost:  140
c ---[2530]---> BDD-cost:  140
c ---[2529]---> BDD-cost:  137
c ---[2528]---> BDD-cost:  137
c ---[2527]---> BDD-cost:  140
c ---[2526]---> BDD-cost:  140
c ---[2525]---> BDD-cost:  137
c ---[2524]---> BDD-cost:  137
c ---[2523]---> BDD-cost:  140
c ---[2522]---> BDD-cost:  140
c ---[2521]---> BDD-cost:  137
c ---[2519]---> BDD-cost:  137
c ---[2518]---> BDD-cost:  143
c ---[2517]---> BDD-cost:  143
c ---[2516]---> BDD-cost:  137
c ---[2515]---> BDD-cost:  137
c ---[2514]---> BDD-cost:  140
c ---[2513]---> BDD-cost:  140
c ---[2512]---> BDD-cost:  137
c ---[2511]---> BDD-cost:  137
c ---[2510]---> BDD-cost:  140
c ---[2508]---> BDD-cost:  140
c ---[2507]---> BDD-cost:  137
c ---[2506]---> BDD-cost:  137
c ---[2505]---> BDD-cost:  143
c ---[2504]---> BDD-cost:  143
c ---[2503]---> BDD-cost:  137
c ---[2502]---> BDD-cost:  137
c ---[2501]---> BDD-cost:  143
c ---[2500]---> BDD-cost:  143
c ---[2499]---> BDD-cost:  137
c ---[2497]---> BDD-cost:  137
c ---[2496]---> BDD-cost:  143
c ---[2495]---> BDD-cost:  143
c ---[2494]---> BDD-cost:  137
c ---[2493]---> BDD-cost:  137
c ---[2492]---> BDD-cost:  140
c ---[2491]---> BDD-cost:  140
c ---[2490]---> BDD-cost:  137
c ---[2489]---> BDD-cost:  137
c ---[2488]---> BDD-cost:  143
c ---[2486]---> BDD-cost:  143
c ---[2485]---> BDD-cost:  137
c ---[2484]---> BDD-cost:  137
c ---[2483]---> BDD-cost:  140
c ---[2482]---> BDD-cost:  140
c ---[2481]---> BDD-cost:  137
c ---[2480]---> BDD-cost:  137
c ---[2479]---> BDD-cost:  128
c ---[2478]---> BDD-cost:  128
c ---[2477]---> BDD-cost:  137
c ---[2474]---> BDD-cost:  137
c ---[2473]---> BDD-cost:  138
c ---[2472]---> BDD-cost:  138
c ---[2471]---> BDD-cost:  137
c ---[2470]---> BDD-cost:  137
c ---[2469]---> BDD-cost:  133
c ---[2468]---> BDD-cost:  133
c ---[2467]---> BDD-cost:  137
c ---[2466]---> BDD-cost:  137
c ---[2465]---> BDD-cost:  140
c ---[2463]---> BDD-cost:  140
c ---[2462]---> BDD-cost:  137
c ---[2461]---> BDD-cost:  137
c ---[2460]---> BDD-cost:  140
c ---[2459]---> BDD-cost:  140
c ---[2458]---> BDD-cost:  137
c ---[2457]---> BDD-cost:  137
c ---[2456]---> BDD-cost:  140
c ---[2455]---> BDD-cost:  140
c ---[2454]---> BDD-cost:  137
c ---[2452]---> BDD-cost:  137
c ---[2451]---> BDD-cost:  140
c ---[2450]---> BDD-cost:  140
c ---[2449]---> BDD-cost:  137
c ---[2448]---> BDD-cost:  137
c ---[2447]---> BDD-cost:  137
c ---[2446]---> BDD-cost:  137
c ---[2445]---> BDD-cost:  137
c ---[2444]---> BDD-cost:  137
c ---[2443]---> BDD-cost:  143
c ---[2441]---> BDD-cost:  143
c ---[2440]---> BDD-cost:  137
c ---[2439]---> BDD-cost:  137
c ---[2438]---> BDD-cost:  143
c ---[2437]---> BDD-cost:  143
c ---[2436]---> BDD-cost:  137
c ---[2435]---> BDD-cost:  137
c ---[2434]---> BDD-cost:  141
c ---[2433]---> BDD-cost:  141
c ---[2432]---> BDD-cost:  137
c ---[2430]---> BDD-cost:  137
c ---[2429]---> BDD-cost:  140
c ---[2428]---> BDD-cost:  140
c ---[2427]---> BDD-cost:  137
c ---[2426]---> BDD-cost:  137
c ---[2425]---> BDD-cost:  126
c ---[2424]---> BDD-cost:  126
c ---[2423]---> BDD-cost:  137
c ---[2422]---> BDD-cost:  137
c ---[2421]---> BDD-cost:  135
c ---[2419]---> BDD-cost:  135
c ---[2418]---> BDD-cost:  137
c ---[2417]---> BDD-cost:  137
c ---[2416]---> BDD-cost:  140
c ---[2415]---> BDD-cost:  140
c ---[2414]---> BDD-cost:  137
c ---[2413]---> BDD-cost:  137
c ---[2412]---> BDD-cost:  135
c ---[2411]---> BDD-cost:  135
c ---[2410]---> BDD-cost:  137
c ---[2408]---> BDD-cost:  137
c ---[2407]---> BDD-cost:  135
c ---[2406]---> BDD-cost:  135
c ---[2405]---> BDD-cost:  137
c ---[2404]---> BDD-cost:  137
c ---[2403]---> BDD-cost:  143
c ---[2402]---> BDD-cost:  143
c ---[2401]---> BDD-cost:  137
c ---[2400]---> BDD-cost:  137
c ---[2399]---> BDD-cost:  138
c ---[2397]---> BDD-cost:  138
c ---[2396]---> BDD-cost:  137
c ---[2395]---> BDD-cost:  137
c ---[2394]---> BDD-cost:  135
c ---[2393]---> BDD-cost:  135
c ---[2392]---> BDD-cost:  137
c ---[2391]---> BDD-cost:  137
c ---[2390]---> BDD-cost:  136
c ---[2389]---> BDD-cost:  136
c ---[2388]---> BDD-cost:  137
c ---[2386]---> BDD-cost:  137
c ---[2385]---> BDD-cost:  146
c ---[2384]---> BDD-cost:  146
c ---[2383]---> BDD-cost:  137
c ---[2382]---> BDD-cost:  137
c ---[2381]---> BDD-cost:  138
c ---[2380]---> BDD-cost:  138
c ---[2379]---> BDD-cost:  137
c ---[2378]---> BDD-cost:  137
c ---[2377]---> BDD-cost:  143
c ---[2375]---> BDD-cost:  143
c ---[2374]---> BDD-cost:  137
c ---[2373]---> BDD-cost:  137
c ---[2372]---> BDD-cost:  123
c ---[2371]---> BDD-cost:  123
c ---[2370]---> BDD-cost:  137
c ---[2369]---> BDD-cost:  137
c ---[2368]---> BDD-cost:  146
c ---[2367]---> BDD-cost:  146
c ---[2366]---> BDD-cost:  137
c ---[2363]---> BDD-cost:  137
c ---[2362]---> BDD-cost:  143
c ---[2361]---> BDD-cost:  143
c ---[2360]---> BDD-cost:  137
c ---[2359]---> BDD-cost:  137
c ---[2358]---> BDD-cost:  140
c ---[2357]---> BDD-cost:  140
c ---[2356]---> BDD-cost:  137
c ---[2355]---> BDD-cost:  137
c ---[2354]---> BDD-cost:  128
c ---[2352]---> BDD-cost:  128
c ---[2351]---> BDD-cost:  137
c ---[2350]---> BDD-cost:  137
c ---[2349]---> BDD-cost:  143
c ---[2348]---> BDD-cost:  143
c ---[2347]---> BDD-cost:  137
c ---[2346]---> BDD-cost:  137
c ---[2345]---> BDD-cost:  133
c ---[2344]---> BDD-cost:  133
c ---[2343]---> BDD-cost:  137
c ---[2341]---> BDD-cost:  137
c ---[2340]---> BDD-cost:  141
c ---[2339]---> BDD-cost:  141
c ---[2338]---> BDD-cost:  137
c ---[2337]---> BDD-cost:  137
c ---[2336]---> BDD-cost:  138
c ---[2335]---> BDD-cost:  138
c ---[2334]---> BDD-cost:  137
c ---[2333]---> BDD-cost:  137
c ---[2332]---> BDD-cost:  125
c ---[2330]---> BDD-cost:  125
c ---[2329]---> BDD-cost:  137
c ---[2328]---> BDD-cost:  137
c ---[2327]---> BDD-cost:  143
c ---[2326]---> BDD-cost:  143
c ---[2325]---> BDD-cost:  137
c ---[2324]---> BDD-cost:  137
c ---[2323]---> BDD-cost:  143
c ---[2322]---> BDD-cost:  143
c ---[2321]---> BDD-cost:  137
c ---[2319]---> BDD-cost:  137
c ---[2318]---> BDD-cost:  143
c ---[2317]---> BDD-cost:  143
c ---[2316]---> BDD-cost:  137
c ---[2315]---> BDD-cost:  137
c ---[2314]---> BDD-cost:  135
c ---[2313]---> BDD-cost:  135
c ---[2312]---> BDD-cost:  137
c ---[2311]---> BDD-cost:  137
c ---[2310]---> BDD-cost:  140
c ---[2308]---> BDD-cost:  140
c ---[2307]---> BDD-cost:  137
c ---[2306]---> BDD-cost:  137
c ---[2305]---> BDD-cost:  128
c ---[2304]---> BDD-cost:  128
c ---[2303]---> BDD-cost:  137
c ---[2302]---> BDD-cost:  137
c ---[2301]---> BDD-cost:  143
c ---[2300]---> BDD-cost:  143
c ---[2299]---> BDD-cost:  137
c ---[2297]---> BDD-cost:  137
c ---[2296]---> BDD-cost:  138
c ---[2295]---> BDD-cost:  138
c ---[2294]---> BDD-cost:  137
c ---[2293]---> BDD-cost:  137
c ---[2292]---> BDD-cost:  123
c ---[2291]---> BDD-cost:  123
c ---[2290]---> BDD-cost:  137
c ---[2289]---> BDD-cost:  137
c ---[2288]---> BDD-cost:  140
c ---[2286]---> BDD-cost:  140
c ---[2285]---> BDD-cost:  137
c ---[2284]---> BDD-cost:  137
c ---[2283]---> BDD-cost:  140
c ---[2282]---> BDD-cost:  140
c ---[2281]---> BDD-cost:  137
c ---[2280]---> BDD-cost:  137
c ---[2279]---> BDD-cost:  140
c ---[2278]---> BDD-cost:  140
c ---[2277]---> BDD-cost:  137
c ---[2275]---> BDD-cost:  137
c ---[2274]---> BDD-cost:  135
c ---[2273]---> BDD-cost:  135
c ---[2272]---> BDD-cost:  137
c ---[2271]---> BDD-cost:  137
c ---[2270]---> BDD-cost:  138
c ---[2269]---> BDD-cost:  138
c ---[2268]---> BDD-cost:  137
c ---[2267]---> BDD-cost:  137
c ---[2266]---> BDD-cost:  143
c ---[2264]---> BDD-cost:  143
c ---[2263]---> BDD-cost:  137
c ---[2262]---> BDD-cost:  137
c ---[2261]---> BDD-cost:  138
c ---[2260]---> BDD-cost:  138
c ---[2259]---> BDD-cost:  137
c ---[2258]---> BDD-cost:  137
c ---[2257]---> BDD-cost:  143
c ---[2256]---> BDD-cost:  143
c ---[2255]---> BDD-cost:  137
c ---[2252]---> BDD-cost:  137
c ---[2251]---> BDD-cost:  143
c ---[2250]---> BDD-cost:  143
c ---[2249]---> BDD-cost:  137
c ---[2248]---> BDD-cost:  137
c ---[2247]---> BDD-cost:  128
c ---[2246]---> BDD-cost:  128
c ---[2245]---> BDD-cost:  137
c ---[2244]---> BDD-cost:  137
c ---[2243]---> BDD-cost:  143
c ---[2241]---> BDD-cost:  143
c ---[2240]---> BDD-cost:  137
c ---[2239]---> BDD-cost:  137
c ---[2238]---> BDD-cost:  133
c ---[2237]---> BDD-cost:  133
c ---[2236]---> BDD-cost:  137
c ---[2235]---> BDD-cost:  137
c ---[2234]---> BDD-cost:  140
c ---[2233]---> BDD-cost:  140
c ---[2232]---> BDD-cost:  137
c ---[2230]---> BDD-cost:  137
c ---[2229]---> BDD-cost:  130
c ---[2228]---> BDD-cost:  130
c ---[2227]---> BDD-cost:  137
c ---[2226]---> BDD-cost:  137
c ---[2225]---> BDD-cost:  140
c ---[2224]---> BDD-cost:  140
c ---[2223]---> BDD-cost:  137
c ---[2222]---> BDD-cost:  137
c ---[2221]---> BDD-cost:  133
c ---[2219]---> BDD-cost:  133
c ---[2218]---> BDD-cost:  137
c ---[2217]---> BDD-cost:  137
c ---[2216]---> BDD-cost:  118
c ---[2215]---> BDD-cost:  118
c ---[2214]---> BDD-cost:  137
c ---[2213]---> BDD-cost:  137
c ---[2212]---> BDD-cost:  140
c ---[2211]---> BDD-cost:  140
c ---[2210]---> BDD-cost:  137
c ---[2208]---> BDD-cost:  137
c ---[2207]---> BDD-cost:  143
c ---[2206]---> BDD-cost:  143
c ---[2205]---> BDD-cost:  137
c ---[2204]---> BDD-cost:  137
c ---[2203]---> BDD-cost:  140
c ---[2202]---> BDD-cost:  140
c ---[2201]---> BDD-cost:  137
c ---[2200]---> BDD-cost:  137
c ---[2199]---> BDD-cost:  140
c ---[2197]---> BDD-cost:  140
c ---[2196]---> BDD-cost:  137
c ---[2195]---> BDD-cost:  137
c ---[2194]---> BDD-cost:  143
c ---[2193]---> BDD-cost:  143
c ---[2192]---> BDD-cost:  137
c ---[2191]---> BDD-cost:  137
c ---[2190]---> BDD-cost:  143
c ---[2189]---> BDD-cost:  143
c ---[2188]---> BDD-cost:  137
c ---[2186]---> BDD-cost:  137
c ---[2185]---> BDD-cost:  135
c ---[2184]---> BDD-cost:  135
c ---[2183]---> BDD-cost:  137
c ---[2182]---> BDD-cost:  137
c ---[2181]---> BDD-cost:  134
c ---[2180]---> BDD-cost:  143
c ---[2179]---> BDD-cost:  129
c ---[2178]---> BDD-cost:  136
c ---[2177]---> BDD-cost:  124
c ---[2175]---> BDD-cost:  141
c ---[2174]---> BDD-cost:  126
c ---[2173]---> BDD-cost:  138
c ---[2172]---> BDD-cost:  124
c ---[2171]---> BDD-cost:  143
c ---[2170]---> BDD-cost:  137
c ---[2169]---> BDD-cost:  125
c ---[2168]---> BDD-cost:  129
c ---[2167]---> BDD-cost:  140
c ---[2166]---> BDD-cost:  134
c ---[2164]---> BDD-cost:  140
c ---[2163]---> BDD-cost:  132
c ---[2162]---> BDD-cost:  140
c ---[2161]---> BDD-cost:  132
c ---[2160]---> BDD-cost:  143
c ---[2159]---> BDD-cost:  132
c ---[2158]---> BDD-cost:  135
c ---[2157]---> BDD-cost:  132
c ---[2156]---> BDD-cost:  137
c ---[2155]---> BDD-cost:  126
c ---[2153]---> BDD-cost:  143
c ---[2152]---> BDD-cost:  132
c ---[2151]---> BDD-cost:  135
c ---[2150]---> BDD-cost:  127
c ---[2149]---> BDD-cost:  143
c ---[2148]---> BDD-cost:  137
c ---[2147]---> BDD-cost:  143
c ---[2146]---> BDD-cost:  120
c ---[2145]---> BDD-cost:  146
c ---[2144]---> BDD-cost:  132
c ---[2141]---> BDD-cost:  136
c ---[2140]---> BDD-cost:  132
c ---[2139]---> BDD-cost:  135
c ---[2138]---> BDD-cost:  137
c ---[2137]---> BDD-cost:  143
c ---[2136]---> BDD-cost:  124
c ---[2135]---> BDD-cost:  143
c ---[2134]---> BDD-cost:  131
c ---[2133]---> BDD-cost:  132
c ---[2132]---> BDD-cost:  124
c ---[2130]---> BDD-cost:  133
c ---[2129]---> BDD-cost:  126
c ---[2128]---> BDD-cost:  140
c ---[2127]---> BDD-cost:  120
c ---[2126]---> BDD-cost:  123
c ---[2125]---> BDD-cost:  126
c ---[2124]---> BDD-cost:  141
c ---[2123]---> BDD-cost:  137
c ---[2122]---> BDD-cost:  128
c ---[2121]---> BDD-cost:  137
c ---[2119]---> BDD-cost:  146
c ---[2118]---> BDD-cost:  132
c ---[2117]---> BDD-cost:  146
c ---[2116]---> BDD-cost:  120
c ---[2115]---> BDD-cost:  140
c ---[2114]---> BDD-cost:  137
c ---[2113]---> BDD-cost:  143
c ---[2112]---> BDD-cost:  137
c ---[2111]---> BDD-cost:  138
c ---[2110]---> BDD-cost:  137
c ---[2108]---> BDD-cost:  138
c ---[2107]---> BDD-cost:  132
c ---[2106]---> BDD-cost:  143
c ---[2105]---> BDD-cost:  134
c ---[2104]---> BDD-cost:  137
c ---[2103]---> BDD-cost:  137
c ---[2102]---> BDD-cost:  116
c ---[2101]---> BDD-cost:  134
c ---[2100]---> BDD-cost:  141
c ---[2099]---> BDD-cost:  122
c ---[2097]---> BDD-cost:  135
c ---[2096]---> BDD-cost:  120
c ---[2095]---> BDD-cost:  143
c ---[2094]---> BDD-cost:  137
c ---[2093]---> BDD-cost:  143
c ---[2092]---> BDD-cost:  126
c ---[2091]---> BDD-cost:  125
c ---[2090]---> BDD-cost:  124
c ---[2089]---> BDD-cost:  140
c ---[2088]---> BDD-cost:  131
c ---[2086]---> BDD-cost:  133
c ---[2085]---> BDD-cost:  127
c ---[2084]---> BDD-cost:  126
c ---[2083]---> BDD-cost:  127
c ---[2082]---> BDD-cost:  143
c ---[2081]---> BDD-cost:  122
c ---[2080]---> BDD-cost:  143
c ---[2079]---> BDD-cost:  132
c ---[2078]---> BDD-cost:  137
c ---[2077]---> BDD-cost:  134
c ---[2075]---> BDD-cost:  134
c ---[2074]---> BDD-cost:  126
c ---[2073]---> BDD-cost:  143
c ---[2072]---> BDD-cost:  124
c ---[2071]---> BDD-cost:  120
c ---[2070]---> BDD-cost:  127
c ---[2069]---> BDD-cost:  143
c ---[2068]---> BDD-cost:  120
c ---[2067]---> BDD-cost:  138
c ---[2066]---> BDD-cost:  137
c ---[2064]---> BDD-cost:  140
c ---[2063]---> BDD-cost:  129
c ---[2062]---> BDD-cost:  138
c ---[2061]---> BDD-cost:  126
c ---[2060]---> BDD-cost:  143
c ---[2059]---> BDD-cost:  131
c ---[2058]---> BDD-cost:  143
c ---[2057]---> BDD-cost:  129
c ---[2056]---> BDD-cost:  140
c ---[2055]---> BDD-cost:  131
c ---[2053]---> BDD-cost:  143
c ---[2052]---> BDD-cost:  131
c ---[2051]---> BDD-cost:  123
c ---[2050]---> BDD-cost:  140
c ---[2049]---> BDD-cost:  140
c ---[2048]---> BDD-cost:  135
c ---[2047]---> BDD-cost:  129
c ---[2046]---> BDD-cost:  143
c ---[2045]---> BDD-cost:  122
c ---[2044]---> BDD-cost:  133
c ---[2042]---> BDD-cost:  137
c ---[2041]---> BDD-cost:  141
c ---[2040]---> BDD-cost:  134
c ---[2039]---> BDD-cost:  143
c ---[2038]---> BDD-cost:  120
c ---[2037]---> BDD-cost:  125
c ---[2036]---> BDD-cost:  137
c ---[2035]---> BDD-cost:  133
c ---[2034]---> BDD-cost:  137
c ---[2033]---> BDD-cost:  131
c ---[2029]---> BDD-cost:  131
c ---[2028]---> BDD-cost:  137
c ---[2027]---> BDD-cost:  124
c ---[2026]---> BDD-cost:  136
c ---[2025]---> BDD-cost:  127
c ---[2024]---> BDD-cost:  133
c ---[2023]---> BDD-cost:  127
c ---[2022]---> BDD-cost:  146
c ---[2021]---> BDD-cost:  132
c ---[2020]---> BDD-cost:  141
c ---[2018]---> BDD-cost:  132
c ---[2017]---> BDD-cost:  130
c ---[2016]---> BDD-cost:  137
c ---[2015]---> BDD-cost:  140
c ---[2014]---> BDD-cost:  129
c ---[2013]---> BDD-cost:  143
c ---[2012]---> BDD-cost:  132
c ---[2011]---> BDD-cost:  138
c ---[2010]---> BDD-cost:  129
c ---[2009]---> BDD-cost:  136
c ---[2007]---> BDD-cost:  137
c ---[2006]---> BDD-cost:  138
c ---[2005]---> BDD-cost:  137
c ---[2004]---> BDD-cost:  146
c ---[2003]---> BDD-cost:  132
c ---[2002]---> BDD-cost:  146
c ---[2001]---> BDD-cost:  137
c ---[2000]---> BDD-cost:  141
c ---[1999]---> BDD-cost:  137
c ---[1998]---> BDD-cost:  123
c ---[1996]---> BDD-cost:  120
c ---[1995]---> BDD-cost:  143
c ---[1994]---> BDD-cost:  134
c ---[1993]---> BDD-cost:  146
c ---[1992]---> BDD-cost:  124
c ---[1991]---> BDD-cost:  130
c ---[1990]---> BDD-cost:  134
c ---[1989]---> BDD-cost:  141
c ---[1988]---> BDD-cost:  137
c ---[1987]---> BDD-cost:  141
c ---[1985]---> BDD-cost:  132
c ---[1984]---> BDD-cost:  141
c ---[1983]---> BDD-cost:  132
c ---[1982]---> BDD-cost:  146
c ---[1981]---> BDD-cost:  137
c ---[1980]---> BDD-cost:  146
c ---[1979]---> BDD-cost:  140
c ---[1978]---> BDD-cost:  140
c ---[1977]---> BDD-cost:  143
c ---[1976]---> BDD-cost:  120
c ---[1974]---> BDD-cost:  138
c ---[1973]---> BDD-cost:  134
c ---[1972]---> BDD-cost:  131
c ---[1971]---> BDD-cost:  129
c ---[1970]---> BDD-cost:  143
c ---[1969]---> BDD-cost:  134
c ---[1968]---> BDD-cost:  146
c ---[1967]---> BDD-cost:  137
c ---[1966]---> BDD-cost:  146
c ---[1965]---> BDD-cost:  120
c ---[1963]---> BDD-cost:  146
c ---[1962]---> BDD-cost:  122
c ---[1961]---> BDD-cost:  141
c ---[1960]---> BDD-cost:  140
c ---[1959]---> BDD-cost:  140
c ---[1958]---> BDD-cost:  141
c ---[1957]---> BDD-cost:  120
c ---[1956]---> BDD-cost:  138
c ---[1955]---> BDD-cost:  134
c ---[1954]---> BDD-cost:  132
c ---[1952]---> BDD-cost:  129
c ---[1951]---> BDD-cost:  143
c ---[1950]---> BDD-cost:  134
c ---[1949]---> BDD-cost:  134
c ---[1948]---> BDD-cost:  137
c ---[1947]---> BDD-cost:  146
c ---[1946]---> BDD-cost:  120
c ---[1945]---> BDD-cost:  137
c ---[1944]---> BDD-cost:  122
c ---[1943]---> BDD-cost:  128
c ---[1941]---> BDD-cost:  140
c ---[1940]---> BDD-cost:  140
c ---[1939]---> BDD-cost:  138
c ---[1938]---> BDD-cost:  131
c ---[1937]---> BDD-cost:  140
c ---[1936]---> BDD-cost:  124
c ---[1935]---> BDD-cost:  138
c ---[1934]---> BDD-cost:  131
c ---[1933]---> BDD-cost:  132
c ---[1932]---> BDD-cost:  120
c ---[1930]---> BDD-cost:  126
c ---[1929]---> BDD-cost:  120
c ---[1928]---> BDD-cost:  138
c ---[1927]---> BDD-cost:  132
c ---[1926]---> BDD-cost:  146
c ---[1925]---> BDD-cost:  137
c ---[1924]---> BDD-cost:  143
c ---[1923]---> BDD-cost:  137
c ---[1922]---> BDD-cost:  138
c ---[1921]---> BDD-cost:  126
c ---[1918]---> BDD-cost:  146
c ---[1917]---> BDD-cost:  137
c ---[1916]---> BDD-cost:  143
c ---[1915]---> BDD-cost:  137
c ---[1914]---> BDD-cost:  131
c ---[1913]---> BDD-cost:  132
c ---[1912]---> BDD-cost:  138
c ---[1911]---> BDD-cost:  126
c ---[1910]---> BDD-cost:  125
c ---[1909]---> BDD-cost:  131
c ---[1907]---> BDD-cost:  130
c ---[1906]---> BDD-cost:  137
c ---[1905]---> BDD-cost:  134
c ---[1904]---> BDD-cost:  140
c ---[1903]---> BDD-cost:  140
c ---[1902]---> BDD-cost:  143
c ---[1901]---> BDD-cost:  137
c ---[1900]---> BDD-cost:  130
c ---[1899]---> BDD-cost:  124
c ---[1898]---> BDD-cost:  138
c ---[1896]---> BDD-cost:  122
c ---[1895]---> BDD-cost:  138
c ---[1894]---> BDD-cost:  129
c ---[1893]---> BDD-cost:  118
c ---[1892]---> BDD-cost:  137
c ---[1891]---> BDD-cost:  143
c ---[1890]---> BDD-cost:  120
c ---[1889]---> BDD-cost:  146
c ---[1888]---> BDD-cost:  126
c ---[1887]---> BDD-cost:  143
c ---[1885]---> BDD-cost:  124
c ---[1884]---> BDD-cost:  143
c ---[1883]---> BDD-cost:  120
c ---[1882]---> BDD-cost:  138
c ---[1881]---> BDD-cost:  137
c ---[1880]---> BDD-cost:  143
c ---[1879]---> BDD-cost:  131
c ---[1878]---> BDD-cost:  146
c ---[1877]---> BDD-cost:  124
c ---[1876]---> BDD-cost:  140
c ---[1874]---> BDD-cost:  131
c ---[1873]---> BDD-cost:  143
c ---[1872]---> BDD-cost:  140
c ---[1871]---> BDD-cost:  140
c ---[1870]---> BDD-cost:  136
c ---[1869]---> BDD-cost:  132
c ---[1868]---> BDD-cost:  146
c ---[1867]---> BDD-cost:  126
c ---[1866]---> BDD-cost:  143
c ---[1865]---> BDD-cost:  137
c ---[1863]---> BDD-cost:  135
c ---[1862]---> BDD-cost:  129
c ---[1861]---> BDD-cost:  140
c ---[1860]---> BDD-cost:  137
c ---[1859]---> BDD-cost:  120
c ---[1858]---> BDD-cost:  127
c ---[1857]---> BDD-cost:  130
c ---[1856]---> BDD-cost:  137
c ---[1855]---> BDD-cost:  135
c ---[1854]---> BDD-cost:  129
c ---[1852]---> BDD-cost:  140
c ---[1851]---> BDD-cost:  134
c ---[1850]---> BDD-cost:  135
c ---[1849]---> BDD-cost:  129
c ---[1848]---> BDD-cost:  132
c ---[1847]---> BDD-cost:  132
c ---[1846]---> BDD-cost:  128
c ---[1845]---> BDD-cost:  137
c ---[1844]---> BDD-cost:  135
c ---[1843]---> BDD-cost:  137
c ---[1841]---> BDD-cost:  143
c ---[1840]---> BDD-cost:  120
c ---[1839]---> BDD-cost:  143
c ---[1838]---> BDD-cost:  131
c ---[1837]---> BDD-cost:  135
c ---[1836]---> BDD-cost:  132
c ---[1835]---> BDD-cost:  140
c ---[1834]---> BDD-cost:  122
c ---[1833]---> BDD-cost:  124
c ---[1832]---> BDD-cost:  131
c ---[1830]---> BDD-cost:  127
c ---[1829]---> BDD-cost:  137
c ---[1828]---> BDD-cost:  135
c ---[1827]---> BDD-cost:  120
c ---[1826]---> BDD-cost:  134
c ---[1825]---> BDD-cost:  137
c ---[1824]---> BDD-cost:  132
c ---[1823]---> BDD-cost:  129
c ---[1822]---> BDD-cost:  129
c ---[1821]---> BDD-cost:  120
c ---[1819]---> BDD-cost:  122
c ---[1818]---> BDD-cost:  137
c ---[1817]---> BDD-cost:  132
c ---[1816]---> BDD-cost:  127
c ---[1815]---> BDD-cost:  140
c ---[1814]---> BDD-cost:  120
c ---[1813]---> BDD-cost:  130
c ---[1812]---> BDD-cost:  137
c ---[1811]---> BDD-cost:  135
c ---[1810]---> BDD-cost:  137
c ---[1807]---> BDD-cost:  140
c ---[1806]---> BDD-cost:  132
c ---[1805]---> BDD-cost:  140
c ---[1804]---> BDD-cost:  132
c ---[1803]---> BDD-cost:  140
c ---[1802]---> BDD-cost:  126
c ---[1801]---> BDD-cost:  135
c ---[1800]---> BDD-cost:  122
c ---[1799]---> BDD-cost:  133
c ---[1798]---> BDD-cost:  132
c ---[1796]---> BDD-cost:  130
c ---[1795]---> BDD-cost:  137
c ---[1794]---> BDD-cost:  130
c ---[1793]---> BDD-cost:  124
c ---[1792]---> BDD-cost:  135
c ---[1791]---> BDD-cost:  137
c ---[1790]---> BDD-cost:  124
c ---[1789]---> BDD-cost:  132
c ---[1788]---> BDD-cost:  128
c ---[1787]---> BDD-cost:  124
c ---[1785]---> BDD-cost:  134
c ---[1784]---> BDD-cost:  134
c ---[1783]---> BDD-cost:  134
c ---[1782]---> BDD-cost:  134
c ---[1781]---> BDD-cost:  143
c ---[1780]---> BDD-cost:  131
c ---[1779]---> BDD-cost:  141
c ---[1778]---> BDD-cost:  124
c ---[1777]---> BDD-cost:  133
c ---[1776]---> BDD-cost:  134
c ---[1774]---> BDD-cost:  133
c ---[1773]---> BDD-cost:  124
c ---[1772]---> BDD-cost:  133
c ---[1771]---> BDD-cost:  137
c ---[1770]---> BDD-cost:  134
c ---[1769]---> BDD-cost:  137
c ---[1768]---> BDD-cost:  140
c ---[1767]---> BDD-cost:  137
c ---[1766]---> BDD-cost:  140
c ---[1765]---> BDD-cost:  134
c ---[1763]---> BDD-cost:  127
c ---[1762]---> BDD-cost:  137
c ---[1761]---> BDD-cost:  143
c ---[1760]---> BDD-cost:  131
c ---[1759]---> BDD-cost:  132
c ---[1758]---> BDD-cost:  122
c ---[1757]---> BDD-cost:  146
c ---[1756]---> BDD-cost:  122
c ---[1755]---> BDD-cost:  144
c ---[1754]---> BDD-cost:  127
c ---[1752]---> BDD-cost:  138
c ---[1751]---> BDD-cost:  131
c ---[1750]---> BDD-cost:  146
c ---[1749]---> BDD-cost:  120
c ---[1748]---> BDD-cost:  134
c ---[1747]---> BDD-cost:  132
c ---[1746]---> BDD-cost:  131
c ---[1745]---> BDD-cost:  137
c ---[1744]---> BDD-cost:  136
c ---[1743]---> BDD-cost:  136
c ---[1741]---> BDD-cost:  137
c ---[1740]---> BDD-cost:  122
c ---[1739]---> BDD-cost:  124
c ---[1738]---> BDD-cost:  138
c ---[1737]---> BDD-cost:  126
c ---[1736]---> BDD-cost:  143
c ---[1735]---> BDD-cost:  132
c ---[1734]---> BDD-cost:  140
c ---[1733]---> BDD-cost:  137
c ---[1732]---> BDD-cost:  137
c ---[1730]---> BDD-cost:  137
c ---[1729]---> BDD-cost:  129
c ---[1728]---> BDD-cost:  127
c ---[1727]---> BDD-cost:  129
c ---[1726]---> BDD-cost:  127
c ---[1725]---> BDD-cost:  133
c ---[1724]---> BDD-cost:  140
c ---[1723]---> BDD-cost:  140
c ---[1722]---> BDD-cost:  138
c ---[1721]---> BDD-cost:  126
c ---[1719]---> BDD-cost:  130
c ---[1718]---> BDD-cost:  131
c ---[1717]---> BDD-cost:  130
c ---[1716]---> BDD-cost:  122
c ---[1715]---> BDD-cost:  138
c ---[1714]---> BDD-cost:  134
c ---[1713]---> BDD-cost:  146
c ---[1712]---> BDD-cost:  134
c ---[1711]---> BDD-cost:  128
c ---[1710]---> BDD-cost:  134
c ---[1708]---> BDD-cost:  120
c ---[1707]---> BDD-cost:  124
c ---[1706]---> BDD-cost:  138
c ---[1705]---> BDD-cost:  137
c ---[1704]---> BDD-cost:  135
c ---[1703]---> BDD-cost:  137
c ---[1702]---> BDD-cost:  140
c ---[1701]---> BDD-cost:  137
c ---[1700]---> BDD-cost:  128
c ---[1699]---> BDD-cost:  126
c ---[1696]---> BDD-cost:  140
c ---[1695]---> BDD-cost:  134
c ---[1694]---> BDD-cost:  140
c ---[1693]---> BDD-cost:  126
c ---[1692]---> BDD-cost:  135
c ---[1691]---> BDD-cost:  120
c ---[1690]---> BDD-cost:  146
c ---[1689]---> BDD-cost:  120
c ---[1688]---> BDD-cost:  137
c ---[1687]---> BDD-cost:  137
c ---[1685]---> BDD-cost:  143
c ---[1684]---> BDD-cost:  140
c ---[1683]---> BDD-cost:  140
c ---[1682]---> BDD-cost:  137
c ---[1681]---> BDD-cost:  132
c ---[1680]---> BDD-cost:  143
c ---[1679]---> BDD-cost:  137
c ---[1678]---> BDD-cost:  140
c ---[1677]---> BDD-cost:  131
c ---[1676]---> BDD-cost:  141
c ---[1674]---> BDD-cost:  127
c ---[1673]---> BDD-cost:  138
c ---[1672]---> BDD-cost:  134
c ---[1671]---> BDD-cost:  140
c ---[1670]---> BDD-cost:  132
c ---[1669]---> BDD-cost:  124
c ---[1668]---> BDD-cost:  140
c ---[1667]---> BDD-cost:  140
c ---[1666]---> BDD-cost:  136
c ---[1665]---> BDD-cost:  137
c ---[1663]---> BDD-cost:  127
c ---[1662]---> BDD-cost:  122
c ---[1661]---> BDD-cost:  129
c ---[1660]---> BDD-cost:  137
c ---[1659]---> BDD-cost:  146
c ---[1658]---> BDD-cost:  122
c ---[1657]---> BDD-cost:  143
c ---[1656]---> BDD-cost:  120
c ---[1655]---> BDD-cost:  133
c ---[1654]---> BDD-cost:  132
c ---[1652]---> BDD-cost:  141
c ---[1651]---> BDD-cost:  141
c ---[1650]---> BDD-cost:  131
c ---[1649]---> BDD-cost:  146
c ---[1648]---> BDD-cost:  131
c ---[1647]---> BDD-cost:  143
c ---[1646]---> BDD-cost:  126
c ---[1645]---> BDD-cost:  143
c ---[1644]---> BDD-cost:  132
c ---[1643]---> BDD-cost:  128
c ---[1641]---> BDD-cost:  129
c ---[1640]---> BDD-cost:  135
c ---[1639]---> BDD-cost:  129
c ---[1638]---> BDD-cost:  140
c ---[1637]---> BDD-cost:  124
c ---[1636]---> BDD-cost:  143
c ---[1635]---> BDD-cost:  134
c ---[1634]---> BDD-cost:  134
c ---[1633]---> BDD-cost:  126
c ---[1632]---> BDD-cost:  143
c ---[1630]---> BDD-cost:  137
c ---[1629]---> BDD-cost:  123
c ---[1628]---> BDD-cost:  134
c ---[1627]---> BDD-cost:  143
c ---[1626]---> BDD-cost:  122
c ---[1625]---> BDD-cost:  135
c ---[1624]---> BDD-cost:  137
c ---[1623]---> BDD-cost:  146
c ---[1622]---> BDD-cost:  120
c ---[1621]---> BDD-cost:  146
c ---[1619]---> BDD-cost:  132
c ---[1618]---> BDD-cost:  149
c ---[1617]---> BDD-cost:  131
c ---[1616]---> BDD-cost:  141
c ---[1615]---> BDD-cost:  137
c ---[1614]---> BDD-cost:  130
c ---[1613]---> BDD-cost:  132
c ---[1612]---> BDD-cost:  125
c ---[1611]---> BDD-cost:  122
c ---[1610]---> BDD-cost:  126
c ---[1608]---> BDD-cost:  122
c ---[1607]---> BDD-cost:  118
c ---[1606]---> BDD-cost:  137
c ---[1605]---> BDD-cost:  130
c ---[1604]---> BDD-cost:  126
c ---[1603]---> BDD-cost:  143
c ---[1602]---> BDD-cost:  126
c ---[1601]---> BDD-cost:  140
c ---[1600]---> BDD-cost:  131
c ---[1599]---> BDD-cost:  140
c ---[1597]---> BDD-cost:  122
c ---[1596]---> BDD-cost:  143
c ---[1595]---> BDD-cost:  134
c ---[1594]---> BDD-cost:  141
c ---[1593]---> BDD-cost:  134
c ---[1592]---> BDD-cost:  143
c ---[1591]---> BDD-cost:  126
c ---[1590]---> BDD-cost:  133
c ---[1589]---> BDD-cost:  134
c ---[1588]---> BDD-cost:  146
c ---[1585]---> BDD-cost:  120
c ---[1584]---> BDD-cost:  146
c ---[1583]---> BDD-cost:  137
c ---[1582]---> BDD-cost:  146
c ---[1581]---> BDD-cost:  120
c ---[1580]---> BDD-cost:  146
c ---[1579]---> BDD-cost:  137
c ---[1578]---> BDD-cost:  138
c ---[1577]---> BDD-cost:  132
c ---[1576]---> BDD-cost:  130
c ---[1574]---> BDD-cost:  137
c ---[1573]---> BDD-cost:  146
c ---[1572]---> BDD-cost:  129
c ---[1571]---> BDD-cost:  140
c ---[1570]---> BDD-cost:  126
c ---[1569]---> BDD-cost:  131
c ---[1568]---> BDD-cost:  134
c ---[1567]---> BDD-cost:  137
c ---[1566]---> BDD-cost:  140
c ---[1565]---> BDD-cost:  140
c ---[1563]---> BDD-cost:  137
c ---[1562]---> BDD-cost:  137
c ---[1561]---> BDD-cost:  141
c ---[1560]---> BDD-cost:  132
c ---[1559]---> BDD-cost:  146
c ---[1558]---> BDD-cost:  146
c ---[1557]---> BDD-cost:  137
c ---[1556]---> BDD-cost:  146
c ---[1555]---> BDD-cost:  131
c ---[1554]---> BDD-cost:  130
c ---[1552]---> BDD-cost:  140
c ---[1551]---> BDD-cost:  140
c ---[1550]---> BDD-cost:  138
c ---[1549]---> BDD-cost:  122
c ---[1548]---> BDD-cost:  143
c ---[1547]---> BDD-cost:  137
c ---[1546]---> BDD-cost:  146
c ---[1545]---> BDD-cost:  122
c ---[1544]---> BDD-cost:  143
c ---[1543]---> BDD-cost:  137
c ---[1541]---> BDD-cost:  138
c ---[1540]---> BDD-cost:  127
c ---[1539]---> BDD-cost:  141
c ---[1538]---> BDD-cost:  134
c ---[1537]---> BDD-cost:  140
c ---[1536]---> BDD-cost:  122
c ---[1535]---> BDD-cost:  133
c ---[1534]---> BDD-cost:  137
c ---[1533]---> BDD-cost:  133
c ---[1532]---> BDD-cost:  140
c ---[1530]---> BDD-cost:  140
c ---[1529]---> BDD-cost:  146
c ---[1528]---> BDD-cost:  137
c ---[1527]---> BDD-cost:  141
c ---[1526]---> BDD-cost:  132
c ---[1525]---> BDD-cost:  141
c ---[1524]---> BDD-cost:  132
c ---[1523]---> BDD-cost:  143
c ---[1522]---> BDD-cost:  127
c ---[1521]---> BDD-cost:  146
c ---[1519]---> BDD-cost:  137
c ---[1518]---> BDD-cost:  133
c ---[1517]---> BDD-cost:  132
c ---[1516]---> BDD-cost:  118
c ---[1515]---> BDD-cost:  132
c ---[1514]---> BDD-cost:  140
c ---[1513]---> BDD-cost:  132
c ---[1512]---> BDD-cost:  138
c ---[1511]---> BDD-cost:  131
c ---[1510]---> BDD-cost:  146
c ---[1508]---> BDD-cost:  127
c ---[1507]---> BDD-cost:  140
c ---[1506]---> BDD-cost:  127
c ---[1505]---> BDD-cost:  141
c ---[1504]---> BDD-cost:  137
c ---[1503]---> BDD-cost:  136
c ---[1502]---> BDD-cost:  127
c ---[1501]---> BDD-cost:  127
c ---[1500]---> BDD-cost:  131
c ---[1499]---> BDD-cost:  138
c ---[1497]---> BDD-cost:  127
c ---[1496]---> BDD-cost:  140
c ---[1495]---> BDD-cost:  127
c ---[1494]---> BDD-cost:  143
c ---[1493]---> BDD-cost:  122
c ---[1492]---> BDD-cost:  140
c ---[1491]---> BDD-cost:  131
c ---[1490]---> BDD-cost:  136
c ---[1489]---> BDD-cost:  134
c ---[1488]---> BDD-cost:  137
c ---[1486]---> BDD-cost:  122
c ---[1485]---> BDD-cost:  141
c ---[1484]---> BDD-cost:  132
c ---[1483]---> BDD-cost:  128
c ---[1482]---> BDD-cost:  127
c ---[1481]---> BDD-cost:  132
c ---[1480]---> BDD-cost:  129
c ---[1479]---> BDD-cost:  146
c ---[1478]---> BDD-cost:  131
c ---[1477]---> BDD-cost:  146
c ---[1474]---> BDD-cost:  129
c ---[1473]---> BDD-cost:  146
c ---[1472]---> BDD-cost:  132
c ---[1471]---> BDD-cost:  141
c ---[1470]---> BDD-cost:  126
c ---[1469]---> BDD-cost:  138
c ---[1468]---> BDD-cost:  134
c ---[1467]---> BDD-cost:  138
c ---[1466]---> BDD-cost:  120
c ---[1465]---> BDD-cost:  141
c ---[1463]---> BDD-cost:  137
c ---[1462]---> BDD-cost:  143
c ---[1461]---> BDD-cost:  124
c ---[1460]---> BDD-cost:  143
c ---[1459]---> BDD-cost:  122
c ---[1458]---> BDD-cost:  136
c ---[1457]---> BDD-cost:  132
c ---[1456]---> BDD-cost:  143
c ---[1455]---> BDD-cost:  140
c ---[1454]---> BDD-cost:  140
c ---[1452]---> BDD-cost:  143
c ---[1451]---> BDD-cost:  137
c ---[1450]---> BDD-cost:  127
c ---[1449]---> BDD-cost:  122
c ---[1448]---> BDD-cost:  146
c ---[1447]---> BDD-cost:  132
c ---[1446]---> BDD-cost:  143
c ---[1252]---> BDD-cost:  125
c ---[1251]---> BDD-cost:  119
c ---[1250]---> BDD-cost:   88
c ---[1248]---> BDD-cost:   88
c ---[1247]---> BDD-cost:   88
c ---[1246]---> BDD-cost:   88
c ---[1245]---> BDD-cost:  123
c ---[1244]---> BDD-cost:  119
c ---[1243]---> BDD-cost:   88
c ---[1242]---> BDD-cost:   88
c ---[1241]---> BDD-cost:   88
c ---[1240]---> BDD-cost:   88
c ---[1239]---> BDD-cost:  125
c ---[1237]---> BDD-cost:  119
c ---[1236]---> BDD-cost:   88
c ---[1235]---> BDD-cost:   88
c ---[1234]---> BDD-cost:   88
c ---[1233]---> BDD-cost:   88
c ---[1232]---> BDD-cost:  115
c ---[1231]---> BDD-cost:  119
c ---[1230]---> BDD-cost:   88
c ---[1229]---> BDD-cost:   88
c ---[1228]---> BDD-cost:   88
c ---[1226]---> BDD-cost:   88
c ---[1225]---> BDD-cost:  125
c ---[1224]---> BDD-cost:  119
c ---[1223]---> BDD-cost:   88
c ---[1222]---> BDD-cost:   88
c ---[1221]---> BDD-cost:   88
c ---[1220]---> BDD-cost:   88
c ---[1219]---> BDD-cost:  123
c ---[1218]---> BDD-cost:  119
c ---[1217]---> BDD-cost:   88
c ---[1215]---> BDD-cost:   88
c ---[1214]---> BDD-cost:   88
c ---[1213]---> BDD-cost:   88
c ---[1212]---> BDD-cost:  125
c ---[1211]---> BDD-cost:  119
c ---[1210]---> BDD-cost:   88
c ---[1209]---> BDD-cost:   88
c ---[1208]---> BDD-cost:   88
c ---[1207]---> BDD-cost:   88
c ---[1206]---> BDD-cost:  123
c ---[1204]---> BDD-cost:  119
c ---[1203]---> BDD-cost:   88
c ---[1202]---> BDD-cost:   88
c ---[1201]---> BDD-cost:   88
c ---[1200]---> BDD-cost:   88
c ---[1199]---> BDD-cost:  121
c ---[1198]---> BDD-cost:  119
c ---[1197]---> BDD-cost:   88
c ---[1196]---> BDD-cost:   88
c ---[1195]---> BDD-cost:   88
c ---[1193]---> BDD-cost:   88
c ---[1192]---> BDD-cost:  125
c ---[1191]---> BDD-cost:  119
c ---[1190]---> BDD-cost:   88
c ---[1189]---> BDD-cost:   88
c ---[1188]---> BDD-cost:   88
c ---[1187]---> BDD-cost:   88
c ---[1186]---> BDD-cost:  123
c ---[1185]---> BDD-cost:  119
c ---[1184]---> BDD-cost:   88
c ---[1182]---> BDD-cost:   88
c ---[1181]---> BDD-cost:   88
c ---[1180]---> BDD-cost:   88
c ---[1179]---> BDD-cost:  125
c ---[1178]---> BDD-cost:  119
c ---[1177]---> BDD-cost:   88
c ---[1176]---> BDD-cost:   88
c ---[1175]---> BDD-cost:   88
c ---[1174]---> BDD-cost:   88
c ---[1173]---> BDD-cost:  125
c ---[1170]---> BDD-cost:  119
c ---[1169]---> BDD-cost:   88
c ---[1168]---> BDD-cost:   88
c ---[1167]---> BDD-cost:   88
c ---[1166]---> BDD-cost:   88
c ---[1165]---> BDD-cost:  123
c ---[1164]---> BDD-cost:  119
c ---[1163]---> BDD-cost:   88
c ---[1162]---> BDD-cost:   88
c ---[1161]---> BDD-cost:   88
c ---[1159]---> BDD-cost:   88
c ---[1158]---> BDD-cost:  115
c ---[1157]---> BDD-cost:  119
c ---[1156]---> BDD-cost:   88
c ---[1155]---> BDD-cost:   88
c ---[1154]---> BDD-cost:   88
c ---[1153]---> BDD-cost:   88
c ---[1152]---> BDD-cost:  123
c ---[1151]---> BDD-cost:  119
c ---[1150]---> BDD-cost:   88
c ---[1148]---> BDD-cost:   88
c ---[1147]---> BDD-cost:   88
c ---[1146]---> BDD-cost:   88
c ---[1145]---> BDD-cost:  119
c ---[1144]---> BDD-cost:  119
c ---[1143]---> BDD-cost:   88
c ---[1142]---> BDD-cost:   88
c ---[1141]---> BDD-cost:   88
c ---[1140]---> BDD-cost:   88
c ---[1139]---> BDD-cost:  125
c ---[1137]---> BDD-cost:  119
c ---[1136]---> BDD-cost:   88
c ---[1135]---> BDD-cost:   88
c ---[1134]---> BDD-cost:   88
c ---[1133]---> BDD-cost:   88
c ---[1132]---> BDD-cost:  119
c ---[1131]---> BDD-cost:  119
c ---[1130]---> BDD-cost:   88
c ---[1129]---> BDD-cost:   88
c ---[1128]---> BDD-cost:   88
c ---[1126]---> BDD-cost:   88
c ---[1125]---> BDD-cost:  123
c ---[1124]---> BDD-cost:  119
c ---[1123]---> BDD-cost:   88
c ---[1122]---> BDD-cost:   88
c ---[1121]---> BDD-cost:   88
c ---[1120]---> BDD-cost:   88
c ---[1119]---> BDD-cost:  125
c ---[1118]---> BDD-cost:  119
c ---[1117]---> BDD-cost:   88
c ---[1115]---> BDD-cost:   88
c ---[1114]---> BDD-cost:   88
c ---[1113]---> BDD-cost:   88
c ---[1112]---> BDD-cost:  121
c ---[1111]---> BDD-cost:  119
c ---[1110]---> BDD-cost:   88
c ---[1109]---> BDD-cost:   88
c ---[1108]---> BDD-cost:   88
c ---[1107]---> BDD-cost:   88
c ---[1106]---> BDD-cost:  123
c ---[1104]---> BDD-cost:  119
c ---[1103]---> BDD-cost:   88
c ---[1102]---> BDD-cost:   88
c ---[1101]---> BDD-cost:   88
c ---[1100]---> BDD-cost:   88
c ---[1099]---> BDD-cost:  119
c ---[1098]---> BDD-cost:  119
c ---[1097]---> BDD-cost:   88
c ---[1096]---> BDD-cost:   88
c ---[1095]---> BDD-cost:   88
c ---[1093]---> BDD-cost:   88
c ---[1092]---> BDD-cost:  123
c ---[1091]---> BDD-cost:  119
c ---[1090]---> BDD-cost:   88
c ---[1089]---> BDD-cost:   88
c ---[1088]---> BDD-cost:   88
c ---[1087]---> BDD-cost:   88
c ---[1086]---> BDD-cost:  121
c ---[1085]---> BDD-cost:  119
c ---[1084]---> BDD-cost:   88
c ---[1082]---> BDD-cost:   88
c ---[1081]---> BDD-cost:   88
c ---[1080]---> BDD-cost:   88
c ---[1079]---> BDD-cost:  123
c ---[1078]---> BDD-cost:  119
c ---[1077]---> BDD-cost:   88
c ---[1076]---> BDD-cost:   88
c ---[1075]---> BDD-cost:   88
c ---[1074]---> BDD-cost:   88
c ---[1073]---> BDD-cost:  123
c ---[1071]---> BDD-cost:  119
c ---[1070]---> BDD-cost:   88
c ---[1069]---> BDD-cost:   88
c ---[1068]---> BDD-cost:   88
c ---[1067]---> BDD-cost:   88
c ---[1066]---> BDD-cost:  121
c ---[1065]---> BDD-cost:  119
c ---[1064]---> BDD-cost:   88
c ---[1063]---> BDD-cost:   88
c ---[1062]---> BDD-cost:   88
c ---[1059]---> BDD-cost:   88
c ---[1058]---> BDD-cost:  123
c ---[1057]---> BDD-cost:  119
c ---[1056]---> BDD-cost:   88
c ---[1055]---> BDD-cost:   88
c ---[1054]---> BDD-cost:   88
c ---[1053]---> BDD-cost:   88
c ---[1052]---> BDD-cost:  121
c ---[1051]---> BDD-cost:  119
c ---[1050]---> BDD-cost:   88
c ---[1048]---> BDD-cost:   88
c ---[1047]---> BDD-cost:   88
c ---[1046]---> BDD-cost:   88
c ---[1045]---> BDD-cost:  123
c ---[1044]---> BDD-cost:  119
c ---[1043]---> BDD-cost:   88
c ---[1042]---> BDD-cost:   88
c ---[1041]---> BDD-cost:   88
c ---[1040]---> BDD-cost:   88
c ---[1039]---> BDD-cost:  123
c ---[1037]---> BDD-cost:  119
c ---[1036]---> BDD-cost:   88
c ---[1035]---> BDD-cost:   88
c ---[1034]---> BDD-cost:   88
c ---[1033]---> BDD-cost:   88
c ---[1032]---> BDD-cost:  123
c ---[1031]---> BDD-cost:  119
c ---[1030]---> BDD-cost:   88
c ---[1029]---> BDD-cost:   88
c ---[1028]---> BDD-cost:   88
c ---[1026]---> BDD-cost:   88
c ---[1025]---> BDD-cost:  123
c ---[1024]---> BDD-cost:  119
c ---[1023]---> BDD-cost:   88
c ---[1022]---> BDD-cost:   88
c ---[1021]---> BDD-cost:   88
c ---[1020]---> BDD-cost:   88
c ---[1019]---> BDD-cost:  119
c ---[1018]---> BDD-cost:  119
c ---[1017]---> BDD-cost:   88
c ---[1015]---> BDD-cost:   88
c ---[1014]---> BDD-cost:   88
c ---[1013]---> BDD-cost:   88
c ---[1012]---> BDD-cost:  125
c ---[1011]---> BDD-cost:  119
c ---[1010]---> BDD-cost:   88
c ---[1009]---> BDD-cost:   88
c ---[1008]---> BDD-cost:   88
c ---[1007]---> BDD-cost:   88
c ---[1006]---> BDD-cost:  125
c ---[1004]---> BDD-cost:  119
c ---[1003]---> BDD-cost:   88
c ---[1002]---> BDD-cost:   88
c ---[1001]---> BDD-cost:   88
c ---[1000]---> BDD-cost:   88
c ---[ 999]---> BDD-cost:  125
c ---[ 998]---> BDD-cost:  119
c ---[ 997]---> BDD-cost:   88
c ---[ 996]---> BDD-cost:   88
c ---[ 995]---> BDD-cost:   88
c ---[ 993]---> BDD-cost:   88
c ---[ 992]---> BDD-cost:  121
c ---[ 991]---> BDD-cost:  119
c ---[ 990]---> BDD-cost:   88
c ---[ 989]---> BDD-cost:   88
c ---[ 988]---> BDD-cost:   88
c ---[ 987]---> BDD-cost:   88
c ---[ 986]---> BDD-cost:  119
c ---[ 985]---> BDD-cost:  119
c ---[ 984]---> BDD-cost:   88
c ---[ 982]---> BDD-cost:   88
c ---[ 981]---> BDD-cost:   88
c ---[ 980]---> BDD-cost:   88
c ---[ 979]---> BDD-cost:  123
c ---[ 978]---> BDD-cost:  119
c ---[ 977]---> BDD-cost:   88
c ---[ 976]---> BDD-cost:   88
c ---[ 975]---> BDD-cost:   88
c ---[ 974]---> BDD-cost:   88
c ---[ 973]---> BDD-cost:  119
c ---[ 971]---> BDD-cost:  119
c ---[ 970]---> BDD-cost:   88
c ---[ 969]---> BDD-cost:   88
c ---[ 968]---> BDD-cost:   88
c ---[ 967]---> BDD-cost:   88
c ---[ 966]---> BDD-cost:  121
c ---[ 965]---> BDD-cost:  119
c ---[ 964]---> BDD-cost:   88
c ---[ 963]---> BDD-cost:   88
c ---[ 962]---> BDD-cost:   88
c ---[ 960]---> BDD-cost:   88
c ---[ 959]---> BDD-cost:  121
c ---[ 958]---> BDD-cost:  119
c ---[ 957]---> BDD-cost:   88
c ---[ 956]---> BDD-cost:   88
c ---[ 955]---> BDD-cost:   88
c ---[ 954]---> BDD-cost:   88
c ---[ 953]---> BDD-cost:  123
c ---[ 952]---> BDD-cost:  119
c ---[ 951]---> BDD-cost:   88
c ---[ 948]---> BDD-cost:   88
c ---[ 947]---> BDD-cost:   88
c ---[ 946]---> BDD-cost:   88
c ---[ 945]---> BDD-cost:  125
c ---[ 944]---> BDD-cost:  119
c ---[ 943]---> BDD-cost:   88
c ---[ 942]---> BDD-cost:   88
c ---[ 941]---> BDD-cost:   88
c ---[ 940]---> BDD-cost:   88
c ---[ 939]---> BDD-cost:  119
c ---[ 937]---> BDD-cost:  119
c ---[ 936]---> BDD-cost:   88
c ---[ 935]---> BDD-cost:   88
c ---[ 934]---> BDD-cost:   88
c ---[ 933]---> BDD-cost:   88
c ---[ 932]---> BDD-cost:  125
c ---[ 931]---> BDD-cost:  119
c ---[ 930]---> BDD-cost:   88
c ---[ 929]---> BDD-cost:   88
c ---[ 928]---> BDD-cost:   88
c ---[ 926]---> BDD-cost:   88
c ---[ 925]---> BDD-cost:  125
c ---[ 924]---> BDD-cost:  119
c ---[ 923]---> BDD-cost:   88
c ---[ 922]---> BDD-cost:   88
c ---[ 921]---> BDD-cost:   88
c ---[ 920]---> BDD-cost:   88
c ---[ 919]---> BDD-cost:  123
c ---[ 918]---> BDD-cost:  119
c ---[ 917]---> BDD-cost:   88
c ---[ 915]---> BDD-cost:   88
c ---[ 914]---> BDD-cost:   88
c ---[ 913]---> BDD-cost:   88
c ---[ 912]---> BDD-cost:  125
c ---[ 911]---> BDD-cost:  119
c ---[ 910]---> BDD-cost:   88
c ---[ 909]---> BDD-cost:   88
c ---[ 908]---> BDD-cost:   88
c ---[ 907]---> BDD-cost:   88
c ---[ 906]---> BDD-cost:  125
c ---[ 904]---> BDD-cost:  119
c ---[ 903]---> BDD-cost:   88
c ---[ 902]---> BDD-cost:   88
c ---[ 901]---> BDD-cost:   88
c ---[ 900]---> BDD-cost:   88
c ---[ 899]---> BDD-cost:  115
c ---[ 898]---> BDD-cost:  119
c ---[ 897]---> BDD-cost:   88
c ---[ 896]---> BDD-cost:   88
c ---[ 895]---> BDD-cost:   88
c ---[ 893]---> BDD-cost:   88
c ---[ 892]---> BDD-cost:  125
c ---[ 891]---> BDD-cost:  119
c ---[ 890]---> BDD-cost:   88
c ---[ 889]---> BDD-cost:   88
c ---[ 888]---> BDD-cost:   88
c ---[ 887]---> BDD-cost:   88
c ---[ 886]---> BDD-cost:  125
c ---[ 885]---> BDD-cost:  119
c ---[ 884]---> BDD-cost:   88
c ---[ 882]---> BDD-cost:   88
c ---[ 881]---> BDD-cost:   88
c ---[ 880]---> BDD-cost:   88
c ---[ 879]---> BDD-cost:  125
c ---[ 878]---> BDD-cost:  119
c ---[ 877]---> BDD-cost:   88
c ---[ 876]---> BDD-cost:   88
c ---[ 875]---> BDD-cost:   88
c ---[ 874]---> BDD-cost:   88
c ---[ 873]---> BDD-cost:  123
c ---[ 871]---> BDD-cost:  119
c ---[ 870]---> BDD-cost:   88
c ---[ 869]---> BDD-cost:   88
c ---[ 868]---> BDD-cost:   88
c ---[ 867]---> BDD-cost:   88
c ---[ 866]---> BDD-cost:  125
c ---[ 865]---> BDD-cost:  119
c ---[ 864]---> BDD-cost:   88
c ---[ 863]---> BDD-cost:   88
c ---[ 862]---> BDD-cost:   88
c ---[ 860]---> BDD-cost:   88
c ---[ 859]---> BDD-cost:  123
c ---[ 858]---> BDD-cost:  119
c ---[ 857]---> BDD-cost:   88
c ---[ 856]---> BDD-cost:   88
c ---[ 855]---> BDD-cost:   88
c ---[ 854]---> BDD-cost:   88
c ---[ 853]---> BDD-cost:  125
c ---[ 852]---> BDD-cost:  119
c ---[ 851]---> BDD-cost:   88
c ---[ 849]---> BDD-cost:   88
c ---[ 848]---> BDD-cost:   88
c ---[ 847]---> BDD-cost:   88
c ---[ 846]---> BDD-cost:  123
c ---[ 845]---> BDD-cost:  119
c ---[ 844]---> BDD-cost:   88
c ---[ 843]---> BDD-cost:   88
c ---[ 842]---> BDD-cost:   88
c ---[ 841]---> BDD-cost:   88
c ---[ 840]---> BDD-cost:  121
c ---[ 837]---> BDD-cost:  119
c ---[ 836]---> BDD-cost:   88
c ---[ 835]---> BDD-cost:   88
c ---[ 834]---> BDD-cost:   88
c ---[ 833]---> BDD-cost:   88
c ---[ 832]---> BDD-cost:  123
c ---[ 831]---> BDD-cost:  119
c ---[ 830]---> BDD-cost:   88
c ---[ 829]---> BDD-cost:   88
c ---[ 828]---> BDD-cost:   88
c ---[ 826]---> BDD-cost:   88
c ---[ 825]---> BDD-cost:  125
c ---[ 824]---> BDD-cost:  119
c ---[ 823]---> BDD-cost:   88
c ---[ 822]---> BDD-cost:   88
c ---[ 821]---> BDD-cost:   88
c ---[ 820]---> BDD-cost:   88
c ---[ 819]---> BDD-cost:  119
c ---[ 818]---> BDD-cost:  119
c ---[ 817]---> BDD-cost:   88
c ---[ 815]---> BDD-cost:   88
c ---[ 814]---> BDD-cost:   88
c ---[ 813]---> BDD-cost:   88
c ---[ 812]---> BDD-cost:  125
c ---[ 811]---> BDD-cost:  119
c ---[ 810]---> BDD-cost:   88
c ---[ 809]---> BDD-cost:   88
c ---[ 808]---> BDD-cost:   88
c ---[ 807]---> BDD-cost:   88
c ---[ 806]---> BDD-cost:  125
c ---[ 804]---> BDD-cost:  119
c ---[ 803]---> BDD-cost:   88
c ---[ 802]---> BDD-cost:   88
c ---[ 801]---> BDD-cost:   88
c ---[ 800]---> BDD-cost:   88
c ---[ 799]---> BDD-cost:  125
c ---[ 798]---> BDD-cost:  119
c ---[ 797]---> BDD-cost:   88
c ---[ 796]---> BDD-cost:   88
c ---[ 795]---> BDD-cost:   88
c ---[ 793]---> BDD-cost:   88
c ---[ 792]---> BDD-cost:  125
c ---[ 791]---> BDD-cost:  119
c ---[ 790]---> BDD-cost:   88
c ---[ 789]---> BDD-cost:   88
c ---[ 788]---> BDD-cost:   88
c ---[ 787]---> BDD-cost:   88
c ---[ 786]---> BDD-cost:  119
c ---[ 785]---> BDD-cost:  119
c ---[ 784]---> BDD-cost:   88
c ---[ 782]---> BDD-cost:   88
c ---[ 781]---> BDD-cost:   88
c ---[ 780]---> BDD-cost:   88
c ---[ 779]---> BDD-cost:  121
c ---[ 778]---> BDD-cost:  119
c ---[ 777]---> BDD-cost:   88
c ---[ 776]---> BDD-cost:   88
c ---[ 775]---> BDD-cost:   88
c ---[ 774]---> BDD-cost:   88
c ---[ 773]---> BDD-cost:  121
c ---[ 771]---> BDD-cost:  119
c ---[ 770]---> BDD-cost:   88
c ---[ 769]---> BDD-cost:   88
c ---[ 768]---> BDD-cost:   88
c ---[ 767]---> BDD-cost:   88
c ---[ 766]---> BDD-cost:  125
c ---[ 765]---> BDD-cost:  119
c ---[ 764]---> BDD-cost:   88
c ---[ 763]---> BDD-cost:   88
c ---[ 762]---> BDD-cost:   88
c ---[ 760]---> BDD-cost:   88
c ---[ 759]---> BDD-cost:  119
c ---[ 758]---> BDD-cost:  119
c ---[ 757]---> BDD-cost:   88
c ---[ 756]---> BDD-cost:   88
c ---[ 755]---> BDD-cost:   88
c ---[ 754]---> BDD-cost:   88
c ---[ 753]---> BDD-cost:  125
c ---[ 752]---> BDD-cost:  119
c ---[ 751]---> BDD-cost:   88
c ---[ 749]---> BDD-cost:   88
c ---[ 748]---> BDD-cost:   88
c ---[ 747]---> BDD-cost:   88
c ---[ 746]---> BDD-cost:  119
c ---[ 745]---> BDD-cost:  119
c ---[ 744]---> BDD-cost:   88
c ---[ 743]---> BDD-cost:   88
c ---[ 742]---> BDD-cost:   88
c ---[ 741]---> BDD-cost:   88
c ---[ 740]---> BDD-cost:  125
c ---[ 738]---> BDD-cost:  119
c ---[ 737]---> BDD-cost:   88
c ---[ 736]---> BDD-cost:   88
c ---[ 735]---> BDD-cost:   88
c ---[ 734]---> BDD-cost:   88
c ---[ 733]---> BDD-cost:  125
c ---[ 732]---> BDD-cost:  119
c ---[ 731]---> BDD-cost:   88
c ---[ 730]---> BDD-cost:   88
c ---[ 729]---> BDD-cost:   88
c ---[ 726]---> BDD-cost:   88
c ---[ 725]---> BDD-cost:  121
c ---[ 724]---> BDD-cost:  119
c ---[ 723]---> BDD-cost:   88
c ---[ 722]---> BDD-cost:   88
c ---[ 721]---> BDD-cost:   88
c ---[ 720]---> BDD-cost:   88
c ---[ 719]---> BDD-cost:  123
c ---[ 718]---> BDD-cost:  119
c ---[ 717]---> BDD-cost:   88
c ---[ 715]---> BDD-cost:   88
c ---[ 714]---> BDD-cost:   88
c ---[ 713]---> BDD-cost:   88
c ---[ 712]---> BDD-cost:  123
c ---[ 711]---> BDD-cost:  119
c ---[ 710]---> BDD-cost:   88
c ---[ 709]---> BDD-cost:   88
c ---[ 708]---> BDD-cost:   88
c ---[ 707]---> BDD-cost:   88
c ---[ 706]---> BDD-cost:  125
c ---[ 704]---> BDD-cost:  119
c ---[ 703]---> BDD-cost:   88
c ---[ 702]---> BDD-cost:   88
c ---[ 701]---> BDD-cost:   88
c ---[ 700]---> BDD-cost:   88
c ---[ 699]---> BDD-cost:  125
c ---[ 698]---> BDD-cost:  119
c ---[ 697]---> BDD-cost:   88
c ---[ 696]---> BDD-cost:   88
c ---[ 695]---> BDD-cost:   88
c ---[ 693]---> BDD-cost:   88
c ---[ 692]---> BDD-cost:  121
c ---[ 691]---> BDD-cost:  119
c ---[ 690]---> BDD-cost:   88
c ---[ 689]---> BDD-cost:   88
c ---[ 688]---> BDD-cost:   88
c ---[ 687]---> BDD-cost:   88
c ---[ 686]---> BDD-cost:  125
c ---[ 685]---> BDD-cost:  119
c ---[ 684]---> BDD-cost:   88
c ---[ 682]---> BDD-cost:   88
c ---[ 681]---> BDD-cost:   88
c ---[ 680]---> BDD-cost:   88
c ---[ 679]---> BDD-cost:  121
c ---[ 678]---> BDD-cost:  119
c ---[ 677]---> BDD-cost:   88
c ---[ 676]---> BDD-cost:   88
c ---[ 675]---> BDD-cost:   88
c ---[ 674]---> BDD-cost:   88
c ---[ 673]---> BDD-cost:  123
c ---[ 671]---> BDD-cost:  119
c ---[ 670]---> BDD-cost:   88
c ---[ 669]---> BDD-cost:   88
c ---[ 668]---> BDD-cost:   88
c ---[ 667]---> BDD-cost:   88
c ---[ 666]---> BDD-cost:  125
c ---[ 665]---> BDD-cost:  119
c ---[ 664]---> BDD-cost:   88
c ---[ 663]---> BDD-cost:   88
c ---[ 662]---> BDD-cost:   88
c ---[ 660]---> BDD-cost:   88
c ---[ 659]---> BDD-cost:  119
c ---[ 658]---> BDD-cost:  119
c ---[ 657]---> BDD-cost:   88
c ---[ 656]---> BDD-cost:   88
c ---[ 655]---> BDD-cost:   88
c ---[ 654]---> BDD-cost:   88
c ---[ 653]---> BDD-cost:  125
c ---[ 652]---> BDD-cost:  119
c ---[ 651]---> BDD-cost:   88
c ---[ 649]---> BDD-cost:   88
c ---[ 648]---> BDD-cost:   88
c ---[ 647]---> BDD-cost:   88
c ---[ 646]---> BDD-cost:  117
c ---[ 645]---> BDD-cost:  119
c ---[ 644]---> BDD-cost:   88
c ---[ 643]---> BDD-cost:   88
c ---[ 642]---> BDD-cost:   88
c ---[ 641]---> BDD-cost:   88
c ---[ 640]---> BDD-cost:  125
c ---[ 638]---> BDD-cost:  119
c ---[ 637]---> BDD-cost:   88
c ---[ 636]---> BDD-cost:   88
c ---[ 635]---> BDD-cost:   88
c ---[ 634]---> BDD-cost:   88
c ---[ 633]---> BDD-cost:  121
c ---[ 632]---> BDD-cost:  119
c ---[ 631]---> BDD-cost:   88
c ---[ 630]---> BDD-cost:   88
c ---[ 629]---> BDD-cost:   88
c ---[ 627]---> BDD-cost:   88
c ---[ 626]---> BDD-cost:  125
c ---[ 625]---> BDD-cost:  119
c ---[ 624]---> BDD-cost:   88
c ---[ 623]---> BDD-cost:   88
c ---[ 622]---> BDD-cost:   88
c ---[ 621]---> BDD-cost:   88
c ---[ 620]---> BDD-cost:  125
c ---[ 619]---> BDD-cost:  119
c ---[ 618]---> BDD-cost:   88
c ---[ 617]---> BDD-cost:   26
c ---[ 616]---> BDD-cost:   26
c ---[ 615]---> BDD-cost:   26
c ---[ 614]---> BDD-cost:   26
c ---[ 613]---> BDD-cost:   26
c ---[ 612]---> BDD-cost:   26
c ---[ 611]---> BDD-cost:   26
c ---[ 610]---> BDD-cost:   26
c ---[ 609]---> BDD-cost:   26
c ---[ 608]---> BDD-cost:   26
c ---[ 607]---> BDD-cost:   26
c ---[ 606]---> BDD-cost:   26
c ---[ 605]---> BDD-cost:   26
c ---[ 604]---> BDD-cost:   26
c ---[ 603]---> BDD-cost:   26
c ---[ 602]---> BDD-cost:   26
c ---[ 601]---> BDD-cost:   26
c ---[ 600]---> BDD-cost:   26
c ---[ 599]---> BDD-cost:   26
c ---[ 598]---> BDD-cost:   26
c ---[ 597]---> BDD-cost:   26
c ---[ 596]---> BDD-cost:   26
c ---[ 595]---> BDD-cost:   26
c ---[ 594]---> BDD-cost:   26
c ---[ 593]---> BDD-cost:   26
c ---[ 592]---> BDD-cost:   26
c ---[ 591]---> BDD-cost:   26
c ---[ 590]---> BDD-cost:   26
c ---[ 589]---> BDD-cost:   26
c ---[ 588]---> BDD-cost:   26
c ---[ 587]---> BDD-cost:   26
c ---[ 586]---> BDD-cost:   26
c ---[ 585]---> BDD-cost:   26
c ---[ 584]---> BDD-cost:   26
c ---[ 583]---> BDD-cost:   26
c ---[ 582]---> BDD-cost:   26
c ---[ 581]---> BDD-cost:   26
c ---[ 580]---> BDD-cost:   26
c ---[ 579]---> BDD-cost:   26
c ---[ 578]---> BDD-cost:   26
c ---[ 577]---> BDD-cost:   26
c ---[ 576]---> BDD-cost:   26
c ---[ 575]---> BDD-cost:   26
c ---[ 574]---> BDD-cost:   26
c ---[ 573]---> BDD-cost:   26
c ---[ 572]---> BDD-cost:   26
c ---[ 571]---> BDD-cost:   26
c ---[ 570]---> BDD-cost:   26
c ---[ 569]---> BDD-cost:   26
c ---[ 568]---> BDD-cost:   26
c ---[ 567]---> BDD-cost:   26
c ---[ 566]---> BDD-cost:   26
c ---[ 565]---> BDD-cost:   26
c ---[ 564]---> BDD-cost:   26
c ---[ 563]---> BDD-cost:   26
c ---[ 562]---> BDD-cost:   26
c ---[ 561]---> BDD-cost:   26
c ---[ 560]---> BDD-cost:   26
c ---[ 559]---> BDD-cost:   26
c ---[ 558]---> BDD-cost:   26
c ---[ 557]---> BDD-cost:   26
c ---[ 556]---> BDD-cost:   26
c ---[ 555]---> BDD-cost:   26
c ---[ 554]---> BDD-cost:   26
c ---[ 553]---> BDD-cost:   26
c ---[ 552]---> BDD-cost:   26
c ---[ 551]---> BDD-cost:   26
c ---[ 550]---> BDD-cost:   26
c ---[ 549]---> BDD-cost:   26
c ---[ 548]---> BDD-cost:   26
c ---[ 547]---> BDD-cost:   26
c ---[ 546]---> BDD-cost:   26
c ---[ 545]---> BDD-cost:   26
c ---[ 544]---> BDD-cost:   26
c ---[ 543]---> BDD-cost:   26
c ---[ 542]---> BDD-cost:   26
c ---[ 541]---> BDD-cost:   26
c ---[ 540]---> BDD-cost:   26
c ---[ 539]---> BDD-cost:   26
c ---[ 538]---> BDD-cost:   26
c ---[ 537]---> BDD-cost:   26
c ---[ 536]---> BDD-cost:   26
c ---[ 535]---> BDD-cost:   26
c ---[ 534]---> BDD-cost:   26
c ---[ 533]---> BDD-cost:   26
c ---[ 532]---> BDD-cost:   26
c ---[ 531]---> BDD-cost:   26
c ---[ 530]---> BDD-cost:   26
c ---[ 529]---> BDD-cost:   26
c ---[ 528]---> BDD-cost:   26
c ---[ 527]---> BDD-cost:   26
c ---[ 526]---> BDD-cost:   26
c ---[ 525]---> BDD-cost:   26
c ---[ 524]---> BDD-cost:   26
c ---[ 523]---> BDD-cost:   26
c ---[ 522]---> BDD-cost:   26
c ---[ 521]---> BDD-cost:   26
c ---[ 520]---> BDD-cost:   26
c ---[ 519]---> BDD-cost:   26
c ---[ 518]---> BDD-cost:   26
c ---[ 517]---> BDD-cost:   26
c ---[ 516]---> BDD-cost:   26
c ---[ 515]---> BDD-cost:   26
c ---[ 514]---> BDD-cost:   26
c ---[ 513]---> BDD-cost:   26
c ---[ 512]---> BDD-cost:   26
c ---[ 511]---> BDD-cost:   26
c ---[ 510]---> BDD-cost:   26
c ---[ 509]---> BDD-cost:   26
c ---[ 508]---> BDD-cost:   26
c ---[ 507]---> BDD-cost:   26
c ---[ 506]---> BDD-cost:   26
c ---[ 505]---> BDD-cost:   26
c ---[ 504]---> BDD-cost:   26
c ---[ 503]---> BDD-cost:   26
c ---[ 502]---> BDD-cost:   26
c ---[ 501]---> BDD-cost:   26
c ---[ 500]---> BDD-cost:   26
c ---[ 499]---> BDD-cost:   26
c ---[ 498]---> BDD-cost:   26
c ---[ 497]---> BDD-cost:   26
c ---[ 496]---> BDD-cost:   26
c ---[ 495]---> BDD-cost:   26
c ---[ 494]---> BDD-cost:   26
c ---[ 493]---> BDD-cost:   26
c ---[ 492]---> BDD-cost:   26
c ---[ 491]---> BDD-cost:   26
c ---[ 490]---> BDD-cost:   26
c ---[ 489]---> BDD-cost:   26
c ---[ 488]---> BDD-cost:   26
c ---[ 487]---> BDD-cost:   26
c ---[ 486]---> BDD-cost:   26
c ---[ 485]---> BDD-cost:   26
c ---[ 484]---> BDD-cost:   26
c ---[ 483]---> BDD-cost:   26
c ---[ 482]---> BDD-cost:   26
c ---[ 481]---> BDD-cost:   26
c ---[ 480]---> BDD-cost:   26
c ---[ 479]---> BDD-cost:   26
c ---[ 478]---> BDD-cost:   26
c ---[ 477]---> BDD-cost:   26
c ---[ 476]---> BDD-cost:   26
c ---[ 475]---> BDD-cost:   26
c ---[ 474]---> BDD-cost:   26
c ---[ 473]---> BDD-cost:   26
c ---[ 472]---> BDD-cost:   26
c ---[ 471]---> BDD-cost:   26
c ---[ 470]---> BDD-cost:   26
c ---[ 469]---> BDD-cost:   26
c ---[ 468]---> BDD-cost:   26
c ---[ 467]---> BDD-cost:   26
c ---[ 466]---> BDD-cost:   26
c ---[ 465]---> BDD-cost:   26
c ---[ 464]---> BDD-cost:   26
c ---[ 463]---> BDD-cost:   26
c ---[ 462]---> BDD-cost:   26
c ---[ 461]---> BDD-cost:   26
c ---[ 460]---> BDD-cost:   26
c ---[ 459]---> BDD-cost:   26
c ---[ 458]---> BDD-cost:   26
c ---[ 457]---> BDD-cost:   26
c ---[ 456]---> BDD-cost:   26
c ---[ 455]---> BDD-cost:   26
c ---[ 454]---> BDD-cost:   26
c ---[ 453]---> BDD-cost:   26
c ---[ 452]---> BDD-cost:   26
c ---[ 451]---> BDD-cost:   26
c ---[ 450]---> BDD-cost:   26
c ---[ 449]---> BDD-cost:   26
c ---[ 448]---> BDD-cost:   26
c ---[ 447]---> BDD-cost:   26
c ---[ 446]---> BDD-cost:   26
c ---[ 445]---> BDD-cost:   26
c ---[ 444]---> BDD-cost:   26
c ---[ 443]---> BDD-cost:   26
c ---[ 442]---> BDD-cost:   26
c ---[ 441]---> BDD-cost:   26
c ---[ 440]---> BDD-cost:   26
c ---[ 439]---> BDD-cost:   26
c ---[ 438]---> BDD-cost:   26
c ---[ 437]---> BDD-cost:   26
c ---[ 436]---> BDD-cost:   26
c ---[ 435]---> BDD-cost:   26
c ---[ 434]---> BDD-cost:   26
c ---[ 433]---> BDD-cost:   26
c ---[ 432]---> BDD-cost:   26
c ---[ 431]---> BDD-cost:   26
c ---[ 430]---> BDD-cost:   26
c ---[ 429]---> BDD-cost:   26
c ---[ 428]---> BDD-cost:   26
c ---[ 427]---> BDD-cost:   26
c ---[ 426]---> BDD-cost:   26
c ---[ 425]---> BDD-cost:   26
c ---[ 424]---> BDD-cost:   26
c ---[ 423]---> BDD-cost:   26
c ---[ 422]---> BDD-cost:   26
c ---[ 421]---> BDD-cost:   26
c ---[ 420]---> BDD-cost:   26
c ---[ 419]---> BDD-cost:   26
c ---[ 418]---> BDD-cost:   26
c ---[ 417]---> BDD-cost:   26
c ---[ 416]---> BDD-cost:   26
c ---[ 415]---> BDD-cost:   26
c ---[ 414]---> BDD-cost:   26
c ---[ 413]---> BDD-cost:   26
c ---[ 412]---> BDD-cost:   26
c ---[ 411]---> BDD-cost:   26
c ---[ 410]---> BDD-cost:   26
c ---[ 409]---> BDD-cost:   26
c ---[ 408]---> BDD-cost:   26
c ---[ 407]---> BDD-cost:   26
c ---[ 406]---> BDD-cost:   26
c ---[ 405]---> BDD-cost:   26
c ---[ 404]---> BDD-cost:   26
c ---[ 403]---> BDD-cost:   26
c ---[ 402]---> BDD-cost:   26
c ---[ 401]---> BDD-cost:   26
c ---[ 400]---> BDD-cost:   26
c ---[ 399]---> BDD-cost:   26
c ---[ 398]---> BDD-cost:   26
c ---[ 397]---> BDD-cost:   26
c ---[ 396]---> BDD-cost:   26
c ---[ 395]---> BDD-cost:   26
c ---[ 394]---> BDD-cost:   26
c ---[ 393]---> BDD-cost:   26
c ---[ 392]---> BDD-cost:   26
c ---[ 391]---> BDD-cost:   26
c ---[ 390]---> BDD-cost:   26
c ---[ 389]---> BDD-cost:   26
c ---[ 388]---> BDD-cost:   26
c ---[ 387]---> BDD-cost:   26
c ---[ 386]---> BDD-cost:   26
c ---[ 385]---> BDD-cost:   26
c ---[ 384]---> BDD-cost:   26
c ---[ 383]---> BDD-cost:   26
c ---[ 382]---> BDD-cost:   26
c ---[ 381]---> BDD-cost:   26
c ---[ 380]---> BDD-cost:   26
c ---[ 379]---> BDD-cost:   26
c ---[ 378]---> BDD-cost:   26
c ---[ 377]---> BDD-cost:   26
c ---[ 376]---> BDD-cost:   26
c ---[ 375]---> BDD-cost:   26
c ---[ 374]---> BDD-cost:   26
c ---[ 373]---> BDD-cost:   26
c ---[ 372]---> BDD-cost:   26
c ---[ 371]---> BDD-cost:   26
c ---[ 370]---> BDD-cost:   26
c ---[ 369]---> BDD-cost:   26
c ---[ 368]---> BDD-cost:   26
c ---[ 367]---> BDD-cost:   26
c ---[ 366]---> BDD-cost:   26
c ---[ 365]---> BDD-cost:   26
c ---[ 364]---> BDD-cost:   26
c ---[ 363]---> BDD-cost:   26
c ---[ 362]---> BDD-cost:   26
c ---[ 361]---> BDD-cost:   26
c ---[ 360]---> BDD-cost:   26
c ---[ 359]---> BDD-cost:   26
c ---[ 358]---> BDD-cost:   26
c ---[ 357]---> BDD-cost:   26
c ---[ 356]---> BDD-cost:   26
c ---[ 355]---> BDD-cost:   26
c ---[ 354]---> BDD-cost:   26
c ---[ 353]---> BDD-cost:   26
c ---[ 352]---> BDD-cost:   26
c ---[ 351]---> BDD-cost:   26
c ---[ 350]---> BDD-cost:   26
c ---[ 349]---> BDD-cost:   26
c ---[ 348]---> BDD-cost:   26
c ---[ 347]---> BDD-cost:   26
c ---[ 346]---> BDD-cost:   26
c ---[ 345]---> BDD-cost:   26
c ---[ 344]---> BDD-cost:   26
c ---[ 343]---> BDD-cost:   26
c ---[ 342]---> BDD-cost:   26
c ---[ 341]---> BDD-cost:   26
c ---[ 340]---> BDD-cost:   26
c ---[ 339]---> BDD-cost:   26
c ---[ 338]---> BDD-cost:   26
c ---[ 337]---> BDD-cost:   26
c ---[ 336]---> BDD-cost:   26
c ---[ 335]---> BDD-cost:   26
c ---[ 334]---> BDD-cost:   26
c ---[ 333]---> BDD-cost:   26
c ---[ 332]---> BDD-cost:   26
c ---[ 331]---> BDD-cost:   26
c ---[ 330]---> BDD-cost:   26
c ---[ 329]---> BDD-cost:   26
c ---[ 328]---> BDD-cost:   26
c ---[ 327]---> BDD-cost:   26
c ---[ 326]---> BDD-cost:   26
c ---[ 325]---> BDD-cost:   26
c ---[ 324]---> BDD-cost:   26
c ---[ 323]---> BDD-cost:   26
c ---[ 322]---> BDD-cost:   26
c ---[ 321]---> BDD-cost:   26
c ---[ 320]---> BDD-cost:   26
c ---[ 319]---> BDD-cost:   26
c ---[ 318]---> BDD-cost:   26
c ---[ 317]---> BDD-cost:   26
c ---[ 316]---> BDD-cost:   26
c ---[ 315]---> BDD-cost:   26
c ---[ 314]---> BDD-cost:   26
c ---[ 313]---> BDD-cost:   26
c ---[ 312]---> BDD-cost:   26
c ---[ 311]---> BDD-cost:   26
c ---[ 310]---> BDD-cost:   26
c ---[ 309]---> BDD-cost:   26
c ---[ 308]---> BDD-cost:   26
c ---[ 307]---> BDD-cost:   26
c ---[ 306]---> BDD-cost:   26
c ---[ 305]---> BDD-cost:   26
c ---[ 304]---> BDD-cost:   26
c ---[ 303]---> BDD-cost:   26
c ---[ 302]---> BDD-cost:   26
c ---[ 301]---> BDD-cost:   26
c ---[ 300]---> BDD-cost:   26
c ---[ 299]---> BDD-cost:   26
c ---[ 298]---> BDD-cost:   26
c ---[ 297]---> BDD-cost:   26
c ---[ 296]---> BDD-cost:   26
c ---[ 295]---> BDD-cost:   26
c ---[ 294]---> BDD-cost:   26
c ---[ 293]---> BDD-cost:   26
c ---[ 292]---> BDD-cost:   26
c ---[ 291]---> BDD-cost:   26
c ---[ 290]---> BDD-cost:   26
c ---[ 289]---> BDD-cost:   26
c ---[ 288]---> BDD-cost:   26
c ---[ 287]---> BDD-cost:   26
c ---[ 286]---> BDD-cost:   26
c ---[ 285]---> BDD-cost:   26
c ---[ 284]---> BDD-cost:   26
c ---[ 283]---> BDD-cost:   26
c ---[ 282]---> BDD-cost:   26
c ---[ 281]---> BDD-cost:   26
c ---[ 280]---> BDD-cost:   26
c ---[ 279]---> BDD-cost:   26
c ---[ 278]---> BDD-cost:   26
c ---[ 277]---> BDD-cost:   26
c ---[ 276]---> BDD-cost:   26
c ---[ 275]---> BDD-cost:   26
c ---[ 274]---> BDD-cost:   26
c ---[ 273]---> BDD-cost:   26
c ---[ 272]---> BDD-cost:   26
c ---[ 271]---> BDD-cost:   26
c ---[ 270]---> BDD-cost:   26
c ---[ 269]---> BDD-cost:   26
c ---[ 268]---> BDD-cost:   26
c ---[ 267]---> BDD-cost:   26
c ---[ 266]---> BDD-cost:   26
c ---[ 265]---> BDD-cost:   26
c ---[ 264]---> BDD-cost:   26
c ---[ 263]---> BDD-cost:   26
c ---[ 262]---> BDD-cost:   26
c ---[ 261]---> BDD-cost:   26
c ---[ 260]---> BDD-cost:   26
c ---[ 259]---> BDD-cost:   26
c ---[ 258]---> BDD-cost:   26
c ---[ 257]---> BDD-cost:   26
c ---[ 256]---> BDD-cost:   26
c ---[ 255]---> BDD-cost:   26
c ---[ 254]---> BDD-cost:   26
c ---[ 253]---> BDD-cost:   26
c ---[ 252]---> BDD-cost:   26
c ---[ 251]---> BDD-cost:   26
c ---[ 250]---> BDD-cost:   26
c ---[ 249]---> BDD-cost:   26
c ---[ 248]---> BDD-cost:   26
c ---[ 247]---> BDD-cost:   26
c ---[ 246]---> BDD-cost:   26
c ---[ 245]---> BDD-cost:   26
c ---[ 244]---> BDD-cost:   26
c ---[ 243]---> BDD-cost:   26
c ---[ 242]---> BDD-cost:   26
c ---[ 241]---> BDD-cost:   26
c ---[ 240]---> BDD-cost:   26
c ---[ 239]---> BDD-cost:   26
c ---[ 238]---> BDD-cost:   26
c ---[ 237]---> BDD-cost:   26
c ---[ 236]---> BDD-cost:   26
c ---[ 235]---> BDD-cost:   26
c ---[ 234]---> BDD-cost:   26
c ---[ 233]---> BDD-cost:   26
c ---[ 232]---> BDD-cost:   26
c ---[ 231]---> BDD-cost:   26
c ---[ 230]---> BDD-cost:   26
c ---[ 229]---> BDD-cost:   26
c ---[ 228]---> BDD-cost:   26
c ---[ 227]---> BDD-cost:   26
c ---[ 226]---> BDD-cost:   26
c ---[ 225]---> BDD-cost:   26
c ---[ 224]---> BDD-cost:   26
c ---[ 223]---> BDD-cost:   26
c ---[ 222]---> BDD-cost:   26
c ---[ 221]---> BDD-cost:   26
c ---[ 220]---> BDD-cost:   26
c ---[ 219]---> BDD-cost:   26
c ---[ 218]---> BDD-cost:   26
c ---[ 217]---> BDD-cost:   26
c ---[ 216]---> BDD-cost:   26
c ---[ 215]---> BDD-cost:   26
c ---[ 214]---> BDD-cost:   26
c ---[ 213]---> BDD-cost:   26
c ---[ 212]---> BDD-cost:   26
c ---[ 211]---> BDD-cost:   26
c ---[ 210]---> BDD-cost:   26
c ---[ 209]---> BDD-cost:   26
c ---[ 208]---> BDD-cost:   26
c ---[ 207]---> BDD-cost:   26
c ---[ 206]---> BDD-cost:   26
c ---[ 205]---> BDD-cost:   26
c ---[ 204]---> BDD-cost:   26
c ---[ 203]---> BDD-cost:   26
c ---[ 202]---> BDD-cost:   26
c ---[ 201]---> BDD-cost:   26
c ---[ 200]---> BDD-cost:   26
c ---[ 199]---> BDD-cost:   26
c ---[ 198]---> BDD-cost:   26
c ---[ 197]---> BDD-cost:   26
c ---[ 196]---> BDD-cost:   26
c ---[ 195]---> BDD-cost:   26
c ---[ 194]---> BDD-cost:   26
c ---[ 193]---> BDD-cost:   26
c ---[ 192]---> BDD-cost:   26
c ---[ 191]---> BDD-cost:   26
c ---[ 190]---> BDD-cost:   26
c ---[ 189]---> BDD-cost:   26
c ---[ 188]---> BDD-cost:   26
c ---[ 187]---> BDD-cost:   26
c ---[ 186]---> BDD-cost:   26
c ---[ 185]---> BDD-cost:   26
c ---[ 184]---> BDD-cost:   26
c ---[ 183]---> BDD-cost:   26
c ---[ 182]---> BDD-cost:   26
c ---[ 181]---> BDD-cost:   26
c ---[ 180]---> BDD-cost:   26
c ---[ 179]---> BDD-cost:   26
c ---[ 178]---> BDD-cost:   26
c ---[ 177]---> BDD-cost:   26
c ---[ 176]---> BDD-cost:   26
c ---[ 175]---> BDD-cost:   26
c ---[ 174]---> BDD-cost:   26
c ---[ 173]---> BDD-cost:   26
c ---[ 172]---> BDD-cost:   26
c ---[ 171]---> BDD-cost:   26
c ---[ 170]---> BDD-cost:   26
c ---[ 169]---> BDD-cost:   26
c ---[ 168]---> BDD-cost:   26
c ---[ 167]---> BDD-cost:   26
c ---[ 166]---> BDD-cost:   26
c ---[ 165]---> BDD-cost:   26
c ---[ 164]---> BDD-cost:   26
c ---[ 163]---> BDD-cost:   26
c ---[ 162]---> BDD-cost:   26
c ---[ 161]---> BDD-cost:   26
c ---[ 160]---> BDD-cost:   26
c ---[ 159]---> BDD-cost:   26
c ---[ 158]---> BDD-cost:   26
c ---[ 157]---> BDD-cost:   26
c ---[ 156]---> BDD-cost:   26
c ---[ 155]---> BDD-cost:   26
c ---[ 154]---> BDD-cost:   26
c ---[ 153]---> BDD-cost:   26
c ---[ 152]---> BDD-cost:   26
c ---[ 151]---> BDD-cost:   26
c ---[ 150]---> BDD-cost:   26
c ---[ 149]---> BDD-cost:   26
c ---[ 148]---> BDD-cost:   26
c ---[ 147]---> BDD-cost:   26
c ---[ 146]---> BDD-cost:   26
c ---[ 145]---> BDD-cost:   26
c ---[ 144]---> BDD-cost:   26
c ---[ 143]---> BDD-cost:   26
c ---[ 142]---> BDD-cost:   26
c ---[ 141]---> BDD-cost:   26
c ---[ 140]---> BDD-cost:   26
c ---[ 139]---> BDD-cost:   26
c ---[ 138]---> BDD-cost:   26
c ---[ 137]---> BDD-cost:   26
c ---[ 136]---> BDD-cost:   26
c ---[ 135]---> BDD-cost:   26
c ---[ 134]---> BDD-cost:   26
c ---[ 133]---> BDD-cost:   26
c ---[ 132]---> BDD-cost:   26
c ---[ 131]---> BDD-cost:   26
c ---[ 130]---> BDD-cost:   26
c ---[ 129]---> BDD-cost:   26
c ---[ 128]---> BDD-cost:   26
c ---[ 127]---> BDD-cost:   26
c ---[ 126]---> BDD-cost:   26
c ---[ 125]---> BDD-cost:   26
c ---[ 124]---> BDD-cost:   26
c ---[ 123]---> BDD-cost:   26
c ---[ 122]---> BDD-cost:   26
c ---[ 121]---> BDD-cost:   26
c ---[ 120]---> BDD-cost:   26
c ---[ 119]---> BDD-cost:   26
c ---[ 118]---> BDD-cost:   26
c ---[ 117]---> BDD-cost:   26
c ---[ 116]---> BDD-cost:   26
c ---[ 115]---> BDD-cost:   26
c ---[ 114]---> BDD-cost:   26
c ---[ 113]---> BDD-cost:   26
c ---[ 112]---> BDD-cost:   26
c ---[ 111]---> BDD-cost:   26
c ---[ 110]---> BDD-cost:   26
c ---[ 109]---> BDD-cost:   26
c ---[ 108]---> BDD-cost:   26
c ---[ 107]---> BDD-cost:   26
c ---[ 106]---> BDD-cost:   26
c ---[ 105]---> BDD-cost:   26
c ---[ 104]---> BDD-cost:   26
c ---[ 103]---> BDD-cost:   26
c ---[ 102]---> BDD-cost:   26
c ---[ 101]---> BDD-cost:   26
c ---[ 100]---> BDD-cost:   26
c ---[  99]---> BDD-cost:   26
c ---[  98]---> BDD-cost:   26
c ---[  97]---> BDD-cost:   26
c ---[  96]---> BDD-cost:   26
c ---[  95]---> BDD-cost:   26
c ---[  94]---> BDD-cost:   26
c ---[  93]---> BDD-cost:   26
c ---[  92]---> BDD-cost:   26
c ---[  91]---> BDD-cost:   26
c ---[  90]---> BDD-cost:   26
c ---[  89]---> BDD-cost:   26
c ---[  88]---> BDD-cost:   26
c ---[  87]---> BDD-cost:   26
c ---[  86]---> BDD-cost:   26
c ---[  85]---> BDD-cost:   26
c ---[  84]---> BDD-cost:   26
c ---[  83]---> BDD-cost:   26
c ---[  82]---> BDD-cost:   26
c ---[  81]---> BDD-cost:   26
c ---[  80]---> BDD-cost:   26
c ---[  79]---> BDD-cost:   26
c ---[  78]---> BDD-cost:   26
c ---[  77]---> BDD-cost:   26
c ---[  76]---> BDD-cost:   26
c ---[  75]---> BDD-cost:   26
c ---[  74]---> BDD-cost:   26
c ---[  73]---> BDD-cost:   26
c ---[  72]---> BDD-cost:   26
c ---[  71]---> BDD-cost:   26
c ---[  70]---> BDD-cost:   26
c ---[  69]---> BDD-cost:   26
c ---[  68]---> BDD-cost:   26
c ---[  67]---> BDD-cost:   26
c ---[  66]---> BDD-cost:   26
c ---[  65]---> BDD-cost:   26
c ---[  64]---> BDD-cost:   26
c ---[  63]---> BDD-cost:   26
c ---[  62]---> BDD-cost:   26
c ---[  61]---> BDD-cost:   26
c ---[  60]---> BDD-cost:   26
c ---[  59]---> BDD-cost:   26
c ---[  58]---> BDD-cost:   26
c ---[  57]---> BDD-cost:   26
c ---[  56]---> BDD-cost:   26
c ---[  55]---> BDD-cost:   26
c ---[  54]---> BDD-cost:   26
c ---[  53]---> BDD-cost:   26
c ---[  52]---> BDD-cost:   26
c ---[  51]---> BDD-cost:   26
c ---[  50]---> BDD-cost:   26
c ---[  49]---> BDD-cost:   26
c ---[  48]---> BDD-cost:   26
c ---[  47]---> BDD-cost:   26
c ---[  46]---> BDD-cost:   26
c ---[  45]---> BDD-cost:   26
c ---[  44]---> BDD-cost:   26
c ---[  43]---> BDD-cost:   26
c ---[  42]---> BDD-cost:   26
c ---[  41]---> BDD-cost:   26
c ---[  40]---> BDD-cost:   26
c ---[  39]---> BDD-cost:   26
c ---[  38]---> BDD-cost:   26
c ---[  37]---> BDD-cost:   26
c ---[  36]---> BDD-cost:   26
c ---[  35]---> BDD-cost:   26
c ---[  34]---> BDD-cost:   26
c ---[  33]---> BDD-cost:   26
c ---[  32]---> BDD-cost:   26
c ---[  31]---> BDD-cost:   26
c ---[  30]---> BDD-cost:   26
c ---[  29]---> BDD-cost:   26
c ---[  28]---> BDD-cost:   26
c ---[  27]---> BDD-cost:   26
c ---[  26]---> BDD-cost:   26
c ---[  25]---> BDD-cost:   26
c ---[  24]---> BDD-cost:   26
c ---[  23]---> BDD-cost:   26
c ---[  22]---> BDD-cost:   26
c ---[  21]---> BDD-cost:   26
c ---[  20]---> BDD-cost:   26
c ---[  19]---> BDD-cost:   26
c ---[  18]---> BDD-cost:   26
c ---[  17]---> BDD-cost:   26
c ---[  16]---> BDD-cost:   26
c ---[  15]---> BDD-cost:   26
c ---[  14]---> BDD-cost:   26
c ---[  13]---> BDD-cost:   26
c ---[  12]---> BDD-cost:   26
c ---[  11]---> BDD-cost:   26
c ---[  10]---> BDD-cost:   26
c ---[   9]---> BDD-cost:   26
c ---[   8]---> BDD-cost:   26
c ---[   7]---> BDD-cost:   26
c ---[   6]---> BDD-cost:   26
c ---[   5]---> BDD-cost:   26
c ---[   4]---> BDD-cost:   26
c ---[   3]---> BDD-cost:   26
c ---[   2]---> BDD-cost:   26
c ---[   1]---> BDD-cost:   26
c ---[   0]---> BDD-cost:   26
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |  488187  1305639 |  162729       0        0     nan |  0.000 % |
c |       100 |  488185  1305635 |  179001      99      789     8.0 |  1.103 % |
c |       250 |  488063  1305391 |  196902     188     1628     8.7 |  1.129 % |
c |       475 |  488063  1305391 |  216592     413     4167    10.1 |  1.129 % |
c |       815 |  488041  1305347 |  238251     742     6934     9.3 |  1.133 % |
c |      1322 |  488029  1305323 |  262076    1243    10742     8.6 |  1.136 % |
c |      2081 |  487977  1305219 |  288284    1975    17960     9.1 |  1.147 % |
c ==============================================================================
c [1mFound solution: 509952[0m
c ---[   0]---> BDD-cost:  302
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      2403 |  488597  1307159 |  162865    2256    20043     8.9 |  1.147 % |
c |      2503 |  488593  1307151 |  179151    2354    21203     9.0 |  1.165 % |
c |      2653 |  488497  1306959 |  197066    2455    22238     9.1 |  1.185 % |
c |      2878 |  488497  1306959 |  216773    2680    24154     9.0 |  1.185 % |
c |      3215 |  488457  1306878 |  238450    2993    27148     9.1 |  1.194 % |
c |      3721 |  488365  1306669 |  262295    3436    31174     9.1 |  1.213 % |
c |      4480 |  488305  1306549 |  288525    4164    40133     9.6 |  1.226 % |
c |      5619 |  488221  1306381 |  317377    5261    67360    12.8 |  1.244 % |
c |      7327 |  487913  1305763 |  349115    6791    88202    13.0 |  1.309 % |
c ==============================================================================
c [1mFound solution: 504832[0m
c ---[   0]---> Sorter-cost: 2294     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      8776 |  489972  1310672 |  163324    8192   101532    12.4 |  1.309 % |
c |      8876 |  489816  1310360 |  179656    8214   102159    12.4 |  1.355 % |
c |      9026 |  489814  1310356 |  197622    8363   103236    12.3 |  1.356 % |
c |      9253 |  489810  1310347 |  217384    8588   105229    12.3 |  1.357 % |
c |      9593 |  489810  1310347 |  239122    8928   110143    12.3 |  1.357 % |
c |     10099 |  489792  1310309 |  263034    9425   114248    12.1 |  1.360 % |
c ==============================================================================
c [1mFound solution: 486400[0m
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     10584 |  490072  1311028 |  163357    9908   118314    11.9 |  1.360 % |
c |     10685 |  490068  1311020 |  179692   10007   118780    11.9 |  1.361 % |
c |     10835 |  489952  1310788 |  197661   10099   120038    11.9 |  1.386 % |
c |     11060 |  489944  1310768 |  217428   10315   122033    11.8 |  1.388 % |
c |     11397 |  489928  1310733 |  239170   10640   125628    11.8 |  1.391 % |
c |     11904 |  489904  1310685 |  263088   11135   130372    11.7 |  1.396 % |
c |     12665 |  489892  1310661 |  289396   11890   138004    11.6 |  1.399 % |
c ==============================================================================
c [1mFound solution: 484352[0m
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     12948 |  489933  1310791 |  163311   12173   140189    11.5 |  1.399 % |
c |     13048 |  489933  1310791 |  179642   12273   141133    11.5 |  1.399 % |
c |     13198 |  489915  1310755 |  197606   12414   142018    11.4 |  1.403 % |
c |     13425 |  489907  1310739 |  217366   12637   143893    11.4 |  1.404 % |
c |     13762 |  489861  1310647 |  239103   12951   146544    11.3 |  1.414 % |
c |     14270 |  489827  1310579 |  263013   13442   153696    11.4 |  1.421 % |
c |     15029 |  489423  1309770 |  289315   13992   158235    11.3 |  1.507 % |
c |     16168 |  489323  1309565 |  318246   15080   172099    11.4 |  1.528 % |
c |     17876 |  489021  1308932 |  350071   16627   189481    11.4 |  1.592 % |
c ==============================================================================
c [1mFound solution: 478208[0m
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     18666 |  489074  1309091 |  163024   17388   197240    11.3 |  1.592 % |
c |     18766 |  489072  1309087 |  179326   17487   198358    11.3 |  1.596 % |
c |     18916 |  489072  1309087 |  197259   17637   199352    11.3 |  1.596 % |
c |     19143 |  489060  1309063 |  216984   17858   201622    11.3 |  1.599 % |
c |     19480 |  489054  1309048 |  238683   18192   204459    11.2 |  1.600 % |
c |     19986 |  489026  1308988 |  262551   18683   209275    11.2 |  1.606 % |
c |     20746 |  488876  1308687 |  288806   19337   216181    11.2 |  1.637 % |
c |     21885 |  488874  1308683 |  317687   20475   241222    11.8 |  1.638 % |
c |     23593 |  488792  1308506 |  349456   22099   264375    12.0 |  1.655 % |
c ==============================================================================
c [1mFound solution: 466944[0m
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     25578 |  488719  1308414 |  162906   23961   286320    11.9 |  1.655 % |
c |     25678 |  488719  1308414 |  179196   24061   287221    11.9 |  1.694 % |
c |     25828 |  488679  1308332 |  197116   24184   288447    11.9 |  1.703 % |
c |     26053 |  488665  1308303 |  216827   24401   290393    11.9 |  1.706 % |
c |     26390 |  488663  1308298 |  238510   24738   294108    11.9 |  1.706 % |
c |     26896 |  488651  1308272 |  262361   25237   299632    11.9 |  1.709 % |
c |     27655 |  488487  1307935 |  288597   25805   305333    11.8 |  1.744 % |
c |     28794 |  488459  1307874 |  317457   26917   331270    12.3 |  1.749 % |
c |     30504 |  488387  1307727 |  349203   28585   367222    12.8 |  1.765 % |
c |     33067 |  488341  1307625 |  384123   31005   398173    12.8 |  1.774 % |
c |     36912 |  488163  1307239 |  422536   34671   442476    12.8 |  1.812 % |
c |     42679 |  487989  1306877 |  464789   40233   532968    13.2 |  1.849 % |
c ==============================================================================
c [1mFound solution: 458752[0m
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     48416 |  487694  1306261 |  162564   45607   607211    13.3 |  1.849 % |
c |     48516 |  487692  1306255 |  178820   45687   607739    13.3 |  1.930 % |
c |     48666 |  487690  1306250 |  196702   45836   609914    13.3 |  1.930 % |
c |     48891 |  487690  1306250 |  216372   46061   615937    13.4 |  1.930 % |
c |     49228 |  487690  1306250 |  238009   46398   619899    13.4 |  1.930 % |
c |     49735 |  487690  1306250 |  261810   46905   640594    13.7 |  1.930 % |
c |     50494 |  487686  1306241 |  287992   47662   650442    13.6 |  1.931 % |
c |     51633 |  487614  1306090 |  316791   48763   664046    13.6 |  1.946 % |
c ==============================================================================
c [1mFound solution: 444416[0m
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     52539 |  487692  1306267 |  162564   49667   678006    13.7 |  1.946 % |
c |     52640 |  487682  1306242 |  178820   49746   678713    13.6 |  1.954 % |
c |     52791 |  487682  1306242 |  196702   49897   680863    13.6 |  1.954 % |
c |     53016 |  487682  1306242 |  216372   50122   683654    13.6 |  1.954 % |
c |     53353 |  487682  1306242 |  238009   50459   688957    13.7 |  1.954 % |
c |     53859 |  487680  1306238 |  261810   50964   695495    13.6 |  1.954 % |
c |     54618 |  487674  1306226 |  287992   51720   710989    13.7 |  1.956 % |
c |     55757 |  487662  1306201 |  316791   52853   725090    13.7 |  1.958 % |
c |     57466 |  487574  1306005 |  348470   54358   749995    13.8 |  1.977 % |
c |     60029 |  487542  1305933 |  383317   56882   793160    13.9 |  1.983 % |
c |     63873 |  487532  1305913 |  421649   60721   853591    14.1 |  1.986 % |
c |     69640 |  487480  1305802 |  463814   66359   960612    14.5 |  1.997 % |
c |     78289 |  487418  1305657 |  510195   74962  1122376    15.0 |  2.010 % |
c |     91263 |  487368  1305543 |  561215   87862  1353859    15.4 |  2.020 % |
c ==============================================================================
c [1mFound solution: 434176[0m
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    102565 |  487244  1305253 |  162414   99036  1626517    16.4 |  2.020 % |
c |    102665 |  487244  1305253 |  178655   99136  1628375    16.4 |  2.062 % |
c |    102816 |  487236  1305237 |  196520   99283  1629665    16.4 |  2.063 % |
c |    103041 |  487236  1305237 |  216173   99508  1631321    16.4 |  2.063 % |
c |    103378 |  487234  1305233 |  237790   99844  1636231    16.4 |  2.064 % |
c |    103884 |  487230  1305225 |  261569  100348  1642807    16.4 |  2.065 % |
c |    104643 |  487228  1305221 |  287726  101106  1651816    16.3 |  2.065 % |
c |    105784 |  487228  1305221 |  316498  102247  1676904    16.4 |  2.065 % |
c |    107493 |  487204  1305163 |  348148  103873  1707407    16.4 |  2.070 % |
c |    110056 |  487194  1305143 |  382963  106431  1746112    16.4 |  2.072 % |
c ==============================================================================
c [1mFound solution: 432128[0m
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    110396 |  487195  1305136 |  162398  106770  1749859    16.4 |  2.072 % |
c |    110496 |  487195  1305136 |  178637  106870  1752728    16.4 |  2.078 % |
c |    110646 |  487187  1305120 |  196501  107016  1755212    16.4 |  2.079 % |
c |    110875 |  487177  1305098 |  216151  107236  1759906    16.4 |  2.081 % |
c |    111213 |  487169  1305078 |  237766  107570  1767251    16.4 |  2.083 % |
c ==============================================================================
c [1mFound solution: 428032[0m
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    111559 |  487179  1305090 |  162393  107914  1772040    16.4 |  2.083 % |
c |    111660 |  487177  1305086 |  178632  108014  1773955    16.4 |  2.089 % |
c |    111810 |  487167  1305064 |  196495  108147  1775716    16.4 |  2.091 % |
c |    112035 |  487167  1305064 |  216145  108372  1778762    16.4 |  2.091 % |
c |    112374 |  487167  1305064 |  237759  108711  1785107    16.4 |  2.091 % |
c |    112880 |  487165  1305060 |  261535  109216  1793849    16.4 |  2.091 % |
c |    113639 |  487119  1304953 |  287689  109921  1805647    16.4 |  2.101 % |
c |    114778 |  487113  1304941 |  316458  111057  1821343    16.4 |  2.102 % |
c |    116486 |  487113  1304941 |  348103  112765  1871438    16.6 |  2.102 % |
c |    119049 |  487101  1304917 |  382914  115322  1908816    16.6 |  2.105 % |
/oldhome/oroussel/solvers/minisat+_script: line 9:  5407 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.97 0.96 2/54 5403
Raw data (stat): 5403 (runsolver) R 5402 21152 21151 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 783784225 1052672 99 4294967295 134512640 135381576 3221224480 3221219688 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.0005 s]
Raw data (loadavg): 0.94 0.97 0.96 2/55 5407
Raw data (stat): 5403 (minisat+_script) S 5402 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783784225 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.0009 s]
Raw data (loadavg): 0.95 0.97 0.96 2/55 5407
Raw data (stat): 5403 (minisat+_script) S 5402 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783784225 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.0012 s]
Raw data (loadavg): 0.95 0.97 0.96 2/55 5407
Raw data (stat): 5403 (minisat+_script) S 5402 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783784225 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.97 0.96 2/55 5407
Raw data (stat): 5403 (minisat+_script) S 5402 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783784225 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.0025 s]
Raw data (loadavg): 0.97 0.97 0.96 2/55 5407
Raw data (stat): 5403 (minisat+_script) S 5402 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783784225 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.0029 s]
Raw data (loadavg): 0.97 0.97 0.96 2/55 5407
Raw data (stat): 5403 (minisat+_script) S 5402 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783784225 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.0028 s]
Raw data (loadavg): 0.97 0.97 0.96 2/55 5407
Raw data (stat): 5403 (minisat+_script) S 5402 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783784225 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.0053 s]
Raw data (loadavg): 0.98 0.97 0.96 3/55 5407
Raw data (stat): 5403 (minisat+_script) S 5402 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783784225 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.0052 s]
Raw data (loadavg): 0.98 0.97 0.96 2/55 5407
Raw data (stat): 5403 (minisat+_script) S 5402 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783784225 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.006 s]
Raw data (loadavg): 0.98 0.97 0.96 2/55 5407
Raw data (stat): 5403 (minisat+_script) S 5402 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783784225 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.007 s]
Raw data (loadavg): 0.99 0.97 0.96 2/55 5407
Raw data (stat): 5403 (minisat+_script) S 5402 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783784225 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.007 s]
Raw data (loadavg): 0.99 0.97 0.96 2/55 5407
Raw data (stat): 5403 (minisat+_script) S 5402 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783784225 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.008 s]
Raw data (loadavg): 0.99 0.97 0.96 2/55 5407
Raw data (stat): 5403 (minisat+_script) S 5402 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783784225 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.007 s]
Raw data (loadavg): 0.99 0.97 0.96 2/55 5407
Raw data (stat): 5403 (minisat+_script) S 5402 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783784225 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.008 s]
Raw data (loadavg): 0.99 0.97 0.96 2/55 5407
Raw data (stat): 5403 (minisat+_script) S 5402 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783784225 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.008 s]
Raw data (loadavg): 0.99 0.97 0.96 2/55 5407
Raw data (stat): 5403 (minisat+_script) S 5402 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783784225 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.008 s]
Raw data (loadavg): 0.99 0.97 0.96 2/55 5407
Raw data (stat): 5403 (minisat+_script) S 5402 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783784225 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.008 s]
Raw data (loadavg): 0.99 0.97 0.96 2/55 5407
Raw data (stat): 5403 (minisat+_script) S 5402 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783784225 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.009 s]
Raw data (loadavg): 0.99 0.97 0.96 2/55 5407
Raw data (stat): 5403 (minisat+_script) S 5402 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783784225 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.01 s]
Raw data (loadavg): 0.99 0.97 0.96 2/55 5407
Raw data (stat): 5403 (minisat+_script) S 5402 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783784225 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.009 s]
Raw data (loadavg): 0.99 0.97 0.96 2/55 5407
Raw data (stat): 5403 (minisat+_script) S 5402 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783784225 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.009 s]
Raw data (loadavg): 0.99 0.97 0.96 2/55 5407
Raw data (stat): 5403 (minisat+_script) S 5402 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783784225 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.01 s]
Raw data (loadavg): 0.99 0.97 0.96 2/55 5407
Raw data (stat): 5403 (minisat+_script) S 5402 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783784225 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.01 s]
Raw data (loadavg): 0.99 0.97 0.96 2/55 5407
Raw data (stat): 5403 (minisat+_script) S 5402 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783784225 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.011 s]
Raw data (loadavg): 0.99 0.97 0.96 2/55 5407
Raw data (stat): 5403 (minisat+_script) S 5402 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783784225 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.012 s]
Raw data (loadavg): 0.99 0.97 0.96 2/55 5407
Raw data (stat): 5403 (minisat+_script) S 5402 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783784225 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.012 s]
Raw data (loadavg): 0.99 0.97 0.96 2/55 5407
Raw data (stat): 5403 (minisat+_script) S 5402 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783784225 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.97 0.96 2/55 5407
Raw data (stat): 5403 (minisat+_script) S 5402 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783784225 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.013 s]
Raw data (loadavg): 0.99 0.97 0.96 2/55 5407
Raw data (stat): 5403 (minisat+_script) S 5402 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783784225 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.014 s]
Raw data (loadavg): 0.99 0.97 0.96 2/55 5407
Raw data (stat): 5403 (minisat+_script) S 5402 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783784225 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.014 s]
Raw data (loadavg): 0.99 0.97 0.96 2/55 5407
Raw data (stat): 5403 (minisat+_script) S 5402 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783784225 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.015 s]
Raw data (loadavg): 0.99 0.97 0.96 2/55 5407
Raw data (stat): 5403 (minisat+_script) S 5402 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783784225 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.016 s]
Raw data (loadavg): 0.99 0.97 0.96 2/55 5407
Raw data (stat): 5403 (minisat+_script) S 5402 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783784225 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.016 s]
Raw data (loadavg): 0.99 0.97 0.96 2/55 5407
Raw data (stat): 5403 (minisat+_script) S 5402 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783784225 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.016 s]
Raw data (loadavg): 0.99 0.97 0.96 2/55 5407
Raw data (stat): 5403 (minisat+_script) S 5402 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783784225 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.017 s]
Raw data (loadavg): 0.99 0.97 0.96 2/55 5407
Raw data (stat): 5403 (minisat+_script) S 5402 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783784225 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.017 s]
Raw data (loadavg): 0.99 0.97 0.96 2/55 5407
Raw data (stat): 5403 (minisat+_script) S 5402 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783784225 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.018 s]
Raw data (loadavg): 0.99 0.97 0.96 2/55 5407
Raw data (stat): 5403 (minisat+_script) S 5402 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783784225 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.019 s]
Raw data (loadavg): 0.99 0.97 0.96 2/55 5407
Raw data (stat): 5403 (minisat+_script) S 5402 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783784225 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.02 s]
Raw data (loadavg): 0.99 0.97 0.96 2/55 5407
Raw data (stat): 5403 (minisat+_script) S 5402 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783784225 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.02 s]
Raw data (loadavg): 0.99 0.97 0.96 2/55 5407
Raw data (stat): 5403 (minisat+_script) S 5402 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783784225 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.02 s]
Raw data (loadavg): 0.99 0.97 0.96 2/55 5407
Raw data (stat): 5403 (minisat+_script) S 5402 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783784225 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.02 s]
Raw data (loadavg): 0.99 0.97 0.96 2/55 5407
Raw data (stat): 5403 (minisat+_script) S 5402 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783784225 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.029 s]
Raw data (loadavg): 0.99 0.97 0.96 2/55 5407
Raw data (stat): 5403 (minisat+_script) S 5402 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783784225 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.032 s]
Raw data (loadavg): 0.99 0.97 0.96 2/55 5407
Raw data (stat): 5403 (minisat+_script) S 5402 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783784225 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.032 s]
Raw data (loadavg): 0.99 0.97 0.96 2/55 5407
Raw data (stat): 5403 (minisat+_script) S 5402 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783784225 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.032 s]
Raw data (loadavg): 0.99 0.97 0.96 2/55 5407
Raw data (stat): 5403 (minisat+_script) S 5402 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783784225 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.033 s]
Raw data (loadavg): 0.99 0.97 0.96 2/55 5407
Raw data (stat): 5403 (minisat+_script) S 5402 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783784225 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.048 s]
Raw data (loadavg): 0.99 0.97 0.96 2/55 5407
Raw data (stat): 5403 (minisat+_script) S 5402 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783784225 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.049 s]
Raw data (loadavg): 0.99 0.97 0.96 2/55 5407
Raw data (stat): 5403 (minisat+_script) S 5402 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783784225 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.049 s]
Raw data (loadavg): 0.99 0.97 0.96 2/55 5407
Raw data (stat): 5403 (minisat+_script) S 5402 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783784225 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.049 s]
Raw data (loadavg): 0.99 0.97 0.96 2/55 5407
Raw data (stat): 5403 (minisat+_script) S 5402 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783784225 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.049 s]
Raw data (loadavg): 0.99 0.97 0.96 2/55 5407
Raw data (stat): 5403 (minisat+_script) S 5402 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783784225 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.05 s]
Raw data (loadavg): 0.99 0.97 0.96 2/55 5407
Raw data (stat): 5403 (minisat+_script) S 5402 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783784225 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.05 s]
Raw data (loadavg): 0.99 0.97 0.96 2/55 5407
Raw data (stat): 5403 (minisat+_script) S 5402 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783784225 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.051 s]
Raw data (loadavg): 0.99 0.97 0.96 2/55 5407
Raw data (stat): 5403 (minisat+_script) S 5402 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783784225 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.052 s]
Raw data (loadavg): 0.99 0.97 0.96 2/55 5407
Raw data (stat): 5403 (minisat+_script) S 5402 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783784225 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.052 s]
Raw data (loadavg): 0.99 0.97 0.96 2/55 5407
Raw data (stat): 5403 (minisat+_script) S 5402 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783784225 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.052 s]
Raw data (loadavg): 0.99 0.97 0.96 2/55 5407
Raw data (stat): 5403 (minisat+_script) S 5402 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783784225 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.053 s]
Raw data (loadavg): 0.99 0.97 0.96 2/55 5407
Raw data (stat): 5403 (minisat+_script) S 5402 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783784225 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.053 s]
Raw data (loadavg): 0.99 0.97 0.96 2/55 5407
Raw data (stat): 5403 (minisat+_script) S 5402 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783784225 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.053 s]
Raw data (loadavg): 0.99 0.97 0.96 2/55 5407
Raw data (stat): 5403 (minisat+_script) S 5402 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783784225 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.054 s]
Raw data (loadavg): 0.99 0.97 0.96 2/55 5407
Raw data (stat): 5403 (minisat+_script) S 5402 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783784225 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.053 s]
Raw data (loadavg): 0.99 0.97 0.96 2/55 5407
Raw data (stat): 5403 (minisat+_script) S 5402 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783784225 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.054 s]
Raw data (loadavg): 0.99 0.97 0.96 2/55 5407
Raw data (stat): 5403 (minisat+_script) S 5402 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783784225 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.055 s]
Raw data (loadavg): 0.99 0.97 0.96 2/55 5407
Raw data (stat): 5403 (minisat+_script) S 5402 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783784225 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.055 s]
Raw data (loadavg): 0.99 0.97 0.96 2/55 5407
Raw data (stat): 5403 (minisat+_script) S 5402 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783784225 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.055 s]
Raw data (loadavg): 0.99 0.97 0.96 2/55 5407
Raw data (stat): 5403 (minisat+_script) S 5402 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783784225 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.056 s]
Raw data (loadavg): 0.99 0.97 0.96 2/55 5407
Raw data (stat): 5403 (minisat+_script) S 5402 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783784225 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.056 s]
Raw data (loadavg): 0.99 0.97 0.96 2/55 5407
Raw data (stat): 5403 (minisat+_script) S 5402 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783784225 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.057 s]
Raw data (loadavg): 0.99 0.97 0.96 2/55 5407
Raw data (stat): 5403 (minisat+_script) S 5402 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783784225 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.056 s]
Raw data (loadavg): 0.99 0.97 0.96 2/55 5407
Raw data (stat): 5403 (minisat+_script) S 5402 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783784225 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.057 s]
Raw data (loadavg): 0.99 0.97 0.96 2/55 5407
Raw data (stat): 5403 (minisat+_script) S 5402 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783784225 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.058 s]
Raw data (loadavg): 0.99 0.97 0.96 2/55 5407
Raw data (stat): 5403 (minisat+_script) S 5402 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783784225 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.058 s]
Raw data (loadavg): 0.99 0.97 0.96 2/55 5407
Raw data (stat): 5403 (minisat+_script) S 5402 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783784225 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.059 s]
Raw data (loadavg): 0.99 0.97 0.96 2/55 5407
Raw data (stat): 5403 (minisat+_script) S 5402 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783784225 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.059 s]
Raw data (loadavg): 0.99 0.97 0.96 2/55 5407
Raw data (stat): 5403 (minisat+_script) S 5402 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783784225 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.06 s]
Raw data (loadavg): 0.99 0.97 0.96 2/55 5407
Raw data (stat): 5403 (minisat+_script) S 5402 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783784225 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.059 s]
Raw data (loadavg): 0.99 0.97 0.96 2/55 5407
Raw data (stat): 5403 (minisat+_script) S 5402 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783784225 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.061 s]
Raw data (loadavg): 0.99 0.97 0.96 2/55 5407
Raw data (stat): 5403 (minisat+_script) S 5402 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783784225 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.061 s]
Raw data (loadavg): 0.99 0.97 0.96 2/55 5407
Raw data (stat): 5403 (minisat+_script) S 5402 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783784225 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.061 s]
Raw data (loadavg): 0.99 0.97 0.96 2/55 5407
Raw data (stat): 5403 (minisat+_script) S 5402 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783784225 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.061 s]
Raw data (loadavg): 0.99 0.97 0.96 2/55 5407
Raw data (stat): 5403 (minisat+_script) S 5402 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783784225 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.062 s]
Raw data (loadavg): 0.99 0.97 0.96 2/55 5407
Raw data (stat): 5403 (minisat+_script) S 5402 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783784225 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.066 s]
Raw data (loadavg): 0.99 0.97 0.96 2/55 5407
Raw data (stat): 5403 (minisat+_script) S 5402 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783784225 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.067 s]
Raw data (loadavg): 0.99 0.97 0.96 2/55 5407
Raw data (stat): 5403 (minisat+_script) S 5402 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783784225 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.067 s]
Raw data (loadavg): 0.99 0.97 0.96 2/55 5407
Raw data (stat): 5403 (minisat+_script) S 5402 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783784225 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.067 s]
Raw data (loadavg): 0.99 0.97 0.96 2/55 5407
Raw data (stat): 5403 (minisat+_script) S 5402 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783784225 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.067 s]
Raw data (loadavg): 0.99 0.97 0.96 2/55 5407
Raw data (stat): 5403 (minisat+_script) S 5402 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783784225 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.068 s]
Raw data (loadavg): 0.99 0.97 0.96 2/55 5407
Raw data (stat): 5403 (minisat+_script) S 5402 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783784225 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.069 s]
Raw data (loadavg): 0.99 0.97 0.96 2/55 5407
Raw data (stat): 5403 (minisat+_script) S 5402 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783784225 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.069 s]
Raw data (loadavg): 0.99 0.97 0.96 2/55 5407
Raw data (stat): 5403 (minisat+_script) S 5402 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783784225 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.07 s]
Raw data (loadavg): 0.99 0.97 0.96 2/55 5407
Raw data (stat): 5403 (minisat+_script) S 5402 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783784225 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.069 s]
Raw data (loadavg): 0.99 0.97 0.96 2/55 5407
Raw data (stat): 5403 (minisat+_script) S 5402 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783784225 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.07 s]
Raw data (loadavg): 0.99 0.97 0.96 2/55 5407
Raw data (stat): 5403 (minisat+_script) S 5402 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783784225 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.07 s]
Raw data (loadavg): 0.99 0.97 0.96 2/55 5407
Raw data (stat): 5403 (minisat+_script) S 5402 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783784225 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.07 s]
Raw data (loadavg): 0.99 0.97 0.96 2/55 5407
Raw data (stat): 5403 (minisat+_script) S 5402 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783784225 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.071 s]
Raw data (loadavg): 0.99 0.97 0.96 2/55 5407
Raw data (stat): 5403 (minisat+_script) S 5402 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783784225 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.071 s]
Raw data (loadavg): 0.99 0.97 0.96 2/55 5407
Raw data (stat): 5403 (minisat+_script) S 5402 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783784225 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.07 s]
Raw data (loadavg): 0.99 0.97 0.96 2/55 5407
Raw data (stat): 5403 (minisat+_script) S 5402 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783784225 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.07 s]
Raw data (loadavg): 0.99 0.97 0.96 2/55 5407
Raw data (stat): 5403 (minisat+_script) S 5402 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783784225 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.08 s]
Raw data (loadavg): 0.99 0.97 0.96 2/55 5407
Raw data (stat): 5403 (minisat+_script) S 5402 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783784225 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.08 s]
Raw data (loadavg): 0.99 0.97 0.96 2/55 5407
Raw data (stat): 5403 (minisat+_script) S 5402 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783784225 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.08 s]
Raw data (loadavg): 0.99 0.97 0.96 2/55 5407
Raw data (stat): 5403 (minisat+_script) S 5402 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783784225 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.09 s]
Raw data (loadavg): 0.99 0.97 0.96 2/55 5407
Raw data (stat): 5403 (minisat+_script) S 5402 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783784225 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.09 s]
Raw data (loadavg): 0.99 0.97 0.96 2/55 5407
Raw data (stat): 5403 (minisat+_script) S 5402 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783784225 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.09 s]
Raw data (loadavg): 0.99 0.97 0.96 2/55 5407
Raw data (stat): 5403 (minisat+_script) S 5402 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783784225 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.09 s]
Raw data (loadavg): 0.99 0.97 0.96 2/55 5407
Raw data (stat): 5403 (minisat+_script) S 5402 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783784225 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.09 s]
Raw data (loadavg): 0.99 0.97 0.96 2/55 5407
Raw data (stat): 5403 (minisat+_script) S 5402 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783784225 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.09 s]
Raw data (loadavg): 0.99 0.97 0.96 2/55 5407
Raw data (stat): 5403 (minisat+_script) S 5402 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783784225 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.09 s]
Raw data (loadavg): 0.99 0.97 0.96 2/55 5407
Raw data (stat): 5403 (minisat+_script) S 5402 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783784225 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.09 s]
Raw data (loadavg): 0.99 0.97 0.96 2/55 5407
Raw data (stat): 5403 (minisat+_script) S 5402 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783784225 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.09 s]
Raw data (loadavg): 0.99 0.97 0.96 2/55 5407
Raw data (stat): 5403 (minisat+_script) S 5402 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783784225 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.09 s]
Raw data (loadavg): 0.99 0.97 0.96 2/55 5407
Raw data (stat): 5403 (minisat+_script) S 5402 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783784225 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.09 s]
Raw data (loadavg): 0.99 0.97 0.96 2/55 5407
Raw data (stat): 5403 (minisat+_script) S 5402 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783784225 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.09 s]
Raw data (loadavg): 0.99 0.97 0.96 2/55 5407
Raw data (stat): 5403 (minisat+_script) S 5402 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783784225 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.09 s]
Raw data (loadavg): 0.99 0.97 0.96 2/55 5407
Raw data (stat): 5403 (minisat+_script) S 5402 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783784225 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.09 s]
Raw data (loadavg): 0.99 0.97 0.96 2/55 5407
Raw data (stat): 5403 (minisat+_script) S 5402 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783784225 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.09 s]
Raw data (loadavg): 0.99 0.97 0.96 2/55 5407
Raw data (stat): 5403 (minisat+_script) S 5402 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783784225 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.09 s]
Raw data (loadavg): 0.99 0.97 0.96 2/55 5407
Raw data (stat): 5403 (minisat+_script) S 5402 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783784225 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.09 s]
Raw data (loadavg): 0.99 0.97 0.96 2/55 5407
Raw data (stat): 5403 (minisat+_script) S 5402 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783784225 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.09 s]
Raw data (loadavg): 0.99 0.97 0.96 2/55 5407
Raw data (stat): 5403 (minisat+_script) S 5402 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783784225 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.73 s]
Raw data (loadavg): 0.99 0.97 0.96 1/53 5407
Raw data (stat): 5403 (minisat+_script) S 5402 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783784225 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.73
CPU time (s): 1229.88
CPU user time (s): 1229.14
CPU system time (s): 0.738887
CPU usage (%): 100.012
Max. virtual memory (Kb): 2124
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####